%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : MSC015-1.010 : TPTP v8.2.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n017.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 11:52:13 EDT 2024 % Result : Unsatisfiable 34.26s 34.32s % Output : CNFRefutation 34.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : MSC015-1.010 : TPTP v8.2.0. Released v3.5.0. % 0.03/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sat Jun 22 05:51:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.56/0.58 start to proof:theBenchmark % 34.26/34.31 %------------------------------------------- % 34.26/34.31 % File :CSE---1.7 % 34.26/34.31 % Problem :theBenchmark % 34.26/34.31 % Transform :cnf % 34.26/34.31 % Format :tptp:raw % 34.26/34.31 % Command :java -jar mcs_scs.jar %d %s % 34.26/34.31 % 34.26/34.31 % Result :Theorem 33.690000s % 34.26/34.31 % Output :CNFRefutation 33.690000s % 34.26/34.31 %------------------------------------------- % 34.26/34.31 %------------------------------------------------------------------------------ % 34.26/34.31 % File : MSC015-1.010 : TPTP v8.2.0. Released v3.5.0. % 34.26/34.31 % Domain : Miscellaneous % 34.26/34.31 % Problem : Binary counter k=10 % 34.26/34.31 % Version : Especial. % 34.26/34.31 % English : Each instance of the problem asserts % 34.26/34.31 % p(0*). // p[0] % 34.26/34.31 % p(x*01*) -> p(x*10*). // p[i] -> p[i + 1] % 34.26/34.31 % not p(1*). // not p[2^n - 1] % 34.26/34.31 % These problems are unsatisfiable and have exponentially large % 34.26/34.31 % propositional resolution refutations, while there is a short % 34.26/34.31 % (quadratic) first order refutation. % 34.26/34.31 % 34.26/34.31 % Refs : [NV07a] Navarro (2007), Email to Geoff Sutcliffe % 34.26/34.31 % [NV07b] Navarro & Voronkov (2007), Planning with Effectively P % 34.26/34.31 % Source : [NV07a] % 34.26/34.31 % Names : bincount-k10 [NV07a] % 34.26/34.31 % 34.26/34.31 % Status : Unsatisfiable % 34.26/34.31 % Rating : 0.00 v3.5.0 % 34.26/34.31 % Syntax : Number of clauses : 12 ( 2 unt; 0 nHn; 12 RR) % 34.26/34.31 % Number of literals : 22 ( 0 equ; 11 neg) % 34.26/34.31 % Maximal clause size : 2 ( 1 avg) % 34.26/34.31 % Maximal term depth : 1 ( 1 avg) % 34.26/34.31 % Number of predicates : 1 ( 1 usr; 0 prp; 10-10 aty) % 34.26/34.31 % Number of functors : 2 ( 2 usr; 2 con; 0-0 aty) % 34.26/34.31 % Number of variables : 45 ( 0 sgn) % 34.26/34.31 % SPC : CNF_UNS_EPR_NEQ_HRN % 34.26/34.31 % 34.26/34.31 % Comments : k >= 23 not solved by any prover in less than 1 hr. (2007) % 34.26/34.31 %------------------------------------------------------------------------------ % 34.26/34.31 cnf(init,axiom, % 34.26/34.31 p(s0,s0,s0,s0,s0,s0,s0,s0,s0,s0) ). % 34.26/34.31 % 34.26/34.31 cnf(rule1,axiom, % 34.26/34.31 ( ~ p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s0) % 34.26/34.31 | p(X0,X1,X2,X3,X4,X5,X6,X7,X8,s1) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule2,axiom, % 34.26/34.31 ( ~ p(X0,X1,X2,X3,X4,X5,X6,X7,s0,s1) % 34.26/34.31 | p(X0,X1,X2,X3,X4,X5,X6,X7,s1,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule3,axiom, % 34.26/34.31 ( ~ p(X0,X1,X2,X3,X4,X5,X6,s0,s1,s1) % 34.26/34.31 | p(X0,X1,X2,X3,X4,X5,X6,s1,s0,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule4,axiom, % 34.26/34.31 ( ~ p(X0,X1,X2,X3,X4,X5,s0,s1,s1,s1) % 34.26/34.31 | p(X0,X1,X2,X3,X4,X5,s1,s0,s0,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule5,axiom, % 34.26/34.31 ( ~ p(X0,X1,X2,X3,X4,s0,s1,s1,s1,s1) % 34.26/34.31 | p(X0,X1,X2,X3,X4,s1,s0,s0,s0,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule6,axiom, % 34.26/34.31 ( ~ p(X0,X1,X2,X3,s0,s1,s1,s1,s1,s1) % 34.26/34.31 | p(X0,X1,X2,X3,s1,s0,s0,s0,s0,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule7,axiom, % 34.26/34.31 ( ~ p(X0,X1,X2,s0,s1,s1,s1,s1,s1,s1) % 34.26/34.31 | p(X0,X1,X2,s1,s0,s0,s0,s0,s0,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule8,axiom, % 34.26/34.31 ( ~ p(X0,X1,s0,s1,s1,s1,s1,s1,s1,s1) % 34.26/34.31 | p(X0,X1,s1,s0,s0,s0,s0,s0,s0,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule9,axiom, % 34.26/34.31 ( ~ p(X0,s0,s1,s1,s1,s1,s1,s1,s1,s1) % 34.26/34.31 | p(X0,s1,s0,s0,s0,s0,s0,s0,s0,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(rule10,axiom, % 34.26/34.31 ( ~ p(s0,s1,s1,s1,s1,s1,s1,s1,s1,s1) % 34.26/34.31 | p(s1,s0,s0,s0,s0,s0,s0,s0,s0,s0) ) ). % 34.26/34.31 % 34.26/34.31 cnf(goal,negated_conjecture, % 34.26/34.31 ~ p(s1,s1,s1,s1,s1,s1,s1,s1,s1,s1) ). % 34.26/34.31 % 34.26/34.31 %------------------------------------------------------------------------------ % 34.26/34.31 %------------------------------------------- % 34.26/34.31 % Proof found % 34.26/34.32 % SZS status Theorem for theBenchmark % 34.30/34.32 % SZS output start Proof % 34.30/34.32 %ClaNum:12(EqnAxiom:0) % 34.30/34.32 %VarNum:90(SingletonVarNum:45) % 34.30/34.32 %MaxLitNum:2 % 34.30/34.32 %MaxfuncDepth:0 % 34.30/34.32 %SharedTerms:6 % 34.30/34.32 %goalClause: 2 % 34.30/34.32 %singleGoalClaCount:1 % 34.30/34.32 [1]P1(a1,a1,a1,a1,a1,a1,a1,a1,a1,a1) % 34.30/34.32 [2]~P1(a2,a2,a2,a2,a2,a2,a2,a2,a2,a2) % 34.30/34.32 [3]P1(a2,a1,a1,a1,a1,a1,a1,a1,a1,a1)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2) % 34.30/34.32 [4]~P1(x41,a1,a2,a2,a2,a2,a2,a2,a2,a2)+P1(x41,a2,a1,a1,a1,a1,a1,a1,a1,a1) % 34.30/34.32 [5]~P1(x51,x52,a1,a2,a2,a2,a2,a2,a2,a2)+P1(x51,x52,a2,a1,a1,a1,a1,a1,a1,a1) % 34.30/34.32 [6]~P1(x61,x62,x63,a1,a2,a2,a2,a2,a2,a2)+P1(x61,x62,x63,a2,a1,a1,a1,a1,a1,a1) % 34.30/34.32 [7]~P1(x71,x72,x73,x74,a1,a2,a2,a2,a2,a2)+P1(x71,x72,x73,x74,a2,a1,a1,a1,a1,a1) % 34.30/34.32 [8]~P1(x81,x82,x83,x84,x85,a1,a2,a2,a2,a2)+P1(x81,x82,x83,x84,x85,a2,a1,a1,a1,a1) % 34.30/34.32 [9]~P1(x91,x92,x93,x94,x95,x96,a1,a2,a2,a2)+P1(x91,x92,x93,x94,x95,x96,a2,a1,a1,a1) % 34.30/34.32 [10]~P1(x101,x102,x103,x104,x105,x106,x107,a1,a2,a2)+P1(x101,x102,x103,x104,x105,x106,x107,a2,a1,a1) % 34.30/34.32 [11]~P1(x111,x112,x113,x114,x115,x116,x117,x118,a1,a2)+P1(x111,x112,x113,x114,x115,x116,x117,x118,a2,a1) % 34.30/34.32 [12]~P1(x121,x122,x123,x124,x125,x126,x127,x128,x129,a1)+P1(x121,x122,x123,x124,x125,x126,x127,x128,x129,a2) % 34.30/34.32 %EqnAxiom % 34.30/34.32 % 34.30/34.32 %------------------------------------------- % 34.30/34.32 cnf(15,plain, % 34.30/34.32 (~P1(a2,a2,a2,a2,a2,a2,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[2,12,11])). % 34.30/34.33 cnf(19,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a2,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[15,12,10])). % 34.30/34.33 cnf(23,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a2,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[19,12,11])). % 34.30/34.33 cnf(27,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a2,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[23,12,9])). % 34.30/34.33 cnf(31,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a2,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[27,12,11])). % 34.30/34.33 cnf(35,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a2,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[31,12,10])). % 34.30/34.33 cnf(39,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a2,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[35,12,11])). % 34.30/34.33 cnf(43,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a1,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[39,12,8])). % 34.30/34.33 cnf(47,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a1,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[43,12,11])). % 34.30/34.33 cnf(51,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a1,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[47,12,10])). % 34.30/34.33 cnf(55,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a1,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[51,12,11])). % 34.30/34.33 cnf(59,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a1,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[55,12,9])). % 34.30/34.33 cnf(63,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a1,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[59,12,11])). % 34.30/34.33 cnf(67,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a1,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[63,12,10])). % 34.30/34.33 cnf(71,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a2,a1,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[67,12,11])). % 34.30/34.33 cnf(75,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[71,12,7])). % 34.30/34.33 cnf(77,plain, % 34.30/34.33 (P1(a2,a1,a1,a1,a1,a1,a1,a1,a1,a2)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[3,12])). % 34.30/34.33 cnf(80,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a2,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[75,12,11])). % 34.30/34.33 cnf(84,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a2,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[80,12,10])). % 34.30/34.33 cnf(88,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a2,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[84,12,11])). % 34.30/34.33 cnf(92,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a2,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[88,12,9])). % 34.30/34.33 cnf(96,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a2,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[92,12,11])). % 34.30/34.33 cnf(100,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a2,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[96,12,10])). % 34.30/34.33 cnf(104,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a2,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[100,12,11])). % 34.30/34.33 cnf(108,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a1,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[104,12,8])). % 34.30/34.33 cnf(112,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a1,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[108,12,11])). % 34.30/34.33 cnf(116,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a1,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[112,12,10])). % 34.30/34.33 cnf(120,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a1,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[116,12,11])). % 34.30/34.33 cnf(124,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a1,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[120,12,9])). % 34.30/34.33 cnf(128,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a1,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[124,12,11])). % 34.30/34.33 cnf(132,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a1,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[128,12,10])). % 34.30/34.33 cnf(136,plain, % 34.30/34.33 (~P1(a2,a2,a2,a2,a1,a1,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[132,12,11])). % 34.30/34.33 cnf(138,plain, % 34.30/34.33 (P1(x1381,a2,a1,a1,a1,a1,a1,a1,a1,a2)+~P1(x1381,a1,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[4,12])). % 34.30/34.33 cnf(141,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[136,12,6])). % 34.30/34.33 cnf(145,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a2,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[141,12,11])). % 34.30/34.33 cnf(149,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a2,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[145,12,10])). % 34.30/34.33 cnf(153,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a2,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[149,12,11])). % 34.30/34.33 cnf(157,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a2,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[153,12,9])). % 34.30/34.33 cnf(161,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a2,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[157,12,11])). % 34.30/34.33 cnf(165,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a2,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[161,12,10])). % 34.30/34.33 cnf(169,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a2,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[165,12,11])). % 34.30/34.33 cnf(173,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a1,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[169,12,8])). % 34.30/34.33 cnf(177,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a1,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[173,12,11])). % 34.30/34.33 cnf(181,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a1,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[177,12,10])). % 34.30/34.33 cnf(185,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a1,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[181,12,11])). % 34.30/34.33 cnf(189,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a1,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[185,12,9])). % 34.30/34.33 cnf(193,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a1,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[189,12,11])). % 34.30/34.33 cnf(197,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a1,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[193,12,10])). % 34.30/34.33 cnf(202,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a2,a1,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[197,12,11])). % 34.30/34.33 cnf(206,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[202,12,7])). % 34.30/34.33 cnf(210,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a2,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[206,12,11])). % 34.30/34.33 cnf(214,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a2,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[210,12,10])). % 34.30/34.33 cnf(218,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a2,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[214,12,11])). % 34.30/34.33 cnf(222,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a2,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[218,12,9])). % 34.30/34.33 cnf(226,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a2,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[222,12,11])). % 34.30/34.33 cnf(230,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a2,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[226,12,10])). % 34.30/34.33 cnf(234,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a2,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[230,12,11])). % 34.30/34.33 cnf(238,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a1,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[234,12,8])). % 34.30/34.33 cnf(242,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a1,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[238,12,11])). % 34.30/34.33 cnf(246,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a1,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[242,12,10])). % 34.30/34.33 cnf(250,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a1,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[246,12,11])). % 34.30/34.33 cnf(254,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a1,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[250,12,9])). % 34.30/34.33 cnf(258,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a1,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[254,12,11])). % 34.30/34.33 cnf(260,plain, % 34.30/34.33 (P1(a2,a1,a1,a1,a1,a1,a1,a1,a2,a1)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[77,11])). % 34.30/34.33 cnf(263,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a1,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[258,12,10])). % 34.30/34.33 cnf(267,plain, % 34.30/34.33 (~P1(a2,a2,a2,a1,a1,a1,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[263,12,11])). % 34.30/34.33 cnf(271,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[267,12,5])). % 34.30/34.33 cnf(275,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a2,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[271,12,11])). % 34.30/34.33 cnf(279,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a2,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[275,12,10])). % 34.30/34.33 cnf(283,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a2,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[279,12,11])). % 34.30/34.33 cnf(287,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a2,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[283,12,9])). % 34.30/34.33 cnf(291,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a2,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[287,12,11])). % 34.30/34.33 cnf(295,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a2,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[291,12,10])). % 34.30/34.33 cnf(299,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a2,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[295,12,11])). % 34.30/34.33 cnf(303,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a1,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[299,12,8])). % 34.30/34.33 cnf(307,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a1,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[303,12,11])). % 34.30/34.33 cnf(311,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a1,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[307,12,10])). % 34.30/34.33 cnf(315,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a1,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[311,12,11])). % 34.30/34.33 cnf(319,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a1,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[315,12,9])). % 34.30/34.33 cnf(321,plain, % 34.30/34.33 (~P1(x3211,a1,a2,a2,a2,a2,a2,a2,a2,a1)+P1(x3211,a2,a1,a1,a1,a1,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[138,12])). % 34.30/34.33 cnf(324,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a1,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[319,12,11])). % 34.30/34.33 cnf(328,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a1,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[324,12,10])). % 34.30/34.33 cnf(332,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a2,a1,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[328,12,11])). % 34.30/34.33 cnf(336,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[332,12,7])). % 34.30/34.33 cnf(340,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a2,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[336,12,11])). % 34.30/34.33 cnf(344,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a2,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[340,12,10])). % 34.30/34.33 cnf(348,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a2,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[344,12,11])). % 34.30/34.33 cnf(352,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a2,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[348,12,9])). % 34.30/34.33 cnf(356,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a2,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[352,12,11])). % 34.30/34.33 cnf(360,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a2,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[356,12,10])). % 34.30/34.33 cnf(364,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a2,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[360,12,11])). % 34.30/34.33 cnf(368,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a1,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[364,12,8])). % 34.30/34.33 cnf(372,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a1,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[368,12,11])). % 34.30/34.33 cnf(376,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a1,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[372,12,10])). % 34.30/34.33 cnf(380,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a1,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[376,12,11])). % 34.30/34.33 cnf(384,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a1,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[380,12,9])). % 34.30/34.33 cnf(388,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a1,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[384,12,11])). % 34.30/34.33 cnf(392,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a1,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[388,12,10])). % 34.30/34.33 cnf(396,plain, % 34.30/34.33 (~P1(a2,a2,a1,a2,a1,a1,a1,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[392,12,11])). % 34.30/34.33 cnf(400,plain, % 34.30/34.33 (~P1(a2,a2,a1,a1,a2,a2,a2,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[396,12,6])). % 34.30/34.33 cnf(404,plain, % 34.30/34.33 (~P1(a2,a2,a1,a1,a2,a2,a2,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[400,12,11])). % 34.30/34.33 cnf(408,plain, % 34.30/34.33 (~P1(a2,a2,a1,a1,a2,a2,a2,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[404,12,10])). % 34.30/34.33 cnf(412,plain, % 34.30/34.33 (~P1(a2,a2,a1,a1,a2,a2,a2,a1,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[408,12,11])). % 34.30/34.33 cnf(416,plain, % 34.30/34.33 (~P1(a2,a2,a1,a1,a2,a2,a1,a2,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[412,12,9])). % 34.30/34.33 cnf(420,plain, % 34.30/34.33 (~P1(a2,a2,a1,a1,a2,a2,a1,a2,a1,a2)), % 34.30/34.33 inference(scs_inference,[],[416,12,11])). % 34.30/34.33 cnf(424,plain, % 34.30/34.33 (~P1(a2,a2,a1,a1,a2,a2,a1,a1,a2,a2)), % 34.30/34.33 inference(scs_inference,[],[420,12,10])). % 34.30/34.33 cnf(428,plain, % 34.30/34.33 (~P1(a2,a2,a1,a1,a2,a2,a1,a1,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[424,12,11])). % 34.30/34.34 cnf(432,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a2,a1,a2,a2,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[428,12,8])). % 34.30/34.34 cnf(436,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a2,a1,a2,a2,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[432,12,11])). % 34.30/34.34 cnf(440,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a2,a1,a2,a1,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[436,12,10])). % 34.30/34.34 cnf(442,plain, % 34.30/34.34 (P1(a2,a1,a1,a1,a1,a1,a1,a1,a2,a2)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[260,12])). % 34.30/34.34 cnf(445,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a2,a1,a2,a1,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[440,12,11])). % 34.30/34.34 cnf(449,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a2,a1,a1,a2,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[445,12,9])). % 34.30/34.34 cnf(453,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a2,a1,a1,a2,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[449,12,11])). % 34.30/34.34 cnf(457,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a2,a1,a1,a1,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[453,12,10])). % 34.30/34.34 cnf(461,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a2,a1,a1,a1,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[457,12,11])). % 34.30/34.34 cnf(465,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a2,a2,a2,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[461,12,7])). % 34.30/34.34 cnf(469,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a2,a2,a2,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[465,12,11])). % 34.30/34.34 cnf(473,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a2,a2,a1,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[469,12,10])). % 34.30/34.34 cnf(477,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a2,a2,a1,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[473,12,11])). % 34.30/34.34 cnf(481,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a2,a1,a2,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[477,12,9])). % 34.30/34.34 cnf(485,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a2,a1,a2,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[481,12,11])). % 34.30/34.34 cnf(489,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a2,a1,a1,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[485,12,10])). % 34.30/34.34 cnf(493,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a2,a1,a1,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[489,12,11])). % 34.30/34.34 cnf(497,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a1,a2,a2,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[493,12,8])). % 34.30/34.34 cnf(501,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a1,a2,a2,a1,a2)), % 34.30/34.34 inference(scs_inference,[],[497,12,11])). % 34.30/34.34 cnf(506,plain, % 34.30/34.34 (~P1(a2,a2,a1,a1,a1,a1,a2,a1,a2,a2)), % 34.30/34.34 inference(scs_inference,[],[501,12,10])). % 34.37/34.34 cnf(510,plain, % 34.37/34.34 (~P1(a2,a2,a1,a1,a1,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[506,12,11])). % 34.37/34.34 cnf(514,plain, % 34.37/34.34 (~P1(a2,a2,a1,a1,a1,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[510,12,9])). % 34.37/34.34 cnf(518,plain, % 34.37/34.34 (~P1(a2,a2,a1,a1,a1,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[514,12,11])). % 34.37/34.34 cnf(522,plain, % 34.37/34.34 (~P1(a2,a2,a1,a1,a1,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[518,12,10])). % 34.37/34.34 cnf(528,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a2,a2,a2,a2,a1)), % 34.37/34.34 inference(scs_inference,[],[522,12,11,321])). % 34.37/34.34 cnf(530,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[528,11])). % 34.37/34.34 cnf(538,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[530,12,10])). % 34.37/34.34 cnf(542,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[538,12,11])). % 34.37/34.34 cnf(546,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[542,12,9])). % 34.37/34.34 cnf(550,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[546,12,11])). % 34.37/34.34 cnf(554,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[550,12,10])). % 34.37/34.34 cnf(558,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[554,12,11])). % 34.37/34.34 cnf(562,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[558,12,8])). % 34.37/34.34 cnf(566,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[562,12,11])). % 34.37/34.34 cnf(568,plain, % 34.37/34.34 (P1(a2,a1,a1,a1,a1,a1,a1,a2,a1,a1)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[442,10])). % 34.37/34.34 cnf(571,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[566,12,10])). % 34.37/34.34 cnf(575,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[571,12,11])). % 34.37/34.34 cnf(579,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[575,12,9])). % 34.37/34.34 cnf(583,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[579,12,11])). % 34.37/34.34 cnf(587,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[583,12,10])). % 34.37/34.34 cnf(591,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a2,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[587,12,11])). % 34.37/34.34 cnf(595,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[591,12,7])). % 34.37/34.34 cnf(599,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[595,12,11])). % 34.37/34.34 cnf(603,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[599,12,10])). % 34.37/34.34 cnf(607,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[603,12,11])). % 34.37/34.34 cnf(611,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[607,12,9])). % 34.37/34.34 cnf(615,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[611,12,11])). % 34.37/34.34 cnf(619,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[615,12,10])). % 34.37/34.34 cnf(623,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[619,12,11])). % 34.37/34.34 cnf(627,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[623,12,8])). % 34.37/34.34 cnf(631,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[627,12,11])). % 34.37/34.34 cnf(635,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[631,12,10])). % 34.37/34.34 cnf(639,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[635,12,11])). % 34.37/34.34 cnf(643,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[639,12,9])). % 34.37/34.34 cnf(647,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[643,12,11])). % 34.37/34.34 cnf(651,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[647,12,10])). % 34.37/34.34 cnf(655,plain, % 34.37/34.34 (~P1(a2,a1,a2,a2,a1,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[651,12,11])). % 34.37/34.34 cnf(659,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[655,12,6])). % 34.37/34.34 cnf(663,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[659,12,11])). % 34.37/34.34 cnf(667,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[663,12,10])). % 34.37/34.34 cnf(671,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[667,12,11])). % 34.37/34.34 cnf(675,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[671,12,9])). % 34.37/34.34 cnf(679,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[675,12,11])). % 34.37/34.34 cnf(683,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[679,12,10])). % 34.37/34.34 cnf(687,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[683,12,11])). % 34.37/34.34 cnf(689,plain, % 34.37/34.34 (P1(a2,a1,a1,a1,a1,a1,a1,a2,a1,a2)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[568,12])). % 34.37/34.34 cnf(692,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[687,12,8])). % 34.37/34.34 cnf(696,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[692,12,11])). % 34.37/34.34 cnf(700,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[696,12,10])). % 34.37/34.34 cnf(704,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[700,12,11])). % 34.37/34.34 cnf(708,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[704,12,9])). % 34.37/34.34 cnf(712,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[708,12,11])). % 34.37/34.34 cnf(716,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[712,12,10])). % 34.37/34.34 cnf(720,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a2,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[716,12,11])). % 34.37/34.34 cnf(724,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[720,12,7])). % 34.37/34.34 cnf(728,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[724,12,11])). % 34.37/34.34 cnf(732,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[728,12,10])). % 34.37/34.34 cnf(736,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[732,12,11])). % 34.37/34.34 cnf(740,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[736,12,9])). % 34.37/34.34 cnf(744,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[740,12,11])). % 34.37/34.34 cnf(748,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[744,12,10])). % 34.37/34.34 cnf(750,plain, % 34.37/34.34 (P1(a2,a1,a1,a1,a1,a1,a1,a2,a2,a1)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[689,11])). % 34.37/34.34 cnf(753,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[748,12,11])). % 34.37/34.34 cnf(757,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[753,12,8])). % 34.37/34.34 cnf(761,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[757,12,11])). % 34.37/34.34 cnf(765,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[761,12,10])). % 34.37/34.34 cnf(769,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[765,12,11])). % 34.37/34.34 cnf(773,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[769,12,9])). % 34.37/34.34 cnf(777,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[773,12,11])). % 34.37/34.34 cnf(781,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[777,12,10])). % 34.37/34.34 cnf(785,plain, % 34.37/34.34 (~P1(a2,a1,a2,a1,a1,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[781,12,11])). % 34.37/34.34 cnf(789,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[785,12,5])). % 34.37/34.34 cnf(793,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[789,12,11])). % 34.37/34.34 cnf(797,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[793,12,10])). % 34.37/34.34 cnf(801,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[797,12,11])). % 34.37/34.34 cnf(805,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[801,12,9])). % 34.37/34.34 cnf(809,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[805,12,11])). % 34.37/34.34 cnf(811,plain, % 34.37/34.34 (P1(a2,a1,a1,a1,a1,a1,a1,a2,a2,a2)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[750,12])). % 34.37/34.34 cnf(814,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[809,12,10])). % 34.37/34.34 cnf(818,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[814,12,11])). % 34.37/34.34 cnf(822,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[818,12,8])). % 34.37/34.34 cnf(826,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[822,12,11])). % 34.37/34.34 cnf(830,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[826,12,10])). % 34.37/34.34 cnf(834,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[830,12,11])). % 34.37/34.34 cnf(838,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[834,12,9])). % 34.37/34.34 cnf(842,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[838,12,11])). % 34.37/34.34 cnf(846,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[842,12,10])). % 34.37/34.34 cnf(850,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a2,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[846,12,11])). % 34.37/34.34 cnf(854,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[850,12,7])). % 34.37/34.34 cnf(858,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[854,12,11])). % 34.37/34.34 cnf(862,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[858,12,10])). % 34.37/34.34 cnf(866,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[862,12,11])). % 34.37/34.34 cnf(870,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[866,12,9])). % 34.37/34.34 cnf(872,plain, % 34.37/34.34 (P1(a2,a1,a1,a1,a1,a1,a2,a1,a1,a1)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[811,9])). % 34.37/34.34 cnf(875,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[870,12,11])). % 34.37/34.34 cnf(879,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[875,12,10])). % 34.37/34.34 cnf(883,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[879,12,11])). % 34.37/34.34 cnf(887,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[883,12,8])). % 34.37/34.34 cnf(891,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[887,12,11])). % 34.37/34.34 cnf(895,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[891,12,10])). % 34.37/34.34 cnf(899,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[895,12,11])). % 34.37/34.34 cnf(903,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[899,12,9])). % 34.37/34.34 cnf(907,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[903,12,11])). % 34.37/34.34 cnf(911,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[907,12,10])). % 34.37/34.34 cnf(915,plain, % 34.37/34.34 (~P1(a2,a1,a1,a2,a1,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[911,12,11])). % 34.37/34.34 cnf(919,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[915,12,6])). % 34.37/34.34 cnf(923,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[919,12,11])). % 34.37/34.34 cnf(927,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[923,12,10])). % 34.37/34.34 cnf(931,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[927,12,11])). % 34.37/34.34 cnf(933,plain, % 34.37/34.34 (P1(a2,a1,a1,a1,a1,a1,a2,a1,a1,a2)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[872,12])). % 34.37/34.34 cnf(936,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[931,12,9])). % 34.37/34.34 cnf(940,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[936,12,11])). % 34.37/34.34 cnf(944,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[940,12,10])). % 34.37/34.34 cnf(948,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[944,12,11])). % 34.37/34.34 cnf(952,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[948,12,8])). % 34.37/34.34 cnf(956,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[952,12,11])). % 34.37/34.34 cnf(960,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[956,12,10])). % 34.37/34.34 cnf(964,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[960,12,11])). % 34.37/34.34 cnf(968,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[964,12,9])). % 34.37/34.34 cnf(972,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[968,12,11])). % 34.37/34.34 cnf(976,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[972,12,10])). % 34.37/34.34 cnf(980,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a2,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[976,12,11])). % 34.37/34.34 cnf(984,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[980,12,7])). % 34.37/34.34 cnf(988,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[984,12,11])). % 34.37/34.34 cnf(992,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[988,12,10])). % 34.37/34.34 cnf(994,plain, % 34.37/34.34 (P1(a2,a1,a1,a1,a1,a1,a2,a1,a2,a1)+~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[933,11])). % 34.37/34.34 cnf(997,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[992,12,11])). % 34.37/34.34 cnf(1001,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[997,12,9])). % 34.37/34.34 cnf(1005,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1001,12,11])). % 34.37/34.34 cnf(1009,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1005,12,10])). % 34.37/34.34 cnf(1013,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1009,12,11])). % 34.37/34.34 cnf(1017,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1013,12,8])). % 34.37/34.34 cnf(1021,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1017,12,11])). % 34.37/34.34 cnf(1025,plain, % 34.37/34.34 (~P1(a2,a1,a1,a1,a1,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1021,12,10])). % 34.37/34.34 cnf(1029,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1025,12,994])). % 34.37/34.34 cnf(1052,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1029,12,11])). % 34.37/34.34 cnf(1056,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1052,12,10])). % 34.37/34.34 cnf(1060,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1056,12,11])). % 34.37/34.34 cnf(1064,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1060,12,9])). % 34.37/34.34 cnf(1068,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1064,12,11])). % 34.37/34.34 cnf(1072,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1068,12,10])). % 34.37/34.34 cnf(1076,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1072,12,11])). % 34.37/34.34 cnf(1080,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1076,12,8])). % 34.37/34.34 cnf(1084,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1080,12,11])). % 34.37/34.34 cnf(1088,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1084,12,10])). % 34.37/34.34 cnf(1092,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1088,12,11])). % 34.37/34.34 cnf(1096,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1092,12,9])). % 34.37/34.34 cnf(1100,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1096,12,11])). % 34.37/34.34 cnf(1104,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1100,12,10])). % 34.37/34.34 cnf(1108,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a2,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1104,12,11])). % 34.37/34.34 cnf(1112,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1108,12,7])). % 34.37/34.34 cnf(1116,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1112,12,11])). % 34.37/34.34 cnf(1120,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1116,12,10])). % 34.37/34.34 cnf(1124,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1120,12,11])). % 34.37/34.34 cnf(1128,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1124,12,9])). % 34.37/34.34 cnf(1132,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1128,12,11])). % 34.37/34.34 cnf(1136,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1132,12,10])). % 34.37/34.34 cnf(1140,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1136,12,11])). % 34.37/34.34 cnf(1144,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1140,12,8])). % 34.37/34.34 cnf(1148,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1144,12,11])). % 34.37/34.34 cnf(1152,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1148,12,10])). % 34.37/34.34 cnf(1156,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1152,12,11])). % 34.37/34.34 cnf(1160,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1156,12,9])). % 34.37/34.34 cnf(1164,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1160,12,11])). % 34.37/34.34 cnf(1168,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1164,12,10])). % 34.37/34.34 cnf(1172,plain, % 34.37/34.34 (~P1(a1,a2,a2,a2,a1,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1168,12,11])). % 34.37/34.34 cnf(1174,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1172,6,12])). % 34.37/34.34 cnf(1177,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1174,12,11])). % 34.37/34.34 cnf(1181,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1177,12,10])). % 34.37/34.34 cnf(1185,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1181,12,11])). % 34.37/34.34 cnf(1189,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1185,12,9])). % 34.37/34.34 cnf(1193,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1189,12,11])). % 34.37/34.34 cnf(1197,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1193,12,10])). % 34.37/34.34 cnf(1201,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a2,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1197,12,11])). % 34.37/34.34 cnf(1205,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a1,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1201,12,8])). % 34.37/34.34 cnf(1209,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a1,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1205,12,11])). % 34.37/34.34 cnf(1213,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a1,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1209,12,10])). % 34.37/34.34 cnf(1217,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a1,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1213,12,11])). % 34.37/34.34 cnf(1221,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a1,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1217,12,9])). % 34.37/34.34 cnf(1225,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a1,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1221,12,11])). % 34.37/34.34 cnf(1229,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a1,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1225,12,10])). % 34.37/34.34 cnf(1233,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a2,a1,a1,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1229,12,11])). % 34.37/34.34 cnf(1237,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a1,a2,a2,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1233,12,7])). % 34.37/34.34 cnf(1241,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a1,a2,a2,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1237,12,11])). % 34.37/34.34 cnf(1245,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a1,a2,a2,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1241,12,10])). % 34.37/34.34 cnf(1249,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a1,a2,a2,a1,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1245,12,11])). % 34.37/34.34 cnf(1253,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a1,a2,a1,a2,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1249,12,9])). % 34.37/34.34 cnf(1257,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a1,a2,a1,a2,a1,a2)), % 34.37/34.34 inference(scs_inference,[],[1253,12,11])). % 34.37/34.34 cnf(1261,plain, % 34.37/34.34 (~P1(a1,a2,a2,a1,a1,a2,a1,a1,a2,a2)), % 34.37/34.34 inference(scs_inference,[],[1257,12,10])). % 34.37/34.34 cnf(1265,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1261,12,11])). % 34.37/34.35 cnf(1269,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1265,12,8])). % 34.37/34.35 cnf(1273,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1269,12,11])). % 34.37/34.35 cnf(1277,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1273,12,10])). % 34.37/34.35 cnf(1281,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1277,12,11])). % 34.37/34.35 cnf(1285,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1281,12,9])). % 34.37/34.35 cnf(1289,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1285,12,11])). % 34.37/34.35 cnf(1293,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1289,12,10])). % 34.37/34.35 cnf(1297,plain, % 34.37/34.35 (~P1(a1,a2,a2,a1,a1,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1293,12,11])). % 34.37/34.35 cnf(1301,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1297,12,5])). % 34.37/34.35 cnf(1305,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1301,12,11])). % 34.37/34.35 cnf(1309,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1305,12,10])). % 34.37/34.35 cnf(1313,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1309,12,11])). % 34.37/34.35 cnf(1317,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1313,12,9])). % 34.37/34.35 cnf(1321,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1317,12,11])). % 34.37/34.35 cnf(1325,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1321,12,10])). % 34.37/34.35 cnf(1329,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1325,12,11])). % 34.37/34.35 cnf(1333,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1329,12,8])). % 34.37/34.35 cnf(1337,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1333,12,11])). % 34.37/34.35 cnf(1341,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1337,12,10])). % 34.37/34.35 cnf(1345,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1341,12,11])). % 34.37/34.35 cnf(1349,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1345,12,9])). % 34.37/34.35 cnf(1353,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1349,12,11])). % 34.37/34.35 cnf(1357,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1353,12,10])). % 34.37/34.35 cnf(1361,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a2,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1357,12,11])). % 34.37/34.35 cnf(1365,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1361,12,7])). % 34.37/34.35 cnf(1369,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1365,12,11])). % 34.37/34.35 cnf(1373,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1369,12,10])). % 34.37/34.35 cnf(1377,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1373,12,11])). % 34.37/34.35 cnf(1381,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1377,12,9])). % 34.37/34.35 cnf(1385,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1381,12,11])). % 34.37/34.35 cnf(1389,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1385,12,10])). % 34.37/34.35 cnf(1393,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1389,12,11])). % 34.37/34.35 cnf(1397,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1393,12,8])). % 34.37/34.35 cnf(1401,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1397,12,11])). % 34.37/34.35 cnf(1405,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1401,12,10])). % 34.37/34.35 cnf(1409,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1405,12,11])). % 34.37/34.35 cnf(1413,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1409,12,9])). % 34.37/34.35 cnf(1417,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1413,12,11])). % 34.37/34.35 cnf(1421,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1417,12,10])). % 34.37/34.35 cnf(1425,plain, % 34.37/34.35 (~P1(a1,a2,a1,a2,a1,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1421,12,11])). % 34.37/34.35 cnf(1429,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1425,12,6])). % 34.37/34.35 cnf(1433,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1429,12,11])). % 34.37/34.35 cnf(1437,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1433,12,10])). % 34.37/34.35 cnf(1441,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1437,12,11])). % 34.37/34.35 cnf(1445,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1441,12,9])). % 34.37/34.35 cnf(1449,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1445,12,11])). % 34.37/34.35 cnf(1453,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1449,12,10])). % 34.37/34.35 cnf(1457,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1453,12,11])). % 34.37/34.35 cnf(1461,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1457,12,8])). % 34.37/34.35 cnf(1465,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1461,12,11])). % 34.37/34.35 cnf(1469,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1465,12,10])). % 34.37/34.35 cnf(1473,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1469,12,11])). % 34.37/34.35 cnf(1477,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1473,12,9])). % 34.37/34.35 cnf(1481,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1477,12,11])). % 34.37/34.35 cnf(1485,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1481,12,10])). % 34.37/34.35 cnf(1489,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a2,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1485,12,11])). % 34.37/34.35 cnf(1493,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1489,12,7])). % 34.37/34.35 cnf(1497,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1493,12,11])). % 34.37/34.35 cnf(1501,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1497,12,10])). % 34.37/34.35 cnf(1505,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1501,12,11])). % 34.37/34.35 cnf(1509,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1505,12,9])). % 34.37/34.35 cnf(1513,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1509,12,11])). % 34.37/34.35 cnf(1517,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1513,12,10])). % 34.37/34.35 cnf(1521,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1517,12,11])). % 34.37/34.35 cnf(1525,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1521,12,8])). % 34.37/34.35 cnf(1529,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1525,12,11])). % 34.37/34.35 cnf(1533,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1529,12,10])). % 34.37/34.35 cnf(1537,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1533,12,11])). % 34.37/34.35 cnf(1541,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1537,12,9])). % 34.37/34.35 cnf(1545,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1541,12,11])). % 34.37/34.35 cnf(1549,plain, % 34.37/34.35 (~P1(a1,a2,a1,a1,a1,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1545,12,10])). % 34.37/34.35 cnf(1555,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a2,a2,a2,a2,a1)), % 34.37/34.35 inference(scs_inference,[],[1549,12,11,321])). % 34.37/34.35 cnf(1557,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1555,11])). % 34.37/34.35 cnf(1565,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1557,12,10])). % 34.37/34.35 cnf(1569,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1565,12,11])). % 34.37/34.35 cnf(1573,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1569,12,9])). % 34.37/34.35 cnf(1577,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1573,12,11])). % 34.37/34.35 cnf(1581,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1577,12,10])). % 34.37/34.35 cnf(1585,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1581,12,11])). % 34.37/34.35 cnf(1589,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1585,12,8])). % 34.37/34.35 cnf(1593,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1589,12,11])). % 34.37/34.35 cnf(1597,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1593,12,10])). % 34.37/34.35 cnf(1599,plain, % 34.37/34.35 (P1(a1,a1,a1,a1,a1,a1,a1,a1,a2,a1)), % 34.37/34.35 inference(scs_inference,[],[1,12,11])). % 34.37/34.35 cnf(1602,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1597,12,11])). % 34.37/34.35 cnf(1606,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1602,12,9])). % 34.37/34.35 cnf(1610,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1606,12,11])). % 34.37/34.35 cnf(1614,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1610,12,10])). % 34.37/34.35 cnf(1618,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a2,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1614,12,11])). % 34.37/34.35 cnf(1622,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1618,12,7])). % 34.37/34.35 cnf(1626,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1622,12,11])). % 34.37/34.35 cnf(1630,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1626,12,10])). % 34.37/34.35 cnf(1634,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1630,12,11])). % 34.37/34.35 cnf(1638,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1634,12,9])). % 34.37/34.35 cnf(1642,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1638,12,11])). % 34.37/34.35 cnf(1646,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1642,12,10])). % 34.37/34.35 cnf(1650,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1646,12,11])). % 34.37/34.35 cnf(1654,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1650,12,8])). % 34.37/34.35 cnf(1658,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1654,12,11])). % 34.37/34.35 cnf(1660,plain, % 34.37/34.35 (P1(a1,a1,a1,a1,a1,a1,a1,a2,a1,a1)), % 34.37/34.35 inference(scs_inference,[],[1599,12,10])). % 34.37/34.35 cnf(1663,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1658,12,10])). % 34.37/34.35 cnf(1667,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1663,12,11])). % 34.37/34.35 cnf(1671,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1667,12,9])). % 34.37/34.35 cnf(1675,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1671,12,11])). % 34.37/34.35 cnf(1679,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1675,12,10])). % 34.37/34.35 cnf(1683,plain, % 34.37/34.35 (~P1(a1,a1,a2,a2,a1,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1679,12,11])). % 34.37/34.35 cnf(1687,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1683,12,6])). % 34.37/34.35 cnf(1691,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1687,12,11])). % 34.37/34.35 cnf(1695,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1691,12,10])). % 34.37/34.35 cnf(1699,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1695,12,11])). % 34.37/34.35 cnf(1703,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1699,12,9])). % 34.37/34.35 cnf(1707,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1703,12,11])). % 34.37/34.35 cnf(1711,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1707,12,10])). % 34.37/34.35 cnf(1715,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1711,12,11])). % 34.37/34.35 cnf(1719,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1715,12,8])). % 34.37/34.35 cnf(1721,plain, % 34.37/34.35 (P1(a1,a1,a1,a1,a1,a1,a1,a2,a2,a1)), % 34.37/34.35 inference(scs_inference,[],[1660,12,11])). % 34.37/34.35 cnf(1724,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1719,12,11])). % 34.37/34.35 cnf(1728,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1724,12,10])). % 34.37/34.35 cnf(1732,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1728,12,11])). % 34.37/34.35 cnf(1736,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1732,12,9])). % 34.37/34.35 cnf(1740,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1736,12,11])). % 34.37/34.35 cnf(1744,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1740,12,10])). % 34.37/34.35 cnf(1748,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a2,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1744,12,11])). % 34.37/34.35 cnf(1752,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1748,12,7])). % 34.37/34.35 cnf(1756,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1752,12,11])). % 34.37/34.35 cnf(1760,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1756,12,10])). % 34.37/34.35 cnf(1764,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1760,12,11])). % 34.37/34.35 cnf(1768,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1764,12,9])). % 34.37/34.35 cnf(1772,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1768,12,11])). % 34.37/34.35 cnf(1776,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1772,12,10])). % 34.37/34.35 cnf(1780,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1776,12,11])). % 34.37/34.35 cnf(1782,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1780,12,8])). % 34.37/34.35 cnf(1785,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1782,12,11])). % 34.37/34.35 cnf(1789,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1785,12,10])). % 34.37/34.35 cnf(1793,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1789,12,11])). % 34.37/34.35 cnf(1797,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1793,12,9])). % 34.37/34.35 cnf(1801,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1797,12,11])). % 34.37/34.35 cnf(1805,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1801,12,10])). % 34.37/34.35 cnf(1809,plain, % 34.37/34.35 (~P1(a1,a1,a2,a1,a1,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1805,12,11])). % 34.37/34.35 cnf(1813,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1809,12,5])). % 34.37/34.35 cnf(1817,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1813,12,11])). % 34.37/34.35 cnf(1821,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1817,12,10])). % 34.37/34.35 cnf(1825,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1821,12,11])). % 34.37/34.35 cnf(1829,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1825,12,9])). % 34.37/34.35 cnf(1833,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1829,12,11])). % 34.37/34.35 cnf(1837,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1833,12,10])). % 34.37/34.35 cnf(1841,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1837,12,11])). % 34.37/34.35 cnf(1843,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1841,12,8])). % 34.37/34.35 cnf(1846,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1843,12,11])). % 34.37/34.35 cnf(1850,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1846,12,10])). % 34.37/34.35 cnf(1854,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1850,12,11])). % 34.37/34.35 cnf(1858,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1854,12,9])). % 34.37/34.35 cnf(1862,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1858,12,11])). % 34.37/34.35 cnf(1866,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1862,12,10])). % 34.37/34.35 cnf(1870,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a2,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1866,12,11])). % 34.37/34.35 cnf(1874,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1870,12,7])). % 34.37/34.35 cnf(1878,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1874,12,11])). % 34.37/34.35 cnf(1882,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1878,12,10])). % 34.37/34.35 cnf(1886,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1882,12,11])). % 34.37/34.35 cnf(1890,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1886,12,9])). % 34.37/34.35 cnf(1894,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1890,12,11])). % 34.37/34.35 cnf(1898,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1894,12,10])). % 34.37/34.35 cnf(1902,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1898,12,11])). % 34.37/34.35 cnf(1904,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1902,12,8])). % 34.37/34.35 cnf(1907,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1904,12,11])). % 34.37/34.35 cnf(1911,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1907,12,10])). % 34.37/34.35 cnf(1915,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1911,12,11])). % 34.37/34.35 cnf(1919,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1915,12,9])). % 34.37/34.35 cnf(1923,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1919,12,11])). % 34.37/34.35 cnf(1927,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1923,12,10])). % 34.37/34.35 cnf(1931,plain, % 34.37/34.35 (~P1(a1,a1,a1,a2,a1,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1927,12,11])). % 34.37/34.35 cnf(1935,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1931,12,6])). % 34.37/34.35 cnf(1939,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1935,12,11])). % 34.37/34.35 cnf(1943,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1939,12,10])). % 34.37/34.35 cnf(1947,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1943,12,11])). % 34.37/34.35 cnf(1951,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1947,12,9])). % 34.37/34.35 cnf(1955,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1951,12,11])). % 34.37/34.35 cnf(1959,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1955,12,10])). % 34.37/34.35 cnf(1963,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1959,12,11])). % 34.37/34.35 cnf(1965,plain, % 34.37/34.35 (P1(a1,a1,a1,a1,a1,a1,a2,a1,a1,a1)), % 34.37/34.35 inference(scs_inference,[],[1721,12,9])). % 34.37/34.35 cnf(1968,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1963,12,8])). % 34.37/34.35 cnf(1972,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1968,12,11])). % 34.37/34.35 cnf(1976,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1972,12,10])). % 34.37/34.35 cnf(1980,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a1,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1976,12,11])). % 34.37/34.35 cnf(1984,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a1,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1980,12,9])). % 34.37/34.35 cnf(1988,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a1,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1984,12,11])). % 34.37/34.35 cnf(1992,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a1,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1988,12,10])). % 34.37/34.35 cnf(1996,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a2,a1,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[1992,12,11])). % 34.37/34.35 cnf(2000,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a2,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[1996,12,7])). % 34.37/34.35 cnf(2004,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a2,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[2000,12,11])). % 34.37/34.35 cnf(2008,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a2,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[2004,12,10])). % 34.37/34.35 cnf(2012,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a2,a2,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[2008,12,11])). % 34.37/34.35 cnf(2016,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a2,a1,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[2012,12,9])). % 34.37/34.35 cnf(2020,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a2,a1,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[2016,12,11])). % 34.37/34.35 cnf(2024,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a2,a1,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[2020,12,10])). % 34.37/34.35 cnf(2026,plain, % 34.37/34.35 (P1(a1,a1,a1,a1,a1,a1,a2,a1,a2,a1)), % 34.37/34.35 inference(scs_inference,[],[1965,12,11])). % 34.37/34.35 cnf(2029,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a2,a1,a1,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[2024,12,11])). % 34.37/34.35 cnf(2033,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a1,a2,a2,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[2029,12,8])). % 34.37/34.35 cnf(2037,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a1,a2,a2,a1,a2)), % 34.37/34.35 inference(scs_inference,[],[2033,12,11])). % 34.37/34.35 cnf(2041,plain, % 34.37/34.35 (~P1(a1,a1,a1,a1,a1,a1,a2,a1,a2,a2)), % 34.37/34.35 inference(scs_inference,[],[2037,12,10])). % 34.37/34.35 cnf(2043,plain, % 34.37/34.35 ($false), % 34.37/34.35 inference(scs_inference,[],[2041,2026,12]), % 34.37/34.35 ['proof']). % 34.37/34.35 % SZS output end Proof % 34.37/34.35 % Total time :33.690000s %------------------------------------------------------------------------------