%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL101-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n008.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:38 AM UTC 2026
% Result : Unsatisfiable 64.11s 64.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL101-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.10/0.35 % Computer : n008.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Fri Sep 4 15:29:38 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.26/0.52 start to proof:theBenchmark
% 64.11/64.32 %-------------------------------------------
% 64.11/64.32 % File :CSE---1.7
% 64.11/64.32 % Problem :theBenchmark
% 64.11/64.32 % Transform :cnf
% 64.11/64.32 % Format :tptp:raw
% 64.11/64.32 % Command :java -jar mcs_scs.jar %d %s
% 64.11/64.32
% 64.11/64.32 % Result :Theorem 63.726759s
% 64.11/64.32 % Output :CNFRefutation 63.726759s
% 64.11/64.32 %-------------------------------------------
% 64.11/64.32 %--------------------------------------------------------------------------
% 64.11/64.32 % File : LCL101-1 : TPTP v9.3.1. Released v1.0.0.
% 64.11/64.32 % Domain : Logic Calculi (Left group)
% 64.11/64.32 % Problem : P-1 depends on the 3rd McCune system
% 64.11/64.32 % Version : [McC92b] axioms.
% 64.11/64.32 % English : Axiomatisations of the left group calculus are {LG-1,
% 64.11/64.32 % LG-2,LG-3,LG-4,LG-5} by Kalman, {LG-2,LG-3}, {LG-2,P-1},
% 64.11/64.32 % {LG-2,P-4}, {LG-2,Q-1,Q-2}, {P-1,Q-3}, {P-4,Q-3}, {Q-1,
% 64.11/64.32 % Q-2,Q-3}, {Q-1,Q-3,Q-4}, {LG-27-1690} all by McCune. Show
% 64.11/64.32 % that P-1 depends on the 3rd McCune system.
% 64.11/64.32
% 64.11/64.32 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 64.11/64.32 % : [McC92a] McCune (1992), Automated Discovery of New Axiomatisat
% 64.11/64.32 % : [McC92b] McCune (1992), Email to G. Sutcliffe
% 64.11/64.32 % Source : [McC92b]
% 64.11/64.32 % Names : LG-94 [MW92]
% 64.11/64.32
% 64.11/64.32 % Status : Unsatisfiable
% 64.11/64.32 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.05 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v2.2.1, 0.11 v2.1.0, 0.13 v2.0.0
% 64.11/64.32 % Syntax : Number of clauses : 4 ( 3 unt; 0 nHn; 2 RR)
% 64.11/64.32 % Number of literals : 6 ( 0 equ; 3 neg)
% 64.11/64.32 % Maximal clause size : 3 ( 1 avg)
% 64.11/64.32 % Maximal term depth : 6 ( 2 avg)
% 64.11/64.32 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 64.11/64.32 % Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% 64.11/64.32 % Number of variables : 10 ( 0 sgn)
% 64.11/64.32 % SPC : CNF_UNS_RFO_NEQ_HRN
% 64.11/64.32
% 64.11/64.32 % Comments :
% 64.11/64.32 %--------------------------------------------------------------------------
% 64.11/64.32 cnf(condensed_detachment,axiom,
% 64.11/64.32 ( ~ is_a_theorem(equivalent(X,Y))
% 64.11/64.32 | ~ is_a_theorem(X)
% 64.11/64.32 | is_a_theorem(Y) ) ).
% 64.11/64.32
% 64.11/64.32 cnf(lg_2,axiom,
% 64.11/64.32 is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Z)),equivalent(Y,Z)),U),U)) ).
% 64.11/64.32
% 64.11/64.32 cnf(p_4,axiom,
% 64.11/64.32 is_a_theorem(equivalent(X,equivalent(equivalent(equivalent(equivalent(Y,Z),equivalent(Y,U)),equivalent(Z,U)),X))) ).
% 64.11/64.32
% 64.11/64.32 cnf(prove_p_1,negated_conjecture,
% 64.11/64.32 ~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(equivalent(e,b),equivalent(equivalent(a,e),c)))) ).
% 64.11/64.32
% 64.11/64.32 %--------------------------------------------------------------------------
% 64.11/64.32 %-------------------------------------------
% 64.11/64.33 % Proof found
% 64.11/64.33 % SZS status Theorem for theBenchmark
% 64.11/64.33 % SZS output start Proof
% 64.11/64.33 %ClaNum:4(EqnAxiom:0)
% 64.11/64.33 %VarNum:20(SingletonVarNum:10)
% 64.11/64.33 %MaxLitNum:3
% 64.11/64.33 %MaxfuncDepth:4
% 64.11/64.33 %SharedTerms:12
% 64.11/64.33 %goalClause: 3
% 64.11/64.33 %singleGoalClaCount:1
% 64.11/64.33 [3]~P1(f1(f1(f1(a2,a3),a4),f1(f1(a5,a3),f1(f1(a2,a5),a4))))
% 64.11/64.33 [1]P1(f1(x11,f1(f1(f1(f1(x12,x13),f1(x12,x14)),f1(x13,x14)),x11)))
% 64.11/64.33 [2]P1(f1(f1(f1(f1(f1(x21,x22),f1(x21,x23)),f1(x22,x23)),x24),x24))
% 64.11/64.33 [4]P1(x41)+~P1(x42)+~P1(f1(x42,x41))
% 64.11/64.33 %EqnAxiom
% 64.11/64.33
% 64.11/64.33 %-------------------------------------------
% 64.11/64.33 cnf(5,plain,
% 64.11/64.33 (P1(f1(f1(f1(f1(x51,x52),f1(x51,x53)),f1(x52,x53)),f1(f1(f1(x54,x55),f1(x54,x56)),f1(x55,x56))))),
% 64.11/64.33 inference(scs_inference,[],[2,1,4])).
% 64.11/64.33 cnf(11,plain,
% 64.11/64.33 (P1(f1(f1(f1(x111,x112),f1(x111,x113)),f1(x112,x113)))),
% 64.11/64.33 inference(scs_inference,[],[2,5,4])).
% 64.11/64.33 cnf(15,plain,
% 64.11/64.33 (P1(f1(f1(x151,x152),f1(x151,x152)))),
% 64.11/64.33 inference(scs_inference,[],[5,11,4])).
% 64.11/64.33 cnf(22,plain,
% 64.11/64.33 (P1(f1(x221,x221))),
% 64.11/64.33 inference(scs_inference,[],[15,11,4])).
% 64.11/64.33 cnf(26,plain,
% 64.11/64.33 (P1(f1(f1(f1(f1(x261,x262),f1(x261,x263)),f1(x262,x263)),f1(x264,x264)))),
% 64.11/64.33 inference(scs_inference,[],[22,1,4])).
% 64.11/64.33 cnf(29,plain,
% 64.11/64.33 (P1(f1(f1(x291,x292),f1(f1(x293,x291),f1(x293,x292))))),
% 64.11/64.33 inference(scs_inference,[],[11,26,4])).
% 64.11/64.33 cnf(33,plain,
% 64.11/64.33 (P1(f1(f1(x331,f1(f1(x332,x333),f1(x332,x334))),f1(x331,f1(x333,x334))))),
% 64.11/64.33 inference(scs_inference,[],[11,29,4])).
% 64.11/64.33 cnf(36,plain,
% 64.11/64.33 (P1(f1(f1(x361,f1(f1(f1(x362,x363),f1(x362,x364)),f1(x363,x364))),f1(x361,f1(x365,x365))))),
% 64.11/64.33 inference(scs_inference,[],[29,26,4])).
% 64.11/64.33 cnf(50,plain,
% 64.11/64.33 (P1(f1(f1(f1(x501,x502),f1(f1(f1(x503,x504),f1(x503,x505)),f1(x504,x505))),f1(x502,x501)))),
% 64.11/64.33 inference(scs_inference,[],[33,36,4])).
% 64.11/64.33 cnf(54,plain,
% 64.11/64.33 (P1(f1(f1(f1(x541,x542),f1(x541,x543)),f1(f1(x544,x542),f1(x544,x543))))),
% 64.11/64.33 inference(scs_inference,[],[50,33,4])).
% 64.11/64.33 cnf(62,plain,
% 64.11/64.33 (P1(f1(f1(x621,f1(x622,x623)),f1(x621,f1(f1(x624,x622),f1(x624,x623)))))),
% 64.11/64.33 inference(scs_inference,[],[54,26,4])).
% 64.11/64.33 cnf(77,plain,
% 64.11/64.33 (P1(f1(f1(f1(f1(f1(x771,x772),f1(x771,x773)),f1(x772,x773)),f1(x774,x775)),f1(f1(x776,x774),f1(x776,x775))))),
% 64.11/64.33 inference(scs_inference,[],[62,2,4])).
% 64.11/64.33 cnf(81,plain,
% 64.11/64.33 (P1(f1(x811,f1(f1(x812,f1(f1(f1(x813,x814),f1(x813,x815)),f1(x814,x815))),f1(x812,x811))))),
% 64.11/64.33 inference(scs_inference,[],[1,62,4])).
% 64.11/64.33 cnf(92,plain,
% 64.11/64.33 (P1(f1(f1(f1(f1(x921,x922),x923),f1(x922,x924)),f1(x923,f1(x921,x924))))),
% 64.11/64.33 inference(scs_inference,[],[33,62,4])).
% 64.11/64.33 cnf(103,plain,
% 64.11/64.33 (P1(f1(f1(x1031,x1032),f1(f1(f1(x1033,x1034),f1(x1033,x1031)),f1(x1034,x1032))))),
% 64.11/64.33 inference(scs_inference,[],[92,77,4])).
% 64.11/64.33 cnf(111,plain,
% 64.11/64.33 (P1(f1(f1(x1111,x1111),f1(x1112,x1112)))),
% 64.11/64.33 inference(scs_inference,[],[103,36,4])).
% 64.11/64.33 cnf(122,plain,
% 64.11/64.33 (P1(f1(f1(x1221,f1(x1222,x1223)),f1(f1(f1(x1222,x1224),x1221),f1(x1224,x1223))))),
% 64.11/64.33 inference(scs_inference,[],[92,5,4])).
% 64.11/64.33 cnf(142,plain,
% 64.11/64.33 (P1(f1(f1(f1(f1(x1421,x1422),f1(x1421,x1423)),f1(x1422,x1423)),f1(f1(x1424,x1424),f1(x1425,x1425))))),
% 64.11/64.33 inference(scs_inference,[],[1,111,4])).
% 64.11/64.33 cnf(145,plain,
% 64.11/64.33 (P1(f1(f1(x1451,f1(x1452,x1452)),f1(x1451,f1(x1453,x1453))))),
% 64.11/64.33 inference(scs_inference,[],[142,77,4])).
% 64.11/64.33 cnf(152,plain,
% 64.11/64.33 (P1(f1(f1(f1(x1521,x1522),f1(f1(x1523,x1521),f1(x1523,x1522))),f1(x1524,x1524)))),
% 64.11/64.33 inference(scs_inference,[],[33,145,4])).
% 64.11/64.33 cnf(160,plain,
% 64.11/64.33 (P1(f1(f1(f1(f1(x1601,x1602),x1603),f1(f1(x1604,x1602),f1(x1604,x1605))),f1(x1603,f1(x1601,x1605))))),
% 64.11/64.33 inference(scs_inference,[],[54,122,4])).
% 64.11/64.33 cnf(167,plain,
% 64.11/64.33 (P1(f1(f1(f1(x1671,x1672),x1673),f1(f1(f1(x1674,x1671),f1(x1674,x1672)),x1673)))),
% 64.11/64.33 inference(scs_inference,[],[160,77,4])).
% 64.11/64.33 cnf(174,plain,
% 64.11/64.33 (P1(f1(f1(f1(f1(f1(x1741,x1742),f1(x1741,x1743)),x1744),f1(f1(x1742,x1743),x1745)),f1(x1744,x1745)))),
% 64.11/64.33 inference(scs_inference,[],[122,167,4])).
% 64.11/64.33 cnf(178,plain,
% 64.11/64.33 (P1(f1(f1(f1(x1781,x1782),f1(f1(x1783,x1784),f1(f1(x1785,x1783),f1(x1785,x1784)))),f1(x1782,x1781)))),
% 64.11/64.33 inference(scs_inference,[],[122,152,4])).
% 64.11/64.33 cnf(188,plain,
% 64.11/64.33 (P1(f1(f1(f1(x1881,x1882),f1(f1(x1883,x1884),f1(x1883,x1885))),f1(f1(f1(x1886,x1881),f1(x1886,x1882)),f1(x1884,x1885))))),
% 64.11/64.33 inference(scs_inference,[],[174,178,4])).
% 64.11/64.33 cnf(240,plain,
% 64.11/64.33 (P1(f1(f1(f1(x2401,x2402),f1(x2401,x2403)),f1(f1(f1(f1(x2404,x2405),f1(x2404,x2406)),f1(x2405,x2406)),f1(x2402,x2403))))),
% 64.11/64.33 inference(scs_inference,[],[81,188,4])).
% 64.11/64.33 cnf(305,plain,
% 64.11/64.33 (P1(f1(f1(f1(x3051,f1(f1(x3052,x3053),f1(x3052,x3054))),f1(x3051,x3055)),f1(f1(x3053,x3054),x3055)))),
% 64.11/64.33 inference(scs_inference,[],[1,188,4])).
% 64.11/64.33 cnf(341,plain,
% 64.11/64.33 ($false),
% 64.11/64.33 inference(scs_inference,[],[240,305,3,4]),
% 64.11/64.33 ['proof']).
% 64.11/64.33 % SZS output end Proof
% 64.11/64.33 % Total time :63.726759s
%------------------------------------------------------------------------------