%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL026-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:52 PM UTC 2026
% Result : Unsatisfiable 65.48s 8.72s
% Output : Proof 65.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 75
% Number of leaves : 16
% Syntax : Number of formulae : 236 ( 232 unt; 0 def)
% Number of atoms : 240 ( 239 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 14 ( 10 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-4 aty)
% Number of variables : 333 ( 9 sgn 50 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f14,negated_conjecture,
( join(meet(composition(sk1,top),sk2),composition(sk1,sk2)) != composition(sk1,sk2)
| join(composition(sk1,sk2),meet(composition(sk1,top),sk2)) != meet(composition(sk1,top),sk2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_15) ).
fof(f14_nnf,plain,
( join(meet(composition(sk1,top),sk2),composition(sk1,sk2)) != composition(sk1,sk2)
| join(composition(sk1,sk2),meet(composition(sk1,top),sk2)) != meet(composition(sk1,top),sk2) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( join(meet(composition(sk1,top),sk2),composition(sk1,sk2)) != composition(sk1,sk2)
| join(composition(sk1,sk2),meet(composition(sk1,top),sk2)) != meet(composition(sk1,top),sk2) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( join(meet(composition(sk1,top),sk2),composition(sk1,sk2)) != composition(sk1,sk2)
| join(composition(sk1,sk2),meet(composition(sk1,top),sk2)) != meet(composition(sk1,top),sk2) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(u1,axiom,
ifeq(join(composition(sk1,sk2),meet(composition(sk1,top),sk2)),meet(composition(sk1,top),sk2),ifeq(join(meet(composition(sk1,top),sk2),composition(sk1,sk2)),composition(sk1,sk2),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
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(t14,plain,
ifeq(join(composition(sk1,sk2),complement(join(complement(composition(sk1,top)),complement(sk2)))),complement(join(complement(composition(sk1,top)),complement(sk2))),ifeq(join(complement(join(complement(composition(sk1,top)),complement(sk2))),composition(sk1,sk2)),composition(sk1,sk2),false,true),true) = true,
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
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(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t33,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t58170,plain,
ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),complement(join(complement(composition(sk1,top)),complement(sk2))),ifeq(join(complement(join(complement(composition(sk1,top)),complement(sk2))),composition(sk1,sk2)),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t14,t33]) ).
cnf(t58171,plain,
ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(complement(join(complement(composition(sk1,top)),complement(sk2))),composition(sk1,sk2)),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t58170,t33]) ).
cnf(t58172,plain,
ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(composition(sk1,sk2),complement(join(complement(composition(sk1,top)),complement(sk2)))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t58171,t33]) ).
cnf(t58173,plain,
ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t58172,t33]) ).
cnf(t63,plain,
ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(orient,[status(thm)],[t58173]) ).
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(t13,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t15,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t34,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t15]) ).
cnf(t58190,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t34,t33]) ).
cnf(t256,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t58190]) ).
cnf(t268,plain,
join(complement(X1),X2) = join(complement(X1),complement(join(complement(join(complement(X1),X2)),complement(complement(join(complement(X1),complement(X2))))))),
inference(cp,[status(thm)],[t256,t256]) ).
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(t12,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t21,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t35,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(rw,[status(thm)],[t21]) ).
cnf(t58218,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t35,t33]) ).
cnf(t584,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t58218]) ).
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(t7,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t57,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
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(t19,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t59,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t57,t19]) ).
cnf(t121,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t59]) ).
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(t18,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t122,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t121,t18]) ).
cnf(t58177,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t122,t19]) ).
cnf(t135,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t58177]) ).
cnf(t136,plain,
one = converse(one),
inference(cp,[status(thm)],[t135,t18]) ).
cnf(t140,plain,
converse(one) = one,
inference(orient,[status(thm)],[t136]) ).
cnf(t587,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t584,t140]) ).
cnf(t58178,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t135,t140]) ).
cnf(t149,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t58178]) ).
cnf(t150,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t149]) ).
cnf(t58219,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t587,t150]) ).
cnf(t58220,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t58219,t150]) ).
cnf(t601,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t58220]) ).
cnf(t607,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t256,t601]) ).
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(t3,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t36,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t58263,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t607,t36]) ).
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(t6,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t24,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(orient,[status(thm)],[t6]) ).
cnf(t58169,plain,
complement(top) = zero,
inference(step,[status(thm)],[t24,t36]) ).
cnf(t37,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t58169]) ).
cnf(t64,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t37]) ).
cnf(t58264,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t58263,t64]) ).
cnf(t58265,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t58264,t33]) ).
cnf(t677,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t58265]) ).
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(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t38,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t602,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t601,t64]) ).
cnf(t58221,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t602,t64]) ).
cnf(t58222,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t58221,t64]) ).
cnf(t609,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t58222]) ).
cnf(t610,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t38,t609]) ).
cnf(t702,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t610]) ).
cnf(t703,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t702,t677]) ).
cnf(t58266,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t703,t677]) ).
cnf(t705,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t58266]) ).
cnf(t58267,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t677,t705]) ).
cnf(t717,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t58267]) ).
cnf(t726,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t717]) ).
cnf(t59611,plain,
join(complement(X1),X2) = join(complement(X1),complement(join(complement(join(complement(X1),X2)),join(complement(X1),complement(X2))))),
inference(step,[status(thm)],[t268,t726]) ).
cnf(t42,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t38,t33]) ).
cnf(t58347,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t42,t38]) ).
cnf(t2033,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t58347]) ).
cnf(t59612,plain,
join(complement(X1),X2) = join(complement(X1),complement(join(complement(X1),join(complement(join(complement(X1),X2)),complement(X2))))),
inference(step,[status(thm)],[t59611,t2033]) ).
cnf(t59613,plain,
join(complement(X1),X2) = join(complement(X1),complement(join(complement(X1),join(complement(X2),complement(join(complement(X1),X2)))))),
inference(step,[status(thm)],[t59612,t33]) ).
cnf(t727,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t601,t726]) ).
cnf(t58268,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t727,t726]) ).
cnf(t58269,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t58268,t726]) ).
cnf(t736,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t58269]) ).
cnf(t738,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t38,t736]) ).
cnf(t785,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t738]) ).
cnf(t789,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t785,t256]) ).
cnf(t58276,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t789,t256]) ).
cnf(t58277,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t58276,t33]) ).
cnf(t874,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t58277]) ).
cnf(t876,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(cp,[status(thm)],[t874,t33]) ).
cnf(t896,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t876]) ).
cnf(t899,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t896,t726]) ).
cnf(t945,plain,
join(complement(X1),complement(join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t899]) ).
cnf(t59614,plain,
join(complement(X1),X2) = join(complement(X1),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t59613,t945]) ).
cnf(t57270,plain,
join(complement(X1),complement(join(complement(X1),complement(X2)))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t59614]) ).
cnf(t57286,plain,
join(complement(complement(X1)),X2) = join(X1,complement(join(complement(complement(X1)),complement(X2)))),
inference(cp,[status(thm)],[t57270,t726]) ).
cnf(t59615,plain,
join(X1,X2) = join(X1,complement(join(complement(complement(X1)),complement(X2)))),
inference(step,[status(thm)],[t57286,t726]) ).
cnf(t59616,plain,
join(X1,X2) = join(X1,complement(join(X1,complement(X2)))),
inference(step,[status(thm)],[t59615,t726]) ).
cnf(t57365,plain,
join(X1,complement(join(X1,complement(X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t59616]) ).
cnf(t57398,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t57365,t726]) ).
cnf(t57478,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t57398]) ).
cnf(f6,axiom,
composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
file('/export/starexec/sandbox/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(t11,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t43,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t151,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t43,t150]) ).
cnf(t16225,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t151]) ).
cnf(f8,axiom,
converse(join(A,B)) = join(converse(A),converse(B)),
file('/export/starexec/sandbox/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(t8,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t46,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t48,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t46,t19]) ).
cnf(t93,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t48]) ).
cnf(t144,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t46,t140]) ).
cnf(t58179,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t144,t33]) ).
cnf(t162,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t58179]) ).
cnf(f13,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_14) ).
fof(f13_nnf,plain,
join(sk1,one) = one,
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
join(sk1,one) = one,
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t2,plain,
join(sk1,one) = one,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t51,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t164,plain,
join(one,converse(sk1)) = converse(one),
inference(cp,[status(thm)],[t162,t51]) ).
cnf(t58180,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t164,t140]) ).
cnf(t175,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t58180]) ).
cnf(t16379,plain,
join(X1,composition(converse(sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t16225,t175]) ).
cnf(t58681,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(step,[status(thm)],[t16379,t150]) ).
cnf(t16577,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(orient,[status(thm)],[t58681]) ).
cnf(t16584,plain,
join(X1,converse(composition(converse(sk1),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t93,t16577]) ).
cnf(t58682,plain,
join(X1,composition(converse(converse(X1)),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t16584,t121]) ).
cnf(t58683,plain,
join(X1,composition(X1,sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t58682,t19]) ).
cnf(t58684,plain,
join(X1,composition(X1,sk1)) = X1,
inference(step,[status(thm)],[t58683,t19]) ).
cnf(t16623,plain,
join(X1,composition(X1,sk1)) = X1,
inference(orient,[status(thm)],[t58684]) ).
cnf(t16659,plain,
join(X1,composition(composition(one,sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t16225,t16623]) ).
cnf(f4,axiom,
composition(A,composition(B,C)) = composition(composition(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_associativity_5) ).
fof(f4_nnf,plain,
! [A,B,C] : composition(A,composition(B,C)) = composition(composition(A,B),C),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C] : composition(A,composition(B,C)) = composition(composition(A,B),C),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t9,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t53,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t58685,plain,
join(X1,composition(one,composition(sk1,X1))) = composition(one,X1),
inference(step,[status(thm)],[t16659,t53]) ).
cnf(t58686,plain,
join(X1,composition(sk1,X1)) = composition(one,X1),
inference(step,[status(thm)],[t58685,t150]) ).
cnf(t58687,plain,
join(X1,composition(sk1,X1)) = X1,
inference(step,[status(thm)],[t58686,t150]) ).
cnf(t16660,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t58687]) ).
cnf(t16664,plain,
join(X1,join(composition(sk1,X1),X2)) = join(X1,X2),
inference(cp,[status(thm)],[t38,t16660]) ).
cnf(t17712,plain,
join(X1,join(composition(sk1,X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t16664]) ).
cnf(t129,plain,
converse(join(composition(converse(X1),X2),X3)) = join(composition(converse(X2),X1),converse(X3)),
inference(cp,[status(thm)],[t46,t121]) ).
cnf(t14362,plain,
converse(join(composition(converse(X1),X2),X3)) = join(composition(converse(X2),X1),converse(X3)),
inference(orient,[status(thm)],[t129]) ).
cnf(t62,plain,
composition(join(X1,converse(X2)),converse(X3)) = join(composition(X1,converse(X3)),converse(composition(X3,X2))),
inference(cp,[status(thm)],[t43,t57]) ).
cnf(t12960,plain,
join(composition(X1,converse(X2)),converse(composition(X2,X3))) = composition(join(X1,converse(X3)),converse(X2)),
inference(orient,[status(thm)],[t62]) ).
cnf(t14370,plain,
join(composition(converse(converse(X1)),X2),converse(converse(composition(X1,X3)))) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(cp,[status(thm)],[t14362,t12960]) ).
cnf(t58660,plain,
join(composition(X1,X2),converse(converse(composition(X1,X3)))) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t14370,t19]) ).
cnf(t58661,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t58660,t19]) ).
cnf(t98,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t57,t93]) ).
cnf(t13645,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t98]) ).
cnf(t58662,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t58661,t13645]) ).
cnf(t58663,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t58662,t19]) ).
cnf(t58664,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t58663,t19]) ).
cnf(t14521,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t58664]) ).
cnf(t17730,plain,
join(X1,composition(sk1,X2)) = join(X1,composition(sk1,join(X1,X2))),
inference(cp,[status(thm)],[t17712,t14521]) ).
cnf(t22881,plain,
join(X1,composition(sk1,join(X1,X2))) = join(X1,composition(sk1,X2)),
inference(orient,[status(thm)],[t17730]) ).
cnf(t22980,plain,
join(X1,composition(sk1,complement(X1))) = join(X1,composition(sk1,top)),
inference(cp,[status(thm)],[t22881,t36]) ).
cnf(t23337,plain,
join(X1,composition(sk1,complement(X1))) = join(X1,composition(sk1,top)),
inference(orient,[status(thm)],[t22980]) ).
cnf(t57515,plain,
join(X1,complement(composition(sk1,complement(X1)))) = join(X1,complement(join(X1,composition(sk1,top)))),
inference(cp,[status(thm)],[t57478,t23337]) ).
cnf(t16685,plain,
complement(composition(sk1,X1)) = join(complement(composition(sk1,X1)),complement(X1)),
inference(cp,[status(thm)],[t945,t16660]) ).
cnf(t58800,plain,
complement(composition(sk1,X1)) = join(complement(X1),complement(composition(sk1,X1))),
inference(step,[status(thm)],[t16685,t33]) ).
cnf(t20584,plain,
join(complement(X1),complement(composition(sk1,X1))) = complement(composition(sk1,X1)),
inference(orient,[status(thm)],[t58800]) ).
cnf(t20585,plain,
complement(composition(sk1,complement(X1))) = join(X1,complement(composition(sk1,complement(X1)))),
inference(cp,[status(thm)],[t20584,t726]) ).
cnf(t25666,plain,
join(X1,complement(composition(sk1,complement(X1)))) = complement(composition(sk1,complement(X1))),
inference(orient,[status(thm)],[t20585]) ).
cnf(t59618,plain,
complement(composition(sk1,complement(X1))) = join(X1,complement(join(X1,composition(sk1,top)))),
inference(step,[status(thm)],[t57515,t25666]) ).
cnf(t59619,plain,
complement(composition(sk1,complement(X1))) = join(X1,complement(composition(sk1,top))),
inference(step,[status(thm)],[t59618,t57478]) ).
cnf(t58047,plain,
join(X1,complement(composition(sk1,top))) = complement(composition(sk1,complement(X1))),
inference(orient,[status(thm)],[t59619]) ).
cnf(t59621,plain,
ifeq(join(composition(sk1,sk2),complement(complement(composition(sk1,complement(complement(sk2)))))),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t63,t58047]) ).
cnf(t59622,plain,
ifeq(join(composition(sk1,sk2),composition(sk1,complement(complement(sk2)))),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t59621,t726]) ).
cnf(t59623,plain,
ifeq(composition(sk1,join(sk2,complement(complement(sk2)))),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t59622,t14521]) ).
cnf(t59624,plain,
ifeq(composition(sk1,join(sk2,sk2)),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t59623,t726]) ).
cnf(t59625,plain,
ifeq(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top)))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t59624,t736]) ).
cnf(t59626,plain,
ifeq(composition(sk1,sk2),complement(complement(composition(sk1,complement(complement(sk2))))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t59625,t58047]) ).
cnf(t59627,plain,
ifeq(composition(sk1,sk2),composition(sk1,complement(complement(sk2))),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t59626,t726]) ).
cnf(t59628,plain,
ifeq(composition(sk1,sk2),composition(sk1,sk2),ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true),true) = true,
inference(step,[status(thm)],[t59627,t726]) ).
cnf(t4,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t20,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t59629,plain,
ifeq(join(composition(sk1,sk2),complement(join(complement(sk2),complement(composition(sk1,top))))),composition(sk1,sk2),false,true) = true,
inference(step,[status(thm)],[t59628,t20]) ).
cnf(t59630,plain,
ifeq(join(composition(sk1,sk2),complement(complement(composition(sk1,complement(complement(sk2)))))),composition(sk1,sk2),false,true) = true,
inference(step,[status(thm)],[t59629,t58047]) ).
cnf(t59631,plain,
ifeq(join(composition(sk1,sk2),composition(sk1,complement(complement(sk2)))),composition(sk1,sk2),false,true) = true,
inference(step,[status(thm)],[t59630,t726]) ).
cnf(t59632,plain,
ifeq(composition(sk1,join(sk2,complement(complement(sk2)))),composition(sk1,sk2),false,true) = true,
inference(step,[status(thm)],[t59631,t14521]) ).
cnf(t59633,plain,
ifeq(composition(sk1,join(sk2,sk2)),composition(sk1,sk2),false,true) = true,
inference(step,[status(thm)],[t59632,t726]) ).
cnf(t59634,plain,
ifeq(composition(sk1,sk2),composition(sk1,sk2),false,true) = true,
inference(step,[status(thm)],[t59633,t736]) ).
cnf(t59635,plain,
false = true,
inference(step,[status(thm)],[t59634,t20]) ).
cnf(t58167,plain,
false = true,
inference(rw,[status(thm)],[t59635]) ).
cnf(t58168,plain,
false = true,
inference(orient,[status(thm)],[t58167]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t58168]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL026-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n018.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % 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:23:18 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 65.48/8.72 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.48/8.72 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------