%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL088-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 : n012.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 58.61s 58.86s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL088-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.01 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Fri Sep 4 22:32:12 UTC 2026
% 0.02/0.29 % CPUTime :
% 0.09/0.38 start to proof:theBenchmark
% 58.61/58.86 %-------------------------------------------
% 58.61/58.86 % File :CSE---1.7
% 58.61/58.86 % Problem :theBenchmark
% 58.61/58.86 % Transform :cnf
% 58.61/58.86 % Format :tptp:raw
% 58.61/58.86 % Command :java -jar mcs_scs.jar %d %s
% 58.61/58.86
% 58.61/58.86 % Result :Theorem 58.488419s
% 58.61/58.86 % Output :CNFRefutation 58.488419s
% 58.61/58.86 %-------------------------------------------
% 58.61/58.86 %--------------------------------------------------------------------------
% 58.61/58.86 % File : LCL088-1 : TPTP v9.3.1. Released v1.0.0.
% 58.61/58.86 % Domain : Logic Calculi (Implicational propositional)
% 58.61/58.86 % Problem : IC-3 depends on the 4th Lukasiewicz axiom
% 58.61/58.86 % Version : [TPTP] axioms.
% 58.61/58.86 % English : Axiomatisations of the Implicational propositional calculus
% 58.61/58.86 % are {IC-2,IC-3,IC-4} by Tarski-Bernays and single Lukasiewicz
% 58.61/58.86 % axioms.Show that IC-3 depends on the fourth Lukasiewicz
% 58.61/58.86 % axiom.
% 58.61/58.86
% 58.61/58.86 % Refs : [Luk48] Lukasiewicz (1948), The Shortest Axiom of the Implicat
% 58.61/58.86 % : [Pfe88] Pfenning (1988), Single Axioms in the Implicational Pr
% 58.61/58.86 % Source : [TPTP]
% 58.61/58.86 % Names :
% 58.61/58.86
% 58.61/58.86 % Status : Unsatisfiable
% 58.61/58.86 % 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.33 v2.1.0, 0.38 v2.0.0
% 58.61/58.86 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR)
% 58.61/58.86 % Number of literals : 5 ( 0 equ; 3 neg)
% 58.61/58.86 % Maximal clause size : 3 ( 1 avg)
% 58.61/58.86 % Maximal term depth : 5 ( 2 avg)
% 58.61/58.86 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 58.61/58.86 % Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% 58.61/58.86 % Number of variables : 7 ( 2 sgn)
% 58.61/58.86 % SPC : CNF_UNS_RFO_NEQ_HRN
% 58.61/58.86
% 58.61/58.86 % Comments :
% 58.61/58.86 %--------------------------------------------------------------------------
% 58.61/58.86 cnf(condensed_detachment,axiom,
% 58.61/58.86 ( ~ is_a_theorem(implies(X,Y))
% 58.61/58.86 | ~ is_a_theorem(X)
% 58.61/58.86 | is_a_theorem(Y) ) ).
% 58.61/58.86
% 58.61/58.86 cnf(ic_JLukasiewicz_4,axiom,
% 58.61/58.86 is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(T,implies(implies(S,P),implies(R,P))))) ).
% 58.61/58.86
% 58.61/58.86 cnf(prove_ic_3,negated_conjecture,
% 58.61/58.86 ~ is_a_theorem(implies(implies(implies(a,b),a),a)) ).
% 58.61/58.86
% 58.61/58.86 %--------------------------------------------------------------------------
% 58.61/58.86 %-------------------------------------------
% 58.61/58.86 % Proof found
% 58.61/58.86 % SZS status Theorem for theBenchmark
% 58.61/58.86 % SZS output start Proof
% 58.61/58.86 %ClaNum:3(EqnAxiom:0)
% 58.61/58.86 %VarNum:13(SingletonVarNum:7)
% 58.61/58.86 %MaxLitNum:3
% 58.61/58.86 %MaxfuncDepth:4
% 58.61/58.86 %SharedTerms:6
% 58.61/58.86 %goalClause: 2
% 58.61/58.86 %singleGoalClaCount:1
% 58.61/58.86 [2]~P1(f1(f1(f1(a2,a3),a2),a2))
% 58.61/58.86 [1]P1(f1(f1(f1(x11,x12),f1(x13,x14)),f1(x15,f1(f1(x14,x11),f1(x13,x11)))))
% 58.61/58.86 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31))
% 58.61/58.86 %EqnAxiom
% 58.61/58.86
% 58.61/58.86 %-------------------------------------------
% 58.61/58.86 cnf(4,plain,
% 58.61/58.86 (P1(f1(x41,f1(f1(x42,x43),f1(x44,x43))))+~P1(f1(f1(x43,x45),f1(x44,x42)))),
% 58.61/58.86 inference(scs_inference,[],[1,3])).
% 58.61/58.86 cnf(6,plain,
% 58.61/58.86 (P1(f1(x61,f1(f1(f1(f1(x62,x63),f1(x64,x63)),f1(x63,x65)),f1(x66,f1(x63,x65)))))),
% 58.61/58.86 inference(scs_inference,[],[1,4])).
% 58.61/58.86 cnf(8,plain,
% 58.61/58.86 (P1(f1(f1(f1(f1(x81,x82),f1(x83,x82)),f1(x82,x84)),f1(x85,f1(x82,x84))))),
% 58.61/58.86 inference(scs_inference,[],[6,1,3])).
% 58.61/58.86 cnf(11,plain,
% 58.61/58.86 (P1(f1(x111,f1(x112,f1(f1(x112,x113),f1(x114,x113)))))),
% 58.61/58.86 inference(scs_inference,[],[1,8,3])).
% 58.61/58.86 cnf(15,plain,
% 58.61/58.86 (P1(f1(x151,f1(f1(f1(f1(x152,x153),f1(x154,x153)),x155),f1(x152,x155))))),
% 58.61/58.86 inference(scs_inference,[],[11,4])).
% 58.61/58.86 cnf(18,plain,
% 58.61/58.86 (P1(f1(f1(f1(f1(x181,x182),f1(x183,x182)),x184),f1(x181,x184)))),
% 58.61/58.86 inference(scs_inference,[],[11,15,3])).
% 58.61/58.87 cnf(21,plain,
% 58.61/58.87 (P1(f1(x211,f1(f1(x211,x212),f1(x213,x212))))),
% 58.61/58.87 inference(scs_inference,[],[11,18,3])).
% 58.61/58.87 cnf(26,plain,
% 58.61/58.87 (P1(f1(f1(f1(f1(f1(f1(x261,x262),f1(x263,x262)),x264),f1(x261,x264)),x265),f1(x266,x265)))),
% 58.61/58.87 inference(scs_inference,[],[18,21,3])).
% 58.61/58.87 cnf(29,plain,
% 58.61/58.87 (P1(f1(f1(f1(f1(f1(f1(f1(f1(x291,x292),f1(x293,x292)),x294),f1(x291,x294)),x295),f1(x296,x295)),x297),f1(x298,x297)))),
% 58.61/58.87 inference(scs_inference,[],[21,26,3])).
% 58.61/58.87 cnf(32,plain,
% 58.61/58.87 (~P1(f1(f1(x321,f1(f1(x321,x322),f1(x323,x322))),f1(f1(f1(a2,a3),a2),a2)))),
% 58.61/58.87 inference(scs_inference,[],[21,2,3])).
% 58.61/58.87 cnf(40,plain,
% 58.61/58.87 (P1(f1(x401,f1(f1(x402,x403),f1(x404,f1(x402,x403)))))),
% 58.61/58.87 inference(scs_inference,[],[29,8,3])).
% 58.61/58.87 cnf(44,plain,
% 58.61/58.87 (P1(f1(x441,f1(f1(f1(x442,f1(x443,x444)),x445),f1(f1(x443,x444),x445))))),
% 58.61/58.87 inference(scs_inference,[],[29,8,3,4])).
% 58.61/58.87 cnf(46,plain,
% 58.61/58.87 (P1(f1(f1(x461,x462),f1(x463,f1(x461,x462))))),
% 58.61/58.87 inference(scs_inference,[],[29,40,3])).
% 58.61/58.87 cnf(49,plain,
% 58.61/58.87 (P1(f1(f1(f1(x491,f1(x492,x493)),x494),f1(f1(x492,x493),x494)))),
% 58.61/58.87 inference(scs_inference,[],[29,44,3])).
% 58.61/58.87 cnf(52,plain,
% 58.61/58.87 (P1(f1(x521,f1(f1(f1(x522,x523),x522),f1(x524,x522))))),
% 58.61/58.87 inference(scs_inference,[],[29,46,44,3,4])).
% 58.61/58.87 cnf(56,plain,
% 58.61/58.87 (P1(f1(f1(x561,x562),f1(x563,f1(x564,f1(x561,x562)))))),
% 58.61/58.87 inference(scs_inference,[],[49,46,3])).
% 58.61/58.87 cnf(60,plain,
% 58.61/58.87 (P1(f1(f1(f1(x601,x602),x601),f1(x603,x601)))),
% 58.61/58.87 inference(scs_inference,[],[56,52,3])).
% 58.61/58.87 cnf(82,plain,
% 58.61/58.87 (P1(f1(x821,f1(f1(x822,f1(x822,x823)),f1(x824,f1(x822,x823)))))),
% 58.61/58.87 inference(scs_inference,[],[60,4])).
% 58.61/58.87 cnf(84,plain,
% 58.61/58.87 (P1(f1(f1(x841,f1(x841,x842)),f1(x843,f1(x841,x842))))),
% 58.61/58.87 inference(scs_inference,[],[40,82,3])).
% 58.61/58.87 cnf(87,plain,
% 58.61/58.87 ($false),
% 58.61/58.87 inference(scs_inference,[],[84,32,60,3]),
% 58.61/58.87 ['proof']).
% 58.61/58.87 % SZS output end Proof
% 58.61/58.87 % Total time :58.488419s
%------------------------------------------------------------------------------