%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL088-1 : TPTP v8.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n023.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 04:45:05 EDT 2024 % Result : Unsatisfiable 117.05s 117.15s % Output : CNFRefutation 117.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COL088-1 : TPTP v8.2.0. Released v2.7.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.33 % Computer : n023.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Tue Jun 18 16:18:24 EDT 2024 % 0.14/0.34 % CPUTime : % 0.54/0.57 start to proof:theBenchmark % 117.05/117.13 %------------------------------------------- % 117.05/117.13 % File :CSE---1.7 % 117.05/117.13 % Problem :theBenchmark % 117.05/117.13 % Transform :cnf % 117.05/117.13 % Format :tptp:raw % 117.05/117.13 % Command :java -jar mcs_scs.jar %d %s % 117.05/117.13 % 117.05/117.13 % Result :Theorem 116.500000s % 117.05/117.13 % Output :CNFRefutation 116.500000s % 117.05/117.13 %------------------------------------------- % 117.05/117.14 %-------------------------------------------------------------------------- % 117.05/117.14 % File : COL088-1 : TPTP v8.2.0. Released v2.7.0. % 117.05/117.14 % Domain : Combinatory Logic % 117.05/117.14 % Problem : ap_reduce1_2c1 % 117.05/117.14 % Version : Reduced > Especial. % 117.05/117.14 % English : [| p ---> q; r \<in> comb |] ==> p#r ---> q#r % 117.05/117.14 % 117.05/117.14 % Refs : [Men03] Meng (2003), Email to G. Sutcliffe % 117.05/117.14 % Source : [Men03] % 117.05/117.14 % Names : % 117.05/117.14 % 117.05/117.14 % Status : Unsatisfiable % 117.05/117.14 % Rating : 0.25 v8.2.0, 0.29 v8.1.0, 0.21 v7.5.0, 0.26 v7.4.0, 0.24 v7.3.0, 0.17 v7.1.0, 0.08 v7.0.0, 0.27 v6.3.0, 0.18 v6.2.0, 0.30 v6.1.0, 0.21 v6.0.0, 0.40 v5.5.0, 0.60 v5.3.0, 0.67 v5.2.0, 0.56 v5.1.0, 0.59 v5.0.0, 0.50 v4.1.0, 0.54 v4.0.1, 0.45 v4.0.0, 0.36 v3.7.0, 0.20 v3.5.0, 0.27 v3.4.0, 0.42 v3.3.0, 0.50 v3.2.0, 0.54 v3.1.0, 0.36 v2.7.0 % 117.05/117.14 % Syntax : Number of clauses : 44 ( 14 unt; 1 nHn; 43 RR) % 117.05/117.14 % Number of literals : 93 ( 15 equ; 52 neg) % 117.05/117.14 % Maximal clause size : 5 ( 2 avg) % 117.05/117.14 % Maximal term depth : 5 ( 1 avg) % 117.05/117.14 % Number of predicates : 7 ( 6 usr; 0 prp; 1-3 aty) % 117.05/117.14 % Number of functors : 15 ( 15 usr; 8 con; 0-3 aty) % 117.05/117.14 % Number of variables : 97 ( 25 sgn) % 117.05/117.14 % SPC : CNF_UNS_RFO_SEQ_NHN % 117.05/117.14 % 117.05/117.14 % Comments : Problem coming out of an Isabelle proof. % 117.05/117.14 %-------------------------------------------------------------------------- % 117.05/117.14 %----axioms from CombZF.thy. % 117.05/117.14 %----free algebra for K, S, comb_app(P,Q). % 117.05/117.14 % 117.05/117.14 cnf(k_s,axiom, % 117.05/117.14 combK != combS ). % 117.05/117.14 % 117.05/117.14 cnf(k_app,axiom, % 117.05/117.14 combK != comb_app(P,Q) ). % 117.05/117.14 % 117.05/117.14 cnf(s_app,axiom, % 117.05/117.14 combS != comb_app(P,Q) ). % 117.05/117.14 % 117.05/117.14 cnf(app_app1,axiom, % 117.05/117.14 ( comb_app(P1,Q1) != comb_app(P2,Q2) % 117.05/117.14 | P1 = P2 ) ). % 117.05/117.14 % 117.05/117.14 cnf(app_app2,axiom, % 117.05/117.14 ( comb_app(P1,Q1) != comb_app(P2,Q2) % 117.05/117.14 | Q1 = Q2 ) ). % 117.05/117.14 % 117.05/117.14 cnf(app_app3,axiom, % 117.05/117.14 ( P1 != P2 % 117.05/117.14 | Q1 != Q2 % 117.05/117.14 | comb_app(P1,Q1) = comb_app(P2,Q2) ) ). % 117.05/117.14 % 117.05/117.14 %----add in Ap_E. % 117.05/117.14 cnf(ap_E1,axiom, % 117.05/117.14 ( ~ member(comb_app(P,Q),comb) % 117.05/117.14 | member(P,comb) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_E2,axiom, % 117.05/117.14 ( ~ member(comb_app(P,Q),comb) % 117.05/117.14 | member(Q,comb) ) ). % 117.05/117.14 % 117.05/117.14 %----add in comb.intros(three of them). % 117.05/117.14 cnf(comb_intros1,axiom, % 117.05/117.14 member(combK,comb) ). % 117.05/117.14 % 117.05/117.14 cnf(comb_intros2,axiom, % 117.05/117.14 member(combS,comb) ). % 117.05/117.14 % 117.05/117.14 cnf(comb_intros3,axiom, % 117.05/117.14 ( ~ member(P,comb) % 117.05/117.14 | ~ member(Q,comb) % 117.05/117.14 | member(comb_app(P,Q),comb) ) ). % 117.05/117.14 % 117.05/117.14 %----add in reduction_refl [intro!]: % 117.05/117.14 cnf(reduction_refl,axiom, % 117.05/117.14 ( ~ member(A,comb) % 117.05/117.14 | member(pair(A,A),rtrancl(contract)) ) ). % 117.05/117.14 % 117.05/117.14 %----add in contract.K % 117.05/117.14 cnf(contract_K,axiom, % 117.05/117.14 ( ~ member(P,comb) % 117.05/117.14 | ~ member(Q,comb) % 117.05/117.14 | member(pair(comb_app(comb_app(combK,P),Q),P),contract) ) ). % 117.05/117.14 % 117.05/117.14 %----add in contract.S % 117.05/117.14 cnf(contract_S,axiom, % 117.05/117.14 ( ~ member(P,comb) % 117.05/117.14 | ~ member(Q,comb) % 117.05/117.14 | ~ member(R,comb) % 117.05/117.14 | member(pair(comb_app(comb_app(comb_app(combS,P),Q),R),comb_app(comb_app(P,R),comb_app(Q,R))),contract) ) ). % 117.05/117.14 % 117.05/117.14 %----this manually rename the formula Ap_contractE % 117.05/117.14 cnf(ap_contractE1,axiom, % 117.05/117.14 ( ~ member(pair(comb_app(P,Q),R),contract) % 117.05/117.14 | ap_contractE_c1(P,Q,R) % 117.05/117.14 | ap_contractE_c2(P,Q,R) % 117.05/117.14 | ap_contractE_c3(P,Q,R) % 117.05/117.14 | ap_contractE_c4(P,Q,R) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE2,axiom, % 117.05/117.14 ( ~ ap_contractE_c1(P,Q,R) % 117.05/117.14 | member(R,comb) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE3,axiom, % 117.05/117.14 ( ~ ap_contractE_c1(P,Q,R) % 117.05/117.14 | member(Q,comb) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE4,axiom, % 117.05/117.14 ( ~ ap_contractE_c1(P,Q,R) % 117.05/117.14 | P = comb_app(combK,R) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE5,axiom, % 117.05/117.14 ( ~ ap_contractE_c2(P,Q,R) % 117.05/117.14 | member(ap_contractE_sk1p(P,Q,R),comb) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE6,axiom, % 117.05/117.14 ( ~ ap_contractE_c2(P,Q,R) % 117.05/117.14 | member(ap_contractE_sk1q(P,Q,R),comb) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE7,axiom, % 117.05/117.14 ( ~ ap_contractE_c2(P,Q,R) % 117.05/117.14 | member(Q,comb) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE8,axiom, % 117.05/117.14 ( ~ ap_contractE_c2(P,Q,R) % 117.05/117.14 | R = comb_app(comb_app(ap_contractE_sk1p(P,Q,R),Q),comb_app(ap_contractE_sk1q(P,Q,R),Q)) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE9,axiom, % 117.05/117.14 ( ~ ap_contractE_c2(P,Q,R) % 117.05/117.14 | P = comb_app(comb_app(combS,ap_contractE_sk1p(P,Q,R)),ap_contractE_sk1q(P,Q,R)) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE10,axiom, % 117.05/117.14 ( ~ ap_contractE_c3(P,Q,R) % 117.05/117.14 | member(pair(P,ap_contractE_sk2q(P,Q,R)),contract) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE11,axiom, % 117.05/117.14 ( ~ ap_contractE_c3(P,Q,R) % 117.05/117.14 | member(Q,comb) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE12,axiom, % 117.05/117.14 ( ~ ap_contractE_c3(P,Q,R) % 117.05/117.14 | R = comb_app(ap_contractE_sk2q(P,Q,R),Q) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE13,axiom, % 117.05/117.14 ( ~ ap_contractE_c4(P,Q,R) % 117.05/117.14 | member(pair(Q,ap_contractE_sk3q(P,Q,R)),contract) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE14,axiom, % 117.05/117.14 ( ~ ap_contractE_c4(P,Q,R) % 117.05/117.14 | member(P,comb) ) ). % 117.05/117.14 % 117.05/117.14 cnf(ap_contractE15,axiom, % 117.05/117.14 ( ~ ap_contractE_c4(P,Q,R) % 117.05/117.14 | R = comb_app(P,ap_contractE_sk3q(P,Q,R)) ) ). % 117.05/117.14 % 117.05/117.14 %----add in K_contractE[elim!]: % 117.05/117.14 cnf(k_contractE,axiom, % 117.05/117.14 ~ member(pair(combK,R),contract) ). % 117.05/117.14 % 117.05/117.14 %----add in S_contractE [elim!]: % 117.05/117.14 %----converted by tptp2X(Ap_contractE+cls_otter.tptp) % 117.05/117.14 cnf(s_contractE,axiom, % 117.05/117.14 ~ member(pair(combS,R),contract) ). % 117.05/117.14 % 117.05/117.14 %----second subgoal % 117.05/117.14 %----local axioms: transD,trans_rtrancl,contract_combD2,reduction_rls % 117.05/117.14 cnf(transD,axiom, % 117.05/117.14 ( ~ trans(R) % 117.05/117.14 | ~ member(pair(A,B),R) % 117.05/117.15 | ~ member(pair(B,C),R) % 117.05/117.15 | member(pair(A,C),R) ) ). % 117.05/117.15 % 117.05/117.15 cnf(trans_rtrancl,axiom, % 117.05/117.15 trans(rtrancl(R)) ). % 117.05/117.15 % 117.05/117.15 cnf(contract_combD2,axiom, % 117.05/117.15 ( ~ member(pair(A,B),contract) % 117.05/117.15 | member(B,comb) ) ). % 117.05/117.15 % 117.05/117.15 cnf(reduction_rls_1,axiom, % 117.05/117.15 ( ~ member(B,comb) % 117.05/117.15 | ~ member(Q3,comb) % 117.05/117.15 | ~ member(pair(B,C),rtrancl(contract)) % 117.05/117.15 | member(pair(comb_app(comb_app(combK,B),Q3),C),rtrancl(contract)) ) ). % 117.05/117.15 % 117.05/117.15 cnf(reduction_rls_2,axiom, % 117.05/117.15 ( ~ member(P3,comb) % 117.05/117.15 | ~ member(Q3,comb) % 117.05/117.15 | ~ member(R3,comb) % 117.05/117.15 | ~ member(pair(comb_app(comb_app(P3,R3),comb_app(Q3,R3)),C),rtrancl(contract)) % 117.05/117.15 | member(pair(comb_app(comb_app(comb_app(combS,P3),Q3),R3),C),rtrancl(contract)) ) ). % 117.05/117.15 % 117.05/117.15 cnf(reduction_rls_3,axiom, % 117.05/117.15 ( ~ member(pair(P3,Q3),contract) % 117.05/117.15 | ~ member(R3,comb) % 117.05/117.15 | ~ member(pair(comb_app(Q3,R3),C),rtrancl(contract)) % 117.05/117.15 | member(pair(comb_app(P3,R3),C),rtrancl(contract)) ) ). % 117.05/117.15 % 117.05/117.15 cnf(reduction_rls_4,axiom, % 117.05/117.15 ( ~ member(pair(P3,Q3),contract) % 117.05/117.15 | ~ member(R3,comb) % 117.05/117.15 | ~ member(pair(comb_app(R3,Q3),C),rtrancl(contract)) % 117.05/117.15 | member(pair(comb_app(R3,P3),C),rtrancl(contract)) ) ). % 117.05/117.15 % 117.05/117.15 cnf(ap_reduce1_2h1,hypothesis, % 117.05/117.15 member(r,comb) ). % 117.05/117.15 % 117.05/117.15 cnf(ap_reduce1_2h2,hypothesis, % 117.05/117.15 member(p,comb) ). % 117.05/117.15 % 117.05/117.15 cnf(ap_reduce1_2h3,hypothesis, % 117.05/117.15 member(pair(p,y),rtrancl(contract)) ). % 117.05/117.15 % 117.05/117.15 cnf(ap_reduce1_2h4,hypothesis, % 117.05/117.15 member(pair(y,z),contract) ). % 117.05/117.15 % 117.05/117.15 cnf(ap_reduce1_2h5,hypothesis, % 117.05/117.15 member(pair(comb_app(p,r),comb_app(y,r)),rtrancl(contract)) ). % 117.05/117.15 % 117.05/117.15 cnf(ap_reduce1_2c1,negated_conjecture, % 117.05/117.15 ~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)) ). % 117.05/117.15 % 117.05/117.15 %-------------------------------------------------------------------------- % 117.05/117.15 %------------------------------------------- % 117.05/117.15 % Proof found % 117.05/117.15 % SZS status Theorem for theBenchmark % 117.05/117.15 % SZS output start Proof % 117.05/117.15 %ClaNum:78(EqnAxiom:35) % 117.05/117.15 %VarNum:201(SingletonVarNum:93) % 117.05/117.15 %MaxLitNum:5 % 117.05/117.15 %MaxfuncDepth:4 % 117.05/117.15 %SharedTerms:25 % 117.05/117.15 %goalClause: 49 % 117.05/117.15 %singleGoalClaCount:1 % 117.05/117.15 [37]P2(a2,a3) % 117.05/117.15 [38]P2(a8,a3) % 117.05/117.15 [39]P2(a9,a3) % 117.05/117.15 [40]P2(a10,a3) % 117.05/117.15 [44]~E(a8,a2) % 117.05/117.15 [41]P2(f13(a14,a15),a11) % 117.05/117.15 [42]P2(f13(a10,a14),f1(a11)) % 117.05/117.15 [43]P2(f13(f12(a10,a9),f12(a14,a9)),f1(a11)) % 117.05/117.15 [49]~P2(f13(f12(a10,a9),f12(a15,a9)),f1(a11)) % 117.05/117.15 [36]P1(f1(x361)) % 117.05/117.15 [47]~P2(f13(a2,x471),a11) % 117.05/117.15 [48]~P2(f13(a8,x481),a11) % 117.05/117.15 [45]~E(f12(x451,x452),a2) % 117.05/117.15 [46]~E(f12(x461,x462),a8) % 117.05/117.15 [52]~P2(x521,a3)+P2(f13(x521,x521),f1(a11)) % 117.05/117.15 [53]P2(x531,a3)+~P2(f12(x532,x531),a3) % 117.05/117.15 [54]P2(x541,a3)+~P2(f13(x542,x541),a11) % 117.05/117.15 [55]P2(x551,a3)+~P2(f12(x551,x552),a3) % 117.05/117.15 [57]~P3(x572,x573,x571)+P2(x571,a3) % 117.05/117.15 [58]~P3(x582,x581,x583)+P2(x581,a3) % 117.05/117.15 [59]~P4(x592,x591,x593)+P2(x591,a3) % 117.05/117.15 [60]~P5(x602,x601,x603)+P2(x601,a3) % 117.05/117.15 [61]~P6(x611,x612,x613)+P2(x611,a3) % 117.05/117.15 [62]~P3(x621,x623,x622)+E(x621,f12(a2,x622)) % 117.05/117.15 [64]~P4(x641,x642,x643)+P2(f4(x641,x642,x643),a3) % 117.05/117.15 [65]~P4(x651,x652,x653)+P2(f5(x651,x652,x653),a3) % 117.05/117.15 [66]~P6(x661,x662,x663)+E(f12(x661,f6(x661,x662,x663)),x663) % 117.05/117.15 [67]~P5(x671,x672,x673)+E(f12(f7(x671,x672,x673),x672),x673) % 117.05/117.15 [72]~P6(x722,x721,x723)+P2(f13(x721,f6(x722,x721,x723)),a11) % 117.05/117.15 [73]~P5(x731,x732,x733)+P2(f13(x731,f7(x731,x732,x733)),a11) % 117.05/117.15 [75]~P4(x751,x752,x753)+E(f12(f12(a8,f4(x751,x752,x753)),f5(x751,x752,x753)),x751) % 117.05/117.15 [76]~P4(x761,x762,x763)+E(f12(f12(f4(x761,x762,x763),x762),f12(f5(x761,x762,x763),x762)),x763) % 117.05/117.15 [50]E(x501,x502)+~E(f12(x503,x501),f12(x504,x502)) % 117.05/117.15 [51]E(x511,x512)+~E(f12(x511,x513),f12(x512,x514)) % 117.05/117.15 [56]~P2(x562,a3)+~P2(x561,a3)+P2(f12(x561,x562),a3) % 117.05/117.15 [68]~P2(x682,a3)+~P2(x681,a3)+P2(f13(f12(f12(a2,x681),x682),x681),a11) % 117.05/117.15 [69]~P2(x692,a3)+~P2(x691,a3)+~P2(f13(x691,x693),f1(a11))+P2(f13(f12(f12(a2,x691),x692),x693),f1(a11)) % 117.05/117.15 [77]~P2(x773,a3)+~P2(x772,a3)+~P2(x771,a3)+P2(f13(f12(f12(f12(a8,x771),x772),x773),f12(f12(x771,x773),f12(x772,x773))),a11) % 117.05/117.15 [63]~P1(x633)+~P2(f13(x631,x634),x633)+P2(f13(x631,x632),x633)+~P2(f13(x634,x632),x633) % 117.05/117.15 [70]~P2(x701,a3)+~P2(f13(x702,x704),a11)+~P2(f13(f12(x701,x704),x703),f1(a11))+P2(f13(f12(x701,x702),x703),f1(a11)) % 117.05/117.15 [71]~P2(x712,a3)+~P2(f13(x711,x714),a11)+~P2(f13(f12(x714,x712),x713),f1(a11))+P2(f13(f12(x711,x712),x713),f1(a11)) % 117.05/117.15 [74]P4(x741,x742,x743)+P5(x741,x742,x743)+P6(x741,x742,x743)+P3(x741,x742,x743)+~P2(f13(f12(x741,x742),x743),a11) % 117.05/117.15 [78]~P2(x783,a3)+~P2(x782,a3)+~P2(x781,a3)+~P2(f13(f12(f12(x781,x783),f12(x782,x783)),x784),f1(a11))+P2(f13(f12(f12(f12(a8,x781),x782),x783),x784),f1(a11)) % 117.05/117.15 %EqnAxiom % 117.05/117.15 [1]E(x11,x11) % 117.05/117.15 [2]E(x22,x21)+~E(x21,x22) % 117.05/117.15 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.05/117.15 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 117.05/117.15 [5]~E(x51,x52)+E(f13(x51,x53),f13(x52,x53)) % 117.05/117.15 [6]~E(x61,x62)+E(f13(x63,x61),f13(x63,x62)) % 117.05/117.15 [7]~E(x71,x72)+E(f12(x71,x73),f12(x72,x73)) % 117.05/117.15 [8]~E(x81,x82)+E(f12(x83,x81),f12(x83,x82)) % 117.05/117.15 [9]~E(x91,x92)+E(f6(x91,x93,x94),f6(x92,x93,x94)) % 117.05/117.15 [10]~E(x101,x102)+E(f6(x103,x101,x104),f6(x103,x102,x104)) % 117.05/117.15 [11]~E(x111,x112)+E(f6(x113,x114,x111),f6(x113,x114,x112)) % 117.05/117.15 [12]~E(x121,x122)+E(f7(x121,x123,x124),f7(x122,x123,x124)) % 117.05/117.15 [13]~E(x131,x132)+E(f7(x133,x131,x134),f7(x133,x132,x134)) % 117.05/117.15 [14]~E(x141,x142)+E(f7(x143,x144,x141),f7(x143,x144,x142)) % 117.05/117.15 [15]~E(x151,x152)+E(f4(x151,x153,x154),f4(x152,x153,x154)) % 117.05/117.15 [16]~E(x161,x162)+E(f4(x163,x161,x164),f4(x163,x162,x164)) % 117.05/117.15 [17]~E(x171,x172)+E(f4(x173,x174,x171),f4(x173,x174,x172)) % 117.05/117.15 [18]~E(x181,x182)+E(f5(x181,x183,x184),f5(x182,x183,x184)) % 117.05/117.15 [19]~E(x191,x192)+E(f5(x193,x191,x194),f5(x193,x192,x194)) % 117.05/117.15 [20]~E(x201,x202)+E(f5(x203,x204,x201),f5(x203,x204,x202)) % 117.05/117.15 [21]~P1(x211)+P1(x212)+~E(x211,x212) % 117.05/117.15 [22]P2(x222,x223)+~E(x221,x222)+~P2(x221,x223) % 117.05/117.15 [23]P2(x233,x232)+~E(x231,x232)+~P2(x233,x231) % 117.05/117.15 [24]P4(x242,x243,x244)+~E(x241,x242)+~P4(x241,x243,x244) % 117.05/117.15 [25]P4(x253,x252,x254)+~E(x251,x252)+~P4(x253,x251,x254) % 117.05/117.15 [26]P4(x263,x264,x262)+~E(x261,x262)+~P4(x263,x264,x261) % 117.05/117.15 [27]P3(x272,x273,x274)+~E(x271,x272)+~P3(x271,x273,x274) % 117.05/117.15 [28]P3(x283,x282,x284)+~E(x281,x282)+~P3(x283,x281,x284) % 117.05/117.15 [29]P3(x293,x294,x292)+~E(x291,x292)+~P3(x293,x294,x291) % 117.05/117.15 [30]P6(x302,x303,x304)+~E(x301,x302)+~P6(x301,x303,x304) % 117.05/117.15 [31]P6(x313,x312,x314)+~E(x311,x312)+~P6(x313,x311,x314) % 117.05/117.15 [32]P6(x323,x324,x322)+~E(x321,x322)+~P6(x323,x324,x321) % 117.05/117.15 [33]P5(x332,x333,x334)+~E(x331,x332)+~P5(x331,x333,x334) % 117.05/117.15 [34]P5(x343,x342,x344)+~E(x341,x342)+~P5(x343,x341,x344) % 117.05/117.15 [35]P5(x353,x354,x352)+~E(x351,x352)+~P5(x353,x354,x351) % 117.05/117.15 % 117.05/117.15 %------------------------------------------- % 117.16/117.16 cnf(81,plain, % 117.16/117.16 (P2(a15,a3)), % 117.16/117.16 inference(scs_inference,[],[41,54])). % 117.16/117.16 cnf(83,plain, % 117.16/117.16 (~P6(x831,x832,a2)), % 117.16/117.16 inference(scs_inference,[],[41,45,54,66])). % 117.16/117.16 cnf(84,plain, % 117.16/117.16 (~E(f12(x841,x842),a2)), % 117.16/117.16 inference(rename_variables,[],[45])). % 117.16/117.16 cnf(86,plain, % 117.16/117.16 (~P5(x861,x862,a2)), % 117.16/117.16 inference(scs_inference,[],[41,45,84,54,66,67])). % 117.16/117.16 cnf(87,plain, % 117.16/117.16 (~E(f12(x871,x872),a2)), % 117.16/117.16 inference(rename_variables,[],[45])). % 117.16/117.16 cnf(89,plain, % 117.16/117.16 (~P6(x891,a2,x892)), % 117.16/117.16 inference(scs_inference,[],[47,41,45,84,54,66,67,72])). % 117.16/117.16 cnf(90,plain, % 117.16/117.16 (~P2(f13(a2,x901),a11)), % 117.16/117.16 inference(rename_variables,[],[47])). % 117.16/117.16 cnf(92,plain, % 117.16/117.16 (~P5(a2,x921,x922)), % 117.16/117.16 inference(scs_inference,[],[47,90,41,45,84,54,66,67,72,73])). % 117.16/117.16 cnf(96,plain, % 117.16/117.16 (~E(f12(x961,x962),a2)), % 117.16/117.16 inference(rename_variables,[],[45])). % 117.16/117.16 cnf(98,plain, % 117.16/117.16 (~P4(x981,x982,a2)), % 117.16/117.16 inference(scs_inference,[],[47,90,41,45,84,87,96,54,66,67,72,73,75,76])). % 117.16/117.16 cnf(103,plain, % 117.16/117.16 (~P2(f13(x1031,a10),f1(a11))+P2(f13(x1031,a14),f1(a11))), % 117.16/117.16 inference(scs_inference,[],[49,36,37,42,47,90,41,45,84,87,96,54,66,67,72,73,75,76,22,23,63])). % 117.16/117.16 cnf(108,plain, % 117.16/117.16 (~P2(f13(a10,x1081),a11)+~P2(f13(f12(x1081,a9),f12(a15,a9)),f1(a11))), % 117.16/117.16 inference(scs_inference,[],[49,36,37,39,40,42,47,90,41,45,84,87,96,54,66,67,72,73,75,76,22,23,63,70,71])). % 117.16/117.16 cnf(114,plain, % 117.16/117.16 (~E(f12(x1141,x1142),a8)), % 117.16/117.16 inference(rename_variables,[],[46])). % 117.16/117.16 cnf(116,plain, % 117.16/117.16 (~P5(x1161,x1162,a8)), % 117.16/117.16 inference(scs_inference,[],[46,114,75,67])). % 117.16/117.16 cnf(117,plain, % 117.16/117.16 (~E(f12(x1171,x1172),a8)), % 117.16/117.16 inference(rename_variables,[],[46])). % 117.16/117.16 cnf(119,plain, % 117.16/117.16 (~P6(x1191,x1192,a8)), % 117.16/117.16 inference(scs_inference,[],[46,114,117,75,67,66])). % 117.16/117.16 cnf(120,plain, % 117.16/117.16 (~E(f12(x1201,x1202),a8)), % 117.16/117.16 inference(rename_variables,[],[46])). % 117.16/117.16 cnf(122,plain, % 117.16/117.16 (~P4(x1221,x1222,a8)), % 117.16/117.16 inference(scs_inference,[],[46,114,117,120,75,67,66,76])). % 117.16/117.16 cnf(126,plain, % 117.16/117.16 (~P2(f13(a8,x1261),a11)), % 117.16/117.16 inference(rename_variables,[],[48])). % 117.16/117.16 cnf(131,plain, % 117.16/117.16 (~E(f13(f12(a10,a9),f12(a14,a9)),f13(f12(a10,a9),f12(a15,a9)))), % 117.16/117.16 inference(scs_inference,[],[49,48,126,43,46,114,117,120,75,67,66,76,72,73,22])). % 117.16/117.16 cnf(133,plain, % 117.16/117.16 (~E(a14,a15)), % 117.16/117.16 inference(scs_inference,[],[49,48,126,43,46,114,117,120,75,67,66,76,72,73,22,6,7])). % 117.16/117.16 cnf(139,plain, % 117.16/117.16 (~E(f13(a14,a15),f13(a2,x1391))), % 117.16/117.16 inference(scs_inference,[],[41,47,22])). % 117.16/117.16 cnf(140,plain, % 117.16/117.16 (~E(a14,a2)), % 117.16/117.16 inference(scs_inference,[],[41,47,22,5])). % 117.16/117.16 cnf(147,plain, % 117.16/117.16 (~E(f13(a14,a15),f13(a8,x1471))), % 117.16/117.16 inference(scs_inference,[],[48,41,22])). % 117.16/117.16 cnf(198,plain, % 117.16/117.16 (~E(a2,a14)), % 117.16/117.16 inference(scs_inference,[],[139,2,5])). % 117.16/117.16 cnf(199,plain, % 117.16/117.16 (~P3(x1991,x1992,x1993)+P2(f13(x1993,x1993),f1(a11))), % 117.16/117.16 inference(scs_inference,[],[57,52])). % 117.16/117.16 cnf(210,plain, % 117.16/117.16 (P2(x2101,a3)+~P2(f12(x2102,f12(x2101,x2103)),a3)), % 117.16/117.16 inference(scs_inference,[],[53,55])). % 117.16/117.16 cnf(211,plain, % 117.16/117.16 (E(a2,f12(a2,a2))+~P2(f13(f12(a2,a2),a2),a11)), % 117.16/117.16 inference(scs_inference,[],[92,89,98,62,74])). % 117.16/117.16 cnf(238,plain, % 117.16/117.16 (~E(f13(x2381,a14),f13(f12(a10,a9),f12(a15,a9)))+~P2(f13(x2381,a10),f1(a11))), % 117.16/117.16 inference(scs_inference,[],[49,103,22])). % 117.16/117.16 cnf(239,plain, % 117.16/117.16 (~P2(f13(f12(a2,a2),a2),a11)), % 117.16/117.16 inference(scs_inference,[],[45,211,2])). % 117.16/117.16 cnf(249,plain, % 117.16/117.16 (~E(f13(a14,a15),f13(f12(a2,a2),a2))), % 117.16/117.16 inference(scs_inference,[],[239,41,22])). % 117.16/117.16 cnf(323,plain, % 117.16/117.16 (P3(x3231,x3232,a8)+~E(x3233,x3232)+~P2(f13(f12(x3231,x3233),a8),a11)), % 117.16/117.16 inference(scs_inference,[],[116,119,122,28,74])). % 117.16/117.16 cnf(324,plain, % 117.16/117.16 (P3(x3242,x3241,a8)+~P2(f13(f12(x3242,x3241),a8),a11)), % 117.16/117.16 inference(equality_inference,[],[323])). % 117.16/117.16 cnf(325,plain, % 117.16/117.16 (P2(x3251,a3)+~P2(f13(f12(x3252,x3251),a8),a11)), % 117.16/117.16 inference(scs_inference,[],[324,58])). % 117.16/117.16 cnf(326,plain, % 117.16/117.16 (~P2(f13(f12(x3261,x3262),a8),a11)+P2(f13(x3262,x3262),f1(a11))), % 117.16/117.16 inference(scs_inference,[],[325,52])). % 117.16/117.16 cnf(327,plain, % 117.16/117.16 (~P2(f13(f12(x3271,f12(a15,a9)),a8),a11)+~P2(f13(a10,a15),a11)), % 117.16/117.16 inference(scs_inference,[],[326,108])). % 117.16/117.16 cnf(328,plain, % 117.16/117.16 (~E(f13(a14,a15),f13(a10,a15))+~P2(f13(f12(x3281,f12(a15,a9)),a8),a11)), % 117.16/117.16 inference(scs_inference,[],[41,327,22])). % 117.16/117.16 cnf(329,plain, % 117.16/117.16 (~E(f13(a10,a15),f13(a14,a15))+~P2(f13(f12(x3291,f12(a15,a9)),a8),a11)), % 117.16/117.16 inference(scs_inference,[],[328,2])). % 117.16/117.16 cnf(330,plain, % 117.16/117.16 (~E(a10,a14)+~P2(f13(f12(x3301,f12(a15,a9)),a8),a11)), % 117.16/117.16 inference(scs_inference,[],[329,5])). % 117.16/117.16 cnf(331,plain, % 117.16/117.16 (~P2(f12(a15,a9),a3)+~E(a10,a14)), % 117.16/117.16 inference(scs_inference,[],[38,330,68])). % 117.16/117.16 cnf(332,plain, % 117.16/117.16 (~E(a10,a14)), % 117.16/117.16 inference(scs_inference,[],[39,81,331,56])). % 117.16/117.16 cnf(390,plain, % 117.16/117.16 (~E(a8,a14)), % 117.16/117.16 inference(scs_inference,[],[147,2,5])). % 117.16/117.16 cnf(391,plain, % 117.16/117.16 (~E(f12(a15,a9),f12(a14,a9))), % 117.16/117.16 inference(scs_inference,[],[131,2,6])). % 117.16/117.16 cnf(392,plain, % 117.16/117.16 (~E(a15,a14)), % 117.16/117.16 inference(scs_inference,[],[391,7])). % 117.16/117.16 cnf(400,plain, % 117.16/117.16 (~E(f12(a14,x4001),f12(a8,x4002))), % 117.16/117.16 inference(scs_inference,[],[390,2,51])). % 117.16/117.16 cnf(405,plain, % 117.16/117.16 (~P3(a8,x4051,x4052)), % 117.16/117.16 inference(scs_inference,[],[46,2,62])). % 117.16/117.16 cnf(406,plain, % 117.16/117.16 (~E(f12(x4061,a14),f12(x4062,a15))), % 117.16/117.16 inference(scs_inference,[],[392,2,50])). % 117.16/117.16 cnf(451,plain, % 117.16/117.16 (~E(f12(f12(a8,x4511),x4512),f12(f12(a14,x4513),x4514))), % 117.16/117.16 inference(scs_inference,[],[400,2,51])). % 117.16/117.16 cnf(453,plain, % 117.16/117.16 (~E(f12(f12(a8,x4531),x4532),f12(f12(a14,x4533),x4534))), % 117.16/117.16 inference(rename_variables,[],[451])). % 117.16/117.16 cnf(456,plain, % 117.16/117.16 (~E(f12(f12(a8,x4561),x4562),f12(f12(a14,x4563),x4564))), % 117.16/117.16 inference(rename_variables,[],[451])). % 117.16/117.16 cnf(458,plain, % 117.16/117.16 (~E(f12(a8,x4581),f12(a14,x4582))), % 117.16/117.16 inference(scs_inference,[],[451,453,456,75,66,7])). % 117.16/117.16 cnf(464,plain, % 117.16/117.16 (~E(f12(x4641,f12(x4642,a15)),f12(x4643,f12(x4644,a14)))), % 117.16/117.16 inference(scs_inference,[],[406,2,50])). % 117.16/117.16 cnf(465,plain, % 117.16/117.16 (~E(f12(x4651,a15),f12(x4652,a14))), % 117.16/117.16 inference(scs_inference,[],[464,8])). % 117.16/117.16 cnf(530,plain, % 117.16/117.16 (~E(x5301,x5302)+~P2(f13(f12(a8,x5302),a8),a11)), % 117.16/117.16 inference(scs_inference,[],[405,2,323])). % 117.16/117.16 cnf(531,plain, % 117.16/117.16 (~P2(f13(f12(a8,x5311),a8),a11)), % 117.16/117.16 inference(equality_inference,[],[530])). % 117.16/117.16 cnf(534,plain, % 117.16/117.16 (~E(f12(x5341,f12(a14,x5342)),f12(x5343,f12(a8,x5344)))), % 117.16/117.16 inference(scs_inference,[],[458,2,50])). % 117.16/117.16 cnf(564,plain, % 117.16/117.16 (~E(f12(x5641,f12(x5642,a14)),f12(x5643,f12(x5644,a15)))), % 117.16/117.16 inference(scs_inference,[],[465,2,50])). % 117.16/117.16 cnf(606,plain, % 117.16/117.16 (~E(f13(f12(a8,x6061),a8),f13(a14,a15))), % 117.16/117.16 inference(scs_inference,[],[41,531,2,22])). % 117.16/117.16 cnf(610,plain, % 117.16/117.16 (~E(f12(x6101,f12(x6102,f12(a8,x6103))),f12(x6104,f12(x6105,f12(a14,x6106))))), % 117.16/117.16 inference(scs_inference,[],[534,2,50])). % 117.16/117.16 cnf(643,plain, % 117.16/117.16 (~E(f12(f12(x6431,f12(x6432,a15)),x6433),f12(f12(x6434,f12(x6435,a14)),x6436))), % 117.16/117.16 inference(scs_inference,[],[564,2,51])). % 117.16/117.16 cnf(768,plain, % 117.16/117.16 (~E(f13(f12(a10,a9),f12(a15,a9)),f13(a10,a14))), % 117.16/117.16 inference(scs_inference,[],[42,49,2,22])). % 117.16/117.16 cnf(786,plain, % 117.16/117.16 (~E(f12(a8,x7861),f12(f12(x7862,x7863),x7864))), % 117.16/117.16 inference(scs_inference,[],[46,2,51])). % 117.16/117.16 cnf(787,plain, % 117.16/117.16 (~E(a8,f12(x7871,x7872))), % 117.16/117.16 inference(scs_inference,[],[786,7])). % 117.16/117.16 cnf(845,plain, % 117.16/117.16 (~E(f12(x8451,f13(f12(a2,a2),a2)),f12(x8452,f13(a14,a15)))), % 117.16/117.16 inference(scs_inference,[],[249,2,50])). % 117.16/117.16 cnf(846,plain, % 117.16/117.16 (~E(f13(f12(a2,a2),a2),f13(a14,a15))), % 117.16/117.16 inference(scs_inference,[],[845,8])). % 117.16/117.16 cnf(1021,plain, % 117.16/117.16 (~E(f12(f13(a14,a15),x10211),f12(f13(f12(a8,x10212),a8),x10213))), % 117.16/117.16 inference(scs_inference,[],[606,2,51])). % 117.16/117.16 cnf(1102,plain, % 117.16/117.16 (~E(f12(x11021,f13(a10,a14)),f12(x11022,f13(f12(a10,a9),f12(a15,a9))))), % 117.16/117.16 inference(scs_inference,[],[768,2,50])). % 117.16/117.16 cnf(1152,plain, % 117.16/117.16 (~E(f12(x11521,f12(x11522,x11523)),f12(x11524,a8))), % 117.16/117.16 inference(scs_inference,[],[787,2,50])). % 117.16/117.16 cnf(1210,plain, % 117.16/117.16 (~E(f12(f13(a14,a15),x12101),f12(f13(f12(a2,a2),a2),x12102))), % 117.16/117.16 inference(scs_inference,[],[846,2,51])). % 117.16/117.16 cnf(1362,plain, % 117.16/117.16 (~E(f12(f12(x13621,a8),x13622),f12(f12(x13623,f12(x13624,x13625)),x13626))), % 117.16/117.16 inference(scs_inference,[],[1152,2,51])). % 117.16/117.16 cnf(1471,plain, % 117.16/117.16 (~E(f12(f12(f12(x14711,f12(x14712,x14713)),x14714),x14715),f12(f12(f12(x14716,a8),x14717),x14718))), % 117.16/117.16 inference(scs_inference,[],[1362,2,51])). % 117.16/117.16 cnf(1531,plain, % 117.16/117.16 (~E(x15311,a9)+P2(x15311,a3)), % 117.16/117.16 inference(scs_inference,[],[39,2,22])). % 117.16/117.16 cnf(1543,plain, % 117.16/117.16 (~E(f12(x15431,a2),f12(x15432,f12(x15433,x15434)))), % 117.16/117.16 inference(scs_inference,[],[45,2,50])). % 117.16/117.16 cnf(1544,plain, % 117.16/117.16 (~E(a2,f12(x15441,x15442))), % 117.16/117.16 inference(scs_inference,[],[1543,8])). % 117.16/117.16 cnf(1558,plain, % 117.16/117.16 (~E(x15581,a15)+P2(x15581,a3)), % 117.16/117.16 inference(scs_inference,[],[81,2,22])). % 117.16/117.16 cnf(1608,plain, % 117.16/117.16 (~E(f12(a14,x16081),f12(a10,x16082))), % 117.16/117.16 inference(scs_inference,[],[332,2,51])). % 117.16/117.16 cnf(1949,plain, % 117.16/117.16 (~E(f12(x19491,f12(f13(f12(a8,x19492),a8),x19493)),f12(x19494,f12(f13(a14,a15),x19495)))), % 117.16/117.16 inference(scs_inference,[],[1021,2,50])). % 117.16/117.16 cnf(1956,plain, % 117.16/117.16 (~E(f12(f12(x19561,f13(f12(a10,a9),f12(a15,a9))),x19562),f12(f12(x19563,f13(a10,a14)),x19564))), % 117.16/117.16 inference(scs_inference,[],[1102,2,51])). % 117.16/117.16 cnf(2038,plain, % 117.16/117.16 (~E(f12(x20381,f12(f13(f12(a2,a2),a2),x20382)),f12(x20383,f12(f13(a14,a15),x20384)))), % 117.16/117.16 inference(scs_inference,[],[1210,2,50])). % 117.16/117.16 cnf(2164,plain, % 117.16/117.16 (~E(f12(f12(x21641,x21642),x21643),f12(a2,x21644))), % 117.16/117.16 inference(scs_inference,[],[1544,2,51])). % 117.16/117.16 cnf(2165,plain, % 117.16/117.16 (~P4(f12(a2,x21651),x21652,x21653)), % 117.16/117.16 inference(scs_inference,[],[2164,75])). % 117.16/117.16 cnf(2395,plain, % 117.16/117.16 (~E(f12(f13(f12(a2,a2),a2),x23951),f12(f13(a14,a15),x23952))), % 117.16/117.16 inference(scs_inference,[],[2038,8])). % 117.16/117.16 cnf(2397,plain, % 117.16/117.16 (~E(f12(x23971,f13(f12(a10,a9),f12(a15,a9))),f12(x23972,f13(a10,a14)))), % 117.16/117.16 inference(scs_inference,[],[2038,1956,8,7])). % 117.16/117.16 cnf(2421,plain, % 117.16/117.16 (~E(f12(f13(f12(a8,x24211),a8),x24212),f12(f13(a14,a15),x24213))), % 117.16/117.16 inference(scs_inference,[],[1949,8])). % 117.16/117.16 cnf(2436,plain, % 117.16/117.16 (~E(f12(a14,x24361),f12(a15,x24362))), % 117.16/117.16 inference(scs_inference,[],[133,2397,1471,2,50,51])). % 117.16/117.16 cnf(2438,plain, % 117.16/117.16 (P2(f13(a2,a2),f1(a11))), % 117.16/117.16 inference(scs_inference,[],[133,2397,1471,37,2,50,51,52])). % 117.16/117.16 cnf(2440,plain, % 117.16/117.17 (P2(f12(a2,a2),a3)), % 117.16/117.17 inference(scs_inference,[],[133,2397,1471,37,2,50,51,52,56])). % 117.16/117.17 cnf(2442,plain, % 117.16/117.17 (P2(f13(f12(f12(a2,a2),a2),a2),a11)), % 117.16/117.17 inference(scs_inference,[],[133,2397,1471,37,2,50,51,52,56,68])). % 117.16/117.17 cnf(2444,plain, % 117.16/117.17 (~E(f1(a11),a11)), % 117.16/117.17 inference(scs_inference,[],[133,2397,1471,47,37,2,50,51,52,56,68,23])). % 117.16/117.17 cnf(2452,plain, % 117.16/117.17 (~P2(f13(f12(a14,a9),f12(a15,a9)),f1(a11))), % 117.16/117.17 inference(scs_inference,[],[49,133,2397,1471,36,47,37,43,2,50,51,52,56,68,23,77,69,70,63])). % 117.16/117.17 cnf(2468,plain, % 117.16/117.17 (~E(f12(a2,x24681),f12(a14,x24682))), % 117.16/117.17 inference(scs_inference,[],[198,51])). % 117.16/117.17 cnf(2472,plain, % 117.16/117.17 (~E(a11,f1(a11))), % 117.16/117.17 inference(scs_inference,[],[198,2444,2440,51,52,2])). % 117.16/117.17 cnf(2473,plain, % 117.16/117.17 (~E(f12(x24731,f1(a11)),f12(x24732,a11))), % 117.16/117.17 inference(scs_inference,[],[198,2444,2440,51,52,2,50])). % 117.16/117.17 cnf(2477,plain, % 117.16/117.17 (P2(f12(f12(a2,a2),f12(a2,a2)),a3)), % 117.16/117.17 inference(scs_inference,[],[198,2444,2440,51,52,2,50,68,56])). % 117.16/117.17 cnf(2497,plain, % 117.16/117.17 (~P3(f12(a14,x24971),x24972,x24973)), % 117.16/117.17 inference(scs_inference,[],[2468,2,62])). % 117.16/117.17 cnf(2501,plain, % 117.16/117.17 (~E(f12(a11,x25011),f12(f1(a11),x25012))), % 117.16/117.17 inference(scs_inference,[],[2472,2497,324,51])). % 117.16/117.17 cnf(2512,plain, % 117.16/117.17 (~E(f13(a2,a2),f13(f12(a10,a9),f12(a15,a9)))), % 117.16/117.17 inference(scs_inference,[],[49,2472,2497,2436,2438,2477,324,51,52,50,2,68,56,22])). % 117.16/117.17 cnf(2534,plain, % 117.16/117.17 (~E(f12(f12(x25341,f1(a11)),x25342),f12(f12(x25343,a11),x25344))), % 117.16/117.17 inference(scs_inference,[],[2473,51])). % 117.16/117.17 cnf(2538,plain, % 117.16/117.17 (~E(f12(x25381,f12(x25382,f1(a11))),f12(x25383,f12(x25384,a11)))), % 117.16/117.17 inference(scs_inference,[],[2473,81,51,52,50])). % 117.16/117.17 cnf(2540,plain, % 117.16/117.17 (~E(f13(f12(a10,a9),f12(a15,a9)),f13(a2,a2))), % 117.16/117.17 inference(scs_inference,[],[2473,2512,81,51,52,50,2])). % 117.16/117.17 cnf(2543,plain, % 117.16/117.17 (P2(f12(a15,a15),a3)), % 117.16/117.17 inference(scs_inference,[],[2473,2512,81,51,52,50,2,68,56])). % 117.16/117.17 cnf(2562,plain, % 117.16/117.17 (~E(f12(f13(f12(a10,a9),f12(a15,a9)),x25621),f12(f13(a2,a2),x25622))), % 117.16/117.17 inference(scs_inference,[],[2540,51])). % 117.16/117.17 cnf(2564,plain, % 117.16/117.17 (~E(f12(x25641,f13(f12(a10,a9),f12(a15,a9))),f12(x25642,f13(a2,a2)))), % 117.16/117.17 inference(scs_inference,[],[2540,51,50])). % 117.16/117.17 cnf(2568,plain, % 117.16/117.17 (~E(f12(f1(a11),x25681),f12(a11,x25682))), % 117.16/117.17 inference(scs_inference,[],[2543,2540,2501,51,50,52,2])). % 117.16/117.17 cnf(2569,plain, % 117.16/117.17 (P2(f12(f12(a15,a15),f12(a15,a15)),a3)), % 117.16/117.17 inference(scs_inference,[],[2543,2540,2501,51,50,52,2,56])). % 117.16/117.17 cnf(2589,plain, % 117.16/117.17 (~E(f12(x25891,f12(a11,x25892)),f12(x25893,f12(f1(a11),x25894)))), % 117.16/117.17 inference(scs_inference,[],[2568,2,50])). % 117.16/117.17 cnf(2596,plain, % 117.16/117.17 (~E(f12(f13(a2,a2),x25961),f12(f13(f12(a10,a9),f12(a15,a9)),x25962))), % 117.16/117.17 inference(scs_inference,[],[2569,2562,51,52,50,2])). % 117.16/117.17 cnf(2622,plain, % 117.16/117.17 (~E(f12(x26221,f12(x26222,f13(f12(a10,a9),f12(a15,a9)))),f12(x26223,f12(x26224,f13(a2,a2))))), % 117.16/117.17 inference(scs_inference,[],[2564,51,50])). % 117.16/117.17 cnf(2624,plain, % 117.16/117.17 (P2(f13(a8,a8),f1(a11))), % 117.16/117.17 inference(scs_inference,[],[2564,38,51,50,52])). % 117.16/117.17 cnf(2627,plain, % 117.16/117.17 (P2(f12(a8,a8),a3)), % 117.16/117.17 inference(scs_inference,[],[2564,38,51,50,52,2,56])). % 117.16/117.17 cnf(2629,plain, % 117.16/117.17 (P2(f13(f12(f12(a2,a8),a8),a8),a11)), % 117.16/117.17 inference(scs_inference,[],[2564,38,51,50,52,2,56,68])). % 117.16/117.17 cnf(2648,plain, % 117.16/117.17 (~E(f12(f12(f12(x26481,f1(a11)),x26482),x26483),f12(f12(f12(x26484,a11),x26485),x26486))), % 117.16/117.17 inference(scs_inference,[],[2534,51])). % 117.16/117.17 cnf(2652,plain, % 117.16/117.17 (~E(f12(x26521,f12(f12(x26522,f1(a11)),x26523)),f12(x26524,f12(f12(x26525,a11),x26526)))), % 117.16/117.17 inference(scs_inference,[],[2627,2534,51,52,50])). % 117.16/117.17 cnf(2657,plain, % 117.16/117.17 (P2(f12(f12(a8,a8),f12(a8,a8)),a3)), % 117.16/117.17 inference(scs_inference,[],[2627,2534,51,52,50,2,68,56])). % 117.16/117.17 cnf(2687,plain, % 117.16/117.17 (~E(f13(a8,a8),f13(f12(a10,a9),f12(a15,a9)))), % 117.16/117.17 inference(scs_inference,[],[49,2624,2657,2395,2596,2589,51,50,52,2,56,68,22])). % 117.16/117.17 cnf(2705,plain, % 117.16/117.17 (~E(f12(f13(a8,a8),x27051),f12(f13(f12(a10,a9),f12(a15,a9)),x27052))), % 117.16/117.17 inference(scs_inference,[],[2687,51])). % 117.16/117.17 cnf(2707,plain, % 117.16/117.17 (~E(f12(x27071,f13(a8,a8)),f12(x27072,f13(f12(a10,a9),f12(a15,a9))))), % 117.16/117.17 inference(scs_inference,[],[2687,51,50])). % 117.16/117.17 cnf(2709,plain, % 117.16/117.17 (P2(f13(a10,a10),f1(a11))), % 117.16/117.17 inference(scs_inference,[],[2687,40,51,50,52])). % 117.16/117.17 cnf(2791,plain, % 117.16/117.17 (P2(f13(a9,a9),f1(a11))), % 117.16/117.17 inference(scs_inference,[],[2421,2705,39,51,50,52])). % 117.16/117.17 cnf(2794,plain, % 117.16/117.17 (P2(f12(a9,a9),a3)), % 117.16/117.17 inference(scs_inference,[],[2421,2705,2622,39,51,50,52,2,56])). % 117.16/117.17 cnf(2822,plain, % 117.16/117.17 (P2(f12(f12(a9,a9),f12(a9,a9)),a3)), % 117.16/117.17 inference(scs_inference,[],[2794,2707,2648,51,50,52,2,56])). % 117.16/117.17 cnf(2840,plain, % 117.16/117.17 (~E(f12(a14,x28401),f12(a2,x28402))), % 117.16/117.17 inference(scs_inference,[],[140,51])). % 117.16/117.17 cnf(2842,plain, % 117.16/117.17 (~E(f12(x28421,f12(a14,x28422)),f12(x28423,f12(a10,x28424)))), % 117.16/117.17 inference(scs_inference,[],[140,1608,51,50])). % 117.16/117.17 cnf(2851,plain, % 117.16/117.17 (~E(f13(a9,a9),f13(f12(a10,a9),f12(a15,a9)))), % 117.16/117.17 inference(scs_inference,[],[49,2791,2822,2652,140,1608,51,50,52,2,56,68,22])). % 117.16/117.17 cnf(2869,plain, % 117.16/117.17 (~E(f12(f12(a14,x28691),x28692),f12(f12(a2,x28693),x28694))), % 117.16/117.17 inference(scs_inference,[],[2840,51])). % 117.16/117.17 cnf(2873,plain, % 117.16/117.17 (~E(f13(f12(a10,a9),f12(a15,a9)),f13(a9,a9))), % 117.16/117.17 inference(scs_inference,[],[2840,2851,51,50,2])). % 117.16/117.17 cnf(2895,plain, % 117.16/117.17 (~E(f12(x28951,f13(f12(a10,a9),f12(a15,a9))),f12(x28952,f13(a9,a9)))), % 117.16/117.17 inference(scs_inference,[],[2873,51,50])). % 117.16/117.17 cnf(2897,plain, % 117.16/117.17 (~E(f12(x28971,f12(a10,x28972)),f12(x28973,f12(a14,x28974)))), % 117.16/117.17 inference(scs_inference,[],[2873,2842,51,50,2])). % 117.16/117.17 cnf(2951,plain, % 117.16/117.17 (P2(f13(f12(f12(a2,a10),a10),a10),f1(a11))), % 117.16/117.17 inference(scs_inference,[],[2897,2895,2709,40,51,50,2,69])). % 117.16/117.17 cnf(3558,plain, % 117.16/117.17 (~E(f12(x35581,f12(f12(x35582,x35583),x35584)),f12(x35585,f12(a2,x35586)))), % 117.16/117.17 inference(scs_inference,[],[2164,51,50])). % 117.16/117.17 cnf(4977,plain, % 117.16/117.17 (~E(f12(x49771,f12(f12(x49772,x49773),x49774)),f12(x49775,f12(a2,x49776)))), % 117.16/117.17 inference(rename_variables,[],[3558])). % 117.16/117.17 cnf(4997,plain, % 117.16/117.17 (~P2(f12(a15,a9),a3)), % 117.16/117.17 inference(scs_inference,[],[41,39,2442,86,47,2165,83,2629,2869,3558,4977,2538,2452,2951,76,62,66,67,324,238,22,71,74,52])). % 117.16/117.17 cnf(5011,plain, % 117.16/117.17 (~P2(f12(x50111,f12(f12(a15,a9),x50112)),a3)), % 117.16/117.17 inference(scs_inference,[],[41,39,2442,86,47,2165,83,2629,2869,3558,4977,2538,2452,2951,76,62,66,67,324,238,22,71,74,52,1531,1558,199,58,59,60,61,210])). % 117.16/117.17 cnf(5031,plain, % 117.16/117.17 (~E(f12(x50311,f12(x50312,f1(a11))),f12(x50313,f12(x50314,a11)))), % 117.16/117.17 inference(rename_variables,[],[2538])). % 117.16/117.17 cnf(5051,plain, % 117.16/117.17 ($false), % 117.16/117.17 inference(scs_inference,[],[39,81,610,643,2538,5031,4997,5011,76,62,66,67,1531,1558,59,60,58,61,210,56]), % 117.16/117.17 ['proof']). % 117.16/117.17 % SZS output end Proof % 117.16/117.17 % Total time :116.500000s %------------------------------------------------------------------------------