%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYO691-1.000 : TPTP v8.2.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n029.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 58.55s 59.17s % Output : CNFRefutation 58.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SYO691-1.000 : TPTP v8.2.0. Released v7.3.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 06:52:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.51/0.57 start to proof:theBenchmark % 58.55/59.15 %------------------------------------------- % 58.55/59.15 % File :CSE---1.7 % 58.55/59.15 % Problem :theBenchmark % 58.55/59.16 % Transform :cnf % 58.55/59.16 % Format :tptp:raw % 58.55/59.16 % Command :java -jar mcs_scs.jar %d %s % 58.55/59.16 % 58.55/59.16 % Result :Theorem 58.000000s % 58.55/59.16 % Output :CNFRefutation 58.000000s % 58.55/59.16 %------------------------------------------- % 58.55/59.17 %------------------------------------------------------------------------------ % 58.55/59.17 % File : SYO691-1.000 : TPTP v8.2.0. Released v7.3.0. % 58.55/59.17 % Domain : Syntactic % 58.55/59.17 % Problem : Loop 0 Yes % 58.55/59.17 % Version : Especial. % 58.55/59.17 % English : % 58.55/59.17 % 58.55/59.17 % Refs : [Wal17] Waldman (2017), Email to Geoff Sutcliffe % 58.55/59.17 % Source : [TPTP] % 58.55/59.17 % Names : loop-0-yes.tptp [Wal17] % 58.55/59.17 % 58.55/59.17 % Status : Unsatisfiable % 58.55/59.17 % Rating : 0.00 v7.3.0 % 58.55/59.17 % Syntax : Number of clauses : 7 ( 3 unt; 0 nHn; 3 RR) % 58.55/59.17 % Number of literals : 12 ( 0 equ; 6 neg) % 58.55/59.17 % Maximal clause size : 3 ( 1 avg) % 58.55/59.17 % Maximal term depth : 4 ( 1 avg) % 58.55/59.17 % Number of predicates : 3 ( 3 usr; 0 prp; 2-3 aty) % 58.55/59.17 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty) % 58.55/59.17 % Number of variables : 17 ( 0 sgn) % 58.55/59.17 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.55/59.17 % 58.55/59.17 % Comments : % 58.55/59.17 %------------------------------------------------------------------------------ % 58.55/59.17 cnf(rule_1,axiom, % 58.55/59.17 top(f(f(Z,Y),f(X,a)),f(f(X,f(Y,a)),Z)) ). % 58.55/59.17 % 58.55/59.17 cnf(prove,negated_conjecture, % 58.55/59.17 ~ seq(succ(succ(succ(zero))),X,X) ). % 58.55/59.17 % 58.55/59.17 cnf(rewrite_top,axiom, % 58.55/59.17 ( ~ top(X,Y) % 58.55/59.17 | step(X,Y) ) ). % 58.55/59.17 % 58.55/59.17 cnf(rewrite_left,axiom, % 58.55/59.17 ( ~ step(X,Y) % 58.55/59.17 | step(f(X,Z),f(Y,Z)) ) ). % 58.55/59.17 % 58.55/59.17 cnf(rewrite_right,axiom, % 58.55/59.17 ( ~ step(Y,Z) % 58.55/59.17 | step(f(X,Y),f(X,Z)) ) ). % 58.55/59.17 % 58.55/59.17 cnf(rewrite_sequence_zero,axiom, % 58.55/59.17 seq(zero,X,X) ). % 58.55/59.17 % 58.55/59.17 cnf(rewrite_sequence_succ,axiom, % 58.55/59.17 ( ~ seq(N,X,Y) % 58.55/59.17 | ~ step(Y,Z) % 58.55/59.17 | seq(succ(N),X,Z) ) ). % 58.55/59.17 % 58.55/59.17 %------------------------------------------------------------------------------ % 58.55/59.17 %------------------------------------------- % 58.55/59.17 % Proof found % 58.55/59.17 % SZS status Theorem for theBenchmark % 58.55/59.17 % SZS output start Proof % 58.55/59.17 %ClaNum:7(EqnAxiom:0) % 58.55/59.17 %VarNum:34(SingletonVarNum:17) % 58.55/59.17 %MaxLitNum:3 % 58.55/59.17 %MaxfuncDepth:3 % 58.55/59.17 %SharedTerms:5 % 58.55/59.17 %goalClause: 3 % 58.55/59.17 %singleGoalClaCount:1 % 58.55/59.17 [1]P1(a1,x11,x11) % 58.55/59.17 [3]~P1(f4(f4(f4(a1))),x31,x31) % 58.55/59.17 [2]P2(f2(f2(x21,x22),f2(x23,a3)),f2(f2(x23,f2(x22,a3)),x21)) % 58.55/59.17 [4]~P2(x41,x42)+P3(x41,x42) % 58.55/59.17 [5]~P3(x52,x53)+P3(f2(x51,x52),f2(x51,x53)) % 58.55/59.17 [6]~P3(x61,x63)+P3(f2(x61,x62),f2(x63,x62)) % 58.55/59.17 [7]~P1(x71,x72,x74)+~P3(x74,x73)+P1(f4(x71),x72,x73) % 58.55/59.17 %EqnAxiom % 58.55/59.17 % 58.55/59.17 %------------------------------------------- % 58.55/59.21 cnf(8,plain, % 58.55/59.21 (~P1(f4(f4(a1)),x81,x82)+~P3(x82,x81)), % 58.55/59.21 inference(scs_inference,[],[3,7])). % 58.55/59.21 cnf(11,plain, % 58.55/59.21 (~P1(f4(f4(a1)),f2(f2(x111,f2(x112,a3)),x113),f2(f2(x113,x112),f2(x111,a3)))), % 58.55/59.21 inference(scs_inference,[],[2,8,4])). % 58.55/59.21 cnf(12,plain, % 58.55/59.21 (~P1(f4(a1),f2(f2(x121,f2(x122,a3)),x123),x124)+~P3(x124,f2(f2(x123,x122),f2(x121,a3)))), % 58.55/59.21 inference(scs_inference,[],[11,7])). % 58.55/59.21 cnf(21,plain, % 58.55/59.21 (~P3(x211,f2(x212,a3))+~P1(f4(a1),f2(f2(x212,f2(x213,a3)),x214),f2(f2(x214,x213),x211))), % 58.55/59.21 inference(scs_inference,[],[5,12])). % 58.55/59.21 cnf(22,plain, % 58.55/59.21 (~P1(f4(a1),f2(f2(f2(x221,f2(x222,a3)),f2(x223,a3)),x224),f2(f2(x224,x223),f2(f2(a3,x222),f2(x221,a3))))), % 58.55/59.21 inference(scs_inference,[],[2,21,4])). % 58.55/59.21 cnf(28,plain, % 58.55/59.21 (~P3(x281,f2(x282,x283))+~P1(f4(a1),f2(f2(x284,f2(x283,a3)),x282),f2(x281,f2(x284,a3)))), % 58.55/59.21 inference(scs_inference,[],[6,12])). % 58.55/59.21 cnf(29,plain, % 58.55/59.21 (~P1(f4(a1),f2(f2(x291,f2(x292,a3)),f2(x293,f2(x294,a3))),f2(f2(f2(x292,x294),f2(x293,a3)),f2(x291,a3)))), % 58.55/59.21 inference(scs_inference,[],[2,28,4])). % 58.55/59.21 cnf(44020,plain, % 58.55/59.21 (~P3(f2(f2(f2(x440201,f2(x440202,a3)),f2(x440203,a3)),x440204),f2(f2(x440204,x440203),f2(f2(a3,x440202),f2(x440201,a3))))), % 58.55/59.21 inference(scs_inference,[],[22,1,7])). % 58.55/59.21 cnf(44026,plain, % 58.55/59.21 (~P3(f2(f2(x440261,f2(x440262,a3)),f2(x440263,f2(x440264,a3))),f2(f2(f2(x440262,x440264),f2(x440263,a3)),f2(x440261,a3)))), % 58.55/59.21 inference(scs_inference,[],[29,44020,1,4,7])). % 58.55/59.21 cnf(44030,plain, % 58.55/59.21 (~P3(f2(x440301,f2(x440302,a3)),f2(f2(x440301,x440302),a3))), % 58.55/59.21 inference(scs_inference,[],[44026,5])). % 58.55/59.21 cnf(44336,plain, % 58.55/59.21 ($false), % 58.55/59.21 inference(scs_inference,[],[44030,2,4]), % 58.55/59.21 ['proof']). % 58.68/59.24 % SZS output end Proof % 58.68/59.24 % Total time :58.000000s %------------------------------------------------------------------------------