;-------------------------------------------------------------------------- ; File : LCL024-1 : TPTP v2.2.0. Released v1.0.0. ; Domain : Logic Calculi (Equivalential) ; Problem : PYO depends on XGK ; Version : [Ove90] axioms. ; English : Show that Kalman's shortest single axiom for the ; equivalential calculus, XGK, can be derived from the Meredith ; single axiom PYO. ; Refs : [Wos88] Wos (1988), Automated Reasoning - 33 Basic Research Pr ; : [Ove90] Overbeek (1990), ATP competition announced at CADE-10 ; : [Ove93] Overbeek (1993), The CADE-11 Competitions: A Personal ; : [LM93] Lusk & McCune (1993), Uniform Strategies: The CADE-11 ; Source : [Ove90] ; Names : Test Problem 16 [Wos88] ; : XGK and Equivalential Calculus [Wos88] ; : CADE-11 Competition 4 [Ove90] ; : THEOREM 4 [LM93] ; Status : unsatisfiable ; Rating : 0.78 v2.2.0, 0.89 v2.1.0, 0.75 v2.0.0 ; Syntax : Number of clauses : 3 ( 0 non-Horn; 2 unit; 2 RR) ; Number of literals : 5 ( 0 equality) ; Maximal clause size : 3 ( 1 average) ; Number of predicates : 1 ( 0 propositional; 1-1 arity) ; Number of functors : 4 ( 3 constant; 0-2 arity) ; Number of variables : 5 ( 0 singleton) ; Maximal term depth : 5 ( 2 average) ; Comments : ; : tptp2X -f kif -t rm_equality:rstfp LCL024-1.p ;-------------------------------------------------------------------------- ; condensed_detachment, axiom. (or (not (is_a_theorem (equivalent ?A ?B))) (not (is_a_theorem ?A)) (is_a_theorem ?B)) ; prove_xgk, axiom. (or (is_a_theorem (equivalent ?A (equivalent (equivalent ?B (equivalent ?C ?A)) (equivalent ?C ?B))))) ; prove_pyo, conjecture. (or (not (is_a_theorem (equivalent (equivalent (equivalent a (equivalent b c)) c) (equivalent b a))))) ;--------------------------------------------------------------------------