%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL365+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n002.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:19:01 AM UTC 2026
% Result : Theorem 69.77s 70.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL365+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n002.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.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 5 23:55:21 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.24/0.52 start to proof:theBenchmark
% 69.77/69.99 %-------------------------------------------
% 69.77/69.99 % File :CSE---1.7
% 69.77/69.99 % Problem :theBenchmark
% 69.77/69.99 % Transform :cnf
% 69.77/69.99 % Format :tptp:raw
% 69.77/70.00 % Command :java -jar mcs_scs.jar %d %s
% 69.77/70.00
% 69.77/70.00 % Result :Theorem 69.476921s
% 69.77/70.00 % Output :CNFRefutation 69.476921s
% 69.77/70.00 %-------------------------------------------
% 69.77/70.00 %--------------------------------------------------------------------------
% 69.77/70.00 % File : LCL365+1 : TPTP v9.3.1. Released v9.1.0.
% 69.77/70.00 % Domain : Logic Calculi (Implication/Negation 2 valued sentential)
% 69.77/70.00 % Problem : CN-14 depends on the Lukasiewicz system
% 69.77/70.00 % Version : [Wos96] axioms.
% 69.77/70.00 % English : An axiomatisation of the Implication/Negation 2 valued
% 69.77/70.00 % sentential calculus is {CN-1,CN-2,CN-3} by Lukasiewicz.
% 69.77/70.00 % Show that CN-14 depends on the Lukasiewicz system.
% 69.77/70.00
% 69.77/70.00 % Refs : [Wos96] Wos (1996), Combining Resonance with Heat
% 69.77/70.00 % : [RW+23] Rawson et al. (2023), Lemmas: Generation, Selection, A
% 69.77/70.00 % Source : [Wos96]
% 69.77/70.00 % Names : thesis_14 [Wos96]
% 69.77/70.00
% 69.77/70.00 % Status : Theorem
% 69.77/70.00 % Rating : 0.60 v9.3.0, 0.35 v9.1.0
% 69.77/70.00 % Syntax : Number of formulae : 5 ( 4 unt; 0 def)
% 69.77/70.00 % Number of atoms : 7 ( 0 equ)
% 69.77/70.00 % Maximal formula atoms : 3 ( 1 avg)
% 69.77/70.00 % Number of connectives : 2 ( 0 ~; 0 |; 1 &)
% 69.77/70.00 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 69.77/70.00 % Maximal formula depth : 5 ( 3 avg)
% 69.77/70.00 % Maximal term depth : 6 ( 2 avg)
% 69.77/70.00 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 69.77/70.00 % Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% 69.77/70.00 % Number of variables : 8 ( 8 !; 0 ?)
% 69.77/70.00 % SPC : FOF_THM_RFO_NEQ
% 69.77/70.00
% 69.77/70.00 % Comments :
% 69.77/70.00 %--------------------------------------------------------------------------
% 69.77/70.00 fof(condensed_detachment,axiom,
% 69.77/70.00 ! [X,Y] :
% 69.77/70.00 ( ( is_a_theorem(implies(X,Y))
% 69.77/70.00 & is_a_theorem(X) )
% 69.77/70.00 => is_a_theorem(Y) ) ).
% 69.77/70.00
% 69.77/70.00 fof(cn_1,axiom,
% 69.77/70.00 ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
% 69.77/70.00
% 69.77/70.00 fof(cn_2,axiom,
% 69.77/70.00 ! [X] : is_a_theorem(implies(implies(not(X),X),X)) ).
% 69.77/70.00
% 69.77/70.00 fof(cn_3,axiom,
% 69.77/70.00 ! [X,Y] : is_a_theorem(implies(X,implies(not(X),Y))) ).
% 69.77/70.00
% 69.77/70.00 fof(prove_cn_14,conjecture,
% 69.77/70.00 is_a_theorem(implies(implies(implies(x,implies(implies(y,z),z)),u),implies(implies(not(z),y),u))) ).
% 69.77/70.00
% 69.77/70.00 %--------------------------------------------------------------------------
% 69.77/70.00 %-------------------------------------------
% 69.77/70.00 % Proof found
% 69.77/70.00 % SZS status Theorem for theBenchmark
% 69.77/70.00 % SZS output start Proof
% 69.77/70.00 %ClaNum:5(EqnAxiom:0)
% 69.77/70.00 %VarNum:16(SingletonVarNum:8)
% 69.77/70.00 %MaxLitNum:3
% 69.77/70.00 %MaxfuncDepth:4
% 69.77/70.00 %SharedTerms:13
% 69.77/70.00 %goalClause: 4
% 69.77/70.00 %singleGoalClaCount:1
% 69.77/70.00 [4]~P1(f2(f2(f2(a3,f2(f2(a5,a6),a6)),a4),f2(f2(f1(a6),a5),a4)))
% 69.77/70.00 [2]P1(f2(f2(f1(x21),x21),x21))
% 69.77/70.00 [1]P1(f2(x11,f2(f1(x11),x12)))
% 69.77/70.00 [3]P1(f2(f2(x31,x32),f2(f2(x32,x33),f2(x31,x33))))
% 69.77/70.00 [5]P1(x51)+~P1(x52)+~P1(f2(x52,x51))
% 69.77/70.00 %EqnAxiom
% 69.77/70.00
% 69.77/70.00 %-------------------------------------------
% 69.77/70.01 cnf(6,plain,
% 69.77/70.01 (~P1(f2(f2(f1(a6),a5),f2(a3,f2(f2(a5,a6),a6))))),
% 69.77/70.01 inference(scs_inference,[],[4,3,5])).
% 69.77/70.01 cnf(9,plain,
% 69.77/70.01 (P1(f2(f1(f2(f2(f1(x91),x91),x91)),x92))),
% 69.77/70.01 inference(scs_inference,[],[2,1,5])).
% 69.77/70.01 cnf(15,plain,
% 69.77/70.01 (P1(f2(f1(f2(f2(x151,x152),f2(f2(x152,x153),f2(x151,x153)))),x154))),
% 69.77/70.01 inference(scs_inference,[],[3,1,5])).
% 69.77/70.01 cnf(35,plain,
% 69.77/70.01 (P1(f2(f2(x351,x352),f2(f2(f1(x351),x351),x352)))),
% 69.77/70.01 inference(scs_inference,[],[2,3,5])).
% 69.77/70.01 cnf(39,plain,
% 69.77/70.01 (P1(f2(f1(f2(f2(x391,x392),f2(f2(f1(x391),x391),x392))),x393))),
% 69.77/70.01 inference(scs_inference,[],[35,1,5])).
% 69.77/70.01 cnf(42,plain,
% 69.77/70.01 (P1(f2(f2(f2(f2(f1(x421),x421),x422),x423),f2(f2(x421,x422),x423)))),
% 69.77/70.01 inference(scs_inference,[],[35,3,5])).
% 69.77/70.01 cnf(76,plain,
% 69.77/70.01 (P1(f2(f2(x761,x762),f2(f1(f2(f2(f1(x761),x761),x762)),x763)))),
% 69.77/70.01 inference(scs_inference,[],[42,1,5])).
% 69.77/70.01 cnf(80,plain,
% 69.77/70.01 (P1(f2(f2(x801,x802),f2(f2(x802,x803),f2(f2(f1(x801),x801),x803))))),
% 69.77/70.01 inference(scs_inference,[],[42,3,5])).
% 69.77/70.01 cnf(94,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(x941,x942)),f2(x941,x942)),f2(f2(x942,x943),f2(f2(f1(x941),x941),x943))))),
% 69.77/70.01 inference(scs_inference,[],[80,35,5])).
% 69.77/70.01 cnf(97,plain,
% 69.77/70.01 (P1(f2(f2(f2(f2(x971,x972),f2(x973,x972)),x974),f2(f2(f1(f2(x973,x971)),f2(x973,x971)),x974)))),
% 69.77/70.01 inference(scs_inference,[],[94,15,5])).
% 69.77/70.01 cnf(101,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(x1011,x1012)),f2(x1011,x1012)),f2(f1(f2(f2(x1012,x1013),f2(x1011,x1013))),x1014)))),
% 69.77/70.01 inference(scs_inference,[],[1,97,5])).
% 69.77/70.01 cnf(105,plain,
% 69.77/70.01 (P1(f2(f1(f2(f2(f2(f2(x1051,x1052),f2(x1053,x1052)),x1054),f2(f2(x1053,x1051),x1054))),x1055))),
% 69.77/70.01 inference(scs_inference,[],[101,15,5])).
% 69.77/70.01 cnf(112,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(x1121,x1122)),f2(x1121,x1122)),f2(f2(x1122,x1123),f2(x1121,x1123))))),
% 69.77/70.01 inference(scs_inference,[],[35,3,5])).
% 69.77/70.01 cnf(115,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(x1151,x1152)),f2(x1151,x1152)),f2(f2(f1(f2(x1152,x1153)),f2(x1152,x1153)),f2(x1151,x1153))))),
% 69.77/70.01 inference(scs_inference,[],[35,97,5])).
% 69.77/70.01 cnf(119,plain,
% 69.77/70.01 (P1(f2(f2(f2(f2(x1191,x1192),x1193),x1194),f2(f2(f2(f2(x1192,x1195),f2(x1191,x1195)),x1193),x1194)))),
% 69.77/70.01 inference(scs_inference,[],[112,105,5])).
% 69.77/70.01 cnf(123,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(x1231,x1232)),f2(x1231,x1232)),f2(f2(f1(x1231),x1231),x1232)))),
% 69.77/70.01 inference(scs_inference,[],[115,9,5])).
% 69.77/70.01 cnf(127,plain,
% 69.77/70.01 (P1(f2(f2(f2(f2(f2(x1271,x1272),x1273),f2(f2(x1274,x1272),x1273)),x1275),f2(f2(f1(f2(x1271,x1274)),f2(x1271,x1274)),x1275)))),
% 69.77/70.01 inference(scs_inference,[],[119,97,5])).
% 69.77/70.01 cnf(135,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(f2(f2(x1351,x1352),f2(x1353,x1352)),x1354)),f2(f2(f2(x1351,x1352),f2(x1353,x1352)),x1354)),f2(f2(x1353,x1351),x1354)))),
% 69.77/70.01 inference(scs_inference,[],[123,105,5])).
% 69.77/70.01 cnf(165,plain,
% 69.77/70.01 (P1(f2(f1(f2(f2(f1(x1651),x1651),f2(f1(x1651),x1652))),x1653))),
% 69.77/70.01 inference(scs_inference,[],[76,1,5])).
% 69.77/70.01 cnf(172,plain,
% 69.77/70.01 (P1(f2(f2(x1721,x1722),f2(f2(f1(f2(x1722,x1723)),f2(x1722,x1723)),f2(x1721,x1723))))),
% 69.77/70.01 inference(scs_inference,[],[135,39,5])).
% 69.77/70.01 cnf(202,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(f2(f1(x2021),x2022),x2023)),f2(f2(f1(x2021),x2022),x2023)),f2(x2021,x2023)))),
% 69.77/70.01 inference(scs_inference,[],[172,1,5])).
% 69.77/70.01 cnf(330,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(x3301,f2(x3302,x3303))),f2(x3301,f2(x3302,x3303))),f2(f2(f2(f2(x3303,x3304),f2(x3302,x3304)),x3305),f2(x3301,x3305))))),
% 69.77/70.01 inference(scs_inference,[],[97,119,5])).
% 69.77/70.01 cnf(334,plain,
% 69.77/70.01 (P1(f2(f2(f2(f2(x3341,x3342),f2(f1(x3343),x3342)),x3344),f2(f2(f1(x3343),x3343),x3344)))),
% 69.77/70.01 inference(scs_inference,[],[330,165,5])).
% 69.77/70.01 cnf(378,plain,
% 69.77/70.01 (P1(f2(f2(f2(f2(f2(x3781,x3782),x3783),f2(f2(x3784,x3782),x3783)),x3785),f2(f2(x3781,x3784),x3785)))),
% 69.77/70.01 inference(scs_inference,[],[330,15,5])).
% 69.77/70.01 cnf(382,plain,
% 69.77/70.01 (P1(f2(f2(f1(x3821),x3821),f2(f2(x3822,x3823),f2(f1(x3821),f2(f2(x3823,x3824),x3825)))))),
% 69.77/70.01 inference(scs_inference,[],[378,334,5])).
% 69.77/70.01 cnf(398,plain,
% 69.77/70.01 (P1(f2(f2(x3981,x3982),f2(f1(f2(f2(f1(x3983),x3983),x3983)),f2(f2(x3982,x3984),x3985))))),
% 69.77/70.01 inference(scs_inference,[],[382,9,5])).
% 69.77/70.01 cnf(410,plain,
% 69.77/70.01 (P1(f2(f2(f2(f2(x4101,x4102),f2(x4103,x4102)),x4104),f2(f2(x4103,x4101),x4104)))),
% 69.77/70.01 inference(scs_inference,[],[2,105,5])).
% 69.77/70.01 cnf(414,plain,
% 69.77/70.01 (P1(f2(f2(f1(f2(x4141,x4142)),f2(x4141,x4142)),f2(f2(x4143,x4141),f2(f2(x4142,x4144),f2(x4143,x4144)))))),
% 69.77/70.01 inference(scs_inference,[],[410,127,5])).
% 69.77/70.01 cnf(418,plain,
% 69.77/70.01 (P1(f2(f2(x4181,f2(f1(x4182),x4182)),f2(f2(x4182,x4183),f2(x4181,x4183))))),
% 69.77/70.01 inference(scs_inference,[],[9,414,5])).
% 69.77/70.01 cnf(465,plain,
% 69.77/70.01 (P1(f2(x4651,f2(f2(f1(f1(x4651)),f1(x4651)),x4652)))),
% 69.77/70.01 inference(scs_inference,[],[202,39,5])).
% 69.77/70.01 cnf(586,plain,
% 69.77/70.01 (~P1(f2(f2(f2(f2(f1(a6),x5861),x5862),f2(f2(a5,x5861),x5862)),f2(a3,f2(f2(a5,a6),a6))))),
% 69.77/70.01 inference(scs_inference,[],[378,6,5])).
% 69.77/70.01 cnf(623,plain,
% 69.77/70.01 (P1(f2(f2(f2(f2(f1(x6231),x6231),x6231),x6232),f2(f2(x6233,f1(x6231)),x6232)))),
% 69.77/70.01 inference(scs_inference,[],[418,398,5])).
% 69.77/70.01 cnf(748,plain,
% 69.77/70.01 (P1(f2(f2(x7481,f2(x7482,x7483)),f2(f2(x7484,x7482),f2(x7481,f2(x7484,x7483)))))),
% 69.77/70.01 inference(scs_inference,[],[135,105,5])).
% 69.77/70.01 cnf(758,plain,
% 69.77/70.01 (P1(f2(f2(x7581,f2(x7582,f1(x7583))),f2(f2(f2(f2(f1(x7583),x7583),x7583),x7584),f2(x7581,x7584))))),
% 69.77/70.01 inference(scs_inference,[],[623,748,5])).
% 69.77/70.01 cnf(767,plain,
% 69.77/70.01 ($false),
% 69.77/70.01 inference(scs_inference,[],[758,465,586,5]),
% 69.77/70.01 ['proof']).
% 69.77/70.01 % SZS output end Proof
% 69.77/70.01 % Total time :69.476921s
%------------------------------------------------------------------------------