%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV488+3 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 16:47:28 EDT 2024 % Result : Theorem 75.94s 76.21s % Output : CNFRefutation 75.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : SWV488+3 : TPTP v8.2.0. Released v4.0.0. % 0.02/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.29 % Computer : n022.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Thu Jun 20 20:20:38 EDT 2024 % 0.09/0.29 % CPUTime : % 0.14/0.51 start to proof:theBenchmark % 75.94/76.20 %------------------------------------------- % 75.94/76.20 % File :CSE---1.7 % 75.94/76.20 % Problem :theBenchmark % 75.94/76.20 % Transform :cnf % 75.94/76.20 % Format :tptp:raw % 75.94/76.20 % Command :java -jar mcs_scs.jar %d %s % 75.94/76.20 % 75.94/76.20 % Result :Theorem 75.440000s % 75.94/76.20 % Output :CNFRefutation 75.440000s % 75.94/76.20 %------------------------------------------- % 75.94/76.20 %------------------------------------------------------------------------------ % 75.94/76.20 % File : SWV488+3 : TPTP v8.2.0. Released v4.0.0. % 75.94/76.20 % Domain : Software Verification % 75.94/76.20 % Problem : Matrix has no zero on the diagonal % 75.94/76.20 % Version : Especial. % 75.94/76.20 % English : % 75.94/76.20 % 75.94/76.20 % Refs : [KV09] Kovacs (2009), Email to Geoff Sutcliffe % 75.94/76.20 % Source : [KV09] % 75.94/76.20 % Names : Id4 [KV09] % 75.94/76.20 % 75.94/76.20 % Status : Theorem % 75.94/76.21 % Rating : 0.08 v8.2.0, 0.06 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.03 v6.4.0, 0.08 v6.3.0, 0.00 v6.2.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.11 v5.4.0, 0.18 v5.3.0, 0.22 v5.2.0, 0.05 v5.0.0, 0.08 v4.1.0, 0.13 v4.0.0 % 75.94/76.21 % Syntax : Number of formulae : 13 ( 4 unt; 0 def) % 75.94/76.21 % Number of atoms : 44 ( 13 equ) % 75.94/76.21 % Maximal formula atoms : 17 ( 3 avg) % 75.94/76.21 % Number of connectives : 34 ( 3 ~; 2 |; 15 &) % 75.94/76.21 % ( 3 <=>; 11 =>; 0 <=; 0 <~>) % 75.94/76.21 % Maximal formula depth : 11 ( 5 avg) % 75.94/76.21 % Maximal term depth : 3 ( 1 avg) % 75.94/76.21 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 75.94/76.21 % Number of functors : 7 ( 7 usr; 5 con; 0-2 aty) % 75.94/76.21 % Number of variables : 29 ( 28 !; 1 ?) % 75.94/76.21 % SPC : FOF_THM_RFO_SEQ % 75.94/76.21 % 75.94/76.21 % Comments : % 75.94/76.21 %------------------------------------------------------------------------------ % 75.94/76.21 fof(int_leq,axiom, % 75.94/76.21 ! [I,J] : % 75.94/76.21 ( int_leq(I,J) % 75.94/76.21 <=> ( int_less(I,J) % 75.94/76.21 | I = J ) ) ). % 75.94/76.21 % 75.94/76.21 fof(int_less_transitive,axiom, % 75.94/76.21 ! [I,J,K] : % 75.94/76.21 ( ( int_less(I,J) % 75.94/76.21 & int_less(J,K) ) % 75.94/76.21 => int_less(I,K) ) ). % 75.94/76.21 % 75.94/76.21 fof(int_less_irreflexive,axiom, % 75.94/76.21 ! [I,J] : % 75.94/76.21 ( int_less(I,J) % 75.94/76.21 => I != J ) ). % 75.94/76.21 % 75.94/76.21 fof(int_less_total,axiom, % 75.94/76.21 ! [I,J] : % 75.94/76.21 ( int_less(I,J) % 75.94/76.21 | int_leq(J,I) ) ). % 75.94/76.21 % 75.94/76.21 fof(int_zero_one,axiom, % 75.94/76.21 int_less(int_zero,int_one) ). % 75.94/76.21 % 75.94/76.21 fof(plus_commutative,axiom, % 75.94/76.21 ! [I,J] : plus(I,J) = plus(J,I) ). % 75.94/76.21 % 75.94/76.21 fof(plus_zero,axiom, % 75.94/76.21 ! [I] : plus(I,int_zero) = I ). % 75.94/76.21 % 75.94/76.21 fof(plus_and_order1,axiom, % 75.94/76.21 ! [I1,J1,I2,J2] : % 75.94/76.21 ( ( int_less(I1,J1) % 75.94/76.21 & int_leq(I2,J2) ) % 75.94/76.21 => int_leq(plus(I1,I2),plus(J1,J2)) ) ). % 75.94/76.21 % 75.94/76.21 fof(plus_and_inverse,axiom, % 75.94/76.21 ! [I,J] : % 75.94/76.21 ( int_less(I,J) % 75.94/76.21 <=> ? [K] : % 75.94/76.21 ( plus(I,K) = J % 75.94/76.21 & int_less(int_zero,K) ) ) ). % 75.94/76.21 % 75.94/76.21 fof(one_successor_of_zero,axiom, % 75.94/76.21 ! [I] : % 75.94/76.21 ( int_less(int_zero,I) % 75.94/76.21 <=> int_leq(int_one,I) ) ). % 75.94/76.21 % 75.94/76.21 fof(real_constants,axiom, % 75.94/76.21 real_zero != real_one ). % 75.94/76.21 % 75.94/76.21 fof(qii,hypothesis, % 75.94/76.21 ! [I,J] : % 75.94/76.21 ( ( int_leq(int_one,I) % 75.94/76.21 & int_leq(I,n) % 75.94/76.21 & int_leq(int_one,J) % 75.94/76.21 & int_leq(J,n) ) % 75.94/76.21 => ( ! [C] : % 75.94/76.21 ( ( int_less(int_zero,C) % 75.94/76.21 & I = plus(J,C) ) % 75.94/76.21 => ! [K] : % 75.94/76.21 ( ( int_leq(int_one,K) % 75.94/76.21 & int_leq(K,J) ) % 75.94/76.21 => a(plus(K,C),K) = real_zero ) ) % 75.94/76.21 & ! [K] : % 75.94/76.21 ( ( int_leq(int_one,K) % 75.94/76.21 & int_leq(K,J) ) % 75.94/76.21 => a(K,K) = real_one ) % 75.94/76.21 & ! [C] : % 75.94/76.21 ( ( int_less(int_zero,C) % 75.94/76.21 & J = plus(I,C) ) % 75.94/76.21 => ! [K] : % 75.94/76.21 ( ( int_leq(int_one,K) % 75.94/76.21 & int_leq(K,I) ) % 75.94/76.21 => a(K,plus(K,C)) = real_zero ) ) ) ) ). % 75.94/76.21 % 75.94/76.21 fof(uti,conjecture, % 75.94/76.21 ! [I,J] : % 75.94/76.21 ( ( int_leq(int_one,J) % 75.94/76.21 & int_leq(J,I) % 75.94/76.21 & int_leq(I,n) ) % 75.94/76.21 => ( I = J % 75.94/76.21 => a(I,J) != real_zero ) ) ). % 75.94/76.21 % 75.94/76.21 %------------------------------------------------------------------------------ % 75.94/76.21 %------------------------------------------- % 75.94/76.21 % Proof found % 75.94/76.21 % SZS status Theorem for theBenchmark % 75.94/76.21 % SZS output start Proof % 75.94/76.21 %ClaNum:40(EqnAxiom:15) % 75.94/76.21 %VarNum:99(SingletonVarNum:42) % 75.94/76.21 %MaxLitNum:6 % 75.94/76.21 %MaxfuncDepth:2 % 75.94/76.21 %SharedTerms:15 % 75.94/76.21 %goalClause: 16 17 18 19 20 % 75.94/76.21 %singleGoalClaCount:5 % 75.94/76.21 [16]E(a1,a2) % 75.94/76.21 [18]P1(a6,a1) % 75.94/76.21 [19]P1(a2,a7) % 75.94/76.21 [20]P1(a1,a2) % 75.94/76.21 [21]P3(a8,a6) % 75.94/76.21 [24]~E(a10,a5) % 75.94/76.21 [17]E(f3(a2,a1),a5) % 75.94/76.21 [22]E(f9(x221,a8),x221) % 75.94/76.21 [23]E(f9(x231,x232),f9(x232,x231)) % 75.94/76.21 [28]~P3(a8,x281)+P1(a6,x281) % 75.94/76.21 [29]~P1(a6,x291)+P3(a8,x291) % 75.94/76.21 [25]~E(x251,x252)+P1(x251,x252) % 75.94/76.21 [26]~P3(x261,x262)+~E(x261,x262) % 75.94/76.21 [27]P3(x272,x271)+P1(x271,x272) % 75.94/76.21 [30]~P3(x301,x302)+P1(x301,x302) % 75.94/76.21 [34]~P3(x341,x342)+P3(a8,f4(x341,x342)) % 75.94/76.21 [35]~P3(x351,x352)+E(f9(x351,f4(x351,x352)),x352) % 75.94/76.21 [31]P3(x311,x312)+~P1(x311,x312)+E(x311,x312) % 75.94/76.21 [33]~P3(x331,x333)+P3(x331,x332)+~P3(x333,x332) % 75.94/76.21 [32]P3(x321,x322)+~P3(a8,x323)+~E(f9(x321,x323),x322) % 75.94/76.21 [38]~P1(x382,x384)+~P3(x381,x383)+P1(f9(x381,x382),f9(x383,x384)) % 75.94/76.21 [36]~P1(x361,x362)+~P2(x363,x362)+~P1(a6,x361)+E(f3(x361,x361),a10) % 75.94/76.21 [37]P2(x371,x372)+~P1(x372,a7)+~P1(x371,a7)+~P1(a6,x372)+~P1(a6,x371) % 75.94/76.21 [39]~P1(x391,x394)+~P2(x394,x393)+~P1(a6,x391)+~P3(a8,x392)+~E(x393,f9(x394,x392))+E(f3(x391,f9(x391,x392)),a5) % 75.94/76.21 [40]~P1(x401,x404)+~P2(x403,x404)+~P1(a6,x401)+~P3(a8,x402)+~E(x403,f9(x404,x402))+E(f3(f9(x401,x402),x401),a5) % 75.94/76.21 %EqnAxiom % 75.94/76.21 [1]E(x11,x11) % 75.94/76.21 [2]E(x22,x21)+~E(x21,x22) % 75.94/76.21 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 75.94/76.21 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 75.94/76.21 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 75.94/76.21 [6]~E(x61,x62)+E(f9(x61,x63),f9(x62,x63)) % 75.94/76.21 [7]~E(x71,x72)+E(f9(x73,x71),f9(x73,x72)) % 75.94/76.21 [8]~E(x81,x82)+E(f4(x81,x83),f4(x82,x83)) % 75.94/76.21 [9]~E(x91,x92)+E(f4(x93,x91),f4(x93,x92)) % 75.94/76.21 [10]P1(x102,x103)+~E(x101,x102)+~P1(x101,x103) % 75.94/76.21 [11]P1(x113,x112)+~E(x111,x112)+~P1(x113,x111) % 75.94/76.21 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 75.94/76.21 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 75.94/76.21 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 75.94/76.21 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 75.94/76.21 % 75.94/76.21 %------------------------------------------- % 75.94/76.22 cnf(41,plain, % 75.94/76.22 (P1(x411,x411)), % 75.94/76.22 inference(equality_inference,[],[25])). % 75.94/76.22 cnf(42,plain, % 75.94/76.22 (~P3(x421,x421)), % 75.94/76.22 inference(equality_inference,[],[26])). % 75.94/76.22 cnf(43,plain, % 75.94/76.22 (P3(x431,f9(x431,x432))+~P3(a8,x432)), % 75.94/76.22 inference(equality_inference,[],[32])). % 75.94/76.22 cnf(46,plain, % 75.94/76.22 (~P3(a1,a2)), % 75.94/76.22 inference(scs_inference,[],[16,26])). % 75.94/76.22 cnf(48,plain, % 75.94/76.22 (E(a2,a1)), % 75.94/76.22 inference(scs_inference,[],[16,26,2])). % 75.94/76.22 cnf(49,plain, % 75.94/76.22 (~P1(a6,a8)), % 75.94/76.22 inference(scs_inference,[],[16,42,26,2,29])). % 75.94/76.22 cnf(50,plain, % 75.94/76.22 (~P3(x501,x501)), % 75.94/76.22 inference(rename_variables,[],[42])). % 75.94/76.22 cnf(52,plain, % 75.94/76.22 (~P3(a6,a8)), % 75.94/76.22 inference(scs_inference,[],[16,42,26,2,29,30])). % 75.94/76.22 cnf(54,plain, % 75.94/76.22 (P3(x541,f9(x541,a6))), % 75.94/76.22 inference(scs_inference,[],[16,42,21,26,2,29,30,43])). % 75.94/76.22 cnf(56,plain, % 75.94/76.22 (E(f9(a1,a8),a2)), % 75.94/76.22 inference(scs_inference,[],[16,42,22,21,26,2,29,30,43,3])). % 75.94/76.22 cnf(58,plain, % 75.94/76.22 (P1(a1,a7)), % 75.94/76.22 inference(scs_inference,[],[16,19,42,22,21,26,2,29,30,43,3,10])). % 75.94/76.22 cnf(59,plain, % 75.94/76.22 (~E(a1,a8)), % 75.94/76.22 inference(scs_inference,[],[16,18,19,42,22,21,26,2,29,30,43,3,10,11])). % 75.94/76.22 cnf(60,plain, % 75.94/76.22 (P3(x601,f9(a6,x601))), % 75.94/76.22 inference(scs_inference,[],[16,18,19,42,23,22,21,26,2,29,30,43,3,10,11,32])). % 75.94/76.22 cnf(63,plain, % 75.94/76.22 (P3(a8,f9(a6,a6))), % 75.94/76.22 inference(scs_inference,[],[16,18,19,42,23,22,21,26,2,29,30,43,3,10,11,32,33])). % 75.94/76.22 cnf(66,plain, % 75.94/76.22 (~P3(x661,x661)), % 75.94/76.22 inference(rename_variables,[],[42])). % 75.94/76.22 cnf(73,plain, % 75.94/76.22 (P2(a2,a1)), % 75.94/76.22 inference(scs_inference,[],[16,18,19,42,50,66,23,22,21,26,2,29,30,43,3,10,11,32,33,12,13,37,31,14])). % 75.94/76.22 cnf(74,plain, % 75.94/76.22 (P2(a1,a2)), % 75.94/76.22 inference(scs_inference,[],[16,18,19,42,50,66,23,22,21,26,2,29,30,43,3,10,11,32,33,12,13,37,31,14,15])). % 75.94/76.22 cnf(79,plain, % 75.94/76.22 (~P3(f3(a2,a1),a5)), % 75.94/76.22 inference(scs_inference,[],[17,26])). % 75.94/76.22 cnf(81,plain, % 75.94/76.22 (P3(x811,f9(x811,f9(a8,a6)))), % 75.94/76.22 inference(scs_inference,[],[17,54,26,43])). % 75.94/76.22 cnf(82,plain, % 75.94/76.22 (P3(x821,f9(x821,a6))), % 75.94/76.22 inference(rename_variables,[],[54])). % 75.94/76.22 cnf(84,plain, % 75.94/76.22 (E(a5,f3(a2,a1))), % 75.94/76.22 inference(scs_inference,[],[17,54,26,43,2])). % 75.94/76.22 cnf(85,plain, % 75.94/76.22 (P3(x851,f9(f9(a6,x851),a6))), % 75.94/76.22 inference(scs_inference,[],[17,54,82,60,26,43,2,33])). % 75.94/76.22 cnf(86,plain, % 75.94/76.22 (P3(x861,f9(x861,a6))), % 75.94/76.22 inference(rename_variables,[],[54])). % 75.94/76.22 cnf(90,plain, % 75.94/76.22 (~E(f9(a1,a6),a2)), % 75.94/76.22 inference(scs_inference,[],[17,46,42,54,82,86,60,26,43,2,33,12,13])). % 75.94/76.22 cnf(91,plain, % 75.94/76.22 (P3(x911,f9(x911,a6))), % 75.94/76.22 inference(rename_variables,[],[54])). % 75.94/76.22 cnf(93,plain, % 75.94/76.22 (P3(x931,f9(f9(a8,a6),x931))), % 75.94/76.22 inference(scs_inference,[],[16,17,46,42,54,82,86,91,60,73,23,26,43,2,33,12,13,15,32])). % 75.94/76.22 cnf(100,plain, % 75.94/76.22 (P1(x1001,a1)+~E(a6,x1001)), % 75.94/76.22 inference(scs_inference,[],[16,17,19,18,46,42,54,82,86,91,60,73,23,26,43,2,33,12,13,15,32,3,31,10])). % 75.94/76.22 cnf(108,plain, % 75.94/76.22 (~P3(a2,a1)), % 75.94/76.22 inference(scs_inference,[],[48,26])). % 75.94/76.22 cnf(110,plain, % 75.94/76.22 (P3(x1101,f9(x1101,f9(a6,a6)))), % 75.94/76.22 inference(scs_inference,[],[48,63,26,43])). % 75.94/76.22 cnf(112,plain, % 75.94/76.22 (E(a2,f9(a1,a8))), % 75.94/76.22 inference(scs_inference,[],[48,56,63,26,43,2])). % 75.94/76.22 cnf(113,plain, % 75.94/76.22 (P3(x1131,f9(f9(f9(a8,a6),x1131),f9(a8,a6)))), % 75.94/76.22 inference(scs_inference,[],[48,56,93,81,63,26,43,2,33])). % 75.94/76.22 cnf(118,plain, % 75.94/76.22 (~E(f9(f9(a8,a6),f3(a2,a1)),a5)), % 75.94/76.22 inference(scs_inference,[],[48,56,79,42,93,81,63,26,43,2,33,12,13])). % 75.94/76.22 cnf(120,plain, % 75.94/76.22 (~E(a10,f3(a2,a1))), % 75.94/76.22 inference(scs_inference,[],[17,48,56,79,42,93,81,63,24,26,43,2,33,12,13,3])). % 75.94/76.22 cnf(123,plain, % 75.94/76.22 (P1(a1,x1231)+~E(a7,x1231)), % 75.94/76.22 inference(scs_inference,[],[17,58,48,56,79,42,93,81,63,24,26,43,2,33,12,13,3,31,11])). % 75.94/76.22 cnf(128,plain, % 75.94/76.22 (~P3(a5,f3(a2,a1))), % 75.94/76.22 inference(scs_inference,[],[84,26])). % 75.94/76.22 cnf(130,plain, % 75.94/76.22 (P3(x1301,f9(x1301,f9(a6,a8)))), % 75.94/76.22 inference(scs_inference,[],[84,60,26,43])). % 75.94/76.22 cnf(133,plain, % 75.94/76.22 (E(x1331,f9(x1331,a8))), % 75.94/76.22 inference(scs_inference,[],[84,60,22,26,43,2])). % 75.94/76.22 cnf(134,plain, % 75.94/76.22 (P2(f9(a1,a8),a1)), % 75.94/76.22 inference(scs_inference,[],[84,112,73,60,22,26,43,2,14])). % 75.94/76.22 cnf(135,plain, % 75.94/76.22 (P1(f9(a1,a8),a7)), % 75.94/76.22 inference(scs_inference,[],[19,84,112,73,60,22,26,43,2,14,10])). % 75.94/76.22 cnf(136,plain, % 75.94/76.23 (~P3(f9(a6,a6),a8)), % 75.94/76.23 inference(scs_inference,[],[19,84,112,42,73,60,22,63,26,43,2,14,10,33])). % 75.94/76.23 cnf(137,plain, % 75.94/76.23 (~P3(x1371,x1371)), % 75.94/76.23 inference(rename_variables,[],[42])). % 75.94/76.23 cnf(139,plain, % 75.94/76.23 (P2(a1,f9(a1,a8))), % 75.94/76.23 inference(scs_inference,[],[19,84,112,42,74,73,60,22,63,26,43,2,14,10,33,15])). % 75.94/76.23 cnf(140,plain, % 75.94/76.23 (~E(x1401,f9(f9(f9(a8,a6),x1401),f9(a8,a6)))), % 75.94/76.23 inference(scs_inference,[],[19,84,112,42,137,74,73,113,60,22,63,26,43,2,14,10,33,15,12])). % 75.94/76.23 cnf(144,plain, % 75.94/76.23 (P1(a2,f9(a7,a8))), % 75.94/76.23 inference(scs_inference,[],[19,84,112,108,42,137,74,73,113,60,22,63,26,43,2,14,10,33,15,12,13,11])). % 75.94/76.23 cnf(146,plain, % 75.94/76.23 (P1(a1,f9(a7,a8))), % 75.94/76.23 inference(scs_inference,[],[19,17,84,112,108,42,137,74,73,113,118,60,22,63,26,43,2,14,10,33,15,12,13,11,3,123])). % 75.94/76.23 cnf(151,plain, % 75.94/76.23 (P1(f9(a6,a8),a1)), % 75.94/76.23 inference(scs_inference,[],[133,100])). % 75.94/76.23 cnf(152,plain, % 75.94/76.23 (E(x1521,f9(x1521,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(153,plain, % 75.94/76.23 (~P3(x1531,f9(x1531,a8))), % 75.94/76.23 inference(scs_inference,[],[133,152,100,26])). % 75.94/76.23 cnf(155,plain, % 75.94/76.23 (P2(f9(a2,a8),a1)), % 75.94/76.23 inference(scs_inference,[],[133,152,73,100,26,14])). % 75.94/76.23 cnf(156,plain, % 75.94/76.23 (E(x1561,f9(x1561,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(157,plain, % 75.94/76.23 (P3(x1571,f9(f9(x1571,f9(a6,a6)),f9(a6,a8)))), % 75.94/76.23 inference(scs_inference,[],[133,152,73,130,110,100,26,14,33])). % 75.94/76.23 cnf(158,plain, % 75.94/76.23 (P3(x1581,f9(x1581,f9(a6,a8)))), % 75.94/76.23 inference(rename_variables,[],[130])). % 75.94/76.23 cnf(160,plain, % 75.94/76.23 (P1(f9(a2,a8),a7)), % 75.94/76.23 inference(scs_inference,[],[19,133,152,156,73,130,110,100,26,14,33,10])). % 75.94/76.23 cnf(161,plain, % 75.94/76.23 (E(x1611,f9(x1611,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(162,plain, % 75.94/76.23 (P2(a1,f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[19,133,152,156,161,74,73,130,110,100,26,14,33,10,15])). % 75.94/76.23 cnf(163,plain, % 75.94/76.23 (E(x1631,f9(x1631,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(166,plain, % 75.94/76.23 (~E(f9(a1,a6),f9(a1,a8))), % 75.94/76.23 inference(scs_inference,[],[19,133,152,156,161,56,42,74,73,130,158,110,90,100,26,14,33,10,15,12,3])). % 75.94/76.23 cnf(167,plain, % 75.94/76.23 (P1(a1,f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[19,20,133,152,156,161,163,56,42,74,73,130,158,110,90,100,26,14,33,10,15,12,3,11])). % 75.94/76.23 cnf(178,plain, % 75.94/76.23 (~P1(a6,f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[153,29])). % 75.94/76.23 cnf(179,plain, % 75.94/76.23 (~P3(x1791,f9(x1791,a8))), % 75.94/76.23 inference(rename_variables,[],[153])). % 75.94/76.23 cnf(181,plain, % 75.94/76.23 (~P3(f9(a1,a8),a2)), % 75.94/76.23 inference(scs_inference,[],[56,153,29,26])). % 75.94/76.23 cnf(183,plain, % 75.94/76.23 (P3(x1831,f9(a6,f9(x1831,a6)))), % 75.94/76.23 inference(scs_inference,[],[56,153,54,60,29,26,33])). % 75.94/76.23 cnf(186,plain, % 75.94/76.23 (P1(f9(f9(a6,a8),a8),a1)), % 75.94/76.23 inference(scs_inference,[],[56,153,151,133,54,60,29,26,33,10])). % 75.94/76.23 cnf(187,plain, % 75.94/76.23 (E(x1871,f9(x1871,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(188,plain, % 75.94/76.23 (P2(a2,f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[16,56,153,151,133,54,60,162,29,26,33,10,14])). % 75.94/76.23 cnf(189,plain, % 75.94/76.23 (P2(a1,f9(f9(a2,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[16,56,153,151,133,187,54,60,162,29,26,33,10,14,15])). % 75.94/76.23 cnf(190,plain, % 75.94/76.23 (E(x1901,f9(x1901,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(191,plain, % 75.94/76.23 (~E(a8,f9(a6,a6))), % 75.94/76.23 inference(scs_inference,[],[16,56,153,151,133,187,42,54,60,63,162,29,26,33,10,14,15,12])). % 75.94/76.23 cnf(193,plain, % 75.94/76.23 (~E(f9(a1,a6),f9(a8,a1))), % 75.94/76.23 inference(scs_inference,[],[16,56,153,166,151,133,187,42,54,60,23,63,162,29,26,33,10,14,15,12,3])). % 75.94/76.23 cnf(195,plain, % 75.94/76.23 (~E(f9(x1951,a6),f9(x1951,a8))), % 75.94/76.23 inference(scs_inference,[],[16,56,153,179,166,151,133,187,42,54,60,23,63,162,29,26,33,10,14,15,12,3,13])). % 75.94/76.23 cnf(197,plain, % 75.94/76.23 (P1(a1,f9(f9(a7,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[16,56,146,153,179,166,151,133,187,190,42,54,60,23,63,162,29,26,33,10,14,15,12,3,13,11])). % 75.94/76.23 cnf(199,plain, % 75.94/76.23 (~E(a6,f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[16,56,146,153,179,166,151,133,187,190,42,54,60,23,63,162,29,26,33,10,14,15,12,3,13,11,25])). % 75.94/76.23 cnf(201,plain, % 75.94/76.23 (P3(f9(a8,a8),a6)), % 75.94/76.23 inference(scs_inference,[],[16,56,146,153,179,166,151,133,187,190,42,54,60,23,63,162,29,26,33,10,14,15,12,3,13,11,25,27])). % 75.94/76.23 cnf(203,plain, % 75.94/76.23 (~P3(a6,f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[16,56,146,153,179,166,151,133,187,190,42,54,60,23,63,162,29,26,33,10,14,15,12,3,13,11,25,27,30])). % 75.94/76.23 cnf(212,plain, % 75.94/76.23 (~P3(a2,f9(a1,a8))), % 75.94/76.23 inference(scs_inference,[],[112,26])). % 75.94/76.23 cnf(214,plain, % 75.94/76.23 (P3(x2141,f9(f9(a6,a6),x2141))), % 75.94/76.23 inference(scs_inference,[],[112,63,23,26,32])). % 75.94/76.23 cnf(217,plain, % 75.94/76.23 (P3(a8,f9(f9(a6,a6),a6))), % 75.94/76.23 inference(scs_inference,[],[112,63,54,23,26,32,33])). % 75.94/76.23 cnf(220,plain, % 75.94/76.23 (P1(a2,f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[16,112,167,63,54,23,26,32,33,10])). % 75.94/76.23 cnf(221,plain, % 75.94/76.23 (P2(a2,f9(f9(a2,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[16,112,167,63,54,23,189,26,32,33,10,14])). % 75.94/76.23 cnf(222,plain, % 75.94/76.23 (P2(f9(a1,a8),a2)), % 75.94/76.23 inference(scs_inference,[],[16,112,167,63,54,23,189,134,26,32,33,10,14,15])). % 75.94/76.23 cnf(223,plain, % 75.94/76.23 (~E(x2231,f9(f9(x2231,f9(a6,a6)),f9(a6,a8)))), % 75.94/76.23 inference(scs_inference,[],[16,112,167,42,63,54,23,157,189,134,26,32,33,10,14,15,12])). % 75.94/76.23 cnf(225,plain, % 75.94/76.23 (P1(a1,f9(f9(a2,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[16,112,167,133,42,63,54,23,157,189,134,26,32,33,10,14,15,12,11])). % 75.94/76.23 cnf(229,plain, % 75.94/76.23 (~E(f9(a6,a6),f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[16,199,112,167,153,133,42,22,63,54,23,157,189,134,26,32,33,10,14,15,12,11,3,13])). % 75.94/76.23 cnf(238,plain, % 75.94/76.23 (~P3(f9(x2381,a8),x2381)), % 75.94/76.23 inference(scs_inference,[],[22,223,6,26])). % 75.94/76.23 cnf(240,plain, % 75.94/76.23 (P3(x2401,f9(f9(x2401,a6),a8))), % 75.94/76.23 inference(scs_inference,[],[133,21,22,223,6,26,32])). % 75.94/76.23 cnf(241,plain, % 75.94/76.23 (E(x2411,f9(x2411,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(243,plain, % 75.94/76.23 (P3(a8,f9(a6,f9(a6,a6)))), % 75.94/76.23 inference(scs_inference,[],[133,21,22,223,183,6,26,32,33])). % 75.94/76.23 cnf(246,plain, % 75.94/76.23 (P1(a2,f9(f9(a2,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[16,225,133,21,22,223,183,6,26,32,33,10])). % 75.94/76.23 cnf(247,plain, % 75.94/76.23 (P2(a2,f9(a1,a8))), % 75.94/76.23 inference(scs_inference,[],[16,225,133,21,22,223,183,139,6,26,32,33,10,14])). % 75.94/76.23 cnf(250,plain, % 75.94/76.23 (P2(f9(a2,a8),a2)), % 75.94/76.23 inference(scs_inference,[],[16,225,133,42,21,22,223,201,183,139,155,6,26,32,33,10,14,12,15])). % 75.94/76.23 cnf(251,plain, % 75.94/76.23 (~E(f9(a6,f9(a1,a8)),a2)), % 75.94/76.23 inference(scs_inference,[],[16,181,225,133,42,21,60,22,223,201,183,139,155,6,26,32,33,10,14,12,15,13])). % 75.94/76.23 cnf(253,plain, % 75.94/76.23 (P1(f9(a2,a8),f9(a7,a8))), % 75.94/76.23 inference(scs_inference,[],[16,181,225,160,133,241,42,21,60,22,223,201,183,139,155,6,26,32,33,10,14,12,15,13,11])). % 75.94/76.23 cnf(262,plain, % 75.94/76.23 (~P3(f9(x2621,x2622),f9(x2622,x2621))), % 75.94/76.23 inference(scs_inference,[],[23,26])). % 75.94/76.23 cnf(265,plain, % 75.94/76.23 (~P3(f9(x2651,a8),x2651)), % 75.94/76.23 inference(rename_variables,[],[238])). % 75.94/76.23 cnf(268,plain, % 75.94/76.23 (E(x2681,f9(x2681,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(269,plain, % 75.94/76.23 (P2(f9(f9(a2,a8),a8),a2)), % 75.94/76.23 inference(scs_inference,[],[253,238,133,268,63,23,250,26,33,10,14])). % 75.94/76.23 cnf(270,plain, % 75.94/76.23 (E(x2701,f9(x2701,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(275,plain, % 75.94/76.23 (P1(f9(a2,a8),f9(f9(a7,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[16,48,253,238,265,133,268,270,63,23,250,251,26,33,10,14,12,15,3,11])). % 75.94/76.23 cnf(285,plain, % 75.94/76.23 (~P3(x2851,x2851)), % 75.94/76.23 inference(rename_variables,[],[42])). % 75.94/76.23 cnf(287,plain, % 75.94/76.23 (P1(f9(f9(a2,a8),a8),f9(f9(a7,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[42,275,133,217,33,10])). % 75.94/76.23 cnf(289,plain, % 75.94/76.23 (~E(x2891,f9(f9(a6,x2891),a6))), % 75.94/76.23 inference(scs_inference,[],[42,285,275,133,85,217,33,10,12])). % 75.94/76.23 cnf(291,plain, % 75.94/76.23 (~E(f9(f9(a6,a6),x2911),f9(x2911,a8))), % 75.94/76.23 inference(scs_inference,[],[153,42,285,275,133,214,85,217,33,10,12,13])). % 75.94/76.23 cnf(293,plain, % 75.94/76.23 (P1(f9(f9(a6,a8),a8),a2)), % 75.94/76.23 inference(scs_inference,[],[16,153,42,285,275,186,133,214,85,217,33,10,12,13,11])). % 75.94/76.23 cnf(294,plain, % 75.94/76.23 (~E(f9(a6,a6),a8)), % 75.94/76.23 inference(scs_inference,[],[16,153,42,285,275,186,133,214,85,217,33,10,12,13,11,7])). % 75.94/76.23 cnf(295,plain, % 75.94/76.23 (~E(x2951,f9(a6,f9(x2951,a6)))), % 75.94/76.23 inference(scs_inference,[],[16,153,42,285,275,186,133,214,85,217,33,10,12,13,11,7,6])). % 75.94/76.23 cnf(306,plain, % 75.94/76.23 (~P3(x3061,x3061)), % 75.94/76.23 inference(rename_variables,[],[42])). % 75.94/76.23 cnf(313,plain, % 75.94/76.23 (P1(f9(a1,a8),f9(a7,a8))), % 75.94/76.23 inference(scs_inference,[],[16,153,42,306,197,135,133,240,243,33,10,12,13,11])). % 75.94/76.23 cnf(315,plain, % 75.94/76.23 (~E(f9(x3151,a6),x3151)), % 75.94/76.23 inference(scs_inference,[],[16,153,42,306,197,135,133,240,243,33,10,12,13,11,6])). % 75.94/76.23 cnf(325,plain, % 75.94/76.23 (P3(a8,f9(a6,f9(a6,a8)))), % 75.94/76.23 inference(scs_inference,[],[21,130,33])). % 75.94/76.23 cnf(326,plain, % 75.94/76.23 (P3(x3261,f9(x3261,f9(a6,a8)))), % 75.94/76.23 inference(rename_variables,[],[130])). % 75.94/76.23 cnf(329,plain, % 75.94/76.23 (E(x3291,f9(x3291,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(332,plain, % 75.94/76.23 (~E(f9(a2,a6),a1)), % 75.94/76.23 inference(scs_inference,[],[16,42,315,160,133,21,130,217,33,10,12,3])). % 75.94/76.23 cnf(334,plain, % 75.94/76.23 (~E(f9(x3341,f9(a6,a8)),f9(x3341,a8))), % 75.94/76.23 inference(scs_inference,[],[16,153,42,315,160,133,21,130,326,217,33,10,12,3,13])). % 75.94/76.23 cnf(336,plain, % 75.94/76.23 (P1(f9(a1,a8),f9(f9(a7,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[16,153,42,315,313,160,133,329,21,130,326,217,33,10,12,3,13,11])). % 75.94/76.23 cnf(347,plain, % 75.94/76.23 (~P3(x3471,x3471)), % 75.94/76.23 inference(rename_variables,[],[42])). % 75.94/76.23 cnf(351,plain, % 75.94/76.23 (~E(f9(a5,a6),f3(a2,a1))), % 75.94/76.23 inference(scs_inference,[],[17,42,347,315,325,33,12,3])). % 75.94/76.23 cnf(353,plain, % 75.94/76.23 (~E(f9(a6,f9(a6,a8)),f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[17,153,42,347,315,325,33,12,3,13])). % 75.94/76.23 cnf(355,plain, % 75.94/76.23 (P1(f9(a6,a8),a2)), % 75.94/76.23 inference(scs_inference,[],[16,17,153,42,347,151,315,325,33,12,3,13,11])). % 75.94/76.23 cnf(366,plain, % 75.94/76.23 (~E(x3661,f9(x3661,f9(a8,a6)))), % 75.94/76.23 inference(scs_inference,[],[42,21,157,81,33,12])). % 75.94/76.23 cnf(394,plain, % 75.94/76.23 (P3(a8,f9(f9(a6,a6),f9(a6,a6)))), % 75.94/76.23 inference(scs_inference,[],[63,110,33])). % 75.94/76.23 cnf(395,plain, % 75.94/76.23 (P3(x3951,f9(x3951,f9(a6,a6)))), % 75.94/76.23 inference(rename_variables,[],[110])). % 75.94/76.23 cnf(397,plain, % 75.94/76.23 (~E(x3971,f9(x3971,f9(a6,a6)))), % 75.94/76.23 inference(scs_inference,[],[42,63,110,395,33,12])). % 75.94/76.23 cnf(410,plain, % 75.94/76.23 (P1(f9(a6,a8),a6)), % 75.94/76.23 inference(scs_inference,[],[21,133,28,10])). % 75.94/76.23 cnf(412,plain, % 75.94/76.23 (~P3(x4121,x4121)), % 75.94/76.23 inference(rename_variables,[],[42])). % 75.94/76.23 cnf(415,plain, % 75.94/76.23 (E(x4151,f9(x4151,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(420,plain, % 75.94/76.23 (~E(f9(a2,a6),f9(a1,a8))), % 75.94/76.23 inference(scs_inference,[],[56,133,415,315,42,412,410,394,33,10,11,12,3])). % 75.94/76.23 cnf(422,plain, % 75.94/76.23 (~E(f9(f9(a6,a6),f9(a6,a6)),f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[56,133,415,153,315,42,412,410,394,33,10,11,12,3,13])). % 75.94/76.23 cnf(431,plain, % 75.94/76.23 (P3(a8,f9(f9(f9(a8,a6),f9(a6,a6)),f9(a8,a6)))), % 75.94/76.23 inference(scs_inference,[],[63,113,33])). % 75.94/76.23 cnf(436,plain, % 75.94/76.23 (~E(f9(f9(a6,x4361),a6),f9(x4361,a8))), % 75.94/76.23 inference(scs_inference,[],[153,42,63,85,113,33,12,13])). % 75.94/76.23 cnf(447,plain, % 75.94/76.23 (P2(f9(f9(a1,a8),a8),a2)), % 75.94/76.23 inference(scs_inference,[],[133,222,14])). % 75.94/76.23 cnf(448,plain, % 75.94/76.23 (E(x4481,f9(x4481,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(452,plain, % 75.94/76.23 (P2(a2,f9(f9(a1,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[133,448,42,222,247,431,14,33,15])). % 75.94/76.23 cnf(469,plain, % 75.94/76.23 (P2(a1,f9(f9(a1,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[48,452,14])). % 75.94/76.23 cnf(470,plain, % 75.94/76.23 (P3(a8,f9(f9(f9(a8,a6),a6),f9(a8,a6)))), % 75.94/76.23 inference(scs_inference,[],[48,21,113,452,14,33])). % 75.94/76.23 cnf(473,plain, % 75.94/76.23 (P2(f9(f9(a1,a8),a8),a1)), % 75.94/76.23 inference(scs_inference,[],[48,21,113,452,447,14,33,15])). % 75.94/76.23 cnf(489,plain, % 75.94/76.23 (P3(a8,f9(f9(a6,a6),f9(a6,a8)))), % 75.94/76.23 inference(scs_inference,[],[63,130,33])). % 75.94/76.23 cnf(494,plain, % 75.94/76.23 (~E(f9(f9(a6,a6),a6),f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[153,42,63,217,130,33,12,13])). % 75.94/76.23 cnf(508,plain, % 75.94/76.23 (~E(f9(a6,f9(a6,a6)),f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[153,42,243,489,33,13])). % 75.94/76.23 cnf(519,plain, % 75.94/76.23 (P3(a8,f9(f9(f9(a6,a6),f9(a6,a6)),f9(a6,a8)))), % 75.94/76.23 inference(scs_inference,[],[63,157,33])). % 75.94/76.23 cnf(524,plain, % 75.94/76.23 (~E(f9(x5241,f9(a8,a6)),f9(x5241,a8))), % 75.94/76.23 inference(scs_inference,[],[153,42,63,157,81,33,12,13])). % 75.94/76.23 cnf(535,plain, % 75.94/76.23 (P2(f9(a2,a8),f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[133,188,14])). % 75.94/76.23 cnf(536,plain, % 75.94/76.23 (E(x5361,f9(x5361,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(540,plain, % 75.94/76.23 (P2(f9(a1,a8),f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[133,536,42,188,222,470,14,33,15])). % 75.94/76.23 cnf(541,plain, % 75.94/76.23 (E(x5411,f9(x5411,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(543,plain, % 75.94/76.23 (E(x5431,f9(x5431,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(544,plain, % 75.94/76.23 (P1(f9(a6,a8),f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[133,536,541,543,355,246,42,188,222,470,14,33,15,10,11])). % 75.94/76.23 cnf(557,plain, % 75.94/76.23 (P2(f9(f9(a2,a8),a8),f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[133,535,14])). % 75.94/76.23 cnf(558,plain, % 75.94/76.23 (E(x5581,f9(x5581,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(559,plain, % 75.94/76.23 (P3(a8,f9(f9(a6,a6),f9(a8,a6)))), % 75.94/76.23 inference(scs_inference,[],[133,63,81,535,14,33])). % 75.94/76.23 cnf(562,plain, % 75.94/76.23 (P2(f9(a2,a8),f9(f9(a2,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[133,558,63,81,535,14,33,15])). % 75.94/76.23 cnf(563,plain, % 75.94/76.23 (E(x5631,f9(x5631,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(564,plain, % 75.94/76.23 (P1(f9(f9(a6,a8),a8),f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[133,558,563,544,63,81,535,14,33,15,10])). % 75.94/76.23 cnf(565,plain, % 75.94/76.23 (E(x5651,f9(x5651,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(566,plain, % 75.94/76.23 (P1(f9(a6,a8),f9(f9(a2,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[133,558,563,565,544,63,81,535,14,33,15,10,11])). % 75.94/76.23 cnf(582,plain, % 75.94/76.23 (E(x5821,f9(x5821,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(586,plain, % 75.94/76.23 (P2(f9(a1,a8),f9(f9(a2,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[133,582,42,519,562,540,14,33,15])). % 75.94/76.23 cnf(587,plain, % 75.94/76.23 (E(x5871,f9(x5871,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(590,plain, % 75.94/76.23 (~E(f9(f9(a6,a6),f9(a6,a8)),f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[133,582,587,153,42,566,489,519,562,540,14,33,15,10,13])). % 75.94/76.23 cnf(615,plain, % 75.94/76.23 (P3(a8,f9(f9(a8,a6),f9(a6,a6)))), % 75.94/76.23 inference(scs_inference,[],[63,93,33])). % 75.94/76.23 cnf(631,plain, % 75.94/76.23 (P2(f9(f9(a1,a8),a8),f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[133,540,14])). % 75.94/76.23 cnf(649,plain, % 75.94/76.23 (~E(f9(f9(a8,a6),x6491),f9(x6491,a8))), % 75.94/76.23 inference(scs_inference,[],[153,93,13])). % 75.94/76.23 cnf(658,plain, % 75.94/76.23 (P3(a8,f9(f9(a8,a6),a6))), % 75.94/76.23 inference(scs_inference,[],[21,93,33])). % 75.94/76.23 cnf(663,plain, % 75.94/76.23 (~E(f9(f9(a8,a6),a6),f9(a8,a8))), % 75.94/76.23 inference(scs_inference,[],[153,42,21,93,33,12,13])). % 75.94/76.23 cnf(673,plain, % 75.94/76.23 (P2(f9(a2,a8),f9(a1,a8))), % 75.94/76.23 inference(scs_inference,[],[133,247,14])). % 75.94/76.23 cnf(674,plain, % 75.94/76.23 (E(x6741,f9(x6741,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(678,plain, % 75.94/76.23 (P2(f9(a2,a8),f9(f9(a1,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[133,674,42,247,658,14,33,15])). % 75.94/76.23 cnf(679,plain, % 75.94/76.23 (E(x6791,f9(x6791,a8))), % 75.94/76.23 inference(rename_variables,[],[133])). % 75.94/76.23 cnf(680,plain, % 75.94/76.23 (E(a1,f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[16,133,674,679,42,247,658,14,33,15,3])). % 75.94/76.23 cnf(682,plain, % 75.94/76.23 (~P3(a1,f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[16,133,674,679,42,247,658,14,33,15,3,26])). % 75.94/76.23 cnf(684,plain, % 75.94/76.23 (E(f9(a2,a8),a1)), % 75.94/76.23 inference(scs_inference,[],[16,133,674,679,42,247,658,14,33,15,3,26,2])). % 75.94/76.23 cnf(699,plain, % 75.94/76.23 (~P3(f9(a2,a8),a1)), % 75.94/76.23 inference(scs_inference,[],[684,26])). % 75.94/76.23 cnf(714,plain, % 75.94/76.23 (E(f3(a2,a1),f9(a5,a8))), % 75.94/76.23 inference(scs_inference,[],[17,133,3])). % 75.94/76.23 cnf(716,plain, % 75.94/76.23 (~P3(f3(a2,a1),f9(a5,a8))), % 75.94/76.23 inference(scs_inference,[],[17,133,3,26])). % 75.94/76.23 cnf(718,plain, % 75.94/76.23 (E(f9(a5,a8),f3(a2,a1))), % 75.94/76.23 inference(scs_inference,[],[17,133,3,26,2])). % 75.94/76.23 cnf(720,plain, % 75.94/76.23 (~P3(f9(a5,a8),f3(a2,a1))), % 75.94/76.23 inference(scs_inference,[],[718,26])). % 75.94/76.23 cnf(727,plain, % 75.94/76.23 (~E(f9(a1,a6),f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[315,684,3])). % 75.94/76.23 cnf(740,plain, % 75.94/76.23 (~E(f9(f3(a2,a1),a6),f9(a5,a8))), % 75.94/76.23 inference(scs_inference,[],[315,718,3])). % 75.94/76.23 cnf(742,plain, % 75.94/76.23 (~E(f9(f9(a5,a8),a6),f3(a2,a1))), % 75.94/76.23 inference(scs_inference,[],[315,714,3])). % 75.94/76.23 cnf(745,plain, % 75.94/76.23 (P1(a6,a2)), % 75.94/76.23 inference(scs_inference,[],[22,355,10])). % 75.94/76.23 cnf(747,plain, % 75.94/76.23 (~E(a2,a8)), % 75.94/76.23 inference(scs_inference,[],[22,355,49,10,11])). % 75.94/76.23 cnf(759,plain, % 75.94/76.23 (P1(a6,f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[22,544,10])). % 75.94/76.23 cnf(761,plain, % 75.94/76.23 (~E(f9(a2,a8),a8)), % 75.94/76.23 inference(scs_inference,[],[22,544,49,10,11])). % 75.94/76.23 cnf(772,plain, % 75.94/76.23 (P1(a6,f9(f9(a2,a8),a8))), % 75.94/76.23 inference(scs_inference,[],[22,566,10])). % 75.94/76.23 cnf(807,plain, % 75.94/76.23 (P2(f9(a8,a2),a1)), % 75.94/76.23 inference(scs_inference,[],[23,155,14])). % 75.94/76.23 cnf(808,plain, % 75.94/76.23 (E(f9(x8081,x8082),f9(x8082,x8081))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(809,plain, % 75.94/76.23 (P2(a2,f9(a8,a2))), % 75.94/76.23 inference(scs_inference,[],[23,808,155,188,14,15])). % 75.94/76.23 cnf(810,plain, % 75.94/76.23 (E(f9(x8101,x8102),f9(x8102,x8101))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(811,plain, % 75.94/76.23 (P1(f9(a8,a1),a7)), % 75.94/76.23 inference(scs_inference,[],[23,808,810,135,155,188,14,15,10])). % 75.94/76.23 cnf(812,plain, % 75.94/76.23 (E(f9(x8121,x8122),f9(x8122,x8121))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(813,plain, % 75.94/76.23 (P1(a2,f9(a8,a7))), % 75.94/76.23 inference(scs_inference,[],[23,808,810,812,135,144,155,188,14,15,10,11])). % 75.94/76.23 cnf(825,plain, % 75.94/76.23 (P2(f9(a8,a2),a2)), % 75.94/76.23 inference(scs_inference,[],[23,250,14])). % 75.94/76.23 cnf(843,plain, % 75.94/76.23 (E(f9(x8431,x8432),f9(x8432,x8431))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(844,plain, % 75.94/76.23 (P2(a1,f9(a8,a2))), % 75.94/76.23 inference(scs_inference,[],[23,843,134,162,14,15])). % 75.94/76.23 cnf(845,plain, % 75.94/76.23 (E(f9(x8451,x8452),f9(x8452,x8451))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(846,plain, % 75.94/76.23 (P1(f9(a8,a1),f9(a7,a8))), % 75.94/76.23 inference(scs_inference,[],[23,843,845,313,134,162,14,15,10])). % 75.94/76.23 cnf(859,plain, % 75.94/76.23 (P2(f9(a8,a1),a2)), % 75.94/76.23 inference(scs_inference,[],[23,222,14])). % 75.94/76.23 cnf(860,plain, % 75.94/76.23 (E(f9(x8601,x8602),f9(x8602,x8601))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(861,plain, % 75.94/76.23 (P2(a2,f9(a8,a1))), % 75.94/76.23 inference(scs_inference,[],[23,860,222,247,14,15])). % 75.94/76.23 cnf(877,plain, % 75.94/76.23 (E(f9(x8771,x8772),f9(x8772,x8771))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(878,plain, % 75.94/76.23 (P2(a2,f9(a8,f9(a2,a8)))), % 75.94/76.23 inference(scs_inference,[],[23,877,269,221,14,15])). % 75.94/76.23 cnf(911,plain, % 75.94/76.23 (E(f9(x9111,x9112),f9(x9112,x9111))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(912,plain, % 75.94/76.23 (P2(f9(a2,a8),f9(a8,a2))), % 75.94/76.23 inference(scs_inference,[],[23,911,473,535,14,15])). % 75.94/76.23 cnf(913,plain, % 75.94/76.23 (E(f9(x9131,x9132),f9(x9132,x9131))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(915,plain, % 75.94/76.23 (E(f9(x9151,x9152),f9(x9152,x9151))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(916,plain, % 75.94/76.23 (P1(f9(a1,a8),f9(a8,f9(a7,a8)))), % 75.94/76.23 inference(scs_inference,[],[23,911,913,915,355,336,473,535,14,15,10,11])). % 75.94/76.23 cnf(928,plain, % 75.94/76.23 (E(f9(x9281,x9282),f9(x9282,x9281))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(929,plain, % 75.94/76.23 (P2(f9(a1,a8),f9(a8,a2))), % 75.94/76.23 inference(scs_inference,[],[23,928,447,540,14,15])). % 75.94/76.23 cnf(970,plain, % 75.94/76.23 (P2(f9(a8,a1),f9(a2,a8))), % 75.94/76.23 inference(scs_inference,[],[23,540,14])). % 75.94/76.23 cnf(971,plain, % 75.94/76.23 (E(f9(x9711,x9712),f9(x9712,x9711))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(973,plain, % 75.94/76.23 (E(f9(x9731,x9732),f9(x9732,x9731))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(975,plain, % 75.94/76.23 (E(f9(x9751,x9752),f9(x9752,x9751))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.23 cnf(976,plain, % 75.94/76.23 (P1(a1,f9(a8,f9(a2,a8)))), % 75.94/76.23 inference(scs_inference,[],[23,971,973,975,225,336,540,469,14,15,10,11])). % 75.94/76.23 cnf(990,plain, % 75.94/76.23 (E(f9(x9901,x9902),f9(x9902,x9901))), % 75.94/76.23 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(991,plain, % 75.94/76.24 (P2(a2,f9(a8,f9(a1,a8)))), % 75.94/76.24 inference(scs_inference,[],[23,990,557,452,14,15])). % 75.94/76.24 cnf(1008,plain, % 75.94/76.24 (E(f9(x10081,x10082),f9(x10082,x10081))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1010,plain, % 75.94/76.24 (E(f9(x10101,x10102),f9(x10102,x10101))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1012,plain, % 75.94/76.24 (E(f9(x10121,x10122),f9(x10122,x10121))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1013,plain, % 75.94/76.24 (P1(f9(a6,a8),f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[23,1008,1010,1012,293,544,631,14,15,10,11])). % 75.94/76.24 cnf(1025,plain, % 75.94/76.24 (E(f9(x10251,x10252),f9(x10252,x10251))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1026,plain, % 75.94/76.24 (P2(f9(a8,a1),f9(f9(a2,a8),a8))), % 75.94/76.24 inference(scs_inference,[],[23,1025,586,15,14])). % 75.94/76.24 cnf(1042,plain, % 75.94/76.24 (E(f9(x10421,x10422),f9(x10422,x10421))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1044,plain, % 75.94/76.24 (E(f9(x10441,x10442),f9(x10442,x10441))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1045,plain, % 75.94/76.24 (P1(f9(a8,a6),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[23,1042,1044,544,562,14,15,10])). % 75.94/76.24 cnf(1046,plain, % 75.94/76.24 (E(f9(x10461,x10462),f9(x10462,x10461))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1047,plain, % 75.94/76.24 (P1(a1,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[23,1042,1044,1046,544,167,562,14,15,10,11])). % 75.94/76.24 cnf(1058,plain, % 75.94/76.24 (P2(f9(a2,a8),f9(a8,a1))), % 75.94/76.24 inference(scs_inference,[],[23,673,15])). % 75.94/76.24 cnf(1059,plain, % 75.94/76.24 (E(f9(x10591,x10592),f9(x10592,x10591))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1060,plain, % 75.94/76.24 (P2(f9(a8,a2),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[23,1059,673,15,14])). % 75.94/76.24 cnf(1102,plain, % 75.94/76.24 (E(f9(x11021,x11022),f9(x11022,x11021))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1104,plain, % 75.94/76.24 (E(f9(x11041,x11042),f9(x11042,x11041))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1106,plain, % 75.94/76.24 (E(f9(x11061,x11062),f9(x11062,x11061))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1107,plain, % 75.94/76.24 (P1(a2,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[23,1102,1104,1106,564,220,678,15,14,10,11])). % 75.94/76.24 cnf(1197,plain, % 75.94/76.24 (P2(f9(a8,a1),f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[23,970,15])). % 75.94/76.24 cnf(1198,plain, % 75.94/76.24 (E(f9(x11981,x11982),f9(x11982,x11981))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1200,plain, % 75.94/76.24 (E(f9(x12001,x12002),f9(x12002,x12001))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1201,plain, % 75.94/76.24 (P2(f9(a8,a2),f9(a8,a1))), % 75.94/76.24 inference(scs_inference,[],[23,1198,1200,287,970,1058,15,10,14])). % 75.94/76.24 cnf(1320,plain, % 75.94/76.24 (P1(f9(a8,a1),f9(a8,f9(a7,a8)))), % 75.94/76.24 inference(scs_inference,[],[23,916,10])). % 75.94/76.24 cnf(1321,plain, % 75.94/76.24 (E(f9(x13211,x13212),f9(x13212,x13211))), % 75.94/76.24 inference(rename_variables,[],[23])). % 75.94/76.24 cnf(1322,plain, % 75.94/76.24 (P1(f9(a8,a1),f9(a8,a7))), % 75.94/76.24 inference(scs_inference,[],[23,1321,916,846,10,11])). % 75.94/76.24 cnf(1335,plain, % 75.94/76.24 (P1(f9(a8,a6),f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[23,133,1107,1045,10,11])). % 75.94/76.24 cnf(1587,plain, % 75.94/76.24 (E(a1,f9(a8,a2))+P3(a1,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[1047,31])). % 75.94/76.24 cnf(1589,plain, % 75.94/76.24 (P3(a1,f9(a8,a2))+~E(f9(f9(a8,a2),a6),a1)), % 75.94/76.24 inference(scs_inference,[],[1047,315,31,3])). % 75.94/76.24 cnf(1593,plain, % 75.94/76.24 (E(f9(a8,a2),a1)+P3(a1,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[1047,315,31,3,26,2])). % 75.94/76.24 cnf(1623,plain, % 75.94/76.24 (E(a2,f9(a8,a2))+P3(a2,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[1107,31])). % 75.94/76.24 cnf(1629,plain, % 75.94/76.24 (E(f9(a8,a2),a2)+P3(a2,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[1107,315,31,3,26,2])). % 75.94/76.24 cnf(1717,plain, % 75.94/76.24 (P2(a2,f9(f9(a8,a2),a8))), % 75.94/76.24 inference(scs_inference,[],[133,809,15])). % 75.94/76.24 cnf(1718,plain, % 75.94/76.24 (E(x17181,f9(x17181,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1719,plain, % 75.94/76.24 (P2(f9(f9(a8,a2),a8),a2)), % 75.94/76.24 inference(scs_inference,[],[133,1718,809,825,15,14])). % 75.94/76.24 cnf(1720,plain, % 75.94/76.24 (E(x17201,f9(x17201,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1722,plain, % 75.94/76.24 (E(x17221,f9(x17221,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1725,plain, % 75.94/76.24 (~E(a10,f9(a5,a8))), % 75.94/76.24 inference(scs_inference,[],[24,133,1718,1720,1722,811,813,22,809,825,15,14,10,11,3])). % 75.94/76.24 cnf(1736,plain, % 75.94/76.24 (E(x17361,f9(x17361,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1737,plain, % 75.94/76.24 (P2(f9(f9(a8,a1),a8),a2)), % 75.94/76.24 inference(scs_inference,[],[133,1736,859,861,15,14])). % 75.94/76.24 cnf(1753,plain, % 75.94/76.24 (P2(f9(a2,a8),f9(f9(a8,a2),a8))), % 75.94/76.24 inference(scs_inference,[],[133,912,15])). % 75.94/76.24 cnf(1754,plain, % 75.94/76.24 (E(x17541,f9(x17541,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1755,plain, % 75.94/76.24 (P2(f9(f9(a8,a2),a8),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[133,1754,912,1060,15,14])). % 75.94/76.24 cnf(1772,plain, % 75.94/76.24 (E(x17721,f9(x17721,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1774,plain, % 75.94/76.24 (E(x17741,f9(x17741,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1776,plain, % 75.94/76.24 (E(x17761,f9(x17761,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1777,plain, % 75.94/76.24 (P1(f9(a6,a8),f9(f9(a8,a2),a8))), % 75.94/76.24 inference(scs_inference,[],[133,1772,1774,1776,1013,1322,929,1197,15,14,10,11])). % 75.94/76.24 cnf(1791,plain, % 75.94/76.24 (E(x17911,f9(x17911,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1792,plain, % 75.94/76.24 (P2(f9(f9(a8,a2),a8),f9(a8,a1))), % 75.94/76.24 inference(scs_inference,[],[133,1791,1201,15,14])). % 75.94/76.24 cnf(1870,plain, % 75.94/76.24 (E(x18701,f9(x18701,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1871,plain, % 75.94/76.24 (P2(f9(f9(a8,a2),a8),a1)), % 75.94/76.24 inference(scs_inference,[],[133,1870,807,844,15,14])). % 75.94/76.24 cnf(1922,plain, % 75.94/76.24 (E(x19221,f9(x19221,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1924,plain, % 75.94/76.24 (E(x19241,f9(x19241,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1926,plain, % 75.94/76.24 (E(x19261,f9(x19261,a8))), % 75.94/76.24 inference(rename_variables,[],[133])). % 75.94/76.24 cnf(1927,plain, % 75.94/76.24 (P1(f9(a8,a6),f9(f9(a8,a2),a8))), % 75.94/76.24 inference(scs_inference,[],[133,1922,1924,1926,1335,1320,970,1058,15,14,10,11])). % 75.94/76.24 cnf(2332,plain, % 75.94/76.24 (~E(x23321,f9(a6,x23321))), % 75.94/76.24 inference(scs_inference,[],[42,60,12])). % 75.94/76.24 cnf(2333,plain, % 75.94/76.24 (~P3(x23331,x23331)), % 75.94/76.24 inference(rename_variables,[],[42])). % 75.94/76.24 cnf(2334,plain, % 75.94/76.24 (~E(f9(a6,x23341),x23341)), % 75.94/76.24 inference(scs_inference,[],[42,2333,60,12,13])). % 75.94/76.24 cnf(2337,plain, % 75.94/76.24 (~E(x23371,f9(f9(a6,a6),x23371))), % 75.94/76.24 inference(scs_inference,[],[42,214,12])). % 75.94/76.24 cnf(2343,plain, % 75.94/76.24 (~P3(x23431,x23431)), % 75.94/76.24 inference(rename_variables,[],[42])). % 75.94/76.24 cnf(2346,plain, % 75.94/76.24 (~E(x23461,f9(f9(x23461,a8),a6))), % 75.94/76.24 inference(scs_inference,[],[42,2343,431,240,12,13,6])). % 75.94/76.24 cnf(2348,plain, % 75.94/76.24 (~E(f9(x23481,f9(a6,a6)),x23481)), % 75.94/76.24 inference(scs_inference,[],[42,110,13])). % 75.94/76.24 cnf(2372,plain, % 75.94/76.24 (~P3(f9(a6,a8),a8)), % 75.94/76.24 inference(scs_inference,[],[42,238,21,157,13,6,33])). % 75.94/76.24 cnf(2380,plain, % 75.94/76.24 (E(f4(f9(a1,x23801),x23802),f4(f9(a2,x23801),x23802))), % 75.94/76.24 inference(scs_inference,[],[16,8,6])). % 75.94/76.24 cnf(2383,plain, % 75.94/76.24 (E(f4(f9(a2,x23831),x23832),f4(f9(a1,x23831),x23832))), % 75.94/76.24 inference(scs_inference,[],[2380,26,2])). % 75.94/76.24 cnf(2409,plain, % 75.94/76.24 (~E(f9(x24091,f9(a8,a6)),x24091)), % 75.94/76.24 inference(scs_inference,[],[42,81,13])). % 75.94/76.24 cnf(2415,plain, % 75.94/76.24 (~P3(f9(a6,a8),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[42,238,201,85,13,6,33])). % 75.94/76.24 cnf(2418,plain, % 75.94/76.24 (~E(x24181,f9(f9(a6,a8),x24181))), % 75.94/76.24 inference(scs_inference,[],[42,262,238,201,130,85,13,6,33,12])). % 75.94/76.24 cnf(2434,plain, % 75.94/76.24 (~E(f9(a6,a1),a2)), % 75.94/76.24 inference(scs_inference,[],[46,60,13])). % 75.94/76.24 cnf(2465,plain, % 75.94/76.24 (P3(f9(a8,a8),f9(a6,a6))), % 75.94/76.24 inference(scs_inference,[],[133,63,12])). % 75.94/76.24 cnf(2467,plain, % 75.94/76.24 (P1(a2,a1)), % 75.94/76.24 inference(scs_inference,[],[48,133,41,63,12,11])). % 75.94/76.24 cnf(2471,plain, % 75.94/76.24 (~P3(f9(a6,a6),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[48,133,41,153,42,63,12,11,13,33])). % 75.94/76.24 cnf(2474,plain, % 75.94/76.24 (P3(a1,f9(a2,a6))), % 75.94/76.24 inference(scs_inference,[],[48,54,12])). % 75.94/76.24 cnf(2476,plain, % 75.94/76.24 (~P3(f9(a2,a6),a1)), % 75.94/76.24 inference(scs_inference,[],[48,42,54,12,33])). % 75.94/76.24 cnf(2480,plain, % 75.94/76.24 (P3(a1,f9(a6,a2))), % 75.94/76.24 inference(scs_inference,[],[48,60,12])). % 75.94/76.24 cnf(2482,plain, % 75.94/76.24 (~E(f9(a6,a2),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[48,153,60,12,13])). % 75.94/76.24 cnf(2484,plain, % 75.94/76.24 (~P3(f9(a6,a2),a1)), % 75.94/76.24 inference(scs_inference,[],[48,153,42,60,12,13,33])). % 75.94/76.24 cnf(2488,plain, % 75.94/76.24 (P3(f9(f9(a8,a8),a8),a6)), % 75.94/76.24 inference(scs_inference,[],[133,201,12])). % 75.94/76.24 cnf(2499,plain, % 75.94/76.24 (P3(f9(a8,a8),f9(f9(a6,a6),a6))), % 75.94/76.24 inference(scs_inference,[],[133,217,12])). % 75.94/76.24 cnf(2503,plain, % 75.94/76.24 (~P3(f9(f9(a6,a6),a6),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,217,12,13,33])). % 75.94/76.24 cnf(2507,plain, % 75.94/76.24 (P3(f9(a8,a8),f9(a6,f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,243,12])). % 75.94/76.24 cnf(2511,plain, % 75.94/76.24 (~P3(f9(a6,f9(a6,a6)),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,243,12,13,33])). % 75.94/76.24 cnf(2520,plain, % 75.94/76.24 (P3(f9(a8,a8),f9(f9(a6,a6),f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,394,12])). % 75.94/76.24 cnf(2524,plain, % 75.94/76.24 (~P3(f9(f9(a6,a6),f9(a6,a6)),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,394,12,13,33])). % 75.94/76.24 cnf(2528,plain, % 75.94/76.24 (P3(a1,f9(a2,f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[48,110,12])). % 75.94/76.24 cnf(2530,plain, % 75.94/76.24 (~E(f9(a2,f9(a6,a6)),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[48,153,110,12,13])). % 75.94/76.24 cnf(2535,plain, % 75.94/76.24 (P3(a1,f9(f9(a6,a6),a2))), % 75.94/76.24 inference(scs_inference,[],[48,214,12])). % 75.94/76.24 cnf(2537,plain, % 75.94/76.24 (~E(f9(f9(a6,a6),a2),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[48,153,214,12,13])). % 75.94/76.24 cnf(2543,plain, % 75.94/76.24 (P3(f9(a8,a8),f9(a6,f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[133,325,12])). % 75.94/76.24 cnf(2547,plain, % 75.94/76.24 (~P3(f9(a6,f9(a6,a8)),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,325,12,13,33])). % 75.94/76.24 cnf(2558,plain, % 75.94/76.24 (P3(a1,f9(a2,f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[48,130,12])). % 75.94/76.24 cnf(2560,plain, % 75.94/76.24 (~E(f9(a2,f9(a6,a8)),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[48,153,130,12,13])). % 75.94/76.24 cnf(2576,plain, % 75.94/76.24 (~P3(f9(f9(a6,a6),f9(a6,a8)),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,489,12,13,33])). % 75.94/76.24 cnf(2594,plain, % 75.94/76.24 (P3(f9(a8,a8),f9(f9(a6,a6),f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,559,12])). % 75.94/76.24 cnf(2598,plain, % 75.94/76.24 (~P3(f9(f9(a6,a6),f9(a8,a6)),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,559,12,13,33])). % 75.94/76.24 cnf(2606,plain, % 75.94/76.24 (~P3(f9(f9(a8,a6),f9(a6,a6)),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,615,12,13,33])). % 75.94/76.24 cnf(2613,plain, % 75.94/76.24 (~P3(f9(f9(a8,a6),a6),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,658,12,13,33])). % 75.94/76.24 cnf(2617,plain, % 75.94/76.24 (P3(a1,f9(a2,f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[48,81,12])). % 75.94/76.24 cnf(2619,plain, % 75.94/76.24 (~E(f9(a2,f9(a8,a6)),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[48,153,81,12,13])). % 75.94/76.24 cnf(2625,plain, % 75.94/76.24 (P3(a1,f9(a6,f9(a2,a6)))), % 75.94/76.24 inference(scs_inference,[],[48,183,12])). % 75.94/76.24 cnf(2627,plain, % 75.94/76.24 (~E(f9(a6,f9(a2,a6)),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[48,153,183,12,13])). % 75.94/76.24 cnf(2633,plain, % 75.94/76.24 (P3(a1,f9(f9(a6,a2),a6))), % 75.94/76.24 inference(scs_inference,[],[48,85,12])). % 75.94/76.24 cnf(2635,plain, % 75.94/76.24 (~E(f9(f9(a6,a2),a6),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[48,153,85,12,13])). % 75.94/76.24 cnf(2641,plain, % 75.94/76.24 (P3(a1,f9(f9(a2,a6),a8))), % 75.94/76.24 inference(scs_inference,[],[48,240,12])). % 75.94/76.24 cnf(2646,plain, % 75.94/76.24 (P3(a1,f9(f9(a8,a6),a2))), % 75.94/76.24 inference(scs_inference,[],[48,93,12])). % 75.94/76.24 cnf(2648,plain, % 75.94/76.24 (~E(f9(f9(a8,a6),a2),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[48,153,93,12,13])). % 75.94/76.24 cnf(2654,plain, % 75.94/76.24 (P3(f9(f9(a8,a8),a8),f9(a6,a6))), % 75.94/76.24 inference(scs_inference,[],[133,2465,12])). % 75.94/76.24 cnf(2659,plain, % 75.94/76.24 (P3(a1,f9(a8,a2))+E(f3(a1,x26591),f3(f9(a8,a2),x26591))), % 75.94/76.24 inference(scs_inference,[],[1587,4])). % 75.94/76.24 cnf(2676,plain, % 75.94/76.24 (P3(a2,f9(a8,a2))+E(f3(a2,x26761),f3(f9(a8,a2),x26761))), % 75.94/76.24 inference(scs_inference,[],[1623,4])). % 75.94/76.24 cnf(2687,plain, % 75.94/76.24 (E(f9(a8,a2),a2)), % 75.94/76.24 inference(scs_inference,[],[153,23,1629,13])). % 75.94/76.24 cnf(2688,plain, % 75.94/76.24 (~P3(f9(a8,a2),a2)), % 75.94/76.24 inference(scs_inference,[],[2687,26])). % 75.94/76.24 cnf(2690,plain, % 75.94/76.24 (E(a2,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[2687,26,2])). % 75.94/76.24 cnf(2693,plain, % 75.94/76.24 (~E(f9(a2,a6),f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[133,315,2687,2594,26,2,12,3])). % 75.94/76.24 cnf(2701,plain, % 75.94/76.24 (~P3(a2,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[2690,26])). % 75.94/76.24 cnf(2717,plain, % 75.94/76.24 (E(f3(a2,x27171),f3(f9(a8,a2),x27171))), % 75.94/76.24 inference(scs_inference,[],[2701,2676])). % 75.94/76.24 cnf(2719,plain, % 75.94/76.24 (~P3(f3(a2,x27191),f3(f9(a8,a2),x27191))), % 75.94/76.24 inference(scs_inference,[],[2717,26])). % 75.94/76.24 cnf(2721,plain, % 75.94/76.24 (E(f3(f9(a8,a2),x27211),f3(a2,x27211))), % 75.94/76.24 inference(scs_inference,[],[2717,26,2])). % 75.94/76.24 cnf(2729,plain, % 75.94/76.24 (~P3(f3(f9(a8,a2),x27291),f3(a2,x27291))), % 75.94/76.24 inference(scs_inference,[],[2721,26])). % 75.94/76.24 cnf(2731,plain, % 75.94/76.24 (P1(f9(a2,a8),a1)), % 75.94/76.24 inference(scs_inference,[],[133,2467,10])). % 75.94/76.24 cnf(2733,plain, % 75.94/76.24 (P1(f9(a2,a8),a2)), % 75.94/76.24 inference(scs_inference,[],[16,133,2467,10,11])). % 75.94/76.24 cnf(2734,plain, % 75.94/76.24 (P3(a2,f9(a1,a6))), % 75.94/76.24 inference(scs_inference,[],[16,133,2467,54,10,11,12])). % 75.94/76.24 cnf(2736,plain, % 75.94/76.24 (~P3(f9(a1,a6),a2)), % 75.94/76.24 inference(scs_inference,[],[16,133,42,2467,54,10,11,12,33])). % 75.94/76.24 cnf(2742,plain, % 75.94/76.24 (P1(f9(f9(a2,a8),a8),a2)), % 75.94/76.24 inference(scs_inference,[],[16,133,2731,10,11])). % 75.94/76.24 cnf(2743,plain, % 75.94/76.24 (P3(a2,f9(a6,a1))), % 75.94/76.24 inference(scs_inference,[],[16,133,2731,60,10,11,12])). % 75.94/76.24 cnf(2745,plain, % 75.94/76.24 (~E(f9(a6,a1),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,133,153,2731,60,10,11,12,13])). % 75.94/76.24 cnf(2747,plain, % 75.94/76.24 (~P3(f9(a6,a1),a2)), % 75.94/76.24 inference(scs_inference,[],[16,133,153,42,2731,60,10,11,12,13,33])). % 75.94/76.24 cnf(2762,plain, % 75.94/76.24 (P3(a2,f9(a1,f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[16,133,2742,110,11,12])). % 75.94/76.24 cnf(2764,plain, % 75.94/76.24 (~E(f9(a1,f9(a6,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,133,153,2742,110,11,12,13])). % 75.94/76.24 cnf(2766,plain, % 75.94/76.24 (~P3(f9(a1,f9(a6,a6)),a2)), % 75.94/76.24 inference(scs_inference,[],[16,133,153,42,2742,110,11,12,13,33])). % 75.94/76.24 cnf(2779,plain, % 75.94/76.24 (P3(a2,f9(f9(a6,a6),a1))), % 75.94/76.24 inference(scs_inference,[],[16,214,12])). % 75.94/76.24 cnf(2781,plain, % 75.94/76.24 (~E(f9(f9(a6,a6),a1),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,153,214,12,13])). % 75.94/76.24 cnf(2783,plain, % 75.94/76.24 (~P3(f9(f9(a6,a6),a1),a2)), % 75.94/76.24 inference(scs_inference,[],[16,153,42,214,12,13,33])). % 75.94/76.24 cnf(2804,plain, % 75.94/76.24 (P3(a2,f9(a1,f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[16,130,12])). % 75.94/76.24 cnf(2806,plain, % 75.94/76.24 (~E(f9(a1,f9(a6,a8)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,153,130,12,13])). % 75.94/76.24 cnf(2819,plain, % 75.94/76.24 (P3(a2,f9(a1,f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[16,81,12])). % 75.94/76.24 cnf(2821,plain, % 75.94/76.24 (~E(f9(a1,f9(a8,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,153,81,12,13])). % 75.94/76.24 cnf(2826,plain, % 75.94/76.24 (P3(a2,f9(a6,f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[16,183,12])). % 75.94/76.24 cnf(2828,plain, % 75.94/76.24 (~E(f9(a6,f9(a1,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,153,183,12,13])). % 75.94/76.24 cnf(2833,plain, % 75.94/76.24 (P3(a2,f9(f9(a6,a1),a6))), % 75.94/76.24 inference(scs_inference,[],[16,85,12])). % 75.94/76.24 cnf(2837,plain, % 75.94/76.24 (~P3(f9(f9(a6,a1),a6),a2)), % 75.94/76.24 inference(scs_inference,[],[16,153,42,85,12,13,33])). % 75.94/76.24 cnf(2840,plain, % 75.94/76.24 (P3(a2,f9(f9(a1,a6),a8))), % 75.94/76.24 inference(scs_inference,[],[16,240,12])). % 75.94/76.24 cnf(2842,plain, % 75.94/76.24 (~E(f9(f9(a1,a6),a8),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,153,240,12,13])). % 75.94/76.24 cnf(2844,plain, % 75.94/76.24 (P3(a2,f9(f9(a8,a6),a1))), % 75.94/76.24 inference(scs_inference,[],[16,93,12])). % 75.94/76.24 cnf(2846,plain, % 75.94/76.24 (~E(f9(f9(a8,a6),a1),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,153,93,12,13])). % 75.94/76.24 cnf(2851,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(a1,a6))), % 75.94/76.24 inference(scs_inference,[],[133,2734,12])). % 75.94/76.24 cnf(2855,plain, % 75.94/76.24 (~P3(f9(a1,a6),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,2734,12,13,33])). % 75.94/76.24 cnf(2858,plain, % 75.94/76.24 (P3(f9(f9(a2,a8),a8),f9(a1,a6))), % 75.94/76.24 inference(scs_inference,[],[133,2851,12])). % 75.94/76.24 cnf(2863,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(a6,a1))), % 75.94/76.24 inference(scs_inference,[],[133,2743,12])). % 75.94/76.24 cnf(2867,plain, % 75.94/76.24 (~P3(f9(a6,a1),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,2743,12,13,33])). % 75.94/76.24 cnf(2870,plain, % 75.94/76.24 (P3(f9(f9(a2,a8),a8),f9(a6,a1))), % 75.94/76.24 inference(scs_inference,[],[133,2863,12])). % 75.94/76.24 cnf(2872,plain, % 75.94/76.24 (~P3(f9(a6,a1),f9(f9(a2,a8),a8))), % 75.94/76.24 inference(scs_inference,[],[133,42,2863,12,33])). % 75.94/76.24 cnf(2875,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(a1,f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,2762,12])). % 75.94/76.24 cnf(2879,plain, % 75.94/76.24 (~P3(f9(a1,f9(a6,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,2762,12,13,33])). % 75.94/76.24 cnf(2887,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a6,a6),a1))), % 75.94/76.24 inference(scs_inference,[],[133,2779,12])). % 75.94/76.24 cnf(2891,plain, % 75.94/76.24 (~P3(f9(f9(a6,a6),a1),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,2779,12,13,33])). % 75.94/76.24 cnf(2904,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(a1,f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[133,2804,12])). % 75.94/76.24 cnf(2908,plain, % 75.94/76.24 (~P3(f9(a1,f9(a6,a8)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,2804,12,13,33])). % 75.94/76.24 cnf(2922,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(a1,f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,2819,12])). % 75.94/76.24 cnf(2926,plain, % 75.94/76.24 (~P3(f9(a1,f9(a8,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,2819,12,13,33])). % 75.94/76.24 cnf(2934,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(a6,f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,2826,12])). % 75.94/76.24 cnf(2938,plain, % 75.94/76.24 (~P3(f9(a6,f9(a1,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,2826,12,13,33])). % 75.94/76.24 cnf(2946,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a1,a6),a8))), % 75.94/76.24 inference(scs_inference,[],[133,2840,12])). % 75.94/76.24 cnf(2952,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a6,a1),a6))), % 75.94/76.24 inference(scs_inference,[],[133,2833,12])). % 75.94/76.24 cnf(2964,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a8,a6),a1))), % 75.94/76.24 inference(scs_inference,[],[133,2844,12])). % 75.94/76.24 cnf(2968,plain, % 75.94/76.24 (~P3(f9(f9(a8,a6),a1),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,2844,12,13,33])). % 75.94/76.24 cnf(2978,plain, % 75.94/76.24 (P3(x29781,f9(f9(x29781,a6),f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,110,33])). % 75.94/76.24 cnf(2980,plain, % 75.94/76.24 (~P3(x29801,x29802)+~P3(x29803,x29801)+P3(x29803,x29802)), % 75.94/76.24 inference(rename_variables,[],[33])). % 75.94/76.24 cnf(2981,plain, % 75.94/76.24 (P3(a2,f9(f9(a1,a6),f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,16,110,33,12])). % 75.94/76.24 cnf(2984,plain, % 75.94/76.24 (~P3(f9(a1,a6),a1)), % 75.94/76.24 inference(scs_inference,[],[54,16,153,42,110,33,12,13,2980])). % 75.94/76.24 cnf(3001,plain, % 75.94/76.24 (P3(x30011,f9(f9(a6,a6),f9(x30011,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,214,33])). % 75.94/76.24 cnf(3004,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a1,a6),f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,133,214,2981,33,12])). % 75.94/76.24 cnf(3008,plain, % 75.94/76.24 (P3(x30081,f9(f9(f9(x30081,a6),f9(a6,a6)),f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[54,157,33])). % 75.94/76.24 cnf(3011,plain, % 75.94/76.24 (P3(f9(f9(a2,a8),a8),f9(f9(a1,a6),f9(a6,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,133,157,3004,33,12])). % 75.94/76.24 cnf(3015,plain, % 75.94/76.24 (P3(x30151,f9(f9(x30151,a6),f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[54,130,33])). % 75.94/76.24 cnf(3018,plain, % 75.94/76.24 (P3(a2,f9(f9(f9(a1,a6),f9(a6,a6)),f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[54,16,130,3008,33,12])). % 75.94/76.24 cnf(3022,plain, % 75.94/76.24 (P3(x30221,f9(f9(f9(a8,a6),f9(x30221,a6)),f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,113,33])). % 75.94/76.24 cnf(3025,plain, % 75.94/76.24 (P3(a2,f9(f9(a6,a6),f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,16,113,3001,33,12])). % 75.94/76.24 cnf(3026,plain, % 75.94/76.24 (P3(x30261,f9(f9(a6,a6),f9(x30261,a6)))), % 75.94/76.24 inference(rename_variables,[],[3001])). % 75.94/76.24 cnf(3027,plain, % 75.94/76.24 (~E(f9(f9(a6,a6),f9(x30271,a6)),f9(x30271,a8))), % 75.94/76.24 inference(scs_inference,[],[54,16,153,113,3001,3026,33,12,13])). % 75.94/76.24 cnf(3029,plain, % 75.94/76.24 (P3(x30291,f9(f9(x30291,a6),f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,81,33])). % 75.94/76.24 cnf(3032,plain, % 75.94/76.24 (P3(a2,f9(f9(f9(a8,a6),f9(a1,a6)),f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,16,81,3022,33,12])). % 75.94/76.24 cnf(3036,plain, % 75.94/76.24 (P3(x30361,f9(f9(a8,a6),f9(x30361,a6)))), % 75.94/76.24 inference(scs_inference,[],[54,93,33])). % 75.94/76.24 cnf(3039,plain, % 75.94/76.24 (P3(a2,f9(f9(a1,a6),f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[54,16,93,3015,33,12])). % 75.94/76.24 cnf(3040,plain, % 75.94/76.24 (P3(x30401,f9(f9(x30401,a6),f9(a6,a8)))), % 75.94/76.24 inference(rename_variables,[],[3015])). % 75.94/76.24 cnf(3041,plain, % 75.94/76.24 (~E(f9(f9(x30411,a6),f9(a6,a8)),f9(x30411,a8))), % 75.94/76.24 inference(scs_inference,[],[54,16,153,93,3015,3040,33,12,13])). % 75.94/76.24 cnf(3046,plain, % 75.94/76.24 (P3(a2,f9(f9(a1,a6),f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[16,42,3011,3029,33,12])). % 75.94/76.24 cnf(3053,plain, % 75.94/76.24 (P3(a2,f9(f9(a8,a6),f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[16,42,3036,3018,33,12])). % 75.94/76.24 cnf(3060,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a6,a6),f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3025,33,12])). % 75.94/76.24 cnf(3062,plain, % 75.94/76.24 (~E(f9(f9(a6,a6),f9(a1,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,3025,33,12,13])). % 75.94/76.24 cnf(3064,plain, % 75.94/76.24 (~P3(f9(f9(a6,a6),f9(a1,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[42,3060,33])). % 75.94/76.24 cnf(3067,plain, % 75.94/76.24 (P3(f9(f9(a2,a8),a8),f9(f9(a6,a6),f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3060,33,12])). % 75.94/76.24 cnf(3074,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(f9(a8,a6),f9(a1,a6)),f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3067,3032,33,12])). % 75.94/76.24 cnf(3081,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a1,a6),f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3074,3039,33,12])). % 75.94/76.24 cnf(3083,plain, % 75.94/76.24 (~E(f9(f9(a1,a6),f9(a6,a8)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,3074,3039,33,12,13])). % 75.94/76.24 cnf(3086,plain, % 75.94/76.24 (~P3(f9(f9(a1,a6),f9(a6,a8)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[42,3081,33])). % 75.94/76.24 cnf(3089,plain, % 75.94/76.24 (P3(f9(f9(a2,a8),a8),f9(f9(a1,a6),f9(a6,a8)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3081,33,12])). % 75.94/76.24 cnf(3096,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a1,a6),f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3089,3046,33,12])). % 75.94/76.24 cnf(3098,plain, % 75.94/76.24 (~E(f9(f9(a1,a6),f9(a8,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,3089,3046,33,12,13])). % 75.94/76.24 cnf(3100,plain, % 75.94/76.24 (~P3(f9(f9(a1,a6),f9(a8,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[42,3096,33])). % 75.94/76.24 cnf(3103,plain, % 75.94/76.24 (P3(f9(f9(a2,a8),a8),f9(f9(a1,a6),f9(a8,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3096,33,12])). % 75.94/76.24 cnf(3110,plain, % 75.94/76.24 (P3(f9(a2,a8),f9(f9(a8,a6),f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3103,3053,33,12])). % 75.94/76.24 cnf(3112,plain, % 75.94/76.24 (~E(f9(f9(a8,a6),f9(a1,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,3103,3053,33,12,13])). % 75.94/76.24 cnf(3114,plain, % 75.94/76.24 (~P3(f9(f9(a8,a6),f9(a1,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[42,3110,33])). % 75.94/76.24 cnf(3117,plain, % 75.94/76.24 (P3(f9(f9(a2,a8),a8),f9(f9(a8,a6),f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[133,42,3110,33,12])). % 75.94/76.24 cnf(3126,plain, % 75.94/76.24 (~E(f9(f9(a1,a6),f9(a6,a6)),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[133,153,42,3117,2981,3018,33,12,13])). % 75.94/76.24 cnf(3191,plain, % 75.94/76.24 (E(f3(a1,x31911),f3(a2,x31911))), % 75.94/76.24 inference(scs_inference,[],[16,2654,21,34,35,4])). % 75.94/76.24 cnf(3192,plain, % 75.94/76.24 (E(f3(x31921,a1),f3(x31921,a2))), % 75.94/76.24 inference(scs_inference,[],[16,2654,21,34,35,4,5])). % 75.94/76.24 cnf(3193,plain, % 75.94/76.24 (E(f4(a1,x31931),f4(a2,x31931))), % 75.94/76.24 inference(scs_inference,[],[16,2654,21,34,35,4,5,8])). % 75.94/76.24 cnf(3194,plain, % 75.94/76.24 (E(f4(x31941,a1),f4(x31941,a2))), % 75.94/76.24 inference(scs_inference,[],[16,2654,21,34,35,4,5,8,9])). % 75.94/76.24 cnf(3198,plain, % 75.94/76.24 (P3(a8,f9(f9(a2,a8),a8))), % 75.94/76.24 inference(scs_inference,[],[16,2654,772,3001,21,34,35,4,5,8,9,28,29])). % 75.94/76.24 cnf(3202,plain, % 75.94/76.24 (E(f9(x32021,a1),f9(x32021,a2))), % 75.94/76.24 inference(scs_inference,[],[16,2654,772,3001,2383,21,34,35,4,5,8,9,28,29,25,7])). % 75.94/76.24 cnf(3203,plain, % 75.94/76.24 (P1(a8,a6)), % 75.94/76.24 inference(scs_inference,[],[16,52,2654,772,3001,2383,21,34,35,4,5,8,9,28,29,25,7,27])). % 75.94/76.24 cnf(3207,plain, % 75.94/76.24 (E(f9(a1,x32071),f9(a2,x32071))), % 75.94/76.24 inference(scs_inference,[],[16,52,2654,772,3001,2383,21,34,35,4,5,8,9,28,29,25,7,27,30,6])). % 75.94/76.24 cnf(3210,plain, % 75.94/76.24 (~E(a8,a1)), % 75.94/76.24 inference(scs_inference,[],[16,52,59,2654,772,3001,2383,21,34,35,4,5,8,9,28,29,25,7,27,30,6,26,2])). % 75.94/76.24 cnf(3214,plain, % 75.94/76.24 (~P1(f9(a6,a8),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[16,52,59,2654,178,772,3001,2383,262,22,21,34,35,4,5,8,9,28,29,25,7,27,30,6,26,2,33,10])). % 75.94/76.24 cnf(3215,plain, % 75.94/76.24 (E(f9(x32151,a8),x32151)), % 75.94/76.24 inference(rename_variables,[],[22])). % 75.94/76.24 cnf(3216,plain, % 75.94/76.24 (~P1(f9(a6,a6),a8)), % 75.94/76.24 inference(scs_inference,[],[16,52,59,136,294,2654,178,772,3001,2383,262,22,21,34,35,4,5,8,9,28,29,25,7,27,30,6,26,2,33,10,31])). % 75.94/76.24 cnf(3222,plain, % 75.94/76.24 (~P3(f3(f9(a8,a2),a1),f9(a5,a8))), % 75.94/76.24 inference(scs_inference,[],[16,52,59,136,294,716,2654,140,178,772,3001,2383,2721,714,262,22,3215,21,34,35,4,5,8,9,28,29,25,7,27,30,6,26,2,33,10,31,11,3,12])). % 75.94/76.24 cnf(3223,plain, % 75.94/76.24 (E(f3(f9(a8,a2),x32231),f3(a2,x32231))), % 75.94/76.24 inference(rename_variables,[],[2721])). % 75.94/76.24 cnf(3224,plain, % 75.94/76.24 (~P3(f9(a5,a8),f3(f9(a8,a2),a1))), % 75.94/76.24 inference(scs_inference,[],[16,52,59,136,294,716,720,2654,140,178,772,3001,2383,2721,3223,714,262,22,3215,21,34,35,4,5,8,9,28,29,25,7,27,30,6,26,2,33,10,31,11,3,12,13])). % 75.94/76.24 cnf(3226,plain, % 75.94/76.24 (E(f3(f9(a2,a8),f9(a2,a8)),a10)), % 75.94/76.24 inference(scs_inference,[],[16,52,59,136,294,716,720,2733,2654,140,1719,178,772,3001,2383,2721,3223,714,262,759,22,3215,21,34,35,4,5,8,9,28,29,25,7,27,30,6,26,2,33,10,31,11,3,12,13,36])). % 75.94/76.24 cnf(3234,plain, % 75.94/76.24 (P3(a8,f4(a1,f9(a2,a6)))), % 75.94/76.24 inference(scs_inference,[],[2474,34])). % 75.94/76.24 cnf(3238,plain, % 75.94/76.24 (E(f3(a1,x32381),f3(f9(a2,a8),x32381))), % 75.94/76.24 inference(scs_inference,[],[2474,680,34,9,8,4])). % 75.94/76.24 cnf(3239,plain, % 75.94/76.24 (E(f3(x32391,a1),f3(x32391,f9(a2,a8)))), % 75.94/76.24 inference(scs_inference,[],[2474,680,34,9,8,4,5])). % 75.94/76.24 cnf(3243,plain, % 75.94/76.24 (P1(f3(a1,x32431),f3(a2,x32431))), % 75.94/76.24 inference(scs_inference,[],[3191,2474,3036,680,34,9,8,4,5,28,25])). % 75.94/76.24 cnf(3245,plain, % 75.94/76.24 (P3(a8,f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[3191,2474,3036,680,759,34,9,8,4,5,28,25,29])). % 75.94/76.24 cnf(3247,plain, % 75.94/76.24 (E(f9(x32471,a1),f9(x32471,f9(a2,a8)))), % 75.94/76.24 inference(scs_inference,[],[3191,2474,3036,680,759,34,9,8,4,5,28,25,29,7])). % 75.94/76.24 cnf(3252,plain, % 75.94/76.24 (E(f9(a1,x32521),f9(f9(a2,a8),x32521))), % 75.94/76.24 inference(scs_inference,[],[203,3191,2858,2474,3036,680,759,34,9,8,4,5,28,25,29,7,27,30,6])). % 75.94/76.24 cnf(3255,plain, % 75.94/76.24 (~E(a8,a2)), % 75.94/76.24 inference(scs_inference,[],[747,203,3191,2858,2474,3036,680,759,34,9,8,4,5,28,25,29,7,27,30,6,26,2])). % 75.94/76.24 cnf(3256,plain, % 75.94/76.24 (~P3(f9(a1,a6),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[747,203,212,3191,2858,2474,2734,3036,680,759,34,9,8,4,5,28,25,29,7,27,30,6,26,2,33])). % 75.94/76.24 cnf(3259,plain, % 75.94/76.24 (P1(x32591,x32591)), % 75.94/76.24 inference(rename_variables,[],[41])). % 75.94/76.24 cnf(3260,plain, % 75.94/76.24 (~P1(f9(a6,a6),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[747,203,212,229,2471,3191,2858,2474,2734,3036,680,41,759,34,9,8,4,5,28,25,29,7,27,30,6,26,2,33,10,31])). % 75.94/76.24 cnf(3262,plain, % 75.94/76.24 (P1(f3(x32621,a1),f3(x32621,a2))), % 75.94/76.24 inference(scs_inference,[],[747,203,212,229,2471,3191,3192,2858,2474,2734,3036,680,41,3259,759,34,9,8,4,5,28,25,29,7,27,30,6,26,2,33,10,31,11])). % 75.94/76.24 cnf(3264,plain, % 75.94/76.24 (~E(f9(a8,a2),a8)), % 75.94/76.24 inference(scs_inference,[],[747,203,212,229,2471,3191,3192,2858,2474,2734,3036,680,2690,41,3259,759,34,9,8,4,5,28,25,29,7,27,30,6,26,2,33,10,31,11,3])). % 75.94/76.24 cnf(3265,plain, % 75.94/76.24 (~P3(f3(a1,x32651),f3(f9(a8,a2),x32651))), % 75.94/76.24 inference(scs_inference,[],[747,203,212,229,2471,3191,3192,2858,2719,2474,2734,3036,680,2690,41,3259,759,34,9,8,4,5,28,25,29,7,27,30,6,26,2,33,10,31,11,3,12])). % 75.94/76.24 cnf(3268,plain, % 75.94/76.24 (E(f3(a2,a2),a10)), % 75.94/76.24 inference(scs_inference,[],[16,747,203,212,229,2471,2688,3191,3192,2858,2719,2474,1871,2734,3036,2467,680,2690,41,3259,759,745,34,9,8,4,5,28,25,29,7,27,30,6,26,2,33,10,31,11,3,12,13,36])). % 75.94/76.24 cnf(3274,plain, % 75.94/76.24 (P3(a8,f4(a8,f9(a2,a8)))), % 75.94/76.24 inference(scs_inference,[],[3245,34])). % 75.94/76.24 cnf(3281,plain, % 75.94/76.24 (E(f3(f3(a2,a2),x32811),f3(a10,x32811))), % 75.94/76.24 inference(scs_inference,[],[3245,3268,3234,34,9,8,28,5,4])). % 75.94/76.24 cnf(3282,plain, % 75.94/76.24 (P1(f4(a1,x32821),f4(a2,x32821))), % 75.94/76.24 inference(scs_inference,[],[3245,3193,3268,3234,34,9,8,28,5,4,25])). % 75.94/76.24 cnf(3284,plain, % 75.94/76.24 (P3(a8,a2)), % 75.94/76.24 inference(scs_inference,[],[3245,3193,3268,3234,745,34,9,8,28,5,4,25,29])). % 75.94/76.24 cnf(3292,plain, % 75.94/76.24 (~E(a8,f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[2415,3245,3193,3268,3234,745,34,9,8,28,5,4,25,29,27,7,30,6,26])). % 75.94/76.24 cnf(3294,plain, % 75.94/76.24 (~E(a1,f9(a2,a6))), % 75.94/76.24 inference(scs_inference,[],[332,2415,3245,3193,3268,3234,745,34,9,8,28,5,4,25,29,27,7,30,6,26,2])). % 75.94/76.24 cnf(3299,plain, % 75.94/76.24 (~P3(f9(a2,a8),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[332,682,2415,3245,3193,3268,3234,3203,745,153,34,9,8,28,5,4,25,29,27,7,30,6,26,2,38,32,33])). % 75.94/76.24 cnf(3302,plain, % 75.94/76.24 (~P1(f9(f9(a6,a8),a8),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[332,682,2415,3214,3245,3193,3268,3234,3203,745,22,153,34,9,8,28,5,4,25,29,27,7,30,6,26,2,38,32,33,10])). % 75.94/76.24 cnf(3303,plain, % 75.94/76.24 (E(f9(x33031,a8),x33031)), % 75.94/76.24 inference(rename_variables,[],[22])). % 75.94/76.24 cnf(3304,plain, % 75.94/76.24 (~P1(f9(a2,a6),a1)), % 75.94/76.24 inference(scs_inference,[],[332,682,2415,2476,3214,3245,3193,3268,3234,3203,745,22,153,34,9,8,28,5,4,25,29,27,7,30,6,26,2,38,32,33,10,31])). % 75.94/76.24 cnf(3307,plain, % 75.94/76.24 (E(f9(x33071,a8),x33071)), % 75.94/76.24 inference(rename_variables,[],[22])). % 75.94/76.24 cnf(3308,plain, % 75.94/76.24 (~E(a2,f9(a6,a1))), % 75.94/76.24 inference(scs_inference,[],[16,332,682,2415,2476,3214,3245,3193,3268,3234,2332,3203,745,22,3303,153,34,9,8,28,5,4,25,29,27,7,30,6,26,2,38,32,33,10,31,11,3])). % 75.94/76.24 cnf(3310,plain, % 75.94/76.24 (~P3(f9(f9(a6,a8),a8),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[16,332,682,2415,2476,3214,3245,3193,3268,3234,2332,3203,745,22,3303,3307,153,34,9,8,28,5,4,25,29,27,7,30,6,26,2,38,32,33,10,31,11,3,12])). % 75.94/76.24 cnf(3311,plain, % 75.94/76.24 (E(f9(x33111,a8),x33111)), % 75.94/76.24 inference(rename_variables,[],[22])). % 75.94/76.24 cnf(3316,plain, % 75.94/76.24 (~E(a6,f9(a2,a6))), % 75.94/76.24 inference(scs_inference,[],[16,332,682,2415,2476,3214,3245,3193,3268,3234,2332,3203,745,22,3303,3307,3311,153,34,9,8,28,5,4,25,29,27,7,30,6,26,2,38,32,33,10,31,11,3,12,13,35,100])). % 75.94/76.24 cnf(3319,plain, % 75.94/76.24 (P3(a8,f4(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[3284,34])). % 75.94/76.24 cnf(3327,plain, % 75.94/76.24 (P1(f4(x33271,a1),f4(x33271,a2))), % 75.94/76.24 inference(scs_inference,[],[3284,3194,3274,84,34,28,9,8,5,4,25])). % 75.94/76.24 cnf(3329,plain, % 75.94/76.24 (P3(a8,a1)), % 75.94/76.24 inference(scs_inference,[],[3284,3194,3274,84,18,34,28,9,8,5,4,25,29])). % 75.94/76.24 cnf(3331,plain, % 75.94/76.24 (P1(a1,f9(a6,a2))), % 75.94/76.24 inference(scs_inference,[],[3284,2484,3194,3274,84,18,34,28,9,8,5,4,25,29,27])). % 75.94/76.24 cnf(3333,plain, % 75.94/76.24 (E(f9(x33331,a5),f9(x33331,f3(a2,a1)))), % 75.94/76.24 inference(scs_inference,[],[3284,2484,3194,3274,84,18,34,28,9,8,5,4,25,29,27,7])). % 75.94/76.24 cnf(3334,plain, % 75.94/76.24 (P1(a8,a2)), % 75.94/76.24 inference(scs_inference,[],[3284,2484,3194,3274,84,18,34,28,9,8,5,4,25,29,27,7,30])). % 75.94/76.24 cnf(3336,plain, % 75.94/76.24 (E(f9(a5,x33361),f9(f3(a2,a1),x33361))), % 75.94/76.24 inference(scs_inference,[],[3284,2484,3194,3274,84,18,34,28,9,8,5,4,25,29,27,7,30,6])). % 75.94/76.24 cnf(3339,plain, % 75.94/76.24 (~E(f3(a2,a1),f9(a5,a6))), % 75.94/76.24 inference(scs_inference,[],[3284,351,2484,3194,2870,3274,84,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2])). % 75.94/76.24 cnf(3342,plain, % 75.94/76.24 (~P3(f9(a6,a1),f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[3284,351,699,2484,2701,3194,2870,3274,2743,84,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33])). % 75.94/76.24 cnf(3344,plain, % 75.94/76.24 (P1(f4(a1,a2),f4(a2,a1))), % 75.94/76.24 inference(scs_inference,[],[3284,351,699,2484,2701,3194,3282,2870,3274,2743,84,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10])). % 75.94/76.24 cnf(3345,plain, % 75.94/76.24 (E(f4(x33451,a1),f4(x33451,a2))), % 75.94/76.24 inference(rename_variables,[],[3194])). % 75.94/76.24 cnf(3346,plain, % 75.94/76.24 (P1(f4(a1,x33461),f4(a2,x33461))), % 75.94/76.24 inference(rename_variables,[],[3282])). % 75.94/76.24 cnf(3347,plain, % 75.94/76.24 (~P1(f9(a1,a6),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[3284,351,699,727,2484,2701,2855,3194,3282,2870,3274,2743,84,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31])). % 75.94/76.24 cnf(3349,plain, % 75.94/76.24 (P1(f4(a1,a1),f4(a2,a2))), % 75.94/76.24 inference(scs_inference,[],[3284,351,699,727,2484,2701,2855,3194,3345,3282,3346,2870,3274,2743,84,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31,11])). % 75.94/76.24 cnf(3350,plain, % 75.94/76.24 (E(f4(x33501,a1),f4(x33501,a2))), % 75.94/76.24 inference(rename_variables,[],[3194])). % 75.94/76.24 cnf(3352,plain, % 75.94/76.24 (~E(f9(a8,a8),a2)), % 75.94/76.24 inference(scs_inference,[],[3284,3255,351,699,727,2484,2701,2855,3194,3345,3282,3346,2870,3274,2743,84,133,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31,11,3])). % 75.94/76.24 cnf(3354,plain, % 75.94/76.24 (~P3(a1,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[16,3284,3255,351,699,727,2484,2701,2855,3194,3345,3282,3346,2870,3274,2743,84,133,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31,11,3,12])). % 75.94/76.24 cnf(3355,plain, % 75.94/76.24 (~P3(f9(f4(x33551,a2),a8),f4(x33551,a1))), % 75.94/76.24 inference(scs_inference,[],[16,3284,3255,351,699,727,2484,2701,2855,3194,3345,3350,3282,3346,2870,3274,2743,84,238,133,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31,11,3,12,13])). % 75.94/76.24 cnf(3357,plain, % 75.94/76.24 (E(a1,f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[16,3284,3255,351,699,727,2484,2701,2855,3194,3345,3350,3282,3346,2870,3274,2743,84,238,133,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31,11,3,12,13,1587])). % 75.94/76.24 cnf(3358,plain, % 75.94/76.24 (E(f9(a8,a2),a1)), % 75.94/76.24 inference(scs_inference,[],[16,3284,3255,351,699,727,2484,2701,2855,3194,3345,3350,3282,3346,2870,3274,2743,84,238,133,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31,11,3,12,13,1587,1593])). % 75.94/76.24 cnf(3360,plain, % 75.94/76.24 (E(f3(a1,x33601),f3(f9(a8,a2),x33601))), % 75.94/76.24 inference(scs_inference,[],[16,3284,3255,351,699,727,2484,2701,2855,3194,3345,3350,3282,3346,2870,3274,2743,84,238,133,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31,11,3,12,13,1587,1593,1589,2659])). % 75.94/76.24 cnf(3361,plain, % 75.94/76.24 (E(f9(a8,f4(a8,a1)),a1)), % 75.94/76.24 inference(scs_inference,[],[16,3284,3255,351,699,727,2484,2701,2855,3194,3345,3350,3282,3346,2870,3274,2743,84,238,133,18,34,28,9,8,5,4,25,29,27,7,30,6,26,2,32,33,10,31,11,3,12,13,1587,1593,1589,2659,35])). % 75.94/76.24 cnf(3368,plain, % 75.94/76.24 (P3(a8,f4(a8,a1))), % 75.94/76.24 inference(scs_inference,[],[3329,34])). % 75.94/76.24 cnf(3372,plain, % 75.94/76.24 (E(f3(f9(a8,a2),x33721),f3(a1,x33721))), % 75.94/76.24 inference(scs_inference,[],[3329,3358,3319,34,28,4])). % 75.94/76.24 cnf(3373,plain, % 75.94/76.24 (E(f4(x33731,a1),f4(x33731,f9(a8,a2)))), % 75.94/76.24 inference(scs_inference,[],[3329,3357,3358,3319,34,28,4,9])). % 75.94/76.24 cnf(3374,plain, % 75.94/76.24 (E(f3(x33741,a1),f3(x33741,f9(a8,a2)))), % 75.94/76.24 inference(scs_inference,[],[3329,3357,3358,3319,34,28,4,9,5])). % 75.94/76.24 cnf(3375,plain, % 75.94/76.24 (E(f4(a1,x33751),f4(f9(a8,a2),x33751))), % 75.94/76.24 inference(scs_inference,[],[3329,3357,3358,3319,34,28,4,9,5,8])). % 75.94/76.24 cnf(3380,plain, % 75.94/76.24 (P1(a8,a1)), % 75.94/76.24 inference(scs_inference,[],[3329,3256,3357,3202,3358,3319,34,28,4,9,5,8,25,27,30])). % 75.94/76.24 cnf(3382,plain, % 75.94/76.24 (E(f9(x33821,a1),f9(x33821,f9(a8,a2)))), % 75.94/76.24 inference(scs_inference,[],[3329,3256,3357,3202,3358,3319,34,28,4,9,5,8,25,27,30,7])). % 75.94/76.24 cnf(3384,plain, % 75.94/76.24 (~E(a8,f4(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[3329,3256,3357,3202,3358,3319,34,28,4,9,5,8,25,27,30,7,6,26])). % 75.94/76.24 cnf(3386,plain, % 75.94/76.24 (~E(f9(a1,a8),f9(a2,a6))), % 75.94/76.24 inference(scs_inference,[],[3329,420,3256,3357,3202,3358,3319,34,28,4,9,5,8,25,27,30,7,6,26,2])). % 75.94/76.24 cnf(3391,plain, % 75.94/76.24 (~P3(a1,f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[3329,3334,420,3256,3357,3202,3358,3319,153,34,28,4,9,5,8,25,27,30,7,6,26,2,38,32,33])). % 75.94/76.24 cnf(3394,plain, % 75.94/76.24 (~P1(f9(f9(a6,a6),a8),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[3329,3334,420,3256,3260,3357,3202,3358,3319,22,153,34,28,4,9,5,8,25,27,30,7,6,26,2,38,32,33,10])). % 75.94/76.24 cnf(3395,plain, % 75.94/76.24 (E(f9(x33951,a8),x33951)), % 75.94/76.24 inference(rename_variables,[],[22])). % 75.94/76.24 cnf(3396,plain, % 75.94/76.24 (~P1(f9(a1,a6),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[3329,3334,420,3256,3260,3357,3202,3358,3319,195,22,153,34,28,4,9,5,8,25,27,30,7,6,26,2,38,32,33,10,31])). % 75.94/76.24 cnf(3400,plain, % 75.94/76.24 (E(f9(x34001,a8),x34001)), % 75.94/76.24 inference(rename_variables,[],[22])). % 75.94/76.24 cnf(3401,plain, % 75.94/76.24 (~E(f9(a8,a2),f9(a2,a6))), % 75.94/76.24 inference(scs_inference,[],[3329,3334,420,3256,3260,3357,3202,3358,3294,3319,195,22,3395,153,34,28,4,9,5,8,25,27,30,7,6,26,2,38,32,33,10,31,11,3])). % 75.94/76.24 cnf(3402,plain, % 75.94/76.24 (~P3(f9(f9(a1,a6),a8),f9(a1,a8))), % 75.94/76.24 inference(scs_inference,[],[3329,3334,420,3256,3260,3357,3202,3358,3294,3319,195,22,3395,3400,153,34,28,4,9,5,8,25,27,30,7,6,26,2,38,32,33,10,31,11,3,12])). % 75.94/76.24 cnf(3411,plain, % 75.94/76.24 (P3(a8,f4(a8,f4(a8,a1)))), % 75.94/76.24 inference(scs_inference,[],[3368,34])). % 75.94/76.24 cnf(3417,plain, % 75.94/76.24 (E(f3(x34171,f9(a8,a2)),f3(x34171,a1))), % 75.94/76.24 inference(scs_inference,[],[3368,3372,3358,34,28,25,5])). % 75.94/76.24 cnf(3418,plain, % 75.94/76.24 (E(f4(f9(a8,a2),x34181),f4(a1,x34181))), % 75.94/76.24 inference(scs_inference,[],[3368,3372,3358,34,28,25,5,8])). % 75.94/76.24 cnf(3419,plain, % 75.94/76.24 (E(f3(f9(a2,a8),x34191),f3(a1,x34191))), % 75.94/76.24 inference(scs_inference,[],[3368,3372,3358,684,34,28,25,5,8,4])). % 75.94/76.24 cnf(3422,plain, % 75.94/76.24 (E(f4(x34221,f9(a8,a2)),f4(x34221,a1))), % 75.94/76.24 inference(scs_inference,[],[3342,3368,3372,3358,684,34,28,25,5,8,4,27,9])). % 75.94/76.24 cnf(3425,plain, % 75.94/76.24 (E(f9(x34251,f9(a8,a2)),f9(x34251,a1))), % 75.94/76.24 inference(scs_inference,[],[3342,3368,3372,3358,684,34,28,25,5,8,4,27,9,30,7])). % 75.94/76.24 cnf(3426,plain, % 75.94/76.24 (E(f9(f9(a8,a2),x34261),f9(a1,x34261))), % 75.94/76.24 inference(scs_inference,[],[3342,3368,3372,3358,684,34,28,25,5,8,4,27,9,30,7,6])). % 75.94/76.24 cnf(3427,plain, % 75.94/76.24 (~E(a8,f4(a8,a1))), % 75.94/76.24 inference(scs_inference,[],[3342,3368,3372,3358,684,34,28,25,5,8,4,27,9,30,7,6,26])). % 75.94/76.24 cnf(3434,plain, % 75.94/76.24 (~P3(f9(a6,a2),f9(a8,a2))), % 75.94/76.24 inference(scs_inference,[],[3380,2482,3342,3354,3368,3372,2480,3358,684,34,28,25,5,8,4,27,9,30,7,6,26,2,38,32,33])). % 75.94/76.24 cnf(3437,plain, % 75.94/76.24 (~P1(f9(a6,a1),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[16,3380,2482,3342,2867,2745,3354,3331,3368,3372,2480,3358,684,34,28,25,5,8,4,27,9,30,7,6,26,2,38,32,33,10,31])). % 75.94/76.24 cnf(3442,plain, % 75.94/76.24 (~E(f9(a8,a8),a1)), % 75.94/76.24 inference(scs_inference,[],[16,3210,3380,2482,3342,2867,2745,3262,3354,3331,3368,3372,2480,3358,684,133,34,28,25,5,8,4,27,9,30,7,6,26,2,38,32,33,10,31,11,3])). % 75.94/76.24 cnf(3459,plain, % 75.94/76.24 (P3(a8,f4(f9(a2,a8),f9(a1,a6)))), % 75.94/76.24 inference(scs_inference,[],[2851,34])). % 75.94/76.24 cnf(3463,plain, % 75.94/76.24 (P1(f3(x34631,f9(a8,a2)),f3(x34631,a1))), % 75.94/76.24 inference(scs_inference,[],[3417,3411,2851,34,28,25])). % 75.94/76.24 cnf(3468,plain, % 75.94/76.24 (E(f4(a2,x34681),f4(f9(a8,a2),x34681))), % 75.94/76.24 inference(scs_inference,[],[2736,3417,3411,2851,2690,56,34,28,25,27,4,8])). % 75.94/76.24 cnf(3469,plain, % 75.94/76.24 (E(f4(x34691,a2),f4(x34691,f9(a8,a2)))), % 75.94/76.24 inference(scs_inference,[],[2736,3417,3411,2851,2690,56,34,28,25,27,4,8,9])). % 75.94/76.24 cnf(3470,plain, % 75.94/76.24 (E(f3(x34701,a2),f3(x34701,f9(a8,a2)))), % 75.94/76.24 inference(scs_inference,[],[2736,3417,3411,2851,2690,56,34,28,25,27,4,8,9,5])). % 75.94/76.24 cnf(3473,plain, % 75.94/76.24 (E(f9(x34731,a2),f9(x34731,f9(a8,a2)))), % 75.94/76.24 inference(scs_inference,[],[2736,3417,3198,3411,2851,2690,56,34,28,25,27,4,8,9,5,30,7])). % 75.94/76.24 cnf(3474,plain, % 75.94/76.24 (E(f9(a2,x34741),f9(f9(a8,a2),x34741))), % 75.94/76.24 inference(scs_inference,[],[2736,3417,3198,3411,2851,2690,56,34,28,25,27,4,8,9,5,30,7,6])). % 75.94/76.24 cnf(3477,plain, % 75.94/76.24 (~E(f3(a2,a1),a10)), % 75.94/76.24 inference(scs_inference,[],[2736,120,3417,3198,3411,2851,2690,56,34,28,25,27,4,8,9,5,30,7,6,26,2])). % 75.94/76.24 cnf(3480,plain, % 75.94/76.24 (E(f9(f9(a8,a2),x34801),f9(a1,x34801))), % 75.94/76.24 inference(rename_variables,[],[3426])). % 75.94/76.24 cnf(3481,plain, % 75.94/76.24 (~P3(f9(f9(a2,a8),a8),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[2736,120,3417,3426,3198,3411,1755,1737,2851,2690,56,112,153,34,28,25,27,4,8,9,5,30,7,6,26,2,15,14,33])). % 75.94/76.24 cnf(3484,plain, % 75.94/76.24 (~P1(f9(f9(a8,a2),a6),f9(a2,a8))), % 75.94/76.24 inference(scs_inference,[],[3347,2736,120,3417,3426,3480,3198,3411,1755,1737,2851,2690,56,112,153,34,28,25,27,4,8,9,5,30,7,6,26,2,15,14,33,10])). % 75.94/76.24 cnf(3485,plain, % 75.94/76.24 (E(f9(f9(a8,a2),x34851),f9(a1,x34851))), % 75.94/76.24 inference(rename_variables,[],[3426])). % 75.94/76.24 cnf(3486,plain, % 75.94/76.24 (~P1(f9(a1,a6),a2)), % 75.94/76.24 inference(scs_inference,[],[3347,2736,120,3417,3426,3480,3198,3411,1755,1737,90,2851,2690,56,112,153,34,28,25,27,4,8,9,5,30,7,6,26,2,15,14,33,10,31])). % 75.94/76.24 cnf(3489,plain, % 75.94/76.24 (E(f9(f9(a8,a2),x34891),f9(a1,x34891))), % 75.94/76.24 inference(rename_variables,[],[3426])). % 75.94/76.24 cnf(3494,plain, % 75.94/76.24 (~P3(f9(a6,a1),a1)), % 75.94/76.24 inference(scs_inference,[],[16,3347,3396,2736,120,2747,3417,3426,3480,3485,3489,3198,3411,2337,1755,1737,90,2851,2690,56,112,153,34,28,25,27,4,8,9,5,30,7,6,26,2,15,14,33,10,31,11,3,12,13])). % 75.94/76.24 cnf(3497,plain, % 75.94/76.24 (P3(a8,f4(f9(a2,a8),f9(a6,a1)))), % 75.94/76.24 inference(scs_inference,[],[2863,34])). % 75.94/76.24 cnf(3501,plain, % 75.94/76.24 (P1(f4(f9(a8,a2),x35011),f4(a1,x35011))), % 75.94/76.24 inference(scs_inference,[],[3418,3459,2863,34,28,25])). % 75.94/76.24 cnf(3505,plain, % 75.94/76.24 (E(f4(x35051,f9(a2,a8)),f4(x35051,a1))), % 75.94/76.24 inference(scs_inference,[],[3434,3418,3459,2863,684,34,28,25,27,9])). % 75.94/76.24 cnf(3506,plain, % 75.94/76.24 (E(f4(f9(a2,a8),x35061),f4(a1,x35061))), % 75.94/76.24 inference(scs_inference,[],[3434,3418,3459,2863,684,34,28,25,27,9,8])). % 75.94/76.24 cnf(3507,plain, % 75.94/76.24 (E(f3(a2,x35071),f3(f9(a1,a8),x35071))), % 75.94/76.24 inference(scs_inference,[],[3434,3418,3459,2863,684,112,34,28,25,27,9,8,4])). % 75.94/76.24 cnf(3510,plain, % 75.94/76.24 (E(f3(x35101,f9(a2,a8)),f3(x35101,a1))), % 75.94/76.24 inference(scs_inference,[],[3434,3418,3459,2863,684,112,34,28,25,27,9,8,4,30,5])). % 75.94/76.24 cnf(3511,plain, % 75.94/76.24 (E(f9(x35111,f9(a2,a8)),f9(x35111,a1))), % 75.94/76.24 inference(scs_inference,[],[3434,3418,3459,2863,684,112,34,28,25,27,9,8,4,30,5,7])). % 75.94/76.24 cnf(3512,plain, % 75.94/76.24 (E(f9(f9(a2,a8),x35121),f9(a1,x35121))), % 75.94/76.24 inference(scs_inference,[],[3434,3418,3459,2863,684,112,34,28,25,27,9,8,4,30,5,7,6])). % 75.94/76.24 cnf(3515,plain, % 75.94/76.24 (~E(f9(a5,a8),a10)), % 75.94/76.24 inference(scs_inference,[],[1725,3434,3418,3459,2863,684,112,34,28,25,27,9,8,4,30,5,7,6,26,2])). % 75.94/76.24 cnf(3516,plain, % 75.94/76.24 (~P3(f9(a2,f9(a6,a6)),f9(a8,a8))), % 75.94/76.24 inference(scs_inference,[],[1725,3434,3391,3418,3459,2528,2863,684,112,34,28,25,27,9,8,4,30,5,7,6,26,2,33])). % 75.94/76.24 cnf(3518,plain, % 75.94/76.24 (~P1(f9(a6,a1),a2)), % 75.94/76.25 inference(scs_inference,[],[1725,3434,2434,3391,3418,3459,2528,2747,2863,684,112,34,28,25,27,9,8,4,30,5,7,6,26,2,33,31])). % 75.94/76.25 cnf(3523,plain, % 75.94/76.25 (~P1(f9(a1,a6),a1)), % 75.94/76.25 inference(scs_inference,[],[16,1725,3434,2434,3391,3486,3418,3459,2528,2747,2863,3327,684,112,34,28,25,27,9,8,4,30,5,7,6,26,2,33,31,10,11])). % 75.94/76.25 cnf(3524,plain, % 75.94/76.25 (~E(f9(a8,a8),f9(a6,a6))), % 75.94/76.25 inference(scs_inference,[],[16,191,1725,3434,2434,3391,3486,3418,3459,2528,2747,2863,3327,684,112,133,34,28,25,27,9,8,4,30,5,7,6,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(3529,plain, % 75.94/76.25 (E(f3(a1,a1),a10)), % 75.94/76.25 inference(scs_inference,[],[16,191,1725,3434,2434,3391,3486,3494,3418,3425,2766,3459,2528,878,2747,2863,3327,976,684,112,133,18,34,28,25,27,9,8,4,30,5,7,6,26,2,33,31,10,11,3,12,13,36])). % 75.94/76.25 cnf(3531,plain, % 75.94/76.25 (~E(a6,f9(a1,a6))), % 75.94/76.25 inference(scs_inference,[],[16,191,1725,3434,2434,3391,3486,3494,3418,3425,2766,3459,2528,878,2747,2863,3327,976,684,112,133,18,34,28,25,27,9,8,4,30,5,7,6,26,2,33,31,10,11,3,12,13,36,100])). % 75.94/76.25 cnf(3534,plain, % 75.94/76.25 (P3(a8,f4(f9(a8,a8),f9(a6,a6)))), % 75.94/76.25 inference(scs_inference,[],[2465,34])). % 75.94/76.25 cnf(3542,plain, % 75.94/76.25 (E(f4(x35421,f3(a1,a1)),f4(x35421,a10))), % 75.94/76.25 inference(scs_inference,[],[2984,3529,3497,2465,34,28,25,27,9])). % 75.94/76.25 cnf(3546,plain, % 75.94/76.25 (E(f3(x35461,f3(a1,a1)),f3(x35461,a10))), % 75.94/76.25 inference(scs_inference,[],[2984,3529,3497,2465,34,28,25,27,9,30,8,5])). % 75.94/76.25 cnf(3547,plain, % 75.94/76.25 (E(f3(f3(a1,a1),x35471),f3(a10,x35471))), % 75.94/76.25 inference(scs_inference,[],[2984,3529,3497,2465,34,28,25,27,9,30,8,5,4])). % 75.94/76.25 cnf(3549,plain, % 75.94/76.25 (E(f9(f3(a1,a1),x35491),f9(a10,x35491))), % 75.94/76.25 inference(scs_inference,[],[2984,3529,3497,2465,34,28,25,27,9,30,8,5,4,7,6])). % 75.94/76.25 cnf(3552,plain, % 75.94/76.25 (~E(f9(a2,a6),a6)), % 75.94/76.25 inference(scs_inference,[],[3316,2984,3529,3497,2465,34,28,25,27,9,30,8,5,4,7,6,26,2])). % 75.94/76.25 cnf(3553,plain, % 75.94/76.25 (~P3(f4(f9(a2,a8),f9(a6,a1)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3316,2984,3529,3497,2465,153,34,28,25,27,9,30,8,5,4,7,6,26,2,33])). % 75.94/76.25 cnf(3556,plain, % 75.94/76.25 (~P1(f9(a6,a8),a8)), % 75.94/76.25 inference(scs_inference,[],[3316,2984,2372,3529,3497,2334,2465,153,34,28,25,27,9,30,8,5,4,7,6,26,2,33,31])). % 75.94/76.25 cnf(3561,plain, % 75.94/76.25 (~P1(f9(a6,a1),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[3437,3316,2984,2372,3529,3511,3497,3207,2334,2465,153,34,28,25,27,9,30,8,5,4,7,6,26,2,33,31,10,11])). % 75.94/76.25 cnf(3568,plain, % 75.94/76.25 (E(f3(a6,a6),a10)), % 75.94/76.25 inference(scs_inference,[],[16,3437,3316,2984,2372,3529,3511,3512,3361,3497,3207,2334,2418,2465,221,772,41,153,34,28,25,27,9,30,8,5,4,7,6,26,2,33,31,10,11,3,12,13,36])). % 75.94/76.25 cnf(3572,plain, % 75.94/76.25 (P3(a8,f4(a1,f9(a6,a2)))), % 75.94/76.25 inference(scs_inference,[],[2480,34])). % 75.94/76.25 cnf(3580,plain, % 75.94/76.25 (E(f4(x35801,f3(a6,a6)),f4(x35801,a10))), % 75.94/76.25 inference(scs_inference,[],[3568,2503,3534,2480,34,28,25,27,9])). % 75.94/76.25 cnf(3583,plain, % 75.94/76.25 (E(f3(f3(a6,a6),x35831),f3(a10,x35831))), % 75.94/76.25 inference(scs_inference,[],[3568,2503,3534,2480,34,28,25,27,9,30,4])). % 75.94/76.25 cnf(3584,plain, % 75.94/76.25 (E(f4(f3(a6,a6),x35841),f4(a10,x35841))), % 75.94/76.25 inference(scs_inference,[],[3568,2503,3534,2480,34,28,25,27,9,30,4,8])). % 75.94/76.25 cnf(3586,plain, % 75.94/76.25 (E(f9(x35861,f3(a6,a6)),f9(x35861,a10))), % 75.94/76.25 inference(scs_inference,[],[3568,2503,3534,2480,34,28,25,27,9,30,4,8,5,7])). % 75.94/76.25 cnf(3591,plain, % 75.94/76.25 (~P3(f9(a6,a1),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3531,3568,2503,3481,3534,2870,2480,34,28,25,27,9,30,4,8,5,7,6,26,2,33])). % 75.94/76.25 cnf(3593,plain, % 75.94/76.25 (~P1(f9(a6,f9(a6,a8)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3531,3568,353,2503,2547,3481,3534,2870,2480,34,28,25,27,9,30,4,8,5,7,6,26,2,33,31])). % 75.94/76.25 cnf(3597,plain, % 75.94/76.25 (~P1(f9(a6,a1),a1)), % 75.94/76.25 inference(scs_inference,[],[16,3531,3518,3568,353,2503,2547,3481,3534,2870,2480,41,34,28,25,27,9,30,4,8,5,7,6,26,2,33,31,10,11])). % 75.94/76.25 cnf(3600,plain, % 75.94/76.25 (~P3(f3(a6,a6),f9(a10,a8))), % 75.94/76.25 inference(scs_inference,[],[16,761,3531,3518,3568,353,2503,2547,3481,3474,3534,2870,2480,41,153,34,28,25,27,9,30,4,8,5,7,6,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(3603,plain, % 75.94/76.25 (~E(a6,f9(a6,a1))), % 75.94/76.25 inference(scs_inference,[],[16,761,3531,3518,3568,353,2503,2547,3481,2783,3474,3534,2870,2480,41,153,34,28,25,27,9,30,4,8,5,7,6,26,2,33,31,10,11,3,12,13,100])). % 75.94/76.25 cnf(3609,plain, % 75.94/76.25 (P3(a8,f4(a2,f9(a1,a6)))), % 75.94/76.25 inference(scs_inference,[],[2734,34])). % 75.94/76.25 cnf(3617,plain, % 75.94/76.25 (E(f4(x36171,f9(a1,a8)),f4(x36171,a2))), % 75.94/76.25 inference(scs_inference,[],[3591,3419,3572,2734,56,34,28,25,27,9])). % 75.94/76.25 cnf(3620,plain, % 75.94/76.25 (E(f3(f3(a2,a1),x36201),f3(a5,x36201))), % 75.94/76.25 inference(scs_inference,[],[3591,3419,3572,2734,56,17,34,28,25,27,9,30,4])). % 75.94/76.25 cnf(3621,plain, % 75.94/76.25 (E(f3(x36211,f9(a1,a8)),f3(x36211,a2))), % 75.94/76.25 inference(scs_inference,[],[3591,3419,3572,2734,56,17,34,28,25,27,9,30,4,5])). % 75.94/76.25 cnf(3622,plain, % 75.94/76.25 (E(f4(f9(a1,a8),x36221),f4(a2,x36221))), % 75.94/76.25 inference(scs_inference,[],[3591,3419,3572,2734,56,17,34,28,25,27,9,30,4,5,8])). % 75.94/76.25 cnf(3623,plain, % 75.94/76.25 (E(f9(x36231,f9(a1,a8)),f9(x36231,a2))), % 75.94/76.25 inference(scs_inference,[],[3591,3419,3572,2734,56,17,34,28,25,27,9,30,4,5,8,7])). % 75.94/76.25 cnf(3624,plain, % 75.94/76.25 (E(f9(f9(a1,a8),x36241),f9(a2,x36241))), % 75.94/76.25 inference(scs_inference,[],[3591,3419,3572,2734,56,17,34,28,25,27,9,30,4,5,8,7,6])). % 75.94/76.25 cnf(3627,plain, % 75.94/76.25 (~E(a8,f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[3591,3264,3419,3572,2734,56,17,34,28,25,27,9,30,4,5,8,7,6,26,2])). % 75.94/76.25 cnf(3628,plain, % 75.94/76.25 (P2(f9(a1,a8),f9(a8,a1))), % 75.94/76.25 inference(scs_inference,[],[3591,3264,3419,3572,1792,3426,2734,56,17,34,28,25,27,9,30,4,5,8,7,6,26,2,14])). % 75.94/76.25 cnf(3633,plain, % 75.94/76.25 (~P1(f9(a6,f9(a6,a6)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3591,3264,508,2511,3419,3572,1792,3426,2734,56,17,153,34,28,25,27,9,30,4,5,8,7,6,26,2,14,33,31])). % 75.94/76.25 cnf(3635,plain, % 75.94/76.25 (~P1(f9(a6,f9(a8,a2)),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[3561,3591,3264,508,2511,3419,3572,1792,3425,3426,2734,56,17,153,34,28,25,27,9,30,4,5,8,7,6,26,2,14,33,31,10])). % 75.94/76.25 cnf(3648,plain, % 75.94/76.25 (P3(a8,f4(a2,f9(a6,a1)))), % 75.94/76.25 inference(scs_inference,[],[2743,34])). % 75.94/76.25 cnf(3652,plain, % 75.94/76.25 (P1(f4(x36521,f9(a8,a2)),f4(x36521,a1))), % 75.94/76.25 inference(scs_inference,[],[3422,3609,2743,34,28,25])). % 75.94/76.25 cnf(3658,plain, % 75.94/76.25 (E(f4(x36581,a2),f4(x36581,f9(a1,a8)))), % 75.94/76.25 inference(scs_inference,[],[3600,3422,3609,2743,112,34,28,25,27,30,9])). % 75.94/76.25 cnf(3659,plain, % 75.94/76.25 (E(f3(f9(x36591,a8),x36592),f3(x36591,x36592))), % 75.94/76.25 inference(scs_inference,[],[3600,3422,3609,2743,112,22,34,28,25,27,30,9,4])). % 75.94/76.25 cnf(3660,plain, % 75.94/76.25 (E(f4(a2,x36601),f4(f9(a1,a8),x36601))), % 75.94/76.25 inference(scs_inference,[],[3600,3422,3609,2743,112,22,34,28,25,27,30,9,4,8])). % 75.94/76.25 cnf(3661,plain, % 75.94/76.25 (E(f3(x36611,a2),f3(x36611,f9(a1,a8)))), % 75.94/76.25 inference(scs_inference,[],[3600,3422,3609,2743,112,22,34,28,25,27,30,9,4,8,5])). % 75.94/76.25 cnf(3662,plain, % 75.94/76.25 (E(f9(x36621,a2),f9(x36621,f9(a1,a8)))), % 75.94/76.25 inference(scs_inference,[],[3600,3422,3609,2743,112,22,34,28,25,27,30,9,4,8,5,7])). % 75.94/76.25 cnf(3663,plain, % 75.94/76.25 (E(f9(a2,x36631),f9(f9(a1,a8),x36631))), % 75.94/76.25 inference(scs_inference,[],[3600,3422,3609,2743,112,22,34,28,25,27,30,9,4,8,5,7,6])). % 75.94/76.25 cnf(3678,plain, % 75.94/76.25 (~E(f9(f9(a2,a8),a8),f9(a2,a6))), % 75.94/76.25 inference(scs_inference,[],[3386,3603,3600,422,2524,3422,3501,3506,3252,3609,128,2743,3327,2978,112,22,34,28,25,27,30,9,4,8,5,7,6,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(3688,plain, % 75.94/76.25 (P3(a8,f4(a8,f4(a8,a2)))), % 75.94/76.25 inference(scs_inference,[],[3319,34])). % 75.94/76.25 cnf(3698,plain, % 75.94/76.25 (E(f4(x36981,f3(a2,a1)),f4(x36981,a5))), % 75.94/76.25 inference(scs_inference,[],[2576,3659,3648,3319,17,34,25,28,27,30,9])). % 75.94/76.25 cnf(3699,plain, % 75.94/76.25 (E(f3(a2,x36991),f3(a1,x36991))), % 75.94/76.25 inference(scs_inference,[],[2576,3659,3648,3319,17,48,34,25,28,27,30,9,4])). % 75.94/76.25 cnf(3701,plain, % 75.94/76.25 (E(f4(f3(a2,a1),x37011),f4(a5,x37011))), % 75.94/76.25 inference(scs_inference,[],[2576,3659,3648,3319,17,48,34,25,28,27,30,9,4,5,8])). % 75.94/76.25 cnf(3706,plain, % 75.94/76.25 (~E(f9(a8,a1),f9(a1,a6))), % 75.94/76.25 inference(scs_inference,[],[193,2576,3659,3648,3319,17,48,34,25,28,27,30,9,4,5,8,7,6,26,2])). % 75.94/76.25 cnf(3707,plain, % 75.94/76.25 (~P3(f4(a2,f9(a6,a1)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[193,2576,3659,3648,3319,17,48,153,34,25,28,27,30,9,4,5,8,7,6,26,2,33])). % 75.94/76.25 cnf(3714,plain, % 75.94/76.25 (~P1(f9(a1,a6),f9(a8,f4(a8,a1)))), % 75.94/76.25 inference(scs_inference,[],[193,3216,590,2576,3659,3648,3523,3361,3319,17,22,48,153,34,25,28,27,30,9,4,5,8,7,6,26,2,33,31,10,11])). % 75.94/76.25 cnf(3717,plain, % 75.94/76.25 (~P3(f9(f9(a2,a8),f9(a6,a6)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[16,193,3216,590,2576,2879,3659,3648,3523,2346,3512,3361,3319,17,22,48,153,34,25,28,27,30,9,4,5,8,7,6,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(3719,plain, % 75.94/76.25 (~P3(f9(a6,a1),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[16,193,3216,590,2576,2879,3659,2872,3648,3523,2346,3512,3361,3252,3319,17,22,48,153,34,25,28,27,30,9,4,5,8,7,6,26,2,33,31,10,11,3,12,13])). % 75.94/76.25 cnf(3726,plain, % 75.94/76.25 (P3(a8,f4(f9(a8,a8),a6))), % 75.94/76.25 inference(scs_inference,[],[201,34])). % 75.94/76.25 cnf(3730,plain, % 75.94/76.25 (P1(f4(x37301,f9(a2,a8)),f4(x37301,a1))), % 75.94/76.25 inference(scs_inference,[],[3505,3688,201,34,28,25])). % 75.94/76.25 cnf(3736,plain, % 75.94/76.25 (E(f4(x37361,f9(a8,a2)),f4(x37361,a2))), % 75.94/76.25 inference(scs_inference,[],[3719,3505,3688,201,2687,34,28,25,27,30,9])). % 75.94/76.25 cnf(3737,plain, % 75.94/76.25 (E(f3(x37371,x37372),f3(f9(x37371,a8),x37372))), % 75.94/76.25 inference(scs_inference,[],[3719,3505,3688,201,2687,133,34,28,25,27,30,9,4])). % 75.94/76.25 cnf(3738,plain, % 75.94/76.25 (E(f4(f9(a8,a2),x37381),f4(a2,x37381))), % 75.94/76.25 inference(scs_inference,[],[3719,3505,3688,201,2687,133,34,28,25,27,30,9,4,8])). % 75.94/76.25 cnf(3739,plain, % 75.94/76.25 (E(f3(x37391,f9(a8,a2)),f3(x37391,a2))), % 75.94/76.25 inference(scs_inference,[],[3719,3505,3688,201,2687,133,34,28,25,27,30,9,4,8,5])). % 75.94/76.25 cnf(3740,plain, % 75.94/76.25 (E(f9(x37401,f9(a8,a2)),f9(x37401,a2))), % 75.94/76.25 inference(scs_inference,[],[3719,3505,3688,201,2687,133,34,28,25,27,30,9,4,8,5,7])). % 75.94/76.25 cnf(3741,plain, % 75.94/76.25 (E(f9(f9(a8,a2),x37411),f9(a2,x37411))), % 75.94/76.25 inference(scs_inference,[],[3719,3505,3688,201,2687,133,34,28,25,27,30,9,4,8,5,7,6])). % 75.94/76.25 cnf(3745,plain, % 75.94/76.25 (~P3(f9(a1,f9(a6,a6)),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[3719,3352,3505,3688,212,2762,201,2687,133,34,28,25,27,30,9,4,8,5,7,6,26,2,33])). % 75.94/76.25 cnf(3753,plain, % 75.94/76.25 (E(f3(x37531,f9(a2,a8)),f3(x37531,a1))), % 75.94/76.25 inference(rename_variables,[],[3510])). % 75.94/76.25 cnf(3755,plain, % 75.94/76.25 (~E(f9(f9(a1,a8),a6),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[2693,3719,3243,3352,494,3505,3510,3663,3688,212,3282,2503,2762,201,2687,133,34,28,25,27,30,9,4,8,5,7,6,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(3757,plain, % 75.94/76.25 (~P3(f3(f9(a8,a2),f9(a2,a8)),f9(a5,a8))), % 75.94/76.25 inference(scs_inference,[],[2693,3719,3243,3352,494,3222,3505,3510,3753,3663,3688,212,3282,2503,2762,201,2687,133,34,28,25,27,30,9,4,8,5,7,6,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(3765,plain, % 75.94/76.25 (P3(a8,f4(x37651,f9(a6,x37651)))), % 75.94/76.25 inference(scs_inference,[],[60,34])). % 75.94/76.25 cnf(3769,plain, % 75.94/76.25 (P1(f4(x37691,f9(a1,a8)),f4(x37691,a2))), % 75.94/76.25 inference(scs_inference,[],[3617,3726,60,34,28,25])). % 75.94/76.25 cnf(3775,plain, % 75.94/76.25 (E(f4(x37751,f9(x37752,a8)),f4(x37751,x37752))), % 75.94/76.25 inference(scs_inference,[],[2598,3617,3726,22,60,34,28,25,30,27,9])). % 75.94/76.25 cnf(3776,plain, % 75.94/76.25 (E(f4(f9(x37761,a8),x37762),f4(x37761,x37762))), % 75.94/76.25 inference(scs_inference,[],[2598,3617,3726,22,60,34,28,25,30,27,9,8])). % 75.94/76.25 cnf(3777,plain, % 75.94/76.25 (E(f3(x37771,f9(x37772,a8)),f3(x37771,x37772))), % 75.94/76.25 inference(scs_inference,[],[2598,3617,3726,22,60,34,28,25,30,27,9,8,5])). % 75.94/76.25 cnf(3778,plain, % 75.94/76.25 (E(f9(x37781,f9(x37782,a8)),f9(x37781,x37782))), % 75.94/76.25 inference(scs_inference,[],[2598,3617,3726,22,60,34,28,25,30,27,9,8,5,7])). % 75.94/76.25 cnf(3779,plain, % 75.94/76.25 (E(f9(f9(x37791,a8),x37792),f9(x37791,x37792))), % 75.94/76.25 inference(scs_inference,[],[2598,3617,3726,22,60,34,28,25,30,27,9,8,5,7,6])). % 75.94/76.25 cnf(3782,plain, % 75.94/76.25 (~E(a1,f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3442,2598,3617,3726,22,60,34,28,25,30,27,9,8,5,7,6,26,2])). % 75.94/76.25 cnf(3792,plain, % 75.94/76.25 (~P1(f9(a6,a1),f9(a8,f4(a8,a1)))), % 75.94/76.25 inference(scs_inference,[],[3442,3556,2598,3617,3027,3726,3597,991,3361,112,22,60,153,34,28,25,30,27,9,8,5,7,6,26,2,14,33,31,10,11])). % 75.94/76.25 cnf(3795,plain, % 75.94/76.25 (~P3(f9(f9(a1,a8),f9(a6,a6)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[16,3442,3556,2598,3516,3617,3624,3027,3726,3597,991,397,3361,112,22,60,153,34,28,25,30,27,9,8,5,7,6,26,2,14,33,31,10,11,3,12])). % 75.94/76.25 cnf(3800,plain, % 75.94/76.25 (P3(a8,f4(x38001,f9(x38001,a6)))), % 75.94/76.25 inference(scs_inference,[],[54,34])). % 75.94/76.25 cnf(3804,plain, % 75.94/76.25 (P1(f4(x38041,f9(x38042,a8)),f4(x38041,x38042))), % 75.94/76.25 inference(scs_inference,[],[3775,3765,54,34,28,25])). % 75.94/76.25 cnf(3811,plain, % 75.94/76.25 (E(f4(a2,x38111),f4(a1,x38111))), % 75.94/76.25 inference(scs_inference,[],[2606,3775,3765,54,48,34,28,25,27,30,9,8])). % 75.94/76.25 cnf(3812,plain, % 75.94/76.25 (E(f3(x38121,a2),f3(x38121,a1))), % 75.94/76.25 inference(scs_inference,[],[2606,3775,3765,54,48,34,28,25,27,30,9,8,5])). % 75.94/76.25 cnf(3813,plain, % 75.94/76.25 (E(f9(x38131,a2),f9(x38131,a1))), % 75.94/76.25 inference(scs_inference,[],[2606,3775,3765,54,48,34,28,25,27,30,9,8,5,7])). % 75.94/76.25 cnf(3814,plain, % 75.94/76.25 (E(f9(a2,x38141),f9(a1,x38141))), % 75.94/76.25 inference(scs_inference,[],[2606,3775,3765,54,48,34,28,25,27,30,9,8,5,7,6])). % 75.94/76.25 cnf(3818,plain, % 75.94/76.25 (~P3(f9(f9(a6,a6),a2),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[3384,2606,3775,3765,2535,682,54,48,34,28,25,27,30,9,8,5,7,6,26,2,33])). % 75.94/76.25 cnf(3820,plain, % 75.94/76.25 (~P1(a1,f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3782,3384,2606,3775,3765,2535,682,3391,54,48,34,28,25,27,30,9,8,5,7,6,26,2,33,31])). % 75.94/76.25 cnf(3827,plain, % 75.94/76.25 (~E(f9(a8,f9(a8,a2)),f9(a2,a6))), % 75.94/76.25 inference(scs_inference,[],[3401,3782,3384,2606,3775,3776,3652,3730,3473,3765,2535,682,3391,54,48,34,28,25,27,30,9,8,5,7,6,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(3832,plain, % 75.94/76.25 (~E(a7,f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[16,3401,3782,3384,2606,3707,3775,3776,3622,3652,3730,2837,3473,3765,2535,682,3391,54,48,34,28,25,27,30,9,8,5,7,6,26,2,33,31,10,11,3,12,13,123])). % 75.94/76.25 cnf(3835,plain, % 75.94/76.25 (P3(a8,f4(a8,f9(a6,a6)))), % 75.94/76.25 inference(scs_inference,[],[63,34])). % 75.94/76.25 cnf(3839,plain, % 75.94/76.25 (P1(f4(a2,x38391),f4(a1,x38391))), % 75.94/76.25 inference(scs_inference,[],[3811,3800,63,34,28,25])). % 75.94/76.25 cnf(3847,plain, % 75.94/76.25 (E(f3(x38471,x38472),f3(x38471,f9(x38472,a8)))), % 75.94/76.25 inference(scs_inference,[],[3811,2613,3800,133,63,34,28,25,30,27,9,8,5])). % 75.94/76.25 cnf(3848,plain, % 75.94/76.25 (E(f9(x38481,x38482),f9(x38481,f9(x38482,a8)))), % 75.94/76.25 inference(scs_inference,[],[3811,2613,3800,133,63,34,28,25,30,27,9,8,5,7])). % 75.94/76.25 cnf(3849,plain, % 75.94/76.25 (E(f9(x38491,x38492),f9(f9(x38491,a8),x38492))), % 75.94/76.25 inference(scs_inference,[],[3811,2613,3800,133,63,34,28,25,30,27,9,8,5,7,6])). % 75.94/76.25 cnf(3860,plain, % 75.94/76.25 (E(f9(x38601,f9(x38602,a8)),f9(x38601,x38602))), % 75.94/76.25 inference(rename_variables,[],[3778])). % 75.94/76.25 cnf(3863,plain, % 75.94/76.25 (~P3(f9(f9(a8,a6),f9(a6,a8)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[16,3811,3820,3832,663,2613,3778,3860,3800,366,3361,133,153,63,34,28,25,30,27,9,8,5,7,6,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(3865,plain, % 75.94/76.25 (~P3(f9(f9(a1,a6),a8),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[16,3811,3814,3820,3832,663,2613,3402,3778,3860,3800,366,3361,133,153,63,34,28,25,30,27,9,8,5,7,6,26,2,33,31,10,11,3,12,13])). % 75.94/76.25 cnf(3868,plain, % 75.94/76.25 (~P1(a6,f9(a6,a8))+E(f3(f9(a6,a8),f9(a6,a8)),a10)), % 75.94/76.25 inference(scs_inference,[],[16,3811,3814,3820,3832,663,2613,3402,3778,3860,3800,1753,366,1777,3361,133,153,63,34,28,25,30,27,9,8,5,7,6,26,2,33,31,10,11,3,12,13,123,36])). % 75.94/76.25 cnf(3873,plain, % 75.94/76.25 (P3(a8,f4(a8,a6))), % 75.94/76.25 inference(scs_inference,[],[21,34])). % 75.94/76.25 cnf(3885,plain, % 75.94/76.25 (~E(f4(a8,a1),a8)), % 75.94/76.25 inference(scs_inference,[],[3812,3427,3064,3835,21,34,28,25,27,30,26,2])). % 75.94/76.25 cnf(3886,plain, % 75.94/76.25 (~P3(f9(a1,f9(a6,a6)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3812,3427,3064,3835,3299,2875,21,34,28,25,27,30,26,2,33])). % 75.94/76.25 cnf(3888,plain, % 75.94/76.25 (~P1(f9(a1,f9(a6,a6)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[3812,3427,2764,3064,3835,3299,2879,2875,21,34,28,25,27,30,26,2,33,31])). % 75.94/76.25 cnf(3906,plain, % 75.94/76.25 (P3(a8,f4(a8,f4(a8,a6)))), % 75.94/76.25 inference(scs_inference,[],[3873,34])). % 75.94/76.25 cnf(3910,plain, % 75.94/76.25 (P1(f3(x39101,f9(x39102,a8)),f3(x39101,x39102))), % 75.94/76.25 inference(scs_inference,[],[3873,3777,34,28,25])). % 75.94/76.25 cnf(3916,plain, % 75.94/76.25 (~E(a8,f4(a8,a6))), % 75.94/76.25 inference(scs_inference,[],[3873,3086,3777,34,28,25,27,30,26])). % 75.94/76.25 cnf(3919,plain, % 75.94/76.25 (~P3(f4(a8,a6),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3873,740,3086,3777,153,34,28,25,27,30,26,2,33])). % 75.94/76.25 cnf(3922,plain, % 75.94/76.25 (~P1(f9(f9(a1,a6),f9(a6,a8)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[3873,740,3083,3086,3777,153,34,28,25,27,30,26,2,33,31])). % 75.94/76.25 cnf(3924,plain, % 75.94/76.25 (~P1(f9(f9(a6,a8),f9(a6,a8)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[3873,740,3083,3086,3593,3777,3779,153,34,28,25,27,30,26,2,33,31,10])). % 75.94/76.25 cnf(3925,plain, % 75.94/76.25 (E(f9(f9(x39251,a8),x39252),f9(x39251,x39252))), % 75.94/76.25 inference(rename_variables,[],[3779])). % 75.94/76.25 cnf(3927,plain, % 75.94/76.25 (E(f9(f9(x39271,a8),x39272),f9(x39271,x39272))), % 75.94/76.25 inference(rename_variables,[],[3779])). % 75.94/76.25 cnf(3930,plain, % 75.94/76.25 (~P3(f9(f9(a1,a8),f9(a6,a6)),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[16,3873,740,3083,3086,3593,3745,3777,3779,3925,3927,3792,289,153,34,28,25,27,30,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(3943,plain, % 75.94/76.25 (P1(f3(x39431,f9(a1,a8)),f3(x39431,a2))), % 75.94/76.25 inference(scs_inference,[],[3621,3906,28,25])). % 75.94/76.25 cnf(3965,plain, % 75.94/76.25 (~P3(f9(f9(a6,a6),f9(a1,a8)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[3706,3919,3839,3916,3062,3818,3621,3623,3736,3849,3906,2558,3354,3064,3319,41,28,25,27,30,26,2,32,33,31,10,11,3,12])). % 75.94/76.25 cnf(3982,plain, % 75.94/76.25 (~P3(f9(a2,f9(a8,a6)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[742,3100,3738,2617,682,3015,28,25,27,30,26,2,33])). % 75.94/76.25 cnf(3986,plain, % 75.94/76.25 (~P1(f9(f9(a6,a8),f9(a8,a8)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[742,3098,3100,3302,3738,2617,3778,682,3015,28,25,27,30,26,2,33,31,10])). % 75.94/76.25 cnf(3987,plain, % 75.94/76.25 (E(f9(x39871,f9(x39872,a8)),f9(x39871,x39872))), % 75.94/76.25 inference(rename_variables,[],[3778])). % 75.94/76.25 cnf(3989,plain, % 75.94/76.25 (E(f9(a2,x39891),f9(a1,x39891))), % 75.94/76.25 inference(rename_variables,[],[3814])). % 75.94/76.25 cnf(3992,plain, % 75.94/76.25 (~P3(f9(f9(a6,a8),f9(a8,a8)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[16,742,3098,3100,3302,3310,3635,3738,2617,295,3814,3778,3987,682,3015,28,25,27,30,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(3994,plain, % 75.94/76.25 (~P3(f9(f9(a1,a8),f9(a6,a6)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[16,742,3098,3100,3302,3310,3930,3635,3738,2617,295,3814,3989,3778,3987,682,3015,28,25,27,30,26,2,33,31,10,11,3,12,13])). % 75.94/76.25 cnf(4005,plain, % 75.94/76.25 (P1(a1,f9(a6,f9(a2,a6)))), % 75.94/76.25 inference(scs_inference,[],[3114,3739,2625,2978,28,25,27,30])). % 75.94/76.25 cnf(4010,plain, % 75.94/76.25 (~P3(f9(a1,a6),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[2530,3114,3739,2625,3481,2858,2978,28,25,27,30,26,2,33])). % 75.94/76.25 cnf(4015,plain, % 75.94/76.25 (P1(x40151,x40151)), % 75.94/76.25 inference(rename_variables,[],[41])). % 75.94/76.25 cnf(4018,plain, % 75.94/76.25 (~E(f9(a8,f9(a8,a8)),f9(a6,a6))), % 75.94/76.25 inference(scs_inference,[],[3524,2530,3112,3114,3739,3740,2625,3481,3848,2858,2978,41,4015,28,25,27,30,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(4029,plain, % 75.94/76.25 (P1(f9(f9(a8,a2),x40291),f9(a2,x40291))), % 75.94/76.25 inference(scs_inference,[],[3741,658,28,25])). % 75.94/76.25 cnf(4033,plain, % 75.94/76.25 (P1(a1,f9(f9(a6,a2),a6))), % 75.94/76.25 inference(scs_inference,[],[4010,3741,2633,658,28,25,27,30])). % 75.94/76.25 cnf(4038,plain, % 75.94/76.25 (~E(f9(f9(a1,a6),f4(a8,a2)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[4010,2537,3741,2633,658,3319,28,25,27,30,26,2,32])). % 75.94/76.25 cnf(4046,plain, % 75.94/76.25 (E(f9(f9(x40461,a8),x40462),f9(x40461,x40462))), % 75.94/76.25 inference(rename_variables,[],[3779])). % 75.94/76.25 cnf(4048,plain, % 75.94/76.25 (E(f9(f9(x40481,a8),x40482),f9(x40481,x40482))), % 75.94/76.25 inference(rename_variables,[],[3779])). % 75.94/76.25 cnf(4049,plain, % 75.94/76.25 (~E(f3(f9(a2,a8),a1),f9(a5,a6))), % 75.94/76.25 inference(scs_inference,[],[4010,3339,2537,3633,3717,3741,3714,3737,2633,2348,3779,4046,3354,658,3319,28,25,27,30,26,2,32,33,31,10,11,3])). % 75.94/76.25 cnf(4051,plain, % 75.94/76.25 (~P3(f9(f9(a1,a8),a6),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[4010,3339,2537,3633,3717,3741,3714,3737,2633,2348,3779,4046,4048,3354,658,3319,28,25,27,30,26,2,32,33,31,10,11,3,12])). % 75.94/76.25 cnf(4065,plain, % 75.94/76.25 (P1(a1,f9(f9(a2,a6),a8))), % 75.94/76.25 inference(scs_inference,[],[3553,3281,2641,183,28,25,27,30])). % 75.94/76.25 cnf(4073,plain, % 75.94/76.25 (~P1(f9(f9(a8,a6),a1),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[2560,3553,2846,2968,3281,2641,128,3001,183,28,25,27,30,26,2,33,31])). % 75.94/76.25 cnf(4092,plain, % 75.94/76.25 (P1(f4(x40921,f3(a1,a1)),f4(x40921,a10))), % 75.94/76.25 inference(scs_inference,[],[3542,489,28,25])). % 75.94/76.25 cnf(4094,plain, % 75.94/76.25 (P1(a1,f9(f9(a8,a6),a2))), % 75.94/76.25 inference(scs_inference,[],[3542,2646,489,28,25,30])). % 75.94/76.25 cnf(4108,plain, % 75.94/76.25 (~P1(f9(a2,a6),f9(a8,f4(a8,a1)))), % 75.94/76.25 inference(scs_inference,[],[2648,3394,3795,3863,3041,3542,2646,3304,3391,3778,3361,489,28,25,30,27,26,2,33,31,10,11])). % 75.94/76.25 cnf(4130,plain, % 75.94/76.25 (~P3(f9(f9(a6,a6),a1),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[3126,3886,3546,2488,2779,212,217,28,25,27,30,26,2,33])). % 75.94/76.25 cnf(4138,plain, % 75.94/76.25 (~E(f9(a8,a8),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[16,3292,3126,3886,2781,2891,3910,3546,3547,4005,2488,2779,212,217,133,28,25,27,30,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(4158,plain, % 75.94/76.25 (~E(f9(a2,a8),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[4138,3965,3549,2964,243,28,25,30,27,26,2])). % 75.94/76.25 cnf(4169,plain, % 75.94/76.25 (~E(f3(a2,f9(a1,a8)),a10)), % 75.94/76.25 inference(scs_inference,[],[4138,3477,3888,3965,3982,524,3549,4108,3847,2964,3234,3814,3779,243,153,28,25,30,27,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(4171,plain, % 75.94/76.25 (~P3(f9(f9(a1,a8),f9(a8,a6)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[4138,3477,3888,3965,3982,524,3549,4108,3847,3624,2964,3234,3814,3779,243,153,28,25,30,27,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(4173,plain, % 75.94/76.25 (~P3(f9(a5,a8),f3(a1,a1))), % 75.94/76.25 inference(scs_inference,[],[4138,3477,3888,3965,3982,524,3549,4108,3847,3224,3360,3624,2964,3234,3814,3779,243,153,28,25,30,27,26,2,33,31,10,11,3,12,13])). % 75.94/76.25 cnf(4182,plain, % 75.94/76.25 (P1(f3(a1,a1),f9(a5,a8))), % 75.94/76.25 inference(scs_inference,[],[4173,3580,394,28,25,27])). % 75.94/76.25 cnf(4189,plain, % 75.94/76.25 (~P3(f9(a1,f9(a6,a8)),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[4173,3678,3580,3274,2804,2701,394,28,25,27,30,26,2,33])). % 75.94/76.25 cnf(4191,plain, % 75.94/76.25 (~P1(f9(a2,a8),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[4158,4173,3678,3580,3274,2804,2701,3299,394,28,25,27,30,26,2,33,31])). % 75.94/76.25 cnf(4197,plain, % 75.94/76.25 (~E(f9(f9(a2,a8),a8),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[16,4158,4173,3678,3463,3580,3583,4033,3274,2804,3849,2701,3299,394,28,25,27,30,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(4236,plain, % 75.94/76.25 (~P1(f9(a2,a8),f9(a8,f9(a8,a8)))), % 75.94/76.25 inference(scs_inference,[],[4191,3755,3992,4130,3584,3382,291,3741,3411,3628,3778,85,153,28,25,30,27,26,2,15,33,31,10,11])). % 75.94/76.25 cnf(4238,plain, % 75.94/76.25 (~E(f3(f9(a2,a8),f9(a2,a8)),f9(a5,a6))), % 75.94/76.25 inference(scs_inference,[],[4191,3755,3992,4130,4049,3584,3239,3382,291,3741,3411,3628,3778,85,153,28,25,30,27,26,2,15,33,31,10,11,3])). % 75.94/76.25 cnf(4240,plain, % 75.94/76.25 (~P3(f9(a2,f9(a6,a6)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[4191,3755,3992,3994,4130,4049,3584,3239,3382,291,3741,3411,3663,3628,3778,85,153,28,25,30,27,26,2,15,33,31,10,11,3,12])). % 75.94/76.25 cnf(4268,plain, % 75.94/76.25 (~E(f9(a8,a8),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[16,3627,4018,4051,4197,4029,3586,4094,2819,2844,3481,3029,128,240,133,28,25,30,27,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(4288,plain, % 75.94/76.25 (~E(f9(a8,a2),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[4268,4171,3620,2826,2922,325,28,30,25,27,26,2])). % 75.94/76.25 cnf(4296,plain, % 75.94/76.25 (E(f9(a1,x42961),f9(a2,x42961))), % 75.94/76.25 inference(rename_variables,[],[3207])). % 75.94/76.25 cnf(4297,plain, % 75.94/76.25 (~E(a10,f9(a5,a6))), % 75.94/76.25 inference(scs_inference,[],[4268,3484,3922,4171,4238,3865,3620,3226,2842,2826,2840,2922,3207,108,3848,325,28,30,25,27,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(4300,plain, % 75.94/76.25 (~P3(f9(f9(a1,a8),f9(a8,a6)),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[4268,3484,3922,4171,4238,3757,3865,3620,3226,2842,2826,2840,2922,3847,3207,4296,108,3848,325,28,30,25,27,26,2,33,31,10,11,3,12,13])). % 75.94/76.25 cnf(4318,plain, % 75.94/76.25 (~P3(f9(f9(a6,a1),a6),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[4297,4240,3698,2833,2904,212,110,28,30,25,27,26,2,33])). % 75.94/76.25 cnf(4326,plain, % 75.94/76.25 (~E(f9(a8,f9(a1,a8)),f9(a8,a8))), % 75.94/76.25 inference(scs_inference,[],[16,4288,4297,4240,2806,2908,3804,3698,3701,3662,4065,2833,2904,212,110,28,30,25,27,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(4348,plain, % 75.94/76.25 (~P3(f9(a2,f9(a6,a8)),f9(a2,a8))), % 75.94/76.25 inference(scs_inference,[],[4038,4300,3238,2952,2558,682,214,28,30,27,25,26,2,33])). % 75.94/76.25 cnf(4354,plain, % 75.94/76.25 (E(f9(x43541,x43542),f9(f9(x43541,a8),x43542))), % 75.94/76.25 inference(rename_variables,[],[3849])). % 75.94/76.25 cnf(4355,plain, % 75.94/76.25 (~P1(f9(a2,a8),f9(f9(a8,a8),f9(a8,a8)))), % 75.94/76.25 inference(scs_inference,[],[3986,4038,4300,4236,3238,2409,2952,2558,3849,682,3779,214,28,30,27,25,26,2,33,31,10,11])). % 75.94/76.25 cnf(4359,plain, % 75.94/76.25 (~P3(f9(a1,f9(a8,a6)),f9(a1,a8))), % 75.94/76.25 inference(scs_inference,[],[3885,3986,4038,4300,4236,3238,3373,2409,2952,2558,3849,4354,682,3779,214,28,30,27,25,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(4377,plain, % 75.94/76.25 (~P3(f9(a1,f9(a6,a6)),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[4326,4359,3374,2887,2762,2701,81,28,30,27,25,26,2,33])). % 75.94/76.25 cnf(4382,plain, % 75.94/76.25 (E(f3(x43821,a1),f3(x43821,f9(a8,a2)))), % 75.94/76.25 inference(rename_variables,[],[3374])). % 75.94/76.25 cnf(4389,plain, % 75.94/76.25 (~P3(f3(a2,x43891),f3(f9(a8,a2),x43891))), % 75.94/76.25 inference(rename_variables,[],[2719])). % 75.94/76.25 cnf(4390,plain, % 75.94/76.25 (~P3(f3(a2,a2),f3(f9(a8,a2),a1))), % 75.94/76.25 inference(scs_inference,[],[4182,3349,3552,4326,4359,2821,2926,3374,4382,3469,3192,2887,2719,4389,3474,2762,2701,81,28,30,27,25,26,2,33,31,10,11,3,12,13])). % 75.94/76.25 cnf(4407,plain, % 75.94/76.25 (~P3(f9(a2,f9(a6,a6)),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[4377,3827,3375,2934,2528,3354,130,28,30,27,25,26,2,33])). % 75.94/76.25 cnf(4413,plain, % 75.94/76.25 (E(f9(x44131,x44132),f9(x44131,f9(x44132,a8)))), % 75.94/76.25 inference(rename_variables,[],[3848])). % 75.94/76.25 cnf(4419,plain, % 75.94/76.25 (~P3(f9(f9(a8,a2),f9(a6,a6)),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[3924,4377,3827,4318,649,436,4355,3375,3333,2934,2528,3426,3354,3848,4413,130,28,30,27,25,26,2,33,31,10,11,3,12])). % 75.94/76.25 cnf(4421,plain, % 75.94/76.25 (~P3(f3(a2,a2),f3(f9(a8,a2),f9(a8,a2)))), % 75.94/76.25 inference(scs_inference,[],[3924,4377,3827,4318,649,436,4355,4390,3375,3333,3417,2934,2528,3426,3354,3848,4413,130,28,30,27,25,26,2,33,31,10,11,3,12,13])). % 75.94/76.25 cnf(4445,plain, % 75.94/76.25 (E(f4(a2,x44451),f4(f9(a8,a2),x44451))), % 75.94/76.25 inference(rename_variables,[],[3468])). % 75.94/76.25 cnf(4449,plain, % 75.94/76.25 (~E(f9(a8,a2),f9(a6,a1))), % 75.94/76.25 inference(scs_inference,[],[3308,3344,4407,2619,2828,2938,3769,3468,4445,2946,3299,2690,60,28,30,27,25,26,2,33,31,10,11,3])). % 75.94/76.25 cnf(4456,plain, % 75.94/76.25 (E(f3(f9(a6,a8),f9(a6,a8)),a10)), % 75.94/76.25 inference(scs_inference,[],[3308,3344,4407,2619,2828,2938,3769,3355,3468,4445,3470,3811,2946,3265,3299,2690,60,28,30,27,25,26,2,33,31,10,11,3,12,13,3868])). % 75.94/76.25 cnf(4475,plain, % 75.94/76.25 (~E(f9(a6,a1),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[4449,4419,3507,2499,2507,54,28,30,27,25,26,2])). % 75.94/76.25 cnf(4477,plain, % 75.94/76.25 (E(f9(f9(a2,a8),x44771),f9(a1,x44771))), % 75.94/76.25 inference(rename_variables,[],[3512])). % 75.94/76.25 cnf(4489,plain, % 75.94/76.25 (~P3(f9(f9(a2,a8),f9(a6,a8)),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[4449,3515,4073,4419,4189,3507,3336,3347,3813,2499,2507,2535,2348,3512,4477,3624,1026,3391,54,28,30,27,25,26,2,15,33,31,10,11,3,12])). % 75.94/76.25 cnf(4493,plain, % 75.94/76.25 (E(f3(f9(a8,a6),f9(a8,a6)),a10)), % 75.94/76.25 inference(scs_inference,[],[4449,3515,4073,4419,4189,4421,3507,3336,3347,3813,3360,2499,2507,2535,2348,1717,3512,4477,3624,1026,1927,3391,54,28,30,27,25,26,2,15,33,31,10,11,3,12,13,36])). % 75.94/76.25 cnf(4514,plain, % 75.94/76.25 (~P1(f9(a6,a1),f9(a8,a2))), % 75.94/76.25 inference(scs_inference,[],[4475,4489,2627,3658,2520,3342,3036,128,63,28,30,27,25,26,2,33,31])). % 75.94/76.25 cnf(4526,plain, % 75.94/76.25 (~P3(f3(f9(a8,a2),f9(a1,a8)),f3(a2,a2))), % 75.94/76.25 inference(scs_inference,[],[4475,4489,2627,3943,4092,3658,3660,3661,4493,3699,3247,2520,3342,2729,3036,128,153,63,28,30,27,25,26,2,33,31,10,11,3,12,13])). % 75.94/76.25 cnf(4549,plain, % 75.94/76.25 ($false), % 75.94/76.25 inference(scs_inference,[],[4514,4526,2635,4348,4456,4169,334,3511,3621,2543,2474,3623,682,3268,30,27,25,26,2,33,31,10,11,3]), % 75.94/76.25 ['proof']). % 75.94/76.25 % SZS output end Proof % 75.94/76.25 % Total time :75.440000s %------------------------------------------------------------------------------