%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : ROB021-1 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n004.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:26 EDT 2024
% Result : Unsatisfiable 58.59s 59.11s
% Output : CNFRefutation 58.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.10 % Problem : ROB021-1 : TPTP v8.2.0. Released v1.0.0.
% 0.09/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.10/0.31 % Computer : n004.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Wed Jun 19 18:37:38 EDT 2024
% 0.10/0.31 % CPUTime :
% 0.49/0.55 start to proof:theBenchmark
% 58.57/59.11 %-------------------------------------------
% 58.57/59.11 % File :CSE---1.7
% 58.57/59.11 % Problem :theBenchmark
% 58.57/59.11 % Transform :cnf
% 58.57/59.11 % Format :tptp:raw
% 58.57/59.11 % Command :java -jar mcs_scs.jar %d %s
% 58.57/59.11
% 58.57/59.11 % Result :Theorem 58.060000s
% 58.57/59.11 % Output :CNFRefutation 58.060000s
% 58.57/59.11 %-------------------------------------------
% 58.59/59.11 %--------------------------------------------------------------------------
% 58.59/59.11 % File : ROB021-1 : TPTP v8.2.0. Released v1.0.0.
% 58.59/59.11 % Domain : Robbins Algebra
% 58.59/59.11 % Problem : (-X = -Y)=>(X = Y) => Boolean
% 58.59/59.11 % Version : [Win90] (equality) axioms.
% 58.59/59.11 % English : If (-X = -Y) => (X = Y) then the algebra is Boolean.
% 58.59/59.11
% 58.59/59.11 % Refs : [HMT71] Henkin et al. (1971), Cylindrical Algebras
% 58.59/59.11 % : [Win90] Winker (1990), Robbins Algebra: Conditions that make a
% 58.59/59.11 % : [McC92] McCune (1992), Email to G. Sutcliffe
% 58.59/59.11 % Source : [McC92]
% 58.59/59.11 % Names : - [McC92]
% 58.59/59.11
% 58.59/59.11 % Status : Unsatisfiable
% 58.59/59.11 % Rating : 0.00 v6.3.0, 0.10 v6.2.0, 0.30 v6.1.0, 0.18 v6.0.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.12 v5.1.0, 0.22 v5.0.0, 0.10 v4.1.0, 0.11 v4.0.1, 0.12 v4.0.0, 0.14 v3.7.0, 0.00 v2.2.1, 0.17 v2.2.0, 0.00 v2.0.0
% 58.59/59.11 % Syntax : Number of clauses : 5 ( 4 unt; 0 nHn; 2 RR)
% 58.59/59.11 % Number of literals : 6 ( 6 equ; 2 neg)
% 58.59/59.11 % Maximal clause size : 2 ( 1 avg)
% 58.59/59.11 % Maximal term depth : 6 ( 2 avg)
% 58.59/59.11 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 58.59/59.11 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 58.59/59.11 % Number of variables : 9 ( 0 sgn)
% 58.59/59.11 % SPC : CNF_UNS_RFO_PEQ_NUE
% 58.59/59.11
% 58.59/59.11 % Comments : Commutativity, associativity, and Huntington's axiom
% 58.59/59.11 % axiomatize Boolean algebra.
% 58.59/59.11 %--------------------------------------------------------------------------
% 58.59/59.11 %----Include axioms for Robbins algebra
% 58.59/59.11 include('Axioms/ROB001-0.ax').
% 58.59/59.11 %--------------------------------------------------------------------------
% 58.59/59.11 cnf(negative_equality_implies_positive_equality,hypothesis,
% 58.59/59.11 ( negate(X) != negate(Y)
% 58.59/59.11 | X = Y ) ).
% 58.59/59.11
% 58.59/59.11 cnf(prove_huntingtons_axiom,negated_conjecture,
% 58.59/59.11 add(negate(add(a,negate(b))),negate(add(negate(a),negate(b)))) != b ).
% 58.59/59.11
% 58.59/59.11 %--------------------------------------------------------------------------
% 58.59/59.11 %-------------------------------------------
% 58.59/59.11 % Proof found
% 58.59/59.11 % SZS status Theorem for theBenchmark
% 58.59/59.11 % SZS output start Proof
% 58.59/59.12 %ClaNum:11(EqnAxiom:6)
% 58.59/59.12 %VarNum:19(SingletonVarNum:9)
% 58.59/59.12 %MaxLitNum:2
% 58.59/59.12 %MaxfuncDepth:5
% 58.59/59.12 %SharedTerms:10
% 58.59/59.12 %goalClause: 10
% 58.59/59.12 %singleGoalClaCount:1
% 58.59/59.12 [10]~E(f1(f3(f1(a2,f3(a4))),f3(f1(f3(a2),f3(a4)))),a4)
% 58.59/59.12 [7]E(f1(x71,x72),f1(x72,x71))
% 58.59/59.12 [9]E(f3(f1(f3(f1(x91,x92)),f3(f1(x91,f3(x92))))),x91)
% 58.59/59.12 [8]E(f1(f1(x81,x82),x83),f1(x81,f1(x82,x83)))
% 58.59/59.12 [11]E(x111,x112)+~E(f3(x111),f3(x112))
% 58.59/59.12 %EqnAxiom
% 58.59/59.12 [1]E(x11,x11)
% 58.59/59.12 [2]E(x22,x21)+~E(x21,x22)
% 58.59/59.12 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.59/59.12 [4]~E(x41,x42)+E(f1(x41,x43),f1(x42,x43))
% 58.59/59.12 [5]~E(x51,x52)+E(f1(x53,x51),f1(x53,x52))
% 58.59/59.12 [6]~E(x61,x62)+E(f3(x61),f3(x62))
% 58.59/59.12
% 58.59/59.12 %-------------------------------------------
% 58.59/59.12 cnf(13,plain,
% 58.59/59.12 (E(f1(f3(f1(f3(x131),x132)),f3(f1(f3(x131),f3(x132)))),x131)),
% 58.59/59.12 inference(scs_inference,[],[9,11])).
% 58.59/59.12 cnf(16,plain,
% 58.59/59.12 (E(f1(x161,f1(x162,x163)),f1(f1(x161,x162),x163))),
% 58.59/59.12 inference(scs_inference,[],[8,9,11,2])).
% 58.59/59.12 cnf(17,plain,
% 58.59/59.12 (E(f1(x171,f1(x172,x173)),f1(x172,f1(x173,x171)))),
% 58.59/59.12 inference(scs_inference,[],[7,8,9,11,2,3])).
% 58.59/59.12 cnf(20,plain,
% 58.59/59.12 (E(x201,f1(f3(f1(f3(x201),x202)),f3(f1(f3(x201),f3(x202)))))),
% 58.59/59.12 inference(scs_inference,[],[13,2])).
% 58.59/59.12 cnf(21,plain,
% 58.59/59.12 (E(f1(x211,f1(x212,x213)),f1(x213,f1(x211,x212)))),
% 58.59/59.12 inference(scs_inference,[],[17,2])).
% 58.59/59.12 cnf(23,plain,
% 58.59/59.12 (E(f3(f1(x231,x232)),f3(f1(x232,x231)))),
% 58.59/59.12 inference(scs_inference,[],[7,6,2])).
% 58.59/59.12 cnf(24,plain,
% 58.59/59.12 (E(f1(f1(x241,x242),x243),f1(f1(x243,x241),x242))),
% 58.59/59.12 inference(scs_inference,[],[7,16,3])).
% 58.59/59.12 cnf(29,plain,
% 58.59/59.12 (~E(f3(a4),f3(f1(f3(f1(a2,f3(a4))),f3(f1(f3(a2),f3(a4))))))),
% 58.59/59.12 inference(scs_inference,[],[10,2,11])).
% 58.59/59.12 cnf(32,plain,
% 58.59/59.12 (E(f3(f1(f1(x321,x322),x323)),f3(f1(x321,f1(x322,x323))))),
% 58.59/59.12 inference(scs_inference,[],[16,2,6])).
% 58.59/59.12 cnf(33,plain,
% 58.59/59.12 (E(f3(f1(x331,f1(x332,x333))),f3(f1(f1(x331,x332),x333)))),
% 58.59/59.12 inference(scs_inference,[],[32,2])).
% 58.59/59.12 cnf(34,plain,
% 58.59/59.12 (E(f1(f1(f1(x341,x342),x343),x344),f1(f1(x341,f1(x342,x343)),x344))),
% 58.59/59.12 inference(scs_inference,[],[16,2,4])).
% 58.59/59.12 cnf(35,plain,
% 58.59/59.12 (E(f1(f1(x351,f1(x352,x353)),x354),f1(f1(f1(x351,x352),x353),x354))),
% 58.59/59.12 inference(scs_inference,[],[34,2])).
% 58.59/59.12 cnf(36,plain,
% 58.59/59.12 (E(f1(f1(x361,x362),f1(x363,x364)),f1(f1(x361,f1(x362,x363)),x364))),
% 58.59/59.12 inference(scs_inference,[],[16,34,2,3])).
% 58.59/59.12 cnf(40,plain,
% 58.59/59.12 (E(f1(f1(x401,f1(x402,x403)),x404),f1(f1(x401,x402),f1(x403,x404)))),
% 58.59/59.12 inference(scs_inference,[],[36,2])).
% 58.59/59.12 cnf(41,plain,
% 58.59/59.12 (E(f1(x411,f1(f1(x412,x413),x414)),f1(f1(f1(x411,x412),x413),x414))),
% 58.59/59.12 inference(scs_inference,[],[16,35,36,2,3])).
% 58.59/59.12 cnf(45,plain,
% 58.59/59.12 (E(f1(x451,f1(f1(x452,x453),x454)),f1(f1(x451,x452),f1(x453,x454)))),
% 58.59/59.12 inference(scs_inference,[],[16,40,41,2,3])).
% 58.59/59.12 cnf(49,plain,
% 58.59/59.12 (E(f1(f1(x491,x492),f1(x493,x494)),f1(x491,f1(f1(x492,x493),x494)))),
% 58.59/59.12 inference(scs_inference,[],[45,2])).
% 58.59/59.12 cnf(50,plain,
% 58.59/59.12 (E(f1(x501,f1(x502,f1(f1(x503,x504),x505))),f1(f1(f1(x501,x502),x503),f1(x504,x505)))),
% 58.59/59.12 inference(scs_inference,[],[16,45,2,3])).
% 58.59/59.12 cnf(53,plain,
% 58.59/59.12 (E(f3(f1(x531,f1(x532,f1(x533,x534)))),f3(f1(x531,f1(f1(x532,x533),x534))))),
% 58.59/59.12 inference(scs_inference,[],[16,6,5])).
% 58.59/59.12 cnf(54,plain,
% 58.59/59.12 (E(f1(x541,f1(x542,f1(x543,x544))),f1(x541,f1(f1(x542,x543),x544)))),
% 58.59/59.12 inference(scs_inference,[],[53,11])).
% 58.59/59.12 cnf(56,plain,
% 58.59/59.12 (E(f1(f1(f1(x561,x562),x563),f1(x564,x565)),f1(x561,f1(x562,f1(f1(x563,x564),x565))))),
% 58.59/59.12 inference(scs_inference,[],[50,53,11,2])).
% 58.59/59.12 cnf(57,plain,
% 58.59/59.12 (E(f1(x571,f1(x572,f1(x573,x574))),f1(f1(x571,f1(x572,x573)),x574))),
% 58.59/59.12 inference(scs_inference,[],[16,50,36,53,11,2,3])).
% 58.59/59.12 cnf(62,plain,
% 58.59/59.12 (E(f1(x621,f1(x622,f1(x623,f1(x624,x625)))),f1(f1(x621,x622),f1(f1(x623,x624),x625)))),
% 58.59/59.12 inference(scs_inference,[],[16,54,57,2,3])).
% 58.59/59.12 cnf(65,plain,
% 58.59/59.12 (E(f3(f1(f1(x651,f1(x652,x653)),x654)),f3(f1(f1(f1(x651,x652),x653),x654)))),
% 58.59/59.12 inference(scs_inference,[],[16,6,4])).
% 58.59/59.12 cnf(66,plain,
% 58.59/59.12 (E(f1(f1(x661,x662),f1(f1(x663,x664),x665)),f1(x661,f1(x662,f1(x663,f1(x664,x665)))))),
% 58.59/59.12 inference(scs_inference,[],[62,2])).
% 58.59/59.12 cnf(67,plain,
% 58.59/59.12 (E(f1(f1(x671,x672),f1(x673,f1(x674,x675))),f1(x671,f1(x672,f1(f1(x673,x674),x675))))),
% 58.59/59.12 inference(scs_inference,[],[16,62,56,2,3])).
% 58.59/59.12 cnf(70,plain,
% 58.59/59.12 (E(f3(f1(x701,f1(x702,f1(x703,x704)))),f3(f1(f1(f1(x701,x702),x703),x704)))),
% 58.59/59.12 inference(scs_inference,[],[16,33,6,3])).
% 58.59/59.12 cnf(71,plain,
% 58.59/59.12 (E(f1(x711,f1(x712,f1(x713,x714))),f1(f1(f1(x711,x712),x713),x714))),
% 58.59/59.12 inference(scs_inference,[],[70,11])).
% 58.59/59.12 cnf(74,plain,
% 58.59/59.12 (E(f1(x741,f1(x742,f1(f1(x743,x744),x745))),f1(x741,f1(x742,f1(x743,f1(x744,x745)))))),
% 58.59/59.12 inference(scs_inference,[],[16,66,67,70,11,2,3])).
% 58.59/59.12 cnf(79,plain,
% 58.59/59.12 (E(f1(x791,f1(x792,f1(x793,f1(x794,x795)))),f1(f1(f1(f1(x791,x792),x793),x794),x795))),
% 58.59/59.12 inference(scs_inference,[],[16,71,2,3])).
% 58.59/59.12 cnf(84,plain,
% 58.59/59.12 (E(f1(x841,f1(x842,f1(f1(x843,x844),x845))),f1(f1(f1(f1(x841,x842),x843),x844),x845))),
% 58.59/59.12 inference(scs_inference,[],[16,74,41,2,3])).
% 58.59/59.12 cnf(87,plain,
% 58.59/59.12 (E(f3(f1(x871,f1(x872,f1(x873,x874)))),f3(f1(f1(x871,f1(x872,x873)),x874)))),
% 58.59/59.12 inference(scs_inference,[],[16,54,6,3])).
% 58.59/59.12 cnf(89,plain,
% 58.59/59.12 (E(f1(x891,f1(x892,f1(x893,f1(x894,x895)))),f1(f1(f1(x891,x892),f1(x893,x894)),x895))),
% 58.59/59.12 inference(scs_inference,[],[16,79,57,2,3])).
% 58.59/59.12 cnf(102,plain,
% 58.59/59.12 (E(f3(f1(f1(f1(x1021,x1022),x1023),x1024)),f3(f1(x1021,f1(x1022,f1(x1023,x1024)))))),
% 58.59/59.12 inference(scs_inference,[],[70,2])).
% 58.59/59.12 cnf(105,plain,
% 58.59/59.12 (E(f1(f1(f1(f1(x1051,x1052),x1053),x1054),x1055),f1(f1(x1051,f1(x1052,f1(x1053,x1054))),x1055))),
% 58.59/59.12 inference(scs_inference,[],[102,4,11])).
% 58.59/59.12 cnf(106,plain,
% 58.59/59.12 (E(f3(f1(f1(f1(x1061,x1062),x1063),x1064)),f3(f1(f1(x1061,f1(x1062,x1063)),x1064)))),
% 58.59/59.12 inference(scs_inference,[],[65,2])).
% 58.59/59.12 cnf(107,plain,
% 58.59/59.12 (E(f1(f1(f1(x1071,x1072),x1073),f1(x1074,x1075)),f1(f1(x1071,f1(x1072,f1(x1073,x1074))),x1075))),
% 58.59/59.12 inference(scs_inference,[],[16,65,105,2,3])).
% 58.59/59.12 cnf(111,plain,
% 58.59/59.13 (E(f1(f1(x1111,f1(x1112,f1(x1113,x1114))),x1115),f1(f1(f1(x1111,x1112),x1113),f1(x1114,x1115)))),
% 58.59/59.13 inference(scs_inference,[],[107,2])).
% 58.59/59.13 cnf(112,plain,
% 58.59/59.13 (E(f1(f1(x1121,x1122),f1(x1123,f1(x1124,x1125))),f1(f1(x1121,f1(x1122,f1(x1123,x1124))),x1125))),
% 58.59/59.13 inference(scs_inference,[],[16,107,2,3])).
% 58.59/59.13 cnf(115,plain,
% 58.59/59.13 (E(f1(f1(x1151,f1(x1152,f1(x1153,x1154))),x1155),f1(f1(x1151,f1(f1(x1152,x1153),x1154)),x1155))),
% 58.59/59.13 inference(scs_inference,[],[16,4,5])).
% 58.59/59.13 cnf(116,plain,
% 58.59/59.13 (E(f1(f1(x1161,f1(x1162,f1(x1163,x1164))),x1165),f1(f1(x1161,x1162),f1(x1163,f1(x1164,x1165))))),
% 58.59/59.13 inference(scs_inference,[],[112,2])).
% 58.59/59.13 cnf(117,plain,
% 58.59/59.13 (E(f1(x1171,f1(f1(x1172,f1(x1173,x1174)),x1175)),f1(f1(f1(x1171,x1172),x1173),f1(x1174,x1175)))),
% 58.59/59.13 inference(scs_inference,[],[16,111,112,2,3])).
% 58.59/59.13 cnf(120,plain,
% 58.59/59.13 (E(f1(f1(x1201,f1(x1202,x1203)),f1(x1204,f1(x1205,x1206))),f1(f1(f1(x1201,x1202),x1203),f1(f1(x1204,x1205),x1206)))),
% 58.59/59.13 inference(scs_inference,[],[16,54,4,3])).
% 58.59/59.13 cnf(122,plain,
% 58.59/59.13 (E(f1(x1221,f1(f1(x1222,f1(x1223,x1224)),x1225)),f1(f1(x1221,x1222),f1(x1223,f1(x1224,x1225))))),
% 58.59/59.13 inference(scs_inference,[],[16,117,116,2,3])).
% 58.59/59.13 cnf(125,plain,
% 58.59/59.13 (E(f1(f1(f1(f1(x1251,x1252),x1253),x1254),x1255),f1(f1(f1(x1251,f1(x1252,x1253)),x1254),x1255))),
% 58.59/59.13 inference(scs_inference,[],[106,4,11])).
% 58.59/59.13 cnf(127,plain,
% 58.59/59.13 (E(f1(x1271,f1(f1(x1272,x1273),f1(x1274,f1(x1275,x1276)))),f1(f1(f1(x1271,x1272),x1273),f1(f1(x1274,x1275),x1276)))),
% 58.59/59.13 inference(scs_inference,[],[16,120,2,3])).
% 58.59/59.13 cnf(131,plain,
% 58.59/59.13 (E(f1(f1(x1311,x1312),f1(x1313,f1(x1314,x1315))),f1(x1311,f1(f1(x1312,f1(x1313,x1314)),x1315)))),
% 58.59/59.13 inference(scs_inference,[],[122,2])).
% 58.59/59.13 cnf(137,plain,
% 58.59/59.13 (E(f1(x1371,f1(x1372,f1(x1373,f1(x1374,x1375)))),f1(x1371,f1(f1(x1372,f1(x1373,x1374)),x1375)))),
% 58.59/59.13 inference(scs_inference,[],[16,127,131,2,3])).
% 58.59/59.13 cnf(140,plain,
% 58.59/59.13 (E(f1(f1(x1401,f1(x1402,f1(x1403,x1404))),x1405),f1(f1(f1(x1401,f1(x1402,x1403)),x1404),x1405))),
% 58.59/59.13 inference(scs_inference,[],[16,54,4,3])).
% 58.59/59.13 cnf(150,plain,
% 58.59/59.13 (E(f3(f1(f1(x1501,f1(x1502,x1503)),x1504)),f3(f1(x1501,f1(x1502,f1(x1503,x1504)))))),
% 58.59/59.13 inference(scs_inference,[],[87,2])).
% 58.59/59.13 cnf(151,plain,
% 58.59/59.13 (E(f1(x1511,f1(x1512,f1(x1513,f1(x1514,x1515)))),f1(f1(x1511,f1(x1512,f1(x1513,x1514))),x1515))),
% 58.59/59.13 inference(scs_inference,[],[16,112,87,2,3])).
% 58.59/59.13 cnf(154,plain,
% 58.59/59.13 (E(f1(x1541,f1(x1542,f1(x1543,f1(x1544,x1545)))),f1(x1541,f1(f1(f1(x1542,x1543),x1544),x1545)))),
% 58.59/59.13 inference(scs_inference,[],[16,54,5,3])).
% 58.59/59.13 cnf(156,plain,
% 58.59/59.13 (E(f1(x1561,f1(f1(x1562,f1(x1563,x1564)),x1565)),f1(f1(x1561,f1(f1(x1562,x1563),x1564)),x1565))),
% 58.59/59.13 inference(scs_inference,[],[16,151,115,2,3])).
% 58.59/59.13 cnf(161,plain,
% 58.59/59.13 (E(f1(f1(f1(x1611,x1612),x1613),f1(x1614,x1615)),f1(f1(f1(x1611,f1(x1612,x1613)),x1614),x1615))),
% 58.59/59.13 inference(scs_inference,[],[16,154,125,2,3])).
% 58.59/59.13 cnf(166,plain,
% 58.59/59.13 (E(f1(f1(x1661,x1662),f1(x1663,f1(x1664,x1665))),f1(f1(f1(x1661,f1(x1662,x1663)),x1664),x1665))),
% 58.59/59.13 inference(scs_inference,[],[16,156,161,2,3])).
% 58.59/59.13 cnf(175,plain,
% 58.59/59.13 (E(f1(x1751,f1(f1(x1752,f1(x1753,x1754)),x1755)),f1(f1(f1(x1751,f1(x1752,x1753)),x1754),x1755))),
% 58.59/59.13 inference(scs_inference,[],[16,166,140,2,3])).
% 58.59/59.13 cnf(179,plain,
% 58.59/59.13 (E(f1(f1(x1791,f1(x1792,x1793)),f1(x1794,x1795)),f1(x1791,f1(f1(x1792,f1(x1793,x1794)),x1795)))),
% 58.59/59.13 inference(scs_inference,[],[16,175,2,3])).
% 58.59/59.13 cnf(181,plain,
% 58.59/59.13 (E(f1(x1811,f1(f1(x1812,f1(x1813,x1814)),x1815)),f1(f1(x1811,f1(x1812,x1813)),f1(x1814,x1815)))),
% 58.59/59.13 inference(scs_inference,[],[179,2])).
% 58.59/59.13 cnf(182,plain,
% 58.59/59.13 (E(f1(x1821,f1(f1(x1822,x1823),f1(x1824,x1825))),f1(x1821,f1(f1(x1822,f1(x1823,x1824)),x1825)))),
% 58.59/59.13 inference(scs_inference,[],[16,179,2,3])).
% 58.59/59.13 cnf(186,plain,
% 58.59/59.13 (E(f1(x1861,f1(x1862,f1(f1(x1863,f1(x1864,x1865)),x1866))),f1(f1(f1(x1861,x1862),f1(x1863,x1864)),f1(x1865,x1866)))),
% 58.59/59.13 inference(scs_inference,[],[16,181,182,2,3])).
% 58.59/59.13 cnf(189,plain,
% 58.59/59.13 (E(f1(f1(f1(x1891,f1(x1892,x1893)),x1894),x1895),f1(f1(x1891,f1(x1892,f1(x1893,x1894))),x1895))),
% 58.59/59.13 inference(scs_inference,[],[150,11,4])).
% 58.59/59.13 cnf(191,plain,
% 58.59/59.13 (E(f1(x1911,f1(x1912,f1(f1(x1913,x1914),f1(x1915,x1916)))),f1(f1(x1911,x1912),f1(f1(x1913,f1(x1914,x1915)),x1916)))),
% 58.59/59.13 inference(scs_inference,[],[16,186,182,2,3])).
% 58.59/59.13 cnf(195,plain,
% 58.59/59.13 (E(f1(f1(x1951,f1(x1952,x1953)),f1(x1954,x1955)),f1(f1(x1951,f1(x1952,f1(x1953,x1954))),x1955))),
% 58.59/59.13 inference(scs_inference,[],[16,191,189,2,3])).
% 58.59/59.13 cnf(199,plain,
% 58.59/59.13 (E(f1(x1991,f1(f1(x1992,x1993),f1(x1994,x1995))),f1(f1(x1991,f1(x1992,f1(x1993,x1994))),x1995))),
% 58.59/59.13 inference(scs_inference,[],[16,195,2,3])).
% 58.59/59.13 cnf(203,plain,
% 58.59/59.13 (E(f1(x2031,f1(x2032,f1(f1(x2033,x2034),f1(x2035,x2036)))),f1(f1(f1(x2031,x2032),f1(x2033,f1(x2034,x2035))),x2036))),
% 58.59/59.13 inference(scs_inference,[],[16,199,2,3])).
% 58.59/59.13 cnf(224,plain,
% 58.59/59.13 (E(f1(f1(x2241,f1(x2242,x2243)),f1(x2244,x2245)),f1(f1(f1(f1(x2241,x2242),x2243),x2244),x2245))),
% 58.59/59.13 inference(scs_inference,[],[16,125,2,3])).
% 58.59/59.13 cnf(779,plain,
% 58.59/59.13 (~E(f1(f3(f1(a2,f3(a4))),f3(f1(f3(a2),f3(a4)))),f1(f3(f1(f3(a4),x7791)),f3(f1(f3(a4),f3(x7791)))))),
% 58.59/59.13 inference(scs_inference,[],[20,10,2,3])).
% 58.59/59.13 cnf(901,plain,
% 58.59/59.13 (E(f1(x9011,f1(f1(f1(x9012,f1(x9013,x9014)),x9015),x9016)),f1(f1(f1(x9016,x9011),f1(x9012,x9013)),f1(x9014,x9015)))),
% 58.59/59.13 inference(scs_inference,[],[21,186,3])).
% 58.59/59.13 cnf(905,plain,
% 58.59/59.13 (E(f1(x9051,f1(x9052,f1(x9053,x9054))),f1(x9053,f1(f1(x9054,x9051),x9052)))),
% 58.59/59.13 inference(scs_inference,[],[21,901,49,2,3])).
% 58.59/59.13 cnf(909,plain,
% 58.59/59.13 (E(f1(x9091,f1(f1(x9092,f1(x9093,x9094)),x9095)),f1(f1(f1(x9095,x9091),f1(x9092,x9093)),x9094))),
% 58.59/59.13 inference(scs_inference,[],[21,905,89,2,3])).
% 58.59/59.13 cnf(913,plain,
% 58.59/59.13 (E(f1(x9131,f1(f1(f1(x9132,x9133),x9134),x9135)),f1(f1(f1(f1(x9135,x9131),x9132),x9133),x9134))),
% 58.59/59.13 inference(scs_inference,[],[21,909,84,2,3])).
% 58.59/59.13 cnf(917,plain,
% 58.59/59.13 (E(f1(x9171,f1(f1(x9172,x9173),f1(x9174,x9175))),f1(x9174,f1(f1(x9175,f1(x9171,x9172)),x9173)))),
% 58.59/59.13 inference(scs_inference,[],[21,913,131,2,3])).
% 58.59/59.13 cnf(921,plain,
% 58.59/59.13 (E(f1(x9211,f1(f1(x9212,f1(x9213,x9214)),x9215)),f1(x9215,f1(f1(x9211,f1(x9212,x9213)),x9214)))),
% 58.59/59.13 inference(scs_inference,[],[21,917,137,2,3])).
% 58.59/59.13 cnf(925,plain,
% 58.59/59.13 (E(f1(x9251,f1(f1(x9252,f1(x9253,x9254)),x9255)),f1(f1(x9255,f1(x9251,f1(x9252,x9253))),x9254))),
% 58.59/59.13 inference(scs_inference,[],[21,921,151,2,3])).
% 58.59/59.13 cnf(929,plain,
% 58.59/59.13 (E(f1(x9291,f1(x9292,f1(f1(x9293,x9294),x9295))),f1(f1(f1(x9293,f1(x9294,x9295)),x9291),x9292))),
% 58.59/59.13 inference(scs_inference,[],[21,925,161,2,3])).
% 58.59/59.13 cnf(933,plain,
% 58.59/59.13 (E(f1(x9331,f1(f1(f1(x9332,x9333),x9334),x9335)),f1(f1(f1(x9332,f1(x9333,x9334)),x9335),x9331))),
% 58.59/59.13 inference(scs_inference,[],[21,929,2,3])).
% 58.59/59.13 cnf(937,plain,
% 58.59/59.13 (E(f1(x9371,f1(x9372,f1(x9373,f1(x9374,x9375)))),f1(x9373,f1(f1(x9374,f1(x9375,x9371)),x9372)))),
% 58.59/59.13 inference(scs_inference,[],[21,933,179,2,3])).
% 58.59/59.13 cnf(941,plain,
% 58.59/59.13 (E(f1(f1(x9411,x9412),f1(f1(x9413,x9414),x9415)),f1(x9415,f1(f1(x9411,f1(x9412,x9413)),x9414)))),
% 58.59/59.13 inference(scs_inference,[],[21,937,182,2,3])).
% 58.59/59.13 cnf(945,plain,
% 58.59/59.13 (E(f1(x9451,f1(x9452,f1(x9453,f1(x9454,x9455)))),f1(f1(x9453,f1(x9454,f1(x9455,x9451))),x9452))),
% 58.59/59.13 inference(scs_inference,[],[21,941,195,2,3])).
% 58.59/59.13 cnf(949,plain,
% 58.59/59.13 (E(f1(x9491,f1(f1(x9492,f1(x9493,x9494)),x9495)),f1(f1(x9492,f1(x9493,f1(x9494,x9495))),x9491))),
% 58.59/59.13 inference(scs_inference,[],[21,945,2,3])).
% 58.59/59.13 cnf(953,plain,
% 58.59/59.13 (E(f1(f1(x9531,x9532),f1(f1(x9533,x9534),x9535)),f1(f1(x9535,f1(x9531,f1(x9532,x9533))),x9534))),
% 58.59/59.13 inference(scs_inference,[],[21,949,199,2,3])).
% 58.59/59.13 cnf(957,plain,
% 58.59/59.13 (E(f1(f1(x9571,x9572),f1(x9573,f1(x9574,x9575))),f1(f1(x9573,f1(x9574,f1(x9575,x9571))),x9572))),
% 58.59/59.13 inference(scs_inference,[],[21,953,2,3])).
% 58.59/59.13 cnf(961,plain,
% 58.59/59.13 (E(f1(x9611,f1(f1(f1(x9612,x9613),f1(x9614,x9615)),x9616)),f1(f1(f1(x9616,x9611),f1(x9612,f1(x9613,x9614))),x9615))),
% 58.59/59.13 inference(scs_inference,[],[21,957,203,2,3])).
% 58.59/59.13 cnf(965,plain,
% 58.59/59.13 (E(f1(x9651,f1(x9652,f1(x9653,f1(x9654,x9655)))),f1(f1(f1(f1(x9653,x9654),x9655),x9651),x9652))),
% 58.59/59.13 inference(scs_inference,[],[21,961,224,2,3])).
% 58.59/59.13 cnf(969,plain,
% 58.59/59.13 (E(f1(x9691,f1(f1(x9692,f1(x9693,x9694)),x9695)),f1(f1(f1(f1(x9692,x9693),x9694),x9695),x9691))),
% 58.59/59.13 inference(scs_inference,[],[21,965,2,3])).
% 58.59/59.13 cnf(973,plain,
% 58.59/59.13 (E(f1(f1(x9731,x9732),f1(x9733,x9734)),f1(f1(x9734,x9731),f1(x9732,x9733)))),
% 58.59/59.13 inference(scs_inference,[],[21,969,45,2,3])).
% 58.59/59.13 cnf(976,plain,
% 58.59/59.13 (E(f1(f1(x9761,x9762),f1(x9763,x9764)),f1(f1(x9762,x9763),f1(x9764,x9761)))),
% 58.59/59.13 inference(scs_inference,[],[973,2])).
% 58.59/59.13 cnf(1037,plain,
% 58.59/59.13 (E(f3(f1(f3(f1(x10371,x10372)),x10373)),f3(f1(f3(f1(x10372,x10371)),x10373)))),
% 58.59/59.13 inference(scs_inference,[],[23,6,4])).
% 58.59/59.13 cnf(1042,plain,
% 58.59/59.13 (E(f3(f1(x10421,f3(f1(x10422,x10423)))),f3(f1(x10421,f3(f1(x10423,x10422)))))),
% 58.59/59.13 inference(scs_inference,[],[23,6,5])).
% 58.59/59.13 cnf(1435,plain,
% 58.59/59.13 (~E(f1(f3(f1(f3(a4),x14351)),f3(f1(f3(a4),f3(x14351)))),f1(f3(f1(a2,f3(a4))),f3(f1(f3(a2),f3(a4)))))),
% 58.59/59.13 inference(scs_inference,[],[24,976,779,29,6,4,5,11,2])).
% 58.59/59.13 cnf(1438,plain,
% 58.59/59.13 ($false),
% 58.59/59.13 inference(scs_inference,[],[1435,1037,1042,11,3]),
% 58.59/59.13 ['proof']).
% 58.59/59.13 % SZS output end Proof
% 58.59/59.13 % Total time :58.060000s
%------------------------------------------------------------------------------