Metis---2.4.THM-CRf.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : LCL523+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n003.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Mon Sep  7 12:42:51 PM UTC 2026

% Result   : Theorem 49.25s 49.57s
% Output   : CNFRefutation 49.35s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   61
%            Number of leaves      :   75
% Syntax   : Number of formulae    :  390 ( 195 unt;   0 def)
%            Number of atoms       :  677 ( 284 equ)
%            Maximal formula atoms :   10 (   1 avg)
%            Number of connectives :  550 ( 263   ~; 235   |;  20   &)
%                                         (  26 <=>;   6  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   10 (   2 avg)
%            Maximal term depth    :    6 (   2 avg)
%            Number of predicates  :   21 (  18 usr;  18 prp; 0-2 aty)
%            Number of functors    :   30 (  30 usr;  23 con; 0-2 aty)
%            Number of variables   :  451 (  11 sgn  89   !;  23   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(modus_ponens,axiom,
    ( modus_ponens
  <=> ! [X,Y] :
        ( ( is_a_theorem(X)
          & is_a_theorem(implies(X,Y)) )
       => is_a_theorem(Y) ) ) ).

fof(substitution_of_equivalents,axiom,
    ( substitution_of_equivalents
  <=> ! [X,Y] :
        ( is_a_theorem(equiv(X,Y))
       => X = Y ) ) ).

fof(modus_tollens,axiom,
    ( modus_tollens
  <=> ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ) ).

fof(implies_1,axiom,
    ( implies_1
  <=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) ) ).

fof(implies_2,axiom,
    ( implies_2
  <=> ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ) ).

fof(and_2,axiom,
    ( and_2
  <=> ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ) ).

fof(and_3,axiom,
    ( and_3
  <=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ) ).

fof(or_1,axiom,
    ( or_1
  <=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ) ).

fof(or_2,axiom,
    ( or_2
  <=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ) ).

fof(equivalence_3,axiom,
    ( equivalence_3
  <=> ! [X,Y] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ) ).

fof(op_or,axiom,
    ( op_or
   => ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ) ).

fof(op_implies_and,axiom,
    ( op_implies_and
   => ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ) ).

fof(op_equiv,axiom,
    ( op_equiv
   => ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ) ).

fof(hilbert_op_or,axiom,
    op_or ).

fof(hilbert_op_implies_and,axiom,
    op_implies_and ).

fof(hilbert_op_equiv,axiom,
    op_equiv ).

fof(hilbert_modus_ponens,axiom,
    modus_ponens ).

fof(hilbert_modus_tollens,axiom,
    modus_tollens ).

fof(hilbert_implies_1,axiom,
    implies_1 ).

fof(hilbert_implies_2,axiom,
    implies_2 ).

fof(hilbert_and_2,axiom,
    and_2 ).

fof(hilbert_and_3,axiom,
    and_3 ).

fof(hilbert_or_1,axiom,
    or_1 ).

fof(hilbert_or_2,axiom,
    or_2 ).

fof(hilbert_equivalence_3,axiom,
    equivalence_3 ).

fof(use_substitution_of_equivalents,axiom,
    substitution_of_equivalents ).

fof(axiom_M,axiom,
    ( axiom_M
  <=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ) ).

fof(axiom_4,axiom,
    ( axiom_4
  <=> ! [X] : is_a_theorem(implies(necessarily(X),necessarily(necessarily(X)))) ) ).

fof(axiom_5,axiom,
    ( axiom_5
  <=> ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) ) ).

fof(op_possibly,axiom,
    ( op_possibly
   => ! [X] : possibly(X) = not(necessarily(not(X))) ) ).

fof(km5_op_possibly,axiom,
    op_possibly ).

fof(km5_axiom_M,axiom,
    axiom_M ).

fof(km5_axiom_5,axiom,
    axiom_5 ).

fof(km4b_axiom_4,conjecture,
    axiom_4 ).

fof(subgoal_0,plain,
    axiom_4,
    inference(strip,[],[km4b_axiom_4]) ).

fof(negate_0_0,plain,
    ~ axiom_4,
    inference(negate,[],[subgoal_0]) ).

fof(normalize_0_0,plain,
    ( ~ axiom_4
  <=> ? [X] : ~ is_a_theorem(implies(necessarily(X),necessarily(necessarily(X)))) ),
    inference(canonicalize,[],[axiom_4]) ).

fof(normalize_0_1,plain,
    ! [X] :
      ( ( ~ axiom_4
        | is_a_theorem(implies(necessarily(X),necessarily(necessarily(X)))) )
      & ( ~ is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))))
        | axiom_4 ) ),
    inference(clausify,[],[normalize_0_0]) ).

fof(normalize_0_2,plain,
    ( ~ is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))))
    | axiom_4 ),
    inference(conjunct,[],[normalize_0_1]) ).

fof(normalize_0_3,plain,
    ~ axiom_4,
    inference(canonicalize,[],[negate_0_0]) ).

fof(normalize_0_4,plain,
    ( ~ op_equiv
    | ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
    inference(canonicalize,[],[op_equiv]) ).

fof(normalize_0_5,plain,
    ! [X,Y] :
      ( ~ op_equiv
      | equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
    inference(clausify,[],[normalize_0_4]) ).

fof(normalize_0_6,plain,
    op_equiv,
    inference(canonicalize,[],[hilbert_op_equiv]) ).

fof(normalize_0_7,plain,
    ( ~ substitution_of_equivalents
  <=> ? [X,Y] :
        ( X != Y
        & is_a_theorem(equiv(X,Y)) ) ),
    inference(canonicalize,[],[substitution_of_equivalents]) ).

fof(normalize_0_8,plain,
    ! [X,Y] :
      ( ( skolemFOFtoCNF_X_1 != skolemFOFtoCNF_Y_1
        | substitution_of_equivalents )
      & ( is_a_theorem(equiv(skolemFOFtoCNF_X_1,skolemFOFtoCNF_Y_1))
        | substitution_of_equivalents )
      & ( ~ is_a_theorem(equiv(X,Y))
        | ~ substitution_of_equivalents
        | X = Y ) ),
    inference(clausify,[],[normalize_0_7]) ).

fof(normalize_0_9,plain,
    ! [X,Y] :
      ( ~ is_a_theorem(equiv(X,Y))
      | ~ substitution_of_equivalents
      | X = Y ),
    inference(conjunct,[],[normalize_0_8]) ).

fof(normalize_0_10,plain,
    substitution_of_equivalents,
    inference(canonicalize,[],[use_substitution_of_equivalents]) ).

fof(normalize_0_11,plain,
    ( ~ modus_ponens
  <=> ? [X,Y] :
        ( ~ is_a_theorem(Y)
        & is_a_theorem(X)
        & is_a_theorem(implies(X,Y)) ) ),
    inference(canonicalize,[],[modus_ponens]) ).

fof(normalize_0_12,plain,
    ! [X,Y] :
      ( ( ~ is_a_theorem(skolemFOFtoCNF_Y)
        | modus_ponens )
      & ( is_a_theorem(implies(skolemFOFtoCNF_X,skolemFOFtoCNF_Y))
        | modus_ponens )
      & ( is_a_theorem(skolemFOFtoCNF_X)
        | modus_ponens )
      & ( ~ is_a_theorem(X)
        | ~ is_a_theorem(implies(X,Y))
        | ~ modus_ponens
        | is_a_theorem(Y) ) ),
    inference(clausify,[],[normalize_0_11]) ).

fof(normalize_0_13,plain,
    ! [X,Y] :
      ( ~ is_a_theorem(X)
      | ~ is_a_theorem(implies(X,Y))
      | ~ modus_ponens
      | is_a_theorem(Y) ),
    inference(conjunct,[],[normalize_0_12]) ).

fof(normalize_0_14,plain,
    modus_ponens,
    inference(canonicalize,[],[hilbert_modus_ponens]) ).

fof(normalize_0_15,plain,
    ( ~ and_3
  <=> ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y)))) ),
    inference(canonicalize,[],[and_3]) ).

fof(normalize_0_16,plain,
    ! [X,Y] :
      ( ( ~ and_3
        | is_a_theorem(implies(X,implies(Y,and(X,Y)))) )
      & ( ~ is_a_theorem(implies(skolemFOFtoCNF_X_8,implies(skolemFOFtoCNF_Y_8,and(skolemFOFtoCNF_X_8,skolemFOFtoCNF_Y_8))))
        | and_3 ) ),
    inference(clausify,[],[normalize_0_15]) ).

fof(normalize_0_17,plain,
    ! [X,Y] :
      ( ~ and_3
      | is_a_theorem(implies(X,implies(Y,and(X,Y)))) ),
    inference(conjunct,[],[normalize_0_16]) ).

fof(normalize_0_18,plain,
    and_3,
    inference(canonicalize,[],[hilbert_and_3]) ).

fof(normalize_0_19,plain,
    ( ~ implies_2
  <=> ? [X,Y] : ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
    inference(canonicalize,[],[implies_2]) ).

fof(normalize_0_20,plain,
    ! [X,Y] :
      ( ( ~ implies_2
        | is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) )
      & ( ~ is_a_theorem(implies(implies(skolemFOFtoCNF_X_4,implies(skolemFOFtoCNF_X_4,skolemFOFtoCNF_Y_4)),implies(skolemFOFtoCNF_X_4,skolemFOFtoCNF_Y_4)))
        | implies_2 ) ),
    inference(clausify,[],[normalize_0_19]) ).

fof(normalize_0_21,plain,
    ! [X,Y] :
      ( ~ implies_2
      | is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
    inference(conjunct,[],[normalize_0_20]) ).

fof(normalize_0_22,plain,
    implies_2,
    inference(canonicalize,[],[hilbert_implies_2]) ).

fof(normalize_0_23,plain,
    ( ~ and_2
  <=> ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y)) ),
    inference(canonicalize,[],[and_2]) ).

fof(normalize_0_24,plain,
    ! [X,Y] :
      ( ( ~ and_2
        | is_a_theorem(implies(and(X,Y),Y)) )
      & ( ~ is_a_theorem(implies(and(skolemFOFtoCNF_X_7,skolemFOFtoCNF_Y_7),skolemFOFtoCNF_Y_7))
        | and_2 ) ),
    inference(clausify,[],[normalize_0_23]) ).

fof(normalize_0_25,plain,
    ! [X,Y] :
      ( ~ and_2
      | is_a_theorem(implies(and(X,Y),Y)) ),
    inference(conjunct,[],[normalize_0_24]) ).

fof(normalize_0_26,plain,
    and_2,
    inference(canonicalize,[],[hilbert_and_2]) ).

fof(normalize_0_27,plain,
    ( ~ axiom_5
  <=> ? [X] : ~ is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) ),
    inference(canonicalize,[],[axiom_5]) ).

fof(normalize_0_28,plain,
    ! [X] :
      ( ( ~ axiom_5
        | is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) )
      & ( ~ is_a_theorem(implies(possibly(skolemFOFtoCNF_X_23),necessarily(possibly(skolemFOFtoCNF_X_23))))
        | axiom_5 ) ),
    inference(clausify,[],[normalize_0_27]) ).

fof(normalize_0_29,plain,
    ! [X] :
      ( ~ axiom_5
      | is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) ),
    inference(conjunct,[],[normalize_0_28]) ).

fof(normalize_0_30,plain,
    axiom_5,
    inference(canonicalize,[],[km5_axiom_5]) ).

fof(normalize_0_31,plain,
    ( ~ axiom_M
  <=> ? [X] : ~ is_a_theorem(implies(necessarily(X),X)) ),
    inference(canonicalize,[],[axiom_M]) ).

fof(normalize_0_32,plain,
    ! [X] :
      ( ( ~ axiom_M
        | is_a_theorem(implies(necessarily(X),X)) )
      & ( ~ is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_20),skolemFOFtoCNF_X_20))
        | axiom_M ) ),
    inference(clausify,[],[normalize_0_31]) ).

fof(normalize_0_33,plain,
    ! [X] :
      ( ~ axiom_M
      | is_a_theorem(implies(necessarily(X),X)) ),
    inference(conjunct,[],[normalize_0_32]) ).

fof(normalize_0_34,plain,
    axiom_M,
    inference(canonicalize,[],[km5_axiom_M]) ).

fof(normalize_0_35,plain,
    ( ~ op_possibly
    | ! [X] : possibly(X) = not(necessarily(not(X))) ),
    inference(canonicalize,[],[op_possibly]) ).

fof(normalize_0_36,plain,
    ! [X] :
      ( ~ op_possibly
      | possibly(X) = not(necessarily(not(X))) ),
    inference(clausify,[],[normalize_0_35]) ).

