%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL033+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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:35:55 PM UTC 2026
% Result : Theorem 216.09s 31.87s
% Output : Proof 216.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 96
% Number of leaves : 14
% Syntax : Number of formulae : 439 ( 435 unt; 0 def)
% Number of atoms : 443 ( 442 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 6 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 623 ( 95 sgn 81 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(t6,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t91,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
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]) ).
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(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t48,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t563912,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t48]) ).
cnf(t59,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t563912]) ).
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(t7,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t27,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
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(t2,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t29,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t162,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t29]) ).
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(t163,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t162,t17]) ).
cnf(t563917,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t163,t21]) ).
cnf(t175,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t563917]) ).
cnf(t176,plain,
one = converse(one),
inference(cp,[status(thm)],[t175,t17]) ).
cnf(t185,plain,
converse(one) = one,
inference(orient,[status(thm)],[t176]) ).
cnf(t563918,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t175,t185]) ).
cnf(t195,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t563918]) ).
cnf(t196,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t195]) ).
cnf(t199,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t59,t196]) ).
cnf(t563920,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t199,t185]) ).
cnf(t563921,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t563920,t196]) ).
cnf(t225,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t563921]) ).
cnf(t235,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t91,t225]) ).
cnf(t242,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t235]) ).
cnf(t252,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t91,t242]) ).
cnf(t1333,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t252]) ).
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(t50,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t18]) ).
cnf(t564531,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t50,t48]) ).
cnf(t564532,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t564531,t91]) ).
cnf(t564533,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t564532,t48]) ).
cnf(t19946,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t564533]) ).
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(t4,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t98,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t19947,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t19946,t98]) ).
cnf(t564534,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t19947,t91]) ).
cnf(t20167,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t564534]) ).
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(t51,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
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(t3,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t56,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t92,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t91,t56]) ).
cnf(t563913,plain,
zero = complement(top),
inference(step,[status(thm)],[t92,t98]) ).
cnf(t103,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t563913]) ).
cnf(t229,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t225,t103]) ).
cnf(t563922,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t229,t103]) ).
cnf(t563923,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t563922,t103]) ).
cnf(t236,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t563923]) ).
cnf(t237,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t51,t236]) ).
cnf(t255,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t237]) ).
cnf(t20177,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t255,t20167]) ).
cnf(t564561,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t20177,t20167]) ).
cnf(t20280,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t564561]) ).
cnf(t564574,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t20167,t20280]) ).
cnf(t20395,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t564574]) ).
cnf(t20487,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t20395]) ).
cnf(t564623,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1333,t20487]) ).
cnf(t20527,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t564623]) ).
cnf(t21385,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t20527]) ).
cnf(t226,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t225,t91]) ).
cnf(t563949,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t226,t91]) ).
cnf(t563950,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t563949,t91]) ).
cnf(t552,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t563950]) ).
cnf(t93,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t91,t48]) ).
cnf(t563915,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t93,t91]) ).
cnf(t112,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t563915]) ).
cnf(t553,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t552,t112]) ).
cnf(t585,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t553]) ).
cnf(t20488,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t585,t20487]) ).
cnf(t564636,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t20488,t20487]) ).
cnf(t564637,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t564636,t20487]) ).
cnf(t20552,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t564637]) ).
cnf(t20556,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t51,t20552]) ).
cnf(t20929,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t20556]) ).
cnf(t20951,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t20929,t19946]) ).
cnf(t564687,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t20951,t19946]) ).
cnf(t564688,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t564687,t48]) ).
cnf(t20965,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t564688]) ).
cnf(t20967,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t20965,t112]) ).
cnf(t21006,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t20967]) ).
cnf(t21013,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t51,t21006]) ).
cnf(t26619,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t21013]) ).
cnf(t564710,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t19946,t21385]) ).
cnf(t21508,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t564710]) ).
cnf(t31556,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t21508]) ).
cnf(t31622,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t26619,t31556]) ).
cnf(t31781,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t31622]) ).
cnf(t564616,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t242,t20487]) ).
cnf(t20520,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t564616]) ).
cnf(t20605,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t20520]) ).
cnf(t21445,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t21385,t20605]) ).
cnf(t21762,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t21445]) ).
cnf(t31798,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t31781,t21762]) ).
cnf(t33042,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t31798]) ).
cnf(t33192,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t21385,t33042]) ).
cnf(t564977,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t33192,t20605]) ).
cnf(t564978,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t564977,t91]) ).
cnf(t33216,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t564978]) ).
cnf(t33235,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t33216,t48]) ).
cnf(t33278,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t33235]) ).
cnf(t20973,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t51,t20965]) ).
cnf(t26029,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t20973]) ).
cnf(t33293,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,join(complement(X1),X3)),
inference(cp,[status(thm)],[t33278,t26029]) ).
cnf(t565584,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,X3),
inference(step,[status(thm)],[t33293,t33278]) ).
cnf(t65936,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t565584]) ).
cnf(t21769,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t21006,t21762]) ).
cnf(t106,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t91,t103]) ).
cnf(t129,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t106]) ).
cnf(t131,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t129,t91]) ).
cnf(t7199,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t131]) ).
cnf(t564564,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t7199,t20280]) ).
cnf(t20283,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t564564]) ).
cnf(t564594,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t129,t20280]) ).
cnf(t20411,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t564594]) ).
cnf(t564646,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t20411,t20605]) ).
cnf(t20661,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t564646]) ).
cnf(t564649,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t20283,t20661]) ).
cnf(t20683,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t564649]) ).
cnf(t21694,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t20683]) ).
cnf(t564716,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t21769,t21694]) ).
cnf(t21910,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t564716]) ).
cnf(t21957,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t20605,t21910]) ).
cnf(t564717,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t21957,t20605]) ).
cnf(t22013,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t564717]) ).
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(t8,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t66,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t69,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t66,t21]) ).
cnf(t288,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t69]) ).
cnf(t58,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t51,t56]) ).
cnf(t356,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t58]) ).
cnf(t250,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t56,t242]) ).
cnf(t266,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t250]) ).
cnf(t360,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t356,t266]) ).
cnf(t362,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t356,t225]) ).
cnf(t563929,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t362,t56]) ).
cnf(t374,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t563929]) ).
cnf(t375,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t374,t91]) ).
cnf(t382,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t375]) ).
cnf(t563931,plain,
top = join(X1,top),
inference(step,[status(thm)],[t360,t382]) ).
cnf(t387,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t563931]) ).
cnf(t388,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t387,t48]) ).
cnf(t394,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t388]) ).
cnf(t68,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t66,t21]) ).
cnf(t271,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t68]) ).
cnf(t273,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t271,t56]) ).
cnf(t307,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t273]) ).
cnf(t397,plain,
top = converse(top),
inference(cp,[status(thm)],[t394,t307]) ).
cnf(t401,plain,
converse(top) = top,
inference(orient,[status(thm)],[t397]) ).
cnf(t406,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t27,t401]) ).
cnf(t413,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t406]) ).
cnf(t422,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t288,t413]) ).
cnf(t8103,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t422]) ).
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(t30,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t24,t27]) ).
cnf(t1618,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t30]) ).
cnf(t8104,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t8103,t1618]) ).
cnf(t564289,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t8104,t21]) ).
cnf(t28,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t152,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t28]) ).
cnf(t564290,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t564289,t152]) ).
cnf(t564291,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t564290,t271]) ).
cnf(t564292,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t564291,t401]) ).
cnf(t564293,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t564292,t387]) ).
cnf(t8178,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t564293]) ).
cnf(t8181,plain,
composition(X1,top) = join(composition(X1,top),composition(X1,X2)),
inference(cp,[status(thm)],[t8178,t48]) ).
cnf(t9701,plain,
join(composition(X1,top),composition(X1,X2)) = composition(X1,top),
inference(orient,[status(thm)],[t8181]) ).
fof(f16,conjecture,
! [X0,X1,X2] :
( composition(X0,top) = X0
=> composition(meet(X0,X1),X2) = meet(X0,composition(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( composition(X0,top) = X0
=> composition(meet(X0,X1),X2) = meet(X0,composition(X1,X2)) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1,X2] :
( composition(meet(X0,X1),X2) != meet(X0,composition(X1,X2))
& composition(X0,top) = X0 ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( composition(meet(sk0,sk1),sk2) != meet(sk0,composition(sk1,sk2))
& composition(sk0,top) = sk0 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f16_nnf]) ).
cnf(c16,plain,
composition(sk0,top) = sk0,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t1,plain,
composition(sk0,top) = sk0,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t43,plain,
composition(sk0,top) = sk0,
inference(orient,[status(thm)],[t1]) ).
cnf(t62,plain,
complement(top) = join(complement(top),composition(converse(sk0),complement(sk0))),
inference(cp,[status(thm)],[t59,t43]) ).
cnf(t563990,plain,
zero = join(complement(top),composition(converse(sk0),complement(sk0))),
inference(step,[status(thm)],[t62,t103]) ).
cnf(t563991,plain,
zero = join(zero,composition(converse(sk0),complement(sk0))),
inference(step,[status(thm)],[t563990,t103]) ).
cnf(t1438,plain,
join(zero,composition(converse(sk0),complement(sk0))) = zero,
inference(orient,[status(thm)],[t563991]) ).
cnf(t564581,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(step,[status(thm)],[t1438,t20280]) ).
cnf(t20400,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(rw,[status(thm)],[t564581]) ).
cnf(t20844,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(orient,[status(thm)],[t20400]) ).
cnf(t20855,plain,
composition(converse(complement(sk0)),sk0) = converse(zero),
inference(cp,[status(thm)],[t162,t20844]) ).
cnf(t563938,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t307,t401]) ).
cnf(t404,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t563938]) ).
cnf(t20315,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t20280,t404]) ).
cnf(t20700,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t20315]) ).
cnf(t20701,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t21,t20700]) ).
cnf(t564658,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t20701,t401]) ).
cnf(t20770,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t564658]) ).
cnf(t20771,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t20605,t20770]) ).
cnf(t564659,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t20771,t103]) ).
cnf(t20786,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t564659]) ).
cnf(t564683,plain,
composition(converse(complement(sk0)),sk0) = zero,
inference(step,[status(thm)],[t20855,t20786]) ).
cnf(t20873,plain,
composition(converse(complement(sk0)),sk0) = zero,
inference(orient,[status(thm)],[t564683]) ).
cnf(t20884,plain,
complement(sk0) = join(complement(sk0),composition(converse(converse(complement(sk0))),complement(zero))),
inference(cp,[status(thm)],[t59,t20873]) ).
cnf(t564684,plain,
complement(sk0) = join(complement(sk0),composition(complement(sk0),complement(zero))),
inference(step,[status(thm)],[t20884,t21]) ).
cnf(t563934,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t356,t394]) ).
cnf(t395,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t563934]) ).
cnf(t8182,plain,
composition(X1,top) = join(X1,composition(X1,top)),
inference(cp,[status(thm)],[t8178,t17]) ).
cnf(t8278,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t8182]) ).
cnf(t8310,plain,
join(X1,converse(composition(converse(X1),top))) = converse(composition(converse(X1),top)),
inference(cp,[status(thm)],[t271,t8278]) ).
cnf(t564297,plain,
join(X1,composition(converse(top),X1)) = converse(composition(converse(X1),top)),
inference(step,[status(thm)],[t8310,t162]) ).
cnf(t564298,plain,
join(X1,composition(top,X1)) = converse(composition(converse(X1),top)),
inference(step,[status(thm)],[t564297,t401]) ).
cnf(t564299,plain,
join(X1,composition(top,X1)) = composition(converse(top),X1),
inference(step,[status(thm)],[t564298,t162]) ).
cnf(t564300,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(step,[status(thm)],[t564299,t401]) ).
cnf(t8367,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t564300]) ).
cnf(t8388,plain,
top = join(X1,composition(top,complement(X1))),
inference(cp,[status(thm)],[t395,t8367]) ).
cnf(t8572,plain,
join(X1,composition(top,complement(X1))) = top,
inference(orient,[status(thm)],[t8388]) ).
cnf(t20306,plain,
composition(top,complement(zero)) = top,
inference(cp,[status(thm)],[t20280,t8572]) ).
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(t33,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(t70,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t51,t66]) ).
cnf(t3319,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t70]) ).
cnf(t365,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t356,t48]) ).
cnf(t563940,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t365,t394]) ).
cnf(t457,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t563940]) ).
cnf(t3323,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t3319,t457]) ).
cnf(t564112,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t3323,t48]) ).
cnf(t3381,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t564112]) ).
cnf(t3422,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t3381,t66]) ).
cnf(t564113,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t3422,t21]) ).
cnf(t564114,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t564113,t21]) ).
cnf(t3436,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t564114]) ).
cnf(t3473,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t3436,t48]) ).
cnf(t3477,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t3473]) ).
cnf(t61,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t59,t17]) ).
cnf(t1409,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t61]) ).
cnf(t1420,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1409,t21]) ).
cnf(t1456,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1420]) ).
cnf(t3489,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t3477,t1456]) ).
cnf(t564125,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t3489,t48]) ).
cnf(t3940,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t564125]) ).
cnf(t3956,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t91,t3940]) ).
cnf(t564126,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t3956,t103]) ).
cnf(t3962,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t564126]) ).
cnf(t3984,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)],[t33,t3962]) ).
cnf(t564127,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)],[t3984,t21]) ).
cnf(t564128,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)],[t564127,t185]) ).
cnf(t564129,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)],[t564128,t17]) ).
cnf(t564130,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)],[t564129,t98]) ).
cnf(t564131,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)],[t564130,t3962]) ).
cnf(t564132,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)],[t564131,t17]) ).
cnf(t564133,plain,
composition(zero,zero) = join(meet(X1,complement(X1)),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t564132,t21]) ).
cnf(t564134,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t564133,t98]) ).
cnf(t44,plain,
composition(join(sk0,X1),top) = join(sk0,composition(X1,top)),
inference(cp,[status(thm)],[t24,t43]) ).
cnf(t324,plain,
composition(join(sk0,X1),top) = join(sk0,composition(X1,top)),
inference(orient,[status(thm)],[t44]) ).
cnf(t414,plain,
composition(top,converse(join(sk0,X1))) = converse(join(sk0,composition(X1,top))),
inference(cp,[status(thm)],[t413,t324]) ).
cnf(t1168,plain,
converse(join(sk0,composition(X1,top))) = composition(top,converse(join(sk0,X1))),
inference(orient,[status(thm)],[t414]) ).
cnf(t1169,plain,
composition(top,converse(join(sk0,one))) = converse(join(sk0,top)),
inference(cp,[status(thm)],[t1168,t196]) ).
cnf(t187,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t66,t185]) ).
cnf(t563919,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t187,t48]) ).
cnf(t213,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t563919]) ).
cnf(t563985,plain,
composition(top,join(one,converse(sk0))) = converse(join(sk0,top)),
inference(step,[status(thm)],[t1169,t213]) ).
cnf(t563986,plain,
composition(top,join(one,converse(sk0))) = converse(top),
inference(step,[status(thm)],[t563985,t387]) ).
cnf(t563987,plain,
composition(top,join(one,converse(sk0))) = top,
inference(step,[status(thm)],[t563986,t401]) ).
cnf(t1188,plain,
composition(top,join(one,converse(sk0))) = top,
inference(orient,[status(thm)],[t563987]) ).
cnf(t1622,plain,
composition(join(converse(join(one,converse(sk0))),X1),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(cp,[status(thm)],[t1618,t1188]) ).
cnf(t186,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t66,t185]) ).
cnf(t202,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t186]) ).
cnf(t564002,plain,
composition(join(join(one,converse(converse(sk0))),X1),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t1622,t202]) ).
cnf(t564003,plain,
composition(join(one,join(converse(converse(sk0)),X1)),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t564002,t51]) ).
cnf(t564004,plain,
composition(join(one,join(sk0,X1)),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t564003,t21]) ).
cnf(t564005,plain,
composition(join(one,join(sk0,X1)),top) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t564004,t401]) ).
cnf(t564006,plain,
composition(join(one,join(sk0,X1)),top) = join(top,composition(X1,converse(top))),
inference(step,[status(thm)],[t564005,t401]) ).
cnf(t564007,plain,
composition(join(one,join(sk0,X1)),top) = top,
inference(step,[status(thm)],[t564006,t394]) ).
cnf(t1657,plain,
composition(join(one,join(sk0,X1)),top) = top,
inference(orient,[status(thm)],[t564007]) ).
cnf(t464,plain,
join(one,converse(join(X1,complement(one)))) = converse(top),
inference(cp,[status(thm)],[t202,t457]) ).
cnf(t563941,plain,
join(one,converse(join(X1,complement(one)))) = top,
inference(step,[status(thm)],[t464,t401]) ).
cnf(t467,plain,
join(one,converse(join(X1,complement(one)))) = top,
inference(orient,[status(thm)],[t563941]) ).
cnf(t468,plain,
top = join(one,join(X1,converse(complement(one)))),
inference(cp,[status(thm)],[t467,t271]) ).
cnf(t472,plain,
join(one,join(X1,converse(complement(one)))) = top,
inference(orient,[status(thm)],[t468]) ).
cnf(t1658,plain,
top = composition(top,top),
inference(cp,[status(thm)],[t1657,t472]) ).
cnf(t1699,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t1658]) ).
cnf(t1706,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t59,t1699]) ).
cnf(t564010,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t1706,t103]) ).
cnf(t564011,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t564010,t103]) ).
cnf(t564012,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t564011,t401]) ).
cnf(t564013,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t564012,t103]) ).
cnf(t1708,plain,
join(zero,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t564013]) ).
cnf(t1711,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(cp,[status(thm)],[t51,t1708]) ).
cnf(t1751,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(orient,[status(thm)],[t1711]) ).
cnf(t1753,plain,
join(zero,composition(X1,zero)) = join(zero,composition(join(top,X1),zero)),
inference(cp,[status(thm)],[t1751,t24]) ).
cnf(t564016,plain,
join(zero,composition(X1,zero)) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t1753,t394]) ).
cnf(t564017,plain,
join(zero,composition(X1,zero)) = zero,
inference(step,[status(thm)],[t564016,t1708]) ).
cnf(t1774,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t564017]) ).
cnf(t564135,plain,
composition(zero,zero) = zero,
inference(step,[status(thm)],[t564134,t1774]) ).
cnf(t3985,plain,
composition(zero,zero) = zero,
inference(orient,[status(thm)],[t564135]) ).
cnf(t3987,plain,
composition(join(zero,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t24,t3985]) ).
cnf(t564140,plain,
composition(join(zero,X1),zero) = zero,
inference(step,[status(thm)],[t3987,t1774]) ).
cnf(t4058,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t564140]) ).
cnf(t1778,plain,
join(zero,join(composition(X1,zero),X2)) = join(zero,X2),
inference(cp,[status(thm)],[t51,t1774]) ).
cnf(t1832,plain,
join(zero,join(composition(X1,zero),X2)) = join(zero,X2),
inference(orient,[status(thm)],[t1778]) ).
cnf(t1842,plain,
join(zero,converse(complement(converse(composition(X1,zero))))) = join(zero,top),
inference(cp,[status(thm)],[t1832,t404]) ).
cnf(t105,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t56,t103]) ).
cnf(t563914,plain,
top = join(zero,top),
inference(step,[status(thm)],[t105,t48]) ).
cnf(t110,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t563914]) ).
cnf(t564029,plain,
join(zero,converse(complement(converse(composition(X1,zero))))) = top,
inference(step,[status(thm)],[t1842,t110]) ).
cnf(t1918,plain,
join(zero,converse(complement(converse(composition(X1,zero))))) = top,
inference(orient,[status(thm)],[t564029]) ).
cnf(t4059,plain,
zero = composition(top,zero),
inference(cp,[status(thm)],[t4058,t1918]) ).
cnf(t4092,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t4059]) ).
cnf(t4104,plain,
complement(zero) = join(complement(zero),composition(converse(top),complement(zero))),
inference(cp,[status(thm)],[t59,t4092]) ).
cnf(t564177,plain,
complement(zero) = join(complement(zero),composition(top,complement(zero))),
inference(step,[status(thm)],[t4104,t401]) ).
cnf(t4703,plain,
join(complement(zero),composition(top,complement(zero))) = complement(zero),
inference(orient,[status(thm)],[t564177]) ).
cnf(t564301,plain,
composition(top,complement(zero)) = complement(zero),
inference(step,[status(thm)],[t4703,t8367]) ).
cnf(t8411,plain,
composition(top,complement(zero)) = complement(zero),
inference(rw,[status(thm)],[t564301]) ).
cnf(t8412,plain,
composition(top,complement(zero)) = complement(zero),
inference(orient,[status(thm)],[t8411]) ).
cnf(t564605,plain,
complement(zero) = top,
inference(step,[status(thm)],[t20306,t8412]) ).
cnf(t20422,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t564605]) ).
cnf(t564685,plain,
complement(sk0) = join(complement(sk0),composition(complement(sk0),top)),
inference(step,[status(thm)],[t564684,t20422]) ).
cnf(t564686,plain,
complement(sk0) = composition(complement(sk0),top),
inference(step,[status(thm)],[t564685,t8278]) ).
cnf(t20897,plain,
composition(complement(sk0),top) = complement(sk0),
inference(orient,[status(thm)],[t564686]) ).
cnf(t20898,plain,
composition(complement(sk0),top) = join(complement(sk0),composition(complement(sk0),X1)),
inference(cp,[status(thm)],[t9701,t20897]) ).
cnf(t564772,plain,
complement(sk0) = join(complement(sk0),composition(complement(sk0),X1)),
inference(step,[status(thm)],[t20898,t20897]) ).
cnf(t24418,plain,
join(complement(sk0),composition(complement(sk0),X1)) = complement(sk0),
inference(orient,[status(thm)],[t564772]) ).
cnf(t24419,plain,
composition(complement(sk0),X1) = meet(composition(complement(sk0),X1),complement(sk0)),
inference(cp,[status(thm)],[t22013,t24418]) ).
cnf(t565264,plain,
composition(complement(sk0),X1) = meet(complement(sk0),composition(complement(sk0),X1)),
inference(step,[status(thm)],[t24419,t112]) ).
cnf(t49650,plain,
meet(complement(sk0),composition(complement(sk0),X1)) = composition(complement(sk0),X1),
inference(orient,[status(thm)],[t565264]) ).
cnf(t65994,plain,
meet(sk0,X1) = meet(sk0,join(composition(complement(sk0),X2),X1)),
inference(cp,[status(thm)],[t65936,t49650]) ).
cnf(t82125,plain,
meet(sk0,join(composition(complement(sk0),X1),X2)) = meet(sk0,X2),
inference(orient,[status(thm)],[t65994]) ).
cnf(t82127,plain,
meet(sk0,composition(X1,X2)) = meet(sk0,composition(join(complement(sk0),X1),X2)),
inference(cp,[status(thm)],[t82125,t24]) ).
cnf(t562761,plain,
meet(sk0,composition(join(complement(sk0),X1),X2)) = meet(sk0,composition(X1,X2)),
inference(orient,[status(thm)],[t82127]) ).
cnf(t31799,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t31781,t112]) ).
cnf(t32360,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t31799]) ).
cnf(t32386,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t32360,t20605]) ).
cnf(t33597,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t32386]) ).
cnf(t31817,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t26619,t31781]) ).
cnf(t565557,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(step,[status(thm)],[t31817,t26619]) ).
cnf(t64538,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t565557]) ).
cnf(t251,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t91,t242]) ).
cnf(t1283,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t251]) ).
cnf(t564624,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t1283,t20487]) ).
cnf(t20528,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t564624]) ).
cnf(t21620,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t20528]) ).
cnf(t21633,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t20605,t21620]) ).
cnf(t21844,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t21633]) ).
cnf(t64551,plain,
join(X1,X2) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t64538,t21844]) ).
cnf(t71383,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t64551]) ).
cnf(t71446,plain,
meet(X1,meet(X2,join(X3,complement(complement(X1))))) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t33278,t71383]) ).
cnf(t565695,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t71446,t20605]) ).
cnf(t565696,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(step,[status(thm)],[t565695,t33278]) ).
cnf(t71489,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t565696]) ).
cnf(t71516,plain,
meet(X1,X2) = meet(X1,meet(join(X3,X1),X2)),
inference(cp,[status(thm)],[t71489,t112]) ).
cnf(t71849,plain,
meet(X1,meet(join(X2,X1),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t71516]) ).
cnf(t72053,plain,
meet(X1,X2) = meet(X1,meet(join(X1,X3),X2)),
inference(cp,[status(thm)],[t71849,t48]) ).
cnf(t72747,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t72053]) ).
cnf(t72825,plain,
meet(X1,X2) = meet(X1,meet(composition(X1,top),X2)),
inference(cp,[status(thm)],[t72747,t8278]) ).
cnf(t73281,plain,
meet(X1,meet(composition(X1,top),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t72825]) ).
cnf(t73353,plain,
join(complement(X1),meet(composition(X1,top),X2)) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t33597,t73281]) ).
cnf(t568187,plain,
join(complement(X1),meet(composition(X1,top),X2)) = join(complement(X1),X2),
inference(step,[status(thm)],[t73353,t33597]) ).
cnf(t317345,plain,
join(complement(X1),meet(composition(X1,top),X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t568187]) ).
cnf(t562839,plain,
meet(sk0,composition(meet(composition(sk0,top),X1),X2)) = meet(sk0,composition(join(complement(sk0),X1),X2)),
inference(cp,[status(thm)],[t562761,t317345]) ).
cnf(t569172,plain,
meet(sk0,composition(meet(sk0,X1),X2)) = meet(sk0,composition(join(complement(sk0),X1),X2)),
inference(step,[status(thm)],[t562839,t43]) ).
cnf(t416,plain,
composition(top,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t413,t43]) ).
cnf(t430,plain,
composition(top,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t416]) ).
cnf(t431,plain,
composition(join(top,X1),converse(sk0)) = join(converse(sk0),composition(X1,converse(sk0))),
inference(cp,[status(thm)],[t24,t430]) ).
cnf(t563943,plain,
composition(top,converse(sk0)) = join(converse(sk0),composition(X1,converse(sk0))),
inference(step,[status(thm)],[t431,t394]) ).
cnf(t563944,plain,
converse(sk0) = join(converse(sk0),composition(X1,converse(sk0))),
inference(step,[status(thm)],[t563943,t430]) ).
cnf(t512,plain,
join(converse(sk0),composition(X1,converse(sk0))) = converse(sk0),
inference(orient,[status(thm)],[t563944]) ).
cnf(t518,plain,
join(sk0,converse(composition(X1,converse(sk0)))) = converse(converse(sk0)),
inference(cp,[status(thm)],[t271,t512]) ).
cnf(t563947,plain,
join(sk0,composition(sk0,converse(X1))) = converse(converse(sk0)),
inference(step,[status(thm)],[t518,t152]) ).
cnf(t563948,plain,
join(sk0,composition(sk0,converse(X1))) = sk0,
inference(step,[status(thm)],[t563947,t21]) ).
cnf(t539,plain,
join(sk0,composition(sk0,converse(X1))) = sk0,
inference(orient,[status(thm)],[t563948]) ).
cnf(t545,plain,
sk0 = join(sk0,composition(sk0,X1)),
inference(cp,[status(thm)],[t539,t21]) ).
cnf(t550,plain,
join(sk0,composition(sk0,X1)) = sk0,
inference(orient,[status(thm)],[t545]) ).
cnf(t551,plain,
join(sk0,join(composition(sk0,X1),X2)) = join(sk0,X2),
inference(cp,[status(thm)],[t51,t550]) ).
cnf(t573,plain,
join(sk0,join(composition(sk0,X1),X2)) = join(sk0,X2),
inference(orient,[status(thm)],[t551]) ).
cnf(t574,plain,
join(sk0,composition(X1,X2)) = join(sk0,composition(join(sk0,X1),X2)),
inference(cp,[status(thm)],[t573,t24]) ).
cnf(t2188,plain,
join(sk0,composition(join(sk0,X1),X2)) = join(sk0,composition(X1,X2)),
inference(orient,[status(thm)],[t574]) ).
cnf(t20991,plain,
join(sk0,composition(meet(sk0,X1),X2)) = join(sk0,composition(sk0,X2)),
inference(cp,[status(thm)],[t2188,t20965]) ).
cnf(t564738,plain,
join(sk0,composition(meet(sk0,X1),X2)) = sk0,
inference(step,[status(thm)],[t20991,t550]) ).
cnf(t23033,plain,
join(sk0,composition(meet(sk0,X1),X2)) = sk0,
inference(orient,[status(thm)],[t564738]) ).
cnf(t23036,plain,
composition(meet(sk0,X1),X2) = meet(composition(meet(sk0,X1),X2),sk0),
inference(cp,[status(thm)],[t22013,t23033]) ).
cnf(t565298,plain,
composition(meet(sk0,X1),X2) = meet(sk0,composition(meet(sk0,X1),X2)),
inference(step,[status(thm)],[t23036,t112]) ).
cnf(t51991,plain,
meet(sk0,composition(meet(sk0,X1),X2)) = composition(meet(sk0,X1),X2),
inference(orient,[status(thm)],[t565298]) ).
cnf(t569173,plain,
composition(meet(sk0,X1),X2) = meet(sk0,composition(join(complement(sk0),X1),X2)),
inference(step,[status(thm)],[t569172,t51991]) ).
cnf(t569174,plain,
composition(meet(sk0,X1),X2) = meet(sk0,composition(X1,X2)),
inference(step,[status(thm)],[t569173,t562761]) ).
cnf(t563104,plain,
composition(meet(sk0,X1),X2) = meet(sk0,composition(X1,X2)),
inference(orient,[status(thm)],[t569174]) ).
cnf(c17,plain,
composition(meet(sk0,sk1),sk2) != meet(sk0,composition(sk1,sk2)),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
meet(sk0,composition(sk1,sk2)) != composition(meet(sk0,sk1),sk2),
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
meet(sk0,composition(sk1,sk2)) != meet(sk0,composition(sk1,sk2)),
inference(rw,[status(thm)],[goal_0,t563104]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL033+3 : 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.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 07:31:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 216.09/31.87 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 216.09/31.87 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------