%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL028+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.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:17 PM UTC 2026
% Result : Theorem 138.90s 20.84s
% Output : Proof 138.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 128
% Number of leaves : 13
% Syntax : Number of formulae : 371 ( 367 unt; 0 def)
% Number of atoms : 379 ( 378 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 15 ( 7 ~; 0 |; 6 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 491 ( 46 sgn 70 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f3_nnf,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(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/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f0_nnf,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(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(t282437,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)],[t282437]) ).
fof(f2,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(f2_nnf,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(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(t282453,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t21,t20]) ).
cnf(t282454,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t282453,t44]) ).
cnf(t282455,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t282454,t20]) ).
cnf(t256,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t282455]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f10_nnf,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t13,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t282434,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)],[t282434]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f9_nnf,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(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/sandbox2/benchmark/theBenchmark.p',converse_idempotence) ).
fof(f7_nnf,plain,
! [X0] : converse(converse(X0)) = X0,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X0] : converse(converse(X0)) = X0,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
converse(converse(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t1,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(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/sandbox2/benchmark/theBenchmark.p',composition_identity) ).
fof(f5_nnf,plain,
! [X0] : composition(X0,one) = X0,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X0] : composition(X0,one) = X0,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
composition(X0,one) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t0,plain,
composition(X1,one) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(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(t282443,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t172,t19]) ).
cnf(t186,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t282443]) ).
cnf(t187,plain,
one = converse(one),
inference(cp,[status(thm)],[t186,t18]) ).
cnf(t193,plain,
converse(one) = one,
inference(orient,[status(thm)],[t187]) ).
cnf(t282444,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t186,t193]) ).
cnf(t203,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t282444]) ).
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(t282448,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t207,t193]) ).
cnf(t282449,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t282448,t204]) ).
cnf(t241,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t282449]) ).
cnf(t263,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t256,t241]) ).
cnf(t282457,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/sandbox2/benchmark/theBenchmark.p',def_zero) ).
fof(f12_nnf,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(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(t282458,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t282457,t63]) ).
cnf(t282459,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t282458,t20]) ).
cnf(t272,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t282459]) ).
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity) ).
fof(f1_nnf,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(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/sandbox2/benchmark/theBenchmark.p',def_top) ).
fof(f11_nnf,plain,
! [X0] : top = join(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X0] : top = join(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
top = join(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(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(t282435,plain,
zero = complement(top),
inference(step,[status(thm)],[t45,t63]) ).
cnf(t65,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t282435]) ).
cnf(t245,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t241,t65]) ).
cnf(t282450,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t245,t65]) ).
cnf(t282451,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t282450,t65]) ).
cnf(t252,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t282451]) ).
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(t282466,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t313,t272]) ).
cnf(t316,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t282466]) ).
cnf(t282469,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t272,t316]) ).
cnf(t327,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t282469]) ).
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(t282481,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t349,t346]) ).
cnf(t282482,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t282481,t346]) ).
cnf(t365,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t282482]) ).
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(t282505,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t474,t256]) ).
cnf(t282506,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t282505,t20]) ).
cnf(t512,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t282506]) ).
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(t282546,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)],[t282546]) ).
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(t282738,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t8907,t346]) ).
cnf(t282739,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t282738,t44]) ).
cnf(t9077,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t282739]) ).
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(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(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(t282509,plain,
join(X1,join(complement(X1),X2)) = join(X2,top),
inference(step,[status(thm)],[t557,t545]) ).
cnf(t473,plain,
join(X1,complement(X1)) = join(X1,top),
inference(cp,[status(thm)],[t469,t25]) ).
cnf(t282497,plain,
top = join(X1,top),
inference(step,[status(thm)],[t473,t25]) ).
cnf(t480,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t282497]) ).
cnf(t282510,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t282509,t480]) ).
cnf(t650,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t282510]) ).
fof(f13,conjecture,
! [X0,X1] :
( ( join(X1,one) = one
& join(X0,one) = one )
=> composition(X0,X1) = meet(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f13_neg,negated_conjecture,
~ ! [X0,X1] :
( ( join(X1,one) = one
& join(X0,one) = one )
=> composition(X0,X1) = meet(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f13_nnf,plain,
? [X0,X1] :
( composition(X0,X1) != meet(X0,X1)
& join(X1,one) = one
& join(X0,one) = one ),
inference(nnf_transformation,[status(thm)],[f13_neg]) ).
fof(f13_sk,plain,
( composition(sk0,sk1) != meet(sk0,sk1)
& join(sk1,one) = one
& join(sk0,one) = one ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f13_nnf]) ).
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(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(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(t282522,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)],[t282522]) ).
cnf(t8856,plain,
join(join(complement(sk0),X1),complement(one)) = join(join(complement(sk0),X1),complement(top)),
inference(cp,[status(thm)],[t8759,t785]) ).
cnf(t282981,plain,
join(complement(sk0),join(X1,complement(one))) = join(join(complement(sk0),X1),complement(top)),
inference(step,[status(thm)],[t8856,t22]) ).
cnf(t282982,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),join(X1,complement(top))),
inference(step,[status(thm)],[t282981,t22]) ).
cnf(t282983,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(top),join(complement(sk0),X1)),
inference(step,[status(thm)],[t282982,t545]) ).
cnf(t282984,plain,
join(complement(sk0),join(X1,complement(one))) = join(zero,join(complement(sk0),X1)),
inference(step,[status(thm)],[t282983,t65]) ).
cnf(t282985,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(step,[status(thm)],[t282984,t316]) ).
cnf(t26500,plain,
join(complement(sk0),join(X1,complement(one))) = join(complement(sk0),X1),
inference(orient,[status(thm)],[t282985]) ).
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(t282986,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),join(complement(sk0),X1)),
inference(step,[status(thm)],[t26509,t346]) ).
cnf(t282987,plain,
meet(sk0,join(X1,complement(one))) = meet(complement(complement(sk0)),X1),
inference(step,[status(thm)],[t282986,t10457]) ).
cnf(t282988,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(step,[status(thm)],[t282987,t346]) ).
cnf(t26542,plain,
meet(sk0,join(X1,complement(one))) = meet(sk0,X1),
inference(orient,[status(thm)],[t282988]) ).
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(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]) ).
cnf(t26585,plain,
meet(sk0,meet(one,X1)) = meet(sk0,join(complement(one),X1)),
inference(cp,[status(thm)],[t26581,t9964]) ).
cnf(t282990,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)],[t282990]) ).
fof(f8,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity) ).
fof(f8_nnf,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(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]) ).
fof(f6,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity) ).
fof(f6_nnf,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(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(t283646,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)],[t283646]) ).
cnf(t141,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t140,t25]) ).
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(t500,plain,
converse(top) = top,
inference(cp,[status(thm)],[t499,t486]) ).
cnf(t504,plain,
converse(top) = top,
inference(orient,[status(thm)],[t500]) ).
cnf(t282547,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)],[t282547]) ).
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(t282480,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t348,t346]) ).
cnf(t363,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t282480]) ).
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(t282742,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)],[t282742]) ).
cnf(t9290,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = complement(complement(X1)),
inference(cp,[status(thm)],[t896,t9249]) ).
cnf(t282743,plain,
join(X1,complement(converse(complement(converse(X1))))) = complement(complement(X1)),
inference(step,[status(thm)],[t9290,t346]) ).
cnf(t282744,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t282743,t346]) ).
cnf(t9298,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t282744]) ).
cnf(t9352,plain,
join(X1,converse(complement(converse(complement(converse(converse(X1))))))) = converse(converse(X1)),
inference(cp,[status(thm)],[t140,t9298]) ).
cnf(t282745,plain,
join(X1,converse(complement(converse(complement(X1))))) = converse(converse(X1)),
inference(step,[status(thm)],[t9352,t19]) ).
cnf(t282746,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(step,[status(thm)],[t282745,t19]) ).
cnf(t9361,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(orient,[status(thm)],[t282746]) ).
cnf(t9390,plain,
meet(X1,converse(complement(converse(complement(complement(X1)))))) = meet(X1,complement(X1)),
inference(cp,[status(thm)],[t9135,t9361]) ).
cnf(t282747,plain,
meet(X1,converse(complement(converse(X1)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t9390,t346]) ).
cnf(t282748,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t282747,t63]) ).
cnf(t9413,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t282748]) ).
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(t282789,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(t282790,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t282789,t339]) ).
cnf(t11421,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t282790]) ).
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(t282791,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)],[t282791]) ).
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(t662,plain,
X1 = join(meet(X1,join(complement(complement(X1)),X2)),complement(top)),
inference(cp,[status(thm)],[t256,t650]) ).
cnf(t282511,plain,
X1 = join(complement(top),meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t662,t20]) ).
cnf(t282512,plain,
X1 = join(zero,meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t282511,t65]) ).
cnf(t282513,plain,
X1 = meet(X1,join(complement(complement(X1)),X2)),
inference(step,[status(thm)],[t282512,t316]) ).
cnf(t282514,plain,
X1 = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t282513,t346]) ).
cnf(t676,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t282514]) ).
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(t282533,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)],[t282533]) ).
cnf(t978,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t968,t719]) ).
cnf(t282541,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)],[t282541]) ).
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(t282688,plain,
zero = meet(complement(complement(one)),composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t5677,t74]) ).
cnf(t282689,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t282688,t346]) ).
cnf(t5682,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t282689]) ).
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(t282719,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)],[t282719]) ).
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(t282725,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(t282720,plain,
complement(one) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(step,[status(thm)],[t8043,t19]) ).
cnf(t282721,plain,
complement(one) = meet(converse(complement(one)),converse(converse(complement(one)))),
inference(step,[status(thm)],[t282720,t74]) ).
cnf(t282722,plain,
complement(one) = meet(converse(complement(one)),complement(one)),
inference(step,[status(thm)],[t282721,t19]) ).
cnf(t282723,plain,
complement(one) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t282722,t74]) ).
cnf(t8052,plain,
meet(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t282723]) ).
cnf(t282726,plain,
converse(complement(one)) = complement(one),
inference(step,[status(thm)],[t282725,t8052]) ).
cnf(t8259,plain,
converse(complement(one)) = complement(one),
inference(orient,[status(thm)],[t282726]) ).
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(t282813,plain,
converse(meet(complement(X1),one)) = complement(join(converse(X1),complement(one))),
inference(step,[status(thm)],[t11514,t928]) ).
cnf(t282814,plain,
converse(meet(one,complement(X1))) = complement(join(converse(X1),complement(one))),
inference(step,[status(thm)],[t282813,t74]) ).
cnf(t282815,plain,
converse(meet(one,complement(X1))) = meet(complement(converse(X1)),one),
inference(step,[status(thm)],[t282814,t928]) ).
cnf(t282816,plain,
converse(meet(one,complement(X1))) = meet(one,complement(converse(X1))),
inference(step,[status(thm)],[t282815,t74]) ).
cnf(t282817,plain,
converse(meet(one,complement(X1))) = meet(one,converse(complement(X1))),
inference(step,[status(thm)],[t282816,t11513]) ).
cnf(t11567,plain,
converse(meet(one,complement(X1))) = meet(one,converse(complement(X1))),
inference(orient,[status(thm)],[t282817]) ).
cnf(t11579,plain,
meet(one,converse(complement(complement(X1)))) = converse(meet(one,X1)),
inference(cp,[status(thm)],[t11567,t346]) ).
cnf(t282818,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)],[t282818]) ).
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(t283765,plain,
composition(one,converse(X2)) = join(converse(X2),converse(composition(X2,meet(one,X1)))),
inference(step,[status(thm)],[t86448,t512]) ).
cnf(t283766,plain,
converse(X2) = join(converse(X2),converse(composition(X2,meet(one,X1)))),
inference(step,[status(thm)],[t283765,t204]) ).
cnf(t283767,plain,
converse(X2) = converse(join(X2,composition(X2,meet(one,X1)))),
inference(step,[status(thm)],[t283766,t35]) ).
cnf(t101412,plain,
converse(join(X1,composition(X1,meet(one,X2)))) = converse(X1),
inference(orient,[status(thm)],[t283767]) ).
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(t283768,plain,
X1 = converse(join(converse(X1),converse(composition(meet(one,X2),X1)))),
inference(step,[status(thm)],[t101421,t19]) ).
cnf(t283769,plain,
X1 = join(X1,converse(converse(composition(meet(one,X2),X1)))),
inference(step,[status(thm)],[t283768,t140]) ).
cnf(t283770,plain,
X1 = join(X1,composition(meet(one,X2),X1)),
inference(step,[status(thm)],[t283769,t19]) ).
cnf(t101620,plain,
join(X1,composition(meet(one,X2),X1)) = X1,
inference(orient,[status(thm)],[t283770]) ).
cnf(t197,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t35,t193]) ).
cnf(t282445,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)],[t282445]) ).
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(t282446,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t220,t193]) ).
cnf(t233,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t282446]) ).
cnf(t727,plain,
converse(sk1) = meet(converse(sk1),one),
inference(cp,[status(thm)],[t719,t233]) ).
cnf(t282517,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)],[t282517]) ).
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(t283771,plain,
join(X1,composition(converse(converse(X1)),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t101914,t171]) ).
cnf(t283772,plain,
join(X1,composition(X1,sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t283771,t19]) ).
cnf(t283773,plain,
join(X1,composition(X1,sk1)) = X1,
inference(step,[status(thm)],[t283772,t19]) ).
cnf(t102660,plain,
join(X1,composition(X1,sk1)) = X1,
inference(orient,[status(thm)],[t283773]) ).
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(t285505,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(t283777,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)],[t283777]) ).
cnf(t285506,plain,
composition(X1,sk1) = meet(X1,join(complement(X1),composition(top,sk1))),
inference(step,[status(thm)],[t285505,t102953]) ).
cnf(t285507,plain,
composition(X1,sk1) = meet(X1,composition(top,sk1)),
inference(step,[status(thm)],[t285506,t9135]) ).
cnf(t282038,plain,
meet(X1,composition(top,sk1)) = composition(X1,sk1),
inference(orient,[status(thm)],[t285507]) ).
cnf(t282079,plain,
meet(sk0,composition(top,sk1)) = meet(sk0,composition(one,sk1)),
inference(cp,[status(thm)],[t26681,t282038]) ).
cnf(t285542,plain,
composition(sk0,sk1) = meet(sk0,composition(one,sk1)),
inference(step,[status(thm)],[t282079,t282038]) ).
cnf(t285543,plain,
composition(sk0,sk1) = meet(sk0,sk1),
inference(step,[status(thm)],[t285542,t204]) ).
cnf(t285544,plain,
composition(sk0,sk1) = meet(sk1,sk0),
inference(step,[status(thm)],[t285543,t74]) ).
cnf(t282398,plain,
composition(sk0,sk1) = meet(sk1,sk0),
inference(orient,[status(thm)],[t285544]) ).
cnf(c15,plain,
composition(sk0,sk1) != meet(sk0,sk1),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
meet(sk0,sk1) != composition(sk0,sk1),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(g0_0,plain,
meet(sk1,sk0) != composition(sk0,sk1),
inference(rw,[status(thm)],[goal_0,t74]) ).
cnf(g0_1,plain,
meet(sk1,sk0) != meet(sk1,sk0),
inference(rw,[status(thm)],[g0_0,t282398]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL028+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n010.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 07:22:42 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 138.90/20.84 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 138.90/20.84 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------