%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU126+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : 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 15:01:10 EDT 2024 % Result : Theorem 175.23s 175.35s % Output : CNFRefutation 175.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.10 % Problem : SEU126+1 : TPTP v8.2.0. Released v3.3.0. % 0.06/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.30 % Computer : n024.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Fri Jun 21 15:34:23 EDT 2024 % 0.10/0.31 % CPUTime : % 0.47/0.54 start to proof:theBenchmark % 175.21/175.33 %------------------------------------------- % 175.21/175.33 % File :CSE---1.7 % 175.21/175.33 % Problem :theBenchmark % 175.21/175.33 % Transform :cnf % 175.21/175.33 % Format :tptp:raw % 175.21/175.33 % Command :java -jar mcs_scs.jar %d %s % 175.21/175.33 % 175.21/175.33 % Result :Theorem 174.640000s % 175.21/175.33 % Output :CNFRefutation 174.640000s % 175.21/175.33 %------------------------------------------- % 175.23/175.34 %------------------------------------------------------------------------------ % 175.23/175.34 % File : SEU126+1 : TPTP v8.2.0. Released v3.3.0. % 175.23/175.34 % Domain : Set theory % 175.23/175.34 % Problem : MPTP bushy problem t12_xboole_1 % 175.23/175.34 % Version : [Urb07] axioms : Especial. % 175.23/175.34 % English : % 175.23/175.34 % 175.23/175.34 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 175.23/175.34 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 175.23/175.34 % Source : [Urb07] % 175.23/175.34 % Names : bushy-t12_xboole_1 [Urb07] % 175.23/175.34 % 175.23/175.34 % Status : Theorem % 175.23/175.34 % Rating : 0.19 v8.2.0, 0.22 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.17 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.05 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.26 v3.3.0 % 175.23/175.34 % Syntax : Number of formulae : 19 ( 9 unt; 0 def) % 175.23/175.34 % Number of atoms : 34 ( 8 equ) % 175.23/175.34 % Maximal formula atoms : 4 ( 1 avg) % 175.23/175.34 % Number of connectives : 24 ( 9 ~; 1 |; 4 &) % 175.23/175.34 % ( 4 <=>; 6 =>; 0 <=; 0 <~>) % 175.23/175.34 % Maximal formula depth : 8 ( 4 avg) % 175.23/175.34 % Maximal term depth : 2 ( 1 avg) % 175.23/175.34 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 175.23/175.34 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 175.23/175.34 % Number of variables : 31 ( 29 !; 2 ?) % 175.23/175.34 % SPC : FOF_THM_RFO_SEQ % 175.23/175.34 % 175.23/175.34 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 175.23/175.34 % library, www.mizar.org % 175.23/175.34 %------------------------------------------------------------------------------ % 175.23/175.34 fof(antisymmetry_r2_hidden,axiom, % 175.23/175.34 ! [A,B] : % 175.23/175.34 ( in(A,B) % 175.23/175.34 => ~ in(B,A) ) ). % 175.23/175.34 % 175.23/175.34 fof(commutativity_k2_xboole_0,axiom, % 175.23/175.34 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 175.23/175.34 % 175.23/175.34 fof(d10_xboole_0,axiom, % 175.23/175.34 ! [A,B] : % 175.23/175.35 ( A = B % 175.23/175.35 <=> ( subset(A,B) % 175.23/175.35 & subset(B,A) ) ) ). % 175.23/175.35 % 175.23/175.35 fof(d2_xboole_0,axiom, % 175.23/175.35 ! [A,B,C] : % 175.23/175.35 ( C = set_union2(A,B) % 175.23/175.35 <=> ! [D] : % 175.23/175.35 ( in(D,C) % 175.23/175.35 <=> ( in(D,A) % 175.23/175.35 | in(D,B) ) ) ) ). % 175.23/175.35 % 175.23/175.35 fof(d3_tarski,axiom, % 175.23/175.35 ! [A,B] : % 175.23/175.35 ( subset(A,B) % 175.23/175.35 <=> ! [C] : % 175.23/175.35 ( in(C,A) % 175.23/175.35 => in(C,B) ) ) ). % 175.23/175.35 % 175.23/175.35 fof(dt_k1_xboole_0,axiom, % 175.23/175.35 $true ). % 175.23/175.35 % 175.23/175.35 fof(dt_k2_xboole_0,axiom, % 175.23/175.35 $true ). % 175.23/175.35 % 175.23/175.35 fof(fc1_xboole_0,axiom, % 175.23/175.35 empty(empty_set) ). % 175.23/175.35 % 175.23/175.35 fof(fc2_xboole_0,axiom, % 175.23/175.35 ! [A,B] : % 175.23/175.35 ( ~ empty(A) % 175.23/175.35 => ~ empty(set_union2(A,B)) ) ). % 175.23/175.35 % 175.23/175.35 fof(fc3_xboole_0,axiom, % 175.23/175.35 ! [A,B] : % 175.23/175.35 ( ~ empty(A) % 175.23/175.35 => ~ empty(set_union2(B,A)) ) ). % 175.23/175.35 % 175.23/175.35 fof(idempotence_k2_xboole_0,axiom, % 175.23/175.35 ! [A,B] : set_union2(A,A) = A ). % 175.23/175.35 % 175.23/175.35 fof(rc1_xboole_0,axiom, % 175.23/175.35 ? [A] : empty(A) ). % 175.23/175.35 % 175.23/175.35 fof(rc2_xboole_0,axiom, % 175.23/175.35 ? [A] : ~ empty(A) ). % 175.23/175.35 % 175.23/175.35 fof(reflexivity_r1_tarski,axiom, % 175.23/175.35 ! [A,B] : subset(A,A) ). % 175.23/175.35 % 175.23/175.35 fof(t12_xboole_1,conjecture, % 175.23/175.35 ! [A,B] : % 175.23/175.35 ( subset(A,B) % 175.23/175.35 => set_union2(A,B) = B ) ). % 175.23/175.35 % 175.23/175.35 fof(t1_boole,axiom, % 175.23/175.35 ! [A] : set_union2(A,empty_set) = A ). % 175.23/175.35 % 175.23/175.35 fof(t6_boole,axiom, % 175.23/175.35 ! [A] : % 175.23/175.35 ( empty(A) % 175.23/175.35 => A = empty_set ) ). % 175.23/175.35 % 175.23/175.35 fof(t7_boole,axiom, % 175.23/175.35 ! [A,B] : % 175.23/175.35 ~ ( in(A,B) % 175.23/175.35 & empty(B) ) ). % 175.23/175.35 % 175.23/175.35 fof(t8_boole,axiom, % 175.23/175.35 ! [A,B] : % 175.23/175.35 ~ ( empty(A) % 175.23/175.35 & A != B % 175.23/175.35 & empty(B) ) ). % 175.23/175.35 % 175.23/175.35 %------------------------------------------------------------------------------ % 175.23/175.35 %------------------------------------------- % 175.23/175.35 % Proof found % 175.23/175.35 % SZS status Theorem for theBenchmark % 175.23/175.35 % SZS output start Proof % 175.23/175.35 %ClaNum:42(EqnAxiom:15) % 175.23/175.35 %VarNum:116(SingletonVarNum:48) % 175.23/175.35 %MaxLitNum:4 % 175.23/175.35 %MaxfuncDepth:1 % 175.23/175.35 %SharedTerms:11 % 175.23/175.35 %goalClause: 18 24 % 175.23/175.35 %singleGoalClaCount:2 % 175.23/175.35 [16]P1(a1) % 175.23/175.35 [17]P1(a2) % 175.23/175.35 [18]P2(a5,a7) % 175.23/175.35 [23]~P1(a6) % 175.23/175.35 [24]~E(f8(a5,a7),a7) % 175.23/175.35 [20]P2(x201,x201) % 175.23/175.35 [19]E(f8(x191,a1),x191) % 175.23/175.35 [21]E(f8(x211,x211),x211) % 175.23/175.35 [22]E(f8(x221,x222),f8(x222,x221)) % 175.23/175.35 [25]~P1(x251)+E(x251,a1) % 175.23/175.35 [28]~E(x281,x282)+P2(x281,x282) % 175.23/175.35 [29]~P1(x291)+~P3(x292,x291) % 175.23/175.35 [30]~P3(x302,x301)+~P3(x301,x302) % 175.23/175.35 [32]P1(x321)+~P1(f8(x322,x321)) % 175.23/175.35 [33]P1(x331)+~P1(f8(x331,x332)) % 175.23/175.35 [34]P2(x341,x342)+P3(f3(x341,x342),x341) % 175.23/175.35 [39]P2(x391,x392)+~P3(f3(x391,x392),x392) % 175.23/175.35 [26]~P1(x262)+~P1(x261)+E(x261,x262) % 175.23/175.35 [31]~P2(x312,x311)+~P2(x311,x312)+E(x311,x312) % 175.23/175.35 [35]~P2(x353,x352)+P3(x351,x352)+~P3(x351,x353) % 175.23/175.35 [41]~P3(f4(x412,x413,x411),x411)+~P3(f4(x412,x413,x411),x413)+E(x411,f8(x412,x413)) % 175.23/175.35 [42]~P3(f4(x422,x423,x421),x421)+~P3(f4(x422,x423,x421),x422)+E(x421,f8(x422,x423)) % 175.23/175.35 [36]~P3(x361,x364)+P3(x361,x362)+~E(x362,f8(x363,x364)) % 175.23/175.35 [37]~P3(x371,x373)+P3(x371,x372)+~E(x372,f8(x373,x374)) % 175.23/175.35 [40]P3(f4(x402,x403,x401),x401)+P3(f4(x402,x403,x401),x403)+P3(f4(x402,x403,x401),x402)+E(x401,f8(x402,x403)) % 175.23/175.35 [38]~P3(x381,x384)+P3(x381,x382)+P3(x381,x383)+~E(x384,f8(x383,x382)) % 175.23/175.35 %EqnAxiom % 175.23/175.35 [1]E(x11,x11) % 175.23/175.35 [2]E(x22,x21)+~E(x21,x22) % 175.23/175.35 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 175.23/175.35 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 175.23/175.35 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 175.23/175.35 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 175.23/175.35 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 175.23/175.35 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 175.23/175.35 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 175.23/175.35 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 175.23/175.35 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 175.23/175.35 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 175.23/175.35 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 175.23/175.35 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 175.23/175.35 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 175.23/175.35 % 175.23/175.35 %------------------------------------------- % 175.23/175.37 cnf(44,plain, % 175.23/175.37 (~P3(x441,x442)+P3(x441,f8(x443,x442))), % 175.23/175.37 inference(equality_inference,[],[36])). % 175.23/175.37 cnf(45,plain, % 175.23/175.37 (~P3(x451,x452)+P3(x451,f8(x452,x453))), % 175.23/175.37 inference(equality_inference,[],[37])). % 175.23/175.37 cnf(46,plain, % 175.23/175.37 (~P3(x461,f8(x462,x463))+P3(x461,x463)+P3(x461,x462)), % 175.23/175.37 inference(equality_inference,[],[38])). % 175.23/175.37 cnf(47,plain, % 175.23/175.37 (E(x471,f8(x471,x471))), % 175.23/175.37 inference(scs_inference,[],[21,2])). % 175.23/175.37 cnf(48,plain, % 175.23/175.37 (~P3(x481,a1)), % 175.23/175.37 inference(scs_inference,[],[21,16,2,29])). % 175.23/175.37 cnf(50,plain, % 175.23/175.37 (~E(f8(a5,a7),f8(a7,a7))), % 175.23/175.37 inference(scs_inference,[],[24,21,16,2,29,3])). % 175.23/175.37 cnf(51,plain, % 175.23/175.37 (E(f8(x511,x511),x511)), % 175.23/175.37 inference(rename_variables,[],[21])). % 175.23/175.37 cnf(52,plain, % 175.23/175.37 (P2(x521,f8(x521,x521))), % 175.23/175.37 inference(scs_inference,[],[24,20,21,51,16,2,29,3,14])). % 175.23/175.37 cnf(54,plain, % 175.23/175.37 (P2(a5,f8(a7,a7))), % 175.23/175.37 inference(scs_inference,[],[18,24,20,21,51,16,2,29,3,14,15])). % 175.23/175.37 cnf(55,plain, % 175.23/175.37 (~P3(x551,f8(a1,a1))), % 175.23/175.37 inference(scs_inference,[],[18,24,20,21,51,16,2,29,3,14,15,46])). % 175.23/175.37 cnf(58,plain, % 175.23/175.37 (E(f8(x581,x581),x581)), % 175.23/175.37 inference(rename_variables,[],[21])). % 175.23/175.37 cnf(59,plain, % 175.23/175.37 (~P3(x591,f8(f8(a1,a1),f8(a1,a1)))), % 175.23/175.37 inference(scs_inference,[],[18,24,20,21,51,58,16,23,2,29,3,14,15,46,11,38])). % 175.23/175.37 cnf(62,plain, % 175.23/175.37 (P2(a1,x621)), % 175.23/175.37 inference(scs_inference,[],[18,24,20,21,51,58,16,23,2,29,3,14,15,46,11,38,34])). % 175.23/175.37 cnf(64,plain, % 175.23/175.37 (~E(a5,a7)), % 175.23/175.37 inference(scs_inference,[],[18,24,20,21,51,58,16,23,2,29,3,14,15,46,11,38,34,4])). % 175.23/175.37 cnf(65,plain, % 175.23/175.37 (~P2(a7,a5)), % 175.23/175.37 inference(scs_inference,[],[18,24,20,21,51,58,16,23,2,29,3,14,15,46,11,38,34,4,31])). % 175.23/175.37 cnf(69,plain, % 175.23/175.37 (~E(a7,a5)), % 175.23/175.37 inference(scs_inference,[],[18,24,20,21,51,58,16,23,2,29,3,14,15,46,11,38,34,4,31,26,28])). % 175.23/175.37 cnf(71,plain, % 175.23/175.37 (~P3(x711,x712)+P3(x711,f8(f8(x713,x712),a1))), % 175.23/175.37 inference(scs_inference,[],[18,24,20,21,51,58,19,16,23,2,29,3,14,15,46,11,38,34,4,31,26,28,36])). % 175.23/175.37 cnf(77,plain, % 175.23/175.37 (~P3(x771,a2)), % 175.23/175.37 inference(scs_inference,[],[17,29])). % 175.23/175.37 cnf(79,plain, % 175.23/175.37 (P2(f8(a1,a1),x791)), % 175.23/175.37 inference(scs_inference,[],[55,17,29,34])). % 175.23/175.37 cnf(82,plain, % 175.23/175.37 (E(x821,f8(x821,a1))), % 175.23/175.37 inference(scs_inference,[],[55,17,19,29,34,2])). % 175.23/175.37 cnf(83,plain, % 175.23/175.37 (P1(f8(a2,a2))), % 175.23/175.37 inference(scs_inference,[],[47,55,17,19,29,34,2,11])). % 175.23/175.37 cnf(84,plain, % 175.23/175.37 (E(x841,f8(x841,x841))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(85,plain, % 175.23/175.37 (~E(f8(a7,a7),a5)), % 175.23/175.37 inference(scs_inference,[],[65,47,52,55,17,19,29,34,2,11,15])). % 175.23/175.37 cnf(87,plain, % 175.23/175.37 (~E(f8(a5,a7),f8(a7,a1))), % 175.23/175.37 inference(scs_inference,[],[65,24,47,52,55,17,19,29,34,2,11,15,3])). % 175.23/175.37 cnf(88,plain, % 175.23/175.37 (E(f8(x881,a1),x881)), % 175.23/175.37 inference(rename_variables,[],[19])). % 175.23/175.37 cnf(89,plain, % 175.23/175.37 (P2(f8(a5,a5),a7)), % 175.23/175.37 inference(scs_inference,[],[18,65,24,47,84,52,55,17,19,29,34,2,11,15,3,14])). % 175.23/175.37 cnf(91,plain, % 175.23/175.37 (~P3(x911,x912)+P3(x911,f8(f8(x912,x913),a1))), % 175.23/175.37 inference(scs_inference,[],[18,65,24,47,84,52,55,17,19,88,29,34,2,11,15,3,14,37])). % 175.23/175.37 cnf(96,plain, % 175.23/175.37 (E(a5,f8(a7,a7))+~P2(f8(a7,a7),a5)), % 175.23/175.37 inference(scs_inference,[],[18,65,24,47,84,52,54,55,17,19,88,29,34,2,11,15,3,14,37,42,31])). % 175.23/175.37 cnf(102,plain, % 175.23/175.37 (P2(a2,x1021)), % 175.23/175.37 inference(scs_inference,[],[77,34])). % 175.23/175.37 cnf(105,plain, % 175.23/175.37 (~P3(x1051,f8(a2,a2))), % 175.23/175.37 inference(scs_inference,[],[83,77,34,29])). % 175.23/175.37 cnf(107,plain, % 175.23/175.37 (P2(f8(a5,a1),a7)), % 175.23/175.37 inference(scs_inference,[],[18,82,83,77,34,29,14])). % 175.23/175.37 cnf(108,plain, % 175.23/175.37 (E(x1081,f8(x1081,a1))), % 175.23/175.37 inference(rename_variables,[],[82])). % 175.23/175.37 cnf(109,plain, % 175.23/175.37 (P1(f8(f8(a2,a2),a1))), % 175.23/175.37 inference(scs_inference,[],[18,82,108,83,77,34,29,14,11])). % 175.23/175.37 cnf(110,plain, % 175.23/175.37 (E(x1101,f8(x1101,a1))), % 175.23/175.37 inference(rename_variables,[],[82])). % 175.23/175.37 cnf(111,plain, % 175.23/175.37 (P2(a5,f8(a7,a1))), % 175.23/175.37 inference(scs_inference,[],[18,82,108,110,83,77,34,29,14,11,15])). % 175.23/175.37 cnf(122,plain, % 175.23/175.37 (~P3(x1221,f8(f8(a2,a2),a1))), % 175.23/175.37 inference(scs_inference,[],[109,29])). % 175.23/175.37 cnf(124,plain, % 175.23/175.37 (P2(f8(a2,a2),x1241)), % 175.23/175.37 inference(scs_inference,[],[109,105,29,34])). % 175.23/175.37 cnf(128,plain, % 175.23/175.37 (E(x1281,f8(x1281,x1281))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(129,plain, % 175.23/175.37 (P2(f8(a5,a5),f8(a7,a1))), % 175.23/175.37 inference(scs_inference,[],[47,128,111,109,105,29,34,15,14])). % 175.23/175.37 cnf(130,plain, % 175.23/175.37 (E(x1301,f8(x1301,x1301))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(131,plain, % 175.23/175.37 (P1(f8(f8(a2,a2),f8(a2,a2)))), % 175.23/175.37 inference(scs_inference,[],[47,128,130,111,83,109,105,29,34,15,14,11])). % 175.23/175.37 cnf(135,plain, % 175.23/175.37 (E(a5,f8(a7,a1))+~P2(f8(a7,a1),a5)), % 175.23/175.37 inference(scs_inference,[],[47,128,130,85,111,83,109,105,29,34,15,14,11,26,31])). % 175.23/175.37 cnf(141,plain, % 175.23/175.37 (~P3(x1411,f8(f8(a2,a2),f8(a2,a2)))), % 175.23/175.37 inference(scs_inference,[],[131,29])). % 175.23/175.37 cnf(144,plain, % 175.23/175.37 (E(x1441,f8(x1441,a1))), % 175.23/175.37 inference(rename_variables,[],[82])). % 175.23/175.37 cnf(145,plain, % 175.23/175.37 (P2(f8(x1451,a1),f8(x1451,x1451))), % 175.23/175.37 inference(scs_inference,[],[82,144,52,129,131,29,15,14])). % 175.23/175.37 cnf(160,plain, % 175.23/175.37 (E(x1601,f8(x1601,x1601))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(161,plain, % 175.23/175.37 (P2(f8(f8(x1611,a1),f8(x1611,a1)),f8(x1611,x1611))), % 175.23/175.37 inference(scs_inference,[],[47,160,145,55,105,46,15,14])). % 175.23/175.37 cnf(163,plain, % 175.23/175.37 (P2(f8(f8(a1,a1),f8(a2,a2)),x1631)), % 175.23/175.37 inference(scs_inference,[],[47,160,145,55,105,46,15,14,34])). % 175.23/175.37 cnf(175,plain, % 175.23/175.37 (P2(f8(a5,a1),f8(a7,a7))), % 175.23/175.37 inference(scs_inference,[],[47,107,55,77,46,15])). % 175.23/175.37 cnf(176,plain, % 175.23/175.37 (E(x1761,f8(x1761,x1761))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(177,plain, % 175.23/175.37 (P2(f8(f8(a5,a1),f8(a5,a1)),a7)), % 175.23/175.37 inference(scs_inference,[],[47,176,107,55,77,46,15,14])). % 175.23/175.37 cnf(179,plain, % 175.23/175.37 (P2(f8(f8(a1,a1),a2),x1791)), % 175.23/175.37 inference(scs_inference,[],[47,176,107,55,77,46,15,14,34])). % 175.23/175.37 cnf(190,plain, % 175.23/175.37 (~P3(x1901,f8(f8(a1,a1),a1))), % 175.23/175.37 inference(scs_inference,[],[55,48,46])). % 175.23/175.37 cnf(194,plain, % 175.23/175.37 (E(x1941,f8(x1941,x1941))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(195,plain, % 175.23/175.37 (P2(f8(f8(a5,a1),f8(a5,a1)),f8(a7,a7))), % 175.23/175.37 inference(scs_inference,[],[47,194,175,55,48,46,15,14])). % 175.23/175.37 cnf(197,plain, % 175.23/175.37 (P2(f8(f8(a1,a1),a1),x1971)), % 175.23/175.37 inference(scs_inference,[],[47,194,175,55,48,46,15,14,34])). % 175.23/175.37 cnf(203,plain, % 175.23/175.37 (E(f8(a7,a7),f8(a5,a1))+~P2(f8(a7,a7),f8(a5,a1))), % 175.23/175.37 inference(scs_inference,[],[50,47,194,175,55,48,46,15,14,34,31,3,5,2])). % 175.23/175.37 cnf(205,plain, % 175.23/175.37 (~P2(f8(a7,a7),f8(a5,a1))+~P3(x2051,a7)+P3(x2051,f8(a5,a1))), % 175.23/175.37 inference(scs_inference,[],[24,50,47,194,175,55,48,46,15,14,34,31,3,5,2,36])). % 175.23/175.37 cnf(206,plain, % 175.23/175.37 (P2(f8(f8(a5,a1),f8(a5,a1)),f8(a7,a1))), % 175.23/175.37 inference(scs_inference,[],[82,177,15])). % 175.23/175.37 cnf(220,plain, % 175.23/175.37 (P2(a5,f8(f8(a7,a7),f8(a7,a7)))), % 175.23/175.37 inference(scs_inference,[],[47,54,15])). % 175.23/175.37 cnf(221,plain, % 175.23/175.37 (E(x2211,f8(x2211,x2211))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(222,plain, % 175.23/175.37 (P2(f8(a5,a5),f8(a7,a7))), % 175.23/175.37 inference(scs_inference,[],[47,221,54,15,14])). % 175.23/175.37 cnf(231,plain, % 175.23/175.37 (E(x2311,f8(x2311,a1))), % 175.23/175.37 inference(rename_variables,[],[82])). % 175.23/175.37 cnf(232,plain, % 175.23/175.37 (P2(f8(f8(a5,a5),a1),f8(a7,a7))), % 175.23/175.37 inference(scs_inference,[],[82,231,222,15,14])). % 175.23/175.37 cnf(245,plain, % 175.23/175.37 (E(x2451,f8(x2451,x2451))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(246,plain, % 175.23/175.37 (P2(f8(a5,a5),f8(f8(a7,a7),f8(a7,a7)))), % 175.23/175.37 inference(scs_inference,[],[47,245,220,129,15,14])). % 175.23/175.37 cnf(255,plain, % 175.23/175.37 (P2(f8(f8(a5,a5),f8(a5,a5)),a7)), % 175.23/175.37 inference(scs_inference,[],[47,89,14])). % 175.23/175.37 cnf(256,plain, % 175.23/175.37 (E(x2561,f8(x2561,x2561))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.37 cnf(257,plain, % 175.23/175.37 (P2(f8(f8(a5,a5),f8(a5,a5)),f8(a7,a7))), % 175.23/175.37 inference(scs_inference,[],[47,256,89,14,15])). % 175.23/175.37 cnf(258,plain, % 175.23/175.37 (E(x2581,f8(x2581,x2581))), % 175.23/175.37 inference(rename_variables,[],[47])). % 175.23/175.38 cnf(265,plain, % 175.23/175.38 (~P2(f8(f8(a7,a7),f8(a7,a7)),f8(a5,a5))+~P3(x2651,f8(a7,a7))+P3(x2651,f8(a5,a5))), % 175.23/175.38 inference(scs_inference,[],[24,50,47,256,258,246,89,14,15,31,3,2,36])). % 175.23/175.38 cnf(267,plain, % 175.23/175.38 (E(x2671,f8(x2671,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(268,plain, % 175.23/175.38 (P2(f8(f8(a5,a5),a1),a7)), % 175.23/175.38 inference(scs_inference,[],[82,267,255,89,15,14])). % 175.23/175.38 cnf(280,plain, % 175.23/175.38 (~E(f8(a1,a1),a7)), % 175.23/175.38 inference(scs_inference,[],[65,79,14])). % 175.23/175.38 cnf(281,plain, % 175.23/175.38 (P2(f8(a1,a1),x2811)), % 175.23/175.38 inference(rename_variables,[],[79])). % 175.23/175.38 cnf(284,plain, % 175.23/175.38 (~P2(a7,f8(a1,a1))), % 175.23/175.38 inference(scs_inference,[],[65,79,281,14,26,31])). % 175.23/175.38 cnf(287,plain, % 175.23/175.38 (~E(a7,f8(a1,a1))), % 175.23/175.38 inference(scs_inference,[],[65,79,281,14,26,31,28])). % 175.23/175.38 cnf(294,plain, % 175.23/175.38 (~E(a1,a7)), % 175.23/175.38 inference(scs_inference,[],[284,52,14])). % 175.23/175.38 cnf(295,plain, % 175.23/175.38 (P2(x2951,f8(x2951,x2951))), % 175.23/175.38 inference(rename_variables,[],[52])). % 175.23/175.38 cnf(296,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),a7)), % 175.23/175.38 inference(scs_inference,[],[284,52,287,48,14,40])). % 175.23/175.38 cnf(299,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),f8(x2991,a7))), % 175.23/175.38 inference(scs_inference,[],[284,52,287,48,14,40,44])). % 175.23/175.38 cnf(301,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),f8(a7,x3011))), % 175.23/175.38 inference(scs_inference,[],[284,52,287,48,14,40,44,45])). % 175.23/175.38 cnf(307,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),f8(f8(x3071,a7),f8(x3071,a7)))), % 175.23/175.38 inference(scs_inference,[],[284,52,295,287,48,14,40,44,45,30,205,35])). % 175.23/175.38 cnf(310,plain, % 175.23/175.38 (P3(f8(f4(a1,a1,a7),f4(a1,a1,a7)),a7)), % 175.23/175.38 inference(scs_inference,[],[284,47,52,295,287,48,14,40,44,45,30,205,35,12])). % 175.23/175.38 cnf(312,plain, % 175.23/175.38 (~E(a7,f8(f8(a1,a1),a1))), % 175.23/175.38 inference(scs_inference,[],[284,47,52,295,190,287,48,14,40,44,45,30,205,35,12,13])). % 175.23/175.38 cnf(322,plain, % 175.23/175.38 (~P1(a7)), % 175.23/175.38 inference(scs_inference,[],[284,47,52,295,190,287,21,19,16,48,14,40,44,45,30,205,35,12,13,37,36,46,26])). % 175.23/175.38 cnf(324,plain, % 175.23/175.38 (~P2(a7,a1)), % 175.23/175.38 inference(scs_inference,[],[284,47,52,295,190,62,287,21,19,16,48,14,40,44,45,30,205,35,12,13,37,36,46,26,31])). % 175.23/175.38 cnf(327,plain, % 175.23/175.38 (~E(a7,a1)), % 175.23/175.38 inference(scs_inference,[],[284,47,52,295,190,62,287,21,19,16,48,14,40,44,45,30,205,35,12,13,37,36,46,26,31,28])). % 175.23/175.38 cnf(329,plain, % 175.23/175.38 (E(a2,a1)), % 175.23/175.38 inference(scs_inference,[],[83,32,25])). % 175.23/175.38 cnf(332,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),f8(x3321,f8(a7,x3322)))), % 175.23/175.38 inference(scs_inference,[],[307,301,30,44])). % 175.23/175.38 cnf(334,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),f8(f8(a7,x3341),x3342))), % 175.23/175.38 inference(scs_inference,[],[307,301,30,44,45])). % 175.23/175.38 cnf(336,plain, % 175.23/175.38 (E(a1,a2)), % 175.23/175.38 inference(scs_inference,[],[307,301,329,30,44,45,2])). % 175.23/175.38 cnf(337,plain, % 175.23/175.38 (P3(f8(f4(a1,a1,a7),f4(a1,a1,a7)),f8(a7,a7))), % 175.23/175.38 inference(scs_inference,[],[52,307,301,310,329,30,44,45,2,35])). % 175.23/175.38 cnf(341,plain, % 175.23/175.38 (E(x3411,f8(x3411,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(344,plain, % 175.23/175.38 (P2(f8(f8(a5,a5),a1),f8(a7,a1))), % 175.23/175.38 inference(scs_inference,[],[82,341,52,268,307,190,301,310,329,30,44,45,2,35,12,13,15])). % 175.23/175.38 cnf(345,plain, % 175.23/175.38 (E(x3451,f8(x3451,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(346,plain, % 175.23/175.38 (~E(a7,a2)), % 175.23/175.38 inference(scs_inference,[],[82,341,52,268,307,190,327,301,310,329,30,44,45,2,35,12,13,15,3])). % 175.23/175.38 cnf(349,plain, % 175.23/175.38 (P3(f4(f8(a1,a1),a1,a7),a7)), % 175.23/175.38 inference(scs_inference,[],[82,341,345,52,268,175,307,190,55,327,301,48,312,310,329,30,44,45,2,35,12,13,15,3,14,40])). % 175.23/175.38 cnf(359,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),f8(x3591,f8(x3592,a7)))), % 175.23/175.38 inference(scs_inference,[],[299,44])). % 175.23/175.38 cnf(363,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),f8(f8(x3631,a7),x3632))), % 175.23/175.38 inference(scs_inference,[],[337,299,44,30,45])). % 175.23/175.38 cnf(369,plain, % 175.23/175.38 (E(x3691,f8(x3691,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(372,plain, % 175.23/175.38 (P2(f8(x3721,a1),f8(f8(x3721,x3721),a1))), % 175.23/175.38 inference(scs_inference,[],[82,369,52,145,337,190,299,349,44,30,45,35,12,13,15])). % 175.23/175.38 cnf(373,plain, % 175.23/175.38 (E(x3731,f8(x3731,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(374,plain, % 175.23/175.38 (P2(f8(a5,a1),f8(a7,a1))), % 175.23/175.38 inference(scs_inference,[],[82,369,373,52,145,111,337,190,299,349,44,30,45,35,12,13,15,14])). % 175.23/175.38 cnf(413,plain, % 175.23/175.38 (P3(f4(f8(a1,a1),a1,a7),f8(x4131,a7))), % 175.23/175.38 inference(scs_inference,[],[349,44])). % 175.23/175.38 cnf(417,plain, % 175.23/175.38 (P3(f4(f8(a1,a1),a1,a7),f8(a7,x4171))), % 175.23/175.38 inference(scs_inference,[],[301,349,44,30,45])). % 175.23/175.38 cnf(421,plain, % 175.23/175.38 (~E(f8(a2,a2),a7)), % 175.23/175.38 inference(scs_inference,[],[65,124,301,349,44,30,45,46,14])). % 175.23/175.38 cnf(426,plain, % 175.23/175.38 (E(f8(a7,a1),f8(a5,a1))+~P2(f8(a7,a1),f8(a5,a1))), % 175.23/175.38 inference(scs_inference,[],[65,87,374,124,301,349,44,30,45,46,14,31,3,2])). % 175.23/175.38 cnf(444,plain, % 175.23/175.38 (~E(f8(f8(a1,a1),f8(a2,a2)),a7)), % 175.23/175.38 inference(scs_inference,[],[65,421,124,163,299,30,46,31,14])). % 175.23/175.38 cnf(446,plain, % 175.23/175.38 (~E(a7,f8(a2,a2))), % 175.23/175.38 inference(scs_inference,[],[65,421,124,163,299,30,46,31,14,28])). % 175.23/175.38 cnf(468,plain, % 175.23/175.38 (~E(f8(f8(a1,a1),a1),a7)), % 175.23/175.38 inference(scs_inference,[],[65,444,197,163,334,30,31,14])). % 175.23/175.38 cnf(470,plain, % 175.23/175.38 (P3(f4(a2,a2,a7),a7)), % 175.23/175.38 inference(scs_inference,[],[65,444,197,163,334,446,77,30,31,14,40])). % 175.23/175.38 cnf(473,plain, % 175.23/175.38 (P3(f4(a2,a2,a7),f8(x4731,a7))), % 175.23/175.38 inference(scs_inference,[],[65,444,197,163,334,446,77,30,31,14,40,44])). % 175.23/175.38 cnf(475,plain, % 175.23/175.38 (~E(a7,f8(f8(a1,a1),f8(a2,a2)))), % 175.23/175.38 inference(scs_inference,[],[65,444,197,163,334,446,77,30,31,14,40,44,28])). % 175.23/175.38 cnf(477,plain, % 175.23/175.38 (P3(f4(a2,a2,a7),f8(a7,x4771))), % 175.23/175.38 inference(scs_inference,[],[65,444,197,163,334,446,77,30,31,14,40,44,28,45])). % 175.23/175.38 cnf(481,plain, % 175.23/175.38 (P3(f4(a2,a2,a7),f8(f8(x4811,a7),f8(x4811,a7)))), % 175.23/175.38 inference(scs_inference,[],[65,52,444,197,163,334,446,77,30,31,14,40,44,28,45,205,35])). % 175.23/175.38 cnf(495,plain, % 175.23/175.38 (P3(f4(a2,a2,a7),f8(x4951,f8(a7,x4952)))), % 175.23/175.38 inference(scs_inference,[],[477,44])). % 175.23/175.38 cnf(497,plain, % 175.23/175.38 (P3(f4(a2,a2,a7),f8(f8(a7,x4971),x4972))), % 175.23/175.38 inference(scs_inference,[],[477,44,45])). % 175.23/175.38 cnf(506,plain, % 175.23/175.38 (~E(f8(f8(a1,a1),a2),a7)), % 175.23/175.38 inference(scs_inference,[],[65,47,481,468,179,197,477,44,45,30,12,31,14])). % 175.23/175.38 cnf(508,plain, % 175.23/175.38 (P3(f4(f8(a1,a1),f8(a2,a2),a7),a7)), % 175.23/175.38 inference(scs_inference,[],[65,47,481,468,55,179,197,477,475,105,44,45,30,12,31,14,40])). % 175.23/175.38 cnf(514,plain, % 175.23/175.38 (P3(f4(f8(a1,a1),f8(a2,a2),a7),f8(a7,a7))), % 175.23/175.38 inference(scs_inference,[],[65,47,52,481,468,55,179,197,477,475,105,44,45,30,12,31,14,40,205,35])). % 175.23/175.38 cnf(517,plain, % 175.23/175.38 (P3(f4(a2,a2,a7),f8(f8(x5171,a7),x5172))), % 175.23/175.38 inference(scs_inference,[],[473,45])). % 175.23/175.38 cnf(519,plain, % 175.23/175.38 (P3(f4(a2,a2,a7),f8(x5191,f8(x5192,a7)))), % 175.23/175.38 inference(scs_inference,[],[473,45,44])). % 175.23/175.38 cnf(524,plain, % 175.23/175.38 (E(x5241,f8(x5241,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(528,plain, % 175.23/175.38 (P2(a5,f8(f8(a7,a7),a1))), % 175.23/175.38 inference(scs_inference,[],[82,524,54,514,506,179,473,45,44,30,12,31,15])). % 175.23/175.38 cnf(529,plain, % 175.23/175.38 (E(x5291,f8(x5291,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(530,plain, % 175.23/175.38 (P2(f8(f8(a5,a1),a1),a7)), % 175.23/175.38 inference(scs_inference,[],[82,524,529,54,107,514,506,179,473,45,44,30,12,31,15,14])). % 175.23/175.38 cnf(534,plain, % 175.23/175.38 (P3(f4(f8(a1,a1),a2,a7),a7)), % 175.23/175.38 inference(scs_inference,[],[82,524,529,54,107,514,506,55,179,473,77,45,44,30,12,31,15,14,28,40])). % 175.23/175.38 cnf(540,plain, % 175.23/175.38 (P3(f4(f8(a1,a1),f8(a2,a2),a7),f8(x5401,a7))), % 175.23/175.38 inference(scs_inference,[],[508,44])). % 175.23/175.38 cnf(547,plain, % 175.23/175.38 (E(x5471,f8(x5471,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(548,plain, % 175.23/175.38 (P2(f8(a5,a1),f8(f8(a7,a7),a1))), % 175.23/175.38 inference(scs_inference,[],[82,547,175,413,477,508,44,45,30,12,15])). % 175.23/175.38 cnf(549,plain, % 175.23/175.38 (E(x5491,f8(x5491,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(550,plain, % 175.23/175.38 (P2(f8(f8(a5,a1),a1),f8(a7,a1))), % 175.23/175.38 inference(scs_inference,[],[82,547,549,175,374,413,477,508,44,45,30,12,15,14])). % 175.23/175.38 cnf(575,plain, % 175.23/175.38 (P3(f8(f4(a1,a1,a7),a1),a7)), % 175.23/175.38 inference(scs_inference,[],[82,417,296,534,45,44,30,12])). % 175.23/175.38 cnf(576,plain, % 175.23/175.38 (E(x5761,f8(x5761,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(577,plain, % 175.23/175.38 (P2(a5,f8(f8(a7,a1),a1))), % 175.23/175.38 inference(scs_inference,[],[82,576,111,417,296,534,45,44,30,12,15])). % 175.23/175.38 cnf(580,plain, % 175.23/175.38 (P2(a2,x5801)), % 175.23/175.38 inference(rename_variables,[],[102])). % 175.23/175.38 cnf(583,plain, % 175.23/175.38 (~P2(a7,a2)), % 175.23/175.38 inference(scs_inference,[],[65,82,576,111,102,580,417,296,534,45,44,30,12,15,14,205,31])). % 175.23/175.38 cnf(618,plain, % 175.23/175.38 (~P2(f8(f8(a7,a7),a1),a5)+~P3(x6181,a5)+P3(x6181,f8(a7,a7))), % 175.23/175.38 inference(scs_inference,[],[50,47,528,477,21,48,470,30,46,12,31,3,38])). % 175.23/175.38 cnf(621,plain, % 175.23/175.38 (P3(f8(f4(a2,a2,a7),a1),a7)), % 175.23/175.38 inference(scs_inference,[],[82,540,470,30,12])). % 175.23/175.38 cnf(622,plain, % 175.23/175.38 (E(x6221,f8(x6221,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(623,plain, % 175.23/175.38 (P2(f8(a5,a1),f8(f8(a7,a1),a1))), % 175.23/175.38 inference(scs_inference,[],[82,622,374,540,470,30,12,15])). % 175.23/175.38 cnf(669,plain, % 175.23/175.38 (~P1(f8(x6691,f8(a7,x6692)))), % 175.23/175.38 inference(scs_inference,[],[322,33,32])). % 175.23/175.38 cnf(822,plain, % 175.23/175.38 (~P3(f3(f8(a7,a7),a5),a5)), % 175.23/175.38 inference(scs_inference,[],[65,21,39,14])). % 175.23/175.38 cnf(823,plain, % 175.23/175.38 (~P3(f3(f8(a7,a7),a5),f8(a5,a5))), % 175.23/175.38 inference(scs_inference,[],[822,46])). % 175.23/175.38 cnf(829,plain, % 175.23/175.38 (P2(f8(a7,a7),a5)+~P2(f8(f8(a7,a7),f8(a7,a7)),f8(a5,a5))), % 175.23/175.38 inference(scs_inference,[],[299,822,46,265,12,34])). % 175.23/175.38 cnf(840,plain, % 175.23/175.38 (P1(f8(a1,a1))), % 175.23/175.38 inference(scs_inference,[],[16,47,11])). % 175.23/175.38 cnf(843,plain, % 175.23/175.38 (E(f3(f8(x8431,x8431),x8432),f3(x8431,x8432))), % 175.23/175.38 inference(scs_inference,[],[47,9,2])). % 175.23/175.38 cnf(844,plain, % 175.23/175.38 (E(f3(x8441,x8442),f3(f8(x8441,x8441),x8442))), % 175.23/175.38 inference(scs_inference,[],[843,2])). % 175.23/175.38 cnf(845,plain, % 175.23/175.38 (P1(f8(a2,a1))), % 175.23/175.38 inference(scs_inference,[],[17,82,843,2,11])). % 175.23/175.38 cnf(847,plain, % 175.23/175.38 (~P3(x8471,f8(a2,a1))), % 175.23/175.38 inference(scs_inference,[],[17,82,843,2,11,29])). % 175.23/175.38 cnf(849,plain, % 175.23/175.38 (P2(f8(a2,a1),x8491)), % 175.23/175.38 inference(scs_inference,[],[17,82,843,2,11,29,34])). % 175.23/175.38 cnf(851,plain, % 175.23/175.38 (~E(f8(a2,a1),a7)), % 175.23/175.38 inference(scs_inference,[],[17,65,82,843,2,11,29,34,14])). % 175.23/175.38 cnf(852,plain, % 175.23/175.38 (E(f8(a2,a1),a5)+~P2(a5,f8(a2,a1))), % 175.23/175.38 inference(scs_inference,[],[17,65,82,843,2,11,29,34,14,31])). % 175.23/175.38 cnf(857,plain, % 175.23/175.38 (E(f3(x8571,f8(x8572,x8573)),f3(x8571,f8(f8(x8572,x8572),x8573)))), % 175.23/175.38 inference(scs_inference,[],[47,10,4])). % 175.23/175.38 cnf(864,plain, % 175.23/175.38 (P3(f4(a2,a1,a7),a7)), % 175.23/175.38 inference(scs_inference,[],[844,851,849,77,48,31,28,11,40])). % 175.23/175.38 cnf(870,plain, % 175.23/175.38 (P3(f4(a2,a1,a7),f8(a7,x8701))), % 175.23/175.38 inference(scs_inference,[],[844,851,849,77,48,31,28,11,40,44,45])). % 175.23/175.38 cnf(919,plain, % 175.23/175.38 (P3(f4(a1,a1,a7),f8(f8(x9191,f8(x9192,f8(a7,x9193))),a1))), % 175.23/175.38 inference(scs_inference,[],[301,71,44])). % 175.23/175.38 cnf(952,plain, % 175.23/175.38 (E(a5,f8(a7,a1))+~P3(f3(f8(a7,a1),a5),a5)), % 175.23/175.38 inference(scs_inference,[],[135,39])). % 175.23/175.38 cnf(954,plain, % 175.23/175.38 (P2(f8(x9541,a1),x9541)), % 175.23/175.38 inference(scs_inference,[],[21,145,15])). % 175.23/175.38 cnf(982,plain, % 175.23/175.38 (P2(f8(f8(x9821,a1),f8(x9821,a1)),x9821)), % 175.23/175.38 inference(scs_inference,[],[21,161,15])). % 175.23/175.38 cnf(1007,plain, % 175.23/175.38 (P2(f8(f8(x10071,x10071),a1),x10071)), % 175.23/175.38 inference(scs_inference,[],[21,954,15])). % 175.23/175.38 cnf(1112,plain, % 175.23/175.38 (E(f8(x11121,x11122),f8(x11122,x11121))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1113,plain, % 175.23/175.38 (P2(f8(a5,a5),f8(a1,a7))), % 175.23/175.38 inference(scs_inference,[],[22,1112,129,575,12,15])). % 175.23/175.38 cnf(1114,plain, % 175.23/175.38 (E(f8(x11141,x11142),f8(x11142,x11141))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1117,plain, % 175.23/175.38 (P3(f8(a1,f4(a1,a1,a7)),f8(x11171,a7))), % 175.23/175.38 inference(scs_inference,[],[22,1112,1114,107,129,575,12,15,14,44])). % 175.23/175.38 cnf(1119,plain, % 175.23/175.38 (P3(f8(a1,f4(a1,a1,a7)),f8(a7,x11191))), % 175.23/175.38 inference(scs_inference,[],[22,1112,1114,107,129,575,12,15,14,44,45])). % 175.23/175.38 cnf(1125,plain, % 175.23/175.38 (E(f8(a5,a5),f8(a1,a7))+~P2(f8(a1,a7),f8(a5,a5))), % 175.23/175.38 inference(scs_inference,[],[22,1112,1114,107,129,575,12,15,14,44,45,30,205,31])). % 175.23/175.38 cnf(1131,plain, % 175.23/175.38 (P3(f8(a1,f4(a2,a2,a7)),a7)), % 175.23/175.38 inference(scs_inference,[],[22,1119,621,30,12])). % 175.23/175.38 cnf(1132,plain, % 175.23/175.38 (E(f8(x11321,x11322),f8(x11322,x11321))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1133,plain, % 175.23/175.38 (P2(a5,f8(a1,a7))), % 175.23/175.38 inference(scs_inference,[],[22,1132,111,1119,621,30,12,15])). % 175.23/175.38 cnf(1134,plain, % 175.23/175.38 (E(f8(x11341,x11342),f8(x11342,x11341))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1135,plain, % 175.23/175.38 (P2(f8(a1,a5),f8(a7,a7))), % 175.23/175.38 inference(scs_inference,[],[22,1132,1134,175,111,1119,621,30,12,15,14])). % 175.23/175.38 cnf(1137,plain, % 175.23/175.38 (P3(f8(a1,f4(a2,a2,a7)),f8(x11371,a7))), % 175.23/175.38 inference(scs_inference,[],[22,1132,1134,175,111,1119,621,30,12,15,14,44])). % 175.23/175.38 cnf(1139,plain, % 175.23/175.38 (P3(f8(a1,f4(a2,a2,a7)),f8(a7,x11391))), % 175.23/175.38 inference(scs_inference,[],[22,1132,1134,175,111,1119,621,30,12,15,14,44,45])). % 175.23/175.38 cnf(1151,plain, % 175.23/175.38 (P2(f8(a5,a1),f8(a1,a7))), % 175.23/175.38 inference(scs_inference,[],[22,374,1117,30,15])). % 175.23/175.38 cnf(1152,plain, % 175.23/175.38 (E(f8(x11521,x11522),f8(x11522,x11521))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1153,plain, % 175.23/175.38 (P2(f8(a1,a5),f8(a7,a1))), % 175.23/175.38 inference(scs_inference,[],[22,1152,374,1117,30,15,14])). % 175.23/175.38 cnf(1155,plain, % 175.23/175.38 (E(f8(a1,a5),f8(a7,a7))+~P2(f8(a7,a7),f8(a1,a5))), % 175.23/175.38 inference(scs_inference,[],[22,1152,374,1135,1117,30,15,14,31])). % 175.23/175.38 cnf(1158,plain, % 175.23/175.38 (E(f8(a7,a7),f8(a1,a5))+~P2(f8(a7,a7),f8(a1,a5))), % 175.23/175.38 inference(scs_inference,[],[22,1152,50,374,1135,1117,30,15,14,31,3,2])). % 175.23/175.38 cnf(1171,plain, % 175.23/175.38 (P2(a5,f8(a1,f8(a7,a7)))), % 175.23/175.38 inference(scs_inference,[],[22,528,1139,30,15])). % 175.23/175.38 cnf(1172,plain, % 175.23/175.38 (E(f8(x11721,x11722),f8(x11722,x11721))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1174,plain, % 175.23/175.38 (E(f8(x11741,x11742),f8(x11742,x11741))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1175,plain, % 175.23/175.38 (E(f8(a5,a1),f8(a1,a7))+~P2(f8(a1,a7),f8(a5,a1))), % 175.23/175.38 inference(scs_inference,[],[22,1172,268,528,1151,1139,30,15,14,31])). % 175.23/175.38 cnf(1179,plain, % 175.23/175.38 (E(f8(a1,a7),f8(a5,a1))+~P2(f8(a1,a7),f8(a5,a1))), % 175.23/175.38 inference(scs_inference,[],[22,1172,1174,268,528,1151,1139,30,15,14,31,3,2])). % 175.23/175.38 cnf(1193,plain, % 175.23/175.38 (E(f8(x11931,x11932),f8(x11932,x11931))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1199,plain, % 175.23/175.38 (E(f8(a7,a1),f8(a1,a5))+~P2(f8(a7,a1),f8(a1,a5))), % 175.23/175.38 inference(scs_inference,[],[22,1193,87,577,530,1153,1137,30,15,14,31,3,2])). % 175.23/175.38 cnf(1213,plain, % 175.23/175.38 (E(f8(x12131,x12132),f8(x12132,x12131))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1218,plain, % 175.23/175.38 (E(f8(a5,a1),f8(a1,a7))+~P2(f8(a1,a7),a5)), % 175.23/175.38 inference(scs_inference,[],[22,1213,206,232,1133,19,1131,30,15,14,31,3])). % 175.23/175.38 cnf(1293,plain, % 175.23/175.38 (E(f8(x12931,x12932),f8(x12932,x12931))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1294,plain, % 175.23/175.38 (P2(f8(a1,f8(a5,a5)),f8(a7,a1))), % 175.23/175.38 inference(scs_inference,[],[22,1293,344,15,14])). % 175.23/175.38 cnf(1335,plain, % 175.23/175.38 (P2(f8(f8(a5,a1),a1),f8(a1,a7))), % 175.23/175.38 inference(scs_inference,[],[22,550,15])). % 175.23/175.38 cnf(1356,plain, % 175.23/175.38 (E(f8(x13561,x13562),f8(x13562,x13561))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1357,plain, % 175.23/175.38 (P2(f8(a1,a5),f8(f8(a7,a1),a1))), % 175.23/175.38 inference(scs_inference,[],[22,1356,623,15,14])). % 175.23/175.38 cnf(1374,plain, % 175.23/175.38 (P2(f8(x13741,a1),f8(a1,f8(x13741,x13741)))), % 175.23/175.38 inference(scs_inference,[],[22,372,15])). % 175.23/175.38 cnf(1415,plain, % 175.23/175.38 (E(f8(x14151,x14152),f8(x14152,x14151))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1416,plain, % 175.23/175.38 (P2(f8(a1,x14161),f8(a1,f8(x14161,x14161)))), % 175.23/175.38 inference(scs_inference,[],[22,1415,1294,1374,15,14])). % 175.23/175.38 cnf(1437,plain, % 175.23/175.38 (E(f8(x14371,x14372),f8(x14372,x14371))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1438,plain, % 175.23/175.38 (P2(f8(a1,a5),f8(a1,a7))), % 175.23/175.38 inference(scs_inference,[],[22,1437,1357,1151,15,14])). % 175.23/175.38 cnf(1456,plain, % 175.23/175.38 (E(f8(x14561,x14562),f8(x14562,x14561))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1458,plain, % 175.23/175.38 (E(f8(x14581,x14582),f8(x14582,x14581))), % 175.23/175.38 inference(rename_variables,[],[22])). % 175.23/175.38 cnf(1461,plain, % 175.23/175.38 (E(f8(a5,a1),f8(a1,a7))+~P2(f8(a1,a7),f8(a1,a5))), % 175.23/175.38 inference(scs_inference,[],[22,1456,1458,1438,1416,1335,15,14,31,3])). % 175.23/175.38 cnf(1463,plain, % 175.23/175.38 (E(f8(a1,a7),f8(a1,a5))+~P2(f8(a1,a7),f8(a1,a5))), % 175.23/175.38 inference(scs_inference,[],[22,1456,1458,1438,1416,1335,15,14,31,3,2])). % 175.23/175.38 cnf(1599,plain, % 175.23/175.38 (E(f8(a1,f8(a7,a7)),a5)+~P2(f8(a1,f8(a7,a7)),a5)), % 175.23/175.38 inference(scs_inference,[],[1171,19,669,31,11,3,2])). % 175.23/175.38 cnf(1715,plain, % 175.23/175.38 (~P2(f8(a1,f8(a1,a1)),f8(a1,a1))+P1(f8(a1,f8(a1,a1)))), % 175.23/175.38 inference(scs_inference,[],[1416,840,31,11])). % 175.23/175.38 cnf(1729,plain, % 175.23/175.38 (E(x17291,f8(x17291,x17291))), % 175.23/175.38 inference(rename_variables,[],[47])). % 175.23/175.38 cnf(1730,plain, % 175.23/175.38 (P2(f8(f8(a1,a5),f8(a1,a5)),f8(a1,a7))), % 175.23/175.38 inference(scs_inference,[],[47,1729,1113,1438,15,14])). % 175.23/175.38 cnf(1751,plain, % 175.23/175.38 (E(x17511,f8(x17511,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(1753,plain, % 175.23/175.38 (E(x17531,f8(x17531,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(1760,plain, % 175.23/175.38 (E(f8(a1,a5),f8(a1,a7))+~P2(f8(a1,a7),f8(f8(a1,a5),f8(a1,a5)))), % 175.23/175.38 inference(scs_inference,[],[82,1751,1753,47,1113,1135,1730,870,12,15,14,30,31,3])). % 175.23/175.38 cnf(1811,plain, % 175.23/175.38 (E(x18111,f8(x18111,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(1813,plain, % 175.23/175.38 (E(x18131,f8(x18131,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(1814,plain, % 175.23/175.38 (P2(f8(f8(a1,a5),a1),f8(a1,a7))), % 175.23/175.38 inference(scs_inference,[],[82,1811,1813,1438,1133,864,12,15,14])). % 175.23/175.38 cnf(1963,plain, % 175.23/175.38 (E(f8(a1,a5),f8(a1,a7))+~P2(f8(a1,a7),f8(f8(a1,a5),a1))), % 175.23/175.38 inference(scs_inference,[],[82,1814,31,3])). % 175.23/175.38 cnf(2008,plain, % 175.23/175.38 (~P3(x20081,f8(a1,f8(a1,a1)))), % 175.23/175.38 inference(scs_inference,[],[48,55,46])). % 175.23/175.38 cnf(2013,plain, % 175.23/175.38 (~P1(f8(x20131,a7))), % 175.23/175.38 inference(scs_inference,[],[48,299,55,46,13,25])). % 175.23/175.38 cnf(2016,plain, % 175.23/175.38 (~P3(x20161,f8(a1,f8(a2,a2)))), % 175.23/175.38 inference(scs_inference,[],[48,105,46])). % 175.23/175.38 cnf(2021,plain, % 175.23/175.38 (~P1(f8(a7,x20211))), % 175.23/175.38 inference(scs_inference,[],[48,477,105,46,13,25])). % 175.23/175.38 cnf(2023,plain, % 175.23/175.38 (~P3(x20231,f8(a1,a2))), % 175.23/175.38 inference(scs_inference,[],[48,77,46])). % 175.23/175.38 cnf(2028,plain, % 175.23/175.38 (~P1(f8(f8(a7,x20281),x20282))), % 175.23/175.38 inference(scs_inference,[],[48,497,77,46,13,25])). % 175.23/175.38 cnf(2030,plain, % 175.23/175.38 (P3(f3(a5,f8(a2,a1)),a5)+E(f8(a2,a1),a5)), % 175.23/175.38 inference(scs_inference,[],[852,34])). % 175.23/175.38 cnf(2031,plain, % 175.23/175.38 (P2(f8(a1,a2),x20311)), % 175.23/175.38 inference(scs_inference,[],[2023,34])). % 175.23/175.38 cnf(2032,plain, % 175.23/175.38 (~P3(x20321,f8(a1,a2))), % 175.23/175.38 inference(rename_variables,[],[2023])). % 175.23/175.38 cnf(2039,plain, % 175.23/175.38 (~E(f8(a1,a2),a7)), % 175.23/175.38 inference(scs_inference,[],[48,65,332,2023,2032,34,46,13,14])). % 175.23/175.38 cnf(2040,plain, % 175.23/175.38 (E(f8(a1,a2),a5)+~P2(a5,f8(a1,a2))), % 175.23/175.38 inference(scs_inference,[],[48,65,332,2023,2032,34,46,13,14,31])). % 175.23/175.38 cnf(2057,plain, % 175.23/175.38 (~P2(a7,f8(a1,a2))), % 175.23/175.38 inference(scs_inference,[],[2039,2031,31])). % 175.23/175.38 cnf(2060,plain, % 175.23/175.38 (~P3(x20601,f8(a1,f8(a2,a1)))), % 175.23/175.38 inference(scs_inference,[],[48,2039,2031,847,31,46])). % 175.23/175.38 cnf(2064,plain, % 175.23/175.38 (~P3(x20641,a1)), % 175.23/175.38 inference(rename_variables,[],[48])). % 175.23/175.38 cnf(2073,plain, % 175.23/175.38 (P3(f4(a1,a2,a7),f8(x20731,a7))), % 175.23/175.38 inference(scs_inference,[],[48,2064,2039,359,2031,77,847,31,46,13,25,28,40,44])). % 175.23/175.38 cnf(2075,plain, % 175.23/175.38 (P3(f4(a1,a2,a7),f8(a7,x20751))), % 175.23/175.38 inference(scs_inference,[],[48,2064,2039,359,2031,77,847,31,46,13,25,28,40,44,45])). % 175.23/175.38 cnf(2084,plain, % 175.23/175.38 (P3(f8(f4(a1,a2,a7),f4(a1,a2,a7)),a7)), % 175.23/175.38 inference(scs_inference,[],[48,2064,47,52,2039,359,2031,77,847,31,46,13,25,28,40,44,45,30,35,205,12])). % 175.23/175.38 cnf(2105,plain, % 175.23/175.38 (P3(f4(a1,a2,a7),f8(x21051,f8(x21052,a7)))), % 175.23/175.38 inference(scs_inference,[],[2073,44])). % 175.23/175.38 cnf(2120,plain, % 175.23/175.38 (E(x21201,f8(x21201,a1))), % 175.23/175.38 inference(rename_variables,[],[82])). % 175.23/175.38 cnf(2123,plain, % 175.23/175.38 (E(f8(f8(x21231,x21231),a1),f8(x21231,a1))), % 175.23/175.38 inference(scs_inference,[],[82,2120,372,1007,2105,2075,2084,44,30,12,15,31])). % 175.23/175.38 cnf(2141,plain, % 175.23/175.38 (E(f8(x21411,a1),f8(f8(x21411,x21411),a1))), % 175.23/175.38 inference(scs_inference,[],[2123,2073,30,2])). % 175.23/175.38 cnf(2199,plain, % 175.23/175.39 (P3(f3(a5,f8(a1,a2)),a5)+E(f8(a1,a2),a5)), % 175.23/175.39 inference(scs_inference,[],[2040,34])). % 175.23/175.39 cnf(2200,plain, % 175.23/175.39 (~P3(x22001,f8(f8(a1,a1),f8(a1,a2)))), % 175.23/175.39 inference(scs_inference,[],[55,2023,46])). % 175.23/175.39 cnf(2211,plain, % 175.23/175.39 (~P3(x22111,f8(f8(a1,a1),f8(a2,a1)))), % 175.23/175.39 inference(scs_inference,[],[55,847,46])). % 175.23/175.39 cnf(2214,plain, % 175.23/175.39 (~E(f8(x22141,a7),f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[55,473,847,46,13])). % 175.23/175.39 cnf(2256,plain, % 175.23/175.39 (P1(f8(f8(a1,a1),a1))), % 175.23/175.39 inference(scs_inference,[],[62,1007,16,31,2,11])). % 175.23/175.39 cnf(2259,plain, % 175.23/175.39 (~E(a5,f8(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[64,19,3])). % 175.23/175.39 cnf(2261,plain, % 175.23/175.39 (~P2(f8(a7,a1),a5)), % 175.23/175.39 inference(scs_inference,[],[64,19,3,135])). % 175.23/175.39 cnf(2262,plain, % 175.23/175.39 (~E(f8(a7,a1),a5)), % 175.23/175.39 inference(scs_inference,[],[64,19,3,135,28])). % 175.23/175.39 cnf(2266,plain, % 175.23/175.39 (~P3(f4(a7,a1,a5),f8(a5,a5))+~P3(f4(a7,a1,a5),a7)), % 175.23/175.39 inference(scs_inference,[],[64,19,3,135,28,42,46])). % 175.23/175.39 cnf(2281,plain, % 175.23/175.39 (~P3(f3(f8(a7,a1),a5),a5)), % 175.23/175.39 inference(scs_inference,[],[2259,952])). % 175.23/175.39 cnf(2285,plain, % 175.23/175.39 (~E(f8(a1,f8(a7,a7)),a5)), % 175.23/175.39 inference(scs_inference,[],[2261,1374,2281,46,15])). % 175.23/175.39 cnf(2292,plain, % 175.23/175.39 (~E(f8(f8(a7,a7),f8(a7,a7)),f8(a5,a5))), % 175.23/175.39 inference(scs_inference,[],[64,2261,1374,2281,21,46,15,3,96,829,1599,28])). % 175.23/175.39 cnf(2318,plain, % 175.23/175.39 (P3(f4(a7,a1,a5),a7)), % 175.23/175.39 inference(scs_inference,[],[18,2261,372,2259,48,15,40,44,45,30,618,35])). % 175.23/175.39 cnf(2328,plain, % 175.23/175.39 (~P3(f4(a7,a1,a5),f8(a5,a5))), % 175.23/175.39 inference(scs_inference,[],[2318,2266])). % 175.23/175.39 cnf(2329,plain, % 175.23/175.39 (P3(f4(a7,a1,a5),f8(a7,x23291))), % 175.23/175.39 inference(scs_inference,[],[2318,45])). % 175.23/175.39 cnf(2331,plain, % 175.23/175.39 (P3(f4(a7,a1,a5),f8(x23311,a7))), % 175.23/175.39 inference(scs_inference,[],[2318,45,44])). % 175.23/175.39 cnf(2335,plain, % 175.23/175.39 (P3(f4(a7,a1,a5),f8(f8(a7,x23351),f8(a7,x23351)))), % 175.23/175.39 inference(scs_inference,[],[52,2318,45,44,30,35])). % 175.23/175.39 cnf(2361,plain, % 175.23/175.39 (~P3(f4(a7,a1,a5),f8(f8(a5,a5),f8(a5,a5)))), % 175.23/175.39 inference(scs_inference,[],[52,2335,2328,2329,2331,45,44,30,35,46])). % 175.23/175.39 cnf(2390,plain, % 175.23/175.39 (~P3(f8(x23901,a7),f4(a7,a1,a5))), % 175.23/175.39 inference(scs_inference,[],[2331,30])). % 175.23/175.39 cnf(2413,plain, % 175.23/175.39 (~E(a7,f8(a5,a5))), % 175.23/175.39 inference(scs_inference,[],[69,21,3])). % 175.23/175.39 cnf(2445,plain, % 175.23/175.39 (~P3(x24451,f8(a2,f8(a1,a1)))), % 175.23/175.39 inference(scs_inference,[],[77,55,46])). % 175.23/175.39 cnf(2450,plain, % 175.23/175.39 (~P3(x24501,f8(a2,f8(a1,a2)))), % 175.23/175.39 inference(scs_inference,[],[77,2023,46])). % 175.23/175.39 cnf(2456,plain, % 175.23/175.39 (~P3(x24561,f8(a2,f8(a2,a2)))), % 175.23/175.39 inference(scs_inference,[],[77,105,46])). % 175.23/175.39 cnf(2462,plain, % 175.23/175.39 (~P3(x24621,f8(a2,f8(a2,a1)))), % 175.23/175.39 inference(scs_inference,[],[77,847,46])). % 175.23/175.39 cnf(2477,plain, % 175.23/175.39 (~P3(a5,f3(a5,f8(a1,a2)))+E(f8(a1,a2),a5)), % 175.23/175.39 inference(scs_inference,[],[2199,30])). % 175.23/175.39 cnf(2480,plain, % 175.23/175.39 (~P2(f8(a7,a7),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[85,19,3,203])). % 175.23/175.39 cnf(2512,plain, % 175.23/175.39 (~E(a5,a1)), % 175.23/175.39 inference(scs_inference,[],[87,22,3,4])). % 175.23/175.39 cnf(2513,plain, % 175.23/175.39 (~P1(a5)), % 175.23/175.39 inference(scs_inference,[],[87,22,16,3,4,26])). % 175.23/175.39 cnf(2623,plain, % 175.23/175.39 (~P3(x26231,f8(f8(a2,a1),f8(a2,a1)))), % 175.23/175.39 inference(scs_inference,[],[102,982,346,17,847,31,3,40,45,44,30,2,11,29])). % 175.23/175.39 cnf(2650,plain, % 175.23/175.39 (~P3(a5,f8(f3(a5,f8(a1,a2)),f3(a5,f8(a1,a2))))+E(f8(a1,a2),a5)), % 175.23/175.39 inference(scs_inference,[],[2477,46])). % 175.23/175.39 cnf(2653,plain, % 175.23/175.39 (~P3(x26531,f8(f8(a2,a2),f8(a1,a1)))), % 175.23/175.39 inference(scs_inference,[],[105,55,46])). % 175.23/175.39 cnf(2664,plain, % 175.23/175.39 (~P3(x26641,f8(f8(a2,a2),f8(a1,a2)))), % 175.23/175.39 inference(scs_inference,[],[105,2023,46])). % 175.23/175.39 cnf(2678,plain, % 175.23/175.39 (P2(f8(f8(a2,a2),a2),x26781)), % 175.23/175.39 inference(scs_inference,[],[105,77,46,34])). % 175.23/175.39 cnf(2680,plain, % 175.23/175.39 (~E(f8(f8(a2,a2),a2),a7)), % 175.23/175.39 inference(scs_inference,[],[105,65,77,46,34,14])). % 175.23/175.39 cnf(2691,plain, % 175.23/175.39 (~P3(x26911,f8(f8(a2,a2),f8(a2,a1)))), % 175.23/175.39 inference(scs_inference,[],[105,2680,2678,847,31,46])). % 175.23/175.39 cnf(2694,plain, % 175.23/175.39 (P2(f8(f8(a2,a2),f8(a2,a1)),x26941)), % 175.23/175.39 inference(scs_inference,[],[105,2680,2678,847,31,46,34])). % 175.23/175.39 cnf(2751,plain, % 175.23/175.39 (P1(f8(a1,f8(a2,a2)))), % 175.23/175.39 inference(scs_inference,[],[109,22,11])). % 175.23/175.39 cnf(2900,plain, % 175.23/175.39 (E(f8(a7,a1),f8(a5,a1))+P3(f3(f8(a7,a1),f8(a5,a1)),f8(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[426,34])). % 175.23/175.39 cnf(2907,plain, % 175.23/175.39 (~P2(f8(a1,a7),f8(a5,a5))), % 175.23/175.39 inference(scs_inference,[],[2318,2328,1125,36])). % 175.23/175.39 cnf(2924,plain, % 175.23/175.39 (~P2(f8(a7,a7),f8(a1,a5))+P3(f4(a7,a1,a5),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[2318,1155,37])). % 175.23/175.39 cnf(2938,plain, % 175.23/175.39 (E(f8(a7,a7),f8(a1,a5))+P3(f3(f8(a7,a7),f8(a1,a5)),f8(a7,a7))), % 175.23/175.39 inference(scs_inference,[],[1158,34])). % 175.23/175.39 cnf(2947,plain, % 175.23/175.39 (P3(f4(a7,a7,f8(a1,a1)),f8(x29471,a7))), % 175.23/175.39 inference(scs_inference,[],[280,55,21,3,40,45,44])). % 175.23/175.39 cnf(2954,plain, % 175.23/175.39 (~E(f8(a1,a1),f8(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[280,2947,19,30,3])). % 175.23/175.39 cnf(2964,plain, % 175.23/175.39 (E(f8(a1,a7),f8(a5,a1))+~P3(f3(f8(a1,a7),f8(a5,a1)),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[1179,39])). % 175.23/175.39 cnf(2973,plain, % 175.23/175.39 (E(f8(a7,a1),f8(a1,a5))+P3(f3(f8(a7,a1),f8(a1,a5)),f8(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[1199,34])). % 175.23/175.39 cnf(2978,plain, % 175.23/175.39 (E(f8(a1,a7),f8(a1,a5))+~P3(f3(f8(a1,a7),f8(a1,a5)),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[1463,39])). % 175.23/175.39 cnf(2980,plain, % 175.23/175.39 (~E(a1,f8(a7,a7))), % 175.23/175.39 inference(scs_inference,[],[294,21,3])). % 175.23/175.39 cnf(2982,plain, % 175.23/175.39 (P3(f4(a7,a7,a1),a7)), % 175.23/175.39 inference(scs_inference,[],[294,21,48,3,40])). % 175.23/175.39 cnf(2985,plain, % 175.23/175.39 (P3(f4(a7,a7,a1),f8(a7,x29851))), % 175.23/175.39 inference(scs_inference,[],[294,21,48,3,40,45])). % 175.23/175.39 cnf(2987,plain, % 175.23/175.39 (P3(f4(a7,a7,a1),f8(x29871,a7))), % 175.23/175.39 inference(scs_inference,[],[294,21,48,3,40,45,44])). % 175.23/175.39 cnf(2991,plain, % 175.23/175.39 (P3(f4(a7,a7,a1),f8(a1,f8(a7,a7)))), % 175.23/175.39 inference(scs_inference,[],[294,1374,21,48,3,40,45,44,30,35])). % 175.23/175.39 cnf(2996,plain, % 175.23/175.39 (P3(f8(f4(a7,a7,a1),a1),a7)), % 175.23/175.39 inference(scs_inference,[],[294,82,1374,21,48,3,40,45,44,30,35,46,12])). % 175.23/175.39 cnf(3011,plain, % 175.23/175.39 (E(x30111,f8(x30111,a1))), % 175.23/175.39 inference(rename_variables,[],[82])). % 175.23/175.39 cnf(3014,plain, % 175.23/175.39 (~E(a1,f8(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[294,82,3011,52,2991,2987,2985,19,2996,45,44,30,35,12,13,3])). % 175.23/175.39 cnf(3016,plain, % 175.23/175.39 (P3(f4(a7,a1,a1),a7)), % 175.23/175.39 inference(scs_inference,[],[294,82,3011,52,2991,2987,2985,19,48,2996,45,44,30,35,12,13,3,40])). % 175.23/175.39 cnf(3056,plain, % 175.23/175.39 (P3(f4(a7,a1,a1),f8(a7,x30561))), % 175.23/175.39 inference(scs_inference,[],[3016,45])). % 175.23/175.39 cnf(3058,plain, % 175.23/175.39 (P3(f4(a7,a1,a1),f8(x30581,a7))), % 175.23/175.39 inference(scs_inference,[],[3016,45,44])). % 175.23/175.39 cnf(3108,plain, % 175.23/175.39 (~P3(f8(a7,x31081),f4(a7,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3056,30])). % 175.23/175.39 cnf(3113,plain, % 175.23/175.39 (~P3(f8(x31131,a7),f4(a7,a7,a1))), % 175.23/175.39 inference(scs_inference,[],[2987,30])). % 175.23/175.39 cnf(3118,plain, % 175.23/175.39 (~P3(f8(x31181,a7),f4(a7,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3058,30])). % 175.23/175.39 cnf(3144,plain, % 175.23/175.39 (~P3(a7,f4(a7,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3016,30])). % 175.23/175.39 cnf(3174,plain, % 175.23/175.39 (~P3(f3(a7,a5),a5)), % 175.23/175.39 inference(scs_inference,[],[65,39])). % 175.23/175.39 cnf(3176,plain, % 175.23/175.39 (E(f3(a1,x31761),f3(a2,x31761))), % 175.23/175.39 inference(scs_inference,[],[336,65,39,9])). % 175.23/175.39 cnf(3177,plain, % 175.23/175.39 (E(f3(x31771,a1),f3(x31771,a2))), % 175.23/175.39 inference(scs_inference,[],[336,65,39,9,10])). % 175.23/175.39 cnf(3178,plain, % 175.23/175.39 (E(f4(x31781,a1,x31782),f4(x31781,a2,x31782))), % 175.23/175.39 inference(scs_inference,[],[336,65,39,9,10,7])). % 175.23/175.39 cnf(3179,plain, % 175.23/175.39 (E(f4(x31791,x31792,a1),f4(x31791,x31792,a2))), % 175.23/175.39 inference(scs_inference,[],[336,65,39,9,10,7,8])). % 175.23/175.39 cnf(3180,plain, % 175.23/175.39 (~P1(f8(x31801,a6))), % 175.23/175.39 inference(scs_inference,[],[336,23,65,39,9,10,7,8,32])). % 175.23/175.39 cnf(3182,plain, % 175.23/175.39 (~P1(f8(a6,x31821))), % 175.23/175.39 inference(scs_inference,[],[336,23,65,39,9,10,7,8,32,33])). % 175.23/175.39 cnf(3184,plain, % 175.23/175.39 (E(f4(a1,x31841,x31842),f4(a2,x31841,x31842))), % 175.23/175.39 inference(scs_inference,[],[336,23,65,39,9,10,7,8,32,33,6])). % 175.23/175.39 cnf(3185,plain, % 175.23/175.39 (E(f8(x31851,a1),f8(x31851,a2))), % 175.23/175.39 inference(scs_inference,[],[336,23,65,39,9,10,7,8,32,33,6,5])). % 175.23/175.39 cnf(3186,plain, % 175.23/175.39 (E(f8(a2,a1),a1)), % 175.23/175.39 inference(scs_inference,[],[845,336,23,65,39,9,10,7,8,32,33,6,5,25])). % 175.23/175.39 cnf(3188,plain, % 175.23/175.39 (E(f8(a1,x31881),f8(a2,x31881))), % 175.23/175.39 inference(scs_inference,[],[845,336,23,65,39,9,10,7,8,32,33,6,5,25,4])). % 175.23/175.39 cnf(3189,plain, % 175.23/175.39 (P3(f3(a7,a2),a7)), % 175.23/175.39 inference(scs_inference,[],[583,845,336,23,65,39,9,10,7,8,32,33,6,5,25,4,34])). % 175.23/175.39 cnf(3191,plain, % 175.23/175.39 (P2(f8(x31911,x31911),x31911)), % 175.23/175.39 inference(scs_inference,[],[583,845,336,23,65,21,39,9,10,7,8,32,33,6,5,25,4,34,28])). % 175.23/175.39 cnf(3193,plain, % 175.23/175.39 (~P3(a7,f3(a7,a2))), % 175.23/175.39 inference(scs_inference,[],[583,845,336,23,65,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30])). % 175.23/175.39 cnf(3195,plain, % 175.23/175.39 (~E(a7,f8(a5,a7))), % 175.23/175.39 inference(scs_inference,[],[24,583,845,336,23,65,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30,2])). % 175.23/175.39 cnf(3196,plain, % 175.23/175.39 (~P3(f4(a7,a1,a5),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[24,583,845,336,23,2328,145,65,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30,2,35])). % 175.23/175.39 cnf(3199,plain, % 175.23/175.39 (~E(f8(a1,a2),f8(a7,x31991))), % 175.23/175.39 inference(scs_inference,[],[24,2982,583,845,336,23,2328,2023,145,65,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30,2,35,37])). % 175.23/175.39 cnf(3200,plain, % 175.23/175.39 (~P3(x32001,f8(a1,a2))), % 175.23/175.39 inference(rename_variables,[],[2023])). % 175.23/175.39 cnf(3202,plain, % 175.23/175.39 (~E(f8(a1,a2),f8(x32021,a7))), % 175.23/175.39 inference(scs_inference,[],[24,2982,583,845,336,23,2328,2023,3200,145,65,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30,2,35,37,36])). % 175.23/175.39 cnf(3208,plain, % 175.23/175.39 (~E(f8(a2,a1),f8(x32081,a7))), % 175.23/175.39 inference(scs_inference,[],[24,2982,2013,2214,583,845,336,23,79,2328,2023,3200,145,65,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30,2,35,37,36,31,11])). % 175.23/175.39 cnf(3209,plain, % 175.23/175.39 (~P2(f8(a7,a1),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[24,2982,2013,2214,583,845,336,23,79,2261,2328,2023,3200,145,65,19,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30,2,35,37,36,31,11,15])). % 175.23/175.39 cnf(3210,plain, % 175.23/175.39 (E(f8(x32101,a1),x32101)), % 175.23/175.39 inference(rename_variables,[],[19])). % 175.23/175.39 cnf(3212,plain, % 175.23/175.39 (E(f8(x32121,a1),x32121)), % 175.23/175.39 inference(rename_variables,[],[19])). % 175.23/175.39 cnf(3213,plain, % 175.23/175.39 (~P3(f8(a7,a1),f3(a7,a2))), % 175.23/175.39 inference(scs_inference,[],[24,2982,2013,2057,2214,583,845,336,23,79,2261,2328,2023,3200,145,65,19,3210,3212,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30,2,35,37,36,31,11,15,14,12])). % 175.23/175.39 cnf(3214,plain, % 175.23/175.39 (E(f8(x32141,a1),x32141)), % 175.23/175.39 inference(rename_variables,[],[19])). % 175.23/175.39 cnf(3216,plain, % 175.23/175.39 (~P3(f3(a7,a5),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[24,2982,2980,2013,2057,2214,583,845,336,23,79,2261,2328,2023,3200,145,65,19,3210,3212,3214,21,39,9,10,7,8,32,33,6,5,25,4,34,28,30,2,35,37,36,31,11,15,14,12,3,13])). % 175.23/175.39 cnf(3220,plain, % 175.23/175.39 (~P1(f8(x32201,a5))), % 175.23/175.39 inference(scs_inference,[],[2513,32])). % 175.23/175.39 cnf(3222,plain, % 175.23/175.39 (~P1(f8(a5,x32221))), % 175.23/175.39 inference(scs_inference,[],[2513,32,33])). % 175.23/175.39 cnf(3224,plain, % 175.23/175.39 (E(f3(x32241,a2),f3(x32241,a1))), % 175.23/175.39 inference(scs_inference,[],[2513,329,32,33,10])). % 175.23/175.39 cnf(3225,plain, % 175.23/175.39 (E(f4(x32251,x32252,a2),f4(x32251,x32252,a1))), % 175.23/175.39 inference(scs_inference,[],[2513,329,32,33,10,8])). % 175.23/175.39 cnf(3226,plain, % 175.23/175.39 (E(f3(a2,x32261),f3(a1,x32261))), % 175.23/175.39 inference(scs_inference,[],[2513,329,32,33,10,8,9])). % 175.23/175.39 cnf(3227,plain, % 175.23/175.39 (E(f4(x32271,a2,x32272),f4(x32271,a1,x32272))), % 175.23/175.39 inference(scs_inference,[],[2513,329,32,33,10,8,9,7])). % 175.23/175.39 cnf(3228,plain, % 175.23/175.39 (E(f4(a2,x32281,x32282),f4(a1,x32281,x32282))), % 175.23/175.39 inference(scs_inference,[],[2513,329,32,33,10,8,9,7,6])). % 175.23/175.39 cnf(3229,plain, % 175.23/175.39 (E(f8(x32291,a2),f8(x32291,a1))), % 175.23/175.39 inference(scs_inference,[],[2513,329,32,33,10,8,9,7,6,5])). % 175.23/175.39 cnf(3230,plain, % 175.23/175.39 (E(f8(a2,a2),a1)), % 175.23/175.39 inference(scs_inference,[],[2513,329,83,32,33,10,8,9,7,6,5,25])). % 175.23/175.39 cnf(3232,plain, % 175.23/175.39 (E(f8(a2,x32321),f8(a1,x32321))), % 175.23/175.39 inference(scs_inference,[],[2513,329,83,32,33,10,8,9,7,6,5,25,4])). % 175.23/175.39 cnf(3233,plain, % 175.23/175.39 (P3(f3(a7,a1),a7)), % 175.23/175.39 inference(scs_inference,[],[324,2513,329,83,32,33,10,8,9,7,6,5,25,4,34])). % 175.23/175.39 cnf(3235,plain, % 175.23/175.39 (P2(f4(x32351,a1,x32352),f4(x32351,a2,x32352))), % 175.23/175.39 inference(scs_inference,[],[3178,324,2513,329,83,32,33,10,8,9,7,6,5,25,4,34,28])). % 175.23/175.39 cnf(3239,plain, % 175.23/175.39 (~E(f8(a7,x32391),f8(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3199,3178,324,2513,329,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2])). % 175.23/175.39 cnf(3240,plain, % 175.23/175.39 (~P3(f3(a7,a5),f8(a5,a5))), % 175.23/175.39 inference(scs_inference,[],[3191,3199,3178,3174,324,2513,329,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35])). % 175.23/175.39 cnf(3243,plain, % 175.23/175.39 (~E(f8(a2,a1),f8(a7,x32431))), % 175.23/175.39 inference(scs_inference,[],[3191,3199,3178,3174,3189,324,2513,329,847,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37])). % 175.23/175.39 cnf(3246,plain, % 175.23/175.39 (~E(f8(a2,a2),f8(x32461,a7))), % 175.23/175.39 inference(scs_inference,[],[3191,3199,3178,3174,3189,324,2513,329,847,105,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37,36])). % 175.23/175.39 cnf(3249,plain, % 175.23/175.39 (~P2(f8(a7,a1),f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[2954,3191,3199,3178,3174,3189,324,2513,79,329,847,105,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37,36,31])). % 175.23/175.39 cnf(3252,plain, % 175.23/175.39 (~E(f8(a1,a1),f8(a7,x32521))), % 175.23/175.39 inference(scs_inference,[],[2954,3191,3199,3178,3174,2021,3189,324,2513,840,79,329,847,105,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37,36,31,11])). % 175.23/175.39 cnf(3253,plain, % 175.23/175.39 (~P2(f8(a7,a1),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[2954,3191,3209,3199,3178,3174,2021,3189,324,2513,840,79,329,847,105,22,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37,36,31,11,15])). % 175.23/175.39 cnf(3254,plain, % 175.23/175.39 (E(f8(x32541,x32542),f8(x32542,x32541))), % 175.23/175.39 inference(rename_variables,[],[22])). % 175.23/175.39 cnf(3255,plain, % 175.23/175.39 (P2(f4(x32551,a2,x32552),f4(x32551,a1,x32552))), % 175.23/175.39 inference(scs_inference,[],[2954,3191,3209,3199,3178,3174,2021,3189,324,2513,20,840,79,329,847,105,22,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37,36,31,11,15,14])). % 175.23/175.39 cnf(3257,plain, % 175.23/175.39 (~P3(f8(a1,a7),f3(a7,a2))), % 175.23/175.39 inference(scs_inference,[],[2954,3191,3209,3213,3199,3178,3174,2021,3189,324,2513,20,840,79,329,847,105,22,3254,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37,36,31,11,15,14,12])). % 175.23/175.39 cnf(3258,plain, % 175.23/175.39 (E(f8(x32581,x32582),f8(x32582,x32581))), % 175.23/175.39 inference(rename_variables,[],[22])). % 175.23/175.39 cnf(3259,plain, % 175.23/175.39 (~E(f8(a7,a5),a7)), % 175.23/175.39 inference(scs_inference,[],[24,2954,3191,3209,3213,3199,3178,3174,2021,3189,324,2513,20,840,79,329,847,105,22,3254,3258,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37,36,31,11,15,14,12,3])). % 175.23/175.39 cnf(3261,plain, % 175.23/175.39 (~P3(f8(a7,a1),f3(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[24,2954,3191,3209,3213,3199,3178,3174,3177,2021,3189,324,2513,20,840,79,329,847,105,22,3254,3258,83,32,33,10,8,9,7,6,5,25,4,34,28,30,2,35,37,36,31,11,15,14,12,3,13])). % 175.23/175.39 cnf(3267,plain, % 175.23/175.39 (P3(f3(a7,a5),a7)), % 175.23/175.39 inference(scs_inference,[],[65,34])). % 175.23/175.39 cnf(3269,plain, % 175.23/175.39 (P2(f4(x32691,x32692,a1),f4(x32691,x32692,a2))), % 175.23/175.39 inference(scs_inference,[],[3179,65,34,28])). % 175.23/175.39 cnf(3271,plain, % 175.23/175.39 (~P3(a7,f3(a7,a5))), % 175.23/175.39 inference(scs_inference,[],[3179,65,34,28,30])). % 175.23/175.39 cnf(3273,plain, % 175.23/175.39 (~E(f8(x32731,a7),f8(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3202,3179,65,34,28,30,2])). % 175.23/175.39 cnf(3277,plain, % 175.23/175.39 (~E(f8(a5,a1),f8(a7,x32771))), % 175.23/175.39 inference(scs_inference,[],[3144,3202,3179,3255,3196,65,2318,34,28,30,2,35,37])). % 175.23/175.39 cnf(3279,plain, % 175.23/175.39 (~E(f8(a5,a1),f8(x32791,a7))), % 175.23/175.39 inference(scs_inference,[],[3144,3202,3179,3255,3196,65,2318,34,28,30,2,35,37,36])). % 175.23/175.39 cnf(3284,plain, % 175.23/175.39 (~P2(f8(a7,a1),f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3253,3144,3202,3239,3179,3255,3232,3196,2031,65,2318,34,28,30,2,35,37,36,31,15])). % 175.23/175.39 cnf(3285,plain, % 175.23/175.39 (E(f8(a2,x32851),f8(a1,x32851))), % 175.23/175.39 inference(rename_variables,[],[3232])). % 175.23/175.39 cnf(3286,plain, % 175.23/175.39 (~E(f8(a1,a1),f8(x32861,a6))), % 175.23/175.39 inference(scs_inference,[],[3253,3144,3202,3239,3179,3255,3232,3180,3196,2031,840,65,2318,34,28,30,2,35,37,36,31,15,11])). % 175.23/175.39 cnf(3289,plain, % 175.23/175.39 (~P3(f8(a2,a7),f3(a7,a2))), % 175.23/175.39 inference(scs_inference,[],[3249,3253,3144,3257,3202,3239,3179,3255,3229,3232,3285,3180,3196,2031,840,65,2318,34,28,30,2,35,37,36,31,15,11,14,12])). % 175.23/175.39 cnf(3291,plain, % 175.23/175.39 (E(f4(a1,x32911,a1),f4(a2,x32911,a2))), % 175.23/175.39 inference(scs_inference,[],[3249,3253,3144,3257,3202,3239,3179,3184,3255,3229,3232,3285,3180,3196,2031,840,65,2318,34,28,30,2,35,37,36,31,15,11,14,12,3])). % 175.23/175.39 cnf(3296,plain, % 175.23/175.39 (~P2(f8(a1,a7),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3279,1175])). % 175.23/175.39 cnf(3297,plain, % 175.23/175.39 (~P2(f8(a1,a7),a5)), % 175.23/175.39 inference(scs_inference,[],[3279,1218])). % 175.23/175.39 cnf(3298,plain, % 175.23/175.39 (~P2(f8(a1,a7),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[3279,1461])). % 175.23/175.39 cnf(3299,plain, % 175.23/175.39 (P2(f4(a2,x32991,x32992),f4(a1,x32991,x32992))), % 175.23/175.39 inference(scs_inference,[],[3228,28])). % 175.23/175.39 cnf(3301,plain, % 175.23/175.39 (~E(f8(x33011,a7),f8(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3208,3228,28,2])). % 175.23/175.39 cnf(3304,plain, % 175.23/175.39 (~E(f8(a5,a5),f8(x33041,a7))), % 175.23/175.39 inference(scs_inference,[],[3240,3208,3228,3267,28,2,37,36])). % 175.23/175.39 cnf(3306,plain, % 175.23/175.39 (~P2(f8(a7,a1),a1)), % 175.23/175.39 inference(scs_inference,[],[3014,3240,3208,3228,3267,62,28,2,37,36,31])). % 175.23/175.39 cnf(3309,plain, % 175.23/175.39 (P2(f4(a2,a1,x33091),f4(a1,a2,x33091))), % 175.23/175.39 inference(scs_inference,[],[3014,3240,3208,3228,3235,3267,62,28,2,37,36,31,15])). % 175.23/175.39 cnf(3312,plain, % 175.23/175.39 (~E(f8(a2,a1),f8(a6,x33121))), % 175.23/175.39 inference(scs_inference,[],[3014,3240,3208,3228,3235,3182,3267,845,62,28,2,37,36,31,15,11])). % 175.23/175.39 cnf(3313,plain, % 175.23/175.39 (P2(f4(x33131,a1,a1),f4(x33131,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3014,3240,3208,3227,3228,3235,3269,3182,3267,845,62,28,2,37,36,31,15,11,14])). % 175.23/175.39 cnf(3314,plain, % 175.23/175.39 (E(f4(x33141,a2,x33142),f4(x33141,a1,x33142))), % 175.23/175.39 inference(rename_variables,[],[3227])). % 175.23/175.39 cnf(3316,plain, % 175.23/175.39 (~P3(f4(a7,a2,a5),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3014,3240,3208,3227,3314,3228,3235,3269,3182,3267,3196,845,62,28,2,37,36,31,15,11,14,12])). % 175.23/175.39 cnf(3317,plain, % 175.23/175.39 (E(f4(x33171,a2,x33172),f4(x33171,a1,x33172))), % 175.23/175.39 inference(rename_variables,[],[3227])). % 175.23/175.39 cnf(3322,plain, % 175.23/175.39 (~P3(f4(a7,a2,a5),a5)), % 175.23/175.39 inference(scs_inference,[],[2262,3014,3240,3108,3208,3227,3314,3317,3228,3235,3269,3185,3182,3267,3196,845,62,28,2,37,36,31,15,11,14,12,3,13,45])). % 175.23/175.39 cnf(3327,plain, % 175.23/175.39 (P2(f3(a1,x33271),f3(a2,x33271))), % 175.23/175.39 inference(scs_inference,[],[3176,28])). % 175.23/175.39 cnf(3329,plain, % 175.23/175.39 (~E(f8(a7,x33291),f8(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3243,3176,28,2])). % 175.23/175.39 cnf(3337,plain, % 175.23/175.39 (E(f8(x33371,a2),f8(x33371,a1))), % 175.23/175.39 inference(rename_variables,[],[3229])). % 175.23/175.39 cnf(3338,plain, % 175.23/175.39 (~E(f8(a1,a1),f8(x33381,a5))), % 175.23/175.39 inference(scs_inference,[],[3296,3118,3243,3301,3176,3220,3255,3229,849,840,28,2,35,31,15,11])). % 175.23/175.39 cnf(3339,plain, % 175.23/175.39 (~P2(f8(a2,a7),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3296,3118,3243,3301,3176,3220,3255,3229,3232,849,840,28,2,35,31,15,11,14])). % 175.23/175.39 cnf(3343,plain, % 175.23/175.39 (~E(a1,f8(a7,x33431))), % 175.23/175.39 inference(scs_inference,[],[3296,3186,3261,3118,3243,3301,3176,3220,3255,3229,3337,3232,849,840,28,2,35,31,15,11,14,12,3])). % 175.23/175.39 cnf(3346,plain, % 175.23/175.39 (~E(a5,f8(a7,x33461))), % 175.23/175.39 inference(scs_inference,[],[3296,3186,3261,3113,3118,3243,3301,3176,3220,3174,3225,3255,3229,3337,3232,3267,849,840,28,2,35,31,15,11,14,12,3,13,37])). % 175.23/175.39 cnf(3348,plain, % 175.23/175.39 (~E(a5,f8(x33481,a7))), % 175.23/175.39 inference(scs_inference,[],[3296,3186,3261,3113,3118,3243,3301,3176,3220,3174,3225,3255,3229,3337,3232,3267,849,840,28,2,35,31,15,11,14,12,3,13,37,36])). % 175.23/175.39 cnf(3350,plain, % 175.23/175.39 (P3(f4(a7,a2,a5),a7)), % 175.23/175.39 inference(scs_inference,[],[3296,3186,3261,3113,3118,3243,3301,3176,3220,3322,3174,3225,3255,3229,3337,3232,3267,849,840,77,28,2,35,31,15,11,14,12,3,13,37,36,40])). % 175.23/175.39 cnf(3356,plain, % 175.23/175.39 (P2(f8(a1,x33561),f8(a2,x33561))), % 175.23/175.39 inference(scs_inference,[],[3188,28])). % 175.23/175.39 cnf(3358,plain, % 175.23/175.39 (~E(f8(a7,x33581),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3277,3188,28,2])). % 175.23/175.39 cnf(3362,plain, % 175.23/175.39 (~P2(f8(a7,a1),f8(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3230,3246,3277,3188,3306,124,28,2,31,15])). % 175.23/175.39 cnf(3363,plain, % 175.23/175.39 (~E(f8(a2,a1),f8(a5,x33631))), % 175.23/175.39 inference(scs_inference,[],[3230,3246,3277,3188,3222,3306,124,845,28,2,31,15,11])). % 175.23/175.39 cnf(3364,plain, % 175.23/175.39 (P2(f3(a1,a1),f3(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3230,3246,3277,3188,3224,3222,3327,3306,124,845,28,2,31,15,11,14])). % 175.23/175.39 cnf(3369,plain, % 175.23/175.39 (~E(f8(a7,a1),f8(a5,a7))), % 175.23/175.39 inference(scs_inference,[],[3193,3230,3195,3246,3277,3188,3224,3222,3327,3306,124,845,21,82,28,2,31,15,11,14,12,3])). % 175.23/175.39 cnf(3373,plain, % 175.23/175.39 (P3(f3(f8(a7,a1),f8(a5,a1)),f8(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[3358,2900])). % 175.23/175.39 cnf(3374,plain, % 175.23/175.39 (P2(f3(a2,x33741),f3(a1,x33741))), % 175.23/175.39 inference(scs_inference,[],[3226,28])). % 175.23/175.39 cnf(3376,plain, % 175.23/175.39 (~E(f8(x33761,a7),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3279,3226,28,2])). % 175.23/175.39 cnf(3380,plain, % 175.23/175.39 (~P2(f8(a1,a7),f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3298,3273,3279,3226,3232,2031,28,2,31,15])). % 175.23/175.39 cnf(3381,plain, % 175.23/175.39 (E(f8(a2,x33811),f8(a1,x33811))), % 175.23/175.39 inference(rename_variables,[],[3232])). % 175.23/175.39 cnf(3382,plain, % 175.23/175.39 (~E(a2,f8(x33821,a7))), % 175.23/175.39 inference(scs_inference,[],[3298,3273,3279,3226,2013,3232,2031,17,28,2,31,15,11])). % 175.23/175.39 cnf(3387,plain, % 175.23/175.39 (E(f4(a1,a1,a1),f4(a2,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3297,3298,3271,3273,3279,3226,3291,2013,3178,3232,3381,2031,17,19,28,2,31,15,11,14,12,3])). % 175.23/175.39 cnf(3396,plain, % 175.23/175.39 (~P3(f3(f8(a1,a7),f8(a5,a1)),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3376,2964])). % 175.23/175.39 cnf(3397,plain, % 175.23/175.39 (P2(f4(a1,a1,a1),f4(a2,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3387,28])). % 175.23/175.39 cnf(3399,plain, % 175.23/175.39 (~E(f8(x33991,a6),f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3286,3387,28,2])). % 175.23/175.39 cnf(3403,plain, % 175.23/175.39 (~E(f8(a1,a1),f8(a6,x34031))), % 175.23/175.39 inference(scs_inference,[],[3252,3286,3387,3182,79,840,28,2,31,11])). % 175.23/175.39 cnf(3405,plain, % 175.23/175.39 (P2(f4(a2,a1,a1),f4(a1,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3252,3286,3313,3387,3186,3184,3182,3306,79,840,28,2,31,11,15,14])). % 175.23/175.39 cnf(3416,plain, % 175.23/175.39 (~E(a7,f8(a7,a5))), % 175.23/175.39 inference(scs_inference,[],[3259,3185,28,2])). % 175.23/175.39 cnf(3424,plain, % 175.23/175.39 (E(f8(x34241,a2),f8(x34241,a1))), % 175.23/175.39 inference(rename_variables,[],[3229])). % 175.23/175.39 cnf(3427,plain, % 175.23/175.39 (E(f8(x34271,a2),f8(x34271,a1))), % 175.23/175.39 inference(rename_variables,[],[3229])). % 175.23/175.39 cnf(3429,plain, % 175.23/175.39 (E(f8(x34291,a2),f8(x34291,a1))), % 175.23/175.39 inference(rename_variables,[],[3229])). % 175.23/175.39 cnf(3431,plain, % 175.23/175.39 (~P3(f4(a7,a2,a5),f8(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3362,3339,3316,3259,3329,2390,3230,3246,3185,2021,3213,3255,3229,3424,3427,3429,849,17,28,2,35,31,15,11,14,12,3,13])). % 175.23/175.39 cnf(3433,plain, % 175.23/175.39 (~E(f8(a2,a2),f8(a7,x34331))), % 175.23/175.39 inference(scs_inference,[],[3362,3233,3339,3316,3259,3329,2390,3230,3246,3185,2021,3213,3255,3229,3424,3427,3429,849,17,105,28,2,35,31,15,11,14,12,3,13,37])). % 175.23/175.39 cnf(3439,plain, % 175.23/175.39 (P2(f3(x34391,a2),f3(x34391,a1))), % 175.23/175.39 inference(scs_inference,[],[3224,28])). % 175.23/175.39 cnf(3442,plain, % 175.23/175.39 (~P2(f8(a6,x34421),f8(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3304,3312,3224,849,28,2,31])). % 175.23/175.39 cnf(3445,plain, % 175.23/175.39 (P2(f3(a2,a2),f3(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3304,3312,3374,3224,849,28,2,31,15])). % 175.23/175.39 cnf(3448,plain, % 175.23/175.39 (~E(f8(a2,a1),f8(x34481,a6))), % 175.23/175.39 inference(scs_inference,[],[3304,3312,3374,3224,3180,849,845,28,2,31,15,11])). % 175.23/175.39 cnf(3451,plain, % 175.23/175.39 (~E(a1,f8(a6,x34511))), % 175.23/175.39 inference(scs_inference,[],[3304,3312,3374,3364,3176,3224,3180,3186,849,845,28,2,31,15,11,14,3])). % 175.23/175.39 cnf(3457,plain, % 175.23/175.39 (P2(f4(a1,x34571,a1),f4(a2,x34571,a2))), % 175.23/175.39 inference(scs_inference,[],[3291,28])). % 175.23/175.39 cnf(3459,plain, % 175.23/175.39 (~E(f8(x34591,a5),f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3338,3291,28,2])). % 175.23/175.39 cnf(3460,plain, % 175.23/175.39 (E(f3(a1,a1),f3(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3338,3445,3291,3364,28,2,31])). % 175.23/175.39 cnf(3462,plain, % 175.23/175.39 (E(f4(a1,a2,a1),f4(a2,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3338,3445,3291,3364,3227,28,2,31,3])). % 175.23/175.39 cnf(3465,plain, % 175.23/175.39 (~P2(f8(a2,a7),f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3380,3338,3445,3291,3364,3227,3232,28,2,31,3,14])). % 175.23/175.39 cnf(3467,plain, % 175.23/175.39 (~E(f8(a2,a1),f8(x34671,a5))), % 175.23/175.39 inference(scs_inference,[],[3380,3338,3445,3220,3291,3364,3227,3232,845,28,2,31,3,14,11])). % 175.23/175.39 cnf(3468,plain, % 175.23/175.39 (~P2(f8(a6,x34681),f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3380,3338,3442,3445,3220,3291,3364,3227,3188,3232,845,28,2,31,3,14,11,15])). % 175.23/175.39 cnf(3470,plain, % 175.23/175.39 (~P3(f8(a2,a7),f3(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[3380,3289,3338,3442,3445,3220,3291,3364,3227,3177,3188,3232,845,28,2,31,3,14,11,15,13])). % 175.23/175.39 cnf(3472,plain, % 175.23/175.39 (~P3(x34721,f4(a1,a1,a1))+P3(x34721,f4(a2,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3397,3380,3289,3338,3442,3445,3220,3291,3364,3227,3177,3188,3232,845,28,2,31,3,14,11,15,13,35])). % 175.23/175.39 cnf(3476,plain, % 175.23/175.39 (P2(f4(a1,a2,a1),f4(a2,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3462,28])). % 175.23/175.39 cnf(3481,plain, % 175.23/175.39 (~E(f8(a5,a2),f8(x34811,a7))), % 175.23/175.39 inference(scs_inference,[],[3470,3363,3462,3431,3350,3188,28,2,12,36])). % 175.23/175.39 cnf(3483,plain, % 175.23/175.39 (~P2(f8(a5,x34831),f8(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3470,3363,3462,3431,3350,3188,849,28,2,12,36,31])). % 175.23/175.39 cnf(3486,plain, % 175.23/175.39 (~E(f8(a5,a2),f8(a7,x34861))), % 175.23/175.39 inference(scs_inference,[],[3470,3363,3462,3431,3350,3188,849,28,2,12,36,31,37])). % 175.23/175.39 cnf(3488,plain, % 175.23/175.39 (~E(f8(a2,a2),f8(a5,x34881))), % 175.23/175.39 inference(scs_inference,[],[3470,3363,3462,3431,3350,3185,3188,849,28,2,12,36,31,37,3])). % 175.23/175.39 cnf(3490,plain, % 175.23/175.39 (P2(f3(a1,a2),f3(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3470,3363,3439,3462,3431,3350,3226,3185,3188,849,28,2,12,36,31,37,3,14])). % 175.23/175.39 cnf(3493,plain, % 175.23/175.39 (~E(a1,f8(a5,x34931))), % 175.23/175.39 inference(scs_inference,[],[16,3470,3363,3439,3462,3431,3350,3222,3226,3185,3188,849,28,2,12,36,31,37,3,14,11])). % 175.23/175.39 cnf(3494,plain, % 175.23/175.39 (P2(f4(a2,a2,a1),f4(a2,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[16,3470,3363,3299,3439,3462,3431,3350,3222,3226,3185,3188,849,28,2,12,36,31,37,3,14,11,15])). % 175.23/175.39 cnf(3498,plain, % 175.23/175.39 (P2(f4(a1,x34981,x34982),f4(a2,x34981,x34982))), % 175.23/175.39 inference(scs_inference,[],[3184,28])). % 175.23/175.39 cnf(3500,plain, % 175.23/175.39 (~E(f8(a6,x35001),f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3403,3184,28,2])). % 175.23/175.39 cnf(3501,plain, % 175.23/175.39 (~P3(f4(a7,a1,a5),f8(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3403,3431,3184,3178,28,2,12])). % 175.23/175.39 cnf(3503,plain, % 175.23/175.39 (E(f3(a2,a2),f3(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3403,3445,3364,3431,3184,3178,28,2,12,31])). % 175.23/175.39 cnf(3505,plain, % 175.23/175.39 (E(f4(a1,a1,a1),f4(a1,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3403,3445,3387,3364,3431,3184,3228,3178,28,2,12,31,3])). % 175.23/175.39 cnf(3507,plain, % 175.23/175.39 (~P2(f8(a7,a2),f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3403,3284,3445,3387,3364,3431,3184,3228,3178,3229,28,2,12,31,3,14])). % 175.23/175.39 cnf(3508,plain, % 175.23/175.39 (E(f8(x35081,a2),f8(x35081,a1))), % 175.23/175.39 inference(rename_variables,[],[3229])). % 175.23/175.39 cnf(3511,plain, % 175.23/175.39 (~P3(f3(a7,a5),f8(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3465,3403,3284,3216,3445,3387,3364,3431,3184,3228,3178,3188,3229,3508,28,2,12,31,3,14,15,13])). % 175.23/175.39 cnf(3513,plain, % 175.23/175.39 (~E(a1,f8(x35131,a6))), % 175.23/175.39 inference(scs_inference,[],[16,3465,3403,3284,3216,3445,3387,3180,3364,3431,3184,3228,3178,3188,3229,3508,28,2,12,31,3,14,15,13,11])). % 175.23/175.39 cnf(3514,plain, % 175.23/175.39 (P2(f3(x35141,a1),f3(x35141,a2))), % 175.23/175.39 inference(scs_inference,[],[3177,28])). % 175.23/175.39 cnf(3517,plain, % 175.23/175.39 (~P2(f8(x35171,a6),f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3399,3448,3177,79,28,2,31])). % 175.23/175.39 cnf(3520,plain, % 175.23/175.39 (~E(a1,f8(x35201,a5))), % 175.23/175.39 inference(scs_inference,[],[3399,3448,3467,3177,3186,79,28,2,31,3])). % 175.23/175.39 cnf(3521,plain, % 175.23/175.39 (P2(f4(a1,a2,a2),f4(a2,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3505,3399,3448,3467,3498,3177,3186,79,28,2,31,3,14])). % 175.23/175.39 cnf(3523,plain, % 175.23/175.39 (P2(f4(a2,a1,a1),f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3505,3399,3448,3467,3405,3498,3227,3177,3186,79,28,2,31,3,14,15])). % 175.23/175.39 cnf(3527,plain, % 175.23/175.39 (P2(f8(a2,x35271),f8(a1,x35271))), % 175.23/175.39 inference(scs_inference,[],[3232,28])). % 175.23/175.39 cnf(3529,plain, % 175.23/175.39 (~E(f8(a5,x35291),f8(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3488,3232,28,2])). % 175.23/175.39 cnf(3530,plain, % 175.23/175.39 (E(f4(a2,a1,a1),f4(a1,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3521,3488,3405,3232,28,2,31])). % 175.23/175.39 cnf(3532,plain, % 175.23/175.39 (E(f4(a1,a2,a1),f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3521,3488,3405,3462,3228,3232,28,2,31,3])). % 175.23/175.39 cnf(3534,plain, % 175.23/175.39 (~P2(f8(a7,a2),f8(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3521,3488,3209,3405,3462,3228,3232,3229,28,2,31,3,14])). % 175.23/175.39 cnf(3538,plain, % 175.23/175.39 (~P3(x35381,f4(a1,a2,a1))+P3(x35381,f4(a2,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3476,3507,3521,3488,3209,3405,3462,3228,3232,3188,3229,28,2,31,3,14,15,35])). % 175.23/175.39 cnf(3543,plain, % 175.23/175.39 (P2(f4(a1,a2,a1),f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3532,28])). % 175.23/175.39 cnf(3549,plain, % 175.23/175.39 (~E(f8(a7,a2),f8(a5,a7))), % 175.23/175.39 inference(scs_inference,[],[3532,3433,3481,3369,3185,124,28,2,31,3])). % 175.23/175.39 cnf(3551,plain, % 175.23/175.39 (P2(f4(a1,a1,a2),f4(a2,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3532,3433,3481,3369,3457,3185,124,28,2,31,3,14])). % 175.23/175.39 cnf(3553,plain, % 175.23/175.39 (P2(f3(a2,a1),f3(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3532,3433,3481,3369,3514,3457,3226,3185,124,28,2,31,3,14,15])). % 175.23/175.39 cnf(3559,plain, % 175.23/175.39 (~E(f8(a7,x35591),f8(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3486,3229,28,2])). % 175.23/175.39 cnf(3560,plain, % 175.23/175.39 (E(f3(a1,a2),f3(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3553,3486,3490,3229,28,2,31])). % 175.23/175.39 cnf(3562,plain, % 175.23/175.39 (E(f4(a2,a1,a1),f4(a2,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3530,3553,3486,3490,3184,3229,28,2,31,3])). % 175.23/175.39 cnf(3564,plain, % 175.23/175.39 (~P2(f8(a2,a7),f8(a5,a5))), % 175.23/175.39 inference(scs_inference,[],[3530,3553,3486,3490,2907,3184,3232,3229,28,2,31,3,14])). % 175.23/175.39 cnf(3566,plain, % 175.23/175.39 (~P2(f8(a7,a2),f8(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3534,3530,3553,3486,3490,2907,3184,3232,3229,28,2,31,3,14,15])). % 175.23/175.39 cnf(3568,plain, % 175.23/175.39 (~E(a1,a6)), % 175.23/175.39 inference(scs_inference,[],[16,3534,3530,3553,3486,3490,2907,3184,23,3232,3229,28,2,31,3,14,15,11])). % 175.23/175.39 cnf(3569,plain, % 175.23/175.39 (P2(f4(x35691,x35692,a2),f4(x35691,x35692,a1))), % 175.23/175.39 inference(scs_inference,[],[3225,28])). % 175.23/175.39 cnf(3571,plain, % 175.23/175.39 (~E(a6,a1)), % 175.23/175.39 inference(scs_inference,[],[3568,3225,28,2])). % 175.23/175.39 cnf(3572,plain, % 175.23/175.39 (~P2(a6,a1)), % 175.23/175.39 inference(scs_inference,[],[3568,62,3225,28,2,31])). % 175.23/175.39 cnf(3575,plain, % 175.23/175.39 (~E(a2,a6)), % 175.23/175.39 inference(scs_inference,[],[3568,62,3225,336,28,2,31,3])). % 175.23/175.39 cnf(3576,plain, % 175.23/175.39 (P2(f4(a2,a2,a2),f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3568,3562,3523,62,3225,336,28,2,31,3,14])). % 175.23/175.39 cnf(3577,plain, % 175.23/175.39 (P3(f3(a6,a1),a6)), % 175.23/175.39 inference(scs_inference,[],[3568,3562,3523,62,3225,336,28,2,31,3,14,34])). % 175.23/175.39 cnf(3579,plain, % 175.23/175.39 (~P3(a6,f3(a6,a1))), % 175.23/175.39 inference(scs_inference,[],[3568,3562,3523,62,3225,336,28,2,31,3,14,34,30])). % 175.23/175.39 cnf(3584,plain, % 175.23/175.39 (~E(f8(a1,a2),f8(x35841,a6))), % 175.23/175.39 inference(scs_inference,[],[3568,3562,3523,3439,62,3225,2023,336,28,2,31,3,14,34,30,35,36])). % 175.23/175.39 cnf(3585,plain, % 175.23/175.39 (~P3(x35851,f8(a1,a2))), % 175.23/175.39 inference(rename_variables,[],[2023])). % 175.23/175.39 cnf(3587,plain, % 175.23/175.39 (~P3(f8(a6,a1),f3(a6,a1))), % 175.23/175.39 inference(scs_inference,[],[3568,3562,3523,3439,62,3225,2023,336,19,28,2,31,3,14,34,30,35,36,12])). % 175.23/175.39 cnf(3589,plain, % 175.23/175.39 (~E(f8(a1,a2),f8(a6,x35891))), % 175.23/175.39 inference(scs_inference,[],[3568,3562,3523,3439,62,3225,2023,3585,336,19,28,2,31,3,14,34,30,35,36,12,37])). % 175.23/175.39 cnf(3592,plain, % 175.23/175.39 (~P3(f8(a6,a1),f3(a6,a2))), % 175.23/175.39 inference(scs_inference,[],[3568,3562,3523,3439,3224,62,3225,2023,3585,336,19,28,2,31,3,14,34,30,35,36,12,37,13])). % 175.23/175.39 cnf(3594,plain, % 175.23/175.39 (P2(f8(x35941,x35942),f8(x35942,x35941))), % 175.23/175.39 inference(scs_inference,[],[22,28])). % 175.23/175.39 cnf(3596,plain, % 175.23/175.39 (~E(a6,a2)), % 175.23/175.39 inference(scs_inference,[],[3575,22,28,2])). % 175.23/175.39 cnf(3597,plain, % 175.23/175.39 (~P3(f4(a7,a1,a5),f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3575,3501,22,28,2,35])). % 175.23/175.39 cnf(3599,plain, % 175.23/175.39 (~E(f8(a2,a2),f8(x35991,a6))), % 175.23/175.39 inference(scs_inference,[],[3575,3577,3501,105,22,28,2,35,36])). % 175.23/175.39 cnf(3600,plain, % 175.23/175.39 (~P3(x36001,f8(a2,a2))), % 175.23/175.39 inference(rename_variables,[],[105])). % 175.23/175.39 cnf(3602,plain, % 175.23/175.39 (~P3(f8(a6,a2),f3(a6,a2))), % 175.23/175.39 inference(scs_inference,[],[3575,3592,3577,3501,3229,105,22,28,2,35,36,12])). % 175.23/175.39 cnf(3604,plain, % 175.23/175.39 (E(f4(a1,a1,a2),f4(a2,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3575,3576,3551,3592,3577,3501,3229,105,22,28,2,35,36,12,31])). % 175.23/175.39 cnf(3606,plain, % 175.23/175.39 (~E(f8(a2,a2),f8(a6,x36061))), % 175.23/175.39 inference(scs_inference,[],[3575,3576,3551,3592,3577,3501,3229,105,3600,22,28,2,35,36,12,31,37])). % 175.23/175.39 cnf(3609,plain, % 175.23/175.39 (E(f4(a2,a1,a1),f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3575,3576,3551,3592,3577,3501,3530,3227,3229,105,3600,22,28,2,35,36,12,31,37,3])). % 175.23/175.39 cnf(3611,plain, % 175.23/175.39 (~P2(f8(a6,a1),a1)), % 175.23/175.39 inference(scs_inference,[],[3572,3575,3576,3551,3592,3577,3501,3530,3227,3229,105,3600,19,22,28,2,35,36,12,31,37,3,14])). % 175.23/175.39 cnf(3614,plain, % 175.23/175.39 (~P3(x36141,f3(a1,a2))+P3(x36141,f3(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3572,3575,3576,3551,3592,3560,3577,3501,3530,3230,3227,3229,105,3600,19,22,28,2,35,36,12,31,37,3,14,15,13])). % 175.23/175.39 cnf(3623,plain, % 175.23/175.39 (~E(f8(x36231,a6),f8(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3584,82,28,2])). % 175.23/175.39 cnf(3627,plain, % 175.23/175.39 (~E(f8(a2,a5),f8(x36271,a7))), % 175.23/175.39 inference(scs_inference,[],[3597,3584,3602,3514,2318,82,28,2,35,36])). % 175.23/175.39 cnf(3629,plain, % 175.23/175.39 (~P3(f4(a7,a2,a5),f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3597,3584,3602,3514,3227,2318,82,28,2,35,36,12])). % 175.23/175.39 cnf(3631,plain, % 175.23/175.39 (~P2(a6,a2)), % 175.23/175.39 inference(scs_inference,[],[3596,3597,3584,3602,3514,102,3227,2318,82,28,2,35,36,12,31])). % 175.23/175.39 cnf(3634,plain, % 175.23/175.39 (~E(f8(a2,a5),f8(a7,x36341))), % 175.23/175.39 inference(scs_inference,[],[3596,3597,3584,3602,3514,102,3227,2318,82,28,2,35,36,12,31,37])). % 175.23/175.39 cnf(3636,plain, % 175.23/175.39 (~E(f8(a6,a1),a1)), % 175.23/175.39 inference(scs_inference,[],[3571,3596,3597,3584,3602,3514,102,3227,2318,82,28,2,35,36,12,31,37,3])). % 175.23/175.39 cnf(3638,plain, % 175.23/175.39 (P2(f4(a1,a1,a2),f4(a1,a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3571,3596,3609,3597,3584,3602,3309,3514,102,3227,2318,82,28,2,35,36,12,31,37,3,14])). % 175.23/175.39 cnf(3641,plain, % 175.23/175.39 (E(f8(a1,x36411),f8(a2,x36411))), % 175.23/175.39 inference(rename_variables,[],[3188])). % 175.23/175.39 cnf(3644,plain, % 175.23/175.39 (~P2(f8(a7,a7),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[3571,3596,3609,3597,3483,3584,3602,3309,3514,102,3227,3188,3641,2318,82,28,2,35,36,12,31,37,3,14,15,13,2924])). % 175.23/175.39 cnf(3645,plain, % 175.23/175.39 (P3(f3(a6,a2),a6)), % 175.23/175.39 inference(scs_inference,[],[3571,3596,3609,3597,3483,3584,3602,3309,3514,102,3227,3188,3641,2318,82,28,2,35,36,12,31,37,3,14,15,13,2924,34])). % 175.23/175.39 cnf(3647,plain, % 175.23/175.39 (~E(f8(a6,x36471),f8(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3589,2])). % 175.23/175.39 cnf(3648,plain, % 175.23/175.39 (~P3(f4(a7,a2,a5),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[3629,3589,3356,2,35])). % 175.23/175.39 cnf(3651,plain, % 175.23/175.39 (~E(a2,f8(x36511,a6))), % 175.23/175.39 inference(scs_inference,[],[3629,3589,3356,3645,77,2,35,36])). % 175.23/175.39 cnf(3652,plain, % 175.23/175.39 (~P3(x36521,a2)), % 175.23/175.39 inference(rename_variables,[],[77])). % 175.23/175.39 cnf(3654,plain, % 175.23/175.39 (~P3(f8(a1,a6),f3(a6,a1))), % 175.23/175.39 inference(scs_inference,[],[3629,3587,3589,3356,3645,77,22,2,35,36,12])). % 175.23/175.39 cnf(3656,plain, % 175.23/175.39 (E(f4(a1,a1,a2),f4(a1,a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3629,3543,3638,3587,3589,3356,3645,77,22,2,35,36,12,31])). % 175.23/175.39 cnf(3658,plain, % 175.23/175.39 (~E(a2,f8(a6,x36581))), % 175.23/175.39 inference(scs_inference,[],[3629,3543,3638,3587,3589,3356,3645,77,3652,22,2,35,36,12,31,37])). % 175.23/175.39 cnf(3659,plain, % 175.23/175.39 (~P3(x36591,a2)), % 175.23/175.39 inference(rename_variables,[],[77])). % 175.23/175.39 cnf(3661,plain, % 175.23/175.39 (~P2(f8(a6,a1),f8(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3629,3543,3638,3587,3589,3356,3645,3611,3230,77,3652,22,2,35,36,12,31,37,15])). % 175.23/175.39 cnf(3662,plain, % 175.23/175.39 (~P2(f8(a6,a1),a2)), % 175.23/175.39 inference(scs_inference,[],[3631,3629,3543,3638,3587,3589,3356,3645,3611,3230,19,77,3652,22,2,35,36,12,31,37,15,14])). % 175.23/175.39 cnf(3664,plain, % 175.23/175.39 (~E(a6,f8(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3631,3629,3543,3638,3587,3589,3356,3645,3611,3230,19,77,3652,3659,22,2,35,36,12,31,37,15,14,38])). % 175.23/175.39 cnf(3667,plain, % 175.23/175.39 (~E(f8(a1,a5),f8(x36671,a7))), % 175.23/175.39 inference(scs_inference,[],[3631,3629,3543,3638,3587,3589,3627,3356,3645,3611,3230,3232,19,77,3652,3659,22,2,35,36,12,31,37,15,14,38,3])). % 175.23/175.39 cnf(3669,plain, % 175.23/175.39 (~E(a1,a5)), % 175.23/175.39 inference(scs_inference,[],[16,3631,3629,3543,3638,3587,3589,3627,3356,3645,3611,3230,2513,3232,19,77,3652,3659,22,2,35,36,12,31,37,15,14,38,3,11])). % 175.23/175.39 cnf(3670,plain, % 175.23/175.39 (~P3(x36701,f4(a1,a1,a2))+P3(x36701,f4(a2,a2,a2))), % 175.23/175.39 inference(scs_inference,[],[16,3631,3629,3543,3638,3604,3587,3589,3627,3356,3645,3611,3230,2513,3232,19,77,3652,3659,22,2,35,36,12,31,37,15,14,38,3,11,13])). % 175.23/175.39 cnf(3676,plain, % 175.23/175.39 (~P2(f8(a1,a7),f8(f8(a1,a5),f8(a1,a5)))), % 175.23/175.39 inference(scs_inference,[],[3667,1760])). % 175.23/175.39 cnf(3677,plain, % 175.23/175.39 (~P2(f8(a1,a7),f8(f8(a1,a5),a1))), % 175.23/175.39 inference(scs_inference,[],[3667,1963])). % 175.23/175.39 cnf(3678,plain, % 175.23/175.39 (~E(f8(x36781,a6),f8(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3599,2])). % 175.23/175.39 cnf(3681,plain, % 175.23/175.39 (~P2(f8(a7,a7),f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3644,3661,3599,3232,3229,2,14,15])). % 175.23/175.39 cnf(3682,plain, % 175.23/175.39 (E(f8(a2,x36821),f8(a1,x36821))), % 175.23/175.39 inference(rename_variables,[],[3232])). % 175.23/175.39 cnf(3683,plain, % 175.23/175.39 (~P3(f8(a1,a6),f3(a6,a2))), % 175.23/175.39 inference(scs_inference,[],[3644,3661,3654,3599,3224,3232,3229,2,14,15,13])). % 175.23/175.39 cnf(3685,plain, % 175.23/175.39 (~P3(f3(a7,a5),f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3594,3644,3661,3654,3599,3511,3224,3232,3229,2,14,15,13,35])). % 175.23/175.39 cnf(3690,plain, % 175.23/175.39 (~P2(a5,a1)), % 175.23/175.39 inference(scs_inference,[],[3669,3594,3644,3661,3654,3599,3511,3224,62,3232,3682,3229,2,14,15,13,35,12,31])). % 175.23/175.39 cnf(3693,plain, % 175.23/175.39 (~E(f8(a1,a5),f8(a7,x36931))), % 175.23/175.39 inference(scs_inference,[],[3669,3594,3644,3648,3661,3654,3599,3511,3350,3224,62,3232,3682,3229,2,14,15,13,35,12,31,37])). % 175.23/175.39 cnf(3695,plain, % 175.23/175.39 (E(f4(a2,a1,a1),f4(a1,a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3669,3594,3644,3648,3656,3661,3654,3599,3511,3609,3350,3224,62,3232,3682,3229,2,14,15,13,35,12,31,37,3])). % 175.23/175.39 cnf(3696,plain, % 175.23/175.39 (P3(f3(a5,a1),a5)), % 175.23/175.39 inference(scs_inference,[],[3669,3594,3644,3648,3656,3661,3654,3599,3511,3609,3350,3224,62,3232,3682,3229,2,14,15,13,35,12,31,37,3,34])). % 175.23/175.39 cnf(3698,plain, % 175.23/175.39 (~P3(a5,f3(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3669,3594,3644,3648,3656,3661,3654,3599,3511,3609,3350,3224,62,3232,3682,3229,2,14,15,13,35,12,31,37,3,34,30])). % 175.23/175.39 cnf(3700,plain, % 175.23/175.39 (~E(f8(a1,a2),f8(x37001,a5))), % 175.23/175.39 inference(scs_inference,[],[3669,3594,3644,3648,3656,3661,3654,3599,3511,3609,3350,3224,62,3232,3682,2023,3229,2,14,15,13,35,12,31,37,3,34,30,36])). % 175.23/175.39 cnf(3703,plain, % 175.23/175.39 (~E(f8(a6,x37031),f8(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3606,2])). % 175.23/175.39 cnf(3704,plain, % 175.23/175.39 (~P2(f8(a5,a1),a1)), % 175.23/175.39 inference(scs_inference,[],[3690,3606,19,2,14])). % 175.23/175.39 cnf(3706,plain, % 175.23/175.39 (P2(f4(a2,a1,a2),f4(a1,a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3690,3695,3606,3569,19,2,14,15])). % 175.23/175.39 cnf(3712,plain, % 175.23/175.39 (P3(f3(a5,a1),a7)), % 175.23/175.39 inference(scs_inference,[],[3690,3685,3695,3606,3569,3696,1133,3188,19,48,2,14,15,13,35,46])). % 175.23/175.39 cnf(3715,plain, % 175.23/175.39 (~E(f8(a2,a2),f8(x37151,a5))), % 175.23/175.39 inference(scs_inference,[],[3690,3685,3695,3606,3569,3696,1133,3188,105,19,48,2,14,15,13,35,46,36])). % 175.23/175.39 cnf(3720,plain, % 175.23/175.39 (E(f4(a2,a1,a2),f4(a1,a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3690,3685,3695,3683,3606,3569,3696,3476,1133,3188,3232,105,19,48,2,14,15,13,35,46,36,12,31])). % 175.23/175.39 cnf(3722,plain, % 175.23/175.39 (~E(f8(a1,a2),f8(a5,x37221))), % 175.23/175.39 inference(scs_inference,[],[3690,3685,3695,3683,3606,3569,3696,3476,1133,3188,3232,2023,105,19,48,2,14,15,13,35,46,36,12,31,37])). % 175.23/175.39 cnf(3727,plain, % 175.23/175.39 (~P3(f8(a1,a7),f3(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3690,3685,3695,3683,3606,3569,3636,3696,3476,3185,1133,3188,3232,2023,105,19,48,2,14,15,13,35,46,36,12,31,37,3,30])). % 175.23/175.39 cnf(3732,plain, % 175.23/175.39 (P2(f4(a2,a2,a2),f4(a1,a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3706,3634,3712,3178,2,30,14])). % 175.23/175.39 cnf(3734,plain, % 175.23/175.39 (~P3(f8(a1,a7),f3(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3706,3727,3634,3712,3178,3224,2,30,14,13])). % 175.23/175.39 cnf(3737,plain, % 175.23/175.39 (E(f8(a2,x37371),f8(a1,x37371))), % 175.23/175.39 inference(rename_variables,[],[3232])). % 175.23/175.39 cnf(3738,plain, % 175.23/175.39 (~P3(a7,f4(a7,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3706,3727,3517,3634,3712,3569,3144,3178,3224,3232,2,30,14,13,15,35])). % 175.23/175.39 cnf(3743,plain, % 175.23/175.39 (~P2(f8(x37431,a5),f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3706,3727,3459,3517,3634,3712,3569,3144,3178,3224,79,3232,3737,2,30,14,13,15,35,12,31])). % 175.23/175.39 cnf(3746,plain, % 175.23/175.39 (E(f4(a2,a2,a2),f4(a1,a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3706,3720,3727,3459,3517,3634,3712,3569,3144,3178,3224,79,3227,3232,3737,2,30,14,13,15,35,12,31,3])). % 175.23/175.39 cnf(3749,plain, % 175.23/175.39 (~P2(f8(a7,a1),f8(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3566,3664,3185,2,14])). % 175.23/175.39 cnf(3751,plain, % 175.23/175.39 (P2(f4(a2,a2,a1),f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3566,3664,3494,3228,3185,2,14,15])). % 175.23/175.39 cnf(3755,plain, % 175.23/175.39 (E(f4(a2,a2,a2),f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3566,3664,3494,3551,3576,3696,3228,3185,54,2,14,15,35,31])). % 175.23/175.39 cnf(3759,plain, % 175.23/175.39 (~E(f8(a7,a1),f8(a7,a5))), % 175.23/175.39 inference(scs_inference,[],[3566,3664,3734,3494,3416,3551,3576,3696,3228,3185,54,3232,82,2,14,15,35,31,12,3])). % 175.23/175.39 cnf(3761,plain, % 175.23/175.39 (~P3(f8(a7,a7),f3(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3566,3664,3734,3494,3416,3551,3576,3696,3228,3185,54,3232,82,2,14,15,35,31,12,3,30])). % 175.23/175.39 cnf(3763,plain, % 175.23/175.39 (~P3(x37631,f4(a2,a2,a2))+P3(x37631,f4(a1,a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3566,3746,3664,3734,3494,3416,3551,3576,3696,3228,3185,54,3232,82,2,14,15,35,31,12,3,30,13])). % 175.23/175.39 cnf(3764,plain, % 175.23/175.39 (~E(a2,f8(x37641,a5))), % 175.23/175.39 inference(scs_inference,[],[17,3566,3746,3664,3734,3494,3416,3551,3576,3220,3696,3228,3185,54,3232,82,2,14,15,35,31,12,3,30,13,11])). % 175.23/175.39 cnf(3765,plain, % 175.23/175.39 (~P3(x37651,f4(a2,a2,a2))+P3(x37651,f4(a2,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[17,3566,3746,3664,3734,3494,3416,3551,3576,3220,3696,3228,3185,54,3232,82,2,14,15,35,31,12,3,30,13,11,3538])). % 175.23/175.39 cnf(3781,plain, % 175.23/175.39 (~P3(f8(a5,a1),f3(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[3749,3761,3698,3759,3468,3529,124,3224,3229,19,82,2,14,13,15,31,12])). % 175.23/175.39 cnf(3783,plain, % 175.23/175.39 (~E(a2,f8(a5,x37831))), % 175.23/175.39 inference(scs_inference,[],[17,3749,3761,3698,3759,3468,3529,3222,124,3224,3229,19,82,2,14,13,15,31,12,11])). % 175.23/175.39 cnf(3784,plain, % 175.23/175.39 (E(f4(a2,a2,a1),f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[17,3749,3755,3761,3698,3759,3468,3529,3222,3179,124,3224,3229,19,82,2,14,13,15,31,12,11,3])). % 175.23/175.39 cnf(3786,plain, % 175.23/175.39 (~E(f8(x37861,a7),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[3667,2])). % 175.23/175.39 cnf(3788,plain, % 175.23/175.39 (E(f8(x37881,a2),f8(x37881,a1))), % 175.23/175.39 inference(rename_variables,[],[3229])). % 175.23/175.39 cnf(3793,plain, % 175.23/175.39 (E(f3(a2,a1),f3(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3751,3667,3704,3490,3553,3696,3178,111,3229,2,14,35,15,31])). % 175.23/175.39 cnf(3797,plain, % 175.23/175.39 (~E(a2,a5)), % 175.23/175.39 inference(scs_inference,[],[17,3781,3751,3667,3704,3490,3553,3696,2513,3178,111,3229,3788,2,14,35,15,31,12,11])). % 175.23/175.39 cnf(3798,plain, % 175.23/175.39 (~E(f8(a5,a1),a1)), % 175.23/175.39 inference(scs_inference,[],[17,3781,3751,3667,3704,2512,3490,3553,3696,2513,3178,111,3229,3788,82,2,14,35,15,31,12,11,3])). % 175.23/175.39 cnf(3800,plain, % 175.23/175.39 (~P3(f8(a7,a1),f3(a5,a1))), % 175.23/175.39 inference(scs_inference,[],[17,3781,3751,3667,3704,2512,3490,3553,3696,2513,3178,111,3229,3788,82,2,14,35,15,31,12,11,3,30])). % 175.23/175.39 cnf(3802,plain, % 175.23/175.39 (~P3(x38021,f4(a2,a2,a1))+P3(x38021,f4(a1,a1,a2))), % 175.23/175.39 inference(scs_inference,[],[17,3781,3784,3751,3667,3704,2512,3490,3553,3696,2513,3178,111,3229,3788,82,2,14,35,15,31,12,11,3,30,13])). % 175.23/175.39 cnf(3807,plain, % 175.23/175.39 (P3(f3(f8(a7,a7),f8(a1,a5)),f8(a7,a7))), % 175.23/175.39 inference(scs_inference,[],[3786,2938])). % 175.23/175.39 cnf(3809,plain, % 175.23/175.39 (~P3(f3(f8(a1,a7),f8(a1,a5)),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[3786,2978])). % 175.23/175.39 cnf(3812,plain, % 175.23/175.39 (~E(a5,a2)), % 175.23/175.39 inference(scs_inference,[],[3797,2])). % 175.23/175.39 cnf(3813,plain, % 175.23/175.39 (~P2(a7,f8(a2,a5))), % 175.23/175.39 inference(scs_inference,[],[3797,3681,47,2,14])). % 175.23/175.39 cnf(3817,plain, % 175.23/175.39 (~P3(f8(a7,a1),f3(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3797,3681,3800,3743,3224,3232,47,2,14,15,13])). % 175.23/175.39 cnf(3819,plain, % 175.23/175.39 (~P2(a5,a2)), % 175.23/175.39 inference(scs_inference,[],[3797,3681,3800,3743,102,3224,3232,47,2,14,15,13,31])). % 175.23/175.39 cnf(3824,plain, % 175.23/175.39 (~E(f8(a2,a1),a5)), % 175.23/175.39 inference(scs_inference,[],[3797,3681,3800,3743,102,3224,3232,3229,82,47,2,14,15,13,31,12,3])). % 175.23/175.39 cnf(3826,plain, % 175.23/175.39 (P3(f3(a5,a2),a5)), % 175.23/175.39 inference(scs_inference,[],[3797,3681,3800,3743,102,3224,3232,3229,82,47,2,14,15,13,31,12,3,34])). % 175.23/175.39 cnf(3828,plain, % 175.23/175.39 (~P3(a5,f3(a5,a2))), % 175.23/175.39 inference(scs_inference,[],[3797,3681,3800,3743,102,3224,3232,3229,82,47,2,14,15,13,31,12,3,34,30])). % 175.23/175.39 cnf(3830,plain, % 175.23/175.39 (~P2(a5,f8(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3824,852])). % 175.23/175.39 cnf(3831,plain, % 175.23/175.39 (P3(f3(a5,f8(a2,a1)),a5)), % 175.23/175.39 inference(scs_inference,[],[3824,2030])). % 175.23/175.39 cnf(3832,plain, % 175.23/175.39 (~E(f8(a7,x38321),f8(a1,a5))), % 175.23/175.39 inference(scs_inference,[],[3693,2])). % 175.23/175.39 cnf(3833,plain, % 175.23/175.39 (~P2(f8(a5,a1),a2)), % 175.23/175.39 inference(scs_inference,[],[3819,3693,19,2,14])). % 175.23/175.39 cnf(3835,plain, % 175.23/175.39 (P2(f4(a2,a2,a2),f4(a1,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3819,3732,3693,3227,19,2,14,15])). % 175.23/175.39 cnf(3837,plain, % 175.23/175.39 (E(f4(a2,a2,a2),f4(a1,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3819,3732,3693,3397,3227,19,2,14,15,31])). % 175.23/175.39 cnf(3841,plain, % 175.23/175.39 (~E(f8(a5,a1),a2)), % 175.23/175.39 inference(scs_inference,[],[3812,3819,3732,3817,3693,3397,3227,3229,19,82,2,14,15,31,12,3])). % 175.23/175.39 cnf(3843,plain, % 175.23/175.39 (~P3(x38431,f3(a2,a1))+P3(x38431,f3(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3812,3819,3732,3817,3793,3693,3397,3227,3229,19,82,2,14,15,31,12,3,13])). % 175.23/175.39 cnf(3846,plain, % 175.23/175.39 (~P3(f3(a1,a2),f3(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3812,3819,3732,3817,3793,3693,3397,3227,3229,19,82,2,14,15,31,12,3,13,30])). % 175.23/175.39 cnf(3847,plain, % 175.23/175.39 (P3(f3(f8(a7,a1),f8(a1,a5)),f8(a7,a1))), % 175.23/175.39 inference(scs_inference,[],[3832,2973])). % 175.23/175.39 cnf(3848,plain, % 175.23/175.39 (~E(f8(x38481,a5),f8(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3700,2])). % 175.23/175.39 cnf(3849,plain, % 175.23/175.39 (~P3(f3(a1,a2),f3(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3846,3700,3327,2,35])). % 175.23/175.39 cnf(3852,plain, % 175.23/175.39 (P2(f4(a1,a2,a2),f4(a1,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3846,3835,3700,3327,3228,2,35,14])). % 175.23/175.39 cnf(3855,plain, % 175.23/175.39 (~P2(a5,f8(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3846,3835,3830,3700,3327,3560,3228,3188,2,35,14,13,15])). % 175.23/175.39 cnf(3861,plain, % 175.23/175.39 (E(f4(a2,a2,a1),f4(a1,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3846,3835,3837,3830,3623,3700,3327,3793,3560,3179,2031,3228,3188,2,35,14,13,15,31,12,3])). % 175.23/175.39 cnf(3863,plain, % 175.23/175.39 (~P3(f3(a2,a1),f3(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3846,3835,3837,3830,3623,3700,3327,3793,3560,3179,2031,3228,3188,2,35,14,13,15,31,12,3,3614])). % 175.23/175.39 cnf(3864,plain, % 175.23/175.39 (P2(f4(a2,a2,a1),f4(a1,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3846,3835,3837,3830,3623,3700,3327,3793,3560,3179,2031,3228,3188,2,35,14,13,15,31,12,3,3614,28])). % 175.23/175.39 cnf(3866,plain, % 175.23/175.39 (~E(f8(x38661,a5),f8(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3715,2])). % 175.23/175.39 cnf(3867,plain, % 175.23/175.39 (~P3(f3(a2,a1),f3(a2,a2))), % 175.23/175.39 inference(scs_inference,[],[3863,3715,3374,2,35])). % 175.23/175.39 cnf(3873,plain, % 175.23/175.39 (E(f4(a1,a2,a2),f4(a1,a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3863,3852,3849,3715,3833,3503,3374,3313,3229,2,35,14,13,31])). % 175.23/175.39 cnf(3880,plain, % 175.23/175.39 (~P3(f3(a1,a1),f3(a2,a1))), % 175.23/175.39 inference(scs_inference,[],[3863,3852,3849,3715,3798,3833,3503,3374,3313,3176,3185,3229,2,35,14,13,31,12,3,3843])). % 175.23/175.39 cnf(3887,plain, % 175.23/175.39 (~E(f8(a5,x38871),f8(a1,a2))), % 175.23/175.39 inference(scs_inference,[],[3722,2])). % 175.23/175.39 cnf(3888,plain, % 175.23/175.39 (~P3(f3(a2,a1),f3(a1,a1))), % 175.23/175.39 inference(scs_inference,[],[3867,3722,3460,2,13])). % 175.23/175.39 cnf(3892,plain, % 175.23/175.39 (~P3(f3(a2,a2),f3(a2,a1))), % 175.23/175.40 inference(scs_inference,[],[3880,3867,3678,3722,3503,3460,124,2,13,31,12])). % 175.23/175.40 cnf(3893,plain, % 175.23/175.40 (E(f4(a2,a2,a1),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[3880,3867,3678,3722,3861,3503,3505,3460,124,2,13,31,12,3])). % 175.23/175.40 cnf(3894,plain, % 175.23/175.40 (~E(f8(a5,a7),f8(a7,a2))), % 175.23/175.40 inference(scs_inference,[],[3549,2])). % 175.23/175.40 cnf(3898,plain, % 175.23/175.40 (E(f4(a1,a2,a2),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[3892,3549,3841,3521,3405,3560,3185,2,3,13,31])). % 175.23/175.40 cnf(3900,plain, % 175.23/175.40 (~P3(f3(a1,a1),f3(a1,a1))), % 175.23/175.40 inference(scs_inference,[],[3888,3892,3549,3841,3521,3405,3560,3176,3185,2,3,13,31,12])). % 175.23/175.40 cnf(3902,plain, % 175.23/175.40 (~P3(x39021,f4(a2,a2,a1))+P3(x39021,f4(a1,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[3888,3864,3892,3549,3841,3521,3405,3560,3176,3185,2,3,13,31,12,35])). % 175.23/175.40 cnf(3920,plain, % 175.23/175.40 (E(f4(a1,a2,a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[3898,3824,3179,2,3])). % 175.23/175.40 cnf(3922,plain, % 175.23/175.40 (~P2(f8(a6,a2),a2)), % 175.23/175.40 inference(scs_inference,[],[3898,3824,3662,3179,3229,2,3,14])). % 175.23/175.40 cnf(3929,plain, % 175.23/175.40 (~P3(f8(a5,a1),f3(a5,a2))), % 175.23/175.40 inference(scs_inference,[],[19,3898,3703,3813,3824,3662,3828,3179,124,3188,3229,2,3,14,15,31,12])). % 175.23/175.40 cnf(3931,plain, % 175.23/175.40 (P2(f4(a1,a2,a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3898,3703,3813,3824,3662,3828,3179,124,3188,3229,2,3,14,15,31,12,28])). % 175.23/175.40 cnf(3935,plain, % 175.23/175.40 (~E(f8(a7,a5),f8(a7,a2))), % 175.23/175.40 inference(scs_inference,[],[3894,3346,22,2,3])). % 175.23/175.40 cnf(3937,plain, % 175.23/175.40 (~P2(f8(a7,a1),a2)), % 175.23/175.40 inference(scs_inference,[],[19,3894,3346,583,22,2,3,14])). % 175.23/175.40 cnf(3938,plain, % 175.23/175.40 (E(f8(x39381,a1),x39381)), % 175.23/175.40 inference(rename_variables,[],[19])). % 175.23/175.40 cnf(3943,plain, % 175.23/175.40 (~P3(f3(a2,a2),f3(a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3938,3900,3894,3346,3631,583,3503,89,2413,22,2,3,14,15,31,12])). % 175.23/175.40 cnf(3944,plain, % 175.23/175.40 (~E(f8(a7,a2),f8(a7,a5))), % 175.23/175.40 inference(scs_inference,[],[3935,2])). % 175.23/175.40 cnf(3945,plain, % 175.23/175.40 (E(f4(a2,a2,a2),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[3920,3935,3746,2,3])). % 175.23/175.40 cnf(3946,plain, % 175.23/175.40 (P2(f4(a1,a1,a2),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[3931,3920,3935,3746,3532,2,3,14])). % 175.23/175.40 cnf(3958,plain, % 175.23/175.40 (~P3(f4(a2,a1,a1),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3931,3920,3935,3848,3922,3738,3746,3532,2031,336,2,3,14,15,31,12,28,13,30])). % 175.23/175.40 cnf(3959,plain, % 175.23/175.40 (~P3(f4(a2,a1,a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[3958,3763])). % 175.23/175.40 cnf(3961,plain, % 175.23/175.40 (~P3(f4(a2,a1,a1),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[3958,3348,3638,3763,2,35])). % 175.23/175.40 cnf(3963,plain, % 175.23/175.40 (~E(a6,f8(a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3958,3500,3348,3638,3763,2,35,3])). % 175.23/175.40 cnf(3965,plain, % 175.23/175.40 (E(f8(x39651,a1),x39651)), % 175.23/175.40 inference(rename_variables,[],[19])). % 175.23/175.40 cnf(3968,plain, % 175.23/175.40 (E(f4(a1,a1,a2),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3965,3958,3946,3500,3348,3638,3523,3572,3763,2,35,3,15,31])). % 175.23/175.40 cnf(3970,plain, % 175.23/175.40 (~P3(f4(a2,a2,a2),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3965,3958,3946,3945,3500,3348,3638,3523,3572,3763,2,35,3,15,31,12])). % 175.23/175.40 cnf(3971,plain, % 175.23/175.40 (~P3(f4(a2,a1,a1),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3965,3958,3946,3945,3500,3348,3638,3523,3572,3763,2,35,3,15,31,12,3802])). % 175.23/175.40 cnf(3972,plain, % 175.23/175.40 (~E(f8(a1,a1),f8(a5,x39721))), % 175.23/175.40 inference(scs_inference,[],[19,3965,3958,3946,3945,3500,3348,3638,3523,3572,3222,840,3763,2,35,3,15,31,12,3802,11])). % 175.23/175.40 cnf(3973,plain, % 175.23/175.40 (~P3(f4(a2,a1,a1),f4(a1,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3965,3958,3946,3945,3500,3348,3638,3523,3572,3222,840,3763,2,35,3,15,31,12,3802,11,3472])). % 175.23/175.40 cnf(3978,plain, % 175.23/175.40 (~E(f8(a2,a7),f8(a7,a5))), % 175.23/175.40 inference(scs_inference,[],[3970,3944,3972,3706,22,2,35,3])). % 175.23/175.40 cnf(3985,plain, % 175.23/175.40 (~P3(f4(a2,a2,a2),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[3970,3944,3855,3866,3972,3706,124,3229,22,2,35,3,15,31,3765])). % 175.23/175.40 cnf(3989,plain, % 175.23/175.40 (~P3(f4(a1,a1,a2),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,3970,3961,3968,3944,3855,3866,3972,3706,124,3229,22,2,35,3,15,31,3765,14,12])). % 175.23/175.40 cnf(3991,plain, % 175.23/175.40 (~E(f8(a7,a5),f8(a2,a7))), % 175.23/175.40 inference(scs_inference,[],[3978,2])). % 175.23/175.40 cnf(3995,plain, % 175.23/175.40 (~E(f8(a1,a7),f8(a7,a5))), % 175.23/175.40 inference(scs_inference,[],[3985,3978,3269,3232,2,35,3])). % 175.23/175.40 cnf(4005,plain, % 175.23/175.40 (~P3(f4(a2,a1,a1),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[3973,3995,3852,2,35])). % 175.23/175.40 cnf(4007,plain, % 175.23/175.40 (~E(f8(a5,a7),f8(a2,a7))), % 175.23/175.40 inference(scs_inference,[],[3973,3991,3995,3852,22,2,35,3])). % 175.23/175.40 cnf(4013,plain, % 175.23/175.40 (~P3(f8(x40131,a1),f4(a2,a2,a2))+P3(x40131,f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3973,3991,3995,3887,3852,3945,2031,22,2,35,3,31,13,12])). % 175.23/175.40 cnf(4014,plain, % 175.23/175.40 (~E(f8(a2,a7),f8(a5,a7))), % 175.23/175.40 inference(scs_inference,[],[4007,2])). % 175.23/175.40 cnf(4015,plain, % 175.23/175.40 (~P3(f4(a1,a1,a2),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4007,3989,3543,2,35])). % 175.23/175.40 cnf(4017,plain, % 175.23/175.40 (~E(a7,f8(a5,a2))), % 175.23/175.40 inference(scs_inference,[],[19,4007,3559,3989,3543,2,35,3])). % 175.23/175.40 cnf(4020,plain, % 175.23/175.40 (~P2(f8(a7,a2),f8(a5,a5))), % 175.23/175.40 inference(scs_inference,[],[19,3564,4007,3559,3989,3543,22,2,35,3,14])). % 175.23/175.40 cnf(4024,plain, % 175.23/175.40 (~P3(f4(a2,a2,a2),f4(a1,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3564,4005,4007,3559,3989,3543,3968,3985,22,2,35,3,14,12,3802,3472])). % 175.23/175.40 cnf(4026,plain, % 175.23/175.40 (~P3(f4(a1,a1,a2),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[19,3564,4005,4007,3559,3989,3543,3968,3985,22,2,35,3,14,12,3802,3472,3763])). % 175.23/175.40 cnf(4027,plain, % 175.23/175.40 (E(f4(a1,a1,a1),f4(a2,a2,a1))+~P2(f4(a1,a1,a1),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3564,4005,4007,3559,3989,3543,3864,3968,3985,22,2,35,3,14,12,3802,3472,3763,31])). % 175.23/175.40 cnf(4032,plain, % 175.23/175.40 (~E(f8(a1,a1),a6)), % 175.23/175.40 inference(scs_inference,[],[3963,2])). % 175.23/175.40 cnf(4040,plain, % 175.23/175.40 (~P2(f8(a7,x40401),a1)), % 175.23/175.40 inference(scs_inference,[],[4024,4020,4014,3963,3343,3299,62,3232,47,2,35,3,15,31])). % 175.23/175.40 cnf(4043,plain, % 175.23/175.40 (~E(f8(a1,a1),a5)), % 175.23/175.40 inference(scs_inference,[],[4024,4020,4014,3963,3343,3299,2513,62,840,3232,47,2,35,3,15,31,11])). % 175.23/175.40 cnf(4048,plain, % 175.23/175.40 (~E(a6,f8(a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,3647,4043,3498,3985,2,35,3])). % 175.23/175.40 cnf(4051,plain, % 175.23/175.40 (E(f4(a1,a1,a2),f4(a2,a2,a1))+~P2(f4(a1,a1,a2),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3647,4043,3751,3498,3985,2,35,3,31])). % 175.23/175.40 cnf(4062,plain, % 175.23/175.40 (~P3(f4(a1,a2,a2),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4017,4048,4026,3971,3898,3397,2031,2,35,31,12])). % 175.23/175.40 cnf(4063,plain, % 175.23/175.40 (~P3(f4(a1,a1,a2),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[4017,4048,4015,4026,3971,3898,3695,3397,2031,2,35,31,12,13])). % 175.23/175.40 cnf(4064,plain, % 175.23/175.40 (~E(f8(a6,x40641),a1)), % 175.23/175.40 inference(scs_inference,[],[3451,2])). % 175.23/175.40 cnf(4065,plain, % 175.23/175.40 (~P3(f4(a1,a2,a2),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4062,3451,3184,2,13])). % 175.23/175.40 cnf(4068,plain, % 175.23/175.40 (E(f8(x40681,a2),f8(x40681,a1))), % 175.23/175.40 inference(rename_variables,[],[3229])). % 175.23/175.40 cnf(4071,plain, % 175.23/175.40 (~P3(f4(a2,a2,a1),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4062,3451,3937,3893,2480,3184,3229,4068,2,13,14,15,12])). % 175.23/175.40 cnf(4072,plain, % 175.23/175.40 (~P3(f4(a1,a2,a2),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4062,3451,3937,3893,2480,3184,3229,4068,2,13,14,15,12,3763])). % 175.23/175.40 cnf(4073,plain, % 175.23/175.40 (~P3(f4(a1,a1,a2),f4(a2,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[4062,3451,3937,3893,2480,4015,3706,3184,3229,4068,2,13,14,15,12,3763,35])). % 175.23/175.40 cnf(4077,plain, % 175.23/175.40 (~P3(f4(a1,a2,a2),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[4062,3451,3937,3893,2480,3494,4015,3706,3184,3229,4068,2,13,14,15,12,3763,35,31,3670])). % 175.23/175.40 cnf(4080,plain, % 175.23/175.40 (~P2(f4(a2,a1,a2),f4(a2,a2,a1))+E(f4(a2,a1,a2),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4062,3451,3937,3893,2480,3494,4015,3706,3184,3229,4068,2,13,14,15,12,3763,35,31,3670,28,3])). % 175.23/175.40 cnf(4081,plain, % 175.23/175.40 (~P3(f4(a1,a2,a2),f4(a1,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[4072,3472])). % 175.23/175.40 cnf(4083,plain, % 175.23/175.40 (~E(f8(a5,x40831),a1)), % 175.23/175.40 inference(scs_inference,[],[4072,3493,3472,2])). % 175.23/175.40 cnf(4090,plain, % 175.23/175.40 (~P2(f8(x40901,a7),a2)), % 175.23/175.40 inference(scs_inference,[],[20,4065,4072,4032,3382,3493,4040,3861,3720,102,3185,329,3472,2,3,13,14,15,31])). % 175.23/175.40 cnf(4094,plain, % 175.23/175.40 (E(f4(a1,a1,a1),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[20,4065,4072,4073,4032,3382,3493,4040,3861,3720,3784,102,3185,329,3472,2,3,13,14,15,31,12,4027])). % 175.23/175.40 cnf(4095,plain, % 175.23/175.40 (~P3(f4(a2,a2,a1),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[20,4065,4072,4073,4032,3382,3493,4040,3861,3720,3784,102,3185,329,3472,2,3,13,14,15,31,12,4027,3538])). % 175.23/175.40 cnf(4097,plain, % 175.23/175.40 (~P3(f4(a2,a2,a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[20,4065,4072,4073,4032,3382,3493,4040,3861,3720,3784,102,3185,329,3472,2,3,13,14,15,31,12,4027,3538,3765])). % 175.23/175.40 cnf(4099,plain, % 175.23/175.40 (~E(f8(a2,a1),a6)), % 175.23/175.40 inference(scs_inference,[],[20,4065,4072,4073,4032,3382,3493,4040,3861,3720,3784,23,102,845,3185,329,3472,2,3,13,14,15,31,12,4027,3538,3765,11])). % 175.23/175.40 cnf(4100,plain, % 175.23/175.40 (~E(a6,f8(a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4099,2])). % 175.23/175.40 cnf(4101,plain, % 175.23/175.40 (E(f4(a1,a2,a2),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4094,4099,3873,2,3])). % 175.23/175.40 cnf(4103,plain, % 175.23/175.40 (~P2(f8(a5,a5),a2)), % 175.23/175.40 inference(scs_inference,[],[4071,4094,4099,3873,3819,21,2,3,13,14])). % 175.23/175.40 cnf(4109,plain, % 175.23/175.40 (~P3(f4(a1,a1,a1),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4071,4094,4099,4064,4090,3873,3819,62,336,21,2,3,13,14,15,31,12])). % 175.23/175.40 cnf(4113,plain, % 175.23/175.40 (~E(f8(a6,a1),f8(a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4100,3513,82,2,3])). % 175.23/175.40 cnf(4115,plain, % 175.23/175.40 (~P3(f4(a1,a1,a1),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4101,4109,4100,3513,82,2,3,13])). % 175.23/175.40 cnf(4122,plain, % 175.23/175.40 (~P3(f4(a1,a2,a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[20,4101,4109,4100,4103,3513,3959,3920,3784,62,336,82,2,3,13,14,15,31,12])). % 175.23/175.40 cnf(4123,plain, % 175.23/175.40 (E(f4(a1,a1,a2),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[20,4101,4109,4100,4103,3513,3959,3920,3784,62,336,82,2,3,13,14,15,31,12,4051])). % 175.23/175.40 cnf(4125,plain, % 175.23/175.40 (E(f4(a2,a1,a2),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4123,3520,3228,2,3])). % 175.23/175.40 cnf(4133,plain, % 175.23/175.40 (~P3(f4(a1,a2,a2),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4095,4115,4123,3520,4083,3873,3656,3631,3228,62,21,2,3,13,14,31,12])). % 175.23/175.40 cnf(4134,plain, % 175.23/175.40 (~P3(f4(a1,a2,a1),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[4095,4122,4115,4123,3520,4083,3873,3656,3631,3228,62,21,2,3,13,14,31,12,3670])). % 175.23/175.40 cnf(4135,plain, % 175.23/175.40 (P2(f4(a2,a1,a2),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4095,4122,4115,4123,3520,4083,3873,3656,3631,3228,62,21,2,3,13,14,31,12,3670,28])). % 175.23/175.40 cnf(4137,plain, % 175.23/175.40 (~P3(f4(a2,a2,a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[4095,4122,4115,4123,3520,4083,3309,3873,3656,3631,3228,62,21,2,3,13,14,31,12,3670,28,35])). % 175.23/175.40 cnf(4140,plain, % 175.23/175.40 (E(f4(a2,a1,a2),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4095,4122,4115,4123,3520,4083,3309,3873,3656,3631,3228,62,21,2,3,13,14,31,12,3670,28,35,4080])). % 175.23/175.40 cnf(4142,plain, % 175.23/175.40 (~P3(f4(a1,a2,a1),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4134,3802])). % 175.23/175.40 cnf(4152,plain, % 175.23/175.40 (~P3(f4(a2,a1,a2),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[20,4097,4113,4137,4134,4125,4140,3651,3898,102,3185,3802,2,3,13,14,31,12])). % 175.23/175.40 cnf(4158,plain, % 175.23/175.40 (~P3(f4(a1,a2,a1),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4142,3658,4101,2,13])). % 175.23/175.40 cnf(4159,plain, % 175.23/175.40 (E(f4(a2,a2,a1),f4(a2,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[4142,4135,3658,4101,3494,2,13,31])). % 175.23/175.40 cnf(4161,plain, % 175.23/175.40 (~P3(f4(a2,a1,a2),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4133,4142,4135,3658,4101,4140,3494,2,13,31,12])). % 175.23/175.40 cnf(4162,plain, % 175.23/175.40 (P2(f4(a2,x41621,a2),f4(a1,x41621,a1))), % 175.23/175.40 inference(scs_inference,[],[20,4133,4142,4135,3658,4101,4140,3494,3291,2,13,31,12,14])). % 175.23/175.40 cnf(4165,plain, % 175.23/175.40 (E(f4(a1,a2,a2),f4(a2,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[4159,3764,4101,2,3])). % 175.23/175.40 cnf(4170,plain, % 175.23/175.40 (~P3(f4(a1,a1,a1),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[4152,4159,4077,3764,3604,4101,3505,102,2,3,13,31,12])). % 175.23/175.40 cnf(4172,plain, % 175.23/175.40 (~E(f8(a5,x41721),a2)), % 175.23/175.40 inference(scs_inference,[],[3783,2])). % 175.23/175.40 cnf(4173,plain, % 175.23/175.40 (~E(f8(a1,a2),a5)), % 175.23/175.40 inference(scs_inference,[],[3783,4043,3185,2,3])). % 175.23/175.40 cnf(4176,plain, % 175.23/175.40 (E(f4(a2,x41761,a2),f4(a1,x41761,a1))), % 175.23/175.40 inference(scs_inference,[],[4158,4162,3783,4043,3457,4140,3185,2,3,13,31])). % 175.23/175.40 cnf(4180,plain, % 175.23/175.40 (~P3(f4(a2,a1,a2),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4158,4081,4162,3783,4043,3457,4140,3185,2,3,13,31,12,3902])). % 175.23/175.40 cnf(4184,plain, % 175.23/175.40 (~P3(f4(a1,a2,a1),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[4158,4081,4162,3783,3943,4043,3457,3445,4140,3185,2,3,13,31,12,3902,35,3538])). % 175.23/175.40 cnf(4188,plain, % 175.23/175.40 (~P3(a5,f8(f3(a5,f8(a1,a2)),f3(a5,f8(a1,a2))))), % 175.23/175.40 inference(scs_inference,[],[4173,2650])). % 175.23/175.40 cnf(4195,plain, % 175.23/175.40 (~E(f8(a2,a2),a5)), % 175.23/175.40 inference(scs_inference,[],[4184,4180,4173,4172,4125,3720,102,3188,2,13,31,12,3])). % 175.23/175.40 cnf(4198,plain, % 175.23/175.40 (~P3(f4(a1,a1,a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4170,4195,3755,2,13])). % 175.23/175.40 cnf(4207,plain, % 175.23/175.40 (~P3(f4(a1,a1,a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[21,4198,3467,3562,3819,2,15,13])). % 175.23/175.40 cnf(4213,plain, % 175.23/175.40 (~P3(x42131,f8(a5,a5))+P3(x42131,f8(a1,a7))), % 175.23/175.40 inference(scs_inference,[],[21,3579,3627,1113,2,12,35])). % 175.23/175.40 cnf(4215,plain, % 175.23/175.40 (P3(x42151,a7)+~P3(x42151,f8(a5,a5))), % 175.23/175.40 inference(scs_inference,[],[21,3579,3627,1113,48,2,12,35,46])). % 175.23/175.40 cnf(4236,plain, % 175.23/175.40 (~E(a7,f8(a1,a5))), % 175.23/175.40 inference(scs_inference,[],[21,3786,2413,2,3])). % 175.23/175.40 cnf(4241,plain, % 175.23/175.40 (~P3(f4(a1,a2,a2),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[21,3786,3929,4072,3562,2413,3229,2,3,12,13])). % 175.23/175.40 cnf(4245,plain, % 175.23/175.40 (~P3(f4(a2,a1,a2),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[21,4236,4161,3698,3405,2,12,35])). % 175.23/175.40 cnf(4250,plain, % 175.23/175.40 (P3(f3(a5,a2),a7)), % 175.23/175.40 inference(scs_inference,[],[3826,4215,44])). % 175.23/175.40 cnf(4254,plain, % 175.23/175.40 (~P3(f4(a2,a1,a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[4241,4250,3530,50,30,2,12])). % 175.23/175.40 cnf(4257,plain, % 175.23/175.40 (~P3(f4(a1,a2,a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[4254,3920,12])). % 175.23/175.40 cnf(4263,plain, % 175.23/175.40 (~P3(x42631,f8(a1,a5))+P3(x42631,f8(a7,a7))), % 175.23/175.40 inference(scs_inference,[],[21,3271,1135,12,35])). % 175.23/175.40 cnf(4265,plain, % 175.23/175.40 (P3(x42651,a7)+~P3(x42651,f8(a1,a5))), % 175.23/175.40 inference(scs_inference,[],[21,3271,1135,12,35,46])). % 175.23/175.40 cnf(4302,plain, % 175.23/175.40 (P3(x43021,a7)+~P3(x43021,f8(a5,a1))), % 175.23/175.40 inference(scs_inference,[],[1151,48,35,46])). % 175.23/175.40 cnf(4322,plain, % 175.23/175.40 (~P3(x43221,f8(a5,a1))+P3(x43221,f8(a7,a1))), % 175.23/175.40 inference(scs_inference,[],[374,35])). % 175.23/175.40 cnf(4325,plain, % 175.23/175.40 (~P3(f8(a1,a7),x43251)+~P3(x43251,f8(a5,a5))), % 175.23/175.40 inference(scs_inference,[],[4213,30])). % 175.23/175.40 cnf(4328,plain, % 175.23/175.40 (~P3(x43281,f8(a1,a5))+P3(x43281,f8(x43282,f8(a7,a7)))), % 175.23/175.40 inference(scs_inference,[],[4263,44])). % 175.23/175.40 cnf(4350,plain, % 175.23/175.40 (~P3(f8(a7,a1),x43501)+~P3(x43501,f8(a5,a1))), % 175.23/175.40 inference(scs_inference,[],[4322,30])). % 175.23/175.40 cnf(4351,plain, % 175.23/175.40 (E(a2,f8(a1,a1))), % 175.23/175.40 inference(scs_inference,[],[48,77,40])). % 175.23/175.40 cnf(4361,plain, % 175.23/175.40 (~P3(f8(a1,a7),f8(a1,a5))+~P3(f8(a1,a7),a5)), % 175.23/175.40 inference(scs_inference,[],[1438,35,4325,45])). % 175.23/175.40 cnf(4397,plain, % 175.23/175.40 (~P3(x43971,f8(a5,a5))+P3(x43971,f8(a7,a1))), % 175.23/175.40 inference(scs_inference,[],[129,35])). % 175.23/175.40 cnf(4399,plain, % 175.23/175.40 (~P3(f8(a7,a1),x43991)+~P3(x43991,f8(a5,a5))), % 175.23/175.40 inference(scs_inference,[],[4397,30])). % 175.23/175.40 cnf(4420,plain, % 175.23/175.40 (E(a2,f8(a1,a2))), % 175.23/175.40 inference(scs_inference,[],[77,3826,111,48,35,40])). % 175.23/175.40 cnf(4442,plain, % 175.23/175.40 (~P3(f8(a2,a7),f8(a1,a5))+~P3(f8(a1,a7),a5)), % 175.23/175.40 inference(scs_inference,[],[3232,4361,12])). % 175.23/175.40 cnf(4448,plain, % 175.23/175.40 (~P3(f8(a2,a7),f8(a2,a5))+~P3(f8(a1,a7),a5)), % 175.23/175.40 inference(scs_inference,[],[3232,4442,13])). % 175.23/175.40 cnf(4452,plain, % 175.23/175.40 (~P3(f8(a2,a7),a5)+~P3(f8(a1,a7),a5)), % 175.23/175.40 inference(scs_inference,[],[3232,4448,36])). % 175.23/175.40 cnf(4453,plain, % 175.23/175.40 (~P3(f8(a1,a7),a5)), % 175.23/175.40 inference(scs_inference,[],[3188,4452,12])). % 175.23/175.40 cnf(4456,plain, % 175.23/175.40 (~P3(f8(a1,a7),f8(a5,a1))), % 175.23/175.40 inference(scs_inference,[],[4453,954,3232,12,35])). % 175.23/175.40 cnf(4459,plain, % 175.23/175.40 (~P3(f8(a1,a7),f8(a5,a5))), % 175.23/175.40 inference(scs_inference,[],[4453,954,3232,21,12,35,13])). % 175.23/175.40 cnf(4461,plain, % 175.23/175.40 (~P3(f8(a2,a7),f8(a5,a5))), % 175.23/175.40 inference(scs_inference,[],[4453,954,3232,21,12,35,13,46])). % 175.23/175.40 cnf(4470,plain, % 175.23/175.40 (~P3(f8(a1,a7),f8(a1,a5))), % 175.23/175.40 inference(scs_inference,[],[4456,3594,3232,12,35])). % 175.23/175.40 cnf(4476,plain, % 175.23/175.40 (~P3(f8(a7,a1),f8(a5,a5))), % 175.23/175.40 inference(scs_inference,[],[4459,22,12])). % 175.23/175.40 cnf(4477,plain, % 175.23/175.40 (E(f8(x44771,x44772),f8(x44772,x44771))), % 175.23/175.40 inference(rename_variables,[],[22])). % 175.23/175.40 cnf(4478,plain, % 175.23/175.40 (~P3(f8(a1,a7),f8(a2,a5))), % 175.23/175.40 inference(scs_inference,[],[4459,4470,3527,22,12,35])). % 175.23/175.40 cnf(4481,plain, % 175.23/175.40 (~P3(f8(a7,a1),a5)), % 175.23/175.40 inference(scs_inference,[],[4459,4470,3527,22,4477,12,35,37])). % 175.23/175.40 cnf(4484,plain, % 175.23/175.40 (~P3(f8(a7,a1),f8(a5,a1))), % 175.23/175.40 inference(scs_inference,[],[4459,4470,3527,19,22,4477,12,35,37,13])). % 175.23/175.40 cnf(4491,plain, % 175.23/175.40 (~P3(f8(a7,a2),f8(a5,a1))), % 175.23/175.40 inference(scs_inference,[],[4484,3229,12])). % 175.23/175.40 cnf(4493,plain, % 175.23/175.40 (~P3(f8(a2,a7),f8(a2,a5))), % 175.23/175.40 inference(scs_inference,[],[4478,3232,12])). % 175.23/175.40 cnf(4501,plain, % 175.23/175.40 (~P3(f8(a7,a2),f8(a5,a2))), % 175.23/175.40 inference(scs_inference,[],[4491,4493,4481,3356,3229,82,35,12,13])). % 175.23/175.40 cnf(4505,plain, % 175.23/175.40 (~P3(f8(f4(a2,a2,a2),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[4257,4176,4013,12])). % 175.23/175.40 cnf(4506,plain, % 175.23/175.40 (~P3(f8(a7,a1),f8(a5,a2))), % 175.23/175.40 inference(scs_inference,[],[4501,3185,12])). % 175.23/175.40 cnf(4557,plain, % 175.23/175.40 (E(f8(x45571,f3(x45572,f8(x45573,x45574))),f8(x45571,f3(x45572,f8(f8(x45573,x45573),x45574))))), % 175.23/175.40 inference(scs_inference,[],[3373,4505,3676,2028,857,919,71,91,39,32,33,10,9,7,8,29,3472,6,5])). % 175.23/175.40 cnf(4560,plain, % 175.23/175.40 (P3(f3(f8(a1,a7),f8(f8(a1,a5),f8(a1,a5))),f8(a1,a7))), % 175.23/175.40 inference(scs_inference,[],[3373,4505,3676,2028,857,919,71,91,39,32,33,10,9,7,8,29,3472,6,5,28,34])). % 175.23/175.40 cnf(4566,plain, % 175.23/175.40 (E(f8(f3(x45661,f8(x45662,x45663)),x45664),f8(f3(x45661,f8(f8(x45662,x45662),x45663)),x45664))), % 175.23/175.40 inference(scs_inference,[],[3373,3396,4505,3676,2028,857,919,2751,71,91,39,32,33,10,9,7,8,29,3472,6,5,28,34,45,25,4])). % 175.23/175.40 cnf(4574,plain, % 175.23/175.40 (~P3(x45741,f8(a1,f8(a1,a1)))), % 175.23/175.40 inference(rename_variables,[],[2008])). % 175.23/175.40 cnf(4579,plain, % 175.23/175.40 (P3(f3(a5,f8(a2,a1)),f8(f8(a7,a7),f8(a7,a7)))), % 175.23/175.40 inference(scs_inference,[],[220,2292,3373,3396,3809,4505,2008,3676,3831,2028,857,919,2751,48,71,91,39,32,33,10,9,7,8,29,3472,6,5,28,34,45,25,4,30,44,2,11,36,46,35])). % 175.23/175.40 cnf(4581,plain, % 175.23/175.40 (~P2(f8(a2,a7),f8(f8(a1,a5),f8(a1,a5)))), % 175.23/175.40 inference(scs_inference,[],[220,2292,3373,3396,3809,4505,2008,3676,3831,2028,857,919,2751,3232,48,71,91,39,32,33,10,9,7,8,29,3472,6,5,28,34,45,25,4,30,44,2,11,36,46,35,14])). % 175.23/175.40 cnf(4588,plain, % 175.23/175.40 (~P2(f8(a1,a7),f8(f8(f8(a1,a5),f8(a1,a5)),a1))), % 175.23/175.40 inference(scs_inference,[],[220,4506,2292,3373,3396,3809,4505,2008,3676,3831,2028,857,919,2751,2141,2123,3232,19,48,71,91,39,32,33,10,9,7,8,29,3472,6,5,28,34,45,25,4,30,44,2,11,36,46,35,14,12,37,15])). % 175.23/175.40 cnf(4589,plain, % 175.23/175.40 (E(f8(x45891,a1),x45891)), % 175.23/175.40 inference(rename_variables,[],[19])). % 175.23/175.40 cnf(4593,plain, % 175.23/175.40 (E(f8(x45931,a1),x45931)), % 175.23/175.40 inference(rename_variables,[],[19])). % 175.23/175.40 cnf(4594,plain, % 175.23/175.40 (E(f8(f8(a2,a2),f8(a2,a1)),f8(f8(f8(f8(a2,a2),f8(a2,a1)),a1),f8(f8(f8(a2,a2),f8(a2,a1)),a1)))), % 175.23/175.40 inference(scs_inference,[],[220,4461,4506,2292,3373,3396,3809,4505,2008,2285,3676,3831,2028,857,919,2751,2141,2694,2123,982,3188,3232,19,4589,48,71,91,39,32,33,10,9,7,8,29,3472,6,5,28,34,45,25,4,30,44,2,11,36,46,35,14,12,37,15,3,13,31])). % 175.23/175.40 cnf(4598,plain, % 175.23/175.40 (E(f8(a1,f8(a1,a1)),f8(f8(f8(a2,a2),f8(a1,a1)),f8(a1,f8(a1,a1))))), % 175.23/175.40 inference(scs_inference,[],[220,4461,4506,2292,3373,3396,3809,4505,2008,4574,2285,2653,3676,3831,2028,857,919,2751,2141,2694,2123,982,3188,3232,19,4589,48,71,91,39,32,33,10,9,7,8,29,3472,6,5,28,34,45,25,4,30,44,2,11,36,46,35,14,12,37,15,3,13,31,40])). % 175.23/175.40 cnf(4606,plain, % 175.23/175.40 (~P3(f8(f4(a1,a1,a1),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[220,4461,4506,2292,3373,3396,3809,4505,2008,4574,2285,2653,3676,3831,2028,857,919,2751,2141,4207,2694,2123,982,3188,3232,19,4589,4593,48,71,91,39,32,33,10,9,7,8,29,3472,6,5,28,34,45,25,4,30,44,2,11,36,46,35,14,12,37,15,3,13,31,40,38,4013])). % 175.23/175.40 cnf(4612,plain, % 175.23/175.40 (P3(f3(f8(a7,a1),f8(a5,a1)),f8(x46121,f8(a7,a1)))), % 175.23/175.40 inference(scs_inference,[],[857,3373,2,44])). % 175.23/175.40 cnf(4628,plain, % 175.23/175.40 (~P3(f8(f4(a1,a2,a2),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[857,3373,3676,59,3831,4241,4606,2,44,30,45,34,28,3670,3472,3902,4013])). % 175.23/175.40 cnf(4634,plain, % 175.23/175.40 (~P3(x46341,f8(f8(a1,a1),a1))), % 175.23/175.40 inference(rename_variables,[],[190])). % 175.23/175.40 cnf(4636,plain, % 175.23/175.40 (E(x46361,f8(x46361,x46361))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(4638,plain, % 175.23/175.40 (E(f8(x46381,a1),x46381)), % 175.23/175.40 inference(rename_variables,[],[19])). % 175.23/175.40 cnf(4641,plain, % 175.23/175.40 (~P3(a5,f3(a5,f8(f8(a1,a1),a2)))), % 175.23/175.40 inference(scs_inference,[],[190,47,4636,19,62,857,2031,195,3016,3373,3696,3676,59,3831,4241,4606,4188,4566,2,44,30,45,34,28,3670,3472,3902,4013,31,13,15,3,12,37])). % 175.23/175.40 cnf(4652,plain, % 175.23/175.40 (E(f8(x46521,a1),x46521)), % 175.23/175.40 inference(rename_variables,[],[19])). % 175.23/175.40 cnf(4654,plain, % 175.23/175.40 (~P3(f4(a7,a5,a7),a7)), % 175.23/175.40 inference(scs_inference,[],[299,190,47,4636,823,19,4638,52,62,145,857,2031,195,3016,3373,3696,3676,332,59,3831,3416,4241,4606,4188,4566,2,44,30,45,34,28,3670,3472,3902,4013,31,13,15,3,12,37,14,35,46,36,42])). % 175.23/175.40 cnf(4658,plain, % 175.23/175.40 (~P3(f4(a5,a7,a7),a7)), % 175.23/175.40 inference(scs_inference,[],[299,190,47,4636,823,19,4638,4652,52,669,62,145,857,2031,195,3016,3373,3696,3676,332,59,3831,3195,3416,4241,4606,4188,4566,2,44,30,45,34,28,3670,3472,3902,4013,31,13,15,3,12,37,14,35,46,36,42,11,41])). % 175.23/175.40 cnf(4660,plain, % 175.23/175.40 (~P3(x46601,f8(f8(f8(a1,a1),a1),a2))), % 175.23/175.40 inference(scs_inference,[],[299,190,4634,48,47,4636,823,19,4638,4652,3229,52,669,62,145,857,2031,195,3016,3373,3696,3676,332,59,3831,3195,3416,4241,4606,4188,4566,2,44,30,45,34,28,3670,3472,3902,4013,31,13,15,3,12,37,14,35,46,36,42,11,41,38])). % 175.23/175.40 cnf(4685,plain, % 175.23/175.40 (P2(f8(a1,f8(a1,a1)),x46851)), % 175.23/175.40 inference(scs_inference,[],[3696,3230,919,2008,2,44,30,45,34])). % 175.23/175.40 cnf(4693,plain, % 175.23/175.40 (~P3(f8(f4(a2,a1,a2),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[3696,3230,919,2008,4245,4628,3677,2,44,30,45,34,28,3670,3472,4013])). % 175.23/175.40 cnf(4708,plain, % 175.23/175.40 (~P3(x47081,f8(f8(a1,a1),a1))), % 175.23/175.40 inference(rename_variables,[],[190])). % 175.23/175.40 cnf(4712,plain, % 175.23/175.40 (E(x47121,f8(x47121,x47121))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(4714,plain, % 175.23/175.40 (~P3(x47141,f8(f8(f8(a2,a2),f8(a2,a1)),a1))), % 175.23/175.40 inference(scs_inference,[],[190,296,47,19,3224,257,3696,332,1374,3230,919,2008,4245,4628,4654,4658,2691,4594,3677,2,44,30,45,34,28,3670,3472,4013,4265,3902,4302,4215,4328,31,13,3,15,12,37])). % 175.23/175.40 cnf(4725,plain, % 175.23/175.40 (~P3(x47251,f8(f8(f8(a1,a1),a1),a1))), % 175.23/175.40 inference(scs_inference,[],[190,4708,296,47,4712,19,21,77,52,669,3185,195,3224,257,3696,332,1374,359,3230,3213,919,2008,4245,4628,4654,4658,2691,4594,3677,2,44,30,45,34,28,3670,3472,4013,4265,3902,4302,4215,4328,31,13,3,15,12,37,14,35,46,11,38])). % 175.23/175.40 cnf(4740,plain, % 175.23/175.40 (P1(f8(a1,f8(a1,a1)))), % 175.23/175.40 inference(scs_inference,[],[4685,1715])). % 175.23/175.40 cnf(4744,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(x47441,f8(x47442,f8(a7,x47443))))), % 175.23/175.40 inference(scs_inference,[],[332,4566,2,44])). % 175.23/175.40 cnf(4748,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(f8(x47481,f8(a7,x47482)),x47483))), % 175.23/175.40 inference(scs_inference,[],[332,4566,3807,2,44,30,45])). % 175.23/175.40 cnf(4752,plain, % 175.23/175.40 (P2(f8(f8(a2,a2),f8(a1,a1)),x47521)), % 175.23/175.40 inference(scs_inference,[],[332,2653,4566,3807,4581,2,44,30,45,28,34])). % 175.23/175.40 cnf(4758,plain, % 175.23/175.40 (~P3(f8(f4(a2,a1,a1),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[332,2653,4566,4254,3807,4693,4581,2,44,30,45,28,34,3670,3472,4013])). % 175.23/175.40 cnf(4767,plain, % 175.23/175.40 (E(f8(f4(x47671,a2,x47672),a1),f4(x47671,a1,x47672))), % 175.23/175.40 inference(scs_inference,[],[190,19,62,3227,332,359,2694,2653,4566,4254,3807,4693,4581,2,44,30,45,28,34,3670,3472,4013,3902,31,13,3])). % 175.23/175.40 cnf(4770,plain, % 175.23/175.40 (P2(f4(a2,a1,a1),f8(f4(a1,a2,a2),f4(a1,a2,a2)))), % 175.23/175.40 inference(scs_inference,[],[190,296,47,19,62,3227,332,359,3405,4658,2694,2653,4566,4254,3807,4693,4581,2,44,30,45,28,34,3670,3472,4013,3902,31,13,3,12,15])). % 175.23/175.40 cnf(4771,plain, % 175.23/175.40 (E(x47711,f8(x47711,x47711))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(4777,plain, % 175.23/175.40 (~P3(f4(a5,a7,a7),f8(a7,a7))), % 175.23/175.40 inference(scs_inference,[],[190,296,47,4771,19,52,62,257,3227,332,359,3405,363,4658,2694,2653,4566,4254,3807,4693,4581,2,44,30,45,28,34,3670,3472,4013,3902,31,13,3,12,15,14,35,46])). % 175.23/175.40 cnf(4801,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(x48011,f8(x48012,f8(x48013,a7))))), % 175.23/175.40 inference(scs_inference,[],[359,4594,2,44])). % 175.23/175.40 cnf(4805,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(f8(x48051,f8(x48052,a7)),x48053))), % 175.23/175.40 inference(scs_inference,[],[359,4594,3847,2,44,30,45])). % 175.23/175.40 cnf(4815,plain, % 175.23/175.40 (~P3(f8(f4(a1,a2,a1),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[359,4594,4257,3847,4758,2211,4588,2,44,30,45,28,34,3670,3472,4013])). % 175.23/175.40 cnf(4823,plain, % 175.23/175.40 (~P3(x48231,f8(f8(a1,a1),a1))), % 175.23/175.40 inference(rename_variables,[],[190])). % 175.23/175.40 cnf(4824,plain, % 175.23/175.40 (E(f8(f4(x48241,x48242,a2),a1),f4(x48241,x48242,a1))), % 175.23/175.40 inference(scs_inference,[],[190,19,62,3225,359,363,179,4594,4257,3847,4758,2211,4588,2,44,30,45,28,34,3670,3472,4013,3902,31,13,3])). % 175.23/175.40 cnf(4828,plain, % 175.23/175.40 (E(x48281,f8(x48281,x48281))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(4839,plain, % 175.23/175.40 (~P3(x48391,f8(f8(a1,a1),a1))), % 175.23/175.40 inference(rename_variables,[],[190])). % 175.23/175.40 cnf(4846,plain, % 175.23/175.40 (~P3(x48461,f8(f8(f8(a2,a2),f8(a1,a1)),f8(a1,f8(a1,a1))))), % 175.23/175.40 inference(scs_inference,[],[190,4823,4839,48,47,4828,2318,19,52,62,3225,359,1374,4658,363,3267,161,3846,4566,3513,179,4594,4257,3847,4758,2211,4641,4588,4740,4598,2,44,30,45,28,34,3670,3472,4013,3902,31,13,3,12,15,14,35,46,11,38,40,29])). % 175.23/175.40 cnf(4858,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(x48581,f8(f8(x48582,a7),x48583)))), % 175.23/175.40 inference(scs_inference,[],[363,4598,2,44])). % 175.23/175.40 cnf(4862,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(f8(f8(x48621,a7),x48622),x48623))), % 175.23/175.40 inference(scs_inference,[],[363,4598,4560,2,44,30,45])). % 175.23/175.40 cnf(4870,plain, % 175.23/175.40 (~P3(f8(f4(a2,a2,a1),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[363,4598,4137,4560,4815,2200,2,44,30,45,34,3670,3472,4013])). % 175.23/175.40 cnf(4879,plain, % 175.23/175.40 (E(f8(f4(a2,x48791,x48792),a1),f4(a1,x48791,x48792))), % 175.23/175.40 inference(scs_inference,[],[190,19,62,3228,363,334,163,4598,4137,4560,4815,2200,2,44,30,45,34,3670,3472,4013,3902,31,13,3])). % 175.23/175.40 cnf(4885,plain, % 175.23/175.40 (P2(f8(f4(a2,a1,a1),f4(a2,a1,a1)),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[190,47,19,477,62,3228,3676,363,3405,3594,334,163,4598,4137,4560,4815,2200,4777,2,44,30,45,34,3670,3472,4013,3902,31,13,3,12,15,14])). % 175.23/175.40 cnf(4911,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(x49111,f8(f8(a7,x49112),x49113)))), % 175.23/175.40 inference(scs_inference,[],[334,4420,2,44])). % 175.23/175.40 cnf(4915,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(f8(f8(a7,x49151),x49152),x49153))), % 175.23/175.40 inference(scs_inference,[],[334,4420,4579,2,44,30,45])). % 175.23/175.40 cnf(4923,plain, % 175.23/175.40 (~P3(f8(f4(a1,a1,a2),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[334,4420,4579,4870,2664,4063,2,44,30,45,34,3670,3472,4013])). % 175.23/175.40 cnf(4932,plain, % 175.23/175.40 (E(f8(f4(x49321,a1,x49322),a1),f4(x49321,a2,x49322))), % 175.23/175.40 inference(scs_inference,[],[190,19,62,3178,334,3645,2678,4420,4579,4870,2664,4063,2,44,30,45,34,3670,3472,4013,3902,31,13,3])). % 175.23/175.40 cnf(4935,plain, % 175.23/175.40 (E(x49351,f8(x49351,x49351))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(4936,plain, % 175.23/175.40 (P2(f3(a1,a1),f8(f3(a2,a2),f3(a2,a2)))), % 175.23/175.40 inference(scs_inference,[],[190,47,4935,19,62,332,3178,334,3364,3645,2678,4420,4579,4870,2664,4063,2,44,30,45,34,3670,3472,4013,3902,31,13,3,12,15])). % 175.23/175.40 cnf(4960,plain, % 175.23/175.40 (P3(f3(a7,a5),f8(x49601,a7))), % 175.23/175.40 inference(scs_inference,[],[3267,4767,2,44])). % 175.23/175.40 cnf(4964,plain, % 175.23/175.40 (P3(f3(a7,a5),f8(a7,x49641))), % 175.23/175.40 inference(scs_inference,[],[3267,4612,4767,2,44,30,45])). % 175.23/175.40 cnf(4983,plain, % 175.23/175.40 (E(x49831,f8(x49831,x49831))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(4988,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(a6,a6))), % 175.23/175.40 inference(scs_inference,[],[190,47,4983,19,52,62,3676,359,3177,3267,3594,3645,3397,919,4612,4923,2623,4685,4767,2,44,30,45,34,3670,3472,3902,31,13,3,12,15,14,35])). % 175.23/175.40 cnf(5015,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(x50151,a6))), % 175.23/175.40 inference(scs_inference,[],[3645,4824,2,44])). % 175.23/175.40 cnf(5022,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(a6,x50221))), % 175.23/175.40 inference(scs_inference,[],[3645,4960,141,4824,2,44,30,34,45])). % 175.23/175.40 cnf(5030,plain, % 175.23/175.40 (E(f8(f4(a1,x50301,x50302),a1),f4(a2,x50301,x50302))), % 175.23/175.40 inference(scs_inference,[],[190,19,62,3645,3184,4988,4960,141,4752,4824,2,44,30,34,45,31,13,3])). % 175.23/175.40 cnf(5033,plain, % 175.23/175.40 (E(x50331,f8(x50331,x50331))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5034,plain, % 175.23/175.40 (P2(f3(a2,a2),f8(f3(a1,a1),f3(a1,a1)))), % 175.23/175.40 inference(scs_inference,[],[190,47,5033,19,62,363,3645,3184,3445,4988,4960,141,4752,4824,2,44,30,34,45,31,13,3,12,15])). % 175.23/175.40 cnf(5035,plain, % 175.23/175.40 (E(x50351,f8(x50351,x50351))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5036,plain, % 175.23/175.40 (P2(f8(f3(a1,a1),f3(a1,a1)),f3(a2,a2))), % 175.23/175.40 inference(scs_inference,[],[190,47,5033,5035,19,62,363,3645,3184,3364,3445,4988,4960,141,4752,4824,2,44,30,34,45,31,13,3,12,15,14])). % 175.23/175.40 cnf(5067,plain, % 175.23/175.40 (E(f8(f3(a1,a1),f3(a1,a1)),f3(a2,a2))), % 175.23/175.40 inference(scs_inference,[],[517,4557,4964,2016,5036,5034,2,44,30,34,45,31])). % 175.23/175.40 cnf(5071,plain, % 175.23/175.40 (E(f8(f4(x50711,x50712,a1),a1),f4(x50711,x50712,a2))), % 175.23/175.40 inference(scs_inference,[],[190,19,3179,517,4557,4964,5015,2016,5036,5034,2,44,30,34,45,31,13,3])). % 175.23/175.40 cnf(5075,plain, % 175.23/175.40 (E(x50751,f8(x50751,x50751))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5083,plain, % 175.23/175.40 (P3(f4(a7,a5,a7),a5)), % 175.23/175.40 inference(scs_inference,[],[190,47,5075,19,52,3696,3179,4453,3397,517,4641,3494,495,3416,4654,4557,4964,5015,2016,5036,5034,2,44,30,34,45,31,13,3,12,15,14,35,46,40])). % 175.23/175.40 cnf(5107,plain, % 175.23/175.40 (E(x51071,f8(x51071,x51071))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5109,plain, % 175.23/175.40 (E(x51091,f8(x51091,x51091))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5110,plain, % 175.23/175.40 (P2(f8(f3(a2,a2),f3(a2,a2)),f3(a1,a1))), % 175.23/175.40 inference(scs_inference,[],[47,5107,5109,19,3373,844,3445,519,3706,5015,2060,5067,30,34,45,2,44,3,12,15,14])). % 175.23/175.40 cnf(5140,plain, % 175.23/175.40 (E(f8(f3(a1,a2),a1),f3(a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,3560,495,5022,2445,4879,30,34,45,2,44,3])). % 175.23/175.40 cnf(5175,plain, % 175.23/175.40 (E(f8(f4(a2,a1,a2),a1),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[19,4140,497,4744,2450,5140,30,2,45,44,34,3])). % 175.23/175.40 cnf(5178,plain, % 175.23/175.40 (E(x51781,f8(x51781,x51781))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5182,plain, % 175.23/175.40 (E(x51821,f8(x51821,x51821))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5183,plain, % 175.23/175.40 (P2(f8(f4(a2,a1,a2),f4(a2,a1,a2)),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[190,47,5178,5182,19,3645,3706,4140,497,344,4744,4748,2450,5140,30,2,45,44,34,3,15,13,12,14])). % 175.23/175.40 cnf(5206,plain, % 175.23/175.40 (P3(f3(a5,a2),f8(a5,x52061))), % 175.23/175.40 inference(scs_inference,[],[3826,4748,5175,30,2,45])). % 175.23/175.40 cnf(5220,plain, % 175.23/175.40 (E(x52201,f8(x52201,x52201))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5228,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(f8(x52281,a6),f8(x52281,a6)))), % 175.23/175.40 inference(scs_inference,[],[190,47,5220,19,52,4658,3267,3255,3176,3826,550,5015,4606,4748,2256,4801,2456,5175,30,2,45,44,34,4328,3,13,15,14,12,46,26,35])). % 175.23/175.40 cnf(5275,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(f8(a6,x52751),f8(a6,x52751)))), % 175.23/175.40 inference(scs_inference,[],[190,47,19,52,4658,3016,344,3920,3577,548,5022,4628,4801,3483,5206,2462,4932,2,30,45,44,34,3,15,13,12,14,46,35])). % 175.23/175.40 cnf(5348,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(f8(x53481,a6),x53482))), % 175.23/175.40 inference(scs_inference,[],[5015,5228,5030,2,30,45])). % 175.23/175.40 cnf(5350,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(x53501,f8(x53502,a6)))), % 175.23/175.40 inference(scs_inference,[],[5015,5228,5030,2,30,45,44])). % 175.23/175.40 cnf(5355,plain, % 175.23/175.40 (E(f8(f4(a1,a1,a1),a1),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[19,3505,5015,5228,4660,5030,2,30,45,44,34,3])). % 175.23/175.40 cnf(5397,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(f8(a6,x53971),x53972))), % 175.23/175.40 inference(scs_inference,[],[5022,5275,5355,2,30,45])). % 175.23/175.40 cnf(5399,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(x53991,f8(a6,x53992)))), % 175.23/175.40 inference(scs_inference,[],[5022,5275,5355,2,30,45,44])). % 175.23/175.40 cnf(5404,plain, % 175.23/175.40 (E(f8(f3(a2,a2),a1),f3(a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,5022,3503,5275,4846,5355,2,30,45,44,34,3])). % 175.23/175.40 cnf(5440,plain, % 175.23/175.40 (P3(f3(a5,f8(a2,a1)),f8(x54401,a5))), % 175.23/175.40 inference(scs_inference,[],[3831,5348,5404,2,45,30,44])). % 175.23/175.40 cnf(5451,plain, % 175.23/175.40 (E(f8(f3(a1,a1),a1),f3(a2,a2))), % 175.23/175.40 inference(scs_inference,[],[19,3831,3460,5348,5404,4725,2,45,30,44,34,4328,4325,4399,3])). % 175.23/175.40 cnf(5484,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(f8(x54841,f8(x54842,f8(a7,x54843))),x54844))), % 175.23/175.40 inference(scs_inference,[],[4744,5350,5451,2,30,45])). % 175.23/175.40 cnf(5486,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(x54861,f8(x54862,f8(x54863,f8(a7,x54864)))))), % 175.23/175.40 inference(scs_inference,[],[4744,5350,5451,2,30,45,44])). % 175.23/175.40 cnf(5494,plain, % 175.23/175.40 (P2(f3(a1,a1),f8(f8(f3(a2,a2),f3(a2,a2)),f8(f3(a2,a2),f3(a2,a2))))), % 175.23/175.40 inference(scs_inference,[],[47,19,3826,4453,4744,3226,4936,5350,5451,4714,2,30,45,44,34,3,12,15])). % 175.23/175.40 cnf(5495,plain, % 175.23/175.40 (E(x54951,f8(x54951,x54951))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5498,plain, % 175.23/175.40 (P2(f8(f8(f3(a2,a2),f3(a2,a2)),f8(f3(a2,a2),f3(a2,a2))),f3(a1,a1))), % 175.23/175.40 inference(scs_inference,[],[190,47,5495,19,3826,4453,4744,5110,3226,4936,5350,5440,5451,4714,2,30,45,44,34,3,12,15,13,14])). % 175.23/175.40 cnf(5524,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(x55241,f8(f8(x55242,a6),x55243)))), % 175.23/175.40 inference(scs_inference,[],[5348,5440,5071,2,30,44])). % 175.23/175.40 cnf(5526,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(f8(f8(x55261,a6),x55262),x55263))), % 175.23/175.40 inference(scs_inference,[],[5348,5440,5071,2,30,44,45])). % 175.23/175.40 cnf(5531,plain, % 175.23/175.40 (E(f8(f4(a2,a2,a1),a1),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5348,3784,5440,5071,122,2,30,44,45,34,3])). % 175.23/175.40 cnf(5534,plain, % 175.23/175.40 (E(x55341,f8(x55341,x55341))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5536,plain, % 175.23/175.40 (E(x55361,f8(x55361,x55361))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5543,plain, % 175.23/175.40 (E(f8(f4(a2,a1,a2),f4(a2,a1,a2)),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[190,47,5534,5536,19,3577,2256,5348,4936,3784,3476,5440,5397,5183,5071,122,2,30,44,45,34,3,15,12,13,14,26,31])). % 175.23/175.40 cnf(5573,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(x55731,f8(x55732,f8(x55733,a6))))), % 175.23/175.40 inference(scs_inference,[],[5350,5397,5531,2,30,44])). % 175.23/175.40 cnf(5575,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(f8(x55751,f8(x55752,a6)),x55753))), % 175.23/175.40 inference(scs_inference,[],[5350,5397,5531,2,30,44,45])). % 175.23/175.40 cnf(5577,plain, % 175.23/175.40 (E(f8(f4(a2,a2,a1),a1),f4(a2,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5350,4159,5397,5531,2,30,44,45,3])). % 175.23/175.40 cnf(5580,plain, % 175.23/175.40 (E(x55801,f8(x55801,x55801))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5590,plain, % 175.23/175.40 (P3(f3(a5,f8(a2,a1)),f8(f8(x55901,a5),f8(x55901,a5)))), % 175.23/175.40 inference(scs_inference,[],[190,47,5580,19,52,4658,2256,3350,5350,3476,4159,5440,3490,5397,5399,5498,5494,5531,2,30,44,45,3,15,13,12,14,26,31,35])). % 175.23/175.40 cnf(5609,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(x56091,f8(f8(x56092,f8(a7,x56093)),x56094)))), % 175.23/175.40 inference(scs_inference,[],[4748,5399,5543,2,30,44])). % 175.23/175.40 cnf(5611,plain, % 175.23/175.40 (P3(f4(a1,a1,a7),f8(f8(f8(x56111,f8(a7,x56112)),x56113),x56114))), % 175.23/175.40 inference(scs_inference,[],[4748,5399,5543,2,30,44,45])). % 175.23/175.40 cnf(5613,plain, % 175.23/175.40 (E(f8(f4(a2,a1,a1),a1),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,4748,3695,5399,5543,2,30,44,45,3])). % 175.23/175.40 cnf(5615,plain, % 175.23/175.40 (P2(f4(a1,a2,a2),f8(f4(a2,a1,a1),f4(a2,a1,a1)))), % 175.23/175.40 inference(scs_inference,[],[47,19,4748,3695,3521,5399,5543,2,30,44,45,3,15])). % 175.23/175.40 cnf(5616,plain, % 175.23/175.40 (E(x56161,f8(x56161,x56161))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5619,plain, % 175.23/175.40 (P2(f8(f3(a1,a2),f3(a1,a2)),f3(a2,a1))), % 175.23/175.40 inference(scs_inference,[],[190,47,5616,19,4748,3490,3695,3521,5399,5590,5543,2,30,44,45,3,15,13,14])). % 175.23/175.40 cnf(5649,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(f8(f8(a6,x56491),x56492),x56493))), % 175.23/175.40 inference(scs_inference,[],[5397,5590,5577,2,30,45])). % 175.23/175.40 cnf(5651,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(x56511,f8(f8(a6,x56512),x56513)))), % 175.23/175.40 inference(scs_inference,[],[5397,5590,5577,2,30,45,44])). % 175.23/175.40 cnf(5653,plain, % 175.23/175.40 (E(f8(f4(a1,a2,a1),a1),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5397,3532,5590,5577,2,30,45,44,3])). % 175.23/175.40 cnf(5691,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(f8(x56911,f8(a6,x56912)),x56913))), % 175.23/175.40 inference(scs_inference,[],[5399,4805,5613,2,30,45])). % 175.23/175.40 cnf(5693,plain, % 175.23/175.40 (P3(f3(a6,a2),f8(x56931,f8(x56932,f8(a6,x56933))))), % 175.23/175.40 inference(scs_inference,[],[5399,4805,5613,2,30,45,44])). % 175.23/175.40 cnf(5695,plain, % 175.23/175.40 (E(f8(f4(a2,a1,a2),a1),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,5399,3720,4805,5613,2,30,45,44,3])). % 175.23/175.40 cnf(5725,plain, % 175.23/175.40 (P3(f3(a5,f8(a2,a1)),f8(f8(f8(x57251,a5),f8(x57251,a5)),x57252))), % 175.23/175.40 inference(scs_inference,[],[5590,4858,5653,2,30,45])). % 175.23/175.40 cnf(5727,plain, % 175.23/175.40 (P3(f3(a5,f8(a2,a1)),f8(x57271,f8(f8(x57272,a5),f8(x57272,a5))))), % 175.23/175.40 inference(scs_inference,[],[5590,4858,5653,2,30,45,44])). % 175.23/175.40 cnf(5729,plain, % 175.23/175.40 (E(f8(f4(a1,a2,a1),a1),f4(a2,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5590,3462,4858,5653,2,30,45,44,3])). % 175.23/175.40 cnf(5772,plain, % 175.23/175.40 (E(x57721,f8(x57721,x57721))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5773,plain, % 175.23/175.40 (P2(f4(a1,a2,a2),f8(f8(f4(a2,a1,a1),f4(a2,a1,a1)),f8(f4(a2,a1,a1),f4(a2,a1,a1))))), % 175.23/175.40 inference(scs_inference,[],[47,5772,19,4801,4885,3530,5615,4862,5695,2,45,30,44,3,14,15])). % 175.23/175.40 cnf(5802,plain, % 175.23/175.40 (E(f8(f4(a2,a1,a1),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[19,4805,3562,4911,5729,2,45,30,44,3])). % 175.23/175.40 cnf(5872,plain, % 175.23/175.40 (E(f8(f4(a1,a1,a1),a1),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,4862,4094,5524,5802,2,45,30,44,3])). % 175.23/175.40 cnf(5876,plain, % 175.23/175.40 (P2(f4(a2,a1,a1),f8(f8(f4(a1,a2,a2),f4(a1,a2,a2)),f8(f4(a1,a2,a2),f4(a1,a2,a2))))), % 175.23/175.40 inference(scs_inference,[],[190,47,19,4862,4094,4770,5524,5526,5802,2,45,30,44,3,13,15])). % 175.23/175.40 cnf(5955,plain, % 175.23/175.40 (E(f8(f4(a1,a2,a2),a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,4915,3898,5573,5872,2,45,30,44,3])). % 175.23/175.40 cnf(5957,plain, % 175.23/175.40 (P2(f8(f4(a1,a2,a1),f4(a1,a2,a1)),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[47,19,4915,3543,3898,5573,5872,2,45,30,44,3,14])). % 175.23/175.40 cnf(5992,plain, % 175.23/175.40 (E(f8(f3(f8(x59921,x59921),x59922),a1),f3(x59921,x59922))), % 175.23/175.40 inference(scs_inference,[],[19,5524,843,5575,5955,2,45,44,30,3])). % 175.23/175.40 cnf(5995,plain, % 175.23/175.40 (E(x59951,f8(x59951,x59951))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(5998,plain, % 175.23/175.40 (P2(f4(a1,a1,a2),f8(f4(a2,a2,a2),f4(a2,a2,a2)))), % 175.23/175.40 inference(scs_inference,[],[190,47,5995,19,5524,5773,843,3551,5575,5649,5955,2,45,44,30,3,14,13,15])). % 175.23/175.40 cnf(6031,plain, % 175.23/175.40 (E(f8(f3(a2,a1),a1),f3(a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5526,3793,5649,5992,2,45,44,30,3])). % 175.23/175.40 cnf(6033,plain, % 175.23/175.40 (P2(f8(f4(a1,a1,a2),f4(a1,a1,a2)),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[47,19,5526,3551,3793,5649,5992,2,45,44,30,3,14])). % 175.23/175.40 cnf(6070,plain, % 175.23/175.40 (E(f8(f4(a1,a1,a2),a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,5573,3968,5651,6031,2,45,44,30,3])). % 175.23/175.40 cnf(6111,plain, % 175.23/175.40 (E(f8(f4(a2,a1,a2),a1),f4(a2,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,5575,4125,5691,6070,2,45,44,30,3])). % 175.23/175.40 cnf(6148,plain, % 175.23/175.40 (E(f8(f4(a1,a1,a2),a1),f4(a1,a2,a1))), % 175.23/175.40 inference(scs_inference,[],[19,5649,3656,5693,6111,2,45,44,30,3])). % 175.23/175.40 cnf(6151,plain, % 175.23/175.40 (E(x61511,f8(x61511,x61511))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6154,plain, % 175.23/175.40 (P2(f4(a2,a2,a2),f8(f4(a1,a1,a2),f4(a1,a1,a2)))), % 175.23/175.40 inference(scs_inference,[],[190,47,6151,19,5649,5876,3576,3656,5693,5725,6111,2,45,44,30,3,14,13,15])). % 175.23/175.40 cnf(6189,plain, % 175.23/175.40 (E(f8(f4(a2,a2,a2),a1),f4(a2,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,5651,3945,5725,6148,2,45,44,30,3])). % 175.23/175.40 cnf(6193,plain, % 175.23/175.40 (P2(f8(f4(a2,a2,a2),f4(a2,a2,a2)),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[190,47,19,5651,3576,3945,5725,5727,6148,2,45,44,30,3,13,14])). % 175.23/175.40 cnf(6225,plain, % 175.23/175.40 (E(f8(f4(a2,a2,a2),a1),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5691,3755,5727,6189,2,45,44,30,3])). % 175.23/175.40 cnf(6229,plain, % 175.23/175.40 (P2(f8(f8(f3(a1,a2),f3(a1,a2)),f8(f3(a1,a2),f3(a1,a2))),f3(a2,a1))), % 175.23/175.40 inference(scs_inference,[],[190,47,19,5691,5619,3755,5727,5484,6189,2,45,44,30,3,13,14])). % 175.23/175.40 cnf(6274,plain, % 175.23/175.40 (E(f8(f4(a2,a2,a1),a1),f4(a1,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5693,3893,5484,6225,2,45,44,30,3])). % 175.23/175.40 cnf(6310,plain, % 175.23/175.40 (E(f8(f4(a1,a1,a2),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5725,3604,5486,6274,2,45,44,30,3])). % 175.23/175.40 cnf(6312,plain, % 175.23/175.40 (P2(f8(f8(f4(a1,a1,a2),f4(a1,a1,a2)),f8(f4(a1,a1,a2),f4(a1,a1,a2))),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[47,19,5725,6033,3604,5486,6274,2,45,44,30,3,14])). % 175.23/175.40 cnf(6313,plain, % 175.23/175.40 (E(x63131,f8(x63131,x63131))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6317,plain, % 175.23/175.40 (E(x63171,f8(x63171,x63171))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6318,plain, % 175.23/175.40 (P2(f4(a2,a2,a2),f8(f8(f4(a1,a1,a2),f4(a1,a1,a2)),f8(f4(a1,a1,a2),f4(a1,a1,a2))))), % 175.23/175.40 inference(scs_inference,[],[190,47,6313,6317,19,5573,5725,6033,6154,3604,5486,5609,6274,2,45,44,30,3,14,13,12,15])). % 175.23/175.40 cnf(6324,plain, % 175.23/175.40 (P3(f3(a5,a2),f8(f8(a5,x63241),f8(a5,x63241)))), % 175.23/175.40 inference(scs_inference,[],[190,47,6313,6317,19,52,2256,5573,5725,6033,6154,5206,3604,5486,6193,5998,5609,6274,2,45,44,30,3,14,13,12,15,31,26,35])). % 175.23/175.40 cnf(6362,plain, % 175.23/175.40 (E(f8(f4(a2,a2,a1),a1),f4(a1,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,5727,3861,5609,6310,2,45,44,30,3])). % 175.23/175.40 cnf(6394,plain, % 175.23/175.40 (P3(f3(a5,a2),f8(f8(a5,x63941),x63942))), % 175.23/175.40 inference(scs_inference,[],[5206,6362,2,45])). % 175.23/175.40 cnf(6396,plain, % 175.23/175.40 (P3(f3(a5,a2),f8(x63961,f8(a5,x63962)))), % 175.23/175.40 inference(scs_inference,[],[5206,6362,2,45,44])). % 175.23/175.40 cnf(6400,plain, % 175.23/175.40 (E(f8(f4(a2,a1,a1),a1),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,5206,3609,6324,6362,2,45,44,30,3])). % 175.23/175.40 cnf(6403,plain, % 175.23/175.40 (E(x64031,f8(x64031,x64031))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6405,plain, % 175.23/175.40 (E(x64051,f8(x64051,x64051))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6408,plain, % 175.23/175.40 (P2(f4(a1,a1,a2),f8(f4(a1,a2,a1),f4(a1,a2,a1)))), % 175.23/175.40 inference(scs_inference,[],[190,47,6403,6405,19,5649,5206,6193,3638,3609,6324,5611,6362,2,45,44,30,3,14,12,13,15])). % 175.23/175.40 cnf(6433,plain, % 175.23/175.40 (P3(f3(a5,f8(a2,a1)),f8(f8(x64331,a5),x64332))), % 175.23/175.40 inference(scs_inference,[],[5440,6400,2,45])). % 175.23/175.40 cnf(6442,plain, % 175.23/175.40 (E(x64421,f8(x64421,x64421))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6444,plain, % 175.23/175.40 (E(x64441,f8(x64441,x64441))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6449,plain, % 175.23/175.40 (E(f8(f4(a1,a2,a1),f4(a1,a2,a1)),f4(a1,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[190,47,6442,6444,19,5651,3638,5440,6229,4176,5611,6394,5957,6408,6400,2,45,30,44,3,14,12,13,15,31])). % 175.23/175.40 cnf(6475,plain, % 175.23/175.40 (E(f8(f4(a1,a2,a2),a1),f4(a2,a1,a2))), % 175.23/175.40 inference(scs_inference,[],[19,3233,4165,6394,6449,2,45,30,44,3])). % 175.23/175.40 cnf(6515,plain, % 175.23/175.40 (E(f8(f4(a1,a1,a1),a1),f4(a2,a2,a2))), % 175.23/175.40 inference(scs_inference,[],[19,3387,3189,6396,6475,2,45,30,44,3])). % 175.23/175.40 cnf(6520,plain, % 175.23/175.40 (E(x65201,f8(x65201,x65201))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6522,plain, % 175.23/175.40 (E(x65221,f8(x65221,x65221))), % 175.23/175.40 inference(rename_variables,[],[47])). % 175.23/175.40 cnf(6536,plain, % 175.23/175.40 (P3(f4(a1,a2,f8(a5,x65361)),f8(a5,x65361))), % 175.23/175.40 inference(scs_inference,[],[190,47,6520,6522,48,19,52,77,2256,5693,3985,3751,3387,3189,6394,3852,6396,4476,6312,6318,3887,6433,6475,2,45,30,44,3,13,12,14,15,31,26,35,46,37,40])). % 175.23/175.40 cnf(6560,plain, % 175.23/175.40 (E(f8(f4(a1,a2,a2),a1),f4(a1,a1,a1))), % 175.23/175.40 inference(scs_inference,[],[19,6394,3873,6433,6536,6515,2,45,44,30,4350,3])). % 175.23/175.40 cnf(6598,plain, % 175.23/175.40 (~E(f3(a5,a2),f4(a7,a1,a5))), % 175.23/175.40 inference(scs_inference,[],[47,19,6394,6396,6318,4598,6536,2361,6560,2,45,44,30,3,14,12])). % 175.23/175.40 cnf(6909,plain, % 175.23/175.40 ($false), % 175.23/175.40 inference(scs_inference,[],[18,3227,4658,3233,4654,4250,5083,6598,4351,2,45,30,44,3,12,35]), % 175.23/175.40 ['proof']). % 175.23/175.40 % SZS output end Proof % 175.23/175.40 % Total time :174.640000s %------------------------------------------------------------------------------