%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL132-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 : n031.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:40 AM UTC 2026
% Result : Unsatisfiable 78.67s 78.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL132-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n031.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Fri Sep 4 20:20:54 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.24/0.48 start to proof:theBenchmark
% 78.67/78.87 %-------------------------------------------
% 78.67/78.87 % File :CSE---1.7
% 78.67/78.87 % Problem :theBenchmark
% 78.67/78.87 % Transform :cnf
% 78.67/78.87 % Format :tptp:raw
% 78.67/78.87 % Command :java -jar mcs_scs.jar %d %s
% 78.67/78.87
% 78.67/78.87 % Result :Theorem 78.376335s
% 78.67/78.87 % Output :CNFRefutation 78.376335s
% 78.67/78.87 %-------------------------------------------
% 78.67/78.87 %--------------------------------------------------------------------------
% 78.67/78.87 % File : LCL132-1 : TPTP v9.3.1. Released v1.0.0.
% 78.67/78.87 % Domain : Logic Calculi (Wajsberg Algebra)
% 78.67/78.87 % Problem : A lemma in Wajsberg algebras
% 78.67/78.87 % Version : [Bon91] (equality) axioms.
% 78.67/78.87 % English :
% 78.67/78.87
% 78.67/78.87 % Refs : [FRT84] Font et al. (1984), Wajsberg Algebras
% 78.67/78.87 % : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic
% 78.67/78.87 % Source : [Bon91]
% 78.67/78.87 % Names : Lemma 1 [Bon91]
% 78.67/78.87
% 78.67/78.87 % Status : Unsatisfiable
% 78.67/78.87 % Rating : 0.00 v7.4.0, 0.09 v7.3.0, 0.05 v7.1.0, 0.06 v7.0.0, 0.05 v6.3.0, 0.12 v6.2.0, 0.14 v6.1.0, 0.06 v6.0.0, 0.14 v5.5.0, 0.11 v5.4.0, 0.00 v5.1.0, 0.07 v5.0.0, 0.00 v2.0.0
% 78.67/78.87 % Syntax : Number of clauses : 5 ( 5 unt; 0 nHn; 1 RR)
% 78.67/78.87 % Number of literals : 5 ( 5 equ; 1 neg)
% 78.67/78.87 % Maximal clause size : 1 ( 1 avg)
% 78.67/78.87 % Maximal term depth : 4 ( 2 avg)
% 78.67/78.87 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty)
% 78.67/78.87 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 78.67/78.87 % Number of variables : 8 ( 0 sgn)
% 78.67/78.87 % SPC : CNF_UNS_RFO_PEQ_UEQ
% 78.67/78.87
% 78.67/78.87 % Comments :
% 78.67/78.87 %--------------------------------------------------------------------------
% 78.67/78.87 %----Include Wajsberg algebra axioms
% 78.67/78.87 include('Axioms/LCL001-0.ax').
% 78.67/78.87 %--------------------------------------------------------------------------
% 78.67/78.87 cnf(prove_wajsberg_lemma,negated_conjecture,
% 78.67/78.87 implies(x,x) != truth ).
% 78.67/78.87
% 78.67/78.87 %--------------------------------------------------------------------------
% 78.67/78.87 %-------------------------------------------
% 78.67/78.87 % Proof found
% 78.67/78.87 % SZS status Theorem for theBenchmark
% 78.67/78.87 % SZS output start Proof
% 78.67/78.87 %ClaNum:11(EqnAxiom:6)
% 78.67/78.87 %VarNum:18(SingletonVarNum:8)
% 78.67/78.87 %MaxLitNum:1
% 78.67/78.87 %MaxfuncDepth:3
% 78.67/78.87 %SharedTerms:4
% 78.67/78.87 %goalClause: 11
% 78.67/78.87 %singleGoalClaCount:1
% 78.67/78.87 [11]~E(f2(a4,a4),a1)
% 78.67/78.87 [7]E(f2(a1,x71),x71)
% 78.67/78.87 [8]E(f2(f2(x81,x82),x82),f2(f2(x82,x81),x81))
% 78.67/78.87 [9]E(f2(f2(f3(x91),f3(x92)),f2(x92,x91)),a1)
% 78.67/78.87 [10]E(f2(f2(x101,x102),f2(f2(x102,x103),f2(x101,x103))),a1)
% 78.67/78.87 %EqnAxiom
% 78.67/78.87 [1]E(x11,x11)
% 78.67/78.87 [2]E(x22,x21)+~E(x21,x22)
% 78.67/78.87 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 78.67/78.87 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43))
% 78.67/78.87 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52))
% 78.67/78.87 [6]~E(x61,x62)+E(f3(x61),f3(x62))
% 78.67/78.87
% 78.67/78.87 %-------------------------------------------
% 78.67/78.88 cnf(12,plain,
% 78.67/78.88 (E(x121,f2(a1,x121))),
% 78.67/78.88 inference(scs_inference,[],[7,2])).
% 78.67/78.88 cnf(13,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(a1,a1))),
% 78.67/78.88 inference(scs_inference,[],[11,7,2,3])).
% 78.67/78.88 cnf(15,plain,
% 78.67/78.88 (E(a1,f2(f2(f3(x151),f3(x152)),f2(x152,x151)))),
% 78.67/78.88 inference(scs_inference,[],[9,2])).
% 78.67/78.88 cnf(16,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(f2(f3(x161),f3(x162)),f2(x162,x161)))),
% 78.67/78.88 inference(scs_inference,[],[11,9,2,3])).
% 78.67/78.88 cnf(18,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(f2(x181,x182),f2(f2(x182,x183),f2(x181,x183))))),
% 78.67/78.88 inference(scs_inference,[],[11,10,2,3])).
% 78.67/78.88 cnf(19,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(a1,f2(a1,a1)))),
% 78.67/78.88 inference(scs_inference,[],[13,7,3])).
% 78.67/78.88 cnf(23,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(a1,f2(a1,f2(a1,a1))))),
% 78.67/78.88 inference(scs_inference,[],[19,7,3])).
% 78.67/78.88 cnf(26,plain,
% 78.67/78.88 (E(f2(f2(a1,x261),x262),f2(x261,x262))),
% 78.67/78.88 inference(scs_inference,[],[7,6,4])).
% 78.67/78.88 cnf(27,plain,
% 78.67/78.88 (E(f2(x271,f2(a1,x272)),f2(x271,x272))),
% 78.67/78.88 inference(scs_inference,[],[7,6,4,5])).
% 78.67/78.88 cnf(29,plain,
% 78.67/78.88 (~E(f2(a1,f2(a4,a4)),f2(a1,f2(a1,f2(a1,a1))))),
% 78.67/78.88 inference(scs_inference,[],[7,12,23,6,4,5,2,3])).
% 78.67/78.88 cnf(32,plain,
% 78.67/78.88 (E(f2(f2(f2(a1,x321),x322),x323),f2(f2(x321,x322),x323))),
% 78.67/78.88 inference(scs_inference,[],[26,6,4])).
% 78.67/78.88 cnf(33,plain,
% 78.67/78.88 (E(f2(x331,f2(f2(a1,x332),x333)),f2(x331,f2(x332,x333)))),
% 78.67/78.88 inference(scs_inference,[],[26,6,4,5])).
% 78.67/78.88 cnf(34,plain,
% 78.67/78.88 (~E(f2(f2(x341,x342),f2(f2(x342,x343),f2(x341,x343))),f2(a4,a4))),
% 78.67/78.88 inference(scs_inference,[],[26,18,6,4,5,2])).
% 78.67/78.88 cnf(38,plain,
% 78.67/78.88 (E(f2(f2(x381,f2(a1,x382)),x383),f2(f2(x381,x382),x383))),
% 78.67/78.88 inference(scs_inference,[],[27,6,4])).
% 78.67/78.88 cnf(40,plain,
% 78.67/78.88 (~E(f2(a1,f2(a1,f2(a1,a1))),f2(a1,f2(a4,a4)))),
% 78.67/78.88 inference(scs_inference,[],[27,29,6,4,5,2])).
% 78.67/78.88 cnf(50,plain,
% 78.67/78.88 (E(f2(a1,x501),f2(f2(f2(f3(x502),f3(x503)),f2(x503,x502)),x501))),
% 78.67/78.88 inference(scs_inference,[],[15,6,4])).
% 78.67/78.88 cnf(52,plain,
% 78.67/78.88 (~E(f2(f2(f3(x521),f3(x522)),f2(x522,x521)),f2(a4,a4))),
% 78.67/78.88 inference(scs_inference,[],[15,16,6,4,5,2])).
% 78.67/78.88 cnf(53,plain,
% 78.67/78.88 (~E(f2(a1,f2(a1,a1)),f2(a1,f2(a4,a4)))),
% 78.67/78.88 inference(scs_inference,[],[7,15,40,16,6,4,5,2,3])).
% 78.67/78.88 cnf(55,plain,
% 78.67/78.88 (E(f3(x551),f3(f2(a1,x551)))),
% 78.67/78.88 inference(scs_inference,[],[12,6])).
% 78.67/78.88 cnf(56,plain,
% 78.67/78.88 (E(f2(x561,x562),f2(f2(a1,x561),x562))),
% 78.67/78.88 inference(scs_inference,[],[12,6,4])).
% 78.67/78.88 cnf(57,plain,
% 78.67/78.88 (E(f2(x571,x572),f2(x571,f2(a1,x572)))),
% 78.67/78.88 inference(scs_inference,[],[12,6,4,5])).
% 78.67/78.88 cnf(58,plain,
% 78.67/78.88 (~E(f2(a1,f2(a4,a4)),f2(a1,f2(a1,a1)))),
% 78.67/78.88 inference(scs_inference,[],[53,12,6,4,5,2])).
% 78.67/78.88 cnf(59,plain,
% 78.67/78.88 (~E(f2(a1,a1),f2(a1,f2(a4,a4)))),
% 78.67/78.88 inference(scs_inference,[],[7,53,12,6,4,5,2,3])).
% 78.67/78.88 cnf(62,plain,
% 78.67/78.88 (E(f2(f2(x621,x622),x623),f2(f2(f2(a1,x621),x622),x623))),
% 78.67/78.88 inference(scs_inference,[],[56,6,4])).
% 78.67/78.88 cnf(63,plain,
% 78.67/78.88 (E(f2(x631,f2(x632,x633)),f2(x631,f2(f2(a1,x632),x633)))),
% 78.67/78.88 inference(scs_inference,[],[56,6,4,5])).
% 78.67/78.88 cnf(64,plain,
% 78.67/78.88 (~E(f2(a1,f2(a4,a4)),f2(a1,a1))),
% 78.67/78.88 inference(scs_inference,[],[56,59,6,4,5,2])).
% 78.67/78.88 cnf(65,plain,
% 78.67/78.88 (~E(a1,f2(a1,f2(a4,a4)))),
% 78.67/78.88 inference(scs_inference,[],[7,56,59,6,4,5,2,3])).
% 78.67/78.88 cnf(68,plain,
% 78.67/78.88 (E(f2(f2(x681,x682),x683),f2(f2(x681,f2(a1,x682)),x683))),
% 78.67/78.88 inference(scs_inference,[],[57,6,4])).
% 78.67/78.88 cnf(69,plain,
% 78.67/78.88 (E(f2(x691,f2(x692,x693)),f2(x691,f2(x692,f2(a1,x693))))),
% 78.67/78.88 inference(scs_inference,[],[57,6,4,5])).
% 78.67/78.88 cnf(70,plain,
% 78.67/78.88 (~E(f2(a1,f2(a4,a4)),a1)),
% 78.67/78.88 inference(scs_inference,[],[57,65,6,4,5,2])).
% 78.67/78.88 cnf(71,plain,
% 78.67/78.88 (~E(f2(a1,f2(a1,f2(a4,a4))),f2(a1,a1))),
% 78.67/78.88 inference(scs_inference,[],[64,57,65,6,4,5,2,3])).
% 78.67/78.88 cnf(76,plain,
% 78.67/78.88 (~E(f2(a1,a1),f2(a1,f2(a1,f2(a4,a4))))),
% 78.67/78.88 inference(scs_inference,[],[55,71,6,4,5,2])).
% 78.67/78.88 cnf(77,plain,
% 78.67/78.88 (~E(f2(f2(f3(x771),f3(f2(a1,x772))),f2(x772,x771)),f2(a4,a4))),
% 78.67/78.88 inference(scs_inference,[],[55,52,71,33,6,4,5,2,3])).
% 78.67/78.88 cnf(83,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(f2(f3(x831),f3(f2(a1,x832))),f2(x832,x831)))),
% 78.67/78.88 inference(scs_inference,[],[77,9,6,4,5,2])).
% 78.67/78.88 cnf(84,plain,
% 78.67/78.88 (~E(f2(f2(x841,x842),f2(f2(f2(a1,x842),x843),f2(x841,x843))),f2(a4,a4))),
% 78.67/78.88 inference(scs_inference,[],[34,77,38,9,6,4,5,2,3])).
% 78.67/78.88 cnf(87,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(f2(x871,x872),f2(f2(f2(a1,x872),x873),f2(x871,x873))))),
% 78.67/78.88 inference(scs_inference,[],[84,2])).
% 78.67/78.88 cnf(88,plain,
% 78.67/78.88 (~E(a1,f2(a1,f2(a1,f2(a4,a4))))),
% 78.67/78.88 inference(scs_inference,[],[7,76,84,2,3])).
% 78.67/78.88 cnf(90,plain,
% 78.67/78.88 (~E(f2(a1,f2(a1,f2(a4,a4))),a1)),
% 78.67/78.88 inference(scs_inference,[],[88,2])).
% 78.67/78.88 cnf(91,plain,
% 78.67/78.88 (~E(f2(f2(f2(a1,f3(x911)),f3(x912)),f2(x912,x911)),f2(a4,a4))),
% 78.67/78.88 inference(scs_inference,[],[88,62,52,2,3])).
% 78.67/78.88 cnf(93,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(f2(f2(a1,f3(x931)),f3(x932)),f2(x932,x931)))),
% 78.67/78.88 inference(scs_inference,[],[91,2])).
% 78.67/78.88 cnf(94,plain,
% 78.67/78.88 (~E(f2(a1,f2(f2(a1,a4),a4)),a1)),
% 78.67/78.88 inference(scs_inference,[],[70,91,63,2,3])).
% 78.67/78.88 cnf(97,plain,
% 78.67/78.88 (~E(f2(f2(x971,f2(a1,x972)),f2(f2(x972,x973),f2(x971,x973))),f2(a4,a4))),
% 78.67/78.88 inference(scs_inference,[],[94,68,34,2,3])).
% 78.67/78.88 cnf(99,plain,
% 78.67/78.88 (~E(f2(a4,a4),f2(f2(x991,f2(a1,x992)),f2(f2(x992,x993),f2(x991,x993))))),
% 78.67/78.88 inference(scs_inference,[],[97,2])).
% 78.67/78.88 cnf(100,plain,
% 78.67/78.88 (~E(f2(a1,f2(a4,f2(a1,a4))),f2(a1,f2(a1,a1)))),
% 78.67/78.88 inference(scs_inference,[],[58,97,69,2,3])).
% 78.67/78.88 cnf(103,plain,
% 78.67/78.88 (~E(f2(f2(f2(f3(x1031),f3(x1032)),f2(x1032,x1031)),f2(a1,f2(a4,a4))),a1)),
% 78.67/78.88 inference(scs_inference,[],[90,100,50,2,3])).
% 78.67/78.88 cnf(106,plain,
% 78.67/78.88 (~E(f2(f2(a1,a4),a4),f2(f2(f2(a1,f3(x1061)),f3(x1062)),f2(x1062,x1061)))),
% 78.67/78.88 inference(scs_inference,[],[93,103,56,2,3])).
% 78.67/78.88 cnf(108,plain,
% 78.67/78.88 (~E(f2(f2(f2(a1,f3(x1081)),f3(x1082)),f2(x1082,x1081)),f2(f2(a1,a4),a4))),
% 78.67/78.88 inference(scs_inference,[],[106,2])).
% 78.67/78.88 cnf(109,plain,
% 78.67/78.88 (~E(f2(f2(a4,a1),a1),f2(f2(f2(a1,f3(x1091)),f3(x1092)),f2(x1092,x1091)))),
% 78.67/78.88 inference(scs_inference,[],[8,106,2,3])).
% 78.67/78.88 cnf(112,plain,
% 78.67/78.88 (~E(f2(a1,f2(a4,a4)),f2(f2(f3(x1121),f3(f2(a1,x1122))),f2(x1122,x1121)))),
% 78.67/78.88 inference(scs_inference,[],[109,83,12,2,3])).
% 78.67/78.88 cnf(115,plain,
% 78.67/78.88 (~E(f2(f2(f3(x1151),f3(x1152)),f2(x1152,x1151)),f2(f2(a1,a4),a4))),
% 78.67/78.88 inference(scs_inference,[],[32,108,112,2,3])).
% 78.67/78.88 cnf(117,plain,
% 78.67/78.88 (~E(f2(f2(a1,a4),a4),f2(f2(f3(x1171),f3(x1172)),f2(x1172,x1171)))),
% 78.67/78.88 inference(scs_inference,[],[115,2])).
% 78.67/78.88 cnf(118,plain,
% 78.67/78.88 (~E(f2(f2(a1,a4),a4),f2(f2(x1181,x1182),f2(f2(f2(a1,x1182),x1183),f2(x1181,x1183))))),
% 78.67/78.88 inference(scs_inference,[],[115,87,56,2,3])).
% 78.67/78.88 cnf(121,plain,
% 78.67/78.88 (~E(f2(f2(a4,a1),a1),f2(f2(f3(x1211),f3(x1212)),f2(x1212,x1211)))),
% 78.67/78.88 inference(scs_inference,[],[8,117,118,2,3])).
% 78.67/78.88 cnf(124,plain,
% 78.67/78.88 (~E(f2(a4,f2(a1,a4)),f2(f2(x1241,f2(a1,x1242)),f2(f2(x1242,x1243),f2(x1241,x1243))))),
% 78.67/78.88 inference(scs_inference,[],[121,99,57,2,3])).
% 78.67/78.88 cnf(126,plain,
% 78.67/78.88 (~E(f2(f2(x1261,f2(a1,x1262)),f2(f2(x1262,x1263),f2(x1261,x1263))),f2(a4,f2(a1,a4)))),
% 78.67/78.88 inference(scs_inference,[],[124,2])).
% 78.67/78.88 cnf(673,plain,
% 78.67/78.88 (~E(f2(f2(x6731,f2(a1,a1)),f2(x6732,f2(x6731,x6732))),f2(a4,f2(a1,a4)))),
% 78.67/78.88 inference(scs_inference,[],[33,126,3])).
% 78.67/78.88 cnf(763,plain,
% 78.67/78.88 (~E(f2(f2(x7631,a1),f2(x7632,f2(x7631,x7632))),f2(a4,f2(a1,a4)))),
% 78.67/78.88 inference(scs_inference,[],[38,673,3])).
% 78.67/78.88 cnf(766,plain,
% 78.67/78.88 ($false),
% 78.67/78.88 inference(scs_inference,[],[763,26,7,3]),
% 78.67/78.88 ['proof']).
% 78.67/78.88 % SZS output end Proof
% 78.67/78.88 % Total time :78.376335s
%------------------------------------------------------------------------------