%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET908+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 14:22:56 EDT 2024 % Result : Theorem 105.99s 106.02s % Output : CNFRefutation 106.04s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SET908+1 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 15:37:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 105.96/106.00 %------------------------------------------- % 105.96/106.00 % File :CSE---1.7 % 105.96/106.00 % Problem :theBenchmark % 105.96/106.00 % Transform :cnf % 105.96/106.00 % Format :tptp:raw % 105.96/106.00 % Command :java -jar mcs_scs.jar %d %s % 105.96/106.00 % 105.96/106.00 % Result :Theorem 105.380000s % 105.96/106.00 % Output :CNFRefutation 105.380000s % 105.96/106.00 %------------------------------------------- % 105.99/106.01 %------------------------------------------------------------------------------ % 105.99/106.01 % File : SET908+1 : TPTP v8.2.0. Released v3.2.0. % 105.99/106.01 % Domain : Set theory % 105.99/106.01 % Problem : union(singleton(A),B) != empty_set % 105.99/106.01 % Version : [Urb06] axioms : Especial. % 105.99/106.01 % English : % 105.99/106.01 % 105.99/106.01 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 105.99/106.01 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 105.99/106.01 % Source : [Urb06] % 105.99/106.01 % Names : zfmisc_1__t49_zfmisc_1 [Urb06] % 105.99/106.01 % 105.99/106.01 % Status : Theorem % 105.99/106.01 % Rating : 0.11 v8.2.0, 0.14 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.07 v7.1.0, 0.04 v7.0.0, 0.00 v6.4.0, 0.04 v6.3.0, 0.12 v6.2.0, 0.28 v6.1.0, 0.30 v5.5.0, 0.22 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.05 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v3.7.0, 0.10 v3.5.0, 0.11 v3.4.0, 0.16 v3.3.0, 0.14 v3.2.0 % 105.99/106.01 % Syntax : Number of formulae : 12 ( 6 unt; 0 def) % 105.99/106.01 % Number of atoms : 21 ( 7 equ) % 105.99/106.01 % Maximal formula atoms : 4 ( 1 avg) % 105.99/106.01 % Number of connectives : 17 ( 8 ~; 1 |; 0 &) % 105.99/106.01 % ( 5 <=>; 3 =>; 0 <=; 0 <~>) % 105.99/106.01 % Maximal formula depth : 8 ( 4 avg) % 105.99/106.01 % Maximal term depth : 3 ( 1 avg) % 105.99/106.01 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 105.99/106.01 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 105.99/106.01 % Number of variables : 23 ( 21 !; 2 ?) % 105.99/106.01 % SPC : FOF_THM_RFO_SEQ % 105.99/106.01 % 105.99/106.01 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 105.99/106.01 % library, www.mizar.org % 105.99/106.01 %------------------------------------------------------------------------------ % 105.99/106.01 fof(antisymmetry_r2_hidden,axiom, % 105.99/106.01 ! [A,B] : % 105.99/106.01 ( in(A,B) % 105.99/106.01 => ~ in(B,A) ) ). % 105.99/106.01 % 105.99/106.01 fof(commutativity_k2_xboole_0,axiom, % 105.99/106.01 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 105.99/106.01 % 105.99/106.01 fof(d1_tarski,axiom, % 105.99/106.01 ! [A,B] : % 105.99/106.01 ( B = singleton(A) % 105.99/106.01 <=> ! [C] : % 105.99/106.01 ( in(C,B) % 105.99/106.01 <=> C = A ) ) ). % 105.99/106.01 % 105.99/106.01 fof(d1_xboole_0,axiom, % 105.99/106.01 ! [A] : % 105.99/106.01 ( A = empty_set % 105.99/106.01 <=> ! [B] : ~ in(B,A) ) ). % 105.99/106.01 % 105.99/106.01 fof(d2_xboole_0,axiom, % 105.99/106.01 ! [A,B,C] : % 105.99/106.01 ( C = set_union2(A,B) % 105.99/106.01 <=> ! [D] : % 105.99/106.02 ( in(D,C) % 105.99/106.02 <=> ( in(D,A) % 105.99/106.02 | in(D,B) ) ) ) ). % 105.99/106.02 % 105.99/106.02 fof(fc1_xboole_0,axiom, % 105.99/106.02 empty(empty_set) ). % 105.99/106.02 % 105.99/106.02 fof(fc2_xboole_0,axiom, % 105.99/106.02 ! [A,B] : % 105.99/106.02 ( ~ empty(A) % 105.99/106.02 => ~ empty(set_union2(A,B)) ) ). % 105.99/106.02 % 105.99/106.02 fof(fc3_xboole_0,axiom, % 105.99/106.02 ! [A,B] : % 105.99/106.02 ( ~ empty(A) % 105.99/106.02 => ~ empty(set_union2(B,A)) ) ). % 105.99/106.02 % 105.99/106.02 fof(idempotence_k2_xboole_0,axiom, % 105.99/106.02 ! [A,B] : set_union2(A,A) = A ). % 105.99/106.02 % 105.99/106.02 fof(rc1_xboole_0,axiom, % 105.99/106.02 ? [A] : empty(A) ). % 105.99/106.02 % 105.99/106.02 fof(rc2_xboole_0,axiom, % 105.99/106.02 ? [A] : ~ empty(A) ). % 105.99/106.02 % 105.99/106.02 fof(t49_zfmisc_1,conjecture, % 105.99/106.02 ! [A,B] : set_union2(singleton(A),B) != empty_set ). % 105.99/106.02 % 105.99/106.02 %------------------------------------------------------------------------------ % 105.99/106.02 %------------------------------------------- % 105.99/106.02 % Proof found % 105.99/106.02 % SZS status Theorem for theBenchmark % 105.99/106.02 % SZS output start Proof % 105.99/106.02 %ClaNum:36(EqnAxiom:15) % 105.99/106.02 %VarNum:111(SingletonVarNum:43) % 105.99/106.02 %MaxLitNum:4 % 105.99/106.02 %MaxfuncDepth:2 % 105.99/106.02 %SharedTerms:11 % 105.99/106.02 %goalClause: 19 % 105.99/106.02 %singleGoalClaCount:1 % 105.99/106.02 [16]P1(a1) % 105.99/106.02 [17]P1(a2) % 105.99/106.02 [21]~P1(a8) % 105.99/106.02 [19]E(f6(f10(a7),a9),a1) % 105.99/106.02 [18]E(f6(x181,x181),x181) % 105.99/106.02 [20]E(f6(x201,x202),f6(x202,x201)) % 105.99/106.02 [22]P2(f3(x221),x221)+E(x221,a1) % 105.99/106.02 [23]~P2(x232,x231)+~E(x231,a1) % 105.99/106.02 [26]~P2(x262,x261)+~P2(x261,x262) % 105.99/106.02 [27]P1(x271)+~P1(f6(x272,x271)) % 105.99/106.02 [28]P1(x281)+~P1(f6(x281,x282)) % 105.99/106.02 [29]E(f4(x292,x291),x292)+P2(f4(x292,x291),x291)+E(x291,f10(x292)) % 105.99/106.02 [33]~E(f4(x332,x331),x332)+~P2(f4(x332,x331),x331)+E(x331,f10(x332)) % 105.99/106.02 [24]P2(x241,x242)+~E(x241,x243)+~E(x242,f10(x243)) % 105.99/106.02 [25]~P2(x251,x253)+E(x251,x252)+~E(x253,f10(x252)) % 105.99/106.02 [35]~P2(f5(x352,x353,x351),x351)+~P2(f5(x352,x353,x351),x353)+E(x351,f6(x352,x353)) % 105.99/106.02 [36]~P2(f5(x362,x363,x361),x361)+~P2(f5(x362,x363,x361),x362)+E(x361,f6(x362,x363)) % 105.99/106.02 [30]~P2(x301,x304)+P2(x301,x302)+~E(x302,f6(x303,x304)) % 105.99/106.02 [31]~P2(x311,x313)+P2(x311,x312)+~E(x312,f6(x313,x314)) % 105.99/106.02 [34]P2(f5(x342,x343,x341),x341)+P2(f5(x342,x343,x341),x343)+P2(f5(x342,x343,x341),x342)+E(x341,f6(x342,x343)) % 105.99/106.02 [32]~P2(x321,x324)+P2(x321,x322)+P2(x321,x323)+~E(x324,f6(x323,x322)) % 105.99/106.02 %EqnAxiom % 105.99/106.02 [1]E(x11,x11) % 105.99/106.02 [2]E(x22,x21)+~E(x21,x22) % 105.99/106.02 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 105.99/106.02 [4]~E(x41,x42)+E(f6(x41,x43),f6(x42,x43)) % 105.99/106.02 [5]~E(x51,x52)+E(f6(x53,x51),f6(x53,x52)) % 105.99/106.02 [6]~E(x61,x62)+E(f10(x61),f10(x62)) % 105.99/106.02 [7]~E(x71,x72)+E(f5(x71,x73,x74),f5(x72,x73,x74)) % 105.99/106.02 [8]~E(x81,x82)+E(f5(x83,x81,x84),f5(x83,x82,x84)) % 105.99/106.02 [9]~E(x91,x92)+E(f5(x93,x94,x91),f5(x93,x94,x92)) % 105.99/106.02 [10]~E(x101,x102)+E(f4(x101,x103),f4(x102,x103)) % 105.99/106.02 [11]~E(x111,x112)+E(f4(x113,x111),f4(x113,x112)) % 105.99/106.02 [12]~E(x121,x122)+E(f3(x121),f3(x122)) % 105.99/106.02 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 105.99/106.02 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 105.99/106.02 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 105.99/106.02 % 105.99/106.02 %------------------------------------------- % 106.04/106.03 cnf(37,plain, % 106.04/106.03 (~P2(x371,a1)), % 106.04/106.03 inference(equality_inference,[],[23])). % 106.04/106.03 cnf(38,plain, % 106.04/106.03 (~P2(x381,f10(x382))+E(x381,x382)), % 106.04/106.03 inference(equality_inference,[],[25])). % 106.04/106.03 cnf(39,plain, % 106.04/106.03 (~P2(x391,x392)+P2(x391,f6(x393,x392))), % 106.04/106.03 inference(equality_inference,[],[30])). % 106.04/106.03 cnf(40,plain, % 106.04/106.03 (~P2(x401,x402)+P2(x401,f6(x402,x403))), % 106.04/106.03 inference(equality_inference,[],[31])). % 106.04/106.03 cnf(41,plain, % 106.04/106.03 (~P2(x411,f6(x412,x413))+P2(x411,x413)+P2(x411,x412)), % 106.04/106.03 inference(equality_inference,[],[32])). % 106.04/106.03 cnf(42,plain, % 106.04/106.03 (~P2(x421,f6(f10(a7),a9))), % 106.04/106.03 inference(scs_inference,[],[19,23])). % 106.04/106.03 cnf(44,plain, % 106.04/106.03 (E(a1,f6(f10(a7),a9))), % 106.04/106.03 inference(scs_inference,[],[19,23,2])). % 106.04/106.03 cnf(45,plain, % 106.04/106.03 (P2(f6(f10(a7),a9),f6(f10(a1),f10(a1)))), % 106.04/106.03 inference(scs_inference,[],[19,18,23,2,24])). % 106.04/106.03 cnf(46,plain, % 106.04/106.03 (E(f6(x461,x461),x461)), % 106.04/106.03 inference(rename_variables,[],[18])). % 106.04/106.03 cnf(48,plain, % 106.04/106.03 (~P1(f6(a8,a8))), % 106.04/106.03 inference(scs_inference,[],[19,18,46,21,23,2,24,13])). % 106.04/106.03 cnf(49,plain, % 106.04/106.03 (E(f6(x491,x491),x491)), % 106.04/106.03 inference(rename_variables,[],[18])). % 106.04/106.03 cnf(50,plain, % 106.04/106.03 (~P2(x501,a9)), % 106.04/106.03 inference(scs_inference,[],[19,37,18,46,21,23,2,24,13,30])). % 106.04/106.03 cnf(52,plain, % 106.04/106.03 (~P2(x521,f10(a7))), % 106.04/106.04 inference(scs_inference,[],[19,37,18,46,21,23,2,24,13,30,31])). % 106.04/106.04 cnf(54,plain, % 106.04/106.04 (~P2(x541,f6(a1,a1))), % 106.04/106.04 inference(scs_inference,[],[19,37,18,46,21,23,2,24,13,30,31,41])). % 106.04/106.04 cnf(56,plain, % 106.04/106.04 (P2(a1,f6(f10(a1),f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[19,37,18,46,21,23,2,24,13,30,31,41,14])). % 106.04/106.04 cnf(58,plain, % 106.04/106.04 (~P2(x581,a1)), % 106.04/106.04 inference(rename_variables,[],[37])). % 106.04/106.04 cnf(59,plain, % 106.04/106.04 (~P2(x591,f6(f6(a1,a1),f6(a1,a1)))), % 106.04/106.04 inference(scs_inference,[],[19,37,58,18,46,49,21,23,2,24,13,30,31,41,14,15,32])). % 106.04/106.04 cnf(62,plain, % 106.04/106.04 (~P2(f6(f10(a1),f10(a1)),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[19,37,58,18,46,49,21,23,2,24,13,30,31,41,14,15,32,38])). % 106.04/106.04 cnf(64,plain, % 106.04/106.04 (~E(f6(f10(a1),f10(a1)),f6(f10(a7),a9))), % 106.04/106.04 inference(scs_inference,[],[19,37,58,18,46,49,21,23,2,24,13,30,31,41,14,15,32,38,3])). % 106.04/106.04 cnf(67,plain, % 106.04/106.04 (E(x671,f6(x671,x671))), % 106.04/106.04 inference(scs_inference,[],[18,2])). % 106.04/106.04 cnf(69,plain, % 106.04/106.04 (~P2(x691,f10(a7))), % 106.04/106.04 inference(rename_variables,[],[52])). % 106.04/106.04 cnf(72,plain, % 106.04/106.04 (E(f6(x721,x722),f6(x722,x721))), % 106.04/106.04 inference(rename_variables,[],[20])). % 106.04/106.04 cnf(73,plain, % 106.04/106.04 (P1(f6(f10(a7),a9))), % 106.04/106.04 inference(scs_inference,[],[42,64,44,52,20,16,18,2,41,3,13])). % 106.04/106.04 cnf(74,plain, % 106.04/106.04 (P2(f6(f10(a7),a9),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[42,64,45,44,52,20,72,16,18,2,41,3,13,32])). % 106.04/106.04 cnf(77,plain, % 106.04/106.04 (P1(a9)), % 106.04/106.04 inference(scs_inference,[],[42,64,45,44,52,20,72,16,18,2,41,3,13,32,27])). % 106.04/106.04 cnf(79,plain, % 106.04/106.04 (P1(f10(a7))), % 106.04/106.04 inference(scs_inference,[],[42,64,45,44,52,20,72,16,18,2,41,3,13,32,27,28])). % 106.04/106.04 cnf(81,plain, % 106.04/106.04 (P2(f6(f10(a7),a9),f6(x811,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[42,64,45,44,52,20,72,16,18,2,41,3,13,32,27,28,39])). % 106.04/106.04 cnf(83,plain, % 106.04/106.04 (P2(f6(f10(a7),a9),f6(f10(a1),x831))), % 106.04/106.04 inference(scs_inference,[],[42,64,45,44,52,20,72,16,18,2,41,3,13,32,27,28,39,40])). % 106.04/106.04 cnf(85,plain, % 106.04/106.04 (~E(f6(f10(a7),a9),f6(f10(a1),f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[42,64,45,44,52,62,20,72,16,18,2,41,3,13,32,27,28,39,40,14])). % 106.04/106.04 cnf(86,plain, % 106.04/106.04 (~E(f10(a1),f6(f10(a7),a9))), % 106.04/106.04 inference(scs_inference,[],[42,64,45,44,52,62,20,72,16,18,2,41,3,13,32,27,28,39,40,14,15])). % 106.04/106.04 cnf(88,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,f10(a1)),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[42,64,45,44,52,69,62,50,20,72,16,18,2,41,3,13,32,27,28,39,40,14,15,34])). % 106.04/106.04 cnf(95,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,f10(a1)),f6(x951,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[88,39])). % 106.04/106.04 cnf(99,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,f10(a1)),f6(f10(a1),x991))), % 106.04/106.04 inference(scs_inference,[],[88,39,26,40])). % 106.04/106.04 cnf(105,plain, % 106.04/106.04 (E(x1051,f6(x1051,x1051))), % 106.04/106.04 inference(rename_variables,[],[67])). % 106.04/106.04 cnf(106,plain, % 106.04/106.04 (P1(f6(a9,f10(a7)))), % 106.04/106.04 inference(scs_inference,[],[42,67,73,85,54,88,20,39,26,40,41,3,13])). % 106.04/106.04 cnf(107,plain, % 106.04/106.04 (E(f6(x1071,x1072),f6(x1072,x1071))), % 106.04/106.04 inference(rename_variables,[],[20])). % 106.04/106.04 cnf(108,plain, % 106.04/106.04 (P2(f6(a1,a1),f6(f10(a1),f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[42,67,105,73,56,85,54,88,20,39,26,40,41,3,13,14])). % 106.04/106.04 cnf(110,plain, % 106.04/106.04 (~E(f6(x1101,f10(a1)),f6(f10(a7),a9))), % 106.04/106.04 inference(scs_inference,[],[42,67,105,73,56,85,54,81,88,20,39,26,40,41,3,13,14,15])). % 106.04/106.04 cnf(112,plain, % 106.04/106.04 (P2(a1,f10(a1))), % 106.04/106.04 inference(scs_inference,[],[42,67,105,73,56,85,54,81,88,20,107,39,26,40,41,3,13,14,15,32])). % 106.04/106.04 cnf(115,plain, % 106.04/106.04 (~E(f10(a1),a9)), % 106.04/106.04 inference(scs_inference,[],[42,67,105,73,56,85,54,81,88,20,107,39,26,40,41,3,13,14,15,32,5])). % 106.04/106.04 cnf(118,plain, % 106.04/106.04 (P2(a1,f6(x1181,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[112,39])). % 106.04/106.04 cnf(122,plain, % 106.04/106.04 (P2(a1,f6(f10(a1),x1221))), % 106.04/106.04 inference(scs_inference,[],[99,112,39,26,40])). % 106.04/106.04 cnf(124,plain, % 106.04/106.04 (~P2(f10(a1),f10(a9))), % 106.04/106.04 inference(scs_inference,[],[115,99,112,39,26,40,38])). % 106.04/106.04 cnf(126,plain, % 106.04/106.04 (~P2(f6(f10(a1),f10(a1)),f6(f10(a1),f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[115,99,112,62,39,26,40,38,41])). % 106.04/106.04 cnf(130,plain, % 106.04/106.04 (~E(f6(a1,a1),f6(f10(a1),f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[48,115,108,99,112,62,18,39,26,40,38,41,13,14])). % 106.04/106.04 cnf(131,plain, % 106.04/106.04 (~E(f6(x1311,f10(a1)),a1)), % 106.04/106.04 inference(scs_inference,[],[48,115,44,108,99,110,112,62,18,39,26,40,38,41,13,14,3])). % 106.04/106.04 cnf(134,plain, % 106.04/106.04 (P2(f5(f10(a1),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[42,48,115,44,108,99,110,112,62,54,18,39,26,40,38,41,13,14,3,15,34])). % 106.04/106.04 cnf(137,plain, % 106.04/106.04 (P2(f6(a1,a1),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[42,48,115,44,108,99,110,112,62,54,18,20,39,26,40,38,41,13,14,3,15,34,32])). % 106.04/106.04 cnf(140,plain, % 106.04/106.04 (~E(f10(a1),f10(a7))), % 106.04/106.04 inference(scs_inference,[],[42,48,115,44,108,99,110,112,62,54,18,20,39,26,40,38,41,13,14,3,15,34,32,4])). % 106.04/106.04 cnf(149,plain, % 106.04/106.04 (P2(f6(a1,a1),f6(x1491,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[137,39])). % 106.04/106.04 cnf(151,plain, % 106.04/106.04 (P2(f6(a1,a1),f6(f10(a1),x1511))), % 106.04/106.04 inference(scs_inference,[],[137,39,40])). % 106.04/106.04 cnf(155,plain, % 106.04/106.04 (~P2(f10(a1),f10(f10(a7)))), % 106.04/106.04 inference(scs_inference,[],[140,137,134,39,40,26,38])). % 106.04/106.04 cnf(157,plain, % 106.04/106.04 (E(f5(f10(a7),a9,f10(a1)),a1)), % 106.04/106.04 inference(scs_inference,[],[140,95,137,134,18,39,40,26,38,25])). % 106.04/106.04 cnf(159,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,f10(a1)),f6(x1591,f10(a1)))), % 106.04/106.04 inference(rename_variables,[],[95])). % 106.04/106.04 cnf(161,plain, % 106.04/106.04 (~P2(f10(a1),f6(f10(a9),f10(a9)))), % 106.04/106.04 inference(scs_inference,[],[140,95,137,134,124,18,39,40,26,38,25,41])). % 106.04/106.04 cnf(165,plain, % 106.04/106.04 (~E(f6(a1,a1),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[67,140,126,130,95,159,137,134,124,18,39,40,26,38,25,41,14,3])). % 106.04/106.04 cnf(167,plain, % 106.04/106.04 (~P2(x1671,f5(f10(a7),a9,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[67,140,126,130,95,159,137,134,124,18,39,40,26,38,25,41,14,3,23])). % 106.04/106.04 cnf(169,plain, % 106.04/106.04 (E(a1,f5(f10(a7),a9,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[67,140,126,130,95,159,137,134,124,18,39,40,26,38,25,41,14,3,23,2])). % 106.04/106.04 cnf(172,plain, % 106.04/106.04 (E(f4(a1,f6(a1,a1)),a1)), % 106.04/106.04 inference(scs_inference,[],[67,140,126,130,95,159,137,134,124,54,18,39,40,26,38,25,41,14,3,23,2,33,29])). % 106.04/106.04 cnf(175,plain, % 106.04/106.04 (P1(f5(f10(a7),a9,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[67,140,126,130,95,159,137,134,124,16,54,18,39,40,26,38,25,41,14,3,23,2,33,29,13])). % 106.04/106.04 cnf(176,plain, % 106.04/106.04 (~P2(x1761,f4(a1,f6(a1,a1)))), % 106.04/106.04 inference(scs_inference,[],[172,23])). % 106.04/106.04 cnf(180,plain, % 106.04/106.04 (~P2(f6(a1,a1),f10(f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[165,134,172,23,39,38])). % 106.04/106.04 cnf(184,plain, % 106.04/106.04 (P2(f5(f10(a1),f10(a1),f6(a1,a1)),f6(f10(a1),x1841))), % 106.04/106.04 inference(scs_inference,[],[165,134,172,23,39,38,26,40])). % 106.04/106.04 cnf(192,plain, % 106.04/106.04 (P1(f4(a1,f6(a1,a1)))), % 106.04/106.04 inference(scs_inference,[],[167,165,118,134,172,126,52,16,23,39,38,26,40,2,41,14,13])). % 106.04/106.04 cnf(193,plain, % 106.04/106.04 (~E(f10(a1),a1)), % 106.04/106.04 inference(scs_inference,[],[167,44,165,86,118,134,172,126,52,16,23,39,38,26,40,2,41,14,13,3])). % 106.04/106.04 cnf(194,plain, % 106.04/106.04 (~E(f6(f10(a1),x1941),f5(f10(a7),a9,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[167,44,165,86,83,118,134,172,126,52,16,23,39,38,26,40,2,41,14,13,3,15])). % 106.04/106.04 cnf(196,plain, % 106.04/106.04 (P2(f5(f10(a1),f10(a1),a1),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[167,37,44,165,86,83,118,134,172,126,52,16,23,39,38,26,40,2,41,14,13,3,15,34])). % 106.04/106.04 cnf(199,plain, % 106.04/106.04 (P2(f3(f10(a1)),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[167,37,44,165,86,83,118,134,172,126,52,16,23,39,38,26,40,2,41,14,13,3,15,34,22])). % 106.04/106.04 cnf(201,plain, % 106.04/106.04 (P2(f3(f10(a1)),f6(x2011,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[199,39])). % 106.04/106.04 cnf(205,plain, % 106.04/106.04 (~P2(f6(x2051,f10(a1)),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[131,184,199,39,26,38])). % 106.04/106.04 cnf(212,plain, % 106.04/106.04 (~E(f5(f10(a1),f10(a1),f6(a1,a1)),f6(f10(a1),f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[176,131,134,184,199,62,52,39,26,38,40,41,14])). % 106.04/106.04 cnf(213,plain, % 106.04/106.04 (~E(f6(f10(a1),x2131),a1)), % 106.04/106.04 inference(scs_inference,[],[176,169,131,134,194,184,199,62,52,39,26,38,40,41,14,3])). % 106.04/106.04 cnf(216,plain, % 106.04/106.04 (P2(f5(f10(a1),f10(a1),a1),f6(x2161,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[196,39])). % 106.04/106.04 cnf(218,plain, % 106.04/106.04 (~P2(f10(a1),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[193,196,39,38])). % 106.04/106.04 cnf(222,plain, % 106.04/106.04 (P2(f5(f10(a1),f10(a1),a1),f6(f10(a1),x2221))), % 106.04/106.04 inference(scs_inference,[],[193,196,39,38,26,40])). % 106.04/106.04 cnf(224,plain, % 106.04/106.04 (~P2(f6(x2241,f10(a1)),f6(f10(a1),f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[193,196,205,39,38,26,40,41])). % 106.04/106.04 cnf(230,plain, % 106.04/106.04 (~E(a9,f10(a1))), % 106.04/106.04 inference(scs_inference,[],[167,193,74,81,157,196,205,39,38,26,40,41,14,3,15,5])). % 106.04/106.04 cnf(231,plain, % 106.04/106.04 (E(f4(a1,a9),a1)), % 106.04/106.04 inference(scs_inference,[],[167,193,74,81,157,196,205,50,39,38,26,40,41,14,3,15,5,29])). % 106.04/106.04 cnf(234,plain, % 106.04/106.04 (~P2(x2341,f4(a1,a9))), % 106.04/106.04 inference(scs_inference,[],[167,193,74,81,157,196,205,50,39,38,26,40,41,14,3,15,5,29,23])). % 106.04/106.04 cnf(236,plain, % 106.04/106.04 (E(a1,f4(a1,a9))), % 106.04/106.04 inference(scs_inference,[],[167,193,74,81,157,196,205,50,39,38,26,40,41,14,3,15,5,29,23,2])). % 106.04/106.04 cnf(237,plain, % 106.04/106.04 (P1(f4(a1,a9))), % 106.04/106.04 inference(scs_inference,[],[167,193,74,81,157,196,205,50,16,39,38,26,40,41,14,3,15,5,29,23,2,13])). % 106.04/106.04 cnf(240,plain, % 106.04/106.04 (~P2(f6(f10(a1),x2401),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[213,216,26,38])). % 106.04/106.04 cnf(242,plain, % 106.04/106.04 (~P2(x2421,f6(f4(a1,a9),f4(a1,a9)))), % 106.04/106.04 inference(scs_inference,[],[234,213,216,26,38,41])). % 106.04/106.04 cnf(244,plain, % 106.04/106.04 (~E(a1,f6(x2441,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[234,213,122,224,216,26,38,41,14])). % 106.04/106.04 cnf(245,plain, % 106.04/106.04 (P2(a1,f6(f10(a1),x2451))), % 106.04/106.04 inference(rename_variables,[],[122])). % 106.04/106.04 cnf(246,plain, % 106.04/106.04 (E(f6(f10(a7),a9),f4(a1,a9))), % 106.04/106.04 inference(scs_inference,[],[19,234,236,213,122,224,216,26,38,41,14,3])). % 106.04/106.04 cnf(247,plain, % 106.04/106.04 (~E(f6(f10(a1),x2471),f4(a1,a9))), % 106.04/106.04 inference(scs_inference,[],[19,234,236,213,122,245,224,216,26,38,41,14,3,15])). % 106.04/106.04 cnf(248,plain, % 106.04/106.04 (~P2(x2481,f4(a1,a9))), % 106.04/106.04 inference(rename_variables,[],[234])). % 106.04/106.04 cnf(249,plain, % 106.04/106.04 (P2(f5(f4(a1,a9),f10(a1),a1),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[19,234,248,37,236,213,122,245,224,216,26,38,41,14,3,15,34])). % 106.04/106.04 cnf(253,plain, % 106.04/106.04 (P2(f5(f4(a1,a9),f10(a1),a1),f6(x2531,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[19,234,248,37,236,213,122,245,224,216,26,38,41,14,3,15,34,39])). % 106.04/106.04 cnf(255,plain, % 106.04/106.04 (P2(f5(f4(a1,a9),f10(a1),a1),f6(f10(a1),x2551))), % 106.04/106.04 inference(scs_inference,[],[19,234,248,37,236,213,122,245,224,216,26,38,41,14,3,15,34,39,40])). % 106.04/106.04 cnf(257,plain, % 106.04/106.04 (E(f4(a1,a9),f6(f10(a7),a9))), % 106.04/106.04 inference(scs_inference,[],[19,234,248,37,236,213,122,245,224,216,26,38,41,14,3,15,34,39,40,2])). % 106.04/106.04 cnf(260,plain, % 106.04/106.04 (~P2(a9,f10(f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[230,222,26,38])). % 106.04/106.04 cnf(268,plain, % 106.04/106.04 (~E(f10(a1),f4(a1,a9))), % 106.04/106.04 inference(scs_inference,[],[176,234,257,230,86,83,88,222,240,26,38,41,14,15,3])). % 106.04/106.04 cnf(276,plain, % 106.04/106.04 (~P2(f10(a1),f10(f4(a1,a9)))), % 106.04/106.04 inference(scs_inference,[],[268,255,26,38])). % 106.04/106.04 cnf(281,plain, % 106.04/106.04 (~E(a1,f10(a1))), % 106.04/106.04 inference(scs_inference,[],[167,234,268,112,255,218,26,38,41,14])). % 106.04/106.04 cnf(282,plain, % 106.04/106.04 (~E(f6(x2821,f10(a1)),f4(a1,a9))), % 106.04/106.04 inference(scs_inference,[],[167,234,268,131,112,231,255,218,26,38,41,14,3])). % 106.04/106.04 cnf(285,plain, % 106.04/106.04 (~P2(x2851,a1)), % 106.04/106.04 inference(rename_variables,[],[37])). % 106.04/106.04 cnf(288,plain, % 106.04/106.04 (E(f4(a1,a1),a1)), % 106.04/106.04 inference(scs_inference,[],[167,234,37,285,268,131,112,231,255,218,244,26,38,41,14,3,34,29])). % 106.04/106.04 cnf(291,plain, % 106.04/106.04 (~P2(x2911,f4(a1,a1))), % 106.04/106.04 inference(scs_inference,[],[167,234,37,285,268,131,112,231,255,218,244,26,38,41,14,3,34,29,23])). % 106.04/106.04 cnf(293,plain, % 106.04/106.04 (E(a1,f4(a1,a1))), % 106.04/106.04 inference(scs_inference,[],[167,234,37,285,268,131,112,231,255,218,244,26,38,41,14,3,34,29,23,2])). % 106.04/106.04 cnf(294,plain, % 106.04/106.04 (P1(f4(a1,a1))), % 106.04/106.04 inference(scs_inference,[],[167,234,37,285,268,131,112,231,255,218,244,16,26,38,41,14,3,34,29,23,2,13])). % 106.04/106.04 cnf(299,plain, % 106.04/106.04 (~P2(x2991,f6(f4(a1,a1),f4(a1,a1)))), % 106.04/106.04 inference(scs_inference,[],[291,282,253,26,38,41])). % 106.04/106.04 cnf(302,plain, % 106.04/106.04 (~E(f6(x3021,f10(a1)),f4(a1,a1))), % 106.04/106.04 inference(scs_inference,[],[291,282,118,74,253,240,26,38,41,14,15])). % 106.04/106.04 cnf(303,plain, % 106.04/106.04 (~P2(x3031,f4(a1,a1))), % 106.04/106.04 inference(rename_variables,[],[291])). % 106.04/106.04 cnf(304,plain, % 106.04/106.04 (~E(f6(f10(a1),x3041),f4(a1,a1))), % 106.04/106.04 inference(scs_inference,[],[291,282,213,118,74,253,288,240,26,38,41,14,15,3])). % 106.04/106.04 cnf(305,plain, % 106.04/106.04 (P2(f5(f4(a1,a1),f10(a1),a1),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,26,38,41,14,15,3,34])). % 106.04/106.04 cnf(310,plain, % 106.04/106.04 (~E(f10(a7),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,26,38,41,14,15,3,34,4])). % 106.04/106.04 cnf(311,plain, % 106.04/106.04 (~E(a7,a1)), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,26,38,41,14,15,3,34,4,6])). % 106.04/106.04 cnf(312,plain, % 106.04/106.04 (P2(f5(f4(a1,a1),f10(a1),a1),f6(x3121,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,26,38,41,14,15,3,34,4,6,39])). % 106.04/106.04 cnf(314,plain, % 106.04/106.04 (P2(f5(f4(a1,a1),f10(a1),a1),f6(f10(a1),x3141))), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,26,38,41,14,15,3,34,4,6,39,40])). % 106.04/106.04 cnf(316,plain, % 106.04/106.04 (E(f4(a1,f10(a7)),a1)), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,52,26,38,41,14,15,3,34,4,6,39,40,29])). % 106.04/106.04 cnf(319,plain, % 106.04/106.04 (P2(f3(a7),a7)), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,52,26,38,41,14,15,3,34,4,6,39,40,29,22])). % 106.04/106.04 cnf(321,plain, % 106.04/106.04 (~P2(x3211,f4(a1,f10(a7)))), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,52,26,38,41,14,15,3,34,4,6,39,40,29,22,23])). % 106.04/106.04 cnf(324,plain, % 106.04/106.04 (P1(f4(a1,f10(a7)))), % 106.04/106.04 inference(scs_inference,[],[291,303,37,282,213,118,74,253,288,240,244,52,16,26,38,41,14,15,3,34,4,6,39,40,29,22,23,2,13])). % 106.04/106.04 cnf(325,plain, % 106.04/106.04 (P2(f3(a7),f6(x3251,a7))), % 106.04/106.04 inference(scs_inference,[],[319,39])). % 106.04/106.04 cnf(329,plain, % 106.04/106.04 (P2(f3(a7),f6(a7,x3291))), % 106.04/106.04 inference(scs_inference,[],[314,319,39,26,40])). % 106.04/106.04 cnf(339,plain, % 106.04/106.04 (~P2(x3391,f4(a1,f10(a7)))), % 106.04/106.04 inference(rename_variables,[],[321])). % 106.04/106.04 cnf(340,plain, % 106.04/106.04 (~E(a7,f6(f10(a7),a9))), % 106.04/106.04 inference(scs_inference,[],[19,321,291,304,311,122,99,314,319,224,39,26,40,38,41,14,15,3])). % 106.04/106.04 cnf(341,plain, % 106.04/106.04 (P2(f5(f4(a1,f10(a7)),f10(a1),a1),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[19,321,339,291,37,304,311,122,99,314,319,224,244,39,26,40,38,41,14,15,3,34])). % 106.04/106.04 cnf(357,plain, % 106.04/106.04 (~E(f5(f10(a7),a9,f10(a1)),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[321,234,310,88,312,325,218,39,40,26,38,41,14])). % 106.04/106.04 cnf(360,plain, % 106.04/106.04 (~E(a7,f4(a1,a9))), % 106.04/106.04 inference(scs_inference,[],[321,234,310,340,257,81,88,312,325,218,39,40,26,38,41,14,15,3])). % 106.04/106.04 cnf(361,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,a7),a7)), % 106.04/106.04 inference(scs_inference,[],[321,234,310,340,257,81,88,312,325,218,50,52,39,40,26,38,41,14,15,3,34])). % 106.04/106.04 cnf(365,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,a7),f6(x3651,a7))), % 106.04/106.04 inference(scs_inference,[],[361,39])). % 106.04/106.04 cnf(369,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,a7),f6(a7,x3691))), % 106.04/106.04 inference(scs_inference,[],[201,361,39,26,40])). % 106.04/106.04 cnf(373,plain, % 106.04/106.04 (~P2(f6(f10(a1),x3731),f6(f10(a1),f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[360,201,361,240,39,26,40,38,41])). % 106.04/106.04 cnf(375,plain, % 106.04/106.04 (~E(f6(a1,a1),f6(x3751,f10(a1)))), % 106.04/106.04 inference(scs_inference,[],[360,137,201,361,205,240,39,26,40,38,41,14])). % 106.04/106.04 cnf(377,plain, % 106.04/106.04 (~P2(x3771,f4(a1,f10(a7)))), % 106.04/106.04 inference(rename_variables,[],[321])). % 106.04/106.04 cnf(379,plain, % 106.04/106.04 (P2(f5(f4(a1,f10(a7)),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.04 inference(scs_inference,[],[321,377,360,311,137,316,201,361,205,240,54,39,26,40,38,41,14,15,3,34])). % 106.04/106.04 cnf(384,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,a7),f6(x3841,f6(x3842,a7)))), % 106.04/106.04 inference(scs_inference,[],[365,39])). % 106.04/106.04 cnf(386,plain, % 106.04/106.04 (P2(f5(f10(a7),a9,a7),f6(f6(x3861,a7),x3862))), % 106.04/106.04 inference(scs_inference,[],[365,39,40])). % 106.04/106.04 cnf(390,plain, % 106.04/106.04 (~P2(a7,f10(a1))), % 106.04/106.04 inference(scs_inference,[],[311,341,365,39,40,26,38])). % 106.04/106.04 cnf(392,plain, % 106.04/106.04 (~P2(x3921,f6(f4(a1,a1),f4(a1,a9)))), % 106.04/106.04 inference(scs_inference,[],[291,234,311,341,365,39,40,26,38,41])). % 106.04/106.04 cnf(395,plain, % 106.04/106.04 (~E(a1,f6(f10(a1),x3951))), % 106.04/106.04 inference(scs_inference,[],[291,234,311,118,373,341,365,39,40,26,38,41,14])). % 106.04/106.04 cnf(397,plain, % 106.04/106.04 (~E(f10(a1),f4(a1,a1))), % 106.04/106.04 inference(scs_inference,[],[291,234,311,118,74,373,341,365,39,40,26,38,41,14,15])). % 106.04/106.04 cnf(398,plain, % 106.04/106.04 (~P2(x3981,f4(a1,a1))), % 106.04/106.04 inference(rename_variables,[],[291])). % 106.04/106.04 cnf(399,plain, % 106.04/106.04 (~E(f5(f10(a1),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[291,234,67,311,118,74,212,373,341,365,39,40,26,38,41,14,15,3])). % 106.04/106.05 cnf(401,plain, % 106.04/106.05 (P2(f5(f4(a1,a1),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[291,398,234,67,311,118,74,212,373,375,341,365,54,39,40,26,38,41,14,15,3,34])). % 106.04/106.05 cnf(410,plain, % 106.04/106.05 (P2(f5(f4(a1,a1),f10(a1),f6(a1,a1)),f6(f10(a1),x4101))), % 106.04/106.05 inference(scs_inference,[],[384,401,39,26,40])). % 106.04/106.05 cnf(418,plain, % 106.04/106.05 (~P2(x4181,f4(a1,f6(a1,a1)))), % 106.04/106.05 inference(rename_variables,[],[176])). % 106.04/106.05 cnf(420,plain, % 106.04/106.05 (~E(f10(a1),f6(f10(a7),f10(a7)))), % 106.04/106.05 inference(scs_inference,[],[176,291,140,399,81,88,384,401,390,18,39,26,40,38,41,15,14,3])). % 106.04/106.05 cnf(422,plain, % 106.04/106.05 (P2(f5(f4(a1,f6(a1,a1)),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[176,418,291,140,399,81,88,384,401,390,375,18,54,39,26,40,38,41,15,14,3,34])). % 106.04/106.05 cnf(427,plain, % 106.04/106.05 (P2(f5(f10(a7),a9,a7),f6(x4271,f6(a7,x4272)))), % 106.04/106.05 inference(scs_inference,[],[369,39])). % 106.04/106.05 cnf(429,plain, % 106.04/106.05 (P2(f5(f10(a7),a9,a7),f6(f6(a7,x4291),x4292))), % 106.04/106.05 inference(scs_inference,[],[369,39,40])). % 106.04/106.05 cnf(438,plain, % 106.04/106.05 (~E(f6(f10(a7),a9),a7)), % 106.04/106.05 inference(scs_inference,[],[167,291,74,281,386,369,390,39,40,26,38,41,14])). % 106.04/106.05 cnf(441,plain, % 106.04/106.05 (P2(f5(f10(a7),f10(a7),f10(a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[167,291,420,74,281,386,369,390,52,39,40,26,38,41,14,15,34])). % 106.04/106.05 cnf(446,plain, % 106.04/106.05 (~P2(f10(a1),f10(f4(a1,a1)))), % 106.04/106.05 inference(scs_inference,[],[397,441,39,38])). % 106.04/106.05 cnf(452,plain, % 106.04/106.05 (~P2(f10(a1),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[397,427,441,218,39,38,26,40,41])). % 106.04/106.05 cnf(455,plain, % 106.04/106.05 (~P2(x4551,f4(a1,f10(a7)))), % 106.04/106.05 inference(rename_variables,[],[321])). % 106.04/106.05 cnf(456,plain, % 106.04/106.05 (~E(f6(a1,a1),f6(f10(a1),x4561))), % 106.04/106.05 inference(scs_inference,[],[321,397,427,149,441,373,218,39,38,26,40,41,15,14])). % 106.04/106.05 cnf(458,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,f10(a7)),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[321,455,397,427,149,441,373,218,54,39,38,26,40,41,15,14,34])). % 106.04/106.05 cnf(462,plain, % 106.04/106.05 (P2(f3(a7),f6(x4621,f6(a7,x4622)))), % 106.04/106.05 inference(scs_inference,[],[329,39])). % 106.04/106.05 cnf(464,plain, % 106.04/106.05 (P2(f3(a7),f6(f6(a7,x4641),x4642))), % 106.04/106.05 inference(scs_inference,[],[329,39,40])). % 106.04/106.05 cnf(475,plain, % 106.04/106.05 (~P2(x4751,f6(f10(a7),a9))), % 106.04/106.05 inference(rename_variables,[],[42])). % 106.04/106.05 cnf(481,plain, % 106.04/106.05 (~E(f6(a7,x4811),f10(a7))), % 106.04/106.05 inference(scs_inference,[],[42,475,234,134,429,357,456,329,390,54,39,40,26,38,41,14,15,34,4])). % 106.04/106.05 cnf(491,plain, % 106.04/106.05 (~P2(a7,f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[481,379,390,38,26,41])). % 106.04/106.05 cnf(506,plain, % 106.04/106.05 (~P2(f10(a1),f5(f4(a1,a9),f10(a1),a1))), % 106.04/106.05 inference(scs_inference,[],[249,247,38,26])). % 106.04/106.05 cnf(521,plain, % 106.04/106.05 (~P2(f10(a1),f5(f4(a1,a1),f10(a1),a1))), % 106.04/106.05 inference(scs_inference,[],[305,302,38,26])). % 106.04/106.05 cnf(524,plain, % 106.04/106.05 (~P2(x5241,f6(a1,a1))), % 106.04/106.05 inference(rename_variables,[],[54])). % 106.04/106.05 cnf(527,plain, % 106.04/106.05 (~P2(x5271,f5(f10(a7),a9,f10(a1)))), % 106.04/106.05 inference(rename_variables,[],[167])). % 106.04/106.05 cnf(529,plain, % 106.04/106.05 (P2(f5(f5(f10(a7),a9,f10(a1)),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[167,527,134,375,305,361,302,240,54,524,38,26,41,15,14,34])). % 106.04/106.05 cnf(541,plain, % 106.04/106.05 (~E(f5(f4(a1,a9),f10(a1),a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[321,249,199,365,218,52,26,41,15,14])). % 106.04/106.05 cnf(549,plain, % 106.04/106.05 (~E(f6(a7,x5491),f6(f10(a7),a9))), % 106.04/106.05 inference(scs_inference,[],[42,291,441,369,26,41,15])). % 106.04/106.05 cnf(551,plain, % 106.04/106.05 (~E(f6(a1,a1),a7)), % 106.04/106.05 inference(scs_inference,[],[42,291,137,441,369,390,26,41,15,14])). % 106.04/106.05 cnf(567,plain, % 106.04/106.05 (~P2(x5671,f6(f4(a1,a9),f4(a1,a1)))), % 106.04/106.05 inference(scs_inference,[],[234,291,401,26,41])). % 106.04/106.05 cnf(570,plain, % 106.04/106.05 (~E(f6(x5701,a7),f4(a1,a9))), % 106.04/106.05 inference(scs_inference,[],[234,291,401,325,26,41,15])). % 106.04/106.05 cnf(571,plain, % 106.04/106.05 (~P2(x5711,f4(a1,a9))), % 106.04/106.05 inference(rename_variables,[],[234])). % 106.04/106.05 cnf(573,plain, % 106.04/106.05 (P2(f5(f4(a1,a9),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[234,571,291,305,401,325,375,205,54,26,41,15,14,34])). % 106.04/106.05 cnf(596,plain, % 106.04/106.05 (P2(f6(f3(a7),f3(a7)),f6(a7,x5961))), % 106.04/106.05 inference(scs_inference,[],[176,67,329,26,41,15,14])). % 106.04/106.05 cnf(598,plain, % 106.04/106.05 (P2(f5(f10(a7),a9,f6(a7,x5981)),f6(a7,x5981))), % 106.04/106.05 inference(scs_inference,[],[176,67,329,549,50,52,26,41,15,14,34])). % 106.04/106.05 cnf(602,plain, % 106.04/106.05 (P2(f6(f3(a7),f3(a7)),f6(x6021,f6(a7,x6022)))), % 106.04/106.05 inference(scs_inference,[],[176,67,329,549,50,52,26,41,15,14,34,39])). % 106.04/106.05 cnf(604,plain, % 106.04/106.05 (P2(f6(f3(a7),f3(a7)),f6(f6(a7,x6041),x6042))), % 106.04/106.05 inference(scs_inference,[],[176,67,329,549,50,52,26,41,15,14,34,39,40])). % 106.04/106.05 cnf(606,plain, % 106.04/106.05 (P2(f5(f10(a7),a9,f6(a7,x6061)),f6(x6062,f6(a7,x6061)))), % 106.04/106.05 inference(scs_inference,[],[598,39])). % 106.04/106.05 cnf(608,plain, % 106.04/106.05 (P2(f5(f10(a7),a9,f6(a7,x6081)),f6(f6(a7,x6081),x6082))), % 106.04/106.05 inference(scs_inference,[],[598,39,40])). % 106.04/106.05 cnf(610,plain, % 106.04/106.05 (~P2(a7,f3(a7))), % 106.04/106.05 inference(scs_inference,[],[319,598,39,40,26])). % 106.04/106.05 cnf(615,plain, % 106.04/106.05 (~P2(x6151,f5(f10(a7),a9,f10(a1)))), % 106.04/106.05 inference(rename_variables,[],[167])). % 106.04/106.05 cnf(617,plain, % 106.04/106.05 (P2(f6(f3(a7),f3(a7)),a7)), % 106.04/106.05 inference(scs_inference,[],[167,615,18,249,319,365,604,598,240,39,40,26,41,15,14,32])). % 106.04/106.05 cnf(620,plain, % 106.04/106.05 (~P2(x6201,f5(f10(a7),a9,f10(a1)))), % 106.04/106.05 inference(rename_variables,[],[167])). % 106.04/106.05 cnf(622,plain, % 106.04/106.05 (P2(f5(f10(a1),f5(f10(a7),a9,f10(a1)),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[167,615,620,18,249,319,365,456,604,598,240,54,39,40,26,41,15,14,32,34])). % 106.04/106.05 cnf(627,plain, % 106.04/106.05 (P2(f6(f3(a7),f3(a7)),f6(x6271,a7))), % 106.04/106.05 inference(scs_inference,[],[617,39])). % 106.04/106.05 cnf(638,plain, % 106.04/106.05 (~E(f5(f4(a1,a1),f10(a1),a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[321,305,361,369,617,218,54,39,40,26,41,15,14])). % 106.04/106.05 cnf(654,plain, % 106.04/106.05 (~E(f6(x6541,a7),f6(f10(a7),a9))), % 106.04/106.05 inference(scs_inference,[],[42,441,365,205,26,14,15])). % 106.04/106.05 cnf(671,plain, % 106.04/106.05 (P2(f5(f10(a7),a9,f6(x6711,a7)),f6(x6711,a7))), % 106.04/106.05 inference(scs_inference,[],[167,196,369,654,240,50,52,26,14,15,34])). % 106.04/106.05 cnf(675,plain, % 106.04/106.05 (P2(f5(f10(a7),a9,f6(x6751,a7)),f6(x6752,f6(x6751,a7)))), % 106.04/106.05 inference(scs_inference,[],[167,196,369,654,240,50,52,26,14,15,34,39])). % 106.04/106.05 cnf(681,plain, % 106.04/106.05 (~P2(x6811,f6(f4(a1,a9),a1))), % 106.04/106.05 inference(scs_inference,[],[234,37,458,26,41])). % 106.04/106.05 cnf(684,plain, % 106.04/106.05 (~E(f6(a7,x6841),f4(a1,a9))), % 106.04/106.05 inference(scs_inference,[],[234,37,329,458,26,41,15])). % 106.04/106.05 cnf(685,plain, % 106.04/106.05 (~P2(x6851,f4(a1,a9))), % 106.04/106.05 inference(rename_variables,[],[234])). % 106.04/106.05 cnf(686,plain, % 106.04/106.05 (~E(f5(f4(a1,a1),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[234,37,401,329,458,218,26,41,15,14])). % 106.04/106.05 cnf(687,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,a9),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[234,685,37,401,329,456,458,218,54,26,41,15,14,34])). % 106.04/106.05 cnf(702,plain, % 106.04/106.05 (~P2(x7021,f6(f4(a1,a1),a1))), % 106.04/106.05 inference(scs_inference,[],[291,37,422,686,38,26,41])). % 106.04/106.05 cnf(707,plain, % 106.04/106.05 (~P2(x7071,f4(a1,a1))), % 106.04/106.05 inference(rename_variables,[],[291])). % 106.04/106.05 cnf(708,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[291,707,37,249,319,456,422,686,390,54,38,26,41,14,15,34])). % 106.04/106.05 cnf(713,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,a1),f6(a1,a1)),f6(x7131,f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[291,707,37,249,319,456,422,686,390,54,38,26,41,14,15,34,39])). % 106.04/106.05 cnf(715,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,a1),f6(a1,a1)),f6(f10(a1),x7151))), % 106.04/106.05 inference(scs_inference,[],[291,707,37,249,319,456,422,686,390,54,38,26,41,14,15,34,39,40])). % 106.04/106.05 cnf(741,plain, % 106.04/106.05 (~P2(x7411,f6(f4(a1,a9),f10(a7)))), % 106.04/106.05 inference(scs_inference,[],[234,671,52,26,41])). % 106.04/106.05 cnf(745,plain, % 106.04/106.05 (~P2(x7451,f4(a1,a9))), % 106.04/106.05 inference(rename_variables,[],[234])). % 106.04/106.05 cnf(746,plain, % 106.04/106.05 (~E(f5(f10(a7),f10(a7),f10(a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[234,441,671,218,52,602,26,41,15,14])). % 106.04/106.05 cnf(747,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,a9),a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[234,745,37,441,671,218,52,602,395,26,41,15,14,34])). % 106.04/106.05 cnf(752,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,a9),a1),f6(x7521,f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[234,745,37,441,671,218,52,602,395,26,41,15,14,34,39])). % 106.04/106.05 cnf(768,plain, % 106.04/106.05 (~P2(x7681,f6(f4(a1,a1),f10(a7)))), % 106.04/106.05 inference(scs_inference,[],[291,573,52,746,38,26,41])). % 106.04/106.05 cnf(771,plain, % 106.04/106.05 (~E(f6(x7711,a7),f4(a1,a1))), % 106.04/106.05 inference(scs_inference,[],[291,325,573,52,746,38,26,41,15])). % 106.04/106.05 cnf(772,plain, % 106.04/106.05 (~P2(x7721,f4(a1,a1))), % 106.04/106.05 inference(rename_variables,[],[291])). % 106.04/106.05 cnf(774,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,a1),a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[291,772,37,196,325,573,390,52,746,395,38,26,41,15,14,34])). % 106.04/106.05 cnf(781,plain, % 106.04/106.05 (P2(f5(f10(a1),f4(a1,a1),a1),f6(f10(a1),x7811))), % 106.04/106.05 inference(scs_inference,[],[291,772,37,196,325,573,390,52,746,395,38,26,41,15,14,34,39,40])). % 106.04/106.05 cnf(787,plain, % 106.04/106.05 (~P2(x7871,f6(f4(a1,a9),f6(a1,a1)))), % 106.04/106.05 inference(scs_inference,[],[234,687,54,771,38,26,41])). % 106.04/106.05 cnf(790,plain, % 106.04/106.05 (~E(f6(f6(a7,x7901),x7902),f4(a1,a9))), % 106.04/106.05 inference(scs_inference,[],[234,687,54,771,608,38,26,41,15])). % 106.04/106.05 cnf(797,plain, % 106.04/106.05 (~P2(x7971,f6(f4(a1,a1),f6(a1,a1)))), % 106.04/106.05 inference(scs_inference,[],[291,708,54,790,38,26,41])). % 106.04/106.05 cnf(800,plain, % 106.04/106.05 (~E(f6(a7,x8001),f4(a1,a1))), % 106.04/106.05 inference(scs_inference,[],[291,369,708,54,790,38,26,41,15])). % 106.04/106.05 cnf(807,plain, % 106.04/106.05 (~P2(x8071,f6(f4(a1,a9),a9))), % 106.04/106.05 inference(scs_inference,[],[234,598,800,50,38,26,41])). % 106.04/106.05 cnf(810,plain, % 106.04/106.05 (~E(f6(x8101,f6(x8102,a7)),f4(a1,a9))), % 106.04/106.05 inference(scs_inference,[],[234,598,800,675,50,38,26,41,15])). % 106.04/106.05 cnf(817,plain, % 106.04/106.05 (~P2(x8171,f6(f4(a1,a1),a9))), % 106.04/106.05 inference(scs_inference,[],[291,747,810,50,38,26,41])). % 106.04/106.05 cnf(820,plain, % 106.04/106.05 (~E(f6(x8201,f6(a7,x8202)),f4(a1,a1))), % 106.04/106.05 inference(scs_inference,[],[291,747,810,606,50,38,26,41,15])). % 106.04/106.05 cnf(825,plain, % 106.04/106.05 (~P2(f10(a1),f5(f10(a1),f4(a1,a1),a1))), % 106.04/106.05 inference(scs_inference,[],[774,820,38,26])). % 106.04/106.05 cnf(858,plain, % 106.04/106.05 (~E(f5(f4(a1,a9),f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[573,218,529,26,14])). % 106.04/106.05 cnf(863,plain, % 106.04/106.05 (~E(f5(f10(a7),f10(a7),f10(a1)),a7)), % 106.04/106.05 inference(scs_inference,[],[441,390,622,26,14])). % 106.04/106.05 cnf(872,plain, % 106.04/106.05 (~E(f5(f10(a1),f4(a1,a9),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[687,218,713,26,14])). % 106.04/106.05 cnf(886,plain, % 106.04/106.05 (~E(f5(f10(a1),f4(a1,a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[708,218,410,26,14])). % 106.04/106.05 cnf(901,plain, % 106.04/106.05 (~E(f5(f10(a1),f4(a1,a9),a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[452,752,26,14])). % 106.04/106.05 cnf(933,plain, % 106.04/106.05 (~E(f5(f10(a1),f4(a1,a1),a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[452,781,606,26,14])). % 106.04/106.05 cnf(953,plain, % 106.04/106.05 (P1(f6(a1,a1))), % 106.04/106.05 inference(scs_inference,[],[16,67,13])). % 106.04/106.05 cnf(957,plain, % 106.04/106.05 (P1(f6(a2,a2))), % 106.04/106.05 inference(scs_inference,[],[17,67,13])). % 106.04/106.05 cnf(963,plain, % 106.04/106.05 (~P2(x9631,f6(a1,f4(a1,a9)))), % 106.04/106.05 inference(scs_inference,[],[37,234,41])). % 106.04/106.05 cnf(967,plain, % 106.04/106.05 (~P2(x9671,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(968,plain, % 106.04/106.05 (P2(f5(a1,f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[37,967,234,375,365,54,41,15,34])). % 106.04/106.05 cnf(973,plain, % 106.04/106.05 (P2(f3(f6(x9731,a7)),f6(x9731,a7))), % 106.04/106.05 inference(scs_inference,[],[37,967,234,375,365,54,41,15,34,22])). % 106.04/106.05 cnf(975,plain, % 106.04/106.05 (P2(f5(a1,f10(a1),f6(a1,a1)),f6(x9751,f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[37,967,234,375,365,54,41,15,34,22,39])). % 106.04/106.05 cnf(977,plain, % 106.04/106.05 (P2(f5(a1,f10(a1),f6(a1,a1)),f6(f10(a1),x9771))), % 106.04/106.05 inference(scs_inference,[],[37,967,234,375,365,54,41,15,34,22,39,40])). % 106.04/106.05 cnf(979,plain, % 106.04/106.05 (~P2(f6(x9791,a7),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[37,967,234,375,365,54,41,15,34,22,39,40,38])). % 106.04/106.05 cnf(985,plain, % 106.04/106.05 (P2(f3(f6(x9851,a7)),f6(x9852,f6(x9851,a7)))), % 106.04/106.05 inference(scs_inference,[],[973,39])). % 106.04/106.05 cnf(987,plain, % 106.04/106.05 (P2(f3(f6(x9871,a7)),f6(f6(x9871,a7),x9872))), % 106.04/106.05 inference(scs_inference,[],[973,39,40])). % 106.04/106.05 cnf(991,plain, % 106.04/106.05 (~P2(x9911,f6(a1,f4(a1,a1)))), % 106.04/106.05 inference(scs_inference,[],[37,291,977,973,39,40,26,41])). % 106.04/106.05 cnf(995,plain, % 106.04/106.05 (~P2(x9951,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(996,plain, % 106.04/106.05 (~E(f5(a1,f10(a1),f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[37,291,329,977,973,452,39,40,26,41,15,14])). % 106.04/106.05 cnf(998,plain, % 106.04/106.05 (P2(f5(f10(a1),a1,f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[37,995,291,329,456,54,977,973,452,39,40,26,41,15,14,34])). % 106.04/106.05 cnf(1003,plain, % 106.04/106.05 (P2(f3(f6(a7,x10031)),f6(a7,x10031))), % 106.04/106.05 inference(scs_inference,[],[37,995,291,329,456,54,977,973,452,39,40,26,41,15,14,34,22])). % 106.04/106.05 cnf(1005,plain, % 106.04/106.05 (~P2(f6(a7,x10051),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[37,995,291,329,456,54,977,973,452,39,40,26,41,15,14,34,22,38])). % 106.04/106.05 cnf(1008,plain, % 106.04/106.05 (P2(f3(f6(a7,x10081)),f6(x10082,f6(a7,x10081)))), % 106.04/106.05 inference(scs_inference,[],[1003,39])). % 106.04/106.05 cnf(1010,plain, % 106.04/106.05 (P2(f3(f6(a7,x10101)),f6(f6(a7,x10101),x10102))), % 106.04/106.05 inference(scs_inference,[],[1003,39,40])). % 106.04/106.05 cnf(1016,plain, % 106.04/106.05 (~P2(x10161,f6(a1,f10(a7)))), % 106.04/106.05 inference(scs_inference,[],[37,52,985,1003,996,39,40,38,26,41])). % 106.04/106.05 cnf(1019,plain, % 106.04/106.05 (~E(f6(x10191,f6(x10192,a7)),a1)), % 106.04/106.05 inference(scs_inference,[],[37,52,985,1003,996,39,40,38,26,41,15])). % 106.04/106.05 cnf(1020,plain, % 106.04/106.05 (~P2(x10201,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(1023,plain, % 106.04/106.05 (P2(f3(f6(a1,a7)),a7)), % 106.04/106.05 inference(scs_inference,[],[37,1020,18,52,985,975,1003,996,491,39,40,38,26,41,15,14,32])). % 106.04/106.05 cnf(1026,plain, % 106.04/106.05 (~P2(x10261,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(1028,plain, % 106.04/106.05 (P2(f5(a1,f10(a1),a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[37,1020,1026,18,244,52,985,975,1003,996,491,39,40,38,26,41,15,14,32,34])). % 106.04/106.05 cnf(1034,plain, % 106.04/106.05 (P2(f5(f10(a1),a1,f6(a1,a1)),f6(x10341,f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[998,39])). % 106.04/106.05 cnf(1036,plain, % 106.04/106.05 (P2(f5(f10(a1),a1,f6(a1,a1)),f6(f10(a1),x10361))), % 106.04/106.05 inference(scs_inference,[],[998,39,40])). % 106.04/106.05 cnf(1038,plain, % 106.04/106.05 (~P2(f6(x10381,f6(x10382,a7)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[998,1019,39,40,38])). % 106.04/106.05 cnf(1042,plain, % 106.04/106.05 (~P2(x10421,f6(a1,f6(a1,a1)))), % 106.04/106.05 inference(scs_inference,[],[37,54,987,998,1019,39,40,38,26,41])). % 106.04/106.05 cnf(1045,plain, % 106.04/106.05 (~E(f6(f6(x10451,a7),x10452),a1)), % 106.04/106.05 inference(scs_inference,[],[37,54,987,998,1019,39,40,38,26,41,15])). % 106.04/106.05 cnf(1046,plain, % 106.04/106.05 (~P2(x10461,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(1048,plain, % 106.04/106.05 (P2(f5(f10(a1),a1,a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[37,1046,240,54,987,968,998,1019,395,39,40,38,26,41,15,14,34])). % 106.04/106.05 cnf(1054,plain, % 106.04/106.05 (P2(f3(f6(a1,a7)),f6(x10541,a7))), % 106.04/106.05 inference(scs_inference,[],[1023,39])). % 106.04/106.05 cnf(1056,plain, % 106.04/106.05 (P2(f3(f6(a1,a7)),f6(a7,x10561))), % 106.04/106.05 inference(scs_inference,[],[1023,39,40])). % 106.04/106.05 cnf(1058,plain, % 106.04/106.05 (~P2(f6(f6(x10581,a7),x10582),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[1023,1045,39,40,38])). % 106.04/106.05 cnf(1062,plain, % 106.04/106.05 (~P2(f6(x10621,f6(x10622,a7)),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1008,1023,1038,1045,39,40,38,26,41])). % 106.04/106.05 cnf(1064,plain, % 106.04/106.05 (~E(f6(x10641,f6(a7,x10642)),a1)), % 106.04/106.05 inference(scs_inference,[],[37,1008,1023,1038,1045,39,40,38,26,41,15])). % 106.04/106.05 cnf(1065,plain, % 106.04/106.05 (~P2(x10651,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(1068,plain, % 106.04/106.05 (P2(f3(f6(a7,a1)),a7)), % 106.04/106.05 inference(scs_inference,[],[37,1065,18,1008,1023,1034,1038,1045,224,39,40,38,26,41,15,14,32])). % 106.04/106.05 cnf(1074,plain, % 106.04/106.05 (P2(f5(a1,f10(a1),a1),f6(x10741,f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1028,39])). % 106.04/106.05 cnf(1076,plain, % 106.04/106.05 (P2(f5(a1,f10(a1),a1),f6(f10(a1),x10761))), % 106.04/106.05 inference(scs_inference,[],[1028,39,40])). % 106.04/106.05 cnf(1078,plain, % 106.04/106.05 (~P2(f6(x10781,f6(a7,x10782)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[1028,1064,39,40,38])). % 106.04/106.05 cnf(1080,plain, % 106.04/106.05 (~P2(f10(a1),f5(a1,f10(a1),a1))), % 106.04/106.05 inference(scs_inference,[],[1028,1064,39,40,38,26])). % 106.04/106.05 cnf(1082,plain, % 106.04/106.05 (~P2(f6(f6(x10821,a7),x10822),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1028,1058,1064,39,40,38,26,41])). % 106.04/106.05 cnf(1084,plain, % 106.04/106.05 (~E(f6(f6(a7,x10841),x10842),a1)), % 106.04/106.05 inference(scs_inference,[],[37,1028,1010,1058,1064,39,40,38,26,41,15])). % 106.04/106.05 cnf(1085,plain, % 106.04/106.05 (~P2(x10851,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(1088,plain, % 106.04/106.05 (~E(a9,f6(x10881,a7))), % 106.04/106.05 inference(scs_inference,[],[37,83,1028,1062,1010,1058,1064,39,40,38,26,41,15,14,5])). % 106.04/106.05 cnf(1089,plain, % 106.04/106.05 (P2(f5(a1,a7,a9),a7)), % 106.04/106.05 inference(scs_inference,[],[37,1085,83,1028,1062,1010,1058,1064,50,39,40,38,26,41,15,14,5,34])). % 106.04/106.05 cnf(1094,plain, % 106.04/106.05 (P2(f5(f10(a1),a1,a1),f6(x10941,f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1048,39])). % 106.04/106.05 cnf(1096,plain, % 106.04/106.05 (P2(f5(f10(a1),a1,a1),f6(f10(a1),x10961))), % 106.04/106.05 inference(scs_inference,[],[1048,39,40])). % 106.04/106.05 cnf(1098,plain, % 106.04/106.05 (~P2(a9,f10(f6(x10981,a7)))), % 106.04/106.05 inference(scs_inference,[],[1088,1048,39,40,38])). % 106.04/106.05 cnf(1102,plain, % 106.04/106.05 (~P2(f6(x11021,f6(a7,x11022)),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1088,1048,1078,39,40,38,26,41])). % 106.04/106.05 cnf(1106,plain, % 106.04/106.05 (P2(f5(f6(x11061,a7),a1,a1),f6(x11061,a7))), % 106.04/106.05 inference(scs_inference,[],[37,1088,122,1048,1082,1078,39,40,38,26,41,14,34])). % 106.04/106.05 cnf(1115,plain, % 106.04/106.05 (~P2(f6(f6(a7,x11151),x11152),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[1068,1084,39,40,38])). % 106.04/106.05 cnf(1119,plain, % 106.04/106.05 (~P2(f6(x11191,a7),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1068,979,1084,39,40,38,26,41])). % 106.04/106.05 cnf(1124,plain, % 106.04/106.05 (P2(f5(a1,a7,a9),f6(x11241,a7))), % 106.04/106.05 inference(scs_inference,[],[1089,39])). % 106.04/106.05 cnf(1126,plain, % 106.04/106.05 (P2(f5(a1,a7,a9),f6(a7,x11261))), % 106.04/106.05 inference(scs_inference,[],[1089,39,40])). % 106.04/106.05 cnf(1128,plain, % 106.04/106.05 (~P2(a7,f5(a1,a7,a9))), % 106.04/106.05 inference(scs_inference,[],[1089,39,40,26])). % 106.04/106.05 cnf(1130,plain, % 106.04/106.05 (~E(a9,a7)), % 106.04/106.05 inference(scs_inference,[],[67,1088,1089,39,40,26,3])). % 106.04/106.05 cnf(1133,plain, % 106.04/106.05 (~P2(f6(f6(a7,x11331),x11332),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[67,1088,1089,1115,39,40,26,3,41])). % 106.04/106.05 cnf(1135,plain, % 106.04/106.05 (~E(f6(f10(a7),a9),f6(x11351,a7))), % 106.04/106.05 inference(scs_inference,[],[67,1088,83,1089,1119,1115,39,40,26,3,41,14])). % 106.04/106.05 cnf(1140,plain, % 106.04/106.05 (P2(f5(a1,a7,a9),f6(x11401,f6(x11402,a7)))), % 106.04/106.05 inference(scs_inference,[],[1124,39])). % 106.04/106.05 cnf(1142,plain, % 106.04/106.05 (P2(f5(a1,a7,a9),f6(f6(x11421,a7),x11422))), % 106.04/106.05 inference(scs_inference,[],[1124,39,40])). % 106.04/106.05 cnf(1146,plain, % 106.04/106.05 (~E(a9,f6(a7,x11461))), % 106.04/106.05 inference(scs_inference,[],[1088,20,1094,1124,39,40,26,3])). % 106.04/106.05 cnf(1148,plain, % 106.04/106.05 (~P2(f6(a7,x11481),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1088,20,1094,1124,1005,39,40,26,3,41])). % 106.04/106.05 cnf(1150,plain, % 106.04/106.05 (~E(a1,f6(f6(a7,x11501),x11502))), % 106.04/106.05 inference(scs_inference,[],[1088,20,118,1133,1094,1124,1005,39,40,26,3,41,14])). % 106.04/106.05 cnf(1152,plain, % 106.04/106.05 (P2(f5(a7,a1,a9),a7)), % 106.04/106.05 inference(scs_inference,[],[37,1088,20,118,1133,1094,1124,1005,50,39,40,26,3,41,14,34])). % 106.04/106.05 cnf(1158,plain, % 106.04/106.05 (P2(f5(a1,a7,a9),f6(x11581,f6(a7,x11582)))), % 106.04/106.05 inference(scs_inference,[],[1126,39])). % 106.04/106.05 cnf(1160,plain, % 106.04/106.05 (P2(f5(a1,a7,a9),f6(f6(a7,x11601),x11602))), % 106.04/106.05 inference(scs_inference,[],[1126,39,40])). % 106.04/106.05 cnf(1162,plain, % 106.04/106.05 (~P2(a9,f10(f6(a7,x11621)))), % 106.04/106.05 inference(scs_inference,[],[1146,1126,39,40,38])). % 106.04/106.05 cnf(1164,plain, % 106.04/106.05 (~P2(f6(x11641,f6(x11642,a7)),f5(a1,a7,a9))), % 106.04/106.05 inference(scs_inference,[],[1146,1140,1126,39,40,38,26])). % 106.04/106.05 cnf(1168,plain, % 106.04/106.05 (~E(a1,f6(a7,x11681))), % 106.04/106.05 inference(scs_inference,[],[1146,122,1140,1148,1126,1128,39,40,38,26,41,14])). % 106.04/106.05 cnf(1170,plain, % 106.04/106.05 (P2(f5(f6(a7,x11701),a1,a1),f6(a7,x11701))), % 106.04/106.05 inference(scs_inference,[],[37,1146,122,1140,1148,1126,1128,1150,39,40,38,26,41,14,34])). % 106.04/106.05 cnf(1176,plain, % 106.04/106.05 (P2(f5(f6(x11761,a7),a1,a1),f6(x11762,f6(x11761,a7)))), % 106.04/106.05 inference(scs_inference,[],[1106,39])). % 106.04/106.05 cnf(1178,plain, % 106.04/106.05 (P2(f5(f6(x11781,a7),a1,a1),f6(f6(x11781,a7),x11782))), % 106.04/106.05 inference(scs_inference,[],[1106,39,40])). % 106.04/106.05 cnf(1182,plain, % 106.04/106.05 (~P2(f6(x11821,f6(a7,x11822)),f5(a1,a7,a9))), % 106.04/106.05 inference(scs_inference,[],[1158,1106,1168,39,40,38,26])). % 106.04/106.05 cnf(1188,plain, % 106.04/106.05 (P2(f5(a7,a1,a1),a7)), % 106.04/106.05 inference(scs_inference,[],[37,99,1164,1158,1106,1168,1062,39,40,38,26,41,14,34])). % 106.04/106.05 cnf(1194,plain, % 106.04/106.05 (P2(f5(a7,a1,a9),f6(x11941,a7))), % 106.04/106.05 inference(scs_inference,[],[1152,39])). % 106.04/106.05 cnf(1196,plain, % 106.04/106.05 (P2(f5(a7,a1,a9),f6(a7,x11961))), % 106.04/106.05 inference(scs_inference,[],[1152,39,40])). % 106.04/106.05 cnf(1204,plain, % 106.04/106.05 (~E(f10(a7),f6(x12041,a7))), % 106.04/106.05 inference(scs_inference,[],[81,1182,1160,1152,1082,39,40,26,41,14,4])). % 106.04/106.05 cnf(1207,plain, % 106.04/106.05 (P2(f5(a1,a7,f10(a7)),a7)), % 106.04/106.05 inference(scs_inference,[],[37,81,52,1182,1160,1152,1082,39,40,26,41,14,4,38,34])). % 106.04/106.05 cnf(1212,plain, % 106.04/106.05 (P2(f5(a7,a1,a1),f6(x12121,a7))), % 106.04/106.05 inference(scs_inference,[],[1188,39])). % 106.04/106.05 cnf(1214,plain, % 106.04/106.05 (P2(f5(a7,a1,a1),f6(a7,x12141))), % 106.04/106.05 inference(scs_inference,[],[1188,39,40])). % 106.04/106.05 cnf(1216,plain, % 106.04/106.05 (~P2(f6(f6(x12161,a7),x12162),f5(a1,a7,a9))), % 106.04/106.05 inference(scs_inference,[],[1142,1188,39,40,26])). % 106.04/106.05 cnf(1223,plain, % 106.04/106.05 (P2(f5(a1,a7,f10(a7)),f6(x12231,a7))), % 106.04/106.05 inference(scs_inference,[],[1207,39])). % 106.04/106.05 cnf(1225,plain, % 106.04/106.05 (P2(f5(a1,a7,f10(a7)),f6(a7,x12251))), % 106.04/106.05 inference(scs_inference,[],[1207,39,40])). % 106.04/106.05 cnf(1233,plain, % 106.04/106.05 (P2(f5(f6(a1,a7),a1,a1),a7)), % 106.04/106.05 inference(scs_inference,[],[37,18,99,1216,1207,1176,1133,39,40,26,41,14,32])). % 106.04/106.05 cnf(1238,plain, % 106.04/106.05 (P2(f5(a7,a1,a9),f6(x12381,f6(x12382,a7)))), % 106.04/106.05 inference(scs_inference,[],[1194,39])). % 106.04/106.05 cnf(1240,plain, % 106.04/106.05 (P2(f5(a7,a1,a9),f6(f6(x12401,a7),x12402))), % 106.04/106.05 inference(scs_inference,[],[1194,39,40])). % 106.04/106.05 cnf(1244,plain, % 106.04/106.05 (~P2(x12441,f6(a1,a9))), % 106.04/106.05 inference(scs_inference,[],[37,1096,1194,50,39,40,26,41])). % 106.04/106.05 cnf(1247,plain, % 106.04/106.05 (~E(a1,f6(x12471,a7))), % 106.04/106.05 inference(scs_inference,[],[37,118,1096,1194,1119,50,39,40,26,41,14])). % 106.04/106.05 cnf(1249,plain, % 106.04/106.05 (P2(f5(a1,a7,a1),a7)), % 106.04/106.05 inference(scs_inference,[],[37,118,1096,1194,1119,50,39,40,26,41,14,34])). % 106.04/106.05 cnf(1262,plain, % 106.04/106.05 (~P2(f6(x12621,f6(x12622,a7)),f5(a7,a1,a9))), % 106.04/106.05 inference(scs_inference,[],[1238,1233,1247,39,40,38,26])). % 106.04/106.05 cnf(1264,plain, % 106.04/106.05 (~P2(x12641,f6(a1,f6(a1,a9)))), % 106.04/106.05 inference(scs_inference,[],[37,1238,1233,1244,1247,39,40,38,26,41])). % 106.04/106.05 cnf(1267,plain, % 106.04/106.05 (~E(f6(f10(a7),a9),f6(a7,x12671))), % 106.04/106.05 inference(scs_inference,[],[37,81,1238,1233,1244,1247,1148,39,40,38,26,41,14])). % 106.04/106.05 cnf(1269,plain, % 106.04/106.05 (~E(f10(a7),a7)), % 106.04/106.05 inference(scs_inference,[],[37,81,1238,1233,1244,1247,1148,39,40,38,26,41,14,4])). % 106.04/106.05 cnf(1271,plain, % 106.04/106.05 (P2(f5(a1,a7,a1),f6(x12711,a7))), % 106.04/106.05 inference(scs_inference,[],[1249,39])). % 106.04/106.05 cnf(1273,plain, % 106.04/106.05 (P2(f5(a1,a7,a1),f6(a7,x12731))), % 106.04/106.05 inference(scs_inference,[],[1249,39,40])). % 106.04/106.05 cnf(1283,plain, % 106.04/106.05 (P2(f5(a1,f6(x12831,a7),a1),f6(x12831,a7))), % 106.04/106.05 inference(scs_inference,[],[37,122,1262,1240,1249,1267,1062,39,40,38,26,41,14,34])). % 106.04/106.05 cnf(1288,plain, % 106.04/106.05 (P2(f5(a7,a1,a9),f6(x12881,f6(a7,x12882)))), % 106.04/106.05 inference(scs_inference,[],[1196,39])). % 106.04/106.05 cnf(1290,plain, % 106.04/106.05 (P2(f5(a7,a1,a9),f6(f6(a7,x12901),x12902))), % 106.04/106.05 inference(scs_inference,[],[1196,39,40])). % 106.04/106.05 cnf(1299,plain, % 106.04/106.05 (P2(f5(a7,a1,a1),f6(x12991,f6(x12992,a7)))), % 106.04/106.05 inference(scs_inference,[],[1212,39])). % 106.04/106.05 cnf(1309,plain, % 106.04/106.05 (P2(f5(a1,f6(a7,x13091),a1),f6(a7,x13091))), % 106.04/106.05 inference(scs_inference,[],[37,118,1288,1212,1102,39,40,26,41,14,34])). % 106.04/106.05 cnf(1324,plain, % 106.04/106.05 (~E(f10(a7),f6(a7,x13241))), % 106.04/106.05 inference(scs_inference,[],[83,1290,1214,1133,39,40,26,41,14,4])). % 106.04/106.05 cnf(1327,plain, % 106.04/106.05 (P2(f5(a7,a1,f10(a7)),a7)), % 106.04/106.05 inference(scs_inference,[],[37,83,52,1290,1214,1133,39,40,26,41,14,4,38,34])). % 106.04/106.05 cnf(1334,plain, % 106.04/106.05 (P2(f5(a1,a7,f10(a7)),f6(f6(x13341,a7),x13342))), % 106.04/106.05 inference(scs_inference,[],[1223,39,40])). % 106.04/106.05 cnf(1340,plain, % 106.04/106.05 (P2(f6(f5(a7,a1,a1),f5(a7,a1,a1)),f6(x13401,f6(x13402,a7)))), % 106.04/106.05 inference(scs_inference,[],[67,1299,1223,39,40,26,41,14])). % 106.04/106.05 cnf(1345,plain, % 106.04/106.05 (P2(f5(a7,a1,f10(a7)),f6(a7,x13451))), % 106.04/106.05 inference(scs_inference,[],[1327,39,40])). % 106.04/106.05 cnf(1354,plain, % 106.04/106.05 (P2(f5(a1,a7,f10(a7)),f6(x13541,f6(a7,x13542)))), % 106.04/106.05 inference(scs_inference,[],[1225,39])). % 106.04/106.05 cnf(1378,plain, % 106.04/106.05 (P2(f5(a7,a1,f10(a7)),f6(f6(a7,x13781),x13782))), % 106.04/106.05 inference(scs_inference,[],[1345,39,40])). % 106.04/106.05 cnf(1387,plain, % 106.04/106.05 (P2(f5(a1,a7,a1),f6(f6(x13871,a7),x13872))), % 106.04/106.05 inference(scs_inference,[],[1271,39,40])). % 106.04/106.05 cnf(1391,plain, % 106.04/106.05 (~E(f5(f10(a7),a9,f10(a1)),f6(x13911,a7))), % 106.04/106.05 inference(scs_inference,[],[99,1334,1271,1119,39,40,26,14])). % 106.04/106.05 cnf(1404,plain, % 106.04/106.05 (P2(f6(f5(a7,a1,a1),f5(a7,a1,a1)),a7)), % 106.04/106.05 inference(scs_inference,[],[37,18,99,1340,1354,1273,1148,39,40,26,14,32])). % 106.04/106.05 cnf(1423,plain, % 106.04/106.05 (P2(f6(f5(a7,a1,a1),f5(a7,a1,a1)),f6(a7,x14231))), % 106.04/106.05 inference(scs_inference,[],[1404,39,40])). % 106.04/106.05 cnf(1438,plain, % 106.04/106.05 (P2(f5(f6(a7,x14381),a1,a1),f6(x14382,f6(a7,x14381)))), % 106.04/106.05 inference(scs_inference,[],[1170,39])). % 106.04/106.05 cnf(1453,plain, % 106.04/106.05 (~E(f5(f10(a1),a1,f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[1378,1036,1283,452,39,40,26,14])). % 106.04/106.05 cnf(1468,plain, % 106.04/106.05 (P2(f3(f6(a1,a7)),f6(f6(x14681,a7),x14682))), % 106.04/106.05 inference(scs_inference,[],[1054,39,40])). % 106.04/106.05 cnf(1475,plain, % 106.04/106.05 (P2(f3(f6(a1,a7)),f6(x14751,f6(a7,x14752)))), % 106.04/106.05 inference(scs_inference,[],[1056,39])). % 106.04/106.05 cnf(1477,plain, % 106.04/106.05 (P2(f3(f6(a1,a7)),f6(f6(a7,x14771),x14772))), % 106.04/106.05 inference(scs_inference,[],[1056,39,40])). % 106.04/106.05 cnf(1533,plain, % 106.04/106.05 (P2(f5(a1,f6(x15331,a7),f6(a1,a1)),f6(x15331,a7))), % 106.04/106.05 inference(scs_inference,[],[37,54,151,1468,1062,26,14,34])). % 106.04/106.05 cnf(1539,plain, % 106.04/106.05 (P2(f5(a1,f6(x15391,a7),f6(a1,a1)),f6(f6(x15391,a7),x15392))), % 106.04/106.05 inference(scs_inference,[],[37,54,151,1468,1062,26,14,34,39,40])). % 106.04/106.05 cnf(1551,plain, % 106.04/106.05 (P2(f5(a1,f6(a7,x15511),f6(a1,a1)),f6(a7,x15511))), % 106.04/106.05 inference(scs_inference,[],[37,54,1539,149,1102,26,14,34])). % 106.04/106.05 cnf(1555,plain, % 106.04/106.05 (P2(f5(a1,f6(a7,x15551),f6(a1,a1)),f6(x15552,f6(a7,x15551)))), % 106.04/106.05 inference(scs_inference,[],[37,54,1539,149,1102,26,14,34,39])). % 106.04/106.05 cnf(1563,plain, % 106.04/106.05 (P2(f5(f6(a7,x15631),a1,f6(a1,a1)),f6(a7,x15631))), % 106.04/106.05 inference(scs_inference,[],[37,54,1555,151,1133,26,14,34])). % 106.04/106.05 cnf(1569,plain, % 106.04/106.05 (P2(f5(f6(a7,x15691),a1,f6(a1,a1)),f6(f6(a7,x15691),x15692))), % 106.04/106.05 inference(scs_inference,[],[37,54,1555,151,1133,26,14,34,39,40])). % 106.04/106.05 cnf(1582,plain, % 106.04/106.05 (~E(f5(a1,f10(a1),a1),f6(x15821,a7))), % 106.04/106.05 inference(scs_inference,[],[1569,1074,1119,26,14])). % 106.04/106.05 cnf(1588,plain, % 106.04/106.05 (~E(f5(a1,f10(a1),a1),f6(a7,x15881))), % 106.04/106.05 inference(scs_inference,[],[1475,1076,1148,26,14])). % 106.04/106.05 cnf(1594,plain, % 106.04/106.05 (P2(f6(f5(a7,a1,a9),f5(a7,a1,a9)),a7)), % 106.04/106.05 inference(scs_inference,[],[67,1477,1152,26,14])). % 106.04/106.05 cnf(1596,plain, % 106.04/106.05 (P2(f6(f5(a7,a1,a9),f5(a7,a1,a9)),f6(x15961,a7))), % 106.04/106.05 inference(scs_inference,[],[67,1477,1152,26,14,39])). % 106.04/106.05 cnf(1598,plain, % 106.04/106.05 (P2(f6(f5(a7,a1,a9),f5(a7,a1,a9)),f6(a7,x15981))), % 106.04/106.05 inference(scs_inference,[],[67,1477,1152,26,14,39,40])). % 106.04/106.05 cnf(1602,plain, % 106.04/106.05 (P2(f6(f5(a1,a7,a1),f5(a1,a7,a1)),a7)), % 106.04/106.05 inference(scs_inference,[],[67,1596,1249,26,14])). % 106.04/106.05 cnf(1604,plain, % 106.04/106.05 (P2(f6(f5(a1,a7,a1),f5(a1,a7,a1)),f6(x16041,a7))), % 106.04/106.05 inference(scs_inference,[],[67,1596,1249,26,14,39])). % 106.04/106.05 cnf(1611,plain, % 106.04/106.05 (~E(f5(f10(a1),a1,a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[1598,1094,452,26,14])). % 106.04/106.05 cnf(1647,plain, % 106.04/106.05 (~E(f5(f10(a1),f4(a1,a1),f6(a1,a1)),f6(x16471,a7))), % 106.04/106.05 inference(scs_inference,[],[1551,715,1119,26,14])). % 106.04/106.05 cnf(1653,plain, % 106.04/106.05 (~E(f5(f10(a1),f10(a1),a1),f6(a7,x16531))), % 106.04/106.05 inference(scs_inference,[],[1563,216,1148,26,14])). % 106.04/106.05 cnf(1660,plain, % 106.04/106.05 (~E(f5(a1,f10(a1),a1),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[1178,1076,452,26,14])). % 106.04/106.05 cnf(1667,plain, % 106.04/106.05 (P2(f6(f5(a1,a7,a9),f5(a1,a7,a9)),f6(x16671,a7))), % 106.04/106.05 inference(scs_inference,[],[67,1438,1124,26,14])). % 106.04/106.05 cnf(1671,plain, % 106.04/106.05 (P2(f6(f5(a1,a7,a9),f5(a1,a7,a9)),f6(a7,x16711))), % 106.04/106.05 inference(scs_inference,[],[67,1667,1126,26,14])). % 106.04/106.05 cnf(1675,plain, % 106.04/106.05 (P2(f6(f5(a1,a7,a9),f5(a1,a7,a9)),a7)), % 106.04/106.05 inference(scs_inference,[],[67,1671,1089,26,14])). % 106.04/106.05 cnf(1711,plain, % 106.04/106.05 (~E(f10(a7),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[140,18,2,3])). % 106.04/106.05 cnf(1714,plain, % 106.04/106.05 (P2(f5(f10(a1),f10(a1),f10(a7)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[1711,52,1387,26,34])). % 106.04/106.05 cnf(1719,plain, % 106.04/106.05 (P2(f5(f10(a1),f10(a1),f10(a7)),f6(f10(a1),x17191))), % 106.04/106.05 inference(scs_inference,[],[1711,52,1387,26,34,39,40])). % 106.04/106.05 cnf(1751,plain, % 106.04/106.05 (~P2(a7,f5(a7,a1,a1))), % 106.04/106.05 inference(scs_inference,[],[1188,26])). % 106.04/106.05 cnf(1775,plain, % 106.04/106.05 (~P2(f6(x17751,a7),f5(a7,a1,a9))), % 106.04/106.05 inference(scs_inference,[],[1194,26])). % 106.04/106.05 cnf(1777,plain, % 106.04/106.05 (P1(f6(f10(a7),f10(a7)))), % 106.04/106.05 inference(scs_inference,[],[106,67,27,13])). % 106.04/106.05 cnf(1778,plain, % 106.04/106.05 (~P2(f6(a7,x17781),f5(a7,a1,a9))), % 106.04/106.05 inference(scs_inference,[],[1196,26])). % 106.04/106.05 cnf(1782,plain, % 106.04/106.05 (P1(f6(a9,a9))), % 106.04/106.05 inference(scs_inference,[],[106,67,28,13])). % 106.04/106.05 cnf(1783,plain, % 106.04/106.05 (~P2(f6(a7,x17831),f5(a7,a1,a1))), % 106.04/106.05 inference(scs_inference,[],[1214,26])). % 106.04/106.05 cnf(1787,plain, % 106.04/106.05 (E(f3(f10(a1)),a1)), % 106.04/106.05 inference(scs_inference,[],[193,22,38])). % 106.04/106.05 cnf(1788,plain, % 106.04/106.05 (~P2(x17881,f3(f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1787,23])). % 106.04/106.05 cnf(1790,plain, % 106.04/106.05 (E(a1,f3(f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1787,23,2])). % 106.04/106.05 cnf(1793,plain, % 106.04/106.05 (P1(f3(f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[1787,1225,16,23,2,26,13])). % 106.04/106.05 cnf(1822,plain, % 106.04/106.05 (E(f10(f6(a1,a1)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[137,38,6])). % 106.04/106.05 cnf(1823,plain, % 106.04/106.05 (E(f10(a1),f10(f6(a1,a1)))), % 106.04/106.05 inference(scs_inference,[],[1822,2])). % 106.04/106.05 cnf(1826,plain, % 106.04/106.05 (P2(f6(f10(a7),a9),f10(f6(a1,a1)))), % 106.04/106.05 inference(scs_inference,[],[19,1822,1309,2,26,24])). % 106.04/106.05 cnf(1832,plain, % 106.04/106.05 (~P2(x18321,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(1836,plain, % 106.04/106.05 (E(f4(f6(a1,a1),f10(a7)),f6(a1,a1))), % 106.04/106.05 inference(scs_inference,[],[37,19,310,311,1822,52,1309,2,26,24,25,3,15,6,38,29])). % 106.04/106.05 cnf(1840,plain, % 106.04/106.05 (~P2(f10(f6(a1,a1)),f6(f10(a1),f10(a1)))), % 106.04/106.05 inference(scs_inference,[],[37,19,310,311,1822,52,1309,2,26,24,25,3,15,6,38,29,13,41])). % 106.04/106.05 cnf(1842,plain, % 106.04/106.05 (~P2(x18421,f4(f6(a1,a1),f10(a7)))), % 106.04/106.05 inference(scs_inference,[],[37,1832,19,310,311,1822,52,1309,2,26,24,25,3,15,6,38,29,13,41,32])). % 106.04/106.05 cnf(1844,plain, % 106.04/106.05 (P2(f5(a1,a1,a7),a7)), % 106.04/106.05 inference(scs_inference,[],[37,1832,19,310,311,1822,52,1309,2,26,24,25,3,15,6,38,29,13,41,32,34])). % 106.04/106.05 cnf(1847,plain, % 106.04/106.05 (P2(f5(a1,a1,a7),f6(x18471,a7))), % 106.04/106.05 inference(scs_inference,[],[37,1832,19,310,311,1822,52,1309,2,26,24,25,3,15,6,38,29,13,41,32,34,39])). % 106.04/106.05 cnf(1849,plain, % 106.04/106.05 (P2(f5(a1,a1,a7),f6(a7,x18491))), % 106.04/106.05 inference(scs_inference,[],[37,1832,19,310,311,1822,52,1309,2,26,24,25,3,15,6,38,29,13,41,32,34,39,40])). % 106.04/106.05 cnf(1851,plain, % 106.04/106.05 (P2(f6(f5(a1,a1,a7),f5(a1,a1,a7)),a7)), % 106.04/106.05 inference(scs_inference,[],[37,1832,19,67,310,311,1822,52,1309,2,26,24,25,3,15,6,38,29,13,41,32,34,39,40,14])). % 106.04/106.05 cnf(1855,plain, % 106.04/106.05 (P2(f5(a1,a1,a7),f6(x18551,f6(a7,x18552)))), % 106.04/106.05 inference(scs_inference,[],[1836,1849,2,39])). % 106.04/106.05 cnf(1857,plain, % 106.04/106.05 (P2(f5(a1,a1,a7),f6(f6(a7,x18571),x18572))), % 106.04/106.05 inference(scs_inference,[],[1836,1849,2,39,40])). % 106.04/106.05 cnf(1859,plain, % 106.04/106.05 (~P2(a7,f5(a7,a1,a9))), % 106.04/106.05 inference(scs_inference,[],[1152,1836,1849,2,39,40,26])). % 106.04/106.05 cnf(1861,plain, % 106.04/106.05 (~E(f6(x18611,f10(a1)),f6(a1,a1))), % 106.04/106.05 inference(scs_inference,[],[1823,1152,205,1836,1849,2,39,40,26,24])). % 106.04/106.05 cnf(1865,plain, % 106.04/106.05 (P1(f4(f6(a1,a1),f10(a7)))), % 106.04/106.05 inference(scs_inference,[],[193,953,1823,1822,1152,205,1836,1849,2,39,40,26,24,25,13])). % 106.04/106.05 cnf(1871,plain, % 106.04/106.05 (P2(f5(a1,a1,a7),f6(f6(x18711,a7),x18712))), % 106.04/106.05 inference(scs_inference,[],[1847,40])). % 106.04/106.05 cnf(1873,plain, % 106.04/106.05 (~P2(a7,f5(a1,a7,a1))), % 106.04/106.05 inference(scs_inference,[],[1249,1847,40,26])). % 106.04/106.05 cnf(1875,plain, % 106.04/106.05 (P2(f5(a1,a1,a7),f6(x18751,f6(x18752,a7)))), % 106.04/106.05 inference(scs_inference,[],[1249,1847,40,26,39])). % 106.04/106.05 cnf(1881,plain, % 106.04/106.05 (E(f4(f6(a1,a1),a1),f6(a1,a1))), % 106.04/106.05 inference(scs_inference,[],[37,1823,1249,118,240,1847,1840,40,26,39,24,14,29])). % 106.04/106.05 cnf(1882,plain, % 106.04/106.05 (~P2(x18821,a1)), % 106.04/106.05 inference(rename_variables,[],[37])). % 106.04/106.05 cnf(1885,plain, % 106.04/106.05 (~P2(x18851,f4(f6(a1,a1),a1))), % 106.04/106.05 inference(scs_inference,[],[37,1882,1861,1823,1249,118,240,1847,1840,1836,40,26,39,24,14,29,3,32])). % 106.04/106.05 cnf(1887,plain, % 106.04/106.05 (E(f6(a1,a1),f4(f6(a1,a1),a1))), % 106.04/106.05 inference(scs_inference,[],[37,1882,1861,1823,1249,118,240,1847,1840,1836,40,26,39,24,14,29,3,32,2])). % 106.04/106.05 cnf(1900,plain, % 106.04/106.05 (P2(f6(f5(a1,a1,a7),f5(a1,a1,a7)),f6(a7,x19001))), % 106.04/106.05 inference(scs_inference,[],[1851,40])). % 106.04/106.05 cnf(1904,plain, % 106.04/106.05 (P2(f6(f5(a1,a1,a7),f5(a1,a1,a7)),f6(x19041,a7))), % 106.04/106.05 inference(scs_inference,[],[1124,1851,40,26,39])). % 106.04/106.05 cnf(1906,plain, % 106.04/106.05 (~E(f10(a1),f6(a1,a1))), % 106.04/106.05 inference(scs_inference,[],[1823,1124,218,1851,40,26,39,24])). % 106.04/106.05 cnf(1909,plain, % 106.04/106.05 (~P2(x19091,f6(f10(a7),a9))), % 106.04/106.05 inference(rename_variables,[],[42])). % 106.04/106.05 cnf(1910,plain, % 106.04/106.05 (P1(f4(f6(a1,a1),a1))), % 106.04/106.05 inference(scs_inference,[],[42,953,1887,1826,1823,1124,218,1851,40,26,39,24,15,13])). % 106.04/106.05 cnf(1911,plain, % 106.04/106.05 (~E(f5(f10(a1),f10(a1),f10(a7)),f10(a1))), % 106.04/106.05 inference(scs_inference,[],[42,953,1887,1826,1823,1714,1124,218,1851,40,26,39,24,15,13,14])). % 106.04/106.05 cnf(1912,plain, % 106.04/106.05 (E(a1,f4(f6(a1,a1),a1))), % 106.04/106.05 inference(scs_inference,[],[42,67,953,1887,1826,1823,1714,1124,218,1851,40,26,39,24,15,13,14,3])). % 106.04/106.05 cnf(1921,plain, % 106.04/106.05 (E(f4(f6(a1,a1),a1),a1)), % 106.04/106.05 inference(scs_inference,[],[42,1909,1204,67,953,1887,1826,1823,1714,1124,218,52,1851,40,26,39,24,15,13,14,3,34,38,2])). % 106.04/106.05 cnf(1924,plain, % 106.04/106.05 (~P2(f6(a7,x19241),f5(a1,a7,a9))), % 106.04/106.05 inference(scs_inference,[],[1126,1900,40,26])). % 106.04/106.05 cnf(1929,plain, % 106.04/106.05 (~P2(x19291,f6(f10(a7),a9))), % 106.04/106.05 inference(rename_variables,[],[42])). % 106.04/106.05 cnf(1939,plain, % 106.04/106.05 (~P2(f6(a7,x19391),f10(a9))), % 106.04/106.05 inference(scs_inference,[],[42,1929,1324,311,1921,1126,99,52,462,1900,1840,40,26,39,15,14,3,34,5,38])). % 106.04/106.05 cnf(1954,plain, % 106.04/106.05 (P2(f5(a1,a1,f10(a1)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[42,37,193,1906,1921,1719,1238,1054,1904,1840,40,39,26,15,14,3,34])). % 106.04/106.06 cnf(1958,plain, % 106.04/106.06 (~P2(f6(x19581,a7),f10(a9))), % 106.04/106.06 inference(scs_inference,[],[42,37,193,1906,1921,1719,1238,1054,1904,1840,40,39,26,15,14,3,34,5,38])). % 106.04/106.06 cnf(2009,plain, % 106.04/106.06 (~P2(a7,f5(a1,a1,a7))), % 106.04/106.06 inference(scs_inference,[],[1844,26])). % 106.04/106.06 cnf(2020,plain, % 106.04/106.06 (~P2(f6(f6(x20201,a7),x20202),f5(a1,a1,a7))), % 106.04/106.06 inference(scs_inference,[],[1871,26])). % 106.04/106.06 cnf(2032,plain, % 106.04/106.06 (~E(f5(f4(a1,a1),f10(a1),a1),f6(a7,x20321))), % 106.04/106.06 inference(scs_inference,[],[314,1875,1148,26,41,14])). % 106.04/106.06 cnf(2078,plain, % 106.04/106.06 (~P2(f6(a7,x20781),f5(a1,a1,a7))), % 106.04/106.06 inference(scs_inference,[],[1849,26])). % 106.04/106.06 cnf(2080,plain, % 106.04/106.06 (~P2(f6(x20801,a7),f5(a1,a1,a7))), % 106.04/106.06 inference(scs_inference,[],[1847,26])). % 106.04/106.06 cnf(2085,plain, % 106.04/106.06 (~E(f10(f6(a1,a1)),f4(a1,a9))), % 106.04/106.06 inference(scs_inference,[],[234,1826,15])). % 106.04/106.06 cnf(2086,plain, % 106.04/106.06 (~P2(x20861,f4(a1,a9))), % 106.04/106.06 inference(rename_variables,[],[234])). % 106.04/106.06 cnf(2087,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,a9),a7)), % 106.04/106.06 inference(scs_inference,[],[234,2086,1088,1826,50,15,34])). % 106.04/106.06 cnf(2092,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,a9),f6(a7,x20921))), % 106.04/106.06 inference(scs_inference,[],[234,2086,1088,1826,50,15,34,40])). % 106.04/106.06 cnf(2096,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,a9),f6(x20961,a7))), % 106.04/106.06 inference(scs_inference,[],[234,2086,1088,1826,50,15,34,40,38,39])). % 106.04/106.06 cnf(2101,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,a9),f6(f6(x21011,a7),x21012))), % 106.04/106.06 inference(scs_inference,[],[2096,40])). % 106.04/106.06 cnf(2103,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,a9),f6(x21031,f6(x21032,a7)))), % 106.04/106.06 inference(scs_inference,[],[2096,40,39])). % 106.04/106.06 cnf(2107,plain, % 106.04/106.06 (~E(f10(f6(a1,a1)),f4(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[291,1826,2096,40,39,26,15])). % 106.04/106.06 cnf(2108,plain, % 106.04/106.06 (~P2(x21081,f4(a1,a1))), % 106.04/106.06 inference(rename_variables,[],[291])). % 106.04/106.06 cnf(2109,plain, % 106.04/106.06 (P2(f5(f4(a1,a1),a7,a9),a7)), % 106.04/106.06 inference(scs_inference,[],[291,2108,1088,1826,50,2096,40,39,26,15,34])). % 106.04/106.06 cnf(2116,plain, % 106.04/106.06 (E(f6(a1,a1),f6(f10(a7),a9))), % 106.04/106.06 inference(scs_inference,[],[1826,38,2])). % 106.04/106.06 cnf(2117,plain, % 106.04/106.06 (E(f6(f10(a7),a9),f6(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[2116,2])). % 106.04/106.06 cnf(2118,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,a9),f6(f6(a7,x21181),x21182))), % 106.04/106.06 inference(scs_inference,[],[2116,2092,2,40])). % 106.04/106.06 cnf(2120,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,a9),f6(x21201,f6(a7,x21202)))), % 106.04/106.06 inference(scs_inference,[],[2116,2092,2,40,39])). % 106.04/106.06 cnf(2124,plain, % 106.04/106.06 (P2(f5(a7,f4(a1,a9),a9),a7)), % 106.04/106.06 inference(scs_inference,[],[234,1146,2116,50,2101,2092,2,40,39,26,34])). % 106.04/106.06 cnf(2130,plain, % 106.04/106.06 (P2(f5(a7,f4(a1,a9),a9),f6(a7,x21301))), % 106.04/106.06 inference(scs_inference,[],[2124,40])). % 106.04/106.06 cnf(2132,plain, % 106.04/106.06 (P2(f5(a7,f4(a1,a9),a9),f6(x21321,a7))), % 106.04/106.06 inference(scs_inference,[],[2124,40,39])). % 106.04/106.06 cnf(2137,plain, % 106.04/106.06 (~P2(x21371,f4(a1,a1))), % 106.04/106.06 inference(rename_variables,[],[291])). % 106.04/106.06 cnf(2138,plain, % 106.04/106.06 (P2(f5(a7,f4(a1,a1),a9),a7)), % 106.04/106.06 inference(scs_inference,[],[291,2137,1146,464,50,2103,2124,40,39,26,15,34])). % 106.04/106.06 cnf(2152,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,f10(a7)),a7)), % 106.04/106.06 inference(scs_inference,[],[234,1204,52,2118,2130,40,39,26,34])). % 106.04/106.06 cnf(2158,plain, % 106.04/106.06 (P2(f5(a7,f4(a1,a9),a9),f6(f6(x21581,a7),x21582))), % 106.04/106.06 inference(scs_inference,[],[2132,40])). % 106.04/106.06 cnf(2164,plain, % 106.04/106.06 (~E(f6(x21641,f6(x21642,a7)),f4(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[291,1299,2120,2132,40,39,26,15])). % 106.04/106.06 cnf(2165,plain, % 106.04/106.06 (~P2(x21651,f4(a1,a1))), % 106.04/106.06 inference(rename_variables,[],[291])). % 106.04/106.06 cnf(2166,plain, % 106.04/106.06 (P2(f5(f4(a1,a1),a7,f10(a7)),a7)), % 106.04/106.06 inference(scs_inference,[],[291,2165,1204,52,1299,2120,2132,40,39,26,15,34])). % 106.04/106.06 cnf(2174,plain, % 106.04/106.06 (P2(f5(f4(a1,a1),a7,a9),f6(a7,x21741))), % 106.04/106.06 inference(scs_inference,[],[2109,40])). % 106.04/106.06 cnf(2176,plain, % 106.04/106.06 (P2(f5(f4(a1,a1),a7,a9),f6(x21761,a7))), % 106.04/106.06 inference(scs_inference,[],[2109,40,39])). % 106.04/106.06 cnf(2180,plain, % 106.04/106.06 (P2(f5(a7,f4(a1,a9),f10(a7)),a7)), % 106.04/106.06 inference(scs_inference,[],[234,1324,52,2158,2109,40,39,26,34])). % 106.04/106.06 cnf(2186,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,f10(a7)),f6(a7,x21861))), % 106.04/106.06 inference(scs_inference,[],[2152,40])). % 106.04/106.06 cnf(2188,plain, % 106.04/106.06 (P2(f5(f4(a1,a9),a7,f10(a7)),f6(x21881,a7))), % 106.04/106.06 inference(scs_inference,[],[2152,40,39])). % 106.04/106.06 cnf(2192,plain, % 106.04/106.06 (P2(f5(a7,f4(a1,a1),f10(a7)),a7)), % 106.04/106.06 inference(scs_inference,[],[291,1324,52,2174,2152,40,39,26,34])). % 106.04/106.06 cnf(2198,plain, % 106.04/106.06 (E(f3(a1),f3(f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[293,12])). % 106.04/106.06 cnf(2199,plain, % 106.04/106.06 (E(f4(a1,x21991),f4(f4(a1,a1),x21991))), % 106.04/106.06 inference(scs_inference,[],[293,12,10])). % 106.04/106.06 cnf(2200,plain, % 106.04/106.06 (E(f4(x22001,a1),f4(x22001,f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[293,12,10,11])). % 106.04/106.06 cnf(2201,plain, % 106.04/106.06 (E(f5(a1,x22011,x22012),f5(f4(a1,a1),x22011,x22012))), % 106.04/106.06 inference(scs_inference,[],[293,12,10,11,7])). % 106.04/106.06 cnf(2202,plain, % 106.04/106.06 (E(f5(x22021,a1,x22022),f5(x22021,f4(a1,a1),x22022))), % 106.04/106.06 inference(scs_inference,[],[293,12,10,11,7,8])). % 106.04/106.06 cnf(2204,plain, % 106.04/106.06 (~P1(f6(a8,x22041))), % 106.04/106.06 inference(scs_inference,[],[293,21,12,10,11,7,8,9,28])). % 106.04/106.06 cnf(2206,plain, % 106.04/106.06 (~P1(f6(x22061,a8))), % 106.04/106.06 inference(scs_inference,[],[293,21,12,10,11,7,8,9,28,27])). % 106.04/106.06 cnf(2208,plain, % 106.04/106.06 (E(f6(a1,a9),a1)), % 106.04/106.06 inference(scs_inference,[],[293,21,1244,12,10,11,7,8,9,28,27,22])). % 106.04/106.06 cnf(2209,plain, % 106.04/106.06 (~P2(x22091,f6(a1,a9))), % 106.04/106.06 inference(rename_variables,[],[1244])). % 106.04/106.06 cnf(2213,plain, % 106.04/106.06 (E(f10(a1),f10(f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[293,21,1244,12,10,11,7,8,9,28,27,22,5,4,6])). % 106.04/106.06 cnf(2214,plain, % 106.04/106.06 (~E(f4(a1,a9),f6(x22141,a7))), % 106.04/106.06 inference(scs_inference,[],[570,293,21,1244,12,10,11,7,8,9,28,27,22,5,4,6,2])). % 106.04/106.06 cnf(2215,plain, % 106.04/106.06 (E(f5(a1,f10(a1),f6(a1,a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[570,293,21,1244,968,12,10,11,7,8,9,28,27,22,5,4,6,2,38])). % 106.04/106.06 cnf(2219,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),a1),f6(a7,x22191))), % 106.04/106.06 inference(scs_inference,[],[570,2186,1885,2087,293,21,1244,968,12,10,11,7,8,9,28,27,22,5,4,6,2,38,26,31])). % 106.04/106.06 cnf(2220,plain, % 106.04/106.06 (~P2(x22201,f4(f6(a1,a1),a1))), % 106.04/106.06 inference(rename_variables,[],[1885])). % 106.04/106.06 cnf(2222,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),a1),f6(x22221,a7))), % 106.04/106.06 inference(scs_inference,[],[570,2186,1885,2220,2087,293,21,1244,968,12,10,11,7,8,9,28,27,22,5,4,6,2,38,26,31,30])). % 106.04/106.06 cnf(2223,plain, % 106.04/106.06 (~P2(x22231,f4(f6(a1,a1),a1))), % 106.04/106.06 inference(rename_variables,[],[1885])). % 106.04/106.06 cnf(2230,plain, % 106.04/106.06 (~E(a9,a8)), % 106.04/106.06 inference(scs_inference,[],[19,77,551,570,2186,1885,2220,2223,2087,293,21,1244,968,149,12,10,11,7,8,9,28,27,22,5,4,6,2,38,26,31,30,24,25,13])). % 106.04/106.06 cnf(2231,plain, % 106.04/106.06 (~E(f6(a1,a1),f6(a7,x22311))), % 106.04/106.06 inference(scs_inference,[],[19,77,551,570,1881,2186,1885,2220,2223,2087,293,21,1244,968,149,12,10,11,7,8,9,28,27,22,5,4,6,2,38,26,31,30,24,25,13,3])). % 106.04/106.06 cnf(2232,plain, % 106.04/106.06 (~P2(x22321,f6(f6(a1,a1),f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[19,77,551,570,1881,2186,1885,2220,2223,2087,787,293,21,1244,968,149,20,12,10,11,7,8,9,28,27,22,5,4,6,2,38,26,31,30,24,25,13,3,15])). % 106.04/106.06 cnf(2233,plain, % 106.04/106.06 (E(f6(x22331,x22332),f6(x22332,x22331))), % 106.04/106.06 inference(rename_variables,[],[20])). % 106.04/106.06 cnf(2235,plain, % 106.04/106.06 (~P2(x22351,f6(a1,a9))), % 106.04/106.06 inference(rename_variables,[],[1244])). % 106.04/106.06 cnf(2241,plain, % 106.04/106.06 (~P2(f4(a7,f6(a1,a9)),f5(a1,a7,a1))+E(f6(a1,a9),f10(a7))), % 106.04/106.06 inference(scs_inference,[],[19,77,551,1873,570,1881,2186,1885,2220,2223,2087,787,293,21,1244,2209,2235,968,149,20,2233,12,10,11,7,8,9,28,27,22,5,4,6,2,38,26,31,30,24,25,13,3,15,32,29,14])). % 106.04/106.06 cnf(2243,plain, % 106.04/106.06 (~P1(f6(f6(a8,x22431),x22432))), % 106.04/106.06 inference(scs_inference,[],[2204,28])). % 106.04/106.06 cnf(2245,plain, % 106.04/106.06 (E(f4(x22451,f6(a1,a9)),f4(x22451,a1))), % 106.04/106.06 inference(scs_inference,[],[2204,2208,28,11])). % 106.04/106.06 cnf(2246,plain, % 106.04/106.06 (E(f4(f6(a1,a9),x22461),f4(a1,x22461))), % 106.04/106.06 inference(scs_inference,[],[2204,2208,28,11,10])). % 106.04/106.06 cnf(2247,plain, % 106.04/106.06 (~P1(f6(x22471,f6(a8,x22472)))), % 106.04/106.06 inference(scs_inference,[],[2204,2208,28,11,10,27])). % 106.04/106.06 cnf(2249,plain, % 106.04/106.06 (E(f5(x22491,x22492,f6(a1,a9)),f5(x22491,x22492,a1))), % 106.04/106.06 inference(scs_inference,[],[2204,2208,28,11,10,27,9])). % 106.04/106.06 cnf(2251,plain, % 106.04/106.06 (E(f5(x22511,f6(a1,a9),x22512),f5(x22511,a1,x22512))), % 106.04/106.06 inference(scs_inference,[],[2204,2208,28,11,10,27,9,12,8])). % 106.04/106.06 cnf(2253,plain, % 106.04/106.06 (E(a9,a1)), % 106.04/106.06 inference(scs_inference,[],[2204,2208,50,28,11,10,27,9,12,8,7,22])). % 106.04/106.06 cnf(2256,plain, % 106.04/106.06 (E(f6(x22561,f6(a1,a9)),f6(x22561,a1))), % 106.04/106.06 inference(scs_inference,[],[2204,2208,50,28,11,10,27,9,12,8,7,22,5])). % 106.04/106.06 cnf(2257,plain, % 106.04/106.06 (E(f6(f6(a1,a9),x22571),f6(a1,x22571))), % 106.04/106.06 inference(scs_inference,[],[2204,2208,50,28,11,10,27,9,12,8,7,22,5,4])). % 106.04/106.06 cnf(2258,plain, % 106.04/106.06 (E(f10(f6(a1,a9)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[2204,2208,50,28,11,10,27,9,12,8,7,22,5,4,6])). % 106.04/106.06 cnf(2259,plain, % 106.04/106.06 (~E(a8,a9)), % 106.04/106.06 inference(scs_inference,[],[2230,2204,2208,50,28,11,10,27,9,12,8,7,22,5,4,6,2])). % 106.04/106.06 cnf(2260,plain, % 106.04/106.06 (E(f5(f10(a1),f4(a1,a9),a1),a1)), % 106.04/106.06 inference(scs_inference,[],[2230,2204,2208,747,50,28,11,10,27,9,12,8,7,22,5,4,6,2,38])). % 106.04/106.06 cnf(2265,plain, % 106.04/106.06 (~P2(x22651,f6(a1,a9))), % 106.04/106.06 inference(rename_variables,[],[1244])). % 106.04/106.06 cnf(2270,plain, % 106.04/106.06 (~P2(a9,f6(f10(a7),f10(a7)))), % 106.04/106.06 inference(scs_inference,[],[1130,2230,2204,2208,2188,1244,2265,747,18,50,28,11,10,27,9,12,8,7,22,5,4,6,2,38,26,31,30,25])). % 106.04/106.06 cnf(2274,plain, % 106.04/106.06 (E(x22741,f6(x22741,x22741))), % 106.04/106.06 inference(rename_variables,[],[67])). % 106.04/106.06 cnf(2276,plain, % 106.04/106.06 (~E(f4(a1,a9),f6(a8,x22761))), % 106.04/106.06 inference(scs_inference,[],[1130,2230,2009,237,2204,2208,2188,1244,2265,747,18,50,67,28,11,10,27,9,12,8,7,22,5,4,6,2,38,26,31,30,25,24,13])). % 106.04/106.06 cnf(2277,plain, % 106.04/106.06 (~E(f6(a9,a9),a7)), % 106.04/106.06 inference(scs_inference,[],[1130,2230,2009,237,2204,2208,2188,1244,2265,747,18,50,67,2274,28,11,10,27,9,12,8,7,22,5,4,6,2,38,26,31,30,25,24,13,3])). % 106.04/106.06 cnf(2279,plain, % 106.04/106.06 (~P2(x22791,f5(a1,f10(a1),f6(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[1130,2230,2009,237,2204,2208,2188,2215,1244,2265,747,18,50,67,2274,37,28,11,10,27,9,12,8,7,22,5,4,6,2,38,26,31,30,25,24,13,3,15])). % 106.04/106.06 cnf(2285,plain, % 106.04/106.06 (~P2(f4(a7,f6(a1,a9)),f5(a1,a7,a1))), % 106.04/106.06 inference(scs_inference,[],[18,1244,2241,24])). % 106.04/106.06 cnf(2286,plain, % 106.04/106.06 (~P1(f6(f6(x22861,a8),x22862))), % 106.04/106.06 inference(scs_inference,[],[2206,28])). % 106.04/106.06 cnf(2288,plain, % 106.04/106.06 (E(f4(a9,x22881),f4(a1,x22881))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,28,10])). % 106.04/106.06 cnf(2289,plain, % 106.04/106.06 (E(f4(x22891,a9),f4(x22891,a1))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,28,10,11])). % 106.04/106.06 cnf(2290,plain, % 106.04/106.06 (~P1(f6(x22901,f6(x22902,a8)))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,28,10,11,27])). % 106.04/106.06 cnf(2292,plain, % 106.04/106.06 (E(f5(x22921,a9,x22922),f5(x22921,a1,x22922))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,28,10,11,27,8])). % 106.04/106.06 cnf(2293,plain, % 106.04/106.06 (E(f10(a7),a1)), % 106.04/106.06 inference(scs_inference,[],[2253,2206,52,28,10,11,27,8,22])). % 106.04/106.06 cnf(2296,plain, % 106.04/106.06 (E(f5(a9,x22961,x22962),f5(a1,x22961,x22962))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,52,28,10,11,27,8,22,7])). % 106.04/106.06 cnf(2297,plain, % 106.04/106.06 (E(f3(a9),f3(a1))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,52,28,10,11,27,8,22,7,12])). % 106.04/106.06 cnf(2298,plain, % 106.04/106.06 (E(f5(x22981,x22982,a9),f5(x22981,x22982,a1))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,52,28,10,11,27,8,22,7,12,9])). % 106.04/106.06 cnf(2299,plain, % 106.04/106.06 (E(f6(x22991,a9),f6(x22991,a1))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,52,28,10,11,27,8,22,7,12,9,5])). % 106.04/106.06 cnf(2300,plain, % 106.04/106.06 (E(f10(a9),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,52,28,10,11,27,8,22,7,12,9,5,6])). % 106.04/106.06 cnf(2301,plain, % 106.04/106.06 (E(f6(a9,x23011),f6(a1,x23011))), % 106.04/106.06 inference(scs_inference,[],[2253,2206,52,28,10,11,27,8,22,7,12,9,5,6,4])). % 106.04/106.06 cnf(2302,plain, % 106.04/106.06 (~E(f4(a1,a9),f6(a7,x23021))), % 106.04/106.06 inference(scs_inference,[],[2253,684,2206,52,28,10,11,27,8,22,7,12,9,5,6,4,2])). % 106.04/106.06 cnf(2303,plain, % 106.04/106.06 (E(f5(f10(a1),f4(a1,a1),a1),a1)), % 106.04/106.06 inference(scs_inference,[],[2253,684,2206,774,52,28,10,11,27,8,22,7,12,9,5,6,4,2,38])). % 106.04/106.06 cnf(2307,plain, % 106.04/106.06 (~E(f6(f6(a1,a1),f4(a1,a9)),f6(x23071,a7))), % 106.04/106.06 inference(scs_inference,[],[2253,684,2206,2176,2232,2138,774,52,28,10,11,27,8,22,7,12,9,5,6,4,2,38,26,30])). % 106.04/106.06 cnf(2308,plain, % 106.04/106.06 (~P2(x23081,f6(f6(a1,a1),f4(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[2232])). % 106.04/106.06 cnf(2310,plain, % 106.04/106.06 (~E(f6(f6(a1,a1),f4(a1,a9)),f6(a7,x23101))), % 106.04/106.06 inference(scs_inference,[],[2253,684,2206,2176,2232,2308,2138,774,52,28,10,11,27,8,22,7,12,9,5,6,4,2,38,26,30,31])). % 106.04/106.06 cnf(2311,plain, % 106.04/106.06 (~P2(x23111,f6(f6(a1,a1),f4(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[2232])). % 106.04/106.06 cnf(2313,plain, % 106.04/106.06 (~E(f6(f6(a1,a1),f4(a1,a9)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2253,684,2206,2176,2232,2308,2311,2138,774,52,28,10,11,27,8,22,7,12,9,5,6,4,2,38,26,30,31,24])). % 106.04/106.06 cnf(2318,plain, % 106.04/106.06 (~E(f4(a1,a1),f6(x23181,a8))), % 106.04/106.06 inference(scs_inference,[],[19,2253,294,684,2206,933,2176,2232,2308,2311,2138,774,52,28,10,11,27,8,22,7,12,9,5,6,4,2,38,26,30,31,24,25,13])). % 106.04/106.06 cnf(2319,plain, % 106.04/106.06 (~E(a1,a8)), % 106.04/106.06 inference(scs_inference,[],[19,2253,294,684,2206,933,2176,2232,2308,2311,2138,2230,774,52,28,10,11,27,8,22,7,12,9,5,6,4,2,38,26,30,31,24,25,13,3])). % 106.04/106.06 cnf(2323,plain, % 106.04/106.06 (E(f4(x23231,f10(a7)),f4(x23231,a1))), % 106.04/106.06 inference(scs_inference,[],[2293,11])). % 106.04/106.06 cnf(2324,plain, % 106.04/106.06 (E(f4(f10(a7),x23241),f4(a1,x23241))), % 106.04/106.06 inference(scs_inference,[],[2293,11,10])). % 106.04/106.06 cnf(2325,plain, % 106.04/106.06 (E(f5(f10(a7),x23251,x23252),f5(a1,x23251,x23252))), % 106.04/106.06 inference(scs_inference,[],[2293,11,10,7])). % 106.04/106.06 cnf(2326,plain, % 106.04/106.06 (E(f5(x23261,x23262,f10(a7)),f5(x23261,x23262,a1))), % 106.04/106.06 inference(scs_inference,[],[2293,11,10,7,9])). % 106.04/106.06 cnf(2327,plain, % 106.04/106.06 (E(f5(x23271,f10(a7),x23272),f5(x23271,a1,x23272))), % 106.04/106.06 inference(scs_inference,[],[2293,11,10,7,9,8])). % 106.04/106.06 cnf(2329,plain, % 106.04/106.06 (E(f6(x23291,f10(a7)),f6(x23291,a1))), % 106.04/106.06 inference(scs_inference,[],[2293,11,10,7,9,8,12,5])). % 106.04/106.06 cnf(2330,plain, % 106.04/106.06 (E(f6(f10(a7),x23301),f6(a1,x23301))), % 106.04/106.06 inference(scs_inference,[],[2293,11,10,7,9,8,12,5,4])). % 106.04/106.06 cnf(2331,plain, % 106.04/106.06 (~E(a8,a1)), % 106.04/106.06 inference(scs_inference,[],[2319,2293,11,10,7,9,8,12,5,4,2])). % 106.04/106.06 cnf(2332,plain, % 106.04/106.06 (E(f10(f10(a7)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[2319,2293,11,10,7,9,8,12,5,4,2,6])). % 106.04/106.06 cnf(2333,plain, % 106.04/106.06 (E(f5(f10(a1),a1,f6(a1,a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[2319,2293,998,11,10,7,9,8,12,5,4,2,6,38])). % 106.04/106.06 cnf(2335,plain, % 106.04/106.06 (~P2(a7,f5(f4(a1,a1),a7,f10(a7)))), % 106.04/106.06 inference(scs_inference,[],[2319,2293,2166,998,11,10,7,9,8,12,5,4,2,6,38,26])). % 106.04/106.06 cnf(2337,plain, % 106.04/106.06 (~E(f5(a1,f10(a1),f6(a1,a1)),f6(a7,x23371))), % 106.04/106.06 inference(scs_inference,[],[2319,2293,2279,2166,998,11,10,7,9,8,12,5,4,2,6,38,26,31])). % 106.04/106.06 cnf(2338,plain, % 106.04/106.06 (~P2(x23381,f5(a1,f10(a1),f6(a1,a1)))), % 106.04/106.06 inference(rename_variables,[],[2279])). % 106.04/106.06 cnf(2340,plain, % 106.04/106.06 (~E(f5(a1,f10(a1),f6(a1,a1)),f6(x23401,a7))), % 106.04/106.06 inference(scs_inference,[],[2319,2293,2279,2338,2166,998,11,10,7,9,8,12,5,4,2,6,38,26,31,30])). % 106.04/106.06 cnf(2351,plain, % 106.04/106.06 (~E(f6(a8,a8),a9)), % 106.04/106.06 inference(scs_inference,[],[2259,2319,1924,2299,79,2293,2279,2338,2243,2166,998,18,67,11,10,7,9,8,12,5,4,2,6,38,26,31,30,25,24,13,3])). % 106.04/106.06 cnf(2356,plain, % 106.04/106.06 (~P2(a8,f10(a9))), % 106.04/106.06 inference(scs_inference,[],[2259,2319,1924,2078,2292,2299,79,2300,2293,155,2279,2338,2243,2166,998,18,67,11,10,7,9,8,12,5,4,2,6,38,26,31,30,25,24,13,3,15,14,40])). % 106.04/106.06 cnf(2363,plain, % 106.04/106.06 (E(f4(x23631,a1),f4(x23631,f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[236,7,10,11])). % 106.04/106.06 cnf(2364,plain, % 106.04/106.06 (E(f5(x23641,x23642,a1),f5(x23641,x23642,f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[236,7,10,11,9])). % 106.04/106.06 cnf(2370,plain, % 106.04/106.06 (E(f10(a1),f10(f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[2231,236,7,10,11,9,8,12,5,2,4,6])). % 106.04/106.06 cnf(2371,plain, % 106.04/106.06 (E(f5(a1,f10(a1),a1),a1)), % 106.04/106.06 inference(scs_inference,[],[2231,236,1028,7,10,11,9,8,12,5,2,4,6,38])). % 106.04/106.06 cnf(2375,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),f10(a7)),f6(a7,x23751))), % 106.04/106.06 inference(scs_inference,[],[2231,2180,1842,236,1028,7,10,11,9,8,12,5,2,4,6,38,26,31])). % 106.04/106.06 cnf(2376,plain, % 106.04/106.06 (~P2(x23761,f4(f6(a1,a1),f10(a7)))), % 106.04/106.06 inference(rename_variables,[],[1842])). % 106.04/106.06 cnf(2378,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),f10(a7)),f6(x23781,a7))), % 106.04/106.06 inference(scs_inference,[],[2231,2180,1842,2376,236,1028,7,10,11,9,8,12,5,2,4,6,38,26,31,30])). % 106.04/106.06 cnf(2379,plain, % 106.04/106.06 (~P2(x23791,f4(f6(a1,a1),f10(a7)))), % 106.04/106.06 inference(rename_variables,[],[1842])). % 106.04/106.06 cnf(2381,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),f10(a7)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2231,2180,1842,2376,2379,236,1028,7,10,11,9,8,12,5,2,4,6,38,26,31,30,24])). % 106.04/106.06 cnf(2386,plain, % 106.04/106.06 (~E(f5(f10(a7),a9,f10(a1)),f6(a8,x23861))), % 106.04/106.06 inference(scs_inference,[],[19,2231,2337,175,2180,1842,2376,2379,236,968,2204,1028,7,10,11,9,8,12,5,2,4,6,38,26,31,30,24,25,13])). % 106.04/106.06 cnf(2387,plain, % 106.04/106.06 (E(f5(a9,x23871,a9),f5(a1,x23871,a1))), % 106.04/106.06 inference(scs_inference,[],[19,2231,2296,2298,2337,175,2180,1842,2376,2379,236,968,2204,1028,7,10,11,9,8,12,5,2,4,6,38,26,31,30,24,25,13,3])). % 106.04/106.06 cnf(2388,plain, % 106.04/106.06 (E(f5(a9,x23881,x23882),f5(a1,x23881,x23882))), % 106.04/106.06 inference(rename_variables,[],[2296])). % 106.04/106.06 cnf(2393,plain, % 106.04/106.06 (~P2(f10(a9),f10(a9))), % 106.04/106.06 inference(scs_inference,[],[19,2080,2231,2296,2388,2298,2337,161,175,2180,1842,2376,2379,2300,236,968,2204,1028,7,10,11,9,8,12,5,2,4,6,38,26,31,30,24,25,13,3,15,14,40])). % 106.04/106.06 cnf(2395,plain, % 106.04/106.06 (E(f4(a1,a9),f10(x23951))+E(f4(x23951,f4(a1,a9)),x23951)), % 106.04/106.06 inference(scs_inference,[],[19,2080,2231,2296,2388,2298,2337,161,175,2180,1842,2376,2379,2300,236,968,2204,1028,234,7,10,11,9,8,12,5,2,4,6,38,26,31,30,24,25,13,3,15,14,40,29])). % 106.04/106.06 cnf(2398,plain, % 106.04/106.06 (E(f4(a1,a9),f10(x23981))+E(x23981,f4(x23981,f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[2395,2])). % 106.04/106.06 cnf(2399,plain, % 106.04/106.06 (E(f4(f4(a1,a9),x23991),f4(a1,x23991))), % 106.04/106.06 inference(scs_inference,[],[231,10])). % 106.04/106.06 cnf(2400,plain, % 106.04/106.06 (E(f5(f4(a1,a9),x24001,x24002),f5(a1,x24001,x24002))), % 106.04/106.06 inference(scs_inference,[],[231,10,7])). % 106.04/106.06 cnf(2401,plain, % 106.04/106.06 (E(f4(x24011,f4(a1,a9)),f4(x24011,a1))), % 106.04/106.06 inference(scs_inference,[],[231,10,7,11])). % 106.04/106.06 cnf(2402,plain, % 106.04/106.06 (E(f5(x24021,f4(a1,a9),x24022),f5(x24021,a1,x24022))), % 106.04/106.06 inference(scs_inference,[],[231,10,7,11,8])). % 106.04/106.06 cnf(2403,plain, % 106.04/106.06 (E(f5(x24031,x24032,f4(a1,a9)),f5(x24031,x24032,a1))), % 106.04/106.06 inference(scs_inference,[],[231,10,7,11,8,9])). % 106.04/106.06 cnf(2405,plain, % 106.04/106.06 (E(f6(x24051,f4(a1,a9)),f6(x24051,a1))), % 106.04/106.06 inference(scs_inference,[],[231,10,7,11,8,9,12,5])). % 106.04/106.06 cnf(2406,plain, % 106.04/106.06 (~E(f6(a8,x24061),f4(a1,a9))), % 106.04/106.06 inference(scs_inference,[],[2276,231,10,7,11,8,9,12,5,2])). % 106.04/106.06 cnf(2407,plain, % 106.04/106.06 (E(f10(f4(a1,a9)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[2276,231,10,7,11,8,9,12,5,2,6])). % 106.04/106.06 cnf(2408,plain, % 106.04/106.06 (E(f6(f4(a1,a9),x24081),f6(a1,x24081))), % 106.04/106.06 inference(scs_inference,[],[2276,231,10,7,11,8,9,12,5,2,6,4])). % 106.04/106.06 cnf(2409,plain, % 106.04/106.06 (E(f5(f10(a1),a1,a1),a1)), % 106.04/106.06 inference(scs_inference,[],[2276,231,1048,10,7,11,8,9,12,5,2,6,4,38])). % 106.04/106.06 cnf(2411,plain, % 106.04/106.06 (~P2(a7,f5(a7,f4(a1,a1),f10(a7)))), % 106.04/106.06 inference(scs_inference,[],[2276,2192,231,1048,10,7,11,8,9,12,5,2,6,4,38,26])). % 106.04/106.06 cnf(2414,plain, % 106.04/106.06 (~P2(x24141,f3(f10(a1)))), % 106.04/106.06 inference(rename_variables,[],[1788])). % 106.04/106.06 cnf(2420,plain, % 106.04/106.06 (E(x24201,f6(x24201,x24201))), % 106.04/106.06 inference(rename_variables,[],[67])). % 106.04/106.06 cnf(2425,plain, % 106.04/106.06 (~E(f6(a8,a8),a1)), % 106.04/106.06 inference(scs_inference,[],[2331,2356,2276,2258,2247,2192,1788,2414,957,231,1048,67,2420,10,7,11,8,9,12,5,2,6,4,38,26,31,30,24,25,13,3])). % 106.04/106.06 cnf(2427,plain, % 106.04/106.06 (~P2(x24271,f4(a9,f10(a7)))), % 106.04/106.06 inference(scs_inference,[],[2331,2356,2276,2288,2258,2247,2192,1788,2414,957,231,1048,321,67,2420,10,7,11,8,9,12,5,2,6,4,38,26,31,30,24,25,13,3,15])). % 106.04/106.06 cnf(2437,plain, % 106.04/106.06 (E(f5(f4(a1,a1),x24371,x24372),f5(a1,x24371,x24372))), % 106.04/106.06 inference(scs_inference,[],[288,7])). % 106.04/106.06 cnf(2438,plain, % 106.04/106.06 (E(f4(f4(a1,a1),x24381),f4(a1,x24381))), % 106.04/106.06 inference(scs_inference,[],[288,7,10])). % 106.04/106.06 cnf(2439,plain, % 106.04/106.06 (E(f4(x24391,f4(a1,a1)),f4(x24391,a1))), % 106.04/106.06 inference(scs_inference,[],[288,7,10,11])). % 106.04/106.06 cnf(2440,plain, % 106.04/106.06 (E(f5(x24401,x24402,f4(a1,a1)),f5(x24401,x24402,a1))), % 106.04/106.06 inference(scs_inference,[],[288,7,10,11,9])). % 106.04/106.06 cnf(2441,plain, % 106.04/106.06 (E(f5(x24411,f4(a1,a1),x24412),f5(x24411,a1,x24412))), % 106.04/106.06 inference(scs_inference,[],[288,7,10,11,9,8])). % 106.04/106.06 cnf(2443,plain, % 106.04/106.06 (E(f6(x24431,f4(a1,a1)),f6(x24431,a1))), % 106.04/106.06 inference(scs_inference,[],[288,7,10,11,9,8,12,5])). % 106.04/106.06 cnf(2444,plain, % 106.04/106.06 (~E(f6(x24441,a8),f4(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[2318,288,7,10,11,9,8,12,5,2])). % 106.04/106.06 cnf(2445,plain, % 106.04/106.06 (E(f6(f4(a1,a1),x24451),f6(a1,x24451))), % 106.04/106.06 inference(scs_inference,[],[2318,288,7,10,11,9,8,12,5,2,4])). % 106.04/106.06 cnf(2447,plain, % 106.04/106.06 (E(f5(a1,a1,f10(a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[2318,288,1954,7,10,11,9,8,12,5,2,4,6,38])). % 106.04/106.06 cnf(2452,plain, % 106.04/106.06 (~P2(x24521,f4(a9,f10(a7)))), % 106.04/106.06 inference(rename_variables,[],[2427])). % 106.04/106.06 cnf(2455,plain, % 106.04/106.06 (~P2(x24551,f4(a9,f10(a7)))), % 106.04/106.06 inference(rename_variables,[],[2427])). % 106.04/106.06 cnf(2457,plain, % 106.04/106.06 (~E(f4(a9,f10(a7)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2318,2427,2452,2455,1675,288,2152,1954,7,10,11,9,8,12,5,2,4,6,38,26,30,31,24])). % 106.04/106.06 cnf(2462,plain, % 106.04/106.06 (~E(f4(a1,f10(a7)),f6(x24621,a8))), % 106.04/106.06 inference(scs_inference,[],[19,2318,324,2427,2452,2455,1675,551,288,2152,151,2206,1954,7,10,11,9,8,12,5,2,4,6,38,26,30,31,24,25,13])). % 106.04/106.06 cnf(2463,plain, % 106.04/106.06 (~E(f4(a1,a1),f6(x24631,a7))), % 106.04/106.06 inference(scs_inference,[],[19,2214,2318,2289,324,2427,2452,2455,1675,551,288,2152,151,2206,1954,7,10,11,9,8,12,5,2,4,6,38,26,30,31,24,25,13,3])). % 106.04/106.06 cnf(2471,plain, % 106.04/106.06 (E(f4(f6(x24711,x24711),x24712),f4(x24711,x24712))), % 106.04/106.06 inference(scs_inference,[],[18,10])). % 106.04/106.06 cnf(2472,plain, % 106.04/106.06 (E(f5(f6(x24721,x24721),x24722,x24723),f5(x24721,x24722,x24723))), % 106.04/106.06 inference(scs_inference,[],[18,10,7])). % 106.04/106.06 cnf(2473,plain, % 106.04/106.06 (E(f4(x24731,f6(x24732,x24732)),f4(x24731,x24732))), % 106.04/106.06 inference(scs_inference,[],[18,10,7,11])). % 106.04/106.06 cnf(2474,plain, % 106.04/106.06 (E(f5(x24741,f6(x24742,x24742),x24743),f5(x24741,x24742,x24743))), % 106.04/106.06 inference(scs_inference,[],[18,10,7,11,8])). % 106.04/106.06 cnf(2475,plain, % 106.04/106.06 (E(f5(x24751,x24752,f6(x24753,x24753)),f5(x24751,x24752,x24753))), % 106.04/106.06 inference(scs_inference,[],[18,10,7,11,8,9])). % 106.04/106.06 cnf(2477,plain, % 106.04/106.06 (E(f6(x24771,f6(x24772,x24772)),f6(x24771,x24772))), % 106.04/106.06 inference(scs_inference,[],[18,10,7,11,8,9,12,5])). % 106.04/106.06 cnf(2478,plain, % 106.04/106.06 (~E(a1,f6(a8,a8))), % 106.04/106.06 inference(scs_inference,[],[2425,18,10,7,11,8,9,12,5,2])). % 106.04/106.06 cnf(2479,plain, % 106.04/106.06 (E(f10(f6(x24791,x24791)),f10(x24791))), % 106.04/106.06 inference(scs_inference,[],[2425,18,10,7,11,8,9,12,5,2,6])). % 106.04/106.06 cnf(2480,plain, % 106.04/106.06 (E(f6(f6(x24801,x24801),x24802),f6(x24801,x24802))), % 106.04/106.06 inference(scs_inference,[],[2425,18,10,7,11,8,9,12,5,2,6,4])). % 106.04/106.06 cnf(2481,plain, % 106.04/106.06 (E(f5(f10(a1),f10(a1),f10(a7)),a1)), % 106.04/106.06 inference(scs_inference,[],[2425,1714,18,10,7,11,8,9,12,5,2,6,4,38])). % 106.04/106.06 cnf(2486,plain, % 106.04/106.06 (~P2(x24861,f6(a1,a9))), % 106.04/106.06 inference(rename_variables,[],[1244])). % 106.04/106.06 cnf(2499,plain, % 106.04/106.06 (~P2(x24991,f6(a9,f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[1269,2393,2302,2301,2425,2286,2199,963,1782,596,2109,2300,1714,1244,2486,18,10,7,11,8,9,12,5,2,6,4,38,26,31,30,24,25,13,3,15])). % 106.04/106.06 cnf(2506,plain, % 106.04/106.06 (E(f5(x25061,x25062,x25063),f5(f6(x25061,x25061),x25062,x25063))), % 106.04/106.06 inference(scs_inference,[],[67,7])). % 106.04/106.06 cnf(2507,plain, % 106.04/106.06 (E(f4(x25071,x25072),f4(f6(x25071,x25071),x25072))), % 106.04/106.06 inference(scs_inference,[],[67,7,10])). % 106.04/106.06 cnf(2508,plain, % 106.04/106.06 (E(f4(x25081,x25082),f4(x25081,f6(x25082,x25082)))), % 106.04/106.06 inference(scs_inference,[],[67,7,10,11])). % 106.04/106.06 cnf(2509,plain, % 106.04/106.06 (E(f5(x25091,x25092,x25093),f5(x25091,x25092,f6(x25093,x25093)))), % 106.04/106.06 inference(scs_inference,[],[67,7,10,11,9])). % 106.04/106.06 cnf(2511,plain, % 106.04/106.06 (E(f6(x25111,x25112),f6(x25111,f6(x25112,x25112)))), % 106.04/106.06 inference(scs_inference,[],[67,7,10,11,9,8,5])). % 106.04/106.06 cnf(2513,plain, % 106.04/106.06 (~E(a7,f6(a9,a9))), % 106.04/106.06 inference(scs_inference,[],[2277,67,7,10,11,9,8,5,12,2])). % 106.04/106.06 cnf(2514,plain, % 106.04/106.06 (E(f6(x25141,x25142),f6(f6(x25141,x25141),x25142))), % 106.04/106.06 inference(scs_inference,[],[2277,67,7,10,11,9,8,5,12,2,4])). % 106.04/106.06 cnf(2515,plain, % 106.04/106.06 (E(f10(x25151),f10(f6(x25151,x25151)))), % 106.04/106.06 inference(scs_inference,[],[2277,67,7,10,11,9,8,5,12,2,4,6])). % 106.04/106.06 cnf(2521,plain, % 106.04/106.06 (~P2(x25211,f6(a9,f4(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[2499])). % 106.04/106.06 cnf(2524,plain, % 106.04/106.06 (~P2(x25241,f6(a9,f4(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[2499])). % 106.04/106.06 cnf(2526,plain, % 106.04/106.06 (~E(f6(a9,f4(a1,a9)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2277,2499,2521,2524,1844,2124,573,67,7,10,11,9,8,5,12,2,4,6,38,26,30,31,24])). % 106.04/106.06 cnf(2535,plain, % 106.04/106.06 (~P2(f4(f6(a7,a7),f6(a1,a9)),f5(a1,a7,a1))), % 106.04/106.06 inference(scs_inference,[],[19,2297,1939,2277,2479,2471,2285,2340,1865,2198,2499,2521,2524,1844,2124,968,21,573,67,7,10,11,9,8,5,12,2,4,6,38,26,30,31,24,25,13,3,15,14])). % 106.04/106.06 cnf(2537,plain, % 106.04/106.06 (E(f4(a1,a1),f10(x25371))+E(f4(x25371,f4(a1,a1)),x25371)), % 106.04/106.06 inference(scs_inference,[],[19,2297,1939,2277,2479,2471,2285,2340,1865,2198,2499,2521,2524,1844,2124,968,21,573,291,67,7,10,11,9,8,5,12,2,4,6,38,26,30,31,24,25,13,3,15,14,29])). % 106.04/106.06 cnf(2540,plain, % 106.04/106.06 (E(f4(a1,a1),f10(x25401))+E(x25401,f4(x25401,f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[2537,2])). % 106.04/106.06 cnf(2541,plain, % 106.04/106.06 (~E(a9,f6(a8,a8))), % 106.04/106.06 inference(scs_inference,[],[2351,2])). % 106.04/106.06 cnf(2542,plain, % 106.04/106.06 (E(f5(f10(a1),f4(a1,a9),f6(a1,a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[2351,687,2,38])). % 106.04/106.06 cnf(2547,plain, % 106.04/106.06 (~P2(x25471,a9)), % 106.04/106.06 inference(rename_variables,[],[50])). % 106.04/106.06 cnf(2556,plain, % 106.04/106.06 (~P2(f6(a8,x25561),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[2406,2351,2480,2020,2370,2186,2138,687,50,2547,2,38,26,31,30,24,25])). % 106.04/106.06 cnf(2558,plain, % 106.04/106.06 (~E(f3(f10(a1)),f6(a8,a8))), % 106.04/106.06 inference(scs_inference,[],[2406,2478,2351,2480,2020,2370,1790,2186,2138,687,50,2547,2,38,26,31,30,24,25,3])). % 106.04/106.06 cnf(2560,plain, % 106.04/106.06 (~P2(f4(f6(a7,a7),f6(a1,a9)),f5(a9,a7,a9))), % 106.04/106.06 inference(scs_inference,[],[2406,2387,2478,2351,2480,2020,2535,2290,2370,1790,17,2186,2138,687,50,2547,2,38,26,31,30,24,25,3,13,15])). % 106.04/106.06 cnf(2568,plain, % 106.04/106.06 (E(f5(f10(a1),f4(a1,a1),f6(a1,a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[2085,708,2,38])). % 106.04/106.06 cnf(2572,plain, % 106.04/106.06 (~E(f6(f4(a1,a1),f6(a1,a1)),f6(a7,x25721))), % 106.04/106.06 inference(scs_inference,[],[2085,797,1594,2130,708,2,38,26,31])). % 106.04/106.06 cnf(2573,plain, % 106.04/106.06 (~P2(x25731,f6(f4(a1,a1),f6(a1,a1)))), % 106.04/106.06 inference(rename_variables,[],[797])). % 106.04/106.06 cnf(2576,plain, % 106.04/106.06 (~P2(x25761,f6(f4(a1,a1),f6(a1,a1)))), % 106.04/106.06 inference(rename_variables,[],[797])). % 106.04/106.06 cnf(2585,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),a1),f6(a8,x25851))), % 106.04/106.06 inference(scs_inference,[],[19,2085,2473,2399,2558,1910,797,2573,2576,1594,2130,2204,708,199,2,38,26,31,30,24,25,3,13])). % 106.04/106.06 cnf(2587,plain, % 106.04/106.06 (~P2(f4(a7,f6(a1,a9)),f5(a9,a7,a9))), % 106.04/106.06 inference(scs_inference,[],[19,2556,2085,2473,2407,2399,2558,2560,2507,1910,797,2573,2576,1594,2130,2204,708,199,2,38,26,31,30,24,25,3,13,15,14])). % 106.04/106.06 cnf(2593,plain, % 106.04/106.06 (E(f4(f6(a1,a1),f4(a1,a9)),f6(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[19,2556,2085,2473,2407,2399,2558,2560,2507,2511,1910,797,2573,2576,242,1594,2130,2204,708,199,2,38,26,31,30,24,25,3,13,15,14,32,2395])). % 106.04/106.06 cnf(2595,plain, % 106.04/106.06 (E(f6(a1,a1),f4(f6(a1,a1),f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[19,2556,2085,2473,2407,2399,2558,2560,2507,2511,1910,797,2573,2576,242,1594,2130,2204,708,199,2,38,26,31,30,24,25,3,13,15,14,32,2395,2398])). % 106.04/106.06 cnf(2598,plain, % 106.04/106.06 (E(f5(f4(a1,a9),f10(a1),a1),a1)), % 106.04/106.06 inference(scs_inference,[],[2107,249,2,38])). % 106.04/106.06 cnf(2603,plain, % 106.04/106.06 (~P2(x26031,f4(a1,a1))), % 106.04/106.06 inference(rename_variables,[],[291])). % 106.04/106.06 cnf(2616,plain, % 106.04/106.06 (~P2(x26161,f4(f6(a1,a1),f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[2444,2463,2107,2593,2245,2587,2508,2213,77,2243,2174,2132,249,291,2603,54,2,38,26,31,30,24,25,3,13,15])). % 106.04/106.06 cnf(2622,plain, % 106.04/106.06 (E(f4(f6(a1,a1),f4(a1,a1)),f6(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[2444,2463,2107,2593,2245,2587,2508,2213,2335,77,2243,2174,2132,249,1244,291,2603,54,18,2,38,26,31,30,24,25,3,13,15,14,32,2537])). % 106.04/106.06 cnf(2636,plain, % 106.04/106.06 (~P2(x26361,f4(f6(a1,a1),f4(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[2616])). % 106.04/106.06 cnf(2639,plain, % 106.04/106.06 (~P2(x26391,f4(f6(a1,a1),f4(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[2616])). % 106.04/106.06 cnf(2641,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),f4(a1,a9)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,638,2616,2636,2639,1602,2092,305,2,38,26,31,30,24])). % 106.04/106.06 cnf(2644,plain, % 106.04/106.06 (E(f5(f6(x26441,x26441),f6(x26442,x26442),x26443),f5(x26441,x26442,x26443))), % 106.04/106.06 inference(scs_inference,[],[19,2472,2474,638,2616,2636,2639,1602,2092,305,2,38,26,31,30,24,3])). % 106.04/106.06 cnf(2646,plain, % 106.04/106.06 (~E(f4(a1,f6(a1,a1)),f6(x26461,a8))), % 106.04/106.06 inference(scs_inference,[],[19,2472,2474,638,2616,2636,2639,192,1602,2092,2206,305,2,38,26,31,30,24,3,13])). % 106.04/106.06 cnf(2653,plain, % 106.04/106.06 (E(f5(f10(a1),f10(a1),a1),a1)), % 106.04/106.06 inference(scs_inference,[],[196,38])). % 106.04/106.06 cnf(2657,plain, % 106.04/106.06 (~P2(x26571,a9)), % 106.04/106.06 inference(rename_variables,[],[50])). % 106.04/106.06 cnf(2662,plain, % 106.04/106.06 (~E(f6(f10(a7),f10(a7)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[541,2270,2176,196,2253,50,2657,38,2,31,30,24])). % 106.04/106.06 cnf(2664,plain, % 106.04/106.06 (~P2(a9,f10(a8))), % 106.04/106.06 inference(scs_inference,[],[2541,541,2515,2270,2176,196,2253,50,2657,38,2,31,30,24,25])). % 106.04/106.06 cnf(2667,plain, % 106.04/106.06 (~E(f6(a7,a7),f6(a9,a9))), % 106.04/106.06 inference(scs_inference,[],[2513,2541,541,2515,2270,2176,196,2253,50,2657,67,38,2,31,30,24,25,3])). % 106.04/106.06 cnf(2670,plain, % 106.04/106.06 (~P2(x26701,f4(f6(a1,a1),f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[2513,2541,2622,541,2515,2270,237,2247,2176,196,2253,50,2657,54,67,38,2,31,30,24,25,3,13,15])). % 106.04/106.06 cnf(2676,plain, % 106.04/106.06 (E(f5(f4(a1,a1),f10(a1),f6(a1,a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[401,38])). % 106.04/106.06 cnf(2678,plain, % 106.04/106.06 (~E(f6(a9,a9),f6(a7,a7))), % 106.04/106.06 inference(scs_inference,[],[2667,401,38,2])). % 106.04/106.06 cnf(2680,plain, % 106.04/106.06 (~P2(x26801,f4(f6(a1,a1),f4(a1,a1)))), % 106.04/106.06 inference(rename_variables,[],[2670])). % 106.04/106.06 cnf(2683,plain, % 106.04/106.06 (~P2(x26831,f4(f6(a1,a1),f4(a1,a1)))), % 106.04/106.06 inference(rename_variables,[],[2670])). % 106.04/106.06 cnf(2685,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),f4(a1,a1)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2667,2670,2680,2683,617,401,38,2,31,30,24])). % 106.04/106.06 cnf(2688,plain, % 106.04/106.06 (E(f5(f6(x26881,x26881),f6(x26882,x26882),f6(x26883,x26883)),f5(x26881,x26882,x26883))), % 106.04/106.06 inference(scs_inference,[],[19,2667,2644,2475,2670,2680,2683,617,401,38,2,31,30,24,3])). % 106.04/106.06 cnf(2690,plain, % 106.04/106.06 (~E(f3(f10(a1)),a8)), % 106.04/106.06 inference(scs_inference,[],[19,2667,2644,2475,2670,2680,2683,1793,617,21,401,38,2,31,30,24,3,13])). % 106.04/106.06 cnf(2691,plain, % 106.04/106.06 (~P2(a9,f10(f6(a8,a8)))), % 106.04/106.06 inference(scs_inference,[],[19,2667,2664,2644,2475,2670,2680,2683,1793,2479,617,21,401,38,2,31,30,24,3,13,15])). % 106.04/106.06 cnf(2693,plain, % 106.04/106.06 (~P2(f10(a9),f10(f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[19,2667,2664,2644,2475,276,2670,2680,2683,1793,2479,617,2300,21,401,38,2,31,30,24,3,13,15,14])). % 106.04/106.06 cnf(2698,plain, % 106.04/106.06 (E(f5(f10(a7),f10(a7),f10(a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[441,38])). % 106.04/106.06 cnf(2703,plain, % 106.04/106.06 (~E(f6(f6(a9,a9),a9),f6(a7,a7))), % 106.04/106.06 inference(scs_inference,[],[2678,858,2514,2691,441,2253,38,2,24,3])). % 106.04/106.06 cnf(2706,plain, % 106.04/106.06 (~P2(f10(a1),f5(f4(a1,a9),f10(a1),f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[2678,858,2403,506,2514,2691,294,2286,441,2253,38,2,24,3,13,15])). % 106.04/106.06 cnf(2712,plain, % 106.04/106.06 (~E(f6(f6(x27121,a7),x27122),f6(a9,a9))), % 106.04/106.06 inference(scs_inference,[],[2678,858,2403,506,2514,2411,2691,294,2286,1871,1533,441,2253,50,18,38,2,24,3,13,15,14,25,32])). % 106.04/106.06 cnf(2716,plain, % 106.04/106.06 (E(f5(f10(a1),f10(a1),f6(a1,a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[134,38])). % 106.04/106.06 cnf(2720,plain, % 106.04/106.06 (~P2(x27201,f4(a1,a9))), % 106.04/106.06 inference(rename_variables,[],[234])). % 106.04/106.06 cnf(2731,plain, % 106.04/106.06 (E(f5(f4(a1,a9),x27311,f4(a1,a1)),f5(a1,x27311,a1))), % 106.04/106.06 inference(scs_inference,[],[19,872,2712,2400,2440,567,2515,1551,134,234,2720,38,2,31,30,24,25,3])). % 106.04/106.06 cnf(2734,plain, % 106.04/106.06 (~E(f6(f10(a7),f10(a7)),f6(a8,x27341))), % 106.04/106.06 inference(scs_inference,[],[19,872,2712,2400,2440,1777,567,2515,1551,2204,134,234,2720,38,2,31,30,24,25,3,13])). % 106.04/106.06 cnf(2735,plain, % 106.04/106.06 (~P2(f10(a9),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,872,2712,2400,2440,2693,1777,567,2515,2370,1551,2204,134,234,2720,38,2,31,30,24,25,3,13,15])). % 106.04/106.06 cnf(2737,plain, % 106.04/106.06 (~E(f6(a7,x27371),f6(a9,a9))), % 106.04/106.06 inference(scs_inference,[],[19,872,2712,2400,2440,2706,2693,1777,567,2515,2370,1551,2300,2204,134,50,234,2720,38,2,31,30,24,25,3,13,15,14,32])). % 106.04/106.06 cnf(2740,plain, % 106.04/106.06 (~E(f6(a9,a9),f6(a7,x27401))), % 106.04/106.06 inference(scs_inference,[],[2737,2])). % 106.04/106.06 cnf(2742,plain, % 106.04/106.06 (~P2(x27421,f6(f4(a1,a1),f4(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[392])). % 106.04/106.06 cnf(2754,plain, % 106.04/106.06 (~P2(f10(f6(a9,a9)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[2737,2735,1660,2249,2506,521,1098,392,2742,79,2290,2479,1851,2253,2,31,30,24,3,13,15,14])). % 106.04/106.06 cnf(2762,plain, % 106.04/106.06 (~E(f6(f4(a1,a1),f4(a1,a1)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,886,299,2,24])). % 106.04/106.06 cnf(2767,plain, % 106.04/106.06 (E(f5(f4(a1,a1),f6(a1,a9),x27671),f5(a1,a1,x27671))), % 106.04/106.06 inference(scs_inference,[],[19,886,2437,2251,2386,299,88,2,24,25,3])). % 106.04/106.06 cnf(2770,plain, % 106.04/106.06 (~E(f5(f10(a7),a9,f10(a1)),f6(x27701,a8))), % 106.04/106.06 inference(scs_inference,[],[19,886,2437,2251,2386,299,175,2206,88,2,24,25,3,13])). % 106.04/106.06 cnf(2778,plain, % 106.04/106.06 (~E(f6(a9,a1),f6(a7,x27781))), % 106.04/106.06 inference(scs_inference,[],[2740,901,1162,2299,2253,2,24,3])). % 106.04/106.06 cnf(2781,plain, % 106.04/106.06 (~P2(f10(a1),f5(f10(a1),f4(a1,a1),f10(a7)))), % 106.04/106.06 inference(scs_inference,[],[2740,901,2326,825,1162,2299,957,2243,2253,2,24,3,13,15])). % 106.04/106.06 cnf(2788,plain, % 106.04/106.06 (~E(f6(a7,x27881),f6(a9,a1))), % 106.04/106.06 inference(scs_inference,[],[2778,2])). % 106.04/106.06 cnf(2792,plain, % 106.04/106.06 (~P2(f4(a1,f10(a7)),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[19,2778,2462,59,2515,2,24,25])). % 106.04/106.06 cnf(2799,plain, % 106.04/106.06 (~P2(f10(a1),f5(f10(a1),a1,f10(a7)))), % 106.04/106.06 inference(scs_inference,[],[19,2778,2441,2462,1647,2781,2202,59,324,2515,21,2,24,25,3,13,15])). % 106.04/106.06 cnf(2803,plain, % 106.04/106.06 (~E(f6(x28031,f6(x28032,a7)),f6(a9,a9))), % 106.04/106.06 inference(scs_inference,[],[19,2778,2441,2462,1647,2781,2202,180,59,2301,324,1875,2515,21,50,2,24,25,3,13,15,14,32])). % 106.04/106.06 cnf(2824,plain, % 106.04/106.06 (~P2(a9,f6(f10(a8),f10(a8)))), % 106.04/106.06 inference(scs_inference,[],[1453,2313,2402,2438,2323,2792,2799,2480,2664,1782,2247,2,24,3,13,15,14,41])). % 106.04/106.06 cnf(2828,plain, % 106.04/106.06 (~E(f6(x28281,f6(a7,x28282)),f6(a9,a9))), % 106.04/106.06 inference(scs_inference,[],[1453,2313,2402,2438,2323,2792,2799,2480,2664,1782,1855,1423,2247,50,2,24,3,13,15,14,41,25,32])). % 106.04/106.06 cnf(2833,plain, % 106.04/106.06 (~E(f6(f4(a1,a9),f10(a7)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,1611,741,2,24])). % 106.04/106.06 cnf(2840,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),f10(a7)),f6(a8,x28401))), % 106.04/106.06 inference(scs_inference,[],[19,1611,2325,1391,2770,741,1865,2204,88,2,24,25,3,13])). % 106.04/106.06 cnf(2847,plain, % 106.04/106.06 (~E(f6(f6(a9,a9),f6(a9,a9)),f6(a7,a7))), % 106.04/106.06 inference(scs_inference,[],[2164,2703,2824,2511,2253,2,24,3])). % 106.04/106.06 cnf(2854,plain, % 106.04/106.06 (~P2(f6(a9,a9),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[2164,2703,2731,2824,1080,2511,17,2286,2253,18,2,24,3,13,15,14,40])). % 106.04/106.06 cnf(2863,plain, % 106.04/106.06 (~E(f10(a1),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[19,2847,2690,768,199,2,24,25])). % 106.04/106.06 cnf(2870,plain, % 106.04/106.06 (~P2(f6(a9,f6(a9,a9)),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[19,2854,2847,2327,863,2690,768,1910,2477,2479,2206,199,2,24,25,3,13,15,14])). % 106.04/106.06 cnf(2886,plain, % 106.04/106.06 (~P2(x28861,f4(f6(a1,a9),f6(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[2863,2408,2246,1958,2213,77,2290,176,2,24,3,13,15])). % 106.04/106.06 cnf(2890,plain, % 106.04/106.06 (~E(f6(f6(a7,x28901),x28902),f6(a9,a9))), % 106.04/106.06 inference(scs_inference,[],[2863,2408,2246,2870,1958,2213,1857,77,2480,2290,176,50,2,24,3,13,15,14,32])). % 106.04/106.06 cnf(2903,plain, % 106.04/106.06 (~E(f4(f6(a1,a9),f6(a1,a1)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2803,2886,1604,291,234,2,31,30,24])). % 106.04/106.06 cnf(2909,plain, % 106.04/106.06 (E(f4(f10(a7),f4(a1,a9)),f4(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[19,2803,2401,2324,2886,1604,2515,291,234,2,31,30,24,25,3])). % 106.04/106.06 cnf(2922,plain, % 106.04/106.06 (~P2(x29221,f6(f4(a1,a9),a1))), % 106.04/106.06 inference(rename_variables,[],[681])). % 106.04/106.06 cnf(2930,plain, % 106.04/106.06 (~E(f6(f4(a1,a1),a1),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[2828,2762,2443,2754,681,2922,1844,2479,2,31,30,24,3])). % 106.04/106.06 cnf(2933,plain, % 106.04/106.06 (~P2(x29331,f4(f10(a7),f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[2828,2762,2909,2443,2754,681,2922,237,2243,1844,2479,291,2,31,30,24,3,13,15])). % 106.04/106.06 cnf(2941,plain, % 106.04/106.06 (~P2(x29411,f10(a7))), % 106.04/106.06 inference(rename_variables,[],[52])). % 106.04/106.06 cnf(2946,plain, % 106.04/106.06 (~E(f4(f10(a7),f4(a1,a9)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2890,2933,1667,52,2941,2,31,30,24])). % 106.04/106.06 cnf(2947,plain, % 106.04/106.06 (~P2(x29471,f4(f10(a7),f4(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[2933])). % 106.04/106.06 cnf(2955,plain, % 106.04/106.06 (~P2(x29551,f4(f10(a7),a1))), % 106.04/106.06 inference(scs_inference,[],[19,2890,1582,2933,2947,2201,2363,1793,1667,2515,2204,52,2941,2,31,30,24,25,3,13,15])). % 106.04/106.06 cnf(2963,plain, % 106.04/106.06 (~P2(x29631,f4(f10(a7),a1))), % 106.04/106.06 inference(rename_variables,[],[2955])). % 106.04/106.06 cnf(2966,plain, % 106.04/106.06 (~P2(x29661,f4(f10(a7),a1))), % 106.04/106.06 inference(rename_variables,[],[2955])). % 106.04/106.06 cnf(2968,plain, % 106.04/106.06 (~E(f4(f10(a7),a1),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,1911,2955,2963,2966,2109,2,31,30,24])). % 106.04/106.06 cnf(2969,plain, % 106.04/106.06 (~P2(x29691,f4(f10(a7),a1))), % 106.04/106.06 inference(rename_variables,[],[2955])). % 106.04/106.06 cnf(2971,plain, % 106.04/106.06 (~E(f6(f4(a1,a9),a1),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,1911,2833,2329,2955,2963,2966,2109,2,31,30,24,3])). % 106.04/106.06 cnf(2974,plain, % 106.04/106.06 (~P2(x29741,f4(f10(a7),f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[19,1911,2833,2439,2329,2955,2963,2966,2969,294,2247,2109,2,31,30,24,3,13,15])). % 106.04/106.06 cnf(2985,plain, % 106.04/106.06 (~E(f4(f10(a7),f4(a1,a1)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2685,2974,627,234,2,31,24])). % 106.04/106.06 cnf(3003,plain, % 106.04/106.06 (~P2(x30031,f6(f4(a1,a1),a1))), % 106.04/106.06 inference(rename_variables,[],[702])). % 106.04/106.06 cnf(3011,plain, % 106.04/106.06 (~P2(x30111,f6(f4(a1,a1),f6(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[2457,1653,2256,2509,1859,702,3003,79,2286,2152,67,2,31,24,3,13,15])). % 106.04/106.06 cnf(3014,plain, % 106.04/106.06 (P2(f5(f10(a7),a9,f6(a9,a7)),a7)), % 106.04/106.06 inference(scs_inference,[],[2457,1653,2256,2509,446,1859,702,3003,671,79,2286,2152,2300,50,67,2,31,24,3,13,15,14,41])). % 106.04/106.06 cnf(3028,plain, % 106.04/106.06 (~P2(x30281,f6(f4(a1,a1),f6(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[3011])). % 106.04/106.06 cnf(3031,plain, % 106.04/106.06 (~P2(x30311,f6(f4(a1,a1),f6(a1,a9)))), % 106.04/106.06 inference(rename_variables,[],[3011])). % 106.04/106.06 cnf(3033,plain, % 106.04/106.06 (~E(f6(f4(a1,a1),f6(a1,a9)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2985,3011,3028,3031,3014,2,31,30,24])). % 106.04/106.06 cnf(3036,plain, % 106.04/106.06 (~P2(f4(f6(a1,a1),a1),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[19,2985,2585,3011,3028,3031,3014,2515,2,31,30,24,25])). % 106.04/106.06 cnf(3042,plain, % 106.04/106.06 (~E(f6(f10(a7),a9),a8)), % 106.04/106.06 inference(scs_inference,[],[19,2985,2585,2767,2447,3011,3028,3031,3014,73,2515,21,2,31,30,24,25,3,13])). % 106.04/106.06 cnf(3050,plain, % 106.04/106.06 (~P2(x30501,f6(f4(a1,a9),a9))), % 106.04/106.06 inference(rename_variables,[],[807])). % 106.04/106.06 cnf(3061,plain, % 106.04/106.06 (~P2(x30611,f6(f6(a1,a9),f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[1588,2307,2257,1751,807,3050,991,2405,3014,953,2290,67,2,31,30,24,3,13,15])). % 106.04/106.06 cnf(3063,plain, % 106.04/106.06 (~P2(a1,f10(a8))), % 106.04/106.06 inference(scs_inference,[],[1588,2307,2257,3036,1912,1751,807,3050,991,2405,3014,953,2290,67,2,31,30,24,3,13,15,14])). % 106.04/106.06 cnf(3073,plain, % 106.04/106.06 (~E(f6(f6(a1,a9),f4(a1,a1)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,3063,2032,3061,112,2,31,30,24])). % 106.04/106.06 cnf(3081,plain, % 106.04/106.06 (~P2(f6(f10(a7),a9),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[19,3063,2032,3061,2364,175,112,2479,21,2,31,30,24,3,13,15,14])). % 106.04/106.06 cnf(3082,plain, % 106.04/106.06 (~E(f10(a1),f6(f10(a8),f10(a8)))), % 106.04/106.06 inference(scs_inference,[],[19,3063,2032,3061,2364,175,112,2479,21,2,31,30,24,3,13,15,14,32])). % 106.04/106.06 cnf(3101,plain, % 106.04/106.06 (~P2(x31011,f6(f4(a1,a1),a9))), % 106.04/106.06 inference(rename_variables,[],[817])). % 106.04/106.06 cnf(3108,plain, % 106.04/106.06 (E(f6(f10(a7),x31081),f6(a1,x31081))), % 106.04/106.06 inference(rename_variables,[],[2330])). % 106.04/106.06 cnf(3110,plain, % 106.04/106.06 (~P2(f4(a1,f6(a1,a1)),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[2219,2646,2330,1775,817,3101,2124,2515,2,31,30,24,25])). % 106.04/106.06 cnf(3117,plain, % 106.04/106.06 (~P2(x31171,f6(f10(a7),f6(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[2219,2375,2646,2330,3108,1775,817,3101,1042,2471,1782,2124,2243,2515,2,31,30,24,25,3,13,15])). % 106.04/106.06 cnf(3119,plain, % 106.04/106.06 (~P2(f6(a1,a1),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[2219,2375,2646,2330,3108,3081,1775,817,3101,1042,2471,2116,1782,2124,2243,2515,2,31,30,24,25,3,13,15,14])). % 106.04/106.06 cnf(3123,plain, % 106.04/106.06 (P2(f5(a1,f6(a9,a7),f6(a1,a1)),a7)), % 106.04/106.06 inference(scs_inference,[],[2219,2375,2646,2330,3108,3081,1775,817,3101,1042,2471,2116,1782,1533,2124,2243,2515,74,1244,50,2,31,30,24,25,3,13,15,14,32,41])). % 106.04/106.06 cnf(3131,plain, % 106.04/106.06 (~P2(x31311,f6(f10(a7),f6(a1,a1)))), % 106.04/106.06 inference(rename_variables,[],[3117])). % 106.04/106.06 cnf(3134,plain, % 106.04/106.06 (~P2(x31341,f6(f10(a7),f6(a1,a1)))), % 106.04/106.06 inference(rename_variables,[],[3117])). % 106.04/106.06 cnf(3136,plain, % 106.04/106.06 (~E(f6(f10(a7),f6(a1,a1)),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[19,2222,3117,3131,3134,3123,26,2,31,30,24])). % 106.04/106.06 cnf(3139,plain, % 106.04/106.06 (~E(f4(a1,a9),a7)), % 106.04/106.06 inference(scs_inference,[],[19,2222,438,3117,3131,3134,3123,246,26,2,31,30,24,3])). % 106.04/106.06 cnf(3143,plain, % 106.04/106.06 (~P2(f4(a9,f6(a1,a1)),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[19,3119,2222,3110,438,3117,3131,3134,3123,246,2288,324,2479,2204,26,2,31,30,24,3,13,15,14])). % 106.04/106.06 cnf(3152,plain, % 106.04/106.06 (~P2(x31521,f6(a1,f10(a7)))), % 106.04/106.06 inference(rename_variables,[],[1016])). % 106.04/106.06 cnf(3163,plain, % 106.04/106.06 (~E(f4(a1,a1),a7)), % 106.04/106.06 inference(scs_inference,[],[3139,2310,3143,1016,3152,2289,2473,2138,2479,2,31,30,24,25,3])). % 106.04/106.06 cnf(3166,plain, % 106.04/106.06 (~P2(x31661,f5(f10(a1),f4(a1,a9),a1))), % 106.04/106.06 inference(scs_inference,[],[3139,2310,3143,2260,1016,3152,2289,2473,17,2138,2247,2479,37,2,31,30,24,25,3,13,15])). % 106.04/106.06 cnf(3170,plain, % 106.04/106.06 (~E(f5(f10(a1),f4(a1,a9),a1),f10(x31701))), % 106.04/106.06 inference(scs_inference,[],[2378,3166,18,2,24])). % 106.04/106.06 cnf(3171,plain, % 106.04/106.06 (~P2(x31711,f5(f10(a1),f4(a1,a9),a1))), % 106.04/106.06 inference(rename_variables,[],[3166])). % 106.04/106.06 cnf(3173,plain, % 106.04/106.06 (~E(f6(a1,a1),a8)), % 106.04/106.06 inference(scs_inference,[],[2117,2378,3166,3042,18,2,24,3])). % 106.04/106.06 cnf(3175,plain, % 106.04/106.06 (~P2(x31751,f5(f10(a1),f4(a1,a9),a9))), % 106.04/106.06 inference(scs_inference,[],[2117,2378,3166,3171,3042,2298,1865,2206,18,2,24,3,13,15])). % 106.04/106.06 cnf(3177,plain, % 106.04/106.06 (~E(f6(f6(x31771,a7),x31772),f6(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[2117,2378,3166,3171,3042,2298,1865,1871,2206,18,37,2,24,3,13,15,32])). % 106.04/106.06 cnf(3187,plain, % 106.04/106.06 (~P2(f4(f6(a1,a1),f4(a1,a9)),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[2117,2378,3166,3171,3042,1264,2298,2401,3036,1865,1871,1387,2166,2206,18,37,2,24,3,13,15,32,22,30,25,14])). % 106.04/106.06 cnf(3201,plain, % 106.04/106.06 (~E(a8,f6(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[3173,2])). % 106.04/106.06 cnf(3210,plain, % 106.04/106.06 (~P2(x32101,f5(f10(a1),a1,f6(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[3163,3173,3187,2333,2200,2593,957,2286,2479,37,2,24,25,3,13,15])). % 106.04/106.06 cnf(3217,plain, % 106.04/106.06 (~E(f5(f10(a1),a1,f6(a1,a1)),f10(x32171))), % 106.04/106.06 inference(scs_inference,[],[3170,3210,18,2,24])). % 106.04/106.06 cnf(3239,plain, % 106.04/106.06 (~E(f6(a8,a8),f6(a1,a1))), % 106.04/106.06 inference(scs_inference,[],[19,3201,3217,3175,2515,67,2,24,25,3])). % 106.04/106.06 cnf(3242,plain, % 106.04/106.06 (~P2(x32421,f5(a1,f10(a1),a1))), % 106.04/106.06 inference(scs_inference,[],[19,3201,3217,2371,3175,237,2290,2515,67,37,2,24,25,3,13,15])). % 106.04/106.06 cnf(3247,plain, % 106.04/106.06 (~E(f6(a1,a1),f6(a8,a8))), % 106.04/106.06 inference(scs_inference,[],[3239,2])). % 106.04/106.06 cnf(3248,plain, % 106.04/106.06 (~E(f5(a1,f10(a1),a1),f10(x32481))), % 106.04/106.06 inference(scs_inference,[],[3239,3242,18,2,24])). % 106.04/106.06 cnf(3275,plain, % 106.04/106.06 (~P2(f6(f10(a7),f10(a7)),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[3248,2734,610,2515,67,2,24,25])). % 106.04/106.06 cnf(3280,plain, % 106.04/106.06 (~E(f4(f6(a1,a1),f4(a1,a9)),f6(a8,a8))), % 106.04/106.06 inference(scs_inference,[],[3247,3248,2734,2595,610,294,2243,2515,67,2,24,25,13,3])). % 106.04/106.06 cnf(3281,plain, % 106.04/106.06 (~P2(x32811,f5(f10(a1),a1,a1))), % 106.04/106.06 inference(scs_inference,[],[3247,3248,2734,2595,2409,610,294,2243,2515,67,37,2,24,25,13,3,15])). % 106.04/106.06 cnf(3282,plain, % 106.04/106.06 (~P2(f4(a9,a1),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[3247,3248,2734,2595,2409,610,3143,2508,294,2243,2515,67,37,2,24,25,13,3,15,14])). % 106.04/106.06 cnf(3296,plain, % 106.04/106.06 (~E(f6(a1,a1),f6(x32961,a7))), % 106.04/106.06 inference(scs_inference,[],[3280,3275,3281,1135,2117,1793,2192,2206,18,2,30,24,13,3])). % 106.04/106.06 cnf(3299,plain, % 106.04/106.06 (~P2(f4(a9,f6(a1,a9)),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[3282,3280,3275,3281,1135,2117,2245,1793,2192,2206,2479,18,2,30,24,13,3,15,14])). % 106.04/106.06 cnf(3319,plain, % 106.04/106.06 (~P2(x33191,f5(f10(a1),f10(a1),f10(a7)))), % 106.04/106.06 inference(scs_inference,[],[3296,2572,2840,2481,2445,260,77,2247,2515,2253,37,2,24,25,13,3,15])). % 106.04/106.06 cnf(3325,plain, % 106.04/106.06 (~E(f5(f10(a1),f10(a1),f10(a7)),f10(x33251))), % 106.04/106.06 inference(scs_inference,[],[3177,3319,18,2,24])). % 106.04/106.06 cnf(3329,plain, % 106.04/106.06 (~E(f4(a1,a1),f10(a1))), % 106.04/106.06 inference(scs_inference,[],[3177,2946,3319,2909,1777,21,18,2,24,13,3])). % 106.04/106.06 cnf(3336,plain, % 106.04/106.06 (E(f4(a1,f4(a1,a1)),a1)), % 106.04/106.06 inference(scs_inference,[],[3299,3177,2946,3319,1778,2688,2909,2471,1777,973,21,18,2,24,13,3,15,14,25,2537])). % 106.04/106.06 cnf(3338,plain, % 106.04/106.06 (E(a1,f4(a1,f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[3299,3177,2946,3319,1778,2688,2909,2471,1777,973,21,18,2,24,13,3,15,14,25,2537,2540])). % 106.04/106.06 cnf(3350,plain, % 106.04/106.06 (~P2(x33501,f5(f10(a1),f4(a1,a1),a1))), % 106.04/106.06 inference(scs_inference,[],[3329,3325,2303,3082,2199,1128,953,2286,2515,67,37,2,24,25,13,3,15])). % 106.04/106.06 cnf(3354,plain, % 106.04/106.06 (~E(f5(f10(a1),f4(a1,a1),a1),f10(x33541))), % 106.04/106.06 inference(scs_inference,[],[2968,3350,18,2,24])). % 106.04/106.06 cnf(3357,plain, % 106.04/106.06 (~E(f6(a9,f10(a7)),f6(a8,x33571))), % 106.04/106.06 inference(scs_inference,[],[2968,3350,106,2204,18,2,24,13])). % 106.04/106.06 cnf(3376,plain, % 106.04/106.06 (~P2(f6(a9,f10(a7)),f10(a8))), % 106.04/106.06 inference(scs_inference,[],[19,3354,3357,392,2515,2,24,25])). % 106.04/106.06 cnf(3380,plain, % 106.04/106.06 (~E(f5(f10(a1),a1,a1),f10(x33801))), % 106.04/106.06 inference(scs_inference,[],[19,3354,3357,2441,392,2515,2,24,25,3])). % 106.04/106.06 cnf(3392,plain, % 106.04/106.06 (~E(f6(f10(a7),a9),f6(x33921,a8))), % 106.04/106.06 inference(scs_inference,[],[3380,3376,2598,2440,2329,73,2206,2,24,3,13])). % 106.04/106.06 cnf(3408,plain, % 106.04/106.06 (~P2(x34081,f5(f10(a1),f4(a1,a9),f6(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[19,2381,2903,2542,2319,1264,2473,17,2243,122,37,2,24,25,3,13,15])). % 106.04/106.06 cnf(3415,plain, % 106.04/106.06 (~E(a1,f6(x34151,a8))), % 106.04/106.06 inference(scs_inference,[],[19,2641,3392,3408,18,2,24,3])). % 106.04/106.06 cnf(3429,plain, % 106.04/106.06 (~E(f6(x34291,a8),a1)), % 106.04/106.06 inference(scs_inference,[],[3415,2])). % 106.04/106.06 cnf(3438,plain, % 106.04/106.06 (~P2(x34381,f5(f10(a1),f4(a1,a1),f6(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[19,3415,2568,3338,2277,787,77,2286,2479,37,2,24,25,3,13,15])). % 106.04/106.06 cnf(3464,plain, % 106.04/106.06 (~P2(x34641,f5(f10(a1),f10(a1),a1))), % 106.04/106.06 inference(scs_inference,[],[19,3033,3073,2653,2443,242,37,2,24,3,15])). % 106.04/106.06 cnf(3474,plain, % 106.04/106.06 (~E(f5(f10(a1),f10(a1),a1),f10(x34741))), % 106.04/106.06 inference(scs_inference,[],[3136,3464,18,2,24])). % 106.04/106.06 cnf(3475,plain, % 106.04/106.06 (~P2(x34751,f5(f10(a1),f10(a1),a1))), % 106.04/106.06 inference(rename_variables,[],[3464])). % 106.04/106.06 cnf(3483,plain, % 106.04/106.06 (~P2(x34831,f5(f10(a1),f10(a1),f4(a1,a9)))), % 106.04/106.06 inference(scs_inference,[],[3136,3464,3475,2351,2400,2403,2251,2479,18,2,24,25,3,15])). % 106.04/106.06 cnf(3499,plain, % 106.04/106.06 (~P2(x34991,f5(f10(a7),f10(a7),f10(a1)))), % 106.04/106.06 inference(scs_inference,[],[19,3474,2662,2698,3438,3483,2330,1594,37,2,31,24,3,15])). % 106.04/106.06 cnf(3505,plain, % 106.04/106.06 (~E(f5(f10(a7),f10(a7),f10(a1)),f10(x35051))), % 106.04/106.06 inference(scs_inference,[],[2930,3499,18,2,24])). % 106.04/106.06 cnf(3526,plain, % 106.04/106.06 (~P2(x35261,f5(f10(a1),f10(a1),f6(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[3505,2716,1783,2325,2256,37,2,24,3,15])). % 106.04/106.06 cnf(3530,plain, % 106.04/106.06 (~E(f5(f10(a1),f10(a1),f6(a1,a1)),f10(x35301))), % 106.04/106.06 inference(scs_inference,[],[2526,3526,18,2,24])). % 106.04/106.06 cnf(3552,plain, % 106.04/106.06 (~P2(x35521,f5(f4(a1,a1),f10(a1),f6(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[19,2788,3530,2676,2514,807,37,2,24,3,15])). % 106.04/106.06 cnf(3561,plain, % 106.04/106.06 (~E(f5(f4(a1,a1),f10(a1),f6(a1,a1)),f10(x35611))), % 106.04/106.06 inference(scs_inference,[],[2971,3552,18,2,24])). % 106.04/106.06 cnf(3577,plain, % 106.04/106.06 (~E(f5(a1,f10(a1),f6(a1,a1)),f10(x35771))), % 106.04/106.06 inference(scs_inference,[],[19,3561,2437,817,2,24,3])). % 106.04/106.06 cnf(3579,plain, % 106.04/106.06 (~P2(x35791,f4(a1,f4(a1,a1)))), % 106.04/106.06 inference(scs_inference,[],[19,3561,3336,2437,817,37,2,24,3,15])). % 106.04/106.06 cnf(3590,plain, % 106.04/106.06 (~E(a1,f10(x35901))), % 106.04/106.06 inference(scs_inference,[],[19,3577,3579,3429,2332,2215,2,24,25,3])). % 106.04/106.06 cnf(3598,plain, % 106.04/106.06 ($false), % 106.04/106.06 inference(scs_inference,[],[3590,2293,2]), % 106.04/106.06 ['proof']). % 106.04/106.06 % SZS output end Proof % 106.04/106.06 % Total time :105.380000s %------------------------------------------------------------------------------