%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL091-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n015.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:41:50 PM UTC 2026
% Result : Unsatisfiable 22.95s 23.27s
% Output : CNFRefutation 23.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 3
% Syntax : Number of clauses : 163 ( 86 unt; 0 nHn; 23 RR)
% Number of literals : 260 ( 0 equ; 98 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 973 ( 425 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(ic_JLukasiewicz_5,axiom,
is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(implies(S,P),implies(T,implies(R,P))))) ).
cnf(prove_ic_2,negated_conjecture,
~ is_a_theorem(implies(a,implies(b,a))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(implies(implies(X_2,X_3),implies(X_4,X_5)))
| ~ is_a_theorem(implies(implies(implies(X_2,X_3),implies(X_4,X_5)),implies(implies(X_5,X_2),implies(X_6,implies(X_4,X_2)))))
| is_a_theorem(implies(implies(X_5,X_2),implies(X_6,implies(X_4,X_2)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_2,X_3),implies(X_4,X_5)))),bind(Y,$fot(implies(implies(X_5,X_2),implies(X_6,implies(X_4,X_2)))))]]) ).
cnf(refute_0_1,plain,
is_a_theorem(implies(implies(implies(X_2,X_3),implies(X_4,X_5)),implies(implies(X_5,X_2),implies(X_6,implies(X_4,X_2))))),
inference(subst,[],[ic_JLukasiewicz_5:[bind(P,$fot(X_2)),bind(Q,$fot(X_3)),bind(R,$fot(X_4)),bind(S,$fot(X_5)),bind(T,$fot(X_6))]]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(implies(implies(X_2,X_3),implies(X_4,X_5)))
| is_a_theorem(implies(implies(X_5,X_2),implies(X_6,implies(X_4,X_2)))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_2,X_3),implies(X_4,X_5)),implies(implies(X_5,X_2),implies(X_6,implies(X_4,X_2))))) )],[refute_0_1,refute_0_0]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(implies(implies(X_2,X_3),implies(X_2527,implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))))))
| is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2)))) ),
inference(subst,[],[refute_0_2:[bind(X_4,$fot(X_2527)),bind(X_5,$fot(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))))))]]) ).
cnf(refute_0_4,plain,
is_a_theorem(implies(implies(implies(P,Q),implies(X_2381,X_2380)),implies(implies(X_2380,P),implies(T,implies(X_2381,P))))),
inference(subst,[],[ic_JLukasiewicz_5:[bind(R,$fot(X_2381)),bind(S,$fot(X_2380))]]) ).
cnf(refute_0_5,plain,
( ~ is_a_theorem(implies(implies(X_1611,implies(X_1613,X_1612)),X_1614))
| ~ is_a_theorem(implies(implies(implies(X_1611,implies(X_1613,X_1612)),X_1614),implies(X_1616,implies(implies(implies(X_1614,X_1615),X_1612),X_1614))))
| is_a_theorem(implies(X_1616,implies(implies(implies(X_1614,X_1615),X_1612),X_1614))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_1611,implies(X_1613,X_1612)),X_1614))),bind(Y,$fot(implies(X_1616,implies(implies(implies(X_1614,X_1615),X_1612),X_1614))))]]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(implies(implies(X_2,X_3),implies(implies(implies(X_2,X_3),X_1604),implies(X_1603,implies(X_1606,X_1604)))))
| is_a_theorem(implies(implies(implies(X_1603,implies(X_1606,X_1604)),X_2),implies(X_6,implies(implies(implies(X_2,X_3),X_1604),X_2)))) ),
inference(subst,[],[refute_0_2:[bind(X_4,$fot(implies(implies(X_2,X_3),X_1604))),bind(X_5,$fot(implies(X_1603,implies(X_1606,X_1604))))]]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_946,implies(X_950,X_948)),implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))))))
| is_a_theorem(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2)))) ),
inference(subst,[],[refute_0_2:[bind(X_4,$fot(implies(X_946,implies(X_950,X_948)))),bind(X_5,$fot(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950)))))]]) ).
cnf(refute_0_8,plain,
is_a_theorem(implies(implies(implies(X_943,X_941),implies(X_941,implies(implies(X_940,X_942),implies(X_942,X_941)))),implies(implies(implies(implies(X_940,X_942),implies(X_942,X_941)),X_943),implies(T,implies(X_941,X_943))))),
inference(subst,[],[ic_JLukasiewicz_5:[bind(P,$fot(X_943)),bind(Q,$fot(X_941)),bind(R,$fot(X_941)),bind(S,$fot(implies(implies(X_940,X_942),implies(X_942,X_941))))]]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(implies(implies(implies(X_115,X_113),implies(X_113,implies(implies(X_112,X_114),implies(X_114,X_113)))),X_110))
| ~ is_a_theorem(implies(implies(implies(implies(X_115,X_113),implies(X_113,implies(implies(X_112,X_114),implies(X_114,X_113)))),X_110),implies(X_116,implies(implies(X_111,implies(X_115,X_113)),X_110))))
| is_a_theorem(implies(X_116,implies(implies(X_111,implies(X_115,X_113)),X_110))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_115,X_113),implies(X_113,implies(implies(X_112,X_114),implies(X_114,X_113)))),X_110))),bind(Y,$fot(implies(X_116,implies(implies(X_111,implies(X_115,X_113)),X_110))))]]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_42,implies(X_47,X_45)),implies(implies(X_47,X_45),implies(X_45,implies(implies(X_44,X_46),implies(X_46,X_45)))))))
| is_a_theorem(implies(implies(implies(implies(X_47,X_45),implies(X_45,implies(implies(X_44,X_46),implies(X_46,X_45)))),X_2),implies(X_6,implies(implies(X_42,implies(X_47,X_45)),X_2)))) ),
inference(subst,[],[refute_0_2:[bind(X_4,$fot(implies(X_42,implies(X_47,X_45)))),bind(X_5,$fot(implies(implies(X_47,X_45),implies(X_45,implies(implies(X_44,X_46),implies(X_46,X_45))))))]]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(implies(implies(X_16,implies(X_14,X_12)),implies(X_12,X_13)))
| ~ is_a_theorem(implies(implies(implies(X_16,implies(X_14,X_12)),implies(X_12,X_13)),implies(X_17,implies(implies(X_15,X_12),implies(X_12,X_13)))))
| is_a_theorem(implies(X_17,implies(implies(X_15,X_12),implies(X_12,X_13)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_16,implies(X_14,X_12)),implies(X_12,X_13)))),bind(Y,$fot(implies(X_17,implies(implies(X_15,X_12),implies(X_12,X_13)))))]]) ).
cnf(refute_0_12,plain,
( ~ is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(implies(S,P),implies(T,implies(R,P)))))
| is_a_theorem(implies(implies(implies(T,implies(R,P)),implies(P,Q)),implies(X_11,implies(implies(S,P),implies(P,Q))))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(implies(P,Q))),bind(X_3,$fot(implies(R,S))),bind(X_4,$fot(implies(S,P))),bind(X_5,$fot(implies(T,implies(R,P)))),bind(X_6,$fot(X_11))]]) ).
cnf(refute_0_13,plain,
is_a_theorem(implies(implies(implies(T,implies(R,P)),implies(P,Q)),implies(X_11,implies(implies(S,P),implies(P,Q))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(implies(S,P),implies(T,implies(R,P))))) )],[ic_JLukasiewicz_5,refute_0_12]) ).
cnf(refute_0_14,plain,
is_a_theorem(implies(implies(implies(X_16,implies(X_14,X_12)),implies(X_12,X_13)),implies(X_17,implies(implies(X_15,X_12),implies(X_12,X_13))))),
inference(subst,[],[refute_0_13:[bind(P,$fot(X_12)),bind(Q,$fot(X_13)),bind(R,$fot(X_14)),bind(S,$fot(X_15)),bind(T,$fot(X_16)),bind(X_11,$fot(X_17))]]) ).
cnf(refute_0_15,plain,
( ~ is_a_theorem(implies(implies(X_16,implies(X_14,X_12)),implies(X_12,X_13)))
| is_a_theorem(implies(X_17,implies(implies(X_15,X_12),implies(X_12,X_13)))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_16,implies(X_14,X_12)),implies(X_12,X_13)),implies(X_17,implies(implies(X_15,X_12),implies(X_12,X_13))))) )],[refute_0_14,refute_0_11]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(implies(implies(X_16,implies(X_14,implies(X_34,X_32))),implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32))))))
| is_a_theorem(implies(X_17,implies(implies(X_15,implies(X_34,X_32)),implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32))))))) ),
inference(subst,[],[refute_0_15:[bind(X_12,$fot(implies(X_34,X_32))),bind(X_13,$fot(implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32)))))]]) ).
cnf(refute_0_17,plain,
is_a_theorem(implies(implies(implies(T,implies(R,X_27)),implies(X_27,X_25)),implies(X_25,implies(implies(S,X_27),implies(X_27,X_25))))),
inference(subst,[],[refute_0_13:[bind(P,$fot(X_27)),bind(Q,$fot(X_25)),bind(X_11,$fot(X_25))]]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(implies(implies(implies(T,implies(R,X_27)),implies(X_27,X_25)),implies(X_25,implies(implies(S,X_27),implies(X_27,X_25)))))
| is_a_theorem(implies(X_30,implies(implies(X_28,X_25),implies(X_25,implies(implies(S,X_27),implies(X_27,X_25)))))) ),
inference(subst,[],[refute_0_15:[bind(X_12,$fot(X_25)),bind(X_13,$fot(implies(implies(S,X_27),implies(X_27,X_25)))),bind(X_14,$fot(X_27)),bind(X_15,$fot(X_28)),bind(X_16,$fot(implies(T,implies(R,X_27)))),bind(X_17,$fot(X_30))]]) ).
cnf(refute_0_19,plain,
is_a_theorem(implies(X_30,implies(implies(X_28,X_25),implies(X_25,implies(implies(S,X_27),implies(X_27,X_25)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(T,implies(R,X_27)),implies(X_27,X_25)),implies(X_25,implies(implies(S,X_27),implies(X_27,X_25))))) )],[refute_0_17,refute_0_18]) ).
cnf(refute_0_20,plain,
is_a_theorem(implies(implies(X_16,implies(X_14,implies(X_34,X_32))),implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32)))))),
inference(subst,[],[refute_0_19:[bind(S,$fot(X_31)),bind(X_25,$fot(X_32)),bind(X_27,$fot(X_33)),bind(X_28,$fot(X_34)),bind(X_30,$fot(implies(X_16,implies(X_14,implies(X_34,X_32)))))]]) ).
cnf(refute_0_21,plain,
is_a_theorem(implies(X_17,implies(implies(X_15,implies(X_34,X_32)),implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32))))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_16,implies(X_14,implies(X_34,X_32))),implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32)))))) )],[refute_0_20,refute_0_16]) ).
cnf(refute_0_22,plain,
is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_42,implies(X_47,X_45)),implies(implies(X_47,X_45),implies(X_45,implies(implies(X_44,X_46),implies(X_46,X_45))))))),
inference(subst,[],[refute_0_21:[bind(X_15,$fot(X_42)),bind(X_17,$fot(implies(X_2,X_3))),bind(X_31,$fot(X_44)),bind(X_32,$fot(X_45)),bind(X_33,$fot(X_46)),bind(X_34,$fot(X_47))]]) ).
cnf(refute_0_23,plain,
is_a_theorem(implies(implies(implies(implies(X_47,X_45),implies(X_45,implies(implies(X_44,X_46),implies(X_46,X_45)))),X_2),implies(X_6,implies(implies(X_42,implies(X_47,X_45)),X_2)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_42,implies(X_47,X_45)),implies(implies(X_47,X_45),implies(X_45,implies(implies(X_44,X_46),implies(X_46,X_45))))))) )],[refute_0_22,refute_0_10]) ).
cnf(refute_0_24,plain,
is_a_theorem(implies(implies(implies(implies(X_115,X_113),implies(X_113,implies(implies(X_112,X_114),implies(X_114,X_113)))),X_110),implies(X_116,implies(implies(X_111,implies(X_115,X_113)),X_110)))),
inference(subst,[],[refute_0_23:[bind(X_2,$fot(X_110)),bind(X_42,$fot(X_111)),bind(X_44,$fot(X_112)),bind(X_45,$fot(X_113)),bind(X_46,$fot(X_114)),bind(X_47,$fot(X_115)),bind(X_6,$fot(X_116))]]) ).
cnf(refute_0_25,plain,
( ~ is_a_theorem(implies(implies(implies(X_115,X_113),implies(X_113,implies(implies(X_112,X_114),implies(X_114,X_113)))),X_110))
| is_a_theorem(implies(X_116,implies(implies(X_111,implies(X_115,X_113)),X_110))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_115,X_113),implies(X_113,implies(implies(X_112,X_114),implies(X_114,X_113)))),X_110),implies(X_116,implies(implies(X_111,implies(X_115,X_113)),X_110)))) )],[refute_0_24,refute_0_9]) ).
cnf(refute_0_26,plain,
( ~ is_a_theorem(implies(implies(implies(X_943,X_941),implies(X_941,implies(implies(X_940,X_942),implies(X_942,X_941)))),implies(implies(implies(implies(X_940,X_942),implies(X_942,X_941)),X_943),implies(T,implies(X_941,X_943)))))
| is_a_theorem(implies(X_944,implies(implies(X_939,implies(X_943,X_941)),implies(implies(implies(implies(X_940,X_942),implies(X_942,X_941)),X_943),implies(T,implies(X_941,X_943)))))) ),
inference(subst,[],[refute_0_25:[bind(X_110,$fot(implies(implies(implies(implies(X_940,X_942),implies(X_942,X_941)),X_943),implies(T,implies(X_941,X_943))))),bind(X_111,$fot(X_939)),bind(X_112,$fot(X_940)),bind(X_113,$fot(X_941)),bind(X_114,$fot(X_942)),bind(X_115,$fot(X_943)),bind(X_116,$fot(X_944))]]) ).
cnf(refute_0_27,plain,
is_a_theorem(implies(X_944,implies(implies(X_939,implies(X_943,X_941)),implies(implies(implies(implies(X_940,X_942),implies(X_942,X_941)),X_943),implies(T,implies(X_941,X_943)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_943,X_941),implies(X_941,implies(implies(X_940,X_942),implies(X_942,X_941)))),implies(implies(implies(implies(X_940,X_942),implies(X_942,X_941)),X_943),implies(T,implies(X_941,X_943))))) )],[refute_0_8,refute_0_26]) ).
cnf(refute_0_28,plain,
is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_946,implies(X_950,X_948)),implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950)))))),
inference(subst,[],[refute_0_27:[bind(T,$fot(X_945)),bind(X_939,$fot(X_946)),bind(X_940,$fot(X_947)),bind(X_941,$fot(X_948)),bind(X_942,$fot(X_949)),bind(X_943,$fot(X_950)),bind(X_944,$fot(implies(X_2,X_3)))]]) ).
cnf(refute_0_29,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_946,implies(X_950,X_948)),implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950)))))) )],[refute_0_28,refute_0_7]) ).
cnf(refute_0_30,plain,
( ~ is_a_theorem(X_182)
| ~ is_a_theorem(implies(X_182,implies(X_184,implies(implies(X_184,X_183),implies(X_181,implies(X_185,X_183))))))
| is_a_theorem(implies(X_184,implies(implies(X_184,X_183),implies(X_181,implies(X_185,X_183))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_182)),bind(Y,$fot(implies(X_184,implies(implies(X_184,X_183),implies(X_181,implies(X_185,X_183))))))]]) ).
cnf(refute_0_31,plain,
is_a_theorem(implies(implies(implies(X_160,X_162),implies(X_162,X_161)),implies(implies(X_161,X_160),implies(T,implies(X_162,X_160))))),
inference(subst,[],[ic_JLukasiewicz_5:[bind(P,$fot(X_160)),bind(Q,$fot(X_162)),bind(R,$fot(X_162)),bind(S,$fot(X_161))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),X_87))
| ~ is_a_theorem(implies(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),X_87),implies(X_83,implies(X_85,X_87))))
| is_a_theorem(implies(X_83,implies(X_85,X_87))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),X_87))),bind(Y,$fot(implies(X_83,implies(X_85,X_87))))]]) ).
cnf(refute_0_33,plain,
( ~ is_a_theorem(implies(implies(X_82,X_80),implies(X_80,implies(implies(X_79,X_81),implies(X_81,X_80)))))
| is_a_theorem(implies(implies(implies(implies(X_79,X_81),implies(X_81,X_80)),X_82),implies(X_6,implies(X_80,X_82)))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(X_82)),bind(X_3,$fot(X_80)),bind(X_4,$fot(X_80)),bind(X_5,$fot(implies(implies(X_79,X_81),implies(X_81,X_80))))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_40,implies(X_37,X_36)),implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36)))))))
| is_a_theorem(implies(implies(implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36)))),X_2),implies(X_6,implies(implies(X_40,implies(X_37,X_36)),X_2)))) ),
inference(subst,[],[refute_0_2:[bind(X_4,$fot(implies(X_40,implies(X_37,X_36)))),bind(X_5,$fot(implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36))))))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(implies(implies(implies(X_16,implies(X_14,X_12)),implies(X_12,X_13)),implies(X_17,implies(implies(X_15,X_12),implies(X_12,X_13)))))
| is_a_theorem(implies(implies(implies(implies(X_15,X_12),implies(X_12,X_13)),implies(X_16,implies(X_14,X_12))),implies(X_6,implies(X_17,implies(X_16,implies(X_14,X_12)))))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(implies(X_16,implies(X_14,X_12)))),bind(X_3,$fot(implies(X_12,X_13))),bind(X_4,$fot(X_17)),bind(X_5,$fot(implies(implies(X_15,X_12),implies(X_12,X_13))))]]) ).
cnf(refute_0_36,plain,
is_a_theorem(implies(implies(implies(implies(X_15,X_12),implies(X_12,X_13)),implies(X_16,implies(X_14,X_12))),implies(X_6,implies(X_17,implies(X_16,implies(X_14,X_12)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_16,implies(X_14,X_12)),implies(X_12,X_13)),implies(X_17,implies(implies(X_15,X_12),implies(X_12,X_13))))) )],[refute_0_14,refute_0_35]) ).
cnf(refute_0_37,plain,
is_a_theorem(implies(implies(implies(implies(X_15,X_12),implies(X_12,X_13)),implies(X_27,implies(X_14,X_12))),implies(implies(X_14,X_12),implies(X_17,implies(X_27,implies(X_14,X_12)))))),
inference(subst,[],[refute_0_36:[bind(X_16,$fot(X_27)),bind(X_6,$fot(implies(X_14,X_12)))]]) ).
cnf(refute_0_38,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_15,X_12),implies(X_12,X_13)),implies(X_27,implies(X_14,X_12))),implies(implies(X_14,X_12),implies(X_17,implies(X_27,implies(X_14,X_12))))))
| is_a_theorem(implies(X_30,implies(implies(X_28,implies(X_14,X_12)),implies(implies(X_14,X_12),implies(X_17,implies(X_27,implies(X_14,X_12))))))) ),
inference(subst,[],[refute_0_15:[bind(X_12,$fot(implies(X_14,X_12))),bind(X_13,$fot(implies(X_17,implies(X_27,implies(X_14,X_12))))),bind(X_14,$fot(X_27)),bind(X_15,$fot(X_28)),bind(X_16,$fot(implies(implies(X_15,X_12),implies(X_12,X_13)))),bind(X_17,$fot(X_30))]]) ).
cnf(refute_0_39,plain,
is_a_theorem(implies(X_30,implies(implies(X_28,implies(X_14,X_12)),implies(implies(X_14,X_12),implies(X_17,implies(X_27,implies(X_14,X_12))))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_15,X_12),implies(X_12,X_13)),implies(X_27,implies(X_14,X_12))),implies(implies(X_14,X_12),implies(X_17,implies(X_27,implies(X_14,X_12)))))) )],[refute_0_37,refute_0_38]) ).
cnf(refute_0_40,plain,
is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_40,implies(X_37,X_36)),implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36))))))),
inference(subst,[],[refute_0_39:[bind(X_12,$fot(X_36)),bind(X_14,$fot(X_37)),bind(X_17,$fot(X_38)),bind(X_27,$fot(X_39)),bind(X_28,$fot(X_40)),bind(X_30,$fot(implies(X_2,X_3)))]]) ).
cnf(refute_0_41,plain,
is_a_theorem(implies(implies(implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36)))),X_2),implies(X_6,implies(implies(X_40,implies(X_37,X_36)),X_2)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2,X_3),implies(implies(X_40,implies(X_37,X_36)),implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36))))))) )],[refute_0_40,refute_0_34]) ).
cnf(refute_0_42,plain,
( ~ is_a_theorem(X_35)
| ~ is_a_theorem(implies(X_35,implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32))))))
| is_a_theorem(implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_35)),bind(Y,$fot(implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32))))))]]) ).
cnf(refute_0_43,plain,
is_a_theorem(implies(X_35,implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32)))))),
inference(subst,[],[refute_0_19:[bind(S,$fot(X_31)),bind(X_25,$fot(X_32)),bind(X_27,$fot(X_33)),bind(X_28,$fot(X_34)),bind(X_30,$fot(X_35))]]) ).
cnf(refute_0_44,plain,
( ~ is_a_theorem(X_35)
| is_a_theorem(implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_35,implies(implies(X_34,X_32),implies(X_32,implies(implies(X_31,X_33),implies(X_33,X_32)))))) )],[refute_0_43,refute_0_42]) ).
cnf(refute_0_45,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36)))),X_2),implies(X_6,implies(implies(X_40,implies(X_37,X_36)),X_2))))
| is_a_theorem(implies(implies(X_77,X_75),implies(X_75,implies(implies(X_74,X_76),implies(X_76,X_75))))) ),
inference(subst,[],[refute_0_44:[bind(X_31,$fot(X_74)),bind(X_32,$fot(X_75)),bind(X_33,$fot(X_76)),bind(X_34,$fot(X_77)),bind(X_35,$fot(implies(implies(implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36)))),X_2),implies(X_6,implies(implies(X_40,implies(X_37,X_36)),X_2)))))]]) ).
cnf(refute_0_46,plain,
is_a_theorem(implies(implies(X_77,X_75),implies(X_75,implies(implies(X_74,X_76),implies(X_76,X_75))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_37,X_36),implies(X_38,implies(X_39,implies(X_37,X_36)))),X_2),implies(X_6,implies(implies(X_40,implies(X_37,X_36)),X_2)))) )],[refute_0_41,refute_0_45]) ).
cnf(refute_0_47,plain,
is_a_theorem(implies(implies(X_82,X_80),implies(X_80,implies(implies(X_79,X_81),implies(X_81,X_80))))),
inference(subst,[],[refute_0_46:[bind(X_74,$fot(X_79)),bind(X_75,$fot(X_80)),bind(X_76,$fot(X_81)),bind(X_77,$fot(X_82))]]) ).
cnf(refute_0_48,plain,
is_a_theorem(implies(implies(implies(implies(X_79,X_81),implies(X_81,X_80)),X_82),implies(X_6,implies(X_80,X_82)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_82,X_80),implies(X_80,implies(implies(X_79,X_81),implies(X_81,X_80))))) )],[refute_0_47,refute_0_33]) ).
cnf(refute_0_49,plain,
is_a_theorem(implies(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),X_87),implies(X_83,implies(X_85,X_87)))),
inference(subst,[],[refute_0_48:[bind(X_6,$fot(X_83)),bind(X_79,$fot(X_84)),bind(X_80,$fot(X_85)),bind(X_81,$fot(X_86)),bind(X_82,$fot(X_87))]]) ).
cnf(refute_0_50,plain,
( ~ is_a_theorem(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),X_87))
| is_a_theorem(implies(X_83,implies(X_85,X_87))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),X_87),implies(X_83,implies(X_85,X_87)))) )],[refute_0_49,refute_0_32]) ).
cnf(refute_0_51,plain,
( ~ is_a_theorem(implies(implies(implies(X_160,X_162),implies(X_162,X_161)),implies(implies(X_161,X_160),implies(T,implies(X_162,X_160)))))
| is_a_theorem(implies(X_159,implies(X_161,implies(implies(X_161,X_160),implies(T,implies(X_162,X_160)))))) ),
inference(subst,[],[refute_0_50:[bind(X_83,$fot(X_159)),bind(X_84,$fot(X_160)),bind(X_85,$fot(X_161)),bind(X_86,$fot(X_162)),bind(X_87,$fot(implies(implies(X_161,X_160),implies(T,implies(X_162,X_160)))))]]) ).
cnf(refute_0_52,plain,
is_a_theorem(implies(X_159,implies(X_161,implies(implies(X_161,X_160),implies(T,implies(X_162,X_160)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_160,X_162),implies(X_162,X_161)),implies(implies(X_161,X_160),implies(T,implies(X_162,X_160))))) )],[refute_0_31,refute_0_51]) ).
cnf(refute_0_53,plain,
is_a_theorem(implies(X_182,implies(X_184,implies(implies(X_184,X_183),implies(X_181,implies(X_185,X_183)))))),
inference(subst,[],[refute_0_52:[bind(T,$fot(X_181)),bind(X_159,$fot(X_182)),bind(X_160,$fot(X_183)),bind(X_161,$fot(X_184)),bind(X_162,$fot(X_185))]]) ).
cnf(refute_0_54,plain,
( ~ is_a_theorem(X_182)
| is_a_theorem(implies(X_184,implies(implies(X_184,X_183),implies(X_181,implies(X_185,X_183))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_182,implies(X_184,implies(implies(X_184,X_183),implies(X_181,implies(X_185,X_183)))))) )],[refute_0_53,refute_0_30]) ).
cnf(refute_0_55,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2))))
| is_a_theorem(implies(X_1601,implies(implies(X_1601,X_1600),implies(X_1598,implies(X_1602,X_1600))))) ),
inference(subst,[],[refute_0_54:[bind(X_181,$fot(X_1598)),bind(X_182,$fot(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2))))),bind(X_183,$fot(X_1600)),bind(X_184,$fot(X_1601)),bind(X_185,$fot(X_1602))]]) ).
cnf(refute_0_56,plain,
is_a_theorem(implies(X_1601,implies(implies(X_1601,X_1600),implies(X_1598,implies(X_1602,X_1600))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2)))) )],[refute_0_29,refute_0_55]) ).
cnf(refute_0_57,plain,
is_a_theorem(implies(implies(X_2,X_3),implies(implies(implies(X_2,X_3),X_1604),implies(X_1603,implies(X_1606,X_1604))))),
inference(subst,[],[refute_0_56:[bind(X_1598,$fot(X_1603)),bind(X_1600,$fot(X_1604)),bind(X_1601,$fot(implies(X_2,X_3))),bind(X_1602,$fot(X_1606))]]) ).
cnf(refute_0_58,plain,
is_a_theorem(implies(implies(implies(X_1603,implies(X_1606,X_1604)),X_2),implies(X_6,implies(implies(implies(X_2,X_3),X_1604),X_2)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2,X_3),implies(implies(implies(X_2,X_3),X_1604),implies(X_1603,implies(X_1606,X_1604))))) )],[refute_0_57,refute_0_6]) ).
cnf(refute_0_59,plain,
is_a_theorem(implies(implies(implies(X_1611,implies(X_1613,X_1612)),X_1614),implies(X_1616,implies(implies(implies(X_1614,X_1615),X_1612),X_1614)))),
inference(subst,[],[refute_0_58:[bind(X_1603,$fot(X_1611)),bind(X_1604,$fot(X_1612)),bind(X_1606,$fot(X_1613)),bind(X_2,$fot(X_1614)),bind(X_3,$fot(X_1615)),bind(X_6,$fot(X_1616))]]) ).
cnf(refute_0_60,plain,
( ~ is_a_theorem(implies(implies(X_1611,implies(X_1613,X_1612)),X_1614))
| is_a_theorem(implies(X_1616,implies(implies(implies(X_1614,X_1615),X_1612),X_1614))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1611,implies(X_1613,X_1612)),X_1614),implies(X_1616,implies(implies(implies(X_1614,X_1615),X_1612),X_1614)))) )],[refute_0_59,refute_0_5]) ).
cnf(refute_0_61,plain,
( ~ is_a_theorem(implies(implies(implies(P,Q),implies(X_2381,X_2380)),implies(implies(X_2380,P),implies(T,implies(X_2381,P)))))
| is_a_theorem(implies(X_2384,implies(implies(implies(implies(implies(X_2380,P),implies(T,implies(X_2381,P))),X_2383),X_2380),implies(implies(X_2380,P),implies(T,implies(X_2381,P)))))) ),
inference(subst,[],[refute_0_60:[bind(X_1611,$fot(implies(P,Q))),bind(X_1612,$fot(X_2380)),bind(X_1613,$fot(X_2381)),bind(X_1614,$fot(implies(implies(X_2380,P),implies(T,implies(X_2381,P))))),bind(X_1615,$fot(X_2383)),bind(X_1616,$fot(X_2384))]]) ).
cnf(refute_0_62,plain,
is_a_theorem(implies(X_2384,implies(implies(implies(implies(implies(X_2380,P),implies(T,implies(X_2381,P))),X_2383),X_2380),implies(implies(X_2380,P),implies(T,implies(X_2381,P)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(P,Q),implies(X_2381,X_2380)),implies(implies(X_2380,P),implies(T,implies(X_2381,P))))) )],[refute_0_4,refute_0_61]) ).
cnf(refute_0_63,plain,
is_a_theorem(implies(implies(X_2448,implies(X_2447,implies(implies(X_2446,X_2447),implies(implies(X_2449,X_2450),implies(X_2450,implies(X_2446,X_2447)))))),implies(implies(implies(implies(implies(X_2380,P),implies(T,implies(X_2381,P))),X_2383),X_2380),implies(implies(X_2380,P),implies(T,implies(X_2381,P)))))),
inference(subst,[],[refute_0_62:[bind(X_2384,$fot(implies(X_2448,implies(X_2447,implies(implies(X_2446,X_2447),implies(implies(X_2449,X_2450),implies(X_2450,implies(X_2446,X_2447))))))))]]) ).
cnf(refute_0_64,plain,
( ~ is_a_theorem(implies(implies(X_419,implies(X_418,implies(implies(X_417,X_418),implies(implies(X_420,X_421),implies(X_421,implies(X_417,X_418)))))),X_416))
| ~ is_a_theorem(implies(implies(implies(X_419,implies(X_418,implies(implies(X_417,X_418),implies(implies(X_420,X_421),implies(X_421,implies(X_417,X_418)))))),X_416),implies(X_423,implies(X_422,X_416))))
| is_a_theorem(implies(X_423,implies(X_422,X_416))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_419,implies(X_418,implies(implies(X_417,X_418),implies(implies(X_420,X_421),implies(X_421,implies(X_417,X_418)))))),X_416))),bind(Y,$fot(implies(X_423,implies(X_422,X_416))))]]) ).
cnf(refute_0_65,plain,
( ~ is_a_theorem(implies(implies(X_2,X_3),implies(X_415,implies(X_411,implies(X_410,implies(implies(X_409,X_410),implies(implies(X_412,X_413),implies(X_413,implies(X_409,X_410)))))))))
| is_a_theorem(implies(implies(implies(X_411,implies(X_410,implies(implies(X_409,X_410),implies(implies(X_412,X_413),implies(X_413,implies(X_409,X_410)))))),X_2),implies(X_6,implies(X_415,X_2)))) ),
inference(subst,[],[refute_0_2:[bind(X_4,$fot(X_415)),bind(X_5,$fot(implies(X_411,implies(X_410,implies(implies(X_409,X_410),implies(implies(X_412,X_413),implies(X_413,implies(X_409,X_410))))))))]]) ).
cnf(refute_0_66,plain,
( ~ is_a_theorem(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),implies(X_288,implies(X_287,implies(implies(X_286,X_287),implies(implies(X_290,X_291),implies(X_291,implies(X_286,X_287))))))))
| is_a_theorem(implies(X_83,implies(X_85,implies(X_288,implies(X_287,implies(implies(X_286,X_287),implies(implies(X_290,X_291),implies(X_291,implies(X_286,X_287))))))))) ),
inference(subst,[],[refute_0_50:[bind(X_87,$fot(implies(X_288,implies(X_287,implies(implies(X_286,X_287),implies(implies(X_290,X_291),implies(X_291,implies(X_286,X_287))))))))]]) ).
cnf(refute_0_67,plain,
is_a_theorem(implies(implies(implies(X_160,X_162),implies(X_162,X_161)),implies(implies(X_162,X_161),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_161)))))),
inference(subst,[],[refute_0_46:[bind(X_75,$fot(implies(X_162,X_161))),bind(X_77,$fot(implies(X_160,X_162)))]]) ).
cnf(refute_0_68,plain,
( ~ is_a_theorem(implies(implies(implies(X_160,X_162),implies(X_162,X_161)),implies(implies(X_162,X_161),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_161))))))
| is_a_theorem(implies(X_159,implies(X_161,implies(implies(X_162,X_161),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_161))))))) ),
inference(subst,[],[refute_0_50:[bind(X_83,$fot(X_159)),bind(X_84,$fot(X_160)),bind(X_85,$fot(X_161)),bind(X_86,$fot(X_162)),bind(X_87,$fot(implies(implies(X_162,X_161),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_161))))))]]) ).
cnf(refute_0_69,plain,
is_a_theorem(implies(X_159,implies(X_161,implies(implies(X_162,X_161),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_161))))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_160,X_162),implies(X_162,X_161)),implies(implies(X_162,X_161),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_161)))))) )],[refute_0_67,refute_0_68]) ).
cnf(refute_0_70,plain,
is_a_theorem(implies(implies(implies(X_254,implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255)))),implies(implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255))),X_252)),implies(X_255,implies(implies(X_162,X_255),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255))))))),
inference(subst,[],[refute_0_69:[bind(X_159,$fot(implies(implies(X_254,implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255)))),implies(implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255))),X_252)))),bind(X_161,$fot(X_255))]]) ).
cnf(refute_0_71,plain,
( ~ is_a_theorem(implies(implies(implies(X_21,X_18),implies(X_18,X_19)),implies(X_22,implies(X_20,X_18))))
| ~ is_a_theorem(implies(implies(implies(implies(X_21,X_18),implies(X_18,X_19)),implies(X_22,implies(X_20,X_18))),implies(X_24,implies(X_23,implies(X_22,implies(X_20,X_18))))))
| is_a_theorem(implies(X_24,implies(X_23,implies(X_22,implies(X_20,X_18))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(implies(X_21,X_18),implies(X_18,X_19)),implies(X_22,implies(X_20,X_18))))),bind(Y,$fot(implies(X_24,implies(X_23,implies(X_22,implies(X_20,X_18))))))]]) ).
cnf(refute_0_72,plain,
is_a_theorem(implies(implies(implies(implies(X_21,X_18),implies(X_18,X_19)),implies(X_22,implies(X_20,X_18))),implies(X_24,implies(X_23,implies(X_22,implies(X_20,X_18)))))),
inference(subst,[],[refute_0_36:[bind(X_12,$fot(X_18)),bind(X_13,$fot(X_19)),bind(X_14,$fot(X_20)),bind(X_15,$fot(X_21)),bind(X_16,$fot(X_22)),bind(X_17,$fot(X_23)),bind(X_6,$fot(X_24))]]) ).
cnf(refute_0_73,plain,
( ~ is_a_theorem(implies(implies(implies(X_21,X_18),implies(X_18,X_19)),implies(X_22,implies(X_20,X_18))))
| is_a_theorem(implies(X_24,implies(X_23,implies(X_22,implies(X_20,X_18))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_21,X_18),implies(X_18,X_19)),implies(X_22,implies(X_20,X_18))),implies(X_24,implies(X_23,implies(X_22,implies(X_20,X_18)))))) )],[refute_0_72,refute_0_71]) ).
cnf(refute_0_74,plain,
( ~ is_a_theorem(implies(implies(implies(X_254,implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255)))),implies(implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255))),X_252)),implies(X_255,implies(implies(X_162,X_255),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255)))))))
| is_a_theorem(implies(X_257,implies(X_256,implies(X_255,implies(implies(X_162,X_255),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255)))))))) ),
inference(subst,[],[refute_0_73:[bind(X_18,$fot(implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255))))),bind(X_19,$fot(X_252)),bind(X_20,$fot(implies(X_162,X_255))),bind(X_21,$fot(X_254)),bind(X_22,$fot(X_255)),bind(X_23,$fot(X_256)),bind(X_24,$fot(X_257))]]) ).
cnf(refute_0_75,plain,
is_a_theorem(implies(X_257,implies(X_256,implies(X_255,implies(implies(X_162,X_255),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255)))))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_254,implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255)))),implies(implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255))),X_252)),implies(X_255,implies(implies(X_162,X_255),implies(implies(X_74,X_76),implies(X_76,implies(X_162,X_255))))))) )],[refute_0_70,refute_0_74]) ).
cnf(refute_0_76,plain,
is_a_theorem(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),implies(X_288,implies(X_287,implies(implies(X_286,X_287),implies(implies(X_290,X_291),implies(X_291,implies(X_286,X_287)))))))),
inference(subst,[],[refute_0_75:[bind(X_162,$fot(X_286)),bind(X_255,$fot(X_287)),bind(X_256,$fot(X_288)),bind(X_257,$fot(implies(implies(X_84,X_86),implies(X_86,X_85)))),bind(X_74,$fot(X_290)),bind(X_76,$fot(X_291))]]) ).
cnf(refute_0_77,plain,
is_a_theorem(implies(X_83,implies(X_85,implies(X_288,implies(X_287,implies(implies(X_286,X_287),implies(implies(X_290,X_291),implies(X_291,implies(X_286,X_287))))))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),implies(X_288,implies(X_287,implies(implies(X_286,X_287),implies(implies(X_290,X_291),implies(X_291,implies(X_286,X_287)))))))) )],[refute_0_76,refute_0_66]) ).
cnf(refute_0_78,plain,
is_a_theorem(implies(implies(X_2,X_3),implies(X_415,implies(X_411,implies(X_410,implies(implies(X_409,X_410),implies(implies(X_412,X_413),implies(X_413,implies(X_409,X_410))))))))),
inference(subst,[],[refute_0_77:[bind(X_286,$fot(X_409)),bind(X_287,$fot(X_410)),bind(X_288,$fot(X_411)),bind(X_290,$fot(X_412)),bind(X_291,$fot(X_413)),bind(X_83,$fot(implies(X_2,X_3))),bind(X_85,$fot(X_415))]]) ).
cnf(refute_0_79,plain,
is_a_theorem(implies(implies(implies(X_411,implies(X_410,implies(implies(X_409,X_410),implies(implies(X_412,X_413),implies(X_413,implies(X_409,X_410)))))),X_2),implies(X_6,implies(X_415,X_2)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2,X_3),implies(X_415,implies(X_411,implies(X_410,implies(implies(X_409,X_410),implies(implies(X_412,X_413),implies(X_413,implies(X_409,X_410))))))))) )],[refute_0_78,refute_0_65]) ).
cnf(refute_0_80,plain,
is_a_theorem(implies(implies(implies(X_419,implies(X_418,implies(implies(X_417,X_418),implies(implies(X_420,X_421),implies(X_421,implies(X_417,X_418)))))),X_416),implies(X_423,implies(X_422,X_416)))),
inference(subst,[],[refute_0_79:[bind(X_2,$fot(X_416)),bind(X_409,$fot(X_417)),bind(X_410,$fot(X_418)),bind(X_411,$fot(X_419)),bind(X_412,$fot(X_420)),bind(X_413,$fot(X_421)),bind(X_415,$fot(X_422)),bind(X_6,$fot(X_423))]]) ).
cnf(refute_0_81,plain,
( ~ is_a_theorem(implies(implies(X_419,implies(X_418,implies(implies(X_417,X_418),implies(implies(X_420,X_421),implies(X_421,implies(X_417,X_418)))))),X_416))
| is_a_theorem(implies(X_423,implies(X_422,X_416))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_419,implies(X_418,implies(implies(X_417,X_418),implies(implies(X_420,X_421),implies(X_421,implies(X_417,X_418)))))),X_416),implies(X_423,implies(X_422,X_416)))) )],[refute_0_80,refute_0_64]) ).
cnf(refute_0_82,plain,
( ~ is_a_theorem(implies(implies(X_2448,implies(X_2447,implies(implies(X_2446,X_2447),implies(implies(X_2449,X_2450),implies(X_2450,implies(X_2446,X_2447)))))),implies(implies(implies(implies(implies(X_2380,P),implies(T,implies(X_2381,P))),X_2383),X_2380),implies(implies(X_2380,P),implies(T,implies(X_2381,P))))))
| is_a_theorem(implies(X_2452,implies(X_2451,implies(implies(implies(implies(implies(X_2380,P),implies(T,implies(X_2381,P))),X_2383),X_2380),implies(implies(X_2380,P),implies(T,implies(X_2381,P))))))) ),
inference(subst,[],[refute_0_81:[bind(X_416,$fot(implies(implies(implies(implies(implies(X_2380,P),implies(T,implies(X_2381,P))),X_2383),X_2380),implies(implies(X_2380,P),implies(T,implies(X_2381,P)))))),bind(X_417,$fot(X_2446)),bind(X_418,$fot(X_2447)),bind(X_419,$fot(X_2448)),bind(X_420,$fot(X_2449)),bind(X_421,$fot(X_2450)),bind(X_422,$fot(X_2451)),bind(X_423,$fot(X_2452))]]) ).
cnf(refute_0_83,plain,
is_a_theorem(implies(X_2452,implies(X_2451,implies(implies(implies(implies(implies(X_2380,P),implies(T,implies(X_2381,P))),X_2383),X_2380),implies(implies(X_2380,P),implies(T,implies(X_2381,P))))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2448,implies(X_2447,implies(implies(X_2446,X_2447),implies(implies(X_2449,X_2450),implies(X_2450,implies(X_2446,X_2447)))))),implies(implies(implies(implies(implies(X_2380,P),implies(T,implies(X_2381,P))),X_2383),X_2380),implies(implies(X_2380,P),implies(T,implies(X_2381,P)))))) )],[refute_0_63,refute_0_82]) ).
cnf(refute_0_84,plain,
is_a_theorem(implies(implies(X_2,X_3),implies(X_2527,implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))))))),
inference(subst,[],[refute_0_83:[bind(P,$fot(X_2522)),bind(T,$fot(X_2523)),bind(X_2380,$fot(X_2524)),bind(X_2381,$fot(X_2525)),bind(X_2383,$fot(X_2526)),bind(X_2451,$fot(X_2527)),bind(X_2452,$fot(implies(X_2,X_3)))]]) ).
cnf(refute_0_85,plain,
is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_2,X_3),implies(X_2527,implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))))))) )],[refute_0_84,refute_0_3]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(X_10573)
| ~ is_a_theorem(implies(X_10573,implies(X_10572,implies(X_10571,X_10572))))
| is_a_theorem(implies(X_10572,implies(X_10571,X_10572))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_10573)),bind(Y,$fot(implies(X_10572,implies(X_10571,X_10572))))]]) ).
cnf(refute_0_87,plain,
( ~ is_a_theorem(X_10510)
| ~ is_a_theorem(implies(X_10510,implies(X_10509,implies(X_10508,implies(X_10507,X_10508)))))
| is_a_theorem(implies(X_10509,implies(X_10508,implies(X_10507,X_10508)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_10510)),bind(Y,$fot(implies(X_10509,implies(X_10508,implies(X_10507,X_10508)))))]]) ).
cnf(refute_0_88,plain,
( ~ is_a_theorem(X_5335)
| ~ is_a_theorem(implies(X_5335,implies(implies(X_5336,X_5337),implies(X_5337,implies(X_5334,X_5337)))))
| is_a_theorem(implies(implies(X_5336,X_5337),implies(X_5337,implies(X_5334,X_5337)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_5335)),bind(Y,$fot(implies(implies(X_5336,X_5337),implies(X_5337,implies(X_5334,X_5337)))))]]) ).
cnf(refute_0_89,plain,
( ~ is_a_theorem(X_4876)
| ~ is_a_theorem(implies(X_4876,implies(X_4877,implies(implies(X_4878,X_4879),implies(X_4879,implies(X_4875,X_4879))))))
| is_a_theorem(implies(X_4877,implies(implies(X_4878,X_4879),implies(X_4879,implies(X_4875,X_4879))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_4876)),bind(Y,$fot(implies(X_4877,implies(implies(X_4878,X_4879),implies(X_4879,implies(X_4875,X_4879))))))]]) ).
cnf(refute_0_90,plain,
( ~ is_a_theorem(implies(implies(implies(X_1915,X_1914),X_1914),implies(X_1914,implies(X_1916,X_1914))))
| is_a_theorem(implies(implies(implies(X_1916,X_1914),implies(X_1915,X_1914)),implies(X_6,implies(X_1914,implies(X_1915,X_1914))))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(implies(X_1915,X_1914))),bind(X_3,$fot(X_1914)),bind(X_4,$fot(X_1914)),bind(X_5,$fot(implies(X_1916,X_1914)))]]) ).
cnf(refute_0_91,plain,
( ~ is_a_theorem(X_1904)
| ~ is_a_theorem(implies(X_1904,implies(implies(implies(X_1902,X_1901),X_1901),implies(X_1901,implies(X_1903,X_1901)))))
| is_a_theorem(implies(implies(implies(X_1902,X_1901),X_1901),implies(X_1901,implies(X_1903,X_1901)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_1904)),bind(Y,$fot(implies(implies(implies(X_1902,X_1901),X_1901),implies(X_1901,implies(X_1903,X_1901)))))]]) ).
cnf(refute_0_92,plain,
( ~ is_a_theorem(X_1697)
| ~ is_a_theorem(implies(X_1697,implies(X_1696,implies(implies(implies(X_1694,X_1693),X_1693),implies(X_1693,implies(X_1695,X_1693))))))
| is_a_theorem(implies(X_1696,implies(implies(implies(X_1694,X_1693),X_1693),implies(X_1693,implies(X_1695,X_1693))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_1697)),bind(Y,$fot(implies(X_1696,implies(implies(implies(X_1694,X_1693),X_1693),implies(X_1693,implies(X_1695,X_1693))))))]]) ).
cnf(refute_0_93,plain,
is_a_theorem(implies(implies(implies(X_1677,Q),implies(X_1681,implies(X_1679,X_1677))),implies(implies(implies(X_1679,X_1677),X_1677),implies(X_1677,implies(X_1681,X_1677))))),
inference(subst,[],[ic_JLukasiewicz_5:[bind(P,$fot(X_1677)),bind(R,$fot(X_1681)),bind(S,$fot(implies(X_1679,X_1677))),bind(T,$fot(X_1677))]]) ).
cnf(refute_0_94,plain,
( ~ is_a_theorem(implies(implies(X_107,implies(X_106,implies(X_104,X_102))),implies(implies(X_105,X_102),implies(X_102,X_103))))
| ~ is_a_theorem(implies(implies(implies(X_107,implies(X_106,implies(X_104,X_102))),implies(implies(X_105,X_102),implies(X_102,X_103))),implies(X_109,implies(X_108,implies(implies(X_105,X_102),implies(X_102,X_103))))))
| is_a_theorem(implies(X_109,implies(X_108,implies(implies(X_105,X_102),implies(X_102,X_103))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_107,implies(X_106,implies(X_104,X_102))),implies(implies(X_105,X_102),implies(X_102,X_103))))),bind(Y,$fot(implies(X_109,implies(X_108,implies(implies(X_105,X_102),implies(X_102,X_103))))))]]) ).
cnf(refute_0_95,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_21,X_18),implies(X_18,X_19)),implies(X_22,implies(X_20,X_18))),implies(X_24,implies(X_23,implies(X_22,implies(X_20,X_18))))))
| is_a_theorem(implies(implies(implies(X_23,implies(X_22,implies(X_20,X_18))),implies(implies(X_21,X_18),implies(X_18,X_19))),implies(X_6,implies(X_24,implies(implies(X_21,X_18),implies(X_18,X_19)))))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(implies(implies(X_21,X_18),implies(X_18,X_19)))),bind(X_3,$fot(implies(X_22,implies(X_20,X_18)))),bind(X_4,$fot(X_24)),bind(X_5,$fot(implies(X_23,implies(X_22,implies(X_20,X_18)))))]]) ).
cnf(refute_0_96,plain,
is_a_theorem(implies(implies(implies(X_23,implies(X_22,implies(X_20,X_18))),implies(implies(X_21,X_18),implies(X_18,X_19))),implies(X_6,implies(X_24,implies(implies(X_21,X_18),implies(X_18,X_19)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_21,X_18),implies(X_18,X_19)),implies(X_22,implies(X_20,X_18))),implies(X_24,implies(X_23,implies(X_22,implies(X_20,X_18)))))) )],[refute_0_72,refute_0_95]) ).
cnf(refute_0_97,plain,
is_a_theorem(implies(implies(implies(X_107,implies(X_106,implies(X_104,X_102))),implies(implies(X_105,X_102),implies(X_102,X_103))),implies(X_109,implies(X_108,implies(implies(X_105,X_102),implies(X_102,X_103)))))),
inference(subst,[],[refute_0_96:[bind(X_18,$fot(X_102)),bind(X_19,$fot(X_103)),bind(X_20,$fot(X_104)),bind(X_21,$fot(X_105)),bind(X_22,$fot(X_106)),bind(X_23,$fot(X_107)),bind(X_24,$fot(X_108)),bind(X_6,$fot(X_109))]]) ).
cnf(refute_0_98,plain,
( ~ is_a_theorem(implies(implies(X_107,implies(X_106,implies(X_104,X_102))),implies(implies(X_105,X_102),implies(X_102,X_103))))
| is_a_theorem(implies(X_109,implies(X_108,implies(implies(X_105,X_102),implies(X_102,X_103))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_107,implies(X_106,implies(X_104,X_102))),implies(implies(X_105,X_102),implies(X_102,X_103))),implies(X_109,implies(X_108,implies(implies(X_105,X_102),implies(X_102,X_103)))))) )],[refute_0_97,refute_0_94]) ).
cnf(refute_0_99,plain,
( ~ is_a_theorem(implies(implies(implies(X_1677,Q),implies(X_1681,implies(X_1679,X_1677))),implies(implies(implies(X_1679,X_1677),X_1677),implies(X_1677,implies(X_1681,X_1677)))))
| is_a_theorem(implies(X_1684,implies(X_1683,implies(implies(implies(X_1679,X_1677),X_1677),implies(X_1677,implies(X_1681,X_1677)))))) ),
inference(subst,[],[refute_0_98:[bind(X_102,$fot(X_1677)),bind(X_103,$fot(implies(X_1681,X_1677))),bind(X_104,$fot(X_1679)),bind(X_105,$fot(implies(X_1679,X_1677))),bind(X_106,$fot(X_1681)),bind(X_107,$fot(implies(X_1677,Q))),bind(X_108,$fot(X_1683)),bind(X_109,$fot(X_1684))]]) ).
cnf(refute_0_100,plain,
is_a_theorem(implies(X_1684,implies(X_1683,implies(implies(implies(X_1679,X_1677),X_1677),implies(X_1677,implies(X_1681,X_1677)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1677,Q),implies(X_1681,implies(X_1679,X_1677))),implies(implies(implies(X_1679,X_1677),X_1677),implies(X_1677,implies(X_1681,X_1677))))) )],[refute_0_93,refute_0_99]) ).
cnf(refute_0_101,plain,
is_a_theorem(implies(X_1697,implies(X_1696,implies(implies(implies(X_1694,X_1693),X_1693),implies(X_1693,implies(X_1695,X_1693)))))),
inference(subst,[],[refute_0_100:[bind(X_1677,$fot(X_1693)),bind(X_1679,$fot(X_1694)),bind(X_1681,$fot(X_1695)),bind(X_1683,$fot(X_1696)),bind(X_1684,$fot(X_1697))]]) ).
cnf(refute_0_102,plain,
( ~ is_a_theorem(X_1697)
| is_a_theorem(implies(X_1696,implies(implies(implies(X_1694,X_1693),X_1693),implies(X_1693,implies(X_1695,X_1693))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_1697,implies(X_1696,implies(implies(implies(X_1694,X_1693),X_1693),implies(X_1693,implies(X_1695,X_1693)))))) )],[refute_0_101,refute_0_92]) ).
cnf(refute_0_103,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2))))
| is_a_theorem(implies(X_1899,implies(implies(implies(X_1897,X_1896),X_1896),implies(X_1896,implies(X_1898,X_1896))))) ),
inference(subst,[],[refute_0_102:[bind(X_1693,$fot(X_1896)),bind(X_1694,$fot(X_1897)),bind(X_1695,$fot(X_1898)),bind(X_1696,$fot(X_1899)),bind(X_1697,$fot(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2)))))]]) ).
cnf(refute_0_104,plain,
is_a_theorem(implies(X_1899,implies(implies(implies(X_1897,X_1896),X_1896),implies(X_1896,implies(X_1898,X_1896))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2)))) )],[refute_0_29,refute_0_103]) ).
cnf(refute_0_105,plain,
is_a_theorem(implies(X_1904,implies(implies(implies(X_1902,X_1901),X_1901),implies(X_1901,implies(X_1903,X_1901))))),
inference(subst,[],[refute_0_104:[bind(X_1896,$fot(X_1901)),bind(X_1897,$fot(X_1902)),bind(X_1898,$fot(X_1903)),bind(X_1899,$fot(X_1904))]]) ).
cnf(refute_0_106,plain,
( ~ is_a_theorem(X_1904)
| is_a_theorem(implies(implies(implies(X_1902,X_1901),X_1901),implies(X_1901,implies(X_1903,X_1901)))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_1904,implies(implies(implies(X_1902,X_1901),X_1901),implies(X_1901,implies(X_1903,X_1901))))) )],[refute_0_105,refute_0_91]) ).
cnf(refute_0_107,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2))))
| is_a_theorem(implies(implies(implies(X_1911,X_1910),X_1910),implies(X_1910,implies(X_1912,X_1910)))) ),
inference(subst,[],[refute_0_106:[bind(X_1901,$fot(X_1910)),bind(X_1902,$fot(X_1911)),bind(X_1903,$fot(X_1912)),bind(X_1904,$fot(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2)))))]]) ).
cnf(refute_0_108,plain,
is_a_theorem(implies(implies(implies(X_1911,X_1910),X_1910),implies(X_1910,implies(X_1912,X_1910)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(X_947,X_949),implies(X_949,X_948)),X_950),implies(X_945,implies(X_948,X_950))),X_2),implies(X_6,implies(implies(X_946,implies(X_950,X_948)),X_2)))) )],[refute_0_29,refute_0_107]) ).
cnf(refute_0_109,plain,
is_a_theorem(implies(implies(implies(X_1915,X_1914),X_1914),implies(X_1914,implies(X_1916,X_1914)))),
inference(subst,[],[refute_0_108:[bind(X_1910,$fot(X_1914)),bind(X_1911,$fot(X_1915)),bind(X_1912,$fot(X_1916))]]) ).
cnf(refute_0_110,plain,
is_a_theorem(implies(implies(implies(X_1916,X_1914),implies(X_1915,X_1914)),implies(X_6,implies(X_1914,implies(X_1915,X_1914))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1915,X_1914),X_1914),implies(X_1914,implies(X_1916,X_1914)))) )],[refute_0_109,refute_0_90]) ).
cnf(refute_0_111,plain,
is_a_theorem(implies(implies(implies(X_1916,X_4861),implies(X_1916,X_4861)),implies(implies(X_4859,X_4861),implies(X_4861,implies(X_1916,X_4861))))),
inference(subst,[],[refute_0_110:[bind(X_1914,$fot(X_4861)),bind(X_1915,$fot(X_1916)),bind(X_6,$fot(implies(X_4859,X_4861)))]]) ).
cnf(refute_0_112,plain,
( ~ is_a_theorem(implies(implies(X_120,X_122),implies(implies(X_119,X_121),implies(X_121,X_120))))
| ~ is_a_theorem(implies(implies(implies(X_120,X_122),implies(implies(X_119,X_121),implies(X_121,X_120))),implies(X_117,implies(X_118,implies(implies(X_119,X_121),implies(X_121,X_120))))))
| is_a_theorem(implies(X_117,implies(X_118,implies(implies(X_119,X_121),implies(X_121,X_120))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_120,X_122),implies(implies(X_119,X_121),implies(X_121,X_120))))),bind(Y,$fot(implies(X_117,implies(X_118,implies(implies(X_119,X_121),implies(X_121,X_120))))))]]) ).
cnf(refute_0_113,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),X_87),implies(X_83,implies(X_85,X_87))))
| is_a_theorem(implies(implies(implies(X_85,X_87),implies(implies(X_84,X_86),implies(X_86,X_85))),implies(X_6,implies(X_83,implies(implies(X_84,X_86),implies(X_86,X_85)))))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(implies(implies(X_84,X_86),implies(X_86,X_85)))),bind(X_3,$fot(X_87)),bind(X_4,$fot(X_83)),bind(X_5,$fot(implies(X_85,X_87)))]]) ).
cnf(refute_0_114,plain,
is_a_theorem(implies(implies(implies(X_85,X_87),implies(implies(X_84,X_86),implies(X_86,X_85))),implies(X_6,implies(X_83,implies(implies(X_84,X_86),implies(X_86,X_85)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),X_87),implies(X_83,implies(X_85,X_87)))) )],[refute_0_49,refute_0_113]) ).
cnf(refute_0_115,plain,
is_a_theorem(implies(implies(implies(X_120,X_122),implies(implies(X_119,X_121),implies(X_121,X_120))),implies(X_117,implies(X_118,implies(implies(X_119,X_121),implies(X_121,X_120)))))),
inference(subst,[],[refute_0_114:[bind(X_6,$fot(X_117)),bind(X_83,$fot(X_118)),bind(X_84,$fot(X_119)),bind(X_85,$fot(X_120)),bind(X_86,$fot(X_121)),bind(X_87,$fot(X_122))]]) ).
cnf(refute_0_116,plain,
( ~ is_a_theorem(implies(implies(X_120,X_122),implies(implies(X_119,X_121),implies(X_121,X_120))))
| is_a_theorem(implies(X_117,implies(X_118,implies(implies(X_119,X_121),implies(X_121,X_120))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_120,X_122),implies(implies(X_119,X_121),implies(X_121,X_120))),implies(X_117,implies(X_118,implies(implies(X_119,X_121),implies(X_121,X_120)))))) )],[refute_0_115,refute_0_112]) ).
cnf(refute_0_117,plain,
( ~ is_a_theorem(implies(implies(implies(X_1916,X_4861),implies(X_1916,X_4861)),implies(implies(X_4859,X_4861),implies(X_4861,implies(X_1916,X_4861)))))
| is_a_theorem(implies(X_4857,implies(X_4858,implies(implies(X_4859,X_4861),implies(X_4861,implies(X_1916,X_4861)))))) ),
inference(subst,[],[refute_0_116:[bind(X_117,$fot(X_4857)),bind(X_118,$fot(X_4858)),bind(X_119,$fot(X_4859)),bind(X_120,$fot(implies(X_1916,X_4861))),bind(X_121,$fot(X_4861)),bind(X_122,$fot(implies(X_1916,X_4861)))]]) ).
cnf(refute_0_118,plain,
is_a_theorem(implies(X_4857,implies(X_4858,implies(implies(X_4859,X_4861),implies(X_4861,implies(X_1916,X_4861)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_1916,X_4861),implies(X_1916,X_4861)),implies(implies(X_4859,X_4861),implies(X_4861,implies(X_1916,X_4861))))) )],[refute_0_111,refute_0_117]) ).
cnf(refute_0_119,plain,
is_a_theorem(implies(X_4876,implies(X_4877,implies(implies(X_4878,X_4879),implies(X_4879,implies(X_4875,X_4879)))))),
inference(subst,[],[refute_0_118:[bind(X_1916,$fot(X_4875)),bind(X_4857,$fot(X_4876)),bind(X_4858,$fot(X_4877)),bind(X_4859,$fot(X_4878)),bind(X_4861,$fot(X_4879))]]) ).
cnf(refute_0_120,plain,
( ~ is_a_theorem(X_4876)
| is_a_theorem(implies(X_4877,implies(implies(X_4878,X_4879),implies(X_4879,implies(X_4875,X_4879))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_4876,implies(X_4877,implies(implies(X_4878,X_4879),implies(X_4879,implies(X_4875,X_4879)))))) )],[refute_0_119,refute_0_89]) ).
cnf(refute_0_121,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2))))
| is_a_theorem(implies(X_5331,implies(implies(X_5332,X_5333),implies(X_5333,implies(X_5329,X_5333))))) ),
inference(subst,[],[refute_0_120:[bind(X_4875,$fot(X_5329)),bind(X_4876,$fot(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2))))),bind(X_4877,$fot(X_5331)),bind(X_4878,$fot(X_5332)),bind(X_4879,$fot(X_5333))]]) ).
cnf(refute_0_122,plain,
is_a_theorem(implies(X_5331,implies(implies(X_5332,X_5333),implies(X_5333,implies(X_5329,X_5333))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2)))) )],[refute_0_85,refute_0_121]) ).
cnf(refute_0_123,plain,
is_a_theorem(implies(X_5335,implies(implies(X_5336,X_5337),implies(X_5337,implies(X_5334,X_5337))))),
inference(subst,[],[refute_0_122:[bind(X_5329,$fot(X_5334)),bind(X_5331,$fot(X_5335)),bind(X_5332,$fot(X_5336)),bind(X_5333,$fot(X_5337))]]) ).
cnf(refute_0_124,plain,
( ~ is_a_theorem(X_5335)
| is_a_theorem(implies(implies(X_5336,X_5337),implies(X_5337,implies(X_5334,X_5337)))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_5335,implies(implies(X_5336,X_5337),implies(X_5337,implies(X_5334,X_5337))))) )],[refute_0_123,refute_0_88]) ).
cnf(refute_0_125,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2))))
| is_a_theorem(implies(implies(X_5352,X_5353),implies(X_5353,implies(X_5350,X_5353)))) ),
inference(subst,[],[refute_0_124:[bind(X_5334,$fot(X_5350)),bind(X_5335,$fot(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2))))),bind(X_5336,$fot(X_5352)),bind(X_5337,$fot(X_5353))]]) ).
cnf(refute_0_126,plain,
is_a_theorem(implies(implies(X_5352,X_5353),implies(X_5353,implies(X_5350,X_5353)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2)))) )],[refute_0_85,refute_0_125]) ).
cnf(refute_0_127,plain,
is_a_theorem(implies(implies(X_10503,X_10503),implies(X_10503,implies(X_10501,X_10503)))),
inference(subst,[],[refute_0_126:[bind(X_5350,$fot(X_10501)),bind(X_5352,$fot(X_10503)),bind(X_5353,$fot(X_10503))]]) ).
cnf(refute_0_128,plain,
( ~ is_a_theorem(implies(implies(X_632,X_631),implies(X_633,implies(X_630,X_632))))
| ~ is_a_theorem(implies(implies(implies(X_632,X_631),implies(X_633,implies(X_630,X_632))),implies(X_635,implies(X_634,implies(X_633,implies(X_630,X_632))))))
| is_a_theorem(implies(X_635,implies(X_634,implies(X_633,implies(X_630,X_632))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(implies(implies(X_632,X_631),implies(X_633,implies(X_630,X_632))))),bind(Y,$fot(implies(X_635,implies(X_634,implies(X_633,implies(X_630,X_632))))))]]) ).
cnf(refute_0_129,plain,
( ~ is_a_theorem(implies(implies(implies(X_477,implies(X_474,X_476)),X_475),implies(X_478,implies(X_476,X_475))))
| is_a_theorem(implies(implies(implies(X_476,X_475),implies(X_477,implies(X_474,X_476))),implies(X_6,implies(X_478,implies(X_477,implies(X_474,X_476)))))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(implies(X_477,implies(X_474,X_476)))),bind(X_3,$fot(X_475)),bind(X_4,$fot(X_478)),bind(X_5,$fot(implies(X_476,X_475)))]]) ).
cnf(refute_0_130,plain,
( ~ is_a_theorem(implies(implies(X_466,X_467),implies(X_467,implies(X_468,implies(X_465,X_467)))))
| is_a_theorem(implies(implies(implies(X_468,implies(X_465,X_467)),X_466),implies(X_6,implies(X_467,X_466)))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(X_466)),bind(X_3,$fot(X_467)),bind(X_4,$fot(X_467)),bind(X_5,$fot(implies(X_468,implies(X_465,X_467))))]]) ).
cnf(refute_0_131,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68)))),X_67),implies(X_73,implies(implies(X_72,implies(X_69,X_68)),X_67))))
| is_a_theorem(implies(implies(implies(implies(X_72,implies(X_69,X_68)),X_67),implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68))))),implies(X_6,implies(X_73,implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68)))))))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68)))))),bind(X_3,$fot(X_67)),bind(X_4,$fot(X_73)),bind(X_5,$fot(implies(implies(X_72,implies(X_69,X_68)),X_67)))]]) ).
cnf(refute_0_132,plain,
is_a_theorem(implies(implies(implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68)))),X_67),implies(X_73,implies(implies(X_72,implies(X_69,X_68)),X_67)))),
inference(subst,[],[refute_0_41:[bind(X_2,$fot(X_67)),bind(X_36,$fot(X_68)),bind(X_37,$fot(X_69)),bind(X_38,$fot(X_70)),bind(X_39,$fot(X_71)),bind(X_40,$fot(X_72)),bind(X_6,$fot(X_73))]]) ).
cnf(refute_0_133,plain,
is_a_theorem(implies(implies(implies(implies(X_72,implies(X_69,X_68)),X_67),implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68))))),implies(X_6,implies(X_73,implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68)))))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68)))),X_67),implies(X_73,implies(implies(X_72,implies(X_69,X_68)),X_67)))) )],[refute_0_132,refute_0_131]) ).
cnf(refute_0_134,plain,
( ~ is_a_theorem(X_90)
| ~ is_a_theorem(implies(X_90,implies(implies(X_89,X_91),implies(X_91,implies(X_92,implies(X_88,X_91))))))
| is_a_theorem(implies(implies(X_89,X_91),implies(X_91,implies(X_92,implies(X_88,X_91))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(X_90)),bind(Y,$fot(implies(implies(X_89,X_91),implies(X_91,implies(X_92,implies(X_88,X_91))))))]]) ).
cnf(refute_0_135,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),implies(X_14,X_83)),implies(X_83,implies(X_85,implies(X_14,X_83)))))
| is_a_theorem(implies(X_17,implies(implies(X_15,X_83),implies(X_83,implies(X_85,implies(X_14,X_83)))))) ),
inference(subst,[],[refute_0_15:[bind(X_12,$fot(X_83)),bind(X_13,$fot(implies(X_85,implies(X_14,X_83)))),bind(X_16,$fot(implies(implies(X_84,X_86),implies(X_86,X_85))))]]) ).
cnf(refute_0_136,plain,
is_a_theorem(implies(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),implies(X_14,X_83)),implies(X_83,implies(X_85,implies(X_14,X_83))))),
inference(subst,[],[refute_0_48:[bind(X_6,$fot(X_83)),bind(X_79,$fot(X_84)),bind(X_80,$fot(X_85)),bind(X_81,$fot(X_86)),bind(X_82,$fot(implies(X_14,X_83)))]]) ).
cnf(refute_0_137,plain,
is_a_theorem(implies(X_17,implies(implies(X_15,X_83),implies(X_83,implies(X_85,implies(X_14,X_83)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_84,X_86),implies(X_86,X_85)),implies(X_14,X_83)),implies(X_83,implies(X_85,implies(X_14,X_83))))) )],[refute_0_136,refute_0_135]) ).
cnf(refute_0_138,plain,
is_a_theorem(implies(X_90,implies(implies(X_89,X_91),implies(X_91,implies(X_92,implies(X_88,X_91)))))),
inference(subst,[],[refute_0_137:[bind(X_14,$fot(X_88)),bind(X_15,$fot(X_89)),bind(X_17,$fot(X_90)),bind(X_83,$fot(X_91)),bind(X_85,$fot(X_92))]]) ).
cnf(refute_0_139,plain,
( ~ is_a_theorem(X_90)
| is_a_theorem(implies(implies(X_89,X_91),implies(X_91,implies(X_92,implies(X_88,X_91))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_90,implies(implies(X_89,X_91),implies(X_91,implies(X_92,implies(X_88,X_91)))))) )],[refute_0_138,refute_0_134]) ).
cnf(refute_0_140,plain,
( ~ is_a_theorem(implies(implies(implies(implies(X_72,implies(X_69,X_68)),X_67),implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68))))),implies(X_6,implies(X_73,implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68))))))))
| is_a_theorem(implies(implies(X_461,X_463),implies(X_463,implies(X_464,implies(X_460,X_463))))) ),
inference(subst,[],[refute_0_139:[bind(X_88,$fot(X_460)),bind(X_89,$fot(X_461)),bind(X_90,$fot(implies(implies(implies(implies(X_72,implies(X_69,X_68)),X_67),implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68))))),implies(X_6,implies(X_73,implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68))))))))),bind(X_91,$fot(X_463)),bind(X_92,$fot(X_464))]]) ).
cnf(refute_0_141,plain,
is_a_theorem(implies(implies(X_461,X_463),implies(X_463,implies(X_464,implies(X_460,X_463))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(X_72,implies(X_69,X_68)),X_67),implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68))))),implies(X_6,implies(X_73,implies(implies(X_69,X_68),implies(X_70,implies(X_71,implies(X_69,X_68)))))))) )],[refute_0_133,refute_0_140]) ).
cnf(refute_0_142,plain,
is_a_theorem(implies(implies(X_466,X_467),implies(X_467,implies(X_468,implies(X_465,X_467))))),
inference(subst,[],[refute_0_141:[bind(X_460,$fot(X_465)),bind(X_461,$fot(X_466)),bind(X_463,$fot(X_467)),bind(X_464,$fot(X_468))]]) ).
cnf(refute_0_143,plain,
is_a_theorem(implies(implies(implies(X_468,implies(X_465,X_467)),X_466),implies(X_6,implies(X_467,X_466)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_466,X_467),implies(X_467,implies(X_468,implies(X_465,X_467))))) )],[refute_0_142,refute_0_130]) ).
cnf(refute_0_144,plain,
is_a_theorem(implies(implies(implies(X_477,implies(X_474,X_476)),X_475),implies(X_478,implies(X_476,X_475)))),
inference(subst,[],[refute_0_143:[bind(X_465,$fot(X_474)),bind(X_466,$fot(X_475)),bind(X_467,$fot(X_476)),bind(X_468,$fot(X_477)),bind(X_6,$fot(X_478))]]) ).
cnf(refute_0_145,plain,
is_a_theorem(implies(implies(implies(X_476,X_475),implies(X_477,implies(X_474,X_476))),implies(X_6,implies(X_478,implies(X_477,implies(X_474,X_476)))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_477,implies(X_474,X_476)),X_475),implies(X_478,implies(X_476,X_475)))) )],[refute_0_144,refute_0_129]) ).
cnf(refute_0_146,plain,
is_a_theorem(implies(implies(implies(X_632,X_631),implies(X_633,implies(X_630,X_632))),implies(X_635,implies(X_634,implies(X_633,implies(X_630,X_632)))))),
inference(subst,[],[refute_0_145:[bind(X_474,$fot(X_630)),bind(X_475,$fot(X_631)),bind(X_476,$fot(X_632)),bind(X_477,$fot(X_633)),bind(X_478,$fot(X_634)),bind(X_6,$fot(X_635))]]) ).
cnf(refute_0_147,plain,
( ~ is_a_theorem(implies(implies(X_632,X_631),implies(X_633,implies(X_630,X_632))))
| is_a_theorem(implies(X_635,implies(X_634,implies(X_633,implies(X_630,X_632))))) ),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(X_632,X_631),implies(X_633,implies(X_630,X_632))),implies(X_635,implies(X_634,implies(X_633,implies(X_630,X_632)))))) )],[refute_0_146,refute_0_128]) ).
cnf(refute_0_148,plain,
( ~ is_a_theorem(implies(implies(X_10503,X_10503),implies(X_10503,implies(X_10501,X_10503))))
| is_a_theorem(implies(X_10506,implies(X_10505,implies(X_10503,implies(X_10501,X_10503))))) ),
inference(subst,[],[refute_0_147:[bind(X_630,$fot(X_10501)),bind(X_631,$fot(X_10503)),bind(X_632,$fot(X_10503)),bind(X_633,$fot(X_10503)),bind(X_634,$fot(X_10505)),bind(X_635,$fot(X_10506))]]) ).
cnf(refute_0_149,plain,
is_a_theorem(implies(X_10506,implies(X_10505,implies(X_10503,implies(X_10501,X_10503))))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(X_10503,X_10503),implies(X_10503,implies(X_10501,X_10503)))) )],[refute_0_127,refute_0_148]) ).
cnf(refute_0_150,plain,
is_a_theorem(implies(X_10510,implies(X_10509,implies(X_10508,implies(X_10507,X_10508))))),
inference(subst,[],[refute_0_149:[bind(X_10501,$fot(X_10507)),bind(X_10503,$fot(X_10508)),bind(X_10505,$fot(X_10509)),bind(X_10506,$fot(X_10510))]]) ).
cnf(refute_0_151,plain,
( ~ is_a_theorem(X_10510)
| is_a_theorem(implies(X_10509,implies(X_10508,implies(X_10507,X_10508)))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_10510,implies(X_10509,implies(X_10508,implies(X_10507,X_10508))))) )],[refute_0_150,refute_0_87]) ).
cnf(refute_0_152,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2))))
| is_a_theorem(implies(X_10569,implies(X_10568,implies(X_10567,X_10568)))) ),
inference(subst,[],[refute_0_151:[bind(X_10507,$fot(X_10567)),bind(X_10508,$fot(X_10568)),bind(X_10509,$fot(X_10569)),bind(X_10510,$fot(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2)))))]]) ).
cnf(refute_0_153,plain,
is_a_theorem(implies(X_10569,implies(X_10568,implies(X_10567,X_10568)))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2)))) )],[refute_0_85,refute_0_152]) ).
cnf(refute_0_154,plain,
is_a_theorem(implies(X_10573,implies(X_10572,implies(X_10571,X_10572)))),
inference(subst,[],[refute_0_153:[bind(X_10567,$fot(X_10571)),bind(X_10568,$fot(X_10572)),bind(X_10569,$fot(X_10573))]]) ).
cnf(refute_0_155,plain,
( ~ is_a_theorem(X_10573)
| is_a_theorem(implies(X_10572,implies(X_10571,X_10572))) ),
inference(resolve,[$cnf( is_a_theorem(implies(X_10573,implies(X_10572,implies(X_10571,X_10572)))) )],[refute_0_154,refute_0_86]) ).
cnf(refute_0_156,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2))))
| is_a_theorem(implies(X_10575,implies(X_10574,X_10575))) ),
inference(subst,[],[refute_0_155:[bind(X_10571,$fot(X_10574)),bind(X_10572,$fot(X_10575)),bind(X_10573,$fot(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2)))))]]) ).
cnf(refute_0_157,plain,
is_a_theorem(implies(X_10575,implies(X_10574,X_10575))),
inference(resolve,[$cnf( is_a_theorem(implies(implies(implies(implies(implies(implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522))),X_2526),X_2524),implies(implies(X_2524,X_2522),implies(X_2523,implies(X_2525,X_2522)))),X_2),implies(X_6,implies(X_2527,X_2)))) )],[refute_0_85,refute_0_156]) ).
cnf(refute_0_158,plain,
is_a_theorem(implies(a,implies(b,a))),
inference(subst,[],[refute_0_157:[bind(X_10574,$fot(b)),bind(X_10575,$fot(a))]]) ).
cnf(refute_0_159,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(implies(a,implies(b,a))) )],[refute_0_158,prove_ic_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL091-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.07/0.35 % Computer : n015.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 5 22:47:28 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.13/0.36 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 22.95/23.27 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.95/23.27
% 22.95/23.27 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 23.16/23.40
%------------------------------------------------------------------------------