%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : COL100-1 : TPTP v8.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n032.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 04:45:09 EDT 2024 % Result : Unsatisfiable 262.02s 262.52s % Output : CNFRefutation 262.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.11 % Problem : COL100-1 : TPTP v8.2.0. Released v2.7.0. % 0.09/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n032.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Tue Jun 18 15:44:38 EDT 2024 % 0.10/0.31 % CPUTime : % 0.46/0.56 start to proof:theBenchmark % 261.93/262.50 %------------------------------------------- % 261.93/262.50 % File :CSE---1.7 % 261.93/262.50 % Problem :theBenchmark % 261.93/262.50 % Transform :cnf % 261.93/262.50 % Format :tptp:raw % 261.93/262.50 % Command :java -jar mcs_scs.jar %d %s % 261.93/262.50 % 261.93/262.50 % Result :Theorem 261.370000s % 261.93/262.50 % Output :CNFRefutation 261.370000s % 261.93/262.50 %------------------------------------------- % 262.02/262.52 %-------------------------------------------------------------------------- % 262.02/262.52 % File : COL100-1 : TPTP v8.2.0. Released v2.7.0. % 262.02/262.52 % Domain : Combinatory Logic % 262.02/262.52 % Problem : diamond_trancl_2c1 % 262.02/262.52 % Version : Reduced > Especial. % 262.02/262.52 % English : diamond(r) ==> diamond(r^+) % 262.02/262.52 % 262.02/262.52 % Refs : [Men03] Meng (2003), Email to G. Sutcliffe % 262.02/262.52 % Source : [Men03] % 262.02/262.52 % Names : % 262.02/262.52 % 262.02/262.52 % Status : Unsatisfiable % 262.02/262.52 % Rating : 0.00 v8.1.0, 0.11 v7.5.0, 0.10 v7.4.0, 0.22 v7.2.0, 0.25 v7.1.0, 0.29 v6.3.0, 0.33 v6.2.0, 0.00 v6.1.0, 0.20 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.22 v4.0.1, 0.17 v3.3.0, 0.14 v3.2.0, 0.00 v2.7.0 % 262.02/262.52 % Syntax : Number of clauses : 18 ( 8 unt; 0 nHn; 17 RR) % 262.02/262.52 % Number of literals : 35 ( 10 equ; 21 neg) % 262.02/262.52 % Maximal clause size : 4 ( 1 avg) % 262.02/262.52 % Maximal term depth : 3 ( 1 avg) % 262.02/262.52 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 262.02/262.52 % Number of functors : 12 ( 12 usr; 7 con; 0-4 aty) % 262.02/262.52 % Number of variables : 35 ( 9 sgn) % 262.02/262.52 % SPC : CNF_UNS_RFO_SEQ_HRN % 262.02/262.52 % 262.02/262.52 % Comments : Problem coming out of an Isabelle proof. % 262.02/262.52 %-------------------------------------------------------------------------- % 262.02/262.52 %----axioms from CombZF.thy. % 262.02/262.52 %----free algebra for K, S, comb_app(P,Q). % 262.02/262.52 cnf(k_s,axiom, % 262.02/262.52 combK != combS ). % 262.02/262.52 % 262.02/262.52 cnf(k_app,axiom, % 262.02/262.52 combK != comb_app(P,Q) ). % 262.02/262.52 % 262.02/262.52 cnf(s_app,axiom, % 262.02/262.52 combS != comb_app(P,Q) ). % 262.02/262.52 % 262.02/262.52 cnf(app_app1,axiom, % 262.02/262.52 ( comb_app(P1,Q1) != comb_app(P2,Q2) % 262.02/262.52 | P1 = P2 ) ). % 262.02/262.52 % 262.02/262.52 cnf(app_app2,axiom, % 262.02/262.52 ( comb_app(P1,Q1) != comb_app(P2,Q2) % 262.02/262.52 | Q1 = Q2 ) ). % 262.02/262.52 % 262.02/262.52 cnf(app_app3,axiom, % 262.02/262.52 ( P1 != P2 % 262.02/262.52 | Q1 != Q2 % 262.02/262.52 | comb_app(P1,Q1) = comb_app(P2,Q2) ) ). % 262.02/262.52 % 262.02/262.52 %----axiom r_intro_trancl, trans_trancl, transD, diamond_strip_lemmaD are needed here locally. % 262.02/262.52 cnf(r_into_trancl,axiom, % 262.02/262.52 ( ~ member(pair(A,B),R) % 262.02/262.52 | member(pair(A,B),trancl(R)) ) ). % 262.02/262.52 % 262.02/262.52 cnf(trans_trancl,axiom, % 262.02/262.52 trans(trancl(R)) ). % 262.02/262.52 % 262.02/262.52 cnf(transD,axiom, % 262.02/262.52 ( ~ trans(R) % 262.02/262.52 | ~ member(pair(A,B),R) % 262.02/262.52 | ~ member(pair(B,C),R) % 262.02/262.52 | member(pair(A,C),R) ) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_strip_lemmaD1,axiom, % 262.02/262.52 ( ~ diamond(R) % 262.02/262.52 | ~ member(pair(X,Y),trancl(R)) % 262.02/262.52 | ~ member(pair(X,YP),R) % 262.02/262.52 | member(pair(YP,diamond_strip_lemmaD_sk1(X,Y,YP,R)),trancl(R)) ) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_strip_lemmaD2,axiom, % 262.02/262.52 ( ~ diamond(R) % 262.02/262.52 | ~ member(pair(X,Y),trancl(R)) % 262.02/262.52 | ~ member(pair(X,YP),R) % 262.02/262.52 | member(pair(Y,diamond_strip_lemmaD_sk1(X,Y,YP,R)),R) ) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_trancl_2h1,hypothesis, % 262.02/262.52 diamond(r) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_trancl_2h2,hypothesis, % 262.02/262.52 member(pair(y,ya),trancl(r)) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_trancl_2h3,hypothesis, % 262.02/262.52 member(pair(ya,z),r) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_trancl_2h4,hypothesis, % 262.02/262.52 ( ~ member(pair(y,YP),trancl(r)) % 262.02/262.52 | member(pair(ya,sk1(YP)),trancl(r)) ) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_trancl_2h5,hypothesis, % 262.02/262.52 ( ~ member(pair(y,YP),trancl(r)) % 262.02/262.52 | member(pair(YP,sk1(YP)),trancl(r)) ) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_trancl_2c1,negated_conjecture, % 262.02/262.52 member(pair(y,yp),trancl(r)) ). % 262.02/262.52 % 262.02/262.52 cnf(diamond_trancl_2c2,negated_conjecture, % 262.02/262.52 ( ~ member(pair(z,ZA),trancl(r)) % 262.02/262.52 | ~ member(pair(yp,ZA),trancl(r)) ) ). % 262.02/262.52 % 262.02/262.52 %-------------------------------------------------------------------------- % 262.02/262.52 %------------------------------------------- % 262.02/262.52 % Proof found % 262.02/262.52 % SZS status Theorem for theBenchmark % 262.02/262.52 % SZS output start Proof % 262.02/262.54 %ClaNum:34(EqnAxiom:17) % 262.02/262.54 %VarNum:66(SingletonVarNum:31) % 262.02/262.54 %MaxLitNum:4 % 262.02/262.54 %MaxfuncDepth:2 % 262.02/262.54 %SharedTerms:16 % 262.02/262.54 %goalClause: 22 31 % 262.02/262.54 %singleGoalClaCount:1 % 262.02/262.54 [18]P1(a1) % 262.02/262.54 [23]~E(a3,a4) % 262.02/262.54 [20]P3(f2(a9,a11),a1) % 262.02/262.54 [21]P3(f2(a10,a9),f7(a1)) % 262.02/262.54 [22]P3(f2(a10,a12),f7(a1)) % 262.02/262.54 [19]P2(f7(x191)) % 262.02/262.54 [24]~E(f5(x241,x242),a3) % 262.02/262.54 [25]~E(f5(x251,x252),a4) % 262.02/262.54 [31]~P3(f2(a12,x311),f7(a1))+~P3(f2(a11,x311),f7(a1)) % 262.02/262.54 [29]~P3(f2(a10,x291),f7(a1))+P3(f2(a9,f8(x291)),f7(a1)) % 262.02/262.54 [30]~P3(f2(a10,x301),f7(a1))+P3(f2(x301,f8(x301)),f7(a1)) % 262.02/262.54 [28]~P3(f2(x281,x282),x283)+P3(f2(x281,x282),f7(x283)) % 262.02/262.54 [26]E(x261,x262)+~E(f5(x263,x261),f5(x264,x262)) % 262.02/262.54 [27]E(x271,x272)+~E(f5(x271,x273),f5(x272,x274)) % 262.02/262.54 [32]~P2(x323)+~P3(f2(x321,x324),x323)+P3(f2(x321,x322),x323)+~P3(f2(x324,x322),x323) % 262.02/262.54 [33]~P1(x334)+~P3(f2(x332,x333),x334)+~P3(f2(x332,x331),f7(x334))+P3(f2(x331,f6(x332,x331,x333,x334)),x334) % 262.02/262.54 [34]~P1(x344)+~P3(f2(x342,x341),x344)+~P3(f2(x342,x343),f7(x344))+P3(f2(x341,f6(x342,x343,x341,x344)),f7(x344)) % 262.02/262.54 %EqnAxiom % 262.02/262.54 [1]E(x11,x11) % 262.02/262.54 [2]E(x22,x21)+~E(x21,x22) % 262.02/262.54 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 262.02/262.54 [4]~E(x41,x42)+E(f7(x41),f7(x42)) % 262.02/262.54 [5]~E(x51,x52)+E(f2(x51,x53),f2(x52,x53)) % 262.02/262.54 [6]~E(x61,x62)+E(f2(x63,x61),f2(x63,x62)) % 262.02/262.54 [7]~E(x71,x72)+E(f6(x71,x73,x74,x75),f6(x72,x73,x74,x75)) % 262.02/262.54 [8]~E(x81,x82)+E(f6(x83,x81,x84,x85),f6(x83,x82,x84,x85)) % 262.02/262.54 [9]~E(x91,x92)+E(f6(x93,x94,x91,x95),f6(x93,x94,x92,x95)) % 262.02/262.54 [10]~E(x101,x102)+E(f6(x103,x104,x105,x101),f6(x103,x104,x105,x102)) % 262.02/262.54 [11]~E(x111,x112)+E(f8(x111),f8(x112)) % 262.02/262.54 [12]~E(x121,x122)+E(f5(x121,x123),f5(x122,x123)) % 262.02/262.54 [13]~E(x131,x132)+E(f5(x133,x131),f5(x133,x132)) % 262.02/262.54 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 262.02/262.54 [15]~P2(x151)+P2(x152)+~E(x151,x152) % 262.02/262.54 [16]P3(x162,x163)+~E(x161,x162)+~P3(x161,x163) % 262.02/262.54 [17]P3(x173,x172)+~E(x171,x172)+~P3(x173,x171) % 262.02/262.54 % 262.02/262.54 %------------------------------------------- % 262.02/262.57 cnf(37,plain, % 262.02/262.57 (P3(x371,f7(a1))+~E(f2(a10,a12),x371)), % 262.02/262.57 inference(scs_inference,[],[22,16])). % 262.02/262.57 cnf(38,plain, % 262.02/262.57 (~E(f2(a10,a12),f2(x381,a10))+P3(f2(x381,a12),f7(a1))), % 262.02/262.57 inference(scs_inference,[],[22,19,16,32])). % 262.02/262.57 cnf(48,plain, % 262.02/262.57 (P3(x481,f7(a1))+~E(f2(a10,a9),x481)), % 262.02/262.57 inference(scs_inference,[],[22,21,17,16])). % 262.02/262.57 cnf(49,plain, % 262.02/262.57 (~E(f2(a10,a9),f2(x491,a10))+P3(f2(x491,a12),f7(a1))), % 262.02/262.57 inference(scs_inference,[],[22,21,19,17,16,32])). % 262.02/262.57 cnf(56,plain, % 262.02/262.57 (~P3(f2(x561,a10),f7(a1))+P3(f2(x561,a12),f7(a1))), % 262.02/262.57 inference(scs_inference,[],[22,21,20,19,17,16,32])). % 262.02/262.57 cnf(68,plain, % 262.02/262.57 (~P3(f2(x681,a10),f7(a1))+P3(f2(x681,a9),f7(a1))), % 262.02/262.57 inference(scs_inference,[],[21,19,32])). % 262.02/262.57 cnf(88,plain, % 262.02/262.57 (~E(f5(x881,a4),f5(x882,a3))), % 262.02/262.57 inference(scs_inference,[],[23,2,26])). % 262.02/262.57 cnf(2118,plain, % 262.02/262.57 (~E(f5(a4,x21181),f5(f5(x21182,x21183),x21184))), % 262.02/262.57 inference(scs_inference,[],[25,2,27])). % 262.02/262.57 cnf(2214,plain, % 262.02/262.57 (~E(x22141,f2(a10,a12))+P3(x22141,f7(a1))), % 262.02/262.57 inference(scs_inference,[],[2,37])). % 262.02/262.57 cnf(2231,plain, % 262.02/262.57 (~E(f5(x22311,f5(x22312,a3)),f5(x22313,f5(x22314,a4)))), % 262.02/262.57 inference(scs_inference,[],[88,2,26])). % 262.02/262.57 cnf(2250,plain, % 262.02/262.57 (~E(f5(f5(x22501,a3),x22502),f5(f5(x22503,a4),x22504))), % 262.02/262.57 inference(scs_inference,[],[88,2,27])). % 262.02/262.57 cnf(2329,plain, % 262.02/262.58 (~E(f2(x23291,a10),f2(a10,a12))+P3(f2(x23291,a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[2,38])). % 262.02/262.58 cnf(3615,plain, % 262.02/262.58 (P3(f2(a10,a12),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[22,28])). % 262.02/262.58 cnf(3623,plain, % 262.02/262.58 (P3(f2(a10,a9),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[21,28])). % 262.02/262.58 cnf(3630,plain, % 262.02/262.58 (P3(f2(a9,a11),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[20,28])). % 262.02/262.58 cnf(3632,plain, % 262.02/262.58 (P3(f2(a10,a11),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,21,20,28,32])). % 262.02/262.58 cnf(3635,plain, % 262.02/262.58 (P3(x36351,f7(a1))+~E(f2(a9,a11),x36351)), % 262.02/262.58 inference(scs_inference,[],[19,21,20,28,32,16])). % 262.02/262.58 cnf(3641,plain, % 262.02/262.58 (P3(f2(a9,a11),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[3630,2231,2,28])). % 262.02/262.58 cnf(3643,plain, % 262.02/262.58 (P3(f2(a10,a11),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[19,3623,3630,2231,2,28,32])). % 262.02/262.58 cnf(3647,plain, % 262.02/262.58 (P3(x36471,f7(a1))+~E(f2(a10,a11),x36471)), % 262.02/262.58 inference(scs_inference,[],[19,3623,3630,3632,2231,2,28,32,3,16])). % 262.02/262.58 cnf(3649,plain, % 262.02/262.58 (~E(f5(f5(x36491,a4),x36492),f5(f5(x36493,a3),x36494))), % 262.02/262.58 inference(scs_inference,[],[2250,2])). % 262.02/262.58 cnf(3675,plain, % 262.02/262.58 (~E(a3,f5(x36751,x36752))), % 262.02/262.58 inference(scs_inference,[],[24,2])). % 262.02/262.58 cnf(9037,plain, % 262.02/262.58 (P3(f2(a12,f8(a12)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,3675,26,27,30])). % 262.02/262.58 cnf(9039,plain, % 262.02/262.58 (P3(f2(a9,f8(a12)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,3675,26,27,30,29])). % 262.02/262.58 cnf(9041,plain, % 262.02/262.58 (~P3(f2(a11,f8(a12)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,3675,26,27,30,29,31])). % 262.02/262.58 cnf(9043,plain, % 262.02/262.58 (P3(f2(a12,f8(a12)),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[22,3675,26,27,30,29,31,28])). % 262.02/262.58 cnf(9046,plain, % 262.02/262.58 (~E(f2(a10,a12),f2(a11,f8(a12)))), % 262.02/262.58 inference(scs_inference,[],[22,3675,26,27,30,29,31,28,2,16])). % 262.02/262.58 cnf(9047,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,a11,a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,3675,3630,18,20,26,27,30,29,31,28,2,16,34])). % 262.02/262.58 cnf(9049,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,a11,a11,a1)),a1)), % 262.02/262.58 inference(scs_inference,[],[22,3675,3630,18,20,26,27,30,29,31,28,2,16,34,33])). % 262.02/262.58 cnf(9051,plain, % 262.02/262.58 (P3(f2(a10,f8(a12)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,3675,3630,18,19,20,26,27,30,29,31,28,2,16,34,33,32])). % 262.02/262.58 cnf(9059,plain, % 262.02/262.58 (P3(f2(a11,f8(a11)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[3632,30])). % 262.02/262.58 cnf(9061,plain, % 262.02/262.58 (P3(f2(a9,f8(a11)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[3632,30,29])). % 262.02/262.58 cnf(9066,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),f8(a12)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9041,9047,9046,24,3632,19,30,29,27,2,32])). % 262.02/262.58 cnf(9074,plain, % 262.02/262.58 (P3(f2(a9,f8(a9)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[21,30])). % 262.02/262.58 cnf(9092,plain, % 262.02/262.58 (~P3(f2(f8(a11),f8(a12)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9059,9041,19,32])). % 262.02/262.58 cnf(9096,plain, % 262.02/262.58 (~E(f2(a10,a9),f2(f8(a11),f8(a12)))), % 262.02/262.58 inference(scs_inference,[],[9059,9041,19,32,37,48])). % 262.02/262.58 cnf(9102,plain, % 262.02/262.58 (~P3(f2(f8(a11),a9),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9039,9092,9096,19,2,32])). % 262.02/262.58 cnf(9106,plain, % 262.02/262.58 (~E(f2(a10,a9),f2(f8(a11),a9))), % 262.02/262.58 inference(scs_inference,[],[9039,9092,9096,19,2,32,37,48])). % 262.02/262.58 cnf(9121,plain, % 262.02/262.58 (~P3(f2(f8(a9),x91211),f7(a1))+P3(f2(a9,x91211),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9074,19,32])). % 262.02/262.58 cnf(9133,plain, % 262.02/262.58 (~P3(f2(f8(a11),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9102,21,19,32])). % 262.02/262.58 cnf(9146,plain, % 262.02/262.58 (~P3(f2(f8(a11),x91461),f7(a1))+P3(f2(a9,x91461),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9061,19,32])). % 262.02/262.58 cnf(9149,plain, % 262.02/262.58 (~P3(f2(f8(a11),x91491),f7(a1))+P3(f2(a9,x91491),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[9061,19,32,28])). % 262.02/262.58 cnf(9153,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9051,9066,19,32])). % 262.02/262.58 cnf(9167,plain, % 262.02/262.58 (P3(f2(a9,f6(a9,a11,a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9153,9047,3630,19,17,32])). % 262.02/262.58 cnf(9172,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),a9),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9039,9066,19,32])). % 262.02/262.58 cnf(9176,plain, % 262.02/262.58 (~E(f2(a10,a9),f2(f6(a9,a11,a11,a1),a9))), % 262.02/262.58 inference(scs_inference,[],[9039,9066,19,32,37,48])). % 262.02/262.58 cnf(9187,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),x91871),f7(a1))+P3(f2(a9,x91871),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9167,9176,19,2,32])). % 262.02/262.58 cnf(9190,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),x91901),f7(a1))+P3(f2(a9,x91901),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[9167,9176,19,2,32,28])). % 262.02/262.58 cnf(9194,plain, % 262.02/262.58 (P3(f2(a10,f8(a11)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9059,3632,19,32])). % 262.02/262.58 cnf(9197,plain, % 262.02/262.58 (~P3(f2(x91971,a10),f7(a1))+~P3(f2(f6(a9,a11,a11,a1),x91971),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9153,19,32])). % 262.02/262.58 cnf(9205,plain, % 262.02/262.58 (~P3(f2(f8(a11),x92051),f7(a1))+P3(f2(a10,x92051),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9194,19,32])). % 262.02/262.58 cnf(9208,plain, % 262.02/262.58 (~P3(f2(f8(a11),x92081),f7(a1))+P3(f2(a9,f8(x92081)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9194,19,32,29])). % 262.02/262.58 cnf(9215,plain, % 262.02/262.58 (P3(f2(a10,f6(a9,a11,a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9047,3632,19,32])). % 262.02/262.58 cnf(9219,plain, % 262.02/262.58 (~P3(f2(x92191,a10),f7(a1))+~P3(f2(f8(a11),x92191),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9133,19,32])). % 262.02/262.58 cnf(9223,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),x92231),f7(a1))+P3(f2(a10,x92231),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9215,19,32])). % 262.02/262.58 cnf(9226,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),x92261),f7(a1))+P3(f2(a9,f8(x92261)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9215,19,32,29])). % 262.02/262.58 cnf(9228,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),x92281),f7(a1))+P3(f2(x92281,f8(x92281)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9215,19,32,29,30])). % 262.02/262.58 cnf(9230,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),x92301),f7(a1))+P3(f2(a10,x92301),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[9215,19,32,29,30,28])). % 262.02/262.58 cnf(9233,plain, % 262.02/262.58 (~P3(f2(f8(a12),x92331),f7(a1))+P3(f2(a9,x92331),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9039,19,32])). % 262.02/262.58 cnf(9265,plain, % 262.02/262.58 (~P3(f2(f8(a12),x92651),f7(a1))+P3(f2(a10,x92651),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9051,32])). % 262.02/262.58 cnf(9268,plain, % 262.02/262.58 (~P3(f2(f8(a12),x92681),f7(a1))+P3(f2(a10,x92681),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[19,9051,32,28])). % 262.02/262.58 cnf(9270,plain, % 262.02/262.58 (~P3(f2(f8(a12),x92701),f7(a1))+P3(f2(a9,f8(x92701)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9051,32,28,29])). % 262.02/262.58 cnf(9332,plain, % 262.02/262.58 (P3(f2(a10,f8(a9)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9074,21,19,32])). % 262.02/262.58 cnf(9356,plain, % 262.02/262.58 (~P3(f2(f8(a9),x93561),f7(a1))+P3(f2(a10,x93561),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9332,19,32])). % 262.02/262.58 cnf(9370,plain, % 262.02/262.58 (~P3(f2(a11,x93701),f7(f7(a1)))+P3(f2(a10,x93701),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[3643,19,32])). % 262.02/262.58 cnf(9383,plain, % 262.02/262.58 (~P3(f2(a11,x93831),f7(f7(a1)))+P3(f2(a9,x93831),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[3641,19,32])). % 262.02/262.58 cnf(9413,plain, % 262.02/262.58 (~P3(f2(a12,x94131),f7(f7(a1)))+P3(f2(a10,x94131),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[3615,19,32])). % 262.02/262.58 cnf(9428,plain, % 262.02/262.58 (~P3(f2(f8(a12),x94281),f7(a1))+P3(f2(a12,x94281),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9037,19,32])). % 262.02/262.58 cnf(9482,plain, % 262.02/262.58 (~E(x94821,f2(f8(a11),a9))+~E(f2(a10,a9),x94821)), % 262.02/262.58 inference(scs_inference,[],[9106,3])). % 262.02/262.58 cnf(9492,plain, % 262.02/262.58 (~E(a9,x94921)+~E(f2(a10,x94921),f2(f8(a11),a9))), % 262.02/262.58 inference(scs_inference,[],[9482,6])). % 262.02/262.58 cnf(9496,plain, % 262.02/262.58 (~E(f2(f8(a11),a9),f2(a10,x94961))+~E(a9,x94961)), % 262.02/262.58 inference(scs_inference,[],[9492,2])). % 262.02/262.58 cnf(9505,plain, % 262.02/262.58 (~E(f8(a11),a10)), % 262.02/262.58 inference(scs_inference,[],[9496,5])). % 262.02/262.58 cnf(9511,plain, % 262.02/262.58 (~P3(f2(f6(a9,a11,a11,a1),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9037,9505,9066,19,2,26,27,32])). % 262.02/262.58 cnf(9674,plain, % 262.02/262.58 (P3(f2(a9,f8(f8(a9))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9332,9121,30])). % 262.02/262.58 cnf(9677,plain, % 262.02/262.58 (P3(f2(a9,f8(f8(a11))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9194,9146,30])). % 262.02/262.58 cnf(9678,plain, % 262.02/262.58 (P3(f2(a10,f8(f8(a11))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9194,9205,30])). % 262.02/262.58 cnf(9679,plain, % 262.02/262.58 (~P3(f2(f8(f8(a11)),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9194,9219,30])). % 262.02/262.58 cnf(9680,plain, % 262.02/262.58 (P3(f2(a9,f8(f8(a12))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9051,9233,30])). % 262.02/262.58 cnf(9683,plain, % 262.02/262.58 (P3(f2(a10,f8(f8(a12))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9051,9265,30])). % 262.02/262.58 cnf(9684,plain, % 262.02/262.58 (P3(f2(a10,f8(f8(a9))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9332,9356,30])). % 262.02/262.58 cnf(9685,plain, % 262.02/262.58 (P3(f2(a12,f8(f8(a12))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9051,9428,30])). % 262.02/262.58 cnf(9698,plain, % 262.02/262.58 (~P1(f7(a1))+~P3(f2(f8(a11),x96981),f7(a1))+P3(f2(f8(a9),f6(a9,x96981,f8(a9),f7(a1))),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[9074,9149,34])). % 262.02/262.58 cnf(9702,plain, % 262.02/262.58 (P3(f2(a9,f8(f8(f8(a11)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9194,9208,30])). % 262.02/262.58 cnf(9791,plain, % 262.02/262.58 (P3(f2(a9,f8(f8(f8(a12)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9051,9270,30])). % 262.02/262.58 cnf(9799,plain, % 262.02/262.58 (~P3(f2(a12,x97991),f7(f7(a1)))+P3(f2(a10,x97991),f7(f7(f7(a1))))), % 262.02/262.58 inference(scs_inference,[],[9413,28])). % 262.02/262.58 cnf(10156,plain, % 262.02/262.58 (~P3(f2(f8(f6(a9,a11,a11,a1)),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9215,9197,30])). % 262.02/262.58 cnf(10158,plain, % 262.02/262.58 (P3(f2(a10,f8(f6(a9,a11,a11,a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9215,9223,30])). % 262.02/262.58 cnf(10320,plain, % 262.02/262.58 (~E(f2(a10,a12),f2(f8(f8(a11)),a10))), % 262.02/262.58 inference(scs_inference,[],[3649,9043,9679,9684,9413,27,28,2,29,37])). % 262.02/262.58 cnf(10321,plain, % 262.02/262.58 (P3(f2(f8(f6(a9,a11,a11,a1)),f8(f8(f6(a9,a11,a11,a1)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[3649,9043,9679,10158,9684,9413,27,28,2,29,37,30])). % 262.02/262.58 cnf(10323,plain, % 262.02/262.58 (~E(f2(a10,a9),f2(f8(f8(a11)),a10))), % 262.02/262.58 inference(scs_inference,[],[3649,9043,9679,10158,9684,9413,27,28,2,29,37,30,48])). % 262.02/262.58 cnf(10324,plain, % 262.02/262.58 (~P3(f2(a11,f8(f8(a12))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[3649,9043,9679,10158,9684,9685,9413,27,28,2,29,37,30,48,31])). % 262.02/262.58 cnf(10328,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f8(f8(a9)),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[3649,9043,9674,9679,10158,9684,9685,18,20,9413,27,28,2,29,37,30,48,31,26,34])). % 262.02/262.58 cnf(10330,plain, % 262.02/262.58 (P3(f2(f8(a11),f6(a11,f8(a11),f6(a9,a11,a11,a1),a1)),a1)), % 262.02/262.58 inference(scs_inference,[],[3649,9043,9674,9679,10158,9684,9685,9059,18,9049,20,9413,27,28,2,29,37,30,48,31,26,34,33])). % 262.02/262.58 cnf(10334,plain, % 262.02/262.58 (~E(f2(a9,f8(f8(a9))),f2(f8(f8(a11)),a10))), % 262.02/262.58 inference(scs_inference,[],[3649,9043,9674,9679,10158,9684,9685,9059,18,9049,20,9413,27,28,2,29,37,30,48,31,26,34,33,9799,16])). % 262.02/262.58 cnf(10336,plain, % 262.02/262.58 (~P3(f2(f8(f8(f6(a9,a11,a11,a1))),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[3649,9043,9674,9679,10156,10158,9684,9685,9059,18,9049,19,20,9413,27,28,2,29,37,30,48,31,26,34,33,9799,16,17,32])). % 262.02/262.58 cnf(10347,plain, % 262.02/262.58 (~E(f2(f8(f8(a11)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[9677,10320,27,28,2])). % 262.02/262.58 cnf(10348,plain, % 262.02/262.58 (P3(f2(a9,f8(f6(a9,a11,a11,a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9677,10320,9215,27,28,2,29])). % 262.02/262.58 cnf(10350,plain, % 262.02/262.58 (~E(f2(a10,a12),f2(a11,f8(f8(a12))))), % 262.02/262.58 inference(scs_inference,[],[9677,10324,10320,9215,27,28,2,29,37])). % 262.02/262.58 cnf(10351,plain, % 262.02/262.58 (P3(f2(f8(f8(a11)),f8(f8(f8(a11)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9677,9678,10324,10320,9215,27,28,2,29,37,30])). % 262.02/262.58 cnf(10353,plain, % 262.02/262.58 (~E(f2(a10,a9),f2(a11,f8(f8(a12))))), % 262.02/262.58 inference(scs_inference,[],[9677,9678,10324,10320,9215,27,28,2,29,37,30,48])). % 262.02/262.58 cnf(10364,plain, % 262.02/262.58 (P3(f2(a9,f8(f8(a12))),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[9680,10347,27,28])). % 262.02/262.58 cnf(10366,plain, % 262.02/262.58 (~E(f2(f8(f8(a11)),a10),f2(a10,a9))), % 262.02/262.58 inference(scs_inference,[],[9680,10347,10323,27,28,2])). % 262.02/262.58 cnf(10368,plain, % 262.02/262.58 (P3(f2(f8(f8(a12)),f8(f8(f8(a12)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9680,10347,9683,10323,10336,27,28,2,37,30])). % 262.02/262.58 cnf(10373,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9680,10347,9683,10323,10336,10328,18,9049,27,28,2,37,30,48,26,34])). % 262.02/262.58 cnf(10400,plain, % 262.02/262.58 (~E(f2(a11,f8(f8(a12))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10348,10366,10350,27,28,2])). % 262.02/262.58 cnf(10401,plain, % 262.02/262.58 (~E(f2(a10,a12),f2(f8(f6(a9,a11,a11,a1)),a10))), % 262.02/262.58 inference(scs_inference,[],[10348,10366,10350,10156,27,28,2,37])). % 262.02/262.58 cnf(10402,plain, % 262.02/262.58 (P3(f2(f8(f8(a9)),f8(f8(f8(a9)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10348,10366,10350,10156,9684,27,28,2,37,30])). % 262.02/262.58 cnf(10404,plain, % 262.02/262.58 (~E(f2(a10,a9),f2(f8(f6(a9,a11,a11,a1)),a10))), % 262.02/262.58 inference(scs_inference,[],[10348,10366,10350,10156,9684,27,28,2,37,30,48])). % 262.02/262.58 cnf(10407,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10348,10366,10350,10156,9684,18,20,27,28,2,37,30,48,26,34])). % 262.02/262.58 cnf(10421,plain, % 262.02/262.58 (~E(f2(f8(f6(a9,a11,a11,a1)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10400,10401,10364,27,28,2])). % 262.02/262.58 cnf(10422,plain, % 262.02/262.58 (P3(f2(f8(a11),f8(f8(a11))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10400,10401,10364,9194,27,28,2,30])). % 262.02/262.58 cnf(10428,plain, % 262.02/262.58 (~P3(f2(f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1),f8(f8(a12))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10400,10401,10364,10407,10324,9194,18,9049,19,27,28,2,30,26,33,32])). % 262.02/262.58 cnf(10432,plain, % 262.02/262.58 (~E(f2(a10,a9),f2(f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1),f8(f8(a12))))), % 262.02/262.58 inference(scs_inference,[],[10400,10401,10364,10407,10324,9194,18,9049,19,27,28,2,30,26,33,32,37,48])). % 262.02/262.58 cnf(10445,plain, % 262.02/262.58 (P3(f2(f8(a11),f8(f8(a11))),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[10422,10421,27,28])). % 262.02/262.58 cnf(10447,plain, % 262.02/262.58 (~E(f2(f8(f6(a9,a11,a11,a1)),a10),f2(a10,a9))), % 262.02/262.58 inference(scs_inference,[],[10422,10421,10404,27,28,2])). % 262.02/262.58 cnf(10448,plain, % 262.02/262.58 (P3(f2(f8(a9),f8(f8(a9))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10422,10421,10404,9332,27,28,2,30])). % 262.02/262.58 cnf(10455,plain, % 262.02/262.58 (~P3(f2(f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10422,10421,10404,10428,10330,9683,9332,18,19,27,28,2,30,26,16,34,32])). % 262.02/262.58 cnf(10470,plain, % 262.02/262.58 (P3(f2(f8(a9),f8(f8(a9))),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[10448,10447,27,28])). % 262.02/262.58 cnf(10472,plain, % 262.02/262.58 (~E(f2(a11,f8(f8(a12))),f2(a10,a9))), % 262.02/262.58 inference(scs_inference,[],[10448,10447,10353,27,28,2])). % 262.02/262.58 cnf(10473,plain, % 262.02/262.58 (P3(f2(f8(a12),f8(f8(a12))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10448,10447,10353,9051,27,28,2,30])). % 262.02/262.58 cnf(10486,plain, % 262.02/262.58 (P3(f2(a9,f8(f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10448,10447,10353,10373,10402,9051,19,27,28,2,30,26,32,9230,9223,9190,9226])). % 262.02/262.58 cnf(10488,plain, % 262.02/262.58 (~P3(f2(f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10448,10447,10353,10373,10402,9051,19,27,28,2,30,26,32,9230,9223,9190,9226,9197])). % 262.02/262.58 cnf(10496,plain, % 262.02/262.58 (P3(f2(a10,f8(f8(f8(a9)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10448,10447,10353,10373,10402,10422,9051,19,27,28,2,30,26,32,9230,9223,9190,9226,9197,37,48,9698,9268,9356])). % 262.02/262.58 cnf(10507,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f8(f6(a9,a11,a11,a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10473,10472,10334,9215,27,28,2,30])). % 262.02/262.58 cnf(10522,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f8(f6(a9,a11,a11,a1))),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[10507,10432,27,28])). % 262.02/262.58 cnf(10536,plain, % 262.02/262.58 (~E(f2(a12,f6(a9,a11,a11,a1)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[9047,9153,31,28,3635,3647,2214])). % 262.02/262.58 cnf(10537,plain, % 262.02/262.58 (~P3(f2(f8(a12),f6(a9,a11,a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9047,9153,31,28,3635,3647,2214,9428])). % 262.02/262.58 cnf(10540,plain, % 262.02/262.58 (~P3(f2(a12,a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9049,9047,9215,9153,31,28,3635,3647,2214,9428,16,32])). % 262.02/262.58 cnf(10545,plain, % 262.02/262.58 (~P3(f2(a12,f8(a11)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9059,31])). % 262.02/262.58 cnf(10547,plain, % 262.02/262.58 (~P3(f2(f8(a11),a10),a1)), % 262.02/262.58 inference(scs_inference,[],[9059,9133,31,28])). % 262.02/262.58 cnf(10553,plain, % 262.02/262.58 (~E(f2(f8(f8(f6(a9,a11,a11,a1))),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[9059,9133,10507,10336,31,28,3647,3635,9230,2214])). % 262.02/262.58 cnf(10554,plain, % 262.02/262.58 (~P3(f2(f8(a12),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9059,9133,10507,10336,10540,31,28,3647,3635,9230,2214,9428])). % 262.02/262.58 cnf(10557,plain, % 262.02/262.58 (P3(f2(a11,f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9047,9059,9153,9133,10373,10507,10336,10540,31,28,3647,3635,9230,2214,9428,16,32])). % 262.02/262.58 cnf(10567,plain, % 262.02/262.58 (~P3(f2(a12,f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10407,31])). % 262.02/262.58 cnf(10573,plain, % 262.02/262.58 (~E(f2(f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1),f8(f8(a12))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[9172,9092,9679,10407,10428,31,28,3635,3647,2214])). % 262.02/262.58 cnf(10574,plain, % 262.02/262.58 (~P3(f2(f8(a12),f8(a11)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9172,9092,9679,10407,10428,10545,31,28,3635,3647,2214,9428])). % 262.02/262.58 cnf(10577,plain, % 262.02/262.58 (P3(f2(a11,f8(f8(a11))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9049,9059,10422,9172,9092,9679,10407,10428,10545,10547,31,28,3635,3647,2214,9428,16,32])). % 262.02/262.58 cnf(10587,plain, % 262.02/262.58 (~E(f2(a12,a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10540,2214])). % 262.02/262.58 cnf(10588,plain, % 262.02/262.58 (~P3(f2(a12,f6(a9,f8(f8(a9)),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10328,10540,2214,31])). % 262.02/262.58 cnf(10594,plain, % 262.02/262.58 (~P3(f2(f8(a12),f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9092,9679,9066,10328,10540,10567,2214,31,3647,3635,28,9428])). % 262.02/262.58 cnf(10607,plain, % 262.02/262.58 (~E(f2(a12,f8(a11)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10545,2214])). % 262.02/262.58 cnf(10612,plain, % 262.02/262.58 (~P3(f2(a12,f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9679,9066,10324,10545,10557,2214,3647,3635,28,31])). % 262.02/262.58 cnf(10614,plain, % 262.02/262.58 (~P3(f2(f8(a12),f6(a9,f8(f8(a9)),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9679,9066,10324,10545,10588,10557,2214,3647,3635,28,31,9428])). % 262.02/262.58 cnf(10654,plain, % 262.02/262.58 (~E(f2(a12,f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10567,2214])). % 262.02/262.58 cnf(10657,plain, % 262.02/262.58 (~P3(f2(a12,f8(f8(a11))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10324,10156,10567,10577,2214,3647,3635,31])). % 262.02/262.58 cnf(10661,plain, % 262.02/262.58 (~P3(f2(f8(a12),f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[9066,10324,10156,10567,10612,10577,2214,3647,3635,31,28,9428])). % 262.02/262.58 cnf(10664,plain, % 262.02/262.58 (P3(f2(a11,f8(f6(a9,a11,a11,a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9047,9153,9332,9066,10324,10156,10507,10567,10612,10577,2214,3647,3635,31,28,9428,16,32])). % 262.02/262.58 cnf(10692,plain, % 262.02/262.58 (~E(f2(a12,f6(a9,f8(f8(a9)),a11,a1)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10588,2214])). % 262.02/262.58 cnf(10697,plain, % 262.02/262.58 (~P3(f2(a12,f8(f6(a9,a11,a11,a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10324,10156,10336,10588,10664,2214,3635,3647,28,31])). % 262.02/262.58 cnf(10699,plain, % 262.02/262.58 (~P3(f2(f8(a12),f8(f8(a11))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10324,10156,10336,10588,10657,10664,2214,3635,3647,28,31,9428])). % 262.02/262.58 cnf(10702,plain, % 262.02/262.58 (~P3(f2(a11,a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9153,10373,10324,10156,10336,9683,10588,10657,10664,2214,3635,3647,28,31,9428,16,32])). % 262.02/262.58 cnf(10712,plain, % 262.02/262.58 (~E(f2(a12,f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10612,2214])). % 262.02/262.58 cnf(10717,plain, % 262.02/262.58 (~P3(f2(f8(a12),f8(f6(a9,a11,a11,a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10156,10336,10428,10612,10697,2214,3647,3635,28,9428])). % 262.02/262.58 cnf(10750,plain, % 262.02/262.58 (~E(f2(a12,f8(f8(a11))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10657,2214])). % 262.02/262.58 cnf(10751,plain, % 262.02/262.58 (~E(f2(a9,a11),f2(a12,a10))), % 262.02/262.58 inference(scs_inference,[],[10540,10657,2214,3635])). % 262.02/262.58 cnf(10756,plain, % 262.02/262.58 (P3(f2(f8(a11),f8(f8(f8(a11)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9153,10422,10336,10428,10540,10657,10351,2214,3635,3647,28,16,32])). % 262.02/262.58 cnf(10773,plain, % 262.02/262.58 (~E(f2(a12,f8(f6(a9,a11,a11,a1))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10697,2214])). % 262.02/262.58 cnf(10779,plain, % 262.02/262.58 (P3(f2(f8(a12),f8(f8(f8(a12)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9153,9194,10473,10428,10540,10545,10697,10368,2214,3647,3635,28,16,32])). % 262.02/262.58 cnf(10815,plain, % 262.02/262.58 (~E(f2(f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10488,2214])). % 262.02/262.58 cnf(10821,plain, % 262.02/262.58 (P3(f2(a10,f8(f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9153,21,10473,9041,10545,10567,10488,10486,2214,3635,3647,28,16,32])). % 262.02/262.58 cnf(10835,plain, % 262.02/262.58 (P3(f2(a12,f8(f8(f8(a12)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9037,9153,10507,9102,10567,10588,10779,10554,2214,3647,3635,28,16,32])). % 262.02/262.58 cnf(10850,plain, % 262.02/262.58 (P3(f2(a10,f8(f8(f8(a11)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9153,21,9061,10540,10588,10488,10537,9702,2214,3635,3647,28,16,32])). % 262.02/262.58 cnf(10858,plain, % 262.02/262.58 (~E(f2(f8(a12),f8(a11)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10574,2214])). % 262.02/262.58 cnf(10864,plain, % 262.02/262.58 (P3(f2(a10,f8(f8(f8(a12)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9153,21,9039,10545,10488,10612,10574,9791,2214,3635,3647,28,16,32])). % 262.02/262.58 cnf(10869,plain, % 262.02/262.58 (~E(f2(f8(a12),f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10594,2214])). % 262.02/262.58 cnf(10875,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f8(f8(f6(a9,a11,a11,a1)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9153,10507,9074,10488,10612,10657,10594,10321,2214,3647,3635,28,16,32])). % 262.02/262.58 cnf(10891,plain, % 262.02/262.58 (~E(f2(f8(a12),f6(a9,f8(f8(a9)),a11,a1)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10614,2214])). % 262.02/262.58 cnf(10902,plain, % 262.02/262.58 (~E(f2(f8(a12),f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10661,2214])). % 262.02/262.58 cnf(10913,plain, % 262.02/262.58 (~E(f2(f8(a12),f8(f8(a11))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10699,2214])). % 262.02/262.58 cnf(10931,plain, % 262.02/262.58 (~E(f2(f8(a12),f8(f6(a9,a11,a11,a1))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10717,2214])). % 262.02/262.58 cnf(10940,plain, % 262.02/262.58 (~P3(f2(a12,f8(f8(f6(a9,a11,a11,a1)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9047,9153,10657,10348,10537,10574,10717,10875,2214,3647,3635,28,16,32,31])). % 262.02/262.58 cnf(10942,plain, % 262.02/262.58 (~P3(f2(f8(a12),f8(f8(f6(a9,a11,a11,a1)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9047,9153,10657,10348,10537,10574,10717,10875,2214,3647,3635,28,16,32,31,9428])). % 262.02/262.58 cnf(10951,plain, % 262.02/262.58 (~E(f2(a11,a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10702,2214])). % 262.02/262.58 cnf(10960,plain, % 262.02/262.58 (~P3(f2(a12,f8(f8(f8(a11)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9059,9153,10697,9683,10574,10594,10702,10756,2214,3647,3635,28,16,32,31])). % 262.02/262.58 cnf(10962,plain, % 262.02/262.58 (~P3(f2(f8(a12),f8(f8(f8(a11)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,9059,9153,10697,9683,10574,10594,10702,10756,2214,3647,3635,28,16,32,31,9428])). % 262.02/262.58 cnf(10969,plain, % 262.02/262.58 (~E(f2(f8(a12),f8(f8(f6(a9,a11,a11,a1)))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10942,2214])). % 262.02/262.58 cnf(10999,plain, % 262.02/262.58 (~E(f2(f8(a12),f8(f8(f8(a11)))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10614,10962,3647,2214])). % 262.02/262.58 cnf(11009,plain, % 262.02/262.58 (~E(f2(a12,f8(f8(f6(a9,a11,a11,a1)))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10940,2214])). % 262.02/262.58 cnf(11030,plain, % 262.02/262.58 (~E(f2(a12,f8(f8(f8(a11)))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10699,10960,3647,2214])). % 262.02/262.58 cnf(11039,plain, % 262.02/262.58 (~E(f2(f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10455,2214])). % 262.02/262.58 cnf(11041,plain, % 262.02/262.58 (~E(f2(a9,a11),f2(a11,a10))), % 262.02/262.58 inference(scs_inference,[],[10717,10702,10455,2214,3647,3635])). % 262.02/262.58 cnf(11137,plain, % 262.02/262.58 (~P3(f2(f6(a9,f8(f6(a9,a11,a11,a1)),a11,a1),a10),a1)), % 262.02/262.58 inference(scs_inference,[],[10455,28])). % 262.02/262.58 cnf(12152,plain, % 262.02/262.58 (~P3(f2(x121521,f8(a11)),f7(f7(a1)))+P3(f2(x121521,f8(f8(a11))),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[19,10445,32])). % 262.02/262.58 cnf(12160,plain, % 262.02/262.58 (~P3(f2(x121601,f8(a9)),f7(f7(a1)))+P3(f2(x121601,f8(f8(a9))),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[19,10470,32])). % 262.02/262.58 cnf(12168,plain, % 262.02/262.58 (~P3(f2(x121681,f6(a9,a11,a11,a1)),f7(f7(a1)))+P3(f2(x121681,f8(f6(a9,a11,a11,a1))),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[19,10522,32])). % 262.02/262.58 cnf(12234,plain, % 262.02/262.58 (~P3(f2(x122341,a10),f7(a1))+P3(f2(x122341,f8(f8(f8(a12)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,10864,32])). % 262.02/262.58 cnf(12240,plain, % 262.02/262.58 (~P3(f2(x122401,a10),a1)+P3(f2(x122401,f8(f8(f8(a12)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,10864,32,3647,3635,2214,28])). % 262.02/262.58 cnf(12524,plain, % 262.02/262.58 (P3(f2(a11,f8(a11)),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[10536,10587,10537,9059,26,27,2,37,48,28])). % 262.02/262.58 cnf(12526,plain, % 262.02/262.58 (~P3(f2(f8(a12),a11),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,10536,10587,10537,9059,9047,26,27,2,37,48,28,32])). % 262.02/262.58 cnf(12544,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,a11,a11,a1)),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[10607,10751,12526,9047,26,37,27,2,48,28])). % 262.02/262.58 cnf(12546,plain, % 262.02/262.58 (~P3(f2(f8(a12),a9),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[19,10607,10751,12526,3630,9047,26,37,27,2,48,28,32])). % 262.02/262.58 cnf(12576,plain, % 262.02/262.58 (P3(f2(a9,f8(a9)),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[10858,10951,10574,10702,9074,26,27,48,2,37,28])). % 262.02/262.58 cnf(12586,plain, % 262.02/262.58 (P3(f2(a10,f8(a9)),f7(f7(a1)))), % 262.02/262.58 inference(scs_inference,[],[11041,10554,10540,9332,26,27,2,48,37,28])). % 262.02/262.58 cnf(13034,plain, % 262.02/262.58 (~P3(f2(f8(a12),a11),a1)), % 262.02/262.58 inference(scs_inference,[],[12526,28])). % 262.02/262.58 cnf(13411,plain, % 262.02/262.58 (P3(f2(a9,f8(f8(f8(f8(a12))))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10779,9270])). % 262.02/262.58 cnf(13413,plain, % 262.02/262.58 (~P3(f2(f8(f8(f8(a11))),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10779,10756,9270,9219])). % 262.02/262.58 cnf(13417,plain, % 262.02/262.58 (P3(f2(a9,f8(f8(f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10779,10821,10756,9270,9219,9208,29])). % 262.02/262.58 cnf(13421,plain, % 262.02/262.58 (~P3(f2(f8(f8(f8(a11))),a10),a1)), % 262.02/262.58 inference(scs_inference,[],[10779,10496,10821,10756,9270,9219,9208,29,30,28])). % 262.02/262.58 cnf(13428,plain, % 262.02/262.58 (P3(f2(f8(a12),f6(a9,f8(a12),a11,a1)),a1)), % 262.02/262.58 inference(scs_inference,[],[20,9153,18,9039,10779,2231,10496,10821,10756,9270,9219,9208,29,30,28,27,26,16,33])). % 262.02/262.58 cnf(13564,plain, % 262.02/262.58 (P3(f2(f8(f8(f8(a11))),f8(f8(f8(f8(a11))))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10850,30])). % 262.02/262.58 cnf(13753,plain, % 262.02/262.58 (~P3(f2(a11,f8(f8(f8(a12)))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13413,10835,12576,12544,12524,12152,12160,12168,37,31])). % 262.02/262.58 cnf(13756,plain, % 262.02/262.58 (P3(f2(f8(a12),f6(a9,f8(a12),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13413,13428,10835,12576,12544,12524,12152,12160,12168,37,31,48,28])). % 262.02/262.58 cnf(13758,plain, % 262.02/262.58 (~E(f2(f8(f8(f8(a11))),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[13413,13428,10835,12576,12544,12524,12152,12160,12168,37,31,48,28,2214])). % 262.02/262.58 cnf(13766,plain, % 262.02/262.58 (P3(f2(f6(a9,f8(a12),a11,a1),f6(f8(a12),f8(f8(f8(a12))),f6(a9,f8(a12),a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10553,10654,13413,13428,13411,10835,12576,12544,12524,10779,18,20,12152,12160,12168,37,31,48,28,2214,27,26,2,33,34])). % 262.02/262.58 cnf(13768,plain, % 262.02/262.58 (~P3(f2(f8(f8(f8(f8(a11)))),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10553,10654,13413,13428,13411,10835,12576,12544,12524,10779,13564,18,19,20,12152,12160,12168,37,31,48,28,2214,27,26,2,33,34,32])). % 262.02/262.58 cnf(13771,plain, % 262.02/262.58 (P3(f2(a9,f6(a9,f8(a12),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10553,10654,13413,13428,13411,10835,12576,12544,12524,10779,13564,18,19,20,12152,12160,12168,37,31,48,28,2214,27,26,2,33,34,32,9233])). % 262.02/262.58 cnf(13775,plain, % 262.02/262.58 (P3(f2(a9,f8(f6(a9,f8(a12),a11,a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10553,10654,13413,13428,13411,10835,12576,12544,12524,10779,13564,18,19,20,12152,12160,12168,37,31,48,28,2214,27,26,2,33,34,32,9233,9265,9270])). % 262.02/262.58 cnf(13777,plain, % 262.02/262.58 (P3(f2(a12,f6(a9,f8(a12),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10553,10654,13413,13428,13411,10835,12576,12544,12524,10779,13564,18,19,20,12152,12160,12168,37,31,48,28,2214,27,26,2,33,34,32,9233,9265,9270,9428])). % 262.02/262.58 cnf(13779,plain, % 262.02/262.58 (P3(f2(f6(a9,f8(a12),a11,a1),f8(f6(a9,f8(a12),a11,a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10553,10654,13413,13428,13411,10835,12576,12544,12524,10779,13564,18,19,20,12152,12160,12168,37,31,48,28,2214,27,26,2,33,34,32,9233,9265,9270,9428,30])). % 262.02/262.58 cnf(13790,plain, % 262.02/262.58 (~P3(f2(a11,f6(a9,f8(a12),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13777,13753,12586,12160,37,31])). % 262.02/262.58 cnf(13795,plain, % 262.02/262.58 (~E(f2(a11,f8(f8(f8(a12)))),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[13775,13777,13753,12586,12160,37,31,48,28,2214])). % 262.02/262.58 cnf(13803,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10573,10692,13775,13756,13777,13753,12586,13428,18,20,12160,37,31,48,28,2214,27,26,2,33,34])). % 262.02/262.58 cnf(13805,plain, % 262.02/262.58 (~P3(f2(f6(a9,f8(a12),a11,a1),a9),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10573,10692,13775,13756,13777,13753,12586,13428,12546,18,19,20,12160,37,31,48,28,2214,27,26,2,33,34,32])). % 262.02/262.58 cnf(13817,plain, % 262.02/262.58 (~E(f2(a11,f6(a9,f8(a12),a11,a1)),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[13779,13790,37,48,28,2214])). % 262.02/262.58 cnf(13825,plain, % 262.02/262.58 (P3(f2(f6(a9,f8(a12),a11,a1),f6(f8(a12),f6(a9,f8(a12),a11,a1),f6(a9,f8(a12),a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10712,13779,13771,13790,13756,13428,18,20,37,48,28,2214,26,27,2,33,34])). % 262.02/262.58 cnf(13827,plain, % 262.02/262.58 (~P3(f2(f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,f8(a12),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10712,13779,13771,13803,13790,13756,13428,18,19,20,37,48,28,2214,26,27,2,33,34,32])). % 262.02/262.58 cnf(13849,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,10750,13825,13827,13805,13771,10330,10756,18,20,37,48,28,2214,26,27,2,16,33,34])). % 262.02/262.58 cnf(13851,plain, % 262.02/262.58 (~P3(f2(f6(f8(a12),f6(a9,f8(a12),a11,a1),f6(a9,f8(a12),a11,a1),a1),a9),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,10750,13825,13827,13805,13771,10330,10756,18,19,20,37,48,28,2214,26,27,2,16,33,34,32])). % 262.02/262.58 cnf(13869,plain, % 262.02/262.58 (P3(f2(f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1)),a1)), % 262.02/262.58 inference(scs_inference,[],[10773,13766,13849,13851,18,9049,37,48,28,2214,26,27,2,33])). % 262.02/262.58 cnf(13871,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10773,13766,13849,13851,18,9049,37,48,28,2214,26,27,2,33,34])). % 262.02/262.58 cnf(13873,plain, % 262.02/262.58 (~P3(f2(f6(f8(a12),f6(a9,f8(a12),a11,a1),f6(a9,f8(a12),a11,a1),a1),a10),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10773,13766,13849,13851,21,18,9049,19,37,48,28,2214,26,27,2,33,34,32])). % 262.02/262.58 cnf(13876,plain, % 262.02/262.58 (P3(f2(f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10773,13766,13849,13851,21,18,9049,19,37,48,28,2214,26,27,2,33,34,32,9228])). % 262.02/262.58 cnf(13878,plain, % 262.02/262.58 (P3(f2(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10773,13766,13849,13851,21,18,9049,19,37,48,28,2214,26,27,2,33,34,32,9228,9187])). % 262.02/262.58 cnf(13896,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10815,10869,13876,13878,13873,13803,18,9049,20,37,48,28,2214,27,26,2,33,34])). % 262.02/262.58 cnf(13898,plain, % 262.02/262.58 (~P3(f2(f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10815,10869,13876,13871,13878,13873,13803,9511,18,9049,19,20,37,48,28,2214,27,26,2,33,34,32])). % 262.02/262.58 cnf(13901,plain, % 262.02/262.58 (~E(f2(f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10815,10869,13876,13871,13878,13873,13803,9511,18,9049,19,20,37,48,28,2214,27,26,2,33,34,32,2329])). % 262.02/262.58 cnf(13920,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10891,13896,13898,18,9049,37,48,28,2214,26,27,2,33,34])). % 262.02/262.58 cnf(13922,plain, % 262.02/262.58 (~P3(f2(f8(f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10891,13896,13898,13876,18,9049,19,37,48,28,2214,26,27,2,33,34,32])). % 262.02/262.58 cnf(13927,plain, % 262.02/262.58 (P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10891,13896,13898,13876,18,9049,19,37,48,28,2214,26,27,2,33,34,32,9383,9228])). % 262.02/262.58 cnf(13929,plain, % 262.02/262.58 (~E(f2(f8(f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10891,13896,13898,13876,18,9049,19,37,48,28,2214,26,27,2,33,34,32,9383,9228,2329])). % 262.02/262.58 cnf(13931,plain, % 262.02/262.58 (P3(f2(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10891,13896,13898,13876,18,9049,19,37,48,28,2214,26,27,2,33,34,32,9383,9228,2329,9187])). % 262.02/262.58 cnf(13952,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10902,13927,13931,13922,18,20,37,48,28,2214,26,27,2,33,34])). % 262.02/262.58 cnf(13954,plain, % 262.02/262.58 (~P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10902,13927,13920,13931,13922,9511,18,19,20,37,48,28,2214,26,27,2,33,34,32])). % 262.02/262.58 cnf(13957,plain, % 262.02/262.58 (~E(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10902,13927,13920,13931,13922,9511,18,19,20,37,48,28,2214,26,27,2,33,34,32,2329])). % 262.02/262.58 cnf(13976,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,10913,13952,13954,13768,18,9049,37,48,28,2214,26,27,2,16,33,34])). % 262.02/262.58 cnf(13978,plain, % 262.02/262.58 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,10913,13952,13954,13768,13927,18,9049,19,37,48,28,2214,26,27,2,16,33,34,32])). % 262.02/262.58 cnf(13983,plain, % 262.02/262.58 (P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,10913,13952,13954,13768,13927,18,9049,19,37,48,28,2214,26,27,2,16,33,34,32,9383,9228])). % 262.02/262.58 cnf(13987,plain, % 262.02/262.58 (~E(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[22,10913,13952,13954,13768,13927,18,9049,19,37,48,28,2214,26,27,2,16,33,34,32,9383,9228,9370,2329])). % 262.02/262.58 cnf(13989,plain, % 262.02/262.58 (P3(f2(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[22,10913,13952,13954,13768,13927,18,9049,19,37,48,28,2214,26,27,2,16,33,34,32,9383,9228,9370,2329,9187])). % 262.02/262.58 cnf(14008,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10931,13983,13989,13978,18,20,37,48,28,2214,26,27,2,33,34])). % 262.02/262.58 cnf(14010,plain, % 262.02/262.58 (~P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10931,13983,13976,13989,13978,9511,18,19,20,37,48,28,2214,26,27,2,33,34,32])). % 262.02/262.58 cnf(14013,plain, % 262.02/262.58 (~E(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10931,13983,13976,13989,13978,9511,18,19,20,37,48,28,2214,26,27,2,33,34,32,2329])). % 262.02/262.58 cnf(14072,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10969,14008,14010,18,9049,37,48,28,26,2214,27,2,33,34])). % 262.02/262.58 cnf(14074,plain, % 262.02/262.58 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10969,14008,14010,13983,18,9049,19,37,48,28,26,2214,27,2,33,34,32])). % 262.02/262.58 cnf(14079,plain, % 262.02/262.58 (P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10969,14008,14010,13983,18,9049,19,37,48,28,26,2214,27,2,33,34,32,9383,9228])). % 262.02/262.58 cnf(14083,plain, % 262.02/262.58 (P3(f2(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10969,14008,14010,13983,18,9049,19,37,48,28,26,2214,27,2,33,34,32,9383,9228,9370,9187])). % 262.02/262.58 cnf(14085,plain, % 262.02/262.58 (~E(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10969,14008,14010,13983,18,9049,19,37,48,28,26,2214,27,2,33,34,32,9383,9228,9370,9187,2329])). % 262.02/262.58 cnf(14103,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10999,14079,14083,14074,18,20,37,48,28,26,27,2214,2,33,34])). % 262.02/262.58 cnf(14105,plain, % 262.02/262.58 (~P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[10999,14079,14072,14083,14074,9511,18,19,20,37,48,28,26,27,2214,2,33,34,32])). % 262.02/262.58 cnf(14108,plain, % 262.02/262.58 (~E(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[10999,14079,14072,14083,14074,9511,18,19,20,37,48,28,26,27,2214,2,33,34,32,2329])). % 262.02/262.58 cnf(14126,plain, % 262.02/262.58 (P3(f2(f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a1)), % 262.02/262.58 inference(scs_inference,[],[11009,14103,14105,18,9049,37,48,28,26,27,2214,2,33])). % 262.02/262.58 cnf(14128,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11009,14103,14105,18,9049,37,48,28,26,27,2214,2,33,34])). % 262.02/262.58 cnf(14130,plain, % 262.02/262.58 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11009,14103,14105,14079,18,9049,19,37,48,28,26,27,2214,2,33,34,32])). % 262.02/262.58 cnf(14135,plain, % 262.02/262.58 (P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11009,14103,14105,14079,18,9049,19,37,48,28,26,27,2214,2,33,34,32,9383,9228])). % 262.02/262.58 cnf(14139,plain, % 262.02/262.58 (P3(f2(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11009,14103,14105,14079,18,9049,19,37,48,28,26,27,2214,2,33,34,32,9383,9228,9370,9187])). % 262.02/262.58 cnf(14141,plain, % 262.02/262.58 (~E(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[11009,14103,14105,14079,18,9049,19,37,48,28,26,27,2214,2,33,34,32,9383,9228,9370,9187,2329])). % 262.02/262.58 cnf(14161,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11030,14135,14139,13869,14130,13421,18,20,37,48,28,27,26,2214,2,16,33,34])). % 262.02/262.58 cnf(14163,plain, % 262.02/262.58 (~P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11030,14135,14128,14139,13869,14130,13421,9511,18,19,20,37,48,28,27,26,2214,2,16,33,34,32])). % 262.02/262.58 cnf(14166,plain, % 262.02/262.58 (~E(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[11030,14135,14128,14139,13869,14130,13421,9511,18,19,20,37,48,28,27,26,2214,2,16,33,34,32,2329])). % 262.02/262.58 cnf(14186,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11039,13901,14161,14163,18,9049,37,48,28,27,26,2214,2,33,34])). % 262.02/262.58 cnf(14188,plain, % 262.02/262.58 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11039,13901,14161,14163,14135,18,9049,19,37,48,28,27,26,2214,2,33,34,32])). % 262.02/262.58 cnf(14193,plain, % 262.02/262.58 (P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11039,13901,14161,14163,14135,18,9049,19,37,48,28,27,26,2214,2,33,34,32,9383,9228])). % 262.02/262.58 cnf(14197,plain, % 262.02/262.58 (P3(f2(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[11039,13901,14161,14163,14135,18,9049,19,37,48,28,27,26,2214,2,33,34,32,9383,9228,9370,9187])). % 262.02/262.58 cnf(14199,plain, % 262.02/262.58 (~E(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[11039,13901,14161,14163,14135,18,9049,19,37,48,28,27,26,2214,2,33,34,32,9383,9228,9370,9187,2329])). % 262.02/262.58 cnf(14218,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13817,13929,14193,14197,14188,18,20,37,48,28,26,27,2214,2,33,34])). % 262.02/262.58 cnf(14220,plain, % 262.02/262.58 (~P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13817,13929,14193,14186,14197,14188,9511,18,19,20,37,48,28,26,27,2214,2,33,34,32])). % 262.02/262.58 cnf(14223,plain, % 262.02/262.58 (~E(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[13817,13929,14193,14186,14197,14188,9511,18,19,20,37,48,28,26,27,2214,2,33,34,32,2329])). % 262.02/262.58 cnf(14243,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13758,13957,14218,14220,18,9049,37,48,28,27,26,2214,2,33,34])). % 262.02/262.58 cnf(14245,plain, % 262.02/262.58 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13758,13957,14218,14220,14193,18,9049,19,37,48,28,27,26,2214,2,33,34,32])). % 262.02/262.58 cnf(14250,plain, % 262.02/262.58 (P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13758,13957,14218,14220,14193,18,9049,19,37,48,28,27,26,2214,2,33,34,32,9383,9228])). % 262.02/262.58 cnf(14254,plain, % 262.02/262.58 (~E(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[13758,13957,14218,14220,14193,18,9049,19,37,48,28,27,26,2214,2,33,34,32,9383,9228,9370,2329])). % 262.02/262.58 cnf(14274,plain, % 262.02/262.58 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13987,14250,14245,13878,13803,18,9049,20,37,48,28,26,27,2214,2,33,34])). % 262.02/262.58 cnf(14276,plain, % 262.02/262.58 (~P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[13987,14250,14243,14245,13878,13803,9511,18,9049,19,20,37,48,28,26,27,2214,2,33,34,32])). % 262.02/262.58 cnf(14279,plain, % 262.02/262.58 (~E(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[13987,14250,14243,14245,13878,13803,9511,18,9049,19,20,37,48,28,26,27,2214,2,33,34,32,2329])). % 262.02/262.58 cnf(14287,plain, % 262.02/262.58 (P3(f2(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[14274,9228])). % 262.02/262.58 cnf(14301,plain, % 262.02/262.58 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[14013,14274,14276,14250,13775,18,19,20,9228,37,48,28,26,27,2214,2,33,32])). % 262.02/262.58 cnf(14304,plain, % 262.02/262.58 (P3(f2(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.58 inference(scs_inference,[],[14013,14274,14276,14250,13775,18,19,20,9228,37,48,28,26,27,2214,2,33,32,9187])). % 262.02/262.58 cnf(14306,plain, % 262.02/262.58 (~E(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a9,f8(a12),a11,a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f2(a10,a12))), % 262.02/262.58 inference(scs_inference,[],[14013,14274,14276,14250,13775,18,19,20,9228,37,48,28,26,27,2214,2,33,32,9187,2329])). % 262.02/262.58 cnf(14324,plain, % 262.02/262.58 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14085,14287,14304,14301,18,20,37,48,28,26,27,2214,2,33,34])). % 262.02/262.59 cnf(14326,plain, % 262.02/262.59 (P3(f2(a9,f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14085,14287,14304,14301,18,19,20,37,48,28,26,27,2214,2,33,34,32])). % 262.02/262.59 cnf(14343,plain, % 262.02/262.59 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14108,14326,14324,13768,18,9049,20,48,28,26,27,2214,2,33,34])). % 262.02/262.59 cnf(14345,plain, % 262.02/262.59 (~P3(f2(f8(f6(a9,f8(a12),a11,a1)),a9),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14108,14326,14324,13779,13768,13805,18,9049,19,20,48,28,26,27,2214,2,33,34,32])). % 262.02/262.59 cnf(14348,plain, % 262.02/262.59 (P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14108,14326,14324,13779,13768,13805,18,9049,19,20,48,28,26,27,2214,2,33,34,32,9228])). % 262.02/262.59 cnf(14364,plain, % 262.02/262.59 (P3(f2(a11,f6(a9,f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14141,14348,14345,14324,14326,18,9049,20,48,28,26,27,2214,2,33,34])). % 262.02/262.59 cnf(14366,plain, % 262.02/262.59 (~P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14141,14348,14343,14345,14324,14326,9511,18,9049,19,20,48,28,26,27,2214,2,33,34,32])). % 262.02/262.59 cnf(14369,plain, % 262.02/262.59 (~E(f2(f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.59 inference(scs_inference,[],[14141,14348,14343,14345,14324,14326,9511,18,9049,19,20,48,28,26,27,2214,2,33,34,32,2329])). % 262.02/262.59 cnf(14385,plain, % 262.02/262.59 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14166,14364,14366,18,9049,48,28,26,27,2214,2,33,34])). % 262.02/262.59 cnf(14387,plain, % 262.02/262.59 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14166,14364,14366,14348,18,9049,19,48,28,26,27,2214,2,33,34,32])). % 262.02/262.59 cnf(14394,plain, % 262.02/262.59 (P3(f2(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14166,14364,14366,14348,14343,18,9049,19,48,28,26,27,2214,2,33,34,32,9383,9370,9187])). % 262.02/262.59 cnf(14396,plain, % 262.02/262.59 (~E(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f2(a10,a12))), % 262.02/262.59 inference(scs_inference,[],[14166,14364,14366,14348,14343,18,9049,19,48,28,26,27,2214,2,33,34,32,9383,9370,9187,2329])). % 262.02/262.59 cnf(14404,plain, % 262.02/262.59 (P3(f2(f6(a11,f6(a9,f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14385,9228])). % 262.02/262.59 cnf(14417,plain, % 262.02/262.59 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14199,14385,14394,14387,18,20,9228,48,28,26,27,2214,2,33,34])). % 262.02/262.59 cnf(14419,plain, % 262.02/262.59 (~P3(f2(f6(a11,f6(a9,f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14199,14385,14394,14387,9511,18,19,20,9228,48,28,26,27,2214,2,33,34,32])). % 262.02/262.59 cnf(14422,plain, % 262.02/262.59 (~E(f2(f6(a11,f6(a9,f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1),f6(a9,a11,a11,a1),a1),a10),f2(a10,a12))), % 262.02/262.59 inference(scs_inference,[],[14199,14385,14394,14387,9511,18,19,20,9228,48,28,26,27,2214,2,33,34,32,2329])). % 262.02/262.59 cnf(14439,plain, % 262.02/262.59 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14223,14404,14417,14419,18,9049,48,28,26,27,2214,2,33,34])). % 262.02/262.59 cnf(14441,plain, % 262.02/262.59 (~P3(f2(f8(f6(a11,f6(a9,f8(f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14223,14404,14417,14419,18,9049,19,48,28,26,27,2214,2,33,34,32])). % 262.02/262.59 cnf(14444,plain, % 262.02/262.59 (P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14223,14404,14417,14419,18,9049,19,48,28,26,27,2214,2,33,34,32,9228])). % 262.02/262.59 cnf(14460,plain, % 262.02/262.59 (P3(f2(a11,f6(a9,f8(f8(f6(a11,f6(a9,f8(f8(a9)),a11,a1),f6(a9,a11,a11,a1),a1))),a11,a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14254,14444,14441,13417,18,20,48,28,26,27,2214,2,34])). % 262.02/262.59 cnf(14462,plain, % 262.02/262.59 (~P3(f2(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a12),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14254,14444,14439,14441,13417,9511,18,19,20,48,28,26,27,2214,2,34,32])). % 262.02/262.59 cnf(14488,plain, % 262.02/262.59 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a12),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14279,14460,14462,14444,19,48,28,26,27,2214,2,32])). % 262.02/262.59 cnf(14495,plain, % 262.02/262.59 (P3(f2(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14279,14460,14462,14444,14439,19,48,28,26,27,2214,2,32,9383,9370,9187])). % 262.02/262.59 cnf(14518,plain, % 262.02/262.59 (P3(f2(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14306,14495,14126,14488,11137,18,20,48,28,26,27,2214,2,16,33,34])). % 262.02/262.59 cnf(14520,plain, % 262.02/262.59 (P3(f2(a9,f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1))),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14306,14495,14126,14488,11137,14444,18,19,20,48,28,26,27,2214,2,16,33,34,32])). % 262.02/262.59 cnf(14536,plain, % 262.02/262.59 (P3(f2(a11,f6(a9,f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[13795,14369,14520,14518,13805,9049,18,20,28,48,26,27,2214,2,33,34])). % 262.02/262.59 cnf(14538,plain, % 262.02/262.59 (~P3(f2(f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a10),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[22,13795,14369,14520,14518,14488,13805,9049,18,19,20,28,48,26,27,2214,2,33,34,32])). % 262.02/262.59 cnf(14553,plain, % 262.02/262.59 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14396,14536,14538,9049,18,28,48,26,27,2,33,34])). % 262.02/262.59 cnf(14555,plain, % 262.02/262.59 (~P3(f2(f6(a9,f8(f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),a11,a1),f8(f8(f8(a12)))),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14396,14536,14538,13753,9049,18,19,28,48,26,27,2,33,34,32])). % 262.02/262.59 cnf(14585,plain, % 262.02/262.59 (P3(f2(f6(a9,a11,a11,a1),f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f6(a11,f6(a9,f8(f6(a9,f8(a12),a11,a1)),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1),a11,a1),f6(a9,a11,a11,a1),a1)),f7(a1))), % 262.02/262.59 inference(scs_inference,[],[14422,14553,14555,14518,9049,18,9228,28,48,26,27,2,34])). % 262.02/262.59 cnf(14658,plain, % 262.02/262.59 ($false), % 262.02/262.59 inference(scs_inference,[],[20,18,13034,9039,13805,14220,13428,14536,14553,13790,14585,14462,14555,2250,2118,12234,12240,38,49,68,56,9197,9223,9226,9190,9230,31,9187,28,26,27,16,34]), % 262.02/262.59 ['proof']). % 262.02/262.59 % SZS output end Proof % 262.02/262.59 % Total time :261.370000s %------------------------------------------------------------------------------