%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET619+3 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n024.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 14:22:00 EDT 2024 % Result : Theorem 67.03s 67.07s % Output : CNFRefutation 67.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SET619+3 : TPTP v8.2.0. Released v2.2.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n024.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sun Jun 23 15:52:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.50/0.55 start to proof:theBenchmark % 67.02/67.05 %------------------------------------------- % 67.02/67.05 % File :CSE---1.7 % 67.02/67.05 % Problem :theBenchmark % 67.02/67.05 % Transform :cnf % 67.02/67.05 % Format :tptp:raw % 67.02/67.05 % Command :java -jar mcs_scs.jar %d %s % 67.02/67.05 % 67.02/67.05 % Result :Theorem 66.460000s % 67.02/67.05 % Output :CNFRefutation 66.460000s % 67.02/67.05 %------------------------------------------- % 67.03/67.07 %-------------------------------------------------------------------------- % 67.03/67.07 % File : SET619+3 : TPTP v8.2.0. Released v2.2.0. % 67.03/67.07 % Domain : Set Theory % 67.03/67.07 % Problem : X U Y = (X sym\ Y) U X ^ Y % 67.03/67.07 % Version : [Try90] axioms : Reduced > Incomplete. % 67.03/67.07 % English : The union of X and Y is the union of (the symmetric difference % 67.03/67.07 % of X and Y) and the intersection of X and Y. % 67.03/67.07 % 67.03/67.07 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 67.03/67.07 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 67.03/67.07 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 67.03/67.07 % Source : [ILF] % 67.03/67.07 % Names : BOOLE (95) [TS89] % 67.03/67.07 % 67.03/67.07 % Status : Theorem % 67.03/67.07 % Rating : 0.31 v8.2.0, 0.28 v8.1.0, 0.22 v7.5.0, 0.34 v7.4.0, 0.13 v7.3.0, 0.24 v7.2.0, 0.28 v7.1.0, 0.17 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.30 v5.5.0, 0.37 v5.4.0, 0.43 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.38 v5.0.0, 0.46 v4.1.0, 0.43 v4.0.0, 0.46 v3.7.0, 0.40 v3.5.0, 0.37 v3.4.0, 0.32 v3.3.0, 0.29 v3.2.0, 0.27 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.14 v2.5.0, 0.12 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1 % 67.03/67.07 % Syntax : Number of formulae : 14 ( 9 unt; 0 def) % 67.03/67.07 % Number of atoms : 24 ( 10 equ) % 67.03/67.07 % Maximal formula atoms : 3 ( 1 avg) % 67.03/67.07 % Number of connectives : 10 ( 0 ~; 1 |; 2 &) % 67.03/67.07 % ( 6 <=>; 1 =>; 0 <=; 0 <~>) % 67.03/67.07 % Maximal formula depth : 6 ( 4 avg) % 67.03/67.07 % Maximal term depth : 3 ( 1 avg) % 67.03/67.07 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 67.03/67.07 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty) % 67.03/67.07 % Number of variables : 32 ( 32 !; 0 ?) % 67.03/67.07 % SPC : FOF_THM_RFO_SEQ % 67.03/67.07 % 67.03/67.07 % Comments : % 67.03/67.07 %-------------------------------------------------------------------------- % 67.03/67.07 %---- line(boole - df(7),1833089) % 67.03/67.07 fof(symmetric_difference_defn,axiom, % 67.03/67.07 ! [B,C] : symmetric_difference(B,C) = union(difference(B,C),difference(C,B)) ). % 67.03/67.07 % 67.03/67.07 %---- line(boole - th(64),1833712) % 67.03/67.07 fof(associativity_of_union,axiom, % 67.03/67.07 ! [B,C,D] : union(union(B,C),D) = union(B,union(C,D)) ). % 67.03/67.07 % 67.03/67.07 %---- line(boole - th(69),1833784) % 67.03/67.07 fof(union_intersection,axiom, % 67.03/67.07 ! [B,C] : union(B,intersection(B,C)) = B ). % 67.03/67.07 % 67.03/67.07 %---- line(boole - th(80),1833943) % 67.03/67.07 fof(union_intersection_difference,axiom, % 67.03/67.07 ! [B,C] : union(intersection(B,C),difference(B,C)) = B ). % 67.03/67.07 % 67.03/67.07 %---- line(boole - df(2),1833042) % 67.03/67.07 fof(union_defn,axiom, % 67.03/67.07 ! [B,C,D] : % 67.03/67.07 ( member(D,union(B,C)) % 67.03/67.07 <=> ( member(D,B) % 67.03/67.07 | member(D,C) ) ) ). % 67.03/67.07 % 67.03/67.07 %---- line(boole - df(3),1833060) % 67.03/67.07 fof(intersection_defn,axiom, % 67.03/67.07 ! [B,C,D] : % 67.03/67.07 ( member(D,intersection(B,C)) % 67.03/67.07 <=> ( member(D,B) % 67.03/67.07 & member(D,C) ) ) ). % 67.03/67.07 % 67.03/67.07 %---- line(boole - df(8),1833103) % 67.03/67.07 fof(equal_defn,axiom, % 67.03/67.07 ! [B,C] : % 67.03/67.07 ( B = C % 67.03/67.07 <=> ( subset(B,C) % 67.03/67.07 & subset(C,B) ) ) ). % 67.03/67.07 % 67.03/67.07 %---- property(commutativity,op(union,2,function)) % 67.03/67.07 fof(commutativity_of_union,axiom, % 67.03/67.07 ! [B,C] : union(B,C) = union(C,B) ). % 67.03/67.07 % 67.03/67.07 %---- property(commutativity,op(intersection,2,function)) % 67.03/67.07 fof(commutativity_of_intersection,axiom, % 67.03/67.07 ! [B,C] : intersection(B,C) = intersection(C,B) ). % 67.03/67.07 % 67.03/67.07 %---- property(commutativity,op(symmetric_difference,2,function)) % 67.03/67.07 fof(commutativity_of_symmetric_difference,axiom, % 67.03/67.07 ! [B,C] : symmetric_difference(B,C) = symmetric_difference(C,B) ). % 67.03/67.07 % 67.03/67.07 %---- line(hidden - axiom175,1832615) % 67.03/67.07 fof(equal_member_defn,axiom, % 67.03/67.07 ! [B,C] : % 67.03/67.07 ( B = C % 67.03/67.07 <=> ! [D] : % 67.03/67.07 ( member(D,B) % 67.03/67.07 <=> member(D,C) ) ) ). % 67.03/67.07 % 67.03/67.07 %---- line(tarski - df(3),1832749) % 67.03/67.07 fof(subset_defn,axiom, % 67.03/67.07 ! [B,C] : % 67.03/67.07 ( subset(B,C) % 67.03/67.07 <=> ! [D] : % 67.03/67.07 ( member(D,B) % 67.03/67.07 => member(D,C) ) ) ). % 67.03/67.07 % 67.03/67.07 %---- property(reflexivity,op(subset,2,predicate)) % 67.03/67.07 fof(reflexivity_of_subset,axiom, % 67.03/67.07 ! [B] : subset(B,B) ). % 67.03/67.07 % 67.03/67.07 %---- line(boole - th(95),1834220) % 67.03/67.07 fof(prove_th95,conjecture, % 67.03/67.07 ! [B,C] : union(B,C) = union(symmetric_difference(B,C),intersection(B,C)) ). % 67.03/67.07 % 67.03/67.07 %-------------------------------------------------------------------------- % 67.03/67.07 %------------------------------------------- % 67.03/67.07 % Proof found % 67.03/67.07 % SZS status Theorem for theBenchmark % 67.03/67.07 % SZS output start Proof % 67.03/67.07 %ClaNum:39(EqnAxiom:17) % 67.03/67.07 %VarNum:101(SingletonVarNum:45) % 67.03/67.07 %MaxLitNum:3 % 67.03/67.07 %MaxfuncDepth:2 % 67.03/67.07 %SharedTerms:9 % 67.03/67.07 %goalClause: 25 % 67.03/67.07 %singleGoalClaCount:1 % 67.03/67.08 [25]~E(f1(f1(f3(a4,a7),f3(a7,a4)),f2(a4,a7)),f1(a4,a7)) % 67.03/67.08 [18]P1(x181,x181) % 67.03/67.08 [19]E(f1(x191,x192),f1(x192,x191)) % 67.03/67.08 [20]E(f2(x201,x202),f2(x202,x201)) % 67.03/67.08 [21]E(f1(x211,f2(x211,x212)),x211) % 67.03/67.08 [22]E(f1(f2(x221,x222),f3(x221,x222)),x221) % 67.03/67.08 [23]E(f1(f1(x231,x232),x233),f1(x231,f1(x232,x233))) % 67.03/67.08 [27]~E(x271,x272)+P1(x271,x272) % 67.03/67.08 [29]P1(x291,x292)+P2(f5(x291,x292),x291) % 67.03/67.08 [35]P1(x351,x352)+~P2(f5(x351,x352),x352) % 67.03/67.08 [31]~P2(x311,x313)+P2(x311,f1(x312,x313)) % 67.03/67.08 [32]~P2(x321,x322)+P2(x321,f1(x322,x323)) % 67.03/67.08 [33]P2(x331,x332)+~P2(x331,f2(x333,x332)) % 67.03/67.08 [34]P2(x341,x342)+~P2(x341,f2(x342,x343)) % 67.03/67.08 [28]~P1(x282,x281)+~P1(x281,x282)+E(x281,x282) % 67.03/67.08 [36]E(x361,x362)+P2(f6(x361,x362),x362)+P2(f6(x361,x362),x361) % 67.03/67.08 [39]E(x391,x392)+~P2(f6(x391,x392),x392)+~P2(f6(x391,x392),x391) % 67.03/67.08 [30]~P1(x303,x302)+P2(x301,x302)+~P2(x301,x303) % 67.03/67.08 [37]~P2(x371,x373)+~P2(x371,x372)+P2(x371,f2(x372,x373)) % 67.03/67.08 [38]P2(x381,x382)+P2(x381,x383)+~P2(x381,f1(x383,x382)) % 67.03/67.08 %EqnAxiom % 67.03/67.08 [1]E(x11,x11) % 67.03/67.08 [2]E(x22,x21)+~E(x21,x22) % 67.03/67.08 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 67.03/67.08 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 67.03/67.08 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 67.03/67.08 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 67.03/67.08 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 67.03/67.08 [8]~E(x81,x82)+E(f2(x81,x83),f2(x82,x83)) % 67.03/67.08 [9]~E(x91,x92)+E(f2(x93,x91),f2(x93,x92)) % 67.03/67.08 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 67.03/67.08 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 67.03/67.08 [12]~E(x121,x122)+E(f3(x121,x123),f3(x122,x123)) % 67.03/67.08 [13]~E(x131,x132)+E(f3(x133,x131),f3(x133,x132)) % 67.03/67.08 [14]P1(x142,x143)+~E(x141,x142)+~P1(x141,x143) % 67.03/67.08 [15]P1(x153,x152)+~E(x151,x152)+~P1(x153,x151) % 67.03/67.08 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163) % 67.03/67.08 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171) % 67.03/67.08 % 67.03/67.08 %------------------------------------------- % 67.03/67.09 cnf(41,plain, % 67.03/67.09 (E(x411,f1(f2(x411,x412),f3(x411,x412)))), % 67.03/67.09 inference(scs_inference,[],[22,2])). % 67.03/67.09 cnf(42,plain, % 67.03/67.09 (~E(f1(f1(f3(a4,a7),f3(a7,a4)),f2(a4,a7)),f1(a7,a4))), % 67.03/67.09 inference(scs_inference,[],[25,19,22,2,3])). % 67.03/67.09 cnf(43,plain, % 67.03/67.09 (E(f1(x431,x432),f1(x432,x431))), % 67.03/67.09 inference(rename_variables,[],[19])). % 67.03/67.09 cnf(44,plain, % 67.03/67.09 (P1(f1(x441,x442),f1(x442,x441))), % 67.03/67.09 inference(scs_inference,[],[25,18,19,43,22,2,3,14])). % 67.03/67.09 cnf(46,plain, % 67.03/67.09 (E(x461,f1(x461,f2(x461,x462)))), % 67.03/67.09 inference(scs_inference,[],[21,2])). % 67.03/67.09 cnf(47,plain, % 67.03/67.09 (P1(x471,f1(f2(x471,x472),f3(x471,x472)))), % 67.03/67.09 inference(scs_inference,[],[41,21,18,2,15])). % 67.03/67.09 cnf(48,plain, % 67.03/67.09 (P1(x481,x481)), % 67.03/67.09 inference(rename_variables,[],[18])). % 67.03/67.09 cnf(49,plain, % 67.03/67.09 (P1(f1(f2(x491,x492),f3(x491,x492)),x491)), % 67.03/67.09 inference(scs_inference,[],[41,21,18,48,2,15,14])). % 67.03/67.09 cnf(51,plain, % 67.03/67.09 (E(f1(x511,f1(x512,x513)),f1(f1(x511,x512),x513))), % 67.03/67.09 inference(scs_inference,[],[23,2])). % 67.03/67.09 cnf(52,plain, % 67.03/67.09 (P1(f1(x521,x522),f1(f1(x522,x521),f2(f1(x522,x521),x523)))), % 67.03/67.09 inference(scs_inference,[],[46,44,23,2,15])). % 67.03/67.09 cnf(53,plain, % 67.03/67.09 (E(x531,f1(x531,f2(x531,x532)))), % 67.03/67.09 inference(rename_variables,[],[46])). % 67.03/67.09 cnf(54,plain, % 67.03/67.09 (P1(f1(f1(x541,x542),f2(f1(x541,x542),x543)),f1(x542,x541))), % 67.03/67.09 inference(scs_inference,[],[46,53,44,23,2,15,14])). % 67.03/67.09 cnf(56,plain, % 67.03/67.09 (E(f1(f1(x561,x562),f2(f1(x561,x562),x563)),f1(x562,x561))), % 67.03/67.09 inference(scs_inference,[],[54,52,28])). % 67.03/67.09 cnf(59,plain, % 67.03/67.09 (E(f1(f1(x591,x592),x593),f1(f1(x593,x591),x592))), % 67.03/67.09 inference(scs_inference,[],[51,54,52,19,28,3])). % 67.03/67.09 cnf(60,plain, % 67.03/67.09 (E(f1(x601,f1(x602,x603)),f1(f1(x601,x602),x603))), % 67.03/67.09 inference(rename_variables,[],[51])). % 67.03/67.09 cnf(62,plain, % 67.03/67.09 (P1(f1(x621,f1(x622,x623)),f1(f1(x621,x622),x623))), % 67.03/67.09 inference(scs_inference,[],[51,60,54,52,19,18,28,3,15])). % 67.03/67.09 cnf(63,plain, % 67.03/67.09 (P1(x631,x631)), % 67.03/67.09 inference(rename_variables,[],[18])). % 67.03/67.09 cnf(64,plain, % 67.03/67.09 (P1(f1(f1(x641,x642),x643),f1(x641,f1(x642,x643)))), % 67.03/67.09 inference(scs_inference,[],[51,60,54,52,19,18,63,28,3,15,14])). % 67.03/67.09 cnf(67,plain, % 67.03/67.09 (E(f1(f1(x671,x672),x673),f1(f1(x672,x673),x671))), % 67.03/67.09 inference(scs_inference,[],[59,2])). % 67.03/67.09 cnf(68,plain, % 67.03/67.09 (P1(f1(f2(f1(x681,x682),x683),f1(x681,x682)),f1(x682,x681))), % 67.03/67.09 inference(scs_inference,[],[56,59,44,2,15])). % 67.03/67.09 cnf(69,plain, % 67.03/67.09 (P1(f1(x691,x692),f1(x692,x691))), % 67.03/67.09 inference(rename_variables,[],[44])). % 67.03/67.09 cnf(70,plain, % 67.03/67.09 (P1(f1(x701,x702),f1(f2(f1(x702,x701),x703),f1(x702,x701)))), % 67.03/67.09 inference(scs_inference,[],[56,59,44,69,2,15,14])). % 67.03/67.09 cnf(72,plain, % 67.03/67.09 (E(f1(f2(f1(x721,x722),x723),f1(x721,x722)),f1(x722,x721))), % 67.03/67.09 inference(scs_inference,[],[56,59,44,69,2,15,14,28])). % 67.03/67.09 cnf(74,plain, % 67.03/67.09 (E(f1(x741,x742),f1(f2(f1(x742,x741),x743),f1(x742,x741)))), % 67.03/67.09 inference(scs_inference,[],[72,2])). % 67.03/67.09 cnf(75,plain, % 67.03/67.09 (E(f1(f1(x751,x752),x753),f1(x752,f1(x753,x751)))), % 67.03/67.09 inference(scs_inference,[],[67,23,3])). % 67.03/67.09 cnf(77,plain, % 67.03/67.09 (P1(f1(x771,x772),f1(f2(f1(x771,x772),x773),f1(x771,x772)))), % 67.03/67.09 inference(scs_inference,[],[74,67,23,44,3,15])). % 67.03/67.09 cnf(78,plain, % 67.03/67.09 (P1(f1(x781,x782),f1(x782,x781))), % 67.03/67.09 inference(rename_variables,[],[44])). % 67.03/67.09 cnf(81,plain, % 67.03/67.09 (E(f1(x811,f1(x812,x813)),f1(f1(x813,x811),x812))), % 67.03/67.09 inference(scs_inference,[],[74,67,23,44,78,3,15,14,2])). % 67.03/67.09 cnf(82,plain, % 67.03/67.09 (P1(f1(x821,f1(x822,x823)),f1(x822,f1(x823,x821)))), % 67.03/67.09 inference(scs_inference,[],[75,62,15])). % 67.03/67.09 cnf(84,plain, % 67.03/67.09 (P1(f1(x841,f1(x842,x843)),f1(x843,f1(x841,x842)))), % 67.03/67.09 inference(scs_inference,[],[75,62,64,15,14])). % 67.03/67.09 cnf(86,plain, % 67.03/67.09 (E(f1(x861,f1(x862,x863)),f1(x863,f1(x861,x862)))), % 67.03/67.09 inference(scs_inference,[],[81,23,3])). % 67.03/67.09 cnf(88,plain, % 67.03/67.09 (P1(f1(f1(x881,x882),x883),f1(f1(x883,x881),x882))), % 67.03/67.09 inference(scs_inference,[],[81,64,23,3,15])). % 67.03/67.09 cnf(92,plain, % 67.03/67.09 (E(f1(x921,f1(x922,x923)),f1(x922,f1(x923,x921)))), % 67.03/67.09 inference(scs_inference,[],[81,62,64,23,3,15,14,2])). % 67.03/67.09 cnf(93,plain, % 67.03/67.09 (P1(f1(f1(x931,x932),x933),f1(x932,f1(x933,x931)))), % 67.03/67.09 inference(scs_inference,[],[86,44,15])). % 67.03/67.09 cnf(94,plain, % 67.03/67.09 (P1(f1(x941,x942),f1(x942,x941))), % 67.03/67.09 inference(rename_variables,[],[44])). % 67.03/67.09 cnf(95,plain, % 67.03/67.09 (P1(f1(x951,f1(x952,x953)),f1(f1(x953,x951),x952))), % 67.03/67.09 inference(scs_inference,[],[86,44,94,15,14])). % 67.03/67.09 cnf(99,plain, % 67.03/67.09 (E(f1(x991,x992),f1(f2(f1(x991,x992),x993),f1(x991,x992)))), % 67.03/67.09 inference(scs_inference,[],[19,74,3])). % 67.03/67.09 cnf(101,plain, % 67.03/67.09 (P1(x1011,f1(f3(x1011,x1012),f2(x1011,x1012)))), % 67.03/67.09 inference(scs_inference,[],[19,74,47,3,15])). % 67.03/67.09 cnf(112,plain, % 67.03/67.09 (E(f1(x1121,x1122),f1(x1122,x1121))), % 67.03/67.09 inference(rename_variables,[],[19])). % 67.03/67.09 cnf(115,plain, % 67.03/67.09 (E(x1151,f1(f3(x1151,x1152),f2(x1151,x1152)))), % 67.03/67.09 inference(scs_inference,[],[19,112,99,49,101,77,2,15,14,28])). % 67.03/67.09 cnf(120,plain, % 67.03/67.09 (E(f2(x1201,x1202),f1(f2(x1202,x1201),f2(f2(x1202,x1201),x1203)))), % 67.03/67.09 inference(scs_inference,[],[20,46,3])). % 67.03/67.09 cnf(124,plain, % 67.03/67.09 (E(f1(f2(x1241,x1242),f2(f2(x1241,x1242),x1243)),f2(x1242,x1241))), % 67.03/67.09 inference(scs_inference,[],[20,46,18,3,15,2])). % 67.03/67.09 cnf(125,plain, % 67.03/67.09 (E(f1(f2(x1251,x1252),x1253),f1(f2(x1252,x1251),x1253))), % 67.03/67.09 inference(scs_inference,[],[20,4,2])). % 67.03/67.09 cnf(127,plain, % 67.03/67.09 (E(f1(x1271,f2(x1271,x1272)),f1(f2(x1271,x1273),f3(x1271,x1273)))), % 67.03/67.09 inference(scs_inference,[],[21,41,3])). % 67.03/67.09 cnf(129,plain, % 67.03/67.09 (P1(f1(x1291,f2(x1291,x1292)),x1291)), % 67.03/67.09 inference(scs_inference,[],[21,41,18,3,15])). % 67.03/67.09 cnf(130,plain, % 67.03/67.09 (P1(x1301,x1301)), % 67.03/67.09 inference(rename_variables,[],[18])). % 67.03/67.09 cnf(131,plain, % 67.03/67.09 (P1(x1311,f1(x1311,f2(x1311,x1312)))), % 67.03/67.09 inference(scs_inference,[],[21,41,18,130,3,15,14])). % 67.03/67.09 cnf(133,plain, % 67.03/67.09 (E(f1(f2(x1331,x1332),f3(x1331,x1332)),f1(x1331,f2(x1331,x1333)))), % 67.03/67.09 inference(scs_inference,[],[21,41,18,130,3,15,14,2])). % 67.03/67.09 cnf(142,plain, % 67.03/67.09 (E(f1(x1421,f2(x1421,x1422)),f1(f3(x1421,x1423),f2(x1421,x1423)))), % 67.03/67.09 inference(scs_inference,[],[21,115,3])). % 67.03/67.09 cnf(144,plain, % 67.03/67.09 (P1(f1(f2(x1441,x1442),x1441),x1441)), % 67.03/67.09 inference(scs_inference,[],[21,115,44,3,15])). % 67.03/67.09 cnf(145,plain, % 67.03/67.09 (P1(f1(x1451,x1452),f1(x1452,x1451))), % 67.03/67.09 inference(rename_variables,[],[44])). % 67.03/67.09 cnf(146,plain, % 67.03/67.09 (P1(x1461,f1(f2(x1461,x1462),x1461))), % 67.03/67.09 inference(scs_inference,[],[21,115,44,145,3,15,14])). % 67.03/67.09 cnf(155,plain, % 67.03/67.09 (E(f1(f2(x1551,x1552),f3(x1551,x1552)),f1(f3(x1551,x1553),f2(x1551,x1553)))), % 67.03/67.09 inference(scs_inference,[],[22,115,3])). % 67.03/67.09 cnf(157,plain, % 67.03/67.09 (E(f1(f3(x1571,x1572),f2(x1571,x1572)),f1(f2(x1571,x1573),f3(x1571,x1573)))), % 67.03/67.09 inference(scs_inference,[],[22,115,3,2])). % 67.03/67.09 cnf(164,plain, % 67.03/67.09 (P1(f1(x1641,f2(x1641,x1642)),f1(f2(x1641,x1643),f3(x1641,x1643)))), % 67.03/67.09 inference(scs_inference,[],[41,129,15])). % 67.03/67.09 cnf(166,plain, % 67.03/67.09 (P1(f1(f2(x1661,x1662),f3(x1661,x1662)),f1(f2(x1661,x1663),x1661))), % 67.03/67.09 inference(scs_inference,[],[41,129,146,15,14])). % 67.03/67.09 cnf(170,plain, % 67.03/67.09 (E(x1701,f1(f2(x1701,x1702),x1701))+~P1(f1(f2(x1701,x1702),x1701),f1(f2(x1701,x1703),f3(x1701,x1703)))), % 67.03/67.09 inference(scs_inference,[],[41,129,146,15,14,28,3])). % 67.03/67.09 cnf(175,plain, % 67.03/67.09 (P1(f1(f2(x1751,x1752),f3(x1751,x1752)),f1(f2(x1751,x1753),f3(x1751,x1753)))), % 67.03/67.09 inference(scs_inference,[],[41,144,47,15,14])). % 67.03/67.09 cnf(177,plain, % 67.03/67.09 (E(x1771,f1(f2(x1771,x1772),x1771))), % 67.03/67.09 inference(scs_inference,[],[41,144,47,15,14,170])). % 67.03/67.09 cnf(179,plain, % 67.03/67.09 (E(f1(f2(x1791,x1792),x1791),x1791)), % 67.03/67.09 inference(scs_inference,[],[41,144,47,15,14,170,2])). % 67.03/67.09 cnf(180,plain, % 67.03/67.09 (E(f1(f2(x1801,x1802),f3(x1801,x1802)),f1(f2(x1801,x1803),x1801))), % 67.03/67.09 inference(scs_inference,[],[41,166,144,47,15,14,170,2,28])). % 67.03/67.09 cnf(183,plain, % 67.03/67.09 (E(f1(f2(x1831,x1832),x1831),f1(f2(x1831,x1833),f3(x1831,x1833)))), % 67.03/67.09 inference(scs_inference,[],[180,2])). % 67.03/67.09 cnf(198,plain, % 67.03/67.09 (P1(f1(f2(x1981,x1982),x1981),f1(x1981,f2(x1981,x1983)))), % 67.03/67.09 inference(scs_inference,[],[46,144,15])). % 67.03/67.09 cnf(200,plain, % 67.03/67.09 (P1(f1(x2001,f2(x2001,x2002)),f1(f2(x2001,x2003),x2001))), % 67.03/67.09 inference(scs_inference,[],[46,144,146,15,14])). % 67.03/67.09 cnf(203,plain, % 67.03/67.09 (E(f1(f2(x2031,x2032),x2031),f1(x2031,f2(x2031,x2033)))), % 67.03/67.09 inference(scs_inference,[],[198,200,28])). % 67.03/67.09 cnf(206,plain, % 67.03/67.09 (E(f1(x2061,f2(x2061,x2062)),f1(f2(x2061,x2063),x2061))), % 67.03/67.09 inference(scs_inference,[],[198,200,28,2])). % 67.03/67.09 cnf(231,plain, % 67.03/67.09 (E(f3(x2311,f1(f3(x2312,x2313),f2(x2312,x2313))),f3(x2311,x2312))), % 67.03/67.09 inference(scs_inference,[],[115,2,13])). % 67.03/67.09 cnf(233,plain, % 67.03/67.09 (P1(f1(f2(x2331,x2332),x2331),f1(f3(x2331,x2333),f2(x2331,x2333)))), % 67.03/67.09 inference(scs_inference,[],[115,231,144,2,15])). % 67.03/67.09 cnf(235,plain, % 67.03/67.09 (P1(f1(f3(x2351,x2352),f2(x2351,x2352)),f1(f2(x2351,x2353),x2351))), % 67.03/67.09 inference(scs_inference,[],[115,231,144,146,2,15,14])). % 67.03/67.09 cnf(237,plain, % 67.03/67.09 (E(f1(f2(x2371,x2372),x2371),f1(f3(x2371,x2373),f2(x2371,x2373)))), % 67.03/67.09 inference(scs_inference,[],[115,231,144,146,2,15,14,28])). % 67.03/67.09 cnf(239,plain, % 67.03/67.09 (E(f1(f1(f3(x2391,x2392),f2(x2391,x2392)),x2393),f1(x2391,x2393))), % 67.03/67.09 inference(scs_inference,[],[115,2,4])). % 67.03/67.09 cnf(240,plain, % 67.03/67.09 (E(f1(x2401,x2402),f1(f1(f3(x2401,x2403),f2(x2401,x2403)),x2402))), % 67.03/67.09 inference(scs_inference,[],[239,2])). % 67.03/67.09 cnf(241,plain, % 67.03/67.09 (E(f1(f3(x2411,x2412),f2(x2411,x2412)),f1(f2(x2411,x2413),x2411))), % 67.03/67.09 inference(scs_inference,[],[239,233,235,2,28])). % 67.03/67.09 cnf(244,plain, % 67.03/67.09 (E(f1(x2441,f1(f3(x2442,x2443),f2(x2442,x2443))),f1(x2441,x2442))), % 67.03/67.09 inference(scs_inference,[],[115,2,5])). % 67.03/67.09 cnf(245,plain, % 67.03/67.09 (E(f1(x2451,x2452),f1(x2451,f1(f3(x2452,x2453),f2(x2452,x2453))))), % 67.03/67.09 inference(scs_inference,[],[244,2])). % 67.03/67.09 cnf(268,plain, % 67.03/67.09 (E(f1(f2(f2(x2681,x2682),x2683),f2(x2681,x2682)),f2(x2682,x2681))), % 67.03/67.09 inference(scs_inference,[],[120,206,3,2])). % 67.03/67.09 cnf(272,plain, % 67.03/67.09 (P1(f1(f2(f2(x2721,x2722),x2723),f2(x2721,x2722)),f2(x2722,x2721))), % 67.03/67.09 inference(scs_inference,[],[124,198,15])). % 67.03/67.09 cnf(274,plain, % 67.03/67.09 (P1(f2(x2741,x2742),f1(f2(f2(x2742,x2741),x2743),f2(x2742,x2741)))), % 67.03/67.09 inference(scs_inference,[],[124,198,200,15,14])). % 67.03/67.09 cnf(278,plain, % 67.03/67.09 (E(f1(f2(x2781,x2782),f3(x2782,x2781)),f1(f3(x2782,x2783),f2(x2782,x2783)))), % 67.03/67.09 inference(scs_inference,[],[125,155,3])). % 67.03/67.09 cnf(280,plain, % 67.03/67.09 (E(f1(f2(x2801,x2802),x2803),f1(f2(x2802,x2801),x2803))), % 67.03/67.09 inference(rename_variables,[],[125])). % 67.03/67.09 cnf(281,plain, % 67.03/67.09 (P1(f1(f2(x2811,x2812),f3(x2811,x2812)),f1(f2(x2813,x2811),f3(x2811,x2813)))), % 67.03/67.09 inference(scs_inference,[],[125,280,155,175,3,15])). % 67.03/67.09 cnf(283,plain, % 67.03/67.09 (E(f1(f2(x2831,x2832),x2833),f1(f2(x2832,x2831),x2833))), % 67.03/67.09 inference(rename_variables,[],[125])). % 67.03/67.09 cnf(287,plain, % 67.03/67.09 (E(f1(f3(x2871,x2872),f2(x2871,x2872)),f1(f2(x2873,x2871),f3(x2871,x2873)))), % 67.03/67.09 inference(scs_inference,[],[125,280,283,155,272,175,3,15,14,2])). % 67.03/67.09 cnf(291,plain, % 67.03/67.09 (E(f1(f2(x2911,x2912),x2913),f1(f2(x2912,x2911),x2913))), % 67.03/67.09 inference(rename_variables,[],[125])). % 67.03/67.09 cnf(292,plain, % 67.03/67.09 (P1(f1(x2921,x2922),f1(f2(x2923,f1(x2922,x2921)),f1(x2922,x2921)))), % 67.03/67.09 inference(scs_inference,[],[125,291,133,70,3,15])). % 67.03/67.09 cnf(294,plain, % 67.03/67.09 (E(f1(f2(x2941,x2942),x2943),f1(f2(x2942,x2941),x2943))), % 67.03/67.09 inference(rename_variables,[],[125])). % 67.03/67.09 cnf(298,plain, % 67.03/67.09 (E(f1(x2981,f2(x2981,x2982)),f1(f2(x2983,x2981),f3(x2981,x2983)))), % 67.03/67.09 inference(scs_inference,[],[125,291,294,133,281,70,3,15,14,2])). % 67.03/67.09 cnf(300,plain, % 67.03/67.09 (E(f1(f2(x3001,x3002),f2(f2(x3002,x3001),x3003)),f2(x3001,x3002))), % 67.03/67.09 inference(scs_inference,[],[125,124,3])). % 67.03/67.09 cnf(313,plain, % 67.03/67.09 (E(f1(f2(x3131,x3132),x3133),f1(f2(x3132,x3131),x3133))), % 67.03/67.09 inference(rename_variables,[],[125])). % 67.03/67.09 cnf(316,plain, % 67.03/67.10 (E(f1(f2(x3161,x3162),x3163),f1(f2(x3162,x3161),x3163))), % 67.03/67.10 inference(rename_variables,[],[125])). % 67.03/67.10 cnf(317,plain, % 67.03/67.10 (P1(f1(f2(x3171,f1(x3172,x3173)),f1(x3172,x3173)),f1(x3173,x3172))), % 67.03/67.10 inference(scs_inference,[],[125,313,316,268,300,274,68,2,3,15,14])). % 67.03/67.10 cnf(323,plain, % 67.03/67.10 (E(f1(f2(x3231,f1(x3232,x3233)),f1(x3232,x3233)),f1(x3233,x3232))), % 67.03/67.10 inference(scs_inference,[],[317,292,28])). % 67.03/67.10 cnf(326,plain, % 67.03/67.10 (E(f1(f2(x3261,x3262),x3262),f1(f2(x3262,x3263),f3(x3262,x3263)))), % 67.03/67.10 inference(scs_inference,[],[125,183,317,292,28,3])). % 67.03/67.10 cnf(337,plain, % 67.03/67.10 (E(f1(f2(x3371,x3372),f3(x3371,x3372)),f1(f2(x3373,x3371),x3371))), % 67.03/67.10 inference(scs_inference,[],[326,2])). % 67.03/67.10 cnf(338,plain, % 67.03/67.10 (E(f1(f2(x3381,x3382),x3382),f1(f3(x3382,x3383),f2(x3382,x3383)))), % 67.03/67.10 inference(scs_inference,[],[125,237,326,2,3])). % 67.03/67.10 cnf(348,plain, % 67.03/67.10 (E(f1(f3(x3481,x3482),f2(x3481,x3482)),f1(f2(x3483,x3481),x3481))), % 67.03/67.10 inference(scs_inference,[],[338,2])). % 67.03/67.10 cnf(349,plain, % 67.03/67.10 (E(f1(f2(x3491,x3492),f3(x3492,x3491)),f1(f2(x3493,x3492),x3492))), % 67.03/67.10 inference(scs_inference,[],[125,337,338,2,3])). % 67.03/67.10 cnf(359,plain, % 67.03/67.10 (E(f1(f2(x3591,x3592),x3592),f1(f2(x3593,x3592),f3(x3592,x3593)))), % 67.03/67.10 inference(scs_inference,[],[349,2])). % 67.03/67.10 cnf(360,plain, % 67.03/67.10 (E(f1(f2(x3601,x3602),x3602),f1(x3602,f2(x3602,x3603)))), % 67.03/67.10 inference(scs_inference,[],[125,349,203,2,3])). % 67.03/67.10 cnf(362,plain, % 67.03/67.10 (E(f1(f2(x3621,x3622),x3623),f1(f2(x3622,x3621),x3623))), % 67.03/67.10 inference(rename_variables,[],[125])). % 67.03/67.10 cnf(363,plain, % 67.03/67.10 (P1(f1(x3631,f2(x3631,x3632)),f1(f2(x3633,x3631),f3(x3631,x3633)))), % 67.03/67.10 inference(scs_inference,[],[125,362,349,203,164,2,3,15])). % 67.03/67.10 cnf(365,plain, % 67.03/67.10 (E(f1(f2(x3651,x3652),x3653),f1(f2(x3652,x3651),x3653))), % 67.03/67.10 inference(rename_variables,[],[125])). % 67.03/67.10 cnf(366,plain, % 67.03/67.10 (P1(f1(f2(x3661,x3662),f3(x3662,x3661)),x3662)), % 67.03/67.10 inference(scs_inference,[],[125,362,365,349,203,49,164,2,3,15,14])). % 67.03/67.10 cnf(370,plain, % 67.03/67.10 (E(f1(x3701,f2(x3701,x3702)),f1(f2(x3703,x3701),x3701))), % 67.03/67.10 inference(scs_inference,[],[360,2])). % 67.03/67.10 cnf(395,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f3(a4,a7),f1(f3(a7,a4),f2(a4,a7))))), % 67.03/67.10 inference(scs_inference,[],[25,51,2,3])). % 67.03/67.10 cnf(396,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f2(a4,a7),f1(f3(a4,a7),f3(a7,a4))))), % 67.03/67.10 inference(scs_inference,[],[92,395,3])). % 67.03/67.10 cnf(404,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f2(a7,a4),f1(f3(a4,a7),f3(a7,a4))))), % 67.03/67.10 inference(scs_inference,[],[125,396,2,3])). % 67.03/67.10 cnf(405,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f3(a7,a4),f1(f2(a7,a4),f3(a4,a7))))), % 67.03/67.10 inference(scs_inference,[],[92,404,3])). % 67.03/67.10 cnf(409,plain, % 67.03/67.10 (E(f1(f2(x4091,x4092),x4093),f1(f2(x4092,x4091),x4093))), % 67.03/67.10 inference(rename_variables,[],[125])). % 67.03/67.10 cnf(413,plain, % 67.03/67.10 (E(x4131,f1(f2(x4132,x4131),f3(x4131,x4132)))), % 67.03/67.10 inference(scs_inference,[],[125,409,92,366,404,47,198,3,15,14,28])). % 67.03/67.10 cnf(415,plain, % 67.03/67.10 (E(f1(f2(x4151,x4152),f3(x4152,x4151)),x4152)), % 67.03/67.10 inference(scs_inference,[],[125,409,92,366,404,47,198,3,15,14,28,2])). % 67.03/67.10 cnf(416,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f3(a7,a4),f1(f2(a4,a7),f3(a4,a7))))), % 67.03/67.10 inference(scs_inference,[],[25,81,2,3])). % 67.03/67.10 cnf(417,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f1(f3(a4,a7),f3(a7,a4)),f2(a4,a7)))), % 67.03/67.10 inference(scs_inference,[],[75,416,3])). % 67.03/67.10 cnf(421,plain, % 67.03/67.10 (E(f1(f2(x4211,x4212),x4213),f1(f2(x4212,x4211),x4213))), % 67.03/67.10 inference(rename_variables,[],[125])). % 67.03/67.10 cnf(422,plain, % 67.03/67.10 (P1(f1(f2(x4221,x4222),x4222),x4222)), % 67.03/67.10 inference(scs_inference,[],[125,421,75,416,200,144,3,15,14])). % 67.03/67.10 cnf(427,plain, % 67.03/67.10 (P1(x4271,f1(f2(x4272,x4271),x4271))), % 67.03/67.10 inference(scs_inference,[],[125,59,417,146,3,15])). % 67.03/67.10 cnf(429,plain, % 67.03/67.10 (E(f1(f2(x4291,x4292),x4293),f1(f2(x4292,x4291),x4293))), % 67.03/67.10 inference(rename_variables,[],[125])). % 67.03/67.10 cnf(430,plain, % 67.03/67.10 (P1(f1(f2(x4301,x4302),x4303),f1(x4303,f2(x4302,x4301)))), % 67.03/67.10 inference(scs_inference,[],[125,429,59,417,146,44,3,15,14])). % 67.03/67.10 cnf(432,plain, % 67.03/67.10 (E(x4321,f1(f2(x4322,x4321),x4321))), % 67.03/67.10 inference(scs_inference,[],[125,429,59,422,417,146,44,3,15,14,28])). % 67.03/67.10 cnf(434,plain, % 67.03/67.10 (E(f1(f2(x4341,x4342),x4342),x4342)), % 67.03/67.10 inference(scs_inference,[],[125,429,59,422,417,146,44,3,15,14,28,2])). % 67.03/67.10 cnf(444,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f3(a4,a7),f1(f3(a7,a4),f2(a7,a4))))), % 67.03/67.10 inference(scs_inference,[],[92,405,3])). % 67.03/67.10 cnf(446,plain, % 67.03/67.10 (P1(f1(x4461,f2(x4462,x4463)),f1(f2(x4463,x4462),x4461))), % 67.03/67.10 inference(scs_inference,[],[125,92,405,44,3,15])). % 67.03/67.10 cnf(449,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f1(f2(a7,a4),f3(a4,a7)),f3(a7,a4)))), % 67.03/67.10 inference(scs_inference,[],[75,444,3])). % 67.03/67.10 cnf(452,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f1(f3(a7,a4),f2(a7,a4)),f3(a4,a7)))), % 67.03/67.10 inference(scs_inference,[],[67,449,3])). % 67.03/67.10 cnf(457,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(a7,f3(a4,a7)))), % 67.03/67.10 inference(scs_inference,[],[240,452,3])). % 67.03/67.10 cnf(460,plain, % 67.03/67.10 (~E(f1(a4,a7),f1(f3(a4,a7),a7))), % 67.03/67.10 inference(scs_inference,[],[245,444,3])). % 67.03/67.10 cnf(462,plain, % 67.03/67.10 (~E(a4,f3(a4,a7))), % 67.03/67.10 inference(scs_inference,[],[245,444,3,4])). % 67.03/67.10 cnf(471,plain, % 67.03/67.10 (P1(f1(f3(x4711,x4712),f2(x4712,x4711)),f1(x4711,f2(x4711,x4713)))), % 67.03/67.10 inference(scs_inference,[],[133,446,15])). % 67.03/67.10 cnf(475,plain, % 67.03/67.10 (P1(f1(x4751,f2(x4751,x4752)),f1(f3(x4751,x4753),f2(x4753,x4751)))), % 67.03/67.10 inference(scs_inference,[],[133,298,446,430,15,3,14])). % 67.03/67.10 cnf(520,plain, % 67.03/67.10 (P1(f1(x5201,x5202),f1(f1(f2(x5201,x5203),x5201),x5202))), % 67.03/67.10 inference(scs_inference,[],[177,27,4])). % 67.03/67.10 cnf(540,plain, % 67.03/67.10 (P1(f1(x5401,f2(x5402,x5401)),x5401)), % 67.03/67.10 inference(scs_inference,[],[179,446,15])). % 67.03/67.10 cnf(542,plain, % 67.03/67.10 (P1(x5421,f1(x5421,f2(x5422,x5421)))), % 67.03/67.10 inference(scs_inference,[],[179,446,430,15,14])). % 67.03/67.10 cnf(566,plain, % 67.03/67.10 (P1(f1(f1(x5661,x5662),x5663),f1(f1(f2(x5661,x5664),x5661),f1(x5662,x5663)))), % 67.03/67.10 inference(scs_inference,[],[51,520,14])). % 67.03/67.10 cnf(580,plain, % 67.03/67.10 (P1(f1(x5801,f2(x5802,x5801)),f1(x5801,f2(x5801,x5803)))), % 67.03/67.10 inference(scs_inference,[],[203,446,15])). % 67.03/67.10 cnf(582,plain, % 67.03/67.10 (P1(f1(x5821,f2(x5821,x5822)),f1(x5821,f2(x5823,x5821)))), % 67.03/67.10 inference(scs_inference,[],[203,446,430,15,14])). % 67.03/67.10 cnf(584,plain, % 67.03/67.10 (P1(f1(x5841,f2(x5842,x5841)),f1(f2(x5841,x5843),x5841))), % 67.03/67.10 inference(scs_inference,[],[206,580,15])). % 67.03/67.10 cnf(588,plain, % 67.03/67.10 (P1(f1(f2(x5881,x5882),x5881),f1(x5881,f2(x5883,x5881)))), % 67.03/67.10 inference(scs_inference,[],[206,582,14])). % 67.03/67.10 cnf(599,plain, % 67.03/67.10 (P1(f1(x5991,f2(x5992,x5991)),f1(f3(x5991,x5993),f2(x5991,x5993)))), % 67.03/67.10 inference(scs_inference,[],[237,584,15])). % 67.03/67.10 cnf(609,plain, % 67.03/67.10 (P1(f1(f3(x6091,x6092),f2(x6091,x6092)),f1(x6091,f2(x6093,x6091)))), % 67.03/67.10 inference(scs_inference,[],[237,588,14])). % 67.03/67.10 cnf(612,plain, % 67.03/67.10 (E(f1(f1(f3(x6121,x6122),f2(x6121,x6122)),f2(x6121,x6123)),f1(f2(x6121,x6124),f3(x6121,x6124)))), % 67.03/67.10 inference(scs_inference,[],[239,127,3])). % 67.03/67.10 cnf(620,plain, % 67.03/67.10 (E(f1(f2(x6201,x6202),f3(x6201,x6202)),f1(f1(f3(x6201,x6203),f2(x6201,x6203)),f2(x6201,x6204)))), % 67.03/67.10 inference(scs_inference,[],[612,2])). % 67.03/67.10 cnf(621,plain, % 67.03/67.10 (E(f1(f1(f3(x6211,x6212),f2(x6211,x6212)),f2(x6211,x6213)),f1(f3(x6211,x6214),f2(x6211,x6214)))), % 67.03/67.10 inference(scs_inference,[],[239,142,612,2,3])). % 67.03/67.10 cnf(623,plain, % 67.03/67.10 (E(f1(f1(f3(x6231,x6232),f2(x6231,x6232)),x6233),f1(x6231,x6233))), % 67.03/67.10 inference(rename_variables,[],[239])). % 67.03/67.10 cnf(624,plain, % 67.03/67.10 (P1(f1(x6241,f1(f3(x6242,x6243),f2(x6242,x6243))),f1(x6242,x6241))), % 67.03/67.10 inference(scs_inference,[],[239,623,142,612,44,2,3,15])). % 67.03/67.10 cnf(625,plain, % 67.03/67.10 (P1(f1(x6251,x6252),f1(x6252,x6251))), % 67.03/67.10 inference(rename_variables,[],[44])). % 67.03/67.10 cnf(626,plain, % 67.03/67.10 (P1(f1(x6261,x6262),f1(x6262,f1(f3(x6261,x6263),f2(x6261,x6263))))), % 67.03/67.10 inference(scs_inference,[],[239,623,142,612,44,625,2,3,15,14])). % 67.03/67.10 cnf(630,plain, % 67.03/67.10 (E(f1(f1(f3(x6301,x6302),f2(x6301,x6302)),f2(x6301,x6303)),f1(f2(x6304,x6301),x6301))), % 67.03/67.10 inference(scs_inference,[],[239,370,621,2,3])). % 67.03/67.10 cnf(632,plain, % 67.03/67.10 (E(f1(f1(f3(x6321,x6322),f2(x6321,x6322)),x6323),f1(x6321,x6323))), % 67.03/67.10 inference(rename_variables,[],[239])). % 67.03/67.10 cnf(637,plain, % 67.03/67.10 (E(f1(f2(x6371,x6372),f1(x6373,f3(x6371,x6372))),f1(x6371,x6373))), % 67.03/67.10 inference(scs_inference,[],[239,632,370,621,93,95,2,3,15,14,28])). % 67.03/67.10 cnf(641,plain, % 67.03/67.10 (E(f1(f1(f3(x6411,x6412),f2(x6411,x6412)),f2(x6411,x6413)),f1(f2(x6414,x6411),f3(x6411,x6414)))), % 67.03/67.10 inference(scs_inference,[],[239,298,637,2,3])). % 67.03/67.10 cnf(643,plain, % 67.03/67.10 (E(f1(f1(f3(x6431,x6432),f2(x6431,x6432)),x6433),f1(x6431,x6433))), % 67.03/67.10 inference(rename_variables,[],[239])). % 67.03/67.10 cnf(648,plain, % 67.03/67.10 (E(f1(f3(x6481,x6482),f1(f2(x6481,x6482),x6483)),f1(x6481,x6483))), % 67.03/67.10 inference(scs_inference,[],[239,643,298,637,62,64,2,3,15,14,28])). % 67.03/67.10 cnf(651,plain, % 67.03/67.10 (E(f1(f1(f3(x6511,x6512),f2(x6511,x6512)),f2(x6511,x6513)),f1(f2(x6511,x6514),x6511))), % 67.03/67.10 inference(scs_inference,[],[239,206,648,2,3])). % 67.03/67.10 cnf(653,plain, % 67.03/67.10 (E(f1(f1(f3(x6531,x6532),f2(x6531,x6532)),x6533),f1(x6531,x6533))), % 67.03/67.10 inference(rename_variables,[],[239])). % 67.03/67.10 cnf(655,plain, % 67.03/67.10 (P1(f1(f1(x6551,x6552),x6553),f1(f1(x6553,x6551),x6552))), % 67.03/67.10 inference(rename_variables,[],[88])). % 67.03/67.10 cnf(656,plain, % 67.03/67.10 (P1(f1(x6561,x6562),f1(f1(x6562,f3(x6561,x6563)),f2(x6561,x6563)))), % 67.03/67.10 inference(scs_inference,[],[239,653,206,648,88,655,2,3,15,14])). % 67.03/67.10 cnf(662,plain, % 67.03/67.10 (P1(f1(x6621,x6622),f1(f1(f2(x6621,x6623),x6622),f3(x6621,x6623)))), % 67.03/67.10 inference(scs_inference,[],[59,641,656,2,15])). % 67.03/67.10 cnf(677,plain, % 67.03/67.10 (P1(f1(f1(f3(x6771,x6772),f2(x6771,x6772)),f1(x6773,x6774)),f1(f1(x6771,x6773),x6774))), % 67.03/67.10 inference(scs_inference,[],[239,51,27,15])). % 67.03/67.10 cnf(679,plain, % 67.03/67.10 (E(f1(f1(f3(x6791,x6792),f2(x6791,x6792)),f1(x6793,x6794)),f1(f1(x6791,x6793),x6794))+~P1(f1(f1(x6791,x6793),x6794),f1(f1(f3(x6791,x6792),f2(x6791,x6792)),f1(x6793,x6794)))), % 67.03/67.10 inference(scs_inference,[],[651,677,2,28])). % 67.03/67.10 cnf(681,plain, % 67.03/67.10 (~P1(f1(f1(x6811,x6812),x6813),f1(f1(f3(x6811,x6814),f2(x6811,x6814)),f1(x6812,x6813)))+E(f1(f1(x6811,x6812),x6813),f1(f1(f3(x6811,x6814),f2(x6811,x6814)),f1(x6812,x6813)))), % 67.03/67.10 inference(scs_inference,[],[679,2])). % 67.03/67.10 cnf(704,plain, % 67.03/67.10 (E(f1(x7041,f2(x7042,x7041)),f1(f3(x7041,x7043),f2(x7041,x7043)))), % 67.03/67.10 inference(scs_inference,[],[599,609,28])). % 67.03/67.10 cnf(709,plain, % 67.03/67.10 (E(f1(x7091,x7092),f1(f1(f3(x7091,x7093),f2(x7091,x7093)),x7092))), % 67.03/67.10 inference(rename_variables,[],[240])). % 67.03/67.10 cnf(714,plain, % 67.03/67.10 (E(f1(f2(x7141,x7142),f3(x7141,x7142)),f1(x7141,f2(x7143,x7141)))), % 67.03/67.10 inference(scs_inference,[],[240,709,155,93,95,599,609,28,15,14,2,3])). % 67.03/67.10 cnf(717,plain, % 67.03/67.10 (P1(f1(f1(x7171,x7172),x7173),f1(f1(f3(x7171,x7174),f2(x7171,x7174)),f1(x7172,x7173)))), % 67.03/67.10 inference(scs_inference,[],[240,714,64,2,15])). % 67.03/67.10 cnf(719,plain, % 67.03/67.10 (E(f1(x7191,x7192),f1(f1(f3(x7191,x7193),f2(x7191,x7193)),x7192))), % 67.03/67.10 inference(rename_variables,[],[240])). % 67.03/67.10 cnf(720,plain, % 67.03/67.10 (P1(f1(f1(f3(x7201,x7202),f2(x7201,x7202)),f2(x7201,x7203)),x7201)), % 67.03/67.10 inference(scs_inference,[],[240,719,714,64,129,2,15,14])). % 67.03/67.10 cnf(729,plain, % 67.03/67.10 (E(f1(x7291,x7292),f1(f1(f3(x7291,x7293),f2(x7291,x7293)),x7292))), % 67.03/67.10 inference(rename_variables,[],[240])). % 67.03/67.10 cnf(733,plain, % 67.03/67.10 (E(f1(f1(f3(x7331,x7332),f2(x7331,x7332)),f2(x7331,x7333)),x7331)), % 67.03/67.10 inference(scs_inference,[],[240,729,131,363,720,717,681,2,15,14,28])). % 67.03/67.10 cnf(737,plain, % 67.03/67.10 (E(x7371,f1(f1(f3(x7371,x7372),f2(x7371,x7372)),f2(x7371,x7373)))), % 67.03/67.10 inference(scs_inference,[],[733,2])). % 67.03/67.10 cnf(766,plain, % 67.03/67.10 (P1(x7661,f1(f1(f3(x7661,x7662),f2(x7661,x7662)),f2(x7663,x7661)))), % 67.03/67.10 inference(scs_inference,[],[240,542,15])). % 67.03/67.10 cnf(768,plain, % 67.03/67.10 (E(f1(x7681,x7682),f1(f1(f3(x7681,x7683),f2(x7681,x7683)),x7682))), % 67.03/67.10 inference(rename_variables,[],[240])). % 67.03/67.10 cnf(769,plain, % 67.03/67.10 (P1(f1(f1(f3(x7691,x7692),f2(x7691,x7692)),f2(x7693,x7691)),x7691)), % 67.03/67.10 inference(scs_inference,[],[240,768,540,542,15,14])). % 67.03/67.10 cnf(776,plain, % 67.03/67.10 (P1(f1(f3(x7761,x7762),f2(x7761,x7762)),f1(f1(f3(x7761,x7763),f2(x7761,x7763)),f2(x7764,x7761)))), % 67.03/67.10 inference(scs_inference,[],[240,766,769,609,28,15])). % 67.03/67.10 cnf(778,plain, % 67.03/67.10 (E(f1(x7781,x7782),f1(f1(f3(x7781,x7783),f2(x7781,x7783)),x7782))), % 67.03/67.10 inference(rename_variables,[],[240])). % 67.03/67.10 cnf(779,plain, % 67.03/67.10 (P1(f1(f1(f3(x7791,x7792),f2(x7791,x7792)),f2(x7793,x7791)),f1(f3(x7791,x7794),f2(x7791,x7794)))), % 67.03/67.10 inference(scs_inference,[],[240,778,766,769,599,609,28,15,14])). % 67.03/67.10 cnf(784,plain, % 67.03/67.10 (P1(f1(f3(x7841,x7842),f2(x7842,x7841)),f1(f1(f3(x7841,x7843),f2(x7841,x7843)),f2(x7841,x7844)))), % 67.03/67.10 inference(scs_inference,[],[240,471,15])). % 67.03/67.10 cnf(786,plain, % 67.03/67.10 (E(f1(x7861,x7862),f1(f1(f3(x7861,x7863),f2(x7861,x7863)),x7862))), % 67.03/67.10 inference(rename_variables,[],[240])). % 67.03/67.10 cnf(787,plain, % 67.03/67.10 (P1(f1(f1(f3(x7871,x7872),f2(x7871,x7872)),f2(x7871,x7873)),f1(f3(x7871,x7874),f2(x7874,x7871)))), % 67.03/67.10 inference(scs_inference,[],[240,786,471,475,15,14])). % 67.03/67.10 cnf(817,plain, % 67.03/67.10 (P1(x8171,x8172)+P2(f5(x8171,x8172),f1(x8173,x8171))), % 67.03/67.10 inference(scs_inference,[],[29,31])). % 67.03/67.10 cnf(824,plain, % 67.03/67.10 (P1(x8241,x8242)+P2(f5(x8241,x8242),f1(f1(x8243,x8241),x8244))), % 67.03/67.10 inference(scs_inference,[],[817,32])). % 67.03/67.10 cnf(831,plain, % 67.03/67.10 (P1(x8311,f1(f1(x8312,x8311),x8313))), % 67.03/67.10 inference(scs_inference,[],[824,35])). % 67.03/67.10 cnf(872,plain, % 67.03/67.10 (P1(f1(f2(x8721,x8722),f1(f2(x8721,x8723),f3(x8721,x8722))),x8721)), % 67.03/67.10 inference(scs_inference,[],[75,720,14])). % 67.03/67.10 cnf(874,plain, % 67.03/67.10 (P1(x8741,f1(x8742,f1(f1(x8743,x8741),x8744)))), % 67.03/67.10 inference(scs_inference,[],[86,75,831,720,14,15])). % 67.03/67.10 cnf(917,plain, % 67.03/67.10 (E(f1(f1(f2(x9171,x9172),f3(x9171,x9173)),f2(x9171,x9173)),f1(f2(x9171,x9174),f3(x9171,x9174)))), % 67.03/67.10 inference(scs_inference,[],[67,612,624,626,28,3])). % 67.03/67.10 cnf(919,plain, % 67.03/67.10 (P1(f1(f2(x9191,x9192),f1(f3(x9192,x9193),f2(x9192,x9193))),x9192)), % 67.03/67.10 inference(scs_inference,[],[245,67,612,624,422,626,28,3,14])). % 67.03/67.10 cnf(921,plain, % 67.03/67.10 (E(f1(x9211,x9212),f1(x9211,f1(f3(x9212,x9213),f2(x9212,x9213))))), % 67.03/67.10 inference(rename_variables,[],[245])). % 67.03/67.10 cnf(922,plain, % 67.03/67.10 (P1(x9221,f1(f2(x9222,x9221),f1(f3(x9221,x9223),f2(x9221,x9223))))), % 67.03/67.10 inference(scs_inference,[],[245,921,67,612,624,427,422,626,28,3,14,15])). % 67.03/67.10 cnf(930,plain, % 67.03/67.10 (E(f1(f1(f2(x9301,x9302),f3(x9301,x9303)),f2(x9301,x9303)),f1(f3(x9301,x9304),f2(x9301,x9304)))), % 67.03/67.10 inference(scs_inference,[],[67,621,917,919,922,2,28,3])). % 67.03/67.10 cnf(932,plain, % 67.03/67.10 (P1(f1(f2(x9321,x9322),f1(f3(x9321,x9323),f2(x9321,x9323))),x9321)), % 67.03/67.10 inference(scs_inference,[],[245,67,621,917,144,919,922,2,28,3,14])). % 67.03/67.10 cnf(934,plain, % 67.03/67.10 (E(f1(x9341,x9342),f1(x9341,f1(f3(x9342,x9343),f2(x9342,x9343))))), % 67.03/67.10 inference(rename_variables,[],[245])). % 67.03/67.10 cnf(935,plain, % 67.03/67.10 (P1(x9351,f1(f2(x9351,x9352),f1(f3(x9351,x9353),f2(x9351,x9353))))), % 67.03/67.10 inference(scs_inference,[],[245,934,67,621,917,146,144,919,922,2,28,3,14,15])). % 67.03/67.10 cnf(942,plain, % 67.03/67.10 (E(f1(f1(f2(x9421,x9422),f3(x9421,x9423)),f2(x9421,x9423)),f1(f2(x9424,x9421),f3(x9421,x9424)))), % 67.03/67.10 inference(scs_inference,[],[67,641,930,932,935,2,28,3])). % 67.03/67.10 cnf(945,plain, % 67.03/67.10 (E(f1(x9451,f1(x9452,x9453)),f1(x9453,f1(x9451,x9452)))), % 67.03/67.10 inference(rename_variables,[],[86])). % 67.03/67.10 cnf(946,plain, % 67.03/67.10 (P1(x9461,f1(f2(x9461,x9462),f1(f2(x9461,x9463),f3(x9461,x9462))))), % 67.03/67.10 inference(scs_inference,[],[86,945,67,641,930,872,932,935,2,28,3,14,15])). % 67.03/67.10 cnf(952,plain, % 67.03/67.10 (E(f1(f1(f2(x9521,x9522),f3(x9521,x9523)),f2(x9521,x9523)),f1(f2(x9524,x9521),x9521))), % 67.03/67.10 inference(scs_inference,[],[67,630,942,872,946,2,28,3])). % 67.03/67.10 cnf(958,plain, % 67.03/67.10 (E(f1(f1(f2(x9581,x9582),f3(x9581,x9583)),f2(x9581,x9583)),f1(f2(x9581,x9584),x9581))), % 67.03/67.10 inference(scs_inference,[],[67,651,952,919,922,2,28,3])). % 67.03/67.10 cnf(960,plain, % 67.03/67.10 (E(f1(f2(x9601,x9602),x9601),f1(f1(f2(x9601,x9603),f3(x9601,x9604)),f2(x9601,x9604)))), % 67.03/67.10 inference(scs_inference,[],[958,2])). % 67.03/67.10 cnf(964,plain, % 67.03/67.10 (E(f1(f1(f2(x9641,x9642),f2(x9641,x9643)),f3(x9641,x9642)),f1(f2(x9641,x9644),x9641))), % 67.03/67.10 inference(scs_inference,[],[67,958,872,946,2,28,3])). % 67.03/67.10 cnf(966,plain, % 67.03/67.10 (E(f1(f2(x9661,x9662),x9661),f1(f1(f2(x9661,x9663),f2(x9661,x9664)),f3(x9661,x9663)))), % 67.03/67.10 inference(scs_inference,[],[964,2])). % 67.03/67.10 cnf(970,plain, % 67.03/67.10 (E(f1(f1(f2(x9701,x9702),f2(x9701,x9703)),f3(x9701,x9702)),f1(f2(x9701,x9704),f3(x9701,x9704)))), % 67.03/67.10 inference(scs_inference,[],[67,964,917,932,935,2,28,3])). % 67.03/67.10 cnf(973,plain, % 67.03/67.10 (E(f1(f3(x9731,x9732),f2(x9731,x9732)),f1(f1(f2(x9731,x9733),f2(x9731,x9734)),f3(x9731,x9733)))), % 67.03/67.10 inference(scs_inference,[],[241,970,966,2,3])). % 67.03/67.10 cnf(978,plain, % 67.03/67.10 (E(f1(f1(f2(x9781,x9782),f2(x9781,x9783)),f3(x9781,x9782)),f1(f2(x9784,x9781),f3(x9781,x9784)))), % 67.03/67.10 inference(scs_inference,[],[67,973,942,2,3])). % 67.03/67.10 cnf(983,plain, % 67.03/67.10 (E(f1(f3(x9831,x9832),f2(x9831,x9832)),f1(f1(f3(x9831,x9833),f2(x9831,x9833)),f2(x9834,x9831)))), % 67.03/67.10 inference(scs_inference,[],[978,776,779,2,28])). % 67.03/67.10 cnf(989,plain, % 67.03/67.10 (E(f1(f3(x9891,x9892),f2(x9892,x9891)),f1(f1(f3(x9891,x9893),f2(x9891,x9893)),f2(x9891,x9894)))), % 67.03/67.10 inference(scs_inference,[],[983,784,787,2,28])). % 67.03/67.10 cnf(994,plain, % 67.03/67.10 (E(f1(f1(f3(x9941,x9942),f2(x9941,x9942)),f2(x9941,x9943)),f1(f3(x9941,x9944),f2(x9944,x9941)))), % 67.03/67.10 inference(scs_inference,[],[989,2])). % 67.03/67.10 cnf(1031,plain, % 67.03/67.10 (P1(f1(x10311,x10312),f1(f3(x10312,x10313),f1(f2(x10312,x10313),x10311)))), % 67.03/67.10 inference(scs_inference,[],[244,82,14])). % 67.03/67.10 cnf(1032,plain, % 67.03/67.10 (P1(f1(x10321,f1(x10322,x10323)),f1(x10322,f1(x10323,x10321)))), % 67.03/67.10 inference(rename_variables,[],[82])). % 67.03/67.10 cnf(1033,plain, % 67.03/67.10 (P1(f1(f2(x10331,x10332),f1(x10333,f3(x10331,x10332))),f1(x10333,x10331))), % 67.03/67.10 inference(scs_inference,[],[244,82,1032,14,15])). % 67.03/67.10 cnf(1036,plain, % 67.03/67.10 (P1(f1(x10361,x10362),f1(f2(x10362,x10363),f1(x10361,f3(x10362,x10363))))), % 67.03/67.10 inference(scs_inference,[],[244,84,14])). % 67.03/67.10 cnf(1048,plain, % 67.03/67.10 (P1(f1(f3(x10481,x10482),f1(f2(x10481,x10482),x10483)),f1(x10483,x10481))), % 67.03/67.10 inference(scs_inference,[],[244,84,95,14,15])). % 67.13/67.10 cnf(1180,plain, % 67.13/67.10 (E(f1(f2(x11801,x11802),f3(x11802,x11801)),f1(f2(x11803,x11802),f3(x11802,x11803)))), % 67.13/67.10 inference(scs_inference,[],[278,287,3])). % 67.13/67.10 cnf(1249,plain, % 67.13/67.10 (E(f1(x12491,f2(x12491,x12492)),f1(f2(x12493,x12491),f3(x12491,x12493)))), % 67.13/67.10 inference(rename_variables,[],[298])). % 67.13/67.10 cnf(1250,plain, % 67.13/67.10 (P1(f1(f2(x12501,x12502),f3(x12502,x12501)),f1(f1(f2(x12502,x12503),f2(x12502,x12504)),f3(x12502,x12503)))), % 67.13/67.10 inference(scs_inference,[],[298,1249,620,662,3,14])). % 67.13/67.10 cnf(1256,plain, % 67.13/67.10 (E(f1(x12561,f2(x12561,x12562)),f1(f2(x12563,x12561),f3(x12561,x12563)))), % 67.13/67.10 inference(rename_variables,[],[298])). % 67.13/67.10 cnf(1259,plain, % 67.13/67.10 (E(f1(x12591,f2(x12592,x12591)),f1(x12591,f2(x12591,x12593)))), % 67.13/67.10 inference(scs_inference,[],[298,1256,714,656,3,14,2])). % 67.13/67.10 cnf(1284,plain, % 67.13/67.10 (P1(f2(x12841,x12842),f1(f2(f2(x12842,x12841),x12843),f2(x12841,x12842)))), % 67.13/67.10 inference(scs_inference,[],[300,44,14])). % 67.13/67.10 cnf(1288,plain, % 67.13/67.10 (P1(f2(x12881,x12882),f1(f2(x12883,f2(x12882,x12881)),f2(x12881,x12882)))), % 67.13/67.10 inference(scs_inference,[],[300,446,14])). % 67.13/67.10 cnf(1290,plain, % 67.13/67.10 (P1(f1(f2(x12901,f2(x12902,x12903)),f2(x12903,x12902)),f2(x12903,x12902))), % 67.13/67.10 inference(scs_inference,[],[300,446,430,14,15])). % 67.13/67.10 cnf(1305,plain, % 67.13/67.10 (P1(x13051,f1(x13052,f1(x13053,x13051)))), % 67.13/67.10 inference(scs_inference,[],[323,874,44,14,15])). % 67.13/67.10 cnf(1317,plain, % 67.13/67.10 (P1(x13171,f1(x13171,x13172))), % 67.13/67.10 inference(scs_inference,[],[323,1305,15])). % 67.13/67.10 cnf(1446,plain, % 67.13/67.10 (P1(f1(f2(x14461,x14462),x14462),f1(f1(f2(x14462,x14463),f2(x14462,x14464)),f3(x14462,x14463)))), % 67.13/67.10 inference(scs_inference,[],[337,1250,14])). % 67.13/67.10 cnf(1515,plain, % 67.13/67.10 (P1(f1(f2(x15151,x15152),f1(f2(x15153,x15151),f3(x15151,x15152))),x15151)), % 67.13/67.10 inference(scs_inference,[],[75,769,14])). % 67.13/67.10 cnf(1525,plain, % 67.13/67.10 (P1(f1(f1(f2(x15251,x15252),f2(x15251,x15253)),f3(x15251,x15252)),f1(f3(x15251,x15254),f2(x15254,x15251)))), % 67.13/67.10 inference(scs_inference,[],[67,787,14])). % 67.13/67.10 cnf(1630,plain, % 67.13/67.10 (P1(x16301,f1(f2(x16301,x16302),f1(f2(x16303,x16301),f3(x16301,x16302))))), % 67.13/67.10 inference(scs_inference,[],[75,766,15])). % 67.13/67.10 cnf(1640,plain, % 67.13/67.10 (E(f1(f1(x16401,x16402),x16403),f1(f1(x16402,x16403),x16401))), % 67.13/67.10 inference(rename_variables,[],[67])). % 67.13/67.10 cnf(1644,plain, % 67.13/67.10 (E(x16441,f1(f2(x16441,x16442),f1(f2(x16443,x16441),f3(x16441,x16442))))), % 67.13/67.10 inference(scs_inference,[],[67,1640,566,1525,1515,1630,28,14,15,2])). % 67.13/67.10 cnf(1654,plain, % 67.13/67.10 (E(f1(x16541,f2(x16541,x16542)),f1(f3(x16541,x16543),f2(x16543,x16541)))), % 67.13/67.10 inference(scs_inference,[],[240,994,3])). % 67.13/67.10 cnf(1658,plain, % 67.13/67.10 (E(f1(f2(x16581,x16582),f3(x16581,x16582)),f1(f3(x16581,x16583),f2(x16583,x16581)))), % 67.13/67.10 inference(scs_inference,[],[133,1654,3])). % 67.13/67.10 cnf(1661,plain, % 67.13/67.10 (E(f1(f3(x16611,x16612),f2(x16611,x16612)),f1(f3(x16611,x16613),f2(x16613,x16611)))), % 67.13/67.10 inference(scs_inference,[],[157,1658,3])). % 67.13/67.10 cnf(1663,plain, % 67.13/67.10 (E(f1(f3(x16631,x16632),f2(x16632,x16631)),f1(f3(x16631,x16633),f2(x16631,x16633)))), % 67.13/67.10 inference(scs_inference,[],[157,1658,3,2])). % 67.13/67.10 cnf(1711,plain, % 67.13/67.10 (P1(f3(x17111,x17112),f1(f2(x17113,x17111),x17111))), % 67.13/67.10 inference(scs_inference,[],[348,1317,15])). % 67.13/67.10 cnf(1753,plain, % 67.13/67.10 (P1(f3(x17531,x17532),f1(f2(x17533,x17531),f3(x17531,x17533)))), % 67.13/67.10 inference(scs_inference,[],[359,1711,15])). % 67.13/67.10 cnf(1783,plain, % 67.13/67.10 (P1(f3(x17831,x17832),f1(x17831,f2(x17831,x17833)))), % 67.13/67.10 inference(scs_inference,[],[360,1711,1446,14,15])). % 67.13/67.10 cnf(1787,plain, % 67.13/67.10 (E(f1(x17871,f2(x17871,x17872)),f3(x17871,x17873))+~P1(f1(x17871,f2(x17871,x17872)),f3(x17871,x17873))), % 67.13/67.10 inference(scs_inference,[],[360,1711,1446,14,15,28,2])). % 67.13/67.10 cnf(1809,plain, % 67.13/67.10 (~E(f1(a7,f3(a4,a7)),f1(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[457,737,960,27,5,6,7,8,9,10,11,12,13,4,2])). % 67.13/67.10 cnf(1810,plain, % 67.13/67.10 (E(f1(x18101,f2(x18102,x18101)),f1(f3(x18101,x18103),f2(x18103,x18101)))), % 67.13/67.10 inference(scs_inference,[],[457,1661,737,704,960,27,5,6,7,8,9,10,11,12,13,4,2,3])). % 67.13/67.10 cnf(1836,plain, % 67.13/67.10 (P1(f1(x18361,f2(x18362,x18361)),f1(f3(x18361,x18363),f2(x18363,x18361)))), % 67.13/67.10 inference(scs_inference,[],[1810,27])). % 67.13/67.10 cnf(1838,plain, % 67.13/67.10 (E(f2(x18381,x18382),f2(x18381,f1(f2(x18383,x18382),f3(x18382,x18383))))), % 67.13/67.10 inference(scs_inference,[],[1810,413,27,9])). % 67.13/67.10 cnf(1844,plain, % 67.13/67.10 (E(f1(x18441,x18442),f1(x18441,f1(f2(x18443,x18442),f3(x18442,x18443))))), % 67.13/67.10 inference(scs_inference,[],[1810,413,27,9,11,6,8,12,10,5])). % 67.13/67.10 cnf(1849,plain, % 67.13/67.10 (~E(f1(f2(a4,x18491),f1(f2(x18492,a4),f3(a4,x18491))),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[42,1810,1644,413,462,27,9,11,6,8,12,10,5,7,13,4,2,3])). % 67.13/67.10 cnf(1858,plain, % 67.13/67.10 (E(f5(x18581,f1(f2(x18582,x18583),f3(x18583,x18582))),f5(x18581,x18583))), % 67.13/67.10 inference(scs_inference,[],[1838,415,27,11])). % 67.13/67.10 cnf(1859,plain, % 67.13/67.10 (E(f3(f1(f2(x18591,x18592),f3(x18592,x18591)),x18593),f3(x18592,x18593))), % 67.13/67.10 inference(scs_inference,[],[1838,415,27,11,12])). % 67.13/67.10 cnf(1860,plain, % 67.13/67.10 (E(f2(f1(f2(x18601,x18602),f3(x18602,x18601)),x18603),f2(x18602,x18603))), % 67.13/67.10 inference(scs_inference,[],[1838,415,27,11,12,8])). % 67.13/67.10 cnf(1861,plain, % 67.13/67.10 (E(f2(x18611,f1(f2(x18612,x18613),f3(x18613,x18612))),f2(x18611,x18613))), % 67.13/67.10 inference(scs_inference,[],[1838,415,27,11,12,8,9])). % 67.13/67.10 cnf(1862,plain, % 67.13/67.10 (E(f1(x18621,f1(f2(x18622,x18623),f3(x18623,x18622))),f1(x18621,x18623))), % 67.13/67.10 inference(scs_inference,[],[1838,415,27,11,12,8,9,5])). % 67.13/67.10 cnf(1864,plain, % 67.13/67.10 (E(f6(x18641,f1(f2(x18642,x18643),f3(x18643,x18642))),f6(x18641,x18643))), % 67.13/67.10 inference(scs_inference,[],[1838,415,27,11,12,8,9,5,6,7])). % 67.13/67.10 cnf(1866,plain, % 67.13/67.10 (E(f1(f1(f2(x18661,x18662),f3(x18662,x18661)),x18663),f1(x18662,x18663))), % 67.13/67.10 inference(scs_inference,[],[1838,415,27,11,12,8,9,5,6,7,10,4])). % 67.13/67.10 cnf(1867,plain, % 67.13/67.10 (E(f3(x18671,f1(f2(x18672,x18673),f3(x18673,x18672))),f3(x18671,x18673))), % 67.13/67.10 inference(scs_inference,[],[1838,415,27,11,12,8,9,5,6,7,10,4,13])). % 67.13/67.10 cnf(1872,plain, % 67.13/67.10 (~E(f1(a4,f2(x18721,a4)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1290,1288,1849,1838,415,637,27,11,12,8,9,5,6,7,10,4,13,2,28,3])). % 67.13/67.10 cnf(1888,plain, % 67.13/67.10 (E(f1(f1(f2(x18881,x18882),x18882),x18883),f1(x18882,x18883))), % 67.13/67.10 inference(scs_inference,[],[1858,434,27,12,5,11,9,7,8,10,6,13,4])). % 67.13/67.10 cnf(1890,plain, % 67.13/67.10 (~P1(f1(a4,f2(a4,a4)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1872,1858,1783,434,27,12,5,11,9,7,8,10,6,13,4,2,28])). % 67.13/67.10 cnf(1894,plain, % 67.13/67.10 (~E(f1(f2(a4,x18941),a4),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1872,1858,1862,1783,434,1849,27,12,5,11,9,7,8,10,6,13,4,2,28,3])). % 67.13/67.10 cnf(1909,plain, % 67.13/67.10 (E(f1(x19091,x19092),f1(x19091,f1(f2(x19093,x19092),x19092)))), % 67.13/67.10 inference(scs_inference,[],[1859,432,27,5])). % 67.13/67.10 cnf(1919,plain, % 67.13/67.10 (~E(f3(a4,a7),f1(f2(a4,x19191),a4))), % 67.13/67.10 inference(scs_inference,[],[1894,1859,432,27,5,7,12,9,10,11,6,8,4,13,2])). % 67.13/67.10 cnf(1923,plain, % 67.13/67.10 (~E(f1(a4,f2(a4,x19231)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1894,1859,1031,1048,1259,432,1872,27,5,7,12,9,10,11,6,8,4,13,2,28,3])). % 67.13/67.10 cnf(1925,plain, % 67.13/67.10 (~P1(f1(f1(f2(x19251,a4),f3(a4,x19251)),f2(a4,a4)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1890,1894,1859,1866,1031,1048,1259,432,1872,27,5,7,12,9,10,11,6,8,4,13,2,28,3,14])). % 67.13/67.10 cnf(1927,plain, % 67.13/67.10 (~P1(f1(a4,f2(a4,x19271)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1890,1894,1859,1866,1031,1048,1259,432,1872,27,5,7,12,9,10,11,6,8,4,13,2,28,3,14,1787])). % 67.13/67.10 cnf(1929,plain, % 67.13/67.10 (P2(f5(f1(a4,f2(a4,x19291)),f3(a4,a7)),f1(a4,f2(a4,x19291)))), % 67.13/67.10 inference(scs_inference,[],[1890,1894,1859,1866,1031,1048,1259,432,1872,27,5,7,12,9,10,11,6,8,4,13,2,28,3,14,1787,29])). % 67.13/67.10 cnf(1931,plain, % 67.13/67.10 (~P2(f5(f1(a4,f2(a4,x19311)),f3(a4,a7)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1890,1894,1859,1866,1031,1048,1259,432,1872,27,5,7,12,9,10,11,6,8,4,13,2,28,3,14,1787,29,35])). % 67.13/67.10 cnf(1946,plain, % 67.13/67.10 (E(f1(x19461,f1(f2(x19462,x19463),x19462)),f1(x19461,x19462))), % 67.13/67.10 inference(scs_inference,[],[1925,1931,1860,179,33,35,27,10,12,7,5])). % 67.13/67.10 cnf(1960,plain, % 67.13/67.10 (~P1(f1(f2(a4,a4),a4),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1923,1919,1925,1931,1836,1860,1929,1663,1711,179,33,35,27,10,12,7,5,6,8,9,11,13,4,2,30,17,28])). % 67.13/67.10 cnf(1964,plain, % 67.13/67.10 (~E(f1(f2(a4,x19641),f1(f2(x19642,a4),f3(a4,x19642))),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1923,1919,1925,1931,1836,1860,1929,1844,1663,1894,1711,179,33,35,27,10,12,7,5,6,8,9,11,13,4,2,30,17,28,3])). % 67.13/67.10 cnf(1966,plain, % 67.13/67.10 (~P1(f1(f1(f2(x19661,a4),a4),f2(a4,x19662)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1923,1927,1919,1925,1931,1836,1860,1888,1929,1844,1663,1894,1711,179,33,35,27,10,12,7,5,6,8,9,11,13,4,2,30,17,28,3,14])). % 67.13/67.10 cnf(1982,plain, % 67.13/67.10 (E(f6(f2(x19821,x19822),x19823),f6(f2(x19822,x19821),x19823))), % 67.13/67.10 inference(scs_inference,[],[1960,1861,20,35,27,6])). % 67.13/67.10 cnf(1983,plain, % 67.13/67.10 (E(f2(f2(x19831,x19832),x19833),f2(f2(x19832,x19831),x19833))), % 67.13/67.10 inference(scs_inference,[],[1960,1861,20,35,27,6,8])). % 67.13/67.10 cnf(1984,plain, % 67.13/67.10 (E(f6(x19841,f2(x19842,x19843)),f6(x19841,f2(x19843,x19842)))), % 67.13/67.10 inference(scs_inference,[],[1960,1861,20,35,27,6,8,7])). % 67.13/67.10 cnf(1988,plain, % 67.13/67.10 (E(f3(f2(x19881,x19882),x19883),f3(f2(x19882,x19881),x19883))), % 67.13/67.10 inference(scs_inference,[],[1960,1861,20,35,27,6,8,7,10,11,5,12])). % 67.13/67.10 cnf(1998,plain, % 67.13/67.10 (~E(f1(f2(a4,x19981),f3(a4,x19981)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1960,1861,1946,1964,1036,1033,1849,20,22,35,27,6,8,7,10,11,5,12,9,13,4,2,38,28,3])). % 67.13/67.10 cnf(2027,plain, % 67.13/67.10 (E(f1(f1(x20271,x20272),x20273),f1(f1(x20272,x20271),x20273))), % 67.13/67.10 inference(scs_inference,[],[1966,1982,22,19,35,27,5,10,8,6,12,11,7,13,9,4])). % 67.13/67.10 cnf(2029,plain, % 67.13/67.10 (~P1(f1(f2(a4,a4),f3(a4,a4)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[1998,1966,1982,1753,22,19,35,27,5,10,8,6,12,11,7,13,9,4,2,28])). % 67.13/67.10 cnf(2063,plain, % 67.13/67.10 (~E(f1(f3(a4,a7),a7),f1(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[2029,1983,460,177,35,27,11,6,7,10,5,12,8,9,13,4,2])). % 67.13/67.10 cnf(2071,plain, % 67.13/67.10 (E(f1(f1(x20711,x20712),x20713),f1(f1(x20712,x20711),x20713))), % 67.13/67.10 inference(rename_variables,[],[2027])). % 67.13/67.10 cnf(2072,plain, % 67.13/67.10 (~P1(f1(f1(f3(a4,x20721),f2(x20721,a4)),f2(a4,a4)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[25,2029,1983,2027,2071,460,1290,1925,1284,177,35,27,11,6,7,10,5,12,8,9,13,4,2,38,28,3,14])). % 67.13/67.10 cnf(2093,plain, % 67.13/67.10 (E(f2(x20931,f1(x20932,x20933)),f2(x20931,f1(x20933,x20932)))), % 67.13/67.10 inference(scs_inference,[],[2072,1984,19,46,35,27,12,10,6,8,11,5,7,13,9])). % 67.13/67.10 cnf(2168,plain, % 67.13/67.10 (E(f1(x21681,x21682),f1(f1(f2(x21681,x21683),f3(x21681,x21683)),x21682))), % 67.13/67.10 inference(scs_inference,[],[1988,41,27,12,10,5,6,7,8,11,9,4])). % 67.13/67.10 cnf(2250,plain, % 67.13/67.10 (~E(f1(f1(f2(a7,x22501),f3(a7,x22501)),f3(a4,a7)),f1(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[2093,2168,396,1809,27,2,3])). % 67.13/67.10 cnf(2264,plain, % 67.13/67.10 (~E(f1(f2(x22641,a4),f3(a4,x22641)),f3(a4,a7))), % 67.13/67.10 inference(scs_inference,[],[2250,1864,1180,1998,27,2,3])). % 67.13/67.10 cnf(2287,plain, % 67.13/67.10 ($false), % 67.13/67.10 inference(scs_inference,[],[2264,1867,1909,648,2063,27,2,3]), % 67.13/67.10 ['proof']). % 67.13/67.10 % SZS output end Proof % 67.13/67.10 % Total time :66.460000s %------------------------------------------------------------------------------