%--------------------------------------------------------------------------
% File     : SWV001-0 : TPTP v7.2.0. Released v1.0.0.
% Domain   : Software Verification
% Axioms   : Program verification axioms
% Version  : [MOW76] axioms.
% English  :

% Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a
% Source   : [MOW76]
% Names    :

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

% Comments : Only reflexivity is specified from equality, i.e. no symmetry
%            or transitivity.
%          : These axioms were contributed to [MOW76] in private
%            correspondance from G. Ernst.
%--------------------------------------------------------------------------
cnf(predecessor_successor,axiom,
    ( predecessor(successor(X)) = X )).

cnf(successor_predecessor,axiom,
    ( successor(predecessor(X)) = X )).

cnf(well_defined_predecessor,axiom,
    ( X = Y
    | predecessor(X) != predecessor(Y) )).

cnf(well_defined_successor,axiom,
    ( X = Y
    | successor(X) != successor(Y) )).

cnf(predecessor_less_than,axiom,
    ( less_than(predecessor(X),X) )).

cnf(less_than_successor,axiom,
    ( less_than(X,successor(X)) )).

cnf(transitivity_of_less_than,axiom,
    ( less_than(X,Z)
    | ~ less_than(X,Y)
    | ~ less_than(Y,Z) )).

cnf(all_related,axiom,
    ( less_than(X,Y)
    | less_than(Y,X)
    | X = Y )).

cnf(x_not_less_than_x,axiom,
    ( ~ less_than(X,X) )).

cnf(anti_symmetry_of_less_than,axiom,
    ( ~ less_than(X,Y)
    | ~ less_than(Y,X) )).

cnf(equal_and_less_than_transitivity1,axiom,
    ( less_than(Y,Z)
    | X != Y
    | ~ less_than(X,Z) )).

cnf(equal_and_less_than_transitivity2,axiom,
    ( less_than(Z,Y)
    | X != Y
    | ~ less_than(Z,X) )).

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