%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL010+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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:34:41 PM UTC 2026
% Result : Theorem 18.16s 8.92s
% Output : Proof 18.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 140
% Number of leaves : 15
% Syntax : Number of formulae : 464 ( 460 unt; 0 def)
% Number of atoms : 468 ( 467 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 6 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 7 ( 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 : 645 ( 128 sgn 90 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(t27,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]) ).
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(t33,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)],[t27,t21]) ).
cnf(t32620,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)],[t33,t21]) ).
cnf(t6440,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)],[t32620]) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f3_nnf,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t83,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f10_nnf,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t12,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f0_nnf,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(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]) ).
cnf(t32287,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)],[t32287]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f9_nnf,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t7,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t34,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t36,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t34,t21]) ).
cnf(t155,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t36]) ).
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(t156,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t155,t17]) ).
cnf(t32293,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t156,t21]) ).
cnf(t168,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t32293]) ).
cnf(t169,plain,
one = converse(one),
inference(cp,[status(thm)],[t168,t17]) ).
cnf(t178,plain,
converse(one) = one,
inference(orient,[status(thm)],[t169]) ).
cnf(t32294,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t168,t178]) ).
cnf(t188,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t32294]) ).
cnf(t189,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t188]) ).
cnf(t192,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t54,t189]) ).
cnf(t32296,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t192,t178]) ).
cnf(t32297,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t32296,t189]) ).
cnf(t218,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t32297]) ).
cnf(t228,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t83,t218]) ).
cnf(t235,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t228]) ).
cnf(t245,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t83,t235]) ).
cnf(t1080,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t245]) ).
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(t32817,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t45,t43]) ).
cnf(t32818,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t32817,t83]) ).
cnf(t32819,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t32818,t43]) ).
cnf(t15116,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t32819]) ).
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(t90,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t15117,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t15116,t90]) ).
cnf(t32930,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t15117,t83]) ).
cnf(t15796,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t32930]) ).
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(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(t84,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t83,t51]) ).
cnf(t32288,plain,
zero = complement(top),
inference(step,[status(thm)],[t84,t90]) ).
cnf(t99,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t32288]) ).
cnf(t222,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t218,t99]) ).
cnf(t32298,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t222,t99]) ).
cnf(t32299,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t32298,t99]) ).
cnf(t229,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t32299]) ).
cnf(t230,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t46,t229]) ).
cnf(t248,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t230]) ).
cnf(t15801,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t248,t15796]) ).
cnf(t32932,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t15801,t15796]) ).
cnf(t15816,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t32932]) ).
cnf(t32937,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t15796,t15816]) ).
cnf(t15842,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t32937]) ).
cnf(t15869,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t15842]) ).
cnf(t32957,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1080,t15869]) ).
cnf(t15902,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t32957]) ).
cnf(t16265,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t15902]) ).
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(t78,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t82,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t46,t78]) ).
cnf(t1809,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t82]) ).
cnf(t53,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t46,t51]) ).
cnf(t317,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t53]) ).
cnf(t326,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t317,t43]) ).
cnf(t243,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t51,t235]) ).
cnf(t259,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t243]) ).
cnf(t321,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t317,t259]) ).
cnf(t323,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t317,t218]) ).
cnf(t32304,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t323,t51]) ).
cnf(t334,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t32304]) ).
cnf(t335,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t334,t83]) ).
cnf(t351,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t335]) ).
cnf(t32306,plain,
top = join(X1,top),
inference(step,[status(thm)],[t321,t351]) ).
cnf(t357,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t32306]) ).
cnf(t358,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t357,t43]) ).
cnf(t363,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t358]) ).
cnf(t32315,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t326,t363]) ).
cnf(t407,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t32315]) ).
cnf(t1813,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t1809,t407]) ).
cnf(t32401,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t1813,t43]) ).
cnf(t1863,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t32401]) ).
cnf(t1896,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t1863,t78]) ).
cnf(t32402,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t1896,t21]) ).
cnf(t32403,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t32402,t21]) ).
cnf(t1909,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t32403]) ).
cnf(t1939,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t1909,t43]) ).
cnf(t1942,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t1939]) ).
cnf(t16274,plain,
meet(X1,complement(join(X2,X1))) = complement(top),
inference(cp,[status(thm)],[t16265,t1942]) ).
cnf(t32988,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(step,[status(thm)],[t16274,t99]) ).
cnf(t16391,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t32988]) ).
cnf(t219,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t218,t83]) ).
cnf(t32317,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t219,t83]) ).
cnf(t32318,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t32317,t83]) ).
cnf(t443,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t32318]) ).
cnf(t85,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t83,t43]) ).
cnf(t32290,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t85,t83]) ).
cnf(t108,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t32290]) ).
cnf(t444,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t443,t108]) ).
cnf(t464,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t444]) ).
cnf(t15870,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t464,t15869]) ).
cnf(t32973,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t15870,t15869]) ).
cnf(t32974,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t32973,t15869]) ).
cnf(t15936,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t32974]) ).
cnf(t15940,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t46,t15936]) ).
cnf(t15983,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t15940]) ).
cnf(t15999,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t15983,t15116]) ).
cnf(t32978,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t15999,t15116]) ).
cnf(t32979,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t32978,t43]) ).
cnf(t16008,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t32979]) ).
cnf(t16014,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t46,t16008]) ).
cnf(t18293,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t16014]) ).
cnf(t18306,plain,
join(X1,meet(meet(X1,X2),X3)) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t18293,t16008]) ).
cnf(t33032,plain,
join(X1,meet(meet(X1,X2),X3)) = X1,
inference(step,[status(thm)],[t18306,t16008]) ).
cnf(t18362,plain,
join(X1,meet(meet(X1,X2),X3)) = X1,
inference(orient,[status(thm)],[t33032]) ).
cnf(t102,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t83,t99]) ).
cnf(t122,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t102]) ).
cnf(t81,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t78,t21]) ).
cnf(t281,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t81]) ).
cnf(t80,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t78,t21]) ).
cnf(t264,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t80]) ).
cnf(t266,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t264,t51]) ).
cnf(t300,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t266]) ).
cnf(t366,plain,
top = converse(top),
inference(cp,[status(thm)],[t363,t300]) ).
cnf(t369,plain,
converse(top) = top,
inference(orient,[status(thm)],[t366]) ).
cnf(t374,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t34,t369]) ).
cnf(t381,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t374]) ).
cnf(t387,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t281,t381]) ).
cnf(t9624,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t387]) ).
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(t37,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t24,t34]) ).
cnf(t7865,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t37]) ).
cnf(t9625,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t9624,t7865]) ).
cnf(t32704,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t9625,t21]) ).
cnf(t35,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t34,t21]) ).
cnf(t145,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t35]) ).
cnf(t32705,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t32704,t145]) ).
cnf(t32706,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t32705,t264]) ).
cnf(t32707,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t32706,t369]) ).
cnf(t32708,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t32707,t357]) ).
cnf(t9706,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t32708]) ).
cnf(t375,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t34,t369]) ).
cnf(t395,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t375]) ).
cnf(t383,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t78,t381]) ).
cnf(t4219,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t383]) ).
cnf(t4231,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t4219,t369]) ).
cnf(t4265,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t4231]) ).
cnf(t4269,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t4265,t24]) ).
cnf(t32491,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t4269,t381]) ).
cnf(t32492,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t32491,t381]) ).
cnf(t32493,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t32492,t363]) ).
cnf(t32494,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t32493,t369]) ).
cnf(t4385,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t32494]) ).
cnf(t4401,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t4385,t178]) ).
cnf(t32495,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t4401,t17]) ).
cnf(t32496,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t32495,t357]) ).
cnf(t4414,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t32496]) ).
cnf(t4419,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t4414]) ).
cnf(t32504,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t4419,t99]) ).
cnf(t32505,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t32504,t99]) ).
cnf(t32506,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t32505,t369]) ).
cnf(t32507,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t32506,t99]) ).
cnf(t28,plain,
composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t27,t17]) ).
cnf(t32381,plain,
composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t28,t178]) ).
cnf(t32382,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t32381,t17]) ).
cnf(t32383,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t32382,t178]) ).
cnf(t32384,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t32383,t17]) ).
cnf(t1680,plain,
join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))) = composition(meet(X1,X2),meet(one,composition(converse(X1),X2))),
inference(orient,[status(thm)],[t32384]) ).
cnf(t56,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t54,t17]) ).
cnf(t1153,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(top,complement(top))),
inference(cp,[status(thm)],[t1153,t369]) ).
cnf(t32347,plain,
complement(one) = join(complement(one),composition(top,zero)),
inference(step,[status(thm)],[t1158,t99]) ).
cnf(t1178,plain,
join(complement(one),composition(top,zero)) = complement(one),
inference(orient,[status(thm)],[t32347]) ).
cnf(t1954,plain,
top = join(complement(composition(top,zero)),complement(one)),
inference(cp,[status(thm)],[t1942,t1178]) ).
cnf(t32404,plain,
top = join(complement(one),complement(composition(top,zero))),
inference(step,[status(thm)],[t1954,t43]) ).
cnf(t1982,plain,
join(complement(one),complement(composition(top,zero))) = top,
inference(orient,[status(thm)],[t32404]) ).
cnf(t1984,plain,
meet(one,composition(top,zero)) = complement(top),
inference(cp,[status(thm)],[t83,t1982]) ).
cnf(t32405,plain,
meet(one,composition(top,zero)) = zero,
inference(step,[status(thm)],[t1984,t99]) ).
cnf(t1990,plain,
meet(one,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t32405]) ).
cnf(t1996,plain,
composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(cp,[status(thm)],[t1680,t1990]) ).
cnf(t32406,plain,
composition(zero,meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t1996,t1990]) ).
cnf(t32407,plain,
composition(zero,meet(one,composition(one,composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t32406,t178]) ).
cnf(t32408,plain,
composition(zero,meet(one,composition(top,zero))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t32407,t189]) ).
cnf(t32409,plain,
composition(zero,zero) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t32408,t1990]) ).
cnf(t32410,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t32409,t1990]) ).
cnf(t32411,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(one,composition(top,zero))))),
inference(step,[status(thm)],[t32410,t178]) ).
cnf(t32412,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(top,zero)))),
inference(step,[status(thm)],[t32411,t189]) ).
cnf(t32413,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t32412,t1990]) ).
cnf(t1998,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t32413]) ).
cnf(t2001,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t46,t1998]) ).
cnf(t2392,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t2001]) ).
cnf(t2400,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t2392,t24]) ).
cnf(t32430,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t2400,t24]) ).
cnf(t2516,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t32430]) ).
cnf(t250,plain,
join(zero,X1) = join(zero,join(X1,zero)),
inference(cp,[status(thm)],[t248,t43]) ).
cnf(t251,plain,
join(zero,join(X1,zero)) = join(zero,X1),
inference(orient,[status(thm)],[t250]) ).
cnf(t254,plain,
join(zero,join(join(X1,zero),X2)) = join(join(zero,X1),X2),
inference(cp,[status(thm)],[t46,t251]) ).
cnf(t32348,plain,
join(zero,join(X1,join(zero,X2))) = join(join(zero,X1),X2),
inference(step,[status(thm)],[t254,t46]) ).
cnf(t32349,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(step,[status(thm)],[t32348,t46]) ).
cnf(t1210,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(orient,[status(thm)],[t32349]) ).
cnf(t86,plain,
top = join(join(complement(X1),complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t51,t83]) ).
cnf(t32352,plain,
top = join(complement(X1),join(complement(X2),meet(X1,X2))),
inference(step,[status(thm)],[t86,t46]) ).
cnf(t1301,plain,
join(complement(X1),join(complement(X2),meet(X1,X2))) = top,
inference(orient,[status(thm)],[t32352]) ).
fof(f16,conjecture,
! [X0,X1,X2] :
( meet(composition(X0,X1),X2) = zero
=> meet(X1,composition(converse(X0),X2)) = zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( meet(composition(X0,X1),X2) = zero
=> meet(X1,composition(converse(X0),X2)) = zero ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1,X2] :
( meet(X1,composition(converse(X0),X2)) != zero
& meet(composition(X0,X1),X2) = zero ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( meet(sk1,composition(converse(sk0),sk2)) != zero
& meet(composition(sk0,sk1),sk2) = zero ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f16_nnf]) ).
cnf(c16,plain,
meet(composition(sk0,sk1),sk2) = zero,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t5,plain,
meet(composition(sk0,sk1),sk2) = zero,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t95,plain,
meet(composition(sk0,sk1),sk2) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t113,plain,
meet(composition(sk0,sk1),sk2) = zero,
inference(rw,[status(thm)],[t95]) ).
cnf(t32292,plain,
meet(sk2,composition(sk0,sk1)) = zero,
inference(step,[status(thm)],[t113,t108]) ).
cnf(t117,plain,
meet(sk2,composition(sk0,sk1)) = zero,
inference(orient,[status(thm)],[t32292]) ).
cnf(t1320,plain,
top = join(complement(sk2),join(complement(composition(sk0,sk1)),zero)),
inference(cp,[status(thm)],[t1301,t117]) ).
cnf(t32375,plain,
top = join(complement(sk2),join(zero,complement(composition(sk0,sk1)))),
inference(step,[status(thm)],[t1320,t43]) ).
cnf(t1568,plain,
join(complement(sk2),join(zero,complement(composition(sk0,sk1)))) = top,
inference(orient,[status(thm)],[t32375]) ).
cnf(t1570,plain,
join(zero,join(complement(sk2),complement(composition(sk0,sk1)))) = join(zero,top),
inference(cp,[status(thm)],[t1210,t1568]) ).
cnf(t101,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t51,t99]) ).
cnf(t32289,plain,
top = join(zero,top),
inference(step,[status(thm)],[t101,t43]) ).
cnf(t106,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t32289]) ).
cnf(t32390,plain,
join(zero,join(complement(sk2),complement(composition(sk0,sk1)))) = top,
inference(step,[status(thm)],[t1570,t106]) ).
cnf(t1735,plain,
join(zero,join(complement(sk2),complement(composition(sk0,sk1)))) = top,
inference(orient,[status(thm)],[t32390]) ).
cnf(t2519,plain,
composition(join(zero,join(complement(sk2),complement(composition(sk0,sk1)))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t2516,t1735]) ).
cnf(t32431,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t2519,t1735]) ).
cnf(t2546,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t32431]) ).
cnf(t32508,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t32507,t2546]) ).
cnf(t4431,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t32508]) ).
cnf(t4432,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t395,t4431]) ).
cnf(t4452,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t4432]) ).
cnf(t9759,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t9706,t4452]) ).
cnf(t32733,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t9759,t4452]) ).
cnf(t32734,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t32733,t43]) ).
cnf(t10513,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t32734]) ).
cnf(t2536,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t2516,t43]) ).
cnf(t2597,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t2536]) ).
cnf(t4433,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t24,t4431]) ).
cnf(t32515,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t4433,t363]) ).
cnf(t32516,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t32515,t4431]) ).
cnf(t4570,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t32516]) ).
cnf(t32519,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t2597,t4570]) ).
cnf(t4588,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t32519]) ).
cnf(t4630,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t4588]) ).
cnf(t4633,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t4630,t43]) ).
cnf(t4652,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t4633]) ).
cnf(t4654,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t24,t4652]) ).
cnf(t32541,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t4654,t46]) ).
cnf(t32542,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t32541,t4570]) ).
cnf(t4854,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t32542]) ).
cnf(t179,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t78,t178]) ).
cnf(t195,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t179]) ).
cnf(t201,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t155,t195]) ).
cnf(t3983,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t201]) ).
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(t827,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t4417,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t827,t4414]) ).
cnf(t32607,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t4417,t24]) ).
cnf(t6204,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t32607]) ).
cnf(t6211,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t6204,t189]) ).
cnf(t32608,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t6211,t357]) ).
cnf(t32609,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t32608,t4414]) ).
cnf(t6234,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t32609]) ).
cnf(t6236,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t6234,t43]) ).
cnf(t6257,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t6236]) ).
cnf(t6268,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t3983,t6257]) ).
cnf(t32612,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t6268,t369]) ).
cnf(t32613,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t32612,t369]) ).
cnf(t6292,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t32613]) ).
cnf(t6293,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t6292,t43]) ).
cnf(t6308,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t6293]) ).
cnf(t6314,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t54,t6308]) ).
cnf(t32633,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t6314,t369]) ).
cnf(t32634,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t32633,t43]) ).
cnf(t32635,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t32634,t99]) ).
cnf(t32636,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t32635,t4431]) ).
cnf(t7022,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t32636]) ).
cnf(t7031,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t4854,t7022]) ).
cnf(t7271,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t7031]) ).
cnf(t15333,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t7271,t15116]) ).
cnf(t15338,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t15333]) ).
cnf(t15345,plain,
converse(zero) = join(converse(zero),zero),
inference(cp,[status(thm)],[t10513,t15338]) ).
cnf(t32865,plain,
converse(zero) = join(zero,converse(zero)),
inference(step,[status(thm)],[t15345,t43]) ).
cnf(t15500,plain,
join(zero,converse(zero)) = converse(zero),
inference(orient,[status(thm)],[t32865]) ).
cnf(t15510,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t281,t15500]) ).
cnf(t32866,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t15510,t43]) ).
cnf(t32867,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t32866,t15500]) ).
cnf(t32868,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t32867,t21]) ).
cnf(t15513,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t32868]) ).
cnf(t15516,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t34,t15513]) ).
cnf(t32900,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t15516,t15338]) ).
cnf(t32901,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t32900,t15513]) ).
cnf(t15597,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t32901]) ).
cnf(t15614,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t15597,t21]) ).
cnf(t15635,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t15614]) ).
cnf(t15646,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t54,t15635]) ).
cnf(t32902,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t15646,t15513]) ).
cnf(t32903,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t32902,t15635]) ).
cnf(t32904,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t32903,t43]) ).
cnf(t15648,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t32904]) ).
cnf(t32917,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t122,t15648]) ).
cnf(t15689,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t32917]) ).
cnf(t15691,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t15689]) ).
cnf(t15822,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t15816,t43]) ).
cnf(t15855,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t15822]) ).
cnf(t15865,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t15116,t15855]) ).
cnf(t1979,plain,
join(complement(X1),join(join(X2,X1),X3)) = join(top,X3),
inference(cp,[status(thm)],[t46,t1942]) ).
cnf(t32419,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t1979,t46]) ).
cnf(t32420,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t32419,t363]) ).
cnf(t2214,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t32420]) ).
cnf(t7032,plain,
top = join(complement(zero),join(X1,complement(join(X2,one)))),
inference(cp,[status(thm)],[t2214,t7022]) ).
cnf(t8785,plain,
join(complement(zero),join(X1,complement(join(X2,one)))) = top,
inference(orient,[status(thm)],[t7032]) ).
cnf(t15332,plain,
top = join(complement(zero),X1),
inference(cp,[status(thm)],[t8785,t15116]) ).
cnf(t15397,plain,
join(complement(zero),X1) = top,
inference(orient,[status(thm)],[t15332]) ).
cnf(t15398,plain,
top = complement(zero),
inference(cp,[status(thm)],[t15397,t54]) ).
cnf(t15440,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t15398]) ).
cnf(t15445,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t83,t15440]) ).
cnf(t32862,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t15445,t357]) ).
cnf(t32863,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t32862,t99]) ).
cnf(t15489,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t32863]) ).
cnf(t32960,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t15865,t15489]) ).
cnf(t32961,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t32960,t15648]) ).
cnf(t32962,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t32961,t15691]) ).
cnf(t15905,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t32962]) ).
cnf(t32963,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t15691,t15905]) ).
cnf(t15906,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t32963]) ).
cnf(t16010,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t16008,t108]) ).
cnf(t16035,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t16010]) ).
cnf(t16316,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t16265,t15906]) ).
cnf(t16589,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t16316]) ).
cnf(t16596,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t16035,t16589]) ).
cnf(t124,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t122,t83]) ).
cnf(t3514,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t124]) ).
cnf(t32933,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t3514,t15816]) ).
cnf(t15817,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t32933]) ).
cnf(t32969,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t15817,t15905]) ).
cnf(t15933,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t32969]) ).
cnf(t16535,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t15933]) ).
cnf(t32992,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t16596,t16535]) ).
cnf(t16741,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t32992]) ).
cnf(t16771,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t15906,t16741]) ).
cnf(t32993,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t16771,t15906]) ).
cnf(t16829,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t32993]) ).
cnf(t16832,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t16829,t16035]) ).
cnf(t32995,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t16832,t108]) ).
cnf(t16973,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t32995]) ).
cnf(t18366,plain,
X1 = join(X1,meet(meet(X2,X1),X3)),
inference(cp,[status(thm)],[t18362,t16973]) ).
cnf(t18422,plain,
join(X1,meet(meet(X2,X1),X3)) = X1,
inference(orient,[status(thm)],[t18366]) ).
cnf(t18447,plain,
zero = meet(meet(meet(X1,X2),X3),complement(X2)),
inference(cp,[status(thm)],[t16391,t18422]) ).
cnf(t33150,plain,
zero = meet(complement(X2),meet(meet(X1,X2),X3)),
inference(step,[status(thm)],[t18447,t108]) ).
cnf(t28054,plain,
meet(complement(X1),meet(meet(X2,X1),X3)) = zero,
inference(orient,[status(thm)],[t33150]) ).
cnf(t32986,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t15116,t16265]) ).
cnf(t16381,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t32986]) ).
cnf(t21739,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t16381]) ).
cnf(t21765,plain,
sk2 = join(zero,meet(sk2,complement(composition(sk0,sk1)))),
inference(cp,[status(thm)],[t21739,t117]) ).
cnf(t33065,plain,
sk2 = meet(sk2,complement(composition(sk0,sk1))),
inference(step,[status(thm)],[t21765,t15816]) ).
cnf(t21848,plain,
meet(sk2,complement(composition(sk0,sk1))) = sk2,
inference(orient,[status(thm)],[t33065]) ).
cnf(t28109,plain,
zero = meet(complement(complement(composition(sk0,sk1))),meet(sk2,X1)),
inference(cp,[status(thm)],[t28054,t21848]) ).
cnf(t33151,plain,
zero = meet(composition(sk0,sk1),meet(sk2,X1)),
inference(step,[status(thm)],[t28109,t15906]) ).
cnf(t28118,plain,
meet(composition(sk0,sk1),meet(sk2,X1)) = zero,
inference(orient,[status(thm)],[t33151]) ).
cnf(t28119,plain,
zero = meet(meet(sk2,X1),composition(sk0,sk1)),
inference(cp,[status(thm)],[t28118,t108]) ).
cnf(t28149,plain,
meet(meet(sk2,X1),composition(sk0,sk1)) = zero,
inference(orient,[status(thm)],[t28119]) ).
cnf(t28157,plain,
composition(meet(converse(sk0),composition(sk1,converse(meet(sk2,X1)))),meet(meet(sk2,X1),composition(sk0,sk1))) = join(meet(composition(converse(sk0),meet(sk2,X1)),sk1),composition(meet(converse(sk0),composition(sk1,converse(meet(sk2,X1)))),zero)),
inference(cp,[status(thm)],[t6440,t28149]) ).
cnf(t33215,plain,
composition(meet(converse(sk0),composition(sk1,converse(meet(sk2,X1)))),zero) = join(meet(composition(converse(sk0),meet(sk2,X1)),sk1),composition(meet(converse(sk0),composition(sk1,converse(meet(sk2,X1)))),zero)),
inference(step,[status(thm)],[t28157,t28149]) ).
cnf(t33216,plain,
zero = join(meet(composition(converse(sk0),meet(sk2,X1)),sk1),composition(meet(converse(sk0),composition(sk1,converse(meet(sk2,X1)))),zero)),
inference(step,[status(thm)],[t33215,t15338]) ).
cnf(t33217,plain,
zero = join(meet(sk1,composition(converse(sk0),meet(sk2,X1))),composition(meet(converse(sk0),composition(sk1,converse(meet(sk2,X1)))),zero)),
inference(step,[status(thm)],[t33216,t108]) ).
cnf(t33218,plain,
zero = join(meet(sk1,composition(converse(sk0),meet(sk2,X1))),zero),
inference(step,[status(thm)],[t33217,t15338]) ).
cnf(t33219,plain,
zero = meet(sk1,composition(converse(sk0),meet(sk2,X1))),
inference(step,[status(thm)],[t33218,t15855]) ).
cnf(t32232,plain,
meet(sk1,composition(converse(sk0),meet(sk2,X1))) = zero,
inference(orient,[status(thm)],[t33219]) ).
cnf(t16852,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t16829,t43]) ).
cnf(t16866,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t16852]) ).
cnf(t9710,plain,
composition(X1,top) = join(X1,composition(X1,top)),
inference(cp,[status(thm)],[t9706,t17]) ).
cnf(t9810,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t9710]) ).
cnf(t9821,plain,
join(X1,join(composition(X1,top),X2)) = join(composition(X1,top),X2),
inference(cp,[status(thm)],[t46,t9810]) ).
cnf(t13821,plain,
join(X1,join(composition(X1,top),X2)) = join(composition(X1,top),X2),
inference(orient,[status(thm)],[t9821]) ).
cnf(t16867,plain,
X1 = meet(X1,join(composition(X1,top),X2)),
inference(cp,[status(thm)],[t16866,t13821]) ).
cnf(t17641,plain,
meet(X1,join(composition(X1,top),X2)) = X1,
inference(orient,[status(thm)],[t16867]) ).
cnf(t17642,plain,
X1 = meet(X1,composition(join(X1,X2),top)),
inference(cp,[status(thm)],[t17641,t24]) ).
cnf(t17917,plain,
meet(X1,composition(join(X1,X2),top)) = X1,
inference(orient,[status(thm)],[t17642]) ).
cnf(t17943,plain,
X1 = meet(X1,composition(join(X2,X1),top)),
inference(cp,[status(thm)],[t17917,t43]) ).
cnf(t18066,plain,
meet(X1,composition(join(X2,X1),top)) = X1,
inference(orient,[status(thm)],[t17943]) ).
cnf(t18075,plain,
meet(X1,X2) = meet(meet(X1,X2),composition(X2,top)),
inference(cp,[status(thm)],[t18066,t16035]) ).
cnf(t19027,plain,
meet(meet(X1,X2),composition(X2,top)) = meet(X1,X2),
inference(orient,[status(thm)],[t18075]) ).
cnf(t19028,plain,
meet(X1,X2) = meet(composition(X2,top),meet(X1,X2)),
inference(cp,[status(thm)],[t19027,t108]) ).
cnf(t19989,plain,
meet(composition(X1,top),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t19028]) ).
cnf(t21856,plain,
meet(sk2,complement(composition(sk0,sk1))) = meet(composition(complement(composition(sk0,sk1)),top),sk2),
inference(cp,[status(thm)],[t19989,t21848]) ).
cnf(t33167,plain,
sk2 = meet(composition(complement(composition(sk0,sk1)),top),sk2),
inference(step,[status(thm)],[t21856,t21848]) ).
cnf(t33168,plain,
sk2 = meet(sk2,composition(complement(composition(sk0,sk1)),top)),
inference(step,[status(thm)],[t33167,t108]) ).
cnf(t30889,plain,
meet(sk2,composition(complement(composition(sk0,sk1)),top)) = sk2,
inference(orient,[status(thm)],[t33168]) ).
cnf(t32233,plain,
zero = meet(sk1,composition(converse(sk0),sk2)),
inference(cp,[status(thm)],[t32232,t30889]) ).
cnf(t32271,plain,
meet(sk1,composition(converse(sk0),sk2)) = zero,
inference(orient,[status(thm)],[t32233]) ).
cnf(c17,plain,
meet(sk1,composition(converse(sk0),sk2)) != zero,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
meet(sk1,composition(converse(sk0),sk2)) != zero,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
zero != zero,
inference(rw,[status(thm)],[goal_0,t32271]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL010+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.58 % Computer : n008.cluster.edu
% 0.10/5.58 % Model : x86_64 x86_64
% 0.10/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.58 % Memory : 8046.5625MB
% 0.10/5.58 % OS : Linux 6.8.0-71-generic
% 0.10/5.59 % CPULimit : 300
% 0.10/5.59 % WCLimit : 300
% 0.10/5.59 % DateTime : Thu Sep 24 07:08:18 UTC 2026
% 0.10/5.59 % CPUTime :
% 0.10/5.59 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 18.16/8.92 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.16/8.92 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------