fof(normalize_0_37,plain,
    op_possibly,
    inference(canonicalize,[],[km5_op_possibly]) ).

fof(normalize_0_38,plain,
    ( ~ op_or
    | ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
    inference(canonicalize,[],[op_or]) ).

fof(normalize_0_39,plain,
    ! [X,Y] :
      ( ~ op_or
      | or(X,Y) = not(and(not(X),not(Y))) ),
    inference(clausify,[],[normalize_0_38]) ).

fof(normalize_0_40,plain,
    op_or,
    inference(canonicalize,[],[hilbert_op_or]) ).

fof(normalize_0_41,plain,
    ( ~ op_implies_and
    | ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
    inference(canonicalize,[],[op_implies_and]) ).

fof(normalize_0_42,plain,
    ! [X,Y] :
      ( ~ op_implies_and
      | implies(X,Y) = not(and(X,not(Y))) ),
    inference(clausify,[],[normalize_0_41]) ).

fof(normalize_0_43,plain,
    op_implies_and,
    inference(canonicalize,[],[hilbert_op_implies_and]) ).

fof(normalize_0_44,plain,
    ( ~ or_2
  <=> ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y))) ),
    inference(canonicalize,[],[or_2]) ).

fof(normalize_0_45,plain,
    ! [X,Y] :
      ( ( ~ is_a_theorem(implies(skolemFOFtoCNF_Y_10,or(skolemFOFtoCNF_X_10,skolemFOFtoCNF_Y_10)))
        | or_2 )
      & ( ~ or_2
        | is_a_theorem(implies(Y,or(X,Y))) ) ),
    inference(clausify,[],[normalize_0_44]) ).

fof(normalize_0_46,plain,
    ! [X,Y] :
      ( ~ or_2
      | is_a_theorem(implies(Y,or(X,Y))) ),
    inference(conjunct,[],[normalize_0_45]) ).

fof(normalize_0_47,plain,
    or_2,
    inference(canonicalize,[],[hilbert_or_2]) ).

fof(normalize_0_48,plain,
    ( ~ modus_tollens
  <=> ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ),
    inference(canonicalize,[],[modus_tollens]) ).

fof(normalize_0_49,plain,
    ! [X,Y] :
      ( ( ~ is_a_theorem(implies(implies(not(skolemFOFtoCNF_Y_2),not(skolemFOFtoCNF_X_2)),implies(skolemFOFtoCNF_X_2,skolemFOFtoCNF_Y_2)))
        | modus_tollens )
      & ( ~ modus_tollens
        | is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ) ),
    inference(clausify,[],[normalize_0_48]) ).

fof(normalize_0_50,plain,
    ! [X,Y] :
      ( ~ modus_tollens
      | is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ),
    inference(conjunct,[],[normalize_0_49]) ).

fof(normalize_0_51,plain,
    modus_tollens,
    inference(canonicalize,[],[hilbert_modus_tollens]) ).

fof(normalize_0_52,plain,
    ( ~ or_1
  <=> ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y))) ),
    inference(canonicalize,[],[or_1]) ).

fof(normalize_0_53,plain,
    ! [X,Y] :
      ( ( ~ is_a_theorem(implies(skolemFOFtoCNF_X_9,or(skolemFOFtoCNF_X_9,skolemFOFtoCNF_Y_9)))
        | or_1 )
      & ( ~ or_1
        | is_a_theorem(implies(X,or(X,Y))) ) ),
    inference(clausify,[],[normalize_0_52]) ).

fof(normalize_0_54,plain,
    ! [X,Y] :
      ( ~ or_1
      | is_a_theorem(implies(X,or(X,Y))) ),
    inference(conjunct,[],[normalize_0_53]) ).

fof(normalize_0_55,plain,
    or_1,
    inference(canonicalize,[],[hilbert_or_1]) ).

fof(normalize_0_56,plain,
    ( ~ equivalence_3
  <=> ? [X,Y] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ),
    inference(canonicalize,[],[equivalence_3]) ).

fof(normalize_0_57,plain,
    ! [X,Y] :
      ( ( ~ equivalence_3
        | is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) )
      & ( ~ is_a_theorem(implies(implies(skolemFOFtoCNF_X_14,skolemFOFtoCNF_Y_14),implies(implies(skolemFOFtoCNF_Y_14,skolemFOFtoCNF_X_14),equiv(skolemFOFtoCNF_X_14,skolemFOFtoCNF_Y_14))))
        | equivalence_3 ) ),
    inference(clausify,[],[normalize_0_56]) ).

fof(normalize_0_58,plain,
    ! [X,Y] :
      ( ~ equivalence_3
      | is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ),
    inference(conjunct,[],[normalize_0_57]) ).

fof(normalize_0_59,plain,
    equivalence_3,
    inference(canonicalize,[],[hilbert_equivalence_3]) ).

fof(normalize_0_60,plain,
    ( ~ implies_1
  <=> ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X))) ),
    inference(canonicalize,[],[implies_1]) ).

fof(normalize_0_61,plain,
    ! [X,Y] :
      ( ( ~ implies_1
        | is_a_theorem(implies(X,implies(Y,X))) )
      & ( ~ is_a_theorem(implies(skolemFOFtoCNF_X_3,implies(skolemFOFtoCNF_Y_3,skolemFOFtoCNF_X_3)))
        | implies_1 ) ),
    inference(clausify,[],[normalize_0_60]) ).

fof(normalize_0_62,plain,
    ! [X,Y] :
      ( ~ implies_1
      | is_a_theorem(implies(X,implies(Y,X))) ),
    inference(conjunct,[],[normalize_0_61]) ).

fof(normalize_0_63,plain,
    implies_1,
    inference(canonicalize,[],[hilbert_implies_1]) ).

cnf(refute_0_0,plain,
    ( ~ is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))))
    | axiom_4 ),
    inference(canonicalize,[],[normalize_0_2]) ).

cnf(refute_0_1,plain,
    ~ axiom_4,
    inference(canonicalize,[],[normalize_0_3]) ).

cnf(refute_0_2,plain,
    ~ is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21)))),
    inference(resolve,[$cnf( axiom_4 )],[refute_0_0,refute_0_1]) ).

cnf(refute_0_3,plain,
    ( ~ op_equiv
    | equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
    inference(canonicalize,[],[normalize_0_5]) ).

cnf(refute_0_4,plain,
    op_equiv,
    inference(canonicalize,[],[normalize_0_6]) ).

cnf(refute_0_5,plain,
    equiv(X,Y) = and(implies(X,Y),implies(Y,X)),
    inference(resolve,[$cnf( op_equiv )],[refute_0_4,refute_0_3]) ).

cnf(refute_0_6,plain,
    equiv(Y,Y) = and(implies(Y,Y),implies(Y,Y)),
    inference(subst,[],[refute_0_5:[bind(X,$fot(Y))]]) ).

cnf(refute_0_7,plain,
    ( ~ is_a_theorem(equiv(X,Y))
    | ~ substitution_of_equivalents
    | X = Y ),
    inference(canonicalize,[],[normalize_0_9]) ).

cnf(refute_0_8,plain,
    substitution_of_equivalents,
    inference(canonicalize,[],[normalize_0_10]) ).

cnf(refute_0_9,plain,
    ( ~ is_a_theorem(equiv(X,Y))
    | X = Y ),
    inference(resolve,[$cnf( substitution_of_equivalents )],[refute_0_8,refute_0_7]) ).

cnf(refute_0_10,plain,
    ( ~ is_a_theorem(equiv(X_1876,and(X_1876,X_1876)))
    | X_1876 = and(X_1876,X_1876) ),
    inference(subst,[],[refute_0_9:[bind(X,$fot(X_1876)),bind(Y,$fot(and(X_1876,X_1876)))]]) ).

cnf(refute_0_11,plain,
    ( ~ is_a_theorem(X)
    | ~ is_a_theorem(implies(X,Y))
    | ~ modus_ponens
    | is_a_theorem(Y) ),
    inference(canonicalize,[],[normalize_0_13]) ).

cnf(refute_0_12,plain,
    modus_ponens,
    inference(canonicalize,[],[normalize_0_14]) ).

cnf(refute_0_13,plain,
    ( ~ is_a_theorem(X)
    | ~ is_a_theorem(implies(X,Y))
    | is_a_theorem(Y) ),
    inference(resolve,[$cnf( modus_ponens )],[refute_0_12,refute_0_11]) ).

cnf(refute_0_14,plain,
    ( ~ is_a_theorem(implies(and(X_1875,X_1875),X_1875))
    | ~ is_a_theorem(implies(implies(and(X_1875,X_1875),X_1875),equiv(X_1875,and(X_1875,X_1875))))
    | is_a_theorem(equiv(X_1875,and(X_1875,X_1875))) ),
    inference(subst,[],[refute_0_13:[bind(X,$fot(implies(and(X_1875,X_1875),X_1875))),bind(Y,$fot(equiv(X_1875,and(X_1875,X_1875))))]]) ).

cnf(refute_0_15,plain,
    ( ~ and_3
    | is_a_theorem(implies(X,implies(Y,and(X,Y)))) ),
    inference(canonicalize,[],[normalize_0_17]) ).

cnf(refute_0_16,plain,
    and_3,
    inference(canonicalize,[],[normalize_0_18]) ).

cnf(refute_0_17,plain,
    is_a_theorem(implies(X,implies(Y,and(X,Y)))),
    inference(resolve,[$cnf( and_3 )],[refute_0_16,refute_0_15]) ).

cnf(refute_0_18,plain,
    is_a_theorem(implies(X_435,implies(Y,and(X_435,Y)))),
    inference(subst,[],[refute_0_17:[bind(X,$fot(X_435))]]) ).

cnf(refute_0_19,plain,
    ( ~ is_a_theorem(X_435)
    | ~ is_a_theorem(implies(X_435,implies(Y,and(X_435,Y))))
    | is_a_theorem(implies(Y,and(X_435,Y))) ),
    inference(subst,[],[refute_0_13:[bind(X,$fot(X_435)),bind(Y,$fot(implies(Y,and(X_435,Y))))]]) ).

cnf(refute_0_20,plain,
    ( ~ is_a_theorem(X_435)
    | is_a_theorem(implies(Y,and(X_435,Y))) ),
    inference(resolve,[$cnf( is_a_theorem(implies(X_435,implies(Y,and(X_435,Y)))) )],[refute_0_18,refute_0_19]) ).

cnf(refute_0_21,plain,
    ( ~ is_a_theorem(implies(X_1735,and(X_1735,X_1735)))
    | is_a_theorem(implies(Y,and(implies(X_1735,and(X_1735,X_1735)),Y))) ),
    inference(subst,[],[refute_0_20:[bind(X_435,$fot(implies(X_1735,and(X_1735,X_1735))))]]) ).

cnf(refute_0_22,plain,
    is_a_theorem(implies(X_1730,implies(X_1730,and(X_1730,X_1730)))),
    inference(subst,[],[refute_0_17:[bind(X,$fot(X_1730)),bind(Y,$fot(X_1730))]]) ).

cnf(refute_0_23,plain,
    ( ~ implies_2
    | is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
    inference(canonicalize,[],[normalize_0_21]) ).

cnf(refute_0_24,plain,
    implies_2,
    inference(canonicalize,[],[normalize_0_22]) ).

cnf(refute_0_25,plain,
    is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))),
    inference(resolve,[$cnf( implies_2 )],[refute_0_24,refute_0_23]) ).

cnf(refute_0_26,plain,
    ( ~ is_a_theorem(implies(X,implies(X,Y)))
    | ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))
    | is_a_theorem(implies(X,Y)) ),
    inference(subst,[],[refute_0_13:[bind(X,$fot(implies(X,implies(X,Y)))),bind(Y,$fot(implies(X,Y)))]]) ).

cnf(refute_0_27,plain,
    ( ~ is_a_theorem(implies(X,implies(X,Y)))
    | is_a_theorem(implies(X,Y)) ),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) )],[refute_0_25,refute_0_26]) ).

cnf(refute_0_28,plain,
    ( ~ is_a_theorem(implies(X_1730,implies(X_1730,and(X_1730,X_1730))))
    | is_a_theorem(implies(X_1730,and(X_1730,X_1730))) ),
    inference(subst,[],[refute_0_27:[bind(X,$fot(X_1730)),bind(Y,$fot(and(X_1730,X_1730)))]]) ).

cnf(refute_0_29,plain,
    is_a_theorem(implies(X_1730,and(X_1730,X_1730))),
    inference(resolve,[$cnf( is_a_theorem(implies(X_1730,implies(X_1730,and(X_1730,X_1730)))) )],[refute_0_22,refute_0_28]) ).

