%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET620+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 : n020.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 162.86s 163.10s % Output : CNFRefutation 163.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SET620+3 : TPTP v8.2.0. Released v2.2.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 17:21:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.50/0.58 start to proof:theBenchmark % 162.79/163.07 %------------------------------------------- % 162.79/163.07 % File :CSE---1.7 % 162.79/163.07 % Problem :theBenchmark % 162.79/163.07 % Transform :cnf % 162.79/163.07 % Format :tptp:raw % 162.79/163.07 % Command :java -jar mcs_scs.jar %d %s % 162.79/163.07 % 162.79/163.07 % Result :Theorem 162.190000s % 162.79/163.07 % Output :CNFRefutation 162.190000s % 162.79/163.07 %------------------------------------------- % 162.86/163.10 %-------------------------------------------------------------------------- % 162.86/163.10 % File : SET620+3 : TPTP v8.2.0. Released v2.2.0. % 162.86/163.10 % Domain : Set Theory % 162.86/163.10 % Problem : X sym\ Y = (X U Y) \ X ^ Y % 162.86/163.10 % Version : [Try90] axioms : Reduced > Incomplete. % 162.86/163.10 % English : The symmetric difference of X and Y is the difference of (the % 162.86/163.10 % union of X and Y) and the intersection of X and Y. % 162.86/163.10 % 162.86/163.10 % Refs : [ILF] The ILF Group (1998), The ILF System: A Tool for the Int % 162.86/163.10 % : [Try90] Trybulec (1990), Tarski Grothendieck Set Theory % 162.86/163.10 % : [TS89] Trybulec & Swieczkowska (1989), Boolean Properties of % 162.86/163.10 % Source : [ILF] % 162.86/163.10 % Names : BOOLE (96) [TS89] % 162.86/163.10 % 162.86/163.10 % Status : Theorem % 162.86/163.10 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.3.0, 0.14 v7.1.0, 0.04 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.23 v6.0.0, 0.26 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.44 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.30 v4.0.1, 0.35 v4.0.0, 0.33 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.21 v3.3.0, 0.14 v3.2.0, 0.18 v3.1.0, 0.11 v2.7.0, 0.00 v2.2.1 % 162.86/163.10 % Syntax : Number of formulae : 14 ( 8 unt; 0 def) % 162.86/163.10 % Number of atoms : 26 ( 9 equ) % 162.86/163.10 % Maximal formula atoms : 3 ( 1 avg) % 162.86/163.10 % Number of connectives : 13 ( 1 ~; 1 |; 3 &) % 162.86/163.10 % ( 7 <=>; 1 =>; 0 <=; 0 <~>) % 162.86/163.10 % Maximal formula depth : 7 ( 4 avg) % 162.86/163.10 % Maximal term depth : 3 ( 1 avg) % 162.86/163.10 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 162.86/163.10 % Number of functors : 4 ( 4 usr; 0 con; 2-2 aty) % 162.86/163.10 % Number of variables : 33 ( 33 !; 0 ?) % 162.86/163.10 % SPC : FOF_THM_RFO_SEQ % 162.86/163.10 % 162.86/163.10 % Comments : % 162.86/163.10 %-------------------------------------------------------------------------- % 162.86/163.10 %---- line(boole - df(7),1833089) % 162.86/163.10 fof(symmetric_difference_defn,axiom, % 162.86/163.10 ! [B,C] : symmetric_difference(B,C) = union(difference(B,C),difference(C,B)) ). % 162.86/163.10 % 162.86/163.10 %---- line(boole - th(77),1833883) % 162.86/163.10 fof(difference_into_intersection,axiom, % 162.86/163.10 ! [B,C] : difference(B,intersection(B,C)) = difference(B,C) ). % 162.86/163.10 % 162.86/163.10 %---- line(boole - th(89),1834187) % 162.86/163.10 fof(difference_distributes_over_union,axiom, % 162.86/163.10 ! [B,C,D] : difference(union(B,C),D) = union(difference(B,D),difference(C,D)) ). % 162.86/163.10 % 162.86/163.10 %---- line(boole - df(2),1833042) % 162.86/163.10 fof(union_defn,axiom, % 162.86/163.10 ! [B,C,D] : % 162.86/163.10 ( member(D,union(B,C)) % 162.86/163.10 <=> ( member(D,B) % 162.86/163.10 | member(D,C) ) ) ). % 162.86/163.10 % 162.86/163.10 %---- line(boole - df(3),1833060) % 162.86/163.10 fof(intersection_defn,axiom, % 162.86/163.10 ! [B,C,D] : % 162.86/163.10 ( member(D,intersection(B,C)) % 162.86/163.10 <=> ( member(D,B) % 162.86/163.10 & member(D,C) ) ) ). % 162.86/163.10 % 162.86/163.10 %---- line(boole - df(4),1833078) % 162.86/163.10 fof(difference_defn,axiom, % 162.86/163.10 ! [B,C,D] : % 162.86/163.10 ( member(D,difference(B,C)) % 162.86/163.10 <=> ( member(D,B) % 162.86/163.10 & ~ member(D,C) ) ) ). % 162.86/163.10 % 162.86/163.10 %---- line(boole - df(8),1833103) % 162.86/163.10 fof(equal_defn,axiom, % 162.86/163.10 ! [B,C] : % 162.86/163.10 ( B = C % 162.86/163.10 <=> ( subset(B,C) % 162.86/163.10 & subset(C,B) ) ) ). % 162.86/163.10 % 162.86/163.10 %---- property(commutativity,op(union,2,function)) % 162.86/163.10 fof(commutativity_of_union,axiom, % 162.86/163.10 ! [B,C] : union(B,C) = union(C,B) ). % 162.86/163.10 % 162.86/163.10 %---- property(commutativity,op(intersection,2,function)) % 162.86/163.10 fof(commutativity_of_intersection,axiom, % 162.86/163.10 ! [B,C] : intersection(B,C) = intersection(C,B) ). % 162.86/163.10 % 162.86/163.10 %---- property(commutativity,op(symmetric_difference,2,function)) % 162.86/163.10 fof(commutativity_of_symmetric_difference,axiom, % 162.86/163.10 ! [B,C] : symmetric_difference(B,C) = symmetric_difference(C,B) ). % 162.86/163.10 % 162.86/163.10 %---- line(hidden - axiom177,1832615) % 162.86/163.10 fof(equal_member_defn,axiom, % 162.86/163.10 ! [B,C] : % 162.86/163.10 ( B = C % 162.86/163.10 <=> ! [D] : % 162.86/163.10 ( member(D,B) % 162.86/163.10 <=> member(D,C) ) ) ). % 162.86/163.10 % 162.86/163.10 %---- line(tarski - df(3),1832749) % 162.86/163.10 fof(subset_defn,axiom, % 162.86/163.10 ! [B,C] : % 162.86/163.10 ( subset(B,C) % 162.86/163.10 <=> ! [D] : % 162.86/163.10 ( member(D,B) % 162.86/163.10 => member(D,C) ) ) ). % 162.86/163.10 % 162.86/163.10 %---- property(reflexivity,op(subset,2,predicate)) % 162.86/163.10 fof(reflexivity_of_subset,axiom, % 162.86/163.10 ! [B] : subset(B,B) ). % 162.86/163.10 % 162.86/163.10 %---- line(boole - th(96),1834227) % 162.86/163.10 fof(prove_th96,conjecture, % 162.86/163.10 ! [B,C] : symmetric_difference(B,C) = difference(union(B,C),intersection(B,C)) ). % 162.86/163.10 % 162.86/163.10 %-------------------------------------------------------------------------- % 162.86/163.10 %------------------------------------------- % 162.86/163.10 % Proof found % 162.86/163.10 % SZS status Theorem for theBenchmark % 162.86/163.10 % SZS output start Proof % 162.86/163.13 %ClaNum:41(EqnAxiom:17) % 162.86/163.13 %VarNum:115(SingletonVarNum:52) % 162.86/163.13 %MaxLitNum:3 % 162.86/163.13 %MaxfuncDepth:2 % 162.86/163.13 %SharedTerms:9 % 162.86/163.13 %goalClause: 24 % 162.86/163.13 %singleGoalClaCount:1 % 162.86/163.13 [24]~E(f3(f1(a4,a7),f2(a4,a7)),f1(f3(a4,a7),f3(a7,a4))) % 162.86/163.13 [18]P1(x181,x181) % 162.86/163.13 [19]E(f1(x191,x192),f1(x192,x191)) % 162.86/163.13 [20]E(f2(x201,x202),f2(x202,x201)) % 162.86/163.13 [21]E(f3(x211,f2(x211,x212)),f3(x211,x212)) % 162.86/163.13 [22]E(f1(f3(x221,x222),f3(x223,x222)),f3(f1(x221,x223),x222)) % 162.86/163.13 [26]~E(x261,x262)+P1(x261,x262) % 162.86/163.13 [28]P1(x281,x282)+P2(f5(x281,x282),x281) % 162.86/163.13 [36]P1(x361,x362)+~P2(f5(x361,x362),x362) % 162.86/163.13 [30]~P2(x301,x303)+P2(x301,f1(x302,x303)) % 162.86/163.13 [31]~P2(x311,x312)+P2(x311,f1(x312,x313)) % 162.86/163.13 [33]P2(x331,x332)+~P2(x331,f3(x332,x333)) % 162.86/163.13 [34]P2(x341,x342)+~P2(x341,f2(x343,x342)) % 162.86/163.13 [35]P2(x351,x352)+~P2(x351,f2(x352,x353)) % 162.86/163.13 [39]~P2(x391,x392)+~P2(x391,f3(x393,x392)) % 162.86/163.13 [27]~P1(x272,x271)+~P1(x271,x272)+E(x271,x272) % 162.86/163.13 [37]E(x371,x372)+P2(f6(x371,x372),x372)+P2(f6(x371,x372),x371) % 162.86/163.13 [41]E(x411,x412)+~P2(f6(x411,x412),x412)+~P2(f6(x411,x412),x411) % 162.86/163.13 [29]~P1(x293,x292)+P2(x291,x292)+~P2(x291,x293) % 162.86/163.13 [32]~P2(x321,x323)+P2(x321,x322)+P2(x321,f3(x323,x322)) % 162.86/163.13 [38]~P2(x381,x383)+~P2(x381,x382)+P2(x381,f2(x382,x383)) % 162.86/163.13 [40]P2(x401,x402)+P2(x401,x403)+~P2(x401,f1(x403,x402)) % 162.86/163.13 %EqnAxiom % 162.86/163.13 [1]E(x11,x11) % 162.86/163.13 [2]E(x22,x21)+~E(x21,x22) % 162.86/163.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 162.86/163.13 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43)) % 162.86/163.13 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52)) % 162.86/163.13 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63)) % 162.86/163.13 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72)) % 162.86/163.13 [8]~E(x81,x82)+E(f2(x81,x83),f2(x82,x83)) % 162.86/163.13 [9]~E(x91,x92)+E(f2(x93,x91),f2(x93,x92)) % 162.86/163.13 [10]~E(x101,x102)+E(f5(x101,x103),f5(x102,x103)) % 162.86/163.13 [11]~E(x111,x112)+E(f5(x113,x111),f5(x113,x112)) % 162.86/163.13 [12]~E(x121,x122)+E(f3(x121,x123),f3(x122,x123)) % 162.86/163.13 [13]~E(x131,x132)+E(f3(x133,x131),f3(x133,x132)) % 162.86/163.13 [14]P1(x142,x143)+~E(x141,x142)+~P1(x141,x143) % 162.86/163.13 [15]P1(x153,x152)+~E(x151,x152)+~P1(x153,x151) % 162.86/163.13 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163) % 162.86/163.13 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171) % 162.86/163.13 % 162.86/163.13 %------------------------------------------- % 162.86/163.17 cnf(43,plain, % 162.86/163.17 (E(f3(x431,x432),f3(x431,f2(x431,x432)))), % 162.86/163.17 inference(scs_inference,[],[21,2])). % 162.86/163.17 cnf(44,plain, % 162.86/163.17 (~E(f3(f1(a4,a7),f2(a4,a7)),f1(f3(a7,a4),f3(a4,a7)))), % 162.86/163.17 inference(scs_inference,[],[24,19,21,2,3])). % 162.86/163.17 cnf(45,plain, % 162.86/163.17 (E(f1(x451,x452),f1(x452,x451))), % 162.86/163.17 inference(rename_variables,[],[19])). % 162.86/163.17 cnf(46,plain, % 162.86/163.17 (P1(f1(x461,x462),f1(x462,x461))), % 162.86/163.17 inference(scs_inference,[],[24,18,19,45,21,2,3,14])). % 162.86/163.17 cnf(48,plain, % 162.86/163.17 (E(f3(f1(x481,x482),x483),f1(f3(x481,x483),f3(x482,x483)))), % 162.86/163.17 inference(scs_inference,[],[22,2])). % 162.86/163.17 cnf(50,plain, % 162.86/163.17 (P1(f1(x501,x502),f1(x502,x501))), % 162.86/163.17 inference(rename_variables,[],[46])). % 162.86/163.17 cnf(53,plain, % 162.86/163.17 (E(f1(f3(x531,x532),f3(x533,x532)),f3(f1(x533,x531),x532))), % 162.86/163.17 inference(scs_inference,[],[46,50,22,19,2,15,14,3])). % 162.86/163.17 cnf(55,plain, % 162.86/163.17 (E(f3(f1(x551,x552),x553),f1(f3(x552,x553),f3(x551,x553)))), % 162.86/163.17 inference(scs_inference,[],[46,50,22,19,2,15,14,3,27])). % 162.86/163.17 cnf(57,plain, % 162.86/163.17 (P1(f3(x571,x572),f3(x571,f2(x571,x572)))), % 162.86/163.17 inference(scs_inference,[],[43,18,15])). % 162.86/163.17 cnf(58,plain, % 162.86/163.17 (P1(x581,x581)), % 162.86/163.17 inference(rename_variables,[],[18])). % 162.86/163.17 cnf(59,plain, % 162.86/163.17 (P1(f3(x591,f2(x591,x592)),f3(x591,x592))), % 162.86/163.17 inference(scs_inference,[],[43,18,58,15,14])). % 162.86/163.17 cnf(61,plain, % 162.86/163.17 (E(f3(f1(x611,x612),x613),f3(f1(x612,x611),x613))), % 162.86/163.17 inference(scs_inference,[],[43,48,53,18,58,15,14,3])). % 162.86/163.17 cnf(64,plain, % 162.86/163.17 (P1(f1(x641,x642),f1(x642,x641))), % 162.86/163.17 inference(rename_variables,[],[46])). % 162.86/163.17 cnf(65,plain, % 162.86/163.17 (P1(f3(f1(x651,x652),x653),f1(f3(x651,x653),f3(x652,x653)))), % 162.86/163.17 inference(scs_inference,[],[53,46,64,15,14])). % 162.86/163.17 cnf(67,plain, % 162.86/163.17 (P1(f3(f1(x671,x672),x673),f3(f1(x672,x671),x673))), % 162.86/163.17 inference(scs_inference,[],[53,65,15])). % 162.86/163.17 cnf(71,plain, % 162.86/163.17 (P2(x711,x712)+~P2(x711,f3(f2(x713,x712),x714))), % 162.86/163.17 inference(scs_inference,[],[33,34])). % 162.86/163.17 cnf(72,plain, % 162.86/163.17 (P1(f2(x721,x722),f2(x722,x721))), % 162.86/163.17 inference(scs_inference,[],[20,18,14])). % 162.86/163.17 cnf(74,plain, % 162.86/163.17 (P1(x741,x742)+~P2(f5(x741,x742),f2(x742,x743))), % 162.86/163.17 inference(scs_inference,[],[35,36])). % 162.86/163.17 cnf(76,plain, % 162.86/163.17 (P1(f3(x761,f2(x761,f2(x761,x762))),f3(x761,x762))), % 162.86/163.17 inference(scs_inference,[],[21,59,15])). % 162.86/163.17 cnf(78,plain, % 162.86/163.17 (P1(f3(x781,x782),f3(x781,f2(x781,f2(x781,x782))))), % 162.86/163.17 inference(scs_inference,[],[21,59,57,15,14])). % 162.86/163.17 cnf(80,plain, % 162.86/163.17 (E(f3(x801,f2(x801,f2(x801,x802))),f3(x801,x802))), % 162.86/163.17 inference(scs_inference,[],[21,59,57,15,14,27])). % 162.86/163.17 cnf(82,plain, % 162.86/163.17 (E(f3(x821,x822),f3(x821,f2(x821,f2(x821,x822))))), % 162.86/163.17 inference(scs_inference,[],[21,59,57,15,14,27,2])). % 162.86/163.17 cnf(120,plain, % 162.86/163.17 (E(f1(f1(f3(x1201,x1202),f3(x1203,x1202)),x1204),f1(f3(f1(x1201,x1203),x1202),x1204))), % 162.86/163.17 inference(scs_inference,[],[48,2,4])). % 162.86/163.17 cnf(121,plain, % 162.86/163.17 (E(f3(x1211,f1(x1212,x1213)),f3(x1211,f1(x1213,x1212)))), % 162.86/163.17 inference(scs_inference,[],[19,2,13])). % 162.86/163.17 cnf(122,plain, % 162.86/163.17 (P1(f3(f1(x1221,x1222),f1(x1223,x1224)),f3(f1(x1222,x1221),f1(x1224,x1223)))), % 162.86/163.17 inference(scs_inference,[],[121,67,15])). % 162.86/163.17 cnf(125,plain, % 162.86/163.17 (E(f1(x1251,f1(x1252,x1253)),f1(x1251,f1(x1253,x1252)))), % 162.86/163.17 inference(scs_inference,[],[19,2,5])). % 162.86/163.17 cnf(129,plain, % 162.86/163.17 (E(f2(x1291,f3(x1292,f2(x1292,x1293))),f2(x1291,f3(x1292,x1293)))), % 162.86/163.17 inference(scs_inference,[],[43,2,9])). % 162.86/163.17 cnf(131,plain, % 162.86/163.17 (P1(f3(x1311,f1(x1312,x1313)),f3(x1311,f1(x1313,x1312)))), % 162.86/163.17 inference(scs_inference,[],[121,18,15])). % 162.86/163.17 cnf(152,plain, % 162.86/163.17 (E(f2(f3(x1521,f2(x1521,x1522)),x1523),f2(f3(x1521,x1522),x1523))), % 162.86/163.17 inference(scs_inference,[],[43,2,8])). % 162.86/163.17 cnf(153,plain, % 162.86/163.17 (P1(f1(x1531,f1(x1532,x1533)),f1(x1531,f1(x1533,x1532)))), % 162.86/163.17 inference(scs_inference,[],[125,2,26])). % 162.86/163.17 cnf(154,plain, % 162.86/163.17 (P1(f1(x1541,f1(x1542,x1543)),f1(f1(x1543,x1542),x1541))), % 162.86/163.17 inference(scs_inference,[],[125,46,14])). % 162.86/163.17 cnf(155,plain, % 162.86/163.17 (P1(f1(x1551,x1552),f1(x1552,x1551))), % 162.86/163.17 inference(rename_variables,[],[46])). % 162.86/163.17 cnf(156,plain, % 162.86/163.17 (P1(f1(f1(x1561,x1562),x1563),f1(x1563,f1(x1562,x1561)))), % 162.86/163.17 inference(scs_inference,[],[125,46,155,14,15])). % 162.86/163.17 cnf(180,plain, % 162.86/163.17 (E(f6(f1(x1801,x1802),x1803),f6(f1(x1802,x1801),x1803))), % 162.86/163.17 inference(scs_inference,[],[19,2,6])). % 162.86/163.17 cnf(181,plain, % 162.86/163.17 (E(f3(x1811,f2(x1812,x1813)),f3(x1811,f2(x1813,x1812)))), % 162.86/163.17 inference(scs_inference,[],[20,2,13])). % 162.86/163.17 cnf(184,plain, % 162.86/163.17 (E(f5(f3(x1841,f2(x1841,x1842)),x1843),f5(f3(x1841,x1842),x1843))), % 162.86/163.17 inference(scs_inference,[],[43,2,10])). % 162.86/163.17 cnf(200,plain, % 162.86/163.17 (E(f6(x2001,f3(x2002,f2(x2002,f2(x2002,x2003)))),f6(x2001,f3(x2002,x2003)))), % 162.86/163.17 inference(scs_inference,[],[82,2,7])). % 162.86/163.17 cnf(209,plain, % 162.86/163.17 (E(f5(x2091,f1(f3(x2092,x2093),f3(x2094,x2093))),f5(x2091,f3(f1(x2094,x2092),x2093)))), % 162.86/163.17 inference(scs_inference,[],[55,2,11])). % 162.86/163.17 cnf(213,plain, % 162.86/163.17 (E(f6(x2131,f3(x2132,f2(x2132,x2133))),f6(x2131,f3(x2132,x2133)))), % 162.86/163.17 inference(scs_inference,[],[43,2,7])). % 162.86/163.17 cnf(217,plain, % 162.86/163.17 (E(f3(x2171,f2(f2(x2171,x2172),x2171)),f3(x2171,x2172))), % 162.86/163.17 inference(scs_inference,[],[181,80,3])). % 162.86/163.17 cnf(219,plain, % 162.86/163.17 (E(f3(x2191,f2(x2192,x2193)),f3(x2191,f2(x2193,x2192)))), % 162.86/163.17 inference(rename_variables,[],[181])). % 162.86/163.17 cnf(220,plain, % 162.86/163.17 (P1(f3(x2201,f2(f2(x2201,x2202),x2201)),f3(x2201,x2202))), % 162.86/163.17 inference(scs_inference,[],[181,219,80,76,3,14])). % 162.86/163.17 cnf(222,plain, % 162.86/163.17 (E(f3(x2221,f2(x2222,x2223)),f3(x2221,f2(x2223,x2222)))), % 162.86/163.17 inference(rename_variables,[],[181])). % 162.86/163.17 cnf(223,plain, % 162.86/163.17 (P1(f3(x2231,x2232),f3(x2231,f2(f2(x2231,x2232),x2231)))), % 162.86/163.17 inference(scs_inference,[],[181,219,222,80,78,76,3,14,15])). % 162.86/163.17 cnf(226,plain, % 162.86/163.17 (P1(f3(x2261,f2(x2262,x2263)),f3(x2261,f2(x2263,x2262)))), % 162.86/163.17 inference(scs_inference,[],[181,2,26])). % 162.86/163.17 cnf(227,plain, % 162.86/163.17 (E(f3(x2271,x2272),f3(x2271,f2(f2(x2271,x2272),x2271)))), % 162.86/163.17 inference(scs_inference,[],[217,2])). % 162.86/163.17 cnf(228,plain, % 162.86/163.17 (E(f3(x2281,f2(x2282,x2281)),f3(x2281,x2282))), % 162.86/163.17 inference(scs_inference,[],[181,217,21,2,3])). % 162.86/163.17 cnf(230,plain, % 162.86/163.17 (E(f3(x2301,f2(x2302,x2303)),f3(x2301,f2(x2303,x2302)))), % 162.86/163.17 inference(rename_variables,[],[181])). % 162.86/163.17 cnf(231,plain, % 162.86/163.17 (P1(f3(x2311,f2(x2312,x2311)),f3(x2311,x2312))), % 162.86/163.17 inference(scs_inference,[],[181,230,217,59,21,2,3,14])). % 162.86/163.17 cnf(233,plain, % 162.86/163.17 (E(f3(x2331,f2(x2332,x2333)),f3(x2331,f2(x2333,x2332)))), % 162.86/163.17 inference(rename_variables,[],[181])). % 162.86/163.17 cnf(234,plain, % 162.86/163.17 (P1(f3(x2341,x2342),f3(x2341,f2(x2342,x2341)))), % 162.86/163.17 inference(scs_inference,[],[181,230,233,217,59,57,21,2,3,14,15])). % 162.86/163.17 cnf(238,plain, % 162.86/163.17 (E(f3(x2381,x2382),f3(x2381,f2(x2382,x2381)))), % 162.86/163.17 inference(scs_inference,[],[228,2])). % 162.86/163.17 cnf(239,plain, % 162.86/163.17 (P1(f3(f1(x2391,x2392),f2(x2393,x2394)),f3(f1(x2392,x2391),f2(x2394,x2393)))), % 162.86/163.17 inference(scs_inference,[],[181,228,67,2,14])). % 162.86/163.17 cnf(243,plain, % 162.86/163.17 (E(f3(f3(x2431,f2(x2432,x2431)),x2433),f3(f3(x2431,x2432),x2433))), % 162.86/163.17 inference(scs_inference,[],[238,2,12])). % 162.86/163.17 cnf(245,plain, % 162.86/163.17 (E(f1(f3(x2451,f2(f2(x2451,x2452),x2451)),x2453),f1(f3(x2451,x2452),x2453))), % 162.86/163.17 inference(scs_inference,[],[227,2,4])). % 162.86/163.17 cnf(246,plain, % 162.86/163.17 (P1(f3(x2461,x2462),f3(x2461,f2(f2(x2462,x2461),x2461)))), % 162.86/163.17 inference(scs_inference,[],[228,234,14])). % 162.86/163.17 cnf(248,plain, % 162.86/163.17 (P1(f3(x2481,f2(f2(x2482,x2481),x2481)),f3(x2481,x2482))), % 162.86/163.17 inference(scs_inference,[],[228,231,234,14,15])). % 162.86/163.17 cnf(250,plain, % 162.86/163.17 (E(f1(x2501,f3(x2502,f2(x2503,x2502))),f1(x2501,f3(x2502,x2503)))), % 162.86/163.17 inference(scs_inference,[],[238,2,5])). % 162.86/163.17 cnf(253,plain, % 162.86/163.17 (E(f3(x2531,x2532),f3(x2531,f2(x2531,f2(x2532,x2531))))), % 162.86/163.17 inference(scs_inference,[],[238,43,3])). % 162.86/163.17 cnf(255,plain, % 162.86/163.17 (E(f3(x2551,f2(x2551,f2(x2552,x2551))),f3(x2551,x2552))), % 162.86/163.17 inference(scs_inference,[],[238,43,3,2])). % 162.86/163.17 cnf(257,plain, % 162.86/163.17 (P1(f3(x2571,f2(x2571,f2(x2572,x2571))),f3(x2571,x2572))), % 162.86/163.17 inference(scs_inference,[],[253,18,14])). % 162.86/163.17 cnf(262,plain, % 162.86/163.17 (E(f5(f3(x2621,f2(f2(x2621,x2622),x2621)),x2623),f5(f3(x2621,x2622),x2623))), % 162.86/163.17 inference(scs_inference,[],[227,2,10])). % 162.86/163.17 cnf(266,plain, % 162.86/163.17 (E(f1(f3(x2661,f2(x2662,x2661)),x2663),f1(f3(x2661,x2662),x2663))), % 162.86/163.17 inference(scs_inference,[],[238,2,4])). % 162.86/163.17 cnf(269,plain, % 162.86/163.17 (E(f3(x2691,f2(f2(x2692,x2691),x2691)),f3(x2691,x2692))), % 162.86/163.17 inference(scs_inference,[],[246,248,27])). % 162.86/163.17 cnf(272,plain, % 162.86/163.17 (E(f3(x2721,x2722),f3(x2721,f2(f2(x2722,x2721),x2721)))), % 162.86/163.17 inference(scs_inference,[],[246,248,27,2])). % 162.86/163.17 cnf(283,plain, % 162.86/163.17 (E(f2(f1(x2831,x2832),x2833),f2(f1(x2832,x2831),x2833))), % 162.86/163.17 inference(scs_inference,[],[19,2,8])). % 162.86/163.17 cnf(284,plain, % 162.86/163.17 (P1(f2(f1(x2841,x2842),x2843),f2(x2843,f1(x2842,x2841)))), % 162.86/163.17 inference(scs_inference,[],[283,72,14])). % 162.86/163.17 cnf(285,plain, % 162.86/163.17 (P1(f2(x2851,x2852),f2(x2852,x2851))), % 162.86/163.17 inference(rename_variables,[],[72])). % 162.86/163.17 cnf(286,plain, % 162.86/163.17 (P1(f2(x2861,f1(x2862,x2863)),f2(f1(x2863,x2862),x2861))), % 162.86/163.17 inference(scs_inference,[],[283,72,285,14,15])). % 162.86/163.17 cnf(288,plain, % 162.86/163.17 (E(f2(x2881,f1(x2882,x2883)),f2(x2881,f1(x2883,x2882)))), % 162.86/163.17 inference(scs_inference,[],[19,2,9])). % 162.86/163.17 cnf(289,plain, % 162.86/163.17 (P1(f2(f1(x2891,x2892),f1(x2893,x2894)),f2(f1(x2894,x2893),f1(x2892,x2891)))), % 162.86/163.17 inference(scs_inference,[],[288,284,14])). % 162.86/163.17 cnf(292,plain, % 162.86/163.17 (E(f5(f1(x2921,x2922),x2923),f5(f1(x2922,x2921),x2923))), % 162.86/163.17 inference(scs_inference,[],[19,2,10])). % 162.86/163.17 cnf(293,plain, % 162.86/163.17 (E(f5(x2931,f2(x2932,x2933)),f5(x2931,f2(x2933,x2932)))), % 162.86/163.17 inference(scs_inference,[],[20,2,11])). % 162.86/163.17 cnf(294,plain, % 162.86/163.17 (P1(f2(x2941,f1(x2942,x2943)),f2(x2941,f1(x2943,x2942)))), % 162.86/163.17 inference(scs_inference,[],[20,286,15])). % 162.86/163.17 cnf(295,plain, % 162.86/163.17 (P1(f2(x2951,f1(x2952,x2953)),f2(f1(x2953,x2952),x2951))), % 162.86/163.17 inference(rename_variables,[],[286])). % 162.86/163.17 cnf(296,plain, % 162.86/163.17 (E(f2(x2961,x2962),f2(x2962,x2961))), % 162.86/163.17 inference(rename_variables,[],[20])). % 162.86/163.17 cnf(297,plain, % 162.86/163.17 (P1(f2(f1(x2971,x2972),x2973),f2(f1(x2972,x2971),x2973))), % 162.86/163.17 inference(scs_inference,[],[20,296,286,295,15,14])). % 162.86/163.17 cnf(300,plain, % 162.86/163.17 (E(f3(f2(x3001,x3002),x3003),f3(f2(x3002,x3001),x3003))), % 162.86/163.17 inference(scs_inference,[],[20,2,12])). % 162.86/163.17 cnf(301,plain, % 162.86/163.17 (P1(f2(f1(x3011,x3012),f1(x3013,x3014)),f2(f1(x3012,x3011),f1(x3014,x3013)))), % 162.86/163.17 inference(scs_inference,[],[20,289,15])). % 162.86/163.17 cnf(303,plain, % 162.86/163.17 (E(f1(f2(x3031,x3032),x3033),f1(f2(x3032,x3031),x3033))), % 162.86/163.17 inference(scs_inference,[],[20,2,4])). % 162.86/163.17 cnf(304,plain, % 162.86/163.17 (P1(f1(f2(x3041,x3042),f1(x3043,x3044)),f1(f2(x3042,x3041),f1(x3044,x3043)))), % 162.86/163.17 inference(scs_inference,[],[303,153,14])). % 162.86/163.17 cnf(306,plain, % 162.86/163.17 (E(f1(f2(x3061,x3062),x3063),f1(f2(x3062,x3061),x3063))), % 162.86/163.17 inference(rename_variables,[],[303])). % 162.86/163.17 cnf(307,plain, % 162.86/163.17 (P1(f1(f1(x3071,x3072),f2(x3073,x3074)),f1(f2(x3074,x3073),f1(x3072,x3071)))), % 162.86/163.17 inference(scs_inference,[],[303,306,153,156,14,15])). % 162.86/163.17 cnf(314,plain, % 162.86/163.17 (E(f1(x3141,f2(x3142,x3143)),f1(x3141,f2(x3143,x3142)))), % 162.86/163.17 inference(scs_inference,[],[20,2,5])). % 162.86/163.17 cnf(317,plain, % 162.86/163.17 (E(f6(f3(x3171,f2(x3171,x3172)),x3173),f6(f3(x3171,x3172),x3173))), % 162.86/163.17 inference(scs_inference,[],[43,2,6])). % 162.86/163.17 cnf(325,plain, % 162.86/163.17 (P1(f1(x3251,f2(x3252,x3253)),f1(f2(x3253,x3252),x3251))), % 162.86/163.17 inference(scs_inference,[],[303,46,15])). % 162.86/163.17 cnf(327,plain, % 162.86/163.17 (P1(f1(f2(x3271,x3272),f1(x3273,x3274)),f1(f1(x3274,x3273),f2(x3272,x3271)))), % 162.86/163.17 inference(scs_inference,[],[303,154,46,15,14])). % 162.86/163.17 cnf(329,plain, % 162.86/163.17 (E(f1(f2(x3291,x3292),x3293),f1(f2(x3292,x3291),x3293))), % 162.86/163.17 inference(rename_variables,[],[303])). % 162.86/163.17 cnf(330,plain, % 162.86/163.17 (E(f1(f2(x3301,x3302),f1(x3303,x3304)),f1(f1(x3304,x3303),f2(x3302,x3301)))), % 162.86/163.17 inference(scs_inference,[],[303,307,154,46,15,14,27])). % 162.86/163.17 cnf(332,plain, % 162.86/163.17 (E(f1(f2(x3321,x3322),f1(x3323,x3324)),f1(f1(x3324,x3323),f2(x3321,x3322)))), % 162.86/163.17 inference(scs_inference,[],[303,329,307,154,46,15,14,27,3])). % 162.86/163.17 cnf(334,plain, % 162.86/163.17 (E(f1(f1(x3341,x3342),f2(x3343,x3344)),f1(f2(x3344,x3343),f1(x3342,x3341)))), % 162.86/163.17 inference(scs_inference,[],[303,329,307,154,46,15,14,27,3,2])). % 162.86/163.17 cnf(336,plain, % 162.86/163.17 (E(f1(f1(x3361,x3362),f2(x3363,x3364)),f1(f2(x3363,x3364),f1(x3362,x3361)))), % 162.86/163.17 inference(scs_inference,[],[332,2])). % 162.86/163.17 cnf(341,plain, % 162.86/163.17 (E(f1(f2(x3411,x3412),f1(x3413,x3414)),f1(f1(x3413,x3414),f2(x3412,x3411)))), % 162.86/163.17 inference(scs_inference,[],[332,304,325,327,2,15,14,27])). % 162.86/163.17 cnf(344,plain, % 162.86/163.17 (E(f1(f1(x3441,x3442),f2(x3443,x3444)),f1(f1(x3442,x3441),f2(x3443,x3444)))), % 162.86/163.17 inference(scs_inference,[],[332,334,304,325,327,2,15,14,27,3])). % 162.86/163.17 cnf(346,plain, % 162.86/163.17 (E(f1(f1(x3461,x3462),f2(x3463,x3464)),f1(f2(x3464,x3463),f1(x3461,x3462)))), % 162.86/163.17 inference(scs_inference,[],[341,2])). % 162.86/163.17 cnf(360,plain, % 162.86/163.17 (E(f1(f1(x3601,x3602),f2(x3603,x3604)),f1(f1(x3602,x3601),f2(x3604,x3603)))), % 162.86/163.17 inference(scs_inference,[],[346,332,3])). % 162.86/163.17 cnf(371,plain, % 162.86/163.17 (E(f5(f3(x3711,f2(x3711,f2(x3711,x3712))),x3713),f5(f3(x3711,x3712),x3713))), % 162.86/163.17 inference(scs_inference,[],[82,2,10])). % 162.86/163.17 cnf(397,plain, % 162.86/163.17 (E(f5(x3971,f3(x3972,f2(f2(x3972,x3973),x3972))),f5(x3971,f3(x3972,x3973)))), % 162.86/163.17 inference(scs_inference,[],[227,2,11])). % 162.86/163.17 cnf(401,plain, % 162.86/163.17 (E(f6(f3(x4011,f2(x4012,x4011)),x4013),f6(f3(x4011,x4012),x4013))), % 162.86/163.17 inference(scs_inference,[],[238,2,6])). % 162.86/163.17 cnf(405,plain, % 162.86/163.17 (E(f6(x4051,f3(x4052,f2(f2(x4053,x4052),x4052))),f6(x4051,f3(x4052,x4053)))), % 162.86/163.17 inference(scs_inference,[],[272,2,7])). % 162.86/163.17 cnf(408,plain, % 162.86/163.17 (E(f5(f3(x4081,f2(x4081,f2(x4082,x4081))),x4083),f5(f3(x4081,x4082),x4083))), % 162.86/163.17 inference(scs_inference,[],[253,2,10])). % 162.86/163.17 cnf(428,plain, % 162.86/163.17 (P1(f3(f2(x4281,x4282),f1(x4283,x4284)),f3(f2(x4282,x4281),f1(x4284,x4283)))), % 162.86/163.17 inference(scs_inference,[],[300,131,15])). % 162.86/163.17 cnf(430,plain, % 162.86/163.17 (E(f3(f2(x4301,x4302),x4303),f3(f2(x4302,x4301),x4303))), % 162.86/163.17 inference(rename_variables,[],[300])). % 162.86/163.17 cnf(431,plain, % 162.86/163.17 (P1(f3(f2(x4311,x4312),f2(x4313,x4314)),f3(f2(x4312,x4311),f2(x4314,x4313)))), % 162.86/163.17 inference(scs_inference,[],[300,430,131,226,15,14])). % 162.86/163.17 cnf(448,plain, % 162.86/163.17 (E(f3(x4481,f3(x4482,f2(x4483,x4482))),f3(x4481,f3(x4482,x4483)))), % 162.86/163.17 inference(scs_inference,[],[238,2,13])). % 162.86/163.17 cnf(471,plain, % 162.86/163.17 (E(f6(x4711,f1(x4712,x4713)),f6(x4711,f1(x4713,x4712)))), % 162.86/163.17 inference(scs_inference,[],[19,2,7])). % 162.86/163.17 cnf(472,plain, % 162.86/163.17 (E(f2(f2(x4721,x4722),x4723),f2(f2(x4722,x4721),x4723))), % 162.86/163.17 inference(scs_inference,[],[20,2,8])). % 162.86/163.17 cnf(476,plain, % 162.86/163.17 (E(f2(f2(x4761,x4762),x4763),f2(f2(x4762,x4761),x4763))), % 162.86/163.17 inference(rename_variables,[],[472])). % 162.86/163.17 cnf(477,plain, % 162.86/163.17 (P1(f2(f2(x4771,x4772),f1(x4773,x4774)),f2(f1(x4774,x4773),f2(x4772,x4771)))), % 162.86/163.17 inference(scs_inference,[],[472,476,294,286,15,14])). % 162.86/163.17 cnf(486,plain, % 162.86/163.17 (E(f5(x4861,f3(x4862,f2(x4862,x4863))),f5(x4861,f3(x4862,x4863)))), % 162.86/163.17 inference(scs_inference,[],[43,2,11])). % 162.86/163.17 cnf(494,plain, % 162.86/163.17 (E(f2(f1(x4941,x4942),f2(x4943,x4944)),f2(f2(x4944,x4943),f1(x4942,x4941)))), % 162.86/163.17 inference(scs_inference,[],[472,477,284,15,27])). % 162.86/163.17 cnf(496,plain, % 162.86/163.17 (E(f2(f2(x4961,x4962),f1(x4963,x4964)),f2(f1(x4964,x4963),f2(x4962,x4961)))), % 162.86/163.17 inference(scs_inference,[],[472,477,284,15,27,2])). % 162.86/163.17 cnf(498,plain, % 162.86/163.17 (P1(f2(f1(x4981,x4982),f2(x4983,x4984)),f2(f2(x4984,x4983),f1(x4981,x4982)))), % 162.86/163.17 inference(scs_inference,[],[494,297,15])). % 162.86/163.17 cnf(499,plain, % 162.86/163.17 (P1(f2(f1(x4991,x4992),x4993),f2(f1(x4992,x4991),x4993))), % 162.86/163.17 inference(rename_variables,[],[297])). % 162.86/163.17 cnf(500,plain, % 162.86/163.17 (P1(f2(f2(x5001,x5002),f1(x5003,x5004)),f2(f1(x5003,x5004),f2(x5002,x5001)))), % 162.86/163.17 inference(scs_inference,[],[494,297,499,15,14])). % 162.86/163.17 cnf(503,plain, % 162.86/163.17 (E(f2(f1(x5031,x5032),f2(x5033,x5034)),f2(f2(x5034,x5033),f1(x5031,x5032)))), % 162.86/163.17 inference(scs_inference,[],[498,500,27])). % 162.86/163.17 cnf(506,plain, % 162.86/163.17 (E(f2(f2(x5061,x5062),f1(x5063,x5064)),f2(f1(x5064,x5063),f2(x5061,x5062)))), % 162.86/163.17 inference(scs_inference,[],[496,472,498,500,27,3])). % 162.86/163.17 cnf(507,plain, % 162.86/163.17 (E(f2(f2(x5071,x5072),f1(x5073,x5074)),f2(f1(x5074,x5073),f2(x5072,x5071)))), % 162.86/163.17 inference(rename_variables,[],[496])). % 162.86/163.17 cnf(513,plain, % 162.86/163.17 (E(f2(f2(x5131,x5132),f1(x5133,x5134)),f2(f1(x5133,x5134),f2(x5132,x5131)))), % 162.86/163.17 inference(scs_inference,[],[496,507,472,498,500,72,286,27,3,15,14,2])). % 162.86/163.17 cnf(515,plain, % 162.86/163.17 (E(f2(f1(x5151,x5152),f2(x5153,x5154)),f2(f2(x5153,x5154),f1(x5152,x5151)))), % 162.86/163.17 inference(scs_inference,[],[506,2])). % 162.86/163.17 cnf(516,plain, % 162.86/163.17 (E(f2(f1(x5161,x5162),f2(x5163,x5164)),f2(f1(x5162,x5161),f2(x5164,x5163)))), % 162.86/163.17 inference(scs_inference,[],[506,503,2,3])). % 162.86/163.17 cnf(525,plain, % 162.86/163.17 (E(f2(f2(x5251,x5252),f1(x5253,x5254)),f2(f2(x5252,x5251),f1(x5254,x5253)))), % 162.86/163.17 inference(scs_inference,[],[513,515,3])). % 162.86/163.17 cnf(543,plain, % 162.86/163.17 (P1(f2(f2(x5431,x5432),x5433),f2(x5433,f2(x5432,x5431)))), % 162.86/163.17 inference(scs_inference,[],[472,72,14])). % 162.86/163.17 cnf(544,plain, % 162.86/163.17 (P1(f2(x5441,x5442),f2(x5442,x5441))), % 162.86/163.17 inference(rename_variables,[],[72])). % 162.86/163.17 cnf(545,plain, % 162.86/163.17 (P1(f2(x5451,f2(x5452,x5453)),f2(f2(x5453,x5452),x5451))), % 162.86/163.17 inference(scs_inference,[],[472,72,544,14,15])). % 162.86/163.17 cnf(558,plain, % 162.86/163.17 (~E(f1(f3(a4,a7),f3(a7,a4)),f3(f1(a4,a7),f2(f2(f1(a4,a7),f2(a4,a7)),f1(a4,a7))))), % 162.86/163.17 inference(scs_inference,[],[24,217,2,3])). % 162.86/163.17 cnf(566,plain, % 162.86/163.17 (E(f1(x5661,f3(x5662,x5663)),f1(x5661,f3(x5662,f2(x5663,x5662))))), % 162.86/163.17 inference(scs_inference,[],[228,2,5])). % 162.86/163.17 cnf(569,plain, % 162.86/163.17 (E(f2(x5691,f3(x5692,f2(x5693,x5692))),f2(x5691,f3(x5692,x5693)))), % 162.86/163.17 inference(scs_inference,[],[238,2,9])). % 162.86/163.17 cnf(572,plain, % 162.86/163.17 (P1(f2(f2(x5721,x5722),f2(x5723,x5724)),f2(f2(x5724,x5723),f2(x5722,x5721)))), % 162.86/163.17 inference(scs_inference,[],[472,545,14])). % 162.86/163.17 cnf(577,plain, % 162.86/163.17 (E(f1(x5771,f3(x5772,f2(x5772,f2(x5773,x5772)))),f1(x5771,f3(x5772,x5773)))), % 162.86/163.17 inference(scs_inference,[],[253,2,5])). % 162.86/163.17 cnf(582,plain, % 162.86/163.17 (E(f2(x5821,f3(x5822,f2(f2(x5823,x5822),x5822))),f2(x5821,f3(x5822,x5823)))), % 162.86/163.17 inference(scs_inference,[],[272,2,9])). % 162.86/163.17 cnf(630,plain, % 162.86/163.17 (P1(f2(f2(x6301,x6302),x6303),f2(f2(x6302,x6301),x6303))), % 162.86/163.17 inference(scs_inference,[],[472,18,14])). % 162.86/163.17 cnf(648,plain, % 162.86/163.17 (E(f6(f3(x6481,f2(x6481,f2(x6482,x6481))),x6483),f6(f3(x6481,x6482),x6483))), % 162.86/163.17 inference(scs_inference,[],[253,2,6])). % 162.86/163.17 cnf(649,plain, % 162.86/163.17 (E(f5(f3(x6491,f2(f2(x6492,x6491),x6491)),x6493),f5(f3(x6491,x6492),x6493))), % 162.86/163.17 inference(scs_inference,[],[272,2,10])). % 162.86/163.17 cnf(653,plain, % 162.86/163.17 (E(f2(f3(x6531,f2(x6532,x6531)),x6533),f2(f3(x6531,x6532),x6533))), % 162.86/163.17 inference(scs_inference,[],[238,2,8])). % 162.86/163.17 cnf(656,plain, % 162.86/163.17 (E(f5(x6561,f1(x6562,x6563)),f5(x6561,f1(x6563,x6562)))), % 162.86/163.17 inference(scs_inference,[],[19,2,11])). % 162.86/163.17 cnf(657,plain, % 162.86/163.17 (E(f2(x6571,f2(x6572,x6573)),f2(x6571,f2(x6573,x6572)))), % 162.86/163.17 inference(scs_inference,[],[20,2,9])). % 162.86/163.17 cnf(660,plain, % 162.86/163.17 (E(f2(x6601,x6602),f2(x6602,x6601))), % 162.86/163.17 inference(rename_variables,[],[20])). % 162.86/163.17 cnf(661,plain, % 162.86/163.17 (P1(f2(f2(x6611,x6612),f2(x6613,x6614)),f2(f2(x6612,x6611),f2(x6614,x6613)))), % 162.86/163.17 inference(scs_inference,[],[20,660,543,572,14,15])). % 162.86/163.17 cnf(666,plain, % 162.86/163.17 (E(f3(x6661,f3(x6662,f2(x6662,x6663))),f3(x6661,f3(x6662,x6663)))), % 162.86/163.17 inference(scs_inference,[],[43,2,13])). % 162.86/163.17 cnf(675,plain, % 162.86/163.17 (P1(f3(f1(x6751,x6752),f2(f2(f1(x6752,x6751),x6753),f1(x6752,x6751))),f3(f1(x6752,x6751),x6753))), % 162.86/163.17 inference(scs_inference,[],[61,220,2,14])). % 162.86/163.17 cnf(687,plain, % 162.86/163.17 (~P2(x6871,f1(f2(x6872,x6873),f1(x6874,x6875)))+P2(x6871,f1(f1(x6875,x6874),f2(x6872,x6873)))), % 162.86/163.17 inference(scs_inference,[],[332,26,29])). % 162.86/163.17 cnf(688,plain, % 162.86/163.17 (~P2(x6881,f1(f2(x6882,x6883),f1(x6884,x6885)))+P2(x6881,f1(x6886,f1(f1(x6885,x6884),f2(x6882,x6883))))), % 162.86/163.17 inference(scs_inference,[],[687,30])). % 162.86/163.17 cnf(713,plain, % 162.86/163.17 (~P2(x7131,f2(x7132,f1(x7133,x7134)))+P2(x7131,f2(x7132,f1(x7134,x7133)))), % 162.86/163.17 inference(scs_inference,[],[288,26,29])). % 162.86/163.17 cnf(718,plain, % 162.86/163.17 (~P2(x7181,f3(f2(x7182,x7183),x7184))+P2(x7181,f3(f2(x7183,x7182),x7184))), % 162.86/163.17 inference(scs_inference,[],[300,26,29])). % 162.86/163.17 cnf(723,plain, % 162.86/163.17 (~P2(x7231,f2(f2(x7232,x7233),f1(x7234,x7235)))+P2(x7231,f2(f2(x7233,x7232),f1(x7235,x7234)))), % 162.86/163.17 inference(scs_inference,[],[525,26,29])). % 162.86/163.17 cnf(732,plain, % 162.86/163.18 (~P2(x7321,f2(x7322,f2(x7323,x7324)))+P2(x7321,f2(x7322,f2(x7324,x7323)))), % 162.86/163.18 inference(scs_inference,[],[657,26,29])). % 162.86/163.18 cnf(736,plain, % 162.86/163.18 (P1(f3(x7361,x7362),f3(x7361,f2(x7361,f2(f2(f2(x7361,x7362),x7361),x7361))))), % 162.86/163.18 inference(scs_inference,[],[227,253,26,15])). % 162.86/163.18 cnf(738,plain, % 162.86/163.18 (P1(f3(x7381,f2(f2(x7381,f2(x7381,f2(x7382,x7381))),x7381)),f3(x7381,x7382))), % 162.86/163.18 inference(scs_inference,[],[217,255,26,15])). % 162.86/163.18 cnf(747,plain, % 162.86/163.18 (~P2(x7471,f2(f1(x7472,x7473),f2(x7474,x7475)))+P2(x7471,f2(f2(x7475,x7474),f1(x7473,x7472)))), % 162.86/163.18 inference(scs_inference,[],[494,26,29])). % 162.86/163.18 cnf(757,plain, % 162.86/163.18 (~P2(x7571,f1(f1(x7572,x7573),f2(x7574,x7575)))+P2(x7571,f1(f1(x7573,x7572),f2(x7575,x7574)))), % 162.86/163.18 inference(scs_inference,[],[360,26,29])). % 162.86/163.18 cnf(758,plain, % 162.86/163.18 (~P2(x7581,f1(f1(x7582,x7583),f2(x7584,x7585)))+P2(x7581,f1(x7586,f1(f1(x7583,x7582),f2(x7585,x7584))))), % 162.86/163.18 inference(scs_inference,[],[757,30])). % 162.86/163.18 cnf(759,plain, % 162.86/163.18 (P2(x7591,f1(x7592,f1(f1(x7593,x7594),f2(x7595,x7596))))+~P2(x7591,f1(x7594,x7593))), % 162.86/163.18 inference(scs_inference,[],[758,31])). % 162.86/163.18 cnf(760,plain, % 162.86/163.18 (P2(f5(f1(x7601,x7602),x7603),f1(x7604,f1(f1(x7602,x7601),f2(x7605,x7606))))+P1(f1(x7601,x7602),x7603)), % 162.86/163.18 inference(scs_inference,[],[759,28])). % 162.86/163.18 cnf(789,plain, % 162.86/163.18 (P1(f1(f3(x7891,x7892),x7893),f1(f3(x7891,f2(x7891,x7892)),x7893))), % 162.86/163.18 inference(scs_inference,[],[43,26,4])). % 162.86/163.18 cnf(790,plain, % 162.86/163.18 (~P2(x7901,f2(f1(x7902,x7903),f2(x7904,x7905)))+P2(x7901,f2(f1(x7903,x7902),f2(x7905,x7904)))), % 162.86/163.18 inference(scs_inference,[],[516,26,29])). % 162.86/163.18 cnf(795,plain, % 162.86/163.18 (~P2(x7951,f3(f1(x7952,x7953),x7954))+P2(x7951,f1(f3(x7953,x7954),f3(x7952,x7954)))), % 162.86/163.18 inference(scs_inference,[],[55,26,29])). % 162.86/163.18 cnf(800,plain, % 162.86/163.18 (~P2(x8001,f3(x8002,x8003))+P2(x8001,f3(x8002,f2(f2(x8003,x8002),x8002)))), % 162.86/163.18 inference(scs_inference,[],[272,26,29])). % 162.86/163.18 cnf(802,plain, % 162.86/163.18 (~P2(x8021,f3(x8022,f2(f2(x8022,x8023),x8022)))+P2(x8021,f3(x8022,x8023))), % 162.86/163.18 inference(scs_inference,[],[217,26,29])). % 162.86/163.18 cnf(805,plain, % 162.86/163.18 (P1(f1(f3(x8051,f2(x8051,f2(x8052,x8051))),x8053),f1(f3(x8051,x8052),x8053))), % 162.86/163.18 inference(scs_inference,[],[255,26,4])). % 162.86/163.18 cnf(806,plain, % 162.86/163.18 (~P2(x8061,f1(x8062,f1(x8063,x8064)))+P2(x8061,f1(x8062,f1(x8064,x8063)))), % 162.86/163.18 inference(scs_inference,[],[125,26,29])). % 162.86/163.18 cnf(807,plain, % 162.86/163.18 (~P2(x8071,f1(x8072,f1(x8073,x8074)))+P2(x8071,f1(x8075,f1(x8072,f1(x8074,x8073))))), % 162.86/163.18 inference(scs_inference,[],[806,30])). % 162.86/163.18 cnf(811,plain, % 162.86/163.18 (~P2(x8111,f3(x8112,f2(x8113,x8112)))+P2(x8111,f3(x8112,x8113))), % 162.86/163.18 inference(scs_inference,[],[228,26,29])). % 162.86/163.18 cnf(815,plain, % 162.86/163.18 (~P2(x8151,f3(x8152,f2(x8153,x8154)))+P2(x8151,f3(x8152,f2(x8154,x8153)))), % 162.86/163.18 inference(scs_inference,[],[181,26,29])). % 162.86/163.18 cnf(816,plain, % 162.86/163.18 (~P2(x8161,f3(x8162,f2(x8163,x8164)))+P2(x8161,f1(x8165,f3(x8162,f2(x8164,x8163))))), % 162.86/163.18 inference(scs_inference,[],[815,30])). % 162.86/163.18 cnf(817,plain, % 162.86/163.18 (P2(x8171,f1(x8172,f3(x8173,f2(x8174,x8175))))+~P2(x8171,f3(f3(x8173,f2(x8175,x8174)),x8176))), % 162.86/163.18 inference(scs_inference,[],[816,33])). % 162.86/163.18 cnf(820,plain, % 162.86/163.18 (~P2(x8201,f3(x8202,x8203))+P2(x8201,f3(x8202,f2(f2(x8202,x8203),x8202)))), % 162.86/163.18 inference(scs_inference,[],[227,26,29])). % 162.86/163.18 cnf(821,plain, % 162.86/163.18 (~P2(x8211,f3(x8212,x8213))+P2(x8211,f1(x8214,f3(x8212,f2(f2(x8212,x8213),x8212))))), % 162.86/163.18 inference(scs_inference,[],[820,30])). % 162.86/163.18 cnf(828,plain, % 162.86/163.18 (P1(f3(x8281,f2(x8281,f2(f2(f2(x8281,x8282),x8281),x8281))),f3(x8281,x8282))), % 162.86/163.18 inference(scs_inference,[],[255,217,26,15])). % 162.86/163.18 cnf(831,plain, % 162.86/163.18 (P1(f3(x8311,f2(f2(f2(x8312,x8311),x8311),x8311)),f3(x8311,x8312))), % 162.86/163.18 inference(scs_inference,[],[269,228,26,15])). % 162.86/163.18 cnf(832,plain, % 162.86/163.18 (P1(f3(x8321,x8322),f3(x8321,f2(f2(x8321,f2(f2(x8322,x8321),x8321)),x8321)))), % 162.86/163.18 inference(scs_inference,[],[272,227,26,15])). % 162.86/163.18 cnf(833,plain, % 162.86/163.18 (~P2(x8331,f2(f1(x8332,x8333),x8334))+P2(x8331,f2(f1(x8333,x8332),x8334))), % 162.86/163.18 inference(scs_inference,[],[283,26,29])). % 162.86/163.18 cnf(845,plain, % 162.86/163.18 (~P2(x8451,f1(x8452,f2(x8453,x8454)))+P2(x8451,f1(x8452,f2(x8454,x8453)))), % 162.86/163.18 inference(scs_inference,[],[314,26,29])). % 162.86/163.18 cnf(846,plain, % 162.86/163.18 (~P2(x8461,f1(x8462,f2(x8463,x8464)))+P2(x8461,f1(x8465,f1(x8462,f2(x8464,x8463))))), % 162.86/163.18 inference(scs_inference,[],[845,30])). % 162.86/163.18 cnf(850,plain, % 162.86/163.18 (~P2(x8501,f1(f1(x8502,x8503),f2(x8504,x8505)))+P2(x8501,f1(f2(x8505,x8504),f1(x8503,x8502)))), % 162.86/163.18 inference(scs_inference,[],[334,26,29])). % 162.86/163.18 cnf(851,plain, % 162.86/163.18 (~P2(x8511,f1(f1(x8512,x8513),f2(x8514,x8515)))+P2(x8511,f1(x8516,f1(f2(x8515,x8514),f1(x8513,x8512))))), % 162.86/163.18 inference(scs_inference,[],[850,30])). % 162.86/163.18 cnf(858,plain, % 162.86/163.18 (~P2(x8581,f2(f2(x8582,x8583),x8584))+P2(x8581,f2(f2(x8583,x8582),x8584))), % 162.86/163.18 inference(scs_inference,[],[472,26,29])). % 162.86/163.18 cnf(863,plain, % 162.86/163.18 (~P2(x8631,f2(f2(x8632,x8633),f1(x8634,x8635)))+P2(x8631,f2(f1(x8635,x8634),f2(x8633,x8632)))), % 162.86/163.18 inference(scs_inference,[],[496,26,29])). % 162.86/163.18 cnf(886,plain, % 162.86/163.18 (~P2(x8861,f1(f2(x8862,x8863),f1(x8864,x8865)))+P2(x8861,f1(f1(x8865,x8864),f2(x8863,x8862)))), % 162.86/163.18 inference(scs_inference,[],[330,26,29])). % 162.86/163.18 cnf(887,plain, % 162.86/163.18 (~P2(x8871,f1(f2(x8872,x8873),f1(x8874,x8875)))+P2(x8871,f1(x8876,f1(f1(x8875,x8874),f2(x8873,x8872))))), % 162.86/163.18 inference(scs_inference,[],[886,30])). % 162.86/163.18 cnf(895,plain, % 162.86/163.18 (~P2(x8951,f1(x8952,x8953))+P2(x8951,f1(x8953,x8952))), % 162.86/163.18 inference(scs_inference,[],[19,26,29])). % 162.86/163.18 cnf(896,plain, % 162.86/163.18 (~P2(x8961,f1(x8962,x8963))+P2(x8961,f1(x8964,f1(x8963,x8962)))), % 162.86/163.18 inference(scs_inference,[],[895,30])). % 162.86/163.18 cnf(901,plain, % 162.86/163.18 (~P2(x9011,f3(f1(x9012,x9013),x9014))+P2(x9011,f1(f3(x9012,x9014),f3(x9013,x9014)))), % 162.86/163.18 inference(scs_inference,[],[48,26,29])). % 162.86/163.18 cnf(907,plain, % 162.86/163.18 (~P2(x9071,f3(f1(x9072,x9073),x9074))+P2(x9071,f3(f1(x9073,x9072),x9074))), % 162.86/163.18 inference(scs_inference,[],[61,26,29])). % 162.86/163.18 cnf(913,plain, % 162.86/163.18 (P1(f3(x9131,f2(x9131,f2(x9131,f2(f2(x9131,x9132),x9131)))),f3(x9131,x9132))), % 162.86/163.18 inference(scs_inference,[],[80,217,26,15])). % 162.86/163.18 cnf(915,plain, % 162.86/163.18 (~P2(x9151,f3(x9152,f1(x9153,x9154)))+P2(x9151,f3(x9152,f1(x9154,x9153)))), % 162.86/163.18 inference(scs_inference,[],[121,26,29])). % 162.86/163.18 cnf(916,plain, % 162.86/163.18 (~P2(x9161,f3(x9162,f1(x9163,x9164)))+P2(x9161,f1(x9165,f3(x9162,f1(x9164,x9163))))), % 162.86/163.18 inference(scs_inference,[],[915,30])). % 162.86/163.18 cnf(917,plain, % 162.86/163.18 (P2(x9171,f1(x9172,f3(x9173,f1(x9174,x9175))))+~P2(x9171,f3(f3(x9173,f1(x9175,x9174)),x9176))), % 162.86/163.18 inference(scs_inference,[],[916,33])). % 162.86/163.18 cnf(920,plain, % 162.86/163.18 (P1(f1(f3(x9201,f2(x9202,x9201)),x9203),f1(f3(x9201,x9202),x9203))), % 162.86/163.18 inference(scs_inference,[],[228,26,4])). % 162.86/163.18 cnf(921,plain, % 162.86/163.18 (P1(f3(x9211,x9212),f3(x9211,f2(f2(x9211,f2(x9212,x9211)),x9211)))), % 162.86/163.18 inference(scs_inference,[],[238,227,26,15])). % 162.86/163.18 cnf(933,plain, % 162.86/163.18 (P1(f3(x9331,f2(f2(x9331,f2(x9332,x9331)),x9331)),f3(x9331,x9332))), % 162.86/163.18 inference(scs_inference,[],[228,255,26,15])). % 162.86/163.18 cnf(936,plain, % 162.86/163.18 (P1(f5(f3(x9361,x9362),x9363),f5(f3(x9361,f2(x9362,x9361)),x9363))), % 162.86/163.18 inference(scs_inference,[],[238,26,10])). % 162.86/163.18 cnf(945,plain, % 162.86/163.18 (P1(f3(x9451,x9452),f3(x9451,f2(x9451,f2(x9451,f2(f2(x9452,x9451),x9451)))))), % 162.86/163.18 inference(scs_inference,[],[272,82,26,15])). % 162.86/163.18 cnf(975,plain, % 162.86/163.18 (P1(f1(f3(x9751,f1(x9752,x9753)),f3(x9754,f1(x9752,x9753))),f3(f1(x9754,x9751),f1(x9753,x9752)))), % 162.86/163.18 inference(scs_inference,[],[53,121,26,15])). % 162.86/163.18 cnf(997,plain, % 162.86/163.18 (P1(f3(x9971,f2(f2(x9971,f2(f2(x9972,x9971),x9971)),x9971)),f3(x9971,x9972))), % 162.86/163.18 inference(scs_inference,[],[217,269,26,15])). % 162.86/163.18 cnf(999,plain, % 162.86/163.18 (P1(f3(f1(x9991,x9992),x9993),f1(f3(x9991,f2(x9993,f1(x9991,x9992))),f3(x9992,f2(x9993,f1(x9991,x9992)))))), % 162.86/163.18 inference(scs_inference,[],[238,48,26,15])). % 162.86/163.18 cnf(1038,plain, % 162.86/163.18 (P1(f3(f3(x10381,f2(f2(x10381,x10382),x10381)),x10383),f3(f3(x10381,x10382),x10383))), % 162.86/163.18 inference(scs_inference,[],[217,26,12])). % 162.86/163.18 cnf(1041,plain, % 162.86/163.18 (P1(f6(x10411,f3(x10412,f2(x10412,f2(x10413,x10412)))),f6(x10411,f3(x10412,x10413)))), % 162.86/163.18 inference(scs_inference,[],[255,26,7])). % 162.86/163.18 cnf(1042,plain, % 162.86/163.18 (P1(f2(f3(x10421,f2(f2(x10422,x10421),x10421)),x10423),f2(f3(x10421,x10422),x10423))), % 162.86/163.18 inference(scs_inference,[],[269,26,8])). % 162.86/163.18 cnf(1044,plain, % 162.86/163.18 (P1(f5(x10441,f3(x10442,x10443)),f5(x10441,f3(x10442,f2(x10443,x10442))))), % 162.86/163.18 inference(scs_inference,[],[238,26,11])). % 162.86/163.18 cnf(1060,plain, % 162.86/163.18 (P1(f6(f3(x10601,x10602),x10603),f6(f3(x10601,f2(x10602,x10601)),x10603))), % 162.86/163.18 inference(scs_inference,[],[238,26,6])). % 162.86/163.18 cnf(1068,plain, % 162.86/163.18 (P1(f3(x10681,f3(x10682,f2(f2(x10683,x10682),x10682))),f3(x10681,f3(x10682,x10683)))), % 162.86/163.18 inference(scs_inference,[],[269,26,13])). % 162.86/163.18 cnf(1086,plain, % 162.86/163.18 (P1(f3(f1(x10861,x10862),x10863),f1(f3(x10861,f2(f1(x10861,x10862),x10863)),f3(x10862,f2(f1(x10861,x10862),x10863))))), % 162.86/163.18 inference(scs_inference,[],[43,48,26,15])). % 162.86/163.18 cnf(1117,plain, % 162.86/163.18 (P1(f3(x11171,x11172),f3(x11171,f2(f2(x11171,f2(x11171,f2(x11171,x11172))),x11171)))), % 162.86/163.18 inference(scs_inference,[],[82,227,26,15])). % 162.86/163.18 cnf(1127,plain, % 162.86/163.18 (P1(f6(f3(x11271,f2(f2(x11272,x11271),x11271)),x11273),f6(f3(x11271,x11272),x11273))), % 162.86/163.18 inference(scs_inference,[],[269,26,6])). % 162.86/163.18 cnf(1128,plain, % 162.86/163.18 (P1(f3(x11281,f3(x11282,f2(x11283,x11282))),f3(x11281,f3(x11282,x11283)))), % 162.86/163.18 inference(scs_inference,[],[228,26,13])). % 162.86/163.18 cnf(1161,plain, % 162.86/163.18 (P1(f6(f3(x11611,f2(x11611,f2(x11611,x11612))),x11613),f6(f3(x11611,x11612),x11613))), % 162.86/163.18 inference(scs_inference,[],[80,26,6])). % 162.86/163.18 cnf(1167,plain, % 162.86/163.18 (P1(f6(x11671,f3(x11672,x11673)),f6(x11671,f3(x11672,f2(x11672,f2(x11673,x11672)))))), % 162.86/163.18 inference(scs_inference,[],[253,26,7])). % 162.86/163.18 cnf(1173,plain, % 162.86/163.18 (P1(f3(x11731,f3(x11732,x11733)),f3(x11731,f3(x11732,f2(x11732,x11733))))), % 162.86/163.18 inference(scs_inference,[],[43,26,13])). % 162.86/163.18 cnf(1186,plain, % 162.86/163.18 (P1(f2(x11861,f3(x11862,x11863)),f2(x11861,f3(x11862,f2(x11863,x11862))))), % 162.86/163.18 inference(scs_inference,[],[238,26,9])). % 162.86/163.18 cnf(1191,plain, % 162.86/163.18 (P1(f6(f3(x11911,f2(x11911,f2(x11912,x11911))),x11913),f6(f3(x11911,x11912),x11913))), % 162.86/163.18 inference(scs_inference,[],[255,26,6])). % 162.86/163.18 cnf(1215,plain, % 162.86/163.18 (P1(x12151,x12152)+P2(f5(x12151,x12152),f1(x12153,x12151))), % 162.86/163.18 inference(scs_inference,[],[28,30])). % 162.86/163.18 cnf(1216,plain, % 162.86/163.18 (P1(x12161,x12162)+P2(f5(x12161,x12162),f1(f1(x12163,x12161),x12164))), % 162.86/163.18 inference(scs_inference,[],[1215,31])). % 162.86/163.18 cnf(1217,plain, % 162.86/163.18 (P1(x12171,f1(f1(x12172,x12171),x12173))), % 162.86/163.18 inference(scs_inference,[],[1216,36])). % 162.86/163.18 cnf(1218,plain, % 162.86/163.18 (P1(x12181,f1(f2(x12182,x12183),f1(x12181,x12184)))), % 162.86/163.18 inference(scs_inference,[],[334,1217,15])). % 162.86/163.18 cnf(1225,plain, % 162.86/163.18 (P1(x12251,f1(f1(x12251,x12252),f2(x12253,x12254)))), % 162.86/163.18 inference(scs_inference,[],[341,1218,15])). % 162.86/163.18 cnf(1260,plain, % 162.86/163.18 (P1(x12601,x12602)+P2(f5(x12601,x12602),f1(x12601,x12603))), % 162.86/163.18 inference(scs_inference,[],[28,31])). % 162.86/163.18 cnf(1261,plain, % 162.86/163.18 (P1(x12611,x12612)+P2(f5(x12611,x12612),f1(x12613,f1(x12611,x12614)))), % 162.86/163.18 inference(scs_inference,[],[1260,30])). % 162.99/163.18 cnf(1262,plain, % 162.99/163.18 (P1(x12621,f1(x12622,f1(x12621,x12623)))), % 162.99/163.18 inference(scs_inference,[],[1261,36])). % 162.99/163.18 cnf(1273,plain, % 162.99/163.18 (P1(f3(x12731,x12732),x12733)+P2(f5(f3(x12731,x12732),x12733),x12731)), % 162.99/163.18 inference(scs_inference,[],[28,33])). % 162.99/163.18 cnf(1274,plain, % 162.99/163.18 (P1(f3(x12741,x12742),x12743)+P2(f5(f3(x12741,x12742),x12743),f1(x12744,x12741))), % 162.99/163.18 inference(scs_inference,[],[1273,30])). % 162.99/163.18 cnf(1275,plain, % 162.99/163.18 (P1(f3(x12751,x12752),x12753)+P2(f5(f3(x12751,x12752),x12753),f1(f1(x12754,x12751),x12755))), % 162.99/163.18 inference(scs_inference,[],[1274,31])). % 162.99/163.18 cnf(1276,plain, % 162.99/163.18 (P1(f3(x12761,x12762),f1(f1(x12763,x12761),x12764))), % 162.99/163.18 inference(scs_inference,[],[1275,36])). % 162.99/163.18 cnf(1277,plain, % 162.99/163.18 (P1(f3(x12771,x12772),f1(f2(x12773,x12774),f1(x12771,x12775)))), % 162.99/163.18 inference(scs_inference,[],[334,1276,15])). % 162.99/163.18 cnf(1287,plain, % 162.99/163.18 (P1(f3(x12871,x12872),f1(f1(x12871,x12873),f2(x12874,x12875)))), % 162.99/163.18 inference(scs_inference,[],[341,1277,15])). % 162.99/163.18 cnf(1288,plain, % 162.99/163.18 (P1(f3(x12881,x12882),f1(f2(x12883,x12884),f1(x12881,x12885)))), % 162.99/163.18 inference(rename_variables,[],[1277])). % 162.99/163.18 cnf(1291,plain, % 162.99/163.18 (P1(f1(f3(x12911,x12912),f3(x12913,x12912)),f1(f1(f1(x12911,x12913),x12914),f2(x12915,x12916)))), % 162.99/163.18 inference(scs_inference,[],[341,48,1277,1288,15,27,14])). % 162.99/163.18 cnf(1295,plain, % 162.99/163.18 (P1(f3(f1(x12951,x12952),x12953),f1(f1(f1(x12952,x12951),x12954),f2(x12955,x12956)))), % 162.99/163.18 inference(scs_inference,[],[53,1291,14])). % 162.99/163.18 cnf(1304,plain, % 162.99/163.18 (P1(f1(f3(x13041,x13042),f3(x13043,x13042)),f1(f1(f1(x13043,x13041),x13044),f2(x13045,x13046)))), % 162.99/163.18 inference(scs_inference,[],[48,1295,14])). % 162.99/163.18 cnf(1340,plain, % 162.99/163.18 (P1(f1(x13401,x13402),f1(f1(x13403,f1(x13402,x13401)),x13404))), % 162.99/163.18 inference(scs_inference,[],[19,1217,14])). % 162.99/163.18 cnf(1341,plain, % 162.99/163.18 (P1(x13411,f1(f1(x13412,x13411),x13413))), % 162.99/163.18 inference(rename_variables,[],[1217])). % 162.99/163.18 cnf(1342,plain, % 162.99/163.18 (P1(x13421,f1(x13422,f1(x13423,x13421)))), % 162.99/163.18 inference(scs_inference,[],[19,1217,1341,14,15])). % 162.99/163.18 cnf(1353,plain, % 162.99/163.18 (P1(x13531,f1(f1(x13531,x13532),x13533))), % 162.99/163.18 inference(scs_inference,[],[19,1225,1262,14,15])). % 162.99/163.18 cnf(1363,plain, % 162.99/163.18 (P1(f3(x13631,x13632),f1(x13633,f1(x13634,x13631)))), % 162.99/163.18 inference(scs_inference,[],[19,1262,1276,14,15])). % 162.99/163.18 cnf(1471,plain, % 162.99/163.18 (P1(f3(x14711,x14712),f1(x14713,f1(x14711,x14714)))), % 162.99/163.18 inference(scs_inference,[],[125,1363,15])). % 162.99/163.18 cnf(1497,plain, % 162.99/163.18 (P1(f3(f2(x14971,x14972),x14973),f1(f1(f2(x14972,x14971),x14974),f2(x14975,x14976)))), % 162.99/163.18 inference(scs_inference,[],[300,1287,14])). % 162.99/163.18 cnf(1504,plain, % 162.99/163.18 (P1(f3(f1(x15041,x15042),x15043),f1(f1(x15044,f1(x15042,x15041)),f2(x15045,x15046)))), % 162.99/163.18 inference(scs_inference,[],[344,1295,15])). % 162.99/163.18 cnf(1515,plain, % 162.99/163.18 (P1(f1(f3(x15151,x15152),f3(x15153,x15152)),f1(f1(x15154,f1(x15151,x15153)),f2(x15155,x15156)))), % 162.99/163.18 inference(scs_inference,[],[344,48,1291,1504,14,15])). % 162.99/163.18 cnf(1523,plain, % 162.99/163.18 (P1(f3(f2(x15231,x15232),x15233),f1(f1(x15234,f2(x15232,x15231)),f2(x15235,x15236)))), % 162.99/163.18 inference(scs_inference,[],[344,1497,15])). % 162.99/163.18 cnf(1578,plain, % 162.99/163.18 (P1(f2(x15781,x15782),x15783)+P2(f5(f2(x15781,x15782),x15783),x15782)), % 162.99/163.18 inference(scs_inference,[],[28,34])). % 162.99/163.18 cnf(1579,plain, % 162.99/163.18 (P1(f2(x15791,x15792),x15793)+P2(f5(f2(x15791,x15792),x15793),f1(x15794,x15792))), % 162.99/163.18 inference(scs_inference,[],[1578,30])). % 162.99/163.18 cnf(1580,plain, % 162.99/163.18 (P1(f3(x15801,x15802),f1(f1(x15801,x15803),x15804))), % 162.99/163.18 inference(scs_inference,[],[19,1471,15])). % 162.99/163.18 cnf(1589,plain, % 162.99/163.18 (P1(f2(x15891,x15892),x15893)+P2(f5(f2(x15891,x15892),x15893),f1(f1(x15894,x15892),x15895))), % 162.99/163.18 inference(scs_inference,[],[1579,31])). % 162.99/163.18 cnf(1590,plain, % 162.99/163.18 (P1(f2(x15901,x15902),f1(f1(x15903,x15902),x15904))), % 162.99/163.18 inference(scs_inference,[],[1589,36])). % 162.99/163.18 cnf(1591,plain, % 162.99/163.18 (P1(f2(x15911,x15912),f1(f1(x15913,x15911),x15914))), % 162.99/163.18 inference(scs_inference,[],[20,1590,14])). % 162.99/163.18 cnf(1592,plain, % 162.99/163.18 (P1(f2(x15921,x15922),f1(f1(x15923,x15922),x15924))), % 162.99/163.18 inference(rename_variables,[],[1590])). % 162.99/163.18 cnf(1593,plain, % 162.99/163.18 (P1(f2(x15931,x15932),f1(f2(x15933,x15934),f1(x15932,x15935)))), % 162.99/163.18 inference(scs_inference,[],[20,336,1590,1592,14,15])). % 162.99/163.18 cnf(1602,plain, % 162.99/163.18 (P1(f2(x16021,x16022),f1(f2(x16023,x16024),f1(x16022,x16025)))), % 162.99/163.18 inference(rename_variables,[],[1593])). % 162.99/163.18 cnf(1603,plain, % 162.99/163.18 (P1(f2(x16031,x16032),f1(f1(x16032,x16033),f2(x16034,x16035)))), % 162.99/163.18 inference(scs_inference,[],[20,341,1593,1602,14,15])). % 162.99/163.18 cnf(1610,plain, % 162.99/163.18 (P1(f2(x16101,x16102),f1(f1(x16101,x16103),f2(x16104,x16105)))), % 162.99/163.18 inference(scs_inference,[],[20,1603,14])). % 162.99/163.18 cnf(1704,plain, % 162.99/163.18 (P1(f2(f1(x17041,x17042),x17043),f1(f1(f1(x17042,x17041),x17044),f2(x17045,x17046)))), % 162.99/163.18 inference(scs_inference,[],[283,1610,14])). % 162.99/163.18 cnf(1714,plain, % 162.99/163.18 (P1(f2(x17141,f1(x17142,x17143)),f1(f1(f1(x17143,x17142),x17144),f2(x17145,x17146)))), % 162.99/163.18 inference(scs_inference,[],[288,1603,14])). % 162.99/163.18 cnf(1763,plain, % 162.99/163.18 (P1(f2(x17631,f1(x17632,x17633)),f1(f1(x17634,f1(x17633,x17632)),f2(x17635,x17636)))), % 162.99/163.18 inference(scs_inference,[],[344,1714,15])). % 162.99/163.18 cnf(1819,plain, % 162.99/163.18 (E(f1(f1(x18191,x18192),x18193),f1(f1(x18192,x18191),x18193))), % 162.99/163.18 inference(scs_inference,[],[19,4])). % 162.99/163.18 cnf(1821,plain, % 162.99/163.18 (~E(f1(f3(a7,a4),f3(a4,a7)),f3(f1(a4,a7),f2(a4,a7)))), % 162.99/163.18 inference(scs_inference,[],[44,19,20,4,7,2])). % 162.99/163.18 cnf(1822,plain, % 162.99/163.18 (~E(f3(f1(a4,a7),f2(a7,a4)),f1(f3(a7,a4),f3(a4,a7)))), % 162.99/163.18 inference(scs_inference,[],[44,181,19,20,4,7,2,3])). % 162.99/163.18 cnf(1839,plain, % 162.99/163.18 (~E(f3(f1(a7,a4),f2(a7,a4)),f1(f3(a7,a4),f3(a4,a7)))), % 162.99/163.18 inference(scs_inference,[],[1822,61,3])). % 162.99/163.18 cnf(1896,plain, % 162.99/163.18 (P2(x18961,f1(x18962,f1(x18963,x18964)))+~P2(x18961,f1(f1(x18964,x18963),x18962))), % 162.99/163.18 inference(scs_inference,[],[1819,17,895])). % 162.99/163.18 cnf(1898,plain, % 162.99/163.18 (P2(x18981,f1(f1(x18982,x18983),f1(x18984,x18985)))+~P2(x18981,f1(f1(x18983,x18982),f1(x18985,x18984)))), % 162.99/163.18 inference(scs_inference,[],[1819,17,895,806])). % 162.99/163.18 cnf(1952,plain, % 162.99/163.18 (~P2(x19521,f3(f1(x19522,x19523),f2(x19524,x19525)))+P2(x19521,f3(f1(x19523,x19522),f2(x19525,x19524)))), % 162.99/163.18 inference(scs_inference,[],[239,1839,27,29])). % 162.99/163.18 cnf(1954,plain, % 162.99/163.18 (~P2(x19541,f3(x19542,f2(x19542,x19543)))+P2(x19541,f3(x19542,x19543))), % 162.99/163.18 inference(scs_inference,[],[21,17])). % 162.99/163.18 cnf(1975,plain, % 162.99/163.18 (~P2(x19751,f2(x19752,x19753))+P2(x19751,f2(x19753,x19752))), % 162.99/163.18 inference(scs_inference,[],[20,17])). % 162.99/163.18 cnf(1976,plain, % 162.99/163.18 (~P2(f5(x19761,f1(x19762,x19763)),x19764)+P2(f5(x19761,f1(x19763,x19762)),x19764)), % 162.99/163.18 inference(scs_inference,[],[656,16])). % 162.99/163.18 cnf(1977,plain, % 162.99/163.18 (~P2(x19771,f3(f2(x19772,x19773),f1(x19774,x19775)))+P2(x19771,f3(f2(x19773,x19772),f1(x19775,x19774)))), % 162.99/163.18 inference(scs_inference,[],[428,29])). % 162.99/163.18 cnf(1980,plain, % 162.99/163.18 (~P2(x19801,f1(f3(x19802,x19803),f3(x19804,x19803)))+P2(x19801,f3(f1(x19802,x19804),x19803))), % 162.99/163.18 inference(scs_inference,[],[22,17])). % 162.99/163.18 cnf(1984,plain, % 162.99/163.18 (~P2(x19841,f3(f2(x19842,x19843),f2(x19844,x19845)))+P2(x19841,f3(f2(x19843,x19842),f2(x19845,x19844)))), % 162.99/163.18 inference(scs_inference,[],[431,29])). % 162.99/163.18 cnf(1992,plain, % 162.99/163.18 (~P2(x19921,f3(x19922,x19923))+P2(x19921,f3(x19922,f2(x19922,x19923)))), % 162.99/163.18 inference(scs_inference,[],[43,17])). % 162.99/163.18 cnf(2012,plain, % 162.99/163.18 (~P2(x20121,f3(x20122,x20123))+P2(x20121,f1(x20124,f3(x20122,f2(x20122,x20123))))), % 162.99/163.18 inference(scs_inference,[],[1992,30])). % 162.99/163.18 cnf(2013,plain, % 162.99/163.18 (~P2(f5(f1(x20131,x20132),x20133),x20134)+P2(f5(f1(x20132,x20131),x20133),x20134)), % 162.99/163.18 inference(scs_inference,[],[292,16])). % 162.99/163.18 cnf(2014,plain, % 162.99/163.18 (~P2(x20141,f2(f1(x20142,x20143),f1(x20144,x20145)))+P2(x20141,f2(f1(x20143,x20142),f1(x20145,x20144)))), % 162.99/163.18 inference(scs_inference,[],[301,29])). % 162.99/163.18 cnf(2016,plain, % 162.99/163.18 (~P2(x20161,f3(x20162,f2(x20162,f2(x20162,x20163))))+P2(x20161,f3(x20162,x20163))), % 162.99/163.18 inference(scs_inference,[],[80,17])). % 162.99/163.18 cnf(2082,plain, % 162.99/163.18 (~P2(x20821,f2(f2(x20822,x20823),f2(x20824,x20825)))+P2(x20821,f2(f2(x20823,x20822),f2(x20825,x20824)))), % 162.99/163.18 inference(scs_inference,[],[661,29])). % 162.99/163.18 cnf(2084,plain, % 162.99/163.18 (~P2(x20841,f3(x20842,f2(x20842,f2(x20843,x20842))))+P2(x20841,f3(x20842,x20843))), % 162.99/163.18 inference(scs_inference,[],[255,17])). % 162.99/163.18 cnf(2098,plain, % 162.99/163.18 (~P2(x20981,f3(x20982,f2(f2(x20983,x20982),x20982)))+P2(x20981,f3(x20982,x20983))), % 162.99/163.18 inference(scs_inference,[],[269,17])). % 162.99/163.18 cnf(2109,plain, % 162.99/163.18 (~P2(f5(x21091,f1(x21092,x21093)),f3(x21094,x21095))+P2(f5(x21091,f1(x21093,x21092)),x21094)), % 162.99/163.18 inference(scs_inference,[],[1976,33])). % 162.99/163.18 cnf(2112,plain, % 162.99/163.18 (~P2(x21121,f3(x21122,x21123))+P2(x21121,f3(x21122,f2(x21123,x21122)))), % 162.99/163.18 inference(scs_inference,[],[238,17])). % 162.99/163.18 cnf(2134,plain, % 162.99/163.18 (~P2(x21341,f1(f3(x21342,x21343),f3(x21344,x21343)))+P2(x21341,f3(f1(x21344,x21342),x21343))), % 162.99/163.18 inference(scs_inference,[],[53,17])). % 162.99/163.18 cnf(2137,plain, % 162.99/163.18 (~P2(f5(f1(x21371,x21372),x21373),f3(f2(x21374,x21375),x21376))+P2(f5(f1(x21372,x21371),x21373),x21375)), % 162.99/163.18 inference(scs_inference,[],[2013,71])). % 162.99/163.18 cnf(2257,plain, % 162.99/163.18 (~P2(f5(x22571,f1(x22572,x22573)),f3(f2(f1(x22573,x22572),x22574),x22575))+P1(x22571,f1(x22573,x22572))), % 162.99/163.18 inference(scs_inference,[],[2109,74])). % 162.99/163.18 cnf(2284,plain, % 162.99/163.18 (~P2(x22841,f1(f3(x22842,x22843),f3(x22844,x22843)))+P2(x22841,f1(x22844,x22842))), % 162.99/163.18 inference(scs_inference,[],[2134,33])). % 162.99/163.18 cnf(2316,plain, % 162.99/163.18 (~P2(x23161,f2(f1(x23162,x23163),f1(x23164,x23165)))+P2(x23161,f2(f1(x23165,x23164),f1(x23163,x23162)))), % 162.99/163.18 inference(scs_inference,[],[289,29])). % 162.99/163.18 cnf(2342,plain, % 162.99/163.18 (~P2(x23421,f2(f2(x23422,x23423),f2(x23424,x23425)))+P2(x23421,f2(f2(x23425,x23424),f2(x23423,x23422)))), % 162.99/163.18 inference(scs_inference,[],[572,29])). % 162.99/163.18 cnf(2366,plain, % 162.99/163.18 (~P2(x23661,f2(f2(x23662,x23663),x23664))+P2(x23661,f2(x23664,f2(x23663,x23662)))), % 162.99/163.18 inference(scs_inference,[],[543,29])). % 162.99/163.18 cnf(2379,plain, % 162.99/163.18 (~P2(f5(x23791,x23792),f2(f2(x23793,x23794),x23792))+P1(x23791,x23792)), % 162.99/163.18 inference(scs_inference,[],[2366,74])). % 162.99/163.18 cnf(2383,plain, % 162.99/163.18 (~P2(x23831,f2(x23832,f2(x23833,x23834)))+P2(x23831,f2(f2(x23834,x23833),x23832))), % 162.99/163.18 inference(scs_inference,[],[545,29])). % 162.99/163.18 cnf(2488,plain, % 162.99/163.18 (~P2(x24881,f1(x24882,x24883))+P2(x24881,f1(f1(f1(x24883,x24882),x24884),x24885))), % 162.99/163.18 inference(scs_inference,[],[1340,1819,29,17])). % 162.99/163.18 cnf(2494,plain, % 162.99/163.18 (~P2(x24941,f1(x24942,x24943))+P2(x24941,f1(x24944,f1(f1(x24945,f1(x24943,x24942)),f2(x24946,x24947))))), % 162.99/163.18 inference(scs_inference,[],[2488,758])). % 162.99/163.18 cnf(2525,plain, % 162.99/163.18 (~P2(x25251,f1(x25252,f1(x25253,x25254)))+P2(x25251,f1(f1(x25254,x25253),x25252))), % 162.99/163.18 inference(scs_inference,[],[154,29])). % 162.99/163.18 cnf(2656,plain, % 162.99/163.18 (~P2(x26561,f1(x26562,f2(x26563,x26564)))+P2(x26561,f1(f2(x26564,x26563),x26562))), % 162.99/163.18 inference(scs_inference,[],[325,29])). % 162.99/163.18 cnf(2671,plain, % 162.99/163.18 (~P2(x26711,f1(f1(x26712,x26713),f2(x26714,x26715)))+P2(x26711,f1(x26716,f1(f1(x26713,x26712),f2(x26714,x26715))))), % 162.99/163.18 inference(scs_inference,[],[2656,887])). % 162.99/163.18 cnf(2688,plain, % 162.99/163.18 (~P2(x26881,x26882)+P2(x26881,f1(x26883,f1(x26884,x26882)))), % 162.99/163.18 inference(scs_inference,[],[1342,29])). % 162.99/163.18 cnf(2690,plain, % 162.99/163.18 (~P2(x26901,x26902)+P2(x26901,f1(f1(x26902,x26903),f2(x26904,x26905)))), % 162.99/163.18 inference(scs_inference,[],[1342,332,29,17])). % 162.99/163.18 cnf(2704,plain, % 162.99/163.18 (~P2(x27041,x27042)+P2(x27041,f1(x27043,f1(f2(x27044,x27045),f1(x27046,x27042))))), % 162.99/163.18 inference(scs_inference,[],[2690,851])). % 162.99/163.18 cnf(2718,plain, % 162.99/163.18 (P2(x27181,f1(f1(f1(x27182,x27183),f2(x27184,x27185)),f2(x27186,x27187)))+~P2(x27181,x27183)), % 162.99/163.18 inference(scs_inference,[],[2704,886])). % 162.99/163.18 cnf(2722,plain, % 162.99/163.18 (~P2(x27221,f2(f1(x27222,x27223),x27224))+P2(x27221,f2(x27224,f1(x27223,x27222)))), % 162.99/163.18 inference(scs_inference,[],[284,29])). % 162.99/163.18 cnf(2731,plain, % 162.99/163.18 (~P2(x27311,f2(x27312,f1(x27313,x27314)))+P2(x27311,f2(f1(x27314,x27313),x27312))), % 162.99/163.18 inference(scs_inference,[],[286,29])). % 162.99/163.18 cnf(2756,plain, % 162.99/163.18 (~P2(x27561,x27562)+P2(x27561,f1(f1(x27562,x27563),x27564))), % 162.99/163.18 inference(scs_inference,[],[1353,29])). % 162.99/163.18 cnf(2770,plain, % 162.99/163.18 (~P2(x27701,x27702)+P2(x27701,f1(f1(x27703,x27702),x27704))), % 162.99/163.18 inference(scs_inference,[],[1217,29])). % 162.99/163.18 cnf(2827,plain, % 162.99/163.18 (~P2(f5(x28271,f2(x28272,x28273)),f2(f2(x28274,x28275),f2(x28273,x28272)))+P1(x28271,f2(x28272,x28273))), % 162.99/163.18 inference(scs_inference,[],[2342,74])). % 162.99/163.18 cnf(2852,plain, % 162.99/163.18 (P1(f2(f2(x28521,x28522),f2(x28523,x28524)),f2(x28524,x28523))), % 162.99/163.18 inference(scs_inference,[],[2827,28])). % 162.99/163.18 cnf(2853,plain, % 162.99/163.18 (~P2(x28531,f2(f2(x28532,x28533),f2(x28534,x28535)))+P2(x28531,f2(x28535,x28534))), % 162.99/163.18 inference(scs_inference,[],[2852,29])). % 162.99/163.18 cnf(2854,plain, % 162.99/163.18 (~P1(x28541,x28542)+P2(x28543,x28542)+~P2(x28543,x28541)), % 162.99/163.18 inference(rename_variables,[],[29])). % 162.99/163.18 cnf(2855,plain, % 162.99/163.18 (~P2(x28551,f2(f2(x28552,x28553),f2(x28554,f2(x28555,x28556))))+P2(x28551,f2(f2(x28556,x28555),x28554))), % 162.99/163.18 inference(scs_inference,[],[630,2852,29,2854])). % 162.99/163.18 cnf(2858,plain, % 162.99/163.18 (~P2(x28581,f2(f2(x28582,x28583),f2(f1(x28584,x28585),f2(x28586,x28587))))+P2(x28581,f2(f2(x28587,x28586),f1(x28585,x28584)))), % 162.99/163.18 inference(scs_inference,[],[630,2852,525,29,2854,17])). % 162.99/163.18 cnf(2862,plain, % 162.99/163.18 (P2(x28621,f2(f1(x28622,x28623),f2(x28624,x28625)))+~P2(x28621,f2(f2(x28626,x28627),f2(f1(x28623,x28622),f2(x28624,x28625))))), % 162.99/163.18 inference(scs_inference,[],[630,2852,525,29,2854,17,2366,2731])). % 162.99/163.18 cnf(2864,plain, % 162.99/163.18 (P2(x28641,f2(f2(x28642,x28643),f1(x28644,x28645)))+~P2(x28641,f2(f2(x28646,x28647),f2(f1(x28645,x28644),f2(x28642,x28643))))), % 162.99/163.18 inference(scs_inference,[],[630,2852,525,29,2854,17,2366,2731,723])). % 162.99/163.18 cnf(2937,plain, % 162.99/163.18 (E(f5(f6(f3(x29371,f2(x29371,x29372)),x29373),x29374),f5(f6(f3(x29371,x29372),x29373),x29374))), % 162.99/163.18 inference(scs_inference,[],[317,10])). % 162.99/163.18 cnf(2942,plain, % 162.99/163.18 (E(f3(x29421,f6(f3(x29422,f2(x29422,x29423)),x29424)),f3(x29421,f6(f3(x29422,x29423),x29424)))), % 162.99/163.18 inference(scs_inference,[],[272,317,10,11,6,8,12,13])). % 162.99/163.18 cnf(2943,plain, % 162.99/163.18 (E(f1(x29431,f6(f3(x29432,f2(x29432,x29433)),x29434)),f1(x29431,f6(f3(x29432,x29433),x29434)))), % 162.99/163.18 inference(scs_inference,[],[272,317,10,11,6,8,12,13,5])). % 162.99/163.18 cnf(2945,plain, % 162.99/163.18 (E(f1(f6(f3(x29451,f2(x29451,x29452)),x29453),x29454),f1(f6(f3(x29451,x29452),x29453),x29454))), % 162.99/163.18 inference(scs_inference,[],[272,317,10,11,6,8,12,13,5,9,4])). % 162.99/163.18 cnf(2952,plain, % 162.99/163.18 (P1(f3(x29521,f2(f2(f3(x29522,f2(x29523,x29522)),x29521),x29521)),f3(x29521,f3(x29522,x29523)))), % 162.99/163.18 inference(scs_inference,[],[272,317,1128,566,558,10,11,6,8,12,13,5,9,4,7,26,2,3,14])). % 162.99/163.18 cnf(2998,plain, % 162.99/163.18 (E(f6(f6(f3(x29981,f2(x29982,x29981)),x29983),x29984),f6(f6(f3(x29981,x29982),x29983),x29984))), % 162.99/163.18 inference(scs_inference,[],[401,6])). % 162.99/163.18 cnf(2999,plain, % 162.99/163.18 (E(f5(f6(f3(x29991,f2(x29992,x29991)),x29993),x29994),f5(f6(f3(x29991,x29992),x29993),x29994))), % 162.99/163.18 inference(scs_inference,[],[401,6,10])). % 162.99/163.18 cnf(3000,plain, % 162.99/163.18 (E(f3(f6(f3(x30001,f2(x30002,x30001)),x30003),x30004),f3(f6(f3(x30001,x30002),x30003),x30004))), % 162.99/163.18 inference(scs_inference,[],[401,6,10,12])). % 162.99/163.18 cnf(3001,plain, % 162.99/163.18 (E(f1(x30011,f6(f3(x30012,f2(x30013,x30012)),x30014)),f1(x30011,f6(f3(x30012,x30013),x30014)))), % 163.01/163.18 inference(scs_inference,[],[401,6,10,12,5])). % 163.01/163.18 cnf(3002,plain, % 163.01/163.18 (E(f3(x30021,f6(f3(x30022,f2(x30023,x30022)),x30024)),f3(x30021,f6(f3(x30022,x30023),x30024)))), % 163.01/163.18 inference(scs_inference,[],[401,6,10,12,5,13])). % 163.01/163.18 cnf(3003,plain, % 163.01/163.18 (E(f2(x30031,f6(f3(x30032,f2(x30033,x30032)),x30034)),f2(x30031,f6(f3(x30032,x30033),x30034)))), % 163.01/163.18 inference(scs_inference,[],[401,6,10,12,5,13,9])). % 163.01/163.18 cnf(3004,plain, % 163.01/163.18 (E(f2(f6(f3(x30041,f2(x30042,x30041)),x30043),x30044),f2(f6(f3(x30041,x30042),x30043),x30044))), % 163.01/163.18 inference(scs_inference,[],[401,6,10,12,5,13,9,8])). % 163.01/163.18 cnf(3005,plain, % 163.01/163.18 (E(f5(x30051,f6(f3(x30052,f2(x30053,x30052)),x30054)),f5(x30051,f6(f3(x30052,x30053),x30054)))), % 163.01/163.18 inference(scs_inference,[],[401,6,10,12,5,13,9,8,11])). % 163.01/163.18 cnf(3008,plain, % 163.01/163.18 (E(f1(f6(f3(x30081,f2(x30082,x30081)),x30083),x30084),f1(f6(f3(x30081,x30082),x30083),x30084))), % 163.01/163.18 inference(scs_inference,[],[401,486,6,10,12,5,13,9,8,11,26,4])). % 163.01/163.18 cnf(3058,plain, % 163.01/163.18 (E(f3(x30581,f2(f2(x30581,f2(x30581,f2(x30581,x30581))),x30581)),f3(x30581,x30581))), % 163.01/163.18 inference(scs_inference,[],[401,738,1117,2,27])). % 163.01/163.18 cnf(3064,plain, % 163.01/163.18 (~E(f1(f3(a7,a4),f3(a4,a7)),f1(f3(a7,f2(a4,a7)),f3(a4,f2(a4,a7))))), % 163.01/163.18 inference(scs_inference,[],[20,53,401,2852,1821,738,1117,2,27,15,3])). % 163.01/163.18 cnf(3066,plain, % 163.01/163.18 (P1(f1(f3(x30661,f2(f1(x30661,x30662),x30663)),f3(x30662,f2(f1(x30661,x30662),x30663))),f3(f1(x30661,x30662),x30663))), % 163.01/163.18 inference(scs_inference,[],[20,48,53,401,2852,59,1821,738,1117,2,27,15,3,14])). % 163.01/163.18 cnf(3074,plain, % 163.01/163.18 (P1(f3(f1(x30741,x30742),f2(f1(x30741,x30742),x30743)),f1(f3(x30741,x30743),f3(x30742,x30743)))), % 163.01/163.18 inference(scs_inference,[],[48,59,738,1117,486,2,27,15])). % 163.01/163.18 cnf(3078,plain, % 163.01/163.18 (P1(f1(f3(x30781,f3(x30782,f2(x30783,x30782))),f3(x30784,f3(x30782,f2(x30783,x30782)))),f3(f1(x30781,x30784),f3(x30782,x30783)))), % 163.01/163.18 inference(scs_inference,[],[48,269,59,1821,1128,738,1117,486,2,27,15,3,14])). % 163.01/163.18 cnf(3082,plain, % 163.01/163.18 (E(f3(x30821,f2(x30821,f2(f2(f2(x30821,x30822),x30821),x30821))),f3(x30821,x30822))), % 163.01/163.18 inference(scs_inference,[],[828,736,245,2,27])). % 163.01/163.18 cnf(3085,plain, % 163.01/163.18 (P1(f3(f1(x30851,x30852),f3(x30853,f2(x30854,x30853))),f1(f3(x30851,f3(x30853,x30854)),f3(x30852,f3(x30853,x30854))))), % 163.01/163.18 inference(scs_inference,[],[48,1128,828,736,245,2,27,15])). % 163.01/163.18 cnf(3087,plain, % 163.01/163.18 (E(f3(f1(x30871,x30872),x30873),f1(f3(x30871,x30873),f3(x30872,x30873)))), % 163.01/163.18 inference(rename_variables,[],[48])). % 163.01/163.18 cnf(3090,plain, % 163.01/163.18 (P1(f1(f3(x30901,f2(x30902,x30903)),f3(x30904,f2(x30902,x30903))),f3(f1(x30904,x30901),f2(x30903,x30902)))), % 163.01/163.18 inference(scs_inference,[],[48,3087,238,1128,558,239,828,736,245,2,27,15,3,14])). % 163.01/163.18 cnf(3094,plain, % 163.01/163.18 (E(f3(x30941,f2(x30941,f2(x30941,f2(f2(x30941,x30941),x30941)))),f3(x30941,x30941))), % 163.01/163.18 inference(scs_inference,[],[913,945,3082,2,27])). % 163.01/163.18 cnf(3107,plain, % 163.01/163.18 (E(f3(x31071,f2(f2(x31071,f2(f2(x31072,x31071),x31071)),x31071)),f3(x31071,x31072))), % 163.01/163.18 inference(scs_inference,[],[997,832,3094,2,27])). % 163.01/163.18 cnf(3112,plain, % 163.01/163.18 (E(f3(f1(x31121,x31122),x31123),f1(f3(x31121,x31123),f3(x31122,x31123)))), % 163.01/163.18 inference(rename_variables,[],[48])). % 163.01/163.18 cnf(3115,plain, % 163.01/163.18 (P1(f1(f3(x31151,x31152),f3(x31153,x31152)),f3(f1(x31151,x31153),f2(f1(x31151,x31153),x31152)))), % 163.01/163.18 inference(scs_inference,[],[48,3112,228,1821,226,57,997,832,3094,2,27,15,3,14])). % 163.01/163.18 cnf(3119,plain, % 163.01/163.18 (E(f3(x31191,f2(f2(x31191,f2(x31192,x31191)),x31191)),f3(x31191,x31192))), % 163.01/163.18 inference(scs_inference,[],[933,921,3107,2,27])). % 163.01/163.18 cnf(3126,plain, % 163.01/163.18 (P1(f1(f3(x31261,f2(f2(f1(x31261,x31262),x31263),f1(x31261,x31262))),f3(x31262,f2(f2(f1(x31261,x31262),x31263),f1(x31261,x31262)))),f3(f1(x31261,x31262),x31263))), % 163.01/163.18 inference(scs_inference,[],[48,19,53,253,1515,220,933,921,3107,2,27,15,3,14])). % 163.01/163.18 cnf(3130,plain, % 163.01/163.18 (E(f1(f3(x31301,f2(f1(x31301,x31302),f1(x31301,x31302))),f3(x31302,f2(f1(x31301,x31302),f1(x31301,x31302)))),f3(f1(x31301,x31302),f1(x31301,x31302)))), % 163.01/163.18 inference(scs_inference,[],[3066,999,3119,2,27])). % 163.01/163.18 cnf(3134,plain, % 163.01/163.18 (P1(f3(f1(x31341,x31342),f2(f2(f1(x31341,x31342),x31343),f1(x31341,x31342))),f1(f3(x31341,x31343),f3(x31342,x31343)))), % 163.01/163.18 inference(scs_inference,[],[48,220,3066,999,3119,2,27,15])). % 163.01/163.18 cnf(3143,plain, % 163.01/163.18 (~E(f1(f3(a7,a4),f3(a4,a7)),f1(f3(a4,f2(a4,a7)),f3(a7,f2(a4,a7))))), % 163.01/163.18 inference(scs_inference,[],[19,22,1821,1497,3130,2,15,3])). % 163.01/163.18 cnf(3147,plain, % 163.01/163.18 (E(f3(f1(x31471,x31472),f2(f1(x31471,x31472),x31473)),f1(f3(x31471,x31473),f3(x31472,x31473)))), % 163.01/163.18 inference(scs_inference,[],[48,19,22,1821,1497,1471,3074,3115,3130,2,15,3,14,27])). % 163.01/163.18 cnf(3156,plain, % 163.01/163.18 (P1(f1(f3(x31561,x31562),f3(x31563,x31562)),f1(x31564,f1(x31565,f1(x31561,x31563))))), % 163.01/163.18 inference(scs_inference,[],[48,19,292,1763,486,1363,3147,2,15,3,14])). % 163.01/163.18 cnf(3158,plain, % 163.01/163.18 (E(f6(x31581,f3(x31582,f2(x31582,f2(x31583,x31582)))),f6(x31581,f3(x31582,x31583)))), % 163.01/163.18 inference(scs_inference,[],[48,19,292,1763,486,1363,1041,1167,3147,2,15,3,14,27])). % 163.01/163.18 cnf(3166,plain, % 163.01/163.18 (P1(f1(f3(x31661,x31662),f3(x31663,x31662)),f1(f1(x31664,f1(x31661,x31663)),x31665))), % 163.01/163.18 inference(scs_inference,[],[48,19,1714,1276,3147,3064,262,2,15,3,14])). % 163.01/163.18 cnf(3176,plain, % 163.01/163.18 (P1(f1(f3(x31761,x31762),f3(x31763,x31762)),f1(f1(f1(x31761,x31763),x31764),x31765))), % 163.01/163.18 inference(scs_inference,[],[48,19,24,1704,1580,245,577,2,15,3,14])). % 163.01/163.18 cnf(3184,plain, % 163.01/163.18 (E(f5(f3(x31841,f2(f2(x31841,x31842),x31841)),f2(x31843,x31844)),f5(f3(x31841,x31842),f2(x31844,x31843)))), % 163.01/163.18 inference(scs_inference,[],[19,293,1304,262,152,2,15,3])). % 163.01/163.18 cnf(3193,plain, % 163.01/163.18 (P1(f1(f3(x31931,f2(f1(x31931,x31932),x31933)),f3(x31932,f2(f1(x31931,x31932),x31933))),f1(f3(x31931,x31933),f3(x31932,x31933)))), % 163.01/163.18 inference(scs_inference,[],[48,3066,3184,2,15])). % 163.01/163.18 cnf(3207,plain, % 163.01/163.18 (E(f2(x32071,f3(x32072,f2(x32072,x32073))),f2(f3(x32072,x32073),x32071))), % 163.01/163.18 inference(scs_inference,[],[48,20,3090,152,569,2,15,3])). % 163.01/163.18 cnf(3220,plain, % 163.01/163.18 (E(f2(f3(x32201,f2(x32202,x32201)),x32203),f2(x32203,f3(x32201,x32202)))), % 163.01/163.18 inference(scs_inference,[],[48,20,19,1262,1295,569,653,2,15,14,3])). % 163.01/163.18 cnf(3227,plain, % 163.01/163.18 (P1(f3(f1(x32271,x32272),f2(f1(x32271,x32272),f2(f1(x32271,x32272),x32273))),f1(f3(x32271,x32273),f3(x32272,x32273)))), % 163.01/163.18 inference(scs_inference,[],[48,76,666,2,15])). % 163.01/163.18 cnf(3243,plain, % 163.01/163.18 (E(f1(f3(x32431,f3(x32432,f2(x32432,x32433))),f3(x32434,f3(x32432,f2(x32432,x32433)))),f3(f1(x32434,x32431),f3(x32432,x32433)))), % 163.01/163.18 inference(scs_inference,[],[48,19,53,1342,1591,666,3207,2,15,14,3])). % 163.01/163.18 cnf(3253,plain, % 163.01/163.18 (~E(f1(f3(a7,a4),f3(a4,a7)),f1(f3(a4,f2(a4,a7)),f3(a7,a4)))), % 163.01/163.18 inference(scs_inference,[],[19,1523,566,3143,3243,2,15,3])). % 163.01/163.18 cnf(3263,plain, % 163.01/163.18 (E(f1(x32631,x32632),f1(x32632,x32631))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(3267,plain, % 163.01/163.18 (E(f3(f1(x32671,x32672),f3(x32673,f2(x32673,x32674))),f3(f1(x32672,x32671),f3(x32673,x32674)))), % 163.01/163.18 inference(scs_inference,[],[48,19,3263,3227,920,3243,3220,2,15,14,3])). % 163.01/163.18 cnf(3343,plain, % 163.01/163.18 (E(f6(f1(x33431,x33432),f3(x33433,f2(x33433,f2(x33433,x33434)))),f6(f1(x33432,x33431),f3(x33433,x33434)))), % 163.01/163.18 inference(scs_inference,[],[19,180,3193,200,3267,2,15,3])). % 163.01/163.18 cnf(3352,plain, % 163.01/163.18 (P1(f3(f1(x33521,x33522),x33523),f1(f2(x33524,x33525),f1(x33526,f1(x33522,x33521))))), % 163.01/163.18 inference(scs_inference,[],[19,1504,3343,2,15])). % 163.01/163.18 cnf(3448,plain, % 163.01/163.18 (P1(f3(f2(x34481,x34482),f2(f1(x34483,x34484),f2(x34481,x34482))),f3(f2(x34482,x34481),f1(x34484,x34483)))), % 163.01/163.18 inference(scs_inference,[],[48,238,131,428,120,2,15,14])). % 163.01/163.18 cnf(3450,plain, % 163.01/163.18 (E(f5(f3(x34501,f2(x34501,f2(x34501,x34502))),f2(x34503,x34504)),f5(f3(x34501,x34502),f2(x34504,x34503)))), % 163.01/163.18 inference(scs_inference,[],[48,293,238,131,428,371,120,2,15,14,3])). % 163.01/163.18 cnf(3453,plain, % 163.01/163.18 (E(f3(f1(x34531,x34531),f1(x34532,x34533)),f1(f3(x34531,f1(x34533,x34532)),f3(x34531,f1(x34533,x34532))))), % 163.01/163.18 inference(scs_inference,[],[48,293,238,131,428,975,371,120,2,15,14,3,27])). % 163.01/163.18 cnf(3458,plain, % 163.01/163.18 (E(f3(x34581,x34582),f3(x34581,f2(x34582,x34581)))), % 163.01/163.18 inference(rename_variables,[],[238])). % 163.01/163.18 cnf(3459,plain, % 163.01/163.18 (P1(f3(f2(x34591,x34592),f2(f2(x34593,x34594),f2(x34591,x34592))),f3(f2(x34592,x34591),f2(x34594,x34593)))), % 163.01/163.18 inference(scs_inference,[],[238,3458,428,431,3450,2,15,14])). % 163.01/163.18 cnf(3471,plain, % 163.01/163.18 (E(f5(f1(x34711,x34712),f3(x34713,f2(f2(x34713,x34714),x34713))),f5(f1(x34712,x34711),f3(x34713,x34714)))), % 163.01/163.18 inference(scs_inference,[],[19,238,292,431,3078,397,3453,2,15,14,3])). % 163.01/163.18 cnf(3484,plain, % 163.01/163.18 (E(f3(f1(x34841,x34842),f2(f2(f1(x34841,x34842),f1(x34841,x34842)),f1(x34841,x34842))),f1(f3(x34841,f1(x34841,x34842)),f3(x34842,f1(x34841,x34842))))), % 163.01/163.18 inference(scs_inference,[],[48,53,933,3453,3134,246,3471,2,15,14,3,27])). % 163.01/163.18 cnf(3490,plain, % 163.01/163.18 (P1(f1(f3(x34901,f2(f2(x34902,f1(x34901,x34903)),f1(x34901,x34903))),f3(x34903,f2(f2(x34902,f1(x34901,x34903)),f1(x34901,x34903)))),f3(f1(x34901,x34903),x34902))), % 163.01/163.18 inference(scs_inference,[],[19,48,3134,248,3484,2,15,14])). % 163.01/163.18 cnf(3493,plain, % 163.01/163.18 (E(f6(f1(x34931,x34932),f3(x34933,f2(f2(x34934,x34933),x34933))),f6(f1(x34932,x34931),f3(x34933,x34934)))), % 163.01/163.18 inference(scs_inference,[],[19,48,180,3134,248,405,3484,2,15,14,3])). % 163.01/163.18 cnf(3499,plain, % 163.01/163.18 (P1(f3(f1(x34991,x34992),x34993),f1(f3(x34991,f2(f2(x34993,f1(x34991,x34992)),f1(x34991,x34992))),f3(x34992,f2(f2(x34993,f1(x34991,x34992)),f1(x34991,x34992)))))), % 163.01/163.18 inference(scs_inference,[],[48,246,3493,2,15])). % 163.01/163.18 cnf(3501,plain, % 163.01/163.18 (E(f3(f1(x35011,x35012),x35013),f1(f3(x35011,x35013),f3(x35012,x35013)))), % 163.01/163.18 inference(rename_variables,[],[48])). % 163.01/163.18 cnf(3505,plain, % 163.01/163.18 (E(f5(f3(x35051,f2(x35051,f2(x35052,x35051))),f2(x35053,x35054)),f5(f3(x35051,x35052),f2(x35054,x35053)))), % 163.01/163.18 inference(scs_inference,[],[48,3501,293,246,231,408,3493,2,15,14,3])). % 163.01/163.18 cnf(3508,plain, % 163.01/163.18 (E(f1(f3(x35081,f2(f2(f1(x35081,x35082),f1(x35081,x35082)),f1(x35081,x35082))),f3(x35082,f2(f2(f1(x35081,x35082),f1(x35081,x35082)),f1(x35081,x35082)))),f3(f1(x35081,x35082),f1(x35081,x35082)))), % 163.01/163.18 inference(scs_inference,[],[48,3501,293,3126,246,231,408,3493,2,15,14,3,27])). % 163.01/163.18 cnf(3518,plain, % 163.01/163.18 (E(f1(f3(x35181,f2(f2(x35182,f1(x35181,x35183)),f1(x35181,x35183))),f3(x35183,f2(f2(x35182,f1(x35181,x35183)),f1(x35181,x35183)))),f3(f1(x35181,x35183),x35182))), % 163.01/163.18 inference(scs_inference,[],[19,48,248,223,3490,3499,3508,3505,2,15,14,3,27])). % 163.01/163.18 cnf(3522,plain, % 163.01/163.18 (P1(f3(f1(x35221,x35222),f2(x35223,f1(x35221,x35222))),f1(f3(x35221,x35223),f3(x35222,x35223)))), % 163.01/163.18 inference(scs_inference,[],[48,231,3518,2,15])). % 163.01/163.18 cnf(3635,plain, % 163.01/163.18 (P1(f1(f3(x36351,f1(x36352,x36353)),f3(x36354,f1(x36352,x36353))),f1(f3(x36354,f1(x36353,x36352)),f3(x36351,f1(x36353,x36352))))), % 163.01/163.18 inference(scs_inference,[],[48,975,209,2,15])). % 163.01/163.18 cnf(3681,plain, % 163.01/163.18 (E(f1(x36811,x36812),f1(x36812,x36811))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(3685,plain, % 163.01/163.18 (E(f2(f3(x36851,f2(f2(x36852,x36851),x36851)),x36853),f2(x36853,f3(x36851,x36852)))), % 163.01/163.18 inference(scs_inference,[],[19,3681,20,3499,805,582,2937,2,15,14,3])). % 163.01/163.18 cnf(3693,plain, % 163.01/163.18 (E(f1(x36931,x36932),f1(x36932,x36931))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(3696,plain, % 163.01/163.18 (E(f5(f6(f3(x36961,f2(x36961,x36962)),x36963),f2(x36964,x36965)),f5(f6(f3(x36961,x36962),x36963),f2(x36965,x36964)))), % 163.01/163.18 inference(scs_inference,[],[19,3693,293,805,3156,2937,3685,2,15,14,3])). % 163.01/163.18 cnf(3703,plain, % 163.01/163.18 (E(f1(x37031,x37032),f1(x37032,x37031))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(3706,plain, % 163.01/163.18 (E(f6(f3(x37061,f2(x37061,f2(x37061,f2(x37062,x37061)))),x37063),f6(f3(x37061,x37062),x37063))), % 163.01/163.18 inference(scs_inference,[],[19,3703,317,3166,1086,648,3696,2,15,14,3])). % 163.01/163.18 cnf(3712,plain, % 163.01/163.18 (P1(f3(f1(x37121,x37122),f3(x37123,f2(f2(x37124,x37123),x37123))),f1(f3(x37121,f3(x37123,x37124)),f3(x37122,f3(x37123,x37124))))), % 163.01/163.18 inference(scs_inference,[],[48,1068,3706,2,15])). % 163.01/163.18 cnf(3717,plain, % 163.01/163.18 (E(f5(f3(x37171,f2(f2(x37172,x37171),x37171)),f2(x37173,x37174)),f5(f3(x37171,x37172),f2(x37174,x37173)))), % 163.01/163.18 inference(scs_inference,[],[19,48,293,3176,1068,3706,649,2,15,14,3])). % 163.01/163.18 cnf(3729,plain, % 163.01/163.18 (E(f6(f1(x37291,x37292),f3(x37293,f2(x37293,f2(x37294,x37293)))),f6(f1(x37292,x37291),f3(x37293,x37294)))), % 163.01/163.18 inference(scs_inference,[],[20,180,238,1038,1042,3158,3717,2,15,14,3])). % 163.01/163.18 cnf(3735,plain, % 163.01/163.18 (P1(f2(f3(x37351,f2(f2(x37352,x37351),x37351)),x37353),f2(x37353,f3(x37351,x37352)))), % 163.01/163.18 inference(scs_inference,[],[20,1042,3729,2,15])). % 163.01/163.18 cnf(3797,plain, % 163.01/163.18 (E(f2(x37971,x37972),f2(x37972,x37971))), % 163.01/163.18 inference(rename_variables,[],[20])). % 163.01/163.18 cnf(3798,plain, % 163.01/163.18 (E(f2(f3(x37981,f2(x37981,x37982)),x37983),f2(x37983,f3(x37981,x37982)))), % 163.01/163.18 inference(scs_inference,[],[19,20,3797,3712,3735,129,2942,2,15,14,3])). % 163.01/163.18 cnf(3807,plain, % 163.01/163.18 (P1(f3(f2(x38071,x38072),f2(f2(f1(x38073,x38074),f2(x38071,x38072)),f2(x38071,x38072))),f3(f2(x38072,x38071),f1(x38074,x38073)))), % 163.01/163.18 inference(scs_inference,[],[48,238,2952,3448,3798,2,15,14])). % 163.01/163.18 cnf(3815,plain, % 163.01/163.18 (E(f3(x38151,x38152),f3(x38151,f2(x38152,x38151)))), % 163.01/163.18 inference(rename_variables,[],[238])). % 163.01/163.18 cnf(3818,plain, % 163.01/163.18 (E(f5(f3(x38181,f2(x38181,x38182)),f2(x38183,x38184)),f5(f3(x38181,x38182),f2(x38184,x38183)))), % 163.01/163.18 inference(scs_inference,[],[238,3815,293,3448,3807,184,2943,2,15,14,3])). % 163.01/163.18 cnf(3824,plain, % 163.01/163.18 (P1(f3(f2(x38241,x38242),f2(f2(f1(x38243,x38244),f2(x38241,x38242)),f2(x38241,x38242))),f3(f2(x38242,x38241),f2(f1(x38244,x38243),f2(x38242,x38241))))), % 163.01/163.18 inference(scs_inference,[],[238,3807,3818,2,15])). % 163.01/163.18 cnf(3825,plain, % 163.01/163.18 (E(f3(x38251,x38252),f3(x38251,f2(x38252,x38251)))), % 163.01/163.18 inference(rename_variables,[],[238])). % 163.01/163.18 cnf(3826,plain, % 163.01/163.18 (P1(f3(f2(x38261,x38262),f2(f2(f2(x38263,x38264),f2(x38261,x38262)),f2(x38261,x38262))),f3(f2(x38262,x38261),f2(x38264,x38263)))), % 163.01/163.18 inference(scs_inference,[],[238,3825,3807,3459,3818,2,15,14])). % 163.01/163.18 cnf(3843,plain, % 163.01/163.18 (P1(f3(f2(x38431,x38432),f2(f2(f2(x38433,x38434),f2(x38431,x38432)),f2(x38431,x38432))),f3(f2(x38432,x38431),f2(f2(x38434,x38433),f2(x38432,x38431))))), % 163.01/163.18 inference(scs_inference,[],[238,3826,2945,2,15])). % 163.01/163.18 cnf(3877,plain, % 163.01/163.18 (P1(f3(f1(x38771,x38772),f2(f2(f2(x38773,f1(x38771,x38772)),f1(x38771,x38772)),f1(x38771,x38772))),f1(f3(x38771,x38773),f3(x38772,x38773)))), % 163.01/163.18 inference(scs_inference,[],[48,831,2999,2,15])). % 163.01/163.18 cnf(3893,plain, % 163.01/163.18 (E(f6(f6(f3(x38931,f2(x38932,x38931)),x38933),f1(x38934,x38935)),f6(f6(f3(x38931,x38932),x38933),f1(x38935,x38934)))), % 163.01/163.18 inference(scs_inference,[],[48,238,471,2998,122,3824,3000,2,15,14,3])). % 163.01/163.18 cnf(3896,plain, % 163.01/163.18 (E(f3(f1(x38961,x38962),f1(x38963,x38964)),f1(f3(x38962,f1(x38964,x38963)),f3(x38961,f1(x38964,x38963))))), % 163.01/163.18 inference(scs_inference,[],[48,238,471,975,2998,122,3824,3000,2,15,14,3,27])). % 163.01/163.18 cnf(3899,plain, % 163.01/163.18 (P1(f3(f2(x38991,x38992),f2(f2(f1(x38993,x38994),f2(x38991,x38992)),f2(x38991,x38992))),f3(f2(x38992,x38991),f2(f2(f1(x38994,x38993),f2(x38992,x38991)),f2(x38992,x38991))))), % 163.01/163.18 inference(scs_inference,[],[238,3824,3893,2,15])). % 163.01/163.18 cnf(3900,plain, % 163.01/163.18 (E(f3(x39001,x39002),f3(x39001,f2(x39002,x39001)))), % 163.01/163.18 inference(rename_variables,[],[238])). % 163.01/163.18 cnf(3903,plain, % 163.01/163.18 (E(f5(f6(f3(x39031,f2(x39032,x39031)),x39033),f2(x39034,x39035)),f5(f6(f3(x39031,x39032),x39033),f2(x39035,x39034)))), % 163.01/163.18 inference(scs_inference,[],[238,3900,293,3824,2999,3843,3893,2,15,14,3])). % 163.01/163.18 cnf(3912,plain, % 163.01/163.18 (E(f3(x39121,x39122),f3(x39121,f2(x39122,x39121)))), % 163.01/163.18 inference(rename_variables,[],[238])). % 163.01/163.18 cnf(3913,plain, % 163.01/163.18 (E(f3(x39131,f2(x39131,f2(x39131,f2(x39131,x39131)))),f3(x39131,x39131))), % 163.01/163.18 inference(scs_inference,[],[19,238,3912,3877,3899,3058,3903,2,15,14,3])). % 163.01/163.18 cnf(3919,plain, % 163.01/163.18 (P1(f3(f2(x39191,x39192),f2(f2(f2(x39193,x39194),f2(x39191,x39192)),f2(x39191,x39192))),f3(f2(x39192,x39191),f2(f2(f2(x39194,x39193),f2(x39192,x39191)),f2(x39192,x39191))))), % 163.01/163.18 inference(scs_inference,[],[238,3843,3913,2,15])). % 163.01/163.18 cnf(3928,plain, % 163.01/163.18 (E(f1(f3(x39281,f1(x39282,x39283)),f3(x39284,f1(x39282,x39283))),f3(f1(x39284,x39281),f1(x39283,x39282)))), % 163.01/163.18 inference(scs_inference,[],[3896,2])). % 163.01/163.18 cnf(3929,plain, % 163.01/163.18 (P1(f3(f1(x39291,x39292),f2(f1(x39291,x39292),f2(x39293,f1(x39291,x39292)))),f1(f3(x39291,x39293),f3(x39292,x39293)))), % 163.01/163.18 inference(scs_inference,[],[48,257,3896,2,15])). % 163.01/163.18 cnf(3933,plain, % 163.01/163.18 (E(f6(f1(x39331,x39332),f3(x39333,f2(x39333,x39334))),f6(f1(x39332,x39331),f3(x39333,x39334)))), % 163.01/163.18 inference(scs_inference,[],[48,238,180,257,3919,213,3896,2,15,14,3])). % 163.01/163.18 cnf(3950,plain, % 163.01/163.18 (E(f1(x39501,x39502),f1(x39502,x39501))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(3952,plain, % 163.01/163.18 (E(f1(x39521,x39522),f1(x39522,x39521))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(3953,plain, % 163.01/163.18 (E(f1(f3(x39531,f1(x39532,x39533)),f3(x39534,f1(x39532,x39533))),f3(f1(x39531,x39534),f1(x39533,x39532)))), % 163.01/163.18 inference(scs_inference,[],[19,3950,3952,3929,3635,3928,3933,2,15,14,3])). % 163.01/163.18 cnf(3958,plain, % 163.01/163.18 (P1(f3(f1(x39581,x39582),f2(f2(f1(x39582,x39581),x39583),f1(x39582,x39581))),f1(f3(x39582,x39583),f3(x39581,x39583)))), % 163.01/163.18 inference(scs_inference,[],[48,675,3953,2,15])). % 163.01/163.18 cnf(3962,plain, % 163.01/163.18 (E(f1(x39621,x39622),f1(x39622,x39621))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(3976,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(f2(x39761,x39762),f2(f1(f3(a7,a4),f3(a4,a7)),f2(x39763,x39764))))), % 163.01/163.18 inference(scs_inference,[],[19,48,238,3253,675,789,3953,243,2,15,14,3,27,26,2379,723,2864,2858])). % 163.01/163.18 cnf(3978,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(f1(f3(a4,a7),f3(a7,a4)),f2(x39781,x39782)))), % 163.01/163.18 inference(scs_inference,[],[19,48,238,3253,675,789,3953,243,2,15,14,3,27,26,2379,723,2864,2858,2722])). % 163.01/163.18 cnf(3980,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(f2(f2(x39801,x39802),f1(f3(a4,a7),f3(a7,a4))),f2(x39803,x39804)))), % 163.01/163.18 inference(scs_inference,[],[19,48,238,3253,675,789,3953,243,2,15,14,3,27,26,2379,723,2864,2858,2722,2342])). % 163.01/163.18 cnf(3982,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f3(f2(f1(f3(a7,a4),f3(a4,a7)),x39821),x39822))), % 163.01/163.18 inference(scs_inference,[],[19,48,238,3253,675,789,3953,243,2,15,14,3,27,26,2379,723,2864,2858,2722,2342,2257])). % 163.01/163.18 cnf(3989,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(f1(f3(a7,a4),f3(a4,a7)),f2(x39891,x39892)))), % 163.01/163.18 inference(scs_inference,[],[19,48,238,3253,675,789,3953,243,2,15,14,3,27,26,2379,723,2864,2858,2722,2342,2257,2109,1984,1976,1975])). % 163.01/163.18 cnf(3994,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f2(x39941,x39942)),x39943))), % 163.01/163.18 inference(scs_inference,[],[19,3962,48,238,3253,675,789,3953,243,2,15,14,3,27,26,2379,723,2864,2858,2722,2342,2257,2109,1984,1976,1975,820,760,17])). % 163.01/163.18 cnf(3998,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(x39981,f1(f3(a7,a4),f3(a4,a7))))), % 163.01/163.18 inference(scs_inference,[],[19,3962,48,238,292,3253,675,789,3953,243,2,15,14,3,27,26,2379,723,2864,2858,2722,2342,2257,2109,1984,1976,1975,820,760,17,16,32])). % 163.01/163.18 cnf(4002,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f2(x40021,x40022)))), % 163.01/163.18 inference(scs_inference,[],[19,3962,48,238,292,3253,675,789,3953,243,2,15,14,3,27,26,2379,723,2864,2858,2722,2342,2257,2109,1984,1976,1975,820,760,17,16,32,38,40])). % 163.01/163.18 cnf(4076,plain, % 163.01/163.18 (P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f2(x40761,x40762)))), % 163.01/163.18 inference(scs_inference,[],[4002,3989,3001,2,1976,2862,2013])). % 163.01/163.18 cnf(4082,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x40821,f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x40822,x40823))))), % 163.01/163.18 inference(scs_inference,[],[4002,3989,3980,3976,3001,2,1976,2862,2013,2383,858,1975,2671])). % 163.01/163.18 cnf(4085,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(x40851,f1(f3(a7,a4),f3(a4,a7))))), % 163.01/163.18 inference(rename_variables,[],[3998])). % 163.01/163.18 cnf(4089,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x40891,x40892),f2(f1(f3(a7,a4),f3(a4,a7)),f2(x40893,x40894))))), % 163.01/163.18 inference(scs_inference,[],[4002,3989,3980,3998,4085,3976,3001,2,1976,2862,2013,2383,858,1975,2671,723,713,2855])). % 163.01/163.18 cnf(4090,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(x40901,f1(f3(a7,a4),f3(a4,a7))))), % 163.01/163.18 inference(rename_variables,[],[3998])). % 163.01/163.18 cnf(4099,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(x40991,f1(f3(a7,a4),f3(a4,a7))))), % 163.01/163.18 inference(rename_variables,[],[3998])). % 163.01/163.18 cnf(4109,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x41091,f1(f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x41092,x41093)),f2(x41094,x41095))))), % 163.01/163.18 inference(scs_inference,[],[4002,3989,3980,3998,4085,4090,4099,3976,3001,2,1976,2862,2013,2383,858,1975,2671,723,713,2855,2853,790,2342,2316,2082,851,2109,2722,688])). % 163.01/163.18 cnf(4113,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(f2(x41131,f2(f1(f3(a7,a4),f3(a4,a7)),f2(x41132,x41133))),x41134))), % 163.01/163.18 inference(scs_inference,[],[4002,3989,3980,3998,4085,4090,4099,3976,3001,2,1976,2862,2013,2383,858,1975,2671,723,713,2855,2853,790,2342,2316,2082,851,2109,2722,688,758,71])). % 163.01/163.18 cnf(4119,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f2(x41191,x41192),f1(f3(a4,f2(a4,a7)),f3(a7,a4))),x41193))), % 163.01/163.18 inference(scs_inference,[],[4002,3989,3980,3998,4085,4090,4099,3976,3001,2,1976,2862,2013,2383,858,1975,2671,723,713,2855,2853,790,2342,2316,2082,851,2109,2722,688,758,71,1896,833,2525])). % 163.01/163.18 cnf(4122,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f2(x41221,x41222)),x41223))), % 163.01/163.18 inference(rename_variables,[],[3994])). % 163.01/163.18 cnf(4124,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(f2(f2(x41241,x41242),f1(f3(a4,a7),f3(a7,a4))),f2(x41243,x41244)))), % 163.01/163.18 inference(scs_inference,[],[4002,3994,3989,3980,3998,4085,4090,4099,3976,3001,2,1976,2862,2013,2383,858,1975,2671,723,713,2855,2853,790,2342,2316,2082,851,2109,2722,688,758,71,1896,833,2525,1898,2366])). % 163.01/163.18 cnf(4127,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f2(x41271,x41272)),x41273))), % 163.01/163.18 inference(rename_variables,[],[3994])). % 163.01/163.18 cnf(4130,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f2(x41301,x41302)),x41303))), % 163.01/163.18 inference(rename_variables,[],[3994])). % 163.01/163.18 cnf(4134,plain, % 163.01/163.18 (E(f1(x41341,x41342),f1(x41342,x41341))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(4153,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x41531,f1(f1(x41532,f1(f3(a4,f2(a4,a7)),f3(a7,a4))),f2(x41533,x41534))))), % 163.01/163.18 inference(scs_inference,[],[19,4134,293,292,24,789,4002,3994,4122,4127,4130,3989,3980,3998,4085,4090,4099,3976,3982,936,250,3001,2,1976,2862,2013,2383,858,1975,2671,723,713,2855,2853,790,2342,2316,2082,851,2109,2722,688,758,71,1896,833,2525,1898,2366,846,807,15,14,3,17,16,32,40,1984,2112,2494])). % 163.01/163.18 cnf(4155,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x41551,f1(f3(a4,f2(a4,a7)),f3(a7,a4))))), % 163.01/163.18 inference(scs_inference,[],[19,4134,293,292,24,789,4002,3994,4122,4127,4130,3989,3980,3998,4085,4090,4099,3976,3982,936,250,3001,2,1976,2862,2013,2383,858,1975,2671,723,713,2855,2853,790,2342,2316,2082,851,2109,2722,688,758,71,1896,833,2525,1898,2366,846,807,15,14,3,17,16,32,40,1984,2112,2494,896])). % 163.01/163.18 cnf(4159,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f1(f3(a7,a4),f3(a4,a7)))+~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),x41591)), % 163.01/163.18 inference(scs_inference,[],[19,4134,293,292,24,789,4002,3994,4122,4127,4130,3989,3980,3998,4085,4090,4099,3976,3982,936,3352,250,3001,2,1976,2862,2013,2383,858,1975,2671,723,713,2855,2853,790,2342,2316,2082,851,2109,2722,688,758,71,1896,833,2525,1898,2366,846,807,15,14,3,17,16,32,40,1984,2112,2494,896,27,38])). % 163.01/163.18 cnf(4164,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f1(f3(a7,a4),f3(a4,a7)))), % 163.01/163.18 inference(factoring_inference,[],[4159])). % 163.01/163.18 cnf(4166,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(x41661,f1(f3(a7,a4),f3(a4,a7))))), % 163.01/163.18 inference(scs_inference,[],[3998,3002,2,1976])). % 163.01/163.18 cnf(4173,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(f2(x41731,x41732),f2(f2(f1(f3(a7,a4),f3(a4,a7)),f2(x41733,x41734)),f2(x41735,x41736))))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4109,4124,3002,2,1976,1975,713,858,2013,2855])). % 163.01/163.18 cnf(4181,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x41811,x41812),f2(f1(f3(a7,a4),f3(a4,a7)),f1(x41813,x41814))))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4109,4124,4089,3002,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853])). % 163.01/163.18 cnf(4188,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f3(a4,a7))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4109,4124,4164,4089,3002,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30])). % 163.01/163.18 cnf(4194,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x41941,f1(f1(f2(x41942,x41943),f1(f3(a4,f2(a4,a7)),f3(a7,a4))),f1(x41944,x41945))))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4119,4124,4164,4089,3002,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807])). % 163.01/163.18 cnf(4203,plain, % 163.01/163.18 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x42031,f1(f3(a7,a4),f3(a4,a7))),x42032))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4119,4124,4164,4089,3002,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137])). % 163.01/163.18 cnf(4205,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a4,a7),x42051),f3(f3(a7,a4),x42051)))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4119,4124,4164,4089,3002,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284])). % 163.01/163.18 cnf(4207,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(x42071,x42072),f1(f3(a7,a4),f3(a4,f2(a4,a7)))))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4155,4119,4124,4164,4089,3002,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898])). % 163.01/163.18 cnf(4208,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x42081,f1(f3(a4,f2(a4,a7)),f3(a7,a4))))), % 163.01/163.18 inference(rename_variables,[],[4155])). % 163.01/163.18 cnf(4210,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(f2(x42101,f2(f1(f3(a4,a7),f3(a7,a4)),f2(x42102,x42103))),x42104))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4155,4119,4124,4164,4089,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71])). % 163.01/163.18 cnf(4218,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f3(a7,a4))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4155,4208,4119,4124,4164,4089,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71,2366,2525,896,31])). % 163.01/163.18 cnf(4222,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f3(a4,f2(a7,a4)))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4155,4208,4119,4124,4164,4089,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71,2366,2525,896,31,795,811])). % 163.01/163.18 cnf(4226,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f3(a4,f2(f2(a4,a7),a4)))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4155,4208,4119,4124,4164,4089,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71,2366,2525,896,31,795,811,1977,802])). % 163.01/163.18 cnf(4228,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a7,a4),x42281),f3(f3(a4,a7),x42281)))), % 163.01/163.18 inference(scs_inference,[],[3976,3998,4076,4109,4155,4208,4119,4124,4164,4089,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71,2366,2525,896,31,795,811,1977,802,1980])). % 163.01/163.18 cnf(4234,plain, % 163.01/163.18 (E(f1(x42341,x42342),f1(x42342,x42341))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(4237,plain, % 163.01/163.18 (E(f5(f1(x42371,x42372),x42373),f5(f1(x42372,x42371),x42373))), % 163.01/163.18 inference(rename_variables,[],[292])). % 163.01/163.18 cnf(4240,plain, % 163.01/163.18 (E(f1(x42401,x42402),f1(x42402,x42401))), % 163.01/163.18 inference(rename_variables,[],[19])). % 163.01/163.18 cnf(4243,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(x42431,f2(f1(f3(a7,a4),f3(a4,a7)),f2(x42432,x42433))))), % 163.01/163.18 inference(scs_inference,[],[19,4234,4240,292,3989,3976,3998,3001,4076,4109,4155,4208,4119,4124,4164,4089,4113,3958,1044,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71,2366,2525,896,31,795,811,1977,802,1980,1952,800,15,14,3,17,32])). % 163.01/163.18 cnf(4246,plain, % 163.01/163.18 (P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(x42461,f1(f3(a4,f2(a4,a7)),f3(a7,a4))))), % 163.01/163.18 inference(scs_inference,[],[19,4234,4240,292,4237,3989,3976,3998,3001,4076,4109,4155,4208,4119,4124,4164,4089,4113,3958,1044,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71,2366,2525,896,31,795,811,1977,802,1980,1952,800,15,14,3,17,32,16])). % 163.01/163.18 cnf(4248,plain, % 163.01/163.18 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f3(a7,a4),f3(a4,a7)))), % 163.01/163.18 inference(scs_inference,[],[19,4234,4240,292,4237,4002,3989,3976,3998,3001,4076,4109,4155,4208,4119,4124,4164,4089,4113,3958,1044,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71,2366,2525,896,31,795,811,1977,802,1980,1952,800,15,14,3,17,32,16,38])). % 163.01/163.18 cnf(4250,plain, % 163.01/163.18 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x42501,x42502)))), % 163.01/163.18 inference(scs_inference,[],[19,4234,4240,292,4237,4002,3989,3976,3998,3001,4076,4082,4109,4155,4208,4119,4124,4164,4089,4113,3958,1044,3002,3978,2,1976,1975,713,858,2013,2855,2316,2342,2383,2853,2109,2082,30,895,1896,807,2014,2016,718,1954,2137,2284,1898,71,2366,2525,896,31,795,811,1977,802,1980,1952,800,15,14,3,17,32,16,38,40])). % 163.01/163.18 cnf(4275,plain, % 163.01/163.18 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x42751,f1(f3(a7,a4),f3(a4,a7))),x42752))), % 163.01/163.18 inference(rename_variables,[],[4203])). % 163.01/163.18 cnf(4280,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x42801,x42802),f2(f2(f1(f3(a7,a4),f3(a4,a7)),f2(x42803,x42804)),f2(x42805,x42806))))), % 163.01/163.19 inference(scs_inference,[],[4089,4113,4250,4218,4166,4173,4203,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855])). % 163.01/163.19 cnf(4287,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(a4,a7))), % 163.01/163.19 inference(scs_inference,[],[4089,4113,4250,4218,4248,4166,4173,4181,4203,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30])). % 163.01/163.19 cnf(4289,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x42891,x42892),f2(f1(f3(a7,a4),f3(a4,a7)),x42893)))), % 163.01/163.19 inference(scs_inference,[],[3998,4089,4113,4250,4218,4248,4166,4173,4181,4203,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853])). % 163.01/163.19 cnf(4303,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x43031,f1(f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x43032,x43033)),f2(x43034,x43035))))), % 163.01/163.19 inference(rename_variables,[],[4109])). % 163.01/163.19 cnf(4308,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a4,a7),x43081),f3(f3(a7,a4),x43081)))), % 163.01/163.19 inference(rename_variables,[],[4205])). % 163.01/163.19 cnf(4313,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x43131,f3(a4,a7)),x43132))), % 163.01/163.19 inference(scs_inference,[],[4164,3998,4089,4109,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4205,4203,4275,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71])). % 163.01/163.19 cnf(4315,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(a7,a4))), % 163.01/163.19 inference(scs_inference,[],[4164,3998,4089,4109,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4205,4203,4275,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31])). % 163.01/163.19 cnf(4323,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x43231,f3(a4,a7)),x43232))), % 163.01/163.19 inference(scs_inference,[],[4164,3998,4089,4109,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4243,4205,4203,4275,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31,2366,800,1977,2137])). % 163.01/163.19 cnf(4327,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x43271,x43272)),f1(x43273,x43274)))), % 163.01/163.19 inference(scs_inference,[],[4164,3998,4089,4109,4119,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4243,4205,4203,4275,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31,2366,800,1977,2137,833,1898])). % 163.01/163.19 cnf(4336,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x43361,f1(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(x43362,x43363))))), % 163.01/163.19 inference(scs_inference,[],[4164,3998,4089,4109,4119,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4243,4226,4205,4203,4275,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31,2366,800,1977,2137,833,1898,688,802,811,896])). % 163.01/163.19 cnf(4341,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a4,a7),x43411),f3(f3(a7,a4),x43411)))), % 163.01/163.19 inference(rename_variables,[],[4205])). % 163.01/163.19 cnf(4350,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f3(f3(a7,a4),x43501),f3(f3(a4,a7),x43501)))), % 163.01/163.19 inference(scs_inference,[],[4164,3998,4089,4109,4119,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4243,4226,4205,4308,4341,4203,4275,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31,2366,800,1977,2137,833,1898,688,802,811,896,732,2012,815,821,817,2134])). % 163.01/163.19 cnf(4352,plain, % 163.01/163.19 (E(f1(x43521,x43522),f1(x43522,x43521))), % 163.01/163.19 inference(rename_variables,[],[19])). % 163.01/163.19 cnf(4357,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x43571,x43572)),f2(x43573,x43574)),x43575))), % 163.01/163.19 inference(scs_inference,[],[19,4352,24,317,4164,3998,4089,4109,4303,4119,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4243,4226,4205,4308,4341,4203,4275,3522,1060,266,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31,2366,800,1977,2137,833,1898,688,802,811,896,732,2012,815,821,817,2134,15,14,3,17])). % 163.01/163.19 cnf(4358,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(x43581,f1(f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x43582,x43583)),f2(x43584,x43585))))), % 163.01/163.19 inference(rename_variables,[],[4109])). % 163.01/163.19 cnf(4360,plain, % 163.01/163.19 (P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(f1(x43601,x43602),f1(f3(a7,a4),f3(a4,f2(a4,a7)))))), % 163.01/163.19 inference(scs_inference,[],[19,4352,292,24,317,4164,3998,4089,4109,4303,4119,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4243,4226,4205,4308,4341,4203,4275,3522,1060,266,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31,2366,800,1977,2137,833,1898,688,802,811,896,732,2012,815,821,817,2134,15,14,3,17,16])). % 163.01/163.19 cnf(4362,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(x43621,f2(f1(f3(a4,a7),f3(a7,a4)),f2(x43622,x43623))))), % 163.01/163.19 inference(scs_inference,[],[19,4352,292,24,317,3989,4164,3998,4089,4109,4303,4119,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4243,4226,4205,4308,4341,4210,4203,4275,3522,1060,266,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31,2366,800,1977,2137,833,1898,688,802,811,896,732,2012,815,821,817,2134,15,14,3,17,16,32])). % 163.01/163.19 cnf(4365,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x43651,x43652)),f2(x43653,x43654)))), % 163.01/163.19 inference(scs_inference,[],[19,4352,292,24,317,3989,4164,3998,4089,4109,4303,4358,4119,4113,4250,4246,4207,4188,4218,4248,4166,4173,4181,4243,4226,4205,4308,4341,4210,4203,4275,3522,1060,266,3003,2,1976,1975,2013,2084,2098,1984,2112,2383,2855,1954,2342,895,30,2853,807,2016,718,2109,2082,2525,1896,1952,917,2284,1980,71,31,2366,800,1977,2137,833,1898,688,802,811,896,732,2012,815,821,817,2134,15,14,3,17,16,32,40])). % 163.01/163.19 cnf(4383,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(x43831,f2(f1(f3(a7,a4),f3(a4,a7)),f2(x43832,x43833))))), % 163.01/163.19 inference(scs_inference,[],[4243,3004,2,1976])). % 163.01/163.19 cnf(4386,plain, % 163.01/163.19 (P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x43861,x43862)),f1(x43863,x43864)))), % 163.01/163.19 inference(scs_inference,[],[4243,4327,4287,4280,3004,2,1976,1975,2098,2013])). % 163.01/163.19 cnf(4392,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x43921,f3(a4,a7)),x43922))), % 163.01/163.19 inference(rename_variables,[],[4313])). % 163.01/163.19 cnf(4398,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(a4,f2(a4,a7)))), % 163.01/163.19 inference(scs_inference,[],[4243,4327,4287,4280,4313,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954])). % 163.01/163.19 cnf(4401,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(a4,f2(a4,f2(a4,a7))))), % 163.01/163.19 inference(scs_inference,[],[4243,4327,4287,4280,4313,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016])). % 163.01/163.19 cnf(4402,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(f2(x44021,x44022),f2(f2(f1(f3(a7,a4),f3(a4,a7)),f2(x44023,x44024)),x44025)))), % 163.01/163.19 inference(scs_inference,[],[4243,4327,4287,4280,4313,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853])). % 163.01/163.19 cnf(4404,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(f2(x44041,x44042),f2(f2(f1(f3(a4,a7),f3(a7,a4)),f2(x44043,x44044)),f2(x44045,x44046))))), % 163.01/163.19 inference(scs_inference,[],[4243,4327,4287,4280,4313,4362,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855])). % 163.01/163.19 cnf(4405,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f2(x44051,f2(f1(f3(a4,a7),f3(a7,a4)),f2(x44052,x44053))))), % 163.01/163.19 inference(rename_variables,[],[4362])). % 163.01/163.19 cnf(4416,plain, % 163.01/163.19 (P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(x44161,f1(f3(a4,f2(a4,a7)),f3(a7,a4))))), % 163.01/163.19 inference(rename_variables,[],[4246])). % 163.01/163.19 cnf(4423,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x44231,f3(a4,a7)),x44232))), % 163.01/163.19 inference(rename_variables,[],[4323])). % 163.01/163.19 cnf(4425,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(x44251,x44252)))), % 163.01/163.19 inference(scs_inference,[],[4218,3998,4207,4243,4246,4327,4287,4280,4313,4392,4362,4323,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525])). % 163.01/163.19 cnf(4430,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f3(f3(a7,a4),x44301),f3(f3(a4,a7),x44301)))), % 163.01/163.19 inference(rename_variables,[],[4350])). % 163.01/163.19 cnf(4436,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(a4,f2(f2(a4,a7),a4)))), % 163.01/163.19 inference(scs_inference,[],[4218,3998,4207,4243,4246,4327,4287,4280,4313,4392,4362,4405,4323,4350,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815])). % 163.01/163.19 cnf(4440,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(a7,f2(f2(a7,a4),a7)))), % 163.01/163.19 inference(scs_inference,[],[4218,3998,4207,4243,4246,4327,4287,4315,4280,4313,4392,4362,4405,4323,4350,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802])). % 163.01/163.19 cnf(4444,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x44441,f3(a7,a4)),x44442))), % 163.01/163.19 inference(scs_inference,[],[4218,3998,4207,4243,4246,4327,4360,4287,4315,4280,4313,4392,4362,4405,4323,4350,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137])). % 163.01/163.19 cnf(4446,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f2(x44461,x44462),f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f2(x44463,x44464))),f1(x44465,x44466)))), % 163.01/163.19 inference(scs_inference,[],[4218,3998,4207,4243,4246,4327,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4350,4289,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898])). % 163.01/163.19 cnf(4454,plain, % 163.01/163.19 (P1(f6(f3(x44541,f2(f2(f2(x44541,x44542),x44541),x44541)),x44543),f6(f3(x44541,x44542),x44543))), % 163.01/163.19 inference(scs_inference,[],[317,4218,3998,4207,4243,4246,4327,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4350,4430,4289,1127,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15])). % 163.01/163.19 cnf(4456,plain, % 163.01/163.19 (P1(f1(f3(x44561,f3(x44562,x44563)),f3(x44564,f3(x44562,x44563))),f3(f1(x44561,x44564),f3(x44562,f2(x44562,x44563))))), % 163.01/163.19 inference(scs_inference,[],[48,317,4218,3998,4207,4243,4246,4327,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4350,4430,4289,1127,1173,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15,14])). % 163.01/163.19 cnf(4462,plain, % 163.01/163.19 (E(f3(f1(x44621,x44622),f3(x44623,f2(x44623,x44623))),f1(f3(x44621,f3(x44623,x44623)),f3(x44622,f3(x44623,x44623))))), % 163.01/163.19 inference(scs_inference,[],[48,20,317,4218,3998,4207,4243,3085,3003,4246,4327,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4350,4430,4289,1127,1173,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15,14,3,27])). % 163.01/163.19 cnf(4465,plain, % 163.01/163.19 (P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),x44651))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,317,4218,3998,4207,4243,3085,3003,4246,4416,4327,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4350,4430,4289,1127,1173,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15,14,3,27,17])). % 163.01/163.19 cnf(4470,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f2(x44701,f1(f3(a7,a4),f3(a4,a7))))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,292,317,4218,3998,4207,4243,3085,4203,3003,4246,4416,4327,4365,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4423,4350,4430,4289,1127,1173,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15,14,3,27,17,16,32])). % 163.01/163.19 cnf(4473,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f3(a4,f2(a4,a7)),f3(a7,a4)))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,292,317,4218,4248,3998,4207,4243,3085,4203,3003,4246,4416,4155,4327,4365,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4423,4350,4430,4289,1127,1173,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15,14,3,27,17,16,32,40])). % 163.01/163.19 cnf(4476,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f2(x44761,f1(f3(a4,a7),f3(a7,a4))))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,292,317,4218,4248,3998,4207,4243,3085,4203,3003,4246,4416,4155,4327,4365,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4423,4350,4430,4289,1127,1173,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15,14,3,27,17,16,32,40,713])). % 163.01/163.19 cnf(4482,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(x44821,f1(f3(a4,f2(a4,a7)),f3(a7,a4))),f2(x44822,x44823)),f2(x44824,x44825)))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,292,317,4218,4248,3998,4207,4243,3085,4203,3003,4246,4416,4155,4327,4365,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4423,4350,4430,4289,1127,1173,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15,14,3,27,17,16,32,40,713,2316,833,2718])). % 163.01/163.19 cnf(4492,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(f3(a7,a4),f3(a4,a7)))+~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(x44921,x44922))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,292,317,4218,4248,3998,4207,4243,3085,4203,3003,4246,4416,4155,4327,4365,4357,4360,4287,4315,4280,4313,4392,4362,4405,4323,4423,4350,4430,4289,1127,1173,3004,4228,2,1976,1975,2098,2013,2112,2084,2383,1984,2342,30,1954,858,2016,2853,2855,807,718,790,2109,1896,2082,71,1977,2525,863,917,2366,2731,815,811,802,896,2137,1898,732,817,15,14,3,27,17,16,32,40,713,2316,833,2718,2688,2756,2770,887,38])). % 163.01/163.19 cnf(4509,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(f3(a7,a4),f3(a4,a7)))), % 163.01/163.19 inference(factoring_inference,[],[4492])). % 163.01/163.19 cnf(4520,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x45201,f3(a4,a7)),x45202))), % 163.01/163.19 inference(rename_variables,[],[4323])). % 163.01/163.19 cnf(4525,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(a4,a7))), % 163.01/163.19 inference(scs_inference,[],[4315,4203,4357,4362,4323,4509,4404,4436,4440,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30])). % 163.01/163.19 cnf(4531,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x45311,x45312),f2(f2(f1(f3(a7,a4),f3(a4,a7)),x45313),f2(x45314,x45315))))), % 163.01/163.19 inference(scs_inference,[],[4315,4203,4289,4357,4362,4323,4520,4509,4404,4436,4440,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853])). % 163.01/163.19 cnf(4538,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x45381,x45382),f2(f1(f3(a7,a4),f3(a4,a7)),f2(x45383,x45384))))), % 163.01/163.19 inference(scs_inference,[],[4315,4203,4289,4124,4357,4362,4323,4520,4509,4404,4470,4436,4440,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855])). % 163.01/163.19 cnf(4539,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f2(x45391,f1(f3(a7,a4),f3(a4,a7))))), % 163.01/163.19 inference(rename_variables,[],[4470])). % 163.01/163.19 cnf(4543,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(x45431,f1(f3(a4,f2(a4,a7)),f3(a7,a4))),f2(x45432,x45433)),f1(x45434,x45435)))), % 163.01/163.19 inference(scs_inference,[],[4315,4203,4289,4124,4357,4362,4323,4520,4153,4509,4404,4470,4436,4440,4402,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896])). % 163.01/163.19 cnf(4554,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a7,a4),x45541),f3(f3(a4,a7),x45541)))), % 163.01/163.19 inference(rename_variables,[],[4228])). % 163.01/163.19 cnf(4556,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(f2(x45561,f3(a4,a7)),x45562))), % 163.01/163.19 inference(scs_inference,[],[4287,4315,4203,4289,4124,4357,4362,4323,4520,4228,4425,4153,4509,4383,4404,4470,4444,4436,4440,4402,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896,2718,2366,1977,917,71])). % 163.01/163.19 cnf(4558,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a4,a7),x45581),f3(f3(a7,a4),x45581)))), % 163.01/163.19 inference(scs_inference,[],[4287,4315,4203,4289,4124,4357,4362,4323,4520,4228,4425,4153,4509,4383,4404,4470,4444,4436,4440,4402,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896,2718,2366,1977,917,71,2284])). % 163.01/163.19 cnf(4573,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(a7,a4))), % 163.01/163.19 inference(scs_inference,[],[4287,4315,4203,4289,4124,4357,4362,4323,4520,4228,4554,4425,4153,4222,4509,4383,4404,4470,4444,4436,4401,4440,4402,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896,2718,2366,1977,917,71,2284,2137,815,817,811,732,802,31])). % 163.01/163.19 cnf(4575,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(f1(f3(a4,a7),f3(a7,a4)),x45751))), % 163.01/163.19 inference(scs_inference,[],[4287,4315,4203,4289,4124,4357,4362,4323,4520,4228,4554,4425,4153,4222,4509,4383,4404,4470,4444,4436,4401,4440,4402,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896,2718,2366,1977,917,71,2284,2137,815,817,811,732,802,31,901])). % 163.01/163.19 cnf(4577,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x45771,x45772),f2(f1(f3(a4,a7),f3(a7,a4)),f2(x45773,x45774))))), % 163.01/163.19 inference(scs_inference,[],[4287,4315,4203,4289,4124,4357,4362,4323,4520,4228,4554,4425,4153,4222,4509,4383,4404,4470,4539,4444,4436,4401,4440,4402,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896,2718,2366,1977,917,71,2284,2137,815,817,811,732,802,31,901,2864])). % 163.01/163.19 cnf(4578,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f2(x45781,f1(f3(a7,a4),f3(a4,a7))))), % 163.01/163.19 inference(rename_variables,[],[4470])). % 163.01/163.19 cnf(4597,plain, % 163.01/163.19 (P1(f6(f3(x45971,f2(f2(f2(x45971,x45972),x45971),x45971)),x45973),f6(f3(x45971,x45972),x45973))), % 163.01/163.19 inference(rename_variables,[],[4454])). % 163.01/163.19 cnf(4607,plain, % 163.01/163.19 (P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(f3(a4,f2(a4,a7)),f3(a7,a4)))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,292,401,4287,4315,4203,4246,4289,4155,4124,4357,4362,4323,4520,1173,3004,4228,4554,4386,4425,4446,4473,4153,4222,4509,4383,4404,4470,4539,4578,4476,4444,4436,4401,4440,4402,4454,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896,2718,2366,1977,917,71,2284,2137,815,817,811,732,802,31,901,2864,2012,896,1898,795,2722,747,15,14,3,17,16,40])). % 163.01/163.19 cnf(4610,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(x46101,f3(a4,a7)))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,292,401,4218,4287,4315,4203,4246,4289,4155,4124,4357,4313,4362,4323,4520,1173,3004,4228,4554,4386,4425,4446,4473,4153,4222,4509,4383,4404,4470,4539,4578,4476,4444,4436,4401,4440,4402,4454,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896,2718,2366,1977,917,71,2284,2137,815,817,811,732,802,31,901,2864,2012,896,1898,795,2722,747,15,14,3,17,16,40,32])). % 163.01/163.19 cnf(4624,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a7,a4),f3(a7,a4)),f3(f3(a4,a7),f3(a7,a4))))), % 163.01/163.19 inference(scs_inference,[],[19,48,20,292,401,4218,4287,4315,4203,4246,4289,4155,4124,4357,4313,4362,4323,4520,1173,3004,4228,4554,4386,4425,4446,4473,4153,4222,4509,4383,4404,4470,4539,4578,4476,4444,4436,4401,4440,4402,4454,4597,4462,2,1976,2098,1975,2013,2112,2084,2016,1984,2383,1954,30,2342,718,2853,807,2109,2855,2082,1896,2718,2366,1977,917,71,2284,2137,815,817,811,732,802,31,901,2864,2012,896,1898,795,2722,747,15,14,3,17,16,40,32,858,833,1952,2731,1992,27,1980])). % 163.01/163.19 cnf(4626,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(f3(a7,a4),f3(a4,a7)))), % 163.01/163.19 inference(scs_inference,[],[4509,3005,2,1976])). % 163.01/163.19 cnf(4633,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(x46331,f3(a4,a7)))), % 163.01/163.19 inference(rename_variables,[],[4610])). % 163.01/163.19 cnf(4637,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(f2(x46371,f3(a7,a4)),x46372))), % 163.01/163.19 inference(rename_variables,[],[4444])). % 163.01/163.19 cnf(4639,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x46391,x46392),f2(f2(f1(f3(a7,a4),f3(a4,a7)),f2(x46393,x46394)),x46395)))), % 163.01/163.19 inference(scs_inference,[],[4509,4383,4222,4444,4401,4402,4482,4610,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853])). % 163.01/163.19 cnf(4641,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a7,a4),x46411),f3(f3(a4,a7),x46411)))), % 163.01/163.19 inference(scs_inference,[],[4509,4383,4222,4444,4401,4402,4482,4610,4558,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895])). % 163.01/163.19 cnf(4649,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a4,a7),f3(a7,a4))),f2(f2(x46491,x46492),f2(f3(a4,a7),f2(x46493,x46494))))), % 163.01/163.19 inference(scs_inference,[],[4509,4383,4222,4444,4637,4386,4401,4402,4482,4610,4633,4624,4558,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895,718,30,807,2855])). % 163.01/163.19 cnf(4654,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f3(f1(f3(a7,a4),f3(a4,a7)),x46541))), % 163.01/163.19 inference(scs_inference,[],[4509,4383,4222,4444,4637,4386,4401,4402,4482,4610,4633,4624,4558,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895,718,30,807,2855,2342,2109])). % 163.01/163.19 cnf(4660,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a4,a7),x46601),f3(f3(a7,a4),x46601)))), % 163.01/163.19 inference(rename_variables,[],[4558])). % 163.01/163.19 cnf(4662,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f3(f2(x46621,f3(a7,a4)),x46622))), % 163.01/163.19 inference(scs_inference,[],[4315,4509,4383,4222,4444,4637,4386,4401,4402,4482,4610,4633,4538,4624,4558,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895,718,30,807,2855,2342,2109,1980,2082,917,2137])). % 163.01/163.19 cnf(4664,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f1(f3(f3(a4,a7),x46641),f3(f3(a7,a4),x46641)))), % 163.01/163.19 inference(scs_inference,[],[4315,4509,4383,4222,4444,4637,4386,4401,4402,4482,4610,4633,4538,4624,4558,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895,718,30,807,2855,2342,2109,1980,2082,917,2137,2284])). % 163.01/163.19 cnf(4667,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a4,a7),x46671),f3(f3(a7,a4),x46671)))), % 163.01/163.19 inference(rename_variables,[],[4558])). % 163.01/163.19 cnf(4674,plain, % 163.01/163.19 (P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f1(f1(f1(f2(x46741,x46742),f1(f3(a4,f2(a4,a7)),f3(a7,a4))),f1(x46743,x46744)),f1(x46745,x46746)))), % 163.01/163.19 inference(scs_inference,[],[4315,4509,4383,4222,4444,4637,4386,4401,4440,4402,4482,4194,4610,4633,4538,4556,4624,4558,4660,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895,718,30,807,2855,2342,2109,1980,2082,917,2137,2284,817,811,1977,1896])). % 163.01/163.19 cnf(4700,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f3(f1(f3(a4,a7),f3(a7,a4)),f2(f3(a4,a7),x47001)))), % 163.01/163.19 inference(scs_inference,[],[4315,4509,4383,4222,4444,4637,4386,4401,4440,4402,4482,4607,4194,4525,4610,4633,4531,4538,4556,4575,4577,4624,4558,4660,4667,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895,718,30,807,2855,2342,2109,1980,2082,917,2137,2284,817,811,1977,1896,71,31,1952,2366,901,2012,732,802,896,795,821,907])). % 163.01/163.19 cnf(4705,plain, % 163.01/163.19 (E(f1(x47051,x47052),f1(x47052,x47051))), % 163.01/163.19 inference(rename_variables,[],[19])). % 163.01/163.19 cnf(4706,plain, % 163.01/163.19 (E(f1(f3(x47061,f3(x47062,f2(x47063,x47062))),f3(x47064,f3(x47062,f2(x47063,x47062)))),f3(f1(x47064,x47061),f3(x47062,x47063)))), % 163.01/163.19 inference(scs_inference,[],[19,53,317,4315,4509,4383,4222,4444,4637,4386,4401,4440,4402,4482,4607,4194,4525,4610,4633,4531,4538,4556,4575,4577,4624,4558,4660,4667,1161,4456,448,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895,718,30,807,2855,2342,2109,1980,2082,917,2137,2284,817,811,1977,1896,71,31,1952,2366,901,2012,732,802,896,795,821,907,15,14,3])). % 163.01/163.19 cnf(4720,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f3(a4,f2(a4,a7)))), % 163.01/163.19 inference(scs_inference,[],[19,4705,53,292,317,4315,4509,4323,4383,4153,4222,4444,4637,4386,4360,4401,4440,4402,4482,4543,4607,4194,4525,4610,4633,4531,4538,4556,4575,4577,4624,4558,4660,4667,1161,4456,448,3005,2,1976,1975,2013,2098,2084,2016,2383,1954,1984,2853,895,718,30,807,2855,2342,2109,1980,2082,917,2137,2284,817,811,1977,1896,71,31,1952,2366,901,2012,732,802,896,795,821,907,15,14,3,17,16,40,32,2112])). % 163.01/163.19 cnf(4746,plain, % 163.01/163.19 (~P2(f5(f1(f3(a4,f2(a4,a7)),f3(a7,a4)),f1(f3(a7,a4),f3(a4,a7))),f3(f2(x47461,f3(a4,a7)),x47462))), % 163.01/163.19 inference(rename_variables,[],[4556])). % 163.01/163.19 cnf(4758,plain, % 163.01/163.19 (~P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a4,a7),f3(a7,a4))),f1(f3(f3(a7,a4),x47581),f3(f3(a4,a7),x47581)))), % 163.01/163.19 inference(rename_variables,[],[4641])). % 163.01/163.19 cnf(4807,plain, % 163.01/163.19 (E(f5(f1(x48071,x48072),x48073),f5(f1(x48072,x48071),x48073))), % 163.01/163.19 inference(rename_variables,[],[292])). % 163.01/163.19 cnf(4813,plain, % 163.01/163.19 (P2(f5(f1(f3(a7,a4),f3(a4,f2(a4,a7))),f1(f3(a7,a4),f3(a4,a7))),f3(a4,f2(a4,a7)))), % 163.01/163.19 inference(scs_inference,[],[19,20,292,4807,317,4222,4289,4362,4194,4525,4610,4556,4746,3005,4607,4538,4577,4674,4336,4573,4626,4720,4649,4654,4700,4641,4758,4664,4662,4639,1191,1186,4706,4465,2,1976,1975,2098,2112,2013,2084,1954,2016,2383,2853,2855,1984,895,858,807,30,917,718,2342,2109,2082,1952,31,1977,2137,71,817,815,1896,2366,811,802,732,901,1898,15,14,3,17,16,40])). % 163.01/163.19 cnf(4904,plain, % 163.01/163.19 ($false), % 163.01/163.19 inference(scs_inference,[],[4573,4538,4649,4813,3008,4398,2,1976,1975,2098,2013]), % 163.01/163.19 ['proof']). % 163.01/163.19 % SZS output end Proof % 163.01/163.19 % Total time :162.190000s %------------------------------------------------------------------------------