#!/usr/bin/php 1, 'Satz2.2' => 1, 'Satz2.3' => 2, 'Satz2.4' => 1, 'Satz2.5' => 1, 'Satz2.8' => array(5,"diagram"), 'Satz2.11' => 14, 'Satz2.12' => 5, 'Satz2.13' => 1, 'Satz2.14' => 2, 'Satz2.15' => array(13,"hints"), // can be proved from 3.1 without hints 'Satz3.1' => array(2,"sos"), // array(4, "diagram"), 'Satz3.2' => 4, 'Satz3.3' => 1, 'Satz3.4' => 9, 'Satz3.5a' => 4, 'Satz3.6a' => 4, 'Satz3.5b' => 5, 'Satz3.6b' => 4, 'Satz3.7a' => 8, // diagram not needed 'Satz3.7b' => 2, 'Satz3.13a' => 1, 'Satz3.13b' => 1, 'Satz3.14a' => 0, 'Satz3.14b' => 3, 'Satz3.17' => array(8, "diagram"), 'Satz4.2' => array(44,"hints"), // 46 by hand 'Satz4.3' => array(4, "max_seconds = 300"), // 256 seconds required 'Satz4.5' => array(24, "subformula", 60), // array(24,"hints"), // 24 by hand // awaiting replacement with Wos's proof 'Satz4.6' => array(11, "explicit equality axioms"), // 10 by hand 'Satz4.11a' => 3, 'Satz4.11b' => 2, 'Satz4.11c' => 7, 'Satz4.11d' => 2, 'Satz4.11e' => 2, 'Satz4.12' => 1, 'Satz4.12b' => 1, 'Satz4.13' => 16, 'Satz4.14' => array(27, "diagram"), 'Satz4.16' => array(25, "hints", "max_weight = 9", "max_seconds = 300"), // or array(81, "max_weight = 9" ,"max_seconds = 100000"), // 25 steps in 231 seconds using hints, or 81 steps in 95696.25 seconds by just waiting 'Satz4.17' => 2, 'Satz4.18' => 5, 'Satz4.19' => 12, 'Satz5.1' => array(127, "hints"), 'Satz5.2' => 3, // less than 20 seconds 'Satz5.3' => 15, // less than 120 seconds 'Satz5.5a' => 17, 'Satz5.5b' => 8, 'Satz5.6' => 7, 'Satz5.7' => 1, // less than 20 seconds 'Satz5.8' => 8, // required more than 20 seconds 'Satz5.9' => array(20, "diagram"), 'Satz5.10' => 5, 'Satz5.11' => 1, // less than 20 seconds 'Satz5.12a1'=> 1, // less than 20 seconds 'Satz5.12a2'=> 2, // less than 20 seconds 'Satz5.12b' => array(20, "subformula",227), // array(16, "hints"), 'NarbouxLemma1' => 4, // Experiment 66, Chapter 6 without diagrams, 20 seconds proves all but 6.11a and 6.16.b // Experiment 67, with sos, 20 seconds, no result // Experiment 68, Chapter 6 with diagrams // Experiment 74, Chapter 6 with hints // TestChapter run 9.16.15 'Satz6.2a' => 11, 'Satz6.2b' => 5, 'Satz6.3a' => 7, 'Satz6.3b' => 1, 'Satz6.4a' => 13, 'Satz6.4b' => 11, 'Satz6.5' => 3, 'Satz6.6' => 5, 'Satz6.7' => 9, 'Satz6.11a' => array(21, "diagram"), 'Satz6.11b' => 17, 'Satz6.13a' => 11, 'Satz6.13b' => 1, 'Satz6.15a' => 10, 'Satz6.15b' => 1, 'Satz6.15c' => 9, 'Satz6.15d' => 1, 'Satz6.16a' => 8, 'Satz6.16b' => array(29, "subformula", 1881), // array(46, "hints"), 'Satz6.17a' => 1, 'Satz6.17b' => 1, 'Satz6.18' => 19, 'Satz6.21' => 9, 'Satz6.25' => 3, 'Satz6.28' => array(21, "hints"), // needs max_vars = 4 'Satz7.2' => 4, 'Satz7.3a' => 2, 'Satz7.3b' => 2, 'Satz7.4a' => 2, 'Satz7.4b' => 19, 'Satz7.6' => 1, 'Satz7.7' => 2, 'Satz7.8' => 5, 'Satz7.9' => 1, 'Satz7.10a' => 3, 'Satz7.10b' => 4, 'Satz7.13' => array(99, "subformula", 921), // array(72, "hints"), // our proof is 77 steps 'Satz7.15a' => 1, 'Satz7.15b' => 2, 'Satz7.16a' => 2, 'Satz7.16b' => 4, 'Satz7.17' => 17, 'Satz7.18' => 2, 'Satz7.19' => array(7, "subformula"), // array(6, "hints"), // our proof is 9 steps, has hints and a diagram 'Satz7.20' => 9, 'Satz7.21' => array(26, "hints"), // our proof is 31 steps 'Satz7.22a' => array(108, "subformula", 3189), // array(96,"hints"), // our proof is 132 steps 'Satz7.22b' => 12, 'Satz7.22' => 2, 'Satz7.25' => array(114, "hints"), // our proof is 123 steps // Chapter 8 checked on 9.22.13 with max_weight 9, 120 seconds, which did not prove 8.2, 8.12a, 8.13b, 8.14c, and 8.21. // tried again with max_weight 14, 120 seconds; then 8.2, 8.12a, and 8.14c proved // tried again with max_weight 20, 120 seconds; that proved 8.21 but not 8.13b // Actually, 8.13b needs its diagram in the .prf file, so it's correct that it doesn't prove without it. 'Satz8.2' => 5, 'Satz8.3' => 13, 'Satz8.4' => 3, 'Satz8.5' => 4, 'Satz8.6' => 10, 'Satz8.7' => array(23, "subformula",29), // array(23, "hints"), 'Satz8.8' => 3, 'Satz8.9' => 2, 'Satz8.10' => array(30, "diagram"), // 28 steps 'Satz8.12a' => 10, 'Satz8.12b' => 3, 'Satz8.13a' => 29, 'Satz8.13b' => array(15, "diagram"), // 16 steps 'Satz8.14a' => array(11, "diagram"), 'Satz8.14b' => array(13, "subformula", 332), // array(7, "hints"), 'Satz8.14c' => 6, 'Satz8.15' => 2, 'Satz8.16a' => 5, 'Satz8.16b' => 14, 'Satz8.18a' => 12, 'Satz8.18' => array(209, "hints", "max_seconds = 40"), // 23 seconds 'Satz8.20a' => array(30, "hints"), // 36 steps 'Satz8.20b'=> array(8, "diagram"), 'perp1' => array(16,"diagram"), 'Satz8.21a' => array(98, "hints"), // 127 steps 'Satz8.21' => 6, 'Satz8.22b' => array(182,"hints","max_weight = 7"), // 9.24 seconds 'Satz8.22' => array(22,"hints"), // 23 steps 'Satz8.24a' => array(177, "hints", "max_seconds = 60"), // 42 seconds 'Satz8.24b' => array(154, "hints", "max_seconds = 60"), // 43 seconds 'Satz8.24' => array(3, "diagram"), // Experiment 79, Chapter 9 with no diagrams, 20 seconds, proves 9.2 only // Experiment 80, Chapter 9 with diagrams, no results // Experiment 82, Chapter 9 with hints, 60 seconds // 9.18.15, TestSubformulaStrategy run with one hour per problem // 9.19.15, TestChapter run with $check_only_simple, max_weight 9, 20 seconds gets 9.2 and 9.16 // 9.30.15, 9.19b requires max_weight = 7, and 9.16 requires a diagram. 'Satz9.2' => 10, 'Satz9.3a' => array(25, "subformula", 46), // array(25, "hints"), // 27 steps 'Satz9.3' => array(50, "hints"), // 52 steps 'SideReflect' => array(26, "subformula", 49), // array(26, "hints"), //52 steps 'Satz9.4a' => array(40, "hints"), 'Satz9.4a2' => array(35, "hints"), // 35 steps 'Satz9.4b' => array(42,"hints"), // 48 steps 'Satz9.4' => array(9, "max_weight = 9", "max_seconds = 450"), // 350 seconds 'Satz9.4c' => array(41, "hints"), // 48 steps 'Satz9.5' => array(30, "subformula",820), // array(12, "hints"), // 38 steps 'Satz9.6' => array(98, "subformula", 186), // array(91, "hints"), // 111 steps 'Satz9.8' => array(63, "subformula", 1646), //array(48, "hints"), // 52 steps 'Satz9.9' => array(6, "max_weight = 8", "max_seconds = 4000"), 'Satz9.13' => array(65, "hints"), 'Satz9.16' => array(14, "max_weight = 5"), // 7 seconds 'Satz9.19b' => array(8, "max_weight = 7"), // 11 seconds // TestChapter run on Chapter 8A, 9.23.15 and again 9.29.15 'ext1' => 2, 'ExtCol2' => 2, 'ExtPerp' => array(36,"hints"), // 44 steps 'ExtPerp2' => array(7,"diagram","max_weight = 7"), // Takes 75 seconds with diagram and max_weight 7. We found 3 steps // max_weight 8 'ExtPerp3' => 3, // 21 seconds. 'ExtPerp4' => 3, // 'ExtPerp5' => 8, 'ExtPerp6' => 3, // 62 seconds // TestChapter run on Chapter 9A, 9.23.15 and again 9.29.15 'ExtSameSide1' => array(16, "hints"), 'ExtSameSide2'=> array(16, "hints"), 'Lemma9.13a' => 1, 'Lemma9.13b' => 15, // 69 seconds 'Lemma9.13c' => array(11, "max_seconds = 140"), // 120 seconds (plus or minus a fraction of a second!) 'Lemma9.13d' => 11, // 68 seconds 'Lemma9.13e' => 3, 'Lemma9.13g' => array(22,"hints"), 'Lemma9.13f-case1' => array(40,"hints"), 'Lemma9.13f-case2' => array(42,"hints"), 'Lemma9.13f' => 1, // Experiment 33, Chapter 9A with diagrams, 20 seconds. Nothing more proves. // Experiment 34, Chapter 10 without diagrams, 20 seconds. We got a bunch of // bogus proofs, exposing the incorrect positive form of Satz10.2a. Ran it again: // 9.18.15, ran TestChapter on Chapter 10 with diagrams, but no hints, 60 seconds--no results. // Then tried hints, with 120 seconds. // 9.19.15, started TestChapter again, messing up the input files, oops. // 9.19.15, ran TestChapter with hints on, only proved 10.4. // 9.22.15 TestChapter ran successfully // 9.29.15, TestChapter failed to prove 10.7 and 10.8a as well as 10.2b, but // that's because those need special settings that weren't in the code. 'Satz10.2a' =>array(45, "hints"), 'Satz10.2b' => array(49, "hints"), 'Satz10.4' => array(17, "hints"), 'Satz10.5' => 4, 'Satz10.6' => 6, 'Satz10.7' => array(3, "max_weight = 15", "ratio = 1"), 'Satz10.8a' => 5, // or array(3, "hints"), 'Satz10.8a' => array(3, "max_weight = 15", "ratio = 1"), // same settings also worked here 'Satz10.8b' => 3, 'Satz10.10a' => array(13, "hints"), // 33 steps 'Satz10.10' => array(72, "hints"), // 92 steps 'Satz10.12b' => array(91, "hints", "max_weight = 8"), // 100 steps, but using illegal demodulators 'Satz10.12c' => 18, // 11 steps, after using the steps of this one as hints 'Satz10.12a' => array(60, "hints"), // 71 steps 'Satz10.12' => array(26, "hints"), // 26 steps 'Satz10.14' => array(10, "diagram", "max_weight = 10"), 'Satz10.15' => array(74, "hints"), // 78 steps 'Satz10.16a' => array(44, "hints"), // 58 steps 'Satz10.16b' => array(56, "hints"), // 87 steps // TestChapter run 9.30.15 'Satz11.3a' => array(43, "hints", "max_seconds = 200"), 'Satz11.3d' => array(6, "hints"), 'Satz11.4b' => array(37, "hints"), 'Satz11.4' => array(39,"hints"), 'Satz11.4d' => 6, 'Satz11.6' => 1, 'Satz11.7' => array(8, "hints", 8, "diagram", "max_seconds = 1700"), 'Satz11.8' => array(34, "hints"), 'Satz11.9' => 1, 'Satz11.15a' => array(78, "hints"), 'Satz11.15b' =>array(51, "hints"), // 18 seconds, max_vars = 4 required 'Satz11.49a' =>array(5, "hints"), 'Satz11.49b' => array(15, "hints"), // TestChapter run 9.28.15 'ExtParallel' => array(24,"hints"), 'Satz12.6' => array(16,"hints"), // max_weight 6 is enough 'Lemma12.11-case1' => array(8, "hints"), 'Lemma12.11-case2' => array(32, "hints", "max_seconds = 1200"), // 763 with max_vars 3 and pick_given 2, 827 with max_vars 4 and pick_given 4 and max_weight 8 'Lemma12.11' => array(16, "hints", "max_seconds = 400"), // proved by the two preceding cases 'Satz12.11-case1' => array(49, "hints", "max_seconds = 600"), // 301 seconds required 'Satz12.11-case2' => array(56, "hints", "max_seconds = 1200"), 'Satz12.11' => array (10, "diagram") // proved by the two preceding cases ); ?>