%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU121+2 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n032.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 15:01:08 EDT 2024 % Result : Theorem 58.51s 58.67s % Output : CNFRefutation 58.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SEU121+2 : TPTP v8.2.0. Released v3.3.0. % 0.00/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.26 % Computer : n032.cluster.edu % 0.07/0.26 % Model : x86_64 x86_64 % 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.26 % Memory : 8042.1875MB % 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.27 % CPULimit : 300 % 0.07/0.27 % WCLimit : 300 % 0.07/0.27 % DateTime : Fri Jun 21 13:37:38 EDT 2024 % 0.07/0.27 % CPUTime : % 0.11/0.45 start to proof:theBenchmark % 58.51/58.65 %------------------------------------------- % 58.51/58.65 % File :CSE---1.7 % 58.51/58.65 % Problem :theBenchmark % 58.51/58.65 % Transform :cnf % 58.51/58.65 % Format :tptp:raw % 58.51/58.65 % Command :java -jar mcs_scs.jar %d %s % 58.51/58.65 % 58.51/58.65 % Result :Theorem 58.170000s % 58.51/58.65 % Output :CNFRefutation 58.170000s % 58.51/58.65 %------------------------------------------- % 58.51/58.66 %------------------------------------------------------------------------------ % 58.51/58.66 % File : SEU121+2 : TPTP v8.2.0. Released v3.3.0. % 58.51/58.66 % Domain : Set theory % 58.51/58.66 % Problem : MPTP chainy problem t1_xboole_1 % 58.51/58.66 % Version : [Urb07] axioms : Especial. % 58.51/58.66 % English : % 58.51/58.66 % 58.51/58.66 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 58.51/58.66 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 58.51/58.66 % Source : [Urb07] % 58.51/58.66 % Names : chainy-t1_xboole_1 [Urb07] % 58.51/58.66 % 58.51/58.66 % Status : Theorem % 58.51/58.66 % Rating : 0.08 v8.1.0, 0.03 v7.2.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.10 v6.0.0, 0.17 v5.5.0, 0.11 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.05 v5.0.0, 0.08 v4.1.0, 0.09 v4.0.1, 0.13 v4.0.0, 0.17 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0 % 58.51/58.66 % Syntax : Number of formulae : 20 ( 8 unt; 0 def) % 58.51/58.66 % Number of atoms : 43 ( 7 equ) % 58.51/58.66 % Maximal formula atoms : 6 ( 2 avg) % 58.51/58.66 % Number of connectives : 37 ( 14 ~; 0 |; 13 &) % 58.51/58.66 % ( 5 <=>; 5 =>; 0 <=; 0 <~>) % 58.51/58.66 % Maximal formula depth : 9 ( 4 avg) % 58.51/58.66 % Maximal term depth : 2 ( 1 avg) % 58.51/58.66 % Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty) % 58.51/58.66 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 58.51/58.66 % Number of variables : 39 ( 35 !; 4 ?) % 58.51/58.66 % SPC : FOF_THM_RFO_SEQ % 58.51/58.66 % 58.51/58.66 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.51/58.66 % library, www.mizar.org % 58.51/58.66 %------------------------------------------------------------------------------ % 58.51/58.66 fof(antisymmetry_r2_hidden,axiom, % 58.51/58.66 ! [A,B] : % 58.51/58.66 ( in(A,B) % 58.51/58.66 => ~ in(B,A) ) ). % 58.51/58.66 % 58.51/58.66 fof(commutativity_k3_xboole_0,axiom, % 58.51/58.66 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 58.51/58.66 % 58.51/58.66 fof(d1_xboole_0,axiom, % 58.51/58.66 ! [A] : % 58.51/58.66 ( A = empty_set % 58.51/58.66 <=> ! [B] : ~ in(B,A) ) ). % 58.51/58.66 % 58.51/58.66 fof(d3_tarski,axiom, % 58.51/58.66 ! [A,B] : % 58.51/58.66 ( subset(A,B) % 58.51/58.66 <=> ! [C] : % 58.51/58.66 ( in(C,A) % 58.51/58.66 => in(C,B) ) ) ). % 58.51/58.66 % 58.51/58.66 fof(d3_xboole_0,axiom, % 58.51/58.66 ! [A,B,C] : % 58.51/58.66 ( C = set_intersection2(A,B) % 58.51/58.66 <=> ! [D] : % 58.51/58.66 ( in(D,C) % 58.51/58.66 <=> ( in(D,A) % 58.51/58.66 & in(D,B) ) ) ) ). % 58.51/58.66 % 58.51/58.66 fof(d7_xboole_0,axiom, % 58.51/58.66 ! [A,B] : % 58.51/58.66 ( disjoint(A,B) % 58.51/58.66 <=> set_intersection2(A,B) = empty_set ) ). % 58.51/58.66 % 58.51/58.66 fof(dt_k1_xboole_0,axiom, % 58.51/58.66 $true ). % 58.51/58.66 % 58.51/58.66 fof(dt_k3_xboole_0,axiom, % 58.51/58.66 $true ). % 58.51/58.66 % 58.51/58.66 fof(fc1_xboole_0,axiom, % 58.51/58.66 empty(empty_set) ). % 58.51/58.66 % 58.51/58.66 fof(idempotence_k3_xboole_0,axiom, % 58.51/58.66 ! [A,B] : set_intersection2(A,A) = A ). % 58.51/58.66 % 58.51/58.66 fof(rc1_xboole_0,axiom, % 58.51/58.66 ? [A] : empty(A) ). % 58.51/58.66 % 58.51/58.66 fof(rc2_xboole_0,axiom, % 58.51/58.66 ? [A] : ~ empty(A) ). % 58.51/58.66 % 58.51/58.66 fof(reflexivity_r1_tarski,axiom, % 58.51/58.66 ! [A,B] : subset(A,A) ). % 58.51/58.66 % 58.51/58.66 fof(symmetry_r1_xboole_0,axiom, % 58.51/58.66 ! [A,B] : % 58.51/58.66 ( disjoint(A,B) % 58.51/58.66 => disjoint(B,A) ) ). % 58.51/58.66 % 58.51/58.66 fof(t1_xboole_1,conjecture, % 58.51/58.66 ! [A,B,C] : % 58.51/58.66 ( ( subset(A,B) % 58.51/58.66 & subset(B,C) ) % 58.51/58.66 => subset(A,C) ) ). % 58.51/58.66 % 58.51/58.66 fof(t3_xboole_0,lemma, % 58.51/58.66 ! [A,B] : % 58.51/58.66 ( ~ ( ~ disjoint(A,B) % 58.51/58.66 & ! [C] : % 58.51/58.66 ~ ( in(C,A) % 58.51/58.66 & in(C,B) ) ) % 58.51/58.66 & ~ ( ? [C] : % 58.51/58.66 ( in(C,A) % 58.51/58.66 & in(C,B) ) % 58.51/58.66 & disjoint(A,B) ) ) ). % 58.51/58.66 % 58.51/58.66 fof(t4_xboole_0,lemma, % 58.51/58.66 ! [A,B] : % 58.51/58.66 ( ~ ( ~ disjoint(A,B) % 58.51/58.66 & ! [C] : ~ in(C,set_intersection2(A,B)) ) % 58.51/58.66 & ~ ( ? [C] : in(C,set_intersection2(A,B)) % 58.51/58.66 & disjoint(A,B) ) ) ). % 58.51/58.66 % 58.51/58.66 fof(t6_boole,axiom, % 58.51/58.66 ! [A] : % 58.51/58.66 ( empty(A) % 58.51/58.66 => A = empty_set ) ). % 58.51/58.66 % 58.51/58.66 fof(t7_boole,axiom, % 58.51/58.66 ! [A,B] : % 58.51/58.66 ~ ( in(A,B) % 58.51/58.66 & empty(B) ) ). % 58.51/58.67 % 58.51/58.67 fof(t8_boole,axiom, % 58.51/58.67 ! [A,B] : % 58.51/58.67 ~ ( empty(A) % 58.51/58.67 & A != B % 58.51/58.67 & empty(B) ) ). % 58.51/58.67 % 58.51/58.67 %------------------------------------------------------------------------------ % 58.51/58.67 %------------------------------------------- % 58.51/58.67 % Proof found % 58.51/58.67 % SZS status Theorem for theBenchmark % 58.51/58.67 % SZS output start Proof % 58.51/58.67 %ClaNum:54(EqnAxiom:22) % 58.51/58.67 %VarNum:143(SingletonVarNum:60) % 58.51/58.67 %MaxLitNum:4 % 58.51/58.67 %MaxfuncDepth:1 % 58.51/58.67 %SharedTerms:12 % 58.51/58.67 %goalClause: 25 26 31 % 58.51/58.67 %singleGoalClaCount:3 % 58.51/58.67 [23]P1(a1) % 58.51/58.67 [24]P1(a2) % 58.51/58.67 [25]P3(a7,a9) % 58.51/58.67 [26]P3(a9,a10) % 58.51/58.67 [30]~P1(a8) % 58.51/58.67 [31]~P3(a7,a10) % 58.51/58.67 [27]P3(x271,x271) % 58.51/58.67 [28]E(f11(x281,x281),x281) % 58.51/58.67 [29]E(f11(x291,x292),f11(x292,x291)) % 58.51/58.67 [32]~P1(x321)+E(x321,a1) % 58.51/58.67 [34]P4(f3(x341),x341)+E(x341,a1) % 58.51/58.67 [35]~P4(x352,x351)+~E(x351,a1) % 58.51/58.67 [36]~P1(x361)+~P4(x362,x361) % 58.51/58.67 [39]~P2(x392,x391)+P2(x391,x392) % 58.51/58.67 [40]~P4(x402,x401)+~P4(x401,x402) % 58.51/58.67 [37]~P2(x371,x372)+E(f11(x371,x372),a1) % 58.51/58.67 [38]P2(x381,x382)+~E(f11(x381,x382),a1) % 58.51/58.67 [41]P3(x411,x412)+P4(f5(x411,x412),x411) % 58.51/58.67 [42]P2(x421,x422)+P4(f12(x421,x422),x422) % 58.51/58.67 [43]P2(x431,x432)+P4(f12(x431,x432),x431) % 58.51/58.67 [48]P3(x481,x482)+~P4(f5(x481,x482),x482) % 58.51/58.67 [49]P2(x491,x492)+P4(f4(x491,x492),f11(x491,x492)) % 58.51/58.67 [51]~P2(x511,x512)+~P4(x513,f11(x511,x512)) % 58.51/58.67 [33]~P1(x332)+~P1(x331)+E(x331,x332) % 58.51/58.67 [44]~P3(x443,x442)+P4(x441,x442)+~P4(x441,x443) % 58.51/58.67 [47]~P2(x473,x472)+~P4(x471,x472)+~P4(x471,x473) % 58.51/58.67 [52]P4(f6(x522,x523,x521),x521)+P4(f6(x522,x523,x521),x523)+E(x521,f11(x522,x523)) % 58.51/58.67 [53]P4(f6(x532,x533,x531),x531)+P4(f6(x532,x533,x531),x532)+E(x531,f11(x532,x533)) % 58.51/58.67 [45]~P4(x451,x453)+P4(x451,x452)+~E(x453,f11(x454,x452)) % 58.51/58.67 [46]~P4(x461,x463)+P4(x461,x462)+~E(x463,f11(x462,x464)) % 58.51/58.67 [54]~P4(f6(x542,x543,x541),x541)+~P4(f6(x542,x543,x541),x543)+~P4(f6(x542,x543,x541),x542)+E(x541,f11(x542,x543)) % 58.51/58.67 [50]~P4(x501,x504)+~P4(x501,x503)+P4(x501,x502)+~E(x502,f11(x503,x504)) % 58.51/58.67 %EqnAxiom % 58.51/58.67 [1]E(x11,x11) % 58.51/58.67 [2]E(x22,x21)+~E(x21,x22) % 58.51/58.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.51/58.67 [4]~E(x41,x42)+E(f11(x41,x43),f11(x42,x43)) % 58.51/58.67 [5]~E(x51,x52)+E(f11(x53,x51),f11(x53,x52)) % 58.51/58.67 [6]~E(x61,x62)+E(f6(x61,x63,x64),f6(x62,x63,x64)) % 58.51/58.67 [7]~E(x71,x72)+E(f6(x73,x71,x74),f6(x73,x72,x74)) % 58.51/58.67 [8]~E(x81,x82)+E(f6(x83,x84,x81),f6(x83,x84,x82)) % 58.51/58.67 [9]~E(x91,x92)+E(f4(x91,x93),f4(x92,x93)) % 58.51/58.67 [10]~E(x101,x102)+E(f4(x103,x101),f4(x103,x102)) % 58.51/58.67 [11]~E(x111,x112)+E(f3(x111),f3(x112)) % 58.51/58.67 [12]~E(x121,x122)+E(f5(x121,x123),f5(x122,x123)) % 58.51/58.67 [13]~E(x131,x132)+E(f5(x133,x131),f5(x133,x132)) % 58.51/58.67 [14]~E(x141,x142)+E(f12(x141,x143),f12(x142,x143)) % 58.51/58.67 [15]~E(x151,x152)+E(f12(x153,x151),f12(x153,x152)) % 58.51/58.67 [16]~P1(x161)+P1(x162)+~E(x161,x162) % 58.51/58.67 [17]P4(x172,x173)+~E(x171,x172)+~P4(x171,x173) % 58.51/58.67 [18]P4(x183,x182)+~E(x181,x182)+~P4(x183,x181) % 58.51/58.67 [19]P3(x192,x193)+~E(x191,x192)+~P3(x191,x193) % 58.51/58.67 [20]P3(x203,x202)+~E(x201,x202)+~P3(x203,x201) % 58.51/58.67 [21]P2(x212,x213)+~E(x211,x212)+~P2(x211,x213) % 58.51/58.67 [22]P2(x223,x222)+~E(x221,x222)+~P2(x223,x221) % 58.51/58.67 % 58.51/58.67 %------------------------------------------- % 58.51/58.67 cnf(55,plain, % 58.51/58.67 (~P4(x551,a1)), % 58.51/58.67 inference(equality_inference,[],[35])). % 58.51/58.67 cnf(56,plain, % 58.51/58.67 (~P4(x561,f11(x562,x563))+P4(x561,x563)), % 58.51/58.67 inference(equality_inference,[],[45])). % 58.51/58.67 cnf(57,plain, % 58.51/58.67 (~P4(x571,f11(x572,x573))+P4(x571,x572)), % 58.51/58.67 inference(equality_inference,[],[46])). % 58.51/58.67 cnf(58,plain, % 58.51/58.68 (~P4(x581,x582)+~P4(x581,x583)+P4(x581,f11(x583,x582))), % 58.51/58.68 inference(equality_inference,[],[50])). % 58.51/58.68 cnf(60,plain, % 58.51/58.68 (~P4(x601,a1)), % 58.51/58.68 inference(rename_variables,[],[55])). % 58.51/58.68 cnf(63,plain, % 58.51/58.68 (E(f11(x631,x631),x631)), % 58.51/58.68 inference(rename_variables,[],[28])). % 58.51/58.68 cnf(65,plain, % 58.51/58.68 (~P4(x651,a2)), % 58.51/58.68 inference(scs_inference,[],[55,28,24,41,35,36])). % 58.51/58.68 cnf(67,plain, % 58.51/58.68 (P2(x671,a1)), % 58.51/58.68 inference(scs_inference,[],[55,60,28,24,41,35,36,42])). % 58.51/58.68 cnf(68,plain, % 58.51/58.68 (~P4(x681,a1)), % 58.51/58.68 inference(rename_variables,[],[55])). % 58.51/58.68 cnf(70,plain, % 58.51/58.68 (P2(a1,x701)), % 58.51/58.68 inference(scs_inference,[],[55,60,68,28,24,41,35,36,42,43])). % 58.51/58.68 cnf(71,plain, % 58.51/58.68 (~P4(x711,a1)), % 58.51/58.68 inference(rename_variables,[],[55])). % 58.51/58.68 cnf(73,plain, % 58.51/58.68 (~P4(x731,f11(x732,a1))), % 58.51/58.68 inference(scs_inference,[],[55,60,68,71,28,24,41,35,36,42,43,56])). % 58.51/58.68 cnf(75,plain, % 58.51/58.68 (~P4(x751,f11(a1,x752))), % 58.51/58.68 inference(scs_inference,[],[55,60,68,71,28,24,41,35,36,42,43,56,57])). % 58.51/58.68 cnf(77,plain, % 58.51/58.68 (E(x771,f11(x771,x771))), % 58.51/58.68 inference(scs_inference,[],[55,60,68,71,28,63,24,41,35,36,42,43,56,57,2])). % 58.51/58.68 cnf(78,plain, % 58.51/58.68 (P3(f11(a7,a7),a9)), % 58.51/58.68 inference(scs_inference,[],[25,55,60,68,71,28,63,24,41,35,36,42,43,56,57,2,19])). % 58.51/58.68 cnf(79,plain, % 58.51/58.68 (~E(a9,a10)), % 58.51/58.68 inference(scs_inference,[],[25,31,55,60,68,71,28,63,24,41,35,36,42,43,56,57,2,19,20])). % 58.51/58.68 cnf(91,plain, % 58.51/58.68 (P2(x911,f11(x912,a1))), % 58.51/58.68 inference(scs_inference,[],[73,56,42])). % 58.51/58.68 cnf(92,plain, % 58.51/58.68 (~P4(x921,f11(x922,a1))), % 58.51/58.68 inference(rename_variables,[],[73])). % 58.51/58.68 cnf(94,plain, % 58.51/58.68 (P3(f11(x941,a1),x942)), % 58.51/58.68 inference(scs_inference,[],[73,92,56,42,41])). % 58.51/58.68 cnf(95,plain, % 58.51/58.68 (~P4(x951,f11(x952,a1))), % 58.51/58.68 inference(rename_variables,[],[73])). % 58.51/58.68 cnf(99,plain, % 58.51/58.68 (P2(f11(x991,a1),x992)), % 58.51/58.68 inference(scs_inference,[],[73,92,95,56,42,41,57,43])). % 58.51/58.68 cnf(102,plain, % 58.51/58.68 (P1(f11(a1,a1))), % 58.51/58.68 inference(scs_inference,[],[77,73,92,95,23,56,42,41,57,43,16])). % 58.51/58.68 cnf(103,plain, % 58.51/58.68 (E(x1031,f11(x1031,x1031))), % 58.51/58.68 inference(rename_variables,[],[77])). % 58.51/58.68 cnf(105,plain, % 58.51/58.68 (E(f11(x1051,x1052),f11(x1052,x1051))), % 58.51/58.68 inference(rename_variables,[],[29])). % 58.51/58.68 cnf(107,plain, % 58.51/58.68 (P3(a9,f11(a10,a10))), % 58.51/58.68 inference(scs_inference,[],[26,31,29,77,103,73,92,95,23,56,42,41,57,43,16,21,19,20])). % 58.51/58.68 cnf(108,plain, % 58.51/58.68 (E(x1081,f11(x1081,x1081))), % 58.51/58.68 inference(rename_variables,[],[77])). % 58.51/58.68 cnf(110,plain, % 58.51/58.68 (E(f11(x1101,x1102),f11(x1102,x1101))), % 58.51/58.68 inference(rename_variables,[],[29])). % 58.51/58.68 cnf(111,plain, % 58.51/58.68 (E(f11(x1111,x1112),f11(f11(x1112,x1111),f11(x1112,x1111)))), % 58.51/58.68 inference(scs_inference,[],[26,31,29,105,110,77,103,108,73,92,95,23,56,42,41,57,43,16,21,19,20,22,3])). % 58.51/58.68 cnf(113,plain, % 58.51/58.68 (E(f11(f11(x1131,x1132),f11(x1131,x1132)),f11(x1132,x1131))), % 58.51/58.68 inference(scs_inference,[],[26,31,29,105,110,77,103,108,73,92,95,23,56,42,41,57,43,16,21,19,20,22,3,2])). % 58.51/58.68 cnf(120,plain, % 58.51/58.68 (P3(f11(a1,x1201),x1202)), % 58.51/58.68 inference(scs_inference,[],[75,56,57,41])). % 58.51/58.68 cnf(123,plain, % 58.51/58.68 (P2(x1231,a2)), % 58.51/58.68 inference(scs_inference,[],[75,65,56,57,41,42])). % 58.51/58.68 cnf(124,plain, % 58.51/58.68 (~P4(x1241,a2)), % 58.51/58.68 inference(rename_variables,[],[65])). % 58.51/58.68 cnf(126,plain, % 58.51/58.68 (P2(a2,x1261)), % 58.51/58.68 inference(scs_inference,[],[75,65,124,56,57,41,42,43])). % 58.51/58.68 cnf(134,plain, % 58.51/58.68 (P3(x1341,x1341)), % 58.51/58.68 inference(rename_variables,[],[27])). % 58.51/58.68 cnf(137,plain, % 58.51/58.68 (~E(a9,f11(a10,a10))), % 58.51/58.68 inference(scs_inference,[],[31,79,27,134,75,28,111,65,124,77,102,56,57,41,42,43,16,21,19,20,3])). % 58.51/58.68 cnf(163,plain, % 58.51/58.68 (~P4(x1631,f11(x1632,a2))), % 58.51/58.68 inference(scs_inference,[],[65,56])). % 58.51/58.68 cnf(165,plain, % 58.51/58.68 (P2(x1651,f11(x1652,a2))), % 58.51/58.68 inference(scs_inference,[],[65,56,42])). % 58.51/58.68 cnf(168,plain, % 58.51/58.68 (~P4(x1681,a2)), % 58.51/58.68 inference(rename_variables,[],[65])). % 58.51/58.68 cnf(170,plain, % 58.51/58.68 (~E(f11(x1701,a1),a7)), % 58.51/58.68 inference(scs_inference,[],[31,94,65,56,42,57,19])). % 58.51/58.68 cnf(172,plain, % 58.51/58.68 (P3(f11(a7,a7),f11(a9,a9))), % 58.51/58.68 inference(scs_inference,[],[31,94,78,65,77,56,42,57,19,20])). % 58.51/58.68 cnf(183,plain, % 58.51/58.68 (~P1(a7)), % 58.51/58.68 inference(scs_inference,[],[31,94,78,29,113,137,65,168,77,102,56,42,57,19,20,22,3,41,52,33])). % 58.51/58.68 cnf(203,plain, % 58.51/58.68 (~P4(x2031,f11(x2032,f11(x2033,a2)))), % 58.51/58.68 inference(scs_inference,[],[163,56])). % 58.51/58.68 cnf(206,plain, % 58.51/58.68 (~P4(x2061,f11(x2062,a2))), % 58.51/58.68 inference(rename_variables,[],[163])). % 58.51/58.68 cnf(209,plain, % 58.51/58.68 (~P4(x2091,f11(x2092,a2))), % 58.51/58.68 inference(rename_variables,[],[163])). % 58.51/58.68 cnf(211,plain, % 58.51/58.68 (~P4(x2111,f11(f11(x2112,a2),x2113))), % 58.51/58.68 inference(scs_inference,[],[163,206,209,56,41,43,57])). % 58.51/58.68 cnf(216,plain, % 58.51/58.68 (E(f11(x2161,x2162),f11(x2162,x2161))), % 58.51/58.68 inference(rename_variables,[],[29])). % 58.51/58.68 cnf(221,plain, % 58.51/58.68 (P2(x2211,f11(x2212,f11(x2213,a2)))), % 58.51/58.68 inference(scs_inference,[],[31,120,29,216,137,163,206,209,56,41,43,57,19,21,42,33,22])). % 58.51/58.68 cnf(225,plain, % 58.51/58.68 (~P4(x2251,f11(a2,x2252))), % 58.51/58.68 inference(scs_inference,[],[65,57])). % 58.51/58.68 cnf(230,plain, % 58.51/58.68 (E(f11(x2301,x2302),f11(f11(x2302,x2301),f11(x2302,x2301)))), % 58.51/58.68 inference(rename_variables,[],[111])). % 58.51/58.68 cnf(231,plain, % 58.51/58.68 (P2(f11(f11(a1,x2311),f11(a1,x2311)),x2312)), % 58.51/58.68 inference(scs_inference,[],[172,111,230,99,65,57,41,20,21])). % 58.51/58.68 cnf(245,plain, % 58.51/58.68 (P2(f11(x2451,f11(a2,x2452)),x2453)), % 58.51/58.68 inference(scs_inference,[],[225,56,43])). % 58.51/58.68 cnf(248,plain, % 58.51/58.68 (E(x2481,f11(x2481,x2481))), % 58.51/58.68 inference(rename_variables,[],[77])). % 58.51/58.68 cnf(250,plain, % 58.51/58.68 (E(x2501,f11(x2501,x2501))), % 58.51/58.68 inference(rename_variables,[],[77])). % 58.51/58.68 cnf(251,plain, % 58.51/58.68 (P2(x2511,f11(f11(x2512,a1),f11(x2512,a1)))), % 58.51/58.68 inference(scs_inference,[],[107,77,248,250,99,91,225,56,43,20,21,22])). % 58.51/58.68 cnf(252,plain, % 58.51/58.68 (E(x2521,f11(x2521,x2521))), % 58.51/58.68 inference(rename_variables,[],[77])). % 58.51/58.68 cnf(253,plain, % 58.51/58.68 (P3(f11(a9,a9),f11(a10,a10))), % 58.51/58.68 inference(scs_inference,[],[107,77,248,250,252,99,91,225,56,43,20,21,22,19])). % 58.51/58.68 cnf(257,plain, % 58.51/58.68 (P2(f11(f11(a2,x2571),x2572),x2573)), % 58.51/58.68 inference(scs_inference,[],[225,57,43])). % 58.51/58.68 cnf(259,plain, % 58.51/58.68 (P3(f11(a9,a9),a10)), % 58.51/58.68 inference(scs_inference,[],[253,28,225,57,43,20])). % 58.51/58.68 cnf(267,plain, % 58.51/58.68 (P3(a7,f11(a9,a9))), % 58.51/58.68 inference(scs_inference,[],[172,28,19])). % 58.51/58.68 cnf(278,plain, % 58.51/58.68 (~E(f11(a9,a9),a7)), % 58.51/58.68 inference(scs_inference,[],[31,259,19])). % 58.51/58.68 cnf(279,plain, % 58.51/58.68 (E(f11(a1,x2791),a1)), % 58.51/58.68 inference(scs_inference,[],[67,39,37])). % 58.51/58.68 cnf(280,plain, % 58.51/58.68 (E(a1,f11(a1,x2801))), % 58.51/58.68 inference(scs_inference,[],[279,2])). % 58.51/58.68 cnf(281,plain, % 58.51/58.68 (P1(f11(a1,x2811))), % 58.51/58.68 inference(scs_inference,[],[23,279,2,16])). % 58.51/58.68 cnf(282,plain, % 58.51/58.68 (E(f11(x2821,a1),a1)), % 58.51/58.68 inference(scs_inference,[],[23,29,279,2,16,3])). % 58.51/58.68 cnf(285,plain, % 58.51/58.68 (E(a1,f11(x2851,a1))), % 58.51/58.68 inference(scs_inference,[],[282,2])). % 58.51/58.68 cnf(286,plain, % 58.51/58.68 (P1(f11(x2861,a1))), % 58.51/58.68 inference(scs_inference,[],[23,282,2,16])). % 58.51/58.68 cnf(287,plain, % 58.51/58.68 (E(f11(a1,a1),f11(a1,x2871))), % 58.51/58.68 inference(scs_inference,[],[23,28,280,282,2,16,3])). % 58.51/58.68 cnf(291,plain, % 58.51/58.68 (~P1(f11(a7,a7))), % 58.51/58.68 inference(scs_inference,[],[28,287,183,2,16])). % 58.51/58.68 cnf(292,plain, % 58.51/58.68 (E(f11(x2921,x2921),x2921)), % 58.51/58.68 inference(rename_variables,[],[28])). % 58.51/58.68 cnf(293,plain, % 58.51/58.68 (E(f11(a1,a1),f11(x2931,a1))), % 58.51/58.68 inference(scs_inference,[],[28,292,287,285,183,2,16,3])). % 58.51/58.68 cnf(298,plain, % 58.51/58.68 (E(f11(f11(x2981,x2982),f11(x2981,x2982)),f11(x2982,x2981))), % 58.51/58.68 inference(rename_variables,[],[113])). % 58.51/58.68 cnf(299,plain, % 58.51/58.68 (E(f11(f11(a1,x2991),f11(a1,x2991)),a1)), % 58.51/58.68 inference(scs_inference,[],[113,298,293,282,291,2,16,3])). % 58.51/58.68 cnf(302,plain, % 58.51/58.68 (E(f11(f11(x3021,a1),x3022),f11(a1,x3022))), % 58.51/58.68 inference(scs_inference,[],[73,34,4])). % 58.51/58.68 cnf(303,plain, % 58.51/58.68 (E(f11(a1,x3031),f11(f11(x3032,a1),x3031))), % 58.51/58.68 inference(scs_inference,[],[302,2])). % 58.51/58.68 cnf(305,plain, % 58.51/58.68 (E(f11(x3051,f11(x3052,a1)),f11(a1,x3051))), % 58.51/58.68 inference(scs_inference,[],[29,302,281,2,16,3])). % 58.51/58.68 cnf(309,plain, % 58.51/58.68 (E(f11(a1,x3091),f11(x3091,f11(x3092,a1)))), % 58.51/58.68 inference(scs_inference,[],[305,2])). % 58.51/58.68 cnf(315,plain, % 58.64/58.68 (E(f11(x3151,a1),f11(f11(x3152,a1),x3151))), % 58.64/58.68 inference(scs_inference,[],[23,29,303,299,2,16,3])). % 58.64/58.68 cnf(318,plain, % 58.64/58.68 (~P4(f5(f11(a7,a7),a10),a10)), % 58.64/58.68 inference(scs_inference,[],[31,28,48,19])). % 58.64/58.68 cnf(323,plain, % 58.64/58.68 (E(f11(f11(x3231,a1),x3232),f11(x3232,a1))), % 58.64/58.68 inference(scs_inference,[],[318,315,56,57,2])). % 58.64/58.68 cnf(346,plain, % 58.64/58.68 (E(f11(x3461,f11(x3462,a1)),f11(x3461,a1))), % 58.64/58.68 inference(scs_inference,[],[29,309,3,2])). % 58.64/58.68 cnf(560,plain, % 58.64/58.68 (~E(f11(x5601,a1),f11(a7,a7))), % 58.64/58.68 inference(scs_inference,[],[170,28,3])). % 58.64/58.68 cnf(565,plain, % 58.64/58.68 (~E(a7,f11(x5651,a2))), % 58.64/58.68 inference(scs_inference,[],[170,163,75,28,3,53,18])). % 58.64/58.68 cnf(567,plain, % 58.64/58.68 (P4(f6(a7,a7,f11(a1,a1)),f11(a7,a7))), % 58.64/58.68 inference(scs_inference,[],[170,163,75,29,28,3,53,18,50])). % 58.64/58.68 cnf(570,plain, % 58.64/58.68 (~P2(a7,a7)), % 58.64/58.68 inference(scs_inference,[],[170,163,75,29,28,3,53,18,50,51])). % 58.64/58.68 cnf(574,plain, % 58.64/58.68 (~P2(f11(a7,a7),f11(a7,a7))), % 58.64/58.68 inference(scs_inference,[],[170,163,75,29,28,3,53,18,50,51,40,47])). % 58.64/58.68 cnf(576,plain, % 58.64/58.68 (P4(f6(a7,a7,f11(a1,a1)),a9)), % 58.64/58.68 inference(scs_inference,[],[170,25,163,75,29,28,3,53,18,50,51,40,47,44])). % 58.64/58.68 cnf(578,plain, % 58.64/58.68 (P4(f6(x5781,a2,a7),a7)), % 58.64/58.68 inference(scs_inference,[],[170,25,163,75,29,28,65,3,53,18,50,51,40,47,44,52])). % 58.64/58.68 cnf(581,plain, % 58.64/58.68 (P4(f11(f6(x5811,a2,a7),f6(x5811,a2,a7)),a7)), % 58.64/58.68 inference(scs_inference,[],[170,25,163,75,29,28,77,65,3,53,18,50,51,40,47,44,52,17])). % 58.64/58.68 cnf(591,plain, % 58.64/58.68 (~P2(a9,a9)), % 58.64/58.68 inference(scs_inference,[],[576,40,47])). % 58.64/58.68 cnf(593,plain, % 58.64/58.68 (P4(f6(a7,a7,f11(a1,a1)),a10)), % 58.64/58.68 inference(scs_inference,[],[26,576,40,47,44])). % 58.64/58.68 cnf(595,plain, % 58.64/58.68 (~E(a9,f11(x5951,a2))), % 58.64/58.68 inference(scs_inference,[],[26,576,163,40,47,44,18])). % 58.64/58.68 cnf(596,plain, % 58.64/58.68 (~P4(x5961,f11(x5962,a2))), % 58.64/58.68 inference(rename_variables,[],[163])). % 58.64/58.68 cnf(604,plain, % 58.64/58.68 (P4(f6(a7,a7,f11(a1,a1)),f11(a9,a9))), % 58.64/58.68 inference(scs_inference,[],[26,576,163,29,280,123,70,574,565,40,47,44,18,21,22,3,50])). % 58.64/58.68 cnf(607,plain, % 58.64/58.68 (P4(f3(a7),a7)), % 58.64/58.68 inference(scs_inference,[],[26,576,163,29,280,123,70,574,565,40,47,44,18,21,22,3,50,34])). % 58.64/58.68 cnf(612,plain, % 58.64/58.68 (P4(f6(a7,a7,a1),a7)), % 58.64/58.68 inference(scs_inference,[],[26,576,163,596,29,280,55,123,70,574,565,40,47,44,18,21,22,3,50,34,53,52])). % 58.64/58.68 cnf(622,plain, % 58.64/58.68 (~P2(a10,a10)), % 58.64/58.68 inference(scs_inference,[],[593,40,47])). % 58.64/58.68 cnf(624,plain, % 58.64/58.68 (P4(f11(f6(x6241,a2,a7),f6(x6241,a2,a7)),a9)), % 58.64/58.68 inference(scs_inference,[],[25,593,581,40,47,44])). % 58.64/58.68 cnf(626,plain, % 58.64/58.68 (P4(f6(a7,a7,f11(x6261,a1)),a7)), % 58.64/58.68 inference(scs_inference,[],[25,593,73,560,581,40,47,44,53])). % 58.64/58.68 cnf(628,plain, % 58.64/58.68 (~P4(x6281,f11(x6282,a1))), % 58.64/58.68 inference(rename_variables,[],[73])). % 58.64/58.68 cnf(630,plain, % 58.64/58.68 (P4(f6(x6301,a2,a9),a9)), % 58.64/58.68 inference(scs_inference,[],[25,593,73,65,560,581,595,40,47,44,53,52])). % 58.64/58.68 cnf(633,plain, % 58.64/58.68 (~P1(a9)), % 58.64/58.68 inference(scs_inference,[],[25,593,73,65,560,581,595,281,40,47,44,53,52,33])). % 58.64/58.68 cnf(634,plain, % 58.64/58.68 (~E(a9,f11(x6341,a2))), % 58.64/58.68 inference(rename_variables,[],[595])). % 58.64/58.68 cnf(637,plain, % 58.64/58.68 (P4(f11(f6(a7,a7,a1),f6(a7,a7,a1)),a7)), % 58.64/58.68 inference(scs_inference,[],[25,593,73,65,77,560,581,595,612,281,40,47,44,53,52,33,17])). % 58.64/58.68 cnf(639,plain, % 58.64/58.68 (~E(a10,f11(x6391,a1))), % 58.64/58.68 inference(scs_inference,[],[25,593,73,628,65,77,560,581,595,612,281,40,47,44,53,52,33,17,18])). % 58.64/58.68 cnf(645,plain, % 58.64/58.68 (~E(a9,f11(a1,a1))), % 58.64/58.68 inference(scs_inference,[],[25,593,73,628,287,65,77,257,560,581,570,595,634,612,281,221,40,47,44,53,52,33,17,18,21,22,3])). % 58.64/58.68 cnf(648,plain, % 58.64/58.68 (P4(f6(a7,a7,f11(a1,a1)),f11(a10,a10))), % 58.64/58.68 inference(scs_inference,[],[25,593,73,628,29,287,65,77,257,560,581,570,595,634,612,281,221,40,47,44,53,52,33,17,18,21,22,3,50])). % 58.64/58.68 cnf(655,plain, % 58.64/58.68 (~P2(f11(a10,a10),f11(a10,a10))), % 58.64/58.68 inference(scs_inference,[],[624,648,40,47])). % 58.64/58.68 cnf(659,plain, % 58.64/58.68 (P4(f11(f6(x6591,a2,a7),f6(x6591,a2,a7)),a10)), % 58.64/58.68 inference(scs_inference,[],[26,624,648,40,47,58,44])). % 58.64/58.68 cnf(661,plain, % 58.64/58.68 (P4(f6(a1,a1,a9),a9)), % 58.64/58.68 inference(scs_inference,[],[26,624,55,648,645,40,47,58,44,53])). % 58.64/58.68 cnf(662,plain, % 58.64/58.68 (~P4(x6621,a1)), % 58.64/58.68 inference(rename_variables,[],[55])). % 58.64/58.68 cnf(664,plain, % 58.64/58.68 (P4(f6(x6641,a1,a10),a10)), % 58.64/58.68 inference(scs_inference,[],[26,624,55,662,648,645,639,40,47,58,44,53,52])). % 58.64/58.68 cnf(667,plain, % 58.64/58.68 (~P1(a10)), % 58.64/58.68 inference(scs_inference,[],[26,624,55,662,648,645,639,286,40,47,58,44,53,52,33])). % 58.64/58.68 cnf(670,plain, % 58.64/58.68 (P4(f11(f6(x6701,a2,a9),f6(x6701,a2,a9)),a9)), % 58.64/58.68 inference(scs_inference,[],[26,624,55,662,77,648,645,639,630,286,40,47,58,44,53,52,33,17])). % 58.64/58.68 cnf(672,plain, % 58.64/58.68 (~E(a9,f11(x6721,a1))), % 58.64/58.68 inference(scs_inference,[],[26,624,73,55,662,77,648,645,639,630,286,40,47,58,44,53,52,33,17,18])). % 58.64/58.68 cnf(674,plain, % 58.64/58.68 (~E(f11(x6741,a1),a9)), % 58.64/58.68 inference(scs_inference,[],[26,624,73,55,662,77,99,648,591,645,639,630,286,40,47,58,44,53,52,33,17,18,21])). % 58.64/58.68 cnf(678,plain, % 58.64/58.68 (~P1(f11(a9,a9))), % 58.64/58.68 inference(scs_inference,[],[26,624,73,28,55,662,77,99,67,648,591,645,639,630,633,286,40,47,58,44,53,52,33,17,18,21,22,16])). % 58.64/58.68 cnf(682,plain, % 58.64/58.68 (P4(f11(f6(x6821,a2,a7),f6(x6821,a2,a7)),f11(a9,a9))), % 58.64/58.68 inference(scs_inference,[],[26,624,73,29,28,285,55,662,77,99,67,648,591,645,639,630,633,286,40,47,58,44,53,52,33,17,18,21,22,16,3,50])). % 58.64/58.68 cnf(685,plain, % 58.64/58.68 (P4(f3(a9),a9)), % 58.64/58.68 inference(scs_inference,[],[26,624,73,29,28,285,55,662,77,99,67,648,591,645,639,630,633,286,40,47,58,44,53,52,33,17,18,21,22,16,3,50,34])). % 58.64/58.68 cnf(693,plain, % 58.64/58.68 (~P2(f11(a9,a9),f11(a9,a9))), % 58.64/58.68 inference(scs_inference,[],[659,604,40,47])). % 58.64/58.68 cnf(697,plain, % 58.64/58.68 (P4(f6(x6971,a2,a7),a9)), % 58.64/58.68 inference(scs_inference,[],[25,659,578,604,40,47,58,44])). % 58.64/58.68 cnf(700,plain, % 58.64/58.68 (~E(a9,f11(x7001,a1))), % 58.64/58.68 inference(rename_variables,[],[672])). % 58.64/58.68 cnf(701,plain, % 58.64/58.68 (~P4(x7011,f11(x7012,a1))), % 58.64/58.68 inference(rename_variables,[],[73])). % 58.64/58.68 cnf(703,plain, % 58.64/58.68 (P4(f6(x7031,a1,a9),a9)), % 58.64/58.68 inference(scs_inference,[],[25,659,73,55,578,604,672,700,40,47,58,44,53,52])). % 58.64/58.68 cnf(706,plain, % 58.64/58.68 (P4(f11(f6(a1,a1,a9),f6(a1,a1,a9)),a9)), % 58.64/58.68 inference(scs_inference,[],[25,659,73,55,77,578,604,661,672,700,40,47,58,44,53,52,17])). % 58.64/58.68 cnf(708,plain, % 58.64/58.68 (~E(f11(a7,a7),f11(x7081,a1))), % 58.64/58.68 inference(scs_inference,[],[25,659,73,701,55,77,567,578,604,661,672,700,40,47,58,44,53,52,17,18])). % 58.64/58.68 cnf(710,plain, % 58.64/58.68 (~E(f11(x7101,a1),f11(a10,a10))), % 58.64/58.68 inference(scs_inference,[],[25,659,73,701,55,77,99,567,578,655,604,661,672,700,40,47,58,44,53,52,17,18,21])). % 58.64/58.68 cnf(716,plain, % 58.64/58.68 (~E(a9,f11(a1,f11(x7161,a1)))), % 58.64/58.68 inference(scs_inference,[],[25,659,73,701,113,305,55,77,99,67,567,578,655,604,661,672,700,678,40,47,58,44,53,52,17,18,21,22,16,3])). % 58.64/58.68 cnf(719,plain, % 58.64/58.68 (P4(f11(f6(x7191,a2,a7),f6(x7191,a2,a7)),f11(a10,a10))), % 58.64/58.68 inference(scs_inference,[],[25,659,73,701,29,113,305,55,77,99,67,567,578,655,604,661,672,700,678,40,47,58,44,53,52,17,18,21,22,16,3,50])). % 58.64/58.68 cnf(727,plain, % 58.64/58.68 (~P1(f11(a10,a10))), % 58.64/58.68 inference(scs_inference,[],[25,659,73,701,29,113,305,55,77,99,67,567,578,655,604,661,672,700,286,678,40,47,58,44,53,52,17,18,21,22,16,3,50,5,56,57,33])). % 58.64/58.68 cnf(734,plain, % 58.64/58.68 (~P4(x7341,a1)), % 58.64/58.68 inference(rename_variables,[],[55])). % 58.64/58.68 cnf(736,plain, % 58.64/58.68 (P4(f6(x7361,a2,a7),a10)), % 58.64/58.68 inference(scs_inference,[],[26,697,55,567,708,40,52,44])). % 58.64/58.68 cnf(741,plain, % 58.64/58.68 (P4(f11(f3(a9),f3(a9)),a9)), % 58.64/58.68 inference(scs_inference,[],[26,697,55,734,77,567,685,708,716,40,52,44,53,17])). % 58.64/58.68 cnf(743,plain, % 58.64/58.68 (~E(a7,f11(x7431,a1))), % 58.64/58.68 inference(scs_inference,[],[26,697,73,55,734,77,567,581,685,708,716,40,52,44,53,17,18])). % 58.64/58.68 cnf(751,plain, % 58.64/58.68 (~E(f11(a7,a7),a1)), % 58.64/58.68 inference(scs_inference,[],[26,697,73,113,285,55,734,77,91,126,567,581,693,727,685,708,716,40,52,44,53,17,18,21,22,16,3])). % 58.64/58.68 cnf(753,plain, % 58.64/58.68 (P4(f6(x7531,a2,a7),f11(a9,a9))), % 58.64/58.68 inference(scs_inference,[],[26,697,73,29,113,285,55,734,77,91,126,567,581,693,727,685,708,716,40,52,44,53,17,18,21,22,16,3,50])). % 58.64/58.68 cnf(756,plain, % 58.64/58.68 (P4(f3(f11(a7,a7)),f11(a7,a7))), % 58.64/58.68 inference(scs_inference,[],[26,697,73,29,113,285,55,734,77,91,126,567,581,693,727,685,708,716,40,52,44,53,17,18,21,22,16,3,50,34])). % 58.64/58.68 cnf(763,plain, % 58.64/58.68 (P4(f6(x7631,a1,a7),a7)), % 58.64/58.68 inference(scs_inference,[],[55,578,743,40,57,52])). % 58.64/58.68 cnf(766,plain, % 58.64/58.68 (P4(f3(a7),a9)), % 58.64/58.68 inference(scs_inference,[],[25,55,578,607,743,40,57,52,44])). % 58.64/58.68 cnf(770,plain, % 58.64/58.68 (~P4(x7701,f11(x7702,a1))), % 58.64/58.68 inference(rename_variables,[],[73])). % 58.64/58.68 cnf(773,plain, % 58.64/58.68 (~E(f11(a9,a9),f11(x7731,a1))), % 58.64/58.68 inference(scs_inference,[],[25,318,736,73,770,55,578,607,682,743,710,40,57,52,44,53,17,18])). % 58.64/58.68 cnf(779,plain, % 58.64/58.68 (~E(a9,f11(f11(x7791,a1),f11(x7792,a1)))), % 58.64/58.68 inference(scs_inference,[],[25,318,736,73,770,302,55,123,99,716,578,622,607,682,743,710,40,57,52,44,53,17,18,21,22,3])). % 58.64/58.68 cnf(796,plain, % 58.64/58.68 (~P4(x7961,f11(a1,x7962))), % 58.64/58.68 inference(rename_variables,[],[75])). % 58.64/58.68 cnf(798,plain, % 58.64/58.68 (P4(f3(a7),a10)), % 58.64/58.68 inference(scs_inference,[],[26,766,75,55,773,779,40,52,53,44])). % 58.64/58.68 cnf(808,plain, % 58.64/58.68 (~E(f11(a7,a7),f11(a1,f11(x8081,a1)))), % 58.64/58.68 inference(scs_inference,[],[26,659,766,75,796,305,77,55,165,245,708,773,779,574,40,52,53,44,17,18,21,22,3])). % 58.64/58.68 cnf(819,plain, % 58.64/58.68 (~E(f11(a7,a7),f11(a1,f11(x8191,a1)))), % 58.64/58.68 inference(rename_variables,[],[808])). % 58.64/58.68 cnf(820,plain, % 58.64/58.68 (~P4(x8201,f11(a1,x8202))), % 58.64/58.68 inference(rename_variables,[],[75])). % 58.64/58.68 cnf(825,plain, % 58.64/58.68 (P4(f11(f6(a7,a7,a1),f6(a7,a7,a1)),a9)), % 58.64/58.68 inference(scs_inference,[],[25,798,75,55,637,808,819,40,52,53,44])). % 58.64/58.68 cnf(828,plain, % 58.64/58.68 (~E(a9,f11(a1,x8281))), % 58.64/58.68 inference(scs_inference,[],[25,318,697,798,75,820,55,637,808,819,40,52,53,44,17,18])). % 58.64/58.68 cnf(834,plain, % 58.64/58.68 (~E(f11(a7,a7),f11(f11(x8341,a1),x8342))), % 58.64/58.69 inference(scs_inference,[],[25,318,697,798,75,820,323,55,126,165,708,637,808,819,591,40,52,53,44,17,18,21,22,3])). % 58.64/58.69 cnf(851,plain, % 58.64/58.69 (~P4(x8511,f11(x8512,a1))), % 58.64/58.69 inference(rename_variables,[],[73])). % 58.64/58.69 cnf(853,plain, % 58.64/58.69 (P4(f6(f11(x8531,a1),x8532,f11(a7,a7)),f11(a7,a7))), % 58.64/58.69 inference(scs_inference,[],[825,73,851,779,834,40,58,52,53])). % 58.64/58.69 cnf(857,plain, % 58.64/58.69 (P4(f11(f6(a7,a7,a1),f6(a7,a7,a1)),a10)), % 58.64/58.69 inference(scs_inference,[],[26,825,73,851,779,834,40,58,52,53,44])). % 58.64/58.69 cnf(866,plain, % 58.64/58.69 (~E(f11(a7,a7),f11(x8661,f11(x8662,a1)))), % 58.64/58.69 inference(scs_inference,[],[26,318,736,825,163,73,851,346,708,664,779,834,570,231,251,40,58,52,53,44,17,18,21,22,3])). % 58.64/58.69 cnf(883,plain, % 58.64/58.69 (~E(f11(a7,a7),f11(x8831,f11(x8832,a1)))), % 58.64/58.69 inference(rename_variables,[],[866])). % 58.64/58.69 cnf(884,plain, % 58.64/58.69 (~P4(x8841,f11(a1,x8842))), % 58.64/58.69 inference(rename_variables,[],[75])). % 58.64/58.69 cnf(888,plain, % 58.64/58.69 (~P4(x8881,f11(a1,x8882))), % 58.64/58.69 inference(rename_variables,[],[75])). % 58.64/58.69 cnf(890,plain, % 58.64/58.69 (P4(f11(f6(a1,a1,a9),f6(a1,a1,a9)),a10)), % 58.64/58.69 inference(scs_inference,[],[26,857,75,884,706,866,883,40,58,52,53,44])). % 58.64/58.69 cnf(894,plain, % 58.64/58.69 (~E(f11(a7,a7),f11(a1,x8941))), % 58.64/58.69 inference(scs_inference,[],[26,857,75,884,888,77,567,706,703,866,883,40,58,52,53,44,17,18])). % 58.64/58.69 cnf(900,plain, % 58.64/58.69 (~E(f11(a7,a7),f11(f11(a1,x9001),f11(a1,x9001)))), % 58.64/58.69 inference(scs_inference,[],[26,857,75,884,888,77,299,126,751,165,567,706,703,866,883,655,40,58,52,53,44,17,18,21,22,3])). % 58.64/58.69 cnf(912,plain, % 58.64/58.69 (~P4(x9121,f11(a1,x9122))), % 58.64/58.69 inference(rename_variables,[],[75])). % 58.64/58.69 cnf(914,plain, % 58.64/58.69 (P4(f11(f3(a9),f3(a9)),a10)), % 58.64/58.69 inference(scs_inference,[],[26,890,75,741,900,40,58,52,44])). % 58.64/58.69 cnf(921,plain, % 58.64/58.69 (~E(f11(a10,a10),f11(a1,x9211))), % 58.64/58.69 inference(scs_inference,[],[26,890,75,912,77,55,719,741,763,900,894,40,58,52,44,53,17,18])). % 58.64/58.69 cnf(928,plain, % 58.64/58.69 (P4(f3(a10),a10)), % 58.64/58.69 inference(scs_inference,[],[26,890,75,912,77,55,165,257,719,741,763,900,894,622,40,58,52,44,53,17,18,21,22,4,34])). % 58.64/58.69 cnf(940,plain, % 58.64/58.69 (~E(a9,f11(a1,x9401))), % 58.64/58.69 inference(rename_variables,[],[828])). % 58.64/58.69 cnf(941,plain, % 58.64/58.69 (~P4(x9411,f11(a1,x9412))), % 58.64/58.69 inference(rename_variables,[],[75])). % 58.64/58.69 cnf(943,plain, % 58.64/58.69 (P4(f6(a1,x9431,a9),a9)), % 58.64/58.69 inference(scs_inference,[],[914,75,55,828,940,40,58,52,53])). % 58.64/58.69 cnf(946,plain, % 58.64/58.69 (P4(f11(f6(x9461,a2,a9),f6(x9461,a2,a9)),a10)), % 58.64/58.69 inference(scs_inference,[],[26,914,75,55,670,828,940,40,58,52,53,44])). % 58.64/58.69 cnf(951,plain, % 58.64/58.69 (~E(a1,f11(a9,a9))), % 58.64/58.69 inference(scs_inference,[],[26,318,914,75,941,55,70,753,670,828,940,928,693,40,58,52,53,44,17,18,21])). % 58.64/58.69 cnf(972,plain, % 58.64/58.69 (P4(f6(a1,x9721,f11(a10,a10)),f11(a10,a10))), % 58.64/58.69 inference(scs_inference,[],[25,946,73,55,866,626,921,40,58,52,44,53])). % 58.64/58.69 cnf(979,plain, % 58.64/58.69 (~E(a7,a2)), % 58.64/58.69 inference(scs_inference,[],[25,946,163,73,77,55,567,866,626,921,943,40,58,52,44,53,17,18,5])). % 58.64/58.69 cnf(1290,plain, % 58.64/58.69 (P4(f6(a9,a9,a1),a9)), % 58.64/58.69 inference(scs_inference,[],[55,853,951,40,52])). % 58.64/58.69 cnf(1390,plain, % 58.64/58.69 (P4(f6(a9,a9,a1),a10)), % 58.64/58.69 inference(scs_inference,[],[26,972,1290,40,44])). % 58.64/58.69 cnf(1396,plain, % 58.64/58.69 (~P4(a10,f6(a9,a9,a1))), % 58.64/58.69 inference(scs_inference,[],[1390,40])). % 58.64/58.69 cnf(1583,plain, % 58.64/58.69 (P4(f3(f11(a7,a7)),f11(a9,a9))), % 58.64/58.69 inference(scs_inference,[],[172,756,44])). % 58.64/58.69 cnf(1713,plain, % 58.64/58.69 (~E(a9,f11(x17131,f11(x17132,a2)))), % 58.64/58.69 inference(scs_inference,[],[203,697,18])). % 58.64/58.69 cnf(1718,plain, % 58.64/58.69 (P4(f6(x17181,f11(a1,a2),a9),a10)), % 58.64/58.69 inference(scs_inference,[],[203,26,697,75,18,52,44])). % 58.64/58.69 cnf(1725,plain, % 58.64/58.69 (~E(a10,f11(x17251,f11(x17252,a2)))), % 58.64/58.69 inference(scs_inference,[],[203,736,1718,40,18])). % 58.64/58.69 cnf(1727,plain, % 58.64/58.69 (P4(f6(x17271,f11(a1,a2),a10),a10)), % 58.64/58.69 inference(scs_inference,[],[203,736,1718,75,40,18,52])). % 58.64/58.69 cnf(1733,plain, % 58.64/58.69 (~E(f11(a9,a9),f11(x17331,f11(x17332,a2)))), % 58.64/58.69 inference(scs_inference,[],[203,1583,1727,40,18])). % 58.64/58.69 cnf(1741,plain, % 58.64/58.69 (~E(f11(a7,a7),f11(x17411,f11(x17412,a2)))), % 58.64/58.69 inference(scs_inference,[],[203,75,567,1733,52,18])). % 58.64/58.69 cnf(1749,plain, % 58.64/58.69 (~E(f11(a10,a10),f11(x17491,f11(x17492,a2)))), % 58.64/58.69 inference(scs_inference,[],[203,75,719,1741,52,18])). % 58.64/58.69 cnf(1757,plain, % 58.64/58.69 (~E(a7,f11(x17571,f11(x17572,a2)))), % 58.64/58.69 inference(scs_inference,[],[203,75,578,1749,52,18])). % 58.64/58.69 cnf(1840,plain, % 58.64/58.69 (~E(a9,f11(f11(x18401,a2),x18402))), % 58.64/58.69 inference(scs_inference,[],[211,697,18])). % 58.64/58.69 cnf(1843,plain, % 58.64/58.69 (~E(a10,f11(f11(x18431,a2),x18432))), % 58.64/58.69 inference(scs_inference,[],[211,736,18])). % 58.64/58.69 cnf(1846,plain, % 58.64/58.69 (~E(f11(a9,a9),f11(f11(x18461,a2),x18462))), % 58.64/58.69 inference(scs_inference,[],[211,1583,18])). % 58.64/58.69 cnf(1849,plain, % 58.64/58.69 (~E(f11(a7,a7),f11(f11(x18491,a2),x18492))), % 58.64/58.69 inference(scs_inference,[],[211,567,18])). % 58.64/58.69 cnf(1852,plain, % 58.64/58.69 (~E(f11(a10,a10),f11(f11(x18521,a2),x18522))), % 58.64/58.69 inference(scs_inference,[],[211,648,18])). % 58.64/58.69 cnf(1855,plain, % 58.64/58.69 (~E(a7,f11(f11(x18551,a2),x18552))), % 58.64/58.69 inference(scs_inference,[],[211,581,18])). % 58.64/58.69 cnf(1989,plain, % 58.64/58.69 (~E(a9,f11(x19891,f11(x19892,a2)))), % 58.64/58.69 inference(rename_variables,[],[1713])). % 58.64/58.69 cnf(1990,plain, % 58.64/58.69 (~P4(x19901,f11(a2,x19902))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(1992,plain, % 58.64/58.69 (P4(f6(f11(a2,x19921),f11(x19922,a2),a9),a9)), % 58.64/58.69 inference(scs_inference,[],[225,1990,1713,1989,52,53])). % 58.64/58.69 cnf(1994,plain, % 58.64/58.69 (~P4(x19941,f11(a2,x19942))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(1996,plain, % 58.64/58.69 (P4(f6(x19961,f11(a2,a2),a9),a10)), % 58.64/58.69 inference(scs_inference,[],[225,1990,26,1713,1989,52,53,44])). % 58.64/58.69 cnf(1998,plain, % 58.64/58.69 (~E(a7,f11(a2,x19981))), % 58.64/58.69 inference(scs_inference,[],[225,1990,1994,26,1713,1989,578,52,53,44,18])). % 58.64/58.69 cnf(2006,plain, % 58.64/58.69 (~E(a10,f11(x20061,f11(x20062,a2)))), % 58.64/58.69 inference(rename_variables,[],[1725])). % 58.64/58.69 cnf(2007,plain, % 58.64/58.69 (~P4(x20071,f11(a2,x20072))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(2013,plain, % 58.64/58.69 (P4(f6(f11(a2,x20131),f11(x20132,a2),a9),a10)), % 58.64/58.69 inference(scs_inference,[],[225,2007,26,1996,1725,2006,1992,40,52,53,44])). % 58.64/58.69 cnf(2020,plain, % 58.64/58.69 (P4(f6(x20201,f11(a2,a2),f11(a9,a9)),f11(a9,a9))), % 58.64/58.69 inference(scs_inference,[],[225,2013,1733,40,52])). % 58.64/58.69 cnf(2033,plain, % 58.64/58.69 (P4(f6(x20331,f11(a2,a2),f11(a7,a7)),f11(a7,a7))), % 58.64/58.69 inference(scs_inference,[],[225,1741,2020,40,52])). % 58.64/58.69 cnf(2044,plain, % 58.64/58.69 (P4(f6(x20441,f11(a2,a2),f11(a10,a10)),f11(a10,a10))), % 58.64/58.69 inference(scs_inference,[],[225,1749,2033,40,52])). % 58.64/58.69 cnf(2056,plain, % 58.64/58.69 (~E(a7,f11(x20561,f11(x20562,a2)))), % 58.64/58.69 inference(rename_variables,[],[1757])). % 58.64/58.69 cnf(2057,plain, % 58.64/58.69 (~P4(x20571,f11(a2,x20572))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(2059,plain, % 58.64/58.69 (P4(f6(f11(a2,x20591),f11(x20592,a2),a7),a7)), % 58.64/58.69 inference(scs_inference,[],[225,2057,1757,2056,2044,40,52,53])). % 58.64/58.69 cnf(2063,plain, % 58.64/58.69 (P4(f6(x20631,f11(a2,a2),a7),a9)), % 58.64/58.69 inference(scs_inference,[],[225,2057,25,1757,2056,2044,40,52,53,44])). % 58.64/58.69 cnf(2068,plain, % 58.64/58.69 (~E(f11(a9,a9),f11(f11(x20681,a2),x20682))), % 58.64/58.69 inference(rename_variables,[],[1846])). % 58.64/58.69 cnf(2069,plain, % 58.64/58.69 (~P4(x20691,f11(a2,x20692))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(2075,plain, % 58.64/58.69 (P4(f6(x20751,f11(a2,a2),a7),a10)), % 58.64/58.69 inference(scs_inference,[],[225,2069,26,2063,1846,2068,40,52,53,44])). % 58.64/58.69 cnf(2080,plain, % 58.64/58.69 (~E(f11(a7,a7),f11(f11(x20801,a2),x20802))), % 58.64/58.69 inference(rename_variables,[],[1849])). % 58.64/58.69 cnf(2081,plain, % 58.64/58.69 (~P4(x20811,f11(a2,x20812))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(2087,plain, % 58.64/58.69 (P4(f6(f11(a2,x20871),f11(x20872,a2),a7),a9)), % 58.64/58.69 inference(scs_inference,[],[225,2081,25,2075,1849,2080,2059,40,52,53,44])). % 58.64/58.69 cnf(2092,plain, % 58.64/58.69 (~E(f11(a10,a10),f11(f11(x20921,a2),x20922))), % 58.64/58.69 inference(rename_variables,[],[1852])). % 58.64/58.69 cnf(2093,plain, % 58.64/58.69 (~P4(x20931,f11(a2,x20932))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(2099,plain, % 58.64/58.69 (P4(f6(f11(a2,x20991),f11(x20992,a2),a7),a10)), % 58.64/58.69 inference(scs_inference,[],[225,2093,26,2087,1852,2092,40,52,53,44])). % 58.64/58.69 cnf(2104,plain, % 58.64/58.69 (~E(a9,f11(f11(x21041,a2),x21042))), % 58.64/58.69 inference(rename_variables,[],[1840])). % 58.64/58.69 cnf(2105,plain, % 58.64/58.69 (~P4(x21051,f11(a2,x21052))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(2107,plain, % 58.64/58.69 (P4(f6(f11(a2,a2),x21071,a9),a9)), % 58.64/58.69 inference(scs_inference,[],[225,2105,2099,1840,2104,40,52,53])). % 58.64/58.69 cnf(2111,plain, % 58.64/58.69 (P4(f6(f11(x21111,a2),f11(a2,x21112),a9),a10)), % 58.64/58.69 inference(scs_inference,[],[225,2105,26,2099,1840,2104,40,52,53,44])). % 58.64/58.69 cnf(2116,plain, % 58.64/58.69 (~E(a10,f11(f11(x21161,a2),x21162))), % 58.64/58.69 inference(rename_variables,[],[1843])). % 58.64/58.69 cnf(2117,plain, % 58.64/58.69 (~P4(x21171,f11(a2,x21172))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(2123,plain, % 58.64/58.69 (P4(f6(f11(a2,a2),x21231,a9),a10)), % 58.64/58.69 inference(scs_inference,[],[225,2117,26,2111,1843,2116,2107,40,52,53,44])). % 58.64/58.69 cnf(2128,plain, % 58.64/58.69 (~E(a7,f11(f11(x21281,a2),x21282))), % 58.64/58.69 inference(rename_variables,[],[1855])). % 58.64/58.69 cnf(2129,plain, % 58.64/58.69 (~P4(x21291,f11(a2,x21292))), % 58.64/58.69 inference(rename_variables,[],[225])). % 58.64/58.69 cnf(2131,plain, % 58.64/58.69 (P4(f6(f11(a2,a2),x21311,a7),a7)), % 58.64/58.69 inference(scs_inference,[],[225,2129,2123,1855,2128,40,52,53])). % 58.64/58.69 cnf(2135,plain, % 58.64/58.69 (P4(f6(f11(x21351,a2),f11(a2,x21352),a7),a9)), % 58.64/58.69 inference(scs_inference,[],[225,2129,25,2123,1855,2128,40,52,53,44])). % 58.64/58.69 cnf(2140,plain, % 58.64/58.69 (~E(a7,f11(a2,x21401))), % 58.64/58.69 inference(rename_variables,[],[1998])). % 58.64/58.69 cnf(2143,plain, % 58.64/58.69 (P4(f6(a2,x21431,a7),a7)), % 58.64/58.69 inference(scs_inference,[],[225,2135,65,1998,2140,40,52,53])). % 58.64/58.69 cnf(2146,plain, % 58.64/58.69 (P4(f11(f6(a2,x21461,a7),f6(a2,x21461,a7)),a7)), % 58.64/58.69 inference(scs_inference,[],[225,2135,77,65,1998,2140,40,52,53,17])). % 58.64/58.69 cnf(2148,plain, % 58.64/58.69 (P4(f6(f11(x21481,a2),f11(a2,x21482),a7),a10)), % 58.64/58.69 inference(scs_inference,[],[225,26,2135,77,65,1998,2140,40,52,53,17,44])). % 58.64/58.69 cnf(2152,plain, % 58.64/58.69 (P4(f11(f6(a2,x21521,a7),f6(a2,x21521,a7)),a9)), % 58.64/58.69 inference(scs_inference,[],[25,2148,2146,40,44])). % 58.64/58.69 cnf(2154,plain, % 58.64/58.69 (P4(f6(a2,x21541,a7),a9)), % 58.64/58.69 inference(scs_inference,[],[25,2148,28,2146,40,44,17])). % 58.64/58.69 cnf(2160,plain, % 58.64/58.69 (P4(f11(f6(a2,x21601,a7),f6(a2,x21601,a7)),a10)), % 58.64/58.69 inference(scs_inference,[],[26,2152,40,58,44])). % 58.64/58.69 cnf(2170,plain, % 58.64/58.69 (P4(f6(f11(a2,a2),x21701,a7),a9)), % 58.64/58.69 inference(scs_inference,[],[25,2160,2131,40,58,44])). % 58.64/58.69 cnf(2178,plain, % 58.64/58.69 (P4(f6(f11(a2,a2),x21781,a7),a10)), % 58.64/58.69 inference(scs_inference,[],[26,2170,40,44])). % 58.64/58.69 cnf(2182,plain, % 58.64/58.69 (P4(f6(a2,x21821,a7),a10)), % 58.64/58.69 inference(scs_inference,[],[26,2178,2154,40,44])). % 58.64/58.69 cnf(2494,plain, % 58.64/58.69 (~P4(f5(a7,a10),a10)), % 58.64/58.69 inference(scs_inference,[],[31,48])). % 58.64/58.69 cnf(2502,plain, % 58.64/58.69 (P4(f12(a7,a7),a7)), % 58.64/58.69 inference(scs_inference,[],[24,570,123,31,48,37,32,49,42])). % 58.64/58.69 cnf(2504,plain, % 58.64/58.69 (P4(f5(a7,a10),a7)), % 58.64/58.69 inference(scs_inference,[],[24,570,123,31,48,37,32,49,42,41])). % 58.64/58.69 cnf(2507,plain, % 58.64/58.69 (P4(f12(a9,a9),a9)), % 58.64/58.69 inference(scs_inference,[],[24,570,591,123,31,48,37,32,49,42,41,4,43])). % 58.64/58.69 cnf(2514,plain, % 58.64/58.69 (P4(f4(a7,a7),a7)), % 58.64/58.69 inference(scs_inference,[],[278,24,570,591,123,31,225,48,37,32,49,42,41,4,43,34,5,2,57])). % 58.64/58.69 cnf(2518,plain, % 58.64/58.69 (~E(a7,f11(a10,x25181))), % 58.64/58.69 inference(scs_inference,[],[278,24,570,591,123,31,225,48,37,32,49,42,41,4,43,34,5,2,57,40,46])). % 58.64/58.69 cnf(2524,plain, % 58.64/58.69 (~P3(a7,f11(a10,a10))), % 58.64/58.69 inference(scs_inference,[],[2182,278,24,570,591,123,31,225,28,48,37,32,49,42,41,4,43,34,5,2,57,40,46,45,58,20])). % 58.64/58.69 cnf(2525,plain, % 58.64/58.69 (E(f11(x25251,x25251),x25251)), % 58.64/58.69 inference(rename_variables,[],[28])). % 58.64/58.69 cnf(2528,plain, % 58.64/58.69 (E(f11(x25281,x25281),x25281)), % 58.64/58.69 inference(rename_variables,[],[28])). % 58.64/58.69 cnf(2530,plain, % 58.64/58.69 (E(f11(x25301,x25301),x25301)), % 58.64/58.69 inference(rename_variables,[],[28])). % 58.64/58.69 cnf(2532,plain, % 58.64/58.69 (E(f11(x25321,x25321),x25321)), % 58.64/58.69 inference(rename_variables,[],[28])). % 58.64/58.69 cnf(2539,plain, % 58.64/58.69 (~P4(f11(a10,a10),f6(a9,a9,a1))), % 58.64/58.69 inference(scs_inference,[],[667,674,1396,2182,278,24,281,287,570,591,123,163,65,31,225,28,2525,2528,2530,2532,48,37,32,49,42,41,4,43,34,5,2,57,40,46,45,58,20,16,19,21,22,52,3,17])). % 58.64/58.69 cnf(2540,plain, % 58.64/58.69 (E(f11(x25401,x25401),x25401)), % 58.64/58.69 inference(rename_variables,[],[28])). % 58.64/58.69 cnf(2550,plain, % 58.64/58.69 (E(f6(x25501,x25502,a2),f6(x25501,x25502,a1))), % 58.64/58.69 inference(scs_inference,[],[667,674,1396,2182,267,278,24,2143,281,287,570,591,123,163,65,31,225,28,2525,2528,2530,2532,48,37,32,49,42,41,4,43,34,5,2,57,40,46,45,58,20,16,19,21,22,52,3,17,44,11,9,10,12,13,14,15,8])). % 58.64/58.69 cnf(2551,plain, % 58.64/58.69 (E(f6(a2,x25511,x25512),f6(a1,x25511,x25512))), % 58.64/58.69 inference(scs_inference,[],[667,674,1396,2182,267,278,24,2143,281,287,570,591,123,163,65,31,225,28,2525,2528,2530,2532,48,37,32,49,42,41,4,43,34,5,2,57,40,46,45,58,20,16,19,21,22,52,3,17,44,11,9,10,12,13,14,15,8,6])). % 58.64/58.69 cnf(2552,plain, % 58.64/58.69 (E(f6(x25521,a2,x25522),f6(x25521,a1,x25522))), % 58.64/58.69 inference(scs_inference,[],[667,674,1396,2182,267,278,24,2143,281,287,570,591,123,163,65,31,225,28,2525,2528,2530,2532,48,37,32,49,42,41,4,43,34,5,2,57,40,46,45,58,20,16,19,21,22,52,3,17,44,11,9,10,12,13,14,15,8,6,7])). % 58.64/58.69 cnf(2553,plain, % 58.64/58.69 (~P4(f5(a7,a10),f11(a10,a10))), % 58.64/58.69 inference(scs_inference,[],[667,674,1396,2182,267,278,24,2143,281,287,570,591,123,163,65,31,225,28,2525,2528,2530,2532,2540,48,37,32,49,42,41,4,43,34,5,2,57,40,46,45,58,20,16,19,21,22,52,3,17,44,11,9,10,12,13,14,15,8,6,7,18])). % 58.64/58.69 cnf(2573,plain, % 58.64/58.69 (P3(f6(x25731,x25732,a1),f6(x25731,x25732,a2))), % 58.64/58.69 inference(scs_inference,[],[2514,2502,2550,2518,27,622,49,42,2,57,40,58,19])). % 58.64/58.69 cnf(2579,plain, % 58.64/58.69 (~P4(f5(a7,a10),f11(a9,a9))), % 58.64/58.69 inference(scs_inference,[],[979,2539,2514,2502,2550,2518,2494,259,27,622,77,49,42,2,57,40,58,19,3,18,44])). % 58.64/58.69 cnf(2581,plain, % 58.64/58.69 (~E(f11(a10,a10),f11(a7,a7))), % 58.64/58.69 inference(scs_inference,[],[979,2539,2514,2502,2553,2550,2504,2518,2494,259,27,622,77,49,42,2,57,40,58,19,3,18,44,50])). % 58.64/58.69 cnf(2593,plain, % 58.64/58.69 (E(f6(a2,x25931,x25932),f6(a1,x25931,x25932))), % 58.64/58.69 inference(rename_variables,[],[2551])). % 58.64/58.69 cnf(2602,plain, % 58.64/58.69 ($false), % 58.64/58.69 inference(scs_inference,[],[25,2581,2507,2579,2524,2551,2593,2552,2573,2504,591,77,28,49,2,57,40,58,20,19,3,18,44]), % 58.64/58.69 ['proof']). % 58.64/58.69 % SZS output end Proof % 58.64/58.69 % Total time :58.170000s %------------------------------------------------------------------------------