%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU164+3 : TPTP v8.2.0. Bugfixed v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 15:01:28 EDT 2024 % Result : Theorem 181.11s 181.11s % Output : CNFRefutation 181.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU164+3 : TPTP v8.2.0. Bugfixed v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n017.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Fri Jun 21 12:10:39 EDT 2024 % 0.13/0.33 % CPUTime : % 0.52/0.55 start to proof:theBenchmark % 181.06/181.08 %------------------------------------------- % 181.06/181.08 % File :CSE---1.7 % 181.06/181.08 % Problem :theBenchmark % 181.06/181.08 % Transform :cnf % 181.06/181.08 % Format :tptp:raw % 181.06/181.08 % Command :java -jar mcs_scs.jar %d %s % 181.06/181.08 % 181.06/181.08 % Result :Theorem 180.480000s % 181.06/181.08 % Output :CNFRefutation 180.480000s % 181.06/181.08 %------------------------------------------- % 181.11/181.10 %------------------------------------------------------------------------------ % 181.11/181.11 % File : SEU164+3 : TPTP v8.2.0. Bugfixed v4.0.0. % 181.11/181.11 % Domain : Set theory % 181.11/181.11 % Problem : Basic properties of sets, theorem 99 % 181.11/181.11 % Version : [Urb06] axioms : Especial. % 181.11/181.11 % English : % 181.11/181.11 % 181.11/181.11 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 181.11/181.11 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 181.11/181.11 % Source : [Urb06] % 181.11/181.11 % Names : zfmisc_1__t99_zfmisc_1 [Urb06] % 181.11/181.11 % 181.11/181.11 % Status : Theorem % 181.11/181.11 % Rating : 0.44 v8.1.0, 0.42 v7.5.0, 0.38 v7.4.0, 0.43 v7.3.0, 0.38 v7.2.0, 0.34 v7.1.0, 0.35 v7.0.0, 0.40 v6.4.0, 0.38 v6.3.0, 0.42 v6.2.0, 0.52 v6.1.0, 0.67 v6.0.0, 0.52 v5.5.0, 0.56 v5.4.0, 0.61 v5.3.0, 0.63 v5.2.0, 0.50 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.61 v4.0.0 % 181.11/181.11 % Syntax : Number of formulae : 11 ( 4 unt; 0 def) % 181.11/181.11 % Number of atoms : 24 ( 6 equ) % 181.11/181.11 % Maximal formula atoms : 4 ( 2 avg) % 181.11/181.11 % Number of connectives : 15 ( 2 ~; 0 |; 1 &) % 181.11/181.11 % ( 9 <=>; 3 =>; 0 <=; 0 <~>) % 181.11/181.11 % Maximal formula depth : 8 ( 5 avg) % 181.11/181.11 % Maximal term depth : 3 ( 1 avg) % 181.11/181.11 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 181.11/181.11 % Number of functors : 3 ( 3 usr; 0 con; 1-1 aty) % 181.11/181.11 % Number of variables : 25 ( 22 !; 3 ?) % 181.11/181.11 % SPC : FOF_THM_RFO_SEQ % 181.11/181.11 % 181.11/181.11 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 181.11/181.11 % library, www.mizar.org % 181.11/181.11 % Bugfixes : v4.0.0 - Removed duplicate formula t2_tarski % 181.11/181.11 %------------------------------------------------------------------------------ % 181.11/181.11 fof(antisymmetry_r2_hidden,axiom, % 181.11/181.11 ! [A,B] : % 181.11/181.11 ( in(A,B) % 181.11/181.11 => ~ in(B,A) ) ). % 181.11/181.11 % 181.11/181.11 fof(d1_tarski,axiom, % 181.11/181.11 ! [A,B] : % 181.11/181.11 ( B = singleton(A) % 181.11/181.11 <=> ! [C] : % 181.11/181.11 ( in(C,B) % 181.11/181.11 <=> C = A ) ) ). % 181.11/181.11 % 181.11/181.11 fof(d1_zfmisc_1,axiom, % 181.11/181.11 ! [A,B] : % 181.11/181.11 ( B = powerset(A) % 181.11/181.11 <=> ! [C] : % 181.11/181.11 ( in(C,B) % 181.11/181.11 <=> subset(C,A) ) ) ). % 181.11/181.11 % 181.11/181.11 fof(d3_tarski,axiom, % 181.11/181.11 ! [A,B] : % 181.11/181.11 ( subset(A,B) % 181.11/181.11 <=> ! [C] : % 181.11/181.11 ( in(C,A) % 181.11/181.11 => in(C,B) ) ) ). % 181.11/181.11 % 181.11/181.11 fof(d4_tarski,axiom, % 181.11/181.11 ! [A,B] : % 181.11/181.11 ( B = union(A) % 181.11/181.11 <=> ! [C] : % 181.11/181.11 ( in(C,B) % 181.11/181.11 <=> ? [D] : % 181.11/181.11 ( in(C,D) % 181.11/181.11 & in(D,A) ) ) ) ). % 181.11/181.11 % 181.11/181.11 fof(l2_zfmisc_1,axiom, % 181.11/181.11 ! [A,B] : % 181.11/181.11 ( subset(singleton(A),B) % 181.11/181.11 <=> in(A,B) ) ). % 181.11/181.11 % 181.11/181.11 fof(rc1_xboole_0,axiom, % 181.11/181.11 ? [A] : empty(A) ). % 181.11/181.11 % 181.11/181.11 fof(rc2_xboole_0,axiom, % 181.11/181.11 ? [A] : ~ empty(A) ). % 181.11/181.11 % 181.11/181.11 fof(reflexivity_r1_tarski,axiom, % 181.11/181.11 ! [A,B] : subset(A,A) ). % 181.11/181.11 % 181.11/181.11 fof(t2_tarski,axiom, % 181.11/181.11 ! [A,B] : % 181.11/181.11 ( ! [C] : % 181.11/181.11 ( in(C,A) % 181.11/181.11 <=> in(C,B) ) % 181.11/181.11 => A = B ) ). % 181.11/181.11 % 181.11/181.11 fof(t99_zfmisc_1,conjecture, % 181.11/181.11 ! [A] : union(powerset(A)) = A ). % 181.11/181.11 % 181.11/181.11 %------------------------------------------------------------------------------ % 181.11/181.11 %------------------------------------------- % 181.11/181.11 % Proof found % 181.11/181.11 % SZS status Theorem for theBenchmark % 181.11/181.11 % SZS output start Proof % 181.11/181.13 %ClaNum:52(EqnAxiom:26) % 181.11/181.13 %VarNum:153(SingletonVarNum:55) % 181.11/181.13 %MaxLitNum:4 % 181.11/181.13 %MaxfuncDepth:2 % 181.11/181.13 %SharedTerms:8 % 181.11/181.13 %goalClause: 30 % 181.11/181.13 %singleGoalClaCount:1 % 181.11/181.13 [27]P1(a1) % 181.11/181.13 [29]~P1(a9) % 181.11/181.13 [30]~E(f12(f10(a2)),a2) % 181.11/181.13 [28]P2(x281,x281) % 181.11/181.13 [34]~P3(x342,x341)+~P3(x341,x342) % 181.11/181.13 [33]~P3(x331,x332)+P2(f13(x331),x332) % 181.11/181.13 [37]P3(x371,x372)+~P2(f13(x371),x372) % 181.11/181.13 [38]P2(x381,x382)+P3(f3(x381,x382),x381) % 181.11/181.13 [42]P2(x421,x422)+~P3(f3(x421,x422),x422) % 181.11/181.13 [40]E(f4(x402,x401),x402)+P3(f4(x402,x401),x401)+E(x401,f13(x402)) % 181.11/181.13 [43]E(x431,x432)+P3(f11(x431,x432),x432)+P3(f11(x431,x432),x431) % 181.11/181.13 [44]P3(f5(x442,x441),x441)+P2(f5(x442,x441),x442)+E(x441,f10(x442)) % 181.11/181.13 [45]P3(f6(x452,x451),x451)+P3(f8(x452,x451),x452)+E(x451,f12(x452)) % 181.11/181.13 [46]~E(f4(x462,x461),x462)+~P3(f4(x462,x461),x461)+E(x461,f13(x462)) % 181.11/181.13 [47]P3(f6(x472,x471),x471)+P3(f6(x472,x471),f8(x472,x471))+E(x471,f12(x472)) % 181.11/181.13 [48]E(x481,x482)+~P3(f11(x481,x482),x482)+~P3(f11(x481,x482),x481) % 181.11/181.13 [49]~P3(f5(x492,x491),x491)+~P2(f5(x492,x491),x492)+E(x491,f10(x492)) % 181.11/181.13 [39]~P2(x393,x392)+P3(x391,x392)+~P3(x391,x393) % 181.11/181.13 [31]P3(x311,x312)+~E(x311,x313)+~E(x312,f13(x313)) % 181.11/181.13 [32]~P3(x321,x323)+E(x321,x322)+~E(x323,f13(x322)) % 181.11/181.13 [35]~P2(x351,x353)+P3(x351,x352)+~E(x352,f10(x353)) % 181.11/181.13 [36]~P3(x361,x363)+P2(x361,x362)+~E(x363,f10(x362)) % 181.11/181.13 [50]~P3(x501,x503)+~E(x503,f12(x502))+P3(x501,f7(x502,x503,x501)) % 181.11/181.13 [51]~P3(x513,x512)+~E(x512,f12(x511))+P3(f7(x511,x512,x513),x511) % 181.11/181.13 [52]~P3(x523,x522)+~P3(f6(x522,x521),x523)+~P3(f6(x522,x521),x521)+E(x521,f12(x522)) % 181.11/181.13 [41]~P3(x411,x414)+P3(x411,x412)+~P3(x414,x413)+~E(x412,f12(x413)) % 181.11/181.13 %EqnAxiom % 181.11/181.13 [1]E(x11,x11) % 181.11/181.13 [2]E(x22,x21)+~E(x21,x22) % 181.11/181.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 181.11/181.13 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 181.11/181.13 [5]~E(x51,x52)+E(f12(x51),f12(x52)) % 181.11/181.13 [6]~E(x61,x62)+E(f13(x61),f13(x62)) % 181.11/181.13 [7]~E(x71,x72)+E(f11(x71,x73),f11(x72,x73)) % 181.11/181.13 [8]~E(x81,x82)+E(f11(x83,x81),f11(x83,x82)) % 181.11/181.13 [9]~E(x91,x92)+E(f5(x91,x93),f5(x92,x93)) % 181.11/181.13 [10]~E(x101,x102)+E(f5(x103,x101),f5(x103,x102)) % 181.11/181.13 [11]~E(x111,x112)+E(f6(x111,x113),f6(x112,x113)) % 181.11/181.13 [12]~E(x121,x122)+E(f6(x123,x121),f6(x123,x122)) % 181.11/181.13 [13]~E(x131,x132)+E(f8(x131,x133),f8(x132,x133)) % 181.11/181.13 [14]~E(x141,x142)+E(f8(x143,x141),f8(x143,x142)) % 181.11/181.13 [15]~E(x151,x152)+E(f4(x151,x153),f4(x152,x153)) % 181.11/181.13 [16]~E(x161,x162)+E(f4(x163,x161),f4(x163,x162)) % 181.11/181.13 [17]~E(x171,x172)+E(f3(x171,x173),f3(x172,x173)) % 181.11/181.13 [18]~E(x181,x182)+E(f3(x183,x181),f3(x183,x182)) % 181.11/181.13 [19]~E(x191,x192)+E(f7(x191,x193,x194),f7(x192,x193,x194)) % 181.11/181.13 [20]~E(x201,x202)+E(f7(x203,x201,x204),f7(x203,x202,x204)) % 181.11/181.13 [21]~E(x211,x212)+E(f7(x213,x214,x211),f7(x213,x214,x212)) % 181.11/181.13 [22]~P1(x221)+P1(x222)+~E(x221,x222) % 181.11/181.13 [23]P2(x232,x233)+~E(x231,x232)+~P2(x231,x233) % 181.11/181.13 [24]P2(x243,x242)+~E(x241,x242)+~P2(x243,x241) % 181.11/181.13 [25]P3(x252,x253)+~E(x251,x252)+~P3(x251,x253) % 181.11/181.13 [26]P3(x263,x262)+~E(x261,x262)+~P3(x263,x261) % 181.11/181.13 % 181.11/181.13 %------------------------------------------- % 181.17/181.15 cnf(53,plain, % 181.17/181.15 (~P3(x531,f13(x532))+E(x531,x532)), % 181.17/181.15 inference(equality_inference,[],[32])). % 181.17/181.15 cnf(54,plain, % 181.17/181.15 (~P2(x541,x542)+P3(x541,f10(x542))), % 181.17/181.15 inference(equality_inference,[],[35])). % 181.17/181.15 cnf(55,plain, % 181.17/181.15 (~P3(x551,f10(x552))+P2(x551,x552)), % 181.17/181.15 inference(equality_inference,[],[36])). % 181.17/181.15 cnf(56,plain, % 181.17/181.15 (~P3(x561,x562)+P3(x561,f12(x563))+~P3(x562,x563)), % 181.17/181.15 inference(equality_inference,[],[41])). % 181.17/181.15 cnf(57,plain, % 181.17/181.15 (~P3(x571,f12(x572))+P3(x571,f7(x572,f12(x572),x571))), % 181.17/181.15 inference(equality_inference,[],[50])). % 181.17/181.15 cnf(58,plain, % 181.17/181.15 (~P3(x581,f12(x582))+P3(f7(x582,f12(x582),x581),x582)), % 181.17/181.15 inference(equality_inference,[],[51])). % 181.17/181.16 cnf(61,plain, % 181.17/181.16 (P3(x611,f13(x611))), % 181.17/181.16 inference(scs_inference,[],[30,28,53,37])). % 181.17/181.16 cnf(64,plain, % 181.17/181.16 (~E(a2,f12(f10(a2)))), % 181.17/181.16 inference(scs_inference,[],[30,28,53,37,25])). % 181.17/181.16 cnf(67,plain, % 181.17/181.16 (~P3(x671,a2)+P3(x671,f12(f13(a2)))), % 181.17/181.16 inference(scs_inference,[],[30,28,53,37,25,34,56])). % 181.17/181.16 cnf(74,plain, % 181.17/181.16 (~P3(f13(x741),x741)), % 181.17/181.16 inference(scs_inference,[],[61,34])). % 181.17/181.16 cnf(76,plain, % 181.17/181.16 (~P2(f13(f10(x761)),x761)), % 181.17/181.16 inference(scs_inference,[],[61,34,54])). % 181.17/181.16 cnf(78,plain, % 181.17/181.16 (~P3(f10(x781),x781)), % 181.17/181.16 inference(scs_inference,[],[61,34,54,33])). % 181.17/181.16 cnf(80,plain, % 181.17/181.16 (P3(f6(f10(a2),a2),f8(f10(a2),a2))+P3(f6(f10(a2),a2),a2)), % 181.17/181.16 inference(scs_inference,[],[61,64,34,54,33,47])). % 181.17/181.16 cnf(82,plain, % 181.17/181.16 (~E(x821,f13(f10(x821)))), % 181.17/181.16 inference(scs_inference,[],[61,64,28,34,54,33,47,23])). % 181.17/181.16 cnf(83,plain, % 181.17/181.16 (P2(x831,x831)), % 181.17/181.16 inference(rename_variables,[],[28])). % 181.17/181.16 cnf(84,plain, % 181.17/181.16 (~E(f13(f10(x841)),x841)), % 181.17/181.16 inference(scs_inference,[],[61,64,28,83,34,54,33,47,23,24])). % 181.17/181.16 cnf(95,plain, % 181.17/181.16 (~P3(f13(f10(x951)),f13(x951))), % 181.17/181.16 inference(scs_inference,[],[84,53])). % 181.17/181.16 cnf(97,plain, % 181.17/181.16 (~P2(f10(f10(x971)),x971)), % 181.17/181.16 inference(scs_inference,[],[78,84,53,54])). % 181.17/181.16 cnf(100,plain, % 181.17/181.16 (~E(f10(f13(x1001)),x1001)), % 181.17/181.16 inference(scs_inference,[],[78,84,53,54,6])). % 181.17/181.16 cnf(124,plain, % 181.17/181.16 (~P3(f13(f13(f10(x1241))),f10(f13(x1241)))), % 181.17/181.16 inference(scs_inference,[],[95,55,37])). % 181.17/181.16 cnf(126,plain, % 181.17/181.16 (~E(x1261,x1262)+E(f12(f13(x1261)),f12(f13(x1262)))), % 181.17/181.16 inference(scs_inference,[],[5,6])). % 181.17/181.16 cnf(132,plain, % 181.17/181.16 (P3(x1321,f13(x1321))), % 181.17/181.16 inference(rename_variables,[],[61])). % 181.17/181.16 cnf(133,plain, % 181.17/181.16 (~E(x1331,f13(f13(x1331)))), % 181.17/181.16 inference(scs_inference,[],[74,61,132,26,25])). % 181.17/181.16 cnf(151,plain, % 181.17/181.16 (~E(x1511,x1512)+E(f11(f11(x1513,x1511),x1514),f11(f11(x1513,x1512),x1514))), % 181.17/181.16 inference(scs_inference,[],[7,8])). % 181.17/181.16 cnf(168,plain, % 181.17/181.16 (~E(x1681,x1682)+E(f5(f5(x1683,x1681),x1684),f5(f5(x1683,x1682),x1684))), % 181.17/181.16 inference(scs_inference,[],[9,10])). % 181.17/181.16 cnf(170,plain, % 181.17/181.16 (~E(x1701,x1702)+E(f6(f6(x1703,x1701),x1704),f6(f6(x1703,x1702),x1704))), % 181.17/181.16 inference(scs_inference,[],[11,12])). % 181.17/181.16 cnf(172,plain, % 181.17/181.16 (~E(x1721,x1722)+E(f8(f8(x1723,x1721),x1724),f8(f8(x1723,x1722),x1724))), % 181.17/181.16 inference(scs_inference,[],[13,14])). % 181.17/181.16 cnf(174,plain, % 181.17/181.16 (~E(x1741,x1742)+E(f4(f4(x1743,x1741),x1744),f4(f4(x1743,x1742),x1744))), % 181.17/181.16 inference(scs_inference,[],[15,16])). % 181.17/181.16 cnf(176,plain, % 181.17/181.16 (~E(x1761,x1762)+E(f3(f3(x1763,x1761),x1764),f3(f3(x1763,x1762),x1764))), % 181.17/181.16 inference(scs_inference,[],[17,18])). % 181.17/181.16 cnf(178,plain, % 181.17/181.16 (~P3(f7(x1781,f12(x1781),x1782),x1782)+~P3(x1782,f12(x1781))), % 181.17/181.16 inference(scs_inference,[],[57,34])). % 181.17/181.16 cnf(179,plain, % 181.17/181.16 (~P3(x1791,f12(x1791))), % 181.17/181.16 inference(scs_inference,[],[58,178])). % 181.17/181.16 cnf(180,plain, % 181.17/181.16 (~E(x1801,f10(f10(x1801)))), % 181.17/181.16 inference(scs_inference,[],[97,28,23])). % 181.17/181.16 cnf(181,plain, % 181.17/181.16 (P2(x1811,x1811)), % 181.17/181.16 inference(rename_variables,[],[28])). % 181.17/181.16 cnf(184,plain, % 181.17/181.16 (~P3(f10(f10(x1841)),f13(x1841))), % 181.17/181.16 inference(scs_inference,[],[97,28,181,23,24,53])). % 181.17/181.16 cnf(199,plain, % 181.17/181.16 (~E(x1991,x1992)+E(f7(f7(x1993,x1991,x1994),x1995,x1996),f7(f7(x1993,x1992,x1994),x1995,x1996))), % 181.17/181.16 inference(scs_inference,[],[19,20])). % 181.17/181.16 cnf(225,plain, % 181.17/181.16 (~P3(f13(x2251),f13(f12(x2251)))), % 181.17/181.16 inference(scs_inference,[],[179,61,26,53])). % 181.17/181.16 cnf(243,plain, % 181.17/181.16 (~P3(f12(x2431),f13(f13(x2431)))), % 181.17/181.16 inference(scs_inference,[],[225,61,25,53])). % 181.17/181.16 cnf(321,plain, % 181.17/181.16 (~E(a9,a1)), % 181.17/181.16 inference(scs_inference,[],[27,29,22,2])). % 181.17/181.16 cnf(322,plain, % 181.17/181.16 (~P3(a9,f13(a1))), % 181.17/181.16 inference(scs_inference,[],[321,53])). % 181.17/181.16 cnf(324,plain, % 181.17/181.16 (P3(f3(f13(a9),f13(a1)),f13(a9))), % 181.17/181.16 inference(scs_inference,[],[61,322,39,38])). % 181.17/181.16 cnf(327,plain, % 181.17/181.16 (~E(f13(a9),f13(a1))), % 181.17/181.16 inference(scs_inference,[],[322,61,324,34,26])). % 181.17/181.16 cnf(328,plain, % 181.17/181.16 (P3(x3281,f13(x3281))), % 181.17/181.16 inference(rename_variables,[],[61])). % 181.17/181.16 cnf(329,plain, % 181.17/181.16 (~E(a1,a9)), % 181.17/181.16 inference(scs_inference,[],[322,61,328,324,34,26,25])). % 181.17/181.16 cnf(331,plain, % 181.17/181.16 (~P3(f13(a9),f13(f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[322,61,328,324,34,26,25,53])). % 181.17/181.16 cnf(344,plain, % 181.17/181.16 (~P3(a1,f13(a9))), % 181.17/181.16 inference(scs_inference,[],[329,53])). % 181.17/181.16 cnf(347,plain, % 181.17/181.16 (P3(x3471,f13(x3471))), % 181.17/181.16 inference(rename_variables,[],[61])). % 181.17/181.16 cnf(348,plain, % 181.17/181.16 (~E(f13(a1),f13(a9))), % 181.17/181.16 inference(scs_inference,[],[331,61,347,329,53,26,25])). % 181.17/181.16 cnf(363,plain, % 181.17/181.16 (~P3(f13(a1),f13(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[348,53])). % 181.17/181.16 cnf(365,plain, % 181.17/181.16 (~E(f3(f13(a9),f13(a1)),a1)), % 181.17/181.16 inference(scs_inference,[],[344,324,348,53,25])). % 181.17/181.16 cnf(379,plain, % 181.17/181.16 (~P3(f3(f13(a9),f13(a1)),f13(a1))), % 181.17/181.16 inference(scs_inference,[],[365,53])). % 181.17/181.16 cnf(398,plain, % 181.17/181.16 (~E(a1,f3(f13(a9),f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[379,61,25])). % 181.17/181.16 cnf(405,plain, % 181.17/181.16 (~E(f3(f13(a9),f13(a1)),f10(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[78,324,25])). % 181.17/181.16 cnf(435,plain, % 181.17/181.16 (~E(f10(f13(a1)),f13(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[28,363,2,35])). % 181.17/181.16 cnf(437,plain, % 181.17/181.16 (~E(f10(f13(x4371)),f13(f12(x4371)))), % 181.17/181.16 inference(scs_inference,[],[28,225,2,35])). % 181.17/181.16 cnf(441,plain, % 181.17/181.16 (~E(f10(a1),f13(a9))), % 181.17/181.16 inference(scs_inference,[],[28,344,2,35])). % 181.17/181.16 cnf(442,plain, % 181.17/181.16 (~P3(f10(a1),f13(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[441,53])). % 181.17/181.16 cnf(463,plain, % 181.17/181.16 (P3(x4631,f13(x4631))), % 181.17/181.16 inference(rename_variables,[],[61])). % 181.17/181.16 cnf(464,plain, % 181.17/181.16 (~E(f13(a9),f10(a1))), % 181.17/181.16 inference(scs_inference,[],[442,61,463,26,25])). % 181.17/181.16 cnf(466,plain, % 181.17/181.16 (~P3(f13(a9),f13(f10(a1)))), % 181.17/181.16 inference(scs_inference,[],[442,61,463,26,25,53])). % 181.17/181.16 cnf(514,plain, % 181.17/181.16 (~E(f10(f13(a9)),f13(f10(a1)))), % 181.17/181.16 inference(scs_inference,[],[28,466,2,35])). % 181.17/181.16 cnf(516,plain, % 181.17/181.16 (~E(f10(f12(x5161)),f13(f13(x5161)))), % 181.17/181.16 inference(scs_inference,[],[28,243,2,35])). % 181.17/181.16 cnf(530,plain, % 181.17/181.16 (~E(f13(f13(f12(x5301))),f13(f10(f13(x5301))))), % 181.17/181.16 inference(scs_inference,[],[437,61,2,32])). % 181.17/181.16 cnf(531,plain, % 181.17/181.16 (~P2(f13(f13(a9)),f3(f13(a9),f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[324,34,37])). % 181.17/181.16 cnf(535,plain, % 181.17/181.16 (~P3(f13(f13(a9)),x5351)+~E(f3(f13(a9),f13(a1)),f12(x5351))), % 181.17/181.16 inference(scs_inference,[],[324,61,34,41])). % 181.17/181.16 cnf(539,plain, % 181.17/181.16 (P2(f13(f3(f13(f13(a9)),f3(f13(a9),f13(a1)))),f13(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[531,33,38])). % 181.17/181.16 cnf(543,plain, % 181.17/181.16 (~P3(f13(f10(x5431)),x5432)+~E(x5431,f12(x5432))), % 181.17/181.16 inference(scs_inference,[],[76,61,33,41])). % 181.17/181.16 cnf(544,plain, % 181.17/181.16 (~P3(f13(f10(f12(x5441))),x5441)), % 181.17/181.16 inference(equality_inference,[],[543])). % 181.17/181.16 cnf(553,plain, % 181.17/181.16 (~E(x5531,f12(f13(f13(f10(x5531)))))), % 181.17/181.16 inference(scs_inference,[],[28,37,543])). % 181.17/181.16 cnf(560,plain, % 181.17/181.16 (P3(f3(f13(a1),f13(a9)),f13(a1))), % 181.17/181.16 inference(scs_inference,[],[344,37,38])). % 181.17/181.16 cnf(561,plain, % 181.17/181.16 (~P3(f13(a1),f3(f13(a1),f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[560,34])). % 181.17/181.16 cnf(567,plain, % 181.17/181.16 (~P3(f3(f13(a1),f13(a9)),f13(a9))), % 181.17/181.16 inference(scs_inference,[],[322,560,25,53])). % 181.17/181.16 cnf(575,plain, % 181.17/181.16 (P3(x5751,f12(f13(f13(x5751))))), % 181.17/181.16 inference(scs_inference,[],[28,61,37,56])). % 181.17/181.16 cnf(577,plain, % 181.17/181.16 (P3(f3(f13(a9),f13(a1)),f12(f13(f13(a9))))), % 181.17/181.16 inference(scs_inference,[],[28,324,37,56])). % 181.17/181.16 cnf(578,plain, % 181.17/181.16 (P3(f3(f13(x5781),f12(x5781)),f13(x5781))), % 181.17/181.16 inference(scs_inference,[],[179,37,38])). % 181.17/181.16 cnf(584,plain, % 181.17/181.16 (~P3(f13(f10(f10(x5841))),f10(f13(x5841)))), % 181.17/181.16 inference(scs_inference,[],[184,37,55])). % 181.17/181.16 cnf(585,plain, % 181.17/181.16 (~E(f3(f13(x5851),f12(x5851)),f10(f10(x5851)))), % 181.17/181.16 inference(scs_inference,[],[184,578,25])). % 181.17/181.16 cnf(596,plain, % 181.17/181.16 (~P3(f3(f13(a9),f12(a9)),f13(a1))), % 181.17/181.16 inference(scs_inference,[],[344,578,25,53])). % 181.17/181.16 cnf(605,plain, % 181.17/181.16 (~E(f3(f13(a1),f13(a9)),f3(f13(a9),f12(a9)))), % 181.17/181.16 inference(scs_inference,[],[596,560,25])). % 181.17/181.16 cnf(614,plain, % 181.17/181.16 (~P3(f3(f13(a1),f12(a1)),f13(a9))), % 181.17/181.16 inference(scs_inference,[],[322,578,25,53])). % 181.17/181.16 cnf(617,plain, % 181.17/181.16 (~E(f3(f13(a9),f13(a1)),f3(f13(a1),f12(a1)))), % 181.17/181.16 inference(scs_inference,[],[614,324,25])). % 181.17/181.16 cnf(618,plain, % 181.17/181.16 (E(a9,f3(f13(a9),f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[324,53,2])). % 181.17/181.16 cnf(619,plain, % 181.17/181.16 (E(f3(f13(a9),f13(a1)),a9)), % 181.17/181.16 inference(scs_inference,[],[618,2])). % 181.17/181.16 cnf(623,plain, % 181.17/181.16 (~E(f3(f13(a9),f12(a9)),f3(f13(a1),f12(a1)))), % 181.17/181.16 inference(scs_inference,[],[618,614,100,29,578,2,3,22,25])). % 181.17/181.16 cnf(626,plain, % 181.17/181.16 (E(f10(f3(f13(a9),f13(a1))),f10(a9))), % 181.17/181.16 inference(scs_inference,[],[324,53,4])). % 181.17/181.16 cnf(633,plain, % 181.17/181.16 (~P3(f13(f12(f10(a2))),x6331)+~E(f13(a2),f12(x6331))), % 181.17/181.16 inference(scs_inference,[],[30,61,53,41])). % 181.17/181.16 cnf(635,plain, % 181.17/181.16 (~E(f3(f13(a1),f13(a9)),f3(f13(a9),f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[379,560,25])). % 181.17/181.16 cnf(648,plain, % 181.17/181.16 (~P2(f13(f10(a1)),f13(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[441,53,37])). % 181.17/181.16 cnf(655,plain, % 181.17/181.16 (~P2(f13(f10(f12(x6551))),f13(f13(f13(x6551))))), % 181.17/181.16 inference(scs_inference,[],[516,53,37])). % 181.17/181.16 cnf(657,plain, % 181.17/181.16 (E(f3(f13(f13(a9)),f3(f13(a9),f13(a1))),f13(a9))), % 181.17/181.16 inference(scs_inference,[],[531,53,38])). % 181.17/181.16 cnf(669,plain, % 181.17/181.16 (E(f12(f13(f3(f13(a9),f13(a1)))),f12(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[324,53,126])). % 181.17/181.16 cnf(673,plain, % 181.17/181.16 (E(x6731,f3(f13(x6731),f12(x6731)))), % 181.17/181.16 inference(scs_inference,[],[578,53,2])). % 181.17/181.16 cnf(674,plain, % 181.17/181.16 (E(f3(f13(x6741),f12(x6741)),x6741)), % 181.17/181.16 inference(scs_inference,[],[673,2])). % 181.17/181.16 cnf(678,plain, % 181.17/181.16 (P1(f3(f13(a1),f12(a1)))), % 181.17/181.16 inference(scs_inference,[],[673,27,22])). % 181.17/181.16 cnf(682,plain, % 181.17/181.16 (~P2(f13(f3(f13(x6821),f12(x6821))),f13(f10(f10(x6821))))), % 181.17/181.16 inference(scs_inference,[],[585,53,37])). % 181.17/181.16 cnf(688,plain, % 181.17/181.16 (~P2(f13(f3(f13(a1),f13(a9))),f13(f3(f13(a9),f12(a9))))), % 181.17/181.16 inference(scs_inference,[],[605,53,37])). % 181.17/181.16 cnf(692,plain, % 181.17/181.16 (~P2(f13(f3(f13(a9),f13(a1))),f13(f3(f13(a1),f12(a1))))), % 181.17/181.16 inference(scs_inference,[],[617,53,37])). % 181.17/181.16 cnf(697,plain, % 181.17/181.16 (~P2(f13(f3(f13(a9),f12(a9))),f13(f3(f13(a1),f12(a1))))), % 181.17/181.16 inference(scs_inference,[],[623,53,37])). % 181.17/181.16 cnf(698,plain, % 181.17/181.16 (~P2(f13(f3(f13(a1),f13(a9))),f13(f3(f13(a9),f13(a1))))), % 181.17/181.16 inference(scs_inference,[],[635,53,37])). % 181.17/181.16 cnf(699,plain, % 181.17/181.16 (P2(f3(f13(a9),f13(a1)),a9)), % 181.17/181.16 inference(scs_inference,[],[324,28,53,24])). % 181.17/181.16 cnf(700,plain, % 181.17/181.16 (E(f3(f13(f10(a1)),f13(f13(a9))),f10(a1))), % 181.17/181.16 inference(scs_inference,[],[648,53,38])). % 181.17/181.16 cnf(703,plain, % 181.17/181.16 (P3(x7031,f10(x7031))), % 181.17/181.16 inference(scs_inference,[],[61,28,53,35])). % 181.17/181.16 cnf(707,plain, % 181.17/181.16 (P2(f3(f13(x7071),f12(x7071)),x7071)), % 181.17/181.16 inference(scs_inference,[],[673,567,28,560,39,23])). % 181.17/181.16 cnf(708,plain, % 181.17/181.16 (P2(x7081,x7081)), % 181.17/181.16 inference(rename_variables,[],[28])). % 181.17/181.16 cnf(709,plain, % 181.17/181.16 (P2(x7091,f3(f13(x7091),f12(x7091)))), % 181.17/181.16 inference(scs_inference,[],[673,567,28,708,560,39,23,24])). % 181.17/181.16 cnf(711,plain, % 181.17/181.16 (~P3(f13(a1),f10(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[673,567,28,708,560,39,23,24,55])). % 181.17/181.16 cnf(721,plain, % 181.17/181.16 (P3(f3(f13(a9),f13(a1)),f3(f13(f13(a9)),f12(f13(a9))))), % 181.17/181.16 inference(scs_inference,[],[324,674,53,31])). % 181.17/181.16 cnf(723,plain, % 181.17/181.16 (P3(f3(f13(a9),f13(a1)),f10(a9))), % 181.17/181.16 inference(scs_inference,[],[61,699,53,35])). % 181.17/181.16 cnf(724,plain, % 181.17/181.16 (~P2(f10(a9),f13(a1))), % 181.17/181.16 inference(scs_inference,[],[379,723,39])). % 181.17/181.16 cnf(726,plain, % 181.17/181.16 (~P3(f10(a9),f10(f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[379,723,39,55])). % 181.17/181.16 cnf(728,plain, % 181.17/181.16 (P2(f13(x7281),f10(x7281))), % 181.17/181.16 inference(scs_inference,[],[28,54,33])). % 181.17/181.16 cnf(742,plain, % 181.17/181.16 (~P3(f10(x7421),f3(f13(x7421),f12(x7421)))), % 181.17/181.16 inference(scs_inference,[],[707,54,34])). % 181.17/181.16 cnf(745,plain, % 181.17/181.16 (~P2(f10(f13(a1)),f10(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[711,703,39])). % 181.17/181.16 cnf(752,plain, % 181.17/181.16 (P3(x7521,f3(f13(f10(x7521)),f12(f10(x7521))))), % 181.17/181.16 inference(scs_inference,[],[28,673,54,26])). % 181.17/181.16 cnf(758,plain, % 181.17/181.16 (P2(x7581,x7581)), % 181.17/181.16 inference(rename_variables,[],[28])). % 181.17/181.16 cnf(759,plain, % 181.17/181.16 (~E(f13(a1),f10(a9))), % 181.17/181.16 inference(scs_inference,[],[724,28,758,24,23])). % 181.17/181.16 cnf(761,plain, % 181.17/181.16 (~P3(f10(a9),f13(f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[724,28,758,24,23,53])). % 181.17/181.16 cnf(779,plain, % 181.17/181.16 (~P3(f13(a1),f13(f10(a9)))), % 181.17/181.16 inference(scs_inference,[],[759,53])). % 181.17/181.16 cnf(781,plain, % 181.17/181.16 (~P2(f10(f10(a9)),f13(f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[761,703,759,53,39])). % 181.17/181.16 cnf(808,plain, % 181.17/181.16 (~P2(f13(f10(a9)),f13(f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[761,61,39])). % 181.17/181.16 cnf(811,plain, % 181.17/181.16 (~P2(f13(f13(a1)),f13(f10(a9)))), % 181.17/181.16 inference(scs_inference,[],[779,61,39])). % 181.17/181.16 cnf(815,plain, % 181.17/181.16 (~P2(f10(f10(a9)),f10(f13(a1)))), % 181.17/181.16 inference(scs_inference,[],[726,703,39])). % 181.17/181.16 cnf(831,plain, % 181.17/181.16 (~P2(f10(f10(x8311)),f3(f13(x8311),f12(x8311)))), % 181.17/181.16 inference(scs_inference,[],[742,703,39])). % 181.17/181.16 cnf(834,plain, % 181.17/181.16 (~P2(f13(f10(x8341)),f3(f13(x8341),f12(x8341)))), % 181.17/181.16 inference(scs_inference,[],[742,61,39])). % 181.17/181.16 cnf(874,plain, % 181.17/181.16 (P3(x8741,f12(f10(f10(x8741))))), % 181.17/181.16 inference(scs_inference,[],[28,703,54,56])). % 181.17/181.16 cnf(878,plain, % 181.17/181.16 (P3(f3(f13(a9),f13(a1)),f12(f10(f10(a9))))), % 181.17/181.16 inference(scs_inference,[],[28,723,54,56])). % 181.17/181.16 cnf(894,plain, % 181.17/181.16 (P2(f3(f10(f10(x8941)),x8941),f10(x8941))), % 181.17/181.16 inference(scs_inference,[],[97,55,38])). % 181.17/181.16 cnf(895,plain, % 181.17/181.16 (~P1(f3(f13(a9),f12(a9)))), % 181.17/181.16 inference(scs_inference,[],[29,674,22])). % 181.17/181.16 cnf(897,plain, % 181.17/181.16 (P3(f3(f13(a9),f13(a1)),f3(f13(f10(a9)),f12(f10(a9))))), % 181.17/181.16 inference(scs_inference,[],[723,674,55,35])). % 181.17/181.16 cnf(905,plain, % 181.17/181.16 (~P3(f10(f13(x9051)),f10(x9051))), % 181.17/181.16 inference(scs_inference,[],[74,703,39,55])). % 181.17/181.16 cnf(912,plain, % 181.17/181.16 (E(f10(a9),f10(f3(f13(a9),f13(a1))))), % 181.17/181.16 inference(scs_inference,[],[619,4,2])). % 181.17/181.16 cnf(913,plain, % 181.17/181.16 (E(f10(f12(f3(f13(a9),f13(a1)))),f10(f12(a9)))), % 181.17/181.16 inference(scs_inference,[],[619,4,5])). % 181.17/181.16 cnf(914,plain, % 181.17/181.16 (E(f13(f10(f3(f13(a9),f13(a1)))),f13(f10(a9)))), % 181.17/181.16 inference(scs_inference,[],[619,4,6])). % 181.17/181.16 cnf(921,plain, % 181.17/181.16 (~E(f10(f13(x9211)),f3(f13(x9211),f12(x9211)))), % 181.17/181.16 inference(scs_inference,[],[100,674,3])). % 181.17/181.16 cnf(930,plain, % 181.17/181.16 (~P2(f10(x9301),f12(x9301))), % 181.17/181.16 inference(scs_inference,[],[179,703,39])). % 181.17/181.16 cnf(933,plain, % 181.17/181.16 (~P3(f10(x9331),f10(f12(x9331)))), % 181.17/181.16 inference(scs_inference,[],[179,703,39,55])). % 181.17/181.16 cnf(936,plain, % 181.17/181.16 (~P2(f13(x9361),f12(x9361))), % 181.17/181.16 inference(scs_inference,[],[179,61,39])). % 181.17/181.16 cnf(939,plain, % 181.17/181.16 (~P3(f13(x9391),f10(f12(x9391)))), % 181.17/181.16 inference(scs_inference,[],[179,61,39,55])). % 181.17/181.16 cnf(941,plain, % 181.17/181.16 (E(f10(f7(f3(f13(a9),f13(a1)),x9411,x9412)),f10(f7(a9,x9411,x9412)))), % 181.17/181.16 inference(scs_inference,[],[619,4,19])). % 181.17/181.16 cnf(943,plain, % 181.17/181.16 (E(f10(f7(x9431,x9432,f3(f13(a9),f13(a1)))),f10(f7(x9431,x9432,a9)))), % 181.17/181.16 inference(scs_inference,[],[619,4,21])). % 181.17/181.16 cnf(947,plain, % 181.17/181.16 (~P2(f10(f13(x9471)),f13(f12(x9471)))), % 181.17/181.16 inference(scs_inference,[],[225,703,39])). % 181.17/181.16 cnf(964,plain, % 181.17/181.16 (E(f12(f10(f3(f13(a9),f13(a1)))),f12(f10(a9)))), % 181.17/181.16 inference(scs_inference,[],[619,4,5])). % 181.17/181.16 cnf(986,plain, % 181.17/181.16 (E(f10(f7(x9861,f3(f13(a9),f13(a1)),x9862)),f10(f7(x9861,a9,x9862)))), % 181.17/181.16 inference(scs_inference,[],[619,4,20])). % 181.17/181.16 cnf(987,plain, % 181.17/181.16 (~P2(f10(a1),f13(a9))), % 181.17/181.16 inference(scs_inference,[],[344,703,39])). % 181.17/181.16 cnf(990,plain, % 181.17/181.16 (~P3(f10(a1),f10(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[344,703,39,55])). % 181.17/181.16 cnf(1016,plain, % 181.17/181.16 (~P2(f10(f10(a1)),f13(f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[442,703,39])). % 181.17/181.16 cnf(1052,plain, % 181.17/181.16 (~P2(f13(f13(a1)),f3(f13(a1),f13(a9)))), % 181.17/181.16 inference(scs_inference,[],[561,61,39])). % 181.17/181.16 cnf(1062,plain, % 181.17/181.16 (E(f12(f3(f13(x10621),f12(x10621))),f12(x10621))), % 181.17/181.16 inference(scs_inference,[],[578,5,53])). % 181.17/181.16 cnf(1083,plain, % 181.17/181.16 (E(f10(f12(a9)),f10(f12(f3(f13(a9),f13(a1)))))), % 181.17/181.16 inference(scs_inference,[],[618,5,4])). % 181.17/181.16 cnf(1087,plain, % 181.17/181.16 (E(f3(x10871,f12(f3(f13(a9),f13(a1)))),f3(x10871,f12(a9)))), % 181.17/181.16 inference(scs_inference,[],[619,5,18])). % 181.17/181.16 cnf(1094,plain, % 181.17/181.16 (E(f12(f10(x10941)),f12(f10(f3(f13(x10941),f12(x10941)))))), % 181.17/181.16 inference(scs_inference,[],[673,5,4])). % 181.17/181.16 cnf(1095,plain, % 181.17/181.16 (P3(f3(f13(x10951),f12(x10951)),f10(x10951))), % 181.17/181.16 inference(scs_inference,[],[673,703,25])). % 181.17/181.16 cnf(1105,plain, % 181.17/181.16 (~P3(x11051,f3(f13(f13(x11052)),f12(f13(x11052))))+E(f12(x11051),f12(x11052))), % 181.17/181.16 inference(scs_inference,[],[674,5,32])). % 181.17/181.17 cnf(1116,plain, % 181.17/181.17 (E(f10(f13(f3(f13(a9),f13(a1)))),f10(f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[619,6,4])). % 181.17/181.17 cnf(1131,plain, % 181.17/181.17 (~P3(x11311,f13(f10(f13(x11311))))), % 181.17/181.17 inference(scs_inference,[],[82,6,53])). % 181.17/181.17 cnf(1157,plain, % 181.17/181.17 (~P2(f13(f10(x11571)),f10(f12(x11571)))), % 181.17/181.17 inference(scs_inference,[],[933,61,39])). % 181.17/181.17 cnf(1167,plain, % 181.17/181.17 (~P2(f13(f13(x11671)),f10(f12(x11671)))), % 181.17/181.17 inference(scs_inference,[],[939,61,39])). % 181.17/181.17 cnf(1183,plain, % 181.17/181.17 (~P2(f13(f10(a1)),f10(f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[990,61,39])). % 181.17/181.17 cnf(1188,plain, % 181.17/181.17 (P2(f13(f3(f10(f10(a1)),f13(f13(a9)))),f10(f10(a1)))), % 181.17/181.17 inference(scs_inference,[],[1016,38,33])). % 181.17/181.17 cnf(1194,plain, % 181.17/181.17 (P2(f13(f3(f13(f13(a1)),f3(f13(a1),f13(a9)))),f13(f13(a1)))), % 181.17/181.17 inference(scs_inference,[],[1052,38,33])). % 181.17/181.17 cnf(1197,plain, % 181.17/181.17 (P3(f3(f10(a1),f13(a9)),f10(a1))), % 181.17/181.17 inference(scs_inference,[],[1095,614,38,39])). % 181.17/181.17 cnf(1201,plain, % 181.17/181.17 (P3(f3(f10(a9),f13(a1)),f10(a9))), % 181.17/181.17 inference(scs_inference,[],[723,379,38,39])). % 181.17/181.17 cnf(1202,plain, % 181.17/181.17 (~P3(f10(a9),f3(f10(a9),f13(a1)))), % 181.17/181.17 inference(scs_inference,[],[1201,34])). % 181.17/181.17 cnf(1207,plain, % 181.17/181.17 (P2(f13(f3(f13(f13(x12071)),f10(f12(x12071)))),f13(f13(x12071)))), % 181.17/181.17 inference(scs_inference,[],[1167,38,33])). % 181.17/181.17 cnf(1210,plain, % 181.17/181.17 (P3(f3(f10(a1),f12(f3(f10(a1),f13(a9)))),f10(a1))), % 181.17/181.17 inference(scs_inference,[],[1197,179,38,39])). % 181.17/181.17 cnf(1221,plain, % 181.17/181.17 (P3(f3(f13(f13(x12211)),x12211),f13(f13(x12211)))), % 181.17/181.17 inference(scs_inference,[],[74,38,37])). % 181.17/181.17 cnf(1226,plain, % 181.17/181.17 (~E(f10(f3(f13(f10(x12261)),x12261)),x12261)), % 181.17/181.17 inference(scs_inference,[],[76,703,42,26])). % 181.17/181.17 cnf(1231,plain, % 181.17/181.17 (~P3(f3(f13(x12311),f12(x12311)),f12(x12311))), % 181.17/181.17 inference(scs_inference,[],[179,42,37])). % 181.17/181.17 cnf(1248,plain, % 181.17/181.17 (~E(f12(f10(f13(f10(x12481)))),x12481)), % 181.17/181.17 inference(scs_inference,[],[703,543,2])). % 181.17/181.17 cnf(1250,plain, % 181.17/181.17 (~E(x12501,f10(f13(f10(f12(x12501)))))), % 181.17/181.17 inference(scs_inference,[],[703,543,5])). % 181.17/181.17 cnf(1254,plain, % 181.17/181.17 (~E(x12541,f13(f10(f12(f13(x12541)))))), % 181.17/181.17 inference(scs_inference,[],[61,543,126])). % 181.17/181.17 cnf(1275,plain, % 181.17/181.17 (~E(f3(f10(a1),f13(a9)),f10(f13(a1)))), % 181.17/181.17 inference(scs_inference,[],[905,1197,25])). % 181.17/181.17 cnf(1330,plain, % 181.17/181.17 (P3(f3(f13(a1),f13(a9)),f10(a1))), % 181.17/181.17 inference(scs_inference,[],[728,560,39])). % 181.17/181.17 cnf(1335,plain, % 181.17/181.17 (~P3(f10(a1),f3(f13(a1),f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[728,905,560,39,25,34])). % 181.17/181.17 cnf(1692,plain, % 181.17/181.17 (E(f10(f4(a9,x16921)),f10(f4(f3(f13(a9),f13(a1)),x16921)))), % 181.17/181.17 inference(scs_inference,[],[618,15,4])). % 181.17/181.17 cnf(1704,plain, % 181.17/181.17 (~P3(x17041,f3(f13(f13(x17042)),f12(f13(x17042))))+E(f4(x17041,x17043),f4(x17042,x17043))), % 181.17/181.17 inference(scs_inference,[],[674,15,32])). % 181.17/181.17 cnf(1779,plain, % 181.17/181.17 (~P3(x17791,f3(f13(f13(x17792)),f12(f13(x17792))))+E(f3(x17791,x17793),f3(x17792,x17793))), % 181.17/181.17 inference(scs_inference,[],[674,17,32])). % 181.17/181.17 cnf(1819,plain, % 181.17/181.17 (E(f12(f13(a9)),f12(f13(f3(f13(a9),f13(a1)))))), % 181.17/181.17 inference(scs_inference,[],[619,126,2])). % 181.17/181.17 cnf(1837,plain, % 181.17/181.17 (E(f12(f13(x18371)),f12(f13(x18372)))+~P3(x18371,f3(f13(f13(x18372)),f12(f13(x18372))))), % 181.17/181.17 inference(scs_inference,[],[674,126,32])). % 181.17/181.17 cnf(1847,plain, % 181.17/181.17 (E(f12(f13(f3(f13(a1),f13(a9)))),f12(f13(a1)))), % 181.17/181.17 inference(scs_inference,[],[560,126,53])). % 181.17/181.17 cnf(1888,plain, % 181.17/181.17 (~P3(x18881,f12(x18882))+P2(f13(x18881),f7(x18882,f12(x18882),x18881))), % 181.17/181.17 inference(scs_inference,[],[57,33])). % 181.17/181.17 cnf(1889,plain, % 181.17/181.17 (P3(f13(x18891),f10(f7(x18892,f12(x18892),x18891)))+~P3(x18891,f12(x18892))), % 181.17/181.17 inference(scs_inference,[],[1888,54])). % 181.17/181.17 cnf(1891,plain, % 181.17/181.17 (~P3(f3(f13(a9),f13(a1)),f12(x18911))+P3(a9,f7(x18911,f12(x18911),f3(f13(a9),f13(a1))))), % 181.17/181.17 inference(scs_inference,[],[619,57,25])). % 181.17/181.17 cnf(1900,plain, % 181.17/181.17 (~P3(f10(x19001),f12(x19002))+~E(f7(x19002,f12(x19002),f10(x19001)),f10(f12(x19001)))), % 181.17/181.17 inference(scs_inference,[],[930,57,36])). % 181.17/181.17 cnf(1901,plain, % 181.17/181.17 (~E(f10(f12(x19011)),f7(x19012,f12(x19012),f10(x19011)))+~P3(f10(x19011),f12(x19012))), % 181.17/181.17 inference(scs_inference,[],[1900,2])). % 181.17/181.17 cnf(1934,plain, % 181.17/181.17 (~P3(f10(a9),f12(x19341))+~P2(f7(x19341,f12(x19341),f10(a9)),f3(f10(a9),f13(a1)))), % 181.17/181.17 inference(scs_inference,[],[1202,57,39])). % 181.17/181.17 cnf(1939,plain, % 181.17/181.17 (~P3(f10(a9),f12(x19391))+~P2(f7(x19391,f12(x19391),f10(a9)),f13(f13(a1)))), % 181.17/181.17 inference(scs_inference,[],[761,57,39])). % 181.17/181.17 cnf(1949,plain, % 181.17/181.17 (~P3(f10(a1),f12(x19491))+~P2(f7(x19491,f12(x19491),f10(a1)),f3(f13(a1),f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[1335,57,39])). % 181.17/181.17 cnf(1954,plain, % 181.17/181.17 (~P3(f13(a1),f12(x19541))+~P2(f7(x19541,f12(x19541),f13(a1)),f13(f10(a9)))), % 181.17/181.17 inference(scs_inference,[],[779,57,39])). % 181.17/181.17 cnf(1963,plain, % 181.17/181.17 (~P3(x19631,f12(x19632))+~P2(f7(x19632,f12(x19632),x19631),f12(x19631))), % 181.17/181.17 inference(scs_inference,[],[179,57,39])). % 181.17/181.17 cnf(1966,plain, % 181.17/181.17 (~P3(f13(x19661),f12(x19662))+~P2(f7(x19662,f12(x19662),f13(x19661)),f13(f12(x19661)))), % 181.17/181.17 inference(scs_inference,[],[225,57,39])). % 181.17/181.17 cnf(1969,plain, % 181.17/181.17 (~P3(a9,f12(x19691))+~E(f7(x19691,f12(x19691),a9),f13(a1))), % 181.17/181.17 inference(scs_inference,[],[321,57,32])). % 181.17/181.17 cnf(1970,plain, % 181.17/181.17 (~E(f13(a1),f7(x19701,f12(x19701),a9))+~P3(a9,f12(x19701))), % 181.17/181.17 inference(scs_inference,[],[1969,2])). % 181.17/181.17 cnf(1971,plain, % 181.17/181.17 (~P3(f13(a1),f13(f7(x19711,f12(x19711),a9)))+~P3(a9,f12(x19711))), % 181.17/181.17 inference(scs_inference,[],[1970,53])). % 181.17/181.17 cnf(1972,plain, % 181.17/181.17 (~P3(f13(a9),f12(x19721))+~E(f7(x19721,f12(x19721),f13(a9)),f13(f13(a1)))), % 181.17/181.17 inference(scs_inference,[],[327,57,32])). % 181.17/181.17 cnf(1973,plain, % 181.17/181.17 (~E(f13(f13(a1)),f7(x19731,f12(x19731),f13(a9)))+~P3(f13(a9),f12(x19731))), % 181.17/181.17 inference(scs_inference,[],[1972,2])). % 181.17/181.17 cnf(1976,plain, % 181.17/181.17 (~P3(f13(a1),f12(x19761))+~P2(f7(x19761,f12(x19761),f13(a1)),f13(f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[363,57,39])). % 181.17/181.17 cnf(1979,plain, % 181.17/181.17 (~P3(a1,f12(x19791))+~E(f7(x19791,f12(x19791),a1),f13(f3(f13(a9),f13(a1))))), % 181.17/181.17 inference(scs_inference,[],[398,57,32])). % 181.17/181.17 cnf(1980,plain, % 181.17/181.17 (~P3(f3(f13(a9),f13(a1)),f12(x19801))+~E(f7(x19801,f12(x19801),f3(f13(a9),f13(a1))),f13(f10(f13(a9))))), % 181.17/181.17 inference(scs_inference,[],[405,57,32])). % 181.17/181.17 cnf(1983,plain, % 181.17/181.17 (~P3(f10(a1),f12(x19831))+~P2(f7(x19831,f12(x19831),f10(a1)),f13(f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[442,57,39])). % 181.17/181.17 cnf(1985,plain, % 181.17/181.17 (~P3(f13(a9),f12(x19851))+~P2(f7(x19851,f12(x19851),f13(a9)),f13(f10(a1)))), % 181.17/181.17 inference(scs_inference,[],[466,57,39])). % 181.17/181.17 cnf(1989,plain, % 181.17/181.17 (~P3(x19891,f12(x19892))+P3(f3(f13(x19891),f12(x19891)),f7(x19892,f12(x19892),f3(f13(x19891),f12(x19891))))), % 181.17/181.17 inference(scs_inference,[],[673,57,25])). % 181.17/181.17 cnf(1991,plain, % 181.17/181.17 (P3(f3(f10(x19911),f12(x19911)),f10(x19911))), % 181.17/181.17 inference(scs_inference,[],[930,38])). % 181.17/181.17 cnf(1995,plain, % 181.17/181.17 (P3(f13(x19951),f10(f10(x19951)))), % 181.17/181.17 inference(scs_inference,[],[987,930,728,38,42,54])). % 181.17/181.17 cnf(1999,plain, % 181.17/181.17 (E(f3(f13(a1),f13(a9)),a1)), % 181.17/181.17 inference(scs_inference,[],[987,930,1330,728,560,38,42,54,55,53])). % 181.17/181.17 cnf(2006,plain, % 181.17/181.17 (~P3(f10(x20061),f13(f12(x20061)))), % 181.17/181.17 inference(scs_inference,[],[987,1231,930,1330,728,933,707,560,38,42,54,55,53,34,35,39])). % 181.17/181.17 cnf(2016,plain, % 181.17/181.17 (~P3(f3(f10(x20161),f12(x20161)),f12(x20161))), % 181.17/181.17 inference(scs_inference,[],[930,42])). % 181.17/181.17 cnf(2018,plain, % 181.17/181.17 (P2(f3(f10(x20181),f12(x20181)),x20181)), % 181.17/181.17 inference(scs_inference,[],[1991,930,42,55])). % 181.17/181.17 cnf(2027,plain, % 181.17/181.17 (P2(f3(f10(a9),f13(a1)),a9)), % 181.17/181.17 inference(scs_inference,[],[1201,55])). % 181.17/181.17 cnf(2029,plain, % 181.17/181.17 (~P3(f13(x20291),f3(f10(x20291),f12(x20291)))), % 181.17/181.17 inference(scs_inference,[],[2018,1201,74,55,39])). % 181.17/181.17 cnf(2043,plain, % 181.17/181.17 (P2(f3(f13(x20431),f12(x20431)),x20432)+~E(f10(x20431),f10(x20432))), % 181.17/181.17 inference(scs_inference,[],[2027,1095,1197,74,55,39,36])). % 181.17/181.17 cnf(2069,plain, % 181.17/181.17 (P2(f3(f10(x20691),f12(x20691)),x20692)+~E(f10(x20691),f10(x20692))), % 181.17/181.17 inference(scs_inference,[],[1991,36])). % 181.17/181.17 cnf(2071,plain, % 181.17/181.17 (P3(f3(f10(x20711),f12(x20711)),f10(x20712))+~E(f10(x20711),f10(x20712))), % 181.17/181.17 inference(scs_inference,[],[1991,36,54])). % 181.17/181.17 cnf(2073,plain, % 181.17/181.17 (~P3(f10(x20731),f3(f10(x20732),f12(x20732)))+~E(f10(x20732),f10(x20731))), % 181.17/181.17 inference(scs_inference,[],[1991,36,54,34])). % 181.17/181.17 cnf(2075,plain, % 181.17/181.17 (~E(f12(x20751),f10(x20752))+~E(f10(x20751),f10(x20752))), % 181.17/181.17 inference(scs_inference,[],[2016,1991,36,54,34,35])). % 181.17/181.17 cnf(2088,plain, % 181.17/181.17 (P3(f8(f10(a2),a2),f10(a2))+P3(f6(f10(a2),a2),a2)), % 181.17/181.17 inference(scs_inference,[],[64,45])). % 181.17/181.17 cnf(2101,plain, % 181.17/181.17 (P2(a1,f3(f13(a1),f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[28,1999,1330,36,23])). % 181.17/181.17 cnf(2122,plain, % 181.17/181.17 (P2(f3(f10(a9),f13(a1)),x21221)+~E(f10(a9),f10(x21221))), % 181.17/181.17 inference(scs_inference,[],[1201,36])). % 181.17/181.17 cnf(2124,plain, % 181.17/181.17 (P3(f3(f10(a9),f13(a1)),f10(x21241))+~E(f10(a9),f10(x21241))), % 181.17/181.17 inference(scs_inference,[],[1201,36,54])). % 181.17/181.17 cnf(2305,plain, % 181.17/181.17 (~P3(a1,f3(f13(x23051),f12(x23051)))+~E(f13(a9),f12(f10(x23051)))), % 181.17/181.17 inference(scs_inference,[],[1095,344,41])). % 181.17/181.17 cnf(2346,plain, % 181.17/181.17 (~P3(x23461,f3(f10(x23462),f12(x23462)))+~E(f12(x23461),f12(f10(x23462)))), % 181.17/181.17 inference(scs_inference,[],[1991,179,41])). % 181.17/181.17 cnf(2348,plain, % 181.17/181.17 (~P2(f13(x23481),f3(f10(x23482),f12(x23482)))+~E(f12(x23481),f12(f10(x23482)))), % 181.17/181.17 inference(scs_inference,[],[1991,179,41,37])). % 181.17/181.17 cnf(2353,plain, % 181.17/181.17 (P3(f8(f10(a2),a2),f10(a2))), % 181.17/181.17 inference(scs_inference,[],[703,64,2088,52])). % 181.17/181.17 cnf(2354,plain, % 181.17/181.17 (~P3(f10(a2),f8(f10(a2),a2))), % 181.17/181.17 inference(scs_inference,[],[2353,34])). % 181.17/181.17 cnf(2356,plain, % 181.17/181.17 (P2(f8(f10(a2),a2),a2)), % 181.17/181.17 inference(scs_inference,[],[2353,34,55])). % 181.17/181.17 cnf(2397,plain, % 181.17/181.17 (~P3(a9,f3(f13(x23971),f12(x23971)))+~E(f13(a1),f12(f10(x23971)))), % 181.17/181.17 inference(scs_inference,[],[1095,322,41])). % 181.17/181.17 cnf(2400,plain, % 181.17/181.17 (~P3(f13(a9),f13(f12(f10(x24001))))+~P3(a1,f3(f13(x24001),f12(x24001)))), % 181.17/181.17 inference(scs_inference,[],[2305,53])). % 181.17/181.17 cnf(2414,plain, % 181.17/181.17 (~P3(x24141,f8(f10(a2),a2))+~E(f12(x24141),f12(f10(a2)))), % 181.17/181.17 inference(scs_inference,[],[2353,179,41])). % 181.17/181.17 cnf(2420,plain, % 181.17/181.17 (~E(f12(f10(x24201)),f13(a1))+~P3(a9,f3(f13(x24201),f12(x24201)))), % 181.17/181.17 inference(scs_inference,[],[2397,2])). % 181.17/181.17 cnf(2427,plain, % 181.17/181.17 (~P3(f12(f10(x24271)),f13(f13(a1)))+~P3(a9,f3(f13(x24271),f12(x24271)))), % 181.17/181.17 inference(scs_inference,[],[2420,53])). % 181.17/181.17 cnf(2440,plain, % 181.17/181.17 (~P3(x24401,f3(f13(x24402),f12(x24402)))+~E(f12(x24401),f12(f10(x24402)))), % 181.17/181.17 inference(scs_inference,[],[1095,179,41])). % 181.17/181.17 cnf(2467,plain, % 181.17/181.17 (~P3(f6(f10(a2),a2),a2)), % 181.17/181.17 inference(scs_inference,[],[64,703,52])). % 181.17/181.17 cnf(2470,plain, % 181.17/181.17 (P3(f6(f10(a2),a2),f8(f10(a2),a2))), % 181.17/181.17 inference(scs_inference,[],[2467,80])). % 181.17/181.17 cnf(2542,plain, % 181.17/181.17 (~P3(x25421,f3(f10(a9),f13(a1)))+~E(f12(x25421),f12(f10(a9)))), % 181.17/181.17 inference(scs_inference,[],[179,1201,41])). % 181.17/181.17 cnf(2544,plain, % 181.17/181.17 (~P2(f13(x25441),f3(f10(a9),f13(a1)))+~E(f12(x25441),f12(f10(a9)))), % 181.17/181.17 inference(scs_inference,[],[179,1201,41,37])). % 181.17/181.17 cnf(2583,plain, % 181.17/181.17 (~P3(a9,f3(f13(x25831),f12(x25831)))+~E(f13(a1),f12(f13(x25831)))), % 181.17/181.17 inference(scs_inference,[],[578,322,41])). % 181.17/181.17 cnf(2585,plain, % 181.17/181.17 (~E(f12(f13(x25851)),f13(a1))+~P3(a9,f3(f13(x25851),f12(x25851)))), % 181.17/181.17 inference(scs_inference,[],[2583,2])). % 181.17/181.17 cnf(2586,plain, % 181.17/181.17 (~P3(f12(f13(x25861)),f13(f13(a1)))+~P3(a9,f3(f13(x25861),f12(x25861)))), % 181.17/181.17 inference(scs_inference,[],[2585,53])). % 181.17/181.17 cnf(2649,plain, % 181.17/181.17 (~P3(x26491,f3(f13(x26492),f12(x26492)))+~E(f12(x26491),f12(f13(x26492)))), % 181.17/181.17 inference(scs_inference,[],[179,578,41])). % 181.17/181.17 cnf(2676,plain, % 181.17/181.17 (~P3(a1,f3(f13(x26761),f12(x26761)))+~E(f13(a9),f12(f13(x26761)))), % 181.17/181.17 inference(scs_inference,[],[344,578,41])). % 181.17/181.17 cnf(2678,plain, % 181.17/181.17 (~E(f12(f13(x26781)),f13(a9))+~P3(a1,f3(f13(x26781),f12(x26781)))), % 181.17/181.17 inference(scs_inference,[],[2676,2])). % 181.17/181.17 cnf(2679,plain, % 181.17/181.17 (~P3(f12(f13(x26791)),f13(f13(a9)))+~P3(a1,f3(f13(x26791),f12(x26791)))), % 181.17/181.17 inference(scs_inference,[],[2678,53])). % 181.17/181.17 cnf(2745,plain, % 181.17/181.17 (~P3(x27451,f3(f13(a1),f13(a9)))+~E(f12(x27451),f12(f13(a1)))), % 181.17/181.17 inference(scs_inference,[],[179,560,41])). % 181.17/181.17 cnf(2754,plain, % 181.17/181.17 (~P3(x27541,f3(f13(a9),f13(a1)))+~E(f12(x27541),f12(f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[324,179,41])). % 181.17/181.17 cnf(2756,plain, % 181.17/181.17 (~P2(f13(x27561),f3(f13(a9),f13(a1)))+~E(f12(x27561),f12(f13(a9)))), % 181.17/181.17 inference(scs_inference,[],[324,179,41,37])). % 181.17/181.17 cnf(2791,plain, % 181.17/181.17 (~P3(x27911,f3(f13(a9),f13(a1)))+~E(f12(x27911),f12(f10(a9)))), % 181.17/181.17 inference(scs_inference,[],[723,179,41])). % 181.17/181.17 cnf(2843,plain, % 181.17/181.17 (~E(f10(x28431),f12(x28432))+~E(f10(x28432),f10(x28431))), % 181.17/181.17 inference(scs_inference,[],[2075,2])). % 181.17/181.17 cnf(2846,plain, % 181.17/181.17 (~E(f10(x28461),f10(x28462))+~P3(f12(x28461),f13(f10(x28462)))), % 181.17/181.17 inference(scs_inference,[],[2075,53])). % 181.17/181.17 cnf(2850,plain, % 181.17/181.17 (~E(f10(x28501),f10(x28502))+~E(f13(f12(x28501)),f13(f10(x28502)))), % 181.17/181.17 inference(scs_inference,[],[61,2075,32])). % 181.17/181.17 cnf(2855,plain, % 181.17/181.17 (~E(f10(x28551),f10(x28552))+~E(f10(f12(x28551)),f13(f10(x28552)))), % 181.17/181.17 inference(scs_inference,[],[703,2075,32])). % 181.17/181.17 cnf(2856,plain, % 181.17/181.17 (~E(f12(x28561),f10(x28562))+~E(f13(f10(x28561)),f13(f10(x28562)))), % 181.17/181.17 inference(scs_inference,[],[61,2075,32])). % 181.17/181.17 cnf(3160,plain, % 181.17/181.17 (~P3(f13(f10(f12(x31601))),x31601)), % 181.17/181.17 inference(rename_variables,[],[544])). % 181.17/181.17 cnf(3162,plain, % 181.17/181.17 (~E(x31621,f12(f10(f10(f10(x31621)))))), % 181.17/181.17 inference(scs_inference,[],[1062,544,1995,5,67,543])). % 181.17/181.17 cnf(3163,plain, % 181.17/181.17 (P3(f13(x31631),f10(f10(x31631)))), % 181.17/181.17 inference(rename_variables,[],[1995])). % 181.17/181.17 cnf(3181,plain, % 181.17/181.17 (E(f12(f13(x31811)),f12(f13(f3(f13(x31811),f12(x31811)))))), % 181.17/181.17 inference(scs_inference,[],[1062,544,575,1995,673,5,67,543,7,8,9,10,11,12,13,14,15,16,17,18,57,58,126])). % 181.17/181.17 cnf(3202,plain, % 181.17/181.17 (P3(f13(x32021),f10(f10(x32021)))), % 181.17/181.17 inference(rename_variables,[],[1995])). % 181.17/181.17 cnf(3213,plain, % 181.17/181.17 (P3(x32131,f12(f13(f13(x32131))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3216,plain, % 181.17/181.17 (E(f12(f3(f13(x32161),f12(x32161))),f12(x32161))), % 181.17/181.17 inference(rename_variables,[],[1062])). % 181.17/181.17 cnf(3221,plain, % 181.17/181.17 (E(f12(f3(f13(x32211),f12(x32211))),f12(x32211))), % 181.17/181.17 inference(rename_variables,[],[1062])). % 181.17/181.17 cnf(3225,plain, % 181.17/181.17 (~E(f12(f6(f10(a2),a2)),f12(f10(a2)))), % 181.17/181.17 inference(scs_inference,[],[2470,1062,3216,626,544,575,912,752,914,1999,1995,3163,673,5,67,543,7,8,9,10,11,12,13,14,15,16,17,18,57,58,126,2843,19,20,21,1888,2846,2043,2069,151,168,170,172,174,176,633,1889,2850,2855,2856,1969,2346,2440,2649,2122,2414])). % 181.17/181.17 cnf(3228,plain, % 181.17/181.17 (P3(x32281,f12(f13(f13(x32281))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3231,plain, % 181.17/181.17 (P3(x32311,f3(f13(f10(x32311)),f12(f10(x32311))))), % 181.17/181.17 inference(rename_variables,[],[752])). % 181.17/181.17 cnf(3234,plain, % 181.17/181.17 (E(f12(f3(f13(x32341),f12(x32341))),f12(x32341))), % 181.17/181.17 inference(rename_variables,[],[1062])). % 181.17/181.17 cnf(3237,plain, % 181.17/181.17 (P3(x32371,f3(f13(f10(x32371)),f12(f10(x32371))))), % 181.17/181.17 inference(rename_variables,[],[752])). % 181.17/181.17 cnf(3240,plain, % 181.17/181.17 (P3(x32401,f3(f13(f10(x32401)),f12(f10(x32401))))), % 181.17/181.17 inference(rename_variables,[],[752])). % 181.17/181.17 cnf(3243,plain, % 181.17/181.17 (P3(x32431,f3(f13(f10(x32431)),f12(f10(x32431))))), % 181.17/181.17 inference(rename_variables,[],[752])). % 181.17/181.17 cnf(3250,plain, % 181.17/181.17 (P3(x32501,f12(f13(f13(x32501))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3253,plain, % 181.17/181.17 (P3(x32531,f12(f13(f13(x32531))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3256,plain, % 181.17/181.17 (P3(x32561,f12(f13(f13(x32561))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3261,plain, % 181.17/181.17 (E(f12(f3(f13(x32611),f12(x32611))),f12(x32611))), % 181.17/181.17 inference(rename_variables,[],[1062])). % 181.17/181.17 cnf(3264,plain, % 181.17/181.17 (E(f12(f3(f13(x32641),f12(x32641))),f12(x32641))), % 181.17/181.17 inference(rename_variables,[],[1062])). % 181.17/181.17 cnf(3267,plain, % 181.17/181.17 (E(f12(f3(f13(x32671),f12(x32671))),f12(x32671))), % 181.17/181.17 inference(rename_variables,[],[1062])). % 181.17/181.17 cnf(3270,plain, % 181.17/181.17 (P3(x32701,f3(f13(f10(x32701)),f12(f10(x32701))))), % 181.17/181.17 inference(rename_variables,[],[752])). % 181.17/181.17 cnf(3276,plain, % 181.17/181.17 (E(f12(f3(f13(x32761),f12(x32761))),f12(x32761))), % 181.17/181.17 inference(rename_variables,[],[1062])). % 181.17/181.17 cnf(3279,plain, % 181.17/181.17 (E(f12(f3(f13(x32791),f12(x32791))),f12(x32791))), % 181.17/181.17 inference(rename_variables,[],[1062])). % 181.17/181.17 cnf(3282,plain, % 181.17/181.17 (P3(x32821,f12(f13(f13(x32821))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3285,plain, % 181.17/181.17 (P3(x32851,f12(f13(f13(x32851))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3288,plain, % 181.17/181.17 (P3(x32881,f12(f13(f13(x32881))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3291,plain, % 181.17/181.17 (P3(x32911,f12(f13(f13(x32911))))), % 181.17/181.17 inference(rename_variables,[],[575])). % 181.17/181.17 cnf(3300,plain, % 181.17/181.17 (E(f10(f12(f3(f13(x33001),f12(x33001)))),f10(f12(x33001)))), % 181.17/181.17 inference(scs_inference,[],[2470,1062,3216,3221,3234,3261,3264,3267,3276,3279,626,544,575,3213,3228,3250,3253,3256,3282,3285,3288,3291,912,752,3231,3237,3240,3243,3270,577,914,1999,1995,3163,3202,673,5,67,543,7,8,9,10,11,12,13,14,15,16,17,18,57,58,126,2843,19,20,21,1888,2846,2043,2069,151,168,170,172,174,176,633,1889,2850,2855,2856,1969,2346,2440,2649,2122,2414,1971,2305,2348,2420,2583,2585,199,535,1900,1901,1966,2124,2542,2754,2791,2400,2679,2544,2756,1939,1972,1976,1985,1989,1949,1980,4])). % 181.17/181.17 cnf(3305,plain, % 181.17/181.17 (E(f3(f13(f13(x33051)),x33051),f13(x33051))), % 181.17/181.17 inference(scs_inference,[],[947,2470,1062,3216,3221,3234,3261,3264,3267,3276,3279,626,544,575,3213,3228,3250,3253,3256,3282,3285,3288,3291,912,1221,752,3231,3237,3240,3243,3270,577,914,1999,1995,3163,3202,673,5,67,543,7,8,9,10,11,12,13,14,15,16,17,18,57,58,126,2843,19,20,21,1888,2846,2043,2069,151,168,170,172,174,176,633,1889,2850,2855,2856,1969,2346,2440,2649,2122,2414,1971,2305,2348,2420,2583,2585,199,535,1900,1901,1966,2124,2542,2754,2791,2400,2679,2544,2756,1939,1972,1976,1985,1989,1949,1980,4,38,42,53])). % 181.17/181.17 cnf(3319,plain, % 181.17/181.17 (~E(f13(f10(f13(f3(f13(a1),f13(a9))))),f13(a1))), % 181.17/181.17 inference(scs_inference,[],[921,947,2470,894,1062,3216,3221,3234,3261,3264,3267,3276,3279,626,544,3160,575,3213,3228,3250,3253,3256,3282,3285,3288,3291,912,1131,1221,752,3231,3237,3240,3243,3270,577,1210,914,1999,1995,3163,3202,673,5,67,543,7,8,9,10,11,12,13,14,15,16,17,18,57,58,126,2843,19,20,21,1888,2846,2043,2069,151,168,170,172,174,176,633,1889,2850,2855,2856,1969,2346,2440,2649,2122,2414,1971,2305,2348,2420,2583,2585,199,535,1900,1901,1966,2124,2542,2754,2791,2400,2679,2544,2756,1939,1972,1976,1985,1989,1949,1980,4,38,42,53,33,37,34,6,54,2,55,31])). % 181.17/181.17 cnf(3427,plain, % 181.17/181.17 (~P3(f12(f13(f13(x34271))),x34271)), % 181.17/181.17 inference(scs_inference,[],[1999,575,815,544,3319,55,2,54,6,34])). % 181.17/181.17 cnf(3429,plain, % 181.17/181.17 (P3(x34291,f3(f13(f13(x34291)),f12(f13(x34291))))), % 181.17/181.17 inference(scs_inference,[],[1999,709,575,815,544,3319,55,2,54,6,34,37])). % 181.17/181.17 cnf(3430,plain, % 181.17/181.17 (P2(x34301,f3(f13(x34301),f12(x34301)))), % 181.17/181.17 inference(rename_variables,[],[709])). % 181.17/181.17 cnf(3449,plain, % 181.17/181.17 (P3(x34491,f12(f10(f10(x34491))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3458,plain, % 181.17/181.17 (P3(x34581,f12(f10(f10(x34581))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3461,plain, % 181.17/181.17 (P3(x34611,f12(f10(f10(x34611))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3468,plain, % 181.17/181.17 (P3(x34681,f12(f10(f10(x34681))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3475,plain, % 181.17/181.17 (P3(x34751,f12(f10(f10(x34751))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3484,plain, % 181.17/181.17 (P3(x34841,f12(f10(f10(x34841))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3493,plain, % 181.17/181.17 (P3(x34931,f12(f10(f10(x34931))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3496,plain, % 181.17/181.17 (P3(x34961,f12(f10(f10(x34961))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3499,plain, % 181.17/181.17 (P3(x34991,f12(f10(f10(x34991))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3506,plain, % 181.17/181.17 (P3(x35061,f12(f10(f10(x35061))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3509,plain, % 181.17/181.17 (P3(x35091,f12(f10(f10(x35091))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3512,plain, % 181.17/181.17 (P3(x35121,f12(f10(f10(x35121))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3519,plain, % 181.17/181.17 (P3(x35191,f12(f10(f10(x35191))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3526,plain, % 181.17/181.17 (P3(x35261,f12(f10(f10(x35261))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3529,plain, % 181.17/181.17 (P3(x35291,f12(f10(f10(x35291))))), % 181.17/181.17 inference(rename_variables,[],[874])). % 181.17/181.17 cnf(3546,plain, % 181.17/181.17 (E(x35461,f3(f13(x35461),f12(x35461)))), % 181.17/181.17 inference(rename_variables,[],[673])). % 181.17/181.17 cnf(3547,plain, % 181.17/181.17 (~E(x35471,f13(f10(f3(f13(x35471),f12(x35471)))))), % 181.17/181.17 inference(scs_inference,[],[674,673,76,1999,560,709,3430,437,575,912,815,577,878,913,553,544,692,721,874,3449,3458,3461,3468,3475,3484,3493,3496,3499,3506,3509,3512,3519,3526,3529,3300,669,964,1692,3319,3225,1226,55,2,54,6,34,37,33,53,2850,2542,2043,2440,2586,1889,1954,5,2843,2346,1973,1976,2855,2649,1979,1980,1989,1939,2075,4,2846,1969,1891,1888,2071,1966,1983,1985,2420,2073,1900,1901,1971,1105,2348,1970,2427,1963,1949,1934,543,2544,2397,2069,1972,178,26,23])). % 181.17/181.17 cnf(3548,plain, % 181.17/181.17 (~P2(f13(f10(x35481)),x35481)), % 181.17/181.17 inference(rename_variables,[],[76])). % 181.17/181.17 cnf(3549,plain, % 181.17/181.17 (P3(x35491,f12(f13(f10(x35491))))), % 181.17/181.17 inference(scs_inference,[],[674,61,703,673,76,1999,560,709,3430,437,575,912,815,577,878,913,553,544,692,721,874,3449,3458,3461,3468,3475,3484,3493,3496,3499,3506,3509,3512,3519,3526,3529,3300,669,964,1692,3319,3225,1226,55,2,54,6,34,37,33,53,2850,2542,2043,2440,2586,1889,1954,5,2843,2346,1973,1976,2855,2649,1979,1980,1989,1939,2075,4,2846,1969,1891,1888,2071,1966,1983,1985,2420,2073,1900,1901,1971,1105,2348,1970,2427,1963,1949,1934,543,2544,2397,2069,1972,178,26,23,56])). % 181.17/181.17 cnf(3550,plain, % 181.17/181.17 (P3(x35501,f13(x35501))), % 181.17/181.17 inference(rename_variables,[],[61])). % 181.17/181.17 cnf(3557,plain, % 181.17/181.17 (E(x35571,f3(f13(x35571),f12(x35571)))), % 181.17/181.17 inference(rename_variables,[],[673])). % 181.17/181.17 cnf(3558,plain, % 181.17/181.17 (~E(f10(f13(f3(f13(x35581),f12(x35581)))),x35581)), % 181.17/181.17 inference(scs_inference,[],[619,674,61,3550,703,673,3546,3557,76,3548,100,1999,560,709,3430,437,575,678,912,815,577,878,913,553,544,692,721,874,3449,3458,3461,3468,3475,3484,3493,3496,3499,3506,3509,3512,3519,3526,3529,3300,669,964,1692,3319,3225,1226,55,2,54,6,34,37,33,53,2850,2542,2043,2440,2586,1889,1954,5,2843,2346,1973,1976,2855,2649,1979,1980,1989,1939,2075,4,2846,1969,1891,1888,2071,1966,1983,1985,2420,2073,1900,1901,1971,1105,2348,1970,2427,1963,1949,1934,543,2544,2397,2069,1972,178,26,23,56,24,25,22,3])). % 181.17/181.17 cnf(3593,plain, % 181.17/181.17 (E(f12(f10(a9)),f12(f10(f3(f13(a9),f13(a1)))))), % 181.17/181.17 inference(scs_inference,[],[964,781,55,2])). % 181.17/181.17 cnf(3605,plain, % 181.17/181.17 (~E(f13(f3(f13(f10(x36051)),f12(f10(x36051)))),x36051)), % 181.17/181.17 inference(scs_inference,[],[180,577,964,781,530,3558,124,1207,682,55,2,54,6,34,37,53,33,4])). % 181.17/181.17 cnf(3609,plain, % 181.17/181.17 (P3(x36091,f12(f13(f10(x36091))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3614,plain, % 181.17/181.17 (P3(x36141,f12(f13(f10(x36141))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3619,plain, % 181.17/181.17 (P3(x36191,f12(f13(f10(x36191))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3626,plain, % 181.17/181.17 (P3(x36261,f12(f13(f10(x36261))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3631,plain, % 181.17/181.17 (P3(x36311,f12(f13(f10(x36311))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3644,plain, % 181.17/181.17 (P3(x36441,f12(f13(f10(x36441))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3649,plain, % 181.17/181.17 (P3(x36491,f12(f13(f10(x36491))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3652,plain, % 181.17/181.17 (P3(x36521,f12(f13(f10(x36521))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3657,plain, % 181.17/181.17 (P3(x36571,f12(f13(f10(x36571))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3662,plain, % 181.17/181.17 (P3(x36621,f12(f13(f10(x36621))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3667,plain, % 181.17/181.17 (P3(x36671,f12(f13(f10(x36671))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3670,plain, % 181.17/181.17 (P3(x36701,f12(f13(f10(x36701))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3673,plain, % 181.17/181.17 (P3(x36731,f12(f13(f10(x36731))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3676,plain, % 181.17/181.17 (P3(x36761,f12(f13(f10(x36761))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3681,plain, % 181.17/181.17 (P3(x36811,f12(f13(f10(x36811))))), % 181.17/181.17 inference(rename_variables,[],[3549])). % 181.17/181.17 cnf(3686,plain, % 181.17/181.17 (P3(x36861,f3(f13(f13(x36861)),f12(f13(x36861))))), % 181.17/181.17 inference(rename_variables,[],[3429])). % 181.17/181.17 cnf(3689,plain, % 181.17/181.17 (P3(x36891,f3(f13(f13(x36891)),f12(f13(x36891))))), % 181.17/181.17 inference(rename_variables,[],[3429])). % 181.17/181.17 cnf(3697,plain, % 181.17/181.17 (P3(x36971,f3(f13(f13(x36971)),f12(f13(x36971))))), % 181.17/181.17 inference(rename_variables,[],[3429])). % 181.17/181.17 cnf(3700,plain, % 181.17/181.17 (P3(x37001,f3(f13(f13(x37001)),f12(f13(x37001))))), % 181.17/181.17 inference(rename_variables,[],[3429])). % 181.17/181.17 cnf(3705,plain, % 181.17/181.17 (P3(f13(x37051),f3(f13(f10(f10(x37051))),f12(f10(f10(x37051)))))), % 181.17/181.17 inference(scs_inference,[],[673,1062,1995,180,577,964,878,913,1692,781,3225,897,3429,3686,3689,3697,3700,3549,3609,3614,3619,3626,3631,3644,3649,3652,3657,3662,3667,3670,3673,3676,3681,1847,1094,1083,530,3558,124,1207,682,55,2,54,6,34,37,53,33,4,5,1939,1889,1954,2843,1973,2346,2071,1971,2075,1969,1963,2440,2043,2846,1989,1976,2069,1972,1900,2649,1979,2348,1985,1888,1901,1966,1949,1934,543,1983,2073,2400,2679,1970,178,2676,2678,2305,26])). % 181.17/181.17 cnf(3709,plain, % 181.17/181.17 (P3(x37091,f12(f10(f13(x37091))))), % 181.17/181.17 inference(scs_inference,[],[61,703,673,76,1062,1995,180,2101,577,964,878,913,1692,781,3225,897,3429,3686,3689,3697,3700,3549,3609,3614,3619,3626,3631,3644,3649,3652,3657,3662,3667,3670,3673,3676,3681,1847,1094,1083,530,3558,124,1207,682,55,2,54,6,34,37,53,33,4,5,1939,1889,1954,2843,1973,2346,2071,1971,2075,1969,1963,2440,2043,2846,1989,1976,2069,1972,1900,2649,1979,2348,1985,1888,1901,1966,1949,1934,543,1983,2073,2400,2679,1970,178,2676,2678,2305,26,23,56])). % 181.17/181.17 cnf(3762,plain, % 181.17/181.17 (~E(f10(f13(f10(f12(x37621)))),x37621)), % 181.17/181.17 inference(scs_inference,[],[133,878,914,808,1248,3547,584,1194,655,55,2,54,6,34,37,53,33,5])). % 181.17/181.17 cnf(3766,plain, % 181.17/181.17 (~E(x37661,f13(f10(f12(f10(x37661)))))), % 181.17/181.17 inference(scs_inference,[],[133,878,914,808,1248,3709,3547,1250,584,1194,655,55,2,54,6,34,37,53,33,5,1889,4])). % 181.17/181.17 cnf(3769,plain, % 181.17/181.17 (P3(x37691,f12(f10(f13(x37691))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3774,plain, % 181.17/181.17 (P3(x37741,f12(f10(f13(x37741))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3777,plain, % 181.17/181.17 (P3(x37771,f12(f10(f13(x37771))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3788,plain, % 181.17/181.17 (P3(x37881,f12(f10(f13(x37881))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3791,plain, % 181.17/181.17 (P3(x37911,f12(f10(f13(x37911))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3794,plain, % 181.17/181.17 (P3(x37941,f12(f10(f13(x37941))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3796,plain, % 181.17/181.17 (~P3(f13(f10(f12(f10(x37961)))),f10(f3(f13(x37961),f12(x37961))))), % 181.17/181.17 inference(scs_inference,[],[133,878,914,874,3300,1094,1083,808,1248,3709,3769,3774,3777,3788,3791,3181,3547,1250,584,1194,655,55,2,54,6,34,37,53,33,5,1889,4,1954,2075,1939,1971,2843,1963,2649,2069,1973,1976,1985,543])). % 181.17/181.17 cnf(3803,plain, % 181.17/181.17 (P3(x38031,f12(f10(f13(x38031))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3806,plain, % 181.17/181.17 (P3(x38061,f12(f10(f13(x38061))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3809,plain, % 181.17/181.17 (P3(x38091,f12(f10(f13(x38091))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3812,plain, % 181.17/181.17 (P3(x38121,f12(f10(f13(x38121))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3821,plain, % 181.17/181.17 (P3(x38211,f12(f10(f13(x38211))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3824,plain, % 181.17/181.17 (P3(x38241,f12(f10(f13(x38241))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3827,plain, % 181.17/181.17 (P3(x38271,f12(f10(f13(x38271))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3832,plain, % 181.17/181.17 (P3(x38321,f12(f10(f13(x38321))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3835,plain, % 181.17/181.17 (P3(x38351,f12(f10(f13(x38351))))), % 181.17/181.17 inference(rename_variables,[],[3709])). % 181.17/181.17 cnf(3842,plain, % 181.17/181.17 (P3(f3(f13(x38421),f12(x38421)),f3(f13(f13(x38421)),f12(f13(x38421))))), % 181.17/181.17 inference(scs_inference,[],[673,578,1692,133,878,914,874,3300,1094,1083,808,3429,1248,3709,3769,3774,3777,3788,3791,3794,3803,3806,3809,3812,3821,3824,3827,3832,3835,3181,3593,3547,1250,584,1194,655,55,2,54,6,34,37,53,33,5,1889,4,1954,2075,1939,1971,2843,1963,2649,2069,1973,1976,1985,543,2071,2440,1969,1979,1900,1901,1888,2846,1989,1972,1934,1949,2348,1970,1983,178,1966,26])). % 181.17/181.17 cnf(3843,plain, % 181.17/181.17 (E(x38431,f3(f13(x38431),f12(x38431)))), % 181.17/181.17 inference(rename_variables,[],[673])). % 181.17/181.17 cnf(3846,plain, % 181.17/181.17 (P3(f6(f10(a2),a2),f12(f10(a2)))), % 181.17/181.17 inference(scs_inference,[],[673,76,578,2353,1692,133,878,2018,914,2470,874,3300,1094,1083,808,3429,1248,3709,3769,3774,3777,3788,3791,3794,3803,3806,3809,3812,3821,3824,3827,3832,3835,3181,3593,3547,1250,584,1194,655,55,2,54,6,34,37,53,33,5,1889,4,1954,2075,1939,1971,2843,1963,2649,2069,1973,1976,1985,543,2071,2440,1969,1979,1900,1901,1888,2846,1989,1972,1934,1949,2348,1970,1983,178,1966,26,23,56])). % 181.17/181.17 cnf(3849,plain, % 181.17/181.17 (E(x38491,f3(f13(x38491),f12(x38491)))), % 181.17/181.17 inference(rename_variables,[],[673])). % 181.17/181.17 cnf(3873,plain, % 181.17/181.17 (E(f3(f3(f13(x38731),f12(x38731)),x38732),f3(x38731,x38732))), % 181.17/181.17 inference(scs_inference,[],[30,619,28,61,673,3843,3849,179,76,100,1995,578,618,2353,1692,133,878,2018,914,2470,874,3300,1094,1083,894,808,895,3429,3305,1847,1248,3709,3769,3774,3777,3788,3791,3794,3803,3806,3809,3812,3821,3824,3827,3832,3835,700,657,1087,3181,3593,3547,1250,584,1194,655,55,2,54,6,34,37,53,33,5,1889,4,1954,2075,1939,1971,2843,1963,2649,2069,1973,1976,1985,543,2071,2440,1969,1979,1900,1901,1888,2846,1989,1972,1934,1949,2348,1970,1983,178,1966,26,23,56,24,25,22,3,36,32,31,35,41,1704,1779])). % 181.17/181.17 cnf(3875,plain, % 181.17/181.17 (E(f12(f13(f3(f13(x38751),f12(x38751)))),f12(f13(x38751)))), % 181.17/181.17 inference(scs_inference,[],[30,619,28,61,673,3843,3849,179,76,100,1995,578,618,2353,1692,133,878,2018,914,2470,874,3300,1094,1083,894,808,895,3429,3305,1847,1248,3709,3769,3774,3777,3788,3791,3794,3803,3806,3809,3812,3821,3824,3827,3832,3835,700,657,1087,3181,3593,3547,1250,584,1194,655,55,2,54,6,34,37,53,33,5,1889,4,1954,2075,1939,1971,2843,1963,2649,2069,1973,1976,1985,543,2071,2440,1969,1979,1900,1901,1888,2846,1989,1972,1934,1949,2348,1970,1983,178,1966,26,23,56,24,25,22,3,36,32,31,35,41,1704,1779,1837])). % 181.17/181.17 cnf(3898,plain, % 181.17/181.17 (~P3(f12(f10(f10(x38981))),x38981)), % 181.17/181.17 inference(scs_inference,[],[874,3300,811,3605,3427,55,2,54,6,34])). % 181.17/181.17 cnf(3906,plain, % 181.17/181.17 (~E(x39061,f10(f10(f10(f12(x39061)))))), % 181.17/181.17 inference(scs_inference,[],[435,874,3300,811,3605,3162,3427,539,697,55,2,54,6,34,37,53,33,5])). % 181.17/181.17 cnf(3932,plain, % 181.17/181.17 (P2(f13(x39321),f7(f10(f13(x39321)),f12(f10(f13(x39321))),x39321))), % 181.17/181.17 inference(scs_inference,[],[435,1083,874,3300,3709,811,3181,3846,3842,1116,1819,3605,3162,3762,3427,539,697,55,2,54,6,34,37,53,33,5,4,1889,2075,2071,1963,2440,2843,2069,543,2043,2846,2649,1888])). % 181.17/181.17 cnf(3939,plain, % 181.17/181.17 (E(f12(f13(f3(f13(x39391),f12(x39391)))),f12(f13(x39391)))), % 181.17/181.17 inference(rename_variables,[],[3875])). % 181.17/181.17 cnf(3942,plain, % 181.17/181.17 (E(f12(f13(f3(f13(x39421),f12(x39421)))),f12(f13(x39421)))), % 181.17/181.17 inference(rename_variables,[],[3875])). % 181.17/181.17 cnf(3947,plain, % 181.17/181.17 (P3(f8(f10(a2),a2),f3(f13(f10(a2)),f12(f10(a2))))), % 181.17/181.17 inference(scs_inference,[],[673,2353,435,1083,874,3300,3709,811,3181,3846,3842,3875,3939,3942,1116,1819,3605,3162,3762,3427,539,697,55,2,54,6,34,37,53,33,5,4,1889,2075,2071,1963,2440,2843,2069,543,2043,2846,2649,1888,178,2073,2754,2756,2745,26])). % 181.17/181.17 cnf(3948,plain, % 181.17/181.17 (E(x39481,f3(f13(x39481),f12(x39481)))), % 181.17/181.17 inference(rename_variables,[],[673])). % 181.17/181.17 cnf(3955,plain, % 181.17/181.17 (E(x39551,f3(f13(x39551),f12(x39551)))), % 181.17/181.17 inference(rename_variables,[],[673])). % 181.17/181.17 cnf(3960,plain, % 181.17/181.17 (~E(f10(f13(f10(f3(f13(a9),f13(a1))))),f10(a9))), % 181.17/181.17 inference(scs_inference,[],[61,673,3948,3955,76,100,2353,912,575,435,1083,728,874,3300,895,3709,811,2027,3181,3846,3842,3873,3875,3939,3942,1116,1819,3605,3162,3762,3427,539,697,55,2,54,6,34,37,53,33,5,4,1889,2075,2071,1963,2440,2843,2069,543,2043,2846,2649,1888,178,2073,2754,2756,2745,26,23,56,24,25,22,3])). % 181.17/181.17 cnf(3991,plain, % 181.17/181.17 (~P2(f13(f10(f12(f10(x39911)))),f3(f13(x39911),f12(x39911)))), % 181.17/181.17 inference(scs_inference,[],[1094,831,3796,55,2,54])). % 181.17/181.17 cnf(4012,plain, % 181.17/181.17 (P2(f13(f6(f10(a2),a2)),f7(f10(a2),f12(f10(a2)),f6(f10(a2),a2)))), % 181.17/181.17 inference(scs_inference,[],[553,3709,1094,831,3846,1116,3947,941,3960,1254,3796,1188,688,55,2,54,6,34,37,53,33,4,2075,2440,1963,2843,1888])). % 181.17/181.17 cnf(4030,plain, % 181.17/181.17 (P3(f3(f13(x40301),f12(x40301)),f3(f13(f10(x40301)),f12(f10(x40301))))), % 181.17/181.17 inference(scs_inference,[],[673,1095,3300,553,3709,1094,831,3846,1116,1819,3947,941,3960,1254,3796,1188,688,55,2,54,6,34,37,53,33,4,2075,2440,1963,2843,1888,543,178,2846,2346,2542,2348,2791,2544,26])). % 181.17/181.17 cnf(4102,plain, % 181.17/181.17 (~P3(f13(f10(f12(f10(a9)))),f10(f3(f13(a9),f13(a1))))), % 181.17/181.17 inference(scs_inference,[],[398,3305,3846,1116,941,834,3593,3549,4030,943,3766,3906,3898,4012,3991,55,2,54,6,34,37,53,33,4,2075,2440,1963,2843,2846,178,543])). % 181.17/181.17 cnf(4159,plain, % 181.17/181.17 (E(f10(f7(a9,x41591,x41592)),f10(f7(f3(f13(a9),f13(a1)),x41591,x41592)))), % 181.17/181.17 inference(scs_inference,[],[941,947,55,2])). % 181.17/181.17 cnf(4234,plain, % 181.17/181.17 (E(f10(f7(x42341,x42342,a9)),f10(f7(x42341,x42342,f3(f13(a9),f13(a1)))))), % 181.17/181.17 inference(scs_inference,[],[943,1157,55,2])). % 181.17/181.17 cnf(4306,plain, % 181.17/181.17 (E(f10(f7(x43061,a9,x43062)),f10(f7(x43061,f3(f13(a9),f13(a1)),x43062)))), % 181.17/181.17 inference(scs_inference,[],[986,1183,55,2])). % 181.17/181.17 cnf(4467,plain, % 181.17/181.17 (P2(f8(f10(a2),a2),f3(f13(a2),f12(a2)))), % 181.17/181.17 inference(scs_inference,[],[619,673,3709,514,4159,700,745,4234,2356,4030,4306,3705,4102,3932,698,55,2,54,34,37,53,33,2075,2843,2440,2846,25,24])). % 181.17/181.17 cnf(5920,plain, % 181.17/181.17 (~P3(f6(f10(a2),a2),f3(f13(a2),f12(a2)))), % 181.17/181.17 inference(scs_inference,[],[28,2006,2467,930,674,1995,61,36,37,33,35,26])). % 181.17/181.17 cnf(5962,plain, % 181.17/181.17 ($false), % 181.17/181.17 inference(scs_inference,[],[28,1275,2354,2029,4467,5920,2470,936,1995,464,36,37,35,32,2,39]), % 181.17/181.17 ['proof']). % 181.17/181.17 % SZS output end Proof % 181.17/181.17 % Total time :180.480000s %------------------------------------------------------------------------------