%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LAT005-2 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n001.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 10:17:56 EDT 2024
% Result : Unsatisfiable 181.00s 181.18s
% Output : CNFRefutation 181.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : LAT005-2 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.34 % Computer : n001.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Sat Jun 22 00:28:39 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.47/0.58 start to proof:theBenchmark
% 180.93/181.16 %-------------------------------------------
% 180.93/181.16 % File :CSE---1.7
% 180.93/181.16 % Problem :theBenchmark
% 181.00/181.16 % Transform :cnf
% 181.00/181.16 % Format :tptp:raw
% 181.00/181.16 % Command :java -jar mcs_scs.jar %d %s
% 181.00/181.16
% 181.00/181.16 % Result :Theorem 180.350000s
% 181.00/181.16 % Output :CNFRefutation 180.350000s
% 181.00/181.16 %-------------------------------------------
% 181.00/181.17 %--------------------------------------------------------------------------
% 181.00/181.17 % File : LAT005-2 : TPTP v8.2.0. Released v1.0.0.
% 181.00/181.17 % Domain : Lattice Theory
% 181.00/181.17 % Problem : SAM's lemma
% 181.00/181.17 % Version : [McCharen, et al., 1986] axioms :
% 181.00/181.17 % Incomplete > Augmented > Incomplete.
% 181.00/181.17 % English : Let L be a modular lattice with 0 and 1. Suppose that A and
% 181.00/181.17 % B are elements of L such that (A v B) and (A ^ B) both have
% 181.00/181.17 % not necessarily unique complements. Then, (A v B)' =
% 181.00/181.17 % ((A v B)' v ((A ^ B)' ^ B)) ^ ((A v B)' v ((A ^ B)' ^ A)).
% 181.00/181.17
% 181.00/181.17 % Refs : [GO+69] Guard et al. (1969), Semi-Automated Mathematics
% 181.00/181.17 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 181.00/181.17 % : [LM92] Lusk & McCune (1992), Experiments with ROO, a Parallel
% 181.00/181.17 % Source : [OTTER]
% 181.00/181.17 % Names : SAM's lemma [LM92]
% 181.00/181.17 % : sam.in [OTTER]
% 181.00/181.17 % : sam_hyp.in [OTTER]
% 181.00/181.17
% 181.00/181.17 % Status : Unsatisfiable
% 181.00/181.17 % Rating : 0.00 v7.0.0, 0.14 v6.4.0, 0.00 v6.1.0, 0.12 v6.0.0, 0.25 v5.5.0, 0.00 v2.5.0, 0.50 v2.4.0, 0.00 v2.2.0, 0.56 v2.1.0, 0.00 v2.0.0
% 181.00/181.17 % Syntax : Number of clauses : 31 ( 21 unt; 0 nHn; 21 RR)
% 181.00/181.17 % Number of literals : 55 ( 0 equ; 25 neg)
% 181.00/181.17 % Maximal clause size : 5 ( 1 avg)
% 181.00/181.17 % Maximal term depth : 1 ( 1 avg)
% 181.00/181.17 % Number of predicates : 2 ( 2 usr; 0 prp; 3-3 aty)
% 181.00/181.17 % Number of functors : 12 ( 12 usr; 12 con; 0-0 aty)
% 181.00/181.17 % Number of variables : 58 ( 6 sgn)
% 181.00/181.17 % SPC : CNF_UNS_EPR_NEQ_HRN
% 181.00/181.17
% 181.00/181.17 % Comments : Redundant commuted versions of the axioms for meet and join
% 181.00/181.17 % with 0 and 1, are supplied.
% 181.00/181.17 %--------------------------------------------------------------------------
% 181.00/181.17 %----Include Lattice theory axioms
% 181.00/181.17 % include('Axioms/LAT002-0.ax').
% 181.00/181.17 %--------------------------------------------------------------------------
% 181.00/181.17 %----Union of 1 and x is equal to 1 : (1 v X) = 1
% 181.00/181.17 cnf(join_1_and_x,axiom,
% 181.00/181.17 join(n1,X,n1) ).
% 181.00/181.17
% 181.00/181.17 %----Redundant commuted version
% 181.00/181.17 cnf(join_x_and_1,axiom,
% 181.00/181.17 join(X,n1,n1) ).
% 181.00/181.17
% 181.00/181.17 %----Union of x with itself is equal to x : (X v X) = X
% 181.00/181.17 cnf(join_x_and_x,axiom,
% 181.00/181.17 join(X,X,X) ).
% 181.00/181.17
% 181.00/181.18 %----Union of 0 and x is equal to x : (0 v X) = X
% 181.00/181.18 cnf(join_0_and_x,axiom,
% 181.00/181.18 join(n0,X,X) ).
% 181.00/181.18
% 181.00/181.18 %----Redundant commuted version
% 181.00/181.18 cnf(join_x_and_0,axiom,
% 181.00/181.18 join(X,n0,X) ).
% 181.00/181.18
% 181.00/181.18 %----Intersection of 0 and x is equal to 0 : (0 ^ X) = 0
% 181.00/181.18 cnf(meet_0_and_x,axiom,
% 181.00/181.18 meet(n0,X,n0) ).
% 181.00/181.18
% 181.00/181.18 %----Redundant commuted version
% 181.00/181.18 cnf(meet_x_and_0,axiom,
% 181.00/181.18 meet(X,n0,n0) ).
% 181.00/181.18
% 181.00/181.18 %----Intersection of x and itself is equal to x : (X ^ X) = X
% 181.00/181.18 cnf(meet_x_and_x,axiom,
% 181.00/181.18 meet(X,X,X) ).
% 181.00/181.18
% 181.00/181.18 %----Intersection of 1 and x is equal to itself : (1 ^ X) = X
% 181.00/181.18 cnf(meet_1_and_x,axiom,
% 181.00/181.18 meet(n1,X,X) ).
% 181.00/181.18
% 181.00/181.18 %----Redundant commuted version
% 181.00/181.18 cnf(meet_x_and_1,axiom,
% 181.00/181.18 meet(X,n1,X) ).
% 181.00/181.18
% 181.00/181.18 %----Intersection of x and y , is the same as meet of y and x.
% 181.00/181.18 %---- (X ^ Y) = (Y ^ X),
% 181.00/181.18 cnf(commutativity_of_meet,axiom,
% 181.00/181.18 ( ~ meet(X,Y,Z)
% 181.00/181.18 | meet(Y,X,Z) ) ).
% 181.00/181.18
% 181.00/181.18 %----Union of x and y is the same as join of y and x. (X v Y) = (Y v X),
% 181.00/181.18 cnf(commutativity_of_join,axiom,
% 181.00/181.18 ( ~ join(X,Y,Z)
% 181.00/181.18 | join(Y,X,Z) ) ).
% 181.00/181.18
% 181.00/181.18 %----Union of x with the meet of x and y is the same as x.
% 181.00/181.18 %---- X v (X ^ Y) = X
% 181.00/181.18 cnf(absorbtion1,axiom,
% 181.00/181.18 ( ~ meet(X,Y,Z)
% 181.00/181.18 | join(X,Z,X) ) ).
% 181.00/181.18
% 181.00/181.18 %----Intersection of x with the join of x and y is the same as x.
% 181.00/181.18 %---- X ^ (X v Y) = X
% 181.00/181.18 cnf(absorbtion2,axiom,
% 181.00/181.18 ( ~ join(X,Y,Z)
% 181.00/181.18 | meet(X,Z,X) ) ).
% 181.00/181.18
% 181.00/181.18 %----The operation '^', meet ,is associative
% 181.00/181.18 %---- X ^ (Y ^ Z) = (X ^ Y) ^ Z
% 181.00/181.18 cnf(associativity_of_meet1,axiom,
% 181.00/181.18 ( ~ meet(X,Y,Xy)
% 181.00/181.18 | ~ meet(Y,Z,Yz)
% 181.00/181.18 | ~ meet(X,Yz,Xyz)
% 181.00/181.18 | meet(Xy,Z,Xyz) ) ).
% 181.00/181.18
% 181.00/181.18 cnf(associativity_of_meet2,axiom,
% 181.00/181.18 ( ~ meet(X,Y,Xy)
% 181.00/181.18 | ~ meet(Y,Z,Yz)
% 181.00/181.18 | ~ meet(Xy,Z,Xyz)
% 181.00/181.18 | meet(X,Yz,Xyz) ) ).
% 181.00/181.18
% 181.00/181.18 %----The operation 'v' is associative X v (Y v Z) = (X v Y) v Z
% 181.00/181.18 cnf(associativity_of_join1,axiom,
% 181.00/181.18 ( ~ join(X,Y,Xy)
% 181.00/181.18 | ~ join(Y,Z,Yz)
% 181.00/181.18 | ~ join(X,Yz,Xyz)
% 181.00/181.18 | join(Xy,Z,Xyz) ) ).
% 181.00/181.18
% 181.00/181.18 cnf(associativity_of_join2,axiom,
% 181.00/181.18 ( ~ join(X,Y,Xy)
% 181.00/181.18 | ~ join(Y,Z,Yz)
% 181.00/181.18 | ~ join(Xy,Z,Xyz)
% 181.00/181.18 | join(X,Yz,Xyz) ) ).
% 181.00/181.18
% 181.00/181.18 %----(X ^ Z) = X implies that (Z ^ (X v Y)) = (X v (Y ^ Z)),
% 181.00/181.18 cnf(modularity1,axiom,
% 181.00/181.18 ( ~ meet(X,Z,X)
% 181.00/181.18 | ~ join(X,Y,X1)
% 181.00/181.18 | ~ meet(Y,Z,Y1)
% 181.00/181.18 | ~ meet(Z,X1,Z1)
% 181.00/181.18 | join(X,Y1,Z1) ) ).
% 181.00/181.18
% 181.00/181.18 cnf(modularity2,axiom,
% 181.00/181.18 ( ~ meet(X,Z,X)
% 181.00/181.18 | ~ join(X,Y,X1)
% 181.00/181.18 | ~ meet(Y,Z,Y1)
% 181.00/181.18 | ~ join(X,Y1,Z1)
% 181.00/181.18 | meet(Z,X1,Z1) ) ).
% 181.00/181.18
% 181.00/181.18 %----Negation of Sams Lemma :
% 181.00/181.18 cnf(meet_a2_and_b2,negated_conjecture,
% 181.00/181.18 ~ meet(a2,b2,r1) ).
% 181.00/181.18
% 181.00/181.18 cnf(meet_a_and_b,negated_conjecture,
% 181.00/181.18 meet(a,b,c) ).
% 181.00/181.18
% 181.00/181.18 cnf(join_c_and_r2,negated_conjecture,
% 181.00/181.18 join(c,r2,n1) ).
% 181.00/181.18
% 181.00/181.18 cnf(meet_c_and_r2,negated_conjecture,
% 181.00/181.18 meet(c,r2,n0) ).
% 181.00/181.18
% 181.00/181.18 cnf(meet_r2_and_b,negated_conjecture,
% 181.00/181.18 meet(r2,b,e) ).
% 181.00/181.18
% 181.00/181.18 cnf(join_a_and_b,negated_conjecture,
% 181.00/181.18 join(a,b,c2) ).
% 181.00/181.18
% 181.00/181.18 cnf(join_c2_and_r1,negated_conjecture,
% 181.00/181.18 join(c2,r1,n1) ).
% 181.00/181.18
% 181.00/181.18 cnf(meet_c2_and_r1,negated_conjecture,
% 181.00/181.18 meet(c2,r1,n0) ).
% 181.00/181.18
% 181.00/181.18 cnf(meet_r2_and_a,negated_conjecture,
% 181.00/181.18 meet(r2,a,d) ).
% 181.00/181.18
% 181.00/181.18 cnf(join_r1_and_e,negated_conjecture,
% 181.00/181.18 join(r1,e,a2) ).
% 181.00/181.18
% 181.00/181.18 cnf(join_r1_and_d,negated_conjecture,
% 181.00/181.18 join(r1,d,b2) ).
% 181.00/181.18
% 181.00/181.18 %--------------------------------------------------------------------------
% 181.00/181.18 %-------------------------------------------
% 181.00/181.18 % Proof found
% 181.00/181.18 % SZS status Theorem for theBenchmark
% 181.00/181.18 % SZS output start Proof
% 181.00/181.18 %ClaNum:31(EqnAxiom:0)
% 181.00/181.18 %VarNum:120(SingletonVarNum:58)
% 181.00/181.18 %MaxLitNum:5
% 181.00/181.18 %MaxfuncDepth:0
% 181.00/181.18 %SharedTerms:23
% 181.00/181.18 %goalClause: 1 2 3 4 5 6 7 8 9 10 21
% 181.00/181.18 %singleGoalClaCount:11
% 181.00/181.18 [1]P1(a1,a2,a3)
% 181.00/181.18 [2]P1(a1,a5,a6)
% 181.00/181.18 [3]P1(a4,a7,a8)
% 181.00/181.18 [4]P1(a9,a12,a10)
% 181.00/181.18 [5]P1(a8,a1,a10)
% 181.00/181.18 [6]P2(a4,a7,a9)
% 181.00/181.18 [7]P2(a9,a12,a11)
% 181.00/181.18 [8]P2(a12,a4,a5)
% 181.00/181.18 [9]P2(a12,a7,a2)
% 181.00/181.18 [10]P2(a8,a1,a11)
% 181.00/181.18 [21]~P2(a3,a6,a1)
% 181.00/181.18 [11]P1(x111,a10,a10)
% 181.00/181.18 [12]P2(x121,a11,a11)
% 181.00/181.18 [13]P1(a10,x131,a10)
% 181.00/181.18 [14]P2(a11,x141,a11)
% 181.00/181.18 [15]P1(x151,a11,x151)
% 181.00/181.18 [16]P2(x161,a10,x161)
% 181.00/181.18 [17]P1(a11,x171,x171)
% 181.00/181.18 [18]P2(a10,x181,x181)
% 181.00/181.18 [19]P1(x191,x191,x191)
% 181.00/181.18 [20]P2(x201,x201,x201)
% 181.00/181.18 [22]~P1(x222,x221,x223)+P1(x221,x222,x223)
% 181.00/181.18 [23]P1(x231,x232,x231)+~P2(x231,x233,x232)
% 181.00/181.18 [24]~P2(x242,x241,x243)+P2(x241,x242,x243)
% 181.00/181.18 [25]P2(x251,x252,x251)+~P1(x251,x253,x252)
% 181.00/181.18 [26]~P1(x266,x264,x261)+P1(x261,x262,x263)+~P1(x264,x262,x265)+~P1(x266,x265,x263)
% 181.00/181.18 [27]~P1(x271,x276,x274)+P1(x271,x272,x273)+~P1(x274,x275,x273)+~P1(x276,x275,x272)
% 181.00/181.18 [28]~P2(x286,x284,x281)+P2(x281,x282,x283)+~P2(x284,x282,x285)+~P2(x286,x285,x283)
% 181.00/181.18 [29]~P2(x291,x296,x294)+P2(x291,x292,x293)+~P2(x294,x295,x293)+~P2(x296,x295,x292)
% 181.00/181.18 [30]~P2(x306,x305,x303)+~P2(x301,x306,x301)+P1(x301,x302,x303)+~P1(x301,x304,x305)+~P2(x304,x306,x302)
% 181.00/181.18 [31]~P2(x316,x311,x315)+~P2(x314,x311,x314)+P2(x311,x312,x313)+~P1(x314,x315,x313)+~P1(x314,x316,x312)
% 181.00/181.18 %EqnAxiom
% 181.00/181.18
% 181.00/181.18 %-------------------------------------------
% 181.00/181.20 cnf(32,plain,
% 181.00/181.20 (~P2(a6,a3,a1)),
% 181.00/181.20 inference(scs_inference,[],[21,24])).
% 181.00/181.20 cnf(34,plain,
% 181.00/181.20 (P1(a3,a2,a3)),
% 181.00/181.20 inference(scs_inference,[],[1,21,19,24,26])).
% 181.00/181.20 cnf(37,plain,
% 181.00/181.20 (P1(a8,a3,a10)),
% 181.00/181.20 inference(scs_inference,[],[1,5,21,19,13,24,26,27])).
% 181.00/181.20 cnf(40,plain,
% 181.00/181.20 (P2(a9,a7,a9)),
% 181.00/181.20 inference(scs_inference,[],[1,5,6,21,19,20,13,24,26,27,28])).
% 181.00/181.20 cnf(43,plain,
% 181.00/181.20 (P2(a9,a5,a11)),
% 181.00/181.20 inference(scs_inference,[],[1,5,6,7,8,21,19,20,13,14,24,26,27,28,29])).
% 181.00/181.20 cnf(53,plain,
% 181.00/181.20 (P1(a8,a6,a10)),
% 181.00/181.20 inference(scs_inference,[],[2,5,13,27])).
% 181.00/181.20 cnf(56,plain,
% 181.00/181.20 (P2(a9,a2,a11)),
% 181.00/181.20 inference(scs_inference,[],[2,9,5,7,13,14,27,29])).
% 181.00/181.20 cnf(59,plain,
% 181.00/181.20 (P1(a9,a2,a7)),
% 181.00/181.20 inference(scs_inference,[],[2,4,9,5,7,16,40,13,14,27,29,30])).
% 181.00/181.20 cnf(60,plain,
% 181.00/181.20 (P2(x601,a10,x601)),
% 181.00/181.20 inference(rename_variables,[],[16])).
% 181.00/181.20 cnf(62,plain,
% 181.00/181.20 (P2(a2,x621,a12)+~P2(a7,x621,a10)),
% 181.00/181.20 inference(scs_inference,[],[2,4,9,5,7,16,60,40,13,14,27,29,30,28])).
% 181.00/181.20 cnf(65,plain,
% 181.00/181.20 (P1(a3,x651,a1)+~P1(a2,x651,a11)),
% 181.00/181.20 inference(scs_inference,[],[1,2,4,9,5,7,15,16,60,40,13,14,27,29,30,28,26])).
% 181.00/181.20 cnf(66,plain,
% 181.00/181.20 (P1(x661,a11,x661)),
% 181.00/181.20 inference(rename_variables,[],[15])).
% 181.00/181.20 cnf(68,plain,
% 181.00/181.20 (~P2(a1,a11,a1)+P2(a11,a3,a1)),
% 181.00/181.20 inference(scs_inference,[],[1,2,4,9,5,7,15,66,16,60,12,40,13,14,27,29,30,28,26,31])).
% 181.00/181.20 cnf(72,plain,
% 181.00/181.20 (P2(a5,a4,a5)),
% 181.00/181.20 inference(scs_inference,[],[8,20,28])).
% 181.00/181.20 cnf(73,plain,
% 181.00/181.20 (P2(x731,x731,x731)),
% 181.00/181.20 inference(rename_variables,[],[20])).
% 181.00/181.20 cnf(75,plain,
% 181.00/181.20 (P1(a8,a7,a8)),
% 181.00/181.20 inference(scs_inference,[],[3,8,19,20,28,26])).
% 181.00/181.20 cnf(78,plain,
% 181.00/181.20 (P1(a1,a10,x781)+~P1(a3,a10,x781)),
% 181.00/181.20 inference(scs_inference,[],[1,3,8,11,19,20,28,26,27])).
% 181.00/181.20 cnf(81,plain,
% 181.00/181.20 (P2(a12,a9,x811)+~P2(a5,a7,x811)),
% 181.00/181.20 inference(scs_inference,[],[1,3,8,6,11,19,20,28,26,27,29])).
% 181.00/181.20 cnf(84,plain,
% 181.00/181.20 (P2(x841,x841,x841)),
% 181.00/181.20 inference(rename_variables,[],[20])).
% 181.00/181.20 cnf(86,plain,
% 181.00/181.20 (~P2(a4,a7,a4)+P2(a7,a8,a8)),
% 181.00/181.20 inference(scs_inference,[],[1,3,8,6,11,19,20,73,84,28,26,27,29,30,31])).
% 181.00/181.20 cnf(89,plain,
% 181.00/181.20 (P1(a1,a2,x891)+~P1(a3,a11,x891)),
% 181.00/181.20 inference(scs_inference,[],[1,15,27])).
% 181.00/181.20 cnf(101,plain,
% 181.00/181.20 (P1(a6,a5,a6)),
% 181.00/181.20 inference(scs_inference,[],[2,19,26])).
% 181.00/181.20 cnf(118,plain,
% 181.00/181.20 (P2(a2,x1181,a11)+~P2(a7,x1181,a11)),
% 181.00/181.20 inference(scs_inference,[],[9,12,28])).
% 181.00/181.20 cnf(128,plain,
% 181.00/181.20 (P2(a2,x1281,a12)+~P2(a7,x1281,a12)),
% 181.00/181.20 inference(scs_inference,[],[9,20,28])).
% 181.00/181.20 cnf(131,plain,
% 181.00/181.20 (P2(a12,a11,a12)+~P2(a7,a11,a12)),
% 181.00/181.20 inference(scs_inference,[],[9,12,20,28,29])).
% 181.00/181.20 cnf(141,plain,
% 181.00/181.20 (P2(a12,a7,x1411)+~P2(a2,a10,x1411)),
% 181.00/181.20 inference(scs_inference,[],[9,16,29])).
% 181.00/181.20 cnf(142,plain,
% 181.00/181.20 (P2(x1421,a10,x1421)),
% 181.00/181.20 inference(rename_variables,[],[16])).
% 181.00/181.20 cnf(144,plain,
% 181.00/181.20 (P1(a9,x1441,a7)+~P2(a2,a10,x1441)),
% 181.00/181.20 inference(scs_inference,[],[4,9,40,16,142,29,30])).
% 181.00/181.20 cnf(179,plain,
% 181.00/181.20 (P2(a12,a7,x1791)+~P2(a2,a7,x1791)),
% 181.00/181.20 inference(scs_inference,[],[9,20,29])).
% 181.00/181.20 cnf(182,plain,
% 181.00/181.20 (P2(a2,a10,x1821)+~P2(a2,a7,x1821)),
% 181.00/181.20 inference(scs_inference,[],[9,16,20,29,28])).
% 181.00/181.20 cnf(183,plain,
% 181.00/181.20 (P2(x1831,a10,x1831)),
% 181.00/181.20 inference(rename_variables,[],[16])).
% 181.00/181.20 cnf(185,plain,
% 181.00/181.20 (P1(a9,x1851,a7)+~P2(a2,a7,x1851)),
% 181.00/181.20 inference(scs_inference,[],[9,4,40,16,183,20,29,28,30])).
% 181.00/181.20 cnf(231,plain,
% 181.00/181.20 (P2(a2,a3,a2)),
% 181.00/181.20 inference(scs_inference,[],[1,22,25])).
% 181.00/181.20 cnf(232,plain,
% 181.00/181.20 (P1(a12,a11,a2)+~P1(a12,a9,a7)),
% 181.00/181.20 inference(scs_inference,[],[9,7,20,30])).
% 181.00/181.20 cnf(235,plain,
% 181.00/181.20 (P1(a9,a2,a10)+~P1(a12,a9,a7)),
% 181.00/181.20 inference(scs_inference,[],[9,4,7,15,20,30,27])).
% 181.00/181.20 cnf(243,plain,
% 181.00/181.20 (P1(a9,a9,a7)+~P1(a9,a4,a10)),
% 181.00/181.20 inference(scs_inference,[],[6,16,40,30])).
% 181.00/181.20 cnf(307,plain,
% 181.00/181.20 (P1(a12,a12,a2)+~P1(a12,a10,a7)),
% 181.00/181.20 inference(scs_inference,[],[9,20,18,30])).
% 181.00/181.20 cnf(334,plain,
% 181.00/181.20 (P1(a2,a12,a12)),
% 181.00/181.20 inference(scs_inference,[],[9,23,22])).
% 181.00/181.20 cnf(347,plain,
% 181.00/181.20 (P1(a1,a5,x3471)+~P1(a6,a11,x3471)),
% 181.00/181.20 inference(scs_inference,[],[2,15,27])).
% 181.00/181.20 cnf(361,plain,
% 181.00/181.20 (P1(a1,a10,x3611)+~P1(a6,a10,x3611)),
% 181.00/181.20 inference(scs_inference,[],[2,11,27])).
% 181.00/181.20 cnf(375,plain,
% 181.00/181.20 (P1(a6,x3751,a1)+~P1(a5,x3751,a11)),
% 181.00/181.20 inference(scs_inference,[],[2,15,26])).
% 181.00/181.20 cnf(386,plain,
% 181.00/181.20 (P1(a6,x3861,a10)+~P1(a5,x3861,a10)),
% 181.00/181.20 inference(scs_inference,[],[2,11,26])).
% 181.00/181.20 cnf(450,plain,
% 181.00/181.20 (P1(a4,a8,a8)),
% 181.00/181.20 inference(scs_inference,[],[3,19,27])).
% 181.00/181.20 cnf(454,plain,
% 181.00/181.20 (P1(a9,a7,a7)),
% 181.00/181.20 inference(scs_inference,[],[59,19,27])).
% 181.00/181.20 cnf(457,plain,
% 181.00/181.20 (~P2(x4571,a7,a10)+P2(a2,x4571,a12)),
% 181.00/181.20 inference(scs_inference,[],[62,24])).
% 181.00/181.20 cnf(458,plain,
% 181.00/181.20 (~P1(x4581,a2,a11)+P1(a3,x4581,a1)),
% 181.00/181.20 inference(scs_inference,[],[65,22])).
% 181.00/181.20 cnf(460,plain,
% 181.00/181.20 (P1(x4601,a11,x4601)),
% 181.00/181.20 inference(rename_variables,[],[15])).
% 181.00/181.20 cnf(463,plain,
% 181.00/181.20 (P1(x4631,a11,x4631)),
% 181.00/181.20 inference(rename_variables,[],[15])).
% 181.00/181.20 cnf(465,plain,
% 181.00/181.20 (P2(x4651,a10,x4651)),
% 181.00/181.20 inference(rename_variables,[],[16])).
% 181.00/181.20 cnf(470,plain,
% 181.00/181.20 (~P2(a4,a11,a4)+~P1(a8,a11,x4701)+P2(a11,a8,a4)),
% 181.00/181.20 inference(scs_inference,[],[3,9,6,8,15,460,463,16,465,20,12,27,26,31])).
% 181.00/181.20 cnf(472,plain,
% 181.00/181.20 (~P2(a4,a11,a4)+P2(a11,a8,a4)),
% 181.00/181.20 inference(scs_inference,[],[15,470])).
% 181.00/181.20 cnf(473,plain,
% 181.00/181.20 (P1(a4,a10,x4731)+~P1(a8,a10,x4731)),
% 181.00/181.20 inference(scs_inference,[],[3,11,27])).
% 181.00/181.20 cnf(496,plain,
% 181.00/181.20 (P1(a8,x4961,a10)+~P1(a7,x4961,a10)),
% 181.00/181.20 inference(scs_inference,[],[3,11,26])).
% 181.00/181.20 cnf(507,plain,
% 181.00/181.20 (P1(a8,x5071,a4)+~P1(a7,x5071,a4)),
% 181.00/181.20 inference(scs_inference,[],[3,19,26])).
% 181.00/181.20 cnf(510,plain,
% 181.00/181.20 (~P1(a7,a10,a4)+P1(a4,a10,a4)),
% 181.00/181.20 inference(scs_inference,[],[3,19,26,473])).
% 181.00/181.20 cnf(542,plain,
% 181.00/181.20 (P2(a4,a7,x5421)+~P2(a9,a10,x5421)),
% 181.00/181.20 inference(scs_inference,[],[6,16,29])).
% 181.00/181.20 cnf(543,plain,
% 181.00/181.20 (P2(x5431,a10,x5431)),
% 181.00/181.20 inference(rename_variables,[],[16])).
% 181.00/181.20 cnf(548,plain,
% 181.00/181.20 (~P2(a9,a10,a4)+P2(a7,a8,a8)),
% 181.00/181.20 inference(scs_inference,[],[6,16,543,29,28,86])).
% 181.00/181.20 cnf(556,plain,
% 181.00/181.20 (~P2(a7,a5,x5561)+P2(a12,a9,x5561)),
% 181.00/181.20 inference(scs_inference,[],[81,24])).
% 181.00/181.20 cnf(572,plain,
% 181.00/181.20 (P2(a9,x5721,a4)+~P2(a7,x5721,a10)),
% 181.00/181.20 inference(scs_inference,[],[6,16,28])).
% 181.00/181.20 cnf(586,plain,
% 181.00/181.20 (P2(a9,x5861,a4)+~P2(a7,x5861,a4)),
% 181.00/181.20 inference(scs_inference,[],[6,20,28])).
% 181.00/181.20 cnf(589,plain,
% 181.00/181.20 (~P2(a7,a10,a4)+P2(a4,a7,a4)),
% 181.00/181.20 inference(scs_inference,[],[6,20,28,542])).
% 181.00/181.20 cnf(611,plain,
% 181.00/181.20 (P1(a4,a4,a9)+~P1(a4,a4,a7)),
% 181.00/181.20 inference(scs_inference,[],[6,20,30])).
% 181.00/181.20 cnf(619,plain,
% 181.00/181.20 (P1(a4,a4,a9)+~P1(a4,a10,a7)),
% 181.00/181.20 inference(scs_inference,[],[6,20,18,30])).
% 181.00/181.20 cnf(632,plain,
% 181.00/181.20 (P1(x6321,a11,x6321)),
% 181.00/181.20 inference(rename_variables,[],[15])).
% 181.00/181.20 cnf(636,plain,
% 181.00/181.20 (P2(x6361,a10,x6361)),
% 181.00/181.20 inference(rename_variables,[],[16])).
% 181.00/181.20 cnf(639,plain,
% 181.00/181.20 (P1(x6391,a9,a9)+~P1(a12,a11,a11)),
% 181.00/181.20 inference(scs_inference,[],[4,15,632,16,636,11,20,26,31,30])).
% 181.00/181.20 cnf(645,plain,
% 181.00/181.20 (P1(a10,x6451,a9)+~P1(a12,x6451,a9)),
% 181.00/181.20 inference(scs_inference,[],[4,19,26])).
% 181.00/181.20 cnf(673,plain,
% 181.00/181.20 (~P2(a12,a10,a9)+P2(a10,a10,a9)),
% 181.00/181.20 inference(scs_inference,[],[4,16,19,31])).
% 181.00/181.20 cnf(752,plain,
% 181.00/181.20 (~P2(x7521,a7,a12)+P2(a2,x7521,a12)),
% 181.00/181.20 inference(scs_inference,[],[128,24])).
% 181.00/181.20 cnf(787,plain,
% 181.00/181.21 (P2(a12,a4,x7871)+~P2(a5,a10,x7871)),
% 181.00/181.21 inference(scs_inference,[],[8,16,29])).
% 181.00/181.21 cnf(801,plain,
% 181.00/181.21 (P2(a12,a11,x8011)+~P2(a5,a11,x8011)),
% 181.00/181.21 inference(scs_inference,[],[8,12,29])).
% 181.00/181.21 cnf(814,plain,
% 181.00/181.21 (P2(a5,x8141,a12)+~P2(a4,x8141,a10)),
% 181.00/181.21 inference(scs_inference,[],[8,16,28])).
% 181.00/181.21 cnf(817,plain,
% 181.00/181.21 (~P2(a4,a7,a10)+P2(a12,a9,a12)),
% 181.00/181.21 inference(scs_inference,[],[8,16,28,81])).
% 181.00/181.21 cnf(825,plain,
% 181.00/181.21 (P2(a5,x8251,a12)+~P2(a4,x8251,a12)),
% 181.00/181.21 inference(scs_inference,[],[8,20,28])).
% 181.00/181.21 cnf(828,plain,
% 181.00/181.21 (~P2(a4,a11,a12)+P2(a12,a11,a12)),
% 181.00/181.21 inference(scs_inference,[],[8,20,28,801])).
% 181.00/181.21 cnf(835,plain,
% 181.00/181.21 (P2(a5,x8351,a11)+~P2(a4,x8351,a11)),
% 181.00/181.21 inference(scs_inference,[],[8,12,28])).
% 181.00/181.21 cnf(838,plain,
% 181.00/181.21 (~P2(a4,a10,a11)+P2(a12,a4,a11)),
% 181.00/181.21 inference(scs_inference,[],[8,12,28,787])).
% 181.00/181.21 cnf(848,plain,
% 181.00/181.21 (P1(a9,a5,a10)+~P1(a12,a9,a4)),
% 181.00/181.21 inference(scs_inference,[],[8,7,4,15,20,30,27])).
% 181.00/181.21 cnf(857,plain,
% 181.00/181.21 (P1(a12,a12,a5)+~P1(a12,a12,a4)),
% 181.00/181.21 inference(scs_inference,[],[8,20,30])).
% 181.00/181.21 cnf(875,plain,
% 181.00/181.21 (P1(a11,a11,a5)+~P1(a11,a11,a4)),
% 181.00/181.21 inference(scs_inference,[],[8,14,30])).
% 181.00/181.21 cnf(879,plain,
% 181.00/181.21 (~P2(a5,a3,a11)+~P2(a1,a3,a1)),
% 181.00/181.21 inference(scs_inference,[],[2,21,15,31])).
% 181.00/181.21 cnf(900,plain,
% 181.00/181.21 (~P1(a11,x9001,a6)+~P2(x9001,a3,a1)),
% 181.00/181.21 inference(scs_inference,[],[21,14,17,31])).
% 181.00/181.21 cnf(905,plain,
% 181.00/181.21 (~P1(a11,a11,a6)+~P1(a1,x9051,a11)),
% 181.00/181.21 inference(scs_inference,[],[21,14,17,31,68,25])).
% 181.00/181.21 cnf(946,plain,
% 181.00/181.21 (~P2(a10,x9461,a3)+~P2(x9461,a6,a1)),
% 181.00/181.21 inference(scs_inference,[],[21,18,28])).
% 181.00/181.21 cnf(1002,plain,
% 181.00/181.21 (~P2(a7,a2,x10021)+P2(a12,a7,x10021)),
% 181.00/181.21 inference(scs_inference,[],[179,24])).
% 181.00/181.21 cnf(1013,plain,
% 181.00/181.21 (~P2(a7,a7,a10)+P2(a2,a10,a12)),
% 181.00/181.21 inference(scs_inference,[],[182,62])).
% 181.00/181.21 cnf(1032,plain,
% 181.00/181.21 (P1(a12,a11,a11)+~P1(a12,a9,a11)),
% 181.00/181.21 inference(scs_inference,[],[12,7,20,30])).
% 181.00/181.21 cnf(1062,plain,
% 181.00/181.21 (~P1(a5,a9,a11)+P1(a1,a5,a1)),
% 181.00/181.21 inference(scs_inference,[],[12,20,43,30,375,347])).
% 181.00/181.21 cnf(1074,plain,
% 181.00/181.21 (~P1(a2,a9,a11)+P1(a1,a2,a1)),
% 181.00/181.21 inference(scs_inference,[],[12,20,56,30,65,89])).
% 181.00/181.21 cnf(1080,plain,
% 181.00/181.21 (~P2(a7,a7,a11)+P1(a9,a11,a7)),
% 181.00/181.21 inference(scs_inference,[],[185,118])).
% 181.00/181.21 cnf(1081,plain,
% 181.00/181.21 (P1(a10,a3,x10811)+~P1(a10,a2,x10811)),
% 181.00/181.21 inference(scs_inference,[],[13,1,27])).
% 181.00/181.21 cnf(1095,plain,
% 181.00/181.21 (P1(a10,a6,x10951)+~P1(a10,a5,x10951)),
% 181.00/181.21 inference(scs_inference,[],[13,2,27])).
% 181.00/181.21 cnf(1108,plain,
% 181.00/181.21 (P1(a10,a8,x11081)+~P1(a10,a7,x11081)),
% 181.00/181.21 inference(scs_inference,[],[13,3,27])).
% 181.00/181.21 cnf(1121,plain,
% 181.00/181.21 (P1(a10,a10,x11211)+~P1(a10,a1,x11211)),
% 181.00/181.21 inference(scs_inference,[],[13,5,27])).
% 181.00/181.21 cnf(1134,plain,
% 181.00/181.21 (P1(a10,a10,x11341)+~P1(a10,a12,x11341)),
% 181.00/181.21 inference(scs_inference,[],[13,4,27])).
% 181.00/181.21 cnf(1147,plain,
% 181.00/181.21 (P1(a10,a10,x11471)+~P1(a10,a3,x11471)),
% 181.00/181.21 inference(scs_inference,[],[13,37,27])).
% 181.00/181.21 cnf(1160,plain,
% 181.00/181.21 (P1(a10,a10,x11601)+~P1(a10,a6,x11601)),
% 181.00/181.21 inference(scs_inference,[],[13,53,27])).
% 181.00/181.21 cnf(1183,plain,
% 181.00/181.21 (P1(a10,x11831,a10)),
% 181.00/181.21 inference(rename_variables,[],[13])).
% 181.00/181.21 cnf(1185,plain,
% 181.00/181.21 (P1(a10,a7,x11851)+~P1(a10,a8,x11851)),
% 181.00/181.21 inference(scs_inference,[],[13,1183,6,8,3,450,27,29,26])).
% 181.00/181.21 cnf(1203,plain,
% 181.00/181.21 (P1(a10,a7,x12031)+~P1(a10,a2,x12031)),
% 181.00/181.21 inference(scs_inference,[],[13,59,27])).
% 181.00/181.21 cnf(1290,plain,
% 181.00/181.21 (P2(a11,a11,x12901)+~P2(a11,a2,x12901)),
% 181.00/181.21 inference(scs_inference,[],[14,56,29])).
% 181.00/181.21 cnf(1300,plain,
% 181.00/181.21 (P1(a11,a9,a7)+~P1(a11,a4,a10)),
% 181.00/181.21 inference(scs_inference,[],[14,6,16,30])).
% 181.00/181.21 cnf(1315,plain,
% 181.00/181.21 (P1(a11,a11,a2)+~P1(a11,a9,a7)),
% 181.00/181.21 inference(scs_inference,[],[14,9,7,30])).
% 181.00/181.21 cnf(1316,plain,
% 181.00/181.21 (P2(a11,x13161,a11)),
% 181.00/181.21 inference(rename_variables,[],[14])).
% 181.00/181.21 cnf(1318,plain,
% 181.00/181.21 (P2(x13181,a2,a2)+~P1(a11,a9,a7)),
% 181.00/181.21 inference(scs_inference,[],[14,1316,9,7,30,31])).
% 181.00/181.21 cnf(1320,plain,
% 181.00/181.21 (~P1(a11,a9,a7)+P2(a11,a11,a2)),
% 181.00/181.21 inference(scs_inference,[],[14,1316,9,7,30,31,1290])).
% 181.00/181.21 cnf(1325,plain,
% 181.00/181.21 (P1(a11,a11,a5)+~P1(a11,a9,a10)),
% 181.00/181.21 inference(scs_inference,[],[14,16,43,30])).
% 181.00/181.21 cnf(1371,plain,
% 181.00/181.21 (~P1(a9,a12,a7)+P1(a12,a11,a2)),
% 181.00/181.21 inference(scs_inference,[],[232,22])).
% 181.00/181.21 cnf(1372,plain,
% 181.00/181.21 (~P1(a9,a12,a7)+P1(a9,a2,a10)),
% 181.00/181.21 inference(scs_inference,[],[235,22])).
% 181.00/181.21 cnf(1373,plain,
% 181.00/181.21 (P1(a7,a2,a7)),
% 181.00/181.21 inference(scs_inference,[],[19,59,26])).
% 181.00/181.21 cnf(1374,plain,
% 181.00/181.21 (P1(x13741,x13741,x13741)),
% 181.00/181.21 inference(rename_variables,[],[19])).
% 181.00/181.21 cnf(1376,plain,
% 181.00/181.21 (P1(a1,a3,a3)),
% 181.00/181.21 inference(scs_inference,[],[19,1374,1,59,26,27])).
% 181.00/181.21 cnf(1380,plain,
% 181.00/181.21 (P1(a1,a6,a6)),
% 181.00/181.21 inference(scs_inference,[],[19,2,27])).
% 181.00/181.21 cnf(1385,plain,
% 181.00/181.21 (P2(a4,a9,a9)),
% 181.00/181.21 inference(scs_inference,[],[20,6,29])).
% 181.00/181.21 cnf(1386,plain,
% 181.00/181.21 (P2(x13861,x13861,x13861)),
% 181.00/181.21 inference(rename_variables,[],[20])).
% 181.00/181.21 cnf(1388,plain,
% 181.00/181.21 (P1(a8,a2,a8)),
% 181.00/181.21 inference(scs_inference,[],[20,6,3,1373,29,26])).
% 181.00/181.21 cnf(1390,plain,
% 181.00/181.21 (P2(a2,a7,a2)),
% 181.00/181.21 inference(scs_inference,[],[20,1386,6,3,9,1373,29,26,28])).
% 181.00/181.21 cnf(1401,plain,
% 181.00/181.21 (P2(a12,a2,a2)),
% 181.00/181.21 inference(scs_inference,[],[20,9,29])).
% 181.00/181.21 cnf(1417,plain,
% 181.00/181.21 (P2(a12,a5,a5)),
% 181.00/181.21 inference(scs_inference,[],[20,8,29])).
% 181.00/181.21 cnf(1469,plain,
% 181.00/181.21 (P2(a12,a9,x14691)+~P2(a5,a9,x14691)),
% 181.00/181.21 inference(scs_inference,[],[8,1385,29])).
% 181.00/181.21 cnf(1540,plain,
% 181.00/181.21 (~P2(a6,a2,a11)+~P2(a1,a6,a1)),
% 181.00/181.21 inference(scs_inference,[],[32,1,15,31,24])).
% 181.00/181.21 cnf(1546,plain,
% 181.00/181.21 (~P2(a2,a6,a1)+~P2(a1,a6,a1)),
% 181.00/181.21 inference(scs_inference,[],[32,1,19,31])).
% 181.00/181.21 cnf(1572,plain,
% 181.00/181.21 (P1(a7,a12,a10)),
% 181.00/181.21 inference(scs_inference,[],[4,334,59,26])).
% 181.00/181.21 cnf(1574,plain,
% 181.00/181.21 (P1(a8,a12,a10)),
% 181.00/181.21 inference(scs_inference,[],[4,334,59,26,496])).
% 181.00/181.21 cnf(1604,plain,
% 181.00/181.21 (P1(a3,a2,x16041)+~P1(a3,a11,x16041)),
% 181.00/181.21 inference(scs_inference,[],[34,15,27])).
% 181.00/181.21 cnf(1623,plain,
% 181.00/181.21 (P2(a12,a2,a12)+~P1(a12,a10,a7)),
% 181.00/181.21 inference(scs_inference,[],[307,25])).
% 181.00/181.21 cnf(1624,plain,
% 181.00/181.21 (~P1(a11,a8,x16241)+P1(x16241,a3,a10)),
% 181.00/181.21 inference(scs_inference,[],[37,17,26])).
% 181.00/181.21 cnf(1646,plain,
% 181.00/181.21 (P2(a9,a7,x16461)+~P2(a9,a10,x16461)),
% 181.00/181.21 inference(scs_inference,[],[40,16,29])).
% 181.00/181.21 cnf(1715,plain,
% 181.00/181.21 (~P1(a11,a8,x17151)+P1(x17151,a6,a10)),
% 181.00/181.21 inference(scs_inference,[],[53,17,26])).
% 181.00/181.21 cnf(1766,plain,
% 181.00/181.21 (~P1(a4,a9,x17661)+P1(x17661,a2,a8)),
% 181.00/181.21 inference(scs_inference,[],[59,3,26])).
% 181.00/181.21 cnf(1781,plain,
% 181.00/181.21 (~P1(a8,a9,a2)+P2(a3,a8,a8)),
% 181.00/181.21 inference(scs_inference,[],[59,75,231,1373,26,27,31])).
% 181.00/181.21 cnf(1792,plain,
% 181.00/181.21 (~P1(a7,a9,a10)+P1(a10,a10,a7)),
% 181.00/181.21 inference(scs_inference,[],[59,19,26,1081,1147])).
% 181.00/181.21 cnf(1796,plain,
% 181.00/181.21 (~P1(a7,a9,a10)+P1(a10,a8,a7)),
% 181.00/181.21 inference(scs_inference,[],[59,19,26,1081,1147,1203,1108])).
% 181.00/181.21 cnf(1803,plain,
% 181.00/181.21 (~P1(a11,a9,x18031)+P1(x18031,a2,a7)),
% 181.00/181.21 inference(scs_inference,[],[59,17,26])).
% 181.00/181.21 cnf(1833,plain,
% 181.00/181.21 (P1(a9,a2,x18331)+~P1(a7,a11,x18331)),
% 181.00/181.21 inference(scs_inference,[],[59,15,27])).
% 181.00/181.21 cnf(1842,plain,
% 181.00/181.21 (P1(a9,a10,x18421)+~P1(a7,a10,x18421)),
% 181.00/181.21 inference(scs_inference,[],[59,11,27])).
% 181.00/181.21 cnf(1864,plain,
% 181.00/181.21 (P2(a5,a9,x18641)+~P2(a5,a7,x18641)),
% 181.00/181.21 inference(scs_inference,[],[72,6,29])).
% 181.00/181.21 cnf(1872,plain,
% 181.00/181.21 (P2(a5,a4,x18721)+~P2(a5,a10,x18721)),
% 181.00/181.21 inference(scs_inference,[],[72,16,29])).
% 181.00/181.21 cnf(1883,plain,
% 181.00/181.21 (P1(a8,a7,x18831)+~P1(a8,a11,x18831)),
% 181.00/181.21 inference(scs_inference,[],[75,15,27])).
% 181.00/181.21 cnf(1893,plain,
% 181.00/181.21 (P1(a6,a5,x18931)+~P1(a6,a11,x18931)),
% 181.00/181.21 inference(scs_inference,[],[101,15,27])).
% 181.00/181.21 cnf(1950,plain,
% 181.00/181.21 (P2(a3,a1,a3)+~P1(x19501,a2,a11)),
% 181.00/181.21 inference(scs_inference,[],[458,25])).
% 181.00/181.21 cnf(1997,plain,
% 181.00/181.21 (P1(a11,a4,a11)+~P2(a4,a11,a4)),
% 181.00/181.21 inference(scs_inference,[],[472,23])).
% 181.00/181.21 cnf(2098,plain,
% 181.00/181.21 (P1(a11,a11,a5)+~P1(a11,a9,a4)),
% 181.00/181.21 inference(scs_inference,[],[72,14,43,30])).
% 181.00/181.21 cnf(2116,plain,
% 181.00/181.21 (P1(a11,a12,a2)+~P1(a11,a10,a7)),
% 181.00/181.21 inference(scs_inference,[],[9,14,18,30])).
% 181.00/181.21 cnf(2137,plain,
% 181.00/181.21 (~P1(a10,a7,a4)+P1(a4,a10,a4)),
% 181.00/181.21 inference(scs_inference,[],[510,22])).
% 181.00/181.21 cnf(2197,plain,
% 181.00/181.21 (P1(a4,a7,a11)+~P1(a11,a10,a1)),
% 181.00/181.21 inference(scs_inference,[],[3,10,14,17,18,30,26])).
% 181.00/181.21 cnf(2242,plain,
% 181.00/181.21 (~P2(a10,a9,a4)+P2(a7,a8,a8)),
% 181.00/181.21 inference(scs_inference,[],[548,24])).
% 181.00/181.21 cnf(2362,plain,
% 181.00/181.21 (~P2(x23621,a7,a10)+P2(a9,x23621,a4)),
% 181.00/181.21 inference(scs_inference,[],[572,24])).
% 181.00/181.21 cnf(2419,plain,
% 181.00/181.21 (~P2(x24191,a7,a4)+P2(a9,x24191,a4)),
% 181.00/181.21 inference(scs_inference,[],[586,24])).
% 181.00/181.21 cnf(2435,plain,
% 181.00/181.21 (~P2(a10,a7,a4)+P2(a4,a7,a4)),
% 181.00/181.21 inference(scs_inference,[],[17,11,14,589,31])).
% 181.00/181.21 cnf(2461,plain,
% 181.00/181.21 (~P1(a7,a9,x24611)+P1(x24611,a7,a7)),
% 181.00/181.21 inference(scs_inference,[],[454,19,26])).
% 181.00/181.21 cnf(2473,plain,
% 181.00/181.21 (~P1(a11,a9,x24731)+P1(x24731,a7,a7)),
% 181.00/181.21 inference(scs_inference,[],[454,17,26])).
% 181.00/181.21 cnf(2652,plain,
% 181.00/181.21 (P2(a4,a9,a4)+~P1(a4,a10,a7)),
% 181.00/181.21 inference(scs_inference,[],[619,25])).
% 181.00/181.21 cnf(2730,plain,
% 181.00/181.21 (P1(a7,a2,x27301)+~P1(a7,a11,x27301)),
% 181.00/181.21 inference(scs_inference,[],[1373,15,27])).
% 181.00/181.21 cnf(2749,plain,
% 181.00/181.21 (~P1(x27491,a12,a9)+P1(a10,x27491,a9)),
% 181.00/181.21 inference(scs_inference,[],[645,22])).
% 181.00/181.21 cnf(2813,plain,
% 181.00/181.21 (P1(a10,a9,a9)+~P2(a12,a10,a9)),
% 181.00/181.21 inference(scs_inference,[],[20,11,673,30])).
% 181.00/181.21 cnf(2878,plain,
% 181.00/181.21 (~P1(a11,a1,x28781)+P1(x28781,a3,a3)),
% 181.00/181.21 inference(scs_inference,[],[1376,17,26])).
% 181.00/181.21 cnf(3021,plain,
% 181.00/181.21 (~P1(a6,a1,a10)+P1(a10,a10,a6)),
% 181.00/181.21 inference(scs_inference,[],[1380,19,26,1160])).
% 181.00/181.21 cnf(3028,plain,
% 181.00/181.21 (~P1(a11,a1,x30281)+P1(x30281,a6,a6)),
% 181.00/181.21 inference(scs_inference,[],[1380,17,26])).
% 181.00/181.21 cnf(3069,plain,
% 181.00/181.21 (~P2(a10,a7,a12)+P2(a12,a7,a12)),
% 181.00/181.21 inference(scs_inference,[],[752,141])).
% 181.00/181.21 cnf(3070,plain,
% 181.00/181.21 (~P1(a11,a9,x30701)+P1(x30701,a12,a10)),
% 181.00/181.21 inference(scs_inference,[],[4,17,26])).
% 181.00/181.21 cnf(3104,plain,
% 181.00/181.21 (P1(a8,a2,x31041)+~P1(a8,a11,x31041)),
% 181.00/181.21 inference(scs_inference,[],[1388,15,27])).
% 181.00/181.21 cnf(3125,plain,
% 181.00/181.21 (P2(a12,a11,a2)+~P2(a2,a3,a11)),
% 181.00/181.21 inference(scs_inference,[],[1401,231,12,28,29])).
% 181.00/181.21 cnf(3133,plain,
% 181.00/181.21 (P1(a9,a2,a10)+~P1(a12,a9,a2)),
% 181.00/181.21 inference(scs_inference,[],[1401,4,7,20,13,30,27])).
% 181.00/181.21 cnf(3188,plain,
% 181.00/181.21 (~P2(x31881,a4,a10)+P2(a5,x31881,a12)),
% 181.00/181.21 inference(scs_inference,[],[814,24])).
% 181.00/181.21 cnf(3198,plain,
% 181.00/181.21 (P2(a12,a9,a12)+~P2(a9,a10,a10)),
% 181.00/181.21 inference(scs_inference,[],[817,542])).
% 181.00/181.21 cnf(3199,plain,
% 181.00/181.21 (~P1(a11,a8,x31991)+P1(x31991,a12,a10)),
% 181.00/181.21 inference(scs_inference,[],[1574,17,26])).
% 181.00/181.21 cnf(3209,plain,
% 181.00/181.21 (~P1(a10,a8,x32091)+P1(x32091,a12,a10)),
% 181.00/181.21 inference(scs_inference,[],[1574,13,26])).
% 181.00/181.21 cnf(3252,plain,
% 181.00/181.21 (~P2(a10,a4,a11)+P2(a12,a4,a11)),
% 181.00/181.21 inference(scs_inference,[],[838,24])).
% 181.00/181.21 cnf(3266,plain,
% 181.00/181.21 (~P1(a11,a1,x32661)+P1(x32661,a5,a6)),
% 181.00/181.21 inference(scs_inference,[],[2,17,26])).
% 181.00/181.21 cnf(3287,plain,
% 181.00/181.21 (~P1(a9,a12,a4)+P1(a9,a5,a10)),
% 181.00/181.21 inference(scs_inference,[],[848,22])).
% 181.00/181.21 cnf(3288,plain,
% 181.00/181.21 (~P1(a12,a12,a4)+P2(a12,a5,a12)),
% 181.00/181.21 inference(scs_inference,[],[857,25])).
% 181.00/181.21 cnf(3290,plain,
% 181.00/181.21 (~P1(a11,a8,x32901)+P1(x32901,a1,a10)),
% 181.00/181.21 inference(scs_inference,[],[5,17,26])).
% 181.00/181.21 cnf(3311,plain,
% 181.00/181.21 (~P2(a5,a3,a11)),
% 181.00/181.21 inference(scs_inference,[],[1,879,25])).
% 181.00/181.21 cnf(3312,plain,
% 181.00/181.21 (~P2(a3,a5,a11)),
% 181.00/181.21 inference(scs_inference,[],[3311,24])).
% 181.00/181.21 cnf(3314,plain,
% 181.00/181.21 (~P2(a4,a3,a11)),
% 181.00/181.21 inference(scs_inference,[],[8,12,3311,24,28])).
% 181.00/181.21 cnf(3317,plain,
% 181.00/181.21 (~P2(a3,a12,a11)),
% 181.00/181.21 inference(scs_inference,[],[8,12,14,3311,24,28,29])).
% 181.00/181.21 cnf(3330,plain,
% 181.00/181.21 (~P2(a10,a5,a11)),
% 181.00/181.21 inference(scs_inference,[],[16,12,3312,3314,24,28])).
% 181.00/181.21 cnf(3332,plain,
% 181.00/181.21 (P2(x33321,a10,x33321)),
% 181.00/181.21 inference(rename_variables,[],[16])).
% 181.00/181.21 cnf(3334,plain,
% 181.00/181.21 (~P1(a11,a11,a5)),
% 181.00/181.21 inference(scs_inference,[],[16,3332,12,19,3312,3314,24,28,31])).
% 181.00/181.21 cnf(3340,plain,
% 181.00/181.21 (~P1(a9,a11,a10)),
% 181.00/181.21 inference(scs_inference,[],[16,3332,12,19,3312,3314,24,28,31,1325,22])).
% 181.00/181.21 cnf(3355,plain,
% 181.00/181.21 (~P1(a11,a11,a4)),
% 181.00/181.21 inference(scs_inference,[],[3334,875])).
% 181.00/181.21 cnf(3356,plain,
% 181.00/181.21 (~P1(a11,a9,a4)),
% 181.00/181.21 inference(scs_inference,[],[3334,2098])).
% 181.00/181.21 cnf(3360,plain,
% 181.00/181.21 (~P1(a9,a11,a4)),
% 181.00/181.21 inference(scs_inference,[],[3356,22])).
% 181.00/181.21 cnf(3362,plain,
% 181.00/181.21 (~P2(a12,a3,a11)),
% 181.00/181.21 inference(scs_inference,[],[3356,3317,22,24])).
% 181.00/181.21 cnf(3364,plain,
% 181.00/181.21 (~P2(a9,a12,a3)),
% 181.00/181.21 inference(scs_inference,[],[7,20,3356,3317,22,24,28])).
% 181.00/181.21 cnf(3367,plain,
% 181.00/181.21 (~P1(a9,a12,a9)),
% 181.00/181.21 inference(scs_inference,[],[7,4,3340,20,15,3356,3317,22,24,28,26])).
% 181.00/181.21 cnf(3370,plain,
% 181.00/181.21 (~P2(a12,a4,a11)),
% 181.00/181.21 inference(scs_inference,[],[7,4,8,3340,20,18,15,3356,3317,3330,22,24,28,26,29])).
% 181.00/181.21 cnf(3373,plain,
% 181.00/181.21 (~P1(a11,a9,a3)),
% 181.00/181.21 inference(scs_inference,[],[7,4,8,3340,20,18,19,14,15,3356,3317,3330,22,24,28,26,29,31])).
% 181.00/181.21 cnf(3377,plain,
% 181.00/181.21 (~P2(a9,x33771,a12)),
% 181.00/181.21 inference(scs_inference,[],[7,4,8,3340,20,18,19,14,15,3356,3317,3330,22,24,28,26,29,31,23])).
% 181.00/181.21 cnf(3379,plain,
% 181.00/181.21 (~P2(a4,a10,a11)),
% 181.00/181.21 inference(scs_inference,[],[7,4,8,3340,20,18,19,14,15,3356,3317,3330,22,24,28,26,29,31,23,838])).
% 181.00/181.21 cnf(3393,plain,
% 181.00/181.21 (~P2(a10,a4,a11)),
% 181.00/181.21 inference(scs_inference,[],[3370,3252])).
% 181.00/181.21 cnf(3398,plain,
% 181.00/181.21 (~P2(a9,a12,a4)),
% 181.00/181.21 inference(scs_inference,[],[7,3367,16,3379,3364,22,24,28])).
% 181.00/181.21 cnf(3399,plain,
% 181.00/181.21 (P2(x33991,a10,x33991)),
% 181.00/181.21 inference(rename_variables,[],[16])).
% 181.00/181.21 cnf(3403,plain,
% 181.00/181.21 (~P1(a8,a1,a9)),
% 181.00/181.21 inference(scs_inference,[],[7,5,3340,334,3367,16,15,59,3379,3364,22,24,28,27,26])).
% 181.00/181.21 cnf(3407,plain,
% 181.00/181.21 (~P2(a9,x34071,a12)),
% 181.00/181.21 inference(rename_variables,[],[3377])).
% 181.00/181.21 cnf(3415,plain,
% 181.00/181.21 (~P2(a7,a5,a3)),
% 181.00/181.21 inference(scs_inference,[],[7,9,5,3340,334,3367,16,20,19,15,59,3379,3364,3377,3407,22,24,28,27,26,29,31,556])).
% 181.00/181.21 cnf(3417,plain,
% 181.00/181.21 (~P2(a12,a7,a10)),
% 181.00/181.21 inference(scs_inference,[],[7,9,5,3340,334,3367,16,20,19,15,59,3379,3364,3377,3407,22,24,28,27,26,29,31,556,2362])).
% 181.00/181.21 cnf(3419,plain,
% 181.00/181.21 (~P2(a12,a7,a4)),
% 181.00/181.21 inference(scs_inference,[],[7,9,5,3340,334,3367,16,20,19,15,59,3379,3364,3377,3407,22,24,28,27,26,29,31,556,2362,2419])).
% 181.00/181.21 cnf(3423,plain,
% 181.00/181.21 (~P2(a12,a11,a12)),
% 181.00/181.21 inference(scs_inference,[],[7,9,5,3340,334,3367,16,3399,20,12,19,11,15,59,3379,3364,3377,3407,22,24,28,27,26,29,31,556,2362,2419,639,30])).
% 181.00/181.21 cnf(3433,plain,
% 181.00/181.21 (~P1(a12,x34331,a11)),
% 181.00/181.21 inference(scs_inference,[],[7,9,5,3340,334,3367,16,3399,20,12,19,11,15,59,3379,3364,3377,3407,22,24,28,27,26,29,31,556,2362,2419,639,30,131,828,1002,1032,25])).
% 181.00/181.21 cnf(3436,plain,
% 181.00/181.21 (~P2(a7,a2,a4)),
% 181.00/181.21 inference(scs_inference,[],[3419,1002])).
% 181.00/181.21 cnf(3438,plain,
% 181.00/181.21 (~P1(x34381,a12,a11)),
% 181.00/181.21 inference(scs_inference,[],[3433,3419,1002,22])).
% 181.00/181.21 cnf(3445,plain,
% 181.00/181.21 (~P1(a10,x34451,a11)),
% 181.00/181.21 inference(scs_inference,[],[8,3423,3433,14,11,13,3393,3419,1002,22,24,28,27])).
% 181.00/181.21 cnf(3449,plain,
% 181.00/181.21 (~P1(a8,a3,a9)),
% 181.00/181.21 inference(scs_inference,[],[8,3340,37,3423,3433,14,11,15,13,3393,3419,1002,22,24,28,27,26])).
% 181.00/181.21 cnf(3452,plain,
% 181.00/181.21 (~P2(a12,a9,a12)),
% 181.00/181.21 inference(scs_inference,[],[7,8,3340,37,3423,3433,20,14,11,15,13,3393,3419,1002,22,24,28,27,26,29])).
% 181.00/181.21 cnf(3456,plain,
% 181.00/181.21 (~P2(a7,a5,a12)),
% 181.00/181.21 inference(scs_inference,[],[7,8,3340,37,3423,3433,20,14,11,15,13,3393,3419,1002,22,24,28,27,26,29,817,556])).
% 181.00/181.21 cnf(3469,plain,
% 181.00/181.21 (~P2(a9,a10,a10)),
% 181.00/181.21 inference(scs_inference,[],[3452,3198])).
% 181.00/181.21 cnf(3477,plain,
% 181.00/181.21 (~P2(a10,a3,a11)),
% 181.00/181.21 inference(scs_inference,[],[3438,3403,16,12,3398,3362,23,22,24,28])).
% 181.00/181.21 cnf(3478,plain,
% 181.00/181.21 (P2(x34781,a11,a11)),
% 181.00/181.21 inference(rename_variables,[],[12])).
% 181.00/181.21 cnf(3479,plain,
% 181.00/181.21 (P2(x34791,a10,x34791)),
% 181.00/181.21 inference(rename_variables,[],[16])).
% 181.00/181.21 cnf(3481,plain,
% 181.00/181.21 (~P1(a8,a6,a9)),
% 181.00/181.21 inference(scs_inference,[],[3438,3340,53,3403,16,12,15,3398,3362,23,22,24,28,26])).
% 181.00/181.21 cnf(3485,plain,
% 181.00/181.21 (P2(x34851,a11,a11)),
% 181.00/181.21 inference(rename_variables,[],[12])).
% 181.00/181.21 cnf(3487,plain,
% 181.00/181.21 (~P2(a10,a11,a10)),
% 181.00/181.21 inference(scs_inference,[],[9,3438,3340,53,3423,3403,3445,16,3479,12,3478,3485,19,15,3398,3362,23,22,24,28,26,29,30])).
% 181.00/181.21 cnf(3489,plain,
% 181.00/181.21 (P2(x34891,a10,x34891)),
% 181.00/181.21 inference(rename_variables,[],[16])).
% 181.00/181.21 cnf(3491,plain,
% 181.00/181.21 (P1(x34911,x34911,x34911)),
% 181.00/181.21 inference(rename_variables,[],[19])).
% 181.00/181.21 cnf(3493,plain,
% 181.00/181.21 (~P1(a11,a11,a3)),
% 181.00/181.21 inference(scs_inference,[],[9,3438,3340,53,3423,3403,3445,16,3479,3489,12,3478,3485,19,3491,15,3398,3362,23,22,24,28,26,29,30,31])).
% 181.00/181.21 cnf(3500,plain,
% 181.00/181.21 (~P2(a7,a5,a4)),
% 181.00/181.21 inference(scs_inference,[],[9,3438,3340,53,3423,3403,3445,16,3479,3489,12,3478,3485,19,3491,15,3398,3362,23,22,24,28,26,29,30,31,457,556])).
% 181.00/181.21 cnf(3528,plain,
% 181.00/181.21 (~P1(a10,x35281,a9)),
% 181.00/181.21 inference(scs_inference,[],[6,8,5,1,3340,1574,3487,3449,20,15,13,3452,3469,22,24,27,26,29,31,2749,3188,25])).
% 181.00/181.21 cnf(3532,plain,
% 181.00/181.21 (~P2(a12,a10,a9)),
% 181.00/181.21 inference(scs_inference,[],[6,10,8,5,1,3340,1574,3487,3449,20,15,13,3452,3370,3469,22,24,27,26,29,31,2749,3188,25,28,2813])).
% 181.00/181.21 cnf(3543,plain,
% 181.00/181.21 (~P2(a4,a7,a12)),
% 181.00/181.21 inference(scs_inference,[],[6,3481,3528,16,3417,3532,2749,22,24,28])).
% 181.00/181.21 cnf(3563,plain,
% 181.00/181.21 (~P1(x35631,a10,a11)),
% 181.00/181.21 inference(scs_inference,[],[3445,22])).
% 181.00/181.21 cnf(3565,plain,
% 181.00/181.21 (~P2(a7,a12,a4)),
% 181.00/181.21 inference(scs_inference,[],[3445,3419,22,24])).
% 181.00/181.21 cnf(3586,plain,
% 181.00/181.21 (~P1(a9,a11,a3)),
% 181.00/181.21 inference(scs_inference,[],[3373,22])).
% 181.00/181.21 cnf(3590,plain,
% 181.00/181.21 (~P1(a8,a1,a11)),
% 181.00/181.21 inference(scs_inference,[],[5,3563,450,3377,3373,22,24,27])).
% 181.00/181.21 cnf(3593,plain,
% 181.00/181.21 (~P1(a1,a2,a11)),
% 181.00/181.21 inference(scs_inference,[],[5,1,3563,450,15,3377,3493,3373,22,24,27,26])).
% 181.00/181.21 cnf(3605,plain,
% 181.00/181.21 (~P2(a4,a12,a11)),
% 181.00/181.21 inference(scs_inference,[],[3590,3370,22,24])).
% 181.00/181.21 cnf(3610,plain,
% 181.00/181.21 (~P1(a1,a2,a9)),
% 181.00/181.21 inference(scs_inference,[],[1,3586,3563,37,450,3590,15,3370,22,24,27,26])).
% 181.00/181.21 cnf(3622,plain,
% 181.00/181.21 (~P2(a5,a10,a11)),
% 181.00/181.21 inference(scs_inference,[],[3593,3330,22,24])).
% 181.00/181.21 cnf(3627,plain,
% 181.00/181.21 (~P1(a3,a2,a9)),
% 181.00/181.21 inference(scs_inference,[],[3586,3563,53,34,450,3593,15,3330,22,24,27,26])).
% 181.00/181.21 cnf(3659,plain,
% 181.00/181.21 (~P2(a3,a10,a11)),
% 181.00/181.21 inference(scs_inference,[],[3610,3477,22,24])).
% 181.00/181.21 cnf(3661,plain,
% 181.00/181.21 (~P2(a8,a1,a10)),
% 181.00/181.21 inference(scs_inference,[],[10,3487,3610,18,3477,22,24,29])).
% 181.00/181.21 cnf(3671,plain,
% 181.00/181.21 (~P1(a2,a3,a9)),
% 181.00/181.21 inference(scs_inference,[],[3627,22])).
% 181.00/181.21 cnf(3745,plain,
% 181.00/181.21 (~P2(a12,a5,a11)),
% 181.00/181.21 inference(scs_inference,[],[18,1417,3330,3661,24,29])).
% 181.00/181.21 cnf(3775,plain,
% 181.00/181.21 (~P2(a5,a12,a11)),
% 181.00/181.21 inference(scs_inference,[],[3745,24])).
% 181.00/181.21 cnf(3791,plain,
% 181.00/181.21 (~P2(a5,a4,a11)),
% 181.00/181.21 inference(scs_inference,[],[18,72,3330,3543,24,29])).
% 181.00/181.21 cnf(3805,plain,
% 181.00/181.21 (~P1(a11,a1,a6)),
% 181.00/181.21 inference(scs_inference,[],[1,900,25])).
% 181.00/181.21 cnf(3806,plain,
% 181.00/181.21 (~P1(a1,a11,a6)),
% 181.00/181.21 inference(scs_inference,[],[3805,22])).
% 181.00/181.21 cnf(3823,plain,
% 181.00/181.21 (~P1(a5,a9,a11)),
% 181.00/181.21 inference(scs_inference,[],[2,3806,15,3791,24,26,1062])).
% 181.00/181.21 cnf(3824,plain,
% 181.00/181.21 (~P2(a1,x38241,a5)),
% 181.00/181.21 inference(scs_inference,[],[2,3806,15,3791,24,26,1062,23])).
% 181.00/181.21 cnf(3830,plain,
% 181.00/181.21 (~P2(a12,a4,a1)),
% 181.00/181.21 inference(scs_inference,[],[2,8,3671,3806,1376,16,15,3791,24,26,1062,23,22,27,28])).
% 181.00/181.21 cnf(3842,plain,
% 181.00/181.21 (~P2(x38421,a1,a5)),
% 181.00/181.21 inference(scs_inference,[],[3823,3824,22,24])).
% 181.00/181.21 cnf(3855,plain,
% 181.00/181.21 (~P1(a5,x38551,a1)),
% 181.00/181.22 inference(scs_inference,[],[3806,101,20,1417,19,15,3823,3824,22,24,28,26,31,25])).
% 181.00/181.22 cnf(3865,plain,
% 181.00/181.22 (~P1(x38651,a5,a1)),
% 181.00/181.22 inference(scs_inference,[],[3855,22])).
% 181.00/181.22 cnf(3872,plain,
% 181.00/181.22 (~P1(a1,a6,a1)),
% 181.00/181.22 inference(scs_inference,[],[8,3806,1380,3855,15,3830,3842,22,24,28,26])).
% 181.00/181.22 cnf(3877,plain,
% 181.00/181.22 (~P2(a1,x38771,a6)),
% 181.00/181.22 inference(scs_inference,[],[8,3806,1380,3855,15,3830,3842,22,24,28,26,458,23])).
% 181.00/181.22 cnf(3879,plain,
% 181.00/181.22 (~P1(a4,x38791,a1)),
% 181.00/181.22 inference(scs_inference,[],[8,3806,1380,3855,15,3830,3842,22,24,28,26,458,23,25])).
% 181.00/181.22 cnf(3902,plain,
% 181.00/181.22 (~P1(a6,x39021,a1)),
% 181.00/181.22 inference(scs_inference,[],[3872,3877,22,24,25])).
% 181.00/181.22 cnf(3913,plain,
% 181.00/181.22 (~P1(x39131,a4,a1)),
% 181.00/181.22 inference(scs_inference,[],[3879,22])).
% 181.00/181.22 cnf(3942,plain,
% 181.00/181.22 (~P1(x39421,a6,a1)),
% 181.00/181.22 inference(scs_inference,[],[3902,22])).
% 181.00/181.22 cnf(4157,plain,
% 181.00/181.22 (~P1(a1,a5,a11)+~P1(a1,x41571,a11)),
% 181.00/181.22 inference(scs_inference,[],[2,15,905,26])).
% 181.00/181.22 cnf(4158,plain,
% 181.00/181.22 (~P1(a1,a5,a11)),
% 181.00/181.22 inference(factoring_inference,[],[4157])).
% 181.00/181.22 cnf(4167,plain,
% 181.00/181.22 (~P2(x41671,a11,a5)),
% 181.00/181.22 inference(scs_inference,[],[3865,4158,15,22,26,23,24])).
% 181.00/181.22 cnf(4254,plain,
% 181.00/181.22 (~P2(a11,x42541,a4)),
% 181.00/181.22 inference(scs_inference,[],[3913,15,26,1997,23])).
% 181.00/181.22 cnf(4265,plain,
% 181.00/181.22 (~P1(a11,a10,a1)),
% 181.00/181.22 inference(scs_inference,[],[6,3913,20,15,3436,26,1997,23,25,24,22,31,2197])).
% 181.00/181.22 cnf(4269,plain,
% 181.00/181.22 (P1(x42691,a11,x42691)),
% 181.00/181.22 inference(rename_variables,[],[15])).
% 181.00/181.22 cnf(4272,plain,
% 181.00/181.22 (~P2(a11,x42721,a6)),
% 181.00/181.22 inference(scs_inference,[],[3942,15,4265,22,26,23])).
% 181.00/181.22 cnf(4279,plain,
% 181.00/181.22 (~P1(a6,x42791,a11)),
% 181.00/181.22 inference(scs_inference,[],[7,3942,15,4269,3532,4265,22,26,23,24,31,25])).
% 181.00/181.22 cnf(4281,plain,
% 181.00/181.22 (~P1(x42811,a6,a11)),
% 181.00/181.22 inference(scs_inference,[],[4279,22])).
% 181.00/181.22 cnf(4380,plain,
% 181.00/181.22 (~P1(a2,a2,a4)),
% 181.00/181.22 inference(scs_inference,[],[9,334,1390,3565,31])).
% 181.00/181.22 cnf(4555,plain,
% 181.00/181.22 (~P2(a7,a5,a5)),
% 181.00/181.22 inference(scs_inference,[],[7,16,15,3622,28,24,31,556])).
% 181.00/181.22 cnf(4567,plain,
% 181.00/181.22 (~P2(a8,a1,a3)),
% 181.00/181.22 inference(scs_inference,[],[10,16,3659,4555,24,28])).
% 181.00/181.22 cnf(4577,plain,
% 181.00/181.22 (~P1(x45771,a5,a7)),
% 181.00/181.22 inference(scs_inference,[],[10,16,20,19,3659,4555,24,28,31,25,22])).
% 181.00/181.22 cnf(4581,plain,
% 181.00/181.22 (~P1(a7,a9,a5)),
% 181.00/181.22 inference(scs_inference,[],[10,1373,16,20,19,3659,4555,24,28,31,25,22,26,2461])).
% 181.00/181.22 cnf(4583,plain,
% 181.00/181.22 (~P2(a7,x45831,a5)),
% 181.00/181.22 inference(scs_inference,[],[10,1373,16,20,19,3659,4555,24,28,31,25,22,26,2461,23])).
% 181.00/181.22 cnf(4587,plain,
% 181.00/181.22 (~P1(a9,a7,a5)),
% 181.00/181.22 inference(scs_inference,[],[4581,4567,24,22])).
% 181.00/181.22 cnf(4592,plain,
% 181.00/181.22 (~P1(a2,a5,a2)),
% 181.00/181.22 inference(scs_inference,[],[4577,1373,4581,16,56,3622,4567,24,22,28,26])).
% 181.00/181.22 cnf(4595,plain,
% 181.00/181.22 (~P2(a2,x45951,a5)),
% 181.00/181.22 inference(scs_inference,[],[4577,1373,4581,16,56,3622,4567,24,22,28,26,23])).
% 181.00/181.22 cnf(4601,plain,
% 181.00/181.22 (~P2(x46011,a2,a5)),
% 181.00/181.22 inference(scs_inference,[],[4595,24])).
% 181.00/181.22 cnf(4605,plain,
% 181.00/181.22 (~P1(a7,a2,a5)),
% 181.00/181.22 inference(scs_inference,[],[4587,454,1373,4592,4595,24,22,27])).
% 181.00/181.22 cnf(4609,plain,
% 181.00/181.22 (P2(x46091,a10,x46091)),
% 181.00/181.22 inference(rename_variables,[],[16])).
% 181.00/181.22 cnf(4616,plain,
% 181.00/181.22 (~P1(a5,x46161,a2)),
% 181.00/181.22 inference(scs_inference,[],[4587,454,1373,4592,16,4609,15,12,3659,4595,24,22,27,28,31,25])).
% 181.00/181.22 cnf(4618,plain,
% 181.00/181.22 (~P2(x46181,a7,a5)),
% 181.00/181.22 inference(scs_inference,[],[4583,24])).
% 181.00/181.22 cnf(4622,plain,
% 181.00/181.22 (~P1(a9,a2,a5)),
% 181.00/181.22 inference(scs_inference,[],[4587,4605,19,59,4583,24,22,27])).
% 181.00/181.22 cnf(4625,plain,
% 181.00/181.22 (~P2(a9,a5,a5)),
% 181.00/181.22 inference(scs_inference,[],[4587,4605,16,19,43,59,3622,4583,24,22,27,28])).
% 181.00/181.22 cnf(4628,plain,
% 181.00/181.22 (~P1(a9,a9,a5)),
% 181.00/181.22 inference(scs_inference,[],[4587,4605,16,20,19,43,59,3622,4583,24,22,27,28,31])).
% 181.00/181.22 cnf(4634,plain,
% 181.00/181.22 (~P1(x46341,a5,a2)),
% 181.00/181.22 inference(scs_inference,[],[4616,4625,24,22])).
% 181.00/181.22 cnf(4636,plain,
% 181.00/181.22 (~P2(a11,x46361,a3)),
% 181.00/181.22 inference(scs_inference,[],[4616,16,14,3659,4625,24,22,28])).
% 181.00/181.22 cnf(4644,plain,
% 181.00/181.22 (~P1(a5,x46441,a9)),
% 181.00/181.22 inference(scs_inference,[],[4616,16,20,19,14,3659,4625,24,22,28,31,25])).
% 181.00/181.22 cnf(4657,plain,
% 181.00/181.22 (~P1(x46571,a5,a9)),
% 181.00/181.22 inference(scs_inference,[],[4644,4636,24,22])).
% 181.00/181.22 cnf(4679,plain,
% 181.00/181.22 (~P2(a9,x46791,a5)),
% 181.00/181.22 inference(scs_inference,[],[4657,23])).
% 181.00/181.22 cnf(4682,plain,
% 181.00/181.22 (~P2(x46821,a9,a5)),
% 181.00/181.22 inference(scs_inference,[],[4657,23,24])).
% 181.00/181.22 cnf(4698,plain,
% 181.00/181.22 (~P1(a2,a9,a5)),
% 181.00/181.22 inference(scs_inference,[],[4622,22])).
% 181.00/181.22 cnf(4706,plain,
% 181.00/181.22 (~P2(a10,a1,a3)),
% 181.00/181.22 inference(scs_inference,[],[2,946,25])).
% 181.00/181.22 cnf(4726,plain,
% 181.00/181.22 (~P1(a11,a11,a6)),
% 181.00/181.22 inference(scs_inference,[],[3806,1380,15,26])).
% 181.00/181.22 cnf(4770,plain,
% 181.00/181.22 (~P2(a1,x47701,a2)+~P2(a1,a10,a1)),
% 181.00/181.22 inference(scs_inference,[],[1,16,4706,31,1074,23])).
% 181.00/181.22 cnf(4772,plain,
% 181.00/181.22 (~P2(x47721,a1,a2)+~P2(a1,a10,a1)),
% 181.00/181.22 inference(scs_inference,[],[1,16,4706,31,1074,23,24])).
% 181.00/181.22 cnf(4784,plain,
% 181.00/181.22 (~P2(a1,x47841,a2)),
% 181.00/181.22 inference(scs_inference,[],[16,4770])).
% 181.00/181.22 cnf(4785,plain,
% 181.00/181.22 (~P2(x47851,a1,a2)),
% 181.00/181.22 inference(scs_inference,[],[16,4772])).
% 181.00/181.22 cnf(4788,plain,
% 181.00/181.22 (~P1(a11,a9,a7)),
% 181.00/181.22 inference(scs_inference,[],[4784,1318])).
% 181.00/181.22 cnf(4790,plain,
% 181.00/181.22 (~P1(a11,a4,a10)),
% 181.00/181.22 inference(scs_inference,[],[4788,1300])).
% 181.00/181.22 cnf(4791,plain,
% 181.00/181.22 (~P1(a2,x47911,a1)),
% 181.00/181.22 inference(scs_inference,[],[4785,25])).
% 181.00/181.22 cnf(4794,plain,
% 181.00/181.22 (~P1(a9,a11,a7)),
% 181.00/181.22 inference(scs_inference,[],[4788,4785,25,22])).
% 181.00/181.22 cnf(4800,plain,
% 181.00/181.22 (~P2(a7,a7,a11)),
% 181.00/181.22 inference(scs_inference,[],[9,16,4788,4784,4785,25,22,28,1080])).
% 181.00/181.22 cnf(4801,plain,
% 181.00/181.22 (~P2(a7,a2,a1)),
% 181.00/181.22 inference(scs_inference,[],[9,16,4788,4784,4785,25,22,28,1080,1002])).
% 181.00/181.22 cnf(4811,plain,
% 181.00/181.22 (~P1(x48111,a2,a1)),
% 181.00/181.22 inference(scs_inference,[],[4791,4801,24,22])).
% 181.00/181.22 cnf(4813,plain,
% 181.00/181.22 (~P2(a2,a3,a1)),
% 181.00/181.22 inference(scs_inference,[],[231,4791,16,4801,4784,24,22,28])).
% 181.00/181.22 cnf(4826,plain,
% 181.00/181.22 (~P1(a4,a11,a10)),
% 181.00/181.22 inference(scs_inference,[],[4790,4813,24,22])).
% 181.00/181.22 cnf(4828,plain,
% 181.00/181.22 (~P2(a7,a1,a7)),
% 181.00/181.22 inference(scs_inference,[],[9,4785,4790,4813,24,22,28])).
% 181.00/181.22 cnf(4831,plain,
% 181.00/181.22 (~P1(a7,x48311,a1)),
% 181.00/181.22 inference(scs_inference,[],[9,4785,4790,4813,24,22,28,25])).
% 181.00/181.22 cnf(4837,plain,
% 181.00/181.22 (~P2(a3,a1,a3)),
% 181.00/181.22 inference(scs_inference,[],[231,4831,4785,4828,24,22,28])).
% 181.00/181.22 cnf(4840,plain,
% 181.00/181.22 (~P1(x48401,a2,a11)),
% 181.00/181.22 inference(scs_inference,[],[231,4831,4785,4828,24,22,28,1950])).
% 181.00/181.22 cnf(4846,plain,
% 181.00/181.22 (~P2(a11,x48461,a2)),
% 181.00/181.22 inference(scs_inference,[],[4840,23])).
% 181.00/181.22 cnf(4847,plain,
% 181.00/181.22 (~P1(x48471,a2,a11)),
% 181.00/181.22 inference(rename_variables,[],[4840])).
% 181.00/181.22 cnf(4851,plain,
% 181.00/181.22 (~P1(a2,x48511,a11)),
% 181.00/181.22 inference(scs_inference,[],[4840,4847,4837,23,24,22])).
% 181.00/181.22 cnf(4853,plain,
% 181.00/181.22 (~P2(a2,a11,a2)),
% 181.00/181.22 inference(scs_inference,[],[4840,4847,20,15,4837,23,24,22,31])).
% 181.00/181.22 cnf(4858,plain,
% 181.00/181.22 (~P1(a11,a9,a7)),
% 181.00/181.22 inference(scs_inference,[],[4846,1320])).
% 181.00/181.22 cnf(4879,plain,
% 181.00/181.22 (~P2(x48791,a11,a2)),
% 181.00/181.22 inference(scs_inference,[],[4846,24])).
% 181.00/181.22 cnf(4883,plain,
% 181.00/181.22 (~P2(a2,a3,a11)),
% 181.00/181.22 inference(scs_inference,[],[9,4853,4846,24,28,3125])).
% 181.00/181.22 cnf(4884,plain,
% 181.00/181.22 (~P1(a7,x48841,a11)),
% 181.00/181.22 inference(scs_inference,[],[9,4853,4846,24,28,3125,25])).
% 181.00/181.22 cnf(4892,plain,
% 181.00/181.22 (~P2(a3,a2,a11)),
% 181.00/181.22 inference(scs_inference,[],[4883,24])).
% 181.00/181.22 cnf(4938,plain,
% 181.00/181.22 (~P2(a7,a2,x49381)+~P2(x49381,a3,a4)),
% 181.00/181.22 inference(scs_inference,[],[231,3436,29])).
% 181.00/181.22 cnf(5026,plain,
% 181.00/181.22 (~P1(a11,a11,a7)),
% 181.00/181.22 inference(scs_inference,[],[14,15,4800,31])).
% 181.00/181.22 cnf(5032,plain,
% 181.00/181.22 (~P1(a11,a11,a2)),
% 181.00/181.22 inference(scs_inference,[],[14,15,4892,31])).
% 181.00/181.22 cnf(5037,plain,
% 181.00/181.22 (~P1(a11,a9,a7)),
% 181.00/181.22 inference(scs_inference,[],[5032,1315])).
% 181.00/181.22 cnf(5165,plain,
% 181.00/181.22 (~P2(a7,a12,x51651)+~P2(x51651,a4,a3)),
% 181.00/181.22 inference(scs_inference,[],[8,3415,29])).
% 181.00/181.22 cnf(5197,plain,
% 181.00/181.22 (~P2(a7,a12,x51971)+~P2(x51971,a5,a3)),
% 181.00/181.22 inference(scs_inference,[],[1417,3415,29])).
% 181.00/181.22 cnf(5308,plain,
% 181.00/181.22 (~P2(a4,a9,a4)+~P2(a4,a12,a5)),
% 181.00/181.22 inference(scs_inference,[],[14,15,43,3605,28,31])).
% 181.00/181.22 cnf(5314,plain,
% 181.00/181.22 (~P2(a4,a12,a5)+~P2(a4,a7,a4)),
% 181.00/181.22 inference(scs_inference,[],[14,15,43,3605,28,31,2652,2419])).
% 181.00/181.22 cnf(5316,plain,
% 181.00/181.22 (~P1(a4,x53161,a9)+~P2(a4,a12,a5)),
% 181.00/181.22 inference(scs_inference,[],[14,15,43,3605,28,31,2652,2419,25])).
% 181.00/181.22 cnf(5318,plain,
% 181.00/181.22 (~P2(a7,a4,a4)+~P2(a4,a12,a5)),
% 181.00/181.22 inference(scs_inference,[],[14,15,43,3605,28,31,2652,2419,25,24])).
% 181.00/181.22 cnf(5533,plain,
% 181.00/181.22 (~P1(a2,a11,a5)),
% 181.00/181.22 inference(scs_inference,[],[17,20,14,4595,31,22])).
% 181.00/181.22 cnf(5671,plain,
% 181.00/181.22 (~P1(a1,a11,a5)),
% 181.00/181.22 inference(scs_inference,[],[19,2,3806,26])).
% 181.00/181.22 cnf(5672,plain,
% 181.00/181.22 (P1(x56721,x56721,x56721)),
% 181.00/181.22 inference(rename_variables,[],[19])).
% 181.00/181.22 cnf(5674,plain,
% 181.00/181.22 (~P1(a2,a2,a5)),
% 181.00/181.22 inference(scs_inference,[],[19,5672,2,3806,20,4595,26,31])).
% 181.00/181.22 cnf(5680,plain,
% 181.00/181.22 (~P1(a11,a1,a5)),
% 181.00/181.22 inference(scs_inference,[],[19,5672,2,3806,20,4595,26,31,22])).
% 181.00/181.22 cnf(6043,plain,
% 181.00/181.22 (~P2(a4,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[8,16,4595,28,24])).
% 181.00/181.22 cnf(6045,plain,
% 181.00/181.22 (~P1(a2,a9,a4)+~P2(a2,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[7,8,16,15,4595,28,24,31])).
% 181.00/181.22 cnf(6048,plain,
% 181.00/181.22 (~P1(a9,a2,a4)+~P2(a2,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[7,8,16,15,4595,28,24,31,22])).
% 181.00/181.22 cnf(6072,plain,
% 181.00/181.22 (~P2(a6,a2,a11)),
% 181.00/181.22 inference(scs_inference,[],[2,1540,25])).
% 181.00/181.22 cnf(6073,plain,
% 181.00/181.22 (~P2(a2,a6,a11)),
% 181.00/181.22 inference(scs_inference,[],[6072,24])).
% 181.00/181.22 cnf(6081,plain,
% 181.00/181.22 (~P1(a9,a2,a12)+~P2(a2,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[7,15,1417,4595,6072,24,28,31,22])).
% 181.00/181.22 cnf(6102,plain,
% 181.00/181.22 (~P2(a7,a5,a7)),
% 181.00/181.22 inference(scs_inference,[],[7,9,15,56,4800,28,24,31,556])).
% 181.00/181.22 cnf(6104,plain,
% 181.00/181.22 (~P1(a7,x61041,a5)),
% 181.00/181.22 inference(scs_inference,[],[7,9,15,56,4800,28,24,31,556,25])).
% 181.00/181.22 cnf(6113,plain,
% 181.00/181.22 (~P1(x61131,a7,a5)),
% 181.00/181.22 inference(scs_inference,[],[6104,6102,24,22])).
% 181.00/181.22 cnf(6115,plain,
% 181.00/181.22 (~P2(a5,x61151,a7)),
% 181.00/181.22 inference(scs_inference,[],[6104,6102,24,22,23])).
% 181.00/181.22 cnf(6130,plain,
% 181.00/181.22 (~P2(x61301,a5,a7)),
% 181.00/181.22 inference(scs_inference,[],[6115,24])).
% 181.00/181.22 cnf(6143,plain,
% 181.00/181.22 (~P2(a2,a6,a1)),
% 181.00/181.22 inference(scs_inference,[],[2,1546,25])).
% 181.00/181.22 cnf(6149,plain,
% 181.00/181.22 (~P2(a2,a9,a2)),
% 181.00/181.22 inference(scs_inference,[],[56,4851,15,18,14,4892,6143,24,28,30])).
% 181.00/181.22 cnf(6150,plain,
% 181.00/181.22 (P2(a11,x61501,a11)),
% 181.00/181.22 inference(rename_variables,[],[14])).
% 181.00/181.22 cnf(6152,plain,
% 181.00/181.22 (P1(x61521,a11,x61521)),
% 181.00/181.22 inference(rename_variables,[],[15])).
% 181.00/181.22 cnf(6154,plain,
% 181.00/181.22 (~P1(a11,a9,a6)),
% 181.00/181.22 inference(scs_inference,[],[56,4851,15,6152,18,14,6150,4892,6073,6143,24,28,30,31])).
% 181.00/181.22 cnf(6158,plain,
% 181.00/181.22 (~P1(a2,x61581,a9)),
% 181.00/181.22 inference(scs_inference,[],[56,4851,15,6152,18,14,6150,4892,6073,6143,24,28,30,31,25])).
% 181.00/181.22 cnf(6165,plain,
% 181.00/181.22 (~P1(x61651,a2,a9)),
% 181.00/181.22 inference(scs_inference,[],[6149,6158,24,22])).
% 181.00/181.22 cnf(6169,plain,
% 181.00/181.22 (~P2(x61691,a9,a3)),
% 181.00/181.22 inference(scs_inference,[],[56,6,9,6149,6158,12,4892,24,22,29,28])).
% 181.00/181.22 cnf(6171,plain,
% 181.00/181.22 (~P1(a9,a9,a2)),
% 181.00/181.22 inference(scs_inference,[],[56,6,9,6149,6158,20,12,4892,24,22,29,28,31])).
% 181.00/181.22 cnf(6175,plain,
% 181.00/181.22 (~P2(a9,x61751,a2)),
% 181.00/181.22 inference(scs_inference,[],[56,6,9,6149,6158,20,12,4892,24,22,29,28,31,23])).
% 181.00/181.22 cnf(6177,plain,
% 181.00/181.22 (~P1(a3,x61771,a9)),
% 181.00/181.22 inference(scs_inference,[],[56,6,9,6149,6158,20,12,4892,24,22,29,28,31,23,25])).
% 181.00/181.22 cnf(6180,plain,
% 181.00/181.22 (~P2(a9,x61801,a3)),
% 181.00/181.22 inference(scs_inference,[],[6169,24])).
% 181.00/181.22 cnf(6184,plain,
% 181.00/181.22 (~P1(a11,a9,a2)),
% 181.00/181.22 inference(scs_inference,[],[6177,20,14,17,6169,6175,24,22,31])).
% 181.00/181.22 cnf(6200,plain,
% 181.00/181.22 (~P2(x62001,a9,a2)),
% 181.00/181.22 inference(scs_inference,[],[6175,24])).
% 181.00/181.22 cnf(6204,plain,
% 181.00/181.22 (~P2(a7,a5,a2)),
% 181.00/181.22 inference(scs_inference,[],[6184,6175,24,22,556])).
% 181.00/181.22 cnf(6210,plain,
% 181.00/181.22 (~P2(a5,a7,a2)),
% 181.00/181.22 inference(scs_inference,[],[6204,24])).
% 181.00/181.22 cnf(6262,plain,
% 181.00/181.22 (P1(a2,a3,a3)),
% 181.00/181.22 inference(scs_inference,[],[15,1604,22])).
% 181.00/181.22 cnf(6292,plain,
% 181.00/181.22 (~P1(a10,a12,a7)+P2(a12,a2,a12)),
% 181.00/181.22 inference(scs_inference,[],[1623,22])).
% 181.00/181.22 cnf(6308,plain,
% 181.00/181.22 (P1(a3,a8,a10)),
% 181.00/181.22 inference(scs_inference,[],[17,1624,22])).
% 181.00/181.22 cnf(6309,plain,
% 181.00/181.22 (~P2(a10,a5,a2)),
% 181.00/181.22 inference(scs_inference,[],[72,18,4595,28])).
% 181.00/181.22 cnf(6322,plain,
% 181.00/181.22 (~P2(a12,a4,a9)),
% 181.00/181.22 inference(scs_inference,[],[4618,8,16,1646,28])).
% 181.00/181.22 cnf(6323,plain,
% 181.00/181.22 (~P2(a4,a12,a9)),
% 181.00/181.22 inference(scs_inference,[],[6322,24])).
% 181.00/181.22 cnf(6339,plain,
% 181.00/181.22 (P1(a6,a8,a10)),
% 181.00/181.22 inference(scs_inference,[],[17,1715,22])).
% 181.00/181.22 cnf(6382,plain,
% 181.00/181.22 (~P1(a11,a2,a4)),
% 181.00/181.22 inference(scs_inference,[],[1390,18,14,17,3436,4846,28,31])).
% 181.00/181.22 cnf(6388,plain,
% 181.00/181.22 (~P1(a2,a11,a4)),
% 181.00/181.22 inference(scs_inference,[],[1390,18,14,17,3436,4846,28,31,24,22])).
% 181.00/181.22 cnf(6448,plain,
% 181.00/181.22 (~P1(a11,a12,a1)),
% 181.00/181.22 inference(scs_inference,[],[1401,20,14,17,4785,4846,28,31])).
% 181.00/181.22 cnf(6455,plain,
% 181.00/181.22 (~P1(a12,a11,a1)),
% 181.00/181.22 inference(scs_inference,[],[1401,20,14,17,4785,4846,28,31,24,22])).
% 181.00/181.22 cnf(6465,plain,
% 181.00/181.22 (~P1(x64651,a12,a1)+~P1(a12,a8,a10)),
% 181.00/181.22 inference(scs_inference,[],[10,6455,16,30,25,24,22])).
% 181.00/181.22 cnf(6503,plain,
% 181.00/181.22 (~P2(a5,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[1417,20,4595,28])).
% 181.00/181.22 cnf(6512,plain,
% 181.00/181.22 (~P1(a11,a10,a7)),
% 181.00/181.22 inference(scs_inference,[],[1417,20,14,17,4601,4595,28,31,2116])).
% 181.00/181.22 cnf(6515,plain,
% 181.00/181.22 (~P1(a12,a11,a2)),
% 181.00/181.22 inference(scs_inference,[],[1417,20,14,17,4601,4595,28,31,2116,24,22])).
% 181.00/181.22 cnf(6518,plain,
% 181.00/181.22 (~P1(a9,a12,a7)),
% 181.00/181.22 inference(scs_inference,[],[6515,1371])).
% 181.00/181.22 cnf(6524,plain,
% 181.00/181.22 (~P2(a10,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[1417,18,4595,6512,22,28])).
% 181.00/181.22 cnf(6528,plain,
% 181.00/181.22 (~P2(a12,a10,a2)),
% 181.00/181.22 inference(scs_inference,[],[1417,18,4595,6512,22,28,24])).
% 181.00/181.22 cnf(6556,plain,
% 181.00/181.22 (~P1(a2,a9,a10)+~P2(a2,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[7,15,6528,31])).
% 181.00/181.22 cnf(6559,plain,
% 181.00/181.22 (~P1(a9,a2,a10)+~P2(a2,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[7,15,6528,31,22])).
% 181.00/181.22 cnf(6568,plain,
% 181.00/181.22 (~P1(a9,a7,a10)+P1(a10,a8,a7)),
% 181.00/181.22 inference(scs_inference,[],[1796,22])).
% 181.00/181.22 cnf(6569,plain,
% 181.00/181.22 (P1(a2,a9,a7)),
% 181.00/181.22 inference(scs_inference,[],[17,1803,22])).
% 181.00/181.22 cnf(6570,plain,
% 181.00/181.22 (~P1(a2,a4,a5)),
% 181.00/181.22 inference(scs_inference,[],[6,6569,1390,6130,31])).
% 181.00/181.22 cnf(6576,plain,
% 181.00/181.22 (~P1(a1,a11,a7)),
% 181.00/181.22 inference(scs_inference,[],[4811,15,17,1833,26])).
% 181.00/181.22 cnf(6582,plain,
% 181.00/181.22 (~P2(a5,a3,a9)),
% 181.00/181.22 inference(scs_inference,[],[3312,6576,20,43,22,29,24])).
% 181.00/181.22 cnf(6594,plain,
% 181.00/181.22 (P2(a4,a5,a5)),
% 181.00/181.22 inference(scs_inference,[],[16,1872,24])).
% 181.00/181.22 cnf(6630,plain,
% 181.00/181.22 (~P1(a5,a11,a10)+P1(a6,a5,a10)),
% 181.00/181.22 inference(scs_inference,[],[1893,386])).
% 181.00/181.22 cnf(6705,plain,
% 181.00/181.22 (~P1(a9,a9,a4)),
% 181.00/181.22 inference(scs_inference,[],[3356,17,19,27])).
% 181.00/181.22 cnf(6715,plain,
% 181.00/181.22 (~P1(a11,a4,a9)),
% 181.00/181.22 inference(scs_inference,[],[3360,15,17,26,22])).
% 181.00/181.22 cnf(6718,plain,
% 181.00/181.22 (~P1(a4,a4,a9)),
% 181.00/181.22 inference(scs_inference,[],[3360,15,19,26])).
% 181.00/181.22 cnf(6722,plain,
% 181.00/181.22 (~P1(a11,a4,a7)),
% 181.00/181.22 inference(scs_inference,[],[3360,6,6715,15,20,14,19,26,30])).
% 181.00/181.22 cnf(6728,plain,
% 181.00/181.22 (~P1(a4,a4,a7)),
% 181.00/181.22 inference(scs_inference,[],[6718,611])).
% 181.00/181.22 cnf(6729,plain,
% 181.00/181.22 (~P1(a4,a10,a7)),
% 181.00/181.22 inference(scs_inference,[],[6718,619])).
% 181.00/181.22 cnf(6738,plain,
% 181.00/181.22 (~P1(a9,a9,a3)),
% 181.00/181.22 inference(scs_inference,[],[3373,17,19,27])).
% 181.00/181.22 cnf(6752,plain,
% 181.00/181.22 (P1(a4,a10,a4)+~P1(a10,a8,a4)),
% 181.00/181.22 inference(scs_inference,[],[2137,1185])).
% 181.00/181.22 cnf(6883,plain,
% 181.00/181.22 (~P1(a10,x68831,a2)),
% 181.00/181.22 inference(scs_inference,[],[3417,9,16,20,13,29,31,25])).
% 181.00/181.22 cnf(6887,plain,
% 181.00/181.22 (~P2(a2,x68871,a10)),
% 181.00/181.22 inference(scs_inference,[],[3417,9,16,20,13,29,31,25,22,23])).
% 181.00/181.22 cnf(6891,plain,
% 181.00/181.22 (P1(a7,a9,a7)),
% 181.00/181.22 inference(scs_inference,[],[17,2473,22])).
% 181.00/181.22 cnf(6899,plain,
% 181.00/181.22 (P2(x68991,a10,x68991)),
% 181.00/181.22 inference(rename_variables,[],[16])).
% 181.00/181.22 cnf(6901,plain,
% 181.00/181.22 (~P2(a10,a2,a4)),
% 181.00/181.22 inference(scs_inference,[],[3419,9,16,29,24])).
% 181.00/181.22 cnf(6907,plain,
% 181.00/181.22 (~P1(a11,a4,a2)+~P2(a4,a10,a4)),
% 181.00/181.22 inference(scs_inference,[],[3419,9,16,6899,15,29,24,31,22])).
% 181.00/181.22 cnf(6915,plain,
% 181.00/181.22 (P1(a2,a7,a7)),
% 181.00/181.22 inference(scs_inference,[],[15,2730,22])).
% 181.00/181.22 cnf(6917,plain,
% 181.00/181.22 (~P1(a11,a4,a2)),
% 181.00/181.22 inference(scs_inference,[],[16,6907])).
% 181.00/181.22 cnf(6995,plain,
% 181.00/181.22 (~P2(a7,a2,x69951)+~P2(x69951,a2,a4)),
% 181.00/181.22 inference(scs_inference,[],[3436,20,29])).
% 181.00/181.22 cnf(7004,plain,
% 181.00/181.22 (P1(a3,a1,a3)),
% 181.00/181.22 inference(scs_inference,[],[17,2878,22])).
% 181.00/181.22 cnf(7036,plain,
% 181.00/181.22 (~P2(a7,a12,x70361)+~P2(x70361,a5,a12)),
% 181.00/181.22 inference(scs_inference,[],[3456,1417,29])).
% 181.00/181.22 cnf(7071,plain,
% 181.00/181.22 (~P1(a1,a6,a10)+P1(a10,a10,a6)),
% 181.00/181.22 inference(scs_inference,[],[3021,22])).
% 181.00/181.22 cnf(7172,plain,
% 181.00/181.22 (P2(a1,a6,a1)),
% 181.00/181.22 inference(scs_inference,[],[17,3028,25])).
% 181.00/181.22 cnf(7179,plain,
% 181.00/181.22 (~P2(a11,x71791,a8)),
% 181.00/181.22 inference(scs_inference,[],[7172,16,14,3805,30,3290,23])).
% 181.00/181.22 cnf(7187,plain,
% 181.00/181.22 (~P1(a8,x71871,a11)),
% 181.00/181.22 inference(scs_inference,[],[7172,16,14,6072,3805,30,3290,23,24,22,31,25])).
% 181.00/181.22 cnf(7190,plain,
% 181.00/181.22 (~P1(x71901,a8,a11)),
% 181.00/181.22 inference(scs_inference,[],[7187,22])).
% 181.00/181.22 cnf(7312,plain,
% 181.00/181.22 (P1(a12,a9,a10)),
% 181.00/181.22 inference(scs_inference,[],[17,3070,22])).
% 181.00/181.22 cnf(7363,plain,
% 181.00/181.22 (P1(a2,a8,a8)),
% 181.00/181.22 inference(scs_inference,[],[15,3104,22])).
% 181.00/181.22 cnf(7398,plain,
% 181.00/181.22 (~P2(a7,a12,x73981)+~P2(x73981,a5,a4)),
% 181.00/181.22 inference(scs_inference,[],[3500,1417,29])).
% 181.00/181.22 cnf(7449,plain,
% 181.00/181.22 (P1(a12,a8,a10)),
% 181.00/181.22 inference(scs_inference,[],[17,3199,22])).
% 181.00/181.22 cnf(7453,plain,
% 181.00/181.22 (~P1(x74531,a12,a1)),
% 181.00/181.22 inference(scs_inference,[],[7449,6465])).
% 181.00/181.22 cnf(7462,plain,
% 181.00/181.22 (~P2(a1,x74621,a12)),
% 181.00/181.22 inference(scs_inference,[],[7453,23])).
% 181.00/181.22 cnf(7480,plain,
% 181.00/181.22 (~P2(a10,a4,a10)+P1(a10,a5,a4)),
% 181.00/181.22 inference(scs_inference,[],[13,8,16,3209,30])).
% 181.00/181.22 cnf(7534,plain,
% 181.00/181.22 (P1(a5,a1,a6)),
% 181.00/181.22 inference(scs_inference,[],[17,3266,22])).
% 181.00/181.22 cnf(7551,plain,
% 181.00/181.22 (~P2(a7,a12,x75511)+~P2(x75511,a12,a4)),
% 181.00/181.22 inference(scs_inference,[],[3565,20,29])).
% 181.00/181.22 cnf(7628,plain,
% 181.00/181.22 (~P1(a10,a8,a5)),
% 181.00/181.22 inference(scs_inference,[],[6113,1185])).
% 181.00/181.22 cnf(7629,plain,
% 181.00/181.22 (~P1(x76291,a7,a5)),
% 181.00/181.22 inference(rename_variables,[],[6113])).
% 181.00/181.22 cnf(7631,plain,
% 181.00/181.22 (~P1(a8,a11,a9)),
% 181.00/181.22 inference(scs_inference,[],[6165,6113,1185,3104])).
% 181.00/181.22 cnf(7632,plain,
% 181.00/181.22 (~P1(x76321,a2,a9)),
% 181.00/181.22 inference(rename_variables,[],[6165])).
% 181.00/181.22 cnf(7634,plain,
% 181.00/181.22 (~P2(a2,a10,a12)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,6113,1185,3104,144])).
% 181.00/181.22 cnf(7636,plain,
% 181.00/181.22 (~P1(a6,a11,a2)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,4634,6113,1185,3104,144,1893])).
% 181.00/181.22 cnf(7639,plain,
% 181.00/181.22 (~P1(a8,a11,a5)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,4634,6113,7629,1185,3104,144,1893,1883])).
% 181.00/181.22 cnf(7640,plain,
% 181.00/181.22 (~P1(x76401,a7,a5)),
% 181.00/181.22 inference(rename_variables,[],[6113])).
% 181.00/181.22 cnf(7642,plain,
% 181.00/181.22 (~P1(a7,a11,a9)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,7632,4634,6113,7629,1185,3104,144,1893,1883,1833])).
% 181.00/181.22 cnf(7645,plain,
% 181.00/181.22 (~P2(a2,a7,a12)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,7632,4634,6113,7629,1185,3104,144,1893,1883,1833,185])).
% 181.00/181.22 cnf(7647,plain,
% 181.00/181.22 (~P2(a5,a10,a9)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,7632,4634,6113,7629,6322,1185,3104,144,1893,1883,1833,185,787])).
% 181.00/181.22 cnf(7649,plain,
% 181.00/181.22 (~P2(a7,a6,a11)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,7632,4634,6113,7629,6322,6073,1185,3104,144,1893,1883,1833,185,787,118])).
% 181.00/181.22 cnf(7651,plain,
% 181.00/181.22 (~P1(a10,a2,a5)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,7632,4634,6113,7629,7640,6322,6073,1185,3104,144,1893,1883,1833,185,787,118,1203])).
% 181.00/181.22 cnf(7657,plain,
% 181.00/181.22 (~P1(a8,a10,a7)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,7632,4634,6729,6113,7629,7640,6322,6073,4577,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473])).
% 181.00/181.22 cnf(7659,plain,
% 181.00/181.22 (P1(a4,a5,a4)),
% 181.00/181.22 inference(scs_inference,[],[6518,6165,7632,4634,6729,6113,7629,7640,6322,6073,4577,6594,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23])).
% 181.00/181.22 cnf(7661,plain,
% 181.00/181.22 (P2(a1,a3,a1)),
% 181.00/181.22 inference(scs_inference,[],[1,6518,6165,7632,4634,6729,6113,7629,7640,6322,6073,4577,6594,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25])).
% 181.00/181.22 cnf(7663,plain,
% 181.00/181.22 (P2(a2,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[1,6518,6165,7632,4634,6729,6113,7629,7640,6322,6073,4577,6594,1401,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24])).
% 181.00/181.22 cnf(7665,plain,
% 181.00/181.22 (P1(a2,a1,a3)),
% 181.00/181.22 inference(scs_inference,[],[1,6518,6165,7632,4634,6729,6113,7629,7640,6322,6073,4577,6594,1401,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22])).
% 181.00/181.22 cnf(7667,plain,
% 181.00/181.22 (~P1(a2,a9,a12)),
% 181.00/181.22 inference(scs_inference,[],[1,6518,6165,7632,4634,6729,6113,7629,7640,6322,6073,4577,6891,6594,1401,59,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27])).
% 181.00/181.22 cnf(7669,plain,
% 181.00/181.22 (~P2(a9,a2,a8)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6518,6165,7632,4634,6729,6113,7629,7640,6322,6073,4577,6891,6594,1401,1390,56,59,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28])).
% 181.00/181.22 cnf(7672,plain,
% 181.00/181.22 (~P2(a4,a5,a9)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6518,6165,7632,4634,4682,6729,6113,7629,7640,6322,6073,4577,6891,6594,1401,1390,56,59,18,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29])).
% 181.00/181.22 cnf(7673,plain,
% 181.00/181.22 (P2(a10,x76731,x76731)),
% 181.00/181.22 inference(rename_variables,[],[18])).
% 181.00/181.22 cnf(7676,plain,
% 181.00/181.22 (~P1(a8,a3,a2)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,18,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26])).
% 181.00/181.22 cnf(7677,plain,
% 181.00/181.22 (~P1(a10,x76771,a2)),
% 181.00/181.22 inference(rename_variables,[],[6883])).
% 181.00/181.22 cnf(7679,plain,
% 181.00/181.22 (~P2(a10,a10,a2)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30])).
% 181.00/181.22 cnf(7684,plain,
% 181.00/181.22 (P2(a7,a2,a2)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31])).
% 181.00/181.22 cnf(7687,plain,
% 181.00/181.22 (~P2(a7,a10,a10)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62])).
% 181.00/181.22 cnf(7689,plain,
% 181.00/181.22 (~P2(a7,a10,a12)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62,128])).
% 181.00/181.22 cnf(7693,plain,
% 181.00/181.22 (~P2(a2,a2,a4)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62,128,4938,6995])).
% 181.00/181.22 cnf(7695,plain,
% 181.00/181.22 (~P2(a7,a7,a10)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62,128,4938,6995,1013])).
% 181.00/181.22 cnf(7696,plain,
% 181.00/181.22 (~P1(a2,a9,a4)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62,128,4938,6995,1013,6045])).
% 181.00/181.22 cnf(7697,plain,
% 181.00/181.22 (~P1(a9,a2,a4)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62,128,4938,6995,1013,6045,6048])).
% 181.00/181.22 cnf(7698,plain,
% 181.00/181.22 (~P1(a9,a2,a12)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62,128,4938,6995,1013,6045,6048,6081])).
% 181.00/181.22 cnf(7699,plain,
% 181.00/181.22 (~P1(a2,a9,a10)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62,128,4938,6995,1013,6045,6048,6081,6556])).
% 181.00/181.22 cnf(7700,plain,
% 181.00/181.22 (~P1(a9,a2,a10)),
% 181.00/181.22 inference(scs_inference,[],[1,7179,6883,7677,6518,6165,7632,4634,4682,6729,7004,6113,7629,7640,6322,6073,4577,6891,6594,37,1401,1390,56,59,11,18,7673,19,1185,3104,144,1893,1883,1833,185,787,118,1203,347,473,23,25,24,22,27,28,29,26,30,31,62,128,4938,6995,1013,6045,6048,6081,6556,6559])).
% 181.00/181.22 cnf(7701,plain,
% 181.00/181.22 (~P1(a9,a12,a7)),
% 181.00/181.22 inference(scs_inference,[],[7700,1372])).
% 181.00/181.22 cnf(7702,plain,
% 181.00/181.22 (~P1(a12,a9,a2)),
% 181.00/181.22 inference(scs_inference,[],[7700,3133])).
% 181.00/181.22 cnf(7708,plain,
% 181.00/181.22 (~P2(a7,a7,a12)),
% 181.00/181.22 inference(scs_inference,[],[7645,128])).
% 181.00/181.22 cnf(7713,plain,
% 181.00/181.22 (~P1(a7,a11,a4)),
% 181.00/181.22 inference(scs_inference,[],[7697,7645,4657,128,1893,1833])).
% 181.00/181.22 cnf(7715,plain,
% 181.00/181.22 (P1(a12,a2,a12)),
% 181.00/181.22 inference(scs_inference,[],[7697,7645,1401,4657,128,1893,1833,23])).
% 181.00/181.22 cnf(7717,plain,
% 181.00/181.22 (P2(a5,a6,a5)),
% 181.00/181.22 inference(scs_inference,[],[7697,7645,7534,1401,4657,128,1893,1833,23,25])).
% 181.00/181.22 cnf(7719,plain,
% 181.00/181.22 (P2(a3,a1,a1)),
% 181.00/181.22 inference(scs_inference,[],[7697,7645,7661,7534,1401,4657,128,1893,1833,23,25,24])).
% 181.00/181.22 cnf(7721,plain,
% 181.00/181.22 (P1(a5,a4,a4)),
% 181.00/181.22 inference(scs_inference,[],[7659,7697,7645,7661,7534,1401,4657,128,1893,1833,23,25,24,22])).
% 181.00/181.22 cnf(7723,plain,
% 181.00/181.22 (~P2(a10,a7,a10)),
% 181.00/181.22 inference(scs_inference,[],[7695,7659,7697,7645,7661,7534,1401,4657,18,20,128,1893,1833,23,25,24,22,28])).
% 181.00/181.22 cnf(7727,plain,
% 181.00/181.22 (~P2(a5,a4,a9)),
% 181.00/181.22 inference(scs_inference,[],[7695,7659,7697,7645,7661,7672,7534,6594,1401,72,4657,18,20,128,1893,1833,23,25,24,22,28,29])).
% 181.00/181.22 cnf(7729,plain,
% 181.00/181.22 (~P1(a8,a10,a5)),
% 181.00/181.22 inference(scs_inference,[],[7695,7628,7659,7697,7645,7661,7672,7534,7449,1574,6594,1401,72,4657,18,20,128,1893,1833,23,25,24,22,28,29,26])).
% 181.00/181.22 cnf(7733,plain,
% 181.00/181.22 (~P2(a10,a7,a12)),
% 181.00/181.22 inference(scs_inference,[],[7695,7628,7659,7687,7697,7645,7661,7672,7534,7449,1574,6594,1401,72,4,4657,40,18,20,128,1893,1833,23,25,24,22,28,29,26,31,3069])).
% 181.00/181.22 cnf(7736,plain,
% 181.00/181.22 (~P2(a10,a6,a11)),
% 181.00/181.22 inference(scs_inference,[],[4726,6738,7695,7628,7659,7687,7697,7645,7661,7665,7672,7534,7449,1574,6594,1401,72,4,4657,11,40,18,14,20,16,128,1893,1833,23,25,24,22,28,29,26,31,3069,27,30])).
% 181.00/181.22 cnf(7744,plain,
% 181.00/181.22 (P1(a12,a5,a12)),
% 181.00/181.22 inference(scs_inference,[],[7698,1417,1833,23])).
% 181.00/181.22 cnf(7746,plain,
% 181.00/181.22 (P2(a2,a8,a2)),
% 181.00/181.22 inference(scs_inference,[],[7698,7363,1417,1833,23,25])).
% 181.00/181.22 cnf(7748,plain,
% 181.00/181.22 (P2(a6,a5,a5)),
% 181.00/181.22 inference(scs_inference,[],[7698,7717,7363,1417,1833,23,25,24])).
% 181.00/181.22 cnf(7750,plain,
% 181.00/181.22 (P1(a5,a6,a6)),
% 181.00/181.22 inference(scs_inference,[],[7698,7717,7363,101,1417,1833,23,25,24,22])).
% 181.00/181.22 cnf(7752,plain,
% 181.00/181.22 (~P1(a10,a8,a7)),
% 181.00/181.22 inference(scs_inference,[],[7657,7698,7717,7449,7363,101,1574,1417,1833,23,25,24,22,27])).
% 181.00/181.22 cnf(7757,plain,
% 181.00/181.22 (~P2(a10,a10,a7)),
% 181.00/181.22 inference(scs_inference,[],[7723,7657,7663,7698,7717,4254,7449,7363,101,1574,1417,56,18,1833,23,25,24,22,27,28,29])).
% 181.00/181.22 cnf(7761,plain,
% 181.00/181.22 (~P1(a11,a7,a12)),
% 181.00/181.22 inference(scs_inference,[],[7667,7723,7657,7663,7698,7717,4254,7449,7363,6569,101,1574,1417,56,17,18,1833,23,25,24,22,27,28,29,26])).
% 181.00/181.22 cnf(7764,plain,
% 181.00/181.22 (~P1(a9,a7,a10)),
% 181.00/181.22 inference(scs_inference,[],[7667,7723,7657,7663,7698,7717,4254,7449,7363,6569,101,1574,1417,56,17,18,1833,23,25,24,22,27,28,29,26,6568])).
% 181.00/181.22 cnf(7765,plain,
% 181.00/181.22 (~P1(a10,a7,a7)),
% 181.00/181.22 inference(scs_inference,[],[7667,7723,7657,7663,7698,7717,4254,7449,7363,6569,101,1574,1417,56,17,18,1833,23,25,24,22,27,28,29,26,6568,1108])).
% 181.00/181.22 cnf(7769,plain,
% 181.00/181.22 (~P1(a10,a2,a7)),
% 181.00/181.22 inference(scs_inference,[],[7667,7702,7723,7657,7715,7663,7698,7717,4254,7449,7363,6569,101,1574,1417,56,17,18,1833,23,25,24,22,27,28,29,26,6568,1108,30,1203])).
% 181.00/181.22 cnf(7774,plain,
% 181.00/181.22 (~P1(a7,a9,a10)),
% 181.00/181.22 inference(scs_inference,[],[7752,1796])).
% 181.00/181.22 cnf(7778,plain,
% 181.00/181.22 (P1(a4,a9,a4)),
% 181.00/181.22 inference(scs_inference,[],[7700,1385,1833,23])).
% 181.00/181.22 cnf(7780,plain,
% 181.00/181.22 (P2(a4,a8,a4)),
% 181.00/181.22 inference(scs_inference,[],[7700,450,1385,1833,23,25])).
% 181.00/181.22 cnf(7782,plain,
% 181.00/181.22 (P2(a8,a2,a2)),
% 181.00/181.22 inference(scs_inference,[],[7746,7700,450,1385,1833,23,25,24])).
% 181.00/181.22 cnf(7784,plain,
% 181.00/181.22 (P1(a5,a12,a12)),
% 181.00/181.22 inference(scs_inference,[],[7744,7746,7700,450,1385,1833,23,25,24,22])).
% 181.00/181.22 cnf(7786,plain,
% 181.00/181.22 (~P1(a7,a9,a12)),
% 181.00/181.22 inference(scs_inference,[],[7744,7746,7700,7701,6891,450,1385,454,1833,23,25,24,22,27])).
% 181.00/181.22 cnf(7788,plain,
% 181.00/181.22 (~P2(a6,a5,a9)),
% 181.00/181.22 inference(scs_inference,[],[7744,7746,7748,7727,7700,7701,6891,450,72,1385,454,1833,23,25,24,22,27,28])).
% 181.00/181.22 cnf(7790,plain,
% 181.00/181.22 (~P2(a8,a8,a9)),
% 181.00/181.22 inference(scs_inference,[],[7744,7746,7748,7727,7700,7701,6200,6891,450,72,1385,454,1833,23,25,24,22,27,28,29])).
% 181.00/181.22 cnf(7793,plain,
% 181.00/181.22 (~P1(a2,a7,a10)),
% 181.00/181.22 inference(scs_inference,[],[7774,7744,7746,7748,7727,7700,7701,6915,6200,6891,450,72,1385,454,1833,23,25,24,22,27,28,29,26])).
% 181.00/181.22 cnf(7799,plain,
% 181.00/181.22 (P1(a4,a2,a8)),
% 181.00/181.22 inference(scs_inference,[],[5032,7774,7744,7746,7748,7727,7700,7701,6915,6200,6891,450,72,1385,17,454,14,1833,23,25,24,22,27,28,29,26,30,1766])).
% 181.00/181.22 cnf(7803,plain,
% 181.00/181.22 (P2(a5,a12,a5)),
% 181.00/181.22 inference(scs_inference,[],[7784,25])).
% 181.00/181.22 cnf(7805,plain,
% 181.00/181.22 (P2(a8,a4,a4)),
% 181.00/181.22 inference(scs_inference,[],[7780,7784,25,24])).
% 181.00/181.22 cnf(7807,plain,
% 181.00/181.22 (P1(a9,a4,a4)),
% 181.00/181.22 inference(scs_inference,[],[7778,7780,7784,25,24,22])).
% 181.00/181.22 cnf(7809,plain,
% 181.00/181.22 (~P1(a1,a6,a9)),
% 181.00/181.22 inference(scs_inference,[],[7778,7780,7784,6154,1380,17,25,24,22,27])).
% 181.00/181.22 cnf(7812,plain,
% 181.00/181.22 (~P2(a8,a2,a4)),
% 181.00/181.22 inference(scs_inference,[],[7693,7778,7780,7782,7784,6154,1380,17,20,25,24,22,27,28])).
% 181.00/181.22 cnf(7815,plain,
% 181.00/181.22 (~P2(a5,a6,a9)),
% 181.00/181.22 inference(scs_inference,[],[7693,7778,7780,7782,7784,7788,6154,7717,7748,1380,17,20,25,24,22,27,28,29])).
% 181.00/181.22 cnf(7817,plain,
% 181.00/181.22 (~P1(a4,a3,a2)),
% 181.00/181.22 inference(scs_inference,[],[7693,7676,7778,7780,7782,7784,7788,7799,6154,6262,7717,7748,1380,17,20,25,24,22,27,28,29,26])).
% 181.00/181.22 cnf(7819,plain,
% 181.00/181.22 (~P2(a12,a2,a12)),
% 181.00/181.22 inference(scs_inference,[],[7693,7676,7778,7780,7782,7784,7788,7799,7634,6154,6262,7717,7748,7449,7715,1380,17,20,25,24,22,27,28,29,26,31])).
% 181.00/181.22 cnf(7821,plain,
% 181.00/181.22 (P1(a8,a4,a8)),
% 181.00/181.22 inference(scs_inference,[],[7693,7676,7778,7780,7782,7784,7788,7799,7634,6154,6262,7717,7748,7449,7715,1380,17,20,25,24,22,27,28,29,26,31,23])).
% 181.00/181.22 cnf(7827,plain,
% 181.00/181.22 (~P1(a12,a10,a7)),
% 181.00/181.22 inference(scs_inference,[],[7819,1623])).
% 181.00/181.22 cnf(7829,plain,
% 181.00/181.22 (~P1(a10,a12,a7)),
% 181.00/181.22 inference(scs_inference,[],[7819,6292])).
% 181.00/181.22 cnf(7830,plain,
% 181.00/181.22 (P2(a9,a4,a9)),
% 181.00/181.22 inference(scs_inference,[],[7807,25])).
% 181.00/181.22 cnf(7834,plain,
% 181.00/181.22 (P1(a2,a4,a8)),
% 181.00/181.22 inference(scs_inference,[],[7807,7799,7172,25,24,22])).
% 181.00/181.22 cnf(7836,plain,
% 181.00/181.22 (~P1(a1,a8,a7)),
% 181.00/181.22 inference(scs_inference,[],[7807,7793,7665,7799,6308,7172,25,24,22,27])).
% 181.00/181.22 cnf(7838,plain,
% 181.00/181.22 (~P2(a6,a5,a2)),
% 181.00/181.22 inference(scs_inference,[],[7803,7807,7793,6503,7665,7799,7748,6308,7172,25,24,22,27,28])).
% 181.00/181.22 cnf(7843,plain,
% 181.00/181.22 (~P1(a11,a7,a4)),
% 181.00/181.22 inference(scs_inference,[],[7696,7736,7803,7807,7793,6503,7665,7799,7748,6308,6569,7172,56,17,18,25,24,22,27,28,29,26])).
% 181.00/181.22 cnf(7846,plain,
% 181.00/181.22 (~P2(a7,a4,a2)),
% 181.00/181.22 inference(scs_inference,[],[6171,7696,7736,7803,7807,7793,6503,7665,7799,7748,6308,6569,7172,56,40,17,18,6,25,24,22,27,28,29,26,30])).
% 181.00/181.22 cnf(7848,plain,
% 181.00/181.22 (P1(a6,a1,a6)),
% 181.00/181.22 inference(scs_inference,[],[6171,7696,7736,7803,7807,7793,6503,7665,7799,7748,6308,6569,7172,56,40,17,18,6,25,24,22,27,28,29,26,30,23])).
% 181.00/181.22 cnf(7852,plain,
% 181.00/181.22 (P2(a2,a9,a11)),
% 181.00/181.22 inference(scs_inference,[],[56,24])).
% 181.00/181.22 cnf(7854,plain,
% 181.00/181.22 (P1(a7,a8,a8)),
% 181.00/181.22 inference(scs_inference,[],[75,56,24,22])).
% 181.00/181.22 cnf(7856,plain,
% 181.00/181.22 (~P2(a9,a4,a8)),
% 181.00/181.22 inference(scs_inference,[],[7790,7830,7780,75,56,24,22,28])).
% 181.00/181.22 cnf(7858,plain,
% 181.00/181.22 (~P2(a8,a4,a2)),
% 181.00/181.22 inference(scs_inference,[],[7805,7790,7830,6901,7780,75,56,18,24,22,28,29])).
% 181.00/181.22 cnf(7863,plain,
% 181.00/181.22 (P2(a7,a8,a7)),
% 181.00/181.22 inference(scs_inference,[],[7786,7805,7790,7830,6901,7780,6915,6891,75,56,18,24,22,28,29,26,25])).
% 181.00/181.22 cnf(7874,plain,
% 181.00/181.22 (P2(a8,a7,a7)),
% 181.00/181.22 inference(scs_inference,[],[7863,24])).
% 181.00/181.22 cnf(7876,plain,
% 181.00/181.22 (P1(a12,a7,a10)),
% 181.00/181.22 inference(scs_inference,[],[7863,1572,24,22])).
% 181.00/181.22 cnf(7881,plain,
% 181.00/181.22 (~P2(a2,a9,a6)),
% 181.00/181.22 inference(scs_inference,[],[7819,7649,7852,7863,7684,1572,1401,18,24,22,28,29])).
% 181.00/181.22 cnf(7883,plain,
% 181.00/181.22 (~P1(a11,a6,a9)),
% 181.00/181.22 inference(scs_inference,[],[7819,7649,7852,7809,7863,7684,1380,1572,1401,17,18,24,22,28,29,26])).
% 181.00/181.22 cnf(7886,plain,
% 181.00/181.22 (~P2(a8,a7,a4)),
% 181.00/181.22 inference(scs_inference,[],[7713,7819,7649,7852,7809,7863,7684,1380,1572,1401,17,18,14,15,24,22,28,29,26,30])).
% 181.00/181.22 cnf(7892,plain,
% 181.00/181.22 (~P2(a2,a4,a2)+P2(a4,a8,a8)),
% 181.00/181.22 inference(scs_inference,[],[4380,7713,7819,7649,7834,7852,7809,7863,7721,7684,7805,7363,1380,1572,1401,17,18,14,15,24,22,28,29,26,30,27,31])).
% 181.00/181.22 cnf(7894,plain,
% 181.00/181.22 (P2(a5,a9,a11)),
% 181.00/181.22 inference(scs_inference,[],[43,24])).
% 181.00/181.22 cnf(7896,plain,
% 181.00/181.22 (P1(a1,a8,a10)),
% 181.00/181.22 inference(scs_inference,[],[5,43,24,22])).
% 181.00/181.22 cnf(7900,plain,
% 181.00/181.22 (~P2(a6,a5,a11)),
% 181.00/181.22 inference(scs_inference,[],[1,7836,3775,7803,7834,7748,5,43,24,22,27,28])).
% 181.00/181.22 cnf(7902,plain,
% 181.00/181.22 (~P2(a8,a7,a10)),
% 181.00/181.22 inference(scs_inference,[],[1,7874,7757,7836,3775,7803,7834,7748,5,43,18,24,22,27,28,29])).
% 181.00/181.22 cnf(7905,plain,
% 181.00/181.22 (~P1(a11,a7,a10)),
% 181.00/181.22 inference(scs_inference,[],[1,7699,7874,7757,7836,3775,7803,7834,7748,6569,5,43,17,18,24,22,27,28,29,26])).
% 181.00/181.22 cnf(7906,plain,
% 181.00/181.22 (P1(a11,x79061,x79061)),
% 181.00/181.22 inference(rename_variables,[],[17])).
% 181.00/181.22 cnf(7908,plain,
% 181.00/181.22 (~P2(a7,a8,a11)),
% 181.00/181.22 inference(scs_inference,[],[1,5026,7699,7874,7757,7836,3775,7803,7834,7748,6569,5,43,17,7906,18,14,24,22,27,28,29,26,30])).
% 181.00/181.22 cnf(7909,plain,
% 181.00/181.22 (P2(a11,x79091,a11)),
% 181.00/181.22 inference(rename_variables,[],[14])).
% 181.00/181.22 cnf(7910,plain,
% 181.00/181.22 (P1(a11,x79101,x79101)),
% 181.00/181.22 inference(rename_variables,[],[17])).
% 181.00/181.22 cnf(7912,plain,
% 181.00/181.22 (~P1(a11,a1,a12)),
% 181.00/181.22 inference(scs_inference,[],[1,5026,7699,7874,7757,7836,7719,7462,3775,7803,7834,7748,6569,5,43,17,7906,7910,18,14,7909,24,22,27,28,29,26,30,31])).
% 181.00/181.22 cnf(7917,plain,
% 181.00/181.22 (P2(a7,a9,a9)),
% 181.00/181.22 inference(scs_inference,[],[40,24])).
% 181.00/181.22 cnf(7919,plain,
% 181.00/181.22 (P1(a7,a4,a8)),
% 181.00/181.22 inference(scs_inference,[],[40,3,24,22])).
% 181.00/181.22 cnf(7921,plain,
% 181.00/181.22 (P1(a9,a8,a8)),
% 181.00/181.22 inference(scs_inference,[],[7854,7363,59,40,3,24,22,27])).
% 181.00/181.22 cnf(7923,plain,
% 181.00/181.22 (~P2(a2,a9,a8)),
% 181.00/181.22 inference(scs_inference,[],[7908,7854,7852,7684,7363,59,40,3,24,22,27,29])).
% 181.00/181.22 cnf(7932,plain,
% 181.00/181.22 (P2(a9,a8,a9)),
% 181.00/181.22 inference(scs_inference,[],[7912,7876,7908,7854,7752,7852,7684,7363,59,40,17,18,14,3,24,22,27,29,26,30,25])).
% 181.00/181.22 cnf(7940,plain,
% 181.00/181.22 (P2(a8,a9,a9)),
% 181.00/181.22 inference(scs_inference,[],[7932,24])).
% 181.00/181.22 cnf(7942,plain,
% 181.00/181.22 (P1(a8,a9,a8)),
% 181.00/181.22 inference(scs_inference,[],[7921,7932,24,22])).
% 181.00/181.22 cnf(7944,plain,
% 181.00/181.22 (~P1(a9,a4,a9)),
% 181.00/181.22 inference(scs_inference,[],[6705,7921,7932,7807,19,24,22,27])).
% 181.00/181.22 cnf(7956,plain,
% 181.00/181.22 (~P2(a9,a10,a6)),
% 181.00/181.22 inference(scs_inference,[],[6705,7689,7886,7883,7917,7921,7932,7863,7874,7807,17,19,14,16,24,22,27,28,29,30,1646])).
% 181.00/181.22 cnf(7963,plain,
% 181.00/181.22 (P2(a1,a8,a11)),
% 181.00/181.22 inference(scs_inference,[],[10,24])).
% 181.00/181.22 cnf(7965,plain,
% 181.00/181.22 (~P1(a8,a12,a5)),
% 181.00/181.22 inference(scs_inference,[],[7942,7729,4,10,24,27])).
% 181.00/181.22 cnf(7972,plain,
% 181.00/181.22 (P2(x79721,x79721,x79721)),
% 181.00/181.22 inference(rename_variables,[],[20])).
% 181.00/181.22 cnf(7974,plain,
% 181.00/181.22 (~P1(a12,a7,a7)),
% 181.00/181.22 inference(scs_inference,[],[7769,7942,7729,7733,7894,4272,7932,7876,1373,4,18,10,20,24,27,28,29,26])).
% 181.00/181.22 cnf(7976,plain,
% 181.00/181.22 (~P2(a8,a10,a5)),
% 181.00/181.22 inference(scs_inference,[],[7769,7639,7942,7729,7733,7894,4272,7932,7876,1373,5,4,18,10,20,7972,24,27,28,29,26,30])).
% 181.00/181.22 cnf(7979,plain,
% 181.00/181.22 (~P2(a5,a7,a6)),
% 181.00/181.22 inference(scs_inference,[],[7769,7639,7942,7729,7733,7894,4272,7932,7876,1373,5,4,18,10,20,7972,24,27,28,29,26,30,1864])).
% 181.00/181.22 cnf(7988,plain,
% 181.00/181.22 (P2(a12,a9,a11)),
% 181.00/181.22 inference(scs_inference,[],[7,24])).
% 181.00/181.22 cnf(8003,plain,
% 181.00/181.22 (P2(a7,a12,a2)),
% 181.00/181.22 inference(scs_inference,[],[9,24])).
% 181.00/181.22 cnf(8005,plain,
% 181.00/181.22 (~P1(a4,a9,a7)),
% 181.00/181.22 inference(scs_inference,[],[7843,7778,17,9,24,27])).
% 181.00/181.22 cnf(8010,plain,
% 181.00/181.22 (~P1(a8,a3,a5)),
% 181.00/181.22 inference(scs_inference,[],[1,7651,7843,7902,7778,7863,7874,5,17,9,24,27,29,26])).
% 181.00/181.22 cnf(8016,plain,
% 181.00/181.22 (~P2(a2,a5,a3)),
% 181.00/181.22 inference(scs_inference,[],[1,7642,7651,7843,7902,7963,7940,7778,7863,7874,5,17,9,24,27,29,26,30,5165,5197])).
% 181.00/181.22 cnf(8018,plain,
% 181.00/181.22 (~P2(a2,a5,a12)),
% 181.00/181.22 inference(scs_inference,[],[1,7642,7651,7843,7902,7963,7940,7778,7863,7874,5,17,9,24,27,29,26,30,5165,5197,7036])).
% 181.00/181.22 cnf(8020,plain,
% 181.00/181.22 (~P2(a2,a5,a4)),
% 181.00/181.22 inference(scs_inference,[],[1,7642,7651,7843,7902,7963,7940,7778,7863,7874,5,17,9,24,27,29,26,30,5165,5197,7036,7398])).
% 181.00/181.22 cnf(8022,plain,
% 181.00/181.22 (~P2(a2,a12,a4)),
% 181.00/181.22 inference(scs_inference,[],[1,7642,7651,7843,7902,7963,7940,7778,7863,7874,5,17,9,24,27,29,26,30,5165,5197,7036,7398,7551])).
% 181.00/181.22 cnf(8028,plain,
% 181.00/181.22 (P2(a3,a2,a2)),
% 181.00/181.22 inference(scs_inference,[],[231,24])).
% 181.00/181.22 cnf(8030,plain,
% 181.00/181.22 (~P1(a10,a10,a7)),
% 181.00/181.22 inference(scs_inference,[],[7905,11,19,231,24,27])).
% 181.00/181.22 cnf(8034,plain,
% 181.00/181.22 (~P2(a8,a7,a12)),
% 181.00/181.22 inference(scs_inference,[],[7708,7905,7874,11,19,231,20,24,27,28])).
% 181.00/181.22 cnf(8041,plain,
% 181.00/181.22 (~P2(a9,a12,a8)),
% 181.00/181.22 inference(scs_inference,[],[7829,8020,7708,7988,7905,7190,7896,7805,7874,1574,72,11,17,19,14,231,20,24,27,28,29,26,30])).
% 181.00/181.22 cnf(8048,plain,
% 181.00/181.22 (~P1(a10,a6,a7)),
% 181.00/181.22 inference(scs_inference,[],[7829,8020,7708,7988,7905,7190,7896,7805,7874,1574,72,11,17,19,14,231,20,24,27,28,29,26,30,1121,1160])).
% 181.00/181.22 cnf(8054,plain,
% 181.00/181.22 (~P1(a6,a10,a7)),
% 181.00/181.22 inference(scs_inference,[],[7829,8020,7708,7988,7905,7190,7896,7805,7874,1574,72,11,17,19,14,231,20,24,27,28,29,26,30,1121,1160,1147,78,361])).
% 181.00/181.22 cnf(8059,plain,
% 181.00/181.22 (~P1(a7,a9,a10)),
% 181.00/181.22 inference(scs_inference,[],[8030,1792])).
% 181.00/181.22 cnf(8060,plain,
% 181.00/181.22 (P2(a4,a12,a5)),
% 181.00/181.22 inference(scs_inference,[],[8,24])).
% 181.00/181.22 cnf(8062,plain,
% 181.00/181.22 (~P2(a8,a9,a8)),
% 181.00/181.22 inference(scs_inference,[],[7856,7940,7830,8,24,28])).
% 181.00/181.22 cnf(8064,plain,
% 181.00/181.22 (~P2(a6,a6,a11)),
% 181.00/181.22 inference(scs_inference,[],[7856,4167,7940,7830,7717,8,24,28,29])).
% 181.00/181.22 cnf(8067,plain,
% 181.00/181.22 (~P1(a1,a8,a2)),
% 181.00/181.22 inference(scs_inference,[],[7856,4167,7940,7942,7830,6883,7717,7896,8,24,28,29,26])).
% 181.00/181.22 cnf(8070,plain,
% 181.00/181.22 (~P2(a8,a4,a7)),
% 181.00/181.22 inference(scs_inference,[],[8005,7856,4167,7940,7942,7830,6883,7932,7717,7896,7778,7780,8,24,28,29,26,30])).
% 181.00/181.22 cnf(8072,plain,
% 181.00/181.22 (P2(a8,a3,a2)),
% 181.00/181.22 inference(scs_inference,[],[8005,7856,4167,7963,7940,7942,7830,6883,7932,7717,7896,7778,7780,7746,7665,15,8,24,28,29,26,30,31])).
% 181.00/181.22 cnf(8076,plain,
% 181.00/181.22 (~P2(a4,a9,a4)),
% 181.00/181.22 inference(scs_inference,[],[8005,7856,4167,7963,7940,7942,7830,6883,7932,7717,7896,7778,7780,7746,7665,15,8,24,28,29,26,30,31,5316,5308])).
% 181.00/181.22 cnf(8077,plain,
% 181.00/181.22 (~P2(a7,a4,a4)),
% 181.00/181.22 inference(scs_inference,[],[8005,7856,4167,7963,7940,7942,7830,6883,7932,7717,7896,7778,7780,7746,7665,15,8,24,28,29,26,30,31,5316,5308,5318])).
% 181.00/181.22 cnf(8087,plain,
% 181.00/181.22 (~P2(a4,a7,a4)),
% 181.00/181.22 inference(scs_inference,[],[8060,5314])).
% 181.00/181.22 cnf(8088,plain,
% 181.00/181.22 (P2(a3,a8,a2)),
% 181.00/181.22 inference(scs_inference,[],[8072,24])).
% 181.00/181.22 cnf(8094,plain,
% 181.00/181.22 (~P1(x80941,a8,a9)),
% 181.00/181.22 inference(scs_inference,[],[8022,7944,7846,8072,8028,8003,7821,7663,24,28,29,26])).
% 181.00/181.22 cnf(8101,plain,
% 181.00/181.22 (~P1(a9,a1,a8)),
% 181.00/181.22 inference(scs_inference,[],[8022,7944,7846,7761,8072,8028,8003,7821,7790,7963,7932,7663,17,18,14,15,24,28,29,26,30,31])).
% 181.00/181.22 cnf(8107,plain,
% 181.00/181.22 (~P2(a10,a7,a4)),
% 181.00/181.22 inference(scs_inference,[],[8087,2435])).
% 181.00/181.22 cnf(8111,plain,
% 181.00/181.22 (P2(a7,a4,a9)),
% 181.00/181.22 inference(scs_inference,[],[8087,6,542,24])).
% 181.00/181.22 cnf(8113,plain,
% 181.00/181.22 (~P1(a6,a8,a7)),
% 181.00/181.22 inference(scs_inference,[],[8087,8054,7848,7896,6,542,24,27])).
% 181.00/181.22 cnf(8115,plain,
% 181.00/181.22 (~P2(a8,a9,a4)),
% 181.00/181.22 inference(scs_inference,[],[8087,8054,7848,7805,7896,6,542,24,27,28])).
% 181.00/181.22 cnf(8117,plain,
% 181.00/181.22 (~P2(a4,a9,a8)),
% 181.00/181.22 inference(scs_inference,[],[8087,8076,8054,7848,7830,7805,7896,6,542,24,27,28,29])).
% 181.00/181.22 cnf(8119,plain,
% 181.00/181.22 (~P1(a6,a1,a2)),
% 181.00/181.22 inference(scs_inference,[],[7636,8087,8076,8054,7848,7830,7805,7896,15,6,542,24,27,28,29,26])).
% 181.00/181.22 cnf(8127,plain,
% 181.00/181.22 (~P2(a9,a10,a8)),
% 181.00/181.22 inference(scs_inference,[],[7636,8087,8076,8054,8094,7848,7917,7830,7805,7896,17,14,15,6,542,24,27,28,29,26,30,1646])).
% 181.00/181.22 cnf(8139,plain,
% 181.00/181.22 (~P2(a2,a8,a4)),
% 181.00/181.22 inference(scs_inference,[],[8088,7679,8010,8041,8111,8060,6917,6262,7782,7799,17,18,14,28,29,26,30])).
% 181.00/181.22 cnf(8154,plain,
% 181.00/181.22 (~P1(a8,a6,a7)),
% 181.00/181.22 inference(scs_inference,[],[7881,7838,8048,8088,7940,7717,7748,1380,5,28,29,26])).
% 181.00/181.22 cnf(8167,plain,
% 181.00/181.22 (~P2(a4,a8,a7)),
% 181.00/181.22 inference(scs_inference,[],[1,7956,8107,8067,8111,7834,7780,18,16,27,28,29])).
% 181.00/181.22 cnf(8170,plain,
% 181.00/181.22 (~P1(a7,a4,a9)),
% 181.00/181.22 inference(scs_inference,[],[1,7631,7956,8107,8067,7919,8111,7834,7780,18,15,16,27,28,29,26])).
% 181.00/181.22 cnf(8183,plain,
% 181.00/181.22 (~P2(a8,a3,a5)),
% 181.00/181.22 inference(scs_inference,[],[6323,6309,8072,8060,7805,18,28,29])).
% 181.00/181.22 cnf(8188,plain,
% 181.00/181.22 (~P1(a9,a7,a12)),
% 181.00/181.22 inference(scs_inference,[],[4628,8119,6323,6309,8072,8060,8111,7848,7830,7805,1380,18,28,29,26,30])).
% 181.00/181.22 cnf(8196,plain,
% 181.00/181.22 (~P2(a10,a9,a8)),
% 181.00/181.22 inference(scs_inference,[],[8062,7940,18,28])).
% 181.00/181.22 cnf(8199,plain,
% 181.00/181.22 (~P2(a9,a8,a8)),
% 181.00/181.22 inference(scs_inference,[],[8062,7940,7932,18,28,29])).
% 181.00/181.22 cnf(8212,plain,
% 181.00/181.22 (~P2(a4,a2,a6)),
% 181.00/181.22 inference(scs_inference,[],[7979,8113,7942,6339,8060,9,27,28])).
% 181.00/181.22 cnf(8226,plain,
% 181.00/181.22 (~P2(a8,a5,a2)),
% 181.00/181.22 inference(scs_inference,[],[6043,8060,7805,28])).
% 181.00/181.22 cnf(8254,plain,
% 181.00/181.22 (~P2(a5,a12,a9)),
% 181.00/181.22 inference(scs_inference,[],[7647,7803,16,28])).
% 181.00/181.23 cnf(8255,plain,
% 181.00/181.23 (P2(x82551,a10,x82551)),
% 181.00/181.23 inference(rename_variables,[],[16])).
% 181.00/181.23 cnf(8265,plain,
% 181.00/181.23 (~P1(a7,a10,a7)),
% 181.00/181.23 inference(scs_inference,[],[7647,7812,8154,8101,7921,7803,7780,7805,53,18,16,8255,28,29,26,30,1842])).
% 181.00/181.23 cnf(8271,plain,
% 181.00/181.23 (~P1(a10,x82711,a7)),
% 181.00/181.23 inference(scs_inference,[],[7765,11,27])).
% 181.00/181.23 cnf(8277,plain,
% 181.00/181.23 (~P2(a4,a8,a9)),
% 181.00/181.23 inference(scs_inference,[],[8070,8115,7765,7780,7805,11,18,27,28,29])).
% 181.00/181.23 cnf(8288,plain,
% 181.00/181.23 (~P1(a2,a2,a10)),
% 181.00/181.23 inference(scs_inference,[],[8265,1373,27])).
% 181.00/181.23 cnf(8292,plain,
% 181.00/181.23 (~P2(a3,a2,a12)),
% 181.00/181.23 inference(scs_inference,[],[8254,8265,6524,8028,8060,1373,72,18,27,28,29])).
% 181.00/181.23 cnf(8301,plain,
% 181.00/181.23 (~P1(a8,a1,a2)),
% 181.00/181.23 inference(scs_inference,[],[1,8288,8117,7917,37,6,29,26])).
% 181.00/181.23 cnf(8316,plain,
% 181.00/181.23 (P2(x83161,x83161,x83161)),
% 181.00/181.23 inference(rename_variables,[],[20])).
% 181.00/181.23 cnf(8318,plain,
% 181.00/181.23 (~P1(a2,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[1,8199,8196,6570,8067,8111,7363,7834,7780,19,18,20,27,28,29,26])).
% 181.00/181.23 cnf(8321,plain,
% 181.00/181.23 (~P2(a4,a4,a9)),
% 181.00/181.23 inference(scs_inference,[],[1,8199,8196,6570,6705,8067,7807,8111,7363,7830,7834,7780,19,18,20,8316,27,28,29,26,30])).
% 181.00/181.23 cnf(8324,plain,
% 181.00/181.23 (~P2(a8,a5,a3)),
% 181.00/181.23 inference(scs_inference,[],[8016,8088,20,28])).
% 181.00/181.23 cnf(8336,plain,
% 181.00/181.23 (~P1(a11,a2,a10)),
% 181.00/181.23 inference(scs_inference,[],[8016,8271,6887,7744,4601,7684,7717,8088,1574,53,11,17,14,20,28,29,26,27,31])).
% 181.00/181.23 cnf(8354,plain,
% 181.00/181.23 (~P2(a7,a8,a8)),
% 181.00/181.23 inference(scs_inference,[],[8277,8321,7917,8111,7932,6,28,29])).
% 181.00/181.23 cnf(8356,plain,
% 181.00/181.23 (~P1(x83561,a12,a7)),
% 181.00/181.23 inference(scs_inference,[],[8059,8277,8321,7917,8111,7932,7312,11,6,28,29,26])).
% 181.00/181.23 cnf(8358,plain,
% 181.00/181.23 (~P2(a8,a4,a11)),
% 181.00/181.23 inference(scs_inference,[],[8059,8277,8321,3355,7917,8111,7932,7780,7312,11,17,14,6,28,29,26,30])).
% 181.00/181.23 cnf(8362,plain,
% 181.00/181.23 (~P2(a8,a7,a8)),
% 181.00/181.23 inference(scs_inference,[],[8059,8277,8321,3355,7921,7917,8111,7932,7780,7312,11,40,17,14,6,28,29,26,30,31])).
% 181.00/181.23 cnf(8364,plain,
% 181.00/181.23 (~P2(a10,a9,a4)),
% 181.00/181.23 inference(scs_inference,[],[8059,8277,8321,3355,7921,7917,8111,7932,7780,7312,11,40,17,14,6,28,29,26,30,31,2242])).
% 181.00/181.23 cnf(8367,plain,
% 181.00/181.23 (~P2(a4,a7,a4)),
% 181.00/181.23 inference(scs_inference,[],[8354,86])).
% 181.00/181.23 cnf(8371,plain,
% 181.00/181.23 (~P1(a9,a4,a2)),
% 181.00/181.23 inference(scs_inference,[],[7697,7807,19,27])).
% 181.00/181.23 cnf(8372,plain,
% 181.00/181.23 (P1(x83721,x83721,x83721)),
% 181.00/181.23 inference(rename_variables,[],[19])).
% 181.00/181.23 cnf(8384,plain,
% 181.00/181.23 (~P2(a8,a8,a11)),
% 181.00/181.23 inference(scs_inference,[],[8292,6180,5671,4884,7697,7919,8003,7807,8111,7863,7780,19,8372,18,15,27,28,29,26,30])).
% 181.00/181.23 cnf(8390,plain,
% 181.00/181.23 (~P1(a10,a5,a5)),
% 181.00/181.23 inference(scs_inference,[],[7965,7744,1574,27])).
% 181.00/181.23 cnf(8398,plain,
% 181.00/181.23 (~P1(a10,a3,a5)),
% 181.00/181.23 inference(scs_inference,[],[1,8139,7965,7651,4682,7744,7717,8088,1574,13,20,27,28,29,26])).
% 181.00/181.23 cnf(8404,plain,
% 181.00/181.23 (~P2(a7,a4,a7)+P2(a4,a8,a8)),
% 181.00/181.23 inference(scs_inference,[],[1,8139,7965,7651,7784,4682,7744,7919,7854,6113,7717,8088,8060,7805,1574,72,13,20,27,28,29,26,30,31])).
% 181.00/181.23 cnf(8408,plain,
% 181.00/181.23 (~P2(a10,a7,a8)),
% 181.00/181.23 inference(scs_inference,[],[7827,8362,7876,6915,7874,18,27,28])).
% 181.00/181.23 cnf(8411,plain,
% 181.00/181.23 (~P1(a10,a4,a5)),
% 181.00/181.23 inference(scs_inference,[],[7827,8362,8390,7659,7876,6915,7874,13,18,27,28,26])).
% 181.00/181.23 cnf(8414,plain,
% 181.00/181.23 (~P2(a2,a8,a12)),
% 181.00/181.23 inference(scs_inference,[],[7827,8362,8390,8356,7659,7876,6915,7874,7863,1373,13,18,27,28,26,30])).
% 181.00/181.23 cnf(8423,plain,
% 181.00/181.23 (~P1(a2,a2,a12)),
% 181.00/181.23 inference(scs_inference,[],[8356,1373,27])).
% 181.00/181.23 cnf(8426,plain,
% 181.00/181.23 (~P2(a8,a4,a9)),
% 181.00/181.23 inference(scs_inference,[],[8364,8356,7805,1373,18,27,29])).
% 181.00/181.23 cnf(8431,plain,
% 181.00/181.23 (~P1(a9,a4,a3)),
% 181.00/181.23 inference(scs_inference,[],[8411,8371,8364,8356,7821,8072,7449,7932,7805,7780,1373,18,27,29,26,30])).
% 181.00/181.23 cnf(8442,plain,
% 181.00/181.23 (~P2(a12,a5,a9)),
% 181.00/181.23 inference(scs_inference,[],[8188,8426,8431,8254,7917,7807,6915,7830,8060,7874,59,20,8,27,29,30,28])).
% 181.00/181.23 cnf(8453,plain,
% 181.00/181.23 (~P1(a6,a10,a5)),
% 181.00/181.23 inference(scs_inference,[],[1,8442,7817,8398,6339,37,1417,19,18,27,28,26])).
% 181.00/181.23 cnf(8470,plain,
% 181.00/181.23 (~P2(a10,a4,a2)),
% 181.00/181.23 inference(scs_inference,[],[8423,7858,7805,19,18,334,27,28])).
% 181.00/181.23 cnf(8485,plain,
% 181.00/181.23 (~P1(a6,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[8453,7848,7896,27])).
% 181.00/181.23 cnf(8487,plain,
% 181.00/181.23 (~P2(a4,a12,a3)),
% 181.00/181.23 inference(scs_inference,[],[8183,8453,7848,7896,8060,7805,27,29])).
% 181.00/181.23 cnf(8500,plain,
% 181.00/181.23 (~P1(a6,a8,a2)),
% 181.00/181.23 inference(scs_inference,[],[8336,6339,17,27])).
% 181.00/181.23 cnf(8503,plain,
% 181.00/181.23 (~P2(a5,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[8212,8336,6339,8060,1401,17,27,29])).
% 181.00/181.23 cnf(8505,plain,
% 181.00/181.23 (~P1(a5,a10,a5)),
% 181.00/181.23 inference(scs_inference,[],[8212,8485,8336,7750,6339,8060,1401,17,27,29,26])).
% 181.00/181.23 cnf(8515,plain,
% 181.00/181.23 (P1(a5,a8,a8)),
% 181.00/181.23 inference(scs_inference,[],[7721,7799,27])).
% 181.00/181.23 cnf(8517,plain,
% 181.00/181.23 (~P2(a4,a5,a10)),
% 181.00/181.23 inference(scs_inference,[],[7976,7721,7799,6594,7805,27,29])).
% 181.00/181.23 cnf(8519,plain,
% 181.00/181.23 (~P2(a5,a4,a10)),
% 181.00/181.23 inference(scs_inference,[],[8505,7976,7721,7799,6594,7805,72,19,27,29,30])).
% 181.00/181.23 cnf(8522,plain,
% 181.00/181.23 (~P2(a5,a10,a10)),
% 181.00/181.23 inference(scs_inference,[],[8505,7976,7721,7799,6594,7805,72,19,27,29,30,1872])).
% 181.00/181.23 cnf(8524,plain,
% 181.00/181.23 (P2(a5,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[8505,7976,7721,7799,6594,7805,72,19,27,29,30,1872,25])).
% 181.00/181.23 cnf(8526,plain,
% 181.00/181.23 (P2(a8,a5,a5)),
% 181.00/181.23 inference(scs_inference,[],[8505,7976,7721,7799,6594,7805,72,19,27,29,30,1872,25,24])).
% 181.00/181.23 cnf(8528,plain,
% 181.00/181.23 (P1(a8,a5,a8)),
% 181.00/181.23 inference(scs_inference,[],[8505,7976,7721,7799,6594,7805,72,19,27,29,30,1872,25,24,22])).
% 181.00/181.23 cnf(8535,plain,
% 181.00/181.23 (~P2(a5,a2,a9)),
% 181.00/181.23 inference(scs_inference,[],[8524,6582,8072,28])).
% 181.00/181.23 cnf(8537,plain,
% 181.00/181.23 (~P2(a9,a6,a6)),
% 181.00/181.23 inference(scs_inference,[],[8524,6582,4679,7748,8072,28,29])).
% 181.00/181.23 cnf(8540,plain,
% 181.00/181.23 (~P1(a8,a6,a2)),
% 181.00/181.23 inference(scs_inference,[],[8528,8301,8524,6582,4679,7534,7748,8072,28,29,26])).
% 181.00/181.23 cnf(8542,plain,
% 181.00/181.23 (~P2(a5,a8,a10)),
% 181.00/181.23 inference(scs_inference,[],[8528,8301,8524,8526,6582,4679,8505,7534,7748,8072,19,28,29,26,30])).
% 181.00/181.23 cnf(8551,plain,
% 181.00/181.23 (~P2(a8,a5,a10)),
% 181.00/181.23 inference(scs_inference,[],[8522,6722,8526,6891,17,16,27,28])).
% 181.00/181.23 cnf(8554,plain,
% 181.00/181.23 (~P2(a5,a5,a10)),
% 181.00/181.23 inference(scs_inference,[],[8517,8522,6722,8526,6891,8060,1417,17,16,27,28,29])).
% 181.00/181.23 cnf(8559,plain,
% 181.00/181.23 (P2(a8,a6,a5)),
% 181.00/181.23 inference(scs_inference,[],[8517,8522,8540,6722,8528,8526,8524,7534,7963,6891,8060,1417,17,15,20,16,27,28,29,30,31])).
% 181.00/181.23 cnf(8562,plain,
% 181.00/181.23 (P2(a6,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[8517,8522,8540,6722,8528,8526,8524,7534,7963,6891,8060,1417,17,15,20,16,27,28,29,30,31,24])).
% 181.00/181.23 cnf(8564,plain,
% 181.00/181.23 (~P2(a9,a6,a8)),
% 181.00/181.23 inference(scs_inference,[],[8384,8562,43,28])).
% 181.00/181.23 cnf(8566,plain,
% 181.00/181.23 (~P2(a8,a8,a7)),
% 181.00/181.23 inference(scs_inference,[],[8384,8562,8367,7780,43,28,29])).
% 181.00/181.23 cnf(8568,plain,
% 181.00/181.23 (~P1(a2,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[8318,8384,8562,8559,8367,7746,7780,43,18,28,29,30])).
% 181.00/181.23 cnf(8571,plain,
% 181.00/181.23 (~P1(a11,a6,a3)),
% 181.00/181.23 inference(scs_inference,[],[8318,8384,8562,8559,8367,8183,7746,7780,43,17,18,14,28,29,30,31])).
% 181.00/181.23 cnf(8575,plain,
% 181.00/181.23 (~P1(a5,a2,x85751)+P1(a4,x85751,a8)),
% 181.00/181.23 inference(scs_inference,[],[8318,8384,8562,8559,8367,8183,7659,7746,7799,7780,43,17,18,14,28,29,30,31,27])).
% 181.00/181.23 cnf(8581,plain,
% 181.00/181.23 (~P1(a1,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[1,8571,17,27])).
% 181.00/181.23 cnf(8584,plain,
% 181.00/181.23 (~P2(a6,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[1,8503,8571,8562,7782,17,27,28])).
% 181.00/181.23 cnf(8586,plain,
% 181.00/181.23 (~P2(a8,a6,a3)),
% 181.00/181.23 inference(scs_inference,[],[1,8226,8503,8571,8562,7782,8088,17,27,28,29])).
% 181.00/181.23 cnf(8588,plain,
% 181.00/181.23 (~P1(x85881,a12,a2)),
% 181.00/181.23 inference(scs_inference,[],[1,8226,8503,8571,7793,8562,7782,7876,8088,11,17,27,28,29,26])).
% 181.00/181.23 cnf(8604,plain,
% 181.00/181.23 (~P2(a5,a8,a3)),
% 181.00/181.23 inference(scs_inference,[],[7974,7923,8324,8559,8562,8072,6569,20,27,28,29])).
% 181.00/181.23 cnf(8610,plain,
% 181.00/181.23 (~P2(a10,a5,a10)),
% 181.00/181.23 inference(scs_inference,[],[8551,8526,18,28])).
% 181.00/181.23 cnf(8613,plain,
% 181.00/181.23 (~P2(a8,a9,a6)),
% 181.00/181.23 inference(scs_inference,[],[8551,8064,8526,7894,8562,18,28,29])).
% 181.00/181.23 cnf(8625,plain,
% 181.00/181.23 (~P2(a10,a10,a5)),
% 181.00/181.23 inference(scs_inference,[],[8610,18,29])).
% 181.00/181.23 cnf(8641,plain,
% 181.00/181.23 (~P1(a6,a4,a2)),
% 181.00/181.23 inference(scs_inference,[],[8500,7799,19,27])).
% 181.00/181.23 cnf(8644,plain,
% 181.00/181.23 (~P2(a2,x86441,a8)),
% 181.00/181.23 inference(scs_inference,[],[8500,8354,7684,7799,19,27,29])).
% 181.00/181.23 cnf(8646,plain,
% 181.00/181.23 (~P1(a12,a8,a2)),
% 181.00/181.23 inference(scs_inference,[],[8500,8354,7699,7684,7942,7449,7799,19,27,29,26])).
% 181.00/181.23 cnf(8648,plain,
% 181.00/181.23 (~P1(a2,a1,a5)),
% 181.00/181.23 inference(scs_inference,[],[8500,8354,5533,7699,8526,7684,7942,7449,7963,7746,7799,19,27,29,26,30])).
% 181.00/181.23 cnf(8656,plain,
% 181.00/181.23 (~P2(a3,a2,a8)),
% 181.00/181.23 inference(scs_inference,[],[8644,8028,7663,28])).
% 181.00/181.23 cnf(8669,plain,
% 181.00/181.23 (~P2(a7,a2,a12)),
% 181.00/181.23 inference(scs_inference,[],[8414,7684,7746,28])).
% 181.00/181.23 cnf(8671,plain,
% 181.00/181.23 (~P2(a6,a5,a10)),
% 181.00/181.23 inference(scs_inference,[],[8625,8414,7684,7748,7746,18,28,29])).
% 181.00/181.23 cnf(8683,plain,
% 181.00/181.23 (~P1(a8,a1,a5)),
% 181.00/181.23 inference(scs_inference,[],[8358,8669,7639,7988,8526,8003,8111,7963,1401,20,28,29,30])).
% 181.00/181.23 cnf(8686,plain,
% 181.00/181.23 (~P1(a2,a5,x86861)+P1(a4,x86861,a8)),
% 181.00/181.23 inference(scs_inference,[],[8358,8669,7639,7988,8528,8526,8003,8111,7963,7799,1401,20,28,29,30,27])).
% 181.00/181.23 cnf(8693,plain,
% 181.00/181.23 (~P1(a2,a8,a6)),
% 181.00/181.23 inference(scs_inference,[],[8568,7848,5,27])).
% 181.00/181.23 cnf(8695,plain,
% 181.00/181.23 (~P2(a8,a2,a12)),
% 181.00/181.23 inference(scs_inference,[],[8568,8669,7848,7684,7874,5,27,28])).
% 181.00/181.23 cnf(8697,plain,
% 181.00/181.23 (~P1(a3,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[8568,8411,8669,7821,7848,6308,7684,7874,5,27,28,26])).
% 181.00/181.23 cnf(8699,plain,
% 181.00/181.23 (~P1(a7,a7,a6)),
% 181.00/181.23 inference(scs_inference,[],[8568,8411,8669,6104,7821,8559,7848,6308,7684,7863,7874,5,27,28,26,30])).
% 181.00/181.23 cnf(8708,plain,
% 181.00/181.23 (~P1(a3,a8,a6)),
% 181.00/181.23 inference(scs_inference,[],[8568,6262,6308,27])).
% 181.00/181.23 cnf(8713,plain,
% 181.00/181.23 (~P1(a8,a6,a5)),
% 181.00/181.23 inference(scs_inference,[],[8127,8683,8568,6262,8528,7534,6308,16,6,27,28,26])).
% 181.00/181.23 cnf(8719,plain,
% 181.00/181.23 (~P2(a6,a9,a6)),
% 181.00/181.23 inference(scs_inference,[],[8127,8537,8683,8568,8588,7894,6262,8528,8028,101,7534,6308,19,15,231,16,6,27,28,26,30,31])).
% 181.00/181.23 cnf(8730,plain,
% 181.00/181.23 (~P2(a9,x87301,a4)),
% 181.00/181.23 inference(scs_inference,[],[7900,8077,8526,7917,43,28,29])).
% 181.00/181.23 cnf(8734,plain,
% 181.00/181.23 (~P1(a11,a5,a10)),
% 181.00/181.23 inference(scs_inference,[],[8542,7900,8077,8713,8526,7363,7917,53,43,17,14,28,29,26,31])).
% 181.00/181.23 cnf(8740,plain,
% 181.00/181.23 (~P2(a7,x87401,a4)),
% 181.00/181.23 inference(scs_inference,[],[8542,7900,8077,8713,8526,7363,7917,53,43,17,14,28,29,26,31,572,586])).
% 181.00/181.23 cnf(8757,plain,
% 181.00/181.23 (~P1(a1,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[8734,7896,17,27])).
% 181.00/181.23 cnf(8760,plain,
% 181.00/181.23 (~P1(a1,a3,a6)),
% 181.00/181.23 inference(scs_inference,[],[1,8734,8581,7896,19,17,27,26])).
% 181.00/181.23 cnf(8784,plain,
% 181.00/181.23 (~P2(a5,a12,a3)),
% 181.00/181.23 inference(scs_inference,[],[8487,8760,7848,1380,8060,20,27,29])).
% 181.00/181.23 cnf(8814,plain,
% 181.00/181.23 (~P2(a8,a12,a4)),
% 181.00/181.23 inference(scs_inference,[],[7846,8003,7863,29])).
% 181.00/181.23 cnf(8834,plain,
% 181.00/181.23 (~P1(a4,a9,a2)),
% 181.00/181.23 inference(scs_inference,[],[6382,7778,17,27])).
% 181.00/181.23 cnf(8839,plain,
% 181.00/181.23 (~P2(a2,a12,a12)),
% 181.00/181.23 inference(scs_inference,[],[8535,8695,6382,7778,8562,7782,7663,17,27,28,29])).
% 181.00/181.23 cnf(8841,plain,
% 181.00/181.23 (~P2(a8,a6,a7)),
% 181.00/181.23 inference(scs_inference,[],[8535,8695,6382,6113,8515,7778,8562,7782,7717,7663,17,27,28,29,30])).
% 181.00/181.23 cnf(8844,plain,
% 181.00/181.23 (~P2(a7,a12,a12)),
% 181.00/181.23 inference(scs_inference,[],[8535,8695,6382,6113,8515,7778,8562,7782,7717,7663,17,27,28,29,30,128])).
% 181.00/181.23 cnf(8848,plain,
% 181.00/181.23 (~P1(a8,a4,a6)),
% 181.00/181.23 inference(scs_inference,[],[8693,7821,7363,27])).
% 181.00/181.23 cnf(8856,plain,
% 181.00/181.23 (~P1(a4,a9,a3)),
% 181.00/181.23 inference(scs_inference,[],[8834,8167,8554,8693,7821,7363,8072,7863,7932,7780,1417,18,20,27,28,29,30])).
% 181.00/181.23 cnf(8869,plain,
% 181.00/181.23 (~P1(a8,a8,a6)),
% 181.00/181.23 inference(scs_inference,[],[8848,8470,8564,7919,8559,8072,7932,75,18,28,29,26])).
% 181.00/181.23 cnf(8881,plain,
% 181.00/181.23 (~P1(a5,a4,a3)),
% 181.00/181.23 inference(scs_inference,[],[1,8757,8856,7721,7778,7834,27,26])).
% 181.00/181.23 cnf(8889,plain,
% 181.00/181.23 (P1(x88891,x88891,x88891)),
% 181.00/181.23 inference(rename_variables,[],[19])).
% 181.00/181.23 cnf(8891,plain,
% 181.00/181.23 (~P2(a6,a5,a3)),
% 181.00/181.23 inference(scs_inference,[],[8646,8604,7748,8524,7799,19,27,28])).
% 181.00/181.23 cnf(8896,plain,
% 181.00/181.23 (~P1(a5,a8,a6)),
% 181.00/181.23 inference(scs_inference,[],[8646,8604,8869,8740,8515,7748,8111,8524,7799,7805,19,8889,27,28,29,26])).
% 181.00/181.23 cnf(8913,plain,
% 181.00/181.23 (~P1(a5,a6,a8)),
% 181.00/181.23 inference(scs_inference,[],[8896,7750,19,27])).
% 181.00/181.23 cnf(8914,plain,
% 181.00/181.23 (P1(x89141,x89141,x89141)),
% 181.00/181.23 inference(rename_variables,[],[19])).
% 181.00/181.23 cnf(8921,plain,
% 181.00/181.23 (~P1(a2,a3,a5)),
% 181.00/181.23 inference(scs_inference,[],[8648,8784,8896,8470,7665,7750,7803,6594,1401,19,8914,18,27,28,29,26])).
% 181.00/181.23 cnf(8924,plain,
% 181.00/181.23 (~P1(a2,a1,a4)),
% 181.00/181.23 inference(scs_inference,[],[8648,8784,8896,6388,8470,7665,7750,7803,7963,7746,6594,7805,1401,19,8914,18,27,28,29,26,30])).
% 181.00/181.23 cnf(8932,plain,
% 181.00/181.23 (~P2(a10,a5,a3)),
% 181.00/181.23 inference(scs_inference,[],[8586,8881,7659,7721,8559,18,27,28])).
% 181.00/181.23 cnf(8944,plain,
% 181.00/181.23 (~P2(a6,a7,a2)),
% 181.00/181.23 inference(scs_inference,[],[6448,6210,8562,7874,19,17,27,28])).
% 181.00/181.23 cnf(8951,plain,
% 181.00/181.23 (~P1(a5,a1,a8)),
% 181.00/181.23 inference(scs_inference,[],[8896,7534,19,27])).
% 181.00/181.23 cnf(8957,plain,
% 181.00/181.23 (~P2(a8,a12,a5)),
% 181.00/181.23 inference(scs_inference,[],[7815,8896,6204,8003,7534,8559,7863,19,20,27,28,29])).
% 181.00/181.23 cnf(8959,plain,
% 181.00/181.23 (~P1(a7,a8,a6)),
% 181.00/181.23 inference(scs_inference,[],[7815,8848,8896,6204,7821,7854,8003,7534,8559,7863,19,20,27,28,29,26])).
% 181.00/181.23 cnf(8961,plain,
% 181.00/181.23 (~P2(a7,a6,a7)),
% 181.00/181.23 inference(scs_inference,[],[7815,8848,8896,6204,6104,7821,7854,8003,7534,8562,8559,7863,19,20,27,28,29,26,30])).
% 181.00/181.23 cnf(8964,plain,
% 181.00/181.23 (~P1(a6,a1,a8)),
% 181.00/181.23 inference(scs_inference,[],[8951,7534,19,27])).
% 181.00/181.23 cnf(8967,plain,
% 181.00/181.23 (~P2(a10,a2,a8)),
% 181.00/181.23 inference(scs_inference,[],[8656,8951,8028,7534,19,18,27,28])).
% 181.00/181.23 cnf(8972,plain,
% 181.00/181.23 (~P1(a1,a4,a2)),
% 181.00/181.23 inference(scs_inference,[],[8613,8641,8656,8951,8028,7940,7721,7534,7830,19,18,2,27,28,29,26])).
% 181.00/181.23 cnf(8998,plain,
% 181.00/181.23 (~P1(a9,a4,a7)),
% 181.00/181.23 inference(scs_inference,[],[7843,7807,17,27])).
% 181.00/181.23 cnf(9006,plain,
% 181.00/181.23 (~P1(a9,a10,a5)),
% 181.00/181.23 inference(scs_inference,[],[8519,7843,8683,4879,7921,7807,8003,8562,7863,7805,5,17,27,28,29,26])).
% 181.00/181.23 cnf(9010,plain,
% 181.00/181.23 (~P1(a3,a1,a5)),
% 181.00/181.23 inference(scs_inference,[],[8921,6262,7004,27])).
% 181.00/181.23 cnf(9011,plain,
% 181.00/181.23 (~P1(x90111,x90112,x90113)+P1(x90111,x90114,x90115)+~P1(x90113,x90116,x90115)+~P1(x90112,x90116,x90114)),
% 181.00/181.23 inference(rename_variables,[],[27])).
% 181.00/181.23 cnf(9012,plain,
% 181.00/181.23 (~P2(a2,a8,a6)),
% 181.00/181.23 inference(scs_inference,[],[8921,8944,6262,7004,7874,1390,27,28])).
% 181.00/181.23 cnf(9020,plain,
% 181.00/181.23 (~P2(a4,a2,a4)),
% 181.00/181.23 inference(scs_inference,[],[1,8671,8921,8944,8964,8972,8644,6262,101,7748,7004,7684,7803,7534,7799,7874,1390,3,27,28,29,26,9011,31])).
% 181.00/181.23 cnf(9023,plain,
% 181.00/181.23 (~P2(a9,a5,a6)),
% 181.00/181.23 inference(scs_inference,[],[1,8671,8921,8944,8964,8972,4281,8644,7894,6262,101,7748,7004,7684,7803,7534,7799,7874,1390,17,14,3,27,28,29,26,9011,31,30])).
% 181.00/181.23 cnf(9028,plain,
% 181.00/181.23 (~P1(a8,a5,a6)),
% 181.00/181.23 inference(scs_inference,[],[8913,8528,8515,27])).
% 181.00/181.23 cnf(9030,plain,
% 181.00/181.23 (~P2(a3,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[9012,8913,8528,8515,8028,7746,27,28])).
% 181.00/181.23 cnf(9032,plain,
% 181.00/181.23 (~P2(a8,a8,a2)),
% 181.00/181.23 inference(scs_inference,[],[9020,9012,8913,8528,8515,8028,7746,7780,27,28,29])).
% 181.00/181.23 cnf(9037,plain,
% 181.00/181.23 (~P1(a11,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[9020,9012,8924,8913,8528,8515,7665,8028,7782,7746,7780,19,17,14,27,28,29,26,31])).
% 181.00/181.23 cnf(9044,plain,
% 181.00/181.23 (~P1(a1,a6,a3)),
% 181.00/181.23 inference(scs_inference,[],[8760,1380,19,27])).
% 181.00/181.23 cnf(9047,plain,
% 181.00/181.23 (~P2(a4,a2,a8)),
% 181.00/181.23 inference(scs_inference,[],[7669,8760,7684,1380,19,6,27,28])).
% 181.00/181.23 cnf(9052,plain,
% 181.00/181.23 (~P1(a7,a4,a6)),
% 181.00/181.23 inference(scs_inference,[],[7669,9028,6309,8760,7919,7659,7684,8088,1380,19,18,6,27,28,29,26])).
% 181.00/181.23 cnf(9054,plain,
% 181.00/181.23 (~P2(a10,a6,a2)),
% 181.00/181.23 inference(scs_inference,[],[7669,9037,9028,6309,8760,7919,7659,7684,8088,1380,11,19,18,14,16,6,27,28,29,26,30])).
% 181.00/181.23 cnf(9061,plain,
% 181.00/181.23 (~P1(a2,a1,a6)),
% 181.00/181.23 inference(scs_inference,[],[1,9044,7004,27])).
% 181.00/181.23 cnf(9078,plain,
% 181.00/181.23 (P1(a11,x90781,x90781)),
% 181.00/181.23 inference(rename_variables,[],[17])).
% 181.00/181.23 cnf(9082,plain,
% 181.00/181.23 (~P2(a8,a4,a12)),
% 181.00/181.23 inference(scs_inference,[],[8814,9023,9028,101,8111,6594,7805,17,20,27,28,29])).
% 181.00/181.23 cnf(9085,plain,
% 181.00/181.23 (~P1(a11,a3,a6)),
% 181.00/181.23 inference(scs_inference,[],[9061,8814,9023,9028,101,7665,8111,6594,7805,17,9078,20,27,28,29,26])).
% 181.00/181.23 cnf(9091,plain,
% 181.00/181.23 (~P2(a12,a5,a12)+P2(a5,a10,a12)),
% 181.00/181.23 inference(scs_inference,[],[9061,8814,9023,9028,8505,7744,7449,101,8526,7748,7665,8111,7717,6594,7805,17,9078,19,20,27,28,29,26,30,31])).
% 181.00/181.23 cnf(9102,plain,
% 181.00/181.23 (~P2(a10,a6,a3)),
% 181.00/181.23 inference(scs_inference,[],[1,9010,9054,9085,7782,7665,7534,11,17,18,14,16,27,29,26,30])).
% 181.00/181.23 cnf(9110,plain,
% 181.00/181.23 (~P1(a8,a9,a9)),
% 181.00/181.23 inference(scs_inference,[],[8170,7919,7778,27])).
% 181.00/181.23 cnf(9112,plain,
% 181.00/181.23 (~P2(a10,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[8170,9030,7919,7778,8028,18,27,28])).
% 181.00/181.23 cnf(9127,plain,
% 181.00/181.23 (~P1(a9,a9,a6)),
% 181.00/181.23 inference(scs_inference,[],[7883,19,17,27])).
% 181.00/181.23 cnf(9131,plain,
% 181.00/181.23 (~P2(a10,a3,a5)),
% 181.00/181.23 inference(scs_inference,[],[8932,7883,19,17,18,20,27,29])).
% 181.00/181.23 cnf(9159,plain,
% 181.00/181.23 (~P1(a5,a5,a3)),
% 181.00/181.23 inference(scs_inference,[],[9110,8998,9054,4634,7821,7778,8072,8524,454,19,18,27,29,26,30])).
% 181.00/181.23 cnf(9164,plain,
% 181.00/181.23 (~P1(a7,a3,a8)),
% 181.00/181.23 inference(scs_inference,[],[9110,8566,8998,8839,9054,4634,7821,7778,8072,8524,8088,7863,1373,454,19,18,27,29,26,30,28,31])).
% 181.00/181.23 cnf(9166,plain,
% 181.00/181.23 (~P1(a8,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[8959,7919,7799,27])).
% 181.00/181.23 cnf(9172,plain,
% 181.00/181.23 (~P1(a11,a5,a3)),
% 181.00/181.23 inference(scs_inference,[],[9159,8844,8959,8018,7919,8526,7684,7799,8088,17,19,27,28,29,26])).
% 181.00/181.23 cnf(9180,plain,
% 181.00/181.23 (~P1(a8,a5,a3)),
% 181.00/181.23 inference(scs_inference,[],[9164,8528,7854,27])).
% 181.00/181.23 cnf(9201,plain,
% 181.00/181.23 (~P1(a2,a8,a3)),
% 181.00/181.23 inference(scs_inference,[],[9032,9172,9180,8528,7363,8003,7874,19,17,27,29,26])).
% 181.00/181.23 cnf(9203,plain,
% 181.00/181.23 (~P2(a2,a8,a11)),
% 181.00/181.23 inference(scs_inference,[],[9032,9172,9180,4794,8528,7363,8003,7932,7874,59,19,17,27,29,26,30])).
% 181.00/181.23 cnf(9207,plain,
% 181.00/181.23 (~P1(a7,a4,a3)),
% 181.00/181.23 inference(scs_inference,[],[9201,6915,7919,27])).
% 181.00/181.23 cnf(9211,plain,
% 181.00/181.23 (~P1(a2,a4,a6)),
% 181.00/181.23 inference(scs_inference,[],[9203,9052,9201,7852,6915,7919,7807,6569,7663,27,29,26])).
% 181.00/181.23 cnf(9217,plain,
% 181.00/181.23 (~P2(a5,a7,a8)),
% 181.00/181.23 inference(scs_inference,[],[9203,9052,9201,4698,7852,6915,7919,7807,6569,8559,7746,7663,7932,27,29,26,30,1469,81])).
% 181.00/181.23 cnf(9219,plain,
% 181.00/181.23 (~P1(a7,a9,a9)),
% 181.00/181.23 inference(scs_inference,[],[5037,6891,17,27])).
% 181.00/181.23 cnf(9226,plain,
% 181.00/181.23 (~P1(x92261,a10,a4)),
% 181.00/181.23 inference(scs_inference,[],[8408,5037,4826,6891,11,13,17,18,20,27,29,26])).
% 181.00/181.23 cnf(9229,plain,
% 181.00/181.23 (~P1(a10,a7,a4)),
% 181.00/181.23 inference(scs_inference,[],[8408,5037,4826,6891,11,13,17,18,20,27,29,26,2137])).
% 181.00/181.23 cnf(9230,plain,
% 181.00/181.23 (~P1(a10,a8,a4)),
% 181.00/181.23 inference(scs_inference,[],[8408,5037,4826,6891,11,13,17,18,20,27,29,26,2137,6752])).
% 181.00/181.23 cnf(9231,plain,
% 181.00/181.23 (~P1(a10,a2,a4)),
% 181.00/181.23 inference(scs_inference,[],[8408,5037,4826,6891,11,13,17,18,20,27,29,26,2137,6752,1203])).
% 181.00/181.23 cnf(9239,plain,
% 181.00/181.23 (~P1(a10,a12,a4)),
% 181.00/181.23 inference(scs_inference,[],[9226,1134])).
% 181.00/181.23 cnf(9240,plain,
% 181.00/181.23 (~P1(x92401,a10,a4)),
% 181.00/181.23 inference(rename_variables,[],[9226])).
% 181.00/181.23 cnf(9242,plain,
% 181.00/181.23 (~P1(a10,a1,a4)),
% 181.00/181.23 inference(scs_inference,[],[9226,9240,1134,1121])).
% 181.00/181.23 cnf(9243,plain,
% 181.00/181.23 (~P1(x92431,a10,a4)),
% 181.00/181.23 inference(rename_variables,[],[9226])).
% 181.00/181.23 cnf(9245,plain,
% 181.00/181.23 (~P1(a10,a6,a4)),
% 181.00/181.23 inference(scs_inference,[],[9226,9240,9243,1134,1121,1160])).
% 181.00/181.23 cnf(9246,plain,
% 181.00/181.23 (~P1(x92461,a10,a4)),
% 181.00/181.23 inference(rename_variables,[],[9226])).
% 181.00/181.23 cnf(9249,plain,
% 181.00/181.23 (~P1(x92491,a10,a4)),
% 181.00/181.23 inference(rename_variables,[],[9226])).
% 181.00/181.23 cnf(9251,plain,
% 181.00/181.23 (~P1(a5,a5,a10)),
% 181.00/181.23 inference(scs_inference,[],[9226,9240,9243,9246,9249,7659,1134,1121,1160,1147,27])).
% 181.00/181.23 cnf(9259,plain,
% 181.00/181.23 (~P1(a12,a8,a4)),
% 181.00/181.23 inference(scs_inference,[],[9217,9230,9226,9240,9243,9246,9249,9131,7659,7876,7854,8562,7874,18,1134,1121,1160,1147,27,28,29,26])).
% 181.00/181.23 cnf(9261,plain,
% 181.00/181.23 (~P2(a8,a8,a3)),
% 181.00/181.23 inference(scs_inference,[],[9207,9217,9230,9226,9240,9243,9246,9249,9131,7659,7876,7919,7854,8562,7863,7874,7780,18,1134,1121,1160,1147,27,28,29,26,30])).
% 181.00/181.23 cnf(9263,plain,
% 181.00/181.23 (~P1(a10,a5,a4)),
% 181.00/181.23 inference(scs_inference,[],[9207,9217,9230,9226,9240,9243,9246,9249,9131,7659,7876,7919,7854,8562,7863,7874,7780,18,1134,1121,1160,1147,27,28,29,26,30,1095])).
% 181.00/181.23 cnf(9265,plain,
% 181.00/181.23 (~P2(a10,a4,a10)),
% 181.00/181.23 inference(scs_inference,[],[9263,7480])).
% 181.00/181.23 cnf(9266,plain,
% 181.00/181.23 (~P1(a4,a10,a5)),
% 181.00/181.23 inference(scs_inference,[],[9251,7721,11,27])).
% 181.00/181.23 cnf(9273,plain,
% 181.00/181.23 (~P2(a2,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[1,9229,9251,8719,9044,6308,7721,7748,75,11,18,16,27,26,29,30])).
% 181.00/181.23 cnf(9277,plain,
% 181.00/181.23 (~P2(a2,a7,a6)),
% 181.00/181.23 inference(scs_inference,[],[1,9229,9251,8719,9044,6308,7721,7748,75,11,18,16,27,26,29,30,182])).
% 181.00/181.23 cnf(9284,plain,
% 181.00/181.23 (~P2(a10,a10,a4)),
% 181.00/181.23 inference(scs_inference,[],[1,9265,9277,9172,8003,17,18,9,27,28,29])).
% 181.00/181.23 cnf(9290,plain,
% 181.00/181.23 (~P2(a8,a7,a9)),
% 181.00/181.23 inference(scs_inference,[],[1,9219,9265,9231,9277,9172,6891,8003,7932,7863,5,17,18,9,27,28,29,26,30])).
% 181.00/181.23 cnf(9294,plain,
% 181.00/181.23 (~P1(a3,a11,a5)),
% 181.00/181.23 inference(scs_inference,[],[1,9219,9265,9231,9277,9172,6891,8003,7932,7863,5,17,18,9,27,28,29,26,30,507,89])).
% 181.00/181.23 cnf(9296,plain,
% 181.00/181.23 (~P1(a2,a3,a8)),
% 181.00/181.23 inference(scs_inference,[],[9201,6262,19,27])).
% 181.00/181.23 cnf(9305,plain,
% 181.00/181.23 (~P1(a6,a8,a4)),
% 181.00/181.23 inference(scs_inference,[],[9263,9273,9201,9054,8528,6339,6262,8003,8088,19,18,16,27,28,29,26])).
% 181.00/181.23 cnf(9311,plain,
% 181.00/181.23 (~P2(a8,a5,a8)),
% 181.00/181.23 inference(scs_inference,[],[9266,8957,7778,8526,7803,4,27,28])).
% 181.00/181.23 cnf(9318,plain,
% 181.00/181.23 (~P2(a5,a8,a11)),
% 181.00/181.23 inference(scs_inference,[],[9239,9266,8891,8957,3334,7778,8526,7803,1574,8562,4,19,17,14,27,28,29,26,30])).
% 181.00/181.23 cnf(9322,plain,
% 181.00/181.23 (~P2(a4,a8,a11)),
% 181.00/181.23 inference(scs_inference,[],[9239,9266,8891,8957,3334,7778,8526,7803,1574,8562,4,19,17,14,27,28,29,26,30,835])).
% 181.00/181.23 cnf(9329,plain,
% 181.00/181.23 (~P1(a8,a4,a3)),
% 181.00/181.23 inference(scs_inference,[],[9296,7821,7363,27])).
% 181.00/181.23 cnf(9338,plain,
% 181.00/181.23 (~P2(a2,a3,a6)),
% 181.00/181.23 inference(scs_inference,[],[1,9242,9284,9296,9318,9044,7821,7848,7363,7661,8559,53,8562,7805,18,20,27,28,29,26,30])).
% 181.00/181.23 cnf(9341,plain,
% 181.00/181.23 (~P1(a11,a7,a9)),
% 181.00/181.23 inference(scs_inference,[],[1,9242,9284,9296,9318,9044,6200,7821,7848,7363,7661,7684,8559,53,8562,7805,17,18,14,20,27,28,29,26,30,31])).
% 181.00/181.23 cnf(9348,plain,
% 181.00/181.23 (~P1(a2,a4,a3)),
% 181.00/181.23 inference(scs_inference,[],[9296,7834,19,27])).
% 181.00/181.23 cnf(9351,plain,
% 181.00/181.23 (~P2(a2,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[9338,9296,7834,8072,7746,19,27,28])).
% 181.00/181.23 cnf(9355,plain,
% 181.00/181.23 (~P1(a8,a7,a6)),
% 181.00/181.23 inference(scs_inference,[],[9338,9166,8957,9296,7942,7834,8072,7746,8060,7805,59,19,27,28,29,26])).
% 181.00/181.23 cnf(9363,plain,
% 181.00/181.23 (~P2(a12,a5,a12)),
% 181.00/181.23 inference(scs_inference,[],[9127,9338,9166,8957,9296,7784,7942,7834,8111,7830,8072,7746,8060,7805,72,59,454,19,27,28,29,26,30,31,787,9091])).
% 181.00/181.23 cnf(9364,plain,
% 181.00/181.23 (~P2(a4,a10,a10)),
% 181.00/181.23 inference(scs_inference,[],[9127,9338,9166,8957,9296,7784,7942,7834,8111,7830,8072,7746,8060,7805,72,59,454,19,27,28,29,26,30,31,787,9091,814])).
% 181.00/181.23 cnf(9366,plain,
% 181.00/181.23 (~P2(a4,a10,a12)),
% 181.00/181.23 inference(scs_inference,[],[9127,9338,9166,8957,9296,7784,7942,7834,8111,7830,8072,7746,8060,7805,72,59,454,19,27,28,29,26,30,31,787,9091,814,825])).
% 181.00/181.23 cnf(9368,plain,
% 181.00/181.23 (~P1(a12,a12,a4)),
% 181.00/181.23 inference(scs_inference,[],[9363,3288])).
% 181.00/181.23 cnf(9372,plain,
% 181.00/181.23 (~P2(a10,a7,a9)),
% 181.00/181.23 inference(scs_inference,[],[9305,9290,7821,6339,7874,18,27,28])).
% 181.00/181.23 cnf(9375,plain,
% 181.00/181.23 (~P2(a5,a6,a8)),
% 181.00/181.23 inference(scs_inference,[],[9311,9305,9290,7821,6339,8526,7717,7874,18,27,28,29])).
% 181.00/181.23 cnf(9377,plain,
% 181.00/181.23 (~P1(a3,a2,a5)),
% 181.00/181.23 inference(scs_inference,[],[9294,9311,9305,9290,7821,6339,8526,7717,34,7874,18,15,27,28,29,26])).
% 181.00/181.23 cnf(9384,plain,
% 181.00/181.23 (~P1(a9,a9,a7)),
% 181.00/181.23 inference(scs_inference,[],[9341,19,17,27])).
% 181.00/181.23 cnf(9386,plain,
% 181.00/181.23 (P1(a11,x93861,x93861)),
% 181.00/181.23 inference(rename_variables,[],[17])).
% 181.00/181.23 cnf(9396,plain,
% 181.00/181.23 (~P1(a9,a4,a10)),
% 181.00/181.23 inference(scs_inference,[],[1,9377,8841,9341,7917,7004,7863,7874,19,17,9386,14,27,29,26,30,243])).
% 181.00/181.23 cnf(9397,plain,
% 181.00/181.23 (~P2(a2,a10,a9)),
% 181.00/181.23 inference(scs_inference,[],[1,9377,8841,9341,7917,7004,7863,7874,19,17,9386,14,27,29,26,30,243,144])).
% 181.00/181.23 cnf(9399,plain,
% 181.00/181.23 (~P2(a2,a7,a9)),
% 181.00/181.23 inference(scs_inference,[],[1,9377,8841,9341,7917,7004,7863,7874,19,17,9386,14,27,29,26,30,243,144,185])).
% 181.00/181.23 cnf(9401,plain,
% 181.00/181.23 (~P2(a9,a10,a7)),
% 181.00/181.23 inference(scs_inference,[],[1,9377,8841,9341,7917,7004,7863,7874,19,17,9386,14,27,29,26,30,243,144,185,1646])).
% 181.00/181.23 cnf(9403,plain,
% 181.00/181.23 (~P1(a5,a4,a10)),
% 181.00/181.23 inference(scs_inference,[],[9226,7721,19,27])).
% 181.00/181.23 cnf(9407,plain,
% 181.00/181.23 (~P2(a3,a2,a9)),
% 181.00/181.23 inference(scs_inference,[],[9399,9226,7721,8028,1390,19,27,28])).
% 181.00/181.23 cnf(9418,plain,
% 181.00/181.23 (~P1(a1,a8,a4)),
% 181.00/181.23 inference(scs_inference,[],[9403,6339,7534,27])).
% 181.00/181.23 cnf(9423,plain,
% 181.00/181.23 (~P1(a5,a12,a4)),
% 181.00/181.23 inference(scs_inference,[],[9368,9403,9351,6339,7784,7534,1401,19,20,27,28,26])).
% 181.00/181.23 cnf(9430,plain,
% 181.00/181.23 (~P2(a7,a9,a7)),
% 181.00/181.23 inference(scs_inference,[],[9368,9401,9403,9351,5680,7988,6339,7784,7534,7803,1572,1401,19,17,14,15,20,27,28,26,30,31])).
% 181.00/181.23 cnf(9433,plain,
% 181.00/181.23 (~P1(a4,a5,a12)),
% 181.00/181.23 inference(scs_inference,[],[9423,7659,7721,27])).
% 181.00/181.23 cnf(9441,plain,
% 181.00/181.23 (~P1(a9,a5,a10)),
% 181.00/181.23 inference(scs_inference,[],[9396,9423,9364,9329,9375,7659,7821,7921,7721,7830,8524,8559,7805,4,8,27,28,26,30,31])).
% 181.00/181.23 cnf(9443,plain,
% 181.00/181.23 (~P1(a9,a12,a4)),
% 181.00/181.23 inference(scs_inference,[],[9396,9423,9364,9329,9375,7659,7821,7921,7721,7830,8524,8559,7805,4,8,27,28,26,30,31,3287])).
% 181.00/181.23 cnf(9451,plain,
% 181.00/181.23 (~P2(a8,a9,a7)),
% 181.00/181.23 inference(scs_inference,[],[9443,9430,7917,7807,7874,19,27,28])).
% 181.00/181.23 cnf(9460,plain,
% 181.00/181.23 (P2(x94601,a10,x94601)),
% 181.00/181.23 inference(rename_variables,[],[16])).
% 181.00/181.23 cnf(9462,plain,
% 181.00/181.23 (~P2(a10,a8,a2)),
% 181.00/181.23 inference(scs_inference,[],[8967,9397,7782,18,20,16,28,29])).
% 181.00/181.23 cnf(9463,plain,
% 181.00/181.23 (P2(a10,x94631,x94631)),
% 181.00/181.23 inference(rename_variables,[],[18])).
% 181.00/181.23 cnf(9468,plain,
% 181.00/181.23 (~P2(a12,a10,a5)),
% 181.00/181.23 inference(scs_inference,[],[8967,9441,9397,9355,6915,7782,7799,4,18,9463,20,16,9460,28,29,26,30])).
% 181.00/181.23 cnf(9474,plain,
% 181.00/181.23 (~P1(a9,a9,a8)),
% 181.00/181.23 inference(scs_inference,[],[8094,19,27])).
% 181.00/181.23 cnf(9480,plain,
% 181.00/181.23 (P2(a10,x94801,x94801)),
% 181.00/181.23 inference(rename_variables,[],[18])).
% 181.00/181.23 cnf(9482,plain,
% 181.00/181.23 (~P2(a8,a3,a8)),
% 181.00/181.23 inference(scs_inference,[],[9407,9462,8094,8028,8072,19,18,9480,27,28,29])).
% 181.00/181.23 cnf(9502,plain,
% 181.00/181.23 (~P2(a3,a8,a8)),
% 181.00/181.23 inference(scs_inference,[],[9462,8088,18,29])).
% 181.00/181.23 cnf(9503,plain,
% 181.00/181.23 (P2(a10,x95031,x95031)),
% 181.00/181.23 inference(rename_variables,[],[18])).
% 181.00/181.23 cnf(9513,plain,
% 181.00/181.23 (~P1(a8,a9,a2)),
% 181.00/181.23 inference(scs_inference,[],[9474,9006,9462,7921,8088,11,17,18,9503,16,29,26,30,1781])).
% 181.00/181.23 cnf(9519,plain,
% 181.00/181.23 (~P1(a4,a11,a12)),
% 181.00/181.23 inference(scs_inference,[],[9433,7744,17,27])).
% 181.00/181.23 cnf(9534,plain,
% 181.00/181.23 (~P1(a5,a4,a12)),
% 181.00/181.23 inference(scs_inference,[],[9423,7721,19,27])).
% 181.00/181.23 cnf(9541,plain,
% 181.00/181.23 (~P1(a12,a6,a4)),
% 181.00/181.23 inference(scs_inference,[],[9102,9245,9423,7721,7807,4,19,18,20,27,29,26])).
% 181.00/181.23 cnf(9548,plain,
% 181.00/181.23 (~P1(a12,a5,a4)),
% 181.00/181.23 inference(scs_inference,[],[9534,7744,7784,27])).
% 181.00/181.23 cnf(9561,plain,
% 181.00/181.23 (~P1(a12,a11,a4)),
% 181.00/181.23 inference(scs_inference,[],[9548,7659,17,27])).
% 181.00/181.23 cnf(9564,plain,
% 181.00/181.23 (~P1(a2,a4,a2)),
% 181.00/181.23 inference(scs_inference,[],[9548,9513,7659,7834,7778,17,27,26])).
% 181.00/181.23 cnf(9578,plain,
% 181.00/181.23 (~P2(a7,a8,a9)),
% 181.00/181.23 inference(scs_inference,[],[9519,9047,9384,7778,8060,7932,7874,1401,454,19,15,26,29,27,30])).
% 181.00/181.23 cnf(9580,plain,
% 181.00/181.23 (~P1(x95801,a8,a2)),
% 181.00/181.23 inference(scs_inference,[],[9564,7821,26])).
% 181.00/181.23 cnf(9592,plain,
% 181.00/181.23 (~P2(a2,a9,a4)),
% 181.00/181.23 inference(scs_inference,[],[9322,7852,7932,28])).
% 181.00/181.23 cnf(9634,plain,
% 181.00/181.23 (~P1(a10,a9,a4)),
% 181.00/181.23 inference(scs_inference,[],[9259,9592,7449,7942,7940,8088,28,27])).
% 181.00/181.23 cnf(9640,plain,
% 181.00/181.23 (~P2(a8,a4,a8)),
% 181.00/181.23 inference(scs_inference,[],[2,9259,9366,9418,9592,9578,7449,7942,7940,7661,8111,7830,8088,7863,8,4,28,27,31,30,29])).
% 181.00/181.23 cnf(9653,plain,
% 181.00/181.23 (~P2(a7,a4,a7)),
% 181.00/181.23 inference(scs_inference,[],[2,9640,9541,4726,7659,7830,7780,7805,17,18,14,28,29,27,30,8404])).
% 181.00/181.23 cnf(9654,plain,
% 181.00/181.23 (~P1(a12,a2,a4)),
% 181.00/181.23 inference(scs_inference,[],[2,9640,9561,9541,4726,7715,7659,7830,7780,7805,17,18,14,15,28,29,27,30,8404,26])).
% 181.00/181.23 cnf(9657,plain,
% 181.00/181.23 (~P2(a2,a4,a2)),
% 181.00/181.23 inference(scs_inference,[],[2,9640,9561,9541,4726,7715,7659,7830,7780,7805,17,18,14,15,28,29,27,30,8404,26,7892])).
% 181.00/181.23 cnf(9660,plain,
% 181.00/181.23 (~P2(a10,a8,a3)),
% 181.00/181.23 inference(scs_inference,[],[9261,9329,7919,75,18,20,26,28])).
% 181.00/181.23 cnf(9670,plain,
% 181.00/181.23 (~P1(a6,a5,a8)),
% 181.00/181.23 inference(scs_inference,[],[9653,8034,9261,5674,9329,8896,101,7750,7919,7746,8559,8562,75,7863,18,20,26,28,29,30,31,27])).
% 181.00/181.23 cnf(9672,plain,
% 181.00/181.23 (~P1(a6,a11,a8)),
% 181.00/181.23 inference(scs_inference,[],[9670,1893])).
% 181.00/181.23 cnf(9688,plain,
% 181.00/181.23 (~P1(a10,a5,a6)),
% 181.00/181.23 inference(scs_inference,[],[2,9657,8708,9672,6308,8528,8088,7805,15,26,28,27])).
% 181.00/181.23 cnf(9693,plain,
% 181.00/181.23 (~P1(a8,a6,a6)),
% 181.00/181.23 inference(scs_inference,[],[2,9688,5,26])).
% 181.00/181.23 cnf(9698,plain,
% 181.00/181.23 (~P1(a8,a9,a3)),
% 181.00/181.23 inference(scs_inference,[],[2,9082,9688,9296,7363,7942,7805,5,18,26,28,27])).
% 181.00/181.23 cnf(9707,plain,
% 181.00/181.23 (~P1(a5,a10,a3)),
% 181.00/181.23 inference(scs_inference,[],[2,8453,9580,8072,8524,11,18,26,30])).
% 181.00/181.23 cnf(9715,plain,
% 181.00/181.23 (~P1(a8,a12,a3)),
% 181.00/181.23 inference(scs_inference,[],[9707,8515,1574,27])).
% 181.00/181.23 cnf(9740,plain,
% 181.00/181.23 (~P1(a10,a9,a5)),
% 181.00/181.23 inference(scs_inference,[],[8697,6308,7942,27])).
% 181.00/181.23 cnf(9742,plain,
% 181.00/181.23 (~P2(a6,a5,a8)),
% 181.00/181.23 inference(scs_inference,[],[8697,9375,6308,7942,7748,7717,27,28])).
% 181.00/181.23 cnf(9751,plain,
% 181.00/181.23 (~P1(a3,a1,a4)),
% 181.00/181.23 inference(scs_inference,[],[9348,6262,7004,27])).
% 181.00/181.23 cnf(9755,plain,
% 181.00/181.23 (~P1(a5,a9,a10)),
% 181.00/181.23 inference(scs_inference,[],[3,9348,9468,9698,6262,7004,6891,7803,7,15,27,26,31])).
% 181.00/181.23 cnf(9771,plain,
% 181.00/181.23 (~P1(x97711,a12,a5)),
% 181.00/181.23 inference(scs_inference,[],[9755,7312,11,26])).
% 181.00/181.23 cnf(9787,plain,
% 181.00/181.23 (~P1(a1,a3,a4)),
% 181.00/181.23 inference(scs_inference,[],[9771,9751,7744,1376,7004,7784,27,26])).
% 181.00/181.23 cnf(9805,plain,
% 181.00/181.23 (~P1(a10,a1,a5)),
% 181.00/181.23 inference(scs_inference,[],[9740,9742,9259,9670,101,7834,7721,7748,7717,11,13,18,20,27,28,26,30,1121])).
% 181.00/181.23 cnf(9834,plain,
% 181.00/181.23 (P1(a11,x98341,x98341)),
% 181.00/181.23 inference(rename_variables,[],[17])).
% 181.00/181.23 cnf(9838,plain,
% 181.00/181.23 (~P1(a11,a8,a4)),
% 181.00/181.23 inference(scs_inference,[],[9805,9634,9657,7876,7782,7778,17,9834,14,27,26,31])).
% 181.00/181.23 cnf(9848,plain,
% 181.00/181.23 (~P1(a8,a10,a3)),
% 181.00/181.23 inference(scs_inference,[],[4,9715,7764,7942,13,27,26])).
% 181.00/181.23 cnf(9892,plain,
% 181.00/181.23 (~P1(a2,a10,a3)),
% 181.00/181.23 inference(scs_inference,[],[9848,7363,11,26])).
% 181.00/181.23 cnf(9901,plain,
% 181.00/181.23 (~P1(a2,a1,a10)),
% 181.00/181.23 inference(scs_inference,[],[9892,7665,19,27])).
% 181.00/181.23 cnf(9913,plain,
% 181.00/181.23 (~P1(a9,a7,a6)),
% 181.00/181.23 inference(scs_inference,[],[9787,8699,6915,6262,59,1,27,26])).
% 181.00/181.23 cnf(9921,plain,
% 181.00/181.23 (~P2(a4,a6,a12)),
% 181.00/181.23 inference(scs_inference,[],[9787,8699,9771,6915,6262,7748,7717,59,19,1,27,26,30,814,825])).
% 181.00/181.23 cnf(9927,plain,
% 181.00/181.23 (~P1(a4,a5,a8)),
% 181.00/181.23 inference(scs_inference,[],[9838,7659,17,27])).
% 181.00/181.23 cnf(9932,plain,
% 181.00/181.23 (~P1(a2,a5,a5)),
% 181.00/181.23 inference(scs_inference,[],[9838,7659,17,27,8575,8686])).
% 181.00/181.23 cnf(9940,plain,
% 181.00/181.23 (~P1(a9,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[9927,7778,450,27])).
% 181.00/181.23 cnf(9942,plain,
% 181.00/181.23 (~P1(a2,a3,a10)),
% 181.00/181.23 inference(scs_inference,[],[9927,9901,7665,7778,450,19,27,26])).
% 181.00/181.23 cnf(9956,plain,
% 181.00/181.23 (~P1(a11,a12,a4)),
% 181.00/181.23 inference(scs_inference,[],[9913,9654,9657,7715,6891,1401,454,17,334,14,27,26,31])).
% 181.00/181.23 cnf(9976,plain,
% 181.00/181.23 (~P1(a11,a8,a6)),
% 181.00/181.23 inference(scs_inference,[],[9211,7834,17,26])).
% 181.00/181.23 cnf(9981,plain,
% 181.00/181.23 (~P2(a9,a4,a7)),
% 181.00/181.23 inference(scs_inference,[],[9211,9451,9942,6915,7834,7940,7830,1572,17,26,27,29])).
% 181.00/181.23 cnf(9994,plain,
% 181.00/181.23 (~P1(a4,a4,a2)),
% 181.00/181.23 inference(scs_inference,[],[6728,6569,7778,27])).
% 181.00/181.23 cnf(9996,plain,
% 181.00/181.23 (~P2(a6,a10,a8)),
% 181.00/181.23 inference(scs_inference,[],[9976,6728,6569,7778,17,18,14,27,30])).
% 181.00/181.23 cnf(10005,plain,
% 181.00/181.23 (~P1(a5,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[9927,7659,450,27])).
% 181.00/181.23 cnf(10032,plain,
% 181.00/181.23 (~P1(a10,a6,a6)),
% 181.00/181.23 inference(scs_inference,[],[5,9693,1380,27])).
% 181.00/181.23 cnf(10036,plain,
% 181.00/181.23 (~P2(a8,a6,a8)),
% 181.00/181.23 inference(scs_inference,[],[5,9693,10005,9981,8515,1380,8562,7717,7830,1385,27,28,30])).
% 181.00/181.23 cnf(10038,plain,
% 181.00/181.23 (~P1(a6,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[10032,6339,53,26])).
% 181.00/181.23 cnf(10040,plain,
% 181.00/181.23 (~P1(a6,a7,a9)),
% 181.00/181.23 inference(scs_inference,[],[10032,9305,6339,7919,53,7807,26,27])).
% 181.00/181.23 cnf(10042,plain,
% 181.00/181.23 (~P2(x100421,a5,a8)),
% 181.00/181.23 inference(scs_inference,[],[10036,10032,9305,6339,7919,53,7807,7717,26,27,28])).
% 181.00/181.23 cnf(10044,plain,
% 181.00/181.23 (~P2(a2,a5,a2)),
% 181.00/181.23 inference(scs_inference,[],[10036,9932,10032,9305,6339,7919,7363,53,7807,8526,8524,7717,26,27,28,30])).
% 181.00/181.23 cnf(10046,plain,
% 181.00/181.23 (~P1(a8,a12,a6)),
% 181.00/181.23 inference(scs_inference,[],[9688,7744,1574,26])).
% 181.00/181.23 cnf(10052,plain,
% 181.00/181.23 (~P2(a4,a5,a12)),
% 181.00/181.23 inference(scs_inference,[],[9956,9921,9688,7744,1574,8559,7780,19,17,26,27,28])).
% 181.00/181.23 cnf(10054,plain,
% 181.00/181.23 (~P2(a12,a12,a5)),
% 181.00/181.23 inference(scs_inference,[],[9956,10044,9921,9688,7744,1574,7663,8559,7780,19,17,26,27,28,29])).
% 181.00/181.23 cnf(10060,plain,
% 181.00/181.23 (~P1(a8,a2,a5)),
% 181.00/181.23 inference(scs_inference,[],[9940,7921,1388,27])).
% 181.00/181.23 cnf(10061,plain,
% 181.00/181.23 (~P1(x100611,x100612,x100613)+P1(x100611,x100614,x100615)+~P1(x100613,x100616,x100615)+~P1(x100612,x100616,x100614)),
% 181.00/181.23 inference(rename_variables,[],[27])).
% 181.00/181.23 cnf(10064,plain,
% 181.00/181.23 (~P2(a3,a10,a10)),
% 181.00/181.23 inference(scs_inference,[],[10052,9502,9940,7921,1388,6594,7805,18,27,28,29])).
% 181.00/181.23 cnf(10070,plain,
% 181.00/181.23 (~P2(a5,a4,a8)),
% 181.00/181.23 inference(scs_inference,[],[5,10052,9502,9940,10046,10005,7921,1388,6594,7805,72,19,18,27,28,29,10061,30])).
% 181.00/181.23 cnf(10086,plain,
% 181.00/181.23 (~P1(a8,a8,a5)),
% 181.00/181.23 inference(scs_inference,[],[10060,10070,7821,7799,1872,26])).
% 181.00/181.23 cnf(10098,plain,
% 181.00/181.23 (~P2(a10,a3,a10)),
% 181.00/181.23 inference(scs_inference,[],[10064,10086,7363,7661,7799,11,26,31])).
% 181.00/181.23 cnf(10132,plain,
% 181.00/181.23 (~P1(a4,a3,a3)),
% 181.00/181.23 inference(scs_inference,[],[10040,10098,9482,9848,9164,7848,7921,7799,8088,1572,7863,7780,11,18,16,26,29,30,1842,27,31])).
% 181.00/181.23 cnf(10144,plain,
% 181.00/181.23 (~P1(a8,a5,a5)),
% 181.00/181.23 inference(scs_inference,[],[9112,9927,16,8528,450,18,29,27])).
% 181.00/181.23 cnf(10234,plain,
% 181.00/181.23 (~P1(a3,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[8708,7896,7004,26])).
% 181.00/181.23 cnf(10236,plain,
% 181.00/181.23 (~P1(a5,a6,a10)),
% 181.00/181.23 inference(scs_inference,[],[10038,8708,101,7896,7004,19,26,27])).
% 181.00/181.23 cnf(10244,plain,
% 181.00/181.23 (~P2(a10,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[8961,16,29])).
% 181.00/181.23 cnf(10248,plain,
% 181.00/181.23 (~P1(a12,a7,a6)),
% 181.00/181.23 inference(scs_inference,[],[8961,10236,16,7876,7784,29,27])).
% 181.00/181.23 cnf(10254,plain,
% 181.00/181.23 (~P1(a5,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[10248,7876,7784,26])).
% 181.00/181.23 cnf(10261,plain,
% 181.00/181.23 (P2(x102611,a10,x102611)),
% 181.00/181.23 inference(rename_variables,[],[16])).
% 181.00/181.23 cnf(10265,plain,
% 181.00/181.23 (~P2(a2,a10,x102651)+~P2(a8,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[10244,9994,10248,10132,6339,16,10261,7876,7784,7665,8072,7780,56,19,26,27,30,29,24,31])).
% 181.00/181.23 cnf(10272,plain,
% 181.00/181.23 (~P1(a8,a4,a5)),
% 181.00/181.23 inference(scs_inference,[],[10144,7821,16,7659,10265,26])).
% 181.00/181.23 cnf(10284,plain,
% 181.00/181.23 (~P1(a11,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[10254,11,17,26])).
% 181.00/181.23 cnf(10292,plain,
% 181.00/181.23 (~P1(a10,a12,a6)),
% 181.00/181.23 inference(scs_inference,[],[9372,10234,10254,6308,16,1574,11,17,18,26,29,27])).
% 181.00/181.23 cnf(10305,plain,
% 181.00/181.23 (P1(a11,x103051,x103051)),
% 181.00/181.23 inference(rename_variables,[],[17])).
% 181.00/181.23 cnf(10313,plain,
% 181.00/181.23 (~P1(a6,a11,a10)),
% 181.00/181.23 inference(scs_inference,[],[10292,10284,4858,101,7896,16,1574,17,10305,18,26,27,30,6630,1893])).
% 181.00/181.23 cnf(10335,plain,
% 181.00/181.23 (~P1(x103351,a10,a6)),
% 181.00/181.23 inference(scs_inference,[],[10313,11,13,26])).
% 181.00/181.23 cnf(10344,plain,
% 181.00/181.23 (~P1(a10,a1,a6)),
% 181.00/181.23 inference(scs_inference,[],[10272,9660,10313,7821,7778,16,11,13,18,26,29,27,1121])).
% 181.00/181.23 cnf(10352,plain,
% 181.00/181.23 (~P1(a10,a2,a6)),
% 181.00/181.23 inference(scs_inference,[],[10272,9660,10313,10042,7719,7821,7778,16,11,13,18,26,29,27,1121,1147,28,7071,1081])).
% 181.00/181.23 cnf(10356,plain,
% 181.00/181.23 (~P1(a6,a1,a10)),
% 181.00/181.23 inference(scs_inference,[],[10335,3021])).
% 181.00/181.23 cnf(10363,plain,
% 181.00/181.23 (~P1(a12,a9,a6)),
% 181.00/181.23 inference(scs_inference,[],[9996,10352,10236,1388,7312,6339,7784,16,18,28,26,27])).
% 181.00/181.23 cnf(10382,plain,
% 181.00/181.23 (~P1(a6,a6,a10)),
% 181.00/181.23 inference(scs_inference,[],[10356,101,7534,26])).
% 181.00/181.23 cnf(10393,plain,
% 181.00/181.23 (P1(x103931,x103931,x103931)),
% 181.00/181.23 inference(rename_variables,[],[19])).
% 181.00/181.23 cnf(10401,plain,
% 181.00/181.23 (~P1(a2,a6,a5)),
% 181.00/181.23 inference(scs_inference,[],[10363,10054,7696,9932,6569,7312,8526,7746,16,8562,1417,19,10393,26,29,27,30])).
% 181.00/181.23 cnf(10632,plain,
% 181.00/181.23 (~P2(a7,a5,a11)),
% 181.00/181.23 inference(scs_inference,[],[7649,8559,7863,28])).
% 181.00/181.23 cnf(10663,plain,
% 181.00/181.23 (~P1(x106631,a8,a6)),
% 181.00/181.23 inference(scs_inference,[],[10382,53,11,26])).
% 181.00/181.23 cnf(10692,plain,
% 181.00/181.23 (P1(a11,x106921,x106921)),
% 181.00/181.23 inference(rename_variables,[],[17])).
% 181.00/181.23 cnf(10698,plain,
% 181.00/181.23 (~P2(a4,a6,a11)),
% 181.00/181.23 inference(scs_inference,[],[10344,3334,7848,7748,17,10692,14,27,30,835])).
% 181.00/181.23 cnf(10750,plain,
% 181.00/181.23 (~P1(a1,a1,a6)),
% 181.00/181.23 inference(scs_inference,[],[3942,19,27])).
% 181.00/181.23 cnf(10793,plain,
% 181.00/181.23 (~P1(a4,a9,a8)),
% 181.00/181.23 inference(scs_inference,[],[9838,7778,17,27])).
% 181.00/181.23 cnf(10799,plain,
% 181.00/181.23 (~P2(a8,a12,a2)),
% 181.00/181.23 inference(scs_inference,[],[3879,9838,4601,7778,8060,7932,7780,17,27,30,29])).
% 181.00/181.23 cnf(10806,plain,
% 181.00/181.23 (~P1(a9,a8,a4)),
% 181.00/181.23 inference(scs_inference,[],[10793,7921,7942,26])).
% 181.00/181.23 cnf(10825,plain,
% 181.00/181.23 (~P1(a12,a4,a6)),
% 181.00/181.23 inference(scs_inference,[],[10663,7834,7715,27])).
% 181.00/181.23 cnf(10828,plain,
% 181.00/181.23 (~P2(a10,a3,a12)),
% 181.00/181.23 inference(scs_inference,[],[10799,10663,7834,7715,8072,16,27,29])).
% 181.00/181.23 cnf(10837,plain,
% 181.00/181.23 (~P1(a9,a4,a8)),
% 181.00/181.23 inference(scs_inference,[],[10806,7807,19,27])).
% 181.00/181.23 cnf(10844,plain,
% 181.00/181.23 (~P2(a12,a10,a3)),
% 181.00/181.23 inference(scs_inference,[],[10828,16,18,29])).
% 181.00/181.23 cnf(10865,plain,
% 181.00/181.23 (~P2(a10,a12,a3)),
% 181.00/181.23 inference(scs_inference,[],[10825,10844,7312,7807,16,18,27,28])).
% 181.00/181.23 cnf(10869,plain,
% 181.00/181.23 (~P1(a8,a2,a4)),
% 181.00/181.23 inference(scs_inference,[],[10825,10844,10793,6569,7312,7807,75,16,18,27,28,26])).
% 181.00/181.23 cnf(10885,plain,
% 181.00/181.23 (~P2(a8,a6,a1)),
% 181.00/181.23 inference(scs_inference,[],[10869,10837,10750,8528,7363,7921,1388,7896,7172,16,27,26,30])).
% 181.00/181.23 cnf(11014,plain,
% 181.00/181.23 (~P1(a3,a2,a8)),
% 181.00/181.23 inference(scs_inference,[],[9296,9640,8730,9564,23,24,25,22])).
% 181.00/181.23 cnf(11148,plain,
% 181.00/181.23 (~P1(a12,a11,a3)),
% 181.00/181.23 inference(scs_inference,[],[15,14,16,10401,10036,10698,10865,10335,23,22,25,24,31])).
% 181.00/181.23 cnf(11178,plain,
% 181.00/181.23 (~P1(a6,x111781,a2)),
% 181.00/181.23 inference(scs_inference,[],[8584,24,25])).
% 181.00/181.23 cnf(11380,plain,
% 181.00/181.23 (~P1(a1,a2,a12)+~P2(a1,a10,a1)),
% 181.00/181.23 inference(scs_inference,[],[1,16,10828,10313,10885,22,24,31])).
% 181.00/181.23 cnf(11391,plain,
% 181.00/181.23 (~P1(a1,a2,a12)),
% 181.00/181.23 inference(scs_inference,[],[16,11380])).
% 181.00/181.23 cnf(11406,plain,
% 181.00/181.23 (~P1(a11,a12,a3)),
% 181.00/181.23 inference(scs_inference,[],[11148,22])).
% 181.00/181.23 cnf(11482,plain,
% 181.00/181.23 (~P2(a5,a7,a11)),
% 181.00/181.23 inference(scs_inference,[],[11178,10632,22,24])).
% 181.00/181.23 cnf(11888,plain,
% 181.00/181.23 ($false),
% 181.00/181.23 inference(scs_inference,[],[6,8,17,11406,11482,11391,11014,6262,7988,1604,835,542,89,27,28]),
% 181.00/181.23 ['proof']).
% 181.00/181.23 % SZS output end Proof
% 181.00/181.23 % Total time :180.350000s
%------------------------------------------------------------------------------