%--------------------------------------------------------------------------
% File     : LCL093-1 : TPTP v2.1.0. Released v1.0.0.
% Domain   : Logic Calculi (Implicational propositional)
% Problem  : IC-4 depends on the 5th Lukasiewicz axiom
% Version  : [TPTP] axioms.
% English  : Axiomatisations of the Implicational propositional calculus 
%            are {IC-2,IC-3,IC-4} by Tarski-Bernays and single Lukasiewicz 
%            axioms.Show that IC-4 depends on the fifth Lukasiewicz axiom.

% Refs     : [Luk48] Lukasiewicz (1948), The Shortest Axiom of the Implicat
%          : [Pfe88] Pfenning (1988), Single Axioms in the Implicational Pr
% Source   : [TPTP]
% Names    : 

% Status   : unsatisfiable
% Rating   : 0.78 v2.1.0, 0.88 v2.0.0
% Syntax   : Number of clauses    :    3 (   0 non-Horn;   2 unit;   2 RR)
%            Number of literals   :    5 (   0 equality)
%            Maximal clause size  :    3 (   1 average)
%            Number of predicates :    1 (   0 propositional; 1-1 arity)
%            Number of functors   :    4 (   3 constant; 0-2 arity)
%            Number of variables  :    7 (   2 singleton)
%            Maximal term depth   :    5 (   2 average)

% Comments : 
%          : tptp2X -f tptp -t rm_equality:rstfp LCL093-1.p 
%--------------------------------------------------------------------------
input_clause(condensed_detachment,axiom,
    [-- is_a_theorem(implies(X, Y)),
     -- is_a_theorem(X),
     ++ is_a_theorem(Y)]).

input_clause(ic_JLukasiewicz_5,axiom,
    [++ is_a_theorem(implies(implies(implies(P, Q), implies(R, S)), implies(implies(S, P), implies(T, implies(R, P)))))]).

input_clause(prove_ic_4,conjecture,
    [-- is_a_theorem(implies(implies(a, b), implies(implies(b, c), implies(a, c))))]).
%--------------------------------------------------------------------------