%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL017-4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.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:46 PM UTC 2026
% Result : Unsatisfiable 197.03s 29.04s
% Output : Proof 197.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 102
% Number of leaves : 30
% Syntax : Number of formulae : 424 ( 420 unt; 0 def)
% Number of atoms : 428 ( 427 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 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 26 con; 0-4 aty)
% Number of variables : 171 ( 2 sgn 34 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t34,axiom,
sF17 = ifeq(join(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),composition(sk1,sk3)),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
introduced(definition) ).
cnf(f1,axiom,
join(A,join(B,C)) = join(join(A,B),C),
file('/export/starexec/sandbox/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(t64,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t72037,plain,
sF17 = ifeq(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t34,t64]) ).
cnf(t72038,plain,
sF17 = ifeq(join(complement(composition(sk1,sk2)),join(composition(sk1,sk3),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72037,t64]) ).
cnf(t17,axiom,
sF0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t39,plain,
composition(sk1,sk2) = sF0,
inference(orient,[status(thm)],[t17]) ).
cnf(t72039,plain,
sF17 = ifeq(join(complement(sF0),join(composition(sk1,sk3),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72038,t39]) ).
cnf(t18,axiom,
sF1 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t71809,plain,
sF1 = complement(sF0),
inference(step,[status(thm)],[t18,t39]) ).
cnf(t50,plain,
complement(sF0) = sF1,
inference(orient,[status(thm)],[t71809]) ).
cnf(t72040,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sk3),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72039,t50]) ).
cnf(f2,axiom,
A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
file('/export/starexec/sandbox/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(f0,axiom,
join(A,B) = join(B,A),
file('/export/starexec/sandbox/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(t83,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t71823,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t12,t83]) ).
cnf(t251,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t71823]) ).
cnf(f10,axiom,
join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
file('/export/starexec/sandbox/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(t71817,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t83]) ).
cnf(t181,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t71817]) ).
cnf(f9,axiom,
converse(composition(A,B)) = composition(converse(B),converse(A)),
file('/export/starexec/sandbox/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(t53,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/sandbox/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(t38,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t55,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t53,t38]) ).
cnf(t77,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t55]) ).
cnf(f5,axiom,
composition(A,one) = A,
file('/export/starexec/sandbox/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(t37,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t78,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t77,t37]) ).
cnf(t71810,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t78,t38]) ).
cnf(t81,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t71810]) ).
cnf(t82,plain,
one = converse(one),
inference(cp,[status(thm)],[t81,t37]) ).
cnf(t92,plain,
converse(one) = one,
inference(orient,[status(thm)],[t82]) ).
cnf(t195,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t181,t92]) ).
cnf(t71813,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t81,t92]) ).
cnf(t93,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t71813]) ).
cnf(t103,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t93]) ).
cnf(t71827,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t195,t103]) ).
cnf(t71828,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t71827,t103]) ).
cnf(t295,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t71828]) ).
cnf(t302,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t251,t295]) ).
cnf(f11,axiom,
top = join(A,complement(A)),
file('/export/starexec/sandbox/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(t42,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t71894,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t302,t42]) ).
cnf(t71895,plain,
X1 = join(complement(top),complement(complement(X1))),
inference(step,[status(thm)],[t71894,t83]) ).
cnf(f12,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox/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(f3,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox/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(t5,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t71814,plain,
complement(top) = zero,
inference(step,[status(thm)],[t5,t42]) ).
cnf(t104,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t71814]) ).
cnf(t71896,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t71895,t104]) ).
cnf(t583,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t71896]) ).
cnf(t300,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t295,t104]) ).
cnf(t71839,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t300,t104]) ).
cnf(t71840,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t71839,t104]) ).
cnf(t359,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t71840]) ).
cnf(t360,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t64,t359]) ).
cnf(t714,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t360]) ).
cnf(t717,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t714,t583]) ).
cnf(t71957,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t717,t583]) ).
cnf(t718,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t71957]) ).
cnf(t71962,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t583,t718]) ).
cnf(t723,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t71962]) ).
cnf(t820,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t723]) ).
cnf(t22,axiom,
sF5 = complement(sk3),
introduced(definition) ).
cnf(t36,plain,
complement(sk3) = sF5,
inference(orient,[status(thm)],[t22]) ).
cnf(t821,plain,
sk3 = complement(sF5),
inference(cp,[status(thm)],[t820,t36]) ).
cnf(t23,axiom,
sF6 = complement(complement(sk3)),
introduced(definition) ).
cnf(t71808,plain,
sF6 = complement(sF5),
inference(step,[status(thm)],[t23,t36]) ).
cnf(t41,plain,
complement(sF5) = sF6,
inference(orient,[status(thm)],[t71808]) ).
cnf(t71970,plain,
sk3 = sF6,
inference(step,[status(thm)],[t821,t41]) ).
cnf(t833,plain,
sk3 = sF6,
inference(orient,[status(thm)],[t71970]) ).
cnf(t72041,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72040,t833]) ).
cnf(t72042,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(composition(sk1,sk3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72041,t83]) ).
cnf(t72043,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72042,t833]) ).
cnf(t21,axiom,
sF4 = complement(sk2),
introduced(definition) ).
cnf(t35,plain,
complement(sk2) = sF4,
inference(orient,[status(thm)],[t21]) ).
cnf(t72044,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,complement(join(sF4,complement(complement(sk3))))))))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72043,t35]) ).
cnf(t72045,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,complement(join(sF4,sk3))))))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72044,t820]) ).
cnf(t72046,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,complement(join(sF4,sF6))))))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72045,t833]) ).
cnf(t24,axiom,
sF7 = join(complement(sk2),complement(complement(sk3))),
introduced(definition) ).
cnf(t71878,plain,
sF7 = join(sF4,complement(complement(sk3))),
inference(step,[status(thm)],[t24,t35]) ).
cnf(t71879,plain,
sF7 = join(sF4,complement(sF5)),
inference(step,[status(thm)],[t71878,t36]) ).
cnf(t71880,plain,
sF7 = join(sF4,sF6),
inference(step,[status(thm)],[t71879,t41]) ).
cnf(t542,plain,
join(sF4,sF6) = sF7,
inference(orient,[status(thm)],[t71880]) ).
cnf(t72047,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,complement(sF7)))))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72046,t542]) ).
cnf(t25,axiom,
sF8 = complement(join(complement(sk2),complement(complement(sk3)))),
introduced(definition) ).
cnf(t71888,plain,
sF8 = complement(join(sF4,complement(complement(sk3)))),
inference(step,[status(thm)],[t25,t35]) ).
cnf(t71889,plain,
sF8 = complement(join(sF4,complement(sF5))),
inference(step,[status(thm)],[t71888,t36]) ).
cnf(t71890,plain,
sF8 = complement(join(sF4,sF6)),
inference(step,[status(thm)],[t71889,t41]) ).
cnf(t71891,plain,
sF8 = complement(sF7),
inference(step,[status(thm)],[t71890,t542]) ).
cnf(t565,plain,
complement(sF7) = sF8,
inference(orient,[status(thm)],[t71891]) ).
cnf(t72048,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,sF8))))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72047,t565]) ).
cnf(t26,axiom,
sF9 = composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))),
introduced(definition) ).
cnf(t71899,plain,
sF9 = composition(sk1,complement(join(sF4,complement(complement(sk3))))),
inference(step,[status(thm)],[t26,t35]) ).
cnf(t71900,plain,
sF9 = composition(sk1,complement(join(sF4,complement(sF5)))),
inference(step,[status(thm)],[t71899,t36]) ).
cnf(t71901,plain,
sF9 = composition(sk1,complement(join(sF4,sF6))),
inference(step,[status(thm)],[t71900,t41]) ).
cnf(t71902,plain,
sF9 = composition(sk1,complement(sF7)),
inference(step,[status(thm)],[t71901,t542]) ).
cnf(t71903,plain,
sF9 = composition(sk1,sF8),
inference(step,[status(thm)],[t71902,t565]) ).
cnf(t596,plain,
composition(sk1,sF8) = sF9,
inference(orient,[status(thm)],[t71903]) ).
cnf(t72049,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(sF9)))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72048,t596]) ).
cnf(t72050,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(complement(sF9),composition(sk1,sF6)))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72049,t83]) ).
cnf(t27,axiom,
sF10 = complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),
introduced(definition) ).
cnf(t71904,plain,
sF10 = complement(composition(sk1,complement(join(sF4,complement(complement(sk3)))))),
inference(step,[status(thm)],[t27,t35]) ).
cnf(t71905,plain,
sF10 = complement(composition(sk1,complement(join(sF4,complement(sF5))))),
inference(step,[status(thm)],[t71904,t36]) ).
cnf(t71906,plain,
sF10 = complement(composition(sk1,complement(join(sF4,sF6)))),
inference(step,[status(thm)],[t71905,t41]) ).
cnf(t71907,plain,
sF10 = complement(composition(sk1,complement(sF7))),
inference(step,[status(thm)],[t71906,t542]) ).
cnf(t71908,plain,
sF10 = complement(composition(sk1,sF8)),
inference(step,[status(thm)],[t71907,t565]) ).
cnf(t71909,plain,
sF10 = complement(sF9),
inference(step,[status(thm)],[t71908,t596]) ).
cnf(t616,plain,
complement(sF9) = sF10,
inference(orient,[status(thm)],[t71909]) ).
cnf(t72051,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72050,t616]) ).
cnf(t72052,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(composition(sk1,sk3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72051,t83]) ).
cnf(t72053,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(composition(sk1,sF6),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72052,t833]) ).
cnf(t72054,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(composition(sk1,sF6),complement(composition(sk1,complement(join(sF4,complement(complement(sk3))))))),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72053,t35]) ).
cnf(t72055,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(composition(sk1,sF6),complement(composition(sk1,complement(join(sF4,sk3))))),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72054,t820]) ).
cnf(t72056,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(composition(sk1,sF6),complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72055,t833]) ).
cnf(t72057,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(composition(sk1,sF6),complement(composition(sk1,complement(sF7)))),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72056,t542]) ).
cnf(t72058,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(composition(sk1,sF6),complement(composition(sk1,sF8))),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72057,t565]) ).
cnf(t72059,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(composition(sk1,sF6),complement(sF9)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72058,t596]) ).
cnf(t72060,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(complement(sF9),composition(sk1,sF6)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72059,t83]) ).
cnf(t72061,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72060,t616]) ).
cnf(t72062,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72061,t64]) ).
cnf(t72063,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72062,t64]) ).
cnf(t72064,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(complement(composition(sk1,complement(join(sF4,complement(complement(sk3)))))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72063,t35]) ).
cnf(t72065,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(complement(composition(sk1,complement(join(sF4,sk3)))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72064,t820]) ).
cnf(t72066,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(complement(composition(sk1,complement(join(sF4,sF6)))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72065,t833]) ).
cnf(t72067,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(complement(composition(sk1,complement(sF7))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72066,t542]) ).
cnf(t72068,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(complement(composition(sk1,sF8)),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72067,t565]) ).
cnf(t72069,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(complement(sF9),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72068,t596]) ).
cnf(t72070,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(sF10,join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72069,t616]) ).
cnf(t72071,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(sF10,join(composition(sk1,sF6),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72070,t833]) ).
cnf(t72072,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(sF10,join(composition(sk1,sF6),join(composition(sk1,sk3),complement(composition(sk1,sk2))))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72071,t83]) ).
cnf(t72073,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(sF10,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,sk2))))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72072,t833]) ).
cnf(t72074,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(sF10,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(sF0)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72073,t39]) ).
cnf(t72075,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(sF10,join(composition(sk1,sF6),join(complement(sF0),composition(sk1,sF6)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72074,t83]) ).
cnf(t72076,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(join(sF10,join(composition(sk1,sF6),join(sF1,composition(sk1,sF6)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72075,t50]) ).
cnf(t32,axiom,
sF15 = join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),
introduced(definition) ).
cnf(t71977,plain,
sF15 = join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3))),
inference(step,[status(thm)],[t32,t64]) ).
cnf(t71978,plain,
sF15 = join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71977,t64]) ).
cnf(t71979,plain,
sF15 = join(complement(composition(sk1,complement(join(sF4,complement(complement(sk3)))))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71978,t35]) ).
cnf(t71980,plain,
sF15 = join(complement(composition(sk1,complement(join(sF4,sk3)))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71979,t820]) ).
cnf(t71981,plain,
sF15 = join(complement(composition(sk1,complement(join(sF4,sF6)))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71980,t833]) ).
cnf(t71982,plain,
sF15 = join(complement(composition(sk1,complement(sF7))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71981,t542]) ).
cnf(t71983,plain,
sF15 = join(complement(composition(sk1,sF8)),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71982,t565]) ).
cnf(t71984,plain,
sF15 = join(complement(sF9),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71983,t596]) ).
cnf(t71985,plain,
sF15 = join(sF10,join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71984,t616]) ).
cnf(t71986,plain,
sF15 = join(sF10,join(composition(sk1,sF6),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71985,t833]) ).
cnf(t71987,plain,
sF15 = join(sF10,join(composition(sk1,sF6),join(composition(sk1,sk3),complement(composition(sk1,sk2))))),
inference(step,[status(thm)],[t71986,t83]) ).
cnf(t71988,plain,
sF15 = join(sF10,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,sk2))))),
inference(step,[status(thm)],[t71987,t833]) ).
cnf(t71989,plain,
sF15 = join(sF10,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(sF0)))),
inference(step,[status(thm)],[t71988,t39]) ).
cnf(t71990,plain,
sF15 = join(sF10,join(composition(sk1,sF6),join(complement(sF0),composition(sk1,sF6)))),
inference(step,[status(thm)],[t71989,t83]) ).
cnf(t71991,plain,
sF15 = join(sF10,join(composition(sk1,sF6),join(sF1,composition(sk1,sF6)))),
inference(step,[status(thm)],[t71990,t50]) ).
cnf(t849,plain,
join(sF10,join(composition(sk1,sF6),join(sF1,composition(sk1,sF6)))) = sF15,
inference(orient,[status(thm)],[t71991]) ).
cnf(t72077,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(sF15,join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true),
inference(step,[status(thm)],[t72076,t849]) ).
cnf(t72078,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(sF15,join(composition(sk1,sk3),complement(composition(sk1,sk2))),false,true),true),
inference(step,[status(thm)],[t72077,t83]) ).
cnf(t72079,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(sF15,join(composition(sk1,sF6),complement(composition(sk1,sk2))),false,true),true),
inference(step,[status(thm)],[t72078,t833]) ).
cnf(t72080,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(sF15,join(composition(sk1,sF6),complement(sF0)),false,true),true),
inference(step,[status(thm)],[t72079,t39]) ).
cnf(t72081,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(sF15,join(complement(sF0),composition(sk1,sF6)),false,true),true),
inference(step,[status(thm)],[t72080,t83]) ).
cnf(t72082,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),ifeq(sF15,join(sF1,composition(sk1,sF6)),false,true),true),
inference(step,[status(thm)],[t72081,t50]) ).
cnf(t33,axiom,
sF16 = ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
introduced(definition) ).
cnf(t71996,plain,
sF16 = ifeq(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t33,t64]) ).
cnf(t71997,plain,
sF16 = ifeq(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t71996,t64]) ).
cnf(t71998,plain,
sF16 = ifeq(join(complement(composition(sk1,complement(join(sF4,complement(complement(sk3)))))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t71997,t35]) ).
cnf(t71999,plain,
sF16 = ifeq(join(complement(composition(sk1,complement(join(sF4,sk3)))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t71998,t820]) ).
cnf(t72000,plain,
sF16 = ifeq(join(complement(composition(sk1,complement(join(sF4,sF6)))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t71999,t833]) ).
cnf(t72001,plain,
sF16 = ifeq(join(complement(composition(sk1,complement(sF7))),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72000,t542]) ).
cnf(t72002,plain,
sF16 = ifeq(join(complement(composition(sk1,sF8)),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72001,t565]) ).
cnf(t72003,plain,
sF16 = ifeq(join(complement(sF9),join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72002,t596]) ).
cnf(t72004,plain,
sF16 = ifeq(join(sF10,join(composition(sk1,sk3),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72003,t616]) ).
cnf(t72005,plain,
sF16 = ifeq(join(sF10,join(composition(sk1,sF6),join(complement(composition(sk1,sk2)),composition(sk1,sk3)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72004,t833]) ).
cnf(t72006,plain,
sF16 = ifeq(join(sF10,join(composition(sk1,sF6),join(composition(sk1,sk3),complement(composition(sk1,sk2))))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72005,t83]) ).
cnf(t72007,plain,
sF16 = ifeq(join(sF10,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(composition(sk1,sk2))))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72006,t833]) ).
cnf(t72008,plain,
sF16 = ifeq(join(sF10,join(composition(sk1,sF6),join(composition(sk1,sF6),complement(sF0)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72007,t39]) ).
cnf(t72009,plain,
sF16 = ifeq(join(sF10,join(composition(sk1,sF6),join(complement(sF0),composition(sk1,sF6)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72008,t83]) ).
cnf(t72010,plain,
sF16 = ifeq(join(sF10,join(composition(sk1,sF6),join(sF1,composition(sk1,sF6)))),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72009,t50]) ).
cnf(t72011,plain,
sF16 = ifeq(sF15,join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),
inference(step,[status(thm)],[t72010,t849]) ).
cnf(t72012,plain,
sF16 = ifeq(sF15,join(composition(sk1,sk3),complement(composition(sk1,sk2))),false,true),
inference(step,[status(thm)],[t72011,t83]) ).
cnf(t72013,plain,
sF16 = ifeq(sF15,join(composition(sk1,sF6),complement(composition(sk1,sk2))),false,true),
inference(step,[status(thm)],[t72012,t833]) ).
cnf(t72014,plain,
sF16 = ifeq(sF15,join(composition(sk1,sF6),complement(sF0)),false,true),
inference(step,[status(thm)],[t72013,t39]) ).
cnf(t72015,plain,
sF16 = ifeq(sF15,join(complement(sF0),composition(sk1,sF6)),false,true),
inference(step,[status(thm)],[t72014,t83]) ).
cnf(t72016,plain,
sF16 = ifeq(sF15,join(sF1,composition(sk1,sF6)),false,true),
inference(step,[status(thm)],[t72015,t50]) ).
cnf(t862,plain,
ifeq(sF15,join(sF1,composition(sk1,sF6)),false,true) = sF16,
inference(orient,[status(thm)],[t72016]) ).
cnf(t72083,plain,
sF17 = ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),sF16,true),
inference(step,[status(thm)],[t72082,t862]) ).
cnf(t898,plain,
ifeq(join(sF1,join(composition(sk1,sF6),join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),sF16,true) = sF17,
inference(orient,[status(thm)],[t72083]) ).
cnf(t19,axiom,
sF2 = composition(sk1,sk3),
introduced(definition) ).
cnf(t40,plain,
composition(sk1,sk3) = sF2,
inference(orient,[status(thm)],[t19]) ).
cnf(t71971,plain,
composition(sk1,sF6) = sF2,
inference(step,[status(thm)],[t40,t833]) ).
cnf(t835,plain,
composition(sk1,sF6) = sF2,
inference(rw,[status(thm)],[t71971]) ).
cnf(t922,plain,
composition(sk1,sF6) = sF2,
inference(orient,[status(thm)],[t835]) ).
cnf(t72084,plain,
ifeq(join(sF1,join(sF2,join(sF10,composition(sk1,sF6)))),join(sF10,composition(sk1,sF6)),sF16,true) = sF17,
inference(step,[status(thm)],[t898,t922]) ).
cnf(t72085,plain,
ifeq(join(sF1,join(sF2,join(sF10,sF2))),join(sF10,composition(sk1,sF6)),sF16,true) = sF17,
inference(step,[status(thm)],[t72084,t922]) ).
cnf(t72086,plain,
ifeq(join(sF1,join(sF2,join(sF10,sF2))),join(sF10,sF2),sF16,true) = sF17,
inference(step,[status(thm)],[t72085,t922]) ).
cnf(t925,plain,
ifeq(join(sF1,join(sF2,join(sF10,sF2))),join(sF10,sF2),sF16,true) = sF17,
inference(rw,[status(thm)],[t72086]) ).
cnf(t20,axiom,
sF3 = join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
introduced(definition) ).
cnf(t71869,plain,
sF3 = join(composition(sk1,sk3),complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t20,t83]) ).
cnf(t71870,plain,
sF3 = join(sF2,complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t71869,t40]) ).
cnf(t71871,plain,
sF3 = join(sF2,complement(sF0)),
inference(step,[status(thm)],[t71870,t39]) ).
cnf(t71872,plain,
sF3 = join(sF2,sF1),
inference(step,[status(thm)],[t71871,t50]) ).
cnf(t71873,plain,
sF3 = join(sF1,sF2),
inference(step,[status(thm)],[t71872,t83]) ).
cnf(t526,plain,
join(sF1,sF2) = sF3,
inference(orient,[status(thm)],[t71873]) ).
cnf(t529,plain,
join(sF1,join(sF2,X1)) = join(sF3,X1),
inference(cp,[status(thm)],[t64,t526]) ).
cnf(t1171,plain,
join(sF1,join(sF2,X1)) = join(sF3,X1),
inference(orient,[status(thm)],[t529]) ).
cnf(t73064,plain,
ifeq(join(sF3,join(sF10,sF2)),join(sF10,sF2),sF16,true) = sF17,
inference(step,[status(thm)],[t925,t1171]) ).
cnf(t31,axiom,
sF14 = join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),
introduced(definition) ).
cnf(t740,plain,
join(sF3,sF10) = sF14,
inference(orient,[status(thm)],[t31]) ).
cnf(t742,plain,
join(sF3,join(sF10,X1)) = join(sF14,X1),
inference(cp,[status(thm)],[t64,t740]) ).
cnf(t30,axiom,
sF13 = join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),
introduced(definition) ).
cnf(t71945,plain,
sF13 = join(composition(sk1,sk3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t30,t83]) ).
cnf(t71946,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
inference(step,[status(thm)],[t71945,t40]) ).
cnf(t71947,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(sF4,complement(complement(sk3))))))),
inference(step,[status(thm)],[t71946,t35]) ).
cnf(t71948,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(sF4,complement(sF5)))))),
inference(step,[status(thm)],[t71947,t36]) ).
cnf(t71949,plain,
sF13 = join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),
inference(step,[status(thm)],[t71948,t41]) ).
cnf(t71950,plain,
sF13 = join(sF2,complement(composition(sk1,complement(sF7)))),
inference(step,[status(thm)],[t71949,t542]) ).
cnf(t71951,plain,
sF13 = join(sF2,complement(composition(sk1,sF8))),
inference(step,[status(thm)],[t71950,t565]) ).
cnf(t71952,plain,
sF13 = join(sF2,complement(sF9)),
inference(step,[status(thm)],[t71951,t596]) ).
cnf(t71953,plain,
sF13 = join(sF2,sF10),
inference(step,[status(thm)],[t71952,t616]) ).
cnf(t701,plain,
join(sF2,sF10) = sF13,
inference(orient,[status(thm)],[t71953]) ).
cnf(t1176,plain,
join(sF3,sF10) = join(sF1,sF13),
inference(cp,[status(thm)],[t1171,t701]) ).
cnf(t72107,plain,
sF14 = join(sF1,sF13),
inference(step,[status(thm)],[t1176,t740]) ).
cnf(t28,axiom,
sF11 = join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),
introduced(definition) ).
cnf(t71913,plain,
sF11 = join(complement(composition(sk1,sk2)),join(composition(sk1,sk3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t28,t64]) ).
cnf(t71914,plain,
sF11 = join(complement(sF0),join(composition(sk1,sk3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t71913,t39]) ).
cnf(t71915,plain,
sF11 = join(sF1,join(composition(sk1,sk3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t71914,t50]) ).
cnf(t71916,plain,
sF11 = join(sF1,join(sF2,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))))),
inference(step,[status(thm)],[t71915,t40]) ).
cnf(t71917,plain,
sF11 = join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,complement(complement(sk3)))))))),
inference(step,[status(thm)],[t71916,t35]) ).
cnf(t71918,plain,
sF11 = join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,complement(sF5))))))),
inference(step,[status(thm)],[t71917,t36]) ).
cnf(t71919,plain,
sF11 = join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6)))))),
inference(step,[status(thm)],[t71918,t41]) ).
cnf(t71920,plain,
sF11 = join(sF1,join(sF2,complement(composition(sk1,complement(sF7))))),
inference(step,[status(thm)],[t71919,t542]) ).
cnf(t71921,plain,
sF11 = join(sF1,join(sF2,complement(composition(sk1,sF8)))),
inference(step,[status(thm)],[t71920,t565]) ).
cnf(t71922,plain,
sF11 = join(sF1,join(sF2,complement(sF9))),
inference(step,[status(thm)],[t71921,t596]) ).
cnf(t71923,plain,
sF11 = join(sF1,join(sF2,sF10)),
inference(step,[status(thm)],[t71922,t616]) ).
cnf(t647,plain,
join(sF1,join(sF2,sF10)) = sF11,
inference(orient,[status(thm)],[t71923]) ).
cnf(t71954,plain,
join(sF1,sF13) = sF11,
inference(step,[status(thm)],[t647,t701]) ).
cnf(t702,plain,
join(sF1,sF13) = sF11,
inference(rw,[status(thm)],[t71954]) ).
cnf(t706,plain,
join(sF1,sF13) = sF11,
inference(orient,[status(thm)],[t702]) ).
cnf(t72108,plain,
sF14 = sF11,
inference(step,[status(thm)],[t72107,t706]) ).
cnf(t1181,plain,
sF14 = sF11,
inference(orient,[status(thm)],[t72108]) ).
cnf(t72142,plain,
join(sF3,join(sF10,X1)) = join(sF11,X1),
inference(step,[status(thm)],[t742,t1181]) ).
cnf(t1828,plain,
join(sF3,join(sF10,X1)) = join(sF11,X1),
inference(orient,[status(thm)],[t72142]) ).
cnf(t73065,plain,
ifeq(join(sF11,sF2),join(sF10,sF2),sF16,true) = sF17,
inference(step,[status(thm)],[t73064,t1828]) ).
cnf(t73066,plain,
ifeq(join(sF2,sF11),join(sF10,sF2),sF16,true) = sF17,
inference(step,[status(thm)],[t73065,t83]) ).
cnf(t705,plain,
join(sF2,join(sF10,X1)) = join(sF13,X1),
inference(cp,[status(thm)],[t64,t701]) ).
cnf(t1683,plain,
join(sF2,join(sF10,X1)) = join(sF13,X1),
inference(orient,[status(thm)],[t705]) ).
cnf(t825,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t295,t820]) ).
cnf(t72023,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t825,t820]) ).
cnf(t72024,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t72023,t820]) ).
cnf(t871,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t72024]) ).
cnf(t1832,plain,
join(sF11,sF10) = join(sF3,sF10),
inference(cp,[status(thm)],[t1828,t871]) ).
cnf(t72148,plain,
join(sF10,sF11) = join(sF3,sF10),
inference(step,[status(thm)],[t1832,t83]) ).
cnf(t72109,plain,
join(sF3,sF10) = sF11,
inference(step,[status(thm)],[t740,t1181]) ).
cnf(t1182,plain,
join(sF3,sF10) = sF11,
inference(orient,[status(thm)],[t72109]) ).
cnf(t72149,plain,
join(sF10,sF11) = sF11,
inference(step,[status(thm)],[t72148,t1182]) ).
cnf(t1886,plain,
join(sF10,sF11) = sF11,
inference(orient,[status(thm)],[t72149]) ).
cnf(t1892,plain,
join(sF13,sF11) = join(sF2,sF11),
inference(cp,[status(thm)],[t1683,t1886]) ).
cnf(t72150,plain,
join(sF11,sF13) = join(sF2,sF11),
inference(step,[status(thm)],[t1892,t83]) ).
cnf(t708,plain,
join(sF1,join(sF13,X1)) = join(sF11,X1),
inference(cp,[status(thm)],[t64,t706]) ).
cnf(t1796,plain,
join(sF1,join(sF13,X1)) = join(sF11,X1),
inference(orient,[status(thm)],[t708]) ).
cnf(t1800,plain,
join(sF11,sF13) = join(sF1,sF13),
inference(cp,[status(thm)],[t1796,t871]) ).
cnf(t72139,plain,
join(sF11,sF13) = sF11,
inference(step,[status(thm)],[t1800,t706]) ).
cnf(t1810,plain,
join(sF11,sF13) = sF11,
inference(orient,[status(thm)],[t72139]) ).
cnf(t72151,plain,
sF11 = join(sF2,sF11),
inference(step,[status(thm)],[t72150,t1810]) ).
cnf(t1894,plain,
join(sF2,sF11) = sF11,
inference(orient,[status(thm)],[t72151]) ).
cnf(t73067,plain,
ifeq(sF11,join(sF10,sF2),sF16,true) = sF17,
inference(step,[status(thm)],[t73066,t1894]) ).
cnf(t73068,plain,
ifeq(sF11,join(sF2,sF10),sF16,true) = sF17,
inference(step,[status(thm)],[t73067,t83]) ).
cnf(t73069,plain,
ifeq(sF11,sF13,sF16,true) = sF17,
inference(step,[status(thm)],[t73068,t701]) ).
cnf(f16,negated_conjecture,
( join(join(join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)) != join(complement(composition(sk1,sk2)),composition(sk1,sk3))
| join(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,meet(sk2,complement(sk3))))),composition(sk1,sk3)) != join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_17) ).
fof(f16_nnf,plain,
( join(join(join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)) != join(complement(composition(sk1,sk2)),composition(sk1,sk3))
| join(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,meet(sk2,complement(sk3))))),composition(sk1,sk3)) != join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
( join(join(join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)) != join(complement(composition(sk1,sk2)),composition(sk1,sk3))
| join(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,meet(sk2,complement(sk3))))),composition(sk1,sk3)) != join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
( join(join(join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)) != join(complement(composition(sk1,sk2)),composition(sk1,sk3))
| join(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,meet(sk2,complement(sk3))))),composition(sk1,sk3)) != join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(u4,axiom,
ifeq(join(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,meet(sk2,complement(sk3))))),composition(sk1,sk3)),join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t16,plain,
ifeq(join(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),composition(sk1,sk3)),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),ifeq(join(join(join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)),complement(composition(sk1,sk2))),composition(sk1,sk3)),join(complement(composition(sk1,sk2)),composition(sk1,sk3)),false,true),true) = true,
inference(definition_unfolding,[status(thm)],[u4,d0]) ).
cnf(t501,plain,
ifeq(join(sF1,join(sF2,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),join(sF1,sF2),false,true),true) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t71874,plain,
ifeq(join(sF1,join(sF2,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t501,t526]) ).
cnf(t527,plain,
ifeq(join(sF1,join(sF2,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(rw,[status(thm)],[t71874]) ).
cnf(t72726,plain,
ifeq(join(sF3,join(sF2,complement(composition(sk1,complement(join(sF4,sF6)))))),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t527,t1171]) ).
cnf(t90,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(cp,[status(thm)],[t83,t64]) ).
cnf(t1528,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t90]) ).
cnf(t72727,plain,
ifeq(join(sF2,join(complement(composition(sk1,complement(join(sF4,sF6)))),sF3)),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72726,t1528]) ).
cnf(t91,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t64,t83]) ).
cnf(t72127,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t91,t64]) ).
cnf(t1597,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t72127]) ).
cnf(t1177,plain,
join(sF3,sF2) = join(sF1,sF2),
inference(cp,[status(thm)],[t1171,t871]) ).
cnf(t72111,plain,
join(sF2,sF3) = join(sF1,sF2),
inference(step,[status(thm)],[t1177,t83]) ).
cnf(t72112,plain,
join(sF2,sF3) = sF3,
inference(step,[status(thm)],[t72111,t526]) ).
cnf(t1184,plain,
join(sF2,sF3) = sF3,
inference(orient,[status(thm)],[t72112]) ).
cnf(t1640,plain,
join(sF2,join(X1,sF3)) = join(X1,sF3),
inference(cp,[status(thm)],[t1597,t1184]) ).
cnf(t2834,plain,
join(sF2,join(X1,sF3)) = join(X1,sF3),
inference(orient,[status(thm)],[t1640]) ).
cnf(t72728,plain,
ifeq(join(complement(composition(sk1,complement(join(sF4,sF6)))),sF3),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72727,t2834]) ).
cnf(t72729,plain,
ifeq(join(sF3,complement(composition(sk1,complement(join(sF4,sF6))))),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72728,t83]) ).
cnf(t72730,plain,
ifeq(join(sF3,complement(composition(sk1,complement(sF7)))),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72729,t542]) ).
cnf(t72731,plain,
ifeq(join(sF3,complement(composition(sk1,sF8))),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72730,t565]) ).
cnf(t72732,plain,
ifeq(join(sF3,complement(sF9)),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72731,t596]) ).
cnf(t72733,plain,
ifeq(join(sF3,sF10),join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72732,t616]) ).
cnf(t72734,plain,
ifeq(sF11,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72733,t1182]) ).
cnf(t72735,plain,
ifeq(sF11,join(sF2,complement(composition(sk1,complement(sF7)))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72734,t542]) ).
cnf(t72736,plain,
ifeq(sF11,join(sF2,complement(composition(sk1,sF8))),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72735,t565]) ).
cnf(t72737,plain,
ifeq(sF11,join(sF2,complement(sF9)),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72736,t596]) ).
cnf(t72738,plain,
ifeq(sF11,join(sF2,sF10),ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72737,t616]) ).
cnf(t72739,plain,
ifeq(sF11,sF13,ifeq(join(sF2,join(sF1,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72738,t701]) ).
cnf(t72740,plain,
ifeq(sF11,sF13,ifeq(join(sF1,join(join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))),sF2)),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72739,t1528]) ).
cnf(t1174,plain,
join(sF3,X1) = join(sF1,join(X1,sF2)),
inference(cp,[status(thm)],[t1171,t83]) ).
cnf(t2086,plain,
join(sF1,join(X1,sF2)) = join(sF3,X1),
inference(orient,[status(thm)],[t1174]) ).
cnf(t72741,plain,
ifeq(sF11,sF13,ifeq(join(sF3,join(sF2,complement(composition(sk1,complement(join(sF4,sF6)))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72740,t2086]) ).
cnf(t72742,plain,
ifeq(sF11,sF13,ifeq(join(sF2,join(complement(composition(sk1,complement(join(sF4,sF6)))),sF3)),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72741,t1528]) ).
cnf(t72743,plain,
ifeq(sF11,sF13,ifeq(join(complement(composition(sk1,complement(join(sF4,sF6)))),sF3),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72742,t2834]) ).
cnf(t72744,plain,
ifeq(sF11,sF13,ifeq(join(sF3,complement(composition(sk1,complement(join(sF4,sF6))))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72743,t83]) ).
cnf(t72745,plain,
ifeq(sF11,sF13,ifeq(join(sF3,complement(composition(sk1,complement(sF7)))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72744,t542]) ).
cnf(t72746,plain,
ifeq(sF11,sF13,ifeq(join(sF3,complement(composition(sk1,sF8))),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72745,t565]) ).
cnf(t72747,plain,
ifeq(sF11,sF13,ifeq(join(sF3,complement(sF9)),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72746,t596]) ).
cnf(t72748,plain,
ifeq(sF11,sF13,ifeq(join(sF3,sF10),sF3,false,true),true) = true,
inference(step,[status(thm)],[t72747,t616]) ).
cnf(t72749,plain,
ifeq(sF11,sF13,ifeq(sF11,sF3,false,true),true) = true,
inference(step,[status(thm)],[t72748,t1182]) ).
cnf(t924,plain,
ifeq(sF15,join(sF1,sF2),false,true) = sF16,
inference(rw,[status(thm)],[t862]) ).
cnf(t923,plain,
join(sF10,join(sF2,join(sF1,sF2))) = sF15,
inference(rw,[status(thm)],[t849]) ).
cnf(t72564,plain,
join(sF2,join(join(sF1,sF2),sF10)) = sF15,
inference(step,[status(thm)],[t923,t1528]) ).
cnf(t1627,plain,
join(sF2,join(X1,sF10)) = join(X1,sF13),
inference(cp,[status(thm)],[t1597,t701]) ).
cnf(t2510,plain,
join(sF2,join(X1,sF10)) = join(X1,sF13),
inference(orient,[status(thm)],[t1627]) ).
cnf(t72565,plain,
join(join(sF1,sF2),sF13) = sF15,
inference(step,[status(thm)],[t72564,t2510]) ).
cnf(t72566,plain,
join(sF1,join(sF2,sF13)) = sF15,
inference(step,[status(thm)],[t72565,t64]) ).
cnf(t72567,plain,
join(sF3,sF13) = sF15,
inference(step,[status(thm)],[t72566,t1171]) ).
cnf(t29,axiom,
sF12 = join(join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))),composition(sk1,sk3)),
introduced(definition) ).
cnf(t71926,plain,
sF12 = join(join(complement(composition(sk1,sk2)),composition(sk1,sk3)),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3))),
inference(step,[status(thm)],[t29,t64]) ).
cnf(t71927,plain,
sF12 = join(complement(composition(sk1,sk2)),join(composition(sk1,sk3),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71926,t64]) ).
cnf(t71928,plain,
sF12 = join(complement(sF0),join(composition(sk1,sk3),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71927,t39]) ).
cnf(t71929,plain,
sF12 = join(sF1,join(composition(sk1,sk3),join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71928,t50]) ).
cnf(t71930,plain,
sF12 = join(sF1,join(sF2,join(complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3)))))),composition(sk1,sk3)))),
inference(step,[status(thm)],[t71929,t40]) ).
cnf(t71931,plain,
sF12 = join(sF1,join(sF2,join(composition(sk1,sk3),complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),
inference(step,[status(thm)],[t71930,t83]) ).
cnf(t71932,plain,
sF12 = join(sF1,join(sF2,join(sF2,complement(composition(sk1,complement(join(complement(sk2),complement(complement(sk3))))))))),
inference(step,[status(thm)],[t71931,t40]) ).
cnf(t71933,plain,
sF12 = join(sF1,join(sF2,join(sF2,complement(composition(sk1,complement(join(sF4,complement(complement(sk3))))))))),
inference(step,[status(thm)],[t71932,t35]) ).
cnf(t71934,plain,
sF12 = join(sF1,join(sF2,join(sF2,complement(composition(sk1,complement(join(sF4,complement(sF5)))))))),
inference(step,[status(thm)],[t71933,t36]) ).
cnf(t71935,plain,
sF12 = join(sF1,join(sF2,join(sF2,complement(composition(sk1,complement(join(sF4,sF6))))))),
inference(step,[status(thm)],[t71934,t41]) ).
cnf(t71936,plain,
sF12 = join(sF1,join(sF2,join(sF2,complement(composition(sk1,complement(sF7)))))),
inference(step,[status(thm)],[t71935,t542]) ).
cnf(t71937,plain,
sF12 = join(sF1,join(sF2,join(sF2,complement(composition(sk1,sF8))))),
inference(step,[status(thm)],[t71936,t565]) ).
cnf(t71938,plain,
sF12 = join(sF1,join(sF2,join(sF2,complement(sF9)))),
inference(step,[status(thm)],[t71937,t596]) ).
cnf(t71939,plain,
sF12 = join(sF1,join(sF2,join(sF2,sF10))),
inference(step,[status(thm)],[t71938,t616]) ).
cnf(t675,plain,
join(sF1,join(sF2,join(sF2,sF10))) = sF12,
inference(orient,[status(thm)],[t71939]) ).
cnf(t71955,plain,
join(sF1,join(sF2,sF13)) = sF12,
inference(step,[status(thm)],[t675,t701]) ).
cnf(t703,plain,
join(sF1,join(sF2,sF13)) = sF12,
inference(rw,[status(thm)],[t71955]) ).
cnf(t72128,plain,
join(sF3,sF13) = sF12,
inference(step,[status(thm)],[t703,t1171]) ).
cnf(t1676,plain,
join(sF3,sF13) = sF12,
inference(orient,[status(thm)],[t72128]) ).
cnf(t1687,plain,
join(sF13,sF10) = join(sF2,sF10),
inference(cp,[status(thm)],[t1683,t871]) ).
cnf(t72132,plain,
join(sF10,sF13) = join(sF2,sF10),
inference(step,[status(thm)],[t1687,t83]) ).
cnf(t72133,plain,
join(sF10,sF13) = sF13,
inference(step,[status(thm)],[t72132,t701]) ).
cnf(t1702,plain,
join(sF10,sF13) = sF13,
inference(orient,[status(thm)],[t72133]) ).
cnf(t1708,plain,
join(sF13,sF13) = join(sF2,sF13),
inference(cp,[status(thm)],[t1683,t1702]) ).
cnf(t72134,plain,
sF13 = join(sF2,sF13),
inference(step,[status(thm)],[t1708,t871]) ).
cnf(t1747,plain,
join(sF2,sF13) = sF13,
inference(orient,[status(thm)],[t72134]) ).
cnf(t1750,plain,
join(sF3,sF13) = join(sF1,sF13),
inference(cp,[status(thm)],[t1171,t1747]) ).
cnf(t72135,plain,
sF12 = join(sF1,sF13),
inference(step,[status(thm)],[t1750,t1676]) ).
cnf(t72136,plain,
sF12 = sF11,
inference(step,[status(thm)],[t72135,t706]) ).
cnf(t1754,plain,
sF12 = sF11,
inference(orient,[status(thm)],[t72136]) ).
cnf(t72137,plain,
join(sF3,sF13) = sF11,
inference(step,[status(thm)],[t1676,t1754]) ).
cnf(t1758,plain,
join(sF3,sF13) = sF11,
inference(orient,[status(thm)],[t72137]) ).
cnf(t72568,plain,
sF11 = sF15,
inference(step,[status(thm)],[t72567,t1758]) ).
cnf(t13748,plain,
sF15 = sF11,
inference(orient,[status(thm)],[t72568]) ).
cnf(t72569,plain,
ifeq(sF11,join(sF1,sF2),false,true) = sF16,
inference(step,[status(thm)],[t924,t13748]) ).
cnf(t72570,plain,
ifeq(sF11,sF3,false,true) = sF16,
inference(step,[status(thm)],[t72569,t526]) ).
cnf(t13749,plain,
ifeq(sF11,sF3,false,true) = sF16,
inference(orient,[status(thm)],[t72570]) ).
cnf(t72750,plain,
ifeq(sF11,sF13,sF16,true) = true,
inference(step,[status(thm)],[t72749,t13749]) ).
cnf(t23312,plain,
ifeq(sF11,sF13,sF16,true) = true,
inference(orient,[status(thm)],[t72750]) ).
cnf(t73070,plain,
true = sF17,
inference(step,[status(thm)],[t73069,t23312]) ).
cnf(t38462,plain,
true = sF17,
inference(orient,[status(thm)],[t73070]) ).
cnf(t38464,plain,
ifeq(sF11,sF13,sF16,sF17) = true,
inference(rw,[status(thm)],[t23312]) ).
cnf(t73072,plain,
ifeq(sF11,sF13,sF16,sF17) = sF17,
inference(step,[status(thm)],[t38464,t38462]) ).
cnf(t38466,plain,
ifeq(sF11,sF13,sF16,sF17) = sF17,
inference(orient,[status(thm)],[t73072]) ).
cnf(t60615,plain,
ifeq(sF11,sF11,sF16,sF17) = sF17,
inference(rw,[status(thm)],[t38466]) ).
cnf(t3,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t48,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t73303,plain,
sF16 = sF17,
inference(step,[status(thm)],[t60615,t48]) ).
cnf(t63256,plain,
sF17 = sF16,
inference(orient,[status(thm)],[t73303]) ).
cnf(t73304,plain,
true = sF16,
inference(step,[status(thm)],[t38462,t63256]) ).
cnf(t63257,plain,
true = sF16,
inference(orient,[status(thm)],[t73304]) ).
cnf(t73071,plain,
ifeq(sF11,sF3,false,sF17) = sF16,
inference(step,[status(thm)],[t13749,t38462]) ).
cnf(t38463,plain,
ifeq(sF11,sF3,false,sF17) = sF16,
inference(rw,[status(thm)],[t73071]) ).
cnf(t38465,plain,
ifeq(sF11,sF3,false,sF17) = sF16,
inference(orient,[status(thm)],[t38463]) ).
cnf(t73306,plain,
ifeq(sF11,sF3,false,sF16) = sF16,
inference(step,[status(thm)],[t38465,t63256]) ).
cnf(t63259,plain,
ifeq(sF11,sF3,false,sF16) = sF16,
inference(rw,[status(thm)],[t73306]) ).
cnf(t64384,plain,
ifeq(sF11,sF3,false,sF16) = sF16,
inference(orient,[status(thm)],[t63259]) ).
cnf(t68823,plain,
ifeq(sF3,sF3,false,sF16) = sF16,
inference(rw,[status(thm)],[t64384]) ).
cnf(t73444,plain,
false = sF16,
inference(step,[status(thm)],[t68823,t48]) ).
cnf(t71807,plain,
false = sF16,
inference(orient,[status(thm)],[t73444]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(g0_0,plain,
sF16 != false,
inference(rw,[status(thm)],[goal_0,t63257]) ).
cnf(g0_1,plain,
sF16 != sF16,
inference(rw,[status(thm)],[g0_0,t71807]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL017-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.43 % Computer : n014.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Thu Sep 24 07:15:18 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.43 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 197.03/29.04 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 197.03/29.04 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------