%--------------------------------------------------------------------------
% File     : ROB011-1 : TPTP v2.1.0. Released v1.0.0.
% Domain   : Robbins Algebra
% Problem  : If -(a + -b) = c then -(a + -(b + k(a + c))) = c, k=1
% Version  : [Win90] (equality) axioms.
% English  : This is the base step of an induction proof.

% Refs     : [Win90] Winker (1990), Robbins Algebra: Conditions that make a
% Source   : [Win90]
% Names    : Lemma 3.4 [Win90]

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

% Comments : 
%          : tptp2X -f tptp -t rm_equality:rstfp ROB011-1.p 
%--------------------------------------------------------------------------
input_clause(commutativity_of_add,axiom,
    [++ equal(add(X, Y), add(Y, X))]).

input_clause(associativity_of_add,axiom,
    [++ equal(add(add(X, Y), Z), add(X, add(Y, Z)))]).

input_clause(robbins_axiom,axiom,
    [++ equal(negate(add(negate(add(X, Y)), negate(add(X, negate(Y))))), X)]).

input_clause(one_times_x,axiom,
    [++ equal(multiply(one, X), X)]).

input_clause(times_by_adding,axiom,
    [-- positive_integer(X),
     ++ equal(multiply(successor(V), X), add(X, multiply(V, X)))]).

input_clause(one,axiom,
    [++ positive_integer(one)]).

input_clause(next_integer,axiom,
    [-- positive_integer(X),
     ++ positive_integer(successor(X))]).

input_clause(condition,hypothesis,
    [++ equal(negate(add(a, negate(b))), c)]).

input_clause(prove_base_step,conjecture,
    [-- equal(negate(add(a, negate(add(b, multiply(one, add(a, c)))))), c)]).
%--------------------------------------------------------------------------