%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : LCL010-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:39 PM UTC 2026
% Result : Unsatisfiable 9.56s 9.88s
% Output : CNFRefutation 9.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 3
% Syntax : Number of clauses : 116 ( 67 unt; 0 nHn; 23 RR)
% Number of literals : 177 ( 0 equ; 62 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 7 ( 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 : 390 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(condensed_detachment,axiom,
( ~ is_a_theorem(equivalent(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ) ).
cnf(yqf,axiom,
is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(X,Z),equivalent(Z,Y)))) ).
cnf(prove_yql,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(a,b),equivalent(equivalent(c,b),equivalent(a,c)))) ).
cnf(refute_0_0,plain,
( ~ is_a_theorem(equivalent(X_381,X_380))
| ~ is_a_theorem(equivalent(equivalent(X_381,X_380),equivalent(X_380,X_381)))
| is_a_theorem(equivalent(X_380,X_381)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(X_381,X_380))),bind(Y,$fot(equivalent(X_380,X_381)))]]) ).
cnf(refute_0_1,plain,
( ~ is_a_theorem(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)),equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24))))
| is_a_theorem(equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)))),bind(Y,$fot(equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24))))]]) ).
cnf(refute_0_2,plain,
is_a_theorem(equivalent(equivalent(X_19,X_20),equivalent(equivalent(X_19,Z),equivalent(Z,X_20)))),
inference(subst,[],[yqf:[bind(X,$fot(X_19)),bind(Y,$fot(X_20))]]) ).
cnf(refute_0_3,plain,
( ~ is_a_theorem(equivalent(equivalent(X_8,X_9),X_11))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X_8,X_9),X_11),equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9)))))
| is_a_theorem(equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(X_8,X_9),X_11))),bind(Y,$fot(equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9)))))]]) ).
cnf(refute_0_4,plain,
( ~ is_a_theorem(equivalent(X,Y))
| ~ is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(X,Z),equivalent(Z,Y))))
| is_a_theorem(equivalent(equivalent(X,Z),equivalent(Z,Y))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(X,Y))),bind(Y,$fot(equivalent(equivalent(X,Z),equivalent(Z,Y))))]]) ).
cnf(refute_0_5,plain,
( ~ is_a_theorem(equivalent(X,Y))
| is_a_theorem(equivalent(equivalent(X,Z),equivalent(Z,Y))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(X,Z),equivalent(Z,Y)))) )],[yqf,refute_0_4]) ).
cnf(refute_0_6,plain,
( ~ is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(X,Z),equivalent(Z,Y))))
| is_a_theorem(equivalent(equivalent(equivalent(X,Y),X_7),equivalent(X_7,equivalent(equivalent(X,Z),equivalent(Z,Y))))) ),
inference(subst,[],[refute_0_5:[bind(X,$fot(equivalent(X,Y))),bind(Y,$fot(equivalent(equivalent(X,Z),equivalent(Z,Y)))),bind(Z,$fot(X_7))]]) ).
cnf(refute_0_7,plain,
is_a_theorem(equivalent(equivalent(equivalent(X,Y),X_7),equivalent(X_7,equivalent(equivalent(X,Z),equivalent(Z,Y))))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(X,Z),equivalent(Z,Y)))) )],[yqf,refute_0_6]) ).
cnf(refute_0_8,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_8,X_9),X_11),equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9))))),
inference(subst,[],[refute_0_7:[bind(X,$fot(X_8)),bind(Y,$fot(X_9)),bind(Z,$fot(X_10)),bind(X_7,$fot(X_11))]]) ).
cnf(refute_0_9,plain,
( ~ is_a_theorem(equivalent(equivalent(X_8,X_9),X_11))
| is_a_theorem(equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9)))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_8,X_9),X_11),equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9))))) )],[refute_0_8,refute_0_3]) ).
cnf(refute_0_10,plain,
( ~ is_a_theorem(equivalent(equivalent(X_19,X_20),equivalent(equivalent(X_19,Z),equivalent(Z,X_20))))
| is_a_theorem(equivalent(equivalent(equivalent(X_19,Z),equivalent(Z,X_20)),equivalent(equivalent(X_19,X_17),equivalent(X_17,X_20)))) ),
inference(subst,[],[refute_0_9:[bind(X_10,$fot(X_17)),bind(X_11,$fot(equivalent(equivalent(X_19,Z),equivalent(Z,X_20)))),bind(X_8,$fot(X_19)),bind(X_9,$fot(X_20))]]) ).
cnf(refute_0_11,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_19,Z),equivalent(Z,X_20)),equivalent(equivalent(X_19,X_17),equivalent(X_17,X_20)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_19,X_20),equivalent(equivalent(X_19,Z),equivalent(Z,X_20)))) )],[refute_0_2,refute_0_10]) ).
cnf(refute_0_12,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)),equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24)))),
inference(subst,[],[refute_0_11:[bind(Z,$fot(X_21)),bind(X_17,$fot(X_22)),bind(X_19,$fot(X_23)),bind(X_20,$fot(X_24))]]) ).
cnf(refute_0_13,plain,
( ~ is_a_theorem(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)))
| is_a_theorem(equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)),equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24)))) )],[refute_0_12,refute_0_1]) ).
cnf(refute_0_14,plain,
( ~ is_a_theorem(equivalent(equivalent(X_378,X_378),equivalent(X_378,X_378)))
| is_a_theorem(equivalent(equivalent(X_378,X_22),equivalent(X_22,X_378))) ),
inference(subst,[],[refute_0_13:[bind(X_21,$fot(X_378)),bind(X_23,$fot(X_378)),bind(X_24,$fot(X_378))]]) ).
cnf(refute_0_15,plain,
( ~ is_a_theorem(equivalent(equivalent(X_145,X_145),X_146))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X_145,X_145),X_146),equivalent(X_146,equivalent(X_147,X_147))))
| is_a_theorem(equivalent(X_146,equivalent(X_147,X_147))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(X_145,X_145),X_146))),bind(Y,$fot(equivalent(X_146,equivalent(X_147,X_147))))]]) ).
cnf(refute_0_16,plain,
is_a_theorem(equivalent(equivalent(equivalent(Z,Z),equivalent(Z,X_20)),equivalent(equivalent(Z,X_20),equivalent(X_20,X_20)))),
inference(subst,[],[refute_0_11:[bind(X_17,$fot(X_20)),bind(X_19,$fot(Z))]]) ).
cnf(refute_0_17,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(Z,Z),equivalent(Z,X_20)),equivalent(equivalent(Z,X_20),equivalent(X_20,X_20))))
| is_a_theorem(equivalent(equivalent(equivalent(Z,Z),X_136),equivalent(X_136,equivalent(X_20,X_20)))) ),
inference(subst,[],[refute_0_13:[bind(X_21,$fot(equivalent(Z,X_20))),bind(X_22,$fot(X_136)),bind(X_23,$fot(equivalent(Z,Z))),bind(X_24,$fot(equivalent(X_20,X_20)))]]) ).
cnf(refute_0_18,plain,
is_a_theorem(equivalent(equivalent(equivalent(Z,Z),X_136),equivalent(X_136,equivalent(X_20,X_20)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(Z,Z),equivalent(Z,X_20)),equivalent(equivalent(Z,X_20),equivalent(X_20,X_20)))) )],[refute_0_16,refute_0_17]) ).
cnf(refute_0_19,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_145,X_145),X_146),equivalent(X_146,equivalent(X_147,X_147)))),
inference(subst,[],[refute_0_18:[bind(Z,$fot(X_145)),bind(X_136,$fot(X_146)),bind(X_20,$fot(X_147))]]) ).
cnf(refute_0_20,plain,
( ~ is_a_theorem(equivalent(equivalent(X_145,X_145),X_146))
| is_a_theorem(equivalent(X_146,equivalent(X_147,X_147))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_145,X_145),X_146),equivalent(X_146,equivalent(X_147,X_147)))) )],[refute_0_19,refute_0_15]) ).
cnf(refute_0_21,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_375,X_375),equivalent(X_375,X_375)),equivalent(X_377,X_377)))
| is_a_theorem(equivalent(equivalent(X_377,X_377),equivalent(X_147,X_147))) ),
inference(subst,[],[refute_0_20:[bind(X_145,$fot(equivalent(X_375,X_375))),bind(X_146,$fot(equivalent(X_377,X_377)))]]) ).
cnf(refute_0_22,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_19,X_19),equivalent(X_19,X_19)),equivalent(equivalent(X_19,X_17),equivalent(X_17,X_19)))),
inference(subst,[],[refute_0_11:[bind(Z,$fot(X_19)),bind(X_20,$fot(X_19))]]) ).
cnf(refute_0_23,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_19,X_19),equivalent(X_19,X_19)),equivalent(equivalent(X_19,X_17),equivalent(X_17,X_19))))
| is_a_theorem(equivalent(equivalent(equivalent(X_19,X_17),equivalent(X_17,X_19)),equivalent(X_374,X_374))) ),
inference(subst,[],[refute_0_20:[bind(X_145,$fot(equivalent(X_19,X_19))),bind(X_146,$fot(equivalent(equivalent(X_19,X_17),equivalent(X_17,X_19)))),bind(X_147,$fot(X_374))]]) ).
cnf(refute_0_24,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_19,X_17),equivalent(X_17,X_19)),equivalent(X_374,X_374))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_19,X_19),equivalent(X_19,X_19)),equivalent(equivalent(X_19,X_17),equivalent(X_17,X_19)))) )],[refute_0_22,refute_0_23]) ).
cnf(refute_0_25,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_375,X_375),equivalent(X_375,X_375)),equivalent(X_377,X_377))),
inference(subst,[],[refute_0_24:[bind(X_17,$fot(X_375)),bind(X_19,$fot(X_375)),bind(X_374,$fot(X_377))]]) ).
cnf(refute_0_26,plain,
is_a_theorem(equivalent(equivalent(X_377,X_377),equivalent(X_147,X_147))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_375,X_375),equivalent(X_375,X_375)),equivalent(X_377,X_377))) )],[refute_0_25,refute_0_21]) ).
cnf(refute_0_27,plain,
is_a_theorem(equivalent(equivalent(X_378,X_378),equivalent(X_378,X_378))),
inference(subst,[],[refute_0_26:[bind(X_147,$fot(X_378)),bind(X_377,$fot(X_378))]]) ).
cnf(refute_0_28,plain,
is_a_theorem(equivalent(equivalent(X_378,X_22),equivalent(X_22,X_378))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_378,X_378),equivalent(X_378,X_378))) )],[refute_0_27,refute_0_14]) ).
cnf(refute_0_29,plain,
is_a_theorem(equivalent(equivalent(X_381,X_380),equivalent(X_380,X_381))),
inference(subst,[],[refute_0_28:[bind(X_22,$fot(X_380)),bind(X_378,$fot(X_381))]]) ).
cnf(refute_0_30,plain,
( ~ is_a_theorem(equivalent(X_381,X_380))
| is_a_theorem(equivalent(X_380,X_381)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_381,X_380),equivalent(X_380,X_381))) )],[refute_0_29,refute_0_0]) ).
cnf(refute_0_31,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_5285,X_5284),equivalent(X_5283,X_5285)),equivalent(X_5283,X_5284)))
| is_a_theorem(equivalent(equivalent(X_5283,X_5284),equivalent(equivalent(X_5285,X_5284),equivalent(X_5283,X_5285)))) ),
inference(subst,[],[refute_0_30:[bind(X_380,$fot(equivalent(X_5283,X_5284))),bind(X_381,$fot(equivalent(equivalent(X_5285,X_5284),equivalent(X_5283,X_5285))))]]) ).
cnf(refute_0_32,plain,
( ~ is_a_theorem(equivalent(X_794,equivalent(X_795,X_795)))
| ~ is_a_theorem(equivalent(equivalent(X_794,equivalent(X_795,X_795)),X_794))
| is_a_theorem(X_794) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(X_794,equivalent(X_795,X_795)))),bind(Y,$fot(X_794))]]) ).
cnf(refute_0_33,plain,
( ~ is_a_theorem(equivalent(X_792,equivalent(X_792,equivalent(X_793,X_793))))
| is_a_theorem(equivalent(equivalent(X_792,equivalent(X_793,X_793)),X_792)) ),
inference(subst,[],[refute_0_30:[bind(X_380,$fot(equivalent(X_792,equivalent(X_793,X_793)))),bind(X_381,$fot(X_792))]]) ).
cnf(refute_0_34,plain,
( ~ is_a_theorem(equivalent(X_789,X_789))
| ~ is_a_theorem(equivalent(equivalent(X_789,X_789),equivalent(X_790,equivalent(X_790,equivalent(X_791,X_791)))))
| is_a_theorem(equivalent(X_790,equivalent(X_790,equivalent(X_791,X_791)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(X_789,X_789))),bind(Y,$fot(equivalent(X_790,equivalent(X_790,equivalent(X_791,X_791)))))]]) ).
cnf(refute_0_35,plain,
( ~ is_a_theorem(equivalent(equivalent(X_607,equivalent(X_607,equivalent(X_608,X_608))),equivalent(X_606,X_606)))
| is_a_theorem(equivalent(equivalent(X_606,X_606),equivalent(X_607,equivalent(X_607,equivalent(X_608,X_608))))) ),
inference(subst,[],[refute_0_30:[bind(X_380,$fot(equivalent(X_606,X_606))),bind(X_381,$fot(equivalent(X_607,equivalent(X_607,equivalent(X_608,X_608)))))]]) ).
cnf(refute_0_36,plain,
( ~ is_a_theorem(equivalent(equivalent(X_603,X_603),equivalent(X_603,equivalent(X_603,equivalent(X_605,X_605)))))
| is_a_theorem(equivalent(equivalent(X_603,equivalent(X_603,equivalent(X_605,X_605))),equivalent(X_147,X_147))) ),
inference(subst,[],[refute_0_20:[bind(X_145,$fot(X_603)),bind(X_146,$fot(equivalent(X_603,equivalent(X_603,equivalent(X_605,X_605)))))]]) ).
cnf(refute_0_37,plain,
( ~ is_a_theorem(equivalent(equivalent(X_23,equivalent(X_392,X_392)),equivalent(equivalent(X_392,X_392),equivalent(X_23,equivalent(X_392,X_392)))))
| is_a_theorem(equivalent(equivalent(X_23,X_22),equivalent(X_22,equivalent(X_23,equivalent(X_392,X_392))))) ),
inference(subst,[],[refute_0_13:[bind(X_21,$fot(equivalent(X_392,X_392))),bind(X_24,$fot(equivalent(X_23,equivalent(X_392,X_392))))]]) ).
cnf(refute_0_38,plain,
( ~ is_a_theorem(equivalent(X_141,X_140))
| ~ is_a_theorem(equivalent(equivalent(X_141,X_140),equivalent(X_140,equivalent(equivalent(X_139,X_139),X_141))))
| is_a_theorem(equivalent(X_140,equivalent(equivalent(X_139,X_139),X_141))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(X_141,X_140))),bind(Y,$fot(equivalent(X_140,equivalent(equivalent(X_139,X_139),X_141))))]]) ).
cnf(refute_0_39,plain,
is_a_theorem(equivalent(equivalent(equivalent(X,Y),X_20),equivalent(X_20,equivalent(equivalent(X,Z),equivalent(Z,Y))))),
inference(subst,[],[refute_0_7:[bind(X_7,$fot(X_20))]]) ).
cnf(refute_0_40,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X,Y),X_20),equivalent(X_20,equivalent(equivalent(X,Z),equivalent(Z,Y)))))
| is_a_theorem(equivalent(equivalent(X_20,equivalent(equivalent(X,Z),equivalent(Z,Y))),equivalent(equivalent(equivalent(X,Y),X_17),equivalent(X_17,X_20)))) ),
inference(subst,[],[refute_0_9:[bind(X_10,$fot(X_17)),bind(X_11,$fot(equivalent(X_20,equivalent(equivalent(X,Z),equivalent(Z,Y))))),bind(X_8,$fot(equivalent(X,Y))),bind(X_9,$fot(X_20))]]) ).
cnf(refute_0_41,plain,
is_a_theorem(equivalent(equivalent(X_20,equivalent(equivalent(X,Z),equivalent(Z,Y))),equivalent(equivalent(equivalent(X,Y),X_17),equivalent(X_17,X_20)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X,Y),X_20),equivalent(X_20,equivalent(equivalent(X,Z),equivalent(Z,Y))))) )],[refute_0_39,refute_0_40]) ).
cnf(refute_0_42,plain,
is_a_theorem(equivalent(equivalent(X_137,equivalent(equivalent(X,Z),equivalent(Z,Z))),equivalent(equivalent(equivalent(X,Z),equivalent(Z,Z)),equivalent(equivalent(Z,Z),X_137)))),
inference(subst,[],[refute_0_41:[bind(Y,$fot(Z)),bind(X_17,$fot(equivalent(Z,Z))),bind(X_20,$fot(X_137))]]) ).
cnf(refute_0_43,plain,
( ~ is_a_theorem(equivalent(equivalent(X_137,equivalent(equivalent(X,Z),equivalent(Z,Z))),equivalent(equivalent(equivalent(X,Z),equivalent(Z,Z)),equivalent(equivalent(Z,Z),X_137))))
| is_a_theorem(equivalent(equivalent(X_137,X_136),equivalent(X_136,equivalent(equivalent(Z,Z),X_137)))) ),
inference(subst,[],[refute_0_13:[bind(X_21,$fot(equivalent(equivalent(X,Z),equivalent(Z,Z)))),bind(X_22,$fot(X_136)),bind(X_23,$fot(X_137)),bind(X_24,$fot(equivalent(equivalent(Z,Z),X_137)))]]) ).
cnf(refute_0_44,plain,
is_a_theorem(equivalent(equivalent(X_137,X_136),equivalent(X_136,equivalent(equivalent(Z,Z),X_137)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_137,equivalent(equivalent(X,Z),equivalent(Z,Z))),equivalent(equivalent(equivalent(X,Z),equivalent(Z,Z)),equivalent(equivalent(Z,Z),X_137)))) )],[refute_0_42,refute_0_43]) ).
cnf(refute_0_45,plain,
is_a_theorem(equivalent(equivalent(X_141,X_140),equivalent(X_140,equivalent(equivalent(X_139,X_139),X_141)))),
inference(subst,[],[refute_0_44:[bind(Z,$fot(X_139)),bind(X_136,$fot(X_140)),bind(X_137,$fot(X_141))]]) ).
cnf(refute_0_46,plain,
( ~ is_a_theorem(equivalent(X_141,X_140))
| is_a_theorem(equivalent(X_140,equivalent(equivalent(X_139,X_139),X_141))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_141,X_140),equivalent(X_140,equivalent(equivalent(X_139,X_139),X_141)))) )],[refute_0_45,refute_0_38]) ).
cnf(refute_0_47,plain,
( ~ is_a_theorem(equivalent(X_389,X_389))
| is_a_theorem(equivalent(X_389,equivalent(equivalent(X_139,X_139),X_389))) ),
inference(subst,[],[refute_0_46:[bind(X_140,$fot(X_389)),bind(X_141,$fot(X_389))]]) ).
cnf(refute_0_48,plain,
( ~ is_a_theorem(equivalent(equivalent(X_387,X_388),equivalent(equivalent(X_387,X_386),equivalent(X_386,X_388))))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X_387,X_388),equivalent(equivalent(X_387,X_386),equivalent(X_386,X_388))),equivalent(X_385,X_385)))
| is_a_theorem(equivalent(X_385,X_385)) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(X_387,X_388),equivalent(equivalent(X_387,X_386),equivalent(X_386,X_388))))),bind(Y,$fot(equivalent(X_385,X_385)))]]) ).
cnf(refute_0_49,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_74,X_75),X_73),equivalent(equivalent(equivalent(X_74,X_75),Z),equivalent(Z,X_73)))),
inference(subst,[],[yqf:[bind(X,$fot(equivalent(X_74,X_75))),bind(Y,$fot(X_73))]]) ).
cnf(refute_0_50,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_15,X_16),X_14),X_12))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_15,X_16),X_14),X_12),equivalent(X_12,equivalent(X_14,equivalent(equivalent(X_15,X_13),equivalent(X_13,X_16))))))
| is_a_theorem(equivalent(X_12,equivalent(X_14,equivalent(equivalent(X_15,X_13),equivalent(X_13,X_16))))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(equivalent(X_15,X_16),X_14),X_12))),bind(Y,$fot(equivalent(X_12,equivalent(X_14,equivalent(equivalent(X_15,X_13),equivalent(X_13,X_16))))))]]) ).
cnf(refute_0_51,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_8,X_9),X_11),equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9)))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_8,X_9),X_11),Z),equivalent(Z,equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9)))))) ),
inference(subst,[],[refute_0_5:[bind(X,$fot(equivalent(equivalent(X_8,X_9),X_11))),bind(Y,$fot(equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9)))))]]) ).
cnf(refute_0_52,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_8,X_9),X_11),Z),equivalent(Z,equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9)))))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_8,X_9),X_11),equivalent(X_11,equivalent(equivalent(X_8,X_10),equivalent(X_10,X_9))))) )],[refute_0_8,refute_0_51]) ).
cnf(refute_0_53,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_15,X_16),X_14),X_12),equivalent(X_12,equivalent(X_14,equivalent(equivalent(X_15,X_13),equivalent(X_13,X_16)))))),
inference(subst,[],[refute_0_52:[bind(Z,$fot(X_12)),bind(X_10,$fot(X_13)),bind(X_11,$fot(X_14)),bind(X_8,$fot(X_15)),bind(X_9,$fot(X_16))]]) ).
cnf(refute_0_54,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_15,X_16),X_14),X_12))
| is_a_theorem(equivalent(X_12,equivalent(X_14,equivalent(equivalent(X_15,X_13),equivalent(X_13,X_16))))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_15,X_16),X_14),X_12),equivalent(X_12,equivalent(X_14,equivalent(equivalent(X_15,X_13),equivalent(X_13,X_16)))))) )],[refute_0_53,refute_0_50]) ).
cnf(refute_0_55,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_74,X_75),X_73),equivalent(equivalent(equivalent(X_74,X_75),Z),equivalent(Z,X_73))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_74,X_75),Z),equivalent(Z,X_73)),equivalent(X_73,equivalent(equivalent(X_74,X_72),equivalent(X_72,X_75))))) ),
inference(subst,[],[refute_0_54:[bind(X_12,$fot(equivalent(equivalent(equivalent(X_74,X_75),Z),equivalent(Z,X_73)))),bind(X_13,$fot(X_72)),bind(X_14,$fot(X_73)),bind(X_15,$fot(X_74)),bind(X_16,$fot(X_75))]]) ).
cnf(refute_0_56,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_74,X_75),Z),equivalent(Z,X_73)),equivalent(X_73,equivalent(equivalent(X_74,X_72),equivalent(X_72,X_75))))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_74,X_75),X_73),equivalent(equivalent(equivalent(X_74,X_75),Z),equivalent(Z,X_73)))) )],[refute_0_49,refute_0_55]) ).
cnf(refute_0_57,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_74,X_75),equivalent(X_74,X_75)),equivalent(equivalent(X_74,X_75),equivalent(X_74,X_75))),equivalent(equivalent(X_74,X_75),equivalent(equivalent(X_74,X_72),equivalent(X_72,X_75))))),
inference(subst,[],[refute_0_56:[bind(Z,$fot(equivalent(X_74,X_75))),bind(X_73,$fot(equivalent(X_74,X_75)))]]) ).
cnf(refute_0_58,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_74,X_75),equivalent(X_74,X_75)),equivalent(equivalent(X_74,X_75),equivalent(X_74,X_75))),equivalent(equivalent(X_74,X_75),equivalent(equivalent(X_74,X_72),equivalent(X_72,X_75)))))
| is_a_theorem(equivalent(equivalent(equivalent(X_74,X_75),equivalent(equivalent(X_74,X_72),equivalent(X_72,X_75))),equivalent(X_374,X_374))) ),
inference(subst,[],[refute_0_20:[bind(X_145,$fot(equivalent(equivalent(X_74,X_75),equivalent(X_74,X_75)))),bind(X_146,$fot(equivalent(equivalent(X_74,X_75),equivalent(equivalent(X_74,X_72),equivalent(X_72,X_75))))),bind(X_147,$fot(X_374))]]) ).
cnf(refute_0_59,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_74,X_75),equivalent(equivalent(X_74,X_72),equivalent(X_72,X_75))),equivalent(X_374,X_374))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_74,X_75),equivalent(X_74,X_75)),equivalent(equivalent(X_74,X_75),equivalent(X_74,X_75))),equivalent(equivalent(X_74,X_75),equivalent(equivalent(X_74,X_72),equivalent(X_72,X_75))))) )],[refute_0_57,refute_0_58]) ).
cnf(refute_0_60,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_387,X_388),equivalent(equivalent(X_387,X_386),equivalent(X_386,X_388))),equivalent(X_385,X_385))),
inference(subst,[],[refute_0_59:[bind(X_374,$fot(X_385)),bind(X_72,$fot(X_386)),bind(X_74,$fot(X_387)),bind(X_75,$fot(X_388))]]) ).
cnf(refute_0_61,plain,
( ~ is_a_theorem(equivalent(equivalent(X_387,X_388),equivalent(equivalent(X_387,X_386),equivalent(X_386,X_388))))
| is_a_theorem(equivalent(X_385,X_385)) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_387,X_388),equivalent(equivalent(X_387,X_386),equivalent(X_386,X_388))),equivalent(X_385,X_385))) )],[refute_0_60,refute_0_48]) ).
cnf(refute_0_62,plain,
is_a_theorem(equivalent(equivalent(X_387,X_388),equivalent(equivalent(X_387,X_386),equivalent(X_386,X_388)))),
inference(subst,[],[yqf:[bind(X,$fot(X_387)),bind(Y,$fot(X_388)),bind(Z,$fot(X_386))]]) ).
cnf(refute_0_63,plain,
is_a_theorem(equivalent(X_385,X_385)),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_387,X_388),equivalent(equivalent(X_387,X_386),equivalent(X_386,X_388)))) )],[refute_0_62,refute_0_61]) ).
cnf(refute_0_64,plain,
is_a_theorem(equivalent(X_389,X_389)),
inference(subst,[],[refute_0_63:[bind(X_385,$fot(X_389))]]) ).
cnf(refute_0_65,plain,
is_a_theorem(equivalent(X_389,equivalent(equivalent(X_139,X_139),X_389))),
inference(resolve,[$cnf( is_a_theorem(equivalent(X_389,X_389)) )],[refute_0_64,refute_0_47]) ).
cnf(refute_0_66,plain,
is_a_theorem(equivalent(equivalent(X_23,equivalent(X_392,X_392)),equivalent(equivalent(X_392,X_392),equivalent(X_23,equivalent(X_392,X_392))))),
inference(subst,[],[refute_0_65:[bind(X_139,$fot(X_392)),bind(X_389,$fot(equivalent(X_23,equivalent(X_392,X_392))))]]) ).
cnf(refute_0_67,plain,
is_a_theorem(equivalent(equivalent(X_23,X_22),equivalent(X_22,equivalent(X_23,equivalent(X_392,X_392))))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_23,equivalent(X_392,X_392)),equivalent(equivalent(X_392,X_392),equivalent(X_23,equivalent(X_392,X_392))))) )],[refute_0_66,refute_0_37]) ).
cnf(refute_0_68,plain,
is_a_theorem(equivalent(equivalent(X_603,X_603),equivalent(X_603,equivalent(X_603,equivalent(X_605,X_605))))),
inference(subst,[],[refute_0_67:[bind(X_22,$fot(X_603)),bind(X_23,$fot(X_603)),bind(X_392,$fot(X_605))]]) ).
cnf(refute_0_69,plain,
is_a_theorem(equivalent(equivalent(X_603,equivalent(X_603,equivalent(X_605,X_605))),equivalent(X_147,X_147))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_603,X_603),equivalent(X_603,equivalent(X_603,equivalent(X_605,X_605))))) )],[refute_0_68,refute_0_36]) ).
cnf(refute_0_70,plain,
is_a_theorem(equivalent(equivalent(X_607,equivalent(X_607,equivalent(X_608,X_608))),equivalent(X_606,X_606))),
inference(subst,[],[refute_0_69:[bind(X_147,$fot(X_606)),bind(X_603,$fot(X_607)),bind(X_605,$fot(X_608))]]) ).
cnf(refute_0_71,plain,
is_a_theorem(equivalent(equivalent(X_606,X_606),equivalent(X_607,equivalent(X_607,equivalent(X_608,X_608))))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_607,equivalent(X_607,equivalent(X_608,X_608))),equivalent(X_606,X_606))) )],[refute_0_70,refute_0_35]) ).
cnf(refute_0_72,plain,
is_a_theorem(equivalent(equivalent(X_789,X_789),equivalent(X_790,equivalent(X_790,equivalent(X_791,X_791))))),
inference(subst,[],[refute_0_71:[bind(X_606,$fot(X_789)),bind(X_607,$fot(X_790)),bind(X_608,$fot(X_791))]]) ).
cnf(refute_0_73,plain,
( ~ is_a_theorem(equivalent(X_789,X_789))
| is_a_theorem(equivalent(X_790,equivalent(X_790,equivalent(X_791,X_791)))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_789,X_789),equivalent(X_790,equivalent(X_790,equivalent(X_791,X_791))))) )],[refute_0_72,refute_0_34]) ).
cnf(refute_0_74,plain,
is_a_theorem(equivalent(X_789,X_789)),
inference(subst,[],[refute_0_63:[bind(X_385,$fot(X_789))]]) ).
cnf(refute_0_75,plain,
is_a_theorem(equivalent(X_790,equivalent(X_790,equivalent(X_791,X_791)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(X_789,X_789)) )],[refute_0_74,refute_0_73]) ).
cnf(refute_0_76,plain,
is_a_theorem(equivalent(X_792,equivalent(X_792,equivalent(X_793,X_793)))),
inference(subst,[],[refute_0_75:[bind(X_790,$fot(X_792)),bind(X_791,$fot(X_793))]]) ).
cnf(refute_0_77,plain,
is_a_theorem(equivalent(equivalent(X_792,equivalent(X_793,X_793)),X_792)),
inference(resolve,[$cnf( is_a_theorem(equivalent(X_792,equivalent(X_792,equivalent(X_793,X_793)))) )],[refute_0_76,refute_0_33]) ).
cnf(refute_0_78,plain,
is_a_theorem(equivalent(equivalent(X_794,equivalent(X_795,X_795)),X_794)),
inference(subst,[],[refute_0_77:[bind(X_792,$fot(X_794)),bind(X_793,$fot(X_795))]]) ).
cnf(refute_0_79,plain,
( ~ is_a_theorem(equivalent(X_794,equivalent(X_795,X_795)))
| is_a_theorem(X_794) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_794,equivalent(X_795,X_795)),X_794)) )],[refute_0_78,refute_0_32]) ).
cnf(refute_0_80,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_5280,X_5279),equivalent(X_5278,X_5280)),equivalent(X_5278,X_5279)),equivalent(equivalent(equivalent(X_5278,X_5280),equivalent(X_5278,X_5280)),equivalent(equivalent(X_5278,X_5280),equivalent(X_5278,X_5280)))))
| is_a_theorem(equivalent(equivalent(equivalent(X_5280,X_5279),equivalent(X_5278,X_5280)),equivalent(X_5278,X_5279))) ),
inference(subst,[],[refute_0_79:[bind(X_794,$fot(equivalent(equivalent(equivalent(X_5280,X_5279),equivalent(X_5278,X_5280)),equivalent(X_5278,X_5279)))),bind(X_795,$fot(equivalent(equivalent(X_5278,X_5280),equivalent(X_5278,X_5280))))]]) ).
cnf(refute_0_81,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)),equivalent(X_1700,X_1701)))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)),Z),equivalent(Z,equivalent(X_1700,X_1701)))) ),
inference(subst,[],[refute_0_5:[bind(X,$fot(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)))),bind(Y,$fot(equivalent(X_1700,X_1701)))]]) ).
cnf(refute_0_82,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)),equivalent(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)),equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)))))
| is_a_theorem(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694))) ),
inference(subst,[],[refute_0_79:[bind(X_794,$fot(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)))),bind(X_795,$fot(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694))))]]) ).
cnf(refute_0_83,plain,
( ~ is_a_theorem(equivalent(equivalent(X_1687,equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687)),equivalent(equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687),equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687))))
| is_a_theorem(equivalent(X_1687,equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687))) ),
inference(subst,[],[refute_0_79:[bind(X_794,$fot(equivalent(X_1687,equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687)))),bind(X_795,$fot(equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687)))]]) ).
cnf(refute_0_84,plain,
( ~ is_a_theorem(equivalent(equivalent(X_1681,equivalent(equivalent(equivalent(X_1682,X_1683),equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683))),equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)))),equivalent(equivalent(equivalent(equivalent(X_1682,X_1683),equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683))),equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683))),equivalent(equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)),X_1681))))
| is_a_theorem(equivalent(equivalent(X_1681,X_22),equivalent(X_22,equivalent(equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)),X_1681)))) ),
inference(subst,[],[refute_0_13:[bind(X_21,$fot(equivalent(equivalent(equivalent(X_1682,X_1683),equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683))),equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683))))),bind(X_23,$fot(X_1681)),bind(X_24,$fot(equivalent(equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)),X_1681)))]]) ).
cnf(refute_0_85,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_274,equivalent(equivalent(X_270,X_272),equivalent(X_272,X_271))),X_269),equivalent(X_269,equivalent(equivalent(equivalent(X_270,X_271),X_273),equivalent(X_273,X_274)))))
| is_a_theorem(equivalent(equivalent(X_269,equivalent(equivalent(equivalent(X_270,X_271),X_273),equivalent(X_273,X_274))),equivalent(equivalent(equivalent(X_274,equivalent(equivalent(X_270,X_272),equivalent(X_272,X_271))),X_10),equivalent(X_10,X_269)))) ),
inference(subst,[],[refute_0_9:[bind(X_11,$fot(equivalent(X_269,equivalent(equivalent(equivalent(X_270,X_271),X_273),equivalent(X_273,X_274))))),bind(X_8,$fot(equivalent(X_274,equivalent(equivalent(X_270,X_272),equivalent(X_272,X_271))))),bind(X_9,$fot(X_269))]]) ).
cnf(refute_0_86,plain,
( ~ is_a_theorem(equivalent(equivalent(X_35,equivalent(equivalent(X_31,X_33),equivalent(X_33,X_32))),equivalent(equivalent(equivalent(X_31,X_32),X_34),equivalent(X_34,X_35))))
| is_a_theorem(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(X_31,X_33),equivalent(X_33,X_32))),Z),equivalent(Z,equivalent(equivalent(equivalent(X_31,X_32),X_34),equivalent(X_34,X_35))))) ),
inference(subst,[],[refute_0_5:[bind(X,$fot(equivalent(X_35,equivalent(equivalent(X_31,X_33),equivalent(X_33,X_32))))),bind(Y,$fot(equivalent(equivalent(equivalent(X_31,X_32),X_34),equivalent(X_34,X_35))))]]) ).
cnf(refute_0_87,plain,
is_a_theorem(equivalent(equivalent(X_35,equivalent(equivalent(X_31,X_33),equivalent(X_33,X_32))),equivalent(equivalent(equivalent(X_31,X_32),X_34),equivalent(X_34,X_35)))),
inference(subst,[],[refute_0_41:[bind(X,$fot(X_31)),bind(Y,$fot(X_32)),bind(Z,$fot(X_33)),bind(X_17,$fot(X_34)),bind(X_20,$fot(X_35))]]) ).
cnf(refute_0_88,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_35,equivalent(equivalent(X_31,X_33),equivalent(X_33,X_32))),Z),equivalent(Z,equivalent(equivalent(equivalent(X_31,X_32),X_34),equivalent(X_34,X_35))))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_35,equivalent(equivalent(X_31,X_33),equivalent(X_33,X_32))),equivalent(equivalent(equivalent(X_31,X_32),X_34),equivalent(X_34,X_35)))) )],[refute_0_87,refute_0_86]) ).
cnf(refute_0_89,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_274,equivalent(equivalent(X_270,X_272),equivalent(X_272,X_271))),X_269),equivalent(X_269,equivalent(equivalent(equivalent(X_270,X_271),X_273),equivalent(X_273,X_274))))),
inference(subst,[],[refute_0_88:[bind(Z,$fot(X_269)),bind(X_31,$fot(X_270)),bind(X_32,$fot(X_271)),bind(X_33,$fot(X_272)),bind(X_34,$fot(X_273)),bind(X_35,$fot(X_274))]]) ).
cnf(refute_0_90,plain,
is_a_theorem(equivalent(equivalent(X_269,equivalent(equivalent(equivalent(X_270,X_271),X_273),equivalent(X_273,X_274))),equivalent(equivalent(equivalent(X_274,equivalent(equivalent(X_270,X_272),equivalent(X_272,X_271))),X_10),equivalent(X_10,X_269)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_274,equivalent(equivalent(X_270,X_272),equivalent(X_272,X_271))),X_269),equivalent(X_269,equivalent(equivalent(equivalent(X_270,X_271),X_273),equivalent(X_273,X_274))))) )],[refute_0_89,refute_0_85]) ).
cnf(refute_0_91,plain,
is_a_theorem(equivalent(equivalent(X_1681,equivalent(equivalent(equivalent(X_1682,X_1683),equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683))),equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)))),equivalent(equivalent(equivalent(equivalent(X_1682,X_1683),equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683))),equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683))),equivalent(equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)),X_1681)))),
inference(subst,[],[refute_0_90:[bind(X_10,$fot(equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)))),bind(X_269,$fot(X_1681)),bind(X_270,$fot(X_1682)),bind(X_271,$fot(X_1683)),bind(X_272,$fot(X_1684)),bind(X_273,$fot(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)))),bind(X_274,$fot(equivalent(X_1682,X_1683)))]]) ).
cnf(refute_0_92,plain,
is_a_theorem(equivalent(equivalent(X_1681,X_22),equivalent(X_22,equivalent(equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)),X_1681)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_1681,equivalent(equivalent(equivalent(X_1682,X_1683),equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683))),equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)))),equivalent(equivalent(equivalent(equivalent(X_1682,X_1683),equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683))),equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683))),equivalent(equivalent(equivalent(equivalent(X_1682,X_1684),equivalent(X_1684,X_1683)),equivalent(X_1682,X_1683)),X_1681)))) )],[refute_0_91,refute_0_84]) ).
cnf(refute_0_93,plain,
is_a_theorem(equivalent(equivalent(X_1687,equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687)),equivalent(equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687),equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687)))),
inference(subst,[],[refute_0_92:[bind(X_1681,$fot(X_1687)),bind(X_1682,$fot(X_1688)),bind(X_1683,$fot(X_1689)),bind(X_1684,$fot(X_1690)),bind(X_22,$fot(equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687)))]]) ).
cnf(refute_0_94,plain,
is_a_theorem(equivalent(X_1687,equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(X_1687,equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687)),equivalent(equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687),equivalent(equivalent(equivalent(equivalent(X_1688,X_1690),equivalent(X_1690,X_1689)),equivalent(X_1688,X_1689)),X_1687)))) )],[refute_0_93,refute_0_83]) ).
cnf(refute_0_95,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)),equivalent(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)),equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694))))),
inference(subst,[],[refute_0_94:[bind(X_1687,$fot(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)))),bind(X_1688,$fot(X_1693)),bind(X_1689,$fot(X_1694)),bind(X_1690,$fot(X_1695))]]) ).
cnf(refute_0_96,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)),equivalent(equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694)),equivalent(equivalent(equivalent(X_1693,X_1695),equivalent(X_1695,X_1694)),equivalent(X_1693,X_1694))))) )],[refute_0_95,refute_0_82]) ).
cnf(refute_0_97,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)),equivalent(X_1700,X_1701))),
inference(subst,[],[refute_0_96:[bind(X_1693,$fot(X_1700)),bind(X_1694,$fot(X_1701)),bind(X_1695,$fot(X_1702))]]) ).
cnf(refute_0_98,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)),Z),equivalent(Z,equivalent(X_1700,X_1701)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)),equivalent(X_1700,X_1701))) )],[refute_0_97,refute_0_81]) ).
cnf(refute_0_99,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)),equivalent(equivalent(X_1702,X_1701),X_3270)),equivalent(equivalent(equivalent(X_1702,X_1701),X_3270),equivalent(X_1700,X_1701)))),
inference(subst,[],[refute_0_98:[bind(Z,$fot(equivalent(equivalent(X_1702,X_1701),X_3270)))]]) ).
cnf(refute_0_100,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_39,X_37),equivalent(X_37,X_40)),X_36))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_39,X_37),equivalent(X_37,X_40)),X_36),equivalent(X_36,equivalent(equivalent(X_39,X_38),equivalent(X_38,X_40)))))
| is_a_theorem(equivalent(X_36,equivalent(equivalent(X_39,X_38),equivalent(X_38,X_40)))) ),
inference(subst,[],[condensed_detachment:[bind(X,$fot(equivalent(equivalent(equivalent(X_39,X_37),equivalent(X_37,X_40)),X_36))),bind(Y,$fot(equivalent(X_36,equivalent(equivalent(X_39,X_38),equivalent(X_38,X_40)))))]]) ).
cnf(refute_0_101,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)),equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)),Z),equivalent(Z,equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24))))) ),
inference(subst,[],[refute_0_5:[bind(X,$fot(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)))),bind(Y,$fot(equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24))))]]) ).
cnf(refute_0_102,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)),Z),equivalent(Z,equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24))))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_23,X_21),equivalent(X_21,X_24)),equivalent(equivalent(X_23,X_22),equivalent(X_22,X_24)))) )],[refute_0_12,refute_0_101]) ).
cnf(refute_0_103,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_39,X_37),equivalent(X_37,X_40)),X_36),equivalent(X_36,equivalent(equivalent(X_39,X_38),equivalent(X_38,X_40))))),
inference(subst,[],[refute_0_102:[bind(Z,$fot(X_36)),bind(X_21,$fot(X_37)),bind(X_22,$fot(X_38)),bind(X_23,$fot(X_39)),bind(X_24,$fot(X_40))]]) ).
cnf(refute_0_104,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(X_39,X_37),equivalent(X_37,X_40)),X_36))
| is_a_theorem(equivalent(X_36,equivalent(equivalent(X_39,X_38),equivalent(X_38,X_40)))) ),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_39,X_37),equivalent(X_37,X_40)),X_36),equivalent(X_36,equivalent(equivalent(X_39,X_38),equivalent(X_38,X_40))))) )],[refute_0_103,refute_0_100]) ).
cnf(refute_0_105,plain,
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)),equivalent(equivalent(X_1702,X_1701),X_3270)),equivalent(equivalent(equivalent(X_1702,X_1701),X_3270),equivalent(X_1700,X_1701))))
| is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1702,X_1701),X_3270),equivalent(X_1700,X_1701)),equivalent(equivalent(equivalent(X_1700,X_1702),X_3268),equivalent(X_3268,X_3270)))) ),
inference(subst,[],[refute_0_104:[bind(X_36,$fot(equivalent(equivalent(equivalent(X_1702,X_1701),X_3270),equivalent(X_1700,X_1701)))),bind(X_37,$fot(equivalent(X_1702,X_1701))),bind(X_38,$fot(X_3268)),bind(X_39,$fot(equivalent(X_1700,X_1702))),bind(X_40,$fot(X_3270))]]) ).
cnf(refute_0_106,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1702,X_1701),X_3270),equivalent(X_1700,X_1701)),equivalent(equivalent(equivalent(X_1700,X_1702),X_3268),equivalent(X_3268,X_3270)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_1700,X_1702),equivalent(X_1702,X_1701)),equivalent(equivalent(X_1702,X_1701),X_3270)),equivalent(equivalent(equivalent(X_1702,X_1701),X_3270),equivalent(X_1700,X_1701)))) )],[refute_0_99,refute_0_105]) ).
cnf(refute_0_107,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_5280,X_5279),equivalent(X_5278,X_5280)),equivalent(X_5278,X_5279)),equivalent(equivalent(equivalent(X_5278,X_5280),equivalent(X_5278,X_5280)),equivalent(equivalent(X_5278,X_5280),equivalent(X_5278,X_5280))))),
inference(subst,[],[refute_0_106:[bind(X_1700,$fot(X_5278)),bind(X_1701,$fot(X_5279)),bind(X_1702,$fot(X_5280)),bind(X_3268,$fot(equivalent(X_5278,X_5280))),bind(X_3270,$fot(equivalent(X_5278,X_5280)))]]) ).
cnf(refute_0_108,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_5280,X_5279),equivalent(X_5278,X_5280)),equivalent(X_5278,X_5279))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(equivalent(X_5280,X_5279),equivalent(X_5278,X_5280)),equivalent(X_5278,X_5279)),equivalent(equivalent(equivalent(X_5278,X_5280),equivalent(X_5278,X_5280)),equivalent(equivalent(X_5278,X_5280),equivalent(X_5278,X_5280))))) )],[refute_0_107,refute_0_80]) ).
cnf(refute_0_109,plain,
is_a_theorem(equivalent(equivalent(equivalent(X_5285,X_5284),equivalent(X_5283,X_5285)),equivalent(X_5283,X_5284))),
inference(subst,[],[refute_0_108:[bind(X_5278,$fot(X_5283)),bind(X_5279,$fot(X_5284)),bind(X_5280,$fot(X_5285))]]) ).
cnf(refute_0_110,plain,
is_a_theorem(equivalent(equivalent(X_5283,X_5284),equivalent(equivalent(X_5285,X_5284),equivalent(X_5283,X_5285)))),
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(equivalent(X_5285,X_5284),equivalent(X_5283,X_5285)),equivalent(X_5283,X_5284))) )],[refute_0_109,refute_0_31]) ).
cnf(refute_0_111,plain,
is_a_theorem(equivalent(equivalent(a,b),equivalent(equivalent(c,b),equivalent(a,c)))),
inference(subst,[],[refute_0_110:[bind(X_5283,$fot(a)),bind(X_5284,$fot(b)),bind(X_5285,$fot(c))]]) ).
cnf(refute_0_112,plain,
$false,
inference(resolve,[$cnf( is_a_theorem(equivalent(equivalent(a,b),equivalent(equivalent(c,b),equivalent(a,c)))) )],[refute_0_111,prove_yql]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL010-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : metis --show proof --show saturation %s
% 0.07/0.34 % Computer : n005.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sat Sep 5 12:39:35 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 9.56/9.88 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.56/9.88
% 9.56/9.88 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 9.66/9.90
%------------------------------------------------------------------------------