%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG041-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 : n006.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 21.67s 21.79s
% Output : CNFRefutation 21.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : RNG041-1 : TPTP v8.2.0. Released v1.0.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n006.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Jun 18 13:11:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.52/0.60 start to proof:theBenchmark
% 21.67/21.79 %-------------------------------------------
% 21.67/21.79 % File :CSE---1.7
% 21.67/21.79 % Problem :theBenchmark
% 21.67/21.79 % Transform :cnf
% 21.67/21.79 % Format :tptp:raw
% 21.67/21.79 % Command :java -jar mcs_scs.jar %d %s
% 21.67/21.79
% 21.67/21.79 % Result :Theorem 21.090000s
% 21.67/21.79 % Output :CNFRefutation 21.090000s
% 21.67/21.79 %-------------------------------------------
% 21.67/21.79 %--------------------------------------------------------------------------
% 21.67/21.79 % File : RNG041-1 : TPTP v8.2.0. Released v1.0.0.
% 21.67/21.79 % Domain : Ring Theory
% 21.67/21.79 % Problem : Unknown
% 21.67/21.79 % Version : [Wos65] axioms.
% 21.67/21.79 % English :
% 21.67/21.79
% 21.67/21.79 % Refs : [Wos65] Wos (1965), Unpublished Note
% 21.67/21.79 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 21.67/21.79 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 21.67/21.79 % Source : [SPRFN]
% 21.67/21.79 % Names : Problem 30 [Wos65]
% 21.67/21.79 % : wos30 [WM76]
% 21.67/21.79
% 21.67/21.79 % Status : Unsatisfiable
% 21.67/21.79 % Rating : 0.05 v8.1.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.09 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.10 v5.5.0, 0.30 v5.3.0, 0.28 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.10 v3.5.0, 0.09 v3.4.0, 0.08 v3.3.0, 0.14 v3.2.0, 0.15 v3.1.0, 0.09 v2.7.0, 0.17 v2.6.0, 0.10 v2.5.0, 0.08 v2.4.0, 0.22 v2.2.1, 0.11 v2.2.0, 0.11 v2.1.0, 0.22 v2.0.0
% 21.67/21.79 % Syntax : Number of clauses : 26 ( 13 unt; 2 nHn; 14 RR)
% 21.67/21.79 % Number of literals : 61 ( 6 equ; 35 neg)
% 21.67/21.79 % Maximal clause size : 5 ( 2 avg)
% 21.67/21.79 % Maximal term depth : 2 ( 1 avg)
% 21.67/21.79 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 21.67/21.79 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 21.67/21.79 % Number of variables : 77 ( 2 sgn)
% 21.67/21.79 % SPC : CNF_UNS_RFO_SEQ_NHN
% 21.67/21.79
% 21.67/21.79 % Comments : These are the same axioms as in [MOW76].
% 21.67/21.79 %--------------------------------------------------------------------------
% 21.67/21.79 %----Include ring theory axioms
% 21.67/21.79 include('Axioms/RNG001-0.ax').
% 21.67/21.79 %--------------------------------------------------------------------------
% 21.67/21.79 cnf(multiplicative_identity1,hypothesis,
% 21.67/21.79 product(additive_identity,A,additive_identity) ).
% 21.67/21.79
% 21.67/21.79 cnf(multiplicative_identity2,hypothesis,
% 21.67/21.79 product(A,additive_identity,additive_identity) ).
% 21.67/21.79
% 21.67/21.79 cnf(right_multiplicative_identity,hypothesis,
% 21.67/21.79 product(A,multiplicative_identity,A) ).
% 21.67/21.79
% 21.67/21.79 cnf(left_multiplicative_identity,hypothesis,
% 21.67/21.79 product(multiplicative_identity,A,A) ).
% 21.67/21.79
% 21.67/21.79 cnf(clause41,hypothesis,
% 21.67/21.79 ( product(A,h(A),multiplicative_identity)
% 21.67/21.79 | A = additive_identity ) ).
% 21.67/21.79
% 21.67/21.79 cnf(clause42,hypothesis,
% 21.67/21.79 ( product(h(A),A,multiplicative_identity)
% 21.67/21.79 | A = additive_identity ) ).
% 21.67/21.79
% 21.67/21.79 cnf(a_times_b,negated_conjecture,
% 21.67/21.79 product(a,b,additive_identity) ).
% 21.67/21.79
% 21.67/21.79 cnf(a_not_additive_identity,negated_conjecture,
% 21.67/21.79 a != additive_identity ).
% 21.67/21.79
% 21.67/21.79 cnf(prove_b_is_additive_identity,negated_conjecture,
% 21.67/21.79 b != additive_identity ).
% 21.67/21.79
% 21.67/21.79 %--------------------------------------------------------------------------
% 21.67/21.79 %-------------------------------------------
% 21.67/21.79 % Proof found
% 21.67/21.79 % SZS status Theorem for theBenchmark
% 21.67/21.79 % SZS output start Proof
% 21.67/21.80 %ClaNum:41(EqnAxiom:15)
% 21.67/21.80 %VarNum:158(SingletonVarNum:77)
% 21.67/21.80 %MaxLitNum:5
% 21.67/21.80 %MaxfuncDepth:1
% 21.67/21.80 %SharedTerms:7
% 21.67/21.80 %goalClause: 16 27 28
% 21.67/21.80 %singleGoalClaCount:3
% 21.67/21.80 [16]P1(a1,a2,a3)
% 21.67/21.80 [27]~E(a1,a3)
% 21.67/21.80 [28]~E(a2,a3)
% 21.67/21.80 [17]P1(x171,a3,a3)
% 21.67/21.80 [18]P1(a3,x181,a3)
% 21.67/21.80 [19]P2(x191,a3,x191)
% 21.67/21.80 [20]P1(x201,a6,x201)
% 21.67/21.80 [21]P2(a3,x211,x211)
% 21.67/21.80 [22]P1(a6,x221,x221)
% 21.67/21.80 [23]P2(x231,f5(x231),a3)
% 21.67/21.80 [24]P2(f5(x241),x241,a3)
% 21.67/21.80 [25]P2(x251,x252,f4(x251,x252))
% 21.67/21.80 [26]P1(x261,x262,f8(x261,x262))
% 21.67/21.80 [29]E(x291,a3)+P1(x291,f7(x291),a6)
% 21.67/21.80 [30]E(x301,a3)+P1(f7(x301),x301,a6)
% 21.67/21.80 [31]~P2(x312,x311,x313)+P2(x311,x312,x313)
% 21.67/21.80 [32]~P2(x323,x324,x321)+E(x321,x322)+~P2(x323,x324,x322)
% 21.67/21.80 [33]~P1(x333,x334,x331)+E(x331,x332)+~P1(x333,x334,x332)
% 21.67/21.80 [34]~P2(x346,x344,x341)+P2(x341,x342,x343)+~P2(x344,x342,x345)+~P2(x346,x345,x343)
% 21.67/21.80 [35]~P2(x351,x356,x354)+P2(x351,x352,x353)+~P2(x354,x355,x353)+~P2(x356,x355,x352)
% 21.67/21.80 [36]~P1(x366,x364,x361)+P1(x361,x362,x363)+~P1(x364,x362,x365)+~P1(x366,x365,x363)
% 21.67/21.80 [37]~P1(x371,x376,x374)+P1(x371,x372,x373)+~P1(x374,x375,x373)+~P1(x376,x375,x372)
% 21.67/21.80 [38]~P1(x387,x385,x382)+~P1(x387,x384,x381)+P2(x381,x382,x383)+~P2(x384,x385,x386)+~P1(x387,x386,x383)
% 21.67/21.80 [39]~P1(x395,x397,x392)+~P1(x394,x397,x391)+P2(x391,x392,x393)+~P2(x394,x395,x396)+~P1(x396,x397,x393)
% 21.67/21.80 [40]~P1(x407,x402,x405)+~P1(x406,x402,x404)+P1(x401,x402,x403)+~P2(x404,x405,x403)+~P2(x406,x407,x401)
% 21.67/21.80 [41]~P1(x411,x417,x415)+~P1(x411,x416,x414)+P1(x411,x412,x413)+~P2(x414,x415,x413)+~P2(x416,x417,x412)
% 21.67/21.80 %EqnAxiom
% 21.67/21.80 [1]E(x11,x11)
% 21.67/21.80 [2]E(x22,x21)+~E(x21,x22)
% 21.67/21.80 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 21.67/21.80 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 21.67/21.80 [5]~E(x51,x52)+E(f7(x51),f7(x52))
% 21.67/21.80 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 21.67/21.80 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 21.67/21.80 [8]~E(x81,x82)+E(f8(x81,x83),f8(x82,x83))
% 21.67/21.80 [9]~E(x91,x92)+E(f8(x93,x91),f8(x93,x92))
% 21.67/21.80 [10]P1(x102,x103,x104)+~E(x101,x102)+~P1(x101,x103,x104)
% 21.67/21.80 [11]P1(x113,x112,x114)+~E(x111,x112)+~P1(x113,x111,x114)
% 21.67/21.80 [12]P1(x123,x124,x122)+~E(x121,x122)+~P1(x123,x124,x121)
% 21.67/21.80 [13]P2(x132,x133,x134)+~E(x131,x132)+~P2(x131,x133,x134)
% 21.67/21.80 [14]P2(x143,x142,x144)+~E(x141,x142)+~P2(x143,x141,x144)
% 21.67/21.80 [15]P2(x153,x154,x152)+~E(x151,x152)+~P2(x153,x154,x151)
% 21.67/21.80
% 21.67/21.80 %-------------------------------------------
% 21.67/21.81 cnf(42,plain,
% 21.67/21.81 (E(a3,f8(a1,a2))),
% 21.67/21.81 inference(scs_inference,[],[16,26,33])).
% 21.67/21.81 cnf(43,plain,
% 21.67/21.81 (P1(x431,x432,f8(x431,x432))),
% 21.67/21.81 inference(rename_variables,[],[26])).
% 21.67/21.81 cnf(45,plain,
% 21.67/21.81 (P1(f8(a1,a2),a6,a3)),
% 21.67/21.81 inference(scs_inference,[],[16,20,26,33,10])).
% 21.67/21.81 cnf(46,plain,
% 21.67/21.81 (P1(x461,a6,x461)),
% 21.67/21.81 inference(rename_variables,[],[20])).
% 21.67/21.81 cnf(47,plain,
% 21.67/21.81 (E(x471,f4(x471,a3))),
% 21.67/21.81 inference(scs_inference,[],[16,19,20,25,26,33,10,32])).
% 21.67/21.81 cnf(48,plain,
% 21.67/21.81 (P2(x481,x482,f4(x481,x482))),
% 21.67/21.81 inference(rename_variables,[],[25])).
% 21.67/21.81 cnf(50,plain,
% 21.67/21.81 (E(a3,f4(f8(a1,a2),a3))),
% 21.67/21.81 inference(scs_inference,[],[16,19,20,25,26,33,10,32,3])).
% 21.67/21.81 cnf(51,plain,
% 21.67/21.81 (P1(a6,f8(a1,a2),a3)),
% 21.67/21.81 inference(scs_inference,[],[16,19,20,22,25,26,33,10,32,3,11])).
% 21.67/21.81 cnf(52,plain,
% 21.67/21.81 (P1(a6,x521,x521)),
% 21.67/21.81 inference(rename_variables,[],[22])).
% 21.67/21.81 cnf(54,plain,
% 21.67/21.81 (P1(x541,a6,x541)),
% 21.67/21.81 inference(rename_variables,[],[20])).
% 21.67/21.81 cnf(55,plain,
% 21.67/21.81 (P2(f4(f8(a1,a2),a3),a3,f8(a1,a2))),
% 21.67/21.81 inference(scs_inference,[],[16,19,20,46,22,25,26,33,10,32,3,11,12,13])).
% 21.67/21.81 cnf(56,plain,
% 21.67/21.81 (P2(x561,a3,x561)),
% 21.67/21.81 inference(rename_variables,[],[19])).
% 21.67/21.81 cnf(57,plain,
% 21.67/21.81 (P2(x571,f8(a1,a2),x571)),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,20,46,22,25,26,33,10,32,3,11,12,13,14])).
% 21.67/21.81 cnf(58,plain,
% 21.67/21.81 (P2(a3,a3,f8(a1,a2))),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,20,46,22,25,26,33,10,32,3,11,12,13,14,15])).
% 21.67/21.81 cnf(59,plain,
% 21.67/21.81 (P2(x591,a3,x591)),
% 21.67/21.81 inference(rename_variables,[],[19])).
% 21.67/21.81 cnf(60,plain,
% 21.67/21.81 (P1(a1,a2,f8(a3,a6))),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,20,46,54,22,25,26,43,33,10,32,3,11,12,13,14,15,37])).
% 21.67/21.81 cnf(61,plain,
% 21.67/21.81 (P1(x611,a6,x611)),
% 21.67/21.81 inference(rename_variables,[],[20])).
% 21.67/21.81 cnf(62,plain,
% 21.67/21.81 (P1(x621,x622,f8(x621,x622))),
% 21.67/21.81 inference(rename_variables,[],[26])).
% 21.67/21.81 cnf(64,plain,
% 21.67/21.81 (P2(x641,f4(a3,a3),x641)),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,59,20,46,54,22,25,48,26,43,33,10,32,3,11,12,13,14,15,37,35])).
% 21.67/21.81 cnf(65,plain,
% 21.67/21.81 (P2(x651,x652,f4(x651,x652))),
% 21.67/21.81 inference(rename_variables,[],[25])).
% 21.67/21.81 cnf(67,plain,
% 21.67/21.81 (P2(a3,a3,f8(a1,f4(a2,a2)))),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,59,20,46,54,22,25,48,65,26,43,62,33,10,32,3,11,12,13,14,15,37,35,38])).
% 21.67/21.81 cnf(68,plain,
% 21.67/21.81 (P1(x681,x682,f8(x681,x682))),
% 21.67/21.81 inference(rename_variables,[],[26])).
% 21.67/21.81 cnf(69,plain,
% 21.67/21.81 (P2(x691,x692,f4(x691,x692))),
% 21.67/21.81 inference(rename_variables,[],[25])).
% 21.67/21.81 cnf(71,plain,
% 21.67/21.81 (P2(a3,a3,f8(f4(a1,a1),a2))),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,59,20,46,54,22,25,48,65,69,26,43,62,68,33,10,32,3,11,12,13,14,15,37,35,38,39])).
% 21.67/21.81 cnf(73,plain,
% 21.67/21.81 (P2(x731,x732,f4(x731,x732))),
% 21.67/21.81 inference(rename_variables,[],[25])).
% 21.67/21.81 cnf(75,plain,
% 21.67/21.81 (P1(a3,a6,f4(a3,a3))),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,59,20,46,54,61,22,25,48,65,69,73,26,43,62,68,33,10,32,3,11,12,13,14,15,37,35,38,39,40])).
% 21.67/21.81 cnf(76,plain,
% 21.67/21.81 (P2(x761,x762,f4(x761,x762))),
% 21.67/21.81 inference(rename_variables,[],[25])).
% 21.67/21.81 cnf(77,plain,
% 21.67/21.81 (P2(x771,a3,x771)),
% 21.67/21.81 inference(rename_variables,[],[19])).
% 21.67/21.81 cnf(79,plain,
% 21.67/21.81 (P1(x791,a6,x791)),
% 21.67/21.81 inference(rename_variables,[],[20])).
% 21.67/21.81 cnf(81,plain,
% 21.67/21.81 (P1(a6,a6,f4(a6,a3))),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,59,77,20,46,54,61,79,22,52,25,48,65,69,73,76,26,43,62,68,33,10,32,3,11,12,13,14,15,37,35,38,39,40,41])).
% 21.67/21.81 cnf(85,plain,
% 21.67/21.81 (P1(x851,a6,x851)),
% 21.67/21.81 inference(rename_variables,[],[20])).
% 21.67/21.81 cnf(87,plain,
% 21.67/21.81 (E(f8(a1,a2),a3)),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,59,77,20,46,54,61,79,22,52,25,48,65,69,73,76,26,43,62,68,33,10,32,3,11,12,13,14,15,37,35,38,39,40,41,2])).
% 21.67/21.81 cnf(88,plain,
% 21.67/21.81 (P1(a3,x881,a1)+~P1(a2,x881,a6)),
% 21.67/21.81 inference(scs_inference,[],[16,19,56,59,77,20,46,54,61,79,85,22,52,25,48,65,69,73,76,26,43,62,68,33,10,32,3,11,12,13,14,15,37,35,38,39,40,41,2,36])).
% 21.67/21.81 cnf(91,plain,
% 21.67/21.81 (E(f4(x911,a3),x911)),
% 21.67/21.81 inference(scs_inference,[],[47,2])).
% 21.67/21.81 cnf(92,plain,
% 21.67/21.81 (P1(f4(a1,a3),a2,a3)),
% 21.67/21.81 inference(scs_inference,[],[16,47,2,10])).
% 21.67/21.81 cnf(93,plain,
% 21.67/21.81 (E(x931,f4(x931,a3))),
% 21.67/21.81 inference(rename_variables,[],[47])).
% 21.67/21.81 cnf(94,plain,
% 21.67/21.81 (E(f8(a1,f4(a2,a2)),a3)),
% 21.67/21.81 inference(scs_inference,[],[16,67,21,47,2,10,32])).
% 21.67/21.81 cnf(95,plain,
% 21.67/21.81 (P2(a3,x951,x951)),
% 21.67/21.81 inference(rename_variables,[],[21])).
% 21.67/21.81 cnf(98,plain,
% 21.67/21.81 (E(x981,f4(x981,a3))),
% 21.67/21.81 inference(rename_variables,[],[47])).
% 21.67/21.81 cnf(99,plain,
% 21.67/21.81 (~E(a1,f8(a1,a2))),
% 21.67/21.81 inference(scs_inference,[],[16,27,75,67,21,47,93,87,2,10,32,12,3])).
% 21.67/21.81 cnf(100,plain,
% 21.67/21.81 (P2(x1001,f5(x1001),f8(a1,a2))),
% 21.67/21.81 inference(scs_inference,[],[16,27,75,42,67,21,23,47,93,87,2,10,32,12,3,15])).
% 21.67/21.81 cnf(107,plain,
% 21.67/21.81 (P2(a3,x1071,x1071)),
% 21.67/21.81 inference(rename_variables,[],[21])).
% 21.67/21.81 cnf(109,plain,
% 21.67/21.81 (P1(a3,a3,f8(a3,a2))),
% 21.67/21.81 inference(scs_inference,[],[16,27,75,42,67,21,95,23,47,93,98,87,18,26,2,10,32,12,3,15,13,11,14,34,37])).
% 21.67/21.81 cnf(110,plain,
% 21.67/21.81 (P1(a3,x1101,a3)),
% 21.67/21.81 inference(rename_variables,[],[18])).
% 21.67/21.81 cnf(113,plain,
% 21.67/21.81 (P1(f4(a3,a3),a6,a3)),
% 21.67/21.81 inference(scs_inference,[],[16,27,75,42,67,81,21,95,23,47,93,98,87,18,110,26,2,10,32,12,3,15,13,11,14,34,37,36])).
% 21.67/21.81 cnf(114,plain,
% 21.67/21.81 (P1(a3,x1141,a3)),
% 21.67/21.81 inference(rename_variables,[],[18])).
% 21.67/21.81 cnf(117,plain,
% 21.67/21.81 (P2(x1171,x1172,f4(x1171,x1172))),
% 21.67/21.81 inference(rename_variables,[],[25])).
% 21.67/21.81 cnf(119,plain,
% 21.67/21.81 (P2(f4(a3,a3),f4(a3,a3),a3)),
% 21.67/21.81 inference(scs_inference,[],[16,27,75,42,67,81,21,95,23,47,93,98,87,18,110,114,58,25,117,26,2,10,32,12,3,15,13,11,14,34,37,36,35,38])).
% 21.67/21.81 cnf(120,plain,
% 21.67/21.81 (P1(a3,x1201,a3)),
% 21.67/21.81 inference(rename_variables,[],[18])).
% 21.67/21.81 cnf(123,plain,
% 21.67/21.81 (P2(f4(a3,a3),f4(a3,a3),f8(a1,f4(a2,a2)))),
% 21.67/21.81 inference(scs_inference,[],[16,27,75,42,67,81,21,95,23,47,93,98,87,18,110,114,58,20,25,117,26,2,10,32,12,3,15,13,11,14,34,37,36,35,38,39])).
% 21.67/21.81 cnf(126,plain,
% 21.67/21.81 (P1(x1261,f8(a1,f4(a2,a2)),a3)),
% 21.67/21.81 inference(scs_inference,[],[16,27,75,42,67,81,21,95,107,23,47,93,98,87,17,18,110,114,58,20,25,117,26,2,10,32,12,3,15,13,11,14,34,37,36,35,38,39,41])).
% 21.67/21.81 cnf(127,plain,
% 21.67/21.81 (P2(a3,x1271,x1271)),
% 21.67/21.81 inference(rename_variables,[],[21])).
% 21.67/21.81 cnf(129,plain,
% 21.67/21.81 (P1(f8(a1,f4(a2,a2)),a6,f4(a3,a3))),
% 21.67/21.81 inference(scs_inference,[],[16,27,75,42,67,81,21,95,107,127,23,47,93,98,87,17,18,110,114,120,58,20,25,117,26,2,10,32,12,3,15,13,11,14,34,37,36,35,38,39,41,40])).
% 21.67/21.81 cnf(133,plain,
% 21.67/21.81 (E(f4(f8(a1,a2),a3),a3)),
% 21.67/21.81 inference(scs_inference,[],[50,2])).
% 21.67/21.81 cnf(134,plain,
% 21.67/21.81 (E(a3,f8(a1,f4(a2,a2)))),
% 21.67/21.81 inference(scs_inference,[],[126,50,22,2,33])).
% 21.67/21.81 cnf(135,plain,
% 21.67/21.81 (P1(a6,x1351,x1351)),
% 21.67/21.81 inference(rename_variables,[],[22])).
% 21.67/21.81 cnf(136,plain,
% 21.67/21.81 (P1(x1361,f8(a1,f4(a2,a2)),a3)),
% 21.67/21.81 inference(rename_variables,[],[126])).
% 21.67/21.81 cnf(138,plain,
% 21.67/21.81 (P1(f4(a1,a3),a2,f8(a3,a6))),
% 21.67/21.81 inference(scs_inference,[],[126,60,50,22,47,2,33,10])).
% 21.67/21.81 cnf(139,plain,
% 21.67/21.81 (E(x1391,f4(x1391,a3))),
% 21.67/21.81 inference(rename_variables,[],[47])).
% 21.67/21.81 cnf(140,plain,
% 21.67/21.81 (E(f8(f4(a1,a1),a2),a3)),
% 21.67/21.81 inference(scs_inference,[],[126,71,60,21,50,22,47,2,33,10,32])).
% 21.67/21.81 cnf(141,plain,
% 21.67/21.81 (P2(a3,x1411,x1411)),
% 21.67/21.81 inference(rename_variables,[],[21])).
% 21.67/21.81 cnf(144,plain,
% 21.67/21.81 (E(f4(x1441,a3),x1441)),
% 21.67/21.81 inference(rename_variables,[],[91])).
% 21.67/21.81 cnf(145,plain,
% 21.67/21.81 (P2(f4(a3,a3),f4(a3,a3),f8(a1,a2))),
% 21.67/21.81 inference(scs_inference,[],[129,126,119,71,60,42,21,91,50,22,47,2,33,10,32,12,15])).
% 21.67/21.81 cnf(146,plain,
% 21.67/21.81 (~E(a2,f4(a3,a3))),
% 21.67/21.81 inference(scs_inference,[],[28,129,126,119,71,60,42,21,91,144,50,22,47,2,33,10,32,12,15,3])).
% 21.67/21.81 cnf(147,plain,
% 21.67/21.81 (E(f4(x1471,a3),x1471)),
% 21.67/21.81 inference(rename_variables,[],[91])).
% 21.67/21.81 cnf(149,plain,
% 21.67/21.81 (E(f4(x1491,a3),x1491)),
% 21.67/21.81 inference(rename_variables,[],[91])).
% 21.67/21.81 cnf(152,plain,
% 21.67/21.81 (P1(f8(a1,f4(a2,a2)),f4(a6,a3),f4(a3,a3))),
% 21.67/21.81 inference(scs_inference,[],[28,123,129,126,119,71,60,42,21,91,144,147,149,50,22,47,139,2,33,10,32,12,15,3,14,13,11])).
% 21.67/21.81 cnf(154,plain,
% 21.67/21.81 (P2(f8(a1,f4(a2,a2)),f4(a3,a3),f4(a3,a3))),
% 21.67/21.81 inference(scs_inference,[],[28,123,129,126,119,71,60,42,21,64,91,144,147,149,50,22,47,139,2,33,10,32,12,15,3,14,13,11,34])).
% 21.67/21.81 cnf(155,plain,
% 21.67/21.81 (P2(x1551,f4(a3,a3),x1551)),
% 21.67/21.81 inference(rename_variables,[],[64])).
% 21.67/21.81 cnf(157,plain,
% 21.67/21.81 (P1(f8(a3,a2),f8(a1,f4(a2,a2)),f8(a3,a2))),
% 21.67/21.81 inference(scs_inference,[],[28,123,129,126,136,119,71,60,109,42,21,64,91,144,147,149,50,22,47,139,2,33,10,32,12,15,3,14,13,11,34,36])).
% 21.67/21.81 cnf(158,plain,
% 21.67/21.81 (P1(x1581,f8(a1,f4(a2,a2)),a3)),
% 21.67/21.81 inference(rename_variables,[],[126])).
% 21.67/21.81 cnf(161,plain,
% 21.67/21.81 (P2(x1611,f4(a3,a3),x1611)),
% 21.67/21.81 inference(rename_variables,[],[64])).
% 21.67/21.81 cnf(163,plain,
% 21.67/21.81 (P1(x1631,f4(a3,a3),f4(a3,a3))),
% 21.67/21.81 inference(scs_inference,[],[28,123,129,126,136,158,119,71,60,109,42,75,21,64,155,91,144,147,149,50,22,47,139,2,33,10,32,12,15,3,14,13,11,34,36,35,37])).
% 21.67/21.81 cnf(165,plain,
% 21.67/21.81 (P2(f8(a3,a2),f8(a3,a2),f8(a3,a2))),
% 21.67/21.81 inference(scs_inference,[],[28,123,129,126,136,158,119,71,60,109,42,75,21,141,64,155,91,144,147,149,50,22,47,139,2,33,10,32,12,15,3,14,13,11,34,36,35,37,39])).
% 21.67/21.81 cnf(173,plain,
% 21.67/21.81 (P1(f8(a1,a2),f8(a1,f4(a2,a2)),f8(a1,a2))),
% 21.67/21.81 inference(scs_inference,[],[28,123,129,126,136,158,119,71,60,109,42,75,21,141,64,155,161,91,144,147,149,50,58,22,135,47,139,2,33,10,32,12,15,3,14,13,11,34,36,35,37,39,41,40])).
% 21.67/21.81 cnf(178,plain,
% 21.67/21.81 (E(a3,f8(f4(a1,a1),a2))),
% 21.67/21.81 inference(scs_inference,[],[140,2])).
% 21.67/21.81 cnf(179,plain,
% 21.67/21.81 (E(f8(a3,a2),a3)),
% 21.67/21.81 inference(scs_inference,[],[109,140,17,2,33])).
% 21.67/21.81 cnf(182,plain,
% 21.67/21.81 (E(f5(a3),a3)),
% 21.67/21.81 inference(scs_inference,[],[109,21,23,140,17,2,33,32])).
% 21.67/21.81 cnf(188,plain,
% 21.67/21.81 (E(x1881,f4(x1881,a3))),
% 21.67/21.81 inference(rename_variables,[],[47])).
% 21.67/21.81 cnf(191,plain,
% 21.67/21.81 (~E(a1,f8(a1,f4(a2,a2)))),
% 21.67/21.81 inference(scs_inference,[],[16,27,173,165,134,109,21,23,94,140,87,17,47,2,33,32,10,15,12,11,3])).
% 21.67/21.81 cnf(193,plain,
% 21.67/21.81 (E(x1931,f4(x1931,a3))),
% 21.67/21.81 inference(rename_variables,[],[47])).
% 21.67/21.81 cnf(196,plain,
% 21.67/21.81 (P1(a3,f4(a3,a3),f8(a1,f4(a3,a3)))),
% 21.67/21.81 inference(scs_inference,[],[16,27,173,163,165,134,109,21,23,94,140,87,26,17,47,188,193,2,33,32,10,15,12,11,3,13,14,36])).
% 21.67/21.81 cnf(198,plain,
% 21.67/21.81 (P1(x1981,f4(a3,a3),f4(a3,a3))),
% 21.67/21.81 inference(rename_variables,[],[163])).
% 21.67/21.81 cnf(207,plain,
% 21.67/21.81 (P1(x2071,f4(a3,a3),f4(a3,a3))),
% 21.67/21.81 inference(rename_variables,[],[163])).
% 21.67/21.81 cnf(210,plain,
% 21.67/21.81 (P2(f8(a1,a2),f8(a1,a2),a3)),
% 21.67/21.81 inference(scs_inference,[],[16,27,173,163,198,165,134,126,109,123,24,21,23,57,154,94,140,87,18,26,17,47,188,193,2,33,32,10,15,12,11,3,13,14,36,34,35,37,39])).
% 21.67/21.81 cnf(214,plain,
% 21.67/21.81 (P1(x2141,f8(a1,a2),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,27,173,163,198,207,165,134,126,109,123,24,21,23,57,154,145,94,140,87,18,26,17,47,188,193,2,33,32,10,15,12,11,3,13,14,36,34,35,37,39,41])).
% 21.67/21.82 cnf(216,plain,
% 21.67/21.82 (P1(f8(a1,a2),f4(a3,a3),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,27,173,163,198,207,165,134,126,109,123,24,21,23,57,154,145,94,140,87,18,26,17,47,188,193,2,33,32,10,15,12,11,3,13,14,36,34,35,37,39,41,40])).
% 21.67/21.82 cnf(222,plain,
% 21.67/21.82 (E(f8(a1,a2),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[216,179,163,2,33])).
% 21.67/21.82 cnf(223,plain,
% 21.67/21.82 (P1(x2231,f4(a3,a3),f4(a3,a3))),
% 21.67/21.82 inference(rename_variables,[],[163])).
% 21.67/21.82 cnf(225,plain,
% 21.67/21.82 (E(f5(a3),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[216,179,163,21,100,2,33,32])).
% 21.67/21.82 cnf(226,plain,
% 21.67/21.82 (P2(x2261,f5(x2261),f8(a1,a2))),
% 21.67/21.82 inference(rename_variables,[],[100])).
% 21.67/21.82 cnf(227,plain,
% 21.67/21.82 (P2(a3,x2271,x2271)),
% 21.67/21.82 inference(rename_variables,[],[21])).
% 21.67/21.82 cnf(229,plain,
% 21.67/21.82 (P1(a3,f4(a3,a3),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[216,179,163,21,100,87,2,33,32,10])).
% 21.67/21.82 cnf(231,plain,
% 21.67/21.82 (E(x2311,f4(x2311,a3))),
% 21.67/21.82 inference(rename_variables,[],[47])).
% 21.67/21.82 cnf(232,plain,
% 21.67/21.82 (P2(f8(a1,a2),f8(a1,a2),f8(a1,f4(a2,a2)))),
% 21.67/21.82 inference(scs_inference,[],[138,216,210,179,163,134,21,100,87,47,2,33,32,10,12,15])).
% 21.67/21.82 cnf(234,plain,
% 21.67/21.82 (P2(f8(a1,f4(a2,a2)),x2341,x2341)),
% 21.67/21.82 inference(scs_inference,[],[138,216,210,179,163,134,21,227,100,87,47,2,33,32,10,12,15,14,13])).
% 21.67/21.82 cnf(237,plain,
% 21.67/21.82 (~E(a2,f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[28,138,216,210,179,163,134,21,227,100,87,47,231,2,33,32,10,12,15,14,13,11,3])).
% 21.67/21.82 cnf(241,plain,
% 21.67/21.82 (P1(f8(a1,a2),f4(a3,a3),a3)),
% 21.67/21.82 inference(scs_inference,[],[28,138,214,216,210,179,163,134,21,227,100,226,87,18,47,231,2,33,32,10,12,15,14,13,11,3,34,36])).
% 21.67/21.82 cnf(242,plain,
% 21.67/21.82 (P1(a3,x2421,a3)),
% 21.67/21.82 inference(rename_variables,[],[18])).
% 21.67/21.82 cnf(243,plain,
% 21.67/21.82 (P1(x2431,f8(a1,a2),f8(a1,a2))),
% 21.67/21.82 inference(rename_variables,[],[214])).
% 21.67/21.82 cnf(245,plain,
% 21.67/21.82 (P2(f8(a1,a2),a3,f5(f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[28,138,214,216,210,179,163,134,21,227,23,100,226,87,18,47,231,2,33,32,10,12,15,14,13,11,3,34,36,35])).
% 21.67/21.82 cnf(247,plain,
% 21.67/21.82 (P2(a3,x2471,x2471)),
% 21.67/21.82 inference(rename_variables,[],[21])).
% 21.67/21.82 cnf(250,plain,
% 21.67/21.82 (P1(x2501,f8(a1,a2),f8(a1,a2))),
% 21.67/21.82 inference(rename_variables,[],[214])).
% 21.67/21.82 cnf(253,plain,
% 21.67/21.82 (P2(f8(a1,a2),f8(a1,a2),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[16,28,138,214,243,216,210,179,163,223,134,21,227,23,100,226,87,18,242,47,231,2,33,32,10,12,15,14,13,11,3,34,36,35,37,39])).
% 21.67/21.82 cnf(256,plain,
% 21.67/21.82 (P1(a6,a3,f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,28,138,214,243,250,216,210,179,163,223,134,21,227,247,23,100,226,51,87,18,242,47,231,2,33,32,10,12,15,14,13,11,3,34,36,35,37,39,41])).
% 21.67/21.82 cnf(258,plain,
% 21.67/21.82 (P1(x2581,f8(a1,a2),f8(a1,a2))),
% 21.67/21.82 inference(rename_variables,[],[214])).
% 21.67/21.82 cnf(260,plain,
% 21.67/21.82 (P1(a3,f8(a1,a2),f4(f8(a1,a2),f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[16,28,138,214,243,250,258,216,210,179,163,223,134,21,227,247,23,100,226,51,87,25,18,242,47,231,2,33,32,10,12,15,14,13,11,3,34,36,35,37,39,41,40])).
% 21.67/21.82 cnf(267,plain,
% 21.67/21.82 (E(f4(a3,a3),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[222,2])).
% 21.67/21.82 cnf(268,plain,
% 21.67/21.82 (E(f4(f8(a1,a2),f8(a1,a2)),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[222,260,214,2,33])).
% 21.67/21.82 cnf(269,plain,
% 21.67/21.82 (P1(x2691,f8(a1,a2),f8(a1,a2))),
% 21.67/21.82 inference(rename_variables,[],[214])).
% 21.67/21.82 cnf(271,plain,
% 21.67/21.82 (E(f4(a3,a3),f4(f8(a1,a2),f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[253,222,260,214,25,2,33,32])).
% 21.67/21.82 cnf(272,plain,
% 21.67/21.82 (P2(x2721,x2722,f4(x2721,x2722))),
% 21.67/21.82 inference(rename_variables,[],[25])).
% 21.67/21.82 cnf(274,plain,
% 21.67/21.82 (P1(a3,f8(a1,f4(a2,a2)),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[157,253,222,260,214,179,25,2,33,32,10])).
% 21.67/21.82 cnf(277,plain,
% 21.67/21.82 (E(x2771,f4(x2771,a3))),
% 21.67/21.82 inference(rename_variables,[],[47])).
% 21.67/21.82 cnf(278,plain,
% 21.67/21.82 (~E(a2,f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[60,157,253,222,260,214,179,165,146,25,47,2,33,32,10,15,12,3])).
% 21.67/21.82 cnf(281,plain,
% 21.67/21.82 (P2(f8(a1,a2),f4(a3,a3),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[60,157,253,222,260,214,179,165,146,25,47,277,2,33,32,10,15,12,3,11,14])).
% 21.67/21.82 cnf(285,plain,
% 21.67/21.82 (P1(x2851,f8(a1,a2),f8(a1,a2))),
% 21.67/21.82 inference(rename_variables,[],[214])).
% 21.67/21.82 cnf(293,plain,
% 21.67/21.82 (P1(a6,f4(f8(a1,a2),f8(a1,a2)),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,60,157,253,222,260,256,214,269,285,179,165,210,67,234,146,100,25,26,47,277,2,33,32,10,15,12,3,11,14,13,36,35,34,37])).
% 21.67/21.82 cnf(294,plain,
% 21.67/21.82 (P1(x2941,f8(a1,a2),f8(a1,a2))),
% 21.67/21.82 inference(rename_variables,[],[214])).
% 21.67/21.82 cnf(296,plain,
% 21.67/21.82 (P2(f4(a6,a3),f4(a6,a3),f4(a6,a6))),
% 21.67/21.82 inference(scs_inference,[],[16,60,81,157,253,222,260,256,214,269,285,179,165,210,67,234,146,100,22,25,272,26,47,277,2,33,32,10,15,12,3,11,14,13,36,35,34,37,38])).
% 21.67/21.82 cnf(300,plain,
% 21.67/21.82 (P1(a3,f4(a3,a3),f4(f8(a1,a2),f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[16,60,81,157,253,222,260,256,214,269,285,179,165,210,67,21,234,146,100,22,25,272,26,18,47,277,2,33,32,10,15,12,3,11,14,13,36,35,34,37,38,41])).
% 21.67/21.82 cnf(304,plain,
% 21.67/21.82 (P1(f4(a3,a3),f8(a1,a2),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[16,60,81,157,253,222,260,256,214,269,285,294,179,165,210,67,21,234,146,100,22,25,272,26,18,47,277,2,33,32,10,15,12,3,11,14,13,36,35,34,37,38,41,40])).
% 21.67/21.82 cnf(310,plain,
% 21.67/21.82 (E(f4(a6,a6),f4(f4(a6,a3),f4(a6,a3)))),
% 21.67/21.82 inference(scs_inference,[],[268,296,25,2,32])).
% 21.67/21.82 cnf(311,plain,
% 21.67/21.82 (P2(x3111,x3112,f4(x3111,x3112))),
% 21.67/21.82 inference(rename_variables,[],[25])).
% 21.67/21.82 cnf(316,plain,
% 21.67/21.82 (E(x3161,f4(x3161,a3))),
% 21.67/21.82 inference(rename_variables,[],[47])).
% 21.67/21.82 cnf(317,plain,
% 21.67/21.82 (P2(a6,f4(a6,a3),f4(a6,a6))),
% 21.67/21.82 inference(scs_inference,[],[268,92,304,296,134,267,91,25,47,2,32,10,12,15,13])).
% 21.67/21.82 cnf(318,plain,
% 21.67/21.82 (E(f4(x3181,a3),x3181)),
% 21.67/21.82 inference(rename_variables,[],[91])).
% 21.67/21.82 cnf(325,plain,
% 21.67/21.82 (P2(x3251,x3252,f4(x3251,x3252))),
% 21.67/21.82 inference(rename_variables,[],[25])).
% 21.67/21.82 cnf(327,plain,
% 21.67/21.82 (P2(f8(a1,a2),f5(a3),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[268,92,304,296,134,23,267,55,99,91,318,25,311,47,316,2,32,10,12,15,13,14,3,11,35,34])).
% 21.67/21.82 cnf(333,plain,
% 21.67/21.82 (P1(f4(a3,a3),a3,f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[268,92,304,296,229,241,163,134,23,267,55,99,91,318,25,311,18,47,316,2,32,10,12,15,13,14,3,11,35,34,36,37])).
% 21.67/21.82 cnf(336,plain,
% 21.67/21.82 (P1(f8(a1,f4(a2,a2)),f4(a6,a6),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[268,92,304,296,229,241,163,134,23,267,152,55,99,64,91,318,25,311,18,47,316,2,32,10,12,15,13,14,3,11,35,34,36,37,41])).
% 21.67/21.82 cnf(339,plain,
% 21.67/21.82 (P1(f4(a6,a6),f8(a1,a2),f4(f8(a1,a2),f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[268,92,304,296,229,241,214,163,134,23,267,152,55,99,64,91,318,25,311,325,18,47,316,2,32,10,12,15,13,14,3,11,35,34,36,37,41,40])).
% 21.67/21.82 cnf(344,plain,
% 21.67/21.82 (P2(f8(a3,a6),f8(a3,a6),f8(a3,a6))+~P2(a1,a1,a1)),
% 21.67/21.82 inference(scs_inference,[],[60,268,92,304,296,229,241,214,163,134,23,267,152,55,99,64,91,318,25,311,325,18,47,316,2,32,10,12,15,13,14,3,11,35,34,36,37,41,40,39])).
% 21.67/21.82 cnf(347,plain,
% 21.67/21.82 (E(a3,f4(f4(a3,a3),f4(a3,a3)))),
% 21.67/21.82 inference(scs_inference,[],[119,271,25,2,32])).
% 21.67/21.82 cnf(350,plain,
% 21.67/21.82 (P1(f8(a1,a2),f8(a1,f4(a2,a2)),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[274,119,42,271,25,2,32,10])).
% 21.67/21.82 cnf(351,plain,
% 21.67/21.82 (P1(x3511,f8(a1,f4(a2,a2)),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[274,126,119,42,271,25,2,32,10,12])).
% 21.67/21.82 cnf(352,plain,
% 21.67/21.82 (P2(f5(x3521),x3521,f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[274,126,119,42,24,271,25,2,32,10,12,15])).
% 21.67/21.82 cnf(356,plain,
% 21.67/21.82 (~E(a2,f4(f8(a1,a2),f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[274,157,126,119,268,42,24,271,278,94,25,2,32,10,12,15,13,14,11,3])).
% 21.67/21.82 cnf(357,plain,
% 21.67/21.82 (P2(f4(a3,a3),a3,f5(f4(a3,a3)))),
% 21.67/21.82 inference(scs_inference,[],[274,157,126,119,268,42,24,21,23,271,278,94,25,2,32,10,12,15,13,14,11,3,35])).
% 21.67/21.82 cnf(359,plain,
% 21.67/21.82 (P2(a3,x3591,x3591)),
% 21.67/21.82 inference(rename_variables,[],[21])).
% 21.67/21.82 cnf(361,plain,
% 21.67/21.82 (P1(f4(a3,a3),f8(a1,f4(a2,a2)),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[274,157,126,333,119,268,42,24,21,23,271,278,94,25,2,32,10,12,15,13,14,11,3,35,36])).
% 21.67/21.82 cnf(364,plain,
% 21.67/21.82 (P2(f4(a3,a3),f5(a3),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[274,157,126,333,119,268,42,253,24,21,23,271,327,278,94,25,2,32,10,12,15,13,14,11,3,35,36,34])).
% 21.67/21.82 cnf(373,plain,
% 21.67/21.82 (P1(a3,f8(a1,a2),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[81,274,157,126,300,333,119,268,304,214,42,253,24,26,21,359,23,271,327,278,57,94,25,18,2,32,10,12,15,13,14,11,3,35,36,34,37,41,40])).
% 21.67/21.82 cnf(377,plain,
% 21.67/21.82 (E(f8(a1,a2),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[225,2])).
% 21.67/21.82 cnf(378,plain,
% 21.67/21.82 (E(f8(a1,f4(a3,a3)),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[196,163,225,2,33])).
% 21.67/21.82 cnf(381,plain,
% 21.67/21.82 (E(f8(a1,f4(a2,a2)),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[196,163,123,225,64,2,33,32])).
% 21.67/21.82 cnf(382,plain,
% 21.67/21.82 (P2(x3821,f4(a3,a3),x3821)),
% 21.67/21.82 inference(rename_variables,[],[64])).
% 21.67/21.82 cnf(384,plain,
% 21.67/21.82 (P1(f8(a1,f4(a2,a2)),a3,f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[109,196,163,134,123,225,64,2,33,32,10])).
% 21.67/21.82 cnf(387,plain,
% 21.67/21.82 (P2(f5(x3871),x3871,f8(a1,f4(a2,a2)))),
% 21.67/21.82 inference(scs_inference,[],[109,336,196,163,134,123,24,225,267,64,2,33,32,10,12,13,15])).
% 21.67/21.82 cnf(388,plain,
% 21.67/21.82 (~E(a1,f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[27,109,336,196,163,179,134,123,24,225,267,64,2,33,32,10,12,13,15,3])).
% 21.67/21.82 cnf(392,plain,
% 21.67/21.82 (P2(f8(a1,f4(a2,a2)),x3921,x3921)),
% 21.67/21.82 inference(rename_variables,[],[234])).
% 21.67/21.82 cnf(396,plain,
% 21.67/21.82 (P2(a3,x3961,x3961)),
% 21.67/21.82 inference(rename_variables,[],[21])).
% 21.67/21.82 cnf(398,plain,
% 21.67/21.82 (P1(a3,f8(a1,f4(a2,a2)),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[16,27,109,126,339,336,196,71,163,222,179,134,123,24,26,21,23,232,225,267,234,64,2,33,32,10,12,13,15,3,14,11,35,34,36])).
% 21.67/21.82 cnf(402,plain,
% 21.67/21.82 (P1(a3,f8(a3,a2),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,27,274,157,109,126,339,336,196,71,163,222,179,134,123,24,26,21,23,232,225,267,234,64,2,33,32,10,12,13,15,3,14,11,35,34,36,37])).
% 21.67/21.82 cnf(404,plain,
% 21.67/21.82 (P2(f8(a1,a3),f8(a1,a3),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[16,27,274,157,109,126,339,336,196,71,163,222,179,134,123,24,26,21,23,232,225,267,234,392,64,2,33,32,10,12,13,15,3,14,11,35,34,36,37,38])).
% 21.67/21.82 cnf(407,plain,
% 21.67/21.82 (P2(f8(a3,a2),f8(a3,a2),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,27,274,157,109,126,339,336,196,71,163,222,179,134,123,24,26,21,23,351,232,225,267,234,392,64,2,33,32,10,12,13,15,3,14,11,35,34,36,37,38,39])).
% 21.67/21.82 cnf(410,plain,
% 21.67/21.82 (P1(f8(f4(a1,a1),a2),f8(a1,a2),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[16,27,274,157,109,126,339,336,373,196,71,163,222,179,134,123,24,26,21,23,351,232,225,267,234,392,64,382,2,33,32,10,12,13,15,3,14,11,35,34,36,37,38,39,40])).
% 21.67/21.82 cnf(413,plain,
% 21.67/21.82 (P1(a3,f8(f4(a1,a1),a2),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,27,274,157,109,126,339,336,373,196,71,163,222,179,134,123,24,26,21,396,23,17,351,232,225,267,234,392,64,382,2,33,32,10,12,13,15,3,14,11,35,34,36,37,38,39,40,41])).
% 21.67/21.82 cnf(417,plain,
% 21.67/21.82 (E(f4(a3,a3),f8(a1,f4(a3,a3)))),
% 21.67/21.82 inference(scs_inference,[],[378,2])).
% 21.67/21.82 cnf(418,plain,
% 21.67/21.82 (E(f8(a3,a2),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[157,378,351,2,33])).
% 21.67/21.82 cnf(421,plain,
% 21.67/21.82 (E(f8(a1,a2),f4(f8(a3,a2),f8(a3,a2)))),
% 21.67/21.82 inference(scs_inference,[],[157,378,407,351,25,2,33,32])).
% 21.67/21.82 cnf(422,plain,
% 21.67/21.82 (P2(x4221,x4222,f4(x4221,x4222))),
% 21.67/21.82 inference(rename_variables,[],[25])).
% 21.67/21.82 cnf(425,plain,
% 21.67/21.82 (E(f4(x4251,a3),x4251)),
% 21.67/21.82 inference(rename_variables,[],[91])).
% 21.67/21.82 cnf(429,plain,
% 21.67/21.82 (P2(f8(a3,a2),f8(a3,a2),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[157,361,410,378,407,179,222,351,91,425,25,2,33,32,10,12,13,15])).
% 21.67/21.82 cnf(438,plain,
% 21.67/21.82 (P1(a1,a3,f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,157,274,126,361,410,378,407,165,179,222,381,351,146,91,425,25,422,2,33,32,10,12,13,15,11,14,3,35,34,37])).
% 21.67/21.82 cnf(441,plain,
% 21.67/21.82 (P1(a3,f8(a1,a2),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,157,274,126,361,410,378,407,402,165,179,222,21,381,351,146,91,425,25,422,18,2,33,32,10,12,13,15,11,14,3,35,34,37,41])).
% 21.67/21.82 cnf(448,plain,
% 21.67/21.82 (E(f8(a1,a2),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[418,2])).
% 21.67/21.82 cnf(449,plain,
% 21.67/21.82 (E(f5(a3),f8(a1,f4(a2,a2)))),
% 21.67/21.82 inference(scs_inference,[],[418,19,387,2,32])).
% 21.67/21.82 cnf(451,plain,
% 21.67/21.82 (P2(x4511,a3,x4511)),
% 21.67/21.82 inference(rename_variables,[],[19])).
% 21.67/21.82 cnf(453,plain,
% 21.67/21.82 (P1(f4(a3,a3),f8(a1,f4(a2,a2)),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[350,418,222,19,387,2,32,10])).
% 21.67/21.82 cnf(454,plain,
% 21.67/21.82 (P2(f8(a1,a2),f8(a3,a2),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[350,165,418,222,19,387,2,32,10,13])).
% 21.67/21.82 cnf(465,plain,
% 21.67/21.82 (P1(f8(a3,a2),f8(a1,a2),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[28,274,109,350,214,165,253,404,418,441,222,19,451,23,387,182,417,381,47,2,32,10,13,12,15,3,14,11,34,36])).
% 21.67/21.82 cnf(476,plain,
% 21.67/21.82 (E(f4(f8(a3,a2),f8(a3,a2)),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[421,2])).
% 21.67/21.82 cnf(477,plain,
% 21.67/21.82 (P1(f4(a3,a3),a3,f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[384,421,381,2,10])).
% 21.67/21.82 cnf(479,plain,
% 21.67/21.82 (E(x4791,f4(x4791,a3))),
% 21.67/21.82 inference(rename_variables,[],[47])).
% 21.67/21.82 cnf(483,plain,
% 21.67/21.82 (P1(a3,f4(a3,a3),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[384,398,404,418,421,381,47,479,2,10,13,12,15,11])).
% 21.67/21.82 cnf(494,plain,
% 21.67/21.82 (P1(f8(a1,a3),f8(a1,f4(a2,a2)),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[157,384,398,253,361,404,418,119,26,281,23,421,449,245,191,417,381,47,479,2,10,13,12,15,11,3,14,34,35,37,36])).
% 21.67/21.82 cnf(496,plain,
% 21.67/21.82 (P1(x4961,f4(a3,a3),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[157,384,398,214,253,361,404,418,119,26,281,23,421,449,245,191,417,57,381,47,479,2,10,13,12,15,11,3,14,34,35,37,36,41])).
% 21.67/21.82 cnf(500,plain,
% 21.67/21.82 (E(f8(a3,a2),f4(f8(a3,a2),f8(a3,a2)))),
% 21.67/21.82 inference(scs_inference,[],[165,310,25,2,32])).
% 21.67/21.82 cnf(503,plain,
% 21.67/21.82 (P1(f4(a1,a3),a3,f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[438,165,310,25,47,2,32,10])).
% 21.67/21.82 cnf(511,plain,
% 21.67/21.82 (P2(f4(a3,a3),f8(a3,a2),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[438,165,418,134,119,281,476,429,310,278,417,25,47,2,32,10,13,12,11,15,3,14,34])).
% 21.67/21.82 cnf(513,plain,
% 21.67/21.82 (P2(a3,a3,f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[438,165,418,134,119,281,19,24,21,476,429,310,278,417,25,47,2,32,10,13,12,11,15,3,14,34,35])).
% 21.67/21.82 cnf(518,plain,
% 21.67/21.82 (P1(f8(a1,a3),a3,f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[438,165,333,418,134,119,281,19,24,21,476,429,310,483,278,417,25,47,2,32,10,13,12,11,15,3,14,34,35,36])).
% 21.67/21.82 cnf(520,plain,
% 21.67/21.82 (P1(x5201,f8(a3,a2),a3)),
% 21.67/21.82 inference(scs_inference,[],[438,165,333,418,134,119,26,17,281,19,24,21,476,429,310,483,278,417,25,47,2,32,10,13,12,11,15,3,14,34,35,36,37])).
% 21.67/21.82 cnf(524,plain,
% 21.67/21.82 (P1(f5(a3),f8(a1,f4(a2,a2)),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[438,165,126,333,418,134,119,26,17,281,19,24,21,476,429,310,483,278,417,25,47,2,32,10,13,12,11,15,3,14,34,35,36,37,40])).
% 21.67/21.82 cnf(527,plain,
% 21.67/21.82 (P2(f5(a3),f5(a3),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[438,165,126,333,418,134,119,26,17,281,19,24,21,476,429,310,483,278,234,417,25,47,2,32,10,13,12,11,15,3,14,34,35,36,37,40,38])).
% 21.67/21.82 cnf(533,plain,
% 21.67/21.82 (E(f4(f8(a3,a2),f8(a3,a2)),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[500,2])).
% 21.67/21.82 cnf(534,plain,
% 21.67/21.82 (P1(f8(a1,a2),a3,f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[109,42,500,2,10])).
% 21.67/21.82 cnf(535,plain,
% 21.67/21.82 (P2(f8(a1,a2),f5(a3),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[109,527,42,500,225,2,10,13])).
% 21.67/21.82 cnf(540,plain,
% 21.67/21.82 (E(f8(a3,a2),f4(f4(a3,a3),f4(a3,a3)))),
% 21.67/21.82 inference(scs_inference,[],[438,109,402,527,71,418,179,42,500,347,225,2,10,13,12,11,15,14,3])).
% 21.67/21.82 cnf(544,plain,
% 21.67/21.82 (P1(f8(a1,a3),f4(a3,a3),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[438,109,402,163,253,527,71,418,179,42,483,500,347,225,245,100,2,10,13,12,11,15,14,3,34,36])).
% 21.67/21.82 cnf(545,plain,
% 21.67/21.82 (P1(x5451,f4(a3,a3),f4(a3,a3))),
% 21.67/21.82 inference(rename_variables,[],[163])).
% 21.67/21.82 cnf(552,plain,
% 21.67/21.82 (P1(x5521,f4(a3,a3),f4(f8(a1,a2),f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[438,157,274,109,402,163,214,253,527,71,418,179,42,19,483,500,357,347,225,245,100,25,2,10,13,12,11,15,14,3,34,36,35,37,41])).
% 21.67/21.82 cnf(555,plain,
% 21.67/21.82 (P2(f4(a3,a3),f4(a3,a3),f4(f8(a1,a2),f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[438,157,274,109,402,163,545,214,253,527,71,418,179,42,19,483,500,357,347,225,245,100,25,2,10,13,12,11,15,14,3,34,36,35,37,41,39])).
% 21.67/21.82 cnf(567,plain,
% 21.67/21.82 (E(f8(a1,a2),f4(f4(a3,a3),f4(a3,a3)))),
% 21.67/21.82 inference(scs_inference,[],[398,402,413,527,378,418,134,281,19,448,540,182,271,94,2,10,13,12,11,15,14,3])).
% 21.67/21.82 cnf(568,plain,
% 21.67/21.82 (P1(x5681,f8(a3,a2),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[350,398,402,413,214,527,378,418,134,281,19,448,540,182,271,94,2,10,13,12,11,15,14,3,37])).
% 21.67/21.82 cnf(581,plain,
% 21.67/21.82 (E(f4(f4(a3,a3),f4(a3,a3)),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[567,2])).
% 21.67/21.82 cnf(582,plain,
% 21.67/21.82 (E(f8(a1,a3),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[544,496,567,2,33])).
% 21.67/21.82 cnf(583,plain,
% 21.67/21.82 (P1(x5831,f4(a3,a3),f8(a1,a2))),
% 21.67/21.82 inference(rename_variables,[],[496])).
% 21.67/21.82 cnf(596,plain,
% 21.67/21.82 (P1(a1,f8(a1,a3),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[438,157,398,465,477,524,544,253,496,527,555,418,25,567,388,533,449,91,94,2,33,10,13,12,15,11,14,3,34,37])).
% 21.67/21.82 cnf(598,plain,
% 21.67/21.82 (P1(f8(a1,a3),f8(a3,a2),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[438,157,398,465,477,524,544,518,253,496,520,527,555,418,25,567,388,533,449,91,94,2,33,10,13,12,15,11,14,3,34,37,36])).
% 21.67/21.82 cnf(599,plain,
% 21.67/21.82 (P1(x5991,f8(a3,a2),a3)),
% 21.67/21.82 inference(rename_variables,[],[520])).
% 21.67/21.82 cnf(601,plain,
% 21.67/21.82 (P2(f4(a3,a3),f4(a3,a3),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[438,157,398,465,477,524,544,518,253,496,520,527,119,555,418,21,511,25,567,388,533,449,91,94,2,33,10,13,12,15,11,14,3,34,37,36,35])).
% 21.67/21.82 cnf(604,plain,
% 21.67/21.82 (P2(f8(a1,a3),f8(a1,a3),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[438,157,398,465,477,524,544,518,253,496,583,520,404,527,119,555,418,21,511,25,567,388,533,449,91,94,2,33,10,13,12,15,11,14,3,34,37,36,35,39])).
% 21.67/21.82 cnf(607,plain,
% 21.67/21.82 (P1(f5(a3),f8(a3,a2),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[438,157,398,465,477,524,544,518,253,496,583,520,599,404,527,119,555,418,21,511,513,25,567,388,533,449,91,94,2,33,10,13,12,15,11,14,3,34,37,36,35,39,40])).
% 21.67/21.82 cnf(610,plain,
% 21.67/21.82 (P1(x6101,f5(a3),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[438,157,398,465,477,524,544,518,253,496,583,520,599,404,527,119,555,418,17,21,511,513,25,567,388,533,449,91,94,2,33,10,13,12,15,11,14,3,34,37,36,35,39,40,41])).
% 21.67/21.82 cnf(614,plain,
% 21.67/21.82 (E(f8(a1,a3),f4(f8(a1,a2),f8(a1,a2)))),
% 21.67/21.82 inference(scs_inference,[],[544,552,582,2,33])).
% 21.67/21.82 cnf(617,plain,
% 21.67/21.82 (P1(f8(a1,a2),f8(a1,f4(a2,a2)),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,544,552,582,2,33,10])).
% 21.67/21.82 cnf(618,plain,
% 21.67/21.82 (P2(f8(a1,a2),f8(a1,a3),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,544,552,404,582,2,33,10,13])).
% 21.67/21.82 cnf(620,plain,
% 21.67/21.82 (P2(f8(a1,a3),f8(a1,a3),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,465,544,552,404,604,582,222,179,2,33,10,13,12,15])).
% 21.67/21.82 cnf(623,plain,
% 21.67/21.82 (~E(a1,f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[350,494,465,544,552,404,604,582,222,179,99,381,2,33,10,13,12,15,11,14,3])).
% 21.67/21.82 cnf(646,plain,
% 21.67/21.82 (E(f8(a1,a3),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[544,163,614,2,33])).
% 21.67/21.82 cnf(649,plain,
% 21.67/21.82 (E(f8(a1,a2),f8(a1,f4(a2,a2)))),
% 21.67/21.82 inference(scs_inference,[],[544,163,614,352,387,2,33,32])).
% 21.67/21.82 cnf(652,plain,
% 21.67/21.82 (P1(f8(a1,f4(a2,a2)),f8(a1,a2),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[441,544,163,614,134,352,387,2,33,32,10])).
% 21.67/21.82 cnf(658,plain,
% 21.67/21.82 (~E(a2,f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[441,503,518,544,163,404,614,134,21,352,387,356,2,33,32,10,13,12,15,11,3])).
% 21.67/21.82 cnf(660,plain,
% 21.67/21.82 (P2(f4(a3,a3),f8(a1,a3),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[441,503,518,544,163,404,614,134,21,352,387,356,620,2,33,32,10,13,12,15,11,3,14,34])).
% 21.67/21.82 cnf(666,plain,
% 21.67/21.82 (P1(x6661,f8(a3,a2),a3)),
% 21.67/21.82 inference(rename_variables,[],[520])).
% 21.67/21.82 cnf(671,plain,
% 21.67/21.82 (P2(a3,a3,f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[441,503,518,544,253,496,520,666,163,333,527,404,596,614,568,134,21,352,387,356,620,2,33,32,10,13,12,15,11,3,14,34,37,36,35,39])).
% 21.67/21.82 cnf(683,plain,
% 21.67/21.82 (E(f4(a3,a3),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[646,2])).
% 21.67/21.82 cnf(684,plain,
% 21.67/21.82 (P1(f4(a3,a3),f8(a1,f4(a2,a2)),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,646,2,10])).
% 21.67/21.82 cnf(685,plain,
% 21.67/21.82 (P2(f4(a3,a3),f8(a1,a3),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,404,646,2,10,13])).
% 21.67/21.82 cnf(687,plain,
% 21.67/21.82 (P2(a3,f8(a1,a3),f4(a3,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,404,646,21,2,10,13,12,15])).
% 21.67/21.82 cnf(709,plain,
% 21.67/21.82 (E(f8(a1,f4(a2,a2)),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[649,2])).
% 21.67/21.82 cnf(710,plain,
% 21.67/21.82 (E(f8(a1,a3),a3)),
% 21.67/21.82 inference(scs_inference,[],[598,520,649,2,33])).
% 21.67/21.82 cnf(711,plain,
% 21.67/21.82 (P1(x7111,f8(a3,a2),a3)),
% 21.67/21.82 inference(rename_variables,[],[520])).
% 21.67/21.82 cnf(713,plain,
% 21.67/21.82 (E(f5(f8(a1,a2)),a3)),
% 21.67/21.82 inference(scs_inference,[],[598,520,57,24,649,2,33,32])).
% 21.67/21.82 cnf(721,plain,
% 21.67/21.82 (E(f8(a3,a2),f8(f4(a1,a1),a2))),
% 21.67/21.82 inference(scs_inference,[],[453,518,544,598,520,119,582,179,57,24,649,683,178,2,33,32,10,13,12,11,3])).
% 21.67/21.82 cnf(723,plain,
% 21.67/21.82 (P2(f8(a1,a2),f8(a1,a2),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[453,518,544,253,598,520,119,582,179,57,24,649,683,178,2,33,32,10,13,12,11,3,14,15])).
% 21.67/21.82 cnf(726,plain,
% 21.67/21.82 (P1(a3,f8(a1,a3),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[157,109,398,453,518,544,253,598,520,119,582,179,364,57,24,601,649,683,178,2,33,32,10,13,12,11,3,14,15,34,37])).
% 21.67/21.82 cnf(728,plain,
% 21.67/21.82 (P2(f4(a3,a3),f4(a3,a3),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[157,109,398,453,518,544,253,598,520,119,582,179,21,364,57,24,601,649,683,178,2,33,32,10,13,12,11,3,14,15,34,37,35])).
% 21.67/21.82 cnf(731,plain,
% 21.67/21.82 (P2(f8(a1,a3),f8(a1,a3),a3)),
% 21.67/21.82 inference(scs_inference,[],[157,109,398,453,518,544,253,598,520,711,404,119,582,179,21,364,57,24,601,649,683,178,2,33,32,10,13,12,11,3,14,15,34,37,35,39])).
% 21.67/21.82 cnf(734,plain,
% 21.67/21.82 (P1(f5(a3),f4(a3,a3),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[157,109,398,453,518,544,253,163,598,520,711,404,119,582,179,21,364,57,24,601,649,683,178,2,33,32,10,13,12,11,3,14,15,34,37,35,39,40])).
% 21.67/21.82 cnf(749,plain,
% 21.67/21.82 (E(f5(a3),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[607,710,568,2,33])).
% 21.67/21.82 cnf(750,plain,
% 21.67/21.82 (P1(x7501,f8(a3,a2),f8(a3,a2))),
% 21.67/21.82 inference(rename_variables,[],[568])).
% 21.67/21.82 cnf(752,plain,
% 21.67/21.82 (E(f5(f8(a1,a2)),f8(a1,a2))),
% 21.67/21.82 inference(scs_inference,[],[607,710,568,57,352,2,33,32])).
% 21.67/21.82 cnf(754,plain,
% 21.67/21.82 (P2(x7541,f8(a1,a2),x7541)),
% 21.67/21.82 inference(rename_variables,[],[57])).
% 21.67/21.82 cnf(756,plain,
% 21.67/21.82 (P1(a3,f8(a1,f4(a2,a2)),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[524,607,710,568,57,352,182,2,33,32,10])).
% 21.67/21.82 cnf(773,plain,
% 21.67/21.82 (P2(f5(a3),f5(a3),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[16,27,398,524,544,496,253,607,163,527,731,710,568,750,134,454,511,57,754,352,234,709,713,182,2,33,32,10,13,12,15,14,3,11,34,37,35,39])).
% 21.67/21.82 cnf(786,plain,
% 21.67/21.82 (E(f8(a3,a2),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[749,2])).
% 21.67/21.82 cnf(787,plain,
% 21.67/21.82 (E(f8(a1,a3),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[598,749,568,2,33])).
% 21.67/21.82 cnf(788,plain,
% 21.67/21.82 (P1(x7881,f8(a3,a2),f8(a3,a2))),
% 21.67/21.82 inference(rename_variables,[],[568])).
% 21.67/21.82 cnf(790,plain,
% 21.67/21.82 (P1(f8(a3,a2),f8(a1,f4(a2,a2)),f5(a3))),
% 21.67/21.82 inference(scs_inference,[],[524,598,749,568,2,33,10])).
% 21.67/21.82 cnf(794,plain,
% 21.67/21.82 (E(f5(a3),f8(f4(a1,a1),a2))),
% 21.67/21.82 inference(scs_inference,[],[494,524,598,527,749,568,721,709,2,33,10,13,12,11,3])).
% 21.67/21.82 cnf(804,plain,
% 21.67/21.82 (P2(f8(a1,a3),f8(a1,a3),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[494,465,524,598,214,527,404,749,773,568,788,21,25,721,709,2,33,10,13,12,11,3,14,15,37,35,39])).
% 21.67/21.82 cnf(818,plain,
% 21.67/21.82 (P1(f8(a3,a2),f8(a1,f4(a2,a2)),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,787,2,10])).
% 21.67/21.82 cnf(819,plain,
% 21.67/21.82 (P2(f8(a3,a2),f8(a1,a3),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,404,787,2,10,13])).
% 21.67/21.82 cnf(824,plain,
% 21.67/21.82 (E(f8(a1,a2),f8(f4(a1,a1),a2))),
% 21.67/21.82 inference(scs_inference,[],[494,524,518,404,787,749,535,377,794,709,2,10,13,12,15,11,14,3])).
% 21.67/21.82 cnf(825,plain,
% 21.67/21.82 (P2(f8(a3,a2),f8(a1,a3),f8(a3,a2))),
% 21.67/21.82 inference(scs_inference,[],[494,524,518,404,804,787,749,535,377,794,709,2,10,13,12,15,11,14,3,34])).
% 21.67/21.82 cnf(827,plain,
% 21.67/21.82 (P1(a1,f8(a1,a3),a3)),
% 21.67/21.82 inference(scs_inference,[],[494,524,518,598,596,520,404,804,787,749,535,377,794,709,2,10,13,12,15,11,14,3,34,37])).
% 21.67/21.82 cnf(833,plain,
% 21.67/21.82 (P1(x8331,f8(a1,a3),f8(a1,a3))),
% 21.67/21.82 inference(scs_inference,[],[494,524,518,598,596,520,214,404,804,787,749,535,25,723,377,794,709,2,10,13,12,15,11,14,3,34,37,35,41])).
% 21.81/21.82 cnf(851,plain,
% 21.81/21.82 (P1(x8511,f8(a3,a2),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[28,503,607,596,773,671,833,749,418,42,26,511,752,133,267,2,10,13,12,3,11,14,15,37])).
% 21.81/21.82 cnf(852,plain,
% 21.81/21.82 (P1(x8521,x8522,f8(x8521,x8522))),
% 21.81/21.82 inference(rename_variables,[],[26])).
% 21.81/21.82 cnf(853,plain,
% 21.81/21.82 (P1(x8531,f8(a1,a3),f8(a1,a3))),
% 21.81/21.82 inference(rename_variables,[],[833])).
% 21.81/21.82 cnf(854,plain,
% 21.81/21.82 (~P1(x8541,x8542,x8543)+~P1(x8544,x8541,x8545)+P1(x8544,x8543,x8546)+~P1(x8545,x8542,x8546)),
% 21.81/21.82 inference(rename_variables,[],[37])).
% 21.81/21.82 cnf(857,plain,
% 21.81/21.82 (P2(f8(a3,a2),f8(a3,a2),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[28,503,607,596,773,671,833,853,749,418,42,26,429,511,25,752,133,267,2,10,13,12,3,11,14,15,37,35,39])).
% 21.81/21.82 cnf(861,plain,
% 21.81/21.82 (E(f5(a3),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[28,503,607,596,773,671,833,853,749,418,42,26,429,511,25,752,133,267,2,10,13,12,3,11,14,15,37,35,39,33])).
% 21.81/21.82 cnf(863,plain,
% 21.81/21.82 (~P1(f8(x8631,a1),a2,x8632)+P1(x8631,a3,x8632)),
% 21.81/21.82 inference(scs_inference,[],[16,28,503,607,596,773,671,833,853,749,418,42,26,852,429,511,25,752,133,267,2,10,13,12,3,11,14,15,37,35,39,33,854])).
% 21.81/21.82 cnf(874,plain,
% 21.81/21.82 (P1(x8741,a3,f8(f8(x8741,a1),a2))),
% 21.81/21.82 inference(scs_inference,[],[26,863])).
% 21.81/21.82 cnf(877,plain,
% 21.81/21.82 (E(f8(a1,a3),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[861,26,863,2])).
% 21.81/21.82 cnf(878,plain,
% 21.81/21.82 (E(f8(a3,a2),f8(f8(a3,a1),a2))),
% 21.81/21.82 inference(scs_inference,[],[109,861,26,863,2,33])).
% 21.81/21.82 cnf(885,plain,
% 21.81/21.82 (P2(f5(a3),f5(a3),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[109,477,524,544,527,861,26,271,863,2,33,10,13,12,11,14,15])).
% 21.81/21.82 cnf(887,plain,
% 21.81/21.82 (P2(f8(a1,a3),f5(a3),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[27,109,477,524,544,527,861,26,140,271,863,2,33,10,13,12,11,14,15,3,34])).
% 21.81/21.82 cnf(898,plain,
% 21.81/21.82 (E(f8(f8(a3,a1),a2),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[878,2])).
% 21.81/21.82 cnf(904,plain,
% 21.81/21.82 (E(f8(a1,a3),f8(f8(a3,a1),a2))),
% 21.81/21.82 inference(scs_inference,[],[438,465,126,165,878,787,709,2,10,13,12,11,14,3])).
% 21.81/21.82 cnf(911,plain,
% 21.81/21.82 (E(f8(f4(a1,a1),a2),f8(a1,a2))),
% 21.81/21.82 inference(scs_inference,[],[824,2])).
% 21.81/21.82 cnf(912,plain,
% 21.81/21.82 (E(f8(a3,a2),f8(f8(a1,a1),a2))),
% 21.81/21.82 inference(scs_inference,[],[438,874,824,2,33])).
% 21.81/21.82 cnf(919,plain,
% 21.81/21.82 (E(f5(a3),f8(f8(a3,a1),a2))),
% 21.81/21.82 inference(scs_inference,[],[438,503,524,607,773,874,861,878,824,904,2,33,10,13,12,11,3])).
% 21.81/21.82 cnf(932,plain,
% 21.81/21.82 (E(f8(f8(a1,a1),a2),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[912,2])).
% 21.81/21.82 cnf(937,plain,
% 21.81/21.82 (E(f8(a1,a3),f8(f8(a1,a1),a2))),
% 21.81/21.82 inference(scs_inference,[],[109,465,607,165,912,787,2,10,12,13,11,3])).
% 21.81/21.82 cnf(940,plain,
% 21.81/21.82 (P1(a1,f5(a3),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[438,157,109,465,607,165,756,912,787,2,10,12,13,11,3,14,15,37])).
% 21.81/21.82 cnf(945,plain,
% 21.81/21.82 (E(f8(f8(a1,a1),a2),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[937,2])).
% 21.81/21.82 cnf(946,plain,
% 21.81/21.82 (P1(f4(a1,a3),f8(a1,a3),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[596,937,47,2,10])).
% 21.81/21.82 cnf(952,plain,
% 21.81/21.82 (E(f5(a3),f8(f8(a1,a1),a2))),
% 21.81/21.82 inference(scs_inference,[],[503,596,617,671,804,710,912,861,134,937,709,47,2,10,13,12,11,14,3])).
% 21.81/21.82 cnf(962,plain,
% 21.81/21.82 (P1(f8(a3,a2),f4(a3,a3),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[734,749,919,2,10])).
% 21.81/21.82 cnf(964,plain,
% 21.81/21.82 (E(f4(x9641,a3),x9641)),
% 21.81/21.82 inference(rename_variables,[],[91])).
% 21.81/21.82 cnf(969,plain,
% 21.81/21.82 (P2(x9691,f5(x9691),f4(a3,a3))),
% 21.81/21.82 inference(scs_inference,[],[163,734,604,710,222,749,100,945,658,919,91,964,2,10,11,12,13,3,15])).
% 21.81/21.82 cnf(974,plain,
% 21.81/21.82 (P2(f8(a1,a2),f8(a1,a3),f4(a3,a3))),
% 21.81/21.82 inference(scs_inference,[],[126,544,163,684,734,253,804,604,710,222,749,100,618,660,945,658,919,91,964,2,10,11,12,13,3,15,14,37,35])).
% 21.81/21.82 cnf(979,plain,
% 21.81/21.82 (E(f8(a3,a2),f4(a3,a3))),
% 21.81/21.82 inference(scs_inference,[],[438,126,544,607,163,165,684,734,520,253,804,604,710,222,749,100,618,660,945,658,919,91,964,2,10,11,12,13,3,15,14,37,35,41,33])).
% 21.81/21.82 cnf(986,plain,
% 21.81/21.82 (P1(a3,x9861,f8(a1,a2))+~P1(a2,x9861,f4(a3,a3))),
% 21.81/21.82 inference(scs_inference,[],[16,438,126,544,607,163,165,496,684,734,520,253,804,604,710,222,749,100,23,352,234,618,660,945,658,919,91,964,2,10,11,12,13,3,15,14,37,35,41,33,34,36])).
% 21.81/21.82 cnf(989,plain,
% 21.81/21.82 (E(f4(a3,a3),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[979,2])).
% 21.81/21.82 cnf(990,plain,
% 21.81/21.82 (P1(f4(f8(a1,a2),f8(a1,a2)),a3,f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[518,979,614,2,10])).
% 21.81/21.82 cnf(996,plain,
% 21.81/21.82 (P2(f5(a3),f5(a3),f4(a3,a3))),
% 21.81/21.82 inference(scs_inference,[],[157,518,596,165,773,804,979,614,237,898,2,10,11,13,12,3,14,15])).
% 21.81/21.82 cnf(997,plain,
% 21.81/21.82 (P1(f5(a3),f8(a1,a3),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[157,518,524,596,607,165,773,804,818,979,614,237,898,2,10,11,13,12,3,14,15,37])).
% 21.81/21.82 cnf(1020,plain,
% 21.81/21.82 (P1(x10201,f8(a3,a2),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[350,518,596,610,804,253,940,979,646,26,100,932,989,952,388,2,10,11,12,13,3,15,14,34,37])).
% 21.81/21.82 cnf(1024,plain,
% 21.81/21.82 (P2(f4(a3,a3),f5(a3),f4(f5(a3),f4(a3,a3)))),
% 21.81/21.82 inference(scs_inference,[],[350,518,596,610,804,253,940,979,646,26,100,728,25,932,989,952,388,2,10,11,12,13,3,15,14,34,37,35])).
% 21.81/21.82 cnf(1027,plain,
% 21.81/21.82 (E(f8(f8(a3,a1),a2),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[904,2])).
% 21.81/21.82 cnf(1034,plain,
% 21.81/21.82 (P2(x10341,f5(x10341),f8(a1,f4(a2,a2)))),
% 21.81/21.82 inference(scs_inference,[],[465,518,652,804,979,582,222,134,23,904,581,99,2,10,11,13,12,3,14,15])).
% 21.81/21.82 cnf(1035,plain,
% 21.81/21.82 (P2(a3,f4(a3,a3),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[465,518,652,804,671,979,582,222,134,23,819,687,904,581,99,2,10,11,13,12,3,14,15,35])).
% 21.81/21.82 cnf(1040,plain,
% 21.81/21.82 (P2(f8(a3,a2),f8(a3,a2),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[465,518,544,652,568,165,804,671,113,1020,979,582,222,134,26,23,819,687,904,581,99,2,10,11,13,12,3,14,15,35,37,39])).
% 21.81/21.82 cnf(1041,plain,
% 21.81/21.82 (P1(x10411,f8(a3,a2),f5(a3))),
% 21.81/21.82 inference(rename_variables,[],[1020])).
% 21.81/21.82 cnf(1045,plain,
% 21.81/21.82 (P1(x10451,f8(a3,a2),f8(a1,a2))),
% 21.81/21.82 inference(scs_inference,[],[465,518,544,652,568,165,520,804,671,113,1020,1041,979,582,222,134,26,100,23,819,687,904,581,99,2,10,11,13,12,3,14,15,35,37,39,41])).
% 21.81/21.82 cnf(1057,plain,
% 21.81/21.82 (E(a3,f5(f8(a1,a2)))),
% 21.81/21.82 inference(scs_inference,[],[713,2])).
% 21.81/21.82 cnf(1058,plain,
% 21.81/21.82 (P1(f8(a1,a2),f8(a1,a3),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[726,42,713,2,10])).
% 21.81/21.82 cnf(1069,plain,
% 21.81/21.82 (P2(a3,f4(a3,a3),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[441,652,163,726,671,857,45,378,979,42,26,21,825,687,911,713,989,278,2,10,11,12,13,3,15,14,37,35])).
% 21.81/21.82 cnf(1071,plain,
% 21.81/21.82 (P1(x10711,f8(a3,a2),f4(f8(a3,a2),f8(a3,a2)))),
% 21.81/21.82 inference(scs_inference,[],[441,652,165,163,568,726,671,857,45,378,979,42,26,21,825,687,25,911,713,989,278,2,10,11,12,13,3,15,14,37,35,41])).
% 21.81/21.82 cnf(1093,plain,
% 21.81/21.82 (P1(x10931,f8(a3,a2),f8(a1,f4(a2,a2)))),
% 21.81/21.82 inference(scs_inference,[],[157,165,684,163,734,520,857,119,336,1020,268,979,861,26,19,887,885,1034,623,1027,721,989,709,2,10,11,13,12,3,14,15,35,37,41])).
% 21.81/21.82 cnf(1097,plain,
% 21.81/21.82 (E(f8(a3,a2),f8(a1,f4(a2,a2)))),
% 21.81/21.82 inference(scs_inference,[],[157,165,684,568,163,734,520,857,119,336,1020,268,979,861,26,19,887,885,1034,623,1027,721,989,709,2,10,11,13,12,3,14,15,35,37,41,33])).
% 21.81/21.82 cnf(1105,plain,
% 21.81/21.82 (E(f8(a1,f4(a2,a2)),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[1097,2])).
% 21.81/21.82 cnf(1106,plain,
% 21.81/21.82 (P1(f8(a1,f4(a2,a2)),f8(a1,a3),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[726,1097,134,2,10])).
% 21.81/21.82 cnf(1119,plain,
% 21.81/21.82 (E(f8(f4(a1,a1),a2),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[794,2])).
% 21.81/21.82 cnf(1122,plain,
% 21.81/21.82 (P1(x11221,f8(a3,a2),f4(f8(a1,a2),f8(a1,a2)))),
% 21.81/21.82 inference(scs_inference,[],[552,940,794,989,47,2,10,11])).
% 21.81/21.82 cnf(1126,plain,
% 21.81/21.82 (~E(a2,f8(a1,f4(a2,a2)))),
% 21.81/21.82 inference(scs_inference,[],[503,552,940,857,407,1097,1105,237,794,989,47,2,10,11,13,12,14,3])).
% 21.81/21.82 cnf(1130,plain,
% 21.81/21.82 (P2(x11301,x11302,f4(x11301,x11302))),
% 21.81/21.82 inference(rename_variables,[],[25])).
% 21.81/21.82 cnf(1132,plain,
% 21.81/21.82 (P1(a1,f5(a3),a3)),
% 21.81/21.82 inference(scs_inference,[],[438,503,126,165,756,552,940,857,407,378,1097,19,25,1105,237,794,989,47,2,10,11,13,12,14,3,15,35,37])).
% 21.81/21.82 cnf(1138,plain,
% 21.81/21.82 (P2(f8(a3,a2),f8(a3,a2),f4(f8(a1,a2),f8(a1,a2)))),
% 21.81/21.82 inference(scs_inference,[],[438,503,465,126,165,568,756,552,940,857,407,378,1097,19,25,1130,1105,237,794,989,47,2,10,11,13,12,14,3,15,35,37,40,39])).
% 21.81/21.82 cnf(1143,plain,
% 21.81/21.82 (E(f8(a3,a2),f4(f8(a1,a2),f8(a1,a2)))),
% 21.81/21.82 inference(scs_inference,[],[568,1122,347,2,33])).
% 21.81/21.82 cnf(1149,plain,
% 21.81/21.82 (P2(f4(a3,a3),f8(a3,a2),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[726,568,163,790,1040,979,1122,347,267,2,33,10,11,12,13])).
% 21.81/21.82 cnf(1150,plain,
% 21.81/21.82 (P2(f5(x11501),x11501,f4(a3,a3))),
% 21.81/21.82 inference(scs_inference,[],[726,568,163,790,1040,979,222,352,1122,347,267,2,33,10,11,12,13,15])).
% 21.81/21.82 cnf(1162,plain,
% 21.81/21.82 (E(f5(a3),f4(a3,a3))),
% 21.81/21.82 inference(scs_inference,[],[1143,19,1150,2,32])).
% 21.81/21.82 cnf(1171,plain,
% 21.81/21.82 (~E(a1,f4(a3,a3))),
% 21.81/21.82 inference(scs_inference,[],[438,477,544,165,773,1143,19,1150,99,417,267,2,32,10,11,13,12,15,3])).
% 21.81/21.82 cnf(1179,plain,
% 21.81/21.82 (E(f4(a3,a3),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[1162,2])).
% 21.81/21.82 cnf(1189,plain,
% 21.81/21.82 (P1(a1,f5(a3),f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[503,465,568,940,671,833,857,997,1143,378,364,996,1162,1171,2,10,11,12,13,15,14,3,35,37])).
% 21.81/21.82 cnf(1209,plain,
% 21.81/21.82 (E(f8(a1,f4(a2,a2)),f5(a3))),
% 21.81/21.82 inference(scs_inference,[],[449,2])).
% 21.81/21.82 cnf(1222,plain,
% 21.81/21.82 (P1(a6,f8(a1,a3),f8(a3,a2))),
% 21.81/21.82 inference(scs_inference,[],[534,527,568,163,671,962,857,293,1040,990,179,23,387,25,1035,1105,449,683,2,10,11,12,13,15,14,34,35,37])).
% 21.81/21.82 cnf(1226,plain,
% 21.81/21.82 (E(f4(a3,a3),f8(a1,f4(a2,a2)))),
% 21.81/21.82 inference(scs_inference,[],[381,2])).
% 21.81/21.82 cnf(1227,plain,
% 21.81/21.82 (E(f5(a3),f4(f8(a1,a2),f8(a1,a2)))),
% 21.81/21.82 inference(scs_inference,[],[734,552,381,2,33])).
% 21.81/21.82 cnf(1239,plain,
% 21.81/21.82 (P1(x12391,a3,f8(a1,a3))),
% 21.81/21.82 inference(scs_inference,[],[398,652,734,726,527,552,833,857,827,418,23,26,387,1209,381,2,33,10,11,12,13,14,15,34,37])).
% 21.81/21.82 cnf(1247,plain,
% 21.81/21.82 (E(f8(a1,a2),f8(f8(a6,a1),a2))),
% 21.81/21.82 inference(scs_inference,[],[256,874,1227,2,33])).
% 21.81/21.82 cnf(1268,plain,
% 21.81/21.82 (E(f5(a3),f4(f5(a3),f5(a3)))),
% 21.81/21.82 inference(scs_inference,[],[527,1247,25,2,32])).
% 21.81/21.82 cnf(1313,plain,
% 21.81/21.82 (P1(a2,f7(a2),a6)),
% 21.81/21.82 inference(scs_inference,[],[134,1126,29,3])).
% 21.81/21.82 cnf(1314,plain,
% 21.81/21.82 (P1(a3,f7(a2),a1)),
% 21.81/21.82 inference(scs_inference,[],[1313,88])).
% 21.81/21.82 cnf(1323,plain,
% 21.81/21.82 (P2(a3,x13231,x13231)),
% 21.81/21.82 inference(rename_variables,[],[21])).
% 21.81/21.83 cnf(1326,plain,
% 21.81/21.83 (P1(x13261,f5(a3),f5(a3))),
% 21.81/21.83 inference(rename_variables,[],[610])).
% 21.81/21.83 cnf(1330,plain,
% 21.81/21.83 (P2(a1,a1,a1)),
% 21.81/21.83 inference(scs_inference,[],[465,756,520,610,253,119,1189,268,787,1143,1097,42,26,21,1323,685,974,1226,1313,88,10,11,3,12,13,14,15,37,35,39])).
% 21.81/21.83 cnf(1337,plain,
% 21.81/21.83 (P2(f8(a3,a6),f8(a3,a6),f8(a3,a6))),
% 21.81/21.83 inference(scs_inference,[],[465,756,527,520,610,1326,253,119,1189,1132,268,787,1143,1097,42,26,21,1323,685,1034,974,1226,1313,88,10,11,3,12,13,14,15,37,35,39,41,344])).
% 21.81/21.83 cnf(1344,plain,
% 21.81/21.83 (E(f8(a1,a3),f8(f8(x13441,a1),a2))),
% 21.81/21.83 inference(scs_inference,[],[1239,874,33])).
% 21.81/21.83 cnf(1349,plain,
% 21.81/21.83 (E(f8(a1,a3),f5(f8(a1,a2)))),
% 21.81/21.83 inference(scs_inference,[],[568,962,1239,874,710,418,1057,33,10,11,3])).
% 21.81/21.83 cnf(1355,plain,
% 21.81/21.83 (P2(f4(a3,a3),f5(a3),f8(a3,a2))),
% 21.81/21.83 inference(scs_inference,[],[946,568,962,1040,119,1239,874,710,418,1337,21,1149,1057,47,33,10,11,3,13,12,14,15,35])).
% 21.81/21.83 cnf(1370,plain,
% 21.81/21.83 (E(f5(a3),f8(f8(x13701,a1),a2))),
% 21.81/21.83 inference(scs_inference,[],[962,861,979,1344,1349,2,10,3])).
% 21.81/21.83 cnf(1375,plain,
% 21.81/21.83 (P2(a1,a1,f4(a1,a3))),
% 21.81/21.83 inference(scs_inference,[],[946,962,610,1040,1227,861,979,1138,1330,1344,47,1349,2,10,3,11,12,13,14,15])).
% 21.81/21.83 cnf(1389,plain,
% 21.81/21.83 (E(f8(a1,a3),f4(f8(a3,a2),f8(a3,a2)))),
% 21.81/21.83 inference(scs_inference,[],[962,520,787,912,500,1370,2,10,11,3])).
% 21.81/21.83 cnf(1394,plain,
% 21.81/21.83 (P1(a1,f4(f8(a3,a2),f8(a3,a2)),f8(a3,a2))),
% 21.81/21.83 inference(scs_inference,[],[16,726,568,962,520,671,1040,1071,787,912,500,1370,2,10,11,3,13,12,14,15,37])).
% 21.81/21.83 cnf(1403,plain,
% 21.81/21.83 (E(f8(a1,a3),f8(f4(a1,a1),a2))),
% 21.81/21.83 inference(scs_inference,[],[851,1058,710,222,1097,178,1389,2,10,11,3])).
% 21.81/21.83 cnf(1408,plain,
% 21.81/21.83 (P1(x14081,a1,f8(f8(a1,a3),f7(a2)))),
% 21.81/21.83 inference(scs_inference,[],[946,851,1058,1040,1239,1314,710,1227,222,1097,26,535,178,1389,2,10,11,3,12,13,14,15,37])).
% 21.81/21.83 cnf(1409,plain,
% 21.81/21.83 (P1(x14091,x14092,f8(x14091,x14092))),
% 21.81/21.83 inference(rename_variables,[],[26])).
% 21.81/21.83 cnf(1415,plain,
% 21.81/21.83 (E(f8(x14151,a1),f8(f8(a1,a3),f7(a2)))),
% 21.81/21.83 inference(scs_inference,[],[946,851,1058,1040,1239,1314,710,1227,222,1097,26,1409,352,535,25,317,178,1389,2,10,11,3,12,13,14,15,37,35,33])).
% 21.81/21.83 cnf(1428,plain,
% 21.81/21.83 (E(f8(f8(a1,a3),f7(a2)),f8(x14281,a1))),
% 21.81/21.83 inference(scs_inference,[],[1415,2])).
% 21.81/21.83 cnf(1431,plain,
% 21.81/21.83 (E(f8(a1,a3),f4(f8(a1,a2),a3))),
% 21.81/21.83 inference(scs_inference,[],[851,1106,710,1143,1415,50,1105,2,10,11,3])).
% 21.81/21.83 cnf(1437,plain,
% 21.81/21.83 (P1(x14371,f5(a3),a3)),
% 21.81/21.83 inference(scs_inference,[],[726,756,126,851,1106,1040,1239,268,710,1143,1415,57,50,1105,2,10,11,3,13,12,14,15,37])).
% 21.81/21.83 cnf(1450,plain,
% 21.81/21.83 (E(f8(a1,a3),f4(f4(a3,a3),f4(a3,a3)))),
% 21.81/21.83 inference(scs_inference,[],[1222,1045,787,179,540,47,1403,2,10,11,3])).
% 21.81/21.83 cnf(1467,plain,
% 21.81/21.83 (P1(f8(a1,f4(a2,a2)),f7(a2),a1)),
% 21.81/21.83 inference(scs_inference,[],[1314,134,1450,2,10])).
% 21.81/21.83 cnf(1469,plain,
% 21.81/21.83 (E(f4(f8(a1,a2),f8(a1,a2)),a3)),
% 21.81/21.83 inference(scs_inference,[],[520,1314,268,134,878,87,1450,2,10,11,3])).
% 21.81/21.83 cnf(1486,plain,
% 21.81/21.83 (E(f5(a3),f4(f8(a3,a2),f8(a3,a2)))),
% 21.81/21.83 inference(scs_inference,[],[413,1020,749,42,179,500,1431,2,10,11,3])).
% 21.81/21.83 cnf(1488,plain,
% 21.81/21.83 (P2(f8(a1,a2),f8(a1,a3),a3)),
% 21.81/21.83 inference(scs_inference,[],[163,413,731,1020,582,749,42,179,500,1226,1431,2,10,11,3,12,13])).
% 21.81/21.83 cnf(1491,plain,
% 21.81/21.83 (P1(a1,f8(f8(a2,a1),a2),f8(a1,a3))),
% 21.81/21.83 inference(scs_inference,[],[16,163,413,731,1020,1239,874,582,749,42,179,454,500,1226,1431,2,10,11,3,12,13,14,15,37])).
% 21.81/21.83 cnf(1493,plain,
% 21.81/21.83 (P1(x14931,a3,f8(a1,a3))),
% 21.81/21.83 inference(rename_variables,[],[1239])).
% 21.81/21.83 cnf(1498,plain,
% 21.81/21.83 (P2(f8(a1,a3),f8(a1,a3),f5(a3))),
% 21.81/21.83 inference(scs_inference,[],[16,527,163,413,671,731,1020,1239,1493,874,582,749,42,179,454,25,1069,500,1226,1431,2,10,11,3,12,13,14,15,37,35,39])).
% 21.81/21.83 cnf(1504,plain,
% 21.81/21.83 (E(x15041,f4(x15041,a3))),
% 21.81/21.83 inference(rename_variables,[],[47])).
% 21.81/21.83 cnf(1506,plain,
% 21.81/21.83 (E(f8(a1,f4(a3,a3)),f8(a3,a2))),
% 21.81/21.83 inference(scs_inference,[],[1020,293,378,979,989,47,1486,2,10,11,3])).
% 21.81/21.83 cnf(1513,plain,
% 21.81/21.83 (P1(x15131,a1,f8(f8(a1,a3),f7(a2)))),
% 21.81/21.83 inference(rename_variables,[],[1408])).
% 21.81/21.83 cnf(1519,plain,
% 21.81/21.83 (P2(f8(a3,a1),f8(a3,a1),f8(a3,a1))),
% 21.81/21.83 inference(scs_inference,[],[16,413,119,604,1020,293,1408,1337,1330,378,710,979,23,26,364,1355,1226,989,47,1504,1486,2,10,11,3,12,13,14,15,37,35,39])).
% 21.81/21.83 cnf(1521,plain,
% 21.81/21.83 (P1(f8(a3,a1),a1,f8(a3,a1))),
% 21.81/21.83 inference(scs_inference,[],[16,413,119,604,1020,293,1408,1513,1337,1330,378,710,979,23,26,364,1355,1226,989,47,1504,1486,2,10,11,3,12,13,14,15,37,35,39,36])).
% 21.81/21.83 cnf(1527,plain,
% 21.81/21.83 (E(f8(a1,f4(a3,a3)),f5(a3))),
% 21.81/21.83 inference(scs_inference,[],[1020,336,378,1097,1105,1179,1506,2,10,11,3])).
% 21.81/21.83 cnf(1529,plain,
% 21.81/21.83 (P2(f4(a3,a3),f8(a1,a3),f8(a1,a2))),
% 21.81/21.83 inference(scs_inference,[],[726,604,1020,336,378,646,1097,1105,1179,1506,2,10,11,3,12,13])).
% 21.81/21.83 cnf(1543,plain,
% 21.81/21.83 (E(f8(a1,f4(a3,a3)),a3)),
% 21.81/21.83 inference(scs_inference,[],[946,1106,1045,378,1143,1209,91,1469,2,10,11,12,3])).
% 21.81/21.83 cnf(1551,plain,
% 21.81/21.83 (P1(x15511,f4(a3,a3),f8(a3,f4(a6,a6)))),
% 21.81/21.83 inference(scs_inference,[],[946,940,126,610,1106,1045,731,336,378,614,1143,26,454,1209,91,1469,2,10,11,12,3,13,14,15,36,37])).
% 21.81/21.83 cnf(1563,plain,
% 21.81/21.83 (E(f4(a3,a3),f8(a3,f4(a6,a6)))),
% 21.81/21.83 inference(scs_inference,[],[163,1551,1527,2,33])).
% 21.81/21.83 cnf(1566,plain,
% 21.81/21.83 (P1(f8(a1,a2),f7(a2),a1)),
% 21.81/21.83 inference(scs_inference,[],[163,1314,42,1551,1527,2,33,10])).
% 21.81/21.83 cnf(1568,plain,
% 21.81/21.83 (E(x15681,f4(x15681,a3))),
% 21.81/21.83 inference(rename_variables,[],[47])).
% 21.81/21.83 cnf(1569,plain,
% 21.81/21.83 (E(f8(a1,f4(a3,a3)),f8(a1,a3))),
% 21.81/21.83 inference(scs_inference,[],[163,1314,378,42,1551,683,47,1527,2,33,10,11,3])).
% 21.81/21.83 cnf(1572,plain,
% 21.81/21.83 (E(x15721,f4(x15721,a3))),
% 21.81/21.83 inference(rename_variables,[],[47])).
% 21.81/21.83 cnf(1579,plain,
% 21.81/21.83 (P1(x15791,a1,a1)),
% 21.81/21.83 inference(scs_inference,[],[126,163,610,119,1314,1467,1337,1330,1227,378,42,1551,100,1034,1105,683,47,1568,1572,1024,1527,2,33,10,11,3,12,13,14,15,35,37])).
% 21.81/21.83 cnf(1592,plain,
% 21.81/21.83 (E(f8(f8(a1,a3),f7(a2)),a1)),
% 21.81/21.83 inference(scs_inference,[],[1408,1563,1579,2,33])).
% 21.81/21.83 cnf(1593,plain,
% 21.81/21.83 (P1(x15931,a1,a1)),
% 21.81/21.83 inference(rename_variables,[],[1579])).
% 21.81/21.83 cnf(1600,plain,
% 21.81/21.83 (P2(f4(a3,a3),f8(a3,f4(a6,a6)),a3)),
% 21.81/21.83 inference(scs_inference,[],[163,1222,119,113,1408,378,418,1563,1579,267,2,33,10,11,3,12,13,14])).
% 21.81/21.83 cnf(1602,plain,
% 21.81/21.83 (P1(a1,f8(f8(a1,a3),f7(a2)),a1)),
% 21.81/21.83 inference(scs_inference,[],[16,163,1222,253,119,113,1408,378,418,1563,1579,1593,267,2,33,10,11,3,12,13,14,15,37])).
% 21.81/21.83 cnf(1604,plain,
% 21.81/21.83 (P1(x16041,a1,a1)),
% 21.81/21.83 inference(rename_variables,[],[1579])).
% 21.81/21.83 cnf(1610,plain,
% 21.81/21.83 (P1(x16101,a1,a1)),
% 21.81/21.83 inference(rename_variables,[],[1579])).
% 21.81/21.83 cnf(1612,plain,
% 21.81/21.83 (P1(x16121,f4(a1,a3),f4(a1,a3))),
% 21.81/21.83 inference(scs_inference,[],[16,163,1222,253,119,113,1408,378,418,1563,1579,1593,1604,1610,21,1529,1375,267,2,33,10,11,3,12,13,14,15,37,35,40,41])).
% 21.81/21.83 cnf(1618,plain,
% 21.81/21.83 (P2(f4(a1,a3),f4(a1,a3),f4(a1,a3))),
% 21.81/21.83 inference(scs_inference,[],[16,163,1222,253,119,113,1408,1330,378,418,1563,1579,1593,1604,1610,21,1529,1375,267,2,33,10,11,3,12,13,14,15,37,35,40,41,986,36,38])).
% 21.81/21.83 cnf(1624,plain,
% 21.81/21.83 (E(f8(a1,a2),f8(a3,f4(a6,a6)))),
% 21.81/21.83 inference(scs_inference,[],[496,1551,1592,2,33])).
% 21.81/21.83 cnf(1634,plain,
% 21.81/21.83 (P2(f4(a1,a3),f4(a1,a3),a1)),
% 21.81/21.83 inference(scs_inference,[],[496,833,129,1330,1498,1551,710,1618,1592,1415,1563,1209,91,47,2,33,10,11,3,12,13,14,15])).
% 21.81/21.83 cnf(1640,plain,
% 21.81/21.83 (P1(x16401,f8(a3,a6),f8(a3,a6))),
% 21.81/21.83 inference(scs_inference,[],[138,496,833,253,129,1330,1521,1498,1551,710,1612,1618,1592,1602,1415,1563,685,1488,1209,91,47,2,33,10,11,3,12,13,14,15,36,35,37])).
% 21.81/21.83 cnf(1657,plain,
% 21.81/21.83 (P2(x16571,f5(x16571),f8(a3,f4(a6,a6)))),
% 21.81/21.83 inference(scs_inference,[],[833,604,1093,336,787,222,179,1624,1563,969,94,417,2,10,11,3,13,12,14,15])).
% 21.81/21.83 cnf(1682,plain,
% 21.81/21.83 (E(a3,f8(a3,f4(a6,a6)))),
% 21.81/21.83 inference(scs_inference,[],[23,1657,1569,2,32])).
% 21.81/21.83 cnf(1683,plain,
% 21.81/21.83 (P2(x16831,f5(x16831),f8(a3,f4(a6,a6)))),
% 21.81/21.83 inference(rename_variables,[],[1657])).
% 21.81/21.83 cnf(1685,plain,
% 21.81/21.83 (P1(f8(a3,a2),f7(a2),a1)),
% 21.81/21.83 inference(scs_inference,[],[1467,23,1105,1657,1569,2,32,10])).
% 21.81/21.83 cnf(1701,plain,
% 21.81/21.83 (P1(x17011,f5(a3),f5(a3))),
% 21.81/21.83 inference(rename_variables,[],[610])).
% 21.81/21.83 cnf(1703,plain,
% 21.81/21.83 (E(f5(a3),f8(a3,f4(a6,a6)))),
% 21.81/21.83 inference(scs_inference,[],[16,527,833,610,1701,119,1020,1467,1498,1437,1612,582,646,418,1563,23,26,21,364,1600,1105,1657,1683,1569,2,32,10,11,3,13,12,14,15,35,37,41,33])).
% 21.81/21.83 cnf(1716,plain,
% 21.81/21.83 (P1(f5(a3),f7(a2),a1)),
% 21.81/21.83 inference(scs_inference,[],[1467,1703,1209,2,10])).
% 21.81/21.83 cnf(1730,plain,
% 21.81/21.83 (P2(f8(a3,a1),f8(a3,a1),a1)),
% 21.81/21.83 inference(scs_inference,[],[16,833,604,1467,45,1519,1521,1579,614,1703,26,618,25,1634,786,1209,47,2,10,11,3,13,12,14,15,35,37,39])).
% 21.81/21.83 cnf(1759,plain,
% 21.81/21.83 (P1(f4(a3,a3),f7(a2),a1)),
% 21.81/21.83 inference(scs_inference,[],[1566,222,1682,2,10])).
% 21.81/21.83 cnf(1798,plain,
% 21.81/21.83 (E(x17981,f4(x17981,a3))),
% 21.81/21.83 inference(rename_variables,[],[47])).
% 21.81/21.83 cnf(1799,plain,
% 21.81/21.83 (P1(x17991,f4(a1,a3),f8(f8(a1,a3),f7(a2)))),
% 21.81/21.83 inference(scs_inference,[],[1408,1394,47,1798,1543,2,10,11])).
% 21.81/21.83 cnf(1801,plain,
% 21.81/21.83 (E(f8(a1,a3),f4(f5(a3),f5(a3)))),
% 21.81/21.83 inference(scs_inference,[],[1408,1394,877,47,1798,1543,1268,2,10,11,3])).
% 21.81/21.83 cnf(1820,plain,
% 21.81/21.83 (E(f4(a1,a3),f8(f8(a1,a3),f7(a2)))),
% 21.81/21.83 inference(scs_inference,[],[1612,1801,1799,2,33])).
% 21.81/21.83 cnf(1826,plain,
% 21.81/21.83 (E(f5(a3),f5(f8(a1,a2)))),
% 21.81/21.83 inference(scs_inference,[],[1685,1716,1612,1227,861,47,1801,1799,1349,2,33,10,11,3])).
% 21.81/21.83 cnf(1895,plain,
% 21.81/21.83 (E(f8(f4(a1,a1),a2),f4(a3,a3))),
% 21.81/21.83 inference(scs_inference,[],[1640,75,42,1119,1162,47,1826,2,10,11,3])).
% 21.81/21.83 cnf(1916,plain,
% 21.81/21.83 (E(f4(a1,a3),f8(x19161,a1))),
% 21.81/21.83 inference(scs_inference,[],[1521,1759,1820,1563,47,1895,1428,2,10,11,3])).
% 21.81/21.83 cnf(1925,plain,
% 21.81/21.83 (P1(x19251,f4(a3,a3),f8(f8(a1,a3),a6))),
% 21.81/21.83 inference(scs_inference,[],[1239,113,1521,75,1759,134,979,1138,1730,1820,1415,1563,26,969,1150,601,47,1895,1428,2,10,11,3,13,12,14,15,34,37])).
% 21.81/21.83 cnf(1947,plain,
% 21.81/21.83 (E(x19471,f4(x19471,a3))),
% 21.81/21.83 inference(rename_variables,[],[47])).
% 21.81/21.83 cnf(1950,plain,
% 21.81/21.83 (E(f4(f4(a1,a3),a3),f8(x19501,a1))),
% 21.81/21.83 inference(scs_inference,[],[496,1759,1491,1925,91,47,1947,1916,2,33,11,10,3])).
% 21.81/21.83 cnf(2014,plain,
% 21.81/21.83 ($false),
% 21.81/21.83 inference(scs_inference,[],[27,1314,18,1950,2,33]),
% 21.81/21.83 ['proof']).
% 21.81/21.83 % SZS output end Proof
% 21.81/21.83 % Total time :21.090000s
%------------------------------------------------------------------------------