%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN009-4 : TPTP v8.2.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n029.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:51 EDT 2024
% Result : Unsatisfiable 45.53s 45.60s
% Output : CNFRefutation 45.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.15 % Problem : HEN009-4 : TPTP v8.2.0. Bugfixed v1.2.1.
% 0.08/0.15 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.36 % Computer : n029.cluster.edu
% 0.13/0.36 % Model : x86_64 x86_64
% 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36 % Memory : 8042.1875MB
% 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Sat Jun 22 05:29:39 EDT 2024
% 0.13/0.37 % CPUTime :
% 0.58/0.62 start to proof:theBenchmark
% 45.43/45.59 %-------------------------------------------
% 45.43/45.59 % File :CSE---1.7
% 45.43/45.59 % Problem :theBenchmark
% 45.43/45.59 % Transform :cnf
% 45.43/45.59 % Format :tptp:raw
% 45.43/45.59 % Command :java -jar mcs_scs.jar %d %s
% 45.43/45.59
% 45.43/45.59 % Result :Theorem 44.910000s
% 45.43/45.59 % Output :CNFRefutation 44.910000s
% 45.43/45.59 %-------------------------------------------
% 45.53/45.59 %--------------------------------------------------------------------------
% 45.53/45.59 % File : HEN009-4 : TPTP v8.2.0. Bugfixed v1.2.1.
% 45.53/45.59 % Domain : Henkin Models
% 45.53/45.59 % Problem : Define X' as identity/X. Then X' = X'''
% 45.53/45.59 % Version : [MOW76] axioms : Augmented.
% 45.53/45.59 % English :
% 45.53/45.59
% 45.53/45.59 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 45.53/45.59 % Source : [TPTP]
% 45.53/45.59 % Names :
% 45.53/45.59
% 45.53/45.59 % Status : Unsatisfiable
% 45.53/45.59 % Rating : 0.00 v7.4.0, 0.11 v7.2.0, 0.12 v7.1.0, 0.14 v7.0.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.31 v5.4.0, 0.33 v5.3.0, 0.42 v5.2.0, 0.12 v5.1.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.00 v2.0.0
% 45.53/45.59 % Syntax : Number of clauses : 16 ( 9 unt; 0 nHn; 7 RR)
% 45.53/45.59 % Number of literals : 25 ( 8 equ; 10 neg)
% 45.53/45.59 % Maximal clause size : 3 ( 1 avg)
% 45.53/45.59 % Maximal term depth : 4 ( 1 avg)
% 45.53/45.59 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 45.53/45.59 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 45.53/45.59 % Number of variables : 28 ( 5 sgn)
% 45.53/45.59 % SPC : CNF_UNS_RFO_SEQ_HRN
% 45.53/45.59
% 45.53/45.59 % Comments :
% 45.53/45.59 % Bugfixes : v1.2.1 - Clauses id_divide_a_is_b, id_divide_b_is_c,
% 45.53/45.59 % id_divide_c_is_d, and prove_b_equals_d, removed.
% 45.53/45.60 %--------------------------------------------------------------------------
% 45.53/45.60 %----Include Henkin model axioms for equality formulation
% 45.53/45.60 include('Axioms/HEN002-0.ax').
% 45.53/45.60 %--------------------------------------------------------------------------
% 45.53/45.60 cnf(everything_divide_id_is_zero,axiom,
% 45.53/45.60 divide(X,identity) = zero ).
% 45.53/45.60
% 45.53/45.60 cnf(zero_divide_anything_is_zero,axiom,
% 45.53/45.60 divide(zero,X) = zero ).
% 45.53/45.60
% 45.53/45.60 cnf(x_divide_x_is_zero,axiom,
% 45.53/45.60 divide(X,X) = zero ).
% 45.53/45.60
% 45.53/45.60 cnf(x_divide_zero_is_x,axiom,
% 45.53/45.60 divide(a,zero) = a ).
% 45.53/45.60
% 45.53/45.60 cnf(transitivity_of_less_equal,axiom,
% 45.53/45.60 ( ~ less_equal(X,Y)
% 45.53/45.60 | ~ less_equal(Y,Z)
% 45.53/45.60 | less_equal(X,Z) ) ).
% 45.53/45.60
% 45.53/45.60 cnf(property_of_divide1,axiom,
% 45.53/45.60 ( ~ less_equal(divide(X,Y),Z)
% 45.53/45.60 | less_equal(divide(X,Z),Y) ) ).
% 45.53/45.60
% 45.53/45.60 cnf(property_of_divide2,axiom,
% 45.53/45.60 ( ~ less_equal(X,Y)
% 45.53/45.60 | less_equal(divide(Z,Y),divide(Z,X)) ) ).
% 45.53/45.60
% 45.53/45.60 cnf(property_of_divide3,axiom,
% 45.53/45.60 ( ~ less_equal(X,Y)
% 45.53/45.60 | less_equal(divide(X,Z),divide(Y,Z)) ) ).
% 45.53/45.60
% 45.53/45.60 cnf(prove_this,negated_conjecture,
% 45.53/45.60 divide(identity,a) != divide(identity,divide(identity,divide(identity,a))) ).
% 45.53/45.60
% 45.53/45.60 %----This is an alternate way of writing the theorem
% 45.53/45.60 %input_clause(id_divide_a_is_b,hypothesis,
% 45.53/45.60 % [++equal(divide(identity,a),b)]).
% 45.53/45.60 %
% 45.53/45.60 %input_clause(id_divide_b_is_c,hypothesis,
% 45.53/45.60 % [++equal(divide(identity,b),c)]).
% 45.53/45.60 %
% 45.53/45.60 %input_clause(id_divide_c_is_d,hypothesis,
% 45.53/45.60 % [++equal(divide(identity,c),d)]).
% 45.53/45.60 %
% 45.53/45.60 %input_clause(prove_b_equals_d,negated_conjecture,
% 45.53/45.60 % [--equal(b,d)]).
% 45.53/45.60 %--------------------------------------------------------------------------
% 45.53/45.60 %-------------------------------------------
% 45.53/45.60 % Proof found
% 45.53/45.60 % SZS status Theorem for theBenchmark
% 45.53/45.60 % SZS output start Proof
% 45.53/45.60 %ClaNum:23(EqnAxiom:7)
% 45.53/45.60 %VarNum:54(SingletonVarNum:28)
% 45.53/45.60 %MaxLitNum:3
% 45.53/45.60 %MaxfuncDepth:3
% 45.53/45.60 %SharedTerms:9
% 45.53/45.60 %goalClause: 16
% 45.53/45.60 %singleGoalClaCount:1
% 45.53/45.60 [8]E(f3(a1,a2),a1)
% 45.53/45.60 [16]~E(f3(a4,f3(a4,f3(a4,a1))),f3(a4,a1))
% 45.53/45.60 [11]P1(x111,a4)
% 45.53/45.60 [12]P1(a2,x121)
% 45.53/45.60 [9]E(f3(x91,a4),a2)
% 45.53/45.60 [10]E(f3(a2,x101),a2)
% 45.53/45.60 [13]E(f3(x131,x131),a2)
% 45.53/45.60 [14]P1(f3(x141,x142),x141)
% 45.53/45.60 [15]P1(f3(f3(x151,x152),f3(x153,x152)),f3(f3(x151,x153),x152))
% 45.53/45.60 [17]~P1(x171,x172)+E(f3(x171,x172),a2)
% 45.53/45.60 [18]P1(x181,x182)+~E(f3(x181,x182),a2)
% 45.53/45.60 [21]~P1(x213,x212)+P1(f3(x211,x212),f3(x211,x213))
% 45.53/45.60 [22]~P1(x221,x223)+P1(f3(x221,x222),f3(x223,x222))
% 45.53/45.60 [23]~P1(f3(x231,x233),x232)+P1(f3(x231,x232),x233)
% 45.53/45.60 [19]~P1(x192,x191)+~P1(x191,x192)+E(x191,x192)
% 45.53/45.60 [20]~P1(x201,x203)+P1(x201,x202)+~P1(x203,x202)
% 45.53/45.60 %EqnAxiom
% 45.53/45.60 [1]E(x11,x11)
% 45.53/45.60 [2]E(x22,x21)+~E(x21,x22)
% 45.53/45.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 45.53/45.60 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 45.53/45.60 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 45.53/45.60 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 45.53/45.60 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 45.53/45.60
% 45.53/45.60 %-------------------------------------------
% 45.53/45.61 cnf(24,plain,
% 45.53/45.61 (E(a2,f3(x241,x241))),
% 45.53/45.61 inference(scs_inference,[],[13,2])).
% 45.53/45.61 cnf(25,plain,
% 45.53/45.61 (P1(x251,x251)),
% 45.53/45.61 inference(scs_inference,[],[13,2,18])).
% 45.53/45.61 cnf(29,plain,
% 45.53/45.61 (P1(f3(x291,x291),x292)),
% 45.53/45.61 inference(scs_inference,[],[16,12,13,8,2,18,5,3,6])).
% 45.53/45.61 cnf(30,plain,
% 45.53/45.61 (P1(f3(f3(x301,x301),x302),a2)),
% 45.53/45.61 inference(scs_inference,[],[16,12,14,13,8,2,18,5,3,6,7])).
% 45.53/45.61 cnf(31,plain,
% 45.53/45.61 (P1(f3(x311,x312),x311)),
% 45.53/45.61 inference(rename_variables,[],[14])).
% 45.53/45.61 cnf(32,plain,
% 45.53/45.61 (E(f3(x321,x321),f3(f3(x321,x321),x322))),
% 45.53/45.61 inference(scs_inference,[],[16,12,14,31,13,8,2,18,5,3,6,7,19])).
% 45.53/45.61 cnf(33,plain,
% 45.53/45.61 (P1(f3(x331,x332),x331)),
% 45.53/45.61 inference(rename_variables,[],[14])).
% 45.53/45.61 cnf(35,plain,
% 45.53/45.61 (P1(f3(a2,x351),f3(f3(x352,x352),x353))),
% 45.53/45.61 inference(scs_inference,[],[16,12,14,31,33,13,8,2,18,5,3,6,7,19,20])).
% 45.53/45.61 cnf(39,plain,
% 45.53/45.61 (E(f3(f3(x391,x391),x392),f3(x391,x391))),
% 45.53/45.61 inference(scs_inference,[],[32,2])).
% 45.53/45.61 cnf(40,plain,
% 45.53/45.61 (E(f3(a2,x401),f3(f3(x402,x402),f3(x402,x402)))),
% 45.53/45.61 inference(scs_inference,[],[32,29,35,2,19])).
% 45.53/45.61 cnf(42,plain,
% 45.53/45.61 (P1(f3(x421,x421),x422)),
% 45.53/45.61 inference(rename_variables,[],[29])).
% 45.53/45.61 cnf(45,plain,
% 45.53/45.61 (E(a2,f3(f3(x451,x451),x452))),
% 45.53/45.61 inference(scs_inference,[],[32,24,29,35,30,2,19,7,3])).
% 45.53/45.61 cnf(46,plain,
% 45.53/45.61 (E(f3(x461,x461),f3(f3(x461,x461),x462))),
% 45.53/45.61 inference(rename_variables,[],[32])).
% 45.53/45.61 cnf(47,plain,
% 45.53/45.61 (P1(f3(f3(x471,x471),x472),x473)),
% 45.53/45.61 inference(scs_inference,[],[32,46,24,29,42,35,30,2,19,7,3,6])).
% 45.53/45.61 cnf(50,plain,
% 45.53/45.61 (E(f3(f3(x501,x502),f3(x501,x502)),f3(f3(x501,x501),x502))),
% 45.53/45.61 inference(scs_inference,[],[40,47,15,2,19])).
% 45.53/45.61 cnf(54,plain,
% 45.53/45.61 (P1(f3(a2,x541),f3(x542,x542))),
% 45.53/45.61 inference(scs_inference,[],[39,40,47,15,35,2,19,7])).
% 45.53/45.61 cnf(56,plain,
% 45.53/45.61 (E(f3(a2,x561),f3(x562,x562))),
% 45.53/45.61 inference(scs_inference,[],[39,40,47,15,35,2,19,7,3])).
% 45.53/45.61 cnf(58,plain,
% 45.53/45.61 (E(f3(f3(x581,x581),x582),f3(f3(x581,x582),f3(x581,x582)))),
% 45.53/45.61 inference(scs_inference,[],[50,2])).
% 45.53/45.61 cnf(59,plain,
% 45.53/45.61 (E(f3(f3(a2,x591),f3(a2,x591)),f3(a2,x591))),
% 45.53/45.61 inference(scs_inference,[],[50,54,14,2,19])).
% 45.53/45.61 cnf(63,plain,
% 45.53/45.61 (E(f3(a2,x631),f3(f3(x632,x632),x633))),
% 45.53/45.61 inference(scs_inference,[],[50,56,54,14,2,19,3])).
% 45.53/45.61 cnf(67,plain,
% 45.53/45.61 (E(f3(f3(x671,x671),x672),f3(a2,x673))),
% 45.53/45.61 inference(scs_inference,[],[63,2])).
% 45.53/45.61 cnf(68,plain,
% 45.53/45.61 (P1(f3(f3(f3(x681,x681),x682),x683),f3(f3(x681,x682),f3(x681,x682)))),
% 45.53/45.61 inference(scs_inference,[],[58,63,14,2,7])).
% 45.53/45.61 cnf(70,plain,
% 45.53/45.61 (E(f3(f3(a2,x701),f3(a2,x701)),f3(f3(x702,x702),x703))),
% 45.53/45.61 inference(scs_inference,[],[58,59,63,14,2,7,3])).
% 45.53/45.61 cnf(72,plain,
% 45.53/45.61 (E(f3(f3(f3(x721,x721),x722),x723),f3(f3(x721,x722),f3(x721,x722)))),
% 45.53/45.61 inference(scs_inference,[],[58,59,63,29,14,2,7,3,19])).
% 45.53/45.61 cnf(75,plain,
% 45.53/45.61 (E(f3(f3(x751,x752),f3(x751,x752)),f3(f3(f3(x751,x751),x752),x753))),
% 45.53/45.61 inference(scs_inference,[],[72,2])).
% 45.53/45.61 cnf(76,plain,
% 45.53/45.61 (E(f3(f3(f3(x761,x761),x762),x763),f3(f3(x761,x761),x762))),
% 45.53/45.61 inference(scs_inference,[],[72,47,14,2,19])).
% 45.53/45.61 cnf(80,plain,
% 45.53/45.61 (P1(f3(f3(f3(x801,x801),x802),f3(x803,x802)),f3(f3(x801,x803),f3(x801,x803)))),
% 45.53/45.61 inference(scs_inference,[],[72,47,15,14,2,19,7])).
% 45.53/45.61 cnf(82,plain,
% 45.53/45.61 (E(f3(f3(f3(x821,x821),x821),x822),f3(a2,x823))),
% 45.53/45.61 inference(scs_inference,[],[72,67,47,15,14,2,19,7,3])).
% 45.53/45.61 cnf(85,plain,
% 45.53/45.61 (E(f3(f3(x851,x851),x852),f3(f3(f3(x851,x851),x852),x853))),
% 45.53/45.61 inference(scs_inference,[],[76,2])).
% 45.53/45.61 cnf(86,plain,
% 45.53/45.61 (E(f3(f3(f3(x861,x861),x862),f3(x863,x862)),f3(f3(x861,x863),f3(x861,x863)))),
% 45.53/45.61 inference(scs_inference,[],[76,29,80,2,19])).
% 45.53/45.61 cnf(89,plain,
% 45.53/45.61 (P1(f3(f3(f3(x891,x891),x892),f3(x893,x892)),f3(f3(x891,x891),x893))),
% 45.53/45.61 inference(scs_inference,[],[76,29,15,80,2,19,7])).
% 45.53/45.61 cnf(91,plain,
% 45.53/45.61 (E(f3(x911,a4),f3(f3(x912,x912),x913))),
% 45.53/45.61 inference(scs_inference,[],[76,45,9,29,15,80,2,19,7,3])).
% 45.53/45.61 cnf(92,plain,
% 45.53/45.61 (E(f3(f3(x921,x922),f3(x921,x922)),f3(f3(f3(x921,x921),x923),f3(x922,x923)))),
% 45.53/45.61 inference(scs_inference,[],[86,2])).
% 45.53/45.61 cnf(93,plain,
% 45.53/45.61 (E(f3(f3(f3(x931,x931),x932),f3(x933,x932)),f3(f3(x931,x931),x933))),
% 45.53/45.61 inference(scs_inference,[],[86,47,89,2,19])).
% 45.53/45.61 cnf(97,plain,
% 45.53/45.61 (E(f3(f3(x971,x972),f3(x971,x972)),f3(f3(x971,x973),f3(x971,x973)))),
% 45.53/45.61 inference(scs_inference,[],[86,75,47,89,2,19,3])).
% 45.53/45.61 cnf(100,plain,
% 45.53/45.61 (E(f3(f3(x1001,x1001),x1002),f3(f3(f3(x1001,x1001),x1003),f3(x1002,x1003)))),
% 45.53/45.61 inference(scs_inference,[],[93,2])).
% 45.53/45.61 cnf(105,plain,
% 45.53/45.61 (E(f3(f3(x1051,x1052),f3(x1051,x1052)),f3(f3(f3(x1051,x1051),x1053),f3(x1052,x1053)))),
% 45.53/45.61 inference(rename_variables,[],[92])).
% 45.53/45.61 cnf(106,plain,
% 45.53/45.61 (E(f3(f3(x1061,x1062),f3(x1061,x1062)),f3(a2,x1063))),
% 45.53/45.61 inference(scs_inference,[],[92,105,93,82,35,29,2,6,7,3])).
% 45.53/45.61 cnf(110,plain,
% 45.53/45.61 (P1(f3(f3(f3(x1101,x1101),x1102),x1103),f3(f3(x1101,x1104),f3(x1101,x1104)))),
% 45.53/45.61 inference(scs_inference,[],[97,70,68,2,7])).
% 45.53/45.61 cnf(115,plain,
% 45.53/45.61 (E(f3(f3(f3(x1151,x1151),x1152),x1153),f3(f3(x1151,x1151),f3(x1151,x1151)))),
% 45.53/45.61 inference(scs_inference,[],[97,85,70,47,68,2,7,3,19])).
% 45.53/45.61 cnf(119,plain,
% 45.53/45.61 (E(f3(f3(f3(x1191,x1191),x1192),x1193),f3(f3(x1191,x1194),f3(x1191,x1194)))),
% 45.53/45.61 inference(scs_inference,[],[115,29,110,2,19])).
% 45.53/45.61 cnf(124,plain,
% 45.53/45.61 (E(f3(f3(x1241,x1241),x1242),f3(f3(x1241,x1241),f3(x1241,x1241)))),
% 45.53/45.61 inference(scs_inference,[],[100,115,35,29,110,2,19,7,3])).
% 45.53/45.61 cnf(126,plain,
% 45.53/45.61 (E(f3(f3(x1261,x1261),f3(x1261,x1261)),f3(f3(x1261,x1261),x1262))),
% 45.53/45.61 inference(scs_inference,[],[124,2])).
% 45.53/45.61 cnf(129,plain,
% 45.53/45.61 (E(f3(f3(x1291,x1292),f3(x1291,x1292)),f3(f3(f3(x1291,x1291),x1293),x1294))),
% 45.53/45.61 inference(scs_inference,[],[119,2])).
% 45.53/45.61 cnf(130,plain,
% 45.53/45.61 (P1(f3(f3(f3(x1301,x1301),x1302),x1303),f3(f3(x1301,x1301),x1304))),
% 45.53/45.61 inference(scs_inference,[],[126,119,110,2,7])).
% 45.53/45.61 cnf(132,plain,
% 45.53/45.61 (E(f3(f3(x1321,x1322),f3(x1321,x1322)),f3(f3(x1323,x1323),x1324))),
% 45.53/45.61 inference(scs_inference,[],[126,119,106,63,110,2,7,3])).
% 45.53/45.61 cnf(134,plain,
% 45.53/45.61 (E(f3(f3(f3(x1341,x1341),x1342),x1343),f3(f3(x1341,x1341),x1344))),
% 45.53/45.61 inference(scs_inference,[],[126,119,106,63,47,110,2,7,3,19])).
% 45.53/45.61 cnf(137,plain,
% 45.53/45.61 (E(f3(f3(x1371,x1371),x1372),f3(f3(x1373,x1374),f3(x1373,x1374)))),
% 45.53/45.61 inference(scs_inference,[],[132,2])).
% 45.53/45.61 cnf(140,plain,
% 45.53/45.61 (E(f3(f3(x1401,x1402),f3(x1401,x1402)),f3(f3(x1403,x1403),x1404))),
% 45.53/45.61 inference(rename_variables,[],[132])).
% 45.53/45.61 cnf(141,plain,
% 45.53/45.61 (E(f3(f3(x1411,x1412),f3(x1411,x1412)),f3(f3(f3(x1413,x1413),x1414),x1415))),
% 45.53/45.61 inference(scs_inference,[],[132,140,129,130,2,7,3])).
% 45.53/45.61 cnf(144,plain,
% 45.53/45.61 (E(f3(f3(x1441,x1441),x1442),f3(f3(f3(x1441,x1441),x1443),x1444))),
% 45.53/45.61 inference(scs_inference,[],[134,2])).
% 45.53/45.61 cnf(145,plain,
% 45.53/45.61 (E(f3(f3(x1451,x1451),x1452),f3(f3(x1453,x1453),x1454))),
% 45.53/45.61 inference(scs_inference,[],[134,137,2,3])).
% 45.53/45.61 cnf(148,plain,
% 45.53/45.61 (E(f3(f3(f3(x1481,x1481),x1482),x1483),f3(f3(x1484,x1485),f3(x1484,x1485)))),
% 45.53/45.61 inference(scs_inference,[],[141,2])).
% 45.53/45.61 cnf(149,plain,
% 45.53/45.61 (E(f3(f3(x1491,x1491),x1492),f3(f3(f3(x1493,x1493),x1494),x1495))),
% 45.53/45.61 inference(scs_inference,[],[145,144,141,2,3])).
% 45.53/45.61 cnf(151,plain,
% 45.53/45.61 (E(f3(f3(x1511,a4),f3(x1511,x1512)),a2)),
% 45.53/45.61 inference(scs_inference,[],[11,17,21])).
% 45.53/45.61 cnf(152,plain,
% 45.53/45.61 (P1(f3(x1521,a4),f3(x1521,x1522))),
% 45.53/45.61 inference(scs_inference,[],[151,18])).
% 45.53/45.61 cnf(154,plain,
% 45.53/45.61 (E(f3(f3(f3(x1541,x1541),x1542),x1543),f3(f3(x1544,x1544),x1545))),
% 45.53/45.61 inference(scs_inference,[],[149,151,18,2])).
% 45.53/45.61 cnf(157,plain,
% 45.53/45.61 (E(f3(f3(f3(x1571,x1571),x1572),x1573),f3(a2,x1574))),
% 45.53/45.61 inference(scs_inference,[],[148,149,82,25,151,18,2,7,3])).
% 45.53/45.61 cnf(160,plain,
% 45.53/45.61 (E(f3(a2,x1601),f3(f3(f3(x1602,x1602),x1603),x1604))),
% 45.53/45.61 inference(scs_inference,[],[157,2])).
% 45.53/45.61 cnf(161,plain,
% 45.53/45.61 (E(f3(f3(f3(x1611,x1611),x1612),x1613),f3(x1614,x1614))),
% 45.53/45.61 inference(scs_inference,[],[154,157,39,2,3])).
% 45.53/45.61 cnf(163,plain,
% 45.53/45.61 (E(f3(x1631,x1631),f3(f3(f3(x1632,x1632),x1633),x1634))),
% 45.53/45.61 inference(scs_inference,[],[161,2])).
% 45.53/45.61 cnf(166,plain,
% 45.53/45.61 (E(f3(f3(f3(x1661,x1661),x1662),x1663),a2)),
% 45.53/45.61 inference(scs_inference,[],[161,10,25,2,7,3])).
% 45.53/45.61 cnf(169,plain,
% 45.53/45.61 (E(f3(f3(x1691,x1691),x1692),f3(x1693,a4))),
% 45.53/45.61 inference(scs_inference,[],[91,2])).
% 45.53/45.61 cnf(174,plain,
% 45.53/45.61 (E(f3(x1741,x1741),f3(f3(f3(x1742,x1742),x1743),x1744))),
% 45.53/45.61 inference(rename_variables,[],[163])).
% 45.53/45.61 cnf(175,plain,
% 45.53/45.61 (E(f3(x1751,x1751),f3(a2,x1752))),
% 45.53/45.61 inference(scs_inference,[],[163,174,91,106,35,29,2,6,7,3])).
% 45.53/45.62 cnf(178,plain,
% 45.53/45.62 (E(a2,f3(f3(f3(x1781,x1781),x1782),x1783))),
% 45.53/45.62 inference(scs_inference,[],[166,2])).
% 45.53/45.62 cnf(179,plain,
% 45.53/45.62 (P1(f3(a2,x1791),x1792)),
% 45.53/45.62 inference(scs_inference,[],[175,166,47,2,6])).
% 45.53/45.62 cnf(181,plain,
% 45.53/45.62 (E(f3(x1811,x1811),f3(a2,x1812))),
% 45.53/45.62 inference(rename_variables,[],[175])).
% 45.53/45.62 cnf(185,plain,
% 45.53/45.62 (E(f3(f3(x1851,x1851),x1852),a2)),
% 45.53/45.62 inference(scs_inference,[],[175,181,169,166,15,47,2,6,7,3])).
% 45.53/45.62 cnf(188,plain,
% 45.53/45.62 (E(f3(f3(x1881,f3(x1881,x1882)),f3(x1882,f3(x1881,x1882))),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[175,181,169,166,15,47,29,2,6,7,3,19])).
% 45.53/45.62 cnf(191,plain,
% 45.53/45.62 (E(f3(a2,a2),f3(f3(x1911,f3(x1911,x1912)),f3(x1912,f3(x1911,x1912))))),
% 45.53/45.62 inference(scs_inference,[],[188,2])).
% 45.53/45.62 cnf(194,plain,
% 45.53/45.62 (E(f3(a2,x1941),f3(a2,x1942))),
% 45.53/45.62 inference(scs_inference,[],[188,160,67,152,2,7,3])).
% 45.53/45.62 cnf(197,plain,
% 45.53/45.62 (E(f3(f3(x1971,f3(x1971,x1972)),a4),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[188,160,67,29,152,2,7,3,19])).
% 45.53/45.62 cnf(200,plain,
% 45.53/45.62 (E(f3(a2,a2),f3(f3(x2001,f3(x2001,x2002)),a4))),
% 45.53/45.62 inference(scs_inference,[],[197,2])).
% 45.53/45.62 cnf(202,plain,
% 45.53/45.62 (P1(f3(x2021,x2021),x2022)),
% 45.53/45.62 inference(rename_variables,[],[29])).
% 45.53/45.62 cnf(205,plain,
% 45.53/45.62 (E(a2,f3(a2,x2051))),
% 45.53/45.62 inference(scs_inference,[],[191,197,178,67,15,29,2,6,7,3])).
% 45.53/45.62 cnf(208,plain,
% 45.53/45.62 (E(f3(f3(x2081,a4),f3(f3(x2081,x2082),a4)),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[191,197,178,67,15,29,202,2,6,7,3,19])).
% 45.53/45.62 cnf(211,plain,
% 45.53/45.62 (E(f3(a2,a2),f3(f3(x2111,a4),f3(f3(x2111,x2112),a4)))),
% 45.53/45.62 inference(scs_inference,[],[208,2])).
% 45.53/45.62 cnf(213,plain,
% 45.53/45.62 (P1(f3(x2131,x2131),x2132)),
% 45.53/45.62 inference(rename_variables,[],[29])).
% 45.53/45.62 cnf(214,plain,
% 45.53/45.62 (P1(f3(f3(x2141,a4),a4),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[208,200,29,152,2,6,7])).
% 45.53/45.62 cnf(216,plain,
% 45.53/45.62 (E(f3(f3(x2161,a4),f3(f3(x2161,x2162),a4)),f3(f3(a2,a2),x2163))),
% 45.53/45.62 inference(scs_inference,[],[208,200,32,29,152,2,6,7,3])).
% 45.53/45.62 cnf(218,plain,
% 45.53/45.62 (E(f3(f3(x2181,a4),a4),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[208,200,32,29,213,152,2,6,7,3,19])).
% 45.53/45.62 cnf(221,plain,
% 45.53/45.62 (E(f3(f3(a2,a2),x2211),f3(f3(x2212,a4),f3(f3(x2212,x2213),a4)))),
% 45.53/45.62 inference(scs_inference,[],[216,2])).
% 45.53/45.62 cnf(224,plain,
% 45.53/45.62 (P1(f3(f3(x2241,a4),a4),f3(f3(x2242,a4),f3(f3(x2242,x2243),a4)))),
% 45.53/45.62 inference(scs_inference,[],[216,211,29,214,2,6,7])).
% 45.53/45.62 cnf(225,plain,
% 45.53/45.62 (E(f3(f3(x2251,a4),a4),f3(f3(x2252,a4),f3(f3(x2252,x2253),a4)))),
% 45.53/45.62 inference(scs_inference,[],[216,211,218,29,214,2,6,7,3])).
% 45.53/45.62 cnf(226,plain,
% 45.53/45.62 (E(f3(f3(x2261,a4),f3(f3(x2261,x2262),a4)),f3(f3(x2263,a4),a4))),
% 45.53/45.62 inference(scs_inference,[],[225,2])).
% 45.53/45.62 cnf(227,plain,
% 45.53/45.62 (P1(f3(f3(x2271,a4),a4),a2)),
% 45.53/45.62 inference(scs_inference,[],[225,185,224,2,7])).
% 45.53/45.62 cnf(230,plain,
% 45.53/45.62 (E(f3(f3(x2301,x2301),x2302),f3(f3(x2303,a4),f3(f3(x2303,x2304),a4)))),
% 45.53/45.62 inference(scs_inference,[],[221,225,185,137,224,2,7,3])).
% 45.53/45.62 cnf(233,plain,
% 45.53/45.62 (E(f3(f3(x2331,a4),f3(f3(x2331,x2332),a4)),f3(f3(x2333,x2333),x2334))),
% 45.53/45.62 inference(scs_inference,[],[230,2])).
% 45.53/45.62 cnf(234,plain,
% 45.53/45.62 (P1(f3(f3(x2341,a4),a4),f3(a2,x2342))),
% 45.53/45.62 inference(scs_inference,[],[230,205,227,2,7])).
% 45.53/45.62 cnf(235,plain,
% 45.53/45.62 (E(f3(a2,x2351),f3(f3(x2352,f3(x2352,x2353)),f3(x2353,f3(x2352,x2353))))),
% 45.53/45.62 inference(scs_inference,[],[230,194,205,191,227,2,7,3])).
% 45.53/45.62 cnf(237,plain,
% 45.53/45.62 (E(f3(f3(x2371,f3(x2371,x2372)),f3(x2372,f3(x2371,x2372))),f3(a2,x2373))),
% 45.53/45.62 inference(scs_inference,[],[235,2])).
% 45.53/45.62 cnf(240,plain,
% 45.53/45.62 (E(f3(f3(x2401,a4),f3(f3(x2401,x2402),a4)),f3(a2,x2403))),
% 45.53/45.62 inference(scs_inference,[],[233,235,157,224,2,7,3])).
% 45.53/45.62 cnf(243,plain,
% 45.53/45.62 (E(f3(a2,x2431),f3(f3(x2432,a4),f3(f3(x2432,x2433),a4)))),
% 45.53/45.62 inference(scs_inference,[],[240,2])).
% 45.53/45.62 cnf(246,plain,
% 45.53/45.62 (E(f3(f3(x2461,a4),f3(f3(x2461,x2462),a4)),a2)),
% 45.53/45.62 inference(scs_inference,[],[240,226,56,185,234,2,7,3])).
% 45.53/45.62 cnf(249,plain,
% 45.53/45.62 (P1(f3(x2491,a4),f3(f3(x2491,x2492),a4))),
% 45.53/45.62 inference(scs_inference,[],[240,226,56,185,234,2,7,3,18])).
% 45.53/45.62 cnf(255,plain,
% 45.53/45.62 (E(f3(a2,x2551),f3(f3(x2552,a4),a4))),
% 45.53/45.62 inference(scs_inference,[],[243,246,145,226,249,2,7,3])).
% 45.53/45.62 cnf(257,plain,
% 45.53/45.62 (E(f3(f3(x2571,a4),a4),f3(a2,x2572))),
% 45.53/45.62 inference(scs_inference,[],[255,2])).
% 45.53/45.62 cnf(263,plain,
% 45.53/45.62 (E(a2,f3(x2631,a4))),
% 45.53/45.62 inference(scs_inference,[],[9,2])).
% 45.53/45.62 cnf(266,plain,
% 45.53/45.62 (E(f3(f3(x2661,a4),a4),f3(f3(f3(x2662,x2662),x2663),x2664))),
% 45.53/45.62 inference(scs_inference,[],[257,160,9,15,2,7,3])).
% 45.53/45.62 cnf(268,plain,
% 45.53/45.62 (E(f3(f3(x2681,a4),f3(a4,a4)),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[257,160,9,15,29,2,7,3,19])).
% 45.53/45.62 cnf(271,plain,
% 45.53/45.62 (E(f3(a2,a2),f3(f3(x2711,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[268,2])).
% 45.53/45.62 cnf(272,plain,
% 45.53/45.62 (P1(f3(x2721,a4),x2722)),
% 45.53/45.62 inference(scs_inference,[],[268,263,12,2,6])).
% 45.53/45.62 cnf(275,plain,
% 45.53/45.62 (E(f3(f3(x2751,a4),f3(f3(x2751,x2752),a4)),f3(x2753,a4))),
% 45.53/45.62 inference(scs_inference,[],[268,263,246,12,15,2,6,7,3])).
% 45.53/45.62 cnf(276,plain,
% 45.53/45.62 (E(f3(f3(x2761,f3(a4,a4)),f3(a4,f3(a4,a4))),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[268,263,246,12,15,29,2,6,7,3,19])).
% 45.53/45.62 cnf(279,plain,
% 45.53/45.62 (E(f3(a2,a2),f3(f3(x2791,f3(a4,a4)),f3(a4,f3(a4,a4))))),
% 45.53/45.62 inference(scs_inference,[],[276,2])).
% 45.53/45.62 cnf(282,plain,
% 45.53/45.62 (E(f3(f3(x2821,a4),a4),f3(x2822,a4))),
% 45.53/45.62 inference(scs_inference,[],[276,271,266,275,179,2,6,3])).
% 45.53/45.62 cnf(288,plain,
% 45.53/45.62 (E(f3(f3(f3(x2881,x2881),x2882),x2883),f3(x2884,a4))),
% 45.53/45.62 inference(scs_inference,[],[279,282,154,275,29,2,6,3])).
% 45.53/45.62 cnf(291,plain,
% 45.53/45.62 (E(f3(x2911,a4),f3(f3(f3(x2912,x2912),x2913),x2914))),
% 45.53/45.62 inference(scs_inference,[],[288,2])).
% 45.53/45.62 cnf(292,plain,
% 45.53/45.62 (E(f3(f3(x2921,x2921),x2922),f3(x2923,x2923))),
% 45.53/45.62 inference(scs_inference,[],[288,24,185,2,3])).
% 45.53/45.62 cnf(293,plain,
% 45.53/45.62 (E(f3(x2931,x2931),f3(f3(x2932,x2932),x2933))),
% 45.53/45.62 inference(scs_inference,[],[292,2])).
% 45.53/45.62 cnf(294,plain,
% 45.53/45.62 (E(f3(f3(x2941,x2941),x2942),f3(f3(x2943,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[292,271,2,3])).
% 45.53/45.62 cnf(296,plain,
% 45.53/45.62 (E(f3(f3(x2961,a4),f3(a4,a4)),f3(f3(x2962,x2962),x2963))),
% 45.53/45.62 inference(scs_inference,[],[294,2])).
% 45.53/45.62 cnf(297,plain,
% 45.53/45.62 (E(f3(x2971,a4),f3(a2,x2972))),
% 45.53/45.62 inference(scs_inference,[],[294,291,237,2,3])).
% 45.53/45.62 cnf(300,plain,
% 45.53/45.62 (E(f3(a2,x3001),f3(x3002,a4))),
% 45.53/45.62 inference(scs_inference,[],[297,2])).
% 45.53/45.62 cnf(301,plain,
% 45.53/45.62 (E(f3(x3011,a4),f3(f3(x3012,f3(a4,a4)),f3(a4,f3(a4,a4))))),
% 45.53/45.62 inference(scs_inference,[],[297,279,2,3])).
% 45.53/45.62 cnf(303,plain,
% 45.53/45.62 (E(f3(f3(x3031,f3(a4,a4)),f3(a4,f3(a4,a4))),f3(x3032,a4))),
% 45.53/45.62 inference(scs_inference,[],[301,2])).
% 45.53/45.62 cnf(304,plain,
% 45.53/45.62 (E(f3(x3041,x3041),f3(f3(x3042,f3(a4,a4)),f3(a4,f3(a4,a4))))),
% 45.53/45.62 inference(scs_inference,[],[293,301,2,3])).
% 45.53/45.62 cnf(307,plain,
% 45.53/45.62 (E(f3(f3(x3071,f3(a4,a4)),f3(a4,f3(a4,a4))),f3(x3072,x3072))),
% 45.53/45.62 inference(scs_inference,[],[304,2])).
% 45.53/45.62 cnf(308,plain,
% 45.53/45.62 (E(f3(x3081,x3081),f3(x3082,a4))),
% 45.53/45.62 inference(scs_inference,[],[304,303,2,3])).
% 45.53/45.62 cnf(310,plain,
% 45.53/45.62 (E(f3(x3101,a4),f3(x3102,x3102))),
% 45.53/45.62 inference(scs_inference,[],[308,2])).
% 45.53/45.62 cnf(311,plain,
% 45.53/45.62 (E(f3(f3(x3111,a4),f3(a4,a4)),f3(a2,x3112))),
% 45.53/45.62 inference(scs_inference,[],[296,308,240,2,3])).
% 45.53/45.62 cnf(314,plain,
% 45.53/45.62 (E(f3(a2,x3141),f3(f3(x3142,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[311,2])).
% 45.53/45.62 cnf(315,plain,
% 45.53/45.62 (E(f3(f3(x3151,f3(a4,a4)),f3(a4,f3(a4,a4))),f3(a2,x3152))),
% 45.53/45.62 inference(scs_inference,[],[307,311,2,3])).
% 45.53/45.62 cnf(321,plain,
% 45.53/45.62 (E(f3(x3211,a4),f3(x3212,x3212))),
% 45.53/45.62 inference(rename_variables,[],[310])).
% 45.53/45.62 cnf(322,plain,
% 45.53/45.62 (E(f3(x3221,a4),f3(f3(x3222,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[310,321,315,314,15,2,7,3])).
% 45.53/45.62 cnf(325,plain,
% 45.53/45.62 (E(f3(f3(x3251,a4),f3(a4,a4)),f3(x3252,a4))),
% 45.53/45.62 inference(scs_inference,[],[322,2])).
% 45.53/45.62 cnf(326,plain,
% 45.53/45.62 (P1(f3(f3(x3261,a4),f3(x3262,a4)),f3(f3(x3263,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[322,15,2,7])).
% 45.53/45.62 cnf(328,plain,
% 45.53/45.62 (E(f3(x3281,a4),f3(f3(x3282,a4),f3(a4,a4)))),
% 45.53/45.62 inference(rename_variables,[],[322])).
% 45.53/45.62 cnf(329,plain,
% 45.53/45.62 (E(f3(x3291,a4),f3(f3(x3292,x3293),a4))),
% 45.53/45.62 inference(scs_inference,[],[322,328,15,2,7,3])).
% 45.53/45.62 cnf(330,plain,
% 45.53/45.62 (E(f3(f3(x3301,x3302),a4),f3(x3303,a4))),
% 45.53/45.62 inference(scs_inference,[],[329,2])).
% 45.53/45.62 cnf(331,plain,
% 45.53/45.62 (P1(f3(f3(x3311,a4),f3(x3312,a4)),f3(x3313,a4))),
% 45.53/45.62 inference(scs_inference,[],[325,329,326,2,7])).
% 45.53/45.62 cnf(333,plain,
% 45.53/45.62 (E(f3(f3(x3331,a4),f3(a4,a4)),f3(f3(x3332,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[325,329,314,326,2,7,3])).
% 45.53/45.62 cnf(336,plain,
% 45.53/45.62 (E(f3(f3(x3361,a4),f3(x3362,a4)),f3(a2,a4))),
% 45.53/45.62 inference(scs_inference,[],[325,329,314,326,272,2,7,3,19])).
% 45.53/45.62 cnf(339,plain,
% 45.53/45.62 (P1(f3(f3(x3391,a4),x3392),f3(x3393,x3392))),
% 45.53/45.62 inference(scs_inference,[],[11,22,23])).
% 45.53/45.62 cnf(340,plain,
% 45.53/45.62 (E(f3(a2,a4),f3(f3(x3401,a4),f3(x3402,a4)))),
% 45.53/45.62 inference(scs_inference,[],[336,2])).
% 45.53/45.62 cnf(341,plain,
% 45.53/45.62 (E(f3(f3(x3411,a4),f3(x3412,a4)),f3(f3(x3413,x3413),a4))),
% 45.53/45.62 inference(scs_inference,[],[336,47,331,2,19])).
% 45.53/45.62 cnf(345,plain,
% 45.53/45.62 (P1(f3(f3(f3(x3451,a4),f3(a4,a4)),x3452),f3(f3(x3453,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[333,336,47,331,14,2,19,7])).
% 45.53/45.62 cnf(347,plain,
% 45.53/45.62 (E(f3(f3(x3471,a4),f3(a4,a4)),a2)),
% 45.53/45.62 inference(scs_inference,[],[333,336,166,47,331,14,2,19,7,3])).
% 45.53/45.62 cnf(350,plain,
% 45.53/45.62 (E(f3(f3(x3501,x3501),a4),f3(f3(x3502,a4),f3(x3503,a4)))),
% 45.53/45.62 inference(scs_inference,[],[341,2])).
% 45.53/45.62 cnf(351,plain,
% 45.53/45.62 (E(f3(f3(f3(x3511,a4),f3(a4,a4)),x3512),f3(f3(a4,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[341,47,345,2,19])).
% 45.53/45.62 cnf(352,plain,
% 45.53/45.62 (P1(f3(f3(f3(x3521,a4),f3(a4,a4)),x3522),f3(f3(x3523,a4),f3(a4,a4)))),
% 45.53/45.62 inference(rename_variables,[],[345])).
% 45.53/45.62 cnf(360,plain,
% 45.53/45.62 (E(f3(a2,x3601),f3(f3(x3602,a4),f3(x3603,a4)))),
% 45.53/45.62 inference(scs_inference,[],[340,341,300,47,345,352,272,2,19,6,7,3])).
% 45.53/45.62 cnf(362,plain,
% 45.53/45.62 (E(f3(f3(a4,a4),f3(a4,a4)),f3(f3(f3(x3621,a4),f3(a4,a4)),x3622))),
% 45.53/45.62 inference(scs_inference,[],[351,2])).
% 45.53/45.62 cnf(363,plain,
% 45.53/45.62 (P1(f3(f3(x3631,a4),x3632),f3(f3(a4,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[351,339,2,7])).
% 45.53/45.62 cnf(365,plain,
% 45.53/45.62 (E(f3(f3(x3651,x3652),a4),f3(f3(x3653,a4),f3(x3654,a4)))),
% 45.53/45.62 inference(scs_inference,[],[351,350,330,339,2,7,3])).
% 45.53/45.62 cnf(367,plain,
% 45.53/45.62 (E(f3(f3(x3671,a4),f3(x3672,a4)),f3(a2,x3673))),
% 45.53/45.62 inference(scs_inference,[],[360,2])).
% 45.53/45.62 cnf(369,plain,
% 45.53/45.62 (P1(f3(f3(x3691,x3691),x3692),x3693)),
% 45.53/45.62 inference(rename_variables,[],[47])).
% 45.53/45.62 cnf(371,plain,
% 45.53/45.62 (E(f3(a2,x3711),f3(f3(f3(x3712,a4),f3(a4,a4)),x3713))),
% 45.53/45.62 inference(scs_inference,[],[362,360,47,363,2,6,7,3])).
% 45.53/45.62 cnf(373,plain,
% 45.53/45.62 (E(f3(f3(x3731,a4),x3732),f3(f3(f3(a4,a4),f3(a4,a4)),x3733))),
% 45.53/45.62 inference(scs_inference,[],[362,360,47,369,363,2,6,7,3,19])).
% 45.53/45.62 cnf(376,plain,
% 45.53/45.62 (E(f3(f3(f3(a4,a4),f3(a4,a4)),x3761),f3(f3(x3762,a4),x3763))),
% 45.53/45.62 inference(scs_inference,[],[373,2])).
% 45.53/45.62 cnf(377,plain,
% 45.53/45.62 (P1(f3(f3(x3771,x3772),f3(a4,x3772)),f3(f3(f3(a4,a4),f3(a4,a4)),x3773))),
% 45.53/45.62 inference(scs_inference,[],[373,15,2,7])).
% 45.53/45.62 cnf(379,plain,
% 45.53/45.62 (E(f3(f3(x3791,a4),f3(x3792,a4)),f3(f3(f3(x3793,a4),f3(a4,a4)),x3794))),
% 45.53/45.62 inference(scs_inference,[],[373,371,367,15,2,7,3])).
% 45.53/45.62 cnf(381,plain,
% 45.53/45.62 (E(f3(f3(f3(x3811,a4),f3(a4,a4)),x3812),f3(f3(x3813,a4),f3(x3814,a4)))),
% 45.53/45.62 inference(scs_inference,[],[379,2])).
% 45.53/45.62 cnf(384,plain,
% 45.53/45.62 (P1(f3(f3(x3841,x3842),f3(a4,x3842)),f3(f3(x3843,a4),x3844))),
% 45.53/45.62 inference(scs_inference,[],[376,379,47,377,2,6,7])).
% 45.53/45.62 cnf(386,plain,
% 45.53/45.62 (E(f3(f3(x3861,a4),f3(x3862,a4)),f3(f3(x3863,a4),x3864))),
% 45.53/45.62 inference(scs_inference,[],[376,379,47,377,2,6,7,3])).
% 45.53/45.62 cnf(389,plain,
% 45.53/45.62 (E(f3(f3(x3891,a4),x3892),f3(f3(x3893,a4),f3(x3894,a4)))),
% 45.53/45.62 inference(scs_inference,[],[386,2])).
% 45.53/45.62 cnf(390,plain,
% 45.53/45.62 (E(f3(f3(f3(x3901,a4),f3(a4,a4)),x3902),a2)),
% 45.53/45.62 inference(scs_inference,[],[381,386,347,2,3])).
% 45.53/45.62 cnf(393,plain,
% 45.53/45.62 (E(f3(f3(x3931,a4),f3(x3932,a4)),f3(f3(x3933,x3934),a4))),
% 45.53/45.62 inference(scs_inference,[],[365,2])).
% 45.53/45.62 cnf(394,plain,
% 45.53/45.62 (P1(f3(f3(f3(x3941,a4),x3942),x3943),f3(f3(x3944,a4),f3(x3945,a4)))),
% 45.53/45.62 inference(scs_inference,[],[389,365,14,2,7])).
% 45.53/45.62 cnf(396,plain,
% 45.53/45.62 (E(f3(x3961,x3961),f3(f3(x3962,a4),f3(x3963,a4)))),
% 45.53/45.62 inference(scs_inference,[],[389,365,293,14,2,7,3])).
% 45.53/45.62 cnf(399,plain,
% 45.53/45.62 (E(f3(f3(x3991,a4),f3(x3992,a4)),f3(x3993,x3993))),
% 45.53/45.62 inference(scs_inference,[],[396,2])).
% 45.53/45.62 cnf(400,plain,
% 45.53/45.62 (E(f3(f3(f3(x4001,a4),f3(a4,a4)),x4002),f3(f3(x4003,x4003),x4004))),
% 45.53/45.62 inference(scs_inference,[],[396,390,45,2,3])).
% 45.53/45.62 cnf(401,plain,
% 45.53/45.62 (E(f3(f3(x4011,x4011),x4012),f3(f3(f3(x4013,a4),f3(a4,a4)),x4014))),
% 45.53/45.62 inference(scs_inference,[],[400,2])).
% 45.53/45.62 cnf(402,plain,
% 45.53/45.62 (P1(f3(f3(x4021,x4022),f3(a4,x4022)),f3(x4023,x4023))),
% 45.53/45.62 inference(scs_inference,[],[400,399,384,2,7])).
% 45.53/45.62 cnf(404,plain,
% 45.53/45.62 (E(f3(f3(f3(x4041,a4),f3(a4,a4)),x4042),f3(f3(x4043,x4044),a4))),
% 45.53/45.62 inference(scs_inference,[],[400,399,393,384,2,7,3])).
% 45.53/45.62 cnf(408,plain,
% 45.53/45.62 (P1(f3(f3(x4081,x4082),f3(a4,x4082)),f3(f3(f3(x4083,a4),f3(a4,a4)),x4084))),
% 45.53/45.62 inference(scs_inference,[],[401,404,402,2,7])).
% 45.53/45.62 cnf(410,plain,
% 45.53/45.62 (E(f3(f3(x4101,x4101),x4102),f3(f3(f3(x4103,a4),f3(a4,a4)),x4104))),
% 45.53/45.62 inference(rename_variables,[],[401])).
% 45.53/45.62 cnf(411,plain,
% 45.53/45.62 (E(f3(f3(x4111,x4111),x4112),f3(f3(x4113,a4),f3(x4114,a4)))),
% 45.53/45.62 inference(scs_inference,[],[401,410,404,381,402,2,7,3])).
% 45.53/45.62 cnf(413,plain,
% 45.53/45.62 (E(f3(f3(x4131,a4),f3(x4132,a4)),f3(f3(x4133,x4133),x4134))),
% 45.53/45.62 inference(scs_inference,[],[411,2])).
% 45.53/45.62 cnf(414,plain,
% 45.53/45.62 (E(f3(f3(f3(x4141,a4),f3(a4,a4)),x4142),f3(a2,x4143))),
% 45.53/45.62 inference(scs_inference,[],[411,390,205,2,3])).
% 45.53/45.62 cnf(418,plain,
% 45.53/45.62 (E(f3(f3(x4181,a4),f3(x4182,a4)),f3(x4183,a4))),
% 45.53/45.62 inference(scs_inference,[],[413,414,303,347,408,2,7,3])).
% 45.53/45.62 cnf(421,plain,
% 45.53/45.62 (E(f3(f3(x4211,x4212),f3(a4,x4212)),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[413,414,303,347,29,408,2,7,3,19])).
% 45.53/45.62 cnf(424,plain,
% 45.53/45.62 (E(f3(a2,a2),f3(f3(x4241,x4242),f3(a4,x4242)))),
% 45.53/45.62 inference(scs_inference,[],[421,2])).
% 45.53/45.62 cnf(427,plain,
% 45.53/45.62 (E(f3(f3(x4271,x4272),f3(a4,x4272)),f3(f3(f3(x4273,a4),f3(a4,a4)),x4274))),
% 45.53/45.62 inference(scs_inference,[],[421,371,15,2,7,3])).
% 45.53/45.62 cnf(429,plain,
% 45.53/45.62 (E(f3(f3(x4291,f3(a4,x4292)),f3(x4292,f3(a4,x4292))),f3(a2,a2))),
% 45.53/45.62 inference(scs_inference,[],[421,371,15,29,2,7,3,19])).
% 45.53/45.62 cnf(432,plain,
% 45.53/45.62 (E(f3(a2,a2),f3(f3(x4321,f3(a4,x4322)),f3(x4322,f3(a4,x4322))))),
% 45.53/45.62 inference(scs_inference,[],[429,2])).
% 45.53/45.62 cnf(435,plain,
% 45.53/45.62 (E(f3(f3(x4351,x4352),f3(a4,x4352)),f3(f3(x4353,a4),f3(a4,a4)))),
% 45.53/45.62 inference(scs_inference,[],[429,424,427,322,179,2,6,3])).
% 45.53/45.62 cnf(439,plain,
% 45.53/45.62 (E(f3(f3(x4391,a4),f3(a4,a4)),f3(f3(x4392,x4393),f3(a4,x4393)))),
% 45.53/45.62 inference(scs_inference,[],[435,2])).
% 45.53/45.62 cnf(442,plain,
% 45.53/45.62 (E(f3(f3(x4421,x4422),f3(a4,x4422)),f3(x4423,a4))),
% 45.53/45.62 inference(scs_inference,[],[432,435,418,29,2,6,3])).
% 45.53/45.62 cnf(444,plain,
% 45.53/45.62 (E(f3(x4441,a4),f3(f3(x4442,x4443),f3(a4,x4443)))),
% 45.53/45.62 inference(scs_inference,[],[442,2])).
% 45.53/45.62 cnf(445,plain,
% 45.53/45.62 (P1(f3(f3(f3(x4451,a4),x4452),x4453),f3(f3(x4454,x4455),f3(a4,x4455)))),
% 45.53/45.62 inference(scs_inference,[],[439,442,394,2,7])).
% 45.53/45.62 cnf(447,plain,
% 45.53/45.62 (E(f3(f3(x4471,x4472),f3(a4,x4472)),f3(f3(f3(x4473,x4473),x4474),x4475))),
% 45.53/45.62 inference(scs_inference,[],[439,442,160,394,2,7,3])).
% 45.53/45.62 cnf(450,plain,
% 45.53/45.62 (E(f3(f3(f3(x4501,x4501),x4502),x4503),f3(f3(x4504,x4505),f3(a4,x4505)))),
% 45.53/45.62 inference(scs_inference,[],[447,2])).
% 45.53/45.62 cnf(451,plain,
% 45.53/45.62 (E(f3(f3(x4511,x4512),f3(a4,x4512)),f3(f3(x4513,x4514),f3(a4,x4514)))),
% 45.53/45.62 inference(scs_inference,[],[447,444,2,3])).
% 45.53/45.62 cnf(454,plain,
% 45.53/45.62 (E(f3(f3(f3(x4541,a4),f3(a4,a4)),x4542),f3(f3(x4543,x4544),f3(a4,x4544)))),
% 45.53/45.62 inference(scs_inference,[],[427,2])).
% 45.53/45.62 cnf(455,plain,
% 45.53/45.62 (E(f3(f3(f3(x4551,x4551),x4552),x4553),f3(f3(x4554,a4),f3(x4555,a4)))),
% 45.53/45.62 inference(scs_inference,[],[450,427,381,2,3])).
% 45.53/45.62 cnf(458,plain,
% 45.53/45.62 (E(f3(f3(x4581,a4),f3(x4582,a4)),f3(f3(f3(x4583,x4583),x4584),x4585))),
% 45.53/45.62 inference(scs_inference,[],[455,2])).
% 45.53/45.62 cnf(459,plain,
% 45.53/45.62 (E(f3(f3(f3(x4591,a4),f3(a4,a4)),x4592),f3(x4593,a4))),
% 45.53/45.62 inference(scs_inference,[],[454,455,418,2,3])).
% 45.53/45.62 cnf(462,plain,
% 45.53/45.62 (E(f3(x4621,a4),f3(f3(f3(x4622,a4),f3(a4,a4)),x4623))),
% 45.53/45.62 inference(scs_inference,[],[459,2])).
% 45.53/45.62 cnf(463,plain,
% 45.53/45.62 (P1(f3(f3(f3(x4631,x4632),f3(a4,x4632)),x4633),f3(f3(x4634,x4635),f3(a4,x4635)))),
% 45.53/45.62 inference(scs_inference,[],[451,459,14,2,7])).
% 45.53/45.62 cnf(465,plain,
% 45.53/45.62 (E(f3(f3(x4651,x4652),f3(a4,x4652)),f3(a2,x4653))),
% 45.53/45.62 inference(scs_inference,[],[451,459,315,14,2,7,3])).
% 45.53/45.62 cnf(468,plain,
% 45.53/45.62 (E(f3(a2,x4681),f3(f3(x4682,x4683),f3(a4,x4683)))),
% 45.53/45.62 inference(scs_inference,[],[465,2])).
% 45.53/45.62 cnf(469,plain,
% 45.53/45.62 (E(f3(f3(x4691,a4),f3(x4692,a4)),f3(f3(x4693,x4694),f3(a4,x4694)))),
% 45.53/45.62 inference(scs_inference,[],[458,465,444,2,3])).
% 45.53/45.62 cnf(472,plain,
% 45.53/45.62 (E(f3(f3(x4721,x4722),f3(a4,x4722)),f3(f3(x4723,a4),f3(x4724,a4)))),
% 45.53/45.62 inference(scs_inference,[],[469,2])).
% 45.53/45.62 cnf(473,plain,
% 45.53/45.62 (E(f3(x4731,a4),f3(f3(x4732,a4),f3(x4733,a4)))),
% 45.53/45.62 inference(scs_inference,[],[469,462,365,2,3])).
% 45.53/45.62 cnf(476,plain,
% 45.53/45.62 (E(a2,f3(f3(f3(x4761,a4),f3(a4,a4)),x4762))),
% 45.53/45.62 inference(scs_inference,[],[390,2])).
% 45.53/45.62 cnf(479,plain,
% 45.53/45.62 (E(f3(f3(x4791,x4791),x4792),f3(f3(x4793,x4794),f3(a4,x4794)))),
% 45.53/45.62 inference(scs_inference,[],[472,149,444,390,463,2,7,3])).
% 45.53/45.62 cnf(482,plain,
% 45.53/45.62 (E(f3(f3(f3(x4821,x4822),f3(a4,x4822)),x4823),f3(f3(a4,a4),f3(x4824,a4)))),
% 45.53/45.62 inference(scs_inference,[],[472,149,444,390,47,463,2,7,3,19])).
% 45.53/45.62 cnf(485,plain,
% 45.53/45.62 (E(f3(f3(x4851,x4852),f3(a4,x4852)),f3(f3(x4853,x4853),x4854))),
% 45.53/45.62 inference(scs_inference,[],[479,2])).
% 45.53/45.62 cnf(486,plain,
% 45.53/45.62 (E(a2,f3(f3(x4861,a4),f3(x4862,a4)))),
% 45.53/45.63 inference(scs_inference,[],[479,473,476,2,3])).
% 45.53/45.63 cnf(489,plain,
% 45.53/45.63 (E(f3(f3(a4,a4),f3(x4891,a4)),f3(f3(f3(x4892,x4893),f3(a4,x4893)),x4894))),
% 45.53/45.63 inference(scs_inference,[],[482,2])).
% 45.53/45.63 cnf(492,plain,
% 45.53/45.63 (E(f3(f3(x4921,x4922),f3(a4,x4922)),a2)),
% 45.53/45.63 inference(scs_inference,[],[485,482,347,445,2,7,3])).
% 45.53/45.63 cnf(497,plain,
% 45.53/45.63 (E(f3(f3(f3(x4971,a4),x4972),x4973),f3(f3(a4,a4),f3(a4,a4)))),
% 45.53/45.63 inference(scs_inference,[],[485,482,347,47,445,2,7,3,18,19])).
% 45.53/45.63 cnf(500,plain,
% 45.53/45.63 (E(f3(f3(a4,a4),f3(a4,a4)),f3(f3(f3(x5001,a4),x5002),x5003))),
% 45.53/45.63 inference(scs_inference,[],[497,2])).
% 45.53/45.63 cnf(501,plain,
% 45.53/45.63 (E(f3(f3(f3(x5011,a4),x5012),x5013),a2)),
% 45.53/45.63 inference(scs_inference,[],[497,492,2,3])).
% 45.53/45.63 cnf(503,plain,
% 45.53/45.63 (E(a2,f3(f3(f3(x5031,a4),x5032),x5033))),
% 45.53/45.63 inference(scs_inference,[],[501,2])).
% 45.53/45.63 cnf(506,plain,
% 45.53/45.63 (E(f3(a2,x5061),f3(f3(f3(x5062,a4),x5063),x5064))),
% 45.53/45.63 inference(scs_inference,[],[500,468,501,47,2,6,3])).
% 45.53/45.63 cnf(508,plain,
% 45.53/45.63 (E(f3(f3(f3(x5081,a4),x5082),x5083),f3(a2,x5084))),
% 45.53/45.63 inference(scs_inference,[],[506,2])).
% 45.53/45.63 cnf(511,plain,
% 45.53/45.63 (E(a2,f3(f3(f3(x5111,x5112),f3(a4,x5112)),x5113))),
% 45.53/45.63 inference(scs_inference,[],[489,506,486,15,2,6,3])).
% 45.53/45.63 cnf(514,plain,
% 45.53/45.63 (E(f3(f3(f3(x5141,x5142),f3(a4,x5142)),x5143),f3(f3(a4,a4),a4))),
% 45.53/45.63 inference(scs_inference,[],[489,506,486,15,47,2,6,3,19])).
% 45.53/45.63 cnf(517,plain,
% 45.53/45.63 (E(f3(f3(a4,a4),a4),f3(f3(f3(x5171,x5172),f3(a4,x5172)),x5173))),
% 45.53/45.63 inference(scs_inference,[],[514,2])).
% 45.53/45.63 cnf(519,plain,
% 45.53/45.63 (E(f3(f3(f3(x5191,a4),x5192),x5193),f3(f3(x5194,x5195),f3(a4,x5195)))),
% 45.53/45.63 inference(scs_inference,[],[514,508,511,468,12,2,6,3])).
% 45.53/45.63 cnf(522,plain,
% 45.53/45.63 (E(f3(f3(x5221,x5222),f3(a4,x5222)),f3(f3(f3(x5223,a4),x5224),x5225))),
% 45.53/45.63 inference(scs_inference,[],[519,2])).
% 45.53/45.63 cnf(523,plain,
% 45.53/45.63 (E(f3(f3(f3(x5231,a4),x5232),x5233),f3(f3(a4,a4),a4))),
% 45.53/45.63 inference(scs_inference,[],[519,514,2,3])).
% 45.53/45.63 cnf(527,plain,
% 45.53/45.63 (E(f3(f3(f3(x5271,a4),x5272),x5273),f3(f3(x5274,a4),f3(x5275,a4)))),
% 45.53/45.63 inference(scs_inference,[],[523,473,2,3])).
% 45.53/45.63 cnf(530,plain,
% 45.53/45.63 (E(f3(f3(x5301,a4),f3(x5302,a4)),f3(f3(f3(x5303,x5304),f3(a4,x5304)),x5305))),
% 45.53/45.63 inference(scs_inference,[],[527,517,413,2,3])).
% 45.53/45.63 cnf(532,plain,
% 45.53/45.63 (E(f3(f3(f3(x5321,x5322),f3(a4,x5322)),x5323),f3(f3(x5324,a4),f3(x5325,a4)))),
% 45.53/45.63 inference(scs_inference,[],[530,2])).
% 45.53/45.63 cnf(533,plain,
% 45.53/45.63 (E(f3(f3(f3(x5331,a4),x5332),x5333),f3(f3(x5334,x5334),x5335))),
% 45.53/45.63 inference(scs_inference,[],[530,501,45,2,3])).
% 45.53/45.63 cnf(534,plain,
% 45.53/45.63 (E(f3(f3(x5341,x5341),x5342),f3(f3(f3(x5343,a4),x5344),x5345))),
% 45.53/45.63 inference(scs_inference,[],[533,2])).
% 45.53/45.63 cnf(535,plain,
% 45.53/45.63 (E(f3(f3(x5351,x5352),f3(a4,x5352)),f3(f3(f3(x5353,x5354),f3(a4,x5354)),x5355))),
% 45.53/45.63 inference(scs_inference,[],[533,511,492,2,3])).
% 45.53/45.63 cnf(536,plain,
% 45.53/45.63 (E(f3(f3(f3(x5361,x5362),f3(a4,x5362)),x5363),f3(f3(x5364,x5365),f3(a4,x5365)))),
% 45.53/45.63 inference(scs_inference,[],[535,2])).
% 45.53/45.63 cnf(537,plain,
% 45.53/45.63 (E(f3(f3(x5371,x5371),x5372),f3(f3(f3(x5373,x5374),f3(a4,x5374)),x5375))),
% 45.53/45.63 inference(scs_inference,[],[534,535,530,2,3])).
% 45.53/45.63 cnf(540,plain,
% 45.53/45.63 (E(f3(f3(f3(x5401,x5402),f3(a4,x5402)),x5403),f3(f3(x5404,x5404),x5405))),
% 45.53/45.63 inference(scs_inference,[],[537,2])).
% 45.53/45.63 cnf(541,plain,
% 45.53/45.63 (E(f3(f3(f3(x5411,x5412),f3(a4,x5412)),x5413),f3(a2,x5414))),
% 45.53/45.63 inference(scs_inference,[],[537,536,367,2,3])).
% 45.53/45.63 cnf(544,plain,
% 45.53/45.63 (E(f3(a2,x5441),f3(f3(f3(x5442,x5443),f3(a4,x5443)),x5444))),
% 45.53/45.63 inference(scs_inference,[],[541,2])).
% 45.53/45.63 cnf(545,plain,
% 45.53/45.63 (E(f3(f3(f3(x5451,x5452),f3(a4,x5452)),x5453),f3(x5454,a4))),
% 45.53/45.63 inference(scs_inference,[],[540,541,442,2,3])).
% 45.53/45.63 cnf(548,plain,
% 45.53/45.63 (E(f3(x5481,a4),f3(f3(f3(x5482,x5483),f3(a4,x5483)),x5484))),
% 45.53/45.63 inference(scs_inference,[],[545,2])).
% 45.53/45.63 cnf(549,plain,
% 45.53/45.63 (E(f3(f3(f3(x5491,a4),x5492),x5493),f3(x5494,a4))),
% 45.53/45.63 inference(scs_inference,[],[545,501,263,2,3])).
% 45.53/45.63 cnf(550,plain,
% 45.53/45.63 (E(f3(x5501,a4),f3(f3(f3(x5502,a4),x5503),x5504))),
% 45.53/45.63 inference(scs_inference,[],[549,2])).
% 45.53/45.63 cnf(551,plain,
% 45.53/45.63 (E(f3(f3(x5511,x5512),f3(a4,x5512)),f3(f3(x5513,a4),x5514))),
% 45.53/45.63 inference(scs_inference,[],[522,549,376,2,3])).
% 45.53/45.63 cnf(554,plain,
% 45.53/45.63 (E(f3(f3(x5541,a4),x5542),f3(f3(x5543,x5544),f3(a4,x5544)))),
% 45.53/45.63 inference(scs_inference,[],[551,2])).
% 45.53/45.63 cnf(555,plain,
% 45.53/45.63 (E(f3(f3(x5551,x5552),f3(a4,x5552)),f3(x5553,x5553))),
% 45.53/45.63 inference(scs_inference,[],[551,492,24,2,3])).
% 45.53/45.63 cnf(556,plain,
% 45.53/45.63 (E(f3(x5561,x5561),f3(f3(x5562,x5563),f3(a4,x5563)))),
% 45.53/45.63 inference(scs_inference,[],[555,2])).
% 45.53/45.63 cnf(557,plain,
% 45.53/45.63 (E(f3(f3(f3(x5571,x5572),f3(a4,x5572)),x5573),a2)),
% 45.53/45.63 inference(scs_inference,[],[555,532,246,2,3])).
% 45.53/45.63 cnf(560,plain,
% 45.53/45.63 (E(f3(f3(x5601,a4),f3(x5602,a4)),a2)),
% 45.53/45.63 inference(scs_inference,[],[486,2])).
% 45.53/45.63 cnf(561,plain,
% 45.53/45.63 (E(f3(x5611,x5611),f3(f3(f3(x5612,x5613),f3(a4,x5613)),x5614))),
% 45.53/45.63 inference(scs_inference,[],[556,486,530,2,3])).
% 45.53/45.63 cnf(564,plain,
% 45.53/45.63 (E(f3(f3(f3(x5641,x5642),f3(a4,x5642)),x5643),f3(x5644,x5644))),
% 45.53/45.63 inference(scs_inference,[],[561,2])).
% 45.53/45.63 cnf(565,plain,
% 45.53/45.63 (E(f3(f3(x5651,a4),x5652),a2)),
% 45.53/45.63 inference(scs_inference,[],[561,554,560,2,3])).
% 45.53/45.63 cnf(571,plain,
% 45.53/45.63 (E(f3(f3(f3(x5711,x5712),f3(a4,x5712)),x5713),f3(f3(x5714,a4),x5715))),
% 45.53/45.63 inference(scs_inference,[],[564,565,376,15,2,7,3])).
% 45.53/45.63 cnf(575,plain,
% 45.53/45.63 (E(f3(f3(x5751,a4),x5752),f3(f3(f3(x5753,x5754),f3(a4,x5754)),x5755))),
% 45.53/45.63 inference(scs_inference,[],[571,2])).
% 45.53/45.63 cnf(576,plain,
% 45.53/45.63 (E(f3(f3(x5761,f3(a4,x5762)),f3(x5762,f3(a4,x5762))),a2)),
% 45.53/45.63 inference(scs_inference,[],[429,571,10,2,3])).
% 45.53/45.63 cnf(578,plain,
% 45.53/45.63 (P1(f3(x5781,f3(a4,x5782)),f3(x5782,f3(a4,x5782)))),
% 45.53/45.63 inference(scs_inference,[],[429,571,10,2,3,18])).
% 45.53/45.63 cnf(580,plain,
% 45.53/45.63 (P1(f3(x5801,f3(a4,a2)),f3(f3(f3(x5802,x5803),f3(a4,x5803)),x5804))),
% 45.53/45.63 inference(scs_inference,[],[544,429,571,10,2,3,18,7])).
% 45.53/45.63 cnf(582,plain,
% 45.53/45.63 (E(a2,f3(f3(x5821,f3(a4,x5822)),f3(x5822,f3(a4,x5822))))),
% 45.53/45.63 inference(scs_inference,[],[576,2])).
% 45.53/45.63 cnf(583,plain,
% 45.53/45.63 (E(f3(f3(x5831,a4),x5832),f3(a2,x5833))),
% 45.53/45.63 inference(scs_inference,[],[575,576,541,2,3])).
% 45.53/45.63 cnf(588,plain,
% 45.53/45.63 (E(f3(f3(x5881,a4),x5882),f3(a2,x5883))),
% 45.53/45.63 inference(rename_variables,[],[583])).
% 45.53/45.63 cnf(589,plain,
% 45.53/45.63 (E(f3(f3(x5891,a4),x5892),f3(f3(f3(x5893,a4),x5894),x5895))),
% 45.53/45.63 inference(scs_inference,[],[583,588,506,578,2,7,3])).
% 45.53/45.63 cnf(591,plain,
% 45.53/45.63 (E(f3(f3(f3(x5911,a4),x5912),x5913),f3(f3(x5914,a4),x5915))),
% 45.53/45.63 inference(scs_inference,[],[589,2])).
% 45.53/45.63 cnf(592,plain,
% 45.53/45.63 (E(f3(f3(x5921,a4),x5922),f3(f3(x5923,a4),x5924))),
% 45.53/45.63 inference(scs_inference,[],[589,571,2,3])).
% 45.53/45.63 cnf(596,plain,
% 45.53/45.63 (P1(f3(x5961,f3(a4,a2)),f3(f3(x5962,a4),x5963))),
% 45.53/45.63 inference(scs_inference,[],[591,492,580,2,7])).
% 45.53/45.63 cnf(599,plain,
% 45.53/45.63 (E(f3(x5991,a4),f3(f3(x5992,a4),x5993))),
% 45.53/45.63 inference(scs_inference,[],[591,548,571,492,580,2,7,3])).
% 45.53/45.63 cnf(601,plain,
% 45.53/45.63 (E(f3(f3(x6011,a4),x6012),f3(x6013,a4))),
% 45.53/45.63 inference(scs_inference,[],[599,2])).
% 45.53/45.63 cnf(602,plain,
% 45.53/45.63 (P1(f3(x6021,f3(a4,f3(x6022,a4))),f3(f3(x6023,a4),x6024))),
% 45.53/45.63 inference(scs_inference,[],[592,599,578,2,7])).
% 45.53/45.63 cnf(606,plain,
% 45.53/45.63 (P1(f3(x6061,f3(a4,a2)),f3(f3(f3(x6062,a4),x6063),x6064))),
% 45.53/45.63 inference(scs_inference,[],[550,596,8,2,7])).
% 45.53/45.63 cnf(609,plain,
% 45.53/45.63 (E(f3(f3(x6091,a4),x6092),f3(f3(x6093,x6093),x6094))),
% 45.53/45.63 inference(scs_inference,[],[550,601,63,596,8,2,7,3])).
% 45.53/45.63 cnf(612,plain,
% 45.53/45.63 (E(f3(f3(x6121,x6121),x6122),f3(f3(x6123,a4),x6124))),
% 45.53/45.63 inference(scs_inference,[],[609,2])).
% 45.53/45.63 cnf(613,plain,
% 45.53/45.63 (P1(f3(x6131,f3(a4,a2)),f3(f3(x6132,x6132),x6133))),
% 45.53/45.63 inference(scs_inference,[],[609,606,2,7])).
% 45.53/45.63 cnf(616,plain,
% 45.53/45.63 (P1(f3(x6161,f3(a4,f3(x6162,x6162))),f3(f3(x6163,a4),x6164))),
% 45.53/45.63 inference(scs_inference,[],[612,578,7])).
% 45.53/45.63 cnf(623,plain,
% 45.53/45.63 (E(f3(f3(f3(x6231,x6232),x6233),f3(f3(a4,x6232),x6233)),a2)),
% 45.53/45.63 inference(scs_inference,[],[557,12,15,7,19])).
% 45.53/45.63 cnf(628,plain,
% 45.53/45.63 (E(a2,f3(f3(f3(x6281,x6282),x6283),f3(f3(a4,x6282),x6283)))),
% 45.53/45.63 inference(scs_inference,[],[557,12,15,7,19,18,2])).
% 45.53/45.63 cnf(632,plain,
% 45.53/45.63 (E(f3(f3(f3(x6321,x6322),x6323),f3(f3(a4,x6322),x6323)),a2)),
% 45.53/45.63 inference(rename_variables,[],[623])).
% 45.53/45.63 cnf(633,plain,
% 45.53/45.63 (E(f3(f3(f3(x6331,x6332),x6333),f3(f3(a4,x6332),x6333)),f3(a2,x6334))),
% 45.53/45.63 inference(scs_inference,[],[623,632,628,205,12,613,6,7,3])).
% 45.53/45.63 cnf(635,plain,
% 45.53/45.63 (E(f3(x6351,f3(a4,a2)),a2)),
% 45.53/45.63 inference(scs_inference,[],[623,632,628,205,12,613,6,7,3,2,19])).
% 45.53/45.63 cnf(638,plain,
% 45.53/45.63 (P1(x6381,f3(a4,a2))),
% 45.53/45.63 inference(scs_inference,[],[623,632,628,205,12,613,6,7,3,2,19,18])).
% 45.53/45.63 cnf(640,plain,
% 45.53/45.63 (E(a2,f3(x6401,f3(a4,a2)))),
% 45.53/45.63 inference(scs_inference,[],[635,2])).
% 45.53/45.63 cnf(641,plain,
% 45.53/45.63 (E(a4,f3(a4,a2))),
% 45.53/45.63 inference(scs_inference,[],[635,11,638,2,19])).
% 45.53/45.63 cnf(645,plain,
% 45.53/45.63 (P1(f3(x6451,f3(a4,f3(x6452,x6452))),f3(a2,x6453))),
% 45.53/45.63 inference(scs_inference,[],[633,635,11,638,616,2,19,7])).
% 45.53/45.63 cnf(648,plain,
% 45.53/45.63 (E(f3(x6481,f3(a4,a2)),f3(f3(f3(x6482,a4),x6483),x6484))),
% 45.53/45.63 inference(scs_inference,[],[633,503,635,11,638,616,2,19,7,3])).
% 45.53/45.63 cnf(650,plain,
% 45.53/45.63 (E(f3(x6501,f3(a4,a2)),f3(f3(f3(x6502,x6503),f3(a4,x6503)),x6504))),
% 45.53/45.63 inference(scs_inference,[],[648,575,2,3])).
% 45.53/45.63 cnf(653,plain,
% 45.53/45.63 (P1(x6531,x6532)+~E(f3(a4,a2),x6532)),
% 45.53/45.63 inference(scs_inference,[],[648,575,638,2,3,7])).
% 45.53/45.63 cnf(654,plain,
% 45.53/45.63 (~P1(f3(a4,a1),f3(a4,f3(a4,f3(a4,a1))))+~E(f3(a4,a2),f3(a4,a1))),
% 45.53/45.63 inference(scs_inference,[],[16,648,575,638,2,3,7,19])).
% 45.53/45.63 cnf(660,plain,
% 45.53/45.63 (E(f3(a4,a2),a4)),
% 45.53/45.63 inference(scs_inference,[],[641,2])).
% 45.53/45.63 cnf(661,plain,
% 45.53/45.63 (P1(f3(x6611,f3(a4,f3(x6612,a4))),a2)),
% 45.53/45.63 inference(scs_inference,[],[641,623,602,2,7])).
% 45.53/45.63 cnf(664,plain,
% 45.53/45.63 (E(f3(x6641,f3(a4,a2)),f3(a2,x6642))),
% 45.53/45.63 inference(scs_inference,[],[641,623,650,633,602,2,7,3])).
% 45.53/45.63 cnf(669,plain,
% 45.53/45.63 (E(f3(x6691,f3(a4,f3(x6692,a4))),a2)),
% 45.53/45.63 inference(scs_inference,[],[664,12,661,2,19])).
% 45.53/45.63 cnf(672,plain,
% 45.53/45.63 (P1(f3(x6721,f3(a4,f3(x6722,x6722))),a2)),
% 45.53/45.63 inference(scs_inference,[],[635,664,12,645,661,2,19,7])).
% 45.53/45.63 cnf(676,plain,
% 45.53/45.63 (P1(x6761,f3(a4,f3(x6762,a4)))),
% 45.53/45.63 inference(scs_inference,[],[557,635,664,640,12,645,661,2,19,7,3,18])).
% 45.53/45.63 cnf(678,plain,
% 45.53/45.63 (E(a2,f3(x6781,f3(a4,f3(x6782,a4))))),
% 45.53/45.63 inference(scs_inference,[],[669,2])).
% 45.53/45.63 cnf(679,plain,
% 45.53/45.63 (E(a4,f3(a4,f3(x6791,a4)))),
% 45.53/45.63 inference(scs_inference,[],[669,11,676,2,19])).
% 45.53/45.63 cnf(680,plain,
% 45.53/45.63 (P1(x6801,f3(a4,f3(x6802,a4)))),
% 45.53/45.63 inference(rename_variables,[],[676])).
% 45.53/45.63 cnf(683,plain,
% 45.53/45.63 (E(f3(f3(x6831,f3(a4,x6832)),f3(x6832,f3(a4,x6832))),f3(a2,x6833))),
% 45.53/45.63 inference(scs_inference,[],[576,669,205,11,676,2,19,3])).
% 45.53/45.63 cnf(685,plain,
% 45.53/45.63 (~E(f3(a4,f3(x6851,a4)),f3(a4,f3(a4,f3(a4,a1))))+~E(f3(a4,a2),f3(a4,a1))),
% 45.53/45.63 inference(scs_inference,[],[576,669,205,11,676,680,2,19,3,7,654])).
% 45.53/45.63 cnf(695,plain,
% 45.53/45.63 (P1(x6951,f3(a4,f3(x6952,x6952)))),
% 45.53/45.63 inference(scs_inference,[],[565,683,678,12,672,2,19,3,18])).
% 45.53/45.63 cnf(702,plain,
% 45.53/45.63 (E(f3(a4,f3(x7021,a4)),a4)),
% 45.53/45.63 inference(scs_inference,[],[679,2])).
% 45.53/45.63 cnf(707,plain,
% 45.53/45.63 (E(f3(a4,a2),f3(a4,f3(x7071,a4)))),
% 45.53/45.63 inference(scs_inference,[],[660,679,11,695,2,19,3])).
% 45.53/45.63 cnf(718,plain,
% 45.53/45.63 (E(f3(f3(a1,a2),x7181),a1)+~P1(a1,f3(f3(a1,a2),x7181))),
% 45.53/45.63 inference(scs_inference,[],[8,623,707,263,14,2,3,7,19])).
% 45.53/45.63 cnf(726,plain,
% 45.53/45.63 (E(f3(f3(x7261,f3(a4,x7262)),f3(x7262,f3(a4,x7262))),f3(x7263,a4))),
% 45.53/45.63 inference(scs_inference,[],[9,582,3,2])).
% 45.53/45.63 cnf(765,plain,
% 45.53/45.63 (~E(f3(a4,a2),f3(f3(a1,a2),x7651))+E(f3(f3(a1,a2),x7651),a1)),
% 45.53/45.63 inference(scs_inference,[],[718,653])).
% 45.53/45.63 cnf(1112,plain,
% 45.53/45.63 (~E(f3(a4,a1),f3(a4,a2))+~E(f3(a4,f3(x11121,a4)),f3(a4,f3(a4,f3(a4,a1))))),
% 45.53/45.63 inference(scs_inference,[],[685,2])).
% 45.53/45.63 cnf(1252,plain,
% 45.53/45.63 (~P1(f3(a4,a2),f3(a4,a1))+~E(f3(a4,f3(x12521,a4)),f3(a4,f3(a4,f3(a4,a1))))),
% 45.53/45.63 inference(scs_inference,[],[638,1112,19])).
% 45.53/45.63 cnf(1268,plain,
% 45.53/45.63 (~E(a4,f3(a4,a1))+~E(f3(a4,f3(x12681,a4)),f3(a4,f3(a4,f3(a4,a1))))),
% 45.53/45.63 inference(scs_inference,[],[11,1252,7])).
% 45.53/45.63 cnf(1269,plain,
% 45.53/45.63 (~E(f3(a4,a1),a4)+~E(f3(a4,f3(x12691,a4)),f3(a4,f3(a4,f3(a4,a1))))),
% 45.53/45.63 inference(scs_inference,[],[1268,2])).
% 45.53/45.63 cnf(1277,plain,
% 45.53/45.63 (~E(f3(a4,a1),f3(a4,f3(x12771,a4)))+~E(f3(a4,f3(x12772,a4)),f3(a4,f3(a4,f3(a4,a1))))),
% 45.53/45.63 inference(scs_inference,[],[702,1269,3])).
% 45.53/45.63 cnf(1790,plain,
% 45.53/45.63 (~E(a1,f3(x17901,a4))+~E(f3(a4,f3(x17902,a4)),f3(a4,f3(a4,f3(a4,a1))))),
% 45.53/45.63 inference(scs_inference,[],[1277,5])).
% 45.53/45.63 cnf(1792,plain,
% 45.53/45.63 (~E(f3(x17921,a4),f3(a4,f3(a4,a1)))+~E(a1,f3(x17922,a4))),
% 45.53/45.63 inference(scs_inference,[],[1790,5])).
% 45.53/45.63 cnf(1793,plain,
% 45.53/45.63 (~E(f3(a4,f3(a4,a1)),f3(x17931,a4))+~E(a1,f3(x17932,a4))),
% 45.53/45.63 inference(scs_inference,[],[1792,2])).
% 45.53/45.63 cnf(1794,plain,
% 45.53/45.63 (~E(f3(a4,a1),a4)+~E(a1,f3(x17941,a4))),
% 45.53/45.63 inference(scs_inference,[],[1793,5])).
% 45.53/45.63 cnf(1795,plain,
% 45.53/45.63 (~E(a4,f3(a4,a1))+~E(a1,f3(x17951,a4))),
% 45.53/45.63 inference(scs_inference,[],[1794,2])).
% 45.53/45.63 cnf(1796,plain,
% 45.53/45.63 (~P1(a4,f3(a4,a1))+~E(a1,f3(x17961,a4))),
% 45.53/45.63 inference(scs_inference,[],[11,1795,19])).
% 45.53/45.63 cnf(1810,plain,
% 45.53/45.63 (~E(f3(x18101,a4),a1)+~P1(a4,f3(a4,a1))),
% 45.53/45.63 inference(scs_inference,[],[1796,2])).
% 45.53/45.63 cnf(1819,plain,
% 45.53/45.63 (~E(a4,f3(a4,a1))+~E(f3(x18191,a4),a1)),
% 45.53/45.63 inference(scs_inference,[],[11,1810,7])).
% 45.53/45.63 cnf(1830,plain,
% 45.53/45.63 (~E(f3(a4,a1),a4)+~E(f3(x18301,a4),a1)),
% 45.53/45.63 inference(scs_inference,[],[1819,2])).
% 45.53/45.63 cnf(1839,plain,
% 45.53/45.63 (~E(f3(a4,a1),f3(a4,f3(x18391,a4)))+~E(f3(x18392,a4),a1)),
% 45.53/45.63 inference(scs_inference,[],[702,1830,3])).
% 45.53/45.63 cnf(1849,plain,
% 45.53/45.63 (~E(a1,f3(x18491,a4))+~E(f3(x18492,a4),a1)),
% 45.53/45.63 inference(scs_inference,[],[1839,5])).
% 45.53/45.63 cnf(1859,plain,
% 45.53/45.63 (~E(f3(x18591,a4),a1)+~E(f3(x18592,a4),a1)),
% 45.53/45.63 inference(scs_inference,[],[1849,2])).
% 45.53/45.63 cnf(1869,plain,
% 45.53/45.63 (~E(f3(a4,a2),f3(f3(a1,a2),a4))),
% 45.53/45.63 inference(scs_inference,[],[1859,765])).
% 45.53/45.63 cnf(1881,plain,
% 45.53/45.63 ($false),
% 45.53/45.63 inference(scs_inference,[],[578,16,726,11,25,14,1869,20,19,7,3,21,23]),
% 45.53/45.63 ['proof']).
% 45.53/45.63 % SZS output end Proof
% 45.53/45.63 % Total time :44.910000s
%------------------------------------------------------------------------------