%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL416-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n013.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:39 PM UTC 2026
% Result : Unsatisfiable 1.57s 1.89s
% Output : CNFRefutation 1.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 3
% Syntax : Number of clauses : 89 ( 50 unt; 0 nHn; 33 RR)
% Number of literals : 138 ( 0 equ; 50 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-2 aty)
% Number of variables : 489 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(equivalent(A,B))
| ~ is_a_theorem(A)
| is_a_theorem(B) ) ).
cnf(xcb,axiom,
is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C))) ).
cnf(prove_reflexivity,negated_conjecture,
~ is_a_theorem(equivalent(a,a)) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_712,X_711),equivalent(X_712,X_711)),X_710),X_709))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_712,X_711),equivalent(X_712,X_711)),X_710),X_709),equivalent(X_710,X_709)))
| is_a_theorem(equivalent(X_710,X_709)) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(equivalent(equivalent(equivalent(equivalent(X_712,X_711),equivalent(X_712,X_711)),X_710),X_709))),bind(B,$fot(equivalent(X_710,X_709)))]]) ).
cnf(refute_0_1,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),B),equivalent(X_705,B)),X_705))),
inference(subst,[],[xcb:[bind(A,$fot(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705))),bind(C,$fot(X_705))]]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_701),equivalent(X_702,X_701)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_701),equivalent(X_702,X_701)),X_702))
| is_a_theorem(X_702) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_701),equivalent(X_702,X_701)))),bind(B,$fot(X_702))]]) ).
cnf(refute_0_3,plain,
is_a_theorem(equivalent(X_3,equivalent(equivalent(equivalent(X_3,B),equivalent(C,B)),C))),
inference(subst,[],[xcb:[bind(A,$fot(X_3))]]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(X_3)
| ~ is_a_theorem(equivalent(X_3,equivalent(equivalent(equivalent(X_3,B),equivalent(C,B)),C)))
| is_a_theorem(equivalent(equivalent(equivalent(X_3,B),equivalent(C,B)),C)) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(X_3)),bind(B,$fot(equivalent(equivalent(equivalent(X_3,B),equivalent(C,B)),C)))]]) ).
cnf(refute_0_5,plain,
( ~ is_a_theorem(X_3)
| is_a_theorem(equivalent(equivalent(equivalent(X_3,B),equivalent(C,B)),C)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(X_3,equivalent(equivalent(equivalent(X_3,B),equivalent(C,B)),C))) )],[refute_0_3,refute_0_4]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),B),equivalent(C,B)),C)) ),
inference(subst,[],[refute_0_5:[bind(X_3,$fot(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695))))]]) ).
cnf(refute_0_7,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)),X_12))
| is_a_theorem(X_12) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)))),bind(B,$fot(X_12))]]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_5),equivalent(X_6,X_5)),X_6)) ),
inference(subst,[],[refute_0_5:[bind(B,$fot(X_5)),bind(C,$fot(X_6)),bind(X_3,$fot(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C))))]]) ).
cnf(refute_0_9,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_5),equivalent(X_6,X_5)),X_6)),
inference(resolve,[$cnf( is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C))) )],[xcb,refute_0_8]) ).
cnf(refute_0_10,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)),X_12)),
inference(subst,[],[refute_0_9:[bind(A,$fot(X_8)),bind(B,$fot(X_9)),bind(C,$fot(X_10)),bind(X_5,$fot(X_11)),bind(X_6,$fot(X_12))]]) ).
cnf(refute_0_11,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)))
| is_a_theorem(X_12) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)),X_12)) )],[refute_0_10,refute_0_7]) ).
cnf(refute_0_12,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_691,equivalent(equivalent(equivalent(X_691,X_692),equivalent(X_689,X_692)),X_689)),X_694),equivalent(equivalent(equivalent(X_694,X_693),equivalent(X_694,X_693)),X_694)))
| is_a_theorem(equivalent(equivalent(X_694,X_693),equivalent(X_694,X_693))) ),
inference(subst,[],[refute_0_11:[bind(X_10,$fot(X_689)),bind(X_11,$fot(X_694)),bind(X_12,$fot(equivalent(equivalent(X_694,X_693),equivalent(X_694,X_693)))),bind(X_8,$fot(X_691)),bind(X_9,$fot(X_692))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),X_32),equivalent(X_34,X_32)),X_30),equivalent(X_31,X_30)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),X_32),equivalent(X_34,X_32)),X_30),equivalent(X_31,X_30)),X_31))
| is_a_theorem(X_31) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),X_32),equivalent(X_34,X_32)),X_30),equivalent(X_31,X_30)))),bind(B,$fot(X_31))]]) ).
cnf(refute_0_14,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25),equivalent(X_27,X_25)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25),equivalent(X_27,X_25)),B),equivalent(C,B)),C)) ),
inference(subst,[],[refute_0_5:[bind(X_3,$fot(equivalent(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25),equivalent(X_27,X_25))))]]) ).
cnf(refute_0_15,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),equivalent(equivalent(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),B),equivalent(X_21,B)),X_21))),
inference(subst,[],[xcb:[bind(A,$fot(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21))),bind(C,$fot(X_21))]]) ).
cnf(refute_0_16,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),equivalent(equivalent(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),B),equivalent(X_21,B)),X_21)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),B),equivalent(X_21,B))) ),
inference(subst,[],[refute_0_11:[bind(X_10,$fot(X_20)),bind(X_11,$fot(X_21)),bind(X_12,$fot(equivalent(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),B),equivalent(X_21,B)))),bind(X_8,$fot(X_23)),bind(X_9,$fot(X_24))]]) ).
cnf(refute_0_17,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),B),equivalent(X_21,B))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),equivalent(equivalent(equivalent(equivalent(equivalent(X_23,equivalent(equivalent(equivalent(X_23,X_24),equivalent(X_20,X_24)),X_20)),X_21),B),equivalent(X_21,B)),X_21))) )],[refute_0_15,refute_0_16]) ).
cnf(refute_0_18,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25),equivalent(X_27,X_25))),
inference(subst,[],[refute_0_17:[bind(B,$fot(X_25)),bind(X_20,$fot(X_26)),bind(X_21,$fot(X_27)),bind(X_23,$fot(X_28)),bind(X_24,$fot(X_29))]]) ).
cnf(refute_0_19,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25),equivalent(X_27,X_25)),B),equivalent(C,B)),C)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25),equivalent(X_27,X_25))) )],[refute_0_18,refute_0_14]) ).
cnf(refute_0_20,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),X_32),equivalent(X_34,X_32)),X_30),equivalent(X_31,X_30)),X_31)),
inference(subst,[],[refute_0_19:[bind(B,$fot(X_30)),bind(C,$fot(X_31)),bind(X_25,$fot(X_32)),bind(X_26,$fot(X_33)),bind(X_27,$fot(X_34)),bind(X_28,$fot(X_35)),bind(X_29,$fot(X_36))]]) ).
cnf(refute_0_21,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),X_32),equivalent(X_34,X_32)),X_30),equivalent(X_31,X_30)))
| is_a_theorem(X_31) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),X_32),equivalent(X_34,X_32)),X_30),equivalent(X_31,X_30)),X_31)) )],[refute_0_20,refute_0_13]) ).
cnf(refute_0_22,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))),equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)))))
| is_a_theorem(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))) ),
inference(subst,[],[refute_0_21:[bind(X_30,$fot(equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)))),bind(X_31,$fot(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)))),bind(X_32,$fot(equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)))]]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(equivalent(equivalent(X_74,equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),X_74))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_74,equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),X_74),B),equivalent(C,B)),C)) ),
inference(subst,[],[refute_0_5:[bind(X_3,$fot(equivalent(equivalent(X_74,equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),X_74)))]]) ).
cnf(refute_0_24,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(X_37,equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38))),X_37)),
inference(subst,[],[refute_0_9:[bind(X_5,$fot(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38))),bind(X_6,$fot(X_37))]]) ).
cnf(refute_0_25,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25),equivalent(X_27,X_25)))
| is_a_theorem(equivalent(X_27,X_25)) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25))),bind(B,$fot(equivalent(X_27,X_25)))]]) ).
cnf(refute_0_26,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25))
| is_a_theorem(equivalent(X_27,X_25)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_28,equivalent(equivalent(equivalent(X_28,X_29),equivalent(X_26,X_29)),X_26)),X_27),X_25),equivalent(X_27,X_25))) )],[refute_0_18,refute_0_25]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(X_37,equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38))),X_37))
| is_a_theorem(equivalent(equivalent(X_37,equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),X_37)) ),
inference(subst,[],[refute_0_26:[bind(X_25,$fot(X_37)),bind(X_26,$fot(X_38)),bind(X_27,$fot(equivalent(X_37,equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)))),bind(X_28,$fot(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)))),bind(X_29,$fot(X_41))]]) ).
cnf(refute_0_28,plain,
is_a_theorem(equivalent(equivalent(X_37,equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),X_37)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(X_37,equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38))),X_37)) )],[refute_0_24,refute_0_27]) ).
cnf(refute_0_29,plain,
is_a_theorem(equivalent(equivalent(X_74,equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),X_74)),
inference(subst,[],[refute_0_28:[bind(A,$fot(X_71)),bind(B,$fot(X_72)),bind(C,$fot(X_73)),bind(X_37,$fot(X_74)),bind(X_38,$fot(X_75)),bind(X_41,$fot(X_76))]]) ).
cnf(refute_0_30,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_74,equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),X_74),B),equivalent(C,B)),C)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_74,equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),X_74)) )],[refute_0_29,refute_0_23]) ).
cnf(refute_0_31,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75))),equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73))),equivalent(X_655,equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)))),X_655)),
inference(subst,[],[refute_0_30:[bind(B,$fot(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)))),bind(C,$fot(X_655)),bind(X_74,$fot(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75))))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_136,equivalent(equivalent(equivalent(X_136,X_137),equivalent(X_133,X_137)),X_133)),X_134),equivalent(X_135,X_134)),X_135),X_132),X_131))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_136,equivalent(equivalent(equivalent(X_136,X_137),equivalent(X_133,X_137)),X_133)),X_134),equivalent(X_135,X_134)),X_135),X_132),X_131),equivalent(X_132,X_131)))
| is_a_theorem(equivalent(X_132,X_131)) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_136,equivalent(equivalent(equivalent(X_136,X_137),equivalent(X_133,X_137)),X_133)),X_134),equivalent(X_135,X_134)),X_135),X_132),X_131))),bind(B,$fot(equivalent(X_132,X_131)))]]) ).
cnf(refute_0_33,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),B),equivalent(X_124,B)),X_124))),
inference(subst,[],[xcb:[bind(A,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124))),bind(C,$fot(X_124))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_18,equivalent(equivalent(equivalent(X_18,X_19),equivalent(X_15,X_19)),X_15)),X_16),equivalent(X_17,X_16)),X_17),X_13),equivalent(X_14,X_13)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_18,equivalent(equivalent(equivalent(X_18,X_19),equivalent(X_15,X_19)),X_15)),X_16),equivalent(X_17,X_16)),X_17),X_13),equivalent(X_14,X_13)),X_14))
| is_a_theorem(X_14) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_18,equivalent(equivalent(equivalent(X_18,X_19),equivalent(X_15,X_19)),X_15)),X_16),equivalent(X_17,X_16)),X_17),X_13),equivalent(X_14,X_13)))),bind(B,$fot(X_14))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)),X_12))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)),X_12),B),equivalent(C,B)),C)) ),
inference(subst,[],[refute_0_5:[bind(X_3,$fot(equivalent(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)),X_12)))]]) ).
cnf(refute_0_36,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)),X_12),B),equivalent(C,B)),C)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_8,equivalent(equivalent(equivalent(X_8,X_9),equivalent(X_10,X_9)),X_10)),X_11),equivalent(X_12,X_11)),X_12)) )],[refute_0_10,refute_0_35]) ).
cnf(refute_0_37,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_18,equivalent(equivalent(equivalent(X_18,X_19),equivalent(X_15,X_19)),X_15)),X_16),equivalent(X_17,X_16)),X_17),X_13),equivalent(X_14,X_13)),X_14)),
inference(subst,[],[refute_0_36:[bind(B,$fot(X_13)),bind(C,$fot(X_14)),bind(X_10,$fot(X_15)),bind(X_11,$fot(X_16)),bind(X_12,$fot(X_17)),bind(X_8,$fot(X_18)),bind(X_9,$fot(X_19))]]) ).
cnf(refute_0_38,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_18,equivalent(equivalent(equivalent(X_18,X_19),equivalent(X_15,X_19)),X_15)),X_16),equivalent(X_17,X_16)),X_17),X_13),equivalent(X_14,X_13)))
| is_a_theorem(X_14) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_18,equivalent(equivalent(equivalent(X_18,X_19),equivalent(X_15,X_19)),X_15)),X_16),equivalent(X_17,X_16)),X_17),X_13),equivalent(X_14,X_13)),X_14)) )],[refute_0_37,refute_0_34]) ).
cnf(refute_0_39,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),B),equivalent(X_124,B)),X_124)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),B),equivalent(X_124,B))) ),
inference(subst,[],[refute_0_38:[bind(X_13,$fot(X_124)),bind(X_14,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),B),equivalent(X_124,B)))),bind(X_15,$fot(X_126)),bind(X_16,$fot(X_127)),bind(X_17,$fot(X_128)),bind(X_18,$fot(X_129)),bind(X_19,$fot(X_130))]]) ).
cnf(refute_0_40,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),B),equivalent(X_124,B))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(X_128,X_127)),X_128),X_124),B),equivalent(X_124,B)),X_124))) )],[refute_0_33,refute_0_39]) ).
cnf(refute_0_41,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_136,equivalent(equivalent(equivalent(X_136,X_137),equivalent(X_133,X_137)),X_133)),X_134),equivalent(X_135,X_134)),X_135),X_132),X_131),equivalent(X_132,X_131))),
inference(subst,[],[refute_0_40:[bind(B,$fot(X_131)),bind(X_124,$fot(X_132)),bind(X_126,$fot(X_133)),bind(X_127,$fot(X_134)),bind(X_128,$fot(X_135)),bind(X_129,$fot(X_136)),bind(X_130,$fot(X_137))]]) ).
cnf(refute_0_42,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_136,equivalent(equivalent(equivalent(X_136,X_137),equivalent(X_133,X_137)),X_133)),X_134),equivalent(X_135,X_134)),X_135),X_132),X_131))
| is_a_theorem(equivalent(X_132,X_131)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_136,equivalent(equivalent(equivalent(X_136,X_137),equivalent(X_133,X_137)),X_133)),X_134),equivalent(X_135,X_134)),X_135),X_132),X_131),equivalent(X_132,X_131))) )],[refute_0_41,refute_0_32]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75))),equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73))),equivalent(X_655,equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)))),X_655))
| is_a_theorem(equivalent(equivalent(X_655,equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73))),X_655)) ),
inference(subst,[],[refute_0_42:[bind(X_131,$fot(X_655)),bind(X_132,$fot(equivalent(X_655,equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73))))),bind(X_133,$fot(X_75)),bind(X_134,$fot(equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75))),bind(X_135,$fot(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)))),bind(X_136,$fot(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)))),bind(X_137,$fot(X_76))]]) ).
cnf(refute_0_44,plain,
is_a_theorem(equivalent(equivalent(X_655,equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73))),X_655)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75)),equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),equivalent(equivalent(equivalent(equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)),X_76),equivalent(X_75,X_76)),X_75))),equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73))),equivalent(X_655,equivalent(X_71,equivalent(equivalent(equivalent(X_71,X_72),equivalent(X_73,X_72)),X_73)))),X_655)) )],[refute_0_31,refute_0_43]) ).
cnf(refute_0_45,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))),equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))))),
inference(subst,[],[refute_0_44:[bind(X_655,$fot(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))))),bind(X_71,$fot(X_34)),bind(X_72,$fot(X_664)),bind(X_73,$fot(X_665))]]) ).
cnf(refute_0_46,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))),equivalent(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(equivalent(X_35,X_36),equivalent(X_33,X_36)),X_33)),X_34),equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665)),equivalent(X_34,equivalent(equivalent(equivalent(X_34,X_664),equivalent(X_665,X_664)),X_665))))) )],[refute_0_45,refute_0_22]) ).
cnf(refute_0_47,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_691,equivalent(equivalent(equivalent(X_691,X_692),equivalent(X_689,X_692)),X_689)),X_694),equivalent(equivalent(equivalent(X_694,X_693),equivalent(X_694,X_693)),X_694))),
inference(subst,[],[refute_0_46:[bind(X_33,$fot(X_689)),bind(X_34,$fot(X_694)),bind(X_35,$fot(X_691)),bind(X_36,$fot(X_692)),bind(X_664,$fot(X_693)),bind(X_665,$fot(X_694))]]) ).
cnf(refute_0_48,plain,
is_a_theorem(equivalent(equivalent(X_694,X_693),equivalent(X_694,X_693))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_691,equivalent(equivalent(equivalent(X_691,X_692),equivalent(X_689,X_692)),X_689)),X_694),equivalent(equivalent(equivalent(X_694,X_693),equivalent(X_694,X_693)),X_694))) )],[refute_0_47,refute_0_12]) ).
cnf(refute_0_49,plain,
is_a_theorem(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695))),
inference(subst,[],[refute_0_48:[bind(X_693,$fot(X_695)),bind(X_694,$fot(X_696))]]) ).
cnf(refute_0_50,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),B),equivalent(C,B)),C)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695))) )],[refute_0_49,refute_0_6]) ).
cnf(refute_0_51,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_701),equivalent(X_702,X_701)),X_702)),
inference(subst,[],[refute_0_50:[bind(B,$fot(X_701)),bind(C,$fot(X_702)),bind(X_695,$fot(X_703)),bind(X_696,$fot(X_704))]]) ).
cnf(refute_0_52,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_701),equivalent(X_702,X_701)))
| is_a_theorem(X_702) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_701),equivalent(X_702,X_701)),X_702)) )],[refute_0_51,refute_0_2]) ).
cnf(refute_0_53,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),B),equivalent(X_705,B)),X_705)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),B),equivalent(X_705,B))) ),
inference(subst,[],[refute_0_52:[bind(X_701,$fot(X_705)),bind(X_702,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),B),equivalent(X_705,B)))),bind(X_703,$fot(X_707)),bind(X_704,$fot(X_708))]]) ).
cnf(refute_0_54,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),B),equivalent(X_705,B))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_708,X_707),equivalent(X_708,X_707)),X_705),B),equivalent(X_705,B)),X_705))) )],[refute_0_1,refute_0_53]) ).
cnf(refute_0_55,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_712,X_711),equivalent(X_712,X_711)),X_710),X_709),equivalent(X_710,X_709))),
inference(subst,[],[refute_0_54:[bind(B,$fot(X_709)),bind(X_705,$fot(X_710)),bind(X_707,$fot(X_711)),bind(X_708,$fot(X_712))]]) ).
cnf(refute_0_56,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_712,X_711),equivalent(X_712,X_711)),X_710),X_709))
| is_a_theorem(equivalent(X_710,X_709)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_712,X_711),equivalent(X_712,X_711)),X_710),X_709),equivalent(X_710,X_709))) )],[refute_0_55,refute_0_0]) ).
cnf(refute_0_57,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_3056,X_3055),equivalent(X_3056,X_3055)),X_3054),X_3054))
| is_a_theorem(equivalent(X_3054,X_3054)) ),
inference(subst,[],[refute_0_56:[bind(X_709,$fot(X_3054)),bind(X_710,$fot(X_3054)),bind(X_711,$fot(X_3055)),bind(X_712,$fot(X_3056))]]) ).
cnf(refute_0_58,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050)))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)) ),
inference(subst,[],[refute_0_11:[bind(X_10,$fot(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),bind(X_11,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050)))),bind(X_12,$fot(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),bind(X_8,$fot(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),bind(X_9,$fot(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)))]]) ).
cnf(refute_0_59,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042),equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042)),equivalent(X_3040,equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042))),X_3040))
| is_a_theorem(equivalent(equivalent(X_3040,equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042)),X_3040)) ),
inference(subst,[],[refute_0_56:[bind(X_709,$fot(X_3040)),bind(X_710,$fot(equivalent(X_3040,equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042)))),bind(X_711,$fot(X_3042)),bind(X_712,$fot(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041)))))]]) ).
cnf(refute_0_60,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_2763,X_2762),equivalent(X_2763,X_2762)),equivalent(equivalent(equivalent(equivalent(X_2765,X_2764),equivalent(X_2765,X_2764)),X_2760),equivalent(X_2761,X_2760))),X_2761))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_2763,X_2762),equivalent(X_2763,X_2762)),equivalent(equivalent(equivalent(equivalent(X_2765,X_2764),equivalent(X_2765,X_2764)),X_2760),equivalent(X_2761,X_2760))),X_2761),B),equivalent(C,B)),C)) ),
inference(subst,[],[refute_0_5:[bind(X_3,$fot(equivalent(equivalent(equivalent(equivalent(X_2763,X_2762),equivalent(X_2763,X_2762)),equivalent(equivalent(equivalent(equivalent(X_2765,X_2764),equivalent(X_2765,X_2764)),X_2760),equivalent(X_2761,X_2760))),X_2761)))]]) ).
cnf(refute_0_61,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754)),X_2757)),equivalent(equivalent(equivalent(equivalent(equivalent(X_2759,X_2758),equivalent(X_2759,X_2758)),equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754))),X_2757),equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754)),X_2757))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_2759,X_2758),equivalent(X_2759,X_2758)),equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754))),X_2757)) ),
inference(subst,[],[refute_0_52:[bind(X_701,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754)),X_2757))),bind(X_702,$fot(equivalent(equivalent(equivalent(equivalent(X_2759,X_2758),equivalent(X_2759,X_2758)),equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754))),X_2757)))]]) ).
cnf(refute_0_62,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)),X_2743),equivalent(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)),X_2743)),equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739))),equivalent(equivalent(equivalent(equivalent(equivalent(X_2745,X_2744),equivalent(X_2745,X_2744)),X_2740),X_2741),equivalent(X_2740,X_2741))))
| is_a_theorem(equivalent(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)),equivalent(equivalent(equivalent(equivalent(equivalent(X_2745,X_2744),equivalent(X_2745,X_2744)),X_2740),X_2741),equivalent(X_2740,X_2741)))) ),
inference(subst,[],[refute_0_56:[bind(X_709,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(X_2745,X_2744),equivalent(X_2745,X_2744)),X_2740),X_2741),equivalent(X_2740,X_2741)))),bind(X_710,$fot(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)))),bind(X_711,$fot(X_2743)),bind(X_712,$fot(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739))))]]) ).
cnf(refute_0_63,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498)),X_2495)),equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498)))),
inference(subst,[],[refute_0_50:[bind(B,$fot(X_2495)),bind(C,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498))))]]) ).
cnf(refute_0_64,plain,
( ~ is_a_theorem(equivalent(equivalent(X_180,equivalent(equivalent(equivalent(X_180,X_181),equivalent(X_178,X_181)),X_178)),X_179))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X_180,equivalent(equivalent(equivalent(X_180,X_181),equivalent(X_178,X_181)),X_178)),X_179),equivalent(equivalent(equivalent(equivalent(equivalent(X_175,equivalent(equivalent(equivalent(X_175,X_176),equivalent(X_177,X_176)),X_177)),X_183),equivalent(X_182,X_183)),X_182),X_179)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_175,equivalent(equivalent(equivalent(X_175,X_176),equivalent(X_177,X_176)),X_177)),X_183),equivalent(X_182,X_183)),X_182),X_179)) ),
inference(subst,[],[condensed_detachment:[bind(A,$fot(equivalent(equivalent(X_180,equivalent(equivalent(equivalent(X_180,X_181),equivalent(X_178,X_181)),X_178)),X_179))),bind(B,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(X_175,equivalent(equivalent(equivalent(X_175,X_176),equivalent(X_177,X_176)),X_177)),X_183),equivalent(X_182,X_183)),X_182),X_179)))]]) ).
cnf(refute_0_65,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)))),
inference(subst,[],[refute_0_28:[bind(X_37,$fot(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38))))]]) ).
cnf(refute_0_66,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38))))
| is_a_theorem(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127))) ),
inference(subst,[],[refute_0_38:[bind(X_13,$fot(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38))),bind(X_14,$fot(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127)))),bind(X_15,$fot(X_126)),bind(X_16,$fot(X_127)),bind(X_17,$fot(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38))),bind(X_18,$fot(X_129)),bind(X_19,$fot(X_130))]]) ).
cnf(refute_0_67,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)),equivalent(equivalent(equivalent(equivalent(X_129,equivalent(equivalent(equivalent(X_129,X_130),equivalent(X_126,X_130)),X_126)),X_127),equivalent(equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38),X_127)),equivalent(equivalent(equivalent(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C)),X_41),equivalent(X_38,X_41)),X_38)))) )],[refute_0_65,refute_0_66]) ).
cnf(refute_0_68,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_180,equivalent(equivalent(equivalent(X_180,X_181),equivalent(X_178,X_181)),X_178)),X_179),equivalent(equivalent(equivalent(equivalent(equivalent(X_175,equivalent(equivalent(equivalent(X_175,X_176),equivalent(X_177,X_176)),X_177)),X_183),equivalent(X_182,X_183)),X_182),X_179))),
inference(subst,[],[refute_0_67:[bind(A,$fot(X_175)),bind(B,$fot(X_176)),bind(C,$fot(X_177)),bind(X_126,$fot(X_178)),bind(X_127,$fot(X_179)),bind(X_129,$fot(X_180)),bind(X_130,$fot(X_181)),bind(X_38,$fot(X_182)),bind(X_41,$fot(X_183))]]) ).
cnf(refute_0_69,plain,
( ~ is_a_theorem(equivalent(equivalent(X_180,equivalent(equivalent(equivalent(X_180,X_181),equivalent(X_178,X_181)),X_178)),X_179))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_175,equivalent(equivalent(equivalent(X_175,X_176),equivalent(X_177,X_176)),X_177)),X_183),equivalent(X_182,X_183)),X_182),X_179)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_180,equivalent(equivalent(equivalent(X_180,X_181),equivalent(X_178,X_181)),X_178)),X_179),equivalent(equivalent(equivalent(equivalent(equivalent(X_175,equivalent(equivalent(equivalent(X_175,X_176),equivalent(X_177,X_176)),X_177)),X_183),equivalent(X_182,X_183)),X_182),X_179))) )],[refute_0_68,refute_0_64]) ).
cnf(refute_0_70,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498)),X_2495)),equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_2492,equivalent(equivalent(equivalent(X_2492,X_2493),equivalent(X_2494,X_2493)),X_2494)),X_2500),equivalent(X_2499,X_2500)),X_2499),equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498)))) ),
inference(subst,[],[refute_0_69:[bind(X_175,$fot(X_2492)),bind(X_176,$fot(X_2493)),bind(X_177,$fot(X_2494)),bind(X_178,$fot(X_2495)),bind(X_179,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498)))),bind(X_180,$fot(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495))),bind(X_181,$fot(X_2498)),bind(X_182,$fot(X_2499)),bind(X_183,$fot(X_2500))]]) ).
cnf(refute_0_71,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_2492,equivalent(equivalent(equivalent(X_2492,X_2493),equivalent(X_2494,X_2493)),X_2494)),X_2500),equivalent(X_2499,X_2500)),X_2499),equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498)),X_2495)),equivalent(equivalent(equivalent(equivalent(equivalent(X_696,X_695),equivalent(X_696,X_695)),X_2495),X_2498),equivalent(X_2495,X_2498)))) )],[refute_0_63,refute_0_70]) ).
cnf(refute_0_72,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)),X_2743),equivalent(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)),X_2743)),equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739))),equivalent(equivalent(equivalent(equivalent(equivalent(X_2745,X_2744),equivalent(X_2745,X_2744)),X_2740),X_2741),equivalent(X_2740,X_2741)))),
inference(subst,[],[refute_0_71:[bind(X_2492,$fot(X_2737)),bind(X_2493,$fot(X_2738)),bind(X_2494,$fot(X_2739)),bind(X_2495,$fot(X_2740)),bind(X_2498,$fot(X_2741)),bind(X_2499,$fot(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)))),bind(X_2500,$fot(X_2743)),bind(X_695,$fot(X_2744)),bind(X_696,$fot(X_2745))]]) ).
cnf(refute_0_73,plain,
is_a_theorem(equivalent(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)),equivalent(equivalent(equivalent(equivalent(equivalent(X_2745,X_2744),equivalent(X_2745,X_2744)),X_2740),X_2741),equivalent(X_2740,X_2741)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)),X_2743),equivalent(equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739)),X_2743)),equivalent(X_2737,equivalent(equivalent(equivalent(X_2737,X_2738),equivalent(X_2739,X_2738)),X_2739))),equivalent(equivalent(equivalent(equivalent(equivalent(X_2745,X_2744),equivalent(X_2745,X_2744)),X_2740),X_2741),equivalent(X_2740,X_2741)))) )],[refute_0_72,refute_0_62]) ).
cnf(refute_0_74,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754)),X_2757)),equivalent(equivalent(equivalent(equivalent(equivalent(X_2759,X_2758),equivalent(X_2759,X_2758)),equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754))),X_2757),equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754)),X_2757)))),
inference(subst,[],[refute_0_73:[bind(X_2737,$fot(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)))),bind(X_2738,$fot(X_2754)),bind(X_2739,$fot(X_2757)),bind(X_2740,$fot(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754)))),bind(X_2741,$fot(X_2757)),bind(X_2744,$fot(X_2758)),bind(X_2745,$fot(X_2759))]]) ).
cnf(refute_0_75,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_2759,X_2758),equivalent(X_2759,X_2758)),equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754))),X_2757)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754)),X_2757)),equivalent(equivalent(equivalent(equivalent(equivalent(X_2759,X_2758),equivalent(X_2759,X_2758)),equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754))),X_2757),equivalent(equivalent(equivalent(equivalent(equivalent(X_704,X_703),equivalent(X_704,X_703)),X_2754),equivalent(X_2757,X_2754)),X_2757)))) )],[refute_0_74,refute_0_61]) ).
cnf(refute_0_76,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_2763,X_2762),equivalent(X_2763,X_2762)),equivalent(equivalent(equivalent(equivalent(X_2765,X_2764),equivalent(X_2765,X_2764)),X_2760),equivalent(X_2761,X_2760))),X_2761)),
inference(subst,[],[refute_0_75:[bind(X_2754,$fot(X_2760)),bind(X_2757,$fot(X_2761)),bind(X_2758,$fot(X_2762)),bind(X_2759,$fot(X_2763)),bind(X_703,$fot(X_2764)),bind(X_704,$fot(X_2765))]]) ).
cnf(refute_0_77,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_2763,X_2762),equivalent(X_2763,X_2762)),equivalent(equivalent(equivalent(equivalent(X_2765,X_2764),equivalent(X_2765,X_2764)),X_2760),equivalent(X_2761,X_2760))),X_2761),B),equivalent(C,B)),C)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_2763,X_2762),equivalent(X_2763,X_2762)),equivalent(equivalent(equivalent(equivalent(X_2765,X_2764),equivalent(X_2765,X_2764)),X_2760),equivalent(X_2761,X_2760))),X_2761)) )],[refute_0_76,refute_0_60]) ).
cnf(refute_0_78,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042),equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042)),equivalent(X_3040,equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042))),X_3040)),
inference(subst,[],[refute_0_77:[bind(B,$fot(equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042))),bind(C,$fot(X_3040)),bind(X_2760,$fot(X_3041)),bind(X_2761,$fot(X_3042)),bind(X_2762,$fot(X_3043)),bind(X_2763,$fot(X_3044)),bind(X_2764,$fot(X_3045)),bind(X_2765,$fot(X_3046))]]) ).
cnf(refute_0_79,plain,
is_a_theorem(equivalent(equivalent(X_3040,equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042)),X_3040)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042),equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042)),equivalent(X_3040,equivalent(equivalent(equivalent(equivalent(X_3044,X_3043),equivalent(X_3044,X_3043)),equivalent(equivalent(equivalent(equivalent(X_3046,X_3045),equivalent(X_3046,X_3045)),X_3041),equivalent(X_3042,X_3041))),X_3042))),X_3040)) )],[refute_0_78,refute_0_59]) ).
cnf(refute_0_80,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))))),
inference(subst,[],[refute_0_79:[bind(X_3040,$fot(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))))),bind(X_3041,$fot(X_3050)),bind(X_3042,$fot(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),bind(X_3043,$fot(X_3050)),bind(X_3044,$fot(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),bind(X_3045,$fot(X_3052)),bind(X_3046,$fot(X_3053))]]) ).
cnf(refute_0_81,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))),equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050)),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),equivalent(equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050),X_3050))),equivalent(equivalent(equivalent(X_3053,X_3052),equivalent(X_3053,X_3052)),X_3050))))) )],[refute_0_80,refute_0_58]) ).
cnf(refute_0_82,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_3056,X_3055),equivalent(X_3056,X_3055)),X_3054),X_3054)),
inference(subst,[],[refute_0_81:[bind(X_3050,$fot(X_3054)),bind(X_3052,$fot(X_3055)),bind(X_3053,$fot(X_3056))]]) ).
cnf(refute_0_83,plain,
is_a_theorem(equivalent(X_3054,X_3054)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_3056,X_3055),equivalent(X_3056,X_3055)),X_3054),X_3054)) )],[refute_0_82,refute_0_57]) ).
cnf(refute_0_84,plain,
is_a_theorem(equivalent(a,a)),
inference(subst,[],[refute_0_83:[bind(X_3054,$fot(a))]]) ).
cnf(refute_0_85,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(equivalent(a,a)) )],[refute_0_84,prove_reflexivity]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL416-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.11/0.37 % Computer : n013.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 5 12:10:35 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 1.57/1.89 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.57/1.89
% 1.57/1.89 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 1.67/1.92
%------------------------------------------------------------------------------