%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL089-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 : n012.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:06 EDT 2024 % Result : Unsatisfiable 116.92s 117.00s % Output : CNFRefutation 116.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : COL089-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.12/0.33 % Computer : n012.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 : Tue Jun 18 15:52:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.56 start to proof:theBenchmark % 116.91/116.98 %------------------------------------------- % 116.91/116.98 % File :CSE---1.7 % 116.91/116.98 % Problem :theBenchmark % 116.91/116.98 % Transform :cnf % 116.91/116.98 % Format :tptp:raw % 116.91/116.98 % Command :java -jar mcs_scs.jar %d %s % 116.91/116.98 % 116.91/116.98 % Result :Theorem 116.300000s % 116.91/116.98 % Output :CNFRefutation 116.300000s % 116.91/116.98 %------------------------------------------- % 116.91/116.99 %-------------------------------------------------------------------------- % 116.91/116.99 % File : COL089-1 : TPTP v8.2.0. Released v2.7.0. % 116.91/116.99 % Domain : Combinatory Logic % 116.91/116.99 % Problem : ap_reduce2_2c1 % 116.91/116.99 % Version : Reduced > Especial. % 116.91/116.99 % English : % 116.91/116.99 % 116.91/116.99 % Refs : [Men03] Meng (2003), Email to G. Sutcliffe % 116.91/116.99 % Source : [Men03] % 116.91/116.99 % Names : % 116.91/116.99 % 116.91/116.99 % Status : Unsatisfiable % 116.91/116.99 % 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.20 v6.1.0, 0.21 v6.0.0, 0.30 v5.5.0, 0.55 v5.3.0, 0.61 v5.2.0, 0.50 v5.1.0, 0.59 v5.0.0, 0.50 v4.1.0, 0.62 v4.0.1, 0.55 v4.0.0, 0.45 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 % 116.91/116.99 % Syntax : Number of clauses : 44 ( 14 unt; 1 nHn; 43 RR) % 116.91/116.99 % Number of literals : 93 ( 15 equ; 52 neg) % 116.91/116.99 % Maximal clause size : 5 ( 2 avg) % 116.91/116.99 % Maximal term depth : 5 ( 1 avg) % 116.91/116.99 % Number of predicates : 7 ( 6 usr; 0 prp; 1-3 aty) % 116.91/116.99 % Number of functors : 15 ( 15 usr; 8 con; 0-3 aty) % 116.91/116.99 % Number of variables : 97 ( 25 sgn) % 116.91/116.99 % SPC : CNF_UNS_RFO_SEQ_NHN % 116.91/116.99 % 116.91/116.99 % Comments : Problem coming out of an Isabelle proof. % 116.91/116.99 %-------------------------------------------------------------------------- % 116.91/116.99 %----axioms from CombZF.thy. % 116.91/116.99 %----free algebra for K, S, comb_app(P,Q). % 116.91/116.99 cnf(k_s,axiom, % 116.91/116.99 combK != combS ). % 116.91/116.99 % 116.91/116.99 cnf(k_app,axiom, % 116.91/116.99 combK != comb_app(P,Q) ). % 116.91/116.99 % 116.91/116.99 cnf(s_app,axiom, % 116.91/116.99 combS != comb_app(P,Q) ). % 116.91/116.99 % 116.91/116.99 cnf(app_app1,axiom, % 116.91/116.99 ( comb_app(P1,Q1) != comb_app(P2,Q2) % 116.91/116.99 | P1 = P2 ) ). % 116.91/116.99 % 116.91/116.99 cnf(app_app2,axiom, % 116.91/116.99 ( comb_app(P1,Q1) != comb_app(P2,Q2) % 116.91/116.99 | Q1 = Q2 ) ). % 116.91/116.99 % 116.91/116.99 cnf(app_app3,axiom, % 116.91/116.99 ( P1 != P2 % 116.91/116.99 | Q1 != Q2 % 116.91/116.99 | comb_app(P1,Q1) = comb_app(P2,Q2) ) ). % 116.91/116.99 % 116.91/116.99 %----add in Ap_E. % 116.91/116.99 cnf(ap_E1,axiom, % 116.91/116.99 ( ~ member(comb_app(P,Q),comb) % 116.91/116.99 | member(P,comb) ) ). % 116.92/116.99 % 116.92/116.99 cnf(ap_E2,axiom, % 116.92/116.99 ( ~ member(comb_app(P,Q),comb) % 116.92/116.99 | member(Q,comb) ) ). % 116.92/116.99 % 116.92/116.99 %----add in comb.intros(three of them). % 116.92/116.99 cnf(comb_intros1,axiom, % 116.92/116.99 member(combK,comb) ). % 116.92/116.99 % 116.92/116.99 cnf(comb_intros2,axiom, % 116.92/116.99 member(combS,comb) ). % 116.92/116.99 % 116.92/116.99 cnf(comb_intros3,axiom, % 116.92/116.99 ( ~ member(P,comb) % 116.92/116.99 | ~ member(Q,comb) % 116.92/116.99 | member(comb_app(P,Q),comb) ) ). % 116.92/116.99 % 116.92/116.99 %----add in reduction_refl [intro!]: % 116.92/116.99 cnf(reduction_refl,axiom, % 116.92/116.99 ( ~ member(A,comb) % 116.92/116.99 | member(pair(A,A),rtrancl(contract)) ) ). % 116.92/116.99 % 116.92/116.99 %----add in contract.K % 116.92/116.99 cnf(contract_K,axiom, % 116.92/116.99 ( ~ member(P,comb) % 116.92/116.99 | ~ member(Q,comb) % 116.92/116.99 | member(pair(comb_app(comb_app(combK,P),Q),P),contract) ) ). % 116.92/116.99 % 116.92/116.99 %----add in contract.S % 116.92/116.99 cnf(contract_S,axiom, % 116.92/116.99 ( ~ member(P,comb) % 116.92/116.99 | ~ member(Q,comb) % 116.92/116.99 | ~ member(R,comb) % 116.92/116.99 | member(pair(comb_app(comb_app(comb_app(combS,P),Q),R),comb_app(comb_app(P,R),comb_app(Q,R))),contract) ) ). % 116.92/116.99 % 116.92/117.00 %----this manually rename the formula Ap_contractE % 116.92/117.00 cnf(ap_contractE1,axiom, % 116.92/117.00 ( ~ member(pair(comb_app(P,Q),R),contract) % 116.92/117.00 | ap_contractE_c1(P,Q,R) % 116.92/117.00 | ap_contractE_c2(P,Q,R) % 116.92/117.00 | ap_contractE_c3(P,Q,R) % 116.92/117.00 | ap_contractE_c4(P,Q,R) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE2,axiom, % 116.92/117.00 ( ~ ap_contractE_c1(P,Q,R) % 116.92/117.00 | member(R,comb) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE3,axiom, % 116.92/117.00 ( ~ ap_contractE_c1(P,Q,R) % 116.92/117.00 | member(Q,comb) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE4,axiom, % 116.92/117.00 ( ~ ap_contractE_c1(P,Q,R) % 116.92/117.00 | P = comb_app(combK,R) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE5,axiom, % 116.92/117.00 ( ~ ap_contractE_c2(P,Q,R) % 116.92/117.00 | member(ap_contractE_sk1p(P,Q,R),comb) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE6,axiom, % 116.92/117.00 ( ~ ap_contractE_c2(P,Q,R) % 116.92/117.00 | member(ap_contractE_sk1q(P,Q,R),comb) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE7,axiom, % 116.92/117.00 ( ~ ap_contractE_c2(P,Q,R) % 116.92/117.00 | member(Q,comb) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE8,axiom, % 116.92/117.00 ( ~ ap_contractE_c2(P,Q,R) % 116.92/117.00 | R = comb_app(comb_app(ap_contractE_sk1p(P,Q,R),Q),comb_app(ap_contractE_sk1q(P,Q,R),Q)) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE9,axiom, % 116.92/117.00 ( ~ ap_contractE_c2(P,Q,R) % 116.92/117.00 | P = comb_app(comb_app(combS,ap_contractE_sk1p(P,Q,R)),ap_contractE_sk1q(P,Q,R)) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE10,axiom, % 116.92/117.00 ( ~ ap_contractE_c3(P,Q,R) % 116.92/117.00 | member(pair(P,ap_contractE_sk2q(P,Q,R)),contract) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE11,axiom, % 116.92/117.00 ( ~ ap_contractE_c3(P,Q,R) % 116.92/117.00 | member(Q,comb) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE12,axiom, % 116.92/117.00 ( ~ ap_contractE_c3(P,Q,R) % 116.92/117.00 | R = comb_app(ap_contractE_sk2q(P,Q,R),Q) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE13,axiom, % 116.92/117.00 ( ~ ap_contractE_c4(P,Q,R) % 116.92/117.00 | member(pair(Q,ap_contractE_sk3q(P,Q,R)),contract) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE14,axiom, % 116.92/117.00 ( ~ ap_contractE_c4(P,Q,R) % 116.92/117.00 | member(P,comb) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_contractE15,axiom, % 116.92/117.00 ( ~ ap_contractE_c4(P,Q,R) % 116.92/117.00 | R = comb_app(P,ap_contractE_sk3q(P,Q,R)) ) ). % 116.92/117.00 % 116.92/117.00 %----add in K_contractE[elim!]: % 116.92/117.00 cnf(k_contractE,axiom, % 116.92/117.00 ~ member(pair(combK,R),contract) ). % 116.92/117.00 % 116.92/117.00 %----add in S_contractE [elim!]: % 116.92/117.00 %----converted by tptp2X(Ap_contractE+cls_otter.tptp) % 116.92/117.00 cnf(s_contractE,axiom, % 116.92/117.00 ~ member(pair(combS,R),contract) ). % 116.92/117.00 % 116.92/117.00 %----local axioms % 116.92/117.00 %----axiom reduction_rls % 116.92/117.00 cnf(reduction_rls_1,axiom, % 116.92/117.00 ( ~ member(B,comb) % 116.92/117.00 | ~ member(Q3,comb) % 116.92/117.00 | ~ member(pair(B,C),rtrancl(contract)) % 116.92/117.00 | member(pair(comb_app(comb_app(combK,B),Q3),C),rtrancl(contract)) ) ). % 116.92/117.00 % 116.92/117.00 cnf(reduction_rls_2,axiom, % 116.92/117.00 ( ~ member(P3,comb) % 116.92/117.00 | ~ member(Q3,comb) % 116.92/117.00 | ~ member(R3,comb) % 116.92/117.00 | ~ member(pair(comb_app(comb_app(P3,R3),comb_app(Q3,R3)),C),rtrancl(contract)) % 116.92/117.00 | member(pair(comb_app(comb_app(comb_app(combS,P3),Q3),R3),C),rtrancl(contract)) ) ). % 116.92/117.00 % 116.92/117.00 cnf(reduction_rls_3,axiom, % 116.92/117.00 ( ~ member(pair(P3,Q3),contract) % 116.92/117.00 | ~ member(R3,comb) % 116.92/117.00 | ~ member(pair(comb_app(Q3,R3),C),rtrancl(contract)) % 116.92/117.00 | member(pair(comb_app(P3,R3),C),rtrancl(contract)) ) ). % 116.92/117.00 % 116.92/117.00 cnf(reduction_rls_4,axiom, % 116.92/117.00 ( ~ member(pair(P3,Q3),contract) % 116.92/117.00 | ~ member(R3,comb) % 116.92/117.00 | ~ member(pair(comb_app(R3,Q3),C),rtrancl(contract)) % 116.92/117.00 | member(pair(comb_app(R3,P3),C),rtrancl(contract)) ) ). % 116.92/117.00 % 116.92/117.00 %----local axioms. % 116.92/117.00 %----axoim reduction_rls(same as above) % 116.92/117.00 %----axiom trans_rtrancl % 116.92/117.00 cnf(trans_rtrancl,axiom, % 116.92/117.00 trans(rtrancl(R)) ). % 116.92/117.00 % 116.92/117.00 %----axiom transD % 116.92/117.00 cnf(transD,axiom, % 116.92/117.00 ( ~ trans(R) % 116.92/117.00 | ~ member(pair(A,B),R) % 116.92/117.00 | ~ member(pair(B,C),R) % 116.92/117.00 | member(pair(A,C),R) ) ). % 116.92/117.00 % 116.92/117.00 %----axiom contract_combD2 % 116.92/117.00 cnf(contract_combD2,axiom, % 116.92/117.00 ( ~ member(pair(A,B),contract) % 116.92/117.00 | member(B,comb) ) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_reduce2_2h1,hypothesis, % 116.92/117.00 member(r,comb) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_reduce2_2h2,hypothesis, % 116.92/117.00 member(p,comb) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_reduce2_2h3,hypothesis, % 116.92/117.00 member(pair(p,y),rtrancl(contract)) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_reduce2_2h4,hypothesis, % 116.92/117.00 member(pair(y,z),contract) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_reduce2_2h5,hypothesis, % 116.92/117.00 member(pair(comb_app(r,p),comb_app(r,y)),rtrancl(contract)) ). % 116.92/117.00 % 116.92/117.00 cnf(ap_reduce2_2c1,negated_conjecture, % 116.92/117.00 ~ member(pair(comb_app(r,p),comb_app(r,z)),rtrancl(contract)) ). % 116.92/117.00 % 116.92/117.00 %-------------------------------------------------------------------------- % 116.92/117.00 %------------------------------------------- % 116.92/117.00 % Proof found % 116.92/117.00 % SZS status Theorem for theBenchmark % 116.92/117.00 % SZS output start Proof % 116.92/117.00 %ClaNum:78(EqnAxiom:35) % 116.92/117.00 %VarNum:201(SingletonVarNum:93) % 116.92/117.00 %MaxLitNum:5 % 116.92/117.00 %MaxfuncDepth:4 % 116.92/117.00 %SharedTerms:25 % 116.92/117.00 %goalClause: 49 % 116.92/117.00 %singleGoalClaCount:1 % 116.92/117.00 [37]P2(a2,a3) % 116.92/117.00 [38]P2(a8,a3) % 116.92/117.00 [39]P2(a9,a3) % 116.92/117.00 [40]P2(a10,a3) % 116.92/117.00 [44]~E(a8,a2) % 116.92/117.00 [41]P2(f13(a14,a15),a11) % 116.92/117.00 [42]P2(f13(a10,a14),f1(a11)) % 116.92/117.00 [43]P2(f13(f12(a9,a10),f12(a9,a14)),f1(a11)) % 116.92/117.00 [49]~P2(f13(f12(a9,a10),f12(a9,a15)),f1(a11)) % 116.92/117.00 [36]P1(f1(x361)) % 116.92/117.00 [47]~P2(f13(a2,x471),a11) % 116.92/117.00 [48]~P2(f13(a8,x481),a11) % 116.92/117.00 [45]~E(f12(x451,x452),a2) % 116.92/117.00 [46]~E(f12(x461,x462),a8) % 116.92/117.00 [52]~P2(x521,a3)+P2(f13(x521,x521),f1(a11)) % 116.92/117.00 [53]P2(x531,a3)+~P2(f12(x532,x531),a3) % 116.92/117.00 [54]P2(x541,a3)+~P2(f13(x542,x541),a11) % 116.92/117.00 [55]P2(x551,a3)+~P2(f12(x551,x552),a3) % 116.92/117.00 [57]~P3(x572,x573,x571)+P2(x571,a3) % 116.92/117.00 [58]~P3(x582,x581,x583)+P2(x581,a3) % 116.92/117.00 [59]~P4(x592,x591,x593)+P2(x591,a3) % 116.92/117.00 [60]~P5(x602,x601,x603)+P2(x601,a3) % 116.92/117.00 [61]~P6(x611,x612,x613)+P2(x611,a3) % 116.92/117.00 [62]~P3(x621,x623,x622)+E(x621,f12(a2,x622)) % 116.92/117.00 [64]~P4(x641,x642,x643)+P2(f4(x641,x642,x643),a3) % 116.92/117.00 [65]~P4(x651,x652,x653)+P2(f5(x651,x652,x653),a3) % 116.92/117.00 [66]~P6(x661,x662,x663)+E(f12(x661,f6(x661,x662,x663)),x663) % 116.92/117.00 [67]~P5(x671,x672,x673)+E(f12(f7(x671,x672,x673),x672),x673) % 116.92/117.00 [72]~P6(x722,x721,x723)+P2(f13(x721,f6(x722,x721,x723)),a11) % 116.92/117.00 [73]~P5(x731,x732,x733)+P2(f13(x731,f7(x731,x732,x733)),a11) % 116.92/117.00 [75]~P4(x751,x752,x753)+E(f12(f12(a8,f4(x751,x752,x753)),f5(x751,x752,x753)),x751) % 116.92/117.00 [76]~P4(x761,x762,x763)+E(f12(f12(f4(x761,x762,x763),x762),f12(f5(x761,x762,x763),x762)),x763) % 116.92/117.00 [50]E(x501,x502)+~E(f12(x503,x501),f12(x504,x502)) % 116.92/117.00 [51]E(x511,x512)+~E(f12(x511,x513),f12(x512,x514)) % 116.92/117.00 [56]~P2(x562,a3)+~P2(x561,a3)+P2(f12(x561,x562),a3) % 116.92/117.00 [68]~P2(x682,a3)+~P2(x681,a3)+P2(f13(f12(f12(a2,x681),x682),x681),a11) % 116.92/117.00 [69]~P2(x692,a3)+~P2(x691,a3)+~P2(f13(x691,x693),f1(a11))+P2(f13(f12(f12(a2,x691),x692),x693),f1(a11)) % 116.92/117.00 [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) % 116.92/117.00 [63]~P1(x633)+~P2(f13(x631,x634),x633)+P2(f13(x631,x632),x633)+~P2(f13(x634,x632),x633) % 116.92/117.00 [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)) % 116.92/117.00 [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)) % 116.92/117.00 [74]P4(x741,x742,x743)+P5(x741,x742,x743)+P6(x741,x742,x743)+P3(x741,x742,x743)+~P2(f13(f12(x741,x742),x743),a11) % 116.92/117.00 [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)) % 116.92/117.00 %EqnAxiom % 116.92/117.00 [1]E(x11,x11) % 116.92/117.00 [2]E(x22,x21)+~E(x21,x22) % 116.92/117.00 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.92/117.00 [4]~E(x41,x42)+E(f1(x41),f1(x42)) % 116.92/117.00 [5]~E(x51,x52)+E(f13(x51,x53),f13(x52,x53)) % 116.92/117.00 [6]~E(x61,x62)+E(f13(x63,x61),f13(x63,x62)) % 116.92/117.00 [7]~E(x71,x72)+E(f12(x71,x73),f12(x72,x73)) % 116.92/117.00 [8]~E(x81,x82)+E(f12(x83,x81),f12(x83,x82)) % 116.92/117.00 [9]~E(x91,x92)+E(f6(x91,x93,x94),f6(x92,x93,x94)) % 116.92/117.00 [10]~E(x101,x102)+E(f6(x103,x101,x104),f6(x103,x102,x104)) % 116.92/117.00 [11]~E(x111,x112)+E(f6(x113,x114,x111),f6(x113,x114,x112)) % 116.92/117.00 [12]~E(x121,x122)+E(f7(x121,x123,x124),f7(x122,x123,x124)) % 116.92/117.00 [13]~E(x131,x132)+E(f7(x133,x131,x134),f7(x133,x132,x134)) % 116.92/117.00 [14]~E(x141,x142)+E(f7(x143,x144,x141),f7(x143,x144,x142)) % 116.92/117.00 [15]~E(x151,x152)+E(f4(x151,x153,x154),f4(x152,x153,x154)) % 116.92/117.00 [16]~E(x161,x162)+E(f4(x163,x161,x164),f4(x163,x162,x164)) % 116.92/117.00 [17]~E(x171,x172)+E(f4(x173,x174,x171),f4(x173,x174,x172)) % 116.92/117.00 [18]~E(x181,x182)+E(f5(x181,x183,x184),f5(x182,x183,x184)) % 116.92/117.00 [19]~E(x191,x192)+E(f5(x193,x191,x194),f5(x193,x192,x194)) % 116.92/117.00 [20]~E(x201,x202)+E(f5(x203,x204,x201),f5(x203,x204,x202)) % 116.92/117.00 [21]~P1(x211)+P1(x212)+~E(x211,x212) % 116.92/117.00 [22]P2(x222,x223)+~E(x221,x222)+~P2(x221,x223) % 116.92/117.00 [23]P2(x233,x232)+~E(x231,x232)+~P2(x233,x231) % 116.92/117.00 [24]P4(x242,x243,x244)+~E(x241,x242)+~P4(x241,x243,x244) % 116.92/117.00 [25]P4(x253,x252,x254)+~E(x251,x252)+~P4(x253,x251,x254) % 116.92/117.00 [26]P4(x263,x264,x262)+~E(x261,x262)+~P4(x263,x264,x261) % 116.92/117.00 [27]P3(x272,x273,x274)+~E(x271,x272)+~P3(x271,x273,x274) % 116.92/117.00 [28]P3(x283,x282,x284)+~E(x281,x282)+~P3(x283,x281,x284) % 116.92/117.00 [29]P3(x293,x294,x292)+~E(x291,x292)+~P3(x293,x294,x291) % 116.92/117.00 [30]P6(x302,x303,x304)+~E(x301,x302)+~P6(x301,x303,x304) % 116.92/117.00 [31]P6(x313,x312,x314)+~E(x311,x312)+~P6(x313,x311,x314) % 116.92/117.00 [32]P6(x323,x324,x322)+~E(x321,x322)+~P6(x323,x324,x321) % 116.92/117.00 [33]P5(x332,x333,x334)+~E(x331,x332)+~P5(x331,x333,x334) % 116.92/117.00 [34]P5(x343,x342,x344)+~E(x341,x342)+~P5(x343,x341,x344) % 116.92/117.00 [35]P5(x353,x354,x352)+~E(x351,x352)+~P5(x353,x354,x351) % 116.92/117.00 % 116.92/117.00 %------------------------------------------- % 116.92/117.01 cnf(81,plain, % 116.92/117.01 (P2(a15,a3)), % 116.92/117.01 inference(scs_inference,[],[41,54])). % 116.92/117.01 cnf(84,plain, % 116.92/117.01 (~E(f12(x841,x842),a2)), % 116.92/117.01 inference(rename_variables,[],[45])). % 116.92/117.01 cnf(87,plain, % 116.92/117.01 (~E(f12(x871,x872),a2)), % 116.92/117.01 inference(rename_variables,[],[45])). % 116.92/117.01 cnf(89,plain, % 116.92/117.01 (~P6(x891,a2,x892)), % 116.92/117.01 inference(scs_inference,[],[47,41,45,84,54,66,67,72])). % 116.92/117.01 cnf(90,plain, % 116.92/117.01 (~P2(f13(a2,x901),a11)), % 116.92/117.01 inference(rename_variables,[],[47])). % 116.92/117.01 cnf(92,plain, % 116.92/117.01 (~P5(a2,x921,x922)), % 116.92/117.01 inference(scs_inference,[],[47,90,41,45,84,54,66,67,72,73])). % 116.92/117.01 cnf(96,plain, % 116.92/117.01 (~E(f12(x961,x962),a2)), % 116.92/117.01 inference(rename_variables,[],[45])). % 116.92/117.01 cnf(98,plain, % 116.92/117.01 (~P4(x981,x982,a2)), % 116.92/117.01 inference(scs_inference,[],[47,90,41,45,84,87,96,54,66,67,72,73,75,76])). % 116.92/117.01 cnf(102,plain, % 116.92/117.01 (P2(a2,x1021)+~E(a3,x1021)), % 116.92/117.01 inference(scs_inference,[],[49,37,42,47,90,41,45,84,87,96,54,66,67,72,73,75,76,22,23])). % 116.92/117.01 cnf(103,plain, % 116.92/117.01 (~P2(f13(x1031,a10),f1(a11))+P2(f13(x1031,a14),f1(a11))), % 116.92/117.01 inference(scs_inference,[],[49,36,37,42,47,90,41,45,84,87,96,54,66,67,72,73,75,76,22,23,63])). % 116.92/117.01 cnf(114,plain, % 116.92/117.01 (~P2(f13(a8,x1141),a11)), % 116.92/117.01 inference(rename_variables,[],[48])). % 116.92/117.01 cnf(116,plain, % 116.92/117.01 (~P6(x1161,a8,x1162)), % 116.92/117.01 inference(scs_inference,[],[48,114,73,72])). % 116.92/117.01 cnf(120,plain, % 116.92/117.01 (~E(f12(x1201,x1202),a8)), % 116.92/117.01 inference(rename_variables,[],[46])). % 116.92/117.01 cnf(123,plain, % 116.92/117.01 (~E(f12(x1231,x1232),a8)), % 116.92/117.01 inference(rename_variables,[],[46])). % 116.92/117.01 cnf(126,plain, % 116.92/117.01 (~E(f12(x1261,x1262),a8)), % 116.92/117.01 inference(rename_variables,[],[46])). % 116.92/117.01 cnf(134,plain, % 116.92/117.01 (P2(a8,x1341)+~E(a3,x1341)), % 116.92/117.01 inference(scs_inference,[],[49,38,48,114,43,46,120,123,126,73,72,76,66,67,75,22,6,8,23])). % 116.92/117.01 cnf(139,plain, % 116.92/117.01 (~E(f13(a14,a15),f13(a2,x1391))), % 116.92/117.01 inference(scs_inference,[],[41,47,22])). % 116.92/117.01 cnf(140,plain, % 116.92/117.01 (~E(a14,a2)), % 116.92/117.01 inference(scs_inference,[],[41,47,22,5])). % 116.92/117.01 cnf(148,plain, % 116.92/117.01 (~E(a14,a8)), % 116.92/117.01 inference(scs_inference,[],[48,41,22,5])). % 116.92/117.01 cnf(149,plain, % 116.92/117.01 (P2(a15,x1491)+~E(a3,x1491)), % 116.92/117.01 inference(scs_inference,[],[48,41,81,22,5,23])). % 116.92/117.01 cnf(189,plain, % 116.92/117.01 (~E(a9,f12(x1891,x1892))+P2(x1892,a3)), % 116.92/117.01 inference(scs_inference,[],[39,22,53])). % 116.92/117.01 cnf(190,plain, % 116.92/117.01 (~E(a9,f12(x1901,x1902))+P2(x1901,a3)), % 116.92/117.01 inference(scs_inference,[],[39,22,53,55])). % 116.92/117.01 cnf(202,plain, % 116.92/117.01 (~E(a10,f12(x2021,x2022))+P2(x2022,a3)), % 116.92/117.01 inference(scs_inference,[],[40,22,53])). % 116.92/117.01 cnf(203,plain, % 116.92/117.01 (~E(a10,f12(x2031,x2032))+P2(x2031,a3)), % 116.92/117.01 inference(scs_inference,[],[40,22,53,55])). % 116.92/117.01 cnf(208,plain, % 116.92/117.01 (~E(a2,a14)), % 116.92/117.01 inference(scs_inference,[],[139,2,5])). % 116.97/117.01 cnf(209,plain, % 116.97/117.01 (~P3(x2091,x2092,x2093)+P2(f13(x2093,x2093),f1(a11))), % 116.97/117.01 inference(scs_inference,[],[57,52])). % 116.97/117.01 cnf(220,plain, % 116.97/117.01 (~E(a9,f12(x2201,f12(x2202,x2203)))+P2(x2202,a3)), % 116.97/117.01 inference(scs_inference,[],[189,55])). % 116.97/117.01 cnf(221,plain, % 116.97/117.01 (~E(a9,f12(f12(x2211,x2212),x2213))+P2(x2212,a3)), % 116.97/117.01 inference(scs_inference,[],[190,53])). % 116.97/117.01 cnf(222,plain, % 116.97/117.01 (~E(a10,f12(x2221,x2222))+P2(f13(x2222,x2222),f1(a11))), % 116.97/117.01 inference(scs_inference,[],[202,52])). % 116.97/117.01 cnf(223,plain, % 116.97/117.01 (~E(a10,f12(f12(x2231,x2232),x2233))+P2(x2232,a3)), % 116.97/117.01 inference(scs_inference,[],[203,53])). % 116.97/117.01 cnf(224,plain, % 116.97/117.01 (E(a2,f12(a2,a2))+~P2(f13(f12(a2,a2),a2),a11)), % 116.97/117.01 inference(scs_inference,[],[92,89,98,62,74])). % 116.97/117.01 cnf(235,plain, % 116.97/117.01 (~E(a9,f12(x2351,f12(x2352,x2353)))+P2(f13(x2352,x2352),f1(a11))), % 116.97/117.01 inference(scs_inference,[],[220,52])). % 116.97/117.01 cnf(236,plain, % 116.97/117.01 (~E(a9,f12(f12(x2361,f12(x2362,x2363)),x2364))+P2(x2362,a3)), % 116.97/117.02 inference(scs_inference,[],[221,55])). % 116.97/117.02 cnf(237,plain, % 116.97/117.02 (~E(a10,f12(f12(x2371,x2372),x2373))+P2(f13(x2372,x2372),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[223,52])). % 116.97/117.02 cnf(255,plain, % 116.97/117.02 (~E(f13(x2551,a14),f13(f12(a9,a10),f12(a9,a15)))+~P2(f13(x2551,a10),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[49,103,22])). % 116.97/117.02 cnf(256,plain, % 116.97/117.02 (~P2(f13(f12(a2,a2),a2),a11)), % 116.97/117.02 inference(scs_inference,[],[45,224,2])). % 116.97/117.02 cnf(258,plain, % 116.97/117.02 (~E(f13(a14,a15),f13(f12(a2,a2),a2))), % 116.97/117.02 inference(scs_inference,[],[256,41,22])). % 116.97/117.02 cnf(259,plain, % 116.97/117.02 (~E(a9,f12(f12(x2591,f12(f12(x2592,x2593),x2594)),x2595))+P2(x2593,a3)), % 116.97/117.02 inference(scs_inference,[],[236,53])). % 116.97/117.02 cnf(279,plain, % 116.97/117.02 (~E(a9,f12(f12(x2791,f12(f12(x2792,x2793),x2794)),x2795))+P2(f13(x2793,x2793),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[259,52])). % 116.97/117.02 cnf(364,plain, % 116.97/117.02 (P2(f12(a8,a15),a3)), % 116.97/117.02 inference(scs_inference,[],[38,41,56,54])). % 116.97/117.02 cnf(372,plain, % 116.97/117.02 (P2(x3721,a3)+~E(f12(a8,a15),x3721)), % 116.97/117.02 inference(scs_inference,[],[364,22])). % 116.97/117.02 cnf(373,plain, % 116.97/117.02 (~E(f12(a8,a15),f12(x3731,x3732))+P2(x3732,a3)), % 116.97/117.02 inference(scs_inference,[],[364,22,53])). % 116.97/117.02 cnf(442,plain, % 116.97/117.02 (~E(f12(a8,x4421),f12(a14,x4422))), % 116.97/117.02 inference(scs_inference,[],[148,2,51])). % 116.97/117.02 cnf(451,plain, % 116.97/117.02 (~E(f12(x4511,f13(f12(a2,a2),a2)),f12(x4512,f13(a14,a15)))), % 116.97/117.02 inference(scs_inference,[],[258,2,50])). % 116.97/117.02 cnf(453,plain, % 116.97/117.02 (~E(f12(x4531,f13(f12(a2,a2),a2)),f12(x4532,f13(a14,a15)))), % 116.97/117.02 inference(rename_variables,[],[451])). % 116.97/117.02 cnf(456,plain, % 116.97/117.02 (~E(f12(x4561,f13(f12(a2,a2),a2)),f12(x4562,f13(a14,a15)))), % 116.97/117.02 inference(rename_variables,[],[451])). % 116.97/117.02 cnf(458,plain, % 116.97/117.02 (~E(f13(f12(a2,a2),a2),f13(a14,a15))), % 116.97/117.02 inference(scs_inference,[],[451,453,456,62,67,8])). % 116.97/117.02 cnf(579,plain, % 116.97/117.02 (~E(f12(f13(a14,a15),x5791),f12(f13(f12(a2,a2),a2),x5792))), % 116.97/117.02 inference(scs_inference,[],[458,2,51])). % 116.97/117.02 cnf(860,plain, % 116.97/117.02 (~E(f12(a2,x8601),f12(a8,x8602))), % 116.97/117.02 inference(scs_inference,[],[44,2,51])). % 116.97/117.02 cnf(866,plain, % 116.97/117.02 (~E(f12(x8661,a2),f12(x8662,a8))), % 116.97/117.02 inference(scs_inference,[],[44,2,50])). % 116.97/117.02 cnf(881,plain, % 116.97/117.02 (~E(f12(x8811,a8),f12(x8812,f12(x8813,x8814)))), % 116.97/117.02 inference(scs_inference,[],[46,2,50])). % 116.97/117.02 cnf(883,plain, % 116.97/117.02 (~E(f12(x8831,a8),f12(x8832,f12(x8833,x8834)))), % 116.97/117.02 inference(rename_variables,[],[881])). % 116.97/117.02 cnf(884,plain, % 116.97/117.02 (~P5(x8841,a8,f12(x8842,f12(x8843,x8844)))), % 116.97/117.02 inference(scs_inference,[],[881,883,8,67])). % 116.97/117.02 cnf(885,plain, % 116.97/117.02 (~E(f12(x8851,a8),f12(x8852,f12(x8853,x8854)))), % 116.97/117.02 inference(rename_variables,[],[881])). % 116.97/117.02 cnf(887,plain, % 116.97/117.02 (~P3(f12(x8871,a8),x8872,f12(x8873,x8874))), % 116.97/117.02 inference(scs_inference,[],[881,883,885,8,67,62])). % 116.97/117.02 cnf(890,plain, % 116.97/117.02 (~P4(x8901,x8902,f12(x8903,a8))), % 116.97/117.02 inference(scs_inference,[],[881,2,76])). % 116.97/117.02 cnf(894,plain, % 116.97/117.02 (~E(x8941,a15)+P2(x8941,a3)), % 116.97/117.02 inference(scs_inference,[],[81,2,22])). % 116.97/117.02 cnf(1117,plain, % 116.97/117.02 (P2(f13(a2,a2),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[102,52])). % 116.97/117.02 cnf(1118,plain, % 116.97/117.02 (~E(f1(a11),a11)), % 116.97/117.02 inference(scs_inference,[],[47,1117,23])). % 116.97/117.02 cnf(1123,plain, % 116.97/117.02 (P2(f12(a2,a2),a3)), % 116.97/117.02 inference(scs_inference,[],[102,56])). % 116.97/117.02 cnf(1134,plain, % 116.97/117.02 (P2(x11341,a3)+~E(f12(a2,a2),x11341)), % 116.97/117.02 inference(scs_inference,[],[1123,22])). % 116.97/117.02 cnf(1183,plain, % 116.97/117.02 (P2(f13(f12(f12(f12(a8,a2),a2),a2),f12(f12(a2,a2),f12(a2,a2))),a11)), % 116.97/117.02 inference(scs_inference,[],[102,77])). % 116.97/117.02 cnf(1184,plain, % 116.97/117.02 (P2(f12(f12(a2,a2),f12(a2,a2)),a3)), % 116.97/117.02 inference(scs_inference,[],[1183,54])). % 116.97/117.02 cnf(1200,plain, % 116.97/117.02 (P2(x12001,a3)+~E(f12(f12(a2,a2),f12(a2,a2)),x12001)), % 116.97/117.02 inference(scs_inference,[],[1184,22])). % 116.97/117.02 cnf(1201,plain, % 116.97/117.02 (~E(f12(f12(a2,a2),f12(a2,a2)),f12(x12011,x12012))+P2(x12011,a3)), % 116.97/117.02 inference(scs_inference,[],[1184,22,55])). % 116.97/117.02 cnf(1202,plain, % 116.97/117.02 (~E(f12(f12(a2,a2),f12(a2,a2)),f12(x12021,x12022))+P2(x12022,a3)), % 116.97/117.02 inference(scs_inference,[],[1184,22,55,53])). % 116.97/117.02 cnf(2160,plain, % 116.97/117.02 (P2(f13(a8,a8),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[134,52])). % 116.97/117.02 cnf(2161,plain, % 116.97/117.02 (~E(f13(a8,a8),f13(f12(a9,a10),f12(a9,a15)))), % 116.97/117.02 inference(scs_inference,[],[49,2160,22])). % 116.97/117.02 cnf(2225,plain, % 116.97/117.02 (P2(f12(a8,a8),a3)), % 116.97/117.02 inference(scs_inference,[],[134,56])). % 116.97/117.02 cnf(2237,plain, % 116.97/117.02 (P2(x22371,a3)+~E(f12(a8,a8),x22371)), % 116.97/117.02 inference(scs_inference,[],[2225,22])). % 116.97/117.02 cnf(2649,plain, % 116.97/117.02 (P2(f13(f12(f12(a2,a8),a8),a8),a11)), % 116.97/117.02 inference(scs_inference,[],[134,68])). % 116.97/117.02 cnf(2650,plain, % 116.97/117.02 (~E(f13(f12(f12(a2,a8),a8),a8),f13(a8,x26501))), % 116.97/117.02 inference(scs_inference,[],[48,2649,22])). % 116.97/117.02 cnf(2787,plain, % 116.97/117.02 (P2(f13(f12(f12(f12(a8,a8),a8),a8),f12(f12(a8,a8),f12(a8,a8))),a11)), % 116.97/117.02 inference(scs_inference,[],[134,77])). % 116.97/117.02 cnf(2788,plain, % 116.97/117.02 (P2(f12(f12(a8,a8),f12(a8,a8)),a3)), % 116.97/117.02 inference(scs_inference,[],[2787,54])). % 116.97/117.02 cnf(2791,plain, % 116.97/117.02 (P4(f12(f12(a8,a8),a8),a8,f12(f12(a8,a8),f12(a8,a8)))), % 116.97/117.02 inference(scs_inference,[],[47,887,2787,884,116,54,22,74])). % 116.97/117.02 cnf(2807,plain, % 116.97/117.02 (P2(x28071,a3)+~E(f12(f12(a8,a8),f12(a8,a8)),x28071)), % 116.97/117.02 inference(scs_inference,[],[2788,22])). % 116.97/117.02 cnf(2808,plain, % 116.97/117.02 (~E(f12(f12(a8,a8),f12(a8,a8)),f12(x28081,x28082))+P2(x28081,a3)), % 116.97/117.02 inference(scs_inference,[],[2788,22,55])). % 116.97/117.02 cnf(2809,plain, % 116.97/117.02 (~E(f12(f12(a8,a8),f12(a8,a8)),f12(x28091,x28092))+P2(x28092,a3)), % 116.97/117.02 inference(scs_inference,[],[2788,22,55,53])). % 116.97/117.02 cnf(3417,plain, % 116.97/117.02 (P2(f12(a15,a15),a3)), % 116.97/117.02 inference(scs_inference,[],[149,56])). % 116.97/117.02 cnf(3418,plain, % 116.97/117.02 (P2(x34181,a3)+~E(f12(a15,a15),x34181)), % 116.97/117.02 inference(scs_inference,[],[3417,22])). % 116.97/117.02 cnf(3962,plain, % 116.97/117.02 (P2(f13(f12(f12(f12(a8,a15),a15),a15),f12(f12(a15,a15),f12(a15,a15))),a11)), % 116.97/117.02 inference(scs_inference,[],[149,77])). % 116.97/117.02 cnf(3963,plain, % 116.97/117.02 (P2(f12(f12(a15,a15),f12(a15,a15)),a3)), % 116.97/117.02 inference(scs_inference,[],[3962,54])). % 116.97/117.02 cnf(4177,plain, % 116.97/117.02 (~E(a11,f1(a11))), % 116.97/117.02 inference(scs_inference,[],[1118,2])). % 116.97/117.02 cnf(4186,plain, % 116.97/117.02 (P2(f13(f12(f12(a15,a15),f12(a15,a15)),f12(f12(a15,a15),f12(a15,a15))),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[140,1118,2791,3963,2,50,51,64,65,52])). % 116.97/117.02 cnf(4196,plain, % 116.97/117.02 (~P2(f13(f12(a9,a14),f12(a9,a15)),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[49,140,1118,2791,2160,3963,3417,43,36,38,2,50,51,64,65,52,56,68,77,69,63])). % 116.97/117.02 cnf(4217,plain, % 116.97/117.02 (~E(f12(x42171,a2),f12(x42172,a14))), % 116.97/117.02 inference(scs_inference,[],[208,2225,52,50])). % 116.97/117.02 cnf(4219,plain, % 116.97/117.02 (~E(f12(a2,x42191),f12(a14,x42192))), % 116.97/117.02 inference(scs_inference,[],[208,2225,52,50,51])). % 116.97/117.02 cnf(4250,plain, % 116.97/117.02 (~E(f12(a11,x42501),f12(f1(a11),x42502))), % 116.97/117.02 inference(scs_inference,[],[4177,3417,52,50,51])). % 116.97/117.02 cnf(4253,plain, % 116.97/117.02 (P2(f13(f12(f12(a2,f12(a15,a15)),f12(a15,a15)),f12(a15,a15)),a11)), % 116.97/117.02 inference(scs_inference,[],[4177,2161,3417,52,50,51,2,68])). % 116.97/117.02 cnf(4334,plain, % 116.97/117.02 (P2(f12(a9,a9),a3)), % 116.97/117.02 inference(scs_inference,[],[4217,4250,2788,39,52,50,51,2,68,56])). % 116.97/117.02 cnf(4365,plain, % 116.97/117.02 (P2(f13(f12(f12(f12(a2,f12(a15,a15)),f12(a15,a15)),f12(a15,a15)),f12(f12(a15,a15),f12(a15,a15))),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[4219,4334,2650,4253,4186,890,2791,3417,52,50,51,2,26,56,68,71])). % 116.97/117.02 cnf(4551,plain, % 116.97/117.02 (P2(f13(a10,a10),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[40,52])). % 116.97/117.02 cnf(6538,plain, % 116.97/117.02 (~E(f12(f12(x65381,a2),x65382),f12(f12(x65383,a8),x65384))), % 116.97/117.02 inference(scs_inference,[],[866,51])). % 116.97/117.02 cnf(6663,plain, % 116.97/117.02 (~E(f12(f12(a8,x66631),x66632),f12(f12(a14,x66633),x66634))), % 116.97/117.02 inference(scs_inference,[],[442,51])). % 116.97/117.02 cnf(6665,plain, % 116.97/117.02 (~E(f12(x66651,f12(a2,x66652)),f12(x66653,f12(a8,x66654)))), % 116.97/117.02 inference(scs_inference,[],[860,442,51,50])). % 116.97/117.02 cnf(6677,plain, % 116.97/117.02 (~E(f12(f12(a14,x66771),x66772),f12(f12(a8,x66773),x66774))), % 116.97/117.02 inference(scs_inference,[],[6663,51,50,2])). % 116.97/117.02 cnf(6688,plain, % 116.97/117.02 (~E(f12(f12(x66881,f12(a2,x66882)),x66883),f12(f12(x66884,f12(a8,x66885)),x66886))), % 116.97/117.02 inference(scs_inference,[],[6665,51])). % 116.97/117.02 cnf(6692,plain, % 116.97/117.02 (~E(f12(x66921,f12(a8,x66922)),f12(x66923,f12(a2,x66924)))), % 116.97/117.02 inference(scs_inference,[],[6665,51,50,2])). % 116.97/117.02 cnf(6708,plain, % 116.97/117.02 (~E(f13(f12(f12(f12(a2,f12(a15,a15)),f12(a15,a15)),f12(a15,a15)),f12(f12(a15,a15),f12(a15,a15))),f13(f12(a9,a14),f12(a9,a15)))), % 116.97/117.02 inference(scs_inference,[],[6677,6688,4365,4196,51,50,2,22])). % 116.97/117.02 cnf(6736,plain, % 116.97/117.02 (~P2(f13(f12(a9,a15),f12(a9,a15)),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[39,6692,6708,579,4196,41,51,50,2,70])). % 116.97/117.02 cnf(6740,plain, % 116.97/117.02 (~E(a9,f12(x67401,f12(f12(a9,a15),x67402)))), % 116.97/117.02 inference(scs_inference,[],[39,6692,6708,579,4196,41,51,50,2,70,279,235])). % 116.97/117.02 cnf(6744,plain, % 116.97/117.02 (~E(a10,f12(x67441,f12(a9,a15)))), % 116.97/117.02 inference(scs_inference,[],[39,6692,6708,579,4196,41,51,50,2,70,279,235,237,222])). % 116.97/117.02 cnf(6754,plain, % 116.97/117.02 (~E(f12(x67541,f12(a9,a15)),a10)), % 116.97/117.02 inference(scs_inference,[],[6744,51,50,2])). % 116.97/117.02 cnf(6759,plain, % 116.97/117.02 (~E(f12(f12(x67591,f12(a9,a15)),x67592),f12(a10,x67593))), % 116.97/117.02 inference(scs_inference,[],[6754,51])). % 116.97/117.02 cnf(6773,plain, % 116.97/117.02 (P2(f13(f12(f12(a2,a10),a9),a10),f1(a11))), % 116.97/117.02 inference(scs_inference,[],[39,6759,6740,4551,40,51,50,2,69])). % 116.97/117.02 cnf(7054,plain, % 116.97/117.02 (~E(f12(f12(x70541,x70542),x70543),f12(a2,x70544))), % 116.97/117.02 inference(scs_inference,[],[45,51])). % 116.97/117.02 cnf(7336,plain, % 116.97/117.02 (~E(f12(x73361,f12(x73362,x73363)),f12(x73364,a2))), % 116.97/117.02 inference(scs_inference,[],[45,50])). % 116.97/117.02 cnf(7731,plain, % 116.97/117.02 (~E(f12(f12(x77311,a2),x77312),f12(f12(x77313,a8),x77314))), % 116.97/117.02 inference(rename_variables,[],[6538])). % 116.97/117.02 cnf(7739,plain, % 116.97/117.02 (~E(f12(x77391,f12(x77392,x77393)),f12(x77394,a2))), % 116.97/117.02 inference(rename_variables,[],[7336])). % 116.97/117.02 cnf(7787,plain, % 116.97/117.02 ($false), % 116.97/117.02 inference(scs_inference,[],[40,39,81,6736,6538,7731,7336,7739,7054,6773,76,52,66,62,67,75,209,59,61,3418,2807,2808,2809,2237,1200,1201,1202,894,1134,372,373,255,236,221,203,189,190,60,58,22,56]), % 116.97/117.02 ['proof']). % 116.97/117.02 % SZS output end Proof % 116.97/117.02 % Total time :116.300000s %------------------------------------------------------------------------------