%------------------------------------------------------------------------------ % File : LCL107-1 : TPTP v3.3.0. Released v1.0.0. % Domain : Logic Calculi (Left group) % Problem : P-1 depends on the single McCune axiom % Version : [McC92b] axioms. % English : Axiomatisations of the left group calculus are {LG-1, % LG-2,LG-3,LG-4,LG-5} by Kalman, {LG-2,LG-3}, {LG-2,P-1}, % {LG-2,P-4}, {LG-2,Q-1,Q-2}, {P-1,Q-3}, {P-4,Q-3}, {Q-1, % Q-2,Q-3}, {Q-1,Q-3,Q-4}, {LG-27-1690} all by McCune. Show % that P-1 depends on the single McCune axiom. % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio % : [McC92a] McCune (1992), Automated Discovery of New Axiomatisat % : [McC92b] McCune (1992), Email to G. Sutcliffe % Source : [McC92b] % Names : LG-100 [MW92] % Status : Unsatisfiable % Rating : 0.00 v2.2.1, 0.11 v2.1.0, 0.13 v2.0.0 % Syntax : Number of clauses : 3 ( 0 non-Horn; 2 unit; 2 RR) % Number of atoms : 5 ( 0 equality) % Maximal clause size : 3 ( 2 average) % Number of predicates : 1 ( 0 propositional; 1-1 arity) % Number of functors : 5 ( 4 constant; 0-2 arity) % Number of variables : 9 ( 0 singleton) % Maximal term depth : 7 ( 3 average) % Comments : % : tptp2X -f tptp:short LCL107-1.p %------------------------------------------------------------------------------ cnf(condensed_detachment,axiom, ( ~ is_a_theorem(equivalent(X,Y)) | ~ is_a_theorem(X) | is_a_theorem(Y) )). cnf(lg_27_1690,axiom,( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),Z),equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),V6))),equivalent(Z,equivalent(equivalent(Y,X),V6)))) )). cnf(prove_p_1,negated_conjecture,( ~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(equivalent(e,b),equivalent(equivalent(a,e),c)))) )). %------------------------------------------------------------------------------