%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : PLA009-1 : TPTP v8.2.0. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n007.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 13:35:29 EDT 2024
% Result : Unsatisfiable 244.31s 244.48s
% Output : CNFRefutation 244.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : PLA009-1 : TPTP v8.2.0. Released v1.1.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.33 % Computer : n007.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jun 18 16:49:24 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.51/0.58 start to proof:theBenchmark
% 244.31/244.44 %-------------------------------------------
% 244.31/244.44 % File :CSE---1.7
% 244.31/244.44 % Problem :theBenchmark
% 244.31/244.44 % Transform :cnf
% 244.31/244.44 % Format :tptp:raw
% 244.31/244.44 % Command :java -jar mcs_scs.jar %d %s
% 244.31/244.44
% 244.31/244.44 % Result :Theorem 243.660000s
% 244.31/244.44 % Output :CNFRefutation 243.660000s
% 244.31/244.44 %-------------------------------------------
% 244.31/244.47 %--------------------------------------------------------------------------
% 244.31/244.47 % File : PLA009-1 : TPTP v8.2.0. Released v1.1.0.
% 244.31/244.47 % Domain : Planning (Blocks world)
% 244.31/244.47 % Problem : Block A on B and D clear
% 244.31/244.48 % Version : [SE94] axioms.
% 244.31/244.48 % English :
% 244.31/244.48
% 244.31/244.48 % Refs : [Sus73] Sussman (1973), A Computational Model of Skill Acquisi
% 244.31/244.48 % : [SE94] Segre & Elkan (1994), A High-Performance Explanation-B
% 244.31/244.48 % Source : [SE94]
% 244.31/244.48 % Names : - [SE94]
% 244.31/244.48
% 244.31/244.48 % Status : Unsatisfiable
% 244.31/244.48 % Rating : 0.27 v8.2.0, 0.29 v8.1.0, 0.25 v7.4.0, 0.33 v7.3.0, 0.25 v6.2.0, 0.33 v6.1.0, 0.57 v6.0.0, 0.44 v5.5.0, 0.50 v5.4.0, 0.56 v5.3.0, 0.60 v5.2.0, 0.69 v5.1.0, 0.56 v5.0.0, 0.53 v4.0.1, 0.57 v3.4.0, 0.40 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.25 v2.6.0, 0.14 v2.5.0, 0.43 v2.4.0, 0.43 v2.3.0, 0.29 v2.2.1, 0.33 v2.2.0, 0.44 v2.1.0, 0.57 v2.0.0
% 244.31/244.48 % Syntax : Number of clauses : 31 ( 20 unt; 0 nHn; 28 RR)
% 244.31/244.48 % Number of literals : 53 ( 0 equ; 23 neg)
% 244.31/244.48 % Maximal clause size : 4 ( 1 avg)
% 244.31/244.48 % Maximal term depth : 3 ( 1 avg)
% 244.31/244.48 % Number of predicates : 2 ( 2 usr; 0 prp; 2-2 aty)
% 244.31/244.48 % Number of functors : 14 ( 14 usr; 7 con; 0-2 aty)
% 244.31/244.48 % Number of variables : 37 ( 5 sgn)
% 244.31/244.48 % SPC : CNF_UNS_RFO_NEQ_HRN
% 244.31/244.48
% 244.31/244.48 % Comments : The axioms are a reconstruction of the situation calculus
% 244.31/244.48 % blocks world as in [Sus73].
% 244.31/244.48 %--------------------------------------------------------------------------
% 244.31/244.48 %----Include Blocks world axioms
% 244.31/244.48 include('Axioms/PLA001-0.ax').
% 244.31/244.48 %----Include Blocks world difference axioms for 4 blocks
% 244.31/244.48 include('Axioms/PLA001-1.ax').
% 244.31/244.48 %--------------------------------------------------------------------------
% 244.31/244.48 cnf(prove_AB_D,negated_conjecture,
% 244.31/244.48 ~ holds(and(on(a,b),clear(d)),State) ).
% 244.31/244.48
% 244.31/244.48 %--------------------------------------------------------------------------
% 244.31/244.48 %-------------------------------------------
% 244.31/244.48 % Proof found
% 244.31/244.48 % SZS status Theorem for theBenchmark
% 244.31/244.48 % SZS output start Proof
% 244.38/244.50 %ClaNum:31(EqnAxiom:0)
% 244.38/244.50 %VarNum:85(SingletonVarNum:37)
% 244.38/244.50 %MaxLitNum:4
% 244.38/244.50 %MaxfuncDepth:2
% 244.38/244.50 %SharedTerms:36
% 244.38/244.50 %goalClause: 20
% 244.38/244.50 %singleGoalClaCount:1
% 244.38/244.50 [1]P1(a1,a9)
% 244.38/244.50 [2]P2(a2,a14)
% 244.38/244.50 [3]P2(a2,a3)
% 244.38/244.50 [4]P2(a2,a5)
% 244.38/244.50 [5]P2(a2,a6)
% 244.38/244.50 [6]P2(a3,a14)
% 244.38/244.50 [7]P2(a3,a5)
% 244.38/244.50 [8]P2(a3,a6)
% 244.38/244.50 [9]P2(a5,a14)
% 244.38/244.50 [10]P2(a5,a6)
% 244.38/244.50 [11]P2(a6,a14)
% 244.38/244.50 [12]P1(f7(a2),a9)
% 244.38/244.50 [13]P1(f7(a3),a9)
% 244.38/244.50 [14]P1(f7(a5),a9)
% 244.38/244.50 [16]P1(f10(a2,a14),a9)
% 244.38/244.50 [17]P1(f10(a3,a14),a9)
% 244.38/244.50 [18]P1(f10(a5,a6),a9)
% 244.38/244.50 [19]P1(f10(a6,a14),a9)
% 244.38/244.50 [15]P1(f7(a14),x151)
% 244.38/244.50 [20]~P1(f4(f10(a2,a3),f7(a6)),x201)
% 244.38/244.50 [21]~P2(x212,x211)+P2(x211,x212)
% 244.38/244.50 [30]~P1(f10(x301,x302),x305)+P1(f10(x301,x302),f8(f13(x303,x304),x305))
% 244.38/244.50 [22]~P1(x222,x223)+~P1(x221,x223)+P1(f4(x221,x222),x223)
% 244.38/244.50 [23]~P2(x231,x232)+~P1(f7(x231),x233)+P1(f7(x231),f8(f12(x232),x233))
% 244.38/244.50 [26]~P1(f11(x261),x263)+~P1(f7(x262),x263)+P1(a1,f8(f13(x261,x262),x263))
% 244.38/244.50 [27]~P1(f11(x271),x273)+~P1(f7(x272),x273)+P1(f7(x271),f8(f13(x271,x272),x273))
% 244.38/244.50 [31]~P1(f11(x311),x313)+~P1(f7(x312),x313)+P1(f10(x311,x312),f8(f13(x311,x312),x313))
% 244.38/244.50 [25]~P2(x251,x253)+~P1(f7(x251),x254)+P1(f7(x251),f8(f13(x252,x253),x254))
% 244.38/244.50 [28]~P2(x281,x283)+~P1(f10(x281,x282),x284)+P1(f10(x281,x282),f8(f12(x283),x284))
% 244.38/244.50 [24]~P2(x241,a14)+~P1(a1,x242)+~P1(f7(x241),x242)+P1(f11(x241),f8(f12(x241),x242))
% 244.38/244.50 [29]~P1(a1,x293)+~P1(f7(x292),x293)+~P1(f10(x292,x291),x293)+P1(f7(x291),f8(f12(x292),x293))
% 244.38/244.50 %EqnAxiom
% 244.38/244.50
% 244.38/244.50 %-------------------------------------------
% 244.47/244.66 cnf(32,plain,
% 244.47/244.66 (~P1(f7(a6),x321)+~P1(f10(a2,a3),x321)),
% 244.47/244.66 inference(scs_inference,[],[20,22])).
% 244.47/244.66 cnf(34,plain,
% 244.47/244.66 (~P1(f10(a2,a3),f8(f12(a14),x341))+~P1(f7(a6),x341)),
% 244.47/244.66 inference(scs_inference,[],[20,11,22,23])).
% 244.47/244.66 cnf(39,plain,
% 244.47/244.66 (~P1(f10(a14,x391),x392)+P1(f10(a14,x391),f8(f12(a2),x392))),
% 244.47/244.66 inference(scs_inference,[],[2,21,28])).
% 244.47/244.66 cnf(40,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f13(x401,x402),x403))+~P1(f10(a2,a3),x403)),
% 244.47/244.66 inference(scs_inference,[],[32,30])).
% 244.47/244.66 cnf(41,plain,
% 244.47/244.66 (~P1(f10(a2,a3),f8(f12(a14),f8(f13(x411,a14),x412)))+~P1(f7(a6),x412)),
% 244.47/244.66 inference(scs_inference,[],[11,34,25])).
% 244.47/244.66 cnf(42,plain,
% 244.47/244.66 (~P1(f10(a14,x421),x422)+P1(f10(a14,x421),f8(f13(x423,x424),f8(f12(a2),x422)))),
% 244.47/244.66 inference(scs_inference,[],[39,30])).
% 244.47/244.66 cnf(44,plain,
% 244.47/244.66 (P1(a1,f8(f13(a2,a14),f8(f12(a2),a9)))),
% 244.47/244.66 inference(scs_inference,[],[15,12,2,1,26,24])).
% 244.47/244.66 cnf(45,plain,
% 244.47/244.66 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),a9)))),
% 244.47/244.66 inference(scs_inference,[],[15,14,9,1,27,24])).
% 244.47/244.66 cnf(46,plain,
% 244.47/244.66 (P1(f10(a6,a14),f8(f12(a5),a9))),
% 244.47/244.66 inference(scs_inference,[],[10,19,21,28])).
% 244.47/244.66 cnf(49,plain,
% 244.47/244.66 (P1(f7(a3),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[3,13,21,23])).
% 244.47/244.66 cnf(50,plain,
% 244.47/244.66 (P1(f7(a5),f8(f13(x501,a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[4,14,21,25])).
% 244.47/244.66 cnf(51,plain,
% 244.47/244.66 (P1(f10(a6,a14),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[5,19,21,28])).
% 244.47/244.66 cnf(54,plain,
% 244.47/244.66 (P1(f7(a5),f8(f12(a3),a9))),
% 244.47/244.66 inference(scs_inference,[],[7,14,21,23])).
% 244.47/244.66 cnf(55,plain,
% 244.47/244.66 (P1(f10(a6,a14),f8(f12(a3),a9))),
% 244.47/244.66 inference(scs_inference,[],[8,19,21,28])).
% 244.47/244.66 cnf(56,plain,
% 244.47/244.66 (P1(f7(a3),f8(f13(x561,a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[3,13,21,25])).
% 244.47/244.66 cnf(57,plain,
% 244.47/244.66 (P1(f7(a5),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[4,14,21,23])).
% 244.47/244.66 cnf(58,plain,
% 244.47/244.66 (~P1(f7(a6),x581)+P1(f7(a6),f8(f12(a2),x581))),
% 244.47/244.66 inference(scs_inference,[],[5,21,23])).
% 244.47/244.66 cnf(61,plain,
% 244.47/244.66 (~P2(a14,a2)+P1(f11(a2),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[12,1,21,24])).
% 244.47/244.66 cnf(62,plain,
% 244.47/244.66 (P1(f4(f11(a2),f11(a2)),f8(f12(a2),a9))+~P2(a14,a2)),
% 244.47/244.66 inference(scs_inference,[],[61,22])).
% 244.47/244.66 cnf(63,plain,
% 244.47/244.66 (P1(f4(f11(a2),f11(a2)),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[2,62,21])).
% 244.47/244.66 cnf(64,plain,
% 244.47/244.66 (P1(f10(a3,a14),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[3,17,21,28])).
% 244.47/244.66 cnf(65,plain,
% 244.47/244.66 (P1(f10(a5,a6),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[4,18,21,28])).
% 244.47/244.66 cnf(68,plain,
% 244.47/244.66 (~P1(f10(a2,a3),f8(f12(a2),x681))+~P1(f7(a6),x681)),
% 244.47/244.66 inference(scs_inference,[],[32,58])).
% 244.47/244.66 cnf(69,plain,
% 244.47/244.66 (~P1(f10(a2,a3),f8(f12(a2),f8(f12(a14),x691)))+~P1(f7(a6),x691)),
% 244.47/244.66 inference(scs_inference,[],[11,68,23])).
% 244.47/244.66 cnf(70,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f12(a6),x701))+~P1(f10(a2,a3),x701)),
% 244.47/244.66 inference(scs_inference,[],[5,32,28])).
% 244.47/244.66 cnf(71,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f12(a6),f8(f13(x711,x712),x713)))+~P1(f10(a2,a3),x713)),
% 244.47/244.66 inference(scs_inference,[],[70,30])).
% 244.47/244.66 cnf(72,plain,
% 244.47/244.66 (~P1(f10(a2,a3),f8(f13(x721,a14),x722))+~P1(f7(a6),x722)),
% 244.47/244.66 inference(scs_inference,[],[11,32,25])).
% 244.47/244.66 cnf(73,plain,
% 244.47/244.66 (~P1(f10(a2,a3),f8(f13(x731,a14),f8(f12(a2),x732)))+~P1(f7(a6),x732)),
% 244.47/244.66 inference(scs_inference,[],[72,58])).
% 244.47/244.66 cnf(74,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f12(a14),x741))+~P1(f10(a2,a3),x741)),
% 244.47/244.66 inference(scs_inference,[],[2,32,28])).
% 244.47/244.66 cnf(75,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f12(a14),f8(f13(x751,x752),x753)))+~P1(f10(a2,a3),x753)),
% 244.47/244.66 inference(scs_inference,[],[74,30])).
% 244.47/244.66 cnf(77,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f12(a3),x771))+~P1(f10(a2,a3),x771)),
% 244.47/244.66 inference(scs_inference,[],[3,32,28])).
% 244.47/244.66 cnf(78,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f12(a3),f8(f13(x781,x782),x783)))+~P1(f10(a2,a3),x783)),
% 244.47/244.66 inference(scs_inference,[],[77,30])).
% 244.47/244.66 cnf(80,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f12(a5),x801))+~P1(f10(a2,a3),x801)),
% 244.47/244.66 inference(scs_inference,[],[4,32,28])).
% 244.47/244.66 cnf(81,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f12(a5),f8(f13(x811,x812),x813)))+~P1(f10(a2,a3),x813)),
% 244.47/244.66 inference(scs_inference,[],[80,30])).
% 244.47/244.66 cnf(92,plain,
% 244.47/244.66 (~P1(f10(a2,a3),f8(f13(a6,a14),x921))+~P1(f11(a6),x921)),
% 244.47/244.66 inference(scs_inference,[],[15,32,27])).
% 244.47/244.66 cnf(95,plain,
% 244.47/244.66 (~P1(f11(a6),x951)+~P1(f10(a2,a3),x951)),
% 244.47/244.66 inference(scs_inference,[],[92,30])).
% 244.47/244.66 cnf(6470,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f13(a2,a3),f8(f12(a2),a9)))+~P1(f11(a2),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[49,32,31])).
% 244.47/244.66 cnf(6480,plain,
% 244.47/244.66 (~P1(f11(a6),f8(f12(a6),x64801))+~P1(f10(a2,a3),x64801)),
% 244.47/244.66 inference(scs_inference,[],[5,95,28])).
% 244.47/244.66 cnf(6483,plain,
% 244.47/244.66 (~P1(f11(a6),f8(f12(a6),f8(f13(x64831,x64832),x64833)))+~P1(f10(a2,a3),x64833)),
% 244.47/244.66 inference(scs_inference,[],[6480,30])).
% 244.47/244.66 cnf(159233,plain,
% 244.47/244.66 (P1(f10(a2,a14),f8(f13(x1592331,x1592332),a9))),
% 244.47/244.66 inference(scs_inference,[],[16,6,21,30])).
% 244.47/244.66 cnf(159241,plain,
% 244.47/244.66 (P1(f10(a2,a14),f8(f12(a6),a9))),
% 244.47/244.66 inference(scs_inference,[],[16,6,9,5,14,21,30,25,23,22,28])).
% 244.47/244.66 cnf(159243,plain,
% 244.47/244.66 (P1(f11(a5),f8(f12(a5),a9))),
% 244.47/244.66 inference(scs_inference,[],[16,6,9,5,14,1,21,30,25,23,22,28,24])).
% 244.47/244.66 cnf(159245,plain,
% 244.47/244.66 (P1(f7(a6),f8(f12(a5),a9))),
% 244.47/244.66 inference(scs_inference,[],[16,6,9,18,5,14,1,21,30,25,23,22,28,24,29])).
% 244.47/244.66 cnf(159253,plain,
% 244.47/244.66 (P2(a5,a3)),
% 244.47/244.66 inference(scs_inference,[],[7,21])).
% 244.47/244.66 cnf(159255,plain,
% 244.47/244.66 (P1(f10(a3,a14),f8(f13(x1592551,x1592552),a9))),
% 244.47/244.66 inference(scs_inference,[],[7,17,21,30])).
% 244.47/244.66 cnf(159257,plain,
% 244.47/244.66 (P1(f7(a2),f8(f13(x1592571,a6),a9))),
% 244.47/244.66 inference(scs_inference,[],[7,17,5,12,21,30,25])).
% 244.47/244.66 cnf(159263,plain,
% 244.47/244.66 (P1(f11(a3),f8(f12(a3),a9))),
% 244.47/244.66 inference(scs_inference,[],[7,17,6,5,12,1,13,21,30,25,23,22,24])).
% 244.47/244.66 cnf(159267,plain,
% 244.47/244.66 (P1(f10(a3,a14),f8(f12(a5),a9))),
% 244.47/244.66 inference(scs_inference,[],[7,17,6,5,14,12,1,13,21,30,25,23,22,24,31,28])).
% 244.47/244.66 cnf(159269,plain,
% 244.47/244.66 (P2(a6,a3)),
% 244.47/244.66 inference(scs_inference,[],[8,21])).
% 244.47/244.66 cnf(159271,plain,
% 244.47/244.66 (P1(f10(a6,a14),f8(f13(x1592711,x1592712),a9))),
% 244.47/244.66 inference(scs_inference,[],[8,19,21,30])).
% 244.47/244.66 cnf(159273,plain,
% 244.47/244.66 (P1(f7(a3),f8(f12(a6),a9))),
% 244.47/244.66 inference(scs_inference,[],[8,19,13,21,30,23])).
% 244.47/244.66 cnf(159285,plain,
% 244.47/244.66 (P2(a6,a5)),
% 244.47/244.66 inference(scs_inference,[],[10,21])).
% 244.47/244.66 cnf(159287,plain,
% 244.47/244.66 (P1(f10(a5,a6),f8(f13(x1592871,x1592872),a9))),
% 244.47/244.66 inference(scs_inference,[],[10,18,21,30])).
% 244.47/244.66 cnf(159291,plain,
% 244.47/244.66 (P1(f10(a5,a6),f8(f12(a6),a9))),
% 244.47/244.66 inference(scs_inference,[],[10,18,21,30,22,28])).
% 244.47/244.66 cnf(159304,plain,
% 244.47/244.66 (P1(f7(a3),f8(f12(a14),a9))),
% 244.47/244.66 inference(scs_inference,[],[6,11,13,21,23])).
% 244.47/244.66 cnf(159310,plain,
% 244.47/244.66 (P1(f11(a2),f8(f12(a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[6,11,17,12,1,13,2,21,23,22,28,24])).
% 244.47/244.66 cnf(159316,plain,
% 244.47/244.66 (~P1(f7(a6),f8(f13(a2,a3),f8(f12(a2),a9)))),
% 244.47/244.66 inference(scs_inference,[],[159310,6470])).
% 244.47/244.66 cnf(159317,plain,
% 244.47/244.66 (P2(a6,a2)),
% 244.47/244.66 inference(scs_inference,[],[5,21])).
% 244.47/244.66 cnf(159333,plain,
% 244.47/244.66 (P2(a3,a2)),
% 244.47/244.66 inference(scs_inference,[],[3,21])).
% 244.47/244.66 cnf(159342,plain,
% 244.47/244.66 (P2(a5,a2)),
% 244.47/244.66 inference(scs_inference,[],[4,21])).
% 244.47/244.66 cnf(159344,plain,
% 244.47/244.66 (P1(f10(a5,a6),f8(f12(a3),a9))),
% 244.47/244.66 inference(scs_inference,[],[159253,18,4,21,28])).
% 244.47/244.66 cnf(159399,plain,
% 244.47/244.66 (P1(f4(a1,f7(a14)),a9)),
% 244.47/244.66 inference(scs_inference,[],[1,15,22])).
% 244.47/244.66 cnf(159420,plain,
% 244.47/244.66 (P1(f7(a2),f8(f12(a14),a9))),
% 244.47/244.66 inference(scs_inference,[],[2,12,23])).
% 244.47/244.66 cnf(159422,plain,
% 244.47/244.66 (P1(f10(a2,a14),f8(f12(a14),a9))),
% 244.47/244.66 inference(scs_inference,[],[2,16,12,23,28])).
% 244.47/244.66 cnf(159466,plain,
% 244.47/244.66 (P1(f7(a2),f8(f12(a3),a9))),
% 244.47/244.66 inference(scs_inference,[],[3,12,25,23])).
% 244.47/244.66 cnf(159468,plain,
% 244.47/244.66 (P1(f10(a2,a14),f8(f12(a3),a9))),
% 244.47/244.66 inference(scs_inference,[],[3,16,12,25,23,28])).
% 244.47/244.66 cnf(159511,plain,
% 244.47/244.66 (P1(f7(a2),f8(f12(a5),a9))),
% 244.47/244.66 inference(scs_inference,[],[4,16,12,28,25,23])).
% 244.47/244.66 cnf(159611,plain,
% 244.47/244.66 (P1(f7(a3),f8(f12(a5),a9))),
% 244.47/244.66 inference(scs_inference,[],[7,13,23])).
% 244.47/244.66 cnf(159766,plain,
% 244.47/244.66 (P1(f10(a6,a14),f8(f12(a14),a9))),
% 244.47/244.66 inference(scs_inference,[],[11,19,28])).
% 244.47/244.66 cnf(159924,plain,
% 244.47/244.66 (P1(f4(f7(a14),f7(a14)),x1599241)),
% 244.47/244.66 inference(scs_inference,[],[15,22])).
% 244.47/244.66 cnf(176001,plain,
% 244.47/244.66 (P1(f10(a6,a14),f8(f12(a3),f8(f12(a2),a9)))),
% 244.47/244.66 inference(scs_inference,[],[51,159269,159245,68,72,69,41,73,28])).
% 244.47/244.66 cnf(176003,plain,
% 244.47/244.66 (P1(f7(a5),f8(f12(a2),f8(f13(x1760031,a2),a9)))),
% 244.47/244.66 inference(scs_inference,[],[50,51,159269,159342,159245,68,72,69,41,73,28,23])).
% 244.47/244.66 cnf(176007,plain,
% 244.47/244.66 (P1(f4(f7(a5),f7(a5)),f8(f13(x1760071,a2),a9))),
% 244.47/244.66 inference(scs_inference,[],[50,51,159269,159342,159245,68,72,69,41,73,28,23,25,22])).
% 244.47/244.66 cnf(176009,plain,
% 244.47/244.66 (P1(f10(a5,a2),f8(f13(a5,a2),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[50,51,159243,159511,159269,159342,159245,68,72,69,41,73,28,23,25,22,31])).
% 244.58/244.67 cnf(176018,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f12(a5),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[55,159285,28])).
% 244.58/244.67 cnf(176020,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a5),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[55,159285,159245,28,23])).
% 244.58/244.67 cnf(176022,plain,
% 244.58/244.67 (P1(f7(a6),f8(f13(x1760221,a5),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[55,159285,159245,28,23,25])).
% 244.58/244.67 cnf(176024,plain,
% 244.58/244.67 (P1(f10(a3,a2),f8(f13(a3,a2),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[55,159263,159466,159285,159245,28,23,25,31])).
% 244.58/244.67 cnf(176040,plain,
% 244.58/244.67 (P1(f4(f10(a6,a14),f10(a6,a14)),f8(f12(a3),a9))),
% 244.58/244.67 inference(scs_inference,[],[55,159263,159466,159285,159273,6,159245,28,23,25,31,69,41,72,73,68,30,24,22])).
% 244.58/244.67 cnf(176054,plain,
% 244.58/244.67 (P1(f10(a3,a14),f8(f12(a2),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[64,176022,159333,41,72,73,68,69,30,28])).
% 244.58/244.67 cnf(176060,plain,
% 244.58/244.67 (P1(f10(a3,a5),f8(f13(a3,a5),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[50,64,176022,159333,54,159263,159253,41,72,73,68,69,30,28,25,23,31])).
% 244.58/244.67 cnf(176068,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f12(a2),f8(f12(a14),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159766,159317,28])).
% 244.58/244.67 cnf(176070,plain,
% 244.58/244.67 (P1(f7(a6),f8(f13(x1760701,a2),f8(f12(a5),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159766,176020,159317,28,25])).
% 244.58/244.67 cnf(176072,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f12(a5),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159766,176020,159317,28,25,23])).
% 244.58/244.67 cnf(176074,plain,
% 244.58/244.67 (P1(f10(a2,a5),f8(f13(a2,a5),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159766,176020,159317,57,159310,28,25,23,31])).
% 244.58/244.67 cnf(176082,plain,
% 244.58/244.67 (~P1(f7(a3),f8(f13(a2,a14),f8(f12(a2),a9)))+P1(f11(a3),f8(f12(a3),f8(f13(a2,a14),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159766,176020,159317,57,44,6,159310,28,25,23,31,68,72,30,24])).
% 244.58/244.67 cnf(176086,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f12(a2),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[65,176072,159342,68,28])).
% 244.58/244.67 cnf(176090,plain,
% 244.58/244.67 (~P1(f7(a6),f8(f12(a2),a9))),
% 244.58/244.67 inference(scs_inference,[],[65,159420,159316,176072,159269,159342,5,68,28,23,25])).
% 244.58/244.67 cnf(176102,plain,
% 244.58/244.67 (P1(f10(a3,a14),f8(f12(a2),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159267,176090,159333,58,28])).
% 244.58/244.67 cnf(176108,plain,
% 244.58/244.67 (~P1(f7(a5),f8(f13(a2,a14),f8(f12(a2),a9)))+P1(f11(a5),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159267,176090,159257,159333,159304,44,5,9,58,28,23,25,24])).
% 244.58/244.67 cnf(176116,plain,
% 244.58/244.67 (P1(f10(a2,a14),f8(f12(a6),f8(f12(a6),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159241,176090,5,58,28])).
% 244.58/244.67 cnf(176118,plain,
% 244.58/244.67 (P1(f7(a6),f8(f13(x1761181,a5),f8(f13(x1761182,a2),f8(f12(a5),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[159241,176070,176090,159285,5,58,28,25])).
% 244.58/244.67 cnf(176126,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f12(a3),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[46,176090,159269,58,28])).
% 244.58/244.67 cnf(176141,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f12(a2),f8(f12(a6),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159291,176090,159342,58,28])).
% 244.58/244.67 cnf(176151,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f12(a3),f8(f13(x1761511,x1761512),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159271,159269,176090,58,28])).
% 244.58/244.67 cnf(176165,plain,
% 244.58/244.67 (~P1(f7(a2),f8(f13(a2,a14),f8(f12(a2),a9)))+P1(f11(a2),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159422,44,176090,5,2,12,1,58,28,29,24])).
% 244.58/244.67 cnf(176169,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f12(a2),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[51,159317,176090,58,28])).
% 244.58/244.67 cnf(176177,plain,
% 244.58/244.67 (P1(f10(a2,a14),f8(f12(a6),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159468,176090,5,58,28])).
% 244.58/244.67 cnf(176189,plain,
% 244.58/244.67 (P1(f7(a5),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176086,45,159253,176090,58,28,23])).
% 244.58/244.67 cnf(176281,plain,
% 244.58/244.67 (P1(f10(a3,a14),f8(f12(a5),f8(f12(a2),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176102,7,176090,58,28])).
% 244.58/244.67 cnf(176388,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f12(a5),f8(f12(a3),f8(f13(x1763881,x1763882),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176151,159285,176090,58,28])).
% 244.58/244.67 cnf(176513,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,159344,30,58])).
% 244.58/244.67 cnf(176519,plain,
% 244.58/244.67 (P1(a1,f8(f13(a2,a3),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[49,159310,159245,159344,30,58,80,34,26])).
% 244.58/244.67 cnf(176523,plain,
% 244.58/244.67 (P1(f7(a3),f8(f13(x1765231,a14),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[49,159310,159245,6,159344,30,58,80,34,26,23,25])).
% 244.58/244.67 cnf(176525,plain,
% 244.58/244.67 (P1(f7(a2),f8(f13(a2,a3),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[49,159310,159245,6,159344,30,58,80,34,26,23,25,27])).
% 244.58/244.67 cnf(176535,plain,
% 244.58/244.67 (P1(f11(a3),f8(f12(a3),f8(f13(a2,a14),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176523,176082])).
% 244.58/244.67 cnf(176538,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f13(x1765381,x1765382),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[176022,65,58,30])).
% 244.58/244.67 cnf(176550,plain,
% 244.58/244.67 (P1(f7(a3),f8(f13(a3,a14),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[15,56,159245,6,176022,65,159263,58,30,80,34,23,25,22,27])).
% 244.58/244.67 cnf(176551,plain,
% 244.58/244.67 (P1(f7(a14),x1765511)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(176553,plain,
% 244.58/244.67 (P1(a1,f8(f13(a3,a14),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[15,176551,56,159245,6,176022,65,159263,58,30,80,34,23,25,22,27,26])).
% 244.58/244.67 cnf(176573,plain,
% 244.58/244.67 (P1(f7(a6),f8(f13(x1765731,a14),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,11,55,176020,176072,30,58,80,34,25])).
% 244.58/244.67 cnf(176575,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a14),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,11,55,176020,176072,30,58,80,34,25,23])).
% 244.58/244.67 cnf(176577,plain,
% 244.58/244.67 (P1(a1,f8(f13(a5,a14),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,11,55,176020,159243,176072,30,58,80,34,25,23,26])).
% 244.58/244.67 cnf(176578,plain,
% 244.58/244.67 (P1(f7(a14),x1765781)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(176582,plain,
% 244.58/244.67 (P1(f7(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a2,a14),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,176578,159245,11,55,176020,159243,176072,176535,30,58,80,34,25,23,26,22,27])).
% 244.58/244.67 cnf(176606,plain,
% 244.58/244.67 (P1(f7(a5),f8(f13(x1766061,a14),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,9,54,51,176072,176575,58,30,72,80,34,23,25])).
% 244.58/244.67 cnf(176608,plain,
% 244.58/244.67 (P1(a1,f8(f13(a3,a14),f8(f12(a3),f8(f13(a2,a14),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,9,54,51,176072,176535,176575,58,30,72,80,34,23,25,26])).
% 244.58/244.67 cnf(176666,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f13(x1766661,x1766662),f8(f13(x1766663,x1766664),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159287,30])).
% 244.58/244.67 cnf(176668,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159287,176513,30,58])).
% 244.58/244.67 cnf(176674,plain,
% 244.58/244.67 (P1(f7(a5),f8(f13(x1766741,a14),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,9,57,159287,176513,30,58,34,80,25])).
% 244.58/244.67 cnf(176678,plain,
% 244.58/244.67 (P1(f4(f7(a5),f7(a5)),f8(f12(a2),a9))),
% 244.58/244.67 inference(scs_inference,[],[159245,9,57,159287,176513,30,58,34,80,25,23,22])).
% 244.58/244.67 cnf(176680,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,9,44,57,159287,176538,176513,30,58,34,80,25,23,22,29])).
% 244.58/244.67 cnf(176689,plain,
% 244.58/244.67 (P1(f11(a5),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176674,176108])).
% 244.58/244.67 cnf(176719,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1767191,x1767192),f8(f12(a14),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,159766,176668,68,80,58,30])).
% 244.58/244.67 cnf(176727,plain,
% 244.58/244.67 (P1(f7(a6),f8(f13(x1767271,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[159245,11,176680,159766,176668,68,80,58,30,72,34,23,25])).
% 244.58/244.67 cnf(176731,plain,
% 244.58/244.67 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,11,159291,176680,159766,176689,176668,68,80,58,30,72,34,23,25,22,26])).
% 244.58/244.67 cnf(176732,plain,
% 244.58/244.67 (P1(f7(a14),x1767321)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(176734,plain,
% 244.58/244.67 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,176732,159245,11,159291,176680,159766,176689,176668,68,80,58,30,72,34,23,25,22,26,27])).
% 244.58/244.67 cnf(176744,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1767441,x1767442),f8(f13(x1767443,x1767444),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,159271,80,30])).
% 244.58/244.67 cnf(176767,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1767671,x1767672),f8(f12(a3),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176001,80,30])).
% 244.58/244.67 cnf(176790,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1767901,x1767902),f8(f12(a5),f8(f12(a3),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176018,80,30])).
% 244.58/244.67 cnf(176813,plain,
% 244.58/244.67 (P1(f10(a3,a14),f8(f13(x1768131,x1768132),f8(f12(a2),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176054,80,30])).
% 244.58/244.67 cnf(176835,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1768351,x1768352),f8(f12(a2),f8(f12(a14),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176068,30])).
% 244.58/244.67 cnf(176860,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f13(x1768601,x1768602),f8(f12(a2),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176086,80,30])).
% 244.58/244.67 cnf(176862,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a14),f8(f12(a14),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,11,176575,176086,80,30,23])).
% 244.58/244.67 cnf(176889,plain,
% 244.58/244.67 (P1(f10(a3,a14),f8(f13(x1768891,x1768892),f8(f12(a2),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176102,176862,68,34,58,72,30])).
% 244.58/244.67 cnf(176906,plain,
% 244.58/244.67 (P1(f10(a2,a14),f8(f13(x1769061,x1769062),f8(f12(a6),f8(f12(a6),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176116,80,30])).
% 244.58/244.67 cnf(176929,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1769291,x1769292),f8(f12(a3),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176126,80,30])).
% 244.58/244.67 cnf(176931,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a14),f8(f12(a5),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,11,176020,176126,80,30,23])).
% 244.58/244.67 cnf(176958,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f13(x1769581,x1769582),f8(f12(a2),f8(f12(a6),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176141,176931,58,34,72,80,30])).
% 244.58/244.67 cnf(176975,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1769751,x1769752),f8(f12(a2),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176169,80,30])).
% 244.58/244.67 cnf(177004,plain,
% 244.58/244.67 (P1(f7(a3),f8(f13(x1770041,a14),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,6,176931,159611,176177,80,30,23,22,25])).
% 244.58/244.67 cnf(177113,plain,
% 244.58/244.67 (P1(f10(a5,a2),f8(f13(x1771131,x1771132),f8(f13(a5,a2),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176009,80,30])).
% 244.58/244.67 cnf(177136,plain,
% 244.58/244.67 (P1(f10(a2,a5),f8(f13(x1771361,x1771362),f8(f13(a2,a5),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176074,80,30])).
% 244.58/244.67 cnf(177159,plain,
% 244.58/244.67 (P1(f10(a3,a2),f8(f13(x1771591,x1771592),f8(f13(a3,a2),f8(f12(a3),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176024,80,30])).
% 244.58/244.67 cnf(177183,plain,
% 244.58/244.67 (P1(f10(a3,a5),f8(f13(x1771831,x1771832),f8(f13(a3,a5),f8(f12(a3),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176060,80,30])).
% 244.58/244.67 cnf(177206,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1772061,x1772062),f8(f12(a3),f8(f13(x1772063,x1772064),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,176151,80,30])).
% 244.58/244.67 cnf(177323,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a14),f8(f12(a2),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,11,176513,176281,80,30,23])).
% 244.58/244.67 cnf(177344,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f12(a14),f8(f12(a2),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[177323,68,58])).
% 244.58/244.67 cnf(177696,plain,
% 244.58/244.67 (P1(f7(a5),f8(f13(x1776961,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[159245,9,176003,176189,176719,80,30,22,23,25])).
% 244.58/244.67 cnf(177826,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f13(x1778261,x1778262),f8(f13(x1778263,x1778264),f8(f13(x1778265,x1778266),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176666,30])).
% 244.58/244.67 cnf(177849,plain,
% 244.58/244.67 (P1(f10(a6,a14),f8(f13(x1778491,x1778492),f8(f13(x1778493,x1778494),f8(f13(x1778495,x1778496),a9))))),
% 244.58/244.67 inference(scs_inference,[],[176744,30])).
% 244.58/244.67 cnf(178102,plain,
% 244.58/244.67 (P1(f10(a3,a14),f8(f13(x1781021,x1781022),f8(f13(x1781023,x1781024),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159255,30])).
% 244.58/244.67 cnf(178123,plain,
% 244.58/244.67 (P1(f10(a3,a14),f8(f13(x1781231,x1781232),f8(f13(x1781233,x1781234),f8(f13(x1781235,x1781236),a9))))),
% 244.58/244.67 inference(scs_inference,[],[178102,30])).
% 244.58/244.67 cnf(178144,plain,
% 244.58/244.67 (P1(f10(a2,a14),f8(f13(x1781441,x1781442),f8(f13(x1781443,x1781444),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159233,30])).
% 244.58/244.67 cnf(178165,plain,
% 244.58/244.67 (P1(f10(a2,a14),f8(f13(x1781651,x1781652),f8(f13(x1781653,x1781654),f8(f13(x1781655,x1781656),a9))))),
% 244.58/244.67 inference(scs_inference,[],[178144,30])).
% 244.58/244.67 cnf(180875,plain,
% 244.58/244.67 (P1(f4(f4(f11(a2),f11(a2)),f4(f11(a2),f11(a2))),f8(f12(a2),a9))),
% 244.58/244.67 inference(scs_inference,[],[159245,63,80,22])).
% 244.58/244.67 cnf(180911,plain,
% 244.58/244.67 (P1(f4(f4(f10(a6,a14),f10(a6,a14)),f4(f10(a6,a14),f10(a6,a14))),f8(f12(a3),a9))),
% 244.58/244.67 inference(scs_inference,[],[159245,176040,80,22])).
% 244.58/244.67 cnf(181035,plain,
% 244.58/244.67 (P1(f11(a2),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159310,15,176165,27])).
% 244.58/244.67 cnf(181040,plain,
% 244.58/244.67 (P1(a1,f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,176678,181035,80,22,26])).
% 244.58/244.67 cnf(181041,plain,
% 244.58/244.67 (P1(f7(a14),x1810411)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(181043,plain,
% 244.58/244.67 (P1(f7(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,181041,159245,176678,181035,80,22,26,27])).
% 244.58/244.67 cnf(181594,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f13(x1815941,a2),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,159317,159399,80,22,25,68,58])).
% 244.58/244.67 cnf(181602,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a14),f8(f13(x1816021,a2),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[159245,11,159317,159399,80,22,25,68,58,32,72,34,23])).
% 244.58/244.67 cnf(181813,plain,
% 244.58/244.67 (P1(a1,f8(f13(a5,a6),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,159243,176007,80,22,26])).
% 244.58/244.67 cnf(181815,plain,
% 244.58/244.67 (P1(f7(a5),f8(f13(a5,a6),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,159243,176007,80,22,26,27])).
% 244.58/244.67 cnf(188599,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f13(x1885991,a2),f8(f12(a5),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[176070,176388,30,34,58])).
% 244.58/244.67 cnf(188601,plain,
% 244.58/244.67 (P1(f7(a6),f8(f13(x1886011,a3),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,159269,176070,176388,30,34,58,25])).
% 244.58/244.67 cnf(188603,plain,
% 244.58/244.67 (P1(f10(a2,a14),f8(f13(a2,a14),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,159310,159269,176070,176388,30,34,58,25,31])).
% 244.58/244.67 cnf(188604,plain,
% 244.58/244.67 (P1(f7(a14),x1886041)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(188606,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a3),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,159310,159269,176070,176388,30,34,58,25,31,23])).
% 244.58/244.67 cnf(188608,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f12(a14),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,159310,159344,9,159269,176070,176388,30,34,58,25,31,23,28])).
% 244.58/244.67 cnf(188611,plain,
% 244.58/244.67 (P1(f7(a14),x1886111)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(188616,plain,
% 244.58/244.67 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[14,15,188604,159245,159310,159344,9,159269,45,176070,159924,176577,176388,30,34,58,25,31,23,28,27,22,24])).
% 244.58/244.67 cnf(188620,plain,
% 244.58/244.67 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[14,15,188604,188611,159245,159310,159344,9,159269,45,176070,159924,176577,176388,30,34,58,25,31,23,28,27,22,24,32,26])).
% 244.58/244.67 cnf(188631,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f13(x1886311,a5),f8(f13(x1886312,a2),f8(f12(a5),f8(f12(a5),a9))))))),
% 244.58/244.67 inference(scs_inference,[],[176118,188603,188606,30,34,32,58])).
% 244.58/244.67 cnf(188633,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f13(a5,a6),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,159243,176118,188603,188606,30,34,32,58,31])).
% 244.58/244.67 cnf(188635,plain,
% 244.58/244.67 (P1(f7(a3),f8(f12(a5),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,49,7,159243,176118,188603,188606,30,34,32,58,31,23])).
% 244.58/244.67 cnf(188637,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f12(a3),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159245,49,159344,159253,7,159243,176118,188603,188606,30,34,32,58,31,23,28])).
% 244.58/244.67 cnf(188639,plain,
% 244.58/244.67 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,49,159344,159253,7,159243,176118,188603,188606,188616,30,34,32,58,31,23,28,27])).
% 244.58/244.67 cnf(188640,plain,
% 244.58/244.67 (P1(f7(a14),x1886401)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(188644,plain,
% 244.58/244.67 (P1(f11(a6),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,49,11,159344,159253,7,159243,176573,176577,176118,188603,188606,188616,30,34,32,58,31,23,28,27,22,24])).
% 244.58/244.67 cnf(188647,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,159245,49,11,159344,159253,7,159243,176573,176577,176118,181813,188603,188606,188616,181815,30,34,32,58,31,23,28,27,22,24,29])).
% 244.58/244.67 cnf(188649,plain,
% 244.58/244.67 (P1(a1,f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,188640,159245,49,11,159344,159253,7,159243,176573,176577,176118,181813,188603,188606,188616,181815,30,34,32,58,31,23,28,27,22,24,29,26])).
% 244.58/244.67 cnf(188658,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f12(a3),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[188606,188608,188647,30,34,32,58])).
% 244.58/244.67 cnf(188660,plain,
% 244.58/244.67 (P1(f10(a2,a3),f8(f13(a2,a3),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[49,159310,188606,188608,188647,30,34,32,58,31])).
% 244.58/244.67 cnf(188662,plain,
% 244.58/244.67 (P1(f7(a3),f8(f12(a2),f8(f12(a2),a9)))),
% 244.58/244.67 inference(scs_inference,[],[49,159310,159333,188606,188608,188647,30,34,32,58,31,23])).
% 244.58/244.67 cnf(188664,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f12(a6),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[49,159310,159344,10,159333,188606,188608,188647,30,34,32,58,31,23,28])).
% 244.58/244.67 cnf(188666,plain,
% 244.58/244.67 (P1(f7(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,49,159310,159344,10,159333,188606,188608,188644,188647,30,34,32,58,31,23,28,27])).
% 244.58/244.67 cnf(188667,plain,
% 244.58/244.67 (P1(f7(a14),x1886671)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(188671,plain,
% 244.58/244.67 (P1(f11(a5),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,49,159310,159344,9,10,159333,176118,176606,188606,176553,188608,188644,188647,30,34,32,58,31,23,28,27,22,24])).
% 244.58/244.67 cnf(188674,plain,
% 244.58/244.67 (P1(f7(a3),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,49,159310,159344,9,10,159333,176118,176606,176525,188606,176519,176553,188608,188644,188647,30,34,32,58,31,23,28,27,22,24,29])).
% 244.58/244.67 cnf(188692,plain,
% 244.58/244.67 (~P1(f7(a6),f8(f13(x1886921,x1886922),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,49,159310,159344,9,10,159333,176118,176606,176525,188606,176519,176553,188608,188644,188647,30,34,32,58,31,23,28,27,22,24,29,70,71,77,78,95,6480,6483,75,40])).
% 244.58/244.67 cnf(188694,plain,
% 244.58/244.67 (~P1(f7(a6),f8(f12(a14),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,49,159310,159344,9,10,159333,176118,176606,176525,188606,176519,176553,188608,188644,188647,30,34,32,58,31,23,28,27,22,24,29,70,71,77,78,95,6480,6483,75,40,74])).
% 244.58/244.67 cnf(188698,plain,
% 244.58/244.67 (~P1(f7(a6),f8(f12(a5),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,49,159310,159344,9,10,159333,176118,176606,176525,188606,176519,176553,188608,188644,188647,30,34,32,58,31,23,28,27,22,24,29,70,71,77,78,95,6480,6483,75,40,74,81,80])).
% 244.58/244.67 cnf(188700,plain,
% 244.58/244.67 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,188667,49,159310,159344,9,10,159333,176118,176606,176525,188606,176519,176553,188608,188644,188647,30,34,32,58,31,23,28,27,22,24,29,70,71,77,78,95,6480,6483,75,40,74,81,80,26])).
% 244.58/244.67 cnf(188711,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[188647,188633,188660,188658,95,30,34,32,58])).
% 244.58/244.67 cnf(188717,plain,
% 244.58/244.67 (P1(f10(a5,a6),f8(f12(a2),f8(f12(a3),a9)))),
% 244.58/244.67 inference(scs_inference,[],[49,159344,159342,8,176680,176689,188647,188633,188660,188658,95,30,34,32,58,31,23,28])).
% 244.58/244.67 cnf(188719,plain,
% 244.58/244.67 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,49,159344,159342,8,176680,176689,188647,188633,188660,188658,188671,95,30,34,32,58,31,23,28,27])).
% 244.58/244.67 cnf(188720,plain,
% 244.58/244.67 (P1(f7(a14),x1887201)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(188724,plain,
% 244.58/244.67 (P1(f11(a2),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,49,2,159344,159342,8,176680,188606,176525,176689,176519,188647,188633,188660,188658,188671,95,30,34,32,58,31,23,28,27,22,24])).
% 244.58/244.67 cnf(188726,plain,
% 244.58/244.67 (P1(a1,f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,188720,49,2,159344,159342,8,176680,188606,176525,176689,176519,188647,188633,188660,188658,188671,95,30,34,32,58,31,23,28,27,22,24,26])).
% 244.58/244.67 cnf(188733,plain,
% 244.58/244.67 (P1(f10(a2,a3),f8(f13(x1887331,x1887332),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.67 inference(scs_inference,[],[188660,95,30])).
% 244.58/244.67 cnf(188739,plain,
% 244.58/244.67 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a3),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[188658,188660,188711,95,30,34,32,58])).
% 244.58/244.67 cnf(188741,plain,
% 244.58/244.67 (P1(f10(a5,a3),f8(f13(a5,a3),f8(f12(a5),a9)))),
% 244.58/244.67 inference(scs_inference,[],[159243,159611,188658,188660,188711,95,30,34,32,58,31])).
% 244.58/244.67 cnf(188743,plain,
% 244.58/244.67 (P1(f7(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,159243,159611,188658,188660,188724,188711,95,30,34,32,58,31,27])).
% 244.58/244.67 cnf(188744,plain,
% 244.58/244.67 (P1(f7(a14),x1887441)),
% 244.58/244.67 inference(rename_variables,[],[15])).
% 244.58/244.67 cnf(188748,plain,
% 244.58/244.67 (P1(f11(a3),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9))))),
% 244.58/244.67 inference(scs_inference,[],[15,6,159243,159611,176577,188647,177004,188658,188660,188724,188711,95,30,34,32,58,31,27,22,24])).
% 244.58/244.67 cnf(188763,plain,
% 244.58/244.67 (P1(a1,f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9)))))),
% 244.58/244.67 inference(scs_inference,[],[15,188744,6,159243,159611,176577,188647,177004,188658,188660,188724,188711,95,30,34,32,58,31,27,22,24,75,40,71,78,6483,81,26])).
% 244.58/244.67 cnf(188769,plain,
% 244.58/244.67 (P1(f10(a2,a3),f8(f13(x1887691,x1887692),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.67 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(188779,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188711,188637,188733,188769,188739,92,95,30,34,32,58])).
% 244.58/244.68 cnf(188783,plain,
% 244.58/244.68 (P1(f7(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[15,176189,188711,188637,188748,188733,188769,188739,92,95,30,34,32,58,31,27])).
% 244.58/244.68 cnf(188784,plain,
% 244.58/244.68 (P1(f7(a14),x1887841)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(188788,plain,
% 244.58/244.68 (P1(f11(a3),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),a9))))),
% 244.58/244.68 inference(scs_inference,[],[15,6,176189,188658,176550,176553,188711,188637,188748,188733,188769,188739,92,95,30,34,32,58,31,27,22,24])).
% 244.58/244.68 cnf(188790,plain,
% 244.58/244.68 (P1(a1,f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[15,188784,6,176189,188658,176550,176553,188711,188637,188748,188733,188769,188739,92,95,30,34,32,58,31,27,22,24,26])).
% 244.58/244.68 cnf(188796,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1887961,x1887962),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(188800,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1888001,x1888002),f8(f13(x1888003,x1888004),f8(f13(a2,a3),f8(f12(a2),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[188733,188796,92,95,30])).
% 244.58/244.68 cnf(188804,plain,
% 244.58/244.68 (~P1(f10(a2,a3),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[188733,188796,188739,188666,92,95,30,34,32])).
% 244.58/244.68 cnf(188806,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a3),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,188796,188739,188666,92,95,30,34,32,58])).
% 244.58/244.68 cnf(188808,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(a2,a3),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[188724,188733,188796,188739,188674,188666,92,95,30,34,32,58,31])).
% 244.58/244.68 cnf(188810,plain,
% 244.58/244.68 (P1(f7(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[15,188724,188733,188796,188739,188788,188674,188666,92,95,30,34,32,58,31,27])).
% 244.58/244.68 cnf(188811,plain,
% 244.58/244.68 (P1(f7(a14),x1888111)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(188815,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188711,181813,188724,188733,188796,188739,181815,188788,188674,188666,92,95,30,34,32,58,31,27,22,24])).
% 244.58/244.68 cnf(188839,plain,
% 244.58/244.68 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[15,188811,9,188711,181813,188724,188733,188796,188739,181815,188788,188674,188666,92,95,30,34,32,58,31,27,22,24,6480,40,77,70,75,78,71,6483,74,81,80,26])).
% 244.58/244.68 cnf(188846,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1888461,x1888462),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(188858,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,188846,188666,188664,188808,188631,92,40,95,30,34,32,58])).
% 244.58/244.68 cnf(188862,plain,
% 244.58/244.68 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[15,188647,188733,188846,188666,188664,188815,188808,188631,92,40,95,30,34,32,58,31,27])).
% 244.58/244.68 cnf(188863,plain,
% 244.58/244.68 (P1(f7(a14),x1888631)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(188867,plain,
% 244.58/244.68 (P1(f11(a6),f8(f12(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,11,188647,188739,188733,188846,188666,188664,188815,188649,188808,188631,92,40,95,30,34,32,58,31,27,22,24])).
% 244.58/244.68 cnf(188869,plain,
% 244.58/244.68 (P1(a1,f8(f13(a6,a14),f8(f12(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,188863,11,188647,188739,188733,188846,188666,188664,188815,188649,188808,188631,92,40,95,30,34,32,58,31,27,22,24,26])).
% 244.58/244.68 cnf(189284,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1892841,x1892842),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189288,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1892881,x1892882),f8(f13(a2,a3),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189284,188808,92,95,30])).
% 244.58/244.68 cnf(189296,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f13(x1892961,a3),f8(f12(a5),a9))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189284,188808,188601,188858,92,95,30,34,72,32,58])).
% 244.58/244.68 cnf(189298,plain,
% 244.58/244.68 (P1(f7(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,188733,189284,188808,188601,188858,188867,92,95,30,34,72,32,58,27])).
% 244.58/244.68 cnf(189299,plain,
% 244.58/244.68 (P1(f7(a14),x1892991)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189303,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188666,188733,189284,188808,188601,177696,188763,188858,188867,92,95,30,34,72,32,58,27,22,24])).
% 244.58/244.68 cnf(189310,plain,
% 244.58/244.68 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189299,9,188666,188733,189284,188808,188601,177696,188763,188858,188867,92,95,30,34,72,32,58,27,22,24,40,31,26])).
% 244.58/244.68 cnf(189318,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1893181,x1893182),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189328,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189318,188858,188717,189296,189288,40,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189330,plain,
% 244.58/244.68 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,188733,189318,188858,188717,189296,189303,189288,40,92,95,30,34,32,58,27])).
% 244.58/244.68 cnf(189331,plain,
% 244.58/244.68 (P1(f7(a14),x1893311)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189335,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188733,189318,188858,188717,189296,188862,188839,189303,189288,40,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189339,plain,
% 244.58/244.68 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189331,9,188733,189318,188858,188717,189296,188862,188839,189303,189288,40,92,95,30,34,32,58,27,22,24,31,26])).
% 244.58/244.68 cnf(189345,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1893451,x1893452),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189355,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f13(x1893551,a3),f8(f12(a5),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189345,189296,189288,188806,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189357,plain,
% 244.58/244.68 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,188733,189345,189296,189288,189335,188806,92,95,30,34,32,58,27])).
% 244.58/244.68 cnf(189358,plain,
% 244.58/244.68 (P1(f7(a14),x1893581)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189362,plain,
% 244.58/244.68 (P1(f11(a3),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,6,188733,189345,188858,189296,189288,188810,188790,189335,188806,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189366,plain,
% 244.58/244.68 (P1(a1,f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189358,6,188733,189345,188858,189296,189288,188810,188790,189335,188806,92,95,30,34,32,58,27,22,24,31,26])).
% 244.58/244.68 cnf(189372,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1893721,x1893722),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189382,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a3),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189372,188806,188741,189355,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189384,plain,
% 244.58/244.68 (P1(f7(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,188733,189372,188806,188741,189355,189362,92,95,30,34,32,58,27])).
% 244.58/244.68 cnf(189385,plain,
% 244.58/244.68 (P1(f7(a14),x1893851)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189389,plain,
% 244.58/244.68 (P1(f11(a3),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,6,188733,189372,189296,188763,188806,188741,189355,188783,189362,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189393,plain,
% 244.58/244.68 (P1(a1,f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189385,6,188733,189372,189296,188763,188806,188741,189355,188783,189362,92,95,30,34,32,58,27,22,24,31,26])).
% 244.58/244.68 cnf(189399,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1893991,x1893992),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189409,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f13(x1894091,a3),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189399,189355,177206,188779,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189411,plain,
% 244.58/244.68 (P1(f7(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,188733,189399,189355,177206,189389,188779,92,95,30,34,32,58,27])).
% 244.58/244.68 cnf(189412,plain,
% 244.58/244.68 (P1(f7(a14),x1894121)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189416,plain,
% 244.58/244.68 (P1(f11(a2),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,2,188733,189399,188806,189355,177206,188743,188726,189389,188779,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189420,plain,
% 244.58/244.68 (P1(a1,f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189412,2,188733,189399,188806,189355,177206,188743,188726,189389,188779,92,95,30,34,32,58,27,22,24,31,26])).
% 244.58/244.68 cnf(189426,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1894261,x1894262),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189436,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189426,188779,177826,189409,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189438,plain,
% 244.58/244.68 (P1(f7(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,188733,189426,188779,177826,189409,189416,92,95,30,34,32,58,27])).
% 244.58/244.68 cnf(189439,plain,
% 244.58/244.68 (P1(f7(a14),x1894391)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189443,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188733,189426,189355,188779,177826,188719,188700,189409,189416,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189447,plain,
% 244.58/244.68 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189439,9,188733,189426,189355,188779,177826,188719,188700,189409,189416,92,95,30,34,32,58,27,22,24,31,26])).
% 244.58/244.68 cnf(189453,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1894531,x1894532),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189463,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f13(x1894631,a2),f8(f12(a5),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189453,177849,188599,189436,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189465,plain,
% 244.58/244.68 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,188733,189453,177849,188599,189443,189436,92,95,30,34,32,58,27])).
% 244.58/244.68 cnf(189466,plain,
% 244.58/244.68 (P1(f7(a14),x1894661)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189470,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188733,189453,188779,177849,188599,188639,188620,189443,189436,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189474,plain,
% 244.58/244.68 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189466,9,188733,189453,188779,177849,188599,188639,188620,189443,189436,92,95,30,34,32,58,27,22,24,31,26])).
% 244.58/244.68 cnf(189480,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1894801,x1894802),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189490,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189480,189436,178123,189463,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189494,plain,
% 244.58/244.68 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,3,188733,189480,189436,178123,189463,189470,92,95,30,34,32,58,28,27])).
% 244.58/244.68 cnf(189495,plain,
% 244.58/244.68 (P1(f7(a14),x1894951)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189499,plain,
% 244.58/244.68 (P1(f11(a3),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a2,a14),f8(f12(a2),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,3,6,188733,189480,188660,189436,178123,176582,176608,189463,189470,92,95,30,34,32,58,28,27,22,24])).
% 244.58/244.68 cnf(189515,plain,
% 244.58/244.68 (P1(a1,f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a2,a14),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189495,3,6,188733,189480,188660,189436,178123,176582,176608,189463,189470,92,95,30,34,32,58,28,27,22,24,6480,77,70,74,40,80,31,26])).
% 244.58/244.68 cnf(189521,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1895211,x1895212),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189531,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a3),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189521,178165,189382,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189535,plain,
% 244.58/244.68 (P1(f7(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a2,a14),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,2,188733,189521,178165,189499,189382,92,95,30,34,32,58,28,27])).
% 244.58/244.68 cnf(189536,plain,
% 244.58/244.68 (P1(f7(a14),x1895361)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189540,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,2,9,188733,189521,189436,178165,176731,176734,189499,189382,92,95,30,34,32,58,28,27,22,24])).
% 244.58/244.68 cnf(189556,plain,
% 244.58/244.68 (P1(a1,f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189536,2,9,188733,189521,189436,178165,176731,176734,189499,189382,92,95,30,34,32,58,28,27,22,24,77,6480,40,70,74,80,31,26])).
% 244.58/244.68 cnf(189562,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1895621,x1895622),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189572,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189562,177183,189328,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189576,plain,
% 244.58/244.68 (P1(f7(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,4,188733,189562,177183,189540,189328,92,95,30,34,32,58,28,27])).
% 244.58/244.68 cnf(189577,plain,
% 244.58/244.68 (P1(f7(a14),x1895771)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189581,plain,
% 244.58/244.68 (P1(f11(a2),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,2,4,188733,189562,189382,177183,181040,181043,189540,189328,92,95,30,34,32,58,28,27,22,24])).
% 244.58/244.68 cnf(189597,plain,
% 244.58/244.68 (P1(a1,f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189577,2,4,188733,189562,189382,177183,181040,181043,189540,189328,92,95,30,34,32,58,28,27,22,24,6480,77,40,74,70,80,31,26])).
% 244.58/244.68 cnf(189603,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1896031,x1896032),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189613,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f13(a6,a14),f8(f12(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189603,177159,189298,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189617,plain,
% 244.58/244.68 (P1(f7(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[15,5,188733,189603,177159,189581,189298,92,95,30,34,32,58,28,27])).
% 244.58/244.68 cnf(189622,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,5,188733,189603,189328,177159,189581,189576,189556,189298,92,95,30,34,32,58,28,27,22,24])).
% 244.58/244.68 cnf(189645,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1896451,x1896452),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189662,plain,
% 244.58/244.68 (P1(f11(a6),f8(f12(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,11,188733,189645,189298,177136,188869,189622,189613,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189672,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1896721,x1896722),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189689,plain,
% 244.58/244.68 (P1(f11(a2),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,2,188733,189672,189613,177113,189617,189597,189662,189572,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189699,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1896991,x1896992),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189716,plain,
% 244.58/244.68 (P1(f11(a3),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a2,a14),f8(f12(a2),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,6,188733,189699,189572,176767,189535,189515,189689,189531,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189726,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1897261,x1897262),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189736,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9)))))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189726,176790,189490,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189743,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188733,189726,189531,176790,189494,189474,189716,189490,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189753,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1897531,x1897532),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189763,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f13(x1897631,a2),f8(f12(a5),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189753,176813,189736,181594,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189770,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188733,189753,189490,176813,189465,189447,189743,189736,181594,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189780,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1897801,x1897802),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189790,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f13(x1897901,a2),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189780,176835,189763,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189797,plain,
% 244.58/244.68 (P1(f11(a2),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a14),f8(f12(a2),f8(f13(a2,a3),f8(f12(a2),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,2,188733,189780,188601,176835,189763,189438,189420,189770,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189807,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1898071,x1898072),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189817,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a14),f8(f13(x1898171,a2),f8(f12(a5),a9)))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189807,176860,189790,181602,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189824,plain,
% 244.58/244.68 (P1(f11(a3),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,6,188733,189807,189763,176860,189790,189411,189393,189797,181602,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189834,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1898341,x1898342),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189844,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a14),f8(f13(x1898441,a2),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189834,176889,189817,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189851,plain,
% 244.58/244.68 (P1(f11(a3),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),f8(f13(a3,a14),f8(f12(a3),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,6,188733,189834,176519,176889,189817,189384,189366,189824,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189861,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1898611,x1898612),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189871,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a14),f8(f12(a2),f8(f12(a5),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189861,176906,189844,177344,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189878,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a5,a6),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188733,189861,189817,176906,189844,189357,189339,189851,177344,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189888,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1898881,x1898882),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189898,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a14),f8(f12(a2),f8(f12(a5),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189888,176929,189871,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189905,plain,
% 244.58/244.68 (P1(f11(a5),f8(f12(a5),f8(f13(a5,a14),f8(f12(a5),f8(f13(a3,a14),f8(f12(a3),f8(f13(a5,a14),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,9,188733,189888,176553,176929,189871,189330,189310,189878,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189915,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1899151,x1899152),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189925,plain,
% 244.58/244.68 (P1(f7(a6),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a2),f8(f12(a14),f8(f12(a2),f8(f12(a5),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[188733,189915,176958,189898,92,95,30,34,32,58])).
% 244.58/244.68 cnf(189928,plain,
% 244.58/244.68 (P1(f7(a14),x1899281)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(189932,plain,
% 244.58/244.68 (P1(f11(a6),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9))))))),
% 244.58/244.68 inference(scs_inference,[],[15,11,188733,189915,189871,176731,176958,189898,189905,176727,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(189937,plain,
% 244.58/244.68 (P1(a1,f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9)))))))),
% 244.58/244.68 inference(scs_inference,[],[14,15,189928,11,188733,189915,189871,176731,176958,189898,189905,176727,92,95,30,34,32,58,27,22,24,31,26])).
% 244.58/244.68 cnf(189943,plain,
% 244.58/244.68 (P1(f10(a2,a3),f8(f13(x1899431,x1899432),f8(f13(a2,a3),f8(f12(a2),a9))))),
% 244.58/244.68 inference(rename_variables,[],[188733])).
% 244.58/244.68 cnf(189960,plain,
% 244.58/244.68 (P1(f11(a6),f8(f12(a6),f8(f13(a6,a14),f8(f12(a6),f8(f13(a5,a14),f8(f12(a5),f8(f13(a2,a14),f8(f12(a2),a9))))))))),
% 244.58/244.68 inference(scs_inference,[],[15,11,188733,189943,189898,176727,176975,189932,189937,189925,92,95,30,34,32,58,27,22,24])).
% 244.58/244.68 cnf(190371,plain,
% 244.58/244.68 (P1(f7(a14),x1903711)),
% 244.58/244.68 inference(rename_variables,[],[15])).
% 244.58/244.68 cnf(190377,plain,
% 244.58/244.68 (~P1(f10(a14,a6),f8(f13(a2,a3),f8(f12(a2),a9)))),
% 244.58/244.68 inference(scs_inference,[],[180875,188635,188694,188804,188800,188674,189662,188616,188724,188808,176519,8,176090,15,190371,6483,92,95,30,58,25,23,31,27,22,29])).
% 244.58/244.68 cnf(190409,plain,
% 244.58/244.68 (~P1(f7(a5),f8(f13(a2,a3),f8(f12(a2),a9)))),
% 244.58/244.68 inference(scs_inference,[],[180911,188662,190377,188698,188692,188671,188800,189960,176538,188808,176519,176525,7,176090,15,6483,42,92,95,30,58,25,23,31,27,22,29])).
% 244.58/244.68 cnf(190717,plain,
% 244.58/244.68 ($false),
% 244.58/244.68 inference(scs_inference,[],[190409,190377,189288,57,188660,159253,176090,42,92,95,58,25]),
% 244.58/244.68 ['proof']).
% 244.72/244.80 % SZS output end Proof
% 244.72/244.80 % Total time :243.660000s
%------------------------------------------------------------------------------