assign(max_seconds, 30). %------------------------------------------------------------------------------ % File : ALG043+1 : TPTP v3.0.1. Released v2.7.0. % Domain : General Algebra % Problem : Loops 4: REPRESENTATIVES-SATISFY-PROPS-PROBLEM-1 % 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 : 4 ( 1 unit) % Number of atoms : 243 ( 243 equality) % Maximal formula depth : 61 ( 21 average) % Number of connectives : 245 ( 6 ~ ; 150 |; 89 &) % ( 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 : 2 ( 1 average) % Comments : % : tptp2X -f mace4 ALG043+1.p %------------------------------------------------------------------------------ %----NOTE WELL: conjecture has been negated set(prolog_style_variables). formulas(assumptions). % ax1, axiom. ( -(e0 = e1) & -(e0 = e2) & -(e0 = e3) & -(e1 = e2) & -(e1 = e3) & -(e2 = e3) ). % ax2, axiom. ( op(e0,e0) = e0 & op(e0,e1) = e1 & op(e0,e2) = e2 & op(e0,e3) = e3 & op(e1,e0) = e1 & op(e1,e1) = e0 & op(e1,e2) = e3 & op(e1,e3) = e2 & op(e2,e0) = e2 & op(e2,e1) = e3 & op(e2,e2) = e0 & op(e2,e3) = e1 & op(e3,e0) = e3 & op(e3,e1) = e2 & op(e3,e2) = e1 & op(e3,e3) = e0 ). % ax3, axiom. unit = e0. % co1, negated_conjecture. -(( ( ( op(e0,e0) = e0 & op(e1,e1) = e0 & op(e2,e2) = e0 & op(e3,e3) = e0 ) | ( op(e0,e0) = e1 & op(e1,e1) = e1 & op(e2,e2) = e1 & op(e3,e3) = e1 ) | ( op(e0,e0) = e2 & op(e1,e1) = e2 & op(e2,e2) = e2 & op(e3,e3) = e2 ) | ( op(e0,e0) = e3 & op(e1,e1) = e3 & op(e2,e2) = e3 & op(e3,e3) = e3 ) ) & ( op(e0,e0) = e0 | op(e0,e0) = e1 | op(e0,e0) = e2 | op(e0,e0) = e3 ) & ( op(e0,e1) = e0 | op(e0,e1) = e1 | op(e0,e1) = e2 | op(e0,e1) = e3 ) & ( op(e0,e2) = e0 | op(e0,e2) = e1 | op(e0,e2) = e2 | op(e0,e2) = e3 ) & ( op(e0,e3) = e0 | op(e0,e3) = e1 | op(e0,e3) = e2 | op(e0,e3) = e3 ) & ( op(e1,e0) = e0 | op(e1,e0) = e1 | op(e1,e0) = e2 | op(e1,e0) = e3 ) & ( op(e1,e1) = e0 | op(e1,e1) = e1 | op(e1,e1) = e2 | op(e1,e1) = e3 ) & ( op(e1,e2) = e0 | op(e1,e2) = e1 | op(e1,e2) = e2 | op(e1,e2) = e3 ) & ( op(e1,e3) = e0 | op(e1,e3) = e1 | op(e1,e3) = e2 | op(e1,e3) = e3 ) & ( op(e2,e0) = e0 | op(e2,e0) = e1 | op(e2,e0) = e2 | op(e2,e0) = e3 ) & ( op(e2,e1) = e0 | op(e2,e1) = e1 | op(e2,e1) = e2 | op(e2,e1) = e3 ) & ( op(e2,e2) = e0 | op(e2,e2) = e1 | op(e2,e2) = e2 | op(e2,e2) = e3 ) & ( op(e2,e3) = e0 | op(e2,e3) = e1 | op(e2,e3) = e2 | op(e2,e3) = e3 ) & ( op(e3,e0) = e0 | op(e3,e0) = e1 | op(e3,e0) = e2 | op(e3,e0) = e3 ) & ( op(e3,e1) = e0 | op(e3,e1) = e1 | op(e3,e1) = e2 | op(e3,e1) = e3 ) & ( op(e3,e2) = e0 | op(e3,e2) = e1 | op(e3,e2) = e2 | op(e3,e2) = e3 ) & ( op(e3,e3) = e0 | op(e3,e3) = e1 | op(e3,e3) = e2 | op(e3,e3) = e3 ) & op(unit,e0) = e0 & op(e0,unit) = e0 & op(unit,e1) = e1 & op(e1,unit) = e1 & op(unit,e2) = e2 & op(e2,unit) = e2 & op(unit,e3) = e3 & op(e3,unit) = e3 & ( unit = e0 | unit = e1 | unit = e2 | unit = e3 ) & ( op(e0,e0) = e0 | op(e0,e1) = e0 | op(e0,e2) = e0 | op(e0,e3) = e0 ) & ( op(e0,e0) = e0 | op(e1,e0) = e0 | op(e2,e0) = e0 | op(e3,e0) = e0 ) & ( op(e0,e0) = e1 | op(e0,e1) = e1 | op(e0,e2) = e1 | op(e0,e3) = e1 ) & ( op(e0,e0) = e1 | op(e1,e0) = e1 | op(e2,e0) = e1 | op(e3,e0) = e1 ) & ( op(e0,e0) = e2 | op(e0,e1) = e2 | op(e0,e2) = e2 | op(e0,e3) = e2 ) & ( op(e0,e0) = e2 | op(e1,e0) = e2 | op(e2,e0) = e2 | op(e3,e0) = e2 ) & ( op(e0,e0) = e3 | op(e0,e1) = e3 | op(e0,e2) = e3 | op(e0,e3) = e3 ) & ( op(e0,e0) = e3 | op(e1,e0) = e3 | op(e2,e0) = e3 | op(e3,e0) = e3 ) & ( op(e1,e0) = e0 | op(e1,e1) = e0 | op(e1,e2) = e0 | op(e1,e3) = e0 ) & ( op(e0,e1) = e0 | op(e1,e1) = e0 | op(e2,e1) = e0 | op(e3,e1) = e0 ) & ( op(e1,e0) = e1 | op(e1,e1) = e1 | op(e1,e2) = e1 | op(e1,e3) = e1 ) & ( op(e0,e1) = e1 | op(e1,e1) = e1 | op(e2,e1) = e1 | op(e3,e1) = e1 ) & ( op(e1,e0) = e2 | op(e1,e1) = e2 | op(e1,e2) = e2 | op(e1,e3) = e2 ) & ( op(e0,e1) = e2 | op(e1,e1) = e2 | op(e2,e1) = e2 | op(e3,e1) = e2 ) & ( op(e1,e0) = e3 | op(e1,e1) = e3 | op(e1,e2) = e3 | op(e1,e3) = e3 ) & ( op(e0,e1) = e3 | op(e1,e1) = e3 | op(e2,e1) = e3 | op(e3,e1) = e3 ) & ( op(e2,e0) = e0 | op(e2,e1) = e0 | op(e2,e2) = e0 | op(e2,e3) = e0 ) & ( op(e0,e2) = e0 | op(e1,e2) = e0 | op(e2,e2) = e0 | op(e3,e2) = e0 ) & ( op(e2,e0) = e1 | op(e2,e1) = e1 | op(e2,e2) = e1 | op(e2,e3) = e1 ) & ( op(e0,e2) = e1 | op(e1,e2) = e1 | op(e2,e2) = e1 | op(e3,e2) = e1 ) & ( op(e2,e0) = e2 | op(e2,e1) = e2 | op(e2,e2) = e2 | op(e2,e3) = e2 ) & ( op(e0,e2) = e2 | op(e1,e2) = e2 | op(e2,e2) = e2 | op(e3,e2) = e2 ) & ( op(e2,e0) = e3 | op(e2,e1) = e3 | op(e2,e2) = e3 | op(e2,e3) = e3 ) & ( op(e0,e2) = e3 | op(e1,e2) = e3 | op(e2,e2) = e3 | op(e3,e2) = e3 ) & ( op(e3,e0) = e0 | op(e3,e1) = e0 | op(e3,e2) = e0 | op(e3,e3) = e0 ) & ( op(e0,e3) = e0 | op(e1,e3) = e0 | op(e2,e3) = e0 | op(e3,e3) = e0 ) & ( op(e3,e0) = e1 | op(e3,e1) = e1 | op(e3,e2) = e1 | op(e3,e3) = e1 ) & ( op(e0,e3) = e1 | op(e1,e3) = e1 | op(e2,e3) = e1 | op(e3,e3) = e1 ) & ( op(e3,e0) = e2 | op(e3,e1) = e2 | op(e3,e2) = e2 | op(e3,e3) = e2 ) & ( op(e0,e3) = e2 | op(e1,e3) = e2 | op(e2,e3) = e2 | op(e3,e3) = e2 ) & ( op(e3,e0) = e3 | op(e3,e1) = e3 | op(e3,e2) = e3 | op(e3,e3) = e3 ) & ( op(e0,e3) = e3 | op(e1,e3) = e3 | op(e2,e3) = e3 | op(e3,e3) = e3 ) )). end_of_list. %------------------------------------------------------------------------------