%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL042+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 : n017.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:36:06 PM UTC 2026
% Result : Theorem 27.12s 3.95s
% Output : Proof 27.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 153
% Number of leaves : 15
% Syntax : Number of formulae : 529 ( 525 unt; 0 def)
% Number of atoms : 533 ( 532 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 11 ( 7 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 7 ( 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 : 707 ( 141 sgn 90 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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(t43,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/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(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t46,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/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(t12,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t64095,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t43]) ).
cnf(t54,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t64095]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/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(t34,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/sandbox/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(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t36,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t34,t21]) ).
cnf(t160,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t36]) ).
fof(f5,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/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(t17,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t161,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t160,t17]) ).
cnf(t64100,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t161,t21]) ).
cnf(t173,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t64100]) ).
cnf(t174,plain,
one = converse(one),
inference(cp,[status(thm)],[t173,t17]) ).
cnf(t183,plain,
converse(one) = one,
inference(orient,[status(thm)],[t174]) ).
cnf(t64101,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t173,t183]) ).
cnf(t193,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t64101]) ).
cnf(t194,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t193]) ).
cnf(t197,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t54,t194]) ).
cnf(t64103,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t197,t183]) ).
cnf(t64104,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t64103,t194]) ).
cnf(t223,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t64104]) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/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(t83,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t224,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t223,t83]) ).
cnf(t64125,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t224,t83]) ).
cnf(t64126,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t64125,t83]) ).
cnf(t453,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t64126]) ).
cnf(t85,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t83,t43]) ).
cnf(t64098,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t85,t83]) ).
cnf(t111,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t64098]) ).
cnf(t454,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t453,t111]) ).
cnf(t474,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t454]) ).
fof(f2,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/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(t13,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t18,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t45,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t18]) ).
cnf(t64626,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t45,t43]) ).
cnf(t64627,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t64626,t83]) ).
cnf(t64628,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t64627,t43]) ).
cnf(t15217,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t64628]) ).
fof(f12,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/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(t90,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t15218,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t15217,t90]) ).
cnf(t64739,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t15218,t83]) ).
cnf(t15900,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t64739]) ).
fof(f11,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/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(t51,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t84,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t83,t51]) ).
cnf(t64096,plain,
zero = complement(top),
inference(step,[status(thm)],[t84,t90]) ).
cnf(t101,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t64096]) ).
cnf(t227,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t223,t101]) ).
cnf(t64105,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t227,t101]) ).
cnf(t64106,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t64105,t101]) ).
cnf(t234,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t64106]) ).
cnf(t235,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t46,t234]) ).
cnf(t254,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t235]) ).
cnf(t15905,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t254,t15900]) ).
cnf(t64741,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t15905,t15900]) ).
cnf(t15920,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t64741]) ).
cnf(t64746,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t15900,t15920]) ).
cnf(t15946,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t64746]) ).
cnf(t15972,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t15946]) ).
cnf(t15973,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t474,t15972]) ).
cnf(t64781,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t15973,t15972]) ).
cnf(t64782,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t64781,t15972]) ).
cnf(t16039,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t64782]) ).
cnf(t16043,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t46,t16039]) ).
cnf(t16086,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t16043]) ).
cnf(t16102,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t16086,t15217]) ).
cnf(t64786,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t16102,t15217]) ).
cnf(t64787,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t64786,t43]) ).
cnf(t16111,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t64787]) ).
cnf(t16113,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t16111,t111]) ).
cnf(t16138,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t16113]) ).
cnf(t16143,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t46,t16138]) ).
cnf(t18608,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t16143]) ).
cnf(t233,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t83,t223]) ).
cnf(t240,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t233]) ).
cnf(t250,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t83,t240]) ).
cnf(t1097,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t250]) ).
cnf(t64765,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1097,t15972]) ).
cnf(t16005,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t64765]) ).
cnf(t16368,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t16005]) ).
cnf(t64794,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t15217,t16368]) ).
cnf(t16485,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t64794]) ).
cnf(t21849,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t16485]) ).
cnf(t21903,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t18608,t21849]) ).
cnf(t22220,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t21903]) ).
cnf(t22235,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t22220,t111]) ).
cnf(t22726,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t22235]) ).
cnf(t104,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t83,t101]) ).
cnf(t124,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t104]) ).
fof(f8,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/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(t78,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t81,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t78,t21]) ).
cnf(t287,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t81]) ).
cnf(t53,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t46,t51]) ).
cnf(t323,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t53]) ).
cnf(t248,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t51,t240]) ).
cnf(t265,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t248]) ).
cnf(t327,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t323,t265]) ).
cnf(t329,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t323,t223]) ).
cnf(t64111,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t329,t51]) ).
cnf(t340,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t64111]) ).
cnf(t341,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t340,t83]) ).
cnf(t357,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t341]) ).
cnf(t64113,plain,
top = join(X1,top),
inference(step,[status(thm)],[t327,t357]) ).
cnf(t364,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t64113]) ).
cnf(t365,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t364,t43]) ).
cnf(t370,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t365]) ).
cnf(t80,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t78,t21]) ).
cnf(t270,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t80]) ).
cnf(t272,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t270,t51]) ).
cnf(t306,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t272]) ).
cnf(t373,plain,
top = converse(top),
inference(cp,[status(thm)],[t370,t306]) ).
cnf(t376,plain,
converse(top) = top,
inference(orient,[status(thm)],[t373]) ).
cnf(t381,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t34,t376]) ).
cnf(t388,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t381]) ).
cnf(t394,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t287,t388]) ).
cnf(t9650,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t394]) ).
fof(f6,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/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(t11,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t24,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t37,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t24,t34]) ).
cnf(t7919,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t37]) ).
cnf(t9651,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t9650,t7919]) ).
cnf(t64510,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t9651,t21]) ).
cnf(t35,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t34,t21]) ).
cnf(t150,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t35]) ).
cnf(t64511,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t64510,t150]) ).
cnf(t64512,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t64511,t270]) ).
cnf(t64513,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t64512,t376]) ).
cnf(t64514,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t64513,t364]) ).
cnf(t9732,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t64514]) ).
cnf(t382,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t34,t376]) ).
cnf(t402,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t382]) ).
cnf(t390,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t78,t388]) ).
cnf(t4238,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t390]) ).
cnf(t4250,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t4238,t376]) ).
cnf(t4284,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t4250]) ).
cnf(t4288,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t4284,t24]) ).
cnf(t64297,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t4288,t388]) ).
cnf(t64298,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t64297,t388]) ).
cnf(t64299,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t64298,t370]) ).
cnf(t64300,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t64299,t376]) ).
cnf(t4404,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t64300]) ).
cnf(t4420,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t4404,t183]) ).
cnf(t64301,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t4420,t17]) ).
cnf(t64302,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t64301,t364]) ).
cnf(t4433,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t64302]) ).
cnf(t4438,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t4433]) ).
cnf(t64310,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t4438,t101]) ).
cnf(t64311,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t64310,t101]) ).
cnf(t64312,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t64311,t376]) ).
cnf(t64313,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t64312,t101]) ).
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/sandbox/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(t16,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(t27,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)],[t16]) ).
cnf(t28,plain,
composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t27,t17]) ).
cnf(t64193,plain,
composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t28,t183]) ).
cnf(t64194,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t64193,t17]) ).
cnf(t64195,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t64194,t183]) ).
cnf(t64196,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t64195,t17]) ).
cnf(t1701,plain,
join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))) = composition(meet(X1,X2),meet(one,composition(converse(X1),X2))),
inference(orient,[status(thm)],[t64196]) ).
cnf(t82,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t46,t78]) ).
cnf(t1825,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t82]) ).
cnf(t332,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t323,t43]) ).
cnf(t64122,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t332,t370]) ).
cnf(t414,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t64122]) ).
cnf(t1829,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t1825,t414]) ).
cnf(t64207,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t1829,t43]) ).
cnf(t1879,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t64207]) ).
cnf(t1912,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t1879,t78]) ).
cnf(t64208,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t1912,t21]) ).
cnf(t64209,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t64208,t21]) ).
cnf(t1925,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t64209]) ).
cnf(t1955,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t1925,t43]) ).
cnf(t1958,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t1955]) ).
cnf(t56,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t54,t17]) ).
cnf(t1171,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t56]) ).
cnf(t1176,plain,
complement(one) = join(complement(one),composition(top,complement(top))),
inference(cp,[status(thm)],[t1171,t376]) ).
cnf(t64155,plain,
complement(one) = join(complement(one),composition(top,zero)),
inference(step,[status(thm)],[t1176,t101]) ).
cnf(t1196,plain,
join(complement(one),composition(top,zero)) = complement(one),
inference(orient,[status(thm)],[t64155]) ).
cnf(t1970,plain,
top = join(complement(composition(top,zero)),complement(one)),
inference(cp,[status(thm)],[t1958,t1196]) ).
cnf(t64210,plain,
top = join(complement(one),complement(composition(top,zero))),
inference(step,[status(thm)],[t1970,t43]) ).
cnf(t1998,plain,
join(complement(one),complement(composition(top,zero))) = top,
inference(orient,[status(thm)],[t64210]) ).
cnf(t2000,plain,
meet(one,composition(top,zero)) = complement(top),
inference(cp,[status(thm)],[t83,t1998]) ).
cnf(t64211,plain,
meet(one,composition(top,zero)) = zero,
inference(step,[status(thm)],[t2000,t101]) ).
cnf(t2006,plain,
meet(one,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t64211]) ).
cnf(t2012,plain,
composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(cp,[status(thm)],[t1701,t2006]) ).
cnf(t64212,plain,
composition(zero,meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t2012,t2006]) ).
cnf(t64213,plain,
composition(zero,meet(one,composition(one,composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t64212,t183]) ).
cnf(t64214,plain,
composition(zero,meet(one,composition(top,zero))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t64213,t194]) ).
cnf(t64215,plain,
composition(zero,zero) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t64214,t2006]) ).
cnf(t64216,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t64215,t2006]) ).
cnf(t64217,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(one,composition(top,zero))))),
inference(step,[status(thm)],[t64216,t183]) ).
cnf(t64218,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(top,zero)))),
inference(step,[status(thm)],[t64217,t194]) ).
cnf(t64219,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t64218,t2006]) ).
cnf(t2014,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t64219]) ).
cnf(t2017,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t46,t2014]) ).
cnf(t2409,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t2017]) ).
cnf(t2417,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t2409,t24]) ).
cnf(t64236,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t2417,t24]) ).
cnf(t2480,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t64236]) ).
cnf(t52,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t51,t46]) ).
cnf(t492,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t52]) ).
cnf(t509,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t492,t43]) ).
cnf(t593,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t509]) ).
cnf(t605,plain,
top = join(complement(X1),join(X1,complement(top))),
inference(cp,[status(thm)],[t593,t51]) ).
cnf(t64134,plain,
top = join(complement(X1),join(X1,zero)),
inference(step,[status(thm)],[t605,t101]) ).
cnf(t625,plain,
join(complement(X1),join(X1,zero)) = top,
inference(orient,[status(thm)],[t64134]) ).
cnf(t632,plain,
top = join(complement(X1),join(zero,X1)),
inference(cp,[status(thm)],[t625,t43]) ).
cnf(t634,plain,
join(complement(X1),join(zero,X1)) = top,
inference(orient,[status(thm)],[t632]) ).
cnf(t107,plain,
complement(top) = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(cp,[status(thm)],[t54,t101]) ).
cnf(t64162,plain,
zero = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(step,[status(thm)],[t107,t101]) ).
cnf(t1378,plain,
join(zero,composition(converse(X1),complement(composition(X1,top)))) = zero,
inference(orient,[status(thm)],[t64162]) ).
cnf(t1383,plain,
zero = join(zero,composition(top,complement(composition(top,top)))),
inference(cp,[status(thm)],[t1378,t376]) ).
cnf(t1400,plain,
join(zero,composition(top,complement(composition(top,top)))) = zero,
inference(orient,[status(thm)],[t1383]) ).
cnf(t1402,plain,
top = join(complement(composition(top,complement(composition(top,top)))),zero),
inference(cp,[status(thm)],[t634,t1400]) ).
cnf(t64183,plain,
top = join(zero,complement(composition(top,complement(composition(top,top))))),
inference(step,[status(thm)],[t1402,t43]) ).
cnf(t1648,plain,
join(zero,complement(composition(top,complement(composition(top,top))))) = top,
inference(orient,[status(thm)],[t64183]) ).
cnf(t2483,plain,
composition(join(zero,complement(composition(top,complement(composition(top,top))))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t2480,t1648]) ).
cnf(t64237,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t2483,t1648]) ).
cnf(t2509,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t64237]) ).
cnf(t64314,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t64313,t2509]) ).
cnf(t4450,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t64314]) ).
cnf(t4451,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t402,t4450]) ).
cnf(t4471,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t4451]) ).
cnf(t9785,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t9732,t4471]) ).
cnf(t64539,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t9785,t4471]) ).
cnf(t64540,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t64539,t43]) ).
cnf(t10539,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t64540]) ).
cnf(t2499,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t2480,t43]) ).
cnf(t2613,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t2499]) ).
cnf(t4452,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t24,t4450]) ).
cnf(t64320,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t4452,t370]) ).
cnf(t64321,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t64320,t4450]) ).
cnf(t4494,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t64321]) ).
cnf(t64324,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t2613,t4494]) ).
cnf(t4512,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t64324]) ).
cnf(t4652,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t4512]) ).
cnf(t4655,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t4652,t43]) ).
cnf(t4674,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t4655]) ).
cnf(t4676,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t24,t4674]) ).
cnf(t64347,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t4676,t46]) ).
cnf(t64348,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t64347,t4494]) ).
cnf(t4876,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t64348]) ).
cnf(t184,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t78,t183]) ).
cnf(t200,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t184]) ).
cnf(t206,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t160,t200]) ).
cnf(t4002,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t206]) ).
fof(f4,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/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(t9,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t22,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t26,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t24,t22]) ).
cnf(t833,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t4436,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t833,t4433]) ).
cnf(t64413,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t4436,t24]) ).
cnf(t6226,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t64413]) ).
cnf(t6233,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t6226,t194]) ).
cnf(t64414,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t6233,t364]) ).
cnf(t64415,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t64414,t4433]) ).
cnf(t6256,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t64415]) ).
cnf(t6258,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t6256,t43]) ).
cnf(t6279,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t6258]) ).
cnf(t6290,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t4002,t6279]) ).
cnf(t64418,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t6290,t376]) ).
cnf(t64419,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t64418,t376]) ).
cnf(t6314,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t64419]) ).
cnf(t6315,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t6314,t43]) ).
cnf(t6330,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t6315]) ).
cnf(t6336,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t6330]) ).
cnf(t64439,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t6336,t376]) ).
cnf(t64440,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t64439,t43]) ).
cnf(t64441,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t64440,t101]) ).
cnf(t64442,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t64441,t4450]) ).
cnf(t7048,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t64442]) ).
cnf(t7057,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t4876,t7048]) ).
cnf(t7297,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t7057]) ).
cnf(t15434,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t7297,t15217]) ).
cnf(t15439,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t15434]) ).
cnf(t15446,plain,
converse(zero) = join(converse(zero),zero),
inference(cp,[status(thm)],[t10539,t15439]) ).
cnf(t64675,plain,
converse(zero) = join(zero,converse(zero)),
inference(step,[status(thm)],[t15446,t43]) ).
cnf(t15604,plain,
join(zero,converse(zero)) = converse(zero),
inference(orient,[status(thm)],[t64675]) ).
cnf(t15614,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t287,t15604]) ).
cnf(t64676,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t15614,t43]) ).
cnf(t64677,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t64676,t15604]) ).
cnf(t64678,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t64677,t21]) ).
cnf(t15617,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t64678]) ).
cnf(t15620,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t34,t15617]) ).
cnf(t64710,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t15620,t15439]) ).
cnf(t64711,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t64710,t15617]) ).
cnf(t15701,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t64711]) ).
cnf(t15718,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t15701,t21]) ).
cnf(t15739,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t15718]) ).
cnf(t15750,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t54,t15739]) ).
cnf(t64712,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t15750,t15617]) ).
cnf(t64713,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t64712,t15739]) ).
cnf(t64714,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t64713,t43]) ).
cnf(t15752,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t64714]) ).
cnf(t64727,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t124,t15752]) ).
cnf(t15793,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t64727]) ).
cnf(t15794,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t15793]) ).
cnf(t15926,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t15920,t43]) ).
cnf(t15958,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t15926]) ).
cnf(t15968,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t15217,t15958]) ).
cnf(t1995,plain,
join(complement(X1),join(join(X2,X1),X3)) = join(top,X3),
inference(cp,[status(thm)],[t46,t1958]) ).
cnf(t64225,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t1995,t46]) ).
cnf(t64226,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t64225,t370]) ).
cnf(t2232,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t64226]) ).
cnf(t7058,plain,
top = join(complement(zero),join(X1,complement(join(X2,one)))),
inference(cp,[status(thm)],[t2232,t7048]) ).
cnf(t8811,plain,
join(complement(zero),join(X1,complement(join(X2,one)))) = top,
inference(orient,[status(thm)],[t7058]) ).
cnf(t15433,plain,
top = join(complement(zero),X1),
inference(cp,[status(thm)],[t8811,t15217]) ).
cnf(t15499,plain,
join(complement(zero),X1) = top,
inference(orient,[status(thm)],[t15433]) ).
cnf(t15500,plain,
top = complement(zero),
inference(cp,[status(thm)],[t15499,t54]) ).
cnf(t15543,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t15500]) ).
cnf(t15548,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t83,t15543]) ).
cnf(t64672,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t15548,t364]) ).
cnf(t64673,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t64672,t101]) ).
cnf(t15593,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t64673]) ).
cnf(t64768,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t15968,t15593]) ).
cnf(t64769,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t64768,t15752]) ).
cnf(t64770,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t64769,t15794]) ).
cnf(t16008,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t64770]) ).
cnf(t64771,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t15794,t16008]) ).
cnf(t16009,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t64771]) ).
cnf(t22750,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t22726,t16009]) ).
cnf(t23573,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t22750]) ).
cnf(t33,plain,
composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(converse(converse(X1)),X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t64428,plain,
composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))),
inference(step,[status(thm)],[t33,t21]) ).
cnf(t6503,plain,
join(meet(composition(converse(X1),X2),X3),composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3)))) = composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3))),
inference(orient,[status(thm)],[t64428]) ).
cnf(t31,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)],[t27,t21]) ).
cnf(t64332,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)],[t31,t21]) ).
cnf(t4534,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)],[t64332]) ).
cnf(t16377,plain,
meet(X1,complement(join(X2,X1))) = complement(top),
inference(cp,[status(thm)],[t16368,t1958]) ).
cnf(t64796,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(step,[status(thm)],[t16377,t101]) ).
cnf(t16495,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t64796]) ).
cnf(t16117,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t46,t16111]) ).
cnf(t18401,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t16117]) ).
cnf(t18414,plain,
join(X1,meet(meet(X1,X2),X3)) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t18401,t16111]) ).
cnf(t64840,plain,
join(X1,meet(meet(X1,X2),X3)) = X1,
inference(step,[status(thm)],[t18414,t16111]) ).
cnf(t18470,plain,
join(X1,meet(meet(X1,X2),X3)) = X1,
inference(orient,[status(thm)],[t64840]) ).
cnf(t16419,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t16368,t16009]) ).
cnf(t16694,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t16419]) ).
cnf(t16701,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t16138,t16694]) ).
cnf(t126,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t124,t83]) ).
cnf(t3531,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t126]) ).
cnf(t64742,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t3531,t15920]) ).
cnf(t15921,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t64742]) ).
cnf(t64777,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t15921,t16008]) ).
cnf(t16036,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t64777]) ).
cnf(t16640,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t16036]) ).
cnf(t64800,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t16701,t16640]) ).
cnf(t16848,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t64800]) ).
cnf(t16878,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t16009,t16848]) ).
cnf(t64801,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t16878,t16009]) ).
cnf(t16937,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t64801]) ).
cnf(t16940,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t16937,t16138]) ).
cnf(t64803,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t16940,t111]) ).
cnf(t17081,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t64803]) ).
cnf(t18474,plain,
X1 = join(X1,meet(meet(X2,X1),X3)),
inference(cp,[status(thm)],[t18470,t17081]) ).
cnf(t18530,plain,
join(X1,meet(meet(X2,X1),X3)) = X1,
inference(orient,[status(thm)],[t18474]) ).
cnf(t18555,plain,
zero = meet(meet(meet(X1,X2),X3),complement(X2)),
inference(cp,[status(thm)],[t16495,t18530]) ).
cnf(t64955,plain,
zero = meet(complement(X2),meet(meet(X1,X2),X3)),
inference(step,[status(thm)],[t18555,t111]) ).
cnf(t28076,plain,
meet(complement(X1),meet(meet(X2,X1),X3)) = zero,
inference(orient,[status(thm)],[t64955]) ).
fof(f16,conjecture,
! [X0] :
( ! [X1] : meet(composition(X0,X1),composition(X0,complement(X1))) = zero
=> join(composition(converse(X0),X0),one) = one ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0] :
( ! [X1] : meet(composition(X0,X1),composition(X0,complement(X1))) = zero
=> join(composition(converse(X0),X0),one) = one ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0] :
( join(composition(converse(X0),X0),one) != one
& ! [X1] : meet(composition(X0,X1),composition(X0,complement(X1))) = zero ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
! [X1] :
( join(composition(converse(sk0),sk0),one) != one
& meet(composition(sk0,X1),composition(sk0,complement(X1))) = zero ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f16_nnf]) ).
cnf(c16,plain,
meet(composition(sk0,X1),composition(sk0,complement(X1))) = zero,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t8,plain,
meet(composition(sk0,X1),composition(sk0,complement(X1))) = zero,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t95,plain,
meet(composition(sk0,X1),composition(sk0,complement(X1))) = zero,
inference(orient,[status(thm)],[t8]) ).
cnf(t96,plain,
zero = meet(sk0,composition(sk0,complement(one))),
inference(cp,[status(thm)],[t95,t17]) ).
cnf(t149,plain,
meet(sk0,composition(sk0,complement(one))) = zero,
inference(orient,[status(thm)],[t96]) ).
cnf(t21872,plain,
sk0 = join(zero,meet(sk0,complement(composition(sk0,complement(one))))),
inference(cp,[status(thm)],[t21849,t149]) ).
cnf(t64883,plain,
sk0 = meet(sk0,complement(composition(sk0,complement(one)))),
inference(step,[status(thm)],[t21872,t15920]) ).
cnf(t22919,plain,
meet(sk0,complement(composition(sk0,complement(one)))) = sk0,
inference(orient,[status(thm)],[t64883]) ).
cnf(t28130,plain,
zero = meet(complement(complement(composition(sk0,complement(one)))),meet(sk0,X1)),
inference(cp,[status(thm)],[t28076,t22919]) ).
cnf(t65003,plain,
zero = meet(composition(sk0,complement(one)),meet(sk0,X1)),
inference(step,[status(thm)],[t28130,t16009]) ).
cnf(t31683,plain,
meet(composition(sk0,complement(one)),meet(sk0,X1)) = zero,
inference(orient,[status(thm)],[t65003]) ).
cnf(t31684,plain,
zero = meet(meet(sk0,X1),composition(sk0,complement(one))),
inference(cp,[status(thm)],[t31683,t111]) ).
cnf(t32680,plain,
meet(meet(sk0,X1),composition(sk0,complement(one))) = zero,
inference(orient,[status(thm)],[t31684]) ).
cnf(t32692,plain,
composition(meet(meet(sk0,X1),composition(sk0,complement(one))),meet(converse(complement(one)),composition(converse(meet(sk0,X1)),sk0))) = join(meet(composition(meet(sk0,X1),converse(complement(one))),sk0),composition(zero,meet(converse(complement(one)),composition(converse(meet(sk0,X1)),sk0)))),
inference(cp,[status(thm)],[t4534,t32680]) ).
cnf(t65018,plain,
composition(zero,meet(converse(complement(one)),composition(converse(meet(sk0,X1)),sk0))) = join(meet(composition(meet(sk0,X1),converse(complement(one))),sk0),composition(zero,meet(converse(complement(one)),composition(converse(meet(sk0,X1)),sk0)))),
inference(step,[status(thm)],[t32692,t32680]) ).
cnf(t65019,plain,
zero = join(meet(composition(meet(sk0,X1),converse(complement(one))),sk0),composition(zero,meet(converse(complement(one)),composition(converse(meet(sk0,X1)),sk0)))),
inference(step,[status(thm)],[t65018,t15739]) ).
cnf(t65020,plain,
zero = join(meet(sk0,composition(meet(sk0,X1),converse(complement(one)))),composition(zero,meet(converse(complement(one)),composition(converse(meet(sk0,X1)),sk0)))),
inference(step,[status(thm)],[t65019,t111]) ).
cnf(t16422,plain,
join(complement(X1),X2) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t16009,t16368]) ).
cnf(t16711,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t16422]) ).
cnf(t1181,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1171,t21]) ).
cnf(t1199,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1181]) ).
cnf(t1968,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t1958,t1199]) ).
cnf(t64261,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t1968,t43]) ).
cnf(t3065,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t64261]) ).
cnf(t3080,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t83,t3065]) ).
cnf(t64262,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t3080,t101]) ).
cnf(t3085,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t64262]) ).
cnf(t3095,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t3085,t21]) ).
cnf(t3106,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t3095]) ).
cnf(t3127,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t3106,t240]) ).
cnf(t3446,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t3127]) ).
cnf(t2511,plain,
join(zero,join(composition(top,zero),X1)) = join(composition(top,zero),X1),
inference(cp,[status(thm)],[t46,t2509]) ).
cnf(t2628,plain,
join(zero,join(composition(top,zero),X1)) = join(composition(top,zero),X1),
inference(orient,[status(thm)],[t2511]) ).
cnf(t2636,plain,
join(composition(top,zero),X1) = join(zero,join(X1,composition(top,zero))),
inference(cp,[status(thm)],[t2628,t43]) ).
cnf(t2709,plain,
join(zero,join(X1,composition(top,zero))) = join(composition(top,zero),X1),
inference(orient,[status(thm)],[t2636]) ).
cnf(t2712,plain,
join(composition(top,zero),complement(one)) = join(zero,complement(one)),
inference(cp,[status(thm)],[t2709,t1196]) ).
cnf(t64249,plain,
join(complement(one),composition(top,zero)) = join(zero,complement(one)),
inference(step,[status(thm)],[t2712,t43]) ).
cnf(t64250,plain,
complement(one) = join(zero,complement(one)),
inference(step,[status(thm)],[t64249,t1196]) ).
cnf(t2730,plain,
join(zero,complement(one)) = complement(one),
inference(orient,[status(thm)],[t64250]) ).
cnf(t2743,plain,
meet(top,one) = complement(complement(one)),
inference(cp,[status(thm)],[t124,t2730]) ).
cnf(t64251,plain,
meet(top,one) = meet(one,one),
inference(step,[status(thm)],[t2743,t240]) ).
cnf(t2746,plain,
meet(one,one) = meet(top,one),
inference(orient,[status(thm)],[t64251]) ).
cnf(t3457,plain,
zero = meet(one,composition(converse(complement(one)),meet(top,one))),
inference(cp,[status(thm)],[t3446,t2746]) ).
cnf(t3522,plain,
meet(one,composition(converse(complement(one)),meet(top,one))) = zero,
inference(orient,[status(thm)],[t3457]) ).
cnf(t64779,plain,
meet(one,composition(converse(complement(one)),one)) = zero,
inference(step,[status(thm)],[t3522,t16008]) ).
cnf(t64780,plain,
meet(one,converse(complement(one))) = zero,
inference(step,[status(thm)],[t64779,t17]) ).
cnf(t16038,plain,
meet(one,converse(complement(one))) = zero,
inference(rw,[status(thm)],[t64780]) ).
cnf(t16080,plain,
meet(one,converse(complement(one))) = zero,
inference(orient,[status(thm)],[t16038]) ).
cnf(t21867,plain,
one = join(zero,meet(one,complement(converse(complement(one))))),
inference(cp,[status(thm)],[t21849,t16080]) ).
cnf(t64872,plain,
one = meet(one,complement(converse(complement(one)))),
inference(step,[status(thm)],[t21867,t15920]) ).
cnf(t21922,plain,
meet(one,complement(converse(complement(one)))) = one,
inference(orient,[status(thm)],[t64872]) ).
cnf(t21952,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(cp,[status(thm)],[t16711,t21922]) ).
cnf(t21959,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t21952]) ).
cnf(t21967,plain,
converse(complement(one)) = meet(converse(complement(one)),complement(one)),
inference(cp,[status(thm)],[t16937,t21959]) ).
cnf(t64878,plain,
converse(complement(one)) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t21967,t111]) ).
cnf(t16953,plain,
converse(X1) = meet(converse(X1),converse(join(X2,X1))),
inference(cp,[status(thm)],[t16937,t78]) ).
cnf(t18286,plain,
meet(converse(X1),converse(join(X2,X1))) = converse(X1),
inference(orient,[status(thm)],[t16953]) ).
cnf(t21970,plain,
converse(converse(complement(one))) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(cp,[status(thm)],[t18286,t21959]) ).
cnf(t64873,plain,
complement(one) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(step,[status(thm)],[t21970,t21]) ).
cnf(t64874,plain,
complement(one) = meet(converse(complement(one)),converse(converse(complement(one)))),
inference(step,[status(thm)],[t64873,t111]) ).
cnf(t64875,plain,
complement(one) = meet(converse(complement(one)),complement(one)),
inference(step,[status(thm)],[t64874,t21]) ).
cnf(t64876,plain,
complement(one) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t64875,t111]) ).
cnf(t21985,plain,
meet(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t64876]) ).
cnf(t64879,plain,
converse(complement(one)) = complement(one),
inference(step,[status(thm)],[t64878,t21985]) ).
cnf(t22277,plain,
converse(complement(one)) = complement(one),
inference(orient,[status(thm)],[t64879]) ).
cnf(t65021,plain,
zero = join(meet(sk0,composition(meet(sk0,X1),complement(one))),composition(zero,meet(converse(complement(one)),composition(converse(meet(sk0,X1)),sk0)))),
inference(step,[status(thm)],[t65020,t22277]) ).
cnf(t65022,plain,
zero = join(meet(sk0,composition(meet(sk0,X1),complement(one))),zero),
inference(step,[status(thm)],[t65021,t15739]) ).
cnf(t65023,plain,
zero = meet(sk0,composition(meet(sk0,X1),complement(one))),
inference(step,[status(thm)],[t65022,t15958]) ).
cnf(t32704,plain,
meet(sk0,composition(meet(sk0,X1),complement(one))) = zero,
inference(orient,[status(thm)],[t65023]) ).
cnf(t32719,plain,
composition(meet(converse(meet(sk0,X1)),composition(complement(one),converse(sk0))),meet(sk0,composition(meet(sk0,X1),complement(one)))) = join(meet(composition(converse(meet(sk0,X1)),sk0),complement(one)),composition(meet(converse(meet(sk0,X1)),composition(complement(one),converse(sk0))),zero)),
inference(cp,[status(thm)],[t6503,t32704]) ).
cnf(t65511,plain,
composition(meet(converse(meet(sk0,X1)),composition(complement(one),converse(sk0))),zero) = join(meet(composition(converse(meet(sk0,X1)),sk0),complement(one)),composition(meet(converse(meet(sk0,X1)),composition(complement(one),converse(sk0))),zero)),
inference(step,[status(thm)],[t32719,t32704]) ).
cnf(t65512,plain,
zero = join(meet(composition(converse(meet(sk0,X1)),sk0),complement(one)),composition(meet(converse(meet(sk0,X1)),composition(complement(one),converse(sk0))),zero)),
inference(step,[status(thm)],[t65511,t15439]) ).
cnf(t65513,plain,
zero = join(meet(complement(one),composition(converse(meet(sk0,X1)),sk0)),composition(meet(converse(meet(sk0,X1)),composition(complement(one),converse(sk0))),zero)),
inference(step,[status(thm)],[t65512,t111]) ).
cnf(t65514,plain,
zero = join(meet(complement(one),composition(converse(meet(sk0,X1)),sk0)),zero),
inference(step,[status(thm)],[t65513,t15439]) ).
cnf(t65515,plain,
zero = meet(complement(one),composition(converse(meet(sk0,X1)),sk0)),
inference(step,[status(thm)],[t65514,t15958]) ).
cnf(t63937,plain,
meet(complement(one),composition(converse(meet(sk0,X1)),sk0)) = zero,
inference(orient,[status(thm)],[t65515]) ).
cnf(t16960,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t16937,t43]) ).
cnf(t16974,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t16960]) ).
cnf(t47,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t46,t43]) ).
cnf(t17102,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t47]) ).
cnf(t17211,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t16974,t17102]) ).
cnf(t17861,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t17211]) ).
cnf(t18671,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t17861,t18608]) ).
cnf(t19727,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t18671]) ).
cnf(t19728,plain,
meet(X1,X2) = meet(join(X2,X3),meet(X1,X2)),
inference(cp,[status(thm)],[t19727,t111]) ).
cnf(t20669,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(orient,[status(thm)],[t19728]) ).
cnf(t22922,plain,
meet(sk0,complement(composition(sk0,complement(one)))) = meet(join(complement(composition(sk0,complement(one))),X1),sk0),
inference(cp,[status(thm)],[t20669,t22919]) ).
cnf(t65193,plain,
sk0 = meet(join(complement(composition(sk0,complement(one))),X1),sk0),
inference(step,[status(thm)],[t22922,t22919]) ).
cnf(t65194,plain,
sk0 = meet(sk0,join(complement(composition(sk0,complement(one))),X1)),
inference(step,[status(thm)],[t65193,t111]) ).
cnf(t49094,plain,
meet(sk0,join(complement(composition(sk0,complement(one))),X1)) = sk0,
inference(orient,[status(thm)],[t65194]) ).
cnf(t63943,plain,
zero = meet(complement(one),composition(converse(sk0),sk0)),
inference(cp,[status(thm)],[t63937,t49094]) ).
cnf(t64040,plain,
meet(complement(one),composition(converse(sk0),sk0)) = zero,
inference(orient,[status(thm)],[t63943]) ).
cnf(t64042,plain,
join(complement(complement(one)),composition(converse(sk0),sk0)) = join(complement(complement(one)),zero),
inference(cp,[status(thm)],[t23573,t64040]) ).
cnf(t65516,plain,
join(one,composition(converse(sk0),sk0)) = join(complement(complement(one)),zero),
inference(step,[status(thm)],[t64042,t16009]) ).
cnf(t65517,plain,
join(one,composition(converse(sk0),sk0)) = complement(complement(one)),
inference(step,[status(thm)],[t65516,t15958]) ).
cnf(t65518,plain,
join(one,composition(converse(sk0),sk0)) = one,
inference(step,[status(thm)],[t65517,t16009]) ).
cnf(t64062,plain,
join(one,composition(converse(sk0),sk0)) = one,
inference(orient,[status(thm)],[t65518]) ).
cnf(c17,plain,
join(composition(converse(sk0),sk0),one) != one,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
join(composition(converse(sk0),sk0),one) != one,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
join(one,composition(converse(sk0),sk0)) != one,
inference(rw,[status(thm)],[goal_0,t43]) ).
cnf(g0_1,plain,
one != one,
inference(rw,[status(thm)],[g0_0,t64062]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL042+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 07:30:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 27.12/3.95 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.12/3.95 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------