%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL400-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n026.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:36 PM UTC 2026
% Result : Unsatisfiable 113.03s 113.38s
% Output : CNFRefutation 113.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 5
% Syntax : Number of clauses : 338 ( 196 unt; 0 nHn; 91 RR)
% Number of literals : 507 ( 0 equ; 170 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 939 ( 164 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(cn_1,axiom,
is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
cnf(cn_2,axiom,
is_a_theorem(implies(implies(not(X),X),X)) ).
cnf(cn_3,axiom,
is_a_theorem(implies(X,implies(not(X),Y))) ).
cnf(prove_cn_66,negated_conjecture,
~ is_a_theorem(implies(not(implies(x,y)),x)) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(implies(not(implies(implies(not(X_102),X_101),X_103)),implies(implies(not(X_102),X_101),X_103)),implies(X_102,X_103)))
| ~ is_a_theorem(implies(not(implies(implies(not(X_102),X_101),X_103)),implies(implies(not(X_102),X_101),X_103)))
| is_a_theorem(implies(X_102,X_103)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(implies(implies(not(X_102),X_101),X_103)),implies(implies(not(X_102),X_101),X_103)))),bind(Y,$fot(implies(X_102,X_103)))]]) ).
cnf(refute_0_1,plain,
( ~ is_a_theorem(implies(X_21,X_22))
| ~ is_a_theorem(implies(implies(X_21,X_22),implies(implies(not(X_21),X_21),X_22)))
| is_a_theorem(implies(implies(not(X_21),X_21),X_22)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_21,X_22))),bind(Y,$fot(implies(implies(not(X_21),X_21),X_22)))]]) ).
cnf(refute_0_2,plain,
is_a_theorem(implies(implies(not(X_19),X_19),X_19)),
inference(subst,[],[cn_2:[bind(X,$fot(X_19))]]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(Y,Z),implies(X,Z))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z))))]]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(implies(X,Y))
| is_a_theorem(implies(implies(Y,Z),implies(X,Z))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_3]) ).
cnf(refute_0_5,plain,
( ~ is_a_theorem(implies(implies(not(X_19),X_19),X_19))
| is_a_theorem(implies(implies(X_19,X_20),implies(implies(not(X_19),X_19),X_20))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(not(X_19),X_19))),bind(Y,$fot(X_19)),bind(Z,$fot(X_20))]]) ).
cnf(refute_0_6,plain,
is_a_theorem(implies(implies(X_19,X_20),implies(implies(not(X_19),X_19),X_20))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_19),X_19),X_19)) )],[refute_0_2,refute_0_5]) ).
cnf(refute_0_7,plain,
is_a_theorem(implies(implies(X_21,X_22),implies(implies(not(X_21),X_21),X_22))),
inference(subst,[],[refute_0_6:[bind(X_19,$fot(X_21)),bind(X_20,$fot(X_22))]]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(implies(X_21,X_22))
| is_a_theorem(implies(implies(not(X_21),X_21),X_22)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_21,X_22),implies(implies(not(X_21),X_21),X_22))) )],[refute_0_7,refute_0_1]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_27),X_26),X_28),implies(X_27,X_28)))
| is_a_theorem(implies(implies(not(implies(implies(not(X_27),X_26),X_28)),implies(implies(not(X_27),X_26),X_28)),implies(X_27,X_28))) ),
inference(subst,[],[refute_0_8:[bind(X_21,$fot(implies(implies(not(X_27),X_26),X_28))),bind(X_22,$fot(implies(X_27,X_28)))]]) ).
cnf(refute_0_10,plain,
is_a_theorem(implies(X_18,implies(not(X_18),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_18))]]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(implies(X_18,implies(not(X_18),Y)))
| is_a_theorem(implies(implies(implies(not(X_18),Y),X_20),implies(X_18,X_20))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_18)),bind(Y,$fot(implies(not(X_18),Y))),bind(Z,$fot(X_20))]]) ).
cnf(refute_0_12,plain,
is_a_theorem(implies(implies(implies(not(X_18),Y),X_20),implies(X_18,X_20))),
inference(resolve,[$cnf( is_a_theorem(implies(X_18,implies(not(X_18),Y))) )],[refute_0_10,refute_0_11]) ).
cnf(refute_0_13,plain,
is_a_theorem(implies(implies(implies(not(X_27),X_26),X_28),implies(X_27,X_28))),
inference(subst,[],[refute_0_12:[bind(Y,$fot(X_26)),bind(X_18,$fot(X_27)),bind(X_20,$fot(X_28))]]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(implies(not(implies(implies(not(X_27),X_26),X_28)),implies(implies(not(X_27),X_26),X_28)),implies(X_27,X_28))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_27),X_26),X_28),implies(X_27,X_28))) )],[refute_0_13,refute_0_9]) ).
cnf(refute_0_15,plain,
is_a_theorem(implies(implies(not(implies(implies(not(X_102),X_101),X_103)),implies(implies(not(X_102),X_101),X_103)),implies(X_102,X_103))),
inference(subst,[],[refute_0_14:[bind(X_26,$fot(X_101)),bind(X_27,$fot(X_102)),bind(X_28,$fot(X_103))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(X_102),X_101),X_103)),implies(implies(not(X_102),X_101),X_103)))
| is_a_theorem(implies(X_102,X_103)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(implies(not(X_102),X_101),X_103)),implies(implies(not(X_102),X_101),X_103)),implies(X_102,X_103))) )],[refute_0_15,refute_0_0]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(not(implies(X_39429,X_39430))),X_39429),X_39429)),implies(implies(not(not(implies(X_39429,X_39430))),X_39429),X_39429)))
| is_a_theorem(implies(not(implies(X_39429,X_39430)),X_39429)) ),
inference(subst,[],[refute_0_16:[bind(X_101,$fot(X_39429)),bind(X_102,$fot(not(implies(X_39429,X_39430)))),bind(X_103,$fot(X_39429))]]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(implies(X_1637,implies(not(X_1635),X_1635)))
| ~ is_a_theorem(implies(implies(X_1637,implies(not(X_1635),X_1635)),implies(X_1636,implies(X_1637,X_1635))))
| is_a_theorem(implies(X_1636,implies(X_1637,X_1635))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_1637,implies(not(X_1635),X_1635)))),bind(Y,$fot(implies(X_1636,implies(X_1637,X_1635))))]]) ).
cnf(refute_0_19,plain,
( ~ is_a_theorem(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82))
| ~ is_a_theorem(implies(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82),implies(implies(X_79,X_80),X_82)))
| is_a_theorem(implies(implies(X_79,X_80),X_82)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82))),bind(Y,$fot(implies(implies(X_79,X_80),X_82)))]]) ).
cnf(refute_0_20,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_20),implies(implies(X,Y),X_20))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(X,Y))),bind(Y,$fot(implies(implies(Y,Z),implies(X,Z)))),bind(Z,$fot(X_20))]]) ).
cnf(refute_0_21,plain,
is_a_theorem(implies(implies(implies(implies(Y,Z),implies(X,Z)),X_20),implies(implies(X,Y),X_20))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_20]) ).
cnf(refute_0_22,plain,
is_a_theorem(implies(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82),implies(implies(X_79,X_80),X_82))),
inference(subst,[],[refute_0_21:[bind(X,$fot(X_79)),bind(Y,$fot(X_80)),bind(Z,$fot(X_81)),bind(X_20,$fot(X_82))]]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82))
| is_a_theorem(implies(implies(X_79,X_80),X_82)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82),implies(implies(X_79,X_80),X_82))) )],[refute_0_22,refute_0_19]) ).
cnf(refute_0_24,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_1588),X_1588),X_1588),implies(X_79,X_1588)),implies(X_1589,implies(X_79,X_1588))))
| is_a_theorem(implies(implies(X_79,implies(not(X_1588),X_1588)),implies(X_1589,implies(X_79,X_1588)))) ),
inference(subst,[],[refute_0_23:[bind(X_80,$fot(implies(not(X_1588),X_1588))),bind(X_81,$fot(X_1588)),bind(X_82,$fot(implies(X_1589,implies(X_79,X_1588))))]]) ).
cnf(refute_0_25,plain,
( ~ is_a_theorem(implies(X_251,implies(not(implies(implies(not(X_249),X_249),X_249)),X_250)))
| is_a_theorem(implies(implies(implies(not(implies(implies(not(X_249),X_249),X_249)),X_250),Z),implies(X_251,Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_251)),bind(Y,$fot(implies(not(implies(implies(not(X_249),X_249),X_249)),X_250)))]]) ).
cnf(refute_0_26,plain,
is_a_theorem(implies(X_6,implies(not(X_6),Y))),
inference(subst,[],[cn_3:[bind(X,$fot(X_6))]]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(X_6)
| ~ is_a_theorem(implies(X_6,implies(not(X_6),Y)))
| is_a_theorem(implies(not(X_6),Y)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_6)),bind(Y,$fot(implies(not(X_6),Y)))]]) ).
cnf(refute_0_28,plain,
( ~ is_a_theorem(X_6)
| is_a_theorem(implies(not(X_6),Y)) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_6,implies(not(X_6),Y))) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
( ~ is_a_theorem(implies(implies(not(X),X),X))
| is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_8)) ),
inference(subst,[],[refute_0_28:[bind(Y,$fot(X_8)),bind(X_6,$fot(implies(implies(not(X),X),X)))]]) ).
cnf(refute_0_30,plain,
is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_8)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X),X),X)) )],[cn_2,refute_0_29]) ).
cnf(refute_0_31,plain,
is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_19)),
inference(subst,[],[refute_0_30:[bind(X_8,$fot(X_19))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_19))
| is_a_theorem(implies(implies(X_19,X_20),implies(not(implies(implies(not(X),X),X)),X_20))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(not(implies(implies(not(X),X),X)))),bind(Y,$fot(X_19)),bind(Z,$fot(X_20))]]) ).
cnf(refute_0_33,plain,
is_a_theorem(implies(implies(X_19,X_20),implies(not(implies(implies(not(X),X),X)),X_20))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(X),X),X)),X_19)) )],[refute_0_31,refute_0_32]) ).
cnf(refute_0_34,plain,
is_a_theorem(implies(implies(not(X_235),X_234),implies(not(implies(implies(not(X),X),X)),X_234))),
inference(subst,[],[refute_0_33:[bind(X_19,$fot(not(X_235))),bind(X_20,$fot(X_234))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_27),X_26),X_28),implies(X_27,X_28)))
| ~ is_a_theorem(implies(implies(not(X_27),X_26),X_28))
| is_a_theorem(implies(X_27,X_28)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(X_27),X_26),X_28))),bind(Y,$fot(implies(X_27,X_28)))]]) ).
cnf(refute_0_36,plain,
( ~ is_a_theorem(implies(implies(not(X_27),X_26),X_28))
| is_a_theorem(implies(X_27,X_28)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_27),X_26),X_28),implies(X_27,X_28))) )],[refute_0_13,refute_0_35]) ).
cnf(refute_0_37,plain,
( ~ is_a_theorem(implies(implies(not(X_235),X_234),implies(not(implies(implies(not(X),X),X)),X_234)))
| is_a_theorem(implies(X_235,implies(not(implies(implies(not(X),X),X)),X_234))) ),
inference(subst,[],[refute_0_36:[bind(X_26,$fot(X_234)),bind(X_27,$fot(X_235)),bind(X_28,$fot(implies(not(implies(implies(not(X),X),X)),X_234)))]]) ).
cnf(refute_0_38,plain,
is_a_theorem(implies(X_235,implies(not(implies(implies(not(X),X),X)),X_234))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_235),X_234),implies(not(implies(implies(not(X),X),X)),X_234))) )],[refute_0_34,refute_0_37]) ).
cnf(refute_0_39,plain,
is_a_theorem(implies(X_251,implies(not(implies(implies(not(X_249),X_249),X_249)),X_250))),
inference(subst,[],[refute_0_38:[bind(X,$fot(X_249)),bind(X_234,$fot(X_250)),bind(X_235,$fot(X_251))]]) ).
cnf(refute_0_40,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_249),X_249),X_249)),X_250),Z),implies(X_251,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_251,implies(not(implies(implies(not(X_249),X_249),X_249)),X_250))) )],[refute_0_39,refute_0_25]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_249),X_249),X_249)),implies(implies(not(X_249),X_249),X_249)),X_1583),implies(X_251,X_1583))),
inference(subst,[],[refute_0_40:[bind(Z,$fot(X_1583)),bind(X_250,$fot(implies(implies(not(X_249),X_249),X_249)))]]) ).
cnf(refute_0_42,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_33),X_33),X_34),X_32),implies(implies(X_33,X_34),X_32)))
| ~ is_a_theorem(implies(implies(implies(not(X_33),X_33),X_34),X_32))
| is_a_theorem(implies(implies(X_33,X_34),X_32)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(not(X_33),X_33),X_34),X_32))),bind(Y,$fot(implies(implies(X_33,X_34),X_32)))]]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(implies(implies(X_21,X_22),implies(implies(not(X_21),X_21),X_22)))
| is_a_theorem(implies(implies(implies(implies(not(X_21),X_21),X_22),Z),implies(implies(X_21,X_22),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(X_21,X_22))),bind(Y,$fot(implies(implies(not(X_21),X_21),X_22)))]]) ).
cnf(refute_0_44,plain,
is_a_theorem(implies(implies(implies(implies(not(X_21),X_21),X_22),Z),implies(implies(X_21,X_22),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_21,X_22),implies(implies(not(X_21),X_21),X_22))) )],[refute_0_7,refute_0_43]) ).
cnf(refute_0_45,plain,
is_a_theorem(implies(implies(implies(implies(not(X_33),X_33),X_34),X_32),implies(implies(X_33,X_34),X_32))),
inference(subst,[],[refute_0_44:[bind(Z,$fot(X_32)),bind(X_21,$fot(X_33)),bind(X_22,$fot(X_34))]]) ).
cnf(refute_0_46,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_33),X_33),X_34),X_32))
| is_a_theorem(implies(implies(X_33,X_34),X_32)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_33),X_33),X_34),X_32),implies(implies(X_33,X_34),X_32))) )],[refute_0_45,refute_0_42]) ).
cnf(refute_0_47,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(implies(not(X_249),X_249),X_249)),implies(implies(not(X_249),X_249),X_249)),X_1583),implies(X_251,X_1583)))
| is_a_theorem(implies(implies(implies(implies(not(X_249),X_249),X_249),X_1583),implies(X_251,X_1583))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(X_251,X_1583))),bind(X_33,$fot(implies(implies(not(X_249),X_249),X_249))),bind(X_34,$fot(X_1583))]]) ).
cnf(refute_0_48,plain,
is_a_theorem(implies(implies(implies(implies(not(X_249),X_249),X_249),X_1583),implies(X_251,X_1583))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(implies(not(X_249),X_249),X_249)),implies(implies(not(X_249),X_249),X_249)),X_1583),implies(X_251,X_1583))) )],[refute_0_41,refute_0_47]) ).
cnf(refute_0_49,plain,
is_a_theorem(implies(implies(implies(implies(not(X_1588),X_1588),X_1588),implies(X_79,X_1588)),implies(X_1589,implies(X_79,X_1588)))),
inference(subst,[],[refute_0_48:[bind(X_1583,$fot(implies(X_79,X_1588))),bind(X_249,$fot(X_1588)),bind(X_251,$fot(X_1589))]]) ).
cnf(refute_0_50,plain,
is_a_theorem(implies(implies(X_79,implies(not(X_1588),X_1588)),implies(X_1589,implies(X_79,X_1588)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_1588),X_1588),X_1588),implies(X_79,X_1588)),implies(X_1589,implies(X_79,X_1588)))) )],[refute_0_49,refute_0_24]) ).
cnf(refute_0_51,plain,
is_a_theorem(implies(implies(X_1637,implies(not(X_1635),X_1635)),implies(X_1636,implies(X_1637,X_1635)))),
inference(subst,[],[refute_0_50:[bind(X_1588,$fot(X_1635)),bind(X_1589,$fot(X_1636)),bind(X_79,$fot(X_1637))]]) ).
cnf(refute_0_52,plain,
( ~ is_a_theorem(implies(X_1637,implies(not(X_1635),X_1635)))
| is_a_theorem(implies(X_1636,implies(X_1637,X_1635))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1637,implies(not(X_1635),X_1635)),implies(X_1636,implies(X_1637,X_1635)))) )],[refute_0_51,refute_0_18]) ).
cnf(refute_0_53,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(X_39158,X_39160))),X_39158),implies(not(X_39158),X_39158)))
| is_a_theorem(implies(X_1636,implies(implies(not(not(implies(X_39158,X_39160))),X_39158),X_39158))) ),
inference(subst,[],[refute_0_52:[bind(X_1635,$fot(X_39158)),bind(X_1637,$fot(implies(not(not(implies(X_39158,X_39160))),X_39158)))]]) ).
cnf(refute_0_54,plain,
( ~ is_a_theorem(implies(not(X_39135),not(not(implies(X_39135,X_39136)))))
| is_a_theorem(implies(implies(not(not(implies(X_39135,X_39136))),Z),implies(not(X_39135),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(not(X_39135))),bind(Y,$fot(not(not(implies(X_39135,X_39136)))))]]) ).
cnf(refute_0_55,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(not(X_39132)),X_39133),not(not(implies(X_39132,X_39133))))),implies(implies(not(not(X_39132)),X_39133),not(not(implies(X_39132,X_39133))))))
| is_a_theorem(implies(not(X_39132),not(not(implies(X_39132,X_39133))))) ),
inference(subst,[],[refute_0_16:[bind(X_101,$fot(X_39133)),bind(X_102,$fot(not(X_39132))),bind(X_103,$fot(not(not(implies(X_39132,X_39133)))))]]) ).
cnf(refute_0_56,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(X_7702)),X_7702),X_7701),X_7701))
| ~ is_a_theorem(implies(implies(not(not(X_7702)),X_7702),X_7701))
| is_a_theorem(X_7701) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(not(X_7702)),X_7702),X_7701))),bind(Y,$fot(X_7701))]]) ).
cnf(refute_0_57,plain,
( ~ is_a_theorem(X_7284)
| ~ is_a_theorem(implies(X_7284,implies(implies(X_7284,X_7283),X_7283)))
| is_a_theorem(implies(implies(X_7284,X_7283),X_7283)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_7284)),bind(Y,$fot(implies(implies(X_7284,X_7283),X_7283)))]]) ).
cnf(refute_0_58,plain,
( ~ is_a_theorem(implies(implies(X_273,implies(not(X_274),X_272)),X_271))
| ~ is_a_theorem(implies(implies(implies(X_273,implies(not(X_274),X_272)),X_271),implies(X_274,X_271)))
| is_a_theorem(implies(X_274,X_271)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_273,implies(not(X_274),X_272)),X_271))),bind(Y,$fot(implies(X_274,X_271)))]]) ).
cnf(refute_0_59,plain,
( ~ is_a_theorem(implies(X_248,implies(X_247,implies(not(X_248),X_246))))
| is_a_theorem(implies(implies(implies(X_247,implies(not(X_248),X_246)),Z),implies(X_248,Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_248)),bind(Y,$fot(implies(X_247,implies(not(X_248),X_246))))]]) ).
cnf(refute_0_60,plain,
is_a_theorem(implies(implies(implies(not(X_18),X_166),implies(X_164,X_166)),implies(X_18,implies(X_164,X_166)))),
inference(subst,[],[refute_0_12:[bind(Y,$fot(X_166)),bind(X_20,$fot(implies(X_164,X_166)))]]) ).
cnf(refute_0_61,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_18),X_166),implies(X_164,X_166)),implies(X_18,implies(X_164,X_166))))
| is_a_theorem(implies(implies(X_164,not(X_18)),implies(X_18,implies(X_164,X_166)))) ),
inference(subst,[],[refute_0_23:[bind(X_79,$fot(X_164)),bind(X_80,$fot(not(X_18))),bind(X_81,$fot(X_166)),bind(X_82,$fot(implies(X_18,implies(X_164,X_166))))]]) ).
cnf(refute_0_62,plain,
is_a_theorem(implies(implies(X_164,not(X_18)),implies(X_18,implies(X_164,X_166)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_18),X_166),implies(X_164,X_166)),implies(X_18,implies(X_164,X_166)))) )],[refute_0_60,refute_0_61]) ).
cnf(refute_0_63,plain,
is_a_theorem(implies(implies(not(X_235),not(X_18)),implies(X_18,implies(not(X_235),X_166)))),
inference(subst,[],[refute_0_62:[bind(X_164,$fot(not(X_235)))]]) ).
cnf(refute_0_64,plain,
( ~ is_a_theorem(implies(implies(not(X_235),not(X_18)),implies(X_18,implies(not(X_235),X_166))))
| is_a_theorem(implies(X_235,implies(X_18,implies(not(X_235),X_166)))) ),
inference(subst,[],[refute_0_36:[bind(X_26,$fot(not(X_18))),bind(X_27,$fot(X_235)),bind(X_28,$fot(implies(X_18,implies(not(X_235),X_166))))]]) ).
cnf(refute_0_65,plain,
is_a_theorem(implies(X_235,implies(X_18,implies(not(X_235),X_166)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_235),not(X_18)),implies(X_18,implies(not(X_235),X_166)))) )],[refute_0_63,refute_0_64]) ).
cnf(refute_0_66,plain,
is_a_theorem(implies(X_248,implies(X_247,implies(not(X_248),X_246)))),
inference(subst,[],[refute_0_65:[bind(X_166,$fot(X_246)),bind(X_18,$fot(X_247)),bind(X_235,$fot(X_248))]]) ).
cnf(refute_0_67,plain,
is_a_theorem(implies(implies(implies(X_247,implies(not(X_248),X_246)),Z),implies(X_248,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_248,implies(X_247,implies(not(X_248),X_246)))) )],[refute_0_66,refute_0_59]) ).
cnf(refute_0_68,plain,
is_a_theorem(implies(implies(implies(X_273,implies(not(X_274),X_272)),X_271),implies(X_274,X_271))),
inference(subst,[],[refute_0_67:[bind(Z,$fot(X_271)),bind(X_246,$fot(X_272)),bind(X_247,$fot(X_273)),bind(X_248,$fot(X_274))]]) ).
cnf(refute_0_69,plain,
( ~ is_a_theorem(implies(implies(X_273,implies(not(X_274),X_272)),X_271))
| is_a_theorem(implies(X_274,X_271)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_273,implies(not(X_274),X_272)),X_271),implies(X_274,X_271))) )],[refute_0_68,refute_0_58]) ).
cnf(refute_0_70,plain,
( ~ is_a_theorem(implies(implies(not(X_7281),implies(not(X_7282),X_7282)),implies(implies(X_7282,X_7281),X_7281)))
| is_a_theorem(implies(X_7282,implies(implies(X_7282,X_7281),X_7281))) ),
inference(subst,[],[refute_0_69:[bind(X_271,$fot(implies(implies(X_7282,X_7281),X_7281))),bind(X_272,$fot(X_7282)),bind(X_273,$fot(not(X_7281))),bind(X_274,$fot(X_7282))]]) ).
cnf(refute_0_71,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(not(not(X_3587))),not(not(X_3587))),X_3588),X_3587),X_3587))
| ~ is_a_theorem(implies(implies(implies(not(not(not(X_3587))),not(not(X_3587))),X_3588),X_3587))
| is_a_theorem(X_3587) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(not(not(not(X_3587))),not(not(X_3587))),X_3588),X_3587))),bind(Y,$fot(X_3587))]]) ).
cnf(refute_0_72,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(X_373)),X_374),X_373),X_373))
| ~ is_a_theorem(implies(implies(not(not(X_373)),X_374),X_373))
| is_a_theorem(X_373) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(not(X_373)),X_374),X_373))),bind(Y,$fot(X_373))]]) ).
cnf(refute_0_73,plain,
is_a_theorem(implies(implies(not(X_369),X_369),X_369)),
inference(subst,[],[cn_2:[bind(X,$fot(X_369))]]) ).
cnf(refute_0_74,plain,
( ~ is_a_theorem(implies(implies(X_40,X_41),X_38))
| ~ is_a_theorem(implies(implies(implies(X_40,X_41),X_38),implies(implies(implies(not(X_40),X_39),X_41),X_38)))
| is_a_theorem(implies(implies(implies(not(X_40),X_39),X_41),X_38)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_40,X_41),X_38))),bind(Y,$fot(implies(implies(implies(not(X_40),X_39),X_41),X_38)))]]) ).
cnf(refute_0_75,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_27),X_26),X_28),implies(X_27,X_28)))
| is_a_theorem(implies(implies(implies(X_27,X_28),Z),implies(implies(implies(not(X_27),X_26),X_28),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(implies(not(X_27),X_26),X_28))),bind(Y,$fot(implies(X_27,X_28)))]]) ).
cnf(refute_0_76,plain,
is_a_theorem(implies(implies(implies(X_27,X_28),Z),implies(implies(implies(not(X_27),X_26),X_28),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_27),X_26),X_28),implies(X_27,X_28))) )],[refute_0_13,refute_0_75]) ).
cnf(refute_0_77,plain,
is_a_theorem(implies(implies(implies(X_40,X_41),X_38),implies(implies(implies(not(X_40),X_39),X_41),X_38))),
inference(subst,[],[refute_0_76:[bind(Z,$fot(X_38)),bind(X_26,$fot(X_39)),bind(X_27,$fot(X_40)),bind(X_28,$fot(X_41))]]) ).
cnf(refute_0_78,plain,
( ~ is_a_theorem(implies(implies(X_40,X_41),X_38))
| is_a_theorem(implies(implies(implies(not(X_40),X_39),X_41),X_38)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_40,X_41),X_38),implies(implies(implies(not(X_40),X_39),X_41),X_38))) )],[refute_0_77,refute_0_74]) ).
cnf(refute_0_79,plain,
( ~ is_a_theorem(implies(implies(not(X_369),X_369),X_369))
| is_a_theorem(implies(implies(implies(not(not(X_369)),X_370),X_369),X_369)) ),
inference(subst,[],[refute_0_78:[bind(X_38,$fot(X_369)),bind(X_39,$fot(X_370)),bind(X_40,$fot(not(X_369))),bind(X_41,$fot(X_369))]]) ).
cnf(refute_0_80,plain,
is_a_theorem(implies(implies(implies(not(not(X_369)),X_370),X_369),X_369)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_369),X_369),X_369)) )],[refute_0_73,refute_0_79]) ).
cnf(refute_0_81,plain,
is_a_theorem(implies(implies(implies(not(not(X_373)),X_374),X_373),X_373)),
inference(subst,[],[refute_0_80:[bind(X_369,$fot(X_373)),bind(X_370,$fot(X_374))]]) ).
cnf(refute_0_82,plain,
( ~ is_a_theorem(implies(implies(not(not(X_373)),X_374),X_373))
| is_a_theorem(X_373) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(X_373)),X_374),X_373),X_373)) )],[refute_0_81,refute_0_72]) ).
cnf(refute_0_83,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585))),X_374),implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585)))
| is_a_theorem(implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585)) ),
inference(subst,[],[refute_0_82:[bind(X_373,$fot(implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585)))]]) ).
cnf(refute_0_84,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(implies(not(X_283),X_283),X_283)),X_284),X_282),implies(X_285,X_282)))
| ~ is_a_theorem(implies(implies(not(implies(implies(not(X_283),X_283),X_283)),X_284),X_282))
| is_a_theorem(implies(X_285,X_282)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(implies(implies(not(X_283),X_283),X_283)),X_284),X_282))),bind(Y,$fot(implies(X_285,X_282)))]]) ).
cnf(refute_0_85,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(not(X_283),X_283),X_283)),X_284),X_282),implies(X_285,X_282))),
inference(subst,[],[refute_0_40:[bind(Z,$fot(X_282)),bind(X_249,$fot(X_283)),bind(X_250,$fot(X_284)),bind(X_251,$fot(X_285))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(implies(implies(not(implies(implies(not(X_283),X_283),X_283)),X_284),X_282))
| is_a_theorem(implies(X_285,X_282)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(implies(not(X_283),X_283),X_283)),X_284),X_282),implies(X_285,X_282))) )],[refute_0_85,refute_0_84]) ).
cnf(refute_0_87,plain,
( ~ is_a_theorem(implies(implies(not(implies(implies(not(X_3576),X_3576),X_3576)),implies(implies(not(X_3576),X_3576),X_3576)),implies(implies(implies(implies(not(not(not(X_3576))),not(not(X_3576))),X_3578),X_3576),X_3576)))
| is_a_theorem(implies(X_285,implies(implies(implies(implies(not(not(not(X_3576))),not(not(X_3576))),X_3578),X_3576),X_3576))) ),
inference(subst,[],[refute_0_86:[bind(X_282,$fot(implies(implies(implies(implies(not(not(not(X_3576))),not(not(X_3576))),X_3578),X_3576),X_3576))),bind(X_283,$fot(X_3576)),bind(X_284,$fot(implies(implies(not(X_3576),X_3576),X_3576)))]]) ).
cnf(refute_0_88,plain,
( ~ is_a_theorem(implies(implies(implies(X_511,X_509),X_508),implies(implies(implies(implies(not(not(X_511)),not(X_511)),X_510),X_509),X_508)))
| is_a_theorem(implies(implies(not(implies(implies(X_511,X_509),X_508)),implies(implies(X_511,X_509),X_508)),implies(implies(implies(implies(not(not(X_511)),not(X_511)),X_510),X_509),X_508))) ),
inference(subst,[],[refute_0_8:[bind(X_21,$fot(implies(implies(X_511,X_509),X_508))),bind(X_22,$fot(implies(implies(implies(implies(not(not(X_511)),not(X_511)),X_510),X_509),X_508)))]]) ).
cnf(refute_0_89,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(not(X_320)),not(X_320)),X_319),X_318),implies(X_320,X_318)))
| is_a_theorem(implies(implies(implies(X_320,X_318),Z),implies(implies(implies(implies(not(not(X_320)),not(X_320)),X_319),X_318),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(implies(implies(not(not(X_320)),not(X_320)),X_319),X_318))),bind(Y,$fot(implies(X_320,X_318)))]]) ).
cnf(refute_0_90,plain,
( ~ is_a_theorem(implies(X_257,implies(implies(not(not(X_257)),not(X_257)),X_256)))
| is_a_theorem(implies(implies(implies(implies(not(not(X_257)),not(X_257)),X_256),Z),implies(X_257,Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_257)),bind(Y,$fot(implies(implies(not(not(X_257)),not(X_257)),X_256)))]]) ).
cnf(refute_0_91,plain,
is_a_theorem(implies(implies(not(X_235),X_234),implies(implies(not(not(X_235)),not(X_235)),X_234))),
inference(subst,[],[refute_0_6:[bind(X_19,$fot(not(X_235))),bind(X_20,$fot(X_234))]]) ).
cnf(refute_0_92,plain,
( ~ is_a_theorem(implies(implies(not(X_235),X_234),implies(implies(not(not(X_235)),not(X_235)),X_234)))
| is_a_theorem(implies(X_235,implies(implies(not(not(X_235)),not(X_235)),X_234))) ),
inference(subst,[],[refute_0_36:[bind(X_26,$fot(X_234)),bind(X_27,$fot(X_235)),bind(X_28,$fot(implies(implies(not(not(X_235)),not(X_235)),X_234)))]]) ).
cnf(refute_0_93,plain,
is_a_theorem(implies(X_235,implies(implies(not(not(X_235)),not(X_235)),X_234))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_235),X_234),implies(implies(not(not(X_235)),not(X_235)),X_234))) )],[refute_0_91,refute_0_92]) ).
cnf(refute_0_94,plain,
is_a_theorem(implies(X_257,implies(implies(not(not(X_257)),not(X_257)),X_256))),
inference(subst,[],[refute_0_93:[bind(X_234,$fot(X_256)),bind(X_235,$fot(X_257))]]) ).
cnf(refute_0_95,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X_257)),not(X_257)),X_256),Z),implies(X_257,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_257,implies(implies(not(not(X_257)),not(X_257)),X_256))) )],[refute_0_94,refute_0_90]) ).
cnf(refute_0_96,plain,
is_a_theorem(implies(implies(implies(implies(not(not(X_320)),not(X_320)),X_319),X_318),implies(X_320,X_318))),
inference(subst,[],[refute_0_95:[bind(Z,$fot(X_318)),bind(X_256,$fot(X_319)),bind(X_257,$fot(X_320))]]) ).
cnf(refute_0_97,plain,
is_a_theorem(implies(implies(implies(X_320,X_318),Z),implies(implies(implies(implies(not(not(X_320)),not(X_320)),X_319),X_318),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(not(X_320)),not(X_320)),X_319),X_318),implies(X_320,X_318))) )],[refute_0_96,refute_0_89]) ).
cnf(refute_0_98,plain,
is_a_theorem(implies(implies(implies(X_511,X_509),X_508),implies(implies(implies(implies(not(not(X_511)),not(X_511)),X_510),X_509),X_508))),
inference(subst,[],[refute_0_97:[bind(Z,$fot(X_508)),bind(X_318,$fot(X_509)),bind(X_319,$fot(X_510)),bind(X_320,$fot(X_511))]]) ).
cnf(refute_0_99,plain,
is_a_theorem(implies(implies(not(implies(implies(X_511,X_509),X_508)),implies(implies(X_511,X_509),X_508)),implies(implies(implies(implies(not(not(X_511)),not(X_511)),X_510),X_509),X_508))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_511,X_509),X_508),implies(implies(implies(implies(not(not(X_511)),not(X_511)),X_510),X_509),X_508))) )],[refute_0_98,refute_0_88]) ).
cnf(refute_0_100,plain,
is_a_theorem(implies(implies(not(implies(implies(not(X_3576),X_3576),X_3576)),implies(implies(not(X_3576),X_3576),X_3576)),implies(implies(implies(implies(not(not(not(X_3576))),not(not(X_3576))),X_3578),X_3576),X_3576))),
inference(subst,[],[refute_0_99:[bind(X_508,$fot(X_3576)),bind(X_509,$fot(X_3576)),bind(X_510,$fot(X_3578)),bind(X_511,$fot(not(X_3576)))]]) ).
cnf(refute_0_101,plain,
is_a_theorem(implies(X_285,implies(implies(implies(implies(not(not(not(X_3576))),not(not(X_3576))),X_3578),X_3576),X_3576))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(implies(not(X_3576),X_3576),X_3576)),implies(implies(not(X_3576),X_3576),X_3576)),implies(implies(implies(implies(not(not(not(X_3576))),not(not(X_3576))),X_3578),X_3576),X_3576))) )],[refute_0_100,refute_0_87]) ).
cnf(refute_0_102,plain,
is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585))),X_374),implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585))),
inference(subst,[],[refute_0_101:[bind(X_285,$fot(implies(not(not(implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585))),X_374))),bind(X_3576,$fot(X_3585)),bind(X_3578,$fot(X_3586))]]) ).
cnf(refute_0_103,plain,
is_a_theorem(implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585))),X_374),implies(implies(implies(implies(not(not(not(X_3585))),not(not(X_3585))),X_3586),X_3585),X_3585))) )],[refute_0_102,refute_0_83]) ).
cnf(refute_0_104,plain,
is_a_theorem(implies(implies(implies(implies(not(not(not(X_3587))),not(not(X_3587))),X_3588),X_3587),X_3587)),
inference(subst,[],[refute_0_103:[bind(X_3585,$fot(X_3587)),bind(X_3586,$fot(X_3588))]]) ).
cnf(refute_0_105,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(not(X_3587))),not(not(X_3587))),X_3588),X_3587))
| is_a_theorem(X_3587) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(not(not(X_3587))),not(not(X_3587))),X_3588),X_3587),X_3587)) )],[refute_0_104,refute_0_71]) ).
cnf(refute_0_106,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(not(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))),not(not(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))),X_3588),implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))
| is_a_theorem(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))) ),
inference(subst,[],[refute_0_105:[bind(X_3587,$fot(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))]]) ).
cnf(refute_0_107,plain,
( ~ is_a_theorem(implies(implies(not(implies(implies(not(X_7158),X_7158),X_7158)),implies(implies(not(X_7158),X_7158),X_7158)),implies(implies(not(X_7157),implies(not(X_7158),X_7158)),implies(implies(X_7158,X_7157),X_7157))))
| is_a_theorem(implies(X_285,implies(implies(not(X_7157),implies(not(X_7158),X_7158)),implies(implies(X_7158,X_7157),X_7157)))) ),
inference(subst,[],[refute_0_86:[bind(X_282,$fot(implies(implies(not(X_7157),implies(not(X_7158),X_7158)),implies(implies(X_7158,X_7157),X_7157)))),bind(X_283,$fot(X_7158)),bind(X_284,$fot(implies(implies(not(X_7158),X_7158),X_7158)))]]) ).
cnf(refute_0_108,plain,
( ~ is_a_theorem(implies(implies(X_6989,X_6991),implies(implies(not(X_6990),X_6989),implies(implies(X_6991,X_6990),X_6990))))
| is_a_theorem(implies(implies(not(implies(X_6989,X_6991)),implies(X_6989,X_6991)),implies(implies(not(X_6990),X_6989),implies(implies(X_6991,X_6990),X_6990)))) ),
inference(subst,[],[refute_0_8:[bind(X_21,$fot(implies(X_6989,X_6991))),bind(X_22,$fot(implies(implies(not(X_6990),X_6989),implies(implies(X_6991,X_6990),X_6990))))]]) ).
cnf(refute_0_109,plain,
( ~ is_a_theorem(implies(implies(implies(X_80,X_6889),implies(X_6887,X_6889)),implies(implies(not(X_6889),X_6887),implies(implies(X_80,X_6889),X_6889))))
| is_a_theorem(implies(implies(X_6887,X_80),implies(implies(not(X_6889),X_6887),implies(implies(X_80,X_6889),X_6889)))) ),
inference(subst,[],[refute_0_23:[bind(X_79,$fot(X_6887)),bind(X_81,$fot(X_6889)),bind(X_82,$fot(implies(implies(not(X_6889),X_6887),implies(implies(X_80,X_6889),X_6889))))]]) ).
cnf(refute_0_110,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_3223,X_3222),X_3222),X_3221),implies(implies(not(X_3222),X_3223),X_3221)))
| is_a_theorem(implies(not(implies(implies(implies(implies(X_3223,X_3222),X_3222),X_3221),implies(implies(not(X_3222),X_3223),X_3221))),Y)) ),
inference(subst,[],[refute_0_28:[bind(X_6,$fot(implies(implies(implies(implies(X_3223,X_3222),X_3222),X_3221),implies(implies(not(X_3222),X_3223),X_3221))))]]) ).
cnf(refute_0_111,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(implies(X_1947,X_1945),X_1945)),implies(implies(X_1947,X_1945),X_1945)),X_1944),implies(implies(not(X_1945),X_1947),X_1944)))
| is_a_theorem(implies(implies(implies(implies(X_1947,X_1945),X_1945),X_1944),implies(implies(not(X_1945),X_1947),X_1944))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(implies(not(X_1945),X_1947),X_1944))),bind(X_33,$fot(implies(implies(X_1947,X_1945),X_1945))),bind(X_34,$fot(X_1944))]]) ).
cnf(refute_0_112,plain,
( ~ is_a_theorem(implies(implies(not(X_1937),X_1939),implies(X_1938,implies(implies(X_1939,X_1937),X_1937))))
| is_a_theorem(implies(implies(implies(X_1938,implies(implies(X_1939,X_1937),X_1937)),Z),implies(implies(not(X_1937),X_1939),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(not(X_1937),X_1939))),bind(Y,$fot(implies(X_1938,implies(implies(X_1939,X_1937),X_1937))))]]) ).
cnf(refute_0_113,plain,
( ~ is_a_theorem(implies(implies(implies(X_80,X_1635),implies(not(X_1635),X_1635)),implies(X_1636,implies(implies(X_80,X_1635),X_1635))))
| is_a_theorem(implies(implies(not(X_1635),X_80),implies(X_1636,implies(implies(X_80,X_1635),X_1635)))) ),
inference(subst,[],[refute_0_23:[bind(X_79,$fot(not(X_1635))),bind(X_81,$fot(X_1635)),bind(X_82,$fot(implies(X_1636,implies(implies(X_80,X_1635),X_1635))))]]) ).
cnf(refute_0_114,plain,
is_a_theorem(implies(implies(implies(X_80,X_1635),implies(not(X_1635),X_1635)),implies(X_1636,implies(implies(X_80,X_1635),X_1635)))),
inference(subst,[],[refute_0_50:[bind(X_1588,$fot(X_1635)),bind(X_1589,$fot(X_1636)),bind(X_79,$fot(implies(X_80,X_1635)))]]) ).
cnf(refute_0_115,plain,
is_a_theorem(implies(implies(not(X_1635),X_80),implies(X_1636,implies(implies(X_80,X_1635),X_1635)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_80,X_1635),implies(not(X_1635),X_1635)),implies(X_1636,implies(implies(X_80,X_1635),X_1635)))) )],[refute_0_114,refute_0_113]) ).
cnf(refute_0_116,plain,
is_a_theorem(implies(implies(not(X_1937),X_1939),implies(X_1938,implies(implies(X_1939,X_1937),X_1937)))),
inference(subst,[],[refute_0_115:[bind(X_1635,$fot(X_1937)),bind(X_1636,$fot(X_1938)),bind(X_80,$fot(X_1939))]]) ).
cnf(refute_0_117,plain,
is_a_theorem(implies(implies(implies(X_1938,implies(implies(X_1939,X_1937),X_1937)),Z),implies(implies(not(X_1937),X_1939),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_1937),X_1939),implies(X_1938,implies(implies(X_1939,X_1937),X_1937)))) )],[refute_0_116,refute_0_112]) ).
cnf(refute_0_118,plain,
is_a_theorem(implies(implies(implies(not(implies(implies(X_1947,X_1945),X_1945)),implies(implies(X_1947,X_1945),X_1945)),X_1944),implies(implies(not(X_1945),X_1947),X_1944))),
inference(subst,[],[refute_0_117:[bind(Z,$fot(X_1944)),bind(X_1937,$fot(X_1945)),bind(X_1938,$fot(not(implies(implies(X_1947,X_1945),X_1945)))),bind(X_1939,$fot(X_1947))]]) ).
cnf(refute_0_119,plain,
is_a_theorem(implies(implies(implies(implies(X_1947,X_1945),X_1945),X_1944),implies(implies(not(X_1945),X_1947),X_1944))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(implies(X_1947,X_1945),X_1945)),implies(implies(X_1947,X_1945),X_1945)),X_1944),implies(implies(not(X_1945),X_1947),X_1944))) )],[refute_0_118,refute_0_111]) ).
cnf(refute_0_120,plain,
is_a_theorem(implies(implies(implies(implies(X_3223,X_3222),X_3222),X_3221),implies(implies(not(X_3222),X_3223),X_3221))),
inference(subst,[],[refute_0_119:[bind(X_1944,$fot(X_3221)),bind(X_1945,$fot(X_3222)),bind(X_1947,$fot(X_3223))]]) ).
cnf(refute_0_121,plain,
is_a_theorem(implies(not(implies(implies(implies(implies(X_3223,X_3222),X_3222),X_3221),implies(implies(not(X_3222),X_3223),X_3221))),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_3223,X_3222),X_3222),X_3221),implies(implies(not(X_3222),X_3223),X_3221))) )],[refute_0_120,refute_0_110]) ).
cnf(refute_0_122,plain,
is_a_theorem(implies(not(implies(implies(implies(implies(X_3223,X_6864),X_6864),implies(X_6862,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864)))),implies(implies(implies(implies(X_3223,X_6864),X_6864),implies(X_6862,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864))))),
inference(subst,[],[refute_0_121:[bind(Y,$fot(implies(implies(implies(implies(X_3223,X_6864),X_6864),implies(X_6862,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864))))),bind(X_3221,$fot(implies(X_6862,X_6864))),bind(X_3222,$fot(X_6864))]]) ).
cnf(refute_0_123,plain,
( ~ is_a_theorem(implies(implies(not(implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(X_1279,X_1280),X_1282)))
| ~ is_a_theorem(implies(not(implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)))
| is_a_theorem(implies(implies(X_1279,X_1280),X_1282)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)))),bind(Y,$fot(implies(implies(X_1279,X_1280),X_1282)))]]) ).
cnf(refute_0_124,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82),implies(implies(X_79,X_80),X_82)))
| is_a_theorem(implies(implies(not(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82)),implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82)),implies(implies(X_79,X_80),X_82))) ),
inference(subst,[],[refute_0_8:[bind(X_21,$fot(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82))),bind(X_22,$fot(implies(implies(X_79,X_80),X_82)))]]) ).
cnf(refute_0_125,plain,
is_a_theorem(implies(implies(not(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82)),implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82)),implies(implies(X_79,X_80),X_82))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_80,X_81),implies(X_79,X_81)),X_82),implies(implies(X_79,X_80),X_82))) )],[refute_0_22,refute_0_124]) ).
cnf(refute_0_126,plain,
is_a_theorem(implies(implies(not(implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(X_1279,X_1280),X_1282))),
inference(subst,[],[refute_0_125:[bind(X_79,$fot(X_1279)),bind(X_80,$fot(X_1280)),bind(X_81,$fot(X_1281)),bind(X_82,$fot(X_1282))]]) ).
cnf(refute_0_127,plain,
( ~ is_a_theorem(implies(not(implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)))
| is_a_theorem(implies(implies(X_1279,X_1280),X_1282)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(implies(X_1280,X_1281),implies(X_1279,X_1281)),X_1282)),implies(implies(X_1279,X_1280),X_1282))) )],[refute_0_126,refute_0_123]) ).
cnf(refute_0_128,plain,
( ~ is_a_theorem(implies(not(implies(implies(implies(implies(X_3223,X_6864),X_6864),implies(X_6862,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864)))),implies(implies(implies(implies(X_3223,X_6864),X_6864),implies(X_6862,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864)))))
| is_a_theorem(implies(implies(X_6862,implies(X_3223,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864)))) ),
inference(subst,[],[refute_0_127:[bind(X_1279,$fot(X_6862)),bind(X_1280,$fot(implies(X_3223,X_6864))),bind(X_1281,$fot(X_6864)),bind(X_1282,$fot(implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864))))]]) ).
cnf(refute_0_129,plain,
is_a_theorem(implies(implies(X_6862,implies(X_3223,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864)))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(implies(implies(X_3223,X_6864),X_6864),implies(X_6862,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864)))),implies(implies(implies(implies(X_3223,X_6864),X_6864),implies(X_6862,X_6864)),implies(implies(not(X_6864),X_3223),implies(X_6862,X_6864))))) )],[refute_0_122,refute_0_128]) ).
cnf(refute_0_130,plain,
is_a_theorem(implies(implies(implies(X_80,X_6889),implies(X_6887,X_6889)),implies(implies(not(X_6889),X_6887),implies(implies(X_80,X_6889),X_6889)))),
inference(subst,[],[refute_0_129:[bind(X_3223,$fot(X_6887)),bind(X_6862,$fot(implies(X_80,X_6889))),bind(X_6864,$fot(X_6889))]]) ).
cnf(refute_0_131,plain,
is_a_theorem(implies(implies(X_6887,X_80),implies(implies(not(X_6889),X_6887),implies(implies(X_80,X_6889),X_6889)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_80,X_6889),implies(X_6887,X_6889)),implies(implies(not(X_6889),X_6887),implies(implies(X_80,X_6889),X_6889)))) )],[refute_0_130,refute_0_109]) ).
cnf(refute_0_132,plain,
is_a_theorem(implies(implies(X_6989,X_6991),implies(implies(not(X_6990),X_6989),implies(implies(X_6991,X_6990),X_6990)))),
inference(subst,[],[refute_0_131:[bind(X_6887,$fot(X_6989)),bind(X_6889,$fot(X_6990)),bind(X_80,$fot(X_6991))]]) ).
cnf(refute_0_133,plain,
is_a_theorem(implies(implies(not(implies(X_6989,X_6991)),implies(X_6989,X_6991)),implies(implies(not(X_6990),X_6989),implies(implies(X_6991,X_6990),X_6990)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_6989,X_6991),implies(implies(not(X_6990),X_6989),implies(implies(X_6991,X_6990),X_6990)))) )],[refute_0_132,refute_0_108]) ).
cnf(refute_0_134,plain,
is_a_theorem(implies(implies(not(implies(implies(not(X_7158),X_7158),X_7158)),implies(implies(not(X_7158),X_7158),X_7158)),implies(implies(not(X_7157),implies(not(X_7158),X_7158)),implies(implies(X_7158,X_7157),X_7157)))),
inference(subst,[],[refute_0_133:[bind(X_6989,$fot(implies(not(X_7158),X_7158))),bind(X_6990,$fot(X_7157)),bind(X_6991,$fot(X_7158))]]) ).
cnf(refute_0_135,plain,
is_a_theorem(implies(X_285,implies(implies(not(X_7157),implies(not(X_7158),X_7158)),implies(implies(X_7158,X_7157),X_7157)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(implies(not(X_7158),X_7158),X_7158)),implies(implies(not(X_7158),X_7158),X_7158)),implies(implies(not(X_7157),implies(not(X_7158),X_7158)),implies(implies(X_7158,X_7157),X_7157)))) )],[refute_0_134,refute_0_107]) ).
cnf(refute_0_136,plain,
is_a_theorem(implies(implies(implies(not(not(not(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))),not(not(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))),X_3588),implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279)))),
inference(subst,[],[refute_0_135:[bind(X_285,$fot(implies(implies(not(not(not(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))),not(not(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))),X_3588))),bind(X_7157,$fot(X_7279)),bind(X_7158,$fot(X_7280))]]) ).
cnf(refute_0_137,plain,
is_a_theorem(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(not(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))),not(not(implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279))))),X_3588),implies(implies(not(X_7279),implies(not(X_7280),X_7280)),implies(implies(X_7280,X_7279),X_7279)))) )],[refute_0_136,refute_0_106]) ).
cnf(refute_0_138,plain,
is_a_theorem(implies(implies(not(X_7281),implies(not(X_7282),X_7282)),implies(implies(X_7282,X_7281),X_7281))),
inference(subst,[],[refute_0_137:[bind(X_7279,$fot(X_7281)),bind(X_7280,$fot(X_7282))]]) ).
cnf(refute_0_139,plain,
is_a_theorem(implies(X_7282,implies(implies(X_7282,X_7281),X_7281))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_7281),implies(not(X_7282),X_7282)),implies(implies(X_7282,X_7281),X_7281))) )],[refute_0_138,refute_0_70]) ).
cnf(refute_0_140,plain,
is_a_theorem(implies(X_7284,implies(implies(X_7284,X_7283),X_7283))),
inference(subst,[],[refute_0_139:[bind(X_7281,$fot(X_7283)),bind(X_7282,$fot(X_7284))]]) ).
cnf(refute_0_141,plain,
( ~ is_a_theorem(X_7284)
| is_a_theorem(implies(implies(X_7284,X_7283),X_7283)) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_7284,implies(implies(X_7284,X_7283),X_7283))) )],[refute_0_140,refute_0_57]) ).
cnf(refute_0_142,plain,
( ~ is_a_theorem(implies(not(not(X_7677)),X_7677))
| is_a_theorem(implies(implies(implies(not(not(X_7677)),X_7677),X_7283),X_7283)) ),
inference(subst,[],[refute_0_141:[bind(X_7284,$fot(implies(not(not(X_7677)),X_7677)))]]) ).
cnf(refute_0_143,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(not(not(X_7676))),not(not(X_7676))),X_7676)),implies(implies(not(not(not(X_7676))),not(not(X_7676))),X_7676)))
| is_a_theorem(implies(not(not(X_7676)),X_7676)) ),
inference(subst,[],[refute_0_16:[bind(X_101,$fot(not(not(X_7676)))),bind(X_102,$fot(not(not(X_7676)))),bind(X_103,$fot(X_7676))]]) ).
cnf(refute_0_144,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_6055),X_6055),X_6054),implies(implies(not(not(not(X_6055))),not(not(X_6055))),X_6054)))
| is_a_theorem(implies(implies(X_6055,X_6054),implies(implies(not(not(not(X_6055))),not(not(X_6055))),X_6054))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(implies(not(not(not(X_6055))),not(not(X_6055))),X_6054))),bind(X_33,$fot(X_6055)),bind(X_34,$fot(X_6054))]]) ).
cnf(refute_0_145,plain,
( ~ is_a_theorem(implies(implies(not(not(X_6044)),not(X_6044)),implies(X_6044,X_6043)))
| is_a_theorem(implies(implies(implies(X_6044,X_6043),Z),implies(implies(not(not(X_6044)),not(X_6044)),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(not(not(X_6044)),not(X_6044)))),bind(Y,$fot(implies(X_6044,X_6043)))]]) ).
cnf(refute_0_146,plain,
( ~ is_a_theorem(implies(implies(not(implies(not(not(X_6042)),not(X_6042))),X_6041),implies(X_6042,X_6041)))
| is_a_theorem(implies(implies(not(not(X_6042)),not(X_6042)),implies(X_6042,X_6041))) ),
inference(subst,[],[refute_0_36:[bind(X_26,$fot(X_6041)),bind(X_27,$fot(implies(not(not(X_6042)),not(X_6042)))),bind(X_28,$fot(implies(X_6042,X_6041)))]]) ).
cnf(refute_0_147,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(implies(not(not(X_6039)),not(X_6039)))),not(implies(not(not(X_6039)),not(X_6039)))),X_6038),implies(X_6039,X_6038)))
| is_a_theorem(implies(implies(not(implies(not(not(X_6039)),not(X_6039))),X_6038),implies(X_6039,X_6038))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(X_6039,X_6038))),bind(X_33,$fot(not(implies(not(not(X_6039)),not(X_6039))))),bind(X_34,$fot(X_6038))]]) ).
cnf(refute_0_148,plain,
( ~ is_a_theorem(implies(X_4051,implies(not(not(implies(not(not(X_4051)),not(X_4051)))),X_4052)))
| is_a_theorem(implies(implies(implies(not(not(implies(not(not(X_4051)),not(X_4051)))),X_4052),Z),implies(X_4051,Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_4051)),bind(Y,$fot(implies(not(not(implies(not(not(X_4051)),not(X_4051)))),X_4052)))]]) ).
cnf(refute_0_149,plain,
( ~ is_a_theorem(implies(implies(not(X_27),X_3964),implies(not(not(implies(not(not(X_27)),not(X_27)))),X_3964)))
| is_a_theorem(implies(X_27,implies(not(not(implies(not(not(X_27)),not(X_27)))),X_3964))) ),
inference(subst,[],[refute_0_36:[bind(X_26,$fot(X_3964)),bind(X_28,$fot(implies(not(not(implies(not(not(X_27)),not(X_27)))),X_3964)))]]) ).
cnf(refute_0_150,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_3950),X_3950),X_3952),implies(not(not(implies(not(X_3950),X_3950))),X_3952)))
| is_a_theorem(implies(implies(X_3950,X_3952),implies(not(not(implies(not(X_3950),X_3950))),X_3952))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(not(not(implies(not(X_3950),X_3950))),X_3952))),bind(X_33,$fot(X_3950)),bind(X_34,$fot(X_3952))]]) ).
cnf(refute_0_151,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_94,X_95)),implies(X_94,X_95)),implies(implies(X_95,X_96),implies(X_94,X_96))))
| ~ is_a_theorem(implies(not(implies(X_94,X_95)),implies(X_94,X_95)))
| is_a_theorem(implies(implies(X_95,X_96),implies(X_94,X_96))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(implies(X_94,X_95)),implies(X_94,X_95)))),bind(Y,$fot(implies(implies(X_95,X_96),implies(X_94,X_96))))]]) ).
cnf(refute_0_152,plain,
( ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| is_a_theorem(implies(implies(not(implies(X,Y)),implies(X,Y)),implies(implies(Y,Z),implies(X,Z)))) ),
inference(subst,[],[refute_0_8:[bind(X_21,$fot(implies(X,Y))),bind(X_22,$fot(implies(implies(Y,Z),implies(X,Z))))]]) ).
cnf(refute_0_153,plain,
is_a_theorem(implies(implies(not(implies(X,Y)),implies(X,Y)),implies(implies(Y,Z),implies(X,Z)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) )],[cn_1,refute_0_152]) ).
cnf(refute_0_154,plain,
is_a_theorem(implies(implies(not(implies(X_94,X_95)),implies(X_94,X_95)),implies(implies(X_95,X_96),implies(X_94,X_96)))),
inference(subst,[],[refute_0_153:[bind(X,$fot(X_94)),bind(Y,$fot(X_95)),bind(Z,$fot(X_96))]]) ).
cnf(refute_0_155,plain,
( ~ is_a_theorem(implies(not(implies(X_94,X_95)),implies(X_94,X_95)))
| is_a_theorem(implies(implies(X_95,X_96),implies(X_94,X_96))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_94,X_95)),implies(X_94,X_95)),implies(implies(X_95,X_96),implies(X_94,X_96)))) )],[refute_0_154,refute_0_151]) ).
cnf(refute_0_156,plain,
( ~ is_a_theorem(implies(not(implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947))),implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947))))
| is_a_theorem(implies(implies(implies(X_3948,X_3947),X_96),implies(not(not(implies(X_3948,X_3947))),X_96))) ),
inference(subst,[],[refute_0_155:[bind(X_94,$fot(not(not(implies(X_3948,X_3947))))),bind(X_95,$fot(implies(X_3948,X_3947)))]]) ).
cnf(refute_0_157,plain,
( ~ is_a_theorem(X_1638)
| ~ is_a_theorem(implies(X_1638,implies(X_1639,implies(X_1640,X_1638))))
| is_a_theorem(implies(X_1639,implies(X_1640,X_1638))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_1638)),bind(Y,$fot(implies(X_1639,implies(X_1640,X_1638))))]]) ).
cnf(refute_0_158,plain,
( ~ is_a_theorem(implies(implies(X_1637,implies(not(X_1635),X_1635)),implies(X_1636,implies(X_1637,X_1635))))
| is_a_theorem(implies(X_1635,implies(X_1636,implies(X_1637,X_1635)))) ),
inference(subst,[],[refute_0_69:[bind(X_271,$fot(implies(X_1636,implies(X_1637,X_1635)))),bind(X_272,$fot(X_1635)),bind(X_273,$fot(X_1637)),bind(X_274,$fot(X_1635))]]) ).
cnf(refute_0_159,plain,
is_a_theorem(implies(X_1635,implies(X_1636,implies(X_1637,X_1635)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1637,implies(not(X_1635),X_1635)),implies(X_1636,implies(X_1637,X_1635)))) )],[refute_0_51,refute_0_158]) ).
cnf(refute_0_160,plain,
is_a_theorem(implies(X_1638,implies(X_1639,implies(X_1640,X_1638)))),
inference(subst,[],[refute_0_159:[bind(X_1635,$fot(X_1638)),bind(X_1636,$fot(X_1639)),bind(X_1637,$fot(X_1640))]]) ).
cnf(refute_0_161,plain,
( ~ is_a_theorem(X_1638)
| is_a_theorem(implies(X_1639,implies(X_1640,X_1638))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_1638,implies(X_1639,implies(X_1640,X_1638)))) )],[refute_0_160,refute_0_157]) ).
cnf(refute_0_162,plain,
( ~ is_a_theorem(implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705)))
| is_a_theorem(implies(X_1639,implies(X_1640,implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705))))) ),
inference(subst,[],[refute_0_161:[bind(X_1638,$fot(implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705))))]]) ).
cnf(refute_0_163,plain,
( ~ is_a_theorem(implies(implies(X_3702,implies(not(not(not(implies(X_3702,X_3701)))),not(not(implies(X_3702,X_3701))))),implies(X_3702,X_3701)))
| is_a_theorem(implies(not(not(implies(X_3702,X_3701))),implies(X_3702,X_3701))) ),
inference(subst,[],[refute_0_69:[bind(X_271,$fot(implies(X_3702,X_3701))),bind(X_272,$fot(not(not(implies(X_3702,X_3701))))),bind(X_273,$fot(X_3702)),bind(X_274,$fot(not(not(implies(X_3702,X_3701)))))]]) ).
cnf(refute_0_164,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(not(not(implies(X_79,X_3588)))),not(not(implies(X_79,X_3588)))),X_3588),implies(X_79,X_3588)),implies(X_79,X_3588)))
| is_a_theorem(implies(implies(X_79,implies(not(not(not(implies(X_79,X_3588)))),not(not(implies(X_79,X_3588))))),implies(X_79,X_3588))) ),
inference(subst,[],[refute_0_23:[bind(X_80,$fot(implies(not(not(not(implies(X_79,X_3588)))),not(not(implies(X_79,X_3588)))))),bind(X_81,$fot(X_3588)),bind(X_82,$fot(implies(X_79,X_3588)))]]) ).
cnf(refute_0_165,plain,
is_a_theorem(implies(implies(implies(implies(not(not(not(implies(X_79,X_3588)))),not(not(implies(X_79,X_3588)))),X_3588),implies(X_79,X_3588)),implies(X_79,X_3588))),
inference(subst,[],[refute_0_103:[bind(X_3585,$fot(implies(X_79,X_3588))),bind(X_3586,$fot(X_3588))]]) ).
cnf(refute_0_166,plain,
is_a_theorem(implies(implies(X_79,implies(not(not(not(implies(X_79,X_3588)))),not(not(implies(X_79,X_3588))))),implies(X_79,X_3588))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(not(not(implies(X_79,X_3588)))),not(not(implies(X_79,X_3588)))),X_3588),implies(X_79,X_3588)),implies(X_79,X_3588))) )],[refute_0_165,refute_0_164]) ).
cnf(refute_0_167,plain,
is_a_theorem(implies(implies(X_3702,implies(not(not(not(implies(X_3702,X_3701)))),not(not(implies(X_3702,X_3701))))),implies(X_3702,X_3701))),
inference(subst,[],[refute_0_166:[bind(X_3588,$fot(X_3701)),bind(X_79,$fot(X_3702))]]) ).
cnf(refute_0_168,plain,
is_a_theorem(implies(not(not(implies(X_3702,X_3701))),implies(X_3702,X_3701))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_3702,implies(not(not(not(implies(X_3702,X_3701)))),not(not(implies(X_3702,X_3701))))),implies(X_3702,X_3701))) )],[refute_0_167,refute_0_163]) ).
cnf(refute_0_169,plain,
is_a_theorem(implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705))),
inference(subst,[],[refute_0_168:[bind(X_3701,$fot(X_3705)),bind(X_3702,$fot(X_3706))]]) ).
cnf(refute_0_170,plain,
is_a_theorem(implies(X_1639,implies(X_1640,implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705))))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705))) )],[refute_0_169,refute_0_162]) ).
cnf(refute_0_171,plain,
is_a_theorem(implies(not(implies(implies(not(X_3945),X_3944),implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705)))),implies(implies(not(X_3945),X_3944),implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705))))),
inference(subst,[],[refute_0_170:[bind(X_1639,$fot(not(implies(implies(not(X_3945),X_3944),implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705)))))),bind(X_1640,$fot(implies(not(X_3945),X_3944)))]]) ).
cnf(refute_0_172,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(X_3945),X_3944),implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705)))),implies(implies(not(X_3945),X_3944),implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705)))))
| is_a_theorem(implies(X_3945,implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705)))) ),
inference(subst,[],[refute_0_16:[bind(X_101,$fot(X_3944)),bind(X_102,$fot(X_3945)),bind(X_103,$fot(implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705))))]]) ).
cnf(refute_0_173,plain,
is_a_theorem(implies(X_3945,implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705)))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(X_3945),X_3944),implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705)))),implies(implies(not(X_3945),X_3944),implies(not(not(implies(X_3706,X_3705))),implies(X_3706,X_3705))))) )],[refute_0_171,refute_0_172]) ).
cnf(refute_0_174,plain,
is_a_theorem(implies(not(implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947))),implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947)))),
inference(subst,[],[refute_0_173:[bind(X_3705,$fot(X_3947)),bind(X_3706,$fot(X_3948)),bind(X_3945,$fot(not(implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947)))))]]) ).
cnf(refute_0_175,plain,
is_a_theorem(implies(implies(implies(X_3948,X_3947),X_96),implies(not(not(implies(X_3948,X_3947))),X_96))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947))),implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947)))) )],[refute_0_174,refute_0_156]) ).
cnf(refute_0_176,plain,
is_a_theorem(implies(implies(implies(not(X_3950),X_3950),X_3952),implies(not(not(implies(not(X_3950),X_3950))),X_3952))),
inference(subst,[],[refute_0_175:[bind(X_3947,$fot(X_3950)),bind(X_3948,$fot(not(X_3950))),bind(X_96,$fot(X_3952))]]) ).
cnf(refute_0_177,plain,
is_a_theorem(implies(implies(X_3950,X_3952),implies(not(not(implies(not(X_3950),X_3950))),X_3952))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_3950),X_3950),X_3952),implies(not(not(implies(not(X_3950),X_3950))),X_3952))) )],[refute_0_176,refute_0_150]) ).
cnf(refute_0_178,plain,
is_a_theorem(implies(implies(not(X_27),X_3964),implies(not(not(implies(not(not(X_27)),not(X_27)))),X_3964))),
inference(subst,[],[refute_0_177:[bind(X_3950,$fot(not(X_27))),bind(X_3952,$fot(X_3964))]]) ).
cnf(refute_0_179,plain,
is_a_theorem(implies(X_27,implies(not(not(implies(not(not(X_27)),not(X_27)))),X_3964))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_27),X_3964),implies(not(not(implies(not(not(X_27)),not(X_27)))),X_3964))) )],[refute_0_178,refute_0_149]) ).
cnf(refute_0_180,plain,
is_a_theorem(implies(X_4051,implies(not(not(implies(not(not(X_4051)),not(X_4051)))),X_4052))),
inference(subst,[],[refute_0_179:[bind(X_27,$fot(X_4051)),bind(X_3964,$fot(X_4052))]]) ).
cnf(refute_0_181,plain,
is_a_theorem(implies(implies(implies(not(not(implies(not(not(X_4051)),not(X_4051)))),X_4052),Z),implies(X_4051,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_4051,implies(not(not(implies(not(not(X_4051)),not(X_4051)))),X_4052))) )],[refute_0_180,refute_0_148]) ).
cnf(refute_0_182,plain,
is_a_theorem(implies(implies(implies(not(not(implies(not(not(X_6039)),not(X_6039)))),not(implies(not(not(X_6039)),not(X_6039)))),X_6038),implies(X_6039,X_6038))),
inference(subst,[],[refute_0_181:[bind(Z,$fot(X_6038)),bind(X_4051,$fot(X_6039)),bind(X_4052,$fot(not(implies(not(not(X_6039)),not(X_6039)))))]]) ).
cnf(refute_0_183,plain,
is_a_theorem(implies(implies(not(implies(not(not(X_6039)),not(X_6039))),X_6038),implies(X_6039,X_6038))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(implies(not(not(X_6039)),not(X_6039)))),not(implies(not(not(X_6039)),not(X_6039)))),X_6038),implies(X_6039,X_6038))) )],[refute_0_182,refute_0_147]) ).
cnf(refute_0_184,plain,
is_a_theorem(implies(implies(not(implies(not(not(X_6042)),not(X_6042))),X_6041),implies(X_6042,X_6041))),
inference(subst,[],[refute_0_183:[bind(X_6038,$fot(X_6041)),bind(X_6039,$fot(X_6042))]]) ).
cnf(refute_0_185,plain,
is_a_theorem(implies(implies(not(not(X_6042)),not(X_6042)),implies(X_6042,X_6041))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(not(not(X_6042)),not(X_6042))),X_6041),implies(X_6042,X_6041))) )],[refute_0_184,refute_0_146]) ).
cnf(refute_0_186,plain,
is_a_theorem(implies(implies(not(not(X_6044)),not(X_6044)),implies(X_6044,X_6043))),
inference(subst,[],[refute_0_185:[bind(X_6041,$fot(X_6043)),bind(X_6042,$fot(X_6044))]]) ).
cnf(refute_0_187,plain,
is_a_theorem(implies(implies(implies(X_6044,X_6043),Z),implies(implies(not(not(X_6044)),not(X_6044)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(X_6044)),not(X_6044)),implies(X_6044,X_6043))) )],[refute_0_186,refute_0_145]) ).
cnf(refute_0_188,plain,
is_a_theorem(implies(implies(implies(not(X_6055),X_6055),X_6054),implies(implies(not(not(not(X_6055))),not(not(X_6055))),X_6054))),
inference(subst,[],[refute_0_187:[bind(Z,$fot(X_6054)),bind(X_6043,$fot(X_6055)),bind(X_6044,$fot(not(X_6055)))]]) ).
cnf(refute_0_189,plain,
is_a_theorem(implies(implies(X_6055,X_6054),implies(implies(not(not(not(X_6055))),not(not(X_6055))),X_6054))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_6055),X_6055),X_6054),implies(implies(not(not(not(X_6055))),not(not(X_6055))),X_6054))) )],[refute_0_188,refute_0_144]) ).
cnf(refute_0_190,plain,
is_a_theorem(implies(implies(X_7601,X_7601),implies(implies(not(not(not(X_7601))),not(not(X_7601))),X_7601))),
inference(subst,[],[refute_0_189:[bind(X_6054,$fot(X_7601)),bind(X_6055,$fot(X_7601))]]) ).
cnf(refute_0_191,plain,
( ~ is_a_theorem(implies(implies(X_1586,X_1586),X_1584))
| ~ is_a_theorem(implies(implies(implies(X_1586,X_1586),X_1584),implies(X_1585,X_1584)))
| is_a_theorem(implies(X_1585,X_1584)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_1586,X_1586),X_1584))),bind(Y,$fot(implies(X_1585,X_1584)))]]) ).
cnf(refute_0_192,plain,
( ~ is_a_theorem(implies(X_300,implies(not(implies(X_302,X_302)),X_301)))
| is_a_theorem(implies(implies(implies(not(implies(X_302,X_302)),X_301),Z),implies(X_300,Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_300)),bind(Y,$fot(implies(not(implies(X_302,X_302)),X_301)))]]) ).
cnf(refute_0_193,plain,
( ~ is_a_theorem(implies(implies(not(X_27),X_297),implies(not(implies(X_299,X_299)),X_297)))
| is_a_theorem(implies(X_27,implies(not(implies(X_299,X_299)),X_297))) ),
inference(subst,[],[refute_0_36:[bind(X_26,$fot(X_297)),bind(X_28,$fot(implies(not(implies(X_299,X_299)),X_297)))]]) ).
cnf(refute_0_194,plain,
( ~ is_a_theorem(implies(not(implies(X_239,X_239)),X_238))
| is_a_theorem(implies(implies(X_238,Z),implies(not(implies(X_239,X_239)),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(not(implies(X_239,X_239)))),bind(Y,$fot(X_238))]]) ).
cnf(refute_0_195,plain,
( ~ is_a_theorem(implies(X_237,X_237))
| is_a_theorem(implies(not(implies(X_237,X_237)),Y)) ),
inference(subst,[],[refute_0_28:[bind(X_6,$fot(implies(X_237,X_237)))]]) ).
cnf(refute_0_196,plain,
is_a_theorem(implies(implies(not(X_236),X_236),X_236)),
inference(subst,[],[cn_2:[bind(X,$fot(X_236))]]) ).
cnf(refute_0_197,plain,
( ~ is_a_theorem(implies(implies(not(X_236),X_236),X_236))
| is_a_theorem(implies(X_236,X_236)) ),
inference(subst,[],[refute_0_36:[bind(X_26,$fot(X_236)),bind(X_27,$fot(X_236)),bind(X_28,$fot(X_236))]]) ).
cnf(refute_0_198,plain,
is_a_theorem(implies(X_236,X_236)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_236),X_236),X_236)) )],[refute_0_196,refute_0_197]) ).
cnf(refute_0_199,plain,
is_a_theorem(implies(X_237,X_237)),
inference(subst,[],[refute_0_198:[bind(X_236,$fot(X_237))]]) ).
cnf(refute_0_200,plain,
is_a_theorem(implies(not(implies(X_237,X_237)),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(X_237,X_237)) )],[refute_0_199,refute_0_195]) ).
cnf(refute_0_201,plain,
is_a_theorem(implies(not(implies(X_239,X_239)),X_238)),
inference(subst,[],[refute_0_200:[bind(Y,$fot(X_238)),bind(X_237,$fot(X_239))]]) ).
cnf(refute_0_202,plain,
is_a_theorem(implies(implies(X_238,Z),implies(not(implies(X_239,X_239)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_239,X_239)),X_238)) )],[refute_0_201,refute_0_194]) ).
cnf(refute_0_203,plain,
is_a_theorem(implies(implies(not(X_27),X_297),implies(not(implies(X_299,X_299)),X_297))),
inference(subst,[],[refute_0_202:[bind(Z,$fot(X_297)),bind(X_238,$fot(not(X_27))),bind(X_239,$fot(X_299))]]) ).
cnf(refute_0_204,plain,
is_a_theorem(implies(X_27,implies(not(implies(X_299,X_299)),X_297))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_27),X_297),implies(not(implies(X_299,X_299)),X_297))) )],[refute_0_203,refute_0_193]) ).
cnf(refute_0_205,plain,
is_a_theorem(implies(X_300,implies(not(implies(X_302,X_302)),X_301))),
inference(subst,[],[refute_0_204:[bind(X_27,$fot(X_300)),bind(X_297,$fot(X_301)),bind(X_299,$fot(X_302))]]) ).
cnf(refute_0_206,plain,
is_a_theorem(implies(implies(implies(not(implies(X_302,X_302)),X_301),Z),implies(X_300,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_300,implies(not(implies(X_302,X_302)),X_301))) )],[refute_0_205,refute_0_192]) ).
cnf(refute_0_207,plain,
is_a_theorem(implies(implies(implies(not(implies(X_302,X_302)),implies(X_302,X_302)),X_1583),implies(X_300,X_1583))),
inference(subst,[],[refute_0_206:[bind(Z,$fot(X_1583)),bind(X_301,$fot(implies(X_302,X_302)))]]) ).
cnf(refute_0_208,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_302,X_302)),implies(X_302,X_302)),X_1583),implies(X_300,X_1583)))
| is_a_theorem(implies(implies(implies(X_302,X_302),X_1583),implies(X_300,X_1583))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(X_300,X_1583))),bind(X_33,$fot(implies(X_302,X_302))),bind(X_34,$fot(X_1583))]]) ).
cnf(refute_0_209,plain,
is_a_theorem(implies(implies(implies(X_302,X_302),X_1583),implies(X_300,X_1583))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_302,X_302)),implies(X_302,X_302)),X_1583),implies(X_300,X_1583))) )],[refute_0_207,refute_0_208]) ).
cnf(refute_0_210,plain,
is_a_theorem(implies(implies(implies(X_1586,X_1586),X_1584),implies(X_1585,X_1584))),
inference(subst,[],[refute_0_209:[bind(X_1583,$fot(X_1584)),bind(X_300,$fot(X_1585)),bind(X_302,$fot(X_1586))]]) ).
cnf(refute_0_211,plain,
( ~ is_a_theorem(implies(implies(X_1586,X_1586),X_1584))
| is_a_theorem(implies(X_1585,X_1584)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1586,X_1586),X_1584),implies(X_1585,X_1584))) )],[refute_0_210,refute_0_191]) ).
cnf(refute_0_212,plain,
( ~ is_a_theorem(implies(implies(X_7601,X_7601),implies(implies(not(not(not(X_7601))),not(not(X_7601))),X_7601)))
| is_a_theorem(implies(X_7600,implies(implies(not(not(not(X_7601))),not(not(X_7601))),X_7601))) ),
inference(subst,[],[refute_0_211:[bind(X_1584,$fot(implies(implies(not(not(not(X_7601))),not(not(X_7601))),X_7601))),bind(X_1585,$fot(X_7600)),bind(X_1586,$fot(X_7601))]]) ).
cnf(refute_0_213,plain,
is_a_theorem(implies(X_7600,implies(implies(not(not(not(X_7601))),not(not(X_7601))),X_7601))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_7601,X_7601),implies(implies(not(not(not(X_7601))),not(not(X_7601))),X_7601))) )],[refute_0_190,refute_0_212]) ).
cnf(refute_0_214,plain,
is_a_theorem(implies(not(implies(implies(not(not(not(X_7676))),not(not(X_7676))),X_7676)),implies(implies(not(not(not(X_7676))),not(not(X_7676))),X_7676))),
inference(subst,[],[refute_0_213:[bind(X_7600,$fot(not(implies(implies(not(not(not(X_7676))),not(not(X_7676))),X_7676)))),bind(X_7601,$fot(X_7676))]]) ).
cnf(refute_0_215,plain,
is_a_theorem(implies(not(not(X_7676)),X_7676)),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(not(not(X_7676))),not(not(X_7676))),X_7676)),implies(implies(not(not(not(X_7676))),not(not(X_7676))),X_7676))) )],[refute_0_214,refute_0_143]) ).
cnf(refute_0_216,plain,
is_a_theorem(implies(not(not(X_7677)),X_7677)),
inference(subst,[],[refute_0_215:[bind(X_7676,$fot(X_7677))]]) ).
cnf(refute_0_217,plain,
is_a_theorem(implies(implies(implies(not(not(X_7677)),X_7677),X_7283),X_7283)),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(X_7677)),X_7677)) )],[refute_0_216,refute_0_142]) ).
cnf(refute_0_218,plain,
is_a_theorem(implies(implies(implies(not(not(X_7702)),X_7702),X_7701),X_7701)),
inference(subst,[],[refute_0_217:[bind(X_7283,$fot(X_7701)),bind(X_7677,$fot(X_7702))]]) ).
cnf(refute_0_219,plain,
( ~ is_a_theorem(implies(implies(not(not(X_7702)),X_7702),X_7701))
| is_a_theorem(X_7701) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(X_7702)),X_7702),X_7701),X_7701)) )],[refute_0_218,refute_0_56]) ).
cnf(refute_0_220,plain,
( ~ is_a_theorem(implies(implies(not(not(not(implies(X_22842,X_22843)))),not(implies(X_22842,X_22843))),implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),X_22841))))
| is_a_theorem(implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),X_22841))) ),
inference(subst,[],[refute_0_219:[bind(X_7701,$fot(implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),X_22841)))),bind(X_7702,$fot(not(implies(X_22842,X_22843))))]]) ).
cnf(refute_0_221,plain,
( ~ is_a_theorem(implies(implies(X_1124,implies(X_1122,X_1123)),X_1121))
| ~ is_a_theorem(implies(implies(implies(X_1124,implies(X_1122,X_1123)),X_1121),implies(implies(X_1122,not(X_1124)),X_1121)))
| is_a_theorem(implies(implies(X_1122,not(X_1124)),X_1121)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_1124,implies(X_1122,X_1123)),X_1121))),bind(Y,$fot(implies(implies(X_1122,not(X_1124)),X_1121)))]]) ).
cnf(refute_0_222,plain,
( ~ is_a_theorem(implies(implies(X_168,not(X_170)),implies(X_170,implies(X_168,X_169))))
| is_a_theorem(implies(implies(implies(X_170,implies(X_168,X_169)),Z),implies(implies(X_168,not(X_170)),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(X_168,not(X_170)))),bind(Y,$fot(implies(X_170,implies(X_168,X_169))))]]) ).
cnf(refute_0_223,plain,
is_a_theorem(implies(implies(X_168,not(X_170)),implies(X_170,implies(X_168,X_169)))),
inference(subst,[],[refute_0_62:[bind(X_164,$fot(X_168)),bind(X_166,$fot(X_169)),bind(X_18,$fot(X_170))]]) ).
cnf(refute_0_224,plain,
is_a_theorem(implies(implies(implies(X_170,implies(X_168,X_169)),Z),implies(implies(X_168,not(X_170)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_168,not(X_170)),implies(X_170,implies(X_168,X_169)))) )],[refute_0_223,refute_0_222]) ).
cnf(refute_0_225,plain,
is_a_theorem(implies(implies(implies(X_1124,implies(X_1122,X_1123)),X_1121),implies(implies(X_1122,not(X_1124)),X_1121))),
inference(subst,[],[refute_0_224:[bind(Z,$fot(X_1121)),bind(X_168,$fot(X_1122)),bind(X_169,$fot(X_1123)),bind(X_170,$fot(X_1124))]]) ).
cnf(refute_0_226,plain,
( ~ is_a_theorem(implies(implies(X_1124,implies(X_1122,X_1123)),X_1121))
| is_a_theorem(implies(implies(X_1122,not(X_1124)),X_1121)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1124,implies(X_1122,X_1123)),X_1121),implies(implies(X_1122,not(X_1124)),X_1121))) )],[refute_0_225,refute_0_221]) ).
cnf(refute_0_227,plain,
( ~ is_a_theorem(implies(implies(implies(X_20776,X_20777),implies(X_1122,X_1123)),implies(implies(not(not(X_20776)),X_20777),implies(X_1122,X_1123))))
| is_a_theorem(implies(implies(X_1122,not(implies(X_20776,X_20777))),implies(implies(not(not(X_20776)),X_20777),implies(X_1122,X_1123)))) ),
inference(subst,[],[refute_0_226:[bind(X_1121,$fot(implies(implies(not(not(X_20776)),X_20777),implies(X_1122,X_1123)))),bind(X_1124,$fot(implies(X_20776,X_20777)))]]) ).
cnf(refute_0_228,plain,
( ~ is_a_theorem(implies(not(implies(implies(not(not(X_20655)),X_20656),implies(X_20655,X_20656))),implies(implies(not(not(X_20655)),X_20656),implies(X_20655,X_20656))))
| is_a_theorem(implies(implies(implies(X_20655,X_20656),X_96),implies(implies(not(not(X_20655)),X_20656),X_96))) ),
inference(subst,[],[refute_0_155:[bind(X_94,$fot(implies(not(not(X_20655)),X_20656))),bind(X_95,$fot(implies(X_20655,X_20656)))]]) ).
cnf(refute_0_229,plain,
( ~ is_a_theorem(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))))
| is_a_theorem(implies(implies(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))),X_7283),X_7283)) ),
inference(subst,[],[refute_0_141:[bind(X_7284,$fot(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227))))))]]) ).
cnf(refute_0_230,plain,
( ~ is_a_theorem(implies(implies(not(X_3903),implies(not(X_3903),X_3903)),X_3903))
| ~ is_a_theorem(implies(not(X_3903),implies(not(X_3903),X_3903)))
| is_a_theorem(X_3903) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(X_3903),implies(not(X_3903),X_3903)))),bind(Y,$fot(X_3903))]]) ).
cnf(refute_0_231,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902))),X_374),implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902)))
| is_a_theorem(implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902)) ),
inference(subst,[],[refute_0_82:[bind(X_373,$fot(implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902)))]]) ).
cnf(refute_0_232,plain,
( ~ is_a_theorem(implies(implies(X_2745,implies(X_2744,X_2744)),X_2747))
| ~ is_a_theorem(implies(implies(implies(X_2745,implies(X_2744,X_2744)),X_2747),implies(X_2746,X_2747)))
| is_a_theorem(implies(X_2746,X_2747)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_2745,implies(X_2744,X_2744)),X_2747))),bind(Y,$fot(implies(X_2746,X_2747)))]]) ).
cnf(refute_0_233,plain,
( ~ is_a_theorem(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695)))
| is_a_theorem(implies(not(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))),Y)) ),
inference(subst,[],[refute_0_28:[bind(X_6,$fot(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))))]]) ).
cnf(refute_0_234,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_1652,X_1650)),implies(X_1652,X_1650)),X_1649),implies(X_1650,X_1649)))
| is_a_theorem(implies(implies(implies(X_1652,X_1650),X_1649),implies(X_1650,X_1649))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(X_1650,X_1649))),bind(X_33,$fot(implies(X_1652,X_1650))),bind(X_34,$fot(X_1649))]]) ).
cnf(refute_0_235,plain,
( ~ is_a_theorem(implies(X_1638,implies(X_1639,implies(X_1640,X_1638))))
| is_a_theorem(implies(implies(implies(X_1639,implies(X_1640,X_1638)),Z),implies(X_1638,Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_1638)),bind(Y,$fot(implies(X_1639,implies(X_1640,X_1638))))]]) ).
cnf(refute_0_236,plain,
is_a_theorem(implies(implies(implies(X_1639,implies(X_1640,X_1638)),Z),implies(X_1638,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_1638,implies(X_1639,implies(X_1640,X_1638)))) )],[refute_0_160,refute_0_235]) ).
cnf(refute_0_237,plain,
is_a_theorem(implies(implies(implies(not(implies(X_1652,X_1650)),implies(X_1652,X_1650)),X_1649),implies(X_1650,X_1649))),
inference(subst,[],[refute_0_236:[bind(Z,$fot(X_1649)),bind(X_1638,$fot(X_1650)),bind(X_1639,$fot(not(implies(X_1652,X_1650)))),bind(X_1640,$fot(X_1652))]]) ).
cnf(refute_0_238,plain,
is_a_theorem(implies(implies(implies(X_1652,X_1650),X_1649),implies(X_1650,X_1649))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_1652,X_1650)),implies(X_1652,X_1650)),X_1649),implies(X_1650,X_1649))) )],[refute_0_237,refute_0_234]) ).
cnf(refute_0_239,plain,
is_a_theorem(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))),
inference(subst,[],[refute_0_238:[bind(X_1649,$fot(X_1695)),bind(X_1650,$fot(X_1696)),bind(X_1652,$fot(X_1697))]]) ).
cnf(refute_0_240,plain,
is_a_theorem(implies(not(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))),Y)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))) )],[refute_0_239,refute_0_233]) ).
cnf(refute_0_241,plain,
is_a_theorem(implies(not(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))),implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695)))),
inference(subst,[],[refute_0_240:[bind(Y,$fot(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))))]]) ).
cnf(refute_0_242,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_83,X_84)),implies(X_83,X_84)),implies(implies(not(X_83),X_83),X_84)))
| ~ is_a_theorem(implies(not(implies(X_83,X_84)),implies(X_83,X_84)))
| is_a_theorem(implies(implies(not(X_83),X_83),X_84)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(not(implies(X_83,X_84)),implies(X_83,X_84)))),bind(Y,$fot(implies(implies(not(X_83),X_83),X_84)))]]) ).
cnf(refute_0_243,plain,
( ~ is_a_theorem(implies(implies(X_19,X_20),implies(implies(not(X_19),X_19),X_20)))
| is_a_theorem(implies(implies(not(implies(X_19,X_20)),implies(X_19,X_20)),implies(implies(not(X_19),X_19),X_20))) ),
inference(subst,[],[refute_0_8:[bind(X_21,$fot(implies(X_19,X_20))),bind(X_22,$fot(implies(implies(not(X_19),X_19),X_20)))]]) ).
cnf(refute_0_244,plain,
is_a_theorem(implies(implies(not(implies(X_19,X_20)),implies(X_19,X_20)),implies(implies(not(X_19),X_19),X_20))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_19,X_20),implies(implies(not(X_19),X_19),X_20))) )],[refute_0_6,refute_0_243]) ).
cnf(refute_0_245,plain,
is_a_theorem(implies(implies(not(implies(X_83,X_84)),implies(X_83,X_84)),implies(implies(not(X_83),X_83),X_84))),
inference(subst,[],[refute_0_244:[bind(X_19,$fot(X_83)),bind(X_20,$fot(X_84))]]) ).
cnf(refute_0_246,plain,
( ~ is_a_theorem(implies(not(implies(X_83,X_84)),implies(X_83,X_84)))
| is_a_theorem(implies(implies(not(X_83),X_83),X_84)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_83,X_84)),implies(X_83,X_84)),implies(implies(not(X_83),X_83),X_84))) )],[refute_0_245,refute_0_242]) ).
cnf(refute_0_247,plain,
( ~ is_a_theorem(implies(not(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))),implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))))
| is_a_theorem(implies(implies(not(implies(implies(X_1697,X_1696),X_1695)),implies(implies(X_1697,X_1696),X_1695)),implies(X_1696,X_1695))) ),
inference(subst,[],[refute_0_246:[bind(X_83,$fot(implies(implies(X_1697,X_1696),X_1695))),bind(X_84,$fot(implies(X_1696,X_1695)))]]) ).
cnf(refute_0_248,plain,
is_a_theorem(implies(implies(not(implies(implies(X_1697,X_1696),X_1695)),implies(implies(X_1697,X_1696),X_1695)),implies(X_1696,X_1695))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695))),implies(implies(implies(X_1697,X_1696),X_1695),implies(X_1696,X_1695)))) )],[refute_0_241,refute_0_247]) ).
cnf(refute_0_249,plain,
is_a_theorem(implies(implies(not(implies(implies(not(X_2394),X_2394),X_2394)),implies(implies(not(X_2394),X_2394),X_2394)),implies(X_2394,X_2394))),
inference(subst,[],[refute_0_248:[bind(X_1695,$fot(X_2394)),bind(X_1696,$fot(X_2394)),bind(X_1697,$fot(not(X_2394)))]]) ).
cnf(refute_0_250,plain,
( ~ is_a_theorem(implies(implies(not(implies(implies(not(X_2394),X_2394),X_2394)),implies(implies(not(X_2394),X_2394),X_2394)),implies(X_2394,X_2394)))
| is_a_theorem(implies(X_2396,implies(X_2394,X_2394))) ),
inference(subst,[],[refute_0_86:[bind(X_282,$fot(implies(X_2394,X_2394))),bind(X_283,$fot(X_2394)),bind(X_284,$fot(implies(implies(not(X_2394),X_2394),X_2394))),bind(X_285,$fot(X_2396))]]) ).
cnf(refute_0_251,plain,
is_a_theorem(implies(X_2396,implies(X_2394,X_2394))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(implies(not(X_2394),X_2394),X_2394)),implies(implies(not(X_2394),X_2394),X_2394)),implies(X_2394,X_2394))) )],[refute_0_249,refute_0_250]) ).
cnf(refute_0_252,plain,
( ~ is_a_theorem(implies(X_2396,implies(X_2394,X_2394)))
| is_a_theorem(implies(X_2569,implies(X_2570,implies(X_2396,implies(X_2394,X_2394))))) ),
inference(subst,[],[refute_0_161:[bind(X_1638,$fot(implies(X_2396,implies(X_2394,X_2394)))),bind(X_1639,$fot(X_2569)),bind(X_1640,$fot(X_2570))]]) ).
cnf(refute_0_253,plain,
is_a_theorem(implies(X_2569,implies(X_2570,implies(X_2396,implies(X_2394,X_2394))))),
inference(resolve,[$cnf( is_a_theorem(implies(X_2396,implies(X_2394,X_2394))) )],[refute_0_251,refute_0_252]) ).
cnf(refute_0_254,plain,
is_a_theorem(implies(not(implies(X_2674,implies(X_2396,implies(X_2394,X_2394)))),implies(X_2674,implies(X_2396,implies(X_2394,X_2394))))),
inference(subst,[],[refute_0_253:[bind(X_2569,$fot(not(implies(X_2674,implies(X_2396,implies(X_2394,X_2394)))))),bind(X_2570,$fot(X_2674))]]) ).
cnf(refute_0_255,plain,
( ~ is_a_theorem(implies(not(implies(X_2674,implies(X_2396,implies(X_2394,X_2394)))),implies(X_2674,implies(X_2396,implies(X_2394,X_2394)))))
| is_a_theorem(implies(implies(implies(X_2396,implies(X_2394,X_2394)),X_2676),implies(X_2674,X_2676))) ),
inference(subst,[],[refute_0_155:[bind(X_94,$fot(X_2674)),bind(X_95,$fot(implies(X_2396,implies(X_2394,X_2394)))),bind(X_96,$fot(X_2676))]]) ).
cnf(refute_0_256,plain,
is_a_theorem(implies(implies(implies(X_2396,implies(X_2394,X_2394)),X_2676),implies(X_2674,X_2676))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(X_2674,implies(X_2396,implies(X_2394,X_2394)))),implies(X_2674,implies(X_2396,implies(X_2394,X_2394))))) )],[refute_0_254,refute_0_255]) ).
cnf(refute_0_257,plain,
is_a_theorem(implies(implies(implies(X_2745,implies(X_2744,X_2744)),X_2747),implies(X_2746,X_2747))),
inference(subst,[],[refute_0_256:[bind(X_2394,$fot(X_2744)),bind(X_2396,$fot(X_2745)),bind(X_2674,$fot(X_2746)),bind(X_2676,$fot(X_2747))]]) ).
cnf(refute_0_258,plain,
( ~ is_a_theorem(implies(implies(X_2745,implies(X_2744,X_2744)),X_2747))
| is_a_theorem(implies(X_2746,X_2747)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_2745,implies(X_2744,X_2744)),X_2747),implies(X_2746,X_2747))) )],[refute_0_257,refute_0_232]) ).
cnf(refute_0_259,plain,
( ~ is_a_theorem(implies(implies(not(implies(X_3884,X_3884)),implies(X_3884,X_3884)),implies(implies(not(X_3884),implies(not(X_3884),X_3884)),X_3884)))
| is_a_theorem(implies(X_2746,implies(implies(not(X_3884),implies(not(X_3884),X_3884)),X_3884))) ),
inference(subst,[],[refute_0_258:[bind(X_2744,$fot(X_3884)),bind(X_2745,$fot(not(implies(X_3884,X_3884)))),bind(X_2747,$fot(implies(implies(not(X_3884),implies(not(X_3884),X_3884)),X_3884)))]]) ).
cnf(refute_0_260,plain,
( ~ is_a_theorem(implies(implies(X_3881,X_3880),implies(implies(not(X_3881),implies(not(X_3881),X_3881)),X_3880)))
| is_a_theorem(implies(implies(not(implies(X_3881,X_3880)),implies(X_3881,X_3880)),implies(implies(not(X_3881),implies(not(X_3881),X_3881)),X_3880))) ),
inference(subst,[],[refute_0_8:[bind(X_21,$fot(implies(X_3881,X_3880))),bind(X_22,$fot(implies(implies(not(X_3881),implies(not(X_3881),X_3881)),X_3880)))]]) ).
cnf(refute_0_261,plain,
( ~ is_a_theorem(implies(implies(implies(not(X_3878),X_3878),X_3877),implies(implies(not(X_3878),implies(not(X_3878),X_3878)),X_3877)))
| is_a_theorem(implies(implies(X_3878,X_3877),implies(implies(not(X_3878),implies(not(X_3878),X_3878)),X_3877))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(implies(not(X_3878),implies(not(X_3878),X_3878)),X_3877))),bind(X_33,$fot(X_3878)),bind(X_34,$fot(X_3877))]]) ).
cnf(refute_0_262,plain,
( ~ is_a_theorem(implies(implies(implies(not(implies(X_1723,X_1721)),implies(X_1723,X_1721)),X_1720),implies(implies(X_1723,implies(not(X_1721),X_1721)),X_1720)))
| is_a_theorem(implies(implies(implies(X_1723,X_1721),X_1720),implies(implies(X_1723,implies(not(X_1721),X_1721)),X_1720))) ),
inference(subst,[],[refute_0_46:[bind(X_32,$fot(implies(implies(X_1723,implies(not(X_1721),X_1721)),X_1720))),bind(X_33,$fot(implies(X_1723,X_1721))),bind(X_34,$fot(X_1720))]]) ).
cnf(refute_0_263,plain,
( ~ is_a_theorem(implies(implies(X_1637,implies(not(X_1635),X_1635)),implies(X_1636,implies(X_1637,X_1635))))
| is_a_theorem(implies(implies(implies(X_1636,implies(X_1637,X_1635)),Z),implies(implies(X_1637,implies(not(X_1635),X_1635)),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(X_1637,implies(not(X_1635),X_1635)))),bind(Y,$fot(implies(X_1636,implies(X_1637,X_1635))))]]) ).
cnf(refute_0_264,plain,
is_a_theorem(implies(implies(implies(X_1636,implies(X_1637,X_1635)),Z),implies(implies(X_1637,implies(not(X_1635),X_1635)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_1637,implies(not(X_1635),X_1635)),implies(X_1636,implies(X_1637,X_1635)))) )],[refute_0_51,refute_0_263]) ).
cnf(refute_0_265,plain,
is_a_theorem(implies(implies(implies(not(implies(X_1723,X_1721)),implies(X_1723,X_1721)),X_1720),implies(implies(X_1723,implies(not(X_1721),X_1721)),X_1720))),
inference(subst,[],[refute_0_264:[bind(Z,$fot(X_1720)),bind(X_1635,$fot(X_1721)),bind(X_1636,$fot(not(implies(X_1723,X_1721)))),bind(X_1637,$fot(X_1723))]]) ).
cnf(refute_0_266,plain,
is_a_theorem(implies(implies(implies(X_1723,X_1721),X_1720),implies(implies(X_1723,implies(not(X_1721),X_1721)),X_1720))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(implies(X_1723,X_1721)),implies(X_1723,X_1721)),X_1720),implies(implies(X_1723,implies(not(X_1721),X_1721)),X_1720))) )],[refute_0_265,refute_0_262]) ).
cnf(refute_0_267,plain,
is_a_theorem(implies(implies(implies(not(X_3878),X_3878),X_3877),implies(implies(not(X_3878),implies(not(X_3878),X_3878)),X_3877))),
inference(subst,[],[refute_0_266:[bind(X_1720,$fot(X_3877)),bind(X_1721,$fot(X_3878)),bind(X_1723,$fot(not(X_3878)))]]) ).
cnf(refute_0_268,plain,
is_a_theorem(implies(implies(X_3878,X_3877),implies(implies(not(X_3878),implies(not(X_3878),X_3878)),X_3877))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(X_3878),X_3878),X_3877),implies(implies(not(X_3878),implies(not(X_3878),X_3878)),X_3877))) )],[refute_0_267,refute_0_261]) ).
cnf(refute_0_269,plain,
is_a_theorem(implies(implies(X_3881,X_3880),implies(implies(not(X_3881),implies(not(X_3881),X_3881)),X_3880))),
inference(subst,[],[refute_0_268:[bind(X_3877,$fot(X_3880)),bind(X_3878,$fot(X_3881))]]) ).
cnf(refute_0_270,plain,
is_a_theorem(implies(implies(not(implies(X_3881,X_3880)),implies(X_3881,X_3880)),implies(implies(not(X_3881),implies(not(X_3881),X_3881)),X_3880))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_3881,X_3880),implies(implies(not(X_3881),implies(not(X_3881),X_3881)),X_3880))) )],[refute_0_269,refute_0_260]) ).
cnf(refute_0_271,plain,
is_a_theorem(implies(implies(not(implies(X_3884,X_3884)),implies(X_3884,X_3884)),implies(implies(not(X_3884),implies(not(X_3884),X_3884)),X_3884))),
inference(subst,[],[refute_0_270:[bind(X_3880,$fot(X_3884)),bind(X_3881,$fot(X_3884))]]) ).
cnf(refute_0_272,plain,
is_a_theorem(implies(X_2746,implies(implies(not(X_3884),implies(not(X_3884),X_3884)),X_3884))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(implies(X_3884,X_3884)),implies(X_3884,X_3884)),implies(implies(not(X_3884),implies(not(X_3884),X_3884)),X_3884))) )],[refute_0_271,refute_0_259]) ).
cnf(refute_0_273,plain,
is_a_theorem(implies(implies(not(not(implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902))),X_374),implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902))),
inference(subst,[],[refute_0_272:[bind(X_2746,$fot(implies(not(not(implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902))),X_374))),bind(X_3884,$fot(X_3902))]]) ).
cnf(refute_0_274,plain,
is_a_theorem(implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902))),X_374),implies(implies(not(X_3902),implies(not(X_3902),X_3902)),X_3902))) )],[refute_0_273,refute_0_231]) ).
cnf(refute_0_275,plain,
is_a_theorem(implies(implies(not(X_3903),implies(not(X_3903),X_3903)),X_3903)),
inference(subst,[],[refute_0_274:[bind(X_3902,$fot(X_3903))]]) ).
cnf(refute_0_276,plain,
( ~ is_a_theorem(implies(not(X_3903),implies(not(X_3903),X_3903)))
| is_a_theorem(X_3903) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(X_3903),implies(not(X_3903),X_3903)),X_3903)) )],[refute_0_275,refute_0_230]) ).
cnf(refute_0_277,plain,
( ~ is_a_theorem(implies(not(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))),implies(not(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))),not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224)))))))
| is_a_theorem(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))) ),
inference(subst,[],[refute_0_276:[bind(X_3903,$fot(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))))]]) ).
cnf(refute_0_278,plain,
( ~ is_a_theorem(implies(implies(not(not(not(X_16219))),not(X_16219)),implies(not(not(not(implies(implies(not(not(X_16219)),X_16220),implies(X_16219,X_16220))))),X_16222)))
| is_a_theorem(implies(not(not(not(implies(implies(not(not(X_16219)),X_16220),implies(X_16219,X_16220))))),X_16222)) ),
inference(subst,[],[refute_0_219:[bind(X_7701,$fot(implies(not(not(not(implies(implies(not(not(X_16219)),X_16220),implies(X_16219,X_16220))))),X_16222))),bind(X_7702,$fot(not(X_16219)))]]) ).
cnf(refute_0_279,plain,
( ~ is_a_theorem(implies(implies(X_15120,implies(not(X_15122),X_15122)),implies(not(not(not(implies(implies(X_15122,X_15121),implies(X_15120,X_15121))))),X_15123)))
| is_a_theorem(implies(implies(not(X_15122),not(X_15120)),implies(not(not(not(implies(implies(X_15122,X_15121),implies(X_15120,X_15121))))),X_15123))) ),
inference(subst,[],[refute_0_226:[bind(X_1121,$fot(implies(not(not(not(implies(implies(X_15122,X_15121),implies(X_15120,X_15121))))),X_15123))),bind(X_1122,$fot(not(X_15122))),bind(X_1123,$fot(X_15122)),bind(X_1124,$fot(X_15120))]]) ).
cnf(refute_0_280,plain,
( ~ is_a_theorem(implies(X_168,not(X_170)))
| ~ is_a_theorem(implies(implies(X_168,not(X_170)),implies(X_170,implies(X_168,X_169))))
| is_a_theorem(implies(X_170,implies(X_168,X_169))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(X_168,not(X_170)))),bind(Y,$fot(implies(X_170,implies(X_168,X_169))))]]) ).
cnf(refute_0_281,plain,
( ~ is_a_theorem(implies(X_168,not(X_170)))
| is_a_theorem(implies(X_170,implies(X_168,X_169))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_168,not(X_170)),implies(X_170,implies(X_168,X_169)))) )],[refute_0_223,refute_0_280]) ).
cnf(refute_0_282,plain,
( ~ is_a_theorem(implies(not(not(not(X_170))),not(X_170)))
| is_a_theorem(implies(X_170,implies(not(not(not(X_170))),X_169))) ),
inference(subst,[],[refute_0_281:[bind(X_168,$fot(not(not(not(X_170)))))]]) ).
cnf(refute_0_283,plain,
is_a_theorem(implies(not(not(not(X_170))),not(X_170))),
inference(subst,[],[refute_0_215:[bind(X_7676,$fot(not(X_170)))]]) ).
cnf(refute_0_284,plain,
is_a_theorem(implies(X_170,implies(not(not(not(X_170))),X_169))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(not(X_170))),not(X_170))) )],[refute_0_283,refute_0_282]) ).
cnf(refute_0_285,plain,
is_a_theorem(implies(implies(implies(X_14368,X_14367),implies(X_14366,X_14367)),implies(not(not(not(implies(implies(X_14368,X_14367),implies(X_14366,X_14367))))),X_169))),
inference(subst,[],[refute_0_284:[bind(X_170,$fot(implies(implies(X_14368,X_14367),implies(X_14366,X_14367))))]]) ).
cnf(refute_0_286,plain,
( ~ is_a_theorem(implies(implies(implies(X_220,X_219),implies(X_218,X_219)),X_217))
| ~ is_a_theorem(implies(implies(implies(implies(X_220,X_219),implies(X_218,X_219)),X_217),implies(implies(X_218,implies(not(X_220),X_220)),X_217)))
| is_a_theorem(implies(implies(X_218,implies(not(X_220),X_220)),X_217)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_220,X_219),implies(X_218,X_219)),X_217))),bind(Y,$fot(implies(implies(X_218,implies(not(X_220),X_220)),X_217)))]]) ).
cnf(refute_0_287,plain,
( ~ is_a_theorem(implies(implies(X_183,implies(not(X_185),X_185)),implies(implies(X_185,X_184),implies(X_183,X_184))))
| is_a_theorem(implies(implies(implies(implies(X_185,X_184),implies(X_183,X_184)),Z),implies(implies(X_183,implies(not(X_185),X_185)),Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(implies(X_183,implies(not(X_185),X_185)))),bind(Y,$fot(implies(implies(X_185,X_184),implies(X_183,X_184))))]]) ).
cnf(refute_0_288,plain,
is_a_theorem(implies(implies(implies(implies(not(X_21),X_21),X_166),implies(X_164,X_166)),implies(implies(X_21,X_166),implies(X_164,X_166)))),
inference(subst,[],[refute_0_44:[bind(Z,$fot(implies(X_164,X_166))),bind(X_22,$fot(X_166))]]) ).
cnf(refute_0_289,plain,
( ~ is_a_theorem(implies(implies(implies(implies(not(X_21),X_21),X_166),implies(X_164,X_166)),implies(implies(X_21,X_166),implies(X_164,X_166))))
| is_a_theorem(implies(implies(X_164,implies(not(X_21),X_21)),implies(implies(X_21,X_166),implies(X_164,X_166)))) ),
inference(subst,[],[refute_0_23:[bind(X_79,$fot(X_164)),bind(X_80,$fot(implies(not(X_21),X_21))),bind(X_81,$fot(X_166)),bind(X_82,$fot(implies(implies(X_21,X_166),implies(X_164,X_166))))]]) ).
cnf(refute_0_290,plain,
is_a_theorem(implies(implies(X_164,implies(not(X_21),X_21)),implies(implies(X_21,X_166),implies(X_164,X_166)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(not(X_21),X_21),X_166),implies(X_164,X_166)),implies(implies(X_21,X_166),implies(X_164,X_166)))) )],[refute_0_288,refute_0_289]) ).
cnf(refute_0_291,plain,
is_a_theorem(implies(implies(X_183,implies(not(X_185),X_185)),implies(implies(X_185,X_184),implies(X_183,X_184)))),
inference(subst,[],[refute_0_290:[bind(X_164,$fot(X_183)),bind(X_166,$fot(X_184)),bind(X_21,$fot(X_185))]]) ).
cnf(refute_0_292,plain,
is_a_theorem(implies(implies(implies(implies(X_185,X_184),implies(X_183,X_184)),Z),implies(implies(X_183,implies(not(X_185),X_185)),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_183,implies(not(X_185),X_185)),implies(implies(X_185,X_184),implies(X_183,X_184)))) )],[refute_0_291,refute_0_287]) ).
cnf(refute_0_293,plain,
is_a_theorem(implies(implies(implies(implies(X_220,X_219),implies(X_218,X_219)),X_217),implies(implies(X_218,implies(not(X_220),X_220)),X_217))),
inference(subst,[],[refute_0_292:[bind(Z,$fot(X_217)),bind(X_183,$fot(X_218)),bind(X_184,$fot(X_219)),bind(X_185,$fot(X_220))]]) ).
cnf(refute_0_294,plain,
( ~ is_a_theorem(implies(implies(implies(X_220,X_219),implies(X_218,X_219)),X_217))
| is_a_theorem(implies(implies(X_218,implies(not(X_220),X_220)),X_217)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_220,X_219),implies(X_218,X_219)),X_217),implies(implies(X_218,implies(not(X_220),X_220)),X_217))) )],[refute_0_293,refute_0_286]) ).
cnf(refute_0_295,plain,
( ~ is_a_theorem(implies(implies(implies(X_14368,X_14367),implies(X_14366,X_14367)),implies(not(not(not(implies(implies(X_14368,X_14367),implies(X_14366,X_14367))))),X_169)))
| is_a_theorem(implies(implies(X_14366,implies(not(X_14368),X_14368)),implies(not(not(not(implies(implies(X_14368,X_14367),implies(X_14366,X_14367))))),X_169))) ),
inference(subst,[],[refute_0_294:[bind(X_217,$fot(implies(not(not(not(implies(implies(X_14368,X_14367),implies(X_14366,X_14367))))),X_169))),bind(X_218,$fot(X_14366)),bind(X_219,$fot(X_14367)),bind(X_220,$fot(X_14368))]]) ).
cnf(refute_0_296,plain,
is_a_theorem(implies(implies(X_14366,implies(not(X_14368),X_14368)),implies(not(not(not(implies(implies(X_14368,X_14367),implies(X_14366,X_14367))))),X_169))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_14368,X_14367),implies(X_14366,X_14367)),implies(not(not(not(implies(implies(X_14368,X_14367),implies(X_14366,X_14367))))),X_169))) )],[refute_0_285,refute_0_295]) ).
cnf(refute_0_297,plain,
is_a_theorem(implies(implies(X_15120,implies(not(X_15122),X_15122)),implies(not(not(not(implies(implies(X_15122,X_15121),implies(X_15120,X_15121))))),X_15123))),
inference(subst,[],[refute_0_296:[bind(X_14366,$fot(X_15120)),bind(X_14367,$fot(X_15121)),bind(X_14368,$fot(X_15122)),bind(X_169,$fot(X_15123))]]) ).
cnf(refute_0_298,plain,
is_a_theorem(implies(implies(not(X_15122),not(X_15120)),implies(not(not(not(implies(implies(X_15122,X_15121),implies(X_15120,X_15121))))),X_15123))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_15120,implies(not(X_15122),X_15122)),implies(not(not(not(implies(implies(X_15122,X_15121),implies(X_15120,X_15121))))),X_15123))) )],[refute_0_297,refute_0_279]) ).
cnf(refute_0_299,plain,
is_a_theorem(implies(implies(not(not(not(X_16219))),not(X_16219)),implies(not(not(not(implies(implies(not(not(X_16219)),X_16220),implies(X_16219,X_16220))))),X_16222))),
inference(subst,[],[refute_0_298:[bind(X_15120,$fot(X_16219)),bind(X_15121,$fot(X_16220)),bind(X_15122,$fot(not(not(X_16219)))),bind(X_15123,$fot(X_16222))]]) ).
cnf(refute_0_300,plain,
is_a_theorem(implies(not(not(not(implies(implies(not(not(X_16219)),X_16220),implies(X_16219,X_16220))))),X_16222)),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(not(X_16219))),not(X_16219)),implies(not(not(not(implies(implies(not(not(X_16219)),X_16220),implies(X_16219,X_16220))))),X_16222))) )],[refute_0_299,refute_0_278]) ).
cnf(refute_0_301,plain,
is_a_theorem(implies(not(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))),implies(not(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))),not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))))),
inference(subst,[],[refute_0_300:[bind(X_16219,$fot(X_16223)),bind(X_16220,$fot(X_16224)),bind(X_16222,$fot(implies(not(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))),not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224)))))))]]) ).
cnf(refute_0_302,plain,
is_a_theorem(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))),
inference(resolve,[$cnf( is_a_theorem(implies(not(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))),implies(not(not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))),not(not(implies(implies(not(not(X_16223)),X_16224),implies(X_16223,X_16224))))))) )],[refute_0_301,refute_0_277]) ).
cnf(refute_0_303,plain,
is_a_theorem(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227))))),
inference(subst,[],[refute_0_302:[bind(X_16223,$fot(X_16226)),bind(X_16224,$fot(X_16227))]]) ).
cnf(refute_0_304,plain,
is_a_theorem(implies(implies(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))),X_7283),X_7283)),
inference(resolve,[$cnf( is_a_theorem(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227))))) )],[refute_0_303,refute_0_229]) ).
cnf(refute_0_305,plain,
is_a_theorem(implies(implies(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))),implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227))),implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))),
inference(subst,[],[refute_0_304:[bind(X_7283,$fot(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227))))]]) ).
cnf(refute_0_306,plain,
( ~ is_a_theorem(implies(implies(implies(not(not(implies(X_4276,X_4275))),implies(X_4276,X_4275)),X_4274),implies(X_4277,X_4274)))
| ~ is_a_theorem(implies(implies(not(not(implies(X_4276,X_4275))),implies(X_4276,X_4275)),X_4274))
| is_a_theorem(implies(X_4277,X_4274)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(not(not(implies(X_4276,X_4275))),implies(X_4276,X_4275)),X_4274))),bind(Y,$fot(implies(X_4277,X_4274)))]]) ).
cnf(refute_0_307,plain,
( ~ is_a_theorem(implies(X_3949,implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947))))
| is_a_theorem(implies(implies(implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947)),Z),implies(X_3949,Z))) ),
inference(subst,[],[refute_0_4:[bind(X,$fot(X_3949)),bind(Y,$fot(implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947))))]]) ).
cnf(refute_0_308,plain,
is_a_theorem(implies(X_3949,implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947)))),
inference(subst,[],[refute_0_173:[bind(X_3705,$fot(X_3947)),bind(X_3706,$fot(X_3948)),bind(X_3945,$fot(X_3949))]]) ).
cnf(refute_0_309,plain,
is_a_theorem(implies(implies(implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947)),Z),implies(X_3949,Z))),
inference(resolve,[$cnf( is_a_theorem(implies(X_3949,implies(not(not(implies(X_3948,X_3947))),implies(X_3948,X_3947)))) )],[refute_0_308,refute_0_307]) ).
cnf(refute_0_310,plain,
is_a_theorem(implies(implies(implies(not(not(implies(X_4276,X_4275))),implies(X_4276,X_4275)),X_4274),implies(X_4277,X_4274))),
inference(subst,[],[refute_0_309:[bind(Z,$fot(X_4274)),bind(X_3947,$fot(X_4275)),bind(X_3948,$fot(X_4276)),bind(X_3949,$fot(X_4277))]]) ).
cnf(refute_0_311,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(X_4276,X_4275))),implies(X_4276,X_4275)),X_4274))
| is_a_theorem(implies(X_4277,X_4274)) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(not(not(implies(X_4276,X_4275))),implies(X_4276,X_4275)),X_4274),implies(X_4277,X_4274))) )],[refute_0_310,refute_0_306]) ).
cnf(refute_0_312,plain,
( ~ is_a_theorem(implies(implies(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))),implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227))),implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227))))
| is_a_theorem(implies(X_20596,implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))) ),
inference(subst,[],[refute_0_311:[bind(X_4274,$fot(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))),bind(X_4275,$fot(implies(X_16226,X_16227))),bind(X_4276,$fot(implies(not(not(X_16226)),X_16227))),bind(X_4277,$fot(X_20596))]]) ).
cnf(refute_0_313,plain,
is_a_theorem(implies(X_20596,implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))),implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227))),implies(implies(not(not(X_16226)),X_16227),implies(X_16226,X_16227)))) )],[refute_0_305,refute_0_312]) ).
cnf(refute_0_314,plain,
is_a_theorem(implies(not(implies(implies(not(not(X_20655)),X_20656),implies(X_20655,X_20656))),implies(implies(not(not(X_20655)),X_20656),implies(X_20655,X_20656)))),
inference(subst,[],[refute_0_313:[bind(X_16226,$fot(X_20655)),bind(X_16227,$fot(X_20656)),bind(X_20596,$fot(not(implies(implies(not(not(X_20655)),X_20656),implies(X_20655,X_20656)))))]]) ).
cnf(refute_0_315,plain,
is_a_theorem(implies(implies(implies(X_20655,X_20656),X_96),implies(implies(not(not(X_20655)),X_20656),X_96))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(not(X_20655)),X_20656),implies(X_20655,X_20656))),implies(implies(not(not(X_20655)),X_20656),implies(X_20655,X_20656)))) )],[refute_0_314,refute_0_228]) ).
cnf(refute_0_316,plain,
is_a_theorem(implies(implies(implies(X_20776,X_20777),implies(X_1122,X_1123)),implies(implies(not(not(X_20776)),X_20777),implies(X_1122,X_1123)))),
inference(subst,[],[refute_0_315:[bind(X_20655,$fot(X_20776)),bind(X_20656,$fot(X_20777)),bind(X_96,$fot(implies(X_1122,X_1123)))]]) ).
cnf(refute_0_317,plain,
is_a_theorem(implies(implies(X_1122,not(implies(X_20776,X_20777))),implies(implies(not(not(X_20776)),X_20777),implies(X_1122,X_1123)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_20776,X_20777),implies(X_1122,X_1123)),implies(implies(not(not(X_20776)),X_20777),implies(X_1122,X_1123)))) )],[refute_0_316,refute_0_227]) ).
cnf(refute_0_318,plain,
is_a_theorem(implies(implies(not(not(not(implies(X_22842,X_22843)))),not(implies(X_22842,X_22843))),implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),X_22841)))),
inference(subst,[],[refute_0_317:[bind(X_1122,$fot(not(not(not(implies(X_22842,X_22843)))))),bind(X_1123,$fot(X_22841)),bind(X_20776,$fot(X_22842)),bind(X_20777,$fot(X_22843))]]) ).
cnf(refute_0_319,plain,
is_a_theorem(implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),X_22841))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(not(implies(X_22842,X_22843)))),not(implies(X_22842,X_22843))),implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),X_22841)))) )],[refute_0_318,refute_0_220]) ).
cnf(refute_0_320,plain,
is_a_theorem(implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),not(not(implies(X_22842,X_22843)))))),
inference(subst,[],[refute_0_319:[bind(X_22841,$fot(not(not(implies(X_22842,X_22843)))))]]) ).
cnf(refute_0_321,plain,
( ~ is_a_theorem(implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),not(not(implies(X_22842,X_22843))))))
| is_a_theorem(implies(X_38224,implies(implies(not(not(X_22842)),X_22843),not(not(implies(X_22842,X_22843)))))) ),
inference(subst,[],[refute_0_52:[bind(X_1635,$fot(not(not(implies(X_22842,X_22843))))),bind(X_1636,$fot(X_38224)),bind(X_1637,$fot(implies(not(not(X_22842)),X_22843)))]]) ).
cnf(refute_0_322,plain,
is_a_theorem(implies(X_38224,implies(implies(not(not(X_22842)),X_22843),not(not(implies(X_22842,X_22843)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(X_22842)),X_22843),implies(not(not(not(implies(X_22842,X_22843)))),not(not(implies(X_22842,X_22843)))))) )],[refute_0_320,refute_0_321]) ).
cnf(refute_0_323,plain,
is_a_theorem(implies(not(implies(implies(not(not(X_39132)),X_39133),not(not(implies(X_39132,X_39133))))),implies(implies(not(not(X_39132)),X_39133),not(not(implies(X_39132,X_39133)))))),
inference(subst,[],[refute_0_322:[bind(X_22842,$fot(X_39132)),bind(X_22843,$fot(X_39133)),bind(X_38224,$fot(not(implies(implies(not(not(X_39132)),X_39133),not(not(implies(X_39132,X_39133)))))))]]) ).
cnf(refute_0_324,plain,
is_a_theorem(implies(not(X_39132),not(not(implies(X_39132,X_39133))))),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(not(X_39132)),X_39133),not(not(implies(X_39132,X_39133))))),implies(implies(not(not(X_39132)),X_39133),not(not(implies(X_39132,X_39133)))))) )],[refute_0_323,refute_0_55]) ).
cnf(refute_0_325,plain,
is_a_theorem(implies(not(X_39135),not(not(implies(X_39135,X_39136))))),
inference(subst,[],[refute_0_324:[bind(X_39132,$fot(X_39135)),bind(X_39133,$fot(X_39136))]]) ).
cnf(refute_0_326,plain,
is_a_theorem(implies(implies(not(not(implies(X_39135,X_39136))),Z),implies(not(X_39135),Z))),
inference(resolve,[$cnf( is_a_theorem(implies(not(X_39135),not(not(implies(X_39135,X_39136))))) )],[refute_0_325,refute_0_54]) ).
cnf(refute_0_327,plain,
is_a_theorem(implies(implies(not(not(implies(X_39158,X_39160))),X_39158),implies(not(X_39158),X_39158))),
inference(subst,[],[refute_0_326:[bind(Z,$fot(X_39158)),bind(X_39135,$fot(X_39158)),bind(X_39136,$fot(X_39160))]]) ).
cnf(refute_0_328,plain,
is_a_theorem(implies(X_1636,implies(implies(not(not(implies(X_39158,X_39160))),X_39158),X_39158))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(not(not(implies(X_39158,X_39160))),X_39158),implies(not(X_39158),X_39158))) )],[refute_0_327,refute_0_53]) ).
cnf(refute_0_329,plain,
is_a_theorem(implies(not(implies(implies(not(not(implies(X_39429,X_39430))),X_39429),X_39429)),implies(implies(not(not(implies(X_39429,X_39430))),X_39429),X_39429))),
inference(subst,[],[refute_0_328:[bind(X_1636,$fot(not(implies(implies(not(not(implies(X_39429,X_39430))),X_39429),X_39429)))),bind(X_39158,$fot(X_39429)),bind(X_39160,$fot(X_39430))]]) ).
cnf(refute_0_330,plain,
is_a_theorem(implies(not(implies(X_39429,X_39430)),X_39429)),
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(implies(not(not(implies(X_39429,X_39430))),X_39429),X_39429)),implies(implies(not(not(implies(X_39429,X_39430))),X_39429),X_39429))) )],[refute_0_329,refute_0_17]) ).
cnf(refute_0_331,plain,
is_a_theorem(implies(not(implies(x,y)),x)),
inference(subst,[],[refute_0_330:[bind(X_39429,$fot(x)),bind(X_39430,$fot(y))]]) ).
cnf(refute_0_332,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(not(implies(x,y)),x)) )],[refute_0_331,prove_cn_66]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL400-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 4 18:20:40 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 113.03/113.38 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 113.03/113.38
% 113.03/113.38 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 113.14/113.48
%------------------------------------------------------------------------------