%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP012-2 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n021.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.10s 2.21s
% Output : CNFRefutation 2.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP012-2 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n021.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Jun 20 12:43:24 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.21/0.58 start to proof:theBenchmark
% 2.10/2.21 %-------------------------------------------
% 2.10/2.21 % File :CSE---1.7
% 2.10/2.21 % Problem :theBenchmark
% 2.10/2.21 % Transform :cnf
% 2.10/2.21 % Format :tptp:raw
% 2.10/2.21 % Command :java -jar mcs_scs.jar %d %s
% 2.10/2.21
% 2.10/2.21 % Result :Theorem 1.590000s
% 2.10/2.21 % Output :CNFRefutation 1.590000s
% 2.10/2.21 %-------------------------------------------
% 2.10/2.21 %--------------------------------------------------------------------------
% 2.10/2.21 % File : GRP012-2 : TPTP v8.2.0. Released v1.0.0.
% 2.10/2.21 % Domain : Group Theory
% 2.10/2.21 % Problem : Inverse of products = Product of inverses
% 2.10/2.21 % Version : [MOW76] axioms.
% 2.10/2.21 % Theorem formulation : Expressed as a.b = c and b^-1.a^-1
% 2.10/2.21 % = d, then c^-1 = d
% 2.10/2.21 % English : The inverse of products equals the product of the inverse,
% 2.10/2.21 % in opposite order.
% 2.10/2.21
% 2.10/2.21 % Refs : [LS74] Lawrence & Starkey (1974), Experimental tests of resol
% 2.10/2.21 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 2.10/2.21 % Source : [SPRFN]
% 2.10/2.21 % Names : ls36 [LS74]
% 2.10/2.21 % : ls36 [WM76]
% 2.10/2.21
% 2.10/2.21 % Status : Unsatisfiable
% 2.10/2.21 % Rating : 0.00 v6.0.0, 0.22 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.25 v5.1.0, 0.14 v5.0.0, 0.00 v2.0.0
% 2.10/2.21 % Syntax : Number of clauses : 11 ( 8 unt; 0 nHn; 6 RR)
% 2.10/2.21 % Number of literals : 19 ( 2 equ; 9 neg)
% 2.10/2.21 % Maximal clause size : 4 ( 1 avg)
% 2.10/2.21 % Maximal term depth : 2 ( 1 avg)
% 2.10/2.21 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 2.10/2.21 % Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% 2.10/2.21 % Number of variables : 22 ( 0 sgn)
% 2.10/2.21 % SPC : CNF_UNS_RFO_SEQ_HRN
% 2.10/2.21
% 2.10/2.21 % Comments :
% 2.10/2.21 %--------------------------------------------------------------------------
% 2.10/2.21 %----Include group theory axioms
% 2.10/2.21 include('Axioms/GRP003-0.ax').
% 2.10/2.21 %--------------------------------------------------------------------------
% 2.10/2.21 cnf(a_multiply_b_is_c,hypothesis,
% 2.10/2.21 product(a,b,c) ).
% 2.10/2.21
% 2.10/2.21 cnf(inverse_b_multiply_inverse_a_is_d,hypothesis,
% 2.10/2.21 product(inverse(b),inverse(a),d) ).
% 2.10/2.21
% 2.10/2.21 cnf(prove_c_inverse_equals_d,negated_conjecture,
% 2.10/2.21 inverse(c) != d ).
% 2.10/2.21
% 2.10/2.21 %--------------------------------------------------------------------------
% 2.10/2.21 %-------------------------------------------
% 2.10/2.21 % Proof found
% 2.10/2.21 % SZS status Theorem for theBenchmark
% 2.10/2.21 % SZS output start Proof
% 2.10/2.22 %ClaNum:20(EqnAxiom:9)
% 2.10/2.22 %VarNum:44(SingletonVarNum:22)
% 2.10/2.22 %MaxLitNum:4
% 2.10/2.22 %MaxfuncDepth:1
% 2.10/2.22 %SharedTerms:11
% 2.10/2.22 %goalClause: 17
% 2.10/2.22 %singleGoalClaCount:1
% 2.10/2.22 [10]P1(a1,a2,a3)
% 2.10/2.22 [15]P1(f6(a2),f6(a1),a5)
% 2.10/2.22 [17]~E(f6(a3),a5)
% 2.10/2.22 [11]P1(x111,a4,x111)
% 2.10/2.22 [12]P1(a4,x121,x121)
% 2.10/2.22 [13]P1(x131,f6(x131),a4)
% 2.10/2.22 [14]P1(f6(x141),x141,a4)
% 2.10/2.22 [16]P1(x161,x162,f7(x161,x162))
% 2.10/2.22 [18]~P1(x183,x184,x181)+E(x181,x182)+~P1(x183,x184,x182)
% 2.10/2.22 [19]~P1(x196,x194,x191)+P1(x191,x192,x193)+~P1(x194,x192,x195)+~P1(x196,x195,x193)
% 2.10/2.22 [20]~P1(x201,x206,x204)+P1(x201,x202,x203)+~P1(x204,x205,x203)+~P1(x206,x205,x202)
% 2.10/2.22 %EqnAxiom
% 2.10/2.22 [1]E(x11,x11)
% 2.10/2.22 [2]E(x22,x21)+~E(x21,x22)
% 2.10/2.22 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.10/2.22 [4]~E(x41,x42)+E(f6(x41),f6(x42))
% 2.10/2.22 [5]~E(x51,x52)+E(f7(x51,x53),f7(x52,x53))
% 2.10/2.22 [6]~E(x61,x62)+E(f7(x63,x61),f7(x63,x62))
% 2.10/2.22 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 2.10/2.22 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 2.10/2.22 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 2.10/2.22
% 2.10/2.22 %-------------------------------------------
% 2.19/2.22 cnf(21,plain,
% 2.19/2.22 (E(x211,f7(x211,a4))),
% 2.19/2.22 inference(scs_inference,[],[11,16,18])).
% 2.19/2.22 cnf(22,plain,
% 2.19/2.22 (P1(x221,x222,f7(x221,x222))),
% 2.19/2.22 inference(rename_variables,[],[16])).
% 2.19/2.22 cnf(24,plain,
% 2.19/2.22 (P1(f7(x241,a4),a4,x241)),
% 2.19/2.22 inference(scs_inference,[],[11,16,18,7])).
% 2.19/2.22 cnf(26,plain,
% 2.19/2.22 (P1(x261,a4,x261)),
% 2.19/2.22 inference(rename_variables,[],[11])).
% 2.19/2.22 cnf(27,plain,
% 2.19/2.22 (P1(x271,f6(x271),f7(a4,a4))),
% 2.19/2.22 inference(scs_inference,[],[11,16,13,18,7,8,9])).
% 2.19/2.22 cnf(28,plain,
% 2.19/2.22 (P1(x281,f7(a4,a4),x281)),
% 2.19/2.22 inference(scs_inference,[],[11,26,16,22,13,18,7,8,9,20])).
% 2.19/2.22 cnf(32,plain,
% 2.19/2.22 (E(f7(x321,a4),x321)),
% 2.19/2.22 inference(scs_inference,[],[21,2])).
% 2.19/2.22 cnf(34,plain,
% 2.19/2.22 (P1(f7(a5,a4),f7(a4,a4),a5)),
% 2.19/2.22 inference(scs_inference,[],[17,21,28,2,3,7])).
% 2.19/2.22 cnf(35,plain,
% 2.19/2.22 (P1(x351,f7(a4,a4),x351)),
% 2.19/2.22 inference(rename_variables,[],[28])).
% 2.19/2.22 cnf(36,plain,
% 2.19/2.22 (E(x361,f7(x361,a4))),
% 2.19/2.22 inference(rename_variables,[],[21])).
% 2.19/2.22 cnf(37,plain,
% 2.19/2.22 (E(f6(f7(a4,a4)),a4)),
% 2.19/2.22 inference(scs_inference,[],[17,21,28,35,14,2,3,7,18])).
% 2.19/2.22 cnf(39,plain,
% 2.19/2.22 (P1(x391,f7(a4,a4),x391)),
% 2.19/2.22 inference(rename_variables,[],[28])).
% 2.19/2.22 cnf(41,plain,
% 2.19/2.22 (P1(x411,f7(a4,a4),f7(x411,a4))),
% 2.19/2.22 inference(scs_inference,[],[17,21,36,28,35,39,14,2,3,7,18,9])).
% 2.19/2.22 cnf(42,plain,
% 2.19/2.22 (P1(x421,f7(a4,a4),x421)),
% 2.19/2.22 inference(rename_variables,[],[28])).
% 2.19/2.22 cnf(43,plain,
% 2.19/2.22 (P1(x431,f7(f7(a4,a4),a4),x431)),
% 2.19/2.22 inference(scs_inference,[],[17,21,36,28,35,39,42,14,2,3,7,18,9,8])).
% 2.19/2.22 cnf(48,plain,
% 2.19/2.22 (P1(x481,f6(x481),f7(a4,a4))),
% 2.19/2.22 inference(rename_variables,[],[27])).
% 2.19/2.22 cnf(50,plain,
% 2.19/2.22 (P1(a2,a5,f7(f7(a4,a4),f6(a1)))),
% 2.19/2.22 inference(scs_inference,[],[17,21,36,28,35,39,42,27,48,12,14,15,16,2,3,7,18,9,8,19,20])).
% 2.19/2.22 cnf(54,plain,
% 2.19/2.22 (E(a4,f6(f7(a4,a4)))),
% 2.19/2.22 inference(scs_inference,[],[37,2])).
% 2.19/2.22 cnf(55,plain,
% 2.19/2.22 (E(f7(a4,a4),f6(f7(a4,a4)))),
% 2.19/2.22 inference(scs_inference,[],[32,37,2,3])).
% 2.19/2.22 cnf(56,plain,
% 2.19/2.22 (E(f7(x561,a4),x561)),
% 2.19/2.22 inference(rename_variables,[],[32])).
% 2.19/2.22 cnf(59,plain,
% 2.19/2.22 (P1(x591,f7(f7(a4,a4),a4),x591)),
% 2.19/2.22 inference(rename_variables,[],[43])).
% 2.19/2.22 cnf(61,plain,
% 2.19/2.23 (P1(x611,f7(f7(a4,a4),a4),f7(x611,a4))),
% 2.19/2.23 inference(scs_inference,[],[32,56,37,43,59,12,2,3,18,7])).
% 2.19/2.23 cnf(62,plain,
% 2.19/2.23 (P1(x621,f7(f7(a4,a4),a4),x621)),
% 2.19/2.23 inference(rename_variables,[],[43])).
% 2.19/2.23 cnf(63,plain,
% 2.19/2.23 (P1(f7(x631,a4),f7(f7(a4,a4),a4),x631)),
% 2.19/2.23 inference(scs_inference,[],[32,56,37,43,59,62,12,2,3,18,7,9])).
% 2.19/2.23 cnf(65,plain,
% 2.19/2.23 (P1(a2,f7(a5,a4),f7(f7(a4,a4),f6(a1)))),
% 2.19/2.23 inference(scs_inference,[],[32,56,37,21,43,59,62,50,12,2,3,18,7,9,8])).
% 2.19/2.23 cnf(67,plain,
% 2.19/2.23 (P1(a1,f7(f7(a4,a4),f6(a1)),f7(a3,a5))),
% 2.19/2.23 inference(scs_inference,[],[32,56,37,21,43,59,62,50,10,12,16,2,3,18,7,9,8,20])).
% 2.19/2.23 cnf(73,plain,
% 2.19/2.23 (E(f6(f7(a4,a4)),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[55,2])).
% 2.19/2.23 cnf(74,plain,
% 2.19/2.23 (E(f7(f7(x741,a4),a4),x741)),
% 2.19/2.23 inference(scs_inference,[],[55,61,63,2,18])).
% 2.19/2.23 cnf(77,plain,
% 2.19/2.23 (P1(a4,f7(a4,a4),f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[55,41,61,63,2,18,9])).
% 2.19/2.23 cnf(78,plain,
% 2.19/2.23 (P1(x781,f7(a4,a4),f7(x781,a4))),
% 2.19/2.23 inference(rename_variables,[],[41])).
% 2.19/2.23 cnf(79,plain,
% 2.19/2.23 (P1(f7(a2,a4),f7(a5,a4),f7(f7(a4,a4),f6(a1)))),
% 2.19/2.23 inference(scs_inference,[],[55,21,41,61,63,65,2,18,9,7])).
% 2.19/2.23 cnf(81,plain,
% 2.19/2.23 (P1(x811,f6(f7(a4,a4)),f7(x811,a4))),
% 2.19/2.23 inference(scs_inference,[],[55,21,41,78,61,63,65,2,18,9,7,8])).
% 2.19/2.23 cnf(82,plain,
% 2.19/2.23 (P1(f7(f7(a4,a4),a4),f7(a4,a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[55,21,41,78,61,63,65,2,18,9,7,8,19])).
% 2.19/2.23 cnf(87,plain,
% 2.19/2.23 (P1(f6(a2),f7(f7(a4,a4),f6(a1)),f7(a5,a4))),
% 2.19/2.23 inference(scs_inference,[],[55,21,41,78,61,63,65,14,12,2,18,9,7,8,19,20])).
% 2.19/2.23 cnf(91,plain,
% 2.19/2.23 (E(x911,f7(f7(x911,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[74,2])).
% 2.19/2.23 cnf(95,plain,
% 2.19/2.23 (E(f7(x951,a4),x951)),
% 2.19/2.23 inference(rename_variables,[],[32])).
% 2.19/2.23 cnf(100,plain,
% 2.19/2.23 (P1(f7(a4,a4),f7(a4,a4),f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[17,74,32,95,21,87,81,79,67,28,12,2,3,8,9,7,19])).
% 2.19/2.23 cnf(105,plain,
% 2.19/2.23 (P1(f7(f7(a4,a4),a4),a4,a4)),
% 2.19/2.23 inference(scs_inference,[],[17,74,32,95,21,87,81,79,82,67,28,43,12,2,3,8,9,7,19,20])).
% 2.19/2.23 cnf(108,plain,
% 2.19/2.23 (P1(f7(f7(a1,a4),a4),a2,a3)),
% 2.19/2.23 inference(scs_inference,[],[91,10,7])).
% 2.19/2.23 cnf(109,plain,
% 2.19/2.23 (E(x1091,f7(f7(x1091,a4),a4))),
% 2.19/2.23 inference(rename_variables,[],[91])).
% 2.19/2.23 cnf(110,plain,
% 2.19/2.23 (P1(f7(a4,a4),f7(a4,a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[73,91,13,10,7,8])).
% 2.19/2.23 cnf(111,plain,
% 2.19/2.23 (P1(x1111,f6(x1111),a4)),
% 2.19/2.23 inference(rename_variables,[],[13])).
% 2.19/2.23 cnf(112,plain,
% 2.19/2.23 (P1(x1121,f6(x1121),f7(f7(a4,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[73,91,109,13,111,10,7,8,9])).
% 2.19/2.23 cnf(115,plain,
% 2.19/2.23 (P1(f7(x1151,a4),a4,x1151)),
% 2.19/2.23 inference(rename_variables,[],[24])).
% 2.19/2.23 cnf(117,plain,
% 2.19/2.23 (P1(f7(a4,a4),a4,f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[73,91,109,100,24,115,13,111,10,11,7,8,9,19,20])).
% 2.19/2.23 cnf(121,plain,
% 2.19/2.23 (E(f7(f7(a4,a4),a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[112,12,18])).
% 2.19/2.23 cnf(123,plain,
% 2.19/2.23 (P1(x1231,f6(x1231),f7(f7(a4,a4),a4))),
% 2.19/2.23 inference(rename_variables,[],[112])).
% 2.19/2.23 cnf(125,plain,
% 2.19/2.23 (P1(f7(x1251,a4),f6(f7(a4,a4)),x1251)),
% 2.19/2.23 inference(scs_inference,[],[54,112,24,12,18,8])).
% 2.19/2.23 cnf(126,plain,
% 2.19/2.23 (P1(f6(a2),f6(a1),f7(f7(a5,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[54,91,112,24,15,12,18,8,9])).
% 2.19/2.23 cnf(127,plain,
% 2.19/2.23 (E(x1271,f7(f7(x1271,a4),a4))),
% 2.19/2.23 inference(rename_variables,[],[91])).
% 2.19/2.23 cnf(128,plain,
% 2.19/2.23 (P1(f6(f7(a4,a4)),f7(a4,a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[54,91,112,41,24,15,12,18,8,9,7])).
% 2.19/2.23 cnf(129,plain,
% 2.19/2.23 (P1(x1291,f7(a4,a4),f7(x1291,a4))),
% 2.19/2.23 inference(rename_variables,[],[41])).
% 2.19/2.23 cnf(130,plain,
% 2.19/2.23 (P1(f7(f7(a4,a4),a4),f7(a4,a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[54,91,112,123,41,24,15,28,27,12,18,8,9,7,19])).
% 2.19/2.23 cnf(134,plain,
% 2.19/2.23 (P1(x1341,f7(f6(x1341),a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[54,91,112,123,41,129,82,24,15,28,27,12,18,8,9,7,19,20])).
% 2.19/2.23 cnf(137,plain,
% 2.19/2.23 (E(f6(a4),f7(f7(a4,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[54,91,112,123,41,129,82,24,15,28,27,12,18,8,9,7,19,20,2])).
% 2.19/2.23 cnf(138,plain,
% 2.19/2.23 (E(a4,f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[54,91,127,112,123,41,129,82,24,15,28,27,12,18,8,9,7,19,20,2,3])).
% 2.19/2.23 cnf(140,plain,
% 2.19/2.23 (E(f6(a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[138,2])).
% 2.19/2.23 cnf(141,plain,
% 2.19/2.23 (E(f6(f7(a4,a4)),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[138,37,2,3])).
% 2.19/2.23 cnf(142,plain,
% 2.19/2.23 (P1(f6(f7(a4,a4)),a4,f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[138,37,32,128,2,3,8])).
% 2.19/2.23 cnf(144,plain,
% 2.19/2.23 (P1(f7(f7(a4,a4),a4),a4,f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[138,37,32,128,105,2,3,8,9])).
% 2.19/2.23 cnf(145,plain,
% 2.19/2.23 (P1(f6(a4),f7(a4,a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[121,138,37,32,130,128,105,2,3,8,9,7])).
% 2.19/2.23 cnf(146,plain,
% 2.19/2.23 (P1(f7(a4,a4),f7(f6(a4),a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[121,138,37,32,130,128,105,134,2,3,8,9,7,19])).
% 2.19/2.23 cnf(149,plain,
% 2.19/2.23 (P1(f6(a1),a3,f7(a4,a2))),
% 2.19/2.23 inference(scs_inference,[],[121,138,37,32,130,128,105,134,14,10,16,2,3,8,9,7,19,20])).
% 2.19/2.23 cnf(153,plain,
% 2.19/2.23 (E(f6(a4),f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[141,2])).
% 2.19/2.23 cnf(154,plain,
% 2.19/2.23 (E(f7(a4,a4),f7(f6(a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[141,145,41,2,18])).
% 2.19/2.23 cnf(157,plain,
% 2.19/2.23 (P1(f7(x1571,a4),f6(a4),x1571)),
% 2.19/2.23 inference(scs_inference,[],[141,125,145,41,2,18,8])).
% 2.19/2.23 cnf(158,plain,
% 2.19/2.23 (P1(f6(a4),f6(f7(a4,a4)),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[141,121,125,145,41,2,18,8,7])).
% 2.19/2.23 cnf(159,plain,
% 2.19/2.23 (P1(f7(x1591,a4),f6(f7(a4,a4)),x1591)),
% 2.19/2.23 inference(rename_variables,[],[125])).
% 2.19/2.23 cnf(160,plain,
% 2.19/2.23 (P1(f7(a4,a4),a4,f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[141,121,117,125,145,41,2,18,8,7,9])).
% 2.19/2.23 cnf(161,plain,
% 2.19/2.23 (P1(a5,f7(f6(a4),a4),a5)),
% 2.19/2.23 inference(scs_inference,[],[141,121,117,146,125,145,34,41,2,18,8,7,9,19])).
% 2.19/2.23 cnf(163,plain,
% 2.19/2.23 (P1(f7(a4,a4),f6(a4),f7(f7(a4,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[141,121,117,146,125,159,145,34,112,41,2,18,8,7,9,19,20])).
% 2.19/2.23 cnf(167,plain,
% 2.19/2.23 (E(f7(f6(a4),a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[154,2])).
% 2.19/2.23 cnf(168,plain,
% 2.19/2.23 (E(f6(a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[154,153,73,2,3])).
% 2.19/2.23 cnf(169,plain,
% 2.19/2.23 (P1(f6(a1),f7(f7(a3,a4),a4),f7(a4,a2))),
% 2.19/2.23 inference(scs_inference,[],[154,153,73,91,149,2,3,8])).
% 2.19/2.23 cnf(171,plain,
% 2.19/2.23 (P1(f7(a4,a4),f6(a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[154,153,73,121,91,163,149,2,3,8,9])).
% 2.19/2.23 cnf(172,plain,
% 2.19/2.23 (P1(f7(f6(a4),a4),f6(a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[154,153,73,121,91,163,149,157,2,3,8,9,7])).
% 2.19/2.23 cnf(174,plain,
% 2.19/2.23 (P1(f6(a4),f7(f6(a4),a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[154,153,73,121,91,163,149,157,144,134,2,3,8,9,7,19])).
% 2.19/2.23 cnf(177,plain,
% 2.19/2.23 (P1(f6(a4),f7(a4,a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[154,153,73,121,91,163,158,149,157,110,144,128,134,2,3,8,9,7,19,20])).
% 2.19/2.23 cnf(179,plain,
% 2.19/2.23 (E(f7(a4,a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[168,2])).
% 2.19/2.23 cnf(180,plain,
% 2.19/2.23 (E(a4,f7(f6(a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[168,177,41,2,18])).
% 2.19/2.23 cnf(183,plain,
% 2.19/2.23 (P1(f7(a4,a4),f7(a4,a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[168,171,177,41,2,18,8])).
% 2.19/2.23 cnf(184,plain,
% 2.19/2.23 (P1(f7(a4,a4),f7(f6(a4),a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[168,171,177,174,41,2,18,8,7])).
% 2.19/2.23 cnf(185,plain,
% 2.19/2.23 (P1(f7(a4,a4),f6(a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[168,171,177,174,41,2,18,8,7,9])).
% 2.19/2.23 cnf(189,plain,
% 2.19/2.23 (P1(f6(a4),f6(a4),f7(f7(a4,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[168,171,177,174,157,112,41,2,18,8,7,9,19,20])).
% 2.19/2.23 cnf(192,plain,
% 2.19/2.23 (E(f7(f6(a4),a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[180,2])).
% 2.19/2.23 cnf(193,plain,
% 2.19/2.23 (P1(f6(a4),a4,f7(f7(a4,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[140,180,189,2,8])).
% 2.19/2.23 cnf(194,plain,
% 2.19/2.23 (P1(f6(a4),f6(a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[140,180,74,189,2,8,9])).
% 2.19/2.23 cnf(196,plain,
% 2.19/2.23 (P1(f6(a4),f6(a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[140,179,180,74,189,185,2,8,9,7])).
% 2.19/2.23 cnf(197,plain,
% 2.19/2.23 (P1(f6(a4),f6(a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[140,179,180,74,189,183,185,2,8,9,7,19])).
% 2.19/2.23 cnf(199,plain,
% 2.19/2.23 (P1(f6(a4),f7(f7(a4,a4),a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[140,179,180,74,189,183,185,157,2,8,9,7,19,20])).
% 2.19/2.23 cnf(202,plain,
% 2.19/2.23 (P1(f6(a1),f7(a3,a4),f7(a4,a2))),
% 2.19/2.23 inference(scs_inference,[],[32,169,8])).
% 2.19/2.23 cnf(203,plain,
% 2.19/2.23 (E(f7(x2031,a4),x2031)),
% 2.19/2.23 inference(rename_variables,[],[32])).
% 2.19/2.23 cnf(204,plain,
% 2.19/2.23 (P1(f7(f7(a4,a4),a4),f6(a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[137,32,169,197,8,7])).
% 2.19/2.23 cnf(205,plain,
% 2.19/2.23 (P1(f6(a2),f6(a1),f7(a5,a4))),
% 2.19/2.23 inference(scs_inference,[],[137,32,203,169,126,197,8,7,9])).
% 2.19/2.23 cnf(207,plain,
% 2.19/2.23 (P1(f6(a4),f6(f7(a4,a4)),a4)),
% 2.19/2.23 inference(scs_inference,[],[137,32,203,184,169,126,197,125,157,8,7,9,19])).
% 2.19/2.23 cnf(211,plain,
% 2.19/2.23 (P1(f6(a4),f7(a4,a4),f7(f7(a4,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[137,32,203,199,184,169,196,126,197,61,125,157,8,7,9,19,20])).
% 2.19/2.23 cnf(214,plain,
% 2.19/2.23 (P1(a4,f7(a4,a4),f7(f7(a4,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[140,211,7])).
% 2.19/2.23 cnf(215,plain,
% 2.19/2.23 (P1(a4,f6(a4),f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[140,179,211,77,7,8])).
% 2.19/2.23 cnf(216,plain,
% 2.19/2.23 (P1(f6(a4),f6(a4),f7(f6(a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[140,179,180,211,194,77,7,8,9])).
% 2.19/2.23 cnf(217,plain,
% 2.19/2.23 (P1(f7(f7(a4,a4),a4),f7(a4,a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[140,179,180,211,194,77,110,11,7,8,9,19])).
% 2.19/2.23 cnf(220,plain,
% 2.19/2.23 (P1(f6(a2),f7(a4,a2),f7(f7(a5,a4),f7(a3,a4)))),
% 2.19/2.23 inference(scs_inference,[],[140,179,180,211,194,202,205,77,110,11,16,7,8,9,19,20])).
% 2.19/2.23 cnf(223,plain,
% 2.19/2.23 (P1(f7(a4,a4),f6(f7(a4,a4)),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[54,160,8])).
% 2.19/2.23 cnf(225,plain,
% 2.19/2.23 (P1(a4,f7(a4,a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[153,54,121,214,160,197,8,7,9])).
% 2.19/2.23 cnf(226,plain,
% 2.19/2.23 (P1(f6(a4),a4,f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[153,54,121,204,214,160,193,197,63,8,7,9,19])).
% 2.19/2.23 cnf(229,plain,
% 2.19/2.23 (P1(a2,f7(f7(a5,a4),f7(a3,a4)),f7(a4,a2))),
% 2.19/2.23 inference(scs_inference,[],[153,54,121,220,204,214,160,193,197,63,13,12,8,7,9,19,20])).
% 2.19/2.23 cnf(233,plain,
% 2.19/2.23 (P1(f7(f6(a4),a4),f7(a4,a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[180,225,7])).
% 2.19/2.23 cnf(234,plain,
% 2.19/2.23 (P1(a4,f7(f6(a4),a4),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[154,180,225,7,8])).
% 2.19/2.23 cnf(239,plain,
% 2.19/2.23 (P1(f7(f7(a4,a4),a4),f6(a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[154,180,217,223,216,225,207,185,14,7,8,9,19,20])).
% 2.19/2.23 cnf(243,plain,
% 2.19/2.23 (P1(f6(a4),f6(a4),f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[138,142,215,8,7])).
% 2.19/2.23 cnf(245,plain,
% 2.19/2.23 (P1(a5,f6(a4),a5)),
% 2.19/2.23 inference(scs_inference,[],[179,138,161,142,215,172,11,8,7,9,19])).
% 2.19/2.23 cnf(248,plain,
% 2.19/2.23 (P1(f6(a4),f7(a4,a4),f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[179,138,161,142,215,172,117,158,11,8,7,9,19,20])).
% 2.19/2.23 cnf(250,plain,
% 2.19/2.23 (P1(f7(f7(a5,a4),a4),f6(a4),a5)),
% 2.19/2.23 inference(scs_inference,[],[91,245,7])).
% 2.19/2.23 cnf(252,plain,
% 2.19/2.23 (P1(f6(a4),f7(f6(a4),a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[180,91,226,245,7,8])).
% 2.19/2.23 cnf(253,plain,
% 2.19/2.23 (P1(f6(a4),a4,f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[55,180,91,226,245,7,8,9])).
% 2.19/2.23 cnf(257,plain,
% 2.19/2.23 (P1(f7(a4,a4),f6(a4),f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[55,180,91,248,226,245,183,110,11,7,8,9,19,20])).
% 2.19/2.23 cnf(259,plain,
% 2.19/2.23 (P1(a4,a4,f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[192,234,8])).
% 2.19/2.23 cnf(260,plain,
% 2.19/2.23 (P1(f6(a4),f6(f7(a4,a4)),f6(a4))),
% 2.19/2.23 inference(scs_inference,[],[192,179,234,223,8,7])).
% 2.19/2.23 cnf(261,plain,
% 2.19/2.23 (P1(a5,f6(a4),f7(f7(a5,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[192,179,91,234,245,223,8,7,9])).
% 2.19/2.23 cnf(266,plain,
% 2.19/2.23 (P1(f7(f6(a4),a4),f6(a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[192,179,91,252,257,233,243,234,245,184,223,125,8,7,9,19,20])).
% 2.19/2.23 cnf(274,plain,
% 2.19/2.23 (P1(f6(a2),f7(a4,a2),f7(f7(a5,a4),a3))),
% 2.19/2.23 inference(scs_inference,[],[137,54,21,239,260,229,259,149,205,16,7,8,9,19,20])).
% 2.19/2.23 cnf(284,plain,
% 2.19/2.23 (P1(a5,f6(f7(a4,a4)),a5)),
% 2.19/2.23 inference(scs_inference,[],[140,253,266,250,260,67,233,14,12,8,7,9,20,19])).
% 2.19/2.23 cnf(286,plain,
% 2.19/2.23 (P1(f7(a4,a4),f7(a4,a4),f7(f6(a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[167,28,7])).
% 2.19/2.23 cnf(288,plain,
% 2.19/2.23 (P1(f7(x2881,a4),f7(f6(a4),a4),x2881)),
% 2.19/2.23 inference(scs_inference,[],[167,180,24,28,7,8])).
% 2.19/2.23 cnf(304,plain,
% 2.19/2.23 (P1(a5,f7(a4,a4),f7(f7(a5,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[168,91,12,261,7,8])).
% 2.19/2.23 cnf(306,plain,
% 2.19/2.23 (P1(f6(a5),a5,f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[168,179,91,27,14,12,284,261,7,8,9,20])).
% 2.19/2.23 cnf(310,plain,
% 2.19/2.23 (P1(f6(a5),f7(a5,a4),f6(f7(a4,a4)))),
% 2.19/2.23 inference(scs_inference,[],[21,306,8])).
% 2.19/2.23 cnf(311,plain,
% 2.19/2.23 (E(x3111,f7(x3111,a4))),
% 2.19/2.23 inference(rename_variables,[],[21])).
% 2.19/2.23 cnf(312,plain,
% 2.19/2.23 (P1(f7(a4,a4),x3121,x3121)),
% 2.19/2.23 inference(scs_inference,[],[21,311,12,306,8,7])).
% 2.19/2.23 cnf(313,plain,
% 2.19/2.23 (E(x3131,f7(x3131,a4))),
% 2.19/2.23 inference(rename_variables,[],[21])).
% 2.19/2.23 cnf(316,plain,
% 2.19/2.23 (P1(a2,f7(f7(a5,a4),a3),f7(a4,a2))),
% 2.19/2.23 inference(scs_inference,[],[21,311,313,134,13,12,274,306,8,7,9,20])).
% 2.19/2.23 cnf(320,plain,
% 2.19/2.23 (P1(a4,f7(a4,a4),f7(f6(a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[32,286,7])).
% 2.19/2.23 cnf(321,plain,
% 2.19/2.23 (E(f7(x3211,a4),x3211)),
% 2.19/2.23 inference(rename_variables,[],[32])).
% 2.19/2.23 cnf(322,plain,
% 2.19/2.23 (P1(a5,a4,f7(f7(a5,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[32,321,286,304,7,8])).
% 2.19/2.23 cnf(326,plain,
% 2.19/2.23 (P1(f6(a5),f7(f7(a5,a4),a4),f7(a4,a4))),
% 2.19/2.23 inference(scs_inference,[],[32,321,91,14,12,286,304,7,8,9,20])).
% 2.19/2.23 cnf(331,plain,
% 2.19/2.23 (P1(x3311,f7(f6(a4),a4),f7(x3311,a4))),
% 2.19/2.23 inference(scs_inference,[],[74,138,11,288,8,7])).
% 2.19/2.23 cnf(334,plain,
% 2.19/2.23 (P1(f6(a5),f7(f7(a5,a4),a4),a4)),
% 2.19/2.23 inference(scs_inference,[],[74,138,11,14,288,322,8,7,9,20])).
% 2.19/2.23 cnf(339,plain,
% 2.19/2.23 (E(x3391,f7(x3391,a4))),
% 2.19/2.23 inference(rename_variables,[],[21])).
% 2.19/2.23 cnf(344,plain,
% 2.19/2.23 (P1(a1,f7(a4,a2),f7(f7(a3,a4),a4))),
% 2.19/2.23 inference(scs_inference,[],[74,21,339,13,14,12,326,316,169,7,8,9,20])).
% 2.19/2.23 cnf(348,plain,
% 2.19/2.23 (P1(x3481,f6(a4),f7(x3481,a4))),
% 2.19/2.23 inference(scs_inference,[],[32,331,8])).
% 2.19/2.23 cnf(349,plain,
% 2.19/2.23 (E(f7(x3491,a4),x3491)),
% 2.19/2.23 inference(rename_variables,[],[32])).
% 2.19/2.23 cnf(350,plain,
% 2.19/2.23 (P1(f7(a1,a4),a2,a3)),
% 2.19/2.23 inference(scs_inference,[],[32,349,331,108,8,7])).
% 2.19/2.23 cnf(359,plain,
% 2.19/2.23 (P1(a1,f7(a4,a2),a3)),
% 2.19/2.23 inference(scs_inference,[],[74,179,344,320,8,9])).
% 2.19/2.23 cnf(361,plain,
% 2.19/2.23 (P1(f6(f7(a1,a4)),a3,a2)),
% 2.19/2.23 inference(scs_inference,[],[74,179,14,12,344,320,350,8,9,20])).
% 2.19/2.23 cnf(365,plain,
% 2.19/2.23 (P1(f7(f7(a1,a4),a4),f7(a4,a2),a3)),
% 2.19/2.23 inference(scs_inference,[],[74,179,91,14,12,344,320,350,8,9,20,7])).
% 2.19/2.23 cnf(371,plain,
% 2.19/2.23 (P1(f7(f7(a1,a4),a4),f7(a4,a2),f7(a3,a4))),
% 2.19/2.23 inference(scs_inference,[],[32,21,125,365,334,7,8,9])).
% 2.19/2.23 cnf(373,plain,
% 2.19/2.23 (P1(a2,f7(f7(a5,a4),a4),f6(a1))),
% 2.19/2.23 inference(scs_inference,[],[32,21,125,13,12,365,334,126,7,8,9,20])).
% 2.19/2.23 cnf(378,plain,
% 2.19/2.23 (P1(a2,a5,f6(a1))),
% 2.19/2.23 inference(scs_inference,[],[74,373,8])).
% 2.19/2.23 cnf(379,plain,
% 2.19/2.23 (E(f7(f7(x3791,a4),a4),x3791)),
% 2.19/2.24 inference(rename_variables,[],[74])).
% 2.19/2.24 cnf(380,plain,
% 2.19/2.24 (P1(a1,f7(a4,a2),f7(a3,a4))),
% 2.19/2.24 inference(scs_inference,[],[74,379,371,373,8,7])).
% 2.19/2.24 cnf(382,plain,
% 2.19/2.24 (P1(f6(a5),f7(a5,a4),f7(a4,a4))),
% 2.19/2.24 inference(scs_inference,[],[73,74,379,371,373,310,8,7,9])).
% 2.19/2.24 cnf(383,plain,
% 2.19/2.24 (P1(a2,f7(a5,a4),f6(a1))),
% 2.19/2.24 inference(scs_inference,[],[73,74,379,27,371,373,310,312,205,8,7,9,20])).
% 2.19/2.24 cnf(388,plain,
% 2.19/2.24 (E(x3881,f7(f7(x3881,a4),a4))),
% 2.19/2.24 inference(rename_variables,[],[91])).
% 2.19/2.24 cnf(391,plain,
% 2.19/2.24 (P1(f6(a5),f7(a5,a4),f6(a4))),
% 2.19/2.24 inference(scs_inference,[],[179,91,388,382,383,160,7,8,9])).
% 2.19/2.24 cnf(392,plain,
% 2.19/2.24 (P1(f6(a1),a3,a2)),
% 2.19/2.24 inference(scs_inference,[],[179,91,388,14,12,382,383,160,10,7,8,9,20])).
% 2.19/2.24 cnf(396,plain,
% 2.19/2.24 (P1(a1,f7(f7(a4,a2),a4),a3)),
% 2.19/2.24 inference(scs_inference,[],[21,359,8])).
% 2.19/2.24 cnf(397,plain,
% 2.19/2.24 (E(x3971,f7(x3971,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(399,plain,
% 2.19/2.24 (E(x3991,f7(x3991,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(400,plain,
% 2.19/2.24 (P1(a2,a5,f7(f6(a1),a4))),
% 2.19/2.24 inference(scs_inference,[],[21,397,399,359,378,8,7,9])).
% 2.19/2.24 cnf(402,plain,
% 2.19/2.24 (P1(f6(a1),a3,f7(f7(a4,a2),a4))),
% 2.19/2.24 inference(scs_inference,[],[21,397,399,14,12,359,378,8,7,9,20])).
% 2.19/2.24 cnf(407,plain,
% 2.19/2.24 (E(x4071,f7(f7(x4071,a4),a4))),
% 2.19/2.24 inference(rename_variables,[],[91])).
% 2.19/2.24 cnf(409,plain,
% 2.19/2.24 (E(x4091,f7(f7(x4091,a4),a4))),
% 2.19/2.24 inference(rename_variables,[],[91])).
% 2.19/2.24 cnf(410,plain,
% 2.19/2.24 (P1(f6(a1),a3,f7(f7(a2,a4),a4))),
% 2.19/2.24 inference(scs_inference,[],[91,407,409,392,378,7,8,9])).
% 2.19/2.24 cnf(416,plain,
% 2.19/2.24 (P1(a1,f7(f7(a4,a2),a4),f7(a3,a4))),
% 2.19/2.24 inference(scs_inference,[],[21,380,8])).
% 2.19/2.24 cnf(417,plain,
% 2.19/2.24 (E(x4171,f7(x4171,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(419,plain,
% 2.19/2.24 (E(x4191,f7(x4191,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(420,plain,
% 2.19/2.24 (P1(f6(f7(a1,a4)),a3,f7(a2,a4))),
% 2.19/2.24 inference(scs_inference,[],[21,417,419,380,361,8,7,9])).
% 2.19/2.24 cnf(422,plain,
% 2.19/2.24 (P1(a1,f7(f7(a2,a4),a4),a3)),
% 2.19/2.24 inference(scs_inference,[],[21,417,419,13,12,380,361,410,8,7,9,20])).
% 2.19/2.24 cnf(434,plain,
% 2.19/2.24 (E(x4341,f7(x4341,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(436,plain,
% 2.19/2.24 (E(x4361,f7(x4361,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(437,plain,
% 2.19/2.24 (P1(a1,f7(f7(a2,a4),a4),f7(a3,a4))),
% 2.19/2.24 inference(scs_inference,[],[21,434,436,396,422,402,7,8,9])).
% 2.19/2.24 cnf(439,plain,
% 2.19/2.24 (P1(f7(a1,a4),f7(a2,a4),a3)),
% 2.19/2.24 inference(scs_inference,[],[21,434,436,27,396,422,402,420,312,7,8,9,20])).
% 2.19/2.24 cnf(443,plain,
% 2.19/2.24 (P1(a1,f7(a2,a4),a3)),
% 2.19/2.24 inference(scs_inference,[],[32,439,7])).
% 2.19/2.24 cnf(445,plain,
% 2.19/2.24 (P1(a1,a2,f7(a3,a4))),
% 2.19/2.24 inference(scs_inference,[],[74,32,439,437,7,8])).
% 2.19/2.24 cnf(447,plain,
% 2.19/2.24 (P1(f7(a1,a4),f7(a2,a4),f7(f7(a3,a4),a4))),
% 2.19/2.24 inference(scs_inference,[],[74,32,91,439,437,7,8,9])).
% 2.19/2.24 cnf(449,plain,
% 2.19/2.24 (P1(f6(a1),f7(a3,a4),f7(f7(a2,a4),a4))),
% 2.19/2.24 inference(scs_inference,[],[74,32,91,14,12,439,437,7,8,9,20])).
% 2.19/2.24 cnf(454,plain,
% 2.19/2.24 (E(f7(x4541,a4),x4541)),
% 2.19/2.24 inference(rename_variables,[],[32])).
% 2.19/2.24 cnf(457,plain,
% 2.19/2.24 (P1(f6(a1),f7(a3,a4),a2)),
% 2.19/2.24 inference(scs_inference,[],[74,32,454,447,449,7,8,9])).
% 2.19/2.24 cnf(464,plain,
% 2.19/2.24 (E(x4641,f7(x4641,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(465,plain,
% 2.19/2.24 (P1(a1,f7(a2,a4),f7(a3,a4))),
% 2.19/2.24 inference(scs_inference,[],[21,464,416,445,7,8])).
% 2.19/2.24 cnf(473,plain,
% 2.19/2.24 (P1(f7(f7(a1,a4),a4),f7(a2,a4),f7(a3,a4))),
% 2.19/2.24 inference(scs_inference,[],[91,465,7])).
% 2.19/2.24 cnf(484,plain,
% 2.19/2.24 (E(f7(x4841,a4),x4841)),
% 2.19/2.24 inference(rename_variables,[],[32])).
% 2.19/2.24 cnf(486,plain,
% 2.19/2.24 (E(f7(x4861,a4),x4861)),
% 2.19/2.24 inference(rename_variables,[],[32])).
% 2.19/2.24 cnf(489,plain,
% 2.19/2.24 (P1(f6(a1),a3,f7(a2,a4))),
% 2.19/2.24 inference(scs_inference,[],[32,484,486,14,12,473,443,7,8,9,20])).
% 2.19/2.24 cnf(493,plain,
% 2.19/2.24 (P1(a2,f7(a5,a4),f7(f6(a1),a4))),
% 2.19/2.24 inference(scs_inference,[],[21,400,8])).
% 2.19/2.24 cnf(494,plain,
% 2.19/2.24 (E(x4941,f7(x4941,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(495,plain,
% 2.19/2.24 (P1(f7(f6(a5),a4),f7(a5,a4),f6(a4))),
% 2.19/2.24 inference(scs_inference,[],[21,494,391,400,8,7])).
% 2.19/2.24 cnf(502,plain,
% 2.19/2.24 (P1(f7(f6(a5),a4),a5,f6(a4))),
% 2.19/2.24 inference(scs_inference,[],[32,495,8])).
% 2.19/2.24 cnf(516,plain,
% 2.19/2.24 (P1(f7(f6(a5),a4),a5,f7(a4,a4))),
% 2.19/2.24 inference(scs_inference,[],[168,502,250,8,9])).
% 2.19/2.24 cnf(520,plain,
% 2.19/2.24 (P1(x5201,x5202,f7(x5201,x5202))),
% 2.19/2.24 inference(rename_variables,[],[16])).
% 2.19/2.24 cnf(522,plain,
% 2.19/2.24 (E(f7(f7(a3,a4),a4),f7(a1,a2))),
% 2.19/2.24 inference(scs_inference,[],[10,74,16,18,3])).
% 2.19/2.24 cnf(524,plain,
% 2.19/2.24 (P1(f7(f6(a1),a4),a3,f7(a2,a4))),
% 2.19/2.24 inference(scs_inference,[],[10,74,21,489,16,18,3,7])).
% 2.19/2.24 cnf(525,plain,
% 2.19/2.24 (E(x5251,f7(x5251,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(530,plain,
% 2.19/2.24 (P1(a3,f6(a2),a1)),
% 2.19/2.24 inference(scs_inference,[],[10,74,32,21,525,43,489,516,112,16,18,3,7,8,9,19])).
% 2.19/2.24 cnf(534,plain,
% 2.19/2.24 (P1(a1,f7(a4,a4),f7(a3,f6(a2)))),
% 2.19/2.24 inference(scs_inference,[],[10,74,32,21,525,43,27,489,516,112,16,520,18,3,7,8,9,19,20])).
% 2.19/2.24 cnf(541,plain,
% 2.19/2.24 (P1(f7(f7(a3,a4),a4),f6(a2),a1)),
% 2.19/2.24 inference(scs_inference,[],[91,522,530,2,7])).
% 2.19/2.24 cnf(542,plain,
% 2.19/2.24 (E(x5421,f7(f7(x5421,a4),a4))),
% 2.19/2.24 inference(rename_variables,[],[91])).
% 2.19/2.24 cnf(543,plain,
% 2.19/2.24 (P1(a1,f6(a4),f7(a3,f6(a2)))),
% 2.19/2.24 inference(scs_inference,[],[179,91,522,534,530,2,7,8])).
% 2.19/2.24 cnf(544,plain,
% 2.19/2.24 (P1(a3,f6(a2),f7(f7(a1,a4),a4))),
% 2.19/2.24 inference(scs_inference,[],[179,91,542,522,534,530,2,7,8,9])).
% 2.19/2.24 cnf(546,plain,
% 2.19/2.24 (P1(a3,f6(a2),f7(a1,a4))),
% 2.19/2.24 inference(scs_inference,[],[10,179,91,542,522,61,534,530,112,2,7,8,9,19])).
% 2.19/2.24 cnf(550,plain,
% 2.19/2.24 (P1(f6(a1),f7(a3,f6(a2)),f7(a4,a4))),
% 2.19/2.24 inference(scs_inference,[],[10,179,91,542,522,61,14,12,534,530,112,2,7,8,9,19,20])).
% 2.19/2.24 cnf(556,plain,
% 2.19/2.24 (E(x5561,f7(x5561,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(559,plain,
% 2.19/2.24 (P1(f6(a1),f7(a3,f6(a2)),f6(a4))),
% 2.19/2.24 inference(scs_inference,[],[179,21,556,457,550,524,7,8,9])).
% 2.19/2.24 cnf(560,plain,
% 2.19/2.24 (P1(a3,a5,a4)),
% 2.19/2.24 inference(scs_inference,[],[10,179,21,556,134,457,550,524,400,7,8,9,19])).
% 2.19/2.24 cnf(563,plain,
% 2.19/2.24 (P1(f6(a3),f7(a1,a4),f6(a2))),
% 2.19/2.24 inference(scs_inference,[],[10,179,21,556,134,14,12,457,550,524,546,400,7,8,9,19,20])).
% 2.19/2.24 cnf(576,plain,
% 2.19/2.24 (P1(a1,a4,f7(f7(a1,a4),a4))),
% 2.19/2.24 inference(scs_inference,[],[10,140,32,91,134,13,563,559,544,560,493,7,8,9,19,20])).
% 2.19/2.24 cnf(580,plain,
% 2.19/2.24 (P1(f7(a1,a4),f6(a4),f7(a3,f6(a2)))),
% 2.19/2.24 inference(scs_inference,[],[21,543,7])).
% 2.19/2.24 cnf(581,plain,
% 2.19/2.24 (E(x5811,f7(x5811,a4))),
% 2.19/2.24 inference(rename_variables,[],[21])).
% 2.19/2.24 cnf(585,plain,
% 2.19/2.24 (P1(a3,f7(a5,a4),f7(a4,a4))),
% 2.19/2.24 inference(scs_inference,[],[10,138,21,581,27,576,541,543,383,7,8,9,19])).
% 2.19/2.24 cnf(588,plain,
% 2.19/2.24 (P1(f6(a1),f7(f7(a1,a4),a4),a4)),
% 2.19/2.24 inference(scs_inference,[],[10,138,21,581,27,11,14,576,541,543,383,7,8,9,19,20])).
% 2.19/2.24 cnf(593,plain,
% 2.19/2.24 (P1(f7(f7(a3,a4),a4),f7(a5,a4),f7(a4,a4))),
% 2.19/2.24 inference(scs_inference,[],[91,585,7])).
% 2.19/2.24 cnf(600,plain,
% 2.19/2.24 (P1(f6(a3),f7(a4,a4),f7(a5,a4))),
% 2.19/2.24 inference(scs_inference,[],[10,168,138,91,13,14,12,588,580,585,373,7,8,9,19,20])).
% 2.19/2.24 cnf(605,plain,
% 2.19/2.24 (P1(f7(f6(a3),a4),f7(a4,a4),f7(a5,a4))),
% 2.19/2.24 inference(scs_inference,[],[21,600,7])).
% 2.19/2.24 cnf(609,plain,
% 2.19/2.24 (P1(f7(f7(a3,a4),a4),f7(a5,a4),f6(a4))),
% 2.19/2.24 inference(scs_inference,[],[179,32,21,593,600,7,8,9])).
% 2.19/2.24 cnf(620,plain,
% 2.19/2.24 (P1(f7(f6(a3),a4),f6(a4),f7(a5,a4))),
% 2.19/2.24 inference(scs_inference,[],[179,74,605,609,7,8])).
% 2.19/2.24 cnf(632,plain,
% 2.19/2.24 (P1(f6(a3),f6(a4),f7(a5,a4))),
% 2.19/2.24 inference(scs_inference,[],[32,620,7])).
% 2.19/2.24 cnf(646,plain,
% 2.19/2.24 (P1(f7(x6461,a4),a4,x6461)),
% 2.19/2.24 inference(rename_variables,[],[24])).
% 2.19/2.24 cnf(648,plain,
% 2.19/2.24 (~E(f7(f6(a3),a4),f7(a5,a4))),
% 2.19/2.24 inference(scs_inference,[],[17,24,646,18,7])).
% 2.19/2.24 cnf(761,plain,
% 2.19/2.24 ($false),
% 2.19/2.24 inference(scs_inference,[],[648,632,348,18]),
% 2.19/2.24 ['proof']).
% 2.19/2.24 % SZS output end Proof
% 2.19/2.24 % Total time :1.590000s
%------------------------------------------------------------------------------