%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : ROB009-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 : n008.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:10:24 EDT 2024
% Result : Unsatisfiable 113.59s 113.72s
% Output : CNFRefutation 113.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ROB009-1 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.35 % Computer : n008.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Wed Jun 19 18:35:39 EDT 2024
% 0.12/0.35 % CPUTime :
% 0.53/0.62 start to proof:theBenchmark
% 113.59/113.70 %-------------------------------------------
% 113.59/113.70 % File :CSE---1.7
% 113.59/113.70 % Problem :theBenchmark
% 113.59/113.70 % Transform :cnf
% 113.59/113.70 % Format :tptp:raw
% 113.59/113.70 % Command :java -jar mcs_scs.jar %d %s
% 113.59/113.70
% 113.59/113.70 % Result :Theorem 113.040000s
% 113.59/113.70 % Output :CNFRefutation 113.040000s
% 113.59/113.70 %-------------------------------------------
% 113.59/113.72 %--------------------------------------------------------------------------
% 113.59/113.72 % File : ROB009-1 : TPTP v8.2.0. Released v1.0.0.
% 113.59/113.72 % Domain : Robbins Algebra
% 113.59/113.72 % Problem : If -(a + -(b + c)) = -(b + -(a + c)) then a = b
% 113.59/113.72 % Version : [Win90] (equality) axioms.
% 113.59/113.72 % English :
% 113.59/113.72
% 113.59/113.72 % Refs : [Win90] Winker (1990), Robbins Algebra: Conditions that make a
% 113.59/113.72 % Source : [Win90]
% 113.59/113.72 % Names : Lemma 3.2 [Win90]
% 113.59/113.72
% 113.59/113.72 % Status : Unsatisfiable
% 113.59/113.72 % Rating : 0.09 v8.2.0, 0.12 v8.1.0, 0.15 v7.5.0, 0.12 v7.4.0, 0.17 v7.3.0, 0.11 v7.1.0, 0.06 v7.0.0, 0.11 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.12 v6.0.0, 0.24 v5.5.0, 0.21 v5.4.0, 0.07 v5.3.0, 0.00 v5.1.0, 0.13 v5.0.0, 0.14 v4.1.0, 0.18 v4.0.1, 0.14 v4.0.0, 0.15 v3.7.0, 0.11 v3.4.0, 0.00 v2.2.1, 0.22 v2.2.0, 0.14 v2.1.0, 0.50 v2.0.0
% 113.59/113.72 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 2 RR)
% 113.59/113.72 % Number of literals : 5 ( 5 equ; 1 neg)
% 113.59/113.72 % Maximal clause size : 1 ( 1 avg)
% 113.59/113.72 % Maximal term depth : 6 ( 2 avg)
% 113.59/113.72 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 113.59/113.72 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 113.59/113.72 % Number of variables : 7 ( 0 sgn)
% 113.59/113.72 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 113.59/113.72
% 113.59/113.72 % Comments :
% 113.59/113.72 %--------------------------------------------------------------------------
% 113.59/113.72 %----Include axioms for Robbins algebra
% 113.59/113.72 include('Axioms/ROB001-0.ax').
% 113.59/113.72 %--------------------------------------------------------------------------
% 113.59/113.72 cnf(condition,hypothesis,
% 113.59/113.72 negate(add(a,negate(add(b,c)))) = negate(add(b,negate(add(a,c)))) ).
% 113.59/113.72
% 113.59/113.72 cnf(prove_result,negated_conjecture,
% 113.59/113.72 a != b ).
% 113.59/113.72
% 113.59/113.72 %--------------------------------------------------------------------------
% 113.59/113.72 %-------------------------------------------
% 113.59/113.72 % Proof found
% 113.59/113.72 % SZS status Theorem for theBenchmark
% 113.59/113.72 % SZS output start Proof
% 113.70/113.75 %ClaNum:11(EqnAxiom:6)
% 113.70/113.75 %VarNum:15(SingletonVarNum:7)
% 113.70/113.75 %MaxLitNum:1
% 113.70/113.75 %MaxfuncDepth:5
% 113.70/113.75 %SharedTerms:11
% 113.70/113.75 %goalClause: 11
% 113.70/113.75 %singleGoalClaCount:1
% 113.70/113.75 [11]~E(a2,a3)
% 113.70/113.75 [9]E(f5(f1(a2,f5(f1(a3,a4)))),f5(f1(a3,f5(f1(a2,a4)))))
% 113.70/113.75 [7]E(f1(x71,x72),f1(x72,x71))
% 113.70/113.76 [10]E(f5(f1(f5(f1(x101,x102)),f5(f1(x101,f5(x102))))),x101)
% 113.70/113.76 [8]E(f1(f1(x81,x82),x83),f1(x81,f1(x82,x83)))
% 113.70/113.76 %EqnAxiom
% 113.70/113.76 [1]E(x11,x11)
% 113.70/113.76 [2]E(x22,x21)+~E(x21,x22)
% 113.70/113.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 113.70/113.76 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43))
% 113.70/113.76 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52))
% 113.70/113.76 [6]~E(x61,x62)+E(f5(x61),f5(x62))
% 113.70/113.76
% 113.70/113.76 %-------------------------------------------
% 113.70/113.80 cnf(12,plain,
% 113.70/113.80 (E(f1(x121,f1(x122,x123)),f1(f1(x121,x122),x123))),
% 113.70/113.80 inference(scs_inference,[],[8,2])).
% 113.70/113.80 cnf(13,plain,
% 113.70/113.80 (E(f1(x131,f1(x132,x133)),f1(x132,f1(x133,x131)))),
% 113.70/113.80 inference(scs_inference,[],[7,8,2,3])).
% 113.70/113.80 cnf(16,plain,
% 113.70/113.80 (E(f1(x161,f1(x162,x163)),f1(x163,f1(x161,x162)))),
% 113.70/113.80 inference(scs_inference,[],[13,2])).
% 113.70/113.80 cnf(17,plain,
% 113.70/113.80 (~E(a2,f5(f1(f5(f1(a3,x171)),f5(f1(a3,f5(x171))))))),
% 113.70/113.80 inference(scs_inference,[],[11,13,10,2,3])).
% 113.70/113.80 cnf(20,plain,
% 113.70/113.80 (E(f1(x201,f1(x202,x203)),f1(f1(x203,x201),x202))),
% 113.70/113.80 inference(scs_inference,[],[12,16,9,2,3])).
% 113.70/113.80 cnf(22,plain,
% 113.70/113.80 (E(f1(f1(x221,x222),x223),f1(x222,f1(x223,x221)))),
% 113.70/113.80 inference(scs_inference,[],[20,2])).
% 113.70/113.80 cnf(23,plain,
% 113.70/113.80 (E(f1(x231,f1(x232,f1(x233,x234))),f1(f1(x234,f1(x231,x232)),x233))),
% 113.70/113.80 inference(scs_inference,[],[12,20,2,3])).
% 113.70/113.80 cnf(26,plain,
% 113.70/113.80 (E(f1(f1(x261,f1(x262,x263)),x264),f1(x262,f1(x263,f1(x264,x261))))),
% 113.70/113.80 inference(scs_inference,[],[23,2])).
% 113.70/113.80 cnf(27,plain,
% 113.70/113.80 (E(f1(x271,f1(x272,f1(x273,x274))),f1(x274,f1(f1(x271,x272),x273)))),
% 113.70/113.80 inference(scs_inference,[],[22,16,23,2,3])).
% 113.70/113.80 cnf(30,plain,
% 113.70/113.80 (E(f1(x301,f1(f1(x302,x303),x304)),f1(x302,f1(x303,f1(x304,x301))))),
% 113.70/113.80 inference(scs_inference,[],[27,2])).
% 113.70/113.80 cnf(31,plain,
% 113.70/113.80 (E(f1(f1(x311,f1(x312,f1(x313,x314))),x315),f1(x313,f1(x314,f1(f1(x315,x311),x312))))),
% 113.70/113.80 inference(scs_inference,[],[26,22,27,2,3])).
% 113.70/113.80 cnf(34,plain,
% 113.70/113.80 (E(f1(x341,f1(x342,f1(f1(x343,x344),x345))),f1(f1(x344,f1(x345,f1(x341,x342))),x343))),
% 113.70/113.80 inference(scs_inference,[],[31,2])).
% 113.70/113.80 cnf(35,plain,
% 113.70/113.80 (E(f1(x351,f1(f1(f1(x352,x353),x354),x355)),f1(x353,f1(f1(x354,f1(x355,x351)),x352)))),
% 113.70/113.80 inference(scs_inference,[],[30,22,31,2,3])).
% 113.70/113.80 cnf(38,plain,
% 113.70/113.80 (E(f1(x381,f1(f1(x382,f1(x383,x384)),x385)),f1(x384,f1(f1(f1(x385,x381),x382),x383)))),
% 113.70/113.80 inference(scs_inference,[],[35,2])).
% 113.70/113.80 cnf(39,plain,
% 113.70/113.80 (E(f1(x391,f1(x392,f1(f1(x393,x394),x395))),f1(x394,f1(f1(x395,f1(x391,x392)),x393)))),
% 113.70/113.80 inference(scs_inference,[],[34,35,8,2,3])).
% 113.70/113.80 cnf(41,plain,
% 113.70/113.80 (E(f1(x411,f1(f1(x412,f1(x413,x414)),x415)),f1(x413,f1(x414,f1(f1(x415,x411),x412))))),
% 113.70/113.80 inference(scs_inference,[],[39,2])).
% 113.70/113.80 cnf(42,plain,
% 113.70/113.80 (E(f1(x421,f1(f1(x422,f1(x423,x424)),x425)),f1(f1(x424,f1(f1(x425,x421),x422)),x423))),
% 113.70/113.80 inference(scs_inference,[],[38,12,39,2,3])).
% 113.70/113.80 cnf(44,plain,
% 113.70/113.80 (E(f1(f1(x441,f1(f1(x442,x443),x444)),x445),f1(x443,f1(f1(x444,f1(x445,x441)),x442)))),
% 113.70/113.80 inference(scs_inference,[],[42,2])).
% 113.70/113.80 cnf(45,plain,
% 113.70/113.80 (E(f1(x451,f1(f1(x452,f1(x453,x454)),x455)),f1(f1(x453,x454),f1(f1(x455,x451),x452)))),
% 113.70/113.80 inference(scs_inference,[],[41,12,42,2,3])).
% 113.70/113.80 cnf(47,plain,
% 113.70/113.80 (E(f1(f1(x471,x472),f1(f1(x473,x474),x475)),f1(x474,f1(f1(x475,f1(x471,x472)),x473)))),
% 113.70/113.80 inference(scs_inference,[],[45,2])).
% 113.70/113.80 cnf(48,plain,
% 113.70/113.80 (E(f1(f1(x481,f1(f1(x482,x483),x484)),x485),f1(x484,f1(f1(x485,x481),f1(x482,x483))))),
% 113.70/113.80 inference(scs_inference,[],[44,30,45,2,3])).
% 113.70/113.80 cnf(50,plain,
% 113.70/113.80 (E(f1(x501,f1(f1(x502,x503),f1(x504,x505))),f1(f1(x503,f1(f1(x504,x505),x501)),x502))),
% 113.70/113.80 inference(scs_inference,[],[48,2])).
% 113.70/113.80 cnf(51,plain,
% 113.70/113.80 (E(f1(f1(x511,x512),f1(f1(x513,x514),x515)),f1(f1(x514,f1(x515,f1(x511,x512))),x513))),
% 113.70/113.80 inference(scs_inference,[],[47,12,48,2,3])).
% 113.70/113.80 cnf(53,plain,
% 113.70/113.80 (E(f1(f1(x531,f1(x532,f1(x533,x534))),x535),f1(f1(x533,x534),f1(f1(x535,x531),x532)))),
% 113.70/113.80 inference(scs_inference,[],[51,2])).
% 113.70/113.80 cnf(54,plain,
% 113.70/113.80 (E(f1(f1(x541,f1(x542,f1(x543,x544))),x545),f1(f1(x544,f1(f1(x545,x541),x542)),x543))),
% 113.70/113.80 inference(scs_inference,[],[50,26,51,2,3])).
% 113.70/113.80 cnf(58,plain,
% 113.70/113.80 (E(f1(f1(x581,f1(x582,f1(x583,x584))),x585),f1(x584,f1(f1(f1(x585,x581),x582),x583)))),
% 113.70/113.80 inference(scs_inference,[],[53,22,54,2,3])).
% 113.70/113.80 cnf(60,plain,
% 113.70/113.80 (E(f1(x601,f1(f1(f1(x602,x603),x604),x605)),f1(f1(x603,f1(x604,f1(x605,x601))),x602))),
% 113.70/113.80 inference(scs_inference,[],[58,2])).
% 113.70/113.80 cnf(71,plain,
% 113.70/113.80 (E(x711,f5(f1(f5(f1(x711,x712)),f5(f1(x711,f5(x712))))))),
% 113.70/113.80 inference(scs_inference,[],[10,2])).
% 113.77/113.80 cnf(90,plain,
% 113.77/113.80 (E(f1(f1(x901,f1(x902,f1(x903,x904))),x905),f1(f1(f1(f1(x905,x901),x902),x903),x904))),
% 113.77/113.80 inference(scs_inference,[],[7,60,3,2])).
% 113.77/113.80 cnf(94,plain,
% 113.77/113.80 (E(f1(f1(f1(f1(x941,x942),x943),x944),x945),f1(x941,f1(x942,f1(x943,f1(x944,x945)))))),
% 113.77/113.80 inference(scs_inference,[],[7,90,3,2])).
% 113.77/113.80 cnf(98,plain,
% 113.77/113.80 (E(f1(x981,f1(x982,f1(x983,f1(x984,x985)))),f1(x985,f1(f1(f1(x981,x982),x983),x984)))),
% 113.77/113.80 inference(scs_inference,[],[7,94,3,2])).
% 113.77/113.80 cnf(102,plain,
% 113.77/113.80 (E(f1(x1021,f1(x1022,f1(x1023,x1024))),f1(f1(f1(x1021,x1022),x1023),x1024))),
% 113.77/113.80 inference(scs_inference,[],[7,30,3,2])).
% 113.77/113.80 cnf(106,plain,
% 113.77/113.80 (E(f1(f1(f1(x1061,x1062),x1063),x1064),f1(f1(x1062,f1(x1063,x1064)),x1061))),
% 113.77/113.80 inference(scs_inference,[],[7,102,3,2])).
% 113.77/113.80 cnf(107,plain,
% 113.77/113.80 (E(f1(x1071,f1(f1(x1072,x1073),x1074)),f1(f1(x1073,f1(x1074,x1071)),x1072))),
% 113.77/113.80 inference(scs_inference,[],[7,106,3])).
% 113.77/113.80 cnf(114,plain,
% 113.77/113.80 (E(f1(f1(x1141,x1142),x1143),f1(f1(x1143,x1141),x1142))),
% 113.77/113.80 inference(scs_inference,[],[7,12,3])).
% 113.77/113.80 cnf(118,plain,
% 113.77/113.80 (E(f1(f1(x1181,f1(x1182,x1183)),x1184),f1(f1(x1183,f1(x1184,x1181)),x1182))),
% 113.77/113.80 inference(scs_inference,[],[7,23,3])).
% 113.77/113.80 cnf(136,plain,
% 113.77/113.80 (E(f1(x1361,f1(f1(x1362,x1363),x1364)),f1(f1(f1(x1364,x1361),x1362),x1363))),
% 113.77/113.80 inference(scs_inference,[],[8,22,3,2])).
% 113.77/113.80 cnf(224,plain,
% 113.77/113.80 (~E(f5(f1(f5(f1(a2,x2241)),f5(f1(a2,f5(x2241))))),a3)),
% 113.77/113.80 inference(scs_inference,[],[11,114,71,6,4,5,2,3])).
% 113.77/113.80 cnf(229,plain,
% 113.77/113.80 (~E(f5(f1(f5(f1(a3,x2291)),f5(f1(a3,f5(x2291))))),a2)),
% 113.77/113.80 inference(scs_inference,[],[107,17,6,5,4,2])).
% 113.77/113.80 cnf(236,plain,
% 113.77/113.80 (~E(f5(f1(f5(f1(a2,x2361)),f5(f1(a2,f5(x2361))))),f5(f1(f5(f1(a3,x2362)),f5(f1(a3,f5(x2362))))))),
% 113.77/113.80 inference(scs_inference,[],[118,224,71,17,6,4,5,2,3])).
% 113.77/113.80 cnf(241,plain,
% 113.77/113.80 (~E(f5(f1(f5(f1(a3,x2411)),f5(f1(a3,f5(x2411))))),f5(f1(f5(f1(a2,x2412)),f5(f1(a2,f5(x2412))))))),
% 113.77/113.80 inference(scs_inference,[],[136,236,6,5,4,2])).
% 113.77/113.80 cnf(523,plain,
% 113.77/113.80 (E(f1(f5(f1(a2,f5(f1(a3,a4)))),x5231),f1(f5(f1(a3,f5(f1(a2,a4)))),x5231))),
% 113.77/113.80 inference(scs_inference,[],[9,6,4])).
% 113.77/113.80 cnf(632,plain,
% 113.77/113.80 (E(f1(x6321,f1(x6322,x6323)),f1(x6321,f1(x6323,x6322)))),
% 113.77/113.80 inference(scs_inference,[],[7,5])).
% 113.77/113.80 cnf(633,plain,
% 113.77/113.80 (E(f5(f1(x6331,x6332)),f5(f1(x6332,x6331)))),
% 113.77/113.80 inference(scs_inference,[],[7,5,6])).
% 113.77/113.80 cnf(634,plain,
% 113.77/113.80 (E(f1(f1(x6341,x6342),x6343),f1(f1(x6342,x6341),x6343))),
% 113.77/113.80 inference(scs_inference,[],[7,5,6,4])).
% 113.77/113.80 cnf(635,plain,
% 113.77/113.80 (E(f1(x6351,f1(x6352,f1(x6353,x6354))),f1(x6351,f1(x6352,f1(x6354,x6353))))),
% 113.77/113.80 inference(scs_inference,[],[632,5])).
% 113.77/113.80 cnf(636,plain,
% 113.77/113.80 (E(f5(f1(x6361,f1(x6362,x6363))),f5(f1(x6361,f1(x6363,x6362))))),
% 113.77/113.80 inference(scs_inference,[],[632,5,6])).
% 113.77/113.80 cnf(640,plain,
% 113.77/113.80 (~E(f5(f1(f5(f1(a2,x6401)),f5(f1(a2,f5(x6401))))),f5(f1(f5(f1(a3,f5(x6402))),f5(f1(a3,x6402)))))),
% 113.77/113.80 inference(scs_inference,[],[632,633,241,5,6,4,3,2])).
% 113.77/113.80 cnf(642,plain,
% 113.77/113.80 (E(f5(f1(f1(x6421,x6422),x6423)),f5(f1(f1(x6422,x6421),x6423)))),
% 113.77/113.80 inference(scs_inference,[],[634,5,6])).
% 113.77/113.80 cnf(650,plain,
% 113.77/113.80 (~E(f5(f1(f5(f1(a2,f5(x6501))),f5(f1(a2,x6501)))),f5(f1(f5(f1(a3,f5(x6502))),f5(f1(a3,x6502)))))),
% 113.77/113.80 inference(scs_inference,[],[635,640,633,5,6,4,3])).
% 113.77/113.80 cnf(655,plain,
% 113.77/113.80 (E(f1(f5(f1(x6551,f1(x6552,x6553))),x6554),f1(f5(f1(x6551,f1(x6553,x6552))),x6554))),
% 113.77/113.80 inference(scs_inference,[],[636,5,6,4])).
% 113.77/113.80 cnf(671,plain,
% 113.77/113.80 (E(f1(x6711,f5(f1(f1(x6712,x6713),x6714))),f1(x6711,f5(f1(f1(x6713,x6712),x6714))))),
% 113.77/113.80 inference(scs_inference,[],[642,5])).
% 113.77/113.80 cnf(693,plain,
% 113.77/113.80 (E(f1(f1(f1(x6931,x6932),x6933),x6934),f1(f1(x6931,f1(x6932,x6933)),x6934))),
% 113.77/113.80 inference(scs_inference,[],[8,4])).
% 113.77/113.80 cnf(694,plain,
% 113.77/113.80 (E(f1(x6941,f1(f1(x6942,x6943),x6944)),f1(x6941,f1(x6942,f1(x6943,x6944))))),
% 113.77/113.80 inference(scs_inference,[],[8,4,5])).
% 113.77/113.80 cnf(696,plain,
% 113.77/113.80 (E(f1(f1(f1(f1(x6961,x6962),x6963),x6964),x6965),f1(f1(f1(x6961,f1(x6962,x6963)),x6964),x6965))),
% 113.77/113.80 inference(scs_inference,[],[693,4])).
% 113.77/113.80 cnf(699,plain,
% 113.77/113.80 (E(f1(f1(x6991,f1(f1(x6992,x6993),x6994)),x6995),f1(f1(x6991,f1(x6992,f1(x6993,x6994))),x6995))),
% 113.77/113.80 inference(scs_inference,[],[694,4])).
% 113.77/113.80 cnf(720,plain,
% 113.77/113.80 (E(f5(f1(f5(f1(x7201,f1(x7202,x7203))),x7204)),f5(f1(f5(f1(x7201,f1(x7203,x7202))),x7204)))),
% 113.77/113.80 inference(scs_inference,[],[655,4,5,6])).
% 113.77/113.80 cnf(750,plain,
% 113.77/113.80 (~E(f1(f5(f1(a2,f5(x7501))),f5(f1(a2,x7501))),f1(f5(f1(a3,f5(x7502))),f5(f1(a3,x7502))))),
% 113.77/113.80 inference(scs_inference,[],[650,6])).
% 113.77/113.80 cnf(752,plain,
% 113.77/113.80 (~E(f5(f1(f5(f1(a3,f1(x7521,x7522))),f5(f1(a3,f5(f1(x7522,x7521)))))),a2)),
% 113.77/113.80 inference(scs_inference,[],[650,720,229,6,2,3])).
% 113.77/113.80 cnf(757,plain,
% 113.77/113.80 (E(f1(f1(f1(f1(x7571,x7572),x7573),x7574),f5(f1(f1(x7575,x7576),x7577))),f1(f1(f1(x7571,f1(x7572,x7573)),x7574),f5(f1(f1(x7576,x7575),x7577))))),
% 113.77/113.80 inference(scs_inference,[],[671,696,752,6,2,3])).
% 113.77/113.80 cnf(791,plain,
% 113.77/113.80 (E(f1(f1(x7911,f1(f1(x7912,x7913),x7914)),f1(x7915,x7916)),f1(x7916,f1(f1(x7911,f1(x7912,f1(x7913,x7914))),x7915)))),
% 113.77/113.80 inference(scs_inference,[],[16,699,3])).
% 113.77/113.80 cnf(808,plain,
% 113.77/113.80 (E(f1(f1(x8081,f1(x8082,x8083)),x8084),f1(f1(f1(x8083,x8081),x8082),x8084))),
% 113.77/113.80 inference(scs_inference,[],[20,5,4])).
% 113.77/113.80 cnf(812,plain,
% 113.77/113.80 (E(f5(f1(x8121,f1(x8122,x8123))),f5(f1(f1(x8123,x8121),x8122)))),
% 113.77/113.80 inference(scs_inference,[],[20,6])).
% 113.77/113.80 cnf(815,plain,
% 113.77/113.80 (E(f1(f1(x8151,f1(x8152,f1(x8153,x8154))),x8155),f1(f1(f1(x8154,x8152),x8153),f1(x8155,x8151)))),
% 113.77/113.80 inference(scs_inference,[],[22,808,3])).
% 113.77/113.80 cnf(831,plain,
% 113.77/113.80 (E(f1(x8311,f5(f1(x8312,f1(x8313,x8314)))),f1(x8311,f5(f1(f1(x8314,x8312),x8313))))),
% 113.77/113.80 inference(scs_inference,[],[812,5])).
% 113.77/113.80 cnf(833,plain,
% 113.77/113.80 (~E(f1(f5(f1(a2,f5(f1(x8331,x8332)))),f5(f1(f1(x8332,a2),x8331))),f1(f5(f1(a3,f5(x8333))),f5(f1(a3,x8333))))),
% 113.77/113.80 inference(scs_inference,[],[750,831,3])).
% 113.77/113.80 cnf(890,plain,
% 113.77/113.80 (E(f1(f1(x8901,f1(f1(x8902,x8903),x8904)),f1(x8905,x8906)),f1(x8902,f1(f1(x8903,x8904),f1(f1(x8905,x8906),x8901))))),
% 113.77/113.80 inference(scs_inference,[],[41,791,3])).
% 113.77/113.80 cnf(896,plain,
% 113.77/113.80 (E(f1(x8961,f1(f1(x8962,f1(f1(x8963,x8964),x8965)),x8966)),f1(x8966,f1(f1(x8961,x8962),f1(f1(x8963,x8964),x8965))))),
% 113.77/113.80 inference(scs_inference,[],[42,890,3])).
% 113.77/113.80 cnf(1093,plain,
% 113.77/113.80 (E(f1(f1(f1(x10931,f1(x10932,f1(x10933,x10934))),x10935),x10936),f1(f1(f1(f1(x10934,x10932),x10933),f1(x10935,x10931)),x10936))),
% 113.77/113.80 inference(scs_inference,[],[98,896,815,6,3,4])).
% 113.77/113.80 cnf(1109,plain,
% 113.77/113.80 (E(f1(f1(f1(f1(x11091,x11092),f1(x11093,x11094)),x11095),f5(f1(f1(x11096,x11097),x11098))),f1(f1(f1(f1(x11094,x11092),x11093),f1(x11095,x11091)),f5(f1(f1(x11097,x11096),x11098))))),
% 113.77/113.80 inference(scs_inference,[],[1093,757,3])).
% 113.77/113.80 cnf(1254,plain,
% 113.77/113.80 (E(f1(f1(f1(x12541,x12542),x12543),x12544),f1(f1(x12542,f1(x12543,x12544)),x12541))),
% 113.77/113.80 inference(rename_variables,[],[106])).
% 113.77/113.80 cnf(1255,plain,
% 113.77/113.80 (E(f1(f1(f1(f1(x12551,x12552),x12553),x12554),x12555),f1(f1(f1(x12552,f1(x12553,x12554)),x12551),x12555))),
% 113.77/113.80 inference(scs_inference,[],[106,1254,1109,3,4])).
% 113.77/113.80 cnf(1261,plain,
% 113.77/113.80 (E(f1(f1(f1(x12611,x12612),x12613),x12614),f1(f1(x12612,f1(x12613,x12614)),x12611))),
% 113.77/113.80 inference(rename_variables,[],[106])).
% 113.77/113.80 cnf(1264,plain,
% 113.77/113.80 (E(f5(f1(f1(f1(x12641,x12642),x12643),x12644)),f5(f1(f1(x12642,f1(x12643,x12644)),x12641)))),
% 113.77/113.80 inference(scs_inference,[],[106,1261,1255,3,5,6])).
% 113.77/113.80 cnf(1265,plain,
% 113.77/113.80 (~E(f1(f5(f1(a3,f5(f1(a2,a4)))),f5(f1(f1(a4,a2),a3))),f1(f5(f1(a3,f5(x12651))),f5(f1(a3,x12651))))),
% 113.77/113.80 inference(scs_inference,[],[833,523,3])).
% 113.77/113.80 cnf(1270,plain,
% 113.77/113.80 (~E(f1(f1(a4,a2),a3),f1(a3,f1(a2,a4)))),
% 113.77/113.80 inference(scs_inference,[],[1265,5,6])).
% 113.77/113.80 cnf(1278,plain,
% 113.77/113.80 (~E(f1(a3,f1(a2,a4)),f1(f1(a4,a2),a3))),
% 113.77/113.80 inference(scs_inference,[],[1270,1264,5,6,2])).
% 113.77/113.80 cnf(2221,plain,
% 113.77/113.80 ($false),
% 113.77/113.80 inference(scs_inference,[],[1278,632,7,3]),
% 113.77/113.80 ['proof']).
% 113.77/113.80 % SZS output end Proof
% 113.77/113.80 % Total time :113.040000s
%------------------------------------------------------------------------------