% benchmark parameters -n2 -N6 -p

%--------------------------------------------------------------------------
% File     : LAT025-1 : TPTP v2.3.0. Released v2.2.0.
% Domain   : Lattice Theory (Ternary Near Lattices)
% Problem  : Non-uniqueness of meet (dually join) in TNL
% Version  : [MP96] (equality) axioms.
% English  : Let's say we have a ternary near-lattice (TNL) with two meet
%            operations, say meet1 and meet2.  In other words, {join,meet1}
%            and {join,meet2} are TNLs.  Are the two meets necessarily
%            the same?  No, they aren't.  Here is a counterexample.

% Refs     : [McC98] McCune (1998), Email to G. Sutcliffe
%          : [MP96]  McCune & Padmanabhan (1996), Automated Deduction in Eq
% Source   : [McC98]
% Names    : TNL-2 [MP96]

% Status   : satisfiable
% Rating   : 1.00 v2.2.1
% Syntax   : Number of clauses    :   16 (   0 non-Horn;  16 unit;   1 RR)
%            Number of literals   :   16 (  16 equality)
%            Maximal clause size  :    1 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :    5 (   2 constant; 0-2 arity)
%            Number of variables  :   30 (  12 singleton)
%            Maximal term depth   :    4 (   1 average)

% Comments : The smallest model has 5 elements.
%          : tptp2X -f otter:hypothesis:[set(tptp_eq),set(auto),clear(print_given)] -t rm_equality:stfp LAT025-1.p 
%--------------------------------------------------------------------------
set(prolog_style_variables).
set(tptp_eq).
set(auto).
clear(print_given).

list(usable).

% reflexivity, axiom.
 equal(X, X).

% idempotence_of_meet, axiom.
 equal(meet(X, X), X).

% idempotence_of_join, axiom.
 equal(join(X, X), X).

% absorption1, axiom.
 equal(meet(X, join(X, Y)), X).

% absorption2, axiom.
 equal(join(X, meet(X, Y)), X).

% commutativity_of_meet, axiom.
 equal(meet(X, Y), meet(Y, X)).

% commutativity_of_join, axiom.
 equal(join(X, Y), join(Y, X)).

% tnl_1, axiom.
 equal(join(X, meet(Y, meet(X, Z))), X).

% tnl_2, axiom.
 equal(meet(X, join(Y, join(X, Z))), X).

% idempotence_of_meet2, axiom.
 equal(meet2(X, X), X).

% absorption1_2, axiom.
 equal(meet2(X, join(X, Y)), X).

% absorption2_2, axiom.
 equal(join(X, meet2(X, Y)), X).

% commutativity_of_meet2, axiom.
 equal(meet2(X, Y), meet2(Y, X)).

% tnl_1_2, axiom.
 equal(join(X, meet2(Y, meet2(X, Z))), X).

% tnl_2_2, axiom.
 equal(meet2(X, join(Y, join(X, Z))), X).

end_of_list.

list(sos).

% prove_meets_equal, conjecture.
-equal(meet(a, b), meet2(a, b)).

end_of_list.

%--------------------------------------------------------------------------
