%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYO614-1 : TPTP v8.2.0. Released v7.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n017.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:30 EDT 2024 % Result : Unsatisfiable 116.33s 116.40s % Output : CNFRefutation 116.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYO614-1 : TPTP v8.2.0. Released v7.1.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 10:17:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.54 start to proof:theBenchmark % 116.33/116.38 %------------------------------------------- % 116.33/116.38 % File :CSE---1.7 % 116.33/116.38 % Problem :theBenchmark % 116.33/116.38 % Transform :cnf % 116.33/116.38 % Format :tptp:raw % 116.33/116.38 % Command :java -jar mcs_scs.jar %d %s % 116.33/116.38 % 116.33/116.38 % Result :Theorem 115.780000s % 116.33/116.38 % Output :CNFRefutation 115.780000s % 116.33/116.38 %------------------------------------------- % 116.33/116.40 %------------------------------------------------------------------------------ % 116.33/116.40 % File : SYO614-1 : TPTP v8.2.0. Released v7.1.0. % 116.33/116.40 % Domain : Syntactic % 116.33/116.40 % Problem : C(2,0) % 116.33/116.40 % Version : Especial. % 116.33/116.40 % English : % 116.33/116.40 % 116.33/116.40 % Refs : [Cer15] Cerna (2015), Advances in Schematic Cut Elimination % 116.33/116.40 % : [EH+16] Ebner et al. (2016), System Description: GAPT 2.0 % 116.33/116.40 % : [Cer17] Cerna (2017), Email to Geoff Sutcliffe % 116.33/116.40 % Source : [Cer17] % 116.33/116.40 % Names : C(2,0) [Cer17] % 116.33/116.40 % 116.33/116.40 % Status : Unsatisfiable % 116.33/116.40 % Rating : 0.00 v7.1.0 % 116.33/116.40 % Syntax : Number of clauses : 6 ( 1 unt; 1 nHn; 4 RR) % 116.33/116.40 % Number of literals : 13 ( 0 equ; 8 neg) % 116.33/116.40 % Maximal clause size : 3 ( 2 avg) % 116.33/116.40 % Maximal term depth : 2 ( 1 avg) % 116.33/116.40 % Number of predicates : 2 ( 2 usr; 0 prp; 2-2 aty) % 116.33/116.40 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty) % 116.33/116.40 % Number of variables : 12 ( 2 sgn) % 116.33/116.40 % SPC : CNF_UNS_RFO_NEQ_NHN % 116.33/116.40 % 116.33/116.40 % Comments : % 116.33/116.40 %------------------------------------------------------------------------------ % 116.33/116.40 cnf(sos_01,axiom, % 116.33/116.40 le(A,A) ). % 116.33/116.40 % 116.33/116.40 cnf(sos_02,axiom, % 116.33/116.40 ( ~ le(max(A,B),C) % 116.33/116.40 | le(A,C) ) ). % 116.33/116.40 % 116.33/116.40 cnf(sos_03,axiom, % 116.33/116.40 ( ~ le(max(A,B),C) % 116.33/116.40 | le(B,C) ) ). % 116.33/116.40 % 116.33/116.40 cnf(sos_04,axiom, % 116.33/116.40 ( eq(f(A),a0) % 116.33/116.40 | eq(f(A),a1) ) ). % 116.33/116.40 % 116.33/116.40 cnf(sos_05,axiom, % 116.33/116.40 ( ~ eq(f(A0),a0) % 116.33/116.40 | ~ eq(f(A1),a0) % 116.33/116.40 | ~ le(s(A0),A1) ) ). % 116.33/116.40 % 116.33/116.40 cnf(sos_06,axiom, % 116.33/116.40 ( ~ eq(f(A0),a1) % 116.33/116.40 | ~ eq(f(A1),a1) % 116.33/116.40 | ~ le(s(A0),A1) ) ). % 116.33/116.40 % 116.33/116.40 %------------------------------------------------------------------------------ % 116.33/116.40 %------------------------------------------- % 116.33/116.40 % Proof found % 116.33/116.40 % SZS status Theorem for theBenchmark % 116.33/116.40 % SZS output start Proof % 116.33/116.41 %ClaNum:6(EqnAxiom:0) % 116.33/116.41 %VarNum:22(SingletonVarNum:12) % 116.33/116.41 %MaxLitNum:3 % 116.33/116.41 %MaxfuncDepth:1 % 116.33/116.41 %SharedTerms:2 % 116.33/116.41 [1]P1(x11,x11) % 116.33/116.41 [2]P2(f1(x21),a2)+P2(f1(x21),a3) % 116.33/116.41 [3]P1(x31,x32)+~P1(f4(x33,x31),x32) % 116.33/116.41 [4]P1(x41,x42)+~P1(f4(x41,x43),x42) % 116.33/116.41 [5]~P1(f5(x51),x52)+~P2(f1(x52),a2)+~P2(f1(x51),a2) % 116.33/116.41 [6]~P1(f5(x61),x62)+~P2(f1(x62),a3)+~P2(f1(x61),a3) % 116.33/116.41 %EqnAxiom % 116.33/116.41 % 116.33/116.41 %------------------------------------------- % 116.33/116.42 cnf(7,plain, % 116.33/116.42 (P1(x71,f4(x72,x71))), % 116.33/116.42 inference(scs_inference,[],[1,3])). % 116.33/116.42 cnf(8,plain, % 116.33/116.42 (P1(x81,x81)), % 116.33/116.42 inference(rename_variables,[],[1])). % 116.33/116.42 cnf(10,plain, % 116.33/116.42 (P1(x101,f4(x101,x102))), % 116.33/116.42 inference(scs_inference,[],[1,8,3,4])). % 116.33/116.42 cnf(14,plain, % 116.33/116.42 (P1(x141,f4(x142,x141))), % 116.33/116.42 inference(rename_variables,[],[7])). % 116.33/116.42 cnf(16,plain, % 116.33/116.42 (P1(x161,f4(x162,f4(x163,x161)))), % 116.33/116.42 inference(scs_inference,[],[7,14,4,3])). % 116.33/116.42 cnf(20,plain, % 116.33/116.42 (P1(x201,f4(x201,x202))), % 116.33/116.42 inference(rename_variables,[],[10])). % 116.33/116.42 cnf(22,plain, % 116.33/116.42 (P1(x221,f4(f4(x221,x222),x223))), % 116.33/116.42 inference(scs_inference,[],[10,20,3,4])). % 116.33/116.42 cnf(28,plain, % 116.33/116.42 (~P2(f1(x281),a2)+P2(f1(f5(x281)),a3)), % 116.33/116.42 inference(scs_inference,[],[1,2,5])). % 116.33/116.42 cnf(37,plain, % 116.33/116.42 (~P2(f1(x371),a3)+P2(f1(f5(x371)),a2)), % 116.33/116.42 inference(scs_inference,[],[1,2,6])). % 116.33/116.42 cnf(40,plain, % 116.33/116.42 (P2(f1(f5(x401)),a2)+P2(f1(x401),a2)), % 116.33/116.42 inference(scs_inference,[],[2,37])). % 116.33/116.42 cnf(45,plain, % 116.33/116.42 (~P2(f1(x451),a2)+P2(f1(f4(f4(f5(x451),x452),x453)),a3)), % 116.33/116.42 inference(scs_inference,[],[22,2,5])). % 116.33/116.42 cnf(49,plain, % 116.33/116.42 (~P2(f1(f5(x491)),a2)+P2(f1(x491),a3)), % 116.33/116.42 inference(scs_inference,[],[1,2,5])). % 116.33/116.42 cnf(97,plain, % 116.33/116.42 (P2(f1(f5(f5(x971))),a3)+P2(f1(x971),a2)), % 116.33/116.42 inference(scs_inference,[],[28,40])). % 116.33/116.42 cnf(98,plain, % 116.33/116.42 (P2(f1(f5(f5(x981))),a2)+~P2(f1(x981),a2)), % 116.33/116.42 inference(scs_inference,[],[28,37])). % 116.33/116.42 cnf(179,plain, % 116.33/116.42 (~P2(f1(f5(x1791)),a2)+~P2(f1(f4(x1792,f4(x1793,f5(x1791)))),a3)), % 116.33/116.42 inference(scs_inference,[],[16,49,6])). % 116.33/116.42 cnf(364,plain, % 116.33/116.42 (~P2(f1(f5(x3641)),a2)+~P2(f1(x3642),a2)), % 116.33/116.42 inference(scs_inference,[],[179,45])). % 116.33/116.42 cnf(365,plain, % 116.33/116.42 (~P2(f1(x3651),a2)), % 116.33/116.42 inference(scs_inference,[],[364,98])). % 116.33/116.42 cnf(367,plain, % 116.33/116.42 (~P2(f1(x3671),a2)), % 116.33/116.42 inference(rename_variables,[],[365])). % 116.33/116.42 cnf(370,plain, % 116.33/116.42 ($false), % 116.33/116.42 inference(scs_inference,[],[365,367,37,40,97]), % 116.33/116.42 ['proof']). % 116.33/116.42 % SZS output end Proof % 116.33/116.42 % Total time :115.780000s %------------------------------------------------------------------------------