%------------------------------------------------------------------------------
% File     : LCL005-0 : TPTP v7.2.0. Released v3.2.0.
% Domain   : Logic Calculi (Propositional)
% Axioms   : Propositional logic
% Version  : [Pau06] axioms.
% English  :

% Refs     : [Pau06] Paulson (2006), Email to G. Sutcliffe
% Source   : [Pau06]
% Names    : PropLog.ax [Pau06]

% Status   : Satisfiable
% Syntax   : Number of clauses     :   10 (   0 non-Horn;   6 unit;  10 RR)
%            Number of atoms       :   14 (  12 equality)
%            Maximal clause size   :    2 (   1 average)
%            Number of predicates  :    2 (   0 propositional; 2-3 arity)
%            Number of functors    :    5 (   1 constant; 0-3 arity)
%            Number of variables   :   34 (  20 singleton)
%            Maximal term depth    :    2 (   2 average)
% SPC      : 

% Comments : Requires MSC001-0.ax, MSC001-2.ax
%------------------------------------------------------------------------------
cnf(cls_PropLog_Opl_Odistinct__1__iff1_0,axiom,
    ( c_PropLog_Opl_Ofalse != c_PropLog_Opl_Ovar(V_a_H,T_a) )).

cnf(cls_PropLog_Opl_Odistinct__2__iff1_0,axiom,
    ( c_PropLog_Opl_Ovar(V_a_H,T_a) != c_PropLog_Opl_Ofalse )).

cnf(cls_PropLog_Opl_Odistinct__3__iff1_0,axiom,
    ( c_PropLog_Opl_Ofalse != c_PropLog_Opl_Oop_A_N_62(V_pl1_H,V_pl2_H,T_a) )).

cnf(cls_PropLog_Opl_Odistinct__4__iff1_0,axiom,
    ( c_PropLog_Opl_Oop_A_N_62(V_pl1_H,V_pl2_H,T_a) != c_PropLog_Opl_Ofalse )).

cnf(cls_PropLog_Opl_Odistinct__5__iff1_0,axiom,
    ( c_PropLog_Opl_Ovar(V_a,T_a) != c_PropLog_Opl_Oop_A_N_62(V_pl1_H,V_pl2_H,T_a) )).

cnf(cls_PropLog_Opl_Odistinct__6__iff1_0,axiom,
    ( c_PropLog_Opl_Oop_A_N_62(V_pl1_H,V_pl2_H,T_a) != c_PropLog_Opl_Ovar(V_a,T_a) )).

cnf(cls_PropLog_Opl_Oinject__1__iff1_0,axiom,
    ( c_PropLog_Opl_Ovar(V_a,T_a) != c_PropLog_Opl_Ovar(V_a_H,T_a)
    | V_a = V_a_H )).

cnf(cls_PropLog_Opl_Oinject__2__iff1_0,axiom,
    ( c_PropLog_Opl_Oop_A_N_62(V_pl1,V_pl2,T_a) != c_PropLog_Opl_Oop_A_N_62(V_pl1_H,V_pl2_H,T_a)
    | V_pl1 = V_pl1_H )).

cnf(cls_PropLog_Opl_Oinject__2__iff1_1,axiom,
    ( c_PropLog_Opl_Oop_A_N_62(V_pl1,V_pl2,T_a) != c_PropLog_Opl_Oop_A_N_62(V_pl1_H,V_pl2_H,T_a)
    | V_pl2 = V_pl2_H )).

cnf(cls_PropLog_Othms_OH_0,axiom,
    ( ~ c_in(V_p,V_H,tc_PropLog_Opl(T_a))
    | c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) )).

%------------------------------------------------------------------------------