%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL108-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n005.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:52 PM UTC 2026
% Result : Unsatisfiable 0.28s 0.54s
% Output : CNFRefutation 0.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 3
% Syntax : Number of clauses : 53 ( 32 unt; 0 nHn; 24 RR)
% Number of literals : 79 ( 0 equ; 27 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 324 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(equivalent(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(lg_27_1690,axiom,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),Z),equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),V6))),equivalent(Z,equivalent(equivalent(Y,X),V6)))) ).
cnf(prove_q_3,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(equivalent(a,b),equivalent(equivalent(b,a),c)),c)) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_6,X_7),X_8),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_6,X_7),X_8),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))),equivalent(X_8,equivalent(equivalent(X_7,X_6),X_4))))
| is_a_theorem(equivalent(X_8,equivalent(equivalent(X_7,X_6),X_4))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(equivalent(X_6,X_7),X_8),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))))),bind(Y,$fot(equivalent(X_8,equivalent(equivalent(X_7,X_6),X_4))))]]) ).
cnf(refute_0_1,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_6,X_7),X_8),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))),equivalent(X_8,equivalent(equivalent(X_7,X_6),X_4)))),
inference(subst,[],[lg_27_1690:[bind(U,$fot(X_2)),bind(V,$fot(X_3)),bind(V6,$fot(X_4)),bind(W,$fot(X_5)),bind(X,$fot(X_6)),bind(Y,$fot(X_7)),bind(Z,$fot(X_8))]]) ).
cnf(refute_0_2,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_6,X_7),X_8),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))))
| is_a_theorem(equivalent(X_8,equivalent(equivalent(X_7,X_6),X_4))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_6,X_7),X_8),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))),equivalent(X_8,equivalent(equivalent(X_7,X_6),X_4)))) )],[refute_0_1,refute_0_0]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_136,X_137),equivalent(equivalent(equivalent(X_139,X_137),equivalent(X_139,X_136)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4))),equivalent(equivalent(equivalent(X_140,X_141),equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_139,X_137),equivalent(X_139,X_136)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4)),equivalent(equivalent(X_137,X_136),X_4))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(equivalent(X_140,X_141))),bind(X_3,$fot(equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141))))),bind(X_6,$fot(X_136)),bind(X_7,$fot(X_137)),bind(X_8,$fot(equivalent(equivalent(equivalent(X_139,X_137),equivalent(X_139,X_136)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4))))]]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_97,X_94),equivalent(equivalent(X_96,X_97),equivalent(X_96,X_95))),equivalent(X_94,X_95)),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))))
| is_a_theorem(equivalent(equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4)),equivalent(equivalent(equivalent(X_94,X_95),equivalent(equivalent(X_97,X_94),equivalent(equivalent(X_96,X_97),equivalent(X_96,X_95)))),X_4))) ),
inference(subst,[],[refute_0_2:[bind(X_6,$fot(equivalent(equivalent(X_97,X_94),equivalent(equivalent(X_96,X_97),equivalent(X_96,X_95))))),bind(X_7,$fot(equivalent(X_94,X_95))),bind(X_8,$fot(equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))))]]) ).
cnf(refute_0_5,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4))),equivalent(equivalent(X_24,X_23),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4)),equivalent(equivalent(equivalent(X_25,X_23),equivalent(X_25,X_24)),X_4))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(X_24)),bind(X_3,$fot(X_23)),bind(X_6,$fot(equivalent(X_25,X_24))),bind(X_7,$fot(equivalent(X_25,X_23))),bind(X_8,$fot(equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4))))]]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_16,X_17),equivalent(equivalent(equivalent(X_18,X_17),equivalent(X_18,X_16)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4))),equivalent(equivalent(equivalent(X_22,X_19),equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_18,X_17),equivalent(X_18,X_16)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4)),equivalent(equivalent(X_17,X_16),X_4))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(equivalent(X_22,X_19))),bind(X_3,$fot(equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19)))),bind(X_6,$fot(X_16)),bind(X_7,$fot(X_17)),bind(X_8,$fot(equivalent(equivalent(equivalent(X_18,X_17),equivalent(X_18,X_16)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4))))]]) ).
cnf(refute_0_7,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_12,X_9),equivalent(X_12,X_10)),equivalent(X_9,X_10)),equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),X_11))),equivalent(equivalent(X_9,X_10),equivalent(equivalent(equivalent(X_12,X_10),equivalent(X_12,X_9)),X_11)))),
inference(subst,[],[lg_27_1690:[bind(V6,$fot(X_11)),bind(X,$fot(equivalent(X_12,X_9))),bind(Y,$fot(equivalent(X_12,X_10))),bind(Z,$fot(equivalent(X_9,X_10)))]]) ).
cnf(refute_0_8,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_12,X_9),equivalent(X_12,X_10)),equivalent(X_9,X_10)),equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),X_11))),equivalent(equivalent(X_9,X_10),equivalent(equivalent(equivalent(X_12,X_10),equivalent(X_12,X_9)),X_11))))
| is_a_theorem(equivalent(equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),X_11)),equivalent(equivalent(equivalent(X_9,X_10),equivalent(equivalent(X_12,X_9),equivalent(X_12,X_10))),X_11))) ),
inference(subst,[],[refute_0_2:[bind(X_2,$fot(X_9)),bind(X_3,$fot(X_10)),bind(X_4,$fot(X_11)),bind(X_5,$fot(X_12)),bind(X_6,$fot(equivalent(equivalent(X_12,X_9),equivalent(X_12,X_10)))),bind(X_7,$fot(equivalent(X_9,X_10))),bind(X_8,$fot(equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),X_11))))]]) ).
cnf(refute_0_9,plain,
is_a_theorem(equivalent(equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),X_11)),equivalent(equivalent(equivalent(X_9,X_10),equivalent(equivalent(X_12,X_9),equivalent(X_12,X_10))),X_11))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_12,X_9),equivalent(X_12,X_10)),equivalent(X_9,X_10)),equivalent(equivalent(U,V),equivalent(equivalent(equivalent(W,V),equivalent(W,U)),X_11))),equivalent(equivalent(X_9,X_10),equivalent(equivalent(equivalent(X_12,X_10),equivalent(X_12,X_9)),X_11)))) )],[refute_0_7,refute_0_8]) ).
cnf(refute_0_10,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_16,X_17),equivalent(equivalent(equivalent(X_18,X_17),equivalent(X_18,X_16)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4))),equivalent(equivalent(equivalent(X_22,X_19),equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4)))),
inference(subst,[],[refute_0_9:[bind(U,$fot(X_16)),bind(V,$fot(X_17)),bind(W,$fot(X_18)),bind(X_10,$fot(X_19)),bind(X_11,$fot(equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4))),bind(X_12,$fot(X_21)),bind(X_9,$fot(X_22))]]) ).
cnf(refute_0_11,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_18,X_17),equivalent(X_18,X_16)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4)),equivalent(equivalent(X_17,X_16),X_4))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_16,X_17),equivalent(equivalent(equivalent(X_18,X_17),equivalent(X_18,X_16)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4))),equivalent(equivalent(equivalent(X_22,X_19),equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_21,X_22),equivalent(X_21,X_19))),equivalent(X_5,equivalent(X_22,X_19))),X_4)))) )],[refute_0_10,refute_0_6]) ).
cnf(refute_0_12,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4))),equivalent(equivalent(X_24,X_23),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4)))),
inference(subst,[],[refute_0_11:[bind(X_16,$fot(X_23)),bind(X_17,$fot(X_24)),bind(X_18,$fot(X_25)),bind(X_19,$fot(X_26)),bind(X_21,$fot(X_27)),bind(X_22,$fot(X_28)),bind(X_4,$fot(equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4))),bind(X_5,$fot(X_30))]]) ).
cnf(refute_0_13,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4)),equivalent(equivalent(equivalent(X_25,X_23),equivalent(X_25,X_24)),X_4))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4))),equivalent(equivalent(X_24,X_23),equivalent(equivalent(equivalent(X_5,X_23),equivalent(X_5,X_24)),X_4)))) )],[refute_0_12,refute_0_5]) ).
cnf(refute_0_14,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(equivalent(X_85,X_28),equivalent(X_85,X_83))),equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_28,X_83))),equivalent(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(equivalent(X_85,X_28),equivalent(X_85,X_83))),X_86)),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_87,equivalent(X_85,X_83))),X_86))),
inference(subst,[],[refute_0_13:[bind(X_23,$fot(equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83)))),bind(X_24,$fot(equivalent(X_85,X_83))),bind(X_25,$fot(X_87)),bind(X_26,$fot(X_83)),bind(X_27,$fot(X_85)),bind(X_30,$fot(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))))),bind(X_4,$fot(X_86)),bind(X_5,$fot(equivalent(X_85,X_28)))]]) ).
cnf(refute_0_15,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_29)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_29)),equivalent(equivalent(X_24,X_23),X_29)))
| is_a_theorem(equivalent(equivalent(X_24,X_23),X_29)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_29)))),bind(Y,$fot(equivalent(equivalent(X_24,X_23),X_29)))]]) ).
cnf(refute_0_16,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_29)),equivalent(equivalent(X_24,X_23),X_29))),
inference(subst,[],[refute_0_11:[bind(X_16,$fot(X_23)),bind(X_17,$fot(X_24)),bind(X_18,$fot(X_25)),bind(X_19,$fot(X_26)),bind(X_21,$fot(X_27)),bind(X_22,$fot(X_28)),bind(X_4,$fot(X_29)),bind(X_5,$fot(X_30))]]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_29)))
| is_a_theorem(equivalent(equivalent(X_24,X_23),X_29)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_25,X_24),equivalent(X_25,X_23)),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_29)),equivalent(equivalent(X_24,X_23),X_29))) )],[refute_0_16,refute_0_15]) ).
cnf(refute_0_18,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(equivalent(X_85,X_28),equivalent(X_85,X_83))),equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_28,X_83))),equivalent(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(equivalent(X_85,X_28),equivalent(X_85,X_83))),X_86)),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_87,equivalent(X_85,X_83))),X_86)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_28,X_83)),X_86),X_86)) ),
inference(subst,[],[refute_0_17:[bind(X_23,$fot(X_86)),bind(X_24,$fot(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_28,X_83)))),bind(X_25,$fot(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(equivalent(X_85,X_28),equivalent(X_85,X_83))))),bind(X_26,$fot(X_83)),bind(X_27,$fot(X_84)),bind(X_28,$fot(X_85)),bind(X_29,$fot(X_86)),bind(X_30,$fot(X_87))]]) ).
cnf(refute_0_19,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_28,X_83)),X_86),X_86)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(equivalent(X_85,X_28),equivalent(X_85,X_83))),equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_28,X_83))),equivalent(equivalent(equivalent(equivalent(X_85,X_28),equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(equivalent(X_85,X_28),equivalent(X_85,X_83))),X_86)),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_87,equivalent(X_85,X_83))),X_86))) )],[refute_0_14,refute_0_18]) ).
cnf(refute_0_20,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_97,X_94),equivalent(equivalent(X_96,X_97),equivalent(X_96,X_95))),equivalent(X_94,X_95)),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4)))),
inference(subst,[],[refute_0_19:[bind(X_28,$fot(X_94)),bind(X_83,$fot(X_95)),bind(X_84,$fot(X_96)),bind(X_85,$fot(X_97)),bind(X_86,$fot(equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))))]]) ).
cnf(refute_0_21,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4)),equivalent(equivalent(equivalent(X_94,X_95),equivalent(equivalent(X_97,X_94),equivalent(equivalent(X_96,X_97),equivalent(X_96,X_95)))),X_4))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_97,X_94),equivalent(equivalent(X_96,X_97),equivalent(X_96,X_95))),equivalent(X_94,X_95)),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4))),equivalent(equivalent(X_2,X_3),equivalent(equivalent(equivalent(X_5,X_3),equivalent(X_5,X_2)),X_4)))) )],[refute_0_20,refute_0_4]) ).
cnf(refute_0_22,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_136,X_137),equivalent(equivalent(equivalent(X_139,X_137),equivalent(X_139,X_136)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4))),equivalent(equivalent(equivalent(X_140,X_141),equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4)))),
inference(subst,[],[refute_0_21:[bind(X_2,$fot(X_136)),bind(X_3,$fot(X_137)),bind(X_4,$fot(equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4))),bind(X_5,$fot(X_139)),bind(X_94,$fot(X_140)),bind(X_95,$fot(X_141)),bind(X_96,$fot(X_142)),bind(X_97,$fot(X_143))]]) ).
cnf(refute_0_23,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_139,X_137),equivalent(X_139,X_136)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4)),equivalent(equivalent(X_137,X_136),X_4))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_136,X_137),equivalent(equivalent(equivalent(X_139,X_137),equivalent(X_139,X_136)),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4))),equivalent(equivalent(equivalent(X_140,X_141),equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(equivalent(equivalent(X_5,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_5,equivalent(X_140,X_141))),X_4)))) )],[refute_0_22,refute_0_3]) ).
cnf(refute_0_24,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(X_140,X_141))),equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234)))),equivalent(equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(X_140,X_141))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234))),equivalent(equivalent(equivalent(X_233,equivalent(X_140,X_141)),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234)))),
inference(subst,[],[refute_0_23:[bind(X_136,$fot(equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234)))),bind(X_137,$fot(equivalent(X_233,equivalent(X_140,X_141)))),bind(X_139,$fot(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))))),bind(X_4,$fot(equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234))),bind(X_5,$fot(X_233))]]) ).
cnf(refute_0_25,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_93,equivalent(equivalent(X_88,equivalent(X_90,X_91)),equivalent(X_88,equivalent(X_90,X_89)))),equivalent(X_93,equivalent(X_91,X_89))),X_92))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_93,equivalent(equivalent(X_88,equivalent(X_90,X_91)),equivalent(X_88,equivalent(X_90,X_89)))),equivalent(X_93,equivalent(X_91,X_89))),X_92),X_92))
| is_a_theorem(X_92) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(equivalent(X_93,equivalent(equivalent(X_88,equivalent(X_90,X_91)),equivalent(X_88,equivalent(X_90,X_89)))),equivalent(X_93,equivalent(X_91,X_89))),X_92))),bind(Y,$fot(X_92))]]) ).
cnf(refute_0_26,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83)))),equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(X_85,X_83)))),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83)))),X_86)),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_87,equivalent(X_85,X_83))),X_86))),
inference(subst,[],[refute_0_11:[bind(X_16,$fot(equivalent(X_87,equivalent(X_85,X_83)))),bind(X_17,$fot(equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))))),bind(X_18,$fot(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))))),bind(X_19,$fot(equivalent(X_84,X_83))),bind(X_22,$fot(equivalent(X_84,X_85))),bind(X_4,$fot(X_86)),bind(X_5,$fot(X_87))]]) ).
cnf(refute_0_27,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83)))),equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(X_85,X_83)))),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83)))),X_86)),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_87,equivalent(X_85,X_83))),X_86)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(X_85,X_83))),X_86),X_86)) ),
inference(subst,[],[refute_0_17:[bind(X_23,$fot(X_86)),bind(X_24,$fot(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(X_85,X_83))))),bind(X_25,$fot(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83)))))),bind(X_26,$fot(X_83)),bind(X_27,$fot(X_84)),bind(X_28,$fot(X_85)),bind(X_29,$fot(X_86)),bind(X_30,$fot(X_87))]]) ).
cnf(refute_0_28,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(X_85,X_83))),X_86),X_86)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83)))),equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(X_85,X_83)))),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_21,equivalent(X_84,X_85)),equivalent(X_21,equivalent(X_84,X_83)))),equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83)))),X_86)),equivalent(equivalent(equivalent(X_87,equivalent(equivalent(X_84,X_85),equivalent(X_84,X_83))),equivalent(X_87,equivalent(X_85,X_83))),X_86))) )],[refute_0_26,refute_0_27]) ).
cnf(refute_0_29,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_93,equivalent(equivalent(X_88,equivalent(X_90,X_91)),equivalent(X_88,equivalent(X_90,X_89)))),equivalent(X_93,equivalent(X_91,X_89))),X_92),X_92)),
inference(subst,[],[refute_0_28:[bind(X_21,$fot(X_88)),bind(X_83,$fot(X_89)),bind(X_84,$fot(X_90)),bind(X_85,$fot(X_91)),bind(X_86,$fot(X_92)),bind(X_87,$fot(X_93))]]) ).
cnf(refute_0_30,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_93,equivalent(equivalent(X_88,equivalent(X_90,X_91)),equivalent(X_88,equivalent(X_90,X_89)))),equivalent(X_93,equivalent(X_91,X_89))),X_92))
| is_a_theorem(X_92) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_93,equivalent(equivalent(X_88,equivalent(X_90,X_91)),equivalent(X_88,equivalent(X_90,X_89)))),equivalent(X_93,equivalent(X_91,X_89))),X_92),X_92)) )],[refute_0_29,refute_0_25]) ).
cnf(refute_0_31,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(X_140,X_141))),equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234)))),equivalent(equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(X_140,X_141))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234))),equivalent(equivalent(equivalent(X_233,equivalent(X_140,X_141)),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234))))
| is_a_theorem(equivalent(equivalent(equivalent(X_233,equivalent(X_140,X_141)),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234))) ),
inference(subst,[],[refute_0_30:[bind(X_88,$fot(X_233)),bind(X_89,$fot(X_234)),bind(X_90,$fot(equivalent(X_143,X_140))),bind(X_91,$fot(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),bind(X_92,$fot(equivalent(equivalent(equivalent(X_233,equivalent(X_140,X_141)),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234)))),bind(X_93,$fot(equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(X_140,X_141)))))]]) ).
cnf(refute_0_32,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_233,equivalent(X_140,X_141)),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(X_140,X_141))),equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234)))),equivalent(equivalent(equivalent(X_233,equivalent(equivalent(X_143,X_140),equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)))),equivalent(X_233,equivalent(X_140,X_141))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234))),equivalent(equivalent(equivalent(X_233,equivalent(X_140,X_141)),equivalent(X_233,equivalent(equivalent(X_143,X_140),X_234))),equivalent(equivalent(equivalent(X_142,X_143),equivalent(X_142,X_141)),X_234)))) )],[refute_0_24,refute_0_31]) ).
cnf(refute_0_33,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_140,X_143),equivalent(X_140,X_141)),equivalent(equivalent(X_140,X_143),equivalent(equivalent(X_143,X_140),X_345))),equivalent(equivalent(equivalent(X_140,X_143),equivalent(X_140,X_141)),X_345))),
inference(subst,[],[refute_0_32:[bind(X_142,$fot(X_140)),bind(X_233,$fot(equivalent(X_140,X_143))),bind(X_234,$fot(X_345))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(equivalent(equivalent(X_339,X_340),equivalent(X_339,X_338)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X_339,X_340),equivalent(X_339,X_338)),equivalent(X_340,X_338)))
| is_a_theorem(equivalent(X_340,X_338)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(X_339,X_340),equivalent(X_339,X_338)))),bind(Y,$fot(equivalent(X_340,X_338)))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_333,equivalent(equivalent(X_331,equivalent(X_337,equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)))),equivalent(X_331,equivalent(X_337,equivalent(X_336,X_334))))),equivalent(X_333,equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334)))),equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334))))
| is_a_theorem(equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334))) ),
inference(subst,[],[refute_0_30:[bind(X_88,$fot(X_331)),bind(X_89,$fot(equivalent(X_336,X_334))),bind(X_90,$fot(X_337)),bind(X_91,$fot(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)))),bind(X_92,$fot(equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334)))),bind(X_93,$fot(X_333))]]) ).
cnf(refute_0_36,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_248,equivalent(X_250,equivalent(equivalent(X_245,equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26)))),equivalent(X_245,equivalent(X_30,equivalent(X_28,X_26)))))),equivalent(X_248,equivalent(X_250,X_249))),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_249)))
| is_a_theorem(equivalent(equivalent(equivalent(X_250,equivalent(equivalent(X_245,equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26)))),equivalent(X_245,equivalent(X_30,equivalent(X_28,X_26))))),equivalent(X_250,X_249)),X_249)) ),
inference(subst,[],[refute_0_17:[bind(X_23,$fot(equivalent(X_250,X_249))),bind(X_24,$fot(equivalent(X_250,equivalent(equivalent(X_245,equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26)))),equivalent(X_245,equivalent(X_30,equivalent(X_28,X_26))))))),bind(X_25,$fot(X_248)),bind(X_29,$fot(X_249))]]) ).
cnf(refute_0_37,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234)))),equivalent(equivalent(X,Y),equivalent(equivalent(equivalent(W,Y),equivalent(W,X)),X_234))),equivalent(equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234))),equivalent(equivalent(Y,X),X_234)))),
inference(subst,[],[lg_27_1690:[bind(U,$fot(X)),bind(V,$fot(Y)),bind(V6,$fot(X_234)),bind(Z,$fot(equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234)))))]]) ).
cnf(refute_0_38,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234)))),equivalent(equivalent(X,Y),equivalent(equivalent(equivalent(W,Y),equivalent(W,X)),X_234))),equivalent(equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234))),equivalent(equivalent(Y,X),X_234))))
| is_a_theorem(equivalent(equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234))),equivalent(equivalent(Y,X),X_234))) ),
inference(subst,[],[refute_0_30:[bind(X_88,$fot(X_233)),bind(X_89,$fot(X_234)),bind(X_90,$fot(X_235)),bind(X_91,$fot(equivalent(equivalent(W,Y),equivalent(W,X)))),bind(X_92,$fot(equivalent(equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234))),equivalent(equivalent(Y,X),X_234)))),bind(X_93,$fot(equivalent(X,Y)))]]) ).
cnf(refute_0_39,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234))),equivalent(equivalent(Y,X),X_234))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X,Y),equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234)))),equivalent(equivalent(X,Y),equivalent(equivalent(equivalent(W,Y),equivalent(W,X)),X_234))),equivalent(equivalent(equivalent(X_233,equivalent(X_235,equivalent(equivalent(W,Y),equivalent(W,X)))),equivalent(X_233,equivalent(X_235,X_234))),equivalent(equivalent(Y,X),X_234)))) )],[refute_0_37,refute_0_38]) ).
cnf(refute_0_40,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_248,equivalent(X_250,equivalent(equivalent(X_245,equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26)))),equivalent(X_245,equivalent(X_30,equivalent(X_28,X_26)))))),equivalent(X_248,equivalent(X_250,X_249))),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_249))),
inference(subst,[],[refute_0_39:[bind(W,$fot(X_245)),bind(X,$fot(equivalent(X_30,equivalent(X_28,X_26)))),bind(Y,$fot(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))))),bind(X_233,$fot(X_248)),bind(X_234,$fot(X_249)),bind(X_235,$fot(X_250))]]) ).
cnf(refute_0_41,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_250,equivalent(equivalent(X_245,equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26)))),equivalent(X_245,equivalent(X_30,equivalent(X_28,X_26))))),equivalent(X_250,X_249)),X_249)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_248,equivalent(X_250,equivalent(equivalent(X_245,equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26)))),equivalent(X_245,equivalent(X_30,equivalent(X_28,X_26)))))),equivalent(X_248,equivalent(X_250,X_249))),equivalent(equivalent(equivalent(X_30,equivalent(equivalent(X_27,X_28),equivalent(X_27,X_26))),equivalent(X_30,equivalent(X_28,X_26))),X_249))) )],[refute_0_40,refute_0_36]) ).
cnf(refute_0_42,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_333,equivalent(equivalent(X_331,equivalent(X_337,equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)))),equivalent(X_331,equivalent(X_337,equivalent(X_336,X_334))))),equivalent(X_333,equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334)))),equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334)))),
inference(subst,[],[refute_0_41:[bind(X_245,$fot(X_331)),bind(X_249,$fot(equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334)))),bind(X_250,$fot(X_333)),bind(X_26,$fot(X_334)),bind(X_27,$fot(X_335)),bind(X_28,$fot(X_336)),bind(X_30,$fot(X_337))]]) ).
cnf(refute_0_43,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_333,equivalent(equivalent(X_331,equivalent(X_337,equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)))),equivalent(X_331,equivalent(X_337,equivalent(X_336,X_334))))),equivalent(X_333,equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334)))),equivalent(equivalent(equivalent(X_335,X_336),equivalent(X_335,X_334)),equivalent(X_336,X_334)))) )],[refute_0_42,refute_0_35]) ).
cnf(refute_0_44,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_339,X_340),equivalent(X_339,X_338)),equivalent(X_340,X_338))),
inference(subst,[],[refute_0_43:[bind(X_334,$fot(X_338)),bind(X_335,$fot(X_339)),bind(X_336,$fot(X_340))]]) ).
cnf(refute_0_45,plain,
( ~ is_a_theorem(equivalent(equivalent(X_339,X_340),equivalent(X_339,X_338)))
| is_a_theorem(equivalent(X_340,X_338)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_339,X_340),equivalent(X_339,X_338)),equivalent(X_340,X_338))) )],[refute_0_44,refute_0_34]) ).
cnf(refute_0_46,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_140,X_143),equivalent(X_140,X_141)),equivalent(equivalent(X_140,X_143),equivalent(equivalent(X_143,X_140),X_345))),equivalent(equivalent(equivalent(X_140,X_143),equivalent(X_140,X_141)),X_345)))
| is_a_theorem(equivalent(equivalent(equivalent(X_140,X_143),equivalent(equivalent(X_143,X_140),X_345)),X_345)) ),
inference(subst,[],[refute_0_45:[bind(X_338,$fot(X_345)),bind(X_339,$fot(equivalent(equivalent(X_140,X_143),equivalent(X_140,X_141)))),bind(X_340,$fot(equivalent(equivalent(X_140,X_143),equivalent(equivalent(X_143,X_140),X_345))))]]) ).
cnf(refute_0_47,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_140,X_143),equivalent(equivalent(X_143,X_140),X_345)),X_345)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_140,X_143),equivalent(X_140,X_141)),equivalent(equivalent(X_140,X_143),equivalent(equivalent(X_143,X_140),X_345))),equivalent(equivalent(equivalent(X_140,X_143),equivalent(X_140,X_141)),X_345))) )],[refute_0_33,refute_0_46]) ).
cnf(refute_0_48,plain,
is_a_theorem(equivalent(equivalent(equivalent(a,b),equivalent(equivalent(b,a),c)),c)),
inference(subst,[],[refute_0_47:[bind(X_140,$fot(a)),bind(X_143,$fot(b)),bind(X_345,$fot(c))]]) ).
cnf(refute_0_49,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(a,b),equivalent(equivalent(b,a),c)),c)) )],[refute_0_48,prove_q_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL108-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : metis --show proof --show saturation %s
% 0.11/0.37 % Computer : n005.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 16:09:05 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.28/0.54 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.28/0.54
% 0.28/0.54 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 0.28/0.60
%------------------------------------------------------------------------------