%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL108-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 : n029.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 0.41s 0.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL108-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.34 % Computer : n029.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 : Sat Sep 5 16:11:10 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.25/0.50 start to proof:theBenchmark
% 0.41/0.56 %-------------------------------------------
% 0.41/0.56 % File :CSE---1.7
% 0.41/0.56 % Problem :theBenchmark
% 0.41/0.56 % Transform :cnf
% 0.41/0.56 % Format :tptp:raw
% 0.41/0.56 % Command :java -jar mcs_scs.jar %d %s
% 0.41/0.56
% 0.41/0.56 % Result :Theorem 0.083889s
% 0.41/0.56 % Output :CNFRefutation 0.083889s
% 0.41/0.56 %-------------------------------------------
% 0.41/0.56 %--------------------------------------------------------------------------
% 0.41/0.56 % File : LCL108-1 : TPTP v9.3.1. Released v1.0.0.
% 0.41/0.56 % Domain : Logic Calculi (Left group)
% 0.41/0.56 % Problem : Q-3 depends on the single McCune axiom
% 0.41/0.56 % Version : [McC92b] axioms.
% 0.41/0.56 % English : Axiomatisations of the left group calculus are {LG-1,
% 0.41/0.56 % LG-2,LG-3,LG-4,LG-5} by Kalman, {LG-2,LG-3}, {LG-2,P-1},
% 0.41/0.56 % {LG-2,P-4}, {LG-2,Q-1,Q-2}, {P-1,Q-3}, {P-4,Q-3}, {Q-1,
% 0.41/0.56 % Q-2,Q-3}, {Q-1,Q-3,Q-4}, {LG-27-1690} all by McCune. Show
% 0.41/0.56 % that Q-3 depends on the single McCune axiom.
% 0.41/0.56
% 0.41/0.56 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 0.41/0.57 % : [McC92a] McCune (1992), Automated Discovery of New Axiomatisat
% 0.41/0.57 % : [McC92b] McCune (1992), Email to G. Sutcliffe
% 0.41/0.57 % Source : [McC92b]
% 0.41/0.57 % Names : LG-101 [MW92]
% 0.41/0.57
% 0.41/0.57 % Status : Unsatisfiable
% 0.41/0.57 % 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.07 v4.0.1, 0.00 v2.2.1, 0.11 v2.1.0, 0.25 v2.0.0
% 0.41/0.57 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR)
% 0.41/0.57 % Number of literals : 5 ( 0 equ; 3 neg)
% 0.41/0.57 % Maximal clause size : 3 ( 1 avg)
% 0.41/0.57 % Maximal term depth : 7 ( 2 avg)
% 0.41/0.57 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 0.41/0.57 % Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% 0.41/0.57 % Number of variables : 9 ( 0 sgn)
% 0.41/0.57 % SPC : CNF_UNS_RFO_NEQ_HRN
% 0.41/0.57
% 0.41/0.57 % Comments :
% 0.41/0.57 %--------------------------------------------------------------------------
% 0.41/0.57 cnf(condensed_detachment,axiom,
% 0.41/0.57 ( ~ is_a_theorem(equivalent(X,Y))
% 0.41/0.57 | ~ is_a_theorem(X)
% 0.41/0.57 | is_a_theorem(Y) ) ).
% 0.41/0.57
% 0.41/0.57 cnf(lg_27_1690,axiom,
% 0.41/0.57 is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),Z),equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),V6))),equivalent(Z,equivalent(equivalent(Y,X),V6)))) ).
% 0.41/0.57
% 0.41/0.57 cnf(prove_q_3,negated_conjecture,
% 0.41/0.57 ~ is_a_theorem(equivalent(equivalent(equivalent(a,b),equivalent(equivalent(b,a),c)),c)) ).
% 0.41/0.57
% 0.41/0.57 %--------------------------------------------------------------------------
% 0.41/0.57 %-------------------------------------------
% 0.41/0.57 % Proof found
% 0.41/0.57 % SZS status Theorem for theBenchmark
% 0.41/0.57 % SZS output start Proof
% 0.41/0.57 %ClaNum:3(EqnAxiom:0)
% 0.41/0.57 %VarNum:18(SingletonVarNum:9)
% 0.41/0.57 %MaxLitNum:3
% 0.41/0.57 %MaxfuncDepth:4
% 0.41/0.57 %SharedTerms:9
% 0.41/0.57 %goalClause: 2
% 0.41/0.57 %singleGoalClaCount:1
% 0.41/0.57 [2]~P1(f1(f1(f1(a2,a3),f1(f1(a3,a2),a4)),a4))
% 0.41/0.57 [1]P1(f1(f1(f1(f1(x11,x12),x13),f1(f1(x14,x15),f1(f1(f1(x16,x15),f1(x16,x14)),x17))),f1(x13,f1(f1(x12,x11),x17))))
% 0.41/0.57 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31))
% 0.41/0.57 %EqnAxiom
% 0.41/0.57
% 0.41/0.57 %-------------------------------------------
% 0.41/0.57 cnf(4,plain,
% 0.41/0.57 (P1(f1(x41,f1(f1(x42,x43),x44)))+~P1(f1(f1(f1(x43,x42),x41),f1(f1(x45,x46),f1(f1(f1(x47,x46),f1(x47,x45)),x44))))),
% 0.41/0.57 inference(scs_inference,[],[1,3])).
% 0.41/0.57 cnf(6,plain,
% 0.41/0.57 (P1(f1(f1(f1(x61,x62),f1(f1(f1(x63,x62),f1(x63,x61)),x64)),f1(f1(f1(x65,x66),f1(f1(x67,x65),f1(x67,x66))),x64)))),
% 0.41/0.57 inference(scs_inference,[],[1,4])).
% 0.41/0.57 cnf(7,plain,
% 0.41/0.57 (P1(f1(f1(f1(f1(x71,x72),x73),f1(f1(x74,x75),f1(f1(f1(x76,x75),f1(x76,x74)),x77))),f1(x73,f1(f1(x72,x71),x77))))),
% 0.41/0.57 inference(rename_variables,[],[1])).
% 0.41/0.57 cnf(9,plain,
% 0.41/0.57 (P1(f1(f1(f1(f1(x91,x92),f1(x91,x93)),f1(f1(f1(x94,f1(f1(x95,x96),f1(x95,x97))),f1(x94,f1(x96,x97))),x98)),f1(f1(x92,x93),x98)))),
% 0.41/0.57 inference(scs_inference,[],[1,7,4,3])).
% 0.41/0.57 cnf(12,plain,
% 0.41/0.57 (P1(f1(f1(f1(f1(x121,f1(f1(x122,x123),f1(x122,x124))),f1(x121,f1(x123,x124))),f1(f1(f1(x125,x126),f1(x125,x127)),x128)),f1(f1(f1(x129,x126),f1(x129,x127)),x128)))),
% 0.41/0.57 inference(scs_inference,[],[9,1,3])).
% 0.41/0.57 cnf(16,plain,
% 0.41/0.57 (P1(f1(f1(f1(x161,f1(x162,x163)),f1(x161,x164)),f1(f1(f1(x165,x162),f1(x165,x163)),x164)))),
% 0.41/0.57 inference(scs_inference,[],[12,9,3])).
% 0.41/0.57 cnf(21,plain,
% 0.41/0.57 (P1(f1(f1(f1(x211,f1(x212,x213)),f1(x211,x214)),f1(f1(f1(x215,x212),f1(x215,x213)),x214)))),
% 0.41/0.57 inference(rename_variables,[],[16])).
% 0.41/0.57 cnf(23,plain,
% 0.41/0.57 (P1(f1(f1(f1(x231,f1(f1(x232,f1(f1(x233,x234),f1(x233,x235))),f1(x232,f1(x234,x235)))),f1(x231,x236)),x236))),
% 0.41/0.57 inference(scs_inference,[],[16,21,6,4,3])).
% 0.41/0.57 cnf(30,plain,
% 0.41/0.57 (P1(f1(f1(f1(x301,x302),f1(x301,x303)),f1(x302,x303)))),
% 0.41/0.57 inference(scs_inference,[],[23,12,3])).
% 0.41/0.57 cnf(34,plain,
% 0.41/0.57 (P1(f1(f1(x341,f1(f1(f1(x342,x343),f1(x342,x344)),x345)),f1(f1(f1(x344,x343),x341),x345)))),
% 0.41/0.57 inference(scs_inference,[],[30,4])).
% 0.41/0.57 cnf(41,plain,
% 0.41/0.57 (P1(f1(f1(x411,f1(f1(f1(x412,x413),f1(x412,x414)),x415)),f1(f1(f1(x414,x413),x411),x415)))),
% 0.41/0.57 inference(rename_variables,[],[34])).
% 0.41/0.57 cnf(43,plain,
% 0.41/0.57 (~P1(f1(f1(f1(a3,a2),a4),f1(f1(f1(x431,a3),f1(x431,a2)),a4)))),
% 0.41/0.57 inference(scs_inference,[],[2,34,41,4,3])).
% 0.41/0.57 cnf(70,plain,
% 0.41/0.57 (P1(f1(f1(f1(x701,x702),f1(f1(x703,x701),f1(x703,x704))),f1(x702,x704)))),
% 0.41/0.57 inference(scs_inference,[],[6,23,3])).
% 0.41/0.57 cnf(75,plain,
% 0.41/0.57 (P1(f1(f1(f1(x751,x752),f1(f1(x753,x751),f1(x753,x754))),f1(x752,x754)))),
% 0.41/0.57 inference(rename_variables,[],[70])).
% 0.41/0.57 cnf(77,plain,
% 0.41/0.57 (P1(f1(f1(f1(f1(x771,f1(x772,x773)),f1(x771,f1(x772,x774))),f1(f1(x774,x773),x775)),x775))),
% 0.41/0.57 inference(scs_inference,[],[6,70,75,4,3])).
% 0.41/0.57 cnf(82,plain,
% 0.41/0.57 (P1(f1(x821,x821))),
% 0.41/0.57 inference(scs_inference,[],[30,77,3])).
% 0.41/0.57 cnf(87,plain,
% 0.41/0.57 (P1(f1(f1(f1(f1(x871,x872),f1(x871,x873)),x874),f1(f1(x872,x873),x874)))),
% 0.41/0.57 inference(scs_inference,[],[82,4])).
% 0.41/0.57 cnf(95,plain,
% 0.41/0.57 (P1(f1(f1(f1(f1(x951,x952),f1(x951,x953)),x954),f1(f1(x952,x953),x954)))),
% 0.41/0.57 inference(rename_variables,[],[87])).
% 0.41/0.57 cnf(97,plain,
% 0.41/0.57 ($false),
% 0.41/0.57 inference(scs_inference,[],[16,87,95,43,4,3]),
% 0.41/0.57 ['proof']).
% 0.41/0.57 % SZS output end Proof
% 0.41/0.57 % Total time :0.083889s
%------------------------------------------------------------------------------