%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PUZ031-1 : TPTP v8.2.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 13:42:08 EDT 2024 % Result : Unsatisfiable 58.58s 58.87s % Output : CNFRefutation 58.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ031-1 : TPTP v8.2.0. Released v1.0.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n003.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Tue Jun 18 10:14:23 EDT 2024 % 0.12/0.32 % CPUTime : % 0.18/0.54 start to proof:theBenchmark % 58.50/58.84 %------------------------------------------- % 58.50/58.84 % File :CSE---1.7 % 58.50/58.84 % Problem :theBenchmark % 58.50/58.84 % Transform :cnf % 58.50/58.84 % Format :tptp:raw % 58.50/58.84 % Command :java -jar mcs_scs.jar %d %s % 58.50/58.84 % 58.50/58.84 % Result :Theorem 58.010000s % 58.50/58.84 % Output :CNFRefutation 58.010000s % 58.50/58.84 %------------------------------------------- % 58.50/58.86 %------------------------------------------------------------------------------ % 58.50/58.86 % File : PUZ031-1 : TPTP v8.2.0. Released v1.0.0. % 58.50/58.86 % Domain : Puzzles % 58.50/58.86 % Problem : Schubert's Steamroller % 58.50/58.86 % Version : Especial. % 58.50/58.86 % English : Wolves, foxes, birds, caterpillars, and snails are animals, and % 58.50/58.86 % there are some of each of them. Also there are some grains, and % 58.50/58.86 % grains are plants. Every animal either likes to eat all plants % 58.50/58.86 % or all animals much smaller than itself that like to eat some % 58.50/58.86 % plants. Caterpillars and snails are much smaller than birds, % 58.50/58.86 % which are much smaller than foxes, which in turn are much % 58.50/58.86 % smaller than wolves. Wolves do not like to eat foxes or grains, % 58.50/58.86 % while birds like to eat caterpillars but not snails. % 58.50/58.86 % Caterpillars and snails like to eat some plants. Therefore % 58.50/58.86 % there is an animal that likes to eat a grain eating animal. % 58.50/58.86 % 58.50/58.86 % Refs : [Sti86] Stickel (1986), Schubert's Steamroller Problem: Formul % 58.50/58.86 % : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au % 58.50/58.86 % : [WB87] Wang & Bledsoe (1987), Hierarchical Deduction % 58.50/58.86 % : [MB88] Manthey & Bry (1988), SATCHMO: A Theorem Prover Implem % 58.50/58.86 % Source : [Pel86] % 58.50/58.86 % Names : Pelletier 47 [Pel86] % 58.50/58.86 % : steamroller.ver1.in [ANL] % 58.50/58.86 % : steam.in [OTTER] % 58.50/58.86 % : SST [WB87] % 58.50/58.86 % 58.50/58.86 % Status : Unsatisfiable % 58.50/58.86 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.14 v6.2.0, 0.00 v2.2.1, 0.25 v2.1.0, 0.00 v2.0.0 % 58.50/58.86 % Syntax : Number of clauses : 26 ( 6 unt; 1 nHn; 26 RR) % 58.50/58.86 % Number of literals : 63 ( 0 equ; 40 neg) % 58.50/58.86 % Maximal clause size : 8 ( 2 avg) % 58.50/58.86 % Maximal term depth : 2 ( 1 avg) % 58.50/58.86 % Number of predicates : 10 ( 10 usr; 0 prp; 1-2 aty) % 58.50/58.86 % Number of functors : 8 ( 8 usr; 6 con; 0-1 aty) % 58.50/58.86 % Number of variables : 33 ( 0 sgn) % 58.50/58.86 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.50/58.86 % 58.50/58.86 % Comments : This problem is named after Len Schubert. % 58.50/58.86 %------------------------------------------------------------------------------ % 58.50/58.86 cnf(wolf_is_an_animal,axiom, % 58.50/58.86 ( animal(X) % 58.50/58.86 | ~ wolf(X) ) ). % 58.50/58.86 % 58.50/58.86 cnf(fox_is_an_animal,axiom, % 58.50/58.86 ( animal(X) % 58.50/58.86 | ~ fox(X) ) ). % 58.50/58.86 % 58.50/58.86 cnf(bird_is_an_animal,axiom, % 58.50/58.86 ( animal(X) % 58.50/58.86 | ~ bird(X) ) ). % 58.50/58.86 % 58.50/58.86 cnf(caterpillar_is_an_animal,axiom, % 58.50/58.86 ( animal(X) % 58.50/58.86 | ~ caterpillar(X) ) ). % 58.50/58.86 % 58.50/58.86 cnf(snail_is_an_animal,axiom, % 58.50/58.86 ( animal(X) % 58.50/58.86 | ~ snail(X) ) ). % 58.50/58.86 % 58.50/58.86 cnf(there_is_a_wolf,axiom, % 58.50/58.86 wolf(a_wolf) ). % 58.50/58.87 % 58.50/58.87 cnf(there_is_a_fox,axiom, % 58.50/58.87 fox(a_fox) ). % 58.50/58.87 % 58.50/58.87 cnf(there_is_a_bird,axiom, % 58.50/58.87 bird(a_bird) ). % 58.50/58.87 % 58.50/58.87 cnf(there_is_a_caterpillar,axiom, % 58.50/58.87 caterpillar(a_caterpillar) ). % 58.50/58.87 % 58.50/58.87 cnf(there_is_a_snail,axiom, % 58.50/58.87 snail(a_snail) ). % 58.50/58.87 % 58.50/58.87 cnf(there_is_a_grain,axiom, % 58.50/58.87 grain(a_grain) ). % 58.50/58.87 % 58.50/58.87 cnf(grain_is_a_plant,axiom, % 58.50/58.87 ( plant(X) % 58.50/58.87 | ~ grain(X) ) ). % 58.50/58.87 % 58.50/58.87 cnf(eating_habits,axiom, % 58.50/58.87 ( eats(Animal,Plant) % 58.50/58.87 | eats(Animal,Small_animal) % 58.50/58.87 | ~ animal(Animal) % 58.50/58.87 | ~ plant(Plant) % 58.50/58.87 | ~ animal(Small_animal) % 58.50/58.87 | ~ plant(Other_plant) % 58.50/58.87 | ~ much_smaller(Small_animal,Animal) % 58.50/58.87 | ~ eats(Small_animal,Other_plant) ) ). % 58.50/58.87 % 58.50/58.87 cnf(caterpillar_smaller_than_bird,axiom, % 58.50/58.87 ( much_smaller(Catapillar,Bird) % 58.50/58.87 | ~ caterpillar(Catapillar) % 58.50/58.87 | ~ bird(Bird) ) ). % 58.50/58.87 % 58.50/58.87 cnf(snail_smaller_than_bird,axiom, % 58.58/58.87 ( much_smaller(Snail,Bird) % 58.58/58.87 | ~ snail(Snail) % 58.58/58.87 | ~ bird(Bird) ) ). % 58.58/58.87 % 58.58/58.87 cnf(bird_smaller_than_fox,axiom, % 58.58/58.87 ( much_smaller(Bird,Fox) % 58.58/58.87 | ~ bird(Bird) % 58.58/58.87 | ~ fox(Fox) ) ). % 58.58/58.87 % 58.58/58.87 cnf(fox_smaller_than_wolf,axiom, % 58.58/58.87 ( much_smaller(Fox,Wolf) % 58.58/58.87 | ~ fox(Fox) % 58.58/58.87 | ~ wolf(Wolf) ) ). % 58.58/58.87 % 58.58/58.87 cnf(wolf_dont_eat_fox,axiom, % 58.58/58.87 ( ~ wolf(Wolf) % 58.58/58.87 | ~ fox(Fox) % 58.58/58.87 | ~ eats(Wolf,Fox) ) ). % 58.58/58.87 % 58.58/58.87 cnf(wolf_dont_eat_grain,axiom, % 58.58/58.87 ( ~ wolf(Wolf) % 58.58/58.87 | ~ grain(Grain) % 58.58/58.87 | ~ eats(Wolf,Grain) ) ). % 58.58/58.87 % 58.58/58.87 cnf(bird_eats_caterpillar,axiom, % 58.58/58.87 ( eats(Bird,Catapillar) % 58.58/58.87 | ~ bird(Bird) % 58.58/58.87 | ~ caterpillar(Catapillar) ) ). % 58.58/58.87 % 58.58/58.87 cnf(bird_dont_eat_snail,axiom, % 58.58/58.87 ( ~ bird(Bird) % 58.58/58.87 | ~ snail(Snail) % 58.58/58.87 | ~ eats(Bird,Snail) ) ). % 58.58/58.87 % 58.58/58.87 cnf(caterpillar_food_is_a_plant,axiom, % 58.58/58.87 ( plant(caterpillar_food_of(Catapillar)) % 58.58/58.87 | ~ caterpillar(Catapillar) ) ). % 58.58/58.87 % 58.58/58.87 cnf(caterpillar_eats_caterpillar_food,axiom, % 58.58/58.87 ( eats(Catapillar,caterpillar_food_of(Catapillar)) % 58.58/58.87 | ~ caterpillar(Catapillar) ) ). % 58.58/58.87 % 58.58/58.87 cnf(snail_food_is_a_plant,axiom, % 58.58/58.87 ( plant(snail_food_of(Snail)) % 58.58/58.87 | ~ snail(Snail) ) ). % 58.58/58.87 % 58.58/58.87 cnf(snail_eats_snail_food,axiom, % 58.58/58.87 ( eats(Snail,snail_food_of(Snail)) % 58.58/58.87 | ~ snail(Snail) ) ). % 58.58/58.87 % 58.58/58.87 cnf(prove_the_animal_exists,negated_conjecture, % 58.58/58.87 ( ~ animal(Animal) % 58.58/58.87 | ~ animal(Grain_eater) % 58.58/58.87 | ~ grain(Grain) % 58.58/58.87 | ~ eats(Animal,Grain_eater) % 58.58/58.87 | ~ eats(Grain_eater,Grain) ) ). % 58.58/58.87 % 58.58/58.87 %------------------------------------------------------------------------------ % 58.58/58.87 %------------------------------------------- % 58.58/58.87 % Proof found % 58.58/58.87 % SZS status Theorem for theBenchmark % 58.58/58.87 % SZS output start Proof % 58.58/58.88 %ClaNum:26(EqnAxiom:0) % 58.58/58.88 %VarNum:73(SingletonVarNum:33) % 58.58/58.88 %MaxLitNum:8 % 58.58/58.88 %MaxfuncDepth:1 % 58.58/58.88 %SharedTerms:12 % 58.58/58.88 %goalClause: 25 % 58.58/58.88 [1]P1(a1) % 58.58/58.88 [2]P2(a2) % 58.58/58.88 [3]P3(a3) % 58.58/58.88 [4]P5(a4) % 58.58/58.88 [5]P7(a5) % 58.58/58.88 [6]P8(a6) % 58.58/58.88 [7]~P1(x71)+P4(x71) % 58.58/58.88 [8]~P2(x81)+P4(x81) % 58.58/58.88 [9]~P3(x91)+P4(x91) % 58.58/58.88 [10]~P5(x101)+P4(x101) % 58.58/58.88 [11]~P7(x111)+P4(x111) % 58.58/58.88 [12]~P8(x121)+P9(x121) % 58.58/58.88 [13]~P5(x131)+P9(f7(x131)) % 58.58/58.88 [14]~P7(x141)+P9(f8(x141)) % 58.58/58.88 [15]~P5(x151)+P6(x151,f7(x151)) % 58.58/58.88 [16]~P7(x161)+P6(x161,f8(x161)) % 58.58/58.88 [17]~P3(x171)+~P5(x172)+P6(x171,x172) % 58.58/58.88 [18]~P1(x182)+~P2(x181)+P10(x181,x182) % 58.58/58.88 [19]~P2(x192)+~P3(x191)+P10(x191,x192) % 58.58/58.88 [20]~P3(x202)+~P5(x201)+P10(x201,x202) % 58.58/58.88 [21]~P3(x212)+~P7(x211)+P10(x211,x212) % 58.58/58.88 [22]~P6(x221,x222)+~P1(x221)+~P2(x222) % 58.58/58.88 [23]~P6(x231,x232)+~P1(x231)+~P8(x232) % 58.58/58.88 [24]~P6(x241,x242)+~P3(x241)+~P7(x242) % 58.58/58.88 [25]~P6(x251,x253)+~P6(x252,x251)+~P4(x251)+~P4(x252)+~P8(x253) % 58.58/58.88 [26]~P4(x262)+~P4(x261)+~P9(x263)+~P6(x262,x264)+~P10(x262,x261)+P6(x261,x262)+P6(x261,x263)+~P9(x264) % 58.58/58.88 %EqnAxiom % 58.58/58.88 % 58.58/58.88 %------------------------------------------- % 58.74/59.06 cnf(27,plain, % 58.74/59.06 (~P6(a1,a2)), % 58.74/59.06 inference(scs_inference,[],[1,2,22])). % 58.74/59.06 cnf(29,plain, % 58.74/59.06 (~P6(a1,a6)), % 58.74/59.06 inference(scs_inference,[],[1,2,6,22,23])). % 58.74/59.06 cnf(31,plain, % 58.74/59.06 (~P6(a3,a5)), % 58.74/59.06 inference(scs_inference,[],[1,2,3,5,6,22,23,24])). % 58.74/59.06 cnf(375727,plain, % 58.74/59.07 (P4(a1)), % 58.74/59.07 inference(scs_inference,[],[1,7])). % 58.74/59.07 cnf(375729,plain, % 58.74/59.07 (P4(a2)), % 58.74/59.07 inference(scs_inference,[],[1,2,7,8])). % 58.74/59.07 cnf(375731,plain, % 58.74/59.07 (P4(a3)), % 58.74/59.07 inference(scs_inference,[],[1,2,3,7,8,9])). % 58.74/59.07 cnf(375733,plain, % 58.74/59.07 (P4(a4)), % 58.74/59.07 inference(scs_inference,[],[1,2,3,4,7,8,9,10])). % 58.74/59.07 cnf(375735,plain, % 58.74/59.07 (P4(a5)), % 58.74/59.07 inference(scs_inference,[],[1,2,5,3,4,7,8,9,10,11])). % 58.74/59.07 cnf(375737,plain, % 58.74/59.07 (P9(a6)), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12])). % 58.74/59.07 cnf(375739,plain, % 58.74/59.07 (P9(f7(a4))), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12,13])). % 58.74/59.07 cnf(375741,plain, % 58.74/59.07 (P9(f8(a5))), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12,13,14])). % 58.74/59.07 cnf(375743,plain, % 58.74/59.07 (P6(a4,f7(a4))), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12,13,14,15])). % 58.74/59.07 cnf(375745,plain, % 58.74/59.07 (P6(a5,f8(a5))), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12,13,14,15,16])). % 58.74/59.07 cnf(375747,plain, % 58.74/59.07 (P10(a2,a1)), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12,13,14,15,16,18])). % 58.74/59.07 cnf(375749,plain, % 58.74/59.07 (P10(a3,a2)), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12,13,14,15,16,18,19])). % 58.74/59.07 cnf(375753,plain, % 58.74/59.07 (P10(a5,a3)), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12,13,14,15,16,18,19,20,21])). % 58.74/59.07 cnf(375755,plain, % 58.74/59.07 (P6(a3,a4)), % 58.74/59.07 inference(scs_inference,[],[1,2,5,6,3,4,7,8,9,10,11,12,13,14,15,16,18,19,20,21,17])). % 58.74/59.07 cnf(375770,plain, % 58.74/59.07 (~P6(a2,a6)), % 58.74/59.07 inference(scs_inference,[],[375747,375729,375755,375727,375733,375737,375743,375731,27,29,25,26])). % 58.74/59.07 cnf(375791,plain, % 58.74/59.07 (P6(a3,f7(a4))), % 58.74/59.07 inference(scs_inference,[],[375753,375739,375741,375745,375735,375731,31,26])). % 58.74/59.07 cnf(375799,plain, % 58.74/59.07 (~P6(a3,a6)), % 58.74/59.07 inference(scs_inference,[],[375749,375791,375770,375739,375731,375729,375737,6,26,25])). % 58.74/59.07 cnf(375801,plain, % 58.74/59.07 ($false), % 58.74/59.07 inference(scs_inference,[],[375799,375753,375741,375745,375735,375737,375731,31,26]), % 58.74/59.07 ['proof']). % 58.98/59.24 % SZS output end Proof % 58.98/59.24 % Total time :58.010000s %------------------------------------------------------------------------------