%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL018-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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 : Fri Sep 25 02:00:41 PM UTC 2026
% Result : Unsatisfiable 101.91s 13.60s
% Output : Proof 101.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 127
% Number of leaves : 4
% Syntax : Number of formulae : 220 ( 216 unt; 0 def)
% Number of atoms : 228 ( 207 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-4 aty)
% Number of variables : 838 ( 2 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(equivalent(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f0_nnf,plain,
! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(equivalent(X,Y)) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(equivalent(X,Y)) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t3,plain,
ifeq(is_a_theorem(equivalent(X1,X2)),true,ifeq(is_a_theorem(X1),true,is_a_theorem(X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t11,plain,
ifeq(is_a_theorem(equivalent(X1,X2)),true,ifeq(is_a_theorem(X1),true,is_a_theorem(X2),true),true) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(f1,axiom,
is_a_theorem(equivalent(equivalent(equivalent(X,equivalent(Y,Z)),Y),equivalent(Z,X))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pym) ).
fof(f1_nnf,plain,
! [X,Y,Z] : is_a_theorem(equivalent(equivalent(equivalent(X,equivalent(Y,Z)),Y),equivalent(Z,X))),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z] : is_a_theorem(equivalent(equivalent(equivalent(X,equivalent(Y,Z)),Y),equivalent(Z,X))),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(X1,X2)),X1),equivalent(X2,X0))),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t2,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1))) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t10,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1))) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t15,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),X2)),true,is_a_theorem(equivalent(X3,X1)),true),true),
inference(cp,[status(thm)],[t11,t10]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t6,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t210226,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),X2)),true,is_a_theorem(equivalent(X3,X1)),true),
inference(step,[status(thm)],[t15,t6]) ).
cnf(t27,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),X2)),true,is_a_theorem(equivalent(X3,X1)),true) = true,
inference(orient,[status(thm)],[t210226]) ).
cnf(t16,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),X4)),true,ifeq(true,true,is_a_theorem(X4),true),true),
inference(cp,[status(thm)],[t11,t10]) ).
cnf(t210227,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),X4)),true,is_a_theorem(X4),true),
inference(step,[status(thm)],[t16,t6]) ).
cnf(t32,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),X4)),true,is_a_theorem(X4),true) = true,
inference(orient,[status(thm)],[t210227]) ).
cnf(hi0,axiom,
ifeq(is_a_theorem(equivalent(X0,X1)),true,ifeq(is_a_theorem(X0),true,is_a_theorem(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(hi1,axiom,
is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(X1,X2)),X1),equivalent(X2,X0))) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(h0,plain,
is_a_theorem(equivalent(V0,equivalent(V1,equivalent(equivalent(equivalent(V2,V1),V0),V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,hi1]) ).
cnf(t4,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h0,h0]) ).
cnf(t8,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X2))) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t18,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X2)),Y5)),true,ifeq(true,true,is_a_theorem(Y5),true),true),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t210231,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X2)),Y5)),true,is_a_theorem(Y5),true),
inference(step,[status(thm)],[t18,t6]) ).
cnf(t80,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X2)),Y5)),true,is_a_theorem(Y5),true) = true,
inference(orient,[status(thm)],[t210231]) ).
cnf(t33,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),equivalent(X5,equivalent(Y5,equivalent(equivalent(equivalent(Y6,Y5),X5),Y6)))),X1)),true),
inference(cp,[status(thm)],[t32,t8]) ).
cnf(t210235,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),equivalent(X5,equivalent(Y5,equivalent(equivalent(equivalent(Y6,Y5),X5),Y6)))),X1)),
inference(step,[status(thm)],[t33,t6]) ).
cnf(t140,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),equivalent(X5,equivalent(Y5,equivalent(equivalent(equivalent(Y6,Y5),X5),Y6)))),X1)) = true,
inference(orient,[status(thm)],[t210235]) ).
cnf(t144,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X3,equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4))))),true),
inference(cp,[status(thm)],[t27,t140]) ).
cnf(t210236,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X3,equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4))))),
inference(step,[status(thm)],[t144,t6]) ).
cnf(t158,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X3,equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4))))) = true,
inference(orient,[status(thm)],[t210236]) ).
cnf(t173,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,X2),X1),X3))),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)))),true),
inference(cp,[status(thm)],[t80,t158]) ).
cnf(t210241,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,X2),X1),X3))),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)))),
inference(step,[status(thm)],[t173,t6]) ).
cnf(t236,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,X2),X1),X3))),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)))) = true,
inference(orient,[status(thm)],[t210241]) ).
cnf(t239,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),X5),X1),X5)),true),
inference(cp,[status(thm)],[t27,t236]) ).
cnf(t210242,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),X5),X1),X5)),
inference(step,[status(thm)],[t239,t6]) ).
cnf(t251,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),X5),X1),X5)) = true,
inference(orient,[status(thm)],[t210242]) ).
cnf(t252,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),X5),X1)),true,is_a_theorem(X5),true),true),
inference(cp,[status(thm)],[t11,t251]) ).
cnf(t210243,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),X5),X1)),true,is_a_theorem(X5),true),
inference(step,[status(thm)],[t252,t6]) ).
cnf(t268,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X4)),X3),equivalent(X4,X2))),X5),X1)),true,is_a_theorem(X5),true) = true,
inference(orient,[status(thm)],[t210243]) ).
cnf(t269,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4))),X3)),true),
inference(cp,[status(thm)],[t268,t251]) ).
cnf(t210244,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4))),X3)),
inference(step,[status(thm)],[t269,t6]) ).
cnf(t285,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4))),X3)) = true,
inference(orient,[status(thm)],[t210244]) ).
cnf(t286,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4)))),true,is_a_theorem(X3),true),true),
inference(cp,[status(thm)],[t11,t285]) ).
cnf(t210245,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4)))),true,is_a_theorem(X3),true),
inference(step,[status(thm)],[t286,t6]) ).
cnf(t305,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4)))),true,is_a_theorem(X3),true) = true,
inference(orient,[status(thm)],[t210245]) ).
cnf(t306,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X5),X4)),equivalent(X1,X5)))),X2)),true),
inference(cp,[status(thm)],[t305,t236]) ).
cnf(t210247,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X5),X4)),equivalent(X1,X5)))),X2)),
inference(step,[status(thm)],[t306,t6]) ).
cnf(t347,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X5),X4)),equivalent(X1,X5)))),X2)) = true,
inference(orient,[status(thm)],[t210247]) ).
cnf(t351,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3)),X4)),true),
inference(cp,[status(thm)],[t27,t347]) ).
cnf(t210248,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3)),X4)),
inference(step,[status(thm)],[t351,t6]) ).
cnf(t370,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3)),X4)) = true,
inference(orient,[status(thm)],[t210248]) ).
cnf(t371,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3))),true,is_a_theorem(X4),true),true),
inference(cp,[status(thm)],[t11,t370]) ).
cnf(t210249,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3))),true,is_a_theorem(X4),true),
inference(step,[status(thm)],[t371,t6]) ).
cnf(t390,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3))),true,is_a_theorem(X4),true) = true,
inference(orient,[status(thm)],[t210249]) ).
cnf(t5,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h0,hi1]) ).
cnf(t9,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X2))) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t19,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X2)),Y5)),true,ifeq(true,true,is_a_theorem(Y5),true),true),
inference(cp,[status(thm)],[t11,t9]) ).
cnf(t210232,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X2)),Y5)),true,is_a_theorem(Y5),true),
inference(step,[status(thm)],[t19,t6]) ).
cnf(t89,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X2)),Y5)),true,is_a_theorem(Y5),true) = true,
inference(orient,[status(thm)],[t210232]) ).
cnf(t171,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)))),true),
inference(cp,[status(thm)],[t89,t158]) ).
cnf(t210238,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)))),
inference(step,[status(thm)],[t171,t6]) ).
cnf(t191,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)))) = true,
inference(orient,[status(thm)],[t210238]) ).
cnf(t194,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3)))),X2))),true),
inference(cp,[status(thm)],[t27,t191]) ).
cnf(t210239,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3)))),X2))),
inference(step,[status(thm)],[t194,t6]) ).
cnf(t205,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3)))),X2))) = true,
inference(orient,[status(thm)],[t210239]) ).
cnf(t308,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X3),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4))))),true),
inference(cp,[status(thm)],[t305,t205]) ).
cnf(t210260,plain,
true = is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X3),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4))))),
inference(step,[status(thm)],[t308,t6]) ).
cnf(t720,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X3),equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4))))) = true,
inference(orient,[status(thm)],[t210260]) ).
cnf(t728,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X1),equivalent(Y5,X2)),Y5)),true),
inference(cp,[status(thm)],[t390,t720]) ).
cnf(t210269,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X1),equivalent(Y5,X2)),Y5)),
inference(step,[status(thm)],[t728,t6]) ).
cnf(t1011,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X1),equivalent(Y5,X2)),Y5)) = true,
inference(orient,[status(thm)],[t210269]) ).
cnf(t1012,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X1),equivalent(Y5,X2))),true,is_a_theorem(Y5),true),true),
inference(cp,[status(thm)],[t11,t1011]) ).
cnf(t210288,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X1),equivalent(Y5,X2))),true,is_a_theorem(Y5),true),
inference(step,[status(thm)],[t1012,t6]) ).
cnf(t1757,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X3,equivalent(X4,X5)),X4),equivalent(X5,X3))),X1),equivalent(Y5,X2))),true,is_a_theorem(Y5),true) = true,
inference(orient,[status(thm)],[t210288]) ).
cnf(t366,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3)),X4),equivalent(equivalent(equivalent(X5,equivalent(Y5,Y6)),Y5),equivalent(Y6,X5)))),true),
inference(cp,[status(thm)],[t89,t347]) ).
cnf(t210307,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3)),X4),equivalent(equivalent(equivalent(X5,equivalent(Y5,Y6)),Y5),equivalent(Y6,X5)))),
inference(step,[status(thm)],[t366,t6]) ).
cnf(t2953,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(X4,X3)),X4),equivalent(equivalent(equivalent(X5,equivalent(Y5,Y6)),Y5),equivalent(Y6,X5)))) = true,
inference(orient,[status(thm)],[t210307]) ).
cnf(t2972,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,equivalent(equivalent(X3,equivalent(X4,X5)),X4)),equivalent(X5,X3)))),X2)),true),
inference(cp,[status(thm)],[t1757,t2953]) ).
cnf(t210308,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,equivalent(equivalent(X3,equivalent(X4,X5)),X4)),equivalent(X5,X3)))),X2)),
inference(step,[status(thm)],[t2972,t6]) ).
cnf(t3006,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,equivalent(equivalent(X3,equivalent(X4,X5)),X4)),equivalent(X5,X3)))),X2)) = true,
inference(orient,[status(thm)],[t210308]) ).
cnf(t3010,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X4)),X3)),equivalent(X4,X2)),X1)),true),
inference(cp,[status(thm)],[t27,t3006]) ).
cnf(t210309,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X4)),X3)),equivalent(X4,X2)),X1)),
inference(step,[status(thm)],[t3010,t6]) ).
cnf(t3073,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X4)),X3)),equivalent(X4,X2)),X1)) = true,
inference(orient,[status(thm)],[t210309]) ).
cnf(t3079,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X3))),true),
inference(cp,[status(thm)],[t32,t3073]) ).
cnf(t210311,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X3))),
inference(step,[status(thm)],[t3079,t6]) ).
cnf(t3190,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X3))) = true,
inference(orient,[status(thm)],[t210311]) ).
cnf(t3192,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X3)),X4)),true,ifeq(true,true,is_a_theorem(X4),true),true),
inference(cp,[status(thm)],[t11,t3190]) ).
cnf(t210321,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X3)),X4)),true,is_a_theorem(X4),true),
inference(step,[status(thm)],[t3192,t6]) ).
cnf(t3719,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X3)),X4)),true,is_a_theorem(X4),true) = true,
inference(orient,[status(thm)],[t210321]) ).
cnf(t287,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4))),X3),X5)),true,ifeq(true,true,is_a_theorem(X5),true),true),
inference(cp,[status(thm)],[t11,t285]) ).
cnf(t210251,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4))),X3),X5)),true,is_a_theorem(X5),true),
inference(step,[status(thm)],[t287,t6]) ).
cnf(t440,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(X2,equivalent(X4,X1)),X4))),X3),X5)),true,is_a_theorem(X5),true) = true,
inference(orient,[status(thm)],[t210251]) ).
cnf(t147,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)),X3))),true),
inference(cp,[status(thm)],[t32,t140]) ).
cnf(t210237,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)),X3))),
inference(step,[status(thm)],[t147,t6]) ).
cnf(t175,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),X2)),equivalent(equivalent(equivalent(equivalent(X4,equivalent(X5,Y5)),X5),equivalent(Y5,X4)),X3))) = true,
inference(orient,[status(thm)],[t210237]) ).
cnf(t189,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),equivalent(X4,equivalent(X5,equivalent(equivalent(equivalent(Y5,X5),X4),Y5))))),true),
inference(cp,[status(thm)],[t80,t175]) ).
cnf(t210256,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),equivalent(X4,equivalent(X5,equivalent(equivalent(equivalent(Y5,X5),X4),Y5))))),
inference(step,[status(thm)],[t189,t6]) ).
cnf(t570,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),equivalent(X3,X1)),equivalent(X4,equivalent(X5,equivalent(equivalent(equivalent(Y5,X5),X4),Y5))))) = true,
inference(orient,[status(thm)],[t210256]) ).
cnf(t573,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5))))),X2))),true),
inference(cp,[status(thm)],[t27,t570]) ).
cnf(t210257,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5))))),X2))),
inference(step,[status(thm)],[t573,t6]) ).
cnf(t594,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5))))),X2))) = true,
inference(orient,[status(thm)],[t210257]) ).
cnf(t604,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X3),equivalent(X4,equivalent(X5,equivalent(equivalent(equivalent(Y5,X5),X4),Y5)))))),true),
inference(cp,[status(thm)],[t305,t594]) ).
cnf(t210268,plain,
true = is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X3),equivalent(X4,equivalent(X5,equivalent(equivalent(equivalent(Y5,X5),X4),Y5)))))),
inference(step,[status(thm)],[t604,t6]) ).
cnf(t977,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X3),equivalent(X4,equivalent(X5,equivalent(equivalent(equivalent(Y5,X5),X4),Y5)))))) = true,
inference(orient,[status(thm)],[t210268]) ).
cnf(t985,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X1),equivalent(Y5,X2)),Y5)),true),
inference(cp,[status(thm)],[t390,t977]) ).
cnf(t210270,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X1),equivalent(Y5,X2)),Y5)),
inference(step,[status(thm)],[t985,t6]) ).
cnf(t1047,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X1),equivalent(Y5,X2)),Y5)) = true,
inference(orient,[status(thm)],[t210270]) ).
cnf(t1048,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X1),equivalent(Y5,X2))),true,is_a_theorem(Y5),true),true),
inference(cp,[status(thm)],[t11,t1047]) ).
cnf(t210289,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X1),equivalent(Y5,X2))),true,is_a_theorem(Y5),true),
inference(step,[status(thm)],[t1048,t6]) ).
cnf(t1800,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5)))),X1),equivalent(Y5,X2))),true,is_a_theorem(Y5),true) = true,
inference(orient,[status(thm)],[t210289]) ).
cnf(t2989,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,X3),equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5))))),X2)),true),
inference(cp,[status(thm)],[t1800,t2953]) ).
cnf(t210325,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,X3),equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5))))),X2)),
inference(step,[status(thm)],[t2989,t6]) ).
cnf(t3966,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,X3),equivalent(X4,equivalent(equivalent(equivalent(X5,X4),X3),X5))))),X2)) = true,
inference(orient,[status(thm)],[t210325]) ).
cnf(t3970,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X2),X4))),X1)),true),
inference(cp,[status(thm)],[t27,t3966]) ).
cnf(t210326,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X2),X4))),X1)),
inference(step,[status(thm)],[t3970,t6]) ).
cnf(t4042,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X2),X4))),X1)) = true,
inference(orient,[status(thm)],[t210326]) ).
cnf(t4051,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),equivalent(X3,X2))),true),
inference(cp,[status(thm)],[t32,t4042]) ).
cnf(t210328,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),equivalent(X3,X2))),
inference(step,[status(thm)],[t4051,t6]) ).
cnf(t4176,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),equivalent(X3,X2))) = true,
inference(orient,[status(thm)],[t210328]) ).
cnf(t4220,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X1)),X3)),X2)),true),
inference(cp,[status(thm)],[t440,t4176]) ).
cnf(t210334,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X1)),X3)),X2)),
inference(step,[status(thm)],[t4220,t6]) ).
cnf(t4623,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X1)),X3)),X2)) = true,
inference(orient,[status(thm)],[t210334]) ).
cnf(t4641,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X1),X2))),true),
inference(cp,[status(thm)],[t3719,t4623]) ).
cnf(t210335,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X1),X2))),
inference(step,[status(thm)],[t4641,t6]) ).
cnf(t4685,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X1),X2))) = true,
inference(orient,[status(thm)],[t210335]) ).
cnf(t4686,plain,
true = ifeq(true,true,ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(X2,X1),X2)),true),true),
inference(cp,[status(thm)],[t11,t4685]) ).
cnf(t210336,plain,
true = ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(X2,X1),X2)),true),
inference(step,[status(thm)],[t4686,t6]) ).
cnf(t4765,plain,
ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(X2,X1),X2)),true) = true,
inference(orient,[status(thm)],[t210336]) ).
cnf(t4777,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3))),X1)),true),
inference(cp,[status(thm)],[t4765,t4685]) ).
cnf(t210340,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3))),X1)),
inference(step,[status(thm)],[t4777,t6]) ).
cnf(t5115,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3))),X1)) = true,
inference(orient,[status(thm)],[t210340]) ).
cnf(t5120,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X1),X2)),true),
inference(cp,[status(thm)],[t27,t5115]) ).
cnf(t210341,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X1),X2)),
inference(step,[status(thm)],[t5120,t6]) ).
cnf(t5193,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X1),X2)) = true,
inference(orient,[status(thm)],[t210341]) ).
cnf(t5194,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(X1,X2),X1)),true,is_a_theorem(X2),true),true),
inference(cp,[status(thm)],[t11,t5193]) ).
cnf(t210342,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,X2),X1)),true,is_a_theorem(X2),true),
inference(step,[status(thm)],[t5194,t6]) ).
cnf(t5262,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,X2),X1)),true,is_a_theorem(X2),true) = true,
inference(orient,[status(thm)],[t210342]) ).
cnf(t5263,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X1)),X2)),true),
inference(cp,[status(thm)],[t5262,t4623]) ).
cnf(t210343,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X1)),X2)),
inference(step,[status(thm)],[t5263,t6]) ).
cnf(t5343,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X1)),X2)) = true,
inference(orient,[status(thm)],[t210343]) ).
cnf(t5344,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X1))),true,is_a_theorem(X2),true),true),
inference(cp,[status(thm)],[t11,t5343]) ).
cnf(t210347,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X1))),true,is_a_theorem(X2),true),
inference(step,[status(thm)],[t5344,t6]) ).
cnf(t5558,plain,
ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X1))),true,is_a_theorem(X2),true) = true,
inference(orient,[status(thm)],[t210347]) ).
cnf(t3074,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X4)),X3)),equivalent(X4,X2))),true,is_a_theorem(X1),true),true),
inference(cp,[status(thm)],[t11,t3073]) ).
cnf(t210314,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X4)),X3)),equivalent(X4,X2))),true,is_a_theorem(X1),true),
inference(step,[status(thm)],[t3074,t6]) ).
cnf(t3364,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X4)),X3)),equivalent(X4,X2))),true,is_a_theorem(X1),true) = true,
inference(orient,[status(thm)],[t210314]) ).
cnf(t4189,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X1),X3)),true),
inference(cp,[status(thm)],[t3364,t4176]) ).
cnf(t210332,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X1),X3)),
inference(step,[status(thm)],[t4189,t6]) ).
cnf(t4479,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X2),X1),X3)) = true,
inference(orient,[status(thm)],[t210332]) ).
cnf(t4483,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(X3,X2)),X3))),true),
inference(cp,[status(thm)],[t27,t4479]) ).
cnf(t210338,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(X3,X2)),X3))),
inference(step,[status(thm)],[t4483,t6]) ).
cnf(t4939,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),equivalent(X3,X2)),X3))) = true,
inference(orient,[status(thm)],[t210338]) ).
cnf(t5559,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X2,X1))),true),
inference(cp,[status(thm)],[t5558,t4939]) ).
cnf(t210348,plain,
true = is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X2,X1))),
inference(step,[status(thm)],[t5559,t6]) ).
cnf(t5649,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X2,X1))) = true,
inference(orient,[status(thm)],[t210348]) ).
cnf(t5650,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(X2,X1)),true),true),
inference(cp,[status(thm)],[t11,t5649]) ).
cnf(t210358,plain,
true = ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(X2,X1)),true),
inference(step,[status(thm)],[t5650,t6]) ).
cnf(t6478,plain,
ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(X2,X1)),true) = true,
inference(orient,[status(thm)],[t210358]) ).
cnf(t348,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X5),X4)),equivalent(X1,X5))))),true,is_a_theorem(X2),true),true),
inference(cp,[status(thm)],[t11,t347]) ).
cnf(t210253,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X5),X4)),equivalent(X1,X5))))),true,is_a_theorem(X2),true),
inference(step,[status(thm)],[t348,t6]) ).
cnf(t489,plain,
ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(equivalent(X4,X3),X5),X4)),equivalent(X1,X5))))),true,is_a_theorem(X2),true) = true,
inference(orient,[status(thm)],[t210253]) ).
cnf(t6480,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X1)),X3),X2)),true),
inference(cp,[status(thm)],[t6478,t4939]) ).
cnf(t210394,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X1)),X3),X2)),
inference(step,[status(thm)],[t6480,t6]) ).
cnf(t9691,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X1)),X3),X2)) = true,
inference(orient,[status(thm)],[t210394]) ).
cnf(t9707,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)))),true),
inference(cp,[status(thm)],[t27,t9691]) ).
cnf(t210499,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)))),
inference(step,[status(thm)],[t9707,t6]) ).
cnf(t18848,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)))) = true,
inference(orient,[status(thm)],[t210499]) ).
cnf(t18904,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),X3),X2)),true),
inference(cp,[status(thm)],[t489,t18848]) ).
cnf(t210542,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),X3),X2)),
inference(step,[status(thm)],[t18904,t6]) ).
cnf(t22610,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),X3),X2)) = true,
inference(orient,[status(thm)],[t210542]) ).
cnf(t22626,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(X3,X1)),X2))),true),
inference(cp,[status(thm)],[t27,t22610]) ).
cnf(t210569,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(X3,X1)),X2))),
inference(step,[status(thm)],[t22626,t6]) ).
cnf(t24918,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(X3,X1)),X2))) = true,
inference(orient,[status(thm)],[t210569]) ).
cnf(t24922,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X2,X3)),X1),X3)),true),
inference(cp,[status(thm)],[t6478,t24918]) ).
cnf(t210582,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X2,X3)),X1),X3)),
inference(step,[status(thm)],[t24922,t6]) ).
cnf(t26035,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(X2,X3)),X1),X3)) = true,
inference(orient,[status(thm)],[t210582]) ).
cnf(t26053,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),equivalent(X3,X2)))),true),
inference(cp,[status(thm)],[t27,t26035]) ).
cnf(t210590,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),equivalent(X3,X2)))),
inference(step,[status(thm)],[t26053,t6]) ).
cnf(t26725,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X1),X3),equivalent(X3,X2)))) = true,
inference(orient,[status(thm)],[t210590]) ).
cnf(t26758,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),equivalent(X3,equivalent(X1,X2)))),true),
inference(cp,[status(thm)],[t305,t26725]) ).
cnf(t210598,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),equivalent(X3,equivalent(X1,X2)))),
inference(step,[status(thm)],[t26758,t6]) ).
cnf(t27399,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),equivalent(X3,equivalent(X1,X2)))) = true,
inference(orient,[status(thm)],[t210598]) ).
cnf(t27400,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X3))),true,is_a_theorem(equivalent(X3,equivalent(X1,X2))),true),true),
inference(cp,[status(thm)],[t11,t27399]) ).
cnf(t211063,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X3))),true,is_a_theorem(equivalent(X3,equivalent(X1,X2))),true),
inference(step,[status(thm)],[t27400,t6]) ).
cnf(t178310,plain,
ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X3))),true,is_a_theorem(equivalent(X3,equivalent(X1,X2))),true) = true,
inference(orient,[status(thm)],[t211063]) ).
cnf(t4046,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),equivalent(X2,X3))),true),
inference(cp,[status(thm)],[t27,t4042]) ).
cnf(t210327,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),equivalent(X2,X3))),
inference(step,[status(thm)],[t4046,t6]) ).
cnf(t4110,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X1),equivalent(X2,X3))) = true,
inference(orient,[status(thm)],[t210327]) ).
cnf(t4111,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),X1)),true,is_a_theorem(equivalent(X2,X3)),true),true),
inference(cp,[status(thm)],[t11,t4110]) ).
cnf(t210618,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),X1)),true,is_a_theorem(equivalent(X2,X3)),true),
inference(step,[status(thm)],[t4111,t6]) ).
cnf(t29125,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),X1)),true,is_a_theorem(equivalent(X2,X3)),true) = true,
inference(orient,[status(thm)],[t210618]) ).
cnf(t178326,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,X3),equivalent(X3,X2))))),true),
inference(cp,[status(thm)],[t178310,t24918]) ).
cnf(t211078,plain,
true = is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,X3),equivalent(X3,X2))))),
inference(step,[status(thm)],[t178326,t6]) ).
cnf(t182923,plain,
is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X1,X3),equivalent(X3,X2))))) = true,
inference(orient,[status(thm)],[t211078]) ).
cnf(t182927,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(X3,X1))),X2)),true),
inference(cp,[status(thm)],[t6478,t182923]) ).
cnf(t211115,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(X3,X1))),X2)),
inference(step,[status(thm)],[t182927,t6]) ).
cnf(t194025,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(X3,X1))),X2)) = true,
inference(orient,[status(thm)],[t211115]) ).
cnf(t194141,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(X3,equivalent(X2,X1))))),true),
inference(cp,[status(thm)],[t29125,t194025]) ).
cnf(t211148,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(X3,equivalent(X2,X1))))),
inference(step,[status(thm)],[t194141,t6]) ).
cnf(t204336,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(X3,equivalent(X2,X1))))) = true,
inference(orient,[status(thm)],[t211148]) ).
cnf(t204340,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),equivalent(X3,equivalent(X2,X1)))),true),
inference(cp,[status(thm)],[t178310,t204336]) ).
cnf(t211158,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),equivalent(X3,equivalent(X2,X1)))),
inference(step,[status(thm)],[t204340,t6]) ).
cnf(t207523,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X3)),equivalent(X3,equivalent(X2,X1)))) = true,
inference(orient,[status(thm)],[t211158]) ).
cnf(t207527,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X1,X3)),X3))),true),
inference(cp,[status(thm)],[t178310,t207523]) ).
cnf(t211164,plain,
true = is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X1,X3)),X3))),
inference(step,[status(thm)],[t207527,t6]) ).
cnf(t209357,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X1,X3)),X3))) = true,
inference(orient,[status(thm)],[t211164]) ).
cnf(t209361,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X3),equivalent(X2,X1))),true),
inference(cp,[status(thm)],[t6478,t209357]) ).
cnf(t211166,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X3),equivalent(X2,X1))),
inference(step,[status(thm)],[t209361,t6]) ).
cnf(t209943,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X3)),X3),equivalent(X2,X1))) = true,
inference(orient,[status(thm)],[t211166]) ).
cnf(f2,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_pyo) ).
fof(f2_nnf,plain,
~ is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
~ is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
~ is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(goal_0,negated_conjecture,
is_a_theorem(equivalent(equivalent(equivalent(a,equivalent(b,c)),c),equivalent(b,a))) != true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t209943]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL018-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.17/0.43 % Computer : n019.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Wed Sep 23 21:37:50 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 101.91/13.60 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 101.91/13.60 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------