%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL166-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 : n006.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:01:07 PM UTC 2026
% Result : Unsatisfiable 232.42s 35.99s
% Output : Proof 232.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 4
% Syntax : Number of formulae : 257 ( 253 unt; 0 def)
% Number of atoms : 265 ( 244 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 : 14 ( 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 : 1101 ( 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(t2,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(t7,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)],[t2]) ).
cnf(f1,axiom,
is_a_theorem(equivalent(X,equivalent(equivalent(Y,Z),equivalent(equivalent(Z,X),Y)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xhn) ).
fof(f1_nnf,plain,
! [X,Y,Z] : is_a_theorem(equivalent(X,equivalent(equivalent(Y,Z),equivalent(equivalent(Z,X),Y)))),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z] : is_a_theorem(equivalent(X,equivalent(equivalent(Y,Z),equivalent(equivalent(Z,X),Y)))),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X0),X1)))),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t1,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)))) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t5,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)))) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t10,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4)),true,ifeq(true,true,is_a_theorem(X4),true),true),
inference(cp,[status(thm)],[t7,t5]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t4,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t749289,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4)),true,is_a_theorem(X4),true),
inference(step,[status(thm)],[t10,t4]) ).
cnf(t16,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4)),true,is_a_theorem(X4),true) = true,
inference(orient,[status(thm)],[t749289]) ).
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(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X0),X1)))) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t3,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,hi1]) ).
cnf(t6,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1))) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t17,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5)))),X3)),true),
inference(cp,[status(thm)],[t16,t6]) ).
cnf(t749291,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5)))),X3)),
inference(step,[status(thm)],[t17,t4]) ).
cnf(t32,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5)))),X3)) = true,
inference(orient,[status(thm)],[t749291]) ).
cnf(t34,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5)))),X3),Y6)),true,ifeq(true,true,is_a_theorem(Y6),true),true),
inference(cp,[status(thm)],[t7,t32]) ).
cnf(t749295,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5)))),X3),Y6)),true,is_a_theorem(Y6),true),
inference(step,[status(thm)],[t34,t4]) ).
cnf(t84,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5)))),X3),Y6)),true,is_a_theorem(Y6),true) = true,
inference(orient,[status(thm)],[t749295]) ).
cnf(t9,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),true),true),
inference(cp,[status(thm)],[t7,t6]) ).
cnf(t749290,plain,
true = ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),true),
inference(step,[status(thm)],[t9,t4]) ).
cnf(t22,plain,
ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),true) = true,
inference(orient,[status(thm)],[t749290]) ).
cnf(t24,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X4),equivalent(equivalent(X4,X2),X3)))),X5),equivalent(Y5,equivalent(equivalent(Y6,Y7),equivalent(equivalent(Y7,Y5),Y6)))),equivalent(X5,X1))),true),
inference(cp,[status(thm)],[t22,t6]) ).
cnf(t749297,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X4),equivalent(equivalent(X4,X2),X3)))),X5),equivalent(Y5,equivalent(equivalent(Y6,Y7),equivalent(equivalent(Y7,Y5),Y6)))),equivalent(X5,X1))),
inference(step,[status(thm)],[t24,t4]) ).
cnf(t101,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X4),equivalent(equivalent(X4,X2),X3)))),X5),equivalent(Y5,equivalent(equivalent(Y6,Y7),equivalent(equivalent(Y7,Y5),Y6)))),equivalent(X5,X1))) = true,
inference(orient,[status(thm)],[t749297]) ).
cnf(t111,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),equivalent(equivalent(equivalent(X4,X5),equivalent(equivalent(X5,equivalent(Y5,equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X4)),Y5))),true),
inference(cp,[status(thm)],[t84,t101]) ).
cnf(t749311,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),equivalent(equivalent(equivalent(X4,X5),equivalent(equivalent(X5,equivalent(Y5,equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X4)),Y5))),
inference(step,[status(thm)],[t111,t4]) ).
cnf(t347,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),equivalent(equivalent(equivalent(X4,X5),equivalent(equivalent(X5,equivalent(Y5,equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X4)),Y5))) = true,
inference(orient,[status(thm)],[t749311]) ).
cnf(t348,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)))),true,is_a_theorem(equivalent(equivalent(equivalent(X4,X5),equivalent(equivalent(X5,equivalent(Y5,equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X4)),Y5)),true),true),
inference(cp,[status(thm)],[t7,t347]) ).
cnf(t749312,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)))),true,is_a_theorem(equivalent(equivalent(equivalent(X4,X5),equivalent(equivalent(X5,equivalent(Y5,equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X4)),Y5)),true),
inference(step,[status(thm)],[t348,t4]) ).
cnf(t749313,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X4,X5),equivalent(equivalent(X5,equivalent(Y5,equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X4)),Y5)),true),
inference(step,[status(thm)],[t749312,t5]) ).
cnf(t749314,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X4,X5),equivalent(equivalent(X5,equivalent(Y5,equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X4)),Y5)),
inference(step,[status(thm)],[t749313,t4]) ).
cnf(t370,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),X1)),X3)) = true,
inference(orient,[status(thm)],[t749314]) ).
cnf(t371,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),X1))),true,is_a_theorem(X3),true),true),
inference(cp,[status(thm)],[t7,t370]) ).
cnf(t749316,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),X1))),true,is_a_theorem(X3),true),
inference(step,[status(thm)],[t371,t4]) ).
cnf(t416,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),X1))),true,is_a_theorem(X3),true) = true,
inference(orient,[status(thm)],[t749316]) ).
cnf(t8,plain,
true = ifeq(true,true,ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),true),true),
inference(cp,[status(thm)],[t7,t5]) ).
cnf(t749288,plain,
true = ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),true),
inference(step,[status(thm)],[t8,t4]) ).
cnf(t14,plain,
ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),true) = true,
inference(orient,[status(thm)],[t749288]) ).
cnf(t420,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),X4),X3),equivalent(X4,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))),true),
inference(cp,[status(thm)],[t416,t347]) ).
cnf(t749317,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),X4),X3),equivalent(X4,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))),
inference(step,[status(thm)],[t420,t4]) ).
cnf(t439,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),X4),X3),equivalent(X4,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))) = true,
inference(orient,[status(thm)],[t749317]) ).
cnf(t440,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),X4),X3)),true,is_a_theorem(equivalent(X4,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5))))),true),true),
inference(cp,[status(thm)],[t7,t439]) ).
cnf(t749322,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),X4),X3)),true,is_a_theorem(equivalent(X4,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5))))),true),
inference(step,[status(thm)],[t440,t4]) ).
cnf(t569,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),X4),X3)),true,is_a_theorem(equivalent(X4,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5))))),true) = true,
inference(orient,[status(thm)],[t749322]) ).
cnf(t372,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),X1)),X3),Y6)),true,ifeq(true,true,is_a_theorem(Y6),true),true),
inference(cp,[status(thm)],[t7,t370]) ).
cnf(t749320,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),X1)),X3),Y6)),true,is_a_theorem(Y6),true),
inference(step,[status(thm)],[t372,t4]) ).
cnf(t516,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),X1)),X3),Y6)),true,is_a_theorem(Y6),true) = true,
inference(orient,[status(thm)],[t749320]) ).
cnf(t519,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),equivalent(X3,X1)),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),true),
inference(cp,[status(thm)],[t516,t439]) ).
cnf(t749351,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),equivalent(X3,X1)),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),
inference(step,[status(thm)],[t519,t4]) ).
cnf(t1811,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),equivalent(X3,X1)),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))) = true,
inference(orient,[status(thm)],[t749351]) ).
cnf(t1816,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4),equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5))))),true),
inference(cp,[status(thm)],[t569,t1811]) ).
cnf(t749352,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4),equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5))))),
inference(step,[status(thm)],[t1816,t4]) ).
cnf(t1854,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4),equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5))))) = true,
inference(orient,[status(thm)],[t749352]) ).
cnf(t1857,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(equivalent(equivalent(equivalent(equivalent(X3,X4),equivalent(equivalent(X4,equivalent(X5,Y5)),X3)),X5),Y5),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X1))),true),
inference(cp,[status(thm)],[t14,t1854]) ).
cnf(t749378,plain,
true = is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(equivalent(equivalent(equivalent(equivalent(X3,X4),equivalent(equivalent(X4,equivalent(X5,Y5)),X3)),X5),Y5),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X1))),
inference(step,[status(thm)],[t1857,t4]) ).
cnf(t3259,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(equivalent(equivalent(equivalent(equivalent(X3,X4),equivalent(equivalent(X4,equivalent(X5,Y5)),X3)),X5),Y5),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X1))) = true,
inference(orient,[status(thm)],[t749378]) ).
cnf(t3300,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4)),true),
inference(cp,[status(thm)],[t416,t3259]) ).
cnf(t749379,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4)),
inference(step,[status(thm)],[t3300,t4]) ).
cnf(t3333,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4)) = true,
inference(orient,[status(thm)],[t749379]) ).
cnf(t3334,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3)),true,is_a_theorem(X4),true),true),
inference(cp,[status(thm)],[t7,t3333]) ).
cnf(t749380,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3)),true,is_a_theorem(X4),true),
inference(step,[status(thm)],[t3334,t4]) ).
cnf(t3384,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3)),true,is_a_theorem(X4),true) = true,
inference(orient,[status(thm)],[t749380]) ).
cnf(t33,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),true,is_a_theorem(X3),true),true),
inference(cp,[status(thm)],[t7,t32]) ).
cnf(t749293,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),true,is_a_theorem(X3),true),
inference(step,[status(thm)],[t33,t4]) ).
cnf(t48,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),true,is_a_theorem(X3),true) = true,
inference(orient,[status(thm)],[t749293]) ).
cnf(t375,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),true),
inference(cp,[status(thm)],[t48,t370]) ).
cnf(t749315,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))),
inference(step,[status(thm)],[t375,t4]) ).
cnf(t397,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))) = true,
inference(orient,[status(thm)],[t749315]) ).
cnf(t400,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4))),equivalent(Y5,equivalent(equivalent(Y6,Y7),equivalent(equivalent(Y7,Y5),Y6))))),X1))),true),
inference(cp,[status(thm)],[t14,t397]) ).
cnf(t749328,plain,
true = is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4))),equivalent(Y5,equivalent(equivalent(Y6,Y7),equivalent(equivalent(Y7,Y5),Y6))))),X1))),
inference(step,[status(thm)],[t400,t4]) ).
cnf(t750,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4))),equivalent(Y5,equivalent(equivalent(Y6,Y7),equivalent(equivalent(Y7,Y5),Y6))))),X1))) = true,
inference(orient,[status(thm)],[t749328]) ).
cnf(t755,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X3)),true),
inference(cp,[status(thm)],[t16,t750]) ).
cnf(t749367,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X3)),
inference(step,[status(thm)],[t755,t4]) ).
cnf(t2626,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X3),X1)),equivalent(equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))),equivalent(Y6,equivalent(equivalent(Y7,Y8),equivalent(equivalent(Y8,Y6),Y7))))),X3)) = true,
inference(orient,[status(thm)],[t749367]) ).
cnf(t3385,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X4),X2)),equivalent(X5,X1)),X4)),X5)),true),
inference(cp,[status(thm)],[t3384,t2626]) ).
cnf(t749381,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X4),X2)),equivalent(X5,X1)),X4)),X5)),
inference(step,[status(thm)],[t3385,t4]) ).
cnf(t3434,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X4),X2)),equivalent(X5,X1)),X4)),X5)) = true,
inference(orient,[status(thm)],[t749381]) ).
cnf(t3435,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X4),X2)),equivalent(X5,X1)),X4))),true,is_a_theorem(X5),true),true),
inference(cp,[status(thm)],[t7,t3434]) ).
cnf(t749384,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X4),X2)),equivalent(X5,X1)),X4))),true,is_a_theorem(X5),true),
inference(step,[status(thm)],[t3435,t4]) ).
cnf(t3630,plain,
ifeq(is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X4),X2)),equivalent(X5,X1)),X4))),true,is_a_theorem(X5),true) = true,
inference(orient,[status(thm)],[t749384]) ).
cnf(t3344,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X4),equivalent(equivalent(X4,X2),X3)))),equivalent(equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,equivalent(Y6,X1)),X5)),Y6))),true),
inference(cp,[status(thm)],[t22,t3333]) ).
cnf(t749392,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X4),equivalent(equivalent(X4,X2),X3)))),equivalent(equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,equivalent(Y6,X1)),X5)),Y6))),
inference(step,[status(thm)],[t3344,t4]) ).
cnf(t4350,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X4),equivalent(equivalent(X4,X2),X3)))),equivalent(equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,equivalent(Y6,X1)),X5)),Y6))) = true,
inference(orient,[status(thm)],[t749392]) ).
cnf(t4364,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4),X5),equivalent(X4,X5))),true),
inference(cp,[status(thm)],[t3630,t4350]) ).
cnf(t749393,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4),X5),equivalent(X4,X5))),
inference(step,[status(thm)],[t4364,t4]) ).
cnf(t4429,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4),X5),equivalent(X4,X5))) = true,
inference(orient,[status(thm)],[t749393]) ).
cnf(t4430,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4),X5)),true,is_a_theorem(equivalent(X4,X5)),true),true),
inference(cp,[status(thm)],[t7,t4429]) ).
cnf(t749394,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4),X5)),true,is_a_theorem(equivalent(X4,X5)),true),
inference(step,[status(thm)],[t4430,t4]) ).
cnf(t4508,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2))),X4),X5)),true,is_a_theorem(equivalent(X4,X5)),true) = true,
inference(orient,[status(thm)],[t749394]) ).
cnf(t3335,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4),X5)),true,ifeq(true,true,is_a_theorem(X5),true),true),
inference(cp,[status(thm)],[t7,t3333]) ).
cnf(t749383,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4),X5)),true,is_a_theorem(X5),true),
inference(step,[status(thm)],[t3335,t4]) ).
cnf(t3554,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X4)),X1)),X3),X4),X5)),true,is_a_theorem(X5),true) = true,
inference(orient,[status(thm)],[t749383]) ).
cnf(t4396,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),equivalent(Y5,Y5))),true),
inference(cp,[status(thm)],[t416,t4350]) ).
cnf(t749395,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),equivalent(Y5,Y5))),
inference(step,[status(thm)],[t4396,t4]) ).
cnf(t4598,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),equivalent(Y5,Y5))) = true,
inference(orient,[status(thm)],[t749395]) ).
cnf(t4604,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X3)),X1))),true),
inference(cp,[status(thm)],[t3384,t4598]) ).
cnf(t749401,plain,
true = is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X3)),X1))),
inference(step,[status(thm)],[t4604,t4]) ).
cnf(t4811,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X3)),X1))) = true,
inference(orient,[status(thm)],[t749401]) ).
cnf(t4843,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(equivalent(equivalent(X3,X4),equivalent(equivalent(X4,equivalent(X5,X1)),X3)),X5))),true),
inference(cp,[status(thm)],[t3554,t4811]) ).
cnf(t749577,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(equivalent(equivalent(X3,X4),equivalent(equivalent(X4,equivalent(X5,X1)),X3)),X5))),
inference(step,[status(thm)],[t4843,t4]) ).
cnf(t26401,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(equivalent(equivalent(X3,X4),equivalent(equivalent(X4,equivalent(X5,X1)),X3)),X5))) = true,
inference(orient,[status(thm)],[t749577]) ).
cnf(t26495,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X1),X2),X3),equivalent(X2,X3))),true),
inference(cp,[status(thm)],[t3630,t26401]) ).
cnf(t749578,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X1),X2),X3),equivalent(X2,X3))),
inference(step,[status(thm)],[t26495,t4]) ).
cnf(t26548,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X1),X2),X3),equivalent(X2,X3))) = true,
inference(orient,[status(thm)],[t749578]) ).
cnf(t26549,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X1),X2),X3)),true,is_a_theorem(equivalent(X2,X3)),true),true),
inference(cp,[status(thm)],[t7,t26548]) ).
cnf(t749587,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X1),X2),X3)),true,is_a_theorem(equivalent(X2,X3)),true),
inference(step,[status(thm)],[t26549,t4]) ).
cnf(t27888,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X1),X2),X3)),true,is_a_theorem(equivalent(X2,X3)),true) = true,
inference(orient,[status(thm)],[t749587]) ).
cnf(t4599,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1))),true,is_a_theorem(equivalent(Y5,Y5)),true),true),
inference(cp,[status(thm)],[t7,t4598]) ).
cnf(t749396,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1))),true,is_a_theorem(equivalent(Y5,Y5)),true),
inference(step,[status(thm)],[t4599,t4]) ).
cnf(t749397,plain,
true = ifeq(true,true,is_a_theorem(equivalent(Y5,Y5)),true),
inference(step,[status(thm)],[t749396,t6]) ).
cnf(t749398,plain,
true = is_a_theorem(equivalent(Y5,Y5)),
inference(step,[status(thm)],[t749397,t4]) ).
cnf(t4664,plain,
is_a_theorem(equivalent(X1,X1)) = true,
inference(orient,[status(thm)],[t749398]) ).
cnf(t4666,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,X1),X2)),true,ifeq(true,true,is_a_theorem(X2),true),true),
inference(cp,[status(thm)],[t7,t4664]) ).
cnf(t749400,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,X1),X2)),true,is_a_theorem(X2),true),
inference(step,[status(thm)],[t4666,t4]) ).
cnf(t4727,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,X1),X2)),true,is_a_theorem(X2),true) = true,
inference(orient,[status(thm)],[t749400]) ).
cnf(t4815,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X1)),true),
inference(cp,[status(thm)],[t4727,t4811]) ).
cnf(t749402,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X1)),
inference(step,[status(thm)],[t4815,t4]) ).
cnf(t4912,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X1)) = true,
inference(orient,[status(thm)],[t749402]) ).
cnf(t4940,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,X4))),X1)),X3)),true),
inference(cp,[status(thm)],[t3554,t4912]) ).
cnf(t749420,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,X4))),X1)),X3)),
inference(step,[status(thm)],[t4940,t4]) ).
cnf(t6501,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X4,X4))),X1)),X3)) = true,
inference(orient,[status(thm)],[t749420]) ).
cnf(t27892,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,X3))),X1),X2)),true),
inference(cp,[status(thm)],[t27888,t6501]) ).
cnf(t749588,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,X3))),X1),X2)),
inference(step,[status(thm)],[t27892,t4]) ).
cnf(t28407,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,X3))),X1),X2)) = true,
inference(orient,[status(thm)],[t749588]) ).
cnf(t28505,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X1),X2))),true),
inference(cp,[status(thm)],[t4508,t28407]) ).
cnf(t749589,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X1),X2))),
inference(step,[status(thm)],[t28505,t4]) ).
cnf(t28572,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X1),X2))) = true,
inference(orient,[status(thm)],[t749589]) ).
cnf(t28573,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)],[t7,t28572]) ).
cnf(t749590,plain,
true = ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(X2,X1),X2)),true),
inference(step,[status(thm)],[t28573,t4]) ).
cnf(t28731,plain,
ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(X2,X1),X2)),true) = true,
inference(orient,[status(thm)],[t749590]) ).
cnf(t28732,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3))),X1)),true),
inference(cp,[status(thm)],[t28731,t28572]) ).
cnf(t749594,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3))),X1)),
inference(step,[status(thm)],[t28732,t4]) ).
cnf(t29362,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3))),X1)) = true,
inference(orient,[status(thm)],[t749594]) ).
cnf(t29363,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3)))),true,is_a_theorem(X1),true),true),
inference(cp,[status(thm)],[t7,t29362]) ).
cnf(t749607,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3)))),true,is_a_theorem(X1),true),
inference(step,[status(thm)],[t29363,t4]) ).
cnf(t31636,plain,
ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X2),X3)))),true,is_a_theorem(X1),true) = true,
inference(orient,[status(thm)],[t749607]) ).
cnf(t28591,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X3),X4))),X1))),true),
inference(cp,[status(thm)],[t14,t28572]) ).
cnf(t749687,plain,
true = is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X3),X4))),X1))),
inference(step,[status(thm)],[t28591,t4]) ).
cnf(t46840,plain,
is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X3),X4))),X1))) = true,
inference(orient,[status(thm)],[t749687]) ).
cnf(t46909,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X3),X4)))),X1),X2)),true),
inference(cp,[status(thm)],[t31636,t46840]) ).
cnf(t749914,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X3),X4)))),X1),X2)),
inference(step,[status(thm)],[t46909,t4]) ).
cnf(t90522,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X3),X4)))),X1),X2)) = true,
inference(orient,[status(thm)],[t749914]) ).
cnf(t90665,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X2),X3))),true),
inference(cp,[status(thm)],[t4508,t90522]) ).
cnf(t749915,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X2),X3))),
inference(step,[status(thm)],[t90665,t4]) ).
cnf(t90735,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X2),X3))) = true,
inference(orient,[status(thm)],[t749915]) ).
cnf(t90736,plain,
true = ifeq(true,true,ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X2),X3)),true),true),
inference(cp,[status(thm)],[t7,t90735]) ).
cnf(t749916,plain,
true = ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X2),X3)),true),
inference(step,[status(thm)],[t90736,t4]) ).
cnf(t90935,plain,
ifeq(is_a_theorem(X1),true,is_a_theorem(equivalent(equivalent(equivalent(X2,equivalent(X3,X1)),X2),X3)),true) = true,
inference(orient,[status(thm)],[t749916]) ).
cnf(t4913,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X2))),true,is_a_theorem(X1),true),true),
inference(cp,[status(thm)],[t7,t4912]) ).
cnf(t749403,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X2))),true,is_a_theorem(X1),true),
inference(step,[status(thm)],[t4913,t4]) ).
cnf(t4986,plain,
ifeq(is_a_theorem(equivalent(X1,equivalent(X2,X2))),true,is_a_theorem(X1),true) = true,
inference(orient,[status(thm)],[t749403]) ).
cnf(t26648,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,X4)),X2)),X1))),true),
inference(cp,[status(thm)],[t4508,t26548]) ).
cnf(t749627,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,X4)),X2)),X1))),
inference(step,[status(thm)],[t26648,t4]) ).
cnf(t34947,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,X4)),X2)),X1))) = true,
inference(orient,[status(thm)],[t749627]) ).
cnf(t35083,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X1)),X2),equivalent(X3,X3))),true),
inference(cp,[status(thm)],[t3630,t34947]) ).
cnf(t749628,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X1)),X2),equivalent(X3,X3))),
inference(step,[status(thm)],[t35083,t4]) ).
cnf(t35158,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X1)),X2),equivalent(X3,X3))) = true,
inference(orient,[status(thm)],[t749628]) ).
cnf(t35168,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X1)),X2)),true),
inference(cp,[status(thm)],[t4986,t35158]) ).
cnf(t749629,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X1)),X2)),
inference(step,[status(thm)],[t35168,t4]) ).
cnf(t35321,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X1)),X2)) = true,
inference(orient,[status(thm)],[t749629]) ).
cnf(t35323,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X1)),X2),X3)),true,ifeq(true,true,is_a_theorem(X3),true),true),
inference(cp,[status(thm)],[t7,t35321]) ).
cnf(t749644,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X1)),X2),X3)),true,is_a_theorem(X3),true),
inference(step,[status(thm)],[t35323,t4]) ).
cnf(t38048,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X1)),X2),X3)),true,is_a_theorem(X3),true) = true,
inference(orient,[status(thm)],[t749644]) ).
cnf(t4812,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(equivalent(X2,equivalent(X3,X3)),X1)),true),true),
inference(cp,[status(thm)],[t7,t4811]) ).
cnf(t749405,plain,
true = ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(equivalent(X2,equivalent(X3,X3)),X1)),true),
inference(step,[status(thm)],[t4812,t4]) ).
cnf(t5271,plain,
ifeq(is_a_theorem(equivalent(X1,X2)),true,is_a_theorem(equivalent(equivalent(X2,equivalent(X3,X3)),X1)),true) = true,
inference(orient,[status(thm)],[t749405]) ).
cnf(t5308,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X2)),X3),equivalent(X4,X4)),equivalent(X3,X1))),true),
inference(cp,[status(thm)],[t5271,t4811]) ).
cnf(t749427,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X2)),X3),equivalent(X4,X4)),equivalent(X3,X1))),
inference(step,[status(thm)],[t5308,t4]) ).
cnf(t7115,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,equivalent(X2,X2)),X3),equivalent(X4,X4)),equivalent(X3,X1))) = true,
inference(orient,[status(thm)],[t749427]) ).
cnf(t7154,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(X1,equivalent(X3,X3))),X2))),true),
inference(cp,[status(thm)],[t3554,t7115]) ).
cnf(t749428,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(X1,equivalent(X3,X3))),X2))),
inference(step,[status(thm)],[t7154,t4]) ).
cnf(t7199,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(X1,equivalent(X3,X3))),X2))) = true,
inference(orient,[status(thm)],[t749428]) ).
cnf(t7201,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X1,equivalent(X3,X3))),X2)),X4)),true,ifeq(true,true,is_a_theorem(X4),true),true),
inference(cp,[status(thm)],[t7,t7199]) ).
cnf(t749475,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X1,equivalent(X3,X3))),X2)),X4)),true,is_a_theorem(X4),true),
inference(step,[status(thm)],[t7201,t4]) ).
cnf(t12175,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X1,equivalent(X3,X3))),X2)),X4)),true,is_a_theorem(X4),true) = true,
inference(orient,[status(thm)],[t749475]) ).
cnf(t28656,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(X2,equivalent(X4,X4))),X3))),X1)),true),
inference(cp,[status(thm)],[t12175,t28572]) ).
cnf(t749703,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(X2,equivalent(X4,X4))),X3))),X1)),
inference(step,[status(thm)],[t28656,t4]) ).
cnf(t50237,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,equivalent(X2,equivalent(X4,X4))),X3))),X1)) = true,
inference(orient,[status(thm)],[t749703]) ).
cnf(t50299,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(equivalent(X3,equivalent(X2,equivalent(X4,X4))),X3)),X1))),true),
inference(cp,[status(thm)],[t38048,t50237]) ).
cnf(t749929,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(equivalent(X3,equivalent(X2,equivalent(X4,X4))),X3)),X1))),
inference(step,[status(thm)],[t50299,t4]) ).
cnf(t93955,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(equivalent(X3,equivalent(X2,equivalent(X4,X4))),X3)),X1))) = true,
inference(orient,[status(thm)],[t749929]) ).
cnf(t94122,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)),equivalent(X4,X4)))),true),
inference(cp,[status(thm)],[t3630,t93955]) ).
cnf(t750007,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)),equivalent(X4,X4)))),
inference(step,[status(thm)],[t94122,t4]) ).
cnf(t110999,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,X1),X2)),equivalent(X4,X4)))) = true,
inference(orient,[status(thm)],[t750007]) ).
cnf(t111147,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X2)),X3),equivalent(X3,X1))),true),
inference(cp,[status(thm)],[t3630,t110999]) ).
cnf(t750008,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X2)),X3),equivalent(X3,X1))),
inference(step,[status(thm)],[t111147,t4]) ).
cnf(t111217,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,X2)),X3),equivalent(X3,X1))) = true,
inference(orient,[status(thm)],[t750008]) ).
cnf(t111218,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X3)),true,is_a_theorem(equivalent(X3,X1)),true),true),
inference(cp,[status(thm)],[t7,t111217]) ).
cnf(t750009,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X3)),true,is_a_theorem(equivalent(X3,X1)),true),
inference(step,[status(thm)],[t111218,t4]) ).
cnf(t111396,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),X3)),true,is_a_theorem(equivalent(X3,X1)),true) = true,
inference(orient,[status(thm)],[t750009]) ).
cnf(t35346,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(X3,equivalent(X1,X3)))),true),
inference(cp,[status(thm)],[t5271,t35321]) ).
cnf(t749636,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(X3,equivalent(X1,X3)))),
inference(step,[status(thm)],[t35346,t4]) ).
cnf(t36585,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(X3,equivalent(X1,X3)))) = true,
inference(orient,[status(thm)],[t749636]) ).
cnf(t36592,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X3)),equivalent(X4,equivalent(X2,X4)))),X1)),true),
inference(cp,[status(thm)],[t28731,t36585]) ).
cnf(t749816,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X3)),equivalent(X4,equivalent(X2,X4)))),X1)),
inference(step,[status(thm)],[t36592,t4]) ).
cnf(t71367,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X3)),equivalent(X4,equivalent(X2,X4)))),X1)) = true,
inference(orient,[status(thm)],[t749816]) ).
cnf(t71368,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X3)),equivalent(X4,equivalent(X2,X4))))),true,is_a_theorem(X1),true),true),
inference(cp,[status(thm)],[t7,t71367]) ).
cnf(t750267,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X3)),equivalent(X4,equivalent(X2,X4))))),true,is_a_theorem(X1),true),
inference(step,[status(thm)],[t71368,t4]) ).
cnf(t247424,plain,
ifeq(is_a_theorem(equivalent(X1,equivalent(equivalent(X2,equivalent(X3,X3)),equivalent(X4,equivalent(X2,X4))))),true,is_a_theorem(X1),true) = true,
inference(orient,[status(thm)],[t750267]) ).
cnf(t11,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),Y5)),true,ifeq(true,true,is_a_theorem(Y5),true),true),
inference(cp,[status(thm)],[t7,t6]) ).
cnf(t749292,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),Y5)),true,is_a_theorem(Y5),true),
inference(step,[status(thm)],[t11,t4]) ).
cnf(t41,plain,
ifeq(is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(equivalent(X4,X5),equivalent(equivalent(X5,X3),X4)))),X1)),Y5)),true,is_a_theorem(Y5),true) = true,
inference(orient,[status(thm)],[t749292]) ).
cnf(t113,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,equivalent(X1,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))),X2)),X4))),true),
inference(cp,[status(thm)],[t41,t101]) ).
cnf(t749298,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,equivalent(X1,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))),X2)),X4))),
inference(step,[status(thm)],[t113,t4]) ).
cnf(t118,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,equivalent(X1,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))),X2)),X4))) = true,
inference(orient,[status(thm)],[t749298]) ).
cnf(t120,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,equivalent(X1,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))),X2)),X4)),Y7)),true,ifeq(true,true,is_a_theorem(Y7),true),true),
inference(cp,[status(thm)],[t7,t118]) ).
cnf(t749304,plain,
true = ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,equivalent(X1,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))),X2)),X4)),Y7)),true,is_a_theorem(Y7),true),
inference(step,[status(thm)],[t120,t4]) ).
cnf(t243,plain,
ifeq(is_a_theorem(equivalent(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,equivalent(X1,equivalent(X5,equivalent(equivalent(Y5,Y6),equivalent(equivalent(Y6,X5),Y5)))))),X2)),X4)),Y7)),true,is_a_theorem(Y7),true) = true,
inference(orient,[status(thm)],[t749304]) ).
cnf(t3487,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(equivalent(X3,X1),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))))),true),
inference(cp,[status(thm)],[t243,t3434]) ).
cnf(t749387,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(equivalent(X3,X1),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))))),
inference(step,[status(thm)],[t3487,t4]) ).
cnf(t3816,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(equivalent(X3,X1),equivalent(X4,equivalent(equivalent(X5,Y5),equivalent(equivalent(Y5,X4),X5))))))) = true,
inference(orient,[status(thm)],[t749387]) ).
cnf(t247595,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X4,X4))),equivalent(X3,X1))),true),
inference(cp,[status(thm)],[t247424,t3816]) ).
cnf(t750268,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X4,X4))),equivalent(X3,X1))),
inference(step,[status(thm)],[t247595,t4]) ).
cnf(t248314,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X4,X4))),equivalent(X3,X1))) = true,
inference(orient,[status(thm)],[t750268]) ).
cnf(t248356,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(equivalent(X3,X1),X3))),true),
inference(cp,[status(thm)],[t27888,t248314]) ).
cnf(t750270,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(equivalent(X3,X1),X3))),
inference(step,[status(thm)],[t248356,t4]) ).
cnf(t248999,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X2)),equivalent(equivalent(X3,X1),X3))) = true,
inference(orient,[status(thm)],[t750270]) ).
cnf(t249015,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X1),X2)),true),
inference(cp,[status(thm)],[t111396,t248999]) ).
cnf(t750271,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X1),X2)),
inference(step,[status(thm)],[t249015,t4]) ).
cnf(t249281,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X1),X2)) = true,
inference(orient,[status(thm)],[t750271]) ).
cnf(t249349,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,X4),X3),X4))),X1),X2)),true),
inference(cp,[status(thm)],[t90935,t249281]) ).
cnf(t750330,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,X4),X3),X4))),X1),X2)),
inference(step,[status(thm)],[t249349,t4]) ).
cnf(t273701,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(equivalent(X3,X4),X3),X4))),X1),X2)) = true,
inference(orient,[status(thm)],[t750330]) ).
cnf(t274066,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(X2,equivalent(X1,X2)))),true),
inference(cp,[status(thm)],[t4508,t273701]) ).
cnf(t750331,plain,
true = is_a_theorem(equivalent(X1,equivalent(X2,equivalent(X1,X2)))),
inference(step,[status(thm)],[t274066,t4]) ).
cnf(t274152,plain,
is_a_theorem(equivalent(X1,equivalent(X2,equivalent(X1,X2)))) = true,
inference(orient,[status(thm)],[t750331]) ).
cnf(t274160,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X2,X3)))),X1)),true),
inference(cp,[status(thm)],[t28731,t274152]) ).
cnf(t750334,plain,
true = is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X2,X3)))),X1)),
inference(step,[status(thm)],[t274160,t4]) ).
cnf(t275440,plain,
is_a_theorem(equivalent(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X2,X3)))),X1)) = true,
inference(orient,[status(thm)],[t750334]) ).
cnf(t275441,plain,
true = ifeq(true,true,ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X2,X3))))),true,is_a_theorem(X1),true),true),
inference(cp,[status(thm)],[t7,t275440]) ).
cnf(t750341,plain,
true = ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X2,X3))))),true,is_a_theorem(X1),true),
inference(step,[status(thm)],[t275441,t4]) ).
cnf(t278605,plain,
ifeq(is_a_theorem(equivalent(X1,equivalent(X2,equivalent(X3,equivalent(X2,X3))))),true,is_a_theorem(X1),true) = true,
inference(orient,[status(thm)],[t750341]) ).
cnf(t278793,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X2),equivalent(X3,X1))),true),
inference(cp,[status(thm)],[t278605,t3816]) ).
cnf(t750342,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X2),equivalent(X3,X1))),
inference(step,[status(thm)],[t278793,t4]) ).
cnf(t279592,plain,
is_a_theorem(equivalent(equivalent(equivalent(equivalent(X1,X2),X3),X2),equivalent(X3,X1))) = true,
inference(orient,[status(thm)],[t750342]) ).
cnf(t279888,plain,
true = ifeq(true,true,is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,X1)),X2)),X4))),true),
inference(cp,[status(thm)],[t4508,t279592]) ).
cnf(t751053,plain,
true = is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,X1)),X2)),X4))),
inference(step,[status(thm)],[t279888,t4]) ).
cnf(t748057,plain,
is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(equivalent(X3,equivalent(X4,X1)),X2)),X4))) = true,
inference(orient,[status(thm)],[t751053]) ).
cnf(t748649,plain,
true = ifeq(true,true,is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X3,X1)))),true),
inference(cp,[status(thm)],[t3630,t748057]) ).
cnf(t751054,plain,
true = is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X3,X1)))),
inference(step,[status(thm)],[t748649,t4]) ).
cnf(t748722,plain,
is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X3),equivalent(X2,equivalent(X3,X1)))) = true,
inference(orient,[status(thm)],[t751054]) ).
cnf(f2,negated_conjecture,
~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(b,equivalent(c,a)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_um) ).
fof(f2_nnf,plain,
~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(b,equivalent(c,a)))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(b,equivalent(c,a)))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
~ is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(b,equivalent(c,a)))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(goal_0,negated_conjecture,
is_a_theorem(equivalent(equivalent(equivalent(a,b),c),equivalent(b,equivalent(c,a)))) != true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t748722]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL166-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n006.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 22:07:41 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 232.42/35.99 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 232.42/35.99 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------