SWV002-0.ax

%--------------------------------------------------------------------------
% File     : SWV002-0 : TPTP v7.2.0. Released v1.0.0.
% Domain   : Software Verification
% Axioms   : Program verification axioms
% Version  : [MOW76] axioms.
% English  : These "clauses arose in a natural manner from work done
%            in program verification" [MOW76] p.779.

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

% Status   : Satisfiable
% Syntax   : Number of clauses    :   22 (   2 non-Horn;   6 unit;  19 RR)
%            Number of atoms      :   52 (   3 equality)
%            Maximal clause size  :    5 (   2 average)
%            Number of predicates :   11 (   0 propositional; 1-4 arity)
%            Number of functors   :    4 (   2 constant; 0-2 arity)
%            Number of variables  :   48 (   5 singleton)
%            Maximal term depth   :    2 (   1 average)
% SPC      : 

% Comments : These axioms were contributed to [MOW76] by E. McCharen. The
%            axioms are incomplete.
%          : Due to clause_2 being incomplete, no problems have been defined
%            on these axioms.
%--------------------------------------------------------------------------
cnf(clause_1,axiom,
    ( ~ q1(Vj,Vt,Vx)
    | q2(Vj,e(Vx,n1),Vx) )).

%----The second literal is not printed in [MOW76].
%----So this literal may be wrong
cnf(clause_2,axiom,
    ( ~ q2(Vj,Vt,Vx)
    | q3(successor(n1),Vt,VWhat) )).

cnf(clause_3,axiom,
    ( ~ q3(Vj,Vt,Vx)
    | ~ less_or_equal(Vj,n)
    | q4(Vj,Vt,Vx) )).

cnf(clause_4,axiom,
    ( ~ q3(Vj,Vt,Vx)
    | less_or_equal(Vj,n)
    | q7(Vj,Vt,Vx) )).

cnf(clause_5,axiom,
    ( ~ q4(Vj,Vt,Vx)
    | ~ d(Vj)
    | ~ less_or_equal(e(Vx,Vj),Vt)
    | q6(Vj,Vt,Vx) )).

cnf(clause_6,axiom,
    ( ~ q4(Vj,Vt,Vx)
    | ~ d(Vj)
    | less_or_equal(e(Vx,Vj),Vt)
    | q5(Vj,Vt,Vx) )).

cnf(clause_7,axiom,
    ( ~ q5(Vj,Vt,Vx)
    | ~ d(Vj)
    | q6(Vj,e(Vx,Vj),Vx) )).

cnf(clause_8,axiom,
    ( ~ q6(Vj,Vt,Vx)
    | q3(successor(Vj),Vt,Vx) )).

cnf(definition_of_d_1,axiom,
    ( ~ less_or_equal(n1,X)
    | ~ less_or_equal(X,n)
    | d(X) )).

cnf(definition_of_d_2,axiom,
    ( ~ d(X)
    | ~ less_or_equal(n1,X) )).

cnf(definition_of_d_3,axiom,
    ( ~ d(X)
    | less_or_equal(X,n) )).

cnf(one_is_d,axiom,
    ( d(n1) )).

cnf(n_is_d,axiom,
    ( d(n) )).

cnf(clause_9,axiom,
    ( less_or_equal(n1,n) )).

cnf(clause_10,axiom,
    ( ~ ub(W1,X,Y,Z)
    | ~ less_or_equal(W1,W2)
    | ub(W2,X,Y,Z) )).

cnf(clause_11,axiom,
    ( ~ ub(W,X,Y,Z1)
    | successor(Z1) != Z2
    | ~ d(Z2)
    | ~ less_or_equal(e(X,Z2),W)
    | ub(W,X,Y,Z2) )).

cnf(successor_not_less_or_equal,axiom,
    ( ~ less_or_equal(successor(X),X) )).

cnf(less_or_equal_than_successor,axiom,
    ( less_or_equal(X,successor(X)) )).

cnf(less_or_equal_reflexivity,axiom,
    ( less_or_equal(X,X) )).

cnf(less_or_equal_implies_equal,axiom,
    ( ~ less_or_equal(X,Y)
    | ~ less_or_equal(Y,X)
    | X = Y )).

cnf(transitivity_of_less_or_equal,axiom,
    ( ~ less_or_equal(X,Y)
    | ~ less_or_equal(Y,Z)
    | less_or_equal(X,Z) )).

cnf(equal_implies_less_or_equal,axiom,
    ( less_or_equal(X,Y)
    | X != Y )).

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