%------------------------------------------------------------------------------ % File : BOO036-1 : TPTP v3.3.0. Released v2.5.0. % Domain : Algebra (Ternary Boolean) % Problem : Ternary Boolean algebra (equality) axioms % Version : [OTTER] (equality) axioms. % English : % Refs : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr % : [Win82] Winker (1982), Generation and Verification of Finite M % Source : [OTTER] % Names : % Status : Satisfiable % Rating : 0.00 v3.2.0, 0.33 v3.1.0, 0.00 v2.5.0 % Syntax : Number of clauses : 5 ( 0 non-Horn; 5 unit; 0 RR) % Number of atoms : 5 ( 5 equality) % Maximal clause size : 1 ( 1 average) % Number of predicates : 1 ( 0 propositional; 2-2 arity) % Number of functors : 2 ( 0 constant; 1-3 arity) % Number of variables : 13 ( 2 singleton) % Maximal term depth : 3 ( 2 average) % Comments : % : tptp2X -f tptp:short BOO036-1.p %------------------------------------------------------------------------------ cnf(associativity,axiom,( multiply(multiply(V,W,X),Y,multiply(V,W,Z)) = multiply(V,W,multiply(X,Y,Z)) )). cnf(ternary_multiply_1,axiom,( multiply(Y,X,X) = X )). cnf(ternary_multiply_2,axiom,( multiply(X,X,Y) = X )). cnf(left_inverse,axiom,( multiply(inverse(Y),Y,X) = X )). cnf(right_inverse,axiom,( multiply(X,Y,inverse(Y)) = X )). %------------------------------------------------------------------------------