%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL004+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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:37 PM UTC 2026
% Result : Theorem 8.13s 1.82s
% Output : Proof 8.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 125
% Number of leaves : 15
% Syntax : Number of formulae : 430 ( 430 unt; 0 def)
% Number of atoms : 430 ( 429 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 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 : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 587 ( 88 sgn 86 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity) ).
fof(f1_nnf,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
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(t45,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f10_nnf,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
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]) ).
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f0_nnf,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
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(t42,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t24266,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t42]) ).
cnf(t53,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t24266]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f9_nnf,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
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(t26,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
fof(f7,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence) ).
fof(f7_nnf,plain,
! [X0] : converse(converse(X0)) = X0,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X0] : converse(converse(X0)) = X0,
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(t20,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t28,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t26,t20]) ).
cnf(t148,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t28]) ).
fof(f5,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity) ).
fof(f5_nnf,plain,
! [X0] : composition(X0,one) = X0,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X0] : composition(X0,one) = X0,
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(t16,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t149,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t148,t16]) ).
cnf(t24271,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t149,t20]) ).
cnf(t161,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t24271]) ).
cnf(t162,plain,
one = converse(one),
inference(cp,[status(thm)],[t161,t16]) ).
cnf(t171,plain,
converse(one) = one,
inference(orient,[status(thm)],[t162]) ).
cnf(t24272,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t161,t171]) ).
cnf(t181,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t24272]) ).
cnf(t182,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t181]) ).
cnf(t185,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t53,t182]) ).
cnf(t24274,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t185,t171]) ).
cnf(t24275,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t24274,t182]) ).
cnf(t211,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t24275]) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f3_nnf,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
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(t5,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t82,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t212,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t211,t82]) ).
cnf(t24295,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t212,t82]) ).
cnf(t24296,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t24295,t82]) ).
cnf(t435,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t24296]) ).
cnf(t84,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t82,t42]) ).
cnf(t24269,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t84,t82]) ).
cnf(t103,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t24269]) ).
cnf(t436,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t435,t103]) ).
cnf(t456,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t436]) ).
fof(f2,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(f2_nnf,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
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(t17,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t44,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t17]) ).
cnf(t24811,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t44,t42]) ).
cnf(t24812,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t24811,t82]) ).
cnf(t24813,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t24812,t42]) ).
cnf(t15096,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t24813]) ).
fof(f12,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero) ).
fof(f12_nnf,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t3,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t89,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t15097,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t15096,t89]) ).
cnf(t24921,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t15097,t82]) ).
cnf(t15771,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t24921]) ).
fof(f11,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top) ).
fof(f11_nnf,plain,
! [X0] : top = join(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X0] : top = join(X0,complement(X0)),
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(t50,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t83,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t82,t50]) ).
cnf(t24267,plain,
zero = complement(top),
inference(step,[status(thm)],[t83,t89]) ).
cnf(t94,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t24267]) ).
cnf(t215,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t211,t94]) ).
cnf(t24276,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t215,t94]) ).
cnf(t24277,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t24276,t94]) ).
cnf(t222,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t24277]) ).
cnf(t223,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t45,t222]) ).
cnf(t241,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t223]) ).
cnf(t15776,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t241,t15771]) ).
cnf(t24923,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t15776,t15771]) ).
cnf(t15791,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t24923]) ).
cnf(t24928,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t15771,t15791]) ).
cnf(t15817,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t24928]) ).
cnf(t15843,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t15817]) ).
cnf(t15844,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t456,t15843]) ).
cnf(t24963,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t15844,t15843]) ).
cnf(t24964,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t24963,t15843]) ).
cnf(t15910,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t24964]) ).
cnf(t15914,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t45,t15910]) ).
cnf(t15957,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t15914]) ).
cnf(t15973,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t15957,t15096]) ).
cnf(t24968,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t15973,t15096]) ).
cnf(t24969,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t24968,t42]) ).
cnf(t15982,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t24969]) ).
cnf(t15984,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t15982,t103]) ).
cnf(t16009,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t15984]) ).
cnf(t16014,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t45,t16009]) ).
cnf(t18443,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t16014]) ).
cnf(t221,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t82,t211]) ).
cnf(t228,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t221]) ).
cnf(t238,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t82,t228]) ).
cnf(t1070,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t238]) ).
cnf(t24947,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1070,t15843]) ).
cnf(t15876,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t24947]) ).
cnf(t16239,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t15876]) ).
cnf(t24976,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t15096,t16239]) ).
cnf(t16355,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t24976]) ).
cnf(t21675,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t16355]) ).
cnf(t21727,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t18443,t21675]) ).
cnf(t21879,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t21727]) ).
cnf(t21894,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t21879,t103]) ).
cnf(t22548,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t21894]) ).
cnf(t97,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t82,t94]) ).
cnf(t115,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t97]) ).
fof(f8,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity) ).
fof(f8_nnf,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t7,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t59,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t62,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t59,t20]) ).
cnf(t274,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t62]) ).
cnf(t52,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t45,t50]) ).
cnf(t310,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t52]) ).
cnf(t236,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t50,t228]) ).
cnf(t252,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t236]) ).
cnf(t314,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t310,t252]) ).
cnf(t316,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t310,t211]) ).
cnf(t24282,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t316,t50]) ).
cnf(t327,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t24282]) ).
cnf(t328,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t327,t82]) ).
cnf(t335,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t328]) ).
cnf(t24284,plain,
top = join(X1,top),
inference(step,[status(thm)],[t314,t335]) ).
cnf(t349,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t24284]) ).
cnf(t350,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t349,t42]) ).
cnf(t355,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t350]) ).
cnf(t61,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t59,t20]) ).
cnf(t257,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t61]) ).
cnf(t259,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t257,t50]) ).
cnf(t293,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t259]) ).
cnf(t358,plain,
top = converse(top),
inference(cp,[status(thm)],[t355,t293]) ).
cnf(t361,plain,
converse(top) = top,
inference(orient,[status(thm)],[t358]) ).
cnf(t366,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t26,t361]) ).
cnf(t373,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t366]) ).
cnf(t379,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t274,t373]) ).
cnf(t9973,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t379]) ).
fof(f6,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity) ).
fof(f6_nnf,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t10,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t23,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t29,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t23,t26]) ).
cnf(t1678,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t29]) ).
cnf(t9974,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t9973,t1678]) ).
cnf(t24702,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t9974,t20]) ).
cnf(t27,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t26,t20]) ).
cnf(t138,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t27]) ).
cnf(t24703,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t24702,t138]) ).
cnf(t24704,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t24703,t257]) ).
cnf(t24705,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t24704,t361]) ).
cnf(t24706,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t24705,t349]) ).
cnf(t10053,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t24706]) ).
cnf(t367,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t26,t361]) ).
cnf(t387,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t367]) ).
cnf(t375,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t59,t373]) ).
cnf(t4081,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t375]) ).
cnf(t4094,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t4081,t361]) ).
cnf(t4128,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t4094]) ).
cnf(t4132,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t4128,t23]) ).
cnf(t24470,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t4132,t373]) ).
cnf(t24471,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t24470,t373]) ).
cnf(t24472,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t24471,t355]) ).
cnf(t24473,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t24472,t361]) ).
cnf(t4246,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t24473]) ).
cnf(t4262,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t4246,t171]) ).
cnf(t24474,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t4262,t16]) ).
cnf(t24475,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t24474,t349]) ).
cnf(t4275,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t24475]) ).
cnf(t4280,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t53,t4275]) ).
cnf(t24483,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t4280,t94]) ).
cnf(t24484,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t24483,t94]) ).
cnf(t24485,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t24484,t361]) ).
cnf(t24486,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t24485,t94]) ).
fof(f13,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dedekind_law) ).
fof(f13_nnf,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t15,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t32,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t15]) ).
cnf(t63,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t45,t59]) ).
cnf(t1754,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t63]) ).
cnf(t319,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t310,t42]) ).
cnf(t24293,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t319,t355]) ).
cnf(t399,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t24293]) ).
cnf(t1758,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t1754,t399]) ).
cnf(t24373,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t1758,t42]) ).
cnf(t1809,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t24373]) ).
cnf(t1842,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t1809,t59]) ).
cnf(t24374,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t1842,t20]) ).
cnf(t24375,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t24374,t20]) ).
cnf(t1855,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t24375]) ).
cnf(t1885,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t1855,t42]) ).
cnf(t1888,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t1885]) ).
cnf(t55,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t53,t16]) ).
cnf(t1143,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t55]) ).
cnf(t1153,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1143,t20]) ).
cnf(t1171,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1153]) ).
cnf(t1899,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t1888,t1171]) ).
cnf(t24386,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t1899,t42]) ).
cnf(t2236,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t24386]) ).
cnf(t2251,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t82,t2236]) ).
cnf(t24387,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t2251,t94]) ).
cnf(t2257,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t24387]) ).
cnf(t2278,plain,
composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(cp,[status(thm)],[t32,t2257]) ).
cnf(t24388,plain,
composition(meet(X1,composition(complement(X1),converse(one))),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t2278,t20]) ).
cnf(t24389,plain,
composition(meet(X1,composition(complement(X1),one)),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t24388,t171]) ).
cnf(t24390,plain,
composition(meet(X1,complement(X1)),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t24389,t16]) ).
cnf(t24391,plain,
composition(zero,meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t24390,t89]) ).
cnf(t24392,plain,
composition(zero,zero) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t24391,t2257]) ).
cnf(t24393,plain,
composition(zero,zero) = join(meet(X1,complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t24392,t16]) ).
cnf(t24394,plain,
composition(zero,zero) = join(meet(X1,complement(X1)),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t24393,t20]) ).
cnf(t24395,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t24394,t89]) ).
cnf(t24396,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),converse(one))),zero)),
inference(step,[status(thm)],[t24395,t20]) ).
cnf(t24397,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),one)),zero)),
inference(step,[status(thm)],[t24396,t171]) ).
cnf(t24398,plain,
composition(zero,zero) = join(zero,composition(meet(X1,complement(X1)),zero)),
inference(step,[status(thm)],[t24397,t16]) ).
cnf(t24399,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t24398,t89]) ).
cnf(t2279,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t24399]) ).
cnf(t2282,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t45,t2279]) ).
cnf(t2384,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t2282]) ).
cnf(t2392,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t2384,t23]) ).
cnf(t24408,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t2392,t23]) ).
cnf(t2455,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t24408]) ).
cnf(t51,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t50,t45]) ).
cnf(t468,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t51]) ).
cnf(t485,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t468,t42]) ).
cnf(t569,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t485]) ).
cnf(t581,plain,
top = join(complement(X1),join(X1,complement(top))),
inference(cp,[status(thm)],[t569,t50]) ).
cnf(t24304,plain,
top = join(complement(X1),join(X1,zero)),
inference(step,[status(thm)],[t581,t94]) ).
cnf(t601,plain,
join(complement(X1),join(X1,zero)) = top,
inference(orient,[status(thm)],[t24304]) ).
cnf(t608,plain,
top = join(complement(X1),join(zero,X1)),
inference(cp,[status(thm)],[t601,t42]) ).
cnf(t610,plain,
join(complement(X1),join(zero,X1)) = top,
inference(orient,[status(thm)],[t608]) ).
cnf(t99,plain,
complement(top) = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(cp,[status(thm)],[t53,t94]) ).
cnf(t24332,plain,
zero = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(step,[status(thm)],[t99,t94]) ).
cnf(t1344,plain,
join(zero,composition(converse(X1),complement(composition(X1,top)))) = zero,
inference(orient,[status(thm)],[t24332]) ).
cnf(t1349,plain,
zero = join(zero,composition(top,complement(composition(top,top)))),
inference(cp,[status(thm)],[t1344,t361]) ).
cnf(t1366,plain,
join(zero,composition(top,complement(composition(top,top)))) = zero,
inference(orient,[status(thm)],[t1349]) ).
cnf(t1368,plain,
top = join(complement(composition(top,complement(composition(top,top)))),zero),
inference(cp,[status(thm)],[t610,t1366]) ).
cnf(t24353,plain,
top = join(zero,complement(composition(top,complement(composition(top,top))))),
inference(step,[status(thm)],[t1368,t42]) ).
cnf(t1608,plain,
join(zero,complement(composition(top,complement(composition(top,top))))) = top,
inference(orient,[status(thm)],[t24353]) ).
cnf(t2458,plain,
composition(join(zero,complement(composition(top,complement(composition(top,top))))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t2455,t1608]) ).
cnf(t24409,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t2458,t1608]) ).
cnf(t2484,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t24409]) ).
cnf(t24487,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t24486,t2484]) ).
cnf(t4286,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t24487]) ).
cnf(t4287,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t387,t4286]) ).
cnf(t4303,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t4287]) ).
cnf(t10105,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t10053,t4303]) ).
cnf(t24735,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t10105,t4303]) ).
cnf(t24736,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t24735,t42]) ).
cnf(t11080,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t24736]) ).
cnf(t2474,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t2455,t42]) ).
cnf(t2565,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t2474]) ).
cnf(t4288,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t23,t4286]) ).
cnf(t24493,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t4288,t355]) ).
cnf(t24494,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t24493,t4286]) ).
cnf(t4322,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t24494]) ).
cnf(t24497,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t2565,t4322]) ).
cnf(t4340,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t24497]) ).
cnf(t4372,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t4340]) ).
cnf(t4375,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t4372,t42]) ).
cnf(t4389,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t4375]) ).
cnf(t4391,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t23,t4389]) ).
cnf(t24523,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t4391,t45]) ).
cnf(t24524,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t24523,t4322]) ).
cnf(t4675,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t24524]) ).
cnf(t172,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t59,t171]) ).
cnf(t188,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t172]) ).
cnf(t194,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t148,t188]) ).
cnf(t3851,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t194]) ).
fof(f4,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity) ).
fof(f4_nnf,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
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(t8,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t21,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t25,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t23,t21]) ).
cnf(t870,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t25]) ).
cnf(t4278,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t870,t4275]) ).
cnf(t24609,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t4278,t23]) ).
cnf(t6191,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t24609]) ).
cnf(t6203,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t6191,t182]) ).
cnf(t24610,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t6203,t349]) ).
cnf(t24611,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t24610,t4275]) ).
cnf(t6226,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t24611]) ).
cnf(t6228,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t6226,t42]) ).
cnf(t6249,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t6228]) ).
cnf(t6264,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t3851,t6249]) ).
cnf(t24614,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t6264,t361]) ).
cnf(t24615,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t24614,t361]) ).
cnf(t6283,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t24615]) ).
cnf(t6284,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t6283,t42]) ).
cnf(t6298,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t6284]) ).
cnf(t6305,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t53,t6298]) ).
cnf(t24637,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t6305,t361]) ).
cnf(t24638,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t24637,t42]) ).
cnf(t24639,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t24638,t94]) ).
cnf(t24640,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t24639,t4286]) ).
cnf(t7080,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t24640]) ).
cnf(t7089,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t4675,t7080]) ).
cnf(t7349,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t7089]) ).
cnf(t15310,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t7349,t15096]) ).
cnf(t15315,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t15310]) ).
cnf(t15322,plain,
converse(zero) = join(converse(zero),zero),
inference(cp,[status(thm)],[t11080,t15315]) ).
cnf(t24857,plain,
converse(zero) = join(zero,converse(zero)),
inference(step,[status(thm)],[t15322,t42]) ).
cnf(t15476,plain,
join(zero,converse(zero)) = converse(zero),
inference(orient,[status(thm)],[t24857]) ).
cnf(t15486,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t274,t15476]) ).
cnf(t24858,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t15486,t42]) ).
cnf(t24859,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t24858,t15476]) ).
cnf(t24860,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t24859,t20]) ).
cnf(t15489,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t24860]) ).
cnf(t15492,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t26,t15489]) ).
cnf(t24892,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t15492,t15315]) ).
cnf(t24893,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t24892,t15489]) ).
cnf(t15573,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t24893]) ).
cnf(t15590,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t15573,t20]) ).
cnf(t15611,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t15590]) ).
cnf(t15622,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t53,t15611]) ).
cnf(t24894,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t15622,t15489]) ).
cnf(t24895,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t24894,t15611]) ).
cnf(t24896,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t24895,t42]) ).
cnf(t15624,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t24896]) ).
cnf(t24909,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t115,t15624]) ).
cnf(t15665,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t24909]) ).
cnf(t15666,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t15665]) ).
cnf(t15797,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t15791,t42]) ).
cnf(t15829,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t15797]) ).
cnf(t15839,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t15096,t15829]) ).
cnf(t1925,plain,
join(complement(X1),join(join(X2,X1),X3)) = join(top,X3),
inference(cp,[status(thm)],[t45,t1888]) ).
cnf(t24383,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t1925,t45]) ).
cnf(t24384,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t24383,t355]) ).
cnf(t2143,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t24384]) ).
cnf(t7090,plain,
top = join(complement(zero),join(X1,complement(join(X2,one)))),
inference(cp,[status(thm)],[t2143,t7080]) ).
cnf(t9242,plain,
join(complement(zero),join(X1,complement(join(X2,one)))) = top,
inference(orient,[status(thm)],[t7090]) ).
cnf(t15309,plain,
top = join(complement(zero),X1),
inference(cp,[status(thm)],[t9242,t15096]) ).
cnf(t15374,plain,
join(complement(zero),X1) = top,
inference(orient,[status(thm)],[t15309]) ).
cnf(t15375,plain,
top = complement(zero),
inference(cp,[status(thm)],[t15374,t53]) ).
cnf(t15417,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t15375]) ).
cnf(t15422,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t82,t15417]) ).
cnf(t24854,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t15422,t349]) ).
cnf(t24855,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t24854,t94]) ).
cnf(t15465,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t24855]) ).
cnf(t24950,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t15839,t15465]) ).
cnf(t24951,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t24950,t15624]) ).
cnf(t24952,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t24951,t15666]) ).
cnf(t15879,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t24952]) ).
cnf(t24953,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t15666,t15879]) ).
cnf(t15880,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t24953]) ).
cnf(t22572,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t22548,t15880]) ).
cnf(t23348,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t22572]) ).
cnf(t38,plain,
composition(meet(X1,composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(X1),X2))) = join(meet(composition(X1,converse(X3)),X2),composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t32,t20]) ).
cnf(t24690,plain,
composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2))) = join(meet(composition(X1,converse(X3)),X2),composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2)))),
inference(step,[status(thm)],[t38,t20]) ).
cnf(t9048,plain,
join(meet(composition(X1,converse(X2)),X3),composition(meet(X1,composition(X3,X2)),meet(converse(X2),composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,X2)),meet(converse(X2),composition(converse(X1),X3))),
inference(orient,[status(thm)],[t24690]) ).
cnf(t2267,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t2257,t20]) ).
cnf(t2291,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t2267]) ).
cnf(t2310,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t2291,t228]) ).
cnf(t3088,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t2310]) ).
cnf(t24949,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(step,[status(thm)],[t3088,t15843]) ).
cnf(t15878,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(rw,[status(thm)],[t24949]) ).
cnf(t17383,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t15878]) ).
cnf(t17398,plain,
composition(meet(one,composition(converse(complement(X1)),X1)),meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(cp,[status(thm)],[t9048,t17383]) ).
cnf(t24991,plain,
composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t17398,t17383]) ).
cnf(t24992,plain,
zero = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t24991,t15611]) ).
cnf(t24993,plain,
zero = join(meet(converse(complement(X1)),composition(one,converse(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t24992,t103]) ).
cnf(t24994,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t24993,t182]) ).
cnf(t24995,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t24994,t103]) ).
cnf(t24996,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t24995,t15611]) ).
cnf(t24997,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t24996,t15829]) ).
cnf(t17429,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t24997]) ).
cnf(t23385,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t23348,t17429]) ).
cnf(t25083,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t23385,t42]) ).
cnf(t25084,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t25083,t15829]) ).
cnf(t24066,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t25084]) ).
cnf(t24071,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t24066,t15880]) ).
cnf(t24291,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t293,t361]) ).
cnf(t364,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t24291]) ).
cnf(t16286,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t16239,t364]) ).
cnf(t25053,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t16286,t94]) ).
cnf(t21659,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t25053]) ).
cnf(t22553,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t22548,t21659]) ).
cnf(t25065,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t22553,t15880]) ).
cnf(t25066,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t25065,t15829]) ).
cnf(t22741,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t25066]) ).
cnf(t22760,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t22741,t20]) ).
cnf(t23901,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t22760]) ).
cnf(t25085,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t24071,t23901]) ).
cnf(t24118,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t25085]) ).
cnf(t24123,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t24118,t15880]) ).
cnf(t24189,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t24123]) ).
fof(f16,conjecture,
! [X0] : converse(complement(X0)) = complement(converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0] : converse(complement(X0)) = complement(converse(X0)),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0] : converse(complement(X0)) != complement(converse(X0)),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
converse(complement(sk0)) != complement(converse(sk0)),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f16_nnf]) ).
cnf(c16,plain,
converse(complement(sk0)) != complement(converse(sk0)),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
converse(complement(sk0)) != complement(converse(sk0)),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(g0_0,plain,
converse(complement(sk0)) != converse(complement(sk0)),
inference(rw,[status(thm)],[goal_0,t24189]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL004+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n013.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 07:05:51 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.13/1.82 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.13/1.82 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------