%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYO691-1.001 : TPTP v8.2.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n019.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 20:27:47 EDT 2024 % Result : Unsatisfiable 220.98s 221.27s % Output : CNFRefutation 221.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYO691-1.001 : TPTP v8.2.0. Released v7.3.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Sun Jun 23 10:36:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.50/0.60 start to proof:theBenchmark % 220.98/221.22 %------------------------------------------- % 220.98/221.22 % File :CSE---1.7 % 220.98/221.22 % Problem :theBenchmark % 220.98/221.22 % Transform :cnf % 220.98/221.22 % Format :tptp:raw % 220.98/221.22 % Command :java -jar mcs_scs.jar %d %s % 220.98/221.22 % 220.98/221.22 % Result :Theorem 220.270000s % 220.98/221.22 % Output :CNFRefutation 220.270000s % 220.98/221.22 %------------------------------------------- % 220.98/221.27 %------------------------------------------------------------------------------ % 220.98/221.27 % File : SYO691-1.001 : TPTP v8.2.0. Released v7.3.0. % 220.98/221.27 % Domain : Syntactic % 220.98/221.27 % Problem : Loop 1 Yes % 220.98/221.27 % Version : Especial. % 220.98/221.27 % English : % 220.98/221.27 % 220.98/221.27 % Refs : [Wal17] Waldman (2017), Email to Geoff Sutcliffe % 220.98/221.27 % Source : [TPTP] % 220.98/221.27 % Names : loop-1-yes.tptp [Wal17] % 220.98/221.27 % 220.98/221.27 % Status : Unsatisfiable % 220.98/221.27 % Rating : 0.09 v8.2.0, 0.00 v7.3.0 % 220.98/221.27 % Syntax : Number of clauses : 7 ( 3 unt; 0 nHn; 3 RR) % 220.98/221.27 % Number of literals : 12 ( 0 equ; 6 neg) % 220.98/221.27 % Maximal clause size : 3 ( 1 avg) % 220.98/221.27 % Maximal term depth : 6 ( 2 avg) % 220.98/221.27 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty) % 220.98/221.27 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty) % 220.98/221.27 % Number of variables : 17 ( 0 sgn) % 220.98/221.27 % SPC : CNF_UNS_RFO_NEQ_HRN % 220.98/221.27 % 220.98/221.27 % Comments : % 220.98/221.27 %------------------------------------------------------------------------------ % 220.98/221.27 cnf(rule_1,axiom, % 220.98/221.27 top(f(f(f(Z,a),Y),f(X,a)),f(f(X,f(f(Y,a),a)),Z)) ). % 220.98/221.27 % 220.98/221.27 cnf(prove,negated_conjecture, % 220.98/221.27 ~ seq(succ(succ(succ(succ(succ(zero))))),X,X) ). % 220.98/221.27 % 220.98/221.27 cnf(rewrite_top,axiom, % 220.98/221.27 ( ~ top(X,Y) % 220.98/221.27 | step(X,Y) ) ). % 220.98/221.27 % 220.98/221.27 cnf(rewrite_left,axiom, % 220.98/221.27 ( ~ step(X,Y) % 220.98/221.27 | step(f(X,Z),f(Y,Z)) ) ). % 220.98/221.27 % 220.98/221.27 cnf(rewrite_right,axiom, % 220.98/221.27 ( ~ step(Y,Z) % 220.98/221.27 | step(f(X,Y),f(X,Z)) ) ). % 220.98/221.27 % 220.98/221.27 cnf(rewrite_sequence_zero,axiom, % 220.98/221.27 seq(zero,X,X) ). % 220.98/221.27 % 220.98/221.27 cnf(rewrite_sequence_succ,axiom, % 220.98/221.27 ( ~ seq(N,X,Y) % 220.98/221.27 | ~ step(Y,Z) % 220.98/221.27 | seq(succ(N),X,Z) ) ). % 220.98/221.27 % 220.98/221.27 %------------------------------------------------------------------------------ % 220.98/221.27 %------------------------------------------- % 220.98/221.27 % Proof found % 220.98/221.27 % SZS status Theorem for theBenchmark % 220.98/221.27 % SZS output start Proof % 221.08/221.32 %ClaNum:7(EqnAxiom:0) % 221.08/221.32 %VarNum:34(SingletonVarNum:17) % 221.08/221.32 %MaxLitNum:3 % 221.08/221.32 %MaxfuncDepth:5 % 221.08/221.32 %SharedTerms:7 % 221.08/221.32 %goalClause: 3 % 221.08/221.32 %singleGoalClaCount:1 % 221.08/221.32 [1]P1(a1,x11,x11) % 221.08/221.32 [3]~P1(f4(f4(f4(f4(f4(a1))))),x31,x31) % 221.08/221.32 [2]P2(f3(f3(f3(x21,a2),x22),f3(x23,a2)),f3(f3(x23,f3(f3(x22,a2),a2)),x21)) % 221.08/221.32 [4]~P2(x41,x42)+P3(x41,x42) % 221.08/221.32 [5]~P3(x52,x53)+P3(f3(x51,x52),f3(x51,x53)) % 221.08/221.32 [6]~P3(x61,x63)+P3(f3(x61,x62),f3(x63,x62)) % 221.08/221.32 [7]~P1(x71,x72,x74)+~P3(x74,x73)+P1(f4(x71),x72,x73) % 221.08/221.32 %EqnAxiom % 221.08/221.32 % 221.08/221.32 %------------------------------------------- % 221.21/221.48 cnf(8,plain, % 221.21/221.48 (~P1(f4(f4(f4(f4(a1)))),x81,x82)+~P3(x82,x81)), % 221.21/221.48 inference(scs_inference,[],[3,7])). % 221.21/221.48 cnf(10,plain, % 221.21/221.48 (P3(f3(x101,f3(f3(f3(x102,a2),x103),f3(x104,a2))),f3(x101,f3(f3(x104,f3(f3(x103,a2),a2)),x102)))), % 221.21/221.48 inference(scs_inference,[],[2,4,5])). % 221.21/221.48 cnf(11,plain, % 221.21/221.48 (P3(f3(f3(f3(f3(x111,a2),x112),f3(x113,a2)),x114),f3(f3(f3(x113,f3(f3(x112,a2),a2)),x111),x114))), % 221.21/221.48 inference(scs_inference,[],[2,6,4])). % 221.21/221.48 cnf(13,plain, % 221.21/221.48 (~P3(x131,x132)+P3(f3(x133,f3(x131,x134)),f3(x133,f3(x132,x134)))), % 221.21/221.48 inference(scs_inference,[],[5,6])). % 221.21/221.48 cnf(16,plain, % 221.21/221.49 (~P3(x161,x162)+P3(f3(f3(x163,x161),x164),f3(f3(x163,x162),x164))), % 221.21/221.49 inference(scs_inference,[],[5,6])). % 221.21/221.49 cnf(19,plain, % 221.21/221.49 (P3(f3(x191,f3(f3(x192,x193),x194)),f3(x191,f3(f3(x192,x195),x194)))+~P3(x193,x195)), % 221.21/221.49 inference(scs_inference,[],[5,13])). % 221.21/221.49 cnf(23,plain, % 221.21/221.49 (~P3(x231,x232)+~P1(f4(f4(f4(f4(a1)))),f3(x233,x232),f3(x233,x231))), % 221.21/221.49 inference(scs_inference,[],[5,8])). % 221.21/221.49 cnf(26,plain, % 221.21/221.49 (~P3(x261,x262)+~P1(f4(f4(f4(f4(a1)))),f3(x262,x263),f3(x261,x263))), % 221.21/221.49 inference(scs_inference,[],[6,8])). % 221.21/221.49 cnf(41,plain, % 221.21/221.49 (P3(f3(f3(x411,f3(f3(f3(x412,a2),x413),f3(x414,a2))),x415),f3(f3(x411,f3(f3(x414,f3(f3(x413,a2),a2)),x412)),x415))), % 221.21/221.49 inference(scs_inference,[],[2,16,4])). % 221.21/221.49 cnf(48,plain, % 221.21/221.49 (~P3(x481,x482)+~P1(f4(f4(f4(a1))),f3(x483,x482),x484)+~P3(x484,f3(x483,x481))), % 221.21/221.49 inference(scs_inference,[],[23,7])). % 221.21/221.49 cnf(49,plain, % 221.21/221.49 (~P3(x491,x492)+~P1(f4(f4(f4(a1))),f3(f3(x493,f3(f3(x494,a2),a2)),x492),f3(f3(f3(x491,a2),x494),f3(x493,a2)))), % 221.21/221.49 inference(scs_inference,[],[2,48,4])). % 221.21/221.49 cnf(51,plain, % 221.21/221.49 (~P3(x511,x512)+~P1(f4(f4(f4(a1))),f3(x512,x513),x514)+~P3(x514,f3(x511,x513))), % 221.21/221.49 inference(scs_inference,[],[26,7])). % 221.21/221.49 cnf(52,plain, % 221.21/221.49 (~P3(f3(x521,f3(f3(x522,a2),a2)),x523)+~P1(f4(f4(f4(a1))),f3(x523,x524),f3(f3(f3(x524,a2),x522),f3(x521,a2)))), % 221.21/221.49 inference(scs_inference,[],[2,51,4])). % 221.21/221.49 cnf(59,plain, % 221.21/221.49 (~P3(x591,x592)+~P3(f3(f3(x593,x592),x594),x595)+~P1(f4(f4(f4(a1))),f3(x596,x595),f3(x596,f3(f3(x593,x591),x594)))), % 221.21/221.49 inference(scs_inference,[],[19,48])). % 221.21/221.49 cnf(60,plain, % 221.21/221.49 (~P3(f3(f3(x601,f3(f3(x602,f3(f3(x603,a2),a2)),x604)),x605),x606)+~P1(f4(f4(f4(a1))),f3(x607,x606),f3(x607,f3(f3(x601,f3(f3(f3(x604,a2),x603),f3(x602,a2))),x605)))), % 221.21/221.49 inference(scs_inference,[],[2,59,4])). % 221.21/221.49 cnf(81,plain, % 221.21/221.49 (~P3(x811,x812)+~P1(f4(f4(a1)),f3(f3(x813,f3(f3(x814,a2),a2)),x812),x815)+~P3(x815,f3(f3(f3(x811,a2),x814),f3(x813,a2)))), % 221.21/221.49 inference(scs_inference,[],[49,7])). % 221.21/221.49 cnf(82,plain, % 221.21/221.49 (~P3(x821,f3(f3(f3(f3(f3(f3(x822,a2),x823),f3(x824,a2)),a2),x825),f3(x826,a2)))+~P1(f4(f4(a1)),f3(f3(x826,f3(f3(x825,a2),a2)),f3(f3(x824,f3(f3(x823,a2),a2)),x822)),x821)), % 221.21/221.49 inference(scs_inference,[],[2,81,4])). % 221.21/221.49 cnf(85,plain, % 221.21/221.49 (~P1(f4(f4(a1)),f3(x851,x852),x853)+~P3(x853,f3(f3(f3(x852,a2),x854),f3(x855,a2)))+~P3(f3(x855,f3(f3(x854,a2),a2)),x851)), % 221.21/221.49 inference(scs_inference,[],[52,7])). % 221.21/221.49 cnf(86,plain, % 221.21/221.49 (~P3(x861,f3(f3(f3(x862,a2),x863),f3(f3(f3(x864,a2),x865),a2)))+~P1(f4(f4(a1)),f3(f3(f3(f3(x863,a2),f3(f3(x865,a2),a2)),x864),x862),x861)), % 221.21/221.49 inference(scs_inference,[],[2,85,4])). % 221.21/221.49 cnf(54988,plain, % 221.21/221.49 (P3(f3(f3(f3(x549881,a2),x549882),f3(x549883,a2)),f3(f3(x549883,f3(f3(x549882,a2),a2)),x549881))), % 221.21/221.49 inference(scs_inference,[],[2,4])). % 221.21/221.49 cnf(54990,plain, % 221.21/221.49 (P1(f4(a1),f3(f3(f3(f3(x549901,a2),x549902),f3(x549903,a2)),x549904),f3(f3(f3(x549903,f3(f3(x549902,a2),a2)),x549901),x549904))), % 221.21/221.49 inference(scs_inference,[],[1,11,2,4,7])). % 221.21/221.49 cnf(71707,plain, % 221.21/221.49 (~P3(f3(x717071,f3(f3(f3(f3(x717072,a2),a2),a2),a2)),x717073)+~P1(f4(f4(a1)),f3(x717073,x717074),f3(f3(f3(f3(x717071,a2),a2),x717072),f3(f3(x717074,a2),a2)))), % 221.21/221.49 inference(scs_inference,[],[54988,85])). % 221.21/221.49 cnf(74457,plain, % 221.21/221.49 (P3(f3(f3(f3(f3(x744571,a2),x744572),f3(x744573,a2)),x744574),f3(f3(f3(x744573,f3(f3(x744572,a2),a2)),x744571),x744574))), % 221.21/221.49 inference(rename_variables,[],[11])). % 221.21/221.49 cnf(74463,plain, % 221.21/221.49 (P3(f3(x744631,f3(f3(f3(x744632,a2),x744633),f3(x744634,a2))),f3(x744631,f3(f3(x744634,f3(f3(x744633,a2),a2)),x744632)))), % 221.21/221.49 inference(rename_variables,[],[10])). % 221.21/221.49 cnf(74466,plain, % 221.21/221.49 (P3(f3(f3(f3(f3(x744661,a2),x744662),f3(x744663,a2)),x744664),f3(f3(f3(x744663,f3(f3(x744662,a2),a2)),x744661),x744664))), % 221.21/221.49 inference(rename_variables,[],[11])). % 221.21/221.49 cnf(74469,plain, % 221.21/221.49 (P3(f3(f3(f3(f3(x744691,a2),x744692),f3(x744693,a2)),x744694),f3(f3(f3(x744693,f3(f3(x744692,a2),a2)),x744691),x744694))), % 221.21/221.49 inference(rename_variables,[],[11])). % 221.21/221.49 cnf(74477,plain, % 221.21/221.49 (P3(f3(f3(f3(f3(f3(x744771,a2),x744772),f3(x744773,a2)),x744774),x744775),f3(f3(f3(f3(x744773,f3(f3(x744772,a2),a2)),x744771),x744774),x744775))), % 221.21/221.49 inference(scs_inference,[],[54988,10,74463,11,74457,74466,74469,71707,82,86,60,52,23,26,5,6])). % 221.21/221.49 cnf(74564,plain, % 221.21/221.49 (~P1(f4(f4(a1)),f3(f3(x745641,f3(f3(x745642,a2),a2)),f3(f3(f3(x745643,a2),f3(f3(x745644,a2),a2)),x745645)),f3(f3(f3(f3(f3(a2,a2),x745643),f3(f3(f3(x745645,a2),x745644),a2)),x745642),f3(x745641,a2)))), % 221.21/221.49 inference(scs_inference,[],[74477,41,86,6,82])). % 221.21/221.49 cnf(74607,plain, % 221.21/221.49 ($false), % 221.21/221.49 inference(scs_inference,[],[10,74477,41,54990,74564,6,5,7]), % 221.21/221.49 ['proof']). % 221.40/221.62 % SZS output end Proof % 221.40/221.62 % Total time :220.270000s %------------------------------------------------------------------------------