#--------------------------------------------------------------------------
# File     : SYN310-1 : TPTP v2.1.0. Released v1.2.0.
# Domain   : Syntactic
# Problem  : Problem for testing satisfiability
# Version  : Special.
# English  : 

# Refs     : [FL+93] Fermuller et al. (1993), Resolution Methods for the De
# Source   : [FL+93]
# Names    : H1 [FL+93]

# Status   : unsatisfiable
# Rating   : 0.00 v2.0.0
# Syntax   : Number of clauses    :    6 (   0 non-Horn;   2 unit;   6 RR)
#            Number of literals   :   10 (   0 equality)
#            Maximal clause size  :    2 (   1 average)
#            Number of predicates :    1 (   0 propositional; 3-3 arity)
#            Number of functors   :    5 (   3 constant; 0-1 arity)
#            Number of variables  :   12 (   0 singleton)
#            Maximal term depth   :    3 (   1 average)

# Comments : This set belongs to the class PVD [FL+93] p.192.
#          : tptp2X -f setheo:sign -t rm_equality:rstfp SYN310-1.p 
#--------------------------------------------------------------------------
# clause1, conjecture.
p(X, X1, X2) <- 
    p(X2, X1, X).

# clause2, conjecture.
p(X, X1, X2) <- 
    p(X1, X, X2).

# clause3, conjecture.
p(X, X1, X2) <- 
    p(X, X1, g(X2)).

# clause4, conjecture.
p(X, X1, X2) <- 
    p(f(X), X1, X2).

# clause5, conjecture.
 <- p(a, b, c).

# clause6, conjecture.
p(f(g(a)), f(g(b)), f(g(c))) <- .

#--------------------------------------------------------------------------