#--------------------------------------------------------------------------
# File     : LCL207-1 : TPTP v2.1.0. Released v1.1.0.
# Domain   : Logic Calculi (Propositional)
# Problem  : Principia Mathematica 2.521
# Version  : [WR27] axioms.
# English  : 

# Refs     : [WR27]  Whitehead & Russell (1927), Principia Mathematica
#          : [NSS63] Newell et al. (1963), Empirical Explorations with the 
#          : [ORo89] O'Rourke (1989), LT Revisited: Explanation-Based Learn
#          : [SE94]  Segre & Elkan (1994), A High-Performance Explanation-B
# Source   : [SE94]
# Names    : Problem 2.521 [WR27]

# Status   : unsatisfiable
# Rating   : 0.44 v2.1.0, 0.25 v2.0.0
# Syntax   : Number of clauses    :    9 (   0 non-Horn;   6 unit;   4 RR)
#            Number of literals   :   14 (   0 equality)
#            Maximal clause size  :    3 (   1 average)
#            Number of predicates :    2 (   0 propositional; 1-1 arity)
#            Number of functors   :    4 (   2 constant; 0-2 arity)
#            Number of variables  :   17 (   1 singleton)
#            Maximal term depth   :    6 (   3 average)

# Comments : 
#          : tptp2X -f setheo:sign -t rm_equality:rstfp LCL207-1.p 
#--------------------------------------------------------------------------
# axiom_1_2, axiom.
axiom(or(not(or(A, A)), A)) <- .

# axiom_1_3, axiom.
axiom(or(not(A), or(B, A))) <- .

# axiom_1_4, axiom.
axiom(or(not(or(A, B)), or(B, A))) <- .

# axiom_1_5, axiom.
axiom(or(not(or(A, or(B, C))), or(B, or(A, C)))) <- .

# axiom_1_6, axiom.
axiom(or(not(or(not(A), B)), or(not(or(C, A)), or(C, B)))) <- .

# rule_1, axiom.
theorem(X) <- 
    axiom(X).

# rule_2, axiom.
theorem(X) <- 
    axiom(or(not(Y), X)),
    theorem(Y).

# rule_3, axiom.
theorem(or(not(X), Z)) <- 
    axiom(or(not(X), Y)),
    theorem(or(not(Y), Z)).

# prove_this, conjecture.
 <- theorem(or(not(not(or(not(p), q))), or(not(q), p))).

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