%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL086-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n027.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:37 AM UTC 2026
% Result : Unsatisfiable 253.12s 253.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL086-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.36 % Computer : n027.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 07:08:13 UTC 2026
% 0.14/0.37 % CPUTime :
% 0.25/0.53 start to proof:theBenchmark
% 252.99/253.02 %-------------------------------------------
% 252.99/253.02 % File :CSE---1.7
% 252.99/253.02 % Problem :theBenchmark
% 252.99/253.02 % Transform :cnf
% 252.99/253.02 % Format :tptp:raw
% 252.99/253.02 % Command :java -jar mcs_scs.jar %d %s
% 252.99/253.02
% 252.99/253.02 % Result :Theorem 252.502428s
% 252.99/253.02 % Output :CNFRefutation 252.502428s
% 252.99/253.02 %-------------------------------------------
% 252.99/253.02 %--------------------------------------------------------------------------
% 252.99/253.02 % File : LCL086-1 : TPTP v9.3.1. Released v1.0.0.
% 252.99/253.02 % Domain : Logic Calculi (Implicational propositional)
% 252.99/253.02 % Problem : IC-1 depends on the 4th Lukasiewicz axiom
% 252.99/253.02 % Version : [TPTP] axioms.
% 252.99/253.02 % English : Axiomatisations of the Implicational propositional calculus
% 252.99/253.02 % are {IC-2,IC-3,IC-4} by Tarski-Bernays and single Lukasiewicz
% 252.99/253.02 % axioms. Show that IC-1 depends on the fourth Lukasiewicz
% 252.99/253.02 % axiom.
% 252.99/253.02
% 252.99/253.02 % Refs : [Luk48] Lukasiewicz (1948), The Shortest Axiom of the Implicat
% 252.99/253.02 % : [Pfe88] Pfenning (1988), Single Axioms in the Implicational Pr
% 252.99/253.02 % Source : [TPTP]
% 252.99/253.02 % Names :
% 252.99/253.02
% 252.99/253.02 % Status : Unsatisfiable
% 252.99/253.02 % Rating : 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.17 v5.3.0, 0.20 v5.2.0, 0.08 v5.1.0, 0.19 v5.0.0, 0.20 v4.0.1, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.00 v2.3.0, 0.14 v2.2.1, 0.22 v2.1.0, 0.25 v2.0.0
% 252.99/253.02 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR)
% 252.99/253.02 % Number of literals : 5 ( 0 equ; 3 neg)
% 252.99/253.02 % Maximal clause size : 3 ( 1 avg)
% 252.99/253.03 % Maximal term depth : 5 ( 2 avg)
% 252.99/253.03 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 252.99/253.03 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty)
% 252.99/253.03 % Number of variables : 7 ( 2 sgn)
% 252.99/253.03 % SPC : CNF_UNS_RFO_NEQ_HRN
% 252.99/253.03
% 252.99/253.03 % Comments :
% 252.99/253.03 %--------------------------------------------------------------------------
% 252.99/253.03 cnf(condensed_detachment,axiom,
% 252.99/253.03 ( ~ is_a_theorem(implies(X,Y))
% 252.99/253.03 | ~ is_a_theorem(X)
% 252.99/253.03 | is_a_theorem(Y) ) ).
% 252.99/253.03
% 252.99/253.03 cnf(ic_JLukasiewicz_4,axiom,
% 252.99/253.03 is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(T,implies(implies(S,P),implies(R,P))))) ).
% 252.99/253.03
% 252.99/253.03 cnf(prove_ic_1,negated_conjecture,
% 252.99/253.03 ~ is_a_theorem(implies(a,a)) ).
% 253.12/253.03
% 253.12/253.03 %--------------------------------------------------------------------------
% 253.12/253.03 %-------------------------------------------
% 253.12/253.03 % Proof found
% 253.12/253.03 % SZS status Theorem for theBenchmark
% 253.12/253.03 % SZS output start Proof
% 253.12/253.03 %ClaNum:3(EqnAxiom:0)
% 253.12/253.03 %VarNum:13(SingletonVarNum:7)
% 253.12/253.03 %MaxLitNum:3
% 253.12/253.03 %MaxfuncDepth:4
% 253.12/253.03 %SharedTerms:3
% 253.12/253.03 %goalClause: 2
% 253.12/253.03 %singleGoalClaCount:1
% 253.12/253.03 [2]~P1(f1(a2,a2))
% 253.12/253.03 [1]P1(f1(f1(f1(x11,x12),f1(x13,x14)),f1(x15,f1(f1(x14,x11),f1(x13,x11)))))
% 253.12/253.03 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31))
% 253.12/253.03 %EqnAxiom
% 253.12/253.03
% 253.12/253.03 %-------------------------------------------
% 253.12/253.03 cnf(4,plain,
% 253.12/253.03 (P1(f1(x41,f1(f1(x42,x43),f1(x44,x43))))+~P1(f1(f1(x43,x45),f1(x44,x42)))),
% 253.12/253.03 inference(scs_inference,[],[1,3])).
% 253.12/253.03 cnf(6,plain,
% 253.12/253.03 (P1(f1(x61,f1(f1(f1(f1(x62,x63),f1(x64,x63)),f1(x63,x65)),f1(x66,f1(x63,x65)))))),
% 253.12/253.03 inference(scs_inference,[],[1,4])).
% 253.12/253.03 cnf(12,plain,
% 253.12/253.03 (P1(f1(x121,f1(f1(f1(x122,f1(x123,x124)),x125),f1(f1(f1(f1(x126,x123),f1(x127,x123)),f1(x123,x124)),x125))))),
% 253.12/253.03 inference(scs_inference,[],[6,4])).
% 253.12/253.03 cnf(15,plain,
% 253.12/253.03 (P1(f1(x151,f1(f1(f1(f1(f1(f1(x152,x153),f1(x154,x153)),f1(x153,x155)),x156),x157),f1(f1(f1(x158,f1(x153,x155)),x156),x157))))),
% 253.12/253.03 inference(scs_inference,[],[12,4])).
% 253.12/253.03 cnf(20,plain,
% 253.12/253.03 (P1(f1(x201,f1(f1(f1(f1(f1(x202,f1(x203,x204)),x205),x206),x207),f1(f1(f1(f1(f1(f1(x208,x203),f1(x209,x203)),f1(x203,x204)),x205),x206),x207))))),
% 253.12/253.03 inference(scs_inference,[],[15,4])).
% 253.12/253.03 cnf(29,plain,
% 253.12/253.03 (P1(f1(x291,f1(f1(f1(f1(f1(f1(f1(f1(x292,x293),f1(x294,x293)),f1(x293,x295)),x296),x297),x298),x299),f1(f1(f1(f1(f1(x2910,f1(x293,x295)),x296),x297),x298),x299))))),
% 253.12/253.03 inference(scs_inference,[],[20,4])).
% 253.12/253.03 cnf(34,plain,
% 253.12/253.03 (P1(f1(x341,f1(f1(f1(f1(f1(f1(f1(x342,f1(x343,x344)),x345),x346),x347),x348),x349),f1(f1(f1(f1(f1(f1(f1(f1(x3410,x343),f1(x3411,x343)),f1(x343,x344)),x345),x346),x347),x348),x349))))),
% 253.12/253.03 inference(scs_inference,[],[29,4])).
% 253.12/253.03 cnf(503,plain,
% 253.12/253.03 (~P1(f1(f1(x5031,f1(f1(f1(f1(f1(f1(f1(x5032,f1(x5033,x5034)),x5035),x5036),x5037),x5038),x5039),f1(f1(f1(f1(f1(f1(f1(f1(x50310,x5033),f1(x50311,x5033)),f1(x5033,x5034)),x5035),x5036),x5037),x5038),x5039))),f1(a2,a2)))),
% 253.12/253.03 inference(scs_inference,[],[34,2,3])).
% 253.12/253.03 cnf(505,plain,
% 253.12/253.03 (P1(f1(f1(f1(f1(x5051,x5052),f1(x5053,x5052)),f1(x5052,x5054)),f1(x5055,f1(x5052,x5054))))),
% 253.12/253.03 inference(scs_inference,[],[6,1,3])).
% 253.12/253.03 cnf(508,plain,
% 253.12/253.03 (P1(f1(x5081,f1(x5082,f1(f1(x5082,x5083),f1(x5084,x5083)))))),
% 253.12/253.03 inference(scs_inference,[],[505,1,3])).
% 253.12/253.03 cnf(512,plain,
% 253.12/253.03 (P1(f1(x5121,f1(f1(x5121,x5122),f1(x5123,x5122))))),
% 253.12/253.03 inference(scs_inference,[],[508,505,3])).
% 253.12/253.03 cnf(515,plain,
% 253.12/253.03 (P1(f1(x5151,f1(f1(f1(x5152,x5153),x5154),f1(f1(f1(x5154,x5155),x5153),x5154))))),
% 253.12/253.03 inference(scs_inference,[],[1,512,3])).
% 253.12/253.03 cnf(519,plain,
% 253.12/253.03 (P1(f1(f1(f1(x5191,x5192),x5193),f1(f1(f1(x5193,x5194),x5192),x5193)))),
% 253.12/253.03 inference(scs_inference,[],[1,515,3])).
% 253.12/253.03 cnf(522,plain,
% 253.12/253.03 (P1(f1(x5221,f1(f1(x5222,f1(x5223,x5224)),f1(f1(f1(x5222,x5225),x5224),f1(x5223,x5224)))))),
% 253.12/253.03 inference(scs_inference,[],[1,519,3])).
% 253.12/253.03 cnf(525,plain,
% 253.12/253.03 (P1(f1(f1(x5251,f1(x5252,x5253)),f1(f1(f1(x5251,x5254),x5253),f1(x5252,x5253))))),
% 253.12/253.03 inference(scs_inference,[],[1,522,3])).
% 253.12/253.03 cnf(528,plain,
% 253.12/253.03 (P1(f1(f1(f1(f1(f1(x5281,x5282),f1(x5283,x5284)),x5285),f1(f1(x5284,x5281),f1(x5283,x5281))),f1(x5286,f1(f1(x5284,x5281),f1(x5283,x5281)))))),
% 253.12/253.03 inference(scs_inference,[],[1,525,3])).
% 253.12/253.03 cnf(531,plain,
% 253.12/253.03 (P1(f1(x5311,f1(f1(f1(f1(f1(x5312,x5313),x5314),f1(x5315,x5314)),x5316),f1(f1(x5312,f1(x5315,x5314)),x5316))))),
% 253.12/253.03 inference(scs_inference,[],[1,522,3])).
% 253.12/253.03 cnf(535,plain,
% 253.12/253.03 (P1(f1(f1(f1(f1(f1(x5351,x5352),x5353),f1(x5354,x5353)),x5355),f1(f1(x5351,f1(x5354,x5353)),x5355)))),
% 253.12/253.03 inference(scs_inference,[],[1,531,3])).
% 253.12/253.03 cnf(538,plain,
% 253.12/253.03 (P1(f1(f1(x5381,f1(x5382,x5383)),f1(x5384,f1(f1(x5383,f1(x5381,x5385)),f1(x5382,f1(x5381,x5385))))))),
% 253.12/253.03 inference(scs_inference,[],[1,535,3])).
% 253.12/253.03 cnf(542,plain,
% 253.12/253.03 (P1(f1(x5421,f1(f1(x5422,f1(x5422,x5422)),f1(x5422,f1(x5422,x5422)))))),
% 253.12/253.03 inference(scs_inference,[],[528,535,3])).
% 253.12/253.03 cnf(546,plain,
% 253.12/253.03 (P1(f1(f1(x5461,f1(x5461,x5461)),f1(x5461,f1(x5461,x5461))))),
% 253.12/253.03 inference(scs_inference,[],[1,542,3])).
% 253.12/253.03 cnf(549,plain,
% 253.12/253.03 (P1(f1(x5491,f1(f1(f1(x5492,x5492),x5492),f1(x5492,x5492))))),
% 253.12/253.03 inference(scs_inference,[],[1,546,3])).
% 253.12/253.04 cnf(552,plain,
% 253.12/253.04 (P1(f1(f1(f1(x5521,x5521),x5521),f1(x5521,x5521)))),
% 253.12/253.04 inference(scs_inference,[],[1,549,3])).
% 253.12/253.04 cnf(555,plain,
% 253.12/253.04 (P1(f1(x5551,f1(f1(x5552,x5552),f1(x5552,x5552))))),
% 253.12/253.04 inference(scs_inference,[],[552,528,3])).
% 253.12/253.04 cnf(559,plain,
% 253.12/253.04 (P1(f1(f1(x5591,x5591),f1(x5591,x5591)))),
% 253.12/253.04 inference(scs_inference,[],[6,555,3])).
% 253.12/253.04 cnf(562,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(f1(f1(x5621,x5622),f1(x5623,x5622)),f1(x5622,x5624)),x5625),x5626),f1(f1(f1(x5627,f1(x5622,x5624)),x5625),x5626)))),
% 253.12/253.04 inference(scs_inference,[],[6,15,3])).
% 253.12/253.04 cnf(565,plain,
% 253.12/253.04 (P1(f1(x5651,f1(f1(x5652,f1(f1(x5652,x5652),x5653)),f1(x5652,f1(f1(x5652,x5652),x5653)))))),
% 253.12/253.04 inference(scs_inference,[],[559,538,3])).
% 253.12/253.04 cnf(569,plain,
% 253.12/253.04 (P1(f1(f1(x5691,f1(f1(x5691,x5691),x5692)),f1(x5691,f1(f1(x5691,x5691),x5692))))),
% 253.12/253.04 inference(scs_inference,[],[565,562,3])).
% 253.12/253.04 cnf(572,plain,
% 253.12/253.04 (P1(f1(f1(f1(x5721,f1(x5722,x5723)),x5724),f1(f1(f1(f1(x5725,x5722),f1(x5726,x5722)),f1(x5722,x5723)),x5724)))),
% 253.12/253.04 inference(scs_inference,[],[12,569,3])).
% 253.12/253.04 cnf(575,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(f1(x5751,f1(x5752,x5753)),x5754),x5755),x5754),f1(f1(f1(f1(x5756,x5752),f1(x5757,x5752)),f1(x5752,x5753)),x5754)))),
% 253.12/253.04 inference(scs_inference,[],[572,525,3])).
% 253.12/253.04 cnf(578,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(x5781,x5782),f1(x5783,x5782)),f1(x5782,x5784)),f1(x5785,f1(f1(x5784,x5786),f1(x5782,x5786)))))),
% 253.12/253.04 inference(scs_inference,[],[575,528,3])).
% 253.12/253.04 cnf(582,plain,
% 253.12/253.04 (P1(f1(x5821,f1(f1(f1(x5822,x5822),x5823),f1(f1(f1(x5822,x5822),x5822),x5823))))),
% 253.12/253.04 inference(scs_inference,[],[578,549,3])).
% 253.12/253.04 cnf(586,plain,
% 253.12/253.04 (P1(f1(f1(f1(x5861,x5861),x5862),f1(f1(f1(x5861,x5861),x5861),x5862)))),
% 253.12/253.04 inference(scs_inference,[],[582,552,3])).
% 253.12/253.04 cnf(589,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(f1(x5891,x5891),x5892),f1(f1(f1(x5891,x5891),x5891),x5892)),x5893),f1(x5894,x5893)))),
% 253.12/253.04 inference(scs_inference,[],[586,512,3])).
% 253.12/253.04 cnf(592,plain,
% 253.12/253.04 (P1(f1(x5921,f1(f1(f1(f1(f1(f1(x5922,x5922),x5922),x5923),x5924),x5923),f1(f1(f1(x5922,x5922),x5922),x5923))))),
% 253.12/253.04 inference(scs_inference,[],[589,519,3])).
% 253.12/253.04 cnf(596,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(f1(f1(x5961,x5961),x5961),x5962),x5963),x5962),f1(f1(f1(x5961,x5961),x5961),x5962)))),
% 253.12/253.04 inference(scs_inference,[],[592,559,3])).
% 253.12/253.04 cnf(599,plain,
% 253.12/253.04 (P1(f1(x5991,f1(f1(f1(f1(f1(x5992,x5992),x5993),x5994),x5993),f1(f1(f1(x5992,x5992),x5992),x5993))))),
% 253.12/253.04 inference(scs_inference,[],[589,525,3])).
% 253.12/253.04 cnf(603,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(f1(x6031,x6031),x6032),x6033),x6032),f1(f1(f1(x6031,x6031),x6031),x6032)))),
% 253.12/253.04 inference(scs_inference,[],[596,599,3])).
% 253.12/253.04 cnf(606,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(x6061,x6062),f1(x6061,x6062)),f1(x6061,x6062)),f1(x6063,f1(f1(x6062,x6061),f1(x6061,x6061)))))),
% 253.12/253.04 inference(scs_inference,[],[603,528,3])).
% 253.12/253.04 cnf(610,plain,
% 253.12/253.04 (P1(f1(x6101,f1(f1(f1(x6102,x6102),x6103),f1(f1(x6102,x6102),x6103))))),
% 253.12/253.04 inference(scs_inference,[],[555,578,3])).
% 253.12/253.04 cnf(614,plain,
% 253.12/253.04 (P1(f1(f1(f1(x6141,x6141),x6142),f1(f1(x6141,x6141),x6142)))),
% 253.12/253.04 inference(scs_inference,[],[606,610,3])).
% 253.12/253.04 cnf(617,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(f1(x6171,x6171),x6172),f1(f1(x6171,x6171),x6172)),x6173),f1(x6174,x6173)))),
% 253.12/253.04 inference(scs_inference,[],[614,512,3])).
% 253.12/253.04 cnf(635,plain,
% 253.12/253.04 (P1(f1(x6351,f1(f1(f1(x6352,x6352),x6353),f1(x6354,f1(f1(x6352,x6352),x6353)))))),
% 253.12/253.04 inference(scs_inference,[],[505,617,3])).
% 253.12/253.04 cnf(639,plain,
% 253.12/253.04 (P1(f1(f1(f1(x6391,x6391),x6392),f1(x6393,f1(f1(x6391,x6391),x6392))))),
% 253.12/253.04 inference(scs_inference,[],[505,635,3])).
% 253.12/253.04 cnf(691,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(f1(x6911,x6911),x6912),f1(x6913,f1(f1(x6911,x6911),x6912))),x6914),f1(x6915,x6914)))),
% 253.12/253.04 inference(scs_inference,[],[512,639,3])).
% 253.12/253.04 cnf(823,plain,
% 253.12/253.04 (P1(f1(x8231,f1(f1(f1(f1(x8232,x8232),x8233),f1(x8232,x8232)),f1(x8234,f1(x8232,x8232)))))),
% 253.12/253.04 inference(scs_inference,[],[528,691,3])).
% 253.12/253.04 cnf(827,plain,
% 253.12/253.04 (P1(f1(f1(f1(f1(x8271,x8271),x8272),f1(x8271,x8271)),f1(x8273,f1(x8271,x8271))))),
% 253.12/253.04 inference(scs_inference,[],[528,823,3])).
% 253.12/253.04 cnf(830,plain,
% 253.12/253.04 (P1(f1(x8301,f1(f1(x8302,x8303),f1(x8303,x8303))))),
% 253.12/253.04 inference(scs_inference,[],[528,827,3])).
% 253.12/253.04 cnf(834,plain,
% 253.12/253.04 (P1(f1(f1(x8341,x8342),f1(x8342,x8342)))),
% 253.12/253.04 inference(scs_inference,[],[528,830,3])).
% 253.12/253.04 cnf(1077,plain,
% 253.12/253.04 ($false),
% 253.12/253.04 inference(scs_inference,[],[575,503,834,3]),
% 253.12/253.04 ['proof']).
% 253.12/253.04 % SZS output end Proof
% 253.12/253.04 % Total time :252.502428s
%------------------------------------------------------------------------------