%--------------------------------------------------------------------------
% File     : NUM003-0 : TPTP v7.2.0. Bugfixed v1.2.1.
% Domain   : Number Theory
% Axioms   : Number theory axioms, based on Godel set theory
% Version  : [BL+86] axioms.
% English  :

% Refs     : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic:
%          : [McC92] McCune (1992), Email to G. Sutcliffe
% Source   : [McC92]
% Names    :

% Status   : Satisfiable
% Syntax   : Number of clauses    :   54 (  32 non-Horn;   0 unit;  54 RR)
%            Number of atoms      :  215 (  16 equality)
%            Maximal clause size  :    7 (   4 average)
%            Number of predicates :    6 (   0 propositional; 1-3 arity)
%            Number of functors   :   29 (   7 constant; 0-3 arity)
%            Number of variables  :   90 (   0 singleton)
%            Maximal term depth   :    5 (   1 average)
% SPC      : 

% Comments : Requires SET003-0.ax ALG001-0.ax
% Bugfixes : v1.2.1 - Clauses finite3 and finite5 fixed.
%--------------------------------------------------------------------------
%----Definition of natural_numbers (natural numbers)
cnf(natural_numbers1,axiom,
    ( ~ member(Z,natural_numbers)
    | ~ little_set(Xs)
    | ~ member(empty_set,Xs)
    | member(f43(Z,Xs),Xs)
    | member(Z,Xs) )).

cnf(natural_numbers2,axiom,
    ( ~ member(Z,natural_numbers)
    | ~ little_set(Xs)
    | ~ member(empty_set,Xs)
    | ~ member(successor(f43(Z,Xs)),Xs)
    | member(Z,Xs) )).

cnf(natural_numbers3,axiom,
    ( member(Z,natural_numbers)
    | ~ little_set(Z)
    | little_set(f44(Z)) )).

cnf(natural_numbers4,axiom,
    ( member(Z,natural_numbers)
    | ~ little_set(Z)
    | member(empty_set,f44(Z)) )).

cnf(natural_numbers5,axiom,
    ( member(Z,natural_numbers)
    | ~ little_set(Z)
    | ~ member(Xk,f44(Z))
    | member(successor(Xk),f44(Z)) )).

cnf(natural_numbers6,axiom,
    ( member(Z,natural_numbers)
    | ~ member(Z,f44(Z)) )).

%----Definition of plus
cnf(plus1,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | member(f45(Z,Xs),natural_numbers)
    | member(f46(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(plus2,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | member(f45(Z,Xs),natural_numbers)
    | member(f47(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(plus3,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | member(f45(Z,Xs),natural_numbers)
    | member(f48(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(plus4,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | member(f45(Z,Xs),natural_numbers)
    | member(ordered_pair(ordered_pair(f46(Z,Xs),f47(Z,Xs)),f48(Z,Xs)),Xs)
    | member(Z,Xs) )).

cnf(plus5,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | member(f45(Z,Xs),natural_numbers)
    | ~ member(ordered_pair(ordered_pair(successor(f46(Z,Xs)),f47(Z,Xs)),successor(f48(Z,Xs))),Xs)
    | member(Z,Xs) )).

cnf(plus6,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f45(Z,Xs)),f45(Z,Xs)),Xs)
    | member(f46(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(plus7,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f45(Z,Xs)),f45(Z,Xs)),Xs)
    | member(f47(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(plus8,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f45(Z,Xs)),f45(Z,Xs)),Xs)
    | member(f48(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(plus9,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f45(Z,Xs)),f45(Z,Xs)),Xs)
    | member(ordered_pair(ordered_pair(f46(Z,Xs),f47(Z,Xs)),f48(Z,Xs)),Xs)
    | member(Z,Xs) )).

cnf(plus10,axiom,
    ( ~ member(Z,plus)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f45(Z,Xs)),f45(Z,Xs)),Xs)
    | ~ member(ordered_pair(ordered_pair(successor(f46(Z,Xs)),f47(Z,Xs)),successor(f48(Z,Xs))),Xs)
    | member(Z,Xs) )).