cnf(refute_0_30,plain,
    is_a_theorem(implies(X_1735,and(X_1735,X_1735))),
    inference(subst,[],[refute_0_29:[bind(X_1730,$fot(X_1735))]]) ).

cnf(refute_0_31,plain,
    is_a_theorem(implies(Y,and(implies(X_1735,and(X_1735,X_1735)),Y))),
    inference(resolve,[$cnf( is_a_theorem(implies(X_1735,and(X_1735,X_1735))) )],[refute_0_30,refute_0_21]) ).

cnf(refute_0_32,plain,
    is_a_theorem(implies(implies(and(X_1874,X_1874),X_1874),and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874)))),
    inference(subst,[],[refute_0_31:[bind(Y,$fot(implies(and(X_1874,X_1874),X_1874))),bind(X_1735,$fot(X_1874))]]) ).

cnf(refute_0_33,plain,
    equiv(X_1874,and(X_1874,X_1874)) = and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874)),
    inference(subst,[],[refute_0_5:[bind(X,$fot(X_1874)),bind(Y,$fot(and(X_1874,X_1874)))]]) ).

cnf(refute_0_34,plain,
    X0 = X0,
    introduced(tautology,[refl,[$fot(X0)]]) ).

cnf(refute_0_35,plain,
    ( X0 != X0
    | X0 != Y0
    | Y0 = X0 ),
    introduced(tautology,[equality,[$cnf( $equal(X0,X0) ),[0],$fot(Y0)]]) ).

cnf(refute_0_36,plain,
    ( X0 != Y0
    | Y0 = X0 ),
    inference(resolve,[$cnf( $equal(X0,X0) )],[refute_0_34,refute_0_35]) ).

cnf(refute_0_37,plain,
    ( equiv(X_1874,and(X_1874,X_1874)) != and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874))
    | and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874)) = equiv(X_1874,and(X_1874,X_1874)) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(equiv(X_1874,and(X_1874,X_1874)))),bind(Y0,$fot(and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874))))]]) ).

cnf(refute_0_38,plain,
    and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874)) = equiv(X_1874,and(X_1874,X_1874)),
    inference(resolve,[$cnf( $equal(equiv(X_1874,and(X_1874,X_1874)),and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874))) )],[refute_0_33,refute_0_37]) ).

cnf(refute_0_39,plain,
    ( and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874)) != equiv(X_1874,and(X_1874,X_1874))
    | ~ is_a_theorem(implies(implies(and(X_1874,X_1874),X_1874),and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874))))
    | is_a_theorem(implies(implies(and(X_1874,X_1874),X_1874),equiv(X_1874,and(X_1874,X_1874)))) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(implies(implies(and(X_1874,X_1874),X_1874),and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874)))) ),[0,1],$fot(equiv(X_1874,and(X_1874,X_1874)))]]) ).

cnf(refute_0_40,plain,
    ( ~ is_a_theorem(implies(implies(and(X_1874,X_1874),X_1874),and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874))))
    | is_a_theorem(implies(implies(and(X_1874,X_1874),X_1874),equiv(X_1874,and(X_1874,X_1874)))) ),
    inference(resolve,[$cnf( $equal(and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874)),equiv(X_1874,and(X_1874,X_1874))) )],[refute_0_38,refute_0_39]) ).

cnf(refute_0_41,plain,
    is_a_theorem(implies(implies(and(X_1874,X_1874),X_1874),equiv(X_1874,and(X_1874,X_1874)))),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(and(X_1874,X_1874),X_1874),and(implies(X_1874,and(X_1874,X_1874)),implies(and(X_1874,X_1874),X_1874)))) )],[refute_0_32,refute_0_40]) ).

cnf(refute_0_42,plain,
    is_a_theorem(implies(implies(and(X_1875,X_1875),X_1875),equiv(X_1875,and(X_1875,X_1875)))),
    inference(subst,[],[refute_0_41:[bind(X_1874,$fot(X_1875))]]) ).

cnf(refute_0_43,plain,
    ( ~ is_a_theorem(implies(and(X_1875,X_1875),X_1875))
    | is_a_theorem(equiv(X_1875,and(X_1875,X_1875))) ),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(and(X_1875,X_1875),X_1875),equiv(X_1875,and(X_1875,X_1875)))) )],[refute_0_42,refute_0_14]) ).

cnf(refute_0_44,plain,
    ( ~ and_2
    | is_a_theorem(implies(and(X,Y),Y)) ),
    inference(canonicalize,[],[normalize_0_25]) ).

cnf(refute_0_45,plain,
    and_2,
    inference(canonicalize,[],[normalize_0_26]) ).

cnf(refute_0_46,plain,
    is_a_theorem(implies(and(X,Y),Y)),
    inference(resolve,[$cnf( and_2 )],[refute_0_45,refute_0_44]) ).

cnf(refute_0_47,plain,
    is_a_theorem(implies(and(X_1875,X_1875),X_1875)),
    inference(subst,[],[refute_0_46:[bind(X,$fot(X_1875)),bind(Y,$fot(X_1875))]]) ).

cnf(refute_0_48,plain,
    is_a_theorem(equiv(X_1875,and(X_1875,X_1875))),
    inference(resolve,[$cnf( is_a_theorem(implies(and(X_1875,X_1875),X_1875)) )],[refute_0_47,refute_0_43]) ).

cnf(refute_0_49,plain,
    is_a_theorem(equiv(X_1876,and(X_1876,X_1876))),
    inference(subst,[],[refute_0_48:[bind(X_1875,$fot(X_1876))]]) ).

cnf(refute_0_50,plain,
    X_1876 = and(X_1876,X_1876),
    inference(resolve,[$cnf( is_a_theorem(equiv(X_1876,and(X_1876,X_1876))) )],[refute_0_49,refute_0_10]) ).

cnf(refute_0_51,plain,
    implies(Y,Y) = and(implies(Y,Y),implies(Y,Y)),
    inference(subst,[],[refute_0_50:[bind(X_1876,$fot(implies(Y,Y)))]]) ).

cnf(refute_0_52,plain,
    ( implies(Y,Y) != and(implies(Y,Y),implies(Y,Y))
    | and(implies(Y,Y),implies(Y,Y)) = implies(Y,Y) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(implies(Y,Y))),bind(Y0,$fot(and(implies(Y,Y),implies(Y,Y))))]]) ).

cnf(refute_0_53,plain,
    and(implies(Y,Y),implies(Y,Y)) = implies(Y,Y),
    inference(resolve,[$cnf( $equal(implies(Y,Y),and(implies(Y,Y),implies(Y,Y))) )],[refute_0_51,refute_0_52]) ).

cnf(refute_0_54,plain,
    ( and(implies(Y,Y),implies(Y,Y)) != implies(Y,Y)
    | equiv(Y,Y) != and(implies(Y,Y),implies(Y,Y))
    | equiv(Y,Y) = implies(Y,Y) ),
    introduced(tautology,[equality,[$cnf( $equal(equiv(Y,Y),and(implies(Y,Y),implies(Y,Y))) ),[1],$fot(implies(Y,Y))]]) ).

cnf(refute_0_55,plain,
    ( equiv(Y,Y) != and(implies(Y,Y),implies(Y,Y))
    | equiv(Y,Y) = implies(Y,Y) ),
    inference(resolve,[$cnf( $equal(and(implies(Y,Y),implies(Y,Y)),implies(Y,Y)) )],[refute_0_53,refute_0_54]) ).

cnf(refute_0_56,plain,
    equiv(Y,Y) = implies(Y,Y),
    inference(resolve,[$cnf( $equal(equiv(Y,Y),and(implies(Y,Y),implies(Y,Y))) )],[refute_0_6,refute_0_55]) ).

cnf(refute_0_57,plain,
    ( equiv(Y,Y) != implies(Y,Y)
    | implies(Y,Y) = equiv(Y,Y) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(equiv(Y,Y))),bind(Y0,$fot(implies(Y,Y)))]]) ).

cnf(refute_0_58,plain,
    implies(Y,Y) = equiv(Y,Y),
    inference(resolve,[$cnf( $equal(equiv(Y,Y),implies(Y,Y)) )],[refute_0_56,refute_0_57]) ).

cnf(refute_0_59,plain,
    implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)) = equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)),
    inference(subst,[],[refute_0_58:[bind(Y,$fot(necessarily(skolemFOFtoCNF_X_21)))]]) ).

cnf(refute_0_60,plain,
    ( ~ is_a_theorem(equiv(possibly(X_1360),necessarily(possibly(X_1360))))
    | possibly(X_1360) = necessarily(possibly(X_1360)) ),
    inference(subst,[],[refute_0_9:[bind(X,$fot(possibly(X_1360))),bind(Y,$fot(necessarily(possibly(X_1360))))]]) ).

cnf(refute_0_61,plain,
    ( ~ is_a_theorem(implies(implies(necessarily(possibly(X_1359)),possibly(X_1359)),equiv(possibly(X_1359),necessarily(possibly(X_1359)))))
    | ~ is_a_theorem(implies(necessarily(possibly(X_1359)),possibly(X_1359)))
    | is_a_theorem(equiv(possibly(X_1359),necessarily(possibly(X_1359)))) ),
    inference(subst,[],[refute_0_13:[bind(X,$fot(implies(necessarily(possibly(X_1359)),possibly(X_1359)))),bind(Y,$fot(equiv(possibly(X_1359),necessarily(possibly(X_1359)))))]]) ).

cnf(refute_0_62,plain,
    ( ~ axiom_5
    | is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) ),
    inference(canonicalize,[],[normalize_0_29]) ).

cnf(refute_0_63,plain,
    axiom_5,
    inference(canonicalize,[],[normalize_0_30]) ).

cnf(refute_0_64,plain,
    is_a_theorem(implies(possibly(X),necessarily(possibly(X)))),
    inference(resolve,[$cnf( axiom_5 )],[refute_0_63,refute_0_62]) ).

cnf(refute_0_65,plain,
    ( ~ is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
    | is_a_theorem(implies(X_784,and(implies(possibly(X),necessarily(possibly(X))),X_784))) ),
    inference(subst,[],[refute_0_20:[bind(Y,$fot(X_784)),bind(X_435,$fot(implies(possibly(X),necessarily(possibly(X)))))]]) ).

cnf(refute_0_66,plain,
    is_a_theorem(implies(X_784,and(implies(possibly(X),necessarily(possibly(X))),X_784))),
    inference(resolve,[$cnf( is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) )],[refute_0_64,refute_0_65]) ).

cnf(refute_0_67,plain,
    is_a_theorem(implies(implies(necessarily(possibly(X_1357)),possibly(X_1357)),and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357))))),
    inference(subst,[],[refute_0_66:[bind(X,$fot(X_1357)),bind(X_784,$fot(implies(necessarily(possibly(X_1357)),possibly(X_1357))))]]) ).

cnf(refute_0_68,plain,
    equiv(possibly(X_1357),necessarily(possibly(X_1357))) = and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357))),
    inference(subst,[],[refute_0_5:[bind(X,$fot(possibly(X_1357))),bind(Y,$fot(necessarily(possibly(X_1357))))]]) ).

cnf(refute_0_69,plain,
    ( equiv(possibly(X_1357),necessarily(possibly(X_1357))) != and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357)))
    | and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357))) = equiv(possibly(X_1357),necessarily(possibly(X_1357))) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(equiv(possibly(X_1357),necessarily(possibly(X_1357))))),bind(Y0,$fot(and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357)))))]]) ).

cnf(refute_0_70,plain,
    and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357))) = equiv(possibly(X_1357),necessarily(possibly(X_1357))),
    inference(resolve,[$cnf( $equal(equiv(possibly(X_1357),necessarily(possibly(X_1357))),and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357)))) )],[refute_0_68,refute_0_69]) ).

cnf(refute_0_71,plain,
    ( and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357))) != equiv(possibly(X_1357),necessarily(possibly(X_1357)))
    | ~ is_a_theorem(implies(implies(necessarily(possibly(X_1357)),possibly(X_1357)),and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357)))))
    | is_a_theorem(implies(implies(necessarily(possibly(X_1357)),possibly(X_1357)),equiv(possibly(X_1357),necessarily(possibly(X_1357))))) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(implies(implies(necessarily(possibly(X_1357)),possibly(X_1357)),and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357))))) ),[0,1],$fot(equiv(possibly(X_1357),necessarily(possibly(X_1357))))]]) ).

cnf(refute_0_72,plain,
    ( ~ is_a_theorem(implies(implies(necessarily(possibly(X_1357)),possibly(X_1357)),and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357)))))
    | is_a_theorem(implies(implies(necessarily(possibly(X_1357)),possibly(X_1357)),equiv(possibly(X_1357),necessarily(possibly(X_1357))))) ),
    inference(resolve,[$cnf( $equal(and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357))),equiv(possibly(X_1357),necessarily(possibly(X_1357)))) )],[refute_0_70,refute_0_71]) ).

