assign(max_seconds, 30). %------------------------------------------------------------------------------ % File : ALG189+1 : TPTP v3.0.1. Released v2.7.0. % Domain : General Algebra % Problem : Quasigroups 5 QG4: REPRESENTATIVES-SATISFY-PROPS-PROBLEM-4 % Version : Especial. % English : % Refs : [Mei03] Meier (2003), Email to G.Sutcliffe % : [CM+04] Colton et al. (2004), Automatic Generation of Classifi % Source : [Mei03] % Names : % Status : Theorem % Rating : 0.89 v2.7.0 % Syntax : Number of formulae : 3 ( 0 unit) % Number of atoms : 460 ( 460 equality) % Maximal formula depth : 125 ( 54 average) % Number of connectives : 467 ( 10 ~ ; 300 |; 157 &) % ( 0 <=>; 0 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 1 ( 0 propositional; 2-2 arity) % Number of functors : 6 ( 5 constant; 0-2 arity) % Number of variables : 0 ( 0 singleton; 0 !; 0 ?) % Maximal term depth : 3 ( 2 average) % Comments : % : tptp2X -f mace4 ALG189+1.p %------------------------------------------------------------------------------ %----NOTE WELL: conjecture has been negated set(prolog_style_variables). formulas(assumptions). % ax1, axiom. ( -(e0 = e1) & -(e0 = e2) & -(e0 = e3) & -(e0 = e4) & -(e1 = e2) & -(e1 = e3) & -(e1 = e4) & -(e2 = e3) & -(e2 = e4) & -(e3 = e4) ). % ax2, axiom. ( op(e0,e0) = e0 & op(e0,e1) = e3 & op(e0,e2) = e4 & op(e0,e3) = e2 & op(e0,e4) = e1 & op(e1,e0) = e2 & op(e1,e1) = e1 & op(e1,e2) = e3 & op(e1,e3) = e4 & op(e1,e4) = e0 & op(e2,e0) = e1 & op(e2,e1) = e4 & op(e2,e2) = e2 & op(e2,e3) = e0 & op(e2,e4) = e3 & op(e3,e0) = e4 & op(e3,e1) = e0 & op(e3,e2) = e1 & op(e3,e3) = e3 & op(e3,e4) = e2 & op(e4,e0) = e3 & op(e4,e1) = e2 & op(e4,e2) = e0 & op(e4,e3) = e1 & op(e4,e4) = e4 ). % co1, negated_conjecture. -(( op(op(e0,e0),e0) = e0 & op(op(e0,e1),e1) = e0 & op(op(e0,e2),e2) = e0 & op(op(e0,e3),e3) = e0 & op(op(e0,e4),e4) = e0 & op(op(e1,e0),e0) = e1 & op(op(e1,e1),e1) = e1 & op(op(e1,e2),e2) = e1 & op(op(e1,e3),e3) = e1 & op(op(e1,e4),e4) = e1 & op(op(e2,e0),e0) = e2 & op(op(e2,e1),e1) = e2 & op(op(e2,e2),e2) = e2 & op(op(e2,e3),e3) = e2 & op(op(e2,e4),e4) = e2 & op(op(e3,e0),e0) = e3 & op(op(e3,e1),e1) = e3 & op(op(e3,e2),e2) = e3 & op(op(e3,e3),e3) = e3 & op(op(e3,e4),e4) = e3 & op(op(e4,e0),e0) = e4 & op(op(e4,e1),e1) = e4 & op(op(e4,e2),e2) = e4 & op(op(e4,e3),e3) = e4 & op(op(e4,e4),e4) = e4 & ( op(e0,e0) = e0 | op(e0,e0) = e1 | op(e0,e0) = e2 | op(e0,e0) = e3 | op(e0,e0) = e4 ) & ( op(e0,e1) = e0 | op(e0,e1) = e1 | op(e0,e1) = e2 | op(e0,e1) = e3 | op(e0,e1) = e4 ) & ( op(e0,e2) = e0 | op(e0,e2) = e1 | op(e0,e2) = e2 | op(e0,e2) = e3 | op(e0,e2) = e4 ) & ( op(e0,e3) = e0 | op(e0,e3) = e1 | op(e0,e3) = e2 | op(e0,e3) = e3 | op(e0,e3) = e4 ) & ( op(e0,e4) = e0 | op(e0,e4) = e1 | op(e0,e4) = e2 | op(e0,e4) = e3 | op(e0,e4) = e4 ) & ( op(e1,e0) = e0 | op(e1,e0) = e1 | op(e1,e0) = e2 | op(e1,e0) = e3 | op(e1,e0) = e4 ) & ( op(e1,e1) = e0 | op(e1,e1) = e1 | op(e1,e1) = e2 | op(e1,e1) = e3 | op(e1,e1) = e4 ) & ( op(e1,e2) = e0 | op(e1,e2) = e1 | op(e1,e2) = e2 | op(e1,e2) = e3 | op(e1,e2) = e4 ) & ( op(e1,e3) = e0 | op(e1,e3) = e1 | op(e1,e3) = e2 | op(e1,e3) = e3 | op(e1,e3) = e4 ) & ( op(e1,e4) = e0 | op(e1,e4) = e1 | op(e1,e4) = e2 | op(e1,e4) = e3 | op(e1,e4) = e4 ) & ( op(e2,e0) = e0 | op(e2,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e3 | op(e2,e0) = e4 ) & ( op(e2,e1) = e0 | op(e2,e1) = e1 | op(e2,e1) = e2 | op(e2,e1) = e3 | op(e2,e1) = e4 ) & ( op(e2,e2) = e0 | op(e2,e2) = e1 | op(e2,e2) = e2 | op(e2,e2) = e3 | op(e2,e2) = e4 ) & ( op(e2,e3) = e0 | op(e2,e3) = e1 | op(e2,e3) = e2 | op(e2,e3) = e3 | op(e2,e3) = e4 ) & ( op(e2,e4) = e0 | op(e2,e4) = e1 | op(e2,e4) = e2 | op(e2,e4) = e3 | op(e2,e4) = e4 ) & ( op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e2 | op(e3,e0) = e3 | op(e3,e0) = e4 ) & ( op(e3,e1) = e0 | op(e3,e1) = e1 | op(e3,e1) = e2 | op(e3,e1) = e3 | op(e3,e1) = e4 ) & ( op(e3,e2) = e0 | op(e3,e2) = e1 | op(e3,e2) = e2 | op(e3,e2) = e3 | op(e3,e2) = e4 ) & ( op(e3,e3) = e0 | op(e3,e3) = e1 | op(e3,e3) = e2 | op(e3,e3) = e3 | op(e3,e3) = e4 ) & ( op(e3,e4) = e0 | op(e3,e4) = e1 | op(e3,e4) = e2 | op(e3,e4) = e3 | op(e3,e4) = e4 ) & ( op(e4,e0) = e0 | op(e4,e0) = e1 | op(e4,e0) = e2 | op(e4,e0) = e3 | op(e4,e0) = e4 ) & ( op(e4,e1) = e0 | op(e4,e1) = e1 | op(e4,e1) = e2 | op(e4,e1) = e3 | op(e4,e1) = e4 ) & ( op(e4,e2) = e0 | op(e4,e2) = e1 | op(e4,e2) = e2 | op(e4,e2) = e3 | op(e4,e2) = e4 ) & ( op(e4,e3) = e0 | op(e4,e3) = e1 | op(e4,e3) = e2 | op(e4,e3) = e3 | op(e4,e3) = e4 ) & ( op(e4,e4) = e0 | op(e4,e4) = e1 | op(e4,e4) = e2 | op(e4,e4) = e3 | op(e4,e4) = e4 ) & ( op(e0,e0) = e0 | op(e0,e1) = e0 | op(e0,e2) = e0 | op(e0,e3) = e0 | op(e0,e4) = e0 ) & ( op(e0,e0) = e0 | op(e1,e0) = e0 | op(e2,e0) = e0 | op(e3,e0) = e0 | op(e4,e0) = e0 ) & ( op(e0,e0) = e1 | op(e0,e1) = e1 | op(e0,e2) = e1 | op(e0,e3) = e1 | op(e0,e4) = e1 ) & ( op(e0,e0) = e1 | op(e1,e0) = e1 | op(e2,e0) = e1 | op(e3,e0) = e1 | op(e4,e0) = e1 ) & ( op(e0,e0) = e2 | op(e0,e1) = e2 | op(e0,e2) = e2 | op(e0,e3) = e2 | op(e0,e4) = e2 ) & ( op(e0,e0) = e2 | op(e1,e0) = e2 | op(e2,e0) = e2 | op(e3,e0) = e2 | op(e4,e0) = e2 ) & ( op(e0,e0) = e3 | op(e0,e1) = e3 | op(e0,e2) = e3 | op(e0,e3) = e3 | op(e0,e4) = e3 ) & ( op(e0,e0) = e3 | op(e1,e0) = e3 | op(e2,e0) = e3 | op(e3,e0) = e3 | op(e4,e0) = e3 ) & ( op(e0,e0) = e4 | op(e0,e1) = e4 | op(e0,e2) = e4 | op(e0,e3) = e4 | op(e0,e4) = e4 ) & ( op(e0,e0) = e4 | op(e1,e0) = e4 | op(e2,e0) = e4 | op(e3,e0) = e4 | op(e4,e0) = e4 ) & ( op(e1,e0) = e0 | op(e1,e1) = e0 | op(e1,e2) = e0 | op(e1,e3) = e0 | op(e1,e4) = e0 ) & ( op(e0,e1) = e0 | op(e1,e1) = e0 | op(e2,e1) = e0 | op(e3,e1) = e0 | op(e4,e1) = e0 ) & ( op(e1,e0) = e1 | op(e1,e1) = e1 | op(e1,e2) = e1 | op(e1,e3) = e1 | op(e1,e4) = e1 ) & ( op(e0,e1) = e1 | op(e1,e1) = e1 | op(e2,e1) = e1 | op(e3,e1) = e1 | op(e4,e1) = e1 ) & ( op(e1,e0) = e2 | op(e1,e1) = e2 | op(e1,e2) = e2 | op(e1,e3) = e2 | op(e1,e4) = e2 ) & ( op(e0,e1) = e2 | op(e1,e1) = e2 | op(e2,e1) = e2 | op(e3,e1) = e2 | op(e4,e1) = e2 ) & ( op(e1,e0) = e3 | op(e1,e1) = e3 | op(e1,e2) = e3 | op(e1,e3) = e3 | op(e1,e4) = e3 ) & ( op(e0,e1) = e3 | op(e1,e1) = e3 | op(e2,e1) = e3 | op(e3,e1) = e3 | op(e4,e1) = e3 ) & ( op(e1,e0) = e4 | op(e1,e1) = e4 | op(e1,e2) = e4 | op(e1,e3) = e4 | op(e1,e4) = e4 ) & ( op(e0,e1) = e4 | op(e1,e1) = e4 | op(e2,e1) = e4 | op(e3,e1) = e4 | op(e4,e1) = e4 ) & ( op(e2,e0) = e0 | op(e2,e1) = e0 | op(e2,e2) = e0 | op(e2,e3) = e0 | op(e2,e4) = e0 ) & ( op(e0,e2) = e0 | op(e1,e2) = e0 | op(e2,e2) = e0 | op(e3,e2) = e0 | op(e4,e2) = e0 ) & ( op(e2,e0) = e1 | op(e2,e1) = e1 | op(e2,e2) = e1 | op(e2,e3) = e1 | op(e2,e4) = e1 ) & ( op(e0,e2) = e1 | op(e1,e2) = e1 | op(e2,e2) = e1 | op(e3,e2) = e1 | op(e4,e2) = e1 ) & ( op(e2,e0) = e2 | op(e2,e1) = e2 | op(e2,e2) = e2 | op(e2,e3) = e2 | op(e2,e4) = e2 ) & ( op(e0,e2) = e2 | op(e1,e2) = e2 | op(e2,e2) = e2 | op(e3,e2) = e2 | op(e4,e2) = e2 ) & ( op(e2,e0) = e3 | op(e2,e1) = e3 | op(e2,e2) = e3 | op(e2,e3) = e3 | op(e2,e4) = e3 ) & ( op(e0,e2) = e3 | op(e1,e2) = e3 | op(e2,e2) = e3 | op(e3,e2) = e3 | op(e4,e2) = e3 ) & ( op(e2,e0) = e4 | op(e2,e1) = e4 | op(e2,e2) = e4 | op(e2,e3) = e4 | op(e2,e4) = e4 ) & ( op(e0,e2) = e4 | op(e1,e2) = e4 | op(e2,e2) = e4 | op(e3,e2) = e4 | op(e4,e2) = e4 ) & ( op(e3,e0) = e0 | op(e3,e1) = e0 | op(e3,e2) = e0 | op(e3,e3) = e0 | op(e3,e4) = e0 ) & ( op(e0,e3) = e0 | op(e1,e3) = e0 | op(e2,e3) = e0 | op(e3,e3) = e0 | op(e4,e3) = e0 ) & ( op(e3,e0) = e1 | op(e3,e1) = e1 | op(e3,e2) = e1 | op(e3,e3) = e1 | op(e3,e4) = e1 ) & ( op(e0,e3) = e1 | op(e1,e3) = e1 | op(e2,e3) = e1 | op(e3,e3) = e1 | op(e4,e3) = e1 ) & ( op(e3,e0) = e2 | op(e3,e1) = e2 | op(e3,e2) = e2 | op(e3,e3) = e2 | op(e3,e4) = e2 ) & ( op(e0,e3) = e2 | op(e1,e3) = e2 | op(e2,e3) = e2 | op(e3,e3) = e2 | op(e4,e3) = e2 ) & ( op(e3,e0) = e3 | op(e3,e1) = e3 | op(e3,e2) = e3 | op(e3,e3) = e3 | op(e3,e4) = e3 ) & ( op(e0,e3) = e3 | op(e1,e3) = e3 | op(e2,e3) = e3 | op(e3,e3) = e3 | op(e4,e3) = e3 ) & ( op(e3,e0) = e4 | op(e3,e1) = e4 | op(e3,e2) = e4 | op(e3,e3) = e4 | op(e3,e4) = e4 ) & ( op(e0,e3) = e4 | op(e1,e3) = e4 | op(e2,e3) = e4 | op(e3,e3) = e4 | op(e4,e3) = e4 ) & ( op(e4,e0) = e0 | op(e4,e1) = e0 | op(e4,e2) = e0 | op(e4,e3) = e0 | op(e4,e4) = e0 ) & ( op(e0,e4) = e0 | op(e1,e4) = e0 | op(e2,e4) = e0 | op(e3,e4) = e0 | op(e4,e4) = e0 ) & ( op(e4,e0) = e1 | op(e4,e1) = e1 | op(e4,e2) = e1 | op(e4,e3) = e1 | op(e4,e4) = e1 ) & ( op(e0,e4) = e1 | op(e1,e4) = e1 | op(e2,e4) = e1 | op(e3,e4) = e1 | op(e4,e4) = e1 ) & ( op(e4,e0) = e2 | op(e4,e1) = e2 | op(e4,e2) = e2 | op(e4,e3) = e2 | op(e4,e4) = e2 ) & ( op(e0,e4) = e2 | op(e1,e4) = e2 | op(e2,e4) = e2 | op(e3,e4) = e2 | op(e4,e4) = e2 ) & ( op(e4,e0) = e3 | op(e4,e1) = e3 | op(e4,e2) = e3 | op(e4,e3) = e3 | op(e4,e4) = e3 ) & ( op(e0,e4) = e3 | op(e1,e4) = e3 | op(e2,e4) = e3 | op(e3,e4) = e3 | op(e4,e4) = e3 ) & ( op(e4,e0) = e4 | op(e4,e1) = e4 | op(e4,e2) = e4 | op(e4,e3) = e4 | op(e4,e4) = e4 ) & ( op(e0,e4) = e4 | op(e1,e4) = e4 | op(e2,e4) = e4 | op(e3,e4) = e4 | op(e4,e4) = e4 ) & op(op(e0,e0),op(e0,e0)) = e0 & op(op(e1,e0),op(e0,e1)) = e0 & op(op(e2,e0),op(e0,e2)) = e0 & op(op(e3,e0),op(e0,e3)) = e0 & op(op(e4,e0),op(e0,e4)) = e0 & op(op(e0,e1),op(e1,e0)) = e1 & op(op(e1,e1),op(e1,e1)) = e1 & op(op(e2,e1),op(e1,e2)) = e1 & op(op(e3,e1),op(e1,e3)) = e1 & op(op(e4,e1),op(e1,e4)) = e1 & op(op(e0,e2),op(e2,e0)) = e2 & op(op(e1,e2),op(e2,e1)) = e2 & op(op(e2,e2),op(e2,e2)) = e2 & op(op(e3,e2),op(e2,e3)) = e2 & op(op(e4,e2),op(e2,e4)) = e2 & op(op(e0,e3),op(e3,e0)) = e3 & op(op(e1,e3),op(e3,e1)) = e3 & op(op(e2,e3),op(e3,e2)) = e3 & op(op(e3,e3),op(e3,e3)) = e3 & op(op(e4,e3),op(e3,e4)) = e3 & op(op(e0,e4),op(e4,e0)) = e4 & op(op(e1,e4),op(e4,e1)) = e4 & op(op(e2,e4),op(e4,e2)) = e4 & op(op(e3,e4),op(e4,e3)) = e4 & op(op(e4,e4),op(e4,e4)) = e4 )). end_of_list. %------------------------------------------------------------------------------