assign(max_seconds, 30). %------------------------------------------------------------------------------ % File : SYN551+2 : TPTP v3.0.1. Bugfixed v3.1.0. % Domain : Syntactic (Translated) % Problem : Cute Little Problem % Version : Especial. % English : % Refs : [Pra93] Prasetya (1993), How to get FAUST? % : [Jon93] Jones (1993), Little Problem, Solved by Otter % Source : [Pra93] % Names : % Status : Theorem % Rating : 0.56 v2.7.0, 0.67 v2.6.0, 0.50 v2.5.0, 0.43 v2.4.0 % Syntax : Number of formulae : 1 ( 0 unit) % Number of atoms : 4 ( 4 equality) % Maximal formula depth : 5 ( 5 average) % Number of connectives : 3 ( 0 ~ ; 0 |; 0 &) % ( 3 <=>; 0 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 1 ( 0 propositional; 2-2 arity) % Number of functors : 2 ( 0 constant; 1-1 arity) % Number of variables : 4 ( 0 singleton; 2 !; 2 ?) % Maximal term depth : 3 ( 2 average) % Comments : This is a HOL problem translated to FOF. The original HOL is % (?!x. x=f(g x)) = (?!y. y=g(f y)), where ?! means "there exists % a unique". % : tptp2X -f mace4 SYN551+2.p % Bugfixes : v2.3.0 - Equality axioms added. % : v3.1.0 - Removed remaining equality axioms (for TPTP v3.0.0) %------------------------------------------------------------------------------ %----NOTE WELL: conjecture has been negated set(prolog_style_variables). formulas(assumptions). % prove_this_cute_thing, negated_conjecture. -(( ( exists X ( all Y ( Y = f(g(Y)) <-> X = Y ) ) ) <-> ( exists X ( all Y ( Y = g(f(Y)) <-> X = Y ) ) ) )). end_of_list. %------------------------------------------------------------------------------