%--------------------------------------------------------------------------
% File     : LCL160-1 : TPTP v2.1.0. Released v1.0.0.
% Domain   : Logic Calculi (Wajsberg Algebra)
% Problem  : The 8th alternative Wajsberg algebra axiom
% Version  : [Bon91] (equality) axioms.
% English  : 

% Refs     : [FRT84] Font et al. (1984), Wajsberg Algebras
%          : [AB90]  Anantharaman & Bonacina (1990), An Application of the 
%          : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic
% Source   : [Bon91]
% Names    : W' axiom 8 [Bon91]

% Status   : unsatisfiable
% Rating   : 0.67 v2.1.0, 0.88 v2.0.0
% Syntax   : Number of clauses    :   17 (   0 non-Horn;  17 unit;   2 RR)
%            Number of literals   :   17 (  17 equality)
%            Maximal clause size  :    1 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :   10 (   4 constant; 0-2 arity)
%            Number of variables  :   33 (   0 singleton)
%            Maximal term depth   :    5 (   2 average)

% Comments : 
%          : tptp2X -f tptp -t rm_equality:rstfp LCL160-1.p 
%--------------------------------------------------------------------------
input_clause(wajsberg_1,axiom,
    [++ equal(implies(true, X), X)]).

input_clause(wajsberg_2,axiom,
    [++ equal(implies(implies(X, Y), implies(implies(Y, Z), implies(X, Z))), true)]).

input_clause(wajsberg_3,axiom,
    [++ equal(implies(implies(X, Y), Y), implies(implies(Y, X), X))]).

input_clause(wajsberg_4,axiom,
    [++ equal(implies(implies(not(X), not(Y)), implies(Y, X)), true)]).

input_clause(or_definition,axiom,
    [++ equal(or(X, Y), implies(not(X), Y))]).

input_clause(or_associativity,axiom,
    [++ equal(or(or(X, Y), Z), or(X, or(Y, Z)))]).

input_clause(or_commutativity,axiom,
    [++ equal(or(X, Y), or(Y, X))]).

input_clause(and_definition,axiom,
    [++ equal(and(X, Y), not(or(not(X), not(Y))))]).

input_clause(and_associativity,axiom,
    [++ equal(and(and(X, Y), Z), and(X, and(Y, Z)))]).

input_clause(and_commutativity,axiom,
    [++ equal(and(X, Y), and(Y, X))]).

input_clause(xor_definition,axiom,
    [++ equal(xor(X, Y), or(and(X, not(Y)), and(not(X), Y)))]).

input_clause(xor_commutativity,axiom,
    [++ equal(xor(X, Y), xor(Y, X))]).

input_clause(and_star_definition,axiom,
    [++ equal(and_star(X, Y), not(or(not(X), not(Y))))]).

input_clause(and_star_associativity,axiom,
    [++ equal(and_star(and_star(X, Y), Z), and_star(X, and_star(Y, Z)))]).

input_clause(and_star_commutativity,axiom,
    [++ equal(and_star(X, Y), and_star(Y, X))]).

input_clause(false_definition,axiom,
    [++ equal(not(true), false)]).

input_clause(prove_alternative_wajsberg_axiom,conjecture,
    [-- equal(and_star(xor(and_star(xor(true, x), y), true), y), and_star(xor(and_star(xor(true, y), x), true), x))]).
%--------------------------------------------------------------------------