%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG040-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n012.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 14:00:49 EDT 2024
% Result : Unsatisfiable 23.84s 23.88s
% Output : CNFRefutation 23.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : RNG040-1 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.14 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n012.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Tue Jun 18 14:01:39 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.61/0.64 start to proof:theBenchmark
% 23.84/23.87 %-------------------------------------------
% 23.84/23.87 % File :CSE---1.7
% 23.84/23.87 % Problem :theBenchmark
% 23.84/23.87 % Transform :cnf
% 23.84/23.87 % Format :tptp:raw
% 23.84/23.87 % Command :java -jar mcs_scs.jar %d %s
% 23.84/23.87
% 23.84/23.87 % Result :Theorem 23.190000s
% 23.84/23.87 % Output :CNFRefutation 23.190000s
% 23.84/23.87 %-------------------------------------------
% 23.84/23.88 %--------------------------------------------------------------------------
% 23.84/23.88 % File : RNG040-1 : TPTP v8.2.0. Released v1.0.0.
% 23.84/23.88 % Domain : Ring Theory
% 23.84/23.88 % Problem : Ring property 4
% 23.84/23.88 % Version : [Wos65] axioms : Incomplete > Augmented > Complete.
% 23.84/23.88 % English :
% 23.84/23.88
% 23.84/23.88 % Refs : [Wos65] Wos (1965), Unpublished Note
% 23.84/23.88 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 23.84/23.88 % Source : [SPRFN]
% 23.84/23.88 % Names : Problem 29 [Wos65]
% 23.84/23.88
% 23.84/23.88 % Status : Unsatisfiable
% 23.84/23.88 % Rating : 0.00 v8.1.0, 0.11 v7.5.0, 0.05 v7.4.0, 0.12 v7.3.0, 0.08 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.10 v5.5.0, 0.30 v5.3.0, 0.22 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.21 v4.1.0, 0.15 v4.0.1, 0.27 v4.0.0, 0.18 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.00 v3.3.0, 0.07 v3.2.0, 0.00 v3.1.0, 0.09 v2.7.0, 0.25 v2.6.0, 0.20 v2.5.0, 0.17 v2.4.0, 0.22 v2.3.0, 0.11 v2.2.1, 0.33 v2.2.0, 0.11 v2.1.0, 0.11 v2.0.0
% 23.84/23.88 % Syntax : Number of clauses : 27 ( 13 unt; 2 nHn; 17 RR)
% 23.84/23.88 % Number of literals : 63 ( 4 equ; 35 neg)
% 23.84/23.88 % Maximal clause size : 5 ( 2 avg)
% 23.84/23.88 % Maximal term depth : 2 ( 1 avg)
% 23.84/23.88 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 23.84/23.88 % Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% 23.84/23.88 % Number of variables : 78 ( 0 sgn)
% 23.84/23.88 % SPC : CNF_UNS_RFO_SEQ_NHN
% 23.84/23.88
% 23.84/23.88 % Comments : These are the same axioms as in [MOW76].
% 23.84/23.88 %--------------------------------------------------------------------------
% 23.84/23.88 %----Include ring theory axioms
% 23.84/23.88 include('Axioms/RNG001-0.ax').
% 23.84/23.88 %--------------------------------------------------------------------------
% 23.84/23.88 cnf(right_multiplicative_identity,hypothesis,
% 23.84/23.88 product(A,multiplicative_identity,A) ).
% 23.84/23.88
% 23.84/23.88 cnf(left_multiplicative_identity,hypothesis,
% 23.84/23.88 product(multiplicative_identity,A,A) ).
% 23.84/23.88
% 23.84/23.88 cnf(clause30,hypothesis,
% 23.84/23.88 ( product(A,h(A),multiplicative_identity)
% 23.84/23.88 | A = additive_identity ) ).
% 23.84/23.88
% 23.84/23.88 cnf(clause31,hypothesis,
% 23.84/23.88 ( product(h(A),A,multiplicative_identity)
% 23.84/23.88 | A = additive_identity ) ).
% 23.84/23.88
% 23.84/23.88 cnf(product_symmetry,hypothesis,
% 23.84/23.88 ( ~ product(A,B,C)
% 23.84/23.88 | product(B,A,C) ) ).
% 23.84/23.88
% 23.84/23.88 cnf(b_plus_c,negated_conjecture,
% 23.84/23.88 sum(b,c,d) ).
% 23.84/23.88
% 23.84/23.88 cnf(d_plus_a,negated_conjecture,
% 23.84/23.88 product(d,a,additive_identity) ).
% 23.84/23.88
% 23.84/23.88 cnf(b_plus_a,negated_conjecture,
% 23.84/23.88 product(b,a,l) ).
% 23.84/23.88
% 23.84/23.88 cnf(c_plus_a,negated_conjecture,
% 23.84/23.88 product(c,a,n) ).
% 23.84/23.88
% 23.84/23.88 cnf(prove_equation,negated_conjecture,
% 23.84/23.88 ~ sum(l,n,additive_identity) ).
% 23.84/23.88
% 23.84/23.88 %--------------------------------------------------------------------------
% 23.84/23.88 %-------------------------------------------
% 23.84/23.88 % Proof found
% 23.84/23.88 % SZS status Theorem for theBenchmark
% 23.84/23.88 % SZS output start Proof
% 23.84/23.88 %ClaNum:42(EqnAxiom:15)
% 23.84/23.88 %VarNum:162(SingletonVarNum:78)
% 23.84/23.88 %MaxLitNum:5
% 23.84/23.88 %MaxfuncDepth:1
% 23.84/23.88 %SharedTerms:13
% 23.84/23.88 %goalClause: 16 17 18 19 28
% 23.84/23.88 %singleGoalClaCount:5
% 23.84/23.88 [16]P1(a1,a6,a7)
% 23.84/23.88 [17]P2(a1,a2,a8)
% 23.84/23.88 [18]P2(a6,a2,a10)
% 23.84/23.88 [19]P2(a7,a2,a3)
% 23.84/23.88 [28]~P1(a8,a10,a3)
% 23.84/23.88 [20]P1(x201,a3,x201)
% 23.84/23.88 [21]P2(x211,a11,x211)
% 23.84/23.88 [22]P1(a3,x221,x221)
% 23.84/23.88 [23]P2(a11,x231,x231)
% 23.84/23.88 [24]P1(x241,f5(x241),a3)
% 23.84/23.88 [25]P1(f5(x251),x251,a3)
% 23.84/23.88 [26]P1(x261,x262,f4(x261,x262))
% 23.84/23.88 [27]P2(x271,x272,f12(x271,x272))
% 23.84/23.88 [29]E(x291,a3)+P2(x291,f9(x291),a11)
% 23.84/23.88 [30]E(x301,a3)+P2(f9(x301),x301,a11)
% 23.84/23.88 [31]~P1(x312,x311,x313)+P1(x311,x312,x313)
% 23.84/23.88 [32]~P2(x322,x321,x323)+P2(x321,x322,x323)
% 23.84/23.88 [33]~P1(x333,x334,x331)+E(x331,x332)+~P1(x333,x334,x332)
% 23.84/23.88 [34]~P2(x343,x344,x341)+E(x341,x342)+~P2(x343,x344,x342)
% 23.84/23.88 [35]~P1(x356,x354,x351)+P1(x351,x352,x353)+~P1(x354,x352,x355)+~P1(x356,x355,x353)
% 23.84/23.88 [36]~P1(x361,x366,x364)+P1(x361,x362,x363)+~P1(x364,x365,x363)+~P1(x366,x365,x362)
% 23.84/23.88 [37]~P2(x376,x374,x371)+P2(x371,x372,x373)+~P2(x374,x372,x375)+~P2(x376,x375,x373)
% 23.84/23.88 [38]~P2(x381,x386,x384)+P2(x381,x382,x383)+~P2(x384,x385,x383)+~P2(x386,x385,x382)
% 23.84/23.89 [39]~P2(x397,x395,x392)+~P2(x397,x394,x391)+P1(x391,x392,x393)+~P1(x394,x395,x396)+~P2(x397,x396,x393)
% 23.84/23.89 [40]~P2(x405,x407,x402)+~P2(x404,x407,x401)+P1(x401,x402,x403)+~P1(x404,x405,x406)+~P2(x406,x407,x403)
% 23.84/23.89 [41]~P2(x417,x412,x415)+~P2(x416,x412,x414)+P2(x411,x412,x413)+~P1(x414,x415,x413)+~P1(x416,x417,x411)
% 23.84/23.89 [42]~P2(x421,x427,x425)+~P2(x421,x426,x424)+P2(x421,x422,x423)+~P1(x424,x425,x423)+~P1(x426,x427,x422)
% 23.84/23.89 %EqnAxiom
% 23.84/23.89 [1]E(x11,x11)
% 23.84/23.89 [2]E(x22,x21)+~E(x21,x22)
% 23.84/23.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 23.84/23.89 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 23.84/23.89 [5]~E(x51,x52)+E(f9(x51),f9(x52))
% 23.84/23.89 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 23.84/23.89 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 23.84/23.89 [8]~E(x81,x82)+E(f12(x81,x83),f12(x82,x83))
% 23.84/23.89 [9]~E(x91,x92)+E(f12(x93,x91),f12(x93,x92))
% 23.84/23.89 [10]P1(x102,x103,x104)+~E(x101,x102)+~P1(x101,x103,x104)
% 23.84/23.89 [11]P1(x113,x112,x114)+~E(x111,x112)+~P1(x113,x111,x114)
% 23.84/23.89 [12]P1(x123,x124,x122)+~E(x121,x122)+~P1(x123,x124,x121)
% 23.84/23.89 [13]P2(x132,x133,x134)+~E(x131,x132)+~P2(x131,x133,x134)
% 23.84/23.89 [14]P2(x143,x142,x144)+~E(x141,x142)+~P2(x143,x141,x144)
% 23.84/23.89 [15]P2(x153,x154,x152)+~E(x151,x152)+~P2(x153,x154,x151)
% 23.84/23.89
% 23.84/23.89 %-------------------------------------------
% 23.84/23.90 cnf(43,plain,
% 23.84/23.90 (~P1(a10,a8,a3)),
% 23.84/23.90 inference(scs_inference,[],[28,31])).
% 23.84/23.90 cnf(45,plain,
% 23.84/23.90 (E(a7,f4(a1,a6))),
% 23.84/23.90 inference(scs_inference,[],[16,28,26,31,33])).
% 23.84/23.90 cnf(46,plain,
% 23.84/23.90 (P1(x461,x462,f4(x461,x462))),
% 23.84/23.90 inference(rename_variables,[],[26])).
% 23.84/23.90 cnf(48,plain,
% 23.84/23.90 (P1(f4(a1,a6),a3,a7)),
% 23.84/23.90 inference(scs_inference,[],[16,28,20,26,31,33,10])).
% 23.84/23.90 cnf(49,plain,
% 23.84/23.90 (P1(x491,a3,x491)),
% 23.84/23.90 inference(rename_variables,[],[20])).
% 23.84/23.90 cnf(50,plain,
% 23.84/23.90 (E(a8,f12(a1,a2))),
% 23.84/23.90 inference(scs_inference,[],[16,17,28,20,26,27,31,33,10,34])).
% 23.84/23.90 cnf(51,plain,
% 23.84/23.90 (P2(x511,x512,f12(x511,x512))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(53,plain,
% 23.84/23.90 (P1(a3,f4(a1,a6),a7)),
% 23.84/23.90 inference(scs_inference,[],[16,17,28,20,22,26,27,31,33,10,34,11])).
% 23.84/23.90 cnf(56,plain,
% 23.84/23.90 (P1(x561,a3,x561)),
% 23.84/23.90 inference(rename_variables,[],[20])).
% 23.84/23.90 cnf(57,plain,
% 23.84/23.90 (P2(f4(a1,a6),a2,a3)),
% 23.84/23.90 inference(scs_inference,[],[16,17,19,28,20,49,22,26,27,31,33,10,34,11,12,13])).
% 23.84/23.90 cnf(58,plain,
% 23.84/23.90 (P2(a11,f4(a1,a6),a7)),
% 23.84/23.90 inference(scs_inference,[],[16,17,19,28,20,49,22,23,26,27,31,33,10,34,11,12,13,14])).
% 23.84/23.90 cnf(59,plain,
% 23.84/23.90 (P2(a11,x591,x591)),
% 23.84/23.90 inference(rename_variables,[],[23])).
% 23.84/23.90 cnf(60,plain,
% 23.84/23.90 (P2(a7,a11,f4(a1,a6))),
% 23.84/23.90 inference(scs_inference,[],[16,17,19,28,20,49,21,22,23,26,27,31,33,10,34,11,12,13,14,15])).
% 23.84/23.90 cnf(61,plain,
% 23.84/23.90 (P2(x611,a11,x611)),
% 23.84/23.90 inference(rename_variables,[],[21])).
% 23.84/23.90 cnf(62,plain,
% 23.84/23.90 (P1(a7,f5(a6),a1)),
% 23.84/23.90 inference(scs_inference,[],[16,17,19,28,20,49,56,21,22,23,26,27,24,31,33,10,34,11,12,13,14,15,35])).
% 23.84/23.90 cnf(63,plain,
% 23.84/23.90 (P1(x631,a3,x631)),
% 23.84/23.90 inference(rename_variables,[],[20])).
% 23.84/23.90 cnf(66,plain,
% 23.84/23.90 (P1(a1,a6,f4(a7,a3))),
% 23.84/23.90 inference(scs_inference,[],[16,17,19,28,20,49,56,63,21,22,23,26,46,27,24,31,33,10,34,11,12,13,14,15,35,36])).
% 23.84/23.90 cnf(68,plain,
% 23.84/23.90 (P1(x681,x682,f4(x681,x682))),
% 23.84/23.90 inference(rename_variables,[],[26])).
% 23.84/23.90 cnf(70,plain,
% 23.84/23.90 (P2(a8,a11,f12(a1,a2))),
% 23.84/23.90 inference(scs_inference,[],[16,17,19,28,20,49,56,63,21,61,22,23,26,46,27,51,24,31,33,10,34,11,12,13,14,15,35,36,37])).
% 23.84/23.90 cnf(71,plain,
% 23.84/23.90 (P2(x711,x712,f12(x711,x712))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(72,plain,
% 23.84/23.90 (P2(x721,a11,x721)),
% 23.84/23.90 inference(rename_variables,[],[21])).
% 23.84/23.90 cnf(76,plain,
% 23.84/23.90 (P2(x761,x762,f12(x761,x762))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(78,plain,
% 23.84/23.90 (P1(a8,a8,f12(a1,f4(a2,a2)))),
% 23.84/23.90 inference(scs_inference,[],[16,17,19,28,20,49,56,63,21,61,72,22,23,26,46,68,27,51,71,76,24,31,33,10,34,11,12,13,14,15,35,36,37,38,39])).
% 23.84/23.90 cnf(79,plain,
% 23.84/23.90 (P2(x791,x792,f12(x791,x792))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(80,plain,
% 23.84/23.90 (P1(x801,x802,f4(x801,x802))),
% 23.84/23.90 inference(rename_variables,[],[26])).
% 23.84/23.90 cnf(82,plain,
% 23.84/23.90 (P1(a8,a8,f12(f4(a1,a1),a2))),
% 23.84/23.90 inference(scs_inference,[],[16,17,19,28,20,49,56,63,21,61,72,22,23,26,46,68,80,27,51,71,76,79,24,31,33,10,34,11,12,13,14,15,35,36,37,38,39,40])).
% 23.84/23.90 cnf(83,plain,
% 23.84/23.90 (P2(x831,x832,f12(x831,x832))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(84,plain,
% 23.84/23.90 (P1(x841,x842,f4(x841,x842))),
% 23.84/23.90 inference(rename_variables,[],[26])).
% 23.84/23.90 cnf(86,plain,
% 23.84/23.90 (P2(a7,a2,f4(a8,a10))),
% 23.84/23.90 inference(scs_inference,[],[16,17,18,19,28,20,49,56,63,21,61,72,22,23,26,46,68,80,84,27,51,71,76,79,24,31,33,10,34,11,12,13,14,15,35,36,37,38,39,40,41])).
% 23.84/23.90 cnf(87,plain,
% 23.84/23.90 (P1(x871,x872,f4(x871,x872))),
% 23.84/23.90 inference(rename_variables,[],[26])).
% 23.84/23.90 cnf(89,plain,
% 23.84/23.90 (P2(a11,a7,f4(f12(a11,a1),a6))),
% 23.84/23.90 inference(scs_inference,[],[16,17,18,19,28,20,49,56,63,21,61,72,22,23,59,26,46,68,80,84,87,27,51,71,76,79,83,24,31,33,10,34,11,12,13,14,15,35,36,37,38,39,40,41,42])).
% 23.84/23.90 cnf(94,plain,
% 23.84/23.90 (E(f4(a1,a6),a7)),
% 23.84/23.90 inference(scs_inference,[],[16,17,18,19,28,20,49,56,63,21,61,72,22,23,59,26,46,68,80,84,87,27,51,71,76,79,83,24,31,33,10,34,11,12,13,14,15,35,36,37,38,39,40,41,42,2])).
% 23.84/23.90 cnf(97,plain,
% 23.84/23.90 (E(f12(a1,a2),a8)),
% 23.84/23.90 inference(scs_inference,[],[50,2])).
% 23.84/23.90 cnf(98,plain,
% 23.84/23.90 (E(f4(f12(a11,a1),a6),a7)),
% 23.84/23.90 inference(scs_inference,[],[89,50,23,2,34])).
% 23.84/23.90 cnf(99,plain,
% 23.84/23.90 (P2(a11,x991,x991)),
% 23.84/23.90 inference(rename_variables,[],[23])).
% 23.84/23.90 cnf(101,plain,
% 23.84/23.90 (P1(f12(a1,a2),a8,f12(a1,f4(a2,a2)))),
% 23.84/23.90 inference(scs_inference,[],[78,89,50,23,2,34,10])).
% 23.84/23.90 cnf(102,plain,
% 23.84/23.90 (E(f5(a3),a3)),
% 23.84/23.90 inference(scs_inference,[],[78,89,50,22,23,24,2,34,10,33])).
% 23.84/23.90 cnf(104,plain,
% 23.84/23.90 (P1(a3,x1041,x1041)),
% 23.84/23.90 inference(rename_variables,[],[22])).
% 23.84/23.90 cnf(107,plain,
% 23.84/23.90 (P1(a3,x1071,x1071)),
% 23.84/23.90 inference(rename_variables,[],[22])).
% 23.84/23.90 cnf(109,plain,
% 23.84/23.90 (P2(f4(a1,a6),a2,f4(a8,a10))),
% 23.84/23.90 inference(scs_inference,[],[45,78,89,86,50,22,104,23,24,2,34,10,33,12,14,13])).
% 23.84/23.90 cnf(111,plain,
% 23.84/23.90 (P2(a11,a7,f4(a1,a6))),
% 23.84/23.90 inference(scs_inference,[],[45,78,89,86,50,22,104,23,99,24,2,34,10,33,12,14,13,11,15])).
% 23.84/23.90 cnf(112,plain,
% 23.84/23.90 (P2(a11,x1121,x1121)),
% 23.84/23.90 inference(rename_variables,[],[23])).
% 23.84/23.90 cnf(113,plain,
% 23.84/23.90 (P1(f5(a1),a7,a6)),
% 23.84/23.90 inference(scs_inference,[],[16,45,78,89,86,50,25,22,104,107,23,99,24,2,34,10,33,12,14,13,11,15,36])).
% 23.84/23.90 cnf(117,plain,
% 23.84/23.90 (P2(a7,a7,f12(f4(a1,a6),f4(a1,a6)))),
% 23.84/23.90 inference(scs_inference,[],[16,45,78,89,86,50,25,60,58,22,104,107,23,99,27,24,2,34,10,33,12,14,13,11,15,36,38])).
% 23.84/23.90 cnf(118,plain,
% 23.84/23.90 (P2(x1181,x1182,f12(x1181,x1182))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(120,plain,
% 23.84/23.90 (P2(f4(f12(a11,a1),a6),a2,a3)),
% 23.84/23.90 inference(scs_inference,[],[16,19,45,78,89,86,50,25,60,58,22,104,107,23,99,112,27,24,2,34,10,33,12,14,13,11,15,36,38,37])).
% 23.84/23.90 cnf(123,plain,
% 23.84/23.90 (P1(a10,a10,f12(a6,f4(a2,a2)))),
% 23.84/23.90 inference(scs_inference,[],[16,18,19,45,78,89,86,50,25,60,58,22,104,107,23,99,112,26,27,118,24,2,34,10,33,12,14,13,11,15,36,38,37,39])).
% 23.84/23.90 cnf(125,plain,
% 23.84/23.90 (P1(x1251,x1252,f4(x1251,x1252))),
% 23.84/23.90 inference(rename_variables,[],[26])).
% 23.84/23.90 cnf(127,plain,
% 23.84/23.90 (P1(f4(a1,a6),f4(a1,a6),f4(a7,a7))),
% 23.84/23.90 inference(scs_inference,[],[16,18,19,45,78,89,86,50,25,60,58,21,22,104,107,23,99,112,26,125,27,118,24,2,34,10,33,12,14,13,11,15,36,38,37,39,40])).
% 23.84/23.90 cnf(143,plain,
% 23.84/23.90 (E(a3,f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[102,2])).
% 23.84/23.90 cnf(144,plain,
% 23.84/23.90 (E(a3,f12(a7,a2))),
% 23.84/23.90 inference(scs_inference,[],[19,102,27,2,34])).
% 23.84/23.90 cnf(145,plain,
% 23.84/23.90 (P2(x1451,x1452,f12(x1451,x1452))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(147,plain,
% 23.84/23.90 (P1(f4(a1,a6),f5(a6),a1)),
% 23.84/23.90 inference(scs_inference,[],[19,62,102,45,27,2,34,10])).
% 23.84/23.90 cnf(149,plain,
% 23.84/23.90 (P1(f5(x1491),x1491,f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[19,62,102,45,117,25,27,2,34,10,14,12])).
% 23.84/23.90 cnf(151,plain,
% 23.84/23.90 (P1(f4(a1,a6),f5(a3),a7)),
% 23.84/23.90 inference(scs_inference,[],[19,62,48,102,45,117,25,27,2,34,10,14,12,13,11])).
% 23.84/23.90 cnf(152,plain,
% 23.84/23.90 (E(f5(a3),f12(a7,a2))),
% 23.84/23.90 inference(scs_inference,[],[19,62,48,102,45,117,25,27,2,34,10,14,12,13,11,3])).
% 23.84/23.90 cnf(153,plain,
% 23.84/23.90 (P2(a7,a2,f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[19,62,48,102,45,117,25,27,2,34,10,14,12,13,11,3,15])).
% 23.84/23.90 cnf(154,plain,
% 23.84/23.90 (P1(f5(a1),a1,f4(a6,f5(a6)))),
% 23.84/23.90 inference(scs_inference,[],[19,62,48,113,102,45,117,25,26,27,2,34,10,14,12,13,11,3,15,36])).
% 23.84/23.90 cnf(155,plain,
% 23.84/23.90 (P1(x1551,x1552,f4(x1551,x1552))),
% 23.84/23.90 inference(rename_variables,[],[26])).
% 23.84/23.90 cnf(157,plain,
% 23.84/23.90 (P2(a11,f4(a8,a10),a3)),
% 23.84/23.90 inference(scs_inference,[],[19,62,48,113,102,86,89,45,117,120,25,26,27,2,34,10,14,12,13,11,3,15,36,38])).
% 23.84/23.90 cnf(161,plain,
% 23.84/23.90 (P2(a3,a11,f12(a7,a2))),
% 23.84/23.90 inference(scs_inference,[],[19,62,48,113,102,86,89,45,117,120,25,21,26,27,145,2,34,10,14,12,13,11,3,15,36,38,35,37])).
% 23.84/23.90 cnf(162,plain,
% 23.84/23.90 (P2(x1621,x1622,f12(x1621,x1622))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(163,plain,
% 23.84/23.90 (P2(x1631,a11,x1631)),
% 23.84/23.90 inference(rename_variables,[],[21])).
% 23.84/23.90 cnf(165,plain,
% 23.84/23.90 (P1(a3,a3,f12(a7,f4(a2,a2)))),
% 23.84/23.90 inference(scs_inference,[],[19,62,48,113,102,86,89,45,117,120,25,21,26,155,27,145,162,2,34,10,14,12,13,11,3,15,36,38,35,37,39])).
% 23.84/23.90 cnf(169,plain,
% 23.84/23.90 (P1(f12(a1,a2),f12(a1,a2),f12(f4(a1,a1),a2))),
% 23.84/23.90 inference(scs_inference,[],[19,62,48,113,102,82,86,89,45,117,70,120,25,21,163,26,155,27,145,162,2,34,10,14,12,13,11,3,15,36,38,35,37,39,40])).
% 23.84/23.90 cnf(181,plain,
% 23.84/23.90 (E(f12(a7,f4(a2,a2)),a3)),
% 23.84/23.90 inference(scs_inference,[],[165,22,98,2,33])).
% 23.84/23.90 cnf(184,plain,
% 23.84/23.90 (E(f12(a7,a2),a3)),
% 23.84/23.90 inference(scs_inference,[],[165,22,98,161,21,2,33,34])).
% 23.84/23.90 cnf(185,plain,
% 23.84/23.90 (P2(x1851,a11,x1851)),
% 23.84/23.90 inference(rename_variables,[],[21])).
% 23.84/23.90 cnf(187,plain,
% 23.84/23.90 (P1(a7,f4(a1,a6),f4(a7,a7))),
% 23.84/23.90 inference(scs_inference,[],[127,165,22,94,98,161,21,2,33,34,10])).
% 23.84/23.90 cnf(188,plain,
% 23.84/23.90 (P2(a11,a3,f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[127,165,102,22,94,98,161,21,23,2,33,34,10,14])).
% 23.84/23.90 cnf(190,plain,
% 23.84/23.90 (P2(f5(a3),a11,f12(a7,a2))),
% 23.84/23.90 inference(scs_inference,[],[127,165,102,22,94,98,161,143,21,23,2,33,34,10,14,13])).
% 23.84/23.90 cnf(191,plain,
% 23.84/23.90 (P1(f4(a1,a6),a7,f4(a7,a7))),
% 23.84/23.90 inference(scs_inference,[],[127,165,102,22,94,98,161,143,21,23,2,33,34,10,14,13,11])).
% 23.84/23.90 cnf(192,plain,
% 23.84/23.90 (P1(x1921,f5(x1921),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[127,165,102,22,24,94,98,161,143,21,23,2,33,34,10,14,13,11,12])).
% 23.84/23.90 cnf(193,plain,
% 23.84/23.90 (E(f4(a1,a6),f4(f12(a11,a1),a6))),
% 23.84/23.90 inference(scs_inference,[],[127,165,102,22,24,94,98,161,143,21,23,2,33,34,10,14,13,11,12,3])).
% 23.84/23.90 cnf(194,plain,
% 23.84/23.90 (P2(f4(a1,a6),a2,f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[127,165,102,22,24,57,94,98,161,143,21,23,2,33,34,10,14,13,11,12,3,15])).
% 23.84/23.90 cnf(198,plain,
% 23.84/23.90 (P2(a3,f4(a1,a6),f12(f12(a7,a2),a7))),
% 23.84/23.90 inference(scs_inference,[],[127,165,102,22,24,57,94,98,111,161,143,21,23,26,27,2,33,34,10,14,13,11,12,3,15,36,38])).
% 23.84/23.90 cnf(199,plain,
% 23.84/23.90 (P2(x1991,x1992,f12(x1991,x1992))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(201,plain,
% 23.84/23.90 (P1(f4(a6,f5(a6)),a3,f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[127,154,165,102,20,22,24,57,94,149,98,111,161,143,21,23,26,27,2,33,34,10,14,13,11,12,3,15,36,38,35])).
% 23.84/23.90 cnf(203,plain,
% 23.84/23.90 (P1(x2031,a3,x2031)),
% 23.84/23.90 inference(rename_variables,[],[20])).
% 23.84/23.90 cnf(205,plain,
% 23.84/23.90 (P2(a10,a11,f12(a6,a2))),
% 23.84/23.90 inference(scs_inference,[],[18,127,154,165,102,20,22,24,57,94,149,98,111,161,143,21,185,23,26,27,199,2,33,34,10,14,13,11,12,3,15,36,38,35,37])).
% 23.84/23.90 cnf(209,plain,
% 23.84/23.90 (P1(f5(a3),f5(a3),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[18,127,154,165,102,20,203,22,24,57,94,149,98,111,161,143,21,185,23,26,27,199,2,33,34,10,14,13,11,12,3,15,36,38,35,37,39])).
% 23.84/23.90 cnf(210,plain,
% 23.84/23.90 (P1(x2101,a3,x2101)),
% 23.84/23.90 inference(rename_variables,[],[20])).
% 23.84/23.90 cnf(212,plain,
% 23.84/23.90 (P1(f12(a7,a2),f12(a7,a2),f12(a7,a2))),
% 23.84/23.90 inference(scs_inference,[],[18,127,154,165,102,20,203,210,22,24,57,94,149,98,111,161,143,21,185,23,26,27,199,2,33,34,10,14,13,11,12,3,15,36,38,35,37,39,40])).
% 23.84/23.90 cnf(223,plain,
% 23.84/23.90 (E(a3,f12(a7,f4(a2,a2)))),
% 23.84/23.90 inference(scs_inference,[],[181,2])).
% 23.84/23.90 cnf(224,plain,
% 23.84/23.90 (E(f4(a6,f5(a6)),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[181,154,149,2,33])).
% 23.84/23.90 cnf(227,plain,
% 23.84/23.90 (E(f12(a7,a2),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[181,154,190,149,21,2,33,34])).
% 23.84/23.90 cnf(228,plain,
% 23.84/23.90 (P2(x2281,a11,x2281)),
% 23.84/23.90 inference(rename_variables,[],[21])).
% 23.84/23.90 cnf(230,plain,
% 23.84/23.90 (P1(f4(f12(a11,a1),a6),a3,a7)),
% 23.84/23.90 inference(scs_inference,[],[48,181,154,193,190,149,21,2,33,34,10])).
% 23.84/23.90 cnf(231,plain,
% 23.84/23.90 (P2(f4(f12(a11,a1),a6),a2,f4(a8,a10))),
% 23.84/23.90 inference(scs_inference,[],[48,181,154,193,109,190,149,21,2,33,34,10,13])).
% 23.84/23.90 cnf(232,plain,
% 23.84/23.90 (P2(a11,f12(a7,a2),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[48,181,154,193,109,144,190,188,149,21,2,33,34,10,13,14])).
% 23.84/23.90 cnf(233,plain,
% 23.84/23.90 (P1(f12(a7,a2),f12(a7,a2),a3)),
% 23.84/23.90 inference(scs_inference,[],[48,212,181,154,193,109,144,190,184,188,149,21,2,33,34,10,13,14,12])).
% 23.84/23.90 cnf(234,plain,
% 23.84/23.90 (P1(f4(a1,a6),f12(a7,a2),a7)),
% 23.84/23.90 inference(scs_inference,[],[48,212,181,154,193,109,144,190,184,188,149,21,2,33,34,10,13,14,12,11])).
% 23.84/23.90 cnf(235,plain,
% 23.84/23.90 (E(f4(f12(a11,a1),a6),f4(a1,a6))),
% 23.84/23.90 inference(scs_inference,[],[48,212,181,154,45,193,109,144,190,184,188,149,98,21,2,33,34,10,13,14,12,11,3])).
% 23.84/23.90 cnf(236,plain,
% 23.84/23.90 (P2(a11,f4(a8,a10),f12(a7,a2))),
% 23.84/23.90 inference(scs_inference,[],[48,212,181,154,45,193,109,157,144,190,184,188,149,98,21,2,33,34,10,13,14,12,11,3,15])).
% 23.84/23.90 cnf(237,plain,
% 23.84/23.90 (P1(a7,a1,f4(f4(a7,a7),f5(a6)))),
% 23.84/23.90 inference(scs_inference,[],[48,212,147,187,181,154,45,193,109,157,144,190,184,188,149,98,21,26,2,33,34,10,13,14,12,11,3,15,36])).
% 23.84/23.90 cnf(240,plain,
% 23.84/23.90 (P2(f5(a3),a3,f12(f12(a7,a2),f4(a8,a10)))),
% 23.84/23.90 inference(scs_inference,[],[48,212,147,187,181,154,45,193,109,157,144,190,184,188,149,98,21,26,27,2,33,34,10,13,14,12,11,3,15,36,38])).
% 23.84/23.90 cnf(243,plain,
% 23.84/23.90 (P1(a7,f5(a3),a7)),
% 23.84/23.90 inference(scs_inference,[],[48,212,147,187,209,181,154,45,193,109,157,151,144,190,184,188,149,98,21,26,27,2,33,34,10,13,14,12,11,3,15,36,38,35])).
% 23.84/23.90 cnf(245,plain,
% 23.84/23.90 (P1(f12(a7,a2),f12(a7,a2),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[48,212,147,187,209,181,154,45,193,109,157,151,144,190,184,188,149,98,21,228,26,27,2,33,34,10,13,14,12,11,3,15,36,38,35,40])).
% 23.84/23.90 cnf(259,plain,
% 23.84/23.90 (E(f12(a6,a2),a10)),
% 23.84/23.90 inference(scs_inference,[],[224,205,21,2,34])).
% 23.84/23.90 cnf(260,plain,
% 23.84/23.90 (P2(x2601,a11,x2601)),
% 23.84/23.90 inference(rename_variables,[],[21])).
% 23.84/23.90 cnf(262,plain,
% 23.84/23.90 (E(f4(a6,f5(a6)),a3)),
% 23.84/23.90 inference(scs_inference,[],[224,154,205,25,21,2,34,33])).
% 23.84/23.90 cnf(265,plain,
% 23.84/23.90 (P1(a8,f12(a1,a2),f12(f4(a1,a1),a2))),
% 23.84/23.90 inference(scs_inference,[],[169,224,154,97,205,25,21,2,34,33,10])).
% 23.84/23.90 cnf(266,plain,
% 23.84/23.90 (P2(a11,f12(a7,f4(a2,a2)),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[169,224,154,188,97,223,205,25,21,2,34,33,10,14])).
% 23.84/23.90 cnf(271,plain,
% 23.84/23.90 (E(f4(a6,f5(a6)),f12(a7,a2))),
% 23.84/23.90 inference(scs_inference,[],[19,48,169,224,201,154,102,188,152,97,194,223,193,205,25,21,2,34,33,10,14,13,11,12,15,3])).
% 23.84/23.90 cnf(272,plain,
% 23.84/23.90 (P1(f12(a7,a2),f5(a3),f4(f5(a3),f12(a7,a2)))),
% 23.84/23.90 inference(scs_inference,[],[19,48,169,245,224,201,154,102,188,152,97,194,223,193,205,25,21,26,2,34,33,10,14,13,11,12,15,3,36])).
% 23.84/23.90 cnf(275,plain,
% 23.84/23.90 (P2(a11,a3,f4(a8,a10))),
% 23.84/23.90 inference(scs_inference,[],[19,48,169,245,224,201,154,102,89,188,152,97,231,194,223,193,205,25,21,26,2,34,33,10,14,13,11,12,15,3,36,38])).
% 23.84/23.90 cnf(277,plain,
% 23.84/23.90 (P1(f5(a3),f12(a7,a2),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[19,48,169,245,224,201,212,154,102,89,188,152,97,231,194,223,193,205,25,21,26,2,34,33,10,14,13,11,12,15,3,36,38,35])).
% 23.84/23.90 cnf(279,plain,
% 23.84/23.90 (P1(f4(a8,a10),f4(a8,a10),f4(a8,a10))),
% 23.84/23.90 inference(scs_inference,[],[19,48,169,245,224,201,212,154,102,89,20,188,152,97,231,194,223,193,205,25,21,26,2,34,33,10,14,13,11,12,15,3,36,38,35,39])).
% 23.84/23.90 cnf(282,plain,
% 23.84/23.90 (P1(f12(a6,a2),f12(a6,a2),f12(a6,f4(a2,a2)))),
% 23.84/23.90 inference(scs_inference,[],[19,48,123,169,245,224,201,212,154,102,89,20,188,152,97,231,194,223,193,205,25,21,260,26,2,34,33,10,14,13,11,12,15,3,36,38,35,39,40])).
% 23.84/23.90 cnf(295,plain,
% 23.84/23.90 (E(a10,f12(a6,a2))),
% 23.84/23.90 inference(scs_inference,[],[18,262,27,2,34])).
% 23.84/23.90 cnf(296,plain,
% 23.84/23.90 (P2(x2961,x2962,f12(x2961,x2962))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(298,plain,
% 23.84/23.90 (P1(a10,f12(a6,a2),f12(a6,f4(a2,a2)))),
% 23.84/23.90 inference(scs_inference,[],[18,282,262,259,27,2,34,10])).
% 23.84/23.90 cnf(300,plain,
% 23.84/23.90 (P2(a11,f4(f12(a11,a1),a6),a7)),
% 23.84/23.90 inference(scs_inference,[],[18,282,262,58,198,259,193,143,27,2,34,10,13,14])).
% 23.84/23.90 cnf(303,plain,
% 23.84/23.90 (P2(a11,f4(a8,a10),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[18,282,230,262,45,236,58,227,198,259,193,143,27,2,34,10,13,14,12,11,15])).
% 23.84/23.90 cnf(304,plain,
% 23.84/23.90 (P1(f5(a3),f4(f5(a3),f12(a7,a2)),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[18,282,230,272,262,277,209,45,236,58,227,198,259,193,143,27,2,34,10,13,14,12,11,15,36])).
% 23.84/23.90 cnf(306,plain,
% 23.84/23.90 (P1(a7,f12(a7,a2),a7)),
% 23.84/23.90 inference(scs_inference,[],[18,282,230,272,262,277,243,209,45,236,58,227,198,259,193,143,27,2,34,10,13,14,12,11,15,36,35])).
% 23.84/23.90 cnf(308,plain,
% 23.84/23.90 (P2(a8,f5(a3),f12(f12(a1,a2),a3))),
% 23.84/23.90 inference(scs_inference,[],[18,282,230,272,262,277,243,209,45,188,236,58,70,227,198,259,193,143,27,296,2,34,10,13,14,12,11,15,36,35,38])).
% 23.84/23.90 cnf(309,plain,
% 23.84/23.90 (P2(x3091,x3092,f12(x3091,x3092))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(311,plain,
% 23.84/23.90 (P2(a11,a7,f4(a1,f12(a11,a6)))),
% 23.84/23.90 inference(scs_inference,[],[16,18,282,230,272,262,277,243,209,45,188,236,58,70,227,198,259,193,143,27,296,309,23,26,2,34,10,13,14,12,11,15,36,35,38,42])).
% 23.84/23.90 cnf(312,plain,
% 23.84/23.90 (P1(x3121,x3122,f4(x3121,x3122))),
% 23.84/23.90 inference(rename_variables,[],[26])).
% 23.84/23.90 cnf(313,plain,
% 23.84/23.90 (P2(x3131,x3132,f12(x3131,x3132))),
% 23.84/23.90 inference(rename_variables,[],[27])).
% 23.84/23.90 cnf(316,plain,
% 23.84/23.90 (P1(a10,a10,f12(f4(a6,a6),a2))),
% 23.84/23.90 inference(scs_inference,[],[16,18,282,230,272,262,277,243,209,45,188,236,58,70,227,198,259,193,143,27,296,309,313,23,26,312,2,34,10,13,14,12,11,15,36,35,38,42,40])).
% 23.84/23.90 cnf(326,plain,
% 23.84/23.90 (E(f4(a1,f12(a11,a6)),a7)),
% 23.84/23.90 inference(scs_inference,[],[311,271,23,2,34])).
% 23.84/23.90 cnf(327,plain,
% 23.84/23.90 (P2(a11,x3271,x3271)),
% 23.84/23.90 inference(rename_variables,[],[23])).
% 23.84/23.90 cnf(329,plain,
% 23.84/23.90 (P1(a3,f4(f5(a3),f12(a7,a2)),f5(a3))),
% 23.84/23.90 inference(scs_inference,[],[102,304,311,271,23,2,34,10])).
% 23.84/23.90 cnf(330,plain,
% 23.84/23.90 (P2(a3,a11,f4(a6,f5(a6)))),
% 23.84/23.90 inference(scs_inference,[],[262,102,304,311,21,271,23,2,34,10,13])).
% 23.84/23.91 cnf(336,plain,
% 23.84/23.91 (P1(f5(a1),a7,f4(a6,f12(a7,a2)))),
% 23.84/23.91 inference(scs_inference,[],[262,102,45,304,101,306,311,113,232,21,271,50,23,26,2,34,10,13,12,14,11,15,36])).
% 23.84/23.91 cnf(337,plain,
% 23.84/23.91 (P1(x3371,x3372,f4(x3371,x3372))),
% 23.84/23.91 inference(rename_variables,[],[26])).
% 23.84/23.91 cnf(339,plain,
% 23.84/23.91 (P2(f4(a1,f12(a11,a6)),a2,a3)),
% 23.84/23.91 inference(scs_inference,[],[19,262,102,45,304,101,306,311,113,232,21,271,50,23,327,26,2,34,10,13,12,14,11,15,36,37])).
% 23.84/23.91 cnf(342,plain,
% 23.84/23.91 (P1(a7,f4(f5(a3),f12(a7,a2)),a7)),
% 23.84/23.91 inference(scs_inference,[],[19,262,102,45,304,101,306,311,243,113,232,21,271,50,23,327,26,2,34,10,13,12,14,11,15,36,37,35])).
% 23.84/23.91 cnf(344,plain,
% 23.84/23.91 (P2(a7,f5(a3),f12(f4(a1,a6),a3))),
% 23.84/23.91 inference(scs_inference,[],[19,262,102,45,304,101,306,311,243,113,188,232,60,21,271,50,27,23,327,26,2,34,10,13,12,14,11,15,36,37,35,38])).
% 23.84/23.91 cnf(345,plain,
% 23.84/23.91 (P2(x3451,x3452,f12(x3451,x3452))),
% 23.84/23.91 inference(rename_variables,[],[27])).
% 23.84/23.91 cnf(347,plain,
% 23.84/23.91 (P1(a3,a3,f12(f4(a7,a7),a2))),
% 23.84/23.91 inference(scs_inference,[],[19,262,102,45,304,101,306,311,243,113,188,232,60,21,271,50,27,345,23,327,26,337,2,34,10,13,12,14,11,15,36,37,35,38,40])).
% 23.84/23.91 cnf(360,plain,
% 23.84/23.91 (E(f5(a3),f4(f5(a3),f12(a7,a2)))),
% 23.84/23.91 inference(scs_inference,[],[329,22,326,2,33])).
% 23.84/23.91 cnf(361,plain,
% 23.84/23.91 (P1(a3,x3611,x3611)),
% 23.84/23.91 inference(rename_variables,[],[22])).
% 23.84/23.91 cnf(363,plain,
% 23.84/23.91 (P1(f12(a7,a2),f4(f5(a3),f12(a7,a2)),f5(a3))),
% 23.84/23.91 inference(scs_inference,[],[329,22,144,326,2,33,10])).
% 23.84/23.91 cnf(364,plain,
% 23.84/23.91 (P2(a3,a3,f12(f12(a7,a2),f4(a8,a10)))),
% 23.84/23.91 inference(scs_inference,[],[102,329,22,144,326,240,2,33,10,13])).
% 23.84/23.91 cnf(365,plain,
% 23.84/23.91 (P2(a11,f12(a7,a2),f4(a8,a10))),
% 23.84/23.91 inference(scs_inference,[],[102,329,22,275,144,326,240,2,33,10,13,14])).
% 23.84/23.91 cnf(366,plain,
% 23.84/23.91 (E(f4(a1,f12(a11,a6)),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[102,45,329,22,275,144,326,240,2,33,10,13,14,3])).
% 23.92/23.91 cnf(369,plain,
% 23.92/23.91 (P2(f4(f12(a11,a1),a6),a2,f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[102,45,329,336,22,275,120,144,326,240,2,33,10,13,14,3,12,11,15])).
% 23.92/23.91 cnf(370,plain,
% 23.92/23.91 (P1(a1,f4(a6,f12(a7,a2)),a7)),
% 23.92/23.91 inference(scs_inference,[],[102,45,329,336,24,22,361,275,120,144,326,240,2,33,10,13,14,3,12,11,15,36])).
% 23.92/23.91 cnf(374,plain,
% 23.92/23.91 (P1(a6,f4(f5(a3),f12(a7,a2)),a6)),
% 23.92/23.91 inference(scs_inference,[],[102,45,329,336,342,113,24,22,361,275,120,144,326,240,2,33,10,13,14,3,12,11,15,36,35])).
% 23.92/23.91 cnf(376,plain,
% 23.92/23.91 (P2(a8,f12(a7,a2),f12(f12(a1,a2),f4(a8,a10)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,329,336,342,113,24,22,361,236,275,120,70,144,326,240,27,2,33,10,13,14,3,12,11,15,36,35,38])).
% 23.92/23.91 cnf(387,plain,
% 23.92/23.91 (E(f4(f5(a3),f12(a7,a2)),f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[360,2])).
% 23.92/23.91 cnf(388,plain,
% 23.92/23.91 (E(f12(f4(a7,a7),a2),a3)),
% 23.92/23.91 inference(scs_inference,[],[360,347,22,2,33])).
% 23.92/23.91 cnf(391,plain,
% 23.92/23.91 (P1(f12(a6,a2),a10,f12(f4(a6,a6),a2))),
% 23.92/23.91 inference(scs_inference,[],[316,360,347,22,295,2,33,10])).
% 23.92/23.91 cnf(394,plain,
% 23.92/23.91 (P2(a11,f5(a3),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[316,360,347,22,275,143,295,308,50,2,33,10,13,11,14])).
% 23.92/23.91 cnf(396,plain,
% 23.92/23.91 (P2(f4(a6,f5(a6)),a11,a3)),
% 23.92/23.91 inference(scs_inference,[],[262,102,316,363,360,347,21,22,275,143,295,308,50,2,33,10,13,11,14,12,15])).
% 23.92/23.91 cnf(398,plain,
% 23.92/23.91 (P1(f12(a7,a2),f5(a3),f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[262,102,316,363,360,347,277,245,21,22,275,143,295,308,50,2,33,10,13,11,14,12,15,36])).
% 23.92/23.91 cnf(402,plain,
% 23.92/23.91 (P2(a11,f5(a3),a3)),
% 23.92/23.91 inference(scs_inference,[],[66,262,102,316,363,360,374,347,277,245,311,21,153,22,275,339,143,295,308,50,2,33,10,13,11,14,12,15,36,35,38])).
% 23.92/23.91 cnf(404,plain,
% 23.92/23.91 (E(x4041,a3)+~E(x4041,f12(f4(a7,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[66,262,102,316,363,360,374,347,277,245,311,21,153,22,275,339,143,295,308,50,2,33,10,13,11,14,12,15,36,35,38,3])).
% 23.92/23.91 cnf(415,plain,
% 23.92/23.91 (E(a3,f12(f4(a7,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[388,2])).
% 23.92/23.91 cnf(416,plain,
% 23.92/23.91 (E(f4(x4161,f5(x4161)),a3)),
% 23.92/23.91 inference(scs_inference,[],[388,26,24,2,33])).
% 23.92/23.91 cnf(418,plain,
% 23.92/23.91 (P1(x4181,x4182,f4(x4181,x4182))),
% 23.92/23.91 inference(rename_variables,[],[26])).
% 23.92/23.91 cnf(422,plain,
% 23.92/23.91 (P2(a11,a3,f4(a6,f5(a6)))),
% 23.92/23.91 inference(scs_inference,[],[262,45,237,388,26,24,23,369,235,2,33,10,13,14])).
% 23.92/23.91 cnf(426,plain,
% 23.92/23.91 (P2(a3,a11,f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[262,102,45,237,388,391,398,161,26,24,23,369,235,227,295,2,33,10,13,14,12,11,15])).
% 23.92/23.91 cnf(427,plain,
% 23.92/23.91 (P1(a6,f12(a7,a2),a6)),
% 23.92/23.91 inference(scs_inference,[],[262,102,45,237,388,391,398,306,113,161,26,24,23,369,235,227,295,2,33,10,13,14,12,11,15,35])).
% 23.92/23.91 cnf(429,plain,
% 23.92/23.91 (P1(a1,f4(a6,f5(a6)),a1)),
% 23.92/23.91 inference(scs_inference,[],[16,62,262,102,45,237,388,391,398,306,113,161,26,418,24,23,369,235,227,295,2,33,10,13,14,12,11,15,35,36])).
% 23.92/23.91 cnf(432,plain,
% 23.92/23.91 (P2(a3,f5(a3),f12(f12(a7,a2),a3))),
% 23.92/23.91 inference(scs_inference,[],[16,62,262,102,45,237,388,391,398,306,113,188,161,26,418,24,27,23,369,235,227,295,2,33,10,13,14,12,11,15,35,36,38])).
% 23.92/23.91 cnf(435,plain,
% 23.92/23.91 (P1(f12(a7,a2),f12(a7,a2),f12(a7,f4(a2,a2)))),
% 23.92/23.91 inference(scs_inference,[],[16,62,262,102,45,237,388,391,398,306,165,113,188,161,21,26,418,24,27,23,369,235,227,295,2,33,10,13,14,12,11,15,35,36,38,40])).
% 23.92/23.91 cnf(445,plain,
% 23.92/23.91 (E(f4(x4451,f5(x4451)),f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[416,26,192,2,33])).
% 23.92/23.91 cnf(447,plain,
% 23.92/23.91 (P1(x4471,x4472,f4(x4471,x4472))),
% 23.92/23.91 inference(rename_variables,[],[26])).
% 23.92/23.91 cnf(449,plain,
% 23.92/23.91 (P1(a3,f12(a7,a2),f12(a7,f4(a2,a2)))),
% 23.92/23.91 inference(scs_inference,[],[435,416,26,192,184,2,33,10])).
% 23.92/23.91 cnf(450,plain,
% 23.92/23.91 (P2(a3,x4501,f12(f5(a3),x4501))),
% 23.92/23.91 inference(scs_inference,[],[102,435,416,26,27,192,184,2,33,10,13])).
% 23.92/23.91 cnf(451,plain,
% 23.92/23.91 (P2(x4511,x4512,f12(x4511,x4512))),
% 23.92/23.91 inference(rename_variables,[],[27])).
% 23.92/23.91 cnf(454,plain,
% 23.92/23.91 (P2(x4541,a3,f12(x4541,f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,435,416,370,26,27,451,192,184,415,2,33,10,13,3,12,14])).
% 23.92/23.91 cnf(455,plain,
% 23.92/23.91 (P2(x4551,x4552,f12(x4551,x4552))),
% 23.92/23.91 inference(rename_variables,[],[27])).
% 23.92/23.91 cnf(457,plain,
% 23.92/23.91 (P2(f5(a3),a11,a3)),
% 23.92/23.91 inference(scs_inference,[],[102,45,435,416,370,190,26,27,451,192,184,415,2,33,10,13,3,12,14,11,15])).
% 23.92/23.91 cnf(458,plain,
% 23.92/23.91 (P1(a1,f5(a3),a1)),
% 23.92/23.91 inference(scs_inference,[],[102,45,435,416,370,429,201,190,20,26,27,451,192,184,415,2,33,10,13,3,12,14,11,15,36])).
% 23.92/23.91 cnf(461,plain,
% 23.92/23.91 (P1(f4(a7,a3),f12(a7,a2),f4(a7,a3))),
% 23.92/23.91 inference(scs_inference,[],[66,102,45,435,416,427,370,429,201,190,20,26,27,451,192,184,415,2,33,10,13,3,12,14,11,15,36,35])).
% 23.92/23.91 cnf(463,plain,
% 23.92/23.91 (P2(x4631,f12(a7,a2),f12(x4631,f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[66,102,45,435,416,427,370,429,201,190,20,21,26,27,451,455,192,184,415,2,33,10,13,3,12,14,11,15,36,35,38])).
% 23.92/23.91 cnf(467,plain,
% 23.92/23.91 (P1(f12(a7,a2),f12(a7,a2),f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[66,102,45,435,416,427,370,429,201,190,20,161,21,26,447,27,451,455,192,184,415,2,33,10,13,3,12,14,11,15,36,35,38,39])).
% 23.92/23.91 cnf(468,plain,
% 23.92/23.91 (P1(x4681,x4682,f4(x4681,x4682))),
% 23.92/23.91 inference(rename_variables,[],[26])).
% 23.92/23.91 cnf(470,plain,
% 23.92/23.91 (P1(f5(a3),f5(a3),f12(f4(a11,a11),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[66,102,45,435,416,427,370,429,201,190,188,20,161,21,26,447,468,27,451,455,192,184,415,2,33,10,13,3,12,14,11,15,36,35,38,39,40])).
% 23.92/23.91 cnf(473,plain,
% 23.92/23.91 (E(f5(a3),f12(a11,f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[66,102,45,435,416,427,370,429,201,190,188,20,161,232,21,26,447,468,27,451,455,192,184,415,2,33,10,13,3,12,14,11,15,36,35,38,39,40,34])).
% 23.92/23.91 cnf(485,plain,
% 23.92/23.91 (E(f12(a7,a2),f12(f5(a3),a11))),
% 23.92/23.91 inference(scs_inference,[],[445,161,450,2,34])).
% 23.92/23.91 cnf(488,plain,
% 23.92/23.91 (E(f12(a7,f4(a2,a2)),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[445,449,161,22,450,2,34,33])).
% 23.92/23.91 cnf(491,plain,
% 23.92/23.91 (P1(f5(a3),f12(a7,a2),f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[467,445,449,161,22,227,450,2,34,33,10])).
% 23.92/23.91 cnf(492,plain,
% 23.92/23.91 (P2(f4(a1,a6),a11,a7)),
% 23.92/23.91 inference(scs_inference,[],[45,467,445,449,161,21,22,227,450,2,34,33,10,13])).
% 23.92/23.91 cnf(493,plain,
% 23.92/23.91 (P2(x4931,a11,x4931)),
% 23.92/23.91 inference(rename_variables,[],[21])).
% 23.92/23.91 cnf(494,plain,
% 23.92/23.91 (E(f4(x4941,f5(x4941)),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[45,467,445,449,161,21,22,152,227,450,2,34,33,10,13,3])).
% 23.92/23.91 cnf(496,plain,
% 23.92/23.91 (P2(x4961,f4(a1,a6),f12(x4961,a7))),
% 23.92/23.91 inference(scs_inference,[],[45,467,445,449,181,161,21,22,27,152,227,450,2,34,33,10,13,3,12,14])).
% 23.92/23.91 cnf(497,plain,
% 23.92/23.91 (P2(x4971,x4972,f12(x4971,x4972))),
% 23.92/23.91 inference(rename_variables,[],[27])).
% 23.92/23.91 cnf(499,plain,
% 23.92/23.91 (P2(a7,a11,f4(f12(a11,a1),a6))),
% 23.92/23.91 inference(scs_inference,[],[45,467,445,449,181,161,60,21,22,27,152,227,193,450,2,34,33,10,13,3,12,14,11,15])).
% 23.92/23.91 cnf(501,plain,
% 23.92/23.91 (P1(x5011,x5012,f4(x5011,x5012))),
% 23.92/23.91 inference(rename_variables,[],[26])).
% 23.92/23.91 cnf(503,plain,
% 23.92/23.91 (P1(a7,f12(a7,a2),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[16,45,467,445,449,181,187,427,161,60,21,26,501,22,27,152,227,193,234,450,2,34,33,10,13,3,12,14,11,15,36,35])).
% 23.92/23.91 cnf(506,plain,
% 23.92/23.91 (P2(f5(a3),f5(a3),f12(f12(a7,a2),a3))),
% 23.92/23.91 inference(scs_inference,[],[16,45,467,445,449,181,187,427,190,188,161,60,21,26,501,22,27,497,152,227,193,234,450,2,34,33,10,13,3,12,14,11,15,36,35,38])).
% 23.92/23.91 cnf(509,plain,
% 23.92/23.91 (P1(f12(a7,a2),f12(a7,a2),f12(f4(a11,a11),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[16,45,467,445,449,470,181,187,427,190,188,161,60,21,493,26,501,22,27,497,152,227,193,234,450,2,34,33,10,13,3,12,14,11,15,36,35,38,40])).
% 23.92/23.91 cnf(523,plain,
% 23.92/23.91 (E(a7,f12(a11,a7))),
% 23.92/23.91 inference(scs_inference,[],[488,58,496,2,34])).
% 23.92/23.91 cnf(524,plain,
% 23.92/23.91 (P2(x5241,f4(a1,a6),f12(x5241,a7))),
% 23.92/23.91 inference(rename_variables,[],[496])).
% 23.92/23.91 cnf(526,plain,
% 23.92/23.91 (P1(f5(a3),f12(a7,a2),f12(f4(a11,a11),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[488,509,58,227,496,2,34,10])).
% 23.92/23.91 cnf(530,plain,
% 23.92/23.91 (P2(x5301,f4(f12(a11,a1),a6),f12(x5301,a7))),
% 23.92/23.91 inference(scs_inference,[],[488,509,503,58,227,143,193,330,496,524,2,34,10,13,3,12,14])).
% 23.92/23.91 cnf(532,plain,
% 23.92/23.91 (P2(a11,f12(a7,f4(a2,a2)),a3)),
% 23.92/23.91 inference(scs_inference,[],[102,488,461,509,503,58,266,227,143,193,330,496,524,2,34,10,13,3,12,14,11,15])).
% 23.92/23.91 cnf(533,plain,
% 23.92/23.91 (P1(f4(a1,a6),f12(a7,f4(a2,a2)),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[48,102,488,461,509,503,449,58,266,227,143,193,330,496,524,2,34,10,13,3,12,14,11,15,36])).
% 23.92/23.91 cnf(535,plain,
% 23.92/23.91 (P1(f4(a1,a6),f12(a7,a2),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[48,102,488,461,509,503,212,449,58,266,227,143,193,330,496,524,2,34,10,13,3,12,14,11,15,36,35])).
% 23.92/23.91 cnf(537,plain,
% 23.92/23.91 (P2(f5(a3),f5(a3),f12(f12(a7,a2),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[48,102,488,461,509,503,212,449,232,190,58,266,27,227,143,193,330,496,524,2,34,10,13,3,12,14,11,15,36,35,38])).
% 23.92/23.91 cnf(540,plain,
% 23.92/23.91 (P1(a7,a7,f12(f4(a11,a11),a7))),
% 23.92/23.91 inference(scs_inference,[],[48,102,488,461,509,503,212,449,232,190,58,26,266,27,227,143,193,330,496,524,2,34,10,13,3,12,14,11,15,36,35,38,40])).
% 23.92/23.91 cnf(555,plain,
% 23.92/23.91 (E(f4(f12(a11,a1),a6),f12(a11,a7))),
% 23.92/23.91 inference(scs_inference,[],[23,366,530,2,34])).
% 23.92/23.91 cnf(559,plain,
% 23.92/23.91 (P1(f4(f12(a11,a1),a6),f12(a7,a2),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[535,23,193,366,530,2,34,10])).
% 23.92/23.91 cnf(566,plain,
% 23.92/23.91 (P2(f4(a7,a7),a2,a3)),
% 23.92/23.91 inference(scs_inference,[],[102,45,535,491,388,23,27,184,193,366,450,530,499,223,2,34,10,13,3,12,14,11,15])).
% 23.92/23.91 cnf(567,plain,
% 23.92/23.91 (P2(x5671,x5672,f12(x5671,x5672))),
% 23.92/23.91 inference(rename_variables,[],[27])).
% 23.92/23.91 cnf(568,plain,
% 23.92/23.91 (P1(a7,f4(a1,a6),f4(f4(a7,a7),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,535,491,388,187,26,23,27,184,193,366,450,530,499,223,2,34,10,13,3,12,14,11,15,36])).
% 23.92/23.91 cnf(571,plain,
% 23.92/23.91 (P1(f4(a7,a7),f12(a7,f4(a2,a2)),f4(a7,a7))),
% 23.92/23.91 inference(scs_inference,[],[102,45,533,535,491,388,187,26,23,27,184,193,366,450,530,499,223,2,34,10,13,3,12,14,11,15,36,35])).
% 23.92/23.91 cnf(573,plain,
% 23.92/23.91 (P2(f5(a3),f12(a7,a2),f12(f12(a7,a2),f4(a8,a10)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,533,535,491,388,187,236,190,26,23,27,567,184,193,366,450,530,499,223,2,34,10,13,3,12,14,11,15,36,35,38])).
% 23.92/23.91 cnf(587,plain,
% 23.92/23.91 (P1(f4(a1,a6),a7,f12(f4(a11,a11),a7))),
% 23.92/23.91 inference(scs_inference,[],[45,540,494,2,10])).
% 23.92/23.91 cnf(588,plain,
% 23.92/23.91 (P2(f4(a1,a6),x5881,f12(a7,x5881))),
% 23.92/23.91 inference(scs_inference,[],[45,540,27,494,2,10,13])).
% 23.92/23.91 cnf(589,plain,
% 23.92/23.91 (P2(x5891,x5892,f12(x5891,x5892))),
% 23.92/23.91 inference(rename_variables,[],[27])).
% 23.92/23.91 cnf(591,plain,
% 23.92/23.91 (E(f4(a1,a6),f12(a11,a7))),
% 23.92/23.91 inference(scs_inference,[],[45,540,342,27,193,494,555,2,10,13,12,3])).
% 23.92/23.91 cnf(595,plain,
% 23.92/23.91 (P2(a7,f4(a2,a2),a3)),
% 23.92/23.91 inference(scs_inference,[],[45,540,342,181,27,589,193,450,494,555,2,10,13,12,3,14,11,15])).
% 23.92/23.91 cnf(596,plain,
% 23.92/23.91 (P2(x5961,x5962,f12(x5961,x5962))),
% 23.92/23.91 inference(rename_variables,[],[27])).
% 23.92/23.91 cnf(597,plain,
% 23.92/23.91 (P1(a1,f5(a3),f4(a1,f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[45,458,540,342,181,277,26,27,589,193,450,494,555,2,10,13,12,3,14,11,15,36])).
% 23.92/23.91 cnf(598,plain,
% 23.92/23.91 (P1(x5981,x5982,f4(x5981,x5982))),
% 23.92/23.91 inference(rename_variables,[],[26])).
% 23.92/23.91 cnf(600,plain,
% 23.92/23.91 (P1(a7,f12(a7,f4(a2,a2)),a7)),
% 23.92/23.91 inference(scs_inference,[],[45,458,540,342,533,181,277,26,27,589,53,193,450,494,555,2,10,13,12,3,14,11,15,36,35])).
% 23.92/23.91 cnf(602,plain,
% 23.92/23.91 (P2(a3,f5(a3),f12(f12(a7,a2),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[45,458,540,342,533,181,277,232,161,26,27,589,596,53,193,450,494,555,2,10,13,12,3,14,11,15,36,35,38])).
% 23.92/23.91 cnf(605,plain,
% 23.92/23.91 (P1(f12(a7,a2),f12(a7,a2),f12(f4(a7,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[45,458,540,342,533,347,181,277,232,161,21,26,27,589,596,53,193,450,494,555,2,10,13,12,3,14,11,15,36,35,38,40])).
% 23.92/23.91 cnf(606,plain,
% 23.92/23.91 (P2(x6061,a11,x6061)),
% 23.92/23.91 inference(rename_variables,[],[21])).
% 23.92/23.91 cnf(608,plain,
% 23.92/23.91 (P1(f4(a1,a6),f4(a1,a6),f12(a7,f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[45,458,540,342,533,347,181,277,232,161,21,606,26,598,27,589,596,53,193,450,494,555,2,10,13,12,3,14,11,15,36,35,38,40,39])).
% 23.92/23.91 cnf(623,plain,
% 23.92/23.91 (E(f5(a3),f5(f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[102,4,2])).
% 23.92/23.91 cnf(625,plain,
% 23.92/23.91 (E(f4(a1,a6),f12(a7,a11))),
% 23.92/23.91 inference(scs_inference,[],[21,473,588,2,34])).
% 23.92/23.91 cnf(629,plain,
% 23.92/23.91 (P1(a3,f12(a7,a2),f12(f4(a7,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[605,21,184,473,588,2,34,10])).
% 23.92/23.91 cnf(630,plain,
% 23.92/23.91 (P2(a3,f12(a7,a2),f12(f5(a3),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[102,605,21,463,184,473,588,2,34,10,13])).
% 23.92/23.91 cnf(634,plain,
% 23.92/23.91 (E(a7,f12(a7,a11))),
% 23.92/23.91 inference(scs_inference,[],[102,45,605,600,21,463,184,473,506,588,2,34,10,13,12,14,3])).
% 23.92/23.91 cnf(637,plain,
% 23.92/23.91 (P1(a6,f12(a7,f4(a2,a2)),a6)),
% 23.92/23.91 inference(scs_inference,[],[102,45,571,605,600,488,113,21,300,463,184,473,506,588,2,34,10,13,12,14,3,11,15,35])).
% 23.92/23.91 cnf(642,plain,
% 23.92/23.91 (P2(f5(a3),f4(a8,a10),f12(f12(a7,a2),a3))),
% 23.92/23.91 inference(scs_inference,[],[48,102,45,571,605,608,600,488,113,20,275,190,21,27,300,463,184,473,506,588,2,34,10,13,12,14,3,11,15,35,36,38])).
% 23.92/23.91 cnf(654,plain,
% 23.92/23.91 (E(f12(f4(a7,a7),a2),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[629,22,485,2,33])).
% 23.92/23.91 cnf(657,plain,
% 23.92/23.91 (E(f4(a8,a10),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[629,109,22,485,588,2,33,34])).
% 23.92/23.91 cnf(658,plain,
% 23.92/23.91 (P2(f4(a1,a6),x6581,f12(a7,x6581))),
% 23.92/23.91 inference(rename_variables,[],[588])).
% 23.92/23.91 cnf(660,plain,
% 23.92/23.91 (P1(f12(a7,a2),f4(a8,a10),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[279,629,109,22,485,588,2,33,34,10])).
% 23.92/23.91 cnf(661,plain,
% 23.92/23.91 (P2(f4(f12(a11,a1),a6),a11,a7)),
% 23.92/23.91 inference(scs_inference,[],[279,629,109,22,193,492,485,588,2,33,34,10,13])).
% 23.92/23.91 cnf(662,plain,
% 23.92/23.91 (P1(f4(a8,a10),f4(a8,a10),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[279,629,109,22,193,492,485,588,2,33,34,10,13,12])).
% 23.92/23.91 cnf(664,plain,
% 23.92/23.91 (E(f4(f12(a11,a1),a6),f12(a7,a11))),
% 23.92/23.91 inference(scs_inference,[],[102,279,629,109,22,193,492,98,485,432,634,588,2,33,34,10,13,12,14,3])).
% 23.92/23.91 cnf(665,plain,
% 23.92/23.91 (P1(f4(a8,a10),f12(a7,a2),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[102,279,629,109,22,193,492,98,485,432,634,588,2,33,34,10,13,12,14,3,11])).
% 23.92/23.91 cnf(667,plain,
% 23.92/23.91 (P2(f4(a8,a10),a11,f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[102,279,629,275,109,22,21,193,492,98,485,432,634,588,658,2,33,34,10,13,12,14,3,11,15,37])).
% 23.92/23.91 cnf(668,plain,
% 23.92/23.91 (P2(f4(a1,a6),x6681,f12(a7,x6681))),
% 23.92/23.91 inference(rename_variables,[],[588])).
% 23.92/23.91 cnf(673,plain,
% 23.92/23.91 (P1(f4(a1,a6),f12(f4(a7,a7),a2),a7)),
% 23.92/23.91 inference(scs_inference,[],[66,48,102,279,629,637,306,275,109,22,21,193,492,98,485,432,634,588,658,2,33,34,10,13,12,14,3,11,15,37,35,36])).
% 23.92/23.91 cnf(678,plain,
% 23.92/23.91 (P1(f4(a8,a10),f4(a8,a10),f12(a7,f4(a2,a2)))),
% 23.92/23.91 inference(scs_inference,[],[66,48,102,279,629,637,306,190,275,303,109,22,26,21,27,193,492,98,485,432,634,588,658,668,2,33,34,10,13,12,14,3,11,15,37,35,36,38,39])).
% 23.92/23.91 cnf(685,plain,
% 23.92/23.91 (P1(f12(a7,a2),f4(a8,a10),f12(a7,f4(a2,a2)))),
% 23.92/23.91 inference(scs_inference,[],[678,654,657,2,10])).
% 23.92/23.91 cnf(686,plain,
% 23.92/23.91 (P2(f4(a1,a6),f4(a2,a2),a3)),
% 23.92/23.91 inference(scs_inference,[],[45,678,654,595,657,2,10,13])).
% 23.92/23.91 cnf(687,plain,
% 23.92/23.91 (P1(f4(a8,a10),f4(a8,a10),a3)),
% 23.92/23.91 inference(scs_inference,[],[45,678,654,181,595,657,2,10,13,12])).
% 23.92/23.91 cnf(688,plain,
% 23.92/23.91 (P2(f5(a3),a3,f12(f12(a7,a2),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,678,654,181,595,657,537,2,10,13,12,14])).
% 23.92/23.91 cnf(692,plain,
% 23.92/23.91 (P1(f12(a7,a2),f5(a3),f12(f4(a11,a11),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,678,654,526,181,245,394,227,595,657,537,2,10,13,12,14,3,11,15,36])).
% 23.92/23.91 cnf(694,plain,
% 23.92/23.91 (P1(f12(a7,a2),f4(a8,a10),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[102,45,678,654,526,279,181,245,394,227,595,662,657,537,2,10,13,12,14,3,11,15,36,35])).
% 23.92/23.91 cnf(696,plain,
% 23.92/23.91 (P2(f5(a3),f4(a8,a10),f12(f12(a7,a2),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,678,654,526,279,181,245,190,365,394,27,227,595,662,657,537,2,10,13,12,14,3,11,15,36,35,38])).
% 23.92/23.91 cnf(699,plain,
% 23.92/23.91 (P1(f5(a3),f5(a3),f12(a7,f4(a2,a2)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,678,654,526,279,181,245,190,194,365,26,394,27,227,595,662,657,537,588,2,10,13,12,14,3,11,15,36,35,38,39])).
% 23.92/23.91 cnf(706,plain,
% 23.92/23.91 (P1(a3,f4(a8,a10),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[694,184,523,2,10])).
% 23.92/23.91 cnf(707,plain,
% 23.92/23.91 (P2(a3,f12(a7,a2),f12(f12(a7,a2),f4(a8,a10)))),
% 23.92/23.91 inference(scs_inference,[],[102,694,184,523,573,2,10,13])).
% 23.92/23.91 cnf(708,plain,
% 23.92/23.91 (P1(f12(a7,a2),f4(a8,a10),a3)),
% 23.92/23.91 inference(scs_inference,[],[102,694,184,523,573,2,10,13,12])).
% 23.92/23.91 cnf(710,plain,
% 23.92/23.91 (P1(f12(a7,a2),f12(a7,a2),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[102,694,660,184,523,573,642,657,2,10,13,12,14,11])).
% 23.92/23.91 cnf(712,plain,
% 23.92/23.91 (P1(f4(a1,a6),f4(a8,a10),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[102,694,660,559,339,184,143,523,573,642,657,2,10,13,12,14,11,15,35])).
% 23.92/23.91 cnf(714,plain,
% 23.92/23.91 (P1(f4(a1,a6),a7,f4(f4(a7,a7),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[48,102,694,660,559,568,339,53,184,143,523,573,642,657,2,10,13,12,14,11,15,35,36])).
% 23.92/23.91 cnf(716,plain,
% 23.92/23.91 (P2(f5(a3),f5(a3),f12(f12(a7,a2),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[48,102,694,660,559,568,188,190,454,339,53,184,143,523,573,642,657,2,10,13,12,14,11,15,35,36,38])).
% 23.92/23.91 cnf(725,plain,
% 23.92/23.91 (E(f12(a11,a7),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[591,2])).
% 23.92/23.91 cnf(726,plain,
% 23.92/23.91 (E(f12(a7,a2),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[706,22,591,2,33])).
% 23.92/23.91 cnf(729,plain,
% 23.92/23.91 (P1(f4(f12(a11,a1),a6),f4(a8,a10),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[712,706,22,193,591,2,33,10])).
% 23.92/23.91 cnf(730,plain,
% 23.92/23.91 (P2(f12(a7,a2),a11,f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[712,706,22,426,144,193,591,2,33,10,13])).
% 23.92/23.91 cnf(732,plain,
% 23.92/23.91 (E(f12(f4(a7,a7),a2),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[712,706,654,22,426,144,193,591,2,33,10,13,12,3])).
% 23.92/23.91 cnf(736,plain,
% 23.92/23.91 (P2(f4(a1,f12(a11,a6)),a2,f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[102,712,699,706,654,22,339,426,588,144,193,591,2,33,10,13,12,3,14,11,15])).
% 23.92/23.91 cnf(737,plain,
% 23.92/23.91 (P1(f4(a1,a6),f12(a7,a2),f4(a7,f4(a8,a10)))),
% 23.92/23.91 inference(scs_inference,[],[48,102,712,699,706,654,22,26,339,426,588,144,193,591,2,33,10,13,12,3,14,11,15,36])).
% 23.92/23.91 cnf(738,plain,
% 23.92/23.91 (P1(x7381,x7382,f4(x7381,x7382))),
% 23.92/23.91 inference(rename_variables,[],[26])).
% 23.92/23.91 cnf(740,plain,
% 23.92/23.91 (P1(f4(a7,a7),f4(a8,a10),f4(a7,a7))),
% 23.92/23.91 inference(scs_inference,[],[48,102,712,699,706,654,127,22,26,339,426,588,144,193,591,2,33,10,13,12,3,14,11,15,36,35])).
% 23.92/23.91 cnf(745,plain,
% 23.92/23.91 (P1(f4(a1,a6),f4(a1,a6),f12(f4(a11,a11),a7))),
% 23.92/23.91 inference(scs_inference,[],[48,102,712,699,706,654,127,275,161,22,26,738,23,496,27,339,426,588,144,193,591,2,33,10,13,12,3,14,11,15,36,35,38,40])).
% 23.92/23.91 cnf(756,plain,
% 23.92/23.91 (E(f4(a8,a10),f12(f4(a7,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[732,2])).
% 23.92/23.91 cnf(757,plain,
% 23.92/23.91 (P1(f4(a8,a10),f5(a3),f12(f4(a11,a11),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[726,692,732,2,10])).
% 23.92/23.91 cnf(758,plain,
% 23.92/23.91 (P2(f4(f12(a11,a1),a6),x7581,f12(a7,x7581))),
% 23.92/23.91 inference(scs_inference,[],[726,692,588,193,732,2,10,13])).
% 23.92/23.91 cnf(760,plain,
% 23.92/23.91 (E(f12(a7,f4(a2,a2)),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[45,726,673,692,488,588,193,732,2,10,13,12,3])).
% 23.92/23.91 cnf(761,plain,
% 23.92/23.91 (P2(x7611,f4(a8,a10),f12(x7611,f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[45,726,673,692,488,463,588,193,732,2,10,13,12,3,14])).
% 23.92/23.91 cnf(763,plain,
% 23.92/23.91 (P2(f5(a3),a11,f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[45,726,673,737,692,488,190,463,588,193,732,2,10,13,12,3,14,11,15])).
% 23.92/23.91 cnf(764,plain,
% 23.92/23.91 (P1(f12(f4(a11,a11),f5(a3)),a3,a3)),
% 23.92/23.91 inference(scs_inference,[],[45,726,673,737,692,470,488,190,25,463,588,193,732,2,10,13,12,3,14,11,15,35])).
% 23.92/23.91 cnf(767,plain,
% 23.92/23.91 (P1(f12(a7,a2),f4(a8,a10),f4(f4(a8,a10),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[45,726,673,737,692,470,488,190,25,26,463,588,193,710,732,2,10,13,12,3,14,11,15,35,36])).
% 23.92/23.91 cnf(773,plain,
% 23.92/23.91 (E(f12(a7,a2),f12(a11,f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[45,726,673,737,692,470,488,236,190,275,25,26,463,454,588,193,710,732,2,10,13,12,3,14,11,15,35,36,38,34])).
% 23.92/23.91 cnf(780,plain,
% 23.92/23.91 (P1(f4(a8,a10),f4(a8,a10),f4(f4(a8,a10),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[767,726,773,2,10])).
% 23.92/23.91 cnf(781,plain,
% 23.92/23.91 (P2(f12(f4(a7,a7),a2),a11,f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[767,726,667,773,756,2,10,13])).
% 23.92/23.91 cnf(783,plain,
% 23.92/23.91 (P2(a11,f12(f4(a7,a7),a2),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[767,764,726,236,667,143,773,756,2,10,13,12,14])).
% 23.92/23.91 cnf(786,plain,
% 23.92/23.91 (P1(f12(a7,f4(a2,a2)),a3,a3)),
% 23.92/23.91 inference(scs_inference,[],[86,767,740,764,699,726,236,25,667,143,773,756,2,10,13,12,14,11,15,35])).
% 23.92/23.91 cnf(789,plain,
% 23.92/23.91 (P1(f12(a7,a2),a3,f12(f4(a7,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[86,767,740,764,699,629,726,236,25,667,143,773,756,233,2,10,13,12,14,11,15,35,36])).
% 23.92/23.91 cnf(807,plain,
% 23.92/23.91 (P1(a7,f4(a8,a10),f4(a1,a6))),
% 23.92/23.91 inference(scs_inference,[],[729,98,760,2,10])).
% 23.92/23.91 cnf(808,plain,
% 23.92/23.91 (E(a3,f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[729,98,760,223,2,10,3])).
% 23.92/23.91 cnf(809,plain,
% 23.92/23.91 (P1(f12(a7,a2),a3,a3)),
% 23.92/23.91 inference(scs_inference,[],[388,729,789,98,760,223,2,10,3,12])).
% 23.92/23.91 cnf(810,plain,
% 23.92/23.91 (P2(f12(a7,a2),x8101,f12(f5(a3),x8101))),
% 23.92/23.91 inference(scs_inference,[],[388,729,789,450,144,98,760,223,2,10,3,12,13])).
% 23.92/23.91 cnf(814,plain,
% 23.92/23.91 (P1(f4(a7,a7),f4(f5(a3),f12(a7,a2)),f4(a7,a7))),
% 23.92/23.91 inference(scs_inference,[],[45,388,729,714,789,342,275,303,450,144,98,760,756,223,191,2,10,3,12,13,14,11,15,35])).
% 23.92/23.91 cnf(816,plain,
% 23.92/23.91 (P1(f12(a7,a2),f12(f4(a7,a7),a2),a3)),
% 23.92/23.91 inference(scs_inference,[],[45,388,729,714,789,509,764,342,275,303,450,144,98,760,756,223,191,2,10,3,12,13,14,11,15,35,36])).
% 23.92/23.91 cnf(818,plain,
% 23.92/23.91 (P2(a3,f5(a3),f12(f12(a7,a2),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[45,388,729,714,789,509,764,342,188,275,303,161,454,450,144,98,760,756,223,191,2,10,3,12,13,14,11,15,35,36,38])).
% 23.92/23.91 cnf(825,plain,
% 23.92/23.91 (E(a3,f12(f5(a3),a11))),
% 23.92/23.91 inference(scs_inference,[],[21,450,625,2,34])).
% 23.92/23.91 cnf(826,plain,
% 23.92/23.91 (P2(a3,x8261,f12(f5(a3),x8261))),
% 23.92/23.91 inference(rename_variables,[],[450])).
% 23.92/23.91 cnf(827,plain,
% 23.92/23.91 (P2(x8271,a11,x8271)),
% 23.92/23.91 inference(rename_variables,[],[21])).
% 23.92/23.91 cnf(829,plain,
% 23.92/23.91 (P1(f4(a8,a10),f12(f4(a7,a7),a2),a3)),
% 23.92/23.91 inference(scs_inference,[],[726,816,21,450,625,2,34,10])).
% 23.92/23.91 cnf(831,plain,
% 23.92/23.91 (E(f5(a3),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[102,726,807,816,21,450,193,625,808,2,34,10,12,3])).
% 23.92/23.91 cnf(832,plain,
% 23.92/23.91 (P2(f4(f12(a11,a1),a6),f4(a2,a2),a3)),
% 23.92/23.91 inference(scs_inference,[],[102,726,807,816,21,450,686,193,625,808,2,34,10,12,3,13])).
% 23.92/23.91 cnf(835,plain,
% 23.92/23.91 (P2(a3,a11,f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[102,726,814,807,816,21,161,157,450,686,193,625,756,387,808,2,34,10,12,3,13,14,11,15])).
% 23.92/23.91 cnf(836,plain,
% 23.92/23.91 (P1(a6,f5(a3),a6)),
% 23.92/23.91 inference(scs_inference,[],[102,726,814,807,816,243,113,21,161,157,450,686,193,625,756,387,808,2,34,10,12,3,13,14,11,15,35])).
% 23.92/23.91 cnf(838,plain,
% 23.92/23.91 (P1(a3,f12(a7,f4(a2,a2)),a3)),
% 23.92/23.91 inference(scs_inference,[],[102,726,814,807,816,786,243,165,113,21,161,157,450,686,193,625,756,387,808,2,34,10,12,3,13,14,11,15,35,36])).
% 23.92/23.91 cnf(841,plain,
% 23.92/23.91 (P2(x8411,a11,x8411)),
% 23.92/23.91 inference(rename_variables,[],[21])).
% 23.92/23.91 cnf(844,plain,
% 23.92/23.91 (P1(a3,a3,f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[18,102,726,814,807,816,786,243,165,113,21,827,841,161,26,27,157,450,826,686,193,625,756,387,808,2,34,10,12,3,13,14,11,15,35,36,38,39])).
% 23.92/23.91 cnf(860,plain,
% 23.92/23.91 (P1(f12(a7,a2),f12(a7,f4(a2,a2)),a3)),
% 23.92/23.91 inference(scs_inference,[],[838,144,664,2,10])).
% 23.92/23.91 cnf(862,plain,
% 23.92/23.91 (P2(f4(a8,a10),a11,f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[726,829,838,730,144,664,2,10,12,13])).
% 23.92/23.91 cnf(863,plain,
% 23.92/23.91 (E(f4(x8631,f5(x8631)),f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[445,726,829,838,730,144,664,831,2,10,12,13,3])).
% 23.92/23.91 cnf(864,plain,
% 23.92/23.91 (P2(a3,f4(a8,a10),f12(f5(a3),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[445,726,829,838,730,144,664,630,831,2,10,12,13,3,14])).
% 23.92/23.91 cnf(866,plain,
% 23.92/23.91 (P2(a11,f12(a7,a2),f12(f4(a7,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[102,445,726,757,829,838,365,730,144,664,756,630,831,2,10,12,13,3,14,11,15])).
% 23.92/23.91 cnf(867,plain,
% 23.92/23.91 (P1(f5(a3),f12(a7,f4(a2,a2)),f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[102,445,726,757,829,838,201,365,730,144,664,756,630,831,2,10,12,13,3,14,11,15,35])).
% 23.92/23.91 cnf(869,plain,
% 23.92/23.91 (P2(x8691,f5(a3),f12(f12(x8691,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[102,445,726,757,829,838,201,365,194,496,27,730,144,664,756,630,831,2,10,12,13,3,14,11,15,35,38])).
% 23.92/23.91 cnf(872,plain,
% 23.92/23.91 (P1(f4(a7,a3),f12(f4(a7,a7),a2),f4(a7,a3))),
% 23.92/23.91 inference(scs_inference,[],[102,445,726,757,829,838,461,789,201,20,365,194,496,27,730,144,664,756,630,831,2,10,12,13,3,14,11,15,35,38,36])).
% 23.92/23.91 cnf(875,plain,
% 23.92/23.91 (E(f4(a8,a10),f12(f12(a11,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[102,445,726,757,829,838,461,789,201,20,365,194,496,394,27,730,144,664,756,630,831,2,10,12,13,3,14,11,15,35,38,36,34])).
% 23.92/23.91 cnf(887,plain,
% 23.92/23.91 (E(f12(f5(a3),f4(a11,a11)),a3)),
% 23.92/23.91 inference(scs_inference,[],[844,22,555,2,33])).
% 23.92/23.91 cnf(890,plain,
% 23.92/23.91 (P1(f12(a7,a2),a3,f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[844,22,144,555,2,33,10])).
% 23.92/23.91 cnf(892,plain,
% 23.92/23.91 (P2(f4(a8,a10),x8921,f12(f5(a3),x8921))),
% 23.92/23.91 inference(scs_inference,[],[102,726,844,867,22,144,810,555,2,33,10,12,13])).
% 23.92/23.91 cnf(893,plain,
% 23.92/23.91 (E(f5(a3),f12(f5(a3),a11))),
% 23.92/23.91 inference(scs_inference,[],[102,726,844,867,22,144,810,555,825,2,33,10,12,13,3])).
% 23.92/23.91 cnf(894,plain,
% 23.92/23.91 (P2(f12(a7,a2),a3,f12(f5(a3),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[102,726,844,867,22,144,810,555,825,2,33,10,12,13,3,14])).
% 23.92/23.91 cnf(896,plain,
% 23.92/23.91 (P1(a3,f12(a7,a2),f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[102,726,844,867,22,144,810,555,825,2,33,10,12,13,3,14,11])).
% 23.92/23.91 cnf(898,plain,
% 23.92/23.91 (P1(a1,f12(a7,f4(a2,a2)),a1)),
% 23.92/23.91 inference(scs_inference,[],[102,726,844,867,458,22,109,144,810,555,756,825,2,33,10,12,13,3,14,11,15,35])).
% 23.92/23.91 cnf(900,plain,
% 23.92/23.91 (P1(a6,f12(f5(a3),f4(a11,a11)),a6)),
% 23.92/23.91 inference(scs_inference,[],[102,726,844,836,867,458,491,427,22,109,144,810,555,756,825,2,33,10,12,13,3,14,11,15,35,36])).
% 23.92/23.91 cnf(902,plain,
% 23.92/23.91 (P2(x9021,f4(a8,a10),f12(f12(x9021,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[102,726,844,836,867,458,491,427,22,109,496,27,144,810,555,756,825,2,33,10,12,13,3,14,11,15,35,36,38])).
% 23.92/23.91 cnf(905,plain,
% 23.92/23.91 (E(f12(a7,a2),f12(f12(a11,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[102,726,844,836,867,458,491,427,236,22,109,496,27,144,810,555,756,825,2,33,10,12,13,3,14,11,15,35,36,38,34])).
% 23.92/23.91 cnf(920,plain,
% 23.92/23.91 (E(f4(a8,a10),f12(f5(a3),a11))),
% 23.92/23.91 inference(scs_inference,[],[887,21,892,2,34])).
% 23.92/23.91 cnf(921,plain,
% 23.92/23.91 (P2(f4(a8,a10),x9211,f12(f5(a3),x9211))),
% 23.92/23.91 inference(rename_variables,[],[892])).
% 23.92/23.91 cnf(922,plain,
% 23.92/23.91 (P2(x9221,a11,x9221)),
% 23.92/23.91 inference(rename_variables,[],[21])).
% 23.92/23.91 cnf(924,plain,
% 23.92/23.91 (P1(f4(a8,a10),f12(a7,f4(a2,a2)),a3)),
% 23.92/23.91 inference(scs_inference,[],[726,860,887,21,892,2,34,10])).
% 23.92/23.91 cnf(928,plain,
% 23.92/23.91 (E(f5(a3),f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[45,102,726,860,887,21,463,144,892,2,34,10,12,13,3])).
% 23.92/23.91 cnf(929,plain,
% 23.92/23.91 (P2(f4(a1,a6),f4(a1,a6),f12(a7,a7))),
% 23.92/23.91 inference(scs_inference,[],[45,102,726,860,887,21,463,588,144,892,2,34,10,12,13,3,14])).
% 23.92/23.91 cnf(933,plain,
% 23.92/23.91 (P1(a7,f12(f5(a3),f4(a11,a11)),a7)),
% 23.92/23.91 inference(scs_inference,[],[16,45,102,726,860,887,597,900,21,463,394,588,144,756,892,2,34,10,12,13,3,14,11,15,35])).
% 23.92/23.91 cnf(935,plain,
% 23.92/23.91 (P1(f4(a8,a10),a3,f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[16,45,102,726,860,887,597,900,706,21,463,394,588,144,756,892,687,2,34,10,12,13,3,14,11,15,35,36])).
% 23.92/23.91 cnf(941,plain,
% 23.92/23.91 (P1(f4(a8,a10),f4(a8,a10),f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[16,18,45,102,726,860,887,597,900,706,21,922,26,463,496,394,27,588,144,756,892,921,687,2,34,10,12,13,3,14,11,15,35,36,38,39])).
% 23.92/23.91 cnf(953,plain,
% 23.92/23.91 (E(f12(a7,a11),a7)),
% 23.92/23.91 inference(scs_inference,[],[634,2])).
% 23.92/23.91 cnf(954,plain,
% 23.92/23.91 (P1(f12(f4(a7,a7),a2),a3,f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[935,634,756,2,10])).
% 23.92/23.91 cnf(956,plain,
% 23.92/23.91 (P2(f4(f12(a11,a1),a6),f4(a1,a6),f12(a7,a7))),
% 23.92/23.91 inference(scs_inference,[],[45,935,924,144,758,634,756,2,10,12,14])).
% 23.92/23.91 cnf(961,plain,
% 23.92/23.91 (P2(a3,f4(a11,a11),a3)),
% 23.92/23.91 inference(scs_inference,[],[45,935,924,887,530,450,144,758,634,756,2,10,12,14,13,11,15])).
% 23.92/23.91 cnf(963,plain,
% 23.92/23.91 (P1(f4(a1,a6),f12(f5(a3),f4(a11,a11)),a7)),
% 23.92/23.91 inference(scs_inference,[],[45,48,935,924,887,306,530,450,144,758,634,756,896,2,10,12,14,13,11,15,36])).
% 23.92/23.91 cnf(969,plain,
% 23.92/23.91 (P1(a3,f4(a8,a10),a3)),
% 23.92/23.91 inference(scs_inference,[],[18,45,48,935,924,887,306,279,454,530,27,450,144,758,634,756,708,896,2,10,12,14,13,11,15,36,38,35])).
% 23.92/23.91 cnf(976,plain,
% 23.92/23.91 (P1(f4(a8,a10),a3,f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[726,890,863,2,10])).
% 23.92/23.91 cnf(978,plain,
% 23.92/23.91 (P2(x9781,a3,f12(f12(x9781,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[45,102,726,890,963,869,863,2,10,12,14])).
% 23.92/23.91 cnf(983,plain,
% 23.92/23.91 (P2(a6,f12(a2,a11),a10)),
% 23.92/23.91 inference(scs_inference,[],[18,45,102,726,890,963,954,21,761,27,730,144,869,863,2,10,12,14,13,11,15,38])).
% 23.92/23.91 cnf(987,plain,
% 23.92/23.91 (P1(a3,f12(f4(a7,a7),a2),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[18,45,102,726,890,963,954,347,21,761,27,730,144,869,863,2,10,12,14,13,11,15,38,36])).
% 23.92/23.91 cnf(989,plain,
% 23.92/23.91 (P1(a7,f4(a8,a10),a7)),
% 23.92/23.91 inference(scs_inference,[],[18,45,102,48,726,890,963,954,969,347,21,761,27,730,144,869,863,2,10,12,14,13,11,15,38,36,35])).
% 23.92/23.91 cnf(991,plain,
% 23.92/23.91 (E(f5(a3),f12(f12(a11,a7),a2))),
% 23.92/23.91 inference(scs_inference,[],[18,45,102,48,726,890,963,954,969,347,188,21,761,27,730,144,869,863,2,10,12,14,13,11,15,38,36,35,34])).
% 23.92/23.91 cnf(998,plain,
% 23.92/23.91 (P1(f12(a7,a2),f12(f4(a7,a7),a2),f12(a7,a2))),
% 23.92/23.91 inference(scs_inference,[],[987,144,920,2,10])).
% 23.92/23.91 cnf(999,plain,
% 23.92/23.91 (P1(f4(a8,a10),a3,a3)),
% 23.92/23.91 inference(scs_inference,[],[887,976,987,144,920,2,10,12])).
% 23.92/23.91 cnf(1003,plain,
% 23.92/23.91 (P2(f12(a7,a2),a11,f4(a8,a10))),
% 23.92/23.91 inference(scs_inference,[],[45,488,887,898,976,987,835,144,920,810,2,10,12,14,11,13])).
% 23.92/23.91 cnf(1005,plain,
% 23.92/23.91 (P1(f4(f12(a11,a1),a6),f12(a7,a2),a7)),
% 23.92/23.91 inference(scs_inference,[],[45,488,887,898,976,987,559,673,763,835,144,756,920,810,2,10,12,14,11,13,15,36])).
% 23.92/23.91 cnf(1010,plain,
% 23.92/23.91 (P1(f5(a3),f4(a8,a10),f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[45,488,887,898,976,987,559,673,969,201,236,190,761,763,835,144,756,920,810,2,10,12,14,11,13,15,36,38,35])).
% 23.92/23.91 cnf(1026,plain,
% 23.92/23.91 (P1(f4(a1,a6),f4(a8,a10),a7)),
% 23.92/23.91 inference(scs_inference,[],[45,989,875,2,10])).
% 23.92/23.91 cnf(1036,plain,
% 23.92/23.91 (P1(f4(f12(a11,a1),a6),f5(a3),a7)),
% 23.92/23.91 inference(scs_inference,[],[45,726,998,989,1005,398,243,161,275,454,835,862,756,875,892,2,10,14,12,13,11,15,38,36])).
% 23.92/23.91 cnf(1038,plain,
% 23.92/23.91 (P1(a6,f4(a8,a10),a6)),
% 23.92/23.91 inference(scs_inference,[],[45,726,998,989,1005,1010,398,836,243,161,275,454,835,862,756,875,892,2,10,14,12,13,11,15,38,36,35])).
% 23.92/23.91 cnf(1049,plain,
% 23.92/23.91 (E(f4(a8,a10),a3)),
% 23.92/23.91 inference(scs_inference,[],[808,2])).
% 23.92/23.91 cnf(1052,plain,
% 23.92/23.91 (P2(f4(a8,a10),a3,f12(f5(a3),f5(a3)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,1026,1036,193,808,892,2,10,12,14])).
% 23.92/23.91 cnf(1055,plain,
% 23.92/23.91 (P2(f12(a7,a2),f4(a11,a11),a3)),
% 23.92/23.91 inference(scs_inference,[],[102,45,1026,1036,1038,193,144,756,808,892,961,2,10,12,14,11,13])).
% 23.92/23.91 cnf(1057,plain,
% 23.92/23.91 (P1(f4(a8,a10),f12(a7,a2),f12(f5(a3),f4(a11,a11)))),
% 23.92/23.91 inference(scs_inference,[],[102,45,941,1026,1036,1038,935,20,661,193,144,756,808,892,961,2,10,12,14,11,13,15,36])).
% 23.92/23.91 cnf(1063,plain,
% 23.92/23.91 (P1(f4(a7,a3),f4(a8,a10),f4(a7,a3))),
% 23.92/23.91 inference(scs_inference,[],[102,45,66,941,1026,1036,1038,935,20,190,496,58,661,193,144,756,808,892,961,2,10,12,14,11,13,15,36,38,35])).
% 23.92/23.91 cnf(1069,plain,
% 23.92/23.91 (P2(f12(a7,a2),f12(a7,a2),f12(f12(a7,a2),f4(a8,a10)))),
% 23.92/23.91 inference(scs_inference,[],[887,1057,147,193,144,831,978,707,2,10,14,12,13])).
% 23.92/23.91 cnf(1071,plain,
% 23.92/23.91 (P2(f4(a8,a10),a11,a3)),
% 23.92/23.91 inference(scs_inference,[],[102,887,1057,147,169,862,193,144,831,978,707,97,2,10,14,12,13,11,15])).
% 23.92/23.91 cnf(1072,plain,
% 23.92/23.91 (P2(a11,f12(f5(a3),a11),f5(a3))),
% 23.92/23.91 inference(scs_inference,[],[102,887,1057,147,169,21,188,450,862,193,144,831,978,707,97,2,10,14,12,13,11,15,38])).
% 23.92/23.91 cnf(1076,plain,
% 23.92/23.91 (P1(f4(a8,a10),a3,f4(f4(a8,a10),f12(a7,a2)))),
% 23.92/23.91 inference(scs_inference,[],[102,887,1057,780,147,169,20,21,188,450,862,193,144,831,978,707,999,97,2,10,14,12,13,11,15,38,36])).
% 23.92/23.92 cnf(1079,plain,
% 23.92/23.92 (P1(a1,f4(a8,a10),a1)),
% 23.92/23.92 inference(scs_inference,[],[102,887,1057,780,147,169,1010,458,20,21,188,450,862,193,144,831,978,707,999,97,2,10,14,12,13,11,15,38,36,35])).
% 23.92/23.92 cnf(1093,plain,
% 23.92/23.92 (P1(f4(a8,a10),f12(a7,a2),f12(f4(a7,a7),a2))),
% 23.92/23.92 inference(scs_inference,[],[726,605,825,2,10])).
% 23.92/23.92 cnf(1096,plain,
% 23.92/23.92 (P2(f4(a8,a10),f12(a7,a2),f12(f12(a7,a2),f4(a8,a10)))),
% 23.92/23.92 inference(scs_inference,[],[45,726,933,605,825,1069,866,2,10,14,12,13])).
% 23.92/23.92 cnf(1099,plain,
% 23.92/23.92 (P1(f12(a7,a2),f4(f4(a8,a10),f12(a7,a2)),a3)),
% 23.92/23.92 inference(scs_inference,[],[45,726,685,1076,1079,933,605,786,736,756,825,1069,866,2,10,14,12,13,15,11,36])).
% 23.92/23.92 cnf(1104,plain,
% 23.92/23.92 (P1(f5(a3),f12(f4(a7,a7),a2),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[45,726,685,1076,1079,933,998,605,786,277,161,236,761,736,756,825,1069,866,2,10,14,12,13,15,11,36,38,35])).
% 23.92/23.92 cnf(1107,plain,
% 23.92/23.92 (P1(a3,f12(f4(a7,a7),a2),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[102,1104,905,2,10])).
% 23.92/23.92 cnf(1111,plain,
% 23.92/23.92 (P2(f12(a7,a2),f4(a8,a10),f12(f5(a3),f5(a3)))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1093,1104,144,1096,905,864,2,10,14,12,11,13])).
% 23.92/23.92 cnf(1113,plain,
% 23.92/23.92 (P2(x11131,f12(a7,a11),f12(x11131,a7))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1093,1104,21,496,588,781,144,1096,905,864,2,10,14,12,11,13,15,38])).
% 23.92/23.92 cnf(1119,plain,
% 23.92/23.92 (P1(f4(a8,a10),f12(f4(a7,a7),a2),f4(a8,a10))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1063,1093,1104,1057,461,998,21,496,588,781,144,1096,905,665,864,2,10,14,12,11,13,15,38,36,35])).
% 23.92/23.92 cnf(1121,plain,
% 23.92/23.92 (P1(f12(a7,a11),f12(a7,a11),f12(f4(a11,a11),a7))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1063,1093,1104,1057,461,998,21,496,26,23,588,781,144,1096,905,665,864,2,10,14,12,11,13,15,38,36,35,40])).
% 23.92/23.92 cnf(1127,plain,
% 23.92/23.92 (E(f12(a7,a11),f12(a11,a7))),
% 23.92/23.92 inference(scs_inference,[],[23,893,1113,2,34])).
% 23.92/23.92 cnf(1131,plain,
% 23.92/23.92 (P1(f4(a8,a10),f4(f4(a8,a10),f12(a7,a2)),a3)),
% 23.92/23.92 inference(scs_inference,[],[726,1099,23,893,1113,2,34,10])).
% 23.92/23.92 cnf(1135,plain,
% 23.92/23.92 (P1(a3,f12(a7,a2),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[102,726,654,1099,1107,23,396,144,893,716,1113,2,34,10,14,12,15,11])).
% 23.92/23.92 cnf(1137,plain,
% 23.92/23.92 (P1(f4(a8,a10),f12(f5(a3),f4(a11,a11)),f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[102,726,654,1099,1107,1093,890,954,23,396,144,1111,893,716,1113,2,34,10,14,12,15,11,13,36])).
% 23.92/23.92 cnf(1139,plain,
% 23.92/23.92 (P2(a11,f12(f5(a3),a11),f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[102,726,654,1099,1107,1093,890,954,190,188,23,450,396,144,1111,893,716,1113,2,34,10,14,12,15,11,13,36,38])).
% 23.92/23.92 cnf(1142,plain,
% 23.92/23.92 (P1(a3,f12(f4(a7,a7),a2),a3)),
% 23.92/23.92 inference(scs_inference,[],[102,726,654,1119,1099,1107,1093,890,969,954,190,188,23,450,396,144,1111,893,716,1113,2,34,10,14,12,15,11,13,36,38,35])).
% 23.92/23.92 cnf(1157,plain,
% 23.92/23.92 (P1(a7,f12(a7,a11),f12(f4(a11,a11),a7))),
% 23.92/23.92 inference(scs_inference,[],[1121,953,1127,2,10])).
% 23.92/23.92 cnf(1161,plain,
% 23.92/23.92 (P2(a6,f12(a2,a11),f12(a6,a2))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1137,1121,983,953,1127,818,295,2,10,14,12,11,15])).
% 23.92/23.92 cnf(1167,plain,
% 23.92/23.92 (P1(f4(a1,a6),a3,f4(a7,f4(a8,a10)))),
% 23.92/23.92 inference(scs_inference,[],[45,102,726,1137,1121,737,20,161,496,58,902,983,953,1127,818,809,295,2,10,14,12,11,15,13,38,36])).
% 23.92/23.92 cnf(1170,plain,
% 23.92/23.92 (P1(a3,a3,f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[45,102,726,1137,1121,1142,737,954,20,22,161,496,58,902,983,953,1127,818,809,295,2,10,14,12,11,15,13,38,36,35])).
% 23.92/23.92 cnf(1186,plain,
% 23.92/23.92 (P2(f12(a7,a2),a11,f12(f4(a7,a7),a2))),
% 23.92/23.92 inference(scs_inference,[],[45,102,1131,1157,692,869,1003,144,756,991,894,2,10,14,12,11,13,15])).
% 23.92/23.92 cnf(1190,plain,
% 23.92/23.92 (P1(f4(a1,a6),f5(a3),f4(a1,a6))),
% 23.92/23.92 inference(scs_inference,[],[45,102,48,1131,1157,692,503,496,869,929,1003,144,756,991,894,1135,2,10,14,12,11,13,15,38,36])).
% 23.92/23.92 cnf(1197,plain,
% 23.92/23.92 (P1(a3,f12(a7,a2),f12(f4(a11,a11),f5(a3)))),
% 23.92/23.92 inference(scs_inference,[],[102,526,928,2,10])).
% 23.92/23.92 cnf(1209,plain,
% 23.92/23.92 (E(f12(a7,a7),f12(f12(a11,a7),a7))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1190,807,526,737,277,496,530,23,956,783,193,144,756,1113,928,1052,2,10,14,12,11,15,13,36,38,34])).
% 23.92/23.92 cnf(1220,plain,
% 23.92/23.92 (E(f12(f12(a11,a7),a7),f12(a7,a7))),
% 23.92/23.92 inference(scs_inference,[],[1209,2])).
% 23.92/23.92 cnf(1221,plain,
% 23.92/23.92 (E(f12(x12211,f12(a7,a11)),f12(x12211,a7))),
% 23.92/23.92 inference(scs_inference,[],[27,1113,1209,2,34])).
% 23.92/23.92 cnf(1223,plain,
% 23.92/23.92 (P2(x12231,x12232,f12(x12231,x12232))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(1226,plain,
% 23.92/23.92 (P2(a3,a3,f12(f12(a7,a2),f12(a7,a2)))),
% 23.92/23.92 inference(scs_inference,[],[102,726,363,27,1113,602,1209,2,34,10,14])).
% 23.92/23.92 cnf(1227,plain,
% 23.92/23.92 (P1(a3,a3,f4(a8,a10))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1170,363,27,1113,602,1209,2,34,10,14,12])).
% 23.92/23.92 cnf(1228,plain,
% 23.92/23.92 (P2(f4(a1,a6),a3,f12(f12(a7,a7),a2))),
% 23.92/23.92 inference(scs_inference,[],[45,102,726,1170,363,27,978,1113,602,1209,2,34,10,14,12,13])).
% 23.92/23.92 cnf(1232,plain,
% 23.92/23.92 (P2(x12321,f12(a1,a2),f12(x12321,a8))),
% 23.92/23.92 inference(scs_inference,[],[45,102,726,1170,363,398,21,70,27,1223,929,978,1113,602,1209,2,34,10,14,12,13,11,15,38])).
% 23.92/23.92 cnf(1236,plain,
% 23.92/23.92 (P1(f5(a1),f4(a1,a6),a6)),
% 23.92/23.92 inference(scs_inference,[],[45,102,726,1170,363,398,807,1038,113,21,70,27,1223,929,978,1113,602,1209,2,34,10,14,12,13,11,15,38,36])).
% 23.92/23.92 cnf(1247,plain,
% 23.92/23.92 (E(f12(x12471,a7),f12(x12471,f12(a7,a11)))),
% 23.92/23.92 inference(scs_inference,[],[1221,2])).
% 23.92/23.92 cnf(1248,plain,
% 23.92/23.92 (E(f12(x12481,f12(a1,a2)),f12(x12481,a8))),
% 23.92/23.92 inference(scs_inference,[],[27,1232,1221,2,34])).
% 23.92/23.92 cnf(1250,plain,
% 23.92/23.92 (P2(x12501,x12502,f12(x12501,x12502))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(1252,plain,
% 23.92/23.92 (P1(f12(a7,a2),f12(f4(a7,a7),a2),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[1107,27,144,1232,1221,2,34,10])).
% 23.92/23.92 cnf(1253,plain,
% 23.92/23.92 (E(f12(f12(a11,a7),f12(a7,a11)),f12(a7,a7))),
% 23.92/23.92 inference(scs_inference,[],[1107,27,144,1220,1232,1221,2,34,10,3])).
% 23.92/23.92 cnf(1259,plain,
% 23.92/23.92 (P2(a11,f12(a7,f4(a2,a2)),f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[726,987,1107,764,27,532,144,756,1071,1220,1232,1221,1228,2,34,10,3,14,12,11,13,15])).
% 23.92/23.92 cnf(1263,plain,
% 23.92/23.92 (P2(x12631,f12(a6,a2),f12(x12631,a10))),
% 23.92/23.92 inference(scs_inference,[],[726,987,1107,1190,764,127,21,26,205,27,1250,532,144,756,1071,1220,1232,1221,1228,2,34,10,3,14,12,11,13,15,36,38])).
% 23.92/23.92 cnf(1280,plain,
% 23.92/23.92 (E(f12(a7,a7),f12(f12(a11,a7),f12(a7,a11)))),
% 23.92/23.92 inference(scs_inference,[],[1253,2])).
% 23.92/23.92 cnf(1281,plain,
% 23.92/23.92 (E(f12(x12811,f12(a6,a2)),f12(x12811,a10))),
% 23.92/23.92 inference(scs_inference,[],[27,1253,1263,2,34])).
% 23.92/23.92 cnf(1283,plain,
% 23.92/23.92 (P2(x12831,x12832,f12(x12831,x12832))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(1285,plain,
% 23.92/23.92 (P1(a3,f12(a7,f4(a2,a2)),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[102,867,27,1253,1263,2,34,10])).
% 23.92/23.92 cnf(1286,plain,
% 23.92/23.92 (E(a7,f12(a11,f12(a7,a11)))),
% 23.92/23.92 inference(scs_inference,[],[102,867,27,523,1253,1263,1247,2,34,10,3])).
% 23.92/23.92 cnf(1287,plain,
% 23.92/23.92 (E(f12(x12871,a7),f12(x12871,f12(a7,a11)))),
% 23.92/23.92 inference(rename_variables,[],[1247])).
% 23.92/23.92 cnf(1291,plain,
% 23.92/23.92 (P2(f4(a1,a6),f12(a7,a11),f12(a7,a7))),
% 23.92/23.92 inference(scs_inference,[],[45,102,726,660,867,786,27,144,523,756,1113,1253,1263,1247,376,2,34,10,3,14,12,11,13])).
% 23.92/23.92 cnf(1298,plain,
% 23.92/23.92 (P2(a11,a3,f12(a7,f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[45,102,726,660,867,786,1190,187,26,58,27,1283,929,686,144,523,756,1113,1253,1263,1247,1287,376,2,34,10,3,14,12,11,13,15,36,38])).
% 23.92/23.92 cnf(1314,plain,
% 23.92/23.92 (E(f12(x13141,a10),f12(x13141,f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[1281,2])).
% 23.92/23.92 cnf(1315,plain,
% 23.92/23.92 (E(f4(a1,a6),f12(a11,f12(a7,a11)))),
% 23.92/23.92 inference(scs_inference,[],[591,1281,1247,2,3])).
% 23.92/23.92 cnf(1322,plain,
% 23.92/23.92 (P2(f4(a8,a10),f4(a11,a11),a3)),
% 23.92/23.92 inference(scs_inference,[],[102,726,838,1010,245,929,144,591,1055,1280,1281,688,1247,2,3,10,14,12,11,15,13])).
% 23.92/23.92 cnf(1326,plain,
% 23.92/23.92 (P2(x13261,a3,f12(f12(x13261,a7),f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[102,726,838,1010,245,187,113,26,530,27,929,144,591,832,1055,1280,1281,688,1247,2,3,10,14,12,11,15,13,36,38])).
% 23.92/23.92 cnf(1329,plain,
% 23.92/23.92 (E(f5(a3),f12(f12(a11,a7),f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[102,726,838,1010,245,187,113,188,26,530,27,929,144,591,832,1055,1280,1281,688,1247,2,3,10,14,12,11,15,13,36,38,34])).
% 23.92/23.92 cnf(1337,plain,
% 23.92/23.92 (E(f12(a6,a2),f12(a11,a10))),
% 23.92/23.92 inference(scs_inference,[],[23,1263,1315,2,34])).
% 23.92/23.92 cnf(1338,plain,
% 23.92/23.92 (P2(x13381,f12(a6,a2),f12(x13381,a10))),
% 23.92/23.92 inference(rename_variables,[],[1263])).
% 23.92/23.92 cnf(1339,plain,
% 23.92/23.92 (P2(a11,x13391,x13391)),
% 23.92/23.92 inference(rename_variables,[],[23])).
% 23.92/23.92 cnf(1341,plain,
% 23.92/23.92 (E(a10,f12(a11,a10))),
% 23.92/23.92 inference(scs_inference,[],[23,1263,1315,295,2,34,3])).
% 23.92/23.92 cnf(1342,plain,
% 23.92/23.92 (P1(f4(a1,a6),f4(f5(a3),f12(a7,a2)),a7)),
% 23.92/23.92 inference(scs_inference,[],[45,342,23,1263,1315,295,2,34,3,10])).
% 23.92/23.92 cnf(1343,plain,
% 23.92/23.92 (P2(a11,f12(a7,a2),f12(a7,f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[45,342,23,144,1263,1315,1298,295,2,34,3,10,14])).
% 23.92/23.92 cnf(1344,plain,
% 23.92/23.92 (P1(f5(a3),f5(a3),a3)),
% 23.92/23.92 inference(scs_inference,[],[45,102,209,342,23,144,1263,1315,1298,295,2,34,3,10,14,12])).
% 23.92/23.92 cnf(1347,plain,
% 23.92/23.92 (P2(f4(a1,a6),f12(a6,a2),f12(a7,a10))),
% 23.92/23.92 inference(scs_inference,[],[45,102,209,342,201,23,566,144,1263,1338,1315,1298,295,2,34,3,10,14,12,11,15,13])).
% 23.92/23.92 cnf(1348,plain,
% 23.92/23.92 (P2(x13481,f12(a6,a2),f12(x13481,a10))),
% 23.92/23.92 inference(rename_variables,[],[1263])).
% 23.92/23.92 cnf(1349,plain,
% 23.92/23.92 (P1(f4(a1,a6),f12(f4(a11,a11),f5(a3)),a7)),
% 23.92/23.92 inference(scs_inference,[],[48,45,102,209,342,306,201,1197,23,566,144,1263,1338,1315,1298,295,2,34,3,10,14,12,11,15,13,36])).
% 23.92/23.92 cnf(1355,plain,
% 23.92/23.92 (P1(f12(a6,a2),f12(a6,a2),f12(f4(a11,a11),a10))),
% 23.92/23.92 inference(scs_inference,[],[18,48,45,102,209,342,306,201,1197,26,23,1339,27,566,144,1113,1263,1338,1348,1315,1298,295,2,34,3,10,14,12,11,15,13,36,38,40])).
% 23.92/23.92 cnf(1374,plain,
% 23.92/23.92 (E(f12(x13741,a8),f12(x13741,f12(a1,a2)))),
% 23.92/23.92 inference(scs_inference,[],[1248,2])).
% 23.92/23.92 cnf(1375,plain,
% 23.92/23.92 (P1(f4(a8,a10),f5(a3),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[398,726,1248,2,10])).
% 23.92/23.92 cnf(1376,plain,
% 23.92/23.92 (E(f12(a6,a2),f12(a11,f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[398,726,1314,1248,1337,2,10,3])).
% 23.92/23.92 cnf(1378,plain,
% 23.92/23.92 (P2(x13781,f12(a11,a10),f12(x13781,a10))),
% 23.92/23.92 inference(scs_inference,[],[398,726,1263,1314,1248,1337,2,10,3,14])).
% 23.92/23.92 cnf(1382,plain,
% 23.92/23.92 (P2(f12(a11,a10),a11,f12(a6,a2))),
% 23.92/23.92 inference(scs_inference,[],[18,398,1010,127,102,726,205,193,1263,1314,1248,1337,1341,2,10,3,14,11,12,15,13])).
% 23.92/23.92 cnf(1386,plain,
% 23.92/23.92 (P2(f4(a1,a6),a10,f12(f12(a7,a6),a2))),
% 23.92/23.92 inference(scs_inference,[],[18,398,1010,127,102,726,1167,20,205,588,27,193,1263,1314,1248,1337,1341,2,10,3,14,11,12,15,13,36,38])).
% 23.92/23.92 cnf(1404,plain,
% 23.92/23.92 (E(f12(a1,a2),f12(a11,a8))),
% 23.92/23.92 inference(scs_inference,[],[23,1232,1329,2,34])).
% 23.92/23.92 cnf(1405,plain,
% 23.92/23.92 (P2(x14051,f12(a1,a2),f12(x14051,a8))),
% 23.92/23.92 inference(rename_variables,[],[1232])).
% 23.92/23.92 cnf(1406,plain,
% 23.92/23.92 (P2(a11,x14061,x14061)),
% 23.92/23.92 inference(rename_variables,[],[23])).
% 23.92/23.92 cnf(1409,plain,
% 23.92/23.92 (E(a10,f12(a11,f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[279,23,756,1232,1329,1376,295,2,34,10,3])).
% 23.92/23.92 cnf(1413,plain,
% 23.92/23.92 (P2(a10,a11,f12(a11,f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[764,279,187,205,23,193,144,756,1232,1263,1329,1376,295,2,34,10,3,14,11,12,15])).
% 23.92/23.92 cnf(1414,plain,
% 23.92/23.92 (P2(f4(a1,a6),f12(a1,a2),f12(a7,a8))),
% 23.92/23.92 inference(scs_inference,[],[764,279,187,45,205,23,193,144,756,1232,1405,1263,1329,1376,295,2,34,10,3,14,11,12,15,13])).
% 23.92/23.92 cnf(1415,plain,
% 23.92/23.92 (P2(x14151,f12(a1,a2),f12(x14151,a8))),
% 23.92/23.92 inference(rename_variables,[],[1232])).
% 23.92/23.92 cnf(1417,plain,
% 23.92/23.92 (P1(x14171,x14172,f4(x14171,x14172))),
% 23.92/23.92 inference(rename_variables,[],[26])).
% 23.92/23.92 cnf(1419,plain,
% 23.92/23.92 (P2(a11,a3,f12(f5(a3),f4(a11,a11)))),
% 23.92/23.92 inference(scs_inference,[],[764,279,187,113,45,237,188,26,205,23,27,193,144,756,961,1232,1405,1263,1329,1376,295,2,34,10,3,14,11,12,15,13,36,38])).
% 23.92/23.92 cnf(1422,plain,
% 23.92/23.92 (P1(f12(a1,a2),f12(a1,a2),f12(f4(a11,a11),a8))),
% 23.92/23.92 inference(scs_inference,[],[764,279,187,113,45,237,188,26,1417,205,23,1406,27,193,144,756,961,1232,1405,1415,1263,1329,1376,295,2,34,10,3,14,11,12,15,13,36,38,40])).
% 23.92/23.92 cnf(1440,plain,
% 23.92/23.92 (E(f12(a11,a8),f12(a1,a2))),
% 23.92/23.92 inference(scs_inference,[],[1404,2])).
% 23.92/23.92 cnf(1441,plain,
% 23.92/23.92 (E(f12(a1,a2),f12(a11,f12(a1,a2)))),
% 23.92/23.92 inference(scs_inference,[],[1374,1404,2,3])).
% 23.92/23.92 cnf(1443,plain,
% 23.92/23.92 (P1(f4(a8,a10),f12(a7,a2),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[245,726,1374,1404,2,3,10])).
% 23.92/23.92 cnf(1444,plain,
% 23.92/23.92 (P2(x14441,f12(a11,a8),f12(x14441,a8))),
% 23.92/23.92 inference(scs_inference,[],[245,726,1232,1374,1404,2,3,10,14])).
% 23.92/23.92 cnf(1451,plain,
% 23.92/23.92 (P2(f4(a1,a6),a8,f12(f12(a7,a1),a2))),
% 23.92/23.92 inference(scs_inference,[],[18,17,48,786,503,245,1236,726,1197,205,588,27,193,144,1232,1374,1404,1409,2,3,10,14,12,11,15,13,36,38])).
% 23.92/23.92 cnf(1468,plain,
% 23.92/23.92 (E(f12(a11,a8),a8)),
% 23.92/23.92 inference(scs_inference,[],[1441,1440,97,2,3])).
% 23.92/23.92 cnf(1470,plain,
% 23.92/23.92 (P2(x14701,f12(a7,a2),f12(f12(x14701,a7),f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[127,193,144,1326,1441,1440,97,2,3,10,14])).
% 23.92/23.92 cnf(1473,plain,
% 23.92/23.92 (P2(a8,a11,f12(a11,f12(a1,a2)))),
% 23.92/23.92 inference(scs_inference,[],[243,127,45,102,1375,70,193,144,1326,1441,1440,97,2,3,10,14,12,11,15])).
% 23.92/23.92 cnf(1474,plain,
% 23.92/23.92 (P2(f4(a1,a6),a3,f12(f12(a7,a7),f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[243,127,45,102,1375,70,193,144,1326,1441,1440,97,2,3,10,14,12,11,15,13])).
% 23.92/23.92 cnf(1477,plain,
% 23.92/23.92 (P1(x14771,x14772,f4(x14771,x14772))),
% 23.92/23.92 inference(rename_variables,[],[26])).
% 23.92/23.92 cnf(1483,plain,
% 23.92/23.92 (P1(f12(a11,a10),f12(a11,a10),f12(f4(a11,a11),a10))),
% 23.92/23.92 inference(scs_inference,[],[18,243,127,45,102,1375,26,1477,70,23,27,193,144,151,1326,1232,1378,1441,1440,97,2,3,10,14,12,11,15,13,36,38,40])).
% 23.92/23.92 cnf(1495,plain,
% 23.92/23.92 (E(f12(a11,f12(a1,a2)),a8)),
% 23.92/23.92 inference(scs_inference,[],[1286,1468,1248,2,3])).
% 23.92/23.92 cnf(1498,plain,
% 23.92/23.92 (P2(x14981,f12(a11,f12(a1,a2)),f12(x14981,a8))),
% 23.92/23.92 inference(scs_inference,[],[1252,726,1232,1286,1468,1248,1441,2,3,10,14])).
% 23.92/23.92 cnf(1500,plain,
% 23.92/23.92 (P2(a10,a11,f12(a11,a10))),
% 23.92/23.92 inference(scs_inference,[],[954,1252,726,205,1232,1286,1468,1248,1337,1441,2,3,10,14,12,15])).
% 23.92/23.92 cnf(1525,plain,
% 23.92/23.92 (P1(f12(a7,a2),f12(a7,f4(a2,a2)),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[1285,144,1468,2,10])).
% 23.92/23.92 cnf(1526,plain,
% 23.92/23.92 (P2(f4(a1,a6),f12(a11,a8),f12(a7,a8))),
% 23.92/23.92 inference(scs_inference,[],[1285,144,1414,1468,1404,2,10,14])).
% 23.92/23.92 cnf(1529,plain,
% 23.92/23.92 (P2(a8,a11,f12(a11,a8))),
% 23.92/23.92 inference(scs_inference,[],[277,1285,102,1355,70,144,1414,1468,259,1404,2,10,14,12,11,15])).
% 23.92/23.92 cnf(1533,plain,
% 23.92/23.92 (P1(x15331,x15332,f4(x15331,x15332))),
% 23.92/23.92 inference(rename_variables,[],[26])).
% 23.92/23.92 cnf(1539,plain,
% 23.92/23.92 (P1(f12(a11,a8),f12(a11,a8),f12(f4(a11,a11),a8))),
% 23.92/23.92 inference(scs_inference,[],[18,277,187,1285,45,102,1355,26,1533,70,23,27,151,144,1263,1444,1378,1414,1468,259,1404,2,10,14,12,11,15,13,36,38,40])).
% 23.92/23.92 cnf(1559,plain,
% 23.92/23.92 (P1(f12(f4(a7,a7),a2),f5(a3),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[1375,756,1495,2,10])).
% 23.92/23.92 cnf(1560,plain,
% 23.92/23.92 (P2(f4(a1,a6),f12(a7,a2),f12(f12(a7,a7),f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[1375,144,756,1495,1474,2,10,14])).
% 23.92/23.92 cnf(1582,plain,
% 23.92/23.92 (E(f12(a11,f12(a6,a2)),a10)),
% 23.92/23.92 inference(scs_inference,[],[1409,2])).
% 23.92/23.92 cnf(1583,plain,
% 23.92/23.92 (P1(f12(f4(a7,a7),a2),f12(a7,a2),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[1443,756,1409,2,10])).
% 23.92/23.92 cnf(1596,plain,
% 23.92/23.92 (E(f12(a7,a2),f12(f12(a11,a7),f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[187,45,1342,726,1443,1422,236,26,588,27,983,191,756,1409,97,1322,1470,2,10,14,12,15,11,13,36,38,34])).
% 23.92/23.92 cnf(1614,plain,
% 23.92/23.92 (P2(a11,f12(a7,a11),f4(a1,a6))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1375,1525,1559,1113,725,1337,1560,1582,295,2,3,10,14,12,11,15])).
% 23.92/23.92 cnf(1635,plain,
% 23.92/23.92 (E(f12(a11,a10),a10)),
% 23.92/23.92 inference(scs_inference,[],[1341,2])).
% 23.92/23.92 cnf(1636,plain,
% 23.92/23.92 (E(f12(f5(a3),f12(a7,a11)),f12(a3,a7))),
% 23.92/23.92 inference(scs_inference,[],[450,1113,1341,2,34])).
% 23.92/23.92 cnf(1638,plain,
% 23.92/23.92 (P2(a3,x16381,f12(f5(a3),x16381))),
% 23.92/23.92 inference(rename_variables,[],[450])).
% 23.92/23.92 cnf(1640,plain,
% 23.92/23.92 (E(f12(f5(a3),a7),f12(a3,a7))),
% 23.92/23.92 inference(scs_inference,[],[450,1113,1341,1247,2,34,3])).
% 23.92/23.92 cnf(1653,plain,
% 23.92/23.92 (P2(a3,f12(a1,a2),f12(f5(a3),a8))),
% 23.92/23.92 inference(scs_inference,[],[872,838,102,726,1559,1583,298,21,26,70,450,1638,1113,595,193,144,1227,1341,1347,1386,1247,2,34,3,10,14,12,11,15,13,35,36,38])).
% 23.92/23.92 cnf(1666,plain,
% 23.92/23.92 (E(f12(f5(a3),f12(a1,a2)),f12(a3,a8))),
% 23.92/23.92 inference(scs_inference,[],[450,1232,1596,2,34])).
% 23.92/23.92 cnf(1670,plain,
% 23.92/23.92 (E(f12(f5(a3),a8),f12(a3,a8))),
% 23.92/23.92 inference(scs_inference,[],[450,1232,1374,1596,2,34,3])).
% 23.92/23.92 cnf(1672,plain,
% 23.92/23.92 (P1(a8,f12(a11,a8),f12(f4(a11,a11),a8))),
% 23.92/23.92 inference(scs_inference,[],[1539,450,1232,1468,1374,1596,2,34,3,10])).
% 23.92/23.92 cnf(1677,plain,
% 23.92/23.92 (P2(f4(a1,a6),f4(a2,a2),f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1583,1197,1539,450,686,193,144,1232,1468,50,1374,1414,1596,1451,2,34,3,10,14,12,13,11,15])).
% 23.92/23.92 cnf(1694,plain,
% 23.92/23.92 (P1(f12(a1,a2),f12(a11,a8),f12(f4(a11,a11),a8))),
% 23.92/23.92 inference(scs_inference,[],[1672,50,1640,2,10])).
% 23.92/23.92 cnf(1695,plain,
% 23.92/23.92 (P2(a11,f12(a7,a2),f12(f5(a3),f4(a11,a11)))),
% 23.92/23.92 inference(scs_inference,[],[1672,144,50,1640,1419,2,10,14])).
% 23.92/23.92 cnf(1718,plain,
% 23.92/23.92 (E(f12(f5(a3),f12(a6,a2)),f12(a3,a10))),
% 23.92/23.92 inference(scs_inference,[],[450,1263,1636,2,34])).
% 23.92/23.92 cnf(1722,plain,
% 23.92/23.92 (E(f12(f5(a3),a10),f12(a3,a10))),
% 23.92/23.92 inference(scs_inference,[],[450,1263,1314,1636,2,34,3])).
% 23.92/23.92 cnf(1724,plain,
% 23.92/23.92 (P1(a8,f12(a1,a2),f12(f4(a11,a11),a8))),
% 23.92/23.92 inference(scs_inference,[],[1422,450,1263,97,1314,1636,2,34,3,10])).
% 23.92/23.92 cnf(1728,plain,
% 23.92/23.92 (P2(a11,f12(a1,a2),a8)),
% 23.92/23.92 inference(scs_inference,[],[726,745,1422,450,1263,1232,1468,97,1314,1636,1343,1247,2,34,3,10,14,12,15])).
% 23.92/23.92 cnf(1743,plain,
% 23.92/23.92 (E(f12(f5(a3),f12(a11,a8)),f12(a3,a8))),
% 23.92/23.92 inference(scs_inference,[],[450,1444,1670,2,34])).
% 23.92/23.92 cnf(1747,plain,
% 23.92/23.92 (P1(f4(a8,a10),f5(a3),f4(f5(a3),f12(a7,a2)))),
% 23.92/23.92 inference(scs_inference,[],[726,272,450,1444,1670,2,34,10])).
% 23.92/23.92 cnf(1754,plain,
% 23.92/23.92 (P2(x17541,f12(a7,a7),f12(f12(x17541,a7),f12(a7,a11)))),
% 23.92/23.92 inference(scs_inference,[],[102,726,587,1724,272,496,450,27,193,1072,1444,97,1291,1526,1670,1695,1247,2,34,10,14,12,15,11,13,38])).
% 23.92/23.92 cnf(1767,plain,
% 23.92/23.92 (P1(f12(a11,a8),a8,f12(a1,f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[101,1404,1666,2,10])).
% 23.92/23.92 cnf(1768,plain,
% 23.92/23.92 (P2(a11,f12(a11,a8),a8)),
% 23.92/23.92 inference(scs_inference,[],[101,1404,1728,1666,2,10,14])).
% 23.92/23.92 cnf(1772,plain,
% 23.92/23.92 (P2(f12(a11,f12(a6,a2)),a11,f12(a11,a10))),
% 23.92/23.92 inference(scs_inference,[],[726,1694,101,1139,1409,1404,1500,1374,1728,1666,2,10,14,12,15,13])).
% 23.92/23.92 cnf(1774,plain,
% 23.92/23.92 (P2(a11,a3,f12(f12(a7,a2),f4(a11,a11)))),
% 23.92/23.92 inference(scs_inference,[],[726,1694,265,101,236,27,1139,1322,1409,1404,1500,1374,1728,1666,2,10,14,12,15,13,11,38])).
% 23.92/23.92 cnf(1784,plain,
% 23.92/23.92 (P1(a3,f5(a3),f12(f4(a11,a11),f5(a3)))),
% 23.92/23.92 inference(scs_inference,[],[102,470,1743,2,10])).
% 23.92/23.92 cnf(1785,plain,
% 23.92/23.92 (P2(a7,a3,f12(f4(a1,a6),a3))),
% 23.92/23.92 inference(scs_inference,[],[102,470,1743,344,2,10,14])).
% 23.92/23.92 cnf(1787,plain,
% 23.92/23.92 (E(f12(x17871,a10),f12(x17871,f12(a6,a2)))),
% 23.92/23.92 inference(rename_variables,[],[1314])).
% 23.92/23.92 cnf(1788,plain,
% 23.92/23.92 (P2(x17881,f12(a11,a10),f12(x17881,f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[102,1483,470,1378,1314,1787,1743,344,2,10,14,12,15])).
% 23.92/23.92 cnf(1790,plain,
% 23.92/23.92 (P2(f12(a1,a2),a11,f12(a11,a8))),
% 23.92/23.92 inference(scs_inference,[],[102,1483,470,1378,50,1529,1314,1787,1743,344,2,10,14,12,15,13])).
% 23.92/23.92 cnf(1795,plain,
% 23.92/23.92 (E(f12(a7,a10),f12(f12(a11,a7),f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[102,1483,1747,470,496,23,27,1378,1347,50,1529,1314,1787,1743,344,2,10,14,12,15,13,11,38,34])).
% 23.92/23.92 cnf(1812,plain,
% 23.92/23.92 (E(f12(f4(a11,a11),f5(a3)),a3)),
% 23.92/23.92 inference(scs_inference,[],[1784,24,1722,2,33])).
% 23.92/23.92 cnf(1815,plain,
% 23.92/23.92 (P1(a10,f12(a11,a10),f12(f4(a11,a11),a10))),
% 23.92/23.92 inference(scs_inference,[],[1784,1483,24,1635,1722,2,33,10])).
% 23.92/23.92 cnf(1816,plain,
% 23.92/23.92 (P2(x18161,a10,f12(x18161,f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[1784,1483,24,1635,1722,1788,2,33,10,14])).
% 23.92/23.92 cnf(1819,plain,
% 23.92/23.92 (P2(a11,f12(a6,a2),a10)),
% 23.92/23.92 inference(scs_inference,[],[1784,1355,1483,24,1263,1635,1314,1722,1788,2,33,10,14,12,15])).
% 23.92/23.92 cnf(1824,plain,
% 23.92/23.92 (P1(f5(a3),a3,f12(f4(a11,a11),f5(a3)))),
% 23.92/23.92 inference(scs_inference,[],[45,1767,1784,1355,1483,24,1263,1344,50,1754,1635,1314,1722,1788,2,33,10,14,12,15,13,11,36])).
% 23.92/23.92 cnf(1829,plain,
% 23.92/23.92 (P1(a10,a10,f12(f4(a11,a11),f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[45,1767,1784,1355,1483,24,26,496,23,27,1263,1344,50,1414,1754,1635,1314,1722,1788,2,33,10,14,12,15,13,11,36,38,40])).
% 23.92/23.92 cnf(1831,plain,
% 23.92/23.92 (P2(a11,x18311,x18311)),
% 23.92/23.92 inference(rename_variables,[],[23])).
% 23.92/23.92 cnf(1837,plain,
% 23.92/23.92 (E(x18371,a3)+~E(x18371,f12(f4(a11,a11),f5(a3)))),
% 23.92/23.92 inference(scs_inference,[],[45,1767,1784,1355,1483,24,26,496,23,1831,27,1263,1344,50,1414,1754,1635,1314,1722,1788,2,33,10,14,12,15,13,11,36,38,40,34,3])).
% 23.92/23.92 cnf(1846,plain,
% 23.92/23.92 (E(f12(f4(a11,a11),f5(a3)),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[1812,1784,192,2,33])).
% 23.92/23.92 cnf(1850,plain,
% 23.92/23.92 (P1(a3,a3,f12(f4(a11,a11),f5(a3)))),
% 23.92/23.92 inference(scs_inference,[],[102,1812,1824,1784,192,2,33,3,10])).
% 23.92/23.92 cnf(1851,plain,
% 23.92/23.92 (P2(a11,f12(a11,f12(a6,a2)),a10)),
% 23.92/23.92 inference(scs_inference,[],[102,1812,1824,1784,192,1376,1819,2,33,3,10,14])).
% 23.92/23.92 cnf(1854,plain,
% 23.92/23.92 (P2(f4(a11,a11),f12(a7,a2),a3)),
% 23.92/23.92 inference(scs_inference,[],[102,1812,1815,1824,1784,192,463,1376,1314,1819,2,33,3,10,14,12,15])).
% 23.92/23.92 cnf(1858,plain,
% 23.92/23.92 (P1(a3,f12(f4(a11,a11),f5(a3)),a3)),
% 23.92/23.92 inference(scs_inference,[],[764,102,726,1812,1815,1824,1784,192,463,1376,1635,1314,1186,1819,2,33,3,10,14,12,15,13,11,36])).
% 23.92/23.92 cnf(1880,plain,
% 23.92/23.92 (E(f12(a7,a10),f12(f4(a1,a6),f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[588,1816,1718,2,34])).
% 23.92/23.92 cnf(1881,plain,
% 23.92/23.92 (P2(x18811,a10,f12(x18811,f12(a6,a2)))),
% 23.92/23.92 inference(rename_variables,[],[1816])).
% 23.92/23.92 cnf(1882,plain,
% 23.92/23.92 (P2(f4(a1,a6),x18821,f12(a7,x18821))),
% 23.92/23.92 inference(rename_variables,[],[588])).
% 23.92/23.92 cnf(1884,plain,
% 23.92/23.92 (P1(f12(a7,a2),f12(f4(a11,a11),f5(a3)),a3)),
% 23.92/23.92 inference(scs_inference,[],[1858,588,144,1816,1718,2,34,10])).
% 23.92/23.92 cnf(1887,plain,
% 23.92/23.92 (P2(f4(a11,a11),f12(a7,a2),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[1846,1850,1858,463,588,144,1816,1718,1774,2,34,10,14,12,15])).
% 23.92/23.92 cnf(1890,plain,
% 23.92/23.92 (P2(x18901,a10,f12(x18901,f12(a6,a2)))),
% 23.92/23.92 inference(rename_variables,[],[1816])).
% 23.92/23.92 cnf(1893,plain,
% 23.92/23.92 (P2(f4(a1,a6),x18931,f12(a7,x18931))),
% 23.92/23.92 inference(rename_variables,[],[588])).
% 23.92/23.92 cnf(1896,plain,
% 23.92/23.92 (P1(f12(a7,a10),f12(a7,a10),f12(f4(a7,a7),f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[127,45,726,1846,1850,1858,467,21,463,588,1882,1893,144,1382,1816,1881,1890,1718,1774,2,34,10,14,12,15,13,11,38,40])).
% 23.92/23.92 cnf(1897,plain,
% 23.92/23.92 (P2(x18971,a10,f12(x18971,f12(a6,a2)))),
% 23.92/23.92 inference(rename_variables,[],[1816])).
% 23.92/23.92 cnf(1898,plain,
% 23.92/23.92 (P2(f4(a1,a6),x18981,f12(a7,x18981))),
% 23.92/23.92 inference(rename_variables,[],[588])).
% 23.92/23.92 cnf(1899,plain,
% 23.92/23.92 (P2(f4(a1,a6),x18991,f12(a7,x18991))),
% 23.92/23.92 inference(rename_variables,[],[588])).
% 23.92/23.92 cnf(1904,plain,
% 23.92/23.92 (P2(f4(a1,a6),a7,f4(f12(a7,a1),f12(a7,a6)))),
% 23.92/23.92 inference(scs_inference,[],[16,18,127,45,726,1846,1850,1858,467,21,463,26,588,1882,1893,1899,1898,144,1382,1816,1881,1890,1897,1718,1774,2,34,10,14,12,15,13,11,38,40,37,42])).
% 23.92/23.92 cnf(1918,plain,
% 23.92/23.92 (E(f4(f12(a7,a1),f12(a7,a6)),f12(a7,a7))),
% 23.92/23.92 inference(scs_inference,[],[1904,588,1880,2,34])).
% 23.92/23.92 cnf(1919,plain,
% 23.92/23.92 (P2(f4(a1,a6),x19191,f12(a7,x19191))),
% 23.92/23.92 inference(rename_variables,[],[588])).
% 23.92/23.92 cnf(1921,plain,
% 23.92/23.92 (E(f12(f4(a1,a6),a10),f12(a7,a10))),
% 23.92/23.92 inference(scs_inference,[],[1904,588,1314,1880,2,34,3])).
% 23.92/23.92 cnf(1923,plain,
% 23.92/23.92 (P1(f4(a8,a10),f12(f4(a11,a11),f5(a3)),a3)),
% 23.92/23.92 inference(scs_inference,[],[726,1884,1904,588,1314,1880,2,34,3,10])).
% 23.92/23.92 cnf(1926,plain,
% 23.92/23.92 (P2(f4(a11,a11),a3,a3)),
% 23.92/23.92 inference(scs_inference,[],[45,726,1858,1812,1884,1904,454,588,144,1314,1880,2,34,3,10,14,12,15])).
% 23.92/23.92 cnf(1931,plain,
% 23.92/23.92 (P2(f4(f12(a7,a1),f12(a7,a6)),a2,f12(a7,a3))),
% 23.92/23.92 inference(scs_inference,[],[19,45,726,1858,1812,1884,1904,509,454,588,1919,144,1314,1788,1880,2,34,3,10,14,12,15,13,11,37])).
% 23.92/23.92 cnf(1948,plain,
% 23.92/23.92 (E(f12(f5(a3),f12(a11,a10)),f12(a3,a10))),
% 23.92/23.92 inference(scs_inference,[],[450,1378,1918,2,34])).
% 23.92/23.92 cnf(1952,plain,
% 23.92/23.92 (P1(a3,f5(a3),f12(a7,f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[102,699,450,1378,1918,2,34,10])).
% 23.92/23.92 cnf(1953,plain,
% 23.92/23.92 (P2(f4(a11,a11),f4(a8,a10),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[102,726,699,450,1378,1918,1887,2,34,10,14])).
% 23.92/23.92 cnf(1955,plain,
% 23.92/23.92 (P2(f4(a11,a11),f4(a8,a10),a3)),
% 23.92/23.92 inference(scs_inference,[],[102,726,1884,1812,699,761,450,1378,144,1918,1887,2,34,10,14,12,15])).
% 23.92/23.92 cnf(1959,plain,
% 23.92/23.92 (P2(x19591,f12(a7,a8),f12(f12(x19591,a7),f12(a11,a8)))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1884,1812,1483,699,761,496,450,27,1378,144,1526,1635,1918,364,1887,2,34,10,14,12,15,13,11,38])).
% 23.92/23.92 cnf(1972,plain,
% 23.92/23.92 (P1(f12(a7,a2),f5(a3),f12(a7,f4(a2,a2)))),
% 23.92/23.92 inference(scs_inference,[],[1952,144,1921,2,10])).
% 23.92/23.92 cnf(1976,plain,
% 23.92/23.92 (P2(a3,f4(a11,a11),f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[1923,1952,144,961,1281,1851,1921,2,10,14,12,15])).
% 23.92/23.92 cnf(1977,plain,
% 23.92/23.92 (P2(f12(a7,a7),a2,f12(a7,a3))),
% 23.92/23.92 inference(scs_inference,[],[1923,1952,144,961,1281,1931,1851,1921,1918,2,10,14,12,15,13])).
% 23.92/23.92 cnf(1997,plain,
% 23.92/23.92 (E(f12(a7,a8),f12(f12(a11,a7),f12(a11,a8)))),
% 23.92/23.92 inference(scs_inference,[],[23,1948,1959,2,34])).
% 23.92/23.92 cnf(2008,plain,
% 23.92/23.92 (P2(a6,f12(a2,f12(a6,a2)),f12(a10,a10))),
% 23.92/23.92 inference(scs_inference,[],[18,102,726,488,1952,1846,1972,491,454,23,27,756,1816,1953,1948,696,1959,2,34,10,14,12,15,13,11,38])).
% 23.92/23.92 cnf(2021,plain,
% 23.92/23.92 (P2(a11,f12(a11,f12(a1,a2)),a8)),
% 23.92/23.92 inference(scs_inference,[],[726,1896,509,1468,1498,756,1281,1955,1997,2,10,14,12,15])).
% 23.92/23.92 cnf(2023,plain,
% 23.92/23.92 (P2(f12(a7,a2),f4(a11,a11),f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[726,1896,509,1468,144,1498,756,1281,1976,1955,1997,2,10,14,12,15,13])).
% 23.92/23.92 cnf(2069,plain,
% 23.92/23.92 (P2(f12(a6,a2),a11,f12(a11,a10))),
% 23.92/23.92 inference(scs_inference,[],[726,488,1972,1829,1259,1500,1281,295,1314,1795,2008,2,3,10,14,12,15,13])).
% 23.92/23.92 cnf(2137,plain,
% 23.92/23.92 (P2(f4(a1,a6),f4(a2,a2),f4(a8,a10))),
% 23.92/23.92 inference(scs_inference,[],[726,1121,789,144,1677,2023,1247,623,1226,2,10,14,13,12,15])).
% 23.92/23.92 cnf(2154,plain,
% 23.92/23.92 (P1(f12(a7,a2),x21541,x21541)),
% 23.92/23.92 inference(scs_inference,[],[22,144,10])).
% 23.92/23.92 cnf(2157,plain,
% 23.92/23.92 (E(f12(x21571,a7),f12(x21571,f12(a7,a11)))),
% 23.92/23.92 inference(rename_variables,[],[1247])).
% 23.92/23.92 cnf(2162,plain,
% 23.92/23.92 (P2(x21621,f12(a7,a8),f12(f12(x21621,a7),a8))),
% 23.92/23.92 inference(scs_inference,[],[540,1829,22,496,1232,193,144,1414,1614,295,1977,1247,2157,1785,10,14,12,13,15,11,38])).
% 23.92/23.92 cnf(2178,plain,
% 23.92/23.92 (P1(f4(a8,a10),x21781,x21781)),
% 23.92/23.92 inference(scs_inference,[],[726,2154,10])).
% 23.92/23.92 cnf(2202,plain,
% 23.92/23.92 (P1(f12(f4(a7,a7),a2),x22021,x22021)),
% 23.92/23.92 inference(scs_inference,[],[2178,756,10])).
% 23.92/23.92 cnf(2203,plain,
% 23.92/23.92 (P2(a11,f12(a7,a2),f4(a6,f5(a6)))),
% 23.92/23.92 inference(scs_inference,[],[2178,144,756,422,10,14])).
% 23.92/23.92 cnf(2208,plain,
% 23.92/23.92 (P2(a3,f4(a11,a11),f4(a8,a10))),
% 23.92/23.92 inference(scs_inference,[],[45,726,2178,144,756,1976,2162,422,10,14,12,13,15])).
% 23.92/23.92 cnf(2225,plain,
% 23.92/23.92 (P1(a3,f5(f5(a3)),a3)),
% 23.92/23.92 inference(scs_inference,[],[102,24,10])).
% 23.92/23.92 cnf(2232,plain,
% 23.92/23.92 (P2(a11,f12(a11,a8),f12(a1,a2))),
% 23.92/23.92 inference(scs_inference,[],[102,726,1422,24,1378,50,1374,1768,2203,10,14,12,13,15])).
% 23.92/23.92 cnf(2249,plain,
% 23.92/23.92 (P2(x22491,x22492,f12(x22491,x22492))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(2251,plain,
% 23.92/23.92 (P1(f12(a7,a2),f5(f5(a3)),a3)),
% 23.92/23.92 inference(scs_inference,[],[2225,27,1444,144,34,10])).
% 23.92/23.92 cnf(2254,plain,
% 23.92/23.92 (P1(f12(f4(a7,a7),a2),x22541,x22541)),
% 23.92/23.92 inference(rename_variables,[],[2202])).
% 23.92/23.92 cnf(2260,plain,
% 23.92/23.92 (P1(x22601,x22602,f4(x22601,x22602))),
% 23.92/23.92 inference(rename_variables,[],[26])).
% 23.92/23.92 cnf(2262,plain,
% 23.92/23.92 (P2(x22621,f12(a6,a2),f12(x22621,f12(a11,a10)))),
% 23.92/23.92 inference(scs_inference,[],[872,45,2202,2254,2225,26,21,27,2249,1444,1468,144,1382,1635,295,1772,1413,2232,34,10,14,12,13,15,11,36,38])).
% 23.92/23.92 cnf(2263,plain,
% 23.92/23.92 (P2(x22631,x22632,f12(x22631,x22632))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(2266,plain,
% 23.92/23.92 (P1(f12(a3,a10),f12(a3,a10),f12(f12(a7,a2),f12(a6,a2)))),
% 23.92/23.92 inference(scs_inference,[],[1170,872,45,2202,2254,2225,26,21,27,2249,2263,1444,1468,1816,144,1382,1635,295,1772,1413,2232,34,10,14,12,13,15,11,36,38,40])).
% 23.92/23.92 cnf(2268,plain,
% 23.92/23.92 (P2(x22681,x22682,f12(x22681,x22682))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(2269,plain,
% 23.92/23.92 (P2(x22691,x22692,f12(x22691,x22692))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(2272,plain,
% 23.92/23.92 (E(f12(a1,a2),f12(a11,f12(a11,a8)))),
% 23.92/23.92 inference(scs_inference,[],[1170,872,45,2202,2254,2225,26,21,27,2249,2263,1444,1468,1816,144,1382,1404,1635,295,1772,1413,2232,34,10,14,12,13,15,11,36,38,40,2,3])).
% 23.92/23.92 cnf(2275,plain,
% 23.92/23.92 (P2(x22751,a7,f4(f12(x22751,a1),f12(x22751,a6)))),
% 23.92/23.92 inference(scs_inference,[],[16,18,1170,872,45,2202,2254,2225,26,2260,21,27,2249,2263,2269,2268,1444,1468,1816,144,1382,1404,1635,295,1772,1413,2232,34,10,14,12,13,15,11,36,38,40,2,3,37,42])).
% 23.92/23.92 cnf(2289,plain,
% 23.92/23.92 (E(f4(f12(a11,a1),f12(a11,a6)),a7)),
% 23.92/23.92 inference(scs_inference,[],[2275,23,2272,2,34])).
% 23.92/23.92 cnf(2290,plain,
% 23.92/23.92 (P2(a11,x22901,x22901)),
% 23.92/23.92 inference(rename_variables,[],[23])).
% 23.92/23.92 cnf(2291,plain,
% 23.92/23.92 (P2(x22911,a7,f4(f12(x22911,a1),f12(x22911,a6)))),
% 23.92/23.92 inference(rename_variables,[],[2275])).
% 23.92/23.92 cnf(2293,plain,
% 23.92/23.92 (P1(f4(a8,a10),f5(f5(a3)),a3)),
% 23.92/23.92 inference(scs_inference,[],[726,2275,2251,23,2272,2,34,10])).
% 23.92/23.92 cnf(2294,plain,
% 23.92/23.92 (P2(x22941,f4(a1,a6),f4(f12(x22941,a1),f12(x22941,a6)))),
% 23.92/23.92 inference(scs_inference,[],[45,726,2275,2291,2251,23,2272,2,34,10,14])).
% 23.92/23.92 cnf(2300,plain,
% 23.92/23.92 (P2(f4(f12(a11,a1),f12(a11,a6)),a2,a3)),
% 23.92/23.92 inference(scs_inference,[],[19,102,45,726,2225,2275,2291,2251,123,23,2290,1468,1816,144,1341,1790,2272,2,34,10,14,12,13,15,11,37])).
% 23.92/23.92 cnf(2302,plain,
% 23.92/23.92 (P2(x23021,a7,f4(f12(x23021,a1),f12(x23021,a6)))),
% 23.92/23.92 inference(rename_variables,[],[2275])).
% 23.92/23.92 cnf(2304,plain,
% 23.92/23.92 (P2(a6,f4(f12(a2,a1),f12(a2,a6)),f12(a10,a7))),
% 23.92/23.92 inference(scs_inference,[],[18,19,102,45,726,2225,2275,2291,2302,2251,123,27,23,2290,1468,1816,144,1341,1790,2272,2,34,10,14,12,13,15,11,37,38])).
% 23.92/23.92 cnf(2322,plain,
% 23.92/23.92 (E(f12(x23221,f12(a11,a10)),f12(x23221,a10))),
% 23.92/23.92 inference(scs_inference,[],[27,1378,2289,2,34])).
% 23.92/23.92 cnf(2326,plain,
% 23.92/23.92 (P1(a3,f5(f5(a3)),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[102,192,27,1378,2289,2,34,10])).
% 23.92/23.92 cnf(2332,plain,
% 23.92/23.92 (P2(f12(a7,a2),f4(a11,a11),f4(a8,a10))),
% 23.92/23.92 inference(scs_inference,[],[102,726,2251,192,27,1378,144,1788,295,2023,2289,1386,2,34,10,14,12,13,15])).
% 23.92/23.92 cnf(2353,plain,
% 23.92/23.92 (E(f12(x23531,a7),f4(f12(x23531,a1),f12(x23531,a6)))),
% 23.92/23.92 inference(scs_inference,[],[496,2294,2322,2,34])).
% 23.92/23.92 cnf(2356,plain,
% 23.92/23.92 (E(f12(a6,a2),f12(a11,f12(a11,a10)))),
% 23.92/23.92 inference(scs_inference,[],[496,1337,2294,2322,2,34,3])).
% 23.92/23.92 cnf(2357,plain,
% 23.92/23.92 (P1(f12(a7,a2),f5(f5(a3)),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[2326,496,144,1337,2294,2322,2,34,3,10])).
% 23.92/23.92 cnf(2360,plain,
% 23.92/23.92 (P2(f4(a8,a10),f4(a11,a11),f4(a8,a10))),
% 23.92/23.92 inference(scs_inference,[],[726,2293,2326,496,144,1337,2332,2294,2322,707,2,34,3,10,14,12,13])).
% 23.92/23.92 cnf(2361,plain,
% 23.92/23.92 (P2(f4(a11,a11),f12(a7,a2),f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[726,2293,2326,496,144,1337,1854,2332,2294,2322,707,2,34,3,10,14,12,13,15])).
% 23.92/23.92 cnf(2381,plain,
% 23.92/23.92 (E(a10,f12(a11,f12(a11,a10)))),
% 23.92/23.92 inference(scs_inference,[],[295,2356,2,3])).
% 23.92/23.92 cnf(2383,plain,
% 23.92/23.92 (P2(f4(a11,a11),f4(a8,a10),f12(a7,a2))),
% 23.92/23.92 inference(scs_inference,[],[726,2357,295,2361,2356,2,3,10,14])).
% 23.92/23.92 cnf(2391,plain,
% 23.92/23.92 (P1(f4(a1,a6),a7,f4(f4(a7,a7),a3))),
% 23.92/23.92 inference(scs_inference,[],[16,48,127,726,2266,2357,20,26,144,756,1281,295,1926,2360,2361,2356,2,3,10,14,12,13,15,11,35,36])).
% 23.92/23.92 cnf(2394,plain,
% 23.92/23.92 (P2(x23941,a10,x23942)+~P2(f12(x23941,a6),a2,x23942)),
% 23.92/23.92 inference(scs_inference,[],[16,18,48,127,726,2266,2357,20,26,27,144,756,1281,295,1926,2360,2361,2356,2,3,10,14,12,13,15,11,35,36,38])).
% 23.92/23.92 cnf(2400,plain,
% 23.92/23.92 (P2(x24001,a10,f12(f12(x24001,a6),a2))),
% 23.92/23.92 inference(scs_inference,[],[27,2394])).
% 23.92/23.92 cnf(2401,plain,
% 23.92/23.92 (P2(x24011,x24012,f12(x24011,x24012))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(2403,plain,
% 23.92/23.92 (E(f4(f12(x24031,a1),f12(x24031,a6)),f12(x24031,a7))),
% 23.92/23.92 inference(scs_inference,[],[27,2353,2394,2])).
% 23.92/23.92 cnf(2404,plain,
% 23.92/23.92 (E(f5(f4(a8,a10)),a3)),
% 23.92/23.92 inference(scs_inference,[],[2178,24,27,2353,2394,2,33])).
% 23.92/23.92 cnf(2405,plain,
% 23.92/23.92 (P1(x24051,f5(x24051),a3)),
% 23.92/23.92 inference(rename_variables,[],[24])).
% 23.92/23.92 cnf(2408,plain,
% 23.92/23.92 (E(f12(x24081,a10),f12(f12(x24081,a6),a2))),
% 23.92/23.92 inference(scs_inference,[],[2178,24,27,2401,2353,2394,2,33,34])).
% 23.92/23.92 cnf(2409,plain,
% 23.92/23.92 (P2(x24091,x24092,f12(x24091,x24092))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(2411,plain,
% 23.92/23.92 (E(f12(a6,a2),f12(f12(a11,a6),a2))),
% 23.92/23.92 inference(scs_inference,[],[2178,24,27,2401,1337,2353,2394,2,33,34,3])).
% 23.92/23.92 cnf(2412,plain,
% 23.92/23.92 (P1(f4(a1,a6),f5(a7),a3)),
% 23.92/23.92 inference(scs_inference,[],[45,2178,24,2405,27,2401,1337,2353,2394,2,33,34,3,10])).
% 23.92/23.92 cnf(2414,plain,
% 23.92/23.92 (P2(a6,f12(a2,a7),f12(a10,a7))),
% 23.92/23.92 inference(scs_inference,[],[45,2178,24,2405,27,2401,1337,2304,2353,2394,2,33,34,3,10,14])).
% 23.92/23.92 cnf(2420,plain,
% 23.92/23.92 (P1(a7,a3,f4(f4(a7,a7),f5(a7)))),
% 23.92/23.92 inference(scs_inference,[],[187,45,2178,2391,1539,24,2405,26,27,2401,50,1337,1374,2021,2304,1473,2353,2394,2,33,34,3,10,14,12,13,11,15,36])).
% 23.92/23.92 cnf(2423,plain,
% 23.92/23.92 (P2(x24231,f12(a11,a8),f12(x24231,f12(a1,a2)))),
% 23.92/23.92 inference(scs_inference,[],[187,45,2178,2391,1539,24,2405,26,21,27,2401,2409,50,1337,1374,1790,2021,2304,1473,2353,2394,2,33,34,3,10,14,12,13,11,15,36,38])).
% 23.92/23.92 cnf(2440,plain,
% 23.92/23.92 (E(a3,f5(f4(a8,a10)))),
% 23.92/23.92 inference(scs_inference,[],[2404,2])).
% 23.92/23.92 cnf(2441,plain,
% 23.92/23.92 (E(f5(f12(a7,a2)),a3)),
% 23.92/23.92 inference(scs_inference,[],[2154,2404,24,2,33])).
% 23.92/23.92 cnf(2446,plain,
% 23.92/23.92 (P1(f4(f12(a11,a1),a6),f5(a7),a3)),
% 23.92/23.92 inference(scs_inference,[],[2154,2412,2404,24,193,295,2411,2,33,3,10])).
% 23.92/23.92 cnf(2453,plain,
% 23.92/23.92 (P1(f4(a1,a6),a3,f4(f4(a7,a7),f5(a7)))),
% 23.92/23.92 inference(scs_inference,[],[764,1349,2154,2412,2404,2420,24,193,144,756,1635,295,2069,2300,2383,2411,2403,2,33,3,10,14,12,13,15,11,36])).
% 23.92/23.92 cnf(2469,plain,
% 23.92/23.92 (E(a3,f5(f12(a7,a2)))),
% 23.92/23.92 inference(scs_inference,[],[2441,2])).
% 23.92/23.92 cnf(2475,plain,
% 23.92/23.92 (P1(a3,x24751,f4(f5(a3),x24751))),
% 23.92/23.92 inference(scs_inference,[],[102,2178,2441,192,26,2440,2,33,3,10])).
% 23.92/23.92 cnf(2477,plain,
% 23.92/23.92 (P2(x24771,a8,f12(x24771,f12(a1,a2)))),
% 23.92/23.92 inference(scs_inference,[],[102,2178,2441,192,26,1468,2423,2440,2,33,3,10,14])).
% 23.92/23.92 cnf(2481,plain,
% 23.92/23.92 (P2(f5(a3),f12(a6,a2),f12(a3,a10))),
% 23.92/23.92 inference(scs_inference,[],[102,2178,2446,2441,192,26,1468,144,1948,2262,2423,2440,2,33,3,10,14,12,13,15])).
% 23.92/23.92 cnf(2491,plain,
% 23.92/23.92 (P1(f12(a3,a10),f12(a3,a10),f12(a3,a10))),
% 23.92/23.92 inference(scs_inference,[],[18,209,127,102,2178,2453,2446,2441,20,192,26,27,1468,144,1948,2262,2423,2440,2400,2,33,3,10,14,12,13,15,11,36,38,40])).
% 23.92/23.92 cnf(2504,plain,
% 23.92/23.92 (E(f12(a7,a2),f4(f5(a3),f4(a8,a10)))),
% 23.92/23.92 inference(scs_inference,[],[706,2475,2381,2,33])).
% 23.92/23.92 cnf(2505,plain,
% 23.92/23.92 (P1(a3,x25051,f4(f5(a3),x25051))),
% 23.92/23.92 inference(rename_variables,[],[2475])).
% 23.92/23.92 cnf(2509,plain,
% 23.92/23.92 (E(f12(x25091,a10),f12(x25091,f12(a6,a2)))),
% 23.92/23.92 inference(rename_variables,[],[1314])).
% 23.92/23.92 cnf(2513,plain,
% 23.92/23.92 (E(f12(x25131,a10),f12(x25131,f12(a6,a2)))),
% 23.92/23.92 inference(rename_variables,[],[1314])).
% 23.92/23.92 cnf(2522,plain,
% 23.92/23.92 (P2(x25221,a8,f12(x25221,f12(a1,a2)))),
% 23.92/23.92 inference(rename_variables,[],[2477])).
% 23.92/23.92 cnf(2523,plain,
% 23.92/23.92 (P2(x25231,x25232,f12(x25231,x25232))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(2525,plain,
% 23.92/23.92 (P1(f12(a3,a8),f12(a3,a8),f12(f12(a7,a2),f12(a1,a2)))),
% 23.92/23.92 inference(scs_inference,[],[18,62,48,706,1170,102,2491,2475,2505,27,2523,144,756,1314,2509,2513,1247,2137,330,2414,2381,2477,2522,2469,2,33,3,10,14,12,13,15,11,36,38,40])).
% 23.92/23.92 cnf(2539,plain,
% 23.92/23.92 (E(a3,f4(f5(a3),f4(a8,a10)))),
% 23.92/23.92 inference(scs_inference,[],[969,2504,2475,2,33])).
% 23.92/23.92 cnf(2540,plain,
% 23.92/23.92 (P1(a3,x25401,f4(f5(a3),x25401))),
% 23.92/23.92 inference(rename_variables,[],[2475])).
% 23.92/23.92 cnf(2543,plain,
% 23.92/23.92 (P1(f12(a7,a2),x25431,f4(f5(a3),x25431))),
% 23.92/23.92 inference(scs_inference,[],[969,102,2504,2475,2540,144,2,33,3,10])).
% 23.92/23.92 cnf(2556,plain,
% 23.92/23.92 (P2(x25561,a8,x25562)+~P2(f12(x25561,a1),a2,x25562)),
% 23.92/23.92 inference(scs_inference,[],[18,17,969,187,45,102,2525,2504,2475,2540,2453,20,27,144,756,1341,1248,2208,2400,1653,2,33,3,10,14,12,13,15,11,36,37,38])).
% 23.92/23.92 cnf(2565,plain,
% 23.92/23.92 (P2(x25651,a8,f12(f12(x25651,a1),a2))),
% 23.92/23.92 inference(scs_inference,[],[27,2556])).
% 23.92/23.92 cnf(2566,plain,
% 23.92/23.92 (P2(x25661,x25662,f12(x25661,x25662))),
% 23.92/23.92 inference(rename_variables,[],[27])).
% 23.92/23.92 cnf(2573,plain,
% 23.92/23.92 (E(f12(x25731,a8),f12(f12(x25731,a1),a2))),
% 23.92/23.92 inference(scs_inference,[],[2154,2539,192,27,2566,2556,2,33,34])).
% 23.92/23.92 cnf(2583,plain,
% 23.92/23.92 (P1(f5(a3),a3,f4(f5(a3),f12(a7,a2)))),
% 23.92/23.92 inference(scs_inference,[],[19,48,329,706,2154,2412,2539,22,20,192,188,426,27,2566,1404,2556,2,33,34,3,10,14,12,13,15,11,35])).
% 23.92/23.92 cnf(2686,plain,
% 23.92/23.92 (P1(f4(a8,a10),x26861,f4(f5(a3),x26861))),
% 23.92/23.92 inference(scs_inference,[],[726,2543,2408,2,10])).
% 23.92/23.92 cnf(2692,plain,
% 23.92/23.92 (E(f4(f5(a3),f4(a8,a10)),f4(a8,a10))),
% 23.92/23.92 inference(scs_inference,[],[2178,726,2543,2539,20,24,402,1976,1926,2408,2,10,14,12,13,15,11,33])).
% 23.92/23.92 cnf(2697,plain,
% 23.92/23.92 (P1(a1,f5(a3),f4(a1,a3))),
% 23.92/23.92 inference(scs_inference,[],[16,201,429,2178,726,2543,2539,20,24,26,402,1976,1926,2408,2,10,14,12,13,15,11,33,35,36])).
% 23.92/23.92 cnf(2700,plain,
% 23.92/23.92 (P2(x27001,f12(a6,a2),x27002)+~P2(f12(x27001,a6),f12(a2,a11),x27002)),
% 23.92/23.92 inference(scs_inference,[],[16,201,429,2178,726,2543,2539,20,24,26,27,1161,402,1976,1926,2408,2,10,14,12,13,15,11,33,35,36,38])).
% 23.92/23.92 cnf(2712,plain,
% 23.92/23.92 (P2(x27121,f12(a6,a2),f12(f12(x27121,a6),f12(a2,a11)))),
% 23.92/23.92 inference(scs_inference,[],[27,2700])).
% 23.92/23.92 cnf(2728,plain,
% 23.92/23.92 (~E(f4(a10,a8),f5(a3))),
% 23.92/23.92 inference(scs_inference,[],[43,867,45,102,2539,2692,2686,2697,2583,26,27,457,50,2565,2208,2700,2,10,14,12,13,15,11,35,404,1837,3])).
% 23.92/23.92 cnf(2752,plain,
% 23.92/23.92 ($false),
% 23.92/23.92 inference(scs_inference,[],[28,445,2539,22,26,1263,1049,1376,2481,2573,2712,2728,2,34,3,10,14,12]),
% 23.92/23.92 ['proof']).
% 23.92/23.92 % SZS output end Proof
% 23.92/23.92 % Total time :23.190000s
%------------------------------------------------------------------------------