%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL055-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 : n010.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:34 AM UTC 2026
% Result : Unsatisfiable 97.74s 97.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL055-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.09/0.36 % Computer : n010.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.02/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Fri Sep 4 12:59:54 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.26/0.46 start to proof:theBenchmark
% 97.74/97.98 %-------------------------------------------
% 97.74/97.98 % File :CSE---1.7
% 97.74/97.98 % Problem :theBenchmark
% 97.74/97.98 % Transform :cnf
% 97.74/97.98 % Format :tptp:raw
% 97.74/97.98 % Command :java -jar mcs_scs.jar %d %s
% 97.74/97.98
% 97.74/97.98 % Result :Theorem 97.472832s
% 97.74/97.98 % Output :CNFRefutation 97.472832s
% 97.74/97.98 %-------------------------------------------
% 97.74/97.98 %--------------------------------------------------------------------------
% 97.74/97.98 % File : LCL055-1 : TPTP v9.3.1. Released v1.0.0.
% 97.74/97.98 % Domain : Logic Calculi (Implication/Negation 2 valued sentential)
% 97.74/97.98 % Problem : CN-37 depends on the Lukasiewicz system
% 97.74/97.98 % Version : [McC92] axioms.
% 97.74/97.98 % English : Axiomatisations of the Implication/Negation 2 valued
% 97.74/97.98 % sentential calculus are {CN-1,CN-2,CN-3} by Lukasiewicz,
% 97.74/97.98 % {CN-18,CN-21,CN-35,CN-39,CN-39,CN-40,CN-46} by Frege,
% 97.74/97.98 % {CN-3,CN-18,CN-21,CN-22,CN-30,CN-54} by Hilbert, {CN-18,
% 97.74/97.98 % CN-35,CN-49} by Church, {CN-19,CN-37,CN-59} by Lukasiewicz,
% 97.74/97.98 % {CN-19,CN-37,CN-60} by Wos, and the single Meredith axiom.
% 97.74/97.98 % Show that CN-37 depends on the short Lukasiewicz system.
% 97.74/97.98
% 97.74/97.98 % Refs : [Wos96] Wos (1996), The Power of Combining Resonance with Heat
% 97.74/97.99 % : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 97.74/97.99 % : [McC92] McCune (1992), Email to G. Sutcliffe
% 97.74/97.99 % Source : [McC92]
% 97.74/97.99 % Names : thesis_37 [Wos96]
% 97.74/97.99 % : CN-16 [MW92]
% 97.74/97.99
% 97.74/97.99 % Status : Unsatisfiable
% 97.74/97.99 % Rating : 0.00 v9.3.0, 0.12 v9.1.0, 0.13 v9.0.0, 0.00 v6.1.0, 0.14 v6.0.0, 0.00 v5.5.0, 0.25 v5.4.0, 0.33 v5.3.0, 0.40 v5.2.0, 0.15 v5.1.0, 0.31 v5.0.0, 0.20 v4.1.0, 0.33 v4.0.1, 0.00 v3.1.0, 0.17 v2.7.0, 0.38 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.00 v2.3.0, 0.14 v2.2.1, 0.56 v2.1.0, 0.88 v2.0.0
% 97.74/97.99 % Syntax : Number of clauses : 5 ( 4 unt; 0 nHn; 2 RR)
% 97.74/97.99 % Number of literals : 7 ( 0 equ; 3 neg)
% 97.74/97.99 % Maximal clause size : 3 ( 1 avg)
% 97.74/97.99 % Maximal term depth : 4 ( 2 avg)
% 97.74/97.99 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 97.74/97.99 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 97.74/97.99 % Number of variables : 8 ( 1 sgn)
% 97.74/97.99 % SPC : CNF_UNS_RFO_NEQ_HRN
% 97.74/97.99
% 97.74/97.99 % Comments :
% 97.74/97.99 %--------------------------------------------------------------------------
% 97.74/97.99 cnf(condensed_detachment,axiom,
% 97.74/97.99 ( ~ is_a_theorem(implies(X,Y))
% 97.74/97.99 | ~ is_a_theorem(X)
% 97.74/97.99 | is_a_theorem(Y) ) ).
% 97.74/97.99
% 97.74/97.99 cnf(cn_1,axiom,
% 97.74/97.99 is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
% 97.74/97.99
% 97.74/97.99 cnf(cn_2,axiom,
% 97.74/97.99 is_a_theorem(implies(implies(not(X),X),X)) ).
% 97.74/97.99
% 97.74/97.99 cnf(cn_3,axiom,
% 97.74/97.99 is_a_theorem(implies(X,implies(not(X),Y))) ).
% 97.74/97.99
% 97.74/97.99 cnf(prove_cn_37,negated_conjecture,
% 97.74/97.99 ~ is_a_theorem(implies(implies(implies(a,b),c),implies(not(a),c))) ).
% 97.74/97.99
% 97.74/97.99 %--------------------------------------------------------------------------
% 97.74/97.99 %-------------------------------------------
% 97.74/97.99 % Proof found
% 97.74/97.99 % SZS status Theorem for theBenchmark
% 97.74/97.99 % SZS output start Proof
% 97.74/97.99 %ClaNum:5(EqnAxiom:0)
% 97.74/97.99 %VarNum:16(SingletonVarNum:8)
% 97.74/97.99 %MaxLitNum:3
% 97.74/97.99 %MaxfuncDepth:3
% 97.74/97.99 %SharedTerms:9
% 97.74/97.99 %goalClause: 4
% 97.74/97.99 %singleGoalClaCount:1
% 97.74/97.99 [4]~P1(f2(f2(f2(a3,a4),a5),f2(f1(a3),a5)))
% 97.74/97.99 [2]P1(f2(f2(f1(x21),x21),x21))
% 97.74/97.99 [1]P1(f2(x11,f2(f1(x11),x12)))
% 97.74/97.99 [3]P1(f2(f2(x31,x32),f2(f2(x32,x33),f2(x31,x33))))
% 97.74/97.99 [5]P1(x51)+~P1(x52)+~P1(f2(x52,x51))
% 97.74/97.99 %EqnAxiom
% 97.74/97.99
% 97.74/97.99 %-------------------------------------------
% 97.74/97.99 cnf(6,plain,
% 97.74/97.99 (~P1(f2(f1(a3),f2(a3,a4)))),
% 97.74/97.99 inference(scs_inference,[],[4,3,5])).
% 97.74/97.99 cnf(29,plain,
% 97.74/97.99 (~P1(f2(f2(f2(f1(x291),x291),x291),f2(f1(a3),f2(a3,a4))))),
% 97.74/97.99 inference(scs_inference,[],[6,2,5])).
% 97.74/97.99 cnf(39,plain,
% 97.74/97.99 (P1(f2(f2(f2(f1(x391),x392),x393),f2(x391,x393)))),
% 97.74/97.99 inference(scs_inference,[],[3,1,5])).
% 97.74/97.99 cnf(43,plain,
% 97.74/97.99 (~P1(f2(f1(a3),f2(f1(f2(a3,a4)),f2(a3,a4))))),
% 97.74/97.99 inference(scs_inference,[],[29,3,5])).
% 97.74/97.99 cnf(49,plain,
% 97.74/97.99 (P1(f2(x491,x491))),
% 97.74/97.99 inference(scs_inference,[],[39,2,5])).
% 97.74/97.99 cnf(66,plain,
% 97.74/97.99 (P1(f2(x661,f2(f2(x662,x663),f2(f1(x661),x663))))),
% 97.74/97.99 inference(scs_inference,[],[39,3,5])).
% 97.74/97.99 cnf(73,plain,
% 97.74/97.99 (P1(f2(f2(x731,x732),f2(f1(f2(x733,x733)),x732)))),
% 97.74/97.99 inference(scs_inference,[],[66,49,5])).
% 97.74/97.99 cnf(82,plain,
% 97.74/97.99 (P1(f2(x821,f2(f1(f2(x822,x822)),x823)))),
% 97.74/97.99 inference(scs_inference,[],[39,73,5])).
% 97.74/97.99 cnf(91,plain,
% 97.74/97.99 (P1(f2(f2(f2(f1(f2(x911,x911)),x912),x913),f2(x914,x913)))),
% 97.74/97.99 inference(scs_inference,[],[82,3,5])).
% 97.74/97.99 cnf(96,plain,
% 97.74/97.99 (P1(f2(x961,f2(x962,x962)))),
% 97.74/97.99 inference(scs_inference,[],[91,2,5])).
% 97.74/97.99 cnf(136,plain,
% 97.74/97.99 (P1(f2(f2(f2(x1361,x1361),x1362),f2(x1363,x1362)))),
% 97.74/97.99 inference(scs_inference,[],[96,3,5])).
% 97.74/97.99 cnf(139,plain,
% 97.74/97.99 (P1(f2(x1391,f2(x1392,f2(f1(x1392),x1393))))),
% 97.74/97.99 inference(scs_inference,[],[136,39,5])).
% 97.74/97.99 cnf(155,plain,
% 97.74/97.99 (P1(f2(f2(f2(x1551,f2(f1(x1551),x1552)),x1553),f2(x1554,x1553)))),
% 97.74/97.99 inference(scs_inference,[],[139,3,5])).
% 97.74/97.99 cnf(173,plain,
% 97.74/97.99 (P1(f2(x1731,f2(f2(f2(f1(x1732),x1733),x1734),f2(x1732,x1734))))),
% 97.74/97.99 inference(scs_inference,[],[155,3,5])).
% 97.74/97.99 cnf(179,plain,
% 97.74/97.99 (P1(f2(f2(f2(f2(f2(f1(x1791),x1792),x1793),f2(x1791,x1793)),x1794),f2(x1795,x1794)))),
% 97.74/97.99 inference(scs_inference,[],[173,3,5])).
% 97.74/97.99 cnf(206,plain,
% 97.74/97.99 (P1(f2(f2(f2(x2061,x2062),x2063),f2(f2(f2(x2064,x2064),x2062),x2063)))),
% 97.74/97.99 inference(scs_inference,[],[136,3,5])).
% 97.74/97.99 cnf(284,plain,
% 97.74/97.99 (P1(f2(f2(f2(x2841,x2841),x2842),x2842))),
% 97.74/97.99 inference(scs_inference,[],[2,206,5])).
% 97.74/97.99 cnf(291,plain,
% 97.74/97.99 (P1(f2(f2(x2911,x2912),f2(f2(f1(x2911),x2911),x2912)))),
% 97.74/97.99 inference(scs_inference,[],[2,3,5])).
% 97.74/97.99 cnf(297,plain,
% 97.74/97.99 (P1(f2(f2(f1(f2(x2971,x2972)),f2(x2971,x2972)),f2(f2(x2972,x2973),f2(x2971,x2973))))),
% 97.74/97.99 inference(scs_inference,[],[3,291,5])).
% 97.74/97.99 cnf(300,plain,
% 97.74/97.99 (P1(f2(f2(f2(x3001,x3001),x3002),f2(f2(x3002,x3003),f2(x3004,x3003))))),
% 97.74/97.99 inference(scs_inference,[],[3,206,5])).
% 97.74/97.99 cnf(311,plain,
% 97.74/97.99 (P1(f2(f2(f2(x3111,x3111),f2(x3112,x3113)),f2(f2(x3113,x3114),f2(x3112,x3114))))),
% 97.74/97.99 inference(scs_inference,[],[297,206,5])).
% 97.74/97.99 cnf(317,plain,
% 97.74/97.99 (P1(f2(f2(f2(f2(x3171,x3172),f2(f1(x3173),x3172)),x3174),f2(x3173,x3174)))),
% 97.74/97.99 inference(scs_inference,[],[66,3,5])).
% 97.74/97.99 cnf(327,plain,
% 97.74/97.99 (P1(f2(f2(x3271,x3272),f2(f2(f2(x3273,x3273),x3271),x3272)))),
% 97.74/97.99 inference(scs_inference,[],[284,3,5])).
% 97.74/97.99 cnf(333,plain,
% 97.74/97.99 (P1(f2(f2(f2(f2(f1(x3331),x3331),x3331),x3332),f2(x3333,x3332)))),
% 97.74/97.99 inference(scs_inference,[],[291,300,5])).
% 97.74/97.99 cnf(361,plain,
% 97.74/97.99 (P1(f2(x3611,f2(f2(f2(f1(x3611),x3612),x3613),f2(x3614,x3613))))),
% 97.74/97.99 inference(scs_inference,[],[300,317,5])).
% 97.74/97.99 cnf(372,plain,
% 97.74/97.99 (P1(f2(f2(f2(x3721,x3721),f2(f2(x3722,x3722),f2(x3723,x3724))),f2(f2(x3724,x3725),f2(x3723,x3725))))),
% 97.74/97.99 inference(scs_inference,[],[311,327,5])).
% 97.74/97.99 cnf(425,plain,
% 97.74/98.00 (P1(f2(f2(f2(f2(f2(f1(x4251),x4252),x4253),f2(x4254,x4253)),x4255),f2(x4251,x4255)))),
% 97.74/98.00 inference(scs_inference,[],[361,3,5])).
% 97.74/98.00 cnf(458,plain,
% 97.74/98.00 (P1(f2(x4581,f2(x4582,f2(x4583,x4581))))),
% 97.74/98.00 inference(scs_inference,[],[333,425,5])).
% 97.74/98.00 cnf(466,plain,
% 97.74/98.00 (P1(f2(f2(f1(x4661),x4661),f2(x4662,f2(x4663,x4661))))),
% 97.74/98.00 inference(scs_inference,[],[458,291,5])).
% 97.74/98.00 cnf(472,plain,
% 97.74/98.00 (P1(f2(f2(f2(x4721,f2(x4722,x4723)),x4724),f2(x4723,x4724)))),
% 97.74/98.00 inference(scs_inference,[],[458,3,5])).
% 97.74/98.00 cnf(485,plain,
% 97.74/98.00 (P1(f2(x4851,f2(x4852,f2(x4853,f2(x4854,x4851)))))),
% 97.74/98.00 inference(scs_inference,[],[466,472,5])).
% 97.74/98.00 cnf(553,plain,
% 97.74/98.00 (P1(f2(f2(f2(x5531,f2(x5532,f2(x5533,x5534))),x5535),f2(x5534,x5535)))),
% 97.74/98.00 inference(scs_inference,[],[485,3,5])).
% 97.74/98.00 cnf(602,plain,
% 97.74/98.00 (P1(f2(x6021,f2(f2(x6021,x6022),f2(x6023,x6022))))),
% 97.74/98.00 inference(scs_inference,[],[372,553,5])).
% 97.74/98.00 cnf(744,plain,
% 97.74/98.00 (P1(f2(f2(f2(f2(x7441,x7442),f2(x7443,x7442)),x7444),f2(x7441,x7444)))),
% 97.74/98.00 inference(scs_inference,[],[602,3,5])).
% 97.74/98.00 cnf(830,plain,
% 97.74/98.00 (P1(f2(x8301,f2(f1(x8302),f2(x8302,f2(x8303,x8304)))))),
% 97.74/98.00 inference(scs_inference,[],[744,179,5])).
% 97.74/98.00 cnf(887,plain,
% 97.74/98.00 (P1(f2(f2(f2(x8871,f2(x8872,x8873)),x8874),f2(f1(x8871),x8874)))),
% 97.74/98.00 inference(scs_inference,[],[830,311,5])).
% 97.74/98.00 cnf(978,plain,
% 97.74/98.00 (P1(f2(f1(x9781),f2(f2(f2(x9782,x9783),x9784),f2(x9781,x9784))))),
% 97.74/98.00 inference(scs_inference,[],[3,887,5])).
% 97.74/98.00 cnf(982,plain,
% 97.74/98.00 (P1(f2(f2(f2(f2(f2(x9821,x9822),x9823),f2(x9824,x9823)),x9825),f2(f1(x9824),x9825)))),
% 97.74/98.00 inference(scs_inference,[],[3,978,5])).
% 97.74/98.00 cnf(1186,plain,
% 97.74/98.00 ($false),
% 97.74/98.00 inference(scs_inference,[],[333,43,982,5]),
% 97.74/98.00 ['proof']).
% 97.74/98.00 % SZS output end Proof
% 97.74/98.00 % Total time :97.472832s
%------------------------------------------------------------------------------