%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET008+3 : TPTP v8.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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:19:58 EDT 2024 % Result : Theorem 117.30s 117.38s % Output : CNFRefutation 117.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SET008+3 : TPTP v8.2.0. Released v2.2.0. % 0.12/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 16:41:08 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 117.30/117.36 %------------------------------------------- % 117.30/117.36 % File :CSE---1.7 % 117.30/117.36 % Problem :theBenchmark % 117.30/117.36 % Transform :cnf % 117.30/117.36 % Format :tptp:raw % 117.30/117.36 % Command :java -jar mcs_scs.jar %d %s % 117.30/117.36 % 117.30/117.36 % Result :Theorem 116.770000s % 117.30/117.36 % Output :CNFRefutation 116.770000s % 117.30/117.36 %------------------------------------------- % 117.30/117.38 %-------------------------------------------------------------------------- % 117.30/117.38 % File : SET008+3 : TPTP v8.2.0. Released v2.2.0. % 117.30/117.38 % Domain : Set Theory % 117.30/117.38 % Problem : (X \ Y) ^ Y = the empty set % 117.30/117.38 % Version : [Try90] axioms : Reduced > Incomplete. % 117.30/117.38 % English : The intersection of (the difference of X and Y) and Y is the % 117.30/117.38 % empty set. % 117.30/117.38 % 117.30/117.38 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 117.30/117.38 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 117.30/117.38 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 117.30/117.38 % Source : [ILF] % 117.30/117.38 % Names : BOOLE (78) [TS89] % 117.30/117.38 % 117.30/117.38 % Status : Theorem % 117.30/117.38 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.13 v6.4.0, 0.12 v6.3.0, 0.21 v6.2.0, 0.20 v6.1.0, 0.37 v6.0.0, 0.43 v5.5.0, 0.37 v5.4.0, 0.39 v5.3.0, 0.44 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.25 v4.1.0, 0.26 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.00 v2.5.0, 0.12 v2.4.0, 0.00 v2.2.1 % 117.30/117.38 % Syntax : Number of formulae : 10 ( 4 unt; 0 def) % 117.30/117.38 % Number of atoms : 21 ( 4 equ) % 117.30/117.38 % Maximal formula atoms : 3 ( 2 avg) % 117.30/117.38 % Number of connectives : 14 ( 3 ~; 0 |; 3 &) % 117.30/117.38 % ( 7 <=>; 1 =>; 0 <=; 0 <~>) % 117.30/117.38 % Maximal formula depth : 7 ( 5 avg) % 117.30/117.38 % Maximal term depth : 3 ( 1 avg) % 117.30/117.38 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 117.30/117.38 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 117.30/117.38 % Number of variables : 22 ( 22 !; 0 ?) % 117.30/117.38 % SPC : FOF_THM_RFO_SEQ % 117.30/117.38 % 117.30/117.38 % Comments : % 117.30/117.38 %-------------------------------------------------------------------------- % 117.30/117.38 %---- line(boole - df(3),1833060) % 117.30/117.38 fof(intersection_defn,axiom, % 117.30/117.38 ! [B,C,D] : % 117.30/117.38 ( member(D,intersection(B,C)) % 117.30/117.38 <=> ( member(D,B) % 117.30/117.38 & member(D,C) ) ) ). % 117.30/117.38 % 117.30/117.38 %---- line(boole - df(4),1833078) % 117.30/117.38 fof(difference_defn,axiom, % 117.30/117.38 ! [B,C,D] : % 117.30/117.38 ( member(D,difference(B,C)) % 117.30/117.38 <=> ( member(D,B) % 117.30/117.38 & ~ member(D,C) ) ) ). % 117.30/117.38 % 117.30/117.38 %---- line(hidden - axiom135,1832636) % 117.30/117.38 fof(empty_set_defn,axiom, % 117.30/117.38 ! [B] : ~ member(B,empty_set) ). % 117.30/117.38 % 117.30/117.38 %---- line(boole - df(8),1833103) % 117.30/117.38 fof(equal_defn,axiom, % 117.30/117.38 ! [B,C] : % 117.30/117.38 ( B = C % 117.30/117.38 <=> ( subset(B,C) % 117.30/117.38 & subset(C,B) ) ) ). % 117.30/117.38 % 117.30/117.38 %---- property(commutativity,op(intersection,2,function)) % 117.30/117.38 fof(commutativity_of_intersection,axiom, % 117.30/117.38 ! [B,C] : intersection(B,C) = intersection(C,B) ). % 117.30/117.38 % 117.30/117.38 %---- line(tarski - df(3),1832749) % 117.30/117.38 fof(subset_defn,axiom, % 117.30/117.38 ! [B,C] : % 117.30/117.38 ( subset(B,C) % 117.30/117.38 <=> ! [D] : % 117.30/117.38 ( member(D,B) % 117.30/117.38 => member(D,C) ) ) ). % 117.30/117.38 % 117.30/117.38 %---- property(reflexivity,op(subset,2,predicate)) % 117.30/117.38 fof(reflexivity_of_subset,axiom, % 117.30/117.38 ! [B] : subset(B,B) ). % 117.30/117.38 % 117.30/117.38 %---- line(hidden - axiom137,1832628) % 117.30/117.38 fof(empty_defn,axiom, % 117.30/117.38 ! [B] : % 117.30/117.38 ( empty(B) % 117.30/117.38 <=> ! [C] : ~ member(C,B) ) ). % 117.30/117.38 % 117.30/117.38 %---- line(hidden - axiom138,1832615) % 117.30/117.38 fof(equal_member_defn,axiom, % 117.30/117.38 ! [B,C] : % 117.30/117.38 ( B = C % 117.30/117.38 <=> ! [D] : % 117.30/117.38 ( member(D,B) % 117.30/117.38 <=> member(D,C) ) ) ). % 117.30/117.38 % 117.30/117.38 %---- line(boole - th(78),1833894) % 117.30/117.38 fof(prove_intersection_difference_empty_set,conjecture, % 117.30/117.38 ! [B,C] : intersection(difference(B,C),C) = empty_set ). % 117.30/117.38 % 117.30/117.38 %-------------------------------------------------------------------------- % 117.30/117.38 %------------------------------------------- % 117.30/117.38 % Proof found % 117.30/117.38 % SZS status Theorem for theBenchmark % 117.30/117.38 % SZS output start Proof % 117.30/117.39 %ClaNum:37(EqnAxiom:17) % 117.30/117.39 %VarNum:89(SingletonVarNum:40) % 117.30/117.39 %MaxLitNum:3 % 117.30/117.39 %MaxfuncDepth:2 % 117.30/117.39 %SharedTerms:6 % 117.30/117.39 %goalClause: 21 % 117.30/117.39 %singleGoalClaCount:1 % 117.30/117.39 [21]~E(f1(f3(a4,a8),a8),a2) % 117.30/117.39 [18]P1(x181,x181) % 117.30/117.39 [20]~P2(x201,a2) % 117.30/117.39 [19]E(f1(x191,x192),f1(x192,x191)) % 117.30/117.39 [24]P3(x241)+P2(f5(x241),x241) % 117.30/117.39 [23]~E(x231,x232)+P1(x231,x232) % 117.30/117.39 [25]~P3(x251)+~P2(x252,x251) % 117.30/117.39 [27]P1(x271,x272)+P2(f6(x271,x272),x271) % 117.30/117.39 [33]P1(x331,x332)+~P2(f6(x331,x332),x332) % 117.30/117.39 [30]P2(x301,x302)+~P2(x301,f1(x303,x302)) % 117.30/117.39 [31]P2(x311,x312)+~P2(x311,f1(x312,x313)) % 117.30/117.39 [32]P2(x321,x322)+~P2(x321,f3(x322,x323)) % 117.30/117.39 [36]~P2(x361,x362)+~P2(x361,f3(x363,x362)) % 117.30/117.39 [26]~P1(x262,x261)+~P1(x261,x262)+E(x261,x262) % 117.30/117.39 [34]E(x341,x342)+P2(f7(x341,x342),x342)+P2(f7(x341,x342),x341) % 117.30/117.39 [37]E(x371,x372)+~P2(f7(x371,x372),x372)+~P2(f7(x371,x372),x371) % 117.30/117.39 [28]~P1(x283,x282)+P2(x281,x282)+~P2(x281,x283) % 117.30/117.39 [29]~P2(x291,x293)+P2(x291,x292)+P2(x291,f3(x293,x292)) % 117.30/117.39 [35]~P2(x351,x353)+~P2(x351,x352)+P2(x351,f1(x352,x353)) % 117.30/117.39 %EqnAxiom % 117.30/117.39 [1]E(x11,x11) % 117.30/117.39 [2]E(x22,x21)+~E(x21,x22) % 117.30/117.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.30/117.39 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 117.30/117.39 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 117.30/117.39 [6]~E(x61,x62)+E(f7(x61,x63),f7(x62,x63)) % 117.30/117.39 [7]~E(x71,x72)+E(f7(x73,x71),f7(x73,x72)) % 117.30/117.39 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83)) % 117.30/117.39 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92)) % 117.30/117.39 [10]~E(x101,x102)+E(f6(x101,x103),f6(x102,x103)) % 117.30/117.39 [11]~E(x111,x112)+E(f6(x113,x111),f6(x113,x112)) % 117.30/117.39 [12]~E(x121,x122)+E(f5(x121),f5(x122)) % 117.30/117.39 [13]P1(x132,x133)+~E(x131,x132)+~P1(x131,x133) % 117.30/117.39 [14]P1(x143,x142)+~E(x141,x142)+~P1(x143,x141) % 117.30/117.39 [15]P2(x152,x153)+~E(x151,x152)+~P2(x151,x153) % 117.30/117.39 [16]P2(x163,x162)+~E(x161,x162)+~P2(x163,x161) % 117.30/117.39 [17]~P3(x171)+P3(x172)+~E(x171,x172) % 117.30/117.39 % 117.30/117.39 %------------------------------------------- % 117.40/117.41 cnf(39,plain, % 117.40/117.41 (P1(a2,x391)), % 117.40/117.41 inference(scs_inference,[],[20,27])). % 117.40/117.41 cnf(40,plain, % 117.40/117.41 (~P2(x401,a2)), % 117.40/117.41 inference(rename_variables,[],[20])). % 117.40/117.41 cnf(42,plain, % 117.40/117.41 (P3(a2)), % 117.40/117.41 inference(scs_inference,[],[20,40,27,24])). % 117.40/117.41 cnf(45,plain, % 117.40/117.41 (P1(f1(x451,x452),f1(x452,x451))), % 117.40/117.41 inference(scs_inference,[],[18,20,40,19,27,24,13])). % 117.40/117.41 cnf(47,plain, % 117.40/117.41 (~P3(f1(x471,x472))+P3(f1(x472,x471))), % 117.40/117.41 inference(scs_inference,[],[18,20,40,19,27,24,13,17])). % 117.40/117.41 cnf(48,plain, % 117.40/117.41 (P1(x481,x482)+~E(a2,x481)), % 117.40/117.41 inference(scs_inference,[],[39,13])). % 117.40/117.41 cnf(51,plain, % 117.40/117.41 (~E(a2,f1(f3(a4,a8),a8))), % 117.40/117.41 inference(scs_inference,[],[21,18,39,13,26,14])). % 117.40/117.41 cnf(55,plain, % 117.40/117.41 (~E(a2,f1(a8,f3(a4,a8)))), % 117.40/117.41 inference(scs_inference,[],[51,19,3])). % 117.40/117.41 cnf(57,plain, % 117.40/117.41 (~P1(f1(f3(a4,a8),a8),a2)), % 117.40/117.41 inference(scs_inference,[],[51,39,19,3,26])). % 117.40/117.41 cnf(62,plain, % 117.40/117.41 (~P1(f1(a8,f3(a4,a8)),a2)), % 117.40/117.41 inference(scs_inference,[],[55,39,26])). % 117.40/117.41 cnf(65,plain, % 117.40/117.41 (~P2(x651,f1(x652,x653))+~P3(f1(x653,x652))), % 117.40/117.41 inference(scs_inference,[],[25,47])). % 117.40/117.41 cnf(66,plain, % 117.40/117.41 (E(f1(f1(x661,x662),x663),f1(f1(x662,x661),x663))), % 117.40/117.41 inference(scs_inference,[],[19,2,4])). % 117.40/117.41 cnf(67,plain, % 117.40/117.41 (~P3(f1(f1(x671,x672),x673))+P3(f1(f1(x672,x671),x673))), % 117.40/117.41 inference(scs_inference,[],[66,17])). % 117.40/117.41 cnf(68,plain, % 117.40/117.41 (~P3(f1(x681,f1(x682,x683)))+P3(f1(f1(x683,x682),x681))), % 117.40/117.41 inference(scs_inference,[],[66,17,47])). % 117.40/117.41 cnf(70,plain, % 117.40/117.41 (~P2(x701,f1(x702,f1(a2,x703)))), % 117.40/117.41 inference(scs_inference,[],[20,30,31])). % 117.40/117.41 cnf(71,plain, % 117.40/117.41 (P1(f1(x711,f1(a2,x712)),x713)), % 117.40/117.41 inference(scs_inference,[],[70,27])). % 117.40/117.41 cnf(72,plain, % 117.40/117.41 (~P2(x721,f1(x722,f1(a2,x723)))), % 117.40/117.41 inference(rename_variables,[],[70])). % 117.40/117.41 cnf(74,plain, % 117.40/117.41 (P3(f1(x741,f1(a2,x742)))), % 117.40/117.41 inference(scs_inference,[],[70,72,27,24])). % 117.40/117.41 cnf(75,plain, % 117.40/117.41 (~P2(x751,f1(x752,f1(a2,x753)))), % 117.40/117.41 inference(rename_variables,[],[70])). % 117.40/117.41 cnf(78,plain, % 117.40/117.41 (~P2(x781,f1(x782,f1(a2,x783)))), % 117.40/117.41 inference(rename_variables,[],[70])). % 117.40/117.41 cnf(81,plain, % 117.40/117.41 (P1(f1(f1(x811,x812),x813),f1(x813,f1(x812,x811)))), % 117.40/117.41 inference(scs_inference,[],[20,66,45,70,72,75,27,24,34,13])). % 117.40/117.41 cnf(83,plain, % 117.40/117.41 (P3(f1(f1(a2,x831),x832))), % 117.40/117.41 inference(scs_inference,[],[20,66,45,19,70,72,75,27,24,34,13,17])). % 117.40/117.41 cnf(85,plain, % 117.40/117.41 (~P2(x851,f1(f1(a2,x852),x853))), % 117.40/117.41 inference(scs_inference,[],[20,66,45,19,70,72,75,27,24,34,13,17,65])). % 117.40/117.41 cnf(90,plain, % 117.40/117.41 (~E(f1(f3(a4,a8),a8),f1(x901,f1(a2,x902)))), % 117.40/117.41 inference(scs_inference,[],[20,21,66,45,19,70,72,75,78,27,24,34,13,17,65,2,35,3])). % 117.40/117.41 cnf(91,plain, % 117.40/117.41 (~E(a8,f1(a2,x911))), % 117.40/117.41 inference(scs_inference,[],[20,21,66,45,19,70,72,75,78,27,24,34,13,17,65,2,35,3,5])). % 117.40/117.41 cnf(93,plain, % 117.40/117.41 (P1(f1(f1(a2,x931),x932),x933)), % 117.40/117.41 inference(scs_inference,[],[85,27])). % 117.40/117.41 cnf(94,plain, % 117.40/117.41 (~P2(x941,f1(f1(a2,x942),x943))), % 117.40/117.41 inference(rename_variables,[],[85])). % 117.40/117.41 cnf(100,plain, % 117.40/117.41 (~E(f1(f3(a4,a8),a8),f1(f1(a2,x1001),x1002))), % 117.40/117.41 inference(scs_inference,[],[20,90,19,85,94,27,34,3])). % 117.40/117.41 cnf(102,plain, % 117.40/117.41 (P1(f1(f1(x1021,x1022),f1(x1023,x1024)),f1(f1(x1024,x1023),f1(x1022,x1021)))), % 117.40/117.41 inference(scs_inference,[],[20,66,90,81,19,85,94,27,34,3,14])). % 117.40/117.41 cnf(105,plain, % 117.40/117.41 (~E(f1(x1051,f1(a2,x1052)),f1(f3(a4,a8),a8))), % 117.40/117.41 inference(scs_inference,[],[20,57,66,90,81,71,19,85,94,27,34,3,14,13])). % 117.40/117.41 cnf(107,plain, % 117.40/117.41 (~E(f3(a4,a8),f1(a2,x1071))), % 117.40/117.41 inference(scs_inference,[],[20,57,66,90,81,71,19,85,94,27,34,3,14,13,4])). % 117.40/117.41 cnf(108,plain, % 117.40/117.41 (E(f1(f1(a2,x1081),x1082),a2)), % 117.40/117.41 inference(scs_inference,[],[20,57,66,90,81,71,19,85,94,27,34,3,14,13,4,2])). % 117.40/117.41 cnf(109,plain, % 117.40/117.41 (~E(f1(a2,x1091),a8)), % 117.40/117.41 inference(scs_inference,[],[20,57,66,90,81,71,19,85,94,27,34,3,14,13,4,2,5])). % 117.40/117.41 cnf(118,plain, % 117.40/117.41 (~E(f1(f3(a4,a8),a8),f1(f1(x1181,a2),x1182))), % 117.40/117.41 inference(scs_inference,[],[66,100,93,105,26,3])). % 117.40/117.41 cnf(128,plain, % 117.40/117.41 (~E(f1(f3(a4,a8),a8),f1(x1281,f1(x1282,a2)))), % 117.40/117.41 inference(scs_inference,[],[118,109,71,19,26,3])). % 117.40/117.41 cnf(141,plain, % 117.40/117.41 (~P1(f1(f3(a4,a8),a8),f1(x1411,f1(a2,x1412)))), % 117.40/117.41 inference(scs_inference,[],[105,71,26])). % 117.40/117.41 cnf(142,plain, % 117.40/117.41 (P1(f1(x1421,f1(a2,x1422)),x1423)), % 117.40/117.41 inference(rename_variables,[],[71])). % 117.40/117.41 cnf(144,plain, % 117.40/117.41 (~E(f1(x1441,f1(a2,x1442)),f1(a8,f3(a4,a8)))), % 117.40/117.41 inference(scs_inference,[],[62,105,71,142,26,13])). % 117.40/117.41 cnf(146,plain, % 117.40/117.41 (~E(f1(a2,x1461),f3(a4,a8))), % 117.40/117.41 inference(scs_inference,[],[62,105,71,142,26,13,5])). % 117.40/117.41 cnf(148,plain, % 117.40/117.41 (~P1(f1(a8,f3(a4,a8)),f1(f1(a2,x1481),f1(a2,x1482)))), % 117.40/117.41 inference(scs_inference,[],[144,93,26])). % 117.40/117.41 cnf(152,plain, % 117.40/117.41 (~E(f1(f1(a2,x1521),x1522),f1(f3(a4,a8),a8))), % 117.40/117.41 inference(scs_inference,[],[141,45,144,93,26,13])). % 117.40/117.41 cnf(156,plain, % 117.40/117.41 (P3(f1(f1(x1561,a2),f1(x1562,x1563)))), % 117.40/117.41 inference(scs_inference,[],[74,67,68])). % 117.40/117.41 cnf(157,plain, % 117.40/117.41 (~P2(x1571,f1(f1(x1572,a2),f1(x1573,x1574)))), % 117.40/117.41 inference(scs_inference,[],[156,25])). % 117.40/117.41 cnf(159,plain, % 117.40/117.41 (P1(f1(f1(x1591,a2),f1(x1592,x1593)),x1594)), % 117.40/117.41 inference(scs_inference,[],[156,25,27])). % 117.40/117.41 cnf(161,plain, % 117.40/117.41 (~P2(x1611,f1(f1(x1612,x1613),f1(x1614,a2)))), % 117.40/117.41 inference(scs_inference,[],[156,25,27,65])). % 117.40/117.41 cnf(169,plain, % 117.40/117.41 (P3(f1(f1(x1691,a2),x1692))), % 117.40/117.41 inference(scs_inference,[],[20,66,152,93,83,156,25,27,65,34,26,17])). % 117.40/117.41 cnf(171,plain, % 117.40/117.41 (~E(f1(f1(x1711,a2),f1(x1712,a2)),f1(a8,f3(a4,a8)))), % 117.40/117.41 inference(scs_inference,[],[20,148,66,152,102,93,83,156,25,27,65,34,26,17,13])). % 117.40/117.41 cnf(173,plain, % 117.40/117.41 (P1(f1(f1(x1731,x1732),f1(x1733,a2)),x1734)), % 117.40/117.41 inference(scs_inference,[],[20,148,66,152,102,93,83,156,25,27,65,34,26,17,13,48])). % 117.40/117.41 cnf(176,plain, % 117.40/117.41 (~P2(x1761,f1(f1(x1762,a2),x1763))), % 117.40/117.41 inference(scs_inference,[],[169,25])). % 117.40/117.41 cnf(181,plain, % 117.40/117.41 (P1(f1(f1(x1811,a2),x1812),x1813)), % 117.40/117.41 inference(scs_inference,[],[161,169,25,24,27])). % 117.40/117.41 cnf(183,plain, % 117.40/117.41 (~P2(x1831,f1(x1832,f1(x1833,a2)))), % 117.40/117.41 inference(scs_inference,[],[161,169,25,24,27,65])). % 117.40/117.41 cnf(192,plain, % 117.40/117.41 (P3(f1(x1921,f1(x1922,a2)))), % 117.40/117.41 inference(scs_inference,[],[20,159,171,19,157,161,169,25,24,27,65,34,26,17])). % 117.40/117.41 cnf(211,plain, % 117.40/117.41 (E(f1(f1(x2111,a2),x2112),a2)), % 117.40/117.41 inference(scs_inference,[],[20,57,173,176,183,27,34,13,2])). % 117.40/117.41 cnf(213,plain, % 117.40/117.41 (E(a2,f1(x2131,f1(x2132,a2)))), % 117.40/117.41 inference(scs_inference,[],[20,183,34])). % 117.40/117.41 cnf(219,plain, % 117.40/117.41 (E(f1(x2191,f1(x2192,a2)),a2)), % 117.40/117.41 inference(scs_inference,[],[20,62,93,183,34,13,2])). % 117.40/117.41 cnf(220,plain, % 117.40/117.41 (~P2(x2201,f3(a2,x2202))), % 117.40/117.41 inference(scs_inference,[],[18,20,28,32])). % 117.40/117.41 cnf(221,plain, % 117.40/117.41 (P3(f3(a2,x2211))), % 117.40/117.41 inference(scs_inference,[],[220,24])). % 117.40/117.41 cnf(222,plain, % 117.40/117.41 (~P2(x2221,f3(a2,x2222))), % 117.40/117.41 inference(rename_variables,[],[220])). % 117.40/117.41 cnf(224,plain, % 117.40/117.41 (P1(f3(a2,x2241),x2242)), % 117.40/117.41 inference(scs_inference,[],[220,222,24,27])). % 117.40/117.41 cnf(225,plain, % 117.40/117.41 (~P2(x2251,f3(a2,x2252))), % 117.40/117.41 inference(rename_variables,[],[220])). % 117.40/117.41 cnf(227,plain, % 117.40/117.41 (E(a2,f3(a2,x2271))), % 117.40/117.41 inference(scs_inference,[],[20,220,222,225,24,27,34])). % 117.40/117.41 cnf(231,plain, % 117.40/117.41 (E(f1(f1(a2,x2311),x2312),f3(a2,x2313))), % 117.40/117.41 inference(scs_inference,[],[20,108,220,222,225,24,27,34,3])). % 117.40/117.41 cnf(234,plain, % 117.40/117.41 (~E(f1(x2341,a2),f3(a4,a8))), % 117.40/117.41 inference(scs_inference,[],[20,57,108,181,220,222,225,24,27,34,3,13,4])). % 117.40/117.41 cnf(235,plain, % 117.40/117.41 (E(f3(a2,x2351),a2)), % 117.40/117.41 inference(scs_inference,[],[20,57,108,181,220,222,225,24,27,34,3,13,4,2])). % 117.40/117.41 cnf(236,plain, % 117.40/117.41 (~P2(x2361,f1(x2362,a2))), % 117.40/117.41 inference(scs_inference,[],[20,220,29,30])). % 117.40/117.41 cnf(237,plain, % 117.40/117.41 (P3(f1(x2371,a2))), % 117.40/117.41 inference(scs_inference,[],[236,24])). % 117.40/117.41 cnf(238,plain, % 117.40/117.41 (~P2(x2381,f1(x2382,a2))), % 117.40/117.41 inference(rename_variables,[],[236])). % 117.40/117.41 cnf(240,plain, % 117.40/117.41 (P1(f1(x2401,a2),x2402)), % 117.40/117.41 inference(scs_inference,[],[236,238,24,27])). % 117.40/117.41 cnf(241,plain, % 117.40/117.41 (~P2(x2411,f1(x2412,a2))), % 117.40/117.41 inference(rename_variables,[],[236])). % 117.40/117.41 cnf(243,plain, % 117.40/117.41 (~P2(x2431,f1(a2,x2432))), % 117.40/117.41 inference(scs_inference,[],[236,238,24,27,65])). % 117.40/117.41 cnf(245,plain, % 117.40/117.41 (E(f3(a2,x2451),f1(f1(a2,x2452),x2453))), % 117.40/117.41 inference(scs_inference,[],[231,236,238,24,27,65,2])). % 117.40/117.41 cnf(246,plain, % 117.40/117.41 (E(a2,f1(x2461,a2))), % 117.40/117.41 inference(scs_inference,[],[20,231,236,238,241,24,27,65,2,34])). % 117.40/117.41 cnf(250,plain, % 117.40/117.41 (E(f1(f1(x2501,a2),x2502),f3(a2,x2503))), % 117.40/117.41 inference(scs_inference,[],[20,66,231,236,238,241,24,27,65,2,34,3])). % 117.40/117.41 cnf(256,plain, % 117.40/117.41 (P3(f1(a2,x2561))), % 117.40/117.41 inference(scs_inference,[],[243,24])). % 117.40/117.41 cnf(257,plain, % 117.40/117.41 (~P2(x2571,f1(a2,x2572))), % 117.40/117.41 inference(rename_variables,[],[243])). % 117.40/117.41 cnf(259,plain, % 117.40/117.41 (P1(f1(a2,x2591),x2592)), % 117.40/117.41 inference(scs_inference,[],[243,257,24,27])). % 117.40/117.41 cnf(260,plain, % 117.40/117.41 (~P2(x2601,f1(a2,x2602))), % 117.40/117.41 inference(rename_variables,[],[243])). % 117.40/117.41 cnf(262,plain, % 117.40/117.41 (E(f3(a2,x2621),f1(f1(x2622,a2),x2623))), % 117.40/117.41 inference(scs_inference,[],[250,243,257,24,27,2])). % 117.40/117.41 cnf(266,plain, % 117.40/117.41 (E(a2,f1(a2,x2661))), % 117.40/117.41 inference(scs_inference,[],[20,250,144,243,257,260,24,27,2,26,34])). % 117.40/117.41 cnf(273,plain, % 117.40/117.41 (~E(f3(a2,x2731),f1(f3(a4,a8),a8))), % 117.40/117.41 inference(scs_inference,[],[20,57,128,250,245,144,224,243,257,260,24,27,2,26,34,3,13])). % 117.40/117.41 cnf(277,plain, % 117.40/117.41 (E(f1(x2771,a2),a2)), % 117.40/117.41 inference(scs_inference,[],[246,2])). % 117.40/117.41 cnf(282,plain, % 117.40/117.41 (~E(f1(x2821,a2),f1(a8,f3(a4,a8)))), % 117.40/117.41 inference(scs_inference,[],[62,21,246,240,273,224,2,26,3,13])). % 117.40/117.41 cnf(284,plain, % 117.40/117.41 (~E(a8,a2)), % 117.40/117.41 inference(scs_inference,[],[62,21,246,240,273,224,2,26,3,13,5])). % 117.40/117.41 cnf(285,plain, % 117.40/117.41 (~E(a2,f3(a4,a8))), % 117.40/117.41 inference(scs_inference,[],[282,5])). % 117.40/117.41 cnf(287,plain, % 117.40/117.41 (E(f1(a2,x2871),a2)), % 117.40/117.41 inference(scs_inference,[],[266,282,5,2])). % 117.40/117.41 cnf(291,plain, % 117.40/117.41 (~E(f3(a4,a8),a2)), % 117.40/117.41 inference(scs_inference,[],[57,21,266,259,282,5,2,3,13,4])). % 117.40/117.41 cnf(295,plain, % 117.40/117.41 (~E(f1(x2951,a2),a8)), % 117.40/117.41 inference(scs_inference,[],[62,181,13,4])). % 117.40/117.41 cnf(302,plain, % 117.40/117.41 (~E(a2,a8)), % 117.40/117.41 inference(scs_inference,[],[62,259,13,4])). % 117.40/117.41 cnf(317,plain, % 117.40/117.41 (E(f1(x3171,f1(a2,x3172)),f1(f1(a2,x3173),x3174))), % 117.40/117.41 inference(scs_inference,[],[70,85,34])). % 117.40/117.41 cnf(322,plain, % 117.40/117.41 (E(f1(f1(a2,x3221),x3222),f1(x3223,f1(a2,x3224)))), % 117.40/117.41 inference(scs_inference,[],[317,2])). % 117.40/117.41 cnf(323,plain, % 117.40/117.41 (E(f1(x3231,f1(a2,x3232)),f1(f1(x3233,a2),x3234))), % 117.40/117.41 inference(scs_inference,[],[317,70,176,2,34])). % 117.40/117.41 cnf(329,plain, % 117.40/117.41 (E(f1(f1(a2,x3291),x3292),f1(f1(x3293,a2),x3294))), % 117.40/117.41 inference(scs_inference,[],[323,85,176,2,34])). % 117.40/117.41 cnf(335,plain, % 117.40/117.41 (E(f1(x3351,f1(a2,x3352)),f1(x3353,f1(x3354,a2)))), % 117.40/117.41 inference(scs_inference,[],[329,70,183,2,34])). % 117.40/117.41 cnf(340,plain, % 117.40/117.41 (E(f1(f1(a2,x3401),x3402),f1(x3403,f1(x3404,a2)))), % 117.40/117.41 inference(scs_inference,[],[335,85,183,2,34])). % 117.40/117.41 cnf(346,plain, % 117.40/117.41 (E(f1(x3461,f1(a2,x3462)),f1(x3463,a2))), % 117.40/117.41 inference(scs_inference,[],[340,70,236,2,34])). % 117.40/117.41 cnf(352,plain, % 117.40/117.41 (E(f1(f1(a2,x3521),x3522),f1(a2,x3523))), % 117.40/117.41 inference(scs_inference,[],[346,85,243,2,34])). % 117.40/117.41 cnf(358,plain, % 117.40/117.41 (E(f1(x3581,f1(a2,x3582)),f1(a2,x3583))), % 117.40/117.41 inference(scs_inference,[],[352,70,243,2,34])). % 117.40/117.41 cnf(364,plain, % 117.40/117.41 (E(f1(f1(a2,x3641),x3642),f1(x3643,a2))), % 117.40/117.41 inference(scs_inference,[],[358,85,236,2,34])). % 117.40/117.41 cnf(370,plain, % 117.40/117.41 (E(f1(x3701,f1(a2,x3702)),f3(a2,x3703))), % 117.40/117.41 inference(scs_inference,[],[364,70,220,2,34])). % 117.40/117.41 cnf(375,plain, % 117.40/117.41 (E(f3(a2,x3751),f1(x3752,f1(a2,x3753)))), % 117.40/117.41 inference(scs_inference,[],[370,2])). % 117.40/117.41 cnf(402,plain, % 117.40/117.41 (~E(a8,f1(f1(a2,x4021),x4022))), % 117.40/117.41 inference(scs_inference,[],[91,322,3])). % 117.40/117.41 cnf(426,plain, % 117.40/117.41 (~E(f3(a4,a8),f1(f1(a2,x4261),x4262))), % 117.40/117.41 inference(scs_inference,[],[107,322,3])). % 117.40/117.41 cnf(440,plain, % 117.40/117.41 (~E(f3(a4,a8),f3(a2,x4401))), % 117.40/117.41 inference(scs_inference,[],[107,375,3])). % 117.40/117.41 cnf(447,plain, % 117.40/117.41 (P2(f6(f1(f3(a4,a8),a8),a2),f3(a4,a8))), % 117.40/117.41 inference(scs_inference,[],[57,27,31])). % 117.40/117.41 cnf(459,plain, % 117.40/117.41 (~P1(a8,f1(a2,x4591))), % 117.40/117.41 inference(scs_inference,[],[109,259,26])). % 117.40/117.41 cnf(464,plain, % 117.40/117.41 (P2(f6(f1(f3(a4,a8),a8),a2),a8)), % 117.40/117.41 inference(scs_inference,[],[57,27,30])). % 117.40/117.41 cnf(484,plain, % 117.40/117.41 (~P1(f3(a4,a8),f1(a2,x4841))), % 117.40/117.41 inference(scs_inference,[],[146,259,26])). % 117.40/117.41 cnf(518,plain, % 117.40/117.41 (P3(f1(x5181,f1(x5182,f1(x5183,a2))))), % 117.40/117.41 inference(scs_inference,[],[183,30,24])). % 117.40/117.41 cnf(519,plain, % 117.40/117.41 (E(f1(x5191,f1(x5192,a2)),f1(a2,x5193))), % 117.40/117.41 inference(scs_inference,[],[183,243,34])). % 117.40/117.41 cnf(543,plain, % 117.40/117.41 (P3(f1(x5431,f3(a2,x5432)))), % 117.40/117.41 inference(scs_inference,[],[220,30,24])). % 117.40/117.41 cnf(544,plain, % 117.40/117.41 (~P2(x5441,f1(x5442,f3(a2,x5443)))), % 117.40/117.41 inference(scs_inference,[],[543,25])). % 117.40/117.41 cnf(546,plain, % 117.40/117.41 (P1(f1(x5461,f3(a2,x5462)),x5463)), % 117.40/117.41 inference(scs_inference,[],[543,25,27])). % 117.40/117.41 cnf(548,plain, % 117.40/117.41 (~P2(x5481,f1(f3(a2,x5482),x5483))), % 117.40/117.41 inference(scs_inference,[],[543,25,27,65])). % 117.40/117.41 cnf(550,plain, % 117.40/117.41 (P3(f1(f3(a2,x5501),x5502))), % 117.40/117.41 inference(scs_inference,[],[19,543,25,27,65,17])). % 117.40/117.41 cnf(557,plain, % 117.40/117.41 (~E(f3(a2,x5571),f3(a4,a8))), % 117.40/117.41 inference(scs_inference,[],[220,62,236,19,543,25,27,65,17,34,13,5])). % 117.40/117.41 cnf(558,plain, % 117.40/117.41 (E(f1(x5581,a2),f3(a2,x5582))), % 117.40/117.41 inference(scs_inference,[],[220,62,236,19,543,25,27,65,17,34,13,5,2])). % 117.40/117.41 cnf(559,plain, % 117.40/117.41 (E(f1(a8,f3(a2,x5591)),a2)), % 117.40/117.41 inference(scs_inference,[],[220,62,39,236,19,543,25,27,65,17,34,13,5,2,26])). % 117.40/117.41 cnf(563,plain, % 117.40/117.41 (~E(a2,a4)), % 117.40/117.41 inference(scs_inference,[],[220,62,21,39,236,19,543,25,27,65,17,34,13,5,2,26,3,8])). % 117.40/117.41 cnf(569,plain, % 117.40/117.41 (E(f3(a2,x5691),f1(a2,x5692))), % 117.40/117.41 inference(scs_inference,[],[220,559,243,548,27,2,34])). % 117.40/117.41 cnf(573,plain, % 117.40/117.41 (~P1(f3(a4,a8),f3(a2,x5731))), % 117.40/117.41 inference(scs_inference,[],[220,559,557,224,243,548,27,2,34,26])). % 117.40/117.41 cnf(578,plain, % 117.40/117.41 (~E(f3(a2,x5781),a8)), % 117.40/117.41 inference(scs_inference,[],[220,57,559,546,557,224,243,548,27,2,34,26,13,5])). % 117.40/117.41 cnf(579,plain, % 117.40/117.41 (~P2(x5791,f1(f1(x5792,f3(a2,x5793)),x5794))), % 117.40/117.41 inference(scs_inference,[],[220,30,31])). % 117.40/117.41 cnf(581,plain, % 117.40/117.41 (E(f3(a2,x5811),f1(x5812,f3(a2,x5813)))), % 117.40/117.41 inference(scs_inference,[],[220,569,544,2,34])). % 117.40/117.41 cnf(585,plain, % 117.40/117.41 (~P1(a8,f3(a2,x5851))), % 117.40/117.41 inference(scs_inference,[],[220,569,578,224,544,2,34,26])). % 117.40/117.41 cnf(592,plain, % 117.40/117.42 (E(f3(a2,x5921),f1(f3(a2,x5922),x5923))), % 117.40/117.42 inference(scs_inference,[],[220,581,548,2,34])). % 117.40/117.42 cnf(600,plain, % 117.40/117.42 (E(f1(f3(a2,x6001),x6002),f3(a2,x6003))), % 117.40/117.42 inference(scs_inference,[],[592,2])). % 117.40/117.42 cnf(609,plain, % 117.40/117.42 (~E(f3(a4,a8),f1(f3(a2,x6091),x6092))), % 117.40/117.42 inference(scs_inference,[],[440,600,3])). % 117.40/117.42 cnf(668,plain, % 117.40/117.42 (~P2(x6681,f3(f1(a2,x6682),x6683))), % 117.40/117.42 inference(scs_inference,[],[237,32,65])). % 117.40/117.42 cnf(669,plain, % 117.40/117.42 (P3(f3(f1(a2,x6691),x6692))), % 117.40/117.42 inference(scs_inference,[],[668,24])). % 117.40/117.42 cnf(670,plain, % 117.40/117.42 (~P2(x6701,f3(f1(a2,x6702),x6703))), % 117.40/117.42 inference(rename_variables,[],[668])). % 117.40/117.42 cnf(672,plain, % 117.40/117.42 (P1(f3(f1(a2,x6721),x6722),x6723)), % 117.40/117.42 inference(scs_inference,[],[668,670,24,27])). % 117.40/117.42 cnf(673,plain, % 117.40/117.42 (~P2(x6731,f3(f1(a2,x6732),x6733))), % 117.40/117.42 inference(rename_variables,[],[668])). % 117.40/117.42 cnf(675,plain, % 117.40/117.42 (E(f1(x6751,f1(a2,x6752)),f3(f1(a2,x6753),x6754))), % 117.40/117.42 inference(scs_inference,[],[70,668,670,673,24,27,34])). % 117.40/117.42 cnf(679,plain, % 117.40/117.42 (~P1(f3(a4,a8),f1(x6791,a2))), % 117.40/117.42 inference(scs_inference,[],[234,240,70,668,670,673,24,27,34,26])). % 117.40/117.42 cnf(684,plain, % 117.40/117.42 (E(f3(f1(a2,x6841),x6842),f1(x6843,f1(a2,x6844)))), % 117.40/117.42 inference(scs_inference,[],[675,2])). % 117.40/117.42 cnf(685,plain, % 117.40/117.42 (E(f1(f1(a2,x6851),x6852),f3(f1(a2,x6853),x6854))), % 117.40/117.42 inference(scs_inference,[],[675,85,668,2,34])). % 117.40/117.42 cnf(697,plain, % 117.40/117.42 (~P2(x6971,f3(f1(x6972,a2),x6973))), % 117.40/117.42 inference(scs_inference,[],[256,32,65])). % 117.40/117.42 cnf(698,plain, % 117.40/117.42 (P3(f3(f1(x6981,a2),x6982))), % 117.40/117.42 inference(scs_inference,[],[697,24])). % 117.40/117.42 cnf(699,plain, % 117.40/117.42 (~P2(x6991,f3(f1(x6992,a2),x6993))), % 117.40/117.42 inference(rename_variables,[],[697])). % 117.40/117.42 cnf(701,plain, % 117.40/117.42 (P1(f3(f1(x7011,a2),x7012),x7013)), % 117.40/117.42 inference(scs_inference,[],[697,699,24,27])). % 117.40/117.42 cnf(702,plain, % 117.40/117.42 (~P2(x7021,f3(f1(x7022,a2),x7023))), % 117.40/117.42 inference(rename_variables,[],[697])). % 117.40/117.42 cnf(704,plain, % 117.40/117.42 (E(f3(f1(a2,x7041),x7042),f1(f1(a2,x7043),x7044))), % 117.40/117.42 inference(scs_inference,[],[685,697,699,24,27,2])). % 117.40/117.42 cnf(705,plain, % 117.40/117.42 (E(f1(x7051,f1(a2,x7052)),f3(f1(x7053,a2),x7054))), % 117.40/117.42 inference(scs_inference,[],[685,70,697,699,702,24,27,2,34])). % 117.40/117.42 cnf(714,plain, % 117.40/117.42 (E(f3(f1(x7141,a2),x7142),f1(x7143,f1(a2,x7144)))), % 117.40/117.42 inference(scs_inference,[],[705,2])). % 117.40/117.42 cnf(715,plain, % 117.40/117.42 (E(f1(f1(a2,x7151),x7152),f3(f1(x7153,a2),x7154))), % 117.40/117.42 inference(scs_inference,[],[705,85,697,2,34])). % 117.40/117.42 cnf(729,plain, % 117.40/117.42 (E(f3(f1(x7291,a2),x7292),f1(f1(a2,x7293),x7294))), % 117.40/117.42 inference(scs_inference,[],[715,2])). % 117.40/117.42 cnf(740,plain, % 117.40/117.42 (E(f1(a2,x7401),f1(x7402,a2))), % 117.40/117.42 inference(scs_inference,[],[236,243,34,2])). % 117.40/117.42 cnf(742,plain, % 117.40/117.42 (E(f1(x7421,a2),f1(x7422,f3(a2,x7423)))), % 117.40/117.42 inference(scs_inference,[],[236,544,34])). % 117.40/117.42 cnf(766,plain, % 117.40/117.42 (~P2(f6(f3(a4,a8),f1(a2,x7661)),a8)), % 117.40/117.42 inference(scs_inference,[],[484,36,27])). % 117.40/117.42 cnf(768,plain, % 117.40/117.42 (~P2(f6(f3(a4,a8),f3(a2,x7681)),a8)), % 117.40/117.42 inference(scs_inference,[],[573,36,27])). % 117.40/117.42 cnf(780,plain, % 117.40/117.42 (~P2(f6(f3(a4,a8),f1(x7801,a2)),a8)), % 117.40/117.42 inference(scs_inference,[],[679,36,27])). % 117.40/117.42 cnf(792,plain, % 117.40/117.42 (~P2(f7(f1(a2,x7921),f3(a4,a8)),a8)), % 117.40/117.42 inference(scs_inference,[],[243,146,36,34])). % 117.40/117.42 cnf(833,plain, % 117.40/117.42 (~P1(f3(a4,a8),a2)), % 117.40/117.42 inference(scs_inference,[],[285,39,26])). % 117.40/117.42 cnf(881,plain, % 117.40/117.42 (~P1(a8,f1(x8811,a2))), % 117.40/117.42 inference(scs_inference,[],[295,240,26])). % 117.40/117.42 cnf(900,plain, % 117.40/117.42 (~P1(a8,a2)), % 117.40/117.42 inference(scs_inference,[],[302,39,26])). % 117.40/117.42 cnf(954,plain, % 117.40/117.42 (~E(a8,f3(f1(a2,x9541),x9542))), % 117.40/117.42 inference(scs_inference,[],[402,684,3])). % 117.40/117.42 cnf(958,plain, % 117.40/117.42 (~E(a8,f3(f1(x9581,a2),x9582))), % 117.40/117.42 inference(scs_inference,[],[402,714,3])). % 117.40/117.42 cnf(966,plain, % 117.40/117.42 (~E(f3(a4,a8),f3(f1(a2,x9661),x9662))), % 117.40/117.42 inference(scs_inference,[],[426,704,3])). % 117.40/117.42 cnf(968,plain, % 117.40/117.42 (~E(a4,f1(a2,x9681))), % 117.40/117.42 inference(scs_inference,[],[426,704,3,8])). % 117.40/117.42 cnf(969,plain, % 117.40/117.42 (~E(f3(a4,a8),f3(f1(x9691,a2),x9692))), % 117.40/117.42 inference(scs_inference,[],[426,729,3])). % 117.40/117.42 cnf(1006,plain, % 117.40/117.42 (E(f1(x10061,f3(a2,x10062)),f1(f1(x10063,a2),x10064))), % 117.40/117.42 inference(scs_inference,[],[544,176,34])). % 117.40/117.42 cnf(1012,plain, % 117.40/117.42 (E(f1(x10121,f3(a2,x10122)),f1(x10123,f1(x10124,a2)))), % 117.40/117.42 inference(scs_inference,[],[544,1006,183,2,34])). % 117.40/117.42 cnf(1017,plain, % 117.40/117.42 (E(f1(x10171,f3(a2,x10172)),f1(f3(a2,x10173),x10174))), % 117.40/117.42 inference(scs_inference,[],[544,1012,548,2,34])). % 117.40/117.42 cnf(1023,plain, % 117.40/117.42 (E(f1(x10231,f3(a2,x10232)),a2)), % 117.40/117.42 inference(scs_inference,[],[544,1017,20,2,34])). % 117.40/117.42 cnf(1028,plain, % 117.40/117.42 (E(a2,f1(x10281,f3(a2,x10282)))), % 117.40/117.42 inference(scs_inference,[],[1023,2])). % 117.40/117.42 cnf(1029,plain, % 117.40/117.42 (E(f1(x10291,f3(a2,x10292)),f3(f1(a2,x10293),x10294))), % 117.40/117.42 inference(scs_inference,[],[544,1023,668,2,34])). % 117.40/117.42 cnf(1033,plain, % 117.40/117.42 (E(f3(f1(a2,x10331),x10332),f1(x10333,f3(a2,x10334)))), % 117.40/117.42 inference(scs_inference,[],[1029,2])). % 117.40/117.42 cnf(1034,plain, % 117.40/117.42 (E(f1(x10341,f3(a2,x10342)),f3(f1(x10343,a2),x10344))), % 117.40/117.42 inference(scs_inference,[],[544,1029,697,2,34])). % 117.40/117.42 cnf(1039,plain, % 117.40/117.42 (E(f3(f1(x10391,a2),x10392),f1(x10393,f3(a2,x10394)))), % 117.40/117.42 inference(scs_inference,[],[1034,2])). % 117.40/117.42 cnf(1041,plain, % 117.40/117.42 (E(f1(f3(a2,x10411),x10412),f1(f1(x10413,a2),x10414))), % 117.40/117.42 inference(scs_inference,[],[548,176,34])). % 117.40/117.42 cnf(1045,plain, % 117.40/117.42 (~E(f1(a2,x10451),a4)), % 117.40/117.42 inference(scs_inference,[],[966,8,2])). % 117.40/117.42 cnf(1047,plain, % 117.40/117.42 (E(f1(f3(a2,x10471),x10472),f1(x10473,f1(x10474,a2)))), % 117.40/117.42 inference(scs_inference,[],[548,1041,183,2,34])). % 117.40/117.42 cnf(1057,plain, % 117.40/117.42 (E(f1(f3(a2,x10571),x10572),a2)), % 117.40/117.42 inference(scs_inference,[],[548,1047,20,2,34])). % 117.40/117.42 cnf(1067,plain, % 117.40/117.42 (E(f1(f3(a2,x10671),x10672),f3(f1(a2,x10673),x10674))), % 117.40/117.42 inference(scs_inference,[],[548,1057,668,2,34])). % 117.40/117.42 cnf(1081,plain, % 117.40/117.42 (~P1(a4,f1(a2,x10811))), % 117.40/117.42 inference(scs_inference,[],[548,1067,1045,259,697,2,34,26])). % 117.40/117.42 cnf(1087,plain, % 117.40/117.42 (~E(f1(x10871,a2),a4)), % 117.40/117.42 inference(scs_inference,[],[969,8,2])). % 117.40/117.42 cnf(1103,plain, % 117.40/117.42 (~P1(a4,f1(x11031,a2))), % 117.40/117.42 inference(scs_inference,[],[1087,240,26])). % 117.40/117.42 cnf(1117,plain, % 117.40/117.42 (~P1(a4,a2)), % 117.40/117.42 inference(scs_inference,[],[563,39,26])). % 117.40/117.42 cnf(1275,plain, % 117.40/117.42 (~E(a4,f3(f1(a2,x12751),x12752))), % 117.40/117.42 inference(scs_inference,[],[968,1033,3])). % 117.40/117.42 cnf(1279,plain, % 117.40/117.42 (~E(a4,f3(f1(x12791,a2),x12792))), % 117.40/117.42 inference(scs_inference,[],[968,1039,3])). % 117.40/117.42 cnf(1583,plain, % 117.40/117.42 (~P2(f7(f1(a2,x15831),f3(a4,a8)),f1(x15832,a8))), % 117.40/117.42 inference(scs_inference,[],[792,30])). % 117.40/117.42 cnf(1585,plain, % 117.40/117.42 (~P2(f7(f1(a2,x15851),f3(a4,a8)),f1(a8,x15852))), % 117.40/117.42 inference(scs_inference,[],[792,30,31])). % 117.40/117.42 cnf(1587,plain, % 117.40/117.42 (~P2(f7(f1(a2,x15871),f3(a4,a8)),f3(a8,x15872))), % 117.40/117.42 inference(scs_inference,[],[792,30,31,32])). % 117.40/117.42 cnf(1590,plain, % 117.40/117.42 (E(f7(a2,x15901),f7(f3(a2,x15902),x15901))), % 117.40/117.42 inference(scs_inference,[],[792,227,30,31,32,12,6])). % 117.40/117.42 cnf(1591,plain, % 117.40/117.42 (E(f7(x15911,a2),f7(x15911,f3(a2,x15912)))), % 117.40/117.42 inference(scs_inference,[],[792,227,30,31,32,12,6,7])). % 117.40/117.42 cnf(1592,plain, % 117.40/117.42 (E(f3(x15921,a2),f3(x15921,f3(a2,x15922)))), % 117.40/117.42 inference(scs_inference,[],[792,227,30,31,32,12,6,7,9])). % 117.40/117.42 cnf(1593,plain, % 117.40/117.42 (E(f6(a2,x15931),f6(f3(a2,x15932),x15931))), % 117.40/117.42 inference(scs_inference,[],[792,227,30,31,32,12,6,7,9,10])). % 117.40/117.42 cnf(1594,plain, % 117.40/117.42 (E(f6(x15941,a2),f6(x15941,f3(a2,x15942)))), % 117.40/117.42 inference(scs_inference,[],[792,227,30,31,32,12,6,7,9,10,11])). % 117.40/117.42 cnf(1595,plain, % 117.40/117.42 (E(f3(a2,x15951),f3(f3(a2,x15952),x15951))), % 117.40/117.42 inference(scs_inference,[],[792,227,30,31,32,12,6,7,9,10,11,8])). % 117.40/117.42 cnf(1598,plain, % 117.40/117.42 (P2(f6(a8,a2),a8)), % 117.40/117.42 inference(scs_inference,[],[792,900,227,30,31,32,12,6,7,9,10,11,8,23,27])). % 117.40/117.42 cnf(1600,plain, % 117.40/117.42 (~E(f1(f3(a2,x16001),x16002),f3(a4,a8))), % 117.40/117.42 inference(scs_inference,[],[609,792,900,227,30,31,32,12,6,7,9,10,11,8,23,27,2])). % 117.40/117.42 cnf(1601,plain, % 117.40/117.42 (~P2(f6(f3(a4,a8),a2),a8)), % 117.40/117.42 inference(scs_inference,[],[609,792,768,900,227,30,31,32,12,6,7,9,10,11,8,23,27,2,15])). % 117.40/117.42 cnf(1602,plain, % 117.40/117.42 (P2(f6(a8,a2),f3(a8,f1(a2,x16021)))), % 117.40/117.42 inference(scs_inference,[],[609,792,768,900,227,243,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29])). % 117.40/117.42 cnf(1605,plain, % 117.40/117.42 (P2(f6(a8,a2),f1(a8,a8))), % 117.40/117.42 inference(scs_inference,[],[609,792,768,900,227,243,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35])). % 117.40/117.42 cnf(1607,plain, % 117.40/117.42 (~P1(a4,f3(a2,x16071))), % 117.40/117.42 inference(scs_inference,[],[609,792,768,900,1117,227,235,243,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35,14])). % 117.40/117.42 cnf(1608,plain, % 117.40/117.42 (P2(f7(a8,a2),a8)), % 117.40/117.42 inference(scs_inference,[],[284,609,792,768,900,1117,227,235,243,20,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35,14,34])). % 117.40/117.42 cnf(1611,plain, % 117.40/117.42 (~E(f3(a2,x16111),a4)), % 117.40/117.42 inference(scs_inference,[],[18,284,609,792,768,900,1117,227,235,243,20,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35,14,34,13])). % 117.40/117.42 cnf(1618,plain, % 117.40/117.42 (~P2(f6(a8,a2),f3(x16181,a8))), % 117.40/117.42 inference(scs_inference,[],[18,284,609,954,792,768,900,1117,262,227,578,235,672,243,20,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35,14,34,13,26,3,36])). % 117.40/117.42 cnf(1620,plain, % 117.40/117.42 (~P3(a8)), % 117.40/117.42 inference(scs_inference,[],[18,284,609,954,792,768,900,1117,262,227,578,235,672,243,20,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35,14,34,13,26,3,36,25])). % 117.40/117.42 cnf(1622,plain, % 117.40/117.42 (P2(f5(a8),a8)), % 117.40/117.42 inference(scs_inference,[],[18,284,609,954,792,768,900,1117,262,227,578,235,672,243,20,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35,14,34,13,26,3,36,25,24])). % 117.40/117.42 cnf(1624,plain, % 117.40/117.42 (~P3(f1(a8,a8))), % 117.40/117.42 inference(scs_inference,[],[18,284,609,954,792,768,900,1117,262,227,578,235,672,243,20,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35,14,34,13,26,3,36,25,24,65])). % 117.40/117.42 cnf(1628,plain, % 117.40/117.42 (~E(f3(a2,x16281),f1(a8,a8))), % 117.40/117.42 inference(scs_inference,[],[18,284,609,954,792,768,900,1117,221,262,227,578,235,672,243,20,30,31,32,12,6,7,9,10,11,8,23,27,2,15,29,35,14,34,13,26,3,36,25,24,65,28,17])). % 117.40/117.42 cnf(1635,plain, % 117.40/117.42 (E(f7(x16351,f1(x16352,a2)),f7(x16351,a2))), % 117.40/117.42 inference(scs_inference,[],[1618,1605,277,32,36,7])). % 117.40/117.42 cnf(1640,plain, % 117.40/117.42 (E(f3(x16401,f1(x16402,a2)),f3(x16401,a2))), % 117.40/117.42 inference(scs_inference,[],[1618,1605,277,32,36,7,31,30,9])). % 117.40/117.42 cnf(1641,plain, % 117.40/117.42 (E(f7(f1(x16411,a2),x16412),f7(a2,x16412))), % 117.40/117.42 inference(scs_inference,[],[1618,1605,277,32,36,7,31,30,9,6])). % 117.40/117.42 cnf(1642,plain, % 117.40/117.42 (E(f6(f1(x16421,a2),x16422),f6(a2,x16422))), % 117.40/117.42 inference(scs_inference,[],[1618,1605,277,32,36,7,31,30,9,6,10])). % 117.40/117.42 cnf(1643,plain, % 117.40/117.42 (E(f6(x16431,f1(x16432,a2)),f6(x16431,a2))), % 117.40/117.42 inference(scs_inference,[],[1618,1605,277,32,36,7,31,30,9,6,10,11])). % 117.40/117.42 cnf(1644,plain, % 117.40/117.42 (E(f5(f1(x16441,a2)),f5(a2))), % 117.40/117.42 inference(scs_inference,[],[1618,1605,277,32,36,7,31,30,9,6,10,11,12])). % 117.40/117.42 cnf(1645,plain, % 117.40/117.42 (~P3(f3(a8,f1(a2,x16451)))), % 117.40/117.42 inference(scs_inference,[],[1618,1605,1602,277,32,36,7,31,30,9,6,10,11,12,25])). % 117.40/117.42 cnf(1649,plain, % 117.40/117.42 (P1(f7(a2,x16491),f7(f3(a2,x16492),x16491))), % 117.40/117.42 inference(scs_inference,[],[1618,1624,1605,1590,1602,277,32,36,7,31,30,9,6,10,11,12,25,24,23])). % 117.40/117.42 cnf(1651,plain, % 117.40/117.42 (E(f3(f3(a2,x16511),x16512),f3(a2,x16512))), % 117.40/117.42 inference(scs_inference,[],[1618,1624,1605,1590,1602,277,235,32,36,7,31,30,9,6,10,11,12,25,24,23,8])). % 117.40/117.42 cnf(1652,plain, % 117.40/117.42 (P2(f6(a4,f3(a2,x16521)),a4)), % 117.40/117.42 inference(scs_inference,[],[1618,1624,1605,1607,1590,1602,277,235,32,36,7,31,30,9,6,10,11,12,25,24,23,8,27])). % 117.40/117.42 cnf(1654,plain, % 117.40/117.42 (~E(f1(a8,a8),f3(a2,x16541))), % 117.40/117.42 inference(scs_inference,[],[1618,1628,1624,1605,1607,1590,1602,277,235,32,36,7,31,30,9,6,10,11,12,25,24,23,8,27,2])). % 117.40/117.42 cnf(1655,plain, % 117.40/117.42 (P2(f6(a8,a2),f3(f1(a8,a8),f3(x16551,a8)))), % 117.40/117.42 inference(scs_inference,[],[1618,1628,1624,1605,1607,1590,1602,277,235,32,36,7,31,30,9,6,10,11,12,25,24,23,8,27,2,29])). % 117.40/117.42 cnf(1662,plain, % 117.40/117.42 (P1(x16621,x16621)), % 117.40/117.42 inference(rename_variables,[],[18])). % 117.40/117.42 cnf(1663,plain, % 117.40/117.42 (P2(f7(f1(a2,a8),f3(a4,a8)),f3(a4,a8))), % 117.40/117.42 inference(scs_inference,[],[18,1620,1618,1628,1624,1605,1607,1583,1590,1591,1602,669,277,235,146,32,36,7,31,30,9,6,10,11,12,25,24,23,8,27,2,29,15,35,17,14,34])). % 117.40/117.42 cnf(1667,plain, % 117.40/117.42 (P1(f7(f3(a2,x16671),x16672),f7(a2,x16672))), % 117.40/117.42 inference(scs_inference,[],[18,1662,1620,1618,1628,1624,1605,1607,1583,1590,1591,1602,669,277,235,146,32,36,7,31,30,9,6,10,11,12,25,24,23,8,27,2,29,15,35,17,14,34,13])). % 117.40/117.42 cnf(1669,plain, % 117.40/117.42 (~P1(f1(a8,a8),f3(a2,x16691))), % 117.40/117.42 inference(scs_inference,[],[18,1662,1620,1618,1628,1624,1605,1607,1583,1590,1591,1602,669,277,235,146,224,32,36,7,31,30,9,6,10,11,12,25,24,23,8,27,2,29,15,35,17,14,34,13,26])). % 117.40/117.42 cnf(1676,plain, % 117.40/117.42 (~E(a2,f1(a8,a8))), % 117.40/117.42 inference(scs_inference,[],[18,1662,1620,1618,1628,1624,1605,1607,1600,1583,1590,1591,1602,669,742,277,235,146,224,32,36,7,31,30,9,6,10,11,12,25,24,23,8,27,2,29,15,35,17,14,34,13,26,3,48])). % 117.40/117.42 cnf(1677,plain, % 117.40/117.42 (~P3(f1(f1(a8,a8),f1(a8,a8)))), % 117.40/117.42 inference(scs_inference,[],[18,1662,1620,1618,1628,1624,1605,1607,1600,1583,1590,1591,1602,669,742,277,235,146,224,32,36,7,31,30,9,6,10,11,12,25,24,23,8,27,2,29,15,35,17,14,34,13,26,3,48,65])). % 117.40/117.42 cnf(1686,plain, % 117.40/117.42 (~P2(f5(a8),f3(x16861,a8))), % 117.40/117.42 inference(scs_inference,[],[1622,780,32,36])). % 117.40/117.42 cnf(1688,plain, % 117.40/117.42 (E(f7(x16881,a2),f7(x16881,f1(x16882,a2)))), % 117.40/117.42 inference(scs_inference,[],[1622,780,246,32,36,7])). % 117.40/117.42 cnf(1691,plain, % 117.40/117.42 (E(f3(x16911,a2),f3(x16911,f1(x16912,a2)))), % 117.40/117.42 inference(scs_inference,[],[1622,780,246,32,36,7,30,9])). % 117.40/117.42 cnf(1694,plain, % 117.40/117.42 (E(f7(a2,x16941),f7(f1(x16942,a2),x16941))), % 117.40/117.42 inference(scs_inference,[],[1622,780,246,32,36,7,30,9,31,6])). % 117.40/117.42 cnf(1695,plain, % 117.40/117.42 (E(f6(a2,x16951),f6(f1(x16952,a2),x16951))), % 117.40/117.42 inference(scs_inference,[],[1622,780,246,32,36,7,30,9,31,6,10])). % 117.40/117.42 cnf(1696,plain, % 117.40/117.42 (E(f6(x16961,a2),f6(x16961,f1(x16962,a2)))), % 117.40/117.42 inference(scs_inference,[],[1622,780,246,32,36,7,30,9,31,6,10,11])). % 117.40/117.42 cnf(1697,plain, % 117.40/117.42 (E(f5(a2),f5(f1(x16971,a2)))), % 117.40/117.42 inference(scs_inference,[],[1622,780,246,32,36,7,30,9,31,6,10,11,12])). % 117.40/117.42 cnf(1698,plain, % 117.40/117.42 (~P3(f3(a4,a8))), % 117.40/117.42 inference(scs_inference,[],[1622,1663,780,246,32,36,7,30,9,31,6,10,11,12,25])). % 117.40/117.42 cnf(1700,plain, % 117.40/117.42 (P2(f5(f3(a4,a8)),f3(a4,a8))), % 117.40/117.42 inference(scs_inference,[],[1622,1663,780,246,32,36,7,30,9,31,6,10,11,12,25,24])). % 117.40/117.42 cnf(1706,plain, % 117.40/117.42 (~E(f1(a8,a8),a2)), % 117.40/117.42 inference(scs_inference,[],[1669,1622,1676,1663,1635,780,246,32,36,7,30,9,31,6,10,11,12,25,24,23,27,2])). % 117.40/117.42 cnf(1707,plain, % 117.40/117.42 (P2(f6(a8,a2),f3(a8,f3(x17071,a8)))), % 117.40/117.42 inference(scs_inference,[],[1669,1622,1676,1598,1663,1635,780,246,1618,32,36,7,30,9,31,6,10,11,12,25,24,23,27,2,29])). % 117.40/117.42 cnf(1709,plain, % 117.40/117.42 (~P2(f7(a2,f3(a4,a8)),f1(a8,x17091))), % 117.40/117.42 inference(scs_inference,[],[1669,1622,1676,1598,1663,1635,1585,780,246,1618,32,36,7,30,9,31,6,10,11,12,25,24,23,27,2,29,15])). % 117.40/117.42 cnf(1711,plain, % 117.40/117.42 (~E(f3(a4,a8),a8)), % 117.40/117.42 inference(scs_inference,[],[1669,1622,1676,1598,1663,1635,1585,780,246,792,1618,32,36,7,30,9,31,6,10,11,12,25,24,23,27,2,29,15,16])). % 117.40/117.42 cnf(1713,plain, % 117.40/117.42 (P2(f5(a8),f1(a8,a8))), % 117.40/117.42 inference(scs_inference,[],[1669,1622,1676,1598,1663,1635,1585,780,246,792,1618,32,36,7,30,9,31,6,10,11,12,25,24,23,27,2,29,15,16,35])). % 117.40/117.42 cnf(1722,plain, % 117.40/117.42 (E(f7(f3(a2,x17221),x17222),f7(a2,x17222))), % 117.40/117.42 inference(scs_inference,[],[18,291,1669,1622,1676,1598,1663,1635,1667,1585,1677,1649,780,42,833,211,246,792,1618,20,32,36,7,30,9,31,6,10,11,12,25,24,23,27,2,29,15,16,35,17,14,34,13,26])). % 117.40/117.42 cnf(1725,plain, % 117.40/117.42 (E(f7(f1(x17251,a2),f1(x17252,a2)),f7(a2,a2))), % 117.40/117.42 inference(scs_inference,[],[18,291,1669,1622,1676,1598,1663,1635,1641,1667,1585,1677,1649,780,42,833,211,246,792,1618,20,32,36,7,30,9,31,6,10,11,12,25,24,23,27,2,29,15,16,35,17,14,34,13,26,3])). % 117.40/117.42 cnf(1733,plain, % 117.40/117.42 (E(f7(x17331,a2),f7(x17331,f1(a2,x17332)))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,266,32,36,7])). % 117.40/117.42 cnf(1738,plain, % 117.40/117.42 (E(f3(x17381,a2),f3(x17381,f1(a2,x17382)))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,266,32,36,7,31,30,9])). % 117.40/117.42 cnf(1739,plain, % 117.40/117.42 (E(f7(a2,x17391),f7(f1(a2,x17392),x17391))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,266,32,36,7,31,30,9,6])). % 117.40/117.42 cnf(1740,plain, % 117.40/117.42 (E(f6(a2,x17401),f6(f1(a2,x17402),x17401))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,266,32,36,7,31,30,9,6,10])). % 117.40/117.42 cnf(1741,plain, % 117.40/117.42 (E(f6(x17411,a2),f6(x17411,f1(a2,x17412)))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,266,32,36,7,31,30,9,6,10,11])). % 117.40/117.42 cnf(1742,plain, % 117.40/117.42 (E(f5(a2),f5(f1(a2,x17421)))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,266,32,36,7,31,30,9,6,10,11,12])). % 117.40/117.42 cnf(1743,plain, % 117.40/117.42 (~P3(f3(f1(a8,a8),f3(x17431,a8)))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,1655,266,32,36,7,31,30,9,6,10,11,12,25])). % 117.40/117.42 cnf(1745,plain, % 117.40/117.42 (P1(f7(f1(x17451,a2),f1(x17452,a2)),f7(a2,a2))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,1725,1655,266,32,36,7,31,30,9,6,10,11,12,25,23])). % 117.40/117.42 cnf(1747,plain, % 117.40/117.42 (P2(f6(a8,f1(a2,x17471)),a8)), % 117.40/117.42 inference(scs_inference,[],[1713,1686,1725,1655,459,266,32,36,7,31,30,9,6,10,11,12,25,23,27])). % 117.40/117.42 cnf(1752,plain, % 117.40/117.42 (~E(f5(f3(a4,a8)),f5(a8))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,1711,1700,1725,1655,459,266,32,36,7,31,30,9,6,10,11,12,25,23,27,2,29,15])). % 117.40/117.42 cnf(1756,plain, % 117.40/117.42 (~E(f3(a2,x17561),f3(a8,f1(a2,x17562)))), % 117.40/117.42 inference(scs_inference,[],[1713,1686,1711,1700,1725,1655,1645,459,221,266,32,36,7,31,30,9,6,10,11,12,25,23,27,2,29,15,35,17])). % 117.40/117.42 cnf(1757,plain, % 117.40/117.42 (P1(f6(f1(x17571,a2),x17572),f6(a2,x17572))), % 117.40/117.42 inference(scs_inference,[],[18,1713,1686,1711,1700,1725,1642,1655,1645,459,221,266,32,36,7,31,30,9,6,10,11,12,25,23,27,2,29,15,35,17,14])). % 117.40/117.42 cnf(1758,plain, % 117.40/117.42 (P1(x17581,x17581)), % 117.40/117.42 inference(rename_variables,[],[18])). % 117.40/117.42 cnf(1759,plain, % 117.40/117.42 (P2(f7(f3(a2,x17591),a4),a4)), % 117.40/117.42 inference(scs_inference,[],[18,1713,1686,1711,1700,1725,1642,1655,1645,1611,459,221,266,220,32,36,7,31,30,9,6,10,11,12,25,23,27,2,29,15,35,17,14,34])). % 117.40/117.42 cnf(1762,plain, % 117.40/117.42 (P1(f7(a2,a2),f7(f1(x17621,a2),f1(x17622,a2)))), % 117.40/117.42 inference(scs_inference,[],[18,1758,1713,1686,1711,1700,1725,1642,1655,1645,1611,459,221,266,220,32,36,7,31,30,9,6,10,11,12,25,23,27,2,29,15,35,17,14,34,13])). % 117.40/117.42 cnf(1764,plain, % 117.40/117.42 (~P1(f1(a8,a8),a2)), % 117.40/117.42 inference(scs_inference,[],[18,1758,1713,1686,1711,1706,1700,1725,1642,1655,1645,1611,459,221,266,39,220,32,36,7,31,30,9,6,10,11,12,25,23,27,2,29,15,35,17,14,34,13,26])). % 117.40/117.42 cnf(1769,plain, % 117.40/117.42 (E(f7(x17691,f1(a2,x17692)),f7(x17691,a2))), % 117.40/117.42 inference(scs_inference,[],[287,7])). % 117.40/117.42 cnf(1772,plain, % 117.40/117.42 (~P2(f6(a4,f3(a2,x17721)),f3(x17722,a4))), % 117.40/117.42 inference(scs_inference,[],[1601,1652,287,7,32,36])). % 117.40/117.42 cnf(1778,plain, % 117.40/117.42 (E(f3(x17781,f1(a2,x17782)),f3(x17781,a2))), % 117.40/117.42 inference(scs_inference,[],[1601,1652,287,7,32,36,31,30,9])). % 117.40/117.42 cnf(1779,plain, % 117.40/117.42 (E(f7(f1(a2,x17791),x17792),f7(a2,x17792))), % 117.40/117.42 inference(scs_inference,[],[1601,1652,287,7,32,36,31,30,9,6])). % 117.40/117.42 cnf(1780,plain, % 117.40/117.42 (E(f6(f1(a2,x17801),x17802),f6(a2,x17802))), % 117.40/117.42 inference(scs_inference,[],[1601,1652,287,7,32,36,31,30,9,6,10])). % 117.40/117.42 cnf(1781,plain, % 117.40/117.42 (E(f6(x17811,f1(a2,x17812)),f6(x17811,a2))), % 117.40/117.42 inference(scs_inference,[],[1601,1652,287,7,32,36,31,30,9,6,10,11])). % 117.40/117.42 cnf(1782,plain, % 117.40/117.42 (E(f5(f1(a2,x17821)),f5(a2))), % 117.40/117.42 inference(scs_inference,[],[1601,1652,287,7,32,36,31,30,9,6,10,11,12])). % 117.40/117.42 cnf(1783,plain, % 117.40/117.42 (~P3(f3(a8,f3(x17831,a8)))), % 117.40/117.42 inference(scs_inference,[],[1707,1601,1652,287,7,32,36,31,30,9,6,10,11,12,25])). % 117.40/117.42 cnf(1785,plain, % 117.40/117.42 (P1(f3(x17851,f1(x17852,a2)),f3(x17851,a2))), % 117.40/117.42 inference(scs_inference,[],[1640,1707,1601,1652,287,7,32,36,31,30,9,6,10,11,12,25,23])). % 117.40/117.42 cnf(1803,plain, % 117.40/117.42 (E(f3(f3(a2,x18031),f1(x18032,a2)),f3(a2,a2))), % 117.40/117.42 inference(scs_inference,[],[1764,1745,1640,1651,1722,1709,1752,1762,1743,1707,1601,1652,1654,42,219,287,220,7,32,36,31,30,9,6,10,11,12,25,23,27,2,15,35,17,14,34,26,3])). % 117.40/117.42 cnf(1806,plain, % 117.40/117.42 (~P3(f1(a4,a4))), % 117.40/117.42 inference(scs_inference,[],[1764,1745,1640,1651,1722,1709,1752,1762,1743,1707,1601,1652,1654,42,219,287,220,7,32,36,31,30,9,6,10,11,12,25,23,27,2,15,35,17,14,34,26,3,65])). % 117.40/117.42 cnf(1819,plain, % 117.40/117.42 (E(f7(x18191,f3(a2,x18192)),f7(x18191,a2))), % 117.40/117.42 inference(scs_inference,[],[766,1747,235,36,32,7])). % 117.40/117.42 cnf(1822,plain, % 117.40/117.42 (E(f3(x18221,f3(a2,x18222)),f3(x18221,a2))), % 117.40/117.42 inference(scs_inference,[],[766,1747,235,36,32,7,30,9])). % 117.40/117.42 cnf(1825,plain, % 117.40/117.42 (E(f6(f3(a2,x18251),x18252),f6(a2,x18252))), % 117.40/117.42 inference(scs_inference,[],[766,1747,235,36,32,7,30,9,31,10])). % 117.40/117.42 cnf(1826,plain, % 117.40/117.42 (E(f6(x18261,f3(a2,x18262)),f6(x18261,a2))), % 117.40/117.42 inference(scs_inference,[],[766,1747,235,36,32,7,30,9,31,10,11])). % 117.40/117.42 cnf(1827,plain, % 117.40/117.42 (E(f5(f3(a2,x18271)),f5(a2))), % 117.40/117.42 inference(scs_inference,[],[766,1747,235,36,32,7,30,9,31,10,11,12])). % 117.40/117.42 cnf(1828,plain, % 117.40/117.42 (~P3(a4)), % 117.40/117.42 inference(scs_inference,[],[766,1747,1759,235,36,32,7,30,9,31,10,11,12,25])). % 117.40/117.42 cnf(1832,plain, % 117.40/117.42 (P1(f3(f3(a2,x18321),f1(x18322,a2)),f3(a2,a2))), % 117.40/117.42 inference(scs_inference,[],[1806,1803,766,1747,1759,235,36,32,7,30,9,31,10,11,12,25,24,23])). % 117.40/117.42 cnf(1834,plain, % 117.40/117.42 (P2(f6(a8,f3(a2,x18341)),a8)), % 117.40/117.42 inference(scs_inference,[],[1806,1803,766,1747,1759,585,235,36,32,7,30,9,31,10,11,12,25,24,23,27])). % 117.40/117.42 cnf(1836,plain, % 117.40/117.42 (~E(f3(a8,f1(a2,x18361)),f3(a2,x18362))), % 117.40/117.42 inference(scs_inference,[],[1806,1803,1756,766,1747,1759,585,235,36,32,7,30,9,31,10,11,12,25,24,23,27,2])). % 117.40/117.42 cnf(1839,plain, % 117.40/117.42 (~P2(f7(a2,f3(a4,a8)),f3(a8,x18391))), % 117.40/117.42 inference(scs_inference,[],[1806,1803,1587,1694,1756,766,1747,1759,585,235,220,36,32,7,30,9,31,10,11,12,25,24,23,27,2,16,15])). % 117.40/117.42 cnf(1844,plain, % 117.40/117.42 (~E(f3(f1(a2,x18441),x18442),f1(a4,a4))), % 117.40/117.42 inference(scs_inference,[],[1806,1803,1587,1694,1756,766,1747,1759,585,669,235,220,36,32,7,30,9,31,10,11,12,25,24,23,27,2,16,15,35,17])). % 117.40/117.42 cnf(1845,plain, % 117.40/117.42 (P1(f6(x18451,f1(x18452,a2)),f6(x18451,a2))), % 117.40/117.42 inference(scs_inference,[],[18,1806,1803,1643,1587,1694,1756,766,1747,1759,585,669,235,220,36,32,7,30,9,31,10,11,12,25,24,23,27,2,16,15,35,17,14])). % 117.40/117.42 cnf(1847,plain, % 117.40/117.42 (~P1(f3(a8,f1(a2,x18471)),f3(a2,x18472))), % 117.40/117.42 inference(scs_inference,[],[18,1806,1803,1643,1587,1694,1756,766,1747,1759,585,669,235,224,220,36,32,7,30,9,31,10,11,12,25,24,23,27,2,16,15,35,17,14,26])). % 117.40/117.42 cnf(1863,plain, % 117.40/117.42 (P2(f5(a4),a4)), % 117.40/117.42 inference(scs_inference,[],[1828,1834,768,36,32,31,30,24])). % 117.40/117.42 cnf(1867,plain, % 117.40/117.42 (P2(f6(a8,f1(x18671,a2)),a8)), % 117.40/117.42 inference(scs_inference,[],[1828,1769,1834,881,768,36,32,31,30,24,23,27])). % 117.40/117.42 cnf(1869,plain, % 117.40/117.42 (~E(f1(a4,a4),f3(f1(a2,x18691),x18692))), % 117.40/117.42 inference(scs_inference,[],[1828,1844,1769,1834,881,768,36,32,31,30,24,23,27,2])). % 117.40/117.42 cnf(1870,plain, % 117.40/117.42 (~P2(f6(a4,a2),f3(x18701,a4))), % 117.40/117.42 inference(scs_inference,[],[1828,1844,1769,1772,1594,1834,881,768,36,32,31,30,24,23,27,2,15])). % 117.40/117.42 cnf(1879,plain, % 117.40/117.42 (~P1(f3(a8,a2),f3(a2,x18791))), % 117.40/117.42 inference(scs_inference,[],[1828,1844,1769,1772,1847,1594,1691,1834,881,768,1706,698,900,211,20,36,32,31,30,24,23,27,2,15,35,17,14,34,13])). % 117.40/117.42 cnf(1882,plain, % 117.40/117.42 (E(f3(a2,a2),f3(f3(a2,x18821),f1(x18822,a2)))), % 117.40/117.42 inference(scs_inference,[],[1828,1844,1832,1769,1772,1847,1594,1691,1834,881,768,1706,698,900,211,224,20,36,32,31,30,24,23,27,2,15,35,17,14,34,13,26])). % 117.40/117.42 cnf(1885,plain, % 117.40/117.42 (E(f7(f1(a2,x18851),f1(a2,x18852)),f7(a2,a2))), % 117.40/117.42 inference(scs_inference,[],[1828,1844,1832,1769,1779,1772,1847,1594,1691,1834,881,768,1706,698,900,211,224,20,36,32,31,30,24,23,27,2,15,35,17,14,34,13,26,3])). % 117.40/117.42 cnf(1888,plain, % 117.40/117.42 (~E(a2,f3(a8,a2))), % 117.40/117.42 inference(scs_inference,[],[1828,1844,1832,1769,1779,1772,1847,1594,1691,1834,881,768,1706,698,900,211,224,20,36,32,31,30,24,23,27,2,15,35,17,14,34,13,26,3,48])). % 117.40/117.42 cnf(1889,plain, % 117.40/117.42 (~P2(f7(a2,f3(a4,a8)),a8)), % 117.40/117.42 inference(scs_inference,[],[1828,1844,1832,1839,1769,1779,1772,1847,1594,1691,1834,881,768,1709,1706,698,900,211,224,20,36,32,31,30,24,23,27,2,15,35,17,14,34,13,26,3,48,29])). % 117.40/117.42 cnf(1897,plain, % 117.40/117.42 (~P2(f5(a4),f3(x18971,a4))), % 117.40/117.42 inference(scs_inference,[],[1863,36])). % 117.40/117.42 cnf(1905,plain, % 117.40/117.42 (P1(f7(f1(a2,x19051),f1(a2,x19052)),f7(a2,a2))), % 117.40/117.42 inference(scs_inference,[],[1870,1863,1885,36,31,32,30,23])). % 117.40/117.42 cnf(1909,plain, % 117.40/117.42 (~E(f3(a8,a2),a2)), % 117.40/117.42 inference(scs_inference,[],[1870,1879,1888,1863,1885,36,31,32,30,23,27,2])). % 117.40/117.42 cnf(1912,plain, % 117.40/117.42 (P2(f5(a4),f1(a4,a4))), % 117.40/117.42 inference(scs_inference,[],[1870,1879,1888,1863,1885,1781,36,31,32,30,23,27,2,15,35])). % 117.40/117.42 cnf(1915,plain, % 117.40/117.42 (P1(f6(f1(a2,x19151),x19152),f6(a2,x19152))), % 117.40/117.42 inference(scs_inference,[],[18,1870,1879,1888,1863,1885,1780,1781,1783,237,36,31,32,30,23,27,2,15,35,17,14])). % 117.40/117.42 cnf(1916,plain, % 117.40/117.42 (P1(x19161,x19161)), % 117.40/117.42 inference(rename_variables,[],[18])). % 117.40/117.42 cnf(1920,plain, % 117.40/117.42 (P1(f7(a2,a2),f7(f1(a2,x19201),f1(a2,x19202)))), % 117.40/117.42 inference(scs_inference,[],[18,1916,1870,1879,1888,1863,1885,1780,1781,1783,237,20,36,31,32,30,23,27,2,15,35,17,14,34,13])). % 117.40/117.42 cnf(1922,plain, % 117.40/117.42 (~P1(f3(a8,a2),a2)), % 117.40/117.42 inference(scs_inference,[],[18,1916,1870,1879,1888,1863,1885,1780,1781,1783,237,39,20,36,31,32,30,23,27,2,15,35,17,14,34,13,26])). % 117.40/117.42 cnf(1925,plain, % 117.40/117.42 (~E(f1(x19251,f1(x19252,a2)),f3(a8,a2))), % 117.40/117.42 inference(scs_inference,[],[18,1916,1870,1879,1888,1863,1885,1780,1781,1783,213,237,39,20,36,31,32,30,23,27,2,15,35,17,14,34,13,26,3])). % 117.40/117.42 cnf(1926,plain, % 117.40/117.42 (~P3(f3(a8,a2))), % 117.40/117.42 inference(scs_inference,[],[18,1916,1870,1879,1888,1863,1885,1780,1781,1783,213,237,39,20,36,31,32,30,23,27,2,15,35,17,14,34,13,26,3,25])). % 117.40/117.42 cnf(1940,plain, % 117.40/117.42 (P1(f3(x19401,f1(a2,x19402)),f3(x19401,a2))), % 117.40/117.42 inference(scs_inference,[],[1912,1897,1778,32,36,31,30,23])). % 117.40/117.42 cnf(1949,plain, % 117.40/117.42 (~E(f1(a2,x19491),f3(a8,a2))), % 117.40/117.42 inference(scs_inference,[],[1926,1912,1897,1922,1925,1778,256,32,36,31,30,23,27,2,29,35,17])). % 117.40/117.42 cnf(1955,plain, % 117.40/117.42 (E(f3(x19551,f1(a2,x19552)),f3(x19551,a2))), % 117.40/117.42 inference(rename_variables,[],[1778])). % 117.40/117.42 cnf(1959,plain, % 117.40/117.42 (~E(f3(a8,a2),f3(a2,x19591))), % 117.40/117.42 inference(scs_inference,[],[1926,1912,1897,1909,1922,1925,1905,1778,1955,1836,1920,256,219,20,32,36,31,30,23,27,2,29,35,17,14,34,13,26,3])). % 117.40/117.42 cnf(1961,plain, % 117.40/117.42 (~P3(f3(f1(a4,a4),f3(x19611,a4)))), % 117.40/117.42 inference(scs_inference,[],[1926,1912,1897,1909,1922,1925,1905,1778,1955,1836,1920,256,219,20,32,36,31,30,23,27,2,29,35,17,14,34,13,26,3,25])). % 117.40/117.42 cnf(1963,plain, % 117.40/117.42 (~P3(f1(f1(a4,a4),f1(a4,a4)))), % 117.40/117.42 inference(scs_inference,[],[1926,1912,1897,1909,1922,1925,1905,1778,1955,1836,1920,256,219,20,32,36,31,30,23,27,2,29,35,17,14,34,13,26,3,25,65])). % 117.40/117.42 cnf(1970,plain, % 117.40/117.42 (~P2(f7(f3(a2,x19701),a4),f3(x19702,a4))), % 117.40/117.42 inference(scs_inference,[],[1759,220,32,36])). % 117.40/117.42 cnf(1972,plain, % 117.40/117.42 (~P2(f7(a2,f3(a4,a8)),f1(x19721,a8))), % 117.40/117.42 inference(scs_inference,[],[1889,1759,220,32,36,30])). % 117.40/117.42 cnf(1976,plain, % 117.40/117.42 (P2(f6(a4,f1(a2,x19761)),a4)), % 117.40/117.42 inference(scs_inference,[],[1822,1081,1889,1759,220,32,36,30,23,27])). % 117.40/117.42 cnf(1978,plain, % 117.40/117.42 (~E(f3(a2,x19781),f3(a8,a2))), % 117.40/117.42 inference(scs_inference,[],[1959,1822,1081,1889,1759,220,32,36,30,23,27,2])). % 117.40/117.42 cnf(1983,plain, % 117.40/117.42 (~E(f1(f3(a2,x19831),x19832),f3(a8,a2))), % 117.40/117.42 inference(scs_inference,[],[1959,1822,1867,1081,1839,1641,1889,1926,1759,550,220,32,36,30,23,27,2,15,35,17])). % 117.40/117.42 cnf(1985,plain, % 117.40/117.42 (P1(x19851,x19851)), % 117.40/117.42 inference(rename_variables,[],[18])). % 117.40/117.42 cnf(1991,plain, % 117.40/117.42 (~P1(f3(a8,a2),f1(a2,f1(a2,x19911)))), % 117.40/117.42 inference(scs_inference,[],[18,1985,1959,1949,1822,1825,1867,1081,1839,1641,1889,1926,1759,550,71,243,220,32,36,30,23,27,2,15,35,17,14,34,13,26])). % 117.40/117.42 cnf(1995,plain, % 117.40/117.42 (~E(f3(a8,f3(a2,x19951)),f3(a2,x19952))), % 117.40/117.42 inference(scs_inference,[],[18,1985,1959,1949,1822,1825,1867,1592,1081,1839,1641,1889,1926,1759,550,71,243,220,32,36,30,23,27,2,15,35,17,14,34,13,26,3])). % 117.40/117.42 cnf(1999,plain, % 117.40/117.42 (~P2(f7(a8,a2),f3(x19991,a8))), % 117.40/117.42 inference(scs_inference,[],[1608,36])). % 117.40/117.42 cnf(2005,plain, % 117.40/117.42 (P2(f6(a4,f1(x20051,a2)),a4)), % 117.40/117.42 inference(scs_inference,[],[1103,1608,36,32,30,27])). % 117.40/117.42 cnf(2007,plain, % 117.40/117.42 (~E(f3(a8,a2),f1(f3(a2,x20071),x20072))), % 117.40/117.42 inference(scs_inference,[],[1983,1103,1608,36,32,30,27,2])). % 117.40/117.42 cnf(2018,plain, % 117.40/117.42 (~E(f3(a2,x20181),f1(f1(a4,a4),f1(a4,a4)))), % 117.40/117.42 inference(scs_inference,[],[1983,1972,1644,1963,1869,1103,1722,1608,221,701,36,32,30,27,2,23,29,15,26,17])). % 117.40/117.42 cnf(2021,plain, % 117.40/117.42 (~P1(a4,f1(x20211,f3(a2,x20212)))), % 117.40/117.42 inference(scs_inference,[],[1983,1972,1644,1963,1869,1976,1103,1722,1608,1117,221,1023,701,36,32,30,27,2,23,29,15,26,17,35,14])). % 117.40/117.42 cnf(2023,plain, % 117.40/117.42 (~E(f3(a2,x20231),f3(a8,a2))), % 117.40/117.42 inference(rename_variables,[],[1978])). % 117.40/117.42 cnf(2026,plain, % 117.40/117.42 (~E(f3(f3(a2,x20261),f1(x20262,a2)),f3(a8,a2))), % 117.40/117.42 inference(scs_inference,[],[1978,2023,1983,1972,1644,1963,1869,1976,1882,1103,1722,1608,1117,221,1023,701,220,36,32,30,27,2,23,29,15,26,17,35,14,34,3])). % 117.40/117.42 cnf(2028,plain, % 117.40/117.42 (~P1(f3(a8,f3(a2,x20281)),f3(a2,x20282))), % 117.40/117.42 inference(scs_inference,[],[1978,2023,1983,1972,1644,1963,1869,1976,1882,1103,1722,1822,1879,1608,1117,221,1023,701,220,36,32,30,27,2,23,29,15,26,17,35,14,34,3,13])). % 117.40/117.42 cnf(2032,plain, % 117.40/117.42 (~E(a2,f1(a4,a4))), % 117.40/117.42 inference(scs_inference,[],[1978,2023,1983,1972,1644,1963,1869,1976,1882,1103,1722,1822,1879,1608,1117,221,1023,701,220,36,32,30,27,2,23,29,15,26,17,35,14,34,3,13,31,48])). % 117.40/117.42 cnf(2044,plain, % 117.40/117.42 (~E(f1(a4,a4),a2)), % 117.40/117.42 inference(scs_inference,[],[2032,2028,2005,833,36,27,48,2])). % 117.40/117.42 cnf(2047,plain, % 117.40/117.42 (~P1(f1(a4,a4),a2)), % 117.40/117.42 inference(scs_inference,[],[2032,2028,1782,2005,833,39,36,27,48,2,23,26])). % 117.40/117.42 cnf(2052,plain, % 117.40/117.42 (~E(f1(x20521,f1(a2,x20522)),f3(a4,a8))), % 117.40/117.42 inference(scs_inference,[],[1999,2032,2028,1782,2005,1698,1819,833,74,39,36,27,48,2,23,26,15,17])). % 117.40/117.42 cnf(2055,plain, % 117.40/117.42 (~P1(f3(a8,a2),f1(f1(a2,x20551),a2))), % 117.40/117.42 inference(scs_inference,[],[19,1999,2032,2028,1782,1991,2005,1698,1819,833,74,39,36,27,48,2,23,26,15,17,35,14])). % 117.40/117.42 cnf(2060,plain, % 117.40/117.42 (P1(f6(f3(a2,x20601),f1(x20602,a2)),f6(a2,a2))), % 117.40/117.42 inference(scs_inference,[],[19,1999,2032,1845,2028,1782,1991,2005,1593,1698,1819,833,74,39,20,36,27,48,2,23,26,15,17,35,14,34,13])). % 117.40/117.42 cnf(2063,plain, % 117.40/117.42 (~E(f1(x20631,f3(a2,x20632)),f1(a4,a4))), % 117.40/117.42 inference(scs_inference,[],[19,1999,2032,1845,2028,1782,1991,2005,1593,1698,1819,1028,833,74,39,20,36,27,48,2,23,26,15,17,35,14,34,13,3])). % 117.40/117.42 cnf(2073,plain, % 117.40/117.42 (~P1(a8,f3(f1(x20731,a2),x20732))), % 117.40/117.42 inference(scs_inference,[],[2047,2063,1827,958,701,27,2,23,26])). % 117.40/117.42 cnf(2079,plain, % 117.40/117.42 (~P1(f1(a4,a4),f1(f3(a2,x20791),x20792))), % 117.40/117.42 inference(scs_inference,[],[2047,2063,1827,1961,958,1759,42,1057,701,27,2,23,26,17,35,14])). % 117.40/117.42 cnf(2085,plain, % 117.40/117.42 (E(f7(a2,a2),f7(f1(a2,x20851),f1(x20852,a2)))), % 117.40/117.42 inference(scs_inference,[],[2044,2047,2063,1827,1961,958,2021,1688,1739,1759,42,1057,672,701,20,27,2,23,26,17,35,14,34,13,3])). % 117.40/117.42 cnf(2101,plain, % 117.40/117.42 (~P1(f3(a4,a8),f1(x21011,f1(a2,x21012)))), % 117.40/117.42 inference(scs_inference,[],[2052,2026,2085,484,71,27,2,23,26])). % 117.40/117.42 cnf(2106,plain, % 117.40/117.42 (P2(f7(a8,a2),f1(a8,a8))), % 117.40/117.42 inference(scs_inference,[],[2052,2026,2085,1620,484,83,1608,71,27,2,23,26,17,35])). % 117.40/117.42 cnf(2108,plain, % 117.40/117.42 (~P1(f1(a4,a4),f1(x21081,f3(a2,x21082)))), % 117.40/117.42 inference(scs_inference,[],[19,2052,2026,2079,2085,1620,484,83,1608,71,27,2,23,26,17,35,14])). % 117.40/117.42 cnf(2110,plain, % 117.40/117.42 (P1(f6(f1(x21101,a2),f1(x21102,a2)),f6(a2,a2))), % 117.40/117.42 inference(scs_inference,[],[19,2052,2026,1757,2079,2085,1696,1620,484,83,1608,71,27,2,23,26,17,35,14,13])). % 117.40/117.42 cnf(2128,plain, % 117.40/117.42 (P1(f6(x21281,f3(a2,x21282)),f6(x21281,a2))), % 117.40/117.42 inference(scs_inference,[],[1995,1826,573,27,2,23])). % 117.40/117.42 cnf(2133,plain, % 117.40/117.42 (~E(f1(x21331,a2),f1(f1(a4,a4),f1(a4,a4)))), % 117.40/117.42 inference(scs_inference,[],[1995,1275,1826,1963,573,237,672,27,2,23,26,17])). % 117.40/117.42 cnf(2136,plain, % 117.40/117.42 (~P1(f3(a4,a8),f1(f1(a2,x21361),x21362))), % 117.40/117.42 inference(scs_inference,[],[19,2106,1995,2101,1275,1826,1963,573,237,672,27,2,23,26,17,35,14])). % 117.40/117.42 cnf(2137,plain, % 117.40/117.42 (~P1(f3(a4,a8),f1(x21371,f1(a2,x21372)))), % 117.40/117.42 inference(rename_variables,[],[2101])). % 117.40/117.42 cnf(2142,plain, % 117.40/117.42 (E(f6(a2,a2),f6(f1(x21421,a2),f1(a2,x21422)))), % 117.40/117.42 inference(scs_inference,[],[19,2106,1995,2101,2137,1275,1826,1695,1741,1963,573,237,45,672,27,2,23,26,17,35,14,13,3])). % 117.40/117.42 cnf(2147,plain, % 117.40/117.42 (~E(f1(f1(a4,a4),f1(a4,a4)),f1(x21471,a2))), % 117.40/117.42 inference(scs_inference,[],[2133,679,27,2])). % 117.40/117.42 cnf(2148,plain, % 117.40/117.42 (P1(f6(a2,a2),f6(f1(x21481,a2),f1(a2,x21482)))), % 117.40/117.42 inference(scs_inference,[],[2142,2133,679,27,2,23])). % 117.40/117.42 cnf(2150,plain, % 117.40/117.42 (~P1(f3(a8,a2),f1(f3(a2,x21501),f1(a2,x21502)))), % 117.40/117.42 inference(scs_inference,[],[2007,2142,2133,679,71,27,2,23,26])). % 117.40/117.42 cnf(2154,plain, % 117.40/117.42 (~E(f1(x21541,f1(x21542,a2)),f1(a8,a8))), % 117.40/117.42 inference(scs_inference,[],[2007,2142,2133,1624,679,192,71,27,2,23,26,17])). % 117.40/117.42 cnf(2157,plain, % 117.40/117.42 (P1(f6(x21571,f3(a2,x21572)),f6(x21571,a2))), % 117.40/117.42 inference(rename_variables,[],[2128])). % 117.40/117.42 cnf(2161,plain, % 117.40/117.42 (~E(f1(a2,x21611),f1(f1(a4,a4),f1(a4,a4)))), % 117.40/117.42 inference(scs_inference,[],[19,2128,2157,2007,2142,2133,1740,1642,1624,679,192,71,27,2,23,26,17,14,13,3])). % 117.40/117.42 cnf(2164,plain, % 117.40/117.42 (P2(f6(a4,a2),a4)), % 117.40/117.42 inference(scs_inference,[],[1117,27])). % 117.40/117.42 cnf(2171,plain, % 117.40/117.42 (~P2(f7(a2,a4),f3(x21711,a4))), % 117.40/117.42 inference(scs_inference,[],[2154,1970,1733,1590,1117,1870,27,2,23,29,15])). % 117.40/117.42 cnf(2178,plain, % 117.40/117.42 (~E(f1(a2,x21781),f1(f1(a8,a8),f1(a8,a8)))), % 117.40/117.42 inference(scs_inference,[],[2154,2110,2148,1970,1733,1677,1590,1117,256,1870,27,2,23,29,15,26,17])). % 117.40/117.43 cnf(2179,plain, % 117.40/117.43 (P2(f6(a4,a2),f1(a4,a4))), % 117.40/117.43 inference(scs_inference,[],[2154,2110,2148,1970,1733,1677,1590,1117,256,1870,27,2,23,29,15,26,17,35])). % 117.40/117.43 cnf(2183,plain, % 117.40/117.43 (~E(f3(f1(x21831,a2),x21832),f3(a4,a8))), % 117.40/117.43 inference(scs_inference,[],[19,2154,2110,2136,2150,2148,1970,1733,1677,1590,1117,256,1870,701,27,2,23,29,15,26,17,35,14,13])). % 117.40/117.43 cnf(2185,plain, % 117.40/117.43 (E(f6(f1(a2,x21851),f1(a2,x21852)),f6(a2,a2))), % 117.40/117.43 inference(scs_inference,[],[19,2154,2110,2136,2150,2148,1970,1733,1780,1677,1781,1590,1117,256,1870,701,27,2,23,29,15,26,17,35,14,13,3])). % 117.40/117.43 cnf(2196,plain, % 117.40/117.43 (~P3(f3(a4,f3(x21961,a4)))), % 117.40/117.43 inference(scs_inference,[],[19,2154,2110,2136,2150,2148,1970,1733,1780,1677,1781,1590,1117,256,1870,701,27,2,23,29,15,26,17,35,14,13,3,31,32,36,30,25])). % 117.40/117.43 cnf(2213,plain, % 117.40/117.43 (~E(f3(f1(a2,x22131),x22132),f3(a4,a8))), % 117.40/117.43 inference(scs_inference,[],[2171,2183,2185,2161,1779,1698,669,672,2,23,15,26,17])). % 117.40/117.43 cnf(2219,plain, % 117.40/117.43 (~P1(f3(a8,a2),f1(a2,x22191))), % 117.40/117.43 inference(scs_inference,[],[2179,2171,2183,2185,2161,2055,740,1779,285,1698,669,672,20,2,23,15,26,17,35,34,14])). % 117.40/117.43 cnf(2224,plain, % 117.40/117.43 (~E(f1(x22241,a2),f1(f1(a8,a8),f1(a8,a8)))), % 117.40/117.43 inference(scs_inference,[],[19,2179,2171,2183,2185,1915,2161,2178,2055,740,1779,285,1698,669,672,20,2,23,15,26,17,35,34,14,13,3])). % 117.40/117.43 cnf(2243,plain, % 117.40/117.43 (~P2(f7(f1(x22431,a2),f3(a4,a8)),f1(x22432,a8))), % 117.40/117.43 inference(scs_inference,[],[2164,2224,1279,1738,1972,1641,701,243,2,23,29,26,15])). % 117.40/117.43 cnf(2245,plain, % 117.40/117.43 (~E(f3(a2,x22451),f3(a4,f3(x22452,a4)))), % 117.40/117.43 inference(scs_inference,[],[2164,2224,2196,1279,1738,1972,1641,221,701,243,2,23,29,26,15,17])). % 117.40/117.43 cnf(2246,plain, % 117.40/117.43 (~P1(f3(a8,a2),f1(x22461,a2))), % 117.40/117.43 inference(scs_inference,[],[19,2164,2219,2224,2196,1279,1738,1972,1641,221,701,243,2,23,29,26,15,17,14])). % 117.40/117.43 cnf(2247,plain, % 117.40/117.43 (~P1(f3(a8,a2),f1(a2,x22471))), % 117.40/117.43 inference(rename_variables,[],[2219])). % 117.40/117.43 cnf(2249,plain, % 117.40/117.43 (~P1(f3(a8,f1(x22491,a2)),f1(a2,x22492))), % 117.40/117.43 inference(scs_inference,[],[19,2164,2219,2247,2224,2196,1279,1738,1972,1640,1641,221,701,243,2,23,29,26,15,17,14,13])). % 117.40/117.43 cnf(2251,plain, % 117.40/117.43 (E(f7(a2,a2),f7(f1(a2,x22511),f3(a2,x22512)))), % 117.40/117.43 inference(scs_inference,[],[19,2164,2219,2247,2224,2196,1279,1738,1972,1739,1640,1641,1591,221,701,243,2,23,29,26,15,17,14,13,3])). % 117.40/117.43 cnf(2257,plain, % 117.40/117.43 (~P3(f3(a4,f1(a2,x22571)))), % 117.40/117.43 inference(scs_inference,[],[19,2164,2219,2247,2224,2196,1279,1738,1972,1739,1640,1641,1591,221,701,243,2,23,29,26,15,17,14,13,3,27,48,25])). % 117.40/117.43 cnf(2259,plain, % 117.40/117.43 (~E(f1(f1(a4,a4),f1(a4,a4)),f3(a2,x22591))), % 117.40/117.43 inference(scs_inference,[],[2018,2])). % 117.40/117.43 cnf(2270,plain, % 117.40/117.43 (~E(f3(f1(x22701,a2),x22702),f3(a8,a2))), % 117.40/117.43 inference(scs_inference,[],[2213,2243,2251,2018,698,1926,45,672,2,23,28,26,17])). % 117.40/117.43 cnf(2299,plain, % 117.40/117.43 (E(f6(a2,a2),f6(f3(a2,x22991),f1(x22992,a2)))), % 117.40/117.43 inference(scs_inference,[],[19,2246,2270,2147,2249,2257,1697,1696,1593,1676,1778,42,259,20,2,23,26,17,34,14,13,3])). % 117.40/117.43 cnf(2302,plain, % 117.40/117.43 (~E(a2,f1(f1(a4,a4),f1(a4,a4)))), % 117.40/117.43 inference(scs_inference,[],[19,2246,2270,2147,2249,2257,1697,1696,1593,1676,1778,42,259,20,2,23,26,17,34,14,13,3,48])). % 117.40/117.43 cnf(2317,plain, % 117.40/117.43 (P1(f6(a2,a2),f6(f3(a2,x23171),f1(x23172,a2)))), % 117.40/117.43 inference(scs_inference,[],[2299,23])). % 117.40/117.43 cnf(2319,plain, % 117.40/117.43 (~E(f3(a4,f3(x23191,a4)),f3(a2,x23192))), % 117.40/117.43 inference(scs_inference,[],[2299,2245,23,2])). % 117.40/117.43 cnf(2320,plain, % 117.40/117.43 (~P1(f1(f1(a4,a4),f1(a4,a4)),f3(a2,x23201))), % 117.40/117.43 inference(scs_inference,[],[2259,2299,2245,224,23,2,26])). % 117.40/117.43 cnf(2340,plain, % 117.40/117.43 (~E(f1(x23401,a2),f3(f1(a4,a4),f3(x23402,a4)))), % 117.40/117.43 inference(scs_inference,[],[2060,2302,2317,1742,1961,237,23,2,26,17])). % 117.40/117.43 cnf(2347,plain, % 117.40/117.43 (E(f6(a2,a2),f6(f1(x23471,a2),f3(a2,x23472)))), % 117.40/117.43 inference(scs_inference,[],[1785,2060,2302,2317,2108,2073,1742,1961,1594,1695,519,237,23,2,26,17,14,13,3])). % 117.40/117.43 cnf(2350,plain, % 117.40/117.43 (P2(f6(a4,a2),f3(a4,a2))), % 117.40/117.43 inference(scs_inference,[],[20,1785,2060,2302,2317,2108,2073,1742,1961,2164,1594,1695,519,237,23,2,26,17,14,13,3,29])). % 117.40/117.43 cnf(2357,plain, % 117.40/117.43 (~P3(f3(a4,a2))), % 117.40/117.43 inference(scs_inference,[],[20,1785,2060,2302,2317,2108,2073,1742,1961,2164,1594,1695,519,237,23,2,26,17,14,13,3,29,35,36,25])). % 117.40/117.43 cnf(2372,plain, % 117.40/117.43 (~E(f3(a4,f3(x23721,a4)),f3(a2,x23722))), % 117.40/117.43 inference(rename_variables,[],[2319])). % 117.40/117.43 cnf(2378,plain, % 117.40/117.43 (P1(f3(f3(a2,x23781),f1(a2,x23782)),f3(a2,a2))), % 117.40/117.43 inference(scs_inference,[],[20,2357,2350,2320,1940,2319,2347,2340,1595,558,74,224,23,2,29,26,17,14,13])). % 117.40/117.43 cnf(2381,plain, % 117.40/117.43 (~E(f3(a4,a2),f3(a2,x23811))), % 117.40/117.43 inference(scs_inference,[],[20,2357,2350,2320,1940,2319,2372,2347,2340,1595,558,1822,74,224,23,2,29,26,17,14,13,3])). % 117.40/117.43 cnf(2398,plain, % 117.40/117.43 (E(f3(a2,a2),f3(f3(a2,x23981),f1(a2,x23982)))), % 117.40/117.43 inference(scs_inference,[],[20,2381,2378,1651,2179,224,23,2,29,26])). % 117.40/117.43 cnf(3703,plain, % 117.40/117.43 (~P2(x37031,f1(f1(x37032,f3(a2,x37033)),x37034))), % 117.40/117.43 inference(rename_variables,[],[579])). % 117.40/117.43 cnf(3711,plain, % 117.40/117.43 ($false), % 117.40/117.43 inference(scs_inference,[],[2398,447,464,579,3703,518,24,65,2,27,36]), % 117.40/117.43 ['proof']). % 117.40/117.43 % SZS output end Proof % 117.40/117.43 % Total time :116.770000s %------------------------------------------------------------------------------