% benchmark parameters -n2 -N6 -p %-------------------------------------------------------------------------- % File : LCL136-1 : TPTP v2.3.0. Released v1.0.0. % Domain : Logic Calculi (Wajsberg Algebra) % Problem : A lemma in Wajsberg algebras % Version : [Bon91] (equality) axioms. % English : An axiomatisation of the many valued sentential calculus % is {MV-1,MV-2,MV-3,MV-5} by Meredith. Wajsberg provided % a different axiomatisation. Show that a version of MV-2 % depends on the Wajsberg system. % Refs : [FRT84] Font et al. (1984), Wajsberg Algebras % : [Bon91] Bonacina (1991), Problems in Lukasiewicz Logic % : [MW92] McCune & Wos (1992), Experiments in Automated Deductio % Source : [Bon91] % Names : Lemma 5 [Bon91] % Status : satisfiable % Rating : 0.67 v2.2.1, 0.75 v2.2.0, 0.67 v2.1.0, 1.00 v2.0.0 % Syntax : Number of clauses : 7 ( 0 non-Horn; 7 unit; 2 RR) % Number of literals : 7 ( 7 equality) % Maximal clause size : 1 ( 1 average) % Number of predicates : 1 ( 0 propositional; 2-2 arity) % Number of functors : 6 ( 4 constant; 0-2 arity) % Number of variables : 9 ( 0 singleton) % Maximal term depth : 4 ( 2 average) % Comments : % : tptp2X -f otter:hypothesis:[set(tptp_eq),set(auto),clear(print_given)] -t rm_equality:stfp LCL136-1.p %-------------------------------------------------------------------------- set(prolog_style_variables). set(tptp_eq). set(auto). clear(print_given). list(usable). % reflexivity, axiom. equal(X, X). % wajsberg_1, axiom. equal(implies(true, X), X). % wajsberg_2, axiom. equal(implies(implies(X, Y), implies(implies(Y, Z), implies(X, Z))), true). % wajsberg_3, axiom. equal(implies(implies(X, Y), Y), implies(implies(Y, X), X)). % wajsberg_4, axiom. equal(implies(implies(not(X), not(Y)), implies(Y, X)), true). end_of_list. list(sos). % lemma_antecedent, conjecture. equal(implies(x, y), implies(y, z)). % prove_wajsberg_lemma, conjecture. -equal(implies(x, z), true). end_of_list. %--------------------------------------------------------------------------