%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP009-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 : n026.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:26 EDT 2024
% Result : Unsatisfiable 2.69s 2.84s
% Output : CNFRefutation 2.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : GRP009-1 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.31 % Computer : n026.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Thu Jun 20 10:10:24 EDT 2024
% 0.11/0.31 % CPUTime :
% 0.16/0.49 start to proof:theBenchmark
% 2.69/2.83 %-------------------------------------------
% 2.69/2.83 % File :CSE---1.7
% 2.69/2.83 % Problem :theBenchmark
% 2.69/2.83 % Transform :cnf
% 2.69/2.83 % Format :tptp:raw
% 2.69/2.83 % Command :java -jar mcs_scs.jar %d %s
% 2.69/2.83
% 2.69/2.83 % Result :Theorem 2.310000s
% 2.69/2.83 % Output :CNFRefutation 2.310000s
% 2.69/2.83 %-------------------------------------------
% 2.69/2.84 %--------------------------------------------------------------------------
% 2.69/2.84 % File : GRP009-1 : TPTP v8.2.0. Released v1.0.0.
% 2.69/2.84 % Domain : Group Theory
% 2.69/2.84 % Problem : The left inverse of an element is unique
% 2.69/2.84 % Version : [MOW76] axioms.
% 2.69/2.84 % English :
% 2.69/2.84
% 2.69/2.84 % Refs : [Wos65] Wos (1965), Unpublished Note
% 2.69/2.84 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 2.69/2.84 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 2.69/2.84 % Source : [SPRFN]
% 2.69/2.84 % Names : Problem 6 [Wos65]
% 2.69/2.84 % : wos6 [WM76]
% 2.69/2.84
% 2.69/2.84 % Status : Unsatisfiable
% 2.69/2.84 % 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.00 v2.0.0
% 2.69/2.84 % Syntax : Number of clauses : 11 ( 8 unt; 0 nHn; 6 RR)
% 2.69/2.84 % Number of literals : 19 ( 2 equ; 9 neg)
% 2.69/2.84 % Maximal clause size : 4 ( 1 avg)
% 2.69/2.84 % Maximal term depth : 2 ( 1 avg)
% 2.69/2.84 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 2.69/2.84 % Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% 2.69/2.84 % Number of variables : 22 ( 0 sgn)
% 2.69/2.84 % SPC : CNF_UNS_RFO_SEQ_HRN
% 2.69/2.84
% 2.69/2.84 % Comments :
% 2.69/2.84 %--------------------------------------------------------------------------
% 2.69/2.84 %----Include group theory axioms
% 2.69/2.84 include('Axioms/GRP003-0.ax').
% 2.69/2.84 %--------------------------------------------------------------------------
% 2.69/2.84 cnf(a_is_an_inverse_of_b,hypothesis,
% 2.69/2.84 product(a,b,identity) ).
% 2.69/2.84
% 2.69/2.84 cnf(c_is_an_inverse_of_b,hypothesis,
% 2.69/2.84 product(c,b,identity) ).
% 2.69/2.84
% 2.69/2.84 cnf(prove_a_equals_c,negated_conjecture,
% 2.69/2.84 a != c ).
% 2.69/2.84
% 2.69/2.84 %--------------------------------------------------------------------------
% 2.69/2.84 %-------------------------------------------
% 2.69/2.84 % Proof found
% 2.69/2.84 % SZS status Theorem for theBenchmark
% 2.69/2.84 % SZS output start Proof
% 2.69/2.84 %ClaNum:20(EqnAxiom:9)
% 2.69/2.84 %VarNum:44(SingletonVarNum:22)
% 2.69/2.84 %MaxLitNum:4
% 2.69/2.84 %MaxfuncDepth:1
% 2.69/2.84 %SharedTerms:7
% 2.69/2.84 %goalClause: 17
% 2.69/2.84 %singleGoalClaCount:1
% 2.69/2.84 [10]P1(a1,a2,a3)
% 2.69/2.84 [11]P1(a4,a2,a3)
% 2.69/2.84 [17]~E(a4,a1)
% 2.69/2.84 [12]P1(x121,a3,x121)
% 2.69/2.84 [13]P1(a3,x131,x131)
% 2.69/2.84 [14]P1(x141,f5(x141),a3)
% 2.69/2.84 [15]P1(f5(x151),x151,a3)
% 2.69/2.84 [16]P1(x161,x162,f6(x161,x162))
% 2.69/2.84 [18]~P1(x183,x184,x181)+E(x181,x182)+~P1(x183,x184,x182)
% 2.69/2.84 [19]~P1(x196,x194,x191)+P1(x191,x192,x193)+~P1(x194,x192,x195)+~P1(x196,x195,x193)
% 2.69/2.84 [20]~P1(x201,x206,x204)+P1(x201,x202,x203)+~P1(x204,x205,x203)+~P1(x206,x205,x202)
% 2.69/2.84 %EqnAxiom
% 2.69/2.84 [1]E(x11,x11)
% 2.69/2.84 [2]E(x22,x21)+~E(x21,x22)
% 2.69/2.84 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 2.69/2.84 [4]~E(x41,x42)+E(f5(x41),f5(x42))
% 2.69/2.84 [5]~E(x51,x52)+E(f6(x51,x53),f6(x52,x53))
% 2.69/2.84 [6]~E(x61,x62)+E(f6(x63,x61),f6(x63,x62))
% 2.69/2.84 [7]P1(x72,x73,x74)+~E(x71,x72)+~P1(x71,x73,x74)
% 2.69/2.84 [8]P1(x83,x82,x84)+~E(x81,x82)+~P1(x83,x81,x84)
% 2.69/2.84 [9]P1(x93,x94,x92)+~E(x91,x92)+~P1(x93,x94,x91)
% 2.69/2.84
% 2.69/2.84 %-------------------------------------------
% 2.69/2.85 cnf(21,plain,
% 2.69/2.85 (E(x211,f6(x211,a3))),
% 2.69/2.85 inference(scs_inference,[],[12,16,18])).
% 2.69/2.85 cnf(22,plain,
% 2.69/2.85 (P1(x221,x222,f6(x221,x222))),
% 2.69/2.85 inference(rename_variables,[],[16])).
% 2.69/2.85 cnf(24,plain,
% 2.69/2.85 (P1(f6(x241,a3),a3,x241)),
% 2.69/2.85 inference(scs_inference,[],[12,16,18,7])).
% 2.69/2.85 cnf(26,plain,
% 2.69/2.85 (P1(x261,a3,x261)),
% 2.69/2.85 inference(rename_variables,[],[12])).
% 2.69/2.85 cnf(27,plain,
% 2.69/2.85 (P1(x271,f5(x271),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[12,16,14,18,7,8,9])).
% 2.69/2.85 cnf(28,plain,
% 2.69/2.85 (P1(x281,f6(a3,a3),x281)),
% 2.69/2.85 inference(scs_inference,[],[12,26,16,22,14,18,7,8,9,20])).
% 2.69/2.85 cnf(32,plain,
% 2.69/2.85 (E(f6(x321,a3),x321)),
% 2.69/2.85 inference(scs_inference,[],[21,2])).
% 2.69/2.85 cnf(33,plain,
% 2.69/2.85 (~E(a4,f6(a1,a3))),
% 2.69/2.85 inference(scs_inference,[],[17,21,2,3])).
% 2.69/2.85 cnf(34,plain,
% 2.69/2.85 (E(f5(f6(a3,a3)),a3)),
% 2.69/2.85 inference(scs_inference,[],[17,21,28,15,2,3,18])).
% 2.69/2.85 cnf(36,plain,
% 2.69/2.85 (P1(x361,f6(a3,a3),x361)),
% 2.69/2.85 inference(rename_variables,[],[28])).
% 2.69/2.85 cnf(39,plain,
% 2.69/2.85 (P1(x391,f6(a3,a3),x391)),
% 2.69/2.85 inference(rename_variables,[],[28])).
% 2.69/2.85 cnf(40,plain,
% 2.69/2.85 (E(x401,f6(x401,a3))),
% 2.69/2.85 inference(rename_variables,[],[21])).
% 2.69/2.85 cnf(41,plain,
% 2.69/2.85 (P1(f6(x411,a3),f6(a3,a3),x411)),
% 2.69/2.85 inference(scs_inference,[],[17,21,40,28,36,39,15,2,3,18,9,7])).
% 2.69/2.85 cnf(42,plain,
% 2.69/2.85 (P1(x421,f6(a3,a3),x421)),
% 2.69/2.85 inference(rename_variables,[],[28])).
% 2.69/2.85 cnf(43,plain,
% 2.69/2.85 (P1(x431,f6(f6(a3,a3),a3),x431)),
% 2.69/2.85 inference(scs_inference,[],[17,21,40,28,36,39,42,15,2,3,18,9,7,8])).
% 2.69/2.85 cnf(45,plain,
% 2.69/2.85 (P1(a3,f5(f6(a3,a3)),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[17,21,40,28,36,39,42,27,13,15,2,3,18,9,7,8,19])).
% 2.69/2.85 cnf(47,plain,
% 2.69/2.85 (P1(x471,f6(a3,a3),x471)),
% 2.69/2.85 inference(rename_variables,[],[28])).
% 2.69/2.85 cnf(50,plain,
% 2.69/2.85 (P1(x501,f6(f6(a3,a3),f6(a3,a3)),x501)),
% 2.69/2.85 inference(scs_inference,[],[17,21,40,28,36,39,42,47,27,13,15,16,2,3,18,9,7,8,19,20])).
% 2.69/2.85 cnf(53,plain,
% 2.69/2.85 (E(a3,f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[34,2])).
% 2.69/2.85 cnf(54,plain,
% 2.69/2.85 (P1(f6(x541,a3),f6(f6(a3,a3),f6(a3,a3)),x541)),
% 2.69/2.85 inference(scs_inference,[],[32,34,50,2,9])).
% 2.69/2.85 cnf(55,plain,
% 2.69/2.85 (P1(x551,f6(f6(a3,a3),f6(a3,a3)),x551)),
% 2.69/2.85 inference(rename_variables,[],[50])).
% 2.69/2.85 cnf(56,plain,
% 2.69/2.85 (E(f6(a3,a3),f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[32,34,50,2,9,3])).
% 2.69/2.85 cnf(57,plain,
% 2.69/2.85 (E(f6(x571,a3),x571)),
% 2.69/2.85 inference(rename_variables,[],[32])).
% 2.69/2.85 cnf(58,plain,
% 2.69/2.85 (E(a3,f6(f6(a3,a3),f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[32,34,50,55,13,2,9,3,18])).
% 2.69/2.85 cnf(60,plain,
% 2.69/2.85 (P1(x601,f6(f6(a3,a3),f6(a3,a3)),x601)),
% 2.69/2.85 inference(rename_variables,[],[50])).
% 2.69/2.85 cnf(62,plain,
% 2.69/2.85 (P1(x621,f6(f6(a3,a3),f6(a3,a3)),f6(x621,a3))),
% 2.69/2.85 inference(scs_inference,[],[32,57,34,50,55,60,13,2,9,3,18,7])).
% 2.69/2.85 cnf(63,plain,
% 2.69/2.85 (P1(x631,f6(f6(a3,a3),f6(a3,a3)),x631)),
% 2.69/2.85 inference(rename_variables,[],[50])).
% 2.69/2.85 cnf(64,plain,
% 2.69/2.85 (P1(a1,f6(a2,a3),a3)),
% 2.69/2.85 inference(scs_inference,[],[32,57,34,21,50,55,60,10,13,2,9,3,18,7,8])).
% 2.69/2.85 cnf(66,plain,
% 2.69/2.85 (P1(f6(f6(a3,a3),f6(a3,a3)),f6(a3,a3),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[32,57,34,21,50,55,60,63,10,27,13,2,9,3,18,7,8,20])).
% 2.69/2.85 cnf(73,plain,
% 2.69/2.85 (E(f5(f6(a3,a3)),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[56,2])).
% 2.69/2.85 cnf(74,plain,
% 2.69/2.85 (E(f6(f6(x741,a3),a3),x741)),
% 2.69/2.85 inference(scs_inference,[],[56,62,54,2,18])).
% 2.69/2.85 cnf(75,plain,
% 2.69/2.85 (P1(x751,f6(f6(a3,a3),f6(a3,a3)),f6(x751,a3))),
% 2.69/2.85 inference(rename_variables,[],[62])).
% 2.69/2.85 cnf(78,plain,
% 2.69/2.85 (~E(a4,f6(f6(a1,a3),a3))),
% 2.69/2.85 inference(scs_inference,[],[17,56,58,62,54,64,2,18,9,3])).
% 2.69/2.85 cnf(79,plain,
% 2.69/2.85 (P1(f5(f6(a3,a3)),a3,a3)),
% 2.69/2.85 inference(scs_inference,[],[17,56,58,62,54,24,64,2,18,9,3,7])).
% 2.69/2.85 cnf(81,plain,
% 2.69/2.85 (P1(f6(x811,a3),f5(f6(a3,a3)),x811)),
% 2.69/2.85 inference(scs_inference,[],[17,56,58,62,54,41,24,64,2,18,9,3,7,8])).
% 2.69/2.85 cnf(82,plain,
% 2.69/2.85 (P1(f6(f6(x821,a3),a3),f6(a3,a3),x821)),
% 2.69/2.85 inference(scs_inference,[],[17,56,58,66,62,75,54,41,24,64,2,18,9,3,7,8,19])).
% 2.69/2.85 cnf(83,plain,
% 2.69/2.85 (P1(x831,f6(f6(a3,a3),f6(a3,a3)),f6(x831,a3))),
% 2.69/2.85 inference(rename_variables,[],[62])).
% 2.69/2.85 cnf(85,plain,
% 2.69/2.85 (P1(f5(f6(a1,a3)),a1,f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[17,56,58,66,62,75,83,54,41,24,64,15,2,18,9,3,7,8,19,20])).
% 2.69/2.85 cnf(90,plain,
% 2.69/2.85 (E(x901,f6(f6(x901,a3),a3))),
% 2.69/2.85 inference(scs_inference,[],[74,2])).
% 2.69/2.85 cnf(91,plain,
% 2.69/2.85 (P1(f5(f6(a1,a3)),a1,a3)),
% 2.69/2.85 inference(scs_inference,[],[74,32,85,2,9])).
% 2.69/2.85 cnf(92,plain,
% 2.69/2.85 (E(f6(x921,a3),x921)),
% 2.69/2.85 inference(rename_variables,[],[32])).
% 2.69/2.85 cnf(93,plain,
% 2.69/2.85 (P1(x931,f5(f6(a3,a3)),f6(x931,a3))),
% 2.69/2.85 inference(scs_inference,[],[74,32,81,85,2,9,7])).
% 2.69/2.85 cnf(94,plain,
% 2.69/2.85 (P1(f6(x941,a3),f5(f6(a3,a3)),x941)),
% 2.69/2.85 inference(rename_variables,[],[81])).
% 2.69/2.85 cnf(95,plain,
% 2.69/2.85 (P1(f6(f6(x951,a3),a3),a3,x951)),
% 2.69/2.85 inference(scs_inference,[],[74,32,92,81,82,85,2,9,7,8])).
% 2.69/2.85 cnf(97,plain,
% 2.69/2.85 (P1(x971,f5(f6(a3,a3)),x971)),
% 2.69/2.85 inference(scs_inference,[],[74,32,92,43,81,94,82,85,28,2,9,7,8,19])).
% 2.69/2.85 cnf(101,plain,
% 2.69/2.85 (P1(f5(f6(a3,a3)),f6(a3,a3),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[74,32,92,43,81,94,82,85,45,79,28,2,9,7,8,19,20])).
% 2.69/2.85 cnf(104,plain,
% 2.69/2.85 (P1(a4,a2,f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[53,58,11,2,9])).
% 2.69/2.85 cnf(105,plain,
% 2.69/2.85 (P1(x1051,f6(a3,a3),f6(x1051,a3))),
% 2.69/2.85 inference(scs_inference,[],[73,53,58,93,11,2,9,8])).
% 2.69/2.85 cnf(106,plain,
% 2.69/2.85 (P1(f6(f6(a4,a3),a3),a2,a3)),
% 2.69/2.85 inference(scs_inference,[],[73,53,90,58,93,11,2,9,8,7])).
% 2.69/2.85 cnf(108,plain,
% 2.69/2.85 (P1(f6(a3,a3),f6(a3,a3),f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[73,53,90,58,101,93,11,50,16,2,9,8,7,19])).
% 2.69/2.85 cnf(112,plain,
% 2.69/2.85 (P1(f5(f6(a1,a3)),a3,f6(a2,a3))),
% 2.69/2.85 inference(scs_inference,[],[73,53,90,58,101,93,91,11,50,64,13,16,2,9,8,7,19,20])).
% 2.69/2.85 cnf(115,plain,
% 2.69/2.85 (E(f6(a2,a3),f5(f6(a1,a3)))),
% 2.69/2.85 inference(scs_inference,[],[112,12,18])).
% 2.69/2.85 cnf(116,plain,
% 2.69/2.85 (P1(x1161,a3,x1161)),
% 2.69/2.85 inference(rename_variables,[],[12])).
% 2.69/2.85 cnf(118,plain,
% 2.69/2.85 (P1(f6(f6(a1,a3),a3),a2,a3)),
% 2.69/2.85 inference(scs_inference,[],[90,112,10,12,18,7])).
% 2.69/2.85 cnf(119,plain,
% 2.69/2.85 (E(x1191,f6(f6(x1191,a3),a3))),
% 2.69/2.85 inference(rename_variables,[],[90])).
% 2.69/2.85 cnf(120,plain,
% 2.69/2.85 (P1(a4,a2,f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[73,90,112,104,10,12,18,7,9])).
% 2.69/2.85 cnf(121,plain,
% 2.69/2.85 (P1(a1,f6(f6(a2,a3),a3),a3)),
% 2.69/2.85 inference(scs_inference,[],[73,90,119,112,104,10,12,18,7,9,8])).
% 2.69/2.85 cnf(123,plain,
% 2.69/2.85 (P1(f6(x1231,a3),f6(f6(a3,a3),a3),x1231)),
% 2.69/2.85 inference(scs_inference,[],[73,90,119,97,112,104,43,81,10,12,18,7,9,8,19])).
% 2.69/2.85 cnf(127,plain,
% 2.69/2.85 (P1(f6(a1,a3),f6(a2,a3),a3)),
% 2.69/2.85 inference(scs_inference,[],[73,90,119,97,112,104,43,81,14,10,12,116,18,7,9,8,19,20])).
% 2.69/2.85 cnf(131,plain,
% 2.69/2.85 (E(f5(f6(a1,a3)),f6(a2,a3))),
% 2.69/2.85 inference(scs_inference,[],[115,2])).
% 2.69/2.85 cnf(132,plain,
% 2.69/2.85 (P1(f6(f6(a4,a3),a3),a2,f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[115,90,120,2,7])).
% 2.69/2.85 cnf(133,plain,
% 2.69/2.85 (E(x1331,f6(f6(x1331,a3),a3))),
% 2.69/2.85 inference(rename_variables,[],[90])).
% 2.69/2.85 cnf(134,plain,
% 2.69/2.85 (P1(a4,f6(f6(a2,a3),a3),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[115,90,133,120,2,7,8])).
% 2.69/2.85 cnf(136,plain,
% 2.69/2.85 (P1(a2,f6(a3,a3),f5(f6(a1,a3)))),
% 2.69/2.85 inference(scs_inference,[],[115,90,133,105,120,2,7,8,9])).
% 2.69/2.85 cnf(138,plain,
% 2.69/2.85 (P1(f6(a3,a3),a3,f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[115,90,133,108,105,123,120,43,2,7,8,9,20])).
% 2.69/2.85 cnf(142,plain,
% 2.69/2.85 (E(f5(f6(a1,a3)),a2)),
% 2.69/2.85 inference(scs_inference,[],[136,28,18])).
% 2.69/2.85 cnf(145,plain,
% 2.69/2.85 (P1(f6(a1,a3),f6(a2,a3),f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[53,127,136,28,18,9])).
% 2.69/2.85 cnf(146,plain,
% 2.69/2.85 (P1(f6(f6(a1,a3),a3),f6(a2,a3),a3)),
% 2.69/2.85 inference(scs_inference,[],[53,21,127,136,28,18,9,7])).
% 2.69/2.85 cnf(147,plain,
% 2.69/2.85 (E(x1471,f6(x1471,a3))),
% 2.69/2.85 inference(rename_variables,[],[21])).
% 2.69/2.85 cnf(148,plain,
% 2.69/2.85 (P1(f6(f6(a4,a3),a3),f6(a2,a3),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[53,21,147,127,136,132,28,18,9,7,8])).
% 2.69/2.85 cnf(150,plain,
% 2.69/2.85 (P1(f6(a3,a3),f5(a2),a4)),
% 2.69/2.85 inference(scs_inference,[],[53,21,147,127,136,132,95,28,14,18,9,7,8,19])).
% 2.69/2.85 cnf(154,plain,
% 2.69/2.85 (P1(f5(a4),f6(a3,a3),f6(f6(a2,a3),a3))),
% 2.69/2.85 inference(scs_inference,[],[53,21,147,127,136,134,132,95,28,14,15,13,18,9,7,8,19,20])).
% 2.69/2.85 cnf(158,plain,
% 2.69/2.85 (E(a2,f5(f6(a1,a3)))),
% 2.69/2.85 inference(scs_inference,[],[53,21,147,127,136,134,132,95,28,14,15,13,18,9,7,8,19,20,2])).
% 2.69/2.85 cnf(162,plain,
% 2.69/2.85 (P1(f5(a4),f6(a3,a3),a2)),
% 2.69/2.85 inference(scs_inference,[],[74,154,28,18,9])).
% 2.69/2.85 cnf(164,plain,
% 2.69/2.85 (P1(f6(a1,a3),f6(a2,a3),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[131,74,154,27,28,18,9,8])).
% 2.69/2.85 cnf(165,plain,
% 2.69/2.85 (P1(x1651,f5(x1651),f6(a3,a3))),
% 2.69/2.85 inference(rename_variables,[],[27])).
% 2.69/2.85 cnf(168,plain,
% 2.69/2.85 (P1(f6(a3,a3),f5(f6(a2,a3)),a4)),
% 2.69/2.85 inference(scs_inference,[],[131,74,32,145,148,154,82,27,165,28,18,9,8,7,19])).
% 2.69/2.85 cnf(172,plain,
% 2.69/2.85 (P1(f5(a4),f5(f6(a3,a3)),f6(a2,a3))),
% 2.69/2.85 inference(scs_inference,[],[131,74,32,145,148,138,154,82,24,27,165,28,18,9,8,7,19,20])).
% 2.69/2.85 cnf(175,plain,
% 2.69/2.85 (E(f5(a4),f6(f6(a2,a3),a3))),
% 2.69/2.85 inference(scs_inference,[],[131,74,32,145,148,138,154,82,24,27,165,28,18,9,8,7,19,20,2])).
% 2.69/2.85 cnf(176,plain,
% 2.69/2.85 (E(f6(a2,a3),f5(a4))),
% 2.69/2.85 inference(scs_inference,[],[172,97,18])).
% 2.69/2.85 cnf(177,plain,
% 2.69/2.85 (P1(x1771,f5(f6(a3,a3)),x1771)),
% 2.69/2.85 inference(rename_variables,[],[97])).
% 2.69/2.85 cnf(179,plain,
% 2.69/2.85 (E(f5(f6(a1,a3)),f5(a4))),
% 2.69/2.85 inference(scs_inference,[],[131,172,97,18,3])).
% 2.69/2.85 cnf(180,plain,
% 2.69/2.85 (P1(f5(f6(a3,a3)),f5(a2),a4)),
% 2.69/2.85 inference(scs_inference,[],[131,56,172,150,97,18,3,7])).
% 2.69/2.85 cnf(183,plain,
% 2.69/2.85 (P1(f5(a4),a3,f6(a2,a3))),
% 2.69/2.85 inference(scs_inference,[],[34,131,56,90,172,150,97,18,3,7,9,8])).
% 2.69/2.85 cnf(188,plain,
% 2.69/2.85 (P1(a4,f6(a2,a3),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[34,131,56,90,172,146,150,97,177,95,27,14,18,3,7,9,8,19,20])).
% 2.69/2.85 cnf(192,plain,
% 2.69/2.85 (E(f5(a4),f6(a2,a3))),
% 2.69/2.85 inference(scs_inference,[],[34,131,56,90,172,146,150,97,177,95,27,14,18,3,7,9,8,19,20,2])).
% 2.69/2.85 cnf(193,plain,
% 2.69/2.85 (E(f5(a4),f5(f6(a1,a3)))),
% 2.69/2.85 inference(scs_inference,[],[179,2])).
% 2.69/2.85 cnf(194,plain,
% 2.69/2.85 (E(a2,f6(f5(a4),a3))),
% 2.69/2.85 inference(scs_inference,[],[179,162,105,2,18])).
% 2.69/2.85 cnf(197,plain,
% 2.69/2.85 (E(a2,f5(a4))),
% 2.69/2.85 inference(scs_inference,[],[158,179,162,105,2,18,3])).
% 2.69/2.85 cnf(198,plain,
% 2.69/2.85 (P1(f6(a3,a3),f5(f6(a2,a3)),f6(a4,a3))),
% 2.69/2.85 inference(scs_inference,[],[158,179,21,168,162,105,2,18,3,9])).
% 2.69/2.85 cnf(199,plain,
% 2.69/2.85 (E(x1991,f6(x1991,a3))),
% 2.69/2.85 inference(rename_variables,[],[21])).
% 2.69/2.85 cnf(200,plain,
% 2.69/2.85 (P1(f6(a1,a3),f5(a4),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[158,176,179,21,164,168,162,105,2,18,3,9,8])).
% 2.69/2.85 cnf(201,plain,
% 2.69/2.85 (P1(f6(f6(a1,a3),a3),f6(a2,a3),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[158,176,179,21,199,164,168,162,105,2,18,3,9,8,7])).
% 2.69/2.85 cnf(203,plain,
% 2.69/2.85 (P1(f6(a3,a3),f5(f6(a2,a3)),a1)),
% 2.69/2.85 inference(scs_inference,[],[158,176,179,21,199,164,168,162,105,41,27,2,18,3,9,8,7,19])).
% 2.69/2.85 cnf(211,plain,
% 2.69/2.85 (E(f5(a4),a2)),
% 2.69/2.85 inference(scs_inference,[],[142,193,194,2,3])).
% 2.69/2.85 cnf(212,plain,
% 2.69/2.85 (P1(f6(a1,a3),f5(a4),f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[142,193,194,56,200,2,3,9])).
% 2.69/2.85 cnf(213,plain,
% 2.69/2.85 (P1(f6(f6(a1,a3),a3),f5(a4),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[142,193,194,176,56,201,200,2,3,9,8])).
% 2.69/2.85 cnf(214,plain,
% 2.69/2.85 (P1(a1,f6(a2,a3),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[142,193,194,176,74,56,201,200,2,3,9,8,7])).
% 2.69/2.85 cnf(216,plain,
% 2.69/2.85 (P1(f6(a3,a3),f5(f6(a2,a3)),f6(a1,a3))),
% 2.69/2.85 inference(scs_inference,[],[142,193,194,176,74,56,201,200,24,14,2,3,9,8,7,19])).
% 2.69/2.85 cnf(220,plain,
% 2.69/2.85 (P1(f5(f6(a3,a3)),f6(a4,a3),f6(a4,a3))),
% 2.69/2.85 inference(scs_inference,[],[142,193,194,176,74,56,201,198,200,101,24,14,2,3,9,8,7,19,20])).
% 2.69/2.85 cnf(222,plain,
% 2.69/2.85 (P1(f5(f6(a3,a3)),f6(a4,a3),a4)),
% 2.69/2.85 inference(scs_inference,[],[32,220,9])).
% 2.69/2.85 cnf(223,plain,
% 2.69/2.85 (E(f6(x2231,a3),x2231)),
% 2.69/2.85 inference(rename_variables,[],[32])).
% 2.69/2.85 cnf(224,plain,
% 2.69/2.85 (P1(f5(f6(a3,a3)),a4,f6(a4,a3))),
% 2.69/2.85 inference(scs_inference,[],[32,223,220,9,8])).
% 2.69/2.85 cnf(225,plain,
% 2.69/2.85 (E(f6(x2251,a3),x2251)),
% 2.69/2.85 inference(rename_variables,[],[32])).
% 2.69/2.85 cnf(226,plain,
% 2.69/2.85 (P1(a3,f5(f6(a2,a3)),f6(a1,a3))),
% 2.69/2.85 inference(scs_inference,[],[32,223,225,216,220,9,8,7])).
% 2.69/2.85 cnf(228,plain,
% 2.69/2.85 (P1(f6(a3,a3),f5(f5(a4)),a1)),
% 2.69/2.85 inference(scs_inference,[],[32,223,225,216,220,213,82,27,9,8,7,19])).
% 2.69/2.85 cnf(232,plain,
% 2.69/2.85 (P1(a3,f6(a3,a3),f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[32,223,225,216,220,213,108,66,62,82,27,9,8,7,19,20])).
% 2.69/2.85 cnf(235,plain,
% 2.69/2.85 (P1(f5(f6(a1,a3)),a3,f5(a4))),
% 2.69/2.85 inference(scs_inference,[],[176,112,9])).
% 2.69/2.85 cnf(236,plain,
% 2.69/2.85 (P1(a1,f5(a4),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[176,214,112,9,8])).
% 2.69/2.85 cnf(237,plain,
% 2.69/2.85 (P1(f6(a3,a3),f6(a4,a3),a4)),
% 2.69/2.85 inference(scs_inference,[],[73,176,214,222,112,9,8,7])).
% 2.69/2.85 cnf(238,plain,
% 2.69/2.85 (P1(a3,f5(a2),a1)),
% 2.69/2.85 inference(scs_inference,[],[73,176,214,222,118,112,95,14,9,8,7,19])).
% 2.69/2.85 cnf(242,plain,
% 2.69/2.85 (P1(f5(f6(a3,a3)),a4,a4)),
% 2.69/2.85 inference(scs_inference,[],[73,176,214,222,118,97,112,95,14,9,8,7,19,20])).
% 2.69/2.85 cnf(245,plain,
% 2.69/2.85 (P1(f6(a1,a3),f5(a4),a3)),
% 2.69/2.85 inference(scs_inference,[],[34,212,9])).
% 2.69/2.85 cnf(246,plain,
% 2.69/2.85 (P1(a4,f5(f6(a1,a3)),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[34,115,212,188,9,8])).
% 2.69/2.85 cnf(247,plain,
% 2.69/2.85 (P1(a3,a4,f6(a4,a3))),
% 2.69/2.85 inference(scs_inference,[],[34,115,212,188,224,9,8,7])).
% 2.69/2.85 cnf(248,plain,
% 2.69/2.85 (P1(a3,f5(a2),a4)),
% 2.69/2.85 inference(scs_inference,[],[34,115,212,188,224,106,82,27,9,8,7,19])).
% 2.69/2.85 cnf(252,plain,
% 2.69/2.85 (P1(x2521,a4,f6(f6(x2521,a3),a4))),
% 2.69/2.85 inference(scs_inference,[],[34,115,212,242,188,224,106,93,82,16,27,9,8,7,19,20])).
% 2.69/2.85 cnf(256,plain,
% 2.69/2.85 (P1(f6(a3,a3),f6(a4,a3),f6(f6(a4,a3),a3))),
% 2.69/2.85 inference(scs_inference,[],[90,237,9])).
% 2.69/2.85 cnf(259,plain,
% 2.69/2.85 (P1(f5(a4),a4,f6(f6(a2,a3),a4))),
% 2.69/2.85 inference(scs_inference,[],[197,175,90,237,252,236,9,8,7])).
% 2.69/2.85 cnf(261,plain,
% 2.69/2.85 (P1(a4,f5(a4),f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[197,175,90,237,246,252,236,235,138,9,8,7,20])).
% 2.69/2.85 cnf(263,plain,
% 2.69/2.85 (E(f6(a4,a3),f6(f6(a3,a3),a4))),
% 2.69/2.85 inference(scs_inference,[],[247,252,18])).
% 2.69/2.85 cnf(267,plain,
% 2.69/2.85 (E(x2671,f6(x2671,a3))),
% 2.69/2.85 inference(rename_variables,[],[21])).
% 2.69/2.85 cnf(268,plain,
% 2.69/2.85 (P1(a4,f6(a2,a3),f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[192,21,261,247,228,252,18,9,8])).
% 2.69/2.85 cnf(269,plain,
% 2.69/2.85 (P1(f6(a4,a3),f5(a4),f5(f6(a3,a3)))),
% 2.69/2.85 inference(scs_inference,[],[192,21,267,261,247,228,252,18,9,8,7])).
% 2.69/2.85 cnf(271,plain,
% 2.69/2.85 (P1(f6(f6(a4,a3),a3),f5(a4),a3)),
% 2.69/2.85 inference(scs_inference,[],[192,21,267,256,261,247,228,252,81,18,9,8,7,19])).
% 2.69/2.85 cnf(274,plain,
% 2.69/2.85 (P1(a3,f6(f6(a4,a3),a3),f6(a4,a3))),
% 2.69/2.85 inference(scs_inference,[],[192,21,267,256,232,261,247,228,252,220,81,18,9,8,7,19,20])).
% 2.69/2.85 cnf(278,plain,
% 2.69/2.85 (P1(f5(x2781),x2781,a3)),
% 2.69/2.85 inference(rename_variables,[],[15])).
% 2.69/2.85 cnf(280,plain,
% 2.69/2.85 (P1(f6(a4,a3),f5(a4),f6(a3,a3))),
% 2.69/2.85 inference(scs_inference,[],[73,269,259,15,18,9])).
% 2.69/2.85 cnf(281,plain,
% 2.69/2.86 (P1(f6(a4,a3),a2,f5(f6(a3,a3)))),
% 2.69/2.86 inference(scs_inference,[],[211,73,269,259,15,18,9,8])).
% 2.69/2.86 cnf(282,plain,
% 2.69/2.86 (P1(a1,f5(a4),a3)),
% 2.69/2.86 inference(scs_inference,[],[211,73,32,269,245,259,15,18,9,8,7])).
% 2.69/2.86 cnf(284,plain,
% 2.69/2.86 (P1(f6(a2,a3),f5(a2),a3)),
% 2.69/2.86 inference(scs_inference,[],[211,73,32,269,245,183,259,248,15,278,18,9,8,7,19])).
% 2.69/2.86 cnf(289,plain,
% 2.69/2.86 (E(a3,f6(f6(a2,a3),a4))),
% 2.69/2.86 inference(scs_inference,[],[211,73,32,269,274,245,271,183,259,248,15,278,18,9,8,7,19,20,2])).
% 2.69/2.86 cnf(290,plain,
% 2.69/2.86 (P1(f6(a4,a3),a2,a3)),
% 2.69/2.86 inference(scs_inference,[],[34,281,9])).
% 2.69/2.86 cnf(291,plain,
% 2.69/2.86 (P1(f6(a4,a3),f5(f6(a1,a3)),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[193,34,280,281,9,8])).
% 2.69/2.86 cnf(292,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a4),f5(a4),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[263,193,34,280,281,9,8,7])).
% 2.69/2.86 cnf(296,plain,
% 2.69/2.86 (P1(f6(a4,a3),a2,f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[289,142,291,284,9,8])).
% 2.69/2.86 cnf(297,plain,
% 2.69/2.86 (P1(f5(f6(a1,a3)),f5(a2),a3)),
% 2.69/2.86 inference(scs_inference,[],[289,142,115,291,284,9,8,7])).
% 2.69/2.86 cnf(298,plain,
% 2.69/2.86 (P1(f6(a3,a3),a1,f6(f6(a4,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[289,142,115,291,284,85,105,9,8,7,19])).
% 2.69/2.86 cnf(301,plain,
% 2.69/2.86 (P1(f5(f6(a3,a3)),f6(a1,a3),f6(a1,a3))),
% 2.69/2.86 inference(scs_inference,[],[289,142,115,291,226,284,79,85,105,9,8,7,19,20])).
% 2.69/2.86 cnf(303,plain,
% 2.69/2.86 (P1(f6(a3,a3),a1,a4)),
% 2.69/2.86 inference(scs_inference,[],[74,298,9])).
% 2.69/2.86 cnf(312,plain,
% 2.69/2.86 (E(f6(a3,a3),f6(f6(a3,a3),f6(a3,a3)))),
% 2.69/2.86 inference(scs_inference,[],[62,13,18])).
% 2.69/2.86 cnf(316,plain,
% 2.69/2.86 (E(a4,f6(f6(a3,a3),a4))),
% 2.69/2.86 inference(scs_inference,[],[21,263,62,13,18,3])).
% 2.69/2.86 cnf(320,plain,
% 2.69/2.86 (P1(f5(a2),f5(a4),a3)),
% 2.69/2.86 inference(scs_inference,[],[197,21,263,62,54,15,13,18,3,9,8])).
% 2.69/2.86 cnf(333,plain,
% 2.69/2.86 (E(f6(a3,a3),f6(f6(a2,a3),a4))),
% 2.69/2.86 inference(scs_inference,[],[32,289,312,2,3])).
% 2.69/2.86 cnf(336,plain,
% 2.69/2.86 (P1(x3361,f6(f6(a3,a3),a3),x3361)),
% 2.69/2.86 inference(rename_variables,[],[43])).
% 2.69/2.86 cnf(339,plain,
% 2.69/2.86 (P1(f6(a2,a3),f6(f6(a3,a3),a3),f5(a4))),
% 2.69/2.86 inference(scs_inference,[],[192,32,289,312,43,336,15,2,3,9,8,7])).
% 2.69/2.86 cnf(352,plain,
% 2.69/2.86 (P1(a2,f6(a3,a3),f5(a4))),
% 2.69/2.86 inference(scs_inference,[],[211,333,28,12,13,2,9,8,7])).
% 2.69/2.86 cnf(353,plain,
% 2.69/2.86 (P1(x3531,f6(a3,a3),x3531)),
% 2.69/2.86 inference(rename_variables,[],[28])).
% 2.69/2.86 cnf(356,plain,
% 2.69/2.86 (P1(x3561,f6(a3,a3),x3561)),
% 2.69/2.86 inference(rename_variables,[],[28])).
% 2.69/2.86 cnf(358,plain,
% 2.69/2.86 (P1(f6(a3,a3),a1,a1)),
% 2.69/2.86 inference(scs_inference,[],[211,333,54,28,353,356,12,62,13,203,2,9,8,7,19,20])).
% 2.69/2.86 cnf(361,plain,
% 2.69/2.86 (P1(f5(f6(a1,a3)),f6(a3,a3),f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[131,28,9])).
% 2.69/2.86 cnf(363,plain,
% 2.69/2.86 (P1(a3,f6(a2,a3),f5(f6(a1,a3)))),
% 2.69/2.86 inference(scs_inference,[],[131,28,13,9,8])).
% 2.69/2.86 cnf(374,plain,
% 2.69/2.86 (E(f6(x3741,a3),f6(x3741,f6(a3,a3)))),
% 2.69/2.86 inference(scs_inference,[],[105,16,18])).
% 2.69/2.86 cnf(377,plain,
% 2.69/2.86 (E(f5(a4),f6(a2,f6(a3,a3)))),
% 2.69/2.86 inference(scs_inference,[],[192,105,16,18,3])).
% 2.69/2.86 cnf(380,plain,
% 2.69/2.86 (P1(a3,f5(a4),f5(f6(a1,a3)))),
% 2.69/2.86 inference(scs_inference,[],[179,192,105,28,13,16,18,3,9,8])).
% 2.69/2.86 cnf(382,plain,
% 2.69/2.86 (P1(f5(a4),f6(a3,a3),f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[179,197,192,105,28,13,16,18,3,9,8,7])).
% 2.69/2.86 cnf(383,plain,
% 2.69/2.86 (P1(x3831,f6(a3,a3),f6(x3831,a3))),
% 2.69/2.86 inference(rename_variables,[],[105])).
% 2.69/2.86 cnf(384,plain,
% 2.69/2.86 (P1(f6(x3841,a3),a1,f6(f6(x3841,a3),a4))),
% 2.69/2.86 inference(scs_inference,[],[179,197,192,105,383,28,13,303,252,16,18,3,9,8,7,19])).
% 2.69/2.86 cnf(387,plain,
% 2.69/2.86 (P1(f5(f6(a2,a3)),f5(a4),a3)),
% 2.69/2.86 inference(scs_inference,[],[179,197,192,105,383,28,43,15,13,339,303,252,16,18,3,9,8,7,19,20])).
% 2.69/2.86 cnf(392,plain,
% 2.69/2.86 (E(f6(x3921,f6(a3,a3)),f6(x3921,a3))),
% 2.69/2.86 inference(scs_inference,[],[374,2])).
% 2.69/2.86 cnf(407,plain,
% 2.69/2.86 (P1(a3,f5(f6(a1,a3)),f5(a4))),
% 2.69/2.86 inference(scs_inference,[],[179,392,377,13,78,2,3,9])).
% 2.69/2.86 cnf(412,plain,
% 2.69/2.86 (P1(f6(a1,a3),f6(a2,a3),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[179,192,392,377,105,12,27,13,78,361,292,2,3,9,8,7,20])).
% 2.69/2.86 cnf(419,plain,
% 2.69/2.86 (P1(a3,f5(f6(a1,a3)),f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[115,197,377,12,13,3,9,8])).
% 2.69/2.86 cnf(420,plain,
% 2.69/2.86 (P1(a3,x4201,x4201)),
% 2.69/2.86 inference(rename_variables,[],[13])).
% 2.69/2.86 cnf(423,plain,
% 2.69/2.86 (P1(f5(f6(a4,a3)),f6(a3,a3),a2)),
% 2.69/2.86 inference(scs_inference,[],[115,197,377,12,24,15,13,420,296,3,9,8,7,20])).
% 2.69/2.86 cnf(430,plain,
% 2.69/2.86 (P1(f6(a3,a3),f6(f6(a1,a3),a3),a1)),
% 2.69/2.86 inference(scs_inference,[],[73,90,12,358,9,8])).
% 2.69/2.86 cnf(431,plain,
% 2.69/2.86 (E(x4311,f6(f6(x4311,a3),a3))),
% 2.69/2.86 inference(rename_variables,[],[90])).
% 2.69/2.86 cnf(432,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),x4321,x4321)),
% 2.69/2.86 inference(scs_inference,[],[73,90,431,12,13,358,9,8,7])).
% 2.69/2.86 cnf(434,plain,
% 2.69/2.86 (P1(f6(a2,a3),a3,f5(a4))),
% 2.69/2.86 inference(scs_inference,[],[73,90,431,12,14,13,358,387,9,8,7,20])).
% 2.69/2.86 cnf(450,plain,
% 2.69/2.86 (E(x4501,f6(x4501,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(451,plain,
% 2.69/2.86 (P1(f6(a2,a3),f6(a3,a3),f5(a4))),
% 2.69/2.86 inference(scs_inference,[],[21,450,15,434,9,8])).
% 2.69/2.86 cnf(453,plain,
% 2.69/2.86 (P1(f5(f6(a1,a3)),f6(a3,a3),a2)),
% 2.69/2.86 inference(scs_inference,[],[115,21,450,41,15,434,9,8,7])).
% 2.69/2.86 cnf(461,plain,
% 2.69/2.86 (P1(f6(a1,a3),a2,f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[32,90,15,412,9,8])).
% 2.69/2.86 cnf(462,plain,
% 2.69/2.86 (E(f6(x4621,a3),x4621)),
% 2.69/2.86 inference(rename_variables,[],[32])).
% 2.69/2.86 cnf(463,plain,
% 2.69/2.86 (P1(f6(a3,a3),x4631,x4631)),
% 2.69/2.86 inference(scs_inference,[],[32,462,90,15,432,412,9,8,7])).
% 2.69/2.86 cnf(469,plain,
% 2.69/2.86 (P1(a3,f6(a2,a3),f5(a4))),
% 2.69/2.86 inference(scs_inference,[],[179,363,9])).
% 2.69/2.86 cnf(470,plain,
% 2.69/2.86 (P1(f6(a1,a3),f5(a4),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[197,179,363,461,9,8])).
% 2.69/2.86 cnf(487,plain,
% 2.69/2.86 (P1(a3,a2,f5(f6(a1,a3)))),
% 2.69/2.86 inference(scs_inference,[],[211,115,382,380,9,8])).
% 2.69/2.86 cnf(488,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),f6(a2,a3),f5(a4))),
% 2.69/2.86 inference(scs_inference,[],[211,115,90,382,380,469,9,8,7])).
% 2.69/2.86 cnf(490,plain,
% 2.69/2.86 (P1(f5(f6(a2,a3)),f5(a4),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[211,115,90,105,15,451,382,380,469,9,8,7,20])).
% 2.69/2.86 cnf(494,plain,
% 2.69/2.86 (P1(f5(f6(a4,a3)),f6(a3,a3),f5(a4))),
% 2.69/2.86 inference(scs_inference,[],[197,423,9])).
% 2.69/2.86 cnf(496,plain,
% 2.69/2.86 (E(x4961,f6(x4961,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(497,plain,
% 2.69/2.86 (P1(f6(a1,a3),f6(f6(a2,a3),a3),a3)),
% 2.69/2.86 inference(scs_inference,[],[197,21,496,121,423,352,9,8,7])).
% 2.69/2.86 cnf(499,plain,
% 2.69/2.86 (P1(f6(a1,a3),a2,f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[197,21,496,28,27,453,121,423,352,9,8,7,20])).
% 2.69/2.86 cnf(513,plain,
% 2.69/2.86 (P1(f5(f6(a4,a3)),f6(a3,a3),f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[192,494,9])).
% 2.69/2.86 cnf(515,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),f5(a2),a1)),
% 2.69/2.86 inference(scs_inference,[],[192,197,90,494,290,238,9,8,7])).
% 2.69/2.86 cnf(517,plain,
% 2.69/2.86 (P1(f6(a4,a3),f5(a4),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[192,197,90,105,27,494,290,238,9,8,7,20])).
% 2.69/2.86 cnf(521,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),f6(a2,a3),a2)),
% 2.69/2.86 inference(scs_inference,[],[211,488,9])).
% 2.69/2.86 cnf(525,plain,
% 2.69/2.86 (P1(f6(a4,a3),f6(a2,a3),a3)),
% 2.69/2.86 inference(scs_inference,[],[211,21,28,14,513,517,499,488,9,8,7,20])).
% 2.69/2.86 cnf(529,plain,
% 2.69/2.86 (P1(f6(a4,a3),f6(a2,a3),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[90,525,9])).
% 2.69/2.86 cnf(532,plain,
% 2.69/2.86 (P1(a1,f5(a4),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[115,32,90,470,525,9,8,7])).
% 2.69/2.86 cnf(534,plain,
% 2.69/2.86 (P1(f6(a1,a3),a3,f5(a2))),
% 2.69/2.86 inference(scs_inference,[],[115,32,90,27,463,470,525,297,9,8,7,20])).
% 2.69/2.86 cnf(538,plain,
% 2.69/2.86 (P1(f6(a1,a3),a3,f6(f5(a2),a3))),
% 2.69/2.86 inference(scs_inference,[],[21,534,9])).
% 2.69/2.86 cnf(539,plain,
% 2.69/2.86 (E(x5391,f6(x5391,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(540,plain,
% 2.69/2.86 (P1(f6(a1,a3),f6(a3,a3),f5(a2))),
% 2.69/2.86 inference(scs_inference,[],[21,539,534,9,8])).
% 2.69/2.86 cnf(549,plain,
% 2.69/2.86 (E(f6(x5491,a3),x5491)),
% 2.69/2.86 inference(rename_variables,[],[32])).
% 2.69/2.86 cnf(550,plain,
% 2.69/2.86 (P1(f6(a3,a3),f6(a1,a3),a1)),
% 2.69/2.86 inference(scs_inference,[],[32,549,529,430,9,8])).
% 2.69/2.86 cnf(558,plain,
% 2.69/2.86 (P1(f6(a3,a3),f6(a1,a3),f6(f6(a1,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[90,550,9])).
% 2.69/2.86 cnf(559,plain,
% 2.69/2.86 (E(x5591,f6(f6(x5591,a3),a3))),
% 2.69/2.86 inference(rename_variables,[],[90])).
% 2.69/2.86 cnf(563,plain,
% 2.69/2.86 (P1(a3,f6(a4,a3),a4)),
% 2.69/2.86 inference(scs_inference,[],[192,90,559,93,550,532,282,463,224,9,8,7,20])).
% 2.69/2.86 cnf(567,plain,
% 2.69/2.86 (P1(f6(a1,a3),f6(a3,a3),f6(f5(a2),a3))),
% 2.69/2.86 inference(scs_inference,[],[21,540,9])).
% 2.69/2.86 cnf(568,plain,
% 2.69/2.86 (E(x5681,f6(x5681,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(570,plain,
% 2.69/2.86 (E(x5701,f6(x5701,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(573,plain,
% 2.69/2.86 (P1(a3,f6(a1,a3),f6(f6(a1,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[21,568,570,93,558,540,301,9,8,7,20])).
% 2.69/2.86 cnf(581,plain,
% 2.69/2.86 (P1(f6(a2,a3),f6(a1,a3),a3)),
% 2.69/2.86 inference(scs_inference,[],[131,32,90,15,573,563,9,8,7])).
% 2.69/2.86 cnf(583,plain,
% 2.69/2.86 (P1(f6(a3,a3),a4,f6(a4,a3))),
% 2.69/2.86 inference(scs_inference,[],[131,32,90,93,15,573,563,432,222,9,8,7,20])).
% 2.69/2.86 cnf(588,plain,
% 2.69/2.86 (E(x5881,f6(x5881,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(589,plain,
% 2.69/2.86 (P1(a3,f5(a4),f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[179,21,583,419,9,8])).
% 2.69/2.86 cnf(592,plain,
% 2.69/2.86 (P1(f6(a3,a3),a4,a1)),
% 2.69/2.86 inference(scs_inference,[],[179,21,588,93,583,419,515,180,9,8,7,20])).
% 2.69/2.86 cnf(595,plain,
% 2.69/2.86 (P1(f6(a3,a3),a4,f6(f6(a1,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[90,592,9])).
% 2.69/2.86 cnf(596,plain,
% 2.69/2.86 (E(x5961,f6(f6(x5961,a3),a3))),
% 2.69/2.86 inference(rename_variables,[],[90])).
% 2.69/2.86 cnf(599,plain,
% 2.69/2.86 (P1(a1,f6(a3,a3),f6(f5(a2),a3))),
% 2.69/2.86 inference(scs_inference,[],[32,90,596,567,592,9,8,7])).
% 2.69/2.86 cnf(601,plain,
% 2.69/2.86 (P1(a3,a4,a1)),
% 2.69/2.86 inference(scs_inference,[],[32,90,596,93,567,592,242,9,8,7,20])).
% 2.69/2.86 cnf(604,plain,
% 2.69/2.86 (P1(a3,a4,f6(a1,a3))),
% 2.69/2.86 inference(scs_inference,[],[21,601,9])).
% 2.69/2.86 cnf(605,plain,
% 2.69/2.86 (E(x6051,f6(x6051,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(606,plain,
% 2.69/2.86 (P1(a3,f6(a4,a3),a1)),
% 2.69/2.86 inference(scs_inference,[],[21,605,601,9,8])).
% 2.69/2.86 cnf(607,plain,
% 2.69/2.86 (E(x6071,f6(x6071,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(610,plain,
% 2.69/2.86 (P1(a2,f6(a1,a3),a3)),
% 2.69/2.86 inference(scs_inference,[],[21,605,607,93,601,581,268,301,9,8,7,20])).
% 2.69/2.86 cnf(613,plain,
% 2.69/2.86 (P1(a2,f6(a1,a3),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[90,610,9])).
% 2.69/2.86 cnf(615,plain,
% 2.69/2.86 (P1(a2,a1,a3)),
% 2.69/2.86 inference(scs_inference,[],[32,90,610,9,8])).
% 2.69/2.86 cnf(616,plain,
% 2.69/2.86 (E(f6(x6161,a3),x6161)),
% 2.69/2.86 inference(rename_variables,[],[32])).
% 2.69/2.86 cnf(619,plain,
% 2.69/2.86 (P1(f5(a3),f6(f6(a3,a3),f6(a3,a3)),a3)),
% 2.69/2.86 inference(scs_inference,[],[32,616,90,54,28,15,538,610,9,8,7,19])).
% 2.69/2.86 cnf(625,plain,
% 2.69/2.86 (E(x6251,f6(x6251,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(626,plain,
% 2.69/2.86 (P1(f6(a3,a3),f6(a4,a3),f6(f6(a1,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[21,625,619,595,9,8])).
% 2.69/2.86 cnf(628,plain,
% 2.69/2.86 (P1(f5(a4),f6(a1,a3),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[197,21,625,619,595,613,9,8,7])).
% 2.69/2.86 cnf(629,plain,
% 2.69/2.86 (P1(f6(a3,a3),f6(a4,a3),f6(a1,a3))),
% 2.69/2.86 inference(scs_inference,[],[32,626,9])).
% 2.69/2.86 cnf(630,plain,
% 2.69/2.86 (E(f6(x6301,a3),x6301)),
% 2.69/2.86 inference(rename_variables,[],[32])).
% 2.69/2.86 cnf(631,plain,
% 2.69/2.86 (P1(f5(a4),a1,f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[32,630,626,628,9,8])).
% 2.69/2.86 cnf(638,plain,
% 2.69/2.86 (P1(f5(a2),f5(a4),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[90,320,9])).
% 2.69/2.86 cnf(639,plain,
% 2.69/2.86 (E(x6391,f6(f6(x6391,a3),a3))),
% 2.69/2.86 inference(rename_variables,[],[90])).
% 2.69/2.86 cnf(640,plain,
% 2.69/2.86 (P1(f5(a2),f6(a2,a3),a3)),
% 2.69/2.86 inference(scs_inference,[],[192,90,320,9,8])).
% 2.69/2.86 cnf(641,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),f5(a4),f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[192,90,639,589,320,9,8,7])).
% 2.69/2.86 cnf(643,plain,
% 2.69/2.86 (P1(a3,f6(a4,a3),f6(a1,a3))),
% 2.69/2.86 inference(scs_inference,[],[192,90,639,93,629,589,320,220,9,8,7,20])).
% 2.69/2.86 cnf(647,plain,
% 2.69/2.86 (E(x6471,f6(x6471,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(649,plain,
% 2.69/2.86 (P1(f6(f5(a2),a3),f6(a2,a3),a3)),
% 2.69/2.86 inference(scs_inference,[],[211,21,647,490,497,640,9,8,7])).
% 2.69/2.86 cnf(651,plain,
% 2.69/2.86 (P1(a1,f6(a3,a3),f5(a2))),
% 2.69/2.86 inference(scs_inference,[],[32,599,9])).
% 2.69/2.86 cnf(654,plain,
% 2.69/2.86 (E(x6541,f6(f6(x6541,a3),a3))),
% 2.69/2.86 inference(rename_variables,[],[90])).
% 2.69/2.86 cnf(655,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),f6(a4,a3),f6(a1,a3))),
% 2.69/2.86 inference(scs_inference,[],[32,90,654,643,604,599,9,8,7])).
% 2.69/2.86 cnf(657,plain,
% 2.69/2.86 (P1(f6(f5(a2),a3),f6(a2,a3),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[21,649,9])).
% 2.69/2.86 cnf(658,plain,
% 2.69/2.86 (E(x6581,f6(x6581,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(660,plain,
% 2.69/2.86 (E(x6601,f6(x6601,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(661,plain,
% 2.69/2.86 (P1(f6(a3,a3),f6(a4,a3),a1)),
% 2.69/2.86 inference(scs_inference,[],[21,658,660,649,606,9,8,7])).
% 2.69/2.86 cnf(663,plain,
% 2.69/2.86 (P1(f6(a3,a3),a4,f6(a1,a3))),
% 2.69/2.86 inference(scs_inference,[],[21,658,660,93,655,649,606,222,9,8,7,20])).
% 2.69/2.86 cnf(666,plain,
% 2.69/2.86 (P1(f5(a2),f5(a4),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[32,638,9])).
% 2.69/2.86 cnf(667,plain,
% 2.69/2.86 (E(f6(x6671,a3),x6671)),
% 2.69/2.86 inference(rename_variables,[],[32])).
% 2.69/2.86 cnf(670,plain,
% 2.69/2.86 (P1(f5(a2),f6(a2,a3),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[32,667,90,657,663,638,9,8,7])).
% 2.69/2.86 cnf(673,plain,
% 2.69/2.86 (E(x6731,f6(x6731,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(674,plain,
% 2.69/2.86 (P1(f5(a2),f5(f6(a1,a3)),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[115,21,670,9,8])).
% 2.69/2.86 cnf(675,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),f6(a4,a3),a1)),
% 2.69/2.86 inference(scs_inference,[],[115,21,673,670,661,9,8,7])).
% 2.69/2.86 cnf(678,plain,
% 2.69/2.86 (E(f6(x6781,a3),x6781)),
% 2.69/2.86 inference(rename_variables,[],[32])).
% 2.69/2.86 cnf(679,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),a4,a1)),
% 2.69/2.86 inference(scs_inference,[],[32,678,675,674,9,8])).
% 2.69/2.86 cnf(683,plain,
% 2.69/2.86 (P1(a3,a2,f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[131,487,9])).
% 2.69/2.86 cnf(686,plain,
% 2.69/2.86 (P1(f6(a2,a3),a1,f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[131,192,90,631,487,615,9,8,7])).
% 2.69/2.86 cnf(688,plain,
% 2.69/2.86 (P1(a3,f5(f6(a1,a3)),a2)),
% 2.69/2.86 inference(scs_inference,[],[211,407,9])).
% 2.69/2.86 cnf(689,plain,
% 2.69/2.86 (P1(f6(a2,a3),f6(a1,a3),f6(f6(a3,a3),a3))),
% 2.69/2.86 inference(scs_inference,[],[211,21,686,407,9,8])).
% 2.69/2.86 cnf(690,plain,
% 2.69/2.86 (E(x6901,f6(x6901,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.86 cnf(691,plain,
% 2.69/2.86 (P1(f6(f5(a2),a3),f5(a4),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[211,21,690,686,666,407,9,8,7])).
% 2.69/2.86 cnf(693,plain,
% 2.69/2.86 (P1(f6(a2,a3),f6(a1,a3),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[32,689,9])).
% 2.69/2.86 cnf(694,plain,
% 2.69/2.86 (E(f6(x6941,a3),x6941)),
% 2.69/2.86 inference(rename_variables,[],[32])).
% 2.69/2.86 cnf(696,plain,
% 2.69/2.86 (E(f6(x6961,a3),x6961)),
% 2.69/2.86 inference(rename_variables,[],[32])).
% 2.69/2.86 cnf(697,plain,
% 2.69/2.86 (P1(f6(a3,a3),f5(a4),f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[32,694,696,689,641,651,9,8,7])).
% 2.69/2.86 cnf(699,plain,
% 2.69/2.86 (P1(f6(a3,a3),f5(a4),f5(f6(a1,a3)))),
% 2.69/2.86 inference(scs_inference,[],[115,697,9])).
% 2.69/2.86 cnf(701,plain,
% 2.69/2.86 (P1(f6(f6(a3,a3),a3),a2,f6(a2,a3))),
% 2.69/2.86 inference(scs_inference,[],[131,115,90,697,683,688,9,8,7])).
% 2.69/2.86 cnf(703,plain,
% 2.69/2.86 (P1(a2,f6(a1,a3),f6(a3,a3))),
% 2.69/2.86 inference(scs_inference,[],[131,115,90,93,693,697,683,688,301,9,8,7,20])).
% 2.69/2.86 cnf(707,plain,
% 2.69/2.86 (E(x7071,f6(x7071,a3))),
% 2.69/2.86 inference(rename_variables,[],[21])).
% 2.69/2.87 cnf(708,plain,
% 2.69/2.87 (P1(a2,f6(f6(a1,a3),a3),f6(a3,a3))),
% 2.69/2.87 inference(scs_inference,[],[21,707,703,679,9,8])).
% 2.69/2.87 cnf(710,plain,
% 2.69/2.87 (P1(f5(a4),f6(a1,a3),f6(a3,a3))),
% 2.69/2.87 inference(scs_inference,[],[197,21,707,703,679,9,8,7])).
% 2.69/2.87 cnf(712,plain,
% 2.69/2.87 (E(f6(x7121,a3),x7121)),
% 2.69/2.87 inference(rename_variables,[],[32])).
% 2.69/2.87 cnf(714,plain,
% 2.69/2.87 (E(f6(x7141,a3),x7141)),
% 2.69/2.87 inference(rename_variables,[],[32])).
% 2.69/2.87 cnf(715,plain,
% 2.69/2.87 (P1(f6(a3,a3),f6(a2,a3),a2)),
% 2.69/2.87 inference(scs_inference,[],[32,712,714,691,710,521,9,8,7])).
% 2.69/2.87 cnf(718,plain,
% 2.69/2.87 (P1(f6(a3,a3),f5(f6(a1,a3)),a2)),
% 2.69/2.87 inference(scs_inference,[],[197,115,715,9,8])).
% 2.69/2.87 cnf(719,plain,
% 2.69/2.87 (P1(f5(a4),f6(f6(a1,a3),a3),f6(a3,a3))),
% 2.69/2.87 inference(scs_inference,[],[197,115,715,708,9,8,7])).
% 2.69/2.87 cnf(720,plain,
% 2.69/2.87 (P1(f6(a3,a3),f5(f6(a1,a3)),f5(a4))),
% 2.69/2.87 inference(scs_inference,[],[197,718,9])).
% 2.69/2.87 cnf(722,plain,
% 2.69/2.87 (P1(f6(a2,a3),f6(f6(a1,a3),a3),f6(a3,a3))),
% 2.69/2.87 inference(scs_inference,[],[192,197,719,699,718,9,8,7])).
% 2.69/2.87 cnf(728,plain,
% 2.69/2.87 (P1(f6(x7281,a3),f6(a1,a3),f6(f6(x7281,a3),a4))),
% 2.69/2.87 inference(scs_inference,[],[192,21,720,384,9,8])).
% 2.69/2.87 cnf(733,plain,
% 2.69/2.87 (E(f6(x7331,a3),x7331)),
% 2.69/2.87 inference(rename_variables,[],[32])).
% 2.69/2.87 cnf(735,plain,
% 2.69/2.87 (E(f6(x7351,a3),x7351)),
% 2.69/2.87 inference(rename_variables,[],[32])).
% 2.69/2.87 cnf(745,plain,
% 2.69/2.87 ($false),
% 2.69/2.87 inference(scs_inference,[],[32,733,735,316,93,13,722,728,701,33,558,301,9,8,7,20,18,2,3]),
% 2.69/2.87 ['proof']).
% 2.69/2.87 % SZS output end Proof
% 2.69/2.87 % Total time :2.310000s
%------------------------------------------------------------------------------