%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN010-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:53 EDT 2024
% Result : Unsatisfiable 35.99s 36.07s
% Output : CNFRefutation 36.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : HEN010-4 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n028.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Sat Jun 22 05:34:39 EDT 2024
% 0.12/0.32 % CPUTime :
% 0.18/0.55 start to proof:theBenchmark
% 35.99/36.06 %-------------------------------------------
% 35.99/36.06 % File :CSE---1.7
% 35.99/36.06 % Problem :theBenchmark
% 35.99/36.06 % Transform :cnf
% 35.99/36.06 % Format :tptp:raw
% 35.99/36.06 % Command :java -jar mcs_scs.jar %d %s
% 35.99/36.06
% 35.99/36.06 % Result :Theorem 35.490000s
% 35.99/36.06 % Output :CNFRefutation 35.490000s
% 35.99/36.06 %-------------------------------------------
% 35.99/36.07 %--------------------------------------------------------------------------
% 35.99/36.07 % File : HEN010-4 : TPTP v8.2.0. Released v1.0.0.
% 35.99/36.07 % Domain : Henkin Models
% 35.99/36.07 % Problem : Define X' as identity/X. Then X' = X'/(identity/X')
% 35.99/36.07 % Version : [MOW76] axioms : Augmented.
% 35.99/36.07 % English :
% 35.99/36.07
% 35.99/36.07 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 35.99/36.07 % Source : [TPTP]
% 35.99/36.07 % Names :
% 35.99/36.07
% 35.99/36.07 % Status : Unsatisfiable
% 35.99/36.07 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.19 v5.4.0, 0.20 v5.3.0, 0.25 v5.2.0, 0.12 v5.1.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.20 v2.0.0
% 35.99/36.07 % Syntax : Number of clauses : 17 ( 10 unt; 0 nHn; 7 RR)
% 35.99/36.07 % Number of literals : 26 ( 9 equ; 10 neg)
% 35.99/36.07 % Maximal clause size : 3 ( 1 avg)
% 35.99/36.07 % Maximal term depth : 4 ( 1 avg)
% 35.99/36.07 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 35.99/36.07 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 35.99/36.07 % Number of variables : 29 ( 5 sgn)
% 35.99/36.07 % SPC : CNF_UNS_RFO_SEQ_HRN
% 35.99/36.07
% 35.99/36.07 % Comments :
% 35.99/36.07 %--------------------------------------------------------------------------
% 35.99/36.07 %----Include Henkin model axioms for equality formulation
% 35.99/36.07 include('Axioms/HEN002-0.ax').
% 35.99/36.07 %--------------------------------------------------------------------------
% 35.99/36.07 cnf(everything_divide_id_is_zero,axiom,
% 35.99/36.07 divide(X,identity) = zero ).
% 35.99/36.07
% 35.99/36.07 cnf(zero_divide_anything_is_zero,axiom,
% 35.99/36.07 divide(zero,X) = zero ).
% 35.99/36.07
% 35.99/36.07 cnf(x_divide_x_is_zero,axiom,
% 35.99/36.07 divide(X,X) = zero ).
% 35.99/36.07
% 35.99/36.07 cnf(x_divide_zero_is_x,axiom,
% 35.99/36.07 divide(a,zero) = a ).
% 35.99/36.07
% 35.99/36.07 cnf(transitivity_of_less_equal,axiom,
% 35.99/36.07 ( ~ less_equal(X,Y)
% 35.99/36.07 | ~ less_equal(Y,Z)
% 35.99/36.07 | less_equal(X,Z) ) ).
% 35.99/36.07
% 35.99/36.07 cnf(property_of_divide1,axiom,
% 35.99/36.07 ( ~ less_equal(divide(X,Y),Z)
% 35.99/36.07 | less_equal(divide(X,Z),Y) ) ).
% 35.99/36.07
% 35.99/36.07 cnf(property_of_divide2,axiom,
% 35.99/36.07 ( ~ less_equal(X,Y)
% 35.99/36.07 | less_equal(divide(Z,Y),divide(Z,X)) ) ).
% 35.99/36.07
% 35.99/36.07 cnf(property_of_divide3,axiom,
% 35.99/36.07 ( ~ less_equal(X,Y)
% 35.99/36.07 | less_equal(divide(X,Z),divide(Y,Z)) ) ).
% 35.99/36.07
% 35.99/36.07 cnf(one_inversion_equals_three,axiom,
% 35.99/36.07 divide(identity,divide(identity,divide(identity,X))) = divide(identity,X) ).
% 35.99/36.07
% 35.99/36.07 cnf(prove_property_of_inversion,negated_conjecture,
% 35.99/36.07 divide(identity,a) != divide(divide(identity,a),divide(identity,divide(identity,a))) ).
% 35.99/36.07
% 35.99/36.07 %--------------------------------------------------------------------------
% 35.99/36.07 %-------------------------------------------
% 35.99/36.07 % Proof found
% 35.99/36.07 % SZS status Theorem for theBenchmark
% 35.99/36.07 % SZS output start Proof
% 35.99/36.08 %ClaNum:24(EqnAxiom:7)
% 35.99/36.08 %VarNum:56(SingletonVarNum:29)
% 35.99/36.08 %MaxLitNum:3
% 35.99/36.08 %MaxfuncDepth:3
% 35.99/36.08 %SharedTerms:9
% 35.99/36.08 %goalClause: 17
% 35.99/36.08 %singleGoalClaCount:1
% 35.99/36.08 [8]E(f3(a1,a2),a1)
% 35.99/36.08 [17]~E(f3(f3(a4,a1),f3(a4,f3(a4,a1))),f3(a4,a1))
% 35.99/36.08 [11]P1(x111,a4)
% 35.99/36.08 [12]P1(a2,x121)
% 35.99/36.08 [9]E(f3(x91,a4),a2)
% 35.99/36.08 [10]E(f3(a2,x101),a2)
% 35.99/36.08 [13]E(f3(x131,x131),a2)
% 35.99/36.08 [15]E(f3(a4,f3(a4,f3(a4,x151))),f3(a4,x151))
% 35.99/36.08 [14]P1(f3(x141,x142),x141)
% 35.99/36.08 [16]P1(f3(f3(x161,x162),f3(x163,x162)),f3(f3(x161,x163),x162))
% 35.99/36.08 [18]~P1(x181,x182)+E(f3(x181,x182),a2)
% 35.99/36.08 [19]P1(x191,x192)+~E(f3(x191,x192),a2)
% 35.99/36.08 [22]~P1(x223,x222)+P1(f3(x221,x222),f3(x221,x223))
% 35.99/36.08 [23]~P1(x231,x233)+P1(f3(x231,x232),f3(x233,x232))
% 35.99/36.08 [24]~P1(f3(x241,x243),x242)+P1(f3(x241,x242),x243)
% 35.99/36.08 [20]~P1(x202,x201)+~P1(x201,x202)+E(x201,x202)
% 35.99/36.08 [21]~P1(x211,x213)+P1(x211,x212)+~P1(x213,x212)
% 35.99/36.08 %EqnAxiom
% 35.99/36.08 [1]E(x11,x11)
% 35.99/36.08 [2]E(x22,x21)+~E(x21,x22)
% 35.99/36.08 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 35.99/36.08 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 35.99/36.08 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 35.99/36.08 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 35.99/36.08 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 35.99/36.08
% 35.99/36.08 %-------------------------------------------
% 35.99/36.08 cnf(25,plain,
% 35.99/36.08 (E(a2,f3(x251,x251))),
% 35.99/36.08 inference(scs_inference,[],[13,2])).
% 35.99/36.08 cnf(26,plain,
% 35.99/36.08 (P1(x261,x261)),
% 35.99/36.08 inference(scs_inference,[],[13,2,19])).
% 35.99/36.08 cnf(28,plain,
% 35.99/36.08 (~P1(f3(a4,a1),f3(f3(a4,a1),f3(a4,f3(a4,a1))))),
% 35.99/36.08 inference(scs_inference,[],[17,14,13,2,19,20])).
% 35.99/36.08 cnf(31,plain,
% 35.99/36.08 (E(f3(a4,f3(a4,f3(a4,a4))),a2)),
% 35.99/36.08 inference(scs_inference,[],[17,14,13,15,2,19,20,3])).
% 35.99/36.08 cnf(34,plain,
% 35.99/36.08 (~E(a2,f3(a4,a1))),
% 35.99/36.08 inference(scs_inference,[],[17,12,14,13,15,2,19,20,3,6])).
% 35.99/36.08 cnf(38,plain,
% 35.99/36.08 (E(a2,f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.08 inference(scs_inference,[],[31,2])).
% 35.99/36.08 cnf(39,plain,
% 35.99/36.08 (P1(a4,f3(a4,f3(a4,a4)))),
% 35.99/36.08 inference(scs_inference,[],[31,2,19])).
% 35.99/36.08 cnf(41,plain,
% 35.99/36.08 (~P1(f3(a4,a1),a2)),
% 35.99/36.08 inference(scs_inference,[],[31,34,12,2,19,20])).
% 35.99/36.08 cnf(46,plain,
% 35.99/36.08 (E(f3(a4,f3(a4,f3(a4,a4))),f3(x461,x461))),
% 35.99/36.09 inference(scs_inference,[],[28,25,31,26,34,12,2,19,20,7,3])).
% 35.99/36.09 cnf(51,plain,
% 35.99/36.09 (E(f3(x511,x511),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[46,2])).
% 35.99/36.09 cnf(52,plain,
% 35.99/36.09 (E(a4,f3(a4,f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[46,39,11,2,20])).
% 35.99/36.09 cnf(55,plain,
% 35.99/36.09 (P1(f3(f3(x551,a4),f3(x552,a4)),a2)),
% 35.99/36.09 inference(scs_inference,[],[46,39,16,9,11,2,20,7])).
% 35.99/36.09 cnf(56,plain,
% 35.99/36.09 (P1(f3(f3(x561,x562),f3(x563,x562)),f3(f3(x561,x563),x562))),
% 35.99/36.09 inference(rename_variables,[],[16])).
% 35.99/36.09 cnf(58,plain,
% 35.99/36.09 (~E(f3(a2,x581),f3(a4,a1))),
% 35.99/36.09 inference(scs_inference,[],[41,46,39,16,9,11,14,2,20,7,6])).
% 35.99/36.09 cnf(60,plain,
% 35.99/36.09 (~E(a2,a4)),
% 35.99/36.09 inference(scs_inference,[],[41,46,39,16,9,11,14,2,20,7,6,4])).
% 35.99/36.09 cnf(61,plain,
% 35.99/36.09 (P1(f3(f3(x611,f3(x612,a4)),f3(a4,f3(x612,a4))),a2)),
% 35.99/36.09 inference(scs_inference,[],[41,46,39,16,56,9,11,14,2,20,7,6,4,21])).
% 35.99/36.09 cnf(64,plain,
% 35.99/36.09 (E(x641,a1)+~E(x641,f3(a1,a2))),
% 35.99/36.09 inference(scs_inference,[],[41,46,39,16,56,9,8,11,14,2,20,7,6,4,21,3])).
% 35.99/36.09 cnf(67,plain,
% 35.99/36.09 (E(f3(a4,f3(a4,a4)),a4)),
% 35.99/36.09 inference(scs_inference,[],[52,2])).
% 35.99/36.09 cnf(68,plain,
% 35.99/36.09 (P1(f3(f3(x681,f3(x682,a4)),f3(a4,f3(x682,a4))),x683)),
% 35.99/36.09 inference(scs_inference,[],[52,61,12,2,21])).
% 35.99/36.09 cnf(70,plain,
% 35.99/36.09 (E(f3(f3(x701,f3(x702,a4)),f3(a4,f3(x702,a4))),a2)),
% 35.99/36.09 inference(scs_inference,[],[52,61,12,2,21,20])).
% 35.99/36.09 cnf(73,plain,
% 35.99/36.09 (P1(f3(f3(x731,a4),f3(x732,a4)),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[38,52,61,55,12,2,21,20,7])).
% 35.99/36.09 cnf(74,plain,
% 35.99/36.09 (E(f3(x741,x741),f3(x742,x742))),
% 35.99/36.09 inference(scs_inference,[],[51,38,52,46,61,55,12,2,21,20,7,3])).
% 35.99/36.09 cnf(75,plain,
% 35.99/36.09 (~E(f3(f3(x751,f3(x752,a4)),f3(a4,f3(x752,a4))),f3(a4,a1))),
% 35.99/36.09 inference(scs_inference,[],[41,51,38,52,46,61,55,12,2,21,20,7,3,6])).
% 35.99/36.09 cnf(76,plain,
% 35.99/36.09 (P1(f3(x761,f3(x762,a4)),f3(a4,f3(x762,a4)))),
% 35.99/36.09 inference(scs_inference,[],[41,51,38,52,46,61,55,12,2,21,20,7,3,6,19])).
% 35.99/36.09 cnf(78,plain,
% 35.99/36.09 (E(a2,f3(f3(x781,f3(x782,a4)),f3(a4,f3(x782,a4))))),
% 35.99/36.09 inference(scs_inference,[],[70,2])).
% 35.99/36.09 cnf(79,plain,
% 35.99/36.09 (~P1(f3(a4,a1),f3(f3(x791,f3(x792,a4)),f3(a4,f3(x792,a4))))),
% 35.99/36.09 inference(scs_inference,[],[70,68,75,2,20])).
% 35.99/36.09 cnf(82,plain,
% 35.99/36.09 (P1(f3(x821,x821),f3(a4,f3(x822,a4)))),
% 35.99/36.09 inference(scs_inference,[],[74,70,68,75,76,2,20,6])).
% 35.99/36.09 cnf(85,plain,
% 35.99/36.09 (~E(f3(a4,a1),a2)),
% 35.99/36.09 inference(scs_inference,[],[41,74,70,68,75,76,26,2,20,6,7])).
% 35.99/36.09 cnf(87,plain,
% 35.99/36.09 (~E(f3(a4,a1),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[41,31,74,70,68,75,76,26,2,20,6,7,3])).
% 35.99/36.09 cnf(88,plain,
% 35.99/36.09 (~P1(a4,a1)),
% 35.99/36.09 inference(scs_inference,[],[41,31,74,70,68,75,76,26,2,20,6,7,3,18])).
% 35.99/36.09 cnf(91,plain,
% 35.99/36.09 (E(a2,f3(a2,x911))),
% 35.99/36.09 inference(scs_inference,[],[10,2])).
% 35.99/36.09 cnf(92,plain,
% 35.99/36.09 (E(f3(f3(x921,a4),f3(x922,a4)),a2)),
% 35.99/36.09 inference(scs_inference,[],[10,55,12,2,20])).
% 35.99/36.09 cnf(95,plain,
% 35.99/36.09 (P1(f3(x951,x951),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[74,10,73,55,12,2,20,6])).
% 35.99/36.09 cnf(99,plain,
% 35.99/36.09 (~E(a2,f3(a4,f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[67,74,10,60,73,88,39,55,12,2,20,6,7,3])).
% 35.99/36.09 cnf(101,plain,
% 35.99/36.09 (P1(f3(x1011,a4),f3(x1012,a4))),
% 35.99/36.09 inference(scs_inference,[],[67,74,10,60,73,88,39,55,12,2,20,6,7,3,64,19])).
% 35.99/36.09 cnf(103,plain,
% 35.99/36.09 (E(a2,f3(f3(x1031,a4),f3(x1032,a4)))),
% 35.99/36.09 inference(scs_inference,[],[92,2])).
% 35.99/36.09 cnf(104,plain,
% 35.99/36.09 (P1(f3(x1041,a4),f3(a4,f3(x1042,a4)))),
% 35.99/36.09 inference(scs_inference,[],[92,82,101,2,21])).
% 35.99/36.09 cnf(106,plain,
% 35.99/36.09 (P1(f3(x1061,a4),f3(x1062,a4))),
% 35.99/36.09 inference(rename_variables,[],[101])).
% 35.99/36.09 cnf(111,plain,
% 35.99/36.09 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(x1111,a4))),
% 35.99/36.09 inference(scs_inference,[],[92,51,82,101,106,60,11,2,21,20,6])).
% 35.99/36.09 cnf(114,plain,
% 35.99/36.09 (P1(f3(x1141,x1141),a2)),
% 35.99/36.09 inference(scs_inference,[],[31,92,51,82,95,101,106,60,11,2,21,20,6,7])).
% 35.99/36.09 cnf(116,plain,
% 35.99/36.09 (E(a1,f3(a1,a2))),
% 35.99/36.09 inference(scs_inference,[],[8,2])).
% 35.99/36.09 cnf(117,plain,
% 35.99/36.09 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(a4,f3(x1171,a4)))),
% 35.99/36.09 inference(scs_inference,[],[104,111,8,2,21])).
% 35.99/36.09 cnf(120,plain,
% 35.99/36.09 (~P1(f3(a4,f3(a4,a4)),a2)),
% 35.99/36.09 inference(scs_inference,[],[104,111,99,8,12,2,21,20])).
% 35.99/36.09 cnf(123,plain,
% 35.99/36.09 (~E(f3(x1231,x1231),f3(a4,a1))),
% 35.99/36.09 inference(scs_inference,[],[41,104,111,114,99,8,12,2,21,20,6])).
% 35.99/36.09 cnf(124,plain,
% 35.99/36.09 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(x1241,x1241))),
% 35.99/36.09 inference(scs_inference,[],[41,74,104,111,114,99,8,12,2,21,20,6,7])).
% 35.99/36.09 cnf(127,plain,
% 35.99/36.09 (E(f3(a4,f3(a4,f3(a4,a4))),f3(a2,x1271))),
% 35.99/36.09 inference(scs_inference,[],[41,31,91,74,104,111,114,99,8,12,2,21,20,6,7,3])).
% 35.99/36.09 cnf(132,plain,
% 35.99/36.09 (~E(a1,a4)),
% 35.99/36.09 inference(scs_inference,[],[123,4])).
% 35.99/36.09 cnf(134,plain,
% 35.99/36.09 (E(f3(a2,x1341),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[127,123,4,2])).
% 35.99/36.09 cnf(135,plain,
% 35.99/36.09 (P1(f3(a4,f3(a4,f3(a4,a4))),x1351)),
% 35.99/36.09 inference(scs_inference,[],[127,123,124,68,4,2,21])).
% 35.99/36.09 cnf(137,plain,
% 35.99/36.09 (P1(f3(a4,f3(a4,f3(a4,a4))),f3(x1371,x1371))),
% 35.99/36.09 inference(rename_variables,[],[124])).
% 35.99/36.09 cnf(140,plain,
% 35.99/36.09 (~E(f3(a4,f3(a4,f3(a4,a4))),f3(a4,a1))),
% 35.99/36.09 inference(scs_inference,[],[79,127,70,123,124,137,68,85,4,2,21,3,6])).
% 35.99/36.09 cnf(143,plain,
% 35.99/36.09 (~E(f3(a4,f3(a4,a4)),a2)),
% 35.99/36.09 inference(scs_inference,[],[79,120,127,70,123,124,137,68,76,85,4,2,21,3,6,7])).
% 35.99/36.09 cnf(147,plain,
% 35.99/36.09 (E(f3(a4,f3(a4,f3(a4,a4))),f3(a4,f3(x1471,a4)))+~P1(f3(a4,f3(x1471,a4)),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[79,120,127,70,123,124,137,117,68,76,85,4,2,21,3,6,7,18,20])).
% 35.99/36.09 cnf(149,plain,
% 35.99/36.09 (E(a2,f3(x1491,a4))),
% 35.99/36.09 inference(scs_inference,[],[9,2])).
% 35.99/36.09 cnf(150,plain,
% 35.99/36.09 (~P1(f3(a4,a1),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[9,135,140,2,20])).
% 35.99/36.09 cnf(153,plain,
% 35.99/36.09 (P1(f3(x1531,a4),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[134,9,135,140,101,2,20,7])).
% 35.99/36.09 cnf(156,plain,
% 35.99/36.09 (~E(f3(a4,f3(a4,a4)),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[31,134,9,135,140,143,101,2,20,7,3])).
% 35.99/36.09 cnf(157,plain,
% 35.99/36.09 (~E(f3(f3(x1571,a4),f3(x1572,a4)),f3(a4,a1))),
% 35.99/36.09 inference(scs_inference,[],[31,134,9,135,140,143,73,101,2,20,7,3,6])).
% 35.99/36.09 cnf(162,plain,
% 35.99/36.09 (~E(f3(a4,a4),f3(a4,f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[31,134,9,135,140,143,73,101,2,20,7,3,6,22,24,5])).
% 35.99/36.09 cnf(164,plain,
% 35.99/36.09 (E(f3(a4,x1641),f3(a4,f3(a4,f3(a4,x1641))))),
% 35.99/36.09 inference(scs_inference,[],[162,15,5,2])).
% 35.99/36.09 cnf(165,plain,
% 35.99/36.09 (P1(f3(x1651,a4),x1652)),
% 35.99/36.09 inference(scs_inference,[],[162,153,135,15,5,2,21])).
% 35.99/36.09 cnf(167,plain,
% 35.99/36.09 (E(f3(x1671,a4),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[162,153,135,15,5,2,21,20])).
% 35.99/36.09 cnf(170,plain,
% 35.99/36.09 (P1(f3(x1701,x1701),f3(f3(x1702,f3(x1703,a4)),f3(a4,f3(x1703,a4))))),
% 35.99/36.09 inference(scs_inference,[],[78,162,153,135,114,15,5,2,21,20,7])).
% 35.99/36.09 cnf(172,plain,
% 35.99/36.09 (~E(f3(x1721,a4),f3(a4,a1))),
% 35.99/36.09 inference(scs_inference,[],[150,92,78,162,153,135,114,143,15,5,2,21,20,7,3,6])).
% 35.99/36.09 cnf(174,plain,
% 35.99/36.09 (E(f3(a4,f3(a4,f3(a4,a4))),f3(x1741,a4))),
% 35.99/36.09 inference(scs_inference,[],[167,2])).
% 35.99/36.09 cnf(178,plain,
% 35.99/36.09 (~P1(f3(a4,a1),f3(x1781,a4))),
% 35.99/36.09 inference(scs_inference,[],[167,170,165,172,16,2,21,20])).
% 35.99/36.09 cnf(183,plain,
% 35.99/36.09 (~E(a4,a2)),
% 35.99/36.09 inference(scs_inference,[],[41,164,167,87,170,165,172,16,14,2,21,20,3,7])).
% 35.99/36.09 cnf(187,plain,
% 35.99/36.09 (P1(f3(x1871,x1871),x1872)),
% 35.99/36.09 inference(scs_inference,[],[170,68,21])).
% 35.99/36.09 cnf(190,plain,
% 35.99/36.09 (~P1(f3(a4,f3(a4,a4)),f3(a4,a4))),
% 35.99/36.09 inference(scs_inference,[],[162,170,82,68,21,20])).
% 35.99/36.09 cnf(194,plain,
% 35.99/36.09 (P1(f3(f3(x1941,a4),f3(x1942,a4)),f3(f3(x1943,a4),f3(x1944,a4)))),
% 35.99/36.09 inference(scs_inference,[],[31,103,183,162,170,82,68,55,21,20,3,7])).
% 35.99/36.09 cnf(200,plain,
% 35.99/36.09 (P1(f3(f3(x2001,a4),f3(x2002,a4)),f3(x2003,a4))),
% 35.99/36.09 inference(scs_inference,[],[70,149,187,157,183,55,20,3,7])).
% 35.99/36.09 cnf(201,plain,
% 35.99/36.09 (~P1(f3(a4,f3(f3(x2011,a4),f3(x2011,a4))),a1)),
% 35.99/36.09 inference(scs_inference,[],[70,149,187,157,183,55,20,3,7,24])).
% 35.99/36.09 cnf(203,plain,
% 35.99/36.09 (~E(f3(f3(x2031,a4),f3(x2032,a4)),f3(a4,f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[190,70,149,187,157,183,55,20,3,7,24,6])).
% 35.99/36.09 cnf(204,plain,
% 35.99/36.09 (~E(f3(x2041,a4),a4)),
% 35.99/36.09 inference(scs_inference,[],[190,70,149,187,157,183,55,20,3,7,24,6,4])).
% 35.99/36.09 cnf(205,plain,
% 35.99/36.09 (P1(f3(f3(x2051,a4),f3(x2052,a4)),x2053)),
% 35.99/36.09 inference(scs_inference,[],[194,187,21])).
% 35.99/36.09 cnf(206,plain,
% 35.99/36.09 (P1(f3(x2061,x2061),x2062)),
% 35.99/36.09 inference(rename_variables,[],[187])).
% 35.99/36.09 cnf(209,plain,
% 35.99/36.09 (E(f3(f3(x2091,a4),f3(x2092,a4)),f3(a4,a4))),
% 35.99/36.09 inference(scs_inference,[],[194,200,187,206,21,20])).
% 35.99/36.09 cnf(213,plain,
% 35.99/36.09 (~E(f3(a4,a1),f3(a2,x2131))),
% 35.99/36.09 inference(scs_inference,[],[134,87,194,200,187,206,21,20,3])).
% 35.99/36.09 cnf(215,plain,
% 35.99/36.09 (~P1(f3(a4,f3(a4,a4)),f3(f3(x2151,a4),f3(x2152,a4)))),
% 35.99/36.09 inference(scs_inference,[],[205,203,20])).
% 35.99/36.09 cnf(226,plain,
% 35.99/36.09 (~P1(f3(a4,f3(f3(x2261,a4),f3(x2262,a4))),f3(a4,a4))),
% 35.99/36.09 inference(scs_inference,[],[215,24])).
% 35.99/36.09 cnf(239,plain,
% 35.99/36.09 (~P1(f3(a4,f3(a4,a4)),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[156,2,147])).
% 35.99/36.09 cnf(240,plain,
% 35.99/36.09 (E(f3(a2,x2401),f3(f3(a2,x2402),x2401))),
% 35.99/36.09 inference(scs_inference,[],[10,2,4])).
% 35.99/36.09 cnf(241,plain,
% 35.99/36.09 (E(f3(f3(a2,x2411),x2412),f3(a2,x2412))),
% 35.99/36.09 inference(scs_inference,[],[240,2])).
% 35.99/36.09 cnf(245,plain,
% 35.99/36.09 (~E(f3(a4,a1),f3(f3(a2,x2451),x2452))),
% 35.99/36.09 inference(scs_inference,[],[241,213,3])).
% 35.99/36.09 cnf(248,plain,
% 35.99/36.09 (E(f3(x2481,a2),f3(x2481,f3(a2,x2482)))),
% 35.99/36.09 inference(scs_inference,[],[10,2,5])).
% 35.99/36.09 cnf(249,plain,
% 35.99/36.09 (E(f3(x2491,f3(a2,x2492)),f3(x2491,a2))),
% 35.99/36.09 inference(scs_inference,[],[248,2])).
% 35.99/36.09 cnf(251,plain,
% 35.99/36.09 (~E(f3(a2,x2511),a4)),
% 35.99/36.09 inference(scs_inference,[],[245,2,4])).
% 35.99/36.09 cnf(254,plain,
% 35.99/36.09 (E(f3(a1,f3(a2,x2541)),a1)),
% 35.99/36.09 inference(scs_inference,[],[248,2,64])).
% 35.99/36.09 cnf(255,plain,
% 35.99/36.09 (E(a1,f3(a1,f3(a2,x2551)))),
% 35.99/36.09 inference(scs_inference,[],[254,2])).
% 35.99/36.09 cnf(269,plain,
% 35.99/36.09 (E(f3(f3(x2691,x2691),x2692),f3(a2,x2692))),
% 35.99/36.09 inference(scs_inference,[],[26,18,4])).
% 35.99/36.09 cnf(270,plain,
% 35.99/36.09 (E(f3(a2,x2701),f3(f3(x2702,x2702),x2701))),
% 35.99/36.09 inference(scs_inference,[],[269,2])).
% 35.99/36.09 cnf(275,plain,
% 35.99/36.09 (E(f3(x2751,f3(x2752,a4)),f3(x2751,a2))),
% 35.99/36.09 inference(scs_inference,[],[11,18,5])).
% 35.99/36.09 cnf(276,plain,
% 35.99/36.09 (E(f3(x2761,a2),f3(x2761,f3(x2762,a4)))),
% 35.99/36.09 inference(scs_inference,[],[275,2])).
% 35.99/36.09 cnf(277,plain,
% 35.99/36.09 (P1(x2771,f3(a4,f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[11,275,39,2,21])).
% 35.99/36.09 cnf(280,plain,
% 35.99/36.09 (E(f3(f3(x2801,a4),x2802),a2)),
% 35.99/36.09 inference(scs_inference,[],[11,18,24])).
% 35.99/36.09 cnf(281,plain,
% 35.99/36.09 (E(a2,f3(f3(x2811,a4),x2812))),
% 35.99/36.09 inference(scs_inference,[],[280,2])).
% 35.99/36.09 cnf(283,plain,
% 35.99/36.09 (E(f3(f3(x2831,a4),x2832),f3(a2,x2832))),
% 35.99/36.09 inference(scs_inference,[],[11,18,4])).
% 35.99/36.09 cnf(284,plain,
% 35.99/36.09 (E(f3(a2,x2841),f3(f3(x2842,a4),x2841))),
% 35.99/36.09 inference(scs_inference,[],[283,2])).
% 35.99/36.09 cnf(286,plain,
% 35.99/36.09 (E(f3(f3(x2861,x2862),f3(a4,x2862)),a2)),
% 35.99/36.09 inference(scs_inference,[],[11,18,23])).
% 35.99/36.09 cnf(287,plain,
% 35.99/36.09 (P1(f3(x2871,x2872),f3(a4,x2872))),
% 35.99/36.09 inference(scs_inference,[],[286,19])).
% 35.99/36.09 cnf(289,plain,
% 35.99/36.09 (E(a2,f3(f3(x2891,x2892),f3(a4,x2892)))),
% 35.99/36.09 inference(scs_inference,[],[286,19,2])).
% 35.99/36.09 cnf(297,plain,
% 35.99/36.09 (E(f3(x2971,a4),f3(f3(x2972,x2973),f3(a4,x2973)))),
% 35.99/36.09 inference(scs_inference,[],[11,289,18,3])).
% 35.99/36.09 cnf(298,plain,
% 35.99/36.09 (E(f3(f3(x2981,x2982),f3(a4,x2982)),f3(x2983,a4))),
% 35.99/36.09 inference(scs_inference,[],[297,2])).
% 35.99/36.09 cnf(299,plain,
% 35.99/36.09 (P1(f3(x2991,f3(a4,f3(a4,a4))),x2992)),
% 35.99/36.09 inference(scs_inference,[],[297,287,135,2,21])).
% 35.99/36.09 cnf(300,plain,
% 35.99/36.09 (P1(f3(x3001,x3002),f3(a4,x3002))),
% 35.99/36.09 inference(rename_variables,[],[287])).
% 35.99/36.09 cnf(305,plain,
% 35.99/36.09 (~E(f3(x3051,f3(a4,f3(a4,a4))),f3(a4,f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[239,297,287,300,251,135,2,21,20,6])).
% 35.99/36.09 cnf(308,plain,
% 35.99/36.09 (~E(f3(x3081,f3(a4,f3(a4,a4))),a4)),
% 35.99/36.09 inference(scs_inference,[],[85,299,18,6])).
% 35.99/36.09 cnf(309,plain,
% 35.99/36.09 (~P1(f3(a4,f3(a4,a4)),f3(x3091,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[277,305,20])).
% 35.99/36.09 cnf(312,plain,
% 35.99/36.09 (~E(f3(x3121,f3(a4,f3(a4,a4))),f3(a4,a1))),
% 35.99/36.09 inference(scs_inference,[],[41,277,305,299,20,6])).
% 35.99/36.09 cnf(317,plain,
% 35.99/36.09 (E(f3(x3171,a4),f3(f3(x3172,a4),x3173))),
% 35.99/36.09 inference(scs_inference,[],[11,281,18,3])).
% 35.99/36.09 cnf(318,plain,
% 35.99/36.09 (E(f3(f3(x3181,a4),x3182),f3(x3183,a4))),
% 35.99/36.09 inference(scs_inference,[],[317,2])).
% 35.99/36.09 cnf(319,plain,
% 35.99/36.09 (~P1(f3(a4,a1),f3(x3191,f3(a4,f3(a4,a4))))),
% 35.99/36.09 inference(scs_inference,[],[317,312,299,2,20])).
% 35.99/36.09 cnf(322,plain,
% 35.99/36.09 (E(f3(a2,f3(x3221,a4)),f3(a4,a4))),
% 35.99/36.09 inference(scs_inference,[],[209,270,317,312,299,2,20,3])).
% 35.99/36.09 cnf(325,plain,
% 35.99/36.09 (E(f3(a4,a4),f3(a2,f3(x3251,a4)))),
% 35.99/36.09 inference(scs_inference,[],[322,2])).
% 35.99/36.09 cnf(330,plain,
% 35.99/36.09 (P1(f3(f3(x3301,x3302),f3(a4,x3302)),f3(x3303,a4))),
% 35.99/36.09 inference(scs_inference,[],[318,322,308,187,16,2,20,7])).
% 35.99/36.09 cnf(332,plain,
% 35.99/36.09 (~E(f3(f3(x3321,x3322),f3(a4,x3322)),f3(a4,a1))),
% 35.99/36.09 inference(scs_inference,[],[178,318,322,308,187,16,2,20,7,6])).
% 35.99/36.09 cnf(333,plain,
% 35.99/36.09 (E(a1,f3(a1,f3(x3331,a4)))),
% 35.99/36.09 inference(scs_inference,[],[178,116,318,322,276,308,187,16,2,20,7,6,3])).
% 35.99/36.09 cnf(335,plain,
% 35.99/36.09 (P1(f3(a4,x3351),f3(f3(a4,f3(a4,a4)),x3351))),
% 35.99/36.09 inference(scs_inference,[],[31,19,23])).
% 35.99/36.09 cnf(336,plain,
% 35.99/36.09 (E(f3(a1,f3(x3361,a4)),a1)),
% 35.99/36.09 inference(scs_inference,[],[333,2])).
% 35.99/36.09 cnf(337,plain,
% 35.99/36.09 (P1(f3(a4,f3(x3371,f3(a4,a4))),f3(f3(a4,x3371),f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[333,335,16,2,21])).
% 35.99/36.09 cnf(339,plain,
% 35.99/36.09 (P1(f3(a4,x3391),f3(f3(a4,f3(a4,a4)),x3391))),
% 35.99/36.09 inference(rename_variables,[],[335])).
% 35.99/36.09 cnf(341,plain,
% 35.99/36.09 (E(f3(a4,f3(a4,a4)),f3(f3(a4,f3(a4,a4)),f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[333,335,339,277,16,2,21,20])).
% 35.99/36.09 cnf(342,plain,
% 35.99/36.09 (P1(f3(a4,x3421),f3(f3(a4,f3(a4,a4)),x3421))),
% 35.99/36.09 inference(rename_variables,[],[335])).
% 35.99/36.09 cnf(347,plain,
% 35.99/36.09 (~E(f3(f3(x3471,x3472),f3(a4,x3472)),f3(a4,f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[41,190,333,335,339,342,330,277,16,2,21,20,7,6])).
% 35.99/36.09 cnf(349,plain,
% 35.99/36.09 (E(f3(a1,f3(a2,x3491)),f3(a1,f3(a2,x3492)))),
% 35.99/36.09 inference(scs_inference,[],[41,190,255,333,254,335,339,342,330,277,16,2,21,20,7,6,3])).
% 35.99/36.09 cnf(351,plain,
% 35.99/36.09 (E(f3(f3(a4,f3(a4,a4)),f3(a4,a4)),f3(a4,f3(a4,a4)))),
% 35.99/36.09 inference(scs_inference,[],[341,2])).
% 35.99/36.09 cnf(352,plain,
% 35.99/36.10 (P1(f3(x3521,f3(x3522,f3(a4,a4))),f3(f3(a4,x3522),f3(a4,a4)))),
% 35.99/36.10 inference(scs_inference,[],[341,337,287,2,21])).
% 35.99/36.10 cnf(353,plain,
% 35.99/36.10 (P1(f3(x3531,x3532),f3(a4,x3532))),
% 35.99/36.10 inference(rename_variables,[],[287])).
% 35.99/36.10 cnf(355,plain,
% 35.99/36.10 (E(f3(a4,x3551),f3(f3(a4,f3(a4,a4)),x3551))),
% 35.99/36.10 inference(scs_inference,[],[341,337,287,353,335,2,21,20])).
% 35.99/36.10 cnf(359,plain,
% 35.99/36.10 (~E(f3(f3(a4,f3(x3591,a4)),f3(a4,a4)),f3(a4,a4))),
% 35.99/36.10 inference(scs_inference,[],[341,226,337,287,353,335,2,21,20,7])).
% 35.99/36.10 cnf(362,plain,
% 35.99/36.10 (E(a4,f3(f3(a4,f3(a4,a4)),f3(a4,a4)))),
% 35.99/36.10 inference(scs_inference,[],[341,52,226,337,287,353,335,2,21,20,7,3])).
% 35.99/36.10 cnf(363,plain,
% 35.99/36.10 (P1(f3(x3631,f3(x3631,x3632)),x3632)),
% 35.99/36.10 inference(scs_inference,[],[13,19,24])).
% 35.99/36.10 cnf(364,plain,
% 35.99/36.10 (E(f3(f3(a4,f3(a4,a4)),x3641),f3(a4,x3641))),
% 35.99/36.10 inference(scs_inference,[],[355,2])).
% 35.99/36.10 cnf(365,plain,
% 35.99/36.10 (P1(f3(x3651,f3(x3651,f3(x3652,a4))),x3653)),
% 35.99/36.10 inference(scs_inference,[],[355,363,165,2,21])).
% 35.99/36.10 cnf(366,plain,
% 35.99/36.10 (P1(f3(x3661,f3(x3661,x3662)),x3662)),
% 35.99/36.10 inference(rename_variables,[],[363])).
% 35.99/36.10 cnf(369,plain,
% 35.99/36.10 (P1(f3(x3691,f3(x3691,x3692)),x3692)),
% 35.99/36.10 inference(rename_variables,[],[363])).
% 35.99/36.10 cnf(377,plain,
% 35.99/36.10 (E(f3(f3(a4,f3(a4,a4)),f3(a4,a4)),a4)),
% 35.99/36.10 inference(scs_inference,[],[41,351,355,67,363,366,369,352,201,58,165,2,21,20,6,7,3])).
% 35.99/36.10 cnf(379,plain,
% 35.99/36.10 (~E(f3(a4,a2),a1)),
% 35.99/36.10 inference(scs_inference,[],[41,351,355,67,363,366,369,352,201,58,165,2,21,20,6,7,3,64,5])).
% 35.99/36.10 cnf(386,plain,
% 35.99/36.10 (~E(f3(x3861,f3(x3861,f3(x3862,a4))),f3(a4,a1))),
% 35.99/36.10 inference(scs_inference,[],[41,365,379,363,251,64,20,6])).
% 35.99/36.10 cnf(389,plain,
% 35.99/36.10 (~E(f3(a4,f3(x3891,a4)),a1)),
% 35.99/36.10 inference(scs_inference,[],[41,377,132,365,379,363,251,64,20,6,3,5])).
% 35.99/36.10 cnf(392,plain,
% 35.99/36.10 (~P1(f3(a4,a1),f3(x3921,f3(x3921,f3(x3922,a4))))),
% 35.99/36.10 inference(scs_inference,[],[386,389,365,64,20])).
% 35.99/36.10 cnf(397,plain,
% 35.99/36.10 (P1(f3(f3(x3971,x3972),f3(a4,x3972)),x3973)),
% 35.99/36.10 inference(scs_inference,[],[330,165,21])).
% 35.99/36.10 cnf(404,plain,
% 35.99/36.10 (~E(f3(x4041,a4),f3(f3(a4,f3(a4,a4)),f3(a4,a4)))),
% 35.99/36.10 inference(scs_inference,[],[377,204,352,330,205,165,21,20,3])).
% 35.99/36.10 cnf(405,plain,
% 35.99/36.10 (E(f3(f3(a4,a4),f3(a4,a4)),f3(x4051,f3(a4,f3(a4,a4))))),
% 35.99/36.10 inference(scs_inference,[],[377,204,352,330,205,165,21,20,3,2])).
% 35.99/36.10 cnf(406,plain,
% 35.99/36.10 (~P1(f3(a4,a1),f3(f3(x4061,x4062),f3(a4,x4062)))),
% 35.99/36.10 inference(scs_inference,[],[332,397,20])).
% 35.99/36.10 cnf(424,plain,
% 35.99/36.10 (~P1(f3(a4,f3(a4,a4)),f3(f3(x4241,x4242),f3(a4,x4242)))),
% 35.99/36.10 inference(scs_inference,[],[347,397,20])).
% 35.99/36.10 cnf(433,plain,
% 35.99/36.10 (P1(f3(x4331,f3(x4331,f3(x4332,x4333))),x4332)),
% 35.99/36.10 inference(scs_inference,[],[363,14,21])).
% 35.99/36.10 cnf(440,plain,
% 35.99/36.10 (~E(f3(x4401,f3(x4401,f3(a2,x4402))),f3(a4,a1))),
% 35.99/36.10 inference(scs_inference,[],[41,404,363,14,187,21,20,6])).
% 35.99/36.10 cnf(441,plain,
% 35.99/36.10 (P1(f3(a2,x4411),f3(a4,f3(a4,f3(a4,a4))))),
% 35.99/36.10 inference(scs_inference,[],[41,38,404,363,14,187,21,20,6,7])).
% 35.99/36.10 cnf(443,plain,
% 35.99/36.10 (~E(f3(f3(a4,f3(x4431,a4)),f3(a4,a4)),f3(f3(x4432,x4433),f3(a4,x4433)))),
% 35.99/36.10 inference(scs_inference,[],[41,38,298,359,404,363,14,187,21,20,6,7,3])).
% 35.99/36.10 cnf(449,plain,
% 35.99/36.10 (~E(f3(a4,a4),f3(a4,f3(x4491,a4)))),
% 35.99/36.10 inference(scs_inference,[],[443,5])).
% 35.99/36.10 cnf(451,plain,
% 35.99/36.10 (P1(f3(x4511,f3(x4511,f3(a2,x4512))),x4513)),
% 35.99/36.10 inference(scs_inference,[],[433,443,12,5,21])).
% 35.99/36.10 cnf(454,plain,
% 35.99/36.10 (~P1(f3(a4,a1),f3(x4541,f3(x4541,f3(a2,x4542))))),
% 35.99/36.10 inference(scs_inference,[],[433,440,443,12,5,21,20])).
% 35.99/36.10 cnf(471,plain,
% 35.99/36.10 (E(f3(f3(a1,f3(x4711,a4)),a2),a1)),
% 35.99/36.10 inference(scs_inference,[],[336,4,64])).
% 35.99/36.10 cnf(472,plain,
% 35.99/36.10 (E(a1,f3(f3(a1,f3(x4721,a4)),a2))),
% 35.99/36.10 inference(scs_inference,[],[471,2])).
% 35.99/36.10 cnf(479,plain,
% 35.99/36.10 (E(f3(f3(a1,f3(a2,x4791)),a2),a1)),
% 35.99/36.10 inference(scs_inference,[],[254,4,64])).
% 35.99/36.10 cnf(481,plain,
% 35.99/36.10 (~P1(f3(a4,f3(x4811,a4)),f3(a4,a4))),
% 35.99/36.10 inference(scs_inference,[],[479,449,165,2,20])).
% 35.99/36.10 cnf(488,plain,
% 35.99/36.10 (E(f3(a2,f3(a4,a4)),f3(x4881,f3(a4,f3(a4,a4))))),
% 35.99/36.10 inference(scs_inference,[],[405,270,3])).
% 35.99/36.10 cnf(490,plain,
% 35.99/36.10 (E(f3(x4901,f3(a4,f3(a4,a4))),f3(a2,f3(a4,a4)))),
% 35.99/36.10 inference(scs_inference,[],[405,270,3,2])).
% 35.99/36.10 cnf(507,plain,
% 35.99/36.10 (E(f3(a2,f3(a4,a4)),f3(x5071,a4))),
% 35.99/36.10 inference(scs_inference,[],[488,174,3])).
% 35.99/36.10 cnf(511,plain,
% 35.99/36.10 (E(f3(x5111,f3(a4,f3(a4,a4))),f3(x5112,a4))),
% 35.99/36.10 inference(scs_inference,[],[490,507,3])).
% 35.99/36.10 cnf(512,plain,
% 35.99/36.10 (E(f3(x5121,a4),f3(x5122,f3(a4,f3(a4,a4))))),
% 35.99/36.10 inference(scs_inference,[],[490,507,3,2])).
% 35.99/36.10 cnf(514,plain,
% 35.99/36.10 (E(f3(x5141,a4),f3(x5142,a4))),
% 35.99/36.10 inference(scs_inference,[],[511,512,3])).
% 35.99/36.10 cnf(517,plain,
% 35.99/36.10 (E(f3(a1,f3(x5171,a4)),f3(f3(a1,f3(x5172,a4)),a2))),
% 35.99/36.10 inference(scs_inference,[],[472,336,3])).
% 35.99/36.10 cnf(518,plain,
% 35.99/36.10 (E(f3(f3(a1,f3(x5181,a4)),a2),f3(a1,f3(x5182,a4)))),
% 35.99/36.10 inference(scs_inference,[],[472,336,3,2])).
% 35.99/36.10 cnf(520,plain,
% 35.99/36.10 (E(f3(a1,f3(a2,x5201)),f3(f3(a1,f3(x5202,a4)),a2))),
% 35.99/36.10 inference(scs_inference,[],[349,517,3])).
% 35.99/36.10 cnf(523,plain,
% 35.99/36.10 (E(f3(f3(a1,f3(x5231,a4)),a2),f3(a1,f3(a2,x5232)))),
% 35.99/36.10 inference(scs_inference,[],[349,517,3,2])).
% 35.99/36.10 cnf(525,plain,
% 35.99/36.10 (E(f3(f3(a1,f3(x5251,a4)),a2),f3(a1,a2))),
% 35.99/36.10 inference(scs_inference,[],[116,471,3])).
% 35.99/36.10 cnf(528,plain,
% 35.99/36.10 (E(f3(x5281,a4),f3(a2,f3(x5282,a4)))),
% 35.99/36.10 inference(scs_inference,[],[514,325,3])).
% 35.99/36.10 cnf(530,plain,
% 35.99/36.10 (E(f3(a2,f3(x5301,a4)),f3(x5302,a4))),
% 35.99/36.10 inference(scs_inference,[],[514,325,3,2])).
% 35.99/36.10 cnf(532,plain,
% 35.99/36.10 (E(f3(a2,f3(x5321,a4)),f3(x5322,f3(a4,f3(a4,a4))))),
% 35.99/36.10 inference(scs_inference,[],[530,512,3])).
% 35.99/36.10 cnf(534,plain,
% 35.99/36.10 (E(f3(x5341,f3(a4,f3(a4,a4))),f3(a2,f3(x5342,a4)))),
% 35.99/36.10 inference(scs_inference,[],[530,512,3,2])).
% 35.99/36.10 cnf(536,plain,
% 35.99/36.10 (E(f3(x5361,f3(a4,f3(a4,a4))),f3(f3(x5362,a4),f3(x5363,a4)))),
% 35.99/36.10 inference(scs_inference,[],[534,284,3])).
% 35.99/36.10 cnf(538,plain,
% 35.99/36.10 (E(f3(f3(x5381,a4),f3(x5382,a4)),f3(x5383,f3(a4,f3(a4,a4))))),
% 35.99/36.10 inference(scs_inference,[],[534,284,3,2])).
% 35.99/36.10 cnf(540,plain,
% 35.99/36.10 (E(f3(f3(x5401,a4),f3(x5402,a4)),f3(f3(x5403,a4),f3(x5404,a4)))),
% 35.99/36.10 inference(scs_inference,[],[536,538,3])).
% 35.99/36.10 cnf(545,plain,
% 35.99/36.10 (P1(f3(x5451,f3(a4,x5452)),f3(x5451,f3(x5453,x5452)))),
% 35.99/36.10 inference(scs_inference,[],[11,22,23])).
% 35.99/36.10 cnf(546,plain,
% 35.99/36.10 (P1(f3(x5461,f3(a4,f3(a2,x5462))),x5463)),
% 35.99/36.10 inference(scs_inference,[],[545,451,21])).
% 35.99/36.10 cnf(550,plain,
% 35.99/36.10 (~E(f3(x5501,f3(a4,f3(a2,x5502))),f3(a4,a1))),
% 35.99/36.10 inference(scs_inference,[],[41,545,451,21,6])).
% 35.99/36.10 cnf(551,plain,
% 35.99/36.10 (E(f3(f3(x5511,a4),f3(x5512,a4)),f3(a2,x5513))),
% 35.99/36.10 inference(scs_inference,[],[41,538,127,545,451,21,6,3])).
% 35.99/36.10 cnf(553,plain,
% 35.99/36.10 (E(f3(a2,x5531),f3(f3(x5532,a4),f3(x5533,a4)))),
% 35.99/36.10 inference(scs_inference,[],[41,538,127,545,451,21,6,3,2])).
% 35.99/36.10 cnf(554,plain,
% 35.99/36.10 (E(f3(x5541,f3(a4,f3(a2,x5542))),a2)),
% 35.99/36.10 inference(scs_inference,[],[41,538,127,545,451,12,21,6,3,2,20])).
% 35.99/36.10 cnf(557,plain,
% 35.99/36.10 (P1(x5571,f3(a4,f3(a2,x5572)))),
% 35.99/36.10 inference(scs_inference,[],[41,538,127,545,451,12,21,6,3,2,20,19])).
% 35.99/36.10 cnf(559,plain,
% 35.99/36.10 (P1(x5591,f3(f3(a4,f3(a4,a4)),f3(a2,x5592)))),
% 35.99/36.10 inference(scs_inference,[],[41,538,127,355,545,451,12,21,6,3,2,20,19,7])).
% 35.99/36.10 cnf(561,plain,
% 35.99/36.10 (P1(f3(f3(x5611,a4),x5612),f3(f3(x5611,x5613),x5612))),
% 35.99/36.10 inference(scs_inference,[],[11,22,23])).
% 35.99/36.10 cnf(562,plain,
% 35.99/36.10 (E(a2,f3(x5621,f3(a4,f3(a2,x5622))))),
% 35.99/36.10 inference(scs_inference,[],[554,2])).
% 35.99/36.10 cnf(563,plain,
% 35.99/36.10 (P1(f3(f3(x5631,a4),f3(f3(x5631,x5632),f3(x5633,x5634))),x5633)),
% 35.99/36.10 inference(scs_inference,[],[554,561,433,2,21])).
% 35.99/36.10 cnf(567,plain,
% 35.99/36.10 (E(a4,f3(f3(a4,f3(a4,a4)),f3(a2,x5671)))),
% 35.99/36.10 inference(scs_inference,[],[11,554,561,559,433,2,21,20])).
% 35.99/36.10 cnf(571,plain,
% 35.99/36.10 (P1(x5711,f3(a4,a2))),
% 35.99/36.10 inference(scs_inference,[],[11,554,249,561,559,557,433,2,21,20,7])).
% 35.99/36.10 cnf(574,plain,
% 35.99/36.10 (E(f3(a1,f3(a2,x5741)),f3(a1,f3(x5742,a4)))),
% 35.99/36.10 inference(scs_inference,[],[11,520,554,518,249,561,559,557,433,2,21,20,7,3])).
% 35.99/36.10 cnf(576,plain,
% 35.99/36.10 (~E(f3(f3(x5761,a4),f3(f3(x5761,x5762),f3(a1,x5763))),f3(a4,f3(a4,a4)))),
% 35.99/36.10 inference(scs_inference,[],[319,563,22,6])).
% 35.99/36.10 cnf(577,plain,
% 35.99/36.10 (E(f3(a1,f3(x5771,a4)),f3(a1,f3(a2,x5772)))),
% 35.99/36.10 inference(scs_inference,[],[574,2])).
% 35.99/36.10 cnf(578,plain,
% 35.99/36.10 (P1(x5781,f3(f3(a4,f3(a4,a4)),a2))),
% 35.99/36.10 inference(scs_inference,[],[574,571,335,2,21])).
% 35.99/36.10 cnf(581,plain,
% 35.99/36.10 (~P1(f3(a4,a1),f3(x5811,f3(a4,f3(a2,x5812))))),
% 35.99/36.10 inference(scs_inference,[],[574,571,550,546,335,2,21,20])).
% 35.99/36.10 cnf(586,plain,
% 35.99/36.10 (P1(x5861,f3(a4,f3(x5862,a4)))),
% 35.99/36.10 inference(scs_inference,[],[392,574,276,571,550,546,545,335,2,21,20,6,7])).
% 36.12/36.10 cnf(588,plain,
% 36.12/36.10 (E(f3(f3(a4,f3(a4,a4)),f3(a4,a4)),f3(f3(a4,f3(a4,a4)),f3(a2,x5881)))),
% 36.12/36.10 inference(scs_inference,[],[392,574,567,377,276,571,550,546,545,335,2,21,20,6,7,3])).
% 36.12/36.10 cnf(590,plain,
% 36.12/36.10 (E(f3(f3(a4,f3(a4,a4)),f3(a2,x5901)),f3(f3(a4,f3(a4,a4)),f3(a4,a4)))),
% 36.12/36.10 inference(scs_inference,[],[588,2])).
% 36.12/36.10 cnf(591,plain,
% 36.12/36.10 (P1(f3(f3(x5911,a4),f3(f3(x5911,x5912),f3(x5913,a4))),x5914)),
% 36.12/36.10 inference(scs_inference,[],[588,561,365,2,21])).
% 36.12/36.10 cnf(593,plain,
% 36.12/36.10 (P1(f3(f3(x5931,a4),x5932),f3(f3(x5931,x5933),x5932))),
% 36.12/36.10 inference(rename_variables,[],[561])).
% 36.12/36.10 cnf(595,plain,
% 36.12/36.10 (E(a4,f3(f3(a4,f3(a4,a4)),a2))),
% 36.12/36.10 inference(scs_inference,[],[11,588,578,561,365,2,21,20])).
% 36.12/36.10 cnf(601,plain,
% 36.12/36.10 (P1(x6011,f3(a4,f3(a4,f3(a4,a2))))),
% 36.12/36.10 inference(scs_inference,[],[11,406,588,164,578,561,593,571,365,2,21,20,6,7])).
% 36.12/36.10 cnf(603,plain,
% 36.12/36.10 (E(f3(a4,f3(a4,f3(a4,a4))),f3(f3(x6031,x6032),f3(a4,x6032)))),
% 36.12/36.10 inference(scs_inference,[],[11,406,31,588,289,164,578,561,593,571,365,2,21,20,6,7,3])).
% 36.12/36.10 cnf(605,plain,
% 36.12/36.10 (E(f3(f3(x6051,x6052),f3(a4,x6052)),f3(a4,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[603,2])).
% 36.12/36.10 cnf(607,plain,
% 36.12/36.10 (P1(f3(f3(x6071,a4),f3(f3(x6071,x6072),f3(x6073,x6074))),x6073)),
% 36.12/36.10 inference(rename_variables,[],[563])).
% 36.12/36.10 cnf(609,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a4,a4)),f3(f3(x6091,a4),f3(f3(x6091,x6092),f3(a1,x6093))))),
% 36.12/36.10 inference(scs_inference,[],[41,603,576,586,563,2,21,20])).
% 36.12/36.10 cnf(614,plain,
% 36.12/36.10 (P1(x6141,f3(f3(a4,f3(a4,a4)),f3(a4,f3(a4,a2))))),
% 36.12/36.10 inference(scs_inference,[],[41,603,355,576,586,601,563,607,2,21,20,6,7])).
% 36.12/36.10 cnf(616,plain,
% 36.12/36.10 (E(f3(a2,f3(x6161,a4)),f3(f3(x6162,x6163),f3(a4,x6163)))),
% 36.12/36.10 inference(scs_inference,[],[41,603,532,355,576,586,601,563,607,2,21,20,6,7,3])).
% 36.12/36.10 cnf(623,plain,
% 36.12/36.10 (E(a4,f3(f3(a4,f3(a4,a4)),f3(a4,f3(a4,a2))))),
% 36.12/36.10 inference(scs_inference,[],[11,309,616,614,441,2,21,20])).
% 36.12/36.10 cnf(627,plain,
% 36.12/36.10 (~E(f3(f3(x6271,a4),f3(a4,x6272)),f3(a4,f3(a4,a4)))),
% 36.12/36.10 inference(scs_inference,[],[11,424,309,616,614,441,561,2,21,20,6])).
% 36.12/36.10 cnf(629,plain,
% 36.12/36.10 (E(f3(f3(x6291,a4),f3(x6292,a4)),f3(f3(x6293,x6294),f3(a4,x6294)))),
% 36.12/36.10 inference(scs_inference,[],[11,424,309,551,616,614,441,561,2,21,20,6,3])).
% 36.12/36.10 cnf(636,plain,
% 36.12/36.10 (E(f3(f3(x6361,x6362),f3(a4,x6362)),f3(f3(x6363,a4),f3(x6364,a4)))),
% 36.12/36.10 inference(scs_inference,[],[629,2])).
% 36.12/36.10 cnf(645,plain,
% 36.12/36.10 (E(f3(a4,f3(a4,a4)),f3(f3(a4,f3(a4,a4)),a2))),
% 36.12/36.10 inference(scs_inference,[],[41,609,629,595,67,627,586,545,591,2,21,20,6,3])).
% 36.12/36.10 cnf(654,plain,
% 36.12/36.10 (~P1(f3(a4,a1),f3(x6541,f3(x6541,f3(x6542,a4))))),
% 36.12/36.10 inference(rename_variables,[],[392])).
% 36.12/36.10 cnf(656,plain,
% 36.12/36.10 (E(a4,f3(a4,f3(a4,f3(a4,a2))))),
% 36.12/36.10 inference(scs_inference,[],[11,392,645,601,287,2,21,20])).
% 36.12/36.10 cnf(660,plain,
% 36.12/36.10 (~E(f3(a4,f3(f3(a4,f3(a4,a4)),f3(x6601,a4))),f3(a4,a1))),
% 36.12/36.10 inference(scs_inference,[],[11,392,654,645,601,287,335,2,21,20,6])).
% 36.12/36.10 cnf(663,plain,
% 36.12/36.10 (E(f3(f3(a4,f3(a4,a4)),f3(a2,x6631)),f3(f3(a4,f3(a4,a4)),f3(a2,x6632)))),
% 36.12/36.10 inference(scs_inference,[],[11,392,654,590,645,588,601,287,335,2,21,20,6,3])).
% 36.12/36.10 cnf(664,plain,
% 36.12/36.10 (~E(f3(x6641,f3(x6641,f3(a2,x6642))),f3(a4,f3(a2,x6643)))),
% 36.12/36.10 inference(scs_inference,[],[454,451,22,6])).
% 36.12/36.10 cnf(670,plain,
% 36.12/36.10 (P1(f3(f3(x6701,a4),f3(a4,x6702)),f3(a4,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[41,605,623,660,363,561,5,2,21,7])).
% 36.12/36.10 cnf(672,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a2,x6721)),f3(x6722,f3(x6722,f3(a2,x6723))))),
% 36.12/36.10 inference(scs_inference,[],[41,605,623,660,664,557,363,561,5,2,21,7,20])).
% 36.12/36.10 cnf(675,plain,
% 36.12/36.10 (E(f3(f3(x6751,x6752),f3(a4,x6752)),f3(a2,x6753))),
% 36.12/36.10 inference(scs_inference,[],[41,605,636,623,551,660,664,557,363,561,5,2,21,7,20,3])).
% 36.12/36.10 cnf(685,plain,
% 36.12/36.10 (E(f3(a2,x6851),f3(f3(x6852,x6853),f3(a4,x6853)))),
% 36.12/36.10 inference(scs_inference,[],[675,664,5,2])).
% 36.12/36.10 cnf(689,plain,
% 36.12/36.10 (E(f3(f3(x6891,a4),f3(a4,x6892)),f3(a4,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[41,675,670,664,299,591,5,2,21,20])).
% 36.12/36.10 cnf(692,plain,
% 36.12/36.10 (P1(f3(f3(x6921,a4),f3(a4,x6922)),a2)),
% 36.12/36.10 inference(scs_inference,[],[41,31,675,670,664,299,591,5,2,21,20,7])).
% 36.12/36.10 cnf(693,plain,
% 36.12/36.10 (E(f3(a4,f3(a4,f3(a4,a4))),f3(f3(x6931,a4),x6932))),
% 36.12/36.10 inference(scs_inference,[],[41,31,675,281,670,664,299,591,5,2,21,20,7,3])).
% 36.12/36.10 cnf(694,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a2,x6941)),f3(f3(x6942,x6943),f3(a4,x6943)))),
% 36.12/36.10 inference(scs_inference,[],[581,397,22,21])).
% 36.12/36.10 cnf(697,plain,
% 36.12/36.10 (E(f3(f3(x6971,a4),x6972),f3(a4,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[693,694,24,2])).
% 36.12/36.10 cnf(698,plain,
% 36.12/36.10 (~P1(f3(a4,a1),f3(f3(x6981,a4),f3(a4,x6982)))),
% 36.12/36.10 inference(scs_inference,[],[41,693,694,692,24,2,21])).
% 36.12/36.10 cnf(700,plain,
% 36.12/36.10 (P1(f3(f3(x7001,a4),f3(a4,x7002)),f3(x7003,f3(a4,f3(a2,x7004))))),
% 36.12/36.10 inference(scs_inference,[],[41,693,562,694,692,24,2,21,7])).
% 36.12/36.10 cnf(701,plain,
% 36.12/36.10 (E(f3(f3(x7011,a4),f3(a4,x7012)),f3(f3(x7013,a4),x7014))),
% 36.12/36.10 inference(scs_inference,[],[41,693,689,562,694,692,24,2,21,7,3])).
% 36.12/36.10 cnf(705,plain,
% 36.12/36.10 (E(f3(a4,f3(a4,f3(a4,a2))),a4)),
% 36.12/36.10 inference(scs_inference,[],[656,698,24,2])).
% 36.12/36.10 cnf(706,plain,
% 36.12/36.10 (~P1(f3(a4,a1),f3(f3(x7061,a4),f3(x7062,a4)))),
% 36.12/36.10 inference(scs_inference,[],[41,656,698,205,24,2,21])).
% 36.12/36.10 cnf(709,plain,
% 36.12/36.10 (P1(f3(f3(x7091,a4),f3(a4,x7092)),f3(x7093,x7093))),
% 36.12/36.10 inference(scs_inference,[],[41,656,25,698,692,205,24,2,21,7])).
% 36.12/36.10 cnf(710,plain,
% 36.12/36.10 (E(f3(f3(x7101,a4),f3(a4,x7102)),f3(a2,f3(x7103,a4)))),
% 36.12/36.10 inference(scs_inference,[],[41,656,701,528,25,698,692,205,24,2,21,7,3])).
% 36.12/36.10 cnf(718,plain,
% 36.12/36.10 (P1(f3(x7181,x7182),f3(a4,x7182))),
% 36.12/36.10 inference(rename_variables,[],[287])).
% 36.12/36.10 cnf(722,plain,
% 36.12/36.10 (P1(f3(f3(x7221,a4),x7222),f3(a4,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[481,697,710,706,287,718,561,24,2,21,6,7])).
% 36.12/36.10 cnf(724,plain,
% 36.12/36.10 (E(f3(f3(x7241,a4),f3(a4,x7242)),f3(f3(x7243,x7244),f3(a4,x7244)))),
% 36.12/36.10 inference(scs_inference,[],[481,697,685,710,706,287,718,561,24,2,21,6,7,3])).
% 36.12/36.10 cnf(726,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a2,x7261)),f3(f3(x7262,a4),f3(a4,x7263)))),
% 36.12/36.10 inference(scs_inference,[],[672,700,22,21])).
% 36.12/36.10 cnf(729,plain,
% 36.12/36.10 (E(f3(f3(x7291,x7292),f3(a4,x7292)),f3(f3(x7293,a4),f3(a4,x7294)))),
% 36.12/36.10 inference(scs_inference,[],[724,726,24,2])).
% 36.12/36.10 cnf(730,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a4,a4)),f3(f3(x7301,a4),x7302))),
% 36.12/36.10 inference(scs_inference,[],[309,724,722,726,24,2,21])).
% 36.12/36.10 cnf(731,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a4,a4)),f3(x7311,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(rename_variables,[],[309])).
% 36.12/36.10 cnf(735,plain,
% 36.12/36.10 (P1(f3(f3(x7351,a4),x7352),a2)),
% 36.12/36.10 inference(scs_inference,[],[309,731,31,724,722,726,24,2,21,6,7])).
% 36.12/36.10 cnf(736,plain,
% 36.12/36.10 (E(f3(f3(x7361,a4),f3(a4,x7362)),f3(a2,x7363))),
% 36.12/36.10 inference(scs_inference,[],[309,731,31,724,675,722,726,24,2,21,6,7,3])).
% 36.12/36.10 cnf(741,plain,
% 36.12/36.10 (E(f3(a2,x7411),f3(f3(x7412,a4),f3(a4,x7413)))),
% 36.12/36.10 inference(scs_inference,[],[736,730,24,2])).
% 36.12/36.10 cnf(742,plain,
% 36.12/36.10 (~P1(f3(a4,a1),f3(f3(x7421,a4),x7422))),
% 36.12/36.10 inference(scs_inference,[],[41,736,730,735,24,2,21])).
% 36.12/36.10 cnf(745,plain,
% 36.12/36.10 (P1(f3(f3(x7451,a4),x7452),f3(x7453,f3(a4,f3(a2,x7454))))),
% 36.12/36.10 inference(scs_inference,[],[41,736,562,730,735,24,2,21,6,7])).
% 36.12/36.10 cnf(746,plain,
% 36.12/36.10 (E(f3(f3(a1,f3(a2,x7461)),a2),f3(a1,f3(a2,x7462)))),
% 36.12/36.10 inference(scs_inference,[],[41,736,562,255,479,730,735,24,2,21,6,7,3])).
% 36.12/36.10 cnf(752,plain,
% 36.12/36.10 (E(f3(a1,f3(a2,x7521)),f3(f3(a1,f3(a2,x7522)),a2))),
% 36.12/36.10 inference(scs_inference,[],[746,742,24,2])).
% 36.12/36.10 cnf(753,plain,
% 36.12/36.10 (~P1(f3(a4,a1),f3(x7531,x7531))),
% 36.12/36.10 inference(scs_inference,[],[41,746,742,187,24,2,21])).
% 36.12/36.10 cnf(756,plain,
% 36.12/36.10 (P1(f3(f3(x7561,a4),x7562),f3(f3(x7563,a4),f3(a4,x7564)))),
% 36.12/36.10 inference(scs_inference,[],[41,729,746,742,745,187,24,2,21,7])).
% 36.12/36.10 cnf(759,plain,
% 36.12/36.10 (E(f3(a4,f3(a4,f3(a4,a2))),f3(a4,f3(a4,a4)))),
% 36.12/36.10 inference(scs_inference,[],[41,729,746,705,52,742,745,187,24,2,21,7,3])).
% 36.12/36.10 cnf(763,plain,
% 36.12/36.10 (E(f3(a4,f3(a4,a4)),f3(a4,f3(a4,f3(a4,a2))))),
% 36.12/36.10 inference(scs_inference,[],[759,753,24,2])).
% 36.12/36.10 cnf(764,plain,
% 36.12/36.10 (P1(f3(f3(x7641,a4),x7642),f3(f3(x7643,a4),f3(x7644,a4)))),
% 36.12/36.10 inference(scs_inference,[],[759,540,753,756,24,2,7])).
% 36.12/36.10 cnf(767,plain,
% 36.12/36.10 (E(f3(a1,f3(x7671,a4)),f3(f3(a1,f3(a2,x7672)),a2))),
% 36.12/36.10 inference(scs_inference,[],[759,540,577,752,753,756,24,2,7,3])).
% 36.12/36.10 cnf(771,plain,
% 36.12/36.10 (P1(f3(f3(x7711,a4),x7712),f3(a2,x7713))),
% 36.12/36.10 inference(scs_inference,[],[767,91,735,2,7])).
% 36.12/36.10 cnf(772,plain,
% 36.12/36.10 (E(f3(a2,x7721),f3(x7722,a4))),
% 36.12/36.10 inference(scs_inference,[],[741,767,511,91,735,2,7,3])).
% 36.12/36.10 cnf(782,plain,
% 36.12/36.10 (~E(f3(f3(x7821,a4),x7822),f3(a4,f3(a2,x7823)))),
% 36.12/36.10 inference(scs_inference,[],[672,771,22,6])).
% 36.12/36.10 cnf(783,plain,
% 36.12/36.10 (E(f3(x7831,a4),f3(a2,x7832))),
% 36.12/36.10 inference(scs_inference,[],[772,2])).
% 36.12/36.10 cnf(784,plain,
% 36.12/36.10 (E(f3(f3(x7841,a4),x7842),f3(a2,f3(a2,f3(x7843,a4))))),
% 36.12/36.10 inference(scs_inference,[],[772,771,365,2,20])).
% 36.12/36.10 cnf(788,plain,
% 36.12/36.10 (P1(f3(f3(x7881,a4),x7882),f3(x7883,a4))),
% 36.12/36.10 inference(scs_inference,[],[772,149,771,365,735,2,20,7])).
% 36.12/36.10 cnf(789,plain,
% 36.12/36.10 (E(f3(a2,x7891),f3(a2,x7892))),
% 36.12/36.10 inference(scs_inference,[],[553,772,736,149,771,365,735,2,20,7,3])).
% 36.12/36.10 cnf(793,plain,
% 36.12/36.10 (E(f3(a2,f3(a2,f3(x7931,a4))),f3(f3(x7932,a4),x7933))),
% 36.12/36.10 inference(scs_inference,[],[784,2])).
% 36.12/36.10 cnf(794,plain,
% 36.12/36.10 (E(f3(f3(x7941,a4),x7942),f3(a2,f3(a2,f3(a2,x7943))))),
% 36.12/36.10 inference(scs_inference,[],[784,771,451,2,20])).
% 36.12/36.10 cnf(798,plain,
% 36.12/36.10 (E(f3(f3(x7981,a4),x7982),f3(f3(x7983,x7984),f3(a4,x7984)))),
% 36.12/36.10 inference(scs_inference,[],[784,685,771,451,2,20,3])).
% 36.12/36.10 cnf(800,plain,
% 36.12/36.10 (~P1(f3(a4,f3(x8001,a4)),f3(f3(x8002,x8003),f3(a4,x8003)))),
% 36.12/36.10 inference(scs_inference,[],[392,397,22,21])).
% 36.12/36.10 cnf(803,plain,
% 36.12/36.10 (E(f3(f3(x8031,x8032),f3(a4,x8032)),f3(f3(x8033,a4),x8034))),
% 36.12/36.10 inference(scs_inference,[],[798,800,24,2])).
% 36.12/36.10 cnf(804,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a2,x8041)),f3(f3(x8042,a4),x8043))),
% 36.12/36.10 inference(scs_inference,[],[798,800,782,557,24,2,20])).
% 36.12/36.10 cnf(807,plain,
% 36.12/36.10 (P1(f3(f3(x8071,a4),x8072),f3(f3(x8073,x8074),f3(a4,x8074)))),
% 36.12/36.10 inference(scs_inference,[],[798,764,800,782,557,24,2,20,7])).
% 36.12/36.10 cnf(810,plain,
% 36.12/36.10 (E(f3(f3(x8101,a4),x8102),f3(f3(x8103,a4),x8104))),
% 36.12/36.10 inference(scs_inference,[],[798,793,794,764,800,782,557,24,2,20,7,3])).
% 36.12/36.10 cnf(815,plain,
% 36.12/36.10 (E(f3(f3(a4,f3(a4,a4)),a2),a4)),
% 36.12/36.10 inference(scs_inference,[],[804,595,24,2])).
% 36.12/36.10 cnf(817,plain,
% 36.12/36.10 (P1(f3(x8171,f3(x8172,f3(a4,a4))),f3(f3(a4,x8172),f3(a4,a4)))),
% 36.12/36.10 inference(rename_variables,[],[352])).
% 36.12/36.10 cnf(818,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a2,x8181)),f3(f3(x8182,a4),x8183))),
% 36.12/36.10 inference(rename_variables,[],[804])).
% 36.12/36.10 cnf(825,plain,
% 36.12/36.10 (E(f3(f3(x8251,x8252),f3(a4,x8252)),f3(f3(x8253,x8254),f3(a4,x8254)))),
% 36.12/36.10 inference(scs_inference,[],[804,818,803,595,605,603,807,352,817,24,2,21,6,7,3])).
% 36.12/36.10 cnf(828,plain,
% 36.12/36.10 (E(f3(f3(x8281,a4),x8282),f3(a2,f3(a4,f3(a2,x8283))))),
% 36.12/36.10 inference(scs_inference,[],[794,546,771,2,20])).
% 36.12/36.10 cnf(832,plain,
% 36.12/36.10 (E(f3(f3(x8321,x8322),f3(a4,x8322)),f3(x8323,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[825,794,538,546,771,2,20,3])).
% 36.12/36.10 cnf(835,plain,
% 36.12/36.10 (P1(f3(x8351,f3(a4,x8352)),x8352)),
% 36.12/36.10 inference(scs_inference,[],[11,23,24])).
% 36.12/36.10 cnf(836,plain,
% 36.12/36.10 (E(f3(x8361,f3(a4,f3(a4,a4))),f3(f3(x8362,x8363),f3(a4,x8363)))),
% 36.12/36.10 inference(scs_inference,[],[832,2])).
% 36.12/36.10 cnf(838,plain,
% 36.12/36.10 (P1(f3(x8381,f3(a4,x8382)),x8382)),
% 36.12/36.10 inference(rename_variables,[],[835])).
% 36.12/36.10 cnf(845,plain,
% 36.12/36.10 (E(f3(f3(x8451,a4),x8452),f3(x8453,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[41,832,810,512,835,838,709,2,21,6,7,3])).
% 36.12/36.10 cnf(851,plain,
% 36.12/36.10 (E(f3(x8511,f3(a4,f3(a4,a4))),f3(f3(x8512,a4),x8513))),
% 36.12/36.10 inference(scs_inference,[],[845,2])).
% 36.12/36.10 cnf(855,plain,
% 36.12/36.10 (E(f3(x8551,f3(a4,f3(a4,a4))),a2)),
% 36.12/36.10 inference(scs_inference,[],[836,845,554,788,2,7,3])).
% 36.12/36.10 cnf(860,plain,
% 36.12/36.10 (P1(f3(a2,x8601),f3(f3(x8602,a4),x8603))),
% 36.12/36.10 inference(scs_inference,[],[851,828,441,2,7])).
% 36.12/36.10 cnf(862,plain,
% 36.12/36.10 (E(f3(f3(a4,f3(a4,a4)),f3(a2,x8621)),f3(a4,f3(a2,x8622)))),
% 36.12/36.10 inference(scs_inference,[],[851,663,828,364,441,2,7,3])).
% 36.12/36.10 cnf(865,plain,
% 36.12/36.10 (E(f3(a4,f3(a2,x8651)),f3(f3(a4,f3(a4,a4)),f3(a2,x8652)))),
% 36.12/36.10 inference(scs_inference,[],[862,2])).
% 36.12/36.10 cnf(866,plain,
% 36.12/36.10 (E(f3(f3(x8661,a4),x8662),f3(a2,x8663))),
% 36.12/36.10 inference(scs_inference,[],[862,860,771,2,20])).
% 36.12/36.10 cnf(869,plain,
% 36.12/36.10 (P1(f3(a2,x8691),f3(a2,x8692))),
% 36.12/36.10 inference(scs_inference,[],[862,783,860,771,2,20,7])).
% 36.12/36.10 cnf(871,plain,
% 36.12/36.10 (E(f3(x8711,a4),f3(a2,x8712))),
% 36.12/36.10 inference(rename_variables,[],[783])).
% 36.12/36.10 cnf(872,plain,
% 36.12/36.10 (E(f3(x8721,a4),f3(f3(x8722,x8722),x8723))),
% 36.12/36.10 inference(scs_inference,[],[862,783,871,270,860,771,2,20,7,3])).
% 36.12/36.10 cnf(874,plain,
% 36.12/36.10 (E(f3(f3(x8741,x8741),x8742),f3(x8743,a4))),
% 36.12/36.10 inference(scs_inference,[],[872,2])).
% 36.12/36.10 cnf(875,plain,
% 36.12/36.10 (P1(f3(a2,x8751),f3(f3(x8752,x8752),x8753))),
% 36.12/36.10 inference(scs_inference,[],[872,869,2,7])).
% 36.12/36.10 cnf(878,plain,
% 36.12/36.10 (E(f3(a4,f3(a2,x8781)),f3(f3(a4,f3(a4,a4)),f3(a4,a4)))),
% 36.12/36.10 inference(scs_inference,[],[872,865,590,869,2,7,3])).
% 36.12/36.10 cnf(880,plain,
% 36.12/36.10 (P1(f3(x8801,x8802),f3(x8801,f3(x8803,a4)))),
% 36.12/36.10 inference(scs_inference,[],[11,24,22])).
% 36.12/36.10 cnf(881,plain,
% 36.12/36.10 (E(f3(a2,x8811),f3(f3(x8812,a4),x8813))),
% 36.12/36.10 inference(scs_inference,[],[866,2])).
% 36.12/36.10 cnf(882,plain,
% 36.12/36.10 (P1(f3(a2,x8821),f3(x8822,a4))),
% 36.12/36.10 inference(scs_inference,[],[874,866,875,2,7])).
% 36.12/36.10 cnf(884,plain,
% 36.12/36.10 (E(f3(f3(x8841,x8841),x8842),f3(a2,x8843))),
% 36.12/36.10 inference(scs_inference,[],[874,866,875,2,7,3])).
% 36.12/36.10 cnf(888,plain,
% 36.12/36.10 (E(f3(a2,x8881),f3(f3(x8882,x8882),x8883))),
% 36.12/36.10 inference(scs_inference,[],[884,2])).
% 36.12/36.10 cnf(889,plain,
% 36.12/36.10 (E(f3(f3(x8891,x8891),x8892),f3(f3(x8893,a4),x8894))),
% 36.12/36.10 inference(scs_inference,[],[884,881,2,3])).
% 36.12/36.10 cnf(891,plain,
% 36.12/36.10 (P1(f3(f3(x8911,a4),x8912),f3(x8913,x8912))),
% 36.12/36.10 inference(scs_inference,[],[11,24,23])).
% 36.12/36.10 cnf(892,plain,
% 36.12/36.10 (E(f3(f3(x8921,a4),x8922),f3(f3(x8923,x8923),x8924))),
% 36.12/36.10 inference(scs_inference,[],[889,2])).
% 36.12/36.10 cnf(893,plain,
% 36.12/36.10 (P1(f3(f3(x8931,a4),x8932),f3(f3(x8933,x8933),x8934))),
% 36.12/36.10 inference(scs_inference,[],[889,888,771,2,7])).
% 36.12/36.10 cnf(895,plain,
% 36.12/36.10 (E(f3(f3(x8951,x8951),x8952),a2)),
% 36.12/36.10 inference(scs_inference,[],[889,888,855,771,2,7,3])).
% 36.12/36.10 cnf(898,plain,
% 36.12/36.10 (~E(f3(x8981,f3(a4,a1)),f3(a4,a2))),
% 36.12/36.10 inference(scs_inference,[],[41,835,24,6])).
% 36.12/36.10 cnf(899,plain,
% 36.12/36.10 (E(f3(f3(a4,f3(a4,a4)),f3(a4,a4)),f3(a4,f3(a2,x8991)))),
% 36.12/36.10 inference(scs_inference,[],[878,2])).
% 36.12/36.10 cnf(900,plain,
% 36.12/36.10 (~P1(f3(a4,a2),f3(x9001,f3(a4,a1)))),
% 36.12/36.10 inference(scs_inference,[],[878,898,571,2,20])).
% 36.12/36.10 cnf(903,plain,
% 36.12/36.10 (P1(f3(a2,x9031),f3(f3(x9032,x9033),f3(a4,x9033)))),
% 36.12/36.10 inference(scs_inference,[],[878,836,898,571,441,2,20,7])).
% 36.12/36.10 cnf(905,plain,
% 36.12/36.10 (E(f3(f3(x9051,x9051),x9052),f3(a4,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[878,895,836,38,898,571,441,2,20,7,3])).
% 36.12/36.10 cnf(909,plain,
% 36.12/36.10 (E(f3(a4,f3(a4,f3(a4,a4))),f3(f3(x9091,x9091),x9092))),
% 36.12/36.10 inference(scs_inference,[],[905,2])).
% 36.12/36.10 cnf(911,plain,
% 36.12/36.10 (P1(f3(f3(x9111,a4),x9112),f3(f3(x9113,x9113),x9114))),
% 36.12/36.10 inference(rename_variables,[],[893])).
% 36.12/36.10 cnf(912,plain,
% 36.12/36.10 (~P1(f3(a4,a2),f3(x9121,f3(a4,a1)))),
% 36.12/36.10 inference(rename_variables,[],[900])).
% 36.12/36.10 cnf(917,plain,
% 36.12/36.10 (P1(f3(f3(x9171,x9171),x9172),f3(a4,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[900,912,905,880,893,911,2,21,6,7])).
% 36.12/36.10 cnf(920,plain,
% 36.12/36.10 (E(a4,f3(a4,f3(a2,x9201)))),
% 36.12/36.10 inference(scs_inference,[],[900,912,905,899,362,880,893,911,2,21,6,7,3])).
% 36.12/36.10 cnf(924,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a4,a4)),f3(f3(x9241,x9241),x9242))),
% 36.12/36.10 inference(scs_inference,[],[309,920,917,2,21])).
% 36.12/36.10 cnf(925,plain,
% 36.12/36.10 (~P1(f3(a4,f3(a4,a4)),f3(x9251,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(rename_variables,[],[309])).
% 36.12/36.10 cnf(929,plain,
% 36.12/36.10 (P1(f3(f3(x9291,x9291),x9292),f3(f3(x9293,x9293),x9294))),
% 36.12/36.10 inference(scs_inference,[],[309,925,909,920,917,2,21,6,7])).
% 36.12/36.10 cnf(930,plain,
% 36.12/36.10 (E(f3(f3(x9301,x9301),x9302),f3(f3(x9303,x9303),x9304))),
% 36.12/36.10 inference(scs_inference,[],[309,925,909,920,905,917,2,21,6,7,3])).
% 36.12/36.10 cnf(931,plain,
% 36.12/36.10 (~P1(a4,f3(x9311,x9311))),
% 36.12/36.10 inference(scs_inference,[],[309,925,909,920,905,917,2,21,6,7,3,23])).
% 36.12/36.10 cnf(941,plain,
% 36.12/36.10 (E(a2,f3(f3(x9411,x9411),x9412))),
% 36.12/36.10 inference(scs_inference,[],[895,924,24,2])).
% 36.12/36.10 cnf(942,plain,
% 36.12/36.10 (~P1(f3(a4,a2),f3(f3(x9421,x9421),x9422))),
% 36.12/36.10 inference(scs_inference,[],[900,895,924,929,24,2,21])).
% 36.12/36.10 cnf(943,plain,
% 36.12/36.10 (P1(f3(f3(x9431,x9431),x9432),f3(f3(x9433,x9433),x9434))),
% 36.12/36.10 inference(rename_variables,[],[929])).
% 36.12/36.10 cnf(944,plain,
% 36.12/36.10 (~P1(f3(a4,a2),f3(x9441,f3(a4,a1)))),
% 36.12/36.10 inference(rename_variables,[],[900])).
% 36.12/36.10 cnf(949,plain,
% 36.12/36.10 (P1(f3(f3(x9491,x9491),x9492),f3(f3(x9493,a4),x9494))),
% 36.12/36.10 inference(scs_inference,[],[900,944,851,895,924,929,943,917,24,2,21,6,7])).
% 36.12/36.10 cnf(958,plain,
% 36.12/36.10 (~P1(f3(a4,a1),f3(f3(x9581,x9581),x9582))),
% 36.12/36.10 inference(scs_inference,[],[406,855,942,949,24,2,21])).
% 36.12/36.10 cnf(959,plain,
% 36.12/36.10 (P1(f3(f3(x9591,x9591),x9592),f3(f3(x9593,a4),x9594))),
% 36.12/36.10 inference(rename_variables,[],[949])).
% 36.12/36.10 cnf(960,plain,
% 36.12/36.10 (~P1(f3(a4,a1),f3(f3(x9601,x9602),f3(a4,x9602)))),
% 36.12/36.10 inference(rename_variables,[],[406])).
% 36.12/36.10 cnf(965,plain,
% 36.12/36.10 (P1(f3(f3(x9651,x9651),x9652),f3(a2,f3(x9653,a4)))),
% 36.12/36.10 inference(scs_inference,[],[406,960,534,855,942,949,959,917,24,2,21,6,7])).
% 36.12/36.10 cnf(967,plain,
% 36.12/36.10 (E(f3(x9671,f3(a4,f3(a4,a4))),f3(f3(x9672,x9672),x9673))),
% 36.12/36.10 inference(scs_inference,[],[406,960,941,534,855,942,949,959,917,24,2,21,6,7,3])).
% 36.12/36.10 cnf(970,plain,
% 36.12/36.10 (E(f3(f3(x9701,x9701),x9702),f3(x9703,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[967,958,24,2])).
% 36.12/36.10 cnf(971,plain,
% 36.12/36.10 (~P1(f3(a4,a2),f3(a2,x9711))),
% 36.12/36.10 inference(scs_inference,[],[900,967,958,903,24,2,21])).
% 36.12/36.10 cnf(972,plain,
% 36.12/36.10 (P1(f3(a2,x9721),f3(f3(x9722,x9723),f3(a4,x9723)))),
% 36.12/36.10 inference(rename_variables,[],[903])).
% 36.12/36.10 cnf(973,plain,
% 36.12/36.10 (~P1(f3(a4,a2),f3(x9731,f3(a4,a1)))),
% 36.12/36.10 inference(rename_variables,[],[900])).
% 36.12/36.10 cnf(978,plain,
% 36.12/36.10 (P1(f3(f3(x9781,x9781),x9782),f3(a2,x9783))),
% 36.12/36.10 inference(scs_inference,[],[900,973,967,789,958,903,972,965,24,2,21,6,7])).
% 36.12/36.10 cnf(980,plain,
% 36.12/36.10 (E(f3(f3(x9801,x9801),x9802),f3(f3(x9803,x9804),f3(a4,x9804)))),
% 36.12/36.10 inference(scs_inference,[],[900,973,930,967,789,297,958,903,972,965,24,2,21,6,7,3])).
% 36.12/36.10 cnf(986,plain,
% 36.12/36.10 (E(f3(f3(x9861,x9862),f3(a4,x9862)),f3(f3(x9863,x9863),x9864))),
% 36.12/36.10 inference(scs_inference,[],[980,971,24,2])).
% 36.12/36.10 cnf(987,plain,
% 36.12/36.10 (P1(f3(a2,x9871),f3(x9872,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(scs_inference,[],[970,980,971,882,24,2,7])).
% 36.12/36.10 cnf(989,plain,
% 36.12/36.10 (E(f3(f3(x9891,x9891),x9892),f3(x9893,f3(a4,f3(a4,a4))))),
% 36.12/36.10 inference(rename_variables,[],[970])).
% 36.12/36.10 cnf(990,plain,
% 36.12/36.10 (E(f3(f3(x9901,x9901),x9902),f3(x9903,x9903))),
% 36.12/36.10 inference(scs_inference,[],[970,989,980,46,971,882,24,2,7,3])).
% 36.12/36.10 cnf(993,plain,
% 36.12/36.10 (E(f3(x9931,x9931),f3(f3(x9932,x9932),x9933))),
% 36.12/36.10 inference(scs_inference,[],[990,2])).
% 36.12/36.10 cnf(996,plain,
% 36.12/36.10 (E(f3(f3(x9961,x9961),x9962),f3(x9963,f3(a4,f3(a2,x9964))))),
% 36.12/36.10 inference(scs_inference,[],[990,895,562,891,2,7,3])).
% 36.12/36.10 cnf(998,plain,
% 36.12/36.10 (E(f3(x9981,f3(a4,f3(a2,x9982))),f3(f3(x9983,x9983),x9984))),
% 36.12/36.10 inference(scs_inference,[],[996,2])).
% 36.12/36.10 cnf(999,plain,
% 36.12/36.10 (P1(f3(x9991,f3(x9991,f3(x9992,x9992))),f3(f3(x9993,x9993),x9994))),
% 36.12/36.10 inference(scs_inference,[],[993,996,363,2,7])).
% 36.12/36.10 cnf(1003,plain,
% 36.12/36.10 (~P1(f3(a4,a1),f3(f3(x10031,x10032),f3(a4,x10032)))),
% 36.12/36.10 inference(rename_variables,[],[406])).
% 36.12/36.10 cnf(1007,plain,
% 36.12/36.10 (~E(f3(a4,f3(x10071,x10071)),a1)),
% 36.12/36.10 inference(scs_inference,[],[406,1003,993,996,333,336,363,2,7,3,21,6,5])).
% 36.12/36.10 cnf(1008,plain,
% 36.12/36.10 (~E(f3(a4,f3(a4,f3(a4,a2))),a2)),
% 36.12/36.11 inference(scs_inference,[],[763,931,3,19])).
% 36.12/36.11 cnf(1012,plain,
% 36.12/36.11 (E(f3(f3(a4,f3(a4,a4)),f3(a2,x10121)),a4)),
% 36.12/36.11 inference(scs_inference,[],[567,1008,1007,18,64,2])).
% 36.12/36.11 cnf(1014,plain,
% 36.12/36.11 (P1(f3(x10141,f3(x10141,f3(x10142,x10142))),f3(f3(x10143,x10143),x10144))),
% 36.12/36.11 inference(rename_variables,[],[999])).
% 36.12/36.11 cnf(1015,plain,
% 36.12/36.11 (~P1(f3(a4,a2),f3(x10151,f3(a4,a1)))),
% 36.12/36.11 inference(rename_variables,[],[900])).
% 36.12/36.11 cnf(1020,plain,
% 36.12/36.11 (E(f3(x10201,f3(a4,f3(a2,x10202))),f3(x10203,x10203))),
% 36.12/36.11 inference(scs_inference,[],[900,1015,567,25,554,999,1014,1008,1007,18,64,2,21,6,3])).
% 36.12/36.11 cnf(1027,plain,
% 36.12/36.11 (E(f3(x10271,x10271),f3(x10272,f3(a4,f3(a2,x10273))))),
% 36.12/36.11 inference(scs_inference,[],[1020,2])).
% 36.12/36.11 cnf(1028,plain,
% 36.12/36.11 (~P1(f3(a4,a1),f3(a4,f3(f3(a4,f3(a4,a4)),f3(a2,x10281))))),
% 36.12/36.11 inference(scs_inference,[],[454,1020,335,2,21])).
% 36.12/36.11 cnf(1029,plain,
% 36.12/36.11 (P1(f3(a4,x10291),f3(f3(a4,f3(a4,a4)),x10291))),
% 36.12/36.11 inference(rename_variables,[],[335])).
% 36.12/36.11 cnf(1030,plain,
% 36.12/36.11 (~P1(f3(a4,a1),f3(x10301,f3(x10301,f3(a2,x10302))))),
% 36.12/36.11 inference(rename_variables,[],[454])).
% 36.12/36.11 cnf(1032,plain,
% 36.12/36.11 (~E(f3(a4,f3(f3(a4,f3(a4,a4)),f3(a2,x10321))),f3(a4,a1))),
% 36.12/36.11 inference(scs_inference,[],[454,1030,1020,335,1029,2,21,6])).
% 36.12/36.11 cnf(1035,plain,
% 36.12/36.11 (P1(f3(f3(x10351,x10351),x10352),f3(x10353,x10353))),
% 36.12/36.11 inference(scs_inference,[],[454,1030,1020,978,335,1029,2,21,6,7])).
% 36.12/36.11 cnf(1037,plain,
% 36.12/36.11 (E(f3(x10371,f3(a4,f3(a2,x10372))),f3(x10373,x10373))),
% 36.12/36.11 inference(rename_variables,[],[1020])).
% 36.12/36.11 cnf(1038,plain,
% 36.12/36.11 (E(f3(x10381,f3(a4,f3(a2,x10382))),f3(f3(x10383,a4),x10384))),
% 36.12/36.11 inference(scs_inference,[],[454,1030,1020,1037,881,978,335,1029,2,21,6,7,3])).
% 36.12/36.11 cnf(1047,plain,
% 36.12/36.11 (E(f3(f3(x10471,a4),x10472),f3(x10473,f3(a4,f3(a2,x10474))))),
% 36.12/36.11 inference(scs_inference,[],[1038,1032,1028,22,5,24,2])).
% 36.12/36.11 cnf(1048,plain,
% 36.12/36.11 (E(f3(x10481,x10481),f3(f3(x10482,x10483),f3(a4,x10483)))),
% 36.12/36.11 inference(scs_inference,[],[1027,1038,685,1032,1028,22,5,24,2,3])).
% 36.12/36.11 cnf(1053,plain,
% 36.12/36.11 (E(f3(f3(x10531,x10532),f3(a4,x10532)),f3(x10533,x10533))),
% 36.12/36.11 inference(scs_inference,[],[1048,2])).
% 36.12/36.11 cnf(1054,plain,
% 36.12/36.11 (P1(f3(f3(x10541,x10541),x10542),f3(f3(x10543,x10544),f3(a4,x10544)))),
% 36.12/36.11 inference(scs_inference,[],[1048,1035,2,7])).
% 36.12/36.11 cnf(1056,plain,
% 36.12/36.11 (E(f3(x10561,x10561),f3(a2,x10562))),
% 36.12/36.11 inference(scs_inference,[],[1048,884,1035,2,7,3])).
% 36.12/36.11 cnf(1060,plain,
% 36.12/36.11 (E(f3(a2,x10601),f3(x10602,x10602))),
% 36.12/36.11 inference(scs_inference,[],[1056,2])).
% 36.12/36.11 cnf(1064,plain,
% 36.12/36.11 (E(f3(x10641,x10641),f3(x10642,f3(a4,f3(a4,a4))))),
% 36.12/36.11 inference(scs_inference,[],[1053,1056,532,987,2,7,3])).
% 36.12/36.11 cnf(1067,plain,
% 36.12/36.11 (E(f3(x10671,f3(a4,f3(a4,a4))),f3(x10672,x10672))),
% 36.12/36.11 inference(scs_inference,[],[1064,2])).
% 36.12/36.11 cnf(1068,plain,
% 36.12/36.11 (P1(f3(f3(x10681,x10681),x10682),f3(x10683,f3(a4,f3(a4,a4))))),
% 36.12/36.11 inference(scs_inference,[],[1064,1054,2,7])).
% 36.12/36.11 cnf(1070,plain,
% 36.12/36.11 (E(f3(x10701,x10701),f3(x10702,f3(a4,f3(a4,a4))))),
% 36.12/36.11 inference(rename_variables,[],[1064])).
% 36.12/36.11 cnf(1071,plain,
% 36.12/36.11 (E(f3(x10711,x10711),f3(x10712,a4))),
% 36.12/36.11 inference(scs_inference,[],[1064,1070,511,1054,2,7,3])).
% 36.12/36.11 cnf(1074,plain,
% 36.12/36.11 (E(f3(x10741,a4),f3(x10742,x10742))),
% 36.12/36.11 inference(scs_inference,[],[1071,2])).
% 36.12/36.11 cnf(1075,plain,
% 36.12/36.11 (P1(f3(x10751,f3(x10751,f3(x10752,x10752))),f3(x10753,x10753))),
% 36.12/36.11 inference(scs_inference,[],[1067,1071,999,2,7])).
% 36.12/36.11 cnf(1077,plain,
% 36.12/36.11 (E(f3(x10771,f3(a4,f3(a4,a4))),f3(x10772,x10772))),
% 36.12/36.11 inference(rename_variables,[],[1067])).
% 36.12/36.11 cnf(1078,plain,
% 36.12/36.11 (E(f3(x10781,f3(a4,f3(a4,a4))),f3(a2,f3(a2,x10782)))),
% 36.12/36.11 inference(scs_inference,[],[1067,1077,1071,241,999,2,7,3])).
% 36.12/36.11 cnf(1083,plain,
% 36.12/36.11 (E(f3(f3(a4,f3(a4,a4)),f3(a2,x10831)),f3(a4,f3(a4,a4)))),
% 36.12/36.11 inference(scs_inference,[],[1078,1012,52,2,3])).
% 36.12/36.11 cnf(1085,plain,
% 36.12/36.11 (E(f3(f3(a4,f3(a4,a4)),a2),f3(a4,f3(a2,x10851)))),
% 36.12/36.11 inference(scs_inference,[],[1083,815,920,2,3])).
% 36.12/36.11 cnf(1087,plain,
% 36.12/36.11 (E(f3(a4,f3(a2,x10871)),f3(f3(a4,f3(a4,a4)),a2))),
% 36.12/36.11 inference(scs_inference,[],[1085,2])).
% 36.12/36.11 cnf(1088,plain,
% 36.12/36.11 (E(f3(a4,f3(a4,a4)),f3(a4,f3(a2,x10881)))),
% 36.12/36.11 inference(scs_inference,[],[1085,645,2,3])).
% 36.12/36.11 cnf(1091,plain,
% 36.12/36.11 (P1(f3(f3(f3(x10911,x10912),f3(a4,x10912)),x10913),f3(f3(x10914,x10914),x10915))),
% 36.12/36.11 inference(scs_inference,[],[986,1088,14,2,7])).
% 36.12/36.11 cnf(1093,plain,
% 36.12/36.11 (E(f3(a4,f3(a4,f3(a4,a2))),f3(a4,f3(a2,x10931)))),
% 36.12/36.11 inference(scs_inference,[],[986,1088,759,14,2,7,3])).
% 36.12/36.11 cnf(1102,plain,
% 36.12/36.11 (P1(f3(f3(f3(x11021,a4),x11022),x11023),f3(f3(x11024,x11024),x11025))),
% 36.12/36.11 inference(scs_inference,[],[892,1093,14,2,7])).
% 36.12/36.11 cnf(1105,plain,
% 36.12/36.11 (~P1(f3(a4,a1),f3(x11051,f3(a4,f3(a2,x11052))))),
% 36.12/36.11 inference(rename_variables,[],[581])).
% 36.12/36.11 cnf(1109,plain,
% 36.12/36.11 (E(f3(x11091,f3(a4,f3(a2,x11092))),f3(a2,f3(a2,x11093)))),
% 36.12/36.11 inference(scs_inference,[],[581,1105,892,998,1093,1078,14,2,7,21,6,3])).
% 36.12/36.11 cnf(1117,plain,
% 36.12/36.11 (E(f3(f3(a1,f3(a2,x11171)),a2),f3(a1,a2))),
% 36.12/36.11 inference(scs_inference,[],[1047,1109,116,479,1068,2,7,3])).
% 36.12/36.11 cnf(1119,plain,
% 36.12/36.11 (P1(f3(f3(f3(x11191,x11192),f3(a4,x11192)),x11193),f3(x11194,x11194))),
% 36.12/36.11 inference(scs_inference,[],[1074,1117,1091,2,7])).
% 36.12/36.11 cnf(1122,plain,
% 36.12/36.11 (E(f3(a2,x11221),f3(x11222,f3(a4,f3(a4,a4))))),
% 36.12/36.11 inference(scs_inference,[],[1060,1074,1117,512,1091,2,7,3])).
% 36.12/36.11 cnf(1126,plain,
% 36.12/36.11 (E(f3(x11261,f3(a4,f3(a4,a4))),f3(a2,x11262))),
% 36.12/36.11 inference(scs_inference,[],[1122,2])).
% 36.12/36.11 cnf(1130,plain,
% 36.12/36.11 (E(f3(a4,f3(a2,x11301)),f3(f3(a4,f3(a4,a4)),f3(x11302,a4)))),
% 36.12/36.11 inference(scs_inference,[],[1122,1087,1067,276,1102,2,7,3])).
% 36.12/36.11 cnf(1134,plain,
% 36.12/36.11 (P1(f3(x11341,f3(x11341,f3(x11342,x11342))),f3(a2,x11343))),
% 36.12/36.11 inference(scs_inference,[],[1126,1130,1075,2,7])).
% 36.12/36.11 cnf(1320,plain,
% 36.12/36.11 (E(f3(f3(a1,f3(x13201,a4)),f3(a2,x13202)),f3(a1,f3(a2,x13203)))),
% 36.12/36.11 inference(scs_inference,[],[523,249,3])).
% 36.12/36.11 cnf(1338,plain,
% 36.12/36.11 (E(f3(x13381,f3(x13381,f3(x13382,x13382))),a2)),
% 36.12/36.11 inference(scs_inference,[],[12,554,746,249,1320,1134,2,3,7,20])).
% 36.12/36.11 cnf(1369,plain,
% 36.12/36.11 (E(a2,f3(x13691,f3(x13691,f3(x13692,x13692))))),
% 36.12/36.11 inference(scs_inference,[],[1338,2])).
% 36.12/36.11 cnf(1370,plain,
% 36.12/36.11 (P1(f3(f3(f3(x13701,x13702),f3(a4,x13702)),x13703),a2)),
% 36.12/36.11 inference(scs_inference,[],[554,1338,1119,2,7])).
% 36.12/36.11 cnf(1373,plain,
% 36.12/36.11 (E(f3(f3(a1,f3(x13731,a4)),f3(a2,x13732)),f3(a1,a2))),
% 36.12/36.11 inference(scs_inference,[],[554,525,249,1338,1119,2,7,3])).
% 36.12/36.11 cnf(1379,plain,
% 36.12/36.11 (E(f3(f3(f3(x13791,x13792),f3(a4,x13792)),x13793),a2)),
% 36.12/36.11 inference(scs_inference,[],[12,1373,1370,2,20])).
% 36.12/36.11 cnf(1461,plain,
% 36.12/36.11 (E(a2,f3(f3(f3(x14611,x14612),f3(a4,x14612)),x14613))),
% 36.12/36.11 inference(scs_inference,[],[1379,2])).
% 36.12/36.11 cnf(1466,plain,
% 36.12/36.11 (P1(f3(x14661,f3(a4,f3(x14662,x14662))),a2)),
% 36.12/36.11 inference(scs_inference,[],[13,835,7])).
% 36.12/36.11 cnf(1473,plain,
% 36.12/36.11 (E(f3(x14731,f3(a4,f3(x14732,x14732))),a2)),
% 36.12/36.11 inference(scs_inference,[],[13,41,281,12,835,7,21,6,3,2,20])).
% 36.12/36.11 cnf(1476,plain,
% 36.12/36.11 (P1(x14761,f3(a4,f3(x14762,x14762)))),
% 36.12/36.11 inference(scs_inference,[],[13,41,281,12,835,7,21,6,3,2,20,19])).
% 36.12/36.11 cnf(1484,plain,
% 36.12/36.11 (P1(f3(f3(x14841,f3(x14841,x14842)),f3(x14842,f3(x14841,x14842))),a2)),
% 36.12/36.11 inference(scs_inference,[],[13,1473,1476,578,16,2,20,7])).
% 36.12/36.11 cnf(1486,plain,
% 36.12/36.11 (E(f3(x14861,x14861),a2)),
% 36.12/36.11 inference(rename_variables,[],[13])).
% 36.12/36.11 cnf(1490,plain,
% 36.12/36.11 (E(f3(x14901,x14901),f3(x14902,f3(x14902,f3(x14903,x14903))))),
% 36.12/36.11 inference(scs_inference,[],[13,1486,41,1369,1473,1476,578,16,2,20,7,21,6,3])).
% 36.12/36.11 cnf(1497,plain,
% 36.12/36.11 (P1(f3(x14971,f3(x14971,x14972)),f3(x14972,f3(x14971,x14972)))),
% 36.12/36.11 inference(scs_inference,[],[13,941,1490,1461,12,1484,1466,2,20,7,3,19])).
% 36.12/36.11 cnf(1937,plain,
% 36.12/36.11 (P1(f3(x19371,f3(x19371,x19372)),f3(x19372,f3(x19371,x19372)))),
% 36.12/36.11 inference(rename_variables,[],[1497])).
% 36.12/36.11 cnf(1939,plain,
% 36.12/36.11 ($false),
% 36.12/36.11 inference(scs_inference,[],[28,15,1497,1937,21,6]),
% 36.12/36.11 ['proof']).
% 36.12/36.11 % SZS output end Proof
% 36.12/36.11 % Total time :35.490000s
%------------------------------------------------------------------------------