%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL096-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 : n006.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:37 AM UTC 2026
% Result : Unsatisfiable 80.23s 80.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL096-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.34 % Computer : n006.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 4 15:22:17 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.51 start to proof:theBenchmark
% 80.23/80.37 %-------------------------------------------
% 80.23/80.37 % File :CSE---1.7
% 80.23/80.37 % Problem :theBenchmark
% 80.23/80.37 % Transform :cnf
% 80.23/80.37 % Format :tptp:raw
% 80.23/80.37 % Command :java -jar mcs_scs.jar %d %s
% 80.23/80.37
% 80.23/80.37 % Result :Theorem 79.871881s
% 80.23/80.37 % Output :CNFRefutation 79.871881s
% 80.23/80.37 %-------------------------------------------
% 80.23/80.37 %--------------------------------------------------------------------------
% 80.23/80.37 % File : LCL096-1 : TPTP v9.3.1. Released v1.0.0.
% 80.23/80.37 % Domain : Logic Calculi (Left group)
% 80.23/80.37 % Problem : LG-1 depends on LG-2, LG-3, LG-4
% 80.23/80.37 % Version : [McC92b] axioms : Reduced > Complete.
% 80.23/80.37 % English : Axiomatisations of the left group calculus are {LG-1,
% 80.23/80.37 % LG-2,LG-3,LG-4,LG-5} by Kalman, {LG-2,LG-3}, {LG-2,P-1},
% 80.23/80.37 % {LG-2,P-4}, {LG-2,Q-1,Q-2}, {P-1,Q-3}, {P-4,Q-3}, {Q-1,
% 80.23/80.37 % Q-2,Q-3}, {Q-1,Q-3,Q-4}, {LG-27-1690} all by McCune. Show
% 80.23/80.37 % that LG-1 depends on a part of the Kalman system.
% 80.23/80.37
% 80.23/80.37 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 80.23/80.37 % : [McC92a] McCune (1992), Automated Discovery of New Axiomatisat
% 80.23/80.37 % : [McC92b] McCune (1992), Email to G. Sutcliffe
% 80.23/80.37 % Source : [McC92b]
% 80.23/80.37 % Names : LG-89 [MW92]
% 80.23/80.37
% 80.23/80.37 % Status : Unsatisfiable
% 80.23/80.37 % Rating : 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.10 v5.2.0, 0.15 v5.1.0, 0.06 v5.0.0, 0.13 v4.1.0, 0.07 v4.0.1, 0.00 v2.2.1, 0.11 v2.1.0, 0.13 v2.0.0
% 80.23/80.37 % Syntax : Number of clauses : 5 ( 4 unt; 0 nHn; 2 RR)
% 80.23/80.37 % Number of literals : 7 ( 0 equ; 3 neg)
% 80.23/80.37 % Maximal clause size : 3 ( 1 avg)
% 80.23/80.37 % Maximal term depth : 7 ( 2 avg)
% 80.23/80.37 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 80.23/80.37 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 80.23/80.37 % Number of variables : 16 ( 0 sgn)
% 80.23/80.37 % SPC : CNF_UNS_RFO_NEQ_HRN
% 80.23/80.37
% 80.23/80.37 % Comments :
% 80.23/80.37 %--------------------------------------------------------------------------
% 80.23/80.37 cnf(condensed_detachment,axiom,
% 80.23/80.37 ( ~ is_a_theorem(equivalent(X,Y))
% 80.23/80.37 | ~ is_a_theorem(X)
% 80.23/80.37 | is_a_theorem(Y) ) ).
% 80.23/80.37
% 80.23/80.37 cnf(lg_2,axiom,
% 80.23/80.37 is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Z)),equivalent(Y,Z)),U),U)) ).
% 80.23/80.37
% 80.23/80.37 cnf(lg_3,axiom,
% 80.23/80.38 is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Z)),U),equivalent(equivalent(Y,Z),U)),V),V)) ).
% 80.23/80.38
% 80.23/80.38 cnf(lg_4,axiom,
% 80.23/80.38 is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),Z),U),equivalent(equivalent(equivalent(X,V),Z),equivalent(equivalent(Y,V),U)))) ).
% 80.23/80.38
% 80.23/80.38 cnf(prove_lg_1,negated_conjecture,
% 80.23/80.38 ~ is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(equivalent(b,b),a)),c),c)) ).
% 80.23/80.38
% 80.23/80.38 %--------------------------------------------------------------------------
% 80.23/80.38 %-------------------------------------------
% 80.23/80.38 % Proof found
% 80.23/80.38 % SZS status Theorem for theBenchmark
% 80.23/80.38 % SZS output start Proof
% 80.23/80.38 %ClaNum:5(EqnAxiom:0)
% 80.23/80.38 %VarNum:32(SingletonVarNum:16)
% 80.23/80.38 %MaxLitNum:3
% 80.23/80.38 %MaxfuncDepth:5
% 80.23/80.38 %SharedTerms:9
% 80.23/80.38 %goalClause: 4
% 80.23/80.38 %singleGoalClaCount:1
% 80.23/80.38 [4]~P1(f1(f1(f1(a2,f1(f1(a3,a3),a2)),a4),a4))
% 80.23/80.38 [2]P1(f1(f1(f1(f1(f1(x21,x22),f1(x21,x23)),f1(x22,x23)),x24),x24))
% 80.23/80.38 [1]P1(f1(f1(f1(f1(x11,x12),x13),x14),f1(f1(f1(x11,x15),x13),f1(f1(x12,x15),x14))))
% 80.23/80.38 [3]P1(f1(f1(f1(f1(f1(f1(x31,x32),f1(x31,x33)),x34),f1(f1(x32,x33),x34)),x35),x35))
% 80.23/80.38 [5]P1(x51)+~P1(x52)+~P1(f1(x52,x51))
% 80.23/80.38 %EqnAxiom
% 80.23/80.38
% 80.23/80.38 %-------------------------------------------
% 80.23/80.38 cnf(6,plain,
% 80.23/80.38 (P1(f1(f1(f1(f1(f1(x61,x62),f1(x61,x63)),x64),x65),f1(f1(f1(x62,x63),x64),x65)))),
% 80.23/80.38 inference(scs_inference,[],[1,2,5])).
% 80.23/80.38 cnf(9,plain,
% 80.23/80.38 (P1(f1(f1(f1(f1(f1(x91,x92),f1(x91,x93)),x94),x95),f1(f1(x96,x94),f1(f1(f1(x92,x93),x96),x95))))),
% 80.23/80.38 inference(scs_inference,[],[1,6,5])).
% 80.23/80.38 cnf(12,plain,
% 80.23/80.38 (P1(f1(f1(f1(f1(f1(x121,x122),f1(x121,x123)),x124),x125),f1(f1(x126,x124),f1(f1(x127,x126),f1(f1(f1(x122,x123),x127),x125)))))),
% 80.23/80.38 inference(scs_inference,[],[1,9,5])).
% 80.23/80.38 cnf(15,plain,
% 80.23/80.38 (P1(f1(f1(x151,x152),f1(f1(x153,x151),f1(f1(f1(x154,x155),x153),f1(f1(f1(x156,x157),f1(x156,x155)),f1(f1(x154,x157),x152))))))),
% 80.23/80.38 inference(scs_inference,[],[1,12,5])).
% 80.23/80.38 cnf(22,plain,
% 80.23/80.38 (P1(f1(f1(x221,x222),f1(f1(f1(x223,x224),x221),f1(f1(f1(x225,x226),f1(x225,x224)),f1(f1(x223,x226),x222)))))),
% 80.23/80.38 inference(scs_inference,[],[1,9,5])).
% 80.23/80.38 cnf(30,plain,
% 80.23/80.38 (P1(f1(f1(f1(x301,x302),f1(f1(f1(x303,x304),x305),x306)),f1(f1(f1(x307,x308),f1(x307,x302)),f1(f1(x301,x308),f1(f1(f1(x303,x309),x305),f1(f1(x304,x309),x306))))))),
% 80.23/80.38 inference(scs_inference,[],[1,22,5])).
% 80.23/80.38 cnf(33,plain,
% 80.23/80.38 (P1(f1(f1(f1(x331,x332),f1(x331,x333)),f1(f1(f1(f1(x334,x335),x336),x332),f1(f1(f1(x334,x337),x336),f1(f1(x338,x337),f1(f1(x335,x338),x333))))))),
% 80.23/80.38 inference(scs_inference,[],[1,30,5])).
% 80.23/80.38 cnf(36,plain,
% 80.23/80.38 (P1(f1(f1(f1(f1(x361,x362),x363),x364),f1(f1(f1(x361,x365),x363),f1(f1(x366,x365),f1(f1(x362,x366),f1(f1(x367,x367),x364))))))),
% 80.23/80.38 inference(scs_inference,[],[1,33,5])).
% 80.23/80.38 cnf(49,plain,
% 80.23/80.38 (P1(f1(f1(x491,f1(f1(f1(f1(x492,x493),f1(x492,x494)),f1(x493,x494)),x495)),f1(f1(f1(x496,x497),x491),f1(f1(f1(x498,x499),f1(x498,x497)),f1(f1(x496,x499),x495)))))),
% 80.23/80.38 inference(scs_inference,[],[2,15,5])).
% 80.23/80.38 cnf(52,plain,
% 80.23/80.38 (P1(f1(f1(f1(x521,x522),f1(f1(f1(f1(x523,x524),f1(x523,x525)),f1(x524,x525)),f1(f1(f1(f1(x526,x527),f1(x526,x528)),f1(x527,x528)),x529))),f1(f1(f1(x5210,x5211),f1(x5210,x522)),f1(f1(x521,x5211),x529))))),
% 80.23/80.38 inference(scs_inference,[],[2,49,5])).
% 80.23/80.39 cnf(59,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(f1(x591,x592),f1(x591,x593)),x594),x595),f1(f1(x596,x594),f1(f1(f1(x592,x593),x596),f1(f1(x597,x597),x595)))))),
% 80.23/80.39 inference(scs_inference,[],[2,36,5])).
% 80.23/80.39 cnf(62,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(x621,x622),x623),f1(f1(f1(f1(x624,x625),f1(x624,x626)),f1(x625,x626)),x627)),f1(f1(f1(x621,x628),x623),f1(f1(x629,x628),f1(f1(x622,x629),x627)))))),
% 80.23/80.39 inference(scs_inference,[],[2,33,5])).
% 80.23/80.39 cnf(66,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(f1(x661,x662),f1(x661,x663)),x664),f1(f1(f1(f1(x665,x666),f1(x665,x667)),f1(x666,x667)),x668)),f1(f1(x669,x664),f1(f1(f1(x662,x663),x669),x668))))),
% 80.23/80.39 inference(scs_inference,[],[2,62,5])).
% 80.23/80.39 cnf(70,plain,
% 80.23/80.39 (P1(f1(f1(f1(x701,x702),f1(f1(f1(f1(x703,x704),f1(x703,x705)),f1(x704,x705)),x706)),f1(f1(f1(x707,x708),f1(x707,x702)),f1(f1(x701,x708),x706))))),
% 80.23/80.39 inference(scs_inference,[],[2,22,5])).
% 80.23/80.39 cnf(73,plain,
% 80.23/80.39 (P1(f1(f1(f1(x731,x732),f1(x731,f1(f1(f1(f1(x733,x734),f1(x733,x735)),f1(x734,x735)),x736))),f1(f1(f1(f1(f1(x737,x738),f1(x737,x739)),f1(x738,x739)),x732),x736)))),
% 80.23/80.39 inference(scs_inference,[],[2,70,5])).
% 80.23/80.39 cnf(77,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(f1(f1(x771,x772),f1(x771,x773)),x774),x775),x776),f1(f1(x777,x775),f1(f1(f1(f1(x772,x773),x774),x777),f1(f1(x778,x778),x776)))))),
% 80.23/80.39 inference(scs_inference,[],[3,36,5])).
% 80.23/80.39 cnf(80,plain,
% 80.23/80.39 (P1(f1(f1(x801,x802),f1(f1(f1(f1(f1(x803,x804),x805),f1(f1(x806,x804),f1(f1(x803,x806),x805))),x801),f1(f1(x807,x807),x802))))),
% 80.23/80.39 inference(scs_inference,[],[3,77,5])).
% 80.23/80.39 cnf(84,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(f1(x841,x842),x843),f1(f1(x844,x842),f1(f1(x841,x844),x843))),f1(f1(f1(f1(f1(x845,x846),f1(x845,x847)),x848),f1(f1(x846,x847),x848)),x849)),f1(f1(x8410,x8410),x849)))),
% 80.23/80.39 inference(scs_inference,[],[3,80,5])).
% 80.23/80.39 cnf(87,plain,
% 80.23/80.39 (P1(f1(f1(x871,x871),f1(f1(f1(f1(x872,x873),f1(x872,x874)),f1(f1(f1(x875,x876),f1(x875,x877)),x878)),f1(f1(x873,x874),f1(f1(x876,x877),x878)))))),
% 80.23/80.39 inference(scs_inference,[],[3,84,5])).
% 80.23/80.39 cnf(100,plain,
% 80.23/80.39 (P1(f1(f1(x1001,f1(f1(x1002,x1003),f1(x1002,x1004))),f1(f1(f1(x1003,x1004),x1001),f1(f1(f1(f1(x1005,x1006),f1(x1005,x1007)),x1008),f1(f1(x1006,x1007),x1008)))))),
% 80.23/80.39 inference(scs_inference,[],[87,66,5])).
% 80.23/80.39 cnf(112,plain,
% 80.23/80.39 (P1(f1(f1(f1(x1121,x1122),f1(x1121,x1123)),f1(f1(f1(f1(f1(x1124,f1(x1125,x1126)),f1(x1124,f1(x1125,x1127))),f1(x1126,x1127)),x1122),x1123)))),
% 80.23/80.39 inference(scs_inference,[],[6,70,5])).
% 80.23/80.39 cnf(142,plain,
% 80.23/80.39 (P1(f1(f1(f1(x1421,x1422),f1(x1421,x1423)),f1(f1(f1(f1(f1(x1424,x1425),f1(x1424,x1426)),x1427),x1422),f1(f1(f1(x1425,x1428),x1427),f1(f1(x1426,x1428),x1423)))))),
% 80.23/80.39 inference(scs_inference,[],[6,30,5])).
% 80.23/80.39 cnf(145,plain,
% 80.23/80.39 (P1(f1(f1(x1451,x1452),f1(f1(f1(f1(x1453,x1454),x1455),x1451),f1(f1(f1(x1456,x1454),f1(f1(x1453,x1456),x1455)),x1452))))),
% 80.23/80.39 inference(scs_inference,[],[6,9,5])).
% 80.23/80.39 cnf(175,plain,
% 80.23/80.39 (P1(f1(f1(f1(x1751,x1752),f1(x1751,f1(f1(x1753,f1(x1754,x1755)),f1(x1753,f1(x1754,x1756))))),f1(f1(f1(x1755,x1756),x1752),f1(f1(x1757,x1758),f1(x1757,x1758)))))),
% 80.23/80.39 inference(scs_inference,[],[52,100,5])).
% 80.23/80.39 cnf(182,plain,
% 80.23/80.39 (P1(f1(f1(f1(x1821,x1822),x1823),f1(f1(x1824,x1822),f1(f1(f1(f1(x1825,x1825),x1821),x1824),f1(f1(x1826,x1826),x1823)))))),
% 80.23/80.39 inference(scs_inference,[],[62,80,5])).
% 80.23/80.39 cnf(189,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(f1(x1891,x1892),f1(x1891,x1893)),f1(x1892,x1893)),x1894),f1(f1(x1895,x1895),x1894)))),
% 80.23/80.39 inference(scs_inference,[],[73,182,5])).
% 80.23/80.39 cnf(211,plain,
% 80.23/80.39 (P1(f1(f1(f1(x2111,x2112),f1(f1(f1(f1(x2113,x2114),f1(x2113,x2115)),f1(x2114,x2115)),f1(x2111,x2112))),f1(f1(f1(f1(x2116,x2117),f1(x2116,x2118)),x2119),f1(f1(x2117,x2118),x2119))))),
% 80.23/80.39 inference(scs_inference,[],[100,189,5])).
% 80.23/80.39 cnf(215,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(x2151,x2152),x2153),f1(f1(x2151,x2152),x2153)),f1(f1(x2154,x2155),f1(x2154,x2155))))),
% 80.23/80.39 inference(scs_inference,[],[175,59,5])).
% 80.23/80.39 cnf(223,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(x2231,x2232),f1(x2231,x2233)),x2234),f1(f1(x2232,x2233),x2234)))),
% 80.23/80.39 inference(scs_inference,[],[211,142,5])).
% 80.23/80.39 cnf(230,plain,
% 80.23/80.39 (P1(f1(f1(x2301,x2302),f1(f1(f1(f1(f1(x2303,f1(x2304,x2305)),f1(x2303,f1(x2304,x2306))),f1(x2305,x2306)),x2301),x2302)))),
% 80.23/80.39 inference(scs_inference,[],[112,223,5])).
% 80.23/80.39 cnf(253,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(x2531,x2532),x2533),f1(f1(f1(x2534,x2535),f1(x2534,x2536)),x2537)),f1(f1(f1(x2538,x2532),f1(f1(x2531,x2538),x2533)),f1(f1(x2535,x2536),x2537))))),
% 80.23/80.39 inference(scs_inference,[],[145,223,5])).
% 80.23/80.39 cnf(260,plain,
% 80.23/80.39 (P1(f1(f1(f1(x2601,x2602),f1(f1(f1(f1(x2603,f1(x2604,x2605)),f1(x2603,f1(x2604,x2606))),x2601),x2607)),f1(f1(f1(x2605,x2606),x2602),x2607)))),
% 80.23/80.39 inference(scs_inference,[],[230,253,5])).
% 80.23/80.39 cnf(308,plain,
% 80.23/80.39 (~P1(f1(f1(f1(f1(f1(x3081,x3082),x3083),f1(f1(x3081,x3082),x3083)),f1(f1(x3084,x3085),f1(x3084,x3085))),f1(f1(f1(a2,f1(f1(a3,a3),a2)),a4),a4)))),
% 80.23/80.39 inference(scs_inference,[],[215,4,5])).
% 80.23/80.39 cnf(466,plain,
% 80.23/80.39 (P1(f1(f1(f1(f1(f1(x4661,x4662),f1(x4661,x4663)),x4664),x4665),f1(f1(f1(x4662,x4663),x4664),f1(f1(x4666,x4666),x4665))))),
% 80.23/80.39 inference(scs_inference,[],[1,189,5])).
% 80.23/80.39 cnf(476,plain,
% 80.23/80.39 (P1(f1(f1(f1(x4761,x4762),f1(f1(x4763,x4761),x4764)),f1(f1(x4765,x4765),f1(f1(x4763,x4762),x4764))))),
% 80.23/80.39 inference(scs_inference,[],[2,466,5])).
% 80.23/80.39 cnf(480,plain,
% 80.23/80.39 (~P1(f1(f1(x4801,a4),f1(f1(f1(a2,f1(f1(a3,a3),a2)),x4801),a4)))),
% 80.23/80.39 inference(scs_inference,[],[476,308,5])).
% 80.23/80.39 cnf(559,plain,
% 80.23/80.39 ($false),
% 80.23/80.39 inference(scs_inference,[],[80,480,260,5]),
% 80.23/80.39 ['proof']).
% 80.23/80.39 % SZS output end Proof
% 80.23/80.39 % Total time :79.871881s
%------------------------------------------------------------------------------