%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL026+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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:34:52 PM UTC 2026
% Result : Theorem 31.07s 9.91s
% Output : Proof 31.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 178
% Number of leaves : 15
% Syntax : Number of formulae : 607 ( 603 unt; 0 def)
% Number of atoms : 611 ( 610 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 : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 804 ( 130 sgn 88 !; 2 ?)
% 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(t85,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
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(t43,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t87,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t85,t43]) ).
cnf(t93054,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t87,t85]) ).
cnf(t106,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t93054]) ).
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(t93051,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)],[t93051]) ).
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(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(t29,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t169,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(t170,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t169,t17]) ).
cnf(t93058,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t170,t21]) ).
cnf(t182,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t93058]) ).
cnf(t183,plain,
one = converse(one),
inference(cp,[status(thm)],[t182,t17]) ).
cnf(t192,plain,
converse(one) = one,
inference(orient,[status(thm)],[t183]) ).
cnf(t93059,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t182,t192]) ).
cnf(t202,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t93059]) ).
cnf(t203,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t202]) ).
cnf(t206,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t54,t203]) ).
cnf(t93062,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t206,t192]) ).
cnf(t93063,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t93062,t203]) ).
cnf(t236,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t93063]) ).
cnf(t237,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t236,t85]) ).
cnf(t93101,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t237,t85]) ).
cnf(t93102,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t93101,t85]) ).
cnf(t544,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t93102]) ).
cnf(t545,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t544,t106]) ).
cnf(t565,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t545]) ).
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(t93674,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t45,t43]) ).
cnf(t93675,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t93674,t85]) ).
cnf(t93676,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t93675,t43]) ).
cnf(t14257,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t93676]) ).
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(t92,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t14258,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t14257,t92]) ).
cnf(t93785,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t14258,t85]) ).
cnf(t14877,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t93785]) ).
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(t51,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t86,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t85,t51]) ).
cnf(t93052,plain,
zero = complement(top),
inference(step,[status(thm)],[t86,t92]) ).
cnf(t97,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t93052]) ).
cnf(t240,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t236,t97]) ).
cnf(t93064,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t240,t97]) ).
cnf(t93065,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t93064,t97]) ).
cnf(t247,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t93065]) ).
cnf(t248,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t46,t247]) ).
cnf(t269,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t248]) ).
cnf(t14882,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t269,t14877]) ).
cnf(t93787,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t14882,t14877]) ).
cnf(t14893,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t93787]) ).
cnf(t93792,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t14877,t14893]) ).
cnf(t14928,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t93792]) ).
cnf(t14961,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t14928]) ).
cnf(t14962,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t565,t14961]) ).
cnf(t93832,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t14962,t14961]) ).
cnf(t93833,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t93832,t14961]) ).
cnf(t15026,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t93833]) ).
cnf(t15032,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t46,t15026]) ).
cnf(t15073,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t15032]) ).
cnf(t15092,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t15073,t14257]) ).
cnf(t93835,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t15092,t14257]) ).
cnf(t93836,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t93835,t43]) ).
cnf(t15101,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t93836]) ).
cnf(t15103,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t15101,t106]) ).
cnf(t15129,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t15103]) ).
cnf(t15136,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t46,t15129]) ).
cnf(t19528,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t15136]) ).
cnf(t246,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t85,t236]) ).
cnf(t256,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t246]) ).
cnf(t266,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t85,t256]) ).
cnf(t1388,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t266]) ).
cnf(t93816,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1388,t14961]) ).
cnf(t14992,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t93816]) ).
cnf(t15554,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t14992]) ).
cnf(t93852,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t14257,t15554]) ).
cnf(t15642,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t93852]) ).
cnf(t26034,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t15642]) ).
cnf(t26111,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t19528,t26034]) ).
cnf(t26302,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t26111]) ).
cnf(t26322,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t26302,t106]) ).
cnf(t26876,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t26322]) ).
cnf(t100,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t85,t97]) ).
cnf(t123,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t100]) ).
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(t60,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t63,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t60,t21]) ).
cnf(t311,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t63]) ).
cnf(t53,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t46,t51]) ).
cnf(t353,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t53]) ).
cnf(t264,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t51,t256]) ).
cnf(t280,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t264]) ).
cnf(t358,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t353,t280]) ).
cnf(t360,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t353,t236]) ).
cnf(t93073,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t360,t51]) ).
cnf(t373,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t93073]) ).
cnf(t374,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t373,t85]) ).
cnf(t386,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t374]) ).
cnf(t93075,plain,
top = join(X1,top),
inference(step,[status(thm)],[t358,t386]) ).
cnf(t391,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t93075]) ).
cnf(t392,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t391,t43]) ).
cnf(t397,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t392]) ).
cnf(t62,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t60,t21]) ).
cnf(t294,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t62]) ).
cnf(t296,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t294,t51]) ).
cnf(t335,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t296]) ).
cnf(t402,plain,
top = converse(top),
inference(cp,[status(thm)],[t397,t335]) ).
cnf(t405,plain,
converse(top) = top,
inference(orient,[status(thm)],[t402]) ).
cnf(t410,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t27,t405]) ).
cnf(t417,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t410]) ).
cnf(t423,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t311,t417]) ).
cnf(t12010,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t423]) ).
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(t1261,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t30]) ).
cnf(t12012,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t12010,t1261]) ).
cnf(t93623,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t12012,t21]) ).
cnf(t28,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t159,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t28]) ).
cnf(t93624,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t93623,t159]) ).
cnf(t93625,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t93624,t294]) ).
cnf(t93626,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t93625,t405]) ).
cnf(t93627,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t93626,t391]) ).
cnf(t12092,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t93627]) ).
cnf(t411,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t27,t405]) ).
cnf(t431,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t411]) ).
cnf(t419,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t60,t417]) ).
cnf(t5391,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t419]) ).
cnf(t5404,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t5391,t405]) ).
cnf(t5439,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t5404]) ).
cnf(t5443,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t5439,t24]) ).
cnf(t93388,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t5443,t417]) ).
cnf(t93389,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t93388,t417]) ).
cnf(t93390,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t93389,t397]) ).
cnf(t93391,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t93390,t405]) ).
cnf(t5565,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t93391]) ).
cnf(t5581,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t5565,t192]) ).
cnf(t93392,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t5581,t17]) ).
cnf(t93393,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t93392,t391]) ).
cnf(t5594,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t93393]) ).
cnf(t5599,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t5594]) ).
cnf(t93401,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t5599,t97]) ).
cnf(t93402,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t93401,t97]) ).
cnf(t93403,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t93402,t405]) ).
cnf(t93404,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t93403,t97]) ).
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(t64,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t46,t60]) ).
cnf(t2656,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t64]) ).
cnf(t363,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t353,t43]) ).
cnf(t93091,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t363,t397]) ).
cnf(t456,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t93091]) ).
cnf(t2661,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t2656,t456]) ).
cnf(t93282,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t2661,t43]) ).
cnf(t2725,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t93282]) ).
cnf(t2765,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t2725,t60]) ).
cnf(t93283,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t2765,t21]) ).
cnf(t93284,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t93283,t21]) ).
cnf(t2778,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t93284]) ).
cnf(t2815,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t2778,t43]) ).
cnf(t2825,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t2815]) ).
cnf(t56,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t54,t17]) ).
cnf(t1465,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t56]) ).
cnf(t1475,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1465,t21]) ).
cnf(t1493,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1475]) ).
cnf(t2836,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t2825,t1493]) ).
cnf(t93298,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t2836,t43]) ).
cnf(t3322,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t93298]) ).
cnf(t3337,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t85,t3322]) ).
cnf(t93299,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t3337,t97]) ).
cnf(t3343,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t93299]) ).
cnf(t3364,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,t3343]) ).
cnf(t93300,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)],[t3364,t21]) ).
cnf(t93301,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)],[t93300,t192]) ).
cnf(t93302,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)],[t93301,t17]) ).
cnf(t93303,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)],[t93302,t92]) ).
cnf(t93304,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)],[t93303,t3343]) ).
cnf(t93305,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)],[t93304,t17]) ).
cnf(t93306,plain,
composition(zero,zero) = join(meet(X1,complement(X1)),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t93305,t21]) ).
cnf(t93307,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t93306,t92]) ).
cnf(t93308,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),converse(one))),zero)),
inference(step,[status(thm)],[t93307,t21]) ).
cnf(t93309,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),one)),zero)),
inference(step,[status(thm)],[t93308,t192]) ).
cnf(t93310,plain,
composition(zero,zero) = join(zero,composition(meet(X1,complement(X1)),zero)),
inference(step,[status(thm)],[t93309,t17]) ).
cnf(t93311,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t93310,t92]) ).
cnf(t3365,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t93311]) ).
cnf(t3368,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t46,t3365]) ).
cnf(t3524,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t3368]) ).
cnf(t3532,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t3524,t24]) ).
cnf(t93324,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t3532,t24]) ).
cnf(t3610,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t93324]) ).
cnf(t271,plain,
join(zero,X1) = join(zero,join(X1,zero)),
inference(cp,[status(thm)],[t269,t43]) ).
cnf(t272,plain,
join(zero,join(X1,zero)) = join(zero,X1),
inference(orient,[status(thm)],[t271]) ).
cnf(t275,plain,
join(zero,join(join(X1,zero),X2)) = join(join(zero,X1),X2),
inference(cp,[status(thm)],[t46,t272]) ).
cnf(t93154,plain,
join(zero,join(X1,join(zero,X2))) = join(join(zero,X1),X2),
inference(step,[status(thm)],[t275,t46]) ).
cnf(t93155,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(step,[status(thm)],[t93154,t46]) ).
cnf(t1597,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(orient,[status(thm)],[t93155]) ).
cnf(t52,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t51,t46]) ).
cnf(t577,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t52]) ).
cnf(t606,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t577,t43]) ).
cnf(t734,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t606]) ).
cnf(t193,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t60,t192]) ).
cnf(t209,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t193]) ).
fof(f16,conjecture,
! [X0,X1] :
( join(X0,one) = one
=> meet(composition(X0,top),X1) = composition(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1] :
( join(X0,one) = one
=> meet(composition(X0,top),X1) = composition(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1] :
( meet(composition(X0,top),X1) != composition(X0,X1)
& join(X0,one) = one ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( meet(composition(sk0,top),sk1) != composition(sk0,sk1)
& join(sk0,one) = one ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f16_nnf]) ).
cnf(c16,plain,
join(sk0,one) = one,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t2,plain,
join(sk0,one) = one,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t83,plain,
join(sk0,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t84,plain,
join(sk0,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t46,t83]) ).
cnf(t118,plain,
join(sk0,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t84]) ).
cnf(t120,plain,
join(one,X1) = join(sk0,join(X1,one)),
inference(cp,[status(thm)],[t118,t43]) ).
cnf(t142,plain,
join(sk0,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t120]) ).
cnf(t356,plain,
join(top,one) = join(one,complement(sk0)),
inference(cp,[status(thm)],[t353,t142]) ).
cnf(t382,plain,
join(one,complement(sk0)) = join(top,one),
inference(orient,[status(thm)],[t356]) ).
cnf(t383,plain,
join(one,converse(complement(sk0))) = converse(join(top,one)),
inference(cp,[status(thm)],[t209,t382]) ).
cnf(t194,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t60,t192]) ).
cnf(t93060,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t194,t43]) ).
cnf(t220,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t93060]) ).
cnf(t93086,plain,
join(one,converse(complement(sk0))) = join(one,converse(top)),
inference(step,[status(thm)],[t383,t220]) ).
cnf(t93087,plain,
join(one,converse(complement(sk0))) = join(one,top),
inference(step,[status(thm)],[t93086,t405]) ).
cnf(t93088,plain,
join(one,converse(complement(sk0))) = top,
inference(step,[status(thm)],[t93087,t391]) ).
cnf(t443,plain,
join(one,converse(complement(sk0))) = top,
inference(orient,[status(thm)],[t93088]) ).
cnf(t444,plain,
join(one,join(converse(complement(sk0)),X1)) = join(top,X1),
inference(cp,[status(thm)],[t46,t443]) ).
cnf(t93092,plain,
join(one,join(converse(complement(sk0)),X1)) = top,
inference(step,[status(thm)],[t444,t397]) ).
cnf(t471,plain,
join(one,join(converse(complement(sk0)),X1)) = top,
inference(orient,[status(thm)],[t93092]) ).
cnf(t765,plain,
top = join(join(converse(complement(sk0)),X1),join(one,complement(top))),
inference(cp,[status(thm)],[t734,t471]) ).
cnf(t93203,plain,
top = join(converse(complement(sk0)),join(X1,join(one,complement(top)))),
inference(step,[status(thm)],[t765,t46]) ).
cnf(t93204,plain,
top = join(converse(complement(sk0)),join(X1,join(one,zero))),
inference(step,[status(thm)],[t93203,t97]) ).
cnf(t93205,plain,
top = join(converse(complement(sk0)),join(X1,join(zero,one))),
inference(step,[status(thm)],[t93204,t43]) ).
cnf(t2215,plain,
join(converse(complement(sk0)),join(X1,join(zero,one))) = top,
inference(orient,[status(thm)],[t93205]) ).
cnf(t2219,plain,
top = join(converse(complement(sk0)),join(join(zero,one),X1)),
inference(cp,[status(thm)],[t2215,t43]) ).
cnf(t93245,plain,
top = join(converse(complement(sk0)),join(zero,join(one,X1))),
inference(step,[status(thm)],[t2219,t46]) ).
cnf(t2464,plain,
join(converse(complement(sk0)),join(zero,join(one,X1))) = top,
inference(orient,[status(thm)],[t93245]) ).
cnf(t2468,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = join(zero,top),
inference(cp,[status(thm)],[t1597,t2464]) ).
cnf(t99,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t51,t97]) ).
cnf(t93053,plain,
top = join(zero,top),
inference(step,[status(thm)],[t99,t43]) ).
cnf(t104,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t93053]) ).
cnf(t93257,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = top,
inference(step,[status(thm)],[t2468,t104]) ).
cnf(t2519,plain,
join(zero,join(converse(complement(sk0)),join(one,X1))) = top,
inference(orient,[status(thm)],[t93257]) ).
cnf(t3613,plain,
composition(join(zero,join(converse(complement(sk0)),join(one,X1))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t3610,t2519]) ).
cnf(t93325,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t3613,t2519]) ).
cnf(t3644,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t93325]) ).
cnf(t93405,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t93404,t3644]) ).
cnf(t5611,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t93405]) ).
cnf(t5612,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t431,t5611]) ).
cnf(t5635,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t5612]) ).
cnf(t12144,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t12092,t5635]) ).
cnf(t93654,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t12144,t5635]) ).
cnf(t93655,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t93654,t43]) ).
cnf(t13339,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t93655]) ).
cnf(t3633,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t3610,t43]) ).
cnf(t3699,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t3633]) ).
cnf(t5613,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t24,t5611]) ).
cnf(t93412,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t5613,t397]) ).
cnf(t93413,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t93412,t5611]) ).
cnf(t5660,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t93413]) ).
cnf(t93416,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t3699,t5660]) ).
cnf(t5679,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t93416]) ).
cnf(t5724,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t5679]) ).
cnf(t5727,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t5724,t43]) ).
cnf(t5747,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t5727]) ).
cnf(t5749,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t24,t5747]) ).
cnf(t93439,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t5749,t46]) ).
cnf(t93440,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t93439,t5660]) ).
cnf(t5958,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t93440]) ).
cnf(t215,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t169,t209]) ).
cnf(t5136,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t215]) ).
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(t674,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t5597,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t674,t5594]) ).
cnf(t93531,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t5597,t24]) ).
cnf(t7819,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t93531]) ).
cnf(t7831,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t7819,t203]) ).
cnf(t93532,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t7831,t391]) ).
cnf(t93533,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t93532,t5594]) ).
cnf(t7860,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t93533]) ).
cnf(t7862,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t7860,t43]) ).
cnf(t7889,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t7862]) ).
cnf(t7901,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t5136,t7889]) ).
cnf(t93536,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t7901,t405]) ).
cnf(t93537,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t93536,t405]) ).
cnf(t7935,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t93537]) ).
cnf(t7936,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t7935,t43]) ).
cnf(t7956,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t7936]) ).
cnf(t7963,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t7956]) ).
cnf(t93556,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t7963,t405]) ).
cnf(t93557,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t93556,t43]) ).
cnf(t93558,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t93557,t97]) ).
cnf(t93559,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t93558,t5611]) ).
cnf(t8643,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t93559]) ).
cnf(t8652,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t5958,t8643]) ).
cnf(t8943,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t8652]) ).
cnf(t14451,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t8943,t14257]) ).
cnf(t14456,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t14451]) ).
cnf(t14463,plain,
converse(zero) = join(converse(zero),zero),
inference(cp,[status(thm)],[t13339,t14456]) ).
cnf(t93719,plain,
converse(zero) = join(zero,converse(zero)),
inference(step,[status(thm)],[t14463,t43]) ).
cnf(t14611,plain,
join(zero,converse(zero)) = converse(zero),
inference(orient,[status(thm)],[t93719]) ).
cnf(t14618,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t311,t14611]) ).
cnf(t93720,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t14618,t43]) ).
cnf(t93721,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t93720,t14611]) ).
cnf(t93722,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t93721,t21]) ).
cnf(t14621,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t93722]) ).
cnf(t14624,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t27,t14621]) ).
cnf(t93756,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t14624,t14456]) ).
cnf(t93757,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t93756,t14621]) ).
cnf(t14706,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t93757]) ).
cnf(t14723,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t14706,t21]) ).
cnf(t14744,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t14723]) ).
cnf(t14755,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t54,t14744]) ).
cnf(t93758,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t14755,t14621]) ).
cnf(t93759,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t93758,t14744]) ).
cnf(t93760,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t93759,t43]) ).
cnf(t14757,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t93760]) ).
cnf(t93773,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t123,t14757]) ).
cnf(t14800,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t93773]) ).
cnf(t14801,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t14800]) ).
cnf(t14899,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t14893,t43]) ).
cnf(t14946,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t14899]) ).
cnf(t14955,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t14257,t14946]) ).
cnf(t2877,plain,
join(complement(X1),join(join(X2,X1),X3)) = join(top,X3),
inference(cp,[status(thm)],[t46,t2825]) ).
cnf(t93293,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t2877,t46]) ).
cnf(t93294,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t93293,t397]) ).
cnf(t3178,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t93294]) ).
cnf(t8653,plain,
top = join(complement(zero),join(X1,complement(join(X2,one)))),
inference(cp,[status(thm)],[t3178,t8643]) ).
cnf(t11047,plain,
join(complement(zero),join(X1,complement(join(X2,one)))) = top,
inference(orient,[status(thm)],[t8653]) ).
cnf(t14450,plain,
top = join(complement(zero),X1),
inference(cp,[status(thm)],[t11047,t14257]) ).
cnf(t14513,plain,
join(complement(zero),X1) = top,
inference(orient,[status(thm)],[t14450]) ).
cnf(t14514,plain,
top = complement(zero),
inference(cp,[status(thm)],[t14513,t54]) ).
cnf(t14553,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t14514]) ).
cnf(t14558,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t85,t14553]) ).
cnf(t93716,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t14558,t391]) ).
cnf(t93717,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t93716,t97]) ).
cnf(t14600,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t93717]) ).
cnf(t93819,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t14955,t14600]) ).
cnf(t93820,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t93819,t14757]) ).
cnf(t93821,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t93820,t14801]) ).
cnf(t14995,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t93821]) ).
cnf(t93822,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t14801,t14995]) ).
cnf(t14996,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t93822]) ).
cnf(t26899,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t26876,t14996]) ).
cnf(t28391,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t26899]) ).
cnf(t39,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)],[t33,t21]) ).
cnf(t93563,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)],[t39,t21]) ).
cnf(t9032,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)],[t93563]) ).
cnf(t3353,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t3343,t21]) ).
cnf(t3378,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t3353]) ).
cnf(t3397,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t3378,t256]) ).
cnf(t4326,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t3397]) ).
cnf(t93818,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(step,[status(thm)],[t4326,t14961]) ).
cnf(t14994,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(rw,[status(thm)],[t93818]) ).
cnf(t16927,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t14994]) ).
cnf(t16942,plain,
composition(meet(one,composition(converse(complement(X1)),X1)),meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(cp,[status(thm)],[t9032,t16927]) ).
cnf(t93873,plain,
composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t16942,t16927]) ).
cnf(t93874,plain,
zero = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t93873,t14744]) ).
cnf(t93875,plain,
zero = join(meet(converse(complement(X1)),composition(one,converse(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t93874,t106]) ).
cnf(t93876,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t93875,t203]) ).
cnf(t93877,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t93876,t106]) ).
cnf(t93878,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t93877,t14744]) ).
cnf(t93879,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t93878,t14946]) ).
cnf(t16973,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t93879]) ).
cnf(t28466,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t28391,t16973]) ).
cnf(t94114,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t28466,t43]) ).
cnf(t94115,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t94114,t14946]) ).
cnf(t29844,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t94115]) ).
cnf(t29849,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t29844,t14996]) ).
cnf(t93084,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t335,t405]) ).
cnf(t408,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t93084]) ).
cnf(t15595,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t15554,t408]) ).
cnf(t94061,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t15595,t97]) ).
cnf(t26018,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t94061]) ).
cnf(t26884,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t26876,t26018]) ).
cnf(t94082,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t26884,t14996]) ).
cnf(t94083,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t94082,t14946]) ).
cnf(t27421,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t94083]) ).
cnf(t27440,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t27421,t21]) ).
cnf(t29451,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t27440]) ).
cnf(t94116,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t29849,t29451]) ).
cnf(t29895,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t94116]) ).
cnf(t29900,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t29895,t14996]) ).
cnf(t29962,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t29900]) ).
cnf(t29976,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t29962,t294]) ).
cnf(t30874,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t29976]) ).
cnf(t125,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t123,t85]) ).
cnf(t4591,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t125]) ).
cnf(t93788,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t4591,t14893]) ).
cnf(t14894,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t93788]) ).
cnf(t93828,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t14894,t14995]) ).
cnf(t15023,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t93828]) ).
cnf(t16309,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t15023]) ).
cnf(t29989,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t16309,t29962]) ).
cnf(t31445,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t29989]) ).
cnf(t31492,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t30874,t31445]) ).
cnf(t94161,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t31492,t15554]) ).
cnf(t94162,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t94161,t29895]) ).
cnf(t94163,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t94162,t14996]) ).
cnf(t31513,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t94163]) ).
cnf(t15599,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t15554,t14996]) ).
cnf(t16371,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t15599]) ).
cnf(t26321,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t26302,t16371]) ).
cnf(t27674,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t26321]) ).
cnf(t27870,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t15554,t27674]) ).
cnf(t94086,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t27870,t14996]) ).
cnf(t94087,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t94086,t85]) ).
cnf(t27891,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t94087]) ).
cnf(t27917,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t27891,t43]) ).
cnf(t27960,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t27917]) ).
cnf(t28001,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X1,X2)),
inference(cp,[status(thm)],[t27960,t14996]) ).
cnf(t28877,plain,
meet(complement(X1),join(X1,X2)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t28001]) ).
cnf(t472,plain,
top = join(one,converse(join(complement(sk0),X1))),
inference(cp,[status(thm)],[t471,t60]) ).
cnf(t487,plain,
join(one,converse(join(complement(sk0),X1))) = top,
inference(orient,[status(thm)],[t472]) ).
cnf(t489,plain,
join(one,converse(converse(join(complement(sk0),X1)))) = converse(top),
inference(cp,[status(thm)],[t209,t487]) ).
cnf(t93096,plain,
join(one,join(complement(sk0),X1)) = converse(top),
inference(step,[status(thm)],[t489,t21]) ).
cnf(t93097,plain,
join(one,join(complement(sk0),X1)) = top,
inference(step,[status(thm)],[t93096,t405]) ).
cnf(t492,plain,
join(one,join(complement(sk0),X1)) = top,
inference(orient,[status(thm)],[t93097]) ).
cnf(t27791,plain,
join(join(complement(sk0),X1),complement(one)) = join(join(complement(sk0),X1),complement(top)),
inference(cp,[status(thm)],[t27674,t492]) ).
cnf(t94878,plain,
join(complement(sk0),join(X1,complement(one))) = join(join(complement(sk0),X1),complement(top)),
inference(step,[status(thm)],[t27791,t46]) ).
cnf(t94879,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),join(X1,complement(top))),
inference(step,[status(thm)],[t94878,t46]) ).
cnf(t47,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t46,t43]) ).
cnf(t15758,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t47]) ).
cnf(t94880,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(top),join(complement(sk0),X1)),
inference(step,[status(thm)],[t94879,t15758]) ).
cnf(t94881,plain,
join(complement(sk0),join(X1,complement(one))) = join(zero,join(complement(sk0),X1)),
inference(step,[status(thm)],[t94880,t97]) ).
cnf(t94882,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(step,[status(thm)],[t94881,t14893]) ).
cnf(t59707,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(orient,[status(thm)],[t94882]) ).
cnf(t59716,plain,
meet(complement(complement(sk0)),join(X1,complement(one))) = meet(complement(complement(sk0)),join(complement(sk0),X1)),
inference(cp,[status(thm)],[t28877,t59707]) ).
cnf(t94883,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),join(complement(sk0),X1)),
inference(step,[status(thm)],[t59716,t14996]) ).
cnf(t94884,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),X1),
inference(step,[status(thm)],[t94883,t28877]) ).
cnf(t94885,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(step,[status(thm)],[t94884,t14996]) ).
cnf(t59756,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(orient,[status(thm)],[t94885]) ).
cnf(t59760,plain,
meet(sk0,X1) = meet(sk0,join(complement(one),X1)),
inference(cp,[status(thm)],[t59756,t43]) ).
cnf(t59812,plain,
meet(sk0,join(complement(one),X1)) = meet(sk0,X1),
inference(orient,[status(thm)],[t59760]) ).
cnf(t59813,plain,
meet(sk0,composition(converse(X1),complement(X1))) = meet(sk0,complement(one)),
inference(cp,[status(thm)],[t59812,t1465]) ).
cnf(t15558,plain,
meet(X1,complement(join(X1,X2))) = complement(top),
inference(cp,[status(thm)],[t15554,t2778]) ).
cnf(t93855,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(step,[status(thm)],[t15558,t97]) ).
cnf(t15703,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t93855]) ).
cnf(t15718,plain,
zero = meet(sk0,complement(one)),
inference(cp,[status(thm)],[t15703,t83]) ).
cnf(t15738,plain,
meet(sk0,complement(one)) = zero,
inference(orient,[status(thm)],[t15718]) ).
cnf(t94888,plain,
meet(sk0,composition(converse(X1),complement(X1))) = zero,
inference(step,[status(thm)],[t59813,t15738]) ).
cnf(t60035,plain,
meet(sk0,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t94888]) ).
cnf(t60129,plain,
composition(meet(X1,composition(complement(X1),converse(sk0))),meet(sk0,composition(converse(X1),complement(X1)))) = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(cp,[status(thm)],[t33,t60035]) ).
cnf(t31526,plain,
meet(X1,converse(X2)) = converse(meet(X2,converse(X1))),
inference(cp,[status(thm)],[t31513,t106]) ).
cnf(t31631,plain,
converse(meet(X1,converse(X2))) = meet(X2,converse(X1)),
inference(orient,[status(thm)],[t31526]) ).
cnf(t16378,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t15129,t16371]) ).
cnf(t93861,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t16378,t16309]) ).
cnf(t16475,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t93861]) ).
cnf(t16522,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t14996,t16475]) ).
cnf(t93862,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t16522,t14996]) ).
cnf(t16552,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t93862]) ).
cnf(t16590,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t16552,t43]) ).
cnf(t16622,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t16590]) ).
cnf(t16652,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t16622,t15758]) ).
cnf(t17553,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t16652]) ).
cnf(t19615,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t17553,t19528]) ).
cnf(t22093,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t19615]) ).
cnf(t34,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)],[t33,t17]) ).
cnf(t93316,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)],[t34,t192]) ).
cnf(t93317,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)],[t93316,t17]) ).
cnf(t93318,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)],[t93317,t192]) ).
cnf(t93319,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)],[t93318,t17]) ).
cnf(t3445,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)],[t93319]) ).
cnf(t16638,plain,
sk0 = meet(sk0,one),
inference(cp,[status(thm)],[t16622,t83]) ).
cnf(t16669,plain,
meet(sk0,one) = sk0,
inference(orient,[status(thm)],[t16638]) ).
cnf(t16680,plain,
composition(meet(sk0,one),meet(one,composition(converse(sk0),one))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(cp,[status(thm)],[t3445,t16669]) ).
cnf(t93943,plain,
composition(sk0,meet(one,composition(converse(sk0),one))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t16680,t16669]) ).
cnf(t93944,plain,
composition(sk0,meet(one,converse(sk0))) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t93943,t17]) ).
cnf(t221,plain,
join(one,converse(sk0)) = converse(one),
inference(cp,[status(thm)],[t220,t83]) ).
cnf(t93061,plain,
join(one,converse(sk0)) = one,
inference(step,[status(thm)],[t221,t192]) ).
cnf(t233,plain,
join(one,converse(sk0)) = one,
inference(orient,[status(thm)],[t93061]) ).
cnf(t16577,plain,
converse(sk0) = meet(converse(sk0),one),
inference(cp,[status(thm)],[t16552,t233]) ).
cnf(t93863,plain,
converse(sk0) = meet(one,converse(sk0)),
inference(step,[status(thm)],[t16577,t106]) ).
cnf(t16609,plain,
meet(one,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t93863]) ).
cnf(t93945,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(meet(sk0,one),meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t93944,t16609]) ).
cnf(t93946,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,composition(converse(sk0),one)))),
inference(step,[status(thm)],[t93945,t16669]) ).
cnf(t93947,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,meet(one,converse(sk0)))),
inference(step,[status(thm)],[t93946,t17]) ).
cnf(t93948,plain,
composition(sk0,converse(sk0)) = join(sk0,composition(sk0,converse(sk0))),
inference(step,[status(thm)],[t93947,t16609]) ).
cnf(t18589,plain,
join(sk0,composition(sk0,converse(sk0))) = composition(sk0,converse(sk0)),
inference(orient,[status(thm)],[t93948]) ).
cnf(t18590,plain,
sk0 = meet(sk0,composition(sk0,converse(sk0))),
inference(cp,[status(thm)],[t16622,t18589]) ).
cnf(t18604,plain,
meet(sk0,composition(sk0,converse(sk0))) = sk0,
inference(orient,[status(thm)],[t18590]) ).
cnf(t22112,plain,
meet(sk0,composition(sk0,converse(sk0))) = meet(sk0,join(composition(sk0,converse(sk0)),X1)),
inference(cp,[status(thm)],[t22093,t18604]) ).
cnf(t94274,plain,
sk0 = meet(sk0,join(composition(sk0,converse(sk0)),X1)),
inference(step,[status(thm)],[t22112,t18604]) ).
cnf(t38372,plain,
meet(sk0,join(composition(sk0,converse(sk0)),X1)) = sk0,
inference(orient,[status(thm)],[t94274]) ).
cnf(t38375,plain,
sk0 = meet(sk0,composition(join(sk0,X1),converse(sk0))),
inference(cp,[status(thm)],[t38372,t24]) ).
cnf(t46857,plain,
meet(sk0,composition(join(sk0,X1),converse(sk0))) = sk0,
inference(orient,[status(thm)],[t38375]) ).
cnf(t46860,plain,
sk0 = meet(sk0,composition(one,converse(sk0))),
inference(cp,[status(thm)],[t46857,t83]) ).
cnf(t94450,plain,
sk0 = meet(sk0,converse(sk0)),
inference(step,[status(thm)],[t46860,t203]) ).
cnf(t46960,plain,
meet(sk0,converse(sk0)) = sk0,
inference(orient,[status(thm)],[t94450]) ).
cnf(t47025,plain,
meet(sk0,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t31631,t46960]) ).
cnf(t94451,plain,
sk0 = converse(sk0),
inference(step,[status(thm)],[t47025,t46960]) ).
cnf(t47049,plain,
converse(sk0) = sk0,
inference(orient,[status(thm)],[t94451]) ).
cnf(t94889,plain,
composition(meet(X1,composition(complement(X1),sk0)),meet(sk0,composition(converse(X1),complement(X1)))) = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t60129,t47049]) ).
cnf(t94890,plain,
composition(meet(X1,composition(complement(X1),sk0)),zero) = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t94889,t60035]) ).
cnf(t94891,plain,
zero = join(meet(composition(X1,sk0),complement(X1)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t94890,t14456]) ).
cnf(t94892,plain,
zero = join(meet(complement(X1),composition(X1,sk0)),composition(meet(X1,composition(complement(X1),converse(sk0))),zero)),
inference(step,[status(thm)],[t94891,t106]) ).
cnf(t94893,plain,
zero = join(meet(complement(X1),composition(X1,sk0)),zero),
inference(step,[status(thm)],[t94892,t14456]) ).
cnf(t94894,plain,
zero = meet(complement(X1),composition(X1,sk0)),
inference(step,[status(thm)],[t94893,t14946]) ).
cnf(t60137,plain,
meet(complement(X1),composition(X1,sk0)) = zero,
inference(orient,[status(thm)],[t94894]) ).
cnf(t60167,plain,
join(complement(complement(X1)),composition(X1,sk0)) = join(complement(complement(X1)),zero),
inference(cp,[status(thm)],[t28391,t60137]) ).
cnf(t94895,plain,
join(composition(X1,sk0),complement(complement(X1))) = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t60167,t43]) ).
cnf(t94896,plain,
join(composition(X1,sk0),X1) = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t94895,t14996]) ).
cnf(t94897,plain,
join(X1,composition(X1,sk0)) = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t94896,t43]) ).
cnf(t94898,plain,
join(X1,composition(X1,sk0)) = complement(complement(X1)),
inference(step,[status(thm)],[t94897,t14946]) ).
cnf(t94899,plain,
join(X1,composition(X1,sk0)) = X1,
inference(step,[status(thm)],[t94898,t14996]) ).
cnf(t60194,plain,
join(X1,composition(X1,sk0)) = X1,
inference(orient,[status(thm)],[t94899]) ).
cnf(t60215,plain,
join(X1,join(composition(X1,sk0),X2)) = join(X1,X2),
inference(cp,[status(thm)],[t46,t60194]) ).
cnf(t63401,plain,
join(X1,join(composition(X1,sk0),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t60215]) ).
cnf(t63414,plain,
join(X1,composition(X2,sk0)) = join(X1,composition(join(X1,X2),sk0)),
inference(cp,[status(thm)],[t63401,t24]) ).
cnf(t92073,plain,
join(X1,composition(join(X1,X2),sk0)) = join(X1,composition(X2,sk0)),
inference(orient,[status(thm)],[t63414]) ).
cnf(t92149,plain,
join(X1,composition(complement(X1),sk0)) = join(X1,composition(top,sk0)),
inference(cp,[status(thm)],[t92073,t51]) ).
cnf(t92411,plain,
join(X1,composition(complement(X1),sk0)) = join(X1,composition(top,sk0)),
inference(orient,[status(thm)],[t92149]) ).
cnf(t92488,plain,
meet(X1,composition(complement(complement(X1)),sk0)) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(cp,[status(thm)],[t27960,t92411]) ).
cnf(t95274,plain,
meet(X1,composition(X1,sk0)) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(step,[status(thm)],[t92488,t14996]) ).
cnf(t26082,plain,
X1 = join(meet(X2,X1),meet(X1,complement(X2))),
inference(cp,[status(thm)],[t26034,t106]) ).
cnf(t41289,plain,
join(meet(X1,X2),meet(X2,complement(X1))) = X2,
inference(orient,[status(thm)],[t26082]) ).
cnf(t41485,plain,
X1 = join(meet(X2,X1),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t41289,t106]) ).
cnf(t51037,plain,
join(meet(X1,X2),meet(complement(X1),X2)) = X2,
inference(orient,[status(thm)],[t41485]) ).
cnf(t60171,plain,
composition(X1,sk0) = join(zero,meet(complement(complement(X1)),composition(X1,sk0))),
inference(cp,[status(thm)],[t51037,t60137]) ).
cnf(t94903,plain,
composition(X1,sk0) = meet(complement(complement(X1)),composition(X1,sk0)),
inference(step,[status(thm)],[t60171,t14893]) ).
cnf(t94904,plain,
composition(X1,sk0) = meet(composition(X1,sk0),complement(complement(X1))),
inference(step,[status(thm)],[t94903,t106]) ).
cnf(t94905,plain,
composition(X1,sk0) = meet(composition(X1,sk0),X1),
inference(step,[status(thm)],[t94904,t14996]) ).
cnf(t94906,plain,
composition(X1,sk0) = meet(X1,composition(X1,sk0)),
inference(step,[status(thm)],[t94905,t106]) ).
cnf(t60317,plain,
meet(X1,composition(X1,sk0)) = composition(X1,sk0),
inference(orient,[status(thm)],[t94906]) ).
cnf(t95275,plain,
composition(X1,sk0) = meet(X1,join(complement(X1),composition(top,sk0))),
inference(step,[status(thm)],[t95274,t60317]) ).
cnf(t95276,plain,
composition(X1,sk0) = meet(X1,composition(top,sk0)),
inference(step,[status(thm)],[t95275,t27960]) ).
cnf(t92527,plain,
meet(X1,composition(top,sk0)) = composition(X1,sk0),
inference(orient,[status(thm)],[t95276]) ).
cnf(t92609,plain,
meet(X1,converse(composition(top,sk0))) = converse(composition(converse(X1),sk0)),
inference(cp,[status(thm)],[t31513,t92527]) ).
cnf(t95277,plain,
meet(X1,composition(converse(sk0),top)) = converse(composition(converse(X1),sk0)),
inference(step,[status(thm)],[t92609,t431]) ).
cnf(t95278,plain,
meet(X1,composition(sk0,top)) = converse(composition(converse(X1),sk0)),
inference(step,[status(thm)],[t95277,t47049]) ).
cnf(t95279,plain,
meet(X1,composition(sk0,top)) = composition(converse(sk0),X1),
inference(step,[status(thm)],[t95278,t169]) ).
cnf(t95280,plain,
meet(X1,composition(sk0,top)) = composition(sk0,X1),
inference(step,[status(thm)],[t95279,t47049]) ).
cnf(t92929,plain,
meet(X1,composition(sk0,top)) = composition(sk0,X1),
inference(orient,[status(thm)],[t95280]) ).
cnf(c17,plain,
meet(composition(sk0,top),sk1) != composition(sk0,sk1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
meet(composition(sk0,top),sk1) != composition(sk0,sk1),
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
meet(sk1,composition(sk0,top)) != composition(sk0,sk1),
inference(rw,[status(thm)],[goal_0,t106]) ).
cnf(g0_1,plain,
composition(sk0,sk1) != composition(sk0,sk1),
inference(rw,[status(thm)],[g0_0,t92929]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL026+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.39 % Computer : n026.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Thu Sep 24 07:23:44 UTC 2026
% 0.15/5.40 % CPUTime :
% 0.15/5.40 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 31.07/9.91 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.07/9.91 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------