%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN008-4 : 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 : n028.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:50 EDT 2024
% Result : Unsatisfiable 76.95s 76.99s
% Output : CNFRefutation 76.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : HEN008-4 : TPTP v8.2.0. Released v1.0.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n028.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Sat Jun 22 05:25:24 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.52/0.57 start to proof:theBenchmark
% 76.95/76.98 %-------------------------------------------
% 76.95/76.98 % File :CSE---1.7
% 76.95/76.98 % Problem :theBenchmark
% 76.95/76.98 % Transform :cnf
% 76.95/76.98 % Format :tptp:raw
% 76.95/76.98 % Command :java -jar mcs_scs.jar %d %s
% 76.95/76.98
% 76.95/76.98 % Result :Theorem 76.380000s
% 76.95/76.98 % Output :CNFRefutation 76.380000s
% 76.95/76.98 %-------------------------------------------
% 76.95/76.99 %--------------------------------------------------------------------------
% 76.95/76.99 % File : HEN008-4 : TPTP v8.2.0. Released v1.0.0.
% 76.95/76.99 % Domain : Henkin Models
% 76.95/76.99 % Problem : X <= Y => X/Z <= Y/Z
% 76.95/76.99 % Version : [MOW76] axioms : Augmented.
% 76.95/76.99 % English :
% 76.95/76.99
% 76.95/76.99 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 76.95/76.99 % Source : [TPTP]
% 76.95/76.99 % Names :
% 76.95/76.99
% 76.95/76.99 % Status : Unsatisfiable
% 76.95/76.99 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.08 v5.2.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.00 v2.1.0, 0.00 v2.0.0
% 76.95/76.99 % Syntax : Number of clauses : 16 ( 10 unt; 0 nHn; 8 RR)
% 76.95/76.99 % Number of literals : 24 ( 7 equ; 9 neg)
% 76.95/76.99 % Maximal clause size : 3 ( 1 avg)
% 76.95/76.99 % Maximal term depth : 3 ( 1 avg)
% 76.95/76.99 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 76.95/76.99 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% 76.95/76.99 % Number of variables : 25 ( 5 sgn)
% 76.95/76.99 % SPC : CNF_UNS_RFO_SEQ_HRN
% 76.95/76.99
% 76.95/76.99 % Comments :
% 76.95/76.99 %--------------------------------------------------------------------------
% 76.95/76.99 %----Include Henkin model axioms for equality formulation
% 76.95/76.99 include('Axioms/HEN002-0.ax').
% 76.95/76.99 %--------------------------------------------------------------------------
% 76.95/76.99 cnf(everything_divide_id_is_zero,axiom,
% 76.95/76.99 divide(X,identity) = zero ).
% 76.95/76.99
% 76.95/76.99 cnf(zero_divide_anything_is_zero,axiom,
% 76.95/76.99 divide(zero,X) = zero ).
% 76.95/76.99
% 76.95/76.99 cnf(x_divide_x_is_zero,axiom,
% 76.95/76.99 divide(X,X) = zero ).
% 76.95/76.99
% 76.95/76.99 cnf(x_divide_zero_is_x,axiom,
% 76.95/76.99 divide(a,zero) = a ).
% 76.95/76.99
% 76.95/76.99 cnf(transitivity_of_less_equal,axiom,
% 76.95/76.99 ( ~ less_equal(X,Y)
% 76.95/76.99 | ~ less_equal(Y,Z)
% 76.95/76.99 | less_equal(X,Z) ) ).
% 76.95/76.99
% 76.95/76.99 cnf(property_of_divide1,axiom,
% 76.95/76.99 ( ~ less_equal(divide(X,Y),Z)
% 76.95/76.99 | less_equal(divide(X,Z),Y) ) ).
% 76.95/76.99
% 76.95/76.99 cnf(property_of_divide2,axiom,
% 76.95/76.99 ( ~ less_equal(X,Y)
% 76.95/76.99 | less_equal(divide(Z,Y),divide(Z,X)) ) ).
% 76.95/76.99
% 76.95/76.99 cnf(a_LE_b,hypothesis,
% 76.95/76.99 less_equal(a,b) ).
% 76.95/76.99
% 76.95/76.99 cnf(prove_a_divide_c_LE_b_divide_c,negated_conjecture,
% 76.95/76.99 ~ less_equal(divide(a,c),divide(b,c)) ).
% 76.95/76.99
% 76.95/76.99 %--------------------------------------------------------------------------
% 76.95/76.99 %-------------------------------------------
% 76.95/76.99 % Proof found
% 76.95/76.99 % SZS status Theorem for theBenchmark
% 76.95/76.99 % SZS output start Proof
% 76.95/76.99 %ClaNum:23(EqnAxiom:7)
% 76.95/76.99 %VarNum:48(SingletonVarNum:25)
% 76.95/76.99 %MaxLitNum:3
% 76.95/76.99 %MaxfuncDepth:2
% 76.95/76.99 %SharedTerms:11
% 76.95/76.99 %goalClause: 17
% 76.95/76.99 %singleGoalClaCount:1
% 76.95/76.99 [9]P1(a1,a4)
% 76.95/76.99 [8]E(f3(a1,a2),a1)
% 76.95/76.99 [17]~P1(f3(a1,a5),f3(a4,a5))
% 76.95/76.99 [12]P1(x121,a6)
% 76.95/76.99 [13]P1(a2,x131)
% 76.95/76.99 [10]E(f3(x101,a6),a2)
% 76.95/76.99 [11]E(f3(a2,x111),a2)
% 76.95/76.99 [14]E(f3(x141,x141),a2)
% 76.95/76.99 [15]P1(f3(x151,x152),x151)
% 76.95/76.99 [16]P1(f3(f3(x161,x162),f3(x163,x162)),f3(f3(x161,x163),x162))
% 76.95/76.99 [18]~P1(x181,x182)+E(f3(x181,x182),a2)
% 76.95/76.99 [19]P1(x191,x192)+~E(f3(x191,x192),a2)
% 76.95/76.99 [22]~P1(x223,x222)+P1(f3(x221,x222),f3(x221,x223))
% 76.95/76.99 [23]~P1(f3(x231,x233),x232)+P1(f3(x231,x232),x233)
% 76.95/76.99 [20]~P1(x202,x201)+~P1(x201,x202)+E(x201,x202)
% 76.95/76.99 [21]~P1(x211,x213)+P1(x211,x212)+~P1(x213,x212)
% 76.95/76.99 %EqnAxiom
% 76.95/76.99 [1]E(x11,x11)
% 76.95/76.99 [2]E(x22,x21)+~E(x21,x22)
% 76.95/76.99 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 76.95/76.99 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 76.95/76.99 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 76.95/76.99 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 76.95/76.99 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 76.95/76.99
% 76.95/76.99 %-------------------------------------------
% 76.95/77.01 cnf(24,plain,
% 76.95/77.01 (P1(x241,x241)),
% 76.95/77.01 inference(scs_inference,[],[14,19])).
% 76.95/77.01 cnf(26,plain,
% 76.95/77.01 (~P1(f3(a1,f3(a4,a5)),a5)),
% 76.95/77.01 inference(scs_inference,[],[17,14,19,23])).
% 76.95/77.01 cnf(28,plain,
% 76.95/77.01 (E(a2,f3(x281,x281))),
% 76.95/77.01 inference(scs_inference,[],[17,14,19,23,2])).
% 76.95/77.01 cnf(29,plain,
% 76.95/77.01 (~E(a2,f3(a1,a5))),
% 76.95/77.01 inference(scs_inference,[],[17,13,14,19,23,2,6])).
% 76.95/77.01 cnf(30,plain,
% 76.95/77.01 (P1(a2,x301)),
% 76.95/77.01 inference(rename_variables,[],[13])).
% 76.95/77.01 cnf(31,plain,
% 76.95/77.01 (~P1(f3(a1,a5),a2)),
% 76.95/77.01 inference(scs_inference,[],[17,13,30,14,19,23,2,6,20])).
% 76.95/77.01 cnf(34,plain,
% 76.95/77.01 (~E(a6,f3(a4,a5))),
% 76.95/77.01 inference(scs_inference,[],[17,12,13,30,14,19,23,2,6,20,7])).
% 76.95/77.01 cnf(36,plain,
% 76.95/77.01 (E(x361,a1)+~E(x361,f3(a1,a2))),
% 76.95/77.01 inference(scs_inference,[],[17,12,13,30,14,8,19,23,2,6,20,7,3])).
% 76.95/77.01 cnf(38,plain,
% 76.95/77.01 (~P1(f3(a1,a2),a5)),
% 76.95/77.01 inference(scs_inference,[],[31,23])).
% 76.95/77.01 cnf(40,plain,
% 76.95/77.01 (E(a2,f3(x401,a6))),
% 76.95/77.01 inference(scs_inference,[],[31,10,23,2])).
% 76.95/77.01 cnf(41,plain,
% 76.95/77.01 (E(f3(x411,a6),f3(x412,x412))),
% 76.95/77.01 inference(scs_inference,[],[28,31,10,23,2,3])).
% 76.95/77.01 cnf(42,plain,
% 76.95/77.01 (~E(f3(a4,a5),f3(a1,a5))),
% 76.95/77.01 inference(scs_inference,[],[17,24,28,31,10,23,2,3,6])).
% 76.95/77.01 cnf(43,plain,
% 76.95/77.01 (P1(x431,x431)),
% 76.95/77.01 inference(rename_variables,[],[24])).
% 76.95/77.01 cnf(44,plain,
% 76.95/77.01 (~E(f3(a1,a5),f3(a4,a5))),
% 76.95/77.01 inference(scs_inference,[],[17,24,43,28,31,10,23,2,3,6,7])).
% 76.95/77.01 cnf(46,plain,
% 76.95/77.01 (~E(a4,a1)),
% 76.95/77.01 inference(scs_inference,[],[17,24,43,28,31,10,23,2,3,6,7,4])).
% 76.95/77.01 cnf(47,plain,
% 76.95/77.01 (E(f3(f3(x471,x472),f3(x473,x472)),f3(f3(x471,x473),x472))+~P1(f3(f3(x471,x473),x472),f3(f3(x471,x472),f3(x473,x472)))),
% 76.95/77.01 inference(scs_inference,[],[17,24,43,16,28,31,10,23,2,3,6,7,4,20])).
% 76.95/77.01 cnf(49,plain,
% 76.95/77.01 (~E(a4,f3(a1,a2))),
% 76.95/77.01 inference(scs_inference,[],[17,24,43,16,28,31,10,23,2,3,6,7,4,20,36])).
% 76.95/77.01 cnf(51,plain,
% 76.95/77.01 (E(a2,f3(a2,x511))),
% 76.95/77.01 inference(scs_inference,[],[11,44,4,2])).
% 76.95/77.01 cnf(52,plain,
% 76.95/77.01 (~P1(a4,a1)),
% 76.95/77.01 inference(scs_inference,[],[11,44,9,4,2,20])).
% 76.95/77.01 cnf(54,plain,
% 76.95/77.01 (~E(f3(f3(a4,a5),x541),f3(a1,a5))),
% 76.95/77.01 inference(scs_inference,[],[17,15,11,44,9,4,2,20,6])).
% 76.95/77.01 cnf(55,plain,
% 76.95/77.01 (P1(f3(x551,x552),x551)),
% 76.95/77.01 inference(rename_variables,[],[15])).
% 76.95/77.01 cnf(56,plain,
% 76.95/77.01 (~E(a1,f3(a4,a5))),
% 76.95/77.01 inference(scs_inference,[],[17,15,55,11,44,9,4,2,20,6,7])).
% 76.95/77.01 cnf(58,plain,
% 76.95/77.01 (E(f3(a2,x581),f3(x582,a6))),
% 76.95/77.01 inference(scs_inference,[],[17,15,55,11,44,40,9,4,2,20,6,7,3])).
% 76.95/77.01 cnf(61,plain,
% 76.95/77.01 (E(f3(x611,x611),f3(x612,a6))),
% 76.95/77.01 inference(scs_inference,[],[54,41,4,2])).
% 76.95/77.01 cnf(62,plain,
% 76.95/77.01 (E(f3(x621,x621),f3(a2,x622))),
% 76.95/77.01 inference(scs_inference,[],[54,14,41,51,4,2,3])).
% 76.95/77.01 cnf(63,plain,
% 76.95/77.01 (~E(f3(a4,a5),f3(a1,a2))),
% 76.95/77.01 inference(scs_inference,[],[54,14,41,51,4,2,3,36])).
% 76.95/77.01 cnf(64,plain,
% 76.95/77.01 (P1(x641,a4)+~E(a1,x641)),
% 76.95/77.01 inference(scs_inference,[],[54,14,41,51,9,4,2,3,36,6])).
% 76.95/77.01 cnf(69,plain,
% 76.95/77.01 (E(f3(a2,x691),f3(x692,x692))),
% 76.95/77.01 inference(scs_inference,[],[62,2])).
% 76.95/77.01 cnf(70,plain,
% 76.95/77.01 (P1(f3(f3(x701,a6),f3(x702,a6)),a2)),
% 76.95/77.01 inference(scs_inference,[],[16,10,62,2,7])).
% 76.95/77.01 cnf(72,plain,
% 76.95/77.01 (E(f3(x721,a6),a2)),
% 76.95/77.01 inference(rename_variables,[],[10])).
% 76.95/77.01 cnf(73,plain,
% 76.95/77.01 (E(f3(x731,a6),f3(x732,a6))),
% 76.95/77.01 inference(scs_inference,[],[16,10,72,62,40,2,7,3])).
% 76.95/77.01 cnf(74,plain,
% 76.95/77.01 (E(f3(f3(x741,a6),f3(x742,a6)),a2)),
% 76.95/77.01 inference(scs_inference,[],[16,10,72,13,62,40,2,7,3,20])).
% 76.95/77.01 cnf(78,plain,
% 76.95/77.01 (P1(f3(x781,a6),f3(x782,a6))),
% 76.95/77.01 inference(scs_inference,[],[16,10,72,31,13,62,40,2,7,3,20,6,19])).
% 76.95/77.01 cnf(80,plain,
% 76.95/77.01 (E(f3(x801,a6),f3(a2,x802))),
% 76.95/77.01 inference(scs_inference,[],[58,2])).
% 76.95/77.01 cnf(81,plain,
% 76.95/77.01 (P1(f3(x811,a6),a2)),
% 76.95/77.01 inference(scs_inference,[],[78,11,58,2,7])).
% 76.95/77.01 cnf(83,plain,
% 76.95/77.01 (E(f3(a2,x831),a2)),
% 76.95/77.01 inference(rename_variables,[],[11])).
% 76.95/77.01 cnf(84,plain,
% 76.95/77.01 (E(f3(a2,x841),f3(a2,x842))),
% 76.95/77.01 inference(scs_inference,[],[78,11,83,58,51,2,7,3])).
% 76.95/77.01 cnf(85,plain,
% 76.95/77.01 (~E(f3(x851,a6),f3(a1,a5))),
% 76.95/77.01 inference(scs_inference,[],[78,11,83,31,58,51,2,7,3,6])).
% 76.95/77.01 cnf(86,plain,
% 76.95/77.01 (~E(a6,a5)),
% 76.95/77.01 inference(scs_inference,[],[78,11,83,31,58,51,2,7,3,6,5])).
% 76.95/77.01 cnf(87,plain,
% 76.95/77.01 (E(a2,f3(f3(x871,a6),f3(x872,a6)))),
% 76.95/77.01 inference(scs_inference,[],[74,2])).
% 76.95/77.01 cnf(88,plain,
% 76.95/77.01 (~P1(f3(a1,a5),f3(f3(a1,a5),a6))),
% 76.95/77.01 inference(scs_inference,[],[85,15,74,2,20])).
% 76.95/77.01 cnf(93,plain,
% 76.95/77.01 (E(f3(x931,x931),f3(x932,x932))),
% 76.95/77.01 inference(scs_inference,[],[85,15,14,70,74,28,2,20,7,3])).
% 76.95/77.01 cnf(96,plain,
% 76.95/77.01 (E(a1,f3(a1,a2))),
% 76.95/77.01 inference(scs_inference,[],[8,2])).
% 76.95/77.01 cnf(97,plain,
% 76.95/77.01 (P1(f3(a1,a2),a4)),
% 76.95/77.01 inference(scs_inference,[],[9,8,2,6])).
% 76.95/77.01 cnf(98,plain,
% 76.95/77.01 (P1(f3(x981,a6),f3(f3(x982,a6),f3(x983,a6)))),
% 76.95/77.01 inference(scs_inference,[],[9,87,81,8,2,6,7])).
% 76.95/77.01 cnf(99,plain,
% 76.95/77.01 (E(f3(x991,a6),f3(f3(x992,a6),f3(x993,a6)))),
% 76.95/77.01 inference(scs_inference,[],[9,10,87,81,8,2,6,7,3])).
% 76.95/77.01 cnf(100,plain,
% 76.95/77.01 (E(f3(a1,a2),a4)+~P1(a4,f3(a1,a2))),
% 76.95/77.01 inference(scs_inference,[],[9,10,87,81,8,2,6,7,3,20])).
% 76.95/77.01 cnf(102,plain,
% 76.95/77.01 (E(f3(f3(x1021,a6),f3(x1022,a6)),f3(x1023,a6))),
% 76.95/77.01 inference(scs_inference,[],[99,2])).
% 76.95/77.01 cnf(103,plain,
% 76.95/77.01 (~E(a4,a5)),
% 76.95/77.01 inference(scs_inference,[],[38,97,99,2,7])).
% 76.95/77.01 cnf(104,plain,
% 76.95/77.01 (E(f3(x1041,x1041),f3(f3(x1042,a6),f3(x1043,a6)))),
% 76.95/77.01 inference(scs_inference,[],[38,97,93,99,2,7,3])).
% 76.95/77.01 cnf(107,plain,
% 76.95/77.01 (E(f3(f3(x1071,a6),f3(x1072,a6)),f3(x1073,x1073))),
% 76.95/77.01 inference(scs_inference,[],[104,2])).
% 76.95/77.01 cnf(109,plain,
% 76.95/77.01 (E(f3(a2,x1091),f3(f3(x1092,a6),f3(x1093,a6)))),
% 76.95/77.01 inference(scs_inference,[],[11,104,70,87,2,7,3])).
% 76.95/77.01 cnf(110,plain,
% 76.95/77.01 (E(f3(f3(x1101,a6),f3(x1102,a6)),f3(a2,x1103))),
% 76.95/77.01 inference(scs_inference,[],[109,2])).
% 76.95/77.01 cnf(112,plain,
% 76.95/77.01 (E(f3(f3(x1121,a6),f3(x1122,a6)),f3(f3(x1123,a6),f3(x1124,a6)))),
% 76.95/77.01 inference(scs_inference,[],[107,109,70,40,2,7,3])).
% 76.95/77.01 cnf(117,plain,
% 76.95/77.01 (P1(a1,x1171)+~E(a4,x1171)),
% 76.95/77.01 inference(scs_inference,[],[9,7])).
% 76.95/77.01 cnf(119,plain,
% 76.95/77.01 (E(f3(f3(x1191,f3(x1191,x1192)),x1192),a2)),
% 76.95/77.01 inference(scs_inference,[],[24,18,23])).
% 76.95/77.01 cnf(120,plain,
% 76.95/77.01 (P1(f3(x1201,f3(x1201,x1202)),x1202)),
% 76.95/77.01 inference(scs_inference,[],[119,19])).
% 76.95/77.01 cnf(122,plain,
% 76.95/77.01 (E(a2,f3(f3(x1221,f3(x1221,x1222)),x1222))),
% 76.95/77.01 inference(scs_inference,[],[119,19,2])).
% 76.95/77.01 cnf(130,plain,
% 76.95/77.01 (P1(f3(x1301,a4),f3(x1301,f3(a1,a2)))),
% 76.95/77.01 inference(scs_inference,[],[96,22,64])).
% 76.95/77.01 cnf(132,plain,
% 76.95/77.01 (P1(f3(x1321,f3(x1321,x1322)),x1322)),
% 76.95/77.01 inference(rename_variables,[],[120])).
% 76.95/77.01 cnf(134,plain,
% 76.95/77.01 (P1(f3(x1341,f3(x1341,f3(a1,a2))),a1)),
% 76.95/77.01 inference(scs_inference,[],[8,17,120,132,14,122,6,3,7])).
% 76.95/77.01 cnf(136,plain,
% 76.95/77.01 (~E(f3(a1,f3(a4,a5)),a5)),
% 76.95/77.01 inference(scs_inference,[],[8,17,120,132,14,122,6,3,7,5])).
% 76.95/77.01 cnf(138,plain,
% 76.95/77.01 (E(f3(x1381,a4),f3(x1381,f3(a1,a2)))+~P1(f3(x1381,f3(a1,a2)),f3(x1381,a4))),
% 76.95/77.01 inference(scs_inference,[],[8,17,120,132,14,130,122,6,3,7,5,2,20])).
% 76.95/77.01 cnf(141,plain,
% 76.95/77.01 (~E(f3(x1411,f3(x1411,f3(a1,a2))),a4)),
% 76.95/77.01 inference(scs_inference,[],[52,134,6])).
% 76.95/77.01 cnf(144,plain,
% 76.95/77.01 (E(f3(x1441,f3(x1441,f3(a1,a2))),a1)+~P1(a1,f3(x1441,f3(x1441,f3(a1,a2))))),
% 76.95/77.01 inference(scs_inference,[],[10,52,134,122,6,3,2,20])).
% 76.95/77.01 cnf(146,plain,
% 76.95/77.01 (~P1(a4,f3(a1,a2))),
% 76.95/77.01 inference(scs_inference,[],[49,100,2])).
% 76.95/77.01 cnf(150,plain,
% 76.95/77.01 (P1(f3(f3(a1,a2),a4),a2)),
% 76.95/77.01 inference(scs_inference,[],[14,130,7])).
% 76.95/77.01 cnf(153,plain,
% 76.95/77.01 (E(f3(f3(a1,a2),a4),a2)),
% 76.95/77.01 inference(scs_inference,[],[14,13,130,7,20])).
% 76.95/77.01 cnf(156,plain,
% 76.95/77.01 (~E(f3(f3(a1,a2),a4),f3(a1,a5))),
% 76.95/77.01 inference(scs_inference,[],[14,13,31,130,7,20,6])).
% 76.95/77.01 cnf(157,plain,
% 76.95/77.01 (E(x1571,a2)+~E(x1571,f3(f3(a1,a2),a4))),
% 76.95/77.01 inference(scs_inference,[],[14,13,31,130,7,20,6,3])).
% 76.95/77.01 cnf(158,plain,
% 76.95/77.01 (~E(a4,f3(f3(a1,a2),a4))+P1(a1,a2)),
% 76.95/77.01 inference(scs_inference,[],[14,13,31,130,7,20,6,3,117])).
% 76.95/77.01 cnf(162,plain,
% 76.95/77.01 (E(a2,f3(f3(a1,a2),a4))),
% 76.95/77.01 inference(scs_inference,[],[153,2])).
% 76.95/77.01 cnf(163,plain,
% 76.95/77.01 (E(f3(x1631,a6),f3(f3(a1,a2),a4))),
% 76.95/77.01 inference(scs_inference,[],[10,153,2,3])).
% 76.95/77.01 cnf(164,plain,
% 76.95/77.01 (P1(f3(f3(a1,a2),a4),f3(x1641,a6))),
% 76.95/77.01 inference(scs_inference,[],[10,40,153,150,2,3,7])).
% 76.95/77.01 cnf(165,plain,
% 76.95/77.01 (~E(f3(f3(a1,a2),a4),a4)+P1(a1,a2)),
% 76.95/77.01 inference(scs_inference,[],[158,2])).
% 76.95/77.01 cnf(166,plain,
% 76.95/77.01 (E(f3(f3(a1,a2),a4),f3(x1661,a6))),
% 76.95/77.01 inference(scs_inference,[],[163,2])).
% 76.95/77.01 cnf(167,plain,
% 76.95/77.01 (E(f3(a2,x1671),f3(f3(a1,a2),a4))),
% 76.95/77.01 inference(scs_inference,[],[11,162,163,2,3])).
% 76.95/77.01 cnf(169,plain,
% 76.95/77.01 (~E(f3(x1691,a6),a4)+P1(a1,a2)),
% 76.95/77.01 inference(scs_inference,[],[166,165,3])).
% 76.95/77.01 cnf(170,plain,
% 76.95/77.01 (E(f3(f3(a1,a2),a4),f3(a2,x1701))),
% 76.95/77.01 inference(scs_inference,[],[167,2])).
% 76.95/77.01 cnf(171,plain,
% 76.95/77.01 (E(f3(f3(x1711,a6),f3(x1712,a6)),f3(f3(a1,a2),a4))),
% 76.95/77.01 inference(scs_inference,[],[102,167,2,3])).
% 76.95/77.01 cnf(174,plain,
% 76.95/77.01 (P1(f3(f3(a1,a2),a4),f3(x1741,x1741))),
% 76.95/77.01 inference(scs_inference,[],[102,28,167,150,2,3,7])).
% 76.95/77.01 cnf(175,plain,
% 76.95/77.01 (~E(a4,f3(x1751,a6))+P1(a1,a2)),
% 76.95/77.01 inference(scs_inference,[],[169,2])).
% 76.95/77.01 cnf(176,plain,
% 76.95/77.01 (E(f3(f3(a1,a2),a4),f3(f3(x1761,a6),f3(x1762,a6)))),
% 76.95/77.01 inference(scs_inference,[],[171,2])).
% 76.95/77.01 cnf(178,plain,
% 76.95/77.01 (P1(f3(f3(a1,a2),a4),f3(f3(x1781,a6),f3(x1782,a6)))),
% 76.95/77.01 inference(scs_inference,[],[87,174,171,170,150,2,6,7])).
% 76.95/77.01 cnf(179,plain,
% 76.95/77.01 (~P1(a4,f3(a4,a6))+P1(a1,a2)),
% 76.95/77.01 inference(scs_inference,[],[15,175,20])).
% 76.95/77.01 cnf(180,plain,
% 76.95/77.01 (P1(a1,a2)+~E(f3(a4,f3(a4,a6)),a2)),
% 76.95/77.01 inference(scs_inference,[],[179,19])).
% 76.95/77.01 cnf(181,plain,
% 76.95/77.01 (P1(f3(x1811,f3(x1811,f3(x1812,a6))),a2)),
% 76.95/77.01 inference(scs_inference,[],[120,10,7])).
% 76.95/77.01 cnf(183,plain,
% 76.95/77.01 (E(f3(x1831,f3(x1831,f3(x1832,a6))),a2)),
% 76.95/77.01 inference(scs_inference,[],[120,10,13,7,20])).
% 76.95/77.01 cnf(187,plain,
% 76.95/77.01 (P1(x1871,f3(x1871,f3(x1872,a6)))),
% 76.95/77.01 inference(scs_inference,[],[120,10,13,31,7,20,6,19])).
% 76.95/77.01 cnf(190,plain,
% 76.95/77.01 (E(a2,f3(a1,f3(a1,f3(x1901,a6))))),
% 76.95/77.01 inference(scs_inference,[],[120,10,13,31,7,20,6,19,5,2])).
% 76.95/77.01 cnf(191,plain,
% 76.95/77.01 (E(f3(x1911,a6),f3(a1,f3(a1,f3(x1911,a6))))),
% 76.95/77.01 inference(scs_inference,[],[120,10,13,31,7,20,6,19,5,2,3])).
% 76.95/77.01 cnf(192,plain,
% 76.95/77.01 (~E(f3(a4,f3(a4,a6)),f3(f3(a1,a2),a4))+P1(a1,a2)),
% 76.95/77.01 inference(scs_inference,[],[180,157])).
% 76.95/77.01 cnf(194,plain,
% 76.95/77.01 (P1(a1,f3(a4,f3(x1941,a6)))),
% 76.95/77.01 inference(scs_inference,[],[9,187,191,2,21])).
% 76.95/77.01 cnf(195,plain,
% 76.95/77.01 (P1(x1951,f3(x1951,f3(x1952,a6)))),
% 76.95/77.01 inference(rename_variables,[],[187])).
% 76.95/77.01 cnf(197,plain,
% 76.95/77.01 (E(a6,f3(a6,f3(a6,a6)))),
% 76.95/77.02 inference(scs_inference,[],[9,120,187,195,191,2,21,20])).
% 76.95/77.02 cnf(199,plain,
% 76.95/77.02 (P1(f3(x1991,f3(x1991,x1992)),x1992)),
% 76.95/77.02 inference(rename_variables,[],[120])).
% 76.95/77.02 cnf(202,plain,
% 76.95/77.02 (E(f3(a2,x2021),f3(a1,f3(a1,f3(x2022,a6))))),
% 76.95/77.02 inference(scs_inference,[],[9,120,187,195,11,96,191,190,2,21,20,6,3])).
% 76.95/77.02 cnf(203,plain,
% 76.95/77.02 (P1(f3(x2031,f3(x2031,f3(a2,x2032))),a2)),
% 76.95/77.02 inference(scs_inference,[],[9,120,199,187,195,11,96,191,190,2,21,20,6,3,7])).
% 76.95/77.02 cnf(207,plain,
% 76.95/77.02 (E(f3(x2071,f3(x2071,f3(a2,x2072))),a2)),
% 76.95/77.02 inference(scs_inference,[],[13,202,203,2,20])).
% 76.95/77.02 cnf(211,plain,
% 76.95/77.02 (E(f3(x2111,a6),f3(a1,f3(a1,f3(x2112,a6))))),
% 76.95/77.02 inference(scs_inference,[],[10,13,31,202,203,190,2,20,6,3])).
% 76.95/77.02 cnf(212,plain,
% 76.95/77.02 (~E(f3(f3(a1,a5),f3(x2121,a6)),f3(a4,a5))),
% 76.95/77.02 inference(scs_inference,[],[17,187,10,13,31,202,203,190,2,20,6,3,7])).
% 76.95/77.02 cnf(214,plain,
% 76.95/77.02 (P1(x2141,f3(x2141,f3(a2,x2142)))),
% 76.95/77.02 inference(scs_inference,[],[17,187,10,13,31,202,203,190,2,20,6,3,7,19])).
% 76.95/77.02 cnf(219,plain,
% 76.95/77.02 (P1(a1,f3(a4,f3(a2,x2191)))),
% 76.95/77.02 inference(scs_inference,[],[9,214,211,2,21])).
% 76.95/77.02 cnf(220,plain,
% 76.95/77.02 (P1(x2201,f3(x2201,f3(a2,x2202)))),
% 76.95/77.02 inference(rename_variables,[],[214])).
% 76.95/77.02 cnf(223,plain,
% 76.95/77.02 (~E(f3(f3(a1,a5),f3(a2,x2231)),f3(a4,a5))),
% 76.95/77.02 inference(scs_inference,[],[9,17,214,220,96,211,2,21,6,7])).
% 76.95/77.02 cnf(230,plain,
% 76.95/77.02 (E(a2,f3(x2301,f3(x2301,f3(x2302,a6))))),
% 76.95/77.02 inference(scs_inference,[],[183,2])).
% 76.95/77.02 cnf(231,plain,
% 76.95/77.02 (E(f3(a2,x2311),f3(x2312,f3(x2312,f3(x2313,a6))))),
% 76.95/77.02 inference(scs_inference,[],[11,183,2,3])).
% 76.95/77.02 cnf(235,plain,
% 76.95/77.02 (E(a2,f3(x2351,f3(x2351,f3(a2,x2352))))),
% 76.95/77.02 inference(scs_inference,[],[207,2])).
% 76.95/77.02 cnf(236,plain,
% 76.95/77.02 (E(f3(x2361,a6),f3(x2362,f3(x2362,f3(x2363,a6))))),
% 76.95/77.02 inference(scs_inference,[],[10,207,230,2,3])).
% 76.95/77.02 cnf(240,plain,
% 76.95/77.02 (E(f3(a6,f3(a6,a6)),a6)),
% 76.95/77.02 inference(scs_inference,[],[197,2])).
% 76.95/77.02 cnf(241,plain,
% 76.95/77.02 (E(f3(a2,x2411),f3(x2412,f3(x2412,f3(a2,x2413))))),
% 76.95/77.02 inference(scs_inference,[],[11,197,235,2,3])).
% 76.95/77.02 cnf(247,plain,
% 76.95/77.02 (E(f3(x2471,a6),f3(x2472,f3(x2472,f3(a2,x2473))))),
% 76.95/77.02 inference(scs_inference,[],[10,231,235,2,3])).
% 76.95/77.02 cnf(250,plain,
% 76.95/77.02 (P1(f3(x2501,f3(x2501,f3(x2502,a6))),f3(x2503,x2503))),
% 76.95/77.02 inference(scs_inference,[],[28,181,236,2,7])).
% 76.95/77.02 cnf(252,plain,
% 76.95/77.02 (P1(a1,x2521)+~E(f3(a4,f3(x2522,a6)),x2521)),
% 76.95/77.02 inference(scs_inference,[],[194,241,2,7])).
% 76.95/77.02 cnf(257,plain,
% 76.95/77.02 (P1(a1,x2571)+~E(f3(a4,f3(a2,x2572)),x2571)),
% 76.95/77.02 inference(scs_inference,[],[219,247,2,7])).
% 76.95/77.02 cnf(262,plain,
% 76.95/77.02 (~E(f3(f3(a1,a2),a4),f3(a4,f3(a4,a6)))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[192,2])).
% 76.95/77.02 cnf(264,plain,
% 76.95/77.02 (P1(x2641,f3(a6,f3(a2,x2642)))),
% 76.95/77.02 inference(scs_inference,[],[12,214,21])).
% 76.95/77.02 cnf(265,plain,
% 76.95/77.02 (P1(x2651,f3(x2651,f3(a2,x2652)))),
% 76.95/77.02 inference(rename_variables,[],[214])).
% 76.95/77.02 cnf(267,plain,
% 76.95/77.02 (E(a6,f3(a6,f3(a2,x2671)))),
% 76.95/77.02 inference(scs_inference,[],[12,214,265,21,20])).
% 76.95/77.02 cnf(271,plain,
% 76.95/77.02 (E(f3(a6,f3(a6,a6)),f3(a6,f3(a2,x2711)))),
% 76.95/77.02 inference(scs_inference,[],[12,214,265,240,21,20,3])).
% 76.95/77.02 cnf(272,plain,
% 76.95/77.02 (E(f3(a6,f3(a2,x2721)),a6)),
% 76.95/77.02 inference(scs_inference,[],[12,214,265,240,21,20,3,2])).
% 76.95/77.02 cnf(275,plain,
% 76.95/77.02 (P1(x2751,f3(a6,f3(x2752,a6)))),
% 76.95/77.02 inference(scs_inference,[],[12,187,271,2,21])).
% 76.95/77.02 cnf(276,plain,
% 76.95/77.02 (P1(x2761,f3(x2761,f3(x2762,a6)))),
% 76.95/77.02 inference(rename_variables,[],[187])).
% 76.95/77.02 cnf(278,plain,
% 76.95/77.02 (E(a6,f3(a6,f3(x2781,a6)))),
% 76.95/77.02 inference(scs_inference,[],[12,187,276,271,2,21,20])).
% 76.95/77.02 cnf(283,plain,
% 76.95/77.02 (~E(f3(a6,f3(a2,x2831)),f3(a4,a5))),
% 76.95/77.02 inference(scs_inference,[],[12,187,276,17,264,271,267,272,2,21,20,3,7])).
% 76.95/77.02 cnf(288,plain,
% 76.95/77.02 (~E(f3(a6,f3(x2881,a6)),f3(a4,a5))),
% 76.95/77.02 inference(scs_inference,[],[17,275,278,240,2,3,7])).
% 76.95/77.02 cnf(295,plain,
% 76.95/77.02 (~E(a2,f3(a4,f3(a4,a6)))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[153,262,3])).
% 76.95/77.02 cnf(296,plain,
% 76.95/77.02 (~P1(f3(a4,f3(a4,a6)),a2)+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[13,295,20])).
% 76.95/77.02 cnf(297,plain,
% 76.95/77.02 (~P1(f3(a4,a2),f3(a4,a6))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[296,23])).
% 76.95/77.02 cnf(298,plain,
% 76.95/77.02 (E(f3(x2981,x2981),f3(f3(a1,a2),a4))),
% 76.95/77.02 inference(scs_inference,[],[14,162,3])).
% 76.95/77.02 cnf(301,plain,
% 76.95/77.02 (E(f3(f3(a1,a2),a4),f3(x3011,x3011))),
% 76.95/77.02 inference(scs_inference,[],[14,120,162,3,7,2])).
% 76.95/77.02 cnf(303,plain,
% 76.95/77.02 (~E(f3(a1,f3(x3031,x3031)),a5)),
% 76.95/77.02 inference(scs_inference,[],[14,120,31,162,3,7,2,6,5])).
% 76.95/77.02 cnf(304,plain,
% 76.95/77.02 (E(f3(a1,f3(a1,f3(x3041,x3041))),a2)),
% 76.95/77.02 inference(scs_inference,[],[14,120,13,31,162,3,7,2,6,5,20])).
% 76.95/77.02 cnf(307,plain,
% 76.95/77.02 (~P1(a6,a2)+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[297,22])).
% 76.95/77.02 cnf(308,plain,
% 76.95/77.02 (P1(a1,f3(a1,f3(x3081,x3081)))),
% 76.95/77.02 inference(scs_inference,[],[304,19])).
% 76.95/77.02 cnf(310,plain,
% 76.95/77.02 (E(a2,f3(a1,f3(a1,f3(x3101,x3101))))),
% 76.95/77.02 inference(scs_inference,[],[304,19,2])).
% 76.95/77.02 cnf(311,plain,
% 76.95/77.02 (E(a1,f3(a1,f3(a1,a1)))),
% 76.95/77.02 inference(scs_inference,[],[120,304,19,2,20])).
% 76.95/77.02 cnf(314,plain,
% 76.95/77.02 (P1(f3(a1,a2),f3(a1,f3(a1,a1)))),
% 76.95/77.02 inference(scs_inference,[],[120,96,304,19,2,20,6])).
% 76.95/77.02 cnf(315,plain,
% 76.95/77.02 (E(f3(x3151,x3151),f3(x3152,f3(x3152,f3(x3153,a6))))),
% 76.95/77.02 inference(scs_inference,[],[14,120,96,230,304,19,2,20,6,3])).
% 76.95/77.02 cnf(316,plain,
% 76.95/77.02 (P1(f3(a1,f3(a1,a1)),a4)),
% 76.95/77.02 inference(scs_inference,[],[14,120,96,230,304,19,2,20,6,3,64])).
% 76.95/77.02 cnf(319,plain,
% 76.95/77.02 (P1(a1,a2)+~E(f3(a6,a2),a2)),
% 76.95/77.02 inference(scs_inference,[],[307,19])).
% 76.95/77.02 cnf(321,plain,
% 76.95/77.02 (P1(f3(a1,a2),f3(a1,f3(x3211,x3211)))),
% 76.95/77.02 inference(scs_inference,[],[308,96,315,2,6])).
% 76.95/77.02 cnf(322,plain,
% 76.95/77.02 (E(f3(x3221,x3221),f3(x3222,f3(x3222,f3(a2,x3223))))),
% 76.95/77.02 inference(scs_inference,[],[14,308,96,235,315,2,6,3])).
% 76.95/77.02 cnf(325,plain,
% 76.95/77.02 (P1(a1,x3251)+~E(f3(a1,f3(x3252,x3252)),x3251)),
% 76.95/77.02 inference(scs_inference,[],[14,308,314,96,235,315,2,6,3,20,7])).
% 76.95/77.02 cnf(327,plain,
% 76.95/77.02 (~E(f3(a6,a2),f3(f3(a1,a2),a4))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[319,157])).
% 76.95/77.02 cnf(328,plain,
% 76.95/77.02 (E(f3(a1,f3(a1,a1)),a1)),
% 76.95/77.02 inference(scs_inference,[],[311,2])).
% 76.95/77.02 cnf(329,plain,
% 76.95/77.02 (E(f3(a1,a2),f3(a1,f3(a1,a1)))),
% 76.95/77.02 inference(scs_inference,[],[8,311,2,3])).
% 76.95/77.02 cnf(330,plain,
% 76.95/77.02 (E(f3(a1,f3(a1,a1)),a4)+~P1(a4,f3(a1,f3(a1,a1)))),
% 76.95/77.02 inference(scs_inference,[],[316,8,311,2,3,20])).
% 76.95/77.02 cnf(332,plain,
% 76.95/77.02 (P1(f3(a1,f3(a1,a1)),x3321)+~E(a4,x3321)),
% 76.95/77.02 inference(scs_inference,[],[316,8,311,2,3,20,7])).
% 76.95/77.02 cnf(334,plain,
% 76.95/77.02 (~E(f3(f3(a1,a2),a4),f3(a6,a2))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[327,2])).
% 76.95/77.02 cnf(335,plain,
% 76.95/77.02 (E(f3(a1,f3(a1,a1)),f3(a1,a2))),
% 76.95/77.02 inference(scs_inference,[],[329,2])).
% 76.95/77.02 cnf(336,plain,
% 76.95/77.02 (~E(a4,f3(a1,f3(a1,a1)))),
% 76.95/77.02 inference(scs_inference,[],[46,329,328,2,3])).
% 76.95/77.02 cnf(337,plain,
% 76.95/77.02 (E(f3(a1,a2),f3(a1,f3(x3371,x3371)))+~P1(f3(a1,f3(x3371,x3371)),f3(a1,a2))),
% 76.95/77.02 inference(scs_inference,[],[321,46,329,328,2,3,20])).
% 76.95/77.02 cnf(339,plain,
% 76.95/77.02 (~E(a2,f3(a6,a2))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[153,334,3])).
% 76.95/77.02 cnf(342,plain,
% 76.95/77.02 (P1(a1,f3(a1,a2))),
% 76.95/77.02 inference(scs_inference,[],[308,63,335,322,2,3,7])).
% 76.95/77.02 cnf(344,plain,
% 76.95/77.02 (~P1(f3(a6,a2),a2)+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[13,339,20])).
% 76.95/77.02 cnf(347,plain,
% 76.95/77.02 (P1(a1,a2)+~E(f3(f3(a6,a2),a2),a2)),
% 76.95/77.02 inference(scs_inference,[],[344,19])).
% 76.95/77.02 cnf(348,plain,
% 76.95/77.02 (~E(f3(f3(a6,a2),a2),f3(f3(a1,a2),a4))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[347,157])).
% 76.95/77.02 cnf(349,plain,
% 76.95/77.02 (P1(f3(x3491,x3492),f3(x3491,f3(a2,x3493)))),
% 76.95/77.02 inference(scs_inference,[],[15,214,21])).
% 76.95/77.02 cnf(350,plain,
% 76.95/77.02 (P1(x3501,f3(x3501,f3(a2,x3502)))),
% 76.95/77.02 inference(rename_variables,[],[214])).
% 76.95/77.02 cnf(352,plain,
% 76.95/77.02 (E(x3521,f3(x3521,f3(a2,x3522)))),
% 76.95/77.02 inference(scs_inference,[],[15,214,350,21,20])).
% 76.95/77.02 cnf(356,plain,
% 76.95/77.02 (E(f3(a2,x3561),f3(a1,f3(a1,f3(x3562,x3562))))),
% 76.95/77.02 inference(scs_inference,[],[15,214,350,11,310,21,20,3])).
% 76.95/77.02 cnf(357,plain,
% 76.95/77.02 (P1(a1,f3(f3(a4,f3(x3571,a6)),f3(a2,x3572)))),
% 76.95/77.02 inference(scs_inference,[],[15,214,350,194,11,310,21,20,3,7])).
% 76.95/77.02 cnf(359,plain,
% 76.95/77.02 (P1(f3(a1,a2),f3(f3(a4,f3(x3591,a6)),f3(a2,x3592)))),
% 76.95/77.02 inference(scs_inference,[],[15,214,350,194,11,96,310,21,20,3,7,2,6])).
% 76.95/77.02 cnf(362,plain,
% 76.95/77.02 (E(x3621,f3(x3621,f3(a2,x3622)))),
% 76.95/77.02 inference(rename_variables,[],[352])).
% 76.95/77.02 cnf(363,plain,
% 76.95/77.02 (P1(f3(a1,f3(a2,x3631)),a4)),
% 76.95/77.02 inference(scs_inference,[],[352,362,332,64])).
% 76.95/77.02 cnf(364,plain,
% 76.95/77.02 (E(x3641,f3(x3641,f3(a2,x3642)))),
% 76.95/77.02 inference(rename_variables,[],[352])).
% 76.95/77.02 cnf(365,plain,
% 76.95/77.02 (E(f3(x3651,f3(a2,x3652)),x3651)),
% 76.95/77.02 inference(scs_inference,[],[352,362,364,332,64,2])).
% 76.95/77.02 cnf(366,plain,
% 76.95/77.02 (P1(f3(x3661,x3662),f3(x3661,f3(x3663,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,187,352,362,364,332,64,2,21])).
% 76.95/77.02 cnf(367,plain,
% 76.95/77.02 (P1(x3671,f3(x3671,f3(x3672,a6)))),
% 76.95/77.02 inference(rename_variables,[],[187])).
% 76.95/77.02 cnf(369,plain,
% 76.95/77.02 (E(x3691,f3(x3691,f3(x3692,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,187,367,352,362,364,332,64,2,21,20])).
% 76.95/77.02 cnf(373,plain,
% 76.95/77.02 (P1(f3(f3(a1,f3(a1,a1)),f3(a2,x3731)),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,187,367,316,352,362,364,332,64,2,21,20,6])).
% 76.95/77.02 cnf(374,plain,
% 76.95/77.02 (E(x3741,f3(x3741,f3(a2,x3742)))),
% 76.95/77.02 inference(rename_variables,[],[352])).
% 76.95/77.02 cnf(375,plain,
% 76.95/77.02 (E(f3(x3751,a6),f3(a1,f3(a1,f3(x3752,x3752))))),
% 76.95/77.02 inference(scs_inference,[],[15,187,367,316,10,352,362,364,310,332,64,2,21,20,6,3])).
% 76.95/77.02 cnf(376,plain,
% 76.95/77.02 (P1(a1,f3(f3(a1,f3(x3761,x3761)),f3(a2,x3762)))),
% 76.95/77.02 inference(scs_inference,[],[15,187,367,308,316,10,352,362,364,374,310,332,64,2,21,20,6,3,7])).
% 76.95/77.02 cnf(380,plain,
% 76.95/77.02 (E(x3801,f3(x3801,f3(x3802,a6)))),
% 76.95/77.02 inference(rename_variables,[],[369])).
% 76.95/77.02 cnf(381,plain,
% 76.95/77.02 (P1(f3(a1,f3(x3811,a6)),a4)),
% 76.95/77.02 inference(scs_inference,[],[369,380,332,64])).
% 76.95/77.02 cnf(382,plain,
% 76.95/77.02 (E(x3821,f3(x3821,f3(x3822,a6)))),
% 76.95/77.02 inference(rename_variables,[],[369])).
% 76.95/77.02 cnf(383,plain,
% 76.95/77.02 (E(f3(x3831,f3(x3832,a6)),x3831)),
% 76.95/77.02 inference(scs_inference,[],[369,380,382,332,64,2])).
% 76.95/77.02 cnf(384,plain,
% 76.95/77.02 (P1(f3(f3(x3841,f3(x3841,x3842)),x3843),x3842)),
% 76.95/77.02 inference(scs_inference,[],[15,120,369,380,382,332,64,2,21])).
% 76.95/77.02 cnf(385,plain,
% 76.95/77.02 (P1(f3(x3851,x3852),x3851)),
% 76.95/77.02 inference(rename_variables,[],[15])).
% 76.95/77.02 cnf(387,plain,
% 76.95/77.02 (E(a1,f3(a1,f3(x3871,x3871)))),
% 76.95/77.02 inference(scs_inference,[],[15,385,120,308,369,380,382,332,64,2,21,20])).
% 76.95/77.02 cnf(390,plain,
% 76.95/77.02 (P1(f3(f3(a1,f3(a1,a1)),f3(x3901,a6)),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,385,120,308,316,369,380,382,332,64,2,21,20,6])).
% 76.95/77.02 cnf(394,plain,
% 76.95/77.02 (~E(f3(a1,f3(a2,x3941)),f3(a4,a5))),
% 76.95/77.02 inference(scs_inference,[],[15,385,120,17,308,42,316,349,365,369,380,382,332,64,2,21,20,6,3,7])).
% 76.95/77.02 cnf(397,plain,
% 76.95/77.02 (P1(f3(a1,f3(x3971,x3971)),a4)),
% 76.95/77.02 inference(scs_inference,[],[387,64])).
% 76.95/77.02 cnf(399,plain,
% 76.95/77.02 (P1(f3(a1,x3991),f3(a1,f3(x3992,x3992)))),
% 76.95/77.02 inference(scs_inference,[],[15,308,356,387,64,2,21])).
% 76.95/77.02 cnf(402,plain,
% 76.95/77.02 (E(a1,f3(f3(a1,f3(a1,a1)),f3(a2,x4021)))),
% 76.95/77.02 inference(scs_inference,[],[15,308,384,356,376,387,64,2,21,20])).
% 76.95/77.02 cnf(403,plain,
% 76.95/77.02 (P1(a1,f3(f3(a1,f3(x4031,x4031)),f3(a2,x4032)))),
% 76.95/77.02 inference(rename_variables,[],[376])).
% 76.95/77.02 cnf(406,plain,
% 76.95/77.02 (P1(f3(a1,a2),f3(f3(a1,f3(x4061,x4061)),f3(a2,x4062)))),
% 76.95/77.02 inference(scs_inference,[],[15,308,384,96,356,376,403,387,64,2,21,20,6])).
% 76.95/77.02 cnf(409,plain,
% 76.95/77.02 (~E(f3(a1,f3(x4091,a6)),f3(a4,a5))),
% 76.95/77.02 inference(scs_inference,[],[15,17,308,42,384,366,96,383,356,376,403,387,64,2,21,20,6,3,7])).
% 76.95/77.02 cnf(413,plain,
% 76.95/77.02 (P1(f3(f3(a1,a2),x4131),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,97,375,2,21])).
% 76.95/77.02 cnf(416,plain,
% 76.95/77.02 (E(f3(f3(x4161,a2),f3(a2,a2)),f3(f3(x4161,a2),a2))),
% 76.95/77.02 inference(scs_inference,[],[15,97,349,16,375,2,21,20])).
% 76.95/77.02 cnf(421,plain,
% 76.95/77.02 (E(x4211,f3(x4211,f3(a2,x4212)))),
% 76.95/77.02 inference(rename_variables,[],[352])).
% 76.95/77.02 cnf(422,plain,
% 76.95/77.02 (E(f3(a1,a2),f3(f3(a1,f3(a1,a1)),f3(a2,x4221)))),
% 76.95/77.02 inference(scs_inference,[],[15,97,373,349,8,16,375,402,352,2,21,20,6,3])).
% 76.95/77.02 cnf(423,plain,
% 76.95/77.02 (P1(a1,f3(f3(a4,f3(a2,x4231)),f3(a2,x4232)))),
% 76.95/77.02 inference(scs_inference,[],[15,97,219,373,349,8,16,375,402,352,421,2,21,20,6,3,7])).
% 76.95/77.02 cnf(426,plain,
% 76.95/77.02 (E(f3(f3(a1,f3(a1,a1)),f3(a2,x4261)),f3(a1,a2))),
% 76.95/77.02 inference(scs_inference,[],[422,2])).
% 76.95/77.02 cnf(427,plain,
% 76.95/77.02 (P1(f3(a1,x4271),f3(a4,f3(x4272,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,194,422,2,21])).
% 76.95/77.02 cnf(434,plain,
% 76.95/77.02 (P1(f3(a1,a2),f3(f3(a4,f3(a2,x4341)),f3(a2,x4342)))),
% 76.95/77.02 inference(scs_inference,[],[15,194,413,141,96,422,423,2,21,20,6])).
% 76.95/77.02 cnf(435,plain,
% 76.95/77.02 (E(a2,f3(f3(a2,a2),a2))),
% 76.95/77.02 inference(scs_inference,[],[15,194,413,141,96,28,422,416,423,2,21,20,6,3])).
% 76.95/77.02 cnf(440,plain,
% 76.95/77.02 (E(f3(f3(a2,a2),a2),a2)),
% 76.95/77.02 inference(scs_inference,[],[435,2])).
% 76.95/77.02 cnf(441,plain,
% 76.95/77.02 (P1(f3(a1,x4411),f3(a4,f3(a2,x4412)))),
% 76.95/77.02 inference(scs_inference,[],[15,219,435,2,21])).
% 76.95/77.02 cnf(444,plain,
% 76.95/77.02 (P1(f3(f3(a1,f3(a2,x4441)),f3(x4442,a6)),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,219,363,435,369,2,21,6])).
% 76.95/77.02 cnf(445,plain,
% 76.95/77.02 (E(x4451,f3(x4451,f3(x4452,a6)))),
% 76.95/77.02 inference(rename_variables,[],[369])).
% 76.95/77.02 cnf(447,plain,
% 76.95/77.02 (P1(a1,f3(f3(a4,f3(a2,x4471)),f3(x4472,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,219,363,426,435,49,369,445,2,21,6,3,7])).
% 76.95/77.02 cnf(451,plain,
% 76.95/77.02 (~P1(a4,f3(a1,f3(a1,a1)))),
% 76.95/77.02 inference(scs_inference,[],[336,330,2])).
% 76.95/77.02 cnf(456,plain,
% 76.95/77.02 (~E(f3(a1,x4561),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,434,399,402,451,2,21,6])).
% 76.95/77.02 cnf(458,plain,
% 76.95/77.02 (E(f3(f3(f3(a2,a2),a2),f3(x4581,a6)),a2)),
% 76.95/77.02 inference(scs_inference,[],[15,434,399,383,402,451,440,2,21,6,3])).
% 76.95/77.02 cnf(461,plain,
% 76.95/77.02 (P1(f3(f3(a2,a2),a2),f3(x4611,a6))),
% 76.95/77.02 inference(scs_inference,[],[15,38,434,399,383,402,451,440,2,21,6,3,7,19])).
% 76.95/77.02 cnf(465,plain,
% 76.95/77.02 (~E(f3(f3(a1,a2),a4),f3(f3(a6,a2),a2))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[348,2])).
% 76.95/77.02 cnf(466,plain,
% 76.95/77.02 (E(f3(a1,f3(x4661,x4661)),a1)),
% 76.95/77.02 inference(scs_inference,[],[387,2])).
% 76.95/77.02 cnf(467,plain,
% 76.95/77.02 (P1(f3(f3(f3(a2,a2),a2),x4671),f3(x4672,a6))),
% 76.95/77.02 inference(scs_inference,[],[15,461,387,2,21])).
% 76.95/77.02 cnf(473,plain,
% 76.95/77.02 (~E(f3(f3(a2,a2),a2),f3(a1,a5))),
% 76.95/77.02 inference(scs_inference,[],[15,461,456,397,88,387,2,21,20,6])).
% 76.95/77.02 cnf(480,plain,
% 76.95/77.02 (E(a2,f3(f3(f3(a2,a2),a2),f3(x4801,a6)))),
% 76.95/77.02 inference(scs_inference,[],[458,2])).
% 76.95/77.02 cnf(481,plain,
% 76.95/77.02 (P1(f3(f3(a1,x4811),x4812),f3(a4,f3(x4813,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,427,458,2,21])).
% 76.95/77.02 cnf(488,plain,
% 76.95/77.02 (P1(f3(f3(f3(a2,a2),a2),x4881),f3(x4882,a6))),
% 76.95/77.02 inference(rename_variables,[],[467])).
% 76.95/77.02 cnf(490,plain,
% 76.95/77.02 (P1(f3(f3(f3(a2,a2),a2),x4901),a2)),
% 76.95/77.02 inference(scs_inference,[],[15,467,488,427,381,456,10,46,88,458,466,2,21,20,6,3,7])).
% 76.95/77.02 cnf(493,plain,
% 76.95/77.02 (~E(f3(f3(a2,a2),a2),f3(a1,a2))),
% 76.95/77.02 inference(scs_inference,[],[15,467,488,427,381,456,10,46,88,458,466,2,21,20,6,3,7,4,36])).
% 76.95/77.02 cnf(494,plain,
% 76.95/77.02 (~E(f3(f3(a1,a2),a4),f3(f3(f3(a6,a2),a2),f3(a2,x4941)))+P1(a1,a2)),
% 76.95/77.02 inference(scs_inference,[],[365,465,3])).
% 76.95/77.02 cnf(496,plain,
% 76.95/77.02 (E(f3(f3(x4961,a2),a2),f3(f3(x4961,a2),f3(a2,a2)))),
% 76.95/77.02 inference(scs_inference,[],[493,416,4,2])).
% 76.95/77.02 cnf(497,plain,
% 76.95/77.02 (P1(f3(f3(a1,x4971),x4972),f3(a4,f3(a2,x4973)))),
% 76.95/77.02 inference(scs_inference,[],[15,441,493,416,4,2,21])).
% 76.95/77.02 cnf(504,plain,
% 76.95/77.02 (E(x5041,f3(x5041,f3(a2,x5042)))),
% 76.95/77.02 inference(rename_variables,[],[352])).
% 76.95/77.02 cnf(507,plain,
% 76.95/77.02 (E(f3(a2,x5071),f3(f3(f3(a2,a2),a2),f3(x5072,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,481,441,390,363,456,11,352,504,493,480,416,4,2,21,20,6,7,3])).
% 76.95/77.02 cnf(508,plain,
% 76.95/77.02 (~E(f3(a2,a2),f3(a1,a2))),
% 76.95/77.02 inference(scs_inference,[],[15,481,441,390,363,456,11,352,504,493,480,416,4,2,21,20,6,7,3,36])).
% 76.95/77.02 cnf(511,plain,
% 76.95/77.02 (E(f3(f3(f3(a2,a2),a2),f3(x5111,a6)),f3(a2,x5112))),
% 76.95/77.02 inference(scs_inference,[],[508,507,4,2])).
% 76.95/77.02 cnf(512,plain,
% 76.95/77.02 (P1(f3(f3(a1,a2),x5121),f3(f3(a1,f3(x5122,x5122)),f3(a2,x5123)))),
% 76.95/77.02 inference(scs_inference,[],[15,406,508,507,4,2,21])).
% 76.95/77.02 cnf(515,plain,
% 76.95/77.02 (E(f3(f3(f3(a2,a2),a2),x5151),a2)),
% 76.95/77.02 inference(scs_inference,[],[15,406,13,508,507,490,4,2,21,20])).
% 76.95/77.02 cnf(518,plain,
% 76.95/77.02 (P1(f3(f3(f3(a1,f3(a2,x5181)),f3(x5182,a6)),f3(a2,x5183)),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,444,406,13,352,508,507,490,4,2,21,20,6])).
% 76.95/77.02 cnf(519,plain,
% 76.95/77.02 (E(x5191,f3(x5191,f3(a2,x5192)))),
% 76.95/77.02 inference(rename_variables,[],[352])).
% 76.95/77.02 cnf(522,plain,
% 76.95/77.02 (E(f3(f3(f3(x5221,a2),a2),f3(x5222,a6)),f3(f3(x5221,a2),f3(a2,a2)))),
% 76.95/77.02 inference(scs_inference,[],[15,497,444,406,13,352,519,383,508,496,507,490,4,2,21,20,6,7,3])).
% 76.95/77.02 cnf(524,plain,
% 76.95/77.02 (P1(f3(f3(a2,a2),a2),x5241)),
% 76.95/77.02 inference(scs_inference,[],[15,497,444,406,13,352,519,383,508,496,507,490,4,2,21,20,6,7,3,19])).
% 76.95/77.02 cnf(526,plain,
% 76.95/77.02 (~E(a2,f3(a1,a2))),
% 76.95/77.02 inference(scs_inference,[],[15,497,444,406,13,352,519,383,508,496,507,490,4,2,21,20,6,7,3,19,36])).
% 76.95/77.02 cnf(528,plain,
% 76.95/77.02 (E(f3(f3(x5281,a2),f3(a2,a2)),f3(f3(f3(x5281,a2),a2),f3(x5282,a6)))),
% 76.95/77.02 inference(scs_inference,[],[522,2])).
% 76.95/77.02 cnf(529,plain,
% 76.95/77.02 (P1(f3(f3(f3(a2,a2),a2),x5291),x5292)),
% 76.95/77.02 inference(scs_inference,[],[15,524,522,2,21])).
% 76.95/77.02 cnf(535,plain,
% 76.95/77.02 (P1(f3(f3(a1,f3(x5351,x5351)),f3(a2,x5352)),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,524,473,397,352,522,2,21,20,6])).
% 76.95/77.02 cnf(536,plain,
% 76.95/77.02 (E(x5361,f3(x5361,f3(a2,x5362)))),
% 76.95/77.02 inference(rename_variables,[],[352])).
% 76.95/77.02 cnf(538,plain,
% 76.95/77.02 (E(f3(f3(a2,a2),a2),f3(a2,x5381))),
% 76.95/77.02 inference(scs_inference,[],[15,524,38,473,359,397,352,536,522,511,2,21,20,6,7,3])).
% 76.95/77.02 cnf(544,plain,
% 76.95/77.02 (E(f3(a2,x5441),f3(f3(a2,a2),a2))),
% 76.95/77.02 inference(scs_inference,[],[538,2])).
% 76.95/77.02 cnf(552,plain,
% 76.95/77.02 (P1(f3(f3(f3(a1,f3(x5521,x5521)),f3(a2,x5522)),f3(a2,x5523)),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,85,529,535,413,352,538,2,21,20,6])).
% 76.95/77.02 cnf(554,plain,
% 76.95/77.02 (E(f3(f3(f3(a2,a2),a2),f3(a2,x5541)),f3(a2,x5542))),
% 76.95/77.02 inference(scs_inference,[],[15,85,529,535,413,352,365,538,2,21,20,6,3])).
% 76.95/77.02 cnf(556,plain,
% 76.95/77.02 (~E(f3(a1,f3(x5561,x5561)),f3(a4,a5))),
% 76.95/77.02 inference(scs_inference,[],[15,17,85,529,535,399,413,352,365,538,2,21,20,6,3,7])).
% 76.95/77.02 cnf(563,plain,
% 76.95/77.02 (P1(f3(f3(a1,f3(a2,x5631)),f3(a2,x5632)),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,381,363,352,554,2,21,6])).
% 76.95/77.02 cnf(567,plain,
% 76.95/77.02 (E(f3(f3(x5671,a6),f3(x5672,a6)),f3(f3(a2,a2),a2))),
% 76.95/77.02 inference(scs_inference,[],[15,17,427,381,363,110,352,554,544,2,21,6,7,3])).
% 76.95/77.02 cnf(569,plain,
% 76.95/77.02 (~E(f3(x5691,a6),a5)),
% 76.95/77.02 inference(scs_inference,[],[15,17,427,381,363,110,352,554,544,2,21,6,7,3,5])).
% 76.95/77.02 cnf(578,plain,
% 76.95/77.02 (E(x5781,f3(x5781,f3(x5782,a6)))),
% 76.95/77.02 inference(rename_variables,[],[369])).
% 76.95/77.02 cnf(579,plain,
% 76.95/77.02 (P1(a1,f3(f3(a1,f3(x5791,x5791)),f3(x5792,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,308,563,397,369,578,515,2,21,6,7])).
% 76.95/77.02 cnf(581,plain,
% 76.95/77.02 (E(f3(x5811,a6),f3(f3(a2,a2),a2))),
% 76.95/77.02 inference(scs_inference,[],[15,308,563,397,99,369,578,515,567,2,21,6,7,3])).
% 76.95/77.02 cnf(583,plain,
% 76.95/77.02 (E(f3(f3(f3(a1,f3(x5831,x5831)),f3(a2,x5832)),f3(a2,x5833)),a4)+~P1(a4,f3(f3(f3(a1,f3(x5831,x5831)),f3(a2,x5832)),f3(a2,x5833)))),
% 76.95/77.02 inference(scs_inference,[],[15,308,552,563,397,99,369,578,515,567,2,21,6,7,3,20])).
% 76.95/77.02 cnf(586,plain,
% 76.95/77.02 (E(f3(f3(a2,a2),a2),f3(x5861,a6))),
% 76.95/77.02 inference(scs_inference,[],[581,2])).
% 76.95/77.02 cnf(590,plain,
% 76.95/77.02 (E(a1,f3(f3(a1,f3(a1,a1)),f3(x5901,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,384,363,581,579,2,21,20])).
% 76.95/77.02 cnf(595,plain,
% 76.95/77.02 (E(x5951,f3(x5951,f3(a2,x5952)))),
% 76.95/77.02 inference(rename_variables,[],[352])).
% 76.95/77.02 cnf(598,plain,
% 76.95/77.02 (E(f3(x5981,a2),f3(f3(f3(x5981,a2),a2),f3(x5982,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,17,384,441,563,363,352,595,528,581,579,2,21,20,6,7,3])).
% 76.95/77.02 cnf(600,plain,
% 76.95/77.02 (~E(f3(a2,x6001),a5)),
% 76.95/77.02 inference(scs_inference,[],[15,17,384,441,563,363,352,595,528,581,579,2,21,20,6,7,3,5])).
% 76.95/77.02 cnf(602,plain,
% 76.95/77.02 (E(f3(f3(f3(x6021,a2),a2),f3(x6022,a6)),f3(x6021,a2))),
% 76.95/77.02 inference(scs_inference,[],[598,2])).
% 76.95/77.02 cnf(603,plain,
% 76.95/77.02 (P1(f3(f3(x6031,a4),x6032),f3(x6031,f3(a1,a2)))),
% 76.95/77.02 inference(scs_inference,[],[15,130,598,2,21])).
% 76.95/77.02 cnf(606,plain,
% 76.95/77.02 (P1(f3(a1,a2),f3(f3(a4,f3(a2,x6061)),f3(x6062,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,130,96,598,447,2,21,6])).
% 76.95/77.02 cnf(607,plain,
% 76.95/77.02 (E(f3(f3(f3(a2,a2),a2),f3(x6071,a6)),f3(x6072,a6))),
% 76.95/77.02 inference(scs_inference,[],[15,130,96,383,586,598,447,2,21,6,3])).
% 76.95/77.02 cnf(609,plain,
% 76.95/77.02 (P1(a1,f3(f3(f3(a4,f3(x6091,a6)),f3(a2,x6092)),f3(a2,x6093)))),
% 76.95/77.02 inference(scs_inference,[],[15,130,96,352,383,586,598,357,447,2,21,6,3,7])).
% 76.95/77.02 cnf(611,plain,
% 76.95/77.02 (E(f3(f3(f3(a1,f3(a2,x6111)),f3(x6112,a6)),f3(a2,x6113)),a4)+~P1(a4,f3(f3(f3(a1,f3(a2,x6111)),f3(x6112,a6)),f3(a2,x6113)))),
% 76.95/77.02 inference(scs_inference,[],[15,518,130,96,352,383,586,598,357,447,2,21,6,3,7,20])).
% 76.95/77.02 cnf(619,plain,
% 76.95/77.02 (E(f3(f3(f3(a1,a2),a4),f3(a2,x6191)),a2)),
% 76.95/77.02 inference(scs_inference,[],[15,606,96,153,365,590,609,2,21,6,3])).
% 76.95/77.02 cnf(621,plain,
% 76.95/77.02 (P1(a1,f3(f3(a4,f3(x6211,a6)),f3(x6212,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,194,606,96,153,369,365,590,609,2,21,6,3,7])).
% 76.95/77.02 cnf(623,plain,
% 76.95/77.02 (P1(f3(f3(a1,a2),a4),f3(a2,x6231))),
% 76.95/77.02 inference(scs_inference,[],[15,194,606,96,153,369,365,590,609,2,21,6,3,7,19])).
% 76.95/77.02 cnf(628,plain,
% 76.95/77.02 (E(f3(x6281,a6),f3(f3(f3(a2,a2),a2),f3(x6282,a6)))),
% 76.95/77.02 inference(scs_inference,[],[607,2])).
% 76.95/77.02 cnf(629,plain,
% 76.95/77.02 (P1(f3(f3(f3(a1,a2),a4),x6291),f3(a2,x6292))),
% 76.95/77.02 inference(scs_inference,[],[15,623,607,2,21])).
% 76.95/77.02 cnf(632,plain,
% 76.95/77.02 (P1(f3(a1,a2),f3(f3(a4,f3(x6321,a6)),f3(x6322,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,623,96,607,621,2,21,6])).
% 76.95/77.02 cnf(633,plain,
% 76.95/77.02 (E(f3(f3(f3(a1,a2),a4),f3(a2,x6331)),f3(f3(x6332,a6),f3(x6333,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,623,96,365,176,607,621,2,21,6,3])).
% 76.95/77.02 cnf(635,plain,
% 76.95/77.02 (P1(f3(x6351,f3(x6351,a1)),f3(a1,a2))),
% 76.95/77.02 inference(scs_inference,[],[15,120,623,96,365,176,607,621,2,21,6,3,7])).
% 76.95/77.02 cnf(644,plain,
% 76.95/77.02 (P1(f3(f3(f3(a1,a2),a4),f3(a2,x6441)),f3(f3(x6442,a6),f3(x6443,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,632,178,352,619,2,21,6])).
% 76.95/77.02 cnf(646,plain,
% 76.95/77.02 (P1(f3(f3(a2,a4),x6461),a2)),
% 76.95/77.02 inference(scs_inference,[],[15,603,632,178,11,352,619,2,21,6,7])).
% 76.95/77.02 cnf(649,plain,
% 76.95/77.02 (E(f3(f3(f3(a1,a2),a4),f3(x6491,a6)),a2)),
% 76.95/77.02 inference(scs_inference,[],[15,603,632,178,11,352,153,383,619,2,21,6,7,3])).
% 76.95/77.02 cnf(655,plain,
% 76.95/77.02 (P1(f3(a1,x6551),a4)),
% 76.95/77.02 inference(scs_inference,[],[15,9,633,2,21])).
% 76.95/77.02 cnf(658,plain,
% 76.95/77.02 (E(f3(f3(a2,a4),x6581),a2)),
% 76.95/77.02 inference(scs_inference,[],[15,9,13,633,646,2,21,20])).
% 76.95/77.02 cnf(661,plain,
% 76.95/77.02 (P1(f3(f3(f3(a1,a2),a4),f3(x6611,a6)),f3(f3(x6612,a6),f3(x6613,a6)))),
% 76.95/77.02 inference(scs_inference,[],[15,9,178,13,369,633,646,2,21,20,6])).
% 76.95/77.02 cnf(663,plain,
% 76.95/77.02 (E(f3(f3(f3(a1,a2),a4),f3(a2,x6631)),f3(x6632,a6))),
% 76.95/77.02 inference(scs_inference,[],[15,9,178,13,369,365,166,633,646,2,21,20,6,3])).
% 76.95/77.02 cnf(668,plain,
% 76.95/77.02 (P1(f3(a2,a4),x6681)),
% 76.95/77.02 inference(scs_inference,[],[15,644,9,178,14,13,369,365,166,633,646,2,21,20,6,3,7,19])).
% 76.95/77.02 cnf(671,plain,
% 76.95/77.02 (E(f3(x6711,a6),f3(f3(f3(a1,a2),a4),f3(a2,x6712)))),
% 76.95/77.02 inference(scs_inference,[],[663,2])).
% 76.95/77.02 cnf(672,plain,
% 76.95/77.02 (P1(f3(f3(a2,a4),x6721),x6722)),
% 76.95/77.02 inference(scs_inference,[],[15,668,663,2,21])).
% 76.95/77.02 cnf(675,plain,
% 76.95/77.02 (~P1(a5,f3(a2,a4))),
% 76.95/77.02 inference(scs_inference,[],[15,668,663,600,2,21,20])).
% 76.95/77.02 cnf(676,plain,
% 76.95/77.02 (P1(f3(a2,a4),x6761)),
% 76.95/77.02 inference(rename_variables,[],[668])).
% 76.95/77.02 cnf(679,plain,
% 76.95/77.02 (~E(f3(a2,a4),f3(a1,a5))),
% 76.95/77.02 inference(scs_inference,[],[15,17,668,676,663,600,2,21,20,6])).
% 76.95/77.02 cnf(684,plain,
% 76.95/77.02 (E(f3(f3(f3(a1,a2),a4),f3(a2,x6841)),f3(a2,x6842))),
% 76.95/77.02 inference(scs_inference,[],[15,17,668,676,661,14,365,170,663,600,2,21,20,6,7,3])).
% 76.95/77.03 cnf(688,plain,
% 76.95/77.03 (P1(f3(f3(f3(a2,a4),x6881),x6882),x6883)),
% 76.95/77.03 inference(scs_inference,[],[15,672,684,2,21])).
% 76.95/77.03 cnf(691,plain,
% 76.95/77.03 (~P1(f3(a1,a5),f3(a2,a4))),
% 76.95/77.03 inference(scs_inference,[],[15,668,672,679,684,2,21,20])).
% 76.95/77.03 cnf(694,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),a5)),
% 76.95/77.03 inference(scs_inference,[],[15,623,668,672,679,684,675,2,21,20,6])).
% 76.95/77.03 cnf(696,plain,
% 76.95/77.03 (E(f3(f3(f3(a1,a2),a4),f3(a2,x6961)),f3(x6962,x6962))),
% 76.95/77.03 inference(scs_inference,[],[15,623,668,672,679,365,301,684,675,2,21,20,6,3])).
% 76.95/77.03 cnf(698,plain,
% 76.95/77.03 (P1(f3(f3(f3(a1,a2),a4),x6981),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,623,668,672,679,629,10,365,301,684,675,2,21,20,6,3,7])).
% 76.95/77.03 cnf(705,plain,
% 76.95/77.03 (P1(f3(f3(a1,x7051),x7052),a4)),
% 76.95/77.03 inference(scs_inference,[],[15,655,696,2,21])).
% 76.95/77.03 cnf(709,plain,
% 76.95/77.03 (P1(f3(f3(f3(a2,a4),x7091),x7092),x7093)),
% 76.95/77.03 inference(rename_variables,[],[688])).
% 76.95/77.03 cnf(714,plain,
% 76.95/77.03 (~E(a4,f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[15,17,85,688,709,655,696,2,21,20,6,7])).
% 76.95/77.03 cnf(716,plain,
% 76.95/77.03 (~E(f3(a2,a2),f3(f3(f3(a1,a2),a2),f3(x7161,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,17,85,688,709,655,508,696,602,2,21,20,6,7,3])).
% 76.95/77.03 cnf(718,plain,
% 76.95/77.03 (~E(f3(f3(a2,a4),x7181),a1)),
% 76.95/77.03 inference(scs_inference,[],[15,17,85,688,709,655,508,696,602,2,21,20,6,7,3,4])).
% 76.95/77.03 cnf(724,plain,
% 76.95/77.03 (~E(f3(a2,a4),a1)),
% 76.95/77.03 inference(scs_inference,[],[718,36,4])).
% 76.95/77.03 cnf(725,plain,
% 76.95/77.03 (E(a2,f3(f3(a2,a4),x7251))),
% 76.95/77.03 inference(scs_inference,[],[658,718,36,4,2])).
% 76.95/77.03 cnf(726,plain,
% 76.95/77.03 (P1(f3(f3(f3(a1,x7261),x7262),x7263),a4)),
% 76.95/77.03 inference(scs_inference,[],[15,705,658,718,36,4,2,21])).
% 76.95/77.03 cnf(735,plain,
% 76.95/77.03 (~E(f3(a2,a2),f3(f3(a1,a2),a2))),
% 76.95/77.03 inference(scs_inference,[],[15,17,705,672,141,369,716,658,718,36,4,2,21,20,6,3])).
% 76.95/77.03 cnf(738,plain,
% 76.95/77.03 (E(f3(a1,a2),f3(a1,f3(x7381,x7381)))),
% 76.95/77.03 inference(scs_inference,[],[13,337,22])).
% 76.95/77.03 cnf(740,plain,
% 76.95/77.03 (E(f3(a1,f3(x7401,x7401)),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[738,724,36,2])).
% 76.95/77.03 cnf(741,plain,
% 76.95/77.03 (P1(f3(a2,x7411),x7412)),
% 76.95/77.03 inference(scs_inference,[],[15,13,738,724,36,2,21])).
% 76.95/77.03 cnf(751,plain,
% 76.95/77.03 (E(f3(f3(x7511,a6),f3(x7512,a6)),f3(f3(f3(a2,a2),a2),f3(x7513,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,38,85,632,629,672,13,102,691,738,628,724,36,2,21,20,6,7,3])).
% 76.95/77.03 cnf(755,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),a1)),
% 76.95/77.03 inference(scs_inference,[],[15,38,85,632,629,672,13,102,691,738,628,724,36,2,21,20,6,7,3,23,4])).
% 76.95/77.03 cnf(757,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[755,36])).
% 76.95/77.03 cnf(758,plain,
% 76.95/77.03 (E(f3(f3(f3(a2,a2),a2),f3(x7581,a6)),f3(f3(x7582,a6),f3(x7583,a6)))),
% 76.95/77.03 inference(scs_inference,[],[751,755,36,2])).
% 76.95/77.03 cnf(759,plain,
% 76.95/77.03 (P1(f3(f3(a2,x7591),x7592),x7593)),
% 76.95/77.03 inference(scs_inference,[],[15,741,751,755,36,2,21])).
% 76.95/77.03 cnf(762,plain,
% 76.95/77.03 (~P1(f3(a1,a5),f3(a2,a6))),
% 76.95/77.03 inference(scs_inference,[],[15,85,741,751,755,36,2,21,20])).
% 76.95/77.03 cnf(773,plain,
% 76.95/77.03 (~E(f3(f3(f3(a6,a2),a2),f3(a2,x7731)),f3(f3(a1,a2),a4))+P1(a1,a2)),
% 76.95/77.03 inference(scs_inference,[],[494,2])).
% 76.95/77.03 cnf(775,plain,
% 76.95/77.03 (P1(f3(f3(f3(a2,x7751),x7752),x7753),x7754)),
% 76.95/77.03 inference(scs_inference,[],[15,759,649,2,21])).
% 76.95/77.03 cnf(779,plain,
% 76.95/77.03 (P1(f3(f3(a2,x7791),x7792),x7793)),
% 76.95/77.03 inference(rename_variables,[],[759])).
% 76.95/77.03 cnf(785,plain,
% 76.95/77.03 (E(x7851,f3(x7851,f3(x7852,a6)))),
% 76.95/77.03 inference(rename_variables,[],[369])).
% 76.95/77.03 cnf(786,plain,
% 76.95/77.03 (E(f3(f3(a2,a2),a2),f3(f3(x7861,a6),f3(x7862,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,17,85,759,779,497,369,785,758,649,2,21,20,6,7,3])).
% 76.95/77.03 cnf(791,plain,
% 76.95/77.03 (~E(f3(a2,x7911),a1)),
% 76.95/77.03 inference(scs_inference,[],[15,17,85,759,779,497,369,785,758,649,2,21,20,6,7,3,23,4])).
% 76.95/77.03 cnf(793,plain,
% 76.95/77.03 (~P1(a1,f3(a2,f3(a2,f3(a1,a2))))),
% 76.95/77.03 inference(scs_inference,[],[15,17,85,759,779,497,369,785,758,649,2,21,20,6,7,3,23,4,36,144])).
% 76.95/77.03 cnf(800,plain,
% 76.95/77.03 (P1(f3(f3(f3(a2,x8001),x8002),x8003),x8004)),
% 76.95/77.03 inference(rename_variables,[],[775])).
% 76.95/77.03 cnf(805,plain,
% 76.95/77.03 (P1(f3(f3(x8051,f3(x8051,a1)),x8052),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[15,17,85,775,800,384,96,98,21,20,6,7])).
% 76.95/77.03 cnf(807,plain,
% 76.95/77.03 (E(f3(f3(f3(a2,a2),a2),f3(a2,x8071)),f3(f3(x8072,a6),f3(x8073,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,17,85,775,800,384,96,98,365,786,21,20,6,7,3])).
% 76.95/77.03 cnf(815,plain,
% 76.95/77.03 (P1(f3(f3(x8151,a6),x8152),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,81,21])).
% 76.95/77.03 cnf(822,plain,
% 76.95/77.03 (~E(f3(f3(x8221,f3(x8221,a1)),x8222),a4)),
% 76.95/77.03 inference(scs_inference,[],[15,141,655,81,146,805,21,20,6])).
% 76.95/77.03 cnf(829,plain,
% 76.95/77.03 (P1(f3(f3(f3(x8291,a6),x8292),x8293),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,815,21])).
% 76.95/77.03 cnf(832,plain,
% 76.95/77.03 (E(f3(f3(x8321,a6),x8322),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,815,13,21,20])).
% 76.95/77.03 cnf(835,plain,
% 76.95/77.03 (~E(f3(f3(x8351,a6),x8352),f3(a1,a5))),
% 76.95/77.03 inference(scs_inference,[],[15,815,31,13,21,20,6])).
% 76.95/77.03 cnf(838,plain,
% 76.95/77.03 (E(f3(x8381,a6),f3(f3(a2,a4),x8382))),
% 76.95/77.03 inference(scs_inference,[],[15,815,10,31,13,369,725,21,20,6,7,3])).
% 76.95/77.03 cnf(839,plain,
% 76.95/77.03 (P1(f3(x8391,a6),x8392)),
% 76.95/77.03 inference(scs_inference,[],[15,815,10,31,13,369,725,21,20,6,7,3,19])).
% 76.95/77.03 cnf(842,plain,
% 76.95/77.03 (~E(f3(x8421,a6),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[15,815,10,31,13,369,725,21,20,6,7,3,19,4,36])).
% 76.95/77.03 cnf(844,plain,
% 76.95/77.03 (~E(a6,a2)),
% 76.95/77.03 inference(scs_inference,[],[15,815,10,31,13,369,725,21,20,6,7,3,19,4,36,2,5])).
% 76.95/77.03 cnf(848,plain,
% 76.95/77.03 (P1(f3(f3(x8481,a6),x8482),x8483)),
% 76.95/77.03 inference(scs_inference,[],[15,839,838,844,157,2,21])).
% 76.95/77.03 cnf(856,plain,
% 76.95/77.03 (~E(a6,f3(x8561,a6))),
% 76.95/77.03 inference(scs_inference,[],[15,839,54,829,10,31,838,844,157,2,21,20,6,3])).
% 76.95/77.03 cnf(862,plain,
% 76.95/77.03 (~P1(a1,f3(f3(x8621,a6),f3(f3(x8621,a6),f3(a1,a2))))),
% 76.95/77.03 inference(scs_inference,[],[15,839,54,829,9,10,31,793,838,844,157,2,21,20,6,3,7,23,4,36,144])).
% 76.95/77.03 cnf(865,plain,
% 76.95/77.03 (E(a2,f3(f3(x8651,a6),x8652))),
% 76.95/77.03 inference(scs_inference,[],[832,2])).
% 76.95/77.03 cnf(866,plain,
% 76.95/77.03 (P1(f3(f3(f3(x8661,a6),x8662),x8663),x8664)),
% 76.95/77.03 inference(scs_inference,[],[15,848,832,2,21])).
% 76.95/77.03 cnf(873,plain,
% 76.95/77.03 (~E(f3(x8731,f3(x8731,a1)),a4)),
% 76.95/77.03 inference(scs_inference,[],[15,85,848,635,832,146,2,21,20,6])).
% 76.95/77.03 cnf(887,plain,
% 76.95/77.03 (~E(a6,f3(a2,x8871))),
% 76.95/77.03 inference(scs_inference,[],[15,85,866,9,96,11,164,862,579,844,21,20,6,7,3])).
% 76.95/77.03 cnf(900,plain,
% 76.95/77.03 (P1(f3(f3(f3(a1,a2),a4),x9001),f3(x9002,x9002))),
% 76.95/77.03 inference(scs_inference,[],[15,174,21])).
% 76.95/77.03 cnf(903,plain,
% 76.95/77.03 (~P1(a4,f3(f3(a1,f3(a1,a1)),x9031))),
% 76.95/77.03 inference(scs_inference,[],[15,822,705,174,21,20])).
% 76.95/77.03 cnf(907,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),x9071),a4)),
% 76.95/77.03 inference(scs_inference,[],[15,512,822,705,174,21,20,6])).
% 76.95/77.03 cnf(909,plain,
% 76.95/77.03 (~E(f3(a1,a2),f3(a2,f3(a2,f3(a1,a2))))),
% 76.95/77.03 inference(scs_inference,[],[15,512,822,705,174,342,793,21,20,6,7])).
% 76.95/77.03 cnf(912,plain,
% 76.95/77.03 (P1(f3(a1,x9121),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[15,342,21])).
% 76.95/77.03 cnf(915,plain,
% 76.95/77.03 (~P1(a4,f3(f3(a1,a2),x9151))),
% 76.95/77.03 inference(scs_inference,[],[15,907,705,342,21,20])).
% 76.95/77.03 cnf(921,plain,
% 76.95/77.03 (P1(f3(x9211,f3(x9211,a1)),f3(f3(a1,a2),f3(a2,x9212)))),
% 76.95/77.03 inference(scs_inference,[],[15,900,907,705,352,903,635,342,21,20,6,7])).
% 76.95/77.03 cnf(929,plain,
% 76.95/77.03 (P1(f3(a1,x9291),f3(a1,a2))),
% 76.95/77.03 inference(rename_variables,[],[912])).
% 76.95/77.03 cnf(932,plain,
% 76.95/77.03 (~E(f3(x9321,f3(x9321,f3(x9322,a6))),a4)),
% 76.95/77.03 inference(scs_inference,[],[15,912,250,842,915,609,21,20,6])).
% 76.95/77.03 cnf(939,plain,
% 76.95/77.03 (~P1(a1,a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18])).
% 76.95/77.03 cnf(941,plain,
% 76.95/77.03 (~P1(a6,a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22])).
% 76.95/77.03 cnf(948,plain,
% 76.95/77.03 (~E(f3(a4,f3(x9481,a6)),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252])).
% 76.95/77.03 cnf(949,plain,
% 76.95/77.03 (~E(f3(a4,f3(a2,x9491)),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257])).
% 76.95/77.03 cnf(950,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),f3(a4,f3(a4,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262])).
% 76.95/77.03 cnf(953,plain,
% 76.95/77.03 (~E(f3(a1,f3(x9531,x9531)),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325])).
% 76.95/77.03 cnf(954,plain,
% 76.95/77.03 (~E(f3(a6,a2),f3(f3(a1,a2),a4))),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327])).
% 76.95/77.03 cnf(955,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),f3(a6,a2))),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327,334])).
% 76.95/77.03 cnf(956,plain,
% 76.95/77.03 (~E(a2,f3(a6,a2))),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327,334,339])).
% 76.95/77.03 cnf(957,plain,
% 76.95/77.03 (~P1(f3(a6,a2),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327,334,339,344])).
% 76.95/77.03 cnf(961,plain,
% 76.95/77.03 (~E(f3(f3(f3(a6,a2),a2),f3(a2,x9611)),f3(f3(a1,a2),a4))),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327,334,339,344,348,465,494,773])).
% 76.95/77.03 cnf(963,plain,
% 76.95/77.03 (~P1(f3(a1,f3(a1,a6)),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327,334,339,344,348,465,494,773,157,23])).
% 76.95/77.03 cnf(965,plain,
% 76.95/77.03 (~P1(f3(a4,a2),f3(a4,a6))),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327,334,339,344,348,465,494,773,157,23,297])).
% 76.95/77.03 cnf(966,plain,
% 76.95/77.03 (~E(f3(a6,a2),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327,334,339,344,348,465,494,773,157,23,297,319])).
% 76.95/77.03 cnf(967,plain,
% 76.95/77.03 (~E(f3(f3(a6,a2),a2),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,17,912,929,352,250,909,842,915,609,21,20,6,3,7,18,22,158,169,175,179,192,252,257,262,295,296,325,327,334,339,344,348,465,494,773,157,23,297,319,347])).
% 76.95/77.03 cnf(970,plain,
% 76.95/77.03 (~P1(a1,f3(x9701,x9701))),
% 76.95/77.03 inference(scs_inference,[],[953,18])).
% 76.95/77.03 cnf(972,plain,
% 76.95/77.03 (~E(f3(a4,f3(a2,x9721)),f3(x9722,x9722))),
% 76.95/77.03 inference(scs_inference,[],[953,18,257])).
% 76.95/77.03 cnf(973,plain,
% 76.95/77.03 (~E(f3(a4,f3(x9731,a6)),f3(x9732,x9732))),
% 76.95/77.03 inference(scs_inference,[],[953,18,257,252])).
% 76.95/77.03 cnf(974,plain,
% 76.95/77.03 (~E(f3(a1,f3(x9741,x9741)),f3(x9742,x9742))),
% 76.95/77.03 inference(scs_inference,[],[953,18,257,252,325])).
% 76.95/77.03 cnf(977,plain,
% 76.95/77.03 (P1(f3(a1,x9771),f3(f3(a1,f3(x9772,x9772)),f3(a2,x9773)))),
% 76.95/77.03 inference(scs_inference,[],[15,953,376,18,257,252,325,157,5,21])).
% 76.95/77.03 cnf(989,plain,
% 76.95/77.03 (~P1(a4,f3(x9891,a6))),
% 76.95/77.03 inference(scs_inference,[],[948,18])).
% 76.95/77.03 cnf(993,plain,
% 76.95/77.03 (~E(f3(a1,f3(x9931,x9931)),f3(x9932,x9932))),
% 76.95/77.03 inference(rename_variables,[],[974])).
% 76.95/77.03 cnf(994,plain,
% 76.95/77.03 (~E(a1,f3(x9941,x9941))),
% 76.95/77.03 inference(scs_inference,[],[974,993,948,18,157,5,4])).
% 76.95/77.03 cnf(996,plain,
% 76.95/77.03 (~E(f3(x9961,x9961),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[974,993,948,18,157,5,4,36])).
% 76.95/77.03 cnf(997,plain,
% 76.95/77.03 (P1(f3(f3(a1,x9971),x9972),f3(f3(a1,f3(x9973,x9973)),f3(a2,x9974)))),
% 76.95/77.03 inference(scs_inference,[],[15,977,974,993,948,18,157,5,4,36,21])).
% 76.95/77.03 cnf(1003,plain,
% 76.95/77.03 (~E(f3(f3(f3(a1,a2),a4),x10031),a1)),
% 76.95/77.03 inference(scs_inference,[],[15,977,900,481,974,993,950,970,948,18,157,5,4,36,21,20,6])).
% 76.95/77.03 cnf(1010,plain,
% 76.95/77.03 (~P1(a6,f3(f3(a1,a2),a4))),
% 76.95/77.03 inference(scs_inference,[],[15,17,977,967,900,481,10,974,993,950,970,948,18,157,5,4,36,21,20,6,3,7,23,22])).
% 76.95/77.03 cnf(1013,plain,
% 76.95/77.03 (~P1(a4,f3(a2,x10131))),
% 76.95/77.03 inference(scs_inference,[],[949,18])).
% 76.95/77.03 cnf(1016,plain,
% 76.95/77.03 (~E(a1,a2)),
% 76.95/77.03 inference(scs_inference,[],[996,949,18,157,5])).
% 76.95/77.03 cnf(1017,plain,
% 76.95/77.03 (~E(f3(x10171,x10171),f3(a1,a2))),
% 76.95/77.03 inference(rename_variables,[],[996])).
% 76.95/77.03 cnf(1021,plain,
% 76.95/77.03 (P1(f3(a1,x10211),f3(f3(a4,f3(x10212,a6)),f3(a2,x10213)))),
% 76.95/77.03 inference(scs_inference,[],[15,1003,996,972,949,357,18,157,5,4,36,21])).
% 76.95/77.03 cnf(1024,plain,
% 76.95/77.03 (~P1(f3(a1,a2),f3(a1,a1))),
% 76.95/77.03 inference(scs_inference,[],[15,1003,912,996,1017,972,949,357,18,157,5,4,36,21,20])).
% 76.95/77.03 cnf(1028,plain,
% 76.95/77.03 (~E(f3(f3(a1,x10281),x10282),a4)),
% 76.95/77.03 inference(scs_inference,[],[15,997,1003,912,996,1017,972,949,903,357,18,157,5,4,36,21,20,6])).
% 76.95/77.03 cnf(1031,plain,
% 76.95/77.03 (~E(f3(a6,a2),f3(x10311,x10311))),
% 76.95/77.03 inference(scs_inference,[],[15,997,1003,912,966,14,996,1017,972,949,903,357,18,157,5,4,36,21,20,6,3])).
% 76.95/77.03 cnf(1033,plain,
% 76.95/77.03 (~P1(f3(a1,f3(a1,a1)),a2)),
% 76.95/77.03 inference(scs_inference,[],[15,997,1003,912,966,9,14,996,1017,972,939,949,903,357,18,157,5,4,36,21,20,6,3,7,23])).
% 76.95/77.03 cnf(1036,plain,
% 76.95/77.03 (~E(a1,f3(f3(a1,a2),a4))),
% 76.95/77.03 inference(scs_inference,[],[1016,157])).
% 76.95/77.03 cnf(1037,plain,
% 76.95/77.03 (~E(a2,a6)),
% 76.95/77.03 inference(scs_inference,[],[1031,1016,157,5])).
% 76.95/77.03 cnf(1039,plain,
% 76.95/77.03 (P1(f3(a1,x10391),f3(f3(a4,f3(a2,x10392)),f3(a2,x10393)))),
% 76.95/77.03 inference(scs_inference,[],[15,1031,1016,423,157,5,21])).
% 76.95/77.03 cnf(1046,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),f3(a1,f3(a1,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,963,932,655,150,1031,1016,423,157,5,21,20,6])).
% 76.95/77.03 cnf(1051,plain,
% 76.95/77.03 (P1(f3(a1,x10511),f3(f3(a4,f3(a2,x10512)),f3(x10513,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,447,21])).
% 76.95/77.03 cnf(1058,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),f3(a1,f3(a1,a1)))),
% 76.95/77.03 inference(scs_inference,[],[15,1033,873,705,150,447,21,20,6])).
% 76.95/77.03 cnf(1072,plain,
% 76.95/77.03 (~E(f3(f3(a6,a2),a2),f3(a2,x10721))),
% 76.95/77.03 inference(scs_inference,[],[15,17,1051,1028,967,705,11,250,1024,621,21,20,6,7,3])).
% 76.95/77.03 cnf(1074,plain,
% 76.95/77.03 (~P1(a1,f3(x10741,a6))),
% 76.95/77.03 inference(scs_inference,[],[15,17,1051,1028,967,705,11,250,1024,621,21,20,6,7,3,5,18])).
% 76.95/77.03 cnf(1076,plain,
% 76.95/77.03 (~E(f3(a4,f3(a2,x10761)),f3(x10762,a6))),
% 76.95/77.03 inference(scs_inference,[],[15,17,1051,1028,967,705,11,250,1024,621,21,20,6,7,3,5,18,257])).
% 76.95/77.03 cnf(1077,plain,
% 76.95/77.03 (~E(f3(a4,f3(x10771,a6)),f3(x10772,a6))),
% 76.95/77.03 inference(scs_inference,[],[15,17,1051,1028,967,705,11,250,1024,621,21,20,6,7,3,5,18,257,252])).
% 76.95/77.03 cnf(1078,plain,
% 76.95/77.03 (~E(f3(a1,f3(x10781,x10781)),f3(x10782,a6))),
% 76.95/77.03 inference(scs_inference,[],[15,17,1051,1028,967,705,11,250,1024,621,21,20,6,7,3,5,18,257,252,325])).
% 76.95/77.03 cnf(1081,plain,
% 76.95/77.03 (~E(f3(x10811,x10811),a6)),
% 76.95/77.03 inference(scs_inference,[],[1078,5])).
% 76.95/77.03 cnf(1083,plain,
% 76.95/77.03 (P1(f3(a1,x10831),f3(f3(a1,f3(x10832,x10832)),f3(x10833,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,1078,579,5,21])).
% 76.95/77.03 cnf(1098,plain,
% 76.95/77.03 (~E(f3(a2,x10981),a6)),
% 76.95/77.03 inference(scs_inference,[],[1076,5])).
% 76.95/77.03 cnf(1100,plain,
% 76.95/77.03 (P1(f3(f3(a1,x11001),x11002),f3(f3(a1,f3(x11003,x11003)),f3(x11004,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,1083,1076,5,21])).
% 76.95/77.03 cnf(1108,plain,
% 76.95/77.03 (~E(f3(a6,a2),f3(f3(x11081,f3(x11081,x11082)),x11082))),
% 76.95/77.03 inference(scs_inference,[],[15,17,1083,966,13,119,1076,698,5,21,20,7,3])).
% 76.95/77.03 cnf(1109,plain,
% 76.95/77.03 (P1(f3(f3(a1,a2),a4),x11091)),
% 76.95/77.03 inference(scs_inference,[],[15,17,1083,966,13,119,1076,698,5,21,20,7,3,19])).
% 76.95/77.03 cnf(1116,plain,
% 76.95/77.03 (P1(f3(f3(f3(a1,a2),a4),x11161),x11162)),
% 76.95/77.03 inference(scs_inference,[],[15,1109,1077,5,21])).
% 76.95/77.03 cnf(1122,plain,
% 76.95/77.03 (P1(x11221,f3(f3(a6,f3(a2,x11222)),f3(x11223,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,1109,264,156,369,1077,5,21,20,7])).
% 76.95/77.03 cnf(1124,plain,
% 76.95/77.03 (~E(f3(a4,f3(x11241,a6)),f3(f3(x11242,a6),f3(x11243,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,1109,264,156,369,110,973,1077,5,21,20,7,3])).
% 76.95/77.03 cnf(1132,plain,
% 76.95/77.03 (P1(x11321,f3(f3(a6,f3(x11322,a6)),f3(x11323,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1109,275,1058,369,20,7])).
% 76.95/77.03 cnf(1144,plain,
% 76.95/77.03 (P1(x11441,f3(f3(a6,f3(a2,x11442)),f3(a2,x11443)))),
% 76.95/77.03 inference(scs_inference,[],[1109,264,1046,352,20,7])).
% 76.95/77.03 cnf(1156,plain,
% 76.95/77.03 (~E(f3(a6,a2),f3(f3(x11561,a6),f3(x11562,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1109,694,1021,369,102,1108,20,7,3])).
% 76.95/77.03 cnf(1164,plain,
% 76.95/77.03 (P1(x11641,f3(f3(a6,f3(x11642,a6)),f3(a2,x11643)))),
% 76.95/77.03 inference(scs_inference,[],[85,275,1116,352,20,7])).
% 76.95/77.03 cnf(1178,plain,
% 76.95/77.03 (E(f3(f3(a2,x11781),a4),f3(f3(a2,x11781),f3(a1,a2)))),
% 76.95/77.03 inference(scs_inference,[],[759,130,20])).
% 76.95/77.03 cnf(1184,plain,
% 76.95/77.03 (~E(f3(a1,f3(x11841,x11841)),f3(a2,x11842))),
% 76.95/77.03 inference(scs_inference,[],[1051,759,130,369,352,974,20,7,3])).
% 76.95/77.03 cnf(1187,plain,
% 76.95/77.03 (E(f3(f3(a2,x11871),f3(a1,a2)),f3(f3(a2,x11871),a4))),
% 76.95/77.03 inference(scs_inference,[],[1051,759,130,369,352,974,20,7,3,2])).
% 76.95/77.03 cnf(1223,plain,
% 76.95/77.03 (~E(a2,f3(a6,f3(x12231,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1039,966,183,369,3,7,5])).
% 76.95/77.03 cnf(1232,plain,
% 76.95/77.03 (P1(f3(a1,x12321),f3(f3(a1,a2),f3(x12322,a6)))),
% 76.95/77.03 inference(scs_inference,[],[275,912,369,1223,20,7])).
% 76.95/77.03 cnf(1234,plain,
% 76.95/77.03 (~E(f3(f3(a6,a2),a2),f3(f3(x12341,a6),x12342))),
% 76.95/77.03 inference(scs_inference,[],[275,912,967,369,832,1223,20,7,3])).
% 76.95/77.03 cnf(1235,plain,
% 76.95/77.03 (~P1(f3(a6,a2),f3(x12351,a6))),
% 76.95/77.03 inference(scs_inference,[],[275,912,967,369,832,1223,20,7,3,23])).
% 76.95/77.03 cnf(1237,plain,
% 76.95/77.03 (P1(f3(f3(a1,x12371),x12372),f3(f3(a1,a2),f3(x12373,a6)))),
% 76.95/77.03 inference(scs_inference,[],[15,275,912,967,369,832,1223,20,7,3,23,21])).
% 76.95/77.03 cnf(1240,plain,
% 76.95/77.03 (P1(f3(f3(a1,x12401),x12402),f3(f3(f3(a1,a2),f3(x12403,a6)),f3(x12404,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1237,369,7])).
% 76.95/77.03 cnf(1243,plain,
% 76.95/77.03 (~E(a2,f3(a6,f3(a2,x12431)))),
% 76.95/77.03 inference(scs_inference,[],[966,1237,207,369,7,3,5])).
% 76.95/77.03 cnf(1256,plain,
% 76.95/77.03 (~P1(f3(a6,a2),f3(a2,x12561))),
% 76.95/77.03 inference(scs_inference,[],[264,977,352,973,807,1243,20,7,3,23])).
% 76.95/77.03 cnf(1258,plain,
% 76.95/77.03 (~E(a4,f3(f3(a2,a2),a2))),
% 76.95/77.03 inference(scs_inference,[],[264,977,352,973,807,1243,20,7,3,23,4])).
% 76.95/77.03 cnf(1259,plain,
% 76.95/77.03 (~E(f3(a2,x12591),f3(a6,a2))),
% 76.95/77.03 inference(scs_inference,[],[366,1256,6])).
% 76.95/77.03 cnf(1271,plain,
% 76.95/77.03 (~E(f3(f3(a2,a4),x12711),f3(a6,a2))),
% 76.95/77.03 inference(scs_inference,[],[603,1256,6])).
% 76.95/77.03 cnf(1299,plain,
% 76.95/77.03 (E(f3(f3(a1,x12991),x12992),f3(a4,f3(a2,x12993)))+~P1(f3(a4,f3(a2,x12993)),f3(f3(a1,x12991),x12992))),
% 76.95/77.03 inference(scs_inference,[],[497,369,1132,102,972,7,3,20])).
% 76.95/77.03 cnf(1303,plain,
% 76.95/77.03 (P1(f3(a1,x13031),f3(f3(a1,a2),f3(a2,x13032)))),
% 76.95/77.03 inference(scs_inference,[],[912,352,7])).
% 76.95/77.03 cnf(1305,plain,
% 76.95/77.03 (E(f3(f3(x13051,a6),f3(a2,x13052)),f3(f3(f3(a1,a2),a4),f3(a2,x13053)))),
% 76.95/77.03 inference(scs_inference,[],[912,352,365,671,7,3])).
% 76.95/77.03 cnf(1308,plain,
% 76.95/77.03 (P1(f3(f3(a1,x13081),x13082),f3(f3(a1,a2),f3(a2,x13083)))),
% 76.95/77.03 inference(scs_inference,[],[15,912,352,365,671,7,3,2,21])).
% 76.95/77.03 cnf(1334,plain,
% 76.95/77.03 (~E(f3(a4,f3(x13341,a6)),f3(f3(f3(a1,a2),a4),f3(a2,x13342)))),
% 76.95/77.03 inference(scs_inference,[],[973,696,3])).
% 76.95/77.03 cnf(1362,plain,
% 76.95/77.03 (~E(a1,f3(f3(a2,a2),a2))),
% 76.95/77.03 inference(scs_inference,[],[369,1164,974,522,3,7,4])).
% 76.95/77.03 cnf(1449,plain,
% 76.95/77.03 (~E(f3(a2,a2),f3(f3(a1,a2),f3(a2,a2)))),
% 76.95/77.03 inference(scs_inference,[],[416,735,3])).
% 76.95/77.03 cnf(1451,plain,
% 76.95/77.03 (P1(a1,f3(f3(a1,a2),f3(x14511,a6)))),
% 76.95/77.03 inference(scs_inference,[],[342,369,416,735,3,7])).
% 76.95/77.03 cnf(1468,plain,
% 76.95/77.03 (P1(f3(x14681,f3(x14681,a1)),f3(f3(a1,a2),f3(x14682,a6)))),
% 76.95/77.03 inference(scs_inference,[],[635,369,1187,1108,3,7])).
% 76.95/77.03 cnf(1474,plain,
% 76.95/77.03 (~E(f3(a4,f3(x14741,a6)),f3(f3(x14742,a6),f3(a2,x14743)))),
% 76.95/77.03 inference(scs_inference,[],[1305,1334,3])).
% 76.95/77.03 cnf(1488,plain,
% 76.95/77.03 (P1(a1,f3(f3(a1,a2),f3(a2,x14881)))),
% 76.95/77.03 inference(scs_inference,[],[342,352,7])).
% 76.95/77.03 cnf(1498,plain,
% 76.95/77.03 (E(f3(a1,f3(x14981,a6)),f3(f3(a1,a2),f3(x14982,a6)))+~P1(f3(f3(a1,a2),f3(x14982,a6)),a1)),
% 76.95/77.03 inference(scs_inference,[],[579,369,383,1451,7,20,3])).
% 76.95/77.03 cnf(1509,plain,
% 76.95/77.03 (P1(f3(a1,x15091),f3(f3(f3(a1,a2),f3(x15092,a6)),f3(x15093,a6)))),
% 76.95/77.03 inference(scs_inference,[],[369,1232,7])).
% 76.95/77.03 cnf(1530,plain,
% 76.95/77.03 (P1(f3(a1,x15301),f3(f3(f3(a1,a2),f3(x15302,a6)),f3(a2,x15303)))),
% 76.95/77.03 inference(scs_inference,[],[352,1232,7])).
% 76.95/77.03 cnf(1538,plain,
% 76.95/77.03 (P1(f3(a1,x15381),f3(f3(f3(a1,a2),f3(a2,x15382)),f3(x15383,a6)))),
% 76.95/77.03 inference(scs_inference,[],[369,1303,7])).
% 76.95/77.03 cnf(1552,plain,
% 76.95/77.03 (P1(a1,f3(f3(f3(a1,a2),f3(x15521,a6)),f3(x15522,a6)))),
% 76.95/77.03 inference(scs_inference,[],[369,1451,7])).
% 76.95/77.03 cnf(1559,plain,
% 76.95/77.03 (P1(f3(a1,x15591),f3(f3(f3(a1,a2),f3(a2,x15592)),f3(a2,x15593)))),
% 76.95/77.03 inference(scs_inference,[],[352,1303,7])).
% 76.95/77.03 cnf(1573,plain,
% 76.95/77.03 (P1(a1,f3(f3(f3(a1,a2),f3(x15731,a6)),f3(a2,x15732)))),
% 76.95/77.03 inference(scs_inference,[],[352,1451,7])).
% 76.95/77.03 cnf(1580,plain,
% 76.95/77.03 (P1(f3(f3(a1,x15801),x15802),f3(a1,f3(x15803,x15803)))),
% 76.95/77.03 inference(scs_inference,[],[1100,365,7])).
% 76.95/77.03 cnf(1583,plain,
% 76.95/77.03 (E(f3(a1,f3(a1,a1)),f3(f3(a1,a2),f3(a2,x15831)))),
% 76.95/77.03 inference(scs_inference,[],[1100,365,921,7,20])).
% 76.95/77.03 cnf(1587,plain,
% 76.95/77.03 (E(f3(f3(a1,a2),f3(a2,a2)),f3(a1,f3(a1,a1)))),
% 76.95/77.03 inference(scs_inference,[],[1100,365,921,1449,7,20,3,2])).
% 76.95/77.03 cnf(1588,plain,
% 76.95/77.03 (E(f3(f3(a1,a2),f3(a2,x15881)),f3(a1,f3(a1,a1)))),
% 76.95/77.03 inference(scs_inference,[],[1583,2])).
% 76.95/77.03 cnf(1589,plain,
% 76.95/77.03 (E(f3(a1,f3(a1,a1)),f3(f3(a1,a2),f3(x15891,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1468,1583,1580,2,20])).
% 76.95/77.03 cnf(1594,plain,
% 76.95/77.03 (P1(f3(f3(a1,x15941),x15942),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[1237,1058,365,1468,1587,1583,1580,2,20,3,7])).
% 76.95/77.03 cnf(1597,plain,
% 76.95/77.03 (P1(f3(f3(f3(a1,x15971),x15972),x15973),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[15,1237,1058,365,1468,1587,1583,1580,2,20,3,7,21])).
% 76.95/77.03 cnf(1600,plain,
% 76.95/77.03 (~E(f3(f3(f3(a1,x16001),x16002),x16003),a4)),
% 76.95/77.03 inference(scs_inference,[],[15,1237,1058,365,1468,1587,1583,1580,146,2,20,3,7,21,6])).
% 76.95/77.03 cnf(1603,plain,
% 76.95/77.03 (~E(f3(f3(f3(a1,x16031),x16032),x16033),a4)),
% 76.95/77.03 inference(rename_variables,[],[1600])).
% 76.95/77.03 cnf(1605,plain,
% 76.95/77.03 (~E(f3(f3(f3(a1,x16051),x16052),x16053),a4)),
% 76.95/77.03 inference(rename_variables,[],[1600])).
% 76.95/77.03 cnf(1607,plain,
% 76.95/77.03 (~P1(a4,f3(f3(f3(a1,x16071),x16072),x16073))),
% 76.95/77.03 inference(scs_inference,[],[726,1600,1603,1605,1589,611,583,2,20])).
% 76.95/77.03 cnf(1610,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),f3(f3(a1,a2),f3(a2,x16101)))),
% 76.95/77.03 inference(scs_inference,[],[726,1600,1603,1605,1058,1588,1589,611,583,2,20,3])).
% 76.95/77.03 cnf(1611,plain,
% 76.95/77.03 (P1(f3(f3(a1,x16111),x16112),a1)),
% 76.95/77.03 inference(scs_inference,[],[726,1600,1603,1605,1058,365,1588,1589,1580,611,583,2,20,3,7])).
% 76.95/77.03 cnf(1614,plain,
% 76.95/77.03 (E(f3(a1,f3(x16141,a6)),f3(f3(a1,a2),f3(x16142,a6)))),
% 76.95/77.03 inference(scs_inference,[],[726,1600,1603,1605,1058,365,1588,1589,1580,611,583,2,20,3,7,1498])).
% 76.95/77.03 cnf(1619,plain,
% 76.95/77.03 (P1(f3(f3(f3(a1,x16191),x16192),x16193),a1)),
% 76.95/77.03 inference(scs_inference,[],[15,1614,1611,2,21])).
% 76.95/77.03 cnf(1622,plain,
% 76.95/77.03 (~P1(f3(f3(a1,a2),f3(a2,x16221)),f3(f3(a1,a2),a4))),
% 76.95/77.03 inference(scs_inference,[],[15,349,1610,1614,1611,2,21,20])).
% 76.95/77.03 cnf(1635,plain,
% 76.95/77.03 (~P1(a1,f3(f3(f3(a1,a2),a4),x16351))),
% 76.95/77.03 inference(scs_inference,[],[1003,1619,20])).
% 76.95/77.03 cnf(1667,plain,
% 76.95/77.03 (E(f3(f3(a1,a2),f3(x16671,a6)),a1)),
% 76.95/77.03 inference(scs_inference,[],[1451,1611,20,2])).
% 76.95/77.03 cnf(1676,plain,
% 76.95/77.03 (E(f3(f3(a1,a2),f3(a2,x16761)),f3(f3(f3(a1,a2),f3(x16762,a6)),f3(x16763,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1597,365,1509,20,3])).
% 76.95/77.03 cnf(1678,plain,
% 76.95/77.03 (E(f3(f3(f3(a1,a2),f3(x16781,a6)),f3(x16782,a6)),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[1597,365,1509,20,3,2])).
% 76.95/77.03 cnf(1679,plain,
% 76.95/77.03 (E(f3(f3(f3(a1,a2),f3(x16791,a6)),f3(x16792,a6)),f3(f3(a1,a2),f3(a2,x16793)))),
% 76.95/77.03 inference(scs_inference,[],[1676,2])).
% 76.95/77.03 cnf(1680,plain,
% 76.95/77.03 (E(f3(a1,a2),f3(f3(f3(a1,a2),f3(x16801,a6)),f3(a2,x16802)))),
% 76.95/77.03 inference(scs_inference,[],[1597,1530,1676,2,20])).
% 76.95/77.03 cnf(1683,plain,
% 76.95/77.03 (~P1(x16831,x16832)+E(x16831,x16832)+~P1(x16832,x16831)),
% 76.95/77.03 inference(rename_variables,[],[20])).
% 76.95/77.03 cnf(1684,plain,
% 76.95/77.03 (P1(f3(f3(x16841,x16842),f3(x16843,x16842)),f3(f3(f3(x16841,x16843),x16842),f3(a2,x16844)))),
% 76.95/77.03 inference(scs_inference,[],[16,214,1597,1530,1676,2,20,21])).
% 76.95/77.03 cnf(1687,plain,
% 76.95/77.03 (~E(f3(a2,a2),f3(f3(f3(a1,a2),f3(x16871,a6)),f3(x16872,a6)))),
% 76.95/77.03 inference(scs_inference,[],[16,214,1597,1530,1676,1449,2,20,21,3])).
% 76.95/77.03 cnf(1688,plain,
% 76.95/77.03 (~E(f3(f3(a1,a4),f3(a2,a4)),a1)),
% 76.95/77.03 inference(scs_inference,[],[16,214,1597,1530,1676,1635,1449,2,20,21,3,6])).
% 76.95/77.03 cnf(1690,plain,
% 76.95/77.03 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[16,214,1597,1530,1676,1635,1449,2,20,21,3,6,36])).
% 76.95/77.03 cnf(1691,plain,
% 76.95/77.03 (E(f3(f3(a1,a4),f3(a2,a4)),f3(f3(a1,a2),a4))),
% 76.95/77.03 inference(scs_inference,[],[16,214,1109,1597,1530,1676,1635,1449,2,20,21,3,6,36,1683])).
% 76.95/77.03 cnf(1696,plain,
% 76.95/77.03 (E(f3(f3(x16961,a6),f3(x16962,a6)),f3(f3(f3(x16961,x16962),a6),f3(a2,x16963)))),
% 76.95/77.03 inference(scs_inference,[],[848,1684,1691,2,20])).
% 76.95/77.03 cnf(1703,plain,
% 76.95/77.03 (~E(f3(a6,a2),f3(f3(a1,a4),f3(a2,a4)))),
% 76.95/77.03 inference(scs_inference,[],[16,187,848,1684,954,1691,2,20,21,3])).
% 76.95/77.03 cnf(1705,plain,
% 76.95/77.03 (E(f3(a1,a2),f3(f3(f3(a1,a2),f3(a2,x17051)),f3(x17052,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1597,1538,1680,2,20])).
% 76.95/77.03 cnf(1709,plain,
% 76.95/77.03 (P1(f3(f3(a1,a4),f3(a2,a4)),x17091)),
% 76.95/77.03 inference(scs_inference,[],[16,1109,1597,1538,1680,2,20,21])).
% 76.95/77.03 cnf(1712,plain,
% 76.95/77.03 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(a1,a5))),
% 76.95/77.03 inference(scs_inference,[],[16,1109,17,1597,1538,1680,2,20,21,6])).
% 76.95/77.03 cnf(1713,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a4),f3(f3(f3(a1,a2),f3(x17131,a6)),f3(x17132,a6)))),
% 76.95/77.03 inference(scs_inference,[],[16,1109,17,1597,1538,1680,1679,1610,2,20,21,6,3])).
% 76.95/77.03 cnf(1719,plain,
% 76.95/77.03 (P1(f3(f3(x17191,x17192),f3(a6,x17192)),x17193)),
% 76.95/77.03 inference(scs_inference,[],[16,848,1712,1709,1705,2,20,21])).
% 76.95/77.03 cnf(1723,plain,
% 76.95/77.03 (~E(f3(f3(x17231,x17232),f3(a6,x17232)),f3(a1,a5))),
% 76.95/77.03 inference(scs_inference,[],[16,17,848,1712,1709,1705,2,20,21,6])).
% 76.95/77.03 cnf(1724,plain,
% 76.95/77.03 (~E(f3(a2,a2),f3(f3(a1,a2),f3(a2,x17241)))),
% 76.95/77.03 inference(scs_inference,[],[16,17,848,1712,1709,1687,1705,1676,2,20,21,6,3])).
% 76.95/77.03 cnf(1733,plain,
% 76.95/77.03 (P1(f3(f3(f3(a1,a2),x17331),f3(a4,x17331)),x17332)),
% 76.95/77.03 inference(scs_inference,[],[16,1116,54,1719,1696,2,20,21])).
% 76.95/77.03 cnf(1740,plain,
% 76.95/77.03 (P1(f3(f3(x17401,x17402),f3(a4,x17402)),f3(x17401,f3(a1,a2)))),
% 76.95/77.03 inference(scs_inference,[],[16,603,21])).
% 76.95/77.03 cnf(1744,plain,
% 76.95/77.03 (~P1(a1,f3(f3(a1,a4),f3(a2,a4)))),
% 76.95/77.03 inference(scs_inference,[],[16,603,1688,1709,21,20])).
% 76.95/77.03 cnf(1749,plain,
% 76.95/77.03 (~E(a1,f3(a2,x17491))),
% 76.95/77.03 inference(scs_inference,[],[16,17,603,1733,1688,1709,167,1036,21,20,6,3])).
% 76.95/77.03 cnf(1753,plain,
% 76.95/77.03 (~E(a4,f3(a1,a4))),
% 76.95/77.03 inference(scs_inference,[],[16,17,603,1733,1688,1709,167,1036,21,20,6,3,257,252,325,4])).
% 76.95/77.03 cnf(1755,plain,
% 76.95/77.03 (P1(f3(f3(x17551,x17552),f3(a4,x17552)),f3(x17551,f3(a1,a2)))),
% 76.95/77.03 inference(rename_variables,[],[1740])).
% 76.95/77.03 cnf(1766,plain,
% 76.95/77.03 (E(f3(f3(a2,x17661),f3(a1,a2)),f3(f3(f3(a2,x17661),x17662),f3(a4,x17662)))),
% 76.95/77.03 inference(scs_inference,[],[16,759,1256,1740,1755,384,163,961,20,21,6,3,2])).
% 76.95/77.03 cnf(1767,plain,
% 76.95/77.03 (P1(f3(f3(x17671,x17672),f3(x17673,x17672)),f3(x17671,x17673))),
% 76.95/77.03 inference(scs_inference,[],[16,15,21])).
% 76.95/77.03 cnf(1770,plain,
% 76.95/77.03 (E(f3(f3(a2,x17701),f3(a4,x17701)),f3(a2,f3(a1,a2)))),
% 76.95/77.03 inference(scs_inference,[],[16,741,1740,15,21,20])).
% 76.95/77.03 cnf(1774,plain,
% 76.95/77.03 (~E(f3(f3(a4,x17741),f3(a5,x17741)),f3(a1,a5))),
% 76.95/77.03 inference(scs_inference,[],[16,17,741,1740,15,21,20,6])).
% 76.95/77.03 cnf(1779,plain,
% 76.95/77.03 (P1(f3(f3(a4,x17791),f3(a5,x17791)),f3(f3(a4,a5),f3(x17792,a6)))),
% 76.95/77.03 inference(scs_inference,[],[16,17,741,1740,15,369,1124,1766,21,20,6,3,2,7])).
% 76.95/77.03 cnf(1785,plain,
% 76.95/77.03 (P1(f3(f3(x17851,a4),f3(x17852,a4)),f3(f3(x17851,x17852),f3(a1,a2)))),
% 76.95/77.03 inference(scs_inference,[],[16,835,1767,130,20,21])).
% 76.95/77.03 cnf(1795,plain,
% 76.95/77.03 (P1(f3(f3(f3(a4,x17951),f3(a5,x17951)),f3(x17952,a6)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[16,835,1767,130,365,369,1072,1770,1779,20,21,6,3,23,7])).
% 76.95/77.03 cnf(1797,plain,
% 76.95/77.03 (P1(f3(f3(x17971,x17972),f3(f3(x17971,a1),x17972)),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[16,805,21])).
% 76.95/77.03 cnf(1801,plain,
% 76.95/77.03 (E(f3(f3(a2,a4),f3(x18011,a4)),f3(f3(a2,x18011),f3(a1,a2)))),
% 76.95/77.03 inference(scs_inference,[],[16,759,1785,805,21,20])).
% 76.95/77.03 cnf(1813,plain,
% 76.95/77.03 (~E(f3(a2,a2),f3(a1,f3(x18131,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1797,1240,1724,1713,146,1614,20,6,3])).
% 76.95/77.03 cnf(1843,plain,
% 76.95/77.03 (E(a1,f3(f3(f3(a1,a2),f3(x18431,a6)),f3(x18432,a6)))),
% 76.95/77.03 inference(scs_inference,[],[1619,1552,20])).
% 76.95/77.03 cnf(1855,plain,
% 76.95/77.03 (E(a1,f3(f3(f3(a1,a2),f3(x18551,a6)),f3(a2,x18552)))),
% 76.95/77.03 inference(scs_inference,[],[1619,1573,20])).
% 76.95/77.03 cnf(1870,plain,
% 76.95/77.03 (P1(a1,f3(f3(f3(a1,a2),f3(a2,x18701)),f3(a2,x18702)))),
% 76.95/77.03 inference(scs_inference,[],[352,1488,7])).
% 76.95/77.03 cnf(1871,plain,
% 76.95/77.03 (E(x18711,f3(x18711,f3(a2,x18712)))),
% 76.95/77.03 inference(rename_variables,[],[352])).
% 76.95/77.03 cnf(1872,plain,
% 76.95/77.03 (P1(f3(f3(f3(a4,x18721),f3(a5,x18721)),f3(a2,x18722)),f3(f3(a4,a5),f3(x18723,a6)))),
% 76.95/77.03 inference(scs_inference,[],[352,1871,1488,1779,7,6])).
% 76.95/77.03 cnf(1874,plain,
% 76.95/77.03 (E(a1,f3(f3(f3(a1,a2),f3(a2,x18741)),f3(a2,x18742)))),
% 76.95/77.03 inference(scs_inference,[],[1619,352,1871,1488,1779,7,6,20])).
% 76.95/77.03 cnf(1886,plain,
% 76.95/77.03 (P1(f3(a1,x18861),f3(f3(f3(f3(a1,a2),f3(x18862,a6)),f3(x18863,a6)),f3(x18864,a6)))),
% 76.95/77.03 inference(scs_inference,[],[369,1509,7])).
% 76.95/77.03 cnf(1900,plain,
% 76.95/77.03 (P1(f3(f3(f3(a4,x19001),f3(a5,x19001)),f3(a2,x19002)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[1872,365,7])).
% 76.95/77.03 cnf(1902,plain,
% 76.95/77.03 (E(f3(x19021,f3(a2,x19022)),x19021)),
% 76.95/77.03 inference(rename_variables,[],[365])).
% 76.95/77.03 cnf(1908,plain,
% 76.95/77.03 (E(f3(f3(a4,a5),f3(x19081,a6)),f3(f3(a4,x19082),f3(a5,x19082)))+~P1(f3(f3(a4,a5),f3(x19081,a6)),f3(f3(a4,x19082),f3(a5,x19082)))),
% 76.95/77.03 inference(scs_inference,[],[17,1872,365,1902,1779,7,6,20,3,2])).
% 76.95/77.03 cnf(2079,plain,
% 76.95/77.03 (E(f3(f3(a1,x20791),x20792),f3(a4,f3(a2,x20793)))+~P1(f3(a4,f3(f3(a1,x20791),x20792)),f3(a2,x20793))),
% 76.95/77.03 inference(scs_inference,[],[1299,23])).
% 76.95/77.03 cnf(2111,plain,
% 76.95/77.03 (~E(f3(a2,x21111),f3(a1,f3(a4,a5)))),
% 76.95/77.03 inference(scs_inference,[],[26,741,6])).
% 76.95/77.03 cnf(2120,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a5),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[26,1733,6,4,36])).
% 76.95/77.03 cnf(2133,plain,
% 76.95/77.03 (~E(a2,f3(a1,f3(a4,a5)))),
% 76.95/77.03 inference(scs_inference,[],[26,13,6])).
% 76.95/77.03 cnf(2136,plain,
% 76.95/77.03 (~P1(f3(a4,f3(f3(a1,x21361),f3(a1,x21361))),f3(a2,a6))),
% 76.95/77.03 inference(scs_inference,[],[973,2079,2])).
% 76.95/77.03 cnf(2139,plain,
% 76.95/77.03 (P1(f3(x21391,f3(x21391,a2)),f3(x21392,x21392))),
% 76.95/77.03 inference(scs_inference,[],[28,120,2136,23,7])).
% 76.95/77.03 cnf(2144,plain,
% 76.95/77.03 (~E(f3(a4,f3(x21441,a6)),f3(x21442,f3(x21442,a2)))),
% 76.95/77.03 inference(scs_inference,[],[28,839,120,2136,973,23,7,20,3])).
% 76.95/77.03 cnf(2177,plain,
% 76.95/77.03 (~E(a2,f3(f3(a1,a5),f3(a2,x21771)))),
% 76.95/77.03 inference(scs_inference,[],[29,365,3])).
% 76.95/77.03 cnf(2188,plain,
% 76.95/77.03 (~P1(f3(a1,a2),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[31,120,2133,13,6,20,5,23])).
% 76.95/77.03 cnf(2196,plain,
% 76.95/77.03 (~E(a6,f3(f3(a4,a5),f3(a2,x21961)))),
% 76.95/77.03 inference(scs_inference,[],[34,365,3])).
% 76.95/77.03 cnf(2198,plain,
% 76.95/77.03 (~E(a6,f3(f3(a4,a5),f3(x21981,a6)))),
% 76.95/77.03 inference(scs_inference,[],[34,383,3])).
% 76.95/77.03 cnf(2200,plain,
% 76.95/77.03 (~E(f3(x22001,f3(x22001,a5)),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[38,120,6])).
% 76.95/77.03 cnf(2204,plain,
% 76.95/77.03 (~P1(a1,a5)),
% 76.95/77.03 inference(scs_inference,[],[38,120,6,5,157,18])).
% 76.95/77.03 cnf(2213,plain,
% 76.95/77.03 (~E(f3(f3(x22131,x22132),f3(a6,x22132)),f3(a1,a2))),
% 76.95/77.03 inference(scs_inference,[],[38,1719,6])).
% 76.95/77.03 cnf(2226,plain,
% 76.95/77.03 (P1(f3(x22261,f3(x22261,a2)),f3(x22262,a6))),
% 76.95/77.03 inference(scs_inference,[],[40,120,7])).
% 76.95/77.03 cnf(2228,plain,
% 76.95/77.03 (E(f3(x22281,f3(x22281,a2)),f3(x22282,a6))),
% 76.95/77.03 inference(scs_inference,[],[40,839,120,7,20])).
% 76.95/77.03 cnf(2231,plain,
% 76.95/77.03 (E(f3(x22311,a6),f3(x22312,f3(x22312,a2)))),
% 76.95/77.03 inference(scs_inference,[],[40,839,120,7,20,2])).
% 76.95/77.03 cnf(2248,plain,
% 76.95/77.03 (P1(f3(x22481,x22481),f3(f3(a4,f3(x22482,a6)),f3(a2,x22483)))),
% 76.95/77.03 inference(scs_inference,[],[41,1021,6])).
% 76.95/77.03 cnf(2259,plain,
% 76.95/77.03 (P1(f3(x22591,x22591),f3(a4,f3(x22592,a6)))),
% 76.95/77.03 inference(scs_inference,[],[41,427,6])).
% 76.95/77.03 cnf(2276,plain,
% 76.95/77.03 (E(f3(x22761,x22761),f3(a4,f3(x22762,a6)))+~P1(f3(a4,f3(x22761,x22761)),f3(x22762,a6))),
% 76.95/77.03 inference(scs_inference,[],[41,441,2248,2259,352,7,6,20,23])).
% 76.95/77.03 cnf(2288,plain,
% 76.95/77.03 (P1(f3(x22881,x22881),a4)),
% 76.95/77.03 inference(scs_inference,[],[2259,365,7])).
% 76.95/77.03 cnf(2337,plain,
% 76.95/77.03 (P1(f3(x23371,x23371),f3(f3(f3(f3(a1,a2),f3(x23372,a6)),f3(x23373,a6)),f3(x23374,a6)))),
% 76.95/77.03 inference(scs_inference,[],[41,352,1886,1870,7,6])).
% 76.95/77.03 cnf(2345,plain,
% 76.95/77.03 (P1(f3(x23451,x23451),f3(f3(f3(a1,a2),f3(x23452,a6)),f3(x23453,a6)))),
% 76.95/77.03 inference(scs_inference,[],[2337,383,7])).
% 76.95/77.03 cnf(2406,plain,
% 76.95/77.03 (~E(f3(x24061,x24061),a4)),
% 76.95/77.03 inference(scs_inference,[],[2345,1607,6])).
% 76.95/77.03 cnf(2417,plain,
% 76.95/77.03 (~P1(f3(a4,f3(x24171,x24171)),f3(x24172,a6))),
% 76.95/77.03 inference(scs_inference,[],[973,2276,2])).
% 76.95/77.03 cnf(2418,plain,
% 76.95/77.03 (~P1(a6,f3(x24181,x24181))),
% 76.95/77.03 inference(scs_inference,[],[2417,22])).
% 76.95/77.03 cnf(2419,plain,
% 76.95/77.03 (~P1(f3(a4,f3(x24191,x24191)),f3(x24192,a6))),
% 76.95/77.03 inference(rename_variables,[],[2417])).
% 76.95/77.03 cnf(2423,plain,
% 76.95/77.03 (~P1(a4,f3(x24231,x24231))),
% 76.95/77.03 inference(scs_inference,[],[2417,2419,2406,2288,22,23,20])).
% 76.95/77.03 cnf(2461,plain,
% 76.95/77.03 (P1(f3(f3(a1,x24611),x24612),f3(a1,f3(x24613,a6)))),
% 76.95/77.03 inference(scs_inference,[],[369,1611,7])).
% 76.95/77.03 cnf(2474,plain,
% 76.95/77.03 (P1(f3(f3(a1,x24741),x24742),f3(a1,f3(a2,x24743)))),
% 76.95/77.03 inference(scs_inference,[],[352,1611,7])).
% 76.95/77.03 cnf(2509,plain,
% 76.95/77.03 (~E(f3(x25091,f3(x25091,a5)),f3(a1,a2))),
% 76.95/77.03 inference(rename_variables,[],[2200])).
% 76.95/77.03 cnf(2511,plain,
% 76.95/77.03 (~E(f3(x25111,f3(x25111,a2)),f3(a4,a2))),
% 76.95/77.03 inference(scs_inference,[],[965,912,2200,2226,20,6])).
% 76.95/77.03 cnf(2514,plain,
% 76.95/77.03 (~E(f3(a4,a2),a2)),
% 76.95/77.03 inference(scs_inference,[],[965,912,2200,2509,740,2226,20,6,3,5])).
% 76.95/77.03 cnf(2515,plain,
% 76.95/77.03 (~E(f3(a4,a2),f3(f3(a1,a2),a4))),
% 76.95/77.03 inference(scs_inference,[],[965,912,2200,2509,740,2226,20,6,3,5,157])).
% 76.95/77.03 cnf(2516,plain,
% 76.95/77.03 (~P1(a4,a2)),
% 76.95/77.03 inference(scs_inference,[],[965,912,2200,2509,740,2226,20,6,3,5,157,18])).
% 76.95/77.03 cnf(2519,plain,
% 76.95/77.03 (E(f3(f3(a2,x25191),f3(x25192,x25191)),f3(f3(a2,x25192),x25191))),
% 76.95/77.03 inference(scs_inference,[],[759,47])).
% 76.95/77.03 cnf(2523,plain,
% 76.95/77.03 (E(f3(f3(x25231,f3(x25231,a2)),f3(x25232,x25232)),a2)),
% 76.95/77.03 inference(scs_inference,[],[2139,1744,759,47,117,18])).
% 76.95/77.03 cnf(2525,plain,
% 76.95/77.03 (~E(f3(f3(a1,a5),f3(a4,a5)),a2)),
% 76.95/77.03 inference(scs_inference,[],[17,2139,1744,759,47,117,18,19])).
% 76.95/77.03 cnf(2527,plain,
% 76.95/77.03 (P1(f3(x25271,a4),f3(x25271,f3(x25272,x25272)))),
% 76.95/77.03 inference(scs_inference,[],[17,2139,1744,2288,759,47,117,18,19,22])).
% 76.95/77.03 cnf(2529,plain,
% 76.95/77.03 (E(f3(x25291,f3(x25292,x25292)),f3(x25291,f3(x25293,a6)))),
% 76.95/77.03 inference(scs_inference,[],[17,2139,1744,61,2288,759,47,117,18,19,22,5])).
% 76.95/77.03 cnf(2532,plain,
% 76.95/77.03 (E(f3(f3(x25321,x25321),x25322),f3(f3(x25323,a6),x25322))),
% 76.95/77.03 inference(scs_inference,[],[17,2139,1744,61,2288,602,759,47,117,18,19,22,5,36,4])).
% 76.95/77.03 cnf(2533,plain,
% 76.95/77.03 (E(f3(f3(a1,a4),f3(a2,a4)),a2)),
% 76.95/77.03 inference(scs_inference,[],[17,2139,1744,61,2288,602,1691,759,47,117,18,19,22,5,36,4,157])).
% 76.95/77.03 cnf(2534,plain,
% 76.95/77.03 (P1(f3(x25341,f3(x25342,x25342)),f3(x25341,a2))),
% 76.95/77.03 inference(scs_inference,[],[17,2139,1744,61,2288,602,1691,759,47,117,18,19,22,5,36,4,157,23])).
% 76.95/77.03 cnf(2536,plain,
% 76.95/77.03 (~E(a5,a6)),
% 76.95/77.03 inference(scs_inference,[],[17,86,2139,1744,61,2288,602,1691,759,47,117,18,19,22,5,36,4,157,23,2])).
% 76.95/77.03 cnf(2537,plain,
% 76.95/77.03 (P1(f3(x25371,f3(x25371,a2)),f3(a1,f3(a2,x25372)))),
% 76.95/77.03 inference(scs_inference,[],[17,86,2139,1744,61,2474,2288,602,1691,759,47,117,18,19,22,5,36,4,157,23,2,21])).
% 76.95/77.03 cnf(2538,plain,
% 76.95/77.03 (P1(f3(x25381,f3(x25381,a2)),f3(x25382,x25382))),
% 76.95/77.03 inference(rename_variables,[],[2139])).
% 76.95/77.03 cnf(2541,plain,
% 76.95/77.03 (~P1(f3(a1,a5),f3(f3(a4,a5),f3(x25411,a6)))),
% 76.95/77.03 inference(scs_inference,[],[17,86,2139,1744,61,2474,2288,602,1691,759,383,47,117,18,19,22,5,36,4,157,23,2,21,7])).
% 76.95/77.03 cnf(2542,plain,
% 76.95/77.03 (E(f3(x25421,f3(x25422,a6)),x25421)),
% 76.95/77.03 inference(rename_variables,[],[383])).
% 76.95/77.03 cnf(2543,plain,
% 76.95/77.03 (E(f3(f3(a6,x25431),f3(a6,x25431)),f3(x25432,f3(x25432,a2)))),
% 76.95/77.03 inference(scs_inference,[],[17,86,2139,2538,1744,61,2474,2288,602,1719,1691,759,383,47,117,18,19,22,5,36,4,157,23,2,21,7,20])).
% 76.95/77.03 cnf(2547,plain,
% 76.95/77.03 (~P1(f3(f3(a1,a5),f3(x25471,a6)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[17,86,2139,2538,1744,61,2474,2288,602,1719,1691,759,383,2542,47,117,18,19,22,5,36,4,157,23,2,21,7,20,6])).
% 76.95/77.03 cnf(2549,plain,
% 76.95/77.03 (~E(f3(f3(a2,a2),f3(a1,a2)),a6)),
% 76.95/77.03 inference(scs_inference,[],[17,86,1081,2139,2538,1801,1744,61,2474,2288,602,1719,1691,759,383,2542,47,117,18,19,22,5,36,4,157,23,2,21,7,20,6,3])).
% 76.95/77.03 cnf(2561,plain,
% 76.95/77.03 (P1(f3(x25611,f3(a1,a2)),f3(x25611,a1))),
% 76.95/77.03 inference(scs_inference,[],[2418,2534,2527,970,342,47,117,18,19,22])).
% 76.95/77.03 cnf(2563,plain,
% 76.95/77.03 (E(f3(x25631,f3(a2,x25632)),f3(x25631,f3(x25633,x25633)))),
% 76.95/77.03 inference(scs_inference,[],[2418,2534,2527,69,970,342,47,117,18,19,22,5])).
% 76.95/77.03 cnf(2564,plain,
% 76.95/77.03 (E(f3(f3(a2,x25641),x25642),f3(f3(x25643,x25643),x25642))),
% 76.95/77.03 inference(scs_inference,[],[2418,2534,2527,69,970,342,47,117,18,19,22,5,4])).
% 76.95/77.03 cnf(2565,plain,
% 76.95/77.03 (P1(f3(x25651,f3(x25652,a6)),f3(x25651,a2))),
% 76.95/77.03 inference(scs_inference,[],[2418,2534,2527,69,2226,970,342,47,117,18,19,22,5,4,23])).
% 76.95/77.03 cnf(2567,plain,
% 76.95/77.03 (~E(a5,a4)),
% 76.95/77.03 inference(scs_inference,[],[103,2418,2534,2527,69,2226,970,342,47,117,18,19,22,5,4,23,2])).
% 76.95/77.03 cnf(2568,plain,
% 76.95/77.03 (~P1(f3(a1,f3(x25681,x25681)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[17,103,2418,2534,2527,69,2226,970,399,342,47,117,18,19,22,5,4,23,2,21])).
% 76.95/77.03 cnf(2572,plain,
% 76.95/77.03 (~P1(a6,a5)),
% 76.95/77.03 inference(scs_inference,[],[17,941,103,2536,2418,2534,2527,2533,69,2226,970,399,342,12,47,117,18,19,22,5,4,23,2,21,7,20])).
% 76.95/77.03 cnf(2575,plain,
% 76.95/77.03 (~P1(f3(f3(a1,a5),f3(x25751,x25751)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[17,941,103,2536,2418,2547,2534,2527,2533,2529,69,2226,970,399,342,12,47,117,18,19,22,5,4,23,2,21,7,20,6])).
% 76.95/77.03 cnf(2577,plain,
% 76.95/77.03 (~E(f3(f3(x25771,a6),x25772),a6)),
% 76.95/77.03 inference(scs_inference,[],[17,941,1037,103,2536,2418,2547,2534,2527,2533,2529,865,69,2226,970,399,342,12,47,117,18,19,22,5,4,23,2,21,7,20,6,3])).
% 76.95/77.03 cnf(2578,plain,
% 76.95/77.03 (P1(a1,f3(a4,f3(x25781,x25781)))),
% 76.95/77.03 inference(scs_inference,[],[17,941,1037,103,2536,2418,2547,2534,2527,2533,2529,865,69,2226,970,399,342,12,47,117,18,19,22,5,4,23,2,21,7,20,6,3,257])).
% 76.95/77.03 cnf(2580,plain,
% 76.95/77.03 (E(f3(f3(x25801,x25802),f3(a6,x25802)),f3(f3(x25801,a6),x25802))),
% 76.95/77.03 inference(scs_inference,[],[848,47])).
% 76.95/77.03 cnf(2585,plain,
% 76.95/77.03 (~E(f3(a6,a5),a2)),
% 76.95/77.03 inference(scs_inference,[],[2572,2561,848,47,18,19])).
% 76.95/77.03 cnf(2587,plain,
% 76.95/77.03 (P1(f3(x25871,a4),f3(x25871,f3(a1,x25872)))),
% 76.95/77.03 inference(scs_inference,[],[2572,2561,655,848,47,18,19,22])).
% 76.95/77.03 cnf(2590,plain,
% 76.95/77.03 (E(f3(f3(x25901,a6),x25902),f3(f3(x25903,a6),x25902))),
% 76.95/77.03 inference(scs_inference,[],[2572,2561,73,655,848,47,18,19,22,5,4])).
% 76.95/77.03 cnf(2591,plain,
% 76.95/77.03 (P1(f3(f3(x25911,x25912),f3(x25911,x25913)),f3(x25913,x25912))),
% 76.95/77.03 inference(scs_inference,[],[2572,2561,73,1767,655,848,47,18,19,22,5,4,23])).
% 76.95/77.03 cnf(2593,plain,
% 76.95/77.03 (~E(f3(a4,a5),a4)),
% 76.95/77.03 inference(scs_inference,[],[2572,714,2561,73,1767,655,848,47,18,19,22,5,4,23,2])).
% 76.95/77.03 cnf(2594,plain,
% 76.95/77.03 (~P1(f3(f3(a1,a5),a2),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[2572,714,2575,2561,2565,73,1767,655,848,47,18,19,22,5,4,23,2,21])).
% 76.95/77.03 cnf(2595,plain,
% 76.95/77.03 (P1(f3(x25951,f3(x25952,a6)),f3(x25951,a2))),
% 76.95/77.03 inference(rename_variables,[],[2565])).
% 76.95/77.03 cnf(2599,plain,
% 76.95/77.03 (E(f3(f3(a1,a2),a2),f3(f3(a1,a2),f3(a2,a6)))),
% 76.95/77.03 inference(scs_inference,[],[2516,2572,714,2575,2561,2565,2595,2523,73,1767,1308,655,848,47,18,19,22,5,4,23,2,21,7,20])).
% 76.95/77.03 cnf(2603,plain,
% 76.95/77.03 (~P1(f3(a4,f3(x26031,a6)),a2)),
% 76.95/77.03 inference(scs_inference,[],[2516,2572,714,2575,2561,2565,2595,2523,73,1767,1308,655,848,383,47,18,19,22,5,4,23,2,21,7,20,6])).
% 76.95/77.03 cnf(2605,plain,
% 76.95/77.03 (~E(f3(f3(a2,x26051),a4),f3(a6,a2))),
% 76.95/77.03 inference(scs_inference,[],[2516,2572,714,2575,1271,2561,2565,2595,2519,2523,73,1767,1308,655,848,383,47,18,19,22,5,4,23,2,21,7,20,6,3])).
% 76.95/77.03 cnf(2608,plain,
% 76.95/77.03 (E(f3(f3(f3(x26081,x26082),f3(x26081,x26083)),f3(x26083,x26082)),a2)),
% 76.95/77.03 inference(scs_inference,[],[2591,18])).
% 76.95/77.03 cnf(2614,plain,
% 76.95/77.03 (E(f3(x26141,f3(x26142,a6)),f3(x26141,f3(a2,x26143)))),
% 76.95/77.03 inference(scs_inference,[],[2423,2591,80,912,18,19,22,5])).
% 76.95/77.03 cnf(2616,plain,
% 76.95/77.03 (P1(f3(f3(a1,x26161),f3(a1,a2)),x26162)),
% 76.95/77.03 inference(scs_inference,[],[2423,2591,80,1594,912,18,19,22,5,4,23])).
% 76.95/77.03 cnf(2618,plain,
% 76.95/77.03 (~E(a2,f3(a4,a2))),
% 76.95/77.03 inference(scs_inference,[],[2514,2423,2591,80,1594,912,18,19,22,5,4,23,2])).
% 76.95/77.03 cnf(2619,plain,
% 76.95/77.03 (~P1(f3(f3(a1,a2),f3(a2,x26191)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[17,2514,2423,2591,80,1594,1303,912,18,19,22,5,4,23,2,21])).
% 76.95/77.03 cnf(2625,plain,
% 76.95/77.03 (~P1(f3(a1,a2),a2)),
% 76.95/77.03 inference(scs_inference,[],[17,526,2514,2423,2591,2532,80,1594,1303,912,13,18,19,22,5,4,23,2,21,7,20])).
% 76.95/77.03 cnf(2632,plain,
% 76.95/77.03 (E(f3(f3(a1,x26321),a4),f3(f3(a1,x26321),f3(a1,a2)))),
% 76.95/77.03 inference(scs_inference,[],[17,2567,526,2514,2423,2591,2599,2532,1622,80,1594,1303,912,13,352,18,19,22,5,4,23,2,21,7,20,6,3,138])).
% 76.95/77.03 cnf(2636,plain,
% 76.95/77.03 (~E(f3(f3(a1,a2),a2),a2)),
% 76.95/77.03 inference(scs_inference,[],[2625,2565,18,19])).
% 76.95/77.03 cnf(2638,plain,
% 76.95/77.03 (P1(f3(x26381,a4),f3(x26381,a1))),
% 76.95/77.03 inference(scs_inference,[],[2625,2565,9,18,19,22])).
% 76.95/77.03 cnf(2640,plain,
% 76.95/77.03 (E(f3(x26401,f3(a2,x26402)),f3(x26401,f3(a2,x26403)))),
% 76.95/77.03 inference(scs_inference,[],[2625,84,2565,9,18,19,22,5])).
% 76.95/77.03 cnf(2642,plain,
% 76.95/77.03 (P1(f3(f3(f3(a4,x26421),f3(a5,x26421)),f3(a4,a5)),f3(a2,x26422))),
% 76.95/77.03 inference(scs_inference,[],[2625,84,2565,1900,9,18,19,22,5,4,23])).
% 76.95/77.03 cnf(2644,plain,
% 76.95/77.03 (~E(a2,f3(a6,a5))),
% 76.95/77.03 inference(scs_inference,[],[2585,2625,84,2565,1900,9,18,19,22,5,4,23,2])).
% 76.95/77.03 cnf(2645,plain,
% 76.95/77.03 (P1(f3(f3(a1,x26451),a4),x26452)),
% 76.95/77.03 inference(scs_inference,[],[2585,2625,2616,2587,84,2565,1900,9,18,19,22,5,4,23,2,21])).
% 76.95/77.03 cnf(2655,plain,
% 76.95/77.03 (~E(f3(x26551,f3(x26551,a2)),a5)),
% 76.95/77.03 inference(scs_inference,[],[957,2585,2625,569,2616,2587,2537,2608,2231,1184,84,2565,602,1900,9,18,19,22,5,4,23,2,21,7,20,6,3])).
% 76.95/77.03 cnf(2659,plain,
% 76.95/77.03 (E(f3(f3(x26591,a4),f3(x26591,a1)),a2)),
% 76.95/77.03 inference(scs_inference,[],[2638,18])).
% 76.95/77.03 cnf(2663,plain,
% 76.95/77.03 (P1(f3(x26631,f3(x26632,a1)),f3(x26631,f3(x26632,a4)))),
% 76.95/77.03 inference(scs_inference,[],[2638,2619,18,19,22])).
% 76.95/77.03 cnf(2665,plain,
% 76.95/77.03 (E(f3(x26651,f3(x26652,x26652)),f3(x26651,f3(x26653,x26653)))),
% 76.95/77.03 inference(scs_inference,[],[2638,2619,93,18,19,22,5])).
% 76.95/77.03 cnf(2666,plain,
% 76.95/77.03 (P1(f3(x26661,f3(x26661,a1)),a4)),
% 76.95/77.03 inference(scs_inference,[],[2638,2619,93,18,19,22,5,23])).
% 76.95/77.03 cnf(2669,plain,
% 76.95/77.03 (~E(f3(a1,a2),f3(f3(a1,a4),f3(a2,a4)))),
% 76.95/77.03 inference(scs_inference,[],[2638,1690,2619,93,18,19,22,5,23,4,2])).
% 76.95/77.03 cnf(2670,plain,
% 76.95/77.03 (~P1(f3(f3(a1,a2),f3(x26701,a6)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[17,2638,1690,2619,93,1232,18,19,22,5,23,4,2,21])).
% 76.95/77.03 cnf(2673,plain,
% 76.95/77.03 (~P1(a4,f3(a1,a4))),
% 76.95/77.03 inference(scs_inference,[],[17,1753,2638,1690,2619,93,1232,655,18,19,22,5,23,4,2,21,20])).
% 76.95/77.03 cnf(2679,plain,
% 76.95/77.03 (P1(f3(f3(x26791,x26791),a4),f3(f3(a2,x26792),a1))),
% 76.95/77.03 inference(scs_inference,[],[17,1753,2638,989,1690,2619,2564,2580,93,1232,655,18,19,22,5,23,4,2,21,20,7,6])).
% 76.95/77.03 cnf(2682,plain,
% 76.95/77.03 (~E(f3(f3(a2,a2),a2),f3(a6,a2))),
% 76.95/77.03 inference(scs_inference,[],[17,956,1753,2638,989,1690,2619,2564,2580,435,93,1232,655,18,19,22,5,23,4,2,21,20,7,6,3])).
% 76.95/77.03 cnf(2685,plain,
% 76.95/77.03 (P1(f3(x26851,x26852),f3(x26851,a2))),
% 76.95/77.03 inference(scs_inference,[],[2226,13,18,22])).
% 76.95/77.03 cnf(2689,plain,
% 76.95/77.03 (E(f3(x26891,f3(x26892,x26892)),f3(x26891,f3(a2,x26893)))),
% 76.95/77.03 inference(scs_inference,[],[2673,62,2226,13,18,22,19,5])).
% 76.95/77.03 cnf(2690,plain,
% 76.95/77.03 (P1(f3(f3(a1,a4),x26901),f3(a2,a4))),
% 76.95/77.03 inference(scs_inference,[],[2673,62,2226,1709,13,18,22,19,5,23])).
% 76.95/77.03 cnf(2693,plain,
% 76.95/77.03 (~E(f3(a1,a2),f3(f3(a1,a2),a5))),
% 76.95/77.03 inference(scs_inference,[],[2673,2120,62,2226,1709,13,18,22,19,5,23,4,2])).
% 76.95/77.03 cnf(2694,plain,
% 76.95/77.03 (~P1(a4,f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[2673,2120,2568,2666,62,2226,1709,13,18,22,19,5,23,4,2,21])).
% 76.95/77.03 cnf(2702,plain,
% 76.95/77.03 (E(f3(x27021,f3(x27022,a6)),x27021)),
% 76.95/77.03 inference(rename_variables,[],[383])).
% 76.95/77.03 cnf(2703,plain,
% 76.95/77.03 (~P1(f3(a4,f3(x27031,a6)),f3(a1,a4))),
% 76.95/77.03 inference(scs_inference,[],[2673,2120,2670,2568,2515,2645,2666,62,2226,1709,383,2702,13,18,22,19,5,23,4,2,21,20,7,6])).
% 76.95/77.03 cnf(2707,plain,
% 76.95/77.03 (E(f3(f3(x27071,x27072),f3(x27071,a2)),a2)),
% 76.95/77.03 inference(scs_inference,[],[2685,18])).
% 76.95/77.03 cnf(2709,plain,
% 76.95/77.03 (~E(f3(a4,f3(a4,a5)),a2)),
% 76.95/77.03 inference(scs_inference,[],[2685,2694,18,19])).
% 76.95/77.03 cnf(2711,plain,
% 76.95/77.03 (P1(f3(x27111,f3(x27112,a2)),f3(x27111,f3(x27112,x27113)))),
% 76.95/77.03 inference(scs_inference,[],[2685,2694,18,19,22])).
% 76.95/77.03 cnf(2713,plain,
% 76.95/77.03 (P1(f3(x27131,f3(x27131,a2)),x27132)),
% 76.95/77.03 inference(scs_inference,[],[2685,2694,18,19,22,23])).
% 76.95/77.03 cnf(2717,plain,
% 76.95/77.03 (~E(f3(a6,a2),f3(f3(a2,a2),a2))),
% 76.95/77.03 inference(scs_inference,[],[2685,2694,2682,58,18,19,22,23,5,4,2])).
% 76.95/77.03 cnf(2721,plain,
% 76.95/77.03 (~P1(f3(a4,a2),a2)),
% 76.95/77.03 inference(scs_inference,[],[2685,2694,2618,2682,58,1122,13,18,19,22,23,5,4,2,21,20])).
% 76.95/77.03 cnf(2725,plain,
% 76.95/77.03 (~P1(f3(a4,f3(x27251,x27251)),f3(a1,a4))),
% 76.95/77.03 inference(scs_inference,[],[2685,2694,2618,2682,2703,2659,2603,2665,58,1122,13,18,19,22,23,5,4,2,21,20,7,6])).
% 76.95/77.03 cnf(2729,plain,
% 76.95/77.03 (E(f3(a1,a4),f3(a1,f3(a1,a2)))),
% 76.95/77.03 inference(scs_inference,[],[56,2685,2694,2618,2682,2703,2659,2603,2665,1874,58,1122,13,18,19,22,23,5,4,2,21,20,7,6,3,138])).
% 76.95/77.03 cnf(2734,plain,
% 76.95/77.03 (P1(f3(x27341,x27342),f3(x27341,f3(x27342,x27343)))),
% 76.95/77.03 inference(scs_inference,[],[2690,15,18,22])).
% 76.95/77.03 cnf(2738,plain,
% 76.95/77.03 (P1(f3(f3(f3(a4,x27381),f3(a5,x27381)),f3(a4,a5)),f3(x27382,a6))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,1795,15,18,22,19,23])).
% 76.95/77.03 cnf(2740,plain,
% 76.95/77.03 (E(f3(x27401,f3(a1,a2)),f3(x27401,a1))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,1795,8,15,18,22,19,23,5])).
% 76.95/77.03 cnf(2741,plain,
% 76.95/77.03 (E(f3(f3(a1,a2),x27411),f3(a1,x27411))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,1795,8,15,18,22,19,23,5,4])).
% 76.95/77.03 cnf(2742,plain,
% 76.95/77.03 (~E(f3(a4,a2),f3(x27421,f3(x27421,a2)))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,2511,1795,8,15,18,22,19,23,5,4,2])).
% 76.95/77.03 cnf(2743,plain,
% 76.95/77.03 (P1(f3(f3(a1,a4),x27431),f3(a2,f3(x27432,x27432)))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,2511,2527,1795,8,15,18,22,19,23,5,4,2,21])).
% 76.95/77.03 cnf(2746,plain,
% 76.95/77.03 (E(f3(a2,a4),f3(f3(a1,a4),x27461))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,2511,2527,1795,741,8,15,18,22,19,23,5,4,2,21,20])).
% 76.95/77.03 cnf(2749,plain,
% 76.95/77.03 (~P1(f3(a4,a2),f3(f3(x27491,x27492),f3(x27491,a2)))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,2511,2707,2527,1795,741,8,15,18,22,19,23,5,4,2,21,20,7])).
% 76.95/77.03 cnf(2752,plain,
% 76.95/77.03 (~E(f3(f3(a2,x27521),f3(a1,a2)),f3(a6,a2))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,2511,2605,2707,1178,2527,602,1795,741,8,15,18,22,19,23,5,4,2,21,20,7,6,3])).
% 76.95/77.03 cnf(2754,plain,
% 76.95/77.03 (E(f3(f3(x27541,x27542),f3(x27542,x27542)),f3(f3(x27541,x27542),x27542))),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,2511,2605,2707,1178,2527,602,1795,741,8,15,18,22,19,23,5,4,2,21,20,7,6,3,47])).
% 76.95/77.03 cnf(2756,plain,
% 76.95/77.03 (E(f3(f3(a1,a2),a2),a1)),
% 76.95/77.03 inference(scs_inference,[],[2721,2690,2511,2605,2707,1178,2527,602,1795,741,8,15,18,22,19,23,5,4,2,21,20,7,6,3,47,36])).
% 76.95/77.03 cnf(2758,plain,
% 76.95/77.03 (E(f3(f3(x27581,x27581),a4),a2)),
% 76.95/77.03 inference(scs_inference,[],[2288,18])).
% 76.95/77.03 cnf(2762,plain,
% 76.95/77.03 (P1(f3(f3(x27621,x27622),x27623),f3(a6,x27622))),
% 76.95/77.03 inference(scs_inference,[],[2594,2288,1719,18,19,23])).
% 76.95/77.03 cnf(2764,plain,
% 76.95/77.03 (E(f3(x27641,a2),f3(x27641,f3(a2,x27642)))),
% 76.95/77.03 inference(scs_inference,[],[2594,2288,1719,51,18,19,23,5])).
% 76.95/77.03 cnf(2766,plain,
% 76.95/77.03 (~E(f3(a1,a5),f3(f3(x27661,x27662),f3(a6,x27662)))),
% 76.95/77.03 inference(scs_inference,[],[1723,2594,2288,1719,51,18,19,23,5,4,2])).
% 76.95/77.03 cnf(2767,plain,
% 76.95/77.03 (~P1(f3(a1,f3(a5,x27671)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[17,1723,2594,2734,2288,1719,51,18,19,23,5,4,2,21])).
% 76.95/77.03 cnf(2770,plain,
% 76.95/77.03 (~P1(f3(a6,a5),a2)),
% 76.95/77.03 inference(scs_inference,[],[17,2644,1723,2594,2734,2288,1719,51,13,18,19,23,5,4,2,21,20])).
% 76.95/77.03 cnf(2774,plain,
% 76.95/77.03 (E(f3(f3(a1,a2),x27741),f3(a1,x27741))),
% 76.95/77.03 inference(rename_variables,[],[2741])).
% 76.95/77.03 cnf(2775,plain,
% 76.95/77.03 (~P1(f3(f3(a1,a2),a5),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[17,2644,1723,2594,2725,2741,2774,2734,2288,1719,51,13,18,19,23,5,4,2,21,20,7,6])).
% 76.95/77.03 cnf(2777,plain,
% 76.95/77.03 (~E(f3(f3(a4,a5),f3(a2,x27771)),a4)),
% 76.95/77.03 inference(scs_inference,[],[17,2593,2644,1723,2594,2725,2741,2774,2734,2288,1719,51,13,352,18,19,23,5,4,2,21,20,7,6,3])).
% 76.95/77.03 cnf(2784,plain,
% 76.95/77.03 (P1(f3(f3(a1,x27841),a1),x27842)),
% 76.95/77.03 inference(scs_inference,[],[2770,2762,1611,18,19,23])).
% 76.95/77.03 cnf(2786,plain,
% 76.95/77.03 (E(f3(a2,x27861),f3(f3(x27862,a6),x27861))),
% 76.95/77.03 inference(scs_inference,[],[2770,2762,1611,40,18,19,23,4])).
% 76.95/77.03 cnf(2787,plain,
% 76.95/77.03 (E(f3(x27871,a2),f3(x27871,f3(x27872,a6)))),
% 76.95/77.03 inference(scs_inference,[],[2770,2762,1611,40,18,19,23,4,5])).
% 76.95/77.03 cnf(2789,plain,
% 76.95/77.03 (~P1(f3(a6,a2),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[2770,2775,2213,2762,1611,40,18,19,23,4,5,2,21])).
% 76.95/77.03 cnf(2790,plain,
% 76.95/77.03 (P1(f3(f3(x27901,x27902),x27903),f3(a6,x27902))),
% 76.95/77.03 inference(rename_variables,[],[2762])).
% 76.95/77.03 cnf(2792,plain,
% 76.95/77.03 (~P1(f3(a6,a2),f3(f3(a2,a2),a2))),
% 76.95/77.03 inference(scs_inference,[],[2770,2775,2213,2762,2790,2717,1611,40,18,19,23,4,5,2,21,20])).
% 76.95/77.03 cnf(2795,plain,
% 76.95/77.03 (~P1(f3(a6,a5),f3(f3(x27951,x27951),a4))),
% 76.95/77.03 inference(scs_inference,[],[2770,2775,2213,2762,2790,2717,2758,1611,40,18,19,23,4,5,2,21,20,7])).
% 76.95/77.03 cnf(2796,plain,
% 76.95/77.03 (~P1(f3(f3(a6,a5),f3(x27961,a6)),a2)),
% 76.95/77.03 inference(scs_inference,[],[2770,2775,2213,2762,2790,2717,2758,1611,40,383,18,19,23,4,5,2,21,20,7,6])).
% 76.95/77.03 cnf(2804,plain,
% 76.95/77.03 (~E(f3(f3(a6,a2),f3(a4,a5)),a2)),
% 76.95/77.03 inference(scs_inference,[],[2789,1767,18,19])).
% 76.95/77.03 cnf(2806,plain,
% 76.95/77.03 (P1(f3(a1,a4),x28061)),
% 76.95/77.03 inference(scs_inference,[],[2789,1767,655,18,19,23])).
% 76.95/77.03 cnf(2808,plain,
% 76.95/77.03 (E(f3(x28081,a2),f3(x28081,f3(x28082,x28082)))),
% 76.95/77.03 inference(scs_inference,[],[2789,1767,655,28,18,19,23,5])).
% 76.95/77.03 cnf(2809,plain,
% 76.95/77.03 (E(f3(a2,x28091),f3(f3(x28092,x28092),x28091))),
% 76.95/77.03 inference(scs_inference,[],[2789,1767,655,28,18,19,23,5,4])).
% 76.95/77.03 cnf(2810,plain,
% 76.95/77.03 (~E(f3(a6,a2),f3(f3(a2,x28101),f3(a1,a2)))),
% 76.95/77.03 inference(scs_inference,[],[2789,2752,1767,655,28,18,19,23,5,4,2])).
% 76.95/77.03 cnf(2811,plain,
% 76.95/77.03 (~P1(f3(a6,f3(a2,x28111)),f3(a4,a5))),
% 76.95/77.03 inference(scs_inference,[],[2789,2752,2734,1767,655,28,18,19,23,5,4,2,21])).
% 76.95/77.04 cnf(2814,plain,
% 76.95/77.04 (~P1(a6,f3(a2,a6))),
% 76.95/77.04 inference(scs_inference,[],[2789,856,2752,2734,1767,741,655,28,18,19,23,5,4,2,21,20])).
% 76.95/77.04 cnf(2818,plain,
% 76.95/77.04 (~P1(f3(a4,a2),f3(a2,a4))),
% 76.95/77.04 inference(scs_inference,[],[2789,856,2752,2746,2749,2734,1767,741,655,28,18,19,23,5,4,2,21,20,7])).
% 76.95/77.04 cnf(2821,plain,
% 76.95/77.04 (P1(f3(a1,a1),x28211)),
% 76.95/77.04 inference(scs_inference,[],[2789,856,2752,2740,2746,2713,2749,2734,1767,741,655,28,18,19,23,5,4,2,21,20,7,6])).
% 76.95/77.04 cnf(2824,plain,
% 76.95/77.04 (~E(f3(f3(f3(a1,a2),f3(x28241,a6)),f3(x28242,a6)),f3(x28243,x28243))),
% 76.95/77.04 inference(scs_inference,[],[2789,994,856,2752,2740,2746,2713,2749,1843,2734,1767,741,655,28,18,19,23,5,4,2,21,20,7,6,3])).
% 76.95/77.04 cnf(2825,plain,
% 76.95/77.04 (P1(f3(x28251,x28252),f3(x28251,f3(a1,a4)))),
% 76.95/77.04 inference(scs_inference,[],[2789,994,856,2752,2740,2746,2713,2749,1843,2734,1767,741,655,28,18,19,23,5,4,2,21,20,7,6,3,22])).
% 76.95/77.04 cnf(2827,plain,
% 76.95/77.04 (E(f3(f3(a1,a4),x28271),a2)),
% 76.95/77.04 inference(scs_inference,[],[2806,18])).
% 76.95/77.04 cnf(2831,plain,
% 76.95/77.04 (~E(f3(f3(a4,a2),f3(a2,a4)),a2)),
% 76.95/77.04 inference(scs_inference,[],[2806,2818,2821,18,22,19])).
% 76.95/77.04 cnf(2833,plain,
% 76.95/77.04 (P1(f3(x28331,x28331),x28332)),
% 76.95/77.04 inference(scs_inference,[],[2806,2818,2821,15,18,22,19,23])).
% 76.95/77.04 cnf(2835,plain,
% 76.95/77.04 (E(f3(a1,x28351),f3(f3(a1,a2),x28351))),
% 76.95/77.04 inference(scs_inference,[],[2806,2818,2821,96,15,18,22,19,23,4])).
% 76.95/77.04 cnf(2836,plain,
% 76.95/77.04 (E(f3(x28361,a1),f3(x28361,f3(a1,a2)))),
% 76.95/77.04 inference(scs_inference,[],[2806,2818,2821,96,15,18,22,19,23,4,5])).
% 76.95/77.04 cnf(2837,plain,
% 76.95/77.04 (~E(f3(a1,a5),f3(f3(a4,x28371),f3(a5,x28371)))),
% 76.95/77.04 inference(scs_inference,[],[2806,2818,2821,1774,96,15,18,22,19,23,4,5,2])).
% 76.95/77.04 cnf(2838,plain,
% 76.95/77.04 (~P1(f3(a1,f3(a1,a4)),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[17,2806,2818,2821,1774,2825,96,15,18,22,19,23,4,5,2,21])).
% 76.95/77.04 cnf(2852,plain,
% 76.95/77.04 (P1(a1,f3(f3(a1,a2),f3(x28521,x28521)))),
% 76.95/77.04 inference(scs_inference,[],[17,2806,2818,2821,1774,2825,2784,2577,2543,1234,684,602,96,15,18,22,19,23,4,5,2,21,20,7,6,3,325])).
% 76.95/77.04 cnf(2854,plain,
% 76.95/77.04 (E(f3(f3(x28541,x28541),x28542),a2)),
% 76.95/77.04 inference(scs_inference,[],[2833,18])).
% 76.95/77.04 cnf(2856,plain,
% 76.95/77.04 (E(f3(a1,a4),a2)),
% 76.95/77.04 inference(scs_inference,[],[2833,2835,18,157])).
% 76.95/77.04 cnf(2857,plain,
% 76.95/77.04 (E(f3(a1,x28571),f3(f3(a1,a2),x28571))),
% 76.95/77.04 inference(rename_variables,[],[2835])).
% 76.95/77.04 cnf(2858,plain,
% 76.95/77.04 (P1(f3(x28581,x28582),f3(x28581,f3(x28583,x28583)))),
% 76.95/77.04 inference(scs_inference,[],[2833,2835,18,157,22])).
% 76.95/77.04 cnf(2862,plain,
% 76.95/77.04 (E(f3(f3(x28621,x28621),x28622),f3(a2,x28622))),
% 76.95/77.04 inference(scs_inference,[],[2833,2814,2835,14,18,157,22,19,4])).
% 76.95/77.04 cnf(2863,plain,
% 76.95/77.04 (E(f3(x28631,f3(x28632,x28632)),f3(x28631,a2))),
% 76.95/77.04 inference(scs_inference,[],[2833,2814,2835,14,18,157,22,19,4,5])).
% 76.95/77.04 cnf(2868,plain,
% 76.95/77.04 (~P1(f3(a1,a2),f3(f3(a1,a2),a4))),
% 76.95/77.04 inference(scs_inference,[],[2833,2814,757,556,2835,2645,1132,14,18,157,22,19,4,5,2,21,20])).
% 76.95/77.04 cnf(2871,plain,
% 76.95/77.04 (~P1(a6,f3(a1,a4))),
% 76.95/77.04 inference(scs_inference,[],[2833,2814,757,556,1010,2835,2857,2645,1132,14,18,157,22,19,4,5,2,21,20,7])).
% 76.95/77.04 cnf(2873,plain,
% 76.95/77.04 (~P1(f3(f3(a1,a2),a2),a5)),
% 76.95/77.04 inference(scs_inference,[],[2833,2814,757,556,1010,2756,2835,2857,2204,2645,1132,14,18,157,22,19,4,5,2,21,20,7,6])).
% 76.95/77.04 cnf(2874,plain,
% 76.95/77.04 (~E(f3(a6,f3(a2,x28741)),f3(a2,x28742))),
% 76.95/77.04 inference(scs_inference,[],[2833,2814,887,757,556,1010,2756,2835,2857,2204,2645,1132,14,352,18,157,22,19,4,5,2,21,20,7,6,3])).
% 76.95/77.04 cnf(2878,plain,
% 76.95/77.04 (P1(a1,f3(a4,a2))),
% 76.95/77.04 inference(scs_inference,[],[2833,2814,887,757,556,1010,2756,2835,2857,2204,2645,1132,14,352,18,157,22,19,4,5,2,21,20,7,6,3,1908,252])).
% 76.95/77.04 cnf(2880,plain,
% 76.95/77.04 (E(f3(a1,f3(a4,a2)),a2)),
% 76.95/77.04 inference(scs_inference,[],[2878,18])).
% 76.95/77.04 cnf(2882,plain,
% 76.95/77.04 (P1(f3(x28821,f3(a4,a2)),f3(x28821,a1))),
% 76.95/77.04 inference(scs_inference,[],[2878,18,22])).
% 76.95/77.04 cnf(2886,plain,
% 76.95/77.04 (P1(f3(x28861,f3(x28861,a1)),f3(a4,a2))),
% 76.95/77.04 inference(scs_inference,[],[2878,2871,18,22,19,23])).
% 76.95/77.04 cnf(2888,plain,
% 76.95/77.04 (E(f3(f3(a1,a4),x28881),f3(a2,x28881))),
% 76.95/77.04 inference(scs_inference,[],[2878,2856,2871,18,22,19,23,4])).
% 76.95/77.04 cnf(2889,plain,
% 76.95/77.04 (E(f3(x28891,f3(a1,a4)),f3(x28891,a2))),
% 76.95/77.04 inference(scs_inference,[],[2878,2856,2871,18,22,19,23,4,5])).
% 76.95/77.04 cnf(2891,plain,
% 76.95/77.04 (~P1(f3(a4,a2),f3(x28911,a6))),
% 76.95/77.04 inference(scs_inference,[],[2878,2856,2871,2874,1074,18,22,19,23,4,5,2,21])).
% 76.95/77.04 cnf(2898,plain,
% 76.95/77.04 (~P1(f3(a6,f3(x28981,a6)),f3(a1,a4))),
% 76.95/77.04 inference(scs_inference,[],[2878,2856,2871,1013,2862,2874,2852,1074,1611,383,18,22,19,23,4,5,2,21,20,7,6])).
% 76.95/77.04 cnf(2906,plain,
% 76.95/77.04 (~E(f3(f3(a4,a2),f3(x29061,a6)),a2)),
% 76.95/77.04 inference(scs_inference,[],[2891,2886,18,19])).
% 76.95/77.04 cnf(2908,plain,
% 76.95/77.04 (E(f3(f3(a2,x29081),x29082),f3(a2,x29082))),
% 76.95/77.04 inference(scs_inference,[],[2891,2886,11,18,19,4])).
% 76.95/77.04 cnf(2909,plain,
% 76.95/77.04 (E(f3(x29091,f3(a2,x29092)),f3(x29091,a2))),
% 76.95/77.04 inference(scs_inference,[],[2891,2886,11,18,19,4,5])).
% 76.95/77.04 cnf(2911,plain,
% 76.95/77.04 (~P1(f3(a6,f3(x29111,x29111)),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[2891,2886,2811,283,2858,11,18,19,4,5,2,21])).
% 76.95/77.04 cnf(2918,plain,
% 76.95/77.04 (~P1(f3(a6,a2),f3(f3(a2,a2),f3(x29181,x29181)))),
% 76.95/77.04 inference(scs_inference,[],[2891,1098,2886,2863,2811,283,2792,2858,2713,11,18,19,4,5,2,21,20,7])).
% 76.95/77.04 cnf(2920,plain,
% 76.95/77.04 (~P1(f3(a4,f3(a1,a4)),f3(x29201,a6))),
% 76.95/77.04 inference(scs_inference,[],[2891,1098,2886,2863,2889,2811,283,2792,2858,2713,11,18,19,4,5,2,21,20,7,6])).
% 76.95/77.04 cnf(2928,plain,
% 76.95/77.04 (E(f3(f3(x29281,a6),x29282),f3(a2,x29282))),
% 76.95/77.04 inference(scs_inference,[],[2838,2882,10,18,19,4])).
% 76.95/77.04 cnf(2931,plain,
% 76.95/77.04 (~P1(f3(a6,f3(a1,a4)),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[2838,2882,2911,288,2663,10,18,19,4,5,2,21])).
% 76.95/77.04 cnf(2941,plain,
% 76.95/77.04 (~P1(f3(f3(a1,a2),f3(a1,a4)),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[2838,2882,2911,288,2663,2741,2784,383,10,18,19,4,5,2,21,20,7,6])).
% 76.95/77.04 cnf(2943,plain,
% 76.95/77.04 (~E(f3(f3(a1,a5),a2),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[2838,2882,2911,2909,212,288,2663,2741,2784,383,10,18,19,4,5,2,21,20,7,6,3])).
% 76.95/77.04 cnf(2951,plain,
% 76.95/77.04 (E(f3(f3(x29511,a6),x29512),f3(f3(x29513,x29513),x29512))),
% 76.95/77.04 inference(scs_inference,[],[2941,1594,41,18,19,4])).
% 76.95/77.04 cnf(2954,plain,
% 76.95/77.04 (~P1(f3(a4,a2),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[2941,2943,2591,1594,41,18,19,4,5,2,21])).
% 76.95/77.04 cnf(2968,plain,
% 76.95/77.04 (~E(f3(f3(a4,a2),f3(a4,a5)),a2)),
% 76.95/77.04 inference(scs_inference,[],[2954,635,18,19])).
% 76.95/77.04 cnf(2971,plain,
% 76.95/77.04 (P1(f3(f3(a1,a4),x29711),f3(a2,f3(a2,x29712)))),
% 76.95/77.04 inference(scs_inference,[],[2954,394,2711,2743,635,18,19,2,21])).
% 76.95/77.04 cnf(2975,plain,
% 76.95/77.04 (E(f3(a2,a2),f3(f3(f3(a4,x29751),f3(a5,x29751)),f3(a4,a5)))),
% 76.95/77.04 inference(scs_inference,[],[2954,394,2642,2711,2743,2833,635,18,19,2,21,20])).
% 76.95/77.04 cnf(2981,plain,
% 76.95/77.04 (~P1(f3(a4,f3(x29811,x29811)),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[2954,394,2642,2711,2743,2863,2833,635,383,18,19,2,21,20,7,6])).
% 76.95/77.04 cnf(2983,plain,
% 76.95/77.04 (~E(f3(f3(a1,a5),f3(x29831,x29831)),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[2954,223,394,2642,2563,2711,2743,2863,2833,635,383,18,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(2986,plain,
% 76.95/77.04 (E(f3(a1,f3(a1,a2)),a2)),
% 76.95/77.04 inference(scs_inference,[],[342,18])).
% 76.95/77.04 cnf(2991,plain,
% 76.95/77.04 (~P1(f3(a6,f3(x29911,x29911)),f3(a1,a4))),
% 76.95/77.04 inference(scs_inference,[],[2983,2931,2898,2858,342,18,19,2,21])).
% 76.95/77.04 cnf(2994,plain,
% 76.95/77.04 (~P1(a1,f3(a2,f3(a2,a2)))),
% 76.95/77.04 inference(scs_inference,[],[1749,2983,2931,2898,2858,2713,342,18,19,2,21,20])).
% 76.95/77.04 cnf(2995,plain,
% 76.95/77.04 (~E(a1,f3(a2,x29951))),
% 76.95/77.04 inference(rename_variables,[],[1749])).
% 76.95/77.04 cnf(2999,plain,
% 76.95/77.04 (P1(f3(f3(x29991,x29991),f3(a2,a1)),f3(a4,a2))),
% 76.95/77.04 inference(scs_inference,[],[1749,2983,2931,2898,2809,2880,2796,2886,2858,2713,342,18,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3003,plain,
% 76.95/77.04 (P1(f3(f3(x30031,x30031),f3(a4,a2)),f3(a2,a1))),
% 76.95/77.04 inference(scs_inference,[],[1749,2995,2983,2931,2898,2809,2880,2796,1855,2886,2858,2713,342,18,19,2,21,20,7,6,3,23])).
% 76.95/77.04 cnf(3011,plain,
% 76.95/77.04 (P1(f3(f3(x30111,x30111),f3(a2,a1)),f3(a4,f3(a1,a4)))),
% 76.95/77.04 inference(scs_inference,[],[2999,2981,409,2825,18,19,2,21])).
% 76.95/77.04 cnf(3014,plain,
% 76.95/77.04 (E(f3(a2,a1),f3(f3(x30141,x30141),f3(a4,a2)))),
% 76.95/77.04 inference(scs_inference,[],[2999,3003,2981,409,2825,741,18,19,2,21,20])).
% 76.95/77.04 cnf(3019,plain,
% 76.95/77.04 (~P1(f3(a6,a2),f3(a1,a4))),
% 76.95/77.04 inference(scs_inference,[],[2999,3003,2981,2991,409,2808,2825,741,383,18,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3022,plain,
% 76.95/77.04 (~E(a2,a5)),
% 76.95/77.04 inference(scs_inference,[],[2999,3003,2981,2991,409,2808,2986,2655,2825,741,383,18,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3027,plain,
% 76.95/77.04 (~E(f3(f3(a6,a2),f3(a1,a4)),a2)),
% 76.95/77.04 inference(scs_inference,[],[3019,3003,18,19])).
% 76.95/77.04 cnf(3030,plain,
% 76.95/77.04 (~P1(f3(a6,f3(a2,x30301)),f3(a1,a4))),
% 76.95/77.04 inference(scs_inference,[],[3022,3019,3003,2734,18,19,2,21])).
% 76.95/77.04 cnf(3031,plain,
% 76.95/77.04 (P1(f3(x30311,x30312),f3(x30311,f3(x30312,x30313)))),
% 76.95/77.04 inference(rename_variables,[],[2734])).
% 76.95/77.04 cnf(3033,plain,
% 76.95/77.04 (~P1(a5,a2)),
% 76.95/77.04 inference(scs_inference,[],[3022,3019,3003,2734,13,18,19,2,21,20])).
% 76.95/77.04 cnf(3039,plain,
% 76.95/77.04 (P1(f3(f3(x30391,x30391),f3(a4,a2)),f3(a2,f3(a1,x30392)))),
% 76.95/77.04 inference(scs_inference,[],[3022,3019,2920,3014,2754,3003,2734,3031,13,18,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3041,plain,
% 76.95/77.04 (~E(f3(f3(x30411,a6),x30412),a5)),
% 76.95/77.04 inference(scs_inference,[],[3022,3019,2920,3014,2754,3003,865,2734,3031,13,18,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3045,plain,
% 76.95/77.04 (~E(f3(a5,a2),a2)),
% 76.95/77.04 inference(scs_inference,[],[3033,741,18,19])).
% 76.95/77.04 cnf(3057,plain,
% 76.95/77.04 (~E(f3(f3(a1,a2),f3(a1,a2)),f3(a6,a2))),
% 76.95/77.04 inference(scs_inference,[],[3033,955,1258,2827,2994,2578,2738,2632,2833,741,383,18,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3064,plain,
% 76.95/77.04 (~E(a2,f3(a5,a2))),
% 76.95/77.04 inference(scs_inference,[],[3045,2767,655,18,19,2])).
% 76.95/77.04 cnf(3068,plain,
% 76.95/77.04 (~P1(f3(a5,a2),a2)),
% 76.95/77.04 inference(scs_inference,[],[3045,2767,2868,2858,655,13,18,19,2,21,20])).
% 76.95/77.04 cnf(3077,plain,
% 76.95/77.04 (E(f3(f3(x30771,x30772),x30771),a2)),
% 76.95/77.04 inference(scs_inference,[],[15,18])).
% 76.95/77.04 cnf(3081,plain,
% 76.95/77.04 (~E(a2,f3(f3(a1,a5),f3(a4,a5)))),
% 76.95/77.04 inference(scs_inference,[],[3068,2525,15,18,19,2])).
% 76.95/77.04 cnf(3082,plain,
% 76.95/77.04 (P1(f3(f3(x30821,x30821),a4),f3(f3(a2,x30822),f3(a1,a4)))),
% 76.95/77.04 inference(scs_inference,[],[3068,2525,2679,2825,15,18,19,2,21])).
% 76.95/77.04 cnf(3089,plain,
% 76.95/77.04 (~P1(f3(a5,f3(a1,a4)),a2)),
% 76.95/77.04 inference(scs_inference,[],[3068,2525,2854,3039,2679,2889,2825,741,15,18,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3096,plain,
% 76.95/77.04 (~E(f3(f3(a1,a4),f3(a2,a4)),f3(a6,a2))),
% 76.95/77.04 inference(scs_inference,[],[3030,1703,19,2])).
% 76.95/77.04 cnf(3100,plain,
% 76.95/77.04 (~P1(f3(a6,a2),f3(f3(a1,a2),f3(a1,a2)))),
% 76.95/77.04 inference(scs_inference,[],[17,3057,3030,1703,2616,1144,19,2,21,20])).
% 76.95/77.04 cnf(3103,plain,
% 76.95/77.04 (~P1(f3(a6,a5),f3(a2,a4))),
% 76.95/77.04 inference(scs_inference,[],[17,3057,3030,1703,2795,2786,2616,1144,19,2,21,20,7])).
% 76.95/77.04 cnf(3107,plain,
% 76.95/77.04 (~E(f3(f3(a2,a2),a2),f3(a5,a2))),
% 76.95/77.04 inference(scs_inference,[],[17,3064,3057,3030,1703,2795,2786,1667,2616,2994,435,1144,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3109,plain,
% 76.95/77.04 (~E(f3(f3(a6,a5),f3(a2,a4)),a2)),
% 76.95/77.04 inference(scs_inference,[],[3103,19])).
% 76.95/77.04 cnf(3118,plain,
% 76.95/77.04 (~P1(f3(a6,a5),f3(f3(a2,x31181),a4))),
% 76.95/77.04 inference(scs_inference,[],[3103,3107,2908,3082,2852,2204,759,19,2,21,20,7])).
% 76.95/77.04 cnf(3120,plain,
% 76.95/77.04 (~P1(f3(f3(a6,a5),f3(x31201,a6)),f3(a2,a4))),
% 76.95/77.04 inference(scs_inference,[],[3103,3107,2908,3082,2852,2204,759,383,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3122,plain,
% 76.95/77.04 (~E(f3(f3(a1,a4),f3(a2,x31221)),f3(a6,a2))),
% 76.95/77.04 inference(scs_inference,[],[3103,3096,3107,2908,2640,3082,2852,2204,759,383,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3126,plain,
% 76.95/77.04 (~E(f3(a6,a2),f3(f3(a1,a4),f3(a2,x31261)))),
% 76.95/77.04 inference(scs_inference,[],[3120,3122,19,2])).
% 76.95/77.04 cnf(3130,plain,
% 76.95/77.04 (~P1(f3(a6,a2),f3(f3(a1,a4),f3(a2,a4)))),
% 76.95/77.04 inference(scs_inference,[],[17,3120,3122,1164,1709,19,2,21,20])).
% 76.95/77.04 cnf(3136,plain,
% 76.95/77.04 (~P1(f3(f3(a6,a5),a2),f3(a2,a4))),
% 76.95/77.04 inference(scs_inference,[],[17,3120,3122,2928,2764,1164,1709,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3139,plain,
% 76.95/77.04 (~E(f3(f3(a1,a2),f3(a4,a5)),a5)),
% 76.95/77.04 inference(scs_inference,[],[17,3120,3122,2928,136,2764,2835,1164,1709,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3144,plain,
% 76.95/77.04 (~E(f3(a1,f3(x31441,a6)),f3(a2,a2))),
% 76.95/77.04 inference(scs_inference,[],[3136,1813,19,2])).
% 76.95/77.04 cnf(3153,plain,
% 76.95/77.04 (~P1(f3(f3(a6,a5),f3(a2,x31531)),f3(a2,a4))),
% 76.95/77.04 inference(scs_inference,[],[3136,1813,2971,2862,2909,2578,1744,2713,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3164,plain,
% 76.95/77.04 (~P1(f3(a1,f3(x31641,a6)),f3(a2,a2))),
% 76.95/77.04 inference(scs_inference,[],[3153,3144,2541,2549,2685,2833,19,2,21,20])).
% 76.95/77.04 cnf(3169,plain,
% 76.95/77.04 (~P1(f3(f3(a6,a5),f3(x31691,x31691)),f3(a2,a4))),
% 76.95/77.04 inference(scs_inference,[],[3153,3144,3100,2541,2836,2549,2689,2685,2833,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3170,plain,
% 76.95/77.04 (E(f3(x31701,f3(x31702,x31702)),f3(x31701,f3(a2,x31703)))),
% 76.95/77.04 inference(rename_variables,[],[2689])).
% 76.95/77.04 cnf(3171,plain,
% 76.95/77.04 (~E(f3(a1,f3(a2,x31711)),f3(a2,a2))),
% 76.95/77.04 inference(scs_inference,[],[3153,3144,3100,2541,2836,2549,2689,3170,2685,2833,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3178,plain,
% 76.95/77.04 (~P1(f3(f3(a6,a5),f3(a1,a4)),f3(a2,a4))),
% 76.95/77.04 inference(scs_inference,[],[3169,3171,2663,19,2,21])).
% 76.95/77.04 cnf(3180,plain,
% 76.95/77.04 (~P1(f3(f3(a6,a5),f3(x31801,x31801)),f3(a2,a4))),
% 76.95/77.04 inference(rename_variables,[],[3169])).
% 76.95/77.04 cnf(3188,plain,
% 76.95/77.04 (~P1(f3(a1,a2),f3(a2,a2))),
% 76.95/77.04 inference(scs_inference,[],[3169,3180,3164,3171,2787,2144,2888,2711,2663,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3194,plain,
% 76.95/77.04 (~E(f3(f3(a1,a2),f3(a2,a2)),a2)),
% 76.95/77.04 inference(scs_inference,[],[3188,19])).
% 76.95/77.04 cnf(3203,plain,
% 76.95/77.04 (~P1(f3(a5,f3(a1,a4)),f3(f3(x32031,x32032),x32031))),
% 76.95/77.04 inference(scs_inference,[],[3188,1362,3139,3077,3089,2734,759,19,2,21,20,7])).
% 76.95/77.04 cnf(3210,plain,
% 76.95/77.04 (~E(f3(f3(x32101,a6),f3(x32102,a6)),f3(a6,a2))),
% 76.95/77.04 inference(scs_inference,[],[3178,1156,19,2])).
% 76.95/77.04 cnf(3211,plain,
% 76.95/77.04 (P1(f3(f3(x32111,x32111),f3(a2,a1)),f3(a4,f3(x32112,x32112)))),
% 76.95/77.04 inference(scs_inference,[],[3178,1156,3011,2858,19,2,21])).
% 76.95/77.04 cnf(3214,plain,
% 76.95/77.04 (E(f3(f3(a2,a6),a1),f3(f3(x32141,x32141),a4))),
% 76.95/77.04 inference(scs_inference,[],[3178,1156,3011,2679,2858,848,19,2,21,20])).
% 76.95/77.04 cnf(3220,plain,
% 76.95/77.04 (~P1(f3(f3(f3(a6,a5),f3(a1,a4)),f3(x32201,a6)),f3(a2,a4))),
% 76.95/77.04 inference(scs_inference,[],[3178,1156,3011,2908,2679,2858,848,383,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3226,plain,
% 76.95/77.04 (~E(f3(f3(a1,a2),f3(a4,a5)),a2)),
% 76.95/77.04 inference(scs_inference,[],[2188,19])).
% 76.95/77.04 cnf(3232,plain,
% 76.95/77.04 (~P1(f3(a6,a2),f3(f3(a6,a6),f3(a2,a6)))),
% 76.95/77.04 inference(scs_inference,[],[3210,2918,2709,2188,2825,1767,19,2,21,20])).
% 76.95/77.04 cnf(3245,plain,
% 76.95/77.04 (P1(f3(f3(x32451,x32451),f3(a2,a1)),f3(a4,f3(a2,x32452)))),
% 76.95/77.04 inference(scs_inference,[],[2636,3211,762,2711,19,2,21])).
% 76.95/77.04 cnf(3266,plain,
% 76.95/77.04 (~P1(f3(a1,a2),f3(f3(a1,a4),f3(a2,a4)))),
% 76.95/77.04 inference(scs_inference,[],[17,2669,2804,1235,1559,1594,19,2,21,20])).
% 76.95/77.04 cnf(3269,plain,
% 76.95/77.04 (~P1(f3(a5,f3(a1,a4)),f3(a2,a2))),
% 76.95/77.04 inference(scs_inference,[],[17,2669,2804,2975,3203,1235,1559,1594,19,2,21,20,7])).
% 76.95/77.04 cnf(3272,plain,
% 76.95/77.04 (P1(f3(f3(x32721,x32721),a4),f3(a6,a6))),
% 76.95/77.04 inference(scs_inference,[],[17,2669,2804,2975,3203,3214,1235,2762,1559,1594,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3284,plain,
% 76.95/77.04 (P1(f3(f3(a1,a4),x32841),f3(a2,f3(a1,a4)))),
% 76.95/77.04 inference(scs_inference,[],[3269,2831,2743,2663,19,2,21])).
% 76.95/77.04 cnf(3288,plain,
% 76.95/77.04 (E(f3(a6,a6),f3(f3(x32881,x32881),a4))),
% 76.95/77.04 inference(scs_inference,[],[3269,3272,2831,2743,2663,2833,19,2,21,20])).
% 76.95/77.04 cnf(3307,plain,
% 76.95/77.04 (~P1(f3(a6,a5),f3(a6,a6))),
% 76.95/77.04 inference(scs_inference,[],[17,2693,3288,3118,2968,2575,1538,1594,19,2,21,20,7])).
% 76.95/77.04 cnf(3313,plain,
% 76.95/77.04 (~E(f3(f3(a6,a5),f3(a6,a6)),a2)),
% 76.95/77.04 inference(scs_inference,[],[3307,19])).
% 76.95/77.04 cnf(3316,plain,
% 76.95/77.04 (P1(f3(f3(x33161,x33161),a4),f3(f3(a2,x33162),f3(a2,x33163)))),
% 76.95/77.04 inference(scs_inference,[],[3307,3027,3082,349,19,2,21])).
% 76.95/77.04 cnf(3319,plain,
% 76.95/77.04 (E(f3(a2,f3(a1,a4)),f3(f3(a1,a4),x33191))),
% 76.95/77.04 inference(scs_inference,[],[3307,3027,3284,3082,349,741,19,2,21,20])).
% 76.95/77.04 cnf(3322,plain,
% 76.95/77.04 (~P1(f3(a6,a5),f3(x33221,f3(x33221,a2)))),
% 76.95/77.04 inference(scs_inference,[],[3307,3027,3284,2228,3082,349,741,19,2,21,20,7])).
% 76.95/77.04 cnf(3324,plain,
% 76.95/77.04 (~P1(f3(f3(a6,a5),f3(x33241,a6)),f3(a6,a6))),
% 76.95/77.04 inference(scs_inference,[],[3307,3027,3284,2228,3082,349,741,383,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3331,plain,
% 76.95/77.04 (~P1(f3(a1,f3(x33311,a6)),f3(a4,a5))),
% 76.95/77.04 inference(scs_inference,[],[17,3324,3109,366,19,2,21])).
% 76.95/77.04 cnf(3332,plain,
% 76.95/77.04 (P1(f3(x33321,x33322),f3(x33321,f3(x33323,a6)))),
% 76.95/77.04 inference(rename_variables,[],[366])).
% 76.95/77.04 cnf(3338,plain,
% 76.95/77.04 (~P1(f3(a6,a5),f3(a1,a4))),
% 76.95/77.04 inference(scs_inference,[],[17,3324,2729,2742,3322,3109,366,2685,19,2,21,20,7])).
% 76.95/77.04 cnf(3340,plain,
% 76.95/77.04 (P1(f3(f3(a1,a4),x33401),f3(a2,f3(x33402,a6)))),
% 76.95/77.04 inference(scs_inference,[],[17,3324,2729,2742,3322,3109,3319,366,3332,2685,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3349,plain,
% 76.95/77.04 (P1(f3(f3(x33491,x33491),f3(a2,a1)),f3(a4,f3(a2,x33492)))),
% 76.95/77.04 inference(rename_variables,[],[3245])).
% 76.95/77.04 cnf(3355,plain,
% 76.95/77.04 (~P1(f3(a6,a5),f3(f3(a1,a2),a4))),
% 76.95/77.04 inference(scs_inference,[],[3338,3194,3245,3349,3316,1474,2741,19,2,21,20,7])).
% 76.95/77.04 cnf(3357,plain,
% 76.95/77.04 (~P1(f3(f3(a6,a5),f3(x33571,a6)),f3(a1,a4))),
% 76.95/77.04 inference(scs_inference,[],[3338,3194,3245,3349,3316,1474,2741,383,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3359,plain,
% 76.95/77.04 (~E(f3(f3(x33591,x33591),x33592),a5)),
% 76.95/77.04 inference(scs_inference,[],[3338,3194,3041,2951,3245,3349,3316,1474,2741,383,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3367,plain,
% 76.95/77.04 (~P1(f3(a1,a5),f3(f3(x33671,x33672),f3(a6,x33672)))),
% 76.95/77.04 inference(scs_inference,[],[3357,3266,2766,3226,1303,1719,19,2,21,20])).
% 76.95/77.04 cnf(3373,plain,
% 76.95/77.04 (P1(f3(f3(a1,a4),x33731),f3(a2,f3(a1,x33732)))),
% 76.95/77.04 inference(scs_inference,[],[3357,3232,3266,2766,3226,2590,2746,2587,1303,1719,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3380,plain,
% 76.95/77.04 (P1(f3(f3(a1,a4),x33801),f3(a2,a1))),
% 76.95/77.04 inference(scs_inference,[],[3331,3313,3373,2561,19,2,21])).
% 76.95/77.04 cnf(3384,plain,
% 76.95/77.04 (E(f3(a2,f3(x33841,a6)),f3(f3(a1,a4),x33842))),
% 76.95/77.04 inference(scs_inference,[],[3331,3313,3340,3373,2561,741,19,2,21,20])).
% 76.95/77.04 cnf(3395,plain,
% 76.95/77.04 (P1(f3(f3(a1,a4),f3(a2,a1)),x33951)),
% 76.95/77.04 inference(scs_inference,[],[3331,3130,3313,2614,3340,3373,2561,2863,741,383,19,2,21,20,7,6,3,18,23])).
% 76.95/77.04 cnf(3415,plain,
% 76.95/77.04 (~E(a5,f3(f3(x34151,x34151),x34152))),
% 76.95/77.04 inference(scs_inference,[],[3359,2547,19,2])).
% 76.95/77.04 cnf(3420,plain,
% 76.95/77.04 (E(f3(a2,a1),f3(f3(a1,a4),x34201))),
% 76.95/77.04 inference(scs_inference,[],[3380,3359,2547,2666,2642,741,19,2,21,20])).
% 76.95/77.04 cnf(3440,plain,
% 76.95/77.04 (~P1(f3(a1,a5),f3(a2,a1))),
% 76.95/77.04 inference(scs_inference,[],[3420,2810,3367,2873,2177,2670,2474,2762,19,2,21,20,7])).
% 76.95/77.04 cnf(3449,plain,
% 76.95/77.04 (P1(f3(f3(a1,a4),x34491),f3(a4,a2))),
% 76.95/77.04 inference(scs_inference,[],[2196,2568,2971,2886,19,2,21])).
% 76.95/77.04 cnf(3459,plain,
% 76.95/77.04 (~P1(f3(f3(a1,a2),a5),f3(a2,a1))),
% 76.95/77.04 inference(scs_inference,[],[3440,3395,3126,2196,2568,2740,2971,2886,2741,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3465,plain,
% 76.95/77.04 (P1(f3(f3(a1,a4),f3(a4,a2)),x34651)),
% 76.95/77.04 inference(scs_inference,[],[3440,3395,3126,2196,3384,2111,2568,2740,2971,2886,2741,19,2,21,20,7,6,3,18,23])).
% 76.95/77.04 cnf(3470,plain,
% 76.95/77.04 (~P1(f3(a1,f3(x34701,a6)),f3(a2,a1))),
% 76.95/77.04 inference(scs_inference,[],[3459,2198,2461,19,2,21])).
% 76.95/77.04 cnf(3473,plain,
% 76.95/77.04 (~P1(f3(a1,a5),f3(f3(a4,a6),f3(a5,a6)))),
% 76.95/77.04 inference(scs_inference,[],[3459,2837,2198,2461,848,19,2,21,20])).
% 76.95/77.04 cnf(3489,plain,
% 76.95/77.04 (E(f3(a2,f3(a1,x34891)),f3(f3(a1,a4),x34892))),
% 76.95/77.04 inference(scs_inference,[],[3449,3470,2777,2738,3373,741,19,2,21,20])).
% 76.95/77.04 cnf(3494,plain,
% 76.95/77.04 (~P1(f3(a1,a2),f3(a2,a1))),
% 76.95/77.04 inference(scs_inference,[],[3449,3470,2777,2764,2738,3373,2740,741,19,2,21,20,7,6])).
% 76.95/77.04 cnf(3497,plain,
% 76.95/77.04 (~E(f3(a1,a2),f3(x34971,x34971))),
% 76.95/77.04 inference(scs_inference,[],[3449,3470,2777,2824,1678,2764,2738,3373,2740,741,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3501,plain,
% 76.95/77.04 (~E(f3(f3(a1,a2),f3(a2,a1)),a2)),
% 76.95/77.04 inference(scs_inference,[],[3494,19])).
% 76.95/77.04 cnf(3507,plain,
% 76.95/77.04 (~P1(f3(a1,a2),f3(f3(a1,a2),f3(a1,a2)))),
% 76.95/77.04 inference(scs_inference,[],[3494,3497,2906,2616,1122,19,2,21,20])).
% 76.95/77.04 cnf(3527,plain,
% 76.95/77.04 (~P1(f3(a6,a5),f3(x35271,x35271))),
% 76.95/77.04 inference(scs_inference,[],[3355,3415,3501,298,2725,3011,3316,2645,19,2,21,20,7])).
% 76.95/77.04 cnf(3530,plain,
% 76.95/77.04 (~E(f3(f3(a1,a4),x35301),f3(a6,a2))),
% 76.95/77.04 inference(scs_inference,[],[3355,3415,3501,3489,1259,298,2725,3011,3316,2645,383,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3532,plain,
% 76.95/77.04 (~E(f3(f3(a6,a5),f3(x35321,x35321)),a2)),
% 76.95/77.04 inference(scs_inference,[],[3527,19])).
% 76.95/77.04 cnf(3534,plain,
% 76.95/77.04 (~E(f3(a6,a2),f3(f3(a1,a4),x35341))),
% 76.95/77.04 inference(scs_inference,[],[3527,3530,19,2])).
% 76.95/77.04 cnf(3538,plain,
% 76.95/77.04 (~P1(f3(a6,a2),f3(f3(a1,a4),f3(a4,a2)))),
% 76.95/77.04 inference(scs_inference,[],[17,3527,3530,3465,1132,19,2,21,20])).
% 76.95/77.04 cnf(3558,plain,
% 76.95/77.04 (~P1(f3(a1,a5),f3(f3(x35581,a6),f3(x35582,a6)))),
% 76.95/77.04 inference(scs_inference,[],[3473,3534,3532,3220,112,2911,2591,2784,19,2,21,20,7])).
% 76.95/77.04 cnf(3690,plain,
% 76.95/77.04 (~P1(f3(a4,f3(x36901,x36901)),a2)),
% 76.95/77.04 inference(scs_inference,[],[303,2811,2578,939,19,2,21])).
% 76.95/77.04 cnf(3692,plain,
% 76.95/77.04 (E(f3(a1,f3(a1,a2)),f3(f3(a1,x36921),f3(a4,x36921)))),
% 76.95/77.04 inference(scs_inference,[],[303,2811,2578,1740,939,2713,19,2,21,20])).
% 76.95/77.04 cnf(3700,plain,
% 76.95/77.04 (~E(f3(f3(x37001,x37001),f3(a4,a2)),a1)),
% 76.95/77.04 inference(scs_inference,[],[3507,3538,303,791,2811,3014,2836,2578,1740,939,2889,2713,19,2,21,20,7,6,3])).
% 76.95/77.04 cnf(3713,plain,
% 76.95/77.04 (E(f3(a1,f3(a1,a2)),f3(f3(a1,x37131),f3(a4,x37131)))),
% 76.95/77.04 inference(rename_variables,[],[3692])).
% 76.95/77.04 cnf(3715,plain,
% 76.95/77.04 ($false),
% 76.95/77.04 inference(scs_inference,[],[3558,3081,3700,3690,3692,3713,2898,2663,2713,13,19,2,21,20,7,6]),
% 76.95/77.04 ['proof']).
% 76.95/77.04 % SZS output end Proof
% 76.95/77.04 % Total time :76.380000s
%------------------------------------------------------------------------------