%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN556-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n025.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 19:05:57 EDT 2024 % Result : Unsatisfiable 117.26s 117.57s % Output : CNFRefutation 117.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SYN556-1 : TPTP v8.2.0. Released v2.5.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n025.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 23:53:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.53/0.58 start to proof:theBenchmark % 117.26/117.55 %------------------------------------------- % 117.26/117.55 % File :CSE---1.7 % 117.26/117.55 % Problem :theBenchmark % 117.26/117.55 % Transform :cnf % 117.26/117.55 % Format :tptp:raw % 117.26/117.55 % Command :java -jar mcs_scs.jar %d %s % 117.26/117.55 % 117.26/117.55 % Result :Theorem 116.630000s % 117.26/117.55 % Output :CNFRefutation 116.630000s % 117.26/117.55 %------------------------------------------- % 117.26/117.57 %-------------------------------------------------------------------------- % 117.26/117.57 % File : SYN556-1 : TPTP v8.2.0. Released v2.5.0. % 117.26/117.57 % Domain : Syntactic % 117.26/117.57 % Problem : Harrison problem 2167 % 117.26/117.57 % Version : Especial. % 117.26/117.57 % English : % 117.26/117.57 % 117.26/117.57 % Refs : [Har01] Email to G. Sutcliffe % 117.26/117.57 % Source : [Har01] % 117.26/117.57 % Names : % 117.26/117.57 % 117.26/117.57 % Status : Unsatisfiable % 117.26/117.57 % Rating : 0.27 v8.2.0, 0.29 v8.1.0, 0.25 v7.4.0, 0.33 v7.3.0, 0.25 v6.2.0, 0.33 v6.1.0, 0.57 v6.0.0, 0.44 v5.5.0, 0.56 v5.3.0, 0.65 v5.2.0, 0.62 v5.1.0, 0.56 v5.0.0, 0.47 v4.1.0, 0.53 v4.0.1, 0.57 v3.4.0, 0.40 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.38 v2.6.0, 0.33 v2.5.0 % 117.26/117.57 % Syntax : Number of clauses : 12 ( 5 unt; 0 nHn; 10 RR) % 117.26/117.57 % Number of literals : 25 ( 0 equ; 14 neg) % 117.26/117.57 % Maximal clause size : 4 ( 2 avg) % 117.26/117.57 % Maximal term depth : 5 ( 1 avg) % 117.26/117.57 % Number of predicates : 2 ( 2 usr; 0 prp; 2-2 aty) % 117.26/117.57 % Number of functors : 10 ( 10 usr; 5 con; 0-3 aty) % 117.26/117.57 % Number of variables : 26 ( 0 sgn) % 117.26/117.57 % SPC : CNF_UNS_RFO_NEQ_HRN % 117.26/117.57 % 117.26/117.57 % Comments : % 117.26/117.57 %-------------------------------------------------------------------------- % 117.26/117.57 cnf(p2_1,negated_conjecture, % 117.26/117.57 p2(X0,X0) ). % 117.26/117.57 % 117.26/117.57 cnf(p3_2,negated_conjecture, % 117.26/117.57 p3(X15,X15) ). % 117.26/117.57 % 117.26/117.57 cnf(p2_3,negated_conjecture, % 117.26/117.57 p2(c10,c13) ). % 117.26/117.57 % 117.26/117.57 cnf(p2_4,negated_conjecture, % 117.26/117.57 ( p2(f7(X9),f7(X10)) % 117.26/117.57 | ~ p2(X9,X10) ) ). % 117.26/117.57 % 117.26/117.57 cnf(p2_5,negated_conjecture, % 117.26/117.57 ( p2(f6(X7),f6(X8)) % 117.26/117.57 | ~ p2(X7,X8) ) ). % 117.26/117.57 % 117.26/117.57 cnf(p2_6,negated_conjecture, % 117.26/117.57 ( p2(X1,X2) % 117.26/117.57 | ~ p2(X0,X1) % 117.26/117.57 | ~ p2(X0,X2) ) ). % 117.26/117.57 % 117.26/117.57 cnf(p3_7,negated_conjecture, % 117.26/117.57 ( p3(X16,X17) % 117.26/117.57 | ~ p3(X15,X16) % 117.26/117.57 | ~ p3(X15,X17) ) ). % 117.26/117.57 % 117.26/117.57 cnf(p3_8,negated_conjecture, % 117.26/117.57 p3(c9,f4(c13,f5(f8(c11,c13),f6(f7(c12))),c11)) ). % 117.26/117.57 % 117.26/117.57 cnf(not_p3_9,negated_conjecture, % 117.26/117.57 ~ p3(c9,f4(c10,f5(f8(c11,c10),f6(f7(c12))),c11)) ). % 117.26/117.57 % 117.26/117.57 cnf(p2_10,negated_conjecture, % 117.26/117.57 ( p2(f5(X3,X4),f5(X5,X6)) % 117.26/117.57 | ~ p2(X3,X5) % 117.26/117.57 | ~ p2(X4,X6) ) ). % 117.26/117.57 % 117.26/117.57 cnf(p2_11,negated_conjecture, % 117.26/117.57 ( p2(f8(X11,X12),f8(X13,X14)) % 117.26/117.57 | ~ p2(X12,X14) % 117.26/117.57 | ~ p3(X11,X13) ) ). % 117.26/117.57 % 117.26/117.57 cnf(p3_12,negated_conjecture, % 117.26/117.57 ( p3(f4(X18,X19,X20),f4(X21,X22,X23)) % 117.26/117.57 | ~ p2(X19,X22) % 117.26/117.57 | ~ p3(X20,X23) % 117.26/117.57 | ~ p2(X18,X21) ) ). % 117.26/117.57 % 117.26/117.57 %-------------------------------------------------------------------------- % 117.26/117.57 %------------------------------------------- % 117.26/117.57 % Proof found % 117.26/117.57 % SZS status Theorem for theBenchmark % 117.26/117.57 % SZS output start Proof % 117.26/117.58 %ClaNum:12(EqnAxiom:0) % 117.26/117.58 %VarNum:52(SingletonVarNum:26) % 117.26/117.58 %MaxLitNum:4 % 117.26/117.58 %MaxfuncDepth:4 % 117.26/117.58 %SharedTerms:16 % 117.26/117.58 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 % 117.26/117.58 %singleGoalClaCount:5 % 117.26/117.58 [1]P1(a1,a2) % 117.26/117.58 [4]P2(a5,f10(a2,f9(f6(a3,a2),f8(f7(a4))),a3)) % 117.26/117.58 [5]~P2(a5,f10(a1,f9(f6(a3,a1),f8(f7(a4))),a3)) % 117.26/117.58 [2]P1(x21,x21) % 117.26/117.58 [3]P2(x31,x31) % 117.26/117.58 [6]~P1(x61,x62)+P1(f7(x61),f7(x62)) % 117.26/117.58 [7]~P1(x71,x72)+P1(f8(x71),f8(x72)) % 117.26/117.58 [8]~P1(x83,x81)+P1(x81,x82)+~P1(x83,x82) % 117.26/117.58 [9]~P2(x93,x91)+P2(x91,x92)+~P2(x93,x92) % 117.26/117.58 [10]~P1(x102,x104)+~P2(x101,x103)+P1(f6(x101,x102),f6(x103,x104)) % 117.26/117.58 [11]~P1(x112,x114)+~P1(x111,x113)+P1(f9(x111,x112),f9(x113,x114)) % 117.26/117.58 [12]~P1(x122,x125)+~P1(x121,x124)+~P2(x123,x126)+P2(f10(x121,x122,x123),f10(x124,x125,x126)) % 117.26/117.58 %EqnAxiom % 117.26/117.58 % 117.26/117.58 %------------------------------------------- % 117.26/117.60 cnf(13,plain, % 117.26/117.60 (P1(a2,a1)), % 117.26/117.60 inference(scs_inference,[],[1,2,8])). % 117.26/117.60 cnf(18,plain, % 117.26/117.60 (P2(f10(a2,f9(f6(a3,a2),f8(f7(a4))),a3),a5)), % 117.26/117.60 inference(scs_inference,[],[4,3,9])). % 117.26/117.60 cnf(42,plain, % 117.26/117.60 (P1(f9(f8(a1),f8(a1)),f9(f8(a2),f8(a2)))), % 117.26/117.60 inference(scs_inference,[],[1,7,11])). % 117.26/117.60 cnf(68,plain, % 117.26/117.60 (P1(f6(a5,a1),f6(a5,a2))), % 117.26/117.60 inference(scs_inference,[],[18,1,9,10])). % 117.26/117.60 cnf(71,plain, % 117.26/117.60 (P2(f10(a1,a1,a5),f10(a2,a2,a5))), % 117.26/117.60 inference(scs_inference,[],[18,1,9,12])). % 117.26/117.60 cnf(73,plain, % 117.26/117.60 (P2(f10(a2,a2,a5),f10(a1,a1,a5))), % 117.26/117.60 inference(scs_inference,[],[71,3,9])). % 117.26/117.60 cnf(87,plain, % 117.26/117.60 (P1(f6(f10(a1,a1,a5),f6(a5,a1)),f6(f10(a1,a1,a5),f6(a5,a2)))), % 117.26/117.60 inference(scs_inference,[],[73,68,9,10])). % 117.26/117.60 cnf(149,plain, % 117.26/117.60 (P1(f6(f10(a1,a1,a5),f6(a5,a2)),f6(f10(a1,a1,a5),f6(a5,a1)))), % 117.26/117.60 inference(scs_inference,[],[87,2,8])). % 117.26/117.60 cnf(184,plain, % 117.26/117.60 (P2(f10(f6(f10(a1,a1,a5),f6(a5,a2)),f6(f10(a1,a1,a5),f6(a5,a2)),f10(a2,a2,a5)),f10(f6(f10(a1,a1,a5),f6(a5,a1)),f6(f10(a1,a1,a5),f6(a5,a1)),f10(a2,a2,a5)))), % 117.26/117.60 inference(scs_inference,[],[71,149,9,12])). % 117.26/117.60 cnf(185,plain, % 117.26/117.60 (P2(f10(f6(f10(a1,a1,a5),f6(a5,a1)),f6(f10(a1,a1,a5),f6(a5,a1)),f10(a2,a2,a5)),f10(f6(f10(a1,a1,a5),f6(a5,a2)),f6(f10(a1,a1,a5),f6(a5,a2)),f10(a2,a2,a5)))), % 117.26/117.60 inference(scs_inference,[],[184,3,9])). % 117.26/117.60 cnf(652,plain, % 117.26/117.60 (P1(f6(x6521,a1),f6(x6521,a2))), % 117.26/117.60 inference(scs_inference,[],[1,3,10,9])). % 117.26/117.60 cnf(670,plain, % 117.26/117.60 (P1(f7(f9(a1,a1)),f7(f9(a2,a2)))), % 117.26/117.60 inference(scs_inference,[],[1,11,6])). % 117.26/117.60 cnf(771,plain, % 117.26/117.60 (P1(f6(x7711,a2),f6(x7711,a1))), % 117.26/117.60 inference(scs_inference,[],[652,2,8])). % 117.26/117.60 cnf(894,plain, % 117.26/117.60 (P1(f7(f9(a2,a2)),f7(f9(a1,a1)))), % 117.26/117.60 inference(scs_inference,[],[670,2,8])). % 117.26/117.60 cnf(993,plain, % 117.26/117.60 (P1(f6(f10(a2,a2,a5),f8(a1)),f6(f10(a1,a1,a5),f8(a2)))), % 117.26/117.60 inference(scs_inference,[],[1,73,7,10])). % 117.26/117.60 cnf(1883,plain, % 117.26/117.60 (P2(f10(f9(a1,a1),f9(a1,a1),f10(f6(f10(a1,a1,a5),f6(a5,a1)),f6(f10(a1,a1,a5),f6(a5,a1)),f10(a2,a2,a5))),f10(f9(a2,a2),f9(a2,a2),f10(f6(f10(a1,a1,a5),f6(a5,a2)),f6(f10(a1,a1,a5),f6(a5,a2)),f10(a2,a2,a5))))), % 117.26/117.60 inference(scs_inference,[],[1,185,11,12])). % 117.26/117.60 cnf(2947,plain, % 117.26/117.60 (P1(f8(f7(f9(a2,a2))),f8(f7(f9(a1,a1))))), % 117.26/117.60 inference(scs_inference,[],[894,6,7])). % 117.26/117.60 cnf(2950,plain, % 117.26/117.60 (P1(f7(f6(f10(a2,a2,a5),f8(a1))),f7(f6(f10(a1,a1,a5),f8(a2))))), % 117.26/117.60 inference(scs_inference,[],[993,6])). % 117.26/117.60 cnf(3308,plain, % 117.26/117.60 (P1(f8(a1),f8(a2))), % 117.26/117.60 inference(scs_inference,[],[1,6,7])). % 117.26/117.60 cnf(3531,plain, % 117.26/117.60 (~P2(f10(a2,f9(f6(a3,a2),f8(f7(a4))),a3),f10(a1,f9(f6(a3,a1),f8(f7(a4))),a3))), % 117.26/117.60 inference(scs_inference,[],[42,2947,2950,1883,5,3308,18,6,7,10,11,12,9])). % 117.26/117.60 cnf(3537,plain, % 117.26/117.60 ($false), % 117.26/117.60 inference(scs_inference,[],[2,13,3,771,3531,12,11]), % 117.26/117.60 ['proof']). % 117.26/117.60 % SZS output end Proof % 117.26/117.60 % Total time :116.630000s %------------------------------------------------------------------------------