%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL143-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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 : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:18:41 AM UTC 2026
% Result : Unsatisfiable 59.11s 59.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL143-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.35 % Computer : n004.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Fri Sep 4 23:44:44 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.26/0.51 start to proof:theBenchmark
% 59.11/59.27 %-------------------------------------------
% 59.11/59.27 % File :CSE---1.7
% 59.11/59.27 % Problem :theBenchmark
% 59.11/59.27 % Transform :cnf
% 59.11/59.27 % Format :tptp:raw
% 59.11/59.27 % Command :java -jar mcs_scs.jar %d %s
% 59.11/59.27
% 59.11/59.27 % Result :Theorem 58.771900s
% 59.11/59.27 % Output :CNFRefutation 58.771900s
% 59.11/59.27 %-------------------------------------------
% 59.11/59.27 %--------------------------------------------------------------------------
% 59.11/59.27 % File : LCL143-1 : TPTP v9.3.1. Released v1.0.0.
% 59.11/59.27 % Domain : Logic Calculi (Wajsberg Algebra)
% 59.11/59.27 % Problem : A theorem in the lattice structure of Wajsberg algebras
% 59.11/59.27 % Version : [Bon91] (equality) axioms.
% 59.11/59.27 % English :
% 59.11/59.27
% 59.11/59.27 % Refs : [FRT84] Font et al. (1984), Wajsberg Algebras
% 59.11/59.27 % : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic
% 59.11/59.27 % Source : [Bon91]
% 59.11/59.27 % Names : Lattice structure theorem 2 [Bon91]
% 59.11/59.27
% 59.11/59.27 % Status : Unsatisfiable
% 59.11/59.27 % Rating : 0.00 v9.1.0, 0.08 v9.0.0, 0.06 v8.2.0, 0.00 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.20 v5.3.0, 0.33 v5.2.0, 0.25 v5.1.0, 0.14 v5.0.0, 0.00 v2.6.0, 0.14 v2.5.0, 0.00 v2.0.0
% 59.11/59.27 % Syntax : Number of clauses : 10 ( 8 unt; 0 nHn; 4 RR)
% 59.11/59.27 % Number of literals : 12 ( 8 equ; 3 neg)
% 59.11/59.27 % Maximal clause size : 2 ( 1 avg)
% 59.11/59.27 % Maximal term depth : 4 ( 2 avg)
% 59.11/59.27 % Number of predicates : 2 ( 1 usr; 0 prp; 2-2 aty)
% 59.11/59.27 % Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% 59.11/59.27 % Number of variables : 16 ( 0 sgn)
% 59.11/59.27 % SPC : CNF_UNS_RFO_SEQ_HRN
% 59.11/59.27
% 59.11/59.27 % Comments :
% 59.11/59.27 %--------------------------------------------------------------------------
% 59.11/59.27 %----Include Wajsberg algebra axioms
% 59.11/59.27 include('Axioms/LCL001-0.ax').
% 59.11/59.27 %----Include Wajsberg algebra lattice structure axioms
% 59.11/59.27 include('Axioms/LCL001-1.ax').
% 59.11/59.27 %--------------------------------------------------------------------------
% 59.11/59.27 cnf(antecedent,negated_conjecture,
% 59.11/59.27 ordered(x,y) ).
% 59.11/59.27
% 59.11/59.27 cnf(prove_wajsberg_theorem,negated_conjecture,
% 59.11/59.27 ~ ordered(implies(z,x),implies(z,y)) ).
% 59.11/59.27
% 59.11/59.27 %--------------------------------------------------------------------------
% 59.11/59.27 %-------------------------------------------
% 59.11/59.27 % Proof found
% 59.11/59.27 % SZS status Theorem for theBenchmark
% 59.11/59.27 % SZS output start Proof
% 59.11/59.27 %ClaNum:16(EqnAxiom:8)
% 59.11/59.27 %VarNum:26(SingletonVarNum:12)
% 59.11/59.27 %MaxLitNum:2
% 59.11/59.27 %MaxfuncDepth:3
% 59.11/59.27 %SharedTerms:8
% 59.11/59.27 %goalClause: 9 14
% 59.11/59.27 %singleGoalClaCount:2
% 59.11/59.27 [9]P1(a1,a5)
% 59.11/59.27 [14]~P1(f3(a6,a1),f3(a6,a5))
% 59.11/59.27 [10]E(f3(a2,x101),x101)
% 59.11/59.27 [11]E(f3(f3(x111,x112),x112),f3(f3(x112,x111),x111))
% 59.11/59.27 [12]E(f3(f3(f4(x121),f4(x122)),f3(x122,x121)),a2)
% 59.11/59.27 [13]E(f3(f3(x131,x132),f3(f3(x132,x133),f3(x131,x133))),a2)
% 59.11/59.27 [15]~P1(x151,x152)+E(f3(x151,x152),a2)
% 59.11/59.27 [16]P1(x161,x162)+~E(f3(x161,x162),a2)
% 59.11/59.27 %EqnAxiom
% 59.11/59.27 [1]E(x11,x11)
% 59.11/59.27 [2]E(x22,x21)+~E(x21,x22)
% 59.11/59.27 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.11/59.27 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 59.11/59.27 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 59.11/59.27 [6]~E(x61,x62)+E(f4(x61),f4(x62))
% 59.11/59.27 [7]P1(x72,x73)+~E(x71,x72)+~P1(x71,x73)
% 59.11/59.27 [8]P1(x83,x82)+~E(x81,x82)+~P1(x83,x81)
% 59.11/59.27
% 59.11/59.27 %-------------------------------------------
% 59.11/59.28 cnf(17,plain,
% 59.11/59.28 (P1(a2,a2)),
% 59.11/59.28 inference(scs_inference,[],[10,16])).
% 59.11/59.28 cnf(18,plain,
% 59.11/59.28 (E(f3(a2,x181),x181)),
% 59.11/59.28 inference(rename_variables,[],[10])).
% 59.11/59.28 cnf(20,plain,
% 59.11/59.28 (E(x201,f3(a2,x201))),
% 59.11/59.28 inference(scs_inference,[],[10,18,16,2])).
% 59.11/59.28 cnf(21,plain,
% 59.11/59.28 (P1(f3(a2,a1),a5)),
% 59.11/59.28 inference(scs_inference,[],[9,10,18,16,2,7])).
% 59.11/59.28 cnf(22,plain,
% 59.11/59.28 (E(x221,a2)+~E(x221,f3(f3(f4(x222),f4(x223)),f3(x223,x222)))),
% 59.11/59.28 inference(scs_inference,[],[9,10,18,12,16,2,7,3])).
% 59.11/59.28 cnf(25,plain,
% 59.11/59.28 (P1(f3(x251,x252),f3(f3(x252,x253),f3(x251,x253)))),
% 59.11/59.28 inference(scs_inference,[],[13,16])).
% 59.11/59.28 cnf(27,plain,
% 59.11/59.28 (E(a2,f3(f3(x271,x272),f3(f3(x272,x273),f3(x271,x273))))),
% 59.11/59.28 inference(scs_inference,[],[13,16,2])).
% 59.11/59.28 cnf(28,plain,
% 59.11/59.28 (E(f3(f3(x281,x282),x282),f3(a2,f3(f3(x282,x281),x281)))),
% 59.11/59.28 inference(scs_inference,[],[20,11,13,16,2,3])).
% 59.11/59.28 cnf(34,plain,
% 59.11/59.28 (P1(f3(f4(x341),f4(x342)),f3(x342,x341))),
% 59.11/59.28 inference(scs_inference,[],[12,16])).
% 59.11/59.28 cnf(37,plain,
% 59.11/59.28 (E(f3(a2,a2),f3(f3(x371,x372),f3(f3(x372,x373),f3(x371,x373))))),
% 59.11/59.28 inference(scs_inference,[],[28,27,10,12,16,2,3])).
% 59.11/59.28 cnf(43,plain,
% 59.11/59.28 (E(f3(f3(x431,x432),f3(f3(x432,x433),f3(x431,x433))),f3(a2,a2))),
% 59.11/59.28 inference(scs_inference,[],[37,2])).
% 59.11/59.28 cnf(44,plain,
% 59.11/59.28 (~E(f3(f4(a5),f4(a6)),f3(a6,a1))),
% 59.11/59.28 inference(scs_inference,[],[14,34,37,2,7])).
% 59.11/59.28 cnf(50,plain,
% 59.11/59.28 (E(a2,f3(f3(f4(x501),f4(x502)),f3(x502,x501)))),
% 59.11/59.28 inference(scs_inference,[],[12,2])).
% 59.11/59.28 cnf(51,plain,
% 59.11/59.28 (P1(f3(f3(x511,x512),f3(f3(x512,x513),f3(x511,x513))),a2)),
% 59.11/59.28 inference(scs_inference,[],[17,27,12,2,7])).
% 59.11/59.28 cnf(52,plain,
% 59.11/59.28 (E(f3(a2,f3(f3(f4(x521),f4(x522)),f3(x522,x521))),a2)),
% 59.11/59.28 inference(scs_inference,[],[17,27,12,10,2,7,3])).
% 59.11/59.28 cnf(54,plain,
% 59.11/59.28 (P1(f3(a2,a1),f3(a2,a5))),
% 59.11/59.28 inference(scs_inference,[],[21,17,27,12,20,10,2,7,3,8])).
% 59.11/59.28 cnf(56,plain,
% 59.11/59.28 (P1(a2,f3(f3(f4(x561),f4(x562)),f3(x562,x561)))),
% 59.11/59.28 inference(scs_inference,[],[21,17,27,12,20,10,2,7,3,8,16])).
% 59.11/59.28 cnf(59,plain,
% 59.11/59.28 (P1(f3(a2,a2),a2)),
% 59.11/59.28 inference(scs_inference,[],[51,43,52,2,7])).
% 59.11/59.28 cnf(61,plain,
% 59.11/59.28 (~E(f3(f3(a1,x611),f3(a6,x611)),f3(a6,a5))),
% 59.11/59.28 inference(scs_inference,[],[14,51,25,43,52,2,7,8])).
% 59.11/59.28 cnf(63,plain,
% 59.11/59.28 (P1(f3(f3(f4(x631),f4(x632)),f3(x632,x631)),f3(f3(f4(x633),f4(x634)),f3(x634,x633)))),
% 59.11/59.28 inference(scs_inference,[],[50,56,7])).
% 59.11/59.28 cnf(68,plain,
% 59.11/59.28 (P1(f3(a2,a1),f3(a2,f3(a2,a5)))),
% 59.11/59.28 inference(scs_inference,[],[54,17,50,20,7,8])).
% 59.11/59.28 cnf(70,plain,
% 59.11/59.28 (P1(a1,f3(a2,f3(a2,a5)))),
% 59.11/59.28 inference(scs_inference,[],[68,10,7])).
% 59.11/59.28 cnf(72,plain,
% 59.11/59.28 (P1(f3(a2,a2),f3(f3(x721,x722),f3(f3(x722,x723),f3(x721,x723))))),
% 59.11/59.28 inference(scs_inference,[],[59,68,27,10,7,8])).
% 59.11/59.28 cnf(74,plain,
% 59.11/59.28 (E(x741,f3(a2,x741))),
% 59.11/59.28 inference(rename_variables,[],[20])).
% 59.11/59.28 cnf(75,plain,
% 59.11/59.28 (P1(a1,f3(a2,f3(a2,f3(a2,a5))))),
% 59.11/59.28 inference(scs_inference,[],[70,68,20,74,7,8])).
% 59.11/59.28 cnf(79,plain,
% 59.11/59.28 (P1(f3(a2,a2),f3(a2,a2))),
% 59.11/59.28 inference(scs_inference,[],[72,75,43,20,7,8])).
% 59.11/59.28 cnf(81,plain,
% 59.11/59.28 (P1(f3(f3(x811,x812),f3(f3(x812,x813),f3(x811,x813))),f3(a2,a2))),
% 59.11/59.28 inference(scs_inference,[],[79,37,7])).
% 59.11/59.28 cnf(84,plain,
% 59.11/59.28 (E(f3(f3(a2,a1),a5),a2)),
% 59.11/59.28 inference(scs_inference,[],[9,20,15,7])).
% 59.11/59.28 cnf(85,plain,
% 59.11/59.28 (E(a2,f3(f3(a2,a1),a5))),
% 59.11/59.28 inference(scs_inference,[],[84,2])).
% 59.11/59.28 cnf(86,plain,
% 59.11/59.28 (E(f3(a2,f3(f3(a2,a1),a5)),a2)),
% 59.11/59.28 inference(scs_inference,[],[10,84,2,3])).
% 59.11/59.28 cnf(94,plain,
% 59.11/59.28 (E(f3(f3(x941,f3(a2,x942)),x943),f3(f3(x941,x942),x943))),
% 59.11/59.28 inference(scs_inference,[],[10,4,5])).
% 59.11/59.28 cnf(96,plain,
% 59.11/59.28 (E(f3(a2,a2),f3(f3(a2,a1),a5))),
% 59.11/59.28 inference(scs_inference,[],[10,94,85,2,3])).
% 59.11/59.28 cnf(103,plain,
% 59.11/59.28 (E(f3(f3(a2,a1),a5),f3(a2,a2))),
% 59.11/59.28 inference(scs_inference,[],[96,2])).
% 59.11/59.28 cnf(104,plain,
% 59.11/59.28 (E(f3(a2,f3(a2,a2)),f3(f3(a2,a1),a5))),
% 59.11/59.28 inference(scs_inference,[],[10,96,2,3])).
% 59.11/59.28 cnf(112,plain,
% 59.11/59.28 (E(f3(a2,f3(f3(a2,a1),a5)),f3(a2,a2))),
% 59.11/59.28 inference(scs_inference,[],[10,103,86,2,3])).
% 59.11/59.28 cnf(119,plain,
% 59.11/59.28 (E(f3(a2,a2),f3(a2,f3(f3(a2,a1),a5)))),
% 59.11/59.28 inference(scs_inference,[],[112,2])).
% 59.11/59.28 cnf(120,plain,
% 59.11/59.28 (E(f3(a2,f3(a2,f3(a2,a2))),f3(f3(a2,a1),a5))),
% 59.11/59.28 inference(scs_inference,[],[10,112,104,2,3])).
% 59.11/59.28 cnf(122,plain,
% 59.11/59.28 (P1(f3(f3(x1221,x1222),f3(f3(f3(a2,x1222),x1223),f3(x1221,x1223))),f3(a2,a2))),
% 59.11/59.28 inference(scs_inference,[],[10,81,112,104,94,2,3,7])).
% 59.11/59.28 cnf(129,plain,
% 59.11/59.28 (E(f3(a2,f3(a2,a2)),f3(a2,f3(f3(a2,a1),a5)))),
% 59.11/59.28 inference(scs_inference,[],[10,119,120,2,3])).
% 59.11/59.28 cnf(137,plain,
% 59.11/59.28 (E(f3(a2,f3(a2,a2)),f3(f3(x1371,x1372),f3(f3(x1372,x1373),f3(x1371,x1373))))),
% 59.11/59.28 inference(scs_inference,[],[10,129,37,2,3])).
% 59.11/59.28 cnf(142,plain,
% 59.11/59.28 (E(f3(f3(x1421,x1422),f3(f3(x1422,x1423),f3(x1421,x1423))),f3(a2,f3(a2,a2)))),
% 59.11/59.28 inference(scs_inference,[],[137,2])).
% 59.11/59.29 cnf(143,plain,
% 59.11/59.29 (E(f3(a2,a2),f3(f3(f4(x1431),f4(x1432)),f3(x1432,x1431)))),
% 59.11/59.29 inference(scs_inference,[],[10,137,50,2,3])).
% 59.11/59.29 cnf(149,plain,
% 59.11/59.29 (E(f3(f3(f4(x1491),f4(x1492)),f3(x1492,x1491)),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[143,2])).
% 59.11/59.29 cnf(150,plain,
% 59.11/59.29 (E(f3(a2,f3(a2,a2)),f3(f3(f4(x1501),f4(x1502)),f3(x1502,x1501)))),
% 59.11/59.29 inference(scs_inference,[],[10,143,2,3])).
% 59.11/59.29 cnf(152,plain,
% 59.11/59.29 (P1(f3(a2,f3(a2,a2)),a2)),
% 59.11/59.29 inference(scs_inference,[],[10,51,143,142,2,3,7])).
% 59.11/59.29 cnf(155,plain,
% 59.11/59.29 (E(f3(f3(f4(x1551),f4(x1552)),f3(x1552,x1551)),f3(a2,f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[150,2])).
% 59.11/59.29 cnf(156,plain,
% 59.11/59.29 (E(f3(a2,f3(f3(f4(x1561),f4(x1562)),f3(x1562,x1561))),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[10,150,149,2,3])).
% 59.11/59.29 cnf(162,plain,
% 59.11/59.29 (E(f3(x1621,x1622),f3(f3(a2,x1621),x1622))),
% 59.11/59.29 inference(scs_inference,[],[10,2,4])).
% 59.11/59.29 cnf(163,plain,
% 59.11/59.29 (E(f3(f3(a2,x1631),x1632),f3(x1631,x1632))),
% 59.11/59.29 inference(scs_inference,[],[162,2])).
% 59.11/59.29 cnf(164,plain,
% 59.11/59.29 (E(f3(a2,f3(x1641,x1642)),f3(f3(a2,x1641),x1642))),
% 59.11/59.29 inference(scs_inference,[],[10,162,2,3])).
% 59.11/59.29 cnf(166,plain,
% 59.11/59.29 (P1(f3(a2,f3(a2,a2)),f3(f3(f4(x1661),f4(x1662)),f3(x1662,x1661)))),
% 59.11/59.29 inference(scs_inference,[],[10,63,155,162,2,3,7])).
% 59.11/59.29 cnf(168,plain,
% 59.11/59.29 (P1(f3(a2,f3(a2,a2)),f3(f3(a2,a1),a5))),
% 59.11/59.29 inference(scs_inference,[],[10,152,63,155,162,85,2,3,7,8])).
% 59.11/59.29 cnf(169,plain,
% 59.11/59.29 (E(f3(x1691,x1692),f3(x1691,f3(a2,x1692)))),
% 59.11/59.29 inference(scs_inference,[],[10,2,5])).
% 59.11/59.29 cnf(170,plain,
% 59.11/59.29 (E(f3(x1701,f3(a2,x1702)),f3(x1701,x1702))),
% 59.11/59.29 inference(scs_inference,[],[169,2])).
% 59.11/59.29 cnf(172,plain,
% 59.11/59.29 (E(f3(f3(a2,x1721),x1722),f3(x1721,x1722))),
% 59.11/59.29 inference(rename_variables,[],[163])).
% 59.11/59.29 cnf(173,plain,
% 59.11/59.29 (P1(f3(x1731,f3(f3(f3(a2,x1731),x1732),f3(a2,x1732))),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[44,122,163,172,169,2,3,7])).
% 59.11/59.29 cnf(177,plain,
% 59.11/59.29 (E(f4(x1771),f4(f3(a2,x1771)))),
% 59.11/59.29 inference(scs_inference,[],[10,2,6])).
% 59.11/59.29 cnf(178,plain,
% 59.11/59.29 (E(f4(f3(a2,x1781)),f4(x1781))),
% 59.11/59.29 inference(scs_inference,[],[177,2])).
% 59.11/59.29 cnf(180,plain,
% 59.11/59.29 (E(f3(x1801,f3(a2,x1802)),f3(x1801,x1802))),
% 59.11/59.29 inference(rename_variables,[],[170])).
% 59.11/59.29 cnf(184,plain,
% 59.11/59.29 (P1(f3(f3(f3(a2,a2),x1841),f3(a2,x1841)),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[10,166,173,44,170,180,177,2,3,8,7])).
% 59.11/59.29 cnf(187,plain,
% 59.11/59.29 (E(f3(a2,f3(a2,a2)),a2)),
% 59.11/59.29 inference(scs_inference,[],[155,2,22])).
% 59.11/59.29 cnf(191,plain,
% 59.11/59.29 (E(f3(a2,f4(f3(a2,x1911))),f4(x1911))),
% 59.11/59.29 inference(scs_inference,[],[10,178,156,187,16,2,3])).
% 59.11/59.29 cnf(193,plain,
% 59.11/59.29 (P1(f3(f3(f3(a2,a2),x1931),x1931),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[10,184,178,156,187,170,16,2,3,7])).
% 59.11/59.29 cnf(198,plain,
% 59.11/59.29 (E(a2,f3(a1,a5))),
% 59.11/59.29 inference(scs_inference,[],[9,2,15])).
% 59.11/59.29 cnf(200,plain,
% 59.11/59.29 (E(f3(a2,a2),f3(a1,a5))),
% 59.11/59.29 inference(scs_inference,[],[10,191,198,2,3])).
% 59.11/59.29 cnf(207,plain,
% 59.11/59.29 (E(f3(f3(a2,x2071),x2072),f3(a2,f3(x2071,x2072)))),
% 59.11/59.29 inference(scs_inference,[],[164,2])).
% 59.11/59.29 cnf(215,plain,
% 59.11/59.29 (E(f3(a1,a5),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[200,2])).
% 59.11/59.29 cnf(216,plain,
% 59.11/59.29 (E(f3(a2,f3(a2,a2)),f3(a1,a5))),
% 59.11/59.29 inference(scs_inference,[],[10,200,2,3])).
% 59.11/59.29 cnf(222,plain,
% 59.11/59.29 (E(f3(f4(f3(a2,x2221)),x2222),f3(f4(x2221),x2222))),
% 59.11/59.29 inference(scs_inference,[],[10,6,4])).
% 59.11/59.29 cnf(224,plain,
% 59.11/59.29 (E(f3(a2,f3(a2,f3(a2,a2))),f3(a1,a5))),
% 59.11/59.29 inference(scs_inference,[],[10,222,216,2,3])).
% 59.11/59.29 cnf(231,plain,
% 59.11/59.29 (E(f4(f3(x2311,f3(a2,x2312))),f4(f3(x2311,x2312)))),
% 59.11/59.29 inference(scs_inference,[],[10,6,5])).
% 59.11/59.29 cnf(233,plain,
% 59.11/59.29 (E(f3(a2,f3(a1,a5)),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[10,231,215,2,3])).
% 59.11/59.29 cnf(239,plain,
% 59.11/59.29 (E(f3(x2391,f4(f3(a2,x2392))),f3(x2391,f4(x2392)))),
% 59.11/59.29 inference(scs_inference,[],[10,6,5])).
% 59.11/59.29 cnf(241,plain,
% 59.11/59.29 (E(f3(a2,f3(a2,f3(a1,a5))),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[10,239,233,2,3])).
% 59.11/59.29 cnf(243,plain,
% 59.11/59.29 (P1(f3(f3(f3(a2,a2),f4(f3(a2,x2431))),f4(x2431)),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[10,193,239,233,2,3,7])).
% 59.11/59.29 cnf(248,plain,
% 59.11/59.29 (E(f4(f3(a1,a5)),f4(a2))),
% 59.11/59.29 inference(scs_inference,[],[9,6,15])).
% 59.11/59.29 cnf(249,plain,
% 59.11/59.29 (E(f3(a1,a5),f3(a2,f3(a2,f3(a2,a2))))),
% 59.11/59.29 inference(scs_inference,[],[224,2])).
% 59.11/59.29 cnf(251,plain,
% 59.11/59.29 (E(f3(a2,x2511),x2511)),
% 59.11/59.29 inference(rename_variables,[],[10])).
% 59.11/59.29 cnf(254,plain,
% 59.11/59.29 (P1(f3(x2541,f3(f3(x2541,x2542),f3(a2,x2542))),a2)),
% 59.11/59.29 inference(scs_inference,[],[10,251,243,51,224,248,163,2,3,8,7])).
% 59.11/59.29 cnf(258,plain,
% 59.11/59.29 (E(f3(a2,a2),f3(a2,f3(a2,f3(a1,a5))))),
% 59.11/59.29 inference(scs_inference,[],[241,2])).
% 59.11/59.29 cnf(259,plain,
% 59.11/59.29 (E(f3(a2,f3(a1,a5)),f3(a2,f3(a2,f3(a2,a2))))),
% 59.11/59.29 inference(scs_inference,[],[10,249,241,2,3])).
% 59.11/59.29 cnf(260,plain,
% 59.11/59.29 (E(f3(a2,x2601),x2601)),
% 59.11/59.29 inference(rename_variables,[],[10])).
% 59.11/59.29 cnf(261,plain,
% 59.11/59.29 (P1(f3(f3(a2,x2611),f3(a2,x2611)),a2)),
% 59.11/59.29 inference(scs_inference,[],[10,260,254,249,241,2,3,7])).
% 59.11/59.29 cnf(269,plain,
% 59.11/59.29 (P1(f3(f3(a2,x2691),f3(a2,x2691)),f3(a1,a5))),
% 59.11/59.29 inference(scs_inference,[],[10,261,259,258,198,2,3,8])).
% 59.11/59.29 cnf(340,plain,
% 59.11/59.29 (E(f3(a2,f4(a2)),f4(f3(a1,a5)))),
% 59.11/59.29 inference(scs_inference,[],[10,248,2,3])).
% 59.11/59.29 cnf(361,plain,
% 59.11/59.29 (E(f4(f3(a1,a5)),f3(a2,f4(a2)))),
% 59.11/59.29 inference(scs_inference,[],[340,2])).
% 59.11/59.29 cnf(369,plain,
% 59.11/59.29 (E(f3(a1,a5),f3(a2,f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[216,2])).
% 59.11/59.29 cnf(387,plain,
% 59.11/59.29 (E(a2,f3(a2,f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[187,2])).
% 59.11/59.29 cnf(393,plain,
% 59.11/59.29 (E(f4(f3(a2,f3(a1,a5))),f3(a2,f4(a2)))),
% 59.11/59.29 inference(scs_inference,[],[10,361,6,3])).
% 59.11/59.29 cnf(397,plain,
% 59.11/59.29 (P1(f3(x3971,f3(f3(x3971,x3972),f3(a2,x3972))),f3(a2,f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[10,254,393,168,387,2,7,8])).
% 59.11/59.29 cnf(398,plain,
% 59.11/59.29 (E(f4(f3(a1,a5)),f4(f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[10,369,6,3])).
% 59.11/59.29 cnf(399,plain,
% 59.11/59.29 (E(f4(f3(a2,a2)),f4(f3(a1,a5)))),
% 59.11/59.29 inference(scs_inference,[],[398,2])).
% 59.11/59.29 cnf(400,plain,
% 59.11/59.29 (E(f3(a2,f4(f3(a1,a5))),f4(f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[10,398,2,3])).
% 59.11/59.29 cnf(401,plain,
% 59.11/59.29 (E(f3(a2,x4011),x4011)),
% 59.11/59.29 inference(rename_variables,[],[10])).
% 59.11/59.29 cnf(402,plain,
% 59.11/59.29 (P1(f3(f3(a2,x4021),f3(a2,x4021)),f3(a2,f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[10,401,397,398,2,3,7])).
% 59.11/59.29 cnf(409,plain,
% 59.11/59.29 (E(f3(a2,x4091),x4091)),
% 59.11/59.29 inference(rename_variables,[],[10])).
% 59.11/59.29 cnf(413,plain,
% 59.11/59.29 (P1(f3(f3(a2,x4131),f3(a2,x4131)),f3(a2,a2))),
% 59.11/59.29 inference(scs_inference,[],[10,409,402,400,269,399,207,2,3,7,8])).
% 59.11/59.29 cnf(471,plain,
% 59.11/59.29 (P1(f3(f3(a2,x4711),x4711),f3(a2,f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[402,170,7])).
% 59.11/59.29 cnf(475,plain,
% 59.11/59.29 (E(f3(f3(a1,a5),x4751),f3(a2,x4751))),
% 59.11/59.29 inference(scs_inference,[],[9,15,4])).
% 59.11/59.29 cnf(482,plain,
% 59.11/59.29 (E(f3(a1,f3(a2,a5)),a2)),
% 59.11/59.29 inference(scs_inference,[],[9,20,15,8])).
% 59.11/59.29 cnf(484,plain,
% 59.11/59.29 (E(f3(a2,f3(a1,f3(a2,a5))),a2)),
% 59.11/59.29 inference(scs_inference,[],[10,482,2,3])).
% 59.11/59.29 cnf(492,plain,
% 59.11/59.29 (E(f3(x4921,f3(a1,a5)),f3(x4921,a2))),
% 59.11/59.29 inference(scs_inference,[],[9,15,5])).
% 59.11/59.29 cnf(494,plain,
% 59.11/59.29 (E(f3(a2,f3(x4941,f3(a1,a5))),f3(x4941,a2))),
% 59.11/59.29 inference(scs_inference,[],[10,492,2,3])).
% 59.11/59.29 cnf(500,plain,
% 59.11/59.29 (E(f3(x5001,a2),f3(a2,f3(x5001,f3(a1,a5))))),
% 59.11/59.29 inference(scs_inference,[],[494,2])).
% 59.11/59.29 cnf(514,plain,
% 59.11/59.29 (E(f3(a2,f3(x5141,a2)),f3(a2,f3(x5141,f3(a1,a5))))),
% 59.11/59.29 inference(scs_inference,[],[10,484,500,2,3])).
% 59.11/59.29 cnf(545,plain,
% 59.11/59.29 (~E(f3(f3(a6,a1),f3(a6,a5)),f3(f3(f4(x5451),f4(x5452)),f3(x5452,x5451)))),
% 59.11/59.29 inference(scs_inference,[],[14,16,22])).
% 59.11/59.29 cnf(547,plain,
% 59.11/59.29 (~E(f3(f3(a6,a1),f3(a6,a5)),f3(f3(f4(x5471),f4(x5472)),f3(x5472,x5471)))),
% 59.11/59.29 inference(rename_variables,[],[545])).
% 59.11/59.29 cnf(549,plain,
% 59.11/59.29 (~E(f3(f3(a6,a1),f3(a6,a5)),f3(a2,f3(a2,a2)))),
% 59.11/59.29 inference(scs_inference,[],[545,547,514,150,4,2,3])).
% 59.11/59.29 cnf(700,plain,
% 59.11/59.29 (~E(f3(f3(a6,a1),f3(a6,a5)),f3(f3(x7001,x7002),f3(f3(x7002,x7003),f3(x7001,x7003))))),
% 59.11/59.29 inference(scs_inference,[],[142,549,3])).
% 59.11/59.29 cnf(706,plain,
% 59.11/59.29 (~E(f3(a6,a5),f3(a2,f3(f3(a1,x7061),f3(a6,x7061))))),
% 59.11/59.29 inference(scs_inference,[],[700,10,5,3])).
% 59.11/59.29 cnf(852,plain,
% 59.11/59.29 (~E(f3(a6,a5),f3(f3(a2,f3(a1,x8521)),f3(a6,x8521)))),
% 59.11/59.29 inference(scs_inference,[],[706,207,3])).
% 59.11/59.29 cnf(1780,plain,
% 59.11/59.29 (P1(f3(f3(a2,x17801),x17801),f3(a1,a5))),
% 59.11/59.29 inference(scs_inference,[],[471,216,8])).
% 59.11/59.29 cnf(1877,plain,
% 59.11/59.29 (E(f3(f3(f3(a2,x18771),x18771),f3(a1,a5)),a2)),
% 59.11/59.29 inference(scs_inference,[],[1780,15])).
% 59.11/59.29 cnf(1894,plain,
% 59.11/59.29 ($false),
% 59.11/59.29 inference(scs_inference,[],[413,61,852,1877,475,10,15,6,5,4,2,3]),
% 59.11/59.29 ['proof']).
% 59.11/59.29 % SZS output end Proof
% 59.11/59.29 % Total time :58.771900s
%------------------------------------------------------------------------------