%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL121-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 : n027.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 137.76s 137.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL121-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.08/0.35 % Computer : n027.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 6 01:37:43 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.23/0.52 start to proof:theBenchmark
% 137.76/137.83 %-------------------------------------------
% 137.76/137.83 % File :CSE---1.7
% 137.76/137.83 % Problem :theBenchmark
% 137.76/137.83 % Transform :cnf
% 137.76/137.83 % Format :tptp:raw
% 137.76/137.83 % Command :java -jar mcs_scs.jar %d %s
% 137.76/137.83
% 137.76/137.83 % Result :Theorem 137.335012s
% 137.76/137.83 % Output :CNFRefutation 137.335012s
% 137.76/137.83 %-------------------------------------------
% 137.76/137.84 %--------------------------------------------------------------------------
% 137.76/137.84 % File : LCL121-1 : TPTP v9.3.1. Released v1.0.0.
% 137.76/137.84 % Domain : Logic Calculi (Right group)
% 137.76/137.84 % Problem : LG-1 depends on LG-2
% 137.76/137.84 % Version : [McC92b] axioms.
% 137.76/137.84 % English : Kalman's axiomatisation of the right group calculus
% 137.76/137.84 % is {LG-1,LG-2,LG-3,LG-4,LG-5}. McCune has shown that LG-2
% 137.76/137.84 % is a single axiom. Other axiomatisations by McCune are
% 137.76/137.84 % {Q-2,Q-3}, {Q-3,Q-4}, S-2, S-3, S-4, P-4, S-6. Show that LG-1
% 137.76/137.84 % depends on LG-2.
% 137.76/137.84
% 137.76/137.84 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 137.76/137.84 % : [McC92a] McCune (1992), Automated Discovery of New Axiomatisat
% 137.76/137.84 % : [McC92b] McCune (1992), Email to G. Sutcliffe
% 137.76/137.84 % Source : [McC92b]
% 137.76/137.84 % Names : RG-102 [MW92]
% 137.76/137.84
% 137.76/137.84 % Status : Unsatisfiable
% 137.76/137.84 % Rating : 0.00 v9.3.0, 0.06 v9.1.0, 0.00 v6.2.0, 0.17 v6.1.0, 0.29 v6.0.0, 0.11 v5.5.0, 0.31 v5.4.0, 0.33 v5.3.0, 0.45 v5.2.0, 0.15 v5.1.0, 0.31 v5.0.0, 0.33 v4.1.0, 0.40 v4.0.1, 0.00 v3.1.0, 0.17 v2.7.0, 0.38 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.00 v2.3.0, 0.29 v2.2.1, 0.78 v2.1.0, 0.75 v2.0.0
% 137.76/137.84 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR)
% 137.76/137.84 % Number of literals : 5 ( 0 equ; 3 neg)
% 137.76/137.84 % Maximal clause size : 3 ( 1 avg)
% 137.76/137.84 % Maximal term depth : 6 ( 2 avg)
% 137.76/137.84 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 137.76/137.84 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 137.76/137.84 % Number of variables : 6 ( 0 sgn)
% 137.76/137.84 % SPC : CNF_UNS_RFO_NEQ_HRN
% 137.76/137.84
% 137.76/137.84 % Comments :
% 137.76/137.84 %--------------------------------------------------------------------------
% 137.76/137.84 cnf(condensed_detachment,axiom,
% 137.76/137.84 ( ~ is_a_theorem(equivalent(X,Y))
% 137.76/137.84 | ~ is_a_theorem(X)
% 137.76/137.84 | is_a_theorem(Y) ) ).
% 137.76/137.84
% 137.76/137.84 cnf(lg_2,axiom,
% 137.76/137.84 is_a_theorem(equivalent(X,equivalent(X,equivalent(equivalent(Y,Z),equivalent(equivalent(Y,U),equivalent(Z,U)))))) ).
% 137.76/137.84
% 137.76/137.84 cnf(prove_lg_1,negated_conjecture,
% 137.76/137.84 ~ is_a_theorem(equivalent(a,equivalent(a,equivalent(equivalent(b,equivalent(c,c)),b)))) ).
% 137.76/137.84
% 137.76/137.84 %--------------------------------------------------------------------------
% 137.76/137.84 %-------------------------------------------
% 137.76/137.84 % Proof found
% 137.76/137.84 % SZS status Theorem for theBenchmark
% 137.76/137.84 % SZS output start Proof
% 137.76/137.84 %ClaNum:3(EqnAxiom:0)
% 137.76/137.84 %VarNum:12(SingletonVarNum:6)
% 137.76/137.84 %MaxLitNum:3
% 137.76/137.84 %MaxfuncDepth:5
% 137.76/137.84 %SharedTerms:9
% 137.76/137.84 %goalClause: 2
% 137.76/137.84 %singleGoalClaCount:1
% 137.76/137.84 [2]~P1(f1(a2,f1(a2,f1(f1(a3,f1(a4,a4)),a3))))
% 137.76/137.84 [1]P1(f1(x11,f1(x11,f1(f1(x12,x13),f1(f1(x12,x14),f1(x13,x14))))))
% 137.76/137.84 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31))
% 137.76/137.84 %EqnAxiom
% 137.76/137.84
% 137.76/137.84 %-------------------------------------------
% 137.76/137.84 cnf(4,plain,
% 137.76/137.84 (P1(f1(x41,f1(f1(x42,x43),f1(f1(x42,x44),f1(x43,x44)))))+~P1(x41)),
% 137.76/137.84 inference(scs_inference,[],[1,3])).
% 137.76/137.84 cnf(6,plain,
% 137.76/137.84 (P1(f1(f1(x61,f1(x61,f1(f1(x62,x63),f1(f1(x62,x64),f1(x63,x64))))),f1(f1(x65,x66),f1(f1(x65,x67),f1(x66,x67)))))),
% 137.76/137.84 inference(scs_inference,[],[1,4])).
% 137.76/137.84 cnf(8,plain,
% 137.76/137.84 (P1(f1(f1(x81,x82),f1(f1(x81,x83),f1(x82,x83))))),
% 137.76/137.84 inference(scs_inference,[],[1,4,3])).
% 137.76/137.84 cnf(9,plain,
% 137.76/137.84 (~P1(f1(x91,x92))+P1(x92)+~P1(x91)),
% 137.76/137.84 inference(rename_variables,[],[3])).
% 137.76/137.84 cnf(10,plain,
% 137.76/137.84 (P1(f1(f1(f1(x101,x102),f1(f1(x101,x103),f1(x102,x103))),f1(f1(x104,x105),f1(f1(x104,x106),f1(x105,x106)))))),
% 137.76/137.84 inference(scs_inference,[],[1,4,3,9])).
% 137.76/137.84 cnf(13,plain,
% 137.76/137.84 (P1(f1(f1(f1(f1(x131,x132),f1(f1(x131,x133),f1(x132,x133))),f1(f1(x134,x135),f1(f1(x134,x136),f1(x135,x136)))),f1(f1(x137,x138),f1(f1(x137,x139),f1(x138,x139)))))),
% 137.76/137.84 inference(scs_inference,[],[10,4])).
% 137.76/137.84 cnf(15,plain,
% 137.76/137.84 (P1(f1(f1(x151,x152),f1(f1(x151,f1(f1(x153,x154),f1(f1(x153,x155),f1(x154,x155)))),x152)))),
% 137.76/137.84 inference(scs_inference,[],[1,8,10,4,3])).
% 137.76/137.84 cnf(18,plain,
% 137.76/137.84 (P1(f1(f1(x181,f1(f1(x182,x183),f1(f1(x182,x184),f1(x183,x184)))),f1(x181,f1(f1(x185,x186),f1(f1(x185,x187),f1(x186,x187))))))),
% 137.76/137.84 inference(scs_inference,[],[1,15,3])).
% 137.76/137.84 cnf(21,plain,
% 137.76/137.84 (P1(f1(f1(f1(x211,x212),f1(f1(x213,x214),f1(f1(x213,x215),f1(x214,x215)))),f1(f1(x211,x216),f1(x212,x216))))),
% 137.76/137.84 inference(scs_inference,[],[8,15,3])).
% 137.76/137.84 cnf(24,plain,
% 137.76/137.84 (P1(f1(f1(f1(f1(x241,x242),f1(f1(x243,x244),f1(f1(x243,x245),f1(x244,x245)))),x246),f1(f1(f1(x241,x247),f1(x242,x247)),x246)))),
% 137.76/137.84 inference(scs_inference,[],[8,21,3])).
% 137.76/137.84 cnf(27,plain,
% 137.76/137.84 (P1(f1(f1(f1(x271,x272),f1(x273,x272)),f1(f1(f1(x271,x273),x274),f1(f1(f1(x275,x276),f1(f1(x275,x277),f1(x276,x277))),x274))))),
% 137.76/137.84 inference(scs_inference,[],[8,24,3])).
% 137.76/137.84 cnf(31,plain,
% 137.76/137.84 (P1(f1(f1(f1(f1(x311,x312),f1(f1(x311,x313),f1(x312,x313))),x314),f1(f1(f1(x315,x316),f1(f1(x315,x317),f1(x316,x317))),x314)))),
% 137.76/137.84 inference(scs_inference,[],[13,21,3])).
% 137.76/137.84 cnf(34,plain,
% 137.76/137.84 (P1(f1(f1(f1(x341,x342),f1(f1(x341,x343),f1(x342,x343))),f1(f1(f1(x344,x345),x346),f1(f1(f1(x344,x347),f1(x345,x347)),x346))))),
% 137.76/137.84 inference(scs_inference,[],[8,31,3])).
% 137.76/137.84 cnf(38,plain,
% 137.76/137.84 (P1(f1(f1(f1(x381,x382),x383),f1(f1(f1(x381,x384),f1(x382,x384)),x383)))),
% 137.76/137.85 inference(scs_inference,[],[8,34,3])).
% 137.76/137.85 cnf(41,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x411,x412),x413),f1(f1(f1(x411,x414),f1(x412,x414)),x413)),f1(f1(x415,x416),f1(f1(x415,x417),f1(x416,x417)))))),
% 137.76/137.85 inference(scs_inference,[],[8,34,3,4])).
% 137.76/137.85 cnf(43,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x431,x432),x433),x434),f1(f1(f1(f1(x431,x435),f1(x432,x435)),x433),x434)))),
% 137.76/137.85 inference(scs_inference,[],[8,38,3])).
% 137.76/137.85 cnf(46,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x461,x462),f1(x463,x462)),x464),f1(f1(f1(x461,x463),x465),f1(x464,x465))))),
% 137.76/137.85 inference(scs_inference,[],[8,43,3])).
% 137.76/137.85 cnf(52,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(f1(x521,x522),f1(x523,x522)),x524),x525),f1(f1(f1(f1(x521,x523),x526),f1(x524,x526)),x525)))),
% 137.76/137.85 inference(scs_inference,[],[8,46,3])).
% 137.76/137.85 cnf(57,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x571,x572),x573),f1(x574,x573)),f1(f1(f1(f1(x571,x575),f1(x572,x575)),x576),f1(x574,x576))))),
% 137.76/137.85 inference(scs_inference,[],[8,52,3])).
% 137.76/137.85 cnf(61,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(f1(x611,x612),x613),f1(x614,x613)),x615),f1(f1(f1(f1(f1(x611,x616),f1(x612,x616)),x617),f1(x614,x617)),x615)))),
% 137.76/137.85 inference(scs_inference,[],[8,57,3])).
% 137.76/137.85 cnf(64,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(f1(x641,x642),f1(x643,x642)),x644),f1(f1(f1(x641,x645),f1(x643,x645)),x644)),f1(f1(x646,x647),f1(f1(x646,x648),f1(x647,x648)))))),
% 137.76/137.85 inference(scs_inference,[],[41,61,3])).
% 137.76/137.85 cnf(67,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(f1(x671,x672),f1(x673,x672)),f1(f1(x671,x674),f1(x673,x674))),x675),f1(f1(f1(x676,x677),f1(f1(x676,x678),f1(x677,x678))),x675)))),
% 137.76/137.85 inference(scs_inference,[],[64,46,3])).
% 137.76/137.85 cnf(70,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x701,x702),f1(x703,x702)),x704),f1(f1(x701,x703),x704)))),
% 137.76/137.85 inference(scs_inference,[],[10,57,3])).
% 137.76/137.85 cnf(74,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(f1(x741,x742),f1(x743,x742)),x744),f1(f1(x741,x743),x744)),f1(f1(x745,x746),f1(f1(x745,x747),f1(x746,x747)))))),
% 137.76/137.85 inference(scs_inference,[],[10,57,3,4])).
% 137.76/137.85 cnf(76,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x761,x762),f1(x763,x762)),f1(x761,x763)),f1(f1(x764,x765),f1(f1(x764,x766),f1(x765,x766)))))),
% 137.76/137.85 inference(scs_inference,[],[70,74,3])).
% 137.76/137.85 cnf(83,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x831,x832),f1(x833,x832)),f1(f1(x831,x834),f1(x833,x834))),f1(f1(x835,x836),f1(f1(x835,x837),f1(x836,x837)))))),
% 137.76/137.85 inference(scs_inference,[],[10,43,3])).
% 137.76/137.85 cnf(86,plain,
% 137.76/137.85 (P1(f1(f1(f1(x861,x862),f1(x861,x862)),f1(f1(x863,x864),f1(f1(x863,x865),f1(x864,x865)))))),
% 137.76/137.85 inference(scs_inference,[],[83,70,3])).
% 137.76/137.85 cnf(90,plain,
% 137.76/137.85 (P1(f1(f1(x901,x901),f1(f1(x902,x903),f1(f1(x902,x904),f1(x903,x904)))))),
% 137.76/137.85 inference(scs_inference,[],[86,70,3])).
% 137.76/137.85 cnf(93,plain,
% 137.76/137.85 (P1(f1(f1(f1(x931,x931),x932),f1(f1(f1(x933,x934),f1(f1(x933,x935),f1(x934,x935))),x932)))),
% 137.76/137.85 inference(scs_inference,[],[90,46,3])).
% 137.76/137.85 cnf(101,plain,
% 137.76/137.85 (P1(f1(f1(f1(x1011,x1012),f1(f1(x1011,x1013),f1(x1012,x1013))),f1(f1(f1(x1014,x1015),f1(f1(x1014,x1016),f1(x1015,x1016))),f1(f1(f1(x1017,x1018),f1(x1019,x1018)),f1(f1(x1017,x10110),f1(x1019,x10110))))))),
% 137.76/137.85 inference(scs_inference,[],[67,93,3])).
% 137.76/137.85 cnf(105,plain,
% 137.76/137.85 (P1(f1(f1(f1(x1051,x1052),f1(f1(x1051,x1053),f1(x1052,x1053))),f1(f1(f1(x1054,x1055),f1(x1056,x1055)),f1(f1(x1054,x1057),f1(x1056,x1057)))))),
% 137.76/137.85 inference(scs_inference,[],[101,34,3])).
% 137.76/137.85 cnf(109,plain,
% 137.76/137.85 (P1(f1(f1(f1(x1091,x1092),f1(x1093,x1092)),f1(f1(x1091,x1094),f1(x1093,x1094))))),
% 137.76/137.85 inference(scs_inference,[],[105,101,3])).
% 137.76/137.85 cnf(113,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(f1(x1131,x1132),x1133),f1(f1(x1134,x1132),x1133)),x1135),f1(f1(x1131,x1134),x1135)))),
% 137.76/137.85 inference(scs_inference,[],[109,76,3])).
% 137.76/137.85 cnf(119,plain,
% 137.76/137.85 (P1(f1(f1(f1(x1191,x1192),f1(f1(x1191,x1193),f1(x1192,x1193))),f1(f1(x1194,x1195),f1(f1(f1(x1194,x1196),x1197),f1(f1(x1195,x1196),x1197)))))),
% 137.76/137.85 inference(scs_inference,[],[113,67,3])).
% 137.76/137.85 cnf(127,plain,
% 137.76/137.85 (P1(f1(f1(f1(x1271,x1272),f1(f1(f1(x1271,x1273),x1274),f1(f1(x1272,x1273),x1274))),f1(f1(x1275,x1276),f1(f1(x1275,x1277),f1(x1276,x1277)))))),
% 137.76/137.85 inference(scs_inference,[],[119,34,3,4])).
% 137.76/137.85 cnf(162,plain,
% 137.76/137.85 (P1(f1(f1(f1(x1621,x1622),f1(x1623,x1622)),f1(f1(x1621,f1(f1(x1624,x1625),f1(f1(x1624,x1626),f1(x1625,x1626)))),x1623)))),
% 137.76/137.85 inference(scs_inference,[],[15,38,3])).
% 137.76/137.85 cnf(194,plain,
% 137.76/137.85 (P1(f1(f1(x1941,f1(f1(x1942,x1943),f1(f1(x1942,x1944),f1(x1943,x1944)))),x1941))),
% 137.76/137.85 inference(scs_inference,[],[18,162,3])).
% 137.76/137.85 cnf(198,plain,
% 137.76/137.85 (~P1(f1(f1(a2,f1(a2,f1(f1(a3,f1(a4,a4)),a3))),f1(f1(x1981,x1982),f1(f1(x1981,x1983),f1(x1982,x1983)))))),
% 137.76/137.85 inference(scs_inference,[],[194,2,3])).
% 137.76/137.85 cnf(223,plain,
% 137.76/137.85 (P1(f1(f1(f1(x2231,x2232),f1(x2233,x2232)),f1(f1(x2231,x2233),f1(f1(x2234,x2235),f1(f1(x2234,x2236),f1(x2235,x2236))))))),
% 137.76/137.85 inference(scs_inference,[],[18,24,3])).
% 137.76/137.85 cnf(227,plain,
% 137.76/137.85 (~P1(f1(f1(a2,x2271),f1(f1(a2,f1(f1(a3,f1(a4,a4)),a3)),x2271)))),
% 137.76/137.85 inference(scs_inference,[],[223,198,3])).
% 137.76/137.85 cnf(292,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x2921,f1(x2922,x2923)),x2924),f1(x2925,x2924)),f1(f1(f1(x2921,x2926),f1(f1(f1(x2922,x2927),f1(x2923,x2927)),x2926)),x2925)))),
% 137.76/137.85 inference(scs_inference,[],[24,52,3])).
% 137.76/137.85 cnf(296,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(f1(x2961,x2962),f1(x2963,x2962)),x2964),f1(x2965,x2964)),f1(f1(f1(x2961,x2966),f1(x2963,x2966)),f1(x2965,f1(f1(x2967,x2968),f1(f1(x2967,x2969),f1(x2968,x2969)))))))),
% 137.76/137.85 inference(scs_inference,[],[24,61,3])).
% 137.76/137.85 cnf(388,plain,
% 137.76/137.85 (P1(f1(f1(f1(f1(x3881,f1(f1(x3882,x3883),f1(x3884,x3883))),f1(x3881,f1(x3882,x3884))),x3885),f1(f1(f1(x3886,x3887),f1(f1(x3886,x3888),f1(x3887,x3888))),x3885)))),
% 137.76/137.85 inference(scs_inference,[],[6,90,27,4,3])).
% 137.76/137.85 cnf(394,plain,
% 137.76/137.85 (P1(f1(f1(f1(x3941,x3942),f1(f1(x3941,x3943),f1(x3942,x3943))),f1(f1(f1(x3944,f1(f1(x3945,x3946),f1(x3947,x3946))),f1(f1(x3948,x3949),f1(f1(x3948,x39410),f1(x3949,x39410)))),f1(x3944,f1(x3945,x3947)))))),
% 137.76/137.85 inference(scs_inference,[],[15,105,388,4,3])).
% 137.76/137.85 cnf(400,plain,
% 137.76/137.85 (P1(f1(f1(f1(x4001,f1(f1(x4002,x4003),f1(x4004,x4003))),f1(f1(x4005,x4006),f1(f1(x4005,x4007),f1(x4006,x4007)))),f1(x4001,f1(x4002,x4004))))),
% 137.76/137.85 inference(scs_inference,[],[8,127,394,4,3])).
% 137.76/137.85 cnf(519,plain,
% 137.76/137.85 (~P1(f1(f1(f1(f1(a2,x5191),x5192),f1(f1(x5193,x5191),x5192)),f1(f1(a2,f1(f1(a3,f1(a4,a4)),a3)),x5193)))),
% 137.76/137.85 inference(scs_inference,[],[227,113,3])).
% 137.76/137.85 cnf(754,plain,
% 137.76/137.85 (~P1(f1(f1(f1(f1(a2,f1(x7541,x7542)),f1(x7543,x7541)),x7544),f1(f1(f1(a2,f1(f1(a3,f1(a4,a4)),a3)),f1(x7543,x7542)),x7544)))),
% 137.76/137.85 inference(scs_inference,[],[519,292,3])).
% 137.76/137.85 cnf(1138,plain,
% 137.76/137.85 ($false),
% 137.76/137.85 inference(scs_inference,[],[754,400,296,3]),
% 137.76/137.85 ['proof']).
% 137.76/137.85 % SZS output end Proof
% 137.76/137.85 % Total time :137.335012s
%------------------------------------------------------------------------------