%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL097-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 : n020.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.33s 60.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL097-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.08/0.35 % Computer : n020.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 : Sat Sep 5 18:48:12 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.23/0.51 start to proof:theBenchmark
% 60.33/60.52 %-------------------------------------------
% 60.33/60.52 % File :CSE---1.7
% 60.33/60.52 % Problem :theBenchmark
% 60.33/60.52 % Transform :cnf
% 60.33/60.52 % Format :tptp:raw
% 60.33/60.52 % Command :java -jar mcs_scs.jar %d %s
% 60.33/60.52
% 60.33/60.52 % Result :Theorem 59.991322s
% 60.33/60.52 % Output :CNFRefutation 59.991322s
% 60.33/60.52 %-------------------------------------------
% 60.33/60.52 %--------------------------------------------------------------------------
% 60.33/60.52 % File : LCL097-1 : TPTP v9.3.1. Released v1.0.0.
% 60.33/60.52 % Domain : Logic Calculi (Left group)
% 60.33/60.52 % Problem : LG-4 depends on LG-2, LG-3
% 60.33/60.52 % Version : [McC92b] axioms : Reduced > Complete.
% 60.33/60.52 % English : Axiomatisations of the left group calculus are {LG-1,
% 60.33/60.52 % LG-2,LG-3,LG-4,LG-5} by Kalman, {LG-2,LG-3}, {LG-2,P-1},
% 60.33/60.52 % {LG-2,P-4}, {LG-2,Q-1,Q-2}, {P-1,Q-3}, {P-4,Q-3}, {Q-1,
% 60.33/60.52 % Q-2,Q-3}, {Q-1,Q-3,Q-4}, {LG-27-1690} all by McCune. Show
% 60.33/60.52 % that LG-4 depends on a part of the Kalman system.
% 60.33/60.52
% 60.33/60.52 % Refs : [LM92] Lusk & McCune (1992), Experiments with ROO, a Parallel
% 60.33/60.52 % : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 60.33/60.52 % : [McC92a] McCune (1992), Automated Discovery of New Axiomatisat
% 60.33/60.52 % : [McC92b] McCune (1992), Email to G. Sutcliffe
% 60.33/60.52 % Source : [McC92b]
% 60.33/60.52 % Names : CD-90 [LM92]
% 60.33/60.52 % : LG-90 [MW92]
% 60.33/60.52
% 60.33/60.52 % Status : Unsatisfiable
% 60.33/60.52 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.15 v5.1.0, 0.12 v5.0.0, 0.13 v4.1.0, 0.07 v4.0.1, 0.00 v2.4.0, 0.14 v2.3.0, 0.14 v2.2.1, 0.22 v2.2.0, 0.33 v2.1.0, 0.25 v2.0.0
% 60.33/60.52 % Syntax : Number of clauses : 4 ( 3 unt; 0 nHn; 2 RR)
% 60.33/60.52 % Number of literals : 6 ( 0 equ; 3 neg)
% 60.33/60.52 % Maximal clause size : 3 ( 1 avg)
% 60.33/60.52 % Maximal term depth : 7 ( 2 avg)
% 60.33/60.52 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 60.33/60.52 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% 60.33/60.52 % Number of variables : 11 ( 0 sgn)
% 60.33/60.52 % SPC : CNF_UNS_RFO_NEQ_HRN
% 60.33/60.52
% 60.33/60.52 % Comments :
% 60.33/60.52 %--------------------------------------------------------------------------
% 60.33/60.52 cnf(condensed_detachment,axiom,
% 60.33/60.52 ( ~ is_a_theorem(equivalent(X,Y))
% 60.33/60.52 | ~ is_a_theorem(X)
% 60.33/60.52 | is_a_theorem(Y) ) ).
% 60.33/60.52
% 60.33/60.52 cnf(lg_2,axiom,
% 60.33/60.52 is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Z)),equivalent(Y,Z)),U),U)) ).
% 60.33/60.52
% 60.33/60.52 cnf(lg_3,axiom,
% 60.33/60.52 is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(X,Z)),U),equivalent(equivalent(Y,Z),U)),V),V)) ).
% 60.33/60.52
% 60.33/60.52 cnf(prove_lg_4,negated_conjecture,
% 60.33/60.52 ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(a,b),c),e),equivalent(equivalent(equivalent(a,falsehood),c),equivalent(equivalent(b,falsehood),e)))) ).
% 60.33/60.52
% 60.33/60.52 %--------------------------------------------------------------------------
% 60.33/60.52 %-------------------------------------------
% 60.33/60.52 % Proof found
% 60.33/60.52 % SZS status Theorem for theBenchmark
% 60.33/60.52 % SZS output start Proof
% 60.33/60.52 %ClaNum:4(EqnAxiom:0)
% 60.33/60.52 %VarNum:22(SingletonVarNum:11)
% 60.33/60.52 %MaxLitNum:3
% 60.33/60.52 %MaxfuncDepth:5
% 60.33/60.52 %SharedTerms:15
% 60.33/60.52 %goalClause: 3
% 60.33/60.52 %singleGoalClaCount:1
% 60.33/60.52 [3]~P1(f1(f1(f1(f1(a2,a3),a4),a5),f1(f1(f1(a2,a6),a4),f1(f1(a3,a6),a5))))
% 60.33/60.52 [1]P1(f1(f1(f1(f1(f1(x11,x12),f1(x11,x13)),f1(x12,x13)),x14),x14))
% 60.33/60.52 [2]P1(f1(f1(f1(f1(f1(f1(x21,x22),f1(x21,x23)),x24),f1(f1(x22,x23),x24)),x25),x25))
% 60.33/60.52 [4]P1(x41)+~P1(x42)+~P1(f1(x42,x41))
% 60.33/60.52 %EqnAxiom
% 60.33/60.52
% 60.33/60.52 %-------------------------------------------
% 60.33/60.53 cnf(5,plain,
% 60.33/60.53 (~P1(f1(f1(f1(f1(f1(x51,x52),f1(x51,x53)),x54),f1(f1(x52,x53),x54)),f1(f1(f1(f1(a2,a3),a4),a5),f1(f1(f1(a2,a6),a4),f1(f1(a3,a6),a5)))))),
% 60.33/60.53 inference(scs_inference,[],[2,3,4])).
% 60.33/60.53 cnf(16,plain,
% 60.33/60.53 (P1(f1(f1(x161,x162),f1(x161,x162)))),
% 60.33/60.53 inference(scs_inference,[],[2,1,4])).
% 60.33/60.53 cnf(20,plain,
% 60.33/60.53 (P1(f1(f1(f1(f1(x201,x202),f1(x201,x203)),x204),f1(f1(x202,x203),x204)))),
% 60.33/60.53 inference(scs_inference,[],[2,16,4])).
% 60.33/60.53 cnf(28,plain,
% 60.33/60.53 (P1(f1(f1(x281,x282),f1(f1(x283,x281),f1(x283,x282))))),
% 60.33/60.53 inference(scs_inference,[],[16,20,4])).
% 60.33/60.53 cnf(34,plain,
% 60.33/60.53 (P1(f1(f1(x341,f1(f1(f1(x342,x343),f1(x342,x344)),x345)),f1(x341,f1(f1(x343,x344),x345))))),
% 60.33/60.53 inference(scs_inference,[],[28,20,4])).
% 60.33/60.53 cnf(37,plain,
% 60.33/60.53 (~P1(f1(f1(f1(f1(f1(x371,x372),f1(x371,x373)),x374),f1(f1(x372,x373),x374)),f1(f1(f1(x375,f1(f1(a2,a3),a4)),f1(x375,a5)),f1(f1(f1(a2,a6),a4),f1(f1(a3,a6),a5)))))),
% 60.33/60.53 inference(scs_inference,[],[5,34,4])).
% 60.33/60.53 cnf(40,plain,
% 60.33/60.53 ($false),
% 60.33/60.53 inference(scs_inference,[],[37,34,28,4]),
% 60.33/60.53 ['proof']).
% 60.33/60.53 % SZS output end Proof
% 60.33/60.53 % Total time :59.991322s
%------------------------------------------------------------------------------