%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL091-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 : 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 04:45:07 EDT 2024 % Result : Unsatisfiable 58.58s 58.72s % Output : CNFRefutation 58.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : COL091-1 : TPTP v8.2.0. Released v2.7.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n025.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:46:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.49/0.57 start to proof:theBenchmark % 58.58/58.70 %------------------------------------------- % 58.58/58.70 % File :CSE---1.7 % 58.58/58.70 % Problem :theBenchmark % 58.58/58.70 % Transform :cnf % 58.58/58.70 % Format :tptp:raw % 58.58/58.70 % Command :java -jar mcs_scs.jar %d %s % 58.58/58.70 % 58.58/58.70 % Result :Theorem 58.050000s % 58.58/58.70 % Output :CNFRefutation 58.050000s % 58.58/58.70 %------------------------------------------- % 58.58/58.71 %-------------------------------------------------------------------------- % 58.58/58.71 % File : COL091-1 : TPTP v8.2.0. Released v2.7.0. % 58.58/58.71 % Domain : Combinatory Logic % 58.58/58.71 % Problem : k1_contractD_c1 % 58.58/58.71 % Version : Reduced > Especial. % 58.58/58.71 % English : comb.app(K, p) -1-> r ==> EX q. r = comb.app(K, q) & p -1-> q % 58.58/58.71 % 58.58/58.71 % Refs : [Men03] Meng (2003), Email to G. Sutcliffe % 58.58/58.71 % Source : [Men03] % 58.58/58.71 % Names : % 58.58/58.71 % 58.58/58.71 % Status : Unsatisfiable % 58.58/58.71 % Rating : 0.15 v8.2.0, 0.19 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.18 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.20 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.10 v5.5.0, 0.40 v5.4.0, 0.35 v5.3.0, 0.39 v5.2.0, 0.38 v5.1.0, 0.47 v5.0.0, 0.43 v4.1.0, 0.54 v4.0.1, 0.36 v4.0.0, 0.18 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.25 v3.3.0, 0.43 v3.2.0, 0.46 v3.1.0, 0.27 v2.7.0 % 58.58/58.71 % Syntax : Number of clauses : 33 ( 8 unt; 1 nHn; 33 RR) % 58.58/58.71 % Number of literals : 66 ( 16 equ; 36 neg) % 58.58/58.71 % Maximal clause size : 5 ( 2 avg) % 58.58/58.71 % Maximal term depth : 5 ( 1 avg) % 58.58/58.71 % Number of predicates : 6 ( 5 usr; 0 prp; 2-3 aty) % 58.58/58.71 % Number of functors : 13 ( 13 usr; 6 con; 0-3 aty) % 58.58/58.71 % Number of variables : 76 ( 23 sgn) % 58.58/58.71 % SPC : CNF_UNS_RFO_SEQ_NHN % 58.58/58.71 % 58.58/58.71 % Comments : Problem coming out of an Isabelle proof. % 58.58/58.71 %-------------------------------------------------------------------------- % 58.58/58.71 %----axioms from CombZF.thy. % 58.58/58.71 %----free algebra for K, S, comb_app(P,Q). % 58.58/58.71 cnf(k_s,axiom, % 58.58/58.71 combK != combS ). % 58.58/58.71 % 58.58/58.71 cnf(k_app,axiom, % 58.58/58.71 combK != comb_app(P,Q) ). % 58.58/58.71 % 58.58/58.71 cnf(s_app,axiom, % 58.58/58.71 combS != comb_app(P,Q) ). % 58.58/58.71 % 58.58/58.71 cnf(app_app1,axiom, % 58.58/58.71 ( comb_app(P1,Q1) != comb_app(P2,Q2) % 58.58/58.71 | P1 = P2 ) ). % 58.58/58.71 % 58.58/58.71 cnf(app_app2,axiom, % 58.58/58.71 ( comb_app(P1,Q1) != comb_app(P2,Q2) % 58.58/58.71 | Q1 = Q2 ) ). % 58.58/58.71 % 58.58/58.71 cnf(app_app3,axiom, % 58.58/58.71 ( P1 != P2 % 58.58/58.71 | Q1 != Q2 % 58.58/58.71 | comb_app(P1,Q1) = comb_app(P2,Q2) ) ). % 58.58/58.71 % 58.58/58.71 %----add in Ap_E. % 58.58/58.71 cnf(ap_E1,axiom, % 58.58/58.71 ( ~ member(comb_app(P,Q),comb) % 58.58/58.71 | member(P,comb) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_E2,axiom, % 58.58/58.71 ( ~ member(comb_app(P,Q),comb) % 58.58/58.71 | member(Q,comb) ) ). % 58.58/58.71 % 58.58/58.71 %----add in comb.intros(three of them). % 58.58/58.71 cnf(comb_intros1,axiom, % 58.58/58.71 member(combK,comb) ). % 58.58/58.71 % 58.58/58.71 cnf(comb_intros2,axiom, % 58.58/58.71 member(combS,comb) ). % 58.58/58.71 % 58.58/58.71 cnf(comb_intros3,axiom, % 58.58/58.71 ( ~ member(P,comb) % 58.58/58.71 | ~ member(Q,comb) % 58.58/58.71 | member(comb_app(P,Q),comb) ) ). % 58.58/58.71 % 58.58/58.71 %----add in reduction_refl [intro!]: % 58.58/58.71 cnf(reduction_refl,axiom, % 58.58/58.71 ( ~ member(A,comb) % 58.58/58.71 | member(pair(A,A),rtrancl(contract)) ) ). % 58.58/58.71 % 58.58/58.71 %----add in contract.K % 58.58/58.71 cnf(contract_K,axiom, % 58.58/58.71 ( ~ member(P,comb) % 58.58/58.71 | ~ member(Q,comb) % 58.58/58.71 | member(pair(comb_app(comb_app(combK,P),Q),P),contract) ) ). % 58.58/58.71 % 58.58/58.71 %----add in contract.S % 58.58/58.71 cnf(contract_S,axiom, % 58.58/58.71 ( ~ member(P,comb) % 58.58/58.71 | ~ member(Q,comb) % 58.58/58.71 | ~ member(R,comb) % 58.58/58.71 | member(pair(comb_app(comb_app(comb_app(combS,P),Q),R),comb_app(comb_app(P,R),comb_app(Q,R))),contract) ) ). % 58.58/58.71 % 58.58/58.71 %----this manually rename the formula Ap_contractE % 58.58/58.71 cnf(ap_contractE1,axiom, % 58.58/58.71 ( ~ member(pair(comb_app(P,Q),R),contract) % 58.58/58.71 | ap_contractE_c1(P,Q,R) % 58.58/58.71 | ap_contractE_c2(P,Q,R) % 58.58/58.71 | ap_contractE_c3(P,Q,R) % 58.58/58.71 | ap_contractE_c4(P,Q,R) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE2,axiom, % 58.58/58.71 ( ~ ap_contractE_c1(P,Q,R) % 58.58/58.71 | member(R,comb) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE3,axiom, % 58.58/58.71 ( ~ ap_contractE_c1(P,Q,R) % 58.58/58.71 | member(Q,comb) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE4,axiom, % 58.58/58.71 ( ~ ap_contractE_c1(P,Q,R) % 58.58/58.71 | P = comb_app(combK,R) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE5,axiom, % 58.58/58.71 ( ~ ap_contractE_c2(P,Q,R) % 58.58/58.71 | member(ap_contractE_sk1p(P,Q,R),comb) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE6,axiom, % 58.58/58.71 ( ~ ap_contractE_c2(P,Q,R) % 58.58/58.71 | member(ap_contractE_sk1q(P,Q,R),comb) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE7,axiom, % 58.58/58.71 ( ~ ap_contractE_c2(P,Q,R) % 58.58/58.71 | member(Q,comb) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE8,axiom, % 58.58/58.71 ( ~ ap_contractE_c2(P,Q,R) % 58.58/58.71 | R = comb_app(comb_app(ap_contractE_sk1p(P,Q,R),Q),comb_app(ap_contractE_sk1q(P,Q,R),Q)) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE9,axiom, % 58.58/58.71 ( ~ ap_contractE_c2(P,Q,R) % 58.58/58.71 | P = comb_app(comb_app(combS,ap_contractE_sk1p(P,Q,R)),ap_contractE_sk1q(P,Q,R)) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE10,axiom, % 58.58/58.71 ( ~ ap_contractE_c3(P,Q,R) % 58.58/58.71 | member(pair(P,ap_contractE_sk2q(P,Q,R)),contract) ) ). % 58.58/58.71 % 58.58/58.71 cnf(ap_contractE11,axiom, % 58.58/58.71 ( ~ ap_contractE_c3(P,Q,R) % 58.58/58.71 | member(Q,comb) ) ). % 58.58/58.72 % 58.58/58.72 cnf(ap_contractE12,axiom, % 58.58/58.72 ( ~ ap_contractE_c3(P,Q,R) % 58.58/58.72 | R = comb_app(ap_contractE_sk2q(P,Q,R),Q) ) ). % 58.58/58.72 % 58.58/58.72 cnf(ap_contractE13,axiom, % 58.58/58.72 ( ~ ap_contractE_c4(P,Q,R) % 58.58/58.72 | member(pair(Q,ap_contractE_sk3q(P,Q,R)),contract) ) ). % 58.58/58.72 % 58.58/58.72 cnf(ap_contractE14,axiom, % 58.58/58.72 ( ~ ap_contractE_c4(P,Q,R) % 58.58/58.72 | member(P,comb) ) ). % 58.58/58.72 % 58.58/58.72 cnf(ap_contractE15,axiom, % 58.58/58.72 ( ~ ap_contractE_c4(P,Q,R) % 58.58/58.72 | R = comb_app(P,ap_contractE_sk3q(P,Q,R)) ) ). % 58.58/58.72 % 58.58/58.72 %----add in K_contractE[elim!]: % 58.58/58.72 cnf(k_contractE,axiom, % 58.58/58.72 ~ member(pair(combK,R),contract) ). % 58.58/58.72 % 58.58/58.72 %----add in S_contractE [elim!]: % 58.58/58.72 %----converted by tptp2X(Ap_contractE+cls_otter.tptp) % 58.58/58.72 cnf(s_contractE,axiom, % 58.58/58.72 ~ member(pair(combS,R),contract) ). % 58.58/58.72 % 58.58/58.72 cnf(k1_contractD_h1,hypothesis, % 58.58/58.72 member(pair(comb_app(combK,p),r),contract) ). % 58.58/58.72 % 58.58/58.72 cnf(k1_contractD_c1,negated_conjecture, % 58.58/58.72 ( r != comb_app(combK,Q) % 58.58/58.72 | ~ member(pair(p,Q),contract) ) ). % 58.58/58.72 % 58.58/58.72 %-------------------------------------------------------------------------- % 58.58/58.72 %------------------------------------------- % 58.58/58.72 % Proof found % 58.58/58.72 % SZS status Theorem for theBenchmark % 58.58/58.72 % SZS output start Proof % 58.58/58.72 %ClaNum:66(EqnAxiom:34) % 58.58/58.72 %VarNum:152(SingletonVarNum:72) % 58.58/58.72 %MaxLitNum:5 % 58.58/58.72 %MaxfuncDepth:3 % 58.58/58.72 %SharedTerms:13 % 58.58/58.72 %goalClause: 48 % 58.58/58.72 [35]P1(a1,a2) % 58.58/58.72 [36]P1(a7,a2) % 58.58/58.72 [38]~E(a1,a7) % 58.58/58.72 [37]P1(f12(f9(a1,a8),a11),a10) % 58.58/58.72 [41]~P1(f12(a1,x411),a10) % 58.58/58.72 [42]~P1(f12(a7,x421),a10) % 58.58/58.72 [39]~E(f9(x391,x392),a1) % 58.58/58.72 [40]~E(f9(x401,x402),a7) % 58.58/58.72 [45]~P1(x451,a2)+P1(f12(x451,x451),f13(a10)) % 58.58/58.72 [48]~P1(f12(a8,x481),a10)+~E(f9(a1,x481),a11) % 58.58/58.72 [46]P1(x461,a2)+~P1(f9(x462,x461),a2) % 58.58/58.72 [47]P1(x471,a2)+~P1(f9(x471,x472),a2) % 58.58/58.72 [50]~P2(x502,x503,x501)+P1(x501,a2) % 58.58/58.72 [51]~P2(x512,x511,x513)+P1(x511,a2) % 58.58/58.72 [52]~P3(x522,x521,x523)+P1(x521,a2) % 58.58/58.72 [53]~P4(x532,x531,x533)+P1(x531,a2) % 58.58/58.72 [54]~P5(x541,x542,x543)+P1(x541,a2) % 58.58/58.72 [55]~P2(x551,x553,x552)+E(x551,f9(a1,x552)) % 58.58/58.72 [56]~P3(x561,x562,x563)+P1(f3(x561,x562,x563),a2) % 58.58/58.72 [57]~P3(x571,x572,x573)+P1(f4(x571,x572,x573),a2) % 58.58/58.72 [58]~P5(x581,x582,x583)+E(f9(x581,f5(x581,x582,x583)),x583) % 58.58/58.72 [59]~P4(x591,x592,x593)+E(f9(f6(x591,x592,x593),x592),x593) % 58.58/58.72 [61]~P5(x612,x611,x613)+P1(f12(x611,f5(x612,x611,x613)),a10) % 58.58/58.72 [62]~P4(x621,x622,x623)+P1(f12(x621,f6(x621,x622,x623)),a10) % 58.58/58.72 [64]~P3(x641,x642,x643)+E(f9(f9(a7,f3(x641,x642,x643)),f4(x641,x642,x643)),x641) % 58.58/58.72 [65]~P3(x651,x652,x653)+E(f9(f9(f3(x651,x652,x653),x652),f9(f4(x651,x652,x653),x652)),x653) % 58.58/58.72 [43]E(x431,x432)+~E(f9(x433,x431),f9(x434,x432)) % 58.58/58.72 [44]E(x441,x442)+~E(f9(x441,x443),f9(x442,x444)) % 58.58/58.72 [49]~P1(x492,a2)+~P1(x491,a2)+P1(f9(x491,x492),a2) % 58.58/58.72 [60]~P1(x602,a2)+~P1(x601,a2)+P1(f12(f9(f9(a1,x601),x602),x601),a10) % 58.68/58.72 [66]~P1(x663,a2)+~P1(x662,a2)+~P1(x661,a2)+P1(f12(f9(f9(f9(a7,x661),x662),x663),f9(f9(x661,x663),f9(x662,x663))),a10) % 58.68/58.72 [63]P3(x631,x632,x633)+P4(x631,x632,x633)+P5(x631,x632,x633)+P2(x631,x632,x633)+~P1(f12(f9(x631,x632),x633),a10) % 58.68/58.72 %EqnAxiom % 58.68/58.72 [1]E(x11,x11) % 58.68/58.72 [2]E(x22,x21)+~E(x21,x22) % 58.68/58.72 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.68/58.72 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43)) % 58.68/58.72 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52)) % 58.68/58.72 [6]~E(x61,x62)+E(f12(x61,x63),f12(x62,x63)) % 58.68/58.72 [7]~E(x71,x72)+E(f12(x73,x71),f12(x73,x72)) % 58.68/58.72 [8]~E(x81,x82)+E(f6(x81,x83,x84),f6(x82,x83,x84)) % 58.68/58.72 [9]~E(x91,x92)+E(f6(x93,x91,x94),f6(x93,x92,x94)) % 58.68/58.72 [10]~E(x101,x102)+E(f6(x103,x104,x101),f6(x103,x104,x102)) % 58.68/58.72 [11]~E(x111,x112)+E(f4(x111,x113,x114),f4(x112,x113,x114)) % 58.68/58.72 [12]~E(x121,x122)+E(f4(x123,x121,x124),f4(x123,x122,x124)) % 58.68/58.72 [13]~E(x131,x132)+E(f4(x133,x134,x131),f4(x133,x134,x132)) % 58.68/58.72 [14]~E(x141,x142)+E(f5(x141,x143,x144),f5(x142,x143,x144)) % 58.68/58.72 [15]~E(x151,x152)+E(f5(x153,x151,x154),f5(x153,x152,x154)) % 58.68/58.72 [16]~E(x161,x162)+E(f5(x163,x164,x161),f5(x163,x164,x162)) % 58.68/58.72 [17]~E(x171,x172)+E(f13(x171),f13(x172)) % 58.68/58.72 [18]~E(x181,x182)+E(f3(x181,x183,x184),f3(x182,x183,x184)) % 58.68/58.72 [19]~E(x191,x192)+E(f3(x193,x191,x194),f3(x193,x192,x194)) % 58.68/58.72 [20]~E(x201,x202)+E(f3(x203,x204,x201),f3(x203,x204,x202)) % 58.68/58.72 [21]P1(x212,x213)+~E(x211,x212)+~P1(x211,x213) % 58.68/58.72 [22]P1(x223,x222)+~E(x221,x222)+~P1(x223,x221) % 58.68/58.72 [23]P3(x232,x233,x234)+~E(x231,x232)+~P3(x231,x233,x234) % 58.68/58.72 [24]P3(x243,x242,x244)+~E(x241,x242)+~P3(x243,x241,x244) % 58.68/58.72 [25]P3(x253,x254,x252)+~E(x251,x252)+~P3(x253,x254,x251) % 58.68/58.72 [26]P2(x262,x263,x264)+~E(x261,x262)+~P2(x261,x263,x264) % 58.68/58.72 [27]P2(x273,x272,x274)+~E(x271,x272)+~P2(x273,x271,x274) % 58.68/58.72 [28]P2(x283,x284,x282)+~E(x281,x282)+~P2(x283,x284,x281) % 58.68/58.72 [29]P5(x292,x293,x294)+~E(x291,x292)+~P5(x291,x293,x294) % 58.68/58.72 [30]P5(x303,x302,x304)+~E(x301,x302)+~P5(x303,x301,x304) % 58.68/58.72 [31]P5(x313,x314,x312)+~E(x311,x312)+~P5(x313,x314,x311) % 58.68/58.72 [32]P4(x322,x323,x324)+~E(x321,x322)+~P4(x321,x323,x324) % 58.68/58.72 [33]P4(x333,x332,x334)+~E(x331,x332)+~P4(x333,x331,x334) % 58.68/58.72 [34]P4(x343,x344,x342)+~E(x341,x342)+~P4(x343,x344,x341) % 58.68/58.72 % 58.68/58.72 %------------------------------------------- % 58.68/58.73 cnf(69,plain, % 58.68/58.73 (~P5(x691,a1,x692)), % 58.68/58.73 inference(scs_inference,[],[41,61])). % 58.68/58.73 cnf(70,plain, % 58.68/58.73 (~P1(f12(a1,x701),a10)), % 58.68/58.73 inference(rename_variables,[],[41])). % 58.68/58.73 cnf(73,plain, % 58.68/58.73 (~E(f9(x731,x732),a1)), % 58.68/58.73 inference(rename_variables,[],[39])). % 58.68/58.73 cnf(75,plain, % 58.68/58.73 (~P4(a1,x751,x752)), % 58.68/58.73 inference(scs_inference,[],[39,41,70,61,58,62])). % 58.68/58.73 cnf(76,plain, % 58.68/58.73 (~P1(f12(a1,x761),a10)), % 58.68/58.73 inference(rename_variables,[],[41])). % 58.68/58.73 cnf(79,plain, % 58.68/58.73 (~E(f9(x791,x792),a1)), % 58.68/58.73 inference(rename_variables,[],[39])). % 58.68/58.73 cnf(81,plain, % 58.68/58.73 (~P3(a1,x811,x812)), % 58.68/58.73 inference(scs_inference,[],[39,73,79,41,70,61,58,62,59,64])). % 58.68/58.73 cnf(82,plain, % 58.68/58.73 (~E(f9(x821,x822),a1)), % 58.68/58.73 inference(rename_variables,[],[39])). % 58.68/58.73 cnf(87,plain, % 58.68/58.73 (~E(f12(f9(a1,a8),a11),f12(a1,x871))), % 58.68/58.73 inference(scs_inference,[],[39,73,79,82,41,70,76,37,61,58,62,59,64,65,21])). % 58.68/58.73 cnf(88,plain, % 58.68/58.73 (P1(a1,x881)+~E(a2,x881)), % 58.68/58.73 inference(scs_inference,[],[35,39,73,79,82,41,70,76,37,61,58,62,59,64,65,21,22])). % 58.68/58.73 cnf(89,plain, % 58.68/58.73 (P5(a1,a8,a11)+P2(a1,a8,a11)), % 58.68/58.73 inference(scs_inference,[],[35,39,73,79,82,41,70,76,37,61,58,62,59,64,65,21,22,63])). % 58.68/58.73 cnf(92,plain, % 58.68/58.73 (~P3(a7,x921,x922)), % 58.68/58.73 inference(scs_inference,[],[40,64])). % 58.68/58.73 cnf(93,plain, % 58.68/58.73 (~E(f9(x931,x932),a7)), % 58.68/58.73 inference(rename_variables,[],[40])). % 58.68/58.73 cnf(96,plain, % 58.68/58.73 (~E(f9(x961,x962),a7)), % 58.68/58.73 inference(rename_variables,[],[40])). % 58.68/58.73 cnf(98,plain, % 58.68/58.73 (~P5(x981,x982,a7)), % 58.68/58.73 inference(scs_inference,[],[40,93,96,64,65,58])). % 58.68/58.73 cnf(99,plain, % 58.68/58.73 (~E(f9(x991,x992),a7)), % 58.68/58.73 inference(rename_variables,[],[40])). % 58.68/58.73 cnf(101,plain, % 58.68/58.73 (~P4(x1011,x1012,a7)), % 58.68/58.73 inference(scs_inference,[],[40,93,96,99,64,65,58,59])). % 58.68/58.73 cnf(105,plain, % 58.68/58.73 (~P1(f12(a7,x1051),a10)), % 58.68/58.73 inference(rename_variables,[],[42])). % 58.68/58.73 cnf(107,plain, % 58.68/58.73 (~P5(x1071,a7,x1072)), % 58.68/58.73 inference(scs_inference,[],[40,93,96,99,42,105,64,65,58,59,62,61])). % 58.68/58.73 cnf(108,plain, % 58.68/58.73 (~P1(f12(a7,x1081),a10)), % 58.68/58.73 inference(rename_variables,[],[42])). % 58.68/58.73 cnf(111,plain, % 58.68/58.73 (P1(a7,x1111)+~E(a2,x1111)), % 58.68/58.73 inference(scs_inference,[],[36,40,93,96,99,42,105,108,37,64,65,58,59,62,61,21,22])). % 58.68/58.73 cnf(114,plain, % 58.68/58.73 (P1(x1141,a2)+~E(a1,x1141)), % 58.68/58.73 inference(scs_inference,[],[35,37,22,21])). % 58.68/58.73 cnf(128,plain, % 58.68/58.73 (~E(a1,f9(a1,a8))), % 58.68/58.73 inference(scs_inference,[],[87,2,6])). % 58.68/58.73 cnf(129,plain, % 58.68/58.73 (~P2(a1,x1291,a8)), % 58.68/58.73 inference(scs_inference,[],[128,55])). % 58.68/58.73 cnf(132,plain, % 58.68/58.73 (P5(a1,a8,a11)+P1(a8,a2)), % 58.68/58.73 inference(scs_inference,[],[51,89])). % 58.68/58.73 cnf(139,plain, % 58.68/58.73 (P1(a8,a2)+P1(f12(a8,f5(a1,a8,a11)),a10)), % 58.68/58.73 inference(scs_inference,[],[132,61])). % 58.68/58.73 cnf(146,plain, % 58.68/58.73 (~E(f9(f9(a1,x1461),x1462),f9(a11,x1463))+~P1(f12(a8,x1461),a10)), % 58.68/58.73 inference(scs_inference,[],[48,44])). % 58.68/58.73 cnf(157,plain, % 58.68/58.73 (~E(f9(f9(a1,f5(a1,a8,a11)),x1571),f9(a11,x1572))+P1(a8,a2)), % 58.68/58.73 inference(scs_inference,[],[139,146])). % 58.68/58.73 cnf(176,plain, % 58.68/58.73 (~E(f9(a1,f5(a1,a8,a11)),a11)+P1(a8,a2)), % 58.68/58.73 inference(scs_inference,[],[157,4])). % 58.68/58.73 cnf(177,plain, % 58.68/58.73 (~P5(a1,a8,a11)+P1(a8,a2)), % 58.68/58.73 inference(scs_inference,[],[176,58])). % 58.68/58.73 cnf(178,plain, % 58.68/58.73 (P1(a8,a2)), % 58.68/58.73 inference(scs_inference,[],[177,132])). % 58.68/58.73 cnf(210,plain, % 58.68/58.73 (~E(a7,x2101)+~E(f9(x2102,x2103),x2101)), % 58.68/58.73 inference(scs_inference,[],[40,3,2])). % 58.68/58.73 cnf(216,plain, % 58.68/58.73 (~E(a1,x2161)+~P1(f12(f9(a1,a1),a8),a10)), % 58.68/58.73 inference(scs_inference,[],[129,75,69,81,27,63])). % 58.68/58.73 cnf(217,plain, % 58.68/58.73 (~P1(f12(f9(a1,a1),a8),a10)), % 58.68/58.73 inference(equality_inference,[],[216])). % 58.68/58.73 cnf(223,plain, % 58.68/58.73 (P1(f9(a1,x2231),a2)+~P1(f9(x2232,x2231),a2)), % 58.68/58.73 inference(scs_inference,[],[35,49,46])). % 58.68/58.73 cnf(245,plain, % 58.68/58.73 (~E(f12(f9(a1,a8),a11),f12(f9(a1,a1),a8))), % 58.68/58.73 inference(scs_inference,[],[217,37,21])). % 58.68/58.73 cnf(289,plain, % 58.68/58.73 (~E(f9(x2891,f12(f9(a1,a1),a8)),f9(x2892,f12(f9(a1,a8),a11)))), % 58.68/58.73 inference(scs_inference,[],[245,2,43])). % 58.68/58.73 cnf(296,plain, % 58.68/58.73 (~P2(f9(x2961,f12(f9(a1,a8),a11)),x2962,f12(f9(a1,a1),a8))), % 58.68/58.73 inference(scs_inference,[],[289,2,55])). % 58.68/58.73 cnf(430,plain, % 58.68/58.73 (~E(a1,x4301)+~P5(x4302,x4301,x4303)), % 58.68/58.73 inference(scs_inference,[],[69,2,30])). % 58.68/58.73 cnf(449,plain, % 58.68/58.73 (~E(f9(x4491,a7),f9(x4492,f9(x4493,x4494)))), % 58.68/58.73 inference(scs_inference,[],[40,2,43])). % 58.68/58.73 cnf(450,plain, % 58.68/58.73 (~E(a7,f9(x4501,x4502))), % 58.68/58.73 inference(scs_inference,[],[449,5])). % 58.68/58.73 cnf(451,plain, % 58.68/58.73 (~E(f9(x4511,a7),f9(x4512,f9(x4513,x4514)))), % 58.68/58.73 inference(rename_variables,[],[449])). % 58.68/58.73 cnf(452,plain, % 58.68/58.73 (~P4(x4521,a7,f9(x4522,f9(x4523,x4524)))), % 58.68/58.73 inference(scs_inference,[],[449,451,5,59])). % 58.68/58.73 cnf(453,plain, % 58.68/58.73 (~E(f9(x4531,a7),f9(x4532,f9(x4533,x4534)))), % 58.68/58.73 inference(rename_variables,[],[449])). % 58.68/58.73 cnf(455,plain, % 58.68/58.73 (~P2(f9(x4551,a7),x4552,f9(x4553,x4554))), % 58.68/58.73 inference(scs_inference,[],[449,451,453,5,59,55])). % 58.68/58.73 cnf(458,plain, % 58.68/58.73 (~E(f9(a7,x4581),f9(f9(x4582,x4583),x4584))), % 58.68/58.73 inference(scs_inference,[],[40,2,44])). % 58.68/58.73 cnf(462,plain, % 58.68/58.73 (~P2(a7,x4621,x4622)), % 58.68/58.73 inference(scs_inference,[],[458,450,58,55])). % 58.68/58.73 cnf(465,plain, % 58.68/58.73 (~P4(x4651,f9(x4652,x4653),f9(x4654,a7))), % 58.68/58.73 inference(scs_inference,[],[449,2,59])). % 58.68/58.73 cnf(466,plain, % 58.68/58.73 (~E(f9(x4661,f9(x4662,f9(x4663,x4664))),f9(x4665,f9(x4666,a7)))), % 58.68/58.73 inference(scs_inference,[],[449,2,43])). % 58.68/58.73 cnf(486,plain, % 58.68/58.73 (~E(f9(f9(x4861,f9(x4862,x4863)),x4864),f9(f9(x4865,a7),x4866))), % 58.68/58.73 inference(scs_inference,[],[449,2,44])). % 58.68/58.73 cnf(600,plain, % 58.68/58.73 (~E(f9(f9(x6001,x6002),x6003),f9(a7,x6004))), % 58.68/58.73 inference(scs_inference,[],[450,2,44])). % 58.68/58.73 cnf(602,plain, % 58.68/58.73 (~E(f9(f9(x6021,x6022),x6023),f9(a7,x6024))), % 58.68/58.73 inference(rename_variables,[],[600])). % 58.68/58.73 cnf(604,plain, % 58.68/58.73 (~P5(f9(x6041,x6042),x6043,f9(a7,x6044))), % 58.68/58.73 inference(scs_inference,[],[600,602,65,58])). % 58.68/58.73 cnf(615,plain, % 58.68/58.73 (~E(f9(x6151,x6152),x6153)+~P4(x6154,x6153,f9(x6155,a7))), % 58.68/58.73 inference(scs_inference,[],[465,2,33])). % 58.68/58.73 cnf(637,plain, % 58.68/58.73 (P1(f12(f9(f9(f9(a7,a1),a1),a1),f9(f9(a1,a1),f9(a1,a1))),a10)), % 58.68/58.73 inference(scs_inference,[],[88,66])). % 58.68/58.73 cnf(1185,plain, % 58.68/58.73 (P1(f9(a7,a7),a2)), % 58.68/58.73 inference(scs_inference,[],[111,49])). % 58.68/58.73 cnf(1655,plain, % 58.68/58.73 (P1(f12(f9(f9(a1,a7),a7),a7),a10)), % 58.68/58.73 inference(scs_inference,[],[111,60])). % 58.68/58.73 cnf(1656,plain, % 58.68/58.73 (~E(f12(f9(f9(a1,a7),a7),a7),f12(a7,x16561))), % 58.68/58.73 inference(scs_inference,[],[42,1655,21])). % 58.68/58.73 cnf(1972,plain, % 58.68/58.73 (P1(f12(f9(f9(f9(a7,a7),a7),a7),f9(f9(a7,a7),f9(a7,a7))),a10)), % 58.68/58.73 inference(scs_inference,[],[111,66])). % 58.68/58.73 cnf(1974,plain, % 58.68/58.73 (P3(f9(f9(a7,a7),a7),a7,f9(f9(a7,a7),f9(a7,a7)))), % 58.68/58.73 inference(scs_inference,[],[107,42,1972,455,452,21,63])). % 58.68/58.73 cnf(3618,plain, % 58.68/58.73 (~E(a1,x36181)+P1(f9(a8,x36181),a2)), % 58.68/58.73 inference(scs_inference,[],[178,114,49])). % 58.68/58.73 cnf(3619,plain, % 58.68/58.73 (P1(f9(a8,a1),a2)), % 58.68/58.73 inference(equality_inference,[],[3618])). % 58.68/58.73 cnf(6517,plain, % 58.68/58.73 (~E(a1,x65171)+P1(f9(x65171,f9(a7,a7)),a2)), % 58.68/58.73 inference(scs_inference,[],[1185,114,49])). % 58.68/58.73 cnf(6518,plain, % 58.68/58.73 (P1(f9(a1,f9(a7,a7)),a2)), % 58.68/58.73 inference(equality_inference,[],[6517])). % 58.68/58.73 cnf(6850,plain, % 58.68/58.73 (~E(f12(f9(f9(a1,a7),a7),a7),f12(f9(a1,a1),a8))), % 58.68/58.73 inference(scs_inference,[],[1655,217,21])). % 58.68/58.73 cnf(7161,plain, % 58.68/58.73 (~E(f12(f9(f9(f9(a7,a1),a1),a1),f9(f9(a1,a1),f9(a1,a1))),f12(a1,x71611))), % 58.68/58.73 inference(scs_inference,[],[1656,637,41,2,21])). % 58.68/58.73 cnf(7219,plain, % 58.68/58.73 (~E(a1,f9(x72191,x72192))), % 58.68/58.73 inference(scs_inference,[],[39,2])). % 58.68/58.73 cnf(7223,plain, % 58.68/58.73 (P5(a1,a8,a11)), % 58.68/58.73 inference(scs_inference,[],[6850,75,39,37,81,2,55,3,63])). % 58.68/58.73 cnf(7231,plain, % 58.68/58.73 (~E(f9(x72311,f9(x72312,a7)),f9(x72313,f9(x72314,f9(x72315,x72316))))), % 58.68/58.73 inference(scs_inference,[],[466,2])). % 58.68/58.73 cnf(7232,plain, % 58.68/58.73 (~P2(f9(x72321,f9(x72322,a7)),x72323,f9(x72324,f9(x72325,x72326)))), % 58.68/58.73 inference(scs_inference,[],[466,2,55])). % 58.68/58.73 cnf(7255,plain, % 58.68/58.73 (~P5(x72551,x72552,f9(a7,x72553))+~E(x72551,f9(x72554,x72555))), % 58.68/58.73 inference(scs_inference,[],[604,7161,486,296,7232,7231,59,2,58,28,3,26,29])). % 58.68/58.73 cnf(7339,plain, % 58.68/58.73 (~E(a7,a1)), % 58.68/58.73 inference(scs_inference,[],[38,2])). % 58.68/58.73 cnf(7353,plain, % 58.68/58.73 (~E(x73531,a1)+~E(f9(x73532,x73533),x73531)), % 58.68/58.73 inference(scs_inference,[],[39,3])). % 58.68/58.73 cnf(7715,plain, % 58.68/58.73 (~E(x77151,f9(x77152,x77153))+~E(a1,x77151)), % 58.68/58.73 inference(scs_inference,[],[7219,3])). % 58.68/58.73 cnf(8261,plain, % 58.68/58.73 (~P5(x82611,x82612,a7)), % 58.68/58.73 inference(rename_variables,[],[98])). % 58.68/58.73 cnf(8293,plain, % 58.68/58.73 ($false), % 58.68/58.73 inference(scs_inference,[],[98,8261,7339,6518,3619,92,462,217,1972,101,1185,7223,1974,430,43,44,56,57,45,223,58,61,17,6,7,5,4,2,31,49,60,21,3,66,63,210,7353,7715,615,7255,8,9,10,11,12,13,14,15,16,18,19,20,48]), % 58.68/58.73 ['proof']). % 58.68/58.73 % SZS output end Proof % 58.68/58.73 % Total time :58.050000s %------------------------------------------------------------------------------