cnf(refute_0_73,plain,
    is_a_theorem(implies(implies(necessarily(possibly(X_1357)),possibly(X_1357)),equiv(possibly(X_1357),necessarily(possibly(X_1357))))),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(necessarily(possibly(X_1357)),possibly(X_1357)),and(implies(possibly(X_1357),necessarily(possibly(X_1357))),implies(necessarily(possibly(X_1357)),possibly(X_1357))))) )],[refute_0_67,refute_0_72]) ).

cnf(refute_0_74,plain,
    is_a_theorem(implies(implies(necessarily(possibly(X_1359)),possibly(X_1359)),equiv(possibly(X_1359),necessarily(possibly(X_1359))))),
    inference(subst,[],[refute_0_73:[bind(X_1357,$fot(X_1359))]]) ).

cnf(refute_0_75,plain,
    ( ~ is_a_theorem(implies(necessarily(possibly(X_1359)),possibly(X_1359)))
    | is_a_theorem(equiv(possibly(X_1359),necessarily(possibly(X_1359)))) ),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(necessarily(possibly(X_1359)),possibly(X_1359)),equiv(possibly(X_1359),necessarily(possibly(X_1359))))) )],[refute_0_74,refute_0_61]) ).

cnf(refute_0_76,plain,
    ( ~ axiom_M
    | is_a_theorem(implies(necessarily(X),X)) ),
    inference(canonicalize,[],[normalize_0_33]) ).

cnf(refute_0_77,plain,
    axiom_M,
    inference(canonicalize,[],[normalize_0_34]) ).

cnf(refute_0_78,plain,
    is_a_theorem(implies(necessarily(X),X)),
    inference(resolve,[$cnf( axiom_M )],[refute_0_77,refute_0_76]) ).

cnf(refute_0_79,plain,
    is_a_theorem(implies(necessarily(possibly(X_1359)),possibly(X_1359))),
    inference(subst,[],[refute_0_78:[bind(X,$fot(possibly(X_1359)))]]) ).

cnf(refute_0_80,plain,
    is_a_theorem(equiv(possibly(X_1359),necessarily(possibly(X_1359)))),
    inference(resolve,[$cnf( is_a_theorem(implies(necessarily(possibly(X_1359)),possibly(X_1359))) )],[refute_0_79,refute_0_75]) ).

cnf(refute_0_81,plain,
    is_a_theorem(equiv(possibly(X_1360),necessarily(possibly(X_1360)))),
    inference(subst,[],[refute_0_80:[bind(X_1359,$fot(X_1360))]]) ).

cnf(refute_0_82,plain,
    possibly(X_1360) = necessarily(possibly(X_1360)),
    inference(resolve,[$cnf( is_a_theorem(equiv(possibly(X_1360),necessarily(possibly(X_1360)))) )],[refute_0_81,refute_0_60]) ).

cnf(refute_0_83,plain,
    possibly(necessarily(X_6302)) = necessarily(possibly(necessarily(X_6302))),
    inference(subst,[],[refute_0_82:[bind(X_1360,$fot(necessarily(X_6302)))]]) ).

cnf(refute_0_84,plain,
    ( ~ op_possibly
    | possibly(X) = not(necessarily(not(X))) ),
    inference(canonicalize,[],[normalize_0_36]) ).

cnf(refute_0_85,plain,
    op_possibly,
    inference(canonicalize,[],[normalize_0_37]) ).

cnf(refute_0_86,plain,
    possibly(X) = not(necessarily(not(X))),
    inference(resolve,[$cnf( op_possibly )],[refute_0_85,refute_0_84]) ).

cnf(refute_0_87,plain,
    possibly(necessarily(not(X_0))) = not(necessarily(not(necessarily(not(X_0))))),
    inference(subst,[],[refute_0_86:[bind(X,$fot(necessarily(not(X_0))))]]) ).

cnf(refute_0_88,plain,
    possibly(X_0) = not(necessarily(not(X_0))),
    inference(subst,[],[refute_0_86:[bind(X,$fot(X_0))]]) ).

cnf(refute_0_89,plain,
    ( possibly(X_0) != not(necessarily(not(X_0)))
    | not(necessarily(not(X_0))) = possibly(X_0) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(possibly(X_0))),bind(Y0,$fot(not(necessarily(not(X_0)))))]]) ).

cnf(refute_0_90,plain,
    not(necessarily(not(X_0))) = possibly(X_0),
    inference(resolve,[$cnf( $equal(possibly(X_0),not(necessarily(not(X_0)))) )],[refute_0_88,refute_0_89]) ).

cnf(refute_0_91,plain,
    ( not(necessarily(not(X_0))) != possibly(X_0)
    | possibly(necessarily(not(X_0))) != not(necessarily(not(necessarily(not(X_0)))))
    | possibly(necessarily(not(X_0))) = not(necessarily(possibly(X_0))) ),
    introduced(tautology,[equality,[$cnf( $equal(possibly(necessarily(not(X_0))),not(necessarily(not(necessarily(not(X_0)))))) ),[1,0,0],$fot(possibly(X_0))]]) ).

cnf(refute_0_92,plain,
    ( possibly(necessarily(not(X_0))) != not(necessarily(not(necessarily(not(X_0)))))
    | possibly(necessarily(not(X_0))) = not(necessarily(possibly(X_0))) ),
    inference(resolve,[$cnf( $equal(not(necessarily(not(X_0))),possibly(X_0)) )],[refute_0_90,refute_0_91]) ).

cnf(refute_0_93,plain,
    possibly(necessarily(not(X_0))) = not(necessarily(possibly(X_0))),
    inference(resolve,[$cnf( $equal(possibly(necessarily(not(X_0))),not(necessarily(not(necessarily(not(X_0)))))) )],[refute_0_87,refute_0_92]) ).

cnf(refute_0_94,plain,
    ( possibly(X_1360) != necessarily(possibly(X_1360))
    | necessarily(possibly(X_1360)) = possibly(X_1360) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(possibly(X_1360))),bind(Y0,$fot(necessarily(possibly(X_1360))))]]) ).

cnf(refute_0_95,plain,
    necessarily(possibly(X_1360)) = possibly(X_1360),
    inference(resolve,[$cnf( $equal(possibly(X_1360),necessarily(possibly(X_1360))) )],[refute_0_82,refute_0_94]) ).

cnf(refute_0_96,plain,
    necessarily(possibly(X_0)) = possibly(X_0),
    inference(subst,[],[refute_0_95:[bind(X_1360,$fot(X_0))]]) ).

cnf(refute_0_97,plain,
    not(necessarily(possibly(X_0))) = not(necessarily(possibly(X_0))),
    introduced(tautology,[refl,[$fot(not(necessarily(possibly(X_0))))]]) ).

cnf(refute_0_98,plain,
    ( necessarily(possibly(X_0)) != possibly(X_0)
    | not(necessarily(possibly(X_0))) != not(necessarily(possibly(X_0)))
    | not(necessarily(possibly(X_0))) = not(possibly(X_0)) ),
    introduced(tautology,[equality,[$cnf( $equal(not(necessarily(possibly(X_0))),not(necessarily(possibly(X_0)))) ),[1,0],$fot(possibly(X_0))]]) ).

cnf(refute_0_99,plain,
    ( necessarily(possibly(X_0)) != possibly(X_0)
    | not(necessarily(possibly(X_0))) = not(possibly(X_0)) ),
    inference(resolve,[$cnf( $equal(not(necessarily(possibly(X_0))),not(necessarily(possibly(X_0)))) )],[refute_0_97,refute_0_98]) ).

cnf(refute_0_100,plain,
    not(necessarily(possibly(X_0))) = not(possibly(X_0)),
    inference(resolve,[$cnf( $equal(necessarily(possibly(X_0)),possibly(X_0)) )],[refute_0_96,refute_0_99]) ).

cnf(refute_0_101,plain,
    ( not(necessarily(possibly(X_0))) != not(possibly(X_0))
    | possibly(necessarily(not(X_0))) != not(necessarily(possibly(X_0)))
    | possibly(necessarily(not(X_0))) = not(possibly(X_0)) ),
    introduced(tautology,[equality,[$cnf( $equal(possibly(necessarily(not(X_0))),not(necessarily(possibly(X_0)))) ),[1],$fot(not(possibly(X_0)))]]) ).

cnf(refute_0_102,plain,
    ( possibly(necessarily(not(X_0))) != not(necessarily(possibly(X_0)))
    | possibly(necessarily(not(X_0))) = not(possibly(X_0)) ),
    inference(resolve,[$cnf( $equal(not(necessarily(possibly(X_0))),not(possibly(X_0))) )],[refute_0_100,refute_0_101]) ).

cnf(refute_0_103,plain,
    possibly(necessarily(not(X_0))) = not(possibly(X_0)),
    inference(resolve,[$cnf( $equal(possibly(necessarily(not(X_0))),not(necessarily(possibly(X_0)))) )],[refute_0_93,refute_0_102]) ).

cnf(refute_0_104,plain,
    ( ~ op_or
    | or(X,Y) = not(and(not(X),not(Y))) ),
    inference(canonicalize,[],[normalize_0_39]) ).

cnf(refute_0_105,plain,
    op_or,
    inference(canonicalize,[],[normalize_0_40]) ).

cnf(refute_0_106,plain,
    or(X,Y) = not(and(not(X),not(Y))),
    inference(resolve,[$cnf( op_or )],[refute_0_105,refute_0_104]) ).

cnf(refute_0_107,plain,
    ( ~ op_implies_and
    | implies(X,Y) = not(and(X,not(Y))) ),
    inference(canonicalize,[],[normalize_0_42]) ).

cnf(refute_0_108,plain,
    op_implies_and,
    inference(canonicalize,[],[normalize_0_43]) ).

cnf(refute_0_109,plain,
    implies(X,Y) = not(and(X,not(Y))),
    inference(resolve,[$cnf( op_implies_and )],[refute_0_108,refute_0_107]) ).

cnf(refute_0_110,plain,
    ( implies(X,Y) != not(and(X,not(Y)))
    | not(and(X,not(Y))) = implies(X,Y) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(implies(X,Y))),bind(Y0,$fot(not(and(X,not(Y)))))]]) ).

cnf(refute_0_111,plain,
    not(and(X,not(Y))) = implies(X,Y),
    inference(resolve,[$cnf( $equal(implies(X,Y),not(and(X,not(Y)))) )],[refute_0_109,refute_0_110]) ).

cnf(refute_0_112,plain,
    not(and(not(X),not(Y))) = implies(not(X),Y),
    inference(subst,[],[refute_0_111:[bind(X,$fot(not(X)))]]) ).

cnf(refute_0_113,plain,
    ( not(and(not(X),not(Y))) != implies(not(X),Y)
    | or(X,Y) != not(and(not(X),not(Y)))
    | or(X,Y) = implies(not(X),Y) ),
    introduced(tautology,[equality,[$cnf( $equal(or(X,Y),not(and(not(X),not(Y)))) ),[1],$fot(implies(not(X),Y))]]) ).

cnf(refute_0_114,plain,
    ( or(X,Y) != not(and(not(X),not(Y)))
    | or(X,Y) = implies(not(X),Y) ),
    inference(resolve,[$cnf( $equal(not(and(not(X),not(Y))),implies(not(X),Y)) )],[refute_0_112,refute_0_113]) ).

cnf(refute_0_115,plain,
    or(X,Y) = implies(not(X),Y),
    inference(resolve,[$cnf( $equal(or(X,Y),not(and(not(X),not(Y)))) )],[refute_0_106,refute_0_114]) ).

cnf(refute_0_116,plain,
    or(necessarily(not(X)),X_62) = implies(not(necessarily(not(X))),X_62),
    inference(subst,[],[refute_0_115:[bind(X,$fot(necessarily(not(X)))),bind(Y,$fot(X_62))]]) ).

cnf(refute_0_117,plain,
    ( possibly(X) != not(necessarily(not(X)))
    | not(necessarily(not(X))) = possibly(X) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(possibly(X))),bind(Y0,$fot(not(necessarily(not(X)))))]]) ).

cnf(refute_0_118,plain,
    not(necessarily(not(X))) = possibly(X),
    inference(resolve,[$cnf( $equal(possibly(X),not(necessarily(not(X)))) )],[refute_0_86,refute_0_117]) ).

