%------------------------------------------------------------------------------
% File : LisaTT---0.9.1
% Problem : LCL491+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 : n001.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:30 PM UTC 2025
% Result : Theorem 32.73s 18.51s
% Output : Proof 33.20s
% 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(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(principia_r5,axiom,
r5 ).
fof(r1,axiom,
( r1
<=> ! [P] : is_a_theorem(implies(or(P,P),P)) ) ).
fof(principia_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(principia_r1,axiom,
r1 ).
fof(or_2,axiom,
( or
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ) ).
fof(principia_r4,axiom,
r4 ).
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(principia_op_implies_or,axiom,
op_implies_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(principia_r2,axiom,
r2 ).
fof(modus_ponens,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(X)
& is_a_theorem(implies(X,Y)) )
=> is_a_theorem(Y) ) ) ).
fof(principia_op_and,axiom,
op_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(and_3,axiom,
( and
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ) ).
fof(use_substitution_of_equivalents,axiom,
substitution_of_equivalents ).
fof(principia_r3,axiom,
r3 ).
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(principia_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,
( [ or,~ or ]
--> [ ] ),
inference(restate_true,[status(thm)],[]) ).
fof(s1,plain,
( [ r2,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ]
--> [ ] ),
inference(subproof,[status(thm)],[]) ).
fof(s2,plain,
( [ ~ or,r2,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ) ]
--> [ ] ),
inference(left_or,[status(thm)],[s0,s1]) ).
fof(s3,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2 ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s2]) ).
fof(s4,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s3]) ).
fof(s5,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s4]) ).
fof(s6,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)],[s5]) ).
fof(s7,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s6]) ).
fof(s8,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ 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)],[s7]) ).
fof(s9,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s8]) ).
fof(s10,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s9]) ).
fof(s11,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s10]) ).
fof(s12,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s11]) ).
fof(s13,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s12]) ).
fof(s14,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s13]) ).
fof(s15,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s14]) ).
fof(s16,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s15]) ).
fof(s17,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s16]) ).
fof(s18,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s17]) ).
fof(s19,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s18]) ).
fof(s20,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5 ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s19]) ).
fof(s21,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s20]) ).
fof(s22,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s21]) ).
fof(s23,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1 ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s22]) ).
fof(s24,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s23]) ).
fof(s25,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( equivalence
| ? [X,Y] : ~ is_a_theorem(implies(equiv(X,Y),implies(Y,X))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s24]) ).
fof(s26,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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)],[s25]) ).
fof(s27,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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)],[s26]) ).
fof(s28,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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)],[s27]) ).
fof(s29,plain,
( [ ~ or,
( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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)],[s28]) ).
fof(s30,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s29]) ).
fof(s31,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( or
| ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s30]) ).
fof(s32,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s31]) ).
fof(s33,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s32]) ).
fof(s34,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s33]) ).
fof(s35,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s34]) ).
fof(s36,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s35]) ).
fof(s37,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s36]) ).
fof(s38,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s37]) ).
fof(s39,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& op_or ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s38]) ).
fof(s40,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& op_or
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s39]) ).
fof(s41,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& op_or
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s40]) ).
fof(s42,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& op_or
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( 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)],[s41]) ).
fof(s43,plain,
( [ ~ or,
( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& op_or
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( 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))) )
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) ) ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s42]) ).
fof(s44,plain,
( [ ( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& op_or
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( 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))) )
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ~ or ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s43]) ).
fof(s45,plain,
( [ ( op_and
& op_equiv
& ( ~ 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))) )
& ( ~ kn2
| ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) )
& ( kn2
| ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P)) )
& r4
& ( ~ kn1
| ! [P] : is_a_theorem(implies(P,and(P,P))) )
& ( kn1
| ? [P] : ~ is_a_theorem(implies(P,and(P,P))) )
& ( ~ kn3
| ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( kn3
| ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) )
& ( ~ op_implies_and
| ! [X,Y] : not(and(X,not(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)))) )
& ( ~ 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))) )
& r3
& ( ~ 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 ) )
& r2
& ( ~ r4
| ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) )
& ( ~ 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)))) )
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) )
& ( ~ r3
| ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) )
& substitution_of_equivalents
& ( ~ and
| ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) )
& ( and
| ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X)) )
& ( ~ or
| ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) )
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) )
& ( ~ op_implies_or
| ! [X,Y] : or(not(X),Y) = implies(X,Y) )
& op_implies_and
& ( or
| ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) )
& ( ~ op_and
| ! [X,Y] : not(or(not(X),not(Y))) = and(X,Y) )
& op_implies_or
& r5
& ( implies
| ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) )
& ( ~ implies
| ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) )
& r1
& ( ~ r1
| ! [P] : is_a_theorem(implies(or(P,P),P)) )
& ( 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) )
& ( ~ r2
| ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) )
& ( 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)))) )
& ( cn3
| ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ cn3
| ! [P] : is_a_theorem(implies(implies(not(P),P),P)) )
& ( ~ modus_ponens
| ! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) )
& modus_ponens
& ( cn2
| ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q))) )
& ( ~ cn2
| ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) )
& op_or
& ( ~ op_or
| ! [X,Y] : not(and(not(X),not(Y))) = or(X,Y) )
& ( 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))) )
& ( ~ r5
| ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) )
& ~ or ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s44]) ).
fof(s46,plain,
( [ r1,
( 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)) ),
( 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))) ),
( kn1
<=> ! [P] : is_a_theorem(implies(P,and(P,P))) ),
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(X)
& is_a_theorem(implies(X,Y)) )
=> is_a_theorem(Y) ) ),
( kn2
<=> ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
r3,
( 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,op_and,
( r1
<=> ! [P] : is_a_theorem(implies(or(P,P),P)) ),
( r2
<=> ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
r4,
( 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,
( implies
<=> ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
( kn3
<=> ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(not(and(Q,R)),not(and(R,P))))) ),
op_implies_or,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))) ),
r5 ]
--> [ or ] ),
inference(restate,[status(thm)],[s45]) ).
fof(final,theorem,
or,
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,principia_op_implies_or,principia_op_and,principia_op_equiv,principia_modus_ponens,principia_r1,principia_r2,principia_r3,principia_r4,principia_r5,use_substitution_of_equivalents]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : LCL491+1 : TPTP v9.2.0. Bugfixed v9.2.0.
% 0.11/0.13 % Command : java -cp /export/starexec/sandbox/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n001.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Sep 30 12:44:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 32.73/18.51 % SZS status Theorem
% 33.20/18.61 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------