%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL029+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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:29 PM UTC 2026
% Result : Theorem 118.69s 15.59s
% Output : Proof 118.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 157
% Number of leaves : 14
% Syntax : Number of formulae : 768 ( 764 unt; 0 def)
% Number of atoms : 776 ( 775 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 18 ( 10 ~; 0 |; 6 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 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 : 934 ( 99 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(t7,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t44,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
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(t6,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t20,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t46,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t44,t20]) ).
cnf(t288487,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t46,t44]) ).
cnf(t74,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t288487]) ).
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(t14,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t15,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t21,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t15]) ).
cnf(t288503,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t21,t20]) ).
cnf(t288504,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t288503,t44]) ).
cnf(t288505,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t288504,t20]) ).
cnf(t256,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t288505]) ).
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(t13,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t288484,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t20]) ).
cnf(t31,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t288484]) ).
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(t8,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t56,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
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(t19,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t58,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t56,t19]) ).
cnf(t171,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t58]) ).
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(t18,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t172,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t171,t18]) ).
cnf(t288493,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t172,t19]) ).
cnf(t186,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t288493]) ).
cnf(t187,plain,
one = converse(one),
inference(cp,[status(thm)],[t186,t18]) ).
cnf(t193,plain,
converse(one) = one,
inference(orient,[status(thm)],[t187]) ).
cnf(t288494,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t186,t193]) ).
cnf(t203,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t288494]) ).
cnf(t204,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t203]) ).
cnf(t207,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t31,t204]) ).
cnf(t288498,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t207,t193]) ).
cnf(t288499,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t288498,t204]) ).
cnf(t241,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t288499]) ).
cnf(t263,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t256,t241]) ).
cnf(t288507,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t263,t20]) ).
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(t5,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t63,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t288508,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t288507,t63]) ).
cnf(t288509,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t288508,t20]) ).
cnf(t272,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t288509]) ).
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(t11,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t22,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
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(t4,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t25,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t45,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t44,t25]) ).
cnf(t288485,plain,
zero = complement(top),
inference(step,[status(thm)],[t45,t63]) ).
cnf(t65,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t288485]) ).
cnf(t245,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t241,t65]) ).
cnf(t288500,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t245,t65]) ).
cnf(t288501,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t288500,t65]) ).
cnf(t252,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t288501]) ).
cnf(t253,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t22,t252]) ).
cnf(t311,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t253]) ).
cnf(t313,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t311,t272]) ).
cnf(t288516,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t313,t272]) ).
cnf(t316,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t288516]) ).
cnf(t288519,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t272,t316]) ).
cnf(t327,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t288519]) ).
cnf(t346,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t327]) ).
cnf(t347,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t346,t44]) ).
cnf(t808,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t347]) ).
cnf(t811,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t808,t346]) ).
cnf(t912,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t811]) ).
cnf(t918,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t346,t912]) ).
cnf(t1184,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t918]) ).
cnf(t349,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t241,t346]) ).
cnf(t288531,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t349,t346]) ).
cnf(t288532,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t288531,t346]) ).
cnf(t365,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t288532]) ).
cnf(t367,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t22,t365]) ).
cnf(t469,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t367]) ).
cnf(t474,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t469,t256]) ).
cnf(t288555,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t474,t256]) ).
cnf(t288556,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t288555,t20]) ).
cnf(t512,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t288556]) ).
cnf(t514,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t512,t74]) ).
cnf(t519,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t514]) ).
cnf(t522,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t22,t519]) ).
cnf(t2806,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t522]) ).
cnf(t288596,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t256,t1184]) ).
cnf(t1210,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t288596]) ).
cnf(t7900,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t1210]) ).
cnf(t7996,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t2806,t7900]) ).
cnf(t8186,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t7996]) ).
cnf(t810,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t808,t346]) ).
cnf(t896,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t810]) ).
cnf(t903,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t346,t896]) ).
cnf(t928,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t903]) ).
cnf(t945,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t928,t346]) ).
cnf(t1211,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t945]) ).
cnf(t8191,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t8186,t1211]) ).
cnf(t8759,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t8191]) ).
cnf(t8907,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t1184,t8759]) ).
cnf(t288788,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t8907,t346]) ).
cnf(t288789,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t288788,t44]) ).
cnf(t9077,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t288789]) ).
cnf(t9115,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t9077,t20]) ).
cnf(t9135,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t9115]) ).
cnf(t8240,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t2806,t8186]) ).
cnf(t289300,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(step,[status(thm)],[t8240,t2806]) ).
cnf(t42626,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t289300]) ).
cnf(t42645,plain,
join(X1,X2) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t42626,t896]) ).
cnf(t46315,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t42645]) ).
cnf(t46411,plain,
meet(X1,meet(X2,join(X3,complement(complement(X1))))) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t9135,t46315]) ).
cnf(t289347,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t46411,t346]) ).
cnf(t289348,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(step,[status(thm)],[t289347,t9135]) ).
cnf(t46588,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t289348]) ).
cnf(t46689,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X3,X1)),
inference(cp,[status(thm)],[t46588,t512]) ).
cnf(t48725,plain,
meet(meet(X1,X2),meet(X3,X1)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t46689]) ).
cnf(t48748,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t48725,t74]) ).
cnf(t46666,plain,
meet(X1,X2) = meet(X1,meet(join(X3,X1),X2)),
inference(cp,[status(thm)],[t46588,t74]) ).
cnf(t47557,plain,
meet(X1,meet(join(X2,X1),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t46666]) ).
cnf(t47646,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X2,X3)),
inference(cp,[status(thm)],[t47557,t519]) ).
cnf(t50646,plain,
meet(meet(X1,X2),meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t47646]) ).
cnf(t289362,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(step,[status(thm)],[t48748,t50646]) ).
cnf(t51636,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(orient,[status(thm)],[t289362]) ).
cnf(t51667,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(cp,[status(thm)],[t51636,t74]) ).
cnf(t53078,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t51667]) ).
cnf(t8204,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t8186,t74]) ).
cnf(t8512,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t8204]) ).
cnf(t8525,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t8512,t346]) ).
cnf(t9964,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t8525]) ).
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(t9,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t35,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t37,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t35,t19]) ).
cnf(t140,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t37]) ).
cnf(t141,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t140,t25]) ).
cnf(t473,plain,
join(X1,complement(X1)) = join(X1,top),
inference(cp,[status(thm)],[t469,t25]) ).
cnf(t288547,plain,
top = join(X1,top),
inference(step,[status(thm)],[t473,t25]) ).
cnf(t480,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t288547]) ).
cnf(t484,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t140,t480]) ).
cnf(t499,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t484]) ).
cnf(t481,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t480,t20]) ).
cnf(t486,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t481]) ).
cnf(t500,plain,
converse(top) = top,
inference(cp,[status(thm)],[t499,t486]) ).
cnf(t504,plain,
converse(top) = top,
inference(orient,[status(thm)],[t500]) ).
cnf(t288597,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t141,t504]) ).
cnf(t1225,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t288597]) ).
cnf(t9160,plain,
meet(X1,converse(complement(converse(complement(X1))))) = meet(X1,top),
inference(cp,[status(thm)],[t9135,t1225]) ).
cnf(t68,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t44,t65]) ).
cnf(t89,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t68]) ).
cnf(t276,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t89,t272]) ).
cnf(t277,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t276]) ).
cnf(t348,plain,
complement(complement(X1)) = meet(top,X1),
inference(cp,[status(thm)],[t277,t346]) ).
cnf(t288530,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t348,t346]) ).
cnf(t363,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t288530]) ).
cnf(t364,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t363,t74]) ).
cnf(t368,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t364]) ).
cnf(t288792,plain,
meet(X1,converse(complement(converse(complement(X1))))) = X1,
inference(step,[status(thm)],[t9160,t368]) ).
cnf(t9249,plain,
meet(X1,converse(complement(converse(complement(X1))))) = X1,
inference(orient,[status(thm)],[t288792]) ).
cnf(t9290,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = complement(complement(X1)),
inference(cp,[status(thm)],[t896,t9249]) ).
cnf(t288793,plain,
join(X1,complement(converse(complement(converse(X1))))) = complement(complement(X1)),
inference(step,[status(thm)],[t9290,t346]) ).
cnf(t288794,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t288793,t346]) ).
cnf(t9298,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t288794]) ).
cnf(t9352,plain,
join(X1,converse(complement(converse(complement(converse(converse(X1))))))) = converse(converse(X1)),
inference(cp,[status(thm)],[t140,t9298]) ).
cnf(t288795,plain,
join(X1,converse(complement(converse(complement(X1))))) = converse(converse(X1)),
inference(step,[status(thm)],[t9352,t19]) ).
cnf(t288796,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(step,[status(thm)],[t288795,t19]) ).
cnf(t9361,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(orient,[status(thm)],[t288796]) ).
cnf(t9390,plain,
meet(X1,converse(complement(converse(complement(complement(X1)))))) = meet(X1,complement(X1)),
inference(cp,[status(thm)],[t9135,t9361]) ).
cnf(t288797,plain,
meet(X1,converse(complement(converse(X1)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t9390,t346]) ).
cnf(t288798,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t288797,t63]) ).
cnf(t9413,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t288798]) ).
cnf(t9424,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(cp,[status(thm)],[t9413,t19]) ).
cnf(t9435,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t9424]) ).
cnf(t10001,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t9964,t9435]) ).
cnf(t288839,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t10001,t20]) ).
cnf(t318,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t316,t20]) ).
cnf(t339,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t318]) ).
cnf(t288840,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t288839,t339]) ).
cnf(t11421,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t288840]) ).
cnf(t11426,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t11421,t346]) ).
cnf(t9309,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t9298,t19]) ).
cnf(t10767,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t9309]) ).
cnf(t288841,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t11426,t10767]) ).
cnf(t11461,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t288841]) ).
cnf(t11466,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t11461,t346]) ).
cnf(t11513,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t11466]) ).
cnf(t11523,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t11513,t140]) ).
cnf(t12259,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t11523]) ).
cnf(t11534,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t808,t11513]) ).
cnf(t12496,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t11534]) ).
cnf(t12538,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t12259,t12496]) ).
cnf(t288886,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t12538,t1184]) ).
cnf(t288887,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t288886,t11461]) ).
cnf(t288888,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t288887,t346]) ).
cnf(t12548,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t288888]) ).
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(t12,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t28,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t60,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t28,t56]) ).
cnf(t22981,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t60]) ).
cnf(t22984,plain,
composition(join(converse(one),X1),converse(X2)) = join(converse(X2),composition(X1,converse(X2))),
inference(cp,[status(thm)],[t22981,t18]) ).
cnf(t289696,plain,
composition(join(one,X1),converse(X2)) = join(converse(X2),composition(X1,converse(X2))),
inference(step,[status(thm)],[t22984,t193]) ).
cnf(t86398,plain,
join(converse(X1),composition(X2,converse(X1))) = composition(join(one,X2),converse(X1)),
inference(orient,[status(thm)],[t289696]) ).
cnf(t23,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t22,t20]) ).
cnf(t545,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t23]) ).
cnf(t557,plain,
join(complement(X1),join(X2,X1)) = join(X2,top),
inference(cp,[status(thm)],[t545,t25]) ).
cnf(t288559,plain,
join(X1,join(complement(X1),X2)) = join(X2,top),
inference(step,[status(thm)],[t557,t545]) ).
cnf(t288560,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t288559,t480]) ).
cnf(t650,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t288560]) ).
cnf(t662,plain,
X1 = join(meet(X1,join(complement(complement(X1)),X2)),complement(top)),
inference(cp,[status(thm)],[t256,t650]) ).
cnf(t288561,plain,
X1 = join(complement(top),meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t662,t20]) ).
cnf(t288562,plain,
X1 = join(zero,meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t288561,t65]) ).
cnf(t288563,plain,
X1 = meet(X1,join(complement(complement(X1)),X2)),
inference(step,[status(thm)],[t288562,t316]) ).
cnf(t288564,plain,
X1 = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t288563,t346]) ).
cnf(t676,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t288564]) ).
cnf(t687,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t676,t20]) ).
cnf(t719,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t687]) ).
cnf(t654,plain,
top = join(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t650,t20]) ).
cnf(t765,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t654]) ).
cnf(t820,plain,
top = join(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t765,t808]) ).
cnf(t851,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t820]) ).
cnf(t930,plain,
meet(complement(X1),meet(X2,X1)) = complement(top),
inference(cp,[status(thm)],[t928,t851]) ).
cnf(t288583,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(step,[status(thm)],[t930,t65]) ).
cnf(t968,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t288583]) ).
cnf(t978,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t968,t719]) ).
cnf(t288591,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t978,t74]) ).
cnf(t1128,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t288591]) ).
cnf(t33,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t31,t18]) ).
cnf(t5651,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t33]) ).
cnf(t5677,plain,
zero = meet(composition(converse(X1),complement(X1)),complement(complement(one))),
inference(cp,[status(thm)],[t1128,t5651]) ).
cnf(t288738,plain,
zero = meet(complement(complement(one)),composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t5677,t74]) ).
cnf(t288739,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t288738,t346]) ).
cnf(t5682,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t288739]) ).
cnf(t5695,plain,
zero = meet(one,composition(converse(complement(X1)),X1)),
inference(cp,[status(thm)],[t5682,t346]) ).
cnf(t5709,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t5695]) ).
cnf(t5711,plain,
zero = meet(one,converse(complement(one))),
inference(cp,[status(thm)],[t5709,t18]) ).
cnf(t5718,plain,
meet(one,converse(complement(one))) = zero,
inference(orient,[status(thm)],[t5711]) ).
cnf(t7934,plain,
one = join(zero,meet(one,complement(converse(complement(one))))),
inference(cp,[status(thm)],[t7900,t5718]) ).
cnf(t288769,plain,
one = meet(one,complement(converse(complement(one)))),
inference(step,[status(thm)],[t7934,t316]) ).
cnf(t8009,plain,
meet(one,complement(converse(complement(one)))) = one,
inference(orient,[status(thm)],[t288769]) ).
cnf(t8027,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(cp,[status(thm)],[t912,t8009]) ).
cnf(t8031,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t8027]) ).
cnf(t8039,plain,
converse(complement(one)) = meet(converse(complement(one)),complement(one)),
inference(cp,[status(thm)],[t719,t8031]) ).
cnf(t288775,plain,
converse(complement(one)) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t8039,t74]) ).
cnf(t731,plain,
converse(X1) = meet(converse(X1),converse(join(X2,X1))),
inference(cp,[status(thm)],[t719,t35]) ).
cnf(t2438,plain,
meet(converse(X1),converse(join(X2,X1))) = converse(X1),
inference(orient,[status(thm)],[t731]) ).
cnf(t8043,plain,
converse(converse(complement(one))) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(cp,[status(thm)],[t2438,t8031]) ).
cnf(t288770,plain,
complement(one) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(step,[status(thm)],[t8043,t19]) ).
cnf(t288771,plain,
complement(one) = meet(converse(complement(one)),converse(converse(complement(one)))),
inference(step,[status(thm)],[t288770,t74]) ).
cnf(t288772,plain,
complement(one) = meet(converse(complement(one)),complement(one)),
inference(step,[status(thm)],[t288771,t19]) ).
cnf(t288773,plain,
complement(one) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t288772,t74]) ).
cnf(t8052,plain,
meet(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t288773]) ).
cnf(t288776,plain,
converse(complement(one)) = complement(one),
inference(step,[status(thm)],[t288775,t8052]) ).
cnf(t8259,plain,
converse(complement(one)) = complement(one),
inference(orient,[status(thm)],[t288776]) ).
cnf(t8263,plain,
converse(join(X1,complement(one))) = join(converse(X1),complement(one)),
inference(cp,[status(thm)],[t35,t8259]) ).
cnf(t8405,plain,
converse(join(X1,complement(one))) = join(converse(X1),complement(one)),
inference(orient,[status(thm)],[t8263]) ).
cnf(t11514,plain,
converse(complement(join(X1,complement(one)))) = complement(join(converse(X1),complement(one))),
inference(cp,[status(thm)],[t11513,t8405]) ).
cnf(t288863,plain,
converse(meet(complement(X1),one)) = complement(join(converse(X1),complement(one))),
inference(step,[status(thm)],[t11514,t928]) ).
cnf(t288864,plain,
converse(meet(one,complement(X1))) = complement(join(converse(X1),complement(one))),
inference(step,[status(thm)],[t288863,t74]) ).
cnf(t288865,plain,
converse(meet(one,complement(X1))) = meet(complement(converse(X1)),one),
inference(step,[status(thm)],[t288864,t928]) ).
cnf(t288866,plain,
converse(meet(one,complement(X1))) = meet(one,complement(converse(X1))),
inference(step,[status(thm)],[t288865,t74]) ).
cnf(t288867,plain,
converse(meet(one,complement(X1))) = meet(one,converse(complement(X1))),
inference(step,[status(thm)],[t288866,t11513]) ).
cnf(t11567,plain,
converse(meet(one,complement(X1))) = meet(one,converse(complement(X1))),
inference(orient,[status(thm)],[t288867]) ).
cnf(t11579,plain,
meet(one,converse(complement(complement(X1)))) = converse(meet(one,X1)),
inference(cp,[status(thm)],[t11567,t346]) ).
cnf(t288868,plain,
meet(one,converse(X1)) = converse(meet(one,X1)),
inference(step,[status(thm)],[t11579,t346]) ).
cnf(t11606,plain,
converse(meet(one,X1)) = meet(one,converse(X1)),
inference(orient,[status(thm)],[t288868]) ).
cnf(t11629,plain,
converse(composition(X1,meet(one,X2))) = composition(meet(one,converse(X2)),converse(X1)),
inference(cp,[status(thm)],[t56,t11606]) ).
cnf(t82617,plain,
composition(meet(one,converse(X1)),converse(X2)) = converse(composition(X2,meet(one,X1))),
inference(orient,[status(thm)],[t11629]) ).
cnf(t86448,plain,
composition(join(one,meet(one,converse(X1))),converse(X2)) = join(converse(X2),converse(composition(X2,meet(one,X1)))),
inference(cp,[status(thm)],[t86398,t82617]) ).
cnf(t289815,plain,
composition(one,converse(X2)) = join(converse(X2),converse(composition(X2,meet(one,X1)))),
inference(step,[status(thm)],[t86448,t512]) ).
cnf(t289816,plain,
converse(X2) = join(converse(X2),converse(composition(X2,meet(one,X1)))),
inference(step,[status(thm)],[t289815,t204]) ).
cnf(t289817,plain,
converse(X2) = converse(join(X2,composition(X2,meet(one,X1)))),
inference(step,[status(thm)],[t289816,t35]) ).
cnf(t101412,plain,
converse(join(X1,composition(X1,meet(one,X2)))) = converse(X1),
inference(orient,[status(thm)],[t289817]) ).
cnf(t11630,plain,
converse(composition(meet(one,X1),X2)) = composition(converse(X2),meet(one,converse(X1))),
inference(cp,[status(thm)],[t56,t11606]) ).
cnf(t82719,plain,
composition(converse(X1),meet(one,converse(X2))) = converse(composition(meet(one,X2),X1)),
inference(orient,[status(thm)],[t11630]) ).
cnf(t101421,plain,
converse(converse(X1)) = converse(join(converse(X1),converse(composition(meet(one,X2),X1)))),
inference(cp,[status(thm)],[t101412,t82719]) ).
cnf(t289818,plain,
X1 = converse(join(converse(X1),converse(composition(meet(one,X2),X1)))),
inference(step,[status(thm)],[t101421,t19]) ).
cnf(t289819,plain,
X1 = join(X1,converse(converse(composition(meet(one,X2),X1)))),
inference(step,[status(thm)],[t289818,t140]) ).
cnf(t289820,plain,
X1 = join(X1,composition(meet(one,X2),X1)),
inference(step,[status(thm)],[t289819,t19]) ).
cnf(t101620,plain,
join(X1,composition(meet(one,X2),X1)) = X1,
inference(orient,[status(thm)],[t289820]) ).
cnf(t197,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t35,t193]) ).
cnf(t288495,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t197,t20]) ).
cnf(t218,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t288495]) ).
fof(f13,conjecture,
! [X0,X1,X2] :
( ( join(X1,one) = one
& join(X0,one) = one )
=> meet(composition(X0,X2),composition(X1,X2)) = composition(meet(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f13_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( ( join(X1,one) = one
& join(X0,one) = one )
=> meet(composition(X0,X2),composition(X1,X2)) = composition(meet(X0,X1),X2) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f13_nnf,plain,
? [X0,X1,X2] :
( meet(composition(X0,X2),composition(X1,X2)) != composition(meet(X0,X1),X2)
& join(X1,one) = one
& join(X0,one) = one ),
inference(nnf_transformation,[status(thm)],[f13_neg]) ).
fof(f13_sk,plain,
( meet(composition(sk0,sk2),composition(sk1,sk2)) != composition(meet(sk0,sk1),sk2)
& join(sk1,one) = one
& join(sk0,one) = one ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f13_nnf]) ).
cnf(c14,plain,
join(sk1,one) = one,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t3,plain,
join(sk1,one) = one,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t42,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t220,plain,
join(one,converse(sk1)) = converse(one),
inference(cp,[status(thm)],[t218,t42]) ).
cnf(t288496,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t220,t193]) ).
cnf(t233,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t288496]) ).
cnf(t727,plain,
converse(sk1) = meet(converse(sk1),one),
inference(cp,[status(thm)],[t719,t233]) ).
cnf(t288567,plain,
converse(sk1) = meet(one,converse(sk1)),
inference(step,[status(thm)],[t727,t74]) ).
cnf(t737,plain,
meet(one,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t288567]) ).
cnf(t101654,plain,
X1 = join(X1,composition(converse(sk1),X1)),
inference(cp,[status(thm)],[t101620,t737]) ).
cnf(t101814,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(orient,[status(thm)],[t101654]) ).
cnf(t101914,plain,
join(X1,converse(composition(converse(sk1),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t140,t101814]) ).
cnf(t289821,plain,
join(X1,composition(converse(converse(X1)),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t101914,t171]) ).
cnf(t289822,plain,
join(X1,composition(X1,sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t289821,t19]) ).
cnf(t289823,plain,
join(X1,composition(X1,sk1)) = X1,
inference(step,[status(thm)],[t289822,t19]) ).
cnf(t102660,plain,
join(X1,composition(X1,sk1)) = X1,
inference(orient,[status(thm)],[t289823]) ).
cnf(t102680,plain,
join(X1,join(composition(X1,sk1),X2)) = join(X1,X2),
inference(cp,[status(thm)],[t22,t102660]) ).
cnf(t134170,plain,
join(X1,join(composition(X1,sk1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t102680]) ).
cnf(t134198,plain,
join(X1,composition(X2,sk1)) = join(X1,composition(join(X1,X2),sk1)),
inference(cp,[status(thm)],[t134170,t28]) ).
cnf(t281021,plain,
join(X1,composition(join(X1,X2),sk1)) = join(X1,composition(X2,sk1)),
inference(orient,[status(thm)],[t134198]) ).
cnf(t281216,plain,
join(X1,composition(complement(X1),sk1)) = join(X1,composition(top,sk1)),
inference(cp,[status(thm)],[t281021,t25]) ).
cnf(t281837,plain,
join(X1,composition(complement(X1),sk1)) = join(X1,composition(top,sk1)),
inference(orient,[status(thm)],[t281216]) ).
cnf(t281975,plain,
meet(X1,composition(complement(complement(X1)),sk1)) = meet(X1,join(complement(X1),composition(top,sk1))),
inference(cp,[status(thm)],[t9135,t281837]) ).
cnf(t291555,plain,
meet(X1,composition(X1,sk1)) = meet(X1,join(complement(X1),composition(top,sk1))),
inference(step,[status(thm)],[t281975,t346]) ).
cnf(t102679,plain,
composition(X1,sk1) = meet(composition(X1,sk1),X1),
inference(cp,[status(thm)],[t719,t102660]) ).
cnf(t289827,plain,
composition(X1,sk1) = meet(X1,composition(X1,sk1)),
inference(step,[status(thm)],[t102679,t74]) ).
cnf(t102953,plain,
meet(X1,composition(X1,sk1)) = composition(X1,sk1),
inference(orient,[status(thm)],[t289827]) ).
cnf(t291556,plain,
composition(X1,sk1) = meet(X1,join(complement(X1),composition(top,sk1))),
inference(step,[status(thm)],[t291555,t102953]) ).
cnf(t291557,plain,
composition(X1,sk1) = meet(X1,composition(top,sk1)),
inference(step,[status(thm)],[t291556,t9135]) ).
cnf(t282038,plain,
meet(X1,composition(top,sk1)) = composition(X1,sk1),
inference(orient,[status(thm)],[t291557]) ).
cnf(t282174,plain,
meet(X1,converse(composition(top,sk1))) = converse(composition(converse(X1),sk1)),
inference(cp,[status(thm)],[t12548,t282038]) ).
cnf(t508,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t56,t504]) ).
cnf(t536,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t508]) ).
cnf(t291617,plain,
meet(X1,composition(converse(sk1),top)) = converse(composition(converse(X1),sk1)),
inference(step,[status(thm)],[t282174,t536]) ).
cnf(t62,plain,
complement(converse(X1)) = join(complement(converse(X1)),composition(converse(converse(X2)),complement(converse(composition(X1,X2))))),
inference(cp,[status(thm)],[t31,t56]) ).
cnf(t289086,plain,
converse(complement(X1)) = join(complement(converse(X1)),composition(converse(converse(X2)),complement(converse(composition(X1,X2))))),
inference(step,[status(thm)],[t62,t11513]) ).
cnf(t289087,plain,
converse(complement(X1)) = join(converse(complement(X1)),composition(converse(converse(X2)),complement(converse(composition(X1,X2))))),
inference(step,[status(thm)],[t289086,t11513]) ).
cnf(t289088,plain,
converse(complement(X1)) = join(converse(complement(X1)),composition(X2,complement(converse(composition(X1,X2))))),
inference(step,[status(thm)],[t289087,t19]) ).
cnf(t289089,plain,
converse(complement(X1)) = join(converse(complement(X1)),composition(X2,converse(complement(composition(X1,X2))))),
inference(step,[status(thm)],[t289088,t11513]) ).
cnf(t28969,plain,
join(converse(complement(X1)),composition(X2,converse(complement(composition(X1,X2))))) = converse(complement(X1)),
inference(orient,[status(thm)],[t289089]) ).
cnf(t507,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t56,t504]) ).
cnf(t525,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t507]) ).
cnf(t530,plain,
converse(join(X1,composition(X2,top))) = join(converse(X1),composition(top,converse(X2))),
inference(cp,[status(thm)],[t35,t525]) ).
cnf(t80416,plain,
join(converse(X1),composition(top,converse(X2))) = converse(join(X1,composition(X2,top))),
inference(orient,[status(thm)],[t530]) ).
cnf(t86399,plain,
composition(join(one,top),converse(X1)) = converse(join(X1,composition(X1,top))),
inference(cp,[status(thm)],[t86398,t80416]) ).
cnf(t289697,plain,
composition(top,converse(X1)) = converse(join(X1,composition(X1,top))),
inference(step,[status(thm)],[t86399,t480]) ).
cnf(t86593,plain,
converse(join(X1,composition(X1,top))) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t289697]) ).
cnf(t38,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t35,t19]) ).
cnf(t149,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t38]) ).
cnf(t542,plain,
join(converse(X1),composition(top,X2)) = converse(join(X1,composition(converse(X2),top))),
inference(cp,[status(thm)],[t149,t536]) ).
cnf(t80791,plain,
converse(join(X1,composition(converse(X2),top))) = join(converse(X1),composition(top,X2)),
inference(orient,[status(thm)],[t542]) ).
cnf(t86594,plain,
composition(top,converse(converse(X1))) = join(converse(converse(X1)),composition(top,X1)),
inference(cp,[status(thm)],[t86593,t80791]) ).
cnf(t289698,plain,
composition(top,X1) = join(converse(converse(X1)),composition(top,X1)),
inference(step,[status(thm)],[t86594,t19]) ).
cnf(t289699,plain,
composition(top,X1) = join(composition(top,X1),converse(converse(X1))),
inference(step,[status(thm)],[t289698,t20]) ).
cnf(t289700,plain,
composition(top,X1) = join(composition(top,X1),X1),
inference(step,[status(thm)],[t289699,t19]) ).
cnf(t289701,plain,
composition(top,X1) = join(X1,composition(top,X1)),
inference(step,[status(thm)],[t289700,t20]) ).
cnf(t86778,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t289701]) ).
cnf(t86786,plain,
X1 = meet(X1,composition(top,X1)),
inference(cp,[status(thm)],[t676,t86778]) ).
cnf(t87170,plain,
meet(X1,composition(top,X1)) = X1,
inference(orient,[status(thm)],[t86786]) ).
cnf(t87231,plain,
meet(X1,composition(top,join(X2,X1))) = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t47557,t87170]) ).
cnf(t289719,plain,
meet(X1,composition(top,join(X2,X1))) = X1,
inference(step,[status(thm)],[t87231,t719]) ).
cnf(t88769,plain,
meet(X1,composition(top,join(X2,X1))) = X1,
inference(orient,[status(thm)],[t289719]) ).
cnf(t145,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t56,t140]) ).
cnf(t38034,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t145]) ).
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(t10,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t51,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t55,plain,
complement(X1) = join(complement(X1),composition(converse(composition(X2,X3)),complement(composition(X2,composition(X3,X1))))),
inference(cp,[status(thm)],[t31,t51]) ).
cnf(t16888,plain,
join(complement(X1),composition(converse(composition(X2,X3)),complement(composition(X2,composition(X3,X1))))) = complement(X1),
inference(orient,[status(thm)],[t55]) ).
cnf(t32,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(cp,[status(thm)],[t31,t19]) ).
cnf(t4082,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t32]) ).
cnf(t4088,plain,
complement(top) = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(cp,[status(thm)],[t4082,t65]) ).
cnf(t288692,plain,
zero = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(step,[status(thm)],[t4088,t65]) ).
cnf(t288693,plain,
zero = composition(X1,complement(composition(converse(X1),top))),
inference(step,[status(thm)],[t288692,t316]) ).
cnf(t4137,plain,
composition(X1,complement(composition(converse(X1),top))) = zero,
inference(orient,[status(thm)],[t288693]) ).
cnf(t4148,plain,
zero = composition(converse(X1),complement(composition(X1,top))),
inference(cp,[status(thm)],[t4137,t19]) ).
cnf(t4210,plain,
composition(converse(X1),complement(composition(X1,top))) = zero,
inference(orient,[status(thm)],[t4148]) ).
cnf(t16922,plain,
complement(complement(composition(X1,top))) = join(complement(complement(composition(X1,top))),composition(converse(composition(X2,converse(X1))),complement(composition(X2,zero)))),
inference(cp,[status(thm)],[t16888,t4210]) ).
cnf(t289324,plain,
composition(X1,top) = join(complement(complement(composition(X1,top))),composition(converse(composition(X2,converse(X1))),complement(composition(X2,zero)))),
inference(step,[status(thm)],[t16922,t346]) ).
cnf(t289325,plain,
composition(X1,top) = join(composition(X1,top),composition(converse(composition(X2,converse(X1))),complement(composition(X2,zero)))),
inference(step,[status(thm)],[t289324,t346]) ).
cnf(t57,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t56,t19]) ).
cnf(t159,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t57]) ).
cnf(t289326,plain,
composition(X1,top) = join(composition(X1,top),composition(composition(X1,converse(X2)),complement(composition(X2,zero)))),
inference(step,[status(thm)],[t289325,t159]) ).
cnf(t289327,plain,
composition(X1,top) = join(composition(X1,top),composition(X1,composition(converse(X2),complement(composition(X2,zero))))),
inference(step,[status(thm)],[t289326,t51]) ).
cnf(t4141,plain,
zero = composition(top,complement(composition(top,top))),
inference(cp,[status(thm)],[t4137,t504]) ).
cnf(t4160,plain,
composition(top,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t4141]) ).
cnf(t4163,plain,
composition(join(top,X1),complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(cp,[status(thm)],[t28,t4160]) ).
cnf(t288694,plain,
composition(top,complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t4163,t486]) ).
cnf(t288695,plain,
zero = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t288694,t4160]) ).
cnf(t288696,plain,
zero = composition(X1,complement(composition(top,top))),
inference(step,[status(thm)],[t288695,t316]) ).
cnf(t4170,plain,
composition(X1,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t288696]) ).
cnf(t4172,plain,
zero = composition(X1,composition(X2,complement(composition(top,top)))),
inference(cp,[status(thm)],[t4170,t51]) ).
cnf(t288697,plain,
zero = composition(X1,zero),
inference(step,[status(thm)],[t4172,t4170]) ).
cnf(t4177,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t288697]) ).
cnf(t289328,plain,
composition(X1,top) = join(composition(X1,top),composition(X1,composition(converse(X2),complement(zero)))),
inference(step,[status(thm)],[t289327,t4177]) ).
cnf(t317,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t316,t25]) ).
cnf(t329,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t317]) ).
cnf(t289329,plain,
composition(X1,top) = join(composition(X1,top),composition(X1,composition(converse(X2),top))),
inference(step,[status(thm)],[t289328,t329]) ).
cnf(t54,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t28,t51]) ).
cnf(t14516,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t54]) ).
cnf(t289330,plain,
composition(X1,top) = composition(join(X1,composition(X1,converse(X2))),top),
inference(step,[status(thm)],[t289329,t14516]) ).
cnf(t44863,plain,
composition(join(X1,composition(X1,converse(X2))),top) = composition(X1,top),
inference(orient,[status(thm)],[t289330]) ).
cnf(t44901,plain,
composition(X1,top) = composition(join(X1,composition(X1,X2)),top),
inference(cp,[status(thm)],[t44863,t19]) ).
cnf(t44929,plain,
composition(join(X1,composition(X1,X2)),top) = composition(X1,top),
inference(orient,[status(thm)],[t44901]) ).
cnf(t44956,plain,
composition(converse(top),join(X1,converse(composition(converse(X1),X2)))) = converse(composition(converse(X1),top)),
inference(cp,[status(thm)],[t38034,t44929]) ).
cnf(t289387,plain,
composition(top,join(X1,converse(composition(converse(X1),X2)))) = converse(composition(converse(X1),top)),
inference(step,[status(thm)],[t44956,t504]) ).
cnf(t289388,plain,
composition(top,join(X1,composition(converse(X2),X1))) = converse(composition(converse(X1),top)),
inference(step,[status(thm)],[t289387,t171]) ).
cnf(t289389,plain,
composition(top,join(X1,composition(converse(X2),X1))) = composition(converse(top),X1),
inference(step,[status(thm)],[t289388,t171]) ).
cnf(t289390,plain,
composition(top,join(X1,composition(converse(X2),X1))) = composition(top,X1),
inference(step,[status(thm)],[t289389,t504]) ).
cnf(t56140,plain,
composition(top,join(X1,composition(converse(X2),X1))) = composition(top,X1),
inference(orient,[status(thm)],[t289390]) ).
cnf(t56178,plain,
composition(top,X1) = composition(top,join(X1,composition(X2,X1))),
inference(cp,[status(thm)],[t56140,t19]) ).
cnf(t56224,plain,
composition(top,join(X1,composition(X2,X1))) = composition(top,X1),
inference(orient,[status(thm)],[t56178]) ).
cnf(t88771,plain,
composition(X1,X2) = meet(composition(X1,X2),composition(top,X2)),
inference(cp,[status(thm)],[t88769,t56224]) ).
cnf(t92985,plain,
meet(composition(X1,X2),composition(top,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t88771]) ).
cnf(t93011,plain,
zero = meet(complement(composition(top,X1)),composition(X2,X1)),
inference(cp,[status(thm)],[t968,t92985]) ).
cnf(t101003,plain,
meet(complement(composition(top,X1)),composition(X2,X1)) = zero,
inference(orient,[status(thm)],[t93011]) ).
cnf(t102954,plain,
composition(complement(composition(top,sk1)),sk1) = zero,
inference(cp,[status(thm)],[t102953,t101003]) ).
cnf(t106550,plain,
composition(complement(composition(top,sk1)),sk1) = zero,
inference(orient,[status(thm)],[t102954]) ).
cnf(t106565,plain,
converse(complement(complement(composition(top,sk1)))) = join(converse(complement(complement(composition(top,sk1)))),composition(sk1,converse(complement(zero)))),
inference(cp,[status(thm)],[t28969,t106550]) ).
cnf(t290094,plain,
converse(composition(top,sk1)) = join(converse(complement(complement(composition(top,sk1)))),composition(sk1,converse(complement(zero)))),
inference(step,[status(thm)],[t106565,t346]) ).
cnf(t290095,plain,
composition(converse(sk1),top) = join(converse(complement(complement(composition(top,sk1)))),composition(sk1,converse(complement(zero)))),
inference(step,[status(thm)],[t290094,t536]) ).
cnf(t290096,plain,
composition(converse(sk1),top) = join(composition(sk1,converse(complement(zero))),converse(complement(complement(composition(top,sk1))))),
inference(step,[status(thm)],[t290095,t20]) ).
cnf(t290097,plain,
composition(converse(sk1),top) = join(composition(sk1,converse(top)),converse(complement(complement(composition(top,sk1))))),
inference(step,[status(thm)],[t290096,t329]) ).
cnf(t290098,plain,
composition(converse(sk1),top) = join(composition(sk1,top),converse(complement(complement(composition(top,sk1))))),
inference(step,[status(thm)],[t290097,t504]) ).
cnf(t290099,plain,
composition(converse(sk1),top) = join(composition(sk1,top),converse(composition(top,sk1))),
inference(step,[status(thm)],[t290098,t346]) ).
cnf(t290100,plain,
composition(converse(sk1),top) = join(composition(sk1,top),composition(converse(sk1),top)),
inference(step,[status(thm)],[t290099,t536]) ).
cnf(t290101,plain,
composition(converse(sk1),top) = composition(join(sk1,converse(sk1)),top),
inference(step,[status(thm)],[t290100,t28]) ).
cnf(t205,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t28,t204]) ).
cnf(t101974,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t205]) ).
cnf(t102801,plain,
join(X1,composition(composition(one,sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t101974,t102660]) ).
cnf(t289824,plain,
join(X1,composition(one,composition(sk1,X1))) = composition(one,X1),
inference(step,[status(thm)],[t102801,t51]) ).
cnf(t289825,plain,
join(X1,composition(sk1,X1)) = composition(one,X1),
inference(step,[status(thm)],[t289824,t204]) ).
cnf(t289826,plain,
join(X1,composition(sk1,X1)) = X1,
inference(step,[status(thm)],[t289825,t204]) ).
cnf(t102802,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t289826]) ).
cnf(t102820,plain,
composition(sk1,X1) = meet(composition(sk1,X1),X1),
inference(cp,[status(thm)],[t719,t102802]) ).
cnf(t289828,plain,
composition(sk1,X1) = meet(X1,composition(sk1,X1)),
inference(step,[status(thm)],[t102820,t74]) ).
cnf(t103438,plain,
meet(X1,composition(sk1,X1)) = composition(sk1,X1),
inference(orient,[status(thm)],[t289828]) ).
cnf(t87264,plain,
meet(X1,converse(composition(top,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t12548,t87170]) ).
cnf(t289702,plain,
meet(X1,composition(converse(converse(X1)),top)) = converse(converse(X1)),
inference(step,[status(thm)],[t87264,t536]) ).
cnf(t289703,plain,
meet(X1,composition(X1,top)) = converse(converse(X1)),
inference(step,[status(thm)],[t289702,t19]) ).
cnf(t289704,plain,
meet(X1,composition(X1,top)) = X1,
inference(step,[status(thm)],[t289703,t19]) ).
cnf(t87341,plain,
meet(X1,composition(X1,top)) = X1,
inference(orient,[status(thm)],[t289704]) ).
cnf(t87402,plain,
meet(X1,composition(join(X2,X1),top)) = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t47557,t87341]) ).
cnf(t289726,plain,
meet(X1,composition(join(X2,X1),top)) = X1,
inference(step,[status(thm)],[t87402,t719]) ).
cnf(t89779,plain,
meet(X1,composition(join(X2,X1),top)) = X1,
inference(orient,[status(thm)],[t289726]) ).
cnf(t89782,plain,
composition(X1,X2) = meet(composition(X1,X2),composition(X1,top)),
inference(cp,[status(thm)],[t89779,t44929]) ).
cnf(t93032,plain,
meet(composition(X1,X2),composition(X1,top)) = composition(X1,X2),
inference(orient,[status(thm)],[t89782]) ).
cnf(t93056,plain,
zero = meet(complement(composition(X1,top)),composition(X1,X2)),
inference(cp,[status(thm)],[t968,t93032]) ).
cnf(t101069,plain,
meet(complement(composition(X1,top)),composition(X1,X2)) = zero,
inference(orient,[status(thm)],[t93056]) ).
cnf(t103439,plain,
composition(sk1,complement(composition(sk1,top))) = zero,
inference(cp,[status(thm)],[t103438,t101069]) ).
cnf(t106593,plain,
composition(sk1,complement(composition(sk1,top))) = zero,
inference(orient,[status(thm)],[t103439]) ).
cnf(t106605,plain,
complement(complement(composition(sk1,top))) = join(complement(complement(composition(sk1,top))),composition(converse(sk1),complement(zero))),
inference(cp,[status(thm)],[t31,t106593]) ).
cnf(t289902,plain,
composition(sk1,top) = join(complement(complement(composition(sk1,top))),composition(converse(sk1),complement(zero))),
inference(step,[status(thm)],[t106605,t346]) ).
cnf(t289903,plain,
composition(sk1,top) = join(composition(converse(sk1),complement(zero)),complement(complement(composition(sk1,top)))),
inference(step,[status(thm)],[t289902,t20]) ).
cnf(t289904,plain,
composition(sk1,top) = join(composition(converse(sk1),top),complement(complement(composition(sk1,top)))),
inference(step,[status(thm)],[t289903,t329]) ).
cnf(t289905,plain,
composition(sk1,top) = join(composition(converse(sk1),top),composition(sk1,top)),
inference(step,[status(thm)],[t289904,t346]) ).
cnf(t289906,plain,
composition(sk1,top) = composition(join(converse(sk1),sk1),top),
inference(step,[status(thm)],[t289905,t28]) ).
cnf(t289907,plain,
composition(sk1,top) = composition(join(sk1,converse(sk1)),top),
inference(step,[status(thm)],[t289906,t20]) ).
cnf(t108611,plain,
composition(join(sk1,converse(sk1)),top) = composition(sk1,top),
inference(orient,[status(thm)],[t289907]) ).
cnf(t290102,plain,
composition(converse(sk1),top) = composition(sk1,top),
inference(step,[status(thm)],[t290101,t108611]) ).
cnf(t126500,plain,
composition(converse(sk1),top) = composition(sk1,top),
inference(orient,[status(thm)],[t290102]) ).
cnf(t291618,plain,
meet(X1,composition(sk1,top)) = converse(composition(converse(X1),sk1)),
inference(step,[status(thm)],[t291617,t126500]) ).
cnf(t291619,plain,
meet(X1,composition(sk1,top)) = composition(converse(sk1),X1),
inference(step,[status(thm)],[t291618,t171]) ).
cnf(t12558,plain,
meet(X1,converse(X2)) = converse(meet(X2,converse(X1))),
inference(cp,[status(thm)],[t12548,t74]) ).
cnf(t12614,plain,
converse(meet(X1,converse(X2))) = meet(X2,converse(X1)),
inference(orient,[status(thm)],[t12558]) ).
cnf(t9174,plain,
meet(complement(X1),X2) = meet(complement(X1),join(X1,X2)),
inference(cp,[status(thm)],[t9135,t346]) ).
cnf(t10457,plain,
meet(complement(X1),join(X1,X2)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t9174]) ).
cnf(t43,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t22,t42]) ).
cnf(t82,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t43]) ).
cnf(t84,plain,
join(one,X1) = join(sk1,join(X1,one)),
inference(cp,[status(thm)],[t82,t20]) ).
cnf(t119,plain,
join(sk1,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t84]) ).
cnf(t651,plain,
top = join(one,complement(sk1)),
inference(cp,[status(thm)],[t650,t119]) ).
cnf(t664,plain,
join(one,complement(sk1)) = top,
inference(orient,[status(thm)],[t651]) ).
cnf(t667,plain,
join(one,join(complement(sk1),X1)) = join(top,X1),
inference(cp,[status(thm)],[t22,t664]) ).
cnf(t288571,plain,
join(one,join(complement(sk1),X1)) = top,
inference(step,[status(thm)],[t667,t486]) ).
cnf(t778,plain,
join(one,join(complement(sk1),X1)) = top,
inference(orient,[status(thm)],[t288571]) ).
cnf(t8855,plain,
join(join(complement(sk1),X1),complement(one)) = join(join(complement(sk1),X1),complement(top)),
inference(cp,[status(thm)],[t8759,t778]) ).
cnf(t288996,plain,
join(complement(sk1),join(X1,complement(one))) = join(join(complement(sk1),X1),complement(top)),
inference(step,[status(thm)],[t8855,t22]) ).
cnf(t288997,plain,
join(complement(sk1),join(X1,complement(one))) = join(complement(sk1),join(X1,complement(top))),
inference(step,[status(thm)],[t288996,t22]) ).
cnf(t288998,plain,
join(complement(sk1),join(X1,complement(one))) = join(complement(top),join(complement(sk1),X1)),
inference(step,[status(thm)],[t288997,t545]) ).
cnf(t288999,plain,
join(complement(sk1),join(X1,complement(one))) = join(zero,join(complement(sk1),X1)),
inference(step,[status(thm)],[t288998,t65]) ).
cnf(t289000,plain,
join(complement(sk1),join(X1,complement(one))) = join(complement(sk1),X1),
inference(step,[status(thm)],[t288999,t316]) ).
cnf(t24285,plain,
join(complement(sk1),join(X1,complement(one))) = join(complement(sk1),X1),
inference(orient,[status(thm)],[t289000]) ).
cnf(t24294,plain,
meet(complement(complement(sk1)),join(X1,complement(one))) = meet(complement(complement(sk1)),join(complement(sk1),X1)),
inference(cp,[status(thm)],[t10457,t24285]) ).
cnf(t289001,plain,
meet(sk1,join(X1,complement(one))) = meet(complement(complement(sk1)),join(complement(sk1),X1)),
inference(step,[status(thm)],[t24294,t346]) ).
cnf(t289002,plain,
meet(sk1,join(X1,complement(one))) = meet(complement(complement(sk1)),X1),
inference(step,[status(thm)],[t289001,t10457]) ).
cnf(t289003,plain,
meet(sk1,join(X1,complement(one))) = meet(sk1,X1),
inference(step,[status(thm)],[t289002,t346]) ).
cnf(t24327,plain,
meet(sk1,join(X1,complement(one))) = meet(sk1,X1),
inference(orient,[status(thm)],[t289003]) ).
cnf(t24331,plain,
meet(sk1,X1) = meet(sk1,join(complement(one),X1)),
inference(cp,[status(thm)],[t24327,t20]) ).
cnf(t24366,plain,
meet(sk1,join(complement(one),X1)) = meet(sk1,X1),
inference(orient,[status(thm)],[t24331]) ).
cnf(t11535,plain,
complement(meet(X1,converse(X2))) = join(complement(X1),converse(complement(X2))),
inference(cp,[status(thm)],[t808,t11513]) ).
cnf(t12849,plain,
join(complement(X1),converse(complement(X2))) = complement(meet(X1,converse(X2))),
inference(orient,[status(thm)],[t11535]) ).
cnf(t24368,plain,
meet(sk1,converse(complement(X1))) = meet(sk1,complement(meet(one,converse(X1)))),
inference(cp,[status(thm)],[t24366,t12849]) ).
cnf(t11628,plain,
converse(complement(meet(one,X1))) = complement(meet(one,converse(X1))),
inference(cp,[status(thm)],[t11513,t11606]) ).
cnf(t11848,plain,
complement(meet(one,converse(X1))) = converse(complement(meet(one,X1))),
inference(orient,[status(thm)],[t11628]) ).
cnf(t289194,plain,
meet(sk1,converse(complement(X1))) = meet(sk1,converse(complement(meet(one,X1)))),
inference(step,[status(thm)],[t24368,t11848]) ).
cnf(t37685,plain,
meet(sk1,converse(complement(meet(one,X1)))) = meet(sk1,converse(complement(X1))),
inference(orient,[status(thm)],[t289194]) ).
cnf(t37732,plain,
meet(complement(meet(one,X1)),converse(sk1)) = converse(meet(sk1,converse(complement(X1)))),
inference(cp,[status(thm)],[t12614,t37685]) ).
cnf(t289220,plain,
meet(converse(sk1),complement(meet(one,X1))) = converse(meet(sk1,converse(complement(X1)))),
inference(step,[status(thm)],[t37732,t74]) ).
cnf(t289221,plain,
meet(converse(sk1),complement(meet(one,X1))) = meet(complement(X1),converse(sk1)),
inference(step,[status(thm)],[t289220,t12614]) ).
cnf(t289222,plain,
meet(converse(sk1),complement(meet(one,X1))) = meet(converse(sk1),complement(X1)),
inference(step,[status(thm)],[t289221,t74]) ).
cnf(t38650,plain,
meet(converse(sk1),complement(meet(one,X1))) = meet(converse(sk1),complement(X1)),
inference(orient,[status(thm)],[t289222]) ).
cnf(t38651,plain,
meet(converse(sk1),complement(complement(X1))) = meet(converse(sk1),join(complement(one),X1)),
inference(cp,[status(thm)],[t38650,t912]) ).
cnf(t289237,plain,
meet(converse(sk1),X1) = meet(converse(sk1),join(complement(one),X1)),
inference(step,[status(thm)],[t38651,t346]) ).
cnf(t39040,plain,
meet(converse(sk1),join(complement(one),X1)) = meet(converse(sk1),X1),
inference(orient,[status(thm)],[t289237]) ).
cnf(t24,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t22,t20]) ).
cnf(t288589,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t24,t22]) ).
cnf(t1043,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t288589]) ).
cnf(t102798,plain,
join(X1,join(X2,composition(X1,sk1))) = join(X2,X1),
inference(cp,[status(thm)],[t1043,t102660]) ).
cnf(t135063,plain,
join(X1,join(X2,composition(X1,sk1))) = join(X2,X1),
inference(orient,[status(thm)],[t102798]) ).
cnf(t102381,plain,
join(X1,composition(complement(one),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t101974,t25]) ).
cnf(t108382,plain,
join(X1,composition(complement(one),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t102381]) ).
cnf(t135135,plain,
join(sk1,complement(one)) = join(complement(one),composition(top,sk1)),
inference(cp,[status(thm)],[t135063,t108382]) ).
cnf(t135332,plain,
join(complement(one),composition(top,sk1)) = join(sk1,complement(one)),
inference(orient,[status(thm)],[t135135]) ).
cnf(t135351,plain,
meet(converse(sk1),composition(top,sk1)) = meet(converse(sk1),join(sk1,complement(one))),
inference(cp,[status(thm)],[t39040,t135332]) ).
cnf(t126513,plain,
composition(top,converse(converse(sk1))) = converse(composition(sk1,top)),
inference(cp,[status(thm)],[t525,t126500]) ).
cnf(t290103,plain,
composition(top,sk1) = converse(composition(sk1,top)),
inference(step,[status(thm)],[t126513,t19]) ).
cnf(t290104,plain,
composition(top,sk1) = composition(top,converse(sk1)),
inference(step,[status(thm)],[t290103,t525]) ).
cnf(t126647,plain,
composition(top,converse(sk1)) = composition(top,sk1),
inference(orient,[status(thm)],[t290104]) ).
cnf(t126657,plain,
converse(sk1) = meet(converse(sk1),composition(top,sk1)),
inference(cp,[status(thm)],[t87170,t126647]) ).
cnf(t127098,plain,
meet(converse(sk1),composition(top,sk1)) = converse(sk1),
inference(orient,[status(thm)],[t126657]) ).
cnf(t290207,plain,
converse(sk1) = meet(converse(sk1),join(sk1,complement(one))),
inference(step,[status(thm)],[t135351,t127098]) ).
cnf(t8565,plain,
meet(X1,complement(meet(complement(complement(X1)),X2))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t1184,t8512]) ).
cnf(t288808,plain,
meet(X1,join(complement(X1),complement(X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t8565,t896]) ).
cnf(t288809,plain,
meet(X1,complement(meet(X1,X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t288808,t808]) ).
cnf(t288810,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t288809,t1184]) ).
cnf(t10059,plain,
meet(X1,complement(meet(X1,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t288810]) ).
cnf(t38666,plain,
meet(converse(sk1),complement(complement(meet(one,X1)))) = meet(converse(sk1),complement(meet(one,complement(X1)))),
inference(cp,[status(thm)],[t38650,t10059]) ).
cnf(t289226,plain,
meet(converse(sk1),meet(one,X1)) = meet(converse(sk1),complement(meet(one,complement(X1)))),
inference(step,[status(thm)],[t38666,t346]) ).
cnf(t289227,plain,
meet(converse(sk1),meet(one,X1)) = meet(converse(sk1),complement(complement(X1))),
inference(step,[status(thm)],[t289226,t38650]) ).
cnf(t289228,plain,
meet(converse(sk1),meet(one,X1)) = meet(converse(sk1),X1),
inference(step,[status(thm)],[t289227,t346]) ).
cnf(t38775,plain,
meet(converse(sk1),meet(one,X1)) = meet(converse(sk1),X1),
inference(orient,[status(thm)],[t289228]) ).
cnf(t38790,plain,
meet(converse(sk1),join(X1,complement(one))) = meet(converse(sk1),meet(one,X1)),
inference(cp,[status(thm)],[t38775,t9077]) ).
cnf(t289238,plain,
meet(converse(sk1),join(X1,complement(one))) = meet(converse(sk1),X1),
inference(step,[status(thm)],[t38790,t38775]) ).
cnf(t39097,plain,
meet(converse(sk1),join(X1,complement(one))) = meet(converse(sk1),X1),
inference(orient,[status(thm)],[t289238]) ).
cnf(t290208,plain,
converse(sk1) = meet(converse(sk1),sk1),
inference(step,[status(thm)],[t290207,t39097]) ).
cnf(t290209,plain,
converse(sk1) = meet(sk1,converse(sk1)),
inference(step,[status(thm)],[t290208,t74]) ).
cnf(t135382,plain,
meet(sk1,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t290209]) ).
cnf(t135431,plain,
meet(sk1,converse(sk1)) = converse(converse(sk1)),
inference(cp,[status(thm)],[t12614,t135382]) ).
cnf(t290210,plain,
converse(sk1) = converse(converse(sk1)),
inference(step,[status(thm)],[t135431,t135382]) ).
cnf(t290211,plain,
converse(sk1) = sk1,
inference(step,[status(thm)],[t290210,t19]) ).
cnf(t135459,plain,
converse(sk1) = sk1,
inference(orient,[status(thm)],[t290211]) ).
cnf(t291620,plain,
meet(X1,composition(sk1,top)) = composition(sk1,X1),
inference(step,[status(thm)],[t291619,t135459]) ).
cnf(t283058,plain,
meet(X1,composition(sk1,top)) = composition(sk1,X1),
inference(orient,[status(thm)],[t291620]) ).
cnf(t283060,plain,
composition(sk1,X1) = meet(composition(sk1,top),X1),
inference(cp,[status(thm)],[t283058,t74]) ).
cnf(t283652,plain,
meet(composition(sk1,top),X1) = composition(sk1,X1),
inference(orient,[status(thm)],[t283060]) ).
cnf(t283779,plain,
meet(composition(sk1,top),meet(X1,X2)) = meet(composition(sk1,X1),X2),
inference(cp,[status(thm)],[t53078,t283652]) ).
cnf(t291680,plain,
composition(sk1,meet(X1,X2)) = meet(composition(sk1,X1),X2),
inference(step,[status(thm)],[t283779,t283652]) ).
cnf(t283059,plain,
composition(sk1,meet(X1,X2)) = meet(X1,meet(X2,composition(sk1,top))),
inference(cp,[status(thm)],[t283058,t53078]) ).
cnf(t291671,plain,
composition(sk1,meet(X1,X2)) = meet(X1,composition(sk1,X2)),
inference(step,[status(thm)],[t283059,t283058]) ).
cnf(t287205,plain,
composition(sk1,meet(X1,X2)) = meet(X1,composition(sk1,X2)),
inference(orient,[status(thm)],[t291671]) ).
cnf(t291681,plain,
meet(X1,composition(sk1,X2)) = meet(composition(sk1,X1),X2),
inference(step,[status(thm)],[t291680,t287205]) ).
cnf(t287938,plain,
meet(composition(sk1,X1),X2) = meet(X1,composition(sk1,X2)),
inference(orient,[status(thm)],[t291681]) ).
cnf(t196,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t35,t193]) ).
cnf(t208,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t196]) ).
cnf(c13,plain,
join(sk0,one) = one,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t2,plain,
join(sk0,one) = one,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t40,plain,
join(sk0,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t221,plain,
join(one,converse(sk0)) = converse(one),
inference(cp,[status(thm)],[t218,t40]) ).
cnf(t288497,plain,
join(one,converse(sk0)) = one,
inference(step,[status(thm)],[t221,t193]) ).
cnf(t237,plain,
join(one,converse(sk0)) = one,
inference(orient,[status(thm)],[t288497]) ).
cnf(t239,plain,
join(one,join(converse(sk0),X1)) = join(one,X1),
inference(cp,[status(thm)],[t22,t237]) ).
cnf(t1281,plain,
join(one,join(converse(sk0),X1)) = join(one,X1),
inference(orient,[status(thm)],[t239]) ).
cnf(t517,plain,
join(X1,converse(meet(converse(X1),X2))) = converse(converse(X1)),
inference(cp,[status(thm)],[t140,t512]) ).
cnf(t288602,plain,
join(X1,converse(meet(converse(X1),X2))) = X1,
inference(step,[status(thm)],[t517,t19]) ).
cnf(t1363,plain,
join(X1,converse(meet(converse(X1),X2))) = X1,
inference(orient,[status(thm)],[t288602]) ).
cnf(t1379,plain,
join(one,converse(meet(converse(converse(sk0)),X1))) = join(one,converse(sk0)),
inference(cp,[status(thm)],[t1281,t1363]) ).
cnf(t288603,plain,
join(one,converse(meet(sk0,X1))) = join(one,converse(sk0)),
inference(step,[status(thm)],[t1379,t19]) ).
cnf(t288604,plain,
join(one,converse(meet(sk0,X1))) = one,
inference(step,[status(thm)],[t288603,t237]) ).
cnf(t1386,plain,
join(one,converse(meet(sk0,X1))) = one,
inference(orient,[status(thm)],[t288604]) ).
cnf(t1390,plain,
join(one,converse(converse(meet(sk0,X1)))) = converse(one),
inference(cp,[status(thm)],[t208,t1386]) ).
cnf(t288605,plain,
join(one,meet(sk0,X1)) = converse(one),
inference(step,[status(thm)],[t1390,t19]) ).
cnf(t288606,plain,
join(one,meet(sk0,X1)) = one,
inference(step,[status(thm)],[t288605,t193]) ).
cnf(t1397,plain,
join(one,meet(sk0,X1)) = one,
inference(orient,[status(thm)],[t288606]) ).
cnf(t103470,plain,
one = join(one,composition(sk1,sk0)),
inference(cp,[status(thm)],[t1397,t103438]) ).
cnf(t103788,plain,
join(one,composition(sk1,sk0)) = one,
inference(orient,[status(thm)],[t103470]) ).
cnf(t103853,plain,
join(X1,composition(composition(sk1,sk0),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t101974,t103788]) ).
cnf(t289971,plain,
join(X1,composition(sk1,composition(sk0,X1))) = composition(one,X1),
inference(step,[status(thm)],[t103853,t51]) ).
cnf(t289972,plain,
join(X1,composition(sk1,composition(sk0,X1))) = X1,
inference(step,[status(thm)],[t289971,t204]) ).
cnf(t114996,plain,
join(X1,composition(sk1,composition(sk0,X1))) = X1,
inference(orient,[status(thm)],[t289972]) ).
cnf(t115013,plain,
composition(sk1,composition(sk0,X1)) = meet(composition(sk1,composition(sk0,X1)),X1),
inference(cp,[status(thm)],[t719,t114996]) ).
cnf(t291489,plain,
composition(sk1,composition(sk0,X1)) = meet(X1,composition(sk1,composition(sk0,X1))),
inference(step,[status(thm)],[t115013,t74]) ).
cnf(t269090,plain,
meet(X1,composition(sk1,composition(sk0,X1))) = composition(sk1,composition(sk0,X1)),
inference(orient,[status(thm)],[t291489]) ).
cnf(t12575,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(cp,[status(thm)],[t12548,t19]) ).
cnf(t12698,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(orient,[status(thm)],[t12575]) ).
cnf(t41,plain,
join(sk0,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t22,t40]) ).
cnf(t77,plain,
join(sk0,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t79,plain,
join(one,X1) = join(sk0,join(X1,one)),
inference(cp,[status(thm)],[t77,t20]) ).
cnf(t108,plain,
join(sk0,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t79]) ).
cnf(t652,plain,
top = join(one,complement(sk0)),
inference(cp,[status(thm)],[t650,t108]) ).
cnf(t670,plain,
join(one,complement(sk0)) = top,
inference(orient,[status(thm)],[t652]) ).
cnf(t673,plain,
join(one,join(complement(sk0),X1)) = join(top,X1),
inference(cp,[status(thm)],[t22,t670]) ).
cnf(t288572,plain,
join(one,join(complement(sk0),X1)) = top,
inference(step,[status(thm)],[t673,t486]) ).
cnf(t785,plain,
join(one,join(complement(sk0),X1)) = top,
inference(orient,[status(thm)],[t288572]) ).
cnf(t8856,plain,
join(join(complement(sk0),X1),complement(one)) = join(join(complement(sk0),X1),complement(top)),
inference(cp,[status(thm)],[t8759,t785]) ).
cnf(t289031,plain,
join(complement(sk0),join(X1,complement(one))) = join(join(complement(sk0),X1),complement(top)),
inference(step,[status(thm)],[t8856,t22]) ).
cnf(t289032,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),join(X1,complement(top))),
inference(step,[status(thm)],[t289031,t22]) ).
cnf(t289033,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(top),join(complement(sk0),X1)),
inference(step,[status(thm)],[t289032,t545]) ).
cnf(t289034,plain,
join(complement(sk0),join(X1,complement(one))) = join(zero,join(complement(sk0),X1)),
inference(step,[status(thm)],[t289033,t65]) ).
cnf(t289035,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(step,[status(thm)],[t289034,t316]) ).
cnf(t26500,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(orient,[status(thm)],[t289035]) ).
cnf(t26509,plain,
meet(complement(complement(sk0)),join(X1,complement(one))) = meet(complement(complement(sk0)),join(complement(sk0),X1)),
inference(cp,[status(thm)],[t10457,t26500]) ).
cnf(t289036,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),join(complement(sk0),X1)),
inference(step,[status(thm)],[t26509,t346]) ).
cnf(t289037,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),X1),
inference(step,[status(thm)],[t289036,t10457]) ).
cnf(t289038,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(step,[status(thm)],[t289037,t346]) ).
cnf(t26542,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(orient,[status(thm)],[t289038]) ).
cnf(t26546,plain,
meet(sk0,X1) = meet(sk0,join(complement(one),X1)),
inference(cp,[status(thm)],[t26542,t20]) ).
cnf(t26581,plain,
meet(sk0,join(complement(one),X1)) = meet(sk0,X1),
inference(orient,[status(thm)],[t26546]) ).
cnf(t26583,plain,
meet(sk0,converse(complement(X1))) = meet(sk0,complement(meet(one,converse(X1)))),
inference(cp,[status(thm)],[t26581,t12849]) ).
cnf(t289208,plain,
meet(sk0,converse(complement(X1))) = meet(sk0,converse(complement(meet(one,X1)))),
inference(step,[status(thm)],[t26583,t11848]) ).
cnf(t38170,plain,
meet(sk0,converse(complement(meet(one,X1)))) = meet(sk0,converse(complement(X1))),
inference(orient,[status(thm)],[t289208]) ).
cnf(t38217,plain,
meet(complement(meet(one,X1)),converse(sk0)) = converse(meet(sk0,converse(complement(X1)))),
inference(cp,[status(thm)],[t12614,t38170]) ).
cnf(t289244,plain,
meet(converse(sk0),complement(meet(one,X1))) = converse(meet(sk0,converse(complement(X1)))),
inference(step,[status(thm)],[t38217,t74]) ).
cnf(t289245,plain,
meet(converse(sk0),complement(meet(one,X1))) = meet(complement(X1),converse(sk0)),
inference(step,[status(thm)],[t289244,t12614]) ).
cnf(t289246,plain,
meet(converse(sk0),complement(meet(one,X1))) = meet(converse(sk0),complement(X1)),
inference(step,[status(thm)],[t289245,t74]) ).
cnf(t39205,plain,
meet(converse(sk0),complement(meet(one,X1))) = meet(converse(sk0),complement(X1)),
inference(orient,[status(thm)],[t289246]) ).
cnf(t39206,plain,
meet(converse(sk0),complement(complement(X1))) = meet(converse(sk0),join(complement(one),X1)),
inference(cp,[status(thm)],[t39205,t912]) ).
cnf(t289261,plain,
meet(converse(sk0),X1) = meet(converse(sk0),join(complement(one),X1)),
inference(step,[status(thm)],[t39206,t346]) ).
cnf(t39595,plain,
meet(converse(sk0),join(complement(one),X1)) = meet(converse(sk0),X1),
inference(orient,[status(thm)],[t289261]) ).
cnf(t728,plain,
converse(sk0) = meet(converse(sk0),one),
inference(cp,[status(thm)],[t719,t237]) ).
cnf(t288568,plain,
converse(sk0) = meet(one,converse(sk0)),
inference(step,[status(thm)],[t728,t74]) ).
cnf(t740,plain,
meet(one,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t288568]) ).
cnf(t101655,plain,
X1 = join(X1,composition(converse(sk0),X1)),
inference(cp,[status(thm)],[t101620,t740]) ).
cnf(t104046,plain,
join(X1,composition(converse(sk0),X1)) = X1,
inference(orient,[status(thm)],[t101655]) ).
cnf(t104145,plain,
join(X1,converse(composition(converse(sk0),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t140,t104046]) ).
cnf(t289835,plain,
join(X1,composition(converse(converse(X1)),sk0)) = converse(converse(X1)),
inference(step,[status(thm)],[t104145,t171]) ).
cnf(t289836,plain,
join(X1,composition(X1,sk0)) = converse(converse(X1)),
inference(step,[status(thm)],[t289835,t19]) ).
cnf(t289837,plain,
join(X1,composition(X1,sk0)) = X1,
inference(step,[status(thm)],[t289836,t19]) ).
cnf(t104205,plain,
join(X1,composition(X1,sk0)) = X1,
inference(orient,[status(thm)],[t289837]) ).
cnf(t104344,plain,
join(X1,join(X2,composition(X1,sk0))) = join(X2,X1),
inference(cp,[status(thm)],[t1043,t104205]) ).
cnf(t147487,plain,
join(X1,join(X2,composition(X1,sk0))) = join(X2,X1),
inference(orient,[status(thm)],[t104344]) ).
cnf(t147550,plain,
join(sk0,complement(one)) = join(complement(one),composition(top,sk0)),
inference(cp,[status(thm)],[t147487,t108382]) ).
cnf(t147738,plain,
join(complement(one),composition(top,sk0)) = join(sk0,complement(one)),
inference(orient,[status(thm)],[t147550]) ).
cnf(t147760,plain,
meet(converse(sk0),composition(top,sk0)) = meet(converse(sk0),join(sk0,complement(one))),
inference(cp,[status(thm)],[t39595,t147738]) ).
cnf(t104225,plain,
composition(X1,sk0) = meet(composition(X1,sk0),X1),
inference(cp,[status(thm)],[t719,t104205]) ).
cnf(t289841,plain,
composition(X1,sk0) = meet(X1,composition(X1,sk0)),
inference(step,[status(thm)],[t104225,t74]) ).
cnf(t104500,plain,
meet(X1,composition(X1,sk0)) = composition(X1,sk0),
inference(orient,[status(thm)],[t289841]) ).
cnf(t104501,plain,
composition(complement(composition(top,sk0)),sk0) = zero,
inference(cp,[status(thm)],[t104500,t101003]) ).
cnf(t107961,plain,
composition(complement(composition(top,sk0)),sk0) = zero,
inference(orient,[status(thm)],[t104501]) ).
cnf(t107976,plain,
converse(complement(complement(composition(top,sk0)))) = join(converse(complement(complement(composition(top,sk0)))),composition(sk0,converse(complement(zero)))),
inference(cp,[status(thm)],[t28969,t107961]) ).
cnf(t290109,plain,
converse(composition(top,sk0)) = join(converse(complement(complement(composition(top,sk0)))),composition(sk0,converse(complement(zero)))),
inference(step,[status(thm)],[t107976,t346]) ).
cnf(t290110,plain,
composition(converse(sk0),top) = join(converse(complement(complement(composition(top,sk0)))),composition(sk0,converse(complement(zero)))),
inference(step,[status(thm)],[t290109,t536]) ).
cnf(t290111,plain,
composition(converse(sk0),top) = join(composition(sk0,converse(complement(zero))),converse(complement(complement(composition(top,sk0))))),
inference(step,[status(thm)],[t290110,t20]) ).
cnf(t290112,plain,
composition(converse(sk0),top) = join(composition(sk0,converse(top)),converse(complement(complement(composition(top,sk0))))),
inference(step,[status(thm)],[t290111,t329]) ).
cnf(t290113,plain,
composition(converse(sk0),top) = join(composition(sk0,top),converse(complement(complement(composition(top,sk0))))),
inference(step,[status(thm)],[t290112,t504]) ).
cnf(t290114,plain,
composition(converse(sk0),top) = join(composition(sk0,top),converse(composition(top,sk0))),
inference(step,[status(thm)],[t290113,t346]) ).
cnf(t290115,plain,
composition(converse(sk0),top) = join(composition(sk0,top),composition(converse(sk0),top)),
inference(step,[status(thm)],[t290114,t536]) ).
cnf(t290116,plain,
composition(converse(sk0),top) = composition(join(sk0,converse(sk0)),top),
inference(step,[status(thm)],[t290115,t28]) ).
cnf(t104347,plain,
join(X1,composition(composition(one,sk0),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t101974,t104205]) ).
cnf(t289838,plain,
join(X1,composition(one,composition(sk0,X1))) = composition(one,X1),
inference(step,[status(thm)],[t104347,t51]) ).
cnf(t289839,plain,
join(X1,composition(sk0,X1)) = composition(one,X1),
inference(step,[status(thm)],[t289838,t204]) ).
cnf(t289840,plain,
join(X1,composition(sk0,X1)) = X1,
inference(step,[status(thm)],[t289839,t204]) ).
cnf(t104348,plain,
join(X1,composition(sk0,X1)) = X1,
inference(orient,[status(thm)],[t289840]) ).
cnf(t104367,plain,
composition(sk0,X1) = meet(composition(sk0,X1),X1),
inference(cp,[status(thm)],[t719,t104348]) ).
cnf(t289842,plain,
composition(sk0,X1) = meet(X1,composition(sk0,X1)),
inference(step,[status(thm)],[t104367,t74]) ).
cnf(t104910,plain,
meet(X1,composition(sk0,X1)) = composition(sk0,X1),
inference(orient,[status(thm)],[t289842]) ).
cnf(t104911,plain,
composition(sk0,complement(composition(sk0,top))) = zero,
inference(cp,[status(thm)],[t104910,t101069]) ).
cnf(t107992,plain,
composition(sk0,complement(composition(sk0,top))) = zero,
inference(orient,[status(thm)],[t104911]) ).
cnf(t108004,plain,
complement(complement(composition(sk0,top))) = join(complement(complement(composition(sk0,top))),composition(converse(sk0),complement(zero))),
inference(cp,[status(thm)],[t31,t107992]) ).
cnf(t289910,plain,
composition(sk0,top) = join(complement(complement(composition(sk0,top))),composition(converse(sk0),complement(zero))),
inference(step,[status(thm)],[t108004,t346]) ).
cnf(t289911,plain,
composition(sk0,top) = join(composition(converse(sk0),complement(zero)),complement(complement(composition(sk0,top)))),
inference(step,[status(thm)],[t289910,t20]) ).
cnf(t289912,plain,
composition(sk0,top) = join(composition(converse(sk0),top),complement(complement(composition(sk0,top)))),
inference(step,[status(thm)],[t289911,t329]) ).
cnf(t289913,plain,
composition(sk0,top) = join(composition(converse(sk0),top),composition(sk0,top)),
inference(step,[status(thm)],[t289912,t346]) ).
cnf(t289914,plain,
composition(sk0,top) = composition(join(converse(sk0),sk0),top),
inference(step,[status(thm)],[t289913,t28]) ).
cnf(t289915,plain,
composition(sk0,top) = composition(join(sk0,converse(sk0)),top),
inference(step,[status(thm)],[t289914,t20]) ).
cnf(t108828,plain,
composition(join(sk0,converse(sk0)),top) = composition(sk0,top),
inference(orient,[status(thm)],[t289915]) ).
cnf(t290117,plain,
composition(converse(sk0),top) = composition(sk0,top),
inference(step,[status(thm)],[t290116,t108828]) ).
cnf(t127236,plain,
composition(converse(sk0),top) = composition(sk0,top),
inference(orient,[status(thm)],[t290117]) ).
cnf(t127249,plain,
composition(top,converse(converse(sk0))) = converse(composition(sk0,top)),
inference(cp,[status(thm)],[t525,t127236]) ).
cnf(t290118,plain,
composition(top,sk0) = converse(composition(sk0,top)),
inference(step,[status(thm)],[t127249,t19]) ).
cnf(t290119,plain,
composition(top,sk0) = composition(top,converse(sk0)),
inference(step,[status(thm)],[t290118,t525]) ).
cnf(t127315,plain,
composition(top,converse(sk0)) = composition(top,sk0),
inference(orient,[status(thm)],[t290119]) ).
cnf(t127325,plain,
converse(sk0) = meet(converse(sk0),composition(top,sk0)),
inference(cp,[status(thm)],[t87170,t127315]) ).
cnf(t127766,plain,
meet(converse(sk0),composition(top,sk0)) = converse(sk0),
inference(orient,[status(thm)],[t127325]) ).
cnf(t290299,plain,
converse(sk0) = meet(converse(sk0),join(sk0,complement(one))),
inference(step,[status(thm)],[t147760,t127766]) ).
cnf(t39221,plain,
meet(converse(sk0),complement(complement(meet(one,X1)))) = meet(converse(sk0),complement(meet(one,complement(X1)))),
inference(cp,[status(thm)],[t39205,t10059]) ).
cnf(t289250,plain,
meet(converse(sk0),meet(one,X1)) = meet(converse(sk0),complement(meet(one,complement(X1)))),
inference(step,[status(thm)],[t39221,t346]) ).
cnf(t289251,plain,
meet(converse(sk0),meet(one,X1)) = meet(converse(sk0),complement(complement(X1))),
inference(step,[status(thm)],[t289250,t39205]) ).
cnf(t289252,plain,
meet(converse(sk0),meet(one,X1)) = meet(converse(sk0),X1),
inference(step,[status(thm)],[t289251,t346]) ).
cnf(t39330,plain,
meet(converse(sk0),meet(one,X1)) = meet(converse(sk0),X1),
inference(orient,[status(thm)],[t289252]) ).
cnf(t39345,plain,
meet(converse(sk0),join(X1,complement(one))) = meet(converse(sk0),meet(one,X1)),
inference(cp,[status(thm)],[t39330,t9077]) ).
cnf(t289262,plain,
meet(converse(sk0),join(X1,complement(one))) = meet(converse(sk0),X1),
inference(step,[status(thm)],[t39345,t39330]) ).
cnf(t39652,plain,
meet(converse(sk0),join(X1,complement(one))) = meet(converse(sk0),X1),
inference(orient,[status(thm)],[t289262]) ).
cnf(t290300,plain,
converse(sk0) = meet(converse(sk0),sk0),
inference(step,[status(thm)],[t290299,t39652]) ).
cnf(t290301,plain,
converse(sk0) = meet(sk0,converse(sk0)),
inference(step,[status(thm)],[t290300,t74]) ).
cnf(t147792,plain,
meet(sk0,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t290301]) ).
cnf(t147841,plain,
meet(sk0,converse(sk0)) = converse(converse(sk0)),
inference(cp,[status(thm)],[t12614,t147792]) ).
cnf(t290302,plain,
converse(sk0) = converse(converse(sk0)),
inference(step,[status(thm)],[t147841,t147792]) ).
cnf(t290303,plain,
converse(sk0) = sk0,
inference(step,[status(thm)],[t290302,t19]) ).
cnf(t147869,plain,
converse(sk0) = sk0,
inference(orient,[status(thm)],[t290303]) ).
cnf(t147870,plain,
converse(meet(sk0,X1)) = meet(sk0,converse(X1)),
inference(cp,[status(thm)],[t12698,t147869]) ).
cnf(t148224,plain,
converse(meet(sk0,X1)) = meet(sk0,converse(X1)),
inference(orient,[status(thm)],[t147870]) ).
cnf(t282066,plain,
meet(sk0,converse(composition(top,sk1))) = converse(composition(sk0,sk1)),
inference(cp,[status(thm)],[t148224,t282038]) ).
cnf(t291579,plain,
meet(sk0,composition(converse(sk1),top)) = converse(composition(sk0,sk1)),
inference(step,[status(thm)],[t282066,t536]) ).
cnf(t291580,plain,
meet(sk0,composition(sk1,top)) = converse(composition(sk0,sk1)),
inference(step,[status(thm)],[t291579,t126500]) ).
cnf(t26585,plain,
meet(sk0,meet(one,X1)) = meet(sk0,join(complement(one),X1)),
inference(cp,[status(thm)],[t26581,t9964]) ).
cnf(t289040,plain,
meet(sk0,meet(one,X1)) = meet(sk0,X1),
inference(step,[status(thm)],[t26585,t26581]) ).
cnf(t26681,plain,
meet(sk0,meet(one,X1)) = meet(sk0,X1),
inference(orient,[status(thm)],[t289040]) ).
cnf(t135334,plain,
meet(complement(complement(one)),composition(top,sk1)) = meet(complement(complement(one)),join(sk1,complement(one))),
inference(cp,[status(thm)],[t10457,t135332]) ).
cnf(t290251,plain,
meet(composition(top,sk1),complement(complement(one))) = meet(complement(complement(one)),join(sk1,complement(one))),
inference(step,[status(thm)],[t135334,t74]) ).
cnf(t290252,plain,
meet(composition(top,sk1),one) = meet(complement(complement(one)),join(sk1,complement(one))),
inference(step,[status(thm)],[t290251,t346]) ).
cnf(t290253,plain,
meet(one,composition(top,sk1)) = meet(complement(complement(one)),join(sk1,complement(one))),
inference(step,[status(thm)],[t290252,t74]) ).
cnf(t8908,plain,
meet(complement(X1),join(X2,X1)) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t928,t8759]) ).
cnf(t288814,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(step,[status(thm)],[t8908,t928]) ).
cnf(t10261,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t288814]) ).
cnf(t290254,plain,
meet(one,composition(top,sk1)) = meet(complement(complement(one)),sk1),
inference(step,[status(thm)],[t290253,t10261]) ).
cnf(t290255,plain,
meet(one,composition(top,sk1)) = meet(sk1,complement(complement(one))),
inference(step,[status(thm)],[t290254,t74]) ).
cnf(t290256,plain,
meet(one,composition(top,sk1)) = meet(sk1,one),
inference(step,[status(thm)],[t290255,t346]) ).
cnf(t678,plain,
sk1 = meet(sk1,one),
inference(cp,[status(thm)],[t676,t42]) ).
cnf(t691,plain,
meet(sk1,one) = sk1,
inference(orient,[status(thm)],[t678]) ).
cnf(t290257,plain,
meet(one,composition(top,sk1)) = sk1,
inference(step,[status(thm)],[t290256,t691]) ).
cnf(t137028,plain,
meet(one,composition(top,sk1)) = sk1,
inference(orient,[status(thm)],[t290257]) ).
cnf(t137045,plain,
meet(one,converse(composition(top,sk1))) = converse(sk1),
inference(cp,[status(thm)],[t11606,t137028]) ).
cnf(t290258,plain,
meet(one,composition(converse(sk1),top)) = converse(sk1),
inference(step,[status(thm)],[t137045,t536]) ).
cnf(t290259,plain,
meet(one,composition(sk1,top)) = converse(sk1),
inference(step,[status(thm)],[t290258,t126500]) ).
cnf(t290260,plain,
meet(one,composition(sk1,top)) = sk1,
inference(step,[status(thm)],[t290259,t135459]) ).
cnf(t137109,plain,
meet(one,composition(sk1,top)) = sk1,
inference(orient,[status(thm)],[t290260]) ).
cnf(t137121,plain,
meet(sk0,composition(sk1,top)) = meet(sk0,sk1),
inference(cp,[status(thm)],[t26681,t137109]) ).
cnf(t290263,plain,
meet(sk0,composition(sk1,top)) = meet(sk1,sk0),
inference(step,[status(thm)],[t137121,t74]) ).
cnf(t137232,plain,
meet(sk0,composition(sk1,top)) = meet(sk1,sk0),
inference(orient,[status(thm)],[t290263]) ).
cnf(t291581,plain,
meet(sk1,sk0) = converse(composition(sk0,sk1)),
inference(step,[status(thm)],[t291580,t137232]) ).
cnf(t147874,plain,
converse(composition(sk0,X1)) = composition(converse(X1),sk0),
inference(cp,[status(thm)],[t56,t147869]) ).
cnf(t148834,plain,
converse(composition(sk0,X1)) = composition(converse(X1),sk0),
inference(orient,[status(thm)],[t147874]) ).
cnf(t291582,plain,
meet(sk1,sk0) = composition(converse(sk1),sk0),
inference(step,[status(thm)],[t291581,t148834]) ).
cnf(t291583,plain,
meet(sk1,sk0) = composition(sk1,sk0),
inference(step,[status(thm)],[t291582,t135459]) ).
cnf(t282357,plain,
composition(sk1,sk0) = meet(sk1,sk0),
inference(orient,[status(thm)],[t291583]) ).
cnf(t282366,plain,
composition(sk1,composition(sk0,X1)) = composition(meet(sk1,sk0),X1),
inference(cp,[status(thm)],[t51,t282357]) ).
cnf(t285879,plain,
composition(meet(sk1,sk0),X1) = composition(sk1,composition(sk0,X1)),
inference(orient,[status(thm)],[t282366]) ).
cnf(c15,plain,
meet(composition(sk0,sk2),composition(sk1,sk2)) != composition(meet(sk0,sk1),sk2),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
meet(composition(sk0,sk2),composition(sk1,sk2)) != composition(meet(sk0,sk1),sk2),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(g0_0,plain,
meet(composition(sk1,sk2),composition(sk0,sk2)) != composition(meet(sk0,sk1),sk2),
inference(rw,[status(thm)],[goal_0,t74]) ).
cnf(g0_1,plain,
meet(sk2,composition(sk1,composition(sk0,sk2))) != composition(meet(sk0,sk1),sk2),
inference(rw,[status(thm)],[g0_0,t287938]) ).
cnf(g0_2,plain,
composition(sk1,composition(sk0,sk2)) != composition(meet(sk0,sk1),sk2),
inference(rw,[status(thm)],[g0_1,t269090]) ).
cnf(g0_3,plain,
composition(sk1,composition(sk0,sk2)) != composition(meet(sk1,sk0),sk2),
inference(rw,[status(thm)],[g0_2,t74]) ).
cnf(g0_4,plain,
composition(sk1,composition(sk0,sk2)) != composition(sk1,composition(sk0,sk2)),
inference(rw,[status(thm)],[g0_3,t285879]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL029+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n004.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Thu Sep 24 07:23:35 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 118.69/15.59 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 118.69/15.59 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------