% time ./darwin_linux_v1.4.4 --finite-domain true --print-model-finite true sudoku-darwin.tptp Darwin 1.4.4 Finite Domain: setting initial domain size to 1. Finite Domain: using non-ground splitting in preprocessing. Parsing sudoku-darwin.tptp ... Calling eprover for clausification ... Configuration: --resolve : true --subsume : true --compact : true --productivity : true --mixed-literals : true --finite-domain : true --finite-domain-functionality : true --unique-name-assumption : false --lemma : Grounded --lemma-min : 1000 --lemma-max : 5000 --lemma-uip : false --lemma-parametric-assert : 0 --plus-v : false --equality : Axioms --backtracking : Backjumping --iterative-deepening : TermDepth --depth-bound : 1 --max-depth-bound : 0 --lookahead-all : false --restart : Lazy --neg-assert-candidates : Use --eprover : --preprocess-split : NonGround --preprocess-unit : true --preprocess-pure : false --preprocess-resolution : false --preprocess-equality : true --input-format : tptp --timeout-cpu : 0. --timeout-wc : 0. --memory-limit : 0 --print-level : 1 --print-configuration : true --print-preprocess-split : false --print-preprocess-unit : false --print-preprocess-resolution : false --print-preprocess-pure : false --print-preprocess-equality : false --print-equality-axioms : false --print-lemmas : false --print-fd-sorts : false --print-fd-transformation : false --print-fd-axioms : false --print-fd-problem : Silent --print-statistics : true --print-context : false --print-context-file : --print-DIG : false --print-DIG-file : --print-model-finite : true --print-model-tptp : false --print-model-tptp-file : --print-derivation-online : false --print-context-unifier : false --print-assert-candidates : false --print-split-candidates : false --print-constants : false Problem: Horn : false BS : false Equality : true Proving ... SZS status Satisfiable for sudoku-darwin.tptp MODEL (Multiplication Tables): SZS output start FiniteModel for sudoku-darwin.tptp Domain size: 9 Constants: n1 = '1 n2 = '2 n3 = '3 n4 = '4 n5 = '5 n6 = '6 n7 = '7 n8 = '8 n9 = '9 Functions: esk10_1('1) = '2 esk10_1('2) = '1 esk10_1('3) = '1 esk10_1('4) = '3 esk10_1('5) = '2 esk10_1('6) = '1 esk10_1('7) = '2 esk10_1('8) = '3 esk10_1('9) = '3 esk11_1('1) = '5 esk11_1('2) = '4 esk11_1('3) = '6 esk11_1('4) = '4 esk11_1('5) = '5 esk11_1('6) = '6 esk11_1('7) = '4 esk11_1('8) = '5 esk11_1('9) = '6 esk12_1('1) = '4 esk12_1('2) = '5 esk12_1('3) = '4 esk12_1('4) = '4 esk12_1('5) = '5 esk12_1('6) = '6 esk12_1('7) = '6 esk12_1('8) = '6 esk12_1('9) = '5 esk13_1('1) = '6 esk13_1('2) = '5 esk13_1('3) = '4 esk13_1('4) = '6 esk13_1('5) = '4 esk13_1('6) = '5 esk13_1('7) = '6 esk13_1('8) = '4 esk13_1('9) = '5 esk14_1('1) = '8 esk14_1('2) = '9 esk14_1('3) = '8 esk14_1('4) = '7 esk14_1('5) = '7 esk14_1('6) = '8 esk14_1('7) = '9 esk14_1('8) = '9 esk14_1('9) = '7 esk15_1('1) = '9 esk15_1('2) = '7 esk15_1('3) = '9 esk15_1('4) = '8 esk15_1('5) = '9 esk15_1('6) = '7 esk15_1('7) = '8 esk15_1('8) = '7 esk15_1('9) = '8 esk16_1('1) = '3 esk16_1('2) = '3 esk16_1('3) = '2 esk16_1('4) = '1 esk16_1('5) = '1 esk16_1('6) = '2 esk16_1('7) = '3 esk16_1('8) = '1 esk16_1('9) = '2 esk17_1('1) = '8 esk17_1('2) = '9 esk17_1('3) = '7 esk17_1('4) = '7 esk17_1('5) = '8 esk17_1('6) = '8 esk17_1('7) = '9 esk17_1('8) = '9 esk17_1('9) = '7 esk18_1('1) = '5 esk18_1('2) = '6 esk18_1('3) = '6 esk18_1('4) = '5 esk18_1('5) = '6 esk18_1('6) = '4 esk18_1('7) = '5 esk18_1('8) = '4 esk18_1('9) = '4 esk19_1('1) = '7 esk19_1('2) = '8 esk19_1('3) = '8 esk19_1('4) = '9 esk19_1('5) = '7 esk19_1('6) = '9 esk19_1('7) = '7 esk19_1('8) = '8 esk19_1('9) = '9 esk20_1('1) = '9 esk20_1('2) = '7 esk20_1('3) = '9 esk20_1('4) = '9 esk20_1('5) = '8 esk20_1('6) = '7 esk20_1('7) = '7 esk20_1('8) = '8 esk20_1('9) = '8 esk3_1('1) = '1 esk3_1('2) = '2 esk3_1('3) = '3 esk3_1('4) = '1 esk3_1('5) = '1 esk3_1('6) = '2 esk3_1('7) = '2 esk3_1('8) = '3 esk3_1('9) = '3 esk4_1('1) = '1 esk4_1('2) = '2 esk4_1('3) = '3 esk4_1('4) = '2 esk4_1('5) = '3 esk4_1('6) = '3 esk4_1('7) = '1 esk4_1('8) = '2 esk4_1('9) = '1 esk5_1('1) = '2 esk5_1('2) = '1 esk5_1('3) = '2 esk5_1('4) = '3 esk5_1('5) = '2 esk5_1('6) = '3 esk5_1('7) = '3 esk5_1('8) = '1 esk5_1('9) = '1 esk6_1('1) = '6 esk6_1('2) = '4 esk6_1('3) = '5 esk6_1('4) = '6 esk6_1('5) = '4 esk6_1('6) = '5 esk6_1('7) = '4 esk6_1('8) = '5 esk6_1('9) = '6 esk7_1('1) = '3 esk7_1('2) = '3 esk7_1('3) = '1 esk7_1('4) = '2 esk7_1('5) = '3 esk7_1('6) = '1 esk7_1('7) = '1 esk7_1('8) = '2 esk7_1('9) = '2 esk8_1('1) = '7 esk8_1('2) = '8 esk8_1('3) = '7 esk8_1('4) = '8 esk8_1('5) = '9 esk8_1('6) = '9 esk8_1('7) = '8 esk8_1('8) = '7 esk8_1('9) = '9 esk9_1('1) = '4 esk9_1('2) = '6 esk9_1('3) = '5 esk9_1('4) = '5 esk9_1('5) = '6 esk9_1('6) = '4 esk9_1('7) = '5 esk9_1('8) = '6 esk9_1('9) = '4 a('1, '1) = '1 a('1, '2) = '4 a('1, '3) = '5 a('1, '4) = '2 a('1, '5) = '8 a('1, '6) = '9 a('1, '7) = '3 a('1, '8) = '7 a('1, '9) = '6 a('2, '1) = '7 a('2, '2) = '2 a('2, '3) = '6 a('2, '4) = '5 a('2, '5) = '3 a('2, '6) = '1 a('2, '7) = '8 a('2, '8) = '4 a('2, '9) = '9 a('3, '1) = '9 a('3, '2) = '8 a('3, '3) = '3 a('3, '4) = '7 a('3, '5) = '6 a('3, '6) = '4 a('3, '7) = '1 a('3, '8) = '2 a('3, '9) = '5 a('4, '1) = '6 a('4, '2) = '1 a('4, '3) = '9 a('4, '4) = '4 a('4, '5) = '2 a('4, '6) = '7 a('4, '7) = '5 a('4, '8) = '3 a('4, '9) = '8 a('5, '1) = '3 a('5, '2) = '7 a('5, '3) = '4 a('5, '4) = '1 a('5, '5) = '5 a('5, '6) = '8 a('5, '7) = '9 a('5, '8) = '6 a('5, '9) = '2 a('6, '1) = '2 a('6, '2) = '5 a('6, '3) = '8 a('6, '4) = '3 a('6, '5) = '9 a('6, '6) = '6 a('6, '7) = '4 a('6, '8) = '1 a('6, '9) = '7 a('7, '1) = '8 a('7, '2) = '6 a('7, '3) = '2 a('7, '4) = '9 a('7, '5) = '4 a('7, '6) = '3 a('7, '7) = '7 a('7, '8) = '5 a('7, '9) = '1 a('8, '1) = '4 a('8, '2) = '9 a('8, '3) = '7 a('8, '4) = '6 a('8, '5) = '1 a('8, '6) = '5 a('8, '7) = '2 a('8, '8) = '8 a('8, '9) = '3 a('9, '1) = '5 a('9, '2) = '3 a('9, '3) = '1 a('9, '4) = '8 a('9, '5) = '7 a('9, '6) = '2 a('9, '7) = '6 a('9, '8) = '9 a('9, '9) = '4 esk1_2('1, '1) = '1 esk1_2('1, '2) = '6 esk1_2('1, '3) = '7 esk1_2('1, '4) = '2 esk1_2('1, '5) = '4 esk1_2('1, '6) = '8 esk1_2('1, '7) = '9 esk1_2('1, '8) = '5 esk1_2('1, '9) = '3 esk1_2('2, '1) = '4 esk1_2('2, '2) = '2 esk1_2('2, '3) = '8 esk1_2('2, '4) = '5 esk1_2('2, '5) = '9 esk1_2('2, '6) = '1 esk1_2('2, '7) = '3 esk1_2('2, '8) = '7 esk1_2('2, '9) = '6 esk1_2('3, '1) = '7 esk1_2('3, '2) = '5 esk1_2('3, '3) = '3 esk1_2('3, '4) = '8 esk1_2('3, '5) = '1 esk1_2('3, '6) = '4 esk1_2('3, '7) = '6 esk1_2('3, '8) = '9 esk1_2('3, '9) = '2 esk1_2('4, '1) = '2 esk1_2('4, '2) = '8 esk1_2('4, '3) = '6 esk1_2('4, '4) = '4 esk1_2('4, '5) = '3 esk1_2('4, '6) = '7 esk1_2('4, '7) = '5 esk1_2('4, '8) = '1 esk1_2('4, '9) = '9 esk1_2('5, '1) = '3 esk1_2('5, '2) = '4 esk1_2('5, '3) = '9 esk1_2('5, '4) = '7 esk1_2('5, '5) = '5 esk1_2('5, '6) = '2 esk1_2('5, '7) = '8 esk1_2('5, '8) = '6 esk1_2('5, '9) = '1 esk1_2('6, '1) = '9 esk1_2('6, '2) = '3 esk1_2('6, '3) = '5 esk1_2('6, '4) = '1 esk1_2('6, '5) = '8 esk1_2('6, '6) = '6 esk1_2('6, '7) = '2 esk1_2('6, '8) = '4 esk1_2('6, '9) = '7 esk1_2('7, '1) = '8 esk1_2('7, '2) = '1 esk1_2('7, '3) = '4 esk1_2('7, '4) = '6 esk1_2('7, '5) = '2 esk1_2('7, '6) = '9 esk1_2('7, '7) = '7 esk1_2('7, '8) = '3 esk1_2('7, '9) = '5 esk1_2('8, '1) = '5 esk1_2('8, '2) = '7 esk1_2('8, '3) = '2 esk1_2('8, '4) = '9 esk1_2('8, '5) = '6 esk1_2('8, '6) = '3 esk1_2('8, '7) = '1 esk1_2('8, '8) = '8 esk1_2('8, '9) = '4 esk1_2('9, '1) = '6 esk1_2('9, '2) = '9 esk1_2('9, '3) = '1 esk1_2('9, '4) = '3 esk1_2('9, '5) = '7 esk1_2('9, '6) = '5 esk1_2('9, '7) = '4 esk1_2('9, '8) = '2 esk1_2('9, '9) = '8 esk2_2('1, '1) = '1 esk2_2('1, '2) = '4 esk2_2('1, '3) = '9 esk2_2('1, '4) = '5 esk2_2('1, '5) = '8 esk2_2('1, '6) = '2 esk2_2('1, '7) = '3 esk2_2('1, '8) = '6 esk2_2('1, '9) = '7 esk2_2('2, '1) = '6 esk2_2('2, '2) = '2 esk2_2('2, '3) = '7 esk2_2('2, '4) = '1 esk2_2('2, '5) = '4 esk2_2('2, '6) = '9 esk2_2('2, '7) = '8 esk2_2('2, '8) = '3 esk2_2('2, '9) = '5 esk2_2('3, '1) = '5 esk2_2('3, '2) = '9 esk2_2('3, '3) = '3 esk2_2('3, '4) = '6 esk2_2('3, '5) = '2 esk2_2('3, '6) = '7 esk2_2('3, '7) = '1 esk2_2('3, '8) = '4 esk2_2('3, '9) = '8 esk2_2('4, '1) = '8 esk2_2('4, '2) = '1 esk2_2('4, '3) = '5 esk2_2('4, '4) = '4 esk2_2('4, '5) = '7 esk2_2('4, '6) = '3 esk2_2('4, '7) = '6 esk2_2('4, '8) = '2 esk2_2('4, '9) = '9 esk2_2('5, '1) = '9 esk2_2('5, '2) = '6 esk2_2('5, '3) = '1 esk2_2('5, '4) = '2 esk2_2('5, '5) = '5 esk2_2('5, '6) = '8 esk2_2('5, '7) = '4 esk2_2('5, '8) = '7 esk2_2('5, '9) = '3 esk2_2('6, '1) = '4 esk2_2('6, '2) = '7 esk2_2('6, '3) = '2 esk2_2('6, '4) = '8 esk2_2('6, '5) = '3 esk2_2('6, '6) = '6 esk2_2('6, '7) = '9 esk2_2('6, '8) = '5 esk2_2('6, '9) = '1 esk2_2('7, '1) = '2 esk2_2('7, '2) = '5 esk2_2('7, '3) = '8 esk2_2('7, '4) = '3 esk2_2('7, '5) = '9 esk2_2('7, '6) = '4 esk2_2('7, '7) = '7 esk2_2('7, '8) = '1 esk2_2('7, '9) = '6 esk2_2('8, '1) = '7 esk2_2('8, '2) = '3 esk2_2('8, '3) = '6 esk2_2('8, '4) = '9 esk2_2('8, '5) = '1 esk2_2('8, '6) = '5 esk2_2('8, '7) = '2 esk2_2('8, '8) = '8 esk2_2('8, '9) = '4 esk2_2('9, '1) = '3 esk2_2('9, '2) = '8 esk2_2('9, '3) = '4 esk2_2('9, '4) = '7 esk2_2('9, '5) = '6 esk2_2('9, '6) = '1 esk2_2('9, '7) = '5 esk2_2('9, '8) = '9 esk2_2('9, '9) = '2 Predicates: r1: r1('1) r1('2) r1('3) r2: r2('4) r2('5) r2('6) r3: r3('7) r3('8) r3('9) SZS output end FiniteModel for sudoku-darwin.tptp Statistics: Close : 263 Assert : 7698 Split : 530 Resolve : 1296 Subsume : 232 Compact : 0 Productivity Filtered : 254 Assert Candidates : 30765 Split Candidates : 6095136 Jumps : 0 Debug : 0 Global Debug : 0 Global Debug2 : 0 Maximum Context Size : 5639 Incomplete Branches : 0 Restarts : 0 Bound : 9 Lemmas : 197 CPU Time (s) : 128.1 Memory (MB) : 16 ./darwin_linux_v1.4.4 --finite-domain true --print-model-finite 127.96s user 0.11s system 99% cpu 2:08.55 total %