%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET918+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 14:22:59 EDT 2024 % Result : Theorem 127.73s 127.77s % Output : CNFRefutation 127.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET918+1 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n022.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 16:13:53 EDT 2024 % 0.11/0.33 % CPUTime : % 0.52/0.59 start to proof:theBenchmark % 127.73/127.75 %------------------------------------------- % 127.73/127.75 % File :CSE---1.7 % 127.73/127.75 % Problem :theBenchmark % 127.73/127.75 % Transform :cnf % 127.73/127.75 % Format :tptp:raw % 127.73/127.75 % Command :java -jar mcs_scs.jar %d %s % 127.73/127.75 % 127.73/127.75 % Result :Theorem 127.110000s % 127.73/127.75 % Output :CNFRefutation 127.110000s % 127.73/127.75 %------------------------------------------- % 127.73/127.77 %------------------------------------------------------------------------------ % 127.73/127.77 % File : SET918+1 : TPTP v8.2.0. Released v3.2.0. % 127.73/127.77 % Domain : Set theory % 127.73/127.77 % Problem : ~ ( intersection(uno_pair(A,B),C) = sgtn(A) & in(B,C) & A != B ) % 127.73/127.77 % Version : [Urb06] axioms : Especial. % 127.73/127.77 % English : % 127.73/127.77 % 127.73/127.77 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 127.73/127.77 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 127.73/127.77 % Source : [Urb06] % 127.73/127.77 % Names : zfmisc_1__t59_zfmisc_1 [Urb06] % 127.73/127.77 % 127.73/127.77 % Status : Theorem % 127.73/127.77 % Rating : 0.19 v7.5.0, 0.22 v7.4.0, 0.13 v7.3.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.10 v6.4.0, 0.19 v6.3.0, 0.21 v6.2.0, 0.36 v6.1.0, 0.43 v6.0.0, 0.30 v5.5.0, 0.26 v5.4.0, 0.29 v5.3.0, 0.37 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.25 v4.1.0, 0.26 v4.0.1, 0.30 v4.0.0, 0.29 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.37 v3.3.0, 0.36 v3.2.0 % 127.73/127.77 % Syntax : Number of formulae : 10 ( 5 unt; 0 def) % 127.73/127.77 % Number of atoms : 21 ( 11 equ) % 127.73/127.77 % Maximal formula atoms : 4 ( 2 avg) % 127.73/127.77 % Number of connectives : 15 ( 4 ~; 1 |; 3 &) % 127.73/127.77 % ( 6 <=>; 1 =>; 0 <=; 0 <~>) % 127.73/127.77 % Maximal formula depth : 8 ( 5 avg) % 127.73/127.77 % Maximal term depth : 3 ( 1 avg) % 127.73/127.77 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 127.73/127.77 % Number of functors : 3 ( 3 usr; 0 con; 1-2 aty) % 127.73/127.77 % Number of variables : 24 ( 22 !; 2 ?) % 127.73/127.77 % SPC : FOF_THM_RFO_SEQ % 127.73/127.77 % 127.73/127.77 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 127.73/127.77 % library, www.mizar.org % 127.73/127.77 %------------------------------------------------------------------------------ % 127.73/127.77 fof(antisymmetry_r2_hidden,axiom, % 127.73/127.77 ! [A,B] : % 127.73/127.77 ( in(A,B) % 127.73/127.77 => ~ in(B,A) ) ). % 127.73/127.77 % 127.73/127.77 fof(commutativity_k2_tarski,axiom, % 127.73/127.77 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 127.73/127.77 % 127.73/127.77 fof(commutativity_k3_xboole_0,axiom, % 127.73/127.77 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 127.73/127.77 % 127.73/127.77 fof(d1_tarski,axiom, % 127.73/127.77 ! [A,B] : % 127.73/127.77 ( B = singleton(A) % 127.73/127.77 <=> ! [C] : % 127.73/127.77 ( in(C,B) % 127.73/127.77 <=> C = A ) ) ). % 127.73/127.77 % 127.73/127.77 fof(d2_tarski,axiom, % 127.73/127.77 ! [A,B,C] : % 127.73/127.77 ( C = unordered_pair(A,B) % 127.73/127.77 <=> ! [D] : % 127.73/127.77 ( in(D,C) % 127.73/127.77 <=> ( D = A % 127.73/127.77 | D = B ) ) ) ). % 127.73/127.77 % 127.73/127.77 fof(d3_xboole_0,axiom, % 127.73/127.77 ! [A,B,C] : % 127.73/127.77 ( C = set_intersection2(A,B) % 127.73/127.77 <=> ! [D] : % 127.73/127.77 ( in(D,C) % 127.73/127.77 <=> ( in(D,A) % 127.73/127.77 & in(D,B) ) ) ) ). % 127.73/127.77 % 127.73/127.77 fof(idempotence_k3_xboole_0,axiom, % 127.73/127.77 ! [A,B] : set_intersection2(A,A) = A ). % 127.73/127.77 % 127.73/127.77 fof(rc1_xboole_0,axiom, % 127.73/127.77 ? [A] : empty(A) ). % 127.73/127.77 % 127.73/127.77 fof(rc2_xboole_0,axiom, % 127.73/127.77 ? [A] : ~ empty(A) ). % 127.73/127.77 % 127.73/127.77 fof(t59_zfmisc_1,conjecture, % 127.73/127.77 ! [A,B,C] : % 127.73/127.77 ~ ( set_intersection2(unordered_pair(A,B),C) = singleton(A) % 127.73/127.77 & in(B,C) % 127.73/127.77 & A != B ) ). % 127.73/127.77 % 127.73/127.77 %------------------------------------------------------------------------------ % 127.73/127.77 %------------------------------------------- % 127.73/127.77 % Proof found % 127.73/127.77 % SZS status Theorem for theBenchmark % 127.73/127.77 % SZS output start Proof % 127.73/127.78 %ClaNum:44(EqnAxiom:19) % 127.73/127.78 %VarNum:163(SingletonVarNum:59) % 127.73/127.78 %MaxLitNum:4 % 127.73/127.78 %MaxfuncDepth:2 % 127.73/127.78 %SharedTerms:13 % 127.73/127.78 %goalClause: 21 25 26 % 127.73/127.78 %singleGoalClaCount:3 % 127.73/127.78 [20]P1(a1) % 127.73/127.78 [21]P2(a5,a8) % 127.73/127.78 [26]~E(a6,a5) % 127.73/127.78 [27]~P1(a7) % 127.73/127.78 [25]E(f9(f10(a6,a5),a8),f11(a6)) % 127.73/127.78 [22]E(f9(x221,x221),x221) % 127.73/127.78 [23]E(f10(x231,x232),f10(x232,x231)) % 127.73/127.78 [24]E(f9(x241,x242),f9(x242,x241)) % 127.73/127.78 [32]~P2(x322,x321)+~P2(x321,x322) % 127.73/127.78 [34]E(f2(x342,x341),x342)+P2(f2(x342,x341),x341)+E(x341,f11(x342)) % 127.73/127.78 [38]~E(f2(x382,x381),x382)+~P2(f2(x382,x381),x381)+E(x381,f11(x382)) % 127.73/127.78 [28]P2(x281,x282)+~E(x281,x283)+~E(x282,f11(x283)) % 127.73/127.78 [29]~P2(x291,x293)+E(x291,x292)+~E(x293,f11(x292)) % 127.73/127.78 [40]P2(f4(x402,x403,x401),x401)+P2(f4(x402,x403,x401),x403)+E(x401,f9(x402,x403)) % 127.73/127.78 [41]P2(f4(x412,x413,x411),x411)+P2(f4(x412,x413,x411),x412)+E(x411,f9(x412,x413)) % 127.73/127.78 [42]~E(f3(x422,x423,x421),x423)+~P2(f3(x422,x423,x421),x421)+E(x421,f10(x422,x423)) % 127.73/127.78 [43]~E(f3(x432,x433,x431),x432)+~P2(f3(x432,x433,x431),x431)+E(x431,f10(x432,x433)) % 127.73/127.78 [30]P2(x301,x302)+~E(x301,x303)+~E(x302,f10(x304,x303)) % 127.73/127.78 [31]P2(x311,x312)+~E(x311,x313)+~E(x312,f10(x313,x314)) % 127.73/127.79 [35]~P2(x351,x353)+P2(x351,x352)+~E(x353,f9(x354,x352)) % 127.73/127.79 [36]~P2(x361,x363)+P2(x361,x362)+~E(x363,f9(x362,x364)) % 127.73/127.79 [39]E(f3(x392,x393,x391),x393)+E(f3(x392,x393,x391),x392)+P2(f3(x392,x393,x391),x391)+E(x391,f10(x392,x393)) % 127.73/127.79 [44]~P2(f4(x442,x443,x441),x441)+~P2(f4(x442,x443,x441),x443)+~P2(f4(x442,x443,x441),x442)+E(x441,f9(x442,x443)) % 127.73/127.79 [33]~P2(x331,x334)+E(x331,x332)+E(x331,x333)+~E(x334,f10(x333,x332)) % 127.73/127.79 [37]~P2(x371,x374)+~P2(x371,x373)+P2(x371,x372)+~E(x372,f9(x373,x374)) % 127.73/127.79 %EqnAxiom % 127.73/127.79 [1]E(x11,x11) % 127.73/127.79 [2]E(x22,x21)+~E(x21,x22) % 127.73/127.79 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 127.73/127.79 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43)) % 127.73/127.79 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52)) % 127.73/127.79 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63)) % 127.73/127.79 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72)) % 127.73/127.79 [8]~E(x81,x82)+E(f4(x81,x83,x84),f4(x82,x83,x84)) % 127.73/127.79 [9]~E(x91,x92)+E(f4(x93,x91,x94),f4(x93,x92,x94)) % 127.73/127.79 [10]~E(x101,x102)+E(f4(x103,x104,x101),f4(x103,x104,x102)) % 127.73/127.79 [11]~E(x111,x112)+E(f3(x111,x113,x114),f3(x112,x113,x114)) % 127.73/127.79 [12]~E(x121,x122)+E(f3(x123,x121,x124),f3(x123,x122,x124)) % 127.73/127.79 [13]~E(x131,x132)+E(f3(x133,x134,x131),f3(x133,x134,x132)) % 127.73/127.79 [14]~E(x141,x142)+E(f2(x141,x143),f2(x142,x143)) % 127.73/127.79 [15]~E(x151,x152)+E(f2(x153,x151),f2(x153,x152)) % 127.73/127.79 [16]~E(x161,x162)+E(f11(x161),f11(x162)) % 127.73/127.79 [17]~P1(x171)+P1(x172)+~E(x171,x172) % 127.73/127.79 [18]P2(x182,x183)+~E(x181,x182)+~P2(x181,x183) % 127.73/127.79 [19]P2(x193,x192)+~E(x191,x192)+~P2(x193,x191) % 127.73/127.79 % 127.73/127.79 %------------------------------------------- % 127.83/127.80 cnf(45,plain, % 127.83/127.80 (~P2(x451,f11(x452))+E(x451,x452)), % 127.83/127.80 inference(equality_inference,[],[29])). % 127.83/127.80 cnf(46,plain, % 127.83/127.80 (~P2(x461,f10(x462,x463))+E(x461,x463)+E(x461,x462)), % 127.83/127.80 inference(equality_inference,[],[33])). % 127.83/127.80 cnf(47,plain, % 127.83/127.80 (~P2(x471,f9(x472,x473))+P2(x471,x473)), % 127.83/127.80 inference(equality_inference,[],[35])). % 127.83/127.80 cnf(48,plain, % 127.83/127.80 (~P2(x481,f9(x482,x483))+P2(x481,x482)), % 127.83/127.80 inference(equality_inference,[],[36])). % 127.83/127.80 cnf(49,plain, % 127.83/127.80 (~P2(x491,x492)+~P2(x491,x493)+P2(x491,f9(x493,x492))), % 127.83/127.80 inference(equality_inference,[],[37])). % 127.83/127.80 cnf(50,plain, % 127.83/127.80 (~P2(a8,a5)), % 127.83/127.81 inference(scs_inference,[],[21,32])). % 127.83/127.81 cnf(52,plain, % 127.83/127.81 (~P2(a6,f11(a5))), % 127.83/127.81 inference(scs_inference,[],[21,26,32,45])). % 127.83/127.81 cnf(54,plain, % 127.83/127.81 (~P2(a8,f9(x541,a5))), % 127.83/127.81 inference(scs_inference,[],[21,26,32,45,47])). % 127.83/127.81 cnf(56,plain, % 127.83/127.81 (~P2(a8,f9(a5,x561))), % 127.83/127.81 inference(scs_inference,[],[21,26,32,45,47,48])). % 127.83/127.81 cnf(58,plain, % 127.83/127.81 (E(f11(a6),f9(f10(a6,a5),a8))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,32,45,47,48,2])). % 127.83/127.81 cnf(59,plain, % 127.83/127.81 (P2(f9(a6,a6),f9(f10(a6,a5),a8))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,32,45,47,48,2,28])). % 127.83/127.81 cnf(60,plain, % 127.83/127.81 (E(f9(x601,x601),x601)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(63,plain, % 127.83/127.81 (E(f9(x631,x631),x631)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(65,plain, % 127.83/127.81 (P2(f9(f10(a6,a5),a8),f10(f11(a6),x651))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,23,32,45,47,48,2,28,29,30])). % 127.83/127.81 cnf(66,plain, % 127.83/127.81 (E(f10(x661,x662),f10(x662,x661))), % 127.83/127.81 inference(rename_variables,[],[23])). % 127.83/127.81 cnf(68,plain, % 127.83/127.81 (P2(f9(f10(a6,a5),a8),f10(x681,f11(a6)))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,23,66,32,45,47,48,2,28,29,30,31])). % 127.83/127.81 cnf(72,plain, % 127.83/127.81 (E(f9(x721,x721),x721)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(75,plain, % 127.83/127.81 (E(f9(x751,x751),x751)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(77,plain, % 127.83/127.81 (~P2(a6,f10(a5,a5))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,63,72,23,66,32,45,47,48,2,28,29,30,31,35,36,46])). % 127.83/127.81 cnf(79,plain, % 127.83/127.81 (~E(a6,f9(a5,a5))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,63,72,75,23,66,32,45,47,48,2,28,29,30,31,35,36,46,3])). % 127.83/127.81 cnf(80,plain, % 127.83/127.81 (E(f9(x801,x801),x801)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(81,plain, % 127.83/127.81 (~P1(f9(a7,a7))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,63,72,75,80,23,66,27,32,45,47,48,2,28,29,30,31,35,36,46,3,17])). % 127.83/127.81 cnf(82,plain, % 127.83/127.81 (E(f9(x821,x821),x821)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(83,plain, % 127.83/127.81 (P2(a6,f9(f10(a6,a5),a8))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,63,72,75,80,82,23,66,27,32,45,47,48,2,28,29,30,31,35,36,46,3,17,18])). % 127.83/127.81 cnf(84,plain, % 127.83/127.81 (E(f9(x841,x841),x841)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(85,plain, % 127.83/127.81 (P2(f9(a6,a6),f11(a6))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,63,72,75,80,82,23,66,27,32,45,47,48,2,28,29,30,31,35,36,46,3,17,18,19])). % 127.83/127.81 cnf(86,plain, % 127.83/127.81 (~P2(a6,f9(f10(a5,a5),f10(a5,a5)))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,63,72,75,80,82,84,23,66,27,32,45,47,48,2,28,29,30,31,35,36,46,3,17,18,19,33])). % 127.83/127.81 cnf(87,plain, % 127.83/127.81 (E(f9(x871,x871),x871)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(89,plain, % 127.83/127.81 (P2(a5,f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.81 inference(scs_inference,[],[21,26,25,22,60,63,72,75,80,82,84,87,23,66,27,32,45,47,48,2,28,29,30,31,35,36,46,3,17,18,19,33,37])). % 127.83/127.81 cnf(97,plain, % 127.83/127.81 (~P2(a6,f9(x971,f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[52,47])). % 127.83/127.81 cnf(99,plain, % 127.83/127.81 (~P2(a6,f11(f9(a5,a5)))), % 127.83/127.81 inference(scs_inference,[],[52,79,47,45])). % 127.83/127.81 cnf(101,plain, % 127.83/127.81 (~P2(a6,f9(f11(a5),x1011))), % 127.83/127.81 inference(scs_inference,[],[52,79,47,45,48])). % 127.83/127.81 cnf(103,plain, % 127.83/127.81 (~P2(f10(f11(a6),x1031),f9(f10(a6,a5),a8))), % 127.83/127.81 inference(scs_inference,[],[52,65,79,47,45,48,32])). % 127.83/127.81 cnf(105,plain, % 127.83/127.81 (E(x1051,f9(x1051,x1051))), % 127.83/127.81 inference(scs_inference,[],[52,65,79,22,47,45,48,32,2])). % 127.83/127.81 cnf(106,plain, % 127.83/127.81 (~E(f10(f11(a6),x1061),a6)), % 127.83/127.81 inference(scs_inference,[],[25,52,65,79,22,47,45,48,32,2,28])). % 127.83/127.81 cnf(108,plain, % 127.83/127.81 (~P2(a6,f10(f9(a5,a5),f9(a5,a5)))), % 127.83/127.81 inference(scs_inference,[],[25,52,65,79,22,47,45,48,32,2,28,46])). % 127.83/127.81 cnf(110,plain, % 127.83/127.81 (P2(f9(a6,a6),f10(a6,a5))), % 127.83/127.81 inference(scs_inference,[],[25,52,65,85,58,79,22,47,45,48,32,2,28,46,36])). % 127.83/127.81 cnf(112,plain, % 127.83/127.81 (P2(f9(a6,a6),a8)), % 127.83/127.81 inference(scs_inference,[],[25,52,65,85,58,79,22,47,45,48,32,2,28,46,36,35])). % 127.83/127.81 cnf(114,plain, % 127.83/127.81 (P2(f9(a5,a5),a8)), % 127.83/127.81 inference(scs_inference,[],[21,25,52,65,85,58,79,22,47,45,48,32,2,28,46,36,35,18])). % 127.83/127.81 cnf(115,plain, % 127.83/127.81 (~E(f9(f10(a6,a5),a8),f11(a5))), % 127.83/127.81 inference(scs_inference,[],[21,25,52,65,85,58,83,79,22,47,45,48,32,2,28,46,36,35,18,19])). % 127.83/127.81 cnf(116,plain, % 127.83/127.81 (P2(a5,f9(a8,a8))), % 127.83/127.81 inference(scs_inference,[],[21,25,52,65,85,58,83,79,24,22,47,45,48,32,2,28,46,36,35,18,19,37])). % 127.83/127.81 cnf(130,plain, % 127.83/127.81 (~P2(f9(f10(a6,a5),a8),f9(a6,a6))), % 127.83/127.81 inference(scs_inference,[],[54,59,115,48,47,45,32])). % 127.83/127.81 cnf(132,plain, % 127.83/127.81 (~P2(f9(f10(a6,a5),a8),f10(f11(a5),f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[54,59,115,48,47,45,32,46])). % 127.83/127.81 cnf(134,plain, % 127.83/127.81 (~P2(f9(f10(a6,a5),a8),a6)), % 127.83/127.81 inference(scs_inference,[],[54,59,115,48,47,45,32,46,49])). % 127.83/127.81 cnf(136,plain, % 127.83/127.81 (~E(f9(a6,a6),f10(f11(a6),x1361))), % 127.83/127.81 inference(scs_inference,[],[103,54,59,115,48,47,45,32,46,49,18])). % 127.83/127.81 cnf(137,plain, % 127.83/127.81 (P1(f9(a1,a1))), % 127.83/127.81 inference(scs_inference,[],[103,54,105,59,115,20,48,47,45,32,46,49,18,17])). % 127.83/127.81 cnf(162,plain, % 127.83/127.81 (~P2(f10(a6,a5),f9(a6,a6))), % 127.83/127.81 inference(scs_inference,[],[130,110,106,45,47,48,32])). % 127.83/127.81 cnf(166,plain, % 127.83/127.81 (~P2(f10(a6,a5),a6)), % 127.83/127.81 inference(scs_inference,[],[130,110,106,45,47,48,32,46,49])). % 127.83/127.81 cnf(170,plain, % 127.83/127.81 (P1(f9(f9(a1,a1),f9(a1,a1)))), % 127.83/127.81 inference(scs_inference,[],[130,110,136,137,106,105,23,45,47,48,32,46,49,3,17])). % 127.83/127.81 cnf(171,plain, % 127.83/127.81 (E(x1711,f9(x1711,x1711))), % 127.83/127.81 inference(rename_variables,[],[105])). % 127.83/127.81 cnf(172,plain, % 127.83/127.81 (P2(f9(a6,a6),f9(f10(a6,a5),f10(a6,a5)))), % 127.83/127.81 inference(scs_inference,[],[130,110,136,137,106,105,171,23,45,47,48,32,46,49,3,17,19])). % 127.83/127.81 cnf(173,plain, % 127.83/127.81 (E(x1731,f9(x1731,x1731))), % 127.83/127.81 inference(rename_variables,[],[105])). % 127.83/127.81 cnf(174,plain, % 127.83/127.81 (P2(f9(f9(a6,a6),f9(a6,a6)),f10(a6,a5))), % 127.83/127.81 inference(scs_inference,[],[130,110,136,137,106,105,171,173,23,45,47,48,32,46,49,3,17,19,18])). % 127.83/127.81 cnf(185,plain, % 127.83/127.81 (~P2(f9(a8,a8),a5)), % 127.83/127.81 inference(scs_inference,[],[162,116,48,47,32])). % 127.83/127.81 cnf(187,plain, % 127.83/127.81 (P2(f9(a6,a6),f9(a8,a8))), % 127.83/127.81 inference(scs_inference,[],[162,116,112,105,48,47,32,19])). % 127.83/127.81 cnf(188,plain, % 127.83/127.81 (E(x1881,f9(x1881,x1881))), % 127.83/127.81 inference(rename_variables,[],[105])). % 127.83/127.81 cnf(189,plain, % 127.83/127.81 (P2(f9(a5,a5),f9(a8,a8))), % 127.83/127.81 inference(scs_inference,[],[162,116,112,105,188,48,47,32,19,18])). % 127.83/127.81 cnf(199,plain, % 127.83/127.81 (~P2(f9(a8,a8),f9(x1991,a5))), % 127.83/127.81 inference(scs_inference,[],[185,47])). % 127.83/127.81 cnf(201,plain, % 127.83/127.81 (~P2(f9(a8,a8),f9(a5,x2011))), % 127.83/127.81 inference(scs_inference,[],[185,47,48])). % 127.83/127.81 cnf(203,plain, % 127.83/127.81 (~P2(f9(f9(a8,a8),f9(a8,a8)),a5)), % 127.83/127.81 inference(scs_inference,[],[185,89,47,48,32])). % 127.83/127.81 cnf(206,plain, % 127.83/127.81 (E(x2061,f9(x2061,x2061))), % 127.83/127.81 inference(rename_variables,[],[105])). % 127.83/127.81 cnf(207,plain, % 127.83/127.81 (P2(f9(f9(a5,a5),f9(a5,a5)),f9(a8,a8))), % 127.83/127.81 inference(scs_inference,[],[185,189,89,105,206,47,48,32,19,18])). % 127.83/127.81 cnf(213,plain, % 127.83/127.81 (~P2(f9(f9(a8,a8),f9(a8,a8)),f9(a5,x2131))), % 127.83/127.81 inference(scs_inference,[],[203,48])). % 127.83/127.81 cnf(217,plain, % 127.83/127.81 (~P2(f9(f9(a8,a8),f9(a8,a8)),f9(x2171,a5))), % 127.83/127.81 inference(scs_inference,[],[203,207,48,32,47])). % 127.83/127.81 cnf(222,plain, % 127.83/127.81 (P2(f9(f9(a5,a5),f9(a5,a5)),f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.81 inference(scs_inference,[],[203,207,105,24,48,32,47,36,19])). % 127.83/127.81 cnf(223,plain, % 127.83/127.81 (E(x2231,f9(x2231,x2231))), % 127.83/127.81 inference(rename_variables,[],[105])). % 127.83/127.81 cnf(224,plain, % 127.83/127.81 (P2(f9(f9(a6,a6),f9(a6,a6)),f9(a8,a8))), % 127.83/127.81 inference(scs_inference,[],[203,207,187,105,223,24,48,32,47,36,19,18])). % 127.83/127.81 cnf(230,plain, % 127.83/127.81 (~P2(a5,f10(a6,a5))+P2(a5,f11(a6))), % 127.83/127.81 inference(scs_inference,[],[21,203,58,136,207,187,174,105,223,24,23,48,32,47,36,19,18,17,33,39,37])). % 127.83/127.81 cnf(238,plain, % 127.83/127.81 (P2(f9(f9(a6,a6),f9(a6,a6)),f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.81 inference(scs_inference,[],[56,222,224,105,47,32,48,19])). % 127.83/127.81 cnf(239,plain, % 127.83/127.81 (E(x2391,f9(x2391,x2391))), % 127.83/127.81 inference(rename_variables,[],[105])). % 127.83/127.81 cnf(240,plain, % 127.83/127.81 (P2(f9(f9(a6,a6),f9(a6,a6)),f9(f10(a6,a5),f10(a6,a5)))), % 127.83/127.81 inference(scs_inference,[],[56,222,224,172,105,239,47,32,48,19,18])). % 127.83/127.81 cnf(244,plain, % 127.83/127.81 (~P2(f9(a8,a8),f9(f9(x2441,a5),x2442))), % 127.83/127.81 inference(scs_inference,[],[199,48])). % 127.83/127.81 cnf(250,plain, % 127.83/127.81 (~P2(f9(f9(a8,a8),f9(a8,a8)),f9(a6,a6))), % 127.83/127.81 inference(scs_inference,[],[199,238,48,32,47,49])). % 127.83/127.81 cnf(252,plain, % 127.83/127.81 (P2(f9(a6,a6),f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.81 inference(scs_inference,[],[199,238,187,105,48,32,47,49,19])). % 127.83/127.81 cnf(253,plain, % 127.83/127.81 (E(x2531,f9(x2531,x2531))), % 127.83/127.81 inference(rename_variables,[],[105])). % 127.83/127.81 cnf(254,plain, % 127.83/127.81 (P2(f9(f9(a6,a6),f9(a6,a6)),a8)), % 127.83/127.81 inference(scs_inference,[],[199,238,112,187,105,253,48,32,47,49,19,18])). % 127.83/127.81 cnf(260,plain, % 127.83/127.81 (~P2(f9(f10(a6,a5),f10(a6,a5)),f9(f9(a6,a6),f9(a6,a6)))), % 127.83/127.81 inference(scs_inference,[],[201,240,47,32])). % 127.83/127.81 cnf(267,plain, % 127.83/127.81 (P2(f11(a6),f10(f11(a6),x2671))), % 127.83/127.81 inference(scs_inference,[],[25,130,201,250,240,65,47,32,48,49,19,18])). % 127.83/127.81 cnf(277,plain, % 127.83/127.81 (~P2(a8,f9(f9(a6,a6),f9(a6,a6)))), % 127.83/127.81 inference(scs_inference,[],[213,254,48,47,32])). % 127.83/127.81 cnf(281,plain, % 127.83/127.81 (~E(f9(f10(a6,a5),a8),f9(f10(a5,a5),f10(a5,a5)))), % 127.83/127.81 inference(scs_inference,[],[260,213,86,254,83,48,47,32,49,19])). % 127.83/127.81 cnf(282,plain, % 127.83/127.81 (~E(a6,f10(f11(a6),x2821))), % 127.83/127.81 inference(scs_inference,[],[103,260,213,86,254,83,48,47,32,49,19,18])). % 127.83/127.81 cnf(293,plain, % 127.83/127.81 (~P2(f9(a8,a8),f9(f9(a6,a6),f9(a6,a6)))), % 127.83/127.81 inference(scs_inference,[],[224,32])). % 127.83/127.81 cnf(299,plain, % 127.83/127.81 (~P2(a8,f9(a6,a6))), % 127.83/127.81 inference(scs_inference,[],[277,217,224,32,47,48,49])). % 127.83/127.81 cnf(302,plain, % 127.83/127.81 (P2(f11(a6),f10(x3021,f11(a6)))), % 127.83/127.81 inference(scs_inference,[],[25,130,277,217,224,68,32,47,48,49,19,18])). % 127.83/127.81 cnf(312,plain, % 127.83/127.81 (~P2(f10(x3121,f11(a6)),f11(a6))), % 127.83/127.81 inference(scs_inference,[],[134,302,48,32])). % 127.83/127.81 cnf(316,plain, % 127.83/127.81 (~P2(f9(a8,a8),f9(a6,a6))), % 127.83/127.81 inference(scs_inference,[],[293,134,302,48,32,47,49])). % 127.83/127.81 cnf(318,plain, % 127.83/127.81 (~E(f9(f10(a6,a5),a8),f9(f11(a5),x3181))), % 127.83/127.81 inference(scs_inference,[],[293,101,134,302,83,48,32,47,49,19])). % 127.83/127.81 cnf(320,plain, % 127.83/127.81 (~P2(f10(a6,a5),f11(f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[293,101,134,302,83,48,32,47,49,19,4,45])). % 127.83/127.81 cnf(322,plain, % 127.83/127.81 (~P2(f10(a6,a5),f10(f11(a5),f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[293,101,134,302,83,48,32,47,49,19,4,45,46])). % 127.83/127.81 cnf(335,plain, % 127.83/127.81 (~P2(f9(a8,a8),a6)), % 127.83/127.81 inference(scs_inference,[],[312,68,316,47,32,48,49])). % 127.83/127.81 cnf(348,plain, % 127.83/127.81 (~P2(f11(a6),f9(a6,a6))), % 127.83/127.81 inference(scs_inference,[],[85,166,48,47,32])). % 127.83/127.81 cnf(359,plain, % 127.83/127.81 (~P2(f11(a6),a6)), % 127.83/127.81 inference(scs_inference,[],[348,48,47,49])). % 127.83/127.81 cnf(364,plain, % 127.83/127.81 (E(f11(f11(a6)),f11(f9(f10(a6,a5),a8)))), % 127.83/127.81 inference(scs_inference,[],[25,16,2])). % 127.83/127.81 cnf(369,plain, % 127.83/127.81 (~P2(a8,a6)), % 127.83/127.81 inference(scs_inference,[],[299,47,48,49])). % 127.83/127.81 cnf(383,plain, % 127.83/127.81 (~P2(f11(a6),f9(x3831,a6))), % 127.83/127.81 inference(scs_inference,[],[359,47])). % 127.83/127.81 cnf(439,plain, % 127.83/127.81 (~P2(a8,f9(x4391,a6))), % 127.83/127.81 inference(scs_inference,[],[369,47])). % 127.83/127.81 cnf(441,plain, % 127.83/127.81 (~P2(a8,f9(a6,x4411))), % 127.83/127.81 inference(scs_inference,[],[369,47,48])). % 127.83/127.81 cnf(492,plain, % 127.83/127.81 (~P2(f11(a6),f11(f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[65,132,383,48,47,19,6,45])). % 127.83/127.81 cnf(518,plain, % 127.83/127.81 (~P2(a6,f9(f10(a5,a5),x5181))), % 127.83/127.81 inference(scs_inference,[],[77,48])). % 127.83/127.81 cnf(520,plain, % 127.83/127.81 (~P2(a6,f9(x5201,f10(a5,a5)))), % 127.83/127.81 inference(scs_inference,[],[77,48,47])). % 127.83/127.81 cnf(628,plain, % 127.83/127.81 (E(f10(x6281,f11(a6)),f10(x6281,f9(f10(a6,a5),a8)))), % 127.83/127.81 inference(scs_inference,[],[25,7,2])). % 127.83/127.81 cnf(915,plain, % 127.83/127.81 (E(f3(x9151,f3(f9(f10(a6,a5),a8),x9152,x9153),x9154),f3(x9151,f3(f11(a6),x9152,x9153),x9154))), % 127.83/127.81 inference(scs_inference,[],[25,12,11])). % 127.83/127.81 cnf(991,plain, % 127.83/127.81 (P2(a6,a8)), % 127.83/127.81 inference(scs_inference,[],[22,112,18])). % 127.83/127.81 cnf(992,plain, % 127.83/127.81 (E(f9(x9921,x9921),x9921)), % 127.83/127.81 inference(rename_variables,[],[22])). % 127.83/127.81 cnf(993,plain, % 127.83/127.81 (E(f9(f11(a6),f11(a6)),f9(f10(a6,a5),a8))), % 127.83/127.81 inference(scs_inference,[],[22,992,58,112,18,3])). % 127.83/127.81 cnf(995,plain, % 127.83/127.81 (E(f9(f10(a6,a5),a8),f9(f11(a6),f11(a6)))), % 127.83/127.81 inference(scs_inference,[],[22,992,58,112,18,3,2])). % 127.83/127.81 cnf(996,plain, % 127.83/127.81 (~E(a8,f9(f11(a5),x9961))), % 127.83/127.81 inference(scs_inference,[],[22,992,58,112,101,18,3,2,19])). % 127.83/127.81 cnf(997,plain, % 127.83/127.81 (P2(f4(f11(a5),x9971,a8),x9971)+P2(f4(f11(a5),x9971,a8),a8)), % 127.83/127.81 inference(scs_inference,[],[22,992,58,112,101,18,3,2,19,40])). % 127.83/127.81 cnf(999,plain, % 127.83/127.81 (P2(a6,f11(a6))), % 127.83/127.81 inference(scs_inference,[],[22,992,58,83,112,101,18,3,2,19,40,35])). % 127.83/127.81 cnf(1010,plain, % 127.83/127.81 (~E(f11(a6),f9(f11(a5),x10101))), % 127.83/127.81 inference(scs_inference,[],[101,999,19])). % 127.83/127.81 cnf(1011,plain, % 127.83/127.81 (P2(a6,f9(a8,a8))), % 127.83/127.81 inference(scs_inference,[],[22,187,101,999,19,18])). % 127.83/127.81 cnf(1031,plain, % 127.83/127.81 (P2(a6,f10(a6,a5))), % 127.83/127.81 inference(scs_inference,[],[22,52,110,1011,19,18])). % 127.83/127.81 cnf(1033,plain, % 127.83/127.81 (~P2(f9(a8,a8),f11(f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[22,52,110,1011,19,18,45])). % 127.83/127.81 cnf(1035,plain, % 127.83/127.81 (~P2(f9(a8,a8),f10(f11(a5),f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[22,52,110,1011,19,18,45,46])). % 127.83/127.81 cnf(1045,plain, % 127.83/127.81 (P2(a6,f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.81 inference(scs_inference,[],[22,252,18])). % 127.83/127.81 cnf(1047,plain, % 127.83/127.81 (~P2(x10471,f9(f11(a6),f11(a6)))+P2(x10471,f10(a6,a5))), % 127.83/127.81 inference(scs_inference,[],[22,252,993,18,36])). % 127.83/127.81 cnf(1049,plain, % 127.83/127.81 (~E(f9(f9(a8,a8),f9(a8,a8)),f11(a5))), % 127.83/127.81 inference(scs_inference,[],[22,52,252,993,18,36,19])). % 127.83/127.81 cnf(1059,plain, % 127.83/127.81 (~P2(f9(f9(a8,a8),f9(a8,a8)),f11(f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[1049,45])). % 127.83/127.81 cnf(1063,plain, % 127.83/127.81 (~E(f9(f10(a6,a5),a8),f10(a5,a5))), % 127.83/127.81 inference(scs_inference,[],[83,77,1049,45,46,19])). % 127.83/127.81 cnf(1064,plain, % 127.83/127.81 (P2(a6,f9(f10(a6,a5),f10(a6,a5)))), % 127.83/127.81 inference(scs_inference,[],[22,83,77,172,1049,45,46,19,18])). % 127.83/127.81 cnf(1066,plain, % 127.83/127.81 (P2(f4(f11(a5),x10661,a8),a8)+P2(f4(f11(a5),x10661,a8),f11(a5))), % 127.83/127.81 inference(scs_inference,[],[22,83,77,172,996,1049,45,46,19,18,41])). % 127.83/127.81 cnf(1071,plain, % 127.83/127.81 (~P2(a8,f4(f11(a5),a8,a8))+P2(f4(f11(a5),a8,a8),f11(a5))), % 127.83/127.81 inference(scs_inference,[],[22,83,77,172,996,1049,45,46,19,18,41,44,32])). % 127.83/127.81 cnf(1074,plain, % 127.83/127.81 (~P2(f9(f10(a6,a5),a8),f11(f10(a5,a5)))), % 127.83/127.81 inference(scs_inference,[],[1063,45])). % 127.83/127.81 cnf(1078,plain, % 127.83/127.81 (~E(f9(f10(a6,a5),f10(a6,a5)),f11(a5))), % 127.83/127.81 inference(scs_inference,[],[52,1063,1064,45,46,19])). % 127.83/127.81 cnf(1079,plain, % 127.83/127.81 (~E(a6,f10(x10791,f11(a6)))), % 127.83/127.81 inference(scs_inference,[],[312,52,999,1063,1064,45,46,19,18])). % 127.83/127.81 cnf(1090,plain, % 127.83/127.81 (~E(a8,f10(a5,a5))), % 127.83/127.81 inference(scs_inference,[],[77,991,1078,45,46,19])). % 127.83/127.81 cnf(1096,plain, % 127.83/127.81 (~P2(a8,f11(f10(a5,a5)))), % 127.83/127.81 inference(scs_inference,[],[1090,45])). % 127.83/127.81 cnf(1146,plain, % 127.83/127.81 (~P2(f4(f11(a5),x11461,a8),a8)+~P2(f4(f11(a5),x11461,a8),f11(a5))+~P2(f4(f11(a5),x11461,a8),x11461)), % 127.83/127.81 inference(scs_inference,[],[136,996,44])). % 127.83/127.81 cnf(1230,plain, % 127.83/127.81 (E(x12301,f9(x12301,x12301))), % 127.83/127.81 inference(rename_variables,[],[105])). % 127.83/127.81 cnf(1231,plain, % 127.83/127.81 (P2(f9(f11(a6),f11(a6)),f10(f11(a6),x12311))), % 127.83/127.81 inference(scs_inference,[],[105,1230,267,85,19,18])). % 127.83/127.81 cnf(1233,plain, % 127.83/127.81 (~E(a8,f9(x12331,f11(a5)))), % 127.83/127.81 inference(scs_inference,[],[996,105,1230,267,85,24,19,18,3])). % 127.83/127.81 cnf(1241,plain, % 127.83/127.81 (~P2(f9(f11(a6),f11(a6)),a6)), % 127.83/127.81 inference(scs_inference,[],[996,105,1230,267,85,24,19,18,3,32,47,48,49])). % 127.83/127.81 cnf(1243,plain, % 127.83/127.81 (P2(f4(x12431,f11(a5),a8),a8)+P2(f4(x12431,f11(a5),a8),x12431)), % 127.83/127.81 inference(scs_inference,[],[996,105,1230,267,85,24,19,18,3,32,47,48,49,41])). % 127.83/127.81 cnf(1256,plain, % 127.83/127.81 (P2(f9(a6,a6),f10(a5,a6))), % 127.83/127.81 inference(scs_inference,[],[23,110,1241,48,47,19])). % 127.83/127.81 cnf(1260,plain, % 127.83/127.81 (~P2(f10(a5,a6),f9(a6,a6))), % 127.83/127.81 inference(scs_inference,[],[23,105,302,110,1241,48,47,19,18,32])). % 127.83/127.81 cnf(1262,plain, % 127.83/127.81 (~P2(f10(a5,a6),a6)), % 127.83/127.81 inference(scs_inference,[],[23,105,302,110,1241,48,47,19,18,32,49])). % 127.83/127.81 cnf(1264,plain, % 127.83/127.81 (P2(f4(x12641,f11(a5),a8),f11(a5))+P2(f4(x12641,f11(a5),a8),a8)), % 127.83/127.81 inference(scs_inference,[],[23,105,302,110,1241,1233,48,47,19,18,32,49,40])). % 127.83/127.81 cnf(1278,plain, % 127.83/127.81 (P2(f9(f9(a6,a6),f9(a6,a6)),f10(a5,a6))), % 127.83/127.81 inference(scs_inference,[],[1260,105,1256,48,47,18])). % 127.83/127.81 cnf(1433,plain, % 127.83/127.81 (E(f9(a8,f10(a6,a5)),f11(a6))), % 127.83/127.81 inference(scs_inference,[],[24,25,3])). % 127.83/127.81 cnf(1434,plain, % 127.83/127.81 (E(f9(x14341,x14342),f9(x14342,x14341))), % 127.83/127.81 inference(rename_variables,[],[24])). % 127.83/127.81 cnf(1435,plain, % 127.83/127.81 (P2(f9(a8,f10(a6,a5)),f10(x14351,f11(a6)))), % 127.83/127.81 inference(scs_inference,[],[24,1434,25,68,3,18])). % 127.83/127.81 cnf(1436,plain, % 127.83/127.81 (E(f9(x14361,x14362),f9(x14362,x14361))), % 127.83/127.81 inference(rename_variables,[],[24])). % 127.83/127.81 cnf(1437,plain, % 127.83/127.81 (P2(f9(a6,a6),f9(a8,f10(a6,a5)))), % 127.83/127.81 inference(scs_inference,[],[24,1434,1436,25,68,59,3,18,19])). % 127.83/127.81 cnf(1439,plain, % 127.83/127.81 (E(f11(a6),f9(a8,f10(a6,a5)))), % 127.83/127.81 inference(scs_inference,[],[24,1434,1436,25,68,59,3,18,19,2])). % 127.83/127.81 cnf(1444,plain, % 127.83/127.81 (~P2(f4(x14441,f11(a5),a8),a8)+~P2(f4(x14441,f11(a5),a8),x14441)+~P2(f4(x14441,f11(a5),a8),f11(a5))), % 127.83/127.81 inference(scs_inference,[],[24,1434,1436,25,1233,1079,68,59,3,18,19,2,32,44])). % 127.83/127.81 cnf(1447,plain, % 127.83/127.81 (~P2(f9(a8,f10(a6,a5)),a6)), % 127.83/127.81 inference(scs_inference,[],[1437,32,49])). % 127.83/127.81 cnf(1450,plain, % 127.83/127.81 (E(f9(x14501,x14502),f9(x14502,x14501))), % 127.83/127.81 inference(rename_variables,[],[24])). % 127.83/127.81 cnf(1459,plain, % 127.83/127.81 (E(f9(f11(a6),f11(a6)),f9(a8,f10(a6,a5)))), % 127.83/127.81 inference(scs_inference,[],[24,1450,995,105,65,1278,1437,32,49,3,18,19,47,48,2])). % 127.83/127.81 cnf(1466,plain, % 127.83/127.81 (~P2(f9(a8,f10(a6,a5)),f9(x14661,a6))), % 127.83/127.81 inference(scs_inference,[],[1447,47])). % 127.83/127.81 cnf(1468,plain, % 127.83/127.81 (~P2(f9(a8,f10(a6,a5)),f9(a6,x14681))), % 127.83/127.81 inference(scs_inference,[],[1447,47,48])). % 127.83/127.81 cnf(1503,plain, % 127.83/127.82 (~P2(f9(a8,f10(a6,a5)),f9(x15031,f9(x15032,a6)))), % 127.83/127.82 inference(scs_inference,[],[1466,47])). % 127.83/127.82 cnf(1647,plain, % 127.83/127.82 (P2(a6,f9(f11(a6),f11(a6)))), % 127.83/127.82 inference(scs_inference,[],[1459,991,1031,37])). % 127.83/127.82 cnf(1655,plain, % 127.83/127.82 (~E(f11(a6),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[77,999,19])). % 127.83/127.82 cnf(1658,plain, % 127.83/127.82 (~P2(f11(a6),f11(f10(a5,a5)))), % 127.83/127.82 inference(scs_inference,[],[77,999,19,46,45])). % 127.83/127.82 cnf(1923,plain, % 127.83/127.82 (~P2(f4(f11(a5),a8,a8),f11(a5))), % 127.83/127.82 inference(scs_inference,[],[997,1146])). % 127.83/127.82 cnf(1924,plain, % 127.83/127.82 (~P2(a8,f4(f11(a5),a8,a8))), % 127.83/127.82 inference(scs_inference,[],[1923,1071])). % 127.83/127.82 cnf(1925,plain, % 127.83/127.82 (~P2(f4(f11(a5),a8,a8),f9(f11(a5),x19251))), % 127.83/127.82 inference(scs_inference,[],[1923,48])). % 127.83/127.82 cnf(1929,plain, % 127.83/127.82 (P2(f4(f11(a5),a8,a8),a8)), % 127.83/127.82 inference(scs_inference,[],[996,1923,48,47,41])). % 127.83/127.82 cnf(2026,plain, % 127.83/127.82 (~P2(f4(a8,f11(a5),a8),f11(a5))), % 127.83/127.82 inference(scs_inference,[],[1243,1444])). % 127.83/127.82 cnf(2031,plain, % 127.83/127.82 (P2(f4(a8,f11(a5),a8),a8)), % 127.83/127.82 inference(scs_inference,[],[1233,2026,47,48,40])). % 127.83/127.82 cnf(2034,plain, % 127.83/127.82 (~P2(a8,f4(a8,f11(a5),a8))), % 127.83/127.82 inference(scs_inference,[],[1233,2026,47,48,40,32])). % 127.83/127.82 cnf(2152,plain, % 127.83/127.82 (E(f10(x21521,f9(x21522,x21523)),f10(x21521,f9(x21523,x21522)))), % 127.83/127.82 inference(scs_inference,[],[24,7])). % 127.83/127.82 cnf(2153,plain, % 127.83/127.82 (E(f2(f9(x21531,x21532),x21533),f2(f9(x21532,x21531),x21533))), % 127.83/127.82 inference(scs_inference,[],[24,7,14])). % 127.83/127.82 cnf(2154,plain, % 127.83/127.82 (E(f2(x21541,f9(x21542,x21543)),f2(x21541,f9(x21543,x21542)))), % 127.83/127.82 inference(scs_inference,[],[24,7,14,15])). % 127.83/127.82 cnf(2156,plain, % 127.83/127.82 (E(f4(x21561,f9(x21562,x21563),x21564),f4(x21561,f9(x21563,x21562),x21564))), % 127.83/127.82 inference(scs_inference,[],[24,7,14,15,8,9])). % 127.83/127.82 cnf(2159,plain, % 127.83/127.82 (E(f3(x21591,x21592,f9(x21593,x21594)),f3(x21591,x21592,f9(x21594,x21593)))), % 127.83/127.82 inference(scs_inference,[],[24,7,14,15,8,9,10,12,13])). % 127.83/127.82 cnf(2163,plain, % 127.83/127.82 (E(f9(f9(x21631,x21632),x21633),f9(f9(x21632,x21631),x21633))), % 127.83/127.82 inference(scs_inference,[],[24,7,14,15,8,9,10,12,13,16,11,6,4])). % 127.83/127.82 cnf(2166,plain, % 127.83/127.82 (P2(f4(f11(a5),a8,a8),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[1929,281,24,7,14,15,8,9,10,12,13,16,11,6,4,5,2,49])). % 127.83/127.82 cnf(2169,plain, % 127.83/127.82 (E(x21691,f9(x21691,x21691))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2172,plain, % 127.83/127.82 (E(x21721,f9(x21721,x21721))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2179,plain, % 127.83/127.82 (~E(a1,f9(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[81,99,1929,281,20,1655,267,24,105,2169,2172,7,14,15,8,9,10,12,13,16,11,6,4,5,2,49,28,31,29,30,17])). % 127.83/127.82 cnf(2181,plain, % 127.83/127.82 (~P2(f9(a6,a6),f11(f9(a5,a5)))), % 127.83/127.82 inference(scs_inference,[],[81,99,1929,281,20,1655,995,267,24,22,105,2169,2172,7,14,15,8,9,10,12,13,16,11,6,4,5,2,49,28,31,29,30,17,3,18])). % 127.83/127.82 cnf(2183,plain, % 127.83/127.82 (~E(f9(f11(a6),f11(a6)),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[81,99,1929,281,1647,20,1655,995,267,24,22,26,105,2169,2172,7,14,15,8,9,10,12,13,16,11,6,4,5,2,49,28,31,29,30,17,3,18,33])). % 127.83/127.82 cnf(2185,plain, % 127.83/127.82 (~E(f9(f11(a5),x21851),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[81,99,1929,281,1925,1647,20,1655,995,267,24,22,26,105,2169,2172,7,14,15,8,9,10,12,13,16,11,6,4,5,2,49,28,31,29,30,17,3,18,33,37])). % 127.83/127.82 cnf(2187,plain, % 127.83/127.82 (~P2(f9(a8,a8),f4(f11(a5),a8,a8))), % 127.83/127.82 inference(scs_inference,[],[81,99,1929,281,1925,1647,20,1655,995,267,24,22,26,105,2169,2172,7,14,15,8,9,10,12,13,16,11,6,4,5,2,49,28,31,29,30,17,3,18,33,37,32])). % 127.83/127.82 cnf(2191,plain, % 127.83/127.82 (~P2(x21911,f2(f9(x21912,x21913),x21914))+P2(x21911,f2(f9(x21913,x21912),x21914))), % 127.83/127.82 inference(scs_inference,[],[81,99,1929,281,1925,1647,20,1655,995,267,24,52,22,26,105,2169,2172,7,14,15,8,9,10,12,13,16,11,6,4,5,2,49,28,31,29,30,17,3,18,33,37,32,35,19])). % 127.83/127.82 cnf(2192,plain, % 127.83/127.82 (~P2(a1,f10(f9(a7,a7),f9(a7,a7)))), % 127.83/127.82 inference(scs_inference,[],[81,99,1929,281,1925,1647,20,1655,995,267,24,52,22,26,105,2169,2172,7,14,15,8,9,10,12,13,16,11,6,4,5,2,49,28,31,29,30,17,3,18,33,37,32,35,19,46])). % 127.83/127.82 cnf(2195,plain, % 127.83/127.82 (E(f10(x21951,f9(x21952,x21952)),f10(x21951,x21952))), % 127.83/127.82 inference(scs_inference,[],[22,7])). % 127.83/127.82 cnf(2196,plain, % 127.83/127.82 (E(f3(x21961,f9(x21962,x21962),x21963),f3(x21961,x21962,x21963))), % 127.83/127.82 inference(scs_inference,[],[22,7,12])). % 127.83/127.82 cnf(2197,plain, % 127.83/127.82 (E(f4(x21971,x21972,f9(x21973,x21973)),f4(x21971,x21972,x21973))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10])). % 127.83/127.82 cnf(2198,plain, % 127.83/127.82 (E(f4(f9(x21981,x21981),x21982,x21983),f4(x21981,x21982,x21983))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8])). % 127.83/127.82 cnf(2199,plain, % 127.83/127.82 (E(f11(f9(x21991,x21991)),f11(x21991))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16])). % 127.83/127.82 cnf(2200,plain, % 127.83/127.82 (E(f4(x22001,f9(x22002,x22002),x22003),f4(x22001,x22002,x22003))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16,9])). % 127.83/127.82 cnf(2201,plain, % 127.83/127.82 (E(f3(x22011,x22012,f9(x22013,x22013)),f3(x22011,x22012,x22013))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16,9,13])). % 127.83/127.82 cnf(2202,plain, % 127.83/127.82 (E(f2(f9(x22021,x22021),x22022),f2(x22021,x22022))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16,9,13,14])). % 127.83/127.82 cnf(2203,plain, % 127.83/127.82 (E(f2(x22031,f9(x22032,x22032)),f2(x22031,x22032))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16,9,13,14,15])). % 127.83/127.82 cnf(2204,plain, % 127.83/127.82 (E(f10(f9(x22041,x22041),x22042),f10(x22041,x22042))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16,9,13,14,15,6])). % 127.83/127.82 cnf(2205,plain, % 127.83/127.82 (E(f9(f9(x22051,x22051),x22052),f9(x22051,x22052))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16,9,13,14,15,6,4])). % 127.83/127.82 cnf(2206,plain, % 127.83/127.82 (E(f3(f9(x22061,x22061),x22062,x22063),f3(x22061,x22062,x22063))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16,9,13,14,15,6,4,11])). % 127.83/127.82 cnf(2207,plain, % 127.83/127.82 (E(f9(x22071,f9(x22072,x22072)),f9(x22071,x22072))), % 127.83/127.82 inference(scs_inference,[],[22,7,12,10,8,16,9,13,14,15,6,4,11,5])). % 127.83/127.82 cnf(2208,plain, % 127.83/127.82 (~E(f9(a7,a7),a1)), % 127.83/127.82 inference(scs_inference,[],[2179,22,7,12,10,8,16,9,13,14,15,6,4,11,5,2])). % 127.83/127.82 cnf(2209,plain, % 127.83/127.82 (P2(f4(a8,f11(a5),a8),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2179,2031,22,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49])). % 127.83/127.82 cnf(2211,plain, % 127.83/127.82 (~E(a6,f11(f11(a6)))), % 127.83/127.82 inference(scs_inference,[],[2179,2031,1433,1447,22,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28])). % 127.83/127.82 cnf(2213,plain, % 127.83/127.82 (~E(f11(f11(a5)),f10(a8,x22131))), % 127.83/127.82 inference(scs_inference,[],[2179,1033,2031,1433,1447,22,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31])). % 127.83/127.82 cnf(2214,plain, % 127.83/127.82 (E(f9(x22141,x22141),x22141)), % 127.83/127.82 inference(rename_variables,[],[22])). % 127.83/127.82 cnf(2216,plain, % 127.83/127.82 (~E(f9(a8,a8),f9(f11(a5),x22161))), % 127.83/127.82 inference(scs_inference,[],[2179,2166,1033,2031,1433,1447,1923,22,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31,36])). % 127.83/127.82 cnf(2218,plain, % 127.83/127.82 (~E(f9(a8,a8),f9(x22181,f11(a5)))), % 127.83/127.82 inference(scs_inference,[],[2179,2166,1033,2031,1433,1447,1923,22,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31,36,35])). % 127.83/127.82 cnf(2221,plain, % 127.83/127.82 (E(f9(x22211,x22211),x22211)), % 127.83/127.82 inference(rename_variables,[],[22])). % 127.83/127.82 cnf(2223,plain, % 127.83/127.82 (~E(f11(f11(a5)),f10(x22231,a8))), % 127.83/127.82 inference(scs_inference,[],[2179,2166,1033,2031,1433,1447,1923,22,2214,2221,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31,36,35,29,30])). % 127.83/127.82 cnf(2226,plain, % 127.83/127.82 (~E(f9(a8,f10(a6,a5)),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2179,2166,1033,2031,1433,1439,1447,1655,1923,22,2214,2221,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31,36,35,29,30,3])). % 127.83/127.82 cnf(2227,plain, % 127.83/127.82 (~E(f9(a1,a1),a7)), % 127.83/127.82 inference(scs_inference,[],[2179,2166,1033,2031,1433,27,137,1439,1447,1655,1923,22,2214,2221,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31,36,35,29,30,3,17])). % 127.83/127.82 cnf(2230,plain, % 127.83/127.82 (~E(f9(f9(a8,a8),f9(a8,a8)),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2179,2166,320,1033,2031,1045,1433,27,137,1439,1447,1655,1923,23,22,2214,2221,26,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31,36,35,29,30,3,17,18,33])). % 127.83/127.82 cnf(2232,plain, % 127.83/127.82 (~E(f11(a5),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2179,2166,320,1033,2031,1045,1433,27,137,1439,1447,1655,2026,1923,23,22,2214,2221,26,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31,36,35,29,30,3,17,18,33,37])). % 127.83/127.82 cnf(2234,plain, % 127.83/127.82 (~P2(f9(a8,a8),f4(a8,f11(a5),a8))), % 127.83/127.82 inference(scs_inference,[],[2179,2166,320,1033,2031,1045,1433,27,137,1439,1447,1655,2026,1923,23,22,2214,2221,26,7,12,10,8,16,9,13,14,15,6,4,11,5,2,49,28,31,36,35,29,30,3,17,18,33,37,32])). % 127.83/127.82 cnf(2236,plain, % 127.83/127.82 (E(f10(x22361,x22362),f10(x22361,f9(x22362,x22362)))), % 127.83/127.82 inference(scs_inference,[],[105,7])). % 127.83/127.82 cnf(2237,plain, % 127.83/127.82 (E(f4(x22371,x22372,x22373),f4(x22371,f9(x22372,x22372),x22373))), % 127.83/127.82 inference(scs_inference,[],[105,7,9])). % 127.83/127.82 cnf(2238,plain, % 127.83/127.82 (E(f3(x22381,x22382,x22383),f3(x22381,x22382,f9(x22383,x22383)))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13])). % 127.83/127.82 cnf(2239,plain, % 127.83/127.82 (E(f3(x22391,x22392,x22393),f3(x22391,f9(x22392,x22392),x22393))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12])). % 127.83/127.82 cnf(2240,plain, % 127.83/127.82 (E(f4(x22401,x22402,x22403),f4(x22401,x22402,f9(x22403,x22403)))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10])). % 127.83/127.82 cnf(2241,plain, % 127.83/127.82 (E(f4(x22411,x22412,x22413),f4(f9(x22411,x22411),x22412,x22413))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10,8])). % 127.83/127.82 cnf(2242,plain, % 127.83/127.82 (E(f9(x22421,x22422),f9(f9(x22421,x22421),x22422))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10,8,4])). % 127.83/127.82 cnf(2243,plain, % 127.83/127.82 (E(f11(x22431),f11(f9(x22431,x22431)))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10,8,4,16])). % 127.83/127.82 cnf(2244,plain, % 127.83/127.82 (E(f2(x22441,x22442),f2(x22441,f9(x22442,x22442)))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10,8,4,16,15])). % 127.83/127.82 cnf(2245,plain, % 127.83/127.82 (E(f3(x22451,x22452,x22453),f3(f9(x22451,x22451),x22452,x22453))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10,8,4,16,15,11])). % 127.83/127.82 cnf(2246,plain, % 127.83/127.82 (E(f2(x22461,x22462),f2(f9(x22461,x22461),x22462))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10,8,4,16,15,11,14])). % 127.83/127.82 cnf(2247,plain, % 127.83/127.82 (E(f9(x22471,x22472),f9(x22471,f9(x22472,x22472)))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10,8,4,16,15,11,14,5])). % 127.83/127.82 cnf(2248,plain, % 127.83/127.82 (E(f10(x22481,x22482),f10(f9(x22481,x22481),x22482))), % 127.83/127.82 inference(scs_inference,[],[105,7,9,13,12,10,8,4,16,15,11,14,5,6])). % 127.83/127.82 cnf(2249,plain, % 127.83/127.82 (~E(a7,f9(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2227,105,7,9,13,12,10,8,4,16,15,11,14,5,6,2])). % 127.83/127.82 cnf(2251,plain, % 127.83/127.82 (E(x22511,f9(x22511,x22511))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2253,plain, % 127.83/127.82 (~E(a5,f11(f9(a8,a8)))), % 127.83/127.82 inference(scs_inference,[],[2227,50,105,2251,7,9,13,12,10,8,4,16,15,11,14,5,6,2,31,28])). % 127.83/127.82 cnf(2254,plain, % 127.83/127.82 (E(x22541,f9(x22541,x22541))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2256,plain, % 127.83/127.82 (~P2(a8,f4(f11(a5),a8,f9(a8,a8)))), % 127.83/127.82 inference(scs_inference,[],[2227,2197,1924,50,105,2251,7,9,13,12,10,8,4,16,15,11,14,5,6,2,31,28,19])). % 127.83/127.82 cnf(2259,plain, % 127.83/127.82 (E(x22591,f9(x22591,x22591))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2261,plain, % 127.83/127.82 (~E(f9(f9(a1,a1),f9(a1,a1)),f9(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2227,2197,1924,50,81,170,105,2251,2254,7,9,13,12,10,8,4,16,15,11,14,5,6,2,31,28,19,30,17])). % 127.83/127.82 cnf(2262,plain, % 127.83/127.82 (~E(f9(f9(a1,a1),f9(a1,a1)),a7)), % 127.83/127.82 inference(scs_inference,[],[2227,2197,1924,50,81,170,105,2251,2254,2259,7,9,13,12,10,8,4,16,15,11,14,5,6,2,31,28,19,30,17,3])). % 127.83/127.82 cnf(2264,plain, % 127.83/127.82 (~P2(f9(a6,a6),f10(f9(a5,a5),f9(a5,a5)))), % 127.83/127.82 inference(scs_inference,[],[2227,2197,108,1924,50,81,170,105,2251,2254,2259,22,7,9,13,12,10,8,4,16,15,11,14,5,6,2,31,28,19,30,17,3,18])). % 127.83/127.82 cnf(2269,plain, % 127.83/127.82 (P2(a5,f9(f9(a8,a8),a8))), % 127.83/127.82 inference(scs_inference,[],[21,2227,2195,2205,2197,108,1924,50,81,170,105,2251,2254,2259,22,7,9,13,12,10,8,4,16,15,11,14,5,6,2,31,28,19,30,17,3,18,33,37])). % 127.83/127.82 cnf(2272,plain, % 127.83/127.82 (~P2(f9(f9(a8,a8),a8),a5)), % 127.83/127.82 inference(scs_inference,[],[21,2227,2195,2205,2197,108,1924,50,81,170,105,2251,2254,2259,22,7,9,13,12,10,8,4,16,15,11,14,5,6,2,31,28,19,30,17,3,18,33,37,32])). % 127.83/127.82 cnf(2274,plain, % 127.83/127.82 (~P2(f9(a1,a1),f11(f9(a7,a7)))), % 127.83/127.82 inference(scs_inference,[],[21,2227,2199,2195,2205,2197,108,1924,50,81,170,105,2251,2254,2259,22,7,9,13,12,10,8,4,16,15,11,14,5,6,2,31,28,19,30,17,3,18,33,37,32,29])). % 127.83/127.82 cnf(2283,plain, % 127.83/127.82 (E(f4(f9(x22831,x22831),x22832,x22833),f4(x22831,x22832,x22833))), % 127.83/127.82 inference(rename_variables,[],[2198])). % 127.83/127.82 cnf(2286,plain, % 127.83/127.82 (~E(a1,a7)), % 127.83/127.82 inference(scs_inference,[],[2183,2198,2034,1433,20,27,1466,2,31,28,19,30,17])). % 127.83/127.82 cnf(2287,plain, % 127.83/127.82 (~P2(f4(f9(a8,a8),f11(a5),a8),f11(a5))), % 127.83/127.82 inference(scs_inference,[],[2183,2198,2283,2034,1433,20,27,1466,2026,2,31,28,19,30,17,18])). % 127.83/127.82 cnf(2289,plain, % 127.83/127.82 (E(f2(f9(x22891,x22891),f9(x22892,x22892)),f2(x22891,x22892))), % 127.83/127.82 inference(scs_inference,[],[2183,2202,2203,2198,2283,2034,1433,20,27,1466,2026,2,31,28,19,30,17,18,3])). % 127.83/127.82 cnf(2291,plain, % 127.83/127.82 (P2(a5,f9(a8,f9(a8,a8)))), % 127.83/127.82 inference(scs_inference,[],[21,2183,2202,2203,2207,2198,2283,2034,1433,20,27,1466,2026,2,31,28,19,30,17,18,3,37])). % 127.83/127.82 cnf(2294,plain, % 127.83/127.82 (P2(f4(f9(a8,a8),f11(a5),a8),a8)), % 127.83/127.82 inference(scs_inference,[],[21,2183,2202,2203,2207,2198,2283,2034,1433,20,27,1466,2026,2,31,28,19,30,17,18,3,37,1264])). % 127.83/127.82 cnf(2296,plain, % 127.83/127.82 (~P2(f9(a8,f9(a8,a8)),a5)), % 127.83/127.82 inference(scs_inference,[],[21,2183,2202,2203,2207,2198,2283,2034,1433,20,27,1466,2026,2,31,28,19,30,17,18,3,37,1264,32])). % 127.83/127.82 cnf(2298,plain, % 127.83/127.82 (P2(f4(f9(a8,a8),f11(a5),a8),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[21,2183,2202,2203,2207,2198,2283,2034,1433,20,27,1466,2026,2,31,28,19,30,17,18,3,37,1264,32,49])). % 127.83/127.82 cnf(2300,plain, % 127.83/127.82 (E(f4(a8,f11(a5),a8),x23001)+~E(f9(a8,a8),f11(x23001))), % 127.83/127.82 inference(scs_inference,[],[21,2183,2202,2203,2207,2198,2283,2209,2034,1433,20,27,1466,2026,2,31,28,19,30,17,18,3,37,1264,32,49,29])). % 127.83/127.82 cnf(2302,plain, % 127.83/127.82 (~P2(f9(a7,a7),f10(f9(a1,a1),a1))), % 127.83/127.82 inference(scs_inference,[],[21,2208,2183,2202,2203,2204,2207,2198,2283,2209,2034,1433,20,27,1466,2026,2,31,28,19,30,17,18,3,37,1264,32,49,29,33])). % 127.83/127.82 cnf(2305,plain, % 127.83/127.82 (~P2(f9(a8,a8),f4(f9(a8,a8),f11(a5),a8))), % 127.83/127.82 inference(scs_inference,[],[2298,32])). % 127.83/127.82 cnf(2307,plain, % 127.83/127.82 (~E(a7,a1)), % 127.83/127.82 inference(scs_inference,[],[2286,2298,32,2])). % 127.83/127.82 cnf(2309,plain, % 127.83/127.82 (E(x23091,f9(x23091,x23091))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2312,plain, % 127.83/127.82 (E(x23121,f9(x23121,x23121))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2314,plain, % 127.83/127.82 (~P2(f9(f9(a8,a8),a8),f9(x23141,a5))), % 127.83/127.82 inference(scs_inference,[],[2286,2298,2242,2272,369,105,2309,32,2,31,28,35])). % 127.83/127.82 cnf(2317,plain, % 127.83/127.82 (~P2(a1,f11(f9(a7,a7)))), % 127.83/127.82 inference(scs_inference,[],[2286,2298,2242,2272,2199,369,105,2309,32,2,31,28,35,29])). % 127.83/127.82 cnf(2320,plain, % 127.83/127.82 (~P2(f9(a8,a8),f4(f11(a5),f9(a8,a8),a8))), % 127.83/127.82 inference(scs_inference,[],[2286,2200,2298,2187,2242,2272,2199,369,105,2309,32,2,31,28,35,29,19])). % 127.83/127.82 cnf(2325,plain, % 127.83/127.82 (~E(f9(a1,a1),f9(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2286,2200,2298,2187,2242,2272,2199,81,137,369,105,2309,2312,32,2,31,28,35,29,19,30,17])). % 127.83/127.82 cnf(2326,plain, % 127.83/127.82 (~P2(f9(a8,a8),f11(f10(a5,a5)))), % 127.83/127.82 inference(scs_inference,[],[2286,2200,2298,1096,2187,2242,2272,2199,81,137,369,22,105,2309,2312,32,2,31,28,35,29,19,30,17,18])). % 127.83/127.82 cnf(2328,plain, % 127.83/127.82 (~E(f11(f9(a5,a5)),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2286,2232,2200,2298,1096,2187,2243,2242,2272,2199,81,137,369,22,105,2309,2312,32,2,31,28,35,29,19,30,17,18,3])). % 127.83/127.82 cnf(2335,plain, % 127.83/127.82 (~P2(a1,f10(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2286,2232,2200,2298,2287,1096,2187,2243,2242,2272,2199,2195,81,137,369,22,105,2309,2312,32,2,31,28,35,29,19,30,17,18,3,37,33,46])). % 127.83/127.82 cnf(2337,plain, % 127.83/127.82 (~E(f9(a7,a7),f9(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2325,2])). % 127.83/127.82 cnf(2339,plain, % 127.83/127.82 (E(f9(f9(x23391,x23391),x23392),f9(x23391,x23392))), % 127.83/127.82 inference(rename_variables,[],[2205])). % 127.83/127.82 cnf(2342,plain, % 127.83/127.82 (E(f9(f9(x23421,x23421),x23422),f9(x23421,x23422))), % 127.83/127.82 inference(rename_variables,[],[2205])). % 127.83/127.82 cnf(2344,plain, % 127.83/127.82 (~P2(f9(a6,a6),f10(f9(a5,a5),a5))), % 127.83/127.82 inference(scs_inference,[],[2325,2314,2236,2264,2205,2339,2,28,31,19])). % 127.83/127.82 cnf(2345,plain, % 127.83/127.82 (E(f10(x23451,x23452),f10(x23451,f9(x23452,x23452)))), % 127.83/127.82 inference(rename_variables,[],[2236])). % 127.83/127.82 cnf(2347,plain, % 127.83/127.82 (E(f9(f9(x23471,x23471),x23472),f9(x23471,x23472))), % 127.83/127.82 inference(rename_variables,[],[2205])). % 127.83/127.82 cnf(2351,plain, % 127.83/127.82 (E(f3(x23511,f9(x23512,x23512),f9(x23513,x23513)),f3(x23511,x23512,x23513))), % 127.83/127.82 inference(scs_inference,[],[2325,2196,2201,2314,2236,2240,2264,2294,2205,2339,2342,2,28,31,19,30,18,3])). % 127.83/127.82 cnf(2358,plain, % 127.83/127.82 (P2(f4(f9(a8,a8),f11(a5),f9(a8,a8)),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2325,2196,2201,2314,2236,2240,2264,2294,114,2205,2339,2342,2347,2,28,31,19,30,18,3,37,32,49])). % 127.83/127.82 cnf(2360,plain, % 127.83/127.82 (~P2(a1,f9(f10(a7,a7),x23601))), % 127.83/127.82 inference(scs_inference,[],[2325,2335,2196,2201,2314,2236,2247,2240,2264,2294,114,2205,2339,2342,2347,2,28,31,19,30,18,3,37,32,49,36])). % 127.83/127.82 cnf(2365,plain, % 127.83/127.82 (~P2(f4(f9(a8,a8),f11(a5),f9(a8,a8)),f11(a5))), % 127.83/127.82 inference(scs_inference,[],[2325,2335,2196,2201,2314,2236,2247,2240,2264,2294,2218,114,2205,2339,2342,2347,2,28,31,19,30,18,3,37,32,49,36,29,44])). % 127.83/127.82 cnf(2368,plain, % 127.83/127.82 (E(f9(f9(a6,a6),f9(a6,a6)),f9(a5,a5))+E(f9(f9(a6,a6),f9(a6,a6)),a6)), % 127.83/127.82 inference(scs_inference,[],[2325,2335,2196,2201,2314,2236,2345,2247,2240,2264,2294,2218,114,2205,2339,2342,2347,174,2,28,31,19,30,18,3,37,32,49,36,29,44,33])). % 127.83/127.82 cnf(2375,plain, % 127.83/127.82 (E(x23751,f9(x23751,x23751))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2378,plain, % 127.83/127.82 (E(x23781,f9(x23781,x23781))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2380,plain, % 127.83/127.82 (~P2(a7,f11(f9(a1,a1)))), % 127.83/127.82 inference(scs_inference,[],[2307,2226,2358,2335,2199,105,2375,32,2,28,31,29])). % 127.83/127.82 cnf(2390,plain, % 127.83/127.82 (~E(f9(f9(a7,a7),a7),f9(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2307,2337,2226,2358,2365,2234,2241,2335,2197,2242,2199,105,2375,2378,32,2,28,31,29,19,30,18,3])). % 127.83/127.82 cnf(2392,plain, % 127.83/127.82 (P2(f9(a5,a5),f9(a8,f9(a8,a8)))), % 127.83/127.82 inference(scs_inference,[],[2307,2337,2226,2358,2365,2234,2241,2335,2207,2197,2242,114,2199,105,2375,2378,32,2,28,31,29,19,30,18,3,37])). % 127.83/127.82 cnf(2395,plain, % 127.83/127.82 (~P2(a7,f10(f9(a1,a1),a1))), % 127.83/127.82 inference(scs_inference,[],[2307,2337,2226,2358,2365,2234,2241,2335,2204,2207,2197,2242,114,2199,105,2375,2378,32,2,28,31,29,19,30,18,3,37,33])). % 127.83/127.82 cnf(2398,plain, % 127.83/127.82 (P2(f4(a8,f11(a5),f9(a8,a8)),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2307,2337,2226,2358,2365,2234,2241,2335,2204,2207,2197,2242,2218,114,2199,105,2375,2378,32,2,28,31,29,19,30,18,3,37,33,40])). % 127.83/127.82 cnf(2401,plain, % 127.83/127.82 (P2(f4(a8,f11(a5),f9(a8,a8)),a8)), % 127.83/127.82 inference(scs_inference,[],[2307,2337,2226,2358,2365,2234,2241,2335,2204,2207,2197,2242,2218,114,2199,105,2375,2378,32,2,28,31,29,19,30,18,3,37,33,40,48])). % 127.83/127.82 cnf(2403,plain, % 127.83/127.82 (~P2(f9(a8,f9(a8,a8)),f9(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2392,32])). % 127.83/127.82 cnf(2412,plain, % 127.83/127.82 (~P2(f9(a1,a1),f11(a7))), % 127.83/127.82 inference(scs_inference,[],[2230,2392,2274,2243,1468,1433,32,2,31,28,30,19])). % 127.83/127.82 cnf(2416,plain, % 127.83/127.82 (E(f3(f9(x24161,x24161),f9(x24162,x24162),f9(x24163,x24163)),f3(x24161,x24162,x24163))), % 127.83/127.82 inference(scs_inference,[],[2351,2206,2230,322,2392,2274,2243,1468,1433,23,32,2,31,28,30,19,18,3])). % 127.83/127.82 cnf(2418,plain, % 127.83/127.82 (~P2(a7,f10(a1,f9(a1,a1)))), % 127.83/127.82 inference(scs_inference,[],[2249,2351,2206,2230,322,2248,2392,2274,2243,1468,1433,23,32,2,31,28,30,19,18,3,33])). % 127.83/127.82 cnf(2429,plain, % 127.83/127.82 (E(x24291,f9(x24291,x24291))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2431,plain, % 127.83/127.82 (~P2(f9(f9(a7,a7),a7),f11(a1))), % 127.83/127.82 inference(scs_inference,[],[2390,2401,2243,439,105,32,2,28,29])). % 127.83/127.82 cnf(2435,plain, % 127.83/127.82 (E(x24351,f9(x24351,x24351))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2442,plain, % 127.83/127.82 (~P2(f9(f9(a1,a1),a1),f11(a7))), % 127.83/127.82 inference(scs_inference,[],[2412,2390,2192,2401,2236,2205,2243,439,105,2429,2435,32,2,28,29,31,30,19,18])). % 127.83/127.82 cnf(2443,plain, % 127.83/127.82 (E(f9(f9(x24431,x24431),x24432),f9(x24431,x24432))), % 127.83/127.82 inference(rename_variables,[],[2205])). % 127.83/127.82 cnf(2444,plain, % 127.83/127.82 (~E(f9(f9(a7,a7),f9(a7,a7)),f9(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2412,2390,2192,2401,2236,2247,2205,2243,439,105,2429,2435,32,2,28,29,31,30,19,18,3])). % 127.83/127.82 cnf(2446,plain, % 127.83/127.82 (~E(f9(f10(a5,a5),x24461),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2412,2390,2192,2401,518,2236,2247,2205,2243,991,439,105,2429,2435,32,2,28,29,31,30,19,18,3,37])). % 127.83/127.82 cnf(2448,plain, % 127.83/127.82 (~P2(f9(f9(a1,a1),f9(a1,a1)),f10(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2412,2390,2262,2192,2401,518,2236,2247,2205,2243,991,439,105,2429,2435,32,2,28,29,31,30,19,18,3,37,46])). % 127.83/127.82 cnf(2450,plain, % 127.83/127.82 (~P2(f9(a1,a1),f9(f9(x24501,x24501),f11(a7)))), % 127.83/127.82 inference(scs_inference,[],[2412,2390,2262,2192,2401,518,2236,2247,2205,2443,2243,991,439,105,2429,2435,32,2,28,29,31,30,19,18,3,37,46,35])). % 127.83/127.82 cnf(2455,plain, % 127.83/127.82 (~P2(f9(a7,a7),f10(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2446,2302,2248,2,19])). % 127.83/127.82 cnf(2456,plain, % 127.83/127.82 (E(f10(x24561,x24562),f10(f9(x24561,x24561),x24562))), % 127.83/127.82 inference(rename_variables,[],[2248])). % 127.83/127.82 cnf(2457,plain, % 127.83/127.82 (~P2(f9(a1,f9(a1,a1)),f10(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2446,2448,2302,2248,2242,2,19,18])). % 127.83/127.82 cnf(2461,plain, % 127.83/127.82 (~P2(f9(a7,a7),f10(a1,f9(a1,a1)))), % 127.83/127.82 inference(scs_inference,[],[2416,2446,2448,2238,2302,2337,2248,2456,2242,2,19,18,3,33])). % 127.83/127.82 cnf(2464,plain, % 127.83/127.82 (~E(f9(x24641,f10(a5,a5)),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2416,2446,2448,2238,2302,520,2337,2248,2456,2242,991,2,19,18,3,33,37])). % 127.83/127.82 cnf(2466,plain, % 127.83/127.82 (~P2(f9(a1,a1),f9(f11(a7),f9(x24661,x24661)))), % 127.83/127.82 inference(scs_inference,[],[2416,2446,2448,2238,2302,520,2337,2248,2456,2412,2207,2242,991,2,19,18,3,33,37,36])). % 127.83/127.82 cnf(2476,plain, % 127.83/127.82 (E(f4(a8,f11(a5),a8),x24761)+~P2(f9(a8,a8),f11(f11(x24761)))), % 127.83/127.82 inference(scs_inference,[],[2300,45])). % 127.83/127.82 cnf(2478,plain, % 127.83/127.82 (~P2(f9(a1,a1),f10(f9(a7,a7),f9(a7,a7)))), % 127.83/127.82 inference(scs_inference,[],[2464,2325,2,46])). % 127.83/127.82 cnf(2480,plain, % 127.83/127.82 (~E(f11(a7),f11(f9(a1,a1)))), % 127.83/127.82 inference(scs_inference,[],[2464,2442,2325,2205,2,46,28])). % 127.83/127.82 cnf(2481,plain, % 127.83/127.82 (E(f9(f9(x24811,x24811),x24812),f9(x24811,x24812))), % 127.83/127.82 inference(rename_variables,[],[2205])). % 127.83/127.82 cnf(2483,plain, % 127.83/127.82 (~P2(f9(a7,a7),f11(f9(a1,a1)))), % 127.83/127.82 inference(scs_inference,[],[2464,2442,2325,2208,2199,2205,2,46,28,29])). % 127.83/127.82 cnf(2490,plain, % 127.83/127.82 (E(f9(f9(x24901,x24901),x24902),f9(x24901,x24902))), % 127.83/127.82 inference(rename_variables,[],[2205])). % 127.83/127.82 cnf(2494,plain, % 127.83/127.82 (E(f9(x24941,x24942),f9(x24941,f9(x24942,x24942)))), % 127.83/127.82 inference(rename_variables,[],[2247])). % 127.83/127.82 cnf(2495,plain, % 127.83/127.82 (~P2(f9(f9(a7,a7),a7),f10(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2455,2464,2442,2466,2325,2208,2247,441,2199,2205,2481,2490,105,2,46,28,29,31,30,19,18])). % 127.83/127.82 cnf(2497,plain, % 127.83/127.82 (~E(f9(a1,f9(a1,a1)),f9(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2455,2464,2442,2466,2325,2208,2247,2494,441,2199,2205,2481,2490,105,2,46,28,29,31,30,19,18,3])). % 127.83/127.82 cnf(2499,plain, % 127.83/127.82 (~E(f9(f10(a6,a5),f10(a6,a5)),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2455,2464,2442,2466,2325,2208,1064,2247,2494,441,2199,2205,2481,2490,26,105,2,46,28,29,31,30,19,18,3,33])). % 127.83/127.82 cnf(2501,plain, % 127.83/127.82 (~E(f10(f9(a5,a5),f9(a5,a5)),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2455,2464,2442,2466,2325,2208,108,1064,2247,2494,441,2199,2205,2481,2490,991,26,105,2,46,28,29,31,30,19,18,3,33,37])). % 127.83/127.82 cnf(2505,plain, % 127.83/127.82 (E(x25051,f9(x25051,x25051))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2515,plain, % 127.83/127.82 (E(f4(x25151,x25152,x25153),f4(x25151,f9(x25152,x25152),f9(x25153,x25153)))), % 127.83/127.82 inference(scs_inference,[],[2501,2495,2237,2478,2240,2236,56,2205,105,2505,2,28,31,30,19,3])). % 127.83/127.82 cnf(2522,plain, % 127.83/127.82 (~P2(f9(a1,f9(a1,a1)),f11(a7))), % 127.83/127.82 inference(scs_inference,[],[2497,2243,2,29])). % 127.83/127.82 cnf(2523,plain, % 127.83/127.82 (E(f11(x25231),f11(f9(x25231,x25231)))), % 127.83/127.82 inference(rename_variables,[],[2243])). % 127.83/127.82 cnf(2525,plain, % 127.83/127.82 (~E(f11(a1),f11(f9(a7,a7)))), % 127.83/127.82 inference(scs_inference,[],[2497,2431,2243,2205,2,29,28])). % 127.83/127.82 cnf(2526,plain, % 127.83/127.82 (E(f9(f9(x25261,x25261),x25262),f9(x25261,x25262))), % 127.83/127.82 inference(rename_variables,[],[2205])). % 127.83/127.82 cnf(2534,plain, % 127.83/127.82 (~P2(f9(a7,a7),f11(a1))), % 127.83/127.82 inference(scs_inference,[],[2497,2431,2483,2243,2523,56,2205,2526,105,2,29,28,31,30,19])). % 127.83/127.82 cnf(2536,plain, % 127.83/127.82 (~E(f9(f9(a1,a1),a1),f9(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2497,2261,2431,2483,2207,2243,2523,56,2205,2526,105,2,29,28,31,30,19,3])). % 127.83/127.82 cnf(2537,plain, % 127.83/127.82 (E(f9(x25371,f9(x25372,x25372)),f9(x25371,x25372))), % 127.83/127.82 inference(rename_variables,[],[2207])). % 127.83/127.82 cnf(2538,plain, % 127.83/127.82 (~P2(f9(f9(a7,a7),f9(a7,a7)),f11(a1))), % 127.83/127.82 inference(scs_inference,[],[2497,2261,2431,2483,2207,2537,2243,2523,56,2205,2526,105,2,29,28,31,30,19,3,18])). % 127.83/127.82 cnf(2544,plain, % 127.83/127.82 (E(x25441,f9(x25441,x25441))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2552,plain, % 127.83/127.82 (~P2(f9(a6,a6),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2536,2522,2344,2248,441,2207,105,2544,2,28,31,30,19])). % 127.83/127.82 cnf(2554,plain, % 127.83/127.82 (E(f2(x25541,x25542),f2(f9(x25541,x25541),f9(x25542,x25542)))), % 127.83/127.82 inference(scs_inference,[],[2536,2522,2244,2246,2344,2248,441,2207,105,2544,2,28,31,30,19,3])). % 127.83/127.82 cnf(2558,plain, % 127.83/127.82 (E(f9(x25581,x25582),f9(f9(x25581,x25581),x25582))), % 127.83/127.82 inference(rename_variables,[],[2242])). % 127.83/127.82 cnf(2559,plain, % 127.83/127.82 (~P2(f9(a7,a7),f9(f11(a1),x25591))), % 127.83/127.82 inference(scs_inference,[],[2534,2536,2522,2538,2244,2246,2344,2248,2242,2247,441,2207,105,2544,2,28,31,30,19,3,18,36])). % 127.83/127.82 cnf(2567,plain, % 127.83/127.82 (~P2(f11(a5),f10(f9(a8,a8),f9(a8,a8)))), % 127.83/127.82 inference(scs_inference,[],[2534,2536,2522,2538,2244,2246,2344,2232,2358,2248,2242,2558,2247,441,2207,105,2544,2,28,31,30,19,3,18,36,35,29,46])). % 127.83/127.82 cnf(2572,plain, % 127.83/127.82 (~E(f10(a5,a6),f9(x25721,f10(a5,a5)))), % 127.83/127.82 inference(scs_inference,[],[2552,2444,1256,2,36,35])). % 127.83/127.82 cnf(2577,plain, % 127.83/127.82 (~E(f10(a5,a5),f11(f9(a6,a6)))), % 127.83/127.82 inference(scs_inference,[],[2552,2444,1256,52,24,105,2,36,35,31,28])). % 127.83/127.82 cnf(2578,plain, % 127.83/127.82 (E(f9(x25781,x25782),f9(x25782,x25781))), % 127.83/127.82 inference(rename_variables,[],[24])). % 127.83/127.82 cnf(2583,plain, % 127.83/127.82 (~P2(f9(a6,a6),f10(a5,f9(a5,a5)))), % 127.83/127.82 inference(scs_inference,[],[2552,2444,2195,1256,52,24,2578,105,2,36,35,31,28,30,19])). % 127.83/127.82 cnf(2585,plain, % 127.83/127.82 (~E(f9(f9(a8,a8),f10(a6,a5)),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2552,2444,2226,2195,1256,2242,52,24,2578,105,2,36,35,31,28,30,19,3])). % 127.83/127.82 cnf(2587,plain, % 127.83/127.82 (~P2(f9(a6,f9(a6,a6)),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2552,2444,2226,2195,1256,2242,2207,52,24,2578,105,2,36,35,31,28,30,19,3,18])). % 127.83/127.82 cnf(2589,plain, % 127.83/127.82 (~E(f10(a5,a5),f9(f10(a5,a6),f10(a5,a6)))), % 127.83/127.82 inference(scs_inference,[],[2552,2444,2226,2195,1256,2242,2207,52,24,2578,105,2,36,35,31,28,30,19,3,18,37])). % 127.83/127.82 cnf(2593,plain, % 127.83/127.82 (E(f9(x25931,x25932),f9(x25931,f9(x25932,x25932)))), % 127.83/127.82 inference(rename_variables,[],[2247])). % 127.83/127.82 cnf(2602,plain, % 127.83/127.82 (E(x26021,f9(x26021,x26021))), % 127.83/127.82 inference(rename_variables,[],[105])). % 127.83/127.82 cnf(2604,plain, % 127.83/127.82 (~E(f11(a5),f11(f9(a6,a6)))), % 127.83/127.82 inference(scs_inference,[],[2585,2587,2403,2296,2247,2593,2207,52,105,2602,2,36,35,31,30,28])). % 127.83/127.82 cnf(2607,plain, % 127.83/127.82 (P2(a6,f9(a8,f10(a6,a5)))), % 127.83/127.82 inference(scs_inference,[],[2585,2587,2403,2296,1439,999,2247,2593,2207,52,105,2602,2,36,35,31,30,28,19])). % 127.83/127.82 cnf(2608,plain, % 127.83/127.82 (E(f4(x26081,x26082,x26083),f4(f9(x26081,x26081),f9(x26082,x26082),f9(x26083,x26083)))), % 127.83/127.82 inference(scs_inference,[],[2585,2587,2515,2403,2296,2241,1439,999,2247,2593,2207,52,105,2602,2,36,35,31,30,28,19,3])). % 127.83/127.82 cnf(2611,plain, % 127.83/127.82 (~P2(f9(f9(a6,a6),f9(a6,a6)),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2585,2587,2515,2403,2296,2241,1439,999,2247,2593,2205,2207,52,105,2602,2,36,35,31,30,28,19,3,18])). % 127.83/127.82 cnf(2613,plain, % 127.83/127.82 (~E(f10(a5,a5),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2585,2587,2515,2403,2296,2241,254,1439,999,2247,2593,2205,2207,52,105,2602,2,36,35,31,30,28,19,3,18,37])). % 127.83/127.82 cnf(2615,plain, % 127.83/127.82 (~E(f9(a8,a8),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2613,2])). % 127.83/127.82 cnf(2616,plain, % 127.83/127.82 (~E(f10(a6,a5),f9(f10(a5,a5),x26161))), % 127.83/127.82 inference(scs_inference,[],[2613,2611,174,2,36])). % 127.83/127.82 cnf(2620,plain, % 127.83/127.82 (~E(f9(a8,f10(a6,a5)),f11(a5))), % 127.83/127.82 inference(scs_inference,[],[2613,2611,2607,174,26,2,36,35,29])). % 127.83/127.82 cnf(2622,plain, % 127.83/127.82 (~P2(f9(a7,a7),f10(f9(a1,a1),f9(a1,a1)))), % 127.83/127.82 inference(scs_inference,[],[2613,2611,2607,2461,2204,174,26,2,36,35,29,19])). % 127.83/127.82 cnf(2624,plain, % 127.83/127.82 (~E(f10(a5,f9(a5,a5)),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2613,2611,2607,2461,2204,174,2236,26,2,36,35,29,19,3])). % 127.83/127.82 cnf(2626,plain, % 127.83/127.82 (~P2(f9(a1,a1),f10(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2613,2611,2607,2457,2461,2204,174,2236,2247,26,2,36,35,29,19,3,18])). % 127.83/127.82 cnf(2629,plain, % 127.83/127.82 (~P2(f9(a1,a1),f9(f10(a7,a7),x26291))), % 127.83/127.82 inference(scs_inference,[],[2626,2624,2247,2,36])). % 127.83/127.82 cnf(2635,plain, % 127.83/127.82 (~E(f10(a7,a7),f11(a1))), % 127.83/127.82 inference(scs_inference,[],[2626,2624,2242,2247,22,2,36,35,28])). % 127.83/127.82 cnf(2636,plain, % 127.83/127.82 (E(f9(x26361,x26361),x26361)), % 127.83/127.82 inference(rename_variables,[],[22])). % 127.83/127.82 cnf(2638,plain, % 127.83/127.82 (~E(f10(a7,a7),f10(x26381,a1))), % 127.83/127.82 inference(scs_inference,[],[2626,2624,2242,2247,22,2636,2,36,35,28,30])). % 127.83/127.82 cnf(2641,plain, % 127.83/127.82 (~P2(f9(a6,a6),f11(a5))), % 127.83/127.82 inference(scs_inference,[],[2626,2624,2181,2243,2242,2247,22,2636,2,36,35,28,30,19])). % 127.83/127.82 cnf(2643,plain, % 127.83/127.82 (E(f4(x26431,x26432,x26433),f4(f9(x26431,x26431),x26432,f9(x26433,x26433)))), % 127.83/127.82 inference(scs_inference,[],[2626,2624,2608,2181,2200,2243,2242,2247,22,2636,2,36,35,28,30,19,3])). % 127.83/127.82 cnf(2648,plain, % 127.83/127.82 (~P2(f9(a8,a8),f10(f10(a5,a5),f10(a5,a5)))), % 127.83/127.82 inference(scs_inference,[],[2615,2626,2624,2608,2181,2200,2243,2242,2247,2205,22,2636,2,36,35,28,30,19,3,18,46])). % 127.83/127.82 cnf(2655,plain, % 127.83/127.82 (~E(f10(x26551,a1),f10(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2638,2])). % 127.83/127.82 cnf(2662,plain, % 127.83/127.82 (~E(f10(f9(a7,a7),a7),f10(x26621,a1))), % 127.83/127.82 inference(scs_inference,[],[2638,2395,2611,2195,2248,254,2,35,36,19,3])). % 127.83/127.82 cnf(2664,plain, % 127.83/127.82 (~P2(f9(f9(a6,a6),a6),f11(a5))), % 127.83/127.82 inference(scs_inference,[],[2638,2641,2395,2611,2195,2248,254,2205,2,35,36,19,3,18])). % 127.83/127.82 cnf(2666,plain, % 127.83/127.82 (~E(f11(a5),f9(f10(a5,a6),f10(a5,a6)))), % 127.83/127.82 inference(scs_inference,[],[2638,2641,2395,2611,2195,2248,254,1256,2205,2,35,36,19,3,18,37])). % 127.83/127.82 cnf(2668,plain, % 127.83/127.82 (E(f4(f11(a5),a8,a8),x26681)+~E(f9(a8,a8),f11(x26681))), % 127.83/127.82 inference(scs_inference,[],[2638,2641,2395,2611,2166,2195,2248,254,1256,2205,2,35,36,19,3,18,37,29])). % 127.83/127.82 cnf(2673,plain, % 127.83/127.82 (~E(f11(a1),f10(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2635,2])). % 127.83/127.82 cnf(2680,plain, % 127.83/127.82 (~E(f10(f9(a1,a1),f9(a1,a1)),f10(a7,x26801))), % 127.83/127.82 inference(scs_inference,[],[2635,2622,2455,2242,2247,22,2,36,35,31])). % 127.83/127.82 cnf(2681,plain, % 127.83/127.82 (E(f9(x26811,x26811),x26811)), % 127.83/127.82 inference(rename_variables,[],[22])). % 127.83/127.82 cnf(2683,plain, % 127.83/127.82 (~E(f10(f9(a1,a1),f9(a1,a1)),f10(x26831,a7))), % 127.83/127.82 inference(scs_inference,[],[2635,2622,2455,2242,2247,22,2681,2,36,35,31,30])). % 127.83/127.82 cnf(2686,plain, % 127.83/127.82 (~P2(a7,f11(a1))), % 127.83/127.82 inference(scs_inference,[],[2635,2622,2380,2455,2243,2242,2247,22,2681,2,36,35,31,30,19])). % 127.83/127.82 cnf(2688,plain, % 127.83/127.82 (~E(f10(x26881,f9(a1,a1)),f10(a7,a7))), % 127.83/127.82 inference(scs_inference,[],[2655,2635,2622,2380,2455,2236,2243,2242,2247,22,2681,2,36,35,31,30,19,3])). % 127.83/127.82 cnf(2702,plain, % 127.83/127.82 (~P2(f9(a1,a1),f9(x27021,f11(a7)))), % 127.83/127.82 inference(scs_inference,[],[2673,2620,2450,2242,2,46,19])). % 127.83/127.82 cnf(2705,plain, % 127.83/127.82 (~P2(f9(a8,a8),f4(f11(a5),a8,f9(a8,a8)))), % 127.83/127.82 inference(scs_inference,[],[2673,2620,2450,2256,2242,22,2,46,19,18])). % 127.83/127.82 cnf(2706,plain, % 127.83/127.82 (E(f9(x27061,x27061),x27061)), % 127.83/127.82 inference(rename_variables,[],[22])). % 127.83/127.82 cnf(2709,plain, % 127.83/127.82 (~E(f10(f10(a5,a5),f10(a5,a5)),f11(a8))), % 127.83/127.82 inference(scs_inference,[],[2673,2620,2648,2450,2256,2243,2242,22,2706,2,46,19,18,3,28])). % 127.83/127.82 cnf(2713,plain, % 127.83/127.82 (~P2(f9(a8,a8),f4(f11(a5),f9(a8,a8),f9(a8,a8)))), % 127.83/127.82 inference(scs_inference,[],[2328,2705,2200,2,19])). % 127.83/127.82 cnf(2715,plain, % 127.83/127.82 (E(f3(x27151,x27152,x27153),f3(f9(x27151,x27151),f9(x27152,x27152),x27153))), % 127.83/127.82 inference(scs_inference,[],[2328,2239,2245,2705,2200,2,19,3])). % 127.83/127.82 cnf(2720,plain, % 127.83/127.82 (~E(f10(a5,f9(a5,a5)),f10(x27201,a6))), % 127.83/127.82 inference(scs_inference,[],[2328,2239,2245,2583,2705,2200,22,105,2,19,3,18,30])). % 127.83/127.82 cnf(2724,plain, % 127.83/127.82 (~P2(a6,f10(f9(a5,a5),a5))), % 127.83/127.82 inference(scs_inference,[],[2680,2204,77,2,19])). % 127.83/127.82 cnf(2725,plain, % 127.83/127.82 (E(f10(f9(x27251,x27251),x27252),f10(x27251,x27252))), % 127.83/127.82 inference(rename_variables,[],[2204])). % 127.83/127.82 cnf(2726,plain, % 127.83/127.82 (~E(f10(a1,f9(a1,a1)),f10(a7,x27261))), % 127.83/127.82 inference(scs_inference,[],[2680,2204,2725,77,2,19,3])). % 127.83/127.82 cnf(2728,plain, % 127.83/127.82 (~P2(f9(f9(a6,a6),f9(a6,a6)),f11(a5))), % 127.83/127.82 inference(scs_inference,[],[2680,2664,2204,2725,2207,77,2,19,3,18])). % 127.83/127.82 cnf(2732,plain, % 127.83/127.82 (E(f4(f11(a5),a8,a8),x27321)+~E(a8,f11(x27321))), % 127.83/127.82 inference(scs_inference,[],[2680,2664,2635,1929,2204,2725,2207,77,2,19,3,18,46,29])). % 127.83/127.82 cnf(2734,plain, % 127.83/127.82 (~E(f4(f11(a5),f9(a8,a8),f9(a8,a8)),f10(a8,x27341))), % 127.83/127.82 inference(scs_inference,[],[2680,2713,2664,2635,1929,2204,2725,2207,77,22,2,19,3,18,46,29,31])). % 127.83/127.82 cnf(2744,plain, % 127.83/127.82 (~P2(a1,f11(a7))), % 127.83/127.82 inference(scs_inference,[],[2683,2728,2317,1278,2243,2,35,36,19])). % 127.83/127.82 cnf(2746,plain, % 127.83/127.82 (E(f3(x27461,x27462,x27463),f3(f9(x27461,x27461),f9(x27462,x27462),f9(x27463,x27463)))), % 127.83/127.82 inference(scs_inference,[],[2683,2728,2715,2317,2238,1278,2243,2,35,36,19,3])). % 127.83/127.82 cnf(2756,plain, % 127.83/127.82 (E(f9(x27561,x27562),f9(x27561,f9(x27562,x27562)))), % 127.83/127.82 inference(rename_variables,[],[2247])). % 127.83/127.82 cnf(2758,plain, % 127.83/127.82 (~P2(a1,f9(f11(a7),x27581))), % 127.83/127.82 inference(scs_inference,[],[2744,2709,2360,2247,2756,2,35,36])). % 127.83/127.82 cnf(2764,plain, % 127.83/127.82 (~E(f10(a1,a1),f10(a7,x27641))), % 127.83/127.82 inference(scs_inference,[],[2744,2709,2726,2702,2360,2195,2247,2756,22,2,35,36,28,3])). % 127.83/127.82 cnf(2769,plain, % 127.83/127.82 (~E(f10(a7,x27691),f10(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2764,2])). % 127.83/127.82 cnf(2774,plain, % 127.83/127.82 (~E(f10(a1,a1),f11(f9(a7,a7)))), % 127.83/127.82 inference(scs_inference,[],[2764,2495,2728,174,2205,2,35,36,28])). % 127.83/127.82 cnf(2775,plain, % 127.83/127.82 (E(f9(f9(x27751,x27751),x27752),f9(x27751,x27752))), % 127.83/127.82 inference(rename_variables,[],[2205])). % 127.83/127.82 cnf(2780,plain, % 127.83/127.82 (~E(f4(f11(a5),f9(a8,a8),a8),f10(a8,x27801))), % 127.83/127.82 inference(scs_inference,[],[2764,2734,2197,2495,2728,174,2205,2775,2,35,36,28,30,3])). % 127.83/127.82 cnf(2787,plain, % 127.83/127.82 (E(f9(x27871,x27872),f9(x27871,f9(x27872,x27872)))), % 127.83/127.82 inference(rename_variables,[],[2247])). % 127.83/127.82 cnf(2793,plain, % 127.83/127.82 (E(f9(x27931,x27931),x27931)), % 127.83/127.82 inference(rename_variables,[],[22])). % 127.83/127.82 cnf(2795,plain, % 127.83/127.82 (~E(f9(f10(a7,a7),x27951),f10(x27952,a1))), % 127.83/127.82 inference(scs_inference,[],[2662,2758,2629,2686,2247,2787,22,2793,2,35,36,28,30])). % 127.83/127.82 cnf(2796,plain, % 127.83/127.82 (E(f9(x27961,x27961),x27961)), % 127.83/127.82 inference(rename_variables,[],[22])). % 127.83/127.82 cnf(2798,plain, % 127.83/127.82 (~E(f10(f9(a7,a7),x27981),f10(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2769,2662,2758,2629,2686,2248,2247,2787,22,2793,2,35,36,28,30,3])). % 127.83/127.82 cnf(2799,plain, % 127.83/127.82 (~E(f10(a7,x27991),f10(a1,a1))), % 127.83/127.82 inference(rename_variables,[],[2769])). % 127.83/127.82 cnf(2801,plain, % 127.83/127.82 (~P2(f9(a6,a6),f9(f10(a5,a5),x28011))), % 127.83/127.82 inference(scs_inference,[],[2769,2662,2758,2629,2686,518,2248,2247,2787,22,2793,2796,2,35,36,28,30,3,18])). % 127.83/127.82 cnf(2802,plain, % 127.83/127.82 (E(f9(x28021,x28021),x28021)), % 127.83/127.82 inference(rename_variables,[],[22])). % 127.83/127.82 cnf(2803,plain, % 127.83/127.82 (~P2(f10(a7,x28031),f10(f10(a1,a1),f10(a1,a1)))), % 127.83/127.82 inference(scs_inference,[],[2769,2799,2662,2758,2629,2686,518,2248,2247,2787,22,2793,2796,2,35,36,28,30,3,18,46])). % 127.83/127.82 cnf(2805,plain, % 127.83/127.82 (~E(f9(f10(a7,a7),x28051),f10(a1,x28052))), % 127.83/127.82 inference(scs_inference,[],[2769,2799,2662,2758,2629,2686,518,2248,2247,2787,22,2793,2796,2802,2,35,36,28,30,3,18,46,31])). % 127.83/127.82 cnf(2813,plain, % 127.83/127.82 (~P2(f9(a6,a6),f9(x28131,f10(a5,a5)))), % 127.83/127.82 inference(scs_inference,[],[2720,2801,24,2,19])). % 127.83/127.82 cnf(2821,plain, % 127.83/127.82 (~E(f10(f9(a5,a5),a5),f9(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2720,2780,2801,2724,2803,2200,2166,991,23,24,2,19,3,18,33,37])). % 127.83/127.82 cnf(2825,plain, % 127.83/127.82 (~E(f9(a8,a8),f11(f10(a8,x28251)))), % 127.83/127.82 inference(scs_inference,[],[2720,2780,2801,2724,2803,2200,2166,991,23,24,2,19,3,18,33,37,2732,2668])). % 127.83/127.82 cnf(2827,plain, % 127.83/127.82 (~E(f9(f10(a5,a5),x28271),f10(x28272,a6))), % 127.83/127.82 inference(scs_inference,[],[2720,2780,2801,2724,2803,2200,2166,991,23,24,22,2,19,3,18,33,37,2732,2668,30])). % 127.83/127.82 cnf(2831,plain, % 127.83/127.82 (~E(f9(a8,f9(a8,a8)),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2821,2615,2247,2,3])). % 127.83/127.82 cnf(2841,plain, % 127.83/127.82 (~P2(a7,f9(f9(x28411,x28411),f11(a1)))), % 127.83/127.82 inference(scs_inference,[],[2831,2746,2196,2686,2205,2,3,35])). % 127.83/127.82 cnf(2856,plain, % 127.83/127.82 (~E(f9(f9(a8,a8),a8),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2827,2655,2230,2207,2,46,3])). % 127.83/127.82 cnf(2858,plain, % 127.83/127.82 (~P2(f10(f9(a5,a5),a6),a6)), % 127.83/127.82 inference(scs_inference,[],[2827,2655,2230,1262,2204,2207,2,46,3,18])). % 127.83/127.82 cnf(2859,plain, % 127.83/127.82 (E(f10(f9(x28591,x28591),x28592),f10(x28591,x28592))), % 127.83/127.82 inference(rename_variables,[],[2204])). % 127.83/127.82 cnf(2861,plain, % 127.83/127.82 (E(f10(f9(x28611,x28611),x28612),f10(x28611,x28612))), % 127.83/127.82 inference(rename_variables,[],[2204])). % 127.83/127.82 cnf(2866,plain, % 127.83/127.82 (~P2(f10(f9(a5,a5),a6),f9(a6,a6))), % 127.83/127.82 inference(scs_inference,[],[2827,2655,2230,1262,2204,2859,2861,2207,22,2,46,3,18,31,30,19])). % 127.83/127.82 cnf(2873,plain, % 127.83/127.82 (~P2(f10(f9(a5,a5),a6),f9(a6,x28731))), % 127.83/127.82 inference(scs_inference,[],[2856,2858,2247,2,36])). % 127.83/127.82 cnf(2877,plain, % 127.83/127.82 (E(f10(f9(x28771,x28771),x28772),f10(x28771,x28772))), % 127.83/127.82 inference(rename_variables,[],[2204])). % 127.83/127.82 cnf(2880,plain, % 127.83/127.82 (E(f10(f9(x28801,x28801),x28802),f10(x28801,x28802))), % 127.83/127.82 inference(rename_variables,[],[2204])). % 127.83/127.82 cnf(2885,plain, % 127.83/127.82 (~E(f4(f11(a5),a8,f9(a8,a8)),f10(a8,x28851))), % 127.83/127.82 inference(scs_inference,[],[2856,2866,2858,2734,2200,2204,2877,2880,2247,2,36,31,28,30,3])). % 127.83/127.82 cnf(2887,plain, % 127.83/127.82 (~P2(f10(f9(a5,a5),f9(a6,a6)),f9(a6,a6))), % 127.83/127.82 inference(scs_inference,[],[2856,2866,2858,2734,2200,2195,2204,2877,2880,2247,2,36,31,28,30,3,18])). % 127.83/127.82 cnf(2889,plain, % 127.83/127.82 (~P2(x28891,f2(x28892,x28893))+P2(x28891,f2(f9(x28892,x28892),f9(x28893,x28893)))), % 127.83/127.82 inference(scs_inference,[],[2856,2866,2554,2858,2734,2200,2195,2204,2877,2880,2247,2,36,31,28,30,3,18,19])). % 127.83/127.82 cnf(2897,plain, % 127.83/127.82 (~P2(f11(a5),f10(f9(a8,a8),a8))), % 127.83/127.82 inference(scs_inference,[],[2805,2567,2236,2,19])). % 127.83/127.82 cnf(2898,plain, % 127.83/127.82 (E(f10(x28981,x28982),f10(x28981,f9(x28982,x28982)))), % 127.83/127.82 inference(rename_variables,[],[2236])). % 127.83/127.82 cnf(2899,plain, % 127.83/127.82 (~E(f9(a7,f9(a7,a7)),f9(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2805,2567,2444,2236,2205,2,19,3])). % 127.83/127.82 cnf(2903,plain, % 127.83/127.82 (~P2(f10(a5,a5),f10(f9(a8,a8),a8))), % 127.83/127.82 inference(scs_inference,[],[2805,2567,2444,2613,97,2236,2898,2205,22,2,19,3,18,33])). % 127.83/127.82 cnf(2906,plain, % 127.83/127.82 (E(f4(f9(a8,a8),f11(a5),a8),x29061)+~E(f9(a8,a8),f11(x29061))), % 127.83/127.82 inference(scs_inference,[],[2805,2567,2444,2613,97,2298,2236,2898,2205,22,2,19,3,18,33,29])). % 127.83/127.82 cnf(2913,plain, % 127.83/127.82 (~P2(f10(a5,a5),f10(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2899,2903,2638,2248,2,46,19])). % 127.83/127.82 cnf(2914,plain, % 127.83/127.82 (E(f10(x29141,x29142),f10(f9(x29141,x29141),x29142))), % 127.83/127.82 inference(rename_variables,[],[2248])). % 127.83/127.82 cnf(2915,plain, % 127.83/127.82 (~E(f10(x29151,f9(a7,a7)),f10(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2899,2798,2903,2638,2248,23,2,46,19,3])). % 127.83/127.82 cnf(2917,plain, % 127.83/127.82 (~P2(f10(a5,f9(a6,a6)),f9(a6,a6))), % 127.83/127.82 inference(scs_inference,[],[2887,2899,2798,2903,2638,2248,2914,23,2,46,19,3,18])). % 127.83/127.82 cnf(2919,plain, % 127.83/127.82 (~P2(f10(f9(a5,a5),a6),f9(x29191,a6))), % 127.83/127.82 inference(scs_inference,[],[2887,2899,2798,2903,2858,2638,2248,2914,23,2242,2,46,19,3,18,35])). % 127.83/127.82 cnf(2925,plain, % 127.83/127.82 (E(f10(f9(x29251,x29251),x29252),f10(x29251,x29252))), % 127.83/127.82 inference(rename_variables,[],[2204])). % 127.83/127.82 cnf(2928,plain, % 127.83/127.82 (E(f10(f9(x29281,x29281),x29282),f10(x29281,x29282))), % 127.83/127.82 inference(rename_variables,[],[2204])). % 127.83/127.82 cnf(2933,plain, % 127.83/127.82 (~P2(f10(a5,a5),f10(a8,f9(a8,a8)))), % 127.83/127.82 inference(scs_inference,[],[2913,2919,2795,2195,2204,2925,2928,2,31,28,30,19])). % 127.83/127.82 cnf(2934,plain, % 127.83/127.82 (E(f10(x29341,f9(x29342,x29342)),f10(x29341,x29342))), % 127.83/127.82 inference(rename_variables,[],[2195])). % 127.83/127.82 cnf(2935,plain, % 127.83/127.82 (~E(f10(x29351,a7),f10(a1,a1))), % 127.83/127.82 inference(scs_inference,[],[2913,2915,2919,2795,2195,2934,2204,2925,2928,2,31,28,30,19,3])). % 127.83/127.82 cnf(2937,plain, % 127.83/127.82 (E(f10(x29371,f9(x29372,x29372)),f10(x29371,x29372))), % 127.83/127.82 inference(rename_variables,[],[2195])). % 127.83/127.82 cnf(2938,plain, % 127.83/127.82 (~P2(f10(a5,f9(a5,a5)),f10(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2913,2915,2919,2795,2195,2934,2937,2204,2925,2928,2,31,28,30,19,3,18])). % 127.83/127.82 cnf(2940,plain, % 127.83/127.82 (~E(f10(a1,a1),f10(x29401,a7))), % 127.83/127.82 inference(scs_inference,[],[2935,2])). % 127.83/127.82 cnf(2942,plain, % 127.83/127.82 (E(f10(x29421,f9(x29422,x29422)),f10(x29421,x29422))), % 127.83/127.82 inference(rename_variables,[],[2195])). % 127.83/127.82 cnf(2947,plain, % 127.83/127.82 (~P2(f11(a5),f10(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2935,2938,2897,2248,2195,2942,2,28,30,19])). % 127.83/127.82 cnf(2949,plain, % 127.83/127.82 (~P2(f10(f9(a5,a5),f9(a5,a5)),f10(a8,a8))), % 127.83/127.82 inference(scs_inference,[],[2935,2938,2897,2248,2195,2942,2204,2,28,30,19,18])). % 127.83/127.82 cnf(2951,plain, % 127.83/127.82 (~E(f10(a6,a5),f10(a5,a5))), % 127.83/127.82 inference(scs_inference,[],[2935,2499,2938,2897,2248,2195,2942,2204,22,2,28,30,19,18,3])). % 127.83/127.82 cnf(2953,plain, % 127.83/127.82 (~P2(f10(a5,a5),f9(f10(a8,a8),f9(x29531,x29531)))), % 127.83/127.82 inference(scs_inference,[],[2935,2499,2938,2897,2913,2248,2195,2942,2204,2207,22,2,28,30,19,18,3,36])). % 127.83/127.82 cnf(2956,plain, % 127.83/127.83 (~E(f10(a5,a5),f10(a6,a5))), % 127.83/127.83 inference(scs_inference,[],[2951,2])). % 127.83/127.83 cnf(2960,plain, % 127.83/127.83 (E(f11(f9(x29601,x29601)),f11(x29601))), % 127.83/127.83 inference(rename_variables,[],[2199])). % 127.83/127.83 cnf(2961,plain, % 127.83/127.83 (~E(f10(a6,f9(a5,a5)),f10(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[2951,2947,2199,2236,2195,2,19,18,3])). % 127.83/127.83 cnf(2963,plain, % 127.83/127.83 (~E(f10(a8,a8),f10(f11(a5),x29631))), % 127.83/127.83 inference(scs_inference,[],[2951,2947,2199,2960,2236,2195,2,19,18,3,31])). % 127.83/127.83 cnf(2964,plain, % 127.83/127.83 (E(f11(f9(x29641,x29641)),f11(x29641))), % 127.83/127.83 inference(rename_variables,[],[2199])). % 127.83/127.83 cnf(2967,plain, % 127.83/127.83 (E(f11(f9(x29671,x29671)),f11(x29671))), % 127.83/127.83 inference(rename_variables,[],[2199])). % 127.83/127.83 cnf(2969,plain, % 127.83/127.83 (~E(f10(a8,a8),f10(x29691,f11(a5)))), % 127.83/127.83 inference(scs_inference,[],[2951,2947,2199,2960,2964,2967,2236,2195,2,19,18,3,31,28,30])). % 127.83/127.83 cnf(2977,plain, % 127.83/127.83 (~E(f9(x29771,f10(a5,a5)),f10(a6,x29772))), % 127.83/127.83 inference(scs_inference,[],[2961,2813,22,2,31])). % 127.83/127.83 cnf(2978,plain, % 127.83/127.83 (E(f9(x29781,x29781),x29781)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(2984,plain, % 127.83/127.83 (E(f9(x29841,x29842),f9(x29841,f9(x29842,x29842)))), % 127.83/127.83 inference(rename_variables,[],[2247])). % 127.83/127.83 cnf(2986,plain, % 127.83/127.83 (E(f10(x29861,x29862),f10(x29861,f9(x29862,x29862)))), % 127.83/127.83 inference(rename_variables,[],[2236])). % 127.83/127.83 cnf(2987,plain, % 127.83/127.83 (~E(f10(a5,f9(a5,a5)),f10(a6,a5))), % 127.83/127.83 inference(scs_inference,[],[2956,2961,2813,2949,2953,2236,2986,2247,22,2978,2,31,28,19,18,3])). % 127.83/127.83 cnf(2989,plain, % 127.83/127.83 (~P2(f10(a5,f9(a6,a6)),f9(x29891,a6))), % 127.83/127.83 inference(scs_inference,[],[2956,2961,2813,2949,2953,2917,2236,2986,2247,2984,22,2978,2,31,28,19,18,3,35])). % 127.83/127.83 cnf(2994,plain, % 127.83/127.83 (E(f10(f9(x29941,x29941),x29942),f10(x29941,x29942))), % 127.83/127.83 inference(rename_variables,[],[2204])). % 127.83/127.83 cnf(2995,plain, % 127.83/127.83 (~P2(f10(f9(a5,a5),f9(a6,a6)),f9(x29951,a6))), % 127.83/127.83 inference(scs_inference,[],[2987,2989,2933,2204,2994,2,19,18])). % 127.83/127.83 cnf(2997,plain, % 127.83/127.83 (~E(f10(f9(a1,a1),a1),f10(x29971,a7))), % 127.83/127.83 inference(scs_inference,[],[2940,2987,2989,2933,2248,2204,2994,2,19,18,3])). % 127.83/127.83 cnf(3002,plain, % 127.83/127.83 (~P2(f10(f9(a5,a5),f9(a6,a6)),f9(a6,x30021))), % 127.83/127.83 inference(scs_inference,[],[2977,2995,24,2,19])). % 127.83/127.83 cnf(3004,plain, % 127.83/127.83 (~E(f10(f9(a1,a1),x30041),f10(a7,a7))), % 127.83/127.83 inference(scs_inference,[],[2688,2977,2995,23,24,2,19,3])). % 127.83/127.83 cnf(3021,plain, % 127.83/127.83 (~P2(a7,f10(a1,a1))), % 127.83/127.83 inference(scs_inference,[],[2997,2418,2956,2236,2,46,19])). % 127.83/127.83 cnf(3022,plain, % 127.83/127.83 (E(f10(x30221,x30222),f10(x30221,f9(x30222,x30222)))), % 127.83/127.83 inference(rename_variables,[],[2236])). % 127.83/127.83 cnf(3023,plain, % 127.83/127.83 (~P2(f11(f9(a6,a6)),a6)), % 127.83/127.83 inference(scs_inference,[],[2997,2418,2956,359,2199,2236,2,46,19,18])). % 127.83/127.83 cnf(3025,plain, % 127.83/127.83 (~E(f10(a1,f9(a1,a1)),f10(x30251,a7))), % 127.83/127.83 inference(scs_inference,[],[2997,2418,2956,2940,359,2199,2236,3022,2,46,19,18,3])). % 127.83/127.83 cnf(3044,plain, % 127.83/127.83 (~P2(a7,f9(f9(x30441,x30441),f10(a1,a1)))), % 127.83/127.83 inference(scs_inference,[],[3021,3025,2873,2841,2416,2239,2204,2205,2242,2,28,19,3,35])). % 127.83/127.83 cnf(3065,plain, % 127.83/127.83 (~P2(f10(f9(a5,a5),f9(a6,a6)),a6)), % 127.83/127.83 inference(scs_inference,[],[2885,3023,2858,2195,22,2,19,18])). % 127.83/127.83 cnf(3067,plain, % 127.83/127.83 (~E(f10(f9(a7,a7),f9(a7,a7)),f10(x30671,a1))), % 127.83/127.83 inference(scs_inference,[],[2885,3023,2662,2858,2195,2236,22,2,19,18,3])). % 127.83/127.83 cnf(3069,plain, % 127.83/127.83 (~P2(f11(f9(a6,a6)),f9(a6,x30691))), % 127.83/127.83 inference(scs_inference,[],[2885,3023,2662,2858,2195,2236,2247,22,2,19,18,3,36])). % 127.83/127.83 cnf(3075,plain, % 127.83/127.83 (~P2(f10(a5,f9(a6,a6)),a6)), % 127.83/127.83 inference(scs_inference,[],[3067,3065,3044,2248,2242,2,19,18])). % 127.83/127.83 cnf(3077,plain, % 127.83/127.83 (~E(f10(a1,x30771),f10(a7,a7))), % 127.83/127.83 inference(scs_inference,[],[3004,3067,3065,3044,2248,2204,2242,2,19,18,3])). % 127.83/127.83 cnf(3079,plain, % 127.83/127.83 (~E(f10(a7,a7),f10(a1,x30791))), % 127.83/127.83 inference(scs_inference,[],[3077,2])). % 127.83/127.83 cnf(3081,plain, % 127.83/127.83 (E(f10(x30811,f9(x30812,x30812)),f10(x30811,x30812))), % 127.83/127.83 inference(rename_variables,[],[2195])). % 127.83/127.83 cnf(3083,plain, % 127.83/127.83 (~P2(f10(a6,f9(a5,a5)),a6)), % 127.83/127.83 inference(scs_inference,[],[3077,3075,166,2195,3081,2,28,18])). % 127.83/127.83 cnf(3084,plain, % 127.83/127.83 (E(f10(x30841,f9(x30842,x30842)),f10(x30841,x30842))), % 127.83/127.83 inference(rename_variables,[],[2195])). % 127.83/127.83 cnf(3085,plain, % 127.83/127.83 (~E(f10(a5,a5),f10(x30851,a6))), % 127.83/127.83 inference(scs_inference,[],[3077,3075,2720,166,2195,3081,3084,2,28,18,3])). % 127.83/127.83 cnf(3094,plain, % 127.83/127.83 (~E(f10(x30941,a6),f10(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[3085,2])). % 127.83/127.83 cnf(3102,plain, % 127.83/127.83 (~E(f10(f9(a5,a5),a5),f10(x31021,a6))), % 127.83/127.83 inference(scs_inference,[],[3085,3083,3069,2248,2195,24,2,46,28,19,3])). % 127.83/127.83 cnf(3104,plain, % 127.83/127.83 (~P2(f10(f9(a6,a6),f9(a5,a5)),a6)), % 127.83/127.83 inference(scs_inference,[],[3085,3083,3069,2248,2195,2204,24,2,46,28,19,3,18])). % 127.83/127.83 cnf(3106,plain, % 127.83/127.83 (~P2(f11(a5),f9(f9(x31061,x31061),f10(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[3085,3083,3069,2947,2248,2195,2204,2205,24,2,46,28,19,3,18,35])). % 127.83/127.83 cnf(3113,plain, % 127.83/127.83 (~P2(f10(f9(a6,a6),f9(a5,a5)),f9(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3102,3104,22,2,19])). % 127.83/127.83 cnf(3115,plain, % 127.83/127.83 (~E(f10(x31151,f9(a6,a6)),f10(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[3094,3102,3104,2236,22,2,19,3])). % 127.83/127.83 cnf(3117,plain, % 127.83/127.83 (E(f10(x31171,x31172),f10(x31171,f9(x31172,x31172)))), % 127.83/127.83 inference(rename_variables,[],[2236])). % 127.83/127.83 cnf(3118,plain, % 127.83/127.83 (~P2(f10(f9(a6,a6),a5),a6)), % 127.83/127.83 inference(scs_inference,[],[3094,3102,3104,2236,3117,22,2,19,3,18])). % 127.83/127.83 cnf(3120,plain, % 127.83/127.83 (~P2(a7,f9(f10(a1,a1),f9(x31201,x31201)))), % 127.83/127.83 inference(scs_inference,[],[3094,3102,3104,3021,2236,3117,2207,22,2,19,3,18,36])). % 127.83/127.83 cnf(3128,plain, % 127.83/127.83 (~E(f10(f9(a7,a7),a7),f10(a1,x31281))), % 127.83/127.83 inference(scs_inference,[],[3079,2213,3120,2248,2247,2,19,3])). % 127.83/127.83 cnf(3129,plain, % 127.83/127.83 (E(f10(x31291,x31292),f10(f9(x31291,x31291),x31292))), % 127.83/127.83 inference(rename_variables,[],[2248])). % 127.83/127.83 cnf(3130,plain, % 127.83/127.83 (~P2(f10(a6,f9(a5,a5)),f9(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3079,3113,2213,3120,2248,3129,2247,2,19,3,18])). % 127.83/127.83 cnf(3134,plain, % 127.83/127.83 (E(f10(x31341,f9(x31342,x31342)),f10(x31341,x31342))), % 127.83/127.83 inference(rename_variables,[],[2195])). % 127.83/127.83 cnf(3137,plain, % 127.83/127.83 (E(f10(x31371,f9(x31372,x31372)),f10(x31371,x31372))), % 127.83/127.83 inference(rename_variables,[],[2195])). % 127.83/127.83 cnf(3144,plain, % 127.83/127.83 (~E(f10(f9(a7,a7),f9(a7,a7)),f10(a1,x31441))), % 127.83/127.83 inference(scs_inference,[],[3130,3128,3118,2195,3134,3137,2236,22,2,31,30,28,19,3])). % 127.83/127.83 cnf(3146,plain, % 127.83/127.83 (~P2(f9(f9(a8,a8),a8),a6)), % 127.83/127.83 inference(scs_inference,[],[3130,3128,3118,335,2195,3134,3137,2236,2205,22,2,31,30,28,19,3,18])). % 127.83/127.83 cnf(3151,plain, % 127.83/127.83 (~E(f10(f9(a6,a6),x31511),f10(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[3115,3144,23,2,3])). % 127.83/127.83 cnf(3153,plain, % 127.83/127.83 (~P2(f9(a8,f9(a8,a8)),a6)), % 127.83/127.83 inference(scs_inference,[],[3115,3144,3146,23,24,2,3,18])). % 127.83/127.83 cnf(3164,plain, % 127.83/127.83 (~E(f10(f9(a5,a5),f9(a5,a5)),f10(a6,a5))), % 127.83/127.83 inference(scs_inference,[],[2223,3153,2987,2248,22,2,19,3])). % 127.83/127.83 cnf(3165,plain, % 127.83/127.83 (E(f10(x31651,x31652),f10(f9(x31651,x31651),x31652))), % 127.83/127.83 inference(rename_variables,[],[2248])). % 127.83/127.83 cnf(3166,plain, % 127.83/127.83 (~P2(f10(a5,f9(a6,a6)),f9(a6,x31661))), % 127.83/127.83 inference(scs_inference,[],[2223,3153,2987,3002,2248,3165,22,2,19,3,18])). % 127.83/127.83 cnf(3171,plain, % 127.83/127.83 (~P2(f11(a5),f9(f10(a8,a8),f9(x31711,x31711)))), % 127.83/127.83 inference(scs_inference,[],[2223,3106,3153,2987,3002,2947,2248,3165,2207,2247,22,2,19,3,18,37,36])). % 127.83/127.83 cnf(3177,plain, % 127.83/127.83 (~P2(f10(a5,a5),f9(f9(x31771,x31771),f10(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[3164,2913,2205,2,35])). % 127.83/127.83 cnf(3181,plain, % 127.83/127.83 (E(f10(x31811,f9(x31812,x31812)),f10(x31811,x31812))), % 127.83/127.83 inference(rename_variables,[],[2195])). % 127.83/127.83 cnf(3186,plain, % 127.83/127.83 (~E(f10(a6,x31861),f10(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[3151,3164,3166,2913,2195,3181,2204,2205,2,35,31,30,3])). % 127.83/127.83 cnf(3188,plain, % 127.83/127.83 (~P2(f10(f9(a6,a6),a5),f9(a6,x31881))), % 127.83/127.83 inference(scs_inference,[],[3151,3164,3166,2913,2195,3181,2204,23,2205,2,35,31,30,3,18])). % 127.83/127.83 cnf(3198,plain, % 127.83/127.83 (~E(f10(a5,a5),f10(a6,x31981))), % 127.83/127.83 inference(scs_inference,[],[3186,2])). % 127.83/127.83 cnf(3204,plain, % 127.83/127.83 (~E(f10(f9(a5,a5),f9(a5,a5)),f10(x32041,a6))), % 127.83/127.83 inference(scs_inference,[],[3186,3177,3102,2236,2242,2,46,19,3])). % 127.83/127.83 cnf(3206,plain, % 127.83/127.83 (~P2(f9(f10(a6,a5),f9(a8,a8)),a6)), % 127.83/127.83 inference(scs_inference,[],[3186,3177,3102,134,2236,2242,2207,2,46,19,3,18])). % 127.83/127.83 cnf(3214,plain, % 127.83/127.83 (~E(f10(f9(a5,a5),a5),f10(a6,x32141))), % 127.83/127.83 inference(scs_inference,[],[3198,3188,3204,2248,2204,2,28,3])). % 127.83/127.83 cnf(3216,plain, % 127.83/127.83 (~P2(f10(f9(a6,a6),f9(a5,a5)),f9(a6,x32161))), % 127.83/127.83 inference(scs_inference,[],[3198,3188,3204,2248,2195,2204,2,28,3,18])). % 127.83/127.83 cnf(3232,plain, % 127.83/127.83 (~E(f10(f9(a5,a5),f9(a5,a5)),f10(a6,x32321))), % 127.83/127.83 inference(scs_inference,[],[3214,3171,3198,2236,2247,2,46,19,3])). % 127.83/127.83 cnf(3248,plain, % 127.83/127.83 (~P2(x32481,f2(f9(x32482,x32482),x32483))+P2(x32481,f2(x32482,x32483))), % 127.83/127.83 inference(scs_inference,[],[3216,3232,2202,2248,2204,2,3,18,19])). % 127.83/127.83 cnf(3313,plain, % 127.83/127.83 (~P2(f9(a6,a6),f9(f11(a5),x33131))), % 127.83/127.83 inference(scs_inference,[],[2572,2262,101,2205,22,2,3,18])). % 127.83/127.83 cnf(3322,plain, % 127.83/127.83 (~E(f9(f10(a5,a6),f10(a5,a6)),f10(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[2589,2])). % 127.83/127.83 cnf(3323,plain, % 127.83/127.83 (~P2(f9(f10(a6,a5),f9(a8,a8)),f9(x33231,a6))), % 127.83/127.83 inference(scs_inference,[],[2589,3206,2242,2,35])). % 127.83/127.83 cnf(3330,plain, % 127.83/127.83 (E(f9(x33301,x33301),x33301)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3332,plain, % 127.83/127.83 (~E(f9(f11(a5),x33321),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[2589,3313,2206,2746,3206,2242,22,3330,2,35,3,31,28])). % 127.83/127.83 cnf(3359,plain, % 127.83/127.83 (~E(f11(f11(a6)),a6)), % 127.83/127.83 inference(scs_inference,[],[2211,2])). % 127.83/127.83 cnf(3363,plain, % 127.83/127.83 (~E(f11(f9(a8,a8)),a5)), % 127.83/127.83 inference(scs_inference,[],[2253,2])). % 127.83/127.83 cnf(3368,plain, % 127.83/127.83 (~E(f11(f9(a7,a7)),f11(a1))), % 127.83/127.83 inference(scs_inference,[],[2525,2])). % 127.83/127.83 cnf(3369,plain, % 127.83/127.83 (~P2(f9(f9(a8,a8),f10(a6,a5)),f9(x33691,a6))), % 127.83/127.83 inference(scs_inference,[],[2525,3323,24,2,18])). % 127.83/127.83 cnf(3374,plain, % 127.83/127.83 (~P2(f11(f9(a8,a8)),f10(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[2525,3363,3323,2205,24,2,18,37,46])). % 127.83/127.83 cnf(3383,plain, % 127.83/127.83 (E(f11(f9(x33831,x33831)),f11(x33831))), % 127.83/127.83 inference(rename_variables,[],[2199])). % 127.83/127.83 cnf(3385,plain, % 127.83/127.83 (~E(f10(a5,a5),f10(x33851,f11(a8)))), % 127.83/127.83 inference(scs_inference,[],[3374,2480,2199,3383,2,31,30])). % 127.83/127.83 cnf(3386,plain, % 127.83/127.83 (E(f11(f9(x33861,x33861)),f11(x33861))), % 127.83/127.83 inference(rename_variables,[],[2199])). % 127.83/127.83 cnf(3389,plain, % 127.83/127.83 (E(f11(f9(x33891,x33891)),f11(x33891))), % 127.83/127.83 inference(rename_variables,[],[2199])). % 127.83/127.83 cnf(3391,plain, % 127.83/127.83 (~E(f11(a7),f11(a1))), % 127.83/127.83 inference(scs_inference,[],[3374,3368,2480,2199,3383,3386,3389,2,31,30,28,3])). % 127.83/127.83 cnf(3393,plain, % 127.83/127.83 (~E(f11(a1),f11(a7))), % 127.83/127.83 inference(scs_inference,[],[3391,2])). % 127.83/127.83 cnf(3395,plain, % 127.83/127.83 (~E(f9(f11(a1),f11(a1)),f11(a7))), % 127.83/127.83 inference(scs_inference,[],[3393,2604,105,2,3])). % 127.83/127.83 cnf(3397,plain, % 127.83/127.83 (~P2(x33971,f2(x33972,x33973))+P2(x33971,f2(x33972,f9(x33973,x33973)))), % 127.83/127.83 inference(scs_inference,[],[3393,2604,2244,105,2,3,19])). % 127.83/127.83 cnf(3406,plain, % 127.83/127.83 (~E(f11(a8),a5)), % 127.83/127.83 inference(scs_inference,[],[3395,3391,3363,2199,2,46,3])). % 127.83/127.83 cnf(3408,plain, % 127.83/127.83 (~P2(f11(a8),f10(f9(a5,a5),a5))), % 127.83/127.83 inference(scs_inference,[],[3395,3391,3363,2199,2204,2,46,3,33])). % 127.83/127.83 cnf(3413,plain, % 127.83/127.83 (~E(a5,f11(a8))), % 127.83/127.83 inference(scs_inference,[],[3406,2])). % 127.83/127.83 cnf(3418,plain, % 127.83/127.83 (~P2(f11(a8),f10(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[3406,3408,23,105,2,19,3,46])). % 127.83/127.83 cnf(3421,plain, % 127.83/127.83 (~E(f9(f10(a5,a5),x34211),f10(a6,a5))), % 127.83/127.83 inference(scs_inference,[],[2616,2])). % 127.83/127.83 cnf(3422,plain, % 127.83/127.83 (~E(a8,f11(f11(a8)))), % 127.83/127.83 inference(scs_inference,[],[21,3413,2616,2,29])). % 127.83/127.83 cnf(3426,plain, % 127.83/127.83 (~E(f9(a5,a5),f11(a8))), % 127.83/127.83 inference(scs_inference,[],[21,3413,3369,2616,24,105,2,29,19,3])). % 127.83/127.83 cnf(3428,plain, % 127.83/127.83 (~E(a8,f10(f11(a8),f11(a8)))), % 127.83/127.83 inference(scs_inference,[],[21,3413,3369,2616,24,105,2,29,19,3,33])). % 127.83/127.83 cnf(3430,plain, % 127.83/127.83 (~P2(f11(a8),f9(f10(a5,a5),f9(x34301,x34301)))), % 127.83/127.83 inference(scs_inference,[],[21,3418,3413,3369,2616,2207,24,105,2,29,19,3,33,36])). % 127.83/127.83 cnf(3435,plain, % 127.83/127.83 (E(f9(x34351,x34352),f9(f9(x34351,x34351),x34352))), % 127.83/127.83 inference(rename_variables,[],[2242])). % 127.83/127.83 cnf(3437,plain, % 127.83/127.83 (~P2(f11(a8),f11(f9(a5,a5)))), % 127.83/127.83 inference(scs_inference,[],[3426,3418,3406,2199,2242,2,35,29])). % 127.83/127.83 cnf(3443,plain, % 127.83/127.83 (~E(f9(f9(a5,a5),a5),f11(a8))), % 127.83/127.83 inference(scs_inference,[],[3426,3430,3418,3406,2199,2242,3435,2247,2,35,29,19,3])). % 127.83/127.83 cnf(3446,plain, % 127.83/127.83 (~P2(f11(a8),f11(a5))), % 127.83/127.83 inference(scs_inference,[],[3443,3437,2243,2,19])). % 127.83/127.83 cnf(3468,plain, % 127.83/127.83 (~P2(f11(a8),f9(f11(a5),f9(x34681,x34681)))), % 127.83/127.83 inference(scs_inference,[],[2577,3446,2207,2,36])). % 127.83/127.83 cnf(3485,plain, % 127.83/127.83 (~E(f11(f9(a7,a7)),f10(a1,a1))), % 127.83/127.83 inference(scs_inference,[],[2774,2])). % 127.83/127.83 cnf(3487,plain, % 127.83/127.83 (E(f9(f9(x34871,x34871),x34872),f9(x34871,x34872))), % 127.83/127.83 inference(rename_variables,[],[2205])). % 127.83/127.83 cnf(3494,plain, % 127.83/127.83 (~E(f9(a8,a8),f10(f11(a8),f11(a8)))), % 127.83/127.83 inference(scs_inference,[],[2774,3428,3393,2715,3446,2552,2205,3487,105,2,35,46,18,19,3])). % 127.83/127.83 cnf(3502,plain, % 127.83/127.83 (~E(f11(a7),f10(a1,a1))), % 127.83/127.83 inference(scs_inference,[],[3485,2666,3468,2199,2247,2,19,3])). % 127.83/127.83 cnf(3508,plain, % 127.83/127.83 (~E(f10(a1,a1),f11(a7))), % 127.83/127.83 inference(scs_inference,[],[3502,2])). % 127.83/127.83 cnf(3511,plain, % 127.83/127.83 (~P2(f9(f11(a5),x35111),f11(a8))), % 127.83/127.83 inference(scs_inference,[],[3502,2185,3422,2243,105,2,3,29])). % 127.83/127.83 cnf(3521,plain, % 127.83/127.83 (E(f9(x35211,x35211),x35211)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3522,plain, % 127.83/127.83 (~P2(f9(f11(a5),x35221),f11(a8))), % 127.83/127.83 inference(rename_variables,[],[3511])). % 127.83/127.83 cnf(3524,plain, % 127.83/127.83 (~E(f11(a8),f11(f11(a5)))), % 127.83/127.83 inference(scs_inference,[],[3508,3511,3522,3494,2248,22,3521,2,3,31,28])). % 127.83/127.83 cnf(3621,plain, % 127.83/127.83 (~P2(x36211,f2(f9(x36212,x36212),f9(x36213,x36213)))+P2(x36211,f2(x36212,x36213))), % 127.83/127.83 inference(scs_inference,[],[3524,2289,2,19])). % 127.83/127.83 cnf(3654,plain, % 127.83/127.83 (~P2(f9(a5,a5),f10(f11(a8),f11(a8)))), % 127.83/127.83 inference(scs_inference,[],[2825,3426,2,46])). % 127.83/127.83 cnf(3666,plain, % 127.83/127.83 (~P2(x36661,f2(x36662,x36663))+P2(x36661,f2(f9(x36662,x36662),x36663))), % 127.83/127.83 inference(scs_inference,[],[3385,2246,3079,2236,2,3,19])). % 127.83/127.83 cnf(3680,plain, % 127.83/127.83 (~P2(a5,f10(f11(a8),f11(a8)))), % 127.83/127.83 inference(scs_inference,[],[2963,3413,2,46])). % 127.83/127.83 cnf(3685,plain, % 127.83/127.83 (E(f9(x36851,x36851),x36851)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3688,plain, % 127.83/127.83 (E(f9(x36881,x36881),x36881)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3690,plain, % 127.83/127.83 (~E(f10(f11(a8),f11(a8)),f11(a5))), % 127.83/127.83 inference(scs_inference,[],[3654,2969,22,3685,3688,2,31,30,28])). % 127.83/127.83 cnf(3704,plain, % 127.83/127.83 (~E(a5,a6)), % 127.83/127.83 inference(scs_inference,[],[26,2])). % 127.83/127.83 cnf(3705,plain, % 127.83/127.83 (~P2(a5,f10(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[26,2,46])). % 127.83/127.83 cnf(3708,plain, % 127.83/127.83 (E(x37081,f9(x37081,x37081))), % 127.83/127.83 inference(rename_variables,[],[105])). % 127.83/127.83 cnf(3710,plain, % 127.83/127.83 (~P2(a5,f10(a6,f9(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[26,2195,105,2,46,28,19])). % 127.83/127.83 cnf(3712,plain, % 127.83/127.83 (~E(f9(a8,f9(a8,a8)),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[26,2291,2195,105,2,46,28,19,29])). % 127.83/127.83 cnf(3715,plain, % 127.83/127.83 (E(x37151,f9(x37151,x37151))), % 127.83/127.83 inference(rename_variables,[],[105])). % 127.83/127.83 cnf(3717,plain, % 127.83/127.83 (~E(f9(a6,a6),a5)), % 127.83/127.83 inference(scs_inference,[],[26,2291,2195,105,3708,3715,2,46,28,19,29,30,3])). % 127.83/127.83 cnf(3719,plain, % 127.83/127.83 (~P2(f9(a5,a5),f10(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[26,2291,2195,105,3708,3715,22,2,46,28,19,29,30,3,18])). % 127.83/127.83 cnf(3721,plain, % 127.83/127.83 (~E(f9(a8,f9(a8,a8)),f10(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[26,2291,2195,105,3708,3715,22,2,46,28,19,29,30,3,18,33])). % 127.83/127.83 cnf(3726,plain, % 127.83/127.83 (~E(a5,f9(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3717,2])). % 127.83/127.83 cnf(3727,plain, % 127.83/127.83 (~E(f10(a6,a6),f10(a5,x37271))), % 127.83/127.83 inference(scs_inference,[],[3719,3717,22,2,31])). % 127.83/127.83 cnf(3728,plain, % 127.83/127.83 (E(f9(x37281,x37281),x37281)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3730,plain, % 127.83/127.83 (~P2(f9(f9(a5,a5),a5),f10(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3719,3717,2205,22,2,31,18])). % 127.83/127.83 cnf(3732,plain, % 127.83/127.83 (~E(f10(a6,a6),f11(a5))), % 127.83/127.83 inference(scs_inference,[],[3719,3717,2205,22,3728,2,31,18,28])). % 127.83/127.83 cnf(3733,plain, % 127.83/127.83 (E(f9(x37331,x37331),x37331)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3735,plain, % 127.83/127.83 (~P2(f9(a5,a5),f10(f9(a6,a6),a6))), % 127.83/127.83 inference(scs_inference,[],[3719,3717,2204,2205,22,3728,2,31,18,28,19])). % 127.83/127.83 cnf(3737,plain, % 127.83/127.83 (~E(f9(f9(a8,a8),a8),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[3704,3719,3717,2269,2204,2205,22,3728,2,31,18,28,19,29])). % 127.83/127.83 cnf(3739,plain, % 127.83/127.83 (~E(f10(a6,a6),f10(x37391,a5))), % 127.83/127.83 inference(scs_inference,[],[3704,3719,3717,2269,2204,2205,22,3728,3733,2,31,18,28,19,29,30])). % 127.83/127.83 cnf(3744,plain, % 127.83/127.83 (~E(f9(a5,a5),a6)), % 127.83/127.83 inference(scs_inference,[],[3704,3719,3717,2269,114,2204,2205,105,22,3728,3733,2,31,18,28,19,29,30,35,3])). % 127.83/127.83 cnf(3746,plain, % 127.83/127.83 (~E(f10(a6,a6),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[3704,3719,3717,2269,114,2204,2205,105,22,3728,3733,2,31,18,28,19,29,30,35,3,37])). % 127.83/127.83 cnf(3748,plain, % 127.83/127.83 (~E(f9(f9(a8,a8),a8),f10(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3704,3719,3717,2269,114,2204,2205,105,22,3728,3733,2,31,18,28,19,29,30,35,3,37,33])). % 127.83/127.83 cnf(3752,plain, % 127.83/127.83 (~E(f9(a8,a8),f10(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3746,2])). % 127.83/127.83 cnf(3753,plain, % 127.83/127.83 (~P2(f9(a5,a5),f10(a6,f9(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[3746,3710,22,2,18])). % 127.83/127.83 cnf(3754,plain, % 127.83/127.83 (E(f9(x37541,x37541),x37541)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3757,plain, % 127.83/127.83 (~E(f10(f9(a6,a6),a6),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[3746,3710,89,3704,2248,22,2,18,29,3])). % 127.83/127.83 cnf(3758,plain, % 127.83/127.83 (E(f10(x37581,x37582),f10(f9(x37581,x37581),x37582))), % 127.83/127.83 inference(rename_variables,[],[2248])). % 127.83/127.83 cnf(3759,plain, % 127.83/127.83 (~P2(f10(a6,a6),f10(a8,f9(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[3746,3710,89,3704,2248,3758,22,2,18,29,3,33])). % 127.83/127.83 cnf(3763,plain, % 127.83/127.83 (E(f9(x37631,x37631),x37631)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3766,plain, % 127.83/127.83 (E(f9(x37661,x37661),x37661)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3768,plain, % 127.83/127.83 (~E(f10(f9(a6,a6),a6),f10(x37681,a5))), % 127.83/127.83 inference(scs_inference,[],[3746,3735,3710,89,3704,2248,3758,22,3754,3763,3766,2,18,29,3,33,31,28,30])). % 127.83/127.83 cnf(3773,plain, % 127.83/127.83 (~E(f10(a5,x37731),f10(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3727,2])). % 127.83/127.83 cnf(3774,plain, % 127.83/127.83 (~P2(f9(f9(a5,a5),f9(a5,a5)),f10(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3727,3730,2207,2,18])). % 127.83/127.83 cnf(3776,plain, % 127.83/127.83 (~P2(f9(a5,a5),f10(f9(a6,a6),f9(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[3727,3730,3735,2195,2207,2,18,19])). % 127.83/127.83 cnf(3778,plain, % 127.83/127.83 (~E(f9(a8,a8),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[3727,3744,3730,189,3735,2195,2207,2,18,19,29])). % 127.83/127.83 cnf(3780,plain, % 127.83/127.83 (~E(f9(a5,a5),f9(a6,a6))), % 127.83/127.83 inference(scs_inference,[],[3727,3726,3744,3730,189,3735,2195,2207,105,2,18,19,29,3])). % 127.83/127.83 cnf(3786,plain, % 127.83/127.83 (~E(f9(a6,a6),f9(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[3780,2])). % 127.83/127.83 cnf(3791,plain, % 127.83/127.83 (~P2(f9(a8,a8),f10(f10(a6,a6),f10(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[3752,3780,3732,3774,2236,2242,2,18,3,46])). % 127.83/127.83 cnf(3802,plain, % 127.83/127.83 (~P2(f10(a6,a6),f10(f9(a8,a8),f9(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[3739,3759,2204,2,19])). % 127.83/127.83 cnf(3806,plain, % 127.83/127.83 (~E(f9(a6,f9(a6,a6)),f9(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[3786,3739,3759,1256,2204,2247,2,19,29,3])). % 127.83/127.83 cnf(3808,plain, % 127.83/127.83 (~E(f10(a6,f9(a6,a6)),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[3786,3739,3753,3759,114,1256,2204,2247,2,19,29,3,37])). % 127.83/127.83 cnf(3810,plain, % 127.83/127.83 (~E(f9(a8,a8),f9(f10(a6,a6),x38101))), % 127.83/127.83 inference(scs_inference,[],[3786,3739,3753,3759,3774,207,114,1256,2204,2247,2,19,29,3,37,36])). % 127.83/127.83 cnf(3829,plain, % 127.83/127.83 (~E(f11(a6),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[3778,2])). % 127.83/127.83 cnf(3833,plain, % 127.83/127.83 (E(f10(x38331,x38332),f10(x38332,x38331))), % 127.83/127.83 inference(rename_variables,[],[23])). % 127.83/127.83 cnf(3837,plain, % 127.83/127.83 (~E(f10(f9(a6,a6),f9(a6,a6)),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[3773,3778,3776,114,23,2248,2,46,18,3,37])). % 127.83/127.83 cnf(3839,plain, % 127.83/127.83 (~P2(f9(a8,a8),f10(f11(a6),f11(a6)))), % 127.83/127.83 inference(scs_inference,[],[3773,3778,3776,114,23,3833,2248,2,46,18,3,37,33])). % 127.83/127.83 cnf(3842,plain, % 127.83/127.83 (~E(f10(f9(a6,a6),f9(a6,a6)),f10(a5,x38421))), % 127.83/127.83 inference(scs_inference,[],[3773,3778,3776,114,23,3833,2248,22,2,46,18,3,37,33,31])). % 127.83/127.83 cnf(3857,plain, % 127.83/127.83 (~E(f9(a8,f10(a6,a5)),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[3829,3721,3791,1439,105,2,18,3])). % 127.83/127.83 cnf(3859,plain, % 127.83/127.83 (~P2(f10(a6,a6),f10(f9(a8,a8),a8))), % 127.83/127.83 inference(scs_inference,[],[3748,3802,2236,2,19])). % 127.83/127.83 cnf(3865,plain, % 127.83/127.83 (~E(f9(a8,a8),f10(f9(a6,a6),a6))), % 127.83/127.83 inference(scs_inference,[],[3757,2])). % 127.83/127.83 cnf(3866,plain, % 127.83/127.83 (~E(f9(f9(a6,a6),f9(a6,a6)),f9(a5,a5))), % 127.83/127.83 inference(scs_inference,[],[3757,3806,2242,2,3])). % 127.83/127.83 cnf(3870,plain, % 127.83/127.83 (~E(f9(a8,a8),f9(x38701,f10(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[3757,3806,3774,207,174,2242,2,3,29,35])). % 127.83/127.83 cnf(3874,plain, % 127.83/127.83 (E(f9(f9(a6,a6),f9(a6,a6)),a6)), % 127.83/127.83 inference(scs_inference,[],[3866,2368])). % 127.83/127.83 cnf(3877,plain, % 127.83/127.83 (~E(f11(a5),f10(a6,x38771))), % 127.83/127.83 inference(scs_inference,[],[3808,3874,2728,2,31])). % 127.83/127.83 cnf(3879,plain, % 127.83/127.83 (~E(f11(a5),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[3808,3874,2728,2,31,28])). % 127.83/127.83 cnf(3881,plain, % 127.83/127.83 (~E(f11(a5),f10(x38811,a6))), % 127.83/127.83 inference(scs_inference,[],[3808,3874,2728,2,31,28,30])). % 127.83/127.83 cnf(3900,plain, % 127.83/127.83 (~E(f10(f11(a6),f11(a6)),f10(a8,x39001))), % 127.83/127.83 inference(scs_inference,[],[3877,3839,2243,22,2,3,31])). % 127.83/127.83 cnf(3901,plain, % 127.83/127.83 (E(f9(x39011,x39011),x39011)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3905,plain, % 127.83/127.83 (~E(f10(a5,a5),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[3877,3839,3874,2611,2243,22,2,3,31,46,28])). % 127.83/127.83 cnf(3907,plain, % 127.83/127.83 (~E(f10(f11(a6),f11(a6)),f10(x39071,a8))), % 127.83/127.83 inference(scs_inference,[],[3877,3839,3874,2611,2243,22,3901,2,3,31,46,28,30])). % 127.83/127.83 cnf(3910,plain, % 127.83/127.83 (~E(f10(x39101,a6),f11(a5))), % 127.83/127.83 inference(scs_inference,[],[3881,2])). % 127.83/127.83 cnf(3911,plain, % 127.83/127.83 (~E(f11(f9(a5,a5)),f10(x39111,a6))), % 127.83/127.83 inference(scs_inference,[],[3881,2243,2,3])). % 127.83/127.83 cnf(3924,plain, % 127.83/127.83 (~E(f11(f9(a5,a5)),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[3879,3837,2243,2,3])). % 127.83/127.83 cnf(3926,plain, % 127.83/127.83 (~E(f9(a8,a8),f9(a8,f10(a6,a5)))), % 127.83/127.83 inference(scs_inference,[],[3857,2])). % 127.83/127.83 cnf(3950,plain, % 127.83/127.83 (~E(f10(x39501,f9(a6,a6)),f11(a5))), % 127.83/127.83 inference(scs_inference,[],[3910,3737,2236,2,3])). % 127.83/127.83 cnf(3955,plain, % 127.83/127.83 (~P2(x39551,f2(x39552,f9(x39553,x39553)))+P2(x39551,f2(x39552,x39553))), % 127.83/127.83 inference(scs_inference,[],[3712,3780,2203,2247,2,3,19])). % 127.83/127.83 cnf(3985,plain, % 127.83/127.83 (~E(f9(a6,f9(a6,a6)),a5)), % 127.83/127.83 inference(scs_inference,[],[3768,3717,2247,2,3])). % 127.83/127.83 cnf(3989,plain, % 127.83/127.83 (~E(f10(a5,x39891),f10(f9(a6,a6),f9(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[3842,2])). % 127.83/127.83 cnf(3990,plain, % 127.83/127.83 (~E(f4(f9(a8,a8),f11(a5),a8),f10(a8,x39901))), % 127.83/127.83 inference(scs_inference,[],[22,3842,2305,2,31])). % 127.83/127.83 cnf(3991,plain, % 127.83/127.83 (E(f9(x39911,x39911),x39911)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3993,plain, % 127.83/127.83 (~E(f4(a8,f11(a5),a8),f10(a8,x39931))), % 127.83/127.83 inference(scs_inference,[],[22,3842,2305,2198,2,31,3])). % 127.83/127.83 cnf(3995,plain, % 127.83/127.83 (~P2(a5,f9(f10(a6,a6),f10(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[22,3991,3842,2305,2198,3705,2,31,3,19])). % 127.83/127.83 cnf(3996,plain, % 127.83/127.83 (E(f9(x39961,x39961),x39961)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(3998,plain, % 127.83/127.83 (E(f9(x39981,x39981),x39981)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4005,plain, % 127.83/127.83 (E(f9(x40051,x40051),x40051)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4006,plain, % 127.83/127.83 (~E(f4(f9(a8,a8),f11(a5),a8),f11(a8))), % 127.83/127.83 inference(scs_inference,[],[22,3991,3996,3998,4005,3842,2305,2198,3705,2294,2913,2,31,3,19,30,33,2906,18,28])). % 127.83/127.83 cnf(4012,plain, % 127.83/127.83 (~E(f4(f9(a8,a8),f11(a5),f9(a8,a8)),f10(a8,x40121))), % 127.83/127.83 inference(scs_inference,[],[3900,3993,2643,2,3])). % 127.83/127.83 cnf(4014,plain, % 127.83/127.83 (~P2(f10(a6,a6),f10(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[3900,3993,2643,3859,2248,2,3,19])). % 127.83/127.83 cnf(4021,plain, % 127.83/127.83 (~E(f10(x40211,a8),f10(f11(a6),f11(a6)))), % 127.83/127.83 inference(scs_inference,[],[3907,2])). % 127.83/127.83 cnf(4022,plain, % 127.83/127.83 (~E(f10(a8,a8),f10(f10(a6,a6),x40221))), % 127.83/127.83 inference(scs_inference,[],[4014,3907,23,2,31])). % 127.83/127.83 cnf(4023,plain, % 127.83/127.83 (E(f10(x40231,x40232),f10(x40232,x40231))), % 127.83/127.83 inference(rename_variables,[],[23])). % 127.83/127.83 cnf(4027,plain, % 127.83/127.83 (~E(f10(a8,a8),f11(f10(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[22,4014,3907,23,4023,2,31,18,28])). % 127.83/127.83 cnf(4038,plain, % 127.83/127.83 (~E(f11(f10(a5,a5)),f10(a8,x40381))), % 127.83/127.83 inference(scs_inference,[],[22,3990,2326,2,31])). % 127.83/127.83 cnf(4039,plain, % 127.83/127.83 (E(f9(x40391,x40391),x40391)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4041,plain, % 127.83/127.83 (~P2(f9(a5,a5),f9(f10(a6,a6),f10(a6,a6)))), % 127.83/127.83 inference(scs_inference,[],[22,4039,3990,3995,2326,2,31,18])). % 127.83/127.83 cnf(4042,plain, % 127.83/127.83 (E(f9(x40421,x40421),x40421)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4043,plain, % 127.83/127.83 (~E(f11(f10(a5,a5)),f11(a8))), % 127.83/127.83 inference(scs_inference,[],[22,4039,4042,3990,3995,2326,2,31,18,28])). % 127.83/127.83 cnf(4044,plain, % 127.83/127.83 (E(f9(x40441,x40441),x40441)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4046,plain, % 127.83/127.83 (~E(f11(f10(a5,a5)),f10(x40461,a8))), % 127.83/127.83 inference(scs_inference,[],[22,4039,4042,4044,3990,3995,2326,2,31,18,28,30])). % 127.83/127.83 cnf(4051,plain, % 127.83/127.83 (E(f9(x40511,x40511),x40511)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4053,plain, % 127.83/127.83 (~E(f4(a8,f11(a5),f9(a8,a8)),f10(a8,x40531))), % 127.83/127.83 inference(scs_inference,[],[22,4012,4041,2198,2,31,3])). % 127.83/127.83 cnf(4056,plain, % 127.83/127.83 (E(f9(x40561,x40561),x40561)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4058,plain, % 127.83/127.83 (~E(f9(f10(a6,a6),f10(a6,a6)),f10(x40581,a5))), % 127.83/127.83 inference(scs_inference,[],[22,4051,4056,4012,4041,2198,2,31,3,28,30])). % 127.83/127.83 cnf(4064,plain, % 127.83/127.83 (~E(f10(f11(a5),f11(a5)),f10(a8,x40641))), % 127.83/127.83 inference(scs_inference,[],[22,4038,1035,2,31])). % 127.83/127.83 cnf(4065,plain, % 127.83/127.83 (E(f9(x40651,x40651),x40651)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4068,plain, % 127.83/127.83 (E(f9(x40681,x40681),x40681)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4069,plain, % 127.83/127.83 (~E(f4(f11(a5),f9(a8,a8),a8),f11(a8))), % 127.83/127.83 inference(scs_inference,[],[22,4065,4068,4038,3865,2320,1035,2,31,3,28])). % 127.83/127.83 cnf(4070,plain, % 127.83/127.83 (E(f9(x40701,x40701),x40701)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4072,plain, % 127.83/127.83 (~E(f4(f11(a5),f9(a8,a8),a8),f10(x40721,a8))), % 127.83/127.83 inference(scs_inference,[],[22,4065,4068,4070,4038,3865,2320,1035,2,31,3,28,30])). % 127.83/127.83 cnf(4078,plain, % 127.83/127.83 (~E(f4(a8,f11(a5),a8),f11(a8))), % 127.83/127.83 inference(scs_inference,[],[4046,4006,2198,2,3])). % 127.83/127.83 cnf(4086,plain, % 127.83/127.83 (~E(f4(f11(a5),a8,a8),f10(x40861,a8))), % 127.83/127.83 inference(scs_inference,[],[4053,4072,2200,2,3])). % 127.83/127.83 cnf(4088,plain, % 127.83/127.83 (~E(f9(f11(a1),x40881),f10(a7,x40882))), % 127.83/127.83 inference(scs_inference,[],[22,4053,4072,2559,2200,2,3,31])). % 127.83/127.83 cnf(4089,plain, % 127.83/127.83 (E(f9(x40891,x40891),x40891)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4091,plain, % 127.83/127.83 (~E(f9(f11(a1),x40911),f11(a7))), % 127.83/127.83 inference(scs_inference,[],[22,4089,4053,4072,2559,2200,2,3,31,28])). % 127.83/127.83 cnf(4098,plain, % 127.83/127.83 (~E(f4(f11(a5),f9(a8,a8),f9(a8,a8)),f10(x40981,a8))), % 127.83/127.83 inference(scs_inference,[],[4058,4086,2515,2,3])). % 127.83/127.83 cnf(4103,plain, % 127.83/127.83 (~E(f4(f11(a5),a8,f9(a8,a8)),f10(x41031,a8))), % 127.83/127.83 inference(scs_inference,[],[4064,4098,2200,2,3])). % 127.83/127.83 cnf(4114,plain, % 127.83/127.83 (~P2(f4(f11(a5),a8,f9(a8,a8)),f11(a5))), % 127.83/127.83 inference(scs_inference,[],[23,4103,3950,2197,4014,1923,2207,2,36,3,18])). % 127.83/127.83 cnf(4122,plain, % 127.83/127.83 (~P2(f4(f11(a5),f9(a8,a8),f9(a8,a8)),f11(a5))), % 127.83/127.83 inference(scs_inference,[],[3924,4078,4114,2643,2200,2,3,18])). % 127.83/127.83 cnf(4127,plain, % 127.83/127.83 (P2(f4(f11(a5),a8,f9(a8,a8)),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[23,3924,4078,4114,2216,2643,3881,2200,2,3,18,33,41])). % 127.83/127.83 cnf(4130,plain, % 127.83/127.83 (~P2(f10(a6,a6),f9(f9(x41301,x41301),f10(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[23,3924,4078,4114,2216,2643,3881,4014,2200,2205,2,3,18,33,41,35])). % 127.83/127.83 cnf(4142,plain, % 127.83/127.83 (~P2(f4(f11(a5),f9(a8,a8),a8),f11(a5))), % 127.83/127.83 inference(scs_inference,[],[23,4122,4088,4130,3989,2240,2242,2,3,19,18])). % 127.83/127.83 cnf(4148,plain, % 127.83/127.83 (P2(f4(f11(a5),f9(a8,a8),a8),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[23,4122,4088,4130,3989,2240,2242,2,3,19,18,1066,32,49])). % 127.83/127.83 cnf(4160,plain, % 127.83/127.83 (~E(f4(f11(a5),a8,a8),f11(a8))), % 127.83/127.83 inference(scs_inference,[],[3911,4069,2200,2,3])). % 127.83/127.83 cnf(4162,plain, % 127.83/127.83 (P2(f4(f11(a5),f9(a8,a8),f9(a8,a8)),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[3911,4069,2216,4122,2200,2,3,41])). % 127.83/127.83 cnf(4185,plain, % 127.83/127.83 (E(f9(x41851,x41851),x41851)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4188,plain, % 127.83/127.83 (E(f9(x41881,x41881),x41881)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4193,plain, % 127.83/127.83 (~E(f9(x41931,f11(a5)),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[24,3332,4091,244,22,4185,4188,2,31,28,30,3])). % 127.83/127.83 cnf(4205,plain, % 127.83/127.83 (~P2(f10(a6,f9(a6,a6)),f10(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[24,4193,3985,4014,2195,2,3,18])). % 127.83/127.83 cnf(4208,plain, % 127.83/127.83 (~P2(f10(f9(a6,a6),f9(a6,a6)),f10(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[4205,3810,2204,2,18])). % 127.83/127.83 cnf(4220,plain, % 127.83/127.83 (E(f9(x42201,f10(x42202,f9(x42203,x42204))),f9(x42201,f10(x42202,f9(x42204,x42203))))), % 127.83/127.83 inference(scs_inference,[],[2152,4078,2476,7,8,4,12,9,10,13,14,5])). % 127.83/127.83 cnf(4221,plain, % 127.83/127.83 (E(f10(f10(x42211,f9(x42212,x42213)),x42214),f10(f10(x42211,f9(x42213,x42212)),x42214))), % 127.83/127.83 inference(scs_inference,[],[2152,4078,2476,7,8,4,12,9,10,13,14,5,6])). % 127.83/127.83 cnf(4222,plain, % 127.83/127.83 (E(f11(f10(x42221,f9(x42222,x42223))),f11(f10(x42221,f9(x42223,x42222))))), % 127.83/127.83 inference(scs_inference,[],[2152,4078,2476,7,8,4,12,9,10,13,14,5,6,16])). % 127.83/127.83 cnf(4231,plain, % 127.83/127.83 (E(f10(x42311,f9(x42312,x42313)),f10(x42311,f9(x42313,x42312)))), % 127.83/127.83 inference(rename_variables,[],[2152])). % 127.83/127.83 cnf(4233,plain, % 127.83/127.83 (~P2(f10(f9(a6,a6),f9(a6,a6)),f9(x42331,f10(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[24,4208,3870,2152,1503,1435,4078,2195,2476,7,8,4,12,9,10,13,14,5,6,16,15,2,11,35,19,31,36])). % 127.83/127.83 cnf(4245,plain, % 127.83/127.83 (P2(f4(f11(a5),f9(a8,a8),f9(a8,a8)),f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[24,3322,4162,4208,492,3870,2152,4231,364,1503,1435,3857,4078,3359,1433,2195,2476,7,8,4,12,9,10,13,14,5,6,16,15,2,11,35,19,31,36,46,3,28,18,29,49])). % 127.83/127.83 cnf(4266,plain, % 127.83/127.83 (E(f9(f2(f9(x42661,x42662),x42663),x42664),f9(f2(f9(x42662,x42661),x42663),x42664))), % 127.83/127.83 inference(scs_inference,[],[2153,7,8,4])). % 127.83/127.83 cnf(4272,plain, % 127.83/127.83 (E(f9(x42721,f2(f9(x42722,x42723),x42724)),f9(x42721,f2(f9(x42723,x42722),x42724)))), % 127.83/127.83 inference(scs_inference,[],[2153,7,8,4,12,9,13,10,14,5])). % 127.83/127.83 cnf(4273,plain, % 127.83/127.83 (E(f10(f2(f9(x42731,x42732),x42733),x42734),f10(f2(f9(x42732,x42731),x42733),x42734))), % 127.83/127.83 inference(scs_inference,[],[2153,7,8,4,12,9,13,10,14,5,6])). % 127.83/127.83 cnf(4274,plain, % 127.83/127.83 (E(f11(f2(f9(x42741,x42742),x42743)),f11(f2(f9(x42742,x42741),x42743)))), % 127.83/127.83 inference(scs_inference,[],[2153,7,8,4,12,9,13,10,14,5,6,16])). % 127.83/127.83 cnf(4275,plain, % 127.83/127.83 (~E(f10(f10(a6,a6),x42751),f10(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[4022,2153,7,8,4,12,9,13,10,14,5,6,16,2])). % 127.83/127.83 cnf(4281,plain, % 127.83/127.83 (E(f9(x42811,x42812),f9(x42812,x42811))), % 127.83/127.83 inference(rename_variables,[],[24])). % 127.83/127.83 cnf(4283,plain, % 127.83/127.83 (E(f9(x42831,x42832),f9(x42832,x42831))), % 127.83/127.83 inference(rename_variables,[],[24])). % 127.83/127.83 cnf(4297,plain, % 127.83/127.83 (P2(f4(f11(a5),a8,f9(a8,a8)),f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[24,4281,4283,3421,4127,3690,1658,4022,1059,2153,4233,4245,4122,2608,302,2199,2248,7,8,4,12,9,13,10,14,5,6,16,2,15,11,35,19,31,36,3,28,18,29,49])). % 127.83/127.83 cnf(4311,plain, % 127.83/127.83 (E(f10(x43111,f2(x43112,f9(x43113,x43114))),f10(x43111,f2(x43112,f9(x43114,x43113))))), % 127.83/127.83 inference(scs_inference,[],[2154,7])). % 127.83/127.83 cnf(4320,plain, % 127.83/127.83 (E(f10(f2(x43201,f9(x43202,x43203)),x43204),f10(f2(x43201,f9(x43203,x43202)),x43204))), % 127.83/127.83 inference(scs_inference,[],[2154,7,8,4,12,13,9,10,14,5,6])). % 127.83/127.83 cnf(4322,plain, % 127.83/127.83 (E(f11(f2(x43221,f9(x43222,x43223))),f11(f2(x43221,f9(x43223,x43222))))), % 127.83/127.83 inference(scs_inference,[],[2154,7,8,4,12,13,9,10,14,5,6,15,16])). % 127.83/127.83 cnf(4334,plain, % 127.83/127.83 (E(f4(x43341,f9(x43342,x43343),x43344),f4(x43341,f9(x43343,x43342),x43344))), % 127.83/127.83 inference(rename_variables,[],[2156])). % 127.83/127.83 cnf(4336,plain, % 127.83/127.83 (~E(f11(a5),f11(f4(f11(a5),f9(a8,a8),a8)))), % 127.83/127.83 inference(scs_inference,[],[4142,4027,3680,2154,2156,4334,4297,4114,2291,2199,7,8,4,12,13,9,10,14,5,6,15,16,2,11,32,35,19,36,31,28])). % 127.83/127.83 cnf(4346,plain, % 127.83/127.83 (P2(f4(f11(a5),f9(a8,a8),a8),f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[24,4148,4142,4027,3680,1074,2154,2156,4334,2159,4297,915,4103,4114,2291,2199,7,8,4,12,13,9,10,14,5,6,15,16,2,11,32,35,19,36,31,28,3,18,29,49])). % 127.83/127.83 cnf(4370,plain, % 127.83/127.83 (~P2(a5,f11(a6))), % 127.83/127.83 inference(scs_inference,[],[2728,3704,3857,3874,3900,4043,3810,4346,4021,32,48,16,2,6,5,4,7,45])). % 127.83/127.83 cnf(4375,plain, % 127.83/127.83 (E(f9(x43751,x43751),x43751)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4376,plain, % 127.83/127.83 (E(f9(f9(x43761,x43762),f9(x43761,x43762)),f9(x43761,f9(x43762,x43762)))), % 127.83/127.83 inference(scs_inference,[],[22,4375,2247,1256,2728,3704,3857,3874,3900,4043,3810,4346,4021,32,48,16,2,6,5,4,7,45,47,18,3])). % 127.83/127.83 cnf(4381,plain, % 127.83/127.83 (E(f9(x43811,x43812),f9(x43811,f9(x43812,x43812)))), % 127.83/127.83 inference(rename_variables,[],[2247])). % 127.83/127.83 cnf(4382,plain, % 127.83/127.83 (P2(f9(f9(a5,a5),f9(a5,a5)),f9(f9(a8,a8),a8))), % 127.83/127.83 inference(scs_inference,[],[22,4375,2247,4381,1256,2728,207,3704,3857,3874,137,3900,4043,3810,4346,4021,32,48,16,2,6,5,4,7,45,47,18,3,46,17,37])). % 127.83/127.83 cnf(4395,plain, % 127.83/127.83 (~P2(a5,f10(a6,a5))), % 127.83/127.83 inference(scs_inference,[],[4370,230])). % 127.83/127.83 cnf(4419,plain, % 127.83/127.83 (E(f9(f9(f10(a6,a5),a8),f9(f10(a6,a5),a8)),f11(a6))), % 127.83/127.83 inference(scs_inference,[],[1233,22,25,2199,103,174,2515,3993,4382,4395,4275,3926,4336,32,16,2,6,5,45,47,1047,2476,48,18,29,3])). % 127.83/127.83 cnf(4420,plain, % 127.83/127.83 (E(f9(x44201,x44201),x44201)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4421,plain, % 127.83/127.83 (P2(f9(f9(f10(a6,a5),a8),f9(f10(a6,a5),a8)),f11(f11(a6)))), % 127.83/127.83 inference(scs_inference,[],[1233,22,4420,25,2199,103,174,2515,364,3993,4382,4395,4275,3926,4336,32,16,2,6,5,45,47,1047,2476,48,18,29,3,28])). % 127.83/127.83 cnf(4468,plain, % 127.83/127.83 (P2(f9(f10(a6,a5),a8),f10(f11(a6),x44681))), % 127.83/127.83 inference(rename_variables,[],[65])). % 127.83/127.83 cnf(4469,plain, % 127.83/127.83 (~P2(a5,f9(f9(f10(a6,a5),a8),f9(f10(a6,a5),a8)))), % 127.83/127.83 inference(scs_inference,[],[318,3719,65,3704,2608,3839,4421,4419,32,2,45,47,48,49,18,29])). % 127.83/127.83 cnf(4472,plain, % 127.83/127.83 (E(f9(x44721,x44721),x44721)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4473,plain, % 127.83/127.83 (P2(f9(f10(x44731,f9(x44732,x44733)),f10(x44731,f9(x44732,x44733))),f11(f10(x44731,f9(x44733,x44732))))), % 127.83/127.83 inference(scs_inference,[],[318,22,4472,2242,3719,65,3704,2608,3839,4421,4419,4222,32,2,45,47,48,49,18,29,3,28])). % 127.83/127.83 cnf(4474,plain, % 127.83/127.83 (E(f9(x44741,x44741),x44741)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4479,plain, % 127.83/127.83 (E(f9(x44791,x44791),x44791)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4488,plain, % 127.83/127.83 (P2(f9(f10(a6,a5),a8),f9(f10(f11(a6),f9(x44881,x44882)),f10(f11(a6),f9(x44882,x44881))))), % 127.83/127.83 inference(scs_inference,[],[318,22,4472,4474,4479,2242,2205,103,3719,65,4468,3704,116,2608,4395,3839,4220,4421,4419,4222,4273,4311,32,2,45,47,48,49,18,29,3,28,46,31,36,19,30,37])). % 127.83/127.83 cnf(4503,plain, % 127.83/127.83 (E(f11(f9(f10(a6,a5),a8)),f11(f11(a6)))), % 127.83/127.83 inference(scs_inference,[],[364,2])). % 127.83/127.83 cnf(4506,plain, % 127.83/127.83 (~P2(f11(f10(x45061,f9(x45062,x45063))),f9(f10(x45061,f9(x45063,x45062)),f10(x45061,f9(x45063,x45062))))), % 127.83/127.83 inference(scs_inference,[],[2611,364,4473,2,48,32])). % 127.83/127.83 cnf(4514,plain, % 127.83/127.83 (P2(f9(f2(f9(x45141,x45142),x45143),f2(f9(x45141,x45142),x45143)),f11(f2(f9(x45142,x45141),x45143)))), % 127.83/127.83 inference(scs_inference,[],[1079,22,105,2611,2294,364,4473,4274,2,48,32,45,47,18,28])). % 127.83/127.83 cnf(4515,plain, % 127.83/127.83 (E(f9(x45151,x45151),x45151)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4523,plain, % 127.83/127.83 (E(f9(x45231,x45231),x45231)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4525,plain, % 127.83/127.83 (E(f9(f9(f9(x45251,x45251),x45252),f9(f9(x45251,x45251),x45252)),f9(x45251,x45252))), % 127.83/127.83 inference(scs_inference,[],[1079,22,4515,4523,105,2205,2611,2294,364,4473,4274,4320,4322,4469,2,48,32,45,47,18,28,29,49,31,3])). % 127.83/127.83 cnf(4552,plain, % 127.83/127.83 (~P2(f11(f2(f9(x45521,x45522),x45523)),f9(f2(f9(x45522,x45521),x45523),f2(f9(x45522,x45521),x45523)))), % 127.83/127.83 inference(scs_inference,[],[4142,2643,4514,2,47,48,32])). % 127.83/127.83 cnf(4556,plain, % 127.83/127.83 (P2(f9(f4(f11(a5),a8,f9(a8,a8)),f4(f11(a5),a8,f9(a8,a8))),f9(f9(a8,a8),f9(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[996,105,4297,4142,2643,4514,2,47,48,32,45,18])). % 127.83/127.83 cnf(4560,plain, % 127.83/127.83 (E(f9(x45601,x45601),x45601)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4562,plain, % 127.83/127.83 (E(f9(f10(x45621,x45622),f10(x45621,x45622)),f10(x45621,f9(x45622,x45622)))), % 127.83/127.83 inference(scs_inference,[],[996,22,4560,105,2236,4297,4142,4395,2643,2269,4322,4514,2,47,48,32,45,18,19,28,3])). % 127.83/127.83 cnf(4569,plain, % 127.83/127.83 (~P2(f11(f10(x45691,f9(x45692,x45693))),f10(x45691,f9(x45693,x45692)))), % 127.83/127.83 inference(scs_inference,[],[996,22,4560,105,2236,103,3905,4297,4142,4395,2643,2269,4322,4514,4503,4506,2163,2,47,48,32,45,18,19,28,3,29,36,49])). % 127.83/127.83 cnf(4574,plain, % 127.83/127.83 (E(f9(f9(f9(x45741,x45741),x45742),f9(f9(x45741,x45741),x45742)),f9(x45741,x45742))), % 127.83/127.83 inference(rename_variables,[],[4525])). % 127.83/127.83 cnf(4576,plain, % 127.83/127.83 (P2(a5,f9(f9(f9(a8,a8),a8),f9(f9(a8,a8),a8)))), % 127.83/127.83 inference(scs_inference,[],[21,996,22,4560,105,2236,103,3905,4297,4142,4395,2643,2269,4322,4514,4525,4574,4503,4506,2163,2,47,48,32,45,18,19,28,3,29,36,49,46,35,37])). % 127.83/127.83 cnf(4600,plain, % 127.83/127.83 (P2(f9(f4(f9(a8,a8),f11(a5),a8),f4(f9(a8,a8),f11(a5),a8)),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[282,105,4395,2298,4419,4556,2,47,45,48,32,18])). % 127.83/127.83 cnf(4604,plain, % 127.83/127.83 (E(f10(f2(x46041,f9(x46042,x46043)),x46044),f10(f2(x46041,f9(x46043,x46042)),x46044))), % 127.83/127.83 inference(rename_variables,[],[4320])). % 127.83/127.83 cnf(4605,plain, % 127.83/127.83 (~P2(f11(f10(x46051,f9(x46052,x46053))),f10(x46051,f9(x46053,x46052)))), % 127.83/127.83 inference(rename_variables,[],[4569])). % 127.83/127.83 cnf(4607,plain, % 127.83/127.83 (E(f9(f9(x46071,f9(x46072,x46072)),f9(x46071,f9(x46072,x46072))),f9(x46071,x46072))), % 127.83/127.83 inference(scs_inference,[],[282,22,105,2207,4395,2298,89,4419,4320,4556,4569,2,47,45,48,32,18,19,31,3])). % 127.83/127.83 cnf(4614,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46141,x46142),x46143)),f2(f9(x46142,x46141),x46143))), % 127.83/127.83 inference(scs_inference,[],[282,22,105,2207,4395,2298,81,89,4419,4320,4604,4556,4569,4605,4552,2,47,45,48,32,18,19,31,3,17,30,49])). % 127.83/127.83 cnf(4621,plain, % 127.83/127.83 (P2(f9(f9(a5,a5),f9(a5,a5)),f9(f9(f9(a8,a8),a8),f9(f9(a8,a8),a8)))), % 127.83/127.83 inference(scs_inference,[],[282,22,105,2207,207,4395,2298,81,89,4419,4320,4604,4556,4272,4569,4605,4552,4376,2,47,45,48,32,18,19,31,3,17,30,49,46,35,37])). % 127.83/127.83 cnf(4624,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46241,x46241),f9(x46242,x46242))),f2(x46241,x46242))), % 127.83/127.83 inference(scs_inference,[],[282,22,105,2207,207,4395,2298,81,89,4419,4320,4604,4556,4272,4569,4605,4552,4376,2,47,45,48,32,18,19,31,3,17,30,49,46,35,37,2889])). % 127.83/127.83 cnf(4626,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46261,x46261),f9(x46262,x46262))),f2(x46261,f9(x46262,x46262)))), % 127.83/127.83 inference(scs_inference,[],[282,22,105,2207,207,4395,2298,81,89,4419,4320,4604,4556,4272,4569,4605,4552,4376,2,47,45,48,32,18,19,31,3,17,30,49,46,35,37,2889,3955,3666])). % 127.83/127.83 cnf(4629,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46291,x46291),f9(x46292,x46292))),f2(f9(f9(x46291,x46291),f9(x46291,x46291)),f9(x46292,x46292)))), % 127.83/127.83 inference(scs_inference,[],[282,22,105,2207,207,4395,2298,81,89,4419,4320,4604,4556,4272,4569,4605,4552,4376,2,47,45,48,32,18,19,31,3,17,30,49,46,35,37,2889,3955,3666,3621,3397,3248])). % 127.83/127.83 cnf(4630,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x46301,x46302),f9(x46301,x46302)),f9(x46303,x46303))),f2(f9(x46302,x46301),x46303))), % 127.83/127.83 inference(scs_inference,[],[282,22,105,2207,207,4395,2298,81,89,4419,4320,4604,4556,4272,4569,4605,4552,4376,2,47,45,48,32,18,19,31,3,17,30,49,46,35,37,2889,3955,3666,3621,3397,3248,2191])). % 127.83/127.83 cnf(4640,plain, % 127.83/127.83 (E(f9(x46401,x46402),f9(f9(f9(x46401,x46401),x46402),f9(f9(x46401,x46401),x46402)))), % 127.83/127.83 inference(scs_inference,[],[4525,2])). % 127.83/127.83 cnf(4648,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46481,x46481),f9(f9(x46482,x46482),f9(x46482,x46482)))),f2(x46481,x46482))), % 127.83/127.83 inference(scs_inference,[],[1010,4114,4525,4624,4629,2,47,45,48,3621,3397])). % 127.83/127.83 cnf(4649,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46491,x46491),f9(x46492,x46492))),f2(x46491,x46492))), % 127.83/127.83 inference(rename_variables,[],[4624])). % 127.83/127.83 cnf(4652,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x46521,x46522),f9(x46521,x46522)),f9(x46523,x46523))),f2(f9(x46522,x46521),f9(x46523,x46523)))), % 127.83/127.83 inference(scs_inference,[],[1010,4114,4525,4600,4624,4629,4626,2,47,45,48,3621,3397,32,2191])). % 127.83/127.83 cnf(4653,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46531,x46531),f9(x46532,x46532))),f2(x46531,f9(x46532,x46532)))), % 127.83/127.83 inference(rename_variables,[],[4626])). % 127.83/127.83 cnf(4654,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46541,x46541),f9(x46542,x46542))),f2(f9(f9(f9(x46541,x46541),f9(x46541,x46541)),f9(f9(x46541,x46541),f9(x46541,x46541))),f9(x46542,x46542)))), % 127.83/127.83 inference(scs_inference,[],[1010,4114,4525,4600,4624,4629,4626,2,47,45,48,3621,3397,32,2191,3248])). % 127.83/127.83 cnf(4656,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x46561,x46561),f9(x46561,x46561)),f9(f9(x46562,x46562),f9(x46562,x46562)))),f2(x46561,x46562))), % 127.83/127.83 inference(scs_inference,[],[1010,4114,4525,4600,4624,4649,4629,4626,4653,2,47,45,48,3621,3397,32,2191,3248,3955,2889])). % 127.83/127.83 cnf(4657,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46571,x46571),f9(x46572,x46572))),f2(x46571,x46572))), % 127.83/127.83 inference(rename_variables,[],[4624])). % 127.83/127.83 cnf(4658,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x46581,x46581),f9(x46581,x46581)),f9(x46582,x46582))),f2(x46581,x46582))), % 127.83/127.83 inference(scs_inference,[],[1010,4114,4525,4600,4624,4649,4657,4629,4626,4653,2,47,45,48,3621,3397,32,2191,3248,3955,2889,3666])). % 127.83/127.83 cnf(4659,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46591,x46591),f9(x46592,x46592))),f2(x46591,x46592))), % 127.83/127.83 inference(rename_variables,[],[4624])). % 127.83/127.83 cnf(4662,plain, % 127.83/127.83 (P2(f9(f4(f11(a5),a8,f9(a8,a8)),f4(f11(a5),a8,f9(a8,a8))),f9(a8,a8))), % 127.83/127.83 inference(scs_inference,[],[1010,22,4114,1231,3839,4556,4525,4600,4624,4649,4657,4629,4626,4653,2,47,45,48,3621,3397,32,2191,3248,3955,2889,3666,18,19])). % 127.83/127.83 cnf(4663,plain, % 127.83/127.83 (E(f9(x46631,x46631),x46631)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4664,plain, % 127.83/127.83 (E(f9(f10(x46641,x46642),f10(x46641,x46642)),f10(f9(x46641,x46641),x46642))), % 127.83/127.83 inference(scs_inference,[],[1010,22,4663,2248,4114,1231,3839,4556,4525,4600,4624,4649,4657,4629,4626,4653,2,47,45,48,3621,3397,32,2191,3248,3955,2889,3666,18,19,3])). % 127.83/127.83 cnf(4668,plain, % 127.83/127.83 (E(f10(f10(x46681,f9(x46682,x46683)),x46684),f10(f10(x46681,f9(x46683,x46682)),x46684))), % 127.83/127.83 inference(rename_variables,[],[4221])). % 127.83/127.83 cnf(4669,plain, % 127.83/127.83 (~P2(f11(f10(x46691,f9(x46692,x46693))),f10(x46691,f9(x46693,x46692)))), % 127.83/127.83 inference(rename_variables,[],[4569])). % 127.83/127.83 cnf(4677,plain, % 127.83/127.83 (~P2(f11(f2(f9(x46771,x46771),f9(x46772,x46772))),f2(x46771,x46772))), % 127.83/127.83 inference(rename_variables,[],[4624])). % 127.83/127.83 cnf(4685,plain, % 127.83/127.83 (P2(a5,f9(f9(a8,f9(a8,a8)),f9(a8,f9(a8,a8))))), % 127.83/127.83 inference(scs_inference,[],[21,1010,22,4663,2248,137,4114,1231,3839,4556,4525,4272,4569,4669,4266,4600,4607,4221,4668,4624,4649,4657,4659,4677,4629,4626,4653,2,47,45,48,3621,3397,32,2191,3248,3955,2889,3666,18,19,3,17,30,31,36,46,35,37])). % 127.83/127.83 cnf(4700,plain, % 127.83/127.83 (~P2(f11(f2(f9(x47001,x47001),f9(f9(x47002,x47002),f9(x47002,x47002)))),f2(f9(x47001,x47001),x47002))), % 127.83/127.83 inference(scs_inference,[],[3413,3839,4607,4648,2,47,48,45,3248])). % 127.83/127.83 cnf(4701,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(f9(x47011,x47012),f9(x47011,x47012)),f9(f9(x47011,x47012),f9(x47011,x47012))),f9(f9(x47013,x47013),f9(x47013,x47013)))),f2(f9(x47012,x47011),x47013))), % 127.83/127.83 inference(scs_inference,[],[3413,3839,4607,4656,4648,2,47,48,45,3248,2191])). % 127.83/127.83 cnf(4702,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x47021,x47021),f9(x47021,x47021)),f9(f9(x47022,x47022),f9(x47022,x47022)))),f2(x47021,x47022))), % 127.83/127.83 inference(rename_variables,[],[4656])). % 127.83/127.83 cnf(4703,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x47031,x47031),f9(x47031,x47031)),f9(x47032,x47032))),f2(x47031,f9(x47032,x47032)))), % 127.83/127.83 inference(scs_inference,[],[3413,3839,4607,4656,4648,4658,2,47,48,45,3248,2191,3955])). % 127.83/127.83 cnf(4714,plain, % 127.83/127.83 (E(f9(x47141,x47141),x47141)), % 127.83/127.83 inference(rename_variables,[],[22])). % 127.83/127.83 cnf(4719,plain, % 127.83/127.83 (~P2(f11(f10(x47191,f9(x47192,x47193))),f9(f10(x47191,f9(x47193,x47192)),f10(x47191,f9(x47193,x47192))))), % 127.83/127.83 inference(rename_variables,[],[4506])). % 127.83/127.83 cnf(4732,plain, % 127.83/127.83 (P2(f4(f11(a5),a8,f9(a8,a8)),f9(a8,f9(a8,a8)))), % 127.83/127.83 inference(scs_inference,[],[22,4714,105,2195,3413,4297,137,3839,3866,2166,4272,4629,4266,4607,4506,4719,4662,4640,4656,4702,4648,4658,4652,2,47,48,45,3248,2191,3955,3621,3397,3666,32,2889,18,19,17,3,30,31,36,46,35,37])). % 127.83/127.83 cnf(4753,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x47531,x47532),f9(x47531,x47532)),f9(x47533,x47533))),f2(f9(f9(x47532,x47531),f9(x47532,x47531)),f9(x47533,x47533)))), % 127.83/127.83 inference(scs_inference,[],[3905,3735,915,4654,4630,2,47,45,48,3397,3621])). % 127.83/127.83 cnf(4756,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x47561,x47562),f9(x47561,x47562)),f9(f9(x47563,x47563),f9(x47563,x47563)))),f2(f9(x47562,x47561),x47563))), % 127.83/127.83 inference(scs_inference,[],[3905,3735,915,4648,4652,4654,4700,4630,2,47,45,48,3397,3621,3248,3955,2191])). % 127.83/127.83 cnf(4758,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(f9(x47581,x47581),f9(x47581,x47581)),f9(f9(x47581,x47581),f9(x47581,x47581))),f9(x47582,x47582))),f2(x47581,f9(x47582,x47582)))), % 127.83/127.83 inference(scs_inference,[],[3905,3735,915,4648,4652,4654,4700,4703,4630,2,47,45,48,3397,3621,3248,3955,2191,3666])). % 127.83/127.83 cnf(4800,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x48001,x48002),f9(x48001,x48002)),f9(x48003,x48003))),f2(f9(f9(f9(x48002,x48001),f9(x48002,x48001)),f9(f9(x48002,x48001),f9(x48002,x48001))),f9(x48003,x48003)))), % 127.83/127.83 inference(scs_inference,[],[99,628,4758,4753,2,47,48,3621,3397,3248])). % 127.83/127.83 cnf(4841,plain, % 127.83/127.83 (~P2(f11(f2(f9(x48411,x48411),x48412)),f2(x48411,x48412))), % 127.83/127.83 inference(scs_inference,[],[4506,4753,4376,4800,4701,4756,4614,2,3397,3248,47,48,3621,3955,3666])). % 127.83/127.83 cnf(4879,plain, % 127.83/127.83 (~P2(f11(f2(f9(x48791,x48792),f9(x48793,x48793))),f2(f9(x48792,x48791),x48793))), % 127.83/127.83 inference(scs_inference,[],[4562,4614,2,3248,3397])). % 127.83/127.83 cnf(4880,plain, % 127.83/127.83 (~P2(f11(f2(f9(x48801,x48802),x48803)),f2(f9(x48802,x48801),x48803))), % 127.83/127.83 inference(rename_variables,[],[4614])). % 127.83/127.83 cnf(4883,plain, % 127.83/127.83 (~P2(f11(f2(f9(x48831,x48832),x48833)),f2(f9(f9(x48832,x48831),f9(x48832,x48831)),f9(x48833,x48833)))), % 127.83/127.83 inference(scs_inference,[],[3774,4562,4614,4880,2,3248,3397,47,3621])). % 127.83/127.83 cnf(4884,plain, % 127.83/127.83 (~P2(f11(f2(f9(f9(x48841,x48841),f9(x48841,x48841)),x48842)),f2(x48841,x48842))), % 127.83/127.83 inference(scs_inference,[],[3774,4562,4614,4880,4841,2,3248,3397,47,3621,3666])). % 127.83/127.83 cnf(4897,plain, % 127.83/127.83 (E(f9(f9(f11(a6),f11(a6)),f9(f11(a6),f11(a6))),f9(f10(a6,a5),a8))), % 127.83/127.83 inference(scs_inference,[],[22,105,993,2764,3774,2031,4576,4562,4614,4880,4621,4841,2,3248,3397,47,3621,3666,48,45,3955,2191,32,18,19,3])). % 127.83/127.83 cnf(4929,plain, % 127.83/127.83 (~P2(f11(f2(f9(x49291,x49292),x49293)),f2(f9(f9(f9(x49292,x49291),f9(x49292,x49291)),f9(f9(x49292,x49291),f9(x49292,x49291))),f9(x49293,x49293)))), % 127.83/127.83 inference(scs_inference,[],[4664,4883,2,3248])). % 127.83/127.83 cnf(4930,plain, % 127.83/127.83 (~P2(f11(f2(f9(x49301,x49302),f9(f9(x49303,x49303),f9(x49303,x49303)))),f2(f9(x49302,x49301),x49303))), % 127.83/127.83 inference(scs_inference,[],[4664,4883,4879,2,3248,3397])). % 127.83/127.83 cnf(4935,plain, % 127.83/127.83 (~P2(f11(f2(f9(x49351,x49351),x49352)),f2(x49351,f9(x49352,x49352)))), % 127.83/127.83 inference(scs_inference,[],[4841,4664,4884,4883,4879,2,3248,3397,3621,3666,3955])). % 127.83/127.83 cnf(4949,plain, % 127.83/127.83 (E(f9(f4(x49491,f9(x49492,x49492),x49493),f4(x49491,f9(x49492,x49492),x49493)),f4(x49491,x49492,x49493))), % 127.83/127.83 inference(scs_inference,[],[22,105,2200,4395,2940,101,2398,4621,4841,4664,4685,4884,4883,4879,2,3248,3397,3621,3666,3955,47,45,48,2191,32,18,19,3])). % 127.83/127.83 cnf(4980,plain, % 127.83/127.83 (~P2(f11(f2(f9(x49801,x49802),x49803)),f2(f9(f9(x49802,x49801),f9(x49802,x49801)),f9(f9(x49803,x49803),f9(x49803,x49803))))), % 127.83/127.83 inference(scs_inference,[],[4879,4883,4949,4929,4935,2,3621,3248,3397,3666,3955])). % 127.83/127.83 cnf(4981,plain, % 127.83/127.83 (~P2(f11(f2(f9(x49811,x49812),f9(x49813,x49813))),f2(f9(x49811,x49812),x49813))), % 127.83/127.83 inference(scs_inference,[],[4879,4883,4949,4929,4935,2,3621,3248,3397,3666,3955,2191])). % 127.83/127.83 cnf(5025,plain, % 127.83/127.83 (E(x50251,f9(x50251,x50251))), % 127.83/127.83 inference(rename_variables,[],[105])). % 127.83/127.83 cnf(5032,plain, % 127.83/127.83 ($false), % 127.83/127.83 inference(scs_inference,[],[22,105,5025,2236,4395,2198,3866,2305,4732,4160,4473,4488,4897,4935,4930,4981,4980,2,3397,3248,3955,3621,3666,2191,47,48,45,32,18,19,3,46,30]), % 127.83/127.83 ['proof']). % 127.83/127.83 % SZS output end Proof % 127.83/127.83 % Total time :127.110000s %------------------------------------------------------------------------------