%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL016-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n018.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:34:45 PM UTC 2026
% Result : Unsatisfiable 137.16s 20.58s
% Output : Proof 137.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 33
% Syntax : Number of formulae : 667 ( 663 unt; 0 def)
% Number of atoms : 671 ( 670 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 15 ( 11 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 12 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 27 con; 0-4 aty)
% Number of variables : 312 ( 14 sgn 44 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f13,negated_conjecture,
( join(meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3)))
| join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))) != meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f13_nnf,plain,
( join(meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3)))
| join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))) != meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
( join(meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3)))
| join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))) != meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( join(meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3)))
| join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))) != meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(u1,axiom,
ifeq(join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),ifeq(join(meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))),meet(composition(sk1,sk2),complement(composition(sk1,sk3))),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(f3,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet_4) ).
fof(f3_nnf,plain,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(d0,axiom,
meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t13,plain,
ifeq(join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t14,axiom,
sF0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t38,plain,
composition(sk1,sk2) = sF0,
inference(orient,[status(thm)],[t14]) ).
cnf(t90023,plain,
ifeq(join(complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t13,t38]) ).
cnf(t15,axiom,
sF1 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t90004,plain,
sF1 = complement(sF0),
inference(step,[status(thm)],[t15,t38]) ).
cnf(t49,plain,
complement(sF0) = sF1,
inference(orient,[status(thm)],[t90004]) ).
cnf(t90024,plain,
ifeq(join(complement(join(sF1,complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90023,t49]) ).
cnf(t16,axiom,
sF2 = composition(sk1,sk3),
introduced(definition) ).
cnf(t39,plain,
composition(sk1,sk3) = sF2,
inference(orient,[status(thm)],[t16]) ).
cnf(t90025,plain,
ifeq(join(complement(join(sF1,complement(complement(sF2)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90024,t39]) ).
cnf(t17,axiom,
sF3 = complement(composition(sk1,sk3)),
introduced(definition) ).
cnf(t90005,plain,
sF3 = complement(sF2),
inference(step,[status(thm)],[t17,t39]) ).
cnf(t52,plain,
complement(sF2) = sF3,
inference(orient,[status(thm)],[t90005]) ).
cnf(t90026,plain,
ifeq(join(complement(join(sF1,complement(sF3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90025,t52]) ).
cnf(t18,axiom,
sF4 = complement(complement(composition(sk1,sk3))),
introduced(definition) ).
cnf(t90006,plain,
sF4 = complement(complement(sF2)),
inference(step,[status(thm)],[t18,t39]) ).
cnf(t90007,plain,
sF4 = complement(sF3),
inference(step,[status(thm)],[t90006,t52]) ).
cnf(t75,plain,
complement(sF3) = sF4,
inference(orient,[status(thm)],[t90007]) ).
cnf(t90027,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90026,t75]) ).
cnf(f0,axiom,
join(A,B) = join(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
fof(f0_nnf,plain,
! [A,B] : join(A,B) = join(B,A),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] : join(A,B) = join(B,A),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t4,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t77,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t90028,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90027,t77]) ).
cnf(t90029,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90028,t39]) ).
cnf(t90030,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90029,t52]) ).
cnf(t90031,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90030,t75]) ).
cnf(t21,axiom,
sF7 = complement(sk2),
introduced(definition) ).
cnf(t34,plain,
complement(sk2) = sF7,
inference(orient,[status(thm)],[t21]) ).
cnf(t90032,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90031,t34]) ).
cnf(t22,axiom,
sF8 = complement(sk3),
introduced(definition) ).
cnf(t35,plain,
complement(sk3) = sF8,
inference(orient,[status(thm)],[t22]) ).
cnf(t90033,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8)))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90032,t35]) ).
cnf(t23,axiom,
sF9 = complement(complement(sk3)),
introduced(definition) ).
cnf(t90003,plain,
sF9 = complement(sF8),
inference(step,[status(thm)],[t23,t35]) ).
cnf(t40,plain,
complement(sF8) = sF9,
inference(orient,[status(thm)],[t90003]) ).
cnf(t90034,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90033,t40]) ).
cnf(t90035,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90034,t77]) ).
cnf(t90036,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90035,t39]) ).
cnf(t90037,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90036,t52]) ).
cnf(t90038,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90037,t75]) ).
cnf(t90039,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90038,t34]) ).
cnf(t90040,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90039,t35]) ).
cnf(t90041,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90040,t40]) ).
cnf(t90042,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90041,t77]) ).
cnf(t90043,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90042,t38]) ).
cnf(t90044,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90043,t49]) ).
cnf(t90045,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,complement(complement(sF2)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90044,t39]) ).
cnf(t90046,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,complement(sF3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90045,t52]) ).
cnf(t90047,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90046,t75]) ).
cnf(t90048,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90047,t77]) ).
cnf(t90049,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90048,t39]) ).
cnf(t90050,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90049,t52]) ).
cnf(t90051,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90050,t75]) ).
cnf(t90052,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90051,t34]) ).
cnf(t90053,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8)))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90052,t35]) ).
cnf(t90054,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90053,t40]) ).
cnf(t90055,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90054,t38]) ).
cnf(t90056,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF1,complement(complement(composition(sk1,sk3))))),false,true),true) = true,
inference(step,[status(thm)],[t90055,t49]) ).
cnf(t90057,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF1,complement(complement(sF2)))),false,true),true) = true,
inference(step,[status(thm)],[t90056,t39]) ).
cnf(t90058,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF1,complement(sF3))),false,true),true) = true,
inference(step,[status(thm)],[t90057,t52]) ).
cnf(t90059,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF1,sF4)),false,true),true) = true,
inference(step,[status(thm)],[t90058,t75]) ).
cnf(t294,plain,
ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF1,sF4)),false,true),true) = true,
inference(orient,[status(thm)],[t90059]) ).
cnf(t19,axiom,
sF5 = join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))),
introduced(definition) ).
cnf(t90072,plain,
sF5 = join(complement(sF0),complement(complement(composition(sk1,sk3)))),
inference(step,[status(thm)],[t19,t38]) ).
cnf(t90073,plain,
sF5 = join(sF1,complement(complement(composition(sk1,sk3)))),
inference(step,[status(thm)],[t90072,t49]) ).
cnf(t90074,plain,
sF5 = join(sF1,complement(complement(sF2))),
inference(step,[status(thm)],[t90073,t39]) ).
cnf(t90075,plain,
sF5 = join(sF1,complement(sF3)),
inference(step,[status(thm)],[t90074,t52]) ).
cnf(t90076,plain,
sF5 = join(sF1,sF4),
inference(step,[status(thm)],[t90075,t75]) ).
cnf(t345,plain,
join(sF1,sF4) = sF5,
inference(orient,[status(thm)],[t90076]) ).
cnf(t90077,plain,
ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(sF1,sF4)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF1,sF4)),false,true),true) = true,
inference(step,[status(thm)],[t294,t345]) ).
cnf(t90078,plain,
ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF1,sF4)),false,true),true) = true,
inference(step,[status(thm)],[t90077,t345]) ).
cnf(t90079,plain,
ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90078,t345]) ).
cnf(t346,plain,
ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(rw,[status(thm)],[t90079]) ).
cnf(t20,axiom,
sF6 = complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
introduced(definition) ).
cnf(t90112,plain,
sF6 = complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),
inference(step,[status(thm)],[t20,t38]) ).
cnf(t90113,plain,
sF6 = complement(join(sF1,complement(complement(composition(sk1,sk3))))),
inference(step,[status(thm)],[t90112,t49]) ).
cnf(t90114,plain,
sF6 = complement(join(sF1,complement(complement(sF2)))),
inference(step,[status(thm)],[t90113,t39]) ).
cnf(t90115,plain,
sF6 = complement(join(sF1,complement(sF3))),
inference(step,[status(thm)],[t90114,t52]) ).
cnf(t90116,plain,
sF6 = complement(join(sF1,sF4)),
inference(step,[status(thm)],[t90115,t75]) ).
cnf(t90117,plain,
sF6 = complement(sF5),
inference(step,[status(thm)],[t90116,t345]) ).
cnf(t391,plain,
complement(sF5) = sF6,
inference(orient,[status(thm)],[t90117]) ).
cnf(t90683,plain,
ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t346,t391]) ).
cnf(f2,axiom,
A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
fof(f2_nnf,plain,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t12,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t90018,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t12,t77]) ).
cnf(t227,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t90018]) ).
cnf(f10,axiom,
join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity_11) ).
fof(f10_nnf,plain,
! [A,B] : join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A,B] : join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t11,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t90015,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t77]) ).
cnf(t179,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t90015]) ).
cnf(f9,axiom,
converse(composition(A,B)) = composition(converse(B),converse(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
fof(f9_nnf,plain,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t6,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t55,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(f7,axiom,
converse(converse(A)) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f7_nnf,plain,
! [A] : converse(converse(A)) = A,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A] : converse(converse(A)) = A,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
converse(converse(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t1,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t37,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t57,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t55,t37]) ).
cnf(t106,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t57]) ).
cnf(f5,axiom,
composition(A,one) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity_6) ).
fof(f5_nnf,plain,
! [A] : composition(A,one) = A,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A] : composition(A,one) = A,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
composition(X0,one) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t0,plain,
composition(X1,one) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t36,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t107,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t106,t36]) ).
cnf(t90012,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t107,t37]) ).
cnf(t110,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t90012]) ).
cnf(t111,plain,
one = converse(one),
inference(cp,[status(thm)],[t110,t36]) ).
cnf(t112,plain,
converse(one) = one,
inference(orient,[status(thm)],[t111]) ).
cnf(t196,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t179,t112]) ).
cnf(t90013,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t110,t112]) ).
cnf(t113,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t90013]) ).
cnf(t117,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t113]) ).
cnf(t90062,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t196,t117]) ).
cnf(t90063,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t90062,t117]) ).
cnf(t323,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t90063]) ).
cnf(t332,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t227,t323]) ).
cnf(f11,axiom,
top = join(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top_12) ).
fof(f11_nnf,plain,
! [A] : top = join(A,complement(A)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A] : top = join(A,complement(A)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
top = join(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t2,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t41,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t90268,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t332,t41]) ).
cnf(t90269,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t90268,t77]) ).
cnf(f12,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero_13) ).
fof(f12_nnf,plain,
! [A] : zero = meet(A,complement(A)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A] : zero = meet(A,complement(A)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(u0,axiom,
zero = meet(X0,complement(X0)),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t5,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t90010,plain,
complement(top) = zero,
inference(step,[status(thm)],[t5,t41]) ).
cnf(t96,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t90010]) ).
cnf(t90270,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t90269,t96]) ).
cnf(t576,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t90270]) ).
cnf(f1,axiom,
join(A,join(B,C)) = join(join(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity_2) ).
fof(f1_nnf,plain,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t9,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t66,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t330,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t323,t96]) ).
cnf(t90084,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t330,t96]) ).
cnf(t90085,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t90084,t96]) ).
cnf(t356,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t90085]) ).
cnf(t357,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t66,t356]) ).
cnf(t1426,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t357]) ).
cnf(t1428,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t1426,t576]) ).
cnf(t90390,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t1428,t576]) ).
cnf(t1461,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t90390]) ).
cnf(t90392,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t576,t1461]) ).
cnf(t1464,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t90392]) ).
cnf(t1585,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1464]) ).
cnf(t1587,plain,
sF2 = complement(sF3),
inference(cp,[status(thm)],[t1585,t52]) ).
cnf(t90409,plain,
sF2 = sF4,
inference(step,[status(thm)],[t1587,t75]) ).
cnf(t1607,plain,
sF4 = sF2,
inference(orient,[status(thm)],[t90409]) ).
cnf(t90684,plain,
ifeq(join(sF6,complement(join(sF2,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90683,t1607]) ).
cnf(t24,axiom,
sF10 = join(complement(sk2),complement(complement(sk3))),
introduced(definition) ).
cnf(t90122,plain,
sF10 = join(sF7,complement(complement(sk3))),
inference(step,[status(thm)],[t24,t34]) ).
cnf(t90123,plain,
sF10 = join(sF7,complement(sF8)),
inference(step,[status(thm)],[t90122,t35]) ).
cnf(t90124,plain,
sF10 = join(sF7,sF9),
inference(step,[status(thm)],[t90123,t40]) ).
cnf(t407,plain,
join(sF7,sF9) = sF10,
inference(orient,[status(thm)],[t90124]) ).
cnf(t90685,plain,
ifeq(join(sF6,complement(join(sF2,complement(composition(sk1,complement(sF10)))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90684,t407]) ).
cnf(t25,axiom,
sF11 = complement(join(complement(sk2),complement(complement(sk3)))),
introduced(definition) ).
cnf(t90129,plain,
sF11 = complement(join(sF7,complement(complement(sk3)))),
inference(step,[status(thm)],[t25,t34]) ).
cnf(t90130,plain,
sF11 = complement(join(sF7,complement(sF8))),
inference(step,[status(thm)],[t90129,t35]) ).
cnf(t90131,plain,
sF11 = complement(join(sF7,sF9)),
inference(step,[status(thm)],[t90130,t40]) ).
cnf(t90132,plain,
sF11 = complement(sF10),
inference(step,[status(thm)],[t90131,t407]) ).
cnf(t427,plain,
complement(sF10) = sF11,
inference(orient,[status(thm)],[t90132]) ).
cnf(t90686,plain,
ifeq(join(sF6,complement(join(sF2,complement(composition(sk1,sF11))))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90685,t427]) ).
cnf(t26,axiom,
sF12 = composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))),
introduced(definition) ).
cnf(t90137,plain,
sF12 = composition(sk1,complement(join(sF7,complement(complement(sk3))))),
inference(step,[status(thm)],[t26,t34]) ).
cnf(t90138,plain,
sF12 = composition(sk1,complement(join(sF7,complement(sF8)))),
inference(step,[status(thm)],[t90137,t35]) ).
cnf(t90139,plain,
sF12 = composition(sk1,complement(join(sF7,sF9))),
inference(step,[status(thm)],[t90138,t40]) ).
cnf(t90140,plain,
sF12 = composition(sk1,complement(sF10)),
inference(step,[status(thm)],[t90139,t407]) ).
cnf(t90141,plain,
sF12 = composition(sk1,sF11),
inference(step,[status(thm)],[t90140,t427]) ).
cnf(t454,plain,
composition(sk1,sF11) = sF12,
inference(orient,[status(thm)],[t90141]) ).
cnf(t90687,plain,
ifeq(join(sF6,complement(join(sF2,complement(sF12)))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90686,t454]) ).
cnf(t27,axiom,
sF13 = complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),
introduced(definition) ).
cnf(t90152,plain,
sF13 = complement(composition(sk1,complement(join(sF7,complement(complement(sk3)))))),
inference(step,[status(thm)],[t27,t34]) ).
cnf(t90153,plain,
sF13 = complement(composition(sk1,complement(join(sF7,complement(sF8))))),
inference(step,[status(thm)],[t90152,t35]) ).
cnf(t90154,plain,
sF13 = complement(composition(sk1,complement(join(sF7,sF9)))),
inference(step,[status(thm)],[t90153,t40]) ).
cnf(t90155,plain,
sF13 = complement(composition(sk1,complement(sF10))),
inference(step,[status(thm)],[t90154,t407]) ).
cnf(t90156,plain,
sF13 = complement(composition(sk1,sF11)),
inference(step,[status(thm)],[t90155,t427]) ).
cnf(t90157,plain,
sF13 = complement(sF12),
inference(step,[status(thm)],[t90156,t454]) ).
cnf(t480,plain,
complement(sF12) = sF13,
inference(orient,[status(thm)],[t90157]) ).
cnf(t90688,plain,
ifeq(join(sF6,complement(join(sF2,sF13))),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90687,t480]) ).
cnf(t28,axiom,
sF14 = join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))),
introduced(definition) ).
cnf(t90161,plain,
sF14 = join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t28,t77]) ).
cnf(t90162,plain,
sF14 = join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t90161,t39]) ).
cnf(t90163,plain,
sF14 = join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t90162,t52]) ).
cnf(t90164,plain,
sF14 = join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t90163,t75]) ).
cnf(t90165,plain,
sF14 = join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3))))))),
inference(step,[status(thm)],[t90164,t34]) ).
cnf(t90166,plain,
sF14 = join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8)))))),
inference(step,[status(thm)],[t90165,t35]) ).
cnf(t90167,plain,
sF14 = join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))),
inference(step,[status(thm)],[t90166,t40]) ).
cnf(t90168,plain,
sF14 = join(sF4,complement(composition(sk1,complement(sF10)))),
inference(step,[status(thm)],[t90167,t407]) ).
cnf(t90169,plain,
sF14 = join(sF4,complement(composition(sk1,sF11))),
inference(step,[status(thm)],[t90168,t427]) ).
cnf(t90170,plain,
sF14 = join(sF4,complement(sF12)),
inference(step,[status(thm)],[t90169,t454]) ).
cnf(t90171,plain,
sF14 = join(sF4,sF13),
inference(step,[status(thm)],[t90170,t480]) ).
cnf(t507,plain,
join(sF4,sF13) = sF14,
inference(orient,[status(thm)],[t90171]) ).
cnf(t90414,plain,
join(sF2,sF13) = sF14,
inference(step,[status(thm)],[t507,t1607]) ).
cnf(t1616,plain,
join(sF2,sF13) = sF14,
inference(rw,[status(thm)],[t90414]) ).
cnf(t1786,plain,
join(sF2,sF13) = sF14,
inference(orient,[status(thm)],[t1616]) ).
cnf(t90689,plain,
ifeq(join(sF6,complement(sF14)),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90688,t1786]) ).
cnf(t29,axiom,
sF15 = complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),
introduced(definition) ).
cnf(t90174,plain,
sF15 = complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t29,t77]) ).
cnf(t90175,plain,
sF15 = complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t90174,t39]) ).
cnf(t90176,plain,
sF15 = complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t90175,t52]) ).
cnf(t90177,plain,
sF15 = complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t90176,t75]) ).
cnf(t90178,plain,
sF15 = complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3)))))))),
inference(step,[status(thm)],[t90177,t34]) ).
cnf(t90179,plain,
sF15 = complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8))))))),
inference(step,[status(thm)],[t90178,t35]) ).
cnf(t90180,plain,
sF15 = complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),
inference(step,[status(thm)],[t90179,t40]) ).
cnf(t90181,plain,
sF15 = complement(join(sF4,complement(composition(sk1,complement(sF10))))),
inference(step,[status(thm)],[t90180,t407]) ).
cnf(t90182,plain,
sF15 = complement(join(sF4,complement(composition(sk1,sF11)))),
inference(step,[status(thm)],[t90181,t427]) ).
cnf(t90183,plain,
sF15 = complement(join(sF4,complement(sF12))),
inference(step,[status(thm)],[t90182,t454]) ).
cnf(t90184,plain,
sF15 = complement(join(sF4,sF13)),
inference(step,[status(thm)],[t90183,t480]) ).
cnf(t90185,plain,
sF15 = complement(sF14),
inference(step,[status(thm)],[t90184,t507]) ).
cnf(t535,plain,
complement(sF14) = sF15,
inference(orient,[status(thm)],[t90185]) ).
cnf(t90690,plain,
ifeq(join(sF6,sF15),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90689,t535]) ).
cnf(t30,axiom,
sF16 = join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),
introduced(definition) ).
cnf(t90188,plain,
sF16 = join(complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),
inference(step,[status(thm)],[t30,t38]) ).
cnf(t90189,plain,
sF16 = join(complement(join(sF1,complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),
inference(step,[status(thm)],[t90188,t49]) ).
cnf(t90190,plain,
sF16 = join(complement(join(sF1,complement(complement(sF2)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),
inference(step,[status(thm)],[t90189,t39]) ).
cnf(t90191,plain,
sF16 = join(complement(join(sF1,complement(sF3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),
inference(step,[status(thm)],[t90190,t52]) ).
cnf(t90192,plain,
sF16 = join(complement(join(sF1,sF4)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),
inference(step,[status(thm)],[t90191,t75]) ).
cnf(t90193,plain,
sF16 = join(complement(sF5),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),
inference(step,[status(thm)],[t90192,t345]) ).
cnf(t90194,plain,
sF16 = join(sF6,complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),
inference(step,[status(thm)],[t90193,t391]) ).
cnf(t90195,plain,
sF16 = join(sF6,complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),
inference(step,[status(thm)],[t90194,t77]) ).
cnf(t90196,plain,
sF16 = join(sF6,complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),
inference(step,[status(thm)],[t90195,t39]) ).
cnf(t90197,plain,
sF16 = join(sF6,complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),
inference(step,[status(thm)],[t90196,t52]) ).
cnf(t90198,plain,
sF16 = join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),
inference(step,[status(thm)],[t90197,t75]) ).
cnf(t90199,plain,
sF16 = join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3))))))))),
inference(step,[status(thm)],[t90198,t34]) ).
cnf(t90200,plain,
sF16 = join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8)))))))),
inference(step,[status(thm)],[t90199,t35]) ).
cnf(t90201,plain,
sF16 = join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),
inference(step,[status(thm)],[t90200,t40]) ).
cnf(t90202,plain,
sF16 = join(sF6,complement(join(sF4,complement(composition(sk1,complement(sF10)))))),
inference(step,[status(thm)],[t90201,t407]) ).
cnf(t90203,plain,
sF16 = join(sF6,complement(join(sF4,complement(composition(sk1,sF11))))),
inference(step,[status(thm)],[t90202,t427]) ).
cnf(t90204,plain,
sF16 = join(sF6,complement(join(sF4,complement(sF12)))),
inference(step,[status(thm)],[t90203,t454]) ).
cnf(t90205,plain,
sF16 = join(sF6,complement(join(sF4,sF13))),
inference(step,[status(thm)],[t90204,t480]) ).
cnf(t90206,plain,
sF16 = join(sF6,complement(sF14)),
inference(step,[status(thm)],[t90205,t507]) ).
cnf(t90207,plain,
sF16 = join(sF6,sF15),
inference(step,[status(thm)],[t90206,t535]) ).
cnf(t546,plain,
join(sF6,sF15) = sF16,
inference(orient,[status(thm)],[t90207]) ).
cnf(t90691,plain,
ifeq(sF16,complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90690,t546]) ).
cnf(t90692,plain,
ifeq(sF16,complement(join(sF2,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90691,t1607]) ).
cnf(t90693,plain,
ifeq(sF16,complement(join(sF2,complement(composition(sk1,complement(sF10))))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90692,t407]) ).
cnf(t90694,plain,
ifeq(sF16,complement(join(sF2,complement(composition(sk1,sF11)))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90693,t427]) ).
cnf(t90695,plain,
ifeq(sF16,complement(join(sF2,complement(sF12))),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90694,t454]) ).
cnf(t90696,plain,
ifeq(sF16,complement(join(sF2,sF13)),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90695,t480]) ).
cnf(t90697,plain,
ifeq(sF16,complement(sF14),ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90696,t1786]) ).
cnf(t90698,plain,
ifeq(sF16,sF15,ifeq(join(complement(sF5),complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90697,t535]) ).
cnf(t90699,plain,
ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90698,t391]) ).
cnf(t90700,plain,
ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF2,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90699,t1607]) ).
cnf(t90701,plain,
ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF2,complement(composition(sk1,complement(sF10)))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90700,t407]) ).
cnf(t90702,plain,
ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF2,complement(composition(sk1,sF11))))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90701,t427]) ).
cnf(t90703,plain,
ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF2,complement(sF12)))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90702,t454]) ).
cnf(t90704,plain,
ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF2,sF13))),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90703,t480]) ).
cnf(t90705,plain,
ifeq(sF16,sF15,ifeq(join(sF6,complement(sF14)),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90704,t1786]) ).
cnf(t90706,plain,
ifeq(sF16,sF15,ifeq(join(sF6,sF15),complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90705,t535]) ).
cnf(t90707,plain,
ifeq(sF16,sF15,ifeq(sF16,complement(sF5),false,true),true) = true,
inference(step,[status(thm)],[t90706,t546]) ).
cnf(t90708,plain,
ifeq(sF16,sF15,ifeq(sF16,sF6,false,true),true) = true,
inference(step,[status(thm)],[t90707,t391]) ).
cnf(t32,axiom,
sF18 = ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
introduced(definition) ).
cnf(t90239,plain,
sF18 = ifeq(join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t32,t77]) ).
cnf(t90240,plain,
sF18 = ifeq(join(complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90239,t38]) ).
cnf(t90241,plain,
sF18 = ifeq(join(complement(join(sF1,complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90240,t49]) ).
cnf(t90242,plain,
sF18 = ifeq(join(complement(join(sF1,complement(complement(sF2)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90241,t39]) ).
cnf(t90243,plain,
sF18 = ifeq(join(complement(join(sF1,complement(sF3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90242,t52]) ).
cnf(t90244,plain,
sF18 = ifeq(join(complement(join(sF1,sF4)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90243,t75]) ).
cnf(t90245,plain,
sF18 = ifeq(join(complement(sF5),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90244,t345]) ).
cnf(t90246,plain,
sF18 = ifeq(join(sF6,complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90245,t391]) ).
cnf(t90247,plain,
sF18 = ifeq(join(sF6,complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90246,t77]) ).
cnf(t90248,plain,
sF18 = ifeq(join(sF6,complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90247,t39]) ).
cnf(t90249,plain,
sF18 = ifeq(join(sF6,complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90248,t52]) ).
cnf(t90250,plain,
sF18 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90249,t75]) ).
cnf(t90251,plain,
sF18 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90250,t34]) ).
cnf(t90252,plain,
sF18 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8)))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90251,t35]) ).
cnf(t90253,plain,
sF18 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90252,t40]) ).
cnf(t90254,plain,
sF18 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(sF10)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90253,t407]) ).
cnf(t90255,plain,
sF18 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,sF11))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90254,t427]) ).
cnf(t90256,plain,
sF18 = ifeq(join(sF6,complement(join(sF4,complement(sF12)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90255,t454]) ).
cnf(t90257,plain,
sF18 = ifeq(join(sF6,complement(join(sF4,sF13))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90256,t480]) ).
cnf(t90258,plain,
sF18 = ifeq(join(sF6,complement(sF14)),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90257,t507]) ).
cnf(t90259,plain,
sF18 = ifeq(join(sF6,sF15),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90258,t535]) ).
cnf(t90260,plain,
sF18 = ifeq(sF16,complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90259,t546]) ).
cnf(t90261,plain,
sF18 = ifeq(sF16,complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90260,t38]) ).
cnf(t90262,plain,
sF18 = ifeq(sF16,complement(join(sF1,complement(complement(composition(sk1,sk3))))),false,true),
inference(step,[status(thm)],[t90261,t49]) ).
cnf(t90263,plain,
sF18 = ifeq(sF16,complement(join(sF1,complement(complement(sF2)))),false,true),
inference(step,[status(thm)],[t90262,t39]) ).
cnf(t90264,plain,
sF18 = ifeq(sF16,complement(join(sF1,complement(sF3))),false,true),
inference(step,[status(thm)],[t90263,t52]) ).
cnf(t90265,plain,
sF18 = ifeq(sF16,complement(join(sF1,sF4)),false,true),
inference(step,[status(thm)],[t90264,t75]) ).
cnf(t90266,plain,
sF18 = ifeq(sF16,complement(sF5),false,true),
inference(step,[status(thm)],[t90265,t345]) ).
cnf(t90267,plain,
sF18 = ifeq(sF16,sF6,false,true),
inference(step,[status(thm)],[t90266,t391]) ).
cnf(t575,plain,
ifeq(sF16,sF6,false,true) = sF18,
inference(orient,[status(thm)],[t90267]) ).
cnf(t90709,plain,
ifeq(sF16,sF15,sF18,true) = true,
inference(step,[status(thm)],[t90708,t575]) ).
cnf(t33,axiom,
sF19 = ifeq(join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
introduced(definition) ).
cnf(t90275,plain,
sF19 = ifeq(join(complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t33,t38]) ).
cnf(t90276,plain,
sF19 = ifeq(join(complement(join(sF1,complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90275,t49]) ).
cnf(t90277,plain,
sF19 = ifeq(join(complement(join(sF1,complement(complement(sF2)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90276,t39]) ).
cnf(t90278,plain,
sF19 = ifeq(join(complement(join(sF1,complement(sF3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90277,t52]) ).
cnf(t90279,plain,
sF19 = ifeq(join(complement(join(sF1,sF4)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90278,t75]) ).
cnf(t90280,plain,
sF19 = ifeq(join(complement(sF5),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90279,t345]) ).
cnf(t90281,plain,
sF19 = ifeq(join(sF6,complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90280,t391]) ).
cnf(t90282,plain,
sF19 = ifeq(join(sF6,complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90281,t77]) ).
cnf(t90283,plain,
sF19 = ifeq(join(sF6,complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90282,t39]) ).
cnf(t90284,plain,
sF19 = ifeq(join(sF6,complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90283,t52]) ).
cnf(t90285,plain,
sF19 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90284,t75]) ).
cnf(t90286,plain,
sF19 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3))))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90285,t34]) ).
cnf(t90287,plain,
sF19 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8)))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90286,t35]) ).
cnf(t90288,plain,
sF19 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90287,t40]) ).
cnf(t90289,plain,
sF19 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(sF10)))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90288,t407]) ).
cnf(t90290,plain,
sF19 = ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,sF11))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90289,t427]) ).
cnf(t90291,plain,
sF19 = ifeq(join(sF6,complement(join(sF4,complement(sF12)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90290,t454]) ).
cnf(t90292,plain,
sF19 = ifeq(join(sF6,complement(join(sF4,sF13))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90291,t480]) ).
cnf(t90293,plain,
sF19 = ifeq(join(sF6,complement(sF14)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90292,t507]) ).
cnf(t90294,plain,
sF19 = ifeq(join(sF6,sF15),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90293,t535]) ).
cnf(t90295,plain,
sF19 = ifeq(sF16,complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90294,t546]) ).
cnf(t90296,plain,
sF19 = ifeq(sF16,complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90295,t77]) ).
cnf(t90297,plain,
sF19 = ifeq(sF16,complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90296,t39]) ).
cnf(t90298,plain,
sF19 = ifeq(sF16,complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90297,t52]) ).
cnf(t90299,plain,
sF19 = ifeq(sF16,complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90298,t75]) ).
cnf(t90300,plain,
sF19 = ifeq(sF16,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3)))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90299,t34]) ).
cnf(t90301,plain,
sF19 = ifeq(sF16,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8))))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90300,t35]) ).
cnf(t90302,plain,
sF19 = ifeq(sF16,complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9)))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90301,t40]) ).
cnf(t90303,plain,
sF19 = ifeq(sF16,complement(join(sF4,complement(composition(sk1,complement(sF10))))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90302,t407]) ).
cnf(t90304,plain,
sF19 = ifeq(sF16,complement(join(sF4,complement(composition(sk1,sF11)))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90303,t427]) ).
cnf(t90305,plain,
sF19 = ifeq(sF16,complement(join(sF4,complement(sF12))),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90304,t454]) ).
cnf(t90306,plain,
sF19 = ifeq(sF16,complement(join(sF4,sF13)),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90305,t480]) ).
cnf(t90307,plain,
sF19 = ifeq(sF16,complement(sF14),ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90306,t507]) ).
cnf(t90308,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90307,t535]) ).
cnf(t90309,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90308,t77]) ).
cnf(t90310,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90309,t38]) ).
cnf(t90311,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(complement(join(sF1,complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90310,t49]) ).
cnf(t90312,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(complement(join(sF1,complement(complement(sF2)))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90311,t39]) ).
cnf(t90313,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(complement(join(sF1,complement(sF3))),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90312,t52]) ).
cnf(t90314,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(complement(join(sF1,sF4)),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90313,t75]) ).
cnf(t90315,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(complement(sF5),complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90314,t345]) ).
cnf(t90316,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),complement(complement(composition(sk1,sk3)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90315,t391]) ).
cnf(t90317,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(complement(complement(composition(sk1,sk3))),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90316,t77]) ).
cnf(t90318,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(complement(complement(sF2)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90317,t39]) ).
cnf(t90319,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(complement(sF3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90318,t52]) ).
cnf(t90320,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90319,t75]) ).
cnf(t90321,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(complement(sk3))))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90320,t34]) ).
cnf(t90322,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,complement(sF8)))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90321,t35]) ).
cnf(t90323,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(join(sF7,sF9))))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90322,t40]) ).
cnf(t90324,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,complement(sF10)))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90323,t407]) ).
cnf(t90325,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,complement(composition(sk1,sF11))))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90324,t427]) ).
cnf(t90326,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,complement(sF12)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90325,t454]) ).
cnf(t90327,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(join(sF4,sF13))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90326,t480]) ).
cnf(t90328,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,complement(sF14)),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90327,t507]) ).
cnf(t90329,plain,
sF19 = ifeq(sF16,sF15,ifeq(join(sF6,sF15),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90328,t535]) ).
cnf(t90330,plain,
sF19 = ifeq(sF16,sF15,ifeq(sF16,complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90329,t546]) ).
cnf(t90331,plain,
sF19 = ifeq(sF16,sF15,ifeq(sF16,complement(join(complement(sF0),complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90330,t38]) ).
cnf(t90332,plain,
sF19 = ifeq(sF16,sF15,ifeq(sF16,complement(join(sF1,complement(complement(composition(sk1,sk3))))),false,true),true),
inference(step,[status(thm)],[t90331,t49]) ).
cnf(t90333,plain,
sF19 = ifeq(sF16,sF15,ifeq(sF16,complement(join(sF1,complement(complement(sF2)))),false,true),true),
inference(step,[status(thm)],[t90332,t39]) ).
cnf(t90334,plain,
sF19 = ifeq(sF16,sF15,ifeq(sF16,complement(join(sF1,complement(sF3))),false,true),true),
inference(step,[status(thm)],[t90333,t52]) ).
cnf(t90335,plain,
sF19 = ifeq(sF16,sF15,ifeq(sF16,complement(join(sF1,sF4)),false,true),true),
inference(step,[status(thm)],[t90334,t75]) ).
cnf(t90336,plain,
sF19 = ifeq(sF16,sF15,ifeq(sF16,complement(sF5),false,true),true),
inference(step,[status(thm)],[t90335,t345]) ).
cnf(t90337,plain,
sF19 = ifeq(sF16,sF15,ifeq(sF16,sF6,false,true),true),
inference(step,[status(thm)],[t90336,t391]) ).
cnf(t90338,plain,
sF19 = ifeq(sF16,sF15,sF18,true),
inference(step,[status(thm)],[t90337,t575]) ).
cnf(t599,plain,
ifeq(sF16,sF15,sF18,true) = sF19,
inference(orient,[status(thm)],[t90338]) ).
cnf(t90710,plain,
sF19 = true,
inference(step,[status(thm)],[t90709,t599]) ).
cnf(t6898,plain,
true = sF19,
inference(orient,[status(thm)],[t90710]) ).
cnf(t90712,plain,
ifeq(sF16,sF15,sF18,sF19) = sF19,
inference(step,[status(thm)],[t599,t6898]) ).
cnf(t6900,plain,
ifeq(sF16,sF15,sF18,sF19) = sF19,
inference(rw,[status(thm)],[t90712]) ).
cnf(t6934,plain,
ifeq(sF16,sF15,sF18,sF19) = sF19,
inference(orient,[status(thm)],[t6900]) ).
cnf(t237,plain,
X1 = join(complement(join(complement(X1),sF0)),complement(join(complement(X1),sF1))),
inference(cp,[status(thm)],[t227,t49]) ).
cnf(t90612,plain,
X1 = join(complement(join(sF0,complement(X1))),complement(join(complement(X1),sF1))),
inference(step,[status(thm)],[t237,t77]) ).
cnf(t90613,plain,
X1 = join(complement(join(sF0,complement(X1))),complement(join(sF1,complement(X1)))),
inference(step,[status(thm)],[t90612,t77]) ).
cnf(t5083,plain,
join(complement(join(sF0,complement(X1))),complement(join(sF1,complement(X1)))) = X1,
inference(orient,[status(thm)],[t90613]) ).
cnf(t1591,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t323,t1585]) ).
cnf(t90432,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1591,t1585]) ).
cnf(t90433,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t90432,t1585]) ).
cnf(t1700,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t90433]) ).
cnf(t86,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t66,t77]) ).
cnf(t90376,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t86,t66]) ).
cnf(t981,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t90376]) ).
cnf(t1718,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t1700,t981]) ).
cnf(t90516,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t1718,t66]) ).
cnf(t90517,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t90516,t1700]) ).
cnf(t3096,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t90517]) ).
cnf(t236,plain,
sF0 = join(complement(join(sF1,X1)),complement(join(complement(sF0),complement(X1)))),
inference(cp,[status(thm)],[t227,t49]) ).
cnf(t90611,plain,
sF0 = join(complement(join(sF1,X1)),complement(join(sF1,complement(X1)))),
inference(step,[status(thm)],[t236,t49]) ).
cnf(t4945,plain,
join(complement(join(sF1,X1)),complement(join(sF1,complement(X1)))) = sF0,
inference(orient,[status(thm)],[t90611]) ).
cnf(t4949,plain,
sF0 = join(complement(join(sF1,sF2)),complement(join(sF1,sF3))),
inference(cp,[status(thm)],[t4945,t52]) ).
cnf(t90413,plain,
join(sF1,sF2) = sF5,
inference(step,[status(thm)],[t345,t1607]) ).
cnf(t1612,plain,
join(sF1,sF2) = sF5,
inference(rw,[status(thm)],[t90413]) ).
cnf(t1754,plain,
join(sF1,sF2) = sF5,
inference(orient,[status(thm)],[t1612]) ).
cnf(t90785,plain,
sF0 = join(complement(sF5),complement(join(sF1,sF3))),
inference(step,[status(thm)],[t4949,t1754]) ).
cnf(t90786,plain,
sF0 = join(sF6,complement(join(sF1,sF3))),
inference(step,[status(thm)],[t90785,t391]) ).
cnf(t8810,plain,
join(sF6,complement(join(sF1,sF3))) = sF0,
inference(orient,[status(thm)],[t90786]) ).
cnf(t8820,plain,
join(sF6,complement(join(sF1,sF3))) = join(sF6,sF0),
inference(cp,[status(thm)],[t3096,t8810]) ).
cnf(t90787,plain,
sF0 = join(sF6,sF0),
inference(step,[status(thm)],[t8820,t8810]) ).
cnf(t90788,plain,
sF0 = join(sF0,sF6),
inference(step,[status(thm)],[t90787,t77]) ).
cnf(t8830,plain,
join(sF0,sF6) = sF0,
inference(orient,[status(thm)],[t90788]) ).
cnf(t8832,plain,
join(sF0,join(sF6,X1)) = join(sF0,X1),
inference(cp,[status(thm)],[t66,t8830]) ).
cnf(t8840,plain,
join(sF0,join(sF6,X1)) = join(sF0,X1),
inference(orient,[status(thm)],[t8832]) ).
cnf(t1034,plain,
join(sF6,join(X1,sF15)) = join(X1,sF16),
inference(cp,[status(thm)],[t981,t546]) ).
cnf(t2690,plain,
join(sF6,join(X1,sF15)) = join(X1,sF16),
inference(orient,[status(thm)],[t1034]) ).
cnf(t239,plain,
X1 = join(complement(join(complement(X1),sF2)),complement(join(complement(X1),sF3))),
inference(cp,[status(thm)],[t227,t52]) ).
cnf(t90629,plain,
X1 = join(complement(join(sF2,complement(X1))),complement(join(complement(X1),sF3))),
inference(step,[status(thm)],[t239,t77]) ).
cnf(t90630,plain,
X1 = join(complement(join(sF2,complement(X1))),complement(join(sF3,complement(X1)))),
inference(step,[status(thm)],[t90629,t77]) ).
cnf(t5329,plain,
join(complement(join(sF2,complement(X1))),complement(join(sF3,complement(X1)))) = X1,
inference(orient,[status(thm)],[t90630]) ).
cnf(t5339,plain,
sF12 = join(complement(join(sF2,sF13)),complement(join(sF3,complement(sF12)))),
inference(cp,[status(thm)],[t5329,t480]) ).
cnf(t90812,plain,
sF12 = join(complement(sF14),complement(join(sF3,complement(sF12)))),
inference(step,[status(thm)],[t5339,t1786]) ).
cnf(t90813,plain,
sF12 = join(sF15,complement(join(sF3,complement(sF12)))),
inference(step,[status(thm)],[t90812,t535]) ).
cnf(t90814,plain,
sF12 = join(sF15,complement(join(sF3,sF13))),
inference(step,[status(thm)],[t90813,t480]) ).
cnf(t9436,plain,
join(sF15,complement(join(sF3,sF13))) = sF12,
inference(orient,[status(thm)],[t90814]) ).
cnf(t9448,plain,
join(sF15,complement(join(sF3,sF13))) = join(sF15,sF12),
inference(cp,[status(thm)],[t3096,t9436]) ).
cnf(t90815,plain,
sF12 = join(sF15,sF12),
inference(step,[status(thm)],[t9448,t9436]) ).
cnf(t90816,plain,
sF12 = join(sF12,sF15),
inference(step,[status(thm)],[t90815,t77]) ).
cnf(t9461,plain,
join(sF12,sF15) = sF12,
inference(orient,[status(thm)],[t90816]) ).
cnf(t9470,plain,
join(sF12,sF16) = join(sF6,sF12),
inference(cp,[status(thm)],[t2690,t9461]) ).
cnf(t9490,plain,
join(sF12,sF16) = join(sF6,sF12),
inference(orient,[status(thm)],[t9470]) ).
cnf(t9492,plain,
join(sF12,join(sF16,X1)) = join(join(sF6,sF12),X1),
inference(cp,[status(thm)],[t66,t9490]) ).
cnf(t90818,plain,
join(sF12,join(sF16,X1)) = join(sF6,join(sF12,X1)),
inference(step,[status(thm)],[t9492,t66]) ).
cnf(t9574,plain,
join(sF12,join(sF16,X1)) = join(sF6,join(sF12,X1)),
inference(orient,[status(thm)],[t90818]) ).
cnf(t9575,plain,
join(sF6,join(sF12,complement(sF16))) = join(sF12,top),
inference(cp,[status(thm)],[t9574,t41]) ).
cnf(t67,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t66,t41]) ).
cnf(t645,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t67]) ).
cnf(t660,plain,
top = join(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(cp,[status(thm)],[t645,t323]) ).
cnf(t90349,plain,
top = join(complement(X1),top),
inference(step,[status(thm)],[t660,t41]) ).
cnf(t90350,plain,
top = join(top,complement(X1)),
inference(step,[status(thm)],[t90349,t77]) ).
cnf(t757,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t90350]) ).
cnf(t774,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t645,t757]) ).
cnf(t870,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t774]) ).
cnf(t90984,plain,
join(sF6,join(sF12,complement(sF16))) = top,
inference(step,[status(thm)],[t9575,t870]) ).
cnf(t24476,plain,
join(sF6,join(sF12,complement(sF16))) = top,
inference(orient,[status(thm)],[t90984]) ).
cnf(t24489,plain,
join(sF0,join(sF12,complement(sF16))) = join(sF0,top),
inference(cp,[status(thm)],[t8840,t24476]) ).
cnf(t91124,plain,
join(sF0,join(sF12,complement(sF16))) = top,
inference(step,[status(thm)],[t24489,t870]) ).
cnf(t39923,plain,
join(sF0,join(sF12,complement(sF16))) = top,
inference(orient,[status(thm)],[t91124]) ).
cnf(f8,axiom,
converse(join(A,B)) = join(converse(A),converse(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f8_nnf,plain,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t7,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t58,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t59,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t58,t37]) ).
cnf(t148,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t59]) ).
cnf(t155,plain,
composition(converse(X1),join(converse(X2),X3)) = converse(composition(join(X2,converse(X3)),X1)),
inference(cp,[status(thm)],[t106,t148]) ).
cnf(t2864,plain,
converse(composition(join(X1,converse(X2)),X3)) = composition(converse(X3),join(converse(X1),X2)),
inference(orient,[status(thm)],[t155]) ).
cnf(f6,axiom,
composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f6_nnf,plain,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t10,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t135,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t140,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t135,t55]) ).
cnf(t2052,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t140]) ).
cnf(t2053,plain,
composition(join(converse(sk2),X1),converse(sk1)) = join(converse(sF0),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t2052,t38]) ).
cnf(t56833,plain,
composition(join(converse(sk2),X1),converse(sk1)) = join(converse(sF0),composition(X1,converse(sk1))),
inference(orient,[status(thm)],[t2053]) ).
cnf(t56897,plain,
composition(converse(converse(sk1)),join(converse(converse(sk2)),X1)) = converse(join(converse(sF0),composition(converse(X1),converse(sk1)))),
inference(cp,[status(thm)],[t2864,t56833]) ).
cnf(t91258,plain,
composition(sk1,join(converse(converse(sk2)),X1)) = converse(join(converse(sF0),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t56897,t37]) ).
cnf(t91259,plain,
composition(sk1,join(sk2,X1)) = converse(join(converse(sF0),composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t91258,t37]) ).
cnf(t91260,plain,
composition(sk1,join(sk2,X1)) = join(sF0,converse(composition(converse(X1),converse(sk1)))),
inference(step,[status(thm)],[t91259,t148]) ).
cnf(t56,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t55,t37]) ).
cnf(t101,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t56]) ).
cnf(t91261,plain,
composition(sk1,join(sk2,X1)) = join(sF0,composition(sk1,converse(converse(X1)))),
inference(step,[status(thm)],[t91260,t101]) ).
cnf(t91262,plain,
composition(sk1,join(sk2,X1)) = join(sF0,composition(sk1,X1)),
inference(step,[status(thm)],[t91261,t37]) ).
cnf(t57010,plain,
composition(sk1,join(sk2,X1)) = join(sF0,composition(sk1,X1)),
inference(orient,[status(thm)],[t91262]) ).
cnf(t57013,plain,
join(sF0,composition(sk1,X1)) = composition(sk1,join(X1,sk2)),
inference(cp,[status(thm)],[t57010,t77]) ).
cnf(t57145,plain,
composition(sk1,join(X1,sk2)) = join(sF0,composition(sk1,X1)),
inference(orient,[status(thm)],[t57013]) ).
cnf(t431,plain,
X1 = join(complement(join(complement(X1),sF10)),complement(join(complement(X1),sF11))),
inference(cp,[status(thm)],[t227,t427]) ).
cnf(t90726,plain,
X1 = join(complement(join(sF10,complement(X1))),complement(join(complement(X1),sF11))),
inference(step,[status(thm)],[t431,t77]) ).
cnf(t90727,plain,
X1 = join(complement(join(sF10,complement(X1))),complement(join(sF11,complement(X1)))),
inference(step,[status(thm)],[t90726,t77]) ).
cnf(t7210,plain,
join(complement(join(sF10,complement(X1))),complement(join(sF11,complement(X1)))) = X1,
inference(orient,[status(thm)],[t90727]) ).
cnf(t577,plain,
sk2 = join(zero,complement(sF7)),
inference(cp,[status(thm)],[t576,t34]) ).
cnf(t600,plain,
join(zero,complement(sF7)) = sk2,
inference(orient,[status(thm)],[t577]) ).
cnf(t90393,plain,
complement(sF7) = sk2,
inference(step,[status(thm)],[t600,t1461]) ).
cnf(t1465,plain,
complement(sF7) = sk2,
inference(rw,[status(thm)],[t90393]) ).
cnf(t1484,plain,
complement(sF7) = sk2,
inference(orient,[status(thm)],[t1465]) ).
cnf(t7220,plain,
sF7 = join(complement(join(sF10,sk2)),complement(join(sF11,complement(sF7)))),
inference(cp,[status(thm)],[t7210,t1484]) ).
cnf(t409,plain,
join(sF7,join(sF9,X1)) = join(sF10,X1),
inference(cp,[status(thm)],[t66,t407]) ).
cnf(t1951,plain,
join(sF7,join(sF9,X1)) = join(sF10,X1),
inference(orient,[status(thm)],[t409]) ).
cnf(t42,plain,
top = join(sk2,sF7),
inference(cp,[status(thm)],[t41,t34]) ).
cnf(t45,plain,
join(sk2,sF7) = top,
inference(orient,[status(thm)],[t42]) ).
cnf(t90008,plain,
join(sF7,sk2) = top,
inference(step,[status(thm)],[t45,t77]) ).
cnf(t78,plain,
join(sF7,sk2) = top,
inference(rw,[status(thm)],[t90008]) ).
cnf(t90,plain,
join(sF7,sk2) = top,
inference(orient,[status(thm)],[t78]) ).
cnf(t92,plain,
join(sF7,join(sk2,X1)) = join(top,X1),
inference(cp,[status(thm)],[t66,t90]) ).
cnf(t223,plain,
join(sF7,join(sk2,X1)) = join(top,X1),
inference(orient,[status(thm)],[t92]) ).
cnf(t226,plain,
join(top,X1) = join(sF7,join(X1,sk2)),
inference(cp,[status(thm)],[t223,t77]) ).
cnf(t491,plain,
join(sF7,join(X1,sk2)) = join(top,X1),
inference(orient,[status(thm)],[t226]) ).
cnf(t1955,plain,
join(sF10,sk2) = join(top,sF9),
inference(cp,[status(thm)],[t1951,t491]) ).
cnf(t44,plain,
top = join(sF8,sF9),
inference(cp,[status(thm)],[t41,t40]) ).
cnf(t48,plain,
join(sF8,sF9) = top,
inference(orient,[status(thm)],[t44]) ).
cnf(t71,plain,
join(sF8,join(sF9,X1)) = join(top,X1),
inference(cp,[status(thm)],[t66,t48]) ).
cnf(t168,plain,
join(sF8,join(sF9,X1)) = join(top,X1),
inference(orient,[status(thm)],[t71]) ).
cnf(t171,plain,
join(top,X1) = join(sF8,join(X1,sF9)),
inference(cp,[status(thm)],[t168,t77]) ).
cnf(t306,plain,
join(sF8,join(X1,sF9)) = join(top,X1),
inference(orient,[status(thm)],[t171]) ).
cnf(t308,plain,
join(top,X1) = join(join(X1,sF9),sF8),
inference(cp,[status(thm)],[t306,t77]) ).
cnf(t90232,plain,
join(top,X1) = join(X1,join(sF9,sF8)),
inference(step,[status(thm)],[t308,t66]) ).
cnf(t90233,plain,
join(top,X1) = join(X1,join(sF8,sF9)),
inference(step,[status(thm)],[t90232,t77]) ).
cnf(t90234,plain,
join(top,X1) = join(X1,top),
inference(step,[status(thm)],[t90233,t48]) ).
cnf(t558,plain,
join(top,X1) = join(X1,top),
inference(orient,[status(thm)],[t90234]) ).
cnf(t90370,plain,
join(top,X1) = top,
inference(step,[status(thm)],[t558,t870]) ).
cnf(t885,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t90370]) ).
cnf(t90465,plain,
join(sF10,sk2) = top,
inference(step,[status(thm)],[t1955,t885]) ).
cnf(t1973,plain,
join(sF10,sk2) = top,
inference(orient,[status(thm)],[t90465]) ).
cnf(t90728,plain,
sF7 = join(complement(top),complement(join(sF11,complement(sF7)))),
inference(step,[status(thm)],[t7220,t1973]) ).
cnf(t90729,plain,
sF7 = join(zero,complement(join(sF11,complement(sF7)))),
inference(step,[status(thm)],[t90728,t96]) ).
cnf(t90730,plain,
sF7 = complement(join(sF11,complement(sF7))),
inference(step,[status(thm)],[t90729,t1461]) ).
cnf(t90731,plain,
sF7 = complement(join(sF11,sk2)),
inference(step,[status(thm)],[t90730,t1484]) ).
cnf(t7247,plain,
complement(join(sF11,sk2)) = sF7,
inference(orient,[status(thm)],[t90731]) ).
cnf(t7251,plain,
join(sF11,sk2) = join(complement(join(sF7,X1)),complement(join(complement(join(sF11,sk2)),complement(X1)))),
inference(cp,[status(thm)],[t227,t7247]) ).
cnf(t90732,plain,
join(sF11,sk2) = join(complement(join(sF7,X1)),complement(join(sF7,complement(X1)))),
inference(step,[status(thm)],[t7251,t7247]) ).
cnf(t228,plain,
sk2 = join(complement(join(sF7,X1)),complement(join(complement(sk2),complement(X1)))),
inference(cp,[status(thm)],[t227,t34]) ).
cnf(t90592,plain,
sk2 = join(complement(join(sF7,X1)),complement(join(sF7,complement(X1)))),
inference(step,[status(thm)],[t228,t34]) ).
cnf(t4672,plain,
join(complement(join(sF7,X1)),complement(join(sF7,complement(X1)))) = sk2,
inference(orient,[status(thm)],[t90592]) ).
cnf(t90733,plain,
join(sF11,sk2) = sk2,
inference(step,[status(thm)],[t90732,t4672]) ).
cnf(t7286,plain,
join(sF11,sk2) = sk2,
inference(orient,[status(thm)],[t90733]) ).
cnf(t57146,plain,
join(sF0,composition(sk1,sF11)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t57145,t7286]) ).
cnf(t91264,plain,
join(sF0,sF12) = composition(sk1,sk2),
inference(step,[status(thm)],[t57146,t454]) ).
cnf(t91265,plain,
join(sF0,sF12) = sF0,
inference(step,[status(thm)],[t91264,t38]) ).
cnf(t57178,plain,
join(sF0,sF12) = sF0,
inference(orient,[status(thm)],[t91265]) ).
cnf(t57180,plain,
join(sF0,join(sF12,X1)) = join(sF0,X1),
inference(cp,[status(thm)],[t66,t57178]) ).
cnf(t57445,plain,
join(sF0,join(sF12,X1)) = join(sF0,X1),
inference(orient,[status(thm)],[t57180]) ).
cnf(t91272,plain,
join(sF0,complement(sF16)) = top,
inference(step,[status(thm)],[t39923,t57445]) ).
cnf(t57446,plain,
join(sF0,complement(sF16)) = top,
inference(rw,[status(thm)],[t91272]) ).
cnf(t58200,plain,
join(sF0,complement(sF16)) = top,
inference(orient,[status(thm)],[t57446]) ).
cnf(t58208,plain,
sF16 = join(complement(top),complement(join(sF1,complement(sF16)))),
inference(cp,[status(thm)],[t5083,t58200]) ).
cnf(t91289,plain,
sF16 = join(zero,complement(join(sF1,complement(sF16)))),
inference(step,[status(thm)],[t58208,t96]) ).
cnf(t91290,plain,
sF16 = complement(join(sF1,complement(sF16))),
inference(step,[status(thm)],[t91289,t1461]) ).
cnf(t68,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t66,t41]) ).
cnf(t733,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t68]) ).
cnf(t750,plain,
X1 = join(complement(join(top,X2)),complement(join(complement(X1),complement(join(complement(complement(X1)),X2))))),
inference(cp,[status(thm)],[t227,t733]) ).
cnf(t90829,plain,
X1 = join(complement(top),complement(join(complement(X1),complement(join(complement(complement(X1)),X2))))),
inference(step,[status(thm)],[t750,t885]) ).
cnf(t90830,plain,
X1 = join(zero,complement(join(complement(X1),complement(join(complement(complement(X1)),X2))))),
inference(step,[status(thm)],[t90829,t96]) ).
cnf(t90831,plain,
X1 = complement(join(complement(X1),complement(join(complement(complement(X1)),X2)))),
inference(step,[status(thm)],[t90830,t1461]) ).
cnf(t90832,plain,
X1 = complement(join(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t90831,t1585]) ).
cnf(t9758,plain,
complement(join(complement(X1),complement(join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t90832]) ).
cnf(t9778,plain,
sF6 = complement(join(complement(sF6),complement(sF16))),
inference(cp,[status(thm)],[t9758,t546]) ).
cnf(t584,plain,
sF5 = join(zero,complement(sF6)),
inference(cp,[status(thm)],[t576,t391]) ).
cnf(t612,plain,
join(zero,complement(sF6)) = sF5,
inference(orient,[status(thm)],[t584]) ).
cnf(t90397,plain,
complement(sF6) = sF5,
inference(step,[status(thm)],[t612,t1461]) ).
cnf(t1469,plain,
complement(sF6) = sF5,
inference(rw,[status(thm)],[t90397]) ).
cnf(t1509,plain,
complement(sF6) = sF5,
inference(orient,[status(thm)],[t1469]) ).
cnf(t90833,plain,
sF6 = complement(join(sF5,complement(sF16))),
inference(step,[status(thm)],[t9778,t1509]) ).
cnf(t348,plain,
join(sF1,join(sF4,X1)) = join(sF5,X1),
inference(cp,[status(thm)],[t66,t345]) ).
cnf(t1274,plain,
join(sF1,join(sF4,X1)) = join(sF5,X1),
inference(orient,[status(thm)],[t348]) ).
cnf(t90416,plain,
join(sF1,join(sF2,X1)) = join(sF5,X1),
inference(step,[status(thm)],[t1274,t1607]) ).
cnf(t1618,plain,
join(sF1,join(sF2,X1)) = join(sF5,X1),
inference(rw,[status(thm)],[t90416]) ).
cnf(t3067,plain,
join(sF1,join(sF2,X1)) = join(sF5,X1),
inference(orient,[status(thm)],[t1618]) ).
cnf(t238,plain,
sF2 = join(complement(join(sF3,X1)),complement(join(complement(sF2),complement(X1)))),
inference(cp,[status(thm)],[t227,t52]) ).
cnf(t90620,plain,
sF2 = join(complement(join(sF3,X1)),complement(join(sF3,complement(X1)))),
inference(step,[status(thm)],[t238,t52]) ).
cnf(t5210,plain,
join(complement(join(sF3,X1)),complement(join(sF3,complement(X1)))) = sF2,
inference(orient,[status(thm)],[t90620]) ).
cnf(t5222,plain,
sF2 = join(complement(join(sF3,sF14)),complement(join(sF3,sF15))),
inference(cp,[status(thm)],[t5210,t535]) ).
cnf(t485,plain,
complement(sF12) = join(sF13,complement(sF12)),
inference(cp,[status(thm)],[t323,t480]) ).
cnf(t90158,plain,
sF13 = join(sF13,complement(sF12)),
inference(step,[status(thm)],[t485,t480]) ).
cnf(t90159,plain,
sF13 = join(sF13,sF13),
inference(step,[status(thm)],[t90158,t480]) ).
cnf(t489,plain,
join(sF13,sF13) = sF13,
inference(orient,[status(thm)],[t90159]) ).
cnf(t677,plain,
top = join(sF13,join(sF13,complement(sF13))),
inference(cp,[status(thm)],[t645,t489]) ).
cnf(t90342,plain,
top = join(sF13,top),
inference(step,[status(thm)],[t677,t41]) ).
cnf(t76,plain,
top = join(sF3,sF4),
inference(cp,[status(thm)],[t41,t75]) ).
cnf(t87,plain,
join(sF3,sF4) = top,
inference(orient,[status(thm)],[t76]) ).
cnf(t89,plain,
join(sF3,join(sF4,X1)) = join(top,X1),
inference(cp,[status(thm)],[t66,t87]) ).
cnf(t214,plain,
join(sF3,join(sF4,X1)) = join(top,X1),
inference(orient,[status(thm)],[t89]) ).
cnf(t510,plain,
join(top,sF13) = join(sF3,sF14),
inference(cp,[status(thm)],[t214,t507]) ).
cnf(t90172,plain,
join(sF13,top) = join(sF3,sF14),
inference(step,[status(thm)],[t510,t77]) ).
cnf(t512,plain,
join(sF13,top) = join(sF3,sF14),
inference(orient,[status(thm)],[t90172]) ).
cnf(t90343,plain,
top = join(sF3,sF14),
inference(step,[status(thm)],[t90342,t512]) ).
cnf(t723,plain,
join(sF3,sF14) = top,
inference(orient,[status(thm)],[t90343]) ).
cnf(t90625,plain,
sF2 = join(complement(top),complement(join(sF3,sF15))),
inference(step,[status(thm)],[t5222,t723]) ).
cnf(t90626,plain,
sF2 = join(zero,complement(join(sF3,sF15))),
inference(step,[status(thm)],[t90625,t96]) ).
cnf(t90627,plain,
sF2 = complement(join(sF3,sF15)),
inference(step,[status(thm)],[t90626,t1461]) ).
cnf(t5293,plain,
complement(join(sF3,sF15)) = sF2,
inference(orient,[status(thm)],[t90627]) ).
cnf(t5300,plain,
join(sF3,sF15) = complement(sF2),
inference(cp,[status(thm)],[t1585,t5293]) ).
cnf(t90628,plain,
join(sF3,sF15) = sF3,
inference(step,[status(thm)],[t5300,t52]) ).
cnf(t5317,plain,
join(sF3,sF15) = sF3,
inference(orient,[status(thm)],[t90628]) ).
cnf(t5328,plain,
join(sF3,sF16) = join(sF6,sF3),
inference(cp,[status(thm)],[t2690,t5317]) ).
cnf(t90631,plain,
join(sF3,sF16) = join(sF3,sF6),
inference(step,[status(thm)],[t5328,t77]) ).
cnf(t5219,plain,
sF2 = join(complement(join(sF3,sF5)),complement(join(sF3,sF6))),
inference(cp,[status(thm)],[t5210,t391]) ).
cnf(t217,plain,
join(top,X1) = join(sF3,join(X1,sF4)),
inference(cp,[status(thm)],[t214,t77]) ).
cnf(t447,plain,
join(sF3,join(X1,sF4)) = join(top,X1),
inference(orient,[status(thm)],[t217]) ).
cnf(t451,plain,
join(top,sF1) = join(sF3,sF5),
inference(cp,[status(thm)],[t447,t345]) ).
cnf(t90142,plain,
join(sF1,top) = join(sF3,sF5),
inference(step,[status(thm)],[t451,t77]) ).
cnf(t50,plain,
top = join(sF0,sF1),
inference(cp,[status(thm)],[t41,t49]) ).
cnf(t51,plain,
join(sF0,sF1) = top,
inference(orient,[status(thm)],[t50]) ).
cnf(t72,plain,
join(sF0,join(sF1,X1)) = join(top,X1),
inference(cp,[status(thm)],[t66,t51]) ).
cnf(t175,plain,
join(sF0,join(sF1,X1)) = join(top,X1),
inference(orient,[status(thm)],[t72]) ).
cnf(t327,plain,
complement(sF0) = join(sF1,complement(sF0)),
inference(cp,[status(thm)],[t323,t49]) ).
cnf(t90070,plain,
sF1 = join(sF1,complement(sF0)),
inference(step,[status(thm)],[t327,t49]) ).
cnf(t90071,plain,
sF1 = join(sF1,sF1),
inference(step,[status(thm)],[t90070,t49]) ).
cnf(t342,plain,
join(sF1,sF1) = sF1,
inference(orient,[status(thm)],[t90071]) ).
cnf(t344,plain,
join(top,sF1) = join(sF0,sF1),
inference(cp,[status(thm)],[t175,t342]) ).
cnf(t90095,plain,
join(sF1,top) = join(sF0,sF1),
inference(step,[status(thm)],[t344,t77]) ).
cnf(t90096,plain,
join(sF1,top) = top,
inference(step,[status(thm)],[t90095,t51]) ).
cnf(t369,plain,
join(sF1,top) = top,
inference(orient,[status(thm)],[t90096]) ).
cnf(t90143,plain,
top = join(sF3,sF5),
inference(step,[status(thm)],[t90142,t369]) ).
cnf(t459,plain,
join(sF3,sF5) = top,
inference(orient,[status(thm)],[t90143]) ).
cnf(t90621,plain,
sF2 = join(complement(top),complement(join(sF3,sF6))),
inference(step,[status(thm)],[t5219,t459]) ).
cnf(t90622,plain,
sF2 = join(zero,complement(join(sF3,sF6))),
inference(step,[status(thm)],[t90621,t96]) ).
cnf(t90623,plain,
sF2 = complement(join(sF3,sF6)),
inference(step,[status(thm)],[t90622,t1461]) ).
cnf(t5258,plain,
complement(join(sF3,sF6)) = sF2,
inference(orient,[status(thm)],[t90623]) ).
cnf(t5265,plain,
join(sF3,sF6) = complement(sF2),
inference(cp,[status(thm)],[t1585,t5258]) ).
cnf(t90624,plain,
join(sF3,sF6) = sF3,
inference(step,[status(thm)],[t5265,t52]) ).
cnf(t5282,plain,
join(sF3,sF6) = sF3,
inference(orient,[status(thm)],[t90624]) ).
cnf(t90632,plain,
join(sF3,sF16) = sF3,
inference(step,[status(thm)],[t90631,t5282]) ).
cnf(t5359,plain,
join(sF3,sF16) = sF3,
inference(orient,[status(thm)],[t90632]) ).
cnf(t5361,plain,
join(sF3,join(sF16,X1)) = join(sF3,X1),
inference(cp,[status(thm)],[t66,t5359]) ).
cnf(t6318,plain,
join(sF3,join(sF16,X1)) = join(sF3,X1),
inference(orient,[status(thm)],[t5361]) ).
cnf(t6319,plain,
join(sF3,complement(sF16)) = join(sF3,top),
inference(cp,[status(thm)],[t6318,t41]) ).
cnf(t90659,plain,
join(sF3,complement(sF16)) = top,
inference(step,[status(thm)],[t6319,t870]) ).
cnf(t6336,plain,
join(sF3,complement(sF16)) = top,
inference(orient,[status(thm)],[t90659]) ).
cnf(t6344,plain,
sF16 = join(complement(join(sF2,complement(sF16))),complement(top)),
inference(cp,[status(thm)],[t5329,t6336]) ).
cnf(t90672,plain,
sF16 = join(complement(top),complement(join(sF2,complement(sF16)))),
inference(step,[status(thm)],[t6344,t77]) ).
cnf(t90673,plain,
sF16 = join(zero,complement(join(sF2,complement(sF16)))),
inference(step,[status(thm)],[t90672,t96]) ).
cnf(t90674,plain,
sF16 = complement(join(sF2,complement(sF16))),
inference(step,[status(thm)],[t90673,t1461]) ).
cnf(t6728,plain,
complement(join(sF2,complement(sF16))) = sF16,
inference(orient,[status(thm)],[t90674]) ).
cnf(t6734,plain,
join(sF2,complement(sF16)) = complement(sF16),
inference(cp,[status(thm)],[t1585,t6728]) ).
cnf(t6763,plain,
join(sF2,complement(sF16)) = complement(sF16),
inference(orient,[status(thm)],[t6734]) ).
cnf(t6772,plain,
join(sF5,complement(sF16)) = join(sF1,complement(sF16)),
inference(cp,[status(thm)],[t3067,t6763]) ).
cnf(t6777,plain,
join(sF5,complement(sF16)) = join(sF1,complement(sF16)),
inference(orient,[status(thm)],[t6772]) ).
cnf(t90834,plain,
sF6 = complement(join(sF1,complement(sF16))),
inference(step,[status(thm)],[t90833,t6777]) ).
cnf(t9895,plain,
complement(join(sF1,complement(sF16))) = sF6,
inference(orient,[status(thm)],[t90834]) ).
cnf(t9899,plain,
join(sF1,complement(sF16)) = join(complement(join(sF6,X1)),complement(join(complement(join(sF1,complement(sF16))),complement(X1)))),
inference(cp,[status(thm)],[t227,t9895]) ).
cnf(t90835,plain,
join(sF1,complement(sF16)) = join(complement(join(sF6,X1)),complement(join(sF6,complement(X1)))),
inference(step,[status(thm)],[t9899,t9895]) ).
cnf(t394,plain,
sF5 = join(complement(join(sF6,X1)),complement(join(complement(sF5),complement(X1)))),
inference(cp,[status(thm)],[t227,t391]) ).
cnf(t90714,plain,
sF5 = join(complement(join(sF6,X1)),complement(join(sF6,complement(X1)))),
inference(step,[status(thm)],[t394,t391]) ).
cnf(t6935,plain,
join(complement(join(sF6,X1)),complement(join(sF6,complement(X1)))) = sF5,
inference(orient,[status(thm)],[t90714]) ).
cnf(t90836,plain,
join(sF1,complement(sF16)) = sF5,
inference(step,[status(thm)],[t90835,t6935]) ).
cnf(t9943,plain,
join(sF1,complement(sF16)) = sF5,
inference(orient,[status(thm)],[t90836]) ).
cnf(t91291,plain,
sF16 = complement(sF5),
inference(step,[status(thm)],[t91290,t9943]) ).
cnf(t91292,plain,
sF16 = sF6,
inference(step,[status(thm)],[t91291,t391]) ).
cnf(t58245,plain,
sF16 = sF6,
inference(orient,[status(thm)],[t91292]) ).
cnf(t91308,plain,
ifeq(sF6,sF15,sF18,sF19) = sF19,
inference(step,[status(thm)],[t6934,t58245]) ).
cnf(t58285,plain,
ifeq(sF6,sF15,sF18,sF19) = sF19,
inference(rw,[status(thm)],[t91308]) ).
cnf(t62730,plain,
ifeq(sF6,sF15,sF18,sF19) = sF19,
inference(orient,[status(thm)],[t58285]) ).
cnf(t87448,plain,
ifeq(sF6,sF6,sF18,sF19) = sF19,
inference(rw,[status(thm)],[t62730]) ).
cnf(t3,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t47,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t91689,plain,
sF18 = sF19,
inference(step,[status(thm)],[t87448,t47]) ).
cnf(t90000,plain,
sF19 = sF18,
inference(orient,[status(thm)],[t91689]) ).
cnf(t91690,plain,
true = sF18,
inference(step,[status(thm)],[t6898,t90000]) ).
cnf(t90001,plain,
true = sF18,
inference(orient,[status(thm)],[t91690]) ).
cnf(t90711,plain,
ifeq(sF16,sF6,false,sF19) = sF18,
inference(step,[status(thm)],[t575,t6898]) ).
cnf(t6899,plain,
ifeq(sF16,sF6,false,sF19) = sF18,
inference(rw,[status(thm)],[t90711]) ).
cnf(t6933,plain,
ifeq(sF16,sF6,false,sF19) = sF18,
inference(orient,[status(thm)],[t6899]) ).
cnf(t58284,plain,
ifeq(sF6,sF6,false,sF19) = sF18,
inference(rw,[status(thm)],[t6933]) ).
cnf(t91372,plain,
false = sF18,
inference(step,[status(thm)],[t58284,t47]) ).
cnf(t62729,plain,
false = sF18,
inference(orient,[status(thm)],[t91372]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(g0_0,plain,
sF18 != false,
inference(rw,[status(thm)],[goal_0,t90001]) ).
cnf(g0_1,plain,
sF18 != sF18,
inference(rw,[status(thm)],[g0_0,t62729]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL016-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 07:15:18 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 137.16/20.58 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 137.16/20.58 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------