%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : RNG001-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 : n028.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 14:00:32 EDT 2024
% Result : Unsatisfiable 58.59s 58.68s
% Output : CNFRefutation 58.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : RNG001-1 : TPTP v8.2.0. Released v1.0.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n028.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Tue Jun 18 14:18:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.43/0.59 start to proof:theBenchmark
% 58.59/58.67 %-------------------------------------------
% 58.59/58.67 % File :CSE---1.7
% 58.59/58.67 % Problem :theBenchmark
% 58.59/58.67 % Transform :cnf
% 58.59/58.67 % Format :tptp:raw
% 58.59/58.67 % Command :java -jar mcs_scs.jar %d %s
% 58.59/58.67
% 58.59/58.67 % Result :Theorem 58.040000s
% 58.59/58.67 % Output :CNFRefutation 58.040000s
% 58.59/58.67 %-------------------------------------------
% 58.59/58.68 %--------------------------------------------------------------------------
% 58.59/58.68 % File : RNG001-1 : TPTP v8.2.0. Released v1.0.0.
% 58.59/58.68 % Domain : Ring Theory
% 58.59/58.68 % Problem : X.additive_identity = additive_identity for any X
% 58.59/58.68 % Version : [MOW76] axioms.
% 58.59/58.68 % English :
% 58.59/58.68
% 58.59/58.68 % Refs : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% 58.59/58.68 % Source : [MOW76]
% 58.59/58.68 % Names : R1 [MOW76]
% 58.59/58.68 % : zero.ver1.in [ANL]
% 58.59/58.68
% 58.59/58.68 % Status : Unsatisfiable
% 58.59/58.68 % Rating : 0.00 v6.1.0, 0.20 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.27 v5.3.0, 0.42 v5.2.0, 0.12 v5.1.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.00 v3.1.0, 0.11 v2.7.0, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.2.1, 0.11 v2.2.0, 0.14 v2.1.0, 0.00 v2.0.0
% 58.59/58.68 % Syntax : Number of clauses : 18 ( 7 unt; 0 nHn; 12 RR)
% 58.59/58.68 % Number of literals : 51 ( 2 equ; 34 neg)
% 58.59/58.68 % Maximal clause size : 5 ( 2 avg)
% 58.59/58.68 % Maximal term depth : 2 ( 1 avg)
% 58.59/58.68 % Number of predicates : 3 ( 2 usr; 0 prp; 2-3 aty)
% 58.59/58.68 % Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% 58.59/58.68 % Number of variables : 71 ( 0 sgn)
% 58.59/58.68 % SPC : CNF_UNS_RFO_SEQ_HRN
% 58.59/58.68
% 58.59/58.68 % Comments :
% 58.59/58.68 %--------------------------------------------------------------------------
% 58.59/58.68 %----Include ring theory axioms
% 58.59/58.68 include('Axioms/RNG001-0.ax').
% 58.59/58.68 %--------------------------------------------------------------------------
% 58.59/58.68 cnf(prove_a_times_0_is_0,negated_conjecture,
% 58.59/58.68 ~ product(a,additive_identity,additive_identity) ).
% 58.59/58.68
% 58.59/58.68 %--------------------------------------------------------------------------
% 58.59/58.68 %-------------------------------------------
% 58.59/58.68 % Proof found
% 58.59/58.68 % SZS status Theorem for theBenchmark
% 58.59/58.68 % SZS output start Proof
% 58.59/58.69 %ClaNum:32(EqnAxiom:14)
% 58.59/58.69 %VarNum:146(SingletonVarNum:71)
% 58.59/58.69 %MaxLitNum:5
% 58.59/58.69 %MaxfuncDepth:1
% 58.59/58.69 %SharedTerms:3
% 58.59/58.69 %goalClause: 21
% 58.59/58.69 %singleGoalClaCount:1
% 58.59/58.69 [21]~P2(a3,a1,a1)
% 58.59/58.69 [15]P1(x151,a1,x151)
% 58.59/58.69 [16]P1(a1,x161,x161)
% 58.59/58.69 [17]P1(x171,f4(x171),a1)
% 58.59/58.69 [18]P1(f4(x181),x181,a1)
% 58.59/58.69 [19]P1(x191,x192,f2(x191,x192))
% 58.59/58.69 [20]P2(x201,x202,f5(x201,x202))
% 58.59/58.69 [22]~P1(x222,x221,x223)+P1(x221,x222,x223)
% 58.59/58.69 [23]~P1(x233,x234,x231)+E(x231,x232)+~P1(x233,x234,x232)
% 58.59/58.69 [24]~P2(x243,x244,x241)+E(x241,x242)+~P2(x243,x244,x242)
% 58.59/58.69 [25]~P1(x256,x254,x251)+P1(x251,x252,x253)+~P1(x254,x252,x255)+~P1(x256,x255,x253)
% 58.59/58.69 [26]~P1(x261,x266,x264)+P1(x261,x262,x263)+~P1(x264,x265,x263)+~P1(x266,x265,x262)
% 58.59/58.69 [27]~P2(x276,x274,x271)+P2(x271,x272,x273)+~P2(x274,x272,x275)+~P2(x276,x275,x273)
% 58.59/58.69 [28]~P2(x281,x286,x284)+P2(x281,x282,x283)+~P2(x284,x285,x283)+~P2(x286,x285,x282)
% 58.59/58.69 [29]~P2(x297,x295,x292)+~P2(x297,x294,x291)+P1(x291,x292,x293)+~P1(x294,x295,x296)+~P2(x297,x296,x293)
% 58.59/58.69 [30]~P2(x305,x307,x302)+~P2(x304,x307,x301)+P1(x301,x302,x303)+~P1(x304,x305,x306)+~P2(x306,x307,x303)
% 58.59/58.69 [31]~P2(x317,x312,x315)+~P2(x316,x312,x314)+P2(x311,x312,x313)+~P1(x314,x315,x313)+~P1(x316,x317,x311)
% 58.59/58.69 [32]~P2(x321,x327,x325)+~P2(x321,x326,x324)+P2(x321,x322,x323)+~P1(x324,x325,x323)+~P1(x326,x327,x322)
% 58.59/58.69 %EqnAxiom
% 58.59/58.69 [1]E(x11,x11)
% 58.59/58.69 [2]E(x22,x21)+~E(x21,x22)
% 58.59/58.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.59/58.69 [4]~E(x41,x42)+E(f4(x41),f4(x42))
% 58.59/58.69 [5]~E(x51,x52)+E(f5(x51,x53),f5(x52,x53))
% 58.59/58.69 [6]~E(x61,x62)+E(f5(x63,x61),f5(x63,x62))
% 58.59/58.69 [7]~E(x71,x72)+E(f2(x71,x73),f2(x72,x73))
% 58.59/58.69 [8]~E(x81,x82)+E(f2(x83,x81),f2(x83,x82))
% 58.59/58.69 [9]P1(x92,x93,x94)+~E(x91,x92)+~P1(x91,x93,x94)
% 58.59/58.69 [10]P1(x103,x102,x104)+~E(x101,x102)+~P1(x103,x101,x104)
% 58.59/58.69 [11]P1(x113,x114,x112)+~E(x111,x112)+~P1(x113,x114,x111)
% 58.59/58.69 [12]P2(x122,x123,x124)+~E(x121,x122)+~P2(x121,x123,x124)
% 58.59/58.69 [13]P2(x133,x132,x134)+~E(x131,x132)+~P2(x133,x131,x134)
% 58.59/58.69 [14]P2(x143,x144,x142)+~E(x141,x142)+~P2(x143,x144,x141)
% 58.59/58.69
% 58.59/58.69 %-------------------------------------------
% 58.70/58.70 cnf(33,plain,
% 58.70/58.70 (E(x331,f2(x331,a1))),
% 58.70/58.70 inference(scs_inference,[],[15,19,23])).
% 58.70/58.70 cnf(34,plain,
% 58.70/58.70 (P1(x341,x342,f2(x341,x342))),
% 58.70/58.70 inference(rename_variables,[],[19])).
% 58.70/58.70 cnf(36,plain,
% 58.70/58.70 (P1(f2(x361,a1),a1,x361)),
% 58.70/58.70 inference(scs_inference,[],[15,19,23,9])).
% 58.70/58.70 cnf(38,plain,
% 58.70/58.70 (P1(x381,a1,x381)),
% 58.70/58.70 inference(rename_variables,[],[15])).
% 58.70/58.70 cnf(39,plain,
% 58.70/58.70 (P1(x391,f4(x391),f2(a1,a1))),
% 58.70/58.70 inference(scs_inference,[],[15,19,17,23,9,10,11])).
% 58.70/58.70 cnf(40,plain,
% 58.70/58.70 (P2(x401,f2(a1,a1),f5(x401,a1))),
% 58.70/58.70 inference(scs_inference,[],[15,19,20,17,23,9,10,11,13])).
% 58.70/58.70 cnf(41,plain,
% 58.70/58.70 (P2(x411,x412,f5(x411,x412))),
% 58.70/58.70 inference(rename_variables,[],[20])).
% 58.70/58.70 cnf(42,plain,
% 58.70/58.70 (~E(f5(a3,a1),a1)),
% 58.70/58.70 inference(scs_inference,[],[21,15,19,20,41,17,23,9,10,11,13,14])).
% 58.70/58.70 cnf(43,plain,
% 58.70/58.70 (P2(x431,x432,f5(x431,x432))),
% 58.70/58.70 inference(rename_variables,[],[20])).
% 58.70/58.70 cnf(44,plain,
% 58.70/58.70 (P1(x441,f2(a1,a1),x441)),
% 58.70/58.70 inference(scs_inference,[],[21,15,38,19,34,20,41,17,23,9,10,11,13,14,26])).
% 58.70/58.70 cnf(45,plain,
% 58.70/58.70 (P1(x451,x452,f2(x451,x452))),
% 58.70/58.70 inference(rename_variables,[],[19])).
% 58.70/58.70 cnf(47,plain,
% 58.70/58.70 (P2(a1,x471,f2(f5(a1,x471),f5(a1,x471)))),
% 58.70/58.70 inference(scs_inference,[],[21,15,38,19,34,45,20,41,43,17,23,9,10,11,13,14,26,31])).
% 58.70/58.70 cnf(48,plain,
% 58.70/58.70 (P1(x481,x482,f2(x481,x482))),
% 58.70/58.70 inference(rename_variables,[],[19])).
% 58.70/58.70 cnf(49,plain,
% 58.70/58.70 (P1(x491,a1,x491)),
% 58.70/58.70 inference(rename_variables,[],[15])).
% 58.70/58.70 cnf(51,plain,
% 58.70/58.70 (P2(x511,x512,f5(x511,x512))),
% 58.70/58.70 inference(rename_variables,[],[20])).
% 58.70/58.70 cnf(53,plain,
% 58.70/58.70 (P2(x531,a1,f2(f5(x531,a1),f5(x531,a1)))),
% 58.70/58.70 inference(scs_inference,[],[21,15,38,49,19,34,45,48,20,41,43,51,17,23,9,10,11,13,14,26,31,32])).
% 58.70/58.70 cnf(55,plain,
% 58.70/58.70 (P1(x551,a1,x551)),
% 58.70/58.70 inference(rename_variables,[],[15])).
% 58.70/58.70 cnf(57,plain,
% 58.70/58.70 (P2(x571,x572,f5(x571,x572))),
% 58.70/58.70 inference(rename_variables,[],[20])).
% 58.70/58.70 cnf(59,plain,
% 58.70/58.70 (P1(f5(x591,a1),f5(x591,a1),f5(x591,a1))),
% 58.70/58.70 inference(scs_inference,[],[21,15,38,49,55,19,34,45,48,20,41,43,51,57,17,23,9,10,11,13,14,26,31,32,29])).
% 58.70/58.70 cnf(62,plain,
% 58.70/58.70 (P2(x621,x622,f5(x621,x622))),
% 58.70/58.70 inference(rename_variables,[],[20])).
% 58.70/58.70 cnf(63,plain,
% 58.70/58.70 (P1(x631,a1,x631)),
% 58.70/58.70 inference(rename_variables,[],[15])).
% 58.70/58.70 cnf(65,plain,
% 58.70/58.70 (P1(f5(a1,x651),f5(a1,x651),f5(a1,x651))),
% 58.70/58.70 inference(scs_inference,[],[21,15,38,49,55,63,19,34,45,48,20,41,43,51,57,62,17,23,9,10,11,13,14,26,31,32,29,30])).
% 58.70/58.70 cnf(67,plain,
% 58.70/58.70 (P2(x671,x672,f5(x671,x672))),
% 58.70/58.70 inference(rename_variables,[],[20])).
% 58.70/58.70 cnf(68,plain,
% 58.70/58.70 (P2(x681,x682,f5(x681,x682))),
% 58.70/58.70 inference(rename_variables,[],[20])).
% 58.70/58.70 cnf(72,plain,
% 58.70/58.71 (P2(f2(a1,a1),x721,f5(a1,x721))),
% 58.70/58.71 inference(scs_inference,[],[21,15,38,49,55,63,19,34,45,48,20,41,43,51,57,62,68,17,23,9,10,11,13,14,26,31,32,29,30,2,12])).
% 58.70/58.71 cnf(73,plain,
% 58.70/58.71 (P2(x731,x732,f5(x731,x732))),
% 58.70/58.71 inference(rename_variables,[],[20])).
% 58.70/58.71 cnf(74,plain,
% 58.70/58.71 (E(f5(x741,f2(a1,a1)),f5(x741,a1))),
% 58.70/58.71 inference(scs_inference,[],[21,15,38,49,55,63,19,34,45,48,20,41,43,51,57,62,68,73,17,23,9,10,11,13,14,26,31,32,29,30,2,12,24])).
% 58.70/58.71 cnf(75,plain,
% 58.70/58.71 (P2(x751,x752,f5(x751,x752))),
% 58.70/58.71 inference(rename_variables,[],[20])).
% 58.70/58.71 cnf(77,plain,
% 58.70/58.71 (~E(f5(a3,a1),f2(a1,a1))),
% 58.70/58.71 inference(scs_inference,[],[21,15,38,49,55,63,19,34,45,48,20,41,43,51,57,62,68,73,17,23,9,10,11,13,14,26,31,32,29,30,2,12,24,3])).
% 58.70/58.71 cnf(80,plain,
% 58.70/58.71 (P2(x801,f5(x801,x801),f5(f5(x801,x801),x801))),
% 58.70/58.71 inference(scs_inference,[],[21,15,38,49,55,63,19,34,45,48,20,41,43,51,57,62,68,73,75,67,17,23,9,10,11,13,14,26,31,32,29,30,2,12,24,3,27,28])).
% 58.70/58.71 cnf(85,plain,
% 58.70/58.71 (E(f2(x851,a1),x851)),
% 58.70/58.71 inference(scs_inference,[],[33,2])).
% 58.70/58.71 cnf(86,plain,
% 58.70/58.71 (P2(f2(x861,a1),f5(x861,x861),f5(f5(x861,x861),x861))),
% 58.70/58.71 inference(scs_inference,[],[80,33,2,12])).
% 58.70/58.71 cnf(88,plain,
% 58.70/58.71 (P1(a1,x881,f2(x881,a1))),
% 58.70/58.71 inference(scs_inference,[],[80,16,33,2,12,11])).
% 58.70/58.71 cnf(89,plain,
% 58.70/58.71 (P1(a1,x891,x891)),
% 58.70/58.71 inference(rename_variables,[],[16])).
% 58.70/58.71 cnf(90,plain,
% 58.70/58.71 (E(f4(a1),a1)),
% 58.70/58.71 inference(scs_inference,[],[80,16,89,17,33,2,12,11,23])).
% 58.70/58.71 cnf(92,plain,
% 58.70/58.71 (P1(a1,x921,x921)),
% 58.70/58.71 inference(rename_variables,[],[16])).
% 58.70/58.71 cnf(95,plain,
% 58.70/58.71 (E(x951,f2(x951,a1))),
% 58.70/58.71 inference(rename_variables,[],[33])).
% 58.70/58.71 cnf(96,plain,
% 58.70/58.71 (~E(f5(a3,a1),f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[80,72,16,89,17,33,42,2,12,11,23,14,3])).
% 58.70/58.71 cnf(97,plain,
% 58.70/58.71 (P2(f2(a1,a1),f2(x971,a1),f5(a1,x971))),
% 58.70/58.71 inference(scs_inference,[],[80,72,16,89,17,33,95,42,2,12,11,23,14,3,13])).
% 58.70/58.71 cnf(99,plain,
% 58.70/58.71 (P1(a1,f2(x991,a1),x991)),
% 58.70/58.71 inference(scs_inference,[],[80,72,16,89,92,17,33,95,42,2,12,11,23,14,3,13,10])).
% 58.70/58.71 cnf(100,plain,
% 58.70/58.71 (P1(a1,x1001,x1001)),
% 58.70/58.71 inference(rename_variables,[],[16])).
% 58.70/58.71 cnf(101,plain,
% 58.70/58.71 (P1(f2(a1,a1),x1011,x1011)),
% 58.70/58.71 inference(scs_inference,[],[80,72,16,89,92,100,17,33,95,42,2,12,11,23,14,3,13,10,9])).
% 58.70/58.71 cnf(123,plain,
% 58.70/58.71 (E(f5(x1231,a1),f5(x1231,f2(a1,a1)))),
% 58.70/58.71 inference(scs_inference,[],[74,2])).
% 58.70/58.71 cnf(124,plain,
% 58.70/58.71 (E(a1,f4(f2(a1,a1)))),
% 58.70/58.71 inference(scs_inference,[],[17,101,74,2,23])).
% 58.70/58.71 cnf(126,plain,
% 58.70/58.71 (P1(x1261,f4(x1261),a1)),
% 58.70/58.71 inference(rename_variables,[],[17])).
% 58.70/58.71 cnf(129,plain,
% 58.70/58.71 (E(x1291,f2(x1291,a1))),
% 58.70/58.71 inference(rename_variables,[],[33])).
% 58.70/58.71 cnf(130,plain,
% 58.70/58.71 (P2(f2(a1,a1),x1301,f2(f5(a1,x1301),f5(a1,x1301)))),
% 58.70/58.71 inference(scs_inference,[],[47,18,17,101,74,33,129,2,23,11,12])).
% 58.70/58.71 cnf(131,plain,
% 58.70/58.71 (E(x1311,f2(x1311,a1))),
% 58.70/58.71 inference(rename_variables,[],[33])).
% 58.70/58.71 cnf(133,plain,
% 58.70/58.71 (E(f2(x1331,a1),x1331)),
% 58.70/58.71 inference(rename_variables,[],[85])).
% 58.70/58.71 cnf(134,plain,
% 58.70/58.71 (P1(f4(f2(x1341,a1)),x1341,a1)),
% 58.70/58.71 inference(scs_inference,[],[47,18,17,101,77,85,133,74,33,129,2,23,11,12,3,10])).
% 58.70/58.71 cnf(138,plain,
% 58.70/58.71 (~E(f2(f5(a3,a1),f5(a3,a1)),a1)),
% 58.70/58.71 inference(scs_inference,[],[21,47,53,18,17,101,77,85,133,74,33,129,131,2,23,11,12,3,10,13,14])).
% 58.70/58.71 cnf(140,plain,
% 58.70/58.71 (P1(x1401,f4(f2(x1401,a1)),a1)),
% 58.70/58.71 inference(scs_inference,[],[21,47,53,18,17,126,101,77,85,133,74,33,129,131,2,23,11,12,3,10,13,14,9])).
% 58.70/58.71 cnf(142,plain,
% 58.70/58.71 (P1(a1,x1421,f2(f2(x1421,a1),a1))),
% 58.70/58.71 inference(scs_inference,[],[21,47,53,16,18,17,126,101,77,85,133,74,88,99,33,129,131,2,23,11,12,3,10,13,14,9,26])).
% 58.70/58.71 cnf(164,plain,
% 58.70/58.71 (E(a1,f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[90,2])).
% 58.70/58.71 cnf(165,plain,
% 58.70/58.71 (E(f2(f5(a1,x1651),f5(a1,x1651)),f5(a1,x1651))),
% 58.70/58.71 inference(scs_inference,[],[130,72,90,2,24])).
% 58.70/58.71 cnf(168,plain,
% 58.70/58.71 (E(f4(a1),f2(a1,a1))),
% 58.70/58.71 inference(scs_inference,[],[130,72,16,39,90,2,24,23])).
% 58.70/58.71 cnf(170,plain,
% 58.70/58.71 (P1(a1,x1701,x1701)),
% 58.70/58.71 inference(rename_variables,[],[16])).
% 58.70/58.71 cnf(172,plain,
% 58.70/58.71 (P2(a1,f2(x1721,a1),f5(a1,x1721))),
% 58.70/58.71 inference(scs_inference,[],[130,72,97,16,39,90,85,2,24,23,12])).
% 58.70/58.71 cnf(176,plain,
% 58.70/58.71 (E(f5(x1761,a1),f5(x1761,f2(a1,a1)))),
% 58.70/58.71 inference(rename_variables,[],[123])).
% 58.70/58.71 cnf(177,plain,
% 58.70/58.71 (P1(f5(x1771,a1),f5(x1771,f2(a1,a1)),f5(x1771,a1))),
% 58.70/58.71 inference(scs_inference,[],[130,80,72,59,97,16,39,123,176,90,85,2,24,23,12,14,10])).
% 58.70/58.71 cnf(178,plain,
% 58.70/58.71 (P1(f5(x1781,a1),f5(x1781,a1),f5(x1781,a1))),
% 58.70/58.71 inference(rename_variables,[],[59])).
% 58.70/58.71 cnf(180,plain,
% 58.70/58.71 (P1(f5(x1801,a1),f5(x1801,a1),f5(x1801,a1))),
% 58.70/58.71 inference(rename_variables,[],[59])).
% 58.70/58.71 cnf(183,plain,
% 58.70/58.71 (P1(f5(x1831,a1),f5(x1831,a1),f5(x1831,a1))),
% 58.70/58.71 inference(rename_variables,[],[59])).
% 58.70/58.71 cnf(188,plain,
% 58.70/58.71 (P1(f5(x1881,a1),a1,a1)),
% 58.70/58.71 inference(scs_inference,[],[130,80,72,59,178,180,183,97,16,170,17,39,123,176,90,138,85,88,2,24,23,12,14,10,11,3,9,25,26])).
% 58.70/58.71 cnf(197,plain,
% 58.70/58.71 (E(f5(a1,x1971),f2(f5(a1,x1971),f5(a1,x1971)))),
% 58.70/58.71 inference(scs_inference,[],[165,2])).
% 58.70/58.71 cnf(198,plain,
% 58.70/58.71 (E(f5(a1,x1981),f5(a1,f2(x1981,a1)))),
% 58.70/58.71 inference(scs_inference,[],[172,165,20,2,24])).
% 58.70/58.71 cnf(201,plain,
% 58.70/58.71 (E(f4(f2(a1,a1)),a1)),
% 58.70/58.71 inference(scs_inference,[],[172,16,165,140,20,2,24,23])).
% 58.70/58.71 cnf(203,plain,
% 58.70/58.71 (P1(a1,x2031,x2031)),
% 58.70/58.71 inference(rename_variables,[],[16])).
% 58.70/58.71 cnf(207,plain,
% 58.70/58.71 (P1(a1,x2071,x2071)),
% 58.70/58.71 inference(rename_variables,[],[16])).
% 58.70/58.71 cnf(208,plain,
% 58.70/58.71 (E(f2(a1,a1),f4(f2(a1,a1)))),
% 58.70/58.71 inference(scs_inference,[],[172,16,203,165,140,124,20,85,2,24,23,12,10,3])).
% 58.70/58.71 cnf(213,plain,
% 58.70/58.71 (P1(a1,f2(f5(a1,x2131),f5(a1,x2131)),f5(a1,x2131))),
% 58.70/58.71 inference(scs_inference,[],[172,86,16,203,207,165,140,124,123,20,85,2,24,23,12,10,3,14,11])).
% 58.70/58.71 cnf(214,plain,
% 58.70/58.71 (P1(a1,x2141,x2141)),
% 58.70/58.71 inference(rename_variables,[],[16])).
% 58.70/58.71 cnf(216,plain,
% 58.70/58.71 (P1(f5(a1,x2161),a1,a1)),
% 58.70/58.71 inference(scs_inference,[],[172,86,65,16,203,207,214,17,165,140,124,123,20,85,2,24,23,12,10,3,14,11,9,26])).
% 58.70/58.71 cnf(219,plain,
% 58.70/58.71 (P1(a1,f5(a1,x2191),a1)),
% 58.70/58.71 inference(scs_inference,[],[172,86,65,16,203,207,214,18,17,165,140,124,123,20,85,2,24,23,12,10,3,14,11,9,26,25])).
% 58.70/58.71 cnf(238,plain,
% 58.70/58.71 (E(f4(f2(a1,a1)),f2(a1,a1))),
% 58.70/58.71 inference(scs_inference,[],[208,2])).
% 58.70/58.71 cnf(239,plain,
% 58.70/58.71 (E(x2391,f2(f2(x2391,a1),a1))),
% 58.70/58.71 inference(scs_inference,[],[16,208,142,2,23])).
% 58.70/58.71 cnf(242,plain,
% 58.70/58.71 (P2(a1,f4(f2(a1,a1)),f5(a1,a1))),
% 58.70/58.71 inference(scs_inference,[],[172,16,208,142,2,23,13])).
% 58.70/58.71 cnf(243,plain,
% 58.70/58.71 (P2(a1,f2(x2431,a1),f5(a1,x2431))),
% 58.70/58.71 inference(rename_variables,[],[172])).
% 58.70/58.71 cnf(244,plain,
% 58.70/58.71 (P2(f4(a1),f2(x2441,a1),f5(a1,x2441))),
% 58.70/58.71 inference(scs_inference,[],[172,243,16,208,142,164,2,23,13,12])).
% 58.70/58.71 cnf(247,plain,
% 58.70/58.71 (E(f4(a1),f4(f2(a1,a1)))),
% 58.70/58.71 inference(scs_inference,[],[172,243,16,208,168,142,164,2,23,13,12,11,3])).
% 58.70/58.71 cnf(248,plain,
% 58.70/58.71 (P2(a1,f2(x2481,a1),f2(f5(a1,x2481),f5(a1,x2481)))),
% 58.70/58.71 inference(scs_inference,[],[172,243,16,208,197,168,142,164,2,23,13,12,11,3,14])).
% 58.70/58.71 cnf(274,plain,
% 58.70/58.71 (E(f2(f2(x2741,a1),a1),x2741)),
% 58.70/58.71 inference(scs_inference,[],[239,2])).
% 58.70/58.71 cnf(276,plain,
% 58.70/58.71 (E(x2761,f2(f2(x2761,a1),a1))),
% 58.70/58.71 inference(rename_variables,[],[239])).
% 58.70/58.71 cnf(277,plain,
% 58.70/58.71 (E(f5(x2771,a1),f2(f5(x2771,a1),f5(x2771,a1)))),
% 58.70/58.71 inference(scs_inference,[],[172,59,239,19,2,12,23])).
% 58.70/58.71 cnf(281,plain,
% 58.70/58.71 (P1(f2(a1,a1),f2(a1,a1),a1)),
% 58.70/58.71 inference(scs_inference,[],[172,59,17,238,239,77,19,2,12,23,3,10])).
% 58.70/58.71 cnf(282,plain,
% 58.70/58.71 (P1(x2821,f4(x2821),a1)),
% 58.70/58.71 inference(rename_variables,[],[17])).
% 58.70/58.71 cnf(284,plain,
% 58.70/58.71 (E(x2841,f2(f2(x2841,a1),a1))),
% 58.70/58.71 inference(rename_variables,[],[239])).
% 58.70/58.71 cnf(287,plain,
% 58.70/58.71 (P1(f4(a1),f4(a1),a1)),
% 58.70/58.71 inference(scs_inference,[],[172,59,17,282,18,16,238,239,276,284,77,19,2,12,23,3,10,11,9,26])).
% 58.70/58.71 cnf(307,plain,
% 58.70/58.71 (P2(a1,x3071,f5(a1,f2(x3071,a1)))),
% 58.70/58.71 inference(scs_inference,[],[172,277,274,2,13])).
% 58.70/58.71 cnf(309,plain,
% 58.70/58.71 (E(a1,f2(f4(a1),a1))),
% 58.70/58.71 inference(scs_inference,[],[172,17,277,274,88,2,13,23])).
% 58.70/58.71 cnf(311,plain,
% 58.70/58.71 (P1(x3111,f4(x3111),a1)),
% 58.70/58.71 inference(rename_variables,[],[17])).
% 58.70/58.71 cnf(317,plain,
% 58.70/58.71 (P1(x3171,f4(x3171),f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[172,244,47,17,311,277,274,164,88,2,13,23,12,14,11])).
% 58.70/58.71 cnf(332,plain,
% 58.70/58.71 (P1(f4(x3321),x3321,f2(f2(a1,a1),a1))),
% 58.70/58.71 inference(scs_inference,[],[18,247,239,2,11])).
% 58.70/58.71 cnf(333,plain,
% 58.70/58.71 (E(x3331,f2(f2(x3331,a1),a1))),
% 58.70/58.71 inference(rename_variables,[],[239])).
% 58.70/58.71 cnf(336,plain,
% 58.70/58.71 (P1(f2(f2(a1,a1),a1),f5(a1,x3361),a1)),
% 58.70/58.71 inference(scs_inference,[],[18,16,201,247,239,333,219,2,11,10,9])).
% 58.70/58.71 cnf(338,plain,
% 58.70/58.71 (P1(f5(a1,x3381),f4(a1),f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[65,18,16,201,247,239,333,317,219,2,11,10,9,26])).
% 58.70/58.71 cnf(352,plain,
% 58.70/58.71 (E(f2(a1,a1),f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[168,2])).
% 58.70/58.71 cnf(353,plain,
% 58.70/58.71 (P2(f4(a1),f4(f2(a1,a1)),f5(a1,a1))),
% 58.70/58.71 inference(scs_inference,[],[242,168,164,2,12])).
% 58.70/58.71 cnf(355,plain,
% 58.70/58.71 (P2(a1,f2(x3551,a1),f2(f5(a1,x3551),a1))),
% 58.70/58.71 inference(scs_inference,[],[172,53,242,168,164,33,2,12,13,14])).
% 58.70/58.71 cnf(356,plain,
% 58.70/58.71 (E(x3561,f2(x3561,a1))),
% 58.70/58.71 inference(rename_variables,[],[33])).
% 58.70/58.71 cnf(358,plain,
% 58.70/58.71 (E(x3581,f2(x3581,a1))),
% 58.70/58.71 inference(rename_variables,[],[33])).
% 58.70/58.71 cnf(360,plain,
% 58.70/58.71 (E(x3601,f2(x3601,a1))),
% 58.70/58.71 inference(rename_variables,[],[33])).
% 58.70/58.71 cnf(363,plain,
% 58.70/58.71 (P1(f4(a1),x3631,f2(x3631,a1))),
% 58.70/58.71 inference(scs_inference,[],[172,53,65,242,168,164,33,356,358,360,18,16,99,2,12,13,14,10,11,9,26])).
% 58.70/58.71 cnf(367,plain,
% 58.70/58.71 (P1(a1,a1,f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[172,53,65,242,168,164,33,356,358,360,17,18,16,99,19,2,12,13,14,10,11,9,26,25])).
% 58.70/58.71 cnf(385,plain,
% 58.70/58.71 (E(f4(a1),f2(f2(a1,a1),a1))),
% 58.70/58.71 inference(scs_inference,[],[15,332,309,2,23])).
% 58.70/58.71 cnf(390,plain,
% 58.70/58.71 (P2(f4(a1),a1,f5(a1,a1))),
% 58.70/58.71 inference(scs_inference,[],[353,201,15,332,309,42,2,23,3,13])).
% 58.70/58.71 cnf(416,plain,
% 58.70/58.71 (E(f2(f4(a1),a1),f2(a1,a1))),
% 58.70/58.71 inference(scs_inference,[],[88,385,39,2,23])).
% 58.70/58.71 cnf(440,plain,
% 58.70/58.71 (P1(f2(a1,a1),f2(a1,a1),f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[72,281,90,40,164,88,416,2,12,13,10,11])).
% 58.70/58.71 cnf(441,plain,
% 58.70/58.71 (P1(f4(a1),x4411,x4411)),
% 58.70/58.71 inference(scs_inference,[],[72,281,90,40,164,88,16,416,2,12,13,10,11,9])).
% 58.70/58.71 cnf(458,plain,
% 58.70/58.71 (P2(f2(a1,a1),x4581,f5(f4(a1),x4581))),
% 58.70/58.71 inference(scs_inference,[],[168,20,198,2,12])).
% 58.70/58.71 cnf(466,plain,
% 58.70/58.71 (P1(a1,x4661,f2(f4(a1),f2(x4661,a1)))),
% 58.70/58.71 inference(scs_inference,[],[72,168,20,164,367,17,15,18,19,99,198,2,12,13,10,11,9,26])).
% 58.70/58.71 cnf(469,plain,
% 58.70/58.71 (P1(f4(a1),f2(x4691,a1),x4691)),
% 58.70/58.71 inference(scs_inference,[],[72,168,20,164,367,17,15,18,16,19,99,198,2,12,13,10,11,9,26,25])).
% 58.70/58.71 cnf(472,plain,
% 58.70/58.71 (E(f4(a1),f2(f4(a1),f2(a1,a1)))),
% 58.70/58.71 inference(scs_inference,[],[72,168,20,164,367,17,15,18,16,19,99,198,2,12,13,10,11,9,26,25,23])).
% 58.70/58.71 cnf(486,plain,
% 58.70/58.71 (E(f2(f4(a1),f2(x4861,a1)),x4861)),
% 58.70/58.71 inference(scs_inference,[],[19,469,472,2,23])).
% 58.70/58.71 cnf(501,plain,
% 58.70/58.71 (P2(f4(a1),x5011,f5(a1,f2(x5011,a1)))),
% 58.70/58.71 inference(scs_inference,[],[307,164,486,2,12])).
% 58.70/58.71 cnf(503,plain,
% 58.70/58.71 (P1(f2(x5031,a1),f4(a1),x5031)),
% 58.70/58.71 inference(scs_inference,[],[390,307,164,36,486,2,12,13,10])).
% 58.70/58.71 cnf(514,plain,
% 58.70/58.71 (E(f2(f2(x5141,a1),f4(a1)),x5141)),
% 58.70/58.71 inference(scs_inference,[],[390,307,367,247,20,164,17,15,19,134,36,142,486,2,12,13,10,9,11,28,26,23])).
% 58.70/58.71 cnf(530,plain,
% 58.70/58.71 (E(f4(a1),f2(f2(a1,a1),f4(a1)))),
% 58.70/58.71 inference(scs_inference,[],[90,514,2,3])).
% 58.70/58.71 cnf(555,plain,
% 58.70/58.71 (P1(f2(a1,a1),x5551,f2(x5551,a1))),
% 58.70/58.71 inference(scs_inference,[],[501,458,168,99,18,363,530,2,12,10,13,11,9])).
% 58.70/58.71 cnf(556,plain,
% 58.70/58.71 (P1(f4(a1),f2(f2(a1,a1),a1),f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[501,458,287,367,168,99,18,332,363,530,2,12,10,13,11,9,26])).
% 58.70/58.71 cnf(608,plain,
% 58.70/58.71 (P1(f4(a1),f5(a1,x6081),a1)),
% 58.70/58.71 inference(scs_inference,[],[164,216,219,248,12,10,9])).
% 58.70/58.71 cnf(630,plain,
% 58.70/58.71 (P1(f5(x6301,a1),a1,f4(a1))),
% 58.70/58.71 inference(scs_inference,[],[164,188,466,355,12,9,10,11])).
% 58.70/58.71 cnf(633,plain,
% 58.70/58.72 (P1(f4(a1),f4(a1),f2(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[287,164,99,188,466,556,355,12,9,10,11,25,26])).
% 58.70/58.72 cnf(698,plain,
% 58.70/58.72 (P2(x6981,f2(a1,a1),f5(x6981,f4(a1)))),
% 58.70/58.72 inference(scs_inference,[],[168,20,13])).
% 58.70/58.72 cnf(931,plain,
% 58.70/58.72 (P1(a1,a1,f5(a1,x9311))),
% 58.70/58.72 inference(scs_inference,[],[244,99,101,698,336,24,26])).
% 58.70/58.72 cnf(937,plain,
% 58.70/58.72 (P1(f4(f2(a1,a1)),a1,f5(a1,x9371))),
% 58.70/58.72 inference(scs_inference,[],[244,99,124,101,698,336,24,26,2,10,9])).
% 58.70/58.72 cnf(948,plain,
% 58.70/58.72 (P1(f5(x9481,a1),f4(a1),f4(a1))),
% 58.70/58.72 inference(scs_inference,[],[630,164,213,9,10])).
% 58.70/58.72 cnf(982,plain,
% 58.70/58.72 (P1(f2(a1,a1),f5(a1,x9821),f4(a1))),
% 58.70/58.72 inference(scs_inference,[],[15,317,937,26])).
% 58.70/58.72 cnf(1489,plain,
% 58.70/58.72 (P1(a1,f4(a1),f5(a1,x14891))),
% 58.70/58.72 inference(scs_inference,[],[931,164,10])).
% 58.70/58.72 cnf(1491,plain,
% 58.70/58.72 (P1(f4(a1),f5(a1,x14911),f4(a1))),
% 58.70/58.72 inference(scs_inference,[],[608,931,164,10,9,11])).
% 58.70/58.72 cnf(1668,plain,
% 58.70/58.72 (P1(f2(a1,a1),f4(a1),f5(a1,x16681))),
% 58.70/58.72 inference(scs_inference,[],[440,441,982,26])).
% 58.70/58.72 cnf(2034,plain,
% 58.70/58.72 (E(x20341,f2(a1,x20341))),
% 58.70/58.72 inference(scs_inference,[],[16,19,23])).
% 58.70/58.72 cnf(2067,plain,
% 58.70/58.72 (E(f2(a1,x20671),x20671)),
% 58.70/58.72 inference(scs_inference,[],[2034,2])).
% 58.70/58.72 cnf(2130,plain,
% 58.70/58.72 (P1(x21301,f4(a1),f2(x21301,a1))),
% 58.70/58.72 inference(scs_inference,[],[469,503,363,25])).
% 58.70/58.72 cnf(2415,plain,
% 58.70/58.72 (P1(f5(a1,x24151),f2(a1,a1),f4(a1))),
% 58.70/58.72 inference(scs_inference,[],[338,168,10])).
% 58.70/58.72 cnf(2977,plain,
% 58.70/58.72 (P1(f5(x29771,a1),a1,f2(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[555,630,168,10,11])).
% 58.70/58.72 cnf(2978,plain,
% 58.70/58.72 (P1(f2(a1,a1),x29781,f2(f4(a1),x29781))),
% 58.70/58.72 inference(scs_inference,[],[555,630,19,168,10,11,9])).
% 58.70/58.72 cnf(2991,plain,
% 58.70/58.72 (P1(f2(a1,a1),x29911,f2(f4(a1),x29911))),
% 58.70/58.72 inference(rename_variables,[],[2978])).
% 58.70/58.72 cnf(2994,plain,
% 58.70/58.72 (P1(a1,x29941,f2(f4(a1),x29941))),
% 58.70/58.72 inference(scs_inference,[],[16,101,124,2978,2991,2977,23,10,25])).
% 58.70/58.72 cnf(3124,plain,
% 58.70/58.72 (E(f4(a1),f2(x31241,f4(x31241)))),
% 58.70/58.72 inference(scs_inference,[],[17,19,90,23,3])).
% 58.70/58.72 cnf(3126,plain,
% 58.70/58.72 (P1(x31261,f4(x31261),a1)),
% 58.70/58.72 inference(rename_variables,[],[17])).
% 58.70/58.72 cnf(3133,plain,
% 58.70/58.72 (P1(a1,f5(a1,x31331),f2(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[17,3126,172,72,458,1491,441,2130,19,90,23,3,26,27,25])).
% 58.70/58.72 cnf(3151,plain,
% 58.70/58.72 (P1(f4(a1),f4(a1),f5(a1,x31511))),
% 58.70/58.72 inference(scs_inference,[],[17,1489,164,140,2994,3124,2,23,11,9])).
% 58.70/58.72 cnf(3152,plain,
% 58.70/58.72 (P1(f5(x31521,a1),f4(a1),f2(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[17,1489,164,140,2977,2994,3124,2,23,11,9,10])).
% 58.70/58.72 cnf(3250,plain,
% 58.70/58.72 (P1(f2(a1,a1),f5(a1,x32501),f2(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[17,1491,88,633,26,25])).
% 58.70/58.72 cnf(3270,plain,
% 58.70/58.72 (P1(f4(a1),f5(a1,x32701),f4(a1))),
% 58.70/58.72 inference(rename_variables,[],[1491])).
% 58.70/58.72 cnf(3273,plain,
% 58.70/58.72 (P1(f5(a1,x32731),f5(a1,x32732),f5(a1,x32731))),
% 58.70/58.72 inference(scs_inference,[],[1491,3270,441,1489,177,26,25])).
% 58.70/58.72 cnf(3329,plain,
% 58.70/58.72 (P1(f5(a1,x33291),f2(a1,a1),a1)),
% 58.70/58.72 inference(scs_inference,[],[90,2415,11])).
% 58.70/58.72 cnf(3408,plain,
% 58.70/58.72 (P1(f2(x34081,a1),f4(x34081),a1)),
% 58.70/58.72 inference(scs_inference,[],[17,36,16,26])).
% 58.70/58.72 cnf(3794,plain,
% 58.70/58.72 (P1(f2(x37941,a1),f4(x37941),f4(a1))),
% 58.70/58.72 inference(scs_inference,[],[164,3408,11])).
% 58.70/58.72 cnf(3795,plain,
% 58.70/58.72 (P2(f4(a1),x37951,f5(a1,x37951))),
% 58.70/58.72 inference(scs_inference,[],[72,164,352,3408,11,12])).
% 58.70/58.72 cnf(3796,plain,
% 58.70/58.72 (P2(x37961,f4(a1),f5(x37961,a1))),
% 58.70/58.72 inference(scs_inference,[],[72,40,164,352,3408,11,12,13])).
% 58.70/58.72 cnf(3810,plain,
% 58.70/58.72 (P1(f5(a1,x38101),f5(a1,x38102),f5(a1,x38102))),
% 58.70/58.72 inference(scs_inference,[],[3273,22])).
% 58.70/58.72 cnf(3812,plain,
% 58.70/58.72 (~E(f4(a1),f5(a3,a1))),
% 58.70/58.72 inference(scs_inference,[],[3273,96,22,2])).
% 58.70/58.72 cnf(3818,plain,
% 58.70/58.72 (~P2(f2(a1,a3),a1,a1)),
% 58.70/58.72 inference(scs_inference,[],[21,3794,3273,2067,96,40,22,2,23,24,12])).
% 58.70/58.72 cnf(3819,plain,
% 58.70/58.72 (E(f2(a1,x38191),x38191)),
% 58.70/58.72 inference(rename_variables,[],[2067])).
% 58.70/58.72 cnf(3821,plain,
% 58.70/58.72 (E(f2(a1,x38211),x38211)),
% 58.70/58.72 inference(rename_variables,[],[2067])).
% 58.70/58.72 cnf(3822,plain,
% 58.70/58.72 (~P2(a3,a1,f2(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[21,3794,3273,2067,3819,3821,96,40,22,2,23,24,12,13,14])).
% 58.70/58.72 cnf(3824,plain,
% 58.70/58.72 (~P1(f2(a1,a1),f2(a1,a1),f5(a3,a1))),
% 58.70/58.72 inference(scs_inference,[],[21,3794,3273,2067,3819,3821,3250,3152,96,40,22,2,23,24,12,13,14,25])).
% 58.70/58.72 cnf(3826,plain,
% 58.70/58.72 (P1(f5(x38261,a1),f4(a1),f2(a1,a1))),
% 58.70/58.72 inference(rename_variables,[],[3152])).
% 58.70/58.72 cnf(3828,plain,
% 58.70/58.72 (P1(f5(x38281,a1),f5(a1,x38282),f4(a1))),
% 58.70/58.72 inference(scs_inference,[],[21,3794,3273,2067,3819,3821,3250,3152,3826,96,3151,40,22,2,23,24,12,13,14,25,26])).
% 58.70/58.72 cnf(3829,plain,
% 58.70/58.72 (P1(f2(x38291,a1),f4(x38291),f4(a1))),
% 58.70/58.72 inference(rename_variables,[],[3794])).
% 58.70/58.72 cnf(3831,plain,
% 58.70/58.72 (P2(f4(a1),f5(a1,x38311),f5(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[21,3795,3794,3273,2067,3819,3821,3250,3152,3826,96,3151,931,40,22,2,23,24,12,13,14,25,26,32])).
% 58.70/58.72 cnf(3833,plain,
% 58.70/58.72 (P2(f4(a1),x38331,f5(a1,x38331))),
% 58.70/58.72 inference(rename_variables,[],[3795])).
% 58.70/58.72 cnf(3834,plain,
% 58.70/58.72 (P1(f5(a1,x38341),f5(a1,x38342),f5(a1,x38341))),
% 58.70/58.72 inference(rename_variables,[],[3273])).
% 58.70/58.72 cnf(3836,plain,
% 58.70/58.72 (P2(f5(a1,x38361),x38362,f5(a1,x38362))),
% 58.70/58.72 inference(scs_inference,[],[21,3795,3833,3794,3273,3834,2067,3819,3821,3250,3152,3826,96,3151,931,40,22,2,23,24,12,13,14,25,26,32,31])).
% 58.70/58.72 cnf(3841,plain,
% 58.70/58.72 (~E(a1,f5(a3,a1))),
% 58.70/58.72 inference(scs_inference,[],[21,3795,3833,3794,3273,3834,2067,3819,3821,3250,3152,3826,96,3151,931,40,90,22,2,23,24,12,13,14,25,26,32,31,3])).
% 58.70/58.72 cnf(3842,plain,
% 58.70/58.72 (P1(f2(x38421,a1),f4(x38421),f2(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[21,3795,3833,3794,3829,3273,3834,2067,3819,3821,3250,3152,3826,96,3151,931,40,90,168,22,2,23,24,12,13,14,25,26,32,31,3,11])).
% 58.70/58.72 cnf(3854,plain,
% 58.70/58.72 (P1(f4(x38541),f2(x38541,a1),f2(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[3842,22])).
% 58.70/58.72 cnf(3856,plain,
% 58.70/58.72 (~E(f2(a1,a1),f5(a3,a1))),
% 58.70/58.72 inference(scs_inference,[],[3842,77,22,2])).
% 58.70/58.72 cnf(3860,plain,
% 58.70/58.72 (P2(x38601,f4(a1),f5(x38601,a1))),
% 58.70/58.72 inference(rename_variables,[],[3796])).
% 58.70/58.72 cnf(3863,plain,
% 58.70/58.72 (E(f2(a1,x38631),x38631)),
% 58.70/58.72 inference(rename_variables,[],[2067])).
% 58.70/58.72 cnf(3865,plain,
% 58.70/58.72 (E(f2(a1,x38651),x38651)),
% 58.70/58.72 inference(rename_variables,[],[2067])).
% 58.70/58.72 cnf(3867,plain,
% 58.70/58.72 (E(f2(a1,x38671),x38671)),
% 58.70/58.72 inference(rename_variables,[],[2067])).
% 58.70/58.72 cnf(3871,plain,
% 58.70/58.72 (P2(f5(a1,a1),x38711,f5(a1,a1))),
% 58.70/58.72 inference(scs_inference,[],[3824,3822,3842,3836,3812,3831,3828,3841,3818,3329,3133,3796,2067,3863,3865,77,22,2,23,24,12,13,14,25,27])).
% 58.70/58.72 cnf(3872,plain,
% 58.70/58.72 (P2(f4(a1),f5(a1,x38721),f5(a1,a1))),
% 58.70/58.72 inference(rename_variables,[],[3831])).
% 58.70/58.72 cnf(3873,plain,
% 58.70/58.72 (P2(f5(a1,x38731),x38732,f5(a1,x38732))),
% 58.70/58.72 inference(rename_variables,[],[3836])).
% 58.70/58.72 cnf(3876,plain,
% 58.70/58.72 (P1(f2(x38761,a1),f4(x38761),f2(a1,a1))),
% 58.70/58.72 inference(rename_variables,[],[3842])).
% 58.70/58.72 cnf(3877,plain,
% 58.70/58.72 (P2(f5(a1,x38771),x38772,f5(a1,x38772))),
% 58.70/58.72 inference(rename_variables,[],[3836])).
% 58.70/58.72 cnf(3893,plain,
% 58.70/58.72 (~P1(f5(a3,a1),f5(a3,a1),a1)),
% 58.70/58.72 inference(scs_inference,[],[21,3824,3822,3842,3876,3836,3873,3877,3810,3812,3831,3872,3828,3841,3818,3329,3133,1668,3796,3860,2067,3863,3865,3867,77,633,40,287,22,2,23,24,12,13,14,25,27,29,31,10,28,26,32])).
% 58.70/58.72 cnf(3909,plain,
% 58.70/58.72 ($false),
% 58.70/58.72 inference(scs_inference,[],[21,3856,3871,3854,3893,948,3836,85,90,44,22,23,24,11,12,14,25]),
% 58.70/58.72 ['proof']).
% 58.70/58.72 % SZS output end Proof
% 58.70/58.72 % Total time :58.040000s
%------------------------------------------------------------------------------