%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL044+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:36:09 PM UTC 2026
% Result : Theorem 107.79s 16.06s
% Output : Proof 107.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 170
% Number of leaves : 16
% Syntax : Number of formulae : 591 ( 587 unt; 0 def)
% Number of atoms : 595 ( 594 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 11 ( 7 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 887 ( 115 sgn 99 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f0_nnf,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t4,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t43,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux2_join_associativity) ).
fof(f1_nnf,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t46,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f10_nnf,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t12,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t259118,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t43]) ).
cnf(t54,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t259118]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f9_nnf,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t6,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t27,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
fof(f7,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_idempotence) ).
fof(f7_nnf,plain,
! [X0] : converse(converse(X0)) = X0,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X0] : converse(converse(X0)) = X0,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
converse(converse(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t1,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t29,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t151,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t29]) ).
fof(f5,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_identity) ).
fof(f5_nnf,plain,
! [X0] : composition(X0,one) = X0,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X0] : composition(X0,one) = X0,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
composition(X0,one) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t0,plain,
composition(X1,one) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t17,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t152,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t151,t17]) ).
cnf(t259124,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t152,t21]) ).
cnf(t164,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t259124]) ).
cnf(t165,plain,
one = converse(one),
inference(cp,[status(thm)],[t164,t17]) ).
cnf(t174,plain,
converse(one) = one,
inference(orient,[status(thm)],[t165]) ).
cnf(t259125,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t164,t174]) ).
cnf(t184,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t259125]) ).
cnf(t185,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t184]) ).
cnf(t188,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t54,t185]) ).
cnf(t259127,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t188,t174]) ).
cnf(t259128,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t259127,t185]) ).
cnf(t214,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t259128]) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f3_nnf,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t5,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t85,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t215,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t214,t85]) ).
cnf(t259148,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t215,t85]) ).
cnf(t259149,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t259148,t85]) ).
cnf(t439,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t259149]) ).
cnf(t87,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t85,t43]) ).
cnf(t259122,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t87,t85]) ).
cnf(t106,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t259122]) ).
cnf(t440,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t439,t106]) ).
cnf(t460,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t440]) ).
fof(f2,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(f2_nnf,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t13,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t18,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t45,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t18]) ).
cnf(t259664,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t45,t43]) ).
cnf(t259665,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t259664,t85]) ).
cnf(t259666,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t259665,t43]) ).
cnf(t15033,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t259666]) ).
fof(f12,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_zero) ).
fof(f12_nnf,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t3,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t92,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t15034,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t15033,t92]) ).
cnf(t259774,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t15034,t85]) ).
cnf(t15710,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t259774]) ).
fof(f11,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_top) ).
fof(f11_nnf,plain,
! [X0] : top = join(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X0] : top = join(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
top = join(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t2,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t51,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t86,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t85,t51]) ).
cnf(t259120,plain,
zero = complement(top),
inference(step,[status(thm)],[t86,t92]) ).
cnf(t97,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t259120]) ).
cnf(t218,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t214,t97]) ).
cnf(t259129,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t218,t97]) ).
cnf(t259130,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t259129,t97]) ).
cnf(t225,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t259130]) ).
cnf(t226,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t46,t225]) ).
cnf(t244,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t226]) ).
cnf(t15715,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t244,t15710]) ).
cnf(t259776,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t15715,t15710]) ).
cnf(t15730,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t259776]) ).
cnf(t259781,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t15710,t15730]) ).
cnf(t15756,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t259781]) ).
cnf(t15782,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t15756]) ).
cnf(t15783,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t460,t15782]) ).
cnf(t259816,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t15783,t15782]) ).
cnf(t259817,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t259816,t15782]) ).
cnf(t15849,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t259817]) ).
cnf(t15853,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t46,t15849]) ).
cnf(t15896,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t15853]) ).
cnf(t15912,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t15896,t15033]) ).
cnf(t259821,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t15912,t15033]) ).
cnf(t259822,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t259821,t43]) ).
cnf(t15921,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t259822]) ).
cnf(t15923,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t15921,t106]) ).
cnf(t15948,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t15923]) ).
cnf(t15953,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t46,t15948]) ).
cnf(t18408,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t15953]) ).
cnf(t224,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t85,t214]) ).
cnf(t231,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t224]) ).
cnf(t242,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t85,t231]) ).
cnf(t1075,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t242]) ).
cnf(t259800,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1075,t15782]) ).
cnf(t15815,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t259800]) ).
cnf(t16179,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t15815]) ).
cnf(t259831,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t15033,t16179]) ).
cnf(t16296,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t259831]) ).
cnf(t21679,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t16296]) ).
cnf(t21731,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t18408,t21679]) ).
cnf(t22046,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t21731]) ).
cnf(t22061,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t22046,t106]) ).
cnf(t22552,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t22061]) ).
cnf(t100,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t85,t97]) ).
cnf(t118,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t100]) ).
fof(f8,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_additivity) ).
fof(f8_nnf,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t8,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t62,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t65,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t62,t21]) ).
cnf(t277,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t65]) ).
cnf(t53,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t46,t51]) ).
cnf(t313,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t53]) ).
cnf(t239,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t51,t231]) ).
cnf(t255,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t239]) ).
cnf(t317,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t313,t255]) ).
cnf(t319,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t313,t214]) ).
cnf(t259135,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t319,t51]) ).
cnf(t331,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t259135]) ).
cnf(t332,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t331,t85]) ).
cnf(t348,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t332]) ).
cnf(t259137,plain,
top = join(X1,top),
inference(step,[status(thm)],[t317,t348]) ).
cnf(t353,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t259137]) ).
cnf(t354,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t353,t43]) ).
cnf(t359,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t354]) ).
cnf(t64,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t62,t21]) ).
cnf(t260,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t64]) ).
cnf(t262,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t260,t51]) ).
cnf(t296,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t262]) ).
cnf(t362,plain,
top = converse(top),
inference(cp,[status(thm)],[t359,t296]) ).
cnf(t365,plain,
converse(top) = top,
inference(orient,[status(thm)],[t362]) ).
cnf(t370,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t27,t365]) ).
cnf(t377,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t370]) ).
cnf(t383,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t277,t377]) ).
cnf(t10013,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t383]) ).
fof(f6,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_distributivity) ).
fof(f6_nnf,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t11,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t24,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t30,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t24,t27]) ).
cnf(t1679,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t30]) ).
cnf(t10014,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t10013,t1679]) ).
cnf(t259557,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t10014,t21]) ).
cnf(t28,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t141,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t28]) ).
cnf(t259558,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t259557,t141]) ).
cnf(t259559,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t259558,t260]) ).
cnf(t259560,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t259559,t365]) ).
cnf(t259561,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t259560,t353]) ).
cnf(t10093,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t259561]) ).
cnf(t371,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t27,t365]) ).
cnf(t391,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t371]) ).
cnf(t379,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t62,t377]) ).
cnf(t4114,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t379]) ).
cnf(t4127,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t4114,t365]) ).
cnf(t4161,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t4127]) ).
cnf(t4165,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t4161,t24]) ).
cnf(t259325,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t4165,t377]) ).
cnf(t259326,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t259325,t377]) ).
cnf(t259327,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t259326,t359]) ).
cnf(t259328,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t259327,t365]) ).
cnf(t4279,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t259328]) ).
cnf(t4295,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t4279,t174]) ).
cnf(t259329,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t4295,t17]) ).
cnf(t259330,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t259329,t353]) ).
cnf(t4308,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t259330]) ).
cnf(t4313,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t4308]) ).
cnf(t259338,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t4313,t97]) ).
cnf(t259339,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t259338,t97]) ).
cnf(t259340,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t259339,t365]) ).
cnf(t259341,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t259340,t97]) ).
fof(f13,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dedekind_law) ).
fof(f13_nnf,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t16,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t33,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t16]) ).
cnf(t66,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t46,t62]) ).
cnf(t1761,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t66]) ).
cnf(t323,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t313,t43]) ).
cnf(t259146,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t323,t359]) ).
cnf(t403,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t259146]) ).
cnf(t1765,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t1761,t403]) ).
cnf(t259226,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t1765,t43]) ).
cnf(t1816,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t259226]) ).
cnf(t1849,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t1816,t62]) ).
cnf(t259227,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t1849,t21]) ).
cnf(t259228,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t259227,t21]) ).
cnf(t1863,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t259228]) ).
cnf(t1894,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t1863,t43]) ).
cnf(t1897,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t1894]) ).
cnf(t56,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t54,t17]) ).
cnf(t1148,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t56]) ).
cnf(t1158,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1148,t21]) ).
cnf(t1176,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1158]) ).
cnf(t1908,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t1897,t1176]) ).
cnf(t259241,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t1908,t43]) ).
cnf(t2267,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t259241]) ).
cnf(t2285,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t85,t2267]) ).
cnf(t259242,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t2285,t97]) ).
cnf(t2288,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t259242]) ).
cnf(t2309,plain,
composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(cp,[status(thm)],[t33,t2288]) ).
cnf(t259243,plain,
composition(meet(X1,composition(complement(X1),converse(one))),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t2309,t21]) ).
cnf(t259244,plain,
composition(meet(X1,composition(complement(X1),one)),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t259243,t174]) ).
cnf(t259245,plain,
composition(meet(X1,complement(X1)),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t259244,t17]) ).
cnf(t259246,plain,
composition(zero,meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t259245,t92]) ).
cnf(t259247,plain,
composition(zero,zero) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t259246,t2288]) ).
cnf(t259248,plain,
composition(zero,zero) = join(meet(X1,complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t259247,t17]) ).
cnf(t259249,plain,
composition(zero,zero) = join(meet(X1,complement(X1)),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t259248,t21]) ).
cnf(t259250,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t259249,t92]) ).
cnf(t259251,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),converse(one))),zero)),
inference(step,[status(thm)],[t259250,t21]) ).
cnf(t259252,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),one)),zero)),
inference(step,[status(thm)],[t259251,t174]) ).
cnf(t259253,plain,
composition(zero,zero) = join(zero,composition(meet(X1,complement(X1)),zero)),
inference(step,[status(thm)],[t259252,t17]) ).
cnf(t259254,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t259253,t92]) ).
cnf(t2310,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t259254]) ).
cnf(t2313,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t46,t2310]) ).
cnf(t2415,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t2313]) ).
cnf(t2423,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t2415,t24]) ).
cnf(t259263,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t2423,t24]) ).
cnf(t2516,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t259263]) ).
cnf(t52,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t51,t46]) ).
cnf(t472,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t52]) ).
cnf(t489,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t472,t43]) ).
cnf(t573,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t489]) ).
cnf(t585,plain,
top = join(complement(X1),join(X1,complement(top))),
inference(cp,[status(thm)],[t573,t51]) ).
cnf(t259157,plain,
top = join(complement(X1),join(X1,zero)),
inference(step,[status(thm)],[t585,t97]) ).
cnf(t605,plain,
join(complement(X1),join(X1,zero)) = top,
inference(orient,[status(thm)],[t259157]) ).
cnf(t612,plain,
top = join(complement(X1),join(zero,X1)),
inference(cp,[status(thm)],[t605,t43]) ).
cnf(t614,plain,
join(complement(X1),join(zero,X1)) = top,
inference(orient,[status(thm)],[t612]) ).
cnf(t102,plain,
complement(top) = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(cp,[status(thm)],[t54,t97]) ).
cnf(t259185,plain,
zero = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(step,[status(thm)],[t102,t97]) ).
cnf(t1351,plain,
join(zero,composition(converse(X1),complement(composition(X1,top)))) = zero,
inference(orient,[status(thm)],[t259185]) ).
cnf(t1356,plain,
zero = join(zero,composition(top,complement(composition(top,top)))),
inference(cp,[status(thm)],[t1351,t365]) ).
cnf(t1373,plain,
join(zero,composition(top,complement(composition(top,top)))) = zero,
inference(orient,[status(thm)],[t1356]) ).
cnf(t1375,plain,
top = join(complement(composition(top,complement(composition(top,top)))),zero),
inference(cp,[status(thm)],[t614,t1373]) ).
cnf(t259206,plain,
top = join(zero,complement(composition(top,complement(composition(top,top))))),
inference(step,[status(thm)],[t1375,t43]) ).
cnf(t1615,plain,
join(zero,complement(composition(top,complement(composition(top,top))))) = top,
inference(orient,[status(thm)],[t259206]) ).
cnf(t2519,plain,
composition(join(zero,complement(composition(top,complement(composition(top,top))))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t2516,t1615]) ).
cnf(t259264,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t2519,t1615]) ).
cnf(t2545,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t259264]) ).
cnf(t259342,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t259341,t2545]) ).
cnf(t4319,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t259342]) ).
cnf(t4320,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t391,t4319]) ).
cnf(t4336,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t4320]) ).
cnf(t10145,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t10093,t4336]) ).
cnf(t259590,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t10145,t4336]) ).
cnf(t259591,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t259590,t43]) ).
cnf(t11120,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t259591]) ).
cnf(t2535,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t2516,t43]) ).
cnf(t2596,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t2535]) ).
cnf(t4321,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t24,t4319]) ).
cnf(t259348,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t4321,t359]) ).
cnf(t259349,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t259348,t4319]) ).
cnf(t4355,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t259349]) ).
cnf(t259352,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t2596,t4355]) ).
cnf(t4373,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t259352]) ).
cnf(t4505,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t4373]) ).
cnf(t4508,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t4505,t43]) ).
cnf(t4525,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t4508]) ).
cnf(t4527,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t24,t4525]) ).
cnf(t259378,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t4527,t46]) ).
cnf(t259379,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t259378,t4355]) ).
cnf(t4708,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t259379]) ).
cnf(t175,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t62,t174]) ).
cnf(t191,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t175]) ).
cnf(t197,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t151,t191]) ).
cnf(t3884,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t197]) ).
fof(f4,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_associativity) ).
fof(f4_nnf,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t9,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t22,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t26,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t24,t22]) ).
cnf(t836,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t4311,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t836,t4308]) ).
cnf(t259464,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t4311,t24]) ).
cnf(t6224,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t259464]) ).
cnf(t6236,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t6224,t185]) ).
cnf(t259465,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t6236,t353]) ).
cnf(t259466,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t259465,t4308]) ).
cnf(t6259,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t259466]) ).
cnf(t6261,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t6259,t43]) ).
cnf(t6282,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t6261]) ).
cnf(t6297,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t3884,t6282]) ).
cnf(t259469,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t6297,t365]) ).
cnf(t259470,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t259469,t365]) ).
cnf(t6316,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t259470]) ).
cnf(t6317,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t6316,t43]) ).
cnf(t6527,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t6317]) ).
cnf(t6534,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t6527]) ).
cnf(t259492,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t6534,t365]) ).
cnf(t259493,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t259492,t43]) ).
cnf(t259494,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t259493,t97]) ).
cnf(t259495,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t259494,t4319]) ).
cnf(t7119,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t259495]) ).
cnf(t7128,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t4708,t7119]) ).
cnf(t7388,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t7128]) ).
cnf(t15250,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t7388,t15033]) ).
cnf(t15255,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t15250]) ).
cnf(t15262,plain,
converse(zero) = join(converse(zero),zero),
inference(cp,[status(thm)],[t11120,t15255]) ).
cnf(t259710,plain,
converse(zero) = join(zero,converse(zero)),
inference(step,[status(thm)],[t15262,t43]) ).
cnf(t15415,plain,
join(zero,converse(zero)) = converse(zero),
inference(orient,[status(thm)],[t259710]) ).
cnf(t15425,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t277,t15415]) ).
cnf(t259711,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t15425,t43]) ).
cnf(t259712,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t259711,t15415]) ).
cnf(t259713,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t259712,t21]) ).
cnf(t15428,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t259713]) ).
cnf(t15431,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t27,t15428]) ).
cnf(t259745,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t15431,t15255]) ).
cnf(t259746,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t259745,t15428]) ).
cnf(t15512,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t259746]) ).
cnf(t15529,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t15512,t21]) ).
cnf(t15550,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t15529]) ).
cnf(t15561,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t54,t15550]) ).
cnf(t259747,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t15561,t15428]) ).
cnf(t259748,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t259747,t15550]) ).
cnf(t259749,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t259748,t43]) ).
cnf(t15563,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t259749]) ).
cnf(t259762,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t118,t15563]) ).
cnf(t15604,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t259762]) ).
cnf(t15605,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t15604]) ).
cnf(t15736,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t15730,t43]) ).
cnf(t15768,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t15736]) ).
cnf(t15778,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t15033,t15768]) ).
cnf(t1935,plain,
join(complement(X1),join(join(X2,X1),X3)) = join(top,X3),
inference(cp,[status(thm)],[t46,t1897]) ).
cnf(t259238,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t1935,t46]) ).
cnf(t259239,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t259238,t359]) ).
cnf(t2173,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t259239]) ).
cnf(t7129,plain,
top = join(complement(zero),join(X1,complement(join(X2,one)))),
inference(cp,[status(thm)],[t2173,t7119]) ).
cnf(t9282,plain,
join(complement(zero),join(X1,complement(join(X2,one)))) = top,
inference(orient,[status(thm)],[t7129]) ).
cnf(t15249,plain,
top = join(complement(zero),X1),
inference(cp,[status(thm)],[t9282,t15033]) ).
cnf(t15314,plain,
join(complement(zero),X1) = top,
inference(orient,[status(thm)],[t15249]) ).
cnf(t15315,plain,
top = complement(zero),
inference(cp,[status(thm)],[t15314,t54]) ).
cnf(t15356,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t15315]) ).
cnf(t15378,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t85,t15356]) ).
cnf(t259707,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t15378,t353]) ).
cnf(t259708,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t259707,t97]) ).
cnf(t15404,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t259708]) ).
cnf(t259803,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t15778,t15404]) ).
cnf(t259804,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t259803,t15563]) ).
cnf(t259805,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t259804,t15605]) ).
cnf(t15818,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t259805]) ).
cnf(t259806,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t15605,t15818]) ).
cnf(t15819,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t259806]) ).
cnf(t22576,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t22552,t15819]) ).
cnf(t23355,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t22576]) ).
cnf(t35,plain,
composition(meet(converse(X1),composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(converse(X1)),X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(converse(X1)),X2)))),
inference(cp,[status(thm)],[t33,t27]) ).
cnf(t259360,plain,
composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(converse(converse(X1)),X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(converse(X1)),X2)))),
inference(step,[status(thm)],[t35,t21]) ).
cnf(t259361,plain,
composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(X1,X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(converse(X1)),X2)))),
inference(step,[status(thm)],[t259360,t21]) ).
cnf(t259362,plain,
composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(X1,X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(converse(converse(X1)),X2)))),
inference(step,[status(thm)],[t259361,t21]) ).
cnf(t259363,plain,
composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(X1,X2))) = join(meet(converse(composition(X3,X1)),X2),composition(meet(converse(X1),composition(X2,X3)),meet(converse(X3),composition(X1,X2)))),
inference(step,[status(thm)],[t259362,t21]) ).
cnf(t4391,plain,
join(meet(converse(composition(X1,X2)),X3),composition(meet(converse(X2),composition(X3,X1)),meet(converse(X1),composition(X2,X3)))) = composition(meet(converse(X2),composition(X3,X1)),meet(converse(X1),composition(X2,X3))),
inference(orient,[status(thm)],[t259363]) ).
cnf(t39,plain,
composition(meet(X1,composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(X1),X2))) = join(meet(composition(X1,converse(X3)),X2),composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t33,t21]) ).
cnf(t259545,plain,
composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2))) = join(meet(composition(X1,converse(X3)),X2),composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2)))),
inference(step,[status(thm)],[t39,t21]) ).
cnf(t9053,plain,
join(meet(composition(X1,converse(X2)),X3),composition(meet(X1,composition(X3,X2)),meet(converse(X2),composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,X2)),meet(converse(X2),composition(converse(X1),X3))),
inference(orient,[status(thm)],[t259545]) ).
cnf(t2298,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t2288,t21]) ).
cnf(t2322,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t2298]) ).
cnf(t2341,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t2322,t231]) ).
cnf(t3119,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t2341]) ).
cnf(t259802,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(step,[status(thm)],[t3119,t15782]) ).
cnf(t15817,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(rw,[status(thm)],[t259802]) ).
cnf(t17329,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t15817]) ).
cnf(t17344,plain,
composition(meet(one,composition(converse(complement(X1)),X1)),meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(cp,[status(thm)],[t9053,t17329]) ).
cnf(t259846,plain,
composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t17344,t17329]) ).
cnf(t259847,plain,
zero = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t259846,t15550]) ).
cnf(t259848,plain,
zero = join(meet(converse(complement(X1)),composition(one,converse(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t259847,t106]) ).
cnf(t259849,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t259848,t185]) ).
cnf(t259850,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t259849,t106]) ).
cnf(t259851,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t259850,t15550]) ).
cnf(t259852,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t259851,t15768]) ).
cnf(t17375,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t259852]) ).
cnf(t23392,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t23355,t17375]) ).
cnf(t259939,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t23392,t43]) ).
cnf(t259940,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t259939,t15768]) ).
cnf(t24074,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t259940]) ).
cnf(t24079,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t24074,t15819]) ).
cnf(t259144,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t296,t365]) ).
cnf(t368,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t259144]) ).
cnf(t16227,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t16179,t368]) ).
cnf(t259909,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t16227,t97]) ).
cnf(t21663,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t259909]) ).
cnf(t22557,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t22552,t21663]) ).
cnf(t259921,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t22557,t15819]) ).
cnf(t259922,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t259921,t15768]) ).
cnf(t22745,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t259922]) ).
cnf(t22764,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t22745,t21]) ).
cnf(t23909,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t22764]) ).
cnf(t259941,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t24079,t23909]) ).
cnf(t24126,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t259941]) ).
cnf(t24131,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t24126,t15819]) ).
cnf(t24197,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t24131]) ).
cnf(t24211,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t24197,t260]) ).
cnf(t24922,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t24211]) ).
cnf(t120,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t118,t85]) ).
cnf(t3436,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t120]) ).
cnf(t259777,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t3436,t15730]) ).
cnf(t15731,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t259777]) ).
cnf(t259812,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t15731,t15818]) ).
cnf(t15846,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t259812]) ).
cnf(t16451,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t15846]) ).
cnf(t24224,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t16451,t24197]) ).
cnf(t25495,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t24224]) ).
cnf(t25543,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t24922,t25495]) ).
cnf(t259970,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t25543,t16179]) ).
cnf(t259971,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t259970,t24126]) ).
cnf(t259972,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t259971,t15819]) ).
cnf(t25748,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t259972]) ).
cnf(t25767,plain,
meet(X1,converse(X2)) = converse(meet(X2,converse(X1))),
inference(cp,[status(thm)],[t25748,t106]) ).
cnf(t25871,plain,
converse(meet(X1,converse(X2))) = meet(X2,converse(X1)),
inference(orient,[status(thm)],[t25767]) ).
cnf(t25910,plain,
meet(composition(converse(X1),X2),converse(X3)) = converse(meet(X3,composition(converse(X2),X1))),
inference(cp,[status(thm)],[t25871,t151]) ).
cnf(t172412,plain,
converse(meet(X1,composition(converse(X2),X3))) = meet(composition(converse(X3),X2),converse(X1)),
inference(orient,[status(thm)],[t25910]) ).
cnf(t42,plain,
composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(converse(converse(X1)),X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))),
inference(cp,[status(thm)],[t33,t21]) ).
cnf(t259626,plain,
composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))),
inference(step,[status(thm)],[t42,t21]) ).
cnf(t12514,plain,
join(meet(composition(converse(X1),X2),X3),composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3)))) = composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3))),
inference(orient,[status(thm)],[t259626]) ).
cnf(t16231,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t16179,t15819]) ).
cnf(t16505,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t16231]) ).
cnf(t22060,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t22046,t16505]) ).
cnf(t22917,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t22060]) ).
cnf(t23026,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t16179,t22917]) ).
cnf(t259925,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t23026,t15819]) ).
cnf(t259926,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t259925,t85]) ).
cnf(t23043,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t259926]) ).
cnf(t23055,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t23043,t43]) ).
cnf(t23098,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t23055]) ).
cnf(t15927,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t46,t15921]) ).
cnf(t18199,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t15927]) ).
cnf(t23111,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,join(complement(X1),X3)),
inference(cp,[status(thm)],[t23098,t18199]) ).
cnf(t260084,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,X3),
inference(step,[status(thm)],[t23111,t23098]) ).
cnf(t35678,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t260084]) ).
cnf(t16512,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t15948,t16505]) ).
cnf(t259837,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t16512,t16451]) ).
cnf(t16657,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t259837]) ).
cnf(t16688,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t15819,t16657]) ).
cnf(t259838,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t16688,t15819]) ).
cnf(t16746,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t259838]) ).
fof(f16,conjecture,
! [X0,X1,X2] :
( join(composition(complement(X0),X1),complement(X2)) = complement(X2)
=> join(composition(X2,converse(X1)),X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( join(composition(complement(X0),X1),complement(X2)) = complement(X2)
=> join(composition(X2,converse(X1)),X0) = X0 ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1,X2] :
( join(composition(X2,converse(X1)),X0) != X0
& join(composition(complement(X0),X1),complement(X2)) = complement(X2) ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( join(composition(sk2,converse(sk1)),sk0) != sk0
& join(composition(complement(sk0),sk1),complement(sk2)) = complement(sk2) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f16_nnf]) ).
cnf(c16,plain,
join(composition(complement(sk0),sk1),complement(sk2)) = complement(sk2),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t7,plain,
join(composition(complement(sk0),sk1),complement(sk2)) = complement(sk2),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t259119,plain,
join(complement(sk2),composition(complement(sk0),sk1)) = complement(sk2),
inference(step,[status(thm)],[t7,t43]) ).
cnf(t60,plain,
join(complement(sk2),composition(complement(sk0),sk1)) = complement(sk2),
inference(orient,[status(thm)],[t259119]) ).
cnf(t16765,plain,
composition(complement(sk0),sk1) = meet(composition(complement(sk0),sk1),complement(sk2)),
inference(cp,[status(thm)],[t16746,t60]) ).
cnf(t260055,plain,
composition(complement(sk0),sk1) = meet(complement(sk2),composition(complement(sk0),sk1)),
inference(step,[status(thm)],[t16765,t106]) ).
cnf(t32678,plain,
meet(complement(sk2),composition(complement(sk0),sk1)) = composition(complement(sk0),sk1),
inference(orient,[status(thm)],[t260055]) ).
cnf(t35730,plain,
meet(sk2,X1) = meet(sk2,join(composition(complement(sk0),sk1),X1)),
inference(cp,[status(thm)],[t35678,t32678]) ).
cnf(t40995,plain,
meet(sk2,join(composition(complement(sk0),sk1),X1)) = meet(sk2,X1),
inference(orient,[status(thm)],[t35730]) ).
cnf(t40997,plain,
meet(sk2,composition(X1,sk1)) = meet(sk2,composition(join(complement(sk0),X1),sk1)),
inference(cp,[status(thm)],[t40995,t24]) ).
cnf(t256825,plain,
meet(sk2,composition(join(complement(sk0),X1),sk1)) = meet(sk2,composition(X1,sk1)),
inference(orient,[status(thm)],[t40997]) ).
cnf(t256984,plain,
meet(sk2,composition(meet(complement(sk0),X1),sk1)) = meet(sk2,composition(complement(sk0),sk1)),
inference(cp,[status(thm)],[t256825,t15921]) ).
cnf(t1930,plain,
top = join(complement(composition(complement(sk0),sk1)),complement(sk2)),
inference(cp,[status(thm)],[t1897,t60]) ).
cnf(t259236,plain,
top = join(complement(sk2),complement(composition(complement(sk0),sk1))),
inference(step,[status(thm)],[t1930,t43]) ).
cnf(t2121,plain,
join(complement(sk2),complement(composition(complement(sk0),sk1))) = top,
inference(orient,[status(thm)],[t259236]) ).
cnf(t2126,plain,
meet(sk2,composition(complement(sk0),sk1)) = complement(top),
inference(cp,[status(thm)],[t85,t2121]) ).
cnf(t259237,plain,
meet(sk2,composition(complement(sk0),sk1)) = zero,
inference(step,[status(thm)],[t2126,t97]) ).
cnf(t2129,plain,
meet(sk2,composition(complement(sk0),sk1)) = zero,
inference(orient,[status(thm)],[t259237]) ).
cnf(t261747,plain,
meet(sk2,composition(meet(complement(sk0),X1),sk1)) = zero,
inference(step,[status(thm)],[t256984,t2129]) ).
cnf(t257163,plain,
meet(sk2,composition(meet(complement(sk0),X1),sk1)) = zero,
inference(orient,[status(thm)],[t261747]) ).
cnf(t257199,plain,
composition(meet(converse(meet(complement(sk0),X1)),composition(sk1,converse(sk2))),meet(sk2,composition(meet(complement(sk0),X1),sk1))) = join(meet(composition(converse(meet(complement(sk0),X1)),sk2),sk1),composition(meet(converse(meet(complement(sk0),X1)),composition(sk1,converse(sk2))),zero)),
inference(cp,[status(thm)],[t12514,t257163]) ).
cnf(t25792,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(cp,[status(thm)],[t25748,t21]) ).
cnf(t25985,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(orient,[status(thm)],[t25792]) ).
cnf(t26021,plain,
converse(meet(X1,meet(X2,converse(X3)))) = meet(converse(X1),meet(X3,converse(X2))),
inference(cp,[status(thm)],[t25985,t25871]) ).
cnf(t22079,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t18408,t22046]) ).
cnf(t260078,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(step,[status(thm)],[t22079,t18408]) ).
cnf(t35012,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t260078]) ).
cnf(t241,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t85,t231]) ).
cnf(t1025,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t241]) ).
cnf(t259801,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t1025,t15782]) ).
cnf(t15816,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t259801]) ).
cnf(t16378,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t15816]) ).
cnf(t16388,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t15819,t16378]) ).
cnf(t16589,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t16388]) ).
cnf(t35024,plain,
join(X1,X2) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t35012,t16589]) ).
cnf(t35961,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t35024]) ).
cnf(t36011,plain,
meet(X1,meet(X2,join(X3,complement(complement(X1))))) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t23098,t35961]) ).
cnf(t260086,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t36011,t15819]) ).
cnf(t260087,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(step,[status(thm)],[t260086,t23098]) ).
cnf(t36042,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t260087]) ).
cnf(t36090,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X3,X1)),
inference(cp,[status(thm)],[t36042,t15921]) ).
cnf(t37456,plain,
meet(meet(X1,X2),meet(X3,X1)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t36090]) ).
cnf(t37469,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t37456,t106]) ).
cnf(t36065,plain,
meet(X1,X2) = meet(X1,meet(join(X3,X1),X2)),
inference(cp,[status(thm)],[t36042,t106]) ).
cnf(t36245,plain,
meet(X1,meet(join(X2,X1),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t36065]) ).
cnf(t36328,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X2,X3)),
inference(cp,[status(thm)],[t36245,t15948]) ).
cnf(t38242,plain,
meet(meet(X1,X2),meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t36328]) ).
cnf(t260089,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(step,[status(thm)],[t37469,t38242]) ).
cnf(t38513,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(orient,[status(thm)],[t260089]) ).
cnf(t38529,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(cp,[status(thm)],[t38513,t106]) ).
cnf(t39203,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t38529]) ).
cnf(t39409,plain,
meet(X1,converse(meet(X2,X3))) = converse(meet(X2,meet(X3,converse(X1)))),
inference(cp,[status(thm)],[t25871,t39203]) ).
cnf(t112462,plain,
converse(meet(X1,meet(X2,converse(X3)))) = meet(X3,converse(meet(X1,X2))),
inference(orient,[status(thm)],[t39409]) ).
cnf(t261377,plain,
meet(X3,converse(meet(X1,X2))) = meet(converse(X1),meet(X3,converse(X2))),
inference(step,[status(thm)],[t26021,t112462]) ).
cnf(t39323,plain,
meet(converse(X1),meet(converse(X2),X3)) = meet(converse(meet(X1,X2)),X3),
inference(cp,[status(thm)],[t39203,t25985]) ).
cnf(t111740,plain,
meet(converse(X1),meet(converse(X2),X3)) = meet(converse(meet(X1,X2)),X3),
inference(orient,[status(thm)],[t39323]) ).
cnf(t111753,plain,
meet(converse(meet(X1,X2)),X3) = meet(meet(converse(X2),X3),converse(X1)),
inference(cp,[status(thm)],[t111740,t106]) ).
cnf(t261179,plain,
meet(converse(meet(X1,X2)),X3) = meet(converse(X2),meet(X3,converse(X1))),
inference(step,[status(thm)],[t111753,t39203]) ).
cnf(t123024,plain,
meet(converse(X1),meet(X2,converse(X3))) = meet(converse(meet(X3,X1)),X2),
inference(orient,[status(thm)],[t261179]) ).
cnf(t261378,plain,
meet(X3,converse(meet(X1,X2))) = meet(converse(meet(X2,X1)),X3),
inference(step,[status(thm)],[t261377,t123024]) ).
cnf(t172887,plain,
meet(X1,converse(meet(X2,X3))) = meet(converse(meet(X3,X2)),X1),
inference(orient,[status(thm)],[t261378]) ).
cnf(t261792,plain,
composition(meet(composition(sk1,converse(sk2)),converse(meet(X1,complement(sk0)))),meet(sk2,composition(meet(complement(sk0),X1),sk1))) = join(meet(composition(converse(meet(complement(sk0),X1)),sk2),sk1),composition(meet(converse(meet(complement(sk0),X1)),composition(sk1,converse(sk2))),zero)),
inference(step,[status(thm)],[t257199,t172887]) ).
cnf(t261793,plain,
composition(meet(composition(sk1,converse(sk2)),converse(meet(X1,complement(sk0)))),zero) = join(meet(composition(converse(meet(complement(sk0),X1)),sk2),sk1),composition(meet(converse(meet(complement(sk0),X1)),composition(sk1,converse(sk2))),zero)),
inference(step,[status(thm)],[t261792,t257163]) ).
cnf(t261794,plain,
zero = join(meet(composition(converse(meet(complement(sk0),X1)),sk2),sk1),composition(meet(converse(meet(complement(sk0),X1)),composition(sk1,converse(sk2))),zero)),
inference(step,[status(thm)],[t261793,t15255]) ).
cnf(t261795,plain,
zero = join(meet(sk1,composition(converse(meet(complement(sk0),X1)),sk2)),composition(meet(converse(meet(complement(sk0),X1)),composition(sk1,converse(sk2))),zero)),
inference(step,[status(thm)],[t261794,t106]) ).
cnf(t261796,plain,
zero = join(meet(sk1,composition(converse(meet(complement(sk0),X1)),sk2)),zero),
inference(step,[status(thm)],[t261795,t15255]) ).
cnf(t261797,plain,
zero = meet(sk1,composition(converse(meet(complement(sk0),X1)),sk2)),
inference(step,[status(thm)],[t261796,t15768]) ).
cnf(t258623,plain,
meet(sk1,composition(converse(meet(complement(sk0),X1)),sk2)) = zero,
inference(orient,[status(thm)],[t261797]) ).
fof(f15,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modular_law_2) ).
fof(f15_nnf,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
join(meet(composition(X0,X1),X2),meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2)) = meet(composition(meet(X0,composition(X2,converse(X1))),X1),X2),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t15,plain,
join(meet(composition(X1,X2),X3),meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3)) = meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t76,plain,
join(meet(composition(X1,X2),X3),meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3)) = meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3),
inference(orient,[status(thm)],[t15]) ).
cnf(t112,plain,
join(meet(composition(X1,X2),X3),meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3)) = meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3),
inference(rw,[status(thm)],[t76]) ).
cnf(t260682,plain,
join(meet(composition(X1,X2),X3),meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2))) = meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3),
inference(step,[status(thm)],[t112,t106]) ).
cnf(t260683,plain,
join(meet(composition(X1,X2),X3),meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2))) = meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2)),
inference(step,[status(thm)],[t260682,t106]) ).
cnf(t71422,plain,
join(meet(composition(X1,X2),X3),meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2))) = meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2)),
inference(orient,[status(thm)],[t260683]) ).
cnf(t15821,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t15818,t106]) ).
cnf(t15880,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t15821]) ).
cnf(t71566,plain,
meet(top,composition(meet(X1,composition(top,converse(X2))),X2)) = join(composition(X1,X2),meet(top,composition(meet(X1,composition(top,converse(X2))),X2))),
inference(cp,[status(thm)],[t71422,t15880]) ).
cnf(t260684,plain,
composition(meet(X1,composition(top,converse(X2))),X2) = join(composition(X1,X2),meet(top,composition(meet(X1,composition(top,converse(X2))),X2))),
inference(step,[status(thm)],[t71566,t15818]) ).
cnf(t260685,plain,
composition(meet(X1,composition(top,converse(X2))),X2) = join(composition(X1,X2),composition(meet(X1,composition(top,converse(X2))),X2)),
inference(step,[status(thm)],[t260684,t15818]) ).
cnf(t260686,plain,
composition(meet(X1,composition(top,converse(X2))),X2) = composition(join(X1,meet(X1,composition(top,converse(X2)))),X2),
inference(step,[status(thm)],[t260685,t24]) ).
cnf(t260687,plain,
composition(meet(X1,composition(top,converse(X2))),X2) = composition(X1,X2),
inference(step,[status(thm)],[t260686,t15921]) ).
cnf(t71785,plain,
composition(meet(X1,composition(top,converse(X2))),X2) = composition(X1,X2),
inference(orient,[status(thm)],[t260687]) ).
cnf(t26045,plain,
converse(meet(X1,composition(X2,top))) = meet(converse(X1),composition(top,converse(X2))),
inference(cp,[status(thm)],[t25985,t377]) ).
cnf(t111341,plain,
meet(converse(X1),composition(top,converse(X2))) = converse(meet(X1,composition(X2,top))),
inference(orient,[status(thm)],[t26045]) ).
cnf(t111485,plain,
composition(converse(X1),X2) = composition(converse(meet(X1,composition(X2,top))),X2),
inference(cp,[status(thm)],[t71785,t111341]) ).
cnf(t145823,plain,
composition(converse(meet(X1,composition(X2,top))),X2) = composition(converse(X1),X2),
inference(orient,[status(thm)],[t111485]) ).
cnf(t258624,plain,
zero = meet(sk1,composition(converse(complement(sk0)),sk2)),
inference(cp,[status(thm)],[t258623,t145823]) ).
cnf(t258793,plain,
meet(sk1,composition(converse(complement(sk0)),sk2)) = zero,
inference(orient,[status(thm)],[t258624]) ).
cnf(t258813,plain,
meet(composition(converse(sk2),complement(sk0)),converse(sk1)) = converse(zero),
inference(cp,[status(thm)],[t172412,t258793]) ).
cnf(t261801,plain,
meet(converse(sk1),composition(converse(sk2),complement(sk0))) = converse(zero),
inference(step,[status(thm)],[t258813,t106]) ).
cnf(t261802,plain,
meet(converse(sk1),composition(converse(sk2),complement(sk0))) = zero,
inference(step,[status(thm)],[t261801,t15428]) ).
cnf(t258946,plain,
meet(converse(sk1),composition(converse(sk2),complement(sk0))) = zero,
inference(orient,[status(thm)],[t261802]) ).
cnf(t258974,plain,
composition(meet(converse(converse(sk2)),composition(complement(sk0),sk1)),meet(converse(sk1),composition(converse(sk2),complement(sk0)))) = join(meet(converse(composition(sk1,converse(sk2))),complement(sk0)),composition(meet(converse(converse(sk2)),composition(complement(sk0),sk1)),zero)),
inference(cp,[status(thm)],[t4391,t258946]) ).
cnf(t261803,plain,
composition(meet(sk2,composition(complement(sk0),sk1)),meet(converse(sk1),composition(converse(sk2),complement(sk0)))) = join(meet(converse(composition(sk1,converse(sk2))),complement(sk0)),composition(meet(converse(converse(sk2)),composition(complement(sk0),sk1)),zero)),
inference(step,[status(thm)],[t258974,t21]) ).
cnf(t261804,plain,
composition(zero,meet(converse(sk1),composition(converse(sk2),complement(sk0)))) = join(meet(converse(composition(sk1,converse(sk2))),complement(sk0)),composition(meet(converse(converse(sk2)),composition(complement(sk0),sk1)),zero)),
inference(step,[status(thm)],[t261803,t2129]) ).
cnf(t261805,plain,
zero = join(meet(converse(composition(sk1,converse(sk2))),complement(sk0)),composition(meet(converse(converse(sk2)),composition(complement(sk0),sk1)),zero)),
inference(step,[status(thm)],[t261804,t15550]) ).
cnf(t261806,plain,
zero = join(meet(complement(sk0),converse(composition(sk1,converse(sk2)))),composition(meet(converse(converse(sk2)),composition(complement(sk0),sk1)),zero)),
inference(step,[status(thm)],[t261805,t106]) ).
cnf(t261807,plain,
zero = join(meet(complement(sk0),composition(sk2,converse(sk1))),composition(meet(converse(converse(sk2)),composition(complement(sk0),sk1)),zero)),
inference(step,[status(thm)],[t261806,t141]) ).
cnf(t261808,plain,
zero = join(meet(complement(sk0),composition(sk2,converse(sk1))),zero),
inference(step,[status(thm)],[t261807,t15255]) ).
cnf(t261809,plain,
zero = meet(complement(sk0),composition(sk2,converse(sk1))),
inference(step,[status(thm)],[t261808,t15768]) ).
cnf(t258991,plain,
meet(complement(sk0),composition(sk2,converse(sk1))) = zero,
inference(orient,[status(thm)],[t261809]) ).
cnf(t258993,plain,
join(complement(complement(sk0)),composition(sk2,converse(sk1))) = join(complement(complement(sk0)),zero),
inference(cp,[status(thm)],[t23355,t258991]) ).
cnf(t261810,plain,
join(sk0,composition(sk2,converse(sk1))) = join(complement(complement(sk0)),zero),
inference(step,[status(thm)],[t258993,t15819]) ).
cnf(t261811,plain,
join(sk0,composition(sk2,converse(sk1))) = complement(complement(sk0)),
inference(step,[status(thm)],[t261810,t15768]) ).
cnf(t261812,plain,
join(sk0,composition(sk2,converse(sk1))) = sk0,
inference(step,[status(thm)],[t261811,t15819]) ).
cnf(t259038,plain,
join(sk0,composition(sk2,converse(sk1))) = sk0,
inference(orient,[status(thm)],[t261812]) ).
cnf(c17,plain,
join(composition(sk2,converse(sk1)),sk0) != sk0,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
join(composition(sk2,converse(sk1)),sk0) != sk0,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
join(sk0,composition(sk2,converse(sk1))) != sk0,
inference(rw,[status(thm)],[goal_0,t43]) ).
cnf(g0_1,plain,
sk0 != sk0,
inference(rw,[status(thm)],[g0_0,t259038]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL044+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.38 % Computer : n016.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Thu Sep 24 07:41:11 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 107.79/16.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 107.79/16.06 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------