%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP012-1 : 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 : n023.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 06:38:27 EDT 2024
% Result : Unsatisfiable 2.65s 2.71s
% Output : CNFRefutation 2.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP012-1 : TPTP v8.2.0. Released v1.0.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n023.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 11:33:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.53/0.58 start to proof:theBenchmark
% 2.64/2.70 %-------------------------------------------
% 2.64/2.70 % File :CSE---1.7
% 2.64/2.70 % Problem :theBenchmark
% 2.64/2.70 % Transform :cnf
% 2.64/2.70 % Format :tptp:raw
% 2.64/2.70 % Command :java -jar mcs_scs.jar %d %s
% 2.64/2.70
% 2.64/2.70 % Result :Theorem 2.100000s
% 2.64/2.70 % Output :CNFRefutation 2.100000s
% 2.64/2.70 %-------------------------------------------
% 2.65/2.71 %--------------------------------------------------------------------------
% 2.65/2.71 % File : GRP012-1 : TPTP v8.2.0. Released v1.0.0.
% 2.65/2.71 % Domain : Group Theory
% 2.65/2.71 % Problem : Inverse of products = Product of inverses
% 2.65/2.71 % Version : [MOW76] axioms.
% 2.65/2.71 % Theorem formulation : Expressed as (X.Y).(Y^-1.X^-1) = id.
% 2.65/2.71 % English : The inverse of products equals the product of the inverse,
% 2.65/2.71 % in opposite order.
% 2.65/2.71
% 2.65/2.71 % Refs : [Wos65] Wos (1965), Unpublished Note
% 2.65/2.71 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 2.65/2.71 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 2.65/2.71 % Source : [SPRFN]
% 2.65/2.71 % Names : Problem 9 [Wos65]
% 2.65/2.71 % : wos9 [WM76]
% 2.65/2.71
% 2.65/2.71 % Status : Unsatisfiable
% 2.65/2.71 % Rating : 0.00 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.07 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v2.0.0
% 2.65/2.71 % Syntax : Number of clauses : 11 ( 8 unt; 0 nHn; 6 RR)
% 2.65/2.71 % Number of literals : 19 ( 1 equ; 9 neg)
% 2.65/2.71 % Maximal clause size : 4 ( 1 avg)
% 2.65/2.71 % Maximal term depth : 2 ( 1 avg)
% 2.65/2.71 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 2.65/2.71 % Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% 2.65/2.71 % Number of variables : 22 ( 0 sgn)
% 2.65/2.71 % SPC : CNF_UNS_RFO_SEQ_HRN
% 2.65/2.71
% 2.65/2.71 % Comments :
% 2.65/2.71 %--------------------------------------------------------------------------
% 2.65/2.71 %----Include group theory axioms
% 2.65/2.71 include('Axioms/GRP003-0.ax').
% 2.65/2.71 %--------------------------------------------------------------------------
% 2.65/2.71 cnf(a_multiply_b_is_c,hypothesis,
% 2.65/2.71 product(a,b,c) ).
% 2.65/2.71
% 2.65/2.71 cnf(inverse_b_multiply_inverse_a_is_d,hypothesis,
% 2.65/2.71 product(inverse(b),inverse(a),d) ).
% 2.65/2.71
% 2.65/2.71 cnf(prove_c_multiply_d_is_identity,negated_conjecture,
% 2.65/2.71 ~ product(c,d,identity) ).
% 2.65/2.71
% 2.65/2.71 %--------------------------------------------------------------------------
% 2.65/2.71 %-------------------------------------------
% 2.65/2.71 % Proof found
% 2.65/2.71 % SZS status Theorem for theBenchmark
% 2.65/2.71 % SZS output start Proof
% 2.65/2.71 %ClaNum:20(EqnAxiom:9)
% 2.65/2.71 %VarNum:44(SingletonVarNum:22)
% 2.65/2.71 %MaxLitNum:4
% 2.65/2.71 %MaxfuncDepth:1
% 2.65/2.71 %SharedTerms:10
% 2.65/2.71 %goalClause: 17
% 2.65/2.71 %singleGoalClaCount:1
% 2.65/2.71 [10]P1(a1,a2,a3)
% 2.65/2.71 [17]~P1(a3,a5,a4)
% 2.65/2.71 [15]P1(f6(a2),f6(a1),a5)
% 2.65/2.71 [11]P1(x111,a4,x111)
% 2.65/2.71 [12]P1(a4,x121,x121)
% 2.65/2.71 [13]P1(x131,f6(x131),a4)
% 2.65/2.71 [14]P1(f6(x141),x141,a4)
% 2.65/2.71 [16]P1(x161,x162,f7(x161,x162))
% 2.65/2.71 [18]~P1(x183,x184,x181)+E(x181,x182)+~P1(x183,x184,x182)
% 2.65/2.71 [19]~P1(x196,x194,x191)+P1(x191,x192,x193)+~P1(x194,x192,x195)+~P1(x196,x195,x193)
% 2.65/2.71 [20]~P1(x201,x206,x204)+P1(x201,x202,x203)+~P1(x204,x205,x203)+~P1(x206,x205,x202)
% 2.65/2.71 %EqnAxiom
% 2.65/2.71 [1]E(x11,x11)
% 2.65/2.71 [2]E(x22,x21)+~E(x21,x22)
% 2.65/2.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.65/2.71 [4]~E(x41,x42)+E(f6(x41),f6(x42))
% 2.65/2.71 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53))
% 2.65/2.71 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62))
% 2.65/2.71 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 2.65/2.71 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 2.65/2.71 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 2.65/2.71
% 2.65/2.71 %-------------------------------------------
% 2.65/2.72 cnf(21,plain,
% 2.65/2.72 (~E(f6(a5),a3)),
% 2.65/2.72 inference(scs_inference,[],[17,14,7])).
% 2.65/2.72 cnf(23,plain,
% 2.65/2.72 (E(x231,f7(x231,a4))),
% 2.65/2.72 inference(scs_inference,[],[17,11,16,14,7,18])).
% 2.65/2.72 cnf(24,plain,
% 2.65/2.72 (P1(x241,x242,f7(x241,x242))),
% 2.65/2.72 inference(rename_variables,[],[16])).
% 2.65/2.72 cnf(27,plain,
% 2.65/2.72 (P1(x271,a4,x271)),
% 2.65/2.72 inference(rename_variables,[],[11])).
% 2.65/2.72 cnf(28,plain,
% 2.65/2.72 (~E(f7(a3,a5),a4)),
% 2.65/2.72 inference(scs_inference,[],[17,11,16,24,14,7,18,8,9])).
% 2.65/2.72 cnf(29,plain,
% 2.65/2.72 (P1(x291,x292,f7(x291,x292))),
% 2.65/2.72 inference(rename_variables,[],[16])).
% 2.65/2.72 cnf(30,plain,
% 2.65/2.72 (~P1(a4,a5,f6(a3))),
% 2.65/2.72 inference(scs_inference,[],[17,11,27,16,24,13,14,7,18,8,9,19])).
% 2.65/2.72 cnf(32,plain,
% 2.65/2.72 (P1(x321,a4,x321)),
% 2.65/2.72 inference(rename_variables,[],[11])).
% 2.65/2.72 cnf(34,plain,
% 2.65/2.72 (P1(x341,f7(a4,a4),x341)),
% 2.65/2.72 inference(scs_inference,[],[17,11,27,32,16,24,29,13,14,7,18,8,9,19,20])).
% 2.65/2.72 cnf(38,plain,
% 2.65/2.72 (~E(f7(a3,a5),f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[17,11,27,32,16,24,29,13,14,7,18,8,9,19,20,2,3])).
% 2.65/2.72 cnf(39,plain,
% 2.65/2.72 (E(f7(x391,a4),x391)),
% 2.65/2.72 inference(scs_inference,[],[23,2])).
% 2.65/2.72 cnf(40,plain,
% 2.65/2.72 (P1(x401,f7(f7(a4,a4),a4),x401)),
% 2.65/2.72 inference(scs_inference,[],[34,23,2,8])).
% 2.65/2.72 cnf(41,plain,
% 2.65/2.72 (E(x411,f7(x411,a4))),
% 2.65/2.72 inference(rename_variables,[],[23])).
% 2.65/2.72 cnf(42,plain,
% 2.65/2.72 (~E(f7(a3,a5),f7(f7(a4,a4),a4))),
% 2.65/2.72 inference(scs_inference,[],[34,38,23,2,8,3])).
% 2.65/2.72 cnf(43,plain,
% 2.65/2.72 (E(x431,f7(x431,f7(a4,a4)))),
% 2.65/2.72 inference(scs_inference,[],[34,38,23,16,2,8,3,18])).
% 2.65/2.72 cnf(46,plain,
% 2.65/2.72 (P1(x461,f7(a4,a4),f7(x461,a4))),
% 2.65/2.72 inference(scs_inference,[],[34,38,23,41,16,2,8,3,18,9])).
% 2.65/2.72 cnf(47,plain,
% 2.65/2.72 (P1(x471,f7(a4,a4),x471)),
% 2.65/2.72 inference(rename_variables,[],[34])).
% 2.65/2.72 cnf(48,plain,
% 2.65/2.72 (P1(f7(x481,a4),f7(a4,a4),x481)),
% 2.65/2.72 inference(scs_inference,[],[34,47,38,23,41,16,2,8,3,18,9,7])).
% 2.65/2.72 cnf(49,plain,
% 2.65/2.72 (P1(x491,f7(a4,a4),x491)),
% 2.65/2.72 inference(rename_variables,[],[34])).
% 2.65/2.72 cnf(50,plain,
% 2.65/2.72 (~P1(f7(a4,a4),a5,f6(a3))),
% 2.65/2.72 inference(scs_inference,[],[34,47,49,30,38,23,41,12,16,2,8,3,18,9,7,19])).
% 2.65/2.72 cnf(57,plain,
% 2.65/2.72 (E(f7(x571,f7(a4,a4)),x571)),
% 2.65/2.72 inference(scs_inference,[],[43,2])).
% 2.65/2.72 cnf(58,plain,
% 2.65/2.72 (E(f7(x581,a4),f7(x581,f7(a4,a4)))),
% 2.65/2.72 inference(scs_inference,[],[43,39,2,3])).
% 2.65/2.72 cnf(59,plain,
% 2.65/2.72 (E(x591,f7(x591,f7(a4,a4)))),
% 2.65/2.72 inference(rename_variables,[],[43])).
% 2.65/2.72 cnf(60,plain,
% 2.65/2.72 (E(x601,f7(f7(x601,a4),a4))),
% 2.65/2.72 inference(scs_inference,[],[48,43,46,39,2,3,18])).
% 2.65/2.72 cnf(61,plain,
% 2.65/2.72 (P1(x611,f7(a4,a4),f7(x611,a4))),
% 2.65/2.72 inference(rename_variables,[],[46])).
% 2.65/2.72 cnf(63,plain,
% 2.65/2.72 (P1(f7(x631,a4),f7(f7(a4,a4),f7(a4,a4)),x631)),
% 2.65/2.72 inference(scs_inference,[],[48,43,59,46,39,2,3,18,8])).
% 2.65/2.72 cnf(64,plain,
% 2.65/2.72 (E(x641,f7(x641,f7(a4,a4)))),
% 2.65/2.72 inference(rename_variables,[],[43])).
% 2.65/2.72 cnf(65,plain,
% 2.65/2.72 (P1(f7(x651,a4),f7(a4,a4),f7(x651,f7(a4,a4)))),
% 2.65/2.72 inference(scs_inference,[],[48,43,59,64,46,39,2,3,18,8,9])).
% 2.65/2.72 cnf(66,plain,
% 2.65/2.72 (P1(f7(x661,a4),f7(a4,a4),x661)),
% 2.65/2.72 inference(rename_variables,[],[48])).
% 2.65/2.72 cnf(67,plain,
% 2.65/2.72 (P1(f7(f7(x671,a4),f7(a4,a4)),f7(a4,a4),x671)),
% 2.65/2.72 inference(scs_inference,[],[48,66,43,59,64,46,39,2,3,18,8,9,7])).
% 2.65/2.72 cnf(69,plain,
% 2.65/2.72 (P1(x691,f7(a4,a4),f7(f7(x691,a4),a4))),
% 2.65/2.72 inference(scs_inference,[],[48,66,34,43,59,64,46,61,39,2,3,18,8,9,7,19])).
% 2.65/2.72 cnf(71,plain,
% 2.65/2.72 (P1(x711,f7(a4,a4),x711)),
% 2.65/2.72 inference(rename_variables,[],[34])).
% 2.65/2.72 cnf(73,plain,
% 2.65/2.72 (P1(f7(a4,a4),a4,a4)),
% 2.65/2.72 inference(scs_inference,[],[48,66,34,71,43,59,64,46,61,39,2,3,18,8,9,7,19,20])).
% 2.65/2.72 cnf(78,plain,
% 2.65/2.72 (E(f7(x781,f7(a4,a4)),f7(x781,a4))),
% 2.65/2.72 inference(scs_inference,[],[58,2])).
% 2.65/2.72 cnf(79,plain,
% 2.65/2.72 (E(x791,f7(f7(x791,a4),f7(a4,a4)))),
% 2.65/2.72 inference(scs_inference,[],[67,34,58,2,18])).
% 2.65/2.72 cnf(86,plain,
% 2.65/2.72 (P1(x861,f7(a4,a4),f7(f7(x861,a4),f7(a4,a4)))),
% 2.65/2.72 inference(scs_inference,[],[67,69,73,21,34,57,58,60,2,18,3,8,9])).
% 2.65/2.72 cnf(87,plain,
% 2.65/2.72 (E(f7(x871,a4),f7(x871,f7(a4,a4)))),
% 2.65/2.72 inference(rename_variables,[],[58])).
% 2.65/2.72 cnf(88,plain,
% 2.65/2.72 (P1(f7(a4,f7(a4,a4)),a4,a4)),
% 2.65/2.72 inference(scs_inference,[],[67,69,73,21,34,57,58,87,60,2,18,3,8,9,7])).
% 2.65/2.72 cnf(90,plain,
% 2.65/2.72 (P1(f7(f7(a4,a4),a4),a4,a4)),
% 2.65/2.72 inference(scs_inference,[],[67,69,73,21,34,57,58,87,60,12,2,18,3,8,9,7,19])).
% 2.65/2.72 cnf(94,plain,
% 2.65/2.72 (E(f7(f7(x941,a4),f7(a4,a4)),x941)),
% 2.65/2.72 inference(scs_inference,[],[79,2])).
% 2.65/2.72 cnf(98,plain,
% 2.65/2.72 (E(x981,f7(f7(x981,a4),f7(a4,a4)))),
% 2.65/2.72 inference(rename_variables,[],[79])).
% 2.65/2.72 cnf(99,plain,
% 2.65/2.72 (P1(f7(a4,a4),a4,f7(f7(a4,a4),f7(a4,a4)))),
% 2.65/2.72 inference(scs_inference,[],[73,79,98,78,42,10,2,3,8,9])).
% 2.65/2.72 cnf(100,plain,
% 2.65/2.72 (E(x1001,f7(f7(x1001,a4),f7(a4,a4)))),
% 2.65/2.72 inference(rename_variables,[],[79])).
% 2.65/2.72 cnf(101,plain,
% 2.65/2.72 (P1(f7(f7(a1,a4),f7(a4,a4)),a2,a3)),
% 2.65/2.72 inference(scs_inference,[],[73,79,98,100,78,42,10,2,3,8,9,7])).
% 2.65/2.72 cnf(103,plain,
% 2.65/2.72 (P1(f6(a1),a3,a2)),
% 2.65/2.72 inference(scs_inference,[],[73,79,98,100,78,42,10,14,12,2,3,8,9,7,20])).
% 2.65/2.72 cnf(105,plain,
% 2.65/2.72 (P1(a4,x1051,x1051)),
% 2.65/2.72 inference(rename_variables,[],[12])).
% 2.65/2.72 cnf(107,plain,
% 2.65/2.72 (P1(f7(f7(a4,a4),a4),f7(a4,a4),a4)),
% 2.65/2.72 inference(scs_inference,[],[69,48,73,79,98,100,78,42,10,14,12,105,2,3,8,9,7,20,19])).
% 2.65/2.72 cnf(112,plain,
% 2.65/2.72 (E(f7(f7(x1121,a4),a4),x1121)),
% 2.65/2.72 inference(scs_inference,[],[60,2])).
% 2.65/2.72 cnf(116,plain,
% 2.65/2.72 (E(x1161,f7(f7(x1161,a4),a4))),
% 2.65/2.72 inference(rename_variables,[],[60])).
% 2.65/2.72 cnf(119,plain,
% 2.65/2.72 (P1(x1191,f7(f7(a4,a4),f7(a4,a4)),x1191)),
% 2.65/2.72 inference(scs_inference,[],[103,21,94,63,39,60,116,2,3,8,9,7])).
% 2.65/2.72 cnf(121,plain,
% 2.65/2.72 (P1(a1,a2,f7(a4,a3))),
% 2.65/2.72 inference(scs_inference,[],[103,21,94,63,39,60,116,13,16,2,3,8,9,7,20])).
% 2.65/2.72 cnf(132,plain,
% 2.65/2.72 (E(f6(a4),a4)),
% 2.65/2.72 inference(scs_inference,[],[12,13,18])).
% 2.65/2.72 cnf(134,plain,
% 2.65/2.72 (P1(a4,x1341,x1341)),
% 2.65/2.72 inference(rename_variables,[],[12])).
% 2.65/2.72 cnf(137,plain,
% 2.65/2.72 (E(x1371,f7(x1371,f7(a4,a4)))),
% 2.65/2.72 inference(rename_variables,[],[43])).
% 2.65/2.72 cnf(138,plain,
% 2.65/2.72 (~E(f6(a5),f7(f7(a3,a4),a4))),
% 2.65/2.72 inference(scs_inference,[],[121,21,12,112,43,13,18,8,3])).
% 2.65/2.72 cnf(141,plain,
% 2.65/2.72 (E(x1411,f7(x1411,f7(a4,a4)))),
% 2.65/2.72 inference(rename_variables,[],[43])).
% 2.65/2.72 cnf(142,plain,
% 2.65/2.72 (P1(f7(a1,f7(a4,a4)),a2,f7(a4,a3))),
% 2.65/2.72 inference(scs_inference,[],[121,21,12,112,43,137,141,13,18,8,3,9,7])).
% 2.65/2.72 cnf(144,plain,
% 2.65/2.72 (~P1(f7(f7(a4,a4),f7(a4,a4)),a5,f6(a3))),
% 2.65/2.72 inference(scs_inference,[],[119,121,30,21,12,134,112,43,137,141,13,18,8,3,9,7,19])).
% 2.65/2.72 cnf(146,plain,
% 2.65/2.72 (P1(x1461,f7(f7(a4,a4),f7(a4,a4)),x1461)),
% 2.65/2.72 inference(rename_variables,[],[119])).
% 2.65/2.72 cnf(148,plain,
% 2.65/2.72 (P1(f7(f7(a4,a4),f7(a4,a4)),a4,a4)),
% 2.65/2.72 inference(scs_inference,[],[119,146,121,67,30,21,12,134,112,43,137,141,13,18,8,3,9,7,19,20])).
% 2.65/2.72 cnf(152,plain,
% 2.65/2.72 (E(a4,f6(a4))),
% 2.65/2.72 inference(scs_inference,[],[119,146,121,67,30,21,12,134,112,43,137,141,13,18,8,3,9,7,19,20,2])).
% 2.65/2.72 cnf(153,plain,
% 2.65/2.72 (~E(f7(a3,a5),f6(a4))),
% 2.65/2.72 inference(scs_inference,[],[28,132,3])).
% 2.65/2.72 cnf(155,plain,
% 2.65/2.72 (P1(f7(f7(a4,a4),a4),a4,f6(a4))),
% 2.65/2.72 inference(scs_inference,[],[90,28,152,132,3,8,9])).
% 2.65/2.72 cnf(156,plain,
% 2.65/2.72 (P1(f6(a4),f7(f7(a4,a4),f7(a4,a4)),a4)),
% 2.65/2.72 inference(scs_inference,[],[90,119,28,152,132,3,8,9,7])).
% 2.65/2.72 cnf(158,plain,
% 2.65/2.72 (P1(a4,f7(f7(a4,a4),f7(a4,a4)),f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[90,119,12,28,152,132,63,3,8,9,7,19])).
% 2.65/2.72 cnf(162,plain,
% 2.65/2.72 (P1(f6(a4),f7(a4,a4),a4)),
% 2.65/2.72 inference(scs_inference,[],[156,57,8])).
% 2.65/2.72 cnf(163,plain,
% 2.65/2.72 (E(f7(x1631,f7(a4,a4)),x1631)),
% 2.65/2.72 inference(rename_variables,[],[57])).
% 2.65/2.72 cnf(168,plain,
% 2.65/2.72 (P1(f7(a1,a4),a2,a3)),
% 2.65/2.72 inference(scs_inference,[],[156,101,103,138,57,163,79,23,8,9,3,7])).
% 2.65/2.72 cnf(170,plain,
% 2.65/2.72 (P1(f7(f7(a4,a4),f7(a4,a4)),f7(a4,a4),f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[148,158,156,101,103,138,57,163,79,23,8,9,3,7,20])).
% 2.65/2.72 cnf(176,plain,
% 2.65/2.72 (P1(f7(a1,a4),a2,f7(a4,a3))),
% 2.65/2.72 inference(scs_inference,[],[170,142,168,78,39,43,9,8,7])).
% 2.65/2.72 cnf(178,plain,
% 2.65/2.72 (P1(f7(a4,f7(a4,a4)),f7(a4,a4),f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[170,142,88,168,158,78,39,43,9,8,7,20])).
% 2.65/2.72 cnf(183,plain,
% 2.65/2.72 (P1(f7(a1,f7(a4,a4)),a2,a3)),
% 2.65/2.72 inference(scs_inference,[],[107,176,168,58,152,79,8,9,7])).
% 2.65/2.72 cnf(185,plain,
% 2.65/2.72 (P1(f7(a4,a4),a4,f7(a4,f7(a4,a4)))),
% 2.65/2.72 inference(scs_inference,[],[178,107,176,168,119,99,58,152,79,8,9,7,19])).
% 2.65/2.72 cnf(188,plain,
% 2.65/2.72 (P1(f6(a4),f7(a4,a4),f7(f7(a4,a4),a4))),
% 2.65/2.72 inference(scs_inference,[],[178,107,176,170,156,168,119,69,99,58,152,79,8,9,7,19,20])).
% 2.65/2.72 cnf(194,plain,
% 2.65/2.72 (P1(f7(f7(a1,a4),a4),a2,f7(a4,a3))),
% 2.65/2.72 inference(scs_inference,[],[188,176,34,23,18,7])).
% 2.65/2.72 cnf(195,plain,
% 2.65/2.72 (E(x1951,f7(x1951,a4))),
% 2.65/2.72 inference(rename_variables,[],[23])).
% 2.65/2.72 cnf(196,plain,
% 2.65/2.72 (P1(f7(a1,f7(a4,a4)),a2,f7(a3,a4))),
% 2.65/2.72 inference(scs_inference,[],[188,183,176,34,23,195,18,7,9])).
% 2.65/2.72 cnf(197,plain,
% 2.65/2.72 (E(x1971,f7(x1971,a4))),
% 2.65/2.72 inference(rename_variables,[],[23])).
% 2.65/2.72 cnf(198,plain,
% 2.65/2.72 (P1(f7(a1,f7(a4,a4)),f7(a2,a4),a3)),
% 2.65/2.72 inference(scs_inference,[],[188,183,176,34,23,195,197,18,7,9,8])).
% 2.65/2.72 cnf(200,plain,
% 2.65/2.72 (P1(f6(a4),f7(a4,f7(a4,a4)),a4)),
% 2.65/2.72 inference(scs_inference,[],[188,185,183,176,90,34,23,195,197,18,7,9,8,20])).
% 2.65/2.72 cnf(206,plain,
% 2.65/2.72 (P1(f7(a4,f7(a4,a4)),f7(a4,a4),a4)),
% 2.65/2.72 inference(scs_inference,[],[178,39,9])).
% 2.65/2.72 cnf(207,plain,
% 2.65/2.72 (E(f7(x2071,a4),x2071)),
% 2.65/2.72 inference(rename_variables,[],[39])).
% 2.65/2.72 cnf(208,plain,
% 2.65/2.72 (P1(a4,f7(a4,f7(a4,a4)),a4)),
% 2.65/2.72 inference(scs_inference,[],[200,178,132,39,9,7])).
% 2.65/2.72 cnf(211,plain,
% 2.65/2.72 (P1(a4,f7(a4,a4),f6(a4))),
% 2.65/2.72 inference(scs_inference,[],[200,178,34,132,39,207,9,7,8,19])).
% 2.65/2.72 cnf(214,plain,
% 2.65/2.72 (P1(a4,a4,f7(a4,f7(a4,a4)))),
% 2.65/2.72 inference(scs_inference,[],[200,178,148,185,158,34,132,39,207,9,7,8,19,20])).
% 2.65/2.72 cnf(219,plain,
% 2.65/2.72 (P1(a4,f7(a4,f7(a4,a4)),f6(a4))),
% 2.65/2.72 inference(scs_inference,[],[211,58,86,18,8])).
% 2.65/2.72 cnf(221,plain,
% 2.65/2.72 (P1(f7(a1,a4),a2,f7(f7(a3,a4),a4))),
% 2.65/2.72 inference(scs_inference,[],[211,168,58,60,86,18,8,9])).
% 2.65/2.72 cnf(222,plain,
% 2.65/2.72 (E(x2221,f7(f7(x2221,a4),a4))),
% 2.65/2.72 inference(rename_variables,[],[60])).
% 2.65/2.72 cnf(223,plain,
% 2.65/2.72 (P1(f7(f7(a4,a4),a4),x2231,x2231)),
% 2.65/2.72 inference(scs_inference,[],[211,168,58,60,222,12,86,18,8,9,7])).
% 2.65/2.72 cnf(225,plain,
% 2.65/2.72 (P1(f6(a4),f7(a4,f7(a4,a4)),f6(a4))),
% 2.65/2.72 inference(scs_inference,[],[211,208,168,58,60,222,12,155,86,18,8,9,7,19])).
% 2.65/2.72 cnf(227,plain,
% 2.65/2.72 (P1(a4,f6(a4),f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[214,211,208,168,178,58,60,222,12,155,86,18,8,9,7,19,20])).
% 2.65/2.72 cnf(236,plain,
% 2.65/2.72 (P1(f6(a4),f6(a4),f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[227,214,152,43,12,18,9,8,7])).
% 2.65/2.72 cnf(237,plain,
% 2.65/2.72 (P1(f7(a4,a4),f7(a4,f7(a4,a4)),f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[225,227,214,152,43,12,18,9,8,7,19])).
% 2.65/2.72 cnf(239,plain,
% 2.65/2.72 (P1(f7(f7(a4,a4),a4),a4,f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[223,225,227,214,170,67,152,43,12,18,9,8,7,19,20])).
% 2.65/2.72 cnf(244,plain,
% 2.65/2.72 (P1(f6(a4),a4,f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[236,132,8])).
% 2.65/2.72 cnf(246,plain,
% 2.65/2.72 (E(x2461,f7(f7(x2461,a4),f7(a4,a4)))),
% 2.65/2.72 inference(rename_variables,[],[79])).
% 2.65/2.72 cnf(252,plain,
% 2.65/2.72 (P1(f6(a4),f7(a4,a4),f7(f7(a4,a4),f6(a4)))),
% 2.65/2.72 inference(scs_inference,[],[236,208,121,30,168,132,79,246,12,16,8,9,7,19,20])).
% 2.65/2.72 cnf(260,plain,
% 2.65/2.72 (P1(a4,f7(a4,f7(a4,a4)),f7(a4,a4))),
% 2.65/2.72 inference(scs_inference,[],[237,252,34,39,153,18,3,7])).
% 2.65/2.72 cnf(261,plain,
% 2.65/2.72 (E(f7(x2611,a4),x2611)),
% 2.65/2.73 inference(rename_variables,[],[39])).
% 2.65/2.73 cnf(263,plain,
% 2.65/2.73 (E(f7(x2631,a4),x2631)),
% 2.65/2.73 inference(rename_variables,[],[39])).
% 2.65/2.73 cnf(266,plain,
% 2.65/2.73 (P1(f7(f7(a4,a4),f6(a4)),a4,a4)),
% 2.65/2.73 inference(scs_inference,[],[237,252,73,34,39,261,263,153,14,18,3,7,8,9,19])).
% 2.65/2.73 cnf(269,plain,
% 2.65/2.73 (P1(f7(f7(a4,a4),a4),f6(a4),f7(a4,a4))),
% 2.65/2.73 inference(scs_inference,[],[237,252,239,73,34,39,261,263,153,219,14,18,3,7,8,9,19,20])).
% 2.65/2.73 cnf(272,plain,
% 2.65/2.73 (E(a4,f7(f7(a4,a4),f6(a4)))),
% 2.65/2.73 inference(scs_inference,[],[266,11,18])).
% 2.65/2.73 cnf(275,plain,
% 2.65/2.73 (P1(a4,f7(a4,a4),f7(f7(a4,a4),f6(a4)))),
% 2.65/2.73 inference(scs_inference,[],[266,252,132,11,18,7])).
% 2.65/2.73 cnf(280,plain,
% 2.65/2.73 (~P1(f6(a4),a5,f6(a3))),
% 2.65/2.73 inference(scs_inference,[],[269,50,266,223,236,176,252,132,58,60,11,18,7,8,9,19])).
% 2.65/2.73 cnf(283,plain,
% 2.65/2.73 (P1(f7(f7(a4,a4),f6(a4)),f7(a4,a4),f7(a4,a4))),
% 2.65/2.73 inference(scs_inference,[],[269,260,50,266,223,236,176,252,132,58,60,11,18,7,8,9,19,20])).
% 2.65/2.73 cnf(286,plain,
% 2.65/2.73 (E(f7(a4,a4),f7(f7(a4,a4),f6(a4)))),
% 2.65/2.73 inference(scs_inference,[],[283,34,272,2,18])).
% 2.65/2.73 cnf(290,plain,
% 2.65/2.73 (E(x2901,f7(x2901,f7(a4,a4)))),
% 2.65/2.73 inference(rename_variables,[],[43])).
% 2.65/2.73 cnf(291,plain,
% 2.65/2.73 (P1(f7(a4,f7(a4,a4)),f7(a4,a4),f6(a4))),
% 2.65/2.73 inference(scs_inference,[],[283,176,211,34,43,290,272,2,18,8,7])).
% 2.65/2.73 cnf(292,plain,
% 2.65/2.73 (E(x2921,f7(x2921,f7(a4,a4)))),
% 2.65/2.73 inference(rename_variables,[],[43])).
% 2.65/2.73 cnf(295,plain,
% 2.65/2.73 (P1(f7(a4,a4),a4,f7(f7(a4,a4),f6(a4)))),
% 2.65/2.73 inference(scs_inference,[],[283,119,176,211,34,43,290,292,272,99,2,18,8,7,9,19])).
% 2.65/2.73 cnf(298,plain,
% 2.65/2.73 (P1(f6(a4),a4,f7(f7(a4,a4),a4))),
% 2.65/2.73 inference(scs_inference,[],[283,225,119,188,176,211,34,43,290,292,206,272,99,2,18,8,7,9,19,20])).
% 2.65/2.73 cnf(301,plain,
% 2.65/2.73 (E(f6(a4),f7(a4,f7(a4,a4)))),
% 2.65/2.73 inference(scs_inference,[],[291,34,286,2,18])).
% 2.65/2.73 cnf(302,plain,
% 2.65/2.73 (P1(x3021,f7(a4,a4),x3021)),
% 2.65/2.73 inference(rename_variables,[],[34])).
% 2.65/2.73 cnf(306,plain,
% 2.65/2.73 (P1(a4,a4,f7(f7(a4,a4),a4))),
% 2.65/2.73 inference(scs_inference,[],[291,298,121,34,132,79,286,2,18,8,7])).
% 2.65/2.73 cnf(309,plain,
% 2.65/2.73 (P1(f6(a4),a4,f7(a4,f7(a4,a4)))),
% 2.65/2.73 inference(scs_inference,[],[291,298,119,121,34,302,112,132,79,286,99,2,18,8,7,9,19])).
% 2.65/2.73 cnf(312,plain,
% 2.65/2.73 (P1(f6(a4),f7(f7(a4,a4),f6(a4)),a4)),
% 2.65/2.73 inference(scs_inference,[],[291,298,275,107,119,121,34,302,112,132,79,286,99,2,18,8,7,9,19,20])).
% 2.65/2.73 cnf(317,plain,
% 2.65/2.73 (E(f7(x3171,a4),x3171)),
% 2.65/2.73 inference(rename_variables,[],[39])).
% 2.65/2.73 cnf(318,plain,
% 2.65/2.73 (P1(a4,f7(f7(a4,a4),f6(a4)),a4)),
% 2.65/2.73 inference(scs_inference,[],[312,275,132,39,301,153,2,3,8,7])).
% 2.65/2.73 cnf(321,plain,
% 2.65/2.73 (P1(a4,f7(a4,a4),f7(f6(a4),a4))),
% 2.65/2.73 inference(scs_inference,[],[312,275,283,132,39,317,301,153,46,2,3,8,7,9,19])).
% 2.65/2.73 cnf(324,plain,
% 2.65/2.73 (P1(a4,f7(f7(a4,a4),a4),f7(a4,a4))),
% 2.65/2.73 inference(scs_inference,[],[312,306,239,275,283,132,39,317,301,153,46,2,3,8,7,9,19,20])).
% 2.65/2.73 cnf(330,plain,
% 2.65/2.73 (P1(f7(x3301,a4),f7(a4,f7(a4,a4)),x3301)),
% 2.65/2.73 inference(scs_inference,[],[321,48,34,58,28,18,3,8])).
% 2.65/2.73 cnf(331,plain,
% 2.65/2.73 (E(f7(x3311,a4),f7(x3311,f7(a4,a4)))),
% 2.65/2.73 inference(rename_variables,[],[58])).
% 2.65/2.73 cnf(332,plain,
% 2.65/2.73 (P1(a1,a2,f7(a3,a4))),
% 2.65/2.73 inference(scs_inference,[],[321,48,34,57,58,196,28,18,3,8,7])).
% 2.65/2.73 cnf(336,plain,
% 2.65/2.73 (P1(f7(a4,a4),f7(a4,a4),f7(f7(a4,a4),f6(a4)))),
% 2.65/2.73 inference(scs_inference,[],[324,321,295,48,34,57,58,331,40,196,28,18,3,8,7,9,20])).
% 2.65/2.73 cnf(339,plain,
% 2.65/2.73 (P1(f7(a4,a4),f7(f7(a4,a4),f6(a4)),f7(a4,a4))),
% 2.65/2.73 inference(scs_inference,[],[324,318,321,295,239,48,34,57,58,331,40,196,28,18,3,8,7,9,20,19])).
% 2.65/2.73 cnf(343,plain,
% 2.65/2.73 (E(x3431,f7(f7(x3431,a4),a4))),
% 2.65/2.73 inference(rename_variables,[],[60])).
% 2.65/2.73 cnf(344,plain,
% 2.65/2.73 (P1(f7(f7(a1,a4),a4),a2,f7(a3,a4))),
% 2.65/2.73 inference(scs_inference,[],[332,60,343,8,7])).
% 2.65/2.73 cnf(348,plain,
% 2.65/2.73 (P1(f6(a4),f7(f7(a4,a4),f6(a4)),f6(a4))),
% 2.65/2.73 inference(scs_inference,[],[339,332,291,30,60,343,12,8,7,9,19])).
% 2.65/2.73 cnf(350,plain,
% 2.65/2.73 (P1(f6(a4),f7(a4,a4),f7(a4,f7(a4,a4)))),
% 2.65/2.73 inference(scs_inference,[],[339,309,332,324,291,30,60,343,12,40,8,7,9,19,20])).
% 2.65/2.73 cnf(354,plain,
% 2.65/2.73 (P1(a4,f7(f7(a4,a4),f6(a4)),f6(a4))),
% 2.65/2.73 inference(scs_inference,[],[348,88,132,152,8,7])).
% 2.65/2.73 cnf(357,plain,
% 2.65/2.73 (P1(f7(f7(a4,a4),f6(a4)),a4,f7(a4,a4))),
% 2.65/2.73 inference(scs_inference,[],[336,350,348,88,119,78,132,152,99,8,7,9,19])).
% 2.65/2.73 cnf(360,plain,
% 2.65/2.73 (P1(f7(a4,a4),f7(f7(a4,a4),f6(a4)),a4)),
% 2.65/2.73 inference(scs_inference,[],[336,350,348,88,295,266,119,78,132,152,99,8,7,9,19,20])).
% 2.65/2.73 cnf(363,plain,
% 2.65/2.73 (E(x3631,f7(x3631,f7(a4,a4)))),
% 2.65/2.73 inference(rename_variables,[],[43])).
% 2.65/2.73 cnf(365,plain,
% 2.65/2.73 (E(x3651,f7(x3651,f7(a4,a4)))),
% 2.65/2.73 inference(rename_variables,[],[43])).
% 2.65/2.73 cnf(366,plain,
% 2.65/2.73 (P1(f7(f6(a4),f7(a4,a4)),f6(a4),f7(a4,a4))),
% 2.65/2.73 inference(scs_inference,[],[332,236,43,363,365,8,9,7])).
% 2.65/2.73 cnf(371,plain,
% 2.65/2.73 (P1(f7(f7(a4,a4),f6(a4)),f6(a4),a4)),
% 2.65/2.73 inference(scs_inference,[],[280,360,357,354,332,236,43,363,365,12,8,9,7,19,20])).
% 2.65/2.73 cnf(374,plain,
% 2.65/2.73 (E(x3741,f7(f7(x3741,a4),f7(a4,a4)))),
% 2.65/2.73 inference(rename_variables,[],[79])).
% 2.65/2.73 cnf(375,plain,
% 2.65/2.73 (P1(f7(f7(a4,a4),f7(a4,a4)),f6(a4),f7(a4,a4))),
% 2.65/2.73 inference(scs_inference,[],[227,168,79,374,8,7])).
% 2.65/2.73 cnf(376,plain,
% 2.65/2.73 (E(x3761,f7(f7(x3761,a4),f7(a4,a4)))),
% 2.65/2.73 inference(rename_variables,[],[79])).
% 2.65/2.73 cnf(379,plain,
% 2.65/2.73 (P1(f7(a4,a3),f6(a2),f7(f7(a1,a4),a4))),
% 2.65/2.73 inference(scs_inference,[],[194,227,168,79,374,376,162,11,13,8,7,9,19])).
% 2.65/2.73 cnf(383,plain,
% 2.65/2.73 (P1(f7(f6(a4),f7(a4,a4)),a4,f7(a4,a4))),
% 2.65/2.73 inference(scs_inference,[],[194,366,200,237,227,168,79,374,376,162,11,13,8,7,9,19,20])).
% 2.65/2.73 cnf(385,plain,
% 2.65/2.73 (E(f7(a4,a4),f7(f6(a4),f7(a4,a4)))),
% 2.65/2.73 inference(scs_inference,[],[383,11,18])).
% 2.65/2.73 cnf(389,plain,
% 2.65/2.73 (E(f7(x3891,a4),x3891)),
% 2.65/2.73 inference(rename_variables,[],[39])).
% 2.65/2.73 cnf(391,plain,
% 2.69/2.73 (E(f7(x3911,a4),x3911)),
% 2.69/2.73 inference(rename_variables,[],[39])).
% 2.69/2.73 cnf(392,plain,
% 2.69/2.73 (P1(a4,f7(f7(a4,a4),f6(a4)),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[383,339,321,39,389,391,11,18,9,8,7])).
% 2.69/2.73 cnf(394,plain,
% 2.69/2.73 (P1(f7(a4,a4),f6(a4),a4)),
% 2.69/2.73 inference(scs_inference,[],[383,375,339,321,67,236,39,389,391,11,18,9,8,7,19])).
% 2.69/2.73 cnf(397,plain,
% 2.69/2.73 (P1(f7(f6(a4),f7(a4,a4)),f7(a4,a4),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[383,375,339,260,321,237,67,236,39,389,391,11,18,9,8,7,19,20])).
% 2.69/2.73 cnf(404,plain,
% 2.69/2.73 (E(f7(f7(x4041,a4),a4),x4041)),
% 2.69/2.73 inference(rename_variables,[],[112])).
% 2.69/2.73 cnf(405,plain,
% 2.69/2.73 (P1(x4051,f7(a4,f7(a4,a4)),f7(x4051,a4))),
% 2.69/2.73 inference(scs_inference,[],[379,121,112,404,60,385,330,38,2,3,8,9,7])).
% 2.69/2.73 cnf(407,plain,
% 2.69/2.73 (P1(f7(a4,a4),a4,f7(f6(a4),f7(a4,a4)))),
% 2.69/2.73 inference(scs_inference,[],[397,379,121,119,112,404,60,385,330,38,99,2,3,8,9,7,19])).
% 2.69/2.73 cnf(410,plain,
% 2.69/2.73 (P1(f7(f7(a4,a4),f6(a4)),f6(a4),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[397,371,392,379,348,121,119,112,404,60,385,330,38,99,2,3,8,9,7,19,20])).
% 2.69/2.73 cnf(415,plain,
% 2.69/2.73 (P1(f6(a4),f7(f7(a4,a4),f6(a4)),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[407,392,57,152,8,9,7])).
% 2.69/2.73 cnf(416,plain,
% 2.69/2.73 (P1(f7(f6(a4),a4),a4,a4)),
% 2.69/2.73 inference(scs_inference,[],[405,407,392,88,57,152,14,8,9,7,19])).
% 2.69/2.73 cnf(418,plain,
% 2.69/2.73 (P1(x4181,f7(a4,f7(a4,a4)),f7(x4181,a4))),
% 2.69/2.73 inference(rename_variables,[],[405])).
% 2.69/2.73 cnf(420,plain,
% 2.69/2.73 (P1(a4,a4,f7(f6(a4),f7(a4,a4)))),
% 2.69/2.73 inference(scs_inference,[],[405,418,407,392,88,57,152,14,8,9,7,19,20])).
% 2.69/2.73 cnf(427,plain,
% 2.69/2.73 (E(x4271,f7(x4271,f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[43])).
% 2.69/2.73 cnf(428,plain,
% 2.69/2.73 (P1(f7(f6(a4),a4),f7(a4,a4),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[420,397,103,78,43,12,18,8,7])).
% 2.69/2.73 cnf(432,plain,
% 2.69/2.73 (P1(a4,f7(f6(a4),f7(a4,a4)),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[420,394,397,383,103,78,43,427,12,18,8,7,9,20])).
% 2.69/2.73 cnf(438,plain,
% 2.69/2.73 (E(f7(a4,a4),f7(f6(a4),a4))),
% 2.69/2.73 inference(scs_inference,[],[428,34,18])).
% 2.69/2.73 cnf(441,plain,
% 2.69/2.73 (P1(f7(f7(a4,a4),f7(a4,a4)),f7(a4,a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[428,211,34,79,18,7])).
% 2.69/2.73 cnf(442,plain,
% 2.69/2.73 (E(x4421,f7(f7(x4421,a4),f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[79])).
% 2.69/2.73 cnf(444,plain,
% 2.69/2.73 (E(x4441,f7(f7(x4441,a4),f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[79])).
% 2.69/2.73 cnf(445,plain,
% 2.69/2.73 (P1(f7(a4,a4),f6(a4),f7(f7(a4,a4),f7(a4,a4)))),
% 2.69/2.73 inference(scs_inference,[],[428,394,211,332,34,79,442,444,18,7,8,9])).
% 2.69/2.73 cnf(447,plain,
% 2.69/2.73 (P1(f7(a4,a4),f7(f7(a4,a4),f6(a4)),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[428,394,339,211,332,48,34,79,442,444,18,7,8,9,19])).
% 2.69/2.73 cnf(450,plain,
% 2.69/2.73 (P1(f7(f6(a4),a4),f6(a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[428,416,394,339,354,211,332,48,34,79,442,444,18,7,8,9,19,20])).
% 2.69/2.73 cnf(455,plain,
% 2.69/2.73 (P1(f7(f6(a4),f7(a4,a4)),f6(a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[450,58,132,438,2,8,7])).
% 2.69/2.73 cnf(457,plain,
% 2.69/2.73 (P1(f7(f6(a4),a4),f6(a4),a4)),
% 2.69/2.73 inference(scs_inference,[],[450,58,132,438,2,8,7,9])).
% 2.69/2.73 cnf(461,plain,
% 2.69/2.73 (P1(f7(f7(a4,a4),f6(a4)),f7(a4,a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[410,450,432,415,447,50,58,132,12,438,2,8,7,9,19,20])).
% 2.69/2.73 cnf(463,plain,
% 2.69/2.73 (P1(f6(a4),f6(a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[455,57,7])).
% 2.69/2.73 cnf(466,plain,
% 2.69/2.73 (E(f7(x4661,a4),x4661)),
% 2.69/2.73 inference(rename_variables,[],[39])).
% 2.69/2.73 cnf(472,plain,
% 2.69/2.73 (P1(a4,f6(a4),f7(f7(a4,a4),f6(a4)))),
% 2.69/2.73 inference(scs_inference,[],[461,344,455,318,275,119,57,39,466,445,7,8,9,19,20])).
% 2.69/2.73 cnf(475,plain,
% 2.69/2.73 (E(x4751,f7(f7(x4751,a4),a4))),
% 2.69/2.73 inference(rename_variables,[],[60])).
% 2.69/2.73 cnf(478,plain,
% 2.69/2.73 (P1(a1,f7(a2,a4),a3)),
% 2.69/2.73 inference(scs_inference,[],[394,168,57,60,475,198,9,8,7])).
% 2.69/2.73 cnf(480,plain,
% 2.69/2.73 (P1(f7(a4,a4),f6(a4),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[463,269,394,168,57,60,475,198,9,8,7,19])).
% 2.69/2.73 cnf(482,plain,
% 2.69/2.73 (P1(a4,f7(f7(a4,a4),a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[472,463,269,394,461,188,168,57,60,475,198,9,8,7,19,20])).
% 2.69/2.73 cnf(484,plain,
% 2.69/2.73 (P1(f7(a4,f7(a4,a4)),f6(a4),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[480,58,7])).
% 2.69/2.73 cnf(490,plain,
% 2.69/2.73 (P1(f6(a4),f6(a4),a4)),
% 2.69/2.73 inference(scs_inference,[],[480,441,482,478,67,112,58,79,7,8,9,19])).
% 2.69/2.73 cnf(493,plain,
% 2.69/2.73 (P1(f7(a4,a4),f7(f6(a4),a4),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[480,441,482,478,405,237,67,112,58,79,7,8,9,19,20])).
% 2.69/2.73 cnf(497,plain,
% 2.69/2.73 (E(f7(x4971,a4),x4971)),
% 2.69/2.73 inference(rename_variables,[],[39])).
% 2.69/2.73 cnf(498,plain,
% 2.69/2.73 (P1(a4,f7(f6(a4),a4),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[493,39,497,9,7])).
% 2.69/2.73 cnf(499,plain,
% 2.69/2.73 (E(f7(x4991,a4),x4991)),
% 2.69/2.73 inference(rename_variables,[],[39])).
% 2.69/2.73 cnf(502,plain,
% 2.69/2.73 (P1(f6(a4),f7(f6(a4),a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[493,441,39,497,499,9,7,8,19])).
% 2.69/2.73 cnf(504,plain,
% 2.69/2.73 (P1(f7(a4,f7(a4,a4)),f6(a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[493,484,447,441,348,39,497,499,9,7,8,19,20])).
% 2.69/2.73 cnf(509,plain,
% 2.69/2.73 (E(x5091,f7(f7(x5091,a4),a4))),
% 2.69/2.73 inference(rename_variables,[],[60])).
% 2.69/2.73 cnf(512,plain,
% 2.69/2.73 (P1(a4,f7(f6(a4),a4),a4)),
% 2.69/2.73 inference(scs_inference,[],[502,490,478,58,60,509,8,7,9,19])).
% 2.69/2.73 cnf(514,plain,
% 2.69/2.73 (P1(f6(a4),f7(f6(a4),f7(a4,a4)),a4)),
% 2.69/2.73 inference(scs_inference,[],[502,490,350,478,407,88,58,60,509,8,7,9,19,20])).
% 2.69/2.73 cnf(518,plain,
% 2.69/2.73 (P1(a4,f7(f6(a4),f7(a4,a4)),a4)),
% 2.69/2.73 inference(scs_inference,[],[504,514,512,132,152,9,8,7])).
% 2.69/2.73 cnf(522,plain,
% 2.69/2.73 (P1(f7(a4,a4),f7(a4,f7(a4,a4)),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[504,514,498,512,50,291,132,152,12,65,9,8,7,19,20])).
% 2.69/2.73 cnf(525,plain,
% 2.69/2.73 (P1(f7(f7(a1,a4),f7(a4,a4)),f7(a2,a4),a3)),
% 2.69/2.73 inference(scs_inference,[],[478,79,7])).
% 2.69/2.73 cnf(526,plain,
% 2.69/2.73 (E(x5261,f7(f7(x5261,a4),f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[79])).
% 2.69/2.73 cnf(528,plain,
% 2.69/2.73 (E(x5281,f7(f7(x5281,a4),f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[79])).
% 2.69/2.73 cnf(531,plain,
% 2.69/2.73 (P1(f7(a4,a4),f7(f6(a4),f7(a4,a4)),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[518,357,478,490,103,79,526,528,7,9,8,19])).
% 2.69/2.73 cnf(536,plain,
% 2.69/2.73 (E(f7(x5361,a4),x5361)),
% 2.69/2.73 inference(rename_variables,[],[39])).
% 2.69/2.73 cnf(538,plain,
% 2.69/2.73 (E(f7(x5381,a4),x5381)),
% 2.69/2.73 inference(rename_variables,[],[39])).
% 2.69/2.73 cnf(541,plain,
% 2.69/2.73 (P1(f7(a4,a4),f6(a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[531,522,463,504,428,39,536,538,221,8,7,9,20])).
% 2.69/2.73 cnf(554,plain,
% 2.69/2.73 (P1(x5541,a4,f7(f7(x5541,a4),f7(a4,a4)))),
% 2.69/2.73 inference(scs_inference,[],[478,94,58,60,11,9,8,7])).
% 2.69/2.73 cnf(556,plain,
% 2.69/2.73 (P1(f7(x5561,a4),f6(a4),f7(f7(x5561,a4),a4))),
% 2.69/2.73 inference(scs_inference,[],[405,484,478,69,94,58,60,11,9,8,7,19])).
% 2.69/2.73 cnf(559,plain,
% 2.69/2.73 (P1(f7(a4,a4),f7(a4,a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[405,541,531,366,484,478,69,94,58,60,11,9,8,7,19,20])).
% 2.69/2.73 cnf(562,plain,
% 2.69/2.73 (P1(f7(x5621,a4),f6(a4),x5621)),
% 2.69/2.73 inference(scs_inference,[],[556,512,112,152,7,9])).
% 2.69/2.73 cnf(564,plain,
% 2.69/2.73 (P1(x5641,f6(a4),f7(f7(x5641,a4),f7(a4,a4)))),
% 2.69/2.73 inference(scs_inference,[],[556,554,512,112,152,7,9,8])).
% 2.69/2.73 cnf(565,plain,
% 2.69/2.73 (P1(f7(x5651,a4),a4,f7(f7(x5651,a4),f7(a4,a4)))),
% 2.69/2.73 inference(scs_inference,[],[405,556,554,512,88,112,152,7,9,8,19])).
% 2.69/2.73 cnf(573,plain,
% 2.69/2.73 (P1(f7(f7(a1,a4),f7(a4,a4)),a2,f7(a3,a4))),
% 2.69/2.73 inference(scs_inference,[],[332,30,79,12,8,7])).
% 2.69/2.73 cnf(575,plain,
% 2.69/2.73 (P1(f7(x5751,a4),a4,x5751)),
% 2.69/2.73 inference(scs_inference,[],[565,332,30,94,79,12,8,7,9])).
% 2.69/2.73 cnf(577,plain,
% 2.69/2.73 (P1(f7(f7(x5771,a4),a4),f6(a4),x5771)),
% 2.69/2.73 inference(scs_inference,[],[405,565,484,332,30,48,94,79,12,8,7,9,19])).
% 2.69/2.73 cnf(578,plain,
% 2.69/2.73 (P1(x5781,f7(a4,f7(a4,a4)),f7(x5781,a4))),
% 2.69/2.73 inference(rename_variables,[],[405])).
% 2.69/2.73 cnf(580,plain,
% 2.69/2.73 (P1(f7(a4,a4),f6(a4),f7(f6(a4),a4))),
% 2.69/2.73 inference(scs_inference,[],[405,578,559,565,522,484,332,30,48,94,79,12,8,7,9,19,20])).
% 2.69/2.73 cnf(584,plain,
% 2.69/2.73 (E(f7(x5841,a4),f7(x5841,f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[58])).
% 2.69/2.73 cnf(587,plain,
% 2.69/2.73 (P1(x5871,f6(a4),x5871)),
% 2.69/2.73 inference(scs_inference,[],[577,332,34,112,58,584,9,8,7])).
% 2.69/2.73 cnf(592,plain,
% 2.69/2.73 (P1(a4,f6(a4),f7(f6(a4),a4))),
% 2.69/2.73 inference(scs_inference,[],[405,580,577,504,332,34,112,58,584,564,9,8,7,19,20])).
% 2.69/2.73 cnf(595,plain,
% 2.69/2.73 (P1(x5951,f6(a4),f7(x5951,a4))),
% 2.69/2.73 inference(scs_inference,[],[112,562,7])).
% 2.69/2.73 cnf(598,plain,
% 2.69/2.73 (P1(x5981,f6(a4),x5981)),
% 2.69/2.73 inference(rename_variables,[],[587])).
% 2.69/2.73 cnf(601,plain,
% 2.69/2.73 (P1(f7(f7(x6011,a4),a4),a4,x6011)),
% 2.69/2.73 inference(scs_inference,[],[405,587,88,94,112,60,244,562,575,7,9,8,19])).
% 2.69/2.73 cnf(604,plain,
% 2.69/2.73 (P1(f7(a4,a4),f7(f6(a4),a4),f6(a4))),
% 2.69/2.73 inference(scs_inference,[],[405,587,598,559,580,88,94,112,60,244,562,575,7,9,8,19,20])).
% 2.69/2.73 cnf(608,plain,
% 2.69/2.73 (P1(f7(a1,a4),a2,f7(a3,a4))),
% 2.69/2.73 inference(scs_inference,[],[573,455,57,132,8,7])).
% 2.69/2.73 cnf(609,plain,
% 2.69/2.73 (E(f7(x6091,f7(a4,a4)),x6091)),
% 2.69/2.73 inference(rename_variables,[],[57])).
% 2.69/2.73 cnf(612,plain,
% 2.69/2.73 (P1(x6121,f6(a4),f7(f7(x6121,a4),a4))),
% 2.69/2.73 inference(scs_inference,[],[405,595,573,587,455,504,57,609,132,8,7,9,20])).
% 2.69/2.73 cnf(617,plain,
% 2.69/2.73 (E(x6171,f7(f7(x6171,a4),f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[79])).
% 2.69/2.73 cnf(618,plain,
% 2.69/2.73 (P1(f7(a1,a4),f7(f7(a2,a4),f7(a4,a4)),f7(a3,a4))),
% 2.69/2.73 inference(scs_inference,[],[608,79,617,13,9,8])).
% 2.69/2.73 cnf(619,plain,
% 2.69/2.73 (E(x6191,f7(f7(x6191,a4),f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[79])).
% 2.69/2.73 cnf(620,plain,
% 2.69/2.73 (P1(f7(f7(a4,a4),f7(a4,a4)),x6201,x6201)),
% 2.69/2.73 inference(scs_inference,[],[608,79,617,619,12,13,9,8,7])).
% 2.69/2.73 cnf(625,plain,
% 2.69/2.73 (E(f7(x6251,a4),f7(x6251,f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[58])).
% 2.69/2.73 cnf(627,plain,
% 2.69/2.73 (E(f7(x6271,a4),f7(x6271,f7(a4,a4)))),
% 2.69/2.73 inference(rename_variables,[],[58])).
% 2.69/2.73 cnf(630,plain,
% 2.69/2.73 (~P1(f7(f7(a5,a4),a4),a4,f6(a3))),
% 2.69/2.73 inference(scs_inference,[],[620,144,604,601,592,58,625,627,457,7,9,8,20])).
% 2.69/2.73 cnf(634,plain,
% 2.69/2.73 (~E(f6(a3),f7(f7(a5,a4),a4))),
% 2.69/2.73 inference(scs_inference,[],[630,11,7])).
% 2.69/2.73 cnf(647,plain,
% 2.69/2.73 (P1(f6(a4),f7(f6(a4),a4),f7(a4,a4))),
% 2.69/2.73 inference(scs_inference,[],[612,634,498,132,152,23,3,8,7])).
% 2.69/2.73 cnf(664,plain,
% 2.69/2.73 (P1(x6641,f6(x6641),f7(f7(a4,a4),a4))),
% 2.69/2.73 inference(scs_inference,[],[647,58,60,13,8,9])).
% 2.69/2.73 cnf(710,plain,
% 2.69/2.73 (P1(x7101,f7(f7(a4,a4),a4),f7(x7101,a4))),
% 2.69/2.73 inference(scs_inference,[],[112,60,575,8,7])).
% 2.69/2.73 cnf(733,plain,
% 2.69/2.73 (P1(x7331,x7332,f7(x7331,x7332))),
% 2.69/2.73 inference(rename_variables,[],[16])).
% 2.69/2.73 cnf(735,plain,
% 2.69/2.73 (E(f7(a3,f7(a4,a4)),f7(a1,a2))),
% 2.69/2.73 inference(scs_inference,[],[10,57,16,18,3])).
% 2.69/2.73 cnf(736,plain,
% 2.69/2.73 (E(f7(x7361,f7(a4,a4)),x7361)),
% 2.69/2.73 inference(rename_variables,[],[57])).
% 2.69/2.73 cnf(737,plain,
% 2.69/2.73 (P1(f7(a1,a4),f7(a2,a4),a3)),
% 2.69/2.73 inference(scs_inference,[],[10,525,57,736,16,18,3,7])).
% 2.69/2.73 cnf(738,plain,
% 2.69/2.73 (E(f7(x7381,f7(a4,a4)),x7381)),
% 2.69/2.73 inference(rename_variables,[],[57])).
% 2.69/2.73 cnf(743,plain,
% 2.69/2.73 (P1(a3,f6(a2),f7(a1,a4))),
% 2.69/2.73 inference(scs_inference,[],[10,710,525,34,57,736,738,664,618,16,18,3,7,9,8,19])).
% 2.69/2.73 cnf(747,plain,
% 2.69/2.73 (P1(a1,a4,f7(a3,f6(a2)))),
% 2.69/2.73 inference(scs_inference,[],[10,710,525,34,57,736,738,13,664,618,16,733,18,3,7,9,8,19,20])).
% 2.69/2.73 cnf(751,plain,
% 2.69/2.73 (E(f7(a1,a2),a3)),
% 2.69/2.73 inference(scs_inference,[],[10,710,525,34,57,736,738,13,664,618,16,733,18,3,7,9,8,19,20,2])).
% 2.69/2.73 cnf(759,plain,
% 2.69/2.73 (E(x7591,f7(f7(x7591,a4),a4))),
% 2.69/2.73 inference(rename_variables,[],[60])).
% 2.69/2.73 cnf(768,plain,
% 2.69/2.73 (~P1(f7(a1,a4),f6(a1),a4)),
% 2.69/2.73 inference(scs_inference,[],[10,17,737,743,747,554,21,58,60,759,11,13,735,751,15,2,18,3,7,9,8,19,20])).
% 2.69/2.73 cnf(838,plain,
% 2.69/2.73 ($false),
% 2.69/2.73 inference(scs_inference,[],[34,768,23,13,28,14,18,3,7]),
% 2.69/2.73 ['proof']).
% 2.69/2.73 % SZS output end Proof
% 2.69/2.73 % Total time :2.100000s
%------------------------------------------------------------------------------