%------------------------------------------------------------------------------
% File : LisaTT---0.9.1
% Problem : LCL506+1 : TPTP v9.2.0. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 1 12:41:31 PM UTC 2025
% Result : Theorem 25.95s 13.74s
% Output : Proof 26.37s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(hilbert_op_or,axiom,
op_or ).
fof(modus_tollens,axiom,
( modus_tollens
<=> ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ) ).
fof(and_2,axiom,
( and
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ) ).
fof(or_3,axiom,
( or
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) ) ).
fof(hilbert_op_implies_and,axiom,
op_implies_and ).
fof(implies_1,axiom,
( implies
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) ) ).
fof(and_1,axiom,
( and
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) ) ).
fof(hilbert_op_equiv,axiom,
op_equiv ).
fof(or_1,axiom,
( or
<=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ) ).
fof(kn1,axiom,
( kn1
<=> ! [P] : is_a_theorem(implies(P,and(P,P))) ) ).
fof(and_3,axiom,
( and
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ) ).
fof(implies_3,axiom,
( implies
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ) ).
fof(substitution_of_equivalents,axiom,
( substitution_of_equivalents
<=> ! [X,Y] :
( is_a_theorem(equiv(X,Y))
=> X = Y ) ) ).
fof(equivalence_1,axiom,
( equivalence
<=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) ) ).
fof(r1,axiom,
( r1
<=> ! [P] : is_a_theorem(implies(or(P,P),P)) ) ).
fof(rosser_modus_ponens,axiom,
modus_ponens ).
fof(r2,axiom,
( r2
<=> ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ) ).
fof(kn3,axiom,
( kn3
<=> ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) ) ).
fof(op_or,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ) ).
fof(cn1,axiom,
( cn1
<=> ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) ) ).
fof(op_equiv,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ) ).
fof(r5,axiom,
( r5
<=> ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) ) ).
fof(rosser_kn1,axiom,
kn1 ).
fof(or_2,axiom,
( or
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ) ).
fof(use_substitution_of_equivalents,axiom,
substitution_of_equivalents ).
fof(equivalence_3,axiom,
( equivalence
<=> ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ) ).
fof(op_implies_or,axiom,
( op_implies_or
=> ! [X,Y] : implies(X,Y) = or(not(X),Y) ) ).
fof(rosser_op_or,axiom,
op_or ).
fof(cn2,axiom,
( cn2
<=> ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) ) ).
fof(r4,axiom,
( r4
<=> ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) ) ).
fof(implies_2,axiom,
( implies
<=> ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ) ).
fof(rosser_kn2,axiom,
kn2 ).
fof(modus_ponens,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(X)
& is_a_theorem(implies(X,Y)) )
=> is_a_theorem(Y) ) ) ).
fof(rosser_op_implies_and,axiom,
op_implies_and ).
fof(equivalence_2,axiom,
( equivalence
<=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) ) ).
fof(op_implies_and,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ) ).
fof(rosser_kn3,axiom,
kn3 ).
fof(r3,axiom,
( r3
<=> ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) ) ).
fof(cn3,axiom,
( cn3
<=> ! [P] : is_a_theorem(implies(implies(not(P),P),P)) ) ).
fof(rosser_op_equiv,axiom,
op_equiv ).
fof(op_and,axiom,
( op_and
=> ! [X,Y] : and(X,Y) = not(or(not(X),not(Y))) ) ).
fof(kn2,axiom,
( kn2
<=> ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ) ).
fof(s0,plain,
( [ and,~ and ]
--> [ ] ),
inference(restate_true,[status(thm)],[]) ).
fof(s1,plain,
( [ kn2,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s2,plain,
( [ ~ and,kn2,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) ) ]
--> [ ] ),
inference(left_or,[status(thm)],[s0,s1]) ).
fof(s3,plain,
( [ ~ and,kn2,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s2]) ).
fof(s4,plain,
( [ ~ and,kn2,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s3]) ).
fof(s5,plain,
( [ ~ and,kn2,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s4]) ).
fof(s6,plain,
( [ ~ and,kn2,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s5]) ).
fof(s7,plain,
( [ ~ and,kn2,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s6]) ).
fof(s8,plain,
( [ ~ and,kn2,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s7]) ).
fof(s9,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2 ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s8]) ).
fof(s10,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s9]) ).
fof(s11,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s10]) ).
fof(s12,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s11]) ).
fof(s13,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s12]) ).
fof(s14,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s13]) ).
fof(s15,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s14]) ).
fof(s16,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s15]) ).
fof(s17,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s16]) ).
fof(s18,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s17]) ).
fof(s19,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s18]) ).
fof(s20,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s19]) ).
fof(s21,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s20]) ).
fof(s22,plain,
( [ ~ and,
( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& kn3 ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s21]) ).
fof(s23,plain,
( [ ~ and,
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& kn3
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s22]) ).
fof(s24,plain,
( [ ~ and,
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& kn3
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& kn1 ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s23]) ).
fof(s25,plain,
( [ ~ and,
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& kn3
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& kn1
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s24]) ).
fof(s26,plain,
( [ ~ and,
( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& kn3
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& kn1
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s25]) ).
fof(s27,plain,
( [ ( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& kn3
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& kn1
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) )
& ~ and ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s26]) ).
fof(s28,plain,
( [ ( op_equiv
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( ~ modus_tollens
| ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& ( modus_tollens
| ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )
& op_or
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& modus_ponens
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ or
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( r2
| ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q))) )
& ( ~ cn1
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( cn1
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) )
& ( ~ substitution_of_equivalents
| ! [X,Y] :
( ~ is_a_theorem(equiv(X,Y))
| Y = X ) )
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( r1
| ? [P] : ~ is_a_theorem(implies(or(P,P),P)) )
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( r4
| ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& substitution_of_equivalents
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( r5
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& op_implies_and
& ( r3
| ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
& kn2
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) )
& ( implies
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ implies
| ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )
& ( ~ op_equiv
| ! [X,Y] : and(implies(X,Y),implies(Y,X)) = equiv(X,Y) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ equivalence
| ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(Y))) = implies(X,Y) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& kn3
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& kn1
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) )
& ~ and ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s27]) ).
fof(s29,plain,
( [ ( kn2
<=> ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
( equivalence
<=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(X,Y))) ),
op_or,
( and
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ),
kn1,
( r5
<=> ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) ),
( cn2
<=> ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) ),
kn2,
( kn1
<=> ! [P] : is_a_theorem(implies(P,and(P,P))) ),
( r1
<=> ! [P] : is_a_theorem(implies(or(P,P),P)) ),
kn3,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(X)
& is_a_theorem(implies(X,Y)) )
=> is_a_theorem(Y) ) ),
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
( op_and
=> ! [X,Y] : and(X,Y) = not(or(not(X),not(Y))) ),
( and
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ),
( implies
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) ),
( r4
<=> ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) ),
( cn1
<=> ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) ),
( modus_tollens
<=> ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ),
op_equiv,
( or
<=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ),
( op_implies_or
=> ! [X,Y] : implies(X,Y) = or(not(X),Y) ),
modus_ponens,
( r3
<=> ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) ),
( r2
<=> ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( cn3
<=> ! [P] : is_a_theorem(implies(implies(not(P),P),P)) ),
( substitution_of_equivalents
<=> ! [X,Y] :
( is_a_theorem(equiv(X,Y))
=> X = Y ) ),
op_implies_and,
( kn3
<=> ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) ),
( implies
<=> ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
substitution_of_equivalents,
( equivalence
<=> ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ),
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
( implies
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ),
( equivalence
<=> ! [X,Y] : is_a_theorem(implies(equiv(X,Y),implies(Y,X))) ),
( and
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) ),
( or
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ),
( or
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) ),
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ) ]
--> [ and ] ),
inference(restate,[status(thm)],[s28]) ).
fof(final,theorem,
and,
inference(big_cut,[status(thm)],[hilbert_op_or,hilbert_op_implies_and,hilbert_op_equiv,modus_ponens,substitution_of_equivalents,modus_tollens,implies_1,implies_2,implies_3,and_1,and_2,and_3,or_1,or_2,or_3,equivalence_1,equivalence_2,equivalence_3,kn1,kn2,kn3,cn1,cn2,cn3,r1,r2,r3,r4,r5,op_or,op_and,op_implies_and,op_implies_or,op_equiv,rosser_op_or,rosser_op_implies_and,rosser_op_equiv,rosser_modus_ponens,rosser_kn1,rosser_kn2,rosser_kn3,use_substitution_of_equivalents]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : LCL506+1 : TPTP v9.2.0. Bugfixed v9.2.0.
% 0.08/0.12 % Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Sep 30 13:27:08 EDT 2025
% 0.12/0.34 % CPUTime :
% 25.95/13.74 % SZS status Theorem
% 26.37/13.83 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------