%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU129+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n021.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:11 EDT 2024 % Result : Theorem 180.85s 180.80s % Output : CNFRefutation 181.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU129+1 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 13:45:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.59 start to proof:theBenchmark % 180.81/180.78 %------------------------------------------- % 180.81/180.78 % File :CSE---1.7 % 180.81/180.78 % Problem :theBenchmark % 180.81/180.78 % Transform :cnf % 180.81/180.78 % Format :tptp:raw % 180.81/180.78 % Command :java -jar mcs_scs.jar %d %s % 180.81/180.78 % 180.81/180.78 % Result :Theorem 180.140000s % 180.81/180.78 % Output :CNFRefutation 180.140000s % 180.81/180.78 %------------------------------------------- % 180.81/180.80 %------------------------------------------------------------------------------ % 180.81/180.80 % File : SEU129+1 : TPTP v8.2.0. Released v3.3.0. % 180.81/180.80 % Domain : Set theory % 180.81/180.80 % Problem : MPTP bushy problem t26_xboole_1 % 180.81/180.80 % Version : [Urb07] axioms : Especial. % 180.81/180.80 % English : % 180.81/180.80 % 180.81/180.80 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 180.81/180.80 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 180.81/180.80 % Source : [Urb07] % 180.81/180.80 % Names : bushy-t26_xboole_1 [Urb07] % 180.81/180.80 % 180.81/180.80 % Status : Theorem % 180.81/180.80 % Rating : 0.22 v8.2.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.20 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.13 v7.0.0, 0.17 v6.4.0, 0.23 v6.3.0, 0.12 v6.2.0, 0.28 v6.1.0, 0.40 v6.0.0, 0.26 v5.5.0, 0.37 v5.4.0, 0.43 v5.3.0, 0.48 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.29 v4.1.0, 0.30 v4.0.0, 0.29 v3.7.0, 0.30 v3.5.0, 0.26 v3.4.0, 0.32 v3.3.0 % 180.81/180.80 % Syntax : Number of formulae : 16 ( 9 unt; 0 def) % 180.81/180.80 % Number of atoms : 27 ( 6 equ) % 180.81/180.80 % Maximal formula atoms : 4 ( 1 avg) % 180.81/180.80 % Number of connectives : 16 ( 5 ~; 0 |; 4 &) % 180.81/180.80 % ( 3 <=>; 4 =>; 0 <=; 0 <~>) % 180.81/180.80 % Maximal formula depth : 8 ( 4 avg) % 180.81/180.80 % Maximal term depth : 2 ( 1 avg) % 180.81/180.80 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 180.81/180.80 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 180.81/180.80 % Number of variables : 26 ( 24 !; 2 ?) % 180.81/180.80 % SPC : FOF_THM_RFO_SEQ % 180.81/180.80 % 180.81/180.80 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 180.81/180.80 % library, www.mizar.org % 180.81/180.80 %------------------------------------------------------------------------------ % 180.81/180.80 fof(antisymmetry_r2_hidden,axiom, % 180.81/180.80 ! [A,B] : % 180.81/180.80 ( in(A,B) % 180.81/180.80 => ~ in(B,A) ) ). % 180.81/180.80 % 180.81/180.80 fof(commutativity_k3_xboole_0,axiom, % 180.81/180.80 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 180.81/180.80 % 180.81/180.80 fof(d3_tarski,axiom, % 180.81/180.80 ! [A,B] : % 180.81/180.80 ( subset(A,B) % 180.81/180.80 <=> ! [C] : % 180.85/180.80 ( in(C,A) % 180.85/180.80 => in(C,B) ) ) ). % 180.85/180.80 % 180.85/180.80 fof(d3_xboole_0,axiom, % 180.85/180.80 ! [A,B,C] : % 180.85/180.80 ( C = set_intersection2(A,B) % 180.85/180.80 <=> ! [D] : % 180.85/180.80 ( in(D,C) % 180.85/180.80 <=> ( in(D,A) % 180.85/180.80 & in(D,B) ) ) ) ). % 180.85/180.80 % 180.85/180.80 fof(dt_k1_xboole_0,axiom, % 180.85/180.80 $true ). % 180.85/180.80 % 180.85/180.80 fof(dt_k3_xboole_0,axiom, % 180.85/180.80 $true ). % 180.85/180.80 % 180.85/180.80 fof(fc1_xboole_0,axiom, % 180.85/180.80 empty(empty_set) ). % 180.85/180.80 % 180.85/180.80 fof(idempotence_k3_xboole_0,axiom, % 180.85/180.80 ! [A,B] : set_intersection2(A,A) = A ). % 180.85/180.80 % 180.85/180.80 fof(rc1_xboole_0,axiom, % 180.85/180.80 ? [A] : empty(A) ). % 180.85/180.80 % 180.85/180.80 fof(rc2_xboole_0,axiom, % 180.85/180.80 ? [A] : ~ empty(A) ). % 180.85/180.80 % 180.85/180.80 fof(reflexivity_r1_tarski,axiom, % 180.85/180.80 ! [A,B] : subset(A,A) ). % 180.85/180.80 % 180.85/180.80 fof(t26_xboole_1,conjecture, % 180.85/180.80 ! [A,B,C] : % 180.85/180.80 ( subset(A,B) % 180.85/180.80 => subset(set_intersection2(A,C),set_intersection2(B,C)) ) ). % 180.85/180.80 % 180.85/180.80 fof(t2_boole,axiom, % 180.85/180.80 ! [A] : set_intersection2(A,empty_set) = empty_set ). % 180.85/180.80 % 180.85/180.80 fof(t6_boole,axiom, % 180.85/180.80 ! [A] : % 180.85/180.80 ( empty(A) % 180.85/180.80 => A = empty_set ) ). % 180.85/180.80 % 180.85/180.80 fof(t7_boole,axiom, % 180.85/180.80 ! [A,B] : % 180.85/180.80 ~ ( in(A,B) % 180.85/180.80 & empty(B) ) ). % 180.85/180.80 % 180.85/180.80 fof(t8_boole,axiom, % 180.85/180.80 ! [A,B] : % 180.85/180.80 ~ ( empty(A) % 180.85/180.80 & A != B % 180.85/180.80 & empty(B) ) ). % 180.85/180.80 % 180.85/180.80 %------------------------------------------------------------------------------ % 180.85/180.80 %------------------------------------------- % 180.85/180.80 % Proof found % 180.85/180.80 % SZS status Theorem for theBenchmark % 180.85/180.80 % SZS output start Proof % 180.85/180.82 %ClaNum:37(EqnAxiom:15) % 180.85/180.82 %VarNum:99(SingletonVarNum:40) % 180.85/180.82 %MaxLitNum:4 % 180.85/180.82 %MaxfuncDepth:1 % 180.85/180.82 %SharedTerms:13 % 180.85/180.82 %goalClause: 18 24 % 180.85/180.82 %singleGoalClaCount:2 % 180.85/180.82 [16]P1(a1) % 180.85/180.82 [17]P1(a2) % 180.85/180.82 [18]P2(a5,a7) % 180.85/180.82 [23]~P1(a6) % 180.85/180.82 [24]~P2(f8(a5,a9),f8(a7,a9)) % 180.85/180.82 [20]P2(x201,x201) % 180.85/180.82 [19]E(f8(x191,a1),a1) % 180.85/180.82 [21]E(f8(x211,x211),x211) % 180.85/180.82 [22]E(f8(x221,x222),f8(x222,x221)) % 180.85/180.82 [25]~P1(x251)+E(x251,a1) % 180.85/180.82 [27]~P1(x271)+~P3(x272,x271) % 180.85/180.82 [28]~P3(x282,x281)+~P3(x281,x282) % 180.85/180.82 [29]P2(x291,x292)+P3(f3(x291,x292),x291) % 180.85/180.82 [33]P2(x331,x332)+~P3(f3(x331,x332),x332) % 180.85/180.82 [26]~P1(x262)+~P1(x261)+E(x261,x262) % 180.85/180.82 [30]~P2(x303,x302)+P3(x301,x302)+~P3(x301,x303) % 180.85/180.82 [35]P3(f4(x352,x353,x351),x351)+P3(f4(x352,x353,x351),x353)+E(x351,f8(x352,x353)) % 180.85/180.82 [36]P3(f4(x362,x363,x361),x361)+P3(f4(x362,x363,x361),x362)+E(x361,f8(x362,x363)) % 180.85/180.82 [31]~P3(x311,x313)+P3(x311,x312)+~E(x313,f8(x314,x312)) % 180.85/180.82 [32]~P3(x321,x323)+P3(x321,x322)+~E(x323,f8(x322,x324)) % 180.85/180.82 [37]~P3(f4(x372,x373,x371),x371)+~P3(f4(x372,x373,x371),x373)+~P3(f4(x372,x373,x371),x372)+E(x371,f8(x372,x373)) % 180.85/180.82 [34]~P3(x341,x344)+~P3(x341,x343)+P3(x341,x342)+~E(x342,f8(x343,x344)) % 180.85/180.82 %EqnAxiom % 180.85/180.82 [1]E(x11,x11) % 180.85/180.82 [2]E(x22,x21)+~E(x21,x22) % 180.85/180.82 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 180.85/180.82 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 180.85/180.82 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 180.85/180.82 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 180.85/180.82 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 180.85/180.82 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 180.85/180.82 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 180.85/180.82 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 180.85/180.82 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 180.85/180.82 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 180.85/180.82 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 180.85/180.82 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 180.85/180.82 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 180.85/180.82 % 180.85/180.82 %------------------------------------------- % 180.85/180.85 cnf(38,plain, % 180.85/180.85 (~P3(x381,f8(x382,x383))+P3(x381,x383)), % 180.85/180.85 inference(equality_inference,[],[31])). % 180.85/180.85 cnf(39,plain, % 180.85/180.85 (~P3(x391,f8(x392,x393))+P3(x391,x392)), % 180.85/180.85 inference(equality_inference,[],[32])). % 180.85/180.85 cnf(40,plain, % 180.85/180.85 (~P3(x401,x402)+~P3(x401,x403)+P3(x401,f8(x403,x402))), % 180.85/180.85 inference(equality_inference,[],[34])). % 180.85/180.85 cnf(41,plain, % 180.85/180.85 (~P3(x411,a1)), % 180.85/180.85 inference(scs_inference,[],[16,27])). % 180.85/180.85 cnf(43,plain, % 180.85/180.85 (~P3(x431,f8(x432,a1))), % 180.85/180.85 inference(scs_inference,[],[16,27,38])). % 180.85/180.85 cnf(45,plain, % 180.85/180.85 (~P3(x451,f8(a1,x452))), % 180.85/180.85 inference(scs_inference,[],[16,27,38,39])). % 180.85/180.85 cnf(47,plain, % 180.85/180.85 (E(x471,f8(x471,x471))), % 180.85/180.85 inference(scs_inference,[],[21,16,27,38,39,2])). % 180.85/180.85 cnf(48,plain, % 180.85/180.85 (P2(f8(a5,a5),a7)), % 180.85/180.85 inference(scs_inference,[],[18,21,16,27,38,39,2,14])). % 180.85/180.85 cnf(49,plain, % 180.85/180.85 (~E(f8(a5,a9),f8(a7,a9))), % 180.85/180.85 inference(scs_inference,[],[18,24,20,21,16,27,38,39,2,14,15])). % 180.85/180.85 cnf(51,plain, % 180.85/180.85 (~E(f8(a5,a9),f8(a9,a7))), % 180.85/180.85 inference(scs_inference,[],[18,24,20,21,22,16,27,38,39,2,14,15,3])). % 180.85/180.85 cnf(53,plain, % 180.85/180.85 (P2(a1,x531)), % 180.85/180.85 inference(scs_inference,[],[18,24,20,21,22,16,27,38,39,2,14,15,3,29])). % 180.85/180.85 cnf(55,plain, % 180.85/180.85 (~E(a5,a7)), % 180.85/180.85 inference(scs_inference,[],[18,24,20,21,22,16,27,38,39,2,14,15,3,29,4])). % 180.85/180.85 cnf(64,plain, % 180.85/180.85 (~P3(x641,f8(f8(x642,a1),x643))), % 180.85/180.85 inference(scs_inference,[],[43,39])). % 180.85/180.85 cnf(66,plain, % 180.85/180.85 (~P3(x661,a2)), % 180.85/180.85 inference(scs_inference,[],[43,17,39,27])). % 180.85/180.85 cnf(68,plain, % 180.85/180.85 (P2(f8(x681,a1),x682)), % 180.85/180.85 inference(scs_inference,[],[43,17,39,27,29])). % 180.85/180.85 cnf(69,plain, % 180.85/180.85 (~P3(x691,f8(x692,a1))), % 180.85/180.85 inference(rename_variables,[],[43])). % 180.85/180.85 cnf(71,plain, % 180.85/180.85 (~P3(x711,f8(x712,f8(x713,a1)))), % 180.85/180.85 inference(scs_inference,[],[43,69,17,39,27,29,38])). % 180.85/180.85 cnf(73,plain, % 180.85/180.85 (E(a1,f8(x731,a1))), % 180.85/180.85 inference(scs_inference,[],[43,69,19,17,39,27,29,38,2])). % 180.85/180.85 cnf(75,plain, % 180.85/180.85 (E(x751,f8(x751,x751))), % 180.85/180.85 inference(rename_variables,[],[47])). % 180.85/180.85 cnf(76,plain, % 180.85/180.85 (E(f8(x761,a1),f8(a1,a1))), % 180.85/180.85 inference(scs_inference,[],[47,75,43,69,19,16,17,39,27,29,38,2,11,3])). % 180.85/180.85 cnf(77,plain, % 180.85/180.85 (E(x771,f8(x771,x771))), % 180.85/180.85 inference(rename_variables,[],[47])). % 180.85/180.85 cnf(78,plain, % 180.85/180.85 (P2(a5,f8(a7,a7))), % 180.85/180.85 inference(scs_inference,[],[18,47,75,77,43,69,19,16,17,39,27,29,38,2,11,3,15])). % 180.85/180.85 cnf(79,plain, % 180.85/180.85 (E(x791,f8(x791,x791))), % 180.85/180.85 inference(rename_variables,[],[47])). % 180.85/180.85 cnf(80,plain, % 180.85/180.85 (~E(a1,f8(a5,a9))), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,43,69,19,16,17,39,27,29,38,2,11,3,15,14])). % 180.85/180.85 cnf(84,plain, % 180.85/180.85 (P3(f4(a5,a9,a1),a5)), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,43,69,41,55,19,16,17,39,27,29,38,2,11,3,15,14,26,36])). % 180.85/180.85 cnf(85,plain, % 180.85/180.85 (~P3(x851,a1)), % 180.85/180.85 inference(rename_variables,[],[41])). % 180.85/180.85 cnf(87,plain, % 180.85/180.85 (P3(f8(f4(a5,a9,a1),f4(a5,a9,a1)),a5)), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,79,43,69,41,55,19,16,17,39,27,29,38,2,11,3,15,14,26,36,12])). % 180.85/180.85 cnf(89,plain, % 180.85/180.85 (P3(f4(a5,a9,a1),a9)), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,79,43,69,41,85,55,19,16,17,39,27,29,38,2,11,3,15,14,26,36,12,35])). % 180.85/180.85 cnf(92,plain, % 180.85/180.85 (P3(f4(a5,a9,a1),f8(f8(a5,a5),f8(a5,a5)))), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,79,43,69,41,85,55,19,21,16,17,39,27,29,38,2,11,3,15,14,26,36,12,35,34])). % 180.85/180.85 cnf(95,plain, % 180.85/180.85 (~P3(a5,f4(a5,a9,a1))), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,79,43,69,41,85,55,19,21,16,17,39,27,29,38,2,11,3,15,14,26,36,12,35,34,28])). % 180.85/180.85 cnf(97,plain, % 180.85/180.85 (P3(f4(a5,a9,a1),a7)), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,79,43,69,41,85,55,19,21,16,17,39,27,29,38,2,11,3,15,14,26,36,12,35,34,28,30])). % 180.85/180.85 cnf(99,plain, % 180.85/180.85 (~E(a5,f8(x991,a1))), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,79,43,69,41,85,55,19,21,16,17,39,27,29,38,2,11,3,15,14,26,36,12,35,34,28,30,13])). % 180.85/180.85 cnf(101,plain, % 180.85/180.85 (P3(f4(a5,a9,a1),f8(a5,a5))), % 180.85/180.85 inference(scs_inference,[],[18,24,53,47,75,77,79,43,69,41,85,55,19,21,22,16,17,39,27,29,38,2,11,3,15,14,26,36,12,35,34,28,30,13,31])). % 180.85/180.85 cnf(105,plain, % 180.85/180.85 (~P3(a7,f4(a5,a9,a1))), % 180.85/180.85 inference(scs_inference,[],[97,28])). % 180.85/180.85 cnf(107,plain, % 180.85/180.85 (~P3(x1071,f8(f8(a1,x1072),x1073))), % 180.85/180.85 inference(scs_inference,[],[97,45,28,39])). % 180.85/180.85 cnf(109,plain, % 180.85/180.85 (P2(f8(a1,x1091),x1092)), % 180.85/180.85 inference(scs_inference,[],[97,45,28,39,29])). % 180.85/180.85 cnf(110,plain, % 180.85/180.85 (~P3(x1101,f8(a1,x1102))), % 180.85/180.85 inference(rename_variables,[],[45])). % 180.85/180.85 cnf(112,plain, % 180.85/180.85 (~P3(x1121,f8(x1122,f8(a1,x1123)))), % 180.85/180.85 inference(scs_inference,[],[97,45,110,28,39,29,38])). % 180.85/180.85 cnf(114,plain, % 180.85/180.85 (E(f8(a1,a1),f8(x1141,a1))), % 180.85/180.85 inference(scs_inference,[],[97,45,110,76,28,39,29,38,2])). % 180.85/180.85 cnf(115,plain, % 180.85/180.85 (~E(a7,f8(f8(x1151,a1),x1152))), % 180.85/180.85 inference(scs_inference,[],[97,64,45,110,76,28,39,29,38,2,13])). % 180.85/180.85 cnf(119,plain, % 180.85/180.85 (P3(f8(f4(a5,a9,a1),f4(a5,a9,a1)),a7)), % 180.85/180.85 inference(scs_inference,[],[18,97,80,64,45,110,76,87,16,28,39,29,38,2,13,26,30])). % 180.85/180.85 cnf(122,plain, % 180.85/180.85 (E(a1,f8(x1221,a1))), % 180.85/180.85 inference(rename_variables,[],[73])). % 180.85/180.85 cnf(123,plain, % 180.85/180.85 (P3(f4(x1231,a1,a5),a5)), % 180.85/180.85 inference(scs_inference,[],[18,97,80,64,45,110,76,87,73,99,41,16,28,39,29,38,2,13,26,30,3,35])). % 180.85/180.85 cnf(126,plain, % 180.85/180.85 (P3(f8(f4(a5,a9,a1),f4(a5,a9,a1)),f8(a5,a5))), % 180.85/180.85 inference(scs_inference,[],[18,97,80,101,64,45,110,76,87,73,99,47,41,16,28,39,29,38,2,13,26,30,3,35,12])). % 180.85/180.85 cnf(127,plain, % 180.85/180.85 (E(x1271,f8(x1271,x1271))), % 180.85/180.85 inference(rename_variables,[],[47])). % 180.85/180.85 cnf(128,plain, % 180.85/180.85 (P1(f8(x1281,a1))), % 180.85/180.85 inference(scs_inference,[],[18,97,80,101,64,45,110,76,87,73,122,99,47,41,16,28,39,29,38,2,13,26,30,3,35,12,11])). % 180.85/180.85 cnf(129,plain, % 180.85/180.85 (P2(f8(a5,a5),f8(a7,a7))), % 180.85/180.85 inference(scs_inference,[],[18,48,97,80,101,64,45,110,76,87,73,122,99,47,127,41,16,28,39,29,38,2,13,26,30,3,35,12,11,15])). % 180.85/180.85 cnf(131,plain, % 180.85/180.85 (~E(f8(x1311,a1),f8(a5,a9))), % 180.85/180.85 inference(scs_inference,[],[18,24,68,48,97,80,101,64,45,110,76,87,73,122,99,47,127,41,16,28,39,29,38,2,13,26,30,3,35,12,11,15,14])). % 180.85/180.85 cnf(136,plain, % 180.85/180.85 (~P1(a5)), % 180.85/180.85 inference(scs_inference,[],[18,24,68,48,97,80,22,101,64,45,110,76,87,73,122,99,47,127,41,16,28,39,29,38,2,13,26,30,3,35,12,11,15,14,34,25])). % 180.85/180.85 cnf(138,plain, % 180.85/180.85 (~E(a1,a9)), % 180.85/180.85 inference(scs_inference,[],[18,24,68,48,97,80,22,101,64,45,110,76,87,73,122,99,47,127,41,16,28,39,29,38,2,13,26,30,3,35,12,11,15,14,34,25,5])). % 180.85/180.85 cnf(144,plain, % 180.85/180.85 (P2(a2,x1441)), % 180.85/180.85 inference(scs_inference,[],[119,66,28,29])). % 180.85/180.85 cnf(145,plain, % 180.85/180.85 (~P3(x1451,a2)), % 180.85/180.85 inference(rename_variables,[],[66])). % 180.85/180.85 cnf(147,plain, % 180.85/180.85 (~P3(x1471,f8(a2,x1472))), % 180.85/180.85 inference(scs_inference,[],[119,66,145,28,29,39])). % 180.85/180.85 cnf(149,plain, % 180.85/180.85 (~P3(x1491,f8(x1492,a2))), % 180.85/180.85 inference(scs_inference,[],[119,66,145,28,29,39,38])). % 180.85/180.85 cnf(151,plain, % 180.85/180.85 (~P1(a7)), % 180.85/180.85 inference(scs_inference,[],[119,66,145,115,128,28,29,39,38,26])). % 180.85/180.85 cnf(153,plain, % 180.85/180.85 (P1(f8(x1531,a1))), % 180.85/180.85 inference(rename_variables,[],[128])). % 180.85/180.85 cnf(155,plain, % 180.85/180.85 (P3(f4(a5,a9,f8(x1551,a1)),a5)), % 180.85/180.85 inference(scs_inference,[],[119,131,43,66,145,115,128,28,29,39,38,26,36])). % 180.85/180.85 cnf(156,plain, % 180.85/180.85 (~E(f8(x1561,a1),f8(a5,a9))), % 180.85/180.85 inference(rename_variables,[],[131])). % 180.85/180.85 cnf(157,plain, % 180.85/180.85 (~P3(x1571,f8(x1572,a1))), % 180.85/180.85 inference(rename_variables,[],[43])). % 180.85/180.85 cnf(159,plain, % 180.85/180.85 (P3(f8(f4(a5,a9,a1),f4(a5,a9,a1)),f8(a7,a7))), % 180.85/180.85 inference(scs_inference,[],[129,119,131,43,126,66,145,115,128,28,29,39,38,26,36,30])). % 180.85/180.85 cnf(161,plain, % 180.85/180.85 (~E(a7,f8(x1611,f8(x1612,a1)))), % 180.85/180.85 inference(scs_inference,[],[129,119,131,71,43,126,66,145,115,128,28,29,39,38,26,36,30,13])). % 180.85/180.85 cnf(167,plain, % 180.85/180.85 (P3(f8(f4(a5,a9,a1),f4(a5,a9,a1)),a9)), % 180.85/180.85 inference(scs_inference,[],[129,119,131,156,71,43,157,126,89,66,145,115,47,128,28,29,39,38,26,36,30,13,35,12])). % 180.85/180.85 cnf(169,plain, % 180.85/180.85 (P1(f8(a1,x1691))), % 180.85/180.85 inference(scs_inference,[],[129,119,131,156,71,43,157,22,126,89,66,145,115,47,128,153,28,29,39,38,26,36,30,13,35,12,11])). % 180.85/180.85 cnf(173,plain, % 180.85/180.85 (~E(f8(a1,x1731),f8(a5,a9))), % 180.85/180.85 inference(scs_inference,[],[24,49,129,109,119,131,156,21,71,43,157,22,126,89,66,145,115,47,128,153,28,29,39,38,26,36,30,13,35,12,11,3,14])). % 180.85/180.85 cnf(183,plain, % 180.85/180.85 (P2(f8(a2,x1831),x1832)), % 180.85/180.85 inference(scs_inference,[],[159,105,147,28,39,29])). % 180.85/180.85 cnf(188,plain, % 180.85/180.85 (~P3(f8(a7,a7),f4(a5,a9,a1))), % 180.85/180.85 inference(scs_inference,[],[159,105,147,28,39,29,38,40])). % 180.85/180.85 cnf(190,plain, % 180.85/180.85 (~P1(a9)), % 180.85/180.85 inference(scs_inference,[],[159,16,105,138,147,28,39,29,38,40,26])). % 180.85/180.85 cnf(192,plain, % 180.85/180.85 (P3(f4(x1921,a1,a5),a7)), % 180.85/180.85 inference(scs_inference,[],[18,159,16,105,138,147,123,28,39,29,38,40,26,30])). % 180.85/180.85 cnf(196,plain, % 180.85/180.85 (~P3(x1961,f8(x1962,a1))), % 180.85/180.85 inference(rename_variables,[],[43])). % 180.85/180.86 cnf(202,plain, % 180.85/180.86 (~E(f8(a7,a7),f8(x2021,f8(x2022,a1)))), % 180.85/180.86 inference(scs_inference,[],[18,159,71,43,196,16,105,138,147,161,123,115,28,39,29,38,40,26,30,36,35,13])). % 180.85/180.86 cnf(204,plain, % 180.85/180.86 (P3(f8(f4(x2041,a1,a5),f4(x2041,a1,a5)),a5)), % 180.85/180.86 inference(scs_inference,[],[18,159,71,43,196,16,105,138,147,161,123,115,47,28,39,29,38,40,26,30,36,35,13,12])). % 180.85/180.86 cnf(211,plain, % 180.85/180.86 (~E(a7,f8(x2111,a1))), % 180.85/180.86 inference(scs_inference,[],[202,5])). % 180.85/180.86 cnf(212,plain, % 180.85/180.86 (~E(f8(a7,a7),f8(x2121,f8(x2122,a1)))), % 180.85/180.86 inference(rename_variables,[],[202])). % 180.85/180.86 cnf(213,plain, % 180.85/180.86 (~P3(a7,f4(x2131,a1,a5))), % 180.85/180.86 inference(scs_inference,[],[192,202,5,28])). % 180.85/180.86 cnf(215,plain, % 180.85/180.86 (P2(f8(x2151,a2),x2152)), % 180.85/180.86 inference(scs_inference,[],[192,202,149,5,28,29])). % 180.85/180.86 cnf(222,plain, % 180.95/180.86 (P3(f8(f4(x2221,a1,a5),f4(x2221,a1,a5)),a7)), % 180.95/180.86 inference(scs_inference,[],[18,192,188,202,149,204,5,28,29,39,38,30])). % 180.95/180.86 cnf(224,plain, % 180.95/180.86 (~P1(f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[18,192,188,202,212,149,204,169,5,28,29,39,38,30,26])). % 180.95/180.86 cnf(225,plain, % 180.95/180.86 (~E(f8(a7,a7),f8(x2251,f8(x2252,a1)))), % 180.95/180.86 inference(rename_variables,[],[202])). % 180.95/180.86 cnf(232,plain, % 180.95/180.86 (~E(a5,f8(x2321,f8(x2322,a1)))), % 180.95/180.86 inference(scs_inference,[],[18,192,71,43,84,188,202,212,225,149,204,169,5,28,29,39,38,30,26,35,13])). % 180.95/180.86 cnf(234,plain, % 180.95/180.86 (~E(f8(a2,x2341),f8(a5,a9))), % 180.95/180.86 inference(scs_inference,[],[18,24,183,192,71,43,84,188,202,212,225,149,204,169,5,28,29,39,38,30,26,35,13,14])). % 180.95/180.86 cnf(236,plain, % 180.95/180.86 (P3(f4(x2361,a1,a5),f8(f8(a7,a7),f8(a7,a7)))), % 180.95/180.86 inference(scs_inference,[],[18,24,183,192,21,71,43,84,188,202,212,225,149,204,169,5,28,29,39,38,30,26,35,13,14,34])). % 180.95/180.86 cnf(245,plain, % 180.95/180.86 (~P3(x2451,f8(f8(a2,x2452),x2453))), % 180.95/180.86 inference(scs_inference,[],[222,147,28,39])). % 180.95/180.86 cnf(247,plain, % 180.95/180.86 (~P3(x2471,f8(x2472,f8(a2,x2473)))), % 180.95/180.86 inference(scs_inference,[],[222,147,28,39,38])). % 180.95/180.86 cnf(249,plain, % 180.95/180.86 (P3(f4(a5,a9,f8(x2491,a1)),a7)), % 180.95/180.86 inference(scs_inference,[],[18,222,147,155,28,39,38,30])). % 180.95/180.86 cnf(251,plain, % 180.95/180.86 (P3(f4(x2511,a1,a7),a7)), % 180.95/180.86 inference(scs_inference,[],[18,222,147,211,155,41,28,39,38,30,35])). % 180.95/180.86 cnf(254,plain, % 180.95/180.86 (~E(a7,f8(f8(a1,x2541),x2542))), % 180.95/180.86 inference(scs_inference,[],[18,119,222,107,147,211,155,41,28,39,38,30,35,13])). % 180.95/180.86 cnf(256,plain, % 180.95/180.86 (~E(a2,f8(a5,a9))), % 180.95/180.86 inference(scs_inference,[],[18,24,144,119,222,107,147,211,155,41,28,39,38,30,35,13,14])). % 180.95/180.86 cnf(258,plain, % 180.95/180.86 (P2(f8(f8(a2,x2581),x2582),x2583)), % 180.95/180.86 inference(scs_inference,[],[18,24,144,119,222,107,147,211,155,41,28,39,38,30,35,13,14,29])). % 180.95/180.86 cnf(262,plain, % 180.95/180.86 (P3(f8(f4(x2621,a1,a7),f4(x2621,a1,a7)),a7)), % 180.95/180.86 inference(scs_inference,[],[18,24,144,119,222,47,107,51,147,211,155,41,28,39,38,30,35,13,14,29,36,12])). % 180.95/180.86 cnf(268,plain, % 180.95/180.86 (~P3(x2681,f8(f8(x2682,a2),x2683))), % 180.95/180.86 inference(scs_inference,[],[249,149,28,39])). % 180.95/180.86 cnf(272,plain, % 180.95/180.86 (P3(f4(a5,a9,a2),a5)), % 180.95/180.86 inference(scs_inference,[],[249,256,149,66,28,39,38,36])). % 180.95/180.86 cnf(273,plain, % 180.95/180.86 (~P3(x2731,a2)), % 180.95/180.86 inference(rename_variables,[],[66])). % 180.95/180.86 cnf(275,plain, % 180.95/180.86 (P3(f8(f4(a5,a9,a2),f4(a5,a9,a2)),a5)), % 180.95/180.86 inference(scs_inference,[],[249,256,47,149,66,28,39,38,36,12])). % 180.95/180.86 cnf(277,plain, % 180.95/180.86 (P3(f4(a5,a9,a2),a9)), % 180.95/180.86 inference(scs_inference,[],[249,256,47,149,66,273,28,39,38,36,12,35])). % 180.95/180.86 cnf(280,plain, % 180.95/180.86 (~E(f8(a7,a7),f8(x2801,f8(a1,x2802)))), % 180.95/180.86 inference(scs_inference,[],[159,249,256,47,112,149,66,273,28,39,38,36,12,35,13])). % 180.95/180.86 cnf(282,plain, % 180.95/180.86 (~E(f8(x2821,a2),f8(a5,a9))), % 180.95/180.86 inference(scs_inference,[],[24,159,215,249,256,47,112,149,66,273,28,39,38,36,12,35,13,14])). % 180.95/180.86 cnf(284,plain, % 180.95/180.86 (~E(a2,a9)), % 180.95/180.86 inference(scs_inference,[],[24,159,215,249,256,47,112,149,66,273,28,39,38,36,12,35,13,14,5])). % 180.95/180.86 cnf(285,plain, % 180.95/180.86 (P2(f8(f8(x2851,a2),x2852),x2853)), % 180.95/180.86 inference(scs_inference,[],[24,159,215,249,256,47,112,149,66,273,28,39,38,36,12,35,13,14,5,29])). % 180.95/180.86 cnf(287,plain, % 180.95/180.86 (P3(f4(a5,a9,a2),a7)), % 180.95/180.86 inference(scs_inference,[],[18,24,159,215,249,256,47,112,149,66,273,28,39,38,36,12,35,13,14,5,29,30])). % 180.95/180.86 cnf(292,plain, % 180.95/180.86 (~P3(a7,f4(a5,a9,a2))), % 180.95/180.86 inference(scs_inference,[],[287,280,5,28])). % 180.95/180.86 cnf(298,plain, % 180.95/180.86 (P3(f8(f4(a5,a9,a2),f4(a5,a9,a2)),a7)), % 180.95/180.86 inference(scs_inference,[],[18,287,280,95,275,5,28,39,38,30])). % 180.95/180.86 cnf(300,plain, % 180.95/180.86 (P3(f4(a1,x3001,a7),a7)), % 180.95/180.86 inference(scs_inference,[],[18,287,280,95,275,41,5,28,39,38,30,36])). % 180.95/180.86 cnf(303,plain, % 180.95/180.86 (P3(f8(f4(a5,a9,a2),f4(a5,a9,a2)),a9)), % 180.95/180.86 inference(scs_inference,[],[18,287,47,280,95,277,275,41,5,28,39,38,30,36,12])). % 180.95/180.86 cnf(305,plain, % 180.95/180.86 (~E(f8(a7,a7),f8(f8(x3051,a1),x3052))), % 180.95/180.86 inference(scs_inference,[],[18,159,287,47,64,280,95,277,275,41,5,28,39,38,30,36,12,13])). % 180.95/180.86 cnf(309,plain, % 180.95/180.86 (~E(f8(a2,x3091),a5)), % 180.95/180.86 inference(scs_inference,[],[18,24,159,258,287,47,64,280,95,277,275,41,5,28,39,38,30,36,12,13,14,4])). % 180.95/180.86 cnf(320,plain, % 180.95/180.86 (~E(a5,f8(x3201,f8(x3202,a1)))), % 180.95/180.86 inference(rename_variables,[],[232])). % 180.95/180.86 cnf(321,plain, % 180.95/180.86 (~P3(x3211,f8(x3212,a1))), % 180.95/180.86 inference(rename_variables,[],[43])). % 180.95/180.86 cnf(323,plain, % 180.95/180.86 (P3(f4(x3231,f8(x3232,a1),a5),a5)), % 180.95/180.86 inference(scs_inference,[],[298,43,321,232,320,292,28,39,38,36,35])). % 180.95/180.86 cnf(325,plain, % 180.95/180.86 (~P3(x3251,f8(x3252,a1))), % 180.95/180.86 inference(rename_variables,[],[43])). % 180.95/180.86 cnf(327,plain, % 180.95/180.86 (P3(f8(f4(a1,x3271,a7),f4(a1,x3271,a7)),a7)), % 180.95/180.86 inference(scs_inference,[],[298,43,321,47,232,320,292,300,28,39,38,36,35,12])). % 180.95/180.86 cnf(329,plain, % 180.95/180.86 (~E(f8(a7,a7),f8(x3291,a1))), % 180.95/180.86 inference(scs_inference,[],[159,298,43,321,325,47,232,320,292,300,28,39,38,36,35,12,13])). % 180.95/180.86 cnf(335,plain, % 180.95/180.86 (P3(f4(f8(x3351,a1),f8(x3352,a1),a5),a7)), % 180.95/180.86 inference(scs_inference,[],[18,24,159,285,298,43,321,325,47,232,320,292,300,28,39,38,36,35,12,13,14,5,4,30])). % 180.95/180.86 cnf(344,plain, % 180.95/180.86 (P3(f4(x3441,f8(x3442,a1),a5),a7)), % 180.95/180.86 inference(scs_inference,[],[18,335,323,213,28,39,38,30])). % 180.95/180.86 cnf(349,plain, % 180.95/180.86 (P3(f4(f8(x3491,a1),x3492,f8(a7,a7)),f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[18,335,43,305,329,323,213,41,28,39,38,30,35,36])). % 180.95/180.86 cnf(351,plain, % 180.95/180.86 (~P3(x3511,f8(x3512,a1))), % 180.95/180.86 inference(rename_variables,[],[43])). % 180.95/180.86 cnf(353,plain, % 180.95/180.86 (~E(a9,f8(x3531,a1))), % 180.95/180.86 inference(scs_inference,[],[18,335,43,351,167,305,329,323,213,41,28,39,38,30,35,36,13])). % 180.95/180.86 cnf(360,plain, % 180.95/180.86 (~E(a9,f8(x3601,a1))), % 180.95/180.86 inference(rename_variables,[],[353])). % 180.95/180.86 cnf(361,plain, % 180.95/180.86 (~P3(x3611,f8(x3612,a1))), % 180.95/180.86 inference(rename_variables,[],[43])). % 180.95/180.86 cnf(363,plain, % 180.95/180.86 (P3(f4(x3631,a1,a9),a9)), % 180.95/180.86 inference(scs_inference,[],[344,43,353,360,41,28,36,35])). % 180.95/180.86 cnf(366,plain, % 180.95/180.86 (P3(f8(f4(x3661,a1,a9),f4(x3661,a1,a9)),a9)), % 180.95/180.86 inference(scs_inference,[],[344,43,47,353,360,41,28,36,35,12])). % 180.95/180.86 cnf(368,plain, % 180.95/180.86 (~E(f8(a5,a5),f8(x3681,a1))), % 180.95/180.86 inference(scs_inference,[],[344,43,361,47,126,353,360,41,28,36,35,12,13])). % 180.95/180.86 cnf(370,plain, % 180.95/180.86 (~P1(f8(a5,a5))), % 180.95/180.86 inference(scs_inference,[],[344,43,361,47,126,353,360,41,128,28,36,35,12,13,26])). % 180.95/180.86 cnf(377,plain, % 180.95/180.86 (P3(f4(x3771,a1,f8(a5,a5)),f8(a5,a5))), % 180.95/180.86 inference(scs_inference,[],[167,368,41,28,40,35])). % 180.95/180.86 cnf(382,plain, % 180.95/180.86 (~E(f8(a5,a5),a1)), % 180.95/180.86 inference(scs_inference,[],[43,167,92,368,41,28,40,35,13,5])). % 180.95/180.86 cnf(390,plain, % 180.95/180.86 (P3(f4(x3901,a1,f8(a5,a5)),f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[129,43,167,92,368,41,128,28,40,35,13,5,39,38,26,30])). % 180.95/180.86 cnf(399,plain, % 180.95/180.86 (P3(f4(x3991,a1,f8(a5,a5)),a7)), % 180.95/180.86 inference(scs_inference,[],[48,390,377,28,30])). % 180.95/180.86 cnf(401,plain, % 180.95/180.86 (P3(f4(a5,a9,f8(x4011,a2)),a5)), % 180.95/180.86 inference(scs_inference,[],[48,282,390,149,377,28,30,36])). % 180.95/180.86 cnf(418,plain, % 180.95/180.86 (P3(f4(a5,a9,f8(x4181,a2)),a7)), % 180.95/180.86 inference(scs_inference,[],[18,399,401,28,30])). % 180.95/180.86 cnf(433,plain, % 180.95/180.86 (~E(f8(a7,a7),f8(x4331,f8(a1,x4332)))), % 180.95/180.86 inference(rename_variables,[],[280])). % 180.95/180.86 cnf(434,plain, % 180.95/180.86 (~P3(x4341,f8(x4342,a2))), % 180.95/180.86 inference(rename_variables,[],[149])). % 180.95/180.86 cnf(438,plain, % 180.95/180.86 (~P3(x4381,f8(x4382,a2))), % 180.95/180.86 inference(rename_variables,[],[149])). % 180.95/180.86 cnf(440,plain, % 180.95/180.86 (~E(a7,f8(x4401,a2))), % 180.95/180.86 inference(scs_inference,[],[192,418,149,434,438,280,433,28,36,35,13])). % 180.95/180.86 cnf(449,plain, % 180.95/180.86 (~P3(f3(f8(a9,a5),f8(a7,a9)),f8(a7,a9))), % 180.95/180.86 inference(scs_inference,[],[24,22,33,14])). % 180.95/180.86 cnf(450,plain, % 180.95/180.86 (~P3(f8(a5,a5),f4(a5,a9,a1))), % 180.95/180.86 inference(scs_inference,[],[101,28])). % 180.95/180.86 cnf(453,plain, % 180.95/180.86 (~E(a7,f8(f8(a1,x4531),x4532))), % 180.95/180.86 inference(rename_variables,[],[254])). % 180.95/180.86 cnf(454,plain, % 180.95/180.86 (~P3(x4541,f8(x4542,a2))), % 180.95/180.86 inference(rename_variables,[],[149])). % 180.95/180.86 cnf(458,plain, % 180.95/180.86 (~P3(x4581,f8(x4582,a2))), % 180.95/180.86 inference(rename_variables,[],[149])). % 180.95/180.86 cnf(460,plain, % 180.95/180.86 (~E(f8(a7,a7),f8(x4601,a2))), % 180.95/180.86 inference(scs_inference,[],[159,149,454,458,101,254,453,28,36,35,13])). % 180.95/180.86 cnf(469,plain, % 180.95/180.86 (~E(a7,a2)), % 180.95/180.86 inference(scs_inference,[],[97,159,21,149,454,458,101,254,453,28,36,35,13,34,39,38,5])). % 180.95/180.86 cnf(470,plain, % 180.95/180.86 (~P3(f3(f8(a9,a5),f8(a7,a9)),a9)+~P3(f3(f8(a9,a5),f8(a7,a9)),a7)), % 180.95/180.86 inference(scs_inference,[],[97,159,449,21,149,454,458,101,254,453,28,36,35,13,34,39,38,5,40])). % 180.95/180.86 cnf(480,plain, % 180.95/180.86 (~E(f8(a1,x4801),f8(a5,a9))), % 180.95/180.86 inference(rename_variables,[],[173])). % 180.95/180.86 cnf(481,plain, % 180.95/180.86 (~P3(x4811,f8(a1,x4812))), % 180.95/180.86 inference(rename_variables,[],[45])). % 180.95/180.86 cnf(485,plain, % 180.95/180.86 (~P3(x4851,f8(a1,x4852))), % 180.95/180.86 inference(rename_variables,[],[45])). % 180.95/180.86 cnf(487,plain, % 180.95/180.86 (~E(f8(a7,a7),f8(a1,x4871))), % 180.95/180.86 inference(scs_inference,[],[173,480,159,204,45,481,485,28,40,35,36,13])). % 180.95/180.86 cnf(493,plain, % 180.95/180.86 (P3(f4(a5,a9,f8(a1,x4931)),a7)), % 180.95/180.86 inference(scs_inference,[],[18,173,480,159,204,45,481,485,28,40,35,36,13,38,39,30])). % 180.95/180.86 cnf(499,plain, % 180.95/180.86 (~E(f8(a2,x4991),f8(a5,a9))), % 180.95/180.86 inference(rename_variables,[],[234])). % 180.95/180.86 cnf(500,plain, % 180.95/180.86 (~P3(x5001,f8(a2,x5002))), % 180.95/180.86 inference(rename_variables,[],[147])). % 180.95/180.86 cnf(506,plain, % 180.95/180.86 (~E(a5,f8(a1,x5061))), % 180.95/180.86 inference(scs_inference,[],[234,499,493,84,45,147,500,28,35,36,13])). % 180.95/180.86 cnf(508,plain, % 180.95/180.86 (P3(f4(a5,a9,f8(a2,x5081)),a7)), % 180.95/180.86 inference(scs_inference,[],[18,234,499,493,84,45,147,500,28,35,36,13,30])). % 180.95/180.86 cnf(515,plain, % 180.95/180.86 (~P3(x5151,f8(a1,x5152))), % 180.95/180.86 inference(rename_variables,[],[45])). % 180.95/180.86 cnf(519,plain, % 180.95/180.86 (~P3(x5191,f8(a1,x5192))), % 180.95/180.86 inference(rename_variables,[],[45])). % 180.95/180.86 cnf(521,plain, % 180.95/180.86 (~E(f8(a5,a5),f8(a1,x5211))), % 180.95/180.86 inference(scs_inference,[],[508,45,515,519,126,280,254,28,35,36,13])). % 180.95/180.86 cnf(533,plain, % 180.95/180.86 (~E(a7,f8(a2,x5331))), % 180.95/180.86 inference(scs_inference,[],[119,147,66,272,41,460,487,28,35,36,13])). % 180.95/180.86 cnf(547,plain, % 180.95/180.86 (P3(f4(x5471,a2,a7),a7)), % 180.95/180.86 inference(scs_inference,[],[66,41,303,440,521,28,40,36,35])). % 180.95/180.86 cnf(550,plain, % 180.95/180.86 (~E(a9,f8(a1,x5501))), % 180.95/180.86 inference(scs_inference,[],[45,167,66,41,303,440,521,28,40,36,35,13])). % 180.95/180.86 cnf(564,plain, % 180.95/180.86 (P3(f4(a1,x5641,a5),a5)), % 180.95/180.86 inference(scs_inference,[],[41,262,506,28,40,36])). % 180.95/180.86 cnf(605,plain, % 180.95/180.86 (P3(f4(a2,x6051,a7),a7)), % 180.95/180.86 inference(scs_inference,[],[66,327,533,28,40,36])). % 180.95/180.86 cnf(610,plain, % 180.95/180.86 (~P3(x6101,f8(a2,x6102))), % 180.95/180.86 inference(rename_variables,[],[147])). % 180.95/180.86 cnf(612,plain, % 180.95/180.86 (~E(a5,f8(a2,x6121))), % 180.95/180.86 inference(scs_inference,[],[87,147,610,66,327,533,550,28,40,36,35,13])). % 180.95/180.86 cnf(626,plain, % 180.95/180.86 (P3(f4(a2,x6261,a5),a5)), % 180.95/180.86 inference(scs_inference,[],[66,366,612,28,40,36])). % 180.95/180.86 cnf(629,plain, % 180.95/180.86 (P3(f8(f4(a2,x6291,a5),f4(a2,x6291,a5)),a5)), % 180.95/180.86 inference(scs_inference,[],[47,66,366,612,28,40,36,12])). % 180.95/180.86 cnf(633,plain, % 180.95/180.86 (~P3(x6331,f8(x6332,a2))), % 180.95/180.86 inference(rename_variables,[],[149])). % 180.95/180.86 cnf(635,plain, % 180.95/180.86 (~E(a5,f8(x6351,a2))), % 180.95/180.86 inference(scs_inference,[],[47,84,149,633,66,366,612,550,28,40,36,12,35,13])). % 180.95/180.86 cnf(641,plain, % 180.95/180.86 (P3(f4(a2,x6411,a5),a7)), % 180.95/180.86 inference(scs_inference,[],[18,47,84,149,633,66,366,612,550,28,40,36,12,35,13,38,39,30])). % 180.95/180.86 cnf(649,plain, % 180.95/180.86 (~E(a5,f8(x6491,a2))), % 180.95/180.86 inference(rename_variables,[],[635])). % 180.95/180.86 cnf(650,plain, % 180.95/180.86 (~P3(x6501,f8(a1,x6502))), % 180.95/180.86 inference(rename_variables,[],[45])). % 180.95/180.86 cnf(652,plain, % 180.95/180.86 (P3(f4(x6521,a2,a5),a5)), % 180.95/180.86 inference(scs_inference,[],[18,641,45,66,629,635,649,28,30,36,35])). % 180.95/180.86 cnf(661,plain, % 180.95/180.86 (P3(f8(f4(x6611,a2,a5),f4(x6611,a2,a5)),a5)), % 180.95/180.86 inference(scs_inference,[],[18,641,47,45,650,66,236,629,635,649,28,30,36,35,13,38,39,12])). % 180.95/180.86 cnf(667,plain, % 180.95/180.86 (P3(f8(f4(x6671,a2,a5),f4(x6671,a2,a5)),a7)), % 180.95/180.86 inference(scs_inference,[],[18,323,661,28,30])). % 180.95/180.86 cnf(669,plain, % 180.95/180.86 (P3(f4(a1,x6691,a9),a9)), % 180.95/180.86 inference(scs_inference,[],[18,41,323,661,550,28,30,36])). % 180.95/180.86 cnf(674,plain, % 180.95/180.86 (~E(a9,f8(a2,x6741))), % 180.95/180.86 inference(scs_inference,[],[18,47,147,89,41,323,661,550,28,30,36,12,13])). % 180.95/180.86 cnf(683,plain, % 180.95/180.86 (P3(f4(x6831,a2,a5),a7)), % 180.95/180.86 inference(scs_inference,[],[18,667,652,28,40,30])). % 180.95/180.86 cnf(685,plain, % 180.95/180.86 (P3(f4(a2,x6851,a9),a9)), % 180.95/180.86 inference(scs_inference,[],[18,667,66,674,652,28,40,30,36])). % 180.95/180.86 cnf(690,plain, % 180.95/180.86 (~E(f8(a5,a5),f8(x6901,a2))), % 180.95/180.86 inference(scs_inference,[],[18,667,47,149,66,101,674,652,28,40,30,36,12,13])). % 180.95/180.86 cnf(704,plain, % 180.95/180.86 (~E(f8(a5,a5),f8(x7041,a2))), % 180.95/180.86 inference(rename_variables,[],[690])). % 180.95/180.86 cnf(705,plain, % 180.95/180.86 (~P3(x7051,f8(x7052,a2))), % 180.95/180.86 inference(rename_variables,[],[149])). % 180.95/180.86 cnf(710,plain, % 180.95/180.86 (~E(a9,f8(x7101,a2))), % 180.95/180.86 inference(scs_inference,[],[149,705,66,167,155,690,704,28,36,35,13])). % 180.95/180.86 cnf(717,plain, % 180.95/180.86 (~E(a9,f8(x7171,a2))), % 180.95/180.86 inference(rename_variables,[],[710])). % 180.95/180.86 cnf(718,plain, % 180.95/180.86 (~P3(x7181,f8(x7182,a2))), % 180.95/180.86 inference(rename_variables,[],[149])). % 180.95/180.86 cnf(720,plain, % 180.95/180.86 (P3(f4(x7201,a2,a9),a9)), % 180.95/180.86 inference(scs_inference,[],[149,66,401,710,717,28,36,35])). % 180.95/180.86 cnf(725,plain, % 180.95/180.86 (~E(f8(a5,a5),a2)), % 180.95/180.86 inference(scs_inference,[],[149,718,66,401,92,710,717,28,36,35,13,5])). % 180.95/180.86 cnf(726,plain, % 180.95/180.86 (P3(f8(f4(x7261,a2,a9),f4(x7261,a2,a9)),a9)), % 180.95/180.86 inference(scs_inference,[],[47,149,718,66,401,92,710,717,28,36,35,13,5,12])). % 180.95/180.86 cnf(730,plain, % 180.95/180.86 (E(f3(f8(x7301,a1),x7302),f3(a1,x7302))), % 180.95/180.86 inference(scs_inference,[],[73,9,2])). % 180.95/180.86 cnf(736,plain, % 180.95/180.86 (~E(f8(a7,a7),a2)), % 180.95/180.86 inference(scs_inference,[],[149,349,236,730,2,28,13,5])). % 180.95/180.86 cnf(740,plain, % 180.95/180.86 (~P3(a5,f4(a1,x7401,a5))), % 180.95/180.86 inference(scs_inference,[],[564,28])). % 180.95/180.86 cnf(762,plain, % 180.95/180.86 (~P3(a5,f4(x7621,a2,a5))), % 180.95/180.86 inference(scs_inference,[],[661,28,40])). % 180.95/180.86 cnf(822,plain, % 180.95/180.86 (~P3(a9,f4(x8221,a2,a9))), % 180.95/180.86 inference(scs_inference,[],[726,28,40])). % 180.95/180.86 cnf(854,plain, % 180.95/180.86 (~P3(f8(f8(a7,a7),f8(a7,a7)),f4(x8541,a1,a5))), % 180.95/180.86 inference(scs_inference,[],[236,28])). % 180.95/180.86 cnf(1176,plain, % 180.95/180.86 (P1(f8(a2,a2))), % 180.95/180.86 inference(scs_inference,[],[17,47,11])). % 180.95/180.86 cnf(1301,plain, % 180.95/180.86 (~P3(f3(f8(a9,a5),f8(a7,a9)),a7)+~P3(f3(f8(a9,a5),f8(a7,a9)),f8(a9,x13011))), % 180.95/180.86 inference(scs_inference,[],[22,470,31])). % 180.95/180.86 cnf(1586,plain, % 180.95/180.86 (~P3(f3(f8(a9,a5),f8(a7,a9)),f8(a7,x15861))+~P3(f3(f8(a9,a5),f8(a7,a9)),f8(a9,x15862))), % 180.95/180.86 inference(scs_inference,[],[1301,39])). % 180.95/180.86 cnf(1801,plain, % 180.95/180.86 (E(f8(a2,a2),a1)), % 180.95/180.86 inference(scs_inference,[],[1176,736,2,25])). % 180.95/180.86 cnf(1805,plain, % 180.95/180.86 (~P3(f8(a5,a5),f4(a1,x18051,a5))), % 180.95/180.86 inference(scs_inference,[],[1176,740,736,78,564,21,2,25,30,12])). % 180.95/180.86 cnf(1807,plain, % 180.95/180.86 (~E(f8(a2,a2),a6)), % 180.95/180.86 inference(scs_inference,[],[23,1176,740,736,78,564,21,2,25,30,12,11])). % 180.95/180.86 cnf(1808,plain, % 180.95/180.86 (P3(f4(x18081,a2,a7),f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[23,1176,740,736,547,78,564,21,2,25,30,12,11,40])). % 180.95/180.86 cnf(1815,plain, % 180.95/180.86 (E(f8(a2,x18151),f8(x18152,a2))), % 180.95/180.86 inference(scs_inference,[],[23,1176,740,736,547,309,78,564,76,21,147,66,2,25,30,12,11,40,3,28,35])). % 180.95/180.86 cnf(1816,plain, % 180.95/180.86 (~P3(x18161,a2)), % 180.95/180.86 inference(rename_variables,[],[66])). % 180.95/180.86 cnf(1817,plain, % 180.95/180.86 (~P3(x18171,f8(a2,x18172))), % 180.95/180.86 inference(rename_variables,[],[147])). % 180.95/180.86 cnf(1819,plain, % 180.95/180.86 (~P2(f8(a5,a9),f8(a9,a7))), % 180.95/180.86 inference(scs_inference,[],[23,1176,740,736,547,309,78,564,76,21,147,24,66,22,2,25,30,12,11,40,3,28,35,15])). % 180.95/180.86 cnf(1820,plain, % 180.95/180.86 (E(f8(x18201,x18202),f8(x18202,x18201))), % 180.95/180.86 inference(rename_variables,[],[22])). % 180.95/180.86 cnf(1821,plain, % 180.95/180.86 (~P2(f8(a9,a5),f8(a7,a9))), % 180.95/180.86 inference(scs_inference,[],[23,1176,740,736,547,309,78,564,76,21,147,24,66,22,1820,2,25,30,12,11,40,3,28,35,15,14])). % 180.95/180.86 cnf(1823,plain, % 180.95/180.86 (E(f8(a2,x18231),f8(a2,x18232))), % 180.95/180.86 inference(scs_inference,[],[23,1176,740,736,547,309,78,564,76,21,147,1817,24,66,1816,22,1820,2,25,30,12,11,40,3,28,35,15,14,36])). % 180.95/180.86 cnf(1825,plain, % 180.95/180.86 (~P3(x18251,f8(a2,x18252))), % 180.95/180.86 inference(rename_variables,[],[147])). % 180.95/180.86 cnf(1827,plain, % 180.95/180.86 (~E(f8(a2,x18271),f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[23,1176,740,736,547,309,78,564,76,21,147,1817,1825,24,66,1816,22,1820,2,25,30,12,11,40,3,28,35,15,14,36,34])). % 180.95/180.86 cnf(1830,plain, % 180.95/180.86 (E(f8(a1,x18301),a1)), % 180.95/180.86 inference(scs_inference,[],[169,25])). % 180.95/180.86 cnf(1832,plain, % 180.95/180.86 (~E(a6,f8(a2,a2))), % 180.95/180.86 inference(scs_inference,[],[1807,169,25,2])). % 180.95/180.86 cnf(1835,plain, % 180.95/180.86 (P3(f4(a2,x18351,a7),f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[1808,1807,605,169,25,2,28,40])). % 180.95/180.86 cnf(1837,plain, % 180.95/180.86 (~E(f8(a1,x18371),a5)), % 180.95/180.86 inference(scs_inference,[],[136,1808,1807,605,169,25,2,28,40,11])). % 180.95/180.86 cnf(1838,plain, % 180.95/180.86 (~E(f8(x18381,a2),f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[136,1827,1808,1815,1807,605,169,25,2,28,40,11,3])). % 180.95/180.86 cnf(1843,plain, % 180.95/180.86 (E(a2,a1)), % 180.95/180.86 inference(scs_inference,[],[17,25])). % 180.95/180.86 cnf(1849,plain, % 180.95/180.86 (P3(f4(a1,x18491,a9),f8(a9,a9))), % 180.95/180.86 inference(scs_inference,[],[1835,725,669,17,25,4,2,28,40])). % 180.95/180.86 cnf(1851,plain, % 180.95/180.86 (~E(f8(a2,a2),a7)), % 180.95/180.86 inference(scs_inference,[],[151,1835,725,669,1176,17,25,4,2,28,40,11])). % 180.95/180.86 cnf(1854,plain, % 180.95/180.86 (E(f3(a2,x18541),f3(a1,x18541))), % 180.95/180.86 inference(scs_inference,[],[151,1838,1835,1801,725,669,1176,17,25,4,2,28,40,11,3,9])). % 180.95/180.86 cnf(1855,plain, % 180.95/180.86 (E(f3(x18551,a2),f3(x18551,a1))), % 180.95/180.86 inference(scs_inference,[],[151,1838,1835,1801,725,669,1176,17,25,4,2,28,40,11,3,9,10])). % 180.95/180.86 cnf(1856,plain, % 180.95/180.86 (E(f4(a2,x18561,x18562),f4(a1,x18561,x18562))), % 180.95/180.86 inference(scs_inference,[],[151,1838,1835,1801,725,669,1176,17,25,4,2,28,40,11,3,9,10,6])). % 180.95/180.86 cnf(1857,plain, % 180.95/180.86 (E(f4(x18571,a2,x18572),f4(x18571,a1,x18572))), % 180.95/180.86 inference(scs_inference,[],[151,1838,1835,1801,725,669,1176,17,25,4,2,28,40,11,3,9,10,6,7])). % 180.95/180.86 cnf(1858,plain, % 180.95/180.86 (E(f4(x18581,x18582,a2),f4(x18581,x18582,a1))), % 180.95/180.86 inference(scs_inference,[],[151,1838,1835,1801,725,669,1176,17,25,4,2,28,40,11,3,9,10,6,7,8])). % 180.95/180.86 cnf(1859,plain, % 180.95/180.86 (E(f8(x18591,a2),f8(x18591,a1))), % 180.95/180.86 inference(scs_inference,[],[151,1838,1835,1801,725,669,1176,17,25,4,2,28,40,11,3,9,10,6,7,8,5])). % 180.95/180.86 cnf(1860,plain, % 180.95/180.86 (~P1(f8(a9,a9))), % 180.95/180.86 inference(scs_inference,[],[151,1838,1835,1801,725,669,1176,17,25,4,2,28,40,11,3,9,10,6,7,8,5,27])). % 180.95/180.86 cnf(1865,plain, % 180.95/180.86 (~E(a2,a7)), % 180.95/180.86 inference(scs_inference,[],[1849,469,28,2])). % 180.95/180.86 cnf(1866,plain, % 180.95/180.86 (~E(f8(a9,a9),f8(a2,x18661))), % 180.95/180.86 inference(scs_inference,[],[1849,469,66,28,2,32])). % 180.95/180.86 cnf(1867,plain, % 180.95/180.86 (~P3(x18671,a2)), % 180.95/180.86 inference(rename_variables,[],[66])). % 180.95/180.86 cnf(1872,plain, % 180.95/180.86 (P3(f4(a2,x18721,a9),f8(a9,a9))), % 180.95/180.86 inference(scs_inference,[],[1856,1849,1805,469,685,66,28,2,32,13,40])). % 180.95/180.86 cnf(1874,plain, % 180.95/180.86 (~E(f8(a2,a2),a9)), % 180.95/180.86 inference(scs_inference,[],[190,1856,1849,1805,469,685,1176,66,28,2,32,13,40,11])). % 180.95/180.86 cnf(1875,plain, % 180.95/180.86 (~E(f8(a6,a6),f8(a2,a2))), % 180.95/180.86 inference(scs_inference,[],[190,1856,1849,1832,1805,469,685,1176,66,47,28,2,32,13,40,11,3])). % 180.95/180.86 cnf(1877,plain, % 180.95/180.86 (~E(f8(a9,a9),f8(x18771,a2))), % 180.95/180.86 inference(scs_inference,[],[190,1856,1849,1832,1805,469,685,1176,66,1867,47,28,2,32,13,40,11,3,31])). % 180.95/180.86 cnf(1882,plain, % 180.95/180.86 (~E(f8(x18821,a2),f8(a9,a9))), % 180.95/180.86 inference(scs_inference,[],[1877,1872,28,2])). % 180.95/180.86 cnf(1887,plain, % 180.95/180.86 (~E(a1,a7)), % 180.95/180.86 inference(scs_inference,[],[1843,1865,1877,1858,1872,720,450,28,2,13,40,3])). % 180.95/180.86 cnf(1888,plain, % 180.95/180.86 (~E(f8(a1,x18881),f8(a5,a5))), % 180.95/180.86 inference(scs_inference,[],[1843,1865,370,1877,1858,1872,720,450,169,28,2,13,40,3,11])). % 180.95/180.86 cnf(1889,plain, % 180.95/180.86 (E(f8(a2,x18891),f8(x18892,a1))), % 180.95/180.86 inference(scs_inference,[],[1843,1865,370,1877,1858,1872,720,450,169,147,41,28,2,13,40,3,11,35])). % 180.95/180.86 cnf(1890,plain, % 180.95/180.86 (~P3(x18901,a1)), % 180.95/180.86 inference(rename_variables,[],[41])). % 180.95/180.86 cnf(1891,plain, % 180.95/180.86 (~P3(x18911,f8(a2,x18912))), % 180.95/180.86 inference(rename_variables,[],[147])). % 180.95/180.86 cnf(1893,plain, % 180.95/180.86 (P3(f4(a2,x18931,a5),f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[1843,1865,370,1877,1858,1872,720,450,626,78,169,147,41,28,2,13,40,3,11,35,30])). % 180.95/180.86 cnf(1895,plain, % 180.95/180.86 (~P3(f8(a5,a5),f4(x18951,a2,a5))), % 180.95/180.86 inference(scs_inference,[],[1843,1865,370,1877,1858,1872,720,762,450,626,78,169,21,147,41,28,2,13,40,3,11,35,30,12])). % 180.95/180.86 cnf(1897,plain, % 180.95/180.86 (E(f8(a2,x18971),f8(a1,x18972))), % 180.95/180.86 inference(scs_inference,[],[1843,1865,370,1877,1858,1872,720,762,450,626,78,169,21,147,1891,41,1890,28,2,13,40,3,11,35,30,12,36])). % 180.95/180.86 cnf(1901,plain, % 180.95/180.86 (P2(f4(x19011,a1,x19012),f4(x19011,a2,x19012))), % 180.95/180.86 inference(scs_inference,[],[1843,1865,370,1877,1857,1858,1872,720,762,450,626,78,20,169,21,147,1891,41,1890,28,2,13,40,3,11,35,30,12,36,14])). % 180.95/180.86 cnf(1905,plain, % 180.95/180.86 (~E(f8(a2,x19051),f8(a9,a9))), % 180.95/180.86 inference(scs_inference,[],[1866,1893,28,2])). % 180.95/180.86 cnf(1908,plain, % 180.95/180.86 (P2(f4(x19081,a1,x19082),f4(x19081,a2,x19082))), % 180.95/180.86 inference(rename_variables,[],[1901])). % 180.95/180.86 cnf(1912,plain, % 180.95/180.86 (P2(f4(a2,a1,x19121),f4(a1,a2,x19121))), % 180.95/180.86 inference(scs_inference,[],[1866,1901,1908,1893,1895,1856,1858,188,28,2,30,13,15])). % 180.95/180.86 cnf(1915,plain, % 180.95/180.86 (P3(f4(x19151,a2,a5),f8(a7,a7))), % 180.95/180.86 inference(scs_inference,[],[1866,1901,1908,1893,1895,683,1856,1858,188,28,2,30,13,15,40])). % 180.95/180.86 cnf(1917,plain, % 180.95/180.86 (~E(a2,f8(a9,a9))), % 180.95/180.86 inference(scs_inference,[],[1860,1866,1901,1908,1893,1895,683,1856,1858,188,17,28,2,30,13,15,40,11])). % 180.95/180.86 cnf(1918,plain, % 180.95/180.86 (~E(f8(x19181,a1),a7)), % 180.95/180.86 inference(scs_inference,[],[1887,1860,1866,1901,1908,1893,1895,683,1856,1858,188,17,73,28,2,30,13,15,40,11,3])). % 180.95/180.86 cnf(1919,plain, % 180.95/180.87 (~E(f8(a1,x19191),f8(a9,a9))), % 180.95/180.87 inference(scs_inference,[],[1887,1860,1866,1901,1908,1893,1895,683,363,1856,1858,188,17,73,45,28,2,30,13,15,40,11,3,34])). % 180.95/180.87 cnf(1926,plain, % 180.95/180.87 (P3(f4(x19261,a1,a7),f8(a7,a7))), % 180.95/180.87 inference(scs_inference,[],[1919,1915,251,28,2,40])). % 180.95/180.87 cnf(1929,plain, % 180.95/180.87 (E(f3(a2,a2),f3(a1,a1))), % 180.95/180.87 inference(scs_inference,[],[224,1919,1915,1854,1855,251,128,28,2,40,11,3])). % 180.95/180.87 cnf(1932,plain, % 180.95/180.87 (~E(f8(a2,x19321),f8(a5,a5))), % 180.95/180.87 inference(scs_inference,[],[224,1919,1915,1854,1855,251,652,128,147,28,2,40,11,3,34])). % 180.95/180.87 cnf(1939,plain, % 180.95/180.87 (P3(f4(a5,a9,a2),f8(a9,a9))), % 180.95/180.87 inference(scs_inference,[],[1932,1926,277,28,2,40])). % 180.95/180.87 cnf(1941,plain, % 180.95/180.87 (~E(f8(x19411,a1),f8(a9,a9))), % 180.95/180.87 inference(scs_inference,[],[1932,1882,1926,1859,277,28,2,40,3])). % 180.95/180.87 cnf(1948,plain, % 180.95/180.87 (P3(f4(a1,x19481,a7),f8(a7,a7))), % 180.95/180.87 inference(scs_inference,[],[1939,1941,300,28,2,40])). % 180.95/180.87 cnf(1952,plain, % 180.95/180.87 (E(f8(a1,x19521),f8(x19522,a2))), % 180.95/180.87 inference(scs_inference,[],[1939,1851,1941,1897,300,45,66,28,2,40,3,35])). % 180.95/180.87 cnf(1953,plain, % 180.95/180.87 (~P3(x19531,a2)), % 180.95/180.87 inference(rename_variables,[],[66])). % 180.95/180.87 cnf(1954,plain, % 180.95/180.87 (~P3(x19541,f8(a1,x19542))), % 180.95/180.87 inference(rename_variables,[],[45])). % 180.95/180.87 cnf(1958,plain, % 180.95/180.87 (E(f8(a1,x19581),f8(a2,x19582))), % 180.95/180.87 inference(scs_inference,[],[1939,1851,1941,1897,822,300,21,45,1954,66,1953,28,2,40,3,35,12,36])). % 180.95/180.87 cnf(1962,plain, % 180.95/180.87 (P2(f3(a1,a1),f3(a2,a2))), % 180.95/180.87 inference(scs_inference,[],[1939,1851,1941,1897,1929,822,300,20,21,45,1954,66,1953,28,2,40,3,35,12,36,14])). % 180.95/180.87 cnf(1966,plain, % 180.95/180.87 (~E(f8(a2,a2),f8(a6,a6))), % 180.95/180.87 inference(scs_inference,[],[1948,1875,28,2])). % 180.95/180.87 cnf(1967,plain, % 180.95/180.87 (P3(f4(x19671,a1,a9),f8(a9,a9))), % 180.95/180.87 inference(scs_inference,[],[1948,1875,363,28,2,40])). % 180.95/180.87 cnf(1971,plain, % 180.95/180.87 (P2(f4(a2,a1,x19711),f4(a1,a1,x19711))), % 180.95/180.87 inference(scs_inference,[],[1874,1948,1875,1889,1912,1857,363,28,2,40,3,15])). % 180.95/180.87 cnf(1978,plain, % 180.95/180.87 (~E(a1,f8(a9,a9))), % 180.95/180.87 inference(scs_inference,[],[1905,1967,1917,1801,564,28,2,40,3])). % 180.95/180.87 cnf(1994,plain, % 180.95/180.87 (~P3(f3(a2,a2),f3(a1,a1))), % 180.95/180.87 inference(scs_inference,[],[1962,1888,1978,1952,626,2,40,3,30,28])). % 180.95/180.87 cnf(1996,plain, % 180.95/180.87 (~P3(f3(a2,a2),f3(a2,a1))), % 180.95/180.87 inference(scs_inference,[],[1994,284,1854,2,13])). % 180.95/180.87 cnf(2000,plain, % 180.95/180.87 (E(f4(a2,a2,x20001),f4(a1,a1,x20001))), % 180.95/180.87 inference(scs_inference,[],[1994,284,1854,1856,1857,652,2,13,40,3])). % 180.95/180.87 cnf(2009,plain, % 180.95/180.87 (~E(a1,f8(a5,a5))), % 180.95/180.87 inference(scs_inference,[],[382,2])). % 180.95/180.87 cnf(2012,plain, % 180.95/180.87 (~E(f8(a2,x20121),f8(a6,a6))), % 180.95/180.87 inference(scs_inference,[],[1966,1823,382,272,2,40,3])). % 180.95/180.87 cnf(2017,plain, % 180.95/180.87 (~E(f8(a6,a6),f8(a2,x20171))), % 180.95/180.87 inference(scs_inference,[],[2012,2])). % 180.95/180.87 cnf(2020,plain, % 180.95/180.87 (E(f4(a2,a2,a2),f4(a1,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2000,2012,1858,123,2,40,3])). % 180.95/180.87 cnf(2023,plain, % 180.95/180.87 (~E(f8(a1,x20231),a6)), % 180.95/180.87 inference(scs_inference,[],[2000,2012,23,1858,123,169,2,40,3,11])). % 180.95/180.87 cnf(2024,plain, % 180.95/180.87 (~P3(x20241,f4(a2,a2,a2))+P3(x20241,f4(a1,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2000,2012,23,1858,123,169,2,40,3,11,13])). % 180.95/180.87 cnf(2028,plain, % 180.95/180.87 (~E(a6,f8(a2,x20281))), % 180.95/180.87 inference(scs_inference,[],[2017,2023,89,21,2,40,3])). % 180.95/180.87 cnf(2031,plain, % 180.95/180.87 (P2(f4(a1,a1,a1),f4(a2,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2020,2028,20,2,14])). % 180.95/180.87 cnf(2033,plain, % 180.95/180.87 (~P3(x20331,f4(a1,a1,a1))+P3(x20331,f4(a2,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2020,2028,20,2,14,30])). % 180.95/180.87 cnf(2040,plain, % 180.95/180.87 (P2(f4(a1,a1,a1),f4(a1,a1,a2))), % 180.95/180.87 inference(scs_inference,[],[2031,1837,114,2000,674,2,3,15])). % 180.95/180.87 cnf(2044,plain, % 180.95/180.87 (~E(a2,a6)), % 180.95/180.87 inference(scs_inference,[],[2009,710,23,17,73,2,3,11])). % 180.95/180.87 cnf(2045,plain, % 180.95/180.87 (~E(a6,a2)), % 180.95/180.87 inference(scs_inference,[],[2044,2])). % 180.95/180.87 cnf(2046,plain, % 180.95/180.87 (~E(a1,a6)), % 180.95/180.87 inference(scs_inference,[],[2044,1843,2,3])). % 180.95/180.87 cnf(2048,plain, % 180.95/180.87 (~E(f8(x20481,a1),a6)), % 180.95/180.87 inference(scs_inference,[],[2046,73,2,3])). % 180.95/180.87 cnf(2051,plain, % 180.95/180.87 (P2(f4(a1,a1,x20511),f4(a2,a2,x20511))), % 180.95/180.87 inference(scs_inference,[],[2046,2040,2000,20,73,2,3,30,14])). % 180.95/180.87 cnf(2055,plain, % 180.95/180.87 (~P3(f4(a1,a1,a2),f4(a1,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2046,2040,2000,20,73,2,3,30,14,28])). % 180.95/180.87 cnf(2057,plain, % 180.95/180.87 (~P3(f4(a1,a1,a2),f4(a2,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2055,2024])). % 180.95/180.87 cnf(2059,plain, % 180.95/180.87 (~P3(f4(a2,a2,a2),f4(a1,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2055,2048,2000,2024,2,12])). % 180.95/180.87 cnf(2060,plain, % 180.95/180.87 (E(f4(a2,a2,x20601),f4(a1,a1,x20601))), % 180.95/180.87 inference(rename_variables,[],[2000])). % 180.95/180.87 cnf(2061,plain, % 180.95/180.87 (~P3(f4(a1,a1,a2),f4(a2,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2055,1971,2048,2000,2024,2,12,30])). % 180.95/180.87 cnf(2064,plain, % 180.95/180.87 (~P3(f4(a1,a1,a2),f4(a2,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2055,1971,2048,2000,2060,2024,2,12,30,13])). % 180.95/180.87 cnf(2066,plain, % 180.95/180.87 (P2(f4(a1,a1,a2),f4(a1,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2055,1971,2051,2048,2020,2000,2060,2024,2,12,30,13,15])). % 180.95/180.87 cnf(2071,plain, % 180.95/180.87 (~P3(f4(a2,a1,a2),f4(a2,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2059,2066,2057,440,1856,2,30,12])). % 180.95/180.87 cnf(2072,plain, % 180.95/180.87 (E(f4(a2,x20721,x20722),f4(a1,x20721,x20722))), % 180.95/180.87 inference(rename_variables,[],[1856])). % 180.95/180.87 cnf(2073,plain, % 180.95/180.87 (~P3(f4(a2,a2,a2),f4(a2,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2059,2066,2057,440,2020,1856,2,30,12,13])). % 180.95/180.87 cnf(2074,plain, % 180.95/180.87 (E(f4(a2,x20741,a2),f4(a1,x20741,a1))), % 180.95/180.87 inference(scs_inference,[],[2059,2066,2057,440,2020,1856,2072,1858,2,30,12,13,3])). % 180.95/180.87 cnf(2077,plain, % 180.95/180.87 (~P3(f4(a2,a1,a2),f4(a1,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2059,2066,2057,440,2020,1856,2072,1858,2,30,12,13,3,2033])). % 180.95/180.87 cnf(2079,plain, % 180.95/180.87 (~E(f8(a5,a9),a1)), % 180.95/180.87 inference(scs_inference,[],[80,2])). % 180.95/180.87 cnf(2082,plain, % 180.95/180.87 (~P3(f4(a1,a2,a2),f4(a2,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2077,2061,2066,80,1857,2,30,12])). % 180.95/180.87 cnf(2086,plain, % 180.95/180.87 (~E(f8(a6,a6),a2)), % 180.95/180.87 inference(scs_inference,[],[2045,2077,2061,2074,2066,80,1857,47,2,30,12,13,3])). % 180.95/180.87 cnf(2088,plain, % 180.95/180.87 (~E(a2,f8(a6,a6))), % 180.95/180.87 inference(scs_inference,[],[2086,2])). % 180.95/180.87 cnf(2094,plain, % 180.95/180.87 (~P3(f4(a1,a2,a2),f4(a2,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2073,2086,2064,2082,1901,2000,1857,2,30,12,13])). % 180.95/180.87 cnf(2100,plain, % 180.95/180.87 (~P3(f4(a1,a2,a2),f4(a1,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2094,2051,282,2,30])). % 180.95/180.87 cnf(2107,plain, % 180.95/180.87 (~E(a1,f8(a6,a6))), % 180.95/180.87 inference(scs_inference,[],[2094,2088,2051,2061,282,1843,1856,1858,2,30,12,13,3])). % 180.95/180.87 cnf(2110,plain, % 180.95/180.87 (~E(f8(a6,a6),a1)), % 180.95/180.87 inference(scs_inference,[],[2107,2])). % 180.95/180.87 cnf(2111,plain, % 180.95/180.87 (~P3(f4(a1,a2,a2),f4(a1,a1,a2))), % 180.95/180.87 inference(scs_inference,[],[2100,2107,2066,2,30])). % 180.95/180.87 cnf(2129,plain, % 180.95/180.87 (~P3(x21291,f4(a2,a1,a1))+P3(x21291,f4(a1,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[1918,1958,1912,131,1858,2,14,3,30])). % 180.95/180.87 cnf(2139,plain, % 180.95/180.87 (P2(f4(a2,a1,a1),f4(a1,a1,a2))), % 180.95/180.87 inference(scs_inference,[],[1971,51,1858,2,14])). % 180.95/180.87 cnf(2152,plain, % 180.95/180.87 (~P2(f8(a9,a5),f8(a9,a7))), % 180.95/180.87 inference(scs_inference,[],[1819,22,14])). % 180.95/180.87 cnf(2161,plain, % 180.95/180.87 (~P3(x21611,f8(f4(a2,a1,a1),x21612))+P3(x21611,f4(a1,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2129,39])). % 180.95/180.87 cnf(2181,plain, % 180.95/180.87 (E(a1,f8(x21811,a2))), % 180.95/180.87 inference(scs_inference,[],[41,66,35])). % 180.95/180.87 cnf(2183,plain, % 180.95/180.87 (~P3(x21831,a1)), % 180.95/180.87 inference(rename_variables,[],[41])). % 180.95/180.87 cnf(2185,plain, % 180.95/180.87 (E(a1,f8(a1,x21851))), % 180.95/180.87 inference(scs_inference,[],[41,2183,66,35,36])). % 180.95/180.87 cnf(2190,plain, % 180.95/180.87 (E(f8(x21901,a2),f8(x21902,a1))), % 180.95/180.87 inference(scs_inference,[],[41,149,35])). % 180.95/180.87 cnf(2210,plain, % 180.95/180.87 (E(a1,f8(a2,x22101))), % 180.95/180.87 inference(scs_inference,[],[41,66,36])). % 180.95/180.87 cnf(2230,plain, % 180.95/180.87 (E(f8(x22301,a1),f8(x22302,a2))), % 180.95/180.87 inference(scs_inference,[],[43,66,35])). % 180.95/180.87 cnf(2231,plain, % 180.95/180.87 (~P3(x22311,a2)), % 180.95/180.87 inference(rename_variables,[],[66])). % 180.95/180.87 cnf(2232,plain, % 180.95/180.87 (~P3(x22321,f8(x22322,a1))), % 180.95/180.87 inference(rename_variables,[],[43])). % 180.95/180.87 cnf(2234,plain, % 180.95/180.87 (E(f8(x22341,a1),f8(a2,x22342))), % 180.95/180.87 inference(scs_inference,[],[43,2232,66,2231,35,36])). % 180.95/180.87 cnf(2240,plain, % 180.95/180.87 (~E(f8(a9,a5),a1)), % 180.95/180.87 inference(scs_inference,[],[2079,22,3])). % 180.95/180.87 cnf(2243,plain, % 180.95/180.87 (~E(a1,f8(a9,a5))), % 180.95/180.87 inference(scs_inference,[],[2240,2])). % 180.95/180.87 cnf(2258,plain, % 180.95/180.87 (~E(f8(a2,x22581),f8(a9,a5))), % 180.95/180.87 inference(scs_inference,[],[2210,2243,3])). % 180.95/180.87 cnf(2264,plain, % 180.95/180.87 (~E(f8(a9,a5),f8(x22641,a2))), % 180.95/180.87 inference(scs_inference,[],[2181,2243,3,2])). % 180.95/180.87 cnf(2265,plain, % 180.95/180.87 (E(a1,f8(x22651,f8(a2,x22652)))), % 180.95/180.87 inference(scs_inference,[],[16,147,27,35])). % 180.95/180.87 cnf(2267,plain, % 180.95/180.87 (E(a2,f8(x22671,a2))), % 180.95/180.87 inference(scs_inference,[],[66,35])). % 180.95/180.87 cnf(2269,plain, % 180.95/180.87 (~P3(x22691,a2)), % 180.95/180.87 inference(rename_variables,[],[66])). % 180.95/180.87 cnf(2271,plain, % 180.95/180.87 (E(a2,f8(a2,x22711))), % 180.95/180.87 inference(scs_inference,[],[66,2269,35,36])). % 180.95/180.87 cnf(2276,plain, % 180.95/180.87 (E(a2,f8(x22761,a1))), % 180.95/180.87 inference(scs_inference,[],[66,41,35])). % 180.95/180.87 cnf(2305,plain, % 180.95/180.87 (E(f8(a1,x23051),f8(f8(a2,x23052),x23053))), % 180.95/180.87 inference(scs_inference,[],[169,147,27,36])). % 180.95/180.87 cnf(2306,plain, % 180.95/180.87 (E(a2,f8(f8(x23061,a2),x23062))), % 180.95/180.87 inference(scs_inference,[],[17,149,27,36])). % 180.95/180.87 cnf(2322,plain, % 180.95/180.87 (E(f8(x23221,f8(x23222,a2)),f8(x23221,a2))), % 180.95/180.87 inference(scs_inference,[],[2267,2,5])). % 180.95/180.87 cnf(2323,plain, % 180.95/180.87 (E(f4(x23231,f8(a2,x23232),x23233),f4(x23231,a2,x23233))), % 180.95/180.87 inference(scs_inference,[],[2271,2,7])). % 180.95/180.87 cnf(2324,plain, % 180.95/180.87 (E(f4(x23241,x23242,f8(x23243,a1)),f4(x23241,x23242,a2))), % 180.95/180.87 inference(scs_inference,[],[2276,2,8])). % 180.95/180.87 cnf(2341,plain, % 180.95/180.87 (E(f4(x23411,f8(a1,x23412),x23413),f4(x23411,a1,x23413))), % 180.95/180.87 inference(scs_inference,[],[2185,2,7])). % 180.95/180.87 cnf(2342,plain, % 180.95/180.87 (E(f4(x23421,x23422,f8(a2,x23423)),f4(x23421,x23422,a1))), % 180.95/180.87 inference(scs_inference,[],[2210,2,8])). % 180.95/180.87 cnf(2369,plain, % 180.95/180.87 (E(f4(x23691,f8(x23692,a1),x23693),f4(x23691,a2,x23693))), % 180.95/180.87 inference(scs_inference,[],[2276,2,7])). % 180.95/180.87 cnf(2407,plain, % 180.95/180.87 (E(f3(x24071,a1),f3(x24071,a2))), % 180.95/180.87 inference(scs_inference,[],[1843,2,10])). % 180.95/180.87 cnf(2408,plain, % 180.95/180.87 (~P3(f3(a2,a1),f3(a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2407,1996,12])). % 180.95/180.87 cnf(2409,plain, % 180.95/180.87 (E(f3(x24091,a1),f3(x24091,a2))), % 180.95/180.87 inference(rename_variables,[],[2407])). % 180.95/180.87 cnf(2412,plain, % 180.95/180.87 (E(f3(a2,a1),f3(a1,a2))), % 180.95/180.87 inference(scs_inference,[],[2407,2409,1996,1854,1855,12,13,3])). % 180.95/180.87 cnf(2423,plain, % 180.95/180.87 (E(f8(x24231,f3(a1,a2)),f8(x24231,f3(a2,a1)))), % 180.95/180.87 inference(scs_inference,[],[2412,2,5])). % 180.95/180.87 cnf(2437,plain, % 180.95/180.87 (E(f4(x24371,a1,x24372),f4(x24371,a2,x24372))), % 180.95/180.87 inference(scs_inference,[],[1843,2,7])). % 180.95/180.87 cnf(2438,plain, % 180.95/180.87 (P2(f4(a2,a2,a1),f4(a1,a1,a2))), % 180.95/180.87 inference(scs_inference,[],[2139,2437,14])). % 180.95/180.87 cnf(2439,plain, % 180.95/180.87 (E(f4(x24391,a1,x24392),f4(x24391,a2,x24392))), % 180.95/180.87 inference(rename_variables,[],[2437])). % 180.95/180.87 cnf(2440,plain, % 180.95/180.87 (E(f4(a2,a1,a2),f4(a1,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2139,2437,2439,2074,14,3])). % 180.95/180.87 cnf(2441,plain, % 180.95/180.87 (E(f4(x24411,a1,x24412),f4(x24411,a2,x24412))), % 180.95/180.87 inference(rename_variables,[],[2437])). % 180.95/180.87 cnf(2443,plain, % 180.95/180.87 (~P3(f4(a1,a1,a2),f4(a1,a1,a2))), % 180.95/180.87 inference(scs_inference,[],[2139,2437,2439,2441,2111,2074,14,3,12])). % 180.95/180.87 cnf(2445,plain, % 180.95/180.87 (~P3(x24451,f4(a2,a1,a2))+P3(x24451,f4(a1,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2139,2437,2439,2441,2111,2074,14,3,12,13])). % 180.95/180.87 cnf(2447,plain, % 180.95/180.87 (P2(f4(a2,a2,a1),f4(a1,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2438,2437,15])). % 180.95/180.87 cnf(2450,plain, % 180.95/180.87 (E(f8(f4(a1,a2,a1),x24501),f8(f4(a2,a1,a2),x24501))), % 180.95/180.87 inference(scs_inference,[],[2440,2,4])). % 180.95/180.87 cnf(2451,plain, % 180.95/180.87 (P2(f4(a1,a2,a1),f4(a2,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2440,1901,14])). % 180.95/180.87 cnf(2453,plain, % 180.95/180.87 (E(f4(a2,a1,x24531),f4(a1,a2,x24531))), % 180.95/180.87 inference(scs_inference,[],[2440,1901,2437,1856,14,3])). % 180.95/180.87 cnf(2457,plain, % 180.95/180.87 (~P3(f4(a2,a1,a2),f4(a1,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2451,2071,30])). % 180.95/180.87 cnf(2459,plain, % 180.95/180.87 (~P3(f4(a2,a2,a2),f4(a1,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2451,2071,1857,30,12])). % 180.95/180.87 cnf(2461,plain, % 180.95/180.87 (P2(f4(a1,a2,a1),f4(a1,a1,a1))), % 180.95/180.87 inference(scs_inference,[],[2451,2071,2020,1857,30,12,15])). % 180.95/180.87 cnf(2463,plain, % 180.95/180.87 (~P3(f4(a1,a2,a2),f4(a1,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2461,2100,30])). % 180.95/180.87 cnf(2466,plain, % 180.95/180.87 (~P3(f4(a1,a1,a2),f4(a1,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2461,2055,30])). % 180.95/180.87 cnf(2472,plain, % 180.95/180.87 (E(f4(x24721,a1,a2),f4(x24721,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2437,1858,3])). % 180.95/180.87 cnf(2473,plain, % 180.95/180.87 (E(f4(x24731,x24732,a2),f4(x24731,x24732,a1))), % 180.95/180.87 inference(rename_variables,[],[1858])). % 180.95/180.87 cnf(2475,plain, % 180.95/180.87 (P2(f4(a2,a2,a1),f4(a1,a2,a1))), % 180.95/180.87 inference(scs_inference,[],[2447,2437,1858,2473,3,15])). % 180.95/180.87 cnf(2479,plain, % 180.95/180.87 (~P3(f4(a1,a1,a2),f4(a1,a2,a2))), % 180.95/180.87 inference(scs_inference,[],[2443,1857,13])). % 180.95/180.87 cnf(2490,plain, % 181.01/180.87 (~P3(f4(a1,a2,a2),f4(a1,a2,a2))), % 181.01/180.87 inference(scs_inference,[],[1857,2479,12])). % 181.01/180.87 cnf(2491,plain, % 181.01/180.87 (E(f4(x24911,a2,x24912),f4(x24911,a1,x24912))), % 181.01/180.87 inference(rename_variables,[],[1857])). % 181.01/180.87 cnf(2492,plain, % 181.01/180.87 (E(f4(x24921,a2,a2),f4(x24921,a1,a1))), % 181.01/180.87 inference(scs_inference,[],[1857,2491,2479,1858,12,3])). % 181.01/180.87 cnf(2515,plain, % 181.01/180.87 (P2(f4(x25151,a1,a2),f4(x25151,a1,a1))), % 181.01/180.87 inference(scs_inference,[],[1901,2492,15])). % 181.01/180.87 cnf(2517,plain, % 181.01/180.87 (P2(f4(x25171,a1,x25172),f4(x25171,a2,x25172))), % 181.01/180.87 inference(rename_variables,[],[1901])). % 181.01/180.87 cnf(2518,plain, % 181.01/180.87 (P2(f4(a1,a2,x25181),f4(a2,a2,x25181))), % 181.01/180.87 inference(scs_inference,[],[1901,2517,2453,2492,15,14])). % 181.01/180.87 cnf(2525,plain, % 181.01/180.87 (P2(f4(x25251,a2,a2),f4(x25251,a1,a1))), % 181.01/180.87 inference(scs_inference,[],[2515,2437,14])). % 181.01/180.87 cnf(2527,plain, % 181.01/180.87 (P2(f4(a1,a2,a2),f4(a1,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2515,2518,2437,2074,14,15])). % 181.01/180.87 cnf(2534,plain, % 181.01/180.87 (P2(f4(a1,a2,a1),f4(a2,a1,a1))), % 181.01/180.87 inference(scs_inference,[],[2515,2440,14])). % 181.01/180.87 cnf(2536,plain, % 181.01/180.87 (P2(f4(a2,a2,a2),f4(a1,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2525,2515,2440,2453,14,15])). % 181.01/180.87 cnf(2545,plain, % 181.01/180.87 (P3(f4(a6,a6,a1),a6)), % 181.01/180.87 inference(scs_inference,[],[2110,41,2,35])). % 181.01/180.87 cnf(2546,plain, % 181.01/180.87 (~P3(a6,f4(a6,a6,a1))), % 181.01/180.87 inference(scs_inference,[],[2545,28])). % 181.01/180.87 cnf(2548,plain, % 181.01/180.87 (~P3(f8(a6,a6),f4(a6,a6,a1))), % 181.01/180.87 inference(scs_inference,[],[2545,21,28,12])). % 181.01/180.87 cnf(2580,plain, % 181.01/180.87 (P2(f4(a2,a2,x25801),f4(a1,a1,x25801))), % 181.01/180.87 inference(scs_inference,[],[1971,2437,14])). % 181.01/180.87 cnf(2582,plain, % 181.01/180.87 (P2(f4(a2,a1,a2),f4(a1,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[1971,2437,2472,14,15])). % 181.01/180.87 cnf(2586,plain, % 181.01/180.87 (E(f4(x25861,x25862,a1),f4(x25861,x25862,a2))), % 181.01/180.87 inference(scs_inference,[],[1843,2,8])). % 181.01/180.87 cnf(2587,plain, % 181.01/180.87 (~P3(f4(a2,a1,a1),f4(a1,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2457,2586,12])). % 181.01/180.87 cnf(2588,plain, % 181.01/180.87 (E(f4(x25881,x25882,a1),f4(x25881,x25882,a2))), % 181.01/180.87 inference(rename_variables,[],[2586])). % 181.01/180.87 cnf(2589,plain, % 181.01/180.87 (E(f4(a2,a2,a1),f4(a1,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2457,2586,2588,2000,12,3])). % 181.01/180.87 cnf(2592,plain, % 181.01/180.87 (~P3(f4(a2,a1,a1),f4(a2,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2457,2475,2586,2588,2000,12,3,30])). % 181.01/180.87 cnf(2594,plain, % 181.01/180.87 (~P3(f4(a2,a1,a1),f4(a2,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2457,2475,2586,2588,2440,2000,12,3,30,13])). % 181.01/180.87 cnf(2596,plain, % 181.01/180.87 (~P3(f4(a2,a1,a1),f4(a1,a1,a1))), % 181.01/180.87 inference(scs_inference,[],[2592,2051,30])). % 181.01/180.87 cnf(2599,plain, % 181.01/180.87 (~P3(f4(a2,a2,a1),f4(a1,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2459,2592,2586,2051,30,12])). % 181.01/180.87 cnf(2601,plain, % 181.01/180.87 (~P3(f4(a2,a2,a1),f4(a2,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2459,2592,2586,2051,30,12,2445])). % 181.01/180.87 cnf(2606,plain, % 181.01/180.87 (~P3(f4(a1,a2,a1),f4(a1,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2463,2527,2587,2586,30,12])). % 181.01/180.87 cnf(2608,plain, % 181.01/180.87 (P2(f4(a1,a1,a2),f4(a1,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2463,2527,2536,2587,2586,2000,30,12,14])). % 181.01/180.87 cnf(2613,plain, % 181.01/180.87 (~P3(f4(a2,a1,a1),f4(a1,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2596,2515,30])). % 181.01/180.87 cnf(2616,plain, % 181.01/180.87 (~P3(f4(a1,a2,a1),f4(a1,a2,a2))), % 181.01/180.87 inference(scs_inference,[],[2490,2596,2515,2586,30,12])). % 181.01/180.87 cnf(2617,plain, % 181.01/180.87 (E(f4(x26171,x26172,a1),f4(x26171,x26172,a2))), % 181.01/180.87 inference(rename_variables,[],[2586])). % 181.01/180.87 cnf(2618,plain, % 181.01/180.87 (P2(f4(a1,a2,a1),f4(a2,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2490,2534,2596,2515,2586,2617,30,12,15])). % 181.01/180.87 cnf(2623,plain, % 181.01/180.87 (~P3(f4(a1,a1,a1),f4(a1,a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2466,2582,2606,2586,30,12])). % 181.01/180.87 cnf(2627,plain, % 181.01/180.87 (E(f4(a2,a2,a1),f4(a1,a2,a2))), % 181.01/180.87 inference(scs_inference,[],[2466,2582,2599,2606,2589,2586,2074,2437,30,12,13,3])). % 181.01/180.87 cnf(2629,plain, % 181.01/180.87 (~P3(f4(a2,a2,a1),f4(a1,a1,a1))), % 181.01/180.87 inference(scs_inference,[],[2466,2582,2599,2606,2589,2586,2074,2437,30,12,13,3,2033])). % 181.01/180.87 cnf(2632,plain, % 181.01/180.87 (~P3(f4(a1,a1,a1),f4(a1,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2608,2623,30])). % 181.01/180.87 cnf(2642,plain, % 181.01/180.87 (P2(f4(a2,a2,x26421),f4(a1,a1,x26421))), % 181.01/180.87 inference(rename_variables,[],[2580])). % 181.01/180.87 cnf(2644,plain, % 181.01/180.87 (~P3(f4(a2,a2,a1),f4(a1,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2629,2632,2580,2000,30,12])). % 181.01/180.87 cnf(2650,plain, % 181.01/180.87 (P2(f4(a1,a2,x26501),f4(a1,a1,x26501))), % 181.01/180.87 inference(scs_inference,[],[2601,2616,2629,2632,2580,2642,2586,1856,2000,30,12,13,2129,14])). % 181.01/180.87 cnf(2654,plain, % 181.01/180.87 (E(f4(a2,a1,a1),f4(a1,a2,a2))), % 181.01/180.87 inference(scs_inference,[],[2627,2437,3])). % 181.01/180.87 cnf(2697,plain, % 181.01/180.87 (P3(f4(a2,x26971,f8(a6,a6)),f8(a6,a6))), % 181.01/180.87 inference(scs_inference,[],[2012,66,2,36])). % 181.01/180.87 cnf(2734,plain, % 181.01/180.87 (E(f3(a1,x27341),f3(a2,x27341))), % 181.01/180.87 inference(scs_inference,[],[1843,2,9])). % 181.01/180.87 cnf(2735,plain, % 181.01/180.87 (~P3(f3(a1,a1),f3(a2,a1))), % 181.01/180.87 inference(scs_inference,[],[2734,2408,12])). % 181.01/180.87 cnf(2736,plain, % 181.01/180.87 (E(f3(a1,x27361),f3(a2,x27361))), % 181.01/180.87 inference(rename_variables,[],[2734])). % 181.01/180.87 cnf(2738,plain, % 181.01/180.87 (E(f3(a1,x27381),f3(a2,x27381))), % 181.01/180.87 inference(rename_variables,[],[2734])). % 181.01/180.87 cnf(2739,plain, % 181.01/180.87 (E(f3(a1,a1),f3(a2,a2))), % 181.01/180.87 inference(scs_inference,[],[2734,2736,2738,2408,2407,12,13,3])). % 181.01/180.87 cnf(2753,plain, % 181.01/180.87 (E(f8(x27531,f3(a2,a2)),f8(x27531,f3(a1,a1)))), % 181.01/180.87 inference(scs_inference,[],[2739,2,5])). % 181.01/180.87 cnf(2879,plain, % 181.01/180.87 (P3(f3(f8(a9,a5),f8(a9,a7)),a5)), % 181.01/180.87 inference(scs_inference,[],[2152,29,38])). % 181.01/180.87 cnf(2880,plain, % 181.01/180.87 (P3(f3(f8(a9,a5),f8(a7,a9)),a9)), % 181.01/180.87 inference(scs_inference,[],[1821,29,39])). % 181.01/180.87 cnf(2881,plain, % 181.01/180.87 (P3(f3(f8(a5,a9),f8(a9,a7)),a9)), % 181.01/180.87 inference(scs_inference,[],[1819,29,38])). % 181.01/180.87 cnf(2882,plain, % 181.01/180.87 (P3(f3(f8(a9,a5),f8(a9,a7)),a9)), % 181.01/180.87 inference(scs_inference,[],[2152,29,39])). % 181.01/180.87 cnf(2884,plain, % 181.01/180.87 (P3(f3(f8(a5,a9),f8(a9,a7)),a5)), % 181.01/180.87 inference(scs_inference,[],[1819,29,39])). % 181.01/180.87 cnf(2885,plain, % 181.01/180.87 (P3(f8(f3(f8(a9,a5),f8(a9,a7)),f3(f8(a9,a5),f8(a9,a7))),f8(a9,a5))), % 181.01/180.87 inference(scs_inference,[],[2152,47,29,12])). % 181.01/180.87 cnf(2887,plain, % 181.01/180.87 (P3(f3(f8(a5,a9),f8(a9,a7)),f8(f8(a5,a9),f8(a5,a9)))), % 181.01/180.87 inference(scs_inference,[],[1819,47,29,13])). % 181.01/180.87 cnf(2889,plain, % 181.01/180.87 (~P2(f8(a9,a5),a1)), % 181.01/180.87 inference(scs_inference,[],[1821,41,29,30])). % 181.01/180.87 cnf(2890,plain, % 181.01/180.87 (~P2(f8(a9,a5),f8(a2,a2))), % 181.01/180.87 inference(scs_inference,[],[2889,1801,15])). % 181.01/180.87 cnf(2891,plain, % 181.01/180.87 (~P2(f8(a5,a9),a1)), % 181.01/180.87 inference(scs_inference,[],[2889,1801,22,15,14])). % 181.01/180.87 cnf(2894,plain, % 181.01/180.87 (~P2(f8(a5,a9),f8(a1,x28941))), % 181.01/180.87 inference(scs_inference,[],[2891,1830,15])). % 181.01/180.87 cnf(2896,plain, % 181.01/180.87 (~P2(f8(a5,a9),f8(x28961,a2))), % 181.01/180.87 inference(scs_inference,[],[2894,2190,15])). % 181.01/180.87 cnf(2900,plain, % 181.01/180.87 (~P2(f8(a9,a5),f8(x29001,a1))), % 181.01/180.87 inference(scs_inference,[],[2890,2230,15])). % 181.01/180.87 cnf(2902,plain, % 181.01/180.87 (~P3(f3(f8(a9,a5),f8(a7,a9)),a7)), % 181.01/180.87 inference(scs_inference,[],[2880,470])). % 181.01/180.87 cnf(2903,plain, % 181.01/180.87 (~E(f8(f8(a2,x29031),x29032),f8(a9,a5))), % 181.01/180.87 inference(scs_inference,[],[245,2900,29,14])). % 181.01/180.87 cnf(2904,plain, % 181.01/180.87 (~P3(f3(f8(a5,a9),f8(a9,a7)),f8(a9,a7))), % 181.01/180.87 inference(scs_inference,[],[1819,33])). % 181.01/180.87 cnf(2906,plain, % 181.01/180.87 (P3(f3(f8(a5,a9),f8(x29061,a2)),f8(a5,a9))), % 181.01/180.87 inference(scs_inference,[],[2896,1819,33,29])). % 181.01/180.87 cnf(2916,plain, % 181.01/180.87 (E(f8(f4(x29161,f8(a2,x29162),x29163),x29164),f8(f4(x29161,a2,x29163),x29164))), % 181.01/180.87 inference(scs_inference,[],[2697,2323,2896,1819,33,29,38,8,10,6,9,7,5,4])). % 181.01/180.87 cnf(2919,plain, % 181.01/180.87 (P3(f3(f8(a5,a9),f8(a9,a7)),f8(a5,a9))), % 181.01/180.87 inference(scs_inference,[],[2697,2323,2887,2896,1819,33,29,38,8,10,6,9,7,5,4,27,39])). % 181.01/180.87 cnf(2924,plain, % 181.01/180.87 (~E(f8(a6,a6),f8(f8(x29241,f8(a2,x29242)),x29243))), % 181.01/180.87 inference(scs_inference,[],[2903,2697,2323,2887,247,2896,1819,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32])). % 181.01/180.87 cnf(2925,plain, % 181.01/180.87 (~P3(x29251,f8(x29252,f8(a2,x29253)))), % 181.01/180.87 inference(rename_variables,[],[247])). % 181.01/180.87 cnf(2927,plain, % 181.01/180.87 (~E(a9,f8(x29271,a7))), % 181.01/180.87 inference(scs_inference,[],[2903,2697,2323,2902,2880,2887,247,2896,1819,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32,31])). % 181.01/180.87 cnf(2931,plain, % 181.01/180.87 (~P3(x29311,f8(x29312,f8(a2,x29313)))), % 181.01/180.87 inference(rename_variables,[],[247])). % 181.01/180.87 cnf(2939,plain, % 181.01/180.87 (P2(f4(a1,a2,x29391),f4(a1,a1,x29391))), % 181.01/180.87 inference(rename_variables,[],[2650])). % 181.01/180.87 cnf(2941,plain, % 181.01/180.87 (P3(f4(a2,x29411,f8(a6,a6)),f8(f8(a6,a6),f8(a6,a6)))), % 181.01/180.87 inference(scs_inference,[],[2650,2903,2697,2323,854,2902,2880,2887,247,2925,2931,2896,1819,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32,31,35,36,30,40])). % 181.01/180.87 cnf(2943,plain, % 181.01/180.87 (P2(f4(a1,a2,f8(x29431,a1)),f4(a1,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2650,2939,2903,2697,2323,2324,854,2902,2880,2887,247,2925,2931,2896,1819,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32,31,35,36,30,40,15])). % 181.01/180.87 cnf(2946,plain, % 181.01/180.87 (~P2(f8(f8(a5,a9),f8(a5,a9)),f8(x29461,a2))), % 181.01/180.87 inference(scs_inference,[],[2650,2939,2903,2697,2323,2324,854,2902,2880,2887,247,2925,2931,2896,1819,21,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32,31,35,36,30,40,15,14])). % 181.01/180.87 cnf(2947,plain, % 181.01/180.87 (E(f8(x29471,x29471),x29471)), % 181.01/180.87 inference(rename_variables,[],[21])). % 181.01/180.87 cnf(2953,plain, % 181.01/180.87 (~E(a7,f8(a9,a9))), % 181.01/180.87 inference(scs_inference,[],[1887,2546,2548,2650,2939,2903,2697,2323,2324,2342,854,2902,2880,2265,2887,247,2925,2931,2896,1819,21,2947,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32,31,35,36,30,40,15,14,12,13,3,34])). % 181.01/180.87 cnf(2958,plain, % 181.01/180.87 (~P3(f3(f8(a9,a5),f8(a7,a9)),f8(a7,x29581))), % 181.01/180.87 inference(scs_inference,[],[1821,29,1586])). % 181.01/180.87 cnf(2959,plain, % 181.01/180.87 (~P3(f3(f8(a9,a5),f8(a9,a7)),f8(a9,a7))), % 181.01/180.87 inference(scs_inference,[],[2152,33])). % 181.01/180.87 cnf(2961,plain, % 181.01/180.87 (P3(f3(f8(f8(a5,a9),f8(a5,a9)),f8(x29611,a2)),f8(f8(a5,a9),f8(a5,a9)))), % 181.01/180.87 inference(scs_inference,[],[2946,2152,33,29])). % 181.01/180.87 cnf(2979,plain, % 181.01/180.87 (~E(f8(a5,a9),f8(f8(a9,a7),x29791))), % 181.01/180.87 inference(scs_inference,[],[2953,2904,2919,2906,2341,2946,2879,2941,2152,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32])). % 181.01/180.87 cnf(2985,plain, % 181.01/180.87 (~P3(x29851,f8(f8(x29852,a2),x29853))), % 181.01/180.87 inference(rename_variables,[],[268])). % 181.01/180.87 cnf(2995,plain, % 181.01/180.87 (~P2(f8(f8(a5,a9),f8(a5,a9)),f8(x29951,f8(x29952,a2)))), % 181.01/180.87 inference(scs_inference,[],[2613,2953,2904,2919,2906,2341,2946,2322,2943,2879,2941,268,2985,2152,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32,31,35,36,30,40,15])). % 181.01/180.87 cnf(2999,plain, % 181.01/180.87 (~P3(f4(a2,f8(a1,x29991),a1),f4(a2,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[2594,2613,2953,2904,2919,2906,2341,2946,2322,2943,2879,2941,268,2985,2152,20,33,29,38,8,10,6,9,7,5,4,27,39,28,2,32,31,35,36,30,40,15,14,12])). % 181.01/180.87 cnf(3028,plain, % 181.01/180.87 (~P3(x30281,f8(f8(a2,x30282),x30283))), % 181.01/180.87 inference(rename_variables,[],[245])). % 181.01/180.87 cnf(3034,plain, % 181.01/180.87 (~P3(x30341,f8(f8(a2,x30342),x30343))), % 181.01/180.87 inference(rename_variables,[],[245])). % 181.01/180.87 cnf(3042,plain, % 181.01/180.87 (P3(f3(f8(a5,a9),f8(a9,a7)),f8(a9,a9))), % 181.01/180.87 inference(scs_inference,[],[2618,2927,2959,2369,2999,2881,2882,2995,2961,2885,245,3028,3034,24,33,29,38,8,10,9,6,7,5,4,39,28,2,32,31,35,36,30,40])). % 181.01/180.87 cnf(3074,plain, % 181.01/180.87 (E(f8(x30741,x30741),x30741)), % 181.01/180.87 inference(rename_variables,[],[21])). % 181.01/180.87 cnf(3076,plain, % 181.01/180.87 (~P3(x30761,f8(a2,x30762))), % 181.01/180.87 inference(rename_variables,[],[147])). % 181.01/180.87 cnf(3085,plain, % 181.01/180.87 (~P3(f3(f8(a5,a9),f8(a9,a7)),a7)), % 181.01/180.87 inference(scs_inference,[],[22,47,147,21,1858,2000,128,20,2230,159,2055,2881,1901,92,2880,2904,71,2479,2979,2958,2,28,39,4,38,29,2161,3,13,12,14,15,11,40])). % 181.01/180.87 cnf(3088,plain, % 181.01/180.87 (~P3(x30881,f8(a2,x30882))), % 181.01/180.87 inference(rename_variables,[],[147])). % 181.01/180.87 cnf(3091,plain, % 181.01/180.87 (~P3(x30911,a1)), % 181.01/180.87 inference(rename_variables,[],[41])). % 181.01/180.87 cnf(3096,plain, % 181.01/180.87 (~P3(x30961,f8(f8(x30962,f8(a2,x30963)),f8(x30962,f8(a2,x30963))))), % 181.01/180.87 inference(scs_inference,[],[22,47,147,3076,3088,41,3091,21,3074,1858,2000,128,20,2230,159,2055,2881,1901,92,2880,2904,2243,71,2479,2979,2958,2,28,39,4,38,29,2161,3,13,12,14,15,11,40,30,36,35,31])). % 181.01/180.87 cnf(3123,plain, % 181.01/180.87 (E(f8(x31231,x31231),x31231)), % 181.01/180.87 inference(rename_variables,[],[21])). % 181.01/180.87 cnf(3125,plain, % 181.01/180.87 (~P3(x31251,f8(a2,x31252))), % 181.01/180.87 inference(rename_variables,[],[147])). % 181.01/180.87 cnf(3128,plain, % 181.01/180.87 (E(x31281,f8(x31281,x31281))), % 181.01/180.87 inference(rename_variables,[],[47])). % 181.01/180.87 cnf(3136,plain, % 181.01/180.87 (~P3(x31361,f8(a2,x31362))), % 181.01/180.87 inference(rename_variables,[],[147])). % 181.01/180.87 cnf(3139,plain, % 181.01/180.87 (~E(f8(a2,x31391),f8(a9,a5))), % 181.01/180.87 inference(rename_variables,[],[2258])). % 181.01/180.87 cnf(3140,plain, % 181.01/180.87 (~P3(x31401,f8(a2,x31402))), % 181.01/180.87 inference(rename_variables,[],[147])). % 181.01/180.87 cnf(3150,plain, % 181.01/180.87 (P3(f8(f4(a5,a9,a1),f4(a5,a9,a1)),f8(f8(f8(a7,a7),f8(a7,a7)),f8(f8(a7,a7),f8(a7,a7))))), % 181.01/180.87 inference(scs_inference,[],[47,3128,147,3125,3136,3140,21,3123,1857,159,128,2627,119,2234,97,1901,2904,1971,236,2258,3139,2887,2594,2902,2735,64,2882,2959,2490,2924,2423,2450,2,28,39,4,38,29,2161,3,13,12,14,15,11,40,30,36,35,31,32,34])). % 181.01/180.87 cnf(3161,plain, % 181.01/180.87 (~P3(x31611,f8(x31612,f8(x31613,f8(x31614,a1))))), % 181.01/180.87 inference(scs_inference,[],[2492,71,2882,2,28,39,38])). % 181.01/180.87 cnf(3382,plain, % 181.01/180.87 (E(x33821,f8(x33821,x33821))), % 181.01/180.87 inference(rename_variables,[],[47])). % 181.01/180.87 cnf(3386,plain, % 181.01/180.87 (E(f8(f4(a2,a2,a1),f4(a2,a2,a1)),f4(a1,a1,a2))), % 181.01/180.87 inference(scs_inference,[],[47,21,128,2589,2074,2606,2139,2623,3150,3161,2305,39,29,2,28,38,15,11,3])). % 181.01/180.87 cnf(3389,plain, % 181.01/180.87 (E(x33891,f8(x33891,x33891))), % 181.01/180.87 inference(rename_variables,[],[47])). % 181.01/180.87 cnf(3396,plain, % 181.01/180.87 (~E(f8(a9,a5),f8(x33961,a2))), % 181.01/180.87 inference(rename_variables,[],[2264])). % 181.01/180.87 cnf(3397,plain, % 181.01/180.87 (~P3(x33971,f8(a2,x33972))), % 181.01/180.87 inference(rename_variables,[],[147])). % 181.01/180.87 cnf(3404,plain, % 181.01/180.87 (P3(f4(x34041,a2,f8(a9,a5)),f8(a9,a5))), % 181.01/180.87 inference(scs_inference,[],[47,3382,3389,147,3397,21,66,128,2589,2074,2094,2887,1994,2606,2139,2919,2623,2475,2264,3396,3150,2753,2916,3161,2305,39,29,2,28,38,15,11,3,14,12,32,36,30,31,35])). % 181.01/180.87 cnf(3428,plain, % 181.01/180.87 (P1(f8(f8(x34281,a2),x34282))), % 181.01/180.87 inference(scs_inference,[],[47,21,17,2654,2020,2623,2451,2735,3404,3096,2306,2,39,29,38,28,3,15,11])). % 181.01/180.87 cnf(5804,plain, % 181.01/180.87 ($false), % 181.01/180.87 inference(scs_inference,[],[18,19,21,3386,3085,3428,2644,3042,2884,8,10,6,9,7,5,25,4,13,34,30]), % 181.01/180.87 ['proof']). % 181.01/180.87 % SZS output end Proof % 181.01/180.87 % Total time :180.140000s %------------------------------------------------------------------------------