%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU125+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 : n021.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 221.95s 222.04s % Output : CNFRefutation 222.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SEU125+1 : TPTP v8.2.0. Released v3.3.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n021.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 21 14:56:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.59 start to proof:theBenchmark % 221.95/222.02 %------------------------------------------- % 221.95/222.02 % File :CSE---1.7 % 221.95/222.02 % Problem :theBenchmark % 221.95/222.02 % Transform :cnf % 221.95/222.02 % Format :tptp:raw % 221.95/222.02 % Command :java -jar mcs_scs.jar %d %s % 221.95/222.02 % 221.95/222.02 % Result :Theorem 221.270000s % 221.95/222.02 % Output :CNFRefutation 221.270000s % 221.95/222.02 %------------------------------------------- % 221.95/222.04 %------------------------------------------------------------------------------ % 221.95/222.04 % File : SEU125+1 : TPTP v8.2.0. Released v3.3.0. % 221.95/222.04 % Domain : Set theory % 221.95/222.04 % Problem : MPTP bushy problem t8_xboole_1 % 221.95/222.04 % Version : [Urb07] axioms : Especial. % 221.95/222.04 % English : % 221.95/222.04 % 221.95/222.04 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 221.95/222.04 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 221.95/222.04 % Source : [Urb07] % 221.95/222.04 % Names : bushy-t8_xboole_1 [Urb07] % 221.95/222.04 % 221.95/222.04 % Status : Theorem % 221.95/222.04 % Rating : 0.25 v8.2.0, 0.28 v7.4.0, 0.17 v7.3.0, 0.21 v7.2.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.32 v6.1.0, 0.40 v6.0.0, 0.30 v5.5.0, 0.41 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.30 v5.1.0, 0.33 v5.0.0, 0.38 v4.1.0, 0.39 v4.0.0, 0.42 v3.7.0, 0.40 v3.5.0, 0.42 v3.3.0 % 221.95/222.04 % Syntax : Number of formulae : 18 ( 9 unt; 0 def) % 221.95/222.04 % Number of atoms : 32 ( 6 equ) % 221.95/222.04 % Maximal formula atoms : 4 ( 1 avg) % 221.95/222.04 % Number of connectives : 23 ( 9 ~; 1 |; 4 &) % 221.95/222.04 % ( 3 <=>; 6 =>; 0 <=; 0 <~>) % 221.95/222.04 % Maximal formula depth : 8 ( 4 avg) % 221.95/222.04 % Maximal term depth : 2 ( 1 avg) % 221.95/222.04 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 221.95/222.04 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty) % 221.95/222.04 % Number of variables : 30 ( 28 !; 2 ?) % 221.95/222.04 % SPC : FOF_THM_RFO_SEQ % 221.95/222.04 % 221.95/222.04 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 221.95/222.04 % library, www.mizar.org % 221.95/222.04 %------------------------------------------------------------------------------ % 221.95/222.04 fof(antisymmetry_r2_hidden,axiom, % 221.95/222.04 ! [A,B] : % 221.95/222.04 ( in(A,B) % 221.95/222.04 => ~ in(B,A) ) ). % 221.95/222.04 % 221.95/222.04 fof(commutativity_k2_xboole_0,axiom, % 221.95/222.04 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 221.95/222.04 % 221.95/222.04 fof(d2_xboole_0,axiom, % 221.95/222.04 ! [A,B,C] : % 221.95/222.04 ( C = set_union2(A,B) % 221.95/222.04 <=> ! [D] : % 221.95/222.04 ( in(D,C) % 221.95/222.04 <=> ( in(D,A) % 221.95/222.04 | in(D,B) ) ) ) ). % 221.95/222.04 % 221.95/222.04 fof(d3_tarski,axiom, % 221.95/222.04 ! [A,B] : % 221.95/222.04 ( subset(A,B) % 221.95/222.04 <=> ! [C] : % 221.95/222.04 ( in(C,A) % 221.95/222.04 => in(C,B) ) ) ). % 221.95/222.04 % 221.95/222.04 fof(dt_k1_xboole_0,axiom, % 221.95/222.04 $true ). % 221.95/222.04 % 221.95/222.04 fof(dt_k2_xboole_0,axiom, % 221.95/222.04 $true ). % 221.95/222.04 % 221.95/222.04 fof(fc1_xboole_0,axiom, % 221.95/222.04 empty(empty_set) ). % 221.95/222.04 % 221.95/222.04 fof(fc2_xboole_0,axiom, % 221.95/222.04 ! [A,B] : % 221.95/222.04 ( ~ empty(A) % 221.95/222.04 => ~ empty(set_union2(A,B)) ) ). % 221.95/222.04 % 221.95/222.04 fof(fc3_xboole_0,axiom, % 221.95/222.04 ! [A,B] : % 221.95/222.04 ( ~ empty(A) % 221.95/222.04 => ~ empty(set_union2(B,A)) ) ). % 221.95/222.04 % 221.95/222.04 fof(idempotence_k2_xboole_0,axiom, % 221.95/222.04 ! [A,B] : set_union2(A,A) = A ). % 221.95/222.04 % 221.95/222.04 fof(rc1_xboole_0,axiom, % 221.95/222.04 ? [A] : empty(A) ). % 221.95/222.04 % 221.95/222.04 fof(rc2_xboole_0,axiom, % 221.95/222.04 ? [A] : ~ empty(A) ). % 221.95/222.04 % 221.95/222.04 fof(reflexivity_r1_tarski,axiom, % 221.95/222.04 ! [A,B] : subset(A,A) ). % 221.95/222.04 % 221.95/222.04 fof(t1_boole,axiom, % 221.95/222.04 ! [A] : set_union2(A,empty_set) = A ). % 221.95/222.04 % 221.95/222.04 fof(t6_boole,axiom, % 221.95/222.04 ! [A] : % 221.95/222.04 ( empty(A) % 221.95/222.04 => A = empty_set ) ). % 221.95/222.04 % 221.95/222.04 fof(t7_boole,axiom, % 221.95/222.04 ! [A,B] : % 221.95/222.04 ~ ( in(A,B) % 221.95/222.04 & empty(B) ) ). % 221.95/222.04 % 221.95/222.04 fof(t8_boole,axiom, % 221.95/222.04 ! [A,B] : % 221.95/222.04 ~ ( empty(A) % 221.95/222.04 & A != B % 221.95/222.04 & empty(B) ) ). % 221.95/222.04 % 221.95/222.04 fof(t8_xboole_1,conjecture, % 221.95/222.04 ! [A,B,C] : % 221.95/222.04 ( ( subset(A,B) % 221.95/222.04 & subset(C,B) ) % 221.95/222.04 => subset(set_union2(A,C),B) ) ). % 221.95/222.04 % 221.95/222.04 %------------------------------------------------------------------------------ % 221.95/222.04 %------------------------------------------- % 221.95/222.04 % Proof found % 221.95/222.04 % SZS status Theorem for theBenchmark % 221.95/222.04 % SZS output start Proof % 222.01/222.06 %ClaNum:40(EqnAxiom:15) % 222.01/222.06 %VarNum:106(SingletonVarNum:44) % 222.01/222.06 %MaxLitNum:4 % 222.01/222.06 %MaxfuncDepth:1 % 222.01/222.06 %SharedTerms:13 % 222.01/222.06 %goalClause: 18 19 25 % 222.01/222.06 %singleGoalClaCount:3 % 222.01/222.06 [16]P1(a1) % 222.01/222.06 [17]P1(a2) % 222.01/222.06 [18]P2(a5,a7) % 222.01/222.06 [19]P2(a8,a7) % 222.01/222.06 [24]~P1(a6) % 222.01/222.06 [25]~P2(f9(a5,a8),a7) % 222.01/222.06 [21]P2(x211,x211) % 222.01/222.06 [20]E(f9(x201,a1),x201) % 222.01/222.06 [22]E(f9(x221,x221),x221) % 222.01/222.06 [23]E(f9(x231,x232),f9(x232,x231)) % 222.01/222.06 [26]~P1(x261)+E(x261,a1) % 222.01/222.06 [28]~P1(x281)+~P3(x282,x281) % 222.01/222.06 [29]~P3(x292,x291)+~P3(x291,x292) % 222.01/222.06 [30]P1(x301)+~P1(f9(x302,x301)) % 222.01/222.06 [31]P1(x311)+~P1(f9(x311,x312)) % 222.01/222.06 [32]P2(x321,x322)+P3(f3(x321,x322),x321) % 222.01/222.06 [37]P2(x371,x372)+~P3(f3(x371,x372),x372) % 222.01/222.06 [27]~P1(x272)+~P1(x271)+E(x271,x272) % 222.01/222.06 [33]~P2(x333,x332)+P3(x331,x332)+~P3(x331,x333) % 222.01/222.06 [39]~P3(f4(x392,x393,x391),x391)+~P3(f4(x392,x393,x391),x393)+E(x391,f9(x392,x393)) % 222.01/222.06 [40]~P3(f4(x402,x403,x401),x401)+~P3(f4(x402,x403,x401),x402)+E(x401,f9(x402,x403)) % 222.01/222.06 [34]~P3(x341,x344)+P3(x341,x342)+~E(x342,f9(x343,x344)) % 222.01/222.06 [35]~P3(x351,x353)+P3(x351,x352)+~E(x352,f9(x353,x354)) % 222.01/222.06 [38]P3(f4(x382,x383,x381),x381)+P3(f4(x382,x383,x381),x383)+P3(f4(x382,x383,x381),x382)+E(x381,f9(x382,x383)) % 222.01/222.06 [36]~P3(x361,x364)+P3(x361,x362)+P3(x361,x363)+~E(x364,f9(x363,x362)) % 222.01/222.06 %EqnAxiom % 222.01/222.06 [1]E(x11,x11) % 222.01/222.06 [2]E(x22,x21)+~E(x21,x22) % 222.01/222.06 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 222.01/222.06 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43)) % 222.01/222.06 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52)) % 222.01/222.06 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 222.01/222.06 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 222.01/222.06 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 222.01/222.06 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 222.01/222.06 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 222.01/222.06 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 222.01/222.06 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 222.01/222.06 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 222.01/222.06 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 222.01/222.06 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 222.01/222.06 % 222.01/222.06 %------------------------------------------- % 222.01/222.09 cnf(41,plain, % 222.01/222.09 (~P3(x411,x412)+P3(x411,f9(x413,x412))), % 222.01/222.09 inference(equality_inference,[],[34])). % 222.01/222.09 cnf(42,plain, % 222.01/222.09 (~P3(x421,x422)+P3(x421,f9(x422,x423))), % 222.01/222.09 inference(equality_inference,[],[35])). % 222.01/222.09 cnf(43,plain, % 222.01/222.09 (~P3(x431,f9(x432,x433))+P3(x431,x433)+P3(x431,x432)), % 222.01/222.09 inference(equality_inference,[],[36])). % 222.01/222.09 cnf(44,plain, % 222.01/222.09 (~P3(x441,a1)), % 222.01/222.10 inference(scs_inference,[],[16,28])). % 222.01/222.10 cnf(46,plain, % 222.01/222.10 (E(x461,f9(x461,x461))), % 222.01/222.10 inference(scs_inference,[],[22,16,28,2])). % 222.01/222.10 cnf(47,plain, % 222.01/222.10 (~E(a5,f9(a5,a8))), % 222.01/222.10 inference(scs_inference,[],[18,25,22,16,28,2,14])). % 222.01/222.10 cnf(48,plain, % 222.01/222.10 (P2(a5,f9(a7,a7))), % 222.01/222.10 inference(scs_inference,[],[18,25,22,16,28,2,14,15])). % 222.01/222.10 cnf(49,plain, % 222.01/222.10 (~P3(f4(a5,a8,a5),a5)), % 222.01/222.10 inference(scs_inference,[],[18,25,22,16,28,2,14,15,40])). % 222.01/222.10 cnf(51,plain, % 222.01/222.10 (~P3(x511,f9(a1,a1))), % 222.01/222.10 inference(scs_inference,[],[18,25,22,16,28,2,14,15,40,43])). % 222.01/222.10 cnf(53,plain, % 222.01/222.10 (~E(a5,f9(a8,a5))), % 222.01/222.10 inference(scs_inference,[],[18,25,22,23,16,28,2,14,15,40,43,3])). % 222.01/222.10 cnf(56,plain, % 222.01/222.10 (E(f9(x561,a1),x561)), % 222.01/222.10 inference(rename_variables,[],[20])). % 222.01/222.10 cnf(57,plain, % 222.01/222.10 (~P3(x571,f9(f9(a1,a1),a1))), % 222.01/222.10 inference(scs_inference,[],[18,25,22,23,20,56,16,24,28,2,14,15,40,43,3,11,36])). % 222.01/222.10 cnf(58,plain, % 222.01/222.10 (E(f9(x581,a1),x581)), % 222.01/222.10 inference(rename_variables,[],[20])). % 222.01/222.10 cnf(60,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),a8)), % 222.01/222.10 inference(scs_inference,[],[18,25,22,23,20,56,16,24,28,2,14,15,40,43,3,11,36,38])). % 222.01/222.10 cnf(62,plain, % 222.01/222.10 (P2(a1,x621)), % 222.01/222.10 inference(scs_inference,[],[18,25,22,23,20,56,16,24,28,2,14,15,40,43,3,11,36,38,32])). % 222.01/222.10 cnf(64,plain, % 222.01/222.10 (~P3(a8,f4(a5,a8,a5))), % 222.01/222.10 inference(scs_inference,[],[18,25,22,23,20,56,16,24,28,2,14,15,40,43,3,11,36,38,32,29])). % 222.01/222.10 cnf(66,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(x661,a8))), % 222.01/222.10 inference(scs_inference,[],[18,25,22,23,20,56,16,24,28,2,14,15,40,43,3,11,36,38,32,29,41])). % 222.01/222.10 cnf(68,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(a8,x681))), % 222.01/222.10 inference(scs_inference,[],[18,25,22,23,20,56,16,24,28,2,14,15,40,43,3,11,36,38,32,29,41,42])). % 222.01/222.10 cnf(70,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),a7)), % 222.01/222.10 inference(scs_inference,[],[18,19,25,22,23,20,56,16,24,28,2,14,15,40,43,3,11,36,38,32,29,41,42,33])). % 222.01/222.10 cnf(75,plain, % 222.01/222.10 (E(f9(x751,a1),x751)), % 222.01/222.10 inference(rename_variables,[],[20])). % 222.01/222.10 cnf(80,plain, % 222.01/222.10 (~P3(f4(a8,a5,a5),a5)), % 222.01/222.10 inference(scs_inference,[],[18,19,25,22,23,20,56,58,75,16,24,28,2,14,15,40,43,3,11,36,38,32,29,41,42,33,27,34,35,39])). % 222.01/222.10 cnf(83,plain, % 222.01/222.10 (P3(x831,a8)+~E(f4(a5,a8,a5),x831)), % 222.01/222.10 inference(scs_inference,[],[18,19,25,22,23,20,56,58,75,16,24,28,2,14,15,40,43,3,11,36,38,32,29,41,42,33,27,34,35,39,13,12])). % 222.01/222.10 cnf(85,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(x851,a7))), % 222.01/222.10 inference(scs_inference,[],[70,41])). % 222.01/222.10 cnf(89,plain, % 222.01/222.10 (P2(f9(a1,a1),x891)), % 222.01/222.10 inference(scs_inference,[],[70,51,41,29,32])). % 222.01/222.10 cnf(92,plain, % 222.01/222.10 (~P3(x921,a2)), % 222.01/222.10 inference(scs_inference,[],[70,51,17,41,29,32,28])). % 222.01/222.10 cnf(94,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(a7,x941))), % 222.01/222.10 inference(scs_inference,[],[70,51,17,41,29,32,28,42])). % 222.01/222.10 cnf(96,plain, % 222.01/222.10 (E(x961,f9(x961,a1))), % 222.01/222.10 inference(scs_inference,[],[70,51,20,17,41,29,32,28,42,2])). % 222.01/222.10 cnf(97,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(f9(x971,a7),f9(x971,a7)))), % 222.01/222.10 inference(scs_inference,[],[70,51,22,20,17,41,29,32,28,42,2,34])). % 222.01/222.10 cnf(98,plain, % 222.01/222.10 (E(f9(x981,x981),x981)), % 222.01/222.10 inference(rename_variables,[],[22])). % 222.01/222.10 cnf(100,plain, % 222.01/222.10 (~P3(f4(a5,a8,a5),f9(a5,a5))), % 222.01/222.10 inference(scs_inference,[],[70,51,49,22,20,17,41,29,32,28,42,2,34,43])). % 222.01/222.10 cnf(102,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(f9(a7,x1021),f9(a7,x1021)))), % 222.01/222.10 inference(scs_inference,[],[70,51,49,22,98,20,17,41,29,32,28,42,2,34,43,35])). % 222.01/222.10 cnf(103,plain, % 222.01/222.10 (E(f9(x1031,x1031),x1031)), % 222.01/222.10 inference(rename_variables,[],[22])). % 222.01/222.10 cnf(105,plain, % 222.01/222.10 (P3(f9(f4(a5,a8,a5),f4(a5,a8,a5)),a7)), % 222.01/222.10 inference(scs_inference,[],[70,46,51,49,22,98,20,17,41,29,32,28,42,2,34,43,35,12])). % 222.01/222.10 cnf(106,plain, % 222.01/222.10 (E(x1061,f9(x1061,x1061))), % 222.01/222.10 inference(rename_variables,[],[46])). % 222.01/222.10 cnf(107,plain, % 222.01/222.10 (P1(f9(a1,a1))), % 222.01/222.10 inference(scs_inference,[],[70,46,106,51,49,22,98,20,16,17,41,29,32,28,42,2,34,43,35,12,11])). % 222.01/222.10 cnf(108,plain, % 222.01/222.10 (E(x1081,f9(x1081,x1081))), % 222.01/222.10 inference(rename_variables,[],[46])). % 222.01/222.10 cnf(109,plain, % 222.01/222.10 (~E(a7,f9(f9(a1,a1),a1))), % 222.01/222.10 inference(scs_inference,[],[70,46,106,57,51,49,22,98,20,16,17,41,29,32,28,42,2,34,43,35,12,11,13])). % 222.01/222.10 cnf(113,plain, % 222.01/222.10 (P2(a8,f9(a7,a7))), % 222.01/222.10 inference(scs_inference,[],[19,70,47,46,106,108,57,51,49,22,98,103,20,16,17,41,29,32,28,42,2,34,43,35,12,11,13,3,15])). % 222.01/222.10 cnf(115,plain, % 222.01/222.10 (~E(a8,f9(a5,a8))), % 222.01/222.10 inference(scs_inference,[],[19,25,70,47,46,106,108,57,51,49,22,98,103,20,16,17,41,29,32,28,42,2,34,43,35,12,11,13,3,15,14])). % 222.01/222.10 cnf(116,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),a8)), % 222.01/222.10 inference(scs_inference,[],[19,25,70,47,46,106,108,57,51,49,53,80,22,98,103,20,16,17,41,29,32,28,42,2,34,43,35,12,11,13,3,15,14,38])). % 222.01/222.10 cnf(120,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),a7)), % 222.01/222.10 inference(scs_inference,[],[19,25,70,47,46,106,108,57,51,49,53,80,22,98,103,20,16,17,41,29,32,28,42,2,34,43,35,12,11,13,3,15,14,38,27,33])). % 222.01/222.10 cnf(122,plain, % 222.01/222.10 (~P3(f4(a5,a8,a8),a8)), % 222.01/222.10 inference(scs_inference,[],[19,25,70,47,46,106,108,57,51,49,53,80,22,98,103,20,16,17,41,29,32,28,42,2,34,43,35,12,11,13,3,15,14,38,27,33,39])). % 222.01/222.10 cnf(128,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(x1281,a7))), % 222.01/222.10 inference(scs_inference,[],[120,41])). % 222.01/222.10 cnf(130,plain, % 222.01/222.10 (P2(a2,x1301)), % 222.01/222.10 inference(scs_inference,[],[120,92,41,32])). % 222.01/222.10 cnf(133,plain, % 222.01/222.10 (~P3(a7,f4(a8,a5,a5))), % 222.01/222.10 inference(scs_inference,[],[120,92,41,32,29])). % 222.01/222.10 cnf(135,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(a7,x1351))), % 222.01/222.10 inference(scs_inference,[],[120,92,41,32,29,42])). % 222.01/222.10 cnf(138,plain, % 222.01/222.10 (E(f9(x1381,a1),x1381)), % 222.01/222.10 inference(rename_variables,[],[20])). % 222.01/222.10 cnf(143,plain, % 222.01/222.10 (E(f9(x1431,a1),x1431)), % 222.01/222.10 inference(rename_variables,[],[20])). % 222.01/222.10 cnf(145,plain, % 222.01/222.10 (P3(f9(f4(a8,a5,a5),a1),a7)), % 222.01/222.10 inference(scs_inference,[],[120,20,138,96,100,92,41,32,29,42,34,43,35,12])). % 222.01/222.10 cnf(146,plain, % 222.01/222.10 (E(x1461,f9(x1461,a1))), % 222.01/222.10 inference(rename_variables,[],[96])). % 222.01/222.10 cnf(151,plain, % 222.01/222.10 (P2(a5,f9(a7,a1))), % 222.01/222.10 inference(scs_inference,[],[18,47,120,20,138,143,96,146,100,44,92,41,32,29,42,34,43,35,12,3,13,15])). % 222.01/222.10 cnf(153,plain, % 222.01/222.10 (~E(a7,f9(a5,a8))), % 222.01/222.10 inference(scs_inference,[],[18,25,47,21,120,20,138,143,96,146,100,44,92,41,32,29,42,34,43,35,12,3,13,15,14])). % 222.01/222.10 cnf(155,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),a5)), % 222.01/222.10 inference(scs_inference,[],[18,25,47,21,120,115,20,138,143,96,146,100,44,92,122,41,32,29,42,34,43,35,12,3,13,15,14,38])). % 222.01/222.10 cnf(157,plain, % 222.01/222.10 (~P1(a7)), % 222.01/222.10 inference(scs_inference,[],[18,25,47,21,120,115,20,138,143,96,146,100,44,92,122,41,32,29,42,34,43,35,12,3,13,15,14,38,26])). % 222.01/222.10 cnf(161,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),a7)), % 222.01/222.10 inference(scs_inference,[],[18,25,47,21,120,115,20,138,143,96,146,100,44,92,122,41,32,29,42,34,43,35,12,3,13,15,14,38,26,27,33])). % 222.01/222.10 cnf(167,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(x1671,a7))), % 222.01/222.10 inference(scs_inference,[],[161,41])). % 222.01/222.10 cnf(169,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(a7,x1691))), % 222.01/222.10 inference(scs_inference,[],[161,41,42])). % 222.01/222.10 cnf(171,plain, % 222.01/222.10 (~P3(a7,f4(a5,a8,a8))), % 222.01/222.10 inference(scs_inference,[],[161,41,42,29])). % 222.01/222.10 cnf(173,plain, % 222.01/222.10 (~P3(f4(a5,a8,a8),f9(a8,a8))), % 222.01/222.10 inference(scs_inference,[],[161,122,41,42,29,43])). % 222.01/222.10 cnf(176,plain, % 222.01/222.10 (E(f9(x1761,x1761),x1761)), % 222.01/222.10 inference(rename_variables,[],[22])). % 222.01/222.10 cnf(181,plain, % 222.01/222.10 (P3(f9(f4(a5,a8,a8),f4(a5,a8,a8)),a7)), % 222.01/222.10 inference(scs_inference,[],[161,46,22,176,122,41,42,29,43,34,35,12])). % 222.01/222.10 cnf(183,plain, % 222.01/222.10 (~E(a7,a8)), % 222.01/222.10 inference(scs_inference,[],[161,46,22,176,122,41,42,29,43,34,35,12,13])). % 222.01/222.10 cnf(184,plain, % 222.01/222.10 (~E(a7,f9(a1,a1))), % 222.01/222.10 inference(scs_inference,[],[161,46,22,176,122,109,96,41,42,29,43,34,35,12,13,3])). % 222.01/222.10 cnf(186,plain, % 222.01/222.10 (P2(a5,f9(a1,a7))), % 222.01/222.10 inference(scs_inference,[],[161,151,23,46,22,176,122,109,96,41,42,29,43,34,35,12,13,3,15])). % 222.01/222.10 cnf(188,plain, % 222.01/222.10 (~E(f9(a1,a1),f9(a5,a8))), % 222.01/222.10 inference(scs_inference,[],[25,89,161,151,23,46,22,176,122,109,96,41,42,29,43,34,35,12,13,3,15,14])). % 222.01/222.10 cnf(190,plain, % 222.01/222.10 (P3(f4(f9(a1,a1),a1,a7),a7)), % 222.01/222.10 inference(scs_inference,[],[25,89,161,151,23,46,22,176,122,109,96,51,44,41,42,29,43,34,35,12,13,3,15,14,38])). % 222.01/222.10 cnf(198,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(x1981,a8))), % 222.01/222.10 inference(scs_inference,[],[116,41])). % 222.01/222.10 cnf(200,plain, % 222.01/222.10 (~P3(a8,f4(a8,a5,a5))), % 222.01/222.10 inference(scs_inference,[],[116,41,29])). % 222.01/222.10 cnf(202,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(a8,x2021))), % 222.01/222.10 inference(scs_inference,[],[116,41,29,42])). % 222.01/222.10 cnf(204,plain, % 222.01/222.10 (~P3(f4(a5,a8,a8),f9(a8,a2))), % 222.01/222.10 inference(scs_inference,[],[116,122,92,41,29,42,43])). % 222.01/222.10 cnf(205,plain, % 222.01/222.10 (~P3(x2051,a2)), % 222.01/222.10 inference(rename_variables,[],[92])). % 222.01/222.10 cnf(210,plain, % 222.01/222.10 (E(f9(x2101,a1),x2101)), % 222.01/222.10 inference(rename_variables,[],[20])). % 222.01/222.10 cnf(215,plain, % 222.01/222.10 (P3(f9(f4(a8,a5,a5),f4(a8,a5,a5)),a7)), % 222.01/222.10 inference(scs_inference,[],[188,70,120,20,210,46,116,122,92,107,41,29,42,43,27,34,35,12])). % 222.01/222.10 cnf(216,plain, % 222.01/222.10 (E(x2161,f9(x2161,x2161))), % 222.01/222.10 inference(rename_variables,[],[46])). % 222.01/222.10 cnf(217,plain, % 222.01/222.10 (~E(a7,a2)), % 222.01/222.10 inference(scs_inference,[],[188,70,120,20,210,46,116,122,92,205,107,41,29,42,43,27,34,35,12,13])). % 222.01/222.10 cnf(219,plain, % 222.01/222.10 (~E(f9(a5,a8),a7)), % 222.01/222.10 inference(scs_inference,[],[25,188,21,70,120,20,210,46,116,122,92,205,107,41,29,42,43,27,34,35,12,13,15])). % 222.01/222.10 cnf(223,plain, % 222.01/222.10 (P3(f4(a1,a1,a7),a7)), % 222.01/222.10 inference(scs_inference,[],[25,48,188,21,70,120,20,210,46,216,116,122,92,205,184,44,107,41,29,42,43,27,34,35,12,13,15,14,38])). % 222.01/222.10 cnf(226,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(x2261,a5))), % 222.01/222.10 inference(scs_inference,[],[155,41])). % 222.01/222.10 cnf(228,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(a5,x2281))), % 222.01/222.10 inference(scs_inference,[],[155,41,42])). % 222.01/222.10 cnf(230,plain, % 222.01/222.10 (~P3(a5,f4(a5,a8,a8))), % 222.01/222.10 inference(scs_inference,[],[155,41,42,29])). % 222.01/222.10 cnf(235,plain, % 222.01/222.10 (E(f9(x2351,a1),x2351)), % 222.01/222.10 inference(rename_variables,[],[20])). % 222.01/222.10 cnf(241,plain, % 222.01/222.10 (~E(a8,a2)), % 222.01/222.10 inference(scs_inference,[],[161,20,235,60,116,155,122,92,173,41,42,29,43,34,35,12,13])). % 222.01/222.10 cnf(243,plain, % 222.01/222.10 (P2(f9(a8,a8),f9(a7,a7))), % 222.01/222.10 inference(scs_inference,[],[113,161,20,235,46,60,116,155,122,92,173,41,42,29,43,34,35,12,13,14])). % 222.01/222.10 cnf(248,plain, % 222.01/222.10 (P3(f4(a1,a1,a7),f9(x2481,a7))), % 222.01/222.10 inference(scs_inference,[],[223,41])). % 222.01/222.10 cnf(252,plain, % 222.01/222.10 (P3(f4(a1,a1,a7),f9(a7,x2521))), % 222.01/222.10 inference(scs_inference,[],[97,223,41,29,42])). % 222.01/222.10 cnf(255,plain, % 222.01/222.10 (~P3(x2551,f9(a1,a1))), % 222.01/222.10 inference(rename_variables,[],[51])). % 222.01/222.10 cnf(257,plain, % 222.01/222.10 (~P1(a8)), % 222.01/222.10 inference(scs_inference,[],[122,51,97,223,241,17,41,29,42,43,27])). % 222.01/222.10 cnf(259,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(f9(a7,x2591),f9(a7,x2591)))), % 222.01/222.10 inference(scs_inference,[],[120,22,122,51,97,223,241,17,41,29,42,43,27,35])). % 222.01/222.10 cnf(260,plain, % 222.01/222.10 (E(f9(x2601,x2601),x2601)), % 222.01/222.10 inference(rename_variables,[],[22])). % 222.01/222.10 cnf(262,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(f9(x2621,a7),f9(x2621,a7)))), % 222.01/222.10 inference(scs_inference,[],[120,22,260,122,51,97,223,241,17,41,29,42,43,27,35,34])). % 222.01/222.10 cnf(265,plain, % 222.01/222.10 (P3(f9(f4(a5,a8,a8),a1),a7)), % 222.01/222.10 inference(scs_inference,[],[120,161,22,260,96,122,51,97,223,241,17,41,29,42,43,27,35,34,12])). % 222.01/222.10 cnf(266,plain, % 222.01/222.10 (E(x2661,f9(x2661,a1))), % 222.01/222.10 inference(rename_variables,[],[96])). % 222.01/222.10 cnf(269,plain, % 222.01/222.10 (P2(a8,f9(a7,a1))), % 222.01/222.10 inference(scs_inference,[],[19,120,161,22,260,96,266,60,122,51,255,97,223,241,17,41,29,42,43,27,35,34,12,13,15])). % 222.01/222.10 cnf(270,plain, % 222.01/222.10 (E(x2701,f9(x2701,a1))), % 222.01/222.10 inference(rename_variables,[],[96])). % 222.01/222.10 cnf(271,plain, % 222.01/222.10 (P2(f9(a5,a1),f9(a1,a7))), % 222.01/222.10 inference(scs_inference,[],[19,186,120,161,22,260,96,266,270,60,122,51,255,97,223,241,17,41,29,42,43,27,35,34,12,13,15,14])). % 222.01/222.10 cnf(273,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),a8)), % 222.01/222.10 inference(scs_inference,[],[19,186,120,161,22,260,96,266,270,60,122,51,255,44,97,223,241,17,41,29,42,43,27,35,34,12,13,15,14,38])). % 222.01/222.10 cnf(276,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),a7)), % 222.01/222.10 inference(scs_inference,[],[19,186,120,161,22,260,96,266,270,60,122,51,255,44,97,223,241,17,41,29,42,43,27,35,34,12,13,15,14,38,33])). % 222.01/222.10 cnf(278,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(x2781,a7))), % 222.01/222.10 inference(scs_inference,[],[276,41])). % 222.01/222.10 cnf(280,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(a7,x2801))), % 222.01/222.10 inference(scs_inference,[],[276,41,42])). % 222.01/222.10 cnf(284,plain, % 222.01/222.10 (~P3(f4(a5,a8,a8),f9(a8,a1))), % 222.01/222.10 inference(scs_inference,[],[276,122,44,41,42,29,43])). % 222.01/222.10 cnf(287,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(f9(a7,x2871),f9(a7,x2871)))), % 222.01/222.10 inference(scs_inference,[],[276,22,122,44,41,42,29,43,35])). % 222.01/222.10 cnf(288,plain, % 222.01/222.10 (E(f9(x2881,x2881),x2881)), % 222.01/222.10 inference(rename_variables,[],[22])). % 222.01/222.10 cnf(290,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(f9(x2901,a7),f9(x2901,a7)))), % 222.01/222.10 inference(scs_inference,[],[276,22,288,122,44,41,42,29,43,35,34])). % 222.01/222.10 cnf(293,plain, % 222.01/222.10 (P3(f9(f4(a1,a1,a8),a1),a7)), % 222.01/222.10 inference(scs_inference,[],[276,22,288,96,122,44,41,42,29,43,35,34,12])). % 222.01/222.10 cnf(295,plain, % 222.01/222.10 (P2(f9(a5,a1),f9(a7,a1))), % 222.01/222.10 inference(scs_inference,[],[271,276,23,22,288,96,122,44,41,42,29,43,35,34,12,15])). % 222.01/222.10 cnf(297,plain, % 222.01/222.10 (~E(f9(f9(a7,x2971),f9(a7,x2971)),f9(a1,a1))), % 222.01/222.10 inference(scs_inference,[],[271,276,23,22,288,96,122,51,44,259,41,42,29,43,35,34,12,15,13])). % 222.01/222.10 cnf(299,plain, % 222.01/222.10 (~E(a1,f9(a5,a8))), % 222.01/222.10 inference(scs_inference,[],[25,62,271,276,23,22,288,96,122,51,44,259,41,42,29,43,35,34,12,15,13,14])). % 222.01/222.10 cnf(304,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(x3041,a8))), % 222.01/222.10 inference(scs_inference,[],[273,41])). % 222.01/222.10 cnf(306,plain, % 222.01/222.10 (~P3(a8,f4(a1,a1,a8))), % 222.01/222.10 inference(scs_inference,[],[273,41,29])). % 222.01/222.10 cnf(308,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(a8,x3081))), % 222.01/222.10 inference(scs_inference,[],[273,41,29,42])). % 222.01/222.10 cnf(313,plain, % 222.01/222.10 (E(f9(x3131,a1),x3131)), % 222.01/222.10 inference(rename_variables,[],[20])). % 222.01/222.10 cnf(320,plain, % 222.01/222.10 (P3(f9(f4(a1,a1,a8),f4(a1,a1,a8)),a7)), % 222.01/222.10 inference(scs_inference,[],[276,20,313,46,273,297,204,107,41,29,42,43,34,27,35,12])). % 222.01/222.10 cnf(322,plain, % 222.01/222.10 (P2(a8,f9(a1,a7))), % 222.01/222.10 inference(scs_inference,[],[269,276,23,20,313,46,273,297,204,107,41,29,42,43,34,27,35,12,15])). % 222.01/222.10 cnf(326,plain, % 222.01/222.10 (~E(a2,f9(a5,a8))), % 222.01/222.10 inference(scs_inference,[],[25,130,269,276,23,20,313,46,92,273,297,262,204,107,41,29,42,43,34,27,35,12,15,13,14])). % 222.01/222.10 cnf(356,plain, % 222.01/222.10 (P3(f9(f4(a5,a8,a5),f4(a5,a8,a5)),f9(x3561,a7))), % 222.01/222.10 inference(scs_inference,[],[105,41])). % 222.01/222.10 cnf(360,plain, % 222.01/222.10 (P3(f9(f4(a5,a8,a5),f4(a5,a8,a5)),f9(a7,x3601))), % 222.01/222.10 inference(scs_inference,[],[102,105,41,29,42])). % 222.01/222.10 cnf(364,plain, % 222.01/222.10 (P3(f9(f4(a5,a8,a5),a1),a7)), % 222.01/222.10 inference(scs_inference,[],[70,96,171,102,105,41,29,42,43,12])). % 222.01/222.10 cnf(374,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(x3741,f9(x3742,a8)))), % 222.01/222.10 inference(scs_inference,[],[198,41])). % 222.01/222.10 cnf(376,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(f9(x3761,a8),x3762))), % 222.01/222.10 inference(scs_inference,[],[198,41,42])). % 222.01/222.10 cnf(387,plain, % 222.01/222.10 (P2(f9(a8,a8),f9(a1,a7))), % 222.01/222.10 inference(scs_inference,[],[243,322,22,46,155,51,133,287,290,198,80,41,42,29,43,12,15,13,14])). % 222.01/222.10 cnf(403,plain, % 222.01/222.10 (~E(f4(a1,a1,a8),f4(a5,a8,a8))), % 222.01/222.10 inference(scs_inference,[],[122,273,64,374,215,41,29,42,43,12])). % 222.01/222.10 cnf(406,plain, % 222.01/222.10 (~E(f9(x4061,f9(x4062,a8)),f9(a1,a1))), % 222.01/222.10 inference(scs_inference,[],[387,23,122,273,51,64,374,215,41,29,42,43,12,15,13])). % 222.01/222.10 cnf(408,plain, % 222.01/222.10 (P2(f9(a8,a1),f9(a7,a7))), % 222.01/222.10 inference(scs_inference,[],[113,387,23,96,122,273,51,64,374,215,41,29,42,43,12,15,13,14])). % 222.01/222.10 cnf(411,plain, % 222.01/222.10 (~P1(f9(x4111,a8))), % 222.01/222.10 inference(scs_inference,[],[113,387,23,96,122,273,51,64,374,215,41,29,42,43,12,15,13,14,5,26])). % 222.01/222.10 cnf(416,plain, % 222.01/222.10 (P3(f9(f4(a5,a8,a8),f4(a5,a8,a8)),f9(x4161,a7))), % 222.01/222.10 inference(scs_inference,[],[181,41])). % 222.01/222.10 cnf(424,plain, % 222.01/222.10 (~P1(f9(x4241,f9(x4242,a8)))), % 222.01/222.10 inference(scs_inference,[],[200,406,376,181,107,41,42,29,43,27])). % 222.01/222.10 cnf(428,plain, % 222.01/222.10 (P2(f9(a8,a1),a7)), % 222.01/222.10 inference(scs_inference,[],[408,22,46,200,406,376,181,248,107,41,42,29,43,27,12,15])). % 222.01/222.10 cnf(430,plain, % 222.01/222.10 (~E(f9(f9(x4301,a8),x4302),a2)), % 222.01/222.10 inference(scs_inference,[],[408,22,46,92,200,406,376,181,248,107,41,42,29,43,27,12,15,13])). % 222.01/222.10 cnf(452,plain, % 222.01/222.10 (P2(f9(a5,a1),a7)), % 222.01/222.10 inference(scs_inference,[],[295,20,96,60,44,230,320,85,430,17,41,29,42,43,27,12,13,15])). % 222.01/222.10 cnf(464,plain, % 222.01/222.10 (~P3(a7,f9(f4(a8,a5,a5),a1))), % 222.01/222.10 inference(scs_inference,[],[145,41,42,29])). % 222.01/222.10 cnf(466,plain, % 222.01/222.10 (~P3(f4(a5,a8,a8),f9(f9(a8,a1),f9(a8,a1)))), % 222.01/222.10 inference(scs_inference,[],[284,145,41,42,29,43])). % 222.01/222.10 cnf(469,plain, % 222.01/222.10 (E(x4691,f9(x4691,a1))), % 222.01/222.10 inference(rename_variables,[],[96])). % 222.01/222.10 cnf(475,plain, % 222.01/222.10 (P3(f4(a1,a1,f9(a8,x4751)),f9(a8,x4751))), % 222.01/222.10 inference(scs_inference,[],[25,428,96,469,51,44,284,145,202,94,41,42,29,43,12,15,13,14,38])). % 222.01/222.10 cnf(480,plain, % 222.01/222.10 (~P1(f9(a8,x4801))), % 222.01/222.10 inference(scs_inference,[],[25,428,96,469,51,44,284,145,202,94,107,41,42,29,43,12,15,13,14,38,40,27])). % 222.01/222.10 cnf(496,plain, % 222.01/222.10 (~E(f9(a5,a1),f9(a5,a8))), % 222.01/222.10 inference(scs_inference,[],[25,452,46,122,306,293,226,252,41,29,42,43,13,12,14])). % 222.01/222.10 cnf(509,plain, % 222.01/222.10 (~P3(f4(a8,a5,a5),f9(a5,a5))), % 222.01/222.10 inference(scs_inference,[],[265,80,41,42,29,43])). % 222.01/222.10 cnf(513,plain, % 222.01/222.10 (~E(f9(a5,x5131),a8)), % 222.01/222.10 inference(scs_inference,[],[96,122,265,228,248,80,41,42,29,43,12,13])). % 222.01/222.10 cnf(522,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(x5221,f9(x5222,a7)))), % 222.01/222.10 inference(scs_inference,[],[167,41])). % 222.01/222.10 cnf(526,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(f9(x5261,a7),x5262))), % 222.01/222.10 inference(scs_inference,[],[364,167,41,29,42])). % 222.01/222.10 cnf(534,plain, % 222.01/222.10 (~P1(f9(x5341,a7))), % 222.01/222.10 inference(scs_inference,[],[46,92,509,364,356,167,223,17,41,29,42,43,13,12,27])). % 222.01/222.10 cnf(554,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(x5541,f9(x5542,a7)))), % 222.01/222.10 inference(scs_inference,[],[128,41])). % 222.01/222.10 cnf(558,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(f9(x5581,a7),x5582))), % 222.01/222.10 inference(scs_inference,[],[526,128,41,29,42])). % 222.01/222.10 cnf(563,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(x5631,f9(a7,x5632)))), % 222.01/222.10 inference(scs_inference,[],[135,41])). % 222.01/222.10 cnf(565,plain, % 222.01/222.10 (P3(f4(a8,a5,a5),f9(f9(a7,x5651),x5652))), % 222.01/222.10 inference(scs_inference,[],[135,41,42])). % 222.01/222.10 cnf(572,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(x5721,f9(a8,x5722)))), % 222.01/222.10 inference(scs_inference,[],[68,41])). % 222.01/222.10 cnf(581,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(x5811,f9(x5812,a8)))), % 222.01/222.10 inference(scs_inference,[],[304,41])). % 222.01/222.10 cnf(583,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(f9(x5831,a8),x5832))), % 222.01/222.10 inference(scs_inference,[],[304,41,42])). % 222.01/222.10 cnf(589,plain, % 222.01/222.10 (~E(f9(x5891,f9(x5892,a7)),f9(a1,a1))), % 222.01/222.10 inference(scs_inference,[],[153,20,51,554,304,41,42,29,3,13])). % 222.01/222.10 cnf(607,plain, % 222.01/222.10 (P3(f4(a1,a1,a8),f9(f9(a8,x6071),x6072))), % 222.01/222.10 inference(scs_inference,[],[558,308,41,29,42])). % 222.01/222.10 cnf(611,plain, % 222.01/222.10 (~P1(f9(x6111,f9(x6112,a7)))), % 222.01/222.10 inference(scs_inference,[],[153,23,589,558,308,107,41,29,42,3,27])). % 222.01/222.10 cnf(615,plain, % 222.01/222.10 (~E(f9(f9(x6151,a7),x6152),a2)), % 222.01/222.10 inference(scs_inference,[],[153,23,92,173,589,558,308,475,107,41,29,42,3,27,12,13])). % 222.01/222.10 cnf(622,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(x6221,f9(x6222,a8)))), % 222.01/222.10 inference(scs_inference,[],[66,41])). % 222.01/222.10 cnf(624,plain, % 222.01/222.10 (P3(f4(a5,a8,a5),f9(f9(x6241,a8),x6242))), % 222.01/222.10 inference(scs_inference,[],[66,41,42])). % 222.01/222.10 cnf(630,plain, % 222.01/222.10 (~P1(f9(f9(x6301,a7),x6302))), % 222.01/222.10 inference(scs_inference,[],[153,22,563,66,615,17,41,42,29,3,27])). % 222.01/222.10 cnf(634,plain, % 222.01/222.10 (~E(f9(x6341,f9(a7,x6342)),f9(a1,a1))), % 222.01/222.10 inference(scs_inference,[],[153,22,51,204,563,66,615,475,17,41,42,29,3,27,12,13])). % 222.01/222.10 cnf(636,plain, % 222.01/222.10 (~E(f9(a7,x6361),a1)), % 222.01/222.10 inference(scs_inference,[],[153,22,51,204,563,66,615,475,17,41,42,29,3,27,12,13,5])). % 222.01/222.10 cnf(646,plain, % 222.01/222.10 (~P1(f9(a7,x6461))), % 222.01/222.10 inference(scs_inference,[],[636,26])). % 222.01/222.10 cnf(654,plain, % 222.01/222.10 (~P1(f9(x6541,f9(a7,x6542)))), % 222.01/222.10 inference(scs_inference,[],[634,565,278,636,107,26,41,29,42,27])). % 222.01/222.10 cnf(658,plain, % 222.01/222.10 (~E(f9(f9(a7,x6581),x6582),a2)), % 222.01/222.10 inference(scs_inference,[],[92,284,634,565,278,636,475,107,26,41,29,42,27,12,13])). % 222.01/222.10 cnf(671,plain, % 222.01/222.10 (~P1(f9(f9(a7,x6711),x6712))), % 222.01/222.10 inference(scs_inference,[],[572,280,658,17,41,29,42,27])). % 222.01/222.10 cnf(693,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(x6931,f9(x6932,a5)))), % 222.01/222.10 inference(scs_inference,[],[226,41])). % 222.01/222.10 cnf(697,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(f9(x6971,a5),x6972))), % 222.01/222.10 inference(scs_inference,[],[581,226,41,29,42])). % 222.01/222.10 cnf(706,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(x7061,f9(a5,x7062)))), % 222.01/222.10 inference(scs_inference,[],[228,41])). % 222.01/222.10 cnf(710,plain, % 222.01/222.10 (P3(f4(a5,a8,a8),f9(f9(a5,x7101),x7102))), % 222.01/222.10 inference(scs_inference,[],[583,228,41,29,42])). % 222.01/222.10 cnf(745,plain, % 222.01/222.10 (~E(f9(a7,x7451),a2)), % 222.01/222.10 inference(scs_inference,[],[92,622,360,248,41,29,42,13])). % 222.01/222.10 cnf(784,plain, % 222.01/222.10 (~E(f9(a7,x7841),a8)), % 222.01/222.10 inference(scs_inference,[],[122,416,169,29,13])). % 222.01/222.10 cnf(819,plain, % 222.01/222.10 (E(f3(x8191,x8192),f3(f9(x8191,a1),x8192))), % 222.01/222.10 inference(scs_inference,[],[20,9,2])). % 222.01/222.10 cnf(820,plain, % 222.01/222.10 (E(f3(f9(x8201,a1),x8202),f3(x8201,x8202))), % 222.01/222.10 inference(scs_inference,[],[819,2])). % 222.01/222.10 cnf(846,plain, % 222.01/222.10 (P3(f4(a1,a1,f9(a7,x8461)),f9(a7,x8461))), % 222.01/222.10 inference(scs_inference,[],[96,51,44,135,223,29,12,13,38])). % 222.01/222.10 cnf(849,plain, % 222.01/222.10 (~P3(f9(x8491,a8),f4(a1,a1,a8))), % 222.01/222.10 inference(scs_inference,[],[304,29])). % 222.01/222.10 cnf(858,plain, % 222.01/222.10 (~P3(f9(a8,x8581),f4(a1,a1,a8))), % 222.01/222.10 inference(scs_inference,[],[308,29])). % 222.01/222.10 cnf(864,plain, % 222.01/222.10 (P3(f4(a1,a1,f9(x8641,a7)),f9(x8641,a7))), % 222.01/222.10 inference(scs_inference,[],[51,44,308,278,29,43,13,38])). % 222.01/222.10 cnf(875,plain, % 222.01/222.10 (~P3(f9(a7,x8751),f4(a1,a1,a8))), % 222.01/222.10 inference(scs_inference,[],[280,29])). % 222.01/222.10 cnf(881,plain, % 222.01/222.10 (~P3(f9(x8811,a8),f4(a8,a5,a5))), % 222.01/222.10 inference(scs_inference,[],[198,29])). % 222.01/222.10 cnf(925,plain, % 222.01/222.10 (~P3(f9(x9251,a7),f4(a1,a1,a8))), % 222.01/222.11 inference(scs_inference,[],[278,29])). % 222.01/222.11 cnf(928,plain, % 222.01/222.11 (~P3(a7,f4(a1,a1,a7))), % 222.01/222.11 inference(scs_inference,[],[223,29])). % 222.01/222.11 cnf(931,plain, % 222.01/222.11 (~P3(f9(x9311,a7),f4(a1,a1,a7))), % 222.01/222.11 inference(scs_inference,[],[248,29])). % 222.01/222.11 cnf(934,plain, % 222.01/222.11 (~P3(f9(a7,x9341),f4(a1,a1,a7))), % 222.01/222.11 inference(scs_inference,[],[252,29])). % 222.01/222.11 cnf(967,plain, % 222.01/222.11 (E(f3(x9671,x9672),f3(x9671,f9(x9672,a1)))), % 222.01/222.11 inference(scs_inference,[],[20,10,2])). % 222.01/222.11 cnf(968,plain, % 222.01/222.11 (E(f3(x9681,f9(x9682,a1)),f3(x9681,x9682))), % 222.01/222.11 inference(scs_inference,[],[967,2])). % 222.01/222.11 cnf(1090,plain, % 222.01/222.11 (E(f3(f9(x10901,a1),f9(x10902,a1)),f3(x10901,x10902))), % 222.01/222.11 inference(scs_inference,[],[820,968,3])). % 222.01/222.11 cnf(1096,plain, % 222.01/222.11 (E(f3(x10961,x10962),f3(f9(x10961,a1),f9(x10962,a1)))), % 222.01/222.11 inference(scs_inference,[],[1090,2])). % 222.01/222.11 cnf(1397,plain, % 222.01/222.11 (P3(f4(f9(a5,a8),f9(a5,a8),a1),f9(a5,a8))), % 222.01/222.11 inference(scs_inference,[],[299,22,44,3,38])). % 222.01/222.11 cnf(1514,plain, % 222.01/222.11 (P1(f9(a2,a1))), % 222.01/222.11 inference(scs_inference,[],[17,96,11])). % 222.01/222.11 cnf(1521,plain, % 222.01/222.11 (~P3(x15211,f9(a2,a1))), % 222.01/222.11 inference(scs_inference,[],[17,326,22,96,92,11,3,38,28])). % 222.01/222.11 cnf(1528,plain, % 222.01/222.11 (P1(f9(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[17,46,11])). % 222.01/222.11 cnf(1530,plain, % 222.01/222.11 (~P3(f4(a5,a8,a8),f9(a8,f9(a2,a1)))), % 222.01/222.11 inference(scs_inference,[],[17,46,122,1521,11,43])). % 222.01/222.11 cnf(1538,plain, % 222.01/222.11 (~P3(x15381,f9(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[17,188,22,46,122,51,1521,11,43,3,38,28])). % 222.01/222.11 cnf(1540,plain, % 222.01/222.11 (P2(f9(a2,a2),x15401)), % 222.01/222.11 inference(scs_inference,[],[17,188,22,46,122,51,1521,11,43,3,38,28,32])). % 222.01/222.11 cnf(1853,plain, % 222.01/222.11 (~P1(f9(x18531,a6))), % 222.01/222.11 inference(scs_inference,[],[24,30])). % 222.01/222.11 cnf(1855,plain, % 222.01/222.11 (~P1(f9(a6,x18551))), % 222.01/222.11 inference(scs_inference,[],[24,30,31])). % 222.01/222.11 cnf(1857,plain, % 222.01/222.11 (~E(a2,f9(a7,x18571))), % 222.01/222.11 inference(scs_inference,[],[745,24,30,31,2])). % 222.01/222.11 cnf(1858,plain, % 222.01/222.11 (~P1(f9(x18581,a5))), % 222.01/222.11 inference(scs_inference,[],[745,24,226,30,31,2,28])). % 222.01/222.11 cnf(1860,plain, % 222.01/222.11 (E(f9(a2,a1),a1)), % 222.01/222.11 inference(scs_inference,[],[1514,745,24,226,30,31,2,28,26])). % 222.01/222.11 cnf(1862,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(a8,x18621))), % 222.01/222.11 inference(scs_inference,[],[1514,745,24,1538,226,273,30,31,2,28,26,35])). % 222.01/222.11 cnf(1863,plain, % 222.01/222.11 (~P3(x18631,f9(a2,a2))), % 222.01/222.11 inference(rename_variables,[],[1538])). % 222.01/222.11 cnf(1865,plain, % 222.01/222.11 (~P2(f9(a5,a8),f9(a7,a7))), % 222.01/222.11 inference(scs_inference,[],[1514,745,24,1538,226,273,22,25,30,31,2,28,26,35,15])). % 222.01/222.11 cnf(1867,plain, % 222.01/222.11 (~E(f9(a2,a1),a7)), % 222.01/222.11 inference(scs_inference,[],[157,1514,745,24,1538,226,273,22,25,30,31,2,28,26,35,15,11])). % 222.01/222.11 cnf(1868,plain, % 222.01/222.11 (~P3(x18681,f9(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[157,1514,745,24,1538,1521,226,273,23,22,25,30,31,2,28,26,35,15,11,13])). % 222.01/222.11 cnf(1869,plain, % 222.01/222.11 (E(f9(x18691,x18692),f9(x18692,x18691))), % 222.01/222.11 inference(rename_variables,[],[23])). % 222.01/222.11 cnf(1871,plain, % 222.01/222.11 (E(f9(x18711,x18712),f9(x18712,x18711))), % 222.01/222.11 inference(rename_variables,[],[23])). % 222.01/222.11 cnf(1872,plain, % 222.01/222.11 (~P2(f9(a8,a5),a7)), % 222.01/222.11 inference(scs_inference,[],[157,219,1514,745,24,1538,1521,226,273,23,1869,1871,22,25,30,31,2,28,26,35,15,11,13,3,14])). % 222.01/222.11 cnf(1874,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(x18741,a8))), % 222.01/222.11 inference(scs_inference,[],[157,219,1514,745,24,1538,1863,1521,226,273,23,1869,1871,22,25,30,31,2,28,26,35,15,11,13,3,14,34])). % 222.01/222.11 cnf(1877,plain, % 222.01/222.11 (~E(f9(x18771,a8),f9(a5,a5))), % 222.01/222.11 inference(scs_inference,[],[157,219,1514,745,24,1538,1863,1521,66,49,226,273,23,1869,1871,22,25,30,31,2,28,26,35,15,11,13,3,14,34,36])). % 222.01/222.11 cnf(1879,plain, % 222.01/222.11 (~P1(f9(a5,x18791))), % 222.01/222.11 inference(scs_inference,[],[228,28])). % 222.01/222.11 cnf(1882,plain, % 222.01/222.11 (E(f9(a2,a2),a1)), % 222.01/222.11 inference(scs_inference,[],[1862,1528,228,28,2,26])). % 222.01/222.11 cnf(1884,plain, % 222.01/222.11 (~E(f9(a2,a2),a8)), % 222.01/222.11 inference(scs_inference,[],[257,1862,1528,228,28,2,26,11])). % 222.01/222.11 cnf(1885,plain, % 222.01/222.11 (~E(a1,a7)), % 222.01/222.11 inference(scs_inference,[],[257,1862,1860,1867,1528,228,28,2,26,11,3])). % 222.01/222.11 cnf(1888,plain, % 222.01/222.11 (~E(f9(x18881,a7),f9(a5,a5))), % 222.01/222.11 inference(scs_inference,[],[257,1862,1865,1860,1867,1528,128,80,228,23,28,2,26,11,3,14,36])). % 222.01/222.11 cnf(1890,plain, % 222.01/222.11 (~P1(a5)), % 222.01/222.11 inference(scs_inference,[],[155,28])). % 222.01/222.11 cnf(1893,plain, % 222.01/222.11 (E(a2,a1)), % 222.01/222.11 inference(scs_inference,[],[1874,155,17,28,2,26])). % 222.01/222.11 cnf(1895,plain, % 222.01/222.11 (~E(f9(a2,a1),f9(x18951,a8))), % 222.01/222.11 inference(scs_inference,[],[1874,411,1514,155,17,28,2,26,11])). % 222.01/222.11 cnf(1898,plain, % 222.01/222.11 (E(f3(a2,x18981),f3(a1,x18981))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,155,17,96,28,2,26,11,3,9])). % 222.01/222.11 cnf(1899,plain, % 222.01/222.11 (E(f3(x18991,a2),f3(x18991,a1))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,155,17,96,28,2,26,11,3,9,10])). % 222.01/222.11 cnf(1900,plain, % 222.01/222.11 (E(f4(a2,x19001,x19002),f4(a1,x19001,x19002))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,155,17,96,28,2,26,11,3,9,10,6])). % 222.01/222.11 cnf(1901,plain, % 222.01/222.11 (E(f4(x19011,a2,x19012),f4(x19011,a1,x19012))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,155,17,96,28,2,26,11,3,9,10,6,7])). % 222.01/222.11 cnf(1902,plain, % 222.01/222.11 (E(f4(x19021,x19022,a2),f4(x19021,x19022,a1))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,155,17,96,28,2,26,11,3,9,10,6,7,8])). % 222.01/222.11 cnf(1903,plain, % 222.01/222.11 (E(f9(a2,x19031),f9(a1,x19031))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,155,17,96,28,2,26,11,3,9,10,6,7,8,4])). % 222.01/222.11 cnf(1904,plain, % 222.01/222.11 (E(f9(x19041,a2),f9(x19041,a1))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,155,17,96,28,2,26,11,3,9,10,6,7,8,4,5])). % 222.01/222.11 cnf(1905,plain, % 222.01/222.11 (~P3(x19051,f3(a2,x19052))+P3(x19051,f3(a1,x19052))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,155,17,96,28,2,26,11,3,9,10,6,7,8,4,5,13])). % 222.01/222.11 cnf(1906,plain, % 222.01/222.11 (P2(f3(a1,x19061),f3(a2,x19061))), % 222.01/222.11 inference(scs_inference,[],[1885,1874,411,1514,21,155,17,96,28,2,26,11,3,9,10,6,7,8,4,5,13,14])). % 222.01/222.11 cnf(1911,plain, % 222.01/222.11 (~E(f9(a5,a5),f9(x19111,a8))), % 222.01/222.11 inference(scs_inference,[],[1877,2])). % 222.01/222.11 cnf(1912,plain, % 222.01/222.11 (P2(f3(a1,a2),f3(a2,a1))), % 222.01/222.11 inference(scs_inference,[],[1877,1899,1906,2,15])). % 222.01/222.11 cnf(1917,plain, % 222.01/222.11 (~E(f9(a2,a2),a5)), % 222.01/222.11 inference(scs_inference,[],[1890,1877,1900,1899,1906,928,1528,2,15,13,11])). % 222.01/222.11 cnf(1919,plain, % 222.01/222.11 (~P3(f9(a7,a7),f4(a2,a1,a7))), % 222.01/222.11 inference(scs_inference,[],[1890,1893,1877,1900,1899,1906,1857,928,1528,22,2,15,13,11,3,12])). % 222.01/222.11 cnf(1922,plain, % 222.01/222.11 (~P3(f9(a7,a7),f4(a2,a2,a7))), % 222.01/222.11 inference(scs_inference,[],[1919,1888,1901,2,13])). % 222.01/222.11 cnf(1927,plain, % 222.01/222.11 (~E(f9(a1,a2),f9(a8,x19271))), % 222.01/222.11 inference(scs_inference,[],[1919,1888,1895,1901,1903,480,1868,16,116,2,13,11,3,35])). % 222.01/222.11 cnf(1928,plain, % 222.01/222.11 (~P3(x19281,f9(a1,a2))), % 222.01/222.11 inference(rename_variables,[],[1868])). % 222.01/222.11 cnf(1930,plain, % 222.01/222.11 (~E(f9(a1,a2),f9(x19301,a8))), % 222.01/222.11 inference(scs_inference,[],[1919,1888,1895,1901,1903,480,1868,1928,16,116,2,13,11,3,35,34])). % 222.01/222.11 cnf(1936,plain, % 222.01/222.11 (~P3(f9(x19361,a8),f4(a2,a1,a8))), % 222.01/222.11 inference(scs_inference,[],[1927,1922,849,1900,46,2,12,13])). % 222.01/222.11 cnf(1937,plain, % 222.01/222.11 (E(f4(a2,x19371,x19372),f4(a1,x19371,x19372))), % 222.01/222.11 inference(rename_variables,[],[1900])). % 222.01/222.11 cnf(1938,plain, % 222.01/222.11 (E(f4(a2,x19381,a2),f4(a1,x19381,a1))), % 222.01/222.11 inference(scs_inference,[],[1927,1902,1922,849,1900,1937,46,2,12,13,3])). % 222.01/222.11 cnf(1941,plain, % 222.01/222.11 (~E(f9(a2,a1),f9(x19411,a7))), % 222.01/222.11 inference(scs_inference,[],[1927,1902,534,1922,849,1900,1937,1514,46,2,12,13,3,11])). % 222.01/222.11 cnf(1942,plain, % 222.01/222.11 (~E(f9(x19421,a7),f9(a8,a8))), % 222.01/222.11 inference(scs_inference,[],[1927,1902,534,1922,849,1900,1937,1514,167,46,122,2,12,13,3,11,36])). % 222.01/222.11 cnf(1947,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(a7,x19471))), % 222.01/222.11 inference(scs_inference,[],[1941,646,1903,1528,2,3,11])). % 222.01/222.11 cnf(1948,plain, % 222.01/222.11 (~P3(f9(a8,x19481),f4(a2,a1,a8))), % 222.01/222.11 inference(scs_inference,[],[1941,646,858,1903,1900,1528,2,3,11,13])). % 222.01/222.11 cnf(1950,plain, % 222.01/222.11 (~E(f9(a7,x19501),f9(a8,a8))), % 222.01/222.11 inference(scs_inference,[],[1941,646,858,1903,1900,1528,169,122,2,3,11,13,36])). % 222.01/222.11 cnf(1956,plain, % 222.01/222.11 (P2(f4(a1,x19561,a1),f4(a2,x19561,a2))), % 222.01/222.11 inference(scs_inference,[],[1941,1898,646,1938,1912,858,1903,1900,1528,21,169,122,2,3,11,13,36,33,15,14])). % 222.01/222.11 cnf(1958,plain, % 222.01/222.11 (~P3(x19581,f3(a1,a2))+P3(x19581,f3(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[1941,1898,646,1938,1912,858,1903,1900,1528,21,169,122,2,3,11,13,36,33,15,14,1905])). % 222.01/222.11 cnf(1961,plain, % 222.01/222.11 (~P3(f3(a2,a1),f3(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[1941,1898,646,1938,1912,858,1903,1900,1528,21,169,122,2,3,11,13,36,33,15,14,1905,29])). % 222.01/222.11 cnf(1962,plain, % 222.01/222.11 (~P3(f3(a2,a1),f3(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[1961,1905])). % 222.01/222.11 cnf(1967,plain, % 222.01/222.11 (E(f4(x19671,a2,x19672),f4(x19671,a1,x19672))), % 222.01/222.11 inference(rename_variables,[],[1901])). % 222.01/222.11 cnf(1968,plain, % 222.01/222.11 (E(f4(x19681,a2,a2),f4(x19681,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[1961,1942,1948,1901,1967,1902,1899,1905,2,12,13,3])). % 222.01/222.11 cnf(1971,plain, % 222.01/222.11 (~E(a1,f9(x19711,a6))), % 222.01/222.11 inference(scs_inference,[],[1961,1942,1948,1853,1901,1967,1902,1899,16,1905,2,12,13,3,11])). % 222.01/222.11 cnf(1973,plain, % 222.01/222.11 (~P3(f3(a2,a2),f3(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[1962,1947,1899,2,12])). % 222.01/222.11 cnf(1975,plain, % 222.01/222.11 (~E(f9(a2,a1),f9(a7,x19751))), % 222.01/222.11 inference(scs_inference,[],[1962,1947,1904,1899,2,12,3])). % 222.01/222.11 cnf(1977,plain, % 222.01/222.11 (~P3(f9(a7,x19771),f4(a2,a1,a8))), % 222.01/222.11 inference(scs_inference,[],[1962,1947,1904,875,1899,1900,2,12,3,13])). % 222.01/222.11 cnf(1979,plain, % 222.01/222.11 (~E(f9(a2,a1),f9(a6,x19791))), % 222.01/222.11 inference(scs_inference,[],[1962,1947,1855,1904,875,1899,1900,1514,2,12,3,13,11])). % 222.01/222.11 cnf(1980,plain, % 222.01/222.11 (~E(f9(a1,a2),f9(a7,x19801))), % 222.01/222.11 inference(scs_inference,[],[1962,1947,1855,1904,875,1868,1899,1900,1514,223,2,12,3,13,11,35])). % 222.01/222.11 cnf(1989,plain, % 222.01/222.11 (E(f4(a2,a2,a2),f4(a1,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[1950,1977,1968,1901,1900,2,13,3])). % 222.01/222.11 cnf(1992,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(x19921,a5))), % 222.01/222.11 inference(scs_inference,[],[1950,1977,1858,1968,1901,1900,1528,2,13,3,11])). % 222.01/222.11 cnf(1993,plain, % 222.01/222.11 (~P3(f9(x19931,a7),f4(a2,a1,a8))), % 222.01/222.11 inference(scs_inference,[],[1950,1977,1858,1968,1901,1900,1528,23,2,13,3,11,12])). % 222.01/222.11 cnf(1998,plain, % 222.01/222.11 (~E(a1,f9(a6,x19981))), % 222.01/222.11 inference(scs_inference,[],[1975,1979,1993,1860,1901,2,13,3])). % 222.01/222.11 cnf(1999,plain, % 222.01/222.11 (~E(a1,f9(a5,x19991))), % 222.01/222.11 inference(scs_inference,[],[1975,1979,1993,1879,1860,1901,16,2,13,3,11])). % 222.01/222.11 cnf(2000,plain, % 222.01/222.11 (~P3(x20001,f4(a1,x20002,a1))+P3(x20001,f4(a2,x20002,a2))), % 222.01/222.11 inference(scs_inference,[],[1975,1979,1993,1879,1956,1860,1901,16,2,13,3,11,33])). % 222.01/222.11 cnf(2002,plain, % 222.01/222.11 (P2(f4(a1,a2,a1),f4(a1,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[1975,1979,1993,1879,1956,1989,1860,1901,16,2,13,3,11,33,15])). % 222.01/222.11 cnf(2004,plain, % 222.01/222.11 (P2(f4(a1,a1,a1),f4(a2,a2,a2))), % 222.01/222.11 inference(scs_inference,[],[1975,1979,1993,1879,1956,1989,1860,1901,16,21,2,13,3,11,33,15,14])). % 222.01/222.11 cnf(2006,plain, % 222.01/222.11 (~E(f9(x20061,a5),f9(a8,a8))), % 222.01/222.11 inference(scs_inference,[],[1975,1979,1993,1879,1956,1989,1860,1901,16,21,226,122,2,13,3,11,33,15,14,36])). % 222.01/222.11 cnf(2010,plain, % 222.01/222.11 (~P3(f4(a2,a2,a2),f4(a1,a2,a1))), % 222.01/222.11 inference(scs_inference,[],[1975,1979,1993,1879,1956,1989,1860,1901,16,21,226,122,2,13,3,11,33,15,14,36,29])). % 222.01/222.11 cnf(2013,plain, % 222.01/222.11 (~P3(f4(a2,a2,a2),f4(a2,a2,a2))), % 222.01/222.11 inference(scs_inference,[],[2010,1992,1938,2,13])). % 222.01/222.11 cnf(2015,plain, % 222.01/222.11 (~E(f9(a2,a1),f9(a8,x20151))), % 222.01/222.11 inference(scs_inference,[],[2010,1992,480,1938,1514,2,13,11])). % 222.01/222.11 cnf(2016,plain, % 222.01/222.11 (~E(a1,f9(x20161,a5))), % 222.01/222.11 inference(scs_inference,[],[2010,1992,1882,480,1938,1514,2,13,11,3])). % 222.01/222.11 cnf(2017,plain, % 222.01/222.11 (~E(f9(a5,x20171),f9(a8,a8))), % 222.01/222.11 inference(scs_inference,[],[2010,1992,1882,480,1938,1514,228,122,2,13,11,3,36])). % 222.01/222.11 cnf(2019,plain, % 222.01/222.11 (~P3(f4(a2,a2,a2),f4(a1,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2010,2004,1992,1882,480,1938,1514,228,122,2,13,11,3,36,33])). % 222.01/222.11 cnf(2021,plain, % 222.01/222.11 (~E(f9(a8,a8),f9(x20211,a5))), % 222.01/222.11 inference(scs_inference,[],[2006,2])). % 222.01/222.11 cnf(2027,plain, % 222.01/222.11 (~E(f9(a5,a5),f9(a8,x20271))), % 222.01/222.11 inference(scs_inference,[],[2019,2006,2015,411,1968,509,1903,16,116,2,13,3,11,35])). % 222.01/222.11 cnf(2029,plain, % 222.01/222.11 (~E(f9(a1,a2),f9(x20291,a5))), % 222.01/222.11 inference(scs_inference,[],[2019,2006,2015,411,1968,509,1903,1868,16,116,155,2,13,3,11,35,34])). % 222.01/222.11 cnf(2035,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(x20351,a7))), % 222.01/222.11 inference(scs_inference,[],[2017,1936,534,1901,1528,2,13,11])). % 222.01/222.11 cnf(2036,plain, % 222.01/222.11 (E(f3(a2,a2),f3(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2017,1936,1898,534,1899,1901,1528,2,13,11,3])). % 222.01/222.11 cnf(2045,plain, % 222.01/222.11 (P2(f3(a1,a1),f3(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[2036,2027,1980,1904,21,2,3,14])). % 222.01/222.11 cnf(2048,plain, % 222.01/222.11 (~E(f9(a2,a1),f9(x20481,a6))), % 222.01/222.11 inference(scs_inference,[],[2036,2027,1980,1853,1904,21,1514,2,3,14,13,11])). % 222.01/222.11 cnf(2050,plain, % 222.01/222.11 (~P3(f3(a2,a2),f3(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2045,2035,1973,2,33])). % 222.01/222.11 cnf(2052,plain, % 222.01/222.11 (P2(f3(a1,a1),f3(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[2045,2035,1973,1898,2,33,15])). % 222.01/222.11 cnf(2054,plain, % 222.01/222.11 (~P3(f9(x20541,a7),f4(a2,a1,a7))), % 222.01/222.11 inference(scs_inference,[],[2045,2035,1973,931,1898,1900,2,33,15,13])). % 222.01/222.11 cnf(2056,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(a6,x20561))), % 222.01/222.11 inference(scs_inference,[],[2045,2035,1973,931,1855,1898,1900,1528,2,33,15,13,11])). % 222.01/222.11 cnf(2058,plain, % 222.01/222.11 (~P3(f3(a2,a2),f3(a2,a1))), % 222.01/222.11 inference(scs_inference,[],[2045,2035,1973,931,1855,1882,1898,1900,1528,2,33,15,13,11,3,1905])). % 222.01/222.11 cnf(2060,plain, % 222.01/222.11 (~P3(f3(a2,a1),f3(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2052,2048,1961,2,33])). % 222.01/222.11 cnf(2064,plain, % 222.01/222.11 (~E(a1,a5)), % 222.01/222.11 inference(scs_inference,[],[2052,2048,2054,1890,1961,1901,16,2,33,13,11])). % 222.01/222.11 cnf(2065,plain, % 222.01/222.11 (~E(f9(a1,a1),f9(x20651,a5))), % 222.01/222.11 inference(scs_inference,[],[2052,2048,2054,2029,1890,1904,1961,1901,16,2,33,13,11,3])). % 222.01/222.11 cnf(2067,plain, % 222.01/222.11 (~E(f9(a8,a2),f9(a5,x20671))), % 222.01/222.11 inference(scs_inference,[],[2052,2048,2054,2029,1890,1904,1961,204,1901,16,155,2,33,13,11,3,35])). % 222.01/222.11 cnf(2071,plain, % 222.01/222.11 (~E(a5,a1)), % 222.01/222.11 inference(scs_inference,[],[2064,2])). % 222.01/222.11 cnf(2074,plain, % 222.01/222.11 (~E(f9(a2,a1),f9(x20741,a5))), % 222.01/222.11 inference(scs_inference,[],[2064,934,1858,1900,1514,2,13,11])). % 222.01/222.11 cnf(2080,plain, % 222.01/222.11 (~E(f9(a6,x20801),f9(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[2056,2])). % 222.01/222.11 cnf(2081,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(a5,x20811))), % 222.01/222.11 inference(scs_inference,[],[2056,1879,1528,2,11])). % 222.01/222.11 cnf(2084,plain, % 222.01/222.11 (P2(f4(x20841,x20842,a1),f4(x20841,x20842,a2))), % 222.01/222.11 inference(scs_inference,[],[2071,2056,1879,1902,21,1528,96,2,11,3,14])). % 222.01/222.11 cnf(2088,plain, % 222.01/222.11 (P2(f4(x20881,x20882,a1),f4(x20881,x20882,a2))), % 222.01/222.11 inference(rename_variables,[],[2084])). % 222.01/222.11 cnf(2091,plain, % 222.01/222.11 (P2(f4(a2,a2,a1),f4(a1,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2060,2065,2084,2088,2013,1989,2,33,1905,15])). % 222.01/222.11 cnf(2093,plain, % 222.01/222.11 (~P3(f9(x20931,a7),f4(a1,a2,a8))), % 222.01/222.11 inference(scs_inference,[],[2060,2065,2084,2088,2013,925,1989,1901,2,33,1905,15,13])). % 222.01/222.11 cnf(2096,plain, % 222.01/222.11 (~E(f9(a8,a1),f9(a5,x20961))), % 222.01/222.11 inference(scs_inference,[],[2067,284,155,2,35])). % 222.01/222.11 cnf(2098,plain, % 222.01/222.11 (~E(f9(a8,a1),f9(x20981,a5))), % 222.01/222.11 inference(scs_inference,[],[2067,284,155,2,35,34])). % 222.01/222.11 cnf(2104,plain, % 222.01/222.11 (P2(f4(x21041,a1,a1),f4(x21041,a2,a2))), % 222.01/222.11 inference(scs_inference,[],[1884,2074,1968,1903,21,2,3,14])). % 222.01/222.11 cnf(2106,plain, % 222.01/222.11 (~E(a1,a6)), % 222.01/222.11 inference(scs_inference,[],[1884,2074,1968,1903,24,16,21,2,3,14,11])). % 222.01/222.11 cnf(2107,plain, % 222.01/222.11 (~E(a6,a1)), % 222.01/222.11 inference(scs_inference,[],[2106,2])). % 222.01/222.11 cnf(2108,plain, % 222.01/222.11 (~P3(f4(a2,a2,a2),f4(a2,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2106,2104,2013,2,33])). % 222.01/222.11 cnf(2109,plain, % 222.01/222.11 (P2(f4(x21091,a1,a1),f4(x21091,a2,a2))), % 222.01/222.11 inference(rename_variables,[],[2104])). % 222.01/222.11 cnf(2111,plain, % 222.01/222.11 (~E(f9(a1,a1),a6)), % 222.01/222.11 inference(scs_inference,[],[2106,2104,2013,46,2,33,3])). % 222.01/222.11 cnf(2113,plain, % 222.01/222.11 (P2(f4(a2,a1,a1),f4(a1,a2,a1))), % 222.01/222.11 inference(scs_inference,[],[2106,2104,2109,2013,1938,46,2,33,3,15])). % 222.01/222.11 cnf(2121,plain, % 222.01/222.11 (~E(f9(a5,a5),f9(a7,x21211))), % 222.01/222.11 inference(scs_inference,[],[2107,2081,100,70,96,2,3,35])). % 222.01/222.11 cnf(2124,plain, % 222.01/222.11 (~E(f9(a1,a8),f9(a5,x21241))), % 222.01/222.11 inference(scs_inference,[],[2096,23,2,3])). % 222.01/222.11 cnf(2128,plain, % 222.01/222.11 (P2(f4(a2,a1,a1),f4(a1,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2091,2098,1901,2,14])). % 222.01/222.11 cnf(2131,plain, % 222.01/222.11 (~E(a5,f9(x21311,a8))), % 222.01/222.11 inference(scs_inference,[],[2091,1911,2098,257,1901,1514,22,2,14,11,3])). % 222.01/222.11 cnf(2133,plain, % 222.01/222.11 (~E(f9(a7,x21331),f9(a5,a5))), % 222.01/222.11 inference(scs_inference,[],[2121,2])). % 222.01/222.11 cnf(2134,plain, % 222.01/222.11 (~P2(f9(a8,a5),f9(a7,a1))), % 222.01/222.11 inference(scs_inference,[],[2121,1872,20,2,15])). % 222.01/222.11 cnf(2136,plain, % 222.01/222.11 (~P2(f9(a5,a8),f9(a7,a1))), % 222.01/222.11 inference(scs_inference,[],[2121,1872,23,20,2,15,14])). % 222.01/222.11 cnf(2138,plain, % 222.01/222.11 (~P3(f4(a2,a2,a2),f4(a2,a1,a2))), % 222.01/222.11 inference(scs_inference,[],[2108,2121,1872,1902,23,20,2,15,14,13])). % 222.01/222.11 cnf(2141,plain, % 222.01/222.11 (~P2(f9(a8,a5),f9(a7,a2))), % 222.01/222.11 inference(scs_inference,[],[2134,2124,1904,2,15])). % 222.01/222.11 cnf(2144,plain, % 222.01/222.11 (~P2(f9(a5,a8),f9(a7,a2))), % 222.01/222.11 inference(scs_inference,[],[2136,1930,1904,2,15])). % 222.01/222.11 cnf(2151,plain, % 222.01/222.11 (~P2(f9(a8,a5),f9(a2,a7))), % 222.01/222.11 inference(scs_inference,[],[2141,1917,23,2,15])). % 222.01/222.11 cnf(2152,plain, % 222.01/222.11 (E(f9(x21521,x21522),f9(x21522,x21521))), % 222.01/222.11 inference(rename_variables,[],[23])). % 222.01/222.11 cnf(2153,plain, % 222.01/222.11 (~P2(f9(a5,a8),f9(a2,a7))), % 222.01/222.11 inference(scs_inference,[],[2141,1917,23,2152,2,15,14])). % 222.01/222.11 cnf(2157,plain, % 222.01/222.11 (~E(a6,f9(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2111,2])). % 222.01/222.11 cnf(2167,plain, % 222.01/222.11 (~E(f9(a6,x21671),a1)), % 222.01/222.11 inference(scs_inference,[],[1998,2])). % 222.01/222.11 cnf(2171,plain, % 222.01/222.11 (~P3(f4(a5,a8,a8),f9(a2,a8))), % 222.01/222.11 inference(scs_inference,[],[1999,204,23,2,13])). % 222.01/222.11 cnf(2185,plain, % 222.01/222.11 (~E(f9(a2,a8),f9(a7,x21851))), % 222.01/222.11 inference(scs_inference,[],[2131,2171,161,2,35])). % 222.01/222.11 cnf(2202,plain, % 222.01/222.11 (~E(a2,a7)), % 222.01/222.11 inference(scs_inference,[],[217,2])). % 222.01/222.11 cnf(2205,plain, % 222.01/222.11 (~E(f9(a5,a8),f9(a5,a1))), % 222.01/222.11 inference(scs_inference,[],[496,2])). % 222.01/222.11 cnf(2207,plain, % 222.01/222.11 (~E(f9(a8,a5),f9(a5,a1))), % 222.01/222.11 inference(scs_inference,[],[2205,784,23,2,3])). % 222.01/222.11 cnf(2209,plain, % 222.01/222.11 (~E(f9(a5,a1),f9(a8,a5))), % 222.01/222.11 inference(scs_inference,[],[2207,2])). % 222.01/222.11 cnf(2212,plain, % 222.01/222.11 (~P3(f9(f3(a2,a2),f3(a2,a2)),f3(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[2050,22,1958,12])). % 222.01/222.11 cnf(2214,plain, % 222.01/222.11 (~E(f9(a1,a5),f9(a8,a5))), % 222.01/222.11 inference(scs_inference,[],[2209,513,23,2,3])). % 222.01/222.11 cnf(2216,plain, % 222.01/222.11 (~E(f9(a8,a5),f9(a1,a5))), % 222.01/222.11 inference(scs_inference,[],[2214,2])). % 222.01/222.11 cnf(2220,plain, % 222.01/222.11 (~E(f4(a5,a8,a8),f4(a1,a1,a8))), % 222.01/222.11 inference(scs_inference,[],[403,2])). % 222.01/222.11 cnf(2221,plain, % 222.01/222.11 (~E(a8,a7)), % 222.01/222.11 inference(scs_inference,[],[183,2])). % 222.01/222.11 cnf(2222,plain, % 222.01/222.11 (~E(f9(a1,a1),a5)), % 222.01/222.11 inference(scs_inference,[],[183,2064,46,2,3])). % 222.01/222.11 cnf(2224,plain, % 222.01/222.11 (~E(a5,f9(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2222,2])). % 222.01/222.11 cnf(2228,plain, % 222.01/222.11 (~E(f9(a5,a8),f9(a1,a5))), % 222.01/222.11 inference(scs_inference,[],[2216,1979,23,2,3])). % 222.01/222.11 cnf(2231,plain, % 222.01/222.11 (~E(f9(a8,a1),a7)), % 222.01/222.11 inference(scs_inference,[],[2221,2228,96,2,3])). % 222.01/222.11 cnf(2233,plain, % 222.01/222.11 (~E(a7,f9(a8,a1))), % 222.01/222.11 inference(scs_inference,[],[2231,2])). % 222.01/222.11 cnf(2244,plain, % 222.01/222.11 (~E(a2,a8)), % 222.01/222.11 inference(scs_inference,[],[241,2])). % 222.01/222.11 cnf(2251,plain, % 222.01/222.11 (~E(f9(a1,a8),f9(a7,x22511))), % 222.01/222.11 inference(scs_inference,[],[2185,1903,3])). % 222.01/222.11 cnf(2255,plain, % 222.01/222.11 (~P3(f9(f4(a2,a2,a2),f4(a2,a2,a2)),f4(a1,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2138,22,2000,12])). % 222.01/222.11 cnf(2256,plain, % 222.01/222.11 (~E(a2,f9(x22561,a6))), % 222.01/222.11 inference(scs_inference,[],[17,1853,11])). % 222.01/222.11 cnf(2258,plain, % 222.01/222.11 (~P3(f4(a5,a8,a5),f9(a5,a1))), % 222.01/222.11 inference(scs_inference,[],[20,49,13])). % 222.01/222.11 cnf(2260,plain, % 222.01/222.11 (~E(f9(a7,a1),f9(a8,a1))), % 222.01/222.11 inference(scs_inference,[],[20,2233,49,96,13,3])). % 222.01/222.11 cnf(2263,plain, % 222.01/222.11 (~E(f9(a5,a1),f9(x22631,a8))), % 222.01/222.11 inference(scs_inference,[],[2258,2260,60,2,34])). % 222.01/222.11 cnf(2265,plain, % 222.01/222.11 (~E(f9(a5,a1),f9(a8,x22651))), % 222.01/222.11 inference(scs_inference,[],[2258,2260,60,2,34,35])). % 222.01/222.11 cnf(2267,plain, % 222.01/222.11 (~P3(f4(a5,a8,a5),f9(a5,a2))), % 222.01/222.11 inference(scs_inference,[],[2258,2260,1904,60,2,34,35,13])). % 222.01/222.11 cnf(2270,plain, % 222.01/222.11 (~P3(f4(a8,a5,a5),f9(a5,a1))), % 222.01/222.11 inference(scs_inference,[],[20,2263,80,2,13])). % 222.01/222.11 cnf(2273,plain, % 222.01/222.11 (~P3(f4(a8,a5,a5),f9(a5,a2))), % 222.01/222.11 inference(scs_inference,[],[2270,2265,1904,2,13])). % 222.01/222.11 cnf(2279,plain, % 222.01/222.11 (~P3(f4(a8,a5,a5),f9(a2,a5))), % 222.01/222.11 inference(scs_inference,[],[20,2273,2080,23,3,13])). % 222.01/222.11 cnf(2281,plain, % 222.01/222.11 (~E(f9(a2,a2),a6)), % 222.01/222.11 inference(scs_inference,[],[20,2273,2080,23,3,13,2])). % 222.01/222.11 cnf(2284,plain, % 222.01/222.11 (~E(f9(a2,a5),f9(a8,x22841))), % 222.01/222.11 inference(scs_inference,[],[2279,116,34,35])). % 222.01/222.11 cnf(2289,plain, % 222.01/222.11 (~E(f9(a1,a2),a6)), % 222.01/222.11 inference(scs_inference,[],[2281,2284,1903,2,3])). % 222.01/222.11 cnf(2292,plain, % 222.01/222.11 (~E(a6,f9(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[2289,2])). % 222.01/222.11 cnf(2293,plain, % 222.01/222.11 (~E(a7,f9(a5,a5))), % 222.01/222.11 inference(scs_inference,[],[20,2133,2289,2,3])). % 222.01/222.11 cnf(2297,plain, % 222.01/222.11 (~E(f9(a5,a5),a7)), % 222.01/222.11 inference(scs_inference,[],[2293,2])). % 222.01/222.11 cnf(2298,plain, % 222.01/222.11 (~P3(f4(a5,a8,a5),f9(a2,a5))), % 222.01/222.11 inference(scs_inference,[],[2267,2293,23,2,13])). % 222.01/222.11 cnf(2303,plain, % 222.01/222.11 (~E(f9(a5,a1),f9(a7,x23031))), % 222.01/222.11 inference(scs_inference,[],[2270,120,34,35])). % 222.01/222.11 cnf(2308,plain, % 222.01/222.11 (~E(f9(a6,a6),f9(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[2292,2303,46,2,3])). % 222.01/222.11 cnf(2312,plain, % 222.01/222.11 (P2(f3(x23121,a1),f3(x23121,a2))), % 222.01/222.11 inference(scs_inference,[],[21,2308,1899,2,14])). % 222.01/222.11 cnf(2313,plain, % 222.01/222.11 (P2(x23131,x23131)), % 222.01/222.11 inference(rename_variables,[],[21])). % 222.01/222.11 cnf(2314,plain, % 222.01/222.11 (P2(f3(a2,a2),f3(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[21,2313,2308,2036,1899,2,14,15])). % 222.01/222.11 cnf(2320,plain, % 222.01/222.11 (~E(f9(a5,a2),f9(a8,x23201))), % 222.01/222.11 inference(scs_inference,[],[2273,116,34,35])). % 222.01/222.11 cnf(2325,plain, % 222.01/222.11 (~E(a5,a7)), % 222.01/222.11 inference(scs_inference,[],[22,2297,2320,2,3])). % 222.01/222.11 cnf(2328,plain, % 222.01/222.11 (P2(f3(a2,a1),f3(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[2325,2314,1899,2,14])). % 222.01/222.11 cnf(2330,plain, % 222.01/222.11 (P2(f3(a2,a1),f3(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[2325,2314,2312,1898,1899,2,14,15])). % 222.01/222.11 cnf(2336,plain, % 222.01/222.11 (E(f9(x23361,x23362),f9(x23362,x23361))), % 222.01/222.11 inference(rename_variables,[],[23])). % 222.01/222.11 cnf(2337,plain, % 222.01/222.11 (~P2(f9(a8,a5),f9(a1,a7))), % 222.01/222.11 inference(scs_inference,[],[23,2336,2134,2258,13,15])). % 222.01/222.11 cnf(2338,plain, % 222.01/222.11 (E(f9(x23381,x23382),f9(x23382,x23381))), % 222.01/222.11 inference(rename_variables,[],[23])). % 222.01/222.11 cnf(2339,plain, % 222.01/222.11 (~P3(f9(a7,x23391),f4(a1,a2,a8))), % 222.01/222.11 inference(scs_inference,[],[23,2336,2338,2093,2134,2258,13,15,12])). % 222.01/222.11 cnf(2341,plain, % 222.01/222.11 (E(f9(x23411,x23412),f9(x23412,x23411))), % 222.01/222.11 inference(rename_variables,[],[23])). % 222.01/222.11 cnf(2346,plain, % 222.01/222.11 (~P2(f9(a5,a8),f9(a1,a7))), % 222.01/222.11 inference(scs_inference,[],[23,2336,2338,2341,2298,2093,2134,2258,70,13,15,12,34,35,14])). % 222.01/222.11 cnf(2357,plain, % 222.01/222.11 (~E(f9(a2,a1),a6)), % 222.01/222.11 inference(scs_inference,[],[24,1514,11])). % 222.01/222.11 cnf(2370,plain, % 222.01/222.11 (~E(a2,a6)), % 222.01/222.11 inference(scs_inference,[],[24,17,11])). % 222.01/222.11 cnf(2386,plain, % 222.01/222.11 (E(f9(a2,a2),f9(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[44,1538,38])). % 222.01/222.11 cnf(2389,plain, % 222.01/222.11 (~P3(x23891,a1)), % 222.01/222.11 inference(rename_variables,[],[44])). % 222.01/222.11 cnf(2391,plain, % 222.01/222.11 (~E(f9(a5,x23911),f9(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[44,2389,1538,228,38,36])). % 222.01/222.11 cnf(2397,plain, % 222.01/222.11 (E(a1,f9(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[44,2391,92,2,38])). % 222.01/222.11 cnf(2413,plain, % 222.01/222.11 (E(a2,f9(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[44,2251,92,23,3,2,38])). % 222.01/222.11 cnf(2419,plain, % 222.01/222.11 (~P3(a7,f4(a1,a2,a8))), % 222.01/222.11 inference(scs_inference,[],[46,2339,12])). % 222.01/222.11 cnf(2451,plain, % 222.01/222.11 (~P3(x24511,a2)), % 222.01/222.11 inference(rename_variables,[],[92])). % 222.01/222.11 cnf(2453,plain, % 222.01/222.11 (E(a2,f9(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[92,2451,155,44,34,38])). % 222.01/222.11 cnf(2456,plain, % 222.01/222.11 (~P3(x24561,a2)), % 222.01/222.11 inference(rename_variables,[],[92])). % 222.01/222.11 cnf(2459,plain, % 222.01/222.11 (~E(a2,f9(a5,x24591))), % 222.01/222.11 inference(scs_inference,[],[92,2451,2456,155,44,34,38,2,35])). % 222.01/222.11 cnf(2464,plain, % 222.01/222.11 (E(f9(a1,a2),f9(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[92,2202,2453,2459,1868,2,3,38])). % 222.01/222.11 cnf(2477,plain, % 222.01/222.11 (~E(f9(a1,a2),f9(x24771,a6))), % 222.01/222.11 inference(scs_inference,[],[2397,1971,3])). % 222.01/222.11 cnf(2483,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(x24831,a6))), % 222.01/222.11 inference(scs_inference,[],[2464,2477,3])). % 222.01/222.11 cnf(2508,plain, % 222.01/222.11 (~P1(f9(f9(a6,x25081),x25082))), % 222.01/222.11 inference(scs_inference,[],[2167,26,31])). % 222.01/222.11 cnf(2512,plain, % 222.01/222.11 (~E(f9(a2,a2),f9(f9(a7,x25121),x25122))), % 222.01/222.11 inference(scs_inference,[],[1528,280,28,35])). % 222.01/222.11 cnf(2517,plain, % 222.01/222.11 (~E(f9(a2,a1),f9(x25171,f9(x25172,a8)))), % 222.01/222.11 inference(scs_inference,[],[1514,198,28,34])). % 222.01/222.11 cnf(2520,plain, % 222.01/222.11 (~P3(f3(a2,a2),f9(f3(a2,a1),f9(a1,a1)))), % 222.01/222.11 inference(scs_inference,[],[107,2058,28,43])). % 222.01/222.11 cnf(2544,plain, % 222.01/222.11 (~P3(a8,f4(a1,a2,a8))), % 222.01/222.11 inference(scs_inference,[],[306,1901,13])). % 222.01/222.11 cnf(2553,plain, % 222.01/222.11 (~P3(a7,f9(f9(f4(a1,a2,a8),f9(a2,a1)),f9(f4(a1,a2,a8),f9(a2,a1))))), % 222.01/222.11 inference(scs_inference,[],[1514,2419,22,28,36])). % 222.01/222.11 cnf(2557,plain, % 222.01/222.11 (E(f9(a1,a1),f9(f9(a2,a2),f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[107,1538,28,38])). % 222.01/222.11 cnf(2585,plain, % 222.01/222.11 (E(f9(a2,a2),f9(f9(a2,a1),f9(a2,a1)))), % 222.01/222.11 inference(scs_inference,[],[1528,1521,28,38])). % 222.01/222.11 cnf(2589,plain, % 222.01/222.11 (E(f9(a2,a1),f9(f9(a2,a2),f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[1514,1538,28,38])). % 222.01/222.11 cnf(2593,plain, % 222.01/222.11 (E(f9(a1,a1),f9(f9(a1,a2),f9(a1,a2)))), % 222.01/222.11 inference(scs_inference,[],[107,1868,28,38])). % 222.01/222.11 cnf(2597,plain, % 222.01/222.11 (E(a2,f9(f9(a2,a1),f9(a2,a1)))), % 222.01/222.11 inference(scs_inference,[],[17,1521,28,38])). % 222.01/222.11 cnf(2608,plain, % 222.01/222.11 (E(f9(a1,a2),f9(a1,f9(a1,a2)))), % 222.01/222.11 inference(scs_inference,[],[16,1868,28,38])). % 222.01/222.11 cnf(2609,plain, % 222.01/222.11 (~P3(f9(x26091,a8),f9(f9(f4(a8,a5,a5),a2),a1))), % 222.01/222.11 inference(scs_inference,[],[17,881,20,28,36])). % 222.01/222.11 cnf(2613,plain, % 222.01/222.11 (E(f9(a2,a1),f9(a1,f9(a2,a1)))), % 222.01/222.11 inference(scs_inference,[],[16,1521,28,38])). % 222.01/222.11 cnf(2615,plain, % 222.01/222.11 (E(f9(a2,a2),f9(f9(a2,a2),f9(a1,a1)))), % 222.01/222.11 inference(scs_inference,[],[107,1538,28,38])). % 222.01/222.11 cnf(2643,plain, % 222.01/222.11 (E(f9(a2,a1),f9(f9(a2,a1),f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[1528,1521,28,38])). % 222.01/222.11 cnf(2644,plain, % 222.01/222.11 (E(f9(a2,a2),f9(a1,f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[16,1538,28,38])). % 222.01/222.11 cnf(2645,plain, % 222.01/222.11 (E(f9(a1,a2),f9(f9(a1,a2),f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[1528,1868,28,38])). % 222.01/222.11 cnf(2648,plain, % 222.01/222.11 (~P3(f3(f9(a5,a8),f9(a7,a2)),f9(a7,a2))), % 222.01/222.11 inference(scs_inference,[],[2144,37])). % 222.01/222.11 cnf(2650,plain, % 222.01/222.11 (E(f9(x26501,f9(a2,a2)),f9(x26501,f9(a1,a1)))), % 222.01/222.11 inference(scs_inference,[],[2144,2386,37,5])). % 222.01/222.11 cnf(2657,plain, % 222.01/222.11 (P3(f9(f4(a5,a8,a5),a1),a8)), % 222.01/222.11 inference(scs_inference,[],[2144,2386,611,96,37,5,31,30,10,7,83])). % 222.01/222.11 cnf(2662,plain, % 222.01/222.11 (E(f9(f9(a2,a2),x26621),f9(f9(a1,a1),x26621))), % 222.01/222.11 inference(scs_inference,[],[2144,2386,611,96,37,5,31,30,10,7,83,8,6,9,4])). % 222.01/222.11 cnf(2663,plain, % 222.01/222.11 (P3(f3(f9(a5,a8),f9(a7,a2)),f9(a5,a8))), % 222.01/222.11 inference(scs_inference,[],[2144,2386,611,96,37,5,31,30,10,7,83,8,6,9,4,32])). % 222.01/222.11 cnf(2665,plain, % 222.01/222.11 (~P3(f9(f3(a2,a2),f3(a2,a2)),f3(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[2144,2386,2212,611,96,37,5,31,30,10,7,83,8,6,9,4,32,1905])). % 222.01/222.11 cnf(2673,plain, % 222.01/222.11 (~P3(f9(f3(a2,a2),f3(a2,a2)),f3(a2,a1))), % 222.01/222.11 inference(scs_inference,[],[464,2144,2386,2330,2212,2512,611,2609,2553,96,37,5,31,30,10,7,83,8,6,9,4,32,1905,41,42,2,43,33])). % 222.01/222.11 cnf(2675,plain, % 222.01/222.11 (~P3(f9(f4(a5,a8,a8),f4(a5,a8,a8)),f9(f9(a8,a1),f9(a8,a1)))), % 222.01/222.11 inference(scs_inference,[],[464,2144,2386,2330,2212,466,2512,611,2609,2553,96,22,37,5,31,30,10,7,83,8,6,9,4,32,1905,41,42,2,43,33,12])). % 222.01/222.11 cnf(2676,plain, % 222.01/222.11 (E(f9(x26761,x26761),x26761)), % 222.01/222.11 inference(rename_variables,[],[22])). % 222.01/222.11 cnf(2677,plain, % 222.01/222.11 (~E(f9(f9(a8,a1),f9(a8,a1)),f9(x26771,f9(x26772,f9(x26773,a7))))), % 222.01/222.11 inference(scs_inference,[],[464,2144,2386,2330,2212,466,2512,611,2609,2553,522,96,22,37,5,31,30,10,7,83,8,6,9,4,32,1905,41,42,2,43,33,12,34])). % 222.01/222.11 cnf(2680,plain, % 222.01/222.11 (~P3(x26801,f9(f9(a1,a1),a1))), % 222.01/222.11 inference(rename_variables,[],[57])). % 222.01/222.11 cnf(2682,plain, % 222.01/222.11 (P2(f9(f9(a2,a2),f9(a2,a2)),x26821)), % 222.01/222.11 inference(scs_inference,[],[464,2144,2386,2330,2212,466,2557,2512,611,2609,2553,1397,57,89,522,96,22,37,5,31,30,10,7,83,8,6,9,4,32,1905,41,42,2,43,33,12,34,35,14])). % 222.01/222.11 cnf(2684,plain, % 222.01/222.11 (~P3(f9(f3(a2,a2),f3(a2,a2)),f3(a1,f9(a2,a1)))), % 222.01/222.11 inference(scs_inference,[],[464,2244,2144,2386,2330,2212,466,2557,2597,2512,611,2609,2553,1397,57,89,522,968,96,22,37,5,31,30,10,7,83,8,6,9,4,32,1905,41,42,2,43,33,12,34,35,14,3,13])). % 222.01/222.11 cnf(2688,plain, % 222.01/222.11 (E(f9(a2,a1),f9(f9(f9(a1,a1),a1),f9(f9(a1,a1),a1)))), % 222.01/222.11 inference(scs_inference,[],[464,2244,2144,2386,2330,2212,466,2557,2597,2512,611,2609,2553,1397,57,2680,89,522,968,1521,96,22,2676,37,5,31,30,10,7,83,8,6,9,4,32,1905,41,42,2,43,33,12,34,35,14,3,13,15,38])). % 222.01/222.11 cnf(2693,plain, % 222.01/222.11 (~E(f9(x26931,f9(x26932,a7)),f9(f9(f9(a8,a1),f9(a8,a1)),f9(f9(a8,a1),f9(a8,a1))))), % 222.01/222.11 inference(scs_inference,[],[464,2244,2144,2386,2330,2212,466,2557,2597,2512,611,2609,2553,1397,57,2680,89,522,968,1521,96,22,2676,37,5,31,30,10,7,83,8,6,9,4,32,1905,41,42,2,43,33,12,34,35,14,3,13,15,38,36])). % 222.01/222.11 cnf(2699,plain, % 222.01/222.11 (~P3(f3(f9(a8,a5),f9(a2,a7)),f9(a2,a7))), % 222.01/222.11 inference(scs_inference,[],[2151,37])). % 222.01/222.11 cnf(2701,plain, % 222.01/222.11 (E(f9(x27011,f9(a2,a2)),f9(x27011,f9(f9(a2,a1),f9(a2,a1))))), % 222.01/222.11 inference(scs_inference,[],[2151,2585,37,5])). % 222.01/222.11 cnf(2708,plain, % 222.01/222.11 (E(f4(x27081,f9(a2,a2),x27082),f4(x27081,f9(f9(a2,a1),f9(a2,a1)),x27082))), % 222.01/222.11 inference(scs_inference,[],[2151,2585,630,2663,37,5,29,31,30,7])). % 222.01/222.11 cnf(2709,plain, % 222.01/222.11 (E(f3(x27091,f9(a2,a2)),f3(x27091,f9(f9(a2,a1),f9(a2,a1))))), % 222.01/222.11 inference(scs_inference,[],[2151,2585,630,2663,37,5,29,31,30,7,10])). % 222.01/222.11 cnf(2712,plain, % 222.01/222.11 (E(f4(x27121,x27122,f9(a2,a2)),f4(x27121,x27122,f9(f9(a2,a1),f9(a2,a1))))), % 222.01/222.11 inference(scs_inference,[],[2151,2585,630,2663,46,37,5,29,31,30,7,10,83,8])). % 222.01/222.11 cnf(2713,plain, % 222.01/222.11 (E(f4(f9(a2,a2),x27131,x27132),f4(f9(f9(a2,a1),f9(a2,a1)),x27131,x27132))), % 222.01/222.11 inference(scs_inference,[],[2151,2585,630,2663,46,37,5,29,31,30,7,10,83,8,6])). % 222.01/222.11 cnf(2716,plain, % 222.01/222.11 (P3(f3(f9(a8,a5),f9(a2,a7)),f9(a8,a5))), % 222.01/222.11 inference(scs_inference,[],[2151,2585,630,2663,46,37,5,29,31,30,7,10,83,8,6,9,4,32])). % 222.01/222.11 cnf(2718,plain, % 222.01/222.11 (~P3(f9(f4(a5,a8,a8),f4(a5,a8,a8)),f9(a8,a1))), % 222.01/222.11 inference(scs_inference,[],[2151,2585,630,2675,2663,46,37,5,29,31,30,7,10,83,8,6,9,4,32,41])). % 222.01/222.11 cnf(2720,plain, % 222.01/222.11 (~P3(f3(f9(a5,a8),f9(a7,a2)),a7)), % 222.01/222.11 inference(scs_inference,[],[2151,2648,2585,630,2675,2663,46,37,5,29,31,30,7,10,83,8,6,9,4,32,41,42])). % 222.01/222.11 cnf(2723,plain, % 222.01/222.11 (P3(f4(a1,a1,f9(a7,f9(f9(a1,a1),a1))),a7)), % 222.01/222.11 inference(scs_inference,[],[2151,2648,2585,2517,630,2675,2663,846,57,46,37,5,29,31,30,7,10,83,8,6,9,4,32,41,42,2,43])). % 222.01/222.11 cnf(2725,plain, % 222.01/222.11 (~P3(x27251,f9(f9(a1,a1),a1))), % 222.01/222.11 inference(rename_variables,[],[57])). % 222.01/222.11 cnf(2729,plain, % 222.01/222.11 (~P3(f3(f9(f9(a5,a8),a1),f9(a7,a2)),f9(a7,a2))), % 222.01/222.11 inference(scs_inference,[],[2151,2128,2255,2648,2585,2517,630,2675,2663,846,57,820,46,37,5,29,31,30,7,10,83,8,6,9,4,32,41,42,2,43,33,12])). % 222.01/222.11 cnf(2731,plain, % 222.01/222.11 (~E(f9(f9(a1,a1),a1),f9(x27311,a8))), % 222.01/222.11 inference(scs_inference,[],[2151,2128,2255,2648,2585,2657,2517,630,2675,2663,846,57,2725,820,46,37,5,29,31,30,7,10,83,8,6,9,4,32,41,42,2,43,33,12,34])). % 222.01/222.11 cnf(2732,plain, % 222.01/222.11 (~P3(x27321,f9(f9(a1,a1),a1))), % 222.01/222.11 inference(rename_variables,[],[57])). % 222.01/222.11 cnf(2736,plain, % 222.01/222.11 (~P2(f9(f9(a8,a5),a1),f9(a2,a7))), % 222.01/222.11 inference(scs_inference,[],[2151,2128,2255,2648,2585,2657,2517,630,2675,2663,846,57,2725,820,46,20,37,5,29,31,30,7,10,83,8,6,9,4,32,41,42,2,43,33,12,34,35,14])). % 222.01/222.11 cnf(2738,plain, % 222.01/222.11 (~E(f9(f9(a2,a1),f9(a2,a1)),f9(x27381,a6))), % 222.01/222.11 inference(scs_inference,[],[2151,2128,2483,2255,2648,2585,2657,2517,630,2675,2663,846,57,2725,820,46,20,37,5,29,31,30,7,10,83,8,6,9,4,32,41,42,2,43,33,12,34,35,14,3])). % 222.01/222.11 cnf(2743,plain, % 222.01/222.11 (E(f9(f9(a1,a1),a1),f9(f9(a2,a2),f9(f9(a1,a1),a1)))), % 222.01/222.11 inference(scs_inference,[],[464,2151,2328,2128,2483,2255,2648,2585,2657,2517,630,2675,1096,2663,846,57,2725,2732,820,1904,1538,46,20,37,5,29,31,30,7,10,83,8,6,9,4,32,41,42,2,43,33,12,34,35,14,3,13,15,38])). % 222.01/222.11 cnf(2753,plain, % 222.01/222.11 (~P3(f3(f9(a5,a8),f9(a2,a7)),f9(a2,a7))), % 222.01/222.11 inference(scs_inference,[],[2153,37])). % 222.01/222.11 cnf(2755,plain, % 222.01/222.11 (E(f9(x27551,f9(a2,a1)),f9(x27551,f9(f9(a2,a2),f9(a2,a2))))), % 222.01/222.11 inference(scs_inference,[],[2153,2589,37,5])). % 222.01/222.11 cnf(2767,plain, % 222.01/222.11 (E(f9(f9(a2,a1),x27671),f9(f9(f9(a2,a2),f9(a2,a2)),x27671))), % 222.01/222.11 inference(scs_inference,[],[2153,2716,2589,654,37,5,29,31,30,7,10,8,6,9,4])). % 222.01/222.11 cnf(2768,plain, % 222.01/222.11 (P3(f3(f9(a5,a8),f9(a2,a7)),f9(a5,a8))), % 222.01/222.11 inference(scs_inference,[],[2153,2716,2589,654,37,5,29,31,30,7,10,8,6,9,4,32])). % 222.01/222.11 cnf(2770,plain, % 222.01/222.11 (~P3(f3(f9(a8,a5),f9(a2,a7)),a7)), % 222.01/222.11 inference(scs_inference,[],[2153,2699,2716,2589,654,37,5,29,31,30,7,10,8,6,9,4,32,41])). % 222.01/222.11 cnf(2772,plain, % 222.01/222.11 (~P3(f9(f4(a5,a8,a8),f4(a5,a8,a8)),a8)), % 222.01/222.11 inference(scs_inference,[],[2153,2699,2716,2718,2589,654,37,5,29,31,30,7,10,8,6,9,4,32,41,42])). % 222.01/222.11 cnf(2783,plain, % 222.01/222.11 (P2(f9(f9(a2,a2),f9(a1,a1)),x27831)), % 222.01/222.11 inference(scs_inference,[],[2153,2665,2699,2716,2718,2731,2589,2615,654,1540,968,37,5,29,31,30,7,10,8,6,9,4,32,41,42,2,43,12,34,35,14])). % 222.01/222.11 cnf(2789,plain, % 222.01/222.11 (E(f9(f9(a1,a1),a1),f9(f9(f9(a1,a1),a1),f9(a1,a2)))), % 222.01/222.11 inference(scs_inference,[],[2370,2153,2665,2699,2716,2718,2731,2520,2589,2615,654,2650,1540,2597,57,968,1868,22,37,5,29,31,30,7,10,8,6,9,4,32,41,42,2,43,12,34,35,14,3,13,15,38])). % 222.01/222.11 cnf(2799,plain, % 222.01/222.11 (~P3(f3(f9(a5,a8),f9(a1,a7)),f9(a1,a7))), % 222.01/222.11 inference(scs_inference,[],[2346,37])). % 222.01/222.11 cnf(2803,plain, % 222.01/222.11 (E(f9(x28031,f9(a2,a1)),f9(x28031,f9(f9(a2,a1),f9(a2,a2))))), % 222.01/222.11 inference(scs_inference,[],[2346,2643,2723,37,29,5])). % 222.01/222.11 cnf(2813,plain, % 222.01/222.11 (E(f9(f9(a2,a1),x28131),f9(f9(f9(a2,a1),f9(a2,a2)),x28131))), % 222.01/222.11 inference(scs_inference,[],[2346,2643,671,2723,37,29,5,31,30,7,10,8,6,9,4])). % 222.01/222.11 cnf(2814,plain, % 222.01/222.11 (P3(f3(f9(a5,a8),f9(a1,a7)),f9(a5,a8))), % 222.01/222.11 inference(scs_inference,[],[2346,2643,671,2723,37,29,5,31,30,7,10,8,6,9,4,32])). % 222.01/222.11 cnf(2823,plain, % 222.01/222.11 (~P3(x28231,f9(f9(a1,a1),a1))), % 222.01/222.11 inference(rename_variables,[],[57])). % 222.01/222.11 cnf(2826,plain, % 222.01/222.11 (E(f3(f9(x28261,a1),x28262),f3(x28261,x28262))), % 222.01/222.11 inference(rename_variables,[],[820])). % 222.01/222.11 cnf(2828,plain, % 222.01/222.11 (~P3(x28281,f9(f9(a1,a1),a1))), % 222.01/222.11 inference(rename_variables,[],[57])). % 222.01/222.11 cnf(2839,plain, % 222.01/222.11 (E(f9(f9(a1,a1),a1),f9(f9(a2,a1),f9(f9(a1,a1),a1)))), % 222.01/222.11 inference(scs_inference,[],[2357,2346,2673,2753,2736,2738,2643,671,2729,2723,2768,864,820,2826,57,2823,2828,1904,1521,20,37,29,5,31,30,7,10,8,6,9,4,32,41,42,2,43,12,34,35,14,3,13,15,38])). % 222.01/222.11 cnf(2846,plain, % 222.01/222.11 (~P3(x28461,f9(f9(a2,a1),f9(a2,a1)))), % 222.01/222.11 inference(scs_inference,[],[1514,22,28,13])). % 222.01/222.11 cnf(2862,plain, % 222.01/222.11 (E(x28621,f9(x28621,a1))), % 222.01/222.11 inference(rename_variables,[],[96])). % 222.01/222.11 cnf(2864,plain, % 222.01/222.11 (~P3(x28641,a1)), % 222.01/222.11 inference(rename_variables,[],[44])). % 222.01/222.11 cnf(2867,plain, % 222.01/222.11 (P2(f9(f3(a1,a1),a1),f3(a2,a2))), % 222.01/222.11 inference(scs_inference,[],[44,96,2862,1901,57,2716,2768,2045,563,2772,2684,2220,2677,2,42,41,1905,32,83,5,29,15,13,3,14])). % 222.01/222.11 cnf(2869,plain, % 222.01/222.11 (~P3(x28691,f9(f9(a2,a2),f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[44,96,2862,1901,57,2716,2768,2045,563,2767,2772,2846,2684,2220,2677,2,42,41,1905,32,83,5,29,15,13,3,14,35])). % 222.01/222.11 cnf(2875,plain, % 222.01/222.11 (~E(f4(a5,a8,a5),f3(f9(a5,a8),f9(a7,a2)))), % 222.01/222.11 inference(scs_inference,[],[44,96,2862,70,1901,57,2716,2768,2045,563,2767,2803,1530,2772,2846,2684,2720,2220,2677,2,42,41,1905,32,83,5,29,15,13,3,14,35,34,12])). % 222.01/222.11 cnf(2876,plain, % 222.01/222.11 (P1(f9(a1,a2))), % 222.01/222.11 inference(scs_inference,[],[23,1514,44,96,2862,70,1901,57,2716,2768,2045,563,2767,2803,1530,2772,2846,2684,2720,2220,2677,2,42,41,1905,32,83,5,29,15,13,3,14,35,34,12,11])). % 222.01/222.11 cnf(2884,plain, % 222.01/222.11 (P3(f4(a1,a2,a6),a6)), % 222.01/222.11 inference(scs_inference,[],[122,20,23,1514,44,2864,96,2862,92,70,1868,1901,57,2716,2768,2292,2045,563,2767,2803,1530,2772,2846,2684,2720,2220,2677,2,42,41,1905,32,83,5,29,15,13,3,14,35,34,12,11,43,36,38])). % 222.01/222.11 cnf(2888,plain, % 222.01/222.11 (~P3(f4(a8,x28881,f9(a5,a5)),x28881)+~P3(f4(a8,x28881,f9(a5,a5)),f9(a5,a5))), % 222.01/222.11 inference(scs_inference,[],[122,20,23,1514,44,2864,96,2862,92,70,1868,1901,57,2716,2768,2292,2027,2045,563,2767,2803,1530,2772,2846,2684,2720,2220,2677,2,42,41,1905,32,83,5,29,15,13,3,14,35,34,12,11,43,36,38,39])). % 222.01/222.11 cnf(2893,plain, % 222.01/222.11 (P3(f4(a8,f9(a5,a5),f9(a5,a5)),a8)), % 222.01/222.11 inference(scs_inference,[],[2027,2888,38])). % 222.01/222.11 cnf(2899,plain, % 222.01/222.11 (P2(f9(f9(a2,a1),f9(a2,a1)),x28991)), % 222.01/222.11 inference(scs_inference,[],[1904,2768,2846,2,42,41,32])). % 222.01/222.11 cnf(2900,plain, % 222.01/222.11 (~P3(x29001,f9(f9(a2,a1),f9(a2,a1)))), % 222.01/222.11 inference(rename_variables,[],[2846])). % 222.01/222.11 cnf(2907,plain, % 222.01/222.11 (E(x29071,f9(x29071,a1))), % 222.01/222.11 inference(rename_variables,[],[96])). % 222.01/222.11 cnf(2909,plain, % 222.01/222.11 (~P3(x29091,a1)), % 222.01/222.11 inference(rename_variables,[],[44])). % 222.01/222.11 cnf(2913,plain, % 222.01/222.11 (E(x29131,f9(x29131,a1))), % 222.01/222.11 inference(rename_variables,[],[96])). % 222.01/222.11 cnf(2914,plain, % 222.01/222.11 (~P3(f4(a8,f9(a5,a5),f9(a5,a5)),f9(a5,a5))), % 222.01/222.11 inference(scs_inference,[],[44,96,2907,1904,1900,2768,2027,1956,565,2846,2220,2814,2893,2693,2,42,41,32,5,29,15,13,3,14,40])). % 222.01/222.11 cnf(2917,plain, % 222.01/222.11 (~P3(x29171,f9(f9(a2,a1),f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[44,96,2907,1904,1900,2768,2027,1956,565,2846,2900,2220,2813,2814,2893,2693,2,42,41,32,5,29,15,13,3,14,40,35])). % 222.01/222.11 cnf(2937,plain, % 222.01/222.11 (~P3(x29371,f9(f9(a2,a1),a1))), % 222.01/222.11 inference(scs_inference,[],[122,1514,44,2909,96,2907,2913,161,1538,19,1904,1900,57,2768,2027,1956,2035,565,2767,2846,2900,2720,2220,2813,2814,2893,2869,2693,2,42,41,32,5,29,15,13,3,14,40,35,12,11,33,43,36,38,28])). % 222.01/222.11 cnf(2946,plain, % 222.01/222.11 (P3(f4(a5,a8,a8),f9(x29461,f9(x29462,f9(x29463,a7))))), % 222.01/222.11 inference(scs_inference,[],[1900,522,2,42,41])). % 222.01/222.11 cnf(2948,plain, % 222.01/222.11 (P2(f9(f9(a2,a1),f9(a2,a2)),x29481)), % 222.01/222.11 inference(scs_inference,[],[1900,522,2917,2,42,41,32])). % 222.01/222.11 cnf(2954,plain, % 222.01/222.11 (E(x29541,f9(x29541,a1))), % 222.01/222.11 inference(rename_variables,[],[96])). % 222.01/222.11 cnf(2958,plain, % 222.01/222.11 (P2(f9(f3(a1,a2),a1),f3(a2,a1))), % 222.01/222.11 inference(scs_inference,[],[122,22,96,2954,1900,2643,522,2893,1912,2917,2,42,41,32,29,15,13,3,14])). % 222.01/222.11 cnf(2961,plain, % 222.01/222.11 (P1(f9(f9(a2,a1),f9(a2,a1)))), % 222.01/222.11 inference(scs_inference,[],[122,22,1514,96,2954,46,120,1900,2643,522,2893,2720,1912,2917,2,42,41,32,29,15,13,3,14,12,11])). % 222.01/222.11 cnf(2993,plain, % 222.01/222.11 (E(x29931,f9(x29931,a1))), % 222.01/222.11 inference(rename_variables,[],[96])). % 222.01/222.11 cnf(2997,plain, % 222.01/222.11 (P2(f9(f4(a1,a1,a1),a1),f4(a2,a2,a2))), % 222.01/222.11 inference(scs_inference,[],[122,22,96,2993,1903,819,475,322,2004,2884,2946,2937,2,42,41,32,29,15,13,3,14])). % 222.01/222.11 cnf(3000,plain, % 222.01/222.11 (P1(f9(f9(a2,a1),f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[122,22,1514,96,2993,276,1903,2643,819,475,2720,322,2004,2884,2946,2937,2,42,41,32,29,15,13,3,14,12,11])). % 222.01/222.11 cnf(3003,plain, % 222.01/222.11 (P3(f4(a1,a6,a1),a6)), % 222.01/222.11 inference(scs_inference,[],[122,22,1514,44,96,2993,276,1903,2643,819,2171,475,2720,1971,322,2004,2884,2946,2937,2,42,41,32,29,15,13,3,14,12,11,43,38])). % 222.01/222.11 cnf(3018,plain, % 222.01/222.11 (P3(f4(a8,a5,a5),f9(x30181,f9(f9(x30182,a8),x30183)))), % 222.01/222.11 inference(scs_inference,[],[2643,376,2,42,41])). % 222.01/222.11 cnf(3023,plain, % 222.01/222.11 (E(x30231,f9(x30231,a1))), % 222.01/222.11 inference(rename_variables,[],[96])). % 222.01/222.11 cnf(3026,plain, % 222.01/222.11 (E(f9(f3(x30261,a2),f3(x30261,a2)),f3(x30261,a1))), % 222.01/222.11 inference(scs_inference,[],[44,22,96,2643,1899,376,2004,2946,2,42,41,29,15,13,3])). % 222.01/222.11 cnf(3028,plain, % 222.01/222.11 (P2(f9(f3(a2,a2),a1),f3(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[44,22,96,3023,2643,1899,376,2004,2946,2314,2,42,41,29,15,13,3,14])). % 222.01/222.11 cnf(3031,plain, % 222.01/222.11 (P1(f9(f9(a2,a2),f9(a2,a2)))), % 222.01/222.11 inference(scs_inference,[],[44,22,1514,96,3023,2643,2589,223,1899,2720,376,2004,2946,2314,2,42,41,29,15,13,3,14,12,11])). % 222.01/222.11 cnf(3057,plain, % 222.01/222.11 (E(x30571,f9(x30571,a1))), % 222.01/222.11 inference(rename_variables,[],[96])). % 222.01/222.11 cnf(3059,plain, % 222.01/222.11 (~P3(x30591,a1)), % 222.01/222.11 inference(rename_variables,[],[44])). % 222.01/222.11 cnf(3060,plain, % 222.01/222.11 (E(f9(f4(x30601,x30602,a2),f4(x30601,x30602,a2)),f4(x30601,x30602,a1))), % 222.01/222.11 inference(scs_inference,[],[44,22,96,2585,1902,583,2314,3003,3018,2,42,41,29,15,13,3])). % 222.01/222.11 cnf(3062,plain, % 222.01/222.11 (P2(f9(f3(a2,a1),a1),f3(a1,a1))), % 222.01/222.11 inference(scs_inference,[],[44,22,96,3057,2585,1902,583,2314,2328,3003,3018,2,42,41,29,15,13,3,14])). % 222.01/222.11 cnf(3064,plain, % 222.01/222.11 (~E(f4(a5,a8,a5),f3(f9(a8,a5),f9(a2,a7)))), % 222.01/222.11 inference(scs_inference,[],[44,22,96,3057,2585,85,2699,1902,583,2314,2328,3003,3018,2,42,41,29,15,13,3,14,12])). % 222.01/222.11 cnf(3070,plain, % 222.01/222.11 (~P3(f3(f9(a5,a8),f9(a7,a2)),f9(a7,a7))), % 222.01/222.11 inference(scs_inference,[],[44,22,96,3057,16,2585,85,2699,1902,2720,583,2314,2767,2328,3003,3018,3000,2,42,41,29,15,13,3,14,12,11,27,43])). % 222.01/222.11 cnf(3083,plain, % 222.01/222.11 (P3(f4(a5,a1,a1),a7)), % 222.01/222.11 inference(scs_inference,[],[18,44,3059,22,96,3057,16,2585,85,2699,1902,2720,583,2314,1999,2767,2293,2328,3003,3018,3000,2,42,41,29,15,13,3,14,12,11,27,43,38,28,32,39,33])). % 222.01/222.11 cnf(3092,plain, % 222.01/222.11 (P3(f4(a1,a1,a8),f9(f9(f9(a8,x30921),x30922),x30923))), % 222.01/222.11 inference(scs_inference,[],[2589,607,3018,41,2,29,42])). % 222.01/222.11 cnf(3094,plain, % 222.01/222.11 (P2(f9(f4(a2,a1,a1),a1),f4(a1,a1,a1))), % 222.01/222.11 inference(scs_inference,[],[96,2589,607,3018,2128,41,2,29,42,14])). % 222.01/222.11 cnf(3095,plain, % 222.01/222.11 (E(x30951,f9(x30951,a1))), % 222.01/222.11 inference(rename_variables,[],[96])). % 222.01/222.11 cnf(3105,plain, % 222.01/222.11 (~P3(x31051,a1)), % 222.01/222.11 inference(rename_variables,[],[44])). % 222.01/222.11 cnf(3106,plain, % 222.01/222.11 (~E(f4(a5,a8,a5),f3(f9(f9(a5,a8),a1),f9(f9(a7,a2),a1)))), % 222.01/222.11 inference(scs_inference,[],[44,96,3095,2589,2699,167,1090,2753,607,2328,3018,2128,2662,2875,3031,41,2,29,42,14,12,11,15,43,13,3])). % 222.01/222.11 cnf(3117,plain, % 222.01/222.11 (P2(f9(f9(a1,a1),f9(a2,a2)),x31171)), % 222.01/222.11 inference(scs_inference,[],[44,3105,96,3095,92,2589,2699,167,1090,2753,607,2328,2459,3018,2128,2662,2875,3031,41,2,29,42,14,12,11,15,43,13,3,38,26,28,32])). % 222.01/222.11 cnf(3129,plain, % 222.01/222.11 (E(f3(x31291,a1),f3(x31291,a2))), % 222.01/222.11 inference(scs_inference,[],[1899,624,41,2])). % 222.01/222.12 cnf(3134,plain, % 222.01/222.12 (P2(f9(f3(a2,a1),a1),f3(a1,a2))), % 222.01/222.12 inference(scs_inference,[],[96,1899,624,2330,3083,41,2,29,42,14])). % 222.01/222.12 cnf(3135,plain, % 222.01/222.12 (E(x31351,f9(x31351,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3141,plain, % 222.01/222.12 (E(x31411,f9(x31411,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3145,plain, % 222.01/222.12 (~P3(x31451,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3157,plain, % 222.01/222.12 (P2(f9(f9(f9(a2,a1),f9(a2,a2)),f9(a2,a2)),x31571)), % 222.01/222.12 inference(scs_inference,[],[44,3145,96,3135,3141,1521,2643,2699,1899,128,624,2267,2128,1895,2330,3000,2813,3083,3092,41,2,29,42,14,12,11,15,43,13,3,38,26,28,32])). % 222.01/222.12 cnf(3168,plain, % 222.01/222.12 (P3(f3(f9(a5,a8),f9(a7,a2)),f9(x31681,f9(a5,a8)))), % 222.01/222.12 inference(scs_inference,[],[2386,2663,2,41])). % 222.01/222.12 cnf(3174,plain, % 222.01/222.12 (P2(f9(f4(a2,a2,a1),a1),f4(a1,a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,2386,2663,3092,2091,2,41,29,42,14])). % 222.01/222.12 cnf(3199,plain, % 222.01/222.12 (E(f4(x31991,x31992,a1),f4(x31991,x31992,a2))), % 222.01/222.12 inference(scs_inference,[],[1902,2])). % 222.01/222.12 cnf(3200,plain, % 222.01/222.12 (P3(f4(a8,f9(a5,a5),f9(a5,a5)),f9(x32001,a8))), % 222.01/222.12 inference(scs_inference,[],[1902,2893,2,41])). % 222.01/222.12 cnf(3202,plain, % 222.01/222.12 (P3(f4(a8,f9(a5,a5),f9(a5,a5)),f9(a8,x32021))), % 222.01/222.12 inference(scs_inference,[],[1902,2893,2,41,42])). % 222.01/222.12 cnf(3207,plain, % 222.01/222.12 (E(x32071,f9(x32071,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3213,plain, % 222.01/222.12 (E(x32131,f9(x32131,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3225,plain, % 222.01/222.12 (P2(f9(f9(a2,a1),f9(a1,a1)),x32251)), % 222.01/222.12 inference(scs_inference,[],[44,96,3207,3213,22,1538,2716,1902,1898,2273,2893,2091,3000,1992,2084,2650,3168,2,41,42,29,14,3,11,15,12,43,38,28,32])). % 222.01/222.12 cnf(3229,plain, % 222.01/222.12 (P3(f4(a1,a5,f9(a2,a2)),a7)), % 222.01/222.12 inference(scs_inference,[],[44,96,3207,3213,22,1538,18,2716,1902,1898,2273,2893,2091,3000,1992,2084,1877,2650,3168,2,41,42,29,14,3,11,15,12,43,38,28,32,39,33])). % 222.01/222.12 cnf(3235,plain, % 222.01/222.12 (E(f3(a1,x32351),f3(a2,x32351))), % 222.01/222.12 inference(scs_inference,[],[1898,2])). % 222.01/222.12 cnf(3238,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(f9(x32381,f9(a7,x32382)),x32383))), % 222.01/222.12 inference(scs_inference,[],[1898,563,2,41,42])). % 222.01/222.12 cnf(3243,plain, % 222.01/222.12 (E(x32431,f9(x32431,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3249,plain, % 222.01/222.12 (E(x32491,f9(x32491,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3250,plain, % 222.01/222.12 (P3(f9(f3(f9(a5,a8),f9(a2,a7)),a1),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[96,3243,3249,2768,1090,1898,563,3106,2084,1906,2803,3200,2961,2,41,42,29,14,11,3,15,12])). % 222.01/222.12 cnf(3271,plain, % 222.01/222.12 (E(f4(a1,a1,a1),f4(a2,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[1989,2])). % 222.01/222.12 cnf(3272,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(x32721,f9(f9(a7,x32722),x32723)))), % 222.01/222.12 inference(scs_inference,[],[1989,565,2,41])). % 222.01/222.12 cnf(3274,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(f9(f9(a7,x32741),x32742),x32743))), % 222.01/222.12 inference(scs_inference,[],[1989,565,2,41,42])). % 222.01/222.12 cnf(3308,plain, % 222.01/222.12 (P3(f4(a5,a8,a5),f9(x33081,f9(x33082,f9(a8,x33083))))), % 222.01/222.12 inference(scs_inference,[],[2036,572,2,41])). % 222.01/222.12 cnf(3310,plain, % 222.01/222.12 (P3(f4(a5,a8,a5),f9(f9(x33101,f9(a8,x33102)),x33103))), % 222.01/222.12 inference(scs_inference,[],[2036,572,2,41,42])). % 222.01/222.12 cnf(3314,plain, % 222.01/222.12 (P2(f9(f4(a1,a2,a1),a1),f4(a1,a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,2036,572,3238,2002,2,41,42,29,14])). % 222.01/222.12 cnf(3315,plain, % 222.01/222.12 (E(x33151,f9(x33151,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3316,plain, % 222.01/222.12 (E(f9(f4(a2,a2,a2),f4(a2,a2,a2)),f4(a1,a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,22,1989,2036,572,3238,2002,2,41,42,29,14,3])). % 222.01/222.12 cnf(3319,plain, % 222.01/222.12 (E(x33191,f9(x33191,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3321,plain, % 222.01/222.12 (P3(f9(f3(f9(a5,a8),f9(a7,a2)),a1),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[96,3315,3319,22,1528,2663,1989,2036,572,2312,3238,2002,2644,2,41,42,29,14,3,15,11,12])). % 222.01/222.12 cnf(3342,plain, % 222.01/222.12 (E(f4(a1,x33421,a1),f4(a2,x33421,a2))), % 222.01/222.12 inference(scs_inference,[],[1938,2])). % 222.01/222.12 cnf(3343,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(x33431,f9(f9(x33432,f9(a7,x33433)),x33434)))), % 222.01/222.12 inference(scs_inference,[],[1938,3238,2,41])). % 222.01/222.12 cnf(3345,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(f9(f9(x33451,f9(a7,x33452)),x33453),x33454))), % 222.01/222.12 inference(scs_inference,[],[1938,3238,2,41,42])). % 222.01/222.12 cnf(3349,plain, % 222.01/222.12 (P2(f9(f4(x33491,a1,a1),a1),f4(x33491,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[96,1938,3238,3272,2104,2,41,42,29,14])). % 222.01/222.12 cnf(3350,plain, % 222.01/222.12 (E(x33501,f9(x33501,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3351,plain, % 222.01/222.12 (E(f9(f3(a2,a2),f3(a2,a2)),f3(a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,22,2036,1938,3238,3272,2104,2,41,42,29,14,3])). % 222.01/222.12 cnf(3358,plain, % 222.01/222.12 (~P3(x33581,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3372,plain, % 222.01/222.12 (P3(f4(a8,a1,f9(a2,a1)),a7)), % 222.01/222.12 inference(scs_inference,[],[19,122,44,3358,96,3350,22,1514,1521,2893,2036,1938,2212,3238,2002,2015,3272,2104,3274,3064,2613,2,41,42,29,14,3,11,15,12,13,43,38,28,32,27,33])). % 222.01/222.12 cnf(3378,plain, % 222.01/222.12 (E(f4(x33781,a1,a1),f4(x33781,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[1968,2])). % 222.01/222.12 cnf(3379,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(x33791,f9(x33792,f9(f9(a7,x33793),x33794))))), % 222.01/222.12 inference(scs_inference,[],[1968,3272,2,41])). % 222.01/222.12 cnf(3381,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(f9(x33811,f9(f9(a7,x33812),x33813)),x33814))), % 222.01/222.12 inference(scs_inference,[],[1968,3272,2,41,42])). % 222.01/222.12 cnf(3385,plain, % 222.01/222.12 (P2(f9(f9(f3(a1,a1),a1),a1),f3(a2,a2))), % 222.01/222.12 inference(scs_inference,[],[96,1968,3272,3274,2867,2,41,42,29,14])). % 222.01/222.12 cnf(3386,plain, % 222.01/222.12 (E(x33861,f9(x33861,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3391,plain, % 222.01/222.12 (E(x33911,f9(x33911,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3395,plain, % 222.01/222.12 (~P3(x33951,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3400,plain, % 222.01/222.12 (P3(f4(a1,a1,a6),a6)), % 222.01/222.12 inference(scs_inference,[],[44,3395,96,3386,3391,22,16,107,3238,1938,1968,1961,3272,2104,3274,2157,3308,2867,2593,2,41,42,29,14,11,3,15,12,13,43,27,38])). % 222.01/222.12 cnf(3414,plain, % 222.01/222.12 (E(f9(f9(f9(a2,a2),f9(a2,a2)),x34141),f9(f9(a2,a1),x34141))), % 222.01/222.12 inference(scs_inference,[],[2767,2])). % 222.01/222.12 cnf(3421,plain, % 222.01/222.12 (P2(f9(f9(f4(a1,a1,a1),a1),a1),f4(a2,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[96,2767,3274,3308,2997,2,41,42,29,14])). % 222.01/222.12 cnf(3460,plain, % 222.01/222.12 (P2(f9(f9(f3(a2,a2),a1),a1),f3(a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,3308,1882,3310,3028,2,41,42,29,14])). % 222.01/222.12 cnf(3461,plain, % 222.01/222.12 (E(x34611,f9(x34611,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3462,plain, % 222.01/222.12 (P1(f9(a1,f9(a1,a2)))), % 222.01/222.12 inference(scs_inference,[],[96,3308,1882,3310,2876,3028,2608,2,41,42,29,14,11])). % 222.01/222.12 cnf(3466,plain, % 222.01/222.12 (E(x34661,f9(x34661,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3468,plain, % 222.01/222.12 (~P3(x34681,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3484,plain, % 222.01/222.12 (P3(f4(a1,a1,a5),a7)), % 222.01/222.12 inference(scs_inference,[],[44,3468,96,3461,3466,16,18,3274,3106,820,3308,2298,1882,113,3310,2224,2021,2876,3343,3028,2608,2,41,42,29,14,11,3,15,13,12,43,27,38,28,32,40,33])). % 222.01/222.12 cnf(3492,plain, % 222.01/222.12 (E(f9(f9(a1,a1),x34921),f9(f9(a2,a2),x34921))), % 222.01/222.12 inference(scs_inference,[],[2662,2])). % 222.01/222.12 cnf(3493,plain, % 222.01/222.12 (P3(f4(a5,a8,a5),f9(f9(f9(x34931,f9(a8,x34932)),x34933),x34934))), % 222.01/222.12 inference(scs_inference,[],[3310,2662,2,42])). % 222.01/222.12 cnf(3495,plain, % 222.01/222.12 (P3(f4(a5,a8,a5),f9(x34951,f9(f9(x34952,f9(a8,x34953)),x34954)))), % 222.01/222.12 inference(scs_inference,[],[3310,2662,2,42,41])). % 222.01/222.12 cnf(3500,plain, % 222.01/222.12 (E(x35001,f9(x35001,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3508,plain, % 222.01/222.12 (~P3(x35081,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3510,plain, % 222.01/222.12 (~P3(x35101,f9(a1,f9(a1,a1)))), % 222.01/222.12 inference(scs_inference,[],[44,3508,96,3500,51,2720,3106,3000,190,967,3310,2946,2662,151,3343,3062,2701,2,42,41,29,14,3,11,15,13,12,43])). % 222.01/222.12 cnf(3515,plain, % 222.01/222.12 (~P3(x35151,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3521,plain, % 222.01/222.12 (~P3(x35211,f9(f9(a2,a1),f9(f9(a2,a1),f9(a2,a1))))), % 222.01/222.12 inference(scs_inference,[],[44,3508,3515,96,3500,22,92,51,2720,3106,3000,190,967,3310,2946,2662,151,3343,1857,3062,2701,2,42,41,29,14,3,11,15,13,12,43,38,36,28])). % 222.01/222.12 cnf(3533,plain, % 222.01/222.12 (E(f9(f9(f9(a2,a1),f9(a2,a2)),x35331),f9(f9(a2,a1),x35331))), % 222.01/222.12 inference(scs_inference,[],[2813,2])). % 222.01/222.12 cnf(3534,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(x35341,f9(x35342,f9(x35343,f9(x35344,a7)))))), % 222.01/222.12 inference(scs_inference,[],[2946,2813,2,41])). % 222.01/222.12 cnf(3536,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(x35361,f9(x35362,f9(x35363,a7))),x35364))), % 222.01/222.12 inference(scs_inference,[],[2946,2813,2,41,42])). % 222.01/222.12 cnf(3543,plain, % 222.01/222.12 (P2(f9(f9(f3(a2,a1),a1),a1),f3(a1,a2))), % 222.01/222.12 inference(scs_inference,[],[96,2946,2813,3250,3510,3134,2,41,42,32,29,14])). % 222.01/222.12 cnf(3544,plain, % 222.01/222.12 (E(x35441,f9(x35441,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3546,plain, % 222.01/222.12 (E(x35461,f9(x35461,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3554,plain, % 222.01/222.12 (~P3(x35541,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3561,plain, % 222.01/222.12 (~P3(x35611,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3563,plain, % 222.01/222.12 (~P3(x35631,f9(f9(a2,a2),a1))), % 222.01/222.12 inference(scs_inference,[],[44,3554,3561,96,3544,3546,22,51,57,2946,2662,706,2813,2867,2016,2961,2644,3250,3510,3134,2755,2,41,42,32,29,14,15,11,3,12,13,43,38,36])). % 222.01/222.12 cnf(3567,plain, % 222.01/222.12 (~P3(x35671,f9(f9(a2,a1),f9(f9(a2,a2),f9(a2,a2))))), % 222.01/222.12 inference(scs_inference,[],[44,3554,3561,96,3544,3546,22,51,57,2946,2662,706,2813,2867,2016,2961,2644,3250,3510,3134,2755,2,41,42,32,29,14,15,11,3,12,13,43,38,36,28])). % 222.01/222.12 cnf(3571,plain, % 222.01/222.12 (P3(f4(a1,a5,a1),a7)), % 222.01/222.12 inference(scs_inference,[],[44,3554,3561,96,3544,3546,22,51,18,57,2946,2662,706,2813,2867,2098,2016,2961,2644,3250,3510,3134,2755,2,41,42,32,29,14,15,11,3,12,13,43,38,36,28,40,33])). % 222.01/222.12 cnf(3579,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(x35791,f9(a5,x35792)),x35793))), % 222.01/222.12 inference(scs_inference,[],[706,2650,2,42])). % 222.01/222.12 cnf(3581,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(x35811,f9(x35812,f9(a5,x35813))))), % 222.01/222.12 inference(scs_inference,[],[706,2650,2,42,41])). % 222.01/222.12 cnf(3588,plain, % 222.01/222.12 (P2(f9(f9(f3(a1,a2),a1),a1),f3(a2,a1))), % 222.01/222.12 inference(scs_inference,[],[96,706,2650,3321,3563,2958,2,42,41,32,29,14])). % 222.01/222.12 cnf(3589,plain, % 222.01/222.12 (E(x35891,f9(x35891,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3591,plain, % 222.01/222.12 (~P3(x35911,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3593,plain, % 222.01/222.12 (E(x35931,f9(x35931,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3602,plain, % 222.01/222.12 (~P3(x36021,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3605,plain, % 222.01/222.12 (~P3(x36051,f9(f9(f9(a2,a1),f9(a2,a2)),a1))), % 222.01/222.12 inference(scs_inference,[],[44,3591,3602,96,3589,3593,1514,92,1521,2720,706,145,2544,710,2650,2997,2256,2613,3321,3533,3563,2958,2688,2,42,41,32,29,14,13,15,3,11,12,43,38,36])). % 222.01/222.12 cnf(3609,plain, % 222.01/222.12 (~P3(x36091,f9(f9(f9(a1,a1),a1),f9(f9(a1,a1),a1)))), % 222.01/222.12 inference(scs_inference,[],[44,3591,3602,96,3589,3593,1514,92,1521,2720,706,145,2544,710,2650,2997,2256,2613,3321,3533,3563,2958,2688,2,42,41,32,29,14,13,15,3,11,12,43,38,36,28])). % 222.01/222.12 cnf(3611,plain, % 222.01/222.12 (P1(f9(f9(a1,a1),a1))), % 222.01/222.12 inference(scs_inference,[],[44,3591,3602,96,3589,3593,1514,92,1521,2720,706,145,2544,710,2650,2997,2256,2613,3321,3533,3563,2958,2688,2,42,41,32,29,14,13,15,3,11,12,43,38,36,28,30])). % 222.01/222.12 cnf(3620,plain, % 222.01/222.12 (E(f9(x36201,f9(f9(a2,a1),f9(a2,a2))),f9(x36201,f9(a2,a1)))), % 222.01/222.12 inference(scs_inference,[],[2803,2])). % 222.01/222.12 cnf(3621,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(x36211,f9(f9(a5,x36212),x36213)))), % 222.01/222.12 inference(scs_inference,[],[710,2803,2,41])). % 222.01/222.12 cnf(3623,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(f9(a5,x36231),x36232),x36233))), % 222.01/222.12 inference(scs_inference,[],[710,2803,2,41,42])). % 222.01/222.12 cnf(3628,plain, % 222.01/222.12 (~P3(a7,f4(a1,a1,a5))), % 222.01/222.12 inference(scs_inference,[],[710,2803,3484,3521,2,41,42,32,29])). % 222.01/222.12 cnf(3630,plain, % 222.01/222.12 (P2(f9(f9(f4(a2,a1,a1),a1),a1),f4(a1,a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,710,2803,3484,3521,3094,2,41,42,32,29,14])). % 222.01/222.12 cnf(3631,plain, % 222.01/222.12 (E(x36311,f9(x36311,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3633,plain, % 222.01/222.12 (~P3(x36331,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3637,plain, % 222.01/222.12 (P1(f9(f9(a2,a2),a1))), % 222.01/222.12 inference(scs_inference,[],[44,96,3631,2720,710,265,693,2803,3028,3484,3521,3611,3094,3492,2,41,42,32,29,14,13,12,15,11])). % 222.01/222.12 cnf(3645,plain, % 222.01/222.12 (~P3(x36451,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3648,plain, % 222.01/222.12 (~P3(x36481,f9(f9(f9(a2,a2),f9(a2,a2)),a1))), % 222.01/222.12 inference(scs_inference,[],[44,3633,3645,96,3631,22,1521,57,2720,710,265,2279,693,2803,3028,2731,2645,3484,3521,3611,3094,3414,3492,2,41,42,32,29,14,13,12,15,11,3,43,38,36])). % 222.01/222.12 cnf(3662,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(x36621,f9(x36622,a5)),x36623))), % 222.01/222.12 inference(scs_inference,[],[693,2397,2,42])). % 222.01/222.12 cnf(3664,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(x36641,f9(x36642,f9(x36643,a5))))), % 222.01/222.12 inference(scs_inference,[],[693,2397,2,42,41])). % 222.01/222.12 cnf(3669,plain, % 222.01/222.12 (~P3(a6,f4(a1,a1,a6))), % 222.01/222.12 inference(scs_inference,[],[693,2397,3400,3567,2,42,41,32,29])). % 222.01/222.12 cnf(3671,plain, % 222.01/222.12 (P2(f9(f9(f4(a2,a2,a1),a1),a1),f4(a1,a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,693,2397,3400,3567,3174,2,42,41,32,29,14])). % 222.01/222.12 cnf(3672,plain, % 222.01/222.12 (E(x36721,f9(x36721,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3676,plain, % 222.01/222.12 (~P3(x36761,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3681,plain, % 222.01/222.12 (~P3(x36811,f9(a1,f9(f9(a2,a1),f9(a2,a1))))), % 222.01/222.12 inference(scs_inference,[],[44,3676,96,3672,22,2720,693,293,2846,697,2397,3062,3611,2608,3400,3567,3174,2789,2,42,41,32,29,14,3,13,12,15,11,43])). % 222.01/222.12 cnf(3682,plain, % 222.01/222.12 (~P3(x36821,f9(f9(a2,a1),f9(a2,a1)))), % 222.01/222.12 inference(rename_variables,[],[2846])). % 222.01/222.12 cnf(3686,plain, % 222.01/222.12 (~P3(x36861,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3689,plain, % 222.01/222.12 (~P3(x36891,f9(a1,f9(f9(a2,a1),f9(a2,a2))))), % 222.01/222.12 inference(scs_inference,[],[44,3676,3686,96,3672,22,1521,2720,693,293,2846,3682,697,2397,3062,3611,2738,2608,3400,3620,3567,3174,2789,2,42,41,32,29,14,3,13,12,15,11,43,38,36])). % 222.01/222.12 cnf(3693,plain, % 222.01/222.12 (~P3(x36931,f9(f9(f9(a1,a1),a1),f9(a1,a2)))), % 222.01/222.12 inference(scs_inference,[],[44,3676,3686,96,3672,22,1521,2720,693,293,2846,3682,697,2397,3062,3611,2738,2608,3400,3620,3567,3174,2789,2,42,41,32,29,14,3,13,12,15,11,43,38,36,28])). % 222.01/222.12 cnf(3702,plain, % 222.01/222.12 (E(f9(a1,a1),a2)), % 222.01/222.12 inference(scs_inference,[],[2413,2])). % 222.01/222.12 cnf(3703,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(f9(x37031,a5),x37032),x37033))), % 222.01/222.12 inference(scs_inference,[],[697,2413,2,42])). % 222.01/222.12 cnf(3705,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(x37051,f9(f9(x37052,a5),x37053)))), % 222.01/222.12 inference(scs_inference,[],[697,2413,2,42,41])). % 222.01/222.12 cnf(3713,plain, % 222.01/222.12 (E(x37131,f9(x37131,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3715,plain, % 222.01/222.12 (~P3(x37151,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(3717,plain, % 222.01/222.12 (E(x37171,f9(x37171,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3731,plain, % 222.01/222.12 (~P3(x37311,f9(f9(a2,a2),f9(f9(a1,a1),a1)))), % 222.01/222.12 inference(scs_inference,[],[44,3715,96,3713,3717,16,1538,2720,697,320,3611,1977,2413,3134,1874,2789,3571,3579,3693,3314,2743,2,42,41,32,29,14,13,3,15,12,11,27,43,38,28])). % 222.01/222.12 cnf(3742,plain, % 222.01/222.12 (E(f9(a1,a2),a2)), % 222.01/222.12 inference(scs_inference,[],[2453,2])). % 222.01/222.12 cnf(3752,plain, % 222.01/222.12 (P2(f9(f9(f9(f3(a2,a1),a1),a1),a1),f3(a1,a2))), % 222.01/222.12 inference(scs_inference,[],[96,3343,2453,3579,3731,3543,2,42,41,32,29,14])). % 222.01/222.12 cnf(3753,plain, % 222.01/222.12 (E(x37531,f9(x37531,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3755,plain, % 222.01/222.12 (E(x37551,f9(x37551,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3759,plain, % 222.01/222.12 (E(x37591,f9(x37591,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(3765,plain, % 222.01/222.12 (~P3(f4(a2,a2,a2),f9(f4(a2,a2,a2),f4(a2,a2,a2)))), % 222.01/222.12 inference(scs_inference,[],[44,96,3753,3755,3759,16,3611,3343,2013,2453,3579,2958,2743,3581,3731,3543,2839,2,42,41,32,29,14,3,13,12,15,11,27,43])). % 222.01/222.12 cnf(3783,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(f9(x37831,f9(a5,x37832)),x37833),x37834))), % 222.01/222.12 inference(scs_inference,[],[3579,2615,2,42])). % 222.01/222.12 cnf(3785,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(x37851,f9(f9(x37852,f9(a5,x37853)),x37854)))), % 222.01/222.12 inference(scs_inference,[],[3579,2615,2,42,41])). % 222.01/222.12 cnf(3819,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(x38191,f9(x38192,f9(a5,x38193))),x38194))), % 222.01/222.12 inference(scs_inference,[],[3581,2789,2,42])). % 222.01/222.12 cnf(3830,plain, % 222.01/222.12 (E(f9(f4(a1,a1,a1),f4(a1,a1,a1)),f4(a2,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[96,22,3581,2789,3621,3271,3609,2113,2,42,32,41,29,14,3])). % 222.01/222.12 cnf(3902,plain, % 222.01/222.12 (E(f9(f9(f4(a2,a2,a2),f4(a2,a2,a2)),f9(f4(a2,a2,a2),f4(a2,a2,a2))),f4(a1,a1,a1))), % 222.01/222.12 inference(scs_inference,[],[44,96,22,3623,2613,3662,3664,3316,3605,3385,2,32,42,41,29,14,13,3])). % 222.01/222.12 cnf(3932,plain, % 222.01/222.12 (P2(f9(f9(f9(f4(a1,a1,a1),a1),a1),a1),f4(a2,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[96,3662,2645,3664,3648,3421,2,42,32,41,29,14])). % 222.01/222.12 cnf(3936,plain, % 222.01/222.12 (E(f9(f9(f3(a2,a2),f3(a2,a2)),f9(f3(a2,a2),f3(a2,a2))),f3(a1,a1))), % 222.01/222.12 inference(scs_inference,[],[44,96,22,3662,2645,3664,3703,3351,3648,3421,2,42,32,41,29,14,13,3])). % 222.01/222.12 cnf(3967,plain, % 222.01/222.12 (P2(f9(f9(f9(f3(a2,a2),a1),a1),a1),f3(a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,3664,2608,3703,3681,3460,2,42,32,41,29,14])). % 222.01/222.12 cnf(3971,plain, % 222.01/222.12 (E(f9(f9(f4(a1,a1,a1),f4(a1,a1,a1)),f9(f4(a1,a1,a1),f4(a1,a1,a1))),f4(a2,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[44,96,22,3664,2608,3703,3705,3830,3681,3460,2,42,32,41,29,14,13,3])). % 222.01/222.12 cnf(3992,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(f9(f9(x39921,a5),x39922),x39923),x39924))), % 222.01/222.12 inference(scs_inference,[],[3703,2597,2,42])). % 222.01/222.12 cnf(3997,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(x39971,f9(f9(f9(x39972,a5),x39973),x39974)))), % 222.01/222.12 inference(scs_inference,[],[3703,2597,3689,2,42,32,41])). % 222.01/222.12 cnf(4001,plain, % 222.01/222.12 (P2(f9(f9(f9(f3(a1,a2),a1),a1),a1),f3(a2,a1))), % 222.01/222.12 inference(scs_inference,[],[96,3703,2597,3705,3689,3588,2,42,32,41,29,14])). % 222.01/222.12 cnf(4026,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(f9(x40261,f9(f9(x40262,a5),x40263)),x40264))), % 222.01/222.12 inference(scs_inference,[],[3705,2743,2,42])). % 222.01/222.12 cnf(4028,plain, % 222.01/222.12 (P3(f4(a5,a8,a8),f9(x40281,f9(x40282,f9(f9(x40283,a5),x40284))))), % 222.01/222.12 inference(scs_inference,[],[3705,2743,2,42,41])). % 222.01/222.12 cnf(4060,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(x40601,f9(f9(f9(x40602,f9(a7,x40603)),x40604),x40605)))), % 222.01/222.12 inference(scs_inference,[],[3345,2839,2,41])). % 222.01/222.12 cnf(4062,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(f9(f9(f9(x40621,f9(a7,x40622)),x40623),x40624),x40625))), % 222.01/222.12 inference(scs_inference,[],[3345,2839,2,41,42])). % 222.01/222.12 cnf(4068,plain, % 222.01/222.12 (P2(f9(f9(f9(f4(a2,a1,a1),a1),a1),a1),f4(a1,a1,a1))), % 222.01/222.12 inference(scs_inference,[],[44,96,3345,2839,3379,3381,3630,2,41,42,29,13,14])). % 222.01/222.12 cnf(4070,plain, % 222.01/222.12 (E(f9(f9(f4(x40701,x40702,a2),f4(x40701,x40702,a2)),f9(f4(x40701,x40702,a2),f4(x40701,x40702,a2))),f4(x40701,x40702,a1))), % 222.01/222.12 inference(scs_inference,[],[44,96,22,3345,2839,3379,3381,3060,3630,2,41,42,29,13,14,3])). % 222.01/222.12 cnf(4089,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(f9(x40891,f9(x40892,f9(f9(a7,x40893),x40894))),x40895))), % 222.01/222.12 inference(scs_inference,[],[3379,3316,2,42])). % 222.01/222.12 cnf(4091,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(x40911,f9(x40912,f9(x40913,f9(f9(a7,x40914),x40915)))))), % 222.01/222.12 inference(scs_inference,[],[3379,3316,2,42,41])). % 222.01/222.12 cnf(4097,plain, % 222.01/222.12 (P2(f9(f9(f9(f4(a2,a2,a1),a1),a1),a1),f4(a1,a1,a1))), % 222.01/222.12 inference(scs_inference,[],[96,22,3379,3381,3316,3199,3671,2,42,41,29,3,14])). % 222.01/222.12 cnf(4122,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(f9(f9(x41221,f9(f9(a7,x41222),x41223)),x41224),x41225))), % 222.01/222.12 inference(scs_inference,[],[3381,3351,2,42])). % 222.01/222.12 cnf(4124,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(x41241,f9(f9(x41242,f9(f9(a7,x41243),x41244)),x41245)))), % 222.01/222.12 inference(scs_inference,[],[3381,3351,2,42,41])). % 222.01/222.12 cnf(4292,plain, % 222.01/222.12 (E(x42921,f9(x42921,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(4297,plain, % 222.01/222.12 (E(f9(f3(x42971,a1),f3(x42971,a1)),f3(x42971,a2))), % 222.01/222.12 inference(scs_inference,[],[44,96,4292,22,3493,3495,3026,3752,3534,3129,3967,2,41,42,29,14,15,13,3])). % 222.01/222.12 cnf(4350,plain, % 222.01/222.12 (E(x43501,f9(x43501,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(4355,plain, % 222.01/222.12 (E(f9(f3(a1,x43551),f3(a1,x43551)),f3(a2,x43551))), % 222.01/222.12 inference(scs_inference,[],[44,96,4350,22,3534,3536,4297,3932,3783,3235,4001,2,42,41,29,14,15,13,3])). % 222.01/222.12 cnf(4410,plain, % 222.01/222.12 (E(x44101,f9(x44101,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(4415,plain, % 222.01/222.12 (E(f9(f4(a1,x44151,a1),f4(a1,x44151,a1)),f4(a2,x44151,a2))), % 222.01/222.12 inference(scs_inference,[],[44,96,4410,22,3783,3785,4355,4068,3819,3342,4097,2,42,41,29,14,13,15,3])). % 222.01/222.12 cnf(4795,plain, % 222.01/222.12 (P2(f9(f9(f4(x47951,a1,a1),a1),a1),f4(x47951,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[96,3992,3997,2755,3349,2,42,41,29,14])). % 222.01/222.12 cnf(4867,plain, % 222.01/222.12 (P2(f9(f9(f9(f4(x48671,a1,a1),a1),a1),a1),f4(x48671,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[96,4026,4028,2593,4795,2,42,41,29,14])). % 222.01/222.12 cnf(4928,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(f9(x49281,f9(f9(x49282,a8),x49283)),x49284))), % 222.01/222.12 inference(scs_inference,[],[3018,3902,2,42])). % 222.01/222.12 cnf(4930,plain, % 222.01/222.12 (P3(f4(a8,a5,a5),f9(x49301,f9(x49302,f9(f9(x49303,a8),x49304))))), % 222.01/222.12 inference(scs_inference,[],[3018,3902,2,42,41])). % 222.01/222.12 cnf(4964,plain, % 222.01/222.12 (P3(f4(a1,a1,a8),f9(f9(f9(f9(a8,x49641),x49642),x49643),x49644))), % 222.01/222.12 inference(scs_inference,[],[3092,3936,2,42])). % 222.01/222.12 cnf(4966,plain, % 222.01/222.12 (P3(f4(a1,a1,a8),f9(x49661,f9(f9(f9(a8,x49662),x49663),x49664)))), % 222.01/222.12 inference(scs_inference,[],[3092,3936,2,42,41])). % 222.01/222.12 cnf(4972,plain, % 222.01/222.12 (~E(f9(f9(a2,a2),f9(a2,a2)),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[44,25,3092,4060,4928,3936,2682,2,42,41,29,13,14])). % 222.01/222.12 cnf(5028,plain, % 222.01/222.12 (E(f4(x50281,f9(f9(a2,a1),f9(a2,a1)),x50282),f4(x50281,f9(a2,a2),x50282))), % 222.01/222.12 inference(scs_inference,[],[2708,2])). % 222.01/222.12 cnf(5037,plain, % 222.01/222.12 (~E(f9(f9(a2,a2),f9(a1,a1)),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[44,25,846,4930,2708,4964,2783,2,42,41,29,13,14])). % 222.01/222.12 cnf(5067,plain, % 222.01/222.12 (~P3(x50671,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(5071,plain, % 222.01/222.12 (E(x50711,f9(x50711,a1))), % 222.01/222.12 inference(rename_variables,[],[96])). % 222.01/222.12 cnf(5076,plain, % 222.01/222.12 (~P3(x50761,f9(a1,f9(f9(a2,a2),a1)))), % 222.01/222.12 inference(scs_inference,[],[44,5067,96,5071,22,25,4928,4930,4964,2709,4867,3563,4966,5028,2899,2,42,41,29,13,14,15,12,3,43])). % 222.01/222.12 cnf(5111,plain, % 222.01/222.12 (~E(f9(f9(a2,a1),f9(a2,a2)),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[44,25,4930,4966,4062,3971,5076,2948,2,42,41,29,32,13,14])). % 222.01/222.12 cnf(5179,plain, % 222.01/222.12 (E(f4(x51791,x51792,f9(f9(a2,a1),f9(a2,a1))),f4(x51791,x51792,f9(a2,a2)))), % 222.01/222.12 inference(scs_inference,[],[2712,2])). % 222.01/222.12 cnf(5188,plain, % 222.01/222.12 (~E(f9(f9(a1,a1),f9(a2,a2)),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[44,25,4966,4089,2712,4091,3117,2,42,41,29,13,14])). % 222.01/222.12 cnf(5221,plain, % 222.01/222.12 (~P3(x52211,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(5229,plain, % 222.01/222.12 (~P3(x52291,f9(a1,f9(a1,f9(a1,a1))))), % 222.01/222.12 inference(scs_inference,[],[44,5221,96,22,25,2720,864,105,4091,2713,3510,271,4122,5179,3157,2,42,29,41,13,14,15,12,3,43])). % 222.01/222.12 cnf(5259,plain, % 222.01/222.12 (~E(f9(f9(a2,a1),f9(a1,a1)),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[44,96,25,2720,526,181,4122,295,4124,5229,4070,3225,2,42,41,29,32,13,15,12,14])). % 222.01/222.12 cnf(5847,plain, % 222.01/222.12 (~P3(f3(f9(a5,a8),a7),a7)), % 222.01/222.12 inference(scs_inference,[],[25,37])). % 222.01/222.12 cnf(5853,plain, % 222.01/222.12 (E(f3(x58531,f9(x58532,x58532)),f3(x58531,x58532))), % 222.01/222.12 inference(scs_inference,[],[25,22,1853,37,5,31,7,10])). % 222.01/222.12 cnf(5857,plain, % 222.01/222.12 (E(f3(f9(x58571,x58571),x58572),f3(x58571,x58572))), % 222.01/222.12 inference(scs_inference,[],[25,22,1853,1855,37,5,31,7,10,30,8,9])). % 222.01/222.12 cnf(5871,plain, % 222.01/222.12 (P3(f3(f9(a5,a8),a7),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[18,25,22,2799,2914,3229,3202,2770,1853,2814,1855,3563,3637,37,5,31,7,10,30,8,9,6,4,34,26,35,36,33,32])). % 222.01/222.12 cnf(5877,plain, % 222.01/222.12 (~P3(f3(f9(a5,a8),f9(a1,a7)),a7)), % 222.01/222.12 inference(scs_inference,[],[18,25,22,2799,2914,3229,3628,3202,2770,1853,2814,1855,3563,3637,37,5,31,7,10,30,8,9,6,4,34,26,35,36,33,32,43,42,41])). % 222.01/222.12 cnf(5882,plain, % 222.01/222.12 (E(f9(x58821,x58822),f9(x58822,x58821))), % 222.01/222.12 inference(rename_variables,[],[23])). % 222.01/222.12 cnf(5884,plain, % 222.01/222.12 (E(f9(x58841,x58841),x58841)), % 222.01/222.12 inference(rename_variables,[],[22])). % 222.01/222.12 cnf(5885,plain, % 222.01/222.12 (~P2(f9(f9(a5,a8),f9(a5,a8)),a7)), % 222.01/222.12 inference(scs_inference,[],[18,25,22,5884,23,2799,2914,5111,3229,2337,3628,3202,2770,1853,2814,1855,3563,3637,37,5,31,7,10,30,8,9,6,4,34,26,35,36,33,32,43,42,41,29,3,15,14])). % 222.01/222.12 cnf(5888,plain, % 222.01/222.12 (~P3(f3(f9(a5,a8),f9(a1,a7)),f9(a7,a1))), % 222.01/222.12 inference(scs_inference,[],[18,25,22,5884,23,5882,2799,2914,4972,5111,3229,2337,3628,3202,2770,1853,2814,1855,3563,3637,37,5,31,7,10,30,8,9,6,4,34,26,35,36,33,32,43,42,41,29,3,15,14,2,13])). % 222.01/222.12 cnf(5893,plain, % 222.01/222.12 (~P3(f3(f9(a5,a8),f9(a7,a1)),f9(a7,a1))), % 222.01/222.12 inference(scs_inference,[],[2136,37])). % 222.01/222.12 cnf(5912,plain, % 222.01/222.12 (P3(f3(f9(a5,a8),f9(a7,a1)),f9(a5,a8))), % 222.01/222.12 inference(scs_inference,[],[18,20,3070,5871,5847,2136,2663,3702,3611,37,5,9,10,7,34,26,8,6,4,35,36,33,32])). % 222.01/222.12 cnf(5914,plain, % 222.01/222.12 (P3(f3(f9(a5,a8),a7),a8)), % 222.01/222.12 inference(scs_inference,[],[18,20,3070,5871,5847,2136,2663,3702,3611,37,5,9,10,7,34,26,8,6,4,35,36,33,32,43])). % 222.01/222.12 cnf(5922,plain, % 222.01/222.12 (E(f3(f9(x59221,x59221),f9(x59222,x59222)),f3(x59221,x59222))), % 222.01/222.12 inference(scs_inference,[],[18,21,20,3070,5853,5857,5871,5847,2136,2663,3702,3611,37,5,9,10,7,34,26,8,6,4,35,36,33,32,43,42,29,15,3])). % 222.01/222.12 cnf(5925,plain, % 222.01/222.12 (E(f9(x59251,x59251),x59251)), % 222.01/222.12 inference(rename_variables,[],[22])). % 222.01/222.12 cnf(5932,plain, % 222.01/222.12 (~P3(f4(a2,a1,a1),f4(a2,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[18,21,16,22,5925,20,3070,5037,5853,5857,5871,3765,5847,2508,2136,2663,3702,3378,3611,37,5,9,10,7,34,26,8,6,4,35,36,33,32,43,42,29,15,3,14,2,13,11,12,41])). % 222.01/222.12 cnf(5953,plain, % 222.01/222.12 (P3(f3(f9(a8,a5),f9(a7,a2)),f9(a8,a5))), % 222.01/222.12 inference(scs_inference,[],[18,5888,5893,5912,5877,2141,2814,3742,3462,37,26,5,34,9,7,10,4,8,6,35,36,33,32])). % 222.01/222.12 cnf(5964,plain, % 222.01/222.12 (E(f9(x59641,x59641),x59641)), % 222.01/222.12 inference(rename_variables,[],[22])). % 222.01/222.12 cnf(5971,plain, % 222.01/222.12 (~P3(f9(f4(a2,a1,a1),f4(a2,a1,a1)),f4(a2,a2,a2))), % 222.01/222.12 inference(scs_inference,[],[18,25,24,22,5964,20,23,5188,5259,5888,5893,5912,5932,5885,3669,5877,2141,2814,4415,3742,3611,3462,37,26,5,34,9,7,10,4,8,6,35,36,33,32,43,42,29,3,15,14,2,13,11,12])). % 222.01/222.12 cnf(6595,plain, % 222.01/222.12 (~P3(x65951,a1)), % 222.01/222.12 inference(rename_variables,[],[44])). % 222.01/222.12 cnf(6600,plain, % 222.01/222.12 ($false), % 222.01/222.12 inference(scs_inference,[],[44,6595,96,23,19,228,5953,3000,3372,5847,5922,2134,424,5914,5971,31,30,37,2000,26,9,10,7,5,6,4,8,32,42,41,29,2,34,35,33]), % 222.01/222.12 ['proof']). % 222.01/222.12 % SZS output end Proof % 222.01/222.12 % Total time :221.270000s %------------------------------------------------------------------------------