cnf(plus11,axiom,
    ( member(Z,plus)
    | ~ little_set(Z)
    | little_set(f49(Z)) )).

cnf(plus12,axiom,
    ( member(Z,plus)
    | ~ little_set(Z)
    | ~ member(Xi,natural_numbers)
    | member(ordered_pair(ordered_pair(empty_set,Xi),Xi),f49(Z)) )).

cnf(plus13,axiom,
    ( member(Z,plus)
    | ~ little_set(Z)
    | ~ member(Uu1,natural_numbers)
    | ~ member(Xj,natural_numbers)
    | ~ member(Xk,natural_numbers)
    | ~ member(ordered_pair(ordered_pair(Uu1,Xj),Xk),f49(Z))
    | member(ordered_pair(ordered_pair(successor(Uu1),Xj),successor(Xk)),f49(Z)) )).

cnf(plus14,axiom,
    ( member(Z,plus)
    | ~ member(Z,f49(Z)) )).

%----Definition of times
cnf(times1,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | member(f50(Z,Xs),natural_numbers)
    | member(f51(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(times2,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | member(f50(Z,Xs),natural_numbers)
    | member(f52(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(times3,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | member(f50(Z,Xs),natural_numbers)
    | member(f53(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(times4,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | member(f50(Z,Xs),natural_numbers)
    | member(ordered_pair(ordered_pair(f51(Z,Xs),f52(Z,Xs)),f53(Z,Xs)),Xs)
    | member(Z,Xs) )).

cnf(times5,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | member(f50(Z,Xs),natural_numbers)
    | ~ member(ordered_pair(ordered_pair(successor(f51(Z,Xs)),f52(Z,Xs)),apply_to_two_arguments(plus,f53(Z,Xs),f52(Z,Xs))),Xs)
    | member(Z,Xs) )).

cnf(times6,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f50(Z,Xs)),empty_set),Xs)
    | member(f51(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(times7,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f50(Z,Xs)),empty_set),Xs)
    | member(f52(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(times8,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f50(Z,Xs)),empty_set),Xs)
    | member(f53(Z,Xs),natural_numbers)
    | member(Z,Xs) )).

cnf(times9,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f50(Z,Xs)),empty_set),Xs)
    | member(ordered_pair(ordered_pair(f51(Z,Xs),f52(Z,Xs)),f53(Z,Xs)),Xs)
    | member(Z,Xs) )).

cnf(times10,axiom,
    ( ~ member(Z,times)
    | ~ little_set(Xs)
    | ~ member(ordered_pair(ordered_pair(empty_set,f50(Z,Xs)),empty_set),Xs)
    | ~ member(ordered_pair(ordered_pair(successor(f51(Z,Xs)),f52(Z,Xs)),apply_to_two_arguments(plus,f53(Z,Xs),f52(Z,Xs))),Xs)
    | member(Z,Xs) )).

cnf(times11,axiom,
    ( member(Z,times)
    | ~ little_set(Z)
    | little_set(f54(Z)) )).

cnf(times12,axiom,
    ( member(Z,times)
    | ~ little_set(Z)
    | ~ member(Xi,natural_numbers)
    | member(ordered_pair(ordered_pair(empty_set,Xi),empty_set),f54(Z)) )).

cnf(times13,axiom,
    ( member(Z,times)
    | ~ little_set(Z)
    | ~ member(Uu2,natural_numbers)
    | ~ member(Xj,natural_numbers)
    | ~ member(Xk,natural_numbers)
    | ~ member(ordered_pair(ordered_pair(Uu2,Xj),Xk),f54(Z))
    | member(ordered_pair(ordered_pair(successor(Uu2),Xj),apply_to_two_arguments(plus,Xk,Xj)),f54(Z)) )).