cnf(refute_0_119,plain,
    ( not(necessarily(not(X))) != possibly(X)
    | or(necessarily(not(X)),X_62) != implies(not(necessarily(not(X))),X_62)
    | or(necessarily(not(X)),X_62) = implies(possibly(X),X_62) ),
    introduced(tautology,[equality,[$cnf( $equal(or(necessarily(not(X)),X_62),implies(not(necessarily(not(X))),X_62)) ),[1,0],$fot(possibly(X))]]) ).

cnf(refute_0_120,plain,
    ( or(necessarily(not(X)),X_62) != implies(not(necessarily(not(X))),X_62)
    | or(necessarily(not(X)),X_62) = implies(possibly(X),X_62) ),
    inference(resolve,[$cnf( $equal(not(necessarily(not(X))),possibly(X)) )],[refute_0_118,refute_0_119]) ).

cnf(refute_0_121,plain,
    or(necessarily(not(X)),X_62) = implies(possibly(X),X_62),
    inference(resolve,[$cnf( $equal(or(necessarily(not(X)),X_62),implies(not(necessarily(not(X))),X_62)) )],[refute_0_116,refute_0_120]) ).

cnf(refute_0_122,plain,
    or(necessarily(not(X)),necessarily(not(X))) = implies(possibly(X),necessarily(not(X))),
    inference(subst,[],[refute_0_121:[bind(X_62,$fot(necessarily(not(X))))]]) ).

cnf(refute_0_123,plain,
    implies(not(Y),Y) = not(and(not(Y),not(Y))),
    inference(subst,[],[refute_0_109:[bind(X,$fot(not(Y)))]]) ).

cnf(refute_0_124,plain,
    not(Y) = and(not(Y),not(Y)),
    inference(subst,[],[refute_0_50:[bind(X_1876,$fot(not(Y)))]]) ).

cnf(refute_0_125,plain,
    ( not(Y) != and(not(Y),not(Y))
    | and(not(Y),not(Y)) = not(Y) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(not(Y))),bind(Y0,$fot(and(not(Y),not(Y))))]]) ).

cnf(refute_0_126,plain,
    and(not(Y),not(Y)) = not(Y),
    inference(resolve,[$cnf( $equal(not(Y),and(not(Y),not(Y))) )],[refute_0_124,refute_0_125]) ).

cnf(refute_0_127,plain,
    ( and(not(Y),not(Y)) != not(Y)
    | implies(not(Y),Y) != not(and(not(Y),not(Y)))
    | implies(not(Y),Y) = not(not(Y)) ),
    introduced(tautology,[equality,[$cnf( $equal(implies(not(Y),Y),not(and(not(Y),not(Y)))) ),[1,0],$fot(not(Y))]]) ).

cnf(refute_0_128,plain,
    ( implies(not(Y),Y) != not(and(not(Y),not(Y)))
    | implies(not(Y),Y) = not(not(Y)) ),
    inference(resolve,[$cnf( $equal(and(not(Y),not(Y)),not(Y)) )],[refute_0_126,refute_0_127]) ).

cnf(refute_0_129,plain,
    implies(not(Y),Y) = not(not(Y)),
    inference(resolve,[$cnf( $equal(implies(not(Y),Y),not(and(not(Y),not(Y)))) )],[refute_0_123,refute_0_128]) ).

cnf(refute_0_130,plain,
    ( or(X,Y) != implies(not(X),Y)
    | implies(not(X),Y) = or(X,Y) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(or(X,Y))),bind(Y0,$fot(implies(not(X),Y)))]]) ).

cnf(refute_0_131,plain,
    implies(not(X),Y) = or(X,Y),
    inference(resolve,[$cnf( $equal(or(X,Y),implies(not(X),Y)) )],[refute_0_115,refute_0_130]) ).

cnf(refute_0_132,plain,
    implies(not(Y),Y) = or(Y,Y),
    inference(subst,[],[refute_0_131:[bind(X,$fot(Y))]]) ).

cnf(refute_0_133,plain,
    ( implies(not(Y),Y) != not(not(Y))
    | implies(not(Y),Y) != or(Y,Y)
    | or(Y,Y) = not(not(Y)) ),
    introduced(tautology,[equality,[$cnf( $equal(implies(not(Y),Y),not(not(Y))) ),[0],$fot(or(Y,Y))]]) ).

cnf(refute_0_134,plain,
    ( implies(not(Y),Y) != not(not(Y))
    | or(Y,Y) = not(not(Y)) ),
    inference(resolve,[$cnf( $equal(implies(not(Y),Y),or(Y,Y)) )],[refute_0_132,refute_0_133]) ).

cnf(refute_0_135,plain,
    or(Y,Y) = not(not(Y)),
    inference(resolve,[$cnf( $equal(implies(not(Y),Y),not(not(Y))) )],[refute_0_129,refute_0_134]) ).

cnf(refute_0_136,plain,
    ( ~ is_a_theorem(equiv(X_6295,not(not(X_6295))))
    | X_6295 = not(not(X_6295)) ),
    inference(subst,[],[refute_0_9:[bind(X,$fot(X_6295)),bind(Y,$fot(not(not(X_6295))))]]) ).

cnf(refute_0_137,plain,
    ( ~ is_a_theorem(implies(or(not(X_6294),X_6294),equiv(X_6294,not(not(X_6294)))))
    | ~ is_a_theorem(or(not(X_6294),X_6294))
    | is_a_theorem(equiv(X_6294,not(not(X_6294)))) ),
    inference(subst,[],[refute_0_13:[bind(X,$fot(or(not(X_6294),X_6294))),bind(Y,$fot(equiv(X_6294,not(not(X_6294)))))]]) ).

cnf(refute_0_138,plain,
    ( ~ or_2
    | is_a_theorem(implies(Y,or(X,Y))) ),
    inference(canonicalize,[],[normalize_0_46]) ).

cnf(refute_0_139,plain,
    or_2,
    inference(canonicalize,[],[normalize_0_47]) ).

cnf(refute_0_140,plain,
    is_a_theorem(implies(Y,or(X,Y))),
    inference(resolve,[$cnf( or_2 )],[refute_0_139,refute_0_138]) ).

cnf(refute_0_141,plain,
    ( ~ is_a_theorem(implies(Y,or(X,Y)))
    | is_a_theorem(implies(X_784,and(implies(Y,or(X,Y)),X_784))) ),
    inference(subst,[],[refute_0_20:[bind(Y,$fot(X_784)),bind(X_435,$fot(implies(Y,or(X,Y))))]]) ).

cnf(refute_0_142,plain,
    is_a_theorem(implies(X_784,and(implies(Y,or(X,Y)),X_784))),
    inference(resolve,[$cnf( is_a_theorem(implies(Y,or(X,Y))) )],[refute_0_140,refute_0_141]) ).

cnf(refute_0_143,plain,
    is_a_theorem(implies(X_6291,and(implies(X_6290,or(X_6290,X_6290)),X_6291))),
    inference(subst,[],[refute_0_142:[bind(X,$fot(X_6290)),bind(Y,$fot(X_6290)),bind(X_784,$fot(X_6291))]]) ).

cnf(refute_0_144,plain,
    or(X_6290,X_6290) = not(not(X_6290)),
    inference(subst,[],[refute_0_135:[bind(Y,$fot(X_6290))]]) ).

cnf(refute_0_145,plain,
    ( or(X_6290,X_6290) != not(not(X_6290))
    | ~ is_a_theorem(implies(X_6291,and(implies(X_6290,or(X_6290,X_6290)),X_6291)))
    | is_a_theorem(implies(X_6291,and(implies(X_6290,not(not(X_6290))),X_6291))) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(implies(X_6291,and(implies(X_6290,or(X_6290,X_6290)),X_6291))) ),[0,1,0,1],$fot(not(not(X_6290)))]]) ).

cnf(refute_0_146,plain,
    ( ~ is_a_theorem(implies(X_6291,and(implies(X_6290,or(X_6290,X_6290)),X_6291)))
    | is_a_theorem(implies(X_6291,and(implies(X_6290,not(not(X_6290))),X_6291))) ),
    inference(resolve,[$cnf( $equal(or(X_6290,X_6290),not(not(X_6290))) )],[refute_0_144,refute_0_145]) ).

cnf(refute_0_147,plain,
    is_a_theorem(implies(X_6291,and(implies(X_6290,not(not(X_6290))),X_6291))),
    inference(resolve,[$cnf( is_a_theorem(implies(X_6291,and(implies(X_6290,or(X_6290,X_6290)),X_6291))) )],[refute_0_143,refute_0_146]) ).

cnf(refute_0_148,plain,
    is_a_theorem(implies(implies(not(not(X_6292)),X_6292),and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292)))),
    inference(subst,[],[refute_0_147:[bind(X_6290,$fot(X_6292)),bind(X_6291,$fot(implies(not(not(X_6292)),X_6292)))]]) ).

cnf(refute_0_149,plain,
    equiv(X_6292,not(not(X_6292))) = and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292)),
    inference(subst,[],[refute_0_5:[bind(X,$fot(X_6292)),bind(Y,$fot(not(not(X_6292))))]]) ).

cnf(refute_0_150,plain,
    ( equiv(X_6292,not(not(X_6292))) != and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292))
    | and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292)) = equiv(X_6292,not(not(X_6292))) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(equiv(X_6292,not(not(X_6292))))),bind(Y0,$fot(and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292))))]]) ).

cnf(refute_0_151,plain,
    and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292)) = equiv(X_6292,not(not(X_6292))),
    inference(resolve,[$cnf( $equal(equiv(X_6292,not(not(X_6292))),and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292))) )],[refute_0_149,refute_0_150]) ).

cnf(refute_0_152,plain,
    ( and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292)) != equiv(X_6292,not(not(X_6292)))
    | ~ is_a_theorem(implies(implies(not(not(X_6292)),X_6292),and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292))))
    | is_a_theorem(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292))))) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(implies(implies(not(not(X_6292)),X_6292),and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292)))) ),[0,1],$fot(equiv(X_6292,not(not(X_6292))))]]) ).

cnf(refute_0_153,plain,
    ( ~ is_a_theorem(implies(implies(not(not(X_6292)),X_6292),and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292))))
    | is_a_theorem(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292))))) ),
    inference(resolve,[$cnf( $equal(and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292)),equiv(X_6292,not(not(X_6292)))) )],[refute_0_151,refute_0_152]) ).

cnf(refute_0_154,plain,
    is_a_theorem(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292))))),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(X_6292)),X_6292),and(implies(X_6292,not(not(X_6292))),implies(not(not(X_6292)),X_6292)))) )],[refute_0_148,refute_0_153]) ).

cnf(refute_0_155,plain,
    implies(not(not(X_6292)),X_6292) = or(not(X_6292),X_6292),
    inference(subst,[],[refute_0_131:[bind(X,$fot(not(X_6292))),bind(Y,$fot(X_6292))]]) ).

cnf(refute_0_156,plain,
    implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))) = implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))),
    introduced(tautology,[refl,[$fot(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))))]]) ).

cnf(refute_0_157,plain,
    ( implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))) != implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292))))
    | implies(not(not(X_6292)),X_6292) != or(not(X_6292),X_6292)
    | implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))) = implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292)))) ),
    introduced(tautology,[equality,[$cnf( $equal(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))),implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292))))) ),[1,0],$fot(or(not(X_6292),X_6292))]]) ).

cnf(refute_0_158,plain,
    ( implies(not(not(X_6292)),X_6292) != or(not(X_6292),X_6292)
    | implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))) = implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292)))) ),
    inference(resolve,[$cnf( $equal(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))),implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292))))) )],[refute_0_156,refute_0_157]) ).

cnf(refute_0_159,plain,
    implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))) = implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292)))),
    inference(resolve,[$cnf( $equal(implies(not(not(X_6292)),X_6292),or(not(X_6292),X_6292)) )],[refute_0_155,refute_0_158]) ).

cnf(refute_0_160,plain,
    ( implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))) != implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292))))
    | ~ is_a_theorem(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))))
    | is_a_theorem(implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292))))) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292))))) ),[0],$fot(implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292)))))]]) ).

cnf(refute_0_161,plain,
    ( ~ is_a_theorem(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))))
    | is_a_theorem(implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292))))) ),
    inference(resolve,[$cnf( $equal(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292)))),implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292))))) )],[refute_0_159,refute_0_160]) ).

cnf(refute_0_162,plain,
    is_a_theorem(implies(or(not(X_6292),X_6292),equiv(X_6292,not(not(X_6292))))),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(X_6292)),X_6292),equiv(X_6292,not(not(X_6292))))) )],[refute_0_154,refute_0_161]) ).

