% paramodulation-0.1.elf
% Author: Carsten Schuermann
% -----------------------------------------------------------------------------
% File     : SYN0011 : TPTP v4.0.0. Released v4.0.0.
% Domain   : Syntactic
% Problem  : 
% Version  : 
% English  : 

% Source   : [BB05]
% Names    : 

% Status   : Theorem (SEMANTICS)
% Rating   : ? v4.0.0
% Syntax   : 
% -----------------------------------------------------------------------------

% Paramodulation example:

% all [x] p (a, f (x, b, c)) \/ q (x)
% all [z] f (a, b, z) = j (z)
% ------------------------------------
% p (a, j (c)), q (a)


%abbrev
d = [p:i -> i -> o] [q:i -> o] [f: i -> i -> i -> i] [a:i] [b:i] [c:i][j:i -> i] 
    [u1 : |- all [x] or (p a (f x b c)) (q x)]
    [u2 : |- all [z] (f a b z) == (j z)]
    paramod ([x] p a x) (select (inst u2)) (left (select (inst u1))).