cnf(times14,axiom,
    ( member(Z,times)
    | ~ member(Z,f54(Z)) )).

%----Definition of prime_numbers
cnf(prime_numbers1,axiom,
    ( ~ member(Z,prime_numbers)
    | member(Z,natural_numbers) )).

cnf(prime_numbers2,axiom,
    ( ~ member(Z,prime_numbers)
    | Z != empty_set )).

cnf(prime_numbers3,axiom,
    ( ~ member(Z,prime_numbers)
    | Z != successor(empty_set) )).

cnf(prime_numbers4,axiom,
    ( ~ member(Z,prime_numbers)
    | ~ member(U,natural_numbers)
    | ~ member(V,natural_numbers)
    | apply_to_two_arguments(times,U,V) != Z
    | member(U,non_ordered_pair(successor(empty_set),Z)) )).

cnf(prime_numbers5,axiom,
    ( member(Z,prime_numbers)
    | ~ member(Z,natural_numbers)
    | Z = empty_set
    | Z = successor(empty_set)
    | member(f55(Z),natural_numbers) )).

cnf(prime_numbers6,axiom,
    ( member(Z,prime_numbers)
    | ~ member(Z,natural_numbers)
    | Z = empty_set
    | Z = successor(empty_set)
    | member(f56(Z),natural_numbers) )).

cnf(prime_numbers7,axiom,
    ( member(Z,prime_numbers)
    | ~ member(Z,natural_numbers)
    | Z = empty_set
    | Z = successor(empty_set)
    | apply_to_two_arguments(times,f55(Z),f56(Z)) = Z )).

cnf(prime_numbers8,axiom,
    ( member(Z,prime_numbers)
    | ~ member(Z,natural_numbers)
    | Z = empty_set
    | Z = successor(empty_set)
    | ~ member(f55(Z),non_ordered_pair(successor(empty_set),Z)) )).

%----Definition of finite
cnf(finite1,axiom,
    ( ~ finite(X)
    | member(f57(X),natural_numbers) )).

cnf(finite2,axiom,
    ( ~ finite(X)
    | maps(f58(X),f57(X),X) )).

cnf(finite3,axiom,
    ( ~ finite(X)
    | range_of(f58(X)) = X )).

cnf(finite4,axiom,
    ( ~ finite(X)
    | one_to_one_function(f58(X)) )).

cnf(finite5,axiom,
    ( finite(X)
    | ~ member(Xn,natural_numbers)
    | ~ maps(Xf,Xn,X)
    | range_of(Xf) != X
    | ~ one_to_one_function(Xf) )).

%----Definition of twin prime_numbers
cnf(twin_primes1,axiom,
    ( ~ member(Z,twin_prime_numbers)
    | member(Z,prime_numbers) )).

cnf(twin_primes2,axiom,
    ( ~ member(Z,twin_prime_numbers)
    | member(successor(successor(Z)),prime_numbers) )).

cnf(twin_primes3,axiom,
    ( member(Z,twin_prime_numbers)
    | ~ member(Z,prime_numbers)
    | ~ member(successor(successor(Z)),prime_numbers) )).

%----Definition of even_numbers (even natural numbers)
cnf(even_numbers1,axiom,
    ( ~ member(Z,even_numbers)
    | member(Z,natural_numbers) )).

cnf(even_numbers2,axiom,
    ( ~ member(Z,even_numbers)
    | member(f59(Z),natural_numbers) )).

cnf(even_numbers3,axiom,
    ( ~ member(Z,even_numbers)
    | apply_to_two_arguments(plus,f59(Z),f59(Z)) = Z )).

cnf(even_numbers4,axiom,
    ( member(Z,even_numbers)
    | ~ member(Z,natural_numbers)
    | ~ member(X,natural_numbers)
    | apply_to_two_arguments(plus,X,X) != Z )).

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