%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV488+2 : 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 : n024.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 62.99s 63.04s % Output : CNFRefutation 62.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV488+2 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 18:30:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 62.91/63.02 %------------------------------------------- % 62.91/63.02 % File :CSE---1.7 % 62.91/63.02 % Problem :theBenchmark % 62.91/63.02 % Transform :cnf % 62.91/63.02 % Format :tptp:raw % 62.91/63.02 % Command :java -jar mcs_scs.jar %d %s % 62.91/63.02 % 62.91/63.02 % Result :Theorem 62.400000s % 62.91/63.02 % Output :CNFRefutation 62.400000s % 62.91/63.02 %------------------------------------------- % 62.99/63.03 %------------------------------------------------------------------------------ % 62.99/63.03 % File : SWV488+2 : TPTP v8.2.0. Released v4.0.0. % 62.99/63.03 % Domain : Software Verification % 62.99/63.03 % Problem : Matrix has no zero on the diagonal % 62.99/63.03 % Version : Especial. % 62.99/63.03 % English : % 62.99/63.03 % 62.99/63.03 % Refs : [KV09] Kovacs (2009), Email to Geoff Sutcliffe % 62.99/63.03 % Source : [KV09] % 62.99/63.03 % Names : getL2 [KV09] % 62.99/63.03 % 62.99/63.03 % Status : Theorem % 62.99/63.03 % Rating : 0.11 v8.2.0, 0.08 v8.1.0, 0.11 v7.5.0, 0.16 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.17 v6.0.0, 0.13 v5.5.0, 0.15 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.05 v5.0.0, 0.08 v4.1.0, 0.13 v4.0.0 % 62.99/63.03 % Syntax : Number of formulae : 13 ( 4 unt; 0 def) % 62.99/63.03 % Number of atoms : 44 ( 13 equ) % 62.99/63.03 % Maximal formula atoms : 17 ( 3 avg) % 62.99/63.03 % Number of connectives : 34 ( 3 ~; 2 |; 15 &) % 62.99/63.03 % ( 3 <=>; 11 =>; 0 <=; 0 <~>) % 62.99/63.03 % Maximal formula depth : 11 ( 5 avg) % 62.99/63.03 % Maximal term depth : 3 ( 1 avg) % 62.99/63.03 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty) % 62.99/63.03 % Number of functors : 8 ( 8 usr; 5 con; 0-2 aty) % 62.99/63.03 % Number of variables : 29 ( 28 !; 1 ?) % 62.99/63.03 % SPC : FOF_THM_RFO_SEQ % 62.99/63.03 % 62.99/63.03 % Comments : % 62.99/63.03 %------------------------------------------------------------------------------ % 62.99/63.03 fof(int_leq,axiom, % 62.99/63.03 ! [I,J] : % 62.99/63.03 ( int_leq(I,J) % 62.99/63.03 <=> ( int_less(I,J) % 62.99/63.03 | I = J ) ) ). % 62.99/63.03 % 62.99/63.03 fof(int_less_transitive,axiom, % 62.99/63.03 ! [I,J,K] : % 62.99/63.03 ( ( int_less(I,J) % 62.99/63.03 & int_less(J,K) ) % 62.99/63.03 => int_less(I,K) ) ). % 62.99/63.03 % 62.99/63.03 fof(int_less_irreflexive,axiom, % 62.99/63.03 ! [I,J] : % 62.99/63.03 ( int_less(I,J) % 62.99/63.03 => I != J ) ). % 62.99/63.03 % 62.99/63.03 fof(int_less_total,axiom, % 62.99/63.03 ! [I,J] : % 62.99/63.03 ( int_less(I,J) % 62.99/63.03 | int_leq(J,I) ) ). % 62.99/63.03 % 62.99/63.03 fof(int_zero_one,axiom, % 62.99/63.03 int_less(int_zero,int_one) ). % 62.99/63.03 % 62.99/63.03 fof(plus_commutative,axiom, % 62.99/63.03 ! [I,J] : plus(I,J) = plus(J,I) ). % 62.99/63.03 % 62.99/63.03 fof(plus_zero,axiom, % 62.99/63.03 ! [I] : plus(I,int_zero) = I ). % 62.99/63.03 % 62.99/63.03 fof(plus_and_order1,axiom, % 62.99/63.03 ! [I1,J1,I2,J2] : % 62.99/63.03 ( ( int_less(I1,J1) % 62.99/63.03 & int_leq(I2,J2) ) % 62.99/63.03 => int_leq(plus(I1,I2),plus(J1,J2)) ) ). % 62.99/63.03 % 62.99/63.03 fof(plus_and_inverse,axiom, % 62.99/63.03 ! [I,J] : % 62.99/63.03 ( int_less(I,J) % 62.99/63.03 <=> ? [K] : % 62.99/63.03 ( plus(I,K) = J % 62.99/63.03 & int_less(int_zero,K) ) ) ). % 62.99/63.03 % 62.99/63.03 fof(one_successor_of_zero,axiom, % 62.99/63.03 ! [I] : % 62.99/63.03 ( int_less(int_zero,I) % 62.99/63.03 <=> int_leq(int_one,I) ) ). % 62.99/63.03 % 62.99/63.03 fof(real_constants,axiom, % 62.99/63.03 real_zero != real_one ). % 62.99/63.03 % 62.99/63.03 fof(qil,hypothesis, % 62.99/63.03 ! [I,J] : % 62.99/63.03 ( ( int_leq(int_one,I) % 62.99/63.03 & int_leq(I,n) % 62.99/63.03 & int_leq(int_one,J) % 62.99/63.03 & int_leq(J,n) ) % 62.99/63.03 => ( ! [C] : % 62.99/63.03 ( ( int_less(int_zero,C) % 62.99/63.03 & I = plus(J,C) ) % 62.99/63.03 => ! [K] : % 62.99/63.03 ( ( int_leq(int_one,K) % 62.99/63.03 & int_leq(K,J) ) % 62.99/63.03 => a(plus(K,C),K) = lu(plus(K,C),K) ) ) % 62.99/63.03 & ! [K] : % 62.99/63.03 ( ( int_leq(int_one,K) % 62.99/63.04 & int_leq(K,J) ) % 62.99/63.04 => a(K,K) = real_one ) % 62.99/63.04 & ! [C] : % 62.99/63.04 ( ( int_less(int_zero,C) % 62.99/63.04 & J = plus(I,C) ) % 62.99/63.04 => ! [K] : % 62.99/63.04 ( ( int_leq(int_one,K) % 62.99/63.04 & int_leq(K,I) ) % 62.99/63.04 => a(K,plus(K,C)) = real_zero ) ) ) ) ). % 62.99/63.04 % 62.99/63.04 fof(lti,conjecture, % 62.99/63.04 ! [I,J] : % 62.99/63.04 ( ( int_leq(int_one,I) % 62.99/63.04 & int_leq(I,J) % 62.99/63.04 & int_leq(J,n) ) % 62.99/63.04 => ( I = J % 62.99/63.04 => a(I,J) != real_zero ) ) ). % 62.99/63.04 % 62.99/63.04 %------------------------------------------------------------------------------ % 62.99/63.04 %------------------------------------------- % 62.99/63.04 % Proof found % 62.99/63.04 % SZS status Theorem for theBenchmark % 62.99/63.04 % SZS output start Proof % 62.99/63.04 %ClaNum:42(EqnAxiom:17) % 62.99/63.04 %VarNum:102(SingletonVarNum:42) % 62.99/63.04 %MaxLitNum:6 % 62.99/63.04 %MaxfuncDepth:2 % 62.99/63.04 %SharedTerms:15 % 62.99/63.04 %goalClause: 18 19 20 21 22 % 62.99/63.04 %singleGoalClaCount:5 % 62.99/63.04 [18]E(a1,a2) % 62.99/63.04 [20]P1(a6,a2) % 62.99/63.04 [21]P1(a2,a1) % 62.99/63.04 [22]P1(a1,a7) % 62.99/63.04 [23]P3(a8,a6) % 62.99/63.04 [26]~E(a11,a5) % 62.99/63.04 [19]E(f3(a2,a1),a5) % 62.99/63.04 [24]E(f10(x241,a8),x241) % 62.99/63.04 [25]E(f10(x251,x252),f10(x252,x251)) % 62.99/63.04 [30]~P3(a8,x301)+P1(a6,x301) % 62.99/63.04 [31]~P1(a6,x311)+P3(a8,x311) % 62.99/63.04 [27]~E(x271,x272)+P1(x271,x272) % 62.99/63.04 [28]~P3(x281,x282)+~E(x281,x282) % 62.99/63.04 [29]P3(x292,x291)+P1(x291,x292) % 62.99/63.04 [32]~P3(x321,x322)+P1(x321,x322) % 62.99/63.04 [36]~P3(x361,x362)+P3(a8,f4(x361,x362)) % 62.99/63.04 [37]~P3(x371,x372)+E(f10(x371,f4(x371,x372)),x372) % 62.99/63.04 [33]P3(x331,x332)+~P1(x331,x332)+E(x331,x332) % 62.99/63.04 [35]~P3(x351,x353)+P3(x351,x352)+~P3(x353,x352) % 62.99/63.04 [34]P3(x341,x342)+~P3(a8,x343)+~E(f10(x341,x343),x342) % 62.99/63.04 [40]~P1(x402,x404)+~P3(x401,x403)+P1(f10(x401,x402),f10(x403,x404)) % 62.99/63.04 [38]~P1(x381,x382)+~P2(x383,x382)+~P1(a6,x381)+E(f3(x381,x381),a11) % 62.99/63.04 [39]P2(x391,x392)+~P1(x392,a7)+~P1(x391,a7)+~P1(a6,x392)+~P1(a6,x391) % 62.99/63.04 [41]~P1(x411,x414)+~P2(x414,x413)+~P1(a6,x411)+~P3(a8,x412)+~E(x413,f10(x414,x412))+E(f3(x411,f10(x411,x412)),a5) % 62.99/63.04 [42]~P1(x421,x424)+~P2(x423,x424)+~P1(a6,x421)+~P3(a8,x422)+~E(x423,f10(x424,x422))+E(f9(f10(x421,x422),x421),f3(f10(x421,x422),x421)) % 62.99/63.04 %EqnAxiom % 62.99/63.04 [1]E(x11,x11) % 62.99/63.04 [2]E(x22,x21)+~E(x21,x22) % 62.99/63.04 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 62.99/63.04 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 62.99/63.04 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 62.99/63.04 [6]~E(x61,x62)+E(f10(x61,x63),f10(x62,x63)) % 62.99/63.04 [7]~E(x71,x72)+E(f10(x73,x71),f10(x73,x72)) % 62.99/63.04 [8]~E(x81,x82)+E(f9(x81,x83),f9(x82,x83)) % 62.99/63.04 [9]~E(x91,x92)+E(f9(x93,x91),f9(x93,x92)) % 62.99/63.04 [10]~E(x101,x102)+E(f4(x101,x103),f4(x102,x103)) % 62.99/63.04 [11]~E(x111,x112)+E(f4(x113,x111),f4(x113,x112)) % 62.99/63.04 [12]P1(x122,x123)+~E(x121,x122)+~P1(x121,x123) % 62.99/63.04 [13]P1(x133,x132)+~E(x131,x132)+~P1(x133,x131) % 62.99/63.04 [14]P3(x142,x143)+~E(x141,x142)+~P3(x141,x143) % 62.99/63.04 [15]P3(x153,x152)+~E(x151,x152)+~P3(x153,x151) % 62.99/63.04 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163) % 62.99/63.04 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171) % 62.99/63.04 % 62.99/63.04 %------------------------------------------- % 62.99/63.05 cnf(43,plain, % 62.99/63.05 (P1(x431,x431)), % 62.99/63.05 inference(equality_inference,[],[27])). % 62.99/63.05 cnf(44,plain, % 62.99/63.05 (~P3(x441,x441)), % 62.99/63.05 inference(equality_inference,[],[28])). % 62.99/63.05 cnf(45,plain, % 62.99/63.05 (P3(x451,f10(x451,x452))+~P3(a8,x452)), % 62.99/63.05 inference(equality_inference,[],[34])). % 62.99/63.05 cnf(48,plain, % 62.99/63.05 (~P3(a1,a2)), % 62.99/63.05 inference(scs_inference,[],[18,28])). % 62.99/63.05 cnf(50,plain, % 62.99/63.05 (E(a2,a1)), % 62.99/63.05 inference(scs_inference,[],[18,28,2])). % 62.99/63.05 cnf(51,plain, % 62.99/63.05 (~P1(a6,a8)), % 62.99/63.05 inference(scs_inference,[],[18,44,28,2,31])). % 62.99/63.05 cnf(52,plain, % 62.99/63.05 (~P3(x521,x521)), % 62.99/63.05 inference(rename_variables,[],[44])). % 62.99/63.05 cnf(54,plain, % 62.99/63.05 (~P3(a6,a8)), % 62.99/63.05 inference(scs_inference,[],[18,44,28,2,31,32])). % 62.99/63.05 cnf(56,plain, % 62.99/63.05 (P3(x561,f10(x561,a6))), % 62.99/63.05 inference(scs_inference,[],[18,44,23,28,2,31,32,45])). % 62.99/63.05 cnf(58,plain, % 62.99/63.05 (E(f10(a1,a8),a2)), % 62.99/63.05 inference(scs_inference,[],[18,44,24,23,28,2,31,32,45,3])). % 62.99/63.05 cnf(60,plain, % 62.99/63.05 (P1(a2,a7)), % 62.99/63.05 inference(scs_inference,[],[18,22,44,24,23,28,2,31,32,45,3,12])). % 62.99/63.05 cnf(61,plain, % 62.99/63.05 (~E(a2,a8)), % 62.99/63.05 inference(scs_inference,[],[18,20,22,44,24,23,28,2,31,32,45,3,12,13])). % 62.99/63.05 cnf(62,plain, % 62.99/63.05 (P3(x621,f10(a6,x621))), % 62.99/63.05 inference(scs_inference,[],[18,20,22,44,25,24,23,28,2,31,32,45,3,12,13,34])). % 62.99/63.05 cnf(65,plain, % 62.99/63.05 (P3(a8,f10(a6,a6))), % 62.99/63.05 inference(scs_inference,[],[18,20,22,44,25,24,23,28,2,31,32,45,3,12,13,34,35])). % 62.99/63.05 cnf(68,plain, % 62.99/63.05 (~P3(x681,x681)), % 62.99/63.05 inference(rename_variables,[],[44])). % 62.99/63.05 cnf(71,plain, % 62.99/63.05 (P2(a2,a2)), % 62.99/63.05 inference(scs_inference,[],[18,20,22,44,52,68,25,24,23,28,2,31,32,45,3,12,13,34,35,14,15,39])). % 62.99/63.05 cnf(75,plain, % 62.99/63.05 (P2(a1,a2)), % 62.99/63.05 inference(scs_inference,[],[18,20,22,44,52,68,25,24,23,28,2,31,32,45,3,12,13,34,35,14,15,39,33,16])). % 62.99/63.05 cnf(76,plain, % 62.99/63.05 (P2(a2,a1)), % 62.99/63.05 inference(scs_inference,[],[18,20,22,44,52,68,25,24,23,28,2,31,32,45,3,12,13,34,35,14,15,39,33,16,17])). % 62.99/63.05 cnf(81,plain, % 62.99/63.05 (P3(x811,f10(x811,f10(a8,a6)))), % 62.99/63.05 inference(scs_inference,[],[56,45])). % 62.99/63.05 cnf(82,plain, % 62.99/63.05 (P3(x821,f10(x821,a6))), % 62.99/63.05 inference(rename_variables,[],[56])). % 62.99/63.05 cnf(84,plain, % 62.99/63.05 (~P3(f3(a2,a1),a5)), % 62.99/63.05 inference(scs_inference,[],[19,56,45,28])). % 62.99/63.05 cnf(86,plain, % 62.99/63.05 (E(a5,f3(a2,a1))), % 62.99/63.05 inference(scs_inference,[],[19,56,45,28,2])). % 62.99/63.05 cnf(87,plain, % 62.99/63.05 (P3(x871,f10(f10(a6,x871),a6))), % 62.99/63.05 inference(scs_inference,[],[19,56,82,62,45,28,2,35])). % 62.99/63.05 cnf(88,plain, % 62.99/63.05 (P3(x881,f10(x881,a6))), % 62.99/63.05 inference(rename_variables,[],[56])). % 62.99/63.05 cnf(90,plain, % 62.99/63.05 (P3(x901,f10(f10(a8,a6),x901))), % 62.99/63.05 inference(scs_inference,[],[19,56,82,88,62,25,45,28,2,35,34])). % 62.99/63.05 cnf(92,plain, % 62.99/63.05 (P3(x921,f10(x921,a6))), % 62.99/63.05 inference(rename_variables,[],[56])). % 62.99/63.05 cnf(97,plain, % 62.99/63.05 (~E(a11,f3(a2,a1))), % 62.99/63.05 inference(scs_inference,[],[19,50,44,56,82,88,92,62,26,76,25,45,28,2,35,34,16,14,3])). % 62.99/63.05 cnf(98,plain, % 62.99/63.05 (~E(f10(a1,a6),a2)), % 62.99/63.05 inference(scs_inference,[],[19,48,50,44,56,82,88,92,62,26,76,25,45,28,2,35,34,16,14,3,15])). % 62.99/63.05 cnf(103,plain, % 62.99/63.05 (P1(x1031,a2)+~E(a6,x1031)), % 62.99/63.05 inference(scs_inference,[],[19,22,20,48,50,44,56,82,88,92,62,26,76,25,45,28,2,35,34,16,14,3,15,33,13,12])). % 62.99/63.05 cnf(110,plain, % 62.99/63.05 (P3(x1101,f10(x1101,f10(f10(a8,a6),a8)))), % 62.99/63.05 inference(scs_inference,[],[90,45])). % 62.99/63.05 cnf(111,plain, % 62.99/63.05 (P3(x1111,f10(f10(a8,a6),x1111))), % 62.99/63.05 inference(rename_variables,[],[90])). % 62.99/63.05 cnf(113,plain, % 62.99/63.05 (~P3(f10(a1,a8),a2)), % 62.99/63.05 inference(scs_inference,[],[58,90,45,28])). % 62.99/63.05 cnf(115,plain, % 62.99/63.05 (E(a2,f10(a1,a8))), % 62.99/63.05 inference(scs_inference,[],[58,90,45,28,2])). % 62.99/63.05 cnf(116,plain, % 62.99/63.05 (P3(x1161,f10(f10(f10(a8,a6),a8),x1161))), % 62.99/63.05 inference(scs_inference,[],[58,90,111,25,45,28,2,34])). % 62.99/63.05 cnf(118,plain, % 62.99/63.05 (P3(x1181,f10(f10(a8,a6),x1181))), % 62.99/63.05 inference(rename_variables,[],[90])). % 62.99/63.05 cnf(120,plain, % 62.99/63.05 (P3(x1201,f10(f10(a8,a6),f10(x1201,f10(a8,a6))))), % 62.99/63.05 inference(scs_inference,[],[58,90,111,118,81,25,45,28,2,34,35])). % 62.99/63.05 cnf(121,plain, % 62.99/63.05 (P3(x1211,f10(f10(a8,a6),x1211))), % 62.99/63.05 inference(rename_variables,[],[90])). % 62.99/63.05 cnf(126,plain, % 62.99/63.05 (~E(f10(f10(a8,a6),f3(a2,a1)),a5)), % 62.99/63.05 inference(scs_inference,[],[18,58,84,44,90,111,118,121,81,98,25,45,28,2,34,35,14,3,15])). % 62.99/63.05 cnf(130,plain, % 62.99/63.05 (P1(a2,x1301)+~E(a7,x1301)), % 62.99/63.05 inference(scs_inference,[],[18,60,58,84,44,90,111,118,121,81,98,25,45,28,2,34,35,14,3,15,33,13])). % 62.99/63.05 cnf(137,plain, % 62.99/63.05 (P3(x1371,f10(x1371,f10(f10(a6,a8),a6)))), % 62.99/63.05 inference(scs_inference,[],[87,45])). % 62.99/63.05 cnf(142,plain, % 62.99/63.05 (E(x1421,f10(x1421,a8))), % 62.99/63.05 inference(scs_inference,[],[86,87,24,45,28,2])). % 62.99/63.05 cnf(143,plain, % 62.99/63.05 (P2(a2,f10(a1,a8))), % 62.99/63.05 inference(scs_inference,[],[86,115,71,87,24,45,28,2,17])). % 62.99/63.05 cnf(144,plain, % 62.99/63.05 (~P3(f10(a6,a6),a8)), % 62.99/63.05 inference(scs_inference,[],[86,115,44,71,87,65,24,45,28,2,17,35])). % 62.99/63.05 cnf(145,plain, % 62.99/63.05 (~P3(x1451,x1451)), % 62.99/63.05 inference(rename_variables,[],[44])). % 62.99/63.05 cnf(147,plain, % 62.99/63.05 (P2(f10(a1,a8),a2)), % 62.99/63.05 inference(scs_inference,[],[86,115,44,71,87,65,24,45,28,2,17,35,16])). % 62.99/63.05 cnf(148,plain, % 62.99/63.05 (P1(a1,f10(a7,a8))), % 62.99/63.05 inference(scs_inference,[],[22,86,115,44,71,87,65,24,45,28,2,17,35,16,13])). % 62.99/63.05 cnf(149,plain, % 62.99/63.05 (~E(x1491,f10(f10(a8,a6),f10(x1491,f10(a8,a6))))), % 62.99/63.05 inference(scs_inference,[],[22,86,115,44,145,71,120,87,65,24,45,28,2,17,35,16,13,14])). % 62.99/63.05 cnf(152,plain, % 62.99/63.05 (P1(f10(a1,a8),a1)), % 62.99/63.05 inference(scs_inference,[],[21,22,19,86,115,44,145,71,120,87,126,65,24,45,28,2,17,35,16,13,14,3,12])). % 62.99/63.05 cnf(153,plain, % 62.99/63.05 (~E(f10(f10(a8,a6),f10(f10(a1,a8),f10(a8,a6))),a2)), % 62.99/63.05 inference(scs_inference,[],[21,22,19,86,113,115,44,145,71,120,87,126,65,24,45,28,2,17,35,16,13,14,3,12,15])). % 62.99/63.05 cnf(161,plain, % 62.99/63.05 (P1(f10(a6,a8),a2)), % 62.99/63.05 inference(scs_inference,[],[142,103])). % 62.99/63.05 cnf(162,plain, % 62.99/63.05 (E(x1621,f10(x1621,a8))), % 62.99/63.05 inference(rename_variables,[],[142])). % 62.99/63.05 cnf(165,plain, % 62.99/63.05 (P3(x1651,f10(x1651,f10(a8,f10(a8,a6))))), % 62.99/63.05 inference(scs_inference,[],[142,149,81,103,7,45])). % 62.99/63.05 cnf(168,plain, % 62.99/63.05 (~P3(x1681,f10(x1681,a8))), % 62.99/63.05 inference(scs_inference,[],[142,162,149,81,103,7,45,28])). % 62.99/63.05 cnf(170,plain, % 62.99/63.05 (P2(a1,f10(a2,a8))), % 62.99/63.05 inference(scs_inference,[],[142,162,75,149,81,103,7,45,28,17])). % 62.99/63.05 cnf(171,plain, % 62.99/63.05 (E(x1711,f10(x1711,a8))), % 62.99/63.05 inference(rename_variables,[],[142])). % 62.99/63.05 cnf(172,plain, % 62.99/63.05 (P2(f10(a2,a8),a1)), % 62.99/63.05 inference(scs_inference,[],[142,162,171,75,76,149,81,103,7,45,28,17,16])). % 62.99/63.05 cnf(173,plain, % 62.99/63.05 (E(x1731,f10(x1731,a8))), % 62.99/63.05 inference(rename_variables,[],[142])). % 62.99/63.05 cnf(174,plain, % 62.99/63.05 (P1(a1,f10(f10(a7,a8),a8))), % 62.99/63.05 inference(scs_inference,[],[142,162,171,173,148,75,76,149,81,103,7,45,28,17,16,13])). % 62.99/63.05 cnf(175,plain, % 62.99/63.05 (E(x1751,f10(x1751,a8))), % 62.99/63.05 inference(rename_variables,[],[142])). % 62.99/63.05 cnf(178,plain, % 62.99/63.05 (P1(f10(a2,a8),a1)), % 62.99/63.05 inference(scs_inference,[],[21,142,162,171,173,175,148,44,75,76,149,116,81,103,7,45,28,17,16,13,14,12])). % 62.99/63.05 cnf(190,plain, % 62.99/63.05 (~P1(a6,f10(a8,a8))), % 62.99/63.05 inference(scs_inference,[],[168,31])). % 62.99/63.05 cnf(191,plain, % 62.99/63.05 (~P3(x1911,f10(x1911,a8))), % 62.99/63.05 inference(rename_variables,[],[168])). % 62.99/63.05 cnf(193,plain, % 62.99/63.05 (~P3(a6,f10(a8,a8))), % 62.99/63.05 inference(scs_inference,[],[168,31,32])). % 62.99/63.05 cnf(195,plain, % 62.99/63.05 (P3(x1951,f10(x1951,f10(a6,a6)))), % 62.99/63.05 inference(scs_inference,[],[168,65,31,32,45])). % 62.99/63.05 cnf(197,plain, % 62.99/63.05 (~P3(a2,a1)), % 62.99/63.05 inference(scs_inference,[],[50,168,65,31,32,45,28])). % 62.99/63.05 cnf(202,plain, % 62.99/63.05 (P3(x2021,f10(f10(x2021,f10(a6,a6)),a8))), % 62.99/63.05 inference(scs_inference,[],[50,168,142,65,165,31,32,45,28,35,34])). % 62.99/63.05 cnf(203,plain, % 62.99/63.05 (E(x2031,f10(x2031,a8))), % 62.99/63.05 inference(rename_variables,[],[142])). % 62.99/63.05 cnf(205,plain, % 62.99/63.05 (P2(f10(a2,a8),a2)), % 62.99/63.05 inference(scs_inference,[],[18,50,168,142,65,165,172,31,32,45,28,35,34,17])). % 62.99/63.05 cnf(206,plain, % 62.99/63.05 (P2(f10(f10(a2,a8),a8),a1)), % 62.99/63.05 inference(scs_inference,[],[18,50,168,142,203,65,165,172,31,32,45,28,35,34,17,16])). % 62.99/63.05 cnf(207,plain, % 62.99/63.05 (E(x2071,f10(x2071,a8))), % 62.99/63.05 inference(rename_variables,[],[142])). % 62.99/63.05 cnf(209,plain, % 62.99/63.05 (P1(f10(a2,a8),a2)), % 62.99/63.05 inference(scs_inference,[],[18,50,58,168,178,142,203,65,165,172,153,31,32,45,28,35,34,17,16,3,13])). % 62.99/63.05 cnf(210,plain, % 62.99/63.05 (P1(f10(f10(a2,a8),a8),a1)), % 62.99/63.05 inference(scs_inference,[],[18,50,58,168,178,142,203,207,65,165,172,153,31,32,45,28,35,34,17,16,3,13,12])). % 62.99/63.05 cnf(212,plain, % 62.99/63.05 (~E(a8,f10(a6,a6))), % 62.99/63.05 inference(scs_inference,[],[18,50,58,168,178,142,203,207,44,65,165,172,153,31,32,45,28,35,34,17,16,3,13,12,14])). % 62.99/63.05 cnf(214,plain, % 62.99/63.05 (~E(f10(a6,a6),f10(a8,a8))), % 62.99/63.05 inference(scs_inference,[],[18,50,58,168,191,178,142,203,207,44,65,165,172,153,31,32,45,28,35,34,17,16,3,13,12,14,15])). % 62.99/63.05 cnf(218,plain, % 62.99/63.05 (P3(f10(a8,a8),a6)), % 62.99/63.05 inference(scs_inference,[],[18,50,58,168,191,178,142,203,207,44,65,165,172,153,31,32,45,28,35,34,17,16,3,13,12,14,15,27,29])). % 62.99/63.05 cnf(225,plain, % 62.99/63.05 (P3(x2251,f10(x2251,f10(a8,f10(a6,a6))))), % 62.99/63.05 inference(scs_inference,[],[195,45])). % 62.99/63.05 cnf(228,plain, % 62.99/63.05 (~P3(a2,f10(a1,a8))), % 62.99/63.05 inference(scs_inference,[],[115,195,45,28])). % 62.99/63.05 cnf(233,plain, % 62.99/63.05 (P3(x2331,f10(f10(x2331,a6),a8))), % 62.99/63.05 inference(scs_inference,[],[115,142,23,110,195,45,28,35,34])). % 62.99/63.05 cnf(234,plain, % 62.99/63.05 (E(x2341,f10(x2341,a8))), % 62.99/63.05 inference(rename_variables,[],[142])). % 62.99/63.05 cnf(236,plain, % 62.99/63.05 (P2(f10(f10(a2,a8),a8),a2)), % 62.99/63.05 inference(scs_inference,[],[18,115,142,23,110,195,206,45,28,35,34,17])). % 62.99/63.05 cnf(237,plain, % 62.99/63.05 (P2(f10(f10(f10(a2,a8),a8),a8),a1)), % 62.99/63.05 inference(scs_inference,[],[18,115,142,234,23,110,195,206,45,28,35,34,17,16])). % 62.99/63.05 cnf(238,plain, % 62.99/63.05 (E(x2381,f10(x2381,a8))), % 62.99/63.05 inference(rename_variables,[],[142])). % 62.99/63.05 cnf(239,plain, % 62.99/63.05 (P1(f10(a6,a8),a1)), % 62.99/63.05 inference(scs_inference,[],[18,50,115,161,142,234,23,110,195,206,45,28,35,34,17,16,13])). % 62.99/63.05 cnf(241,plain, % 62.99/63.05 (P1(f10(f10(a6,a8),a8),a2)), % 62.99/63.05 inference(scs_inference,[],[18,50,58,115,161,142,234,238,23,110,195,206,98,45,28,35,34,17,16,13,3,12])). % 62.99/63.05 cnf(252,plain, % 62.99/63.05 (P3(x2521,f10(x2521,f10(a6,a8)))), % 62.99/63.05 inference(scs_inference,[],[62,45])). % 62.99/63.05 cnf(255,plain, % 62.99/63.05 (~P3(f10(x2551,a8),x2551)), % 62.99/63.05 inference(scs_inference,[],[24,62,45,28])). % 62.99/63.05 cnf(260,plain, % 62.99/63.05 (P3(x2601,f10(f10(a6,a6),x2601))), % 62.99/63.05 inference(scs_inference,[],[24,25,65,137,62,45,28,35,34])). % 62.99/63.05 cnf(264,plain, % 62.99/63.05 (P2(a1,f10(a1,a8))), % 62.99/63.05 inference(scs_inference,[],[18,50,24,25,65,137,237,143,62,45,28,35,34,17,16])). % 62.99/63.05 cnf(265,plain, % 62.99/63.06 (P1(a1,f10(f10(f10(a7,a8),a8),a8))), % 62.99/63.06 inference(scs_inference,[],[18,50,174,142,24,25,65,137,237,143,62,45,28,35,34,17,16,13])). % 62.99/63.06 cnf(267,plain, % 62.99/63.06 (P1(a2,f10(f10(a7,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[18,50,174,142,24,25,65,137,237,143,62,45,28,35,34,17,16,13,12])). % 62.99/63.06 cnf(280,plain, % 62.99/63.06 (P3(x2801,f10(x2801,f10(a8,f10(a6,a8))))), % 62.99/63.06 inference(scs_inference,[],[252,45])). % 62.99/63.06 cnf(281,plain, % 62.99/63.06 (P3(x2811,f10(x2811,f10(a6,a8)))), % 62.99/63.06 inference(rename_variables,[],[252])). % 62.99/63.06 cnf(283,plain, % 62.99/63.06 (~P3(f10(x2831,x2832),f10(x2832,x2831))), % 62.99/63.06 inference(scs_inference,[],[25,252,45,28])). % 62.99/63.06 cnf(285,plain, % 62.99/63.06 (~P3(f10(a6,a8),a8)), % 62.99/63.06 inference(scs_inference,[],[255,25,23,252,45,28,35])). % 62.99/63.06 cnf(288,plain, % 62.99/63.06 (P2(f10(a1,a8),a1)), % 62.99/63.06 inference(scs_inference,[],[50,255,25,23,252,147,45,28,35,17])). % 62.99/63.06 cnf(289,plain, % 62.99/63.06 (P2(a2,f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[18,50,255,25,23,252,147,170,45,28,35,17,16])). % 62.99/63.06 cnf(293,plain, % 62.99/63.06 (E(x2931,f10(x2931,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(294,plain, % 62.99/63.06 (P1(f10(f10(a6,a8),a8),a1)), % 62.99/63.06 inference(scs_inference,[],[18,50,168,255,239,267,142,293,25,23,252,281,147,170,45,28,35,17,16,15,13,12])). % 62.99/63.06 cnf(305,plain, % 62.99/63.06 (P3(x3051,f10(x3051,f10(f10(a6,a6),a8)))), % 62.99/63.06 inference(scs_inference,[],[260,45])). % 62.99/63.06 cnf(309,plain, % 62.99/63.06 (P3(x3091,f10(x3091,f10(a8,f10(a6,a8))))), % 62.99/63.06 inference(rename_variables,[],[280])). % 62.99/63.06 cnf(311,plain, % 62.99/63.06 (P2(f10(f10(a2,a8),a8),f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[115,65,280,260,236,45,35,17])). % 62.99/63.06 cnf(312,plain, % 62.99/63.06 (P2(f10(a1,a8),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[115,65,280,260,236,289,45,35,17,16])). % 62.99/63.06 cnf(315,plain, % 62.99/63.06 (P1(f10(a2,a8),f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[115,168,209,65,280,309,260,236,289,45,35,17,16,15,13])). % 62.99/63.06 cnf(316,plain, % 62.99/63.06 (P1(f10(a1,a8),a7)), % 62.99/63.06 inference(scs_inference,[],[60,115,168,209,65,280,309,260,236,289,45,35,17,16,15,13,12])). % 62.99/63.06 cnf(329,plain, % 62.99/63.06 (P3(x3291,f10(x3291,f10(a8,f10(a6,a6))))), % 62.99/63.06 inference(rename_variables,[],[225])). % 62.99/63.06 cnf(331,plain, % 62.99/63.06 (P2(f10(a1,a8),f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,23,225,312,35,17])). % 62.99/63.06 cnf(332,plain, % 62.99/63.06 (E(x3321,f10(x3321,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(334,plain, % 62.99/63.06 (E(x3341,f10(x3341,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(337,plain, % 62.99/63.06 (P1(f10(a1,a8),a2)), % 62.99/63.06 inference(scs_inference,[],[18,142,332,168,152,23,225,329,311,312,35,17,16,15,13])). % 62.99/63.06 cnf(338,plain, % 62.99/63.06 (P1(f10(f10(a2,a8),a8),f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[18,142,332,334,168,315,152,23,225,329,311,312,35,17,16,15,13,12])). % 62.99/63.06 cnf(351,plain, % 62.99/63.06 (P3(a8,f10(f10(f10(a6,a6),a6),a8))), % 62.99/63.06 inference(scs_inference,[],[65,233,35])). % 62.99/63.06 cnf(352,plain, % 62.99/63.06 (P3(x3521,f10(f10(x3521,a6),a8))), % 62.99/63.06 inference(rename_variables,[],[233])). % 62.99/63.06 cnf(354,plain, % 62.99/63.06 (P2(f10(a1,a8),f10(f10(f10(a2,a8),a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,65,233,331,35,17])). % 62.99/63.06 cnf(355,plain, % 62.99/63.06 (E(x3551,f10(x3551,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(356,plain, % 62.99/63.06 (P2(a2,f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[58,142,65,233,331,35,17,16])). % 62.99/63.06 cnf(359,plain, % 62.99/63.06 (P1(f10(f10(a2,a8),a8),a2)), % 62.99/63.06 inference(scs_inference,[],[58,142,168,338,65,233,352,331,35,17,16,15,13])). % 62.99/63.06 cnf(360,plain, % 62.99/63.06 (P1(f10(f10(f10(a2,a8),a8),a8),f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[58,142,355,168,338,65,233,352,331,35,17,16,15,13,12])). % 62.99/63.06 cnf(364,plain, % 62.99/63.06 (~E(f10(x3641,a6),x3641)), % 62.99/63.06 inference(scs_inference,[],[58,142,355,168,44,338,65,233,352,252,331,35,17,16,15,13,12,14,6])). % 62.99/63.06 cnf(373,plain, % 62.99/63.06 (P3(a8,f10(f10(a8,a6),a6))), % 62.99/63.06 inference(scs_inference,[],[23,90,35])). % 62.99/63.06 cnf(374,plain, % 62.99/63.06 (P3(x3741,f10(f10(a8,a6),x3741))), % 62.99/63.06 inference(rename_variables,[],[90])). % 62.99/63.06 cnf(377,plain, % 62.99/63.06 (P2(a1,f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[58,142,23,90,354,170,35,16,17])). % 62.99/63.06 cnf(378,plain, % 62.99/63.06 (E(x3781,f10(x3781,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(380,plain, % 62.99/63.06 (~E(f10(a2,a6),a1)), % 62.99/63.06 inference(scs_inference,[],[18,58,142,364,360,23,90,354,170,35,16,17,13,3])). % 62.99/63.06 cnf(388,plain, % 62.99/63.06 (P3(x3881,f10(x3881,f10(f10(a8,a6),a6)))), % 62.99/63.06 inference(scs_inference,[],[18,58,142,378,168,44,364,360,210,23,90,374,195,354,170,35,16,17,13,3,15,12,14,45])). % 62.99/63.06 cnf(397,plain, % 62.99/63.06 (P3(a8,f10(f10(a6,a6),f10(a6,a6)))), % 62.99/63.06 inference(scs_inference,[],[65,260,35])). % 62.99/63.06 cnf(398,plain, % 62.99/63.06 (P3(x3981,f10(f10(a6,a6),x3981))), % 62.99/63.06 inference(rename_variables,[],[260])). % 62.99/63.06 cnf(401,plain, % 62.99/63.06 (E(x4011,f10(x4011,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(402,plain, % 62.99/63.06 (~E(f10(a5,a6),f3(a2,a1))), % 62.99/63.06 inference(scs_inference,[],[19,142,364,65,260,377,35,17,3])). % 62.99/63.06 cnf(404,plain, % 62.99/63.06 (P1(f10(a1,a8),f10(a7,a8))), % 62.99/63.06 inference(scs_inference,[],[19,142,401,316,364,65,260,377,35,17,3,13])). % 62.99/63.06 cnf(405,plain, % 62.99/63.06 (E(x4051,f10(x4051,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(410,plain, % 62.99/63.06 (~E(x4101,f10(f10(a6,x4101),a6))), % 62.99/63.06 inference(scs_inference,[],[19,168,142,401,405,44,241,316,364,65,260,398,87,377,35,17,3,13,15,12,14])). % 62.99/63.06 cnf(412,plain, % 62.99/63.06 (~E(f10(a6,a6),a8)), % 62.99/63.06 inference(scs_inference,[],[19,168,142,401,405,44,241,316,364,65,260,398,87,377,35,17,3,13,15,12,14,6])). % 62.99/63.06 cnf(424,plain, % 62.99/63.06 (P3(a8,f10(a6,f10(a6,a8)))), % 62.99/63.06 inference(scs_inference,[],[23,252,410,6,35])). % 62.99/63.06 cnf(427,plain, % 62.99/63.06 (~E(f10(a2,a6),f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[58,364,23,252,410,6,35,3])). % 62.99/63.06 cnf(431,plain, % 62.99/63.06 (P1(f10(a1,a8),f10(f10(a7,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[58,168,142,404,364,23,56,252,410,6,35,3,15,13])). % 62.99/63.06 cnf(432,plain, % 62.99/63.06 (E(x4321,f10(x4321,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(437,plain, % 62.99/63.06 (P3(x4371,f10(x4371,f10(a6,f10(a6,a8))))), % 62.99/63.06 inference(scs_inference,[],[58,168,142,432,44,404,294,364,23,56,252,81,410,6,35,3,15,13,12,14,45])). % 62.99/63.06 cnf(446,plain, % 62.99/63.06 (P3(a8,f10(f10(a8,a6),f10(a6,a6)))), % 62.99/63.06 inference(scs_inference,[],[65,90,35])). % 62.99/63.06 cnf(455,plain, % 62.99/63.06 (P3(x4551,f10(x4551,f10(f10(a8,a6),f10(a6,a6))))), % 62.99/63.06 inference(scs_inference,[],[168,142,44,431,65,90,195,388,35,13,15,14,45])). % 62.99/63.06 cnf(466,plain, % 62.99/63.06 (P1(f10(a6,a8),a6)), % 62.99/63.06 inference(scs_inference,[],[23,142,30,12])). % 62.99/63.06 cnf(467,plain, % 62.99/63.06 (P3(a8,f10(f10(a6,a6),a6))), % 62.99/63.06 inference(scs_inference,[],[65,56,35])). % 62.99/63.06 cnf(472,plain, % 62.99/63.06 (P1(f10(f10(a6,a8),a8),a6)), % 62.99/63.06 inference(scs_inference,[],[86,142,364,466,65,56,35,3,12])). % 62.99/63.06 cnf(473,plain, % 62.99/63.06 (E(x4731,f10(x4731,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(474,plain, % 62.99/63.06 (~E(f10(a6,x4741),f10(x4741,a8))), % 62.99/63.06 inference(scs_inference,[],[86,168,142,364,466,65,56,62,35,3,12,15])). % 62.99/63.06 cnf(476,plain, % 62.99/63.06 (P1(f10(f10(a6,a8),a8),f10(a6,a8))), % 62.99/63.06 inference(scs_inference,[],[86,168,142,473,364,466,65,56,62,35,3,12,15,13])). % 62.99/63.06 cnf(480,plain, % 62.99/63.06 (P3(x4801,f10(x4801,f10(f10(a6,a6),a6)))), % 62.99/63.06 inference(scs_inference,[],[86,168,142,473,364,44,466,65,56,62,455,35,3,12,15,13,14,45])). % 62.99/63.06 cnf(489,plain, % 62.99/63.06 (P3(a8,f10(a6,f10(a8,a6)))), % 62.99/63.06 inference(scs_inference,[],[23,81,35])). % 62.99/63.06 cnf(500,plain, % 62.99/63.06 (P3(x5001,f10(x5001,f10(a6,f10(a8,a6))))), % 62.99/63.06 inference(scs_inference,[],[115,168,142,364,44,476,23,87,81,480,35,12,3,15,14,45])). % 62.99/63.06 cnf(509,plain, % 62.99/63.06 (P3(a8,f10(f10(a6,a6),f10(a6,a8)))), % 62.99/63.06 inference(scs_inference,[],[65,252,35])). % 62.99/63.06 cnf(518,plain, % 62.99/63.06 (P3(x5181,f10(x5181,f10(f10(a6,a6),f10(a6,a8))))), % 62.99/63.06 inference(scs_inference,[],[168,142,472,44,65,252,81,500,35,12,15,14,45])). % 62.99/63.06 cnf(529,plain, % 62.99/63.06 (P3(a8,f10(a6,f10(a6,a6)))), % 62.99/63.06 inference(scs_inference,[],[23,195,35])). % 62.99/63.06 cnf(533,plain, % 62.99/63.06 (P3(x5331,f10(x5331,f10(f10(a6,a6),f10(a6,a8))))), % 62.99/63.06 inference(rename_variables,[],[518])). % 62.99/63.06 cnf(536,plain, % 62.99/63.06 (~E(f10(f10(a6,a6),f10(a6,a8)),a8)), % 62.99/63.06 inference(scs_inference,[],[168,44,23,195,518,533,35,15,14,7])). % 62.99/63.06 cnf(537,plain, % 62.99/63.06 (P3(x5371,f10(x5371,f10(a6,f10(a6,a6))))), % 62.99/63.06 inference(scs_inference,[],[168,44,23,195,518,533,35,15,14,7,45])). % 62.99/63.06 cnf(565,plain, % 62.99/63.06 (~P3(f10(f10(a6,a6),a6),a8)), % 62.99/63.06 inference(scs_inference,[],[44,467,35])). % 62.99/63.06 cnf(568,plain, % 62.99/63.06 (~E(f10(f10(a6,a6),a6),f10(a8,a8))), % 62.99/63.06 inference(scs_inference,[],[168,44,467,35,15])). % 62.99/63.06 cnf(582,plain, % 62.99/63.06 (~P3(x5821,x5821)), % 62.99/63.06 inference(rename_variables,[],[44])). % 62.99/63.06 cnf(586,plain, % 62.99/63.06 (~E(f10(f10(a8,a6),a6),f10(a8,a8))), % 62.99/63.06 inference(scs_inference,[],[168,44,582,373,35,14,15])). % 62.99/63.06 cnf(597,plain, % 62.99/63.06 (P3(a8,f10(f10(a6,a6),f10(a8,a6)))), % 62.99/63.06 inference(scs_inference,[],[65,81,35])). % 62.99/63.06 cnf(600,plain, % 62.99/63.06 (~E(f10(f10(a6,a6),f10(a6,a6)),f10(a8,a8))), % 62.99/63.06 inference(scs_inference,[],[168,65,81,397,35,15])). % 62.99/63.06 cnf(615,plain, % 62.99/63.06 (~P3(f10(a6,f10(a6,a6)),a8)), % 62.99/63.06 inference(scs_inference,[],[44,529,35])). % 62.99/63.06 cnf(631,plain, % 62.99/63.06 (P2(f10(a2,a8),f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,356,16])). % 62.99/63.06 cnf(632,plain, % 62.99/63.06 (E(x6321,f10(x6321,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(633,plain, % 62.99/63.06 (~P3(f10(a6,f10(a6,a8)),a8)), % 62.99/63.06 inference(scs_inference,[],[142,44,356,424,16,35])). % 62.99/63.06 cnf(636,plain, % 62.99/63.06 (P2(f10(a2,a8),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[142,632,44,356,205,424,16,35,17])). % 62.99/63.06 cnf(637,plain, % 62.99/63.06 (E(x6371,f10(x6371,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(639,plain, % 62.99/63.06 (E(x6391,f10(x6391,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(640,plain, % 62.99/63.06 (P1(f10(a2,a8),a7)), % 62.99/63.06 inference(scs_inference,[],[60,142,632,637,639,359,44,356,205,424,16,35,17,13,12])). % 62.99/63.06 cnf(655,plain, % 62.99/63.06 (P2(f10(f10(a2,a8),a8),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[142,636,16])). % 62.99/63.06 cnf(656,plain, % 62.99/63.06 (E(x6561,f10(x6561,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(661,plain, % 62.99/63.06 (E(x6611,f10(x6611,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(662,plain, % 62.99/63.06 (P1(f10(a2,a8),f10(a7,a8))), % 62.99/63.06 inference(scs_inference,[],[142,656,661,44,640,489,636,631,16,35,17,13])). % 62.99/63.06 cnf(680,plain, % 62.99/63.06 (E(x6801,f10(x6801,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(681,plain, % 62.99/63.06 (~P3(f10(f10(a6,a6),f10(a6,a8)),a8)), % 62.99/63.06 inference(scs_inference,[],[142,44,509,655,16,35])). % 62.99/63.06 cnf(685,plain, % 62.99/63.06 (E(x6851,f10(x6851,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(687,plain, % 62.99/63.06 (E(x6871,f10(x6871,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(688,plain, % 62.99/63.06 (P1(f10(f10(a2,a8),a8),f10(a7,a8))), % 62.99/63.06 inference(scs_inference,[],[142,680,685,687,44,662,509,655,16,35,17,13,12])). % 62.99/63.06 cnf(704,plain, % 62.99/63.06 (P1(f10(f10(a2,a8),a8),f10(f10(a7,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,44,688,446,35,13])). % 62.99/63.06 cnf(705,plain, % 62.99/63.06 (E(x7051,f10(x7051,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(706,plain, % 62.99/63.06 (P1(f10(f10(f10(a2,a8),a8),a8),f10(a7,a8))), % 62.99/63.06 inference(scs_inference,[],[142,705,44,688,446,35,13,12])). % 62.99/63.06 cnf(724,plain, % 62.99/63.06 (P1(f10(f10(a2,a8),a8),a7)), % 62.99/63.06 inference(scs_inference,[],[142,44,640,397,35,12])). % 62.99/63.06 cnf(740,plain, % 62.99/63.06 (~P3(x7401,x7401)), % 62.99/63.06 inference(rename_variables,[],[44])). % 62.99/63.06 cnf(748,plain, % 62.99/63.06 (~E(f10(a6,f10(a6,a8)),a8)), % 62.99/63.06 inference(scs_inference,[],[142,168,44,740,724,597,437,35,12,14,15,7])). % 62.99/63.06 cnf(758,plain, % 62.99/63.06 (P3(x7581,f10(x7581,f10(a6,f10(a6,a6))))), % 62.99/63.06 inference(rename_variables,[],[537])). % 62.99/63.06 cnf(762,plain, % 62.99/63.06 (~E(x7621,f10(x7621,f10(a6,f10(a6,a6))))), % 62.99/63.06 inference(scs_inference,[],[18,142,44,65,537,758,35,3,14])). % 62.99/63.06 cnf(766,plain, % 62.99/63.06 (~E(f10(a6,f10(a6,a6)),a8)), % 62.99/63.06 inference(scs_inference,[],[18,142,168,44,65,537,758,35,3,14,15,7])). % 62.99/63.06 cnf(767,plain, % 62.99/63.06 (~P3(a1,f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[18,142,168,44,65,537,758,35,3,14,15,7,28])). % 62.99/63.06 cnf(769,plain, % 62.99/63.06 (E(f10(a2,a8),a1)), % 62.99/63.06 inference(scs_inference,[],[18,142,168,44,65,537,758,35,3,14,15,7,28,2])). % 62.99/63.06 cnf(776,plain, % 62.99/63.06 (~P3(f10(a2,a8),a1)), % 62.99/63.06 inference(scs_inference,[],[769,28])). % 62.99/63.06 cnf(793,plain, % 62.99/63.06 (P3(x7931,f10(x7931,f10(f10(a6,a6),a8)))), % 62.99/63.06 inference(rename_variables,[],[305])). % 62.99/63.06 cnf(799,plain, % 62.99/63.06 (~E(f10(f10(a6,a6),a6),a8)), % 62.99/63.06 inference(scs_inference,[],[168,44,65,351,305,793,35,14,15,6])). % 62.99/63.06 cnf(957,plain, % 62.99/63.06 (P2(f10(a2,a8),f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[142,143,16])). % 62.99/63.06 cnf(958,plain, % 62.99/63.06 (E(x9581,f10(x9581,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(959,plain, % 62.99/63.06 (P3(a8,f10(a6,f10(f10(a6,a6),f10(a6,a8))))), % 62.99/63.06 inference(scs_inference,[],[142,143,23,518,16,35])). % 62.99/63.06 cnf(962,plain, % 62.99/63.06 (P1(f10(f10(a6,a8),a8),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[241,142,958,143,23,518,16,35,13])). % 62.99/63.06 cnf(963,plain, % 62.99/63.06 (E(x9631,f10(x9631,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(966,plain, % 62.99/63.06 (~E(x9661,f10(x9661,f10(a8,f10(a6,a8))))), % 62.99/63.06 inference(scs_inference,[],[241,142,958,963,44,143,23,518,280,16,35,13,12,14])). % 62.99/63.06 cnf(983,plain, % 62.99/63.06 (P1(f10(f10(a6,a8),a8),f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,44,962,959,35,13])). % 62.99/63.06 cnf(1296,plain, % 62.99/63.06 (E(f3(a2,a1),f10(a5,a8))), % 62.99/63.06 inference(scs_inference,[],[19,142,3])). % 62.99/63.06 cnf(1298,plain, % 62.99/63.06 (~P3(f3(a2,a1),f10(a5,a8))), % 62.99/63.06 inference(scs_inference,[],[19,142,3,28])). % 62.99/63.06 cnf(1300,plain, % 62.99/63.06 (E(f10(a5,a8),f3(a2,a1))), % 62.99/63.06 inference(scs_inference,[],[19,142,3,28,2])). % 62.99/63.06 cnf(1301,plain, % 62.99/63.06 (~P3(f10(a5,a8),f3(a2,a1))), % 62.99/63.06 inference(scs_inference,[],[1300,28])). % 62.99/63.06 cnf(1305,plain, % 62.99/63.06 (~E(f10(a1,a6),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[769,364,3])). % 62.99/63.06 cnf(1321,plain, % 62.99/63.06 (P1(a6,a1)), % 62.99/63.06 inference(scs_inference,[],[24,239,12])). % 62.99/63.06 cnf(1325,plain, % 62.99/63.06 (~E(a1,a8)), % 62.99/63.06 inference(scs_inference,[],[24,239,51,12,33,13])). % 62.99/63.06 cnf(1336,plain, % 62.99/63.06 (P1(f10(a6,a8),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[161,142,13])). % 62.99/63.06 cnf(1338,plain, % 62.99/63.06 (P1(a2,f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[24,315,161,142,13,12])). % 62.99/63.06 cnf(1350,plain, % 62.99/63.06 (P1(f10(a6,a8),f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[24,983,12])). % 62.99/63.06 cnf(1364,plain, % 62.99/63.06 (P1(a1,a2)), % 62.99/63.06 inference(scs_inference,[],[24,142,337,13,12])). % 62.99/63.06 cnf(1376,plain, % 62.99/63.06 (P1(a6,f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[24,1336,12])). % 62.99/63.06 cnf(1391,plain, % 62.99/63.06 (P1(a6,f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[24,142,1350,1364,13,12])). % 62.99/63.06 cnf(1404,plain, % 62.99/63.06 (P1(a1,f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[50,1338,1391,51,13,12])). % 62.99/63.06 cnf(1452,plain, % 62.99/63.06 (E(f10(x14521,x14522),f10(x14522,x14521))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1453,plain, % 62.99/63.06 (P2(a1,f10(a8,a1))), % 62.99/63.06 inference(scs_inference,[],[25,1452,264,288,16,17])). % 62.99/63.06 cnf(1454,plain, % 62.99/63.06 (E(f10(x14541,x14542),f10(x14542,x14541))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1456,plain, % 62.99/63.06 (E(f10(x14561,x14562),f10(x14562,x14561))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1457,plain, % 62.99/63.06 (P1(f10(a8,a1),a7)), % 62.99/63.06 inference(scs_inference,[],[25,1452,1454,1456,316,148,264,288,16,17,13,12])). % 62.99/63.06 cnf(1470,plain, % 62.99/63.06 (P2(a2,f10(a8,a2))), % 62.99/63.06 inference(scs_inference,[],[25,289,17])). % 62.99/63.06 cnf(1471,plain, % 62.99/63.06 (E(f10(x14711,x14712),f10(x14712,x14711))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1472,plain, % 62.99/63.06 (P2(f10(a8,a1),a2)), % 62.99/63.06 inference(scs_inference,[],[25,1471,147,289,17,16])). % 62.99/63.06 cnf(1489,plain, % 62.99/63.06 (E(f10(x14891,x14892),f10(x14892,x14891))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1490,plain, % 62.99/63.06 (P2(f10(f10(a2,a8),a8),f10(a8,a1))), % 62.99/63.06 inference(scs_inference,[],[25,1489,205,311,16,17])). % 62.99/63.06 cnf(1524,plain, % 62.99/63.06 (P2(f10(a8,a1),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[25,312,16])). % 62.99/63.06 cnf(1560,plain, % 62.99/63.06 (P2(f10(a8,f10(a2,a8)),f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[25,311,16])). % 62.99/63.06 cnf(1561,plain, % 62.99/63.06 (E(f10(x15611,x15612),f10(x15612,x15611))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1563,plain, % 62.99/63.06 (E(f10(x15631,x15632),f10(x15632,x15631))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1565,plain, % 62.99/63.06 (E(f10(x15651,x15652),f10(x15652,x15651))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1566,plain, % 62.99/63.06 (P1(f10(a8,a6),a1)), % 62.99/63.06 inference(scs_inference,[],[25,1561,1563,1565,239,174,170,311,16,17,13,12])). % 62.99/63.06 cnf(1596,plain, % 62.99/63.06 (P2(f10(a8,a1),f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[25,331,16])). % 62.99/63.06 cnf(1597,plain, % 62.99/63.06 (E(f10(x15971,x15972),f10(x15972,x15971))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1598,plain, % 62.99/63.06 (P2(f10(a1,a8),f10(a8,a2))), % 62.99/63.06 inference(scs_inference,[],[25,1597,312,331,16,17])). % 62.99/63.06 cnf(1687,plain, % 62.99/63.06 (E(f10(x16871,x16872),f10(x16872,x16871))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1688,plain, % 62.99/63.06 (P2(f10(a8,a2),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[25,1687,636,17,16])). % 62.99/63.06 cnf(1689,plain, % 62.99/63.06 (E(f10(x16891,x16892),f10(x16892,x16891))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1691,plain, % 62.99/63.06 (E(f10(x16911,x16912),f10(x16912,x16911))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1692,plain, % 62.99/63.06 (P1(f10(a8,f10(a6,a8)),a6)), % 62.99/63.06 inference(scs_inference,[],[25,1687,1689,1691,472,265,636,17,16,13,12])). % 62.99/63.06 cnf(1704,plain, % 62.99/63.06 (P2(f10(a8,a2),f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[25,631,16])). % 62.99/63.06 cnf(1722,plain, % 62.99/63.06 (P2(f10(f10(a2,a8),a8),f10(a8,a2))), % 62.99/63.06 inference(scs_inference,[],[25,655,17])). % 62.99/63.06 cnf(1740,plain, % 62.99/63.06 (P2(f10(a8,a2),f10(a1,a8))), % 62.99/63.06 inference(scs_inference,[],[25,957,16])). % 62.99/63.06 cnf(1741,plain, % 62.99/63.06 (E(f10(x17411,x17412),f10(x17412,x17411))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1742,plain, % 62.99/63.06 (P2(f10(a2,a8),f10(a8,a1))), % 62.99/63.06 inference(scs_inference,[],[25,1741,957,16,17])). % 62.99/63.06 cnf(1808,plain, % 62.99/63.06 (P2(f10(a8,a2),f10(a8,a1))), % 62.99/63.06 inference(scs_inference,[],[25,1742,16])). % 62.99/63.06 cnf(1876,plain, % 62.99/63.06 (P2(f10(a8,a2),f10(a8,a2))), % 62.99/63.06 inference(scs_inference,[],[25,1688,17])). % 62.99/63.06 cnf(1877,plain, % 62.99/63.06 (E(f10(x18771,x18772),f10(x18772,x18771))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1878,plain, % 62.99/63.06 (P2(f10(a8,f10(a2,a8)),f10(a8,a1))), % 62.99/63.06 inference(scs_inference,[],[25,1877,1688,1490,17,16])). % 62.99/63.06 cnf(1899,plain, % 62.99/63.06 (E(f10(x18991,x18992),f10(x18992,x18991))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1900,plain, % 62.99/63.06 (P2(f10(a8,a1),f10(a8,a2))), % 62.99/63.06 inference(scs_inference,[],[25,1899,1596,1598,17,16])). % 62.99/63.06 cnf(1953,plain, % 62.99/63.06 (E(f10(x19531,x19532),f10(x19532,x19531))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1954,plain, % 62.99/63.06 (P1(a2,f10(a8,a1))), % 62.99/63.06 inference(scs_inference,[],[25,1953,706,1338,12,13])). % 62.99/63.06 cnf(1964,plain, % 62.99/63.06 (E(f10(x19641,x19642),f10(x19642,x19641))), % 62.99/63.06 inference(rename_variables,[],[25])). % 62.99/63.06 cnf(1965,plain, % 62.99/63.06 (P1(a1,f10(a8,a1))), % 62.99/63.06 inference(scs_inference,[],[25,1964,704,1404,12,13])). % 62.99/63.06 cnf(2782,plain, % 62.99/63.06 (E(x27821,f10(x27821,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(2784,plain, % 62.99/63.06 (E(x27841,f10(x27841,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(2786,plain, % 62.99/63.06 (E(x27861,f10(x27861,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(2789,plain, % 62.99/63.06 (~E(a11,f10(a5,a8))), % 62.99/63.06 inference(scs_inference,[],[26,142,2782,2784,2786,316,315,24,264,288,17,16,12,13,3])). % 62.99/63.06 cnf(2851,plain, % 62.99/63.06 (P2(a1,f10(f10(a8,a1),a8))), % 62.99/63.06 inference(scs_inference,[],[142,1453,17])). % 62.99/63.06 cnf(2869,plain, % 62.99/63.06 (E(x28691,f10(x28691,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(2871,plain, % 62.99/63.06 (E(x28711,f10(x28711,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(2872,plain, % 62.99/63.06 (P1(f10(f10(a1,a8),a8),a2)), % 62.99/63.06 inference(scs_inference,[],[142,2869,2871,337,1470,1472,16,17,12])). % 62.99/63.06 cnf(2903,plain, % 62.99/63.06 (E(x29031,f10(x29031,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(2904,plain, % 62.99/63.06 (P2(f10(a8,f10(a2,a8)),f10(f10(a1,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,2903,1524,1560,16,17])). % 62.99/63.06 cnf(2905,plain, % 62.99/63.06 (E(x29051,f10(x29051,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(2906,plain, % 62.99/63.06 (P1(f10(f10(a8,a1),a8),a7)), % 62.99/63.06 inference(scs_inference,[],[142,2903,2905,1457,1524,1560,16,17,12])). % 62.99/63.06 cnf(2951,plain, % 62.99/63.06 (P2(f10(f10(a2,a8),a8),f10(f10(a8,a2),a8))), % 62.99/63.06 inference(scs_inference,[],[142,1722,17])). % 62.99/63.06 cnf(2984,plain, % 62.99/63.06 (E(x29841,f10(x29841,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(2985,plain, % 62.99/63.06 (P2(f10(f10(a8,a2),a8),f10(a8,a2))), % 62.99/63.06 inference(scs_inference,[],[142,2984,1876,17,16])). % 62.99/63.06 cnf(2999,plain, % 62.99/63.06 (E(x29991,f10(x29991,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3001,plain, % 62.99/63.06 (E(x30011,f10(x30011,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3003,plain, % 62.99/63.06 (E(x30031,f10(x30031,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3004,plain, % 62.99/63.06 (P1(a2,f10(f10(a8,a1),a8))), % 62.99/63.06 inference(scs_inference,[],[142,2999,3001,3003,1954,1566,1878,17,16,12,13])). % 62.99/63.06 cnf(3016,plain, % 62.99/63.06 (E(x30161,f10(x30161,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3017,plain, % 62.99/63.06 (P2(f10(f10(a8,a1),a8),f10(a8,a2))), % 62.99/63.06 inference(scs_inference,[],[142,3016,1900,17,16])). % 62.99/63.06 cnf(3081,plain, % 62.99/63.06 (P2(f10(f10(a8,a2),a8),f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,1704,16])). % 62.99/63.06 cnf(3141,plain, % 62.99/63.06 (E(x31411,f10(x31411,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3142,plain, % 62.99/63.06 (P2(f10(f10(a8,a2),a8),f10(a2,a8))), % 62.99/63.06 inference(scs_inference,[],[142,3141,1688,1740,17,16])). % 62.99/63.06 cnf(3157,plain, % 62.99/63.06 (P2(f10(a2,a8),f10(f10(a8,a1),a8))), % 62.99/63.06 inference(scs_inference,[],[142,1742,17])). % 62.99/63.06 cnf(3174,plain, % 62.99/63.06 (P2(f10(a8,a2),f10(f10(a8,a1),a8))), % 62.99/63.06 inference(scs_inference,[],[142,1808,17])). % 62.99/63.06 cnf(3264,plain, % 62.99/63.06 (P2(f10(a8,a2),f10(f10(f10(a8,a1),a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,3174,17])). % 62.99/63.06 cnf(3280,plain, % 62.99/63.06 (E(x32801,f10(x32801,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3281,plain, % 62.99/63.06 (P2(f10(a2,a8),f10(f10(f10(a8,a1),a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,3280,3142,3157,16,17])). % 62.99/63.06 cnf(3318,plain, % 62.99/63.06 (E(x33181,f10(x33181,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3320,plain, % 62.99/63.06 (E(x33201,f10(x33201,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3322,plain, % 62.99/63.06 (E(x33221,f10(x33221,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3323,plain, % 62.99/63.06 (P1(a1,f10(f10(a8,a1),a8))), % 62.99/63.06 inference(scs_inference,[],[142,3318,3320,3322,1692,1965,3017,2985,17,16,12,13])). % 62.99/63.06 cnf(3393,plain, % 62.99/63.06 (P2(a1,f10(f10(f10(a8,a1),a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,2851,17])). % 62.99/63.06 cnf(3693,plain, % 62.99/63.06 (E(x36931,f10(x36931,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3694,plain, % 62.99/63.06 (P1(a2,f10(f10(f10(a8,a1),a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,3693,2872,3004,12,13])). % 62.99/63.06 cnf(3704,plain, % 62.99/63.06 (E(x37041,f10(x37041,a8))), % 62.99/63.06 inference(rename_variables,[],[142])). % 62.99/63.06 cnf(3705,plain, % 62.99/63.06 (P1(a1,f10(f10(f10(a8,a1),a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,3704,2906,3323,12,13])). % 62.99/63.06 cnf(3809,plain, % 62.99/63.06 (P1(f10(a2,a8),f10(f10(f10(a8,a1),a8),a8))), % 62.99/63.06 inference(scs_inference,[],[142,3694,12])). % 62.99/63.06 cnf(4241,plain, % 62.99/63.06 (P3(f10(a8,a8),f10(a6,f10(a6,f10(a6,a6))))), % 62.99/63.06 inference(scs_inference,[],[218,537,35])). % 62.99/63.06 cnf(4244,plain, % 62.99/63.06 (~E(a2,f10(a8,a8))), % 62.99/63.06 inference(scs_inference,[],[20,218,537,190,35,13])). % 62.99/63.06 cnf(4273,plain, % 62.99/63.06 (~E(f10(a2,a8),f10(a8,a8))), % 62.99/63.06 inference(scs_inference,[],[1376,190,13])). % 62.99/63.06 cnf(4390,plain, % 62.99/63.06 (P3(a8,f4(x43901,f10(f10(x43901,a6),a8)))), % 62.99/63.06 inference(scs_inference,[],[233,36])). % 62.99/63.06 cnf(4394,plain, % 62.99/63.06 (E(f3(a1,x43941),f3(a2,x43941))), % 62.99/63.06 inference(scs_inference,[],[18,233,218,36,37,4])). % 62.99/63.06 cnf(4395,plain, % 62.99/63.06 (E(f3(x43951,a1),f3(x43951,a2))), % 62.99/63.06 inference(scs_inference,[],[18,233,218,36,37,4,5])). % 62.99/63.06 cnf(4396,plain, % 62.99/63.06 (E(f9(a1,x43961),f9(a2,x43961))), % 62.99/63.06 inference(scs_inference,[],[18,233,218,36,37,4,5,8])). % 62.99/63.06 cnf(4397,plain, % 62.99/63.06 (E(f9(x43971,a1),f9(x43971,a2))), % 62.99/63.06 inference(scs_inference,[],[18,233,218,36,37,4,5,8,9])). % 62.99/63.06 cnf(4398,plain, % 62.99/63.06 (E(f4(a1,x43981),f4(a2,x43981))), % 62.99/63.06 inference(scs_inference,[],[18,233,218,36,37,4,5,8,9,10])). % 62.99/63.06 cnf(4399,plain, % 62.99/63.06 (E(f4(x43991,a1),f4(x43991,a2))), % 62.99/63.06 inference(scs_inference,[],[18,233,218,36,37,4,5,8,9,10,11])). % 62.99/63.06 cnf(4401,plain, % 62.99/63.06 (P3(x44011,f10(f10(x44011,a6),a8))), % 62.99/63.06 inference(rename_variables,[],[233])). % 62.99/63.06 cnf(4403,plain, % 62.99/63.06 (E(f10(a1,x44031),f10(a2,x44031))), % 62.99/63.06 inference(scs_inference,[],[18,233,218,36,37,4,5,8,9,10,11,30,6])). % 62.99/63.06 cnf(4404,plain, % 62.99/63.06 (P1(a8,a6)), % 62.99/63.06 inference(scs_inference,[],[18,54,233,218,36,37,4,5,8,9,10,11,30,6,29])). % 62.99/63.06 cnf(4406,plain, % 62.99/63.06 (P3(a8,f10(f10(a2,a8),a8))), % 62.99/63.06 inference(scs_inference,[],[18,54,233,1391,218,36,37,4,5,8,9,10,11,30,6,29,31])). % 62.99/63.07 cnf(4408,plain, % 62.99/63.07 (P1(f3(a2,a1),f10(a5,a8))), % 62.99/63.07 inference(scs_inference,[],[18,54,233,1391,1296,218,36,37,4,5,8,9,10,11,30,6,29,31,27])). % 62.99/63.07 cnf(4415,plain, % 62.99/63.07 (~E(a8,a2)), % 62.99/63.07 inference(scs_inference,[],[18,54,61,4241,233,4401,1391,1296,218,36,37,4,5,8,9,10,11,30,6,29,31,27,32,7,28,2])). % 62.99/63.07 cnf(4417,plain, % 62.99/63.07 (P3(x44171,f10(f10(x44171,a6),a8))), % 62.99/63.07 inference(rename_variables,[],[233])). % 62.99/63.07 cnf(4419,plain, % 62.99/63.07 (~P3(f10(a6,a6),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[18,54,61,144,4241,233,4401,1391,1296,218,24,36,37,4,5,8,9,10,11,30,6,29,31,27,32,7,28,2,35,15])). % 62.99/63.07 cnf(4420,plain, % 62.99/63.07 (E(f10(x44201,a8),x44201)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(4421,plain, % 62.99/63.07 (~P1(f10(a6,a8),a8)), % 62.99/63.07 inference(scs_inference,[],[18,54,61,144,4241,233,4401,1391,1296,218,51,24,4420,36,37,4,5,8,9,10,11,30,6,29,31,27,32,7,28,2,35,15,12])). % 62.99/63.07 cnf(4422,plain, % 62.99/63.07 (E(f10(x44221,a8),x44221)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(4423,plain, % 62.99/63.07 (~P3(f10(a6,a8),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[18,54,61,144,193,4241,233,4401,1391,1296,218,51,24,4420,4422,36,37,4,5,8,9,10,11,30,6,29,31,27,32,7,28,2,35,15,12,14])). % 62.99/63.07 cnf(4424,plain, % 62.99/63.07 (E(f10(x44241,a8),x44241)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(4428,plain, % 62.99/63.07 (~P1(a6,f10(f10(a8,a8),a8))), % 62.99/63.07 inference(scs_inference,[],[18,54,61,144,193,4241,233,4401,4417,1391,1296,218,51,190,24,4420,4422,4424,36,37,4,5,8,9,10,11,30,6,29,31,27,32,7,28,2,35,15,12,14,34,13])). % 62.99/63.07 cnf(4430,plain, % 62.99/63.07 (~P1(f10(a6,a6),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[18,54,61,144,193,214,4241,233,4401,4417,1391,1296,218,51,190,24,4420,4422,4424,36,37,4,5,8,9,10,11,30,6,29,31,27,32,7,28,2,35,15,12,14,34,13,33])). % 62.99/63.07 cnf(4442,plain, % 62.99/63.07 (E(f10(x44421,f4(x44421,f10(x44421,a6))),f10(x44421,a6))), % 62.99/63.07 inference(scs_inference,[],[56,37])). % 62.99/63.07 cnf(4449,plain, % 62.99/63.07 (P3(a8,f4(a8,f10(f10(a2,a8),a8)))), % 62.99/63.07 inference(scs_inference,[],[4394,4406,4390,56,37,11,4,30,9,36])). % 62.99/63.07 cnf(4452,plain, % 62.99/63.07 (P1(f10(x44521,x44522),f10(x44522,x44521))), % 62.99/63.07 inference(scs_inference,[],[283,4394,4406,4390,56,37,11,4,30,9,36,5,29])). % 62.99/63.07 cnf(4456,plain, % 62.99/63.07 (P3(a8,f10(a2,a8))), % 62.99/63.07 inference(scs_inference,[],[283,4394,4406,4390,56,1376,37,11,4,30,9,36,5,29,10,8,31])). % 62.99/63.07 cnf(4458,plain, % 62.99/63.07 (P1(f3(a1,x44581),f3(a2,x44581))), % 62.99/63.07 inference(scs_inference,[],[283,4394,4406,4390,56,1376,37,11,4,30,9,36,5,29,10,8,31,27])). % 62.99/63.07 cnf(4466,plain, % 62.99/63.07 (~E(a8,a1)), % 62.99/63.07 inference(scs_inference,[],[1325,283,4394,4406,4390,56,1376,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2])). % 62.99/63.07 cnf(4469,plain, % 62.99/63.07 (~P3(f10(f10(a6,a6),a2),f10(a1,a8))), % 62.99/63.07 inference(scs_inference,[],[1325,4404,228,283,4394,4406,4390,260,56,1376,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2,40,35])). % 62.99/63.07 cnf(4472,plain, % 62.99/63.07 (P1(f3(a2,x44721),f3(a1,x44721))), % 62.99/63.07 inference(scs_inference,[],[1325,4404,228,283,4394,4406,4390,260,56,1376,43,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2,40,35,12])). % 62.99/63.07 cnf(4473,plain, % 62.99/63.07 (P1(x44731,x44731)), % 62.99/63.07 inference(rename_variables,[],[43])). % 62.99/63.07 cnf(4474,plain, % 62.99/63.07 (~P3(f10(a5,a8),f3(a1,a1))), % 62.99/63.07 inference(scs_inference,[],[1325,4404,228,283,1301,4394,4406,4390,260,56,1376,43,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2,40,35,12,15])). % 62.99/63.07 cnf(4475,plain, % 62.99/63.07 (E(f3(a1,x44751),f3(a2,x44751))), % 62.99/63.07 inference(rename_variables,[],[4394])). % 62.99/63.07 cnf(4476,plain, % 62.99/63.07 (~P3(f3(a1,a1),f10(a5,a8))), % 62.99/63.07 inference(scs_inference,[],[1325,4404,228,283,1298,1301,4394,4475,4406,4390,260,56,1376,43,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2,40,35,12,15,14])). % 62.99/63.07 cnf(4480,plain, % 62.99/63.07 (P1(f3(x44801,a1),f3(x44801,a2))), % 62.99/63.07 inference(scs_inference,[],[1325,4404,228,283,1298,1301,4394,4475,4395,4406,4390,260,56,1376,43,4473,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2,40,35,12,15,14,34,13])). % 62.99/63.07 cnf(4482,plain, % 62.99/63.07 (~P1(f10(a6,a8),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[1325,4404,228,283,1298,1301,4423,4394,4475,4395,4406,4390,474,260,56,1376,43,4473,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2,40,35,12,15,14,34,13,33])). % 62.99/63.07 cnf(4485,plain, % 62.99/63.07 (~E(f10(a8,a8),a2)), % 62.99/63.07 inference(scs_inference,[],[1325,4415,4404,228,283,1298,1301,4423,4394,4475,4395,4406,4390,474,260,56,1376,43,4473,142,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2,40,35,12,15,14,34,13,33,3])). % 62.99/63.07 cnf(4487,plain, % 62.99/63.07 (E(f3(f10(a2,a8),f10(a2,a8)),a11)), % 62.99/63.07 inference(scs_inference,[],[1325,4415,4404,228,283,1298,1301,4423,4394,4475,4395,4406,3264,4390,474,3809,260,56,1376,43,4473,142,37,11,4,30,9,36,5,29,10,8,31,27,6,32,7,28,2,40,35,12,15,14,34,13,33,3,38])). % 62.99/63.07 cnf(4494,plain, % 62.99/63.07 (E(f10(a8,f4(a8,f10(a2,a8))),f10(a2,a8))), % 62.99/63.07 inference(scs_inference,[],[4456,37])). % 62.99/63.07 cnf(4497,plain, % 62.99/63.07 (P1(f10(a8,a8),f10(a6,a6))), % 62.99/63.07 inference(scs_inference,[],[4419,4456,4396,37,11,29])). % 62.99/63.07 cnf(4499,plain, % 62.99/63.07 (P3(a8,f4(a8,f10(a2,a8)))), % 62.99/63.07 inference(scs_inference,[],[4419,4456,4396,37,11,29,36])). % 62.99/63.07 cnf(4504,plain, % 62.99/63.07 (P3(a8,a1)), % 62.99/63.07 inference(scs_inference,[],[4419,4456,4396,4449,1321,37,11,29,36,30,4,31])). % 62.99/63.07 cnf(4506,plain, % 62.99/63.07 (P1(f9(a1,x45061),f9(a2,x45061))), % 62.99/63.07 inference(scs_inference,[],[4419,4456,4396,4449,1321,37,11,29,36,30,4,31,27])). % 62.99/63.07 cnf(4516,plain, % 62.99/63.07 (~E(a8,f10(a2,a8))), % 62.99/63.07 inference(scs_inference,[],[4419,4456,4396,4449,1321,37,11,29,36,30,4,31,27,5,10,9,6,8,32,7,28])). % 62.99/63.07 cnf(4521,plain, % 62.99/63.07 (~P3(f10(a2,a8),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[97,4419,4452,4456,4396,4449,1321,168,37,11,29,36,30,4,31,27,5,10,9,6,8,32,7,28,2,40,35])). % 62.99/63.07 cnf(4525,plain, % 62.99/63.07 (E(f10(x45251,f4(x45251,f10(x45251,a6))),f10(x45251,a6))), % 62.99/63.07 inference(rename_variables,[],[4442])). % 62.99/63.07 cnf(4527,plain, % 62.99/63.07 (E(f10(x45271,a8),x45271)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(4532,plain, % 62.99/63.07 (~P1(f10(a6,a6),f10(f10(a8,a8),a8))), % 62.99/63.07 inference(scs_inference,[],[97,767,4419,4430,4452,4456,4396,4442,4525,4449,1321,24,4527,168,37,11,29,36,30,4,31,27,5,10,9,6,8,32,7,28,2,40,35,12,15,14,34,13])). % 62.99/63.07 cnf(4534,plain, % 62.99/63.07 (~P1(f10(a6,a6),a8)), % 62.99/63.07 inference(scs_inference,[],[97,412,767,4419,4430,4452,4456,4396,4442,4525,4449,144,1321,24,4527,168,37,11,29,36,30,4,31,27,5,10,9,6,8,32,7,28,2,40,35,12,15,14,34,13,33])). % 62.99/63.07 cnf(4542,plain, % 62.99/63.07 (E(f10(a8,f4(a8,a1)),a1)), % 62.99/63.07 inference(scs_inference,[],[4504,37])). % 62.99/63.07 cnf(4544,plain, % 62.99/63.07 (P3(a8,f4(a8,a1))), % 62.99/63.07 inference(scs_inference,[],[4504,37,36])). % 62.99/63.07 cnf(4546,plain, % 62.99/63.07 (P3(a8,a2)), % 62.99/63.07 inference(scs_inference,[],[4504,20,37,36,31])). % 62.99/63.07 cnf(4549,plain, % 62.99/63.07 (P1(f10(a8,a8),f10(a2,a8))), % 62.99/63.07 inference(scs_inference,[],[4504,4521,4397,20,37,36,31,4,29])). % 62.99/63.07 cnf(4554,plain, % 62.99/63.07 (P1(f9(x45541,a1),f9(x45541,a2))), % 62.99/63.07 inference(scs_inference,[],[4504,4521,4397,4499,20,37,36,31,4,29,30,11,27])). % 62.99/63.07 cnf(4561,plain, % 62.99/63.07 (P1(a8,a1)), % 62.99/63.07 inference(scs_inference,[],[4504,4521,4397,4499,20,37,36,31,4,29,30,11,27,10,9,5,6,8,32])). % 62.99/63.07 cnf(4573,plain, % 62.99/63.07 (E(f9(x45731,a1),f9(x45731,a2))), % 62.99/63.07 inference(rename_variables,[],[4397])). % 62.99/63.07 cnf(4574,plain, % 62.99/63.07 (P1(f9(a1,x45741),f9(a2,x45741))), % 62.99/63.07 inference(rename_variables,[],[4506])). % 62.99/63.07 cnf(4575,plain, % 62.99/63.07 (~P3(f10(f9(x45751,a2),a8),f9(x45751,a1))), % 62.99/63.07 inference(scs_inference,[],[4504,380,776,4497,4521,4397,4573,4506,4499,255,137,20,37,36,31,4,29,30,11,27,10,9,5,6,8,32,7,28,2,40,35,12,15])). % 62.99/63.07 cnf(4577,plain, % 62.99/63.07 (~P3(f9(x45771,a1),f10(f9(x45771,a2),a8))), % 62.99/63.07 inference(scs_inference,[],[4504,380,776,4497,4521,4397,4573,4506,4499,255,137,20,168,37,36,31,4,29,30,11,27,10,9,5,6,8,32,7,28,2,40,35,12,15,14])). % 62.99/63.07 cnf(4581,plain, % 62.99/63.07 (~P1(f10(a2,a8),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[4504,380,776,4497,4521,4397,4573,4506,4499,4273,255,137,20,168,37,36,31,4,29,30,11,27,10,9,5,6,8,32,7,28,2,40,35,12,15,14,34,33])). % 62.99/63.07 cnf(4586,plain, % 62.99/63.07 (~E(f10(a8,a8),a1)), % 62.99/63.07 inference(scs_inference,[],[4504,4466,380,776,4497,4521,4397,4573,4506,4574,4499,4273,255,137,20,168,142,37,36,31,4,29,30,11,27,10,9,5,6,8,32,7,28,2,40,35,12,15,14,34,33,13,3])). % 62.99/63.07 cnf(4596,plain, % 62.99/63.07 (E(f10(a8,f4(a8,a2)),a2)), % 62.99/63.07 inference(scs_inference,[],[4546,37])). % 62.99/63.07 cnf(4600,plain, % 62.99/63.07 (P3(a8,f4(a8,a2))), % 62.99/63.07 inference(scs_inference,[],[4546,4544,37,30,36])). % 62.99/63.07 cnf(4603,plain, % 62.99/63.07 (P1(f10(a5,a8),f3(a1,a1))), % 62.99/63.07 inference(scs_inference,[],[4546,4476,4398,4544,37,30,36,4,29])). % 62.99/63.07 cnf(4606,plain, % 62.99/63.07 (P1(f4(a1,x46061),f4(a2,x46061))), % 62.99/63.07 inference(scs_inference,[],[4546,4476,4398,4544,37,30,36,4,29,11,27])). % 62.99/63.07 cnf(4613,plain, % 62.99/63.07 (P1(a8,a2)), % 62.99/63.07 inference(scs_inference,[],[4546,4476,4398,4544,37,30,36,4,29,11,27,9,10,5,6,8,32])). % 62.99/63.07 cnf(4616,plain, % 62.99/63.07 (~E(a8,f4(a8,a1))), % 62.99/63.07 inference(scs_inference,[],[4546,4476,4398,4544,37,30,36,4,29,11,27,9,10,5,6,8,32,7,28])). % 62.99/63.07 cnf(4619,plain, % 62.99/63.07 (P1(f10(a8,a8),f10(a2,a1))), % 62.99/63.07 inference(scs_inference,[],[4546,4561,402,4476,4398,4544,37,30,36,4,29,11,27,9,10,5,6,8,32,7,28,2,40])). % 62.99/63.07 cnf(4621,plain, % 62.99/63.07 (~P3(a2,f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[4546,4561,402,4476,4398,4544,168,37,30,36,4,29,11,27,9,10,5,6,8,32,7,28,2,40,35])). % 62.99/63.07 cnf(4627,plain, % 62.99/63.07 (E(f10(x46271,a8),x46271)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(4628,plain, % 62.99/63.07 (~P3(f3(a1,a1),f3(a2,a1))), % 62.99/63.07 inference(scs_inference,[],[4546,4561,402,4482,4476,4398,4544,2904,1296,24,25,168,37,30,36,4,29,11,27,9,10,5,6,8,32,7,28,2,40,35,17,12,15])). % 62.99/63.07 cnf(4630,plain, % 62.99/63.07 (E(f10(x46301,a8),x46301)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(4631,plain, % 62.99/63.07 (~E(f10(f3(a1,a1),a2),f10(a5,a8))), % 62.99/63.07 inference(scs_inference,[],[4546,4561,402,4482,4476,4398,4544,2904,1296,24,4627,25,168,37,30,36,4,29,11,27,9,10,5,6,8,32,7,28,2,40,35,17,12,15,14,34])). % 62.99/63.07 cnf(4633,plain, % 62.99/63.07 (~P1(a2,f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[4546,4561,402,4482,4244,4476,4398,4544,2904,1296,24,4627,25,168,37,30,36,4,29,11,27,9,10,5,6,8,32,7,28,2,40,35,17,12,15,14,34,33])). % 62.99/63.07 cnf(4639,plain, % 62.99/63.07 (E(f3(a1,a1),a11)), % 62.99/63.07 inference(scs_inference,[],[4546,4561,402,4482,4244,4476,4398,4544,2904,966,3281,3705,1296,1321,24,4627,4630,25,168,37,30,36,4,29,11,27,9,10,5,6,8,32,7,28,2,40,35,17,12,15,14,34,33,13,3,38])). % 62.99/63.07 cnf(4641,plain, % 62.99/63.07 (~E(a7,f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[4546,4561,402,4482,4244,4476,4398,4544,2904,966,3281,3705,1296,1321,24,4627,4630,25,168,37,30,36,4,29,11,27,9,10,5,6,8,32,7,28,2,40,35,17,12,15,14,34,33,13,3,38,130])). % 62.99/63.07 cnf(4653,plain, % 62.99/63.07 (P3(a8,f4(a8,f4(a8,a2)))), % 62.99/63.07 inference(scs_inference,[],[4399,4600,37,30,27,36])). % 62.99/63.07 cnf(4667,plain, % 62.99/63.07 (~E(a8,f4(a8,a2))), % 62.99/63.07 inference(scs_inference,[],[285,4399,4600,37,30,27,36,11,4,29,5,9,10,32,6,8,7,28])). % 62.99/63.07 cnf(4678,plain, % 62.99/63.07 (~P3(a1,f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[18,4613,427,285,4399,4621,4633,4600,255,225,37,30,27,36,11,4,29,5,9,10,32,6,8,7,28,2,40,35,12,15,14])). % 62.99/63.07 cnf(4681,plain, % 62.99/63.07 (E(f10(a5,a8),f3(a1,a1))), % 62.99/63.07 inference(scs_inference,[],[18,4613,427,4603,285,4399,4474,4621,4633,4600,255,225,37,30,27,36,11,4,29,5,9,10,32,6,8,7,28,2,40,35,12,15,14,34,33])). % 62.99/63.07 cnf(4686,plain, % 62.99/63.07 (~E(f10(a8,a8),f10(a6,a6))), % 62.99/63.07 inference(scs_inference,[],[18,4613,212,427,4603,285,4399,4474,4606,4621,4633,4600,255,225,142,37,30,27,36,11,4,29,5,9,10,32,6,8,7,28,2,40,35,12,15,14,34,33,13,3])). % 62.99/63.07 cnf(4688,plain, % 62.99/63.07 (E(f3(a2,a2),a11)), % 62.99/63.07 inference(scs_inference,[],[18,4613,212,427,4603,285,4399,4474,4606,4621,4633,4600,3393,3694,255,225,20,142,37,30,27,36,11,4,29,5,9,10,32,6,8,7,28,2,40,35,12,15,14,34,33,13,3,38])). % 62.99/63.07 cnf(4699,plain, % 62.99/63.07 (P3(a8,f4(a8,f4(a8,f4(a8,a2))))), % 62.99/63.07 inference(scs_inference,[],[4653,4544,37,36])). % 62.99/63.07 cnf(4701,plain, % 62.99/63.07 (P1(f10(a8,a8),a1)), % 62.99/63.07 inference(scs_inference,[],[4678,4653,4544,37,36,29])). % 62.99/63.07 cnf(4722,plain, % 62.99/63.07 (~P3(f4(a8,f4(a8,a2)),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[1305,4549,4681,4678,4639,4653,4544,168,37,36,29,30,27,4,11,10,32,5,9,6,8,7,28,2,40,35])). % 62.99/63.07 cnf(4726,plain, % 62.99/63.07 (~P3(f3(a1,a1),a5)), % 62.99/63.07 inference(scs_inference,[],[1305,4549,4581,4681,4628,4678,4639,4653,4494,4544,86,168,37,36,29,30,27,4,11,10,32,5,9,6,8,7,28,2,40,35,12,15])). % 62.99/63.07 cnf(4730,plain, % 62.99/63.07 (P3(f10(a8,a8),f10(a6,a6))), % 62.99/63.07 inference(scs_inference,[],[1305,4549,4581,4686,4681,4628,4678,4639,4653,4542,4494,4497,4544,86,168,37,36,29,30,27,4,11,10,32,5,9,6,8,7,28,2,40,35,12,15,14,34,33])). % 62.99/63.07 cnf(4732,plain, % 62.99/63.07 (~P1(f10(a2,a8),f10(f10(a8,a8),a8))), % 62.99/63.07 inference(scs_inference,[],[1305,4549,4581,4686,4681,4628,4678,4639,4653,4542,4494,4497,4544,86,24,168,37,36,29,30,27,4,11,10,32,5,9,6,8,7,28,2,40,35,12,15,14,34,33,13])). % 62.99/63.07 cnf(4741,plain, % 62.99/63.07 (E(f10(f10(a8,a8),f4(f10(a8,a8),f10(a6,a6))),f10(a6,a6))), % 62.99/63.07 inference(scs_inference,[],[4730,37])). % 62.99/63.07 cnf(4745,plain, % 62.99/63.07 (P3(a8,f4(f10(a8,a8),f10(a6,a6)))), % 62.99/63.07 inference(scs_inference,[],[4730,4699,37,30,36])). % 62.99/63.07 cnf(4749,plain, % 62.99/63.07 (E(f3(f3(a2,a2),x47491),f3(a11,x47491))), % 62.99/63.07 inference(scs_inference,[],[4730,4726,4688,4699,37,30,36,29,4])). % 62.99/63.07 cnf(4752,plain, % 62.99/63.07 (E(f4(x47521,f3(a2,a2)),f4(x47521,a11))), % 62.99/63.07 inference(scs_inference,[],[4730,4726,4688,4699,37,30,36,29,4,27,11])). % 62.99/63.07 cnf(4755,plain, % 62.99/63.07 (E(f3(x47551,f3(a2,a2)),f3(x47551,a11))), % 62.99/63.07 inference(scs_inference,[],[4730,4726,4688,4699,37,30,36,29,4,27,11,32,5])). % 62.99/63.07 cnf(4757,plain, % 62.99/63.07 (E(f9(x47571,f3(a2,a2)),f9(x47571,a11))), % 62.99/63.07 inference(scs_inference,[],[4730,4726,4688,4699,37,30,36,29,4,27,11,32,5,10,9])). % 62.99/63.07 cnf(4759,plain, % 62.99/63.07 (E(f9(f3(a2,a2),x47591),f9(a11,x47591))), % 62.99/63.07 inference(scs_inference,[],[4730,4726,4688,4699,37,30,36,29,4,27,11,32,5,10,9,6,8])). % 62.99/63.07 cnf(4769,plain, % 62.99/63.07 (~P3(f10(a11,a8),f3(a2,a2))), % 62.99/63.07 inference(scs_inference,[],[2789,4730,4408,4726,4688,4699,202,255,37,30,36,29,4,27,11,32,5,10,9,6,8,7,28,2,40,35,15])). % 62.99/63.07 cnf(4773,plain, % 62.99/63.07 (~P3(f3(a2,a2),f10(a11,a8))), % 62.99/63.07 inference(scs_inference,[],[2789,4730,4408,4472,4726,4688,4699,202,255,168,37,30,36,29,4,27,11,32,5,10,9,6,8,7,28,2,40,35,15,12,14])). % 62.99/63.07 cnf(4775,plain, % 62.99/63.07 (~P1(f10(f10(a6,a6),a6),a8)), % 62.99/63.07 inference(scs_inference,[],[2789,4730,4408,4472,4726,4688,565,799,4699,202,255,168,37,30,36,29,4,27,11,32,5,10,9,6,8,7,28,2,40,35,15,12,14,33])). % 62.99/63.07 cnf(4777,plain, % 62.99/63.07 (P1(f10(a8,a8),a2)), % 62.99/63.07 inference(scs_inference,[],[18,2789,4730,4408,4472,4701,4726,4688,565,799,4699,202,255,168,37,30,36,29,4,27,11,32,5,10,9,6,8,7,28,2,40,35,15,12,14,33,13])). % 62.99/63.07 cnf(4778,plain, % 62.99/63.07 (~E(f10(a11,a8),f10(a5,a8))), % 62.99/63.07 inference(scs_inference,[],[18,2789,4730,4408,4472,4701,4726,4688,565,799,4699,202,255,168,142,37,30,36,29,4,27,11,32,5,10,9,6,8,7,28,2,40,35,15,12,14,33,13,3])). % 62.99/63.07 cnf(4788,plain, % 62.99/63.07 (P1(f10(a11,a8),f3(a2,a2))), % 62.99/63.07 inference(scs_inference,[],[4773,62,37,29])). % 62.99/63.07 cnf(4794,plain, % 62.99/63.07 (P3(a8,f4(a8,f4(f10(a8,a8),f10(a6,a6))))), % 62.99/63.07 inference(scs_inference,[],[4773,4749,4745,62,37,29,27,30,36])). % 62.99/63.07 cnf(4811,plain, % 62.99/63.07 (~P3(f4(f10(a8,a8),f10(a6,a6)),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[4641,4458,4773,4749,4745,4487,62,168,37,29,27,30,36,11,4,32,10,5,9,6,8,28,7,2,40,35])). % 62.99/63.07 cnf(4818,plain, % 62.99/63.07 (~P3(f10(a11,a8),f3(a2,a1))), % 62.99/63.07 inference(scs_inference,[],[4641,4421,4458,4773,4769,4749,4745,2951,4487,4395,62,24,25,168,37,29,27,30,36,11,4,32,10,5,9,6,8,28,7,2,40,35,17,12,15])). % 62.99/63.07 cnf(4819,plain, % 62.99/63.07 (E(f3(x48191,a1),f3(x48191,a2))), % 62.99/63.07 inference(rename_variables,[],[4395])). % 62.99/63.07 cnf(4822,plain, % 62.99/63.07 (~P3(f3(a2,a1),f10(a11,a8))), % 62.99/63.07 inference(scs_inference,[],[4641,4421,4458,4773,4769,4749,4745,2951,4487,4395,4819,62,24,25,168,37,29,27,30,36,11,4,32,10,5,9,6,8,28,7,2,40,35,17,12,15,34,14])). % 62.99/63.07 cnf(4824,plain, % 62.99/63.07 (P3(f10(a8,a8),a2)), % 62.99/63.07 inference(scs_inference,[],[4641,4421,4458,4773,4485,4769,4777,4749,4745,2951,4487,4395,4819,62,24,25,168,37,29,27,30,36,11,4,32,10,5,9,6,8,28,7,2,40,35,17,12,15,34,14,33])). % 62.99/63.07 cnf(4838,plain, % 62.99/63.07 (P3(a8,f4(f10(a8,a8),a2))), % 62.99/63.07 inference(scs_inference,[],[4824,4752,37,27,36])). % 62.99/63.07 cnf(4842,plain, % 62.99/63.07 (P1(f10(a11,a8),f3(a2,a1))), % 62.99/63.07 inference(scs_inference,[],[4822,4824,4752,4794,37,27,36,30,29])). % 62.99/63.07 cnf(4856,plain, % 62.99/63.07 (~E(f10(a5,a8),f10(a11,a8))), % 62.99/63.07 inference(scs_inference,[],[4778,4822,4824,4752,4794,4596,37,27,36,30,29,11,4,32,5,10,9,8,6,28,7,2])). % 62.99/63.07 cnf(4865,plain, % 62.99/63.07 (E(f4(x48651,f3(a2,a2)),f4(x48651,a11))), % 62.99/63.07 inference(rename_variables,[],[4752])). % 62.99/63.07 cnf(4871,plain, % 62.99/63.07 (E(f10(a11,a8),f3(a2,a1))), % 62.99/63.07 inference(scs_inference,[],[4778,4822,4788,4818,4824,4752,4865,4794,4596,4606,4499,233,255,168,37,27,36,30,29,11,4,32,5,10,9,8,6,28,7,2,40,35,15,12,34,14,33])). % 62.99/63.07 cnf(4882,plain, % 62.99/63.07 (E(f10(a8,f4(a8,a6)),a6)), % 62.99/63.07 inference(scs_inference,[],[23,37])). % 62.99/63.07 cnf(4884,plain, % 62.99/63.07 (P3(a8,f4(a8,f4(f10(a8,a8),a2)))), % 62.99/63.07 inference(scs_inference,[],[4838,23,37,36])). % 62.99/63.07 cnf(4888,plain, % 62.99/63.07 (P1(f3(x48881,f3(a2,a2)),f3(x48881,a11))), % 62.99/63.07 inference(scs_inference,[],[4811,4755,4838,23,37,36,29,27])). % 62.99/63.07 cnf(4907,plain, % 62.99/63.07 (~P3(f4(f10(a8,a8),a2),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[4842,4871,4667,4811,4755,4838,168,23,37,36,29,27,30,11,4,32,10,5,6,8,9,28,7,2,40,35])). % 62.99/63.07 cnf(4911,plain, % 62.99/63.07 (E(f10(x49111,a8),x49111)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(4916,plain, % 62.99/63.07 (E(f10(x49161,a8),x49161)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(4917,plain, % 62.99/63.07 (P3(f10(a8,a8),a1)), % 62.99/63.07 inference(scs_inference,[],[4842,4871,4586,4534,4667,4811,4755,4838,4741,48,4701,24,4911,168,23,37,36,29,27,30,11,4,32,10,5,6,8,9,28,7,2,40,35,15,12,34,14,33])). % 62.99/63.07 cnf(4923,plain, % 62.99/63.07 (E(f3(a6,a6),a11)), % 62.99/63.07 inference(scs_inference,[],[4842,4871,4586,4534,4667,4811,4755,4532,4838,4741,762,3081,48,4701,1391,24,4911,4916,43,168,23,37,36,29,27,30,11,4,32,10,5,6,8,9,28,7,2,40,35,15,12,34,14,33,13,3,38])). % 62.99/63.07 cnf(4935,plain, % 62.99/63.07 (P3(a8,f4(f10(a8,a8),a1))), % 62.99/63.07 inference(scs_inference,[],[4917,4907,4884,37,29,30,36])). % 62.99/63.07 cnf(4957,plain, % 62.99/63.07 (~P3(f10(a11,a8),f3(a6,a6))), % 62.99/63.07 inference(scs_inference,[],[4480,4917,4616,4923,4907,4884,260,255,37,29,30,36,27,11,4,32,5,10,9,6,8,28,7,2,40,35,15])). % 62.99/63.07 cnf(4963,plain, % 62.99/63.07 (~P3(f3(a6,a6),f10(a11,a8))), % 62.99/63.07 inference(scs_inference,[],[4480,4917,4616,4923,4907,4884,4544,260,255,43,168,37,29,30,36,27,11,4,32,5,10,9,6,8,28,7,2,40,35,15,12,34,14])). % 62.99/63.07 cnf(4978,plain, % 62.99/63.07 (P1(f9(x49781,f3(a2,a2)),f9(x49781,a11))), % 62.99/63.07 inference(scs_inference,[],[4757,4935,65,37,30,27])). % 62.99/63.07 cnf(4980,plain, % 62.99/63.07 (P1(f10(a11,a8),f3(a6,a6))), % 62.99/63.07 inference(scs_inference,[],[4963,4757,4935,65,37,30,27,29])). % 62.99/63.07 cnf(4982,plain, % 62.99/63.07 (P3(a8,f4(a8,f4(f10(a8,a8),a1)))), % 62.99/63.07 inference(scs_inference,[],[4963,4757,4935,65,37,30,27,29,36])). % 62.99/63.07 cnf(4995,plain, % 62.99/63.07 (E(f10(x49951,f10(a8,f4(a8,a6))),f10(x49951,a6))), % 62.99/63.07 inference(scs_inference,[],[4963,4757,4935,4882,65,37,30,27,29,36,11,32,4,10,5,8,9,28,6,7])). % 62.99/63.07 cnf(4999,plain, % 62.99/63.07 (~P3(f4(f10(a8,a8),a1),f10(a8,a8))), % 62.99/63.07 inference(scs_inference,[],[4554,4963,568,4757,4935,4882,168,65,37,30,27,29,36,11,32,4,10,5,8,9,28,6,7,2,40,35])). % 62.99/63.07 cnf(5003,plain, % 62.99/63.07 (E(f10(x50031,a8),x50031)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(5009,plain, % 62.99/63.07 (~P3(f10(f3(a6,a6),a8),f10(a11,a8))), % 62.99/63.07 inference(scs_inference,[],[4554,4963,4957,568,4757,536,681,4428,4935,4882,24,5003,168,65,37,30,27,29,36,11,32,4,10,5,8,9,28,6,7,2,40,35,15,34,12,33,14])). % 62.99/63.07 cnf(5023,plain, % 62.99/63.07 (P3(a8,f4(a8,f10(a6,f10(a8,a6))))), % 62.99/63.07 inference(scs_inference,[],[4759,489,27,36])). % 62.99/63.07 cnf(5031,plain, % 62.99/63.07 (E(f4(x50311,f3(a1,a1)),f4(x50311,a11))), % 62.99/63.07 inference(scs_inference,[],[4999,4759,4982,4639,489,27,36,30,29,32,11])). % 62.99/63.07 cnf(5032,plain, % 62.99/63.07 (E(f3(f3(a1,a1),x50321),f3(a11,x50321))), % 62.99/63.07 inference(scs_inference,[],[4999,4759,4982,4639,489,27,36,30,29,32,11,4])). % 62.99/63.07 cnf(5033,plain, % 62.99/63.07 (E(f3(x50331,f3(a1,a1)),f3(x50331,a11))), % 62.99/63.07 inference(scs_inference,[],[4999,4759,4982,4639,489,27,36,30,29,32,11,4,5])). % 62.99/63.07 cnf(5037,plain, % 62.99/63.07 (E(f10(f3(a1,a1),x50371),f10(a11,x50371))), % 62.99/63.07 inference(scs_inference,[],[4999,4759,4982,4639,489,27,36,30,29,32,11,4,5,10,28,6])). % 62.99/63.07 cnf(5048,plain, % 62.99/63.07 (E(f9(f3(a2,a2),x50481),f9(a11,x50481))), % 62.99/63.07 inference(rename_variables,[],[4759])). % 62.99/63.07 cnf(5053,plain, % 62.99/63.07 (E(f9(f3(a2,a2),x50531),f9(a11,x50531))), % 62.99/63.07 inference(rename_variables,[],[4759])). % 62.99/63.07 cnf(5054,plain, % 62.99/63.07 (P1(f9(x50541,f3(a2,a2)),f9(x50541,a11))), % 62.99/63.07 inference(rename_variables,[],[4978])). % 62.99/63.07 cnf(5058,plain, % 62.99/63.07 (E(f9(f3(a2,a2),x50581),f9(a11,x50581))), % 62.99/63.07 inference(rename_variables,[],[4759])). % 62.99/63.07 cnf(5063,plain, % 62.99/63.07 (~E(f10(a8,a8),f10(a2,a8))), % 62.99/63.07 inference(scs_inference,[],[4516,4619,586,4999,4978,5054,4759,5048,5053,5058,4575,615,766,4577,4982,4639,489,90,4544,142,27,36,30,29,32,11,4,5,10,28,6,8,9,7,2,40,35,15,34,12,33,14,13,3])). % 62.99/63.07 cnf(5069,plain, % 62.99/63.07 (P3(a8,f4(a8,f4(a8,f10(a2,a8))))), % 62.99/63.07 inference(scs_inference,[],[5031,4499,27,36])). % 62.99/63.07 cnf(5092,plain, % 62.99/63.07 (E(f10(f3(a1,a1),x50921),f10(a11,x50921))), % 62.99/63.07 inference(rename_variables,[],[5037])). % 62.99/63.07 cnf(5095,plain, % 62.99/63.07 (P3(f10(a8,a8),f10(a2,a8))), % 62.99/63.07 inference(scs_inference,[],[5063,600,5009,5031,5037,4775,4995,5023,4549,4542,4499,168,27,36,29,30,32,11,4,10,5,28,6,8,9,7,2,35,15,12,33])). % 62.99/63.07 cnf(5098,plain, % 62.99/63.07 (E(f10(x50981,a8),x50981)), % 62.99/63.07 inference(rename_variables,[],[24])). % 62.99/63.07 cnf(5101,plain, % 62.99/63.07 (~E(f10(a11,a2),f10(a5,a8))), % 62.99/63.07 inference(scs_inference,[],[5063,600,5009,5031,5037,5092,4631,4732,4775,4995,5023,4549,4542,4499,24,5098,168,27,36,29,30,32,11,4,10,5,28,6,8,9,7,2,35,15,12,33,14,13,3])). % 62.99/63.07 cnf(5111,plain, % 62.99/63.07 (P3(a8,f4(f10(a8,a8),f10(a2,a8)))), % 62.99/63.07 inference(scs_inference,[],[5095,5032,27,36])). % 62.99/63.07 cnf(5138,plain, % 62.99/63.07 (E(f3(f3(a1,a1),x51381),f3(a11,x51381))), % 62.99/63.07 inference(rename_variables,[],[5032])). % 62.99/63.07 cnf(5139,plain, % 62.99/63.07 (P1(f3(x51391,f3(a2,a2)),f3(x51391,a11))), % 62.99/63.07 inference(rename_variables,[],[4888])). % 62.99/63.07 cnf(5147,plain, % 62.99/63.07 (~E(f3(a2,a1),f10(a11,a8))), % 62.99/63.07 inference(scs_inference,[],[5095,4856,5101,4980,4722,5032,5138,4888,5139,633,748,5069,197,4395,1300,537,255,44,27,36,30,29,32,11,4,5,10,28,8,6,9,7,2,40,35,15,12,33,14,13,3])). % 62.99/63.07 cnf(5171,plain, % 62.99/63.07 ($false), % 62.99/63.07 inference(scs_inference,[],[5147,4469,5033,5111,4403,4871,27,36,29,30,32,11,5,4,10,28,6,8,9,7,2]), % 62.99/63.07 ['proof']). % 62.99/63.07 % SZS output end Proof % 62.99/63.07 % Total time :62.400000s %------------------------------------------------------------------------------