cnf(refute_0_163,plain,
    is_a_theorem(implies(or(not(X_6294),X_6294),equiv(X_6294,not(not(X_6294))))),
    inference(subst,[],[refute_0_162:[bind(X_6292,$fot(X_6294))]]) ).

cnf(refute_0_164,plain,
    ( ~ is_a_theorem(or(not(X_6294),X_6294))
    | is_a_theorem(equiv(X_6294,not(not(X_6294)))) ),
    inference(resolve,[$cnf( is_a_theorem(implies(or(not(X_6294),X_6294),equiv(X_6294,not(not(X_6294))))) )],[refute_0_163,refute_0_137]) ).

cnf(refute_0_165,plain,
    ( ~ modus_tollens
    | is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ),
    inference(canonicalize,[],[normalize_0_50]) ).

cnf(refute_0_166,plain,
    modus_tollens,
    inference(canonicalize,[],[normalize_0_51]) ).

cnf(refute_0_167,plain,
    is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))),
    inference(resolve,[$cnf( modus_tollens )],[refute_0_166,refute_0_165]) ).

cnf(refute_0_168,plain,
    implies(not(Y),not(X)) = or(Y,not(X)),
    inference(subst,[],[refute_0_131:[bind(X,$fot(Y)),bind(Y,$fot(not(X)))]]) ).

cnf(refute_0_169,plain,
    implies(implies(not(Y),not(X)),implies(X,Y)) = implies(implies(not(Y),not(X)),implies(X,Y)),
    introduced(tautology,[refl,[$fot(implies(implies(not(Y),not(X)),implies(X,Y)))]]) ).

cnf(refute_0_170,plain,
    ( implies(implies(not(Y),not(X)),implies(X,Y)) != implies(implies(not(Y),not(X)),implies(X,Y))
    | implies(not(Y),not(X)) != or(Y,not(X))
    | implies(implies(not(Y),not(X)),implies(X,Y)) = implies(or(Y,not(X)),implies(X,Y)) ),
    introduced(tautology,[equality,[$cnf( $equal(implies(implies(not(Y),not(X)),implies(X,Y)),implies(implies(not(Y),not(X)),implies(X,Y))) ),[1,0],$fot(or(Y,not(X)))]]) ).

cnf(refute_0_171,plain,
    ( implies(not(Y),not(X)) != or(Y,not(X))
    | implies(implies(not(Y),not(X)),implies(X,Y)) = implies(or(Y,not(X)),implies(X,Y)) ),
    inference(resolve,[$cnf( $equal(implies(implies(not(Y),not(X)),implies(X,Y)),implies(implies(not(Y),not(X)),implies(X,Y))) )],[refute_0_169,refute_0_170]) ).

cnf(refute_0_172,plain,
    implies(implies(not(Y),not(X)),implies(X,Y)) = implies(or(Y,not(X)),implies(X,Y)),
    inference(resolve,[$cnf( $equal(implies(not(Y),not(X)),or(Y,not(X))) )],[refute_0_168,refute_0_171]) ).

cnf(refute_0_173,plain,
    ( implies(implies(not(Y),not(X)),implies(X,Y)) != implies(or(Y,not(X)),implies(X,Y))
    | ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y)))
    | is_a_theorem(implies(or(Y,not(X)),implies(X,Y))) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ),[0],$fot(implies(or(Y,not(X)),implies(X,Y)))]]) ).

cnf(refute_0_174,plain,
    ( ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y)))
    | is_a_theorem(implies(or(Y,not(X)),implies(X,Y))) ),
    inference(resolve,[$cnf( $equal(implies(implies(not(Y),not(X)),implies(X,Y)),implies(or(Y,not(X)),implies(X,Y))) )],[refute_0_172,refute_0_173]) ).

cnf(refute_0_175,plain,
    is_a_theorem(implies(or(Y,not(X)),implies(X,Y))),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) )],[refute_0_167,refute_0_174]) ).

cnf(refute_0_176,plain,
    ( ~ is_a_theorem(implies(or(Y,not(X)),implies(X,Y)))
    | ~ is_a_theorem(or(Y,not(X)))
    | is_a_theorem(implies(X,Y)) ),
    inference(subst,[],[refute_0_13:[bind(X,$fot(or(Y,not(X)))),bind(Y,$fot(implies(X,Y)))]]) ).

cnf(refute_0_177,plain,
    ( ~ is_a_theorem(or(Y,not(X)))
    | is_a_theorem(implies(X,Y)) ),
    inference(resolve,[$cnf( is_a_theorem(implies(or(Y,not(X)),implies(X,Y))) )],[refute_0_175,refute_0_176]) ).

cnf(refute_0_178,plain,
    ( ~ is_a_theorem(or(X_1917,not(not(not(X_1917)))))
    | is_a_theorem(implies(not(not(X_1917)),X_1917)) ),
    inference(subst,[],[refute_0_177:[bind(X,$fot(not(not(X_1917)))),bind(Y,$fot(X_1917))]]) ).

cnf(refute_0_179,plain,
    ( ~ or_1
    | is_a_theorem(implies(X,or(X,Y))) ),
    inference(canonicalize,[],[normalize_0_54]) ).

cnf(refute_0_180,plain,
    or_1,
    inference(canonicalize,[],[normalize_0_55]) ).

cnf(refute_0_181,plain,
    is_a_theorem(implies(X,or(X,Y))),
    inference(resolve,[$cnf( or_1 )],[refute_0_180,refute_0_179]) ).

cnf(refute_0_182,plain,
    is_a_theorem(implies(not(X_61),or(not(X_61),Y))),
    inference(subst,[],[refute_0_181:[bind(X,$fot(not(X_61)))]]) ).

cnf(refute_0_183,plain,
    or(X_61,or(not(X_61),Y)) = implies(not(X_61),or(not(X_61),Y)),
    inference(subst,[],[refute_0_115:[bind(X,$fot(X_61)),bind(Y,$fot(or(not(X_61),Y)))]]) ).

cnf(refute_0_184,plain,
    ( or(X_61,or(not(X_61),Y)) != implies(not(X_61),or(not(X_61),Y))
    | implies(not(X_61),or(not(X_61),Y)) = or(X_61,or(not(X_61),Y)) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(or(X_61,or(not(X_61),Y)))),bind(Y0,$fot(implies(not(X_61),or(not(X_61),Y))))]]) ).

cnf(refute_0_185,plain,
    implies(not(X_61),or(not(X_61),Y)) = or(X_61,or(not(X_61),Y)),
    inference(resolve,[$cnf( $equal(or(X_61,or(not(X_61),Y)),implies(not(X_61),or(not(X_61),Y))) )],[refute_0_183,refute_0_184]) ).

cnf(refute_0_186,plain,
    ( implies(not(X_61),or(not(X_61),Y)) != or(X_61,or(not(X_61),Y))
    | ~ is_a_theorem(implies(not(X_61),or(not(X_61),Y)))
    | is_a_theorem(or(X_61,or(not(X_61),Y))) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(implies(not(X_61),or(not(X_61),Y))) ),[0],$fot(or(X_61,or(not(X_61),Y)))]]) ).

cnf(refute_0_187,plain,
    ( ~ is_a_theorem(implies(not(X_61),or(not(X_61),Y)))
    | is_a_theorem(or(X_61,or(not(X_61),Y))) ),
    inference(resolve,[$cnf( $equal(implies(not(X_61),or(not(X_61),Y)),or(X_61,or(not(X_61),Y))) )],[refute_0_185,refute_0_186]) ).

cnf(refute_0_188,plain,
    is_a_theorem(or(X_61,or(not(X_61),Y))),
    inference(resolve,[$cnf( is_a_theorem(implies(not(X_61),or(not(X_61),Y))) )],[refute_0_182,refute_0_187]) ).

cnf(refute_0_189,plain,
    is_a_theorem(or(X_61,or(not(X_61),not(X_61)))),
    inference(subst,[],[refute_0_188:[bind(Y,$fot(not(X_61)))]]) ).

cnf(refute_0_190,plain,
    or(not(X_61),not(X_61)) = not(not(not(X_61))),
    inference(subst,[],[refute_0_135:[bind(Y,$fot(not(X_61)))]]) ).

cnf(refute_0_191,plain,
    ( or(not(X_61),not(X_61)) != not(not(not(X_61)))
    | ~ is_a_theorem(or(X_61,or(not(X_61),not(X_61))))
    | is_a_theorem(or(X_61,not(not(not(X_61))))) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(or(X_61,or(not(X_61),not(X_61)))) ),[0,1],$fot(not(not(not(X_61))))]]) ).

cnf(refute_0_192,plain,
    ( ~ is_a_theorem(or(X_61,or(not(X_61),not(X_61))))
    | is_a_theorem(or(X_61,not(not(not(X_61))))) ),
    inference(resolve,[$cnf( $equal(or(not(X_61),not(X_61)),not(not(not(X_61)))) )],[refute_0_190,refute_0_191]) ).

cnf(refute_0_193,plain,
    is_a_theorem(or(X_61,not(not(not(X_61))))),
    inference(resolve,[$cnf( is_a_theorem(or(X_61,or(not(X_61),not(X_61)))) )],[refute_0_189,refute_0_192]) ).

cnf(refute_0_194,plain,
    is_a_theorem(or(X_1917,not(not(not(X_1917))))),
    inference(subst,[],[refute_0_193:[bind(X_61,$fot(X_1917))]]) ).

cnf(refute_0_195,plain,
    is_a_theorem(implies(not(not(X_1917)),X_1917)),
    inference(resolve,[$cnf( is_a_theorem(or(X_1917,not(not(not(X_1917))))) )],[refute_0_194,refute_0_178]) ).

cnf(refute_0_196,plain,
    implies(not(not(X_1917)),X_1917) = or(not(X_1917),X_1917),
    inference(subst,[],[refute_0_131:[bind(X,$fot(not(X_1917))),bind(Y,$fot(X_1917))]]) ).

cnf(refute_0_197,plain,
    ( implies(not(not(X_1917)),X_1917) != or(not(X_1917),X_1917)
    | ~ is_a_theorem(implies(not(not(X_1917)),X_1917))
    | is_a_theorem(or(not(X_1917),X_1917)) ),
    introduced(tautology,[equality,[$cnf( is_a_theorem(implies(not(not(X_1917)),X_1917)) ),[0],$fot(or(not(X_1917),X_1917))]]) ).

cnf(refute_0_198,plain,
    ( ~ is_a_theorem(implies(not(not(X_1917)),X_1917))
    | is_a_theorem(or(not(X_1917),X_1917)) ),
    inference(resolve,[$cnf( $equal(implies(not(not(X_1917)),X_1917),or(not(X_1917),X_1917)) )],[refute_0_196,refute_0_197]) ).

cnf(refute_0_199,plain,
    is_a_theorem(or(not(X_1917),X_1917)),
    inference(resolve,[$cnf( is_a_theorem(implies(not(not(X_1917)),X_1917)) )],[refute_0_195,refute_0_198]) ).

cnf(refute_0_200,plain,
    is_a_theorem(or(not(X_6294),X_6294)),
    inference(subst,[],[refute_0_199:[bind(X_1917,$fot(X_6294))]]) ).

cnf(refute_0_201,plain,
    is_a_theorem(equiv(X_6294,not(not(X_6294)))),
    inference(resolve,[$cnf( is_a_theorem(or(not(X_6294),X_6294)) )],[refute_0_200,refute_0_164]) ).

cnf(refute_0_202,plain,
    is_a_theorem(equiv(X_6295,not(not(X_6295)))),
    inference(subst,[],[refute_0_201:[bind(X_6294,$fot(X_6295))]]) ).

cnf(refute_0_203,plain,
    X_6295 = not(not(X_6295)),
    inference(resolve,[$cnf( is_a_theorem(equiv(X_6295,not(not(X_6295)))) )],[refute_0_202,refute_0_136]) ).

cnf(refute_0_204,plain,
    ( X_6295 != not(not(X_6295))
    | not(not(X_6295)) = X_6295 ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(X_6295)),bind(Y0,$fot(not(not(X_6295))))]]) ).

cnf(refute_0_205,plain,
    not(not(X_6295)) = X_6295,
    inference(resolve,[$cnf( $equal(X_6295,not(not(X_6295))) )],[refute_0_203,refute_0_204]) ).

cnf(refute_0_206,plain,
    not(not(Y)) = Y,
    inference(subst,[],[refute_0_205:[bind(X_6295,$fot(Y))]]) ).

cnf(refute_0_207,plain,
    ( not(not(Y)) != Y
    | or(Y,Y) != not(not(Y))
    | or(Y,Y) = Y ),
    introduced(tautology,[equality,[$cnf( $equal(or(Y,Y),not(not(Y))) ),[1],$fot(Y)]]) ).

