%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN007-2 : 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 : n026.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 07:26:49 EDT 2024
% Result : Unsatisfiable 59.19s 59.23s
% Output : CNFRefutation 59.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : HEN007-2 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sat Jun 22 05:25:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 59.11/59.22 %-------------------------------------------
% 59.11/59.22 % File :CSE---1.7
% 59.11/59.22 % Problem :theBenchmark
% 59.11/59.22 % Transform :cnf
% 59.11/59.22 % Format :tptp:raw
% 59.11/59.22 % Command :java -jar mcs_scs.jar %d %s
% 59.11/59.22
% 59.11/59.22 % Result :Theorem 58.620000s
% 59.11/59.22 % Output :CNFRefutation 58.620000s
% 59.11/59.22 %-------------------------------------------
% 59.19/59.23 %--------------------------------------------------------------------------
% 59.19/59.23 % File : HEN007-2 : TPTP v8.2.0. Released v1.0.0.
% 59.19/59.23 % Domain : Henkin Models
% 59.19/59.23 % Problem : X <= Y => Z/Y <= Z/X
% 59.19/59.23 % Version : [MOW76] axioms : Augmented.
% 59.19/59.23 % English :
% 59.19/59.23
% 59.19/59.23 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 59.19/59.23 % Source : [MOW76]
% 59.19/59.23 % Names : H7 [MOW76]
% 59.19/59.23
% 59.19/59.23 % Status : Unsatisfiable
% 59.19/59.23 % Rating : 0.06 v8.2.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 59.19/59.23 % Syntax : Number of clauses : 19 ( 11 unt; 0 nHn; 12 RR)
% 59.19/59.23 % Number of literals : 36 ( 2 equ; 18 neg)
% 59.19/59.23 % Maximal clause size : 6 ( 1 avg)
% 59.19/59.23 % Maximal term depth : 2 ( 1 avg)
% 59.19/59.23 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 59.19/59.23 % Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% 59.19/59.23 % Number of variables : 37 ( 5 sgn)
% 59.19/59.23 % SPC : CNF_UNS_RFO_SEQ_HRN
% 59.19/59.23
% 59.19/59.23 % Comments :
% 59.19/59.23 %--------------------------------------------------------------------------
% 59.19/59.23 %----Include Henkin model axioms
% 59.19/59.23 include('Axioms/HEN001-0.ax').
% 59.19/59.23 %--------------------------------------------------------------------------
% 59.19/59.23 %----McCharen uses these earlier results too. I don't
% 59.19/59.23 cnf(everything_divide_identity_is_zero,axiom,
% 59.19/59.23 quotient(X,identity,zero) ).
% 59.19/59.23
% 59.19/59.23 cnf(zero_divide_anything_is_zero,axiom,
% 59.19/59.23 quotient(zero,X,zero) ).
% 59.19/59.23
% 59.19/59.23 cnf(x_divide_x_is_zero,axiom,
% 59.19/59.23 quotient(X,X,zero) ).
% 59.19/59.23
% 59.19/59.23 cnf(x_divde_zero_is_x,axiom,
% 59.19/59.23 quotient(X,zero,X) ).
% 59.19/59.23
% 59.19/59.23 cnf(transitivity_of_less_equal,axiom,
% 59.19/59.23 ( ~ less_equal(X,Y)
% 59.19/59.23 | ~ less_equal(Y,Z)
% 59.19/59.23 | less_equal(X,Z) ) ).
% 59.19/59.23
% 59.19/59.23 cnf(xQyLEz_implies_xQzLEy,axiom,
% 59.19/59.23 ( ~ quotient(X,Y,W1)
% 59.19/59.23 | ~ less_equal(W1,Z)
% 59.19/59.23 | ~ quotient(X,Z,W2)
% 59.19/59.23 | less_equal(W2,Y) ) ).
% 59.19/59.23
% 59.19/59.23 cnf(xLEy,hypothesis,
% 59.19/59.23 less_equal(x,y) ).
% 59.19/59.23
% 59.19/59.23 cnf(zQy,hypothesis,
% 59.19/59.23 quotient(z,y,zQy) ).
% 59.19/59.23
% 59.19/59.23 cnf(zQx,hypothesis,
% 59.19/59.23 quotient(z,x,zQx) ).
% 59.19/59.23
% 59.19/59.23 cnf(prove_zQyLEzQx,negated_conjecture,
% 59.19/59.23 ~ less_equal(zQy,zQx) ).
% 59.19/59.23
% 59.19/59.23 %--------------------------------------------------------------------------
% 59.19/59.23 %-------------------------------------------
% 59.19/59.23 % Proof found
% 59.19/59.23 % SZS status Theorem for theBenchmark
% 59.19/59.23 % SZS output start Proof
% 59.19/59.23 %ClaNum:29(EqnAxiom:10)
% 59.19/59.23 %VarNum:72(SingletonVarNum:37)
% 59.19/59.23 %MaxLitNum:6
% 59.19/59.23 %MaxfuncDepth:1
% 59.19/59.23 %SharedTerms:11
% 59.19/59.23 %goalClause: 21
% 59.19/59.23 %singleGoalClaCount:1
% 59.19/59.23 [11]P1(a1,a4)
% 59.19/59.23 [14]P2(a6,a1,a7)
% 59.19/59.23 [15]P2(a6,a4,a8)
% 59.19/59.23 [21]~P1(a8,a7)
% 59.19/59.23 [12]P1(x121,a2)
% 59.19/59.23 [13]P1(a5,x131)
% 59.19/59.23 [16]P2(x161,a2,a5)
% 59.19/59.23 [17]P2(a5,x171,a5)
% 59.19/59.23 [18]P2(x181,x181,a5)
% 59.19/59.23 [19]P2(x191,a5,x191)
% 59.19/59.23 [20]P2(x201,x202,f3(x201,x202))
% 59.19/59.23 [24]~P1(x241,x242)+P2(x241,x242,a5)
% 59.19/59.23 [25]P1(x251,x252)+~P2(x251,x252,a5)
% 59.19/59.23 [26]P1(x261,x262)+~P2(x262,x263,x261)
% 59.19/59.23 [22]~P1(x222,x221)+~P1(x221,x222)+E(x221,x222)
% 59.19/59.23 [23]~P1(x231,x233)+P1(x231,x232)+~P1(x233,x232)
% 59.19/59.23 [27]~P2(x273,x274,x271)+E(x271,x272)+~P2(x273,x274,x272)
% 59.19/59.23 [28]~P2(x285,x282,x283)+P1(x281,x282)+~P2(x285,x284,x281)+~P1(x283,x284)
% 59.19/59.23 [29]~P2(x298,x297,x295)+P1(x291,x292)+~P2(x293,x294,x291)+~P2(x295,x296,x292)+~P2(x297,x296,x294)+~P2(x298,x296,x293)
% 59.19/59.23 %EqnAxiom
% 59.19/59.23 [1]E(x11,x11)
% 59.19/59.23 [2]E(x22,x21)+~E(x21,x22)
% 59.19/59.23 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.19/59.23 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 59.19/59.23 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 59.19/59.23 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 59.19/59.23 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 59.19/59.23 [8]P2(x82,x83,x84)+~E(x81,x82)+~P2(x81,x83,x84)
% 59.19/59.23 [9]P2(x93,x92,x94)+~E(x91,x92)+~P2(x93,x91,x94)
% 59.19/59.23 [10]P2(x103,x104,x102)+~E(x101,x102)+~P2(x103,x104,x101)
% 59.19/59.23
% 59.19/59.23 %-------------------------------------------
% 59.19/59.24 cnf(30,plain,
% 59.19/59.24 (P1(x301,x301)),
% 59.19/59.24 inference(scs_inference,[],[18,25])).
% 59.19/59.24 cnf(32,plain,
% 59.19/59.24 (~P2(a7,x321,a8)),
% 59.19/59.24 inference(scs_inference,[],[21,18,25,26])).
% 59.19/59.24 cnf(34,plain,
% 59.19/59.24 (~E(a5,a8)),
% 59.19/59.24 inference(scs_inference,[],[21,18,13,25,26,6])).
% 59.19/59.24 cnf(35,plain,
% 59.19/59.24 (P1(a5,x351)),
% 59.19/59.24 inference(rename_variables,[],[13])).
% 59.19/59.24 cnf(36,plain,
% 59.19/59.24 (~P1(a8,a5)),
% 59.19/59.24 inference(scs_inference,[],[21,18,13,35,25,26,6,22])).
% 59.19/59.24 cnf(39,plain,
% 59.19/59.24 (E(a5,f3(x391,x391))),
% 59.19/59.24 inference(scs_inference,[],[21,18,20,13,35,25,26,6,22,27])).
% 59.19/59.24 cnf(40,plain,
% 59.19/59.24 (P2(x401,x402,f3(x401,x402))),
% 59.19/59.24 inference(rename_variables,[],[20])).
% 59.19/59.24 cnf(42,plain,
% 59.19/59.24 (~E(a2,a7)),
% 59.19/59.24 inference(scs_inference,[],[21,18,20,12,13,35,25,26,6,22,27,7])).
% 59.19/59.24 cnf(44,plain,
% 59.19/59.24 (P2(f3(a5,a5),a5,a5)),
% 59.19/59.24 inference(scs_inference,[],[21,18,20,12,13,35,25,26,6,22,27,7,8])).
% 59.19/59.24 cnf(45,plain,
% 59.19/59.24 (P2(x451,x451,a5)),
% 59.19/59.24 inference(rename_variables,[],[18])).
% 59.19/59.24 cnf(46,plain,
% 59.19/59.24 (P2(x461,f3(a5,a5),x461)),
% 59.19/59.24 inference(scs_inference,[],[21,18,19,20,12,13,35,25,26,6,22,27,7,8,9])).
% 59.19/59.24 cnf(48,plain,
% 59.19/59.24 (P2(x481,a5,x481)),
% 59.19/59.24 inference(rename_variables,[],[19])).
% 59.19/59.24 cnf(49,plain,
% 59.19/59.24 (P1(f3(a1,a4),a5)),
% 59.19/59.24 inference(scs_inference,[],[21,18,19,48,20,40,12,13,35,11,25,26,6,22,27,7,8,9,10,28])).
% 59.19/59.24 cnf(51,plain,
% 59.19/59.24 (P2(x511,x512,f3(x511,x512))),
% 59.19/59.24 inference(rename_variables,[],[20])).
% 59.19/59.24 cnf(53,plain,
% 59.19/59.24 (P1(f3(a7,a7),a5)),
% 59.19/59.24 inference(scs_inference,[],[21,18,45,19,48,20,40,51,12,13,35,17,11,14,25,26,6,22,27,7,8,9,10,28,29])).
% 59.19/59.24 cnf(58,plain,
% 59.19/59.24 (E(f3(a5,a5),a5)),
% 59.19/59.24 inference(scs_inference,[],[21,18,45,19,48,20,40,51,12,13,35,17,11,14,25,26,6,22,27,7,8,9,10,28,29,2])).
% 59.19/59.24 cnf(59,plain,
% 59.19/59.24 (P1(f3(a5,a5),a5)),
% 59.19/59.24 inference(scs_inference,[],[44,25])).
% 59.19/59.24 cnf(61,plain,
% 59.19/59.24 (~P2(a5,x611,a8)),
% 59.19/59.24 inference(scs_inference,[],[44,36,25,26])).
% 59.19/59.24 cnf(63,plain,
% 59.19/59.24 (E(f3(x631,x631),a5)),
% 59.19/59.24 inference(scs_inference,[],[39,44,36,25,26,2])).
% 59.19/59.24 cnf(64,plain,
% 59.19/59.24 (E(f3(a5,a5),f3(x641,x641))),
% 59.19/59.24 inference(scs_inference,[],[58,39,44,36,25,26,2,3])).
% 59.19/59.24 cnf(65,plain,
% 59.19/59.24 (E(f3(a1,a4),a5)),
% 59.19/59.24 inference(scs_inference,[],[49,58,39,44,36,13,25,26,2,3,22])).
% 59.19/59.24 cnf(68,plain,
% 59.19/59.25 (~E(a8,a7)),
% 59.19/59.25 inference(scs_inference,[],[32,49,46,58,39,44,36,13,25,26,2,3,22,8])).
% 59.19/59.25 cnf(69,plain,
% 59.19/59.25 (P2(x691,f3(a5,a5),x691)),
% 59.19/59.25 inference(rename_variables,[],[46])).
% 59.19/59.25 cnf(71,plain,
% 59.19/59.25 (E(x711,f3(x711,f3(a5,a5)))),
% 59.19/59.25 inference(scs_inference,[],[32,49,46,69,58,39,44,36,20,13,25,26,2,3,22,8,27])).
% 59.19/59.25 cnf(72,plain,
% 59.19/59.25 (P2(x721,x722,f3(x721,x722))),
% 59.19/59.25 inference(rename_variables,[],[20])).
% 59.19/59.25 cnf(74,plain,
% 59.19/59.25 (P2(x741,f3(a2,f3(a5,a5)),a5)),
% 59.19/59.25 inference(scs_inference,[],[32,49,46,69,58,39,16,44,36,20,13,25,26,2,3,22,8,27,9])).
% 59.19/59.25 cnf(75,plain,
% 59.19/59.25 (~E(f3(a1,a4),a8)),
% 59.19/59.25 inference(scs_inference,[],[32,49,46,69,58,39,16,44,36,20,13,25,26,2,3,22,8,27,9,6])).
% 59.19/59.25 cnf(76,plain,
% 59.19/59.25 (P2(f3(a5,a5),a5,f3(x761,x761))),
% 59.19/59.25 inference(scs_inference,[],[32,49,46,69,58,39,16,44,36,20,13,25,26,2,3,22,8,27,9,6,10])).
% 59.19/59.25 cnf(78,plain,
% 59.19/59.25 (P1(f3(a5,a2),a5)),
% 59.19/59.25 inference(scs_inference,[],[32,49,46,69,58,39,16,44,36,20,72,13,17,19,25,26,2,3,22,8,27,9,6,10,7,29])).
% 59.19/59.25 cnf(81,plain,
% 59.19/59.25 (P2(x811,x812,f3(x811,x812))),
% 59.19/59.25 inference(rename_variables,[],[20])).
% 59.19/59.25 cnf(84,plain,
% 59.19/59.25 (~P2(a1,f3(x841,x841),x842)+P1(x842,a4)),
% 59.19/59.25 inference(scs_inference,[],[32,49,46,69,58,39,16,44,36,20,72,81,13,17,19,25,26,2,3,22,8,27,9,6,10,7,29,28])).
% 59.19/59.25 cnf(87,plain,
% 59.19/59.25 (P1(x871,f3(a2,f3(a5,a5)))),
% 59.19/59.25 inference(scs_inference,[],[74,25])).
% 59.19/59.25 cnf(89,plain,
% 59.19/59.25 (E(f3(x891,f3(a5,a5)),x891)),
% 59.19/59.25 inference(scs_inference,[],[71,74,25,2])).
% 59.19/59.25 cnf(90,plain,
% 59.19/59.25 (E(f3(a5,a5),f3(f3(x901,x901),f3(a5,a5)))),
% 59.19/59.25 inference(scs_inference,[],[71,64,74,25,2,3])).
% 59.19/59.25 cnf(91,plain,
% 59.19/59.25 (E(x911,f3(x911,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(92,plain,
% 59.19/59.25 (E(f3(x921,x921),f3(f3(a5,a5),a5))),
% 59.19/59.25 inference(scs_inference,[],[71,64,76,74,20,25,2,3,27])).
% 59.19/59.25 cnf(93,plain,
% 59.19/59.25 (P2(x931,x932,f3(x931,x932))),
% 59.19/59.25 inference(rename_variables,[],[20])).
% 59.19/59.25 cnf(95,plain,
% 59.19/59.25 (E(f3(a5,a2),a5)),
% 59.19/59.25 inference(scs_inference,[],[78,71,64,76,74,20,13,25,2,3,27,22])).
% 59.19/59.25 cnf(99,plain,
% 59.19/59.25 (E(x991,f3(x991,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(100,plain,
% 59.19/59.25 (P2(f3(f3(a5,a5),f3(a5,a5)),a5,f3(x1001,x1001))),
% 59.19/59.25 inference(scs_inference,[],[78,71,91,99,64,76,74,20,13,25,2,3,27,22,9,8])).
% 59.19/59.25 cnf(101,plain,
% 59.19/59.25 (E(x1011,f3(x1011,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(102,plain,
% 59.19/59.25 (~E(f3(a5,a5),a8)),
% 59.19/59.25 inference(scs_inference,[],[59,78,71,91,99,64,76,74,20,13,36,25,2,3,27,22,9,8,6])).
% 59.19/59.25 cnf(103,plain,
% 59.19/59.25 (P2(f3(a5,a5),a5,f3(f3(x1031,x1031),f3(a5,a5)))),
% 59.19/59.25 inference(scs_inference,[],[59,78,71,91,99,101,64,76,74,20,13,36,25,2,3,27,22,9,8,6,10])).
% 59.19/59.25 cnf(104,plain,
% 59.19/59.25 (E(x1041,f3(x1041,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(107,plain,
% 59.19/59.25 (P1(f3(f3(a5,a2),a5),f3(a5,a5))),
% 59.19/59.25 inference(scs_inference,[],[59,78,71,91,99,101,104,64,76,74,46,20,93,13,36,25,2,3,27,22,9,8,6,10,7,28])).
% 59.19/59.25 cnf(111,plain,
% 59.19/59.25 (E(f3(f3(x1111,x1111),f3(a5,a5)),f3(a5,a5))),
% 59.19/59.25 inference(scs_inference,[],[90,2])).
% 59.19/59.25 cnf(112,plain,
% 59.19/59.25 (E(f3(x1121,x1121),f3(f3(a5,a5),f3(a5,a5)))),
% 59.19/59.25 inference(scs_inference,[],[90,100,19,2,27])).
% 59.19/59.25 cnf(117,plain,
% 59.19/59.25 (~E(a6,a5)),
% 59.19/59.25 inference(scs_inference,[],[34,61,15,89,90,100,19,2,27,3,8])).
% 59.19/59.25 cnf(119,plain,
% 59.19/59.25 (P2(a6,f3(a4,f3(a5,a5)),a8)),
% 59.19/59.25 inference(scs_inference,[],[34,61,15,89,90,100,71,19,2,27,3,8,9])).
% 59.19/59.25 cnf(120,plain,
% 59.19/59.25 (E(x1201,f3(x1201,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(124,plain,
% 59.19/59.25 (~E(f3(a2,f3(a5,a5)),a7)),
% 59.19/59.25 inference(scs_inference,[],[21,87,34,61,53,15,89,90,100,71,120,19,36,2,27,3,8,9,6,10,7])).
% 59.19/59.25 cnf(126,plain,
% 59.19/59.25 (P1(f3(a6,a8),a4)),
% 59.19/59.25 inference(scs_inference,[],[21,30,87,34,61,53,15,89,90,100,71,120,19,20,36,2,27,3,8,9,6,10,7,28])).
% 59.19/59.25 cnf(128,plain,
% 59.19/59.25 (P2(x1281,x1282,f3(x1281,x1282))),
% 59.19/59.25 inference(rename_variables,[],[20])).
% 59.19/59.25 cnf(130,plain,
% 59.19/59.25 (P1(f3(a8,a8),a5)),
% 59.19/59.25 inference(scs_inference,[],[21,30,87,34,61,53,15,89,90,100,71,120,17,18,19,20,128,36,2,27,3,8,9,6,10,7,28,29])).
% 59.19/59.25 cnf(135,plain,
% 59.19/59.25 (E(f3(f3(a5,a2),a5),f3(a5,a5))+~P1(f3(a5,a5),f3(f3(a5,a2),a5))),
% 59.19/59.25 inference(scs_inference,[],[21,30,87,107,34,61,53,15,89,90,100,71,120,17,18,19,20,128,36,2,27,3,8,9,6,10,7,28,29,22])).
% 59.19/59.25 cnf(137,plain,
% 59.19/59.25 (E(f3(f3(a5,a5),f3(a5,a5)),f3(x1371,x1371))),
% 59.19/59.25 inference(scs_inference,[],[112,2])).
% 59.19/59.25 cnf(138,plain,
% 59.19/59.25 (E(a7,f3(a6,a1))),
% 59.19/59.25 inference(scs_inference,[],[14,112,20,2,27])).
% 59.19/59.25 cnf(139,plain,
% 59.19/59.25 (P2(x1391,x1392,f3(x1391,x1392))),
% 59.19/59.25 inference(rename_variables,[],[20])).
% 59.19/59.25 cnf(141,plain,
% 59.19/59.25 (E(f3(x1411,x1411),f3(a5,a5))),
% 59.19/59.25 inference(scs_inference,[],[14,111,112,20,2,27,3])).
% 59.19/59.25 cnf(143,plain,
% 59.19/59.25 (P2(f3(a6,f3(a5,a5)),a1,a7)),
% 59.19/59.25 inference(scs_inference,[],[14,111,112,71,20,2,27,3,8])).
% 59.19/59.25 cnf(144,plain,
% 59.19/59.25 (E(x1441,f3(x1441,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(146,plain,
% 59.19/59.25 (E(x1461,f3(x1461,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(147,plain,
% 59.19/59.25 (P2(a6,f3(a1,f3(a5,a5)),a7)),
% 59.19/59.25 inference(scs_inference,[],[14,111,112,71,144,146,20,2,27,3,8,10,9])).
% 59.19/59.25 cnf(148,plain,
% 59.19/59.25 (E(x1481,f3(x1481,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(149,plain,
% 59.19/59.25 (P1(f3(f3(a6,a8),f3(a5,a5)),a4)),
% 59.19/59.25 inference(scs_inference,[],[126,14,111,112,71,144,146,148,20,2,27,3,8,10,9,6])).
% 59.19/59.25 cnf(150,plain,
% 59.19/59.25 (E(x1501,f3(x1501,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(151,plain,
% 59.19/59.25 (P1(f3(a6,a8),f3(a4,f3(a5,a5)))),
% 59.19/59.25 inference(scs_inference,[],[126,14,111,112,71,144,146,148,150,20,2,27,3,8,10,9,6,7])).
% 59.19/59.25 cnf(153,plain,
% 59.19/59.25 (P1(f3(a6,a7),a1)),
% 59.19/59.25 inference(scs_inference,[],[30,126,14,111,112,71,144,146,148,150,20,139,2,27,3,8,10,9,6,7,28])).
% 59.19/59.25 cnf(155,plain,
% 59.19/59.25 (P2(x1551,x1552,f3(x1551,x1552))),
% 59.19/59.25 inference(rename_variables,[],[20])).
% 59.19/59.25 cnf(157,plain,
% 59.19/59.25 (P1(f3(a7,a5),a7)),
% 59.19/59.25 inference(scs_inference,[],[30,126,14,111,112,71,144,146,148,150,17,19,20,139,155,2,27,3,8,10,9,6,7,28,29])).
% 59.19/59.25 cnf(164,plain,
% 59.19/59.25 (E(f3(f3(a5,a5),a5),f3(x1641,x1641))),
% 59.19/59.25 inference(scs_inference,[],[92,2])).
% 59.19/59.25 cnf(166,plain,
% 59.19/59.25 (~E(a6,a7)),
% 59.19/59.25 inference(scs_inference,[],[32,15,92,95,117,2,3,8])).
% 59.19/59.25 cnf(170,plain,
% 59.19/59.25 (E(x1701,f3(x1701,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(171,plain,
% 59.19/59.25 (P2(f3(a5,a5),a5,f3(a5,f3(a5,a5)))),
% 59.19/59.25 inference(scs_inference,[],[130,32,44,36,15,92,95,117,71,170,2,3,8,6,7,10])).
% 59.19/59.25 cnf(172,plain,
% 59.19/59.25 (E(x1721,f3(x1721,f3(a5,a5)))),
% 59.19/59.25 inference(rename_variables,[],[71])).
% 59.19/59.25 cnf(175,plain,
% 59.19/59.25 (P1(f3(f3(a6,a7),a1),f3(a5,a5))),
% 59.19/59.25 inference(scs_inference,[],[130,153,32,44,36,15,92,95,117,46,71,170,172,20,2,3,8,6,7,10,9,28])).
% 59.19/59.25 cnf(181,plain,
% 59.19/59.25 (E(a5,f3(a1,a4))),
% 59.19/59.25 inference(scs_inference,[],[65,2])).
% 59.19/59.25 cnf(182,plain,
% 59.19/59.25 (~E(a6,f3(a1,a4))),
% 59.19/59.25 inference(scs_inference,[],[65,117,2,3])).
% 59.19/59.25 cnf(183,plain,
% 59.19/59.25 (P2(f3(x1831,x1831),x1832,a5)),
% 59.19/59.25 inference(scs_inference,[],[17,65,117,39,2,3,8])).
% 59.19/59.25 cnf(184,plain,
% 59.19/59.25 (~E(f3(a7,a5),a8)),
% 59.19/59.25 inference(scs_inference,[],[21,157,17,65,117,39,2,3,8,6])).
% 59.19/59.25 cnf(185,plain,
% 59.19/59.25 (P2(f3(f3(a5,a5),f3(a5,a5)),f3(x1851,x1851),f3(x1852,x1852))),
% 59.19/59.25 inference(scs_inference,[],[21,157,17,100,65,117,39,2,3,8,6,9])).
% 59.19/59.25 cnf(188,plain,
% 59.19/59.25 (P1(f3(f3(a6,a7),a1),a5)),
% 59.19/59.25 inference(scs_inference,[],[21,59,175,157,17,143,100,19,65,138,117,46,39,2,3,8,6,9,7,10,28])).
% 59.19/59.25 cnf(192,plain,
% 59.19/59.25 (P1(f3(f3(a6,a1),f3(a6,a1)),a5)),
% 59.19/59.25 inference(scs_inference,[],[21,59,175,157,17,143,100,18,19,65,138,117,46,39,20,2,3,8,6,9,7,10,28,29])).
% 59.19/59.25 cnf(199,plain,
% 59.19/59.25 (E(f3(f3(a6,a7),a1),f3(a5,a5))+~P1(f3(a5,a5),f3(f3(a6,a7),a1))),
% 59.19/59.25 inference(scs_inference,[],[21,59,175,157,17,143,100,18,19,65,138,117,46,39,20,2,3,8,6,9,7,10,28,29,25,22])).
% 59.19/59.25 cnf(201,plain,
% 59.19/59.25 (P1(f3(x2011,x2011),x2012)),
% 59.19/59.25 inference(scs_inference,[],[183,25])).
% 59.19/59.25 cnf(203,plain,
% 59.19/59.25 (E(a5,f3(a5,a2))),
% 59.19/59.25 inference(scs_inference,[],[183,95,25,2])).
% 59.19/59.25 cnf(204,plain,
% 59.19/59.25 (E(f3(f3(a6,a7),a1),a5)),
% 59.19/59.25 inference(scs_inference,[],[188,183,95,13,25,2,22])).
% 59.19/59.25 cnf(207,plain,
% 59.19/59.25 (P2(f3(a1,a4),x2071,a5)),
% 59.19/59.25 inference(scs_inference,[],[188,17,183,181,95,13,25,2,22,8])).
% 59.19/59.25 cnf(208,plain,
% 59.19/59.25 (~E(a6,f3(x2081,x2081))),
% 59.19/59.25 inference(scs_inference,[],[188,17,183,63,181,95,117,13,25,2,22,8,3])).
% 59.19/59.25 cnf(210,plain,
% 59.19/59.25 (P2(a6,f3(a1,f3(a5,a5)),f3(a6,a1))),
% 59.19/59.25 inference(scs_inference,[],[192,188,36,17,147,183,63,181,95,138,117,13,25,2,22,8,3,6,10])).
% 59.19/59.25 cnf(213,plain,
% 59.19/59.25 (P1(f3(f3(a5,a2),a5),a5)),
% 59.19/59.25 inference(scs_inference,[],[192,188,107,36,17,147,100,19,183,63,181,95,138,117,13,46,25,2,22,8,3,6,10,9,7,28])).
% 59.19/59.25 cnf(217,plain,
% 59.19/59.25 (E(f3(f3(a5,a2),a5),f3(a5,a5))),
% 59.19/59.25 inference(scs_inference,[],[201,135])).
% 59.19/59.25 cnf(218,plain,
% 59.19/59.25 (E(f3(f3(a6,a7),a1),f3(a5,a5))),
% 59.19/59.25 inference(scs_inference,[],[201,199])).
% 59.19/59.25 cnf(219,plain,
% 59.19/59.25 (P1(f3(a1,a4),x2191)),
% 59.19/59.25 inference(scs_inference,[],[207,25])).
% 59.19/59.25 cnf(221,plain,
% 59.19/59.25 (E(a5,f3(f3(a6,a7),a1))),
% 59.19/59.25 inference(scs_inference,[],[207,204,25,2])).
% 59.19/59.25 cnf(223,plain,
% 59.19/59.25 (P1(f3(x2231,x2231),x2232)),
% 59.19/59.25 inference(rename_variables,[],[201])).
% 59.19/59.25 cnf(225,plain,
% 59.19/59.25 (P2(f3(a5,a2),x2251,a5)),
% 59.19/59.25 inference(scs_inference,[],[201,102,17,207,203,204,25,2,22,8])).
% 59.19/59.25 cnf(228,plain,
% 59.19/59.25 (~E(f3(x2281,x2281),a8)),
% 59.19/59.25 inference(scs_inference,[],[21,201,223,102,17,164,207,208,203,204,25,2,22,8,3,6])).
% 59.19/59.25 cnf(230,plain,
% 59.19/59.25 (P2(f3(a1,a4),x2301,f3(a5,a2))),
% 59.19/59.25 inference(scs_inference,[],[21,201,223,102,17,164,207,208,203,204,25,2,22,8,3,6,10])).
% 59.19/59.25 cnf(233,plain,
% 59.19/59.25 (P1(f3(f3(a7,a5),a7),a5)),
% 59.19/59.25 inference(scs_inference,[],[21,201,223,102,213,157,17,100,19,164,207,208,203,204,20,25,2,22,8,3,6,10,9,7,28])).
% 59.19/59.25 cnf(235,plain,
% 59.19/59.25 (P2(x2351,x2352,f3(x2351,x2352))),
% 59.19/59.25 inference(rename_variables,[],[20])).
% 59.19/59.25 cnf(237,plain,
% 59.19/59.25 (P1(f3(a5,f3(a5,a2)),a5)),
% 59.19/59.25 inference(scs_inference,[],[21,201,223,102,213,157,74,17,100,19,164,207,208,203,204,20,235,25,2,22,8,3,6,10,9,7,28,29])).
% 59.19/59.25 cnf(243,plain,
% 59.19/59.25 (~P2(f3(a5,a5),x2431,a8)),
% 59.19/59.25 inference(scs_inference,[],[21,201,223,102,213,157,74,17,100,19,164,207,208,203,204,20,235,25,2,22,8,3,6,10,9,7,28,29,26])).
% 59.19/59.25 cnf(245,plain,
% 59.19/59.25 (P1(f3(a5,a2),x2451)),
% 59.19/59.25 inference(scs_inference,[],[225,25])).
% 59.19/59.25 cnf(248,plain,
% 59.19/59.25 (E(a5,f3(x2481,a2))),
% 59.19/59.25 inference(scs_inference,[],[16,217,225,20,25,2,27])).
% 59.19/59.25 cnf(249,plain,
% 59.19/59.25 (P2(x2491,x2492,f3(x2491,x2492))),
% 59.19/59.25 inference(rename_variables,[],[20])).
% 59.19/59.25 cnf(254,plain,
% 59.19/59.25 (P2(f3(f3(a6,a7),a1),x2541,a5)),
% 59.19/59.25 inference(scs_inference,[],[219,75,16,17,217,225,221,20,25,2,27,22,8])).
% 59.19/59.25 cnf(255,plain,
% 59.19/59.25 (~E(f3(a5,f3(a5,a5)),a8)),
% 59.19/59.25 inference(scs_inference,[],[219,243,75,16,17,217,171,225,221,20,25,2,27,22,8,10])).
% 59.19/59.25 cnf(260,plain,
% 59.19/59.25 (~E(f3(a5,f3(a5,a2)),a8)),
% 59.19/59.25 inference(scs_inference,[],[219,243,237,75,16,36,17,76,217,171,225,221,208,20,25,2,27,22,8,10,3,9,6])).
% 59.19/59.25 cnf(261,plain,
% 59.19/59.25 (P1(f3(a6,a7),f3(a1,f3(a5,a5)))),
% 59.19/59.25 inference(scs_inference,[],[219,243,237,75,153,16,36,17,76,217,171,225,221,208,71,20,25,2,27,22,8,10,3,9,6,7])).
% 59.19/59.25 cnf(263,plain,
% 59.19/59.25 (P1(f3(f3(a6,a8),a4),a5)),
% 59.19/59.25 inference(scs_inference,[],[219,243,237,75,153,126,16,36,17,76,19,217,171,225,221,208,71,20,249,25,2,27,22,8,10,3,9,6,7,28])).
% 59.19/59.25 cnf(267,plain,
% 59.19/59.25 (~P2(f3(a1,a4),x2671,a8)),
% 59.19/59.25 inference(scs_inference,[],[219,243,237,75,153,126,16,36,17,76,19,217,171,225,221,208,71,20,249,25,2,27,22,8,10,3,9,6,7,28,26])).
% 59.19/59.25 cnf(269,plain,
% 59.19/59.25 (P1(f3(f3(a6,a7),a1),x2691)),
% 59.19/59.25 inference(scs_inference,[],[254,25])).
% 59.19/59.25 cnf(271,plain,
% 59.19/59.25 (E(f3(a5,a5),f3(f3(a6,a7),a1))),
% 59.19/59.25 inference(scs_inference,[],[218,254,25,2])).
% 59.19/59.25 cnf(272,plain,
% 59.19/59.25 (~P1(a8,f3(x2721,x2721))),
% 59.19/59.25 inference(scs_inference,[],[201,228,218,254,25,2,22])).
% 59.19/59.25 cnf(275,plain,
% 59.19/59.25 (P2(f3(x2751,a2),x2752,a5)),
% 59.19/59.25 inference(scs_inference,[],[201,228,17,218,254,248,25,2,22,8])).
% 59.19/59.25 cnf(278,plain,
% 59.19/59.25 (P2(f3(f3(a5,a5),f3(a5,a5)),f3(x2781,a2),f3(x2782,x2782))),
% 59.19/59.25 inference(scs_inference,[],[201,228,17,100,218,254,248,208,25,2,22,8,3,9])).
% 59.19/59.26 cnf(279,plain,
% 59.19/59.26 (~E(f3(a5,a2),a8)),
% 59.19/59.26 inference(scs_inference,[],[201,267,228,17,100,230,218,254,248,208,25,2,22,8,3,9,10])).
% 59.19/59.26 cnf(281,plain,
% 59.19/59.26 (~E(f3(f3(a7,a5),a7),a8)),
% 59.19/59.26 inference(scs_inference,[],[201,233,267,228,36,17,100,230,218,254,248,208,25,2,22,8,3,9,10,6])).
% 59.19/59.26 cnf(282,plain,
% 59.19/59.26 (P1(f3(f3(a7,a5),a7),f3(x2821,a2))),
% 59.19/59.26 inference(scs_inference,[],[201,233,267,228,36,17,100,230,218,254,248,208,25,2,22,8,3,9,10,6,7])).
% 59.19/59.26 cnf(283,plain,
% 59.19/59.26 (~P2(f3(x2831,x2831),x2832,a8)),
% 59.19/59.26 inference(scs_inference,[],[201,233,267,228,36,17,100,230,218,254,248,208,25,2,22,8,3,9,10,6,7,26])).
% 59.19/59.26 cnf(285,plain,
% 59.19/59.26 (P1(f3(x2851,a2),x2852)),
% 59.19/59.26 inference(scs_inference,[],[275,25])).
% 59.19/59.26 cnf(287,plain,
% 59.19/59.26 (E(f3(a6,a1),a7)),
% 59.19/59.26 inference(scs_inference,[],[275,138,25,2])).
% 59.19/59.26 cnf(291,plain,
% 59.19/59.26 (~E(a8,f3(x2911,x2911))),
% 59.19/59.26 inference(scs_inference,[],[245,283,19,279,275,138,25,2,22,8])).
% 59.19/59.26 cnf(292,plain,
% 59.19/59.26 (P2(x2921,a5,x2921)),
% 59.19/59.26 inference(rename_variables,[],[19])).
% 59.19/59.26 cnf(293,plain,
% 59.19/59.26 (~P2(f3(x2931,x2931),x2932,a8)),
% 59.19/59.26 inference(rename_variables,[],[283])).
% 59.19/59.26 cnf(299,plain,
% 59.19/59.26 (~E(f3(f3(a6,a7),a1),a8)),
% 59.19/59.26 inference(scs_inference,[],[21,245,269,283,293,19,292,279,103,275,111,221,138,208,25,2,22,8,10,3,9,6])).
% 59.19/59.26 cnf(301,plain,
% 59.19/59.26 (P1(f3(a7,a5),f3(a6,a1))),
% 59.19/59.26 inference(scs_inference,[],[21,245,269,283,293,157,19,292,279,103,275,111,221,138,208,25,2,22,8,10,3,9,6,7])).
% 59.19/59.26 cnf(302,plain,
% 59.19/59.26 (P1(f3(f3(a7,a5),f3(a6,a1)),a5)),
% 59.19/59.26 inference(scs_inference,[],[21,245,269,283,293,157,19,292,279,103,275,111,221,138,208,20,25,2,22,8,10,3,9,6,7,28])).
% 59.19/59.26 cnf(306,plain,
% 59.19/59.26 (~P2(f3(a5,a2),x3061,a8)),
% 59.19/59.26 inference(scs_inference,[],[21,245,269,283,293,157,19,292,279,103,275,111,221,138,208,20,25,2,22,8,10,3,9,6,7,28,26])).
% 59.19/59.26 cnf(308,plain,
% 59.19/59.26 (E(f3(x3081,a2),a5)),
% 59.19/59.26 inference(scs_inference,[],[248,2])).
% 59.19/59.26 cnf(315,plain,
% 59.19/59.26 (P2(f3(f3(a6,a7),a1),x3151,f3(a1,a4))),
% 59.19/59.26 inference(scs_inference,[],[269,306,299,19,254,181,248,2,22,8,10])).
% 59.19/59.26 cnf(318,plain,
% 59.19/59.26 (~E(f3(x3181,a2),a8)),
% 59.19/59.26 inference(scs_inference,[],[21,285,269,306,299,76,19,68,287,254,181,248,2,22,8,10,9,3,6])).
% 59.19/59.26 cnf(321,plain,
% 59.19/59.26 (P1(f3(a5,f3(a1,a4)),a5)),
% 59.19/59.26 inference(scs_inference,[],[21,285,269,263,306,299,74,17,76,19,68,287,254,181,248,20,2,22,8,10,9,3,6,7,29])).
% 59.19/59.26 cnf(327,plain,
% 59.19/59.26 (~P2(f3(f3(a6,a7),a1),x3271,a8)),
% 59.19/59.26 inference(scs_inference,[],[21,285,269,263,306,299,74,17,76,19,68,287,254,181,248,20,2,22,8,10,9,3,6,7,29,26])).
% 59.19/59.26 cnf(335,plain,
% 59.19/59.26 (~E(f3(f3(a7,a5),f3(a6,a1)),a8)),
% 59.19/59.26 inference(scs_inference,[],[285,302,327,318,36,19,22,8,6])).
% 59.19/59.26 cnf(336,plain,
% 59.19/59.26 (P2(x3361,f3(a5,a5),f3(x3361,f3(x3362,x3362)))),
% 59.19/59.26 inference(scs_inference,[],[285,302,327,318,36,19,141,20,22,8,6,9])).
% 59.19/59.26 cnf(342,plain,
% 59.19/59.26 (~P2(f3(x3421,a2),x3422,a8)),
% 59.19/59.26 inference(scs_inference,[],[285,302,327,318,36,19,141,282,308,117,20,22,8,6,9,3,7,26])).
% 59.19/59.26 cnf(344,plain,
% 59.19/59.26 (E(a5,f3(a5,f3(a2,a2)))),
% 59.19/59.26 inference(scs_inference,[],[285,302,327,318,36,17,19,141,282,308,117,20,22,8,6,9,3,7,26,27])).
% 59.19/59.26 cnf(347,plain,
% 59.19/59.26 (~E(f3(a5,f3(a2,a2)),a8)),
% 59.19/59.26 inference(scs_inference,[],[285,302,327,318,61,36,17,19,141,282,308,117,20,22,8,6,9,3,7,26,27,10])).
% 59.19/59.26 cnf(349,plain,
% 59.19/59.26 (E(f3(a5,f3(a2,a2)),a5)),
% 59.19/59.26 inference(scs_inference,[],[285,302,327,318,61,36,17,19,141,282,308,117,20,22,8,6,9,3,7,26,27,10,2])).
% 59.19/59.26 cnf(350,plain,
% 59.19/59.26 (P2(f3(a1,f3(x3501,x3501)),a4,a5)),
% 59.19/59.26 inference(scs_inference,[],[336,24,84])).
% 59.19/59.26 cnf(351,plain,
% 59.19/59.26 (P1(f3(a1,f3(x3511,x3511)),a4)),
% 59.19/59.26 inference(scs_inference,[],[350,25])).
% 59.19/59.26 cnf(353,plain,
% 59.19/59.26 (E(a5,f3(a5,f3(x3531,x3531)))),
% 59.19/59.26 inference(scs_inference,[],[17,350,336,25,27])).
% 59.19/59.26 cnf(354,plain,
% 59.19/59.26 (P2(x3541,f3(a5,a5),f3(x3541,f3(x3542,x3542)))),
% 59.19/59.26 inference(rename_variables,[],[336])).
% 59.19/59.26 cnf(355,plain,
% 59.19/59.26 (P2(a5,x3551,a5)),
% 59.19/59.26 inference(rename_variables,[],[17])).
% 59.19/59.26 cnf(357,plain,
% 59.19/59.26 (E(f3(a5,f3(a1,a4)),a5)),
% 59.19/59.26 inference(scs_inference,[],[321,17,350,336,13,25,27,22])).
% 59.19/59.26 cnf(360,plain,
% 59.19/59.26 (P2(f3(a5,f3(a2,a2)),x3601,a5)),
% 59.19/59.26 inference(scs_inference,[],[321,17,355,344,350,336,13,25,27,22,8])).
% 59.19/59.26 cnf(361,plain,
% 59.19/59.26 (~E(f3(a5,f3(a1,a4)),a8)),
% 59.19/59.26 inference(scs_inference,[],[321,36,17,355,344,350,336,13,25,27,22,8,6])).
% 59.19/59.26 cnf(363,plain,
% 59.19/59.26 (~E(f3(f3(x3631,a2),f3(x3632,x3632)),a8)),
% 59.19/59.26 inference(scs_inference,[],[321,342,36,17,355,76,344,350,336,354,13,25,27,22,8,6,9,10])).
% 59.19/59.26 cnf(367,plain,
% 59.19/59.26 (P1(a1,f3(a4,f3(a5,a5)))),
% 59.19/59.26 inference(scs_inference,[],[321,342,36,17,355,76,349,344,350,336,354,11,117,13,71,25,27,22,8,6,9,10,3,7])).
% 59.19/59.26 cnf(369,plain,
% 59.19/59.26 (E(f3(a5,f3(x3691,x3691)),a5)),
% 59.19/59.26 inference(scs_inference,[],[321,342,36,17,355,76,349,344,350,336,354,11,117,13,71,25,27,22,8,6,9,10,3,7,2])).
% 59.19/59.26 cnf(370,plain,
% 59.19/59.26 (P1(f3(a5,f3(a2,a2)),x3701)),
% 59.19/59.26 inference(scs_inference,[],[360,25])).
% 59.19/59.26 cnf(372,plain,
% 59.19/59.26 (E(a5,f3(a5,f3(a1,a4)))),
% 59.19/59.26 inference(scs_inference,[],[360,357,25,2])).
% 59.19/59.26 cnf(373,plain,
% 59.19/59.26 (E(f3(a5,f3(a5,a2)),a5)),
% 59.19/59.26 inference(scs_inference,[],[237,360,357,13,25,2,22])).
% 59.19/59.26 cnf(376,plain,
% 59.19/59.26 (P2(f3(a5,f3(x3761,x3761)),x3762,a5)),
% 59.19/59.26 inference(scs_inference,[],[237,17,360,357,353,13,25,2,22,8])).
% 59.19/59.26 cnf(380,plain,
% 59.19/59.26 (~E(f3(f3(a6,a8),a4),a8)),
% 59.19/59.26 inference(scs_inference,[],[237,263,283,36,17,360,357,353,336,13,25,2,22,8,10,6])).
% 59.19/59.26 cnf(383,plain,
% 59.19/59.26 (P1(f3(a5,f3(x3831,x3831)),x3832)),
% 59.19/59.26 inference(scs_inference,[],[376,25])).
% 59.19/59.26 cnf(385,plain,
% 59.19/59.26 (E(a5,f3(a5,f3(a5,a2)))),
% 59.19/59.26 inference(scs_inference,[],[376,373,25,2])).
% 59.19/59.26 cnf(389,plain,
% 59.19/59.26 (P2(f3(a5,f3(a1,a4)),x3891,a5)),
% 59.19/59.26 inference(scs_inference,[],[370,17,376,373,372,347,25,2,22,8])).
% 59.19/59.26 cnf(392,plain,
% 59.19/59.26 (~E(f3(f3(a5,a2),a5),a8)),
% 59.19/59.26 inference(scs_inference,[],[370,213,36,17,76,376,373,372,347,117,25,2,22,8,9,3,6])).
% 59.19/59.26 cnf(395,plain,
% 59.19/59.26 (P1(f3(a5,f3(a1,a4)),x3951)),
% 59.19/59.26 inference(scs_inference,[],[389,25])).
% 59.19/59.26 cnf(398,plain,
% 59.19/59.26 (P1(f3(a5,f3(x3981,x3981)),x3982)),
% 59.19/59.26 inference(rename_variables,[],[383])).
% 59.19/59.26 cnf(400,plain,
% 59.19/59.26 (P2(f3(a5,f3(a5,a2)),x4001,a5)),
% 59.19/59.26 inference(scs_inference,[],[383,17,255,389,385,25,22,8])).
% 59.19/59.26 cnf(401,plain,
% 59.19/59.26 (~E(f3(a5,f3(x4011,x4011)),a8)),
% 59.19/59.26 inference(scs_inference,[],[21,383,398,17,255,389,385,25,22,8,6])).
% 59.19/59.26 cnf(404,plain,
% 59.19/59.26 (~E(a6,f3(a5,f3(x4041,x4041)))),
% 59.19/59.26 inference(scs_inference,[],[21,383,398,17,76,255,389,385,369,117,25,22,8,6,9,3])).
% 59.19/59.26 cnf(405,plain,
% 59.19/59.26 (~P2(f3(a5,f3(a5,a5)),x4051,a8)),
% 59.19/59.26 inference(scs_inference,[],[21,383,398,17,76,255,389,385,369,117,25,22,8,6,9,3,26])).
% 59.19/59.26 cnf(407,plain,
% 59.19/59.26 (P1(f3(a5,f3(a5,a2)),x4071)),
% 59.19/59.26 inference(scs_inference,[],[400,25])).
% 59.19/59.26 cnf(412,plain,
% 59.19/59.26 (P2(f3(x4121,x4121),a5,f3(x4122,x4122))),
% 59.19/59.26 inference(scs_inference,[],[395,361,100,137,400,25,22,8])).
% 59.19/59.26 cnf(413,plain,
% 59.19/59.26 (P1(f3(f3(a6,a7),f3(a5,a5)),a1)),
% 59.19/59.26 inference(scs_inference,[],[395,361,153,100,137,400,71,25,22,8,6])).
% 59.19/59.26 cnf(417,plain,
% 59.19/59.26 (~P2(f3(a5,f3(a1,a4)),x4171,a8)),
% 59.19/59.26 inference(scs_inference,[],[395,361,153,100,19,124,137,400,287,385,71,25,22,8,6,9,3,26])).
% 59.19/59.26 cnf(422,plain,
% 59.19/59.26 (~E(a8,f3(a5,f3(a5,a5)))),
% 59.19/59.26 inference(scs_inference,[],[407,260,405,19,22,8])).
% 59.19/59.26 cnf(423,plain,
% 59.19/59.26 (P2(x4231,a5,x4231)),
% 59.19/59.26 inference(rename_variables,[],[19])).
% 59.19/59.26 cnf(425,plain,
% 59.19/59.26 (P1(f3(f3(a7,a5),f3(a5,a5)),f3(a6,a1))),
% 59.19/59.26 inference(scs_inference,[],[407,260,405,19,301,71,22,8,6])).
% 59.19/59.26 cnf(430,plain,
% 59.19/59.26 (~P2(f3(a5,f3(a5,a2)),x4301,a8)),
% 59.19/59.26 inference(scs_inference,[],[407,260,405,19,423,301,291,164,372,71,22,8,6,9,3,26])).
% 59.19/59.26 cnf(432,plain,
% 59.19/59.26 (P1(f3(f3(a7,a5),f3(a5,a5)),a7)),
% 59.19/59.26 inference(scs_inference,[],[407,260,405,19,423,301,291,164,287,372,71,22,8,6,9,3,26,7])).
% 59.19/59.26 cnf(437,plain,
% 59.19/59.26 (P2(x4371,a5,x4371)),
% 59.19/59.26 inference(rename_variables,[],[19])).
% 59.19/59.26 cnf(439,plain,
% 59.19/59.26 (~E(f3(f3(a7,a5),f3(a5,a5)),a8)),
% 59.19/59.26 inference(scs_inference,[],[21,383,430,401,19,432,22,8,6])).
% 59.19/59.26 cnf(440,plain,
% 59.19/59.26 (P2(x4401,f3(a5,f3(x4402,x4402)),x4401)),
% 59.19/59.26 inference(scs_inference,[],[21,383,430,401,19,437,432,353,22,8,6,9])).
% 59.19/59.26 cnf(445,plain,
% 59.19/59.26 (E(f3(f3(a7,a5),f3(a6,a1)),a5)),
% 59.19/59.26 inference(scs_inference,[],[302,13,22])).
% 59.19/59.26 cnf(454,plain,
% 59.19/59.26 (E(a5,f3(f3(a7,a5),f3(a6,a1)))),
% 59.19/59.26 inference(scs_inference,[],[417,302,19,412,217,291,221,13,22,8,9,3,2])).
% 59.19/59.26 cnf(455,plain,
% 59.19/59.26 (E(f3(f3(a6,a8),a4),a5)),
% 59.19/59.26 inference(scs_inference,[],[263,13,22])).
% 59.19/59.26 cnf(458,plain,
% 59.19/59.26 (P2(f3(f3(a7,a5),f3(a6,a1)),x4581,a5)),
% 59.19/59.26 inference(scs_inference,[],[263,17,454,13,22,8])).
% 59.19/59.26 cnf(460,plain,
% 59.19/59.26 (~E(a6,f3(f3(a7,a5),f3(a6,a1)))),
% 59.19/59.26 inference(scs_inference,[],[263,17,19,454,445,13,117,22,8,9,3])).
% 59.19/59.26 cnf(461,plain,
% 59.19/59.26 (P1(f3(f3(a7,a5),f3(a6,a1)),x4611)),
% 59.19/59.26 inference(scs_inference,[],[263,17,19,454,445,13,117,22,8,9,3,25])).
% 59.19/59.26 cnf(463,plain,
% 59.19/59.26 (E(a5,f3(f3(a6,a8),a4))),
% 59.19/59.26 inference(scs_inference,[],[263,17,19,454,445,13,117,22,8,9,3,25,2])).
% 59.19/59.26 cnf(467,plain,
% 59.19/59.26 (P2(f3(f3(a6,a8),a4),x4671,a5)),
% 59.19/59.26 inference(scs_inference,[],[461,335,17,463,22,8])).
% 59.19/59.26 cnf(470,plain,
% 59.19/59.26 (~P2(f3(f3(a7,a5),f3(a6,a1)),x4701,a8)),
% 59.19/59.26 inference(scs_inference,[],[461,335,17,19,463,455,117,22,8,9,3,26])).
% 59.19/59.26 cnf(472,plain,
% 59.19/59.26 (P1(f3(f3(a6,a8),a4),x4721)),
% 59.19/59.26 inference(scs_inference,[],[461,335,17,19,463,455,117,22,8,9,3,26,25])).
% 59.19/59.26 cnf(480,plain,
% 59.19/59.26 (P2(f3(x4801,x4801),f3(f3(a7,a5),f3(a6,a1)),f3(x4802,x4802))),
% 59.19/59.26 inference(scs_inference,[],[472,380,470,19,412,454,22,8,9])).
% 59.19/59.26 cnf(481,plain,
% 59.19/59.26 (~E(a2,f3(a6,a1))),
% 59.19/59.26 inference(scs_inference,[],[472,380,470,19,42,412,454,287,22,8,9,3])).
% 59.19/59.26 cnf(482,plain,
% 59.19/59.26 (~P2(f3(f3(a6,a8),a4),x4821,a8)),
% 59.19/59.26 inference(scs_inference,[],[472,380,470,19,42,412,454,287,22,8,9,3,26])).
% 59.19/59.26 cnf(484,plain,
% 59.19/59.26 (E(f3(f3(a7,a5),a7),a5)),
% 59.19/59.26 inference(scs_inference,[],[233,13,22])).
% 59.19/59.26 cnf(491,plain,
% 59.19/59.26 (~E(a8,a5)),
% 59.19/59.26 inference(scs_inference,[],[482,233,19,422,463,412,353,13,22,9,8,3])).
% 59.19/59.26 cnf(493,plain,
% 59.19/59.26 (E(a5,f3(f3(a7,a5),a7))),
% 59.19/59.26 inference(scs_inference,[],[482,233,19,422,463,412,353,13,22,9,8,3,2])).
% 59.19/59.26 cnf(494,plain,
% 59.19/59.26 (E(f3(f3(a5,a2),a5),a5)),
% 59.19/59.26 inference(scs_inference,[],[213,13,22])).
% 59.19/59.26 cnf(497,plain,
% 59.19/59.26 (P2(f3(f3(a7,a5),a7),x4971,a5)),
% 59.19/59.26 inference(scs_inference,[],[213,17,493,13,22,8])).
% 59.19/59.26 cnf(500,plain,
% 59.19/59.26 (P1(f3(f3(a7,a5),a7),x5001)),
% 59.19/59.26 inference(scs_inference,[],[213,17,19,493,484,491,13,22,8,9,3,25])).
% 59.19/59.26 cnf(502,plain,
% 59.19/59.26 (E(a5,f3(f3(a5,a2),a5))),
% 59.19/59.26 inference(scs_inference,[],[213,17,19,493,484,491,13,22,8,9,3,25,2])).
% 59.19/59.26 cnf(506,plain,
% 59.19/59.26 (P2(x5061,f3(f3(a5,a2),a5),x5061)),
% 59.19/59.26 inference(scs_inference,[],[500,281,19,502,22,9])).
% 59.19/59.26 cnf(507,plain,
% 59.19/59.26 (P2(f3(f3(a5,a2),a5),x5071,a5)),
% 59.19/59.26 inference(scs_inference,[],[500,281,17,19,502,22,9,8])).
% 59.19/59.26 cnf(509,plain,
% 59.19/59.26 (~P2(f3(f3(a7,a5),a7),x5091,a8)),
% 59.19/59.26 inference(scs_inference,[],[500,281,17,19,502,308,491,22,9,8,3,26])).
% 59.19/59.26 cnf(511,plain,
% 59.19/59.26 (P1(f3(f3(a5,a2),a5),x5111)),
% 59.19/59.26 inference(scs_inference,[],[500,281,17,19,502,308,491,22,9,8,3,26,25])).
% 59.19/59.26 cnf(519,plain,
% 59.19/59.26 (P2(f3(x5191,x5191),f3(f3(a7,a5),a7),f3(x5192,x5192))),
% 59.19/59.26 inference(scs_inference,[],[511,392,509,15,369,493,491,412,22,8,3,9])).
% 59.19/59.26 cnf(527,plain,
% 59.19/59.26 (E(f3(a1,f3(x5271,x5271)),a4)+~P1(a4,f3(a1,f3(x5271,x5271)))),
% 59.19/59.26 inference(scs_inference,[],[351,184,185,137,89,502,412,3,9,8,22])).
% 59.19/59.26 cnf(529,plain,
% 59.19/59.26 (E(a4,f3(a1,f3(x5291,x5291)))+~P1(a4,f3(a1,f3(x5291,x5291)))),
% 59.19/59.26 inference(scs_inference,[],[351,184,185,137,89,502,412,3,9,8,22,2])).
% 59.19/59.26 cnf(531,plain,
% 59.19/59.26 (P2(a5,x5311,f3(a1,a4))),
% 59.19/59.26 inference(scs_inference,[],[315,204,8])).
% 59.19/59.26 cnf(532,plain,
% 59.19/59.26 (~E(a8,f3(a1,a4))),
% 59.19/59.26 inference(scs_inference,[],[315,204,65,491,8,3])).
% 59.19/59.26 cnf(545,plain,
% 59.19/59.26 (P2(f3(f3(a5,a5),a5),x5451,a5)),
% 59.19/59.26 inference(scs_inference,[],[275,92,8])).
% 59.19/59.26 cnf(548,plain,
% 59.19/59.26 (P1(f3(f3(a5,a5),a5),x5481)),
% 59.19/59.26 inference(scs_inference,[],[275,92,8,25])).
% 59.19/59.26 cnf(552,plain,
% 59.19/59.26 (~E(f3(f3(a5,a5),a5),a8)),
% 59.19/59.26 inference(scs_inference,[],[21,425,275,92,8,25,22,6])).
% 59.19/59.26 cnf(559,plain,
% 59.19/59.26 (P2(x5591,a5,f3(x5591,f3(x5592,x5592)))),
% 59.19/59.26 inference(scs_inference,[],[548,552,336,63,22,9])).
% 59.19/59.26 cnf(560,plain,
% 59.19/59.26 (E(f3(x5601,x5601),a5)),
% 59.19/59.26 inference(rename_variables,[],[63])).
% 59.19/59.26 cnf(561,plain,
% 59.19/59.26 (P2(a5,f3(f3(a7,a5),a7),f3(x5611,x5611))),
% 59.19/59.26 inference(scs_inference,[],[548,552,519,336,63,560,22,9,8])).
% 59.19/59.26 cnf(565,plain,
% 59.19/59.26 (P2(a5,a5,f3(x5651,x5651))),
% 59.19/59.26 inference(scs_inference,[],[484,561,9])).
% 59.19/59.26 cnf(566,plain,
% 59.19/59.26 (P2(f3(a5,a5),f3(x5661,a2),f3(x5662,x5662))),
% 59.19/59.26 inference(scs_inference,[],[278,484,141,561,9,8])).
% 59.19/59.26 cnf(577,plain,
% 59.19/59.26 (E(a1,a4)+~P1(a4,a1)),
% 59.19/59.26 inference(scs_inference,[],[11,46,531,112,454,9,8,22])).
% 59.19/59.26 cnf(581,plain,
% 59.19/59.26 (E(a4,a1)+~P1(a4,a1)),
% 59.19/59.26 inference(scs_inference,[],[11,46,531,112,454,89,9,8,22,3,2])).
% 59.19/59.26 cnf(586,plain,
% 59.19/59.26 (E(f3(a7,a5),f3(a6,a1))+~P1(f3(a6,a1),f3(a7,a5))),
% 59.19/59.26 inference(scs_inference,[],[301,480,63,463,565,9,8,22])).
% 59.19/59.26 cnf(608,plain,
% 59.19/59.26 (E(x6081,f3(x6081,f3(a5,a5)))),
% 59.19/59.26 inference(rename_variables,[],[71])).
% 59.19/59.26 cnf(609,plain,
% 59.19/59.26 (P2(f3(f3(x6091,a2),f3(a5,a5)),x6092,a5)),
% 59.19/59.26 inference(scs_inference,[],[275,71,608,566,9,8])).
% 59.19/59.26 cnf(611,plain,
% 59.19/59.26 (P1(f3(f3(x6111,a2),f3(a5,a5)),x6112)),
% 59.19/59.26 inference(scs_inference,[],[275,71,608,566,9,8,25])).
% 59.19/59.26 cnf(632,plain,
% 59.19/59.26 (~P2(f3(f3(x6321,a2),f3(a5,a5)),x6322,a8)),
% 59.19/59.26 inference(scs_inference,[],[611,531,502,565,363,22,9,8,26])).
% 59.19/59.26 cnf(637,plain,
% 59.19/59.26 (E(a1,f3(a4,f3(a5,a5)))+~P1(f3(a4,f3(a5,a5)),a1)),
% 59.19/59.26 inference(scs_inference,[],[632,440,367,8,22])).
% 59.19/59.26 cnf(640,plain,
% 59.19/59.26 (E(a4,a1)+~P1(f3(a4,f3(a5,a5)),a1)),
% 59.19/59.26 inference(scs_inference,[],[632,440,71,367,8,22,2,3])).
% 59.19/59.26 cnf(644,plain,
% 59.19/59.26 (E(a1,a4)+~P2(a4,a1,a5)),
% 59.19/59.26 inference(scs_inference,[],[577,25])).
% 59.19/59.26 cnf(653,plain,
% 59.19/59.26 (P2(f3(a1,f3(x6531,x6531)),a4,f3(x6532,a2))),
% 59.19/59.26 inference(scs_inference,[],[350,248,10])).
% 59.19/59.26 cnf(654,plain,
% 59.19/59.26 (P2(x6541,f3(x6542,a2),x6541)),
% 59.19/59.26 inference(scs_inference,[],[19,350,248,10,9])).
% 59.19/59.26 cnf(669,plain,
% 59.19/59.26 (P2(x6691,f3(a1,a4),x6691)),
% 59.19/59.26 inference(scs_inference,[],[19,350,181,10,9])).
% 59.19/59.26 cnf(670,plain,
% 59.19/59.26 (P2(f3(a1,a4),x6701,f3(a1,a4))),
% 59.19/59.26 inference(scs_inference,[],[531,19,350,181,10,9,8])).
% 59.19/59.26 cnf(671,plain,
% 59.19/59.26 (~P2(a1,x6711,a4)+E(a4,a1)),
% 59.19/59.26 inference(scs_inference,[],[581,26])).
% 59.19/59.26 cnf(681,plain,
% 59.19/59.26 (P2(a1,f3(a5,f3(x6811,x6811)),a4)+~P2(a4,a1,a5)),
% 59.19/59.26 inference(scs_inference,[],[440,644,10])).
% 59.19/59.26 cnf(700,plain,
% 59.19/59.26 (P2(x7001,a2,f3(x7002,x7002))),
% 59.19/59.26 inference(scs_inference,[],[16,39,10])).
% 59.19/59.26 cnf(701,plain,
% 59.19/59.26 (P2(x7011,f3(x7012,x7012),x7011)),
% 59.19/59.26 inference(scs_inference,[],[16,19,39,10,9])).
% 59.19/59.26 cnf(708,plain,
% 59.19/59.26 (P2(a5,x7081,f3(f3(a6,a7),a1))),
% 59.19/59.26 inference(scs_inference,[],[17,221,10])).
% 59.19/59.26 cnf(712,plain,
% 59.19/59.26 (P2(x7121,f3(a2,f3(a5,a5)),f3(x7122,x7122))),
% 59.19/59.26 inference(scs_inference,[],[17,454,71,700,10,9])).
% 59.19/59.26 cnf(725,plain,
% 59.19/59.26 (P2(f3(a1,a4),f3(f3(a7,a5),a7),f3(x7251,x7251))),
% 59.19/59.26 inference(scs_inference,[],[16,412,561,181,10,9,8])).
% 59.19/59.26 cnf(728,plain,
% 59.19/59.26 (P2(f3(a1,a4),a5,f3(x7281,x7281))),
% 59.19/59.26 inference(scs_inference,[],[18,484,221,725,10,9])).
% 59.19/59.26 cnf(739,plain,
% 59.19/59.26 (P2(x7391,x7391,f3(f3(a7,a5),f3(a6,a1)))),
% 59.19/59.26 inference(scs_inference,[],[18,454,10])).
% 59.19/59.26 cnf(755,plain,
% 59.19/59.26 (P2(a5,x7551,f3(x7552,x7552))),
% 59.19/59.26 inference(scs_inference,[],[17,39,10])).
% 59.19/59.26 cnf(756,plain,
% 59.19/59.26 (P2(f3(a5,a5),f3(x7561,x7561),f3(f3(x7562,x7562),f3(a5,a5)))),
% 59.19/59.26 inference(scs_inference,[],[17,103,39,10,9])).
% 59.19/59.26 cnf(759,plain,
% 59.19/59.26 (P2(a5,x7591,f3(x7592,a2))),
% 59.19/59.26 inference(scs_inference,[],[17,248,10])).
% 59.19/59.26 cnf(776,plain,
% 59.19/59.26 (~P2(a4,f3(a1,f3(x7761,x7761)),a5)+E(f3(a1,f3(x7761,x7761)),a4)),
% 59.19/59.26 inference(scs_inference,[],[527,25])).
% 59.19/59.26 cnf(786,plain,
% 59.19/59.26 (E(f3(a7,a5),f3(a6,a1))+~P2(f3(a6,a1),f3(a7,a5),a5)),
% 59.19/59.26 inference(scs_inference,[],[586,25])).
% 59.19/59.26 cnf(789,plain,
% 59.19/59.26 (P2(f3(a1,a4),x7891,f3(f3(a6,a7),a1))),
% 59.19/59.26 inference(scs_inference,[],[18,103,181,708,10,9,8])).
% 59.19/59.26 cnf(791,plain,
% 59.19/59.26 (P2(f3(x7911,a2),x7912,f3(f3(a6,a7),a1))),
% 59.19/59.26 inference(scs_inference,[],[275,221,10])).
% 59.19/59.26 cnf(792,plain,
% 59.19/59.26 (P2(f3(a1,a4),f3(f3(a6,a7),a1),f3(x7921,x7921))),
% 59.19/59.26 inference(scs_inference,[],[275,221,728,10,9])).
% 59.19/59.26 cnf(800,plain,
% 59.19/59.26 (E(a1,f3(a4,f3(a5,a5)))+~P2(f3(a4,f3(a5,a5)),a1,a5)),
% 59.19/59.26 inference(scs_inference,[],[637,25])).
% 59.19/59.26 cnf(809,plain,
% 59.19/59.26 (P2(x8091,x8091,f3(x8092,x8092))),
% 59.19/59.26 inference(scs_inference,[],[18,39,10])).
% 59.19/59.26 cnf(812,plain,
% 59.19/59.26 (P2(x8121,x8121,f3(x8122,a2))),
% 59.19/59.26 inference(scs_inference,[],[18,248,10])).
% 59.19/59.26 cnf(819,plain,
% 59.19/59.26 (P2(f3(a7,a5),f3(a6,a1),a5)),
% 59.19/59.26 inference(scs_inference,[],[20,445,10])).
% 59.19/59.26 cnf(821,plain,
% 59.19/59.26 (P2(f3(a7,a5),a7,a5)),
% 59.19/59.26 inference(scs_inference,[],[20,445,287,10,9])).
% 59.19/59.26 cnf(829,plain,
% 59.19/59.26 (P2(x8291,x8291,f3(a5,f3(x8292,x8292)))),
% 59.19/59.26 inference(scs_inference,[],[18,353,10])).
% 59.19/59.26 cnf(831,plain,
% 59.19/59.26 (P2(f3(a7,a5),f3(a5,f3(x8311,x8311)),f3(a6,a1))+~P2(f3(a6,a1),f3(a7,a5),a5)),
% 59.19/59.26 inference(scs_inference,[],[440,786,10])).
% 59.19/59.26 cnf(836,plain,
% 59.19/59.26 (P2(f3(a6,a8),a4,a5)),
% 59.19/59.26 inference(scs_inference,[],[20,455,10])).
% 59.19/59.26 cnf(849,plain,
% 59.19/59.26 (P2(f3(f3(a6,a8),a4),x8491,f3(x8492,x8492))),
% 59.19/59.26 inference(scs_inference,[],[275,463,755,10,8])).
% 59.19/59.26 cnf(851,plain,
% 59.19/59.26 (~P2(x8511,a2,a8)),
% 59.19/59.26 inference(scs_inference,[],[16,491,27])).
% 59.19/59.26 cnf(855,plain,
% 59.19/59.26 (~P1(a2,a4)),
% 59.19/59.26 inference(scs_inference,[],[16,15,12,493,819,491,27,10,9,22])).
% 59.19/59.26 cnf(862,plain,
% 59.19/59.26 (~E(a1,a2)),
% 59.19/59.26 inference(scs_inference,[],[11,16,15,12,493,819,491,27,10,9,22,84,26,6])).
% 59.19/59.26 cnf(867,plain,
% 59.19/59.26 (~P1(a2,a1)),
% 59.19/59.26 inference(scs_inference,[],[351,862,18,12,855,491,27,6,22])).
% 59.19/59.26 cnf(879,plain,
% 59.19/59.26 (~E(f3(a6,a8),a2)),
% 59.19/59.26 inference(scs_inference,[],[126,439,15,855,27,6])).
% 59.19/59.26 cnf(890,plain,
% 59.19/59.26 (~E(f3(a6,a7),a2)),
% 59.19/59.26 inference(scs_inference,[],[153,14,867,42,27,6])).
% 59.19/59.26 cnf(894,plain,
% 59.19/59.26 (~E(f3(a6,a8),f3(a2,f3(a5,a5)))),
% 59.19/59.26 inference(scs_inference,[],[153,879,14,12,89,867,42,27,6,22,3])).
% 59.19/59.26 cnf(902,plain,
% 59.19/59.26 (~P2(a6,a1,a8)),
% 59.19/59.26 inference(scs_inference,[],[14,68,27])).
% 59.19/59.26 cnf(904,plain,
% 59.19/59.26 (~E(f3(f3(a6,a8),f3(a5,a5)),a2)),
% 59.19/59.26 inference(scs_inference,[],[149,14,68,855,27,6])).
% 59.19/59.26 cnf(908,plain,
% 59.19/59.26 (~E(f3(a6,a7),f3(a2,f3(a5,a5)))),
% 59.19/59.26 inference(scs_inference,[],[87,149,890,14,89,894,68,855,27,6,22,3])).
% 59.19/59.26 cnf(911,plain,
% 59.19/59.26 (~E(a5,a2)),
% 59.19/59.26 inference(scs_inference,[],[87,149,890,14,19,385,89,894,68,851,836,855,27,6,22,3,10,9])).
% 59.19/59.26 cnf(918,plain,
% 59.19/59.26 (~P2(a6,a4,a5)),
% 59.19/59.26 inference(scs_inference,[],[34,15,27])).
% 59.19/59.26 cnf(920,plain,
% 59.19/59.26 (~E(f3(f3(a6,a7),f3(a5,a5)),a2)),
% 59.19/59.26 inference(scs_inference,[],[413,34,15,867,27,6])).
% 59.19/59.26 cnf(927,plain,
% 59.19/59.26 (~E(a5,a6)),
% 59.19/59.26 inference(scs_inference,[],[87,413,34,16,17,15,454,908,867,836,27,6,22,10,9,8])).
% 59.19/59.26 cnf(929,plain,
% 59.19/59.26 (~P1(a6,a4)),
% 59.19/59.26 inference(scs_inference,[],[87,413,34,16,17,15,454,908,867,836,27,6,22,10,9,8,24])).
% 59.19/59.26 cnf(940,plain,
% 59.19/59.26 (~E(a1,a6)),
% 59.19/59.26 inference(scs_inference,[],[11,14,929,124,26,27,6])).
% 59.19/59.26 cnf(941,plain,
% 59.19/59.26 (~P1(a2,f3(f3(a6,a8),f3(a5,a5)))),
% 59.19/59.26 inference(scs_inference,[],[11,904,14,12,929,124,26,27,6,22])).
% 59.19/59.26 cnf(945,plain,
% 59.19/59.26 (~E(a6,a4)),
% 59.19/59.26 inference(scs_inference,[],[11,904,18,14,12,493,918,929,124,836,26,27,6,22,10,9])).
% 59.19/59.26 cnf(954,plain,
% 59.19/59.26 (~E(f3(a1,f3(x9541,x9541)),a6)),
% 59.19/59.26 inference(scs_inference,[],[351,75,15,941,929,26,27,6])).
% 59.19/59.26 cnf(955,plain,
% 59.19/59.26 (~P1(a2,f3(f3(a6,a7),f3(a5,a5)))),
% 59.19/59.26 inference(scs_inference,[],[351,920,75,15,12,941,929,26,27,6,22])).
% 59.19/59.26 cnf(959,plain,
% 59.19/59.26 (~E(a4,a1)),
% 59.19/59.26 inference(scs_inference,[],[351,920,75,275,15,12,502,941,902,929,26,27,6,22,10,9])).
% 59.19/59.26 cnf(962,plain,
% 59.19/59.26 (~P1(a4,a1)),
% 59.19/59.26 inference(scs_inference,[],[351,920,75,315,275,15,12,502,941,902,929,26,27,6,22,10,9,8,581])).
% 59.19/59.26 cnf(963,plain,
% 59.19/59.26 (~P1(f3(a4,f3(a5,a5)),a1)),
% 59.19/59.26 inference(scs_inference,[],[351,920,75,315,275,15,12,502,941,902,929,26,27,6,22,10,9,8,581,640])).
% 59.19/59.26 cnf(964,plain,
% 59.19/59.26 (~P2(a1,x9641,a4)),
% 59.19/59.26 inference(scs_inference,[],[959,671])).
% 59.19/59.26 cnf(967,plain,
% 59.19/59.26 (~P2(a4,a1,a5)),
% 59.19/59.26 inference(scs_inference,[],[964,681])).
% 59.19/59.26 cnf(971,plain,
% 59.19/59.26 (~P2(a6,a1,a6)),
% 59.19/59.26 inference(scs_inference,[],[964,14,955,166,681,26,27])).
% 59.19/59.26 cnf(982,plain,
% 59.19/59.26 (~P2(a6,a4,f3(a7,a5))),
% 59.19/59.26 inference(scs_inference,[],[184,15,27])).
% 59.19/59.26 cnf(985,plain,
% 59.19/59.26 (P2(f3(x9851,x9851),x9852,f3(x9853,a2))),
% 59.19/59.26 inference(scs_inference,[],[153,184,183,15,248,962,27,6,10])).
% 59.19/59.26 cnf(988,plain,
% 59.19/59.26 (~E(a5,a4)),
% 59.19/59.26 inference(scs_inference,[],[153,967,184,16,17,183,15,248,962,27,6,10,9,8])).
% 59.19/59.26 cnf(993,plain,
% 59.19/59.26 (~E(f3(a6,a7),f3(a4,f3(a5,a5)))),
% 59.19/59.26 inference(scs_inference,[],[153,260,15,963,27,6])).
% 59.19/59.26 cnf(1002,plain,
% 59.19/59.27 (~E(f3(f3(a6,a7),f3(a5,a5)),a4)),
% 59.19/59.27 inference(scs_inference,[],[413,281,15,962,27,6])).
% 59.19/59.27 cnf(1006,plain,
% 59.19/59.27 (~E(f3(x10061,x10061),a4)),
% 59.19/59.27 inference(scs_inference,[],[413,281,967,183,15,74,221,962,819,27,6,10,9,8])).
% 59.19/59.27 cnf(1012,plain,
% 59.19/59.27 (~E(a5,a1)),
% 59.19/59.27 inference(scs_inference,[],[299,15,19,372,971,821,27,10,9])).
% 59.19/59.27 cnf(1014,plain,
% 59.19/59.27 (~E(f3(a1,a4),a4)),
% 59.19/59.27 inference(scs_inference,[],[299,967,207,15,19,372,971,821,27,10,9,8])).
% 59.19/59.27 cnf(1019,plain,
% 59.19/59.27 (~E(f3(a4,f3(a5,a5)),a1)),
% 59.19/59.27 inference(scs_inference,[],[335,15,119,902,27,9])).
% 59.19/59.27 cnf(1040,plain,
% 59.19/59.27 (~P2(x10401,f3(a2,f3(a5,a5)),a8)),
% 59.19/59.27 inference(scs_inference,[],[74,491,27])).
% 59.19/59.27 cnf(1048,plain,
% 59.19/59.27 (~E(a4,f3(a2,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[993,15,19,1040,27,9])).
% 59.19/59.27 cnf(1054,plain,
% 59.19/59.27 (P2(x10541,a5,x10541)),
% 59.19/59.27 inference(rename_variables,[],[19])).
% 59.19/59.27 cnf(1056,plain,
% 59.19/59.27 (~P1(f3(a2,f3(a5,a5)),a4)),
% 59.19/59.27 inference(scs_inference,[],[87,1002,19,1048,27,22])).
% 59.19/59.27 cnf(1059,plain,
% 59.19/59.27 (~E(a5,f3(a2,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[87,1002,19,1054,1048,1040,27,22,9])).
% 59.19/59.27 cnf(1075,plain,
% 59.19/59.27 (~E(a1,f3(a2,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[11,87,954,19,1059,1056,27,22,6])).
% 59.19/59.27 cnf(1076,plain,
% 59.19/59.27 (P2(f3(a6,a7),a1,a5)),
% 59.19/59.27 inference(scs_inference,[],[11,87,954,19,20,204,1059,1056,27,22,6,10])).
% 59.19/59.27 cnf(1092,plain,
% 59.19/59.27 (~E(f3(x10921,a2),a4)),
% 59.19/59.27 inference(scs_inference,[],[87,1075,967,275,19,218,792,789,27,22,10,9,8])).
% 59.19/59.27 cnf(1131,plain,
% 59.19/59.27 (~P2(a6,a4,f3(x11311,a2))),
% 59.19/59.27 inference(scs_inference,[],[318,15,27])).
% 59.19/59.27 cnf(1140,plain,
% 59.19/59.27 (P2(f3(a1,a4),x11401,f3(x11402,a2))),
% 59.19/59.27 inference(scs_inference,[],[401,207,15,248,27,10])).
% 59.19/59.27 cnf(1156,plain,
% 59.19/59.27 (~E(f3(f3(x11561,a2),f3(a5,a5)),a4)),
% 59.19/59.27 inference(scs_inference,[],[967,143,181,559,609,42,27,10,9,8])).
% 59.19/59.27 cnf(1159,plain,
% 59.19/59.27 (~P2(a6,f3(a1,f3(a5,a5)),a8)),
% 59.19/59.27 inference(scs_inference,[],[147,68,27])).
% 59.19/59.27 cnf(1164,plain,
% 59.19/59.27 (P2(f3(a6,a8),a4,f3(f3(a6,a7),a1))),
% 59.19/59.27 inference(scs_inference,[],[611,147,221,1156,68,836,27,22,10])).
% 59.19/59.27 cnf(1173,plain,
% 59.19/59.27 (~E(a4,f3(a1,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[15,210,372,481,1159,1076,27,10,9])).
% 59.19/59.27 cnf(1177,plain,
% 59.19/59.27 (~P1(a4,f3(a1,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[15,210,372,481,849,1159,1131,1076,27,10,9,8,529])).
% 59.19/59.27 cnf(1237,plain,
% 59.19/59.27 (~P1(a6,f3(a4,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[34,119,27,24])).
% 59.19/59.27 cnf(1271,plain,
% 59.19/59.27 (~P1(f3(a6,a1),f3(a7,a5))+P2(f3(a7,a5),f3(a5,f3(x12711,x12711)),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[831,24])).
% 59.19/59.27 cnf(1274,plain,
% 59.19/59.27 (~P2(f3(a7,a5),x12741,f3(a6,a1))+P2(f3(a7,a5),f3(a5,f3(x12742,x12742)),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[1271,26])).
% 59.19/59.27 cnf(1326,plain,
% 59.19/59.27 (~E(f3(a6,a1),f3(a7,a5))+P2(f3(a7,a5),f3(a5,f3(x13261,x13261)),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[440,1274,8])).
% 59.19/59.27 cnf(1329,plain,
% 59.19/59.27 (~P2(f3(a7,a5),f3(a5,f3(x13291,x13291)),a2)+~E(f3(a6,a1),f3(a7,a5))),
% 59.19/59.27 inference(scs_inference,[],[481,1326,27])).
% 59.19/59.27 cnf(1332,plain,
% 59.19/59.27 (~E(f3(a7,a5),f3(a6,a1))+~P2(f3(a7,a5),f3(a5,f3(x13321,x13321)),a2)),
% 59.19/59.27 inference(scs_inference,[],[1329,2])).
% 59.19/59.27 cnf(1335,plain,
% 59.19/59.27 (~P1(f3(a6,a1),f3(a7,a5))+~P2(f3(a7,a5),f3(a5,f3(x13351,x13351)),a2)),
% 59.19/59.27 inference(scs_inference,[],[1332,586])).
% 59.19/59.27 cnf(1336,plain,
% 59.19/59.27 (~P2(x13361,x13361,a6)),
% 59.19/59.27 inference(scs_inference,[],[739,460,27])).
% 59.19/59.27 cnf(1338,plain,
% 59.19/59.27 (~P2(f3(a6,a1),f3(a7,a5),a5)+~P2(f3(a7,a5),f3(a5,f3(x13381,x13381)),a2)),
% 59.19/59.27 inference(scs_inference,[],[1335,25])).
% 59.19/59.27 cnf(1341,plain,
% 59.19/59.27 (~E(a2,f3(a7,a5))+~P2(f3(a7,a5),f3(a5,f3(x13411,x13411)),a2)),
% 59.19/59.27 inference(scs_inference,[],[16,1338,9])).
% 59.19/59.27 cnf(1344,plain,
% 59.19/59.27 (~E(f3(a7,a5),a2)+~P2(f3(a7,a5),f3(a5,f3(x13441,x13441)),a2)),
% 59.19/59.27 inference(scs_inference,[],[1341,2])).
% 59.19/59.27 cnf(1347,plain,
% 59.19/59.27 (~E(f3(a7,a5),a2)),
% 59.19/59.27 inference(scs_inference,[],[440,1344,10])).
% 59.19/59.27 cnf(1371,plain,
% 59.19/59.27 (~P2(a6,a5,a1)),
% 59.19/59.27 inference(scs_inference,[],[940,19,27])).
% 59.19/59.27 cnf(1494,plain,
% 59.19/59.27 (~P2(a2,a7,a5)),
% 59.19/59.27 inference(scs_inference,[],[12,21,23,25])).
% 59.19/59.27 cnf(1497,plain,
% 59.19/59.27 (~P2(a7,x14971,a2)),
% 59.19/59.27 inference(scs_inference,[],[1494,24,26])).
% 59.19/59.27 cnf(1511,plain,
% 59.19/59.27 (~E(f3(a1,a4),a2)),
% 59.19/59.27 inference(scs_inference,[],[1494,207,8])).
% 59.19/59.27 cnf(1516,plain,
% 59.19/59.27 (~P2(a4,f3(a1,f3(a5,a5)),a5)),
% 59.19/59.27 inference(scs_inference,[],[1173,2,776])).
% 59.19/59.27 cnf(1529,plain,
% 59.19/59.27 (~P2(f3(a4,f3(a5,a5)),a1,a5)),
% 59.19/59.27 inference(scs_inference,[],[1019,2,800])).
% 59.19/59.27 cnf(1530,plain,
% 59.19/59.27 (~E(f3(x15301,x15301),f3(a8,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[228,89,3])).
% 59.19/59.27 cnf(1574,plain,
% 59.19/59.27 (~E(a6,a1)),
% 59.19/59.27 inference(scs_inference,[],[954,71,2,3])).
% 59.19/59.27 cnf(1597,plain,
% 59.19/59.27 (~P1(a4,f3(x15971,a2))),
% 59.19/59.27 inference(scs_inference,[],[1516,285,24,23])).
% 59.19/59.27 cnf(1600,plain,
% 59.19/59.27 (~P1(a8,f3(a7,a5))),
% 59.19/59.27 inference(scs_inference,[],[21,157,1597,26,23])).
% 59.19/59.27 cnf(1602,plain,
% 59.19/59.27 (~E(f3(x16021,x16021),f3(a4,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[21,157,1597,1529,183,26,23,8])).
% 59.19/59.27 cnf(1607,plain,
% 59.19/59.27 (~E(a4,f3(a5,a5))),
% 59.19/59.27 inference(scs_inference,[],[21,157,1597,1529,335,183,669,26,23,8,27,5])).
% 59.19/59.27 cnf(1611,plain,
% 59.19/59.27 (~P1(a8,f3(f3(a7,a5),f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[21,1600,432,26,23])).
% 59.19/59.27 cnf(1625,plain,
% 59.19/59.27 (~P1(a6,f3(a6,a8))),
% 59.19/59.27 inference(scs_inference,[],[1611,151,1237,26,23])).
% 59.19/59.27 cnf(1628,plain,
% 59.19/59.27 (~E(f3(x16281,a2),f3(a4,f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[1611,1529,151,275,217,1237,1607,26,23,3,8])).
% 59.19/59.27 cnf(1638,plain,
% 59.19/59.27 (~P1(a4,f3(a6,a7))),
% 59.19/59.27 inference(scs_inference,[],[1625,261,1177,26,23])).
% 59.19/59.27 cnf(1650,plain,
% 59.19/59.27 (~P1(a6,a1)),
% 59.19/59.27 inference(scs_inference,[],[1638,367,1237,26,23])).
% 59.19/59.27 cnf(1657,plain,
% 59.19/59.27 (~P1(a6,f3(a6,a7))),
% 59.19/59.27 inference(scs_inference,[],[153,1650,26,23])).
% 59.19/59.27 cnf(1659,plain,
% 59.19/59.27 (~E(f3(a6,a7),a6)),
% 59.19/59.27 inference(scs_inference,[],[153,1650,26,23,6])).
% 59.19/59.27 cnf(1663,plain,
% 59.19/59.27 (~E(f3(a8,a7),a5)),
% 59.19/59.27 inference(scs_inference,[],[21,20,25,10])).
% 59.19/59.27 cnf(1666,plain,
% 59.19/59.27 (~P1(a6,f3(f3(a6,a7),f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[413,1657,1650,26,23])).
% 59.19/59.27 cnf(1668,plain,
% 59.19/59.27 (~E(f3(f3(a6,a7),f3(a5,a5)),a6)),
% 59.19/59.27 inference(scs_inference,[],[413,1657,1650,26,23,6])).
% 59.19/59.27 cnf(1674,plain,
% 59.19/59.27 (P2(a1,a4,a5)),
% 59.19/59.27 inference(scs_inference,[],[1666,20,65,26,10])).
% 59.19/59.27 cnf(1678,plain,
% 59.19/59.27 (~E(f3(a8,a7),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[1666,20,65,71,1663,26,10,9,3])).
% 59.19/59.27 cnf(1682,plain,
% 59.19/59.27 (~E(f3(a8,a7),f3(f3(a6,a7),a1))),
% 59.19/59.27 inference(scs_inference,[],[204,454,1674,1663,10,3])).
% 59.19/59.27 cnf(1686,plain,
% 59.19/59.27 (P2(f3(a6,a8),a4,f3(a5,a5))),
% 59.19/59.27 inference(scs_inference,[],[218,1164,10])).
% 59.19/59.27 cnf(1711,plain,
% 59.19/59.27 (~E(f3(a8,a7),f3(a5,a5))),
% 59.19/59.27 inference(scs_inference,[],[275,353,271,1682,10,3])).
% 59.19/59.27 cnf(1724,plain,
% 59.19/59.27 (P2(a1,a4,f3(f3(a6,a7),a1))),
% 59.19/59.27 inference(scs_inference,[],[221,1674,10])).
% 59.19/59.27 cnf(1725,plain,
% 59.19/59.27 (~E(f3(a8,a7),f3(f3(x17251,x17251),f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[111,221,1711,1674,10,3])).
% 59.19/59.27 cnf(1726,plain,
% 59.19/59.27 (~P2(a6,a5,f3(a6,a7))),
% 59.19/59.27 inference(scs_inference,[],[1659,19,111,221,1711,1674,10,3,27])).
% 59.19/59.27 cnf(1732,plain,
% 59.19/59.27 (~P2(x17321,f3(a2,f3(a5,a5)),f3(a8,a7))),
% 59.19/59.27 inference(scs_inference,[],[712,217,218,1725,1724,1711,10,3,27])).
% 59.19/59.27 cnf(1743,plain,
% 59.19/59.27 (~E(f3(a8,a7),f3(x17431,x17431))),
% 59.19/59.27 inference(scs_inference,[],[20,372,141,1732,1711,836,9,10,3])).
% 59.19/59.27 cnf(1767,plain,
% 59.19/59.27 (~P2(a8,a5,f3(a5,a5))),
% 59.19/59.27 inference(scs_inference,[],[1530,19,4,27])).
% 59.19/59.27 cnf(1808,plain,
% 59.19/59.27 (~P2(x18081,f3(x18081,f3(x18082,x18082)),a8)),
% 59.19/59.27 inference(scs_inference,[],[30,559,653,36,1743,27,28])).
% 59.19/59.27 cnf(1850,plain,
% 59.19/59.27 (~E(a2,f3(x18501,x18501))),
% 59.19/59.27 inference(scs_inference,[],[1668,1808,654,701,9,27,5])).
% 59.19/59.27 cnf(1875,plain,
% 59.19/59.27 (~E(a7,a5)),
% 59.19/59.27 inference(scs_inference,[],[20,1726,9])).
% 59.19/59.27 cnf(1883,plain,
% 59.19/59.27 (~E(a7,f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[19,111,65,1875,10,3])).
% 59.19/59.27 cnf(1887,plain,
% 59.19/59.27 (~E(a7,f3(f3(a6,a7),a1))),
% 59.19/59.27 inference(scs_inference,[],[204,1875,3])).
% 59.19/59.27 cnf(1888,plain,
% 59.19/59.27 (~P2(a5,x18881,a7)),
% 59.19/59.27 inference(scs_inference,[],[17,204,1875,3,27])).
% 59.19/59.27 cnf(1901,plain,
% 59.19/59.27 (~P1(a4,f3(a5,a5))),
% 59.19/59.27 inference(scs_inference,[],[1602,201,4,22])).
% 59.19/59.27 cnf(1911,plain,
% 59.19/59.27 (~P2(a4,a5,f3(a5,a5))),
% 59.19/59.27 inference(scs_inference,[],[1602,19,4,27])).
% 59.19/59.27 cnf(1912,plain,
% 59.19/59.27 (~P2(x19121,x19121,a7)),
% 59.19/59.27 inference(scs_inference,[],[18,1875,27])).
% 59.19/59.27 cnf(1923,plain,
% 59.19/59.27 (~P2(f3(x19231,x19231),x19232,a7)),
% 59.19/59.27 inference(scs_inference,[],[809,183,1911,1875,9,27])).
% 59.19/59.27 cnf(1958,plain,
% 59.19/59.27 (~P2(f3(a1,a4),x19581,a7)),
% 59.19/59.27 inference(scs_inference,[],[207,1875,27])).
% 59.19/59.27 cnf(1966,plain,
% 59.19/59.27 (~P2(f3(x19661,a2),x19662,a7)),
% 59.19/59.27 inference(scs_inference,[],[791,1887,27])).
% 59.19/59.27 cnf(2019,plain,
% 59.19/59.27 (P2(f3(f3(a5,a5),a5),f3(x20191,x20191),f3(x20192,x20192))),
% 59.19/59.27 inference(scs_inference,[],[701,164,10])).
% 59.19/59.27 cnf(2028,plain,
% 59.19/59.27 (E(f3(a5,x20281),f3(f3(a1,a4),x20281))),
% 59.19/59.27 inference(scs_inference,[],[65,4,2])).
% 59.19/59.27 cnf(2030,plain,
% 59.19/59.27 (P1(f3(a6,a1),a7)),
% 59.19/59.27 inference(scs_inference,[],[30,138,2028,2,6])).
% 59.19/59.27 cnf(2032,plain,
% 59.19/59.27 (~P1(a8,f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[30,21,138,2028,2,6,23])).
% 59.19/59.27 cnf(2034,plain,
% 59.19/59.27 (P2(a7,a5,f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[30,21,19,138,2028,2,6,23,10])).
% 59.19/59.27 cnf(2035,plain,
% 59.19/59.27 (P2(x20351,a5,x20351)),
% 59.19/59.27 inference(rename_variables,[],[19])).
% 59.19/59.27 cnf(2046,plain,
% 59.19/59.27 (P2(a7,f3(f3(a7,a5),f3(a6,a1)),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[30,21,19,2035,138,454,36,2019,1743,2028,2,6,23,10,27,3,28,26,9])).
% 59.19/59.27 cnf(2048,plain,
% 59.19/59.27 (P2(a7,f3(f3(a6,a8),a4),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[463,2034,9])).
% 59.19/59.27 cnf(2049,plain,
% 59.19/59.27 (P2(f3(a7,a5),a7,f3(f3(a6,a8),a4))),
% 59.19/59.27 inference(scs_inference,[],[463,821,2034,9,10])).
% 59.19/59.27 cnf(2053,plain,
% 59.19/59.27 (P1(a7,f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[30,287,6])).
% 59.19/59.27 cnf(2056,plain,
% 59.19/59.27 (P2(f3(a6,a1),a5,a7)),
% 59.19/59.27 inference(scs_inference,[],[30,19,287,138,2049,6,9,10])).
% 59.19/59.27 cnf(2063,plain,
% 59.19/59.27 (P2(a7,f3(f3(a7,a5),a7),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[493,2034,9])).
% 59.19/59.27 cnf(2068,plain,
% 59.19/59.27 (P2(a7,f3(f3(a5,a2),a5),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[502,1076,2034,10,9])).
% 59.19/59.27 cnf(2073,plain,
% 59.19/59.27 (P2(a7,f3(x20731,x20731),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[545,39,2034,10,9])).
% 59.19/59.27 cnf(2078,plain,
% 59.19/59.27 (P2(a7,f3(x20781,a2),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[275,248,2034,10,9])).
% 59.19/59.27 cnf(2084,plain,
% 59.19/59.27 (P2(a7,f3(a5,f3(x20841,x20841)),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[353,1674,2034,10,9])).
% 59.19/59.27 cnf(2089,plain,
% 59.19/59.27 (P2(a7,f3(a1,a4),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[181,821,2034,10,9])).
% 59.19/59.27 cnf(2100,plain,
% 59.19/59.27 (E(f3(x21001,x21001),f3(x21002,x21002))),
% 59.19/59.27 inference(scs_inference,[],[164,372,92,1674,10,3])).
% 59.19/59.27 cnf(2101,plain,
% 59.19/59.27 (P2(a7,f3(a5,f3(a1,a4)),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[164,372,92,1674,2034,10,3,9])).
% 59.19/59.27 cnf(2103,plain,
% 59.19/59.27 (P2(f3(a1,a4),x21031,f3(f3(a5,a5),a5))),
% 59.19/59.27 inference(scs_inference,[],[1140,92,10])).
% 59.19/59.27 cnf(2105,plain,
% 59.19/59.27 (E(f3(x21051,x21051),f3(f3(a5,a5),a5))),
% 59.19/59.27 inference(rename_variables,[],[92])).
% 59.19/59.27 cnf(2107,plain,
% 59.19/59.27 (P2(a7,f3(f3(a5,a5),a5),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[1140,373,39,92,2105,2078,10,3,9])).
% 59.19/59.27 cnf(2111,plain,
% 59.19/59.27 (P2(f3(a6,a1),f3(f3(a5,a5),a5),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[1140,373,138,39,92,2105,2078,10,3,9,2,8])).
% 59.19/59.27 cnf(2117,plain,
% 59.19/59.27 (P2(a7,f3(a5,f3(a5,a2)),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[985,455,385,248,92,2034,10,3,9])).
% 59.19/59.27 cnf(2128,plain,
% 59.19/59.27 (P2(f3(a6,a1),f3(f3(a5,a5),a5),a7)),
% 59.19/59.27 inference(scs_inference,[],[103,287,63,2111,8,10])).
% 59.19/59.27 cnf(2133,plain,
% 59.19/59.27 (~E(f3(a6,a1),f3(x21331,x21331))),
% 59.19/59.27 inference(scs_inference,[],[1923,2128,8])).
% 59.19/59.27 cnf(2138,plain,
% 59.19/59.27 (~E(f3(f3(a5,a5),a5),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[204,39,92,1686,1923,2128,1912,8,10,3,9])).
% 59.19/59.27 cnf(2146,plain,
% 59.19/59.27 (P2(a7,f3(f3(a5,a5),a5),a7)),
% 59.19/59.27 inference(scs_inference,[],[287,63,756,2107,2138,2073,8,27,10])).
% 59.19/59.27 cnf(2149,plain,
% 59.19/59.27 (~P1(a2,f3(a5,a5))),
% 59.19/59.27 inference(scs_inference,[],[1628,201,5,22])).
% 59.19/59.27 cnf(2152,plain,
% 59.19/59.27 (~E(f3(a6,a1),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[1958,2149,2128,26,8])).
% 59.19/59.27 cnf(2203,plain,
% 59.19/59.27 (~E(a7,f3(x22031,a2))),
% 59.19/59.27 inference(scs_inference,[],[1966,2146,8])).
% 59.19/59.27 cnf(2208,plain,
% 59.19/59.27 (~E(f3(a6,a1),a5)),
% 59.19/59.27 inference(scs_inference,[],[1888,2128,8])).
% 59.19/59.27 cnf(2213,plain,
% 59.19/59.27 (~P2(x22131,a2,f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[16,2208,27])).
% 59.19/59.27 cnf(2221,plain,
% 59.19/59.27 (~P2(x22211,x22211,f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[18,2208,27])).
% 59.19/59.27 cnf(2231,plain,
% 59.19/59.27 (E(f3(x22311,a5),f3(x22311,f3(a1,a4)))),
% 59.19/59.27 inference(scs_inference,[],[65,5,2])).
% 59.19/59.27 cnf(2236,plain,
% 59.19/59.27 (~P2(x22361,x22361,f3(a6,a1))),
% 59.19/59.27 inference(rename_variables,[],[2221])).
% 59.19/59.27 cnf(2237,plain,
% 59.19/59.27 (~E(f3(f3(a7,a5),a7),a7)),
% 59.19/59.27 inference(scs_inference,[],[17,2063,2231,2221,2236,2084,2208,2,27,8,9])).
% 59.19/59.27 cnf(2239,plain,
% 59.19/59.27 (E(f3(f3(a6,a7),a1),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[17,204,181,2063,2231,2221,2236,2084,2208,2,27,8,9,3])).
% 59.19/59.27 cnf(2246,plain,
% 59.19/59.27 (E(f3(a5,f3(a1,a4)),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[183,357,181,2239,2046,2213,2208,2,27,9,3])).
% 59.19/59.27 cnf(2253,plain,
% 59.19/59.27 (E(f3(a5,f3(a5,a2)),f3(x22531,a2))),
% 59.19/59.27 inference(scs_inference,[],[207,373,248,2246,2101,2221,2208,2,27,9,3])).
% 59.19/59.27 cnf(2260,plain,
% 59.19/59.27 (E(f3(f3(a6,a8),a4),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[389,455,181,2253,2117,2213,2208,2,27,9,3])).
% 59.19/59.27 cnf(2267,plain,
% 59.19/59.27 (E(f3(f3(a5,a2),a5),f3(x22671,x22671))),
% 59.19/59.27 inference(scs_inference,[],[507,494,39,2260,2048,2221,2208,2,27,9,3])).
% 59.19/59.27 cnf(2274,plain,
% 59.19/59.27 (E(f3(a1,a4),f3(x22741,x22741))),
% 59.19/59.27 inference(scs_inference,[],[376,65,39,2267,2068,2213,2208,2,27,9,3])).
% 59.19/59.27 cnf(2276,plain,
% 59.19/59.27 (E(f3(x22761,x22761),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[2274,2])).
% 59.19/59.27 cnf(2279,plain,
% 59.19/59.27 (~E(f3(a1,a4),a7)),
% 59.19/59.27 inference(scs_inference,[],[458,2274,2089,2221,2208,2,27,9])).
% 59.19/59.27 cnf(2281,plain,
% 59.19/59.27 (E(f3(f3(a5,a5),a5),a5)),
% 59.19/59.27 inference(scs_inference,[],[458,164,308,2274,2089,2221,2208,2,27,9,3])).
% 59.19/59.27 cnf(2290,plain,
% 59.19/59.27 (E(f3(f3(x22901,x22901),f3(a5,a5)),a5)),
% 59.19/59.27 inference(scs_inference,[],[467,111,63,2281,2101,2213,2208,2,27,9,3])).
% 59.19/59.27 cnf(2296,plain,
% 59.19/59.27 (~E(f3(f3(a5,a5),a5),a7)),
% 59.19/59.27 inference(scs_inference,[],[497,2290,2107,2221,2208,2,27,9])).
% 59.19/59.27 cnf(2310,plain,
% 59.19/59.27 (E(f3(f3(a5,a2),f3(a1,a4)),a5)),
% 59.19/59.27 inference(scs_inference,[],[65,494,5,3])).
% 59.19/59.27 cnf(2330,plain,
% 59.19/59.27 (E(a5,f3(f3(a5,a2),f3(a1,a4)))),
% 59.19/59.27 inference(scs_inference,[],[2310,2])).
% 59.19/59.27 cnf(2337,plain,
% 59.19/59.27 (~P2(f3(a6,a1),a5,f3(f3(a5,a5),a5))),
% 59.19/59.27 inference(scs_inference,[],[2296,2056,27])).
% 59.19/59.27 cnf(2340,plain,
% 59.19/59.27 (~P2(f3(a6,f3(a5,a5)),a1,f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[143,2279,27])).
% 59.19/59.27 cnf(2347,plain,
% 59.19/59.27 (E(f3(a1,a4),f3(x23471,a2))),
% 59.19/59.27 inference(scs_inference,[],[531,65,248,2340,2237,2056,8,27,3])).
% 59.19/59.27 cnf(2348,plain,
% 59.19/59.27 (E(f3(x23481,a2),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[531,65,248,2340,2237,2056,8,27,3,2])).
% 59.19/59.27 cnf(2357,plain,
% 59.19/59.27 (~E(f3(a1,a4),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[2103,2337,8])).
% 59.19/59.27 cnf(2359,plain,
% 59.19/59.27 (~P2(a6,a7,a6)),
% 59.19/59.27 inference(scs_inference,[],[14,30,1650,2103,2337,8,28])).
% 59.19/59.27 cnf(2365,plain,
% 59.19/59.27 (~E(a5,a7)),
% 59.19/59.27 inference(scs_inference,[],[2359,19,210,2357,27,9])).
% 59.19/59.27 cnf(2367,plain,
% 59.19/59.27 (~P2(a6,f3(a6,a1),a6)),
% 59.19/59.27 inference(scs_inference,[],[14,1650,2053,2359,19,210,2357,27,9,28])).
% 59.19/59.27 cnf(2372,plain,
% 59.19/59.27 (~E(a5,f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[14,2367,19,2365,27,9])).
% 59.19/59.27 cnf(2377,plain,
% 59.19/59.27 (~E(f3(a5,f3(x23771,x23771)),a7)),
% 59.19/59.27 inference(scs_inference,[],[2359,440,315,182,27,9])).
% 59.19/59.27 cnf(2382,plain,
% 59.19/59.27 (~E(f3(a5,f3(x23821,x23821)),f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[14,2367,440,2377,27,9])).
% 59.19/59.27 cnf(2387,plain,
% 59.19/59.27 (P2(f3(f3(x23871,x23871),f3(a5,a5)),f3(a5,a5),f3(x23872,a2))),
% 59.19/59.27 inference(scs_inference,[],[812,143,111,2365,27,9])).
% 59.19/59.27 cnf(2408,plain,
% 59.19/59.27 (~P1(a8,f3(f3(x24081,x24081),f3(a5,a5)))),
% 59.19/59.27 inference(scs_inference,[],[20,210,65,308,272,2330,2387,2372,10,27,9,3,25,24,26,2,23])).
% 59.19/59.27 cnf(2416,plain,
% 59.19/59.27 (~P2(a7,f3(x24161,x24161),f3(a5,f3(x24162,x24162)))),
% 59.19/59.27 inference(scs_inference,[],[2408,506,287,2382,2073,26,10,27])).
% 59.19/59.27 cnf(2418,plain,
% 59.19/59.27 (P2(f3(a6,a1),a7,f3(a5,f3(x24181,x24181)))),
% 59.19/59.27 inference(scs_inference,[],[2408,829,506,287,2382,2073,26,10,27,9])).
% 59.19/59.27 cnf(2423,plain,
% 59.19/59.27 (P2(f3(a6,a1),a7,a5)),
% 59.19/59.27 inference(scs_inference,[],[829,369,2416,2418,8,10])).
% 59.19/59.27 cnf(2424,plain,
% 59.19/59.27 (P2(f3(a6,a1),a7,f3(a5,f3(x24241,x24241)))),
% 59.19/59.27 inference(rename_variables,[],[2418])).
% 59.19/59.27 cnf(2428,plain,
% 59.19/59.27 (P2(f3(a6,a1),f3(x24281,x24281),a7)),
% 59.19/59.27 inference(scs_inference,[],[829,369,164,2416,2418,2424,404,2128,8,10,27,9])).
% 59.19/59.27 cnf(2430,plain,
% 59.19/59.27 (~E(f3(a6,a1),a2)),
% 59.19/59.27 inference(scs_inference,[],[1494,2423,8])).
% 59.19/59.27 cnf(2511,plain,
% 59.19/59.27 (P1(f3(f3(a1,a4),a5),x25111)),
% 59.19/59.27 inference(scs_inference,[],[65,201,5,6])).
% 59.19/59.27 cnf(2513,plain,
% 59.19/59.27 (P1(f3(f3(a1,a4),a5),x25131)),
% 59.19/59.27 inference(rename_variables,[],[2511])).
% 59.19/59.27 cnf(2521,plain,
% 59.19/59.27 (P2(f3(a6,a1),f3(x25211,a2),a7)),
% 59.19/59.27 inference(scs_inference,[],[219,21,2511,2513,654,287,2377,2056,22,23,27,10])).
% 59.19/59.27 cnf(2555,plain,
% 59.19/59.27 (~P2(a8,a4,a7)),
% 59.19/59.27 inference(scs_inference,[],[15,30,21,829,440,1056,28,29])).
% 59.19/59.27 cnf(2586,plain,
% 59.19/59.27 (~P2(a8,a7,a5)),
% 59.19/59.27 inference(scs_inference,[],[21,25])).
% 59.19/59.27 cnf(2588,plain,
% 59.19/59.27 (P1(a7,a6)),
% 59.19/59.27 inference(scs_inference,[],[21,14,25,26])).
% 59.19/59.27 cnf(2590,plain,
% 59.19/59.27 (~E(a2,a5)),
% 59.19/59.27 inference(scs_inference,[],[21,911,14,25,26,2])).
% 59.19/59.27 cnf(2593,plain,
% 59.19/59.27 (~P1(f3(a6,a1),f3(a2,a2))),
% 59.19/59.27 inference(scs_inference,[],[21,911,2100,1901,2133,285,14,25,26,2,7,22])).
% 59.19/59.27 cnf(2605,plain,
% 59.19/59.27 (~E(f3(a1,a4),a1)),
% 59.19/59.27 inference(scs_inference,[],[21,911,2555,1336,1012,2100,2152,1901,2133,2030,2078,285,138,287,14,181,25,26,2,7,22,6,23,8,27,10,3])).
% 59.19/59.27 cnf(2607,plain,
% 59.19/59.27 (~P1(f3(a6,a1),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[21,911,2555,1371,1336,1012,2100,2152,1901,2133,2030,2078,2089,285,308,138,287,14,181,25,26,2,7,22,6,23,8,27,10,3,9,28])).
% 59.19/59.27 cnf(2608,plain,
% 59.19/59.27 (P2(a7,f3(x26081,a2),f3(a6,a1))),
% 59.19/59.27 inference(rename_variables,[],[2078])).
% 59.19/59.27 cnf(2610,plain,
% 59.19/59.27 (P1(f3(a6,a1),f3(a7,a1))),
% 59.19/59.27 inference(scs_inference,[],[21,911,2555,1371,1336,1012,2100,2152,1901,2133,2030,2078,2608,2089,285,308,809,138,287,14,181,20,25,26,2,7,22,6,23,8,27,10,3,9,28,29])).
% 59.19/59.27 cnf(2615,plain,
% 59.19/59.27 (P2(a7,a6,a5)),
% 59.19/59.27 inference(scs_inference,[],[21,911,2555,1371,1336,1012,2100,2152,1901,2133,2030,2078,2608,2089,285,308,809,138,287,14,181,20,25,26,2,7,22,6,23,8,27,10,3,9,28,29,24])).
% 59.19/59.27 cnf(2620,plain,
% 59.19/59.27 (P2(f3(a6,a1),f3(a7,a1),a5)),
% 59.19/59.27 inference(scs_inference,[],[2032,2610,25,24])).
% 59.19/59.27 cnf(2622,plain,
% 59.19/59.27 (P1(f3(x26221,x26222),x26221)),
% 59.19/59.27 inference(scs_inference,[],[2032,2610,20,25,24,26])).
% 59.19/59.27 cnf(2624,plain,
% 59.19/59.27 (~E(a2,f3(a7,a5))),
% 59.19/59.27 inference(scs_inference,[],[1347,2032,2610,20,25,24,26,2])).
% 59.19/59.27 cnf(2625,plain,
% 59.19/59.27 (~P1(f3(a6,a1),f3(x26251,a2))),
% 59.19/59.27 inference(scs_inference,[],[1347,2032,2348,2607,2610,20,25,24,26,2,7])).
% 59.19/59.27 cnf(2626,plain,
% 59.19/59.27 (~P1(a6,a5)),
% 59.19/59.27 inference(scs_inference,[],[927,1347,2032,2348,2607,2610,13,20,25,24,26,2,7,22])).
% 59.19/59.27 cnf(2631,plain,
% 59.19/59.27 (~P1(a7,f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[927,1347,2032,2348,2593,2607,2610,13,138,20,25,24,26,2,7,22,23,6])).
% 59.19/59.27 cnf(2633,plain,
% 59.19/59.27 (~P2(a7,a6,a6)),
% 59.19/59.27 inference(scs_inference,[],[927,2615,1497,1347,2032,2348,2593,2607,2610,13,138,287,20,25,24,26,2,7,22,23,6,8,27])).
% 59.19/59.27 cnf(2643,plain,
% 59.19/59.27 (~P2(a6,a5,a5)),
% 59.19/59.27 inference(scs_inference,[],[2626,25])).
% 59.19/59.27 cnf(2645,plain,
% 59.19/59.27 (P2(f3(x26451,x26452),x26451,a5)),
% 59.19/59.27 inference(scs_inference,[],[2626,2622,25,24])).
% 59.19/59.27 cnf(2647,plain,
% 59.19/59.27 (P1(a8,a6)),
% 59.19/59.27 inference(scs_inference,[],[2626,2622,15,25,24,26])).
% 59.19/59.27 cnf(2651,plain,
% 59.19/59.27 (~P1(a6,a7)),
% 59.19/59.27 inference(scs_inference,[],[2588,2626,2622,1511,166,308,15,25,24,26,2,7,22])).
% 59.19/59.27 cnf(2653,plain,
% 59.19/59.27 (~P1(f3(a7,a1),f3(x26531,a2))),
% 59.19/59.27 inference(scs_inference,[],[2588,2626,2622,1511,2625,2610,166,308,15,25,24,26,2,7,22,23])).
% 59.19/59.27 cnf(2670,plain,
% 59.19/59.27 (~P2(a6,a7,a5)),
% 59.19/59.27 inference(scs_inference,[],[2651,25])).
% 59.19/59.27 cnf(2674,plain,
% 59.19/59.27 (~E(f3(a1,a4),f3(a8,a7))),
% 59.19/59.27 inference(scs_inference,[],[2647,2651,1678,25,24,2])).
% 59.19/59.27 cnf(2675,plain,
% 59.19/59.27 (~P1(f3(a7,a1),f3(x26751,x26751))),
% 59.19/59.27 inference(scs_inference,[],[2647,2651,1678,2653,2100,25,24,2,7])).
% 59.19/59.27 cnf(2678,plain,
% 59.19/59.27 (~P1(a4,a5)),
% 59.19/59.27 inference(scs_inference,[],[988,2647,2651,1678,2653,2100,13,25,24,2,7,22])).
% 59.19/59.27 cnf(2681,plain,
% 59.19/59.27 (~P1(a6,f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[988,2647,2651,1678,2631,2653,2588,2100,13,25,24,2,7,22,23])).
% 59.19/59.27 cnf(2683,plain,
% 59.19/59.27 (~E(f3(a7,x26831),a8)),
% 59.19/59.27 inference(scs_inference,[],[21,988,2647,2651,1678,2631,2653,2588,2622,2100,13,25,24,2,7,22,23,6])).
% 59.19/59.27 cnf(2688,plain,
% 59.19/59.27 (~P1(f3(a6,a1),f3(x26881,x26881))),
% 59.19/59.27 inference(scs_inference,[],[21,988,2586,2647,2651,1678,2631,2645,2653,2588,2622,2100,2428,63,13,669,25,24,2,7,22,23,6,27,10,28])).
% 59.19/59.27 cnf(2701,plain,
% 59.19/59.27 (P1(f3(x27011,x27012),x27011)),
% 59.19/59.27 inference(rename_variables,[],[2622])).
% 59.19/59.27 cnf(2705,plain,
% 59.19/59.27 (~P1(f3(a7,a1),f3(x27051,x27051))),
% 59.19/59.27 inference(rename_variables,[],[2675])).
% 59.19/59.27 cnf(2706,plain,
% 59.19/59.27 (~P1(a7,f3(x27061,x27061))),
% 59.19/59.27 inference(scs_inference,[],[2678,2675,2705,1006,1850,2274,2622,2701,25,2,22,7,23])).
% 59.19/59.27 cnf(2707,plain,
% 59.19/59.27 (P1(f3(x27071,x27072),x27071)),
% 59.19/59.27 inference(rename_variables,[],[2622])).
% 59.19/59.27 cnf(2717,plain,
% 59.19/59.27 (P1(f3(x27171,x27172),x27171)),
% 59.19/59.27 inference(rename_variables,[],[2622])).
% 59.19/59.27 cnf(2719,plain,
% 59.19/59.27 (~E(f3(a5,x27191),a4)),
% 59.19/59.27 inference(scs_inference,[],[945,2643,2678,2675,2705,1006,1850,1767,670,2274,2622,2701,2707,2717,63,654,25,2,22,7,23,27,10,9,28,6])).
% 59.19/59.27 cnf(2725,plain,
% 59.19/59.27 (~E(a1,f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[2688,2605,25,2])).
% 59.19/59.27 cnf(2726,plain,
% 59.19/59.27 (~P1(a2,a5)),
% 59.19/59.27 inference(scs_inference,[],[2590,2688,2605,12,25,2,22])).
% 59.19/59.27 cnf(2729,plain,
% 59.19/59.27 (~P1(a6,f3(a6,a1))),
% 59.19/59.27 inference(scs_inference,[],[2590,2688,2605,2647,2032,12,25,2,22,23])).
% 59.19/59.27 cnf(2738,plain,
% 59.19/59.27 (~P2(a2,a5,a5)),
% 59.19/59.27 inference(scs_inference,[],[2726,25])).
% 59.19/59.27 cnf(2741,plain,
% 59.19/59.27 (P1(f3(a6,a7),a4)),
% 59.19/59.27 inference(scs_inference,[],[2726,1092,11,153,25,2,23])).
% 59.19/59.27 cnf(2743,plain,
% 59.19/59.27 (~P1(a2,f3(x27431,a2))),
% 59.19/59.27 inference(scs_inference,[],[2726,1092,11,153,308,25,2,23,7])).
% 59.19/59.27 cnf(2747,plain,
% 59.19/59.27 (~E(f3(x27471,x27471),a1)),
% 59.19/59.27 inference(scs_inference,[],[2726,532,1092,1012,11,153,308,654,39,25,2,23,7,27,3])).
% 59.19/59.27 cnf(2749,plain,
% 59.19/59.27 (~P1(f3(a6,a1),a5)),
% 59.19/59.27 inference(scs_inference,[],[2670,2726,532,1092,1012,2688,2078,11,153,308,2034,654,39,25,2,23,7,27,3,10,28])).
% 59.19/59.27 cnf(2772,plain,
% 59.19/59.27 (~P1(a4,f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[1014,2749,2747,219,25,2,22])).
% 59.19/59.27 cnf(2775,plain,
% 59.19/59.27 (~P1(a6,f3(a7,a5))),
% 59.19/59.27 inference(scs_inference,[],[1014,2749,2747,1600,2647,219,25,2,22,23])).
% 59.19/59.27 cnf(2777,plain,
% 59.19/59.27 (~P1(a7,a5)),
% 59.19/59.27 inference(scs_inference,[],[1014,2749,2747,1600,2647,219,138,25,2,22,23,6])).
% 59.19/59.27 cnf(2781,plain,
% 59.19/59.27 (~E(f3(x27811,a2),f3(a8,a7))),
% 59.19/59.27 inference(scs_inference,[],[2633,1014,2749,2620,2674,2747,2372,1600,2347,2647,219,138,287,25,2,22,23,6,8,27,3])).
% 59.19/59.27 cnf(2792,plain,
% 59.19/59.27 (~P2(a7,a5,a5)),
% 59.19/59.27 inference(scs_inference,[],[2777,25])).
% 59.19/59.27 cnf(2794,plain,
% 59.19/59.27 (~E(f3(a8,a7),f3(x27941,a2))),
% 59.19/59.27 inference(scs_inference,[],[2777,2781,25,2])).
% 59.19/59.27 cnf(2800,plain,
% 59.19/59.27 (~E(f3(x28001,x28001),f3(a8,a7))),
% 59.19/59.27 inference(scs_inference,[],[1574,2777,2781,2100,301,2610,701,25,2,23,27,3])).
% 59.19/59.27 cnf(2804,plain,
% 59.19/59.27 (P2(f3(a7,a5),f3(a7,a1),a5)),
% 59.19/59.27 inference(scs_inference,[],[1574,2777,2738,2781,2100,301,2610,308,701,25,2,23,27,3,10,24])).
% 59.19/59.27 cnf(2820,plain,
% 59.19/59.27 (~E(a7,a6)),
% 59.19/59.27 inference(scs_inference,[],[2430,2772,2203,2743,2729,2053,2347,12,25,2,22,7,6])).
% 59.19/59.27 cnf(2825,plain,
% 59.19/59.27 (~P1(f3(a8,a7),f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[21,2792,2430,2772,2203,2743,2804,2729,2053,927,2347,12,308,669,138,20,25,2,22,7,6,27,3,10,28])).
% 59.19/59.27 cnf(2829,plain,
% 59.19/59.27 (~P2(a6,f3(a1,a4),f3(x28291,a2))),
% 59.19/59.27 inference(scs_inference,[],[21,2792,2430,2772,2706,2203,2743,2804,2729,2615,2053,927,2521,2347,2089,759,12,308,669,138,20,25,2,22,7,6,27,3,10,28,29])).
% 59.19/59.27 cnf(2838,plain,
% 59.19/59.27 (~P1(a1,f3(a1,a4))),
% 59.19/59.27 inference(scs_inference,[],[2681,2725,2683,2622,25,2,22])).
% 59.19/59.27 cnf(2843,plain,
% 59.19/59.27 (~E(a5,f3(a8,a7))),
% 59.19/59.27 inference(scs_inference,[],[2820,2681,2800,2725,2683,2521,2622,63,25,2,22,27,3])).
% 59.19/59.27 cnf(2845,plain,
% 59.19/59.27 (~P2(a6,f3(a1,a4),f3(x28451,x28451))),
% 59.19/59.27 inference(scs_inference,[],[2820,2681,2800,2725,2829,2683,2521,2100,2622,63,25,2,22,27,3,10])).
% 59.19/59.27 cnf(2862,plain,
% 59.19/59.27 (~P1(f3(a8,a7),f3(x28621,x28621))),
% 59.19/59.27 inference(scs_inference,[],[2775,2825,2624,2719,2276,12,25,2,22,7])).
% 59.19/59.27 cnf(2868,plain,
% 59.19/59.27 (~E(f3(a1,a4),f3(a7,a1))),
% 59.19/59.27 inference(scs_inference,[],[982,2775,2825,2624,2843,2719,2820,2804,2675,2276,219,12,138,20,25,2,22,7,27,3,10,6])).
% 59.19/59.27 cnf(2886,plain,
% 59.19/59.27 ($false),
% 59.19/59.27 inference(scs_inference,[],[21,1883,2862,2794,2868,2845,2838,2741,2348,2274,2521,285,20,15,25,2,22,7,27,10,28]),
% 59.19/59.27 ['proof']).
% 59.19/59.27 % SZS output end Proof
% 59.19/59.27 % Total time :58.620000s
%------------------------------------------------------------------------------