%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : HEN010-7 : 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 : n032.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 58.64s 58.74s
% Output : CNFRefutation 58.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : HEN010-7 : TPTP v8.2.0. Released v1.0.0.
% 0.00/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.29 % Computer : n032.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Sat Jun 22 05:25:23 EDT 2024
% 0.09/0.29 % CPUTime :
% 0.14/0.49 start to proof:theBenchmark
% 58.64/58.73 %-------------------------------------------
% 58.64/58.73 % File :CSE---1.7
% 58.64/58.73 % Problem :theBenchmark
% 58.64/58.73 % Transform :cnf
% 58.64/58.73 % Format :tptp:raw
% 58.64/58.73 % Command :java -jar mcs_scs.jar %d %s
% 58.64/58.73
% 58.64/58.73 % Result :Theorem 58.200000s
% 58.64/58.73 % Output :CNFRefutation 58.200000s
% 58.64/58.73 %-------------------------------------------
% 58.64/58.74 %--------------------------------------------------------------------------
% 58.64/58.74 % File : HEN010-7 : TPTP v8.2.0. Released v1.0.0.
% 58.64/58.74 % Domain : Henkin Models
% 58.64/58.74 % Problem : Define X' as identity/X. Then X' = X'/(identity/X')
% 58.64/58.74 % Version : [MOW76] axioms : Augmented.
% 58.64/58.74 % English :
% 58.64/58.74
% 58.64/58.74 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 58.64/58.74 % Source : [MOW76]
% 58.64/58.74 % Names : hp10.ver1.in [ANL]
% 58.64/58.74
% 58.64/58.74 % Status : Unsatisfiable
% 58.64/58.74 % Rating : 0.06 v8.2.0, 0.08 v8.1.0, 0.00 v6.0.0, 0.11 v5.5.0, 0.19 v5.4.0, 0.13 v5.3.0, 0.25 v5.2.0, 0.12 v5.1.0, 0.14 v5.0.0, 0.29 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.17 v2.3.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.29 v2.1.0, 0.20 v2.0.0
% 58.64/58.74 % Syntax : Number of clauses : 21 ( 11 unt; 0 nHn; 14 RR)
% 58.64/58.74 % Number of literals : 44 ( 3 equ; 24 neg)
% 58.64/58.74 % Maximal clause size : 6 ( 2 avg)
% 58.64/58.74 % Maximal term depth : 2 ( 1 avg)
% 58.64/58.74 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 58.64/58.74 % Number of functors : 7 ( 7 usr; 6 con; 0-2 aty)
% 58.64/58.74 % Number of variables : 47 ( 5 sgn)
% 58.64/58.74 % SPC : CNF_UNS_RFO_SEQ_HRN
% 58.64/58.74
% 58.64/58.74 % Comments :
% 58.64/58.74 %--------------------------------------------------------------------------
% 58.64/58.74 %----Include Henkin model axioms
% 58.64/58.74 include('Axioms/HEN001-0.ax').
% 58.64/58.74 %--------------------------------------------------------------------------
% 58.64/58.74 %----McCharen uses these earlier results too. I don't
% 58.64/58.74 cnf(everything_divide_identity_is_zero,axiom,
% 58.64/58.74 quotient(X,identity,zero) ).
% 58.64/58.74
% 58.64/58.74 cnf(zero_divide_anything_is_zero,axiom,
% 58.64/58.74 quotient(zero,X,zero) ).
% 58.64/58.74
% 58.64/58.74 cnf(x_divide_x_is_zero,axiom,
% 58.64/58.74 quotient(X,X,zero) ).
% 58.64/58.74
% 58.64/58.74 cnf(x_divde_zero_is_x,axiom,
% 58.64/58.74 quotient(X,zero,X) ).
% 58.64/58.74
% 58.64/58.74 cnf(transitivity_of_less_equal,axiom,
% 58.64/58.74 ( ~ less_equal(X,Y)
% 58.64/58.74 | ~ less_equal(Y,Z)
% 58.64/58.74 | less_equal(X,Z) ) ).
% 58.64/58.74
% 58.64/58.74 cnf(xQyLEz_implies_xQzLEy,axiom,
% 58.64/58.74 ( ~ quotient(X,Y,W1)
% 58.64/58.74 | ~ less_equal(W1,Z)
% 58.64/58.74 | ~ quotient(X,Z,W2)
% 58.64/58.74 | less_equal(W2,Y) ) ).
% 58.64/58.74
% 58.64/58.74 cnf(xLEy_implies_zQyLEzQx,axiom,
% 58.64/58.74 ( ~ less_equal(X,Y)
% 58.64/58.74 | ~ quotient(Z,Y,W1)
% 58.64/58.74 | ~ quotient(Z,X,W2)
% 58.64/58.74 | less_equal(W1,W2) ) ).
% 58.64/58.74
% 58.64/58.74 cnf(xLEy_implies_xQzLEyQz,axiom,
% 58.64/58.74 ( ~ less_equal(X,Y)
% 58.64/58.74 | ~ quotient(X,Z,W1)
% 58.64/58.74 | ~ quotient(Y,Z,W2)
% 58.64/58.74 | less_equal(W1,W2) ) ).
% 58.64/58.74
% 58.64/58.74 cnf(identity_divide_a,hypothesis,
% 58.64/58.74 quotient(identity,a,idQa) ).
% 58.64/58.74
% 58.64/58.74 cnf(identity_divide_idQa,hypothesis,
% 58.64/58.74 quotient(identity,idQa,idQ_idQa) ).
% 58.64/58.74
% 58.64/58.74 cnf(identity_divide_idQ_idQa,hypothesis,
% 58.64/58.74 quotient(idQa,idQ_idQa,idQa_Q__idQ_idQa) ).
% 58.64/58.74
% 58.64/58.74 cnf(prove_idQa_equals_idQa_Q__idQ_idQa,negated_conjecture,
% 58.64/58.74 idQa != idQa_Q__idQ_idQa ).
% 58.64/58.74
% 58.64/58.74 %--------------------------------------------------------------------------
% 58.64/58.74 %-------------------------------------------
% 58.64/58.74 % Proof found
% 58.64/58.74 % SZS status Theorem for theBenchmark
% 58.64/58.74 % SZS output start Proof
% 58.64/58.74 %ClaNum:31(EqnAxiom:10)
% 58.64/58.74 %VarNum:92(SingletonVarNum:47)
% 58.64/58.74 %MaxLitNum:6
% 58.64/58.74 %MaxfuncDepth:1
% 58.64/58.74 %SharedTerms:10
% 58.64/58.74 %goalClause: 21
% 58.64/58.74 %singleGoalClaCount:1
% 58.64/58.74 [13]P2(a1,a2,a3)
% 58.64/58.74 [14]P2(a1,a3,a4)
% 58.64/58.74 [15]P2(a3,a4,a6)
% 58.64/58.74 [21]~E(a6,a3)
% 58.64/58.74 [11]P1(x111,a1)
% 58.64/58.74 [12]P1(a7,x121)
% 58.64/58.74 [16]P2(x161,a1,a7)
% 58.64/58.74 [17]P2(a7,x171,a7)
% 58.64/58.74 [18]P2(x181,x181,a7)
% 58.64/58.74 [19]P2(x191,a7,x191)
% 58.64/58.74 [20]P2(x201,x202,f5(x201,x202))
% 58.64/58.74 [24]~P1(x241,x242)+P2(x241,x242,a7)
% 58.64/58.74 [25]P1(x251,x252)+~P2(x251,x252,a7)
% 58.64/58.74 [26]P1(x261,x262)+~P2(x262,x263,x261)
% 58.64/58.74 [22]~P1(x222,x221)+~P1(x221,x222)+E(x221,x222)
% 58.64/58.74 [23]~P1(x231,x233)+P1(x231,x232)+~P1(x233,x232)
% 58.64/58.74 [27]~P2(x273,x274,x271)+E(x271,x272)+~P2(x273,x274,x272)
% 58.64/58.74 [28]~P2(x285,x282,x283)+P1(x281,x282)+~P2(x285,x284,x281)+~P1(x283,x284)
% 58.64/58.74 [29]~P2(x295,x293,x292)+P1(x291,x292)+~P2(x295,x294,x291)+~P1(x293,x294)
% 58.64/58.74 [30]~P2(x303,x305,x301)+P1(x301,x302)+~P2(x304,x305,x302)+~P1(x303,x304)
% 58.64/58.74 [31]~P2(x318,x317,x315)+P1(x311,x312)+~P2(x313,x314,x311)+~P2(x315,x316,x312)+~P2(x317,x316,x314)+~P2(x318,x316,x313)
% 58.64/58.74 %EqnAxiom
% 58.64/58.74 [1]E(x11,x11)
% 58.64/58.74 [2]E(x22,x21)+~E(x21,x22)
% 58.64/58.74 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.64/58.74 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 58.64/58.74 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 58.64/58.74 [6]P1(x62,x63)+~E(x61,x62)+~P1(x61,x63)
% 58.64/58.74 [7]P1(x73,x72)+~E(x71,x72)+~P1(x73,x71)
% 58.64/58.74 [8]P2(x82,x83,x84)+~E(x81,x82)+~P2(x81,x83,x84)
% 58.64/58.74 [9]P2(x93,x92,x94)+~E(x91,x92)+~P2(x93,x91,x94)
% 58.64/58.74 [10]P2(x103,x104,x102)+~E(x101,x102)+~P2(x103,x104,x101)
% 58.64/58.74
% 58.64/58.74 %-------------------------------------------
% 58.64/58.76 cnf(32,plain,
% 58.64/58.76 (P1(x321,x321)),
% 58.64/58.76 inference(scs_inference,[],[18,25])).
% 58.64/58.76 cnf(34,plain,
% 58.64/58.76 (E(a7,f5(x341,x341))),
% 58.64/58.76 inference(scs_inference,[],[18,20,25,27])).
% 58.64/58.76 cnf(35,plain,
% 58.64/58.76 (P2(x351,x352,f5(x351,x352))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(37,plain,
% 58.64/58.76 (P1(f5(x371,x371),x372)),
% 58.64/58.76 inference(scs_inference,[],[18,20,12,25,27,6])).
% 58.64/58.76 cnf(39,plain,
% 58.64/58.76 (P2(x391,x391,a7)),
% 58.64/58.76 inference(rename_variables,[],[18])).
% 58.64/58.76 cnf(40,plain,
% 58.64/58.76 (P2(x401,f5(a7,a7),x401)),
% 58.64/58.76 inference(scs_inference,[],[18,19,20,12,25,27,6,8,9])).
% 58.64/58.76 cnf(41,plain,
% 58.64/58.76 (P2(x411,x411,f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[18,39,19,20,12,25,27,6,8,9,10])).
% 58.64/58.76 cnf(48,plain,
% 58.64/58.76 (E(f5(a7,a7),a7)),
% 58.64/58.76 inference(scs_inference,[],[18,39,19,20,35,12,25,27,6,8,9,10,31,2])).
% 58.64/58.76 cnf(49,plain,
% 58.64/58.76 (E(f5(a7,f5(a7,a7)),a7)),
% 58.64/58.76 inference(scs_inference,[],[18,39,19,20,35,12,25,27,6,8,9,10,31,2,22])).
% 58.64/58.76 cnf(55,plain,
% 58.64/58.76 (E(a7,f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[49,2])).
% 58.64/58.76 cnf(56,plain,
% 58.64/58.76 (E(f5(a7,a7),f5(x561,x561))),
% 58.64/58.76 inference(scs_inference,[],[49,41,20,2,27])).
% 58.64/58.76 cnf(59,plain,
% 58.64/58.76 (E(f5(a7,f5(a7,a7)),f5(x591,x591))),
% 58.64/58.76 inference(scs_inference,[],[49,34,41,20,2,27,3])).
% 58.64/58.76 cnf(60,plain,
% 58.64/58.76 (P2(a7,f5(a7,f5(a7,a7)),f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[49,34,41,20,2,27,3,8])).
% 58.64/58.76 cnf(61,plain,
% 58.64/58.76 (P2(x611,x611,f5(a7,a7))),
% 58.64/58.76 inference(rename_variables,[],[41])).
% 58.64/58.76 cnf(62,plain,
% 58.64/58.76 (P2(f5(a7,f5(a7,a7)),f5(a7,a7),a7)),
% 58.64/58.76 inference(scs_inference,[],[49,34,41,40,20,2,27,3,8,10])).
% 58.64/58.76 cnf(64,plain,
% 58.64/58.76 (P2(f5(a7,f5(a7,a7)),a7,f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[49,34,41,61,40,20,2,27,3,8,10,9])).
% 58.64/58.76 cnf(69,plain,
% 58.64/58.76 (P2(x691,a7,x691)),
% 58.64/58.76 inference(rename_variables,[],[19])).
% 58.64/58.76 cnf(71,plain,
% 58.64/58.76 (P1(f5(a7,f5(a7,a7)),x711)),
% 58.64/58.76 inference(scs_inference,[],[56,55,64,19,12,2,27,6])).
% 58.64/58.76 cnf(73,plain,
% 58.64/58.76 (P2(a7,f5(x731,x731),f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[56,59,55,60,62,64,19,12,2,27,6,8,9])).
% 58.64/58.76 cnf(74,plain,
% 58.64/58.76 (P2(a7,f5(a7,f5(a7,a7)),f5(x741,x741))),
% 58.64/58.76 inference(scs_inference,[],[56,59,55,60,62,64,19,12,2,27,6,8,9,10])).
% 58.64/58.76 cnf(75,plain,
% 58.64/58.76 (P1(a4,a2)),
% 58.64/58.76 inference(scs_inference,[],[56,59,55,13,14,32,60,62,64,19,12,2,27,6,8,9,10,28])).
% 58.64/58.76 cnf(78,plain,
% 58.64/58.76 (P1(f5(a3,a2),a6)),
% 58.64/58.76 inference(scs_inference,[],[56,59,55,13,14,15,32,60,62,64,19,20,12,2,27,6,8,9,10,28,29])).
% 58.64/58.76 cnf(79,plain,
% 58.64/58.76 (P2(x791,x792,f5(x791,x792))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(81,plain,
% 58.64/58.76 (P1(f5(a3,a7),a3)),
% 58.64/58.76 inference(scs_inference,[],[56,59,55,13,14,15,32,60,62,64,17,19,69,20,79,12,2,27,6,8,9,10,28,29,31])).
% 58.64/58.76 cnf(90,plain,
% 58.64/58.76 (E(f5(x901,x901),f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[59,2])).
% 58.64/58.76 cnf(91,plain,
% 58.64/58.76 (E(a4,f5(a1,a3))),
% 58.64/58.76 inference(scs_inference,[],[59,14,20,2,27])).
% 58.64/58.76 cnf(92,plain,
% 58.64/58.76 (P2(x921,x922,f5(x921,x922))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(94,plain,
% 58.64/58.76 (P2(f5(a7,f5(a7,a7)),f5(x941,x941),f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[55,59,14,73,20,2,27,8])).
% 58.64/58.76 cnf(95,plain,
% 58.64/58.76 (P1(f5(a1,a3),a2)),
% 58.64/58.76 inference(scs_inference,[],[55,59,14,73,75,20,2,27,8,6])).
% 58.64/58.76 cnf(96,plain,
% 58.64/58.76 (P2(x961,a1,f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[55,59,14,16,73,75,20,2,27,8,6,10])).
% 58.64/58.76 cnf(97,plain,
% 58.64/58.76 (P2(a3,f5(a1,a3),a6)),
% 58.64/58.76 inference(scs_inference,[],[55,59,14,15,16,73,75,20,2,27,8,6,10,9])).
% 58.64/58.76 cnf(98,plain,
% 58.64/58.76 (P1(f5(f5(a3,a2),a6),f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[55,59,14,15,16,73,78,75,40,20,92,2,27,8,6,10,9,28])).
% 58.64/58.76 cnf(100,plain,
% 58.64/58.76 (P2(x1001,x1002,f5(x1001,x1002))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(102,plain,
% 58.64/58.76 (P1(f5(f5(a3,a2),a6),a7)),
% 58.64/58.76 inference(scs_inference,[],[55,59,14,15,16,18,73,78,75,40,20,92,100,2,27,8,6,10,9,28,29])).
% 58.64/58.76 cnf(103,plain,
% 58.64/58.76 (P2(x1031,x1031,a7)),
% 58.64/58.76 inference(rename_variables,[],[18])).
% 58.64/58.76 cnf(104,plain,
% 58.64/58.76 (P2(x1041,x1042,f5(x1041,x1042))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(106,plain,
% 58.64/58.76 (P1(a4,f5(a4,a3))),
% 58.64/58.76 inference(scs_inference,[],[55,59,14,15,16,18,103,73,78,75,40,19,20,92,100,104,2,27,8,6,10,9,28,29,31])).
% 58.64/58.76 cnf(111,plain,
% 58.64/58.76 (E(f5(a3,a2),a6)+~P1(a6,f5(a3,a2))),
% 58.64/58.76 inference(scs_inference,[],[55,59,14,15,16,18,103,73,78,75,40,19,20,92,100,104,2,27,8,6,10,9,28,29,31,22])).
% 58.64/58.76 cnf(116,plain,
% 58.64/58.76 (E(f5(x1161,x1161),a7)),
% 58.64/58.76 inference(scs_inference,[],[34,2])).
% 58.64/58.76 cnf(117,plain,
% 58.64/58.76 (E(f5(f5(a3,a2),a6),f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[34,37,98,2,22])).
% 58.64/58.76 cnf(120,plain,
% 58.64/58.76 (E(a7,f5(x1201,a1))),
% 58.64/58.76 inference(scs_inference,[],[34,37,16,98,20,2,22,27])).
% 58.64/58.76 cnf(121,plain,
% 58.64/58.76 (P2(x1211,x1212,f5(x1211,x1212))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(123,plain,
% 58.64/58.76 (P1(f5(a1,a3),f5(a4,a3))),
% 58.64/58.76 inference(scs_inference,[],[34,91,37,16,98,106,20,2,22,27,6])).
% 58.64/58.76 cnf(124,plain,
% 58.64/58.76 (P2(f5(x1241,x1241),x1242,a7)),
% 58.64/58.76 inference(scs_inference,[],[34,91,37,16,17,98,106,20,2,22,27,6,8])).
% 58.64/58.76 cnf(125,plain,
% 58.64/58.76 (P2(a7,f5(x1251,x1251),f5(x1252,x1252))),
% 58.64/58.76 inference(scs_inference,[],[34,59,91,37,16,17,98,74,106,20,2,22,27,6,8,9])).
% 58.64/58.76 cnf(126,plain,
% 58.64/58.76 (P2(x1261,a1,f5(x1262,x1262))),
% 58.64/58.76 inference(scs_inference,[],[34,59,91,37,16,17,98,74,106,20,2,22,27,6,8,9,10])).
% 58.64/58.76 cnf(127,plain,
% 58.64/58.76 (E(f5(a7,a7),f5(x1271,a1))),
% 58.64/58.76 inference(scs_inference,[],[48,34,59,91,37,16,17,98,74,106,20,2,22,27,6,8,9,10,3])).
% 58.64/58.76 cnf(128,plain,
% 58.64/58.76 (P1(f5(f5(a3,a2),a6),f5(x1281,x1281))),
% 58.64/58.76 inference(scs_inference,[],[48,34,59,91,37,16,17,98,102,74,106,20,2,22,27,6,8,9,10,3,7])).
% 58.64/58.76 cnf(129,plain,
% 58.64/58.76 (P1(f5(f5(a3,a7),a3),f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[48,34,59,91,37,16,81,17,98,102,74,106,40,20,121,2,22,27,6,8,9,10,3,7,28])).
% 58.64/58.76 cnf(131,plain,
% 58.64/58.76 (P2(x1311,x1312,f5(x1311,x1312))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(133,plain,
% 58.64/58.76 (P1(f5(a7,a3),a7)),
% 58.64/58.76 inference(scs_inference,[],[48,34,59,91,37,16,81,17,98,102,74,106,40,20,121,131,2,22,27,6,8,9,10,3,7,28,29])).
% 58.64/58.76 cnf(138,plain,
% 58.64/58.76 (E(f5(f5(a3,a2),a6),f5(x1381,x1381))),
% 58.64/58.76 inference(scs_inference,[],[117,37,128,2,22])).
% 58.64/58.76 cnf(142,plain,
% 58.64/58.76 (E(a6,f5(a3,a4))),
% 58.64/58.76 inference(scs_inference,[],[117,37,15,128,20,2,22,27])).
% 58.64/58.76 cnf(143,plain,
% 58.64/58.76 (P2(x1431,x1432,f5(x1431,x1432))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(146,plain,
% 58.64/58.76 (P2(x1461,f5(a7,f5(a7,a7)),x1461)),
% 58.64/58.76 inference(scs_inference,[],[55,117,37,15,17,128,19,20,2,22,27,10,9])).
% 58.64/58.76 cnf(147,plain,
% 58.64/58.76 (P2(f5(a7,f5(a7,a7)),x1471,a7)),
% 58.64/58.76 inference(scs_inference,[],[55,117,37,15,17,128,19,20,2,22,27,10,9,8])).
% 58.64/58.76 cnf(148,plain,
% 58.64/58.76 (E(f5(x1481,x1481),f5(x1482,x1482))),
% 58.64/58.76 inference(scs_inference,[],[55,34,117,116,37,15,17,128,19,20,2,22,27,10,9,8,3])).
% 58.64/58.76 cnf(149,plain,
% 58.64/58.76 (P1(f5(a3,a2),f5(a3,a4))),
% 58.64/58.76 inference(scs_inference,[],[55,34,117,116,37,15,17,78,128,19,20,2,22,27,10,9,8,3,7])).
% 58.64/58.76 cnf(150,plain,
% 58.64/58.76 (P1(f5(a3,a6),a4)),
% 58.64/58.76 inference(scs_inference,[],[55,34,117,116,37,32,15,17,78,128,19,20,143,2,22,27,10,9,8,3,7,28])).
% 58.64/58.76 cnf(152,plain,
% 58.64/58.76 (P2(x1521,x1522,f5(x1521,x1522))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(154,plain,
% 58.64/58.76 (P1(a6,f5(a1,a4))),
% 58.64/58.76 inference(scs_inference,[],[55,34,117,116,37,32,15,11,17,78,128,19,20,143,152,2,22,27,10,9,8,3,7,28,30])).
% 58.64/58.76 cnf(156,plain,
% 58.64/58.76 (P2(x1561,x1562,f5(x1561,x1562))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(158,plain,
% 58.64/58.76 (P1(f5(a7,a6),a7)),
% 58.64/58.76 inference(scs_inference,[],[55,34,117,116,37,32,15,11,17,78,128,19,20,143,152,156,2,22,27,10,9,8,3,7,28,30,29])).
% 58.64/58.76 cnf(159,plain,
% 58.64/58.76 (P2(a7,x1591,a7)),
% 58.64/58.76 inference(rename_variables,[],[17])).
% 58.64/58.76 cnf(160,plain,
% 58.64/58.76 (P2(x1601,x1602,f5(x1601,x1602))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(162,plain,
% 58.64/58.76 (P1(f5(a6,a7),a6)),
% 58.64/58.76 inference(scs_inference,[],[55,34,117,116,37,32,15,11,17,159,78,128,19,20,143,152,156,160,2,22,27,10,9,8,3,7,28,30,29,31])).
% 58.64/58.76 cnf(169,plain,
% 58.64/58.76 (E(f5(x1691,x1691),f5(f5(a3,a2),a6))),
% 58.64/58.76 inference(scs_inference,[],[138,2])).
% 58.64/58.76 cnf(170,plain,
% 58.64/58.76 (E(f5(a7,a3),a7)),
% 58.64/58.76 inference(scs_inference,[],[138,12,133,2,22])).
% 58.64/58.76 cnf(173,plain,
% 58.64/58.76 (P2(x1731,x1731,f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[55,138,12,18,133,2,22,10])).
% 58.64/58.76 cnf(174,plain,
% 58.64/58.76 (P2(f5(x1741,x1741),f5(x1742,x1742),f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[59,55,138,12,18,133,94,2,22,10,8])).
% 58.64/58.76 cnf(175,plain,
% 58.64/58.76 (P1(f5(a3,a4),f5(a1,a4))),
% 58.64/58.76 inference(scs_inference,[],[59,55,138,142,12,18,133,94,154,2,22,10,8,6])).
% 58.64/58.76 cnf(176,plain,
% 58.64/58.76 (P2(x1761,f5(x1762,x1762),x1761)),
% 58.64/58.76 inference(scs_inference,[],[59,55,138,142,12,18,133,146,94,154,2,22,10,8,6,9])).
% 58.64/58.76 cnf(177,plain,
% 58.64/58.76 (E(f5(a7,f5(a7,a7)),f5(x1771,a1))),
% 58.64/58.76 inference(scs_inference,[],[59,55,138,127,142,12,18,133,146,94,154,2,22,10,8,6,9,3])).
% 58.64/58.76 cnf(179,plain,
% 58.64/58.76 (P1(f5(a7,a3),f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[59,55,138,127,142,12,18,133,146,94,154,2,22,10,8,6,9,3,7])).
% 58.64/58.76 cnf(180,plain,
% 58.64/58.76 (P1(f5(a1,f5(a4,a3)),a3)),
% 58.64/58.76 inference(scs_inference,[],[59,55,138,127,142,12,18,14,133,106,146,94,154,20,2,22,10,8,6,9,3,7,28])).
% 58.64/58.76 cnf(187,plain,
% 58.64/58.76 (E(f5(x1871,a1),f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[177,2])).
% 58.64/58.76 cnf(188,plain,
% 58.64/58.76 (E(f5(f5(a3,a7),a3),f5(a7,a7))),
% 58.64/58.76 inference(scs_inference,[],[177,37,129,2,22])).
% 58.64/58.76 cnf(192,plain,
% 58.64/58.76 (P2(x1921,f5(x1922,x1922),x1921)),
% 58.64/58.76 inference(rename_variables,[],[176])).
% 58.64/58.76 cnf(193,plain,
% 58.64/58.76 (P2(x1931,x1931,f5(x1932,x1932))),
% 58.64/58.76 inference(scs_inference,[],[59,34,177,37,18,129,176,2,22,8,10])).
% 58.64/58.76 cnf(194,plain,
% 58.64/58.76 (E(f5(a7,a3),f5(x1941,x1941))),
% 58.64/58.76 inference(scs_inference,[],[59,34,177,170,37,18,129,176,2,22,8,10,3])).
% 58.64/58.76 cnf(195,plain,
% 58.64/58.76 (P1(f5(f5(a3,a7),a3),f5(x1951,x1951))),
% 58.64/58.76 inference(scs_inference,[],[59,34,148,177,170,37,18,129,176,2,22,8,10,3,7])).
% 58.64/58.76 cnf(197,plain,
% 58.64/58.76 (P1(f5(f5(a1,a3),f5(a4,a3)),f5(x1971,x1971))),
% 58.64/58.76 inference(scs_inference,[],[59,34,148,177,170,37,18,123,129,176,192,20,2,22,8,10,3,7,28])).
% 58.64/58.76 cnf(199,plain,
% 58.64/58.76 (P2(x1991,x1992,f5(x1991,x1992))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(205,plain,
% 58.64/58.76 (P2(x2051,x2052,a7)+~E(a1,x2052)),
% 58.64/58.76 inference(scs_inference,[],[59,34,148,177,170,37,16,81,18,123,129,176,192,20,199,2,22,8,10,3,7,28,29,9])).
% 58.64/58.76 cnf(206,plain,
% 58.64/58.76 (P1(x2061,x2062)+~E(a1,x2062)),
% 58.64/58.76 inference(scs_inference,[],[59,34,148,177,170,37,16,81,18,123,129,176,192,20,199,2,22,8,10,3,7,28,29,9,25])).
% 58.64/58.76 cnf(211,plain,
% 58.64/58.76 (E(f5(x2111,x2111),f5(a7,a3))),
% 58.64/58.76 inference(scs_inference,[],[194,2])).
% 58.64/58.76 cnf(212,plain,
% 58.64/58.76 (E(f5(a7,a3),f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[194,71,179,2,22])).
% 58.64/58.76 cnf(215,plain,
% 58.64/58.76 (P2(f5(x2151,x2151),x2152,f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[55,194,71,124,179,2,22,10])).
% 58.64/58.76 cnf(219,plain,
% 58.64/58.76 (E(f5(x2191,x2191),f5(x2192,a1))),
% 58.64/58.76 inference(scs_inference,[],[55,90,194,120,116,71,124,179,174,125,2,22,10,8,9,3])).
% 58.64/58.76 cnf(221,plain,
% 58.64/58.76 (P1(f5(a3,f5(a1,a4)),a4)),
% 58.64/58.76 inference(scs_inference,[],[55,59,90,194,120,116,71,124,15,179,154,174,125,20,2,22,10,8,9,3,7,28])).
% 58.64/58.76 cnf(222,plain,
% 58.64/58.76 (P2(x2221,x2222,f5(x2221,x2222))),
% 58.64/58.76 inference(rename_variables,[],[20])).
% 58.64/58.76 cnf(224,plain,
% 58.64/58.76 (P1(f5(f5(x2241,x2241),a2),a7)),
% 58.64/58.76 inference(scs_inference,[],[55,59,90,194,120,116,71,75,124,15,179,154,174,125,20,222,2,22,10,8,9,3,7,28,29])).
% 58.64/58.76 cnf(230,plain,
% 58.64/58.76 (E(f5(a7,f5(a7,a7)),f5(a7,a3))),
% 58.64/58.76 inference(scs_inference,[],[212,2])).
% 58.64/58.76 cnf(231,plain,
% 58.64/58.76 (E(f5(f5(a3,a2),a6),a7)),
% 58.64/58.76 inference(scs_inference,[],[212,12,102,2,22])).
% 58.64/58.76 cnf(235,plain,
% 58.64/58.76 (P1(f5(f5(a3,a2),a6),x2351)),
% 58.64/58.76 inference(scs_inference,[],[59,169,212,12,37,64,102,2,22,8,6])).
% 58.64/58.76 cnf(237,plain,
% 58.64/58.76 (P2(a7,x2371,f5(x2372,x2372))),
% 58.64/58.76 inference(scs_inference,[],[59,34,169,212,12,17,37,64,102,2,22,8,6,10])).
% 58.64/58.76 cnf(238,plain,
% 58.64/58.76 (P2(x2381,f5(f5(a3,a2),a6),x2381)),
% 58.64/58.76 inference(scs_inference,[],[59,34,169,212,12,17,37,176,64,102,2,22,8,6,10,9])).
% 58.64/58.76 cnf(240,plain,
% 58.64/58.76 (E(f5(a7,a3),f5(x2401,a1))),
% 58.64/58.76 inference(scs_inference,[],[59,34,169,212,170,120,12,17,37,176,64,102,2,22,8,6,10,9,3])).
% 58.64/58.76 cnf(241,plain,
% 58.64/58.76 (P1(f5(a3,a6),f5(a1,a3))),
% 58.64/58.76 inference(scs_inference,[],[59,34,169,212,91,170,120,12,17,37,150,176,64,102,2,22,8,6,10,9,3,7])).
% 58.64/58.76 cnf(242,plain,
% 58.64/58.76 (P1(f5(a4,a2),f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[59,34,169,212,91,170,120,75,12,17,146,37,150,176,64,102,20,2,22,8,6,10,9,3,7,28])).
% 58.64/58.76 cnf(246,plain,
% 58.64/58.76 (E(f5(a7,a7),f5(f5(a3,a7),a3))),
% 58.64/58.76 inference(scs_inference,[],[188,2])).
% 58.64/58.76 cnf(247,plain,
% 58.64/58.76 (E(f5(f5(a1,a3),f5(a4,a3)),f5(x2471,x2471))),
% 58.64/58.76 inference(scs_inference,[],[188,37,197,2,22])).
% 58.64/58.76 cnf(252,plain,
% 58.64/58.76 (E(a7,f5(a7,a3))),
% 58.64/58.76 inference(scs_inference,[],[55,230,188,240,179,37,197,2,22,6,3])).
% 58.64/58.76 cnf(257,plain,
% 58.64/58.76 (P2(f5(a7,a3),x2571,a7)),
% 58.64/58.76 inference(scs_inference,[],[55,230,211,188,240,126,179,37,176,124,197,2,22,6,3,9,10,8])).
% 58.64/58.76 cnf(259,plain,
% 58.64/58.76 (P1(f5(a6,a7),f5(a3,a4))),
% 58.64/58.76 inference(scs_inference,[],[55,230,211,188,240,142,126,179,37,162,176,124,197,2,22,6,3,9,10,8,7])).
% 58.64/58.76 cnf(260,plain,
% 58.64/58.76 (P1(f5(a7,a6),f5(a7,f5(a7,a7)))),
% 58.64/58.76 inference(scs_inference,[],[55,230,211,188,240,142,126,146,179,37,19,162,176,124,197,158,2,22,6,3,9,10,8,7,28])).
% 58.64/58.76 cnf(266,plain,
% 58.64/58.76 (E(f5(x2661,x2661),f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.76 inference(scs_inference,[],[247,2])).
% 58.64/58.76 cnf(267,plain,
% 58.64/58.76 (E(f5(f5(a3,a7),a3),f5(x2671,x2671))),
% 58.64/58.76 inference(scs_inference,[],[247,37,195,2,22])).
% 58.64/58.76 cnf(269,plain,
% 58.64/58.76 (P1(f5(x2691,x2691),x2692)),
% 58.64/58.76 inference(rename_variables,[],[37])).
% 58.64/58.76 cnf(271,plain,
% 58.64/58.76 (E(f5(f5(a3,a2),a6),f5(a7,a3))),
% 58.64/58.76 inference(scs_inference,[],[247,252,231,37,195,2,22,3])).
% 58.64/58.76 cnf(272,plain,
% 58.64/58.76 (P2(f5(f5(a3,a7),a3),x2721,a7)),
% 58.64/58.76 inference(scs_inference,[],[247,246,252,231,37,124,195,2,22,3,8])).
% 58.64/58.76 cnf(274,plain,
% 58.64/58.76 (P2(f5(a7,f5(a7,a7)),x2741,f5(x2742,x2742))),
% 58.64/58.76 inference(scs_inference,[],[34,247,246,252,231,147,37,124,195,2,22,3,8,10])).
% 58.64/58.76 cnf(275,plain,
% 58.64/58.76 (P2(x2751,f5(f5(a3,a7),a3),x2751)),
% 58.64/58.76 inference(scs_inference,[],[34,247,246,252,231,147,37,176,124,195,2,22,3,8,10,9])).
% 58.64/58.76 cnf(277,plain,
% 58.64/58.76 (P1(f5(f5(a3,a7),a3),x2771)),
% 58.64/58.76 inference(scs_inference,[],[34,247,246,252,231,147,37,269,176,124,195,2,22,3,8,10,9,6])).
% 58.64/58.76 cnf(279,plain,
% 58.64/58.76 (P1(f5(a4,a2),f5(x2791,x2791))),
% 58.64/58.76 inference(scs_inference,[],[59,34,247,246,252,231,147,37,269,176,124,195,242,2,22,3,8,10,9,6,7])).
% 58.64/58.76 cnf(280,plain,
% 58.64/58.76 (E(f5(x2801,x2801),f5(f5(a3,a7),a3))),
% 58.64/58.76 inference(scs_inference,[],[267,2])).
% 58.64/58.76 cnf(281,plain,
% 58.64/58.76 (E(f5(f5(a3,a7),a3),a7)),
% 58.64/58.76 inference(scs_inference,[],[267,12,277,2,22])).
% 58.64/58.76 cnf(285,plain,
% 58.64/58.76 (P2(f5(f5(a1,a3),f5(a4,a3)),x2851,a7)),
% 58.64/58.76 inference(scs_inference,[],[266,267,12,124,277,2,22,8])).
% 58.64/58.77 cnf(287,plain,
% 58.64/58.77 (P1(f5(f5(a1,a3),f5(a4,a3)),x2871)),
% 58.64/58.77 inference(scs_inference,[],[266,267,12,37,124,277,2,22,8,6])).
% 58.64/58.77 cnf(289,plain,
% 58.64/58.77 (P2(x2891,f5(f5(a1,a3),f5(a4,a3)),x2891)),
% 58.64/58.77 inference(scs_inference,[],[266,267,12,37,176,124,277,2,22,8,6,9])).
% 58.64/58.77 cnf(291,plain,
% 58.64/58.77 (P2(x2911,a1,f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[266,267,12,126,37,176,124,277,2,22,8,6,9,10])).
% 58.64/58.77 cnf(293,plain,
% 58.64/58.77 (E(f5(f5(a3,a2),a6),f5(x2931,a1))),
% 58.64/58.77 inference(scs_inference,[],[266,267,271,240,12,126,37,176,124,277,2,22,8,6,9,10,3])).
% 58.64/58.77 cnf(294,plain,
% 58.64/58.77 (P1(f5(a4,a2),f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[266,267,271,240,12,126,37,176,124,277,279,2,22,8,6,9,10,3,7])).
% 58.64/58.77 cnf(296,plain,
% 58.64/58.77 (E(a7,f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[266,267,271,240,16,12,126,37,176,124,277,279,2,22,8,6,9,10,3,7,27])).
% 58.64/58.77 cnf(298,plain,
% 58.64/58.77 (E(f5(x2981,a1),f5(x2982,x2982))),
% 58.64/58.77 inference(scs_inference,[],[219,2])).
% 58.64/58.77 cnf(299,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),f5(a4,a3)),a7)),
% 58.64/58.77 inference(scs_inference,[],[219,12,287,2,22])).
% 58.64/58.77 cnf(303,plain,
% 58.64/58.77 (P1(f5(x3031,a1),x3032)),
% 58.64/58.77 inference(scs_inference,[],[219,293,12,287,235,2,22,6])).
% 58.64/58.77 cnf(304,plain,
% 58.64/58.77 (E(f5(f5(a3,a7),a3),f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[219,293,281,252,12,287,235,2,22,6,3])).
% 58.64/58.77 cnf(305,plain,
% 58.64/58.77 (P2(x3051,a1,f5(f5(a3,a7),a3))),
% 58.64/58.77 inference(scs_inference,[],[280,219,293,281,252,12,126,287,235,2,22,6,3,10])).
% 58.64/58.77 cnf(308,plain,
% 58.64/58.77 (P2(f5(x3081,x3081),f5(x3082,x3082),f5(a7,a7))),
% 58.64/58.77 inference(rename_variables,[],[174])).
% 58.64/58.77 cnf(311,plain,
% 58.64/58.77 (P1(f5(a7,a6),f5(x3111,x3111))),
% 58.64/58.77 inference(scs_inference,[],[59,280,219,293,281,252,12,126,174,308,287,235,260,2,22,6,3,10,9,8,7])).
% 58.64/58.77 cnf(312,plain,
% 58.64/58.77 (E(a7,f5(f5(a3,a7),a3))),
% 58.64/58.77 inference(scs_inference,[],[59,280,219,293,281,252,16,12,126,174,308,287,235,260,2,22,6,3,10,9,8,7,27])).
% 58.64/58.77 cnf(315,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[304,294,287,2,22])).
% 58.64/58.77 cnf(318,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),f5(a4,a3)),f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[304,299,252,294,287,2,22,3])).
% 58.64/58.77 cnf(320,plain,
% 58.64/58.77 (P2(x3201,f5(a7,f5(a7,a7)),f5(x3201,a7))),
% 58.64/58.77 inference(scs_inference,[],[55,59,304,299,252,274,294,287,20,2,22,3,8,9])).
% 58.64/58.77 cnf(322,plain,
% 58.64/58.77 (P2(a3,f5(a1,a3),f5(a3,a4))),
% 58.64/58.77 inference(scs_inference,[],[55,59,304,299,252,142,97,274,294,287,20,2,22,3,8,9,10])).
% 58.64/58.77 cnf(323,plain,
% 58.64/58.77 (P1(f5(a3,f5(a1,a4)),f5(a1,a3))),
% 58.64/58.77 inference(scs_inference,[],[55,59,304,299,252,91,142,97,274,294,221,287,20,2,22,3,8,9,10,7])).
% 58.64/58.77 cnf(326,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),f5(a4,a3)),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[315,2])).
% 58.64/58.77 cnf(331,plain,
% 58.64/58.77 (P2(f5(x3311,x3311),x3312,f5(a7,x3312))),
% 58.64/58.77 inference(scs_inference,[],[34,315,37,311,20,2,22,8])).
% 58.64/58.77 cnf(333,plain,
% 58.64/58.77 (P2(f5(f5(a1,a3),f5(a4,a3)),x3331,f5(x3332,x3332))),
% 58.64/58.77 inference(scs_inference,[],[34,315,37,311,285,20,2,22,8,10])).
% 58.64/58.77 cnf(334,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[34,315,318,37,311,285,20,2,22,8,10,3])).
% 58.64/58.77 cnf(335,plain,
% 58.64/58.77 (P2(x3351,f5(x3352,x3352),f5(x3351,a7))),
% 58.64/58.77 inference(scs_inference,[],[34,59,315,318,37,311,285,320,20,2,22,8,10,3,9])).
% 58.64/58.77 cnf(340,plain,
% 58.64/58.77 (E(f5(a7,a3),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[334,2])).
% 58.64/58.77 cnf(341,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(x3411,x3411))),
% 58.64/58.77 inference(scs_inference,[],[334,279,37,2,22])).
% 58.64/58.77 cnf(345,plain,
% 58.64/58.77 (P2(x3451,a1,f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[326,334,279,291,37,2,22,10])).
% 58.64/58.77 cnf(346,plain,
% 58.64/58.77 (P2(x3461,f5(a4,a2),x3461)),
% 58.64/58.77 inference(scs_inference,[],[326,334,279,291,37,289,2,22,10,9])).
% 58.64/58.77 cnf(347,plain,
% 58.64/58.77 (P2(f5(a4,a2),x3471,a7)),
% 58.64/58.77 inference(scs_inference,[],[326,334,279,291,37,285,289,2,22,10,9,8])).
% 58.64/58.77 cnf(348,plain,
% 58.64/58.77 (E(a7,f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[326,296,334,279,291,37,285,289,2,22,10,9,8,3])).
% 58.64/58.77 cnf(349,plain,
% 58.64/58.77 (P1(f5(a4,a2),x3491)),
% 58.64/58.77 inference(scs_inference,[],[326,296,334,279,291,37,285,289,287,2,22,10,9,8,3,6])).
% 58.64/58.77 cnf(350,plain,
% 58.64/58.77 (P1(a4,x3501)+~E(a2,x3501)),
% 58.64/58.77 inference(scs_inference,[],[326,296,334,75,279,291,37,285,289,287,2,22,10,9,8,3,6,7])).
% 58.64/58.77 cnf(352,plain,
% 58.64/58.77 (E(f5(x3521,x3521),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[341,2])).
% 58.64/58.77 cnf(353,plain,
% 58.64/58.77 (E(f5(a7,f5(a7,a7)),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[341,96,345,2,27])).
% 58.64/58.77 cnf(356,plain,
% 58.64/58.77 (E(f5(a7,a6),a7)),
% 58.64/58.77 inference(scs_inference,[],[341,96,12,158,345,2,27,22])).
% 58.64/58.77 cnf(359,plain,
% 58.64/58.77 (E(f5(a7,a3),f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[341,340,315,96,12,158,345,2,27,22,3])).
% 58.64/58.77 cnf(360,plain,
% 58.64/58.77 (P2(f5(a7,f5(a7,a7)),x3601,f5(a7,x3601))),
% 58.64/58.77 inference(scs_inference,[],[55,341,340,315,96,12,158,20,345,2,27,22,3,8])).
% 58.64/58.77 cnf(370,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(a7,f5(a7,a7)))),
% 58.64/58.77 inference(scs_inference,[],[353,2])).
% 58.64/58.77 cnf(371,plain,
% 58.64/58.77 (E(a7,f5(a7,x3711))),
% 58.64/58.77 inference(scs_inference,[],[353,147,360,2,27])).
% 58.64/58.77 cnf(374,plain,
% 58.64/58.77 (E(f5(a7,a6),f5(a7,f5(a7,a7)))),
% 58.64/58.77 inference(scs_inference,[],[353,147,71,260,360,2,27,22])).
% 58.64/58.77 cnf(377,plain,
% 58.64/58.77 (P2(x3771,f5(a4,a2),f5(x3771,a7))),
% 58.64/58.77 inference(scs_inference,[],[352,353,147,71,335,260,360,2,27,22,9])).
% 58.64/58.77 cnf(380,plain,
% 58.64/58.77 (P2(f5(a7,f5(a7,a7)),x3801,f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[352,353,312,356,147,71,274,335,260,360,2,27,22,9,3,10])).
% 58.64/58.77 cnf(384,plain,
% 58.64/58.77 (P1(f5(a7,a6),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[352,353,312,356,147,71,311,274,215,335,260,360,2,27,22,9,3,10,8,7])).
% 58.64/58.77 cnf(386,plain,
% 58.64/58.77 (P1(f5(a6,f5(a1,a4)),f5(x3861,x3861))),
% 58.64/58.77 inference(scs_inference,[],[352,353,312,356,147,71,311,176,274,154,215,335,20,260,360,2,27,22,9,3,10,8,7,28])).
% 58.64/58.77 cnf(392,plain,
% 58.64/58.77 (E(f5(a4,a2),a7)),
% 58.64/58.77 inference(scs_inference,[],[348,2])).
% 58.64/58.77 cnf(393,plain,
% 58.64/58.77 (P1(f5(a3,a2),f5(a1,a4))),
% 58.64/58.77 inference(scs_inference,[],[348,78,154,2,23])).
% 58.64/58.77 cnf(395,plain,
% 58.64/58.77 (E(f5(f5(x3951,x3951),a2),a7)),
% 58.64/58.77 inference(scs_inference,[],[348,78,154,12,224,2,23,22])).
% 58.64/58.77 cnf(398,plain,
% 58.64/58.77 (P2(f5(x3981,x3981),x3982,f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[59,348,78,154,12,224,380,2,23,22,8])).
% 58.64/58.77 cnf(399,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),f5(a4,a3)),f5(a7,x3991))),
% 58.64/58.77 inference(scs_inference,[],[59,348,371,299,78,154,12,224,380,2,23,22,8,3])).
% 58.64/58.77 cnf(400,plain,
% 58.64/58.77 (P2(f5(f5(a3,a7),a3),x4001,f5(x4002,x4002))),
% 58.64/58.77 inference(scs_inference,[],[34,59,348,371,299,78,154,272,12,224,380,2,23,22,8,3,10])).
% 58.64/58.77 cnf(402,plain,
% 58.64/58.77 (P1(f5(f5(a1,a3),a2),f5(x4021,x4021))),
% 58.64/58.77 inference(scs_inference,[],[34,59,348,371,299,78,154,95,176,272,12,224,20,380,2,23,22,8,3,10,7,28])).
% 58.64/58.77 cnf(406,plain,
% 58.64/58.77 (P2(x4061,x4062,f5(x4063,x4063))+~E(a1,x4062)),
% 58.64/58.77 inference(scs_inference,[],[34,59,348,371,299,126,78,154,95,176,272,12,224,20,380,2,23,22,8,3,10,7,28,9])).
% 58.64/58.77 cnf(410,plain,
% 58.64/58.77 (E(f5(a7,x4101),f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[399,2])).
% 58.64/58.77 cnf(413,plain,
% 58.64/58.77 (E(f5(a7,a6),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[399,158,12,349,384,2,23,22])).
% 58.64/58.77 cnf(416,plain,
% 58.64/58.77 (P1(f5(a7,x4161),x4162)),
% 58.64/58.77 inference(scs_inference,[],[399,158,12,287,349,384,2,23,22,6])).
% 58.64/58.77 cnf(417,plain,
% 58.64/58.77 (P2(x4171,f5(a7,x4172),x4171)),
% 58.64/58.77 inference(scs_inference,[],[399,158,12,287,349,289,384,2,23,22,6,9])).
% 58.64/58.77 cnf(418,plain,
% 58.64/58.77 (P2(f5(a7,x4181),x4182,a7)),
% 58.64/58.77 inference(scs_inference,[],[399,158,285,12,287,349,289,384,2,23,22,6,9,8])).
% 58.64/58.77 cnf(420,plain,
% 58.64/58.77 (E(f5(a7,a3),f5(a7,x4201))),
% 58.64/58.77 inference(scs_inference,[],[34,359,399,158,257,285,12,287,349,289,384,2,23,22,6,9,8,10,3])).
% 58.64/58.77 cnf(421,plain,
% 58.64/58.77 (P1(f5(a4,f5(a4,a3)),a7)),
% 58.64/58.77 inference(scs_inference,[],[34,359,399,158,106,257,285,19,12,287,349,289,384,20,2,23,22,6,9,8,10,3,28])).
% 58.64/58.77 cnf(427,plain,
% 58.64/58.77 (E(f5(a7,f5(a7,a7)),f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[374,2])).
% 58.64/58.77 cnf(428,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),a2),f5(x4281,x4281))),
% 58.64/58.77 inference(scs_inference,[],[374,37,402,2,22])).
% 58.64/58.77 cnf(432,plain,
% 58.64/58.77 (P2(f5(a4,a2),x4321,f5(x4322,x4322))),
% 58.64/58.77 inference(scs_inference,[],[34,374,347,37,402,2,22,10])).
% 58.64/58.77 cnf(433,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(f5(a3,a7),a3))),
% 58.64/58.77 inference(scs_inference,[],[34,374,392,312,347,37,402,2,22,10,3])).
% 58.64/58.77 cnf(434,plain,
% 58.64/58.77 (P1(f5(a4,f5(a4,a3)),f5(x4341,x4341))),
% 58.64/58.77 inference(scs_inference,[],[34,374,392,312,347,37,402,421,2,22,10,3,7])).
% 58.64/58.77 cnf(435,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),a4),f5(x4351,x4351))),
% 58.64/58.77 inference(scs_inference,[],[34,374,392,312,176,150,347,37,20,402,421,2,22,10,3,7,28])).
% 58.64/58.77 cnf(448,plain,
% 58.64/58.77 (E(f5(f5(a3,a7),a3),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[433,2])).
% 58.64/58.77 cnf(449,plain,
% 58.64/58.77 (E(f5(a6,f5(a1,a4)),f5(x4491,x4491))),
% 58.64/58.77 inference(scs_inference,[],[433,37,386,2,22])).
% 58.64/58.77 cnf(453,plain,
% 58.64/58.77 (P2(x4531,f5(f5(a3,a7),a3),f5(x4531,a7))),
% 58.64/58.77 inference(scs_inference,[],[433,37,377,386,2,22,9])).
% 58.64/58.77 cnf(454,plain,
% 58.64/58.77 (E(f5(f5(x4541,x4541),a2),f5(x4542,x4542))),
% 58.64/58.77 inference(scs_inference,[],[34,433,395,37,377,386,2,22,9,3])).
% 58.64/58.77 cnf(455,plain,
% 58.64/58.77 (P2(a7,f5(x4551,x4551),f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[34,433,410,395,37,335,377,386,2,22,9,3,10])).
% 58.64/58.77 cnf(463,plain,
% 58.64/58.77 (P2(f5(x4631,x4631),f5(x4632,x4632),f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[34,433,410,395,95,19,180,37,335,377,20,386,2,22,9,3,10,28,6,8])).
% 58.64/58.77 cnf(468,plain,
% 58.64/58.77 (E(f5(x4681,x4681),f5(f5(a1,a3),a2))),
% 58.64/58.77 inference(scs_inference,[],[428,2])).
% 58.64/58.77 cnf(469,plain,
% 58.64/58.77 (E(f5(a4,f5(a4,a3)),f5(x4691,x4691))),
% 58.64/58.77 inference(scs_inference,[],[428,37,434,2,22])).
% 58.64/58.77 cnf(473,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[428,370,427,37,434,2,22,3])).
% 58.64/58.77 cnf(474,plain,
% 58.64/58.77 (P2(f5(a7,x4741),x4742,f5(x4743,x4743))),
% 58.64/58.77 inference(scs_inference,[],[34,428,370,427,37,418,434,2,22,3,10])).
% 58.64/58.77 cnf(475,plain,
% 58.64/58.77 (P1(f5(f5(a6,a7),a6),f5(x4751,x4751))),
% 58.64/58.77 inference(scs_inference,[],[34,428,370,427,176,162,37,418,20,434,2,22,3,10,28])).
% 58.64/58.77 cnf(489,plain,
% 58.64/58.77 (E(f5(x4891,x4891),f5(a4,f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[469,2])).
% 58.64/58.77 cnf(490,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),a4),f5(x4901,x4901))),
% 58.64/58.77 inference(scs_inference,[],[469,37,435,2,22])).
% 58.64/58.77 cnf(492,plain,
% 58.64/58.77 (P1(f5(x4921,x4921),x4922)),
% 58.64/58.77 inference(rename_variables,[],[37])).
% 58.64/58.77 cnf(500,plain,
% 58.64/58.77 (P2(x5001,f5(f5(a1,a3),a2),x5001)),
% 58.64/58.77 inference(scs_inference,[],[468,469,124,126,176,37,492,435,2,22,6,8,10,9])).
% 58.64/58.77 cnf(502,plain,
% 58.64/58.77 (E(f5(f5(a3,a7),a3),f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[448,468,469,473,124,126,176,37,492,435,2,22,6,8,10,9,3])).
% 58.64/58.77 cnf(507,plain,
% 58.64/58.77 (E(a7,f5(f5(a1,a3),a2))),
% 58.64/58.77 inference(scs_inference,[],[448,468,469,473,17,124,126,19,176,150,37,492,20,435,2,22,6,8,10,9,3,28,27])).
% 58.64/58.77 cnf(510,plain,
% 58.64/58.77 (P1(f5(a1,a3),x5101)+~E(a2,x5101)),
% 58.64/58.77 inference(scs_inference,[],[448,468,469,473,17,124,126,19,95,176,150,37,492,20,435,2,22,6,8,10,9,3,28,27,7])).
% 58.64/58.77 cnf(512,plain,
% 58.64/58.77 (E(f5(x5121,x5121),f5(f5(a3,a6),a4))),
% 58.64/58.77 inference(scs_inference,[],[490,2])).
% 58.64/58.77 cnf(513,plain,
% 58.64/58.77 (E(f5(a4,f5(a4,a3)),a7)),
% 58.64/58.77 inference(scs_inference,[],[490,12,421,2,22])).
% 58.64/58.77 cnf(520,plain,
% 58.64/58.77 (E(f5(a7,a6),f5(f5(a1,a3),a2))),
% 58.64/58.77 inference(scs_inference,[],[489,490,507,356,124,12,37,421,2,22,6,8,3])).
% 58.64/58.77 cnf(521,plain,
% 58.64/58.77 (P2(x5211,f5(a4,f5(a4,a3)),x5211)),
% 58.64/58.77 inference(scs_inference,[],[489,490,507,356,124,176,12,37,421,2,22,6,8,3,9])).
% 58.64/58.77 cnf(525,plain,
% 58.64/58.77 (P1(f5(f5(a6,a7),a6),a7)),
% 58.64/58.77 inference(scs_inference,[],[489,490,507,356,124,126,19,162,176,12,37,20,421,2,22,6,8,3,9,10,28])).
% 58.64/58.77 cnf(532,plain,
% 58.64/58.77 (P1(f5(a1,a3),x5321)+~E(f5(a4,a3),x5321)),
% 58.64/58.77 inference(scs_inference,[],[489,490,507,356,17,124,126,123,19,162,176,12,37,20,421,2,22,6,8,3,9,10,28,27,7])).
% 58.64/58.77 cnf(534,plain,
% 58.64/58.77 (E(f5(x5341,x5341),f5(a6,f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[449,2])).
% 58.64/58.77 cnf(535,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),a6),f5(x5351,x5351))),
% 58.64/58.77 inference(scs_inference,[],[449,37,475,2,22])).
% 58.64/58.77 cnf(537,plain,
% 58.64/58.77 (P1(f5(x5371,x5371),x5372)),
% 58.64/58.77 inference(rename_variables,[],[37])).
% 58.64/58.77 cnf(541,plain,
% 58.64/58.77 (P2(f5(f5(a3,a6),a4),x5411,a7)),
% 58.64/58.77 inference(scs_inference,[],[512,449,124,37,537,475,2,22,6,8])).
% 58.64/58.77 cnf(543,plain,
% 58.64/58.77 (P2(a7,x5431,f5(f5(a3,a6),a4))),
% 58.64/58.77 inference(scs_inference,[],[512,449,124,237,37,537,475,2,22,6,8,10])).
% 58.64/58.77 cnf(545,plain,
% 58.64/58.77 (P2(x5451,f5(f5(a3,a6),a4),x5451)),
% 58.64/58.77 inference(scs_inference,[],[512,449,124,237,176,37,537,475,2,22,6,8,10,9])).
% 58.64/58.77 cnf(547,plain,
% 58.64/58.77 (E(f5(a7,a3),f5(f5(a1,a3),a2))),
% 58.64/58.77 inference(scs_inference,[],[512,449,420,520,124,237,176,37,537,475,2,22,6,8,10,9,3])).
% 58.64/58.77 cnf(549,plain,
% 58.64/58.77 (P1(f5(f5(a3,a4),f5(a1,a4)),a7)),
% 58.64/58.77 inference(scs_inference,[],[512,449,420,520,124,237,19,176,175,37,537,20,475,2,22,6,8,10,9,3,28])).
% 58.64/58.77 cnf(553,plain,
% 58.64/58.77 (E(a7,f5(f5(a3,a6),a4))),
% 58.64/58.77 inference(scs_inference,[],[512,449,420,520,16,124,237,19,176,175,37,537,20,475,2,22,6,8,10,9,3,28,27])).
% 58.64/58.77 cnf(558,plain,
% 58.64/58.77 (E(f5(x5581,x5581),f5(f5(a6,a7),a6))),
% 58.64/58.77 inference(scs_inference,[],[535,2])).
% 58.64/58.77 cnf(559,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),a6),a7)),
% 58.64/58.77 inference(scs_inference,[],[535,12,525,2,22])).
% 58.64/58.77 cnf(562,plain,
% 58.64/58.77 (P2(f5(a6,f5(a1,a4)),x5621,a7)),
% 58.64/58.77 inference(scs_inference,[],[535,534,124,12,525,2,22,8])).
% 58.64/58.77 cnf(564,plain,
% 58.64/58.77 (P1(f5(f5(a3,a4),f5(a1,a4)),f5(x5641,x5641))),
% 58.64/58.77 inference(scs_inference,[],[34,535,534,124,12,525,549,2,22,8,7])).
% 58.64/58.77 cnf(567,plain,
% 58.64/58.77 (E(f5(a4,f5(a4,a3)),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[34,535,534,513,348,124,12,37,525,549,2,22,8,7,6,3])).
% 58.64/58.77 cnf(568,plain,
% 58.64/58.77 (P2(x5681,f5(a6,f5(a1,a4)),x5681)),
% 58.64/58.77 inference(scs_inference,[],[34,535,534,513,348,124,176,12,37,525,549,2,22,8,7,6,3,9])).
% 58.64/58.77 cnf(572,plain,
% 58.64/58.77 (P1(f5(f5(a3,a2),f5(a3,a4)),f5(a7,x5721))),
% 58.64/58.77 inference(scs_inference,[],[34,535,534,513,348,124,126,417,176,149,12,37,20,525,549,2,22,8,7,6,3,9,10,28])).
% 58.64/58.77 cnf(576,plain,
% 58.64/58.77 (E(a7,f5(a6,f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[34,535,534,513,348,272,124,126,417,176,149,12,37,20,525,549,2,22,8,7,6,3,9,10,28,27])).
% 58.64/58.77 cnf(579,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(a4,f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[567,2])).
% 58.64/58.77 cnf(580,plain,
% 58.64/58.77 (E(f5(f5(a3,a4),f5(a1,a4)),f5(x5801,x5801))),
% 58.64/58.77 inference(scs_inference,[],[567,37,564,2,22])).
% 58.64/58.77 cnf(584,plain,
% 58.64/58.77 (P1(f5(f5(a3,a2),f5(a3,a4)),f5(x5841,x5841))),
% 58.64/58.77 inference(scs_inference,[],[59,567,37,564,572,2,22,7])).
% 58.64/58.77 cnf(590,plain,
% 58.64/58.77 (E(f5(x5901,a1),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[59,567,558,187,353,124,176,37,564,572,2,22,7,9,8,3])).
% 58.64/58.77 cnf(602,plain,
% 58.64/58.77 (E(f5(x6021,x6021),f5(f5(a3,a4),f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[580,2])).
% 58.64/58.77 cnf(603,plain,
% 58.64/58.77 (E(f5(f5(a3,a2),f5(a3,a4)),f5(x6031,x6031))),
% 58.64/58.77 inference(scs_inference,[],[580,37,584,2,22])).
% 58.64/58.77 cnf(609,plain,
% 58.64/58.77 (P2(f5(a4,f5(a4,a3)),x6091,f5(x6092,x6092))),
% 58.64/58.77 inference(scs_inference,[],[580,579,590,377,432,37,584,2,22,9,3,8])).
% 58.64/58.77 cnf(611,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),f5(a1,a3)),f5(a7,x6111))),
% 58.64/58.77 inference(scs_inference,[],[580,579,590,502,305,417,377,432,241,37,20,584,2,22,9,3,8,10,28])).
% 58.64/58.77 cnf(615,plain,
% 58.64/58.77 (P1(f5(a1,f5(a4,a3)),x6151)+~E(a3,x6151)),
% 58.64/58.77 inference(scs_inference,[],[580,579,590,502,305,417,180,377,432,241,37,20,584,2,22,9,3,8,10,28,7])).
% 58.64/58.77 cnf(619,plain,
% 58.64/58.77 (E(f5(x6191,x6191),f5(f5(a3,a2),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[603,2])).
% 58.64/58.77 cnf(623,plain,
% 58.64/58.77 (E(f5(a7,a6),f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[603,413,334,12,549,2,22,3])).
% 58.64/58.77 cnf(624,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),f5(a1,a3)),f5(x6241,x6241))),
% 58.64/58.77 inference(scs_inference,[],[59,603,413,334,12,549,611,2,22,3,7])).
% 58.64/58.77 cnf(630,plain,
% 58.64/58.77 (P2(f5(f5(a3,a4),f5(a1,a4)),x6301,a7)),
% 58.64/58.77 inference(scs_inference,[],[59,602,603,413,334,124,176,12,37,549,611,2,22,3,7,9,6,8])).
% 58.64/58.77 cnf(641,plain,
% 58.64/58.77 (P2(f5(a1,a3),a2,a7)),
% 58.64/58.77 inference(scs_inference,[],[75,91,24,6])).
% 58.64/58.77 cnf(643,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),f5(a1,a3)),f5(x6431,x6431))),
% 58.64/58.77 inference(scs_inference,[],[553,37,624,2,22])).
% 58.64/58.77 cnf(645,plain,
% 58.64/58.77 (P1(f5(x6451,x6451),x6452)),
% 58.64/58.77 inference(rename_variables,[],[37])).
% 58.64/58.77 cnf(647,plain,
% 58.64/58.77 (P2(f5(f5(a3,a2),f5(a3,a4)),x6471,a7)),
% 58.64/58.77 inference(scs_inference,[],[619,553,124,37,624,2,22,8])).
% 58.64/58.77 cnf(651,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(x6511,a1))),
% 58.64/58.77 inference(scs_inference,[],[619,553,370,177,124,37,645,624,2,22,8,6,3])).
% 58.64/58.77 cnf(652,plain,
% 58.64/58.77 (P2(x6521,f5(f5(a3,a2),f5(a3,a4)),x6521)),
% 58.64/58.77 inference(scs_inference,[],[619,553,370,177,124,176,37,645,624,2,22,8,6,3,9])).
% 58.64/58.77 cnf(656,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),f5(a1,a3)),a7)),
% 58.64/58.77 inference(scs_inference,[],[619,553,370,177,124,126,19,176,241,37,645,20,624,2,22,8,6,3,9,10,28])).
% 58.64/58.77 cnf(660,plain,
% 58.64/58.77 (E(a7,f5(f5(a3,a2),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[619,553,370,177,272,124,126,19,176,241,37,645,20,624,2,22,8,6,3,9,10,28,27])).
% 58.64/58.77 cnf(665,plain,
% 58.64/58.77 (E(f5(x6651,x6651),f5(f5(a3,a6),f5(a1,a3)))),
% 58.64/58.77 inference(scs_inference,[],[643,2])).
% 58.64/58.77 cnf(669,plain,
% 58.64/58.77 (P2(f5(a7,f5(a7,a7)),x6691,f5(x6692,a1))),
% 58.64/58.77 inference(scs_inference,[],[643,651,380,12,656,2,22,10])).
% 58.64/58.77 cnf(670,plain,
% 58.64/58.77 (P2(x6701,f5(x6702,a1),x6701)),
% 58.64/58.77 inference(scs_inference,[],[643,651,380,346,12,656,2,22,10,9])).
% 58.64/58.77 cnf(671,plain,
% 58.64/58.77 (E(f5(f5(a3,a7),a3),f5(x6711,a1))),
% 58.64/58.77 inference(scs_inference,[],[643,651,448,380,346,12,656,2,22,10,9,3])).
% 58.64/58.77 cnf(672,plain,
% 58.64/58.77 (P2(f5(x6721,a1),x6722,a7)),
% 58.64/58.77 inference(scs_inference,[],[643,651,448,347,380,346,12,656,2,22,10,9,3,8])).
% 58.64/58.77 cnf(673,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),f5(a1,a3)),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[643,651,448,347,380,346,241,12,20,656,2,22,10,9,3,8,28])).
% 58.64/58.77 cnf(682,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),f5(a1,a3)),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[576,349,673,2,22])).
% 58.64/58.77 cnf(685,plain,
% 58.64/58.77 (P2(x6851,f5(f5(a3,a6),f5(a1,a3)),x6851)),
% 58.64/58.77 inference(scs_inference,[],[665,576,176,349,673,2,22,9])).
% 58.64/58.77 cnf(691,plain,
% 58.64/58.77 (E(f5(a4,f5(a4,a3)),f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[665,576,567,473,124,176,37,349,673,2,22,9,6,8,3])).
% 58.64/58.77 cnf(694,plain,
% 58.64/58.77 (P1(f5(f5(x6941,x6941),a2),f5(a7,x6942))),
% 58.64/58.77 inference(scs_inference,[],[665,576,567,473,124,237,417,19,176,224,37,349,673,2,22,9,6,8,3,10,28])).
% 58.64/58.77 cnf(703,plain,
% 58.64/58.77 (P1(f5(a3,a6),a2)),
% 58.64/58.77 inference(scs_inference,[],[682,75,150,2,23])).
% 58.64/58.77 cnf(706,plain,
% 58.64/58.77 (E(f5(a4,f5(a4,a3)),f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[682,671,691,623,75,305,150,2,23,10,3])).
% 58.64/58.77 cnf(707,plain,
% 58.64/58.77 (P2(f5(x7071,a1),x7072,f5(x7073,x7073))),
% 58.64/58.77 inference(scs_inference,[],[682,671,691,623,75,305,150,400,2,23,10,3,8])).
% 58.64/58.77 cnf(708,plain,
% 58.64/58.77 (P2(x7081,f5(x7082,a1),f5(x7081,a7))),
% 58.64/58.77 inference(scs_inference,[],[682,671,691,623,75,305,150,400,453,2,23,10,3,8,9])).
% 58.64/58.77 cnf(716,plain,
% 58.64/58.77 (P1(f5(a3,a6),f5(a4,a3))),
% 58.64/58.77 inference(scs_inference,[],[660,106,150,2,23])).
% 58.64/58.77 cnf(718,plain,
% 58.64/58.77 (E(f5(x7181,x7181),f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[660,90,427,106,150,2,23,3])).
% 58.64/58.77 cnf(728,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),a2),f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[547,2])).
% 58.64/58.77 cnf(730,plain,
% 58.64/58.77 (P2(a7,f5(a7,f5(a7,a7)),f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[547,718,304,320,453,2,9,10])).
% 58.64/58.77 cnf(733,plain,
% 58.64/58.77 (P2(f5(x7331,x7331),x7332,f5(f5(a3,a6),a4))),
% 58.64/58.77 inference(scs_inference,[],[34,547,718,304,320,453,543,2,9,10,8])).
% 58.64/58.77 cnf(734,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),a6),f5(a7,x7341))),
% 58.64/58.77 inference(scs_inference,[],[34,547,718,559,304,371,320,453,543,2,9,10,8,3])).
% 58.64/58.77 cnf(735,plain,
% 58.64/58.77 (P1(f5(f5(a3,a2),f5(a1,a4)),f5(a7,x7351))),
% 58.64/58.77 inference(scs_inference,[],[34,547,718,559,304,371,320,417,453,393,543,20,2,9,10,8,3,28])).
% 58.64/58.77 cnf(739,plain,
% 58.64/58.77 (E(a4,f5(a4,a3))+~P1(f5(a4,a3),a4)),
% 58.64/58.77 inference(scs_inference,[],[34,547,718,559,304,371,106,320,417,453,393,543,20,2,9,10,8,3,28,22])).
% 58.64/58.77 cnf(741,plain,
% 58.64/58.77 (P1(f5(f5(a3,a2),f5(a1,a4)),f5(x7411,x7411))),
% 58.64/58.77 inference(scs_inference,[],[59,34,547,718,559,304,371,106,320,417,453,393,543,20,2,9,10,8,3,28,22,7])).
% 58.64/58.77 cnf(745,plain,
% 58.64/58.77 (E(f5(f5(a3,a2),f5(a1,a4)),f5(x7451,x7451))),
% 58.64/58.77 inference(scs_inference,[],[706,37,741,2,22])).
% 58.64/58.77 cnf(750,plain,
% 58.64/58.77 (P2(f5(x7501,x7501),x7502,f5(x7503,a1))),
% 58.64/58.77 inference(scs_inference,[],[59,706,37,669,741,730,2,22,9,8])).
% 58.64/58.77 cnf(751,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),a6),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[59,706,734,413,37,669,741,730,2,22,9,8,3])).
% 58.64/58.77 cnf(753,plain,
% 58.64/58.77 (P2(a7,f5(a7,f5(a7,a7)),f5(x7531,a1))),
% 58.64/58.77 inference(scs_inference,[],[59,706,734,413,219,320,37,669,741,730,2,22,9,8,3,10])).
% 58.64/58.77 cnf(756,plain,
% 58.64/58.77 (P1(f5(f5(a6,a7),f5(a3,a4)),f5(x7561,x7561))),
% 58.64/58.77 inference(scs_inference,[],[59,706,734,413,219,176,320,259,37,669,20,741,730,2,22,9,8,3,10,28])).
% 58.64/58.77 cnf(764,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(f5(a6,a7),a6))),
% 58.64/58.77 inference(scs_inference,[],[751,2])).
% 58.64/58.77 cnf(765,plain,
% 58.64/58.77 (E(f5(f5(x7651,x7651),a2),f5(a7,a1))),
% 58.64/58.77 inference(scs_inference,[],[751,303,694,2,22])).
% 58.64/58.77 cnf(774,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),a2),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[59,34,751,728,340,410,377,303,694,730,753,2,22,9,10,8,3])).
% 58.64/58.77 cnf(778,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(f5(a1,a3),a2))),
% 58.64/58.77 inference(scs_inference,[],[774,2])).
% 58.64/58.77 cnf(779,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),f5(a3,a4)),f5(x7791,x7791))),
% 58.64/58.77 inference(scs_inference,[],[774,37,756,2,22])).
% 58.64/58.77 cnf(783,plain,
% 58.64/58.77 (E(f5(a4,a2),f5(a7,x7831))),
% 58.64/58.77 inference(scs_inference,[],[774,764,734,37,756,2,22,3])).
% 58.64/58.77 cnf(785,plain,
% 58.64/58.77 (P2(f5(x7851,x7851),x7852,f5(f5(a6,a7),a6))),
% 58.64/58.77 inference(scs_inference,[],[774,764,734,398,377,37,756,2,22,3,9,10])).
% 58.64/58.77 cnf(788,plain,
% 58.64/58.77 (P1(x7881,x7882)+~E(f5(a4,a3),x7882)+~E(f5(a3,a6),x7881)),
% 58.64/58.77 inference(scs_inference,[],[774,764,734,398,432,377,37,716,756,2,22,3,9,10,8,7,6])).
% 58.64/58.77 cnf(790,plain,
% 58.64/58.77 (E(f5(x7901,x7901),f5(f5(a6,a7),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[779,2])).
% 58.64/58.77 cnf(791,plain,
% 58.64/58.77 (E(f5(f5(a3,a2),f5(a1,a4)),f5(a7,a1))),
% 58.64/58.77 inference(scs_inference,[],[779,303,735,2,22])).
% 58.64/58.77 cnf(796,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),a2),f5(a7,x7961))),
% 58.64/58.77 inference(scs_inference,[],[778,779,783,774,432,303,735,2,22,8,3])).
% 58.64/58.77 cnf(798,plain,
% 58.64/58.77 (P2(f5(x7981,x7981),x7982,f5(f5(a1,a3),a2))),
% 58.64/58.77 inference(scs_inference,[],[778,779,783,774,398,432,377,303,735,2,22,8,3,9,10])).
% 58.64/58.77 cnf(799,plain,
% 58.64/58.77 (P1(f5(f5(a6,a7),f5(a3,a4)),f5(a7,x7991))),
% 58.64/58.77 inference(scs_inference,[],[778,779,783,774,398,417,259,432,377,303,20,735,2,22,8,3,9,10,28])).
% 58.64/58.77 cnf(803,plain,
% 58.64/58.77 (E(f5(x8031,x8031),f5(f5(a3,a2),f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[745,2])).
% 58.64/58.77 cnf(804,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),f5(a3,a4)),f5(a7,a1))),
% 58.64/58.77 inference(scs_inference,[],[745,303,799,2,22])).
% 58.64/58.77 cnf(806,plain,
% 58.64/58.77 (P1(f5(x8061,a1),x8062)),
% 58.64/58.77 inference(rename_variables,[],[303])).
% 58.64/58.77 cnf(810,plain,
% 58.64/58.77 (E(f5(x8101,x8101),f5(f5(a6,a7),f5(a3,a4)))),
% 58.64/58.77 inference(rename_variables,[],[790])).
% 58.64/58.77 cnf(815,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),f5(a1,a3)),f5(a7,x8151))),
% 58.64/58.77 inference(scs_inference,[],[790,810,745,682,783,124,193,303,806,799,2,22,6,10,8,3])).
% 58.64/58.77 cnf(818,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),a2),f5(a7,x8181))),
% 58.64/58.77 inference(scs_inference,[],[790,810,745,682,783,124,193,417,176,303,806,703,20,799,2,22,6,10,8,3,9,28])).
% 58.64/58.77 cnf(822,plain,
% 58.64/58.77 (E(a7,f5(f5(a6,a7),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[790,810,745,682,783,285,124,193,417,176,303,806,703,20,799,2,22,6,10,8,3,9,28,27])).
% 58.64/58.77 cnf(825,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),a2),f5(x8251,x8251))),
% 58.64/58.77 inference(scs_inference,[],[59,790,810,745,682,783,285,124,193,417,176,303,806,703,20,799,2,22,6,10,8,3,9,28,27,7])).
% 58.64/58.77 cnf(826,plain,
% 58.64/58.77 (E(f5(a7,a1),f5(f5(a6,a7),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[804,2])).
% 58.64/58.77 cnf(829,plain,
% 58.64/58.77 (P1(f5(x8291,a1),x8292)),
% 58.64/58.77 inference(rename_variables,[],[303])).
% 58.64/58.77 cnf(833,plain,
% 58.64/58.77 (E(f5(x8331,x8331),f5(f5(a3,a2),f5(a1,a4)))),
% 58.64/58.77 inference(rename_variables,[],[803])).
% 58.64/58.77 cnf(840,plain,
% 58.64/58.77 (P2(x8401,f5(f5(a3,a2),f5(a1,a4)),x8401)),
% 58.64/58.77 inference(scs_inference,[],[803,833,804,796,356,124,193,176,303,829,825,2,22,6,3,10,8,9])).
% 58.64/58.77 cnf(842,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),f5(a4,a3)),f5(a7,x8421))),
% 58.64/58.77 inference(scs_inference,[],[803,833,804,796,356,124,193,417,176,303,829,716,20,825,2,22,6,3,10,8,9,28])).
% 58.64/58.77 cnf(846,plain,
% 58.64/58.77 (E(a7,f5(f5(a3,a2),f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[803,833,804,796,356,285,124,193,417,176,303,829,716,20,825,2,22,6,3,10,8,9,28,27])).
% 58.64/58.77 cnf(849,plain,
% 58.64/58.77 (P1(f5(f5(a3,a6),f5(a4,a3)),f5(x8491,x8491))),
% 58.64/58.77 inference(scs_inference,[],[59,803,833,804,796,356,285,124,193,417,176,303,829,716,20,825,2,22,6,3,10,8,9,28,27,7])).
% 58.64/58.77 cnf(850,plain,
% 58.64/58.77 (E(f5(a7,a1),f5(f5(a3,a2),f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[791,2])).
% 58.64/58.77 cnf(851,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),f5(a4,a3)),f5(a1,a1))),
% 58.64/58.77 inference(scs_inference,[],[791,303,849,2,22])).
% 58.64/58.77 cnf(859,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),f5(a1,a3)),f5(x8591,a1))),
% 58.64/58.77 inference(scs_inference,[],[826,791,815,177,303,707,708,849,2,22,8,9,3])).
% 58.64/58.77 cnf(864,plain,
% 58.64/58.77 (E(f5(a1,a1),f5(f5(a3,a6),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[851,2])).
% 58.64/58.77 cnf(867,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),a2),f5(a7,a1))),
% 58.64/58.77 inference(scs_inference,[],[851,95,323,303,818,2,23,22])).
% 58.64/58.77 cnf(871,plain,
% 58.64/58.77 (P2(a7,f5(x8711,x8711),f5(f5(a3,a2),f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[851,803,95,323,335,303,818,2,23,22,10])).
% 58.64/58.77 cnf(878,plain,
% 58.64/58.77 (E(f5(a7,a6),f5(x8781,a1))),
% 58.64/58.77 inference(scs_inference,[],[850,851,803,374,177,95,323,335,303,707,708,818,2,23,22,10,8,9,3])).
% 58.64/58.77 cnf(883,plain,
% 58.64/58.77 (E(f5(a7,a1),f5(f5(a3,a6),a2))),
% 58.64/58.77 inference(scs_inference,[],[867,2])).
% 58.64/58.77 cnf(884,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),f5(a4,a3)),f5(a7,a7))),
% 58.64/58.77 inference(scs_inference,[],[867,37,842,2,22])).
% 58.64/58.77 cnf(886,plain,
% 58.64/58.77 (P1(f5(x8861,x8861),x8862)),
% 58.64/58.77 inference(rename_variables,[],[37])).
% 58.64/58.77 cnf(892,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),a6),f5(x8921,a1))),
% 58.64/58.77 inference(scs_inference,[],[867,864,751,651,176,37,886,842,2,22,6,9,3])).
% 58.64/58.77 cnf(897,plain,
% 58.64/58.77 (E(a7,f5(f5(a3,a6),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[867,864,751,651,285,124,193,176,37,886,842,2,22,6,9,3,8,10,27])).
% 58.64/58.77 cnf(900,plain,
% 58.64/58.77 (E(a4,f5(a4,a3))),
% 58.64/58.77 inference(scs_inference,[],[20,26,739])).
% 58.64/58.77 cnf(901,plain,
% 58.64/58.77 (E(f5(a7,a7),f5(f5(a3,a6),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[884,2])).
% 58.64/58.77 cnf(902,plain,
% 58.64/58.77 (E(f5(f5(a3,a6),a2),f5(x9021,x9021))),
% 58.64/58.77 inference(scs_inference,[],[884,37,825,2,22])).
% 58.64/58.77 cnf(908,plain,
% 58.64/58.77 (P2(f5(f5(a3,a6),a2),x9081,a7)),
% 58.64/58.77 inference(scs_inference,[],[884,883,900,75,221,37,672,825,2,22,7,6,8])).
% 58.64/58.77 cnf(910,plain,
% 58.64/58.77 (P2(a1,a3,f5(a4,a3))),
% 58.64/58.77 inference(scs_inference,[],[884,883,900,75,221,14,37,672,825,2,22,7,6,8,10])).
% 58.64/58.77 cnf(911,plain,
% 58.64/58.77 (P2(a3,f5(a4,a3),a6)),
% 58.64/58.77 inference(scs_inference,[],[884,883,900,75,221,15,14,37,672,825,2,22,7,6,8,10,9])).
% 58.64/58.77 cnf(912,plain,
% 58.64/58.77 (E(f5(x9121,a1),a7)),
% 58.64/58.77 inference(scs_inference,[],[884,883,900,392,590,75,221,15,14,37,672,825,2,22,7,6,8,10,9,3])).
% 58.64/58.77 cnf(913,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a2),f5(a7,x9131))),
% 58.64/58.77 inference(scs_inference,[],[884,883,900,392,590,75,221,417,15,14,37,672,20,825,2,22,7,6,8,10,9,3,28])).
% 58.64/58.77 cnf(919,plain,
% 58.64/58.77 (E(f5(x9191,x9191),f5(f5(a3,a6),a2))),
% 58.64/58.77 inference(scs_inference,[],[902,2])).
% 58.64/58.77 cnf(921,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a2),f5(a7,x9211))),
% 58.64/58.77 inference(rename_variables,[],[913])).
% 58.64/58.77 cnf(924,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a2),f5(x9241,x9241))),
% 58.64/58.77 inference(scs_inference,[],[59,902,37,913,921,2,22,7])).
% 58.64/58.77 cnf(928,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),a2),f5(x9281,a1))),
% 58.64/58.77 inference(scs_inference,[],[59,902,901,796,177,126,37,913,921,2,22,7,10,3])).
% 58.64/58.77 cnf(942,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),f5(a3,a4)),a7)),
% 58.64/58.77 inference(scs_inference,[],[822,2])).
% 58.64/58.77 cnf(943,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),a2),f5(x9431,x9431))),
% 58.64/58.77 inference(scs_inference,[],[822,37,924,2,22])).
% 58.64/58.77 cnf(947,plain,
% 58.64/58.77 (P2(f5(f5(a3,a6),a2),x9471,f5(a7,x9471))),
% 58.64/58.77 inference(scs_inference,[],[919,822,331,37,924,2,22,8])).
% 58.64/58.77 cnf(951,plain,
% 58.64/58.77 (P2(x9511,x9511,f5(f5(a3,a6),a2))),
% 58.64/58.77 inference(scs_inference,[],[919,822,193,331,176,37,924,2,22,8,9,10])).
% 58.64/58.77 cnf(967,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a2),a7)),
% 58.64/58.77 inference(scs_inference,[],[859,912,303,913,924,2,22,7])).
% 58.64/58.77 cnf(969,plain,
% 58.64/58.77 (E(f5(x9691,a1),a7)),
% 58.64/58.77 inference(rename_variables,[],[912])).
% 58.64/58.77 cnf(970,plain,
% 58.64/58.77 (P2(a7,x9701,f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[859,912,969,398,303,913,924,2,22,7,8])).
% 58.64/58.77 cnf(981,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),a2),a7)),
% 58.64/58.77 inference(scs_inference,[],[892,12,967,2,22])).
% 58.64/58.77 cnf(985,plain,
% 58.64/58.77 (E(f5(f5(a3,a7),a3),f5(a7,x9851))),
% 58.64/58.77 inference(scs_inference,[],[34,892,281,371,541,12,967,2,22,10,3])).
% 58.64/58.77 cnf(986,plain,
% 58.64/58.77 (P2(a7,x9861,f5(x9862,a1))),
% 58.64/58.77 inference(scs_inference,[],[34,892,281,912,371,541,12,750,967,2,22,10,3,8])).
% 58.64/58.77 cnf(998,plain,
% 58.64/58.77 (E(a7,f5(f5(x9981,x9981),a2))),
% 58.64/58.77 inference(scs_inference,[],[928,224,12,2,23,22])).
% 58.64/58.77 cnf(1001,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a2),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[928,590,224,12,924,2,23,22,7])).
% 58.64/58.77 cnf(1003,plain,
% 58.64/58.77 (E(f5(x10031,a1),f5(a4,a2))),
% 58.64/58.77 inference(rename_variables,[],[590])).
% 58.64/58.77 cnf(1006,plain,
% 58.64/58.77 (E(f5(x10061,a1),f5(a4,a2))),
% 58.64/58.77 inference(rename_variables,[],[590])).
% 58.64/58.77 cnf(1009,plain,
% 58.64/58.77 (E(f5(x10091,a1),f5(a4,a2))),
% 58.64/58.77 inference(rename_variables,[],[590])).
% 58.64/58.77 cnf(1010,plain,
% 58.64/58.77 (P2(f5(a4,a2),x10101,f5(a7,x10101))),
% 58.64/58.77 inference(scs_inference,[],[928,590,1003,1006,1009,333,331,224,463,12,924,2,23,22,7,9,10,8])).
% 58.64/58.77 cnf(1013,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),f5(a3,a4)),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[928,942,348,590,1003,1006,1009,333,331,224,463,12,924,2,23,22,7,9,10,8,3])).
% 58.64/58.77 cnf(1015,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),a2),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[878,349,1001,2,22])).
% 58.64/58.77 cnf(1018,plain,
% 58.64/58.77 (P2(a7,x10181,f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[878,718,237,349,1001,2,22,10])).
% 58.64/58.77 cnf(1020,plain,
% 58.64/58.77 (E(f5(a7,f5(a7,a7)),f5(a7,x10201))),
% 58.64/58.77 inference(scs_inference,[],[878,353,783,718,237,349,1001,2,22,10,3])).
% 58.64/58.77 cnf(1021,plain,
% 58.64/58.77 (P2(x10211,f5(a7,a6),f5(x10211,a7))),
% 58.64/58.77 inference(scs_inference,[],[878,353,783,718,237,349,335,1001,2,22,10,3,9])).
% 58.64/58.77 cnf(1023,plain,
% 58.64/58.77 (P2(f5(a7,a6),x10231,f5(a7,x10231))),
% 58.64/58.77 inference(scs_inference,[],[878,353,783,718,237,331,349,335,1001,2,22,10,3,9,8])).
% 58.64/58.77 cnf(1029,plain,
% 58.64/58.77 (E(f5(f5(a3,a2),a6),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[779,34,271,340,417,562,2,8,10,3])).
% 58.64/58.77 cnf(1040,plain,
% 58.64/58.77 (P2(f5(a7,a1),f5(a7,x10401),f5(f5(a6,a7),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[804,1013,417,2,8])).
% 58.64/58.77 cnf(1041,plain,
% 58.64/58.77 (P2(x10411,f5(a7,x10412),x10411)),
% 58.64/58.77 inference(rename_variables,[],[417])).
% 58.64/58.77 cnf(1042,plain,
% 58.64/58.77 (P2(f5(f5(a6,a7),f5(a3,a4)),f5(a7,x10421),f5(a7,a1))),
% 58.64/58.77 inference(scs_inference,[],[804,1013,417,1041,2,8,10])).
% 58.64/58.77 cnf(1054,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),f5(a3,a4)),f5(a7,x10541))),
% 58.64/58.77 inference(scs_inference,[],[779,34,1013,815,783,19,630,2,10,8,3])).
% 58.64/58.77 cnf(1068,plain,
% 58.64/58.77 (P2(f5(a1,a3),a2,f5(x10681,x10681))),
% 58.64/58.77 inference(scs_inference,[],[779,34,293,346,641,2,8,10])).
% 58.64/58.77 cnf(1080,plain,
% 58.64/58.77 (E(f5(a7,x10801),f5(f5(a6,a7),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[1054,2])).
% 58.64/58.77 cnf(1082,plain,
% 58.64/58.77 (P2(f5(x10821,x10821),f5(x10822,a1),f5(f5(a6,a7),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[779,34,1054,670,647,2,10,8])).
% 58.64/58.77 cnf(1084,plain,
% 58.64/58.77 (E(f5(f5(a6,a7),f5(a3,a4)),f5(x10841,a1))),
% 58.64/58.77 inference(scs_inference,[],[779,34,1054,240,670,647,2,10,8,3])).
% 58.64/58.77 cnf(1086,plain,
% 58.64/58.77 (P2(f5(a7,a1),f5(x10861,x10861),f5(f5(a6,a7),f5(a3,a4)))),
% 58.64/58.77 inference(scs_inference,[],[779,59,34,1054,240,670,647,1040,2,10,8,3,9])).
% 58.64/58.77 cnf(1120,plain,
% 58.64/58.77 (P2(x11201,x11201,f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[1084,590,193,2,10])).
% 58.64/58.77 cnf(1122,plain,
% 58.64/58.77 (E(f5(x11221,a1),f5(a4,a2))),
% 58.64/58.77 inference(rename_variables,[],[590])).
% 58.64/58.77 cnf(1123,plain,
% 58.64/58.77 (P2(f5(a4,a2),x11231,f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[1084,590,1122,193,398,2,10,8])).
% 58.64/58.77 cnf(1149,plain,
% 58.64/58.77 (E(f5(a7,x11491),f5(x11492,x11492))),
% 58.64/58.77 inference(scs_inference,[],[779,34,734,116,1080,785,908,1086,2,8,10,9,3])).
% 58.64/58.77 cnf(1160,plain,
% 58.64/58.77 (P2(a7,x11601,f5(f5(x11602,x11602),a2))),
% 58.64/58.77 inference(scs_inference,[],[998,796,17,2,10])).
% 58.64/58.77 cnf(1162,plain,
% 58.64/58.77 (P2(x11621,f5(f5(x11622,x11622),a2),x11621)),
% 58.64/58.77 inference(scs_inference,[],[998,796,17,19,2,10,8,9])).
% 58.64/58.77 cnf(1168,plain,
% 58.64/58.77 (P2(x11681,x11681,f5(f5(x11682,x11682),a2))),
% 58.64/58.77 inference(scs_inference,[],[998,691,18,237,2,8,10])).
% 58.64/58.77 cnf(1185,plain,
% 58.64/58.77 (P2(a7,f5(a4,a2),f5(f5(a3,a2),f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[998,671,353,352,16,669,871,2,10,8,9])).
% 58.64/58.77 cnf(1199,plain,
% 58.64/58.77 (P2(a7,x11991,f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[371,211,237,331,2,8,10])).
% 58.64/58.77 cnf(1213,plain,
% 58.64/58.77 (E(f5(a7,x12131),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[783,2])).
% 58.64/58.77 cnf(1218,plain,
% 58.64/58.77 (P2(f5(f5(a6,a7),f5(a3,a4)),f5(x12181,x12181),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[779,783,352,400,463,1120,2,10,8,9])).
% 58.64/58.77 cnf(1237,plain,
% 58.64/58.77 (P2(a7,f5(a7,a6),f5(f5(a1,a3),f5(a4,a3)))),
% 58.64/58.77 inference(scs_inference,[],[177,718,1029,333,380,455,2,10,8,9])).
% 58.64/58.77 cnf(1248,plain,
% 58.64/58.77 (P2(f5(x12481,x12481),a6,f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[623,985,331,2,10])).
% 58.64/58.77 cnf(1250,plain,
% 58.64/58.77 (P2(f5(x12501,a1),x12502,f5(a7,x12502))),
% 58.64/58.77 inference(scs_inference,[],[623,177,985,331,360,2,10,8])).
% 58.64/58.77 cnf(1266,plain,
% 58.64/58.77 (P2(x12661,x12661,f5(x12662,a1))),
% 58.64/58.77 inference(scs_inference,[],[177,765,173,2,10])).
% 58.64/58.77 cnf(1267,plain,
% 58.64/58.77 (P2(f5(x12671,a1),x12672,f5(x12673,a1))),
% 58.64/58.77 inference(scs_inference,[],[177,765,173,669,2,10,8])).
% 58.64/58.77 cnf(1279,plain,
% 58.64/58.77 (P2(f5(a7,f5(a7,a7)),a6,f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[623,454,360,2,10])).
% 58.64/58.77 cnf(1281,plain,
% 58.64/58.77 (P2(f5(x12811,x12811),f5(x12812,x12812),f5(f5(a3,a2),f5(a1,a4)))),
% 58.64/58.77 inference(scs_inference,[],[34,623,454,360,871,2,10,8])).
% 58.64/58.77 cnf(1296,plain,
% 58.64/58.77 (P2(a3,f5(a4,a3),f5(a3,a4))),
% 58.64/58.77 inference(scs_inference,[],[878,897,142,913,911,2,7,10])).
% 58.64/58.77 cnf(1300,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),a2),f5(x13001,a1))),
% 58.64/58.77 inference(scs_inference,[],[34,878,897,142,303,913,911,1018,1042,2,7,10,8,9,22])).
% 58.64/58.77 cnf(1312,plain,
% 58.64/58.77 (P2(f5(f5(a3,a6),a2),a6,f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[623,846,947,2,10])).
% 58.64/58.77 cnf(1354,plain,
% 58.64/58.77 (E(f5(x13541,x13541),f5(a7,x13542))),
% 58.64/58.77 inference(scs_inference,[],[1149,2])).
% 58.64/58.77 cnf(1355,plain,
% 58.64/58.77 (P2(x13551,x13551,f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[211,1149,193,2,10])).
% 58.64/58.77 cnf(1371,plain,
% 58.64/58.77 (E(f5(x13711,a1),f5(f5(a4,a3),a2))),
% 58.64/58.77 inference(scs_inference,[],[1300,2])).
% 58.64/58.77 cnf(1372,plain,
% 58.64/58.77 (P2(f5(a6,a7),f5(a3,a4),f5(x13721,x13721))),
% 58.64/58.77 inference(scs_inference,[],[779,1300,20,2,10])).
% 58.64/58.77 cnf(1375,plain,
% 58.64/58.77 (P2(f5(f5(a6,a7),f5(a3,a4)),f5(x13751,x13751),f5(x13752,a1))),
% 58.64/58.77 inference(scs_inference,[],[779,34,1300,20,1160,1266,2,10,8,9])).
% 58.64/58.77 cnf(1389,plain,
% 58.64/58.77 (E(f5(a1,a3),a4)),
% 58.64/58.77 inference(scs_inference,[],[91,2])).
% 58.64/58.77 cnf(1393,plain,
% 58.64/58.77 (E(f5(a1,a3),f5(a4,a3))),
% 58.64/58.77 inference(scs_inference,[],[998,91,900,142,347,641,1248,2,10,8,9,3])).
% 58.64/58.77 cnf(1395,plain,
% 58.64/58.77 (E(f5(a4,a3),f5(a1,a3))),
% 58.64/58.77 inference(scs_inference,[],[1393,2])).
% 58.64/58.77 cnf(1396,plain,
% 58.64/58.77 (P1(a4,f5(a1,a3))),
% 58.64/58.77 inference(scs_inference,[],[1393,106,2,7])).
% 58.64/58.77 cnf(1398,plain,
% 58.64/58.77 (P2(f5(a4,a3),a2,a7)),
% 58.64/58.77 inference(scs_inference,[],[998,1393,106,418,641,2,7,10,8])).
% 58.64/58.77 cnf(1401,plain,
% 58.64/58.77 (P1(f5(a4,f5(a1,a3)),f5(a7,x14011))),
% 58.64/58.77 inference(scs_inference,[],[998,116,1393,106,418,417,641,20,1281,2,7,10,8,9,28])).
% 58.64/58.77 cnf(1405,plain,
% 58.64/58.77 (E(f5(a4,f5(a1,a3)),f5(a7,a1))),
% 58.64/58.77 inference(scs_inference,[],[998,116,1393,106,418,417,641,303,20,1281,2,7,10,8,9,28,22])).
% 58.64/58.77 cnf(1414,plain,
% 58.64/58.77 (E(f5(a3,a4),a6)),
% 58.64/58.77 inference(scs_inference,[],[142,2])).
% 58.64/58.77 cnf(1418,plain,
% 58.64/58.77 (P1(f5(a4,f5(a1,a3)),f5(x14181,x14181))),
% 58.64/58.77 inference(scs_inference,[],[998,142,176,641,970,20,1279,1396,2,10,8,9,28])).
% 58.64/58.77 cnf(1422,plain,
% 58.64/58.77 (E(f5(a4,f5(a1,a3)),f5(a1,a1))),
% 58.64/58.77 inference(scs_inference,[],[998,142,176,641,303,970,20,1279,1396,2,10,8,9,28,22])).
% 58.64/58.77 cnf(1425,plain,
% 58.64/58.77 (P1(f5(a4,f5(a1,a3)),a7)),
% 58.64/58.77 inference(scs_inference,[],[998,116,142,176,641,303,970,20,1279,1396,2,10,8,9,28,22,7])).
% 58.64/58.77 cnf(1444,plain,
% 58.64/58.77 (E(f5(a4,f5(a1,a3)),a7)),
% 58.64/58.77 inference(scs_inference,[],[1405,12,1425,2,22])).
% 58.64/58.77 cnf(1447,plain,
% 58.64/58.77 (P1(f5(a4,f5(a1,a3)),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[352,1405,12,1418,1425,2,22,7])).
% 58.64/58.77 cnf(1454,plain,
% 58.64/58.77 (E(f5(a4,a3),a4)),
% 58.64/58.77 inference(scs_inference,[],[998,352,1389,1395,1405,672,733,12,1086,1418,1425,2,22,7,10,8,9,3])).
% 58.64/58.77 cnf(1455,plain,
% 58.64/58.77 (P1(f5(a1,a3),a4)),
% 58.64/58.77 inference(scs_inference,[],[998,352,1389,1395,1405,672,733,12,1086,1418,1425,2,22,7,10,8,9,3,532])).
% 58.64/58.77 cnf(1456,plain,
% 58.64/58.77 (P1(f5(f5(a1,a3),a4),f5(x14561,x14561))),
% 58.64/58.77 inference(scs_inference,[],[998,352,1389,1395,1405,176,672,733,12,20,1086,1418,1425,2,22,7,10,8,9,3,532,28])).
% 58.64/58.77 cnf(1463,plain,
% 58.64/58.77 (E(f5(a4,f5(a1,a3)),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[1422,349,1447,2,22])).
% 58.64/58.77 cnf(1466,plain,
% 58.64/58.77 (P1(f5(f5(a1,a3),a4),a7)),
% 58.64/58.77 inference(scs_inference,[],[116,1422,349,1447,1456,2,22,7])).
% 58.64/58.77 cnf(1472,plain,
% 58.64/58.77 (P1(f5(f5(a1,a3),a4),f5(a7,x14721))),
% 58.64/58.77 inference(scs_inference,[],[998,623,116,142,1422,417,349,986,1010,20,1312,1447,1456,1455,2,22,7,10,8,9,28])).
% 58.64/58.77 cnf(1486,plain,
% 58.64/58.77 (P1(f5(a4,f5(a1,a3)),f5(x14861,a1))),
% 58.64/58.77 inference(scs_inference,[],[240,1444,303,1401,1472,2,22,7])).
% 58.64/58.77 cnf(1488,plain,
% 58.64/58.77 (P2(f5(f5(a3,a6),a2),a3,f5(x14881,a1))),
% 58.64/58.77 inference(scs_inference,[],[240,1444,303,947,1401,1472,2,22,7,10])).
% 58.64/58.77 cnf(1490,plain,
% 58.64/58.77 (P1(f5(a4,a3),f5(a1,a3))),
% 58.64/58.77 inference(scs_inference,[],[240,1444,900,303,947,1396,1401,1472,2,22,7,10,6])).
% 58.64/58.77 cnf(1491,plain,
% 58.64/58.77 (P2(f5(f5(x14911,x14911),a2),x14912,f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[998,240,1444,900,303,947,1018,1396,1401,1472,2,22,7,10,6,8])).
% 58.64/58.77 cnf(1494,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),f5(a1,a3)),f5(x14941,x14941))),
% 58.64/58.77 inference(scs_inference,[],[998,240,1444,900,176,303,947,1018,20,1040,1396,1401,1472,2,22,7,10,6,8,9,28])).
% 58.64/58.77 cnf(1509,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),f5(a1,a3)),a7)),
% 58.64/58.77 inference(scs_inference,[],[116,981,303,1456,1494,2,22,7])).
% 58.64/58.77 cnf(1515,plain,
% 58.64/58.77 (P1(f5(f5(a1,a3),a4),f5(x15151,a1))),
% 58.64/58.77 inference(scs_inference,[],[878,116,1389,981,670,303,1023,20,1068,1237,1455,1456,1494,2,22,7,10,8,9,28])).
% 58.64/58.77 cnf(1525,plain,
% 58.64/58.77 (E(f5(a4,f5(a1,a3)),f5(x15251,a1))),
% 58.64/58.77 inference(scs_inference,[],[943,303,1486,2,22])).
% 58.64/58.77 cnf(1529,plain,
% 58.64/58.77 (P1(f5(a4,a3),a4)),
% 58.64/58.77 inference(scs_inference,[],[1389,943,303,1490,1486,2,22,7])).
% 58.64/58.77 cnf(1536,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),f5(a1,a3)),f5(a7,x15361))),
% 58.64/58.77 inference(scs_inference,[],[779,623,116,1389,943,417,303,1023,20,1082,1355,1490,1486,2,22,7,10,8,9,28])).
% 58.64/58.77 cnf(1546,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),a4),f5(x15461,a1))),
% 58.64/58.77 inference(scs_inference,[],[1015,303,1515,2,22])).
% 58.64/58.77 cnf(1550,plain,
% 58.64/58.77 (P1(f5(f5(a1,a3),a4),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[352,1015,303,1456,1515,2,22,7])).
% 58.64/58.77 cnf(1558,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a4),f5(x15581,x15581))),
% 58.64/58.77 inference(scs_inference,[],[352,1015,176,609,798,303,20,1218,1456,1515,1529,2,22,7,10,8,9,28])).
% 58.64/58.77 cnf(1568,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),f5(a1,a3)),f5(a1,a1))),
% 58.64/58.77 inference(scs_inference,[],[1463,303,1494,2,22])).
% 58.64/58.77 cnf(1572,plain,
% 58.64/58.77 (P2(f5(x15721,a1),a6,f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[623,1463,303,1250,1494,2,22,10])).
% 58.64/58.77 cnf(1574,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a4),a7)),
% 58.64/58.77 inference(scs_inference,[],[623,116,1463,303,1250,1494,1558,2,22,10,7])).
% 58.64/58.77 cnf(1579,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),f5(a1,a3)),f5(x15791,a1))),
% 58.64/58.77 inference(scs_inference,[],[34,623,116,1463,670,303,20,1250,1185,1375,1490,1494,1558,2,22,10,7,8,9,28])).
% 58.64/58.77 cnf(1589,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),f5(a1,a3)),f5(a7,a1))),
% 58.64/58.77 inference(scs_inference,[],[1525,303,1536,2,22])).
% 58.64/58.77 cnf(1595,plain,
% 58.64/58.77 (P2(f5(x15951,x15951),x15952,f5(a7,a3))),
% 58.64/58.77 inference(scs_inference,[],[34,878,1525,303,947,1199,1536,2,22,10,8])).
% 58.64/58.77 cnf(1597,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a4),f5(a7,x15971))),
% 58.64/58.77 inference(scs_inference,[],[34,878,1525,1414,417,303,947,20,1199,1372,1529,1536,2,22,10,8,9,28])).
% 58.64/58.77 cnf(1601,plain,
% 58.64/58.77 (P1(f5(f5(a4,a3),a4),f5(x16011,a1))),
% 58.64/58.77 inference(scs_inference,[],[34,878,1525,1414,417,303,947,20,1199,1372,1529,1536,2,22,10,8,9,28,7])).
% 58.64/58.77 cnf(1608,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),a4),f5(a4,a2))),
% 58.64/58.77 inference(scs_inference,[],[1546,349,1550,2,22])).
% 58.64/58.77 cnf(1626,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),a4),f5(a1,a1))),
% 58.64/58.77 inference(scs_inference,[],[1568,303,1558,2,22])).
% 58.64/58.77 cnf(1651,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),f5(a1,a3)),f5(x16511,a1))),
% 58.64/58.77 inference(scs_inference,[],[1589,303,1579,2,22])).
% 58.64/58.77 cnf(1660,plain,
% 58.64/58.77 (E(f5(f5(a1,a3),a4),a7)),
% 58.64/58.77 inference(scs_inference,[],[1626,12,1466,2,22])).
% 58.64/58.77 cnf(1668,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),a4),f5(a7,a1))),
% 58.64/58.77 inference(scs_inference,[],[1608,303,1597,2,22])).
% 58.64/58.77 cnf(1672,plain,
% 58.64/58.77 (P2(f5(a4,a3),a2,f5(x16721,x16721))),
% 58.64/58.77 inference(scs_inference,[],[34,1608,303,1398,1597,2,22,10])).
% 58.64/58.77 cnf(1673,plain,
% 58.64/58.77 (P2(f5(a7,a1),x16731,f5(a7,a6))),
% 58.64/58.77 inference(scs_inference,[],[34,765,1608,303,1398,1491,1597,2,22,10,8])).
% 58.64/58.77 cnf(1678,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),f5(a1,a3)),a7)),
% 58.64/58.77 inference(scs_inference,[],[1668,12,1509,2,22])).
% 58.64/58.77 cnf(1686,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),a4),a7)),
% 58.64/58.77 inference(scs_inference,[],[1651,12,1574,2,22])).
% 58.64/58.77 cnf(1708,plain,
% 58.64/58.77 (E(f5(f5(a4,a3),a4),f5(x17081,a1))),
% 58.64/58.77 inference(scs_inference,[],[1660,303,1601,2,22])).
% 58.64/58.77 cnf(1714,plain,
% 58.64/58.77 (P2(a4,f5(a4,a3),a7)),
% 58.64/58.77 inference(scs_inference,[],[1454,1660,18,176,303,1601,2,22,10,8])).
% 58.64/58.77 cnf(1719,plain,
% 58.64/58.77 (P2(f5(a4,a3),f5(x17191,a1),a4)),
% 58.64/58.77 inference(scs_inference,[],[1454,1678,670,2,10])).
% 58.64/58.77 cnf(1722,plain,
% 58.64/58.77 (P2(x17221,x17221,f5(x17222,x17222))),
% 58.64/58.77 inference(rename_variables,[],[193])).
% 58.64/58.77 cnf(1723,plain,
% 58.64/58.77 (P2(f5(a4,a3),a4,f5(x17231,x17231))),
% 58.64/58.78 inference(scs_inference,[],[1454,1678,193,1722,670,2,10,8,9])).
% 58.64/58.78 cnf(1726,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(a7,x17261),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,1686,417,2,10])).
% 58.64/58.78 cnf(1733,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(a3,a2),a6),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,1708,238,2,10])).
% 58.64/58.78 cnf(1742,plain,
% 58.64/58.78 (P2(a4,f5(a7,x17421),f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[1454,1020,417,275,2,10,8])).
% 58.64/58.78 cnf(1760,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(a4,a2),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,346,10])).
% 58.64/58.78 cnf(1764,plain,
% 58.64/58.78 (P2(f5(a4,a3),a4,f5(f5(a3,a6),a2))),
% 58.64/58.78 inference(scs_inference,[],[1454,289,346,951,10,8,9])).
% 58.64/58.78 cnf(1768,plain,
% 58.64/58.78 (P2(a4,a7,f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[1454,19,500,10,8])).
% 58.64/58.78 cnf(1772,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(a4,f5(a4,a3)),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,521,10])).
% 58.64/58.78 cnf(1784,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(a3,a6),a4),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,545,10])).
% 58.64/58.78 cnf(1794,plain,
% 58.64/58.78 (P2(x17941,a4,f5(x17941,f5(a4,a3)))),
% 58.64/58.78 inference(scs_inference,[],[1454,377,568,20,10,8,9])).
% 58.64/58.78 cnf(1803,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(a3,a2),f5(a3,a4)),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,652,10])).
% 58.64/58.78 cnf(1809,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(a3,a6),f5(a1,a3)),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,685,10])).
% 58.64/58.78 cnf(1821,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(a3,a2),f5(a1,a4)),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,840,10])).
% 58.64/58.78 cnf(1826,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(x18261,x18261),a2),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,1162,10])).
% 58.64/58.78 cnf(1841,plain,
% 58.64/58.78 (P2(a4,a3,a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,20,10])).
% 58.64/58.78 cnf(1849,plain,
% 58.64/58.78 (P2(a4,f5(f5(a3,a2),f5(a3,a4)),f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[1454,116,91,652,1372,1764,10,9,8])).
% 58.64/58.78 cnf(1869,plain,
% 58.64/58.78 (P2(a4,f5(f5(a3,a6),f5(a1,a3)),f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[1454,91,685,1733,10,8])).
% 58.64/58.78 cnf(1885,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(a4,a2),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[91,1760,10])).
% 58.64/58.78 cnf(1897,plain,
% 58.64/58.78 (P2(x18971,f5(a1,a3),f5(x18971,f5(a4,a3)))),
% 58.64/58.78 inference(scs_inference,[],[1454,91,1120,1772,1794,10,8,9])).
% 58.64/58.78 cnf(1905,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(a1,a3),f5(x19051,x19051))),
% 58.64/58.78 inference(scs_inference,[],[1454,91,1168,1784,1723,10,8,9])).
% 58.64/58.78 cnf(1914,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(a3,a2),f5(a3,a4)),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[91,1803,10])).
% 58.64/58.78 cnf(1918,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(a3,a6),f5(a1,a3)),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[91,1809,10])).
% 58.64/58.78 cnf(1930,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(a4,a3),a7)),
% 58.64/58.78 inference(scs_inference,[],[91,1001,349,1714,1821,23,10,8])).
% 58.64/58.78 cnf(1941,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(x19411,x19411),f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[34,91,1768,1841,10,8,9])).
% 58.64/58.78 cnf(1947,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(x19471,a1),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[91,1719,10])).
% 58.64/58.78 cnf(1955,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(a4,a3),f5(x19551,x19551))),
% 58.64/58.78 inference(scs_inference,[],[34,1930,10])).
% 58.64/58.78 cnf(1958,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(a7,x19581),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[91,1726,10])).
% 58.64/58.78 cnf(1961,plain,
% 58.64/58.78 (P2(f5(a4,a3),f5(f5(x19611,x19611),a2),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[91,1826,10])).
% 58.64/58.78 cnf(1967,plain,
% 58.64/58.78 (P2(f5(f5(a4,a3),a2),x19671,f5(a7,a6))),
% 58.64/58.78 inference(scs_inference,[],[851,1371,1673,1897,10,8])).
% 58.64/58.78 cnf(1970,plain,
% 58.64/58.78 (P2(a4,f5(a1,a3),f5(x19701,x19701))),
% 58.64/58.78 inference(scs_inference,[],[469,1897,10])).
% 58.64/58.78 cnf(2043,plain,
% 58.64/58.78 (P2(f5(a7,x20431),x20432,f5(f5(a4,a3),a2))),
% 58.64/58.78 inference(scs_inference,[],[1371,474,10])).
% 58.64/58.78 cnf(2045,plain,
% 58.64/58.78 (E(f5(x20451,a1),f5(f5(a4,a3),a2))),
% 58.64/58.78 inference(rename_variables,[],[1371])).
% 58.64/58.78 cnf(2048,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(f5(a4,a3),a2),f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[1371,2045,474,1572,1941,10,8,9])).
% 58.64/58.78 cnf(2053,plain,
% 58.64/58.78 (E(f5(x20531,a1),f5(f5(a4,a3),a2))),
% 58.64/58.78 inference(rename_variables,[],[1371])).
% 58.64/58.78 cnf(2054,plain,
% 58.64/58.78 (P2(f5(f5(a4,a3),a2),x20541,f5(a7,a3))),
% 58.64/58.78 inference(scs_inference,[],[1371,2053,707,1595,10,8])).
% 58.64/58.78 cnf(2077,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(x20771,a1),f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[1371,1300,91,1849,1905,2048,10,8,9])).
% 58.64/58.78 cnf(2086,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(f5(a3,a6),f5(a1,a3)),f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[1371,91,1869,1955,10,8])).
% 58.64/58.78 cnf(2108,plain,
% 58.64/58.78 (P2(f5(a7,x21081),x21082,f5(x21083,a1))),
% 58.64/58.78 inference(scs_inference,[],[1300,2043,10])).
% 58.64/58.78 cnf(2117,plain,
% 58.64/58.78 (P2(a4,f5(a1,a3),f5(f5(a4,a3),a2))),
% 58.64/58.78 inference(scs_inference,[],[1371,1970,10])).
% 58.64/58.78 cnf(2183,plain,
% 58.64/58.78 (P2(a1,x21831,f5(a4,a3))+~E(a3,x21831)),
% 58.64/58.78 inference(scs_inference,[],[1454,910,1885,2086,10,8,9])).
% 58.64/58.78 cnf(2222,plain,
% 58.64/58.78 (P2(f5(f5(a3,a6),a2),x22221,f5(x22222,a1))+~E(a3,x22221)),
% 58.64/58.78 inference(scs_inference,[],[1454,1300,1488,1914,2117,10,8,9])).
% 58.64/58.78 cnf(2225,plain,
% 58.64/58.78 (P2(a1,a2,x22251)+~E(a3,x22251)),
% 58.64/58.78 inference(scs_inference,[],[1454,13,1918,8,10])).
% 58.64/58.78 cnf(2286,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(a7,x22861),f5(a4,a3))),
% 58.64/58.78 inference(scs_inference,[],[1213,91,142,1312,1742,10,9,8])).
% 58.64/58.78 cnf(2291,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(a7,x22911),a4)),
% 58.64/58.78 inference(scs_inference,[],[1454,2286,10])).
% 58.64/58.78 cnf(2422,plain,
% 58.64/58.78 (P2(a4,f5(a7,x24221),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[1454,1958,8])).
% 58.64/58.78 cnf(2426,plain,
% 58.64/58.78 (P2(f5(a4,a3),x24261,f5(x24262,x24262))+~E(a2,x24261)),
% 58.64/58.78 inference(scs_inference,[],[1454,1672,1961,8,9])).
% 58.64/58.78 cnf(2435,plain,
% 58.64/58.78 (P2(a4,x24351,f5(a1,a3))+~E(a3,x24351)),
% 58.64/58.78 inference(scs_inference,[],[1300,91,1550,349,1967,1841,23,8,9,10])).
% 58.64/58.78 cnf(2439,plain,
% 58.64/58.78 (P2(f5(a1,a3),a3,f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[91,1841,8,10])).
% 58.64/58.78 cnf(2440,plain,
% 58.64/58.78 (P2(f5(a1,a3),x24401,a4)+~E(a3,x24401)),
% 58.64/58.78 inference(scs_inference,[],[91,1841,8,10,9])).
% 58.64/58.78 cnf(2448,plain,
% 58.64/58.78 (P2(f5(a1,a3),x24481,f5(a1,a3))+~E(a3,x24481)),
% 58.64/58.78 inference(scs_inference,[],[1300,235,416,2054,2439,22,8,2,9])).
% 58.64/58.78 cnf(2485,plain,
% 58.64/58.78 (P2(x24851,f5(a1,a3),f5(a3,a4))+~E(a3,x24851)),
% 58.64/58.78 inference(scs_inference,[],[322,8])).
% 58.64/58.78 cnf(2486,plain,
% 58.64/58.78 (P2(x24861,a4,f5(a3,a4))+~E(a3,x24861)),
% 58.64/58.78 inference(scs_inference,[],[1389,322,8,9])).
% 58.64/58.78 cnf(2502,plain,
% 58.64/58.78 (P2(x25021,f5(a4,a3),a6)+~E(a3,x25021)),
% 58.64/58.78 inference(scs_inference,[],[911,8])).
% 58.64/58.78 cnf(2503,plain,
% 58.64/58.78 (P2(x25031,f5(a4,a3),f5(a3,a4))+~E(a3,x25031)),
% 58.64/58.78 inference(scs_inference,[],[142,911,8,10])).
% 58.64/58.78 cnf(2656,plain,
% 58.64/58.78 (E(a3,f5(a1,a2))),
% 58.64/58.78 inference(scs_inference,[],[13,20,27])).
% 58.64/58.78 cnf(2657,plain,
% 58.64/58.78 (P2(x26571,x26572,f5(x26571,x26572))),
% 58.64/58.78 inference(rename_variables,[],[20])).
% 58.64/58.78 cnf(2659,plain,
% 58.64/58.78 (P1(f5(a3,a7),f5(a1,a2))),
% 58.64/58.78 inference(scs_inference,[],[13,81,20,27,7])).
% 58.64/58.78 cnf(2660,plain,
% 58.64/58.78 (P2(a1,f5(a1,a2),a4)),
% 58.64/58.78 inference(scs_inference,[],[13,81,14,20,27,7,9])).
% 58.64/58.78 cnf(2661,plain,
% 58.64/58.78 (P2(f5(a1,a2),f5(a1,a3),a6)),
% 58.64/58.78 inference(scs_inference,[],[13,81,97,14,20,27,7,9,8])).
% 58.64/58.78 cnf(2662,plain,
% 58.64/58.78 (P1(f5(f5(a3,a7),f5(a1,a2)),f5(x26621,x26621))),
% 58.64/58.78 inference(scs_inference,[],[13,81,176,97,14,20,2657,27,7,9,8,28])).
% 58.64/58.78 cnf(2664,plain,
% 58.64/58.78 (P2(x26641,x26642,f5(x26641,x26642))),
% 58.64/58.78 inference(rename_variables,[],[20])).
% 58.64/58.78 cnf(2666,plain,
% 58.64/58.78 (P1(a3,f5(a3,a2))),
% 58.64/58.78 inference(scs_inference,[],[13,81,18,176,97,14,19,20,2657,2664,27,7,9,8,28,31])).
% 58.64/58.78 cnf(2673,plain,
% 58.64/58.78 (P2(a4,f5(a1,a2),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[13,81,18,176,97,14,19,20,2657,2664,27,7,9,8,28,31,2183,2222,2435])).
% 58.64/58.78 cnf(2675,plain,
% 58.64/58.78 (P2(f5(a1,a3),f5(a1,a2),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[13,81,18,176,97,14,19,20,2657,2664,27,7,9,8,28,31,2183,2222,2435,2440,2448])).
% 58.64/58.78 cnf(2676,plain,
% 58.64/58.78 (P2(f5(a1,a2),f5(a1,a3),f5(a3,a4))),
% 58.64/58.78 inference(scs_inference,[],[13,81,18,176,97,14,19,20,2657,2664,27,7,9,8,28,31,2183,2222,2435,2440,2448,2485])).
% 58.64/58.78 cnf(2678,plain,
% 58.64/58.78 (P2(f5(a1,a2),f5(a4,a3),a6)),
% 58.64/58.78 inference(scs_inference,[],[13,81,18,176,97,14,19,20,2657,2664,27,7,9,8,28,31,2183,2222,2435,2440,2448,2485,2486,2502])).
% 58.64/58.78 cnf(2681,plain,
% 58.64/58.78 (E(f5(a1,a2),a3)),
% 58.64/58.78 inference(scs_inference,[],[13,81,18,176,97,14,19,20,2657,2664,27,7,9,8,28,31,2183,2222,2435,2440,2448,2485,2486,2502,2503,615,2])).
% 58.64/58.78 cnf(2701,plain,
% 58.64/58.78 (P1(f5(a1,a2),f5(a3,a2))),
% 58.64/58.78 inference(scs_inference,[],[13,21,2656,303,2662,2666,27,22,6])).
% 58.64/58.78 cnf(2703,plain,
% 58.64/58.78 (P2(a4,f5(a1,a2),a4)),
% 58.64/58.78 inference(scs_inference,[],[13,21,1389,2681,2656,303,2662,2673,2666,27,22,6,3,10])).
% 58.64/58.78 cnf(2704,plain,
% 58.64/58.78 (P2(f5(a1,a2),a4,a6)),
% 58.64/58.78 inference(scs_inference,[],[13,21,1389,2681,2656,15,303,2662,2673,2666,27,22,6,3,10,8])).
% 58.64/58.78 cnf(2707,plain,
% 58.64/58.78 (P2(x27071,x27072,f5(x27071,x27072))),
% 58.64/58.78 inference(rename_variables,[],[20])).
% 58.64/58.78 cnf(2714,plain,
% 58.64/58.78 (~E(a3,a6)),
% 58.64/58.78 inference(scs_inference,[],[13,21,1389,2681,2656,670,15,1123,346,20,2707,303,2662,2659,2673,2666,27,22,6,3,10,8,28,31,2225])).
% 58.64/58.78 cnf(2718,plain,
% 58.64/58.78 (~P2(a3,f5(x27181,x27181),a6)),
% 58.64/58.78 inference(scs_inference,[],[21,176,27])).
% 58.64/58.78 cnf(2722,plain,
% 58.64/58.78 (P2(a1,f5(a1,a2),f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[21,91,1414,176,2660,2714,27,3,10])).
% 58.64/58.78 cnf(2723,plain,
% 58.64/58.78 (~E(f5(a1,a3),f5(x27231,x27231))),
% 58.64/58.78 inference(scs_inference,[],[21,91,1414,176,97,2660,2714,27,3,10,9])).
% 58.64/58.78 cnf(2749,plain,
% 58.64/58.78 (~E(f5(a1,a3),f5(x27491,x27491))),
% 58.64/58.78 inference(rename_variables,[],[2723])).
% 58.64/58.78 cnf(2750,plain,
% 58.64/58.78 (~P2(x27501,a1,f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[126,2723,2749,5,27])).
% 58.64/58.78 cnf(2753,plain,
% 58.64/58.78 (~P1(a1,a3)),
% 58.64/58.78 inference(scs_inference,[],[126,11,2723,2749,5,27,22])).
% 58.64/58.78 cnf(2756,plain,
% 58.64/58.78 (~E(f5(a1,a3),a7)),
% 58.64/58.78 inference(scs_inference,[],[34,126,11,2723,2749,5,27,22,3])).
% 58.64/58.78 cnf(2758,plain,
% 58.64/58.78 (~E(f5(a3,a7),a1)),
% 58.64/58.78 inference(scs_inference,[],[34,81,126,11,2723,2749,5,27,22,3,6])).
% 58.64/58.78 cnf(2759,plain,
% 58.64/58.78 (~E(f5(a7,x27591),a1)),
% 58.64/58.78 inference(scs_inference,[],[34,81,126,11,417,2723,2749,5,27,22,3,6,9])).
% 58.64/58.78 cnf(2761,plain,
% 58.64/58.78 (~P2(a3,x27611,a1)),
% 58.64/58.78 inference(scs_inference,[],[34,81,126,11,417,2723,2749,5,27,22,3,6,9,26])).
% 58.64/58.78 cnf(2763,plain,
% 58.64/58.78 (P1(a3,x27631)+~E(f5(a3,a2),x27631)),
% 58.64/58.78 inference(scs_inference,[],[34,81,126,11,417,2666,2723,2749,5,27,22,3,6,9,26,7])).
% 58.64/58.78 cnf(2773,plain,
% 58.64/58.78 (P1(a6,f5(a1,a2))),
% 58.64/58.78 inference(scs_inference,[],[2704,2701,24,26])).
% 58.64/58.78 cnf(2782,plain,
% 58.64/58.78 (~P1(f5(a1,a3),f5(a7,a7))),
% 58.64/58.78 inference(scs_inference,[],[2753,2758,2756,2722,2704,2701,2723,416,24,26,25,2,27,23,22])).
% 58.64/58.78 cnf(2783,plain,
% 58.64/58.78 (P1(f5(a7,x27831),x27832)),
% 58.64/58.78 inference(rename_variables,[],[416])).
% 58.64/58.78 cnf(2787,plain,
% 58.64/58.78 (P1(f5(a1,a2),a3)),
% 58.64/58.78 inference(scs_inference,[],[2753,2758,2756,2722,2704,2701,2723,2681,416,2656,32,24,26,25,2,27,23,22,7,6])).
% 58.64/58.78 cnf(2793,plain,
% 58.64/58.78 (~P2(a3,x27931,a1)),
% 58.64/58.78 inference(rename_variables,[],[2761])).
% 58.64/58.78 cnf(2800,plain,
% 58.64/58.78 (P1(f5(a1,a3),f5(a1,a7))),
% 58.64/58.78 inference(scs_inference,[],[2761,2793,2753,2758,2750,2756,2759,2722,2704,2701,298,1296,2723,2681,416,2783,1021,2656,32,335,24,26,25,2,27,23,22,7,6,3,10,9,8,28,29])).
% 58.64/58.78 cnf(2802,plain,
% 58.64/58.78 (P1(f5(a7,x28021),x28022)),
% 58.64/58.78 inference(rename_variables,[],[416])).
% 58.64/58.78 cnf(2804,plain,
% 58.64/58.78 (~P2(f5(a4,a3),f5(a7,a1),f5(a7,a7))),
% 58.64/58.78 inference(scs_inference,[],[2761,2793,2753,2758,2750,2756,2759,2722,2704,2701,298,2077,1947,2108,1296,2723,2681,416,2783,1021,2656,32,335,24,26,25,2,27,23,22,7,6,3,10,9,8,28,29,31])).
% 58.64/58.78 cnf(2810,plain,
% 58.64/58.78 (E(f5(a3,a2),a6)),
% 58.64/58.78 inference(scs_inference,[],[2761,2793,2753,2758,2750,2756,2759,2722,2704,2701,298,2077,1947,2108,1296,2723,2681,416,2783,1021,2656,32,335,24,26,25,2,27,23,22,7,6,3,10,9,8,28,29,31,2426,111])).
% 58.64/58.78 cnf(2814,plain,
% 58.64/58.78 (~E(f5(a4,a3),f5(a7,a7))),
% 58.64/58.78 inference(scs_inference,[],[2761,2793,2753,2758,2750,2756,2759,2722,2704,2701,298,2077,1947,2108,1296,2723,2681,416,2783,1021,2656,32,335,24,26,25,2,27,23,22,7,6,3,10,9,8,28,29,31,2426,111,206,406,532])).
% 58.64/58.78 cnf(2818,plain,
% 58.64/58.78 (~P2(f5(a7,x28181),a2,f5(a1,a3))),
% 58.64/58.78 inference(scs_inference,[],[2761,2793,2753,2758,2750,2756,2759,2722,2704,2701,298,2077,1947,2108,1296,2723,2681,1672,416,2783,2802,1021,2656,32,335,24,26,25,2,27,23,22,7,6,3,10,9,8,28,29,31,2426,111,206,406,532,510,205,788,30])).
% 58.64/58.78 cnf(2824,plain,
% 58.64/58.78 (P1(a3,a6)),
% 58.64/58.78 inference(scs_inference,[],[2810,2763])).
% 58.64/58.78 cnf(2836,plain,
% 58.64/58.78 (~P1(a6,a3)),
% 58.64/58.78 inference(scs_inference,[],[21,2810,2782,2814,2800,2676,2661,2763,24,26,25,2,27,23,22])).
% 58.64/58.78 cnf(2839,plain,
% 58.64/58.78 (E(f5(x28391,x28391),f5(a7,x28392))),
% 58.64/58.78 inference(rename_variables,[],[1354])).
% 58.64/58.78 cnf(2844,plain,
% 58.64/58.78 (E(f5(x28441,x28441),f5(a7,x28442))),
% 58.64/58.78 inference(rename_variables,[],[1354])).
% 58.64/58.78 cnf(2847,plain,
% 58.64/58.78 (~P1(f5(a1,a3),f5(a7,x28471))),
% 58.64/58.78 inference(scs_inference,[],[21,2810,2782,2804,2814,2800,2818,2718,2675,2676,2661,1354,2839,2844,474,1395,142,2763,24,26,25,2,27,23,22,7,3,6,10,9,8,30])).
% 58.64/58.78 cnf(2864,plain,
% 58.64/58.78 (~E(f5(a4,a3),f5(x28641,x28641))),
% 58.64/58.78 inference(scs_inference,[],[21,2810,2782,2804,2814,2800,2818,2773,2718,2703,2675,2676,2661,2422,1354,2839,2844,2291,1267,1955,474,1395,142,2763,24,26,25,2,27,23,22,7,3,6,10,9,8,30,28,29,31,2426,206,350,532])).
% 58.64/58.78 cnf(2889,plain,
% 58.64/58.78 ($false),
% 58.64/58.78 inference(scs_inference,[],[21,2824,2836,2864,2847,2787,2678,2773,1296,2681,24,206,26,532,25,2,27,23,22,7]),
% 58.64/58.78 ['proof']).
% 58.64/58.78 % SZS output end Proof
% 58.64/58.78 % Total time :58.200000s
%------------------------------------------------------------------------------