cnf(refute_0_208,plain,
    ( or(Y,Y) != not(not(Y))
    | or(Y,Y) = Y ),
    inference(resolve,[$cnf( $equal(not(not(Y)),Y) )],[refute_0_206,refute_0_207]) ).

cnf(refute_0_209,plain,
    or(Y,Y) = Y,
    inference(resolve,[$cnf( $equal(or(Y,Y),not(not(Y))) )],[refute_0_135,refute_0_208]) ).

cnf(refute_0_210,plain,
    or(necessarily(not(X)),necessarily(not(X))) = necessarily(not(X)),
    inference(subst,[],[refute_0_209:[bind(Y,$fot(necessarily(not(X))))]]) ).

cnf(refute_0_211,plain,
    ( or(necessarily(not(X)),necessarily(not(X))) != implies(possibly(X),necessarily(not(X)))
    | or(necessarily(not(X)),necessarily(not(X))) != necessarily(not(X))
    | necessarily(not(X)) = implies(possibly(X),necessarily(not(X))) ),
    introduced(tautology,[equality,[$cnf( $equal(or(necessarily(not(X)),necessarily(not(X))),implies(possibly(X),necessarily(not(X)))) ),[0],$fot(necessarily(not(X)))]]) ).

cnf(refute_0_212,plain,
    ( or(necessarily(not(X)),necessarily(not(X))) != implies(possibly(X),necessarily(not(X)))
    | necessarily(not(X)) = implies(possibly(X),necessarily(not(X))) ),
    inference(resolve,[$cnf( $equal(or(necessarily(not(X)),necessarily(not(X))),necessarily(not(X))) )],[refute_0_210,refute_0_211]) ).

cnf(refute_0_213,plain,
    necessarily(not(X)) = implies(possibly(X),necessarily(not(X))),
    inference(resolve,[$cnf( $equal(or(necessarily(not(X)),necessarily(not(X))),implies(possibly(X),necessarily(not(X)))) )],[refute_0_122,refute_0_212]) ).

cnf(refute_0_214,plain,
    ( X_1876 != and(X_1876,X_1876)
    | and(X_1876,X_1876) = X_1876 ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(X_1876)),bind(Y0,$fot(and(X_1876,X_1876)))]]) ).

cnf(refute_0_215,plain,
    and(X_1876,X_1876) = X_1876,
    inference(resolve,[$cnf( $equal(X_1876,and(X_1876,X_1876)) )],[refute_0_50,refute_0_214]) ).

cnf(refute_0_216,plain,
    and(possibly(X),possibly(X)) = possibly(X),
    inference(subst,[],[refute_0_215:[bind(X_1876,$fot(possibly(X)))]]) ).

cnf(refute_0_217,plain,
    not(and(possibly(X),possibly(X))) = not(and(possibly(X),possibly(X))),
    introduced(tautology,[refl,[$fot(not(and(possibly(X),possibly(X))))]]) ).

cnf(refute_0_218,plain,
    ( and(possibly(X),possibly(X)) != possibly(X)
    | not(and(possibly(X),possibly(X))) != not(and(possibly(X),possibly(X)))
    | not(and(possibly(X),possibly(X))) = not(possibly(X)) ),
    introduced(tautology,[equality,[$cnf( $equal(not(and(possibly(X),possibly(X))),not(and(possibly(X),possibly(X)))) ),[1,0],$fot(possibly(X))]]) ).

cnf(refute_0_219,plain,
    ( and(possibly(X),possibly(X)) != possibly(X)
    | not(and(possibly(X),possibly(X))) = not(possibly(X)) ),
    inference(resolve,[$cnf( $equal(not(and(possibly(X),possibly(X))),not(and(possibly(X),possibly(X)))) )],[refute_0_217,refute_0_218]) ).

cnf(refute_0_220,plain,
    not(and(possibly(X),possibly(X))) = not(possibly(X)),
    inference(resolve,[$cnf( $equal(and(possibly(X),possibly(X)),possibly(X)) )],[refute_0_216,refute_0_219]) ).

cnf(refute_0_221,plain,
    implies(X_18,necessarily(not(X))) = not(and(X_18,not(necessarily(not(X))))),
    inference(subst,[],[refute_0_109:[bind(X,$fot(X_18)),bind(Y,$fot(necessarily(not(X))))]]) ).

cnf(refute_0_222,plain,
    ( implies(X_18,necessarily(not(X))) != not(and(X_18,not(necessarily(not(X)))))
    | not(necessarily(not(X))) != possibly(X)
    | implies(X_18,necessarily(not(X))) = not(and(X_18,possibly(X))) ),
    introduced(tautology,[equality,[$cnf( $equal(implies(X_18,necessarily(not(X))),not(and(X_18,not(necessarily(not(X)))))) ),[1,0,1],$fot(possibly(X))]]) ).

cnf(refute_0_223,plain,
    ( implies(X_18,necessarily(not(X))) != not(and(X_18,not(necessarily(not(X)))))
    | implies(X_18,necessarily(not(X))) = not(and(X_18,possibly(X))) ),
    inference(resolve,[$cnf( $equal(not(necessarily(not(X))),possibly(X)) )],[refute_0_118,refute_0_222]) ).

cnf(refute_0_224,plain,
    implies(X_18,necessarily(not(X))) = not(and(X_18,possibly(X))),
    inference(resolve,[$cnf( $equal(implies(X_18,necessarily(not(X))),not(and(X_18,not(necessarily(not(X)))))) )],[refute_0_221,refute_0_223]) ).

cnf(refute_0_225,plain,
    implies(possibly(X),necessarily(not(X))) = not(and(possibly(X),possibly(X))),
    inference(subst,[],[refute_0_224:[bind(X_18,$fot(possibly(X)))]]) ).

cnf(refute_0_226,plain,
    ( Y0 != X0
    | Y0 != Z
    | X0 = Z ),
    introduced(tautology,[equality,[$cnf( $equal(Y0,Z) ),[0],$fot(X0)]]) ).

cnf(refute_0_227,plain,
    ( X0 != Y0
    | Y0 != Z
    | X0 = Z ),
    inference(resolve,[$cnf( $equal(Y0,X0) )],[refute_0_36,refute_0_226]) ).

cnf(refute_0_228,plain,
    ( implies(possibly(X),necessarily(not(X))) != not(and(possibly(X),possibly(X)))
    | not(and(possibly(X),possibly(X))) != not(possibly(X))
    | implies(possibly(X),necessarily(not(X))) = not(possibly(X)) ),
    inference(subst,[],[refute_0_227:[bind(X0,$fot(implies(possibly(X),necessarily(not(X))))),bind(Y0,$fot(not(and(possibly(X),possibly(X))))),bind(Z,$fot(not(possibly(X))))]]) ).

cnf(refute_0_229,plain,
    ( not(and(possibly(X),possibly(X))) != not(possibly(X))
    | implies(possibly(X),necessarily(not(X))) = not(possibly(X)) ),
    inference(resolve,[$cnf( $equal(implies(possibly(X),necessarily(not(X))),not(and(possibly(X),possibly(X)))) )],[refute_0_225,refute_0_228]) ).

cnf(refute_0_230,plain,
    implies(possibly(X),necessarily(not(X))) = not(possibly(X)),
    inference(resolve,[$cnf( $equal(not(and(possibly(X),possibly(X))),not(possibly(X))) )],[refute_0_220,refute_0_229]) ).

cnf(refute_0_231,plain,
    ( implies(possibly(X),necessarily(not(X))) != not(possibly(X))
    | necessarily(not(X)) != implies(possibly(X),necessarily(not(X)))
    | necessarily(not(X)) = not(possibly(X)) ),
    introduced(tautology,[equality,[$cnf( $equal(necessarily(not(X)),implies(possibly(X),necessarily(not(X)))) ),[1],$fot(not(possibly(X)))]]) ).

cnf(refute_0_232,plain,
    ( necessarily(not(X)) != implies(possibly(X),necessarily(not(X)))
    | necessarily(not(X)) = not(possibly(X)) ),
    inference(resolve,[$cnf( $equal(implies(possibly(X),necessarily(not(X))),not(possibly(X))) )],[refute_0_230,refute_0_231]) ).

cnf(refute_0_233,plain,
    necessarily(not(X)) = not(possibly(X)),
    inference(resolve,[$cnf( $equal(necessarily(not(X)),implies(possibly(X),necessarily(not(X)))) )],[refute_0_213,refute_0_232]) ).

cnf(refute_0_234,plain,
    ( necessarily(not(X)) != not(possibly(X))
    | not(possibly(X)) = necessarily(not(X)) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(necessarily(not(X)))),bind(Y0,$fot(not(possibly(X))))]]) ).

cnf(refute_0_235,plain,
    not(possibly(X)) = necessarily(not(X)),
    inference(resolve,[$cnf( $equal(necessarily(not(X)),not(possibly(X))) )],[refute_0_233,refute_0_234]) ).

cnf(refute_0_236,plain,
    not(possibly(X_0)) = necessarily(not(X_0)),
    inference(subst,[],[refute_0_235:[bind(X,$fot(X_0))]]) ).

cnf(refute_0_237,plain,
    ( not(possibly(X_0)) != necessarily(not(X_0))
    | possibly(necessarily(not(X_0))) != not(possibly(X_0))
    | possibly(necessarily(not(X_0))) = necessarily(not(X_0)) ),
    introduced(tautology,[equality,[$cnf( $equal(possibly(necessarily(not(X_0))),not(possibly(X_0))) ),[1],$fot(necessarily(not(X_0)))]]) ).

cnf(refute_0_238,plain,
    ( possibly(necessarily(not(X_0))) != not(possibly(X_0))
    | possibly(necessarily(not(X_0))) = necessarily(not(X_0)) ),
    inference(resolve,[$cnf( $equal(not(possibly(X_0)),necessarily(not(X_0))) )],[refute_0_236,refute_0_237]) ).

cnf(refute_0_239,plain,
    possibly(necessarily(not(X_0))) = necessarily(not(X_0)),
    inference(resolve,[$cnf( $equal(possibly(necessarily(not(X_0))),not(possibly(X_0))) )],[refute_0_103,refute_0_238]) ).

cnf(refute_0_240,plain,
    possibly(necessarily(not(not(X_6295)))) = necessarily(not(not(X_6295))),
    inference(subst,[],[refute_0_239:[bind(X_0,$fot(not(X_6295)))]]) ).

cnf(refute_0_241,plain,
    ( not(not(X_6295)) != X_6295
    | possibly(necessarily(not(not(X_6295)))) != necessarily(not(not(X_6295)))
    | possibly(necessarily(X_6295)) = necessarily(not(not(X_6295))) ),
    introduced(tautology,[equality,[$cnf( $equal(possibly(necessarily(not(not(X_6295)))),necessarily(not(not(X_6295)))) ),[0,0,0],$fot(X_6295)]]) ).

cnf(refute_0_242,plain,
    ( possibly(necessarily(not(not(X_6295)))) != necessarily(not(not(X_6295)))
    | possibly(necessarily(X_6295)) = necessarily(not(not(X_6295))) ),
    inference(resolve,[$cnf( $equal(not(not(X_6295)),X_6295) )],[refute_0_205,refute_0_241]) ).

cnf(refute_0_243,plain,
    possibly(necessarily(X_6295)) = necessarily(not(not(X_6295))),
    inference(resolve,[$cnf( $equal(possibly(necessarily(not(not(X_6295)))),necessarily(not(not(X_6295)))) )],[refute_0_240,refute_0_242]) ).

cnf(refute_0_244,plain,
    necessarily(not(not(X_6295))) = necessarily(not(not(X_6295))),
    introduced(tautology,[refl,[$fot(necessarily(not(not(X_6295))))]]) ).

cnf(refute_0_245,plain,
    ( necessarily(not(not(X_6295))) != necessarily(not(not(X_6295)))
    | not(not(X_6295)) != X_6295
    | necessarily(not(not(X_6295))) = necessarily(X_6295) ),
    introduced(tautology,[equality,[$cnf( $equal(necessarily(not(not(X_6295))),necessarily(not(not(X_6295)))) ),[1,0],$fot(X_6295)]]) ).

cnf(refute_0_246,plain,
    ( not(not(X_6295)) != X_6295
    | necessarily(not(not(X_6295))) = necessarily(X_6295) ),
    inference(resolve,[$cnf( $equal(necessarily(not(not(X_6295))),necessarily(not(not(X_6295)))) )],[refute_0_244,refute_0_245]) ).

cnf(refute_0_247,plain,
    necessarily(not(not(X_6295))) = necessarily(X_6295),
    inference(resolve,[$cnf( $equal(not(not(X_6295)),X_6295) )],[refute_0_205,refute_0_246]) ).

cnf(refute_0_248,plain,
    ( necessarily(not(not(X_6295))) != necessarily(X_6295)
    | possibly(necessarily(X_6295)) != necessarily(not(not(X_6295)))
    | possibly(necessarily(X_6295)) = necessarily(X_6295) ),
    introduced(tautology,[equality,[$cnf( $equal(possibly(necessarily(X_6295)),necessarily(not(not(X_6295)))) ),[1],$fot(necessarily(X_6295))]]) ).

cnf(refute_0_249,plain,
    ( possibly(necessarily(X_6295)) != necessarily(not(not(X_6295)))
    | possibly(necessarily(X_6295)) = necessarily(X_6295) ),
    inference(resolve,[$cnf( $equal(necessarily(not(not(X_6295))),necessarily(X_6295)) )],[refute_0_247,refute_0_248]) ).

cnf(refute_0_250,plain,
    possibly(necessarily(X_6295)) = necessarily(X_6295),
    inference(resolve,[$cnf( $equal(possibly(necessarily(X_6295)),necessarily(not(not(X_6295)))) )],[refute_0_243,refute_0_249]) ).

cnf(refute_0_251,plain,
    possibly(necessarily(X_6302)) = necessarily(X_6302),
    inference(subst,[],[refute_0_250:[bind(X_6295,$fot(X_6302))]]) ).

cnf(refute_0_252,plain,
    ( possibly(necessarily(X_6302)) != necessarily(X_6302)
    | possibly(necessarily(X_6302)) != necessarily(possibly(necessarily(X_6302)))
    | possibly(necessarily(X_6302)) = necessarily(necessarily(X_6302)) ),
    introduced(tautology,[equality,[$cnf( $equal(possibly(necessarily(X_6302)),necessarily(possibly(necessarily(X_6302)))) ),[1,0],$fot(necessarily(X_6302))]]) ).

cnf(refute_0_253,plain,
    ( possibly(necessarily(X_6302)) != necessarily(possibly(necessarily(X_6302)))
    | possibly(necessarily(X_6302)) = necessarily(necessarily(X_6302)) ),
    inference(resolve,[$cnf( $equal(possibly(necessarily(X_6302)),necessarily(X_6302)) )],[refute_0_251,refute_0_252]) ).

cnf(refute_0_254,plain,
    possibly(necessarily(X_6302)) = necessarily(necessarily(X_6302)),
    inference(resolve,[$cnf( $equal(possibly(necessarily(X_6302)),necessarily(possibly(necessarily(X_6302)))) )],[refute_0_83,refute_0_253]) ).

cnf(refute_0_255,plain,
    ( possibly(necessarily(X_6302)) != necessarily(X_6302)
    | possibly(necessarily(X_6302)) != necessarily(necessarily(X_6302))
    | necessarily(X_6302) = necessarily(necessarily(X_6302)) ),
    introduced(tautology,[equality,[$cnf( $equal(possibly(necessarily(X_6302)),necessarily(necessarily(X_6302))) ),[0],$fot(necessarily(X_6302))]]) ).

cnf(refute_0_256,plain,
    ( possibly(necessarily(X_6302)) != necessarily(necessarily(X_6302))
    | necessarily(X_6302) = necessarily(necessarily(X_6302)) ),
    inference(resolve,[$cnf( $equal(possibly(necessarily(X_6302)),necessarily(X_6302)) )],[refute_0_251,refute_0_255]) ).

cnf(refute_0_257,plain,
    necessarily(X_6302) = necessarily(necessarily(X_6302)),
    inference(resolve,[$cnf( $equal(possibly(necessarily(X_6302)),necessarily(necessarily(X_6302))) )],[refute_0_254,refute_0_256]) ).

cnf(refute_0_258,plain,
    ( necessarily(X_6302) != necessarily(necessarily(X_6302))
    | necessarily(necessarily(X_6302)) = necessarily(X_6302) ),
    inference(subst,[],[refute_0_36:[bind(X0,$fot(necessarily(X_6302))),bind(Y0,$fot(necessarily(necessarily(X_6302))))]]) ).

cnf(refute_0_259,plain,
    necessarily(necessarily(X_6302)) = necessarily(X_6302),
    inference(resolve,[$cnf( $equal(necessarily(X_6302),necessarily(necessarily(X_6302))) )],[refute_0_257,refute_0_258]) ).

cnf(refute_0_260,plain,
    necessarily(necessarily(skolemFOFtoCNF_X_21)) = necessarily(skolemFOFtoCNF_X_21),
    inference(subst,[],[refute_0_259:[bind(X_6302,$fot(skolemFOFtoCNF_X_21))]]) ).

cnf(refute_0_261,plain,
    implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) = implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))),
    introduced(tautology,[refl,[$fot(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))))]]) ).

cnf(refute_0_262,plain,
    ( implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) != implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21)))
    | necessarily(necessarily(skolemFOFtoCNF_X_21)) != necessarily(skolemFOFtoCNF_X_21)
    | implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) = implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)) ),
    introduced(tautology,[equality,[$cnf( $equal(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))),implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21)))) ),[1,1],$fot(necessarily(skolemFOFtoCNF_X_21))]]) ).

cnf(refute_0_263,plain,
    ( necessarily(necessarily(skolemFOFtoCNF_X_21)) != necessarily(skolemFOFtoCNF_X_21)
    | implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) = implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)) ),
    inference(resolve,[$cnf( $equal(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))),implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21)))) )],[refute_0_261,refute_0_262]) ).

cnf(refute_0_264,plain,
    implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) = implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)),
    inference(resolve,[$cnf( $equal(necessarily(necessarily(skolemFOFtoCNF_X_21)),necessarily(skolemFOFtoCNF_X_21)) )],[refute_0_260,refute_0_263]) ).

cnf(refute_0_265,plain,
    ( implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) != implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))
    | implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)) != equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))
    | implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) = equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)) ),
    inference(subst,[],[refute_0_227:[bind(X0,$fot(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))))),bind(Y0,$fot(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)))),bind(Z,$fot(equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))))]]) ).

cnf(refute_0_266,plain,
    ( implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)) != equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))
    | implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) = equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)) ),
    inference(resolve,[$cnf( $equal(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))),implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))) )],[refute_0_264,refute_0_265]) ).

cnf(refute_0_267,plain,
    implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) = equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)),
    inference(resolve,[$cnf( $equal(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)),equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))) )],[refute_0_59,refute_0_266]) ).

cnf(refute_0_268,plain,
    ( implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))) != equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))
    | ~ is_a_theorem(equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)))
    | is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21)))) ),
    introduced(tautology,[equality,[$cnf( ~ is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21)))) ),[0],$fot(equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)))]]) ).

cnf(refute_0_269,plain,
    ( ~ is_a_theorem(equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21)))
    | is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21)))) ),
    inference(resolve,[$cnf( $equal(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21))),equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))) )],[refute_0_267,refute_0_268]) ).

cnf(refute_0_270,plain,
    ~ is_a_theorem(equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))),
    inference(resolve,[$cnf( is_a_theorem(implies(necessarily(skolemFOFtoCNF_X_21),necessarily(necessarily(skolemFOFtoCNF_X_21)))) )],[refute_0_269,refute_0_2]) ).

cnf(refute_0_271,plain,
    ( ~ is_a_theorem(implies(X_1739,X_1739))
    | ~ is_a_theorem(implies(implies(X_1739,X_1739),equiv(X_1739,X_1739)))
    | is_a_theorem(equiv(X_1739,X_1739)) ),
    inference(subst,[],[refute_0_13:[bind(X,$fot(implies(X_1739,X_1739))),bind(Y,$fot(equiv(X_1739,X_1739)))]]) ).

cnf(refute_0_272,plain,
    ( ~ equivalence_3
    | is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))) ),
    inference(canonicalize,[],[normalize_0_58]) ).

cnf(refute_0_273,plain,
    equivalence_3,
    inference(canonicalize,[],[normalize_0_59]) ).

cnf(refute_0_274,plain,
    is_a_theorem(implies(implies(X,Y),implies(implies(Y,X),equiv(X,Y)))),
    inference(resolve,[$cnf( equivalence_3 )],[refute_0_273,refute_0_272]) ).

cnf(refute_0_275,plain,
    is_a_theorem(implies(implies(X,X),implies(implies(X,X),equiv(X,X)))),
    inference(subst,[],[refute_0_274:[bind(Y,$fot(X))]]) ).

cnf(refute_0_276,plain,
    ( ~ is_a_theorem(implies(implies(X,X),implies(implies(X,X),equiv(X,X))))
    | is_a_theorem(implies(implies(X,X),equiv(X,X))) ),
    inference(subst,[],[refute_0_27:[bind(X,$fot(implies(X,X))),bind(Y,$fot(equiv(X,X)))]]) ).

cnf(refute_0_277,plain,
    is_a_theorem(implies(implies(X,X),equiv(X,X))),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(X,X),implies(implies(X,X),equiv(X,X)))) )],[refute_0_275,refute_0_276]) ).

cnf(refute_0_278,plain,
    is_a_theorem(implies(implies(X_1739,X_1739),equiv(X_1739,X_1739))),
    inference(subst,[],[refute_0_277:[bind(X,$fot(X_1739))]]) ).

cnf(refute_0_279,plain,
    ( ~ is_a_theorem(implies(X_1739,X_1739))
    | is_a_theorem(equiv(X_1739,X_1739)) ),
    inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1739,X_1739),equiv(X_1739,X_1739))) )],[refute_0_278,refute_0_271]) ).

cnf(refute_0_280,plain,
    ( ~ implies_1
    | is_a_theorem(implies(X,implies(Y,X))) ),
    inference(canonicalize,[],[normalize_0_62]) ).

cnf(refute_0_281,plain,
    implies_1,
    inference(canonicalize,[],[normalize_0_63]) ).

cnf(refute_0_282,plain,
    is_a_theorem(implies(X,implies(Y,X))),
    inference(resolve,[$cnf( implies_1 )],[refute_0_281,refute_0_280]) ).

cnf(refute_0_283,plain,
    is_a_theorem(implies(X_1731,implies(X_1731,X_1731))),
    inference(subst,[],[refute_0_282:[bind(X,$fot(X_1731)),bind(Y,$fot(X_1731))]]) ).

cnf(refute_0_284,plain,
    ( ~ is_a_theorem(implies(X_1731,implies(X_1731,X_1731)))
    | is_a_theorem(implies(X_1731,X_1731)) ),
    inference(subst,[],[refute_0_27:[bind(X,$fot(X_1731)),bind(Y,$fot(X_1731))]]) ).

cnf(refute_0_285,plain,
    is_a_theorem(implies(X_1731,X_1731)),
    inference(resolve,[$cnf( is_a_theorem(implies(X_1731,implies(X_1731,X_1731))) )],[refute_0_283,refute_0_284]) ).

cnf(refute_0_286,plain,
    is_a_theorem(implies(X_1739,X_1739)),
    inference(subst,[],[refute_0_285:[bind(X_1731,$fot(X_1739))]]) ).

cnf(refute_0_287,plain,
    is_a_theorem(equiv(X_1739,X_1739)),
    inference(resolve,[$cnf( is_a_theorem(implies(X_1739,X_1739)) )],[refute_0_286,refute_0_279]) ).

cnf(refute_0_288,plain,
    is_a_theorem(equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))),
    inference(subst,[],[refute_0_287:[bind(X_1739,$fot(necessarily(skolemFOFtoCNF_X_21)))]]) ).

cnf(refute_0_289,plain,
    $false,
    inference(resolve,[$cnf( is_a_theorem(equiv(necessarily(skolemFOFtoCNF_X_21),necessarily(skolemFOFtoCNF_X_21))) )],[refute_0_288,refute_0_270]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : LCL523+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04  % Command  : metis --show proof --show saturation %s
% 0.10/0.36  % Computer : n003.cluster.edu
% 0.10/0.36  % Model    : x86_64 x86_64
% 0.10/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36  % Memory   : 8046.5625MB
% 0.10/0.36  % OS       : Linux 6.8.0-71-generic
% 0.10/0.36  % CPULimit : 300
% 0.10/0.36  % WCLimit  : 300
% 0.10/0.36  % DateTime : Sat Sep  5 19:28:06 UTC 2026
% 0.13/0.36  % CPUTime  : 
% 0.13/0.37  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 49.25/49.57  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 49.25/49.57  
% 49.25/49.57  % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 49.35/49.68  
%------------------------------------------------------------------------------