%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL102-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 : n005.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 60.91s 61.04s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL102-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.07/0.35 % Computer : n005.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 17:51:50 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.25/0.52 start to proof:theBenchmark
% 60.91/61.04 %-------------------------------------------
% 60.91/61.04 % File :CSE---1.7
% 60.91/61.04 % Problem :theBenchmark
% 60.91/61.04 % Transform :cnf
% 60.91/61.04 % Format :tptp:raw
% 60.91/61.04 % Command :java -jar mcs_scs.jar %d %s
% 60.91/61.04
% 60.91/61.04 % Result :Theorem 60.514560s
% 60.91/61.04 % Output :CNFRefutation 60.514560s
% 60.91/61.04 %-------------------------------------------
% 60.91/61.04 %--------------------------------------------------------------------------
% 60.91/61.04 % File : LCL102-1 : TPTP v9.3.1. Released v1.0.0.
% 60.91/61.04 % Domain : Logic Calculi (Left group)
% 60.91/61.04 % Problem : P-1 depends on the 4th McCune system
% 60.91/61.04 % Version : [McC92b] axioms.
% 60.91/61.04 % English : Axiomatisations of the left group calculus are {LG-1,
% 60.91/61.04 % LG-2,LG-3,LG-4,LG-5} by Kalman, {LG-2,LG-3}, {LG-2,P-1},
% 60.91/61.04 % {LG-2,P-4}, {LG-2,Q-1,Q-2}, {P-1,Q-3}, {P-4,Q-3}, {Q-1,
% 60.91/61.04 % Q-2,Q-3}, {Q-1,Q-3,Q-4}, {LG-27-1690} all by McCune. Show
% 60.91/61.04 % that P-1 depends on the 4th McCune system.
% 60.91/61.04
% 60.91/61.04 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 60.91/61.04 % : [McC92a] McCune (1992), Automated Discovery of New Axiomatisat
% 60.91/61.04 % : [McC92b] McCune (1992), Email to G. Sutcliffe
% 60.91/61.04 % Source : [McC92b]
% 60.91/61.04 % Names : LG-95 [MW92]
% 60.91/61.04
% 60.91/61.04 % Status : Unsatisfiable
% 60.91/61.04 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.13 v4.1.0, 0.07 v4.0.1, 0.00 v2.4.0, 0.00 v2.2.1, 0.11 v2.1.0, 0.25 v2.0.0
% 60.91/61.04 % Syntax : Number of clauses : 5 ( 4 unt; 0 nHn; 2 RR)
% 60.91/61.04 % Number of literals : 7 ( 0 equ; 3 neg)
% 60.91/61.04 % Maximal clause size : 3 ( 1 avg)
% 60.91/61.04 % Maximal term depth : 6 ( 2 avg)
% 60.91/61.04 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 60.91/61.04 % Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% 60.91/61.04 % Number of variables : 12 ( 0 sgn)
% 60.91/61.04 % SPC : CNF_UNS_RFO_NEQ_HRN
% 60.91/61.04
% 60.91/61.04 % Comments :
% 60.91/61.04 %--------------------------------------------------------------------------
% 60.91/61.04 cnf(condensed_detachment,axiom,
% 60.91/61.04 ( ~ is_a_theorem(equivalent(X,Y))
% 60.91/61.04 | ~ is_a_theorem(X)
% 60.91/61.04 | is_a_theorem(Y) ) ).
% 60.91/61.04
% 60.91/61.04 cnf(lg_2,axiom,
% 60.91/61.04 is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Z)),equivalent(Y,Z)),U),U)) ).
% 60.91/61.04
% 60.91/61.04 cnf(q_1,axiom,
% 60.91/61.04 is_a_theorem(equivalent(X,equivalent(equivalent(Y,Z),equivalent(equivalent(Z,Y),X)))) ).
% 60.91/61.04
% 60.91/61.04 cnf(q_2,axiom,
% 60.91/61.04 is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(Z,X),equivalent(Z,Y)))) ).
% 60.91/61.04
% 60.91/61.04 cnf(prove_p_1,negated_conjecture,
% 60.91/61.04 ~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(equivalent(e,b),equivalent(equivalent(a,e),c)))) ).
% 60.91/61.04
% 60.91/61.04 %--------------------------------------------------------------------------
% 60.91/61.04 %-------------------------------------------
% 60.91/61.04 % Proof found
% 60.91/61.04 % SZS status Theorem for theBenchmark
% 60.91/61.04 % SZS output start Proof
% 60.91/61.04 %ClaNum:5(EqnAxiom:0)
% 60.91/61.04 %VarNum:24(SingletonVarNum:12)
% 60.91/61.04 %MaxLitNum:3
% 60.91/61.04 %MaxfuncDepth:4
% 60.91/61.04 %SharedTerms:12
% 60.91/61.04 %goalClause: 4
% 60.91/61.04 %singleGoalClaCount:1
% 60.91/61.04 [4]~P1(f1(f1(f1(a2,a3),a4),f1(f1(a5,a3),f1(f1(a2,a5),a4))))
% 60.91/61.04 [1]P1(f1(f1(x11,x12),f1(f1(x13,x11),f1(x13,x12))))
% 60.91/61.04 [2]P1(f1(x21,f1(f1(x22,x23),f1(f1(x23,x22),x21))))
% 60.91/61.04 [3]P1(f1(f1(f1(f1(f1(x31,x32),f1(x31,x33)),f1(x32,x33)),x34),x34))
% 60.91/61.05 [5]P1(x51)+~P1(x52)+~P1(f1(x52,x51))
% 60.91/61.05 %EqnAxiom
% 60.91/61.05
% 60.91/61.05 %-------------------------------------------
% 60.91/61.05 cnf(15,plain,
% 60.91/61.05 (P1(f1(f1(x151,x152),f1(x151,f1(f1(x153,x154),f1(f1(x154,x153),x152)))))),
% 60.91/61.05 inference(scs_inference,[],[2,1,5])).
% 60.91/61.05 cnf(21,plain,
% 60.91/61.05 (P1(f1(f1(f1(f1(f1(x211,x212),f1(x211,x213)),f1(x212,x213)),x214),f1(f1(x215,x216),f1(f1(x216,x215),x214))))),
% 60.91/61.05 inference(scs_inference,[],[3,15,5])).
% 60.91/61.05 cnf(30,plain,
% 60.91/61.05 (P1(f1(f1(x301,x302),f1(f1(x302,x301),f1(f1(x303,f1(f1(x304,x305),f1(x304,x306))),f1(x303,f1(x305,x306))))))),
% 60.91/61.05 inference(scs_inference,[],[1,21,5])).
% 60.91/61.05 cnf(34,plain,
% 60.91/61.05 (P1(f1(f1(f1(f1(x341,x342),f1(x341,x343)),f1(x342,x343)),f1(f1(x344,f1(f1(x345,x346),f1(x345,x347))),f1(x344,f1(x346,x347)))))),
% 60.91/61.05 inference(scs_inference,[],[1,30,5])).
% 60.91/61.05 cnf(63,plain,
% 60.91/61.05 (P1(f1(f1(f1(x631,x632),f1(f1(x633,x631),f1(x633,x632))),f1(f1(x634,f1(f1(x635,x636),f1(x635,x637))),f1(x634,f1(x636,x637)))))),
% 60.91/61.05 inference(scs_inference,[],[3,30,5])).
% 60.91/61.05 cnf(67,plain,
% 60.91/61.05 (P1(f1(f1(x671,f1(f1(x672,x673),f1(x672,x674))),f1(x671,f1(x673,x674))))),
% 60.91/61.05 inference(scs_inference,[],[63,34,5])).
% 60.91/61.05 cnf(71,plain,
% 60.91/61.05 (P1(f1(f1(f1(x711,x712),f1(f1(x713,x711),f1(x713,x712))),f1(f1(f1(x714,x715),f1(x714,x716)),f1(x715,x716))))),
% 60.91/61.05 inference(scs_inference,[],[67,63,5])).
% 60.91/61.05 cnf(75,plain,
% 60.91/61.05 (P1(f1(f1(f1(x751,x752),f1(x751,x753)),f1(x752,x753)))),
% 60.91/61.05 inference(scs_inference,[],[71,34,5])).
% 60.91/61.05 cnf(79,plain,
% 60.91/61.05 (P1(f1(x791,f1(f1(f1(x792,x793),f1(f1(x794,x792),f1(x794,x793))),x791)))),
% 60.91/61.05 inference(scs_inference,[],[21,75,5])).
% 60.91/61.05 cnf(83,plain,
% 60.91/61.05 (~P1(f1(f1(x831,f1(f1(a2,a3),a4)),f1(x831,f1(f1(a5,a3),f1(f1(a2,a5),a4)))))),
% 60.91/61.05 inference(scs_inference,[],[75,4,5])).
% 60.91/61.05 cnf(86,plain,
% 60.91/61.05 (P1(f1(f1(f1(x861,x862),x863),f1(f1(f1(x864,x861),f1(x864,x862)),x863)))),
% 60.91/61.05 inference(scs_inference,[],[79,67,5])).
% 60.91/61.05 cnf(102,plain,
% 60.91/61.05 (~P1(f1(f1(f1(a3,a5),f1(f1(a2,a3),a4)),f1(f1(a2,a5),a4)))),
% 60.91/61.05 inference(scs_inference,[],[83,15,5])).
% 60.91/61.05 cnf(108,plain,
% 60.91/61.05 ($false),
% 60.91/61.05 inference(scs_inference,[],[102,67,86,5]),
% 60.91/61.05 ['proof']).
% 60.91/61.05 % SZS output end Proof
% 60.91/61.05 % Total time :60.514560s
%------------------------------------------------------------------------------