%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU132+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 : n019.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:13 EDT 2024 % Result : Theorem 202.11s 202.12s % Output : CNFRefutation 202.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU132+1 : TPTP v8.2.0. Released v3.3.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 11:25:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.52/0.58 start to proof:theBenchmark % 202.11/202.09 %------------------------------------------- % 202.11/202.09 % File :CSE---1.7 % 202.11/202.09 % Problem :theBenchmark % 202.11/202.09 % Transform :cnf % 202.11/202.09 % Format :tptp:raw % 202.11/202.09 % Command :java -jar mcs_scs.jar %d %s % 202.11/202.09 % 202.11/202.09 % Result :Theorem 201.420000s % 202.11/202.09 % Output :CNFRefutation 201.420000s % 202.11/202.09 %------------------------------------------- % 202.11/202.11 %------------------------------------------------------------------------------ % 202.11/202.11 % File : SEU132+1 : TPTP v8.2.0. Released v3.3.0. % 202.11/202.11 % Domain : Set theory % 202.11/202.11 % Problem : MPTP bushy problem t33_xboole_1 % 202.11/202.11 % Version : [Urb07] axioms : Especial. % 202.11/202.11 % English : % 202.11/202.11 % 202.11/202.11 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 202.11/202.11 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 202.11/202.11 % Source : [Urb07] % 202.11/202.11 % Names : bushy-t33_xboole_1 [Urb07] % 202.11/202.11 % 202.11/202.11 % Status : Theorem % 202.11/202.11 % Rating : 0.25 v8.2.0, 0.31 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.20 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.32 v6.1.0, 0.50 v6.0.0, 0.30 v5.5.0, 0.41 v5.4.0, 0.46 v5.3.0, 0.56 v5.2.0, 0.35 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.43 v4.0.0, 0.46 v3.7.0, 0.50 v3.5.0, 0.47 v3.4.0, 0.53 v3.3.0 % 202.11/202.11 % Syntax : Number of formulae : 15 ( 8 unt; 0 def) % 202.11/202.11 % Number of atoms : 26 ( 5 equ) % 202.11/202.11 % Maximal formula atoms : 4 ( 1 avg) % 202.11/202.11 % Number of connectives : 17 ( 6 ~; 0 |; 4 &) % 202.11/202.11 % ( 3 <=>; 4 =>; 0 <=; 0 <~>) % 202.11/202.11 % Maximal formula depth : 9 ( 4 avg) % 202.11/202.11 % Maximal term depth : 2 ( 1 avg) % 202.11/202.11 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 202.11/202.11 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 202.11/202.11 % Number of variables : 23 ( 21 !; 2 ?) % 202.11/202.11 % SPC : FOF_THM_RFO_SEQ % 202.11/202.11 % 202.11/202.11 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 202.11/202.11 % library, www.mizar.org % 202.11/202.11 %------------------------------------------------------------------------------ % 202.11/202.11 fof(antisymmetry_r2_hidden,axiom, % 202.11/202.12 ! [A,B] : % 202.11/202.12 ( in(A,B) % 202.11/202.12 => ~ in(B,A) ) ). % 202.11/202.12 % 202.11/202.12 fof(d3_tarski,axiom, % 202.11/202.12 ! [A,B] : % 202.11/202.12 ( subset(A,B) % 202.11/202.12 <=> ! [C] : % 202.11/202.12 ( in(C,A) % 202.11/202.12 => in(C,B) ) ) ). % 202.11/202.12 % 202.11/202.12 fof(d4_xboole_0,axiom, % 202.11/202.12 ! [A,B,C] : % 202.11/202.12 ( C = set_difference(A,B) % 202.11/202.12 <=> ! [D] : % 202.11/202.12 ( in(D,C) % 202.11/202.12 <=> ( in(D,A) % 202.11/202.12 & ~ in(D,B) ) ) ) ). % 202.11/202.12 % 202.11/202.12 fof(dt_k1_xboole_0,axiom, % 202.11/202.12 $true ). % 202.11/202.12 % 202.11/202.12 fof(dt_k4_xboole_0,axiom, % 202.11/202.12 $true ). % 202.11/202.12 % 202.11/202.12 fof(fc1_xboole_0,axiom, % 202.11/202.12 empty(empty_set) ). % 202.11/202.12 % 202.11/202.12 fof(rc1_xboole_0,axiom, % 202.11/202.12 ? [A] : empty(A) ). % 202.11/202.12 % 202.11/202.12 fof(rc2_xboole_0,axiom, % 202.11/202.12 ? [A] : ~ empty(A) ). % 202.11/202.12 % 202.11/202.12 fof(reflexivity_r1_tarski,axiom, % 202.11/202.12 ! [A,B] : subset(A,A) ). % 202.11/202.12 % 202.11/202.12 fof(t33_xboole_1,conjecture, % 202.11/202.12 ! [A,B,C] : % 202.11/202.12 ( subset(A,B) % 202.11/202.12 => subset(set_difference(A,C),set_difference(B,C)) ) ). % 202.11/202.12 % 202.11/202.12 fof(t3_boole,axiom, % 202.11/202.12 ! [A] : set_difference(A,empty_set) = A ). % 202.11/202.12 % 202.11/202.12 fof(t4_boole,axiom, % 202.11/202.12 ! [A] : set_difference(empty_set,A) = empty_set ). % 202.11/202.12 % 202.11/202.12 fof(t6_boole,axiom, % 202.11/202.12 ! [A] : % 202.11/202.12 ( empty(A) % 202.11/202.12 => A = empty_set ) ). % 202.11/202.12 % 202.11/202.12 fof(t7_boole,axiom, % 202.11/202.12 ! [A,B] : % 202.11/202.12 ~ ( in(A,B) % 202.11/202.12 & empty(B) ) ). % 202.11/202.12 % 202.11/202.12 fof(t8_boole,axiom, % 202.11/202.12 ! [A,B] : % 202.11/202.12 ~ ( empty(A) % 202.11/202.12 & A != B % 202.11/202.12 & empty(B) ) ). % 202.11/202.12 % 202.11/202.12 %------------------------------------------------------------------------------ % 202.11/202.12 %------------------------------------------- % 202.11/202.12 % Proof found % 202.11/202.12 % SZS status Theorem for theBenchmark % 202.11/202.12 % SZS output start Proof % 202.16/202.14 %ClaNum:36(EqnAxiom:15) % 202.16/202.14 %VarNum:94(SingletonVarNum:38) % 202.16/202.14 %MaxLitNum:4 % 202.16/202.14 %MaxfuncDepth:1 % 202.16/202.14 %SharedTerms:13 % 202.16/202.14 %goalClause: 18 23 % 202.16/202.14 %singleGoalClaCount:2 % 202.16/202.14 [16]P1(a1) % 202.16/202.14 [17]P1(a2) % 202.16/202.14 [18]P2(a5,a7) % 202.16/202.14 [22]~P1(a6) % 202.16/202.14 [23]~P2(f8(a5,a9),f8(a7,a9)) % 202.16/202.14 [21]P2(x211,x211) % 202.16/202.14 [19]E(f8(a1,x191),a1) % 202.16/202.14 [20]E(f8(x201,a1),x201) % 202.16/202.14 [24]~P1(x241)+E(x241,a1) % 202.16/202.14 [26]~P1(x261)+~P3(x262,x261) % 202.16/202.14 [27]~P3(x272,x271)+~P3(x271,x272) % 202.16/202.14 [28]P2(x281,x282)+P3(f3(x281,x282),x281) % 202.16/202.14 [33]P2(x331,x332)+~P3(f3(x331,x332),x332) % 202.16/202.14 [25]~P1(x252)+~P1(x251)+E(x251,x252) % 202.16/202.14 [29]~P2(x293,x292)+P3(x291,x292)+~P3(x291,x293) % 202.16/202.14 [34]P3(f4(x342,x343,x341),x341)+P3(f4(x342,x343,x341),x342)+E(x341,f8(x342,x343)) % 202.16/202.14 [35]P3(f4(x352,x353,x351),x351)+~P3(f4(x352,x353,x351),x353)+E(x351,f8(x352,x353)) % 202.16/202.14 [30]~P3(x301,x303)+P3(x301,x302)+~E(x303,f8(x302,x304)) % 202.16/202.14 [31]~P3(x314,x313)+~P3(x314,x311)+~E(x311,f8(x312,x313)) % 202.16/202.14 [36]P3(f4(x362,x363,x361),x363)+~P3(f4(x362,x363,x361),x361)+~P3(f4(x362,x363,x361),x362)+E(x361,f8(x362,x363)) % 202.16/202.14 [32]~P3(x321,x324)+P3(x321,x322)+P3(x321,x323)+~E(x322,f8(x324,x323)) % 202.16/202.14 %EqnAxiom % 202.16/202.14 [1]E(x11,x11) % 202.16/202.14 [2]E(x22,x21)+~E(x21,x22) % 202.16/202.14 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 202.16/202.14 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 202.16/202.14 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 202.16/202.14 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 202.16/202.14 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 202.16/202.14 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 202.16/202.14 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 202.16/202.14 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 202.16/202.14 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 202.16/202.14 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 202.16/202.14 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 202.16/202.14 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 202.16/202.14 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 202.16/202.14 % 202.16/202.14 %------------------------------------------- % 202.16/202.18 cnf(37,plain, % 202.16/202.18 (~P3(x371,f8(x372,x373))+P3(x371,x372)), % 202.16/202.18 inference(equality_inference,[],[30])). % 202.16/202.18 cnf(38,plain, % 202.16/202.18 (~P3(x381,x382)+~P3(x381,f8(x383,x382))), % 202.16/202.18 inference(equality_inference,[],[31])). % 202.16/202.18 cnf(39,plain, % 202.16/202.18 (~P3(x391,x392)+P3(x391,f8(x392,x393))+P3(x391,x393)), % 202.16/202.18 inference(equality_inference,[],[32])). % 202.16/202.18 cnf(40,plain, % 202.16/202.18 (~P3(x401,a1)), % 202.16/202.18 inference(scs_inference,[],[16,26])). % 202.16/202.18 cnf(42,plain, % 202.16/202.18 (~P3(x421,f8(a1,x422))), % 202.16/202.18 inference(scs_inference,[],[16,26,37])). % 202.16/202.18 cnf(44,plain, % 202.16/202.18 (E(x441,f8(x441,a1))), % 202.16/202.18 inference(scs_inference,[],[20,16,26,37,2])). % 202.16/202.18 cnf(45,plain, % 202.16/202.18 (P2(f8(a5,a1),a7)), % 202.16/202.18 inference(scs_inference,[],[18,20,16,26,37,2,14])). % 202.16/202.18 cnf(46,plain, % 202.16/202.18 (~E(f8(a5,a9),f8(a7,a9))), % 202.16/202.18 inference(scs_inference,[],[18,23,21,20,16,26,37,2,14,15])). % 202.16/202.18 cnf(48,plain, % 202.16/202.18 (P2(a1,x481)), % 202.16/202.18 inference(scs_inference,[],[18,23,21,20,16,26,37,2,14,15,28])). % 202.16/202.18 cnf(50,plain, % 202.16/202.18 (~E(a5,a7)), % 202.16/202.18 inference(scs_inference,[],[18,23,21,20,16,26,37,2,14,15,28,4])). % 202.16/202.18 cnf(56,plain, % 202.16/202.18 (~P3(x561,a2)), % 202.16/202.18 inference(scs_inference,[],[17,26])). % 202.16/202.18 cnf(58,plain, % 202.16/202.18 (~P3(x581,f8(f8(a1,x582),x583))), % 202.16/202.18 inference(scs_inference,[],[42,17,26,37])). % 202.16/202.18 cnf(60,plain, % 202.16/202.18 (E(a1,f8(a1,x601))), % 202.16/202.18 inference(scs_inference,[],[42,19,17,26,37,2])). % 202.16/202.18 cnf(61,plain, % 202.16/202.18 (P2(f8(a1,x611),x612)), % 202.16/202.18 inference(scs_inference,[],[42,19,17,26,37,2,28])). % 202.16/202.18 cnf(62,plain, % 202.16/202.18 (~P3(x621,f8(a1,x622))), % 202.16/202.18 inference(rename_variables,[],[42])). % 202.16/202.18 cnf(64,plain, % 202.16/202.18 (E(f8(a1,x641),f8(a1,a1))), % 202.16/202.18 inference(scs_inference,[],[44,42,19,17,26,37,2,28,3])). % 202.16/202.18 cnf(65,plain, % 202.16/202.18 (E(x651,f8(x651,a1))), % 202.16/202.18 inference(rename_variables,[],[44])). % 202.16/202.18 cnf(67,plain, % 202.16/202.18 (E(x671,f8(x671,a1))), % 202.16/202.18 inference(rename_variables,[],[44])). % 202.16/202.18 cnf(68,plain, % 202.16/202.18 (~E(a1,f8(a5,a9))), % 202.16/202.18 inference(scs_inference,[],[23,48,44,65,42,19,16,17,26,37,2,28,3,11,14])). % 202.16/202.18 cnf(70,plain, % 202.16/202.18 (P2(a5,f8(a7,a1))), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,42,19,16,17,26,37,2,28,3,11,14,15])). % 202.16/202.18 cnf(71,plain, % 202.16/202.18 (E(x711,f8(x711,a1))), % 202.16/202.18 inference(rename_variables,[],[44])). % 202.16/202.18 cnf(74,plain, % 202.16/202.18 (~P3(f4(a5,a9,a1),a9)), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,42,40,50,19,16,17,26,37,2,28,3,11,14,15,25,35])). % 202.16/202.18 cnf(75,plain, % 202.16/202.18 (~P3(x751,a1)), % 202.16/202.18 inference(rename_variables,[],[40])). % 202.16/202.18 cnf(77,plain, % 202.16/202.18 (P3(f4(a5,a9,a1),a5)), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,42,40,75,50,19,16,17,26,37,2,28,3,11,14,15,25,35,34])). % 202.16/202.18 cnf(80,plain, % 202.16/202.18 (P3(f4(a5,a9,a1),f8(a5,f8(a1,x801)))), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,42,62,40,75,50,19,16,17,26,37,2,28,3,11,14,15,25,35,34,39])). % 202.16/202.18 cnf(81,plain, % 202.16/202.18 (~P3(x811,f8(a1,x812))), % 202.16/202.18 inference(rename_variables,[],[42])). % 202.16/202.18 cnf(86,plain, % 202.16/202.18 (~P3(a5,f4(a5,a9,a1))), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,42,62,40,75,50,19,20,16,17,26,37,2,28,3,11,14,15,25,35,34,39,31,27])). % 202.16/202.18 cnf(88,plain, % 202.16/202.18 (~P3(f4(a5,a9,a1),f8(x881,a5))), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,42,62,40,75,50,19,20,16,17,26,37,2,28,3,11,14,15,25,35,34,39,31,27,38])). % 202.16/202.18 cnf(90,plain, % 202.16/202.18 (P3(f4(a5,a9,a1),a7)), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,42,62,40,75,50,19,20,16,17,26,37,2,28,3,11,14,15,25,35,34,39,31,27,38,29])). % 202.16/202.18 cnf(92,plain, % 202.16/202.18 (P3(f8(f4(a5,a9,a1),a1),a5)), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,71,42,62,40,75,50,19,20,16,17,26,37,2,28,3,11,14,15,25,35,34,39,31,27,38,29,12])). % 202.16/202.18 cnf(94,plain, % 202.16/202.18 (~E(a5,f8(a1,x941))), % 202.16/202.18 inference(scs_inference,[],[18,23,48,44,65,67,71,42,62,81,40,75,50,19,20,16,17,26,37,2,28,3,11,14,15,25,35,34,39,31,27,38,29,12,13])). % 202.16/202.18 cnf(98,plain, % 202.16/202.18 (~P3(a7,f4(a5,a9,a1))), % 202.16/202.18 inference(scs_inference,[],[90,27])). % 202.16/202.18 cnf(100,plain, % 202.16/202.18 (~P3(f4(a5,a9,a1),f8(x1001,a7))), % 202.16/202.18 inference(scs_inference,[],[90,27,38])). % 202.16/202.18 cnf(102,plain, % 202.16/202.18 (P2(a2,x1021)), % 202.16/202.18 inference(scs_inference,[],[90,56,27,38,28])). % 202.16/202.18 cnf(105,plain, % 202.16/202.18 (~P3(f4(a5,a9,a1),f8(f8(x1051,a5),x1052))), % 202.16/202.18 inference(scs_inference,[],[90,88,56,27,38,28,37])). % 202.16/202.18 cnf(108,plain, % 202.16/202.18 (P3(f8(f4(a5,a9,a1),a1),a7)), % 202.16/202.18 inference(scs_inference,[],[18,90,88,64,56,92,27,38,28,37,2,29])). % 202.16/202.18 cnf(110,plain, % 202.16/202.18 (~P1(f8(a5,a9))), % 202.16/202.18 inference(scs_inference,[],[18,90,68,88,64,56,92,16,27,38,28,37,2,29,25])). % 202.16/202.18 cnf(112,plain, % 202.16/202.18 (P3(f4(a1,x1121,a5),a5)), % 202.16/202.18 inference(scs_inference,[],[18,90,68,88,64,56,94,92,40,16,27,38,28,37,2,29,25,34])). % 202.16/202.18 cnf(115,plain, % 202.16/202.18 (~E(a7,f8(f8(a1,x1151),x1152))), % 202.16/202.18 inference(scs_inference,[],[18,90,68,58,88,64,56,94,92,40,16,27,38,28,37,2,29,25,34,13])). % 202.16/202.18 cnf(117,plain, % 202.16/202.18 (P3(f4(a5,a9,a1),f8(a7,f8(x1171,a5)))), % 202.16/202.18 inference(scs_inference,[],[18,90,68,58,88,64,56,94,92,40,16,27,38,28,37,2,29,25,34,13,39])). % 202.16/202.18 cnf(119,plain, % 202.16/202.18 (~E(a5,a1)), % 202.16/202.18 inference(scs_inference,[],[18,90,68,58,88,64,56,60,94,92,40,16,27,38,28,37,2,29,25,34,13,39,3])). % 202.16/202.18 cnf(120,plain, % 202.16/202.18 (E(a1,f8(a1,x1201))), % 202.16/202.18 inference(rename_variables,[],[60])). % 202.16/202.18 cnf(121,plain, % 202.16/202.18 (P3(f8(f4(a1,x1211,a5),a1),a5)), % 202.16/202.18 inference(scs_inference,[],[18,90,68,58,88,64,56,60,94,92,44,40,16,27,38,28,37,2,29,25,34,13,39,3,12])). % 202.16/202.18 cnf(122,plain, % 202.16/202.18 (E(x1221,f8(x1221,a1))), % 202.16/202.18 inference(rename_variables,[],[44])). % 202.16/202.18 cnf(123,plain, % 202.16/202.18 (P1(f8(a1,x1231))), % 202.16/202.18 inference(scs_inference,[],[18,90,68,58,88,64,56,60,120,94,92,44,40,16,27,38,28,37,2,29,25,34,13,39,3,12,11])). % 202.16/202.18 cnf(127,plain, % 202.16/202.18 (P2(f8(a5,a1),f8(a7,a1))), % 202.16/202.18 inference(scs_inference,[],[18,45,90,68,58,88,64,56,60,120,94,92,44,122,40,20,16,27,38,28,37,2,29,25,34,13,39,3,12,11,31,15])). % 202.16/202.18 cnf(129,plain, % 202.16/202.18 (~E(f8(a1,x1291),f8(a5,a9))), % 202.16/202.18 inference(scs_inference,[],[18,23,61,45,90,68,58,88,64,56,60,120,94,92,44,122,40,20,16,27,38,28,37,2,29,25,34,13,39,3,12,11,31,15,14])). % 202.16/202.18 cnf(143,plain, % 202.16/202.18 (P3(f4(a1,x1431,a5),a7)), % 202.16/202.18 inference(scs_inference,[],[18,108,100,112,27,37,38,29])). % 202.16/202.18 cnf(145,plain, % 202.16/202.18 (P3(f4(a5,a9,f8(a1,x1451)),a5)), % 202.16/202.18 inference(scs_inference,[],[18,108,129,100,112,42,27,37,38,29,34])). % 202.16/202.18 cnf(146,plain, % 202.16/202.18 (~E(f8(a1,x1461),f8(a5,a9))), % 202.16/202.18 inference(rename_variables,[],[129])). % 202.16/202.18 cnf(147,plain, % 202.16/202.18 (~P3(x1471,f8(a1,x1472))), % 202.16/202.18 inference(rename_variables,[],[42])). % 202.16/202.18 cnf(149,plain, % 202.16/202.18 (P3(f4(a5,a9,a1),f8(a7,f8(x1491,a7)))), % 202.16/202.18 inference(scs_inference,[],[18,108,129,90,100,112,42,27,37,38,29,34,39])). % 202.16/202.18 cnf(151,plain, % 202.16/202.18 (~E(a7,f8(f8(x1511,a5),x1512))), % 202.16/202.18 inference(scs_inference,[],[18,108,129,90,105,100,112,42,27,37,38,29,34,39,13])). % 202.16/202.18 cnf(152,plain, % 202.16/202.18 (~P3(f4(a5,a9,f8(a1,x1521)),a9)), % 202.16/202.18 inference(scs_inference,[],[18,108,129,146,90,105,100,112,42,147,27,37,38,29,34,39,13,35])). % 202.16/202.18 cnf(156,plain, % 202.16/202.18 (~E(a7,f8(a1,x1561))), % 202.16/202.18 inference(scs_inference,[],[18,108,129,146,90,105,100,115,112,44,42,147,27,37,38,29,34,39,13,35,3])). % 202.16/202.18 cnf(157,plain, % 202.16/202.18 (E(x1571,f8(x1571,a1))), % 202.16/202.18 inference(rename_variables,[],[44])). % 202.16/202.18 cnf(159,plain, % 202.16/202.18 (P3(f8(f4(a1,x1591,a5),a1),a7)), % 202.16/202.18 inference(scs_inference,[],[18,108,129,146,90,105,100,115,112,44,157,42,147,27,37,38,29,34,39,13,35,3,12])). % 202.16/202.18 cnf(160,plain, % 202.16/202.18 (E(x1601,f8(x1601,a1))), % 202.16/202.18 inference(rename_variables,[],[44])). % 202.16/202.18 cnf(162,plain, % 202.16/202.18 (E(x1621,f8(x1621,a1))), % 202.16/202.18 inference(rename_variables,[],[44])). % 202.16/202.18 cnf(163,plain, % 202.16/202.18 (P2(f8(a5,a1),f8(f8(a7,a1),a1))), % 202.16/202.18 inference(scs_inference,[],[18,127,108,129,146,90,105,100,115,112,44,157,160,162,42,147,27,37,38,29,34,39,13,35,3,12,14,15])). % 202.16/202.18 cnf(170,plain, % 202.16/202.18 (~P3(f4(a1,x1701,a5),f8(x1702,a7))), % 202.16/202.18 inference(scs_inference,[],[143,27,38])). % 202.16/202.18 cnf(172,plain, % 202.16/202.18 (~P3(x1721,f8(a2,x1722))), % 202.16/202.18 inference(scs_inference,[],[143,56,27,38,37])). % 202.16/202.18 cnf(175,plain, % 202.16/202.18 (E(f8(x1751,a1),x1751)), % 202.16/202.18 inference(rename_variables,[],[20])). % 202.16/202.18 cnf(177,plain, % 202.16/202.18 (P3(f4(a5,a9,f8(a1,x1771)),a7)), % 202.16/202.18 inference(scs_inference,[],[18,143,20,56,145,27,38,37,30,29])). % 202.16/202.18 cnf(180,plain, % 202.16/202.18 (E(f8(x1801,a1),x1801)), % 202.16/202.18 inference(rename_variables,[],[20])). % 202.16/202.18 cnf(182,plain, % 202.16/202.18 (P3(f4(a1,x1821,a7),a7)), % 202.16/202.18 inference(scs_inference,[],[18,143,20,175,56,40,156,145,27,38,37,30,29,31,34])). % 202.16/202.18 cnf(185,plain, % 202.16/202.18 (~P1(a7)), % 202.16/202.18 inference(scs_inference,[],[18,143,20,175,56,40,156,145,123,27,38,37,30,29,31,34,25])). % 202.16/202.18 cnf(186,plain, % 202.16/202.18 (~E(a7,f8(a1,x1861))), % 202.16/202.18 inference(rename_variables,[],[156])). % 202.16/202.18 cnf(188,plain, % 202.16/202.18 (P3(f4(a1,x1881,a5),f8(a7,a2))), % 202.16/202.18 inference(scs_inference,[],[18,143,20,175,56,40,156,145,123,27,38,37,30,29,31,34,25,39])). % 202.16/202.18 cnf(189,plain, % 202.16/202.18 (~P3(x1891,a2)), % 202.16/202.18 inference(rename_variables,[],[56])). % 202.16/202.18 cnf(195,plain, % 202.16/202.18 (P3(f8(f4(a1,x1951,a7),a1),a7)), % 202.16/202.18 inference(scs_inference,[],[18,143,60,20,175,56,189,40,156,186,145,44,123,27,38,37,30,29,31,34,25,39,3,13,12])). % 202.16/202.18 cnf(197,plain, % 202.16/202.18 (P2(a5,f8(f8(a7,a1),a1))), % 202.16/202.18 inference(scs_inference,[],[18,163,143,60,20,175,180,56,189,40,156,186,145,44,123,27,38,37,30,29,31,34,25,39,3,13,12,14])). % 202.16/202.18 cnf(206,plain, % 202.16/202.18 (P2(f8(a2,x2061),x2062)), % 202.16/202.18 inference(scs_inference,[],[177,172,27,28])). % 202.16/202.18 cnf(209,plain, % 202.16/202.18 (~P3(f4(a5,a9,a1),f8(a9,x2091))), % 202.16/202.18 inference(scs_inference,[],[177,74,172,27,28,37])). % 202.16/202.18 cnf(216,plain, % 202.16/202.18 (P3(f4(f8(a1,x2161),x2162,a7),a7)), % 202.16/202.18 inference(scs_inference,[],[177,42,40,74,172,115,27,28,37,38,39,34])). % 202.16/202.18 cnf(218,plain, % 202.16/202.18 (~P3(x2181,f8(a1,x2182))), % 202.16/202.18 inference(rename_variables,[],[42])). % 202.16/202.18 cnf(222,plain, % 202.16/202.18 (~E(f8(a7,f8(x2221,a7)),f8(a1,x2222))), % 202.16/202.18 inference(scs_inference,[],[46,177,20,42,218,40,74,172,149,115,27,28,37,38,39,34,3,13])). % 202.16/202.18 cnf(226,plain, % 202.16/202.18 (~E(a2,f8(a5,a9))), % 202.16/202.18 inference(scs_inference,[],[23,46,102,177,20,42,218,40,74,172,149,188,115,44,27,28,37,38,39,34,3,13,12,14])). % 202.16/202.18 cnf(230,plain, % 202.16/202.18 (~P3(f4(a5,a9,a2),a9)), % 202.16/202.18 inference(scs_inference,[],[23,46,102,177,20,42,218,40,56,74,172,149,188,115,44,123,27,28,37,38,39,34,3,13,12,14,25,35])). % 202.16/202.18 cnf(246,plain, % 202.16/202.18 (P3(f4(a5,a9,a2),a5)), % 202.16/202.18 inference(scs_inference,[],[226,108,121,40,56,209,27,37,38,39,34])). % 202.16/202.18 cnf(251,plain, % 202.16/202.18 (P3(f4(a5,a9,a1),f8(a7,a1))), % 202.16/202.18 inference(scs_inference,[],[226,108,20,121,42,40,56,209,117,27,37,38,39,34,13,12])). % 202.16/202.18 cnf(257,plain, % 202.16/202.18 (~E(a7,a5)), % 202.16/202.18 inference(scs_inference,[],[23,21,226,108,60,20,121,42,40,56,209,117,222,27,37,38,39,34,13,12,3,14,4])). % 202.16/202.18 cnf(258,plain, % 202.16/202.18 (P3(f4(a5,a9,a2),a7)), % 202.16/202.18 inference(scs_inference,[],[18,23,21,226,108,60,20,121,42,40,56,209,117,222,27,37,38,39,34,13,12,3,14,4,29])). % 202.16/202.18 cnf(265,plain, % 202.16/202.18 (~P3(a7,f4(a5,a9,a2))), % 202.16/202.18 inference(scs_inference,[],[258,27])). % 202.16/202.18 cnf(267,plain, % 202.16/202.18 (~P3(f4(a5,a9,a2),f8(x2671,a7))), % 202.16/202.18 inference(scs_inference,[],[258,27,38])). % 202.16/202.18 cnf(269,plain, % 202.16/202.18 (~P3(x2691,f8(f8(a2,x2692),x2693))), % 202.16/202.18 inference(scs_inference,[],[258,172,27,38,37])). % 202.16/202.18 cnf(274,plain, % 202.16/202.18 (P3(f4(a5,a9,a2),f8(a7,f8(a2,x2741)))), % 202.16/202.18 inference(scs_inference,[],[258,20,172,27,38,37,31,39])). % 202.16/202.18 cnf(275,plain, % 202.16/202.18 (~P3(x2751,f8(a2,x2752))), % 202.16/202.18 inference(rename_variables,[],[172])). % 202.16/202.18 cnf(278,plain, % 202.16/202.18 (~E(a7,f8(f8(x2781,a5),x2782))), % 202.16/202.18 inference(rename_variables,[],[151])). % 202.16/202.18 cnf(279,plain, % 202.16/202.18 (~P3(x2791,f8(a2,x2792))), % 202.16/202.18 inference(rename_variables,[],[172])). % 202.16/202.18 cnf(281,plain, % 202.16/202.18 (~E(a7,f8(a2,x2811))), % 202.16/202.18 inference(scs_inference,[],[258,151,20,172,275,279,27,38,37,31,39,34,13])). % 202.16/202.18 cnf(283,plain, % 202.16/202.18 (~E(a7,f8(x2831,a5))), % 202.16/202.18 inference(scs_inference,[],[258,44,151,278,20,172,275,279,27,38,37,31,39,34,13,3])). % 202.16/202.18 cnf(284,plain, % 202.16/202.18 (E(x2841,f8(x2841,a1))), % 202.16/202.18 inference(rename_variables,[],[44])). % 202.16/202.18 cnf(286,plain, % 202.16/202.19 (P3(f8(f4(a5,a9,a2),a1),a7)), % 202.16/202.19 inference(scs_inference,[],[258,44,284,151,278,20,172,275,279,27,38,37,31,39,34,13,3,12])). % 202.16/202.19 cnf(288,plain, % 202.16/202.19 (~E(f8(a2,x2881),f8(a5,a9))), % 202.16/202.19 inference(scs_inference,[],[23,206,258,44,284,151,278,20,172,275,279,27,38,37,31,39,34,13,3,12,14])). % 202.16/202.19 cnf(296,plain, % 202.16/202.19 (~P3(f4(a5,a9,a2),f8(a9,x2961))), % 202.16/202.19 inference(scs_inference,[],[92,230,27,37])). % 202.16/202.19 cnf(300,plain, % 202.16/202.19 (P3(f8(f4(a5,a9,a1),a1),f8(a7,a2))), % 202.16/202.19 inference(scs_inference,[],[108,92,56,230,27,37,38,39])). % 202.16/202.19 cnf(304,plain, % 202.16/202.19 (~E(f8(a2,x3041),f8(a5,a9))), % 202.16/202.19 inference(rename_variables,[],[288])). % 202.16/202.19 cnf(305,plain, % 202.16/202.19 (~P3(x3051,f8(a2,x3052))), % 202.16/202.19 inference(rename_variables,[],[172])). % 202.16/202.19 cnf(307,plain, % 202.16/202.19 (P3(f4(a5,a9,f8(a2,x3071)),a5)), % 202.16/202.19 inference(scs_inference,[],[288,304,108,92,56,172,305,230,27,37,38,39,35,34])). % 202.16/202.19 cnf(311,plain, % 202.16/202.19 (P3(f8(f4(a5,a9,a2),a1),a5)), % 202.16/202.19 inference(scs_inference,[],[288,304,108,44,92,56,246,172,305,230,27,37,38,39,35,34,12])). % 202.16/202.19 cnf(313,plain, % 202.16/202.19 (~E(f8(a7,a1),f8(a1,x3131))), % 202.16/202.19 inference(scs_inference,[],[288,304,108,44,92,42,56,246,172,305,251,230,27,37,38,39,35,34,12,13])). % 202.16/202.19 cnf(315,plain, % 202.16/202.19 (P3(f4(a5,a9,f8(a2,x3151)),a7)), % 202.16/202.19 inference(scs_inference,[],[18,288,304,108,44,92,42,56,246,172,305,251,230,27,37,38,39,35,34,12,13,29])). % 202.16/202.19 cnf(317,plain, % 202.16/202.19 (~P1(f8(a7,a1))), % 202.16/202.19 inference(scs_inference,[],[18,288,304,108,44,92,42,56,246,172,305,251,230,123,27,37,38,39,35,34,12,13,29,25])). % 202.16/202.19 cnf(329,plain, % 202.16/202.19 (P3(f4(a2,x3291,a7),a7)), % 202.16/202.19 inference(scs_inference,[],[315,281,40,56,98,27,38,37,39,34])). % 202.16/202.19 cnf(339,plain, % 202.16/202.19 (~P3(a5,f4(a1,x3391,a5))), % 202.16/202.19 inference(scs_inference,[],[112,27])). % 202.16/202.19 cnf(343,plain, % 202.16/202.19 (~P3(f4(a1,x3431,a5),f8(x3432,a5))), % 202.16/202.19 inference(scs_inference,[],[112,86,27,37,38])). % 202.16/202.19 cnf(353,plain, % 202.16/202.19 (P3(f4(a5,a9,a1),f8(a7,a2))), % 202.16/202.19 inference(scs_inference,[],[177,20,112,42,313,40,56,300,86,27,37,38,39,34,13,12])). % 202.16/202.19 cnf(355,plain, % 202.16/202.19 (~P1(f8(a7,a2))), % 202.16/202.19 inference(scs_inference,[],[177,20,112,42,313,40,56,300,86,123,27,37,38,39,34,13,12,25])). % 202.16/202.19 cnf(371,plain, % 202.16/202.19 (~P3(x3711,f8(a2,x3712))), % 202.16/202.19 inference(rename_variables,[],[172])). % 202.16/202.19 cnf(373,plain, % 202.16/202.19 (~E(a5,f8(a2,x3731))), % 202.16/202.19 inference(scs_inference,[],[315,77,145,283,172,371,56,296,27,38,37,39,34,13])). % 202.16/202.19 cnf(380,plain, % 202.16/202.19 (~P3(a5,f4(a5,a9,a2))), % 202.16/202.19 inference(scs_inference,[],[246,27])). % 202.16/202.19 cnf(384,plain, % 202.16/202.19 (~P3(f4(a5,a9,a2),f8(x3841,a5))), % 202.16/202.19 inference(scs_inference,[],[246,265,27,37,38])). % 202.16/202.19 cnf(386,plain, % 202.16/202.19 (P3(f4(a5,a9,a2),f8(a7,f8(x3861,a7)))), % 202.16/202.19 inference(scs_inference,[],[258,246,265,267,27,37,38,39])). % 202.16/202.19 cnf(402,plain, % 202.16/202.19 (P3(f4(a5,a9,a2),f8(a7,f8(x4021,a5)))), % 202.16/202.19 inference(scs_inference,[],[258,311,384,27,38,37,39])). % 202.16/202.19 cnf(404,plain, % 202.16/202.19 (P3(f4(a2,x4041,a5),a5)), % 202.16/202.19 inference(scs_inference,[],[258,373,311,56,384,27,38,37,39,34])). % 202.16/202.19 cnf(407,plain, % 202.16/202.19 (P3(f8(f4(a2,x4071,a5),a1),a5)), % 202.16/202.19 inference(scs_inference,[],[258,44,373,311,56,384,27,38,37,39,34,12])). % 202.16/202.19 cnf(409,plain, % 202.16/202.19 (~E(f8(a5,f8(a1,x4091)),f8(a1,x4092))), % 202.16/202.19 inference(scs_inference,[],[258,44,373,42,311,56,384,80,27,38,37,39,34,12,13])). % 202.16/202.19 cnf(411,plain, % 202.16/202.19 (P3(f4(a2,x4111,a5),a7)), % 202.16/202.19 inference(scs_inference,[],[18,258,44,373,42,311,56,384,80,27,38,37,39,34,12,13,29])). % 202.16/202.19 cnf(420,plain, % 202.16/202.19 (~P3(f4(a2,x4201,a5),f8(x4202,a7))), % 202.16/202.19 inference(scs_inference,[],[411,380,27,37,38])). % 202.16/202.19 cnf(425,plain, % 202.16/202.19 (P3(f8(f4(a2,x4251,a5),a1),a7)), % 202.16/202.19 inference(scs_inference,[],[18,411,20,380,407,27,37,38,31,29])). % 202.16/202.19 cnf(427,plain, % 202.16/202.19 (P3(f4(a2,x4271,a5),f8(a7,f8(a1,x4272)))), % 202.16/202.19 inference(scs_inference,[],[18,411,20,42,380,407,27,37,38,31,29,39])). % 202.16/202.19 cnf(443,plain, % 202.16/202.19 (P3(f4(a2,x4431,a5),f8(a7,f8(a2,x4432)))), % 202.16/202.19 inference(scs_inference,[],[411,425,172,170,27,38,37,39])). % 202.16/202.19 cnf(444,plain, % 202.16/202.19 (~P3(x4441,f8(a2,x4442))), % 202.16/202.19 inference(rename_variables,[],[172])). % 202.16/202.19 cnf(446,plain, % 202.16/202.19 (~E(f8(a7,a2),f8(a2,x4461))), % 202.16/202.19 inference(scs_inference,[],[411,425,172,444,353,170,27,38,37,39,13])). % 202.16/202.19 cnf(460,plain, % 202.16/202.19 (P3(f4(a1,x4601,a5),f8(a7,a1))), % 202.16/202.19 inference(scs_inference,[],[143,40,307,343,27,37,38,39])). % 202.16/202.19 cnf(472,plain, % 202.16/202.19 (~P3(a5,f4(a2,x4721,a5))), % 202.16/202.19 inference(scs_inference,[],[404,27])). % 202.16/202.19 cnf(474,plain, % 202.16/202.19 (~P3(f4(a2,x4741,a5),f8(x4742,a5))), % 202.16/202.19 inference(scs_inference,[],[404,27,38])). % 202.16/202.19 cnf(478,plain, % 202.16/202.19 (P3(f4(a2,x4781,a5),f8(a7,a1))), % 202.16/202.19 inference(scs_inference,[],[411,40,404,420,27,38,37,39])). % 202.16/202.19 cnf(481,plain, % 202.16/202.19 (P3(f8(f4(a2,x4811,a5),a1),f8(a7,a1))), % 202.16/202.19 inference(scs_inference,[],[411,44,40,404,420,27,38,37,39,12])). % 202.16/202.19 cnf(488,plain, % 202.16/202.19 (~P3(a7,f4(a1,x4881,a7))), % 202.16/202.19 inference(scs_inference,[],[182,27])). % 202.16/202.19 cnf(492,plain, % 202.16/202.19 (~P3(f4(a1,x4921,a7),f8(x4922,a7))), % 202.16/202.19 inference(scs_inference,[],[182,474,27,37,38])). % 202.16/202.19 cnf(514,plain, % 202.16/202.19 (P3(f4(a2,x5141,a5),f8(a7,a2))), % 202.16/202.19 inference(scs_inference,[],[411,329,56,492,27,38,37,39])). % 202.16/202.19 cnf(517,plain, % 202.16/202.19 (P3(f8(f4(a2,x5171,a5),a1),f8(a7,a2))), % 202.16/202.19 inference(scs_inference,[],[411,44,329,56,492,27,38,37,39,12])). % 202.16/202.19 cnf(538,plain, % 202.16/202.19 (~P3(f8(a7,a1),f4(a5,a9,a1))), % 202.16/202.19 inference(scs_inference,[],[251,27])). % 202.16/202.19 cnf(557,plain, % 202.16/202.19 (~E(f8(a7,a9),f8(a1,x5571))), % 202.16/202.19 inference(scs_inference,[],[177,42,353,538,152,27,37,38,39,13])). % 202.16/202.19 cnf(559,plain, % 202.16/202.19 (~P1(f8(a7,a9))), % 202.16/202.19 inference(scs_inference,[],[177,42,353,538,152,123,27,37,38,39,13,25])). % 202.16/202.19 cnf(565,plain, % 202.16/202.19 (~P3(f8(a7,a2),f4(a1,x5651,a5))), % 202.16/202.19 inference(scs_inference,[],[188,27])). % 202.16/202.19 cnf(581,plain, % 202.16/202.19 (~P3(f8(a7,a1),f4(a1,x5811,a5))), % 202.16/202.19 inference(scs_inference,[],[460,27])). % 202.16/202.19 cnf(587,plain, % 202.16/202.19 (P3(f4(a5,a9,a1),f8(a7,a9))), % 202.16/202.19 inference(scs_inference,[],[90,460,565,74,27,37,38,39])). % 202.16/202.19 cnf(589,plain, % 202.16/202.19 (P3(f8(f4(a5,a9,a1),a1),f8(a7,a9))), % 202.16/202.19 inference(scs_inference,[],[90,44,460,565,74,27,37,38,39,12])). % 202.16/202.19 cnf(595,plain, % 202.16/202.19 (~P3(f8(a7,a1),f4(a2,x5951,a5))), % 202.16/202.19 inference(scs_inference,[],[478,27])). % 202.16/202.19 cnf(601,plain, % 202.16/202.19 (P3(f4(a5,a9,a2),f8(a7,a9))), % 202.16/202.19 inference(scs_inference,[],[258,478,581,230,27,37,38,39])). % 202.16/202.19 cnf(613,plain, % 202.16/202.19 (~P3(f8(f4(a5,a9,a2),a1),f8(x6131,a7))), % 202.16/202.19 inference(scs_inference,[],[286,481,595,27,37,38])). % 202.16/202.19 cnf(615,plain, % 202.16/202.19 (P3(f4(a5,a9,a1),f8(a7,f8(a9,x6151)))), % 202.16/202.19 inference(scs_inference,[],[90,286,481,595,209,27,37,38,39])). % 202.16/202.19 cnf(627,plain, % 202.16/202.19 (P3(f4(a5,a9,a2),f8(a7,f8(a9,x6271)))), % 202.16/202.19 inference(scs_inference,[],[258,159,195,339,296,27,37,38,39])). % 202.16/202.19 cnf(631,plain, % 202.16/202.19 (~E(a5,a2)), % 202.16/202.19 inference(scs_inference,[],[258,172,159,195,80,339,296,27,37,38,39,13,4])). % 202.16/202.19 cnf(657,plain, % 202.16/202.19 (~E(f8(a7,a9),f8(a2,x6571))), % 202.16/202.19 inference(scs_inference,[],[143,172,195,517,587,472,343,27,37,38,39,13])). % 202.16/202.19 cnf(667,plain, % 202.16/202.19 (~P3(a7,f8(f4(a1,x6671,a7),x6672))), % 202.16/202.19 inference(scs_inference,[],[514,488,27,37])). % 202.16/202.19 cnf(678,plain, % 202.16/202.19 (~P3(f3(f8(f8(a5,a9),a1),f8(a7,a9)),f8(a7,a9))), % 202.16/202.19 inference(scs_inference,[],[23,20,33,14])). % 202.16/202.19 cnf(874,plain, % 202.16/202.19 (~E(f8(a2,x8741),f8(f8(a5,a9),a1))), % 202.16/202.19 inference(scs_inference,[],[288,20,3])). % 202.16/202.19 cnf(879,plain, % 202.16/202.19 (~E(f8(a5,a9),f8(a1,x8791))), % 202.16/202.19 inference(scs_inference,[],[288,20,42,172,3,34,13])). % 202.16/202.19 cnf(898,plain, % 202.16/202.19 (P3(f4(a1,x8981,f8(a5,a9)),f8(a5,a9))), % 202.16/202.19 inference(scs_inference,[],[90,40,172,879,39,34])). % 202.16/202.19 cnf(899,plain, % 202.16/202.19 (~P3(x8991,a1)), % 202.16/202.19 inference(rename_variables,[],[40])). % 202.16/202.19 cnf(905,plain, % 202.16/202.19 (~P1(f8(f8(a5,a9),a1))+~P1(f8(a2,x9051))), % 202.16/202.19 inference(scs_inference,[],[90,40,899,172,601,874,879,39,34,13,27,25])). % 202.16/202.19 cnf(910,plain, % 202.16/202.19 (P3(f4(a5,a9,a2),f8(a7,a2))), % 202.16/202.19 inference(scs_inference,[],[258,56,898,27,39])). % 202.16/202.19 cnf(911,plain, % 202.16/202.19 (~P3(x9111,a2)), % 202.16/202.19 inference(rename_variables,[],[56])). % 202.16/202.19 cnf(913,plain, % 202.16/202.19 (~E(f8(a7,a1),a2)), % 202.16/202.19 inference(scs_inference,[],[258,251,56,911,898,27,39,13])). % 202.16/202.19 cnf(915,plain, % 202.16/202.19 (P3(f8(f4(a5,a9,a2),a1),f8(a7,a2))), % 202.16/202.19 inference(scs_inference,[],[258,44,251,56,911,898,27,39,13,12])). % 202.16/202.19 cnf(947,plain, % 202.16/202.19 (~P1(f8(f8(a5,a9),a1))), % 202.16/202.19 inference(scs_inference,[],[44,17,905,11])). % 202.16/202.19 cnf(948,plain, % 202.16/202.19 (~P1(f8(f8(a7,a1),a1))), % 202.16/202.19 inference(scs_inference,[],[20,317,11])). % 202.16/202.19 cnf(1346,plain, % 202.16/202.19 (~P1(f8(a5,a1))), % 202.16/202.19 inference(scs_inference,[],[119,20,24,11])). % 202.16/202.19 cnf(1377,plain, % 202.16/202.19 (~P2(a7,a1)), % 202.16/202.19 inference(scs_inference,[],[16,143,26,29])). % 202.16/202.19 cnf(1380,plain, % 202.16/202.19 (~P2(a7,a2)), % 202.16/202.19 inference(scs_inference,[],[1377,61,90,56,14,29])). % 202.16/202.19 cnf(1384,plain, % 202.16/202.19 (~P2(a5,a2)), % 202.16/202.19 inference(scs_inference,[],[77,56,29])). % 202.16/202.19 cnf(1387,plain, % 202.16/202.19 (~E(f8(f8(a7,a1),a1),a2)), % 202.16/202.19 inference(scs_inference,[],[197,77,56,29,15])). % 202.16/202.19 cnf(1390,plain, % 202.16/202.19 (P3(f4(a5,a9,a2),f8(a7,a1))), % 202.16/202.19 inference(scs_inference,[],[1380,48,197,258,77,56,40,29,15,14,39])). % 202.16/202.19 cnf(1402,plain, % 202.16/202.19 (~P2(f8(a7,a2),a2)), % 202.16/202.19 inference(scs_inference,[],[188,56,29])). % 202.16/202.19 cnf(1409,plain, % 202.16/202.19 (~P2(f8(a7,a1),a2)), % 202.16/202.19 inference(scs_inference,[],[251,56,29])). % 202.16/202.19 cnf(1414,plain, % 202.16/202.19 (P3(f4(a7,a2,a1),a7)), % 202.16/202.19 inference(scs_inference,[],[1402,48,251,56,40,29,14,34])). % 202.16/202.19 cnf(1417,plain, % 202.16/202.19 (P3(f8(f4(a7,a2,a1),a1),a7)), % 202.16/202.19 inference(scs_inference,[],[1402,48,44,251,56,40,29,14,34,12])). % 202.16/202.19 cnf(1419,plain, % 202.16/202.19 (~P3(a7,f4(a7,a2,a1))), % 202.16/202.19 inference(scs_inference,[],[1402,48,44,251,56,40,29,14,34,12,27])). % 202.16/202.19 cnf(1421,plain, % 202.16/202.19 (~P3(f4(a7,a2,a1),f8(x14211,a7))), % 202.16/202.19 inference(scs_inference,[],[1402,48,44,251,56,40,29,14,34,12,27,38])). % 202.16/202.19 cnf(1423,plain, % 202.16/202.19 (P3(f4(a7,a2,a1),f8(a7,f8(x14231,a7)))), % 202.16/202.19 inference(scs_inference,[],[1402,48,44,251,56,40,29,14,34,12,27,38,39])). % 202.16/202.19 cnf(1432,plain, % 202.16/202.19 (~P2(f8(a7,a9),a2)), % 202.16/202.19 inference(scs_inference,[],[56,587,1421,1423,1417,37,27,38,29])). % 202.16/202.19 cnf(1435,plain, % 202.16/202.19 (~E(f8(a1,x14351),f8(a7,a1))), % 202.16/202.19 inference(scs_inference,[],[1409,61,56,587,1421,1423,1417,37,27,38,29,14])). % 202.16/202.19 cnf(1437,plain, % 202.16/202.19 (P3(f4(a7,a1,f8(a1,x14371)),a7)), % 202.16/202.19 inference(scs_inference,[],[1409,61,56,42,587,1421,1423,1417,37,27,38,29,14,34])). % 202.16/202.19 cnf(1447,plain, % 202.16/202.19 (~P2(f8(a7,f8(x14471,a7)),a2)), % 202.16/202.19 inference(scs_inference,[],[56,149,1419,1437,37,27,38,29])). % 202.16/202.19 cnf(1452,plain, % 202.16/202.19 (P3(f4(a7,a9,a1),a7)), % 202.16/202.19 inference(scs_inference,[],[1432,48,56,40,149,1419,1437,37,27,38,29,14,34])). % 202.16/202.19 cnf(1453,plain, % 202.16/202.19 (~P3(x14531,a1)), % 202.16/202.19 inference(rename_variables,[],[40])). % 202.16/202.19 cnf(1455,plain, % 202.16/202.19 (~P3(f4(a7,a9,a1),a9)), % 202.16/202.19 inference(scs_inference,[],[1432,48,56,40,1453,149,1419,1437,37,27,38,29,14,34,35])). % 202.16/202.19 cnf(1458,plain, % 202.16/202.19 (P3(f8(f4(a7,a9,a1),a1),a7)), % 202.16/202.19 inference(scs_inference,[],[1432,48,44,56,40,1453,149,1419,1437,37,27,38,29,14,34,35,12])). % 202.16/202.19 cnf(1460,plain, % 202.16/202.19 (P3(f4(a7,a9,a1),f8(a7,a9))), % 202.16/202.19 inference(scs_inference,[],[1432,48,44,56,40,1453,149,1419,1437,37,27,38,29,14,34,35,12,39])). % 202.16/202.19 cnf(1463,plain, % 202.16/202.19 (~P3(f8(a7,a9),f4(a7,a9,a1))), % 202.16/202.19 inference(scs_inference,[],[1460,27])). % 202.16/202.19 cnf(1465,plain, % 202.16/202.19 (~P3(f4(a7,a9,a1),f8(a9,x14651))), % 202.16/202.19 inference(scs_inference,[],[1460,1455,27,37])). % 202.16/202.19 cnf(1469,plain, % 202.16/202.19 (P3(f4(a7,a9,a1),f8(f8(a7,a9),a9))), % 202.16/202.19 inference(scs_inference,[],[1460,1455,27,37,38,39])). % 202.16/202.19 cnf(1471,plain, % 202.16/202.19 (~P2(f8(a7,f8(a2,x14711)),a2)), % 202.16/202.19 inference(scs_inference,[],[56,443,1460,1455,27,37,38,39,29])). % 202.16/202.19 cnf(1472,plain, % 202.16/202.19 (~P3(x14721,a2)), % 202.16/202.19 inference(rename_variables,[],[56])). % 202.16/202.19 cnf(1476,plain, % 202.16/202.19 (P3(f8(f4(a7,a9,a1),a1),f8(a7,a9))), % 202.16/202.19 inference(scs_inference,[],[1447,61,44,56,443,1460,1455,27,37,38,39,29,14,12])). % 202.16/202.19 cnf(1480,plain, % 202.16/202.19 (P3(f4(a7,f8(x14801,a7),f8(a1,x14802)),a7)), % 202.16/202.19 inference(scs_inference,[],[1447,61,44,56,1472,42,443,1460,1455,27,37,38,39,29,14,12,13,34])). % 202.16/202.19 cnf(1493,plain, % 202.16/202.19 (~P3(f4(a7,a9,a1),f8(x14931,a7))), % 202.16/202.19 inference(scs_inference,[],[1463,1469,1452,37,27,38])). % 202.16/202.19 cnf(1495,plain, % 202.16/202.19 (~P2(f8(a7,f8(x14951,a5)),a2)), % 202.16/202.19 inference(scs_inference,[],[56,402,1463,1469,1452,37,27,38,29])). % 202.16/202.19 cnf(1500,plain, % 202.16/202.19 (P3(f4(a7,f8(a2,x15001),a1),a7)), % 202.16/202.19 inference(scs_inference,[],[1471,48,56,40,402,1463,1469,1452,37,27,38,29,14,34])). % 202.16/202.19 cnf(1510,plain, % 202.16/202.19 (P3(f4(a7,a9,a1),f8(a7,f8(x15101,a7)))), % 202.16/202.19 inference(scs_inference,[],[1458,1493,1452,27,37,38,39])). % 202.16/202.19 cnf(1512,plain, % 202.16/202.19 (~P2(f8(a7,f8(a1,x15121)),a2)), % 202.16/202.19 inference(scs_inference,[],[56,427,1458,1493,1452,27,37,38,39,29])). % 202.16/202.19 cnf(1517,plain, % 202.16/202.19 (P3(f4(a7,f8(x15171,a5),f8(a1,x15172)),a7)), % 202.16/202.19 inference(scs_inference,[],[1495,61,56,42,427,1458,1493,1452,27,37,38,39,29,14,34])). % 202.16/202.19 cnf(1518,plain, % 202.16/202.19 (~P3(x15181,f8(a1,x15182))), % 202.16/202.19 inference(rename_variables,[],[42])). % 202.16/202.19 cnf(1520,plain, % 202.16/202.19 (~P3(f4(a7,f8(x15201,a5),f8(a1,x15202)),f8(x15201,a5))), % 202.16/202.19 inference(scs_inference,[],[1495,61,56,42,1518,427,1458,1493,1452,27,37,38,39,29,14,34,35])). % 202.16/202.19 cnf(1530,plain, % 202.16/202.19 (~P2(f8(a5,f8(a1,x15301)),a2)), % 202.16/202.19 inference(scs_inference,[],[56,80,1465,1510,1480,37,27,38,29])). % 202.16/202.19 cnf(1535,plain, % 202.16/202.19 (P3(f4(a7,f8(a1,x15351),a1),a7)), % 202.16/202.19 inference(scs_inference,[],[1512,48,56,40,80,1465,1510,1480,37,27,38,29,14,34])). % 202.16/202.19 cnf(1543,plain, % 202.16/202.19 (~P2(f8(f8(a7,a9),a9),a2)), % 202.16/202.19 inference(scs_inference,[],[56,1517,1469,27,38,29])). % 202.16/202.19 cnf(1548,plain, % 202.16/202.19 (P3(f4(a5,f8(a1,x15481),f8(a1,x15482)),a5)), % 202.16/202.19 inference(scs_inference,[],[1530,61,56,42,1517,1469,27,38,29,14,34])). % 202.16/202.19 cnf(1556,plain, % 202.16/202.19 (~P2(f8(a5,a9),a2)), % 202.16/202.19 inference(scs_inference,[],[56,1548,898,27,38,29])). % 202.16/202.19 cnf(1562,plain, % 202.16/202.19 (~P3(x15621,a1)), % 202.16/202.19 inference(rename_variables,[],[40])). % 202.16/202.19 cnf(1564,plain, % 202.16/202.19 (P3(f4(f8(a7,a9),a9,a1),f8(a7,a9))), % 202.16/202.19 inference(scs_inference,[],[1543,48,56,40,1562,1548,898,27,38,29,14,35,34])). % 202.16/202.19 cnf(1574,plain, % 202.16/202.19 (~P2(f8(a7,f8(a9,x15741)),a2)), % 202.16/202.19 inference(scs_inference,[],[56,1564,1500,615,27,38,29])). % 202.16/202.19 cnf(1589,plain, % 202.16/202.19 (~P3(a7,f4(a7,a9,a1))), % 202.16/202.19 inference(scs_inference,[],[1452,27])). % 202.16/202.19 cnf(1607,plain, % 202.16/202.20 (E(f8(x16071,a1),f8(x16071,f8(a1,x16072)))), % 202.16/202.20 inference(scs_inference,[],[19,2,5])). % 202.16/202.20 cnf(1608,plain, % 202.16/202.20 (E(f8(x16081,f8(a1,x16082)),f8(x16081,a1))), % 202.16/202.20 inference(scs_inference,[],[1607,2])). % 202.16/202.20 cnf(1610,plain, % 202.16/202.20 (E(f8(a5,a9),f8(f8(a5,a9),f8(a1,x16101)))), % 202.16/202.20 inference(scs_inference,[],[44,947,1607,2,11,3])). % 202.16/202.20 cnf(1615,plain, % 202.16/202.20 (E(f8(f8(a5,a9),f8(a1,x16151)),f8(a5,a9))), % 202.16/202.20 inference(scs_inference,[],[1610,2])). % 202.16/202.20 cnf(1628,plain, % 202.16/202.20 (~P3(x16281,a2)), % 202.16/202.20 inference(rename_variables,[],[56])). % 202.16/202.20 cnf(1629,plain, % 202.16/202.20 (~P2(f8(f8(a5,a9),f8(a1,x16291)),a2)), % 202.16/202.20 inference(scs_inference,[],[1435,77,56,1628,42,74,1608,1610,2,3,34,32,27,38,13,29])). % 202.16/202.20 cnf(1647,plain, % 202.16/202.20 (P3(f4(a7,a9,a1),f8(a7,f8(a9,x16471)))), % 202.16/202.20 inference(scs_inference,[],[1452,1465,39])). % 202.16/202.20 cnf(1743,plain, % 202.16/202.20 (E(a2,a1)), % 202.16/202.20 inference(scs_inference,[],[17,24])). % 202.16/202.20 cnf(1745,plain, % 202.16/202.20 (P3(f3(a7,a2),a7)), % 202.16/202.20 inference(scs_inference,[],[1380,17,24,28])). % 202.16/202.20 cnf(1748,plain, % 202.16/202.20 (~E(f8(a7,a1),f8(a9,x17481))), % 202.16/202.20 inference(scs_inference,[],[913,1390,1380,230,17,24,28,2,30])). % 202.16/202.20 cnf(1750,plain, % 202.16/202.20 (~P2(f8(a5,a1),a2)), % 202.16/202.20 inference(scs_inference,[],[913,1390,1380,1384,230,17,20,24,28,2,30,14])). % 202.16/202.20 cnf(1751,plain, % 202.16/202.20 (E(f8(x17511,a1),x17511)), % 202.16/202.20 inference(rename_variables,[],[20])). % 202.16/202.20 cnf(1752,plain, % 202.16/202.20 (~P2(f8(a5,a9),f8(a2,a1))), % 202.16/202.20 inference(scs_inference,[],[1556,913,1390,1380,1384,230,17,20,1751,24,28,2,30,14,15])). % 202.16/202.20 cnf(1753,plain, % 202.16/202.20 (E(f8(x17531,a1),x17531)), % 202.16/202.20 inference(rename_variables,[],[20])). % 202.16/202.20 cnf(1754,plain, % 202.16/202.20 (~E(a7,f8(x17541,a7))), % 202.16/202.20 inference(scs_inference,[],[1556,913,1390,1414,1380,1384,230,17,20,1751,24,28,2,30,14,15,31])). % 202.16/202.20 cnf(1756,plain, % 202.16/202.20 (~E(a2,a6)), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,230,17,20,1751,24,28,2,30,14,15,31,11])). % 202.16/202.20 cnf(1757,plain, % 202.16/202.20 (~E(a9,f8(a5,a9))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,230,17,246,20,1751,24,28,2,30,14,15,31,11,32])). % 202.16/202.20 cnf(1759,plain, % 202.16/202.20 (E(f8(x17591,a2),f8(x17591,a1))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,230,17,246,20,1751,24,28,2,30,14,15,31,11,32,5])). % 202.16/202.20 cnf(1760,plain, % 202.16/202.20 (E(f3(a2,x17601),f3(a1,x17601))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,230,17,246,20,1751,24,28,2,30,14,15,31,11,32,5,9])). % 202.16/202.20 cnf(1761,plain, % 202.16/202.20 (E(f3(x17611,a2),f3(x17611,a1))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,230,17,246,20,1751,24,28,2,30,14,15,31,11,32,5,9,10])). % 202.16/202.20 cnf(1762,plain, % 202.16/202.20 (E(f4(a2,x17621,x17622),f4(a1,x17621,x17622))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,230,17,246,20,1751,24,28,2,30,14,15,31,11,32,5,9,10,6])). % 202.16/202.20 cnf(1763,plain, % 202.16/202.20 (E(f4(x17631,a2,x17632),f4(x17631,a1,x17632))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,230,17,246,20,1751,24,28,2,30,14,15,31,11,32,5,9,10,6,7])). % 202.16/202.20 cnf(1764,plain, % 202.16/202.20 (E(f4(x17641,x17642,a2),f4(x17641,x17642,a1))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,230,17,246,20,1751,24,28,2,30,14,15,31,11,32,5,9,10,6,7,8])). % 202.16/202.20 cnf(1768,plain, % 202.16/202.20 (~P3(x17681,f8(a5,a1))+P3(x17681,a7)), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,45,230,17,246,20,1751,24,28,2,30,14,15,31,11,32,5,9,10,6,7,8,4,27,29])). % 202.16/202.20 cnf(1770,plain, % 202.16/202.20 (E(f8(a2,x17701),f8(a1,x17702))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,1390,1414,1380,1384,45,230,17,246,172,20,1751,40,24,28,2,30,14,15,31,11,32,5,9,10,6,7,8,4,27,29,34])). % 202.16/202.20 cnf(1774,plain, % 202.16/202.20 (~E(f8(a5,a1),a2)), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,631,1390,1414,1380,1384,45,230,17,246,172,20,1751,40,44,24,28,2,30,14,15,31,11,32,5,9,10,6,7,8,4,27,29,34,3])). % 202.16/202.20 cnf(1777,plain, % 202.16/202.20 (~P3(f8(a7,a1),f4(a7,a9,a1))), % 202.16/202.20 inference(scs_inference,[],[22,1556,913,631,1589,1390,1414,1380,1384,45,230,17,246,172,20,1751,1753,40,44,24,28,2,30,14,15,31,11,32,5,9,10,6,7,8,4,27,29,34,3,13,12])). % 202.16/202.20 cnf(1779,plain, % 202.16/202.20 (P3(f3(a7,a1),a7)), % 202.16/202.20 inference(scs_inference,[],[1377,28])). % 202.16/202.20 cnf(1781,plain, % 202.16/202.20 (~E(a6,a2)), % 202.16/202.20 inference(scs_inference,[],[1756,1377,28,2])). % 202.16/202.20 cnf(1782,plain, % 202.16/202.20 (~E(a7,f8(a9,x17821))), % 202.16/202.20 inference(scs_inference,[],[1756,1377,1455,1452,28,2,30])). % 202.16/202.20 cnf(1784,plain, % 202.16/202.20 (~E(a5,f8(x17841,a5))), % 202.16/202.20 inference(scs_inference,[],[1756,1377,1455,404,1452,28,2,30,31])). % 202.16/202.20 cnf(1786,plain, % 202.16/202.20 (P2(f4(a1,x17861,x17862),f4(a2,x17861,x17862))), % 202.16/202.20 inference(scs_inference,[],[1756,1762,1377,1455,404,21,1452,28,2,30,31,14])). % 202.16/202.20 cnf(1788,plain, % 202.16/202.20 (~P2(f8(a5,a9),f8(a2,a2))), % 202.16/202.20 inference(scs_inference,[],[1756,1762,1759,1752,1377,1455,404,21,1452,28,2,30,31,14,15])). % 202.16/202.20 cnf(1791,plain, % 202.16/202.20 (~E(a1,a6)), % 202.16/202.20 inference(scs_inference,[],[185,1743,1756,1762,1759,1752,1377,1455,404,21,1452,17,28,2,30,31,14,15,11,3])). % 202.16/202.20 cnf(1792,plain, % 202.16/202.20 (~P3(f4(a7,a2,a2),f8(x17921,a7))), % 202.16/202.20 inference(scs_inference,[],[185,1743,1756,1762,1764,1759,1752,1377,1421,1455,404,21,1452,17,28,2,30,31,14,15,11,3,12])). % 202.16/202.20 cnf(1793,plain, % 202.16/202.20 (E(f4(x17931,x17932,a2),f4(x17931,x17932,a1))), % 202.16/202.20 inference(rename_variables,[],[1764])). % 202.16/202.20 cnf(1794,plain, % 202.16/202.20 (~P3(f8(a7,a1),f4(a7,a9,a2))), % 202.16/202.20 inference(scs_inference,[],[185,1743,1756,1777,1762,1764,1793,1759,1752,1377,1421,1455,404,21,1452,17,28,2,30,31,14,15,11,3,12,13])). % 202.16/202.20 cnf(1796,plain, % 202.16/202.20 (~E(a9,f8(a7,a9))), % 202.16/202.20 inference(scs_inference,[],[185,1743,1756,1777,1762,1764,1793,1759,1752,1377,1421,1455,404,21,1452,17,28,2,30,31,14,15,11,3,12,13,32])). % 202.16/202.20 cnf(1798,plain, % 202.16/202.20 (~P3(a7,f3(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[185,1743,1756,1777,1762,1764,1793,1759,1752,1377,1421,1455,404,21,1452,17,28,2,30,31,14,15,11,3,12,13,32,27])). % 202.16/202.20 cnf(1802,plain, % 202.16/202.20 (E(a2,f8(a7,a2))+P3(f4(a7,a2,a2),a7)), % 202.16/202.20 inference(scs_inference,[],[185,1743,1756,1777,1762,1764,1793,1759,1752,1377,1421,1455,404,21,1452,17,28,2,30,31,14,15,11,3,12,13,32,27,39,34])). % 202.16/202.20 cnf(1805,plain, % 202.16/202.20 (P3(f3(a5,a2),a5)), % 202.16/202.20 inference(scs_inference,[],[1384,28])). % 202.16/202.20 cnf(1807,plain, % 202.16/202.20 (~E(a6,a1)), % 202.16/202.20 inference(scs_inference,[],[1791,1384,28,2])). % 202.16/202.20 cnf(1809,plain, % 202.16/202.20 (E(f8(x18091,a2),f8(x18091,a1))), % 202.16/202.20 inference(rename_variables,[],[1759])). % 202.16/202.20 cnf(1810,plain, % 202.16/202.20 (E(f8(a2,x18101),f8(a2,x18102))), % 202.16/202.20 inference(scs_inference,[],[1791,1750,1759,1384,172,56,28,2,14,34])). % 202.16/202.20 cnf(1814,plain, % 202.16/202.20 (~P2(f8(a5,a1),f8(a2,a1))), % 202.16/202.20 inference(scs_inference,[],[1791,1750,1759,1384,172,20,56,28,2,14,34,15])). % 202.16/202.20 cnf(1816,plain, % 202.16/202.20 (~E(f8(a6,a1),a2)), % 202.16/202.20 inference(scs_inference,[],[1781,1791,1750,1759,1384,172,20,44,56,28,2,14,34,15,3])). % 202.16/202.20 cnf(1823,plain, % 202.16/202.20 (~P3(a5,f3(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[1781,1791,1794,1750,1779,1759,1809,1384,172,20,40,44,56,28,2,14,34,15,3,12,32,27])). % 202.16/202.20 cnf(1825,plain, % 202.16/202.20 (~E(a5,f8(a9,x18251))), % 202.16/202.20 inference(scs_inference,[],[1781,1791,1794,1750,1779,1759,1809,1384,74,77,172,20,40,44,56,28,2,14,34,15,3,12,32,27,30])). % 202.16/202.20 cnf(1827,plain, % 202.16/202.20 (~P3(a7,f4(a7,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[1781,1791,1794,1750,1779,1764,1759,1809,1419,1384,74,77,172,20,40,44,56,28,2,14,34,15,3,12,32,27,30,13])). % 202.16/202.20 cnf(1830,plain, % 202.16/202.20 (P2(f4(a1,a1,x18301),f4(a2,a2,x18301))), % 202.16/202.20 inference(scs_inference,[],[1748,1763,1786,2,14])). % 202.16/202.20 cnf(1831,plain, % 202.16/202.20 (E(f4(x18311,a2,x18312),f4(x18311,a1,x18312))), % 202.16/202.20 inference(rename_variables,[],[1763])). % 202.16/202.20 cnf(1832,plain, % 202.16/202.20 (P2(f4(a1,x18321,x18322),f4(a2,x18321,x18322))), % 202.16/202.20 inference(rename_variables,[],[1786])). % 202.16/202.20 cnf(1833,plain, % 202.16/202.20 (P2(f4(a1,a2,x18331),f4(a2,a1,x18331))), % 202.16/202.20 inference(scs_inference,[],[1748,1763,1831,1786,1832,2,14,15])). % 202.16/202.20 cnf(1834,plain, % 202.16/202.20 (E(f4(x18341,a2,x18342),f4(x18341,a1,x18342))), % 202.16/202.20 inference(rename_variables,[],[1763])). % 202.16/202.20 cnf(1836,plain, % 202.16/202.20 (~E(a1,f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[1346,1748,1763,1831,1786,1832,16,2,14,15,11])). % 202.16/202.20 cnf(1837,plain, % 202.16/202.20 (E(f4(a2,a2,x18371),f4(a1,a1,x18371))), % 202.16/202.20 inference(scs_inference,[],[1346,1748,1763,1831,1834,1786,1832,1762,16,2,14,15,11,3])). % 202.16/202.20 cnf(1840,plain, % 202.16/202.20 (~P3(f4(a7,a9,a2),f8(x18401,a7))), % 202.16/202.20 inference(scs_inference,[],[1346,1748,1763,1831,1834,1786,1832,1762,1764,1493,16,2,14,15,11,3,12])). % 202.16/202.20 cnf(1848,plain, % 202.16/202.20 (~P2(f8(a5,a2),f8(a2,a1))), % 202.16/202.20 inference(scs_inference,[],[1757,1814,1759,2,14])). % 202.16/202.20 cnf(1850,plain, % 202.16/202.20 (~P2(f8(a5,a9),f8(a2,x18501))), % 202.16/202.20 inference(scs_inference,[],[1810,1757,1788,1814,1759,2,14,15])). % 202.16/202.20 cnf(1852,plain, % 202.16/202.20 (~E(f8(a6,a1),a1)), % 202.16/202.20 inference(scs_inference,[],[1807,1810,1757,1788,1814,1759,44,2,14,15,3])). % 202.16/202.20 cnf(1856,plain, % 202.16/202.20 (~P3(f8(a7,a1),f3(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[1807,1810,1757,1788,1798,1814,1463,1759,1764,20,44,2,14,15,3,13,12])). % 202.16/202.20 cnf(1858,plain, % 202.16/202.20 (P3(f3(a5,a2),a7)), % 202.16/202.20 inference(scs_inference,[],[18,1807,1810,1757,1788,1798,1805,1814,1463,1759,1764,20,44,2,14,15,3,13,12,29])). % 202.16/202.20 cnf(1860,plain, % 202.16/202.20 (~E(a2,f8(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[18,1807,1810,1757,1788,1798,1805,1814,1463,1759,1764,20,44,56,2,14,15,3,13,12,29,32])). % 202.16/202.20 cnf(1863,plain, % 202.16/202.20 (~P3(a7,f3(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[18,1807,1810,1757,1788,1798,1805,1814,1463,1759,1764,20,44,56,2,14,15,3,13,12,29,32,27])). % 202.16/202.20 cnf(1865,plain, % 202.16/202.20 (P3(f4(a7,a9,a2),a7)+~P3(f4(a7,a9,a2),x18651)), % 202.16/202.20 inference(scs_inference,[],[18,1807,1840,1810,1757,1788,1798,1805,1814,1463,1759,1764,20,44,56,2,14,15,3,13,12,29,32,27,39])). % 202.16/202.20 cnf(1868,plain, % 202.16/202.20 (P2(f3(x18681,a1),f3(x18681,a2))), % 202.16/202.20 inference(scs_inference,[],[1761,1836,21,2,14])). % 202.16/202.20 cnf(1870,plain, % 202.16/202.20 (~P2(f8(a5,a2),f8(a2,x18701))), % 202.16/202.20 inference(scs_inference,[],[1848,1761,1836,1810,21,2,14,15])). % 202.16/202.20 cnf(1872,plain, % 202.16/202.20 (E(f3(a2,a2),f3(a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1848,1761,1836,1760,1810,21,2,14,15,3])). % 202.16/202.20 cnf(1873,plain, % 202.16/202.20 (E(f3(x18731,a2),f3(x18731,a1))), % 202.16/202.20 inference(rename_variables,[],[1761])). % 202.16/202.20 cnf(1877,plain, % 202.16/202.20 (~P3(f8(a7,a2),f3(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[1856,1848,1761,1873,1836,1760,1810,1759,21,2,14,15,3,13,12])). % 202.16/202.20 cnf(1879,plain, % 202.16/202.20 (~E(a2,f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[1774,2])). % 202.16/202.20 cnf(1880,plain, % 202.16/202.20 (~P3(a7,f3(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[1863,1868,1774,2,29])). % 202.16/202.20 cnf(1883,plain, % 202.16/202.20 (~P2(f8(a7,a1),a1)), % 202.16/202.20 inference(scs_inference,[],[1863,1868,1774,1377,20,2,29,14])). % 202.16/202.20 cnf(1884,plain, % 202.16/202.20 (E(f8(x18841,a1),x18841)), % 202.16/202.20 inference(rename_variables,[],[20])). % 202.16/202.20 cnf(1885,plain, % 202.16/202.20 (~P2(f8(a7,a2),f8(a2,a1))), % 202.16/202.20 inference(scs_inference,[],[1863,1868,1774,1402,1377,20,1884,2,29,14,15])). % 202.16/202.20 cnf(1886,plain, % 202.16/202.20 (E(f8(x18861,a1),x18861)), % 202.16/202.20 inference(rename_variables,[],[20])). % 202.16/202.20 cnf(1891,plain, % 202.16/202.20 (~P3(f8(a7,a1),f3(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[1877,1863,1868,1774,1796,1402,1761,1377,20,1884,1886,44,2,29,14,15,13,3,12])). % 202.16/202.20 cnf(1893,plain, % 202.16/202.20 (~E(f8(a7,a9),f8(a9,x18931))), % 202.16/202.20 inference(scs_inference,[],[1877,1863,1868,1774,1796,1402,1761,1377,1455,1460,20,1884,1886,44,2,29,14,15,13,3,12,30])). % 202.16/202.20 cnf(1896,plain, % 202.16/202.20 (P3(f3(a5,a2),f8(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[1893,70,1805,2,29])). % 202.16/202.20 cnf(1898,plain, % 202.16/202.20 (P2(f3(a1,a1),f3(a2,a2))), % 202.16/202.20 inference(scs_inference,[],[1893,1872,70,1805,21,2,29,14])). % 202.16/202.20 cnf(1900,plain, % 202.16/202.20 (P2(f3(a2,a1),f3(a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1893,1872,70,1868,1805,21,2,29,14,15])). % 202.16/202.20 cnf(1902,plain, % 202.16/202.20 (E(f4(a2,a2,a2),f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1893,1837,1872,70,1868,1805,1764,21,2,29,14,15,3])). % 202.16/202.20 cnf(1904,plain, % 202.16/202.20 (E(f4(x19041,x19042,a2),f4(x19041,x19042,a1))), % 202.16/202.20 inference(rename_variables,[],[1764])). % 202.16/202.20 cnf(1905,plain, % 202.16/202.20 (~P3(f4(a7,a9,a2),f8(a9,x19051))), % 202.16/202.20 inference(scs_inference,[],[1893,1837,1872,70,1868,1805,1465,1764,1904,21,2,29,14,15,3,12])). % 202.16/202.20 cnf(1907,plain, % 202.16/202.20 (~E(a2,f8(a7,a2))), % 202.16/202.20 inference(scs_inference,[],[355,1893,1837,1872,70,1868,1805,1465,1764,1904,21,17,2,29,14,15,3,12,11])). % 202.16/202.20 cnf(1911,plain, % 202.16/202.20 (~P3(f3(a1,a1),f3(a2,a2))), % 202.16/202.20 inference(scs_inference,[],[355,1893,1837,1872,70,1868,1805,1465,1764,1904,21,17,2,29,14,15,3,12,11,13,27])). % 202.16/202.20 cnf(1912,plain, % 202.16/202.20 (P3(f4(a7,a2,a2),a7)), % 202.16/202.20 inference(scs_inference,[],[1907,1802])). % 202.16/202.20 cnf(1914,plain, % 202.16/202.20 (~P3(f3(a1,a1),f3(a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1911,1898,1860,2,29])). % 202.16/202.20 cnf(1916,plain, % 202.16/202.20 (~P2(f8(a7,a2),a1)), % 202.16/202.20 inference(scs_inference,[],[1911,1898,1883,1860,1759,2,29,14])). % 202.16/202.20 cnf(1921,plain, % 202.16/202.20 (E(f3(a2,x19211),f3(a1,x19211))), % 202.16/202.20 inference(rename_variables,[],[1760])). % 202.16/202.20 cnf(1922,plain, % 202.16/202.20 (~E(a1,f8(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[1911,1898,1885,1883,1860,1743,1760,1810,1759,2,29,14,15,13,3])). % 202.16/202.20 cnf(1923,plain, % 202.16/202.20 (~P3(f3(a2,a1),f3(a2,a2))), % 202.16/202.20 inference(scs_inference,[],[1911,1898,1885,1883,1860,1743,1760,1921,1810,1759,2,29,14,15,13,3,12])). % 202.16/202.20 cnf(1925,plain, % 202.16/202.20 (~P3(f4(a7,a9,a2),a9)), % 202.16/202.20 inference(scs_inference,[],[1911,1898,1885,1905,1883,1860,1840,1743,1760,1921,1810,1759,2,29,14,15,13,3,12,39])). % 202.16/202.20 cnf(1928,plain, % 202.16/202.20 (~P3(f4(a7,a9,a2),x19281)+~E(a9,f8(x19281,a9))), % 202.16/202.20 inference(scs_inference,[],[1911,1898,1885,1905,1883,1860,1840,1743,1760,1921,1810,1759,2,29,14,15,13,3,12,39,32])). % 202.16/202.20 cnf(1932,plain, % 202.16/202.20 (~P3(f3(a2,a1),f3(a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1923,1922,1898,2,29])). % 202.16/202.20 cnf(1934,plain, % 202.16/202.20 (P2(f4(a1,a1,a1),f4(a2,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[1923,1902,1922,1898,21,2,29,14])). % 202.16/202.20 cnf(1936,plain, % 202.16/202.20 (P2(f4(a1,a1,a2),f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1923,1830,1902,1922,1898,21,2,29,14,15])). % 202.16/202.20 cnf(1938,plain, % 202.16/202.20 (~P3(f3(a1,a1),f3(a1,a2))), % 202.16/202.20 inference(scs_inference,[],[1914,1923,1830,1902,1922,1898,1761,21,2,29,14,15,13])). % 202.16/202.20 cnf(1939,plain, % 202.16/202.20 (E(f3(x19391,a2),f3(x19391,a1))), % 202.16/202.20 inference(rename_variables,[],[1761])). % 202.16/202.20 cnf(1940,plain, % 202.16/202.20 (E(f4(x19401,a2,a2),f4(x19401,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1914,1923,1830,1902,1922,1898,1763,1761,1764,21,2,29,14,15,13,3])). % 202.16/202.20 cnf(1943,plain, % 202.16/202.20 (~P3(f3(a1,a2),f3(a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1914,1923,1830,1902,1922,1898,1763,1761,1939,1764,21,2,29,14,15,13,3,12])). % 202.16/202.20 cnf(1950,plain, % 202.16/202.20 (~P2(f8(a7,a1),f8(a2,a1))), % 202.16/202.20 inference(scs_inference,[],[1943,1900,1754,1409,20,2,29,15])). % 202.16/202.20 cnf(1952,plain, % 202.16/202.20 (~E(f8(a7,a1),f8(x19521,a7))), % 202.16/202.20 inference(scs_inference,[],[1943,1900,1754,1409,20,44,2,29,15,3])). % 202.16/202.20 cnf(1954,plain, % 202.16/202.20 (~P3(f8(a7,a2),f3(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[1891,1943,1900,1754,1409,1759,20,44,2,29,15,3,12])). % 202.16/202.20 cnf(1956,plain, % 202.16/202.20 (~E(f8(a7,a2),f8(a9,x19561))), % 202.16/202.20 inference(scs_inference,[],[1891,1943,1900,1754,1409,910,1759,230,20,44,2,29,15,3,12,30])). % 202.16/202.20 cnf(1961,plain, % 202.16/202.20 (~E(f8(x19611,a7),f8(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[1952,2])). % 202.16/202.20 cnf(1965,plain, % 202.16/202.20 (P2(f4(a1,a1,a1),f4(a1,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[1954,1934,1952,1837,1868,2,29,15])). % 202.16/202.20 cnf(1976,plain, % 202.16/202.20 (~E(f8(a5,a1),f8(x19761,a5))), % 202.16/202.20 inference(scs_inference,[],[1950,1956,1784,1810,44,2,15,3])). % 202.16/202.20 cnf(1980,plain, % 202.16/202.20 (~P3(x19801,f4(x19802,a2,a2))+P3(x19801,f4(x19802,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1950,1932,1956,1784,1940,1810,1761,44,2,15,3,12,13])). % 202.16/202.20 cnf(1981,plain, % 202.16/202.20 (~P3(x19811,f4(a1,a1,a1))+P3(x19811,f4(a2,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1950,1932,1956,1784,1934,1940,1810,1761,44,2,15,3,12,13,29])). % 202.16/202.20 cnf(1984,plain, % 202.16/202.20 (~E(f8(x19841,a5),f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[1976,2])). % 202.16/202.20 cnf(1985,plain, % 202.16/202.20 (P2(f4(a1,a2,a2),f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1976,1786,1902,2,15])). % 202.16/202.20 cnf(1991,plain, % 202.16/202.20 (~P3(x19911,f4(a1,a1,a1))+P3(x19911,f4(a1,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[1965,1961,1976,1938,1786,1902,1872,1810,2,15,3,12,29])). % 202.16/202.20 cnf(1993,plain, % 202.16/202.20 (~P3(x19931,f4(a1,a1,a1))+~P1(f4(a1,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[1965,1961,1976,1938,1786,1902,1872,1810,2,15,3,12,29,26])). % 202.16/202.20 cnf(1998,plain, % 202.16/202.20 (~P2(f8(a7,a9),f8(a2,a1))), % 202.16/202.20 inference(scs_inference,[],[1782,1432,20,2,15])). % 202.16/202.20 cnf(1999,plain, % 202.16/202.20 (E(f8(x19991,a1),x19991)), % 202.16/202.20 inference(rename_variables,[],[20])). % 202.16/202.20 cnf(2000,plain, % 202.16/202.20 (~P3(f8(a7,a1),f4(a7,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[1782,1827,1432,20,1999,2,15,12])). % 202.16/202.20 cnf(2002,plain, % 202.16/202.20 (~E(f8(a1,x20021),f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[1984,1782,1770,1827,1432,20,1999,2,15,12,3])). % 202.16/202.20 cnf(2005,plain, % 202.16/202.20 (P2(f4(a1,a2,a1),f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1984,1985,1782,1770,1827,1432,1764,20,1999,2,15,12,3,14])). % 202.16/202.20 cnf(2007,plain, % 202.16/202.20 (~E(f8(a5,a1),f8(a1,x20071))), % 202.16/202.20 inference(scs_inference,[],[2002,2])). % 202.16/202.20 cnf(2008,plain, % 202.16/202.20 (P2(f4(a1,a1,a2),f4(a2,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2002,1830,1940,2,15])). % 202.16/202.20 cnf(2011,plain, % 202.16/202.20 (E(f4(a2,x20111,a2),f4(a1,x20111,a1))), % 202.16/202.20 inference(scs_inference,[],[2002,1830,1762,1940,1764,2,15,3])). % 202.16/202.20 cnf(2014,plain, % 202.16/202.20 (~P3(f8(a7,a2),f4(a7,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[2000,2002,1830,1762,1940,1759,1764,2,15,3,12])). % 202.16/202.20 cnf(2017,plain, % 202.16/202.20 (~P2(f8(a7,a9),f8(a2,x20171))), % 202.16/202.20 inference(scs_inference,[],[1998,1825,1810,2,15])). % 202.16/202.20 cnf(2019,plain, % 202.16/202.20 (~P3(f8(a5,a1),f3(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[1998,1825,1823,1810,20,2,15,12])). % 202.16/202.20 cnf(2021,plain, % 202.16/202.20 (~E(f8(a5,a1),f8(a9,x20211))), % 202.16/202.20 inference(scs_inference,[],[1998,1825,1823,1810,20,44,2,15,12,3])). % 202.16/202.20 cnf(2023,plain, % 202.16/202.20 (~P3(x20231,f4(a1,a1,a2))+P3(x20231,f4(a2,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1998,2008,1825,1823,1810,20,44,2,15,12,3,29])). % 202.16/202.20 cnf(2026,plain, % 202.16/202.20 (~E(f8(a9,x20261),f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[2021,2])). % 202.16/202.20 cnf(2028,plain, % 202.16/202.20 (~P3(f8(a5,a2),f3(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[2019,1916,2021,19,1759,2,15,12])). % 202.16/202.20 cnf(2030,plain, % 202.16/202.20 (~E(a2,f8(a7,a9))), % 202.16/202.20 inference(scs_inference,[],[2019,1916,2021,559,19,1759,17,2,15,12,11])). % 202.16/202.20 cnf(2031,plain, % 202.16/202.20 (~P3(x20311,f4(a2,x20312,a2))+P3(x20311,f4(a1,x20312,a1))), % 202.16/202.20 inference(scs_inference,[],[2019,1916,2021,2011,559,19,1759,17,2,15,12,11,13])). % 202.16/202.20 cnf(2034,plain, % 202.16/202.20 (~P3(x20341,f4(a2,a1,a2))+P3(x20341,f4(a1,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2019,1916,2021,2011,559,19,1759,17,2,15,12,11,13,1993,1991])). % 202.16/202.20 cnf(2042,plain, % 202.16/202.20 (~E(a1,f8(a6,a1))), % 202.16/202.20 inference(scs_inference,[],[1852,2])). % 202.16/202.20 cnf(2043,plain, % 202.16/202.20 (~P2(f8(a5,a1),f8(a2,x20431))), % 202.16/202.20 inference(scs_inference,[],[1852,1814,1810,2,15])). % 202.16/202.20 cnf(2047,plain, % 202.16/202.20 (P2(f4(a1,x20471,a1),f4(a2,x20471,a2))), % 202.16/202.20 inference(scs_inference,[],[1852,1880,2011,1814,21,1810,20,2,15,12,14])). % 202.16/202.20 cnf(2049,plain, % 202.16/202.20 (~E(a2,f8(a6,a1))), % 202.16/202.20 inference(scs_inference,[],[1816,2])). % 202.16/202.20 cnf(2050,plain, % 202.16/202.20 (P2(f4(a1,a2,a1),f4(a2,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2047,1816,1763,2,15])). % 202.16/202.20 cnf(2054,plain, % 202.16/202.20 (~P2(a7,f8(a2,a1))), % 202.16/202.20 inference(scs_inference,[],[1796,1380,20,2,15])). % 202.16/202.20 cnf(2056,plain, % 202.16/202.20 (~P3(x20561,f4(a1,a2,a1))+P3(x20561,f4(a2,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2050,1796,1380,20,2,15,29])). % 202.16/202.20 cnf(2058,plain, % 202.16/202.20 (~E(f8(a1,x20581),f8(a6,a1))), % 202.16/202.20 inference(scs_inference,[],[2050,2042,1796,1380,60,20,2,15,29,3])). % 202.16/202.20 cnf(2059,plain, % 202.16/202.20 (~E(f8(a6,a1),f8(a1,x20591))), % 202.16/202.20 inference(scs_inference,[],[2058,2])). % 202.16/202.20 cnf(2060,plain, % 202.16/202.20 (P2(f4(a1,a2,a1),f4(a1,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2058,2047,1837,2,15])). % 202.16/202.20 cnf(2063,plain, % 202.16/202.20 (~P3(x20631,f4(a2,a2,a2))+P3(x20631,f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2058,2047,1837,1902,2,15,13])). % 202.16/202.20 cnf(2067,plain, % 202.16/202.20 (~E(f8(x20671,a5),a5)), % 202.16/202.20 inference(scs_inference,[],[1784,2])). % 202.16/202.20 cnf(2068,plain, % 202.16/202.20 (~E(a6,f8(a1,x20681))), % 202.16/202.20 inference(scs_inference,[],[2059,1784,20,2,3])). % 202.16/202.20 cnf(2072,plain, % 202.16/202.20 (~P2(a5,f8(a2,x20721))), % 202.16/202.20 inference(scs_inference,[],[2059,2054,2043,1784,1759,20,44,2,3,15,14])). % 202.16/202.20 cnf(2082,plain, % 202.16/202.20 (~P3(x20821,f4(a1,a2,a1))+P3(x20821,f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2005,2067,557,1810,2,3,29])). % 202.16/202.20 cnf(2101,plain, % 202.16/202.20 (~E(f8(a7,a1),a5)), % 202.16/202.20 inference(scs_inference,[],[257,68,44,2,3])). % 202.16/202.20 cnf(2103,plain, % 202.16/202.20 (~E(a5,f8(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[2101,2])). % 202.16/202.20 cnf(2108,plain, % 202.16/202.20 (~E(f8(a2,x21081),f8(a7,a9))), % 202.16/202.20 inference(scs_inference,[],[657,2])). % 202.16/202.20 cnf(2110,plain, % 202.16/202.20 (~P3(x21101,f4(a1,a1,a2))+P3(x21101,f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[1936,446,2,29])). % 202.16/202.20 cnf(2112,plain, % 202.16/202.20 (~E(f8(a5,a1),f8(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[1936,2103,446,44,2,29,3])). % 202.16/202.20 cnf(2116,plain, % 202.16/202.20 (~P3(f4(a1,a1,a1),f4(a1,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[1936,2103,446,44,2,29,3,27])). % 202.16/202.20 cnf(2117,plain, % 202.16/202.20 (~P3(f4(a1,a1,a1),f4(a2,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2116,2034])). % 202.16/202.20 cnf(2119,plain, % 202.16/202.20 (~E(f8(a7,a1),f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[2112,2116,2034,2])). % 202.16/202.20 cnf(2120,plain, % 202.16/202.20 (~P3(f4(a2,a1,a2),f4(a1,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2112,2116,2011,2034,2,12])). % 202.16/202.20 cnf(2122,plain, % 202.16/202.20 (~P3(f4(a1,a1,a1),f4(a1,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[2112,2116,2011,1763,2034,2,12,13])). % 202.16/202.20 cnf(2124,plain, % 202.16/202.20 (~P3(f4(a1,a1,a1),f4(a1,a2,a1))), % 202.16/202.20 inference(scs_inference,[],[2112,2116,2060,2011,1763,2034,2,12,13,29])). % 202.16/202.20 cnf(2126,plain, % 202.16/202.20 (~P3(f4(a1,a1,a1),f4(a2,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[2112,2116,2060,2011,1763,2034,2,12,13,29,2031])). % 202.16/202.20 cnf(2127,plain, % 202.16/202.20 (~P3(f4(a1,a1,a1),f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2112,2116,2060,2011,1763,2034,2,12,13,29,2031,1991])). % 202.16/202.20 cnf(2130,plain, % 202.16/202.20 (~E(a7,f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[2119,283,20,2,3])). % 202.16/202.20 cnf(2132,plain, % 202.16/202.20 (~P3(f4(a2,a1,a1),f4(a2,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2117,2119,283,1762,20,2,3,12])). % 202.16/202.20 cnf(2133,plain, % 202.16/202.20 (E(f4(a2,x21331,x21332),f4(a1,x21331,x21332))), % 202.16/202.20 inference(rename_variables,[],[1762])). % 202.16/202.20 cnf(2134,plain, % 202.16/202.20 (~P3(f4(a1,a1,a1),f4(a2,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2117,2119,2127,283,1762,2133,20,2,3,12,13])). % 202.16/202.20 cnf(2138,plain, % 202.16/202.20 (~P3(f4(a2,a1,a1),f4(a1,a2,a1))), % 202.16/202.20 inference(scs_inference,[],[2117,2119,2127,2120,2060,283,1762,2133,20,2,3,12,13,29,2056])). % 202.16/202.20 cnf(2140,plain, % 202.16/202.20 (~E(f8(a5,a1),a7)), % 202.16/202.20 inference(scs_inference,[],[2130,2])). % 202.16/202.20 cnf(2141,plain, % 202.16/202.20 (~E(f8(a9,a1),f8(a5,a9))), % 202.16/202.20 inference(scs_inference,[],[2130,1757,44,2,3])). % 202.16/202.20 cnf(2143,plain, % 202.16/202.20 (~P3(f4(a1,a2,a2),f4(a2,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[2126,2130,1757,1940,44,2,3,12])). % 202.16/202.20 cnf(2147,plain, % 202.16/202.20 (~P3(f4(a2,a1,a2),f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2126,2130,2127,1757,2120,1965,1940,1837,44,2,3,12,13,29])). % 202.16/202.20 cnf(2149,plain, % 202.16/202.20 (~P3(f4(a2,a1,a2),f4(a2,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[2126,2130,2127,1757,2120,1965,1940,1837,44,2,3,12,13,29,2063])). % 202.16/202.20 cnf(2150,plain, % 202.16/202.20 (~P3(f4(a2,a1,a2),f4(a1,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[2126,2130,2127,1757,2120,1965,1940,1837,44,2,3,12,13,29,2063,1980])). % 202.16/202.20 cnf(2153,plain, % 202.16/202.20 (~P3(f4(a2,a2,a2),f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2147,2141,1763,2,12])). % 202.16/202.20 cnf(2155,plain, % 202.16/202.20 (~P3(f4(a2,a1,a2),f4(a2,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2147,2141,2011,1763,2,12,13])). % 202.16/202.20 cnf(2161,plain, % 202.16/202.20 (~E(f8(a5,a9),f8(a2,x21611))), % 202.16/202.20 inference(scs_inference,[],[288,2])). % 202.16/202.20 cnf(2164,plain, % 202.16/202.20 (~P3(f4(a2,a2,a2),f4(a2,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2153,2124,288,1762,1940,2,12,13])). % 202.16/202.20 cnf(2171,plain, % 202.16/202.20 (~P3(f4(a2,a2,a1),f4(a1,a2,a1))), % 202.16/202.20 inference(scs_inference,[],[2138,1763,12])). % 202.16/202.20 cnf(2172,plain, % 202.16/202.20 (E(f4(x21721,a2,x21722),f4(x21721,a1,x21722))), % 202.16/202.20 inference(rename_variables,[],[1763])). % 202.16/202.20 cnf(2175,plain, % 202.16/202.20 (~E(f8(a1,x21751),f8(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[2164,2138,1922,1763,2172,60,12,13,3])). % 202.16/202.20 cnf(2176,plain, % 202.16/202.20 (~P3(x21761,f8(a5,a1))+P3(x21761,f8(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[2164,2138,1922,127,1763,2172,60,12,13,3,29])). % 202.16/202.20 cnf(2181,plain, % 202.16/202.20 (~E(f8(a5,a2),f8(a1,x21811))), % 202.16/202.20 inference(scs_inference,[],[2175,2])). % 202.16/202.20 cnf(2184,plain, % 202.16/202.20 (~P3(f4(a2,a1,a1),f4(a2,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[2132,2122,2175,1837,1763,2,12,13])). % 202.16/202.20 cnf(2188,plain, % 202.16/202.20 (~P3(f4(a2,a1,a2),f4(a2,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2134,2011,12])). % 202.16/202.20 cnf(2190,plain, % 202.16/202.20 (~P3(f4(a2,a2,a1),f4(a2,a2,a2))), % 202.16/202.20 inference(scs_inference,[],[2171,2134,2011,12,2031])). % 202.16/202.20 cnf(2193,plain, % 202.16/202.20 (~E(f8(a5,a1),f8(a2,x21931))), % 202.16/202.20 inference(scs_inference,[],[2122,373,1762,44,12,3])). % 202.16/202.20 cnf(2196,plain, % 202.16/202.20 (~P3(f4(a2,a2,a1),f4(a2,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2117,1837,12])). % 202.16/202.20 cnf(2200,plain, % 202.16/202.20 (~P3(f8(a5,a1),f4(a5,a9,a2))), % 202.16/202.20 inference(scs_inference,[],[380,20,12])). % 202.16/202.20 cnf(2204,plain, % 202.16/202.20 (~P3(f8(a5,a1),f4(a5,a9,a1))), % 202.16/202.20 inference(scs_inference,[],[86,20,12])). % 202.16/202.20 cnf(2211,plain, % 202.16/202.20 (~P3(f8(a5,a1),f4(a1,x22111,a5))), % 202.16/202.20 inference(scs_inference,[],[339,20,12])). % 202.16/202.20 cnf(2217,plain, % 202.16/202.20 (~P3(f8(a5,a2),f4(a1,x22171,a5))), % 202.16/202.20 inference(scs_inference,[],[2211,1759,12])). % 202.16/202.20 cnf(2226,plain, % 202.16/202.20 (~P3(f8(a7,a1),x22261)+~P3(x22261,f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[2176,27])). % 202.16/202.20 cnf(2234,plain, % 202.16/202.20 (~P3(f4(a7,a9,a2),x22341)+~E(a9,f8(f8(x22341,a9),a9))), % 202.16/202.20 inference(scs_inference,[],[1925,1928,39])). % 202.16/202.20 cnf(2256,plain, % 202.16/202.20 (~P2(a7,f8(a9,x22561))+~P3(f4(a7,a9,a2),x22562)), % 202.16/202.20 inference(scs_inference,[],[1905,1865,29])). % 202.16/202.20 cnf(2261,plain, % 202.16/202.20 (~P2(a7,f8(a9,x22611))), % 202.16/202.20 inference(scs_inference,[],[56,2030,2256,34])). % 202.16/202.20 cnf(2262,plain, % 202.16/202.20 (~P2(f8(a7,a1),f8(a9,x22621))), % 202.16/202.20 inference(scs_inference,[],[20,2261,14])). % 202.16/202.20 cnf(2264,plain, % 202.16/202.20 (~P3(f8(f4(a2,a1,a2),a1),f4(a1,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[20,2188,2023,12])). % 202.16/202.20 cnf(2265,plain, % 202.16/202.20 (~P2(f8(a7,a2),f8(a9,x22651))), % 202.16/202.20 inference(scs_inference,[],[2262,1759,14])). % 202.16/202.20 cnf(2267,plain, % 202.16/202.20 (~P3(f8(a7,a1),f4(a7,a2,a1))), % 202.16/202.20 inference(scs_inference,[],[20,2262,1419,1759,14,12])). % 202.16/202.20 cnf(2269,plain, % 202.16/202.20 (~P2(f8(a7,a1),a9)), % 202.16/202.20 inference(scs_inference,[],[20,2262,1419,1759,44,14,12,15])). % 202.16/202.20 cnf(2272,plain, % 202.16/202.20 (~P3(f8(f4(a1,a1,a1),a1),f4(a1,a2,a1))), % 202.16/202.20 inference(scs_inference,[],[20,2127,2082,12])). % 202.16/202.20 cnf(2273,plain, % 202.16/202.20 (~P3(f8(a7,a2),f4(a7,a2,a1))), % 202.16/202.20 inference(scs_inference,[],[2267,1759,12])). % 202.16/202.20 cnf(2274,plain, % 202.16/202.20 (E(f8(x22741,a2),f8(x22741,a1))), % 202.16/202.20 inference(rename_variables,[],[1759])). % 202.16/202.20 cnf(2278,plain, % 202.16/202.20 (~P2(f8(a7,a2),a9)), % 202.16/202.20 inference(scs_inference,[],[20,2267,2269,2026,1759,2274,12,3,14])). % 202.16/202.20 cnf(2280,plain, % 202.16/202.20 (~E(f8(a5,a1),a9)), % 202.16/202.20 inference(scs_inference,[],[20,2267,2269,2026,1759,2274,12,3,14,2])). % 202.16/202.20 cnf(2289,plain, % 202.16/202.20 (P2(f3(a2,a2),f3(a1,a1))), % 202.16/202.20 inference(scs_inference,[],[21,1872,15])). % 202.16/202.20 cnf(2292,plain, % 202.16/202.20 (P2(f3(a1,x22921),f3(a2,x22921))), % 202.16/202.20 inference(scs_inference,[],[21,1760,14])). % 202.16/202.20 cnf(2298,plain, % 202.16/202.20 (P2(f3(a1,a2),f3(a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2292,1872,15])). % 202.16/202.20 cnf(2302,plain, % 202.16/202.20 (P3(f3(a7,a2),f8(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[40,1745,39])). % 202.16/202.20 cnf(2303,plain, % 202.16/202.20 (~P3(x23031,a1)), % 202.16/202.20 inference(rename_variables,[],[40])). % 202.16/202.20 cnf(2305,plain, % 202.16/202.20 (E(a1,f8(a2,x23051))), % 202.16/202.20 inference(scs_inference,[],[40,2303,1745,56,39,34])). % 202.16/202.20 cnf(2311,plain, % 202.16/202.20 (E(f8(a1,x23111),f8(a1,x23112))), % 202.16/202.20 inference(scs_inference,[],[40,2305,1791,42,3,34])). % 202.16/202.20 cnf(2315,plain, % 202.16/202.20 (~P2(f8(a7,a9),a1)), % 202.16/202.20 inference(scs_inference,[],[40,2305,2017,1791,42,3,34,15])). % 202.16/202.20 cnf(2317,plain, % 202.16/202.20 (~E(a6,f8(a2,x23171))), % 202.16/202.20 inference(scs_inference,[],[40,2305,2017,1791,42,3,34,15,2])). % 202.16/202.20 cnf(2319,plain, % 202.16/202.20 (E(a2,f8(a1,x23191))), % 202.16/202.20 inference(scs_inference,[],[40,56,34])). % 202.16/202.20 cnf(2325,plain, % 202.16/202.20 (~P2(f8(a5,a2),a1)), % 202.16/202.20 inference(scs_inference,[],[1870,2305,15])). % 202.16/202.20 cnf(2328,plain, % 202.16/202.20 (~P2(f8(a5,a2),f8(a1,x23281))), % 202.16/202.20 inference(scs_inference,[],[2325,19,15])). % 202.16/202.20 cnf(2329,plain, % 202.16/202.20 (P3(f3(a7,a1),f8(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[40,2325,1779,19,15,39])). % 202.16/202.20 cnf(2333,plain, % 202.16/202.20 (~P2(f8(a5,a9),a1)), % 202.16/202.20 inference(scs_inference,[],[1850,2305,15])). % 202.16/202.20 cnf(2335,plain, % 202.16/202.20 (~E(f8(a6,a1),f8(a2,x23351))), % 202.16/202.20 inference(scs_inference,[],[2317,1850,2305,44,15,3])). % 202.16/202.20 cnf(2339,plain, % 202.16/202.20 (~P2(f8(a5,a9),f8(a1,x23391))), % 202.16/202.20 inference(scs_inference,[],[2335,2333,19,2,15])). % 202.16/202.20 cnf(2341,plain, % 202.16/202.20 (~P2(a5,a1)), % 202.16/202.20 inference(scs_inference,[],[2072,2305,15])). % 202.16/202.20 cnf(2343,plain, % 202.16/202.20 (~P2(f8(a5,a1),a1)), % 202.16/202.20 inference(scs_inference,[],[2072,2305,20,15,14])). % 202.16/202.20 cnf(2344,plain, % 202.16/202.20 (E(f8(x23441,a1),x23441)), % 202.16/202.20 inference(rename_variables,[],[20])). % 202.16/202.20 cnf(2345,plain, % 202.16/202.20 (P3(f3(a5,a1),a5)), % 202.16/202.20 inference(scs_inference,[],[2072,2305,20,15,14,28])). % 202.16/202.20 cnf(2349,plain, % 202.16/202.20 (~P3(f8(a5,a1),f3(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[2072,2305,20,2344,15,14,28,27,12])). % 202.16/202.20 cnf(2353,plain, % 202.16/202.20 (P3(f3(a5,a1),f8(a5,a1))), % 202.16/202.20 inference(scs_inference,[],[40,2341,2345,19,15,39])). % 202.16/202.20 cnf(2356,plain, % 202.16/202.20 (P3(f3(a5,a1),f8(a7,a1))), % 202.16/202.20 inference(scs_inference,[],[40,2341,2345,70,19,15,39,29])). % 202.16/202.20 cnf(2358,plain, % 202.16/202.20 (P3(f3(a5,a1),a7)), % 202.16/202.20 inference(scs_inference,[],[40,2341,2345,70,19,15,39,29,1768])). % 202.16/202.20 cnf(2361,plain, % 202.16/202.20 (~E(f8(a2,x23611),f8(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[1922,2305,3])). % 202.16/202.20 cnf(2362,plain, % 202.16/202.20 (~E(f8(a5,a2),f8(a2,x23621))), % 202.16/202.20 inference(scs_inference,[],[2361,2])). % 202.16/202.20 cnf(2363,plain, % 202.16/202.20 (~P2(f8(a5,a1),f8(a1,x23631))), % 202.16/202.20 inference(scs_inference,[],[2343,2361,19,2,15])). % 202.16/202.20 cnf(2367,plain, % 202.16/202.20 (E(f8(a1,x23671),f8(a2,x23672))), % 202.16/202.20 inference(scs_inference,[],[42,2349,1759,56,12,34])). % 202.16/202.20 cnf(2372,plain, % 202.16/202.20 (~P3(f4(a1,a2,a2),f4(a1,a1,a1))), % 202.16/202.20 inference(scs_inference,[],[2143,1934,29])). % 202.16/202.20 cnf(2377,plain, % 202.16/202.20 (~P3(f4(a1,a2,a2),f4(a2,a1,a2))), % 202.16/202.20 inference(scs_inference,[],[2372,2110,2031])). % 202.16/202.20 cnf(2378,plain, % 202.16/202.20 (~P2(a7,a9)), % 202.16/202.20 inference(scs_inference,[],[44,2269,14])). % 202.16/202.20 cnf(2380,plain, % 202.16/202.20 (~P3(f3(a7,a9),a9)), % 202.16/202.20 inference(scs_inference,[],[44,2269,14,33])). % 202.16/202.20 cnf(2382,plain, % 202.16/202.20 (P3(f3(a7,a9),a7)), % 202.16/202.20 inference(scs_inference,[],[44,2269,14,33,28])). % 202.16/202.20 cnf(2384,plain, % 202.16/202.20 (~P3(a7,f3(a7,a9))), % 202.16/202.20 inference(scs_inference,[],[44,2269,14,33,28,27])). % 202.16/202.20 cnf(2386,plain, % 202.16/202.20 (~P3(f3(a7,a9),f8(a9,a1))), % 202.16/202.20 inference(scs_inference,[],[44,2269,20,14,33,28,27,13])). % 202.16/202.20 cnf(2390,plain, % 202.16/202.20 (~P3(f8(a7,a1),f3(a7,a9))), % 202.16/202.20 inference(scs_inference,[],[2386,2384,1759,20,13,12])). % 202.16/202.20 cnf(2392,plain, % 202.16/202.20 (~P3(f8(a7,a2),f3(a7,a9))), % 202.16/202.20 inference(scs_inference,[],[2390,1759,12])). % 202.16/202.20 cnf(2394,plain, % 202.16/202.20 (P3(f3(a7,a9),f8(a7,a9))), % 202.16/202.20 inference(scs_inference,[],[2380,2382,39])). % 202.16/202.20 cnf(2399,plain, % 202.16/202.20 (P3(f3(a5,a1),f8(a7,a2))), % 202.16/202.20 inference(scs_inference,[],[56,2358,39])). % 202.16/202.20 cnf(2400,plain, % 202.16/202.20 (~P3(x24001,a2)), % 202.16/202.20 inference(rename_variables,[],[56])). % 202.16/202.20 cnf(2402,plain, % 202.16/202.20 (E(a2,f8(a2,x24021))), % 202.16/202.20 inference(scs_inference,[],[56,2400,2358,39,34])). % 202.16/202.20 cnf(2406,plain, % 202.16/202.20 (E(f8(f8(a1,x24061),x24062),f8(f8(a1,x24063),x24062))), % 202.16/202.20 inference(scs_inference,[],[2311,2,4])). % 202.16/202.20 cnf(2408,plain, % 202.16/202.20 (E(f8(x24081,f8(a1,x24082)),f8(x24081,a2))), % 202.16/202.20 inference(scs_inference,[],[2319,2,5])). % 202.16/202.20 cnf(2409,plain, % 202.16/202.20 (E(f4(x24091,f8(a2,x24092),x24093),f4(x24091,a2,x24093))), % 202.16/202.20 inference(scs_inference,[],[2402,2,7])). % 202.16/202.20 cnf(2413,plain, % 202.16/202.20 (E(f4(f8(a2,x24131),x24132,x24133),f4(a2,x24132,x24133))), % 202.16/202.20 inference(scs_inference,[],[2402,2,6])). % 202.16/202.20 cnf(2414,plain, % 202.16/202.20 (E(f8(f8(a1,x24141),x24142),f8(f8(a2,x24143),x24142))), % 202.16/202.20 inference(scs_inference,[],[1770,2,4])). % 202.16/202.20 cnf(2416,plain, % 202.16/202.20 (E(f8(x24161,f8(a2,x24162)),f8(x24161,f8(a1,x24163)))), % 202.16/202.20 inference(scs_inference,[],[2367,2,5])). % 202.16/202.20 cnf(2417,plain, % 202.16/202.20 (E(f4(x24171,x24172,f8(a1,x24173)),f4(x24171,x24172,a2))), % 202.16/202.20 inference(scs_inference,[],[2319,2,8])). % 202.16/202.20 cnf(2420,plain, % 202.16/202.20 (E(f8(x24201,a1),f8(x24201,a2))), % 202.16/202.20 inference(scs_inference,[],[1743,2,5])). % 202.16/202.20 cnf(2425,plain, % 202.16/202.20 (E(f8(f8(x24251,a2),x24252),f8(f8(x24251,a1),x24252))), % 202.16/202.20 inference(scs_inference,[],[2420,2,4])). % 202.16/202.20 cnf(2430,plain, % 202.16/202.20 (~E(a7,f8(a5,a2))), % 202.16/202.20 inference(scs_inference,[],[2140,2420,3,2])). % 202.16/202.20 cnf(2432,plain, % 202.16/202.20 (E(f8(f8(a1,x24321),x24322),f8(a2,x24322))), % 202.16/202.21 inference(scs_inference,[],[2319,2,4])). % 202.16/202.21 cnf(2434,plain, % 202.16/202.21 (E(f8(x24341,f8(a1,x24342)),f8(x24341,f8(a2,x24343)))), % 202.16/202.21 inference(scs_inference,[],[1770,2,5])). % 202.16/202.21 cnf(2435,plain, % 202.16/202.21 (~E(f8(a7,a1),f8(a5,a2))), % 202.16/202.21 inference(scs_inference,[],[2430,44,3])). % 202.16/202.21 cnf(2438,plain, % 202.16/202.21 (E(f4(a1,x24381,x24382),f4(a2,x24381,x24382))), % 202.16/202.21 inference(scs_inference,[],[1743,2,6])). % 202.16/202.21 cnf(2439,plain, % 202.16/202.21 (P2(f4(a2,a1,a2),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2438,1936,14])). % 202.16/202.21 cnf(2440,plain, % 202.16/202.21 (E(f4(a1,x24401,x24402),f4(a2,x24401,x24402))), % 202.16/202.21 inference(rename_variables,[],[2438])). % 202.16/202.21 cnf(2443,plain, % 202.16/202.21 (~P3(f4(a2,a2,a1),f4(a1,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[2435,2196,2438,2440,1936,2420,14,3,13])). % 202.16/202.21 cnf(2444,plain, % 202.16/202.21 (E(f4(a1,x24441,x24442),f4(a2,x24441,x24442))), % 202.16/202.21 inference(rename_variables,[],[2438])). % 202.16/202.21 cnf(2447,plain, % 202.16/202.21 (~P3(f4(a2,a2,a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2149,2435,2196,2438,2440,2444,1936,2420,14,3,13,12,1991])). % 202.16/202.21 cnf(2449,plain, % 202.16/202.21 (~E(f8(a5,a2),f8(a7,a2))), % 202.16/202.21 inference(scs_inference,[],[2149,2435,2196,2438,2440,2444,1936,2420,14,3,13,12,1991,2])). % 202.16/202.21 cnf(2454,plain, % 202.16/202.21 (E(f4(a1,x24541,x24542),f4(a2,x24541,x24542))), % 202.16/202.21 inference(rename_variables,[],[2438])). % 202.16/202.21 cnf(2456,plain, % 202.16/202.21 (P2(f4(a2,a1,a2),f4(a2,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2150,2439,2449,2438,2454,1759,3,12,2,15])). % 202.16/202.21 cnf(2459,plain, % 202.16/202.21 (E(f4(a1,a2,a2),f4(a2,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2438,1940,3])). % 202.16/202.21 cnf(2461,plain, % 202.16/202.21 (E(f4(a1,x24611,x24612),f4(a2,x24611,x24612))), % 202.16/202.21 inference(rename_variables,[],[2438])). % 202.16/202.21 cnf(2462,plain, % 202.16/202.21 (~P3(f4(a1,a1,a2),f4(a2,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[2155,2438,2461,1940,3,12])). % 202.16/202.21 cnf(2464,plain, % 202.16/202.21 (~P3(f4(a1,a1,a2),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2155,2050,2438,2461,1940,3,12,29])). % 202.16/202.21 cnf(2471,plain, % 202.16/202.21 (~E(a9,f8(a5,a2))), % 202.16/202.21 inference(scs_inference,[],[2190,2280,2438,2420,3,12,2])). % 202.16/202.21 cnf(2473,plain, % 202.16/202.21 (E(f4(a1,a2,x24731),f4(a2,a1,x24731))), % 202.16/202.21 inference(scs_inference,[],[2438,1763,3])). % 202.16/202.21 cnf(2475,plain, % 202.16/202.21 (E(f4(a1,x24751,x24752),f4(a2,x24751,x24752))), % 202.16/202.21 inference(rename_variables,[],[2438])). % 202.16/202.21 cnf(2476,plain, % 202.16/202.21 (P2(f4(a2,a1,a1),f4(a2,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[1833,2459,2438,1763,3,14])). % 202.16/202.21 cnf(2478,plain, % 202.16/202.21 (~P3(f4(a1,a1,a2),f4(a1,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[2462,1833,2459,2438,2475,1763,3,14,13])). % 202.16/202.21 cnf(2479,plain, % 202.16/202.21 (E(f4(a1,x24791,x24792),f4(a2,x24791,x24792))), % 202.16/202.21 inference(rename_variables,[],[2438])). % 202.16/202.21 cnf(2480,plain, % 202.16/202.21 (~P3(f4(a1,a2,a1),f4(a1,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[2443,2462,1833,2459,2438,2475,2479,1763,3,14,13,12])). % 202.16/202.21 cnf(2483,plain, % 202.16/202.21 (E(f8(f4(a2,a1,x24831),x24832),f8(f4(a1,a2,x24831),x24832))), % 202.16/202.21 inference(scs_inference,[],[2473,2,4])). % 202.16/202.21 cnf(2493,plain, % 202.16/202.21 (P2(f4(a2,a1,a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2476,2478,2480,2471,2011,44,2034,1991,3,2056,2,15])). % 202.16/202.21 cnf(2495,plain, % 202.16/202.21 (~P3(f4(a2,a2,a1),f4(a2,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2447,2476,2478,2480,2471,2011,44,2034,1991,3,2056,2,15,29])). % 202.16/202.21 cnf(2503,plain, % 202.16/202.21 (E(f8(x25031,f4(a2,a1,x25032)),f8(x25031,f4(a1,a2,x25032)))), % 202.16/202.21 inference(scs_inference,[],[2473,2,5])). % 202.16/202.21 cnf(2510,plain, % 202.16/202.21 (P2(f4(a2,a1,a1),f4(a2,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[1786,2459,14])). % 202.16/202.21 cnf(2514,plain, % 202.16/202.21 (~P3(f4(a1,a2,a1),f4(a2,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2464,2495,1786,2459,2438,1762,14,13,12])). % 202.16/202.21 cnf(2517,plain, % 202.16/202.21 (~P3(f4(a1,a2,a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2514,1981])). % 202.16/202.21 cnf(2530,plain, % 202.16/202.21 (~E(f8(a6,a2),f8(a2,x25301))), % 202.16/202.21 inference(scs_inference,[],[2335,2420,3])). % 202.16/202.21 cnf(2534,plain, % 202.16/202.21 (E(f4(f8(a1,x25341),x25342,x25343),f4(a2,x25342,x25343))), % 202.16/202.21 inference(scs_inference,[],[2319,2,6])). % 202.16/202.21 cnf(2535,plain, % 202.16/202.21 (E(f4(x25351,x25352,f8(a2,x25353)),f4(x25351,x25352,a2))), % 202.16/202.21 inference(scs_inference,[],[2402,2,8])). % 202.16/202.21 cnf(2540,plain, % 202.16/202.21 (E(f3(a1,x25401),f3(a2,x25401))), % 202.16/202.21 inference(scs_inference,[],[1743,2,9])). % 202.16/202.21 cnf(2541,plain, % 202.16/202.21 (P2(f3(a2,a2),f3(a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2289,2540,15])). % 202.16/202.21 cnf(2542,plain, % 202.16/202.21 (E(f3(a1,x25421),f3(a2,x25421))), % 202.16/202.21 inference(rename_variables,[],[2540])). % 202.16/202.21 cnf(2543,plain, % 202.16/202.21 (E(f3(a1,a2),f3(a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2289,2540,2542,1761,15,3])). % 202.16/202.21 cnf(2546,plain, % 202.16/202.21 (E(f8(x25461,f3(a2,a1)),f8(x25461,f3(a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[2543,2,5])). % 202.16/202.21 cnf(2547,plain, % 202.16/202.21 (P2(f3(a1,a2),f3(a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2541,1760,14])). % 202.16/202.21 cnf(2551,plain, % 202.16/202.21 (~E(a2,f8(a6,a2))), % 202.16/202.21 inference(scs_inference,[],[2541,1816,1760,2420,14,3,2])). % 202.16/202.21 cnf(2553,plain, % 202.16/202.21 (~E(a1,f8(a6,a2))), % 202.16/202.21 inference(scs_inference,[],[2551,1743,3])). % 202.16/202.21 cnf(2555,plain, % 202.16/202.21 (E(f8(f3(a2,x25551),x25552),f8(f3(a1,x25551),x25552))), % 202.16/202.21 inference(scs_inference,[],[2540,2,4])). % 202.16/202.21 cnf(2560,plain, % 202.16/202.21 (E(f4(f3(a2,a1),x25601,x25602),f4(f3(a1,a2),x25601,x25602))), % 202.16/202.21 inference(scs_inference,[],[2543,2,6])). % 202.16/202.21 cnf(2567,plain, % 202.16/202.21 (E(f8(f3(a2,a1),x25671),f8(f3(a1,a2),x25671))), % 202.16/202.21 inference(scs_inference,[],[2543,2,4])). % 202.16/202.21 cnf(2569,plain, % 202.16/202.21 (E(f8(x25691,f4(a2,a1,a1)),f8(x25691,f4(a1,a2,a2)))), % 202.16/202.21 inference(scs_inference,[],[2459,2,5])). % 202.16/202.21 cnf(2570,plain, % 202.16/202.21 (~E(f8(a5,a2),f8(x25701,a5))), % 202.16/202.21 inference(scs_inference,[],[1976,2420,3])). % 202.16/202.21 cnf(2574,plain, % 202.16/202.21 (E(f8(x25741,f3(a2,x25742)),f8(x25741,f3(a1,x25742)))), % 202.16/202.21 inference(scs_inference,[],[2540,2,5])). % 202.16/202.21 cnf(2594,plain, % 202.16/202.21 (E(f4(x25941,f8(a1,x25942),x25943),f4(x25941,a2,x25943))), % 202.16/202.21 inference(scs_inference,[],[2319,2,7])). % 202.16/202.21 cnf(2599,plain, % 202.16/202.21 (E(f4(x25991,a1,x25992),f4(x25991,a2,x25992))), % 202.16/202.21 inference(scs_inference,[],[1743,2,7])). % 202.16/202.21 cnf(2600,plain, % 202.16/202.21 (P2(f4(a2,a2,a2),f4(a2,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2456,2599,14])). % 202.16/202.21 cnf(2601,plain, % 202.16/202.21 (E(f4(x26011,a1,x26012),f4(x26011,a2,x26012))), % 202.16/202.21 inference(rename_variables,[],[2599])). % 202.16/202.21 cnf(2602,plain, % 202.16/202.21 (P2(f4(a2,a1,a2),f4(a2,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2456,2599,2601,14,15])). % 202.16/202.21 cnf(2603,plain, % 202.16/202.21 (E(f4(x26031,a1,x26032),f4(x26031,a2,x26032))), % 202.16/202.21 inference(rename_variables,[],[2599])). % 202.16/202.21 cnf(2604,plain, % 202.16/202.21 (~P3(f8(a7,a2),f4(a7,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2273,2456,2599,2601,2603,14,15,13])). % 202.16/202.21 cnf(2605,plain, % 202.16/202.21 (E(f4(x26051,a1,x26052),f4(x26051,a2,x26052))), % 202.16/202.21 inference(rename_variables,[],[2599])). % 202.16/202.21 cnf(2606,plain, % 202.16/202.21 (E(f4(a1,a1,a2),f4(a2,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2273,2456,2599,2601,2603,2605,2459,14,15,13,3])). % 202.16/202.21 cnf(2607,plain, % 202.16/202.21 (E(f4(x26071,a1,x26072),f4(x26071,a2,x26072))), % 202.16/202.21 inference(rename_variables,[],[2599])). % 202.16/202.21 cnf(2608,plain, % 202.16/202.21 (~P3(f4(a7,a1,a2),f8(x26081,a7))), % 202.16/202.21 inference(scs_inference,[],[2273,2456,2599,2601,2603,2605,2607,1792,2459,14,15,13,3,12])). % 202.16/202.21 cnf(2610,plain, % 202.16/202.21 (P3(f4(a7,a1,a2),a7)+~P3(f4(a7,a1,a2),x26101)), % 202.16/202.21 inference(scs_inference,[],[2273,2456,2599,2601,2603,2605,2607,1792,2459,14,15,13,3,12,39])). % 202.16/202.21 cnf(2614,plain, % 202.16/202.21 (P3(f4(a7,a1,a2),a7)), % 202.16/202.21 inference(scs_inference,[],[1763,1912,2610,12])). % 202.16/202.21 cnf(2618,plain, % 202.16/202.21 (P2(f4(a2,a2,a2),f4(a2,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2600,2599,15])). % 202.16/202.21 cnf(2619,plain, % 202.16/202.21 (E(f4(x26191,a1,x26192),f4(x26191,a2,x26192))), % 202.16/202.21 inference(rename_variables,[],[2599])). % 202.16/202.21 cnf(2622,plain, % 202.16/202.21 (~P3(f8(a7,a2),f4(a7,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[2600,2014,2599,2619,1764,15,14,13])). % 202.16/202.21 cnf(2623,plain, % 202.16/202.21 (E(f4(x26231,a1,x26232),f4(x26231,a2,x26232))), % 202.16/202.21 inference(rename_variables,[],[2599])). % 202.16/202.21 cnf(2624,plain, % 202.16/202.21 (E(f4(a1,a1,a2),f4(a2,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2600,2014,2606,2599,2619,2623,1764,15,14,13,3])). % 202.16/202.21 cnf(2626,plain, % 202.16/202.21 (~P3(f8(a7,a1),f4(a7,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2600,2604,2014,2606,2599,2619,2623,1764,2420,15,14,13,3,12])). % 202.16/202.21 cnf(2628,plain, % 202.16/202.21 (E(f8(f4(a2,a2,a1),x26281),f8(f4(a1,a1,a2),x26281))), % 202.16/202.21 inference(scs_inference,[],[2624,2,4])). % 202.16/202.21 cnf(2636,plain, % 202.16/202.21 (E(f8(x26361,f4(a2,a1,a1)),f8(x26361,f4(a1,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[2606,2,5])). % 202.16/202.21 cnf(2638,plain, % 202.16/202.21 (P2(f4(a2,a1,a2),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2439,2599,15])). % 202.16/202.21 cnf(2639,plain, % 202.16/202.21 (E(f4(x26391,a1,x26392),f4(x26391,a2,x26392))), % 202.16/202.21 inference(rename_variables,[],[2599])). % 202.16/202.21 cnf(2642,plain, % 202.16/202.21 (E(f4(a1,a2,a2),f4(a2,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2618,2439,2599,2639,2459,1837,15,14,3])). % 202.16/202.21 cnf(2648,plain, % 202.16/202.21 (~P3(f4(a7,a1,a1),f8(x26481,a7))), % 202.16/202.21 inference(scs_inference,[],[1421,2599,12])). % 202.16/202.21 cnf(2656,plain, % 202.16/202.21 (P2(f4(a2,a1,a1),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2493,2599,15])). % 202.16/202.21 cnf(2658,plain, % 202.16/202.21 (P2(f4(a2,a2,a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[2493,1985,2642,2599,15,14])). % 202.16/202.21 cnf(2659,plain, % 202.16/202.21 (E(f4(a1,a1,a2),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2493,1985,2624,2642,2599,1762,15,14,3])). % 202.16/202.21 cnf(2661,plain, % 202.16/202.21 (~P3(f4(a1,a2,a1),f4(a2,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2517,2493,1985,2624,2642,2599,1762,15,14,3,29])). % 202.16/202.21 cnf(2664,plain, % 202.16/202.21 (P2(f4(a2,a2,a1),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2658,2599,15])). % 202.16/202.21 cnf(2665,plain, % 202.16/202.21 (E(f4(x26651,a1,x26652),f4(x26651,a2,x26652))), % 202.16/202.21 inference(rename_variables,[],[2599])). % 202.16/202.21 cnf(2666,plain, % 202.16/202.21 (P2(f4(a2,a2,a1),f4(a2,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[2658,1833,2642,2599,15,14])). % 202.16/202.21 cnf(2668,plain, % 202.16/202.21 (E(f4(a1,a1,x26681),f4(a2,a2,x26681))), % 202.16/202.21 inference(scs_inference,[],[2658,1833,2642,2599,2665,2438,15,14,3])). % 202.16/202.21 cnf(2671,plain, % 202.16/202.21 (E(f8(f4(a2,a2,x26711),x26712),f8(f4(a1,a1,x26711),x26712))), % 202.16/202.21 inference(scs_inference,[],[2668,2,4])). % 202.16/202.21 cnf(2675,plain, % 202.16/202.21 (P2(f4(a2,a2,a1),f4(a2,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[2666,2599,15])). % 202.16/202.21 cnf(2679,plain, % 202.16/202.21 (E(f4(a2,a1,a2),f4(a2,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2664,2666,2668,2599,2011,1837,15,14,3])). % 202.16/202.21 cnf(2686,plain, % 202.16/202.21 (P2(f4(a2,a2,a1),f4(a1,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[2675,1762,15])). % 202.16/202.21 cnf(2688,plain, % 202.16/202.21 (E(f8(x26881,f4(a2,a2,a1)),f8(x26881,f4(a2,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[2679,2,5])). % 202.16/202.21 cnf(2689,plain, % 202.16/202.21 (P2(f4(a2,a1,a1),f4(a1,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[2686,1763,14])). % 202.16/202.21 cnf(2693,plain, % 202.16/202.21 (E(f4(a2,a1,a2),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2659,1762,3])). % 202.16/202.21 cnf(2698,plain, % 202.16/202.21 (E(f8(f4(a1,a2,a1),x26981),f8(f4(a2,a1,a2),x26981))), % 202.16/202.21 inference(scs_inference,[],[2693,2,4])). % 202.16/202.21 cnf(2700,plain, % 202.16/202.21 (E(f8(x27001,f4(a1,a2,a1)),f8(x27001,f4(a2,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[2693,2,5])). % 202.16/202.21 cnf(2710,plain, % 202.16/202.21 (E(f8(x27101,f4(a2,a2,a1)),f8(x27101,f4(a1,a2,a2)))), % 202.16/202.21 inference(scs_inference,[],[2642,2,5])). % 202.16/202.21 cnf(2716,plain, % 202.16/202.21 (E(f8(x27161,f4(a2,a2,a1)),f8(x27161,f4(a1,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[2624,2,5])). % 202.16/202.21 cnf(2718,plain, % 202.16/202.21 (E(f8(x27181,f4(a1,a2,a1)),f8(x27181,f4(a1,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[2659,2,5])). % 202.16/202.21 cnf(2753,plain, % 202.16/202.21 (~P3(f8(a5,a2),f4(f8(a1,x27531),a5,f8(a5,a2)))), % 202.16/202.21 inference(scs_inference,[],[42,2570,27,34])). % 202.16/202.21 cnf(2759,plain, % 202.16/202.21 (E(f4(a2,a1,x27591),f4(a1,a2,x27591))), % 202.16/202.21 inference(scs_inference,[],[1762,2599,3])). % 202.16/202.21 cnf(2775,plain, % 202.16/202.21 (P2(f4(a2,a2,x27751),f4(a2,a1,x27751))), % 202.16/202.21 inference(scs_inference,[],[1786,2668,14])). % 202.16/202.21 cnf(2777,plain, % 202.16/202.21 (P2(f4(a1,x27771,x27772),f4(a2,x27771,x27772))), % 202.16/202.21 inference(rename_variables,[],[1786])). % 202.16/202.21 cnf(2778,plain, % 202.16/202.21 (P3(f3(a5,a2),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[1786,1805,2668,40,14,39])). % 202.16/202.21 cnf(2781,plain, % 202.16/202.21 (P2(f4(a1,a1,x27811),f4(a1,a2,x27811))), % 202.16/202.21 inference(scs_inference,[],[1786,2777,2759,1805,2668,40,14,39,15])). % 202.16/202.21 cnf(2788,plain, % 202.16/202.21 (P2(f4(a2,a2,x27881),f4(a1,a2,x27881))), % 202.16/202.21 inference(scs_inference,[],[2775,2759,15])). % 202.16/202.21 cnf(2790,plain, % 202.16/202.21 (P2(f4(a1,a2,a1),f4(a1,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[2775,2781,2759,2659,15,14])). % 202.16/202.21 cnf(2795,plain, % 202.16/202.21 (P2(f4(a1,a1,a1),f4(a1,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[2788,1902,14])). % 202.16/202.21 cnf(2809,plain, % 202.16/202.21 (P2(f4(a1,a1,a2),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[1830,2011,15])). % 202.16/202.21 cnf(2811,plain, % 202.16/202.21 (P2(f4(a1,a1,x28111),f4(a2,a2,x28111))), % 202.16/202.21 inference(rename_variables,[],[1830])). % 202.16/202.21 cnf(2812,plain, % 202.16/202.21 (P2(f4(a2,a1,x28121),f4(a2,a2,x28121))), % 202.16/202.21 inference(scs_inference,[],[1830,2811,2438,2011,15,14])). % 202.16/202.21 cnf(2818,plain, % 202.16/202.21 (P2(f4(a2,a1,x28181),f4(a1,a1,x28181))), % 202.16/202.21 inference(scs_inference,[],[1837,2812,15])). % 202.16/202.21 cnf(2821,plain, % 202.16/202.21 (P2(f4(a2,a2,a1),f4(a1,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[2818,2679,14])). % 202.16/202.21 cnf(2829,plain, % 202.16/202.21 (P3(f3(f8(a7,a9),a1),a7)), % 202.16/202.21 inference(scs_inference,[],[2315,28,37])). % 202.16/202.21 cnf(2830,plain, % 202.16/202.21 (~P3(f3(a7,a9),f8(x28301,a7))), % 202.16/202.21 inference(scs_inference,[],[2378,28,38])). % 202.16/202.21 cnf(2832,plain, % 202.16/202.21 (P3(f3(f8(a5,a1),a1),a7)), % 202.16/202.21 inference(scs_inference,[],[2343,28,1768])). % 202.16/202.21 cnf(2833,plain, % 202.16/202.21 (P3(f3(f8(a5,a1),f8(a1,x28331)),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[2363,28,2176])). % 202.16/202.21 cnf(2834,plain, % 202.16/202.21 (P2(f3(a2,a1),f3(a1,a2))), % 202.16/202.21 inference(scs_inference,[],[1868,1760,15])). % 202.16/202.21 cnf(2843,plain, % 202.16/202.21 (P3(f3(f8(a5,a1),f8(a2,x28431)),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[2043,28,2176])). % 202.16/202.21 cnf(2845,plain, % 202.16/202.21 (P3(f3(f8(a7,a2),a9),a7)), % 202.16/202.21 inference(scs_inference,[],[2278,28,37])). % 202.16/202.21 cnf(2847,plain, % 202.16/202.21 (P3(f3(f8(a5,a1),a1),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[2343,28,2176])). % 202.16/202.21 cnf(2854,plain, % 202.16/202.21 (P3(f3(f8(a5,a2),f8(a1,x28541)),a5)), % 202.16/202.21 inference(scs_inference,[],[2328,28,37])). % 202.16/202.21 cnf(2857,plain, % 202.16/202.21 (P3(f3(f8(a7,a2),a1),a7)), % 202.16/202.21 inference(scs_inference,[],[1916,28,37])). % 202.16/202.21 cnf(2863,plain, % 202.16/202.21 (~P3(f3(a5,a1),f8(x28631,a5))), % 202.16/202.21 inference(scs_inference,[],[2341,28,38])). % 202.16/202.21 cnf(2864,plain, % 202.16/202.21 (~P3(f3(a5,a2),f8(x28641,a5))), % 202.16/202.21 inference(scs_inference,[],[2863,1761,12])). % 202.16/202.21 cnf(2868,plain, % 202.16/202.21 (P3(f3(f8(a5,a9),a1),a5)), % 202.16/202.21 inference(scs_inference,[],[2333,28,37])). % 202.16/202.21 cnf(2870,plain, % 202.16/202.21 (P3(f3(f8(a5,a9),f8(a1,x28701)),a5)), % 202.16/202.21 inference(scs_inference,[],[2339,28,37])). % 202.16/202.21 cnf(2873,plain, % 202.16/202.21 (P2(f4(a2,a2,a2),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[1936,2668,14])). % 202.16/202.21 cnf(2881,plain, % 202.16/202.21 (~P3(f3(f8(a7,a1),f8(a9,x28811)),f8(a9,x28811))), % 202.16/202.21 inference(scs_inference,[],[2262,33])). % 202.16/202.21 cnf(2890,plain, % 202.16/202.21 (E(f8(x28901,f4(x28902,f8(a2,x28903),x28904)),f8(x28901,f4(x28902,a2,x28904)))), % 202.16/202.21 inference(scs_inference,[],[2264,2409,2262,33,9,2034,8,7,6,10,5])). % 202.16/202.21 cnf(2893,plain, % 202.16/202.21 (E(f8(f4(x28931,f8(a2,x28932),x28933),x28934),f8(f4(x28931,a2,x28933),x28934))), % 202.16/202.21 inference(scs_inference,[],[2264,2409,1564,2262,33,9,2034,8,7,6,10,5,37,4])). % 202.16/202.21 cnf(2896,plain, % 202.16/202.21 (P3(f3(f8(f8(a5,a9),f8(a1,x28961)),a2),f8(f8(a5,a9),f8(a1,x28961)))), % 202.16/202.21 inference(scs_inference,[],[2264,2409,1629,1564,2262,33,9,2034,8,7,6,10,5,37,4,1991,28])). % 202.16/202.21 cnf(2900,plain, % 202.16/202.21 (~E(a2,f8(f8(a7,a1),a1))), % 202.16/202.21 inference(scs_inference,[],[2264,2409,2832,1629,1387,1564,2262,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2])). % 202.16/202.21 cnf(2905,plain, % 202.16/202.21 (~P2(f8(f8(a5,a9),f8(a1,x29051)),f8(a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2656,2264,2272,2409,2832,1629,1387,1476,1564,2262,20,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15])). % 202.16/202.21 cnf(2906,plain, % 202.16/202.21 (E(f8(x29061,a1),x29061)), % 202.16/202.21 inference(rename_variables,[],[20])). % 202.16/202.21 cnf(2907,plain, % 202.16/202.21 (~P2(f8(f8(a5,a9),f8(a2,x29071)),a2)), % 202.16/202.21 inference(scs_inference,[],[2656,2264,2272,2409,2832,1629,2416,1387,1476,1564,2262,20,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14])). % 202.16/202.21 cnf(2914,plain, % 202.16/202.21 (~E(f8(a7,a1),f8(x29141,f8(a7,a1)))), % 202.16/202.21 inference(scs_inference,[],[2656,2847,2264,2272,2409,1520,2832,1629,2416,1387,1476,1564,2262,1517,20,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14,39,31])). % 202.16/202.21 cnf(2917,plain, % 202.16/202.21 (E(f4(x29171,f8(a2,x29172),x29173),f4(x29171,a2,x29173))), % 202.16/202.21 inference(rename_variables,[],[2409])). % 202.16/202.21 cnf(2918,plain, % 202.16/202.21 (~E(f8(a7,a1),f8(f8(f8(a1,x29181),x29182),x29183))), % 202.16/202.21 inference(scs_inference,[],[2656,2661,2847,2264,2272,2409,1520,2832,1629,2416,1387,1476,58,1564,2262,1517,20,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14,39,31,13,30])). % 202.16/202.21 cnf(2919,plain, % 202.16/202.21 (~P3(x29191,f8(f8(a1,x29192),x29193))), % 202.16/202.21 inference(rename_variables,[],[58])). % 202.16/202.21 cnf(2930,plain, % 202.16/202.21 (~E(f8(x29301,a7),f8(f8(a7,a9),f8(x29301,a7)))), % 202.16/202.21 inference(scs_inference,[],[667,2656,2661,2830,2847,2264,2272,2409,2917,2413,1520,2832,1629,2416,1387,1476,58,2919,1564,2262,1517,2394,20,2906,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14,39,31,13,30,34,3,12,32])). % 202.16/202.21 cnf(2933,plain, % 202.16/202.21 (~P3(f8(f4(a1,a1,a1),a1),f4(a2,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[667,2656,2661,2830,2847,2264,2272,2409,2917,2413,1520,2832,1629,2416,1387,1476,58,2919,1564,2262,1517,2394,20,2906,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14,39,31,13,30,34,3,12,32,2063,2031])). % 202.16/202.21 cnf(2934,plain, % 202.16/202.21 (~E(a1,f8(f8(a7,a1),a1))), % 202.16/202.21 inference(scs_inference,[],[667,2656,2661,2830,2847,2264,2272,2409,2917,2413,1520,948,2832,1629,2416,1387,1476,58,2919,1564,2262,1517,2394,16,20,2906,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14,39,31,13,30,34,3,12,32,2063,2031,11])). % 202.16/202.21 cnf(2938,plain, % 202.16/202.21 (~P3(f8(f4(a1,a1,a1),a1),f4(a1,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[667,2656,2661,2830,2847,2264,2272,2409,2917,2413,1520,948,2832,1629,2416,1387,1476,2108,58,2919,1564,2262,1517,2394,16,172,20,2906,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14,39,31,13,30,34,3,12,32,2063,2031,11,35,2023])). % 202.16/202.21 cnf(2940,plain, % 202.16/202.21 (~P3(f8(f4(a2,a1,a2),a1),f4(a1,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[667,2656,2661,2830,2847,2264,2272,2409,2917,2413,1520,948,2832,1629,2416,1387,1476,2108,58,2919,1564,2262,1517,2394,16,172,20,2906,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14,39,31,13,30,34,3,12,32,2063,2031,11,35,2023,1980])). % 202.16/202.21 cnf(2941,plain, % 202.16/202.21 (~P3(f8(f4(a1,a1,a1),a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[667,2656,2661,2830,2847,2264,2272,2409,2917,2413,1520,948,2832,1629,2416,1387,1476,2108,58,2919,1564,2262,1517,2394,16,172,20,2906,33,9,2034,8,7,6,10,5,37,4,1991,28,27,2,38,29,15,14,39,31,13,30,34,3,12,32,2063,2031,11,35,2023,1980,1981])). % 202.16/202.21 cnf(2944,plain, % 202.16/202.21 (~P3(f3(f8(a7,a2),f8(a9,x29441)),f8(a9,x29441))), % 202.16/202.21 inference(scs_inference,[],[2265,33])). % 202.16/202.21 cnf(2951,plain, % 202.16/202.21 (E(f8(x29511,f4(f8(a1,x29512),x29513,x29514)),f8(x29511,f4(a2,x29513,x29514)))), % 202.16/202.21 inference(scs_inference,[],[2534,2265,33,9,8,7,6,10,5])). % 202.16/202.21 cnf(2952,plain, % 202.16/202.21 (P3(f3(f8(f8(a5,a9),f8(a1,x29521)),a2),f8(a5,a9))), % 202.16/202.21 inference(scs_inference,[],[2534,2896,2265,33,9,8,7,6,10,5,37])). % 202.16/202.21 cnf(2954,plain, % 202.16/202.21 (E(f8(f4(f8(a1,x29541),x29542,x29543),x29544),f8(f4(a2,x29542,x29543),x29544))), % 202.16/202.21 inference(scs_inference,[],[2534,2896,2265,33,9,8,7,6,10,5,37,4])). % 202.16/202.21 cnf(2960,plain, % 202.16/202.21 (~P3(f8(f4(a5,a9,a1),a1),a9)), % 202.16/202.21 inference(scs_inference,[],[2905,2534,2914,2845,2896,589,2265,33,9,8,7,6,10,5,37,4,28,27,2,38])). % 202.16/202.21 cnf(2966,plain, % 202.16/202.21 (P2(f4(a2,x29661,x29662),f4(f8(a1,x29663),x29661,x29662))), % 202.16/202.21 inference(scs_inference,[],[2821,2938,2905,2534,2432,2914,2845,2896,589,2265,21,33,9,8,7,6,10,5,37,4,28,27,2,38,29,15,14])). % 202.16/202.21 cnf(2971,plain, % 202.16/202.21 (~E(f8(a7,f8(a9,x29711)),f8(x29712,f8(a7,f8(a9,x29711))))), % 202.16/202.21 inference(scs_inference,[],[2821,2938,2833,2905,2534,2432,2914,1647,2845,2896,589,58,2265,21,33,9,8,7,6,10,5,37,4,28,27,2,38,29,15,14,39,31])). % 202.16/202.21 cnf(2991,plain, % 202.16/202.21 (~E(f8(f8(a1,x29911),x29912),f8(f8(a5,a9),f8(a2,x29913)))), % 202.16/202.21 inference(scs_inference,[],[58,2907,28,14])). % 202.16/202.21 cnf(2999,plain, % 202.16/202.21 (E(f8(x29991,f4(x29992,f8(a1,x29993),x29994)),f8(x29991,f4(x29992,a2,x29994)))), % 202.16/202.21 inference(scs_inference,[],[2594,2261,33,9,8,7,6,10,5])). % 202.16/202.21 cnf(3000,plain, % 202.16/202.21 (P3(f3(f8(f8(a5,a9),f8(a1,x30001)),a2),a5)), % 202.16/202.21 inference(scs_inference,[],[2594,2952,2261,33,9,8,7,6,10,5,37])). % 202.16/202.21 cnf(3002,plain, % 202.16/202.21 (E(f8(f4(x30021,f8(a1,x30022),x30023),x30024),f8(f4(x30021,a2,x30023),x30024))), % 202.16/202.21 inference(scs_inference,[],[2594,2952,2261,33,9,8,7,6,10,5,37,4])). % 202.16/202.21 cnf(3013,plain, % 202.16/202.21 (E(f8(x30131,a1),x30131)), % 202.16/202.21 inference(rename_variables,[],[20])). % 202.16/202.21 cnf(3018,plain, % 202.16/202.21 (~P3(x30181,f8(f8(a2,x30182),x30183))), % 202.16/202.21 inference(rename_variables,[],[269])). % 202.16/202.21 cnf(3023,plain, % 202.16/202.21 (E(f4(x30231,f8(a1,x30232),x30233),f4(x30231,a2,x30233))), % 202.16/202.21 inference(rename_variables,[],[2594])). % 202.16/202.21 cnf(3024,plain, % 202.16/202.21 (~E(f8(a7,a1),f8(f8(f8(a2,x30241),x30242),x30243))), % 202.16/202.21 inference(scs_inference,[],[2689,2933,2940,2843,2881,2594,2934,2829,1574,2952,2261,269,3018,20,3013,33,9,8,7,6,10,5,37,4,28,27,2,38,29,15,14,39,31,13,30])). % 202.16/202.21 cnf(3025,plain, % 202.16/202.21 (~P3(x30251,f8(f8(a2,x30252),x30253))), % 202.16/202.21 inference(rename_variables,[],[269])). % 202.16/202.21 cnf(3027,plain, % 202.16/202.21 (E(f8(f8(a2,x30271),x30272),f8(f8(f8(a2,x30271),x30272),x30273))), % 202.16/202.21 inference(scs_inference,[],[2689,2933,2940,2843,2881,2594,2934,2829,1574,2952,2261,269,3018,3025,20,3013,33,9,8,7,6,10,5,37,4,28,27,2,38,29,15,14,39,31,13,30,34])). % 202.16/202.21 cnf(3029,plain, % 202.16/202.21 (~P3(x30291,f8(f8(a2,x30292),x30293))), % 202.16/202.21 inference(rename_variables,[],[269])). % 202.16/202.21 cnf(3036,plain, % 202.16/202.21 (~E(f8(f8(a2,x30361),x30362),f8(f8(a7,a1),f8(f8(a2,x30361),x30362)))), % 202.16/202.21 inference(scs_inference,[],[2392,2689,2933,2940,2843,2881,2594,3023,2934,2829,1574,2560,2952,2408,2261,269,3018,3025,3029,20,3013,33,9,8,7,6,10,5,37,4,28,27,2,38,29,15,14,39,31,13,30,34,3,12,32])). % 202.16/202.21 cnf(3042,plain, % 202.16/202.21 (E(f4(x30421,x30422,a1),f4(x30421,x30422,a2))), % 202.16/202.21 inference(scs_inference,[],[1764,2394,38,2])). % 202.16/202.21 cnf(3051,plain, % 202.16/202.21 (P3(f8(f3(a5,a2),a1),a5)), % 202.16/202.21 inference(scs_inference,[],[44,1764,2116,1805,2394,1852,2857,2941,38,2,27,37,2031,24,1980,12])). % 202.16/202.21 cnf(3052,plain, % 202.16/202.21 (E(x30521,f8(x30521,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3053,plain, % 202.16/202.21 (E(f8(f8(x30531,a2),a1),f8(x30531,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,1759,1764,2116,1805,2394,1852,2857,2941,38,2,27,37,2031,24,1980,12,3])). % 202.16/202.21 cnf(3055,plain, % 202.16/202.21 (P3(f4(a5,a2,a1),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,40,1759,1764,2116,1805,2394,1922,1852,2857,2941,38,2,27,37,2031,24,1980,12,3,34])). % 202.16/202.21 cnf(3059,plain, % 202.16/202.21 (E(x30591,f8(x30591,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3060,plain, % 202.16/202.21 (P2(f8(f4(a1,x30601,x30602),a1),f4(a2,x30601,x30602))), % 202.16/202.21 inference(scs_inference,[],[20,44,3052,3059,40,1759,1764,1452,2116,1805,1786,2394,1922,1852,2857,2941,38,2,27,37,2031,24,1980,12,3,34,13,14])). % 202.16/202.21 cnf(3061,plain, % 202.16/202.21 (E(x30611,f8(x30611,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3064,plain, % 202.16/202.21 (~P1(f8(f8(a7,a9),f8(a1,a7)))), % 202.16/202.21 inference(scs_inference,[],[20,44,3052,3059,3061,40,1759,1764,123,1452,2116,1805,1786,2394,1922,1852,2857,2941,2930,38,2,27,37,2031,24,1980,12,3,34,13,14,15,25])). % 202.16/202.21 cnf(3087,plain, % 202.16/202.21 (P2(f8(f8(a1,x30871),x30872),x30873)), % 202.16/202.21 inference(scs_inference,[],[2011,80,58,2952,38,2,27,28])). % 202.16/202.21 cnf(3088,plain, % 202.16/202.21 (~P3(x30881,f8(f8(a1,x30882),x30883))), % 202.16/202.21 inference(rename_variables,[],[58])). % 202.16/202.21 cnf(3092,plain, % 202.16/202.21 (~P3(x30921,f8(f8(f8(a1,x30922),x30923),x30924))), % 202.16/202.21 inference(scs_inference,[],[2011,80,58,3088,2952,3024,38,2,27,28,4,37])). % 202.16/202.21 cnf(3097,plain, % 202.16/202.21 (E(x30971,f8(x30971,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3100,plain, % 202.16/202.21 (P3(f4(a5,a2,a2),a5)), % 202.16/202.21 inference(scs_inference,[],[56,20,44,2420,2011,315,80,58,3088,2952,1860,3024,2971,38,2,27,28,4,37,5,12,3,34])). % 202.16/202.21 cnf(3106,plain, % 202.16/202.21 (E(x31061,f8(x31061,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3107,plain, % 202.16/202.21 (P2(f8(f3(x31071,a1),a1),f3(x31071,a2))), % 202.16/202.21 inference(scs_inference,[],[56,20,44,3097,3106,2420,2011,315,2394,80,1868,58,3088,2952,1860,1938,2567,3024,2971,38,2,27,28,4,37,5,12,3,34,30,13,14])). % 202.16/202.21 cnf(3108,plain, % 202.16/202.21 (E(x31081,f8(x31081,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3111,plain, % 202.16/202.21 (P3(f4(a5,a2,a1),a7)), % 202.16/202.21 inference(scs_inference,[],[18,56,20,44,3097,3106,3108,2420,2011,315,2394,80,1868,58,3088,2952,1860,1938,3055,2567,3024,2971,38,2,27,28,4,37,5,12,3,34,30,13,14,15,29])). % 202.16/202.21 cnf(3129,plain, % 202.16/202.21 (P2(f8(f8(a2,x31291),x31292),x31293)), % 202.16/202.21 inference(scs_inference,[],[2659,2952,269,3055,38,2,27,28])). % 202.16/202.21 cnf(3130,plain, % 202.16/202.21 (~P3(x31301,f8(f8(a2,x31302),x31303))), % 202.16/202.21 inference(rename_variables,[],[269])). % 202.16/202.21 cnf(3132,plain, % 202.16/202.21 (~P3(x31321,f8(f8(f8(a2,x31322),x31323),x31324))), % 202.16/202.21 inference(scs_inference,[],[2659,2952,269,3130,3055,38,2,27,28,37])). % 202.16/202.21 cnf(3137,plain, % 202.16/202.21 (P3(f4(a2,x31371,f8(a6,a1)),f8(a6,a1))), % 202.16/202.21 inference(scs_inference,[],[56,20,1762,2659,2394,2952,269,3130,2335,3055,678,38,2,27,28,37,12,3,34])). % 202.16/202.21 cnf(3143,plain, % 202.16/202.21 (E(x31431,f8(x31431,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3144,plain, % 202.16/202.21 (P2(f8(f4(a1,a1,a1),a1),f4(a2,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[56,20,44,3143,1762,2659,2394,80,2116,2952,269,3130,1934,2335,3055,2628,678,38,2,27,28,37,12,3,34,30,13,14])). % 202.16/202.21 cnf(3145,plain, % 202.16/202.21 (E(x31451,f8(x31451,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3148,plain, % 202.16/202.21 (P3(f4(a5,a2,a2),a7)), % 202.16/202.21 inference(scs_inference,[],[18,56,20,44,3143,3145,1762,2659,2394,80,2116,2952,269,3130,1934,2335,3055,3100,2628,678,38,2,27,28,37,12,3,34,30,13,14,15,29])). % 202.16/202.21 cnf(3170,plain, % 202.16/202.21 (P2(f8(f8(f8(a2,x31701),x31702),x31703),x31704)), % 202.16/202.21 inference(scs_inference,[],[2534,402,3100,3132,38,2,27,28])). % 202.16/202.21 cnf(3176,plain, % 202.16/202.21 (E(x31761,f8(x31761,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3179,plain, % 202.16/202.21 (P3(f4(a2,a5,f8(a5,a2)),f8(a5,a2))), % 202.16/202.21 inference(scs_inference,[],[56,20,44,1837,2534,80,402,1840,2570,3100,3132,38,2,27,28,37,12,3,34])). % 202.16/202.21 cnf(3184,plain, % 202.16/202.21 (E(x31841,f8(x31841,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3188,plain, % 202.16/202.21 (E(x31881,f8(x31881,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3189,plain, % 202.16/202.21 (P2(f4(a1,a1,a2),f8(f4(a1,a1,a1),a1))), % 202.16/202.21 inference(scs_inference,[],[56,20,44,3176,3184,3188,1837,2534,80,2952,402,1840,1936,2117,2570,3100,2698,3132,38,2,27,28,37,12,3,34,13,30,14,15])). % 202.16/202.21 cnf(3191,plain, % 202.16/202.21 (P3(f8(f3(a5,a2),a1),a7)), % 202.16/202.21 inference(scs_inference,[],[18,56,20,44,3176,3184,3188,1837,2534,80,2952,402,1840,1936,2117,2570,3100,3051,2698,3132,38,2,27,28,37,12,3,34,13,30,14,15,29])). % 202.16/202.21 cnf(3216,plain, % 202.16/202.21 (P3(f8(f3(f8(f8(a5,a9),f8(a1,x32161)),a2),a1),f8(a5,a9))), % 202.16/202.21 inference(scs_inference,[],[44,2459,2952,427,2117,2896,3092,38,2,27,28,37,12])). % 202.16/202.21 cnf(3217,plain, % 202.16/202.21 (E(x32171,f8(x32171,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3224,plain, % 202.16/202.21 (P3(f4(a5,a9,a2),f8(f8(a7,f8(x32241,a5)),a1))), % 202.16/202.21 inference(scs_inference,[],[56,20,44,3217,1764,2459,2952,402,427,2117,1976,2896,3092,38,2,27,28,37,12,3,34,13])). % 202.16/202.21 cnf(3225,plain, % 202.16/202.21 (E(x32251,f8(x32251,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3229,plain, % 202.16/202.21 (P2(f8(f4(a1,a2,a2),a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[56,20,44,3217,3225,1764,2459,2952,402,427,2117,1985,1419,1976,2896,2893,3092,38,2,27,28,37,12,3,34,13,30,14])). % 202.16/202.21 cnf(3230,plain, % 202.16/202.21 (E(x32301,f8(x32301,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3235,plain, % 202.16/202.21 (P3(f3(f8(a5,a9),a1),a7)), % 202.16/202.21 inference(scs_inference,[],[18,56,20,44,3217,3225,3230,1764,2459,2952,402,427,948,2117,1985,1419,1976,2896,3053,2868,2893,3092,38,2,27,28,37,12,3,34,13,30,14,15,11,29])). % 202.16/202.21 cnf(3253,plain, % 202.16/202.21 (E(x32531,f8(x32531,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3256,plain, % 202.16/202.21 (P3(f4(f8(f8(a2,x32561),x32562),x32563,f8(a7,a1)),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,2011,2679,402,269,2302,1938,2868,3024,38,2,27,37,12,3,34])). % 202.16/202.21 cnf(3261,plain, % 202.16/202.21 (E(x32611,f8(x32611,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3266,plain, % 202.16/202.21 (E(x32661,f8(x32661,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3267,plain, % 202.16/202.21 (P2(f4(a1,a1,x32671),f8(f4(a2,a2,x32671),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,3253,3261,3266,2011,2679,402,427,269,2117,1830,2302,1938,2868,3024,2954,38,2,27,37,12,3,34,13,30,14,15])). % 202.16/202.21 cnf(3269,plain, % 202.16/202.21 (~P1(f8(f8(a7,a9),f8(a2,x32691)))), % 202.16/202.21 inference(scs_inference,[],[20,44,3253,3261,3266,2011,2679,402,427,269,2117,1830,2302,1938,2868,3064,2416,3024,2954,38,2,27,37,12,3,34,13,30,14,15,11])). % 202.16/202.21 cnf(3287,plain, % 202.16/202.21 (E(x32871,f8(x32871,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3288,plain, % 202.16/202.21 (E(f8(f4(a1,a1,a2),a1),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,2659,2409,427,2329,2127,2854,38,2,27,37,12,3])). % 202.16/202.21 cnf(3290,plain, % 202.16/202.21 (P3(f4(f8(a7,a1),a1,a1),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,40,2659,2409,427,2329,2127,2854,2934,38,2,27,37,12,3,34])). % 202.16/202.21 cnf(3294,plain, % 202.16/202.21 (E(x32941,f8(x32941,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3298,plain, % 202.16/202.21 (P2(f4(a1,a2,x32981),f8(f4(a2,a1,x32981),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,3287,3294,40,2659,2409,427,1460,1419,1833,2329,2127,2854,2934,3002,38,2,27,37,12,3,34,13,30,15])). % 202.16/202.21 cnf(3299,plain, % 202.16/202.21 (E(x32991,f8(x32991,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3302,plain, % 202.16/202.21 (~P1(f8(f8(a7,a1),f8(a1,x33021)))), % 202.16/202.21 inference(scs_inference,[],[20,44,3287,3294,3299,40,2659,2409,427,1460,948,1419,1833,2329,2127,2854,2934,1608,3002,38,2,27,37,12,3,34,13,30,15,14,11])). % 202.16/202.21 cnf(3323,plain, % 202.16/202.21 (P3(f4(a5,a9,a1),f8(f8(a7,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[44,2594,353,2356,2122,2870,27,37,38,2,13])). % 202.16/202.21 cnf(3324,plain, % 202.16/202.21 (E(x33241,f8(x33241,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3328,plain, % 202.16/202.21 (P2(f8(f4(a2,a1,a2),a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[44,3324,2594,353,1938,2356,2122,2439,2870,2555,27,37,38,2,13,30,14])). % 202.16/202.21 cnf(3329,plain, % 202.16/202.21 (E(x33291,f8(x33291,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3330,plain, % 202.16/202.21 (P2(f4(a2,a1,a2),f8(f4(a1,a1,a1),a1))), % 202.16/202.21 inference(scs_inference,[],[44,3324,3329,2594,353,1938,2356,2122,2439,2870,2555,27,37,38,2,13,30,14,15])). % 202.16/202.21 cnf(3339,plain, % 202.16/202.21 (P3(f4(f8(a7,a9),f8(a1,a7),f8(a1,a7)),f8(a7,a9))), % 202.16/202.21 inference(scs_inference,[],[18,20,44,3324,3329,42,2534,2594,1460,948,353,1938,2356,2122,2439,2870,678,2930,3000,2425,2555,27,37,38,2,13,30,14,15,12,11,3,29,34])). % 202.16/202.21 cnf(3355,plain, % 202.16/202.21 (E(f3(x33551,a1),f3(x33551,a2))), % 202.16/202.21 inference(scs_inference,[],[1761,2399,678,3000,27,37,38,2])). % 202.16/202.21 cnf(3356,plain, % 202.16/202.21 (P3(f4(a5,a9,a1),f8(f8(a7,a9),a1))), % 202.16/202.21 inference(scs_inference,[],[44,1761,587,2399,678,3000,27,37,38,2,13])). % 202.16/202.21 cnf(3357,plain, % 202.16/202.21 (E(x33571,f8(x33571,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3361,plain, % 202.16/202.21 (P2(f8(f4(a2,a1,a2),a1),f4(a2,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[44,3357,1761,2116,587,2399,678,2456,3000,2671,27,37,38,2,13,30,14])). % 202.16/202.21 cnf(3362,plain, % 202.16/202.21 (E(x33621,f8(x33621,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3364,plain, % 202.16/202.21 (E(x33641,f8(x33641,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3371,plain, % 202.16/202.21 (P3(f4(a2,x33711,a6),a6)), % 202.16/202.21 inference(scs_inference,[],[56,20,44,3357,3362,3364,2459,1761,2116,177,587,2399,678,2456,3000,2317,2434,2671,3269,27,37,38,2,13,30,14,15,12,3,11,34])). % 202.16/202.21 cnf(3393,plain, % 202.16/202.21 (P3(f4(a5,a9,a2),f8(f8(a7,a9),a1))), % 202.16/202.21 inference(scs_inference,[],[44,1902,601,615,2386,3339,38,2,37,27,13])). % 202.16/202.21 cnf(3394,plain, % 202.16/202.21 (E(x33941,f8(x33941,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3395,plain, % 202.16/202.21 (P2(f4(a2,a1,a1),f8(f4(a2,a1,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[44,3394,1902,601,615,2386,2476,3339,38,2,37,27,13,15])). % 202.16/202.21 cnf(3396,plain, % 202.16/202.21 (E(x33961,f8(x33961,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3404,plain, % 202.16/202.21 (P3(f4(a6,a2,a2),a6)), % 202.16/202.21 inference(scs_inference,[],[56,20,44,3394,3396,2438,1902,587,601,678,615,2386,2476,2416,2551,3339,3302,38,2,37,27,13,15,14,3,12,11,34])). % 202.16/202.21 cnf(3421,plain, % 202.16/202.21 (~P3(a7,f4(a5,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[2693,2358,667,3111,37,38,2,27])). % 202.16/202.21 cnf(3424,plain, % 202.16/202.21 (E(x34241,f8(x34241,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3425,plain, % 202.16/202.21 (P2(f8(f4(a2,a1,a1),a1),f4(a2,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[44,3424,2693,77,2358,2510,667,3111,37,38,2,27,13,14])). % 202.16/202.21 cnf(3426,plain, % 202.16/202.21 (E(x34261,f8(x34261,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3432,plain, % 202.16/202.21 (P3(f4(a6,a2,a1),a6)), % 202.16/202.21 inference(scs_inference,[],[20,44,3424,3426,40,1763,2693,601,77,678,2358,2510,667,2553,3111,37,38,2,27,13,14,15,3,12,34])). % 202.16/202.21 cnf(3451,plain, % 202.16/202.21 (P2(f4(a2,a2,a2),f8(f4(a2,a1,a1),a1))), % 202.16/202.21 inference(scs_inference,[],[44,2543,386,2600,2272,3148,2,37,27,38,15])). % 202.16/202.21 cnf(3452,plain, % 202.16/202.21 (E(x34521,f8(x34521,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3454,plain, % 202.16/202.21 (E(x34541,f8(x34541,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3456,plain, % 202.16/202.21 (E(x34561,f8(x34561,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3461,plain, % 202.16/202.21 (P3(f4(a5,a1,a1),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,3452,3454,3456,40,19,2543,2302,2399,386,2600,2272,1836,3148,2,37,27,38,15,14,13,3,12,34])). % 202.16/202.21 cnf(3464,plain, % 202.16/202.21 (P3(f4(a5,a1,a1),a7)), % 202.16/202.21 inference(scs_inference,[],[20,44,3452,3454,3456,40,18,19,2543,2302,2399,386,2600,2272,1836,3148,2,37,27,38,15,14,13,3,12,34,29])). % 202.16/202.21 cnf(3482,plain, % 202.16/202.21 (E(x34821,f8(x34821,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3483,plain, % 202.16/202.21 (P2(f8(f4(a1,a2,a1),a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[44,3482,2606,615,149,2005,1777,3179,2,27,38,37,13,14])). % 202.16/202.21 cnf(3484,plain, % 202.16/202.21 (E(x34841,f8(x34841,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3486,plain, % 202.16/202.21 (E(x34861,f8(x34861,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3489,plain, % 202.16/202.21 (P3(f8(f3(a5,a1),a1),f8(a7,a2))), % 202.16/202.21 inference(scs_inference,[],[20,44,3482,3484,3486,2679,2606,2399,615,149,2005,1777,3179,2,27,38,37,13,14,15,3,12])). % 202.16/202.21 cnf(3491,plain, % 202.16/202.21 (P3(f4(a6,a1,a1),a6)), % 202.16/202.21 inference(scs_inference,[],[20,44,3482,3484,3486,40,2679,2606,2399,615,149,2005,1777,2042,3179,2,27,38,37,13,14,15,3,12,34])). % 202.16/202.21 cnf(3512,plain, % 202.16/202.21 (E(x35121,f8(x35121,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3514,plain, % 202.16/202.21 (E(x35141,f8(x35141,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3515,plain, % 202.16/202.21 (P2(f4(a1,a1,a1),f8(f4(a1,a1,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[44,3512,3514,2624,386,117,1965,1905,3290,2,27,37,38,1980,14,13,15])). % 202.16/202.21 cnf(3516,plain, % 202.16/202.21 (E(x35161,f8(x35161,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3521,plain, % 202.16/202.21 (P3(f4(a1,x35211,a6),a6)), % 202.16/202.21 inference(scs_inference,[],[20,44,3512,3514,3516,40,2409,2624,615,386,117,1965,1905,2068,3290,2,27,37,38,1980,14,13,15,3,12,34])). % 202.16/202.21 cnf(3542,plain, % 202.16/202.21 (E(x35421,f8(x35421,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3543,plain, % 202.16/202.21 (P2(f8(f3(a1,a1),a1),f3(a2,a2))), % 202.16/202.21 inference(scs_inference,[],[44,3542,2688,274,1898,1792,3256,2,27,38,37,15,14])). % 202.16/202.21 cnf(3571,plain, % 202.16/202.21 (E(x35711,f8(x35711,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3572,plain, % 202.16/202.21 (P2(f4(a1,a2,a1),f8(f4(a1,a1,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[44,3571,2642,443,2060,2264,3464,2,27,38,37,14,15])). % 202.16/202.21 cnf(3573,plain, % 202.16/202.21 (E(x35731,f8(x35731,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3576,plain, % 202.16/202.21 (E(f8(f8(x35761,f4(a2,a2,a1)),a1),f8(x35761,f4(a2,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[20,44,3571,3573,2688,2642,117,443,2060,2264,3464,2,27,38,37,14,15,13,3])). % 202.16/202.21 cnf(3609,plain, % 202.16/202.21 (P2(f4(a1,a2,a1),f8(f4(a2,a1,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[44,1872,2778,2050,2120,3404,2,27,37,38,15])). % 202.16/202.21 cnf(3610,plain, % 202.16/202.21 (E(x36101,f8(x36101,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3612,plain, % 202.16/202.21 (E(x36121,f8(x36121,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3614,plain, % 202.16/202.21 (E(x36141,f8(x36141,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3619,plain, % 202.16/202.21 (P3(f4(f8(a5,a9),f8(a2,x36191),f8(f8(a1,x36192),x36193)),f8(a5,a9))), % 202.16/202.21 inference(scs_inference,[],[20,44,3610,3612,3614,2668,1872,117,58,274,2778,2050,2120,2991,3404,2,27,37,38,15,14,13,3,12,34])). % 202.16/202.21 cnf(3640,plain, % 202.16/202.21 (E(f4(x36401,a1,a1),f4(x36401,a2,a2))), % 202.16/202.21 inference(scs_inference,[],[1940,2])). % 202.16/202.21 cnf(3641,plain, % 202.16/202.21 (~P3(a6,f4(a6,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[1940,3432,2,27])). % 202.16/202.21 cnf(3648,plain, % 202.16/202.21 (E(x36481,f8(x36481,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3650,plain, % 202.16/202.21 (E(x36501,f8(x36501,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3652,plain, % 202.16/202.21 (E(x36521,f8(x36521,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3657,plain, % 202.16/202.21 (P3(f4(a1,x36571,f8(a5,a2)),f8(a5,a2))), % 202.16/202.21 inference(scs_inference,[],[20,44,3648,3650,3652,40,1761,1940,274,443,2353,2292,2941,2181,3432,2,27,38,37,14,15,13,3,12,34])). % 202.16/202.21 cnf(3669,plain, % 202.16/202.21 (E(f8(a2,x36691),a1)), % 202.16/202.21 inference(scs_inference,[],[2305,2])). % 202.16/202.21 cnf(3677,plain, % 202.16/202.21 (E(x36771,f8(x36771,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3678,plain, % 202.16/202.21 (P2(f8(f4(a1,x36781,a1),a1),f4(a2,x36781,a2))), % 202.16/202.21 inference(scs_inference,[],[44,3677,2305,1896,2047,1914,3491,2,37,38,27,15,14])). % 202.16/202.21 cnf(3703,plain, % 202.16/202.21 (~P3(f3(a5,a2),f8(x37031,a7))), % 202.16/202.21 inference(scs_inference,[],[2319,1858,2372,2,37,38])). % 202.16/202.21 cnf(3707,plain, % 202.16/202.21 (P2(f8(f4(a2,a1,a1),a1),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[44,2319,1858,2372,2656,3619,2,37,38,27,14])). % 202.16/202.21 cnf(3741,plain, % 202.16/202.21 (E(x37411,f8(x37411,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3742,plain, % 202.16/202.21 (P2(f8(f4(a2,a2,a1),a1),f4(a1,a1,a1))), % 202.16/202.21 inference(scs_inference,[],[44,3741,2402,2847,2147,2658,3137,2,37,38,27,15,14])). % 202.16/202.21 cnf(3779,plain, % 202.16/202.21 (E(x37791,f8(x37791,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3780,plain, % 202.16/202.21 (P2(f4(a2,a2,a1),f8(f4(a2,a1,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[44,3779,1743,2843,2153,2666,3216,2,38,27,37,14,15])). % 202.16/202.21 cnf(3781,plain, % 202.16/202.21 (E(x37811,f8(x37811,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3784,plain, % 202.16/202.21 (P3(f8(f4(a7,a1,a2),a1),a7)), % 202.16/202.21 inference(scs_inference,[],[20,44,3779,3781,2606,1743,2614,2843,2153,2666,3216,2,38,27,37,14,15,3,12])). % 202.16/202.21 cnf(3816,plain, % 202.16/202.21 (E(x38161,f8(x38161,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3818,plain, % 202.16/202.21 (E(x38181,f8(x38181,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3821,plain, % 202.16/202.21 (P3(f4(a7,f8(x38211,a5),f8(a1,x38212)),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,3816,3818,2624,1517,2636,2896,2188,2675,3371,2,27,37,38,15,14,3,13])). % 202.16/202.21 cnf(3848,plain, % 202.16/202.21 (E(x38481,f8(x38481,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3850,plain, % 202.16/202.21 (E(x38501,f8(x38501,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3854,plain, % 202.16/202.21 (E(x38541,f8(x38541,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3857,plain, % 202.16/202.21 (P3(f4(a1,x38571,f8(a6,a1)),f8(a6,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,3848,3850,3854,40,2642,1517,2896,589,2718,2495,2686,2059,3821,2,27,37,38,15,14,3,13,12,34])). % 202.16/202.21 cnf(3880,plain, % 202.16/202.21 (P2(f4(a2,a1,a1),f8(f4(a1,a2,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[44,1564,2569,2648,2689,3857,2,27,38,37,15])). % 202.16/202.21 cnf(3881,plain, % 202.16/202.21 (E(x38811,f8(x38811,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3883,plain, % 202.16/202.21 (E(x38831,f8(x38831,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3887,plain, % 202.16/202.21 (E(x38871,f8(x38871,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3890,plain, % 202.16/202.21 (P3(f4(a7,a9,a2),a7)), % 202.16/202.21 inference(scs_inference,[],[20,44,3881,3883,3887,56,2599,2896,589,1564,2569,2648,2689,2030,3857,2,27,38,37,15,14,3,13,12,34])). % 202.16/202.21 cnf(3919,plain, % 202.16/202.21 (E(x39191,f8(x39191,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3920,plain, % 202.16/202.21 (P2(f8(f4(a2,a2,a1),a1),f4(a1,a1,a2))), % 202.16/202.21 inference(scs_inference,[],[44,3919,898,3053,2200,2821,3521,2,27,38,37,15,14])). % 202.16/202.21 cnf(3921,plain, % 202.16/202.21 (E(x39211,f8(x39211,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3927,plain, % 202.16/202.21 (P3(f4(a1,x39271,f8(a5,a1)),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,3919,3921,40,1872,678,589,1564,898,3053,2200,2821,2007,3521,2,27,38,37,15,14,3,13,12,34])). % 202.16/202.21 cnf(3972,plain, % 202.16/202.21 (E(x39721,f8(x39721,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3974,plain, % 202.16/202.21 (E(x39741,f8(x39741,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3978,plain, % 202.16/202.21 (E(x39781,f8(x39781,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(3979,plain, % 202.16/202.21 (P3(f8(f4(a1,x39791,f8(a5,a9)),a1),f8(a5,a9))), % 202.16/202.21 inference(scs_inference,[],[20,44,3972,3974,3978,1940,898,1469,627,2390,2413,2781,3323,2,27,38,37,15,14,3,13,12])). % 202.16/202.21 cnf(4002,plain, % 202.16/202.21 (P2(f4(a2,a2,x40021),f8(f4(a1,a2,x40021),a1))), % 202.16/202.21 inference(scs_inference,[],[44,300,2392,2417,2788,3979,2,27,38,37,15])). % 202.16/202.21 cnf(4030,plain, % 202.16/202.21 (E(x40301,f8(x40301,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4031,plain, % 202.16/202.21 (P2(f8(f4(a2,a1,x40311),a1),f4(a2,a2,x40311))), % 202.16/202.21 inference(scs_inference,[],[44,4030,3055,2661,2535,2812,3356,2,27,38,37,15,14])). % 202.16/202.21 cnf(4061,plain, % 202.16/202.21 (E(x40611,f8(x40611,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4063,plain, % 202.16/202.21 (E(x40631,f8(x40631,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4066,plain, % 202.16/202.21 (P3(f8(f3(a5,a2),a1),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4061,4063,2473,2778,3100,2933,2560,2818,3393,2,27,38,37,15,14,3,12])). % 202.16/202.21 cnf(4067,plain, % 202.16/202.21 (E(x40671,f8(x40671,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4068,plain, % 202.16/202.21 (P3(f4(f8(a1,x40681),x40682,a7),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4061,4063,4067,2473,2778,216,3100,2933,2560,2818,3393,2,27,38,37,15,14,3,12,13])). % 202.16/202.21 cnf(4089,plain, % 202.16/202.21 (~P3(f3(f8(a5,a9),a1),f8(x40891,a5))), % 202.16/202.21 inference(scs_inference,[],[2868,2890,4068,2,27,38])). % 202.16/202.21 cnf(4096,plain, % 202.16/202.21 (E(x40961,f8(x40961,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4097,plain, % 202.16/202.21 (P2(f3(a2,a1),f8(f3(a1,a1),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4096,1770,2868,2940,1900,2890,4068,2,27,38,37,3,14,15])). % 202.16/202.21 cnf(4098,plain, % 202.16/202.21 (E(x40981,f8(x40981,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4099,plain, % 202.16/202.21 (P3(f4(a5,a2,a1),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4096,4098,1770,3055,2868,2940,1900,2890,4068,2,27,38,37,3,14,15,13])). % 202.16/202.21 cnf(4126,plain, % 202.16/202.21 (P2(f8(f3(a2,a2),a1),f3(a1,a1))), % 202.16/202.21 inference(scs_inference,[],[44,2854,2830,2289,2710,4099,2,38,27,37,14])). % 202.16/202.21 cnf(4127,plain, % 202.16/202.21 (E(x41271,f8(x41271,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4128,plain, % 202.16/202.21 (E(f8(f8(x41281,f4(a2,a1,a1)),a1),f8(x41281,f4(a1,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[20,44,2636,2854,2830,2289,2710,4099,2,38,27,37,14,3])). % 202.16/202.21 cnf(4131,plain, % 202.16/202.21 (E(x41311,f8(x41311,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4132,plain, % 202.16/202.21 (P3(f4(a5,a2,a2),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4127,4131,2636,3100,2854,2830,2289,2710,4099,2,38,27,37,14,3,15,13])). % 202.16/202.21 cnf(4133,plain, % 202.16/202.21 (E(x41331,f8(x41331,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4136,plain, % 202.16/202.21 (P3(f4(a5,a2,f8(a1,x41361)),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,4127,4131,4133,42,3055,2636,3100,2854,2830,2289,2710,2175,4099,2,38,27,37,14,3,15,13,12,34])). % 202.16/202.21 cnf(4140,plain, % 202.16/202.21 (P3(f8(f4(a5,a2,a1),a1),a7)), % 202.16/202.21 inference(scs_inference,[],[20,44,4127,4131,4133,42,18,3055,2636,3100,2854,2830,2289,2710,2175,4099,2,38,27,37,14,3,15,13,12,34,29])). % 202.16/202.21 cnf(4163,plain, % 202.16/202.21 (P2(f3(a2,a2),f8(f3(a2,a1),a1))), % 202.16/202.21 inference(scs_inference,[],[44,2870,2863,2541,2716,4132,2,27,38,37,15])). % 202.16/202.21 cnf(4164,plain, % 202.16/202.21 (E(x41641,f8(x41641,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4168,plain, % 202.16/202.21 (E(x41681,f8(x41681,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4169,plain, % 202.16/202.21 (P3(f3(f8(a5,a9),a1),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4164,4168,1607,2868,2870,2863,2541,2716,4132,2,27,38,37,15,3,14,13])). % 202.16/202.21 cnf(4170,plain, % 202.16/202.21 (E(x41701,f8(x41701,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4171,plain, % 202.16/202.21 (P3(f8(f4(a5,a2,a2),a1),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,4164,4168,4170,3100,1607,2868,2870,2863,2541,2716,4132,2,27,38,37,15,3,14,13,12])). % 202.16/202.21 cnf(4198,plain, % 202.16/202.21 (E(x41981,f8(x41981,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4199,plain, % 202.16/202.21 (P2(f8(f4(a2,a2,a2),a1),f4(a2,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[44,4198,3000,4136,2864,2618,2700,2,38,27,37,15,14])). % 202.16/202.21 cnf(4200,plain, % 202.16/202.21 (E(x42001,f8(x42001,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4201,plain, % 202.16/202.21 (E(f8(f8(x42011,f4(a1,a2,a1)),a1),f8(x42011,f4(a1,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[20,44,4198,2718,3000,4136,2864,2618,2700,2,38,27,37,15,14,3])). % 202.16/202.21 cnf(4203,plain, % 202.16/202.21 (P3(f8(f3(f8(a5,a9),a1),a1),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,4198,4200,2868,2718,3000,4136,2864,2618,2700,2,38,27,37,15,14,3,12])). % 202.16/202.21 cnf(4204,plain, % 202.16/202.21 (E(x42041,f8(x42041,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4205,plain, % 202.16/202.21 (P3(f3(f8(a5,a2),f8(a1,x42051)),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4198,4200,4204,2868,2854,2718,3000,4136,2864,2618,2700,2,38,27,37,15,14,3,12,13])). % 202.16/202.21 cnf(4221,plain, % 202.16/202.21 (E(f8(x42211,f3(a1,a2)),f8(x42211,f3(a2,a1)))), % 202.16/202.21 inference(scs_inference,[],[2546,2])). % 202.16/202.21 cnf(4228,plain, % 202.16/202.21 (P2(f4(a1,a1,a2),f8(f4(a2,a1,a1),a1))), % 202.16/202.21 inference(scs_inference,[],[44,4136,4171,105,2008,2546,2,27,38,37,15])). % 202.16/202.21 cnf(4229,plain, % 202.16/202.21 (E(x42291,f8(x42291,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4231,plain, % 202.16/202.21 (E(x42311,f8(x42311,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4232,plain, % 202.16/202.21 (E(f8(f8(x42321,f4(a2,a1,a1)),a1),f8(x42321,f4(a1,a2,a2)))), % 202.16/202.21 inference(scs_inference,[],[20,44,4229,2569,4136,4171,105,2008,2546,2,27,38,37,15,14,3])). % 202.16/202.21 cnf(4235,plain, % 202.16/202.21 (E(x42351,f8(x42351,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4236,plain, % 202.16/202.21 (P3(f8(f3(f8(a5,a2),f8(a1,x42361)),a1),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,4229,4231,4235,2854,2870,2569,4136,4171,105,2008,2546,2,27,38,37,15,14,3,13,12])). % 202.16/202.21 cnf(4238,plain, % 202.16/202.21 (P3(f4(a5,a1,f8(a1,x42381)),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,4229,4231,4235,42,2854,2870,2569,4136,4171,105,2008,2546,2002,2,27,38,37,15,14,3,13,12,34])). % 202.16/202.21 cnf(4265,plain, % 202.16/202.21 (E(x42651,f8(x42651,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4267,plain, % 202.16/202.21 (E(x42671,f8(x42671,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4270,plain, % 202.16/202.21 (P3(f8(f3(f8(a5,a9),f8(a1,x42701)),a1),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,4265,4267,2870,1615,4171,4203,2028,2567,2790,2,38,27,37,15,14,3,12])). % 202.16/202.21 cnf(4271,plain, % 202.16/202.21 (E(x42711,f8(x42711,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4274,plain, % 202.16/202.21 (~P1(f8(f8(f8(a5,a9),f8(a1,x42741)),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4265,4267,4271,2870,4136,1615,4171,4203,2028,2567,2790,110,2,38,27,37,15,14,3,12,13,11])). % 202.16/202.21 cnf(4296,plain, % 202.16/202.21 (P2(f4(a1,a1,a1),f8(f4(a1,a2,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[44,4203,4238,2132,2628,2795,2,27,38,37,15])). % 202.16/202.21 cnf(4297,plain, % 202.16/202.21 (E(x42971,f8(x42971,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4298,plain, % 202.16/202.21 (E(f8(f8(x42981,f8(a2,x42982)),a1),f8(x42981,f8(a1,x42983)))), % 202.16/202.21 inference(scs_inference,[],[20,44,2416,4203,4238,2132,2628,2795,2,27,38,37,15,3])). % 202.16/202.21 cnf(4301,plain, % 202.16/202.21 (E(x43011,f8(x43011,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4302,plain, % 202.16/202.21 (P3(f8(f4(a5,a2,a2),a1),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4297,4301,4171,2416,4203,4238,2132,2628,2795,2,27,38,37,15,3,14,13])). % 202.16/202.21 cnf(4303,plain, % 202.16/202.21 (E(x43031,f8(x43031,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4304,plain, % 202.16/202.21 (P3(f8(f4(a5,a2,f8(a1,x43041)),a1),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,4297,4301,4303,4136,4171,2416,4203,4238,2132,2628,2795,2,27,38,37,15,3,14,13,12])). % 202.16/202.21 cnf(4335,plain, % 202.16/202.21 (E(x43351,f8(x43351,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4336,plain, % 202.16/202.21 (E(f8(f8(f8(x43361,a2),a1),a1),f8(x43361,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,3053,4238,4236,2143,4232,2809,2,38,27,37,15,3])). % 202.16/202.21 cnf(4338,plain, % 202.16/202.21 (P2(f8(f4(a1,a1,a2),a1),f4(a1,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4335,3053,4238,4236,2143,4232,2809,2,38,27,37,15,3,14])). % 202.16/202.21 cnf(4339,plain, % 202.16/202.21 (E(x43391,f8(x43391,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4340,plain, % 202.16/202.21 (P3(f8(f3(f8(a5,a9),a1),a1),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4335,4339,4203,3053,4238,4236,2143,4232,2809,2,38,27,37,15,3,14,13])). % 202.16/202.21 cnf(4341,plain, % 202.16/202.21 (E(x43411,f8(x43411,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4342,plain, % 202.16/202.21 (P3(f8(f3(a5,a1),a1),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4335,4339,4341,2353,4203,3053,4238,4236,2143,4232,2809,2,38,27,37,15,3,14,13,12])). % 202.16/202.21 cnf(4344,plain, % 202.16/202.21 (P1(f8(f8(a1,f4(a2,a1,a1)),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4335,4339,4341,123,2353,4203,3053,4238,4236,2143,4232,2809,2,38,27,37,15,3,14,13,12,11])). % 202.16/202.21 cnf(4376,plain, % 202.16/202.21 (E(x43761,f8(x43761,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4377,plain, % 202.16/202.21 (E(f8(f8(x43771,f8(a1,x43772)),a1),f8(x43771,a2))), % 202.16/202.21 inference(scs_inference,[],[20,44,2408,4236,4270,4298,2149,2834,2,38,27,37,15,3])). % 202.16/202.21 cnf(4380,plain, % 202.16/202.21 (E(x43801,f8(x43801,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4382,plain, % 202.16/202.21 (E(x43821,f8(x43821,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4383,plain, % 202.16/202.21 (P3(f8(f3(f8(a5,a1),a1),a1),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4376,4380,4382,2847,4238,2408,4236,4270,4298,2149,2834,2,38,27,37,15,3,14,13,12])). % 202.16/202.21 cnf(4387,plain, % 202.16/202.21 (P3(f4(f8(a7,a1),a1,a2),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4376,4380,4382,56,948,2847,4238,2408,4236,4270,4298,2149,4336,2834,2900,2,38,27,37,15,3,14,13,12,11,34])). % 202.16/202.21 cnf(4392,plain, % 202.16/202.21 (P3(f4(a5,a9,a1),f8(a5,f8(a2,x43921)))), % 202.16/202.21 inference(scs_inference,[],[20,44,4376,4380,4382,56,18,80,948,2847,4238,2408,4236,4270,4298,2149,4304,4336,2834,2900,2,38,27,37,15,3,14,13,12,11,34,29,30])). % 202.16/202.21 cnf(4417,plain, % 202.16/202.21 (E(x44171,f8(x44171,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4418,plain, % 202.16/202.21 (E(f8(f8(f8(x44181,f8(a2,x44182)),a1),a1),f8(x44181,f8(a1,x44183)))), % 202.16/202.21 inference(scs_inference,[],[20,44,4298,4270,4304,4336,2150,2873,2,38,27,37,15,3])). % 202.16/202.21 cnf(4421,plain, % 202.16/202.21 (E(x44211,f8(x44211,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4423,plain, % 202.16/202.21 (E(x44231,f8(x44231,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4428,plain, % 202.16/202.21 (P3(f4(f8(f8(a1,x44281),x44282),x44283,f8(a7,a1)),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4417,4421,4423,58,4238,4236,4298,4270,4304,4336,2150,355,4377,2873,2918,2,38,27,37,15,3,14,13,12,11,34])). % 202.16/202.21 cnf(4445,plain, % 202.16/202.21 (E(f8(x44451,a2),f8(f8(x44451,f8(a1,x44452)),a1))), % 202.16/202.21 inference(scs_inference,[],[4377,2])). % 202.16/202.21 cnf(4453,plain, % 202.16/202.21 (E(x44531,f8(x44531,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4454,plain, % 202.16/202.21 (E(f8(f8(f8(f8(x44541,a2),a1),a1),a1),f8(x44541,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4336,4304,4377,2155,4169,3144,2,38,27,37,15,3])). % 202.16/202.21 cnf(4457,plain, % 202.16/202.21 (E(x44571,f8(x44571,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4459,plain, % 202.16/202.21 (E(x44591,f8(x44591,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4464,plain, % 202.16/202.21 (P3(f4(f8(a7,a1),f8(f8(a2,x44641),x44642),f8(f8(a2,x44641),x44642)),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4453,4457,4459,269,2843,4270,4336,4304,3302,4377,2155,4169,4418,3144,3189,3036,2,38,27,37,15,3,14,13,11,12,34])). % 202.16/202.21 cnf(4481,plain, % 202.16/202.21 (E(f8(x44811,f8(a1,x44812)),f8(f8(f8(x44811,f8(a2,x44813)),a1),a1))), % 202.16/202.21 inference(scs_inference,[],[4418,2])). % 202.16/202.21 cnf(4489,plain, % 202.16/202.21 (E(x44891,f8(x44891,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4490,plain, % 202.16/202.21 (E(f8(f8(f8(x44901,f8(a1,x44902)),a1),a1),f8(x44901,a2))), % 202.16/202.21 inference(scs_inference,[],[20,44,4377,1779,4418,2184,4302,3229,2,38,27,37,15,3])). % 202.16/202.21 cnf(4493,plain, % 202.16/202.21 (E(x44931,f8(x44931,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4495,plain, % 202.16/202.21 (E(x44951,f8(x44951,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4500,plain, % 202.16/202.21 (P3(f4(a5,a1,a2),a5)), % 202.16/202.21 inference(scs_inference,[],[20,44,4489,4493,4495,56,948,4377,4304,3000,1779,4418,2184,4302,4454,3229,3330,1879,2,38,27,37,15,3,14,13,11,12,34])). % 202.16/202.21 cnf(4531,plain, % 202.16/202.21 (E(x45311,f8(x45311,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4535,plain, % 202.16/202.21 (E(x45351,f8(x45351,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4537,plain, % 202.16/202.21 (E(x45371,f8(x45371,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4542,plain, % 202.16/202.21 (P3(f4(a6,a1,a2),a6)), % 202.16/202.21 inference(scs_inference,[],[20,44,4531,4535,4537,56,3000,2345,2413,355,1745,4454,2190,4340,4490,3361,3395,2049,2,38,27,37,15,3,14,13,11,12,34])). % 202.16/202.21 cnf(4545,plain, % 202.16/202.21 (P3(f4(a5,a1,a2),a7)), % 202.16/202.21 inference(scs_inference,[],[20,44,4531,4535,4537,56,18,3000,2345,2413,355,1745,4454,2190,4340,4500,4490,3361,3395,2049,2,38,27,37,15,3,14,13,11,12,34,29])). % 202.16/202.21 cnf(4571,plain, % 202.16/202.21 (E(x45711,f8(x45711,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4574,plain, % 202.16/202.21 (E(f8(f8(f8(f8(f8(x45741,a2),a1),a1),a1),a1),f8(x45741,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4571,4454,3339,4500,4490,2196,3425,3451,2,38,27,37,15,14,3])). % 202.16/202.21 cnf(4609,plain, % 202.16/202.21 (E(f8(f8(f8(f8(x46091,f8(a1,x46092)),a1),a1),a1),f8(x46091,a2))), % 202.16/202.21 inference(scs_inference,[],[20,4490,4500,2204,4128,4383,2,38,27,37,3])). % 202.16/202.21 cnf(4612,plain, % 202.16/202.21 (E(x46121,f8(x46121,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4614,plain, % 202.16/202.21 (E(x46141,f8(x46141,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4616,plain, % 202.16/202.21 (E(x46161,f8(x46161,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4617,plain, % 202.16/202.21 (P1(f8(f8(a1,x46171),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4612,4614,4490,407,4500,2204,4128,4383,3483,3515,4344,2406,2,38,27,37,3,15,14,13,11])). % 202.16/202.21 cnf(4621,plain, % 202.16/202.21 (P3(f4(a2,x46211,f8(a5,a9)),f8(a5,a9))), % 202.16/202.21 inference(scs_inference,[],[20,44,4612,4614,4616,56,1548,4490,407,4500,2204,4128,4383,3483,3515,4344,2161,2406,2,38,27,37,3,15,14,13,11,12,34])). % 202.16/202.21 cnf(4641,plain, % 202.16/202.21 (E(f8(x46411,a1),f8(f8(f8(f8(f8(x46411,a2),a1),a1),a1),a1))), % 202.16/202.21 inference(scs_inference,[],[4574,2])). % 202.16/202.21 cnf(4649,plain, % 202.16/202.21 (E(x46491,f8(x46491,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4651,plain, % 202.16/202.21 (E(x46511,f8(x46511,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4654,plain, % 202.16/202.21 (P3(f4(a5,a1,a2),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4649,4651,4500,2417,3111,4574,2267,4387,3543,3572,2,38,27,37,15,14,3,13])). % 202.16/202.21 cnf(4655,plain, % 202.16/202.21 (E(x46551,f8(x46551,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4660,plain, % 202.16/202.21 (P3(f4(a2,x46601,f8(a5,a1)),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4649,4651,4655,56,4500,355,2417,3111,4574,2267,4387,4609,3543,3572,2193,2,38,27,37,15,14,3,13,11,12,34])). % 202.16/202.21 cnf(4689,plain, % 202.16/202.21 (E(x46891,f8(x46891,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4691,plain, % 202.16/202.21 (E(x46911,f8(x46911,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4695,plain, % 202.16/202.21 (E(x46951,f8(x46951,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4701,plain, % 202.16/202.21 (P3(f4(a2,x47011,f8(a5,a2)),f8(a5,a2))), % 202.16/202.21 inference(scs_inference,[],[20,44,4689,4691,4695,56,123,1745,307,2535,3148,4609,2273,4654,4660,4641,3707,3609,2362,2,38,27,37,2226,14,15,3,13,11,12,34])). % 202.16/202.21 cnf(4726,plain, % 202.16/202.21 (E(x47261,f8(x47261,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4728,plain, % 202.16/202.21 (E(x47281,f8(x47281,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4732,plain, % 202.16/202.21 (E(x47321,f8(x47321,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4733,plain, % 202.16/202.21 (P1(f8(f8(a2,x47331),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4726,4728,145,2759,4654,4660,2377,4201,3742,3780,4617,2414,2,38,27,37,15,14,3,13,11])). % 202.16/202.21 cnf(4740,plain, % 202.16/202.21 (P3(f4(a2,x47401,f8(a6,a2)),f8(a6,a2))), % 202.16/202.21 inference(scs_inference,[],[20,44,4726,4728,4732,56,307,145,2759,4654,4660,2377,4201,3036,3742,3780,4617,2414,2530,2,38,27,37,15,14,3,13,11,12,25,34])). % 202.16/202.21 cnf(4813,plain, % 202.16/202.21 (E(x48131,f8(x48131,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4815,plain, % 202.16/202.21 (E(x48151,f8(x48151,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4816,plain, % 202.16/202.21 (E(f8(f8(x48161,a2),a1),f8(f8(x48161,f8(a1,x48162)),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4813,3224,4445,2462,2999,4545,3920,3880,2,38,27,37,14,15,3])). % 202.16/202.21 cnf(4817,plain, % 202.16/202.21 (E(f8(x48171,a1),x48171)), % 202.16/202.21 inference(rename_variables,[],[20])). % 202.16/202.21 cnf(4825,plain, % 202.16/202.21 (~P3(x48251,a1)), % 202.16/202.21 inference(rename_variables,[],[40])). % 202.16/202.21 cnf(4829,plain, % 202.16/202.21 (P3(f4(a5,a9,a1),f8(f8(a5,a2),a1))), % 202.16/202.21 inference(scs_inference,[],[20,4817,44,4813,4815,40,4825,18,80,4660,3224,4445,2462,2999,4545,3920,3880,4733,3027,409,2,38,27,37,14,15,3,13,11,12,34,29,32])). % 202.16/202.21 cnf(4847,plain, % 202.16/202.21 (E(x48471,f8(x48471,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4850,plain, % 202.16/202.21 (E(f8(f8(x48501,f8(a1,x48502)),a1),f8(f8(f8(x48501,f8(a2,x48503)),a1),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4847,4481,3464,2622,2574,4542,4126,4097,2,38,27,37,14,15,3])). % 202.16/202.21 cnf(4880,plain, % 202.16/202.21 (E(x48801,f8(x48801,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4881,plain, % 202.16/202.21 (E(f8(f8(f8(x48811,f4(a2,a1,a1)),a1),a1),f8(x48811,f4(a1,a1,a2)))), % 202.16/202.21 inference(scs_inference,[],[20,44,4128,3290,4816,2608,4428,4163,2,38,27,37,14,3])). % 202.16/202.21 cnf(4884,plain, % 202.16/202.21 (E(x48841,f8(x48841,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4885,plain, % 202.16/202.21 (P3(f8(f4(a5,a9,a1),a1),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4880,4884,92,4128,3290,4816,2608,4428,4199,4163,2,38,27,37,14,3,15,13])). % 202.16/202.21 cnf(4901,plain, % 202.16/202.21 (E(f8(f8(f8(x49011,f8(a2,x49012)),a1),a1),f8(f8(x49011,f8(a1,x49013)),a1))), % 202.16/202.21 inference(scs_inference,[],[4850,2])). % 202.16/202.21 cnf(4910,plain, % 202.16/202.21 (E(f8(f8(x49101,f3(a1,a2)),a1),f8(x49101,f3(a2,a1)))), % 202.16/202.21 inference(scs_inference,[],[20,44,4221,3404,4850,2211,4464,4228,2,38,27,37,14,3])). % 202.16/202.21 cnf(4943,plain, % 202.16/202.21 (E(x49431,f8(x49431,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4944,plain, % 202.16/202.21 (E(f8(f8(f8(x49441,a2),a1),a1),f8(f8(x49441,f8(a1,x49442)),a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4816,3432,2217,4881,4701,4296,2,38,27,37,14,3])). % 202.16/202.21 cnf(4947,plain, % 202.16/202.21 (E(x49471,f8(x49471,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4948,plain, % 202.16/202.21 (P3(f4(a5,a1,a1),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4943,4947,3464,4816,3432,2217,4881,4701,4338,4296,2,38,27,37,14,3,15,13])). % 202.16/202.21 cnf(4949,plain, % 202.16/202.21 (E(x49491,f8(x49491,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(4952,plain, % 202.16/202.21 (P3(f8(f4(f8(a7,a1),a1,a1),a1),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,4943,4947,4949,3464,3290,4274,4816,3432,2217,4881,4701,4901,4338,4296,2,38,27,37,14,3,15,13,11,12])). % 202.16/202.21 cnf(5009,plain, % 202.16/202.21 (E(x50091,f8(x50091,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5010,plain, % 202.16/202.21 (P3(f4(a6,a2,a2),f8(a6,a1))), % 202.16/202.21 inference(scs_inference,[],[23,20,44,5009,3404,4910,4948,4944,1954,4952,3060,3087,2,38,27,37,14,3,15,13])). % 202.16/202.21 cnf(5058,plain, % 202.16/202.21 (E(f8(f8(f8(f8(x50581,a2),a1),a1),a1),f8(f8(x50581,f8(a1,x50582)),a1))), % 202.16/202.21 inference(scs_inference,[],[23,20,4944,4545,2000,2503,5010,3129,2,38,27,37,14,3])). % 202.16/202.21 cnf(5061,plain, % 202.16/202.21 (E(x50611,f8(x50611,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5062,plain, % 202.16/202.21 (P3(f4(a6,a2,a1),f8(a6,a1))), % 202.16/202.21 inference(scs_inference,[],[23,20,44,5061,3432,4944,4545,2000,2503,5010,3107,3129,2,38,27,37,14,3,15,13])). % 202.16/202.21 cnf(5063,plain, % 202.16/202.21 (E(x50631,f8(x50631,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5065,plain, % 202.16/202.21 (P3(f8(f4(a5,a1,a1),a1),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[23,20,44,5061,5063,4274,3432,4944,4948,4545,2000,2503,5010,3107,3129,2,38,27,37,14,3,15,13,11,12])). % 202.16/202.21 cnf(5133,plain, % 202.16/202.21 (E(x51331,f8(x51331,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5137,plain, % 202.16/202.21 (E(x51371,f8(x51371,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5138,plain, % 202.16/202.21 (P3(f4(a6,a1,a1),f8(a6,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,5133,5137,3491,2503,5062,5058,2966,2380,5065,3267,2,38,27,37,14,3,15,13])). % 202.16/202.21 cnf(5163,plain, % 202.16/202.21 (E(x51631,f8(x51631,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5165,plain, % 202.16/202.21 (E(x51651,f8(x51651,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5169,plain, % 202.16/202.21 (E(x51691,f8(x51691,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5170,plain, % 202.16/202.21 (P3(f8(f4(a6,a2,a1),a1),f8(a6,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,5163,5165,5169,3111,5062,3323,3576,1794,2951,5138,3678,3298,2,38,27,37,14,15,3,13,12])). % 202.16/202.21 cnf(5220,plain, % 202.16/202.21 (E(x52201,f8(x52201,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5222,plain, % 202.16/202.21 (E(x52221,f8(x52221,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5225,plain, % 202.16/202.21 (P3(f4(a7,f8(x52251,a7),f8(a1,x52252)),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,5220,5222,1480,2999,4383,1923,2893,5170,4031,4002,2,38,27,37,14,15,3,13])). % 202.16/202.21 cnf(5272,plain, % 202.16/202.21 (E(x52721,f8(x52721,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5273,plain, % 202.16/202.21 (E(f8(f8(f4(a2,a2,a1),x52731),a1),f8(f4(a1,a1,a2),x52731))), % 202.16/202.21 inference(scs_inference,[],[23,20,44,2628,4542,1877,2954,4740,3170,2298,2,38,27,37,14,15,3])). % 202.16/202.21 cnf(5276,plain, % 202.16/202.21 (E(x52761,f8(x52761,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5277,plain, % 202.16/202.21 (P3(f8(f4(f8(a7,a1),a1,a2),a1),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[23,20,44,5272,5276,1437,2628,4387,4542,1877,2954,4740,3170,2298,2,38,27,37,14,15,3,13,12])). % 202.16/202.21 cnf(5309,plain, % 202.16/202.21 (P2(f8(f3(a1,a2),a1),f3(a1,a1))), % 202.16/202.21 inference(scs_inference,[],[44,3132,5065,2298,3002,4621,2,38,27,37,28,14])). % 202.16/202.21 cnf(5311,plain, % 202.16/202.21 (E(f8(f8(f4(a2,a1,x53111),x53112),a1),f8(f4(a1,a2,x53111),x53112))), % 202.16/202.21 inference(scs_inference,[],[20,44,2483,3132,5065,2298,3002,4621,2,38,27,37,28,14,3])). % 202.16/202.21 cnf(5335,plain, % 202.16/202.21 (E(x53351,f8(x53351,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5339,plain, % 202.16/202.21 (E(x53391,f8(x53391,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5340,plain, % 202.16/202.21 (P3(f4(a6,a1,a2),f8(a6,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,5335,5339,4542,2698,4952,2753,5273,2547,5277,5309,2,38,27,37,14,3,15,13])). % 202.16/202.21 cnf(5387,plain, % 202.16/202.21 (P2(f8(f4(a2,a1,a2),a1),f4(a2,a2,a1))), % 202.16/202.21 inference(scs_inference,[],[44,5340,2602,2604,2555,5225,2,38,37,27,14])). % 202.16/202.21 cnf(5388,plain, % 202.16/202.21 (E(x53881,f8(x53881,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5390,plain, % 202.16/202.21 (E(x53901,f8(x53901,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5394,plain, % 202.16/202.21 (E(x53941,f8(x53941,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5395,plain, % 202.16/202.21 (P3(f8(f4(a5,a1,a2),a1),f8(a5,a1))), % 202.16/202.21 inference(scs_inference,[],[20,44,5388,5390,5394,5273,1535,4654,5340,2602,2604,2555,5225,2638,2,38,37,27,14,15,3,13,12])). % 202.16/202.21 cnf(5420,plain, % 202.16/202.21 (E(x54201,f8(x54201,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5422,plain, % 202.16/202.21 (E(x54221,f8(x54221,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5424,plain, % 202.16/202.21 (E(f8(x54241,a1),x54241)), % 202.16/202.21 inference(rename_variables,[],[20])). % 202.16/202.21 cnf(5427,plain, % 202.16/202.21 (P3(f8(f4(a6,a1,a2),a1),f8(a6,a1))), % 202.16/202.21 inference(scs_inference,[],[20,5424,44,5420,5422,5311,5340,4383,5170,2638,2626,2671,5395,5387,2,38,37,27,14,15,3,13,12])). % 202.16/202.21 cnf(5515,plain, % 202.16/202.21 (E(x55151,f8(x55151,a1))), % 202.16/202.21 inference(rename_variables,[],[44])). % 202.16/202.21 cnf(5516,plain, % 202.16/202.21 (E(x55161,f8(x55161,a2))), % 202.16/202.21 inference(scs_inference,[],[44,5515,2420,3521,3461,38,13,3])). % 202.16/202.21 cnf(5518,plain, % 202.16/202.21 (E(f8(x55181,a2),x55181)), % 202.16/202.21 inference(scs_inference,[],[44,5515,2420,3521,3461,38,13,3,2])). % 202.16/202.21 cnf(5570,plain, % 202.16/202.21 (P3(f4(a7,a9,a2),f8(a7,a1))), % 202.16/202.21 inference(scs_inference,[],[44,3890,13])). % 202.16/202.21 cnf(5663,plain, % 202.34/202.21 (~P3(f3(f8(a5,a9),f8(a7,a9)),f8(a7,a9))), % 202.34/202.21 inference(scs_inference,[],[23,5395,5570,3927,3890,2234,1928,2176,1768,33])). % 202.34/202.21 cnf(5672,plain, % 202.34/202.21 (E(f8(x56721,f8(x56722,a1)),f8(x56721,x56722))), % 202.34/202.21 inference(scs_inference,[],[23,20,5395,5570,4733,3927,3890,2234,1928,2176,1768,33,9,8,7,24,6,10,5])). % 202.34/202.21 cnf(5675,plain, % 202.34/202.21 (~P3(x56751,a1)), % 202.34/202.21 inference(rename_variables,[],[40])). % 202.34/202.21 cnf(5683,plain, % 202.34/202.21 (P3(f3(f8(a5,a9),f8(a7,a9)),f8(a5,a9))), % 202.34/202.21 inference(scs_inference,[],[23,20,4885,4829,4140,2960,613,5395,915,5570,4733,3927,3890,40,2234,1928,2176,1768,33,9,8,7,24,6,10,5,4,39,30,32,26,28])). % 202.34/202.21 cnf(5693,plain, % 202.34/202.21 (E(a1,f8(f8(a1,x56931),x56932))), % 202.34/202.21 inference(scs_inference,[],[23,20,3489,4885,4829,4140,2960,3657,613,4621,5395,915,5570,4733,3927,3890,40,5675,42,2234,1928,2176,1768,33,9,8,7,24,6,10,5,4,39,30,32,26,28,37,31,27,38,34])). % 202.34/202.21 cnf(5733,plain, % 202.34/202.21 (P3(f3(f8(a5,a9),f8(a7,a9)),a5)), % 202.34/202.21 inference(scs_inference,[],[19,5663,5683,4392,2315,2269,5518,4660,2944,40,33,2176,8,7,6,5,9,10,4,39,30,32,26,28,37])). % 202.34/202.21 cnf(5739,plain, % 202.34/202.21 (~P3(f3(f8(a5,a9),f8(a7,a9)),a9)), % 202.34/202.21 inference(scs_inference,[],[19,4066,5663,5683,4392,2315,2269,5518,4660,2944,40,33,2176,8,7,6,5,9,10,4,39,30,32,26,28,37,31,27,38])). % 202.34/202.21 cnf(5768,plain, % 202.34/202.21 (~P3(x57681,a1)), % 202.34/202.21 inference(rename_variables,[],[40])). % 202.34/202.21 cnf(5770,plain, % 202.34/202.21 (~E(a1,f8(f8(a5,a1),a1))), % 202.34/202.21 inference(scs_inference,[],[4342,3784,2278,5518,4205,3669,40,5768,33,2176,6,8,7,4,9,5,10,39,32])). % 202.34/202.21 cnf(5776,plain, % 202.34/202.21 (P3(f3(f8(a5,a9),a1),f8(a5,a9))), % 202.34/202.21 inference(scs_inference,[],[4342,3784,3703,2333,2278,5518,4205,3669,1896,40,5768,33,2176,6,8,7,4,9,5,10,39,32,30,28])). % 202.34/202.21 cnf(5830,plain, % 202.34/202.21 (P2(x58301,x58301)), % 202.34/202.21 inference(rename_variables,[],[21])). % 202.34/202.21 cnf(5831,plain, % 202.34/202.21 (P2(f4(x58311,x58312,a2),f4(x58311,x58312,a1))), % 202.34/202.21 inference(scs_inference,[],[21,5830,3421,5518,3042,2759,12,15,14])). % 202.34/202.21 cnf(5837,plain, % 202.34/202.21 (~P3(f8(a6,a2),f4(a6,a2,a1))), % 202.34/202.21 inference(scs_inference,[],[3641,5518,12])). % 202.34/202.21 cnf(5872,plain, % 202.34/202.21 (~P3(f8(a6,a2),f4(a6,a2,a2))), % 202.34/202.21 inference(scs_inference,[],[5837,5831,29])). % 202.34/202.21 cnf(5943,plain, % 202.34/202.21 ($false), % 202.34/202.21 inference(scs_inference,[],[18,1556,3328,5776,5872,3191,3235,5663,3288,5770,5672,4089,5733,5739,5693,5427,3640,3355,3669,5516,40,16,9,8,10,6,7,28,5,38,4,37,27,2,34,11,14,15,13,12,31,30,25,3,39,29]), % 202.34/202.21 ['proof']). % 202.34/202.21 % SZS output end Proof % 202.34/202.21 % Total time :201.420000s %------------------------------------------------------------------------------