%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GRP029-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 : n020.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:32 EDT 2024
% Result : Unsatisfiable 9.72s 9.80s
% Output : CNFRefutation 9.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : GRP029-1 : TPTP v8.2.0. Released v1.0.0.
% 0.12/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n020.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 13:21:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 9.72/9.80 %-------------------------------------------
% 9.72/9.80 % File :CSE---1.7
% 9.72/9.80 % Problem :theBenchmark
% 9.72/9.80 % Transform :cnf
% 9.72/9.80 % Format :tptp:raw
% 9.72/9.80 % Command :java -jar mcs_scs.jar %d %s
% 9.72/9.80
% 9.72/9.80 % Result :Theorem 9.200000s
% 9.72/9.80 % Output :CNFRefutation 9.200000s
% 9.72/9.80 %-------------------------------------------
% 9.72/9.80 %--------------------------------------------------------------------------
% 9.72/9.80 % File : GRP029-1 : TPTP v8.2.0. Released v1.0.0.
% 9.72/9.80 % Domain : Group Theory (Semigroups)
% 9.72/9.80 % Problem : In semigroups, left id and inverse => right id exists
% 9.72/9.80 % Version : [MOW76] axioms :
% 9.72/9.80 % Incomplete > Augmented > Complete.
% 9.72/9.80 % English : If there are a left identity and left inverse, then there
% 9.72/9.80 % is a right identity element.
% 9.72/9.80
% 9.72/9.80 % Refs : [Wos65] Wos (1965), Unpublished Note
% 9.72/9.80 % : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 9.72/9.80 % : [WM76] Wilson & Minker (1976), Resolution, Refinements, and S
% 9.72/9.80 % Source : [SPRFN]
% 9.72/9.80 % Names : Problem 1 [Wos65]
% 9.72/9.80 % : wos1 [WM76]
% 9.72/9.80 % : G5 [MOW76]
% 9.72/9.80 % : ident2.ver1.in [ANL]
% 9.72/9.80
% 9.72/9.80 % Status : Unsatisfiable
% 9.72/9.80 % Rating : 0.06 v8.2.0, 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.29 v5.0.0, 0.14 v4.1.0, 0.11 v4.0.1, 0.17 v3.7.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.00 v2.0.0
% 9.72/9.80 % Syntax : Number of clauses : 7 ( 4 unt; 0 nHn; 4 RR)
% 9.72/9.80 % Number of literals : 15 ( 1 equ; 9 neg)
% 9.72/9.80 % Maximal clause size : 4 ( 2 avg)
% 9.72/9.80 % Maximal term depth : 2 ( 1 avg)
% 9.72/9.80 % Number of predicates : 2 ( 1 usr; 0 prp; 2-3 aty)
% 9.72/9.80 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% 9.72/9.80 % Number of variables : 21 ( 0 sgn)
% 9.72/9.80 % SPC : CNF_UNS_RFO_SEQ_HRN
% 9.72/9.80
% 9.72/9.80 % Comments : This may also be viewed as a group theory problem, to prove
% 9.72/9.80 % that the right identity axiom is dependant on the rest of the
% 9.72/9.80 % axiom set; i.e., each element has a right identity. Note that
% 9.72/9.80 % this is a corollary to proving that the right identity axiom
% 9.72/9.80 % is dependant on the rest of the axiom set, but also that the
% 9.72/9.80 % proof is different due to the introduction of a skolem
% 9.72/9.80 % function for the right identity of each element of the group.
% 9.72/9.80 % : The inverse_substitution substitution axioms are missing
% 9.72/9.80 % in the [MOW76] presentation.
% 9.72/9.80 %--------------------------------------------------------------------------
% 9.72/9.80 %----Include semi-group axioms
% 9.72/9.80 include('Axioms/GRP002-0.ax').
% 9.72/9.80 %--------------------------------------------------------------------------
% 9.72/9.80 cnf(left_identity,axiom,
% 9.72/9.80 product(identity,A,A) ).
% 9.72/9.80
% 9.72/9.80 cnf(left_inverse,axiom,
% 9.72/9.80 product(inverse(A),A,identity) ).
% 9.72/9.80
% 9.72/9.80 cnf(prove_there_is_a_right_identity,negated_conjecture,
% 9.72/9.80 ~ product(not_right_identity(A),A,not_right_identity(A)) ).
% 9.72/9.80
% 9.72/9.80 %--------------------------------------------------------------------------
% 9.72/9.80 %-------------------------------------------
% 9.72/9.80 % Proof found
% 9.72/9.80 % SZS status Theorem for theBenchmark
% 9.72/9.80 % SZS output start Proof
% 9.72/9.81 %ClaNum:17(EqnAxiom:10)
% 9.72/9.81 %VarNum:43(SingletonVarNum:21)
% 9.72/9.81 %MaxLitNum:4
% 9.72/9.81 %MaxfuncDepth:1
% 9.72/9.81 %SharedTerms:1
% 9.72/9.81 %goalClause: 14
% 9.72/9.81 %singleGoalClaCount:1
% 9.72/9.81 [11]P1(a1,x111,x111)
% 9.72/9.81 [12]P1(f2(x121),x121,a1)
% 9.72/9.81 [14]~P1(f4(x141),x141,f4(x141))
% 9.72/9.81 [13]P1(x131,x132,f3(x131,x132))
% 9.72/9.81 [15]~P1(x153,x154,x151)+E(x151,x152)+~P1(x153,x154,x152)
% 9.72/9.81 [16]~P1(x166,x164,x161)+P1(x161,x162,x163)+~P1(x164,x162,x165)+~P1(x166,x165,x163)
% 9.72/9.81 [17]~P1(x171,x176,x174)+P1(x171,x172,x173)+~P1(x174,x175,x173)+~P1(x176,x175,x172)
% 9.72/9.81 %EqnAxiom
% 9.72/9.81 [1]E(x11,x11)
% 9.72/9.81 [2]E(x22,x21)+~E(x21,x22)
% 9.72/9.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 9.72/9.81 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 9.72/9.81 [5]~E(x51,x52)+E(f3(x51,x53),f3(x52,x53))
% 9.72/9.81 [6]~E(x61,x62)+E(f3(x63,x61),f3(x63,x62))
% 9.72/9.81 [7]~E(x71,x72)+E(f4(x71),f4(x72))
% 9.72/9.81 [8]P1(x82,x83,x84)+~E(x81,x82)+~P1(x81,x83,x84)
% 9.72/9.81 [9]P1(x93,x92,x94)+~E(x91,x92)+~P1(x93,x91,x94)
% 9.72/9.81 [10]P1(x103,x104,x102)+~E(x101,x102)+~P1(x103,x104,x101)
% 9.72/9.81
% 9.72/9.81 %-------------------------------------------
% 9.72/9.81 cnf(18,plain,
% 9.72/9.81 (E(x181,f3(a1,x181))),
% 9.72/9.81 inference(scs_inference,[],[11,13,15])).
% 9.72/9.81 cnf(19,plain,
% 9.72/9.81 (P1(x191,x192,f3(x191,x192))),
% 9.72/9.81 inference(rename_variables,[],[13])).
% 9.72/9.81 cnf(21,plain,
% 9.72/9.81 (P1(a1,f3(a1,x211),x211)),
% 9.72/9.81 inference(scs_inference,[],[11,13,15,9])).
% 9.72/9.81 cnf(22,plain,
% 9.72/9.81 (~E(f3(f4(x221),x221),f4(x221))),
% 9.72/9.81 inference(scs_inference,[],[14,11,13,19,15,9,10])).
% 9.72/9.81 cnf(23,plain,
% 9.72/9.81 (P1(x231,x232,f3(x231,x232))),
% 9.72/9.81 inference(rename_variables,[],[13])).
% 9.72/9.81 cnf(24,plain,
% 9.72/9.81 (P1(f3(f2(x241),a1),x241,a1)),
% 9.72/9.81 inference(scs_inference,[],[14,11,13,19,23,12,15,9,10,16])).
% 9.72/9.81 cnf(25,plain,
% 9.72/9.81 (P1(f2(x251),x251,a1)),
% 9.72/9.81 inference(rename_variables,[],[12])).
% 9.72/9.81 cnf(26,plain,
% 9.72/9.81 (P1(x261,x262,f3(x261,x262))),
% 9.72/9.81 inference(rename_variables,[],[13])).
% 9.72/9.81 cnf(28,plain,
% 9.72/9.82 (P1(a1,a1,f3(f2(x281),x281))),
% 9.72/9.82 inference(scs_inference,[],[14,11,13,19,23,26,12,25,15,9,10,16,17])).
% 9.72/9.82 cnf(30,plain,
% 9.72/9.82 (P1(a1,x301,x301)),
% 9.72/9.82 inference(rename_variables,[],[11])).
% 9.72/9.82 cnf(34,plain,
% 9.72/9.82 (P1(x341,x342,x342)+~E(a1,x341)),
% 9.72/9.82 inference(scs_inference,[],[14,11,30,13,19,23,26,12,25,15,9,10,16,17,2,8])).
% 9.72/9.82 cnf(36,plain,
% 9.72/9.82 (P1(f3(a1,a1),x361,x361)),
% 9.72/9.82 inference(scs_inference,[],[18,34])).
% 9.72/9.82 cnf(37,plain,
% 9.72/9.82 (E(x371,f3(a1,x371))),
% 9.72/9.82 inference(rename_variables,[],[18])).
% 9.72/9.82 cnf(38,plain,
% 9.72/9.82 (E(f3(a1,x381),x381)),
% 9.72/9.82 inference(scs_inference,[],[18,37,34,2])).
% 9.72/9.82 cnf(39,plain,
% 9.72/9.82 (E(f3(f2(x391),x391),a1)),
% 9.72/9.82 inference(scs_inference,[],[18,37,13,12,34,2,15])).
% 9.72/9.82 cnf(41,plain,
% 9.72/9.82 (P1(x411,x412,f3(x411,x412))),
% 9.72/9.82 inference(rename_variables,[],[13])).
% 9.72/9.82 cnf(43,plain,
% 9.72/9.82 (P1(f3(a1,a1),a1,f3(f2(x431),x431))),
% 9.72/9.82 inference(scs_inference,[],[28,18,37,13,12,34,2,15,8])).
% 9.72/9.82 cnf(44,plain,
% 9.72/9.82 (E(x441,f3(a1,x441))),
% 9.72/9.82 inference(rename_variables,[],[18])).
% 9.72/9.82 cnf(46,plain,
% 9.72/9.82 (P1(f3(f2(x461),a1),x461,a1)),
% 9.72/9.82 inference(rename_variables,[],[24])).
% 9.72/9.82 cnf(47,plain,
% 9.72/9.82 (P1(f3(f2(x471),a1),x471,f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[24,46,28,18,37,44,13,12,34,2,15,8,9,10])).
% 9.72/9.82 cnf(49,plain,
% 9.72/9.82 (P1(f3(f2(x491),x491),x492,x492)),
% 9.72/9.82 inference(scs_inference,[],[24,46,28,18,37,44,21,13,41,12,34,2,15,8,9,10,16])).
% 9.72/9.82 cnf(53,plain,
% 9.72/9.82 (P1(a1,f3(f2(a1),a1),a1)),
% 9.72/9.82 inference(scs_inference,[],[24,46,28,18,37,44,21,13,41,12,34,2,15,8,9,10,16,17])).
% 9.72/9.82 cnf(59,plain,
% 9.72/9.82 (E(a1,f3(f2(x591),x591))),
% 9.72/9.82 inference(scs_inference,[],[39,2])).
% 9.72/9.82 cnf(60,plain,
% 9.72/9.82 (E(f3(a1,a1),f3(f2(x601),x601))),
% 9.72/9.82 inference(scs_inference,[],[38,39,2,3])).
% 9.72/9.82 cnf(61,plain,
% 9.72/9.82 (E(f3(a1,x611),x611)),
% 9.72/9.82 inference(rename_variables,[],[38])).
% 9.72/9.82 cnf(62,plain,
% 9.72/9.82 (P1(f3(a1,a1),f3(f2(a1),a1),a1)),
% 9.72/9.82 inference(scs_inference,[],[53,38,39,18,2,3,8])).
% 9.72/9.82 cnf(64,plain,
% 9.72/9.82 (P1(f3(f2(x641),x641),f3(a1,x642),x642)),
% 9.72/9.82 inference(scs_inference,[],[49,53,38,61,39,18,2,3,8,10])).
% 9.72/9.82 cnf(65,plain,
% 9.72/9.82 (P1(f3(f2(x651),x651),x652,x652)),
% 9.72/9.82 inference(rename_variables,[],[49])).
% 9.72/9.82 cnf(67,plain,
% 9.72/9.82 (P1(f3(f2(x671),x671),x672,x672)),
% 9.72/9.82 inference(rename_variables,[],[49])).
% 9.72/9.82 cnf(68,plain,
% 9.72/9.82 (P1(a1,f3(f2(x681),x681),a1)),
% 9.72/9.82 inference(scs_inference,[],[49,65,67,53,28,38,61,39,18,2,3,8,10,9,17])).
% 9.72/9.82 cnf(70,plain,
% 9.72/9.82 (P1(f3(f2(x701),x701),x702,x702)),
% 9.72/9.82 inference(rename_variables,[],[49])).
% 9.72/9.82 cnf(72,plain,
% 9.72/9.82 (P1(f3(a1,a1),a1,f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[49,65,67,70,36,53,28,47,38,61,39,18,2,3,8,10,9,17,16])).
% 9.72/9.82 cnf(77,plain,
% 9.72/9.82 (E(f3(f2(x771),x771),f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[60,2])).
% 9.72/9.82 cnf(78,plain,
% 9.72/9.82 (E(f3(a1,a1),f3(f3(a1,a1),a1))),
% 9.72/9.82 inference(scs_inference,[],[72,60,13,2,15])).
% 9.72/9.82 cnf(81,plain,
% 9.72/9.82 (P1(f3(a1,a1),f3(a1,a1),f3(f2(x811),x811))),
% 9.72/9.82 inference(scs_inference,[],[72,36,60,13,2,15,10])).
% 9.72/9.82 cnf(83,plain,
% 9.72/9.82 (P1(f3(a1,f2(x831)),x831,a1)),
% 9.72/9.82 inference(scs_inference,[],[72,36,60,18,13,12,2,15,10,8])).
% 9.72/9.82 cnf(86,plain,
% 9.72/9.82 (P1(f3(a1,a1),f3(f2(x861),x861),a1)),
% 9.72/9.82 inference(scs_inference,[],[72,62,68,49,36,60,59,18,13,12,2,15,10,8,9,17])).
% 9.72/9.82 cnf(87,plain,
% 9.72/9.82 (P1(f3(f2(x871),x871),x872,x872)),
% 9.72/9.82 inference(rename_variables,[],[49])).
% 9.72/9.82 cnf(89,plain,
% 9.72/9.82 (~P1(f4(x891),x891,f3(a1,f4(x891)))),
% 9.72/9.82 inference(scs_inference,[],[14,72,62,68,49,87,36,60,64,59,18,13,12,2,15,10,8,9,17,16])).
% 9.72/9.82 cnf(93,plain,
% 9.72/9.82 (E(f3(f3(a1,a1),a1),f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[78,2])).
% 9.72/9.82 cnf(94,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),a1),x941,x941)),
% 9.72/9.82 inference(scs_inference,[],[36,78,2,8])).
% 9.72/9.82 cnf(95,plain,
% 9.72/9.82 (P1(f2(x951),x951,f3(f2(x952),x952))),
% 9.72/9.82 inference(scs_inference,[],[36,78,59,12,2,8,10])).
% 9.72/9.82 cnf(98,plain,
% 9.72/9.82 (P1(f3(a1,a1),x981,f3(a1,x981))),
% 9.72/9.82 inference(scs_inference,[],[86,43,49,36,77,78,21,59,12,2,8,10,9,17])).
% 9.72/9.82 cnf(109,plain,
% 9.72/9.82 (P1(f3(a1,a1),x1091,x1091)),
% 9.72/9.82 inference(rename_variables,[],[36])).
% 9.72/9.82 cnf(111,plain,
% 9.72/9.82 (P1(f3(a1,a1),x1111,x1111)),
% 9.72/9.82 inference(rename_variables,[],[36])).
% 9.72/9.82 cnf(112,plain,
% 9.72/9.82 (P1(a1,f3(f3(a1,a1),a1),a1)),
% 9.72/9.82 inference(scs_inference,[],[94,83,36,109,81,93,38,8,9,10,16])).
% 9.72/9.82 cnf(115,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),a1),x1151,x1151)),
% 9.72/9.82 inference(rename_variables,[],[94])).
% 9.72/9.82 cnf(117,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),a1),x1171,f3(a1,x1171))),
% 9.72/9.82 inference(scs_inference,[],[94,115,98,83,36,109,111,81,93,38,8,9,10,16,17])).
% 9.72/9.82 cnf(121,plain,
% 9.72/9.82 (P1(f3(a1,a1),f3(a1,x1211),x1211)),
% 9.72/9.82 inference(scs_inference,[],[77,64,8])).
% 9.72/9.82 cnf(123,plain,
% 9.72/9.82 (P1(f2(x1231),x1231,f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[95,77,64,8,10])).
% 9.72/9.82 cnf(125,plain,
% 9.72/9.82 (P1(a1,f3(f3(a1,a1),a1),f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[112,24,95,77,64,47,8,10,16])).
% 9.72/9.82 cnf(132,plain,
% 9.72/9.82 (E(f3(a1,f3(a1,x1321)),x1321)),
% 9.72/9.82 inference(scs_inference,[],[117,112,98,24,83,95,77,64,47,8,10,16,17,15])).
% 9.72/9.82 cnf(135,plain,
% 9.72/9.82 (E(x1351,f3(a1,f3(a1,x1351)))),
% 9.72/9.82 inference(scs_inference,[],[117,112,98,24,83,95,77,64,47,8,10,16,17,15,2])).
% 9.72/9.82 cnf(136,plain,
% 9.72/9.82 (P1(f3(a1,f3(a1,a1)),x1361,x1361)),
% 9.72/9.82 inference(scs_inference,[],[135,34])).
% 9.72/9.82 cnf(137,plain,
% 9.72/9.82 (E(x1371,f3(a1,f3(a1,x1371)))),
% 9.72/9.82 inference(rename_variables,[],[135])).
% 9.72/9.82 cnf(138,plain,
% 9.72/9.82 (E(x1381,f3(f3(a1,a1),f3(a1,x1381)))),
% 9.72/9.82 inference(scs_inference,[],[121,135,13,34,15])).
% 9.72/9.82 cnf(141,plain,
% 9.72/9.82 (P1(f3(a1,a1),x1411,f3(a1,f3(a1,x1411)))),
% 9.72/9.82 inference(scs_inference,[],[121,36,132,135,13,34,15,9])).
% 9.72/9.82 cnf(143,plain,
% 9.72/9.82 (P1(f3(a1,f3(a1,a1)),f3(a1,x1431),x1431)),
% 9.72/9.82 inference(scs_inference,[],[121,36,132,135,137,21,13,34,15,9,8])).
% 9.72/9.82 cnf(145,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),a1),f3(a1,x1451),x1451)),
% 9.72/9.82 inference(scs_inference,[],[121,117,36,132,135,137,21,13,34,15,9,8,10])).
% 9.72/9.82 cnf(146,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),a1),x1461,f3(a1,x1461))),
% 9.72/9.82 inference(rename_variables,[],[117])).
% 9.72/9.82 cnf(147,plain,
% 9.72/9.82 (P1(a1,f3(a1,f3(a1,x1471)),x1471)),
% 9.72/9.82 inference(scs_inference,[],[121,125,117,146,36,132,135,137,21,13,34,15,9,8,10,17])).
% 9.72/9.82 cnf(150,plain,
% 9.72/9.82 (~P1(f3(a1,f4(x1501)),x1501,f4(x1501))),
% 9.72/9.82 inference(scs_inference,[],[121,89,125,117,146,98,36,132,135,137,21,13,34,15,9,8,10,17,16])).
% 9.72/9.82 cnf(154,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),f3(a1,a1)),x1541,x1541)),
% 9.72/9.82 inference(scs_inference,[],[138,34])).
% 9.72/9.82 cnf(155,plain,
% 9.72/9.82 (E(x1551,f3(f3(a1,a1),f3(a1,x1551)))),
% 9.72/9.82 inference(rename_variables,[],[138])).
% 9.72/9.82 cnf(156,plain,
% 9.72/9.82 (E(f3(f3(a1,a1),f3(a1,x1561)),x1561)),
% 9.72/9.82 inference(scs_inference,[],[138,155,34,2])).
% 9.72/9.82 cnf(159,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),f3(a1,a1)),f3(a1,x1591),x1591)),
% 9.72/9.82 inference(scs_inference,[],[98,138,155,21,34,2,9,8])).
% 9.72/9.82 cnf(160,plain,
% 9.72/9.82 (E(x1601,f3(f3(a1,a1),f3(a1,x1601)))),
% 9.72/9.82 inference(rename_variables,[],[138])).
% 9.72/9.82 cnf(167,plain,
% 9.72/9.82 (P1(a1,x1671,f3(a1,f3(a1,x1671)))),
% 9.72/9.82 inference(scs_inference,[],[136,94,86,49,98,36,138,155,160,145,141,21,34,2,9,8,10,17,16])).
% 9.72/9.82 cnf(171,plain,
% 9.72/9.82 (E(f3(f3(a1,a1),f3(a1,x1711)),f3(a1,x1711))),
% 9.72/9.82 inference(scs_inference,[],[156,18,3])).
% 9.72/9.82 cnf(178,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),f3(a1,a1)),x1781,x1781)),
% 9.72/9.82 inference(rename_variables,[],[154])).
% 9.72/9.82 cnf(186,plain,
% 9.72/9.82 (E(f3(a1,x1861),f3(f3(a1,a1),f3(a1,x1861)))),
% 9.72/9.82 inference(scs_inference,[],[154,178,94,24,36,156,145,18,11,3,9,10,17,16,2])).
% 9.72/9.82 cnf(189,plain,
% 9.72/9.82 (P1(f2(x1891),x1891,f3(f3(a1,a1),f3(a1,a1)))),
% 9.72/9.82 inference(scs_inference,[],[123,186,21,9,10])).
% 9.72/9.82 cnf(195,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),f3(a1,x1951)),x1952,f3(x1951,x1952))),
% 9.72/9.82 inference(scs_inference,[],[138,13,8])).
% 9.72/9.82 cnf(197,plain,
% 9.72/9.82 (P1(f2(x1971),f3(f3(a1,a1),f3(a1,x1971)),f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[123,138,13,8,9])).
% 9.72/9.82 cnf(199,plain,
% 9.72/9.82 (P1(f3(a1,f3(a1,x1991)),x1992,f3(x1991,x1992))),
% 9.72/9.82 inference(scs_inference,[],[135,13,8])).
% 9.72/9.82 cnf(205,plain,
% 9.72/9.82 (P1(f3(a1,x2051),x2052,f3(x2051,x2052))),
% 9.72/9.82 inference(scs_inference,[],[195,171,8])).
% 9.72/9.82 cnf(218,plain,
% 9.72/9.82 (P1(x2181,x2182,f3(f3(a1,x2181),x2182))),
% 9.72/9.82 inference(scs_inference,[],[38,13,8])).
% 9.72/9.82 cnf(221,plain,
% 9.72/9.82 (E(f3(a1,x2211),x2211)),
% 9.72/9.82 inference(rename_variables,[],[38])).
% 9.72/9.82 cnf(222,plain,
% 9.72/9.82 (P1(f3(a1,x2221),x2222,f3(x2221,f3(a1,x2222)))),
% 9.72/9.82 inference(scs_inference,[],[205,197,38,221,13,8,10,9])).
% 9.72/9.82 cnf(224,plain,
% 9.72/9.82 (E(x2241,f3(f3(a1,a1),x2241))),
% 9.72/9.82 inference(scs_inference,[],[11,205,197,38,221,13,8,10,9,15])).
% 9.72/9.82 cnf(226,plain,
% 9.72/9.82 (E(f3(a1,x2261),f3(f3(a1,a1),x2261))),
% 9.72/9.82 inference(scs_inference,[],[11,205,197,38,221,13,8,10,9,15,3])).
% 9.72/9.82 cnf(227,plain,
% 9.72/9.82 (E(f3(f3(a1,a1),x2271),x2271)),
% 9.72/9.82 inference(scs_inference,[],[11,205,197,38,221,13,8,10,9,15,3,2])).
% 9.72/9.82 cnf(229,plain,
% 9.72/9.82 (E(f3(f3(a1,a1),x2291),f3(a1,x2291))),
% 9.72/9.82 inference(scs_inference,[],[226,2])).
% 9.72/9.82 cnf(230,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),f2(x2301)),x2301,f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[224,226,123,2,8])).
% 9.72/9.82 cnf(241,plain,
% 9.72/9.82 (E(x2411,f3(f3(a1,a1),x2411))),
% 9.72/9.82 inference(rename_variables,[],[224])).
% 9.72/9.82 cnf(242,plain,
% 9.72/9.82 (~E(f3(f4(x2421),f3(a1,x2421)),f4(x2421))),
% 9.72/9.82 inference(scs_inference,[],[150,222,224,12,8,10])).
% 9.72/9.82 cnf(244,plain,
% 9.72/9.82 (P1(f3(a1,x2441),f3(f3(a1,a1),x2442),f3(x2441,x2442))),
% 9.72/9.82 inference(scs_inference,[],[150,205,222,224,241,12,8,10,9])).
% 9.72/9.82 cnf(247,plain,
% 9.72/9.82 (P1(f3(a1,f2(x2471)),x2471,f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[230,229,8])).
% 9.72/9.82 cnf(254,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),x2541),x2542,f3(x2541,x2542))),
% 9.72/9.82 inference(scs_inference,[],[224,13,8])).
% 9.72/9.82 cnf(259,plain,
% 9.72/9.82 (E(f3(f3(a1,x2591),x2592),f3(x2591,x2592))),
% 9.72/9.82 inference(scs_inference,[],[254,195,15])).
% 9.72/9.82 cnf(260,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),f3(a1,x2601)),x2602,f3(x2601,x2602))),
% 9.72/9.82 inference(rename_variables,[],[195])).
% 9.72/9.82 cnf(261,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),x2611),x2612,f3(x2611,x2612))),
% 9.72/9.82 inference(rename_variables,[],[254])).
% 9.72/9.82 cnf(263,plain,
% 9.72/9.82 (P1(f3(a1,x2631),f3(a1,x2632),f3(x2631,x2632))),
% 9.72/9.82 inference(scs_inference,[],[254,195,244,229,15,9])).
% 9.72/9.82 cnf(265,plain,
% 9.72/9.82 (P1(a1,f3(x2651,x2652),f3(f3(a1,x2651),x2652))),
% 9.72/9.82 inference(scs_inference,[],[11,254,261,195,260,244,229,15,9,17])).
% 9.72/9.82 cnf(267,plain,
% 9.72/9.82 (P1(a1,x2671,x2671)),
% 9.72/9.82 inference(rename_variables,[],[11])).
% 9.72/9.82 cnf(268,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),x2681),x2682,f3(x2681,x2682))),
% 9.72/9.82 inference(rename_variables,[],[254])).
% 9.72/9.82 cnf(270,plain,
% 9.72/9.82 (P1(f3(x2701,a1),a1,f3(x2701,a1))),
% 9.72/9.82 inference(scs_inference,[],[11,267,254,261,268,195,260,244,229,15,9,17,16])).
% 9.72/9.82 cnf(275,plain,
% 9.72/9.82 (E(f3(x2751,x2752),f3(f3(a1,x2751),x2752))),
% 9.72/9.82 inference(scs_inference,[],[11,267,254,261,268,195,260,244,229,15,9,17,16,2])).
% 9.72/9.82 cnf(276,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),x2761),f3(a1,x2762),f3(x2761,x2762))),
% 9.72/9.82 inference(scs_inference,[],[11,267,254,261,268,195,260,244,229,226,15,9,17,16,2,8])).
% 9.72/9.82 cnf(294,plain,
% 9.72/9.82 (P1(x2941,f3(a1,x2942),f3(x2941,x2942))),
% 9.72/9.82 inference(scs_inference,[],[276,227,8])).
% 9.72/9.82 cnf(296,plain,
% 9.72/9.82 (P1(f3(x2961,a1),f3(a1,f3(a1,a1)),f3(x2961,a1))),
% 9.72/9.82 inference(scs_inference,[],[276,270,227,135,8,9])).
% 9.72/9.82 cnf(302,plain,
% 9.72/9.82 (P1(a1,f3(x3021,x3022),f3(x3021,f3(a1,x3022)))),
% 9.72/9.82 inference(scs_inference,[],[11,218,276,270,227,259,135,8,9,17,10])).
% 9.72/9.82 cnf(306,plain,
% 9.72/9.82 (P1(f3(f3(a1,a1),x3061),f3(a1,x3062),f3(x3061,x3062))),
% 9.72/9.82 inference(rename_variables,[],[276])).
% 9.72/9.82 cnf(309,plain,
% 9.72/9.82 (P1(x3091,f3(f2(x3092),x3092),f3(x3091,a1))),
% 9.72/9.82 inference(scs_inference,[],[294,276,306,39,60,156,8,10,9])).
% 9.72/9.82 cnf(310,plain,
% 9.72/9.82 (P1(x3101,f3(a1,x3102),f3(x3101,x3102))),
% 9.72/9.82 inference(rename_variables,[],[294])).
% 9.72/9.82 cnf(311,plain,
% 9.72/9.82 (P1(f3(f2(x3111),f3(a1,a1)),f3(a1,x3111),f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[143,294,310,276,306,39,60,156,123,8,10,9,16])).
% 9.72/9.82 cnf(316,plain,
% 9.72/9.82 (E(f3(a1,a1),f3(f2(x3161),f3(a1,x3161)))),
% 9.72/9.82 inference(scs_inference,[],[247,222,15])).
% 9.72/9.82 cnf(317,plain,
% 9.72/9.82 (P1(f3(a1,x3171),x3172,f3(x3171,f3(a1,x3172)))),
% 9.72/9.82 inference(rename_variables,[],[222])).
% 9.72/9.82 cnf(322,plain,
% 9.72/9.82 (P1(a1,f3(f2(x3221),f3(a1,x3221)),f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[11,247,294,222,317,275,15,9,17])).
% 9.72/9.82 cnf(324,plain,
% 9.72/9.82 (P1(a1,x3241,x3241)),
% 9.72/9.82 inference(rename_variables,[],[11])).
% 9.72/9.82 cnf(326,plain,
% 9.72/9.82 (P1(f3(a1,a1),x3261,f3(f2(a1),x3261))),
% 9.72/9.82 inference(scs_inference,[],[11,324,247,294,205,222,317,275,15,9,17,16])).
% 9.72/9.82 cnf(330,plain,
% 9.72/9.82 (E(f3(f2(a1),f3(a1,a1)),f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[11,324,247,294,205,222,317,275,15,9,17,16,2])).
% 9.72/9.82 cnf(332,plain,
% 9.72/9.82 (E(f3(f2(x3321),f3(a1,x3321)),f3(a1,a1))),
% 9.72/9.82 inference(scs_inference,[],[316,2])).
% 9.72/9.82 cnf(333,plain,
% 9.72/9.82 (E(f3(f2(a1),x3331),f3(a1,x3331))),
% 9.72/9.82 inference(scs_inference,[],[326,205,316,2,15])).
% 9.72/9.82 cnf(334,plain,
% 9.72/9.83 (P1(f3(a1,x3341),x3342,f3(x3341,x3342))),
% 9.72/9.83 inference(rename_variables,[],[205])).
% 9.72/9.83 cnf(336,plain,
% 9.72/9.83 (P1(f3(f2(x3361),f3(a1,x3361)),x3362,f3(a1,x3362))),
% 9.72/9.83 inference(scs_inference,[],[326,205,334,316,2,15,8])).
% 9.72/9.83 cnf(342,plain,
% 9.72/9.83 (P1(f3(x3421,a1),f3(a1,a1),f3(x3421,a1))),
% 9.72/9.83 inference(scs_inference,[],[11,326,199,254,205,334,330,316,296,2,15,8,10,9,16])).
% 9.72/9.83 cnf(350,plain,
% 9.72/9.83 (E(f3(a1,x3501),f3(f2(a1),x3501))),
% 9.72/9.83 inference(scs_inference,[],[333,2])).
% 9.72/9.83 cnf(357,plain,
% 9.72/9.83 (E(f3(a1,x3571),f3(f2(a1),x3571))),
% 9.72/9.83 inference(rename_variables,[],[350])).
% 9.72/9.83 cnf(358,plain,
% 9.72/9.83 (P1(a1,x3581,f3(f2(a1),f3(a1,x3581)))),
% 9.72/9.83 inference(scs_inference,[],[167,136,350,357,8,10])).
% 9.72/9.83 cnf(363,plain,
% 9.72/9.83 (E(x3631,f3(f2(a1),f3(a1,x3631)))),
% 9.72/9.83 inference(scs_inference,[],[11,358,15])).
% 9.72/9.83 cnf(366,plain,
% 9.72/9.83 (P1(f3(f2(a1),f3(a1,x3661)),x3662,f3(x3661,x3662))),
% 9.72/9.83 inference(scs_inference,[],[11,199,358,350,15,8])).
% 9.72/9.83 cnf(367,plain,
% 9.72/9.83 (E(f3(a1,x3671),f3(f2(a1),x3671))),
% 9.72/9.83 inference(rename_variables,[],[350])).
% 9.72/9.83 cnf(368,plain,
% 9.72/9.83 (P1(f3(f3(a1,a1),f2(a1)),x3681,f3(a1,x3681))),
% 9.72/9.83 inference(scs_inference,[],[11,199,254,358,333,350,15,8,10])).
% 9.72/9.83 cnf(372,plain,
% 9.72/9.83 (E(f3(f2(a1),f3(a1,x3721)),x3721)),
% 9.72/9.83 inference(scs_inference,[],[11,147,199,254,358,333,350,367,15,8,10,9,2])).
% 9.72/9.83 cnf(374,plain,
% 9.72/9.83 (P1(f3(f2(a1),f3(a1,x3741)),f3(a1,x3742),f3(x3741,x3742))),
% 9.72/9.83 inference(scs_inference,[],[294,363,8])).
% 9.72/9.83 cnf(381,plain,
% 9.72/9.83 (E(f3(f2(a1),f3(a1,x3811)),f3(a1,x3811))),
% 9.72/9.83 inference(scs_inference,[],[372,18,3])).
% 9.72/9.83 cnf(383,plain,
% 9.72/9.83 (P1(f3(f3(a1,a1),f2(a1)),f3(a1,x3831),x3831)),
% 9.72/9.83 inference(scs_inference,[],[254,372,18,3,10])).
% 9.72/9.83 cnf(385,plain,
% 9.72/9.83 (E(f3(a1,x3851),f3(f2(a1),f3(a1,x3851)))),
% 9.72/9.83 inference(scs_inference,[],[254,372,18,3,10,2])).
% 9.72/9.83 cnf(394,plain,
% 9.72/9.83 (P1(x3941,f3(f2(a1),f3(a1,x3942)),f3(x3941,x3942))),
% 9.72/9.83 inference(scs_inference,[],[294,254,381,385,10,9])).
% 9.72/9.83 cnf(402,plain,
% 9.72/9.83 (P1(f3(a1,f3(a1,x4021)),f3(a1,x4022),f3(x4021,x4022))),
% 9.72/9.83 inference(scs_inference,[],[374,333,8])).
% 9.72/9.83 cnf(403,plain,
% 9.72/9.83 (E(f3(f2(a1),x4031),f3(a1,x4031))),
% 9.72/9.83 inference(rename_variables,[],[333])).
% 9.72/9.83 cnf(406,plain,
% 9.72/9.83 (P1(x4061,f3(f2(a1),x4062),f3(x4061,x4062))),
% 9.72/9.83 inference(scs_inference,[],[374,294,36,333,403,350,8,10,9])).
% 9.72/9.83 cnf(412,plain,
% 9.72/9.83 (P1(f3(f3(a1,a1),f3(a1,x4121)),f3(a1,x4122),f3(x4121,x4122))),
% 9.72/9.83 inference(scs_inference,[],[263,224,8])).
% 9.72/9.83 cnf(413,plain,
% 9.72/9.83 (E(x4131,f3(f3(a1,a1),x4131))),
% 9.72/9.83 inference(rename_variables,[],[224])).
% 9.72/9.83 cnf(414,plain,
% 9.72/9.83 (P1(x4141,f3(f3(a1,a1),f3(a1,x4142)),f3(x4141,x4142))),
% 9.72/9.83 inference(scs_inference,[],[294,263,224,413,8,9])).
% 9.72/9.83 cnf(417,plain,
% 9.72/9.83 (P1(f2(a1),f3(a1,x4171),x4171)),
% 9.72/9.83 inference(scs_inference,[],[383,227,8])).
% 9.72/9.83 cnf(423,plain,
% 9.72/9.83 (P1(f3(a1,f2(a1)),x4231,f3(a1,x4231))),
% 9.72/9.83 inference(scs_inference,[],[368,259,8])).
% 9.72/9.83 cnf(428,plain,
% 9.72/9.83 (P1(f3(f3(a1,x4281),a1),f3(a1,a1),f3(x4281,a1))),
% 9.72/9.83 inference(scs_inference,[],[342,275,8])).
% 9.72/9.83 cnf(429,plain,
% 9.72/9.83 (P1(f3(x4291,a1),f3(a1,a1),f3(x4291,a1))),
% 9.72/9.83 inference(rename_variables,[],[342])).
% 9.72/9.83 cnf(430,plain,
% 9.72/9.83 (E(f3(x4301,x4302),f3(f3(a1,x4301),x4302))),
% 9.72/9.83 inference(rename_variables,[],[275])).
% 9.72/9.83 cnf(435,plain,
% 9.72/9.83 (P1(f3(a1,a1),f2(a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[311,423,342,429,254,332,275,430,8,10,9,16])).
% 9.72/9.83 cnf(440,plain,
% 9.72/9.83 (E(f3(a1,a1),f3(f2(a1),f2(a1)))),
% 9.72/9.83 inference(scs_inference,[],[435,326,15])).
% 9.72/9.83 cnf(441,plain,
% 9.72/9.83 (P1(f3(a1,a1),x4411,f3(f2(a1),x4411))),
% 9.72/9.83 inference(rename_variables,[],[326])).
% 9.72/9.83 cnf(443,plain,
% 9.72/9.83 (P1(f3(f2(x4431),f3(a1,x4431)),f2(a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[435,326,316,15,8])).
% 9.72/9.83 cnf(446,plain,
% 9.72/9.83 (P1(f2(a1),f3(a1,x4461),x4461)),
% 9.72/9.83 inference(rename_variables,[],[417])).
% 9.72/9.83 cnf(447,plain,
% 9.72/9.83 (P1(a1,f3(f2(a1),f2(a1)),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[11,435,417,326,441,316,15,8,10,9,17])).
% 9.72/9.83 cnf(451,plain,
% 9.72/9.83 (P1(f3(a1,a1),f3(a1,f2(a1)),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[11,435,417,446,326,441,316,15,8,10,9,17,16])).
% 9.72/9.83 cnf(456,plain,
% 9.72/9.83 (E(f3(a1,a1),f3(a1,f2(a1)))),
% 9.72/9.83 inference(scs_inference,[],[440,333,3])).
% 9.72/9.83 cnf(458,plain,
% 9.72/9.83 (E(f3(a1,a1),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[451,121,440,333,3,15])).
% 9.72/9.83 cnf(459,plain,
% 9.72/9.83 (P1(f3(a1,a1),f3(a1,x4591),x4591)),
% 9.72/9.83 inference(rename_variables,[],[121])).
% 9.72/9.83 cnf(461,plain,
% 9.72/9.83 (P1(f3(f2(a1),f2(a1)),f3(a1,a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[451,342,121,440,333,3,15,8])).
% 9.72/9.83 cnf(462,plain,
% 9.72/9.83 (P1(f3(x4621,a1),f3(a1,a1),f3(x4621,a1))),
% 9.72/9.83 inference(rename_variables,[],[342])).
% 9.72/9.83 cnf(464,plain,
% 9.72/9.83 (P1(a1,x4641,x4641)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(466,plain,
% 9.72/9.83 (P1(a1,f2(a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[11,464,451,342,462,121,459,440,333,3,15,8,10,9,17])).
% 9.72/9.83 cnf(470,plain,
% 9.72/9.83 (P1(f3(x4701,a1),f3(a1,f2(a1)),f3(x4701,a1))),
% 9.72/9.83 inference(scs_inference,[],[11,464,451,412,342,462,121,459,440,333,3,15,8,10,9,17,16])).
% 9.72/9.83 cnf(473,plain,
% 9.72/9.83 (E(f3(a1,f2(a1)),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[11,464,451,412,342,462,121,459,440,333,3,15,8,10,9,17,16,2])).
% 9.72/9.83 cnf(475,plain,
% 9.72/9.83 (E(f2(a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[458,2])).
% 9.72/9.83 cnf(476,plain,
% 9.72/9.83 (E(f3(a1,a1),f3(f3(a1,a1),f2(a1)))),
% 9.72/9.83 inference(scs_inference,[],[456,458,275,2,3])).
% 9.72/9.83 cnf(478,plain,
% 9.72/9.83 (P1(f3(a1,f2(a1)),f3(a1,a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[342,456,458,275,2,3,8])).
% 9.72/9.83 cnf(481,plain,
% 9.72/9.83 (P1(a1,x4811,x4811)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(484,plain,
% 9.72/9.83 (P1(f3(x4841,a1),f2(a1),f3(x4841,a1))),
% 9.72/9.83 inference(scs_inference,[],[11,481,470,423,342,456,458,275,2,3,8,10,9,16])).
% 9.72/9.83 cnf(488,plain,
% 9.72/9.83 (E(f3(f3(a1,a1),f2(a1)),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[476,2])).
% 9.72/9.83 cnf(489,plain,
% 9.72/9.83 (E(f2(a1),f3(f2(a1),f2(a1)))),
% 9.72/9.83 inference(scs_inference,[],[475,476,440,2,3])).
% 9.72/9.83 cnf(491,plain,
% 9.72/9.83 (P1(f3(x4911,a1),f2(a1),f3(x4911,a1))),
% 9.72/9.83 inference(rename_variables,[],[484])).
% 9.72/9.83 cnf(496,plain,
% 9.72/9.83 (P1(a1,f2(a1),a1)),
% 9.72/9.83 inference(scs_inference,[],[11,484,491,154,86,475,476,440,2,3,8,10,9,16])).
% 9.72/9.83 cnf(501,plain,
% 9.72/9.83 (E(f3(f2(a1),f2(a1)),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[489,2])).
% 9.72/9.83 cnf(512,plain,
% 9.72/9.83 (P1(f2(a1),f3(a1,a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[461,501,8])).
% 9.72/9.83 cnf(513,plain,
% 9.72/9.83 (P1(f3(a1,f2(a1)),f3(a1,a1),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[478,461,501,458,8,10])).
% 9.72/9.83 cnf(516,plain,
% 9.72/9.83 (P1(f3(f3(a1,a1),a1),f2(a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[466,224,8])).
% 9.72/9.83 cnf(527,plain,
% 9.72/9.83 (E(f3(x5271,x5272),f3(x5271,f3(a1,x5272)))),
% 9.72/9.83 inference(scs_inference,[],[402,199,15])).
% 9.72/9.83 cnf(528,plain,
% 9.72/9.83 (P1(f3(a1,f3(a1,x5281)),x5282,f3(x5281,x5282))),
% 9.72/9.83 inference(rename_variables,[],[199])).
% 9.72/9.83 cnf(530,plain,
% 9.72/9.83 (P1(f3(f3(a1,a1),f3(a1,a1)),f2(a1),a1)),
% 9.72/9.83 inference(scs_inference,[],[402,496,199,138,15,8])).
% 9.72/9.83 cnf(539,plain,
% 9.72/9.83 (P1(f3(a1,a1),f3(a1,f2(a1)),a1)),
% 9.72/9.83 inference(scs_inference,[],[11,159,512,402,470,496,199,528,417,473,476,138,15,8,10,9,17,16])).
% 9.72/9.83 cnf(543,plain,
% 9.72/9.83 (E(f3(x5431,f3(a1,x5432)),f3(x5431,x5432))),
% 9.72/9.83 inference(scs_inference,[],[11,159,512,402,470,496,199,528,417,473,476,138,15,8,10,9,17,16,2])).
% 9.72/9.83 cnf(545,plain,
% 9.72/9.83 (E(a1,f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[530,154,15])).
% 9.72/9.83 cnf(548,plain,
% 9.72/9.83 (E(f3(a1,f3(a1,a1)),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[530,154,543,458,15,3])).
% 9.72/9.83 cnf(550,plain,
% 9.72/9.83 (P1(f3(f3(a1,x5501),f3(a1,a1)),f3(a1,a1),f3(x5501,a1))),
% 9.72/9.83 inference(scs_inference,[],[428,530,154,527,543,458,15,3,8])).
% 9.72/9.83 cnf(551,plain,
% 9.72/9.83 (E(f3(x5511,x5512),f3(x5511,f3(a1,x5512)))),
% 9.72/9.83 inference(rename_variables,[],[527])).
% 9.72/9.83 cnf(558,plain,
% 9.72/9.83 (P1(f2(a1),x5581,x5581)),
% 9.72/9.83 inference(scs_inference,[],[428,443,530,466,484,154,527,551,513,543,475,458,15,3,8,10,9,16,34])).
% 9.72/9.83 cnf(559,plain,
% 9.72/9.83 (E(f2(a1),a1)),
% 9.72/9.83 inference(scs_inference,[],[428,443,530,466,484,154,527,551,513,543,475,458,15,3,8,10,9,16,34,2])).
% 9.72/9.83 cnf(561,plain,
% 9.72/9.83 (E(f2(a1),f3(a1,f3(a1,a1)))),
% 9.72/9.83 inference(scs_inference,[],[548,2])).
% 9.72/9.83 cnf(562,plain,
% 9.72/9.83 (E(a1,f3(a1,f2(a1)))),
% 9.72/9.83 inference(scs_inference,[],[539,36,548,2,15])).
% 9.72/9.83 cnf(565,plain,
% 9.72/9.83 (E(a1,f3(f2(a1),f2(a1)))),
% 9.72/9.83 inference(scs_inference,[],[539,36,545,548,489,2,15,3])).
% 9.72/9.83 cnf(570,plain,
% 9.72/9.83 (P1(a1,x5701,x5701)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(571,plain,
% 9.72/9.83 (P1(f2(a1),a1,f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[11,570,447,558,539,36,559,545,548,489,2,15,3,8,10,9,17])).
% 9.72/9.83 cnf(574,plain,
% 9.72/9.83 (P1(f3(f2(a1),f2(a1)),x5741,x5741)),
% 9.72/9.83 inference(scs_inference,[],[11,570,447,558,539,36,559,545,548,489,2,15,3,8,10,9,17,34])).
% 9.72/9.83 cnf(579,plain,
% 9.72/9.83 (E(f3(a1,f2(a1)),a1)),
% 9.72/9.83 inference(scs_inference,[],[562,34,2])).
% 9.72/9.83 cnf(580,plain,
% 9.72/9.83 (E(f2(a1),f3(f3(a1,a1),f3(a1,a1)))),
% 9.72/9.83 inference(scs_inference,[],[571,189,562,34,2,15])).
% 9.72/9.83 cnf(581,plain,
% 9.72/9.83 (P1(f2(x5811),x5811,f3(f3(a1,a1),f3(a1,a1)))),
% 9.72/9.83 inference(rename_variables,[],[189])).
% 9.72/9.83 cnf(583,plain,
% 9.72/9.83 (E(f3(f2(a1),f2(a1)),a1)),
% 9.72/9.83 inference(scs_inference,[],[571,189,562,501,559,34,2,15,3])).
% 9.72/9.83 cnf(584,plain,
% 9.72/9.83 (P1(f3(f2(a1),x5841),x5842,f3(x5841,x5842))),
% 9.72/9.83 inference(scs_inference,[],[366,571,189,562,501,543,559,34,2,15,3,8])).
% 9.72/9.83 cnf(586,plain,
% 9.72/9.83 (E(f3(x5861,f3(a1,x5862)),f3(x5861,x5862))),
% 9.72/9.83 inference(rename_variables,[],[543])).
% 9.72/9.83 cnf(590,plain,
% 9.72/9.83 (P1(a1,f3(a1,f3(a1,a1)),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[11,366,571,336,189,561,562,501,543,586,559,34,2,15,3,8,10,9])).
% 9.72/9.83 cnf(591,plain,
% 9.72/9.83 (P1(a1,x5911,x5911)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(596,plain,
% 9.72/9.83 (P1(f3(a1,a1),a1,f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[11,591,366,571,336,516,94,189,581,561,562,501,543,586,559,34,2,15,3,8,10,9,17,16])).
% 9.72/9.83 cnf(600,plain,
% 9.72/9.83 (E(f3(f3(a1,a1),f3(a1,a1)),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[580,2])).
% 9.72/9.83 cnf(601,plain,
% 9.72/9.83 (E(x6011,f3(f2(a1),x6011))),
% 9.72/9.83 inference(scs_inference,[],[574,584,580,2,15])).
% 9.72/9.83 cnf(602,plain,
% 9.72/9.83 (P1(f3(f2(a1),x6021),x6022,f3(x6021,x6022))),
% 9.72/9.83 inference(rename_variables,[],[584])).
% 9.72/9.83 cnf(604,plain,
% 9.72/9.83 (E(f2(a1),f3(f2(a1),f3(a1,a1)))),
% 9.72/9.83 inference(scs_inference,[],[574,584,561,580,350,2,15,3])).
% 9.72/9.83 cnf(607,plain,
% 9.72/9.83 (P1(f3(f2(a1),x6071),x6072,f3(x6071,x6072))),
% 9.72/9.83 inference(rename_variables,[],[584])).
% 9.72/9.83 cnf(609,plain,
% 9.72/9.83 (P1(f3(f2(a1),x6091),x6092,f3(x6091,x6092))),
% 9.72/9.83 inference(rename_variables,[],[584])).
% 9.72/9.83 cnf(611,plain,
% 9.72/9.83 (P1(a1,x6111,x6111)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(612,plain,
% 9.72/9.83 (P1(a1,f3(f2(a1),x6121),x6121)),
% 9.72/9.83 inference(scs_inference,[],[11,611,574,584,602,607,609,579,583,561,580,350,2,15,3,8,10,9,17])).
% 9.72/9.83 cnf(619,plain,
% 9.72/9.83 (E(f3(f2(a1),f3(a1,a1)),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[604,2])).
% 9.72/9.83 cnf(620,plain,
% 9.72/9.83 (E(f3(f2(a1),x6201),x6201)),
% 9.72/9.83 inference(scs_inference,[],[11,612,604,2,15])).
% 9.72/9.83 cnf(621,plain,
% 9.72/9.83 (P1(a1,x6211,x6211)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(623,plain,
% 9.72/9.83 (E(f3(f3(a1,a1),a1),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[11,612,600,604,527,2,15,3])).
% 9.72/9.83 cnf(630,plain,
% 9.72/9.83 (P1(a1,x6301,x6301)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(635,plain,
% 9.72/9.83 (P1(f3(a1,a1),a1,f3(a1,f2(a1)))),
% 9.72/9.83 inference(scs_inference,[],[11,621,630,550,596,612,584,195,326,600,604,601,527,2,15,3,8,10,9,17,16])).
% 9.72/9.83 cnf(641,plain,
% 9.72/9.83 (E(f3(f2(a1),a1),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[623,620,545,2,3])).
% 9.72/9.83 cnf(646,plain,
% 9.72/9.83 (P1(a1,x6461,x6461)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(648,plain,
% 9.72/9.83 (P1(a1,x6481,x6481)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(649,plain,
% 9.72/9.83 (P1(f3(a1,f2(a1)),f3(a1,x6491),x6491)),
% 9.72/9.83 inference(scs_inference,[],[11,646,648,635,366,121,619,623,620,545,2,3,8,10,9,16])).
% 9.72/9.83 cnf(654,plain,
% 9.72/9.83 (P1(f2(a1),f2(a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[516,623,641,2,8])).
% 9.72/9.83 cnf(672,plain,
% 9.72/9.83 (P1(f3(f3(a1,a1),a1),f2(a1),a1)),
% 9.72/9.83 inference(scs_inference,[],[530,543,8])).
% 9.72/9.83 cnf(682,plain,
% 9.72/9.83 (P1(f3(f2(a1),f2(a1)),f2(a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[466,565,8])).
% 9.72/9.83 cnf(687,plain,
% 9.72/9.83 (P1(f2(a1),f3(a1,f3(a1,a1)),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[11,654,466,136,590,583,565,527,8,10,9,16])).
% 9.72/9.83 cnf(691,plain,
% 9.72/9.83 (E(a1,f3(f3(a1,a1),f2(a1)))),
% 9.72/9.83 inference(scs_inference,[],[562,275,3])).
% 9.72/9.83 cnf(704,plain,
% 9.72/9.83 (P1(f3(f3(a1,a1),f2(a1)),x7041,x7041)),
% 9.72/9.83 inference(scs_inference,[],[649,687,682,672,558,574,484,562,579,623,275,3,8,10,9,17,16,34])).
% 9.72/9.83 cnf(705,plain,
% 9.72/9.83 (E(f3(f3(a1,a1),f2(a1)),a1)),
% 9.72/9.83 inference(scs_inference,[],[649,687,682,672,558,574,484,562,579,623,275,3,8,10,9,17,16,34,2])).
% 9.72/9.83 cnf(707,plain,
% 9.72/9.83 (P1(f3(f3(a1,a1),f2(a1)),f2(a1),a1)),
% 9.72/9.83 inference(scs_inference,[],[496,691,8])).
% 9.72/9.83 cnf(814,plain,
% 9.72/9.83 (E(f3(f2(x8141),f3(a1,x8141)),a1)),
% 9.72/9.83 inference(scs_inference,[],[543,39,3])).
% 9.72/9.83 cnf(821,plain,
% 9.72/9.83 (P1(f3(f2(x8211),f3(a1,x8211)),x8212,x8212)),
% 9.72/9.83 inference(scs_inference,[],[814,2,34])).
% 9.72/9.83 cnf(823,plain,
% 9.72/9.83 (E(f3(f2(x8231),f3(a1,x8231)),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[814,545,2,3])).
% 9.72/9.83 cnf(829,plain,
% 9.72/9.83 (E(f2(a1),f3(f2(x8291),f3(a1,x8291)))),
% 9.72/9.83 inference(scs_inference,[],[823,2])).
% 9.72/9.83 cnf(840,plain,
% 9.72/9.83 (P1(a1,x8401,x8401)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(846,plain,
% 9.72/9.83 (E(f3(f2(x8461),x8461),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[11,840,821,829,543,3,10,9,16,2])).
% 9.72/9.83 cnf(875,plain,
% 9.72/9.83 (P1(f3(f2(a1),f2(x8751)),f3(a1,x8751),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[584,263,823,473,8,10])).
% 9.72/9.83 cnf(882,plain,
% 9.72/9.83 (P1(f2(x8821),f3(a1,x8821),f2(a1))),
% 9.72/9.83 inference(scs_inference,[],[875,620,8])).
% 9.72/9.83 cnf(893,plain,
% 9.72/9.83 (P1(f2(x8931),f3(a1,x8931),f3(f2(x8932),f3(a1,x8932)))),
% 9.72/9.83 inference(scs_inference,[],[882,829,10])).
% 9.72/9.83 cnf(903,plain,
% 9.72/9.83 (P1(x9031,f3(f2(a1),f2(a1)),f3(x9031,a1))),
% 9.72/9.83 inference(scs_inference,[],[882,294,893,475,440,8,10,9])).
% 9.72/9.83 cnf(908,plain,
% 9.72/9.83 (P1(f2(x9081),f3(a1,x9081),a1)),
% 9.72/9.83 inference(scs_inference,[],[882,222,559,548,8,10])).
% 9.72/9.83 cnf(911,plain,
% 9.72/9.83 (~P1(a1,f3(f4(x9111),f3(a1,x9111)),f4(x9111))),
% 9.72/9.83 inference(scs_inference,[],[242,11,2,15])).
% 9.72/9.83 cnf(913,plain,
% 9.72/9.83 (P1(a1,x9131,x9131)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(916,plain,
% 9.72/9.83 (~E(f4(x9161),f3(f4(x9161),f3(a1,x9161)))),
% 9.72/9.83 inference(scs_inference,[],[11,913,882,911,22,561,15,10,9])).
% 9.72/9.83 cnf(917,plain,
% 9.72/9.83 (P1(a1,x9171,x9171)),
% 9.72/9.83 inference(rename_variables,[],[11])).
% 9.72/9.83 cnf(925,plain,
% 9.72/9.83 (~E(f4(x9251),f3(f4(x9251),x9251))),
% 9.72/9.83 inference(scs_inference,[],[11,913,917,707,704,882,584,911,22,561,527,15,10,9,17,16,3])).
% 9.72/9.83 cnf(959,plain,
% 9.72/9.83 (P1(x9591,f2(a1),f3(x9591,a1))),
% 9.72/9.83 inference(scs_inference,[],[205,36,414,916,705,600,15,10,9])).
% 9.72/9.83 cnf(997,plain,
% 9.72/9.83 (~P1(a1,f3(f4(x9971),x9971),f4(x9971))),
% 9.72/9.83 inference(scs_inference,[],[11,36,302,908,406,916,583,691,911,15,10,9,17])).
% 9.72/9.83 cnf(1047,plain,
% 9.72/9.83 (P1(x10471,x10472,f3(x10471,f3(a1,x10472)))),
% 9.72/9.83 inference(scs_inference,[],[309,222,925,38,15,8])).
% 9.72/9.83 cnf(1063,plain,
% 9.72/9.83 (P1(f3(a1,f3(a1,x10631)),f2(a1),f3(x10631,a1))),
% 9.72/9.83 inference(scs_inference,[],[903,959,925,135,15,8])).
% 9.72/9.83 cnf(1089,plain,
% 9.72/9.83 (P1(f3(a1,x10891),f2(a1),f3(x10891,a1))),
% 9.72/9.83 inference(scs_inference,[],[1063,543,8])).
% 9.72/9.83 cnf(1119,plain,
% 9.72/9.83 (P1(f3(x11191,f3(a1,a1)),f3(a1,a1),f3(x11191,a1))),
% 9.72/9.83 inference(scs_inference,[],[550,259,8])).
% 9.72/9.83 cnf(1141,plain,
% 9.72/9.83 (P1(f2(x11411),f3(x11411,x11412),f3(a1,f3(a1,x11412)))),
% 9.72/9.83 inference(scs_inference,[],[12,1047,13,17])).
% 9.72/9.83 cnf(1156,plain,
% 9.72/9.83 (E(f3(x11561,x11562),f3(f3(a1,x11561),f3(a1,x11562)))),
% 9.72/9.83 inference(scs_inference,[],[527,275,3])).
% 9.72/9.83 cnf(1159,plain,
% 9.72/9.83 (E(x11591,f3(f2(a1),x11591))),
% 9.72/9.83 inference(rename_variables,[],[601])).
% 9.72/9.83 cnf(1162,plain,
% 9.72/9.83 (P1(f2(x11621),f3(x11621,x11622),f3(f3(a1,a1),x11622))),
% 9.72/9.83 inference(scs_inference,[],[12,265,1089,294,527,601,1159,275,3,8,9,17])).
% 9.72/9.83 cnf(1166,plain,
% 9.72/9.83 (E(f3(f3(a1,x11661),f3(a1,x11662)),f3(x11661,x11662))),
% 9.72/9.83 inference(scs_inference,[],[12,265,1089,294,527,601,1159,275,3,8,9,17,2])).
% 9.72/9.83 cnf(1172,plain,
% 9.72/9.83 (E(f3(f3(a1,x11721),f3(a1,x11722)),f3(x11721,x11722))),
% 9.72/9.83 inference(rename_variables,[],[1166])).
% 9.72/9.83 cnf(1179,plain,
% 9.72/9.83 (P1(f2(x11791),f3(x11791,a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[12,1162,1119,322,417,394,1166,1172,1156,8,10,9,17])).
% 9.72/9.83 cnf(1184,plain,
% 9.72/9.83 (P1(f3(a1,f2(x11841)),f3(x11841,a1),f3(a1,a1))),
% 9.72/9.83 inference(scs_inference,[],[1179,18,8])).
% 9.72/9.83 cnf(1237,plain,
% 9.72/9.83 (P1(f2(x12371),f3(x12371,x12372),x12372)),
% 9.72/9.83 inference(scs_inference,[],[1141,1184,132,350,8,10])).
% 9.72/9.83 cnf(1249,plain,
% 9.72/9.83 (P1(f2(x12491),f3(x12491,x12492),x12492)),
% 9.72/9.83 inference(rename_variables,[],[1237])).
% 9.72/9.83 cnf(1250,plain,
% 9.72/9.83 ($false),
% 9.72/9.83 inference(scs_inference,[],[12,1162,997,1237,1249,846,488,10,9,16]),
% 9.72/9.83 ['proof']).
% 9.72/9.83 % SZS output end Proof
% 9.72/9.83 % Total time :9.200000s
%------------------------------------------------------------------------------