%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL005-3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.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:38 PM UTC 2026
% Result : Unsatisfiable 17.13s 7.61s
% Output : CNFRefutation 17.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 130
% Number of leaves : 15
% Syntax : Number of clauses : 387 ( 387 unt; 0 nHn; 46 RR)
% Number of literals : 387 ( 386 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 508 ( 88 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t26073,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t42]) ).
cnf(t53,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t26073]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t28,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t26,t20]) ).
cnf(t148,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t28]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t149,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t148,t16]) ).
cnf(t26078,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t149,t20]) ).
cnf(t161,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t26078]) ).
cnf(t162,plain,
one = converse(one),
inference(cp,[status(thm)],[t161,t16]) ).
cnf(t171,plain,
converse(one) = one,
inference(orient,[status(thm)],[t162]) ).
cnf(t26079,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t161,t171]) ).
cnf(t181,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t26079]) ).
cnf(t182,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t181]) ).
cnf(t185,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t53,t182]) ).
cnf(t26081,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t185,t171]) ).
cnf(t26082,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t26081,t182]) ).
cnf(t211,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t26082]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t82,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t212,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t211,t82]) ).
cnf(t26102,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t212,t82]) ).
cnf(t26103,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t26102,t82]) ).
cnf(t435,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t26103]) ).
cnf(t84,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t82,t42]) ).
cnf(t26076,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t84,t82]) ).
cnf(t103,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t26076]) ).
cnf(t436,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t435,t103]) ).
cnf(t456,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t436]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t44,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t17]) ).
cnf(t26618,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t44,t42]) ).
cnf(t26619,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t26618,t82]) ).
cnf(t26620,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t26619,t42]) ).
cnf(t15096,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t26620]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t15097,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t15096,t89]) ).
cnf(t26728,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t15097,t82]) ).
cnf(t15771,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t26728]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t83,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t82,t50]) ).
cnf(t26074,plain,
zero = complement(top),
inference(step,[status(thm)],[t83,t89]) ).
cnf(t94,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t26074]) ).
cnf(t215,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t211,t94]) ).
cnf(t26083,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t215,t94]) ).
cnf(t26084,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t26083,t94]) ).
cnf(t222,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t26084]) ).
cnf(t223,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t45,t222]) ).
cnf(t241,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t223]) ).
cnf(t15776,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t241,t15771]) ).
cnf(t26730,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t15776,t15771]) ).
cnf(t15791,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t26730]) ).
cnf(t26735,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t15771,t15791]) ).
cnf(t15817,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t26735]) ).
cnf(t15843,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t15817]) ).
cnf(t15844,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t456,t15843]) ).
cnf(t26770,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t15844,t15843]) ).
cnf(t26771,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t26770,t15843]) ).
cnf(t15910,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t26771]) ).
cnf(t15914,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t45,t15910]) ).
cnf(t15957,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t15914]) ).
cnf(t15973,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t15957,t15096]) ).
cnf(t26775,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t15973,t15096]) ).
cnf(t26776,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t26775,t42]) ).
cnf(t15982,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t26776]) ).
cnf(t15984,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t15982,t103]) ).
cnf(t16009,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t15984]) ).
cnf(t16014,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t45,t16009]) ).
cnf(t18443,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t16014]) ).
cnf(t221,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t82,t211]) ).
cnf(t228,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t221]) ).
cnf(t238,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t82,t228]) ).
cnf(t1070,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t238]) ).
cnf(t26754,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1070,t15843]) ).
cnf(t15876,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t26754]) ).
cnf(t16239,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t15876]) ).
cnf(t26783,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t15096,t16239]) ).
cnf(t16355,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t26783]) ).
cnf(t21675,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t16355]) ).
cnf(t21727,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t18443,t21675]) ).
cnf(t21879,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t21727]) ).
cnf(t21894,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t21879,t103]) ).
cnf(t22548,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t21894]) ).
cnf(t97,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t82,t94]) ).
cnf(t115,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t97]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t59,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t62,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t59,t20]) ).
cnf(t274,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t62]) ).
cnf(t52,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t45,t50]) ).
cnf(t310,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t52]) ).
cnf(t236,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t50,t228]) ).
cnf(t252,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t236]) ).
cnf(t314,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t310,t252]) ).
cnf(t316,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t310,t211]) ).
cnf(t26089,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t316,t50]) ).
cnf(t327,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t26089]) ).
cnf(t328,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t327,t82]) ).
cnf(t335,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t328]) ).
cnf(t26091,plain,
top = join(X1,top),
inference(step,[status(thm)],[t314,t335]) ).
cnf(t349,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t26091]) ).
cnf(t350,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t349,t42]) ).
cnf(t355,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t350]) ).
cnf(t61,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t59,t20]) ).
cnf(t257,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t61]) ).
cnf(t259,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t257,t50]) ).
cnf(t293,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t259]) ).
cnf(t358,plain,
top = converse(top),
inference(cp,[status(thm)],[t355,t293]) ).
cnf(t361,plain,
converse(top) = top,
inference(orient,[status(thm)],[t358]) ).
cnf(t366,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t26,t361]) ).
cnf(t373,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t366]) ).
cnf(t379,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t274,t373]) ).
cnf(t9973,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t379]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t29,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t23,t26]) ).
cnf(t1678,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t29]) ).
cnf(t9974,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t9973,t1678]) ).
cnf(t26509,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t9974,t20]) ).
cnf(t27,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t26,t20]) ).
cnf(t138,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t27]) ).
cnf(t26510,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t26509,t138]) ).
cnf(t26511,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t26510,t257]) ).
cnf(t26512,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t26511,t361]) ).
cnf(t26513,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t26512,t349]) ).
cnf(t10053,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t26513]) ).
cnf(t367,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t26,t361]) ).
cnf(t387,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t367]) ).
cnf(t375,plain,
converse(join(composition(X1,top),X2)) = join(composition(top,converse(X1)),converse(X2)),
inference(cp,[status(thm)],[t59,t373]) ).
cnf(t4081,plain,
join(composition(top,converse(X1)),converse(X2)) = converse(join(composition(X1,top),X2)),
inference(orient,[status(thm)],[t375]) ).
cnf(t4094,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(cp,[status(thm)],[t4081,t361]) ).
cnf(t4128,plain,
converse(join(composition(top,top),X1)) = join(composition(top,top),converse(X1)),
inference(orient,[status(thm)],[t4094]) ).
cnf(t4132,plain,
join(composition(top,top),converse(composition(X1,top))) = converse(composition(join(top,X1),top)),
inference(cp,[status(thm)],[t4128,t23]) ).
cnf(t26277,plain,
join(composition(top,top),composition(top,converse(X1))) = converse(composition(join(top,X1),top)),
inference(step,[status(thm)],[t4132,t373]) ).
cnf(t26278,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(join(top,X1))),
inference(step,[status(thm)],[t26277,t373]) ).
cnf(t26279,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,converse(top)),
inference(step,[status(thm)],[t26278,t355]) ).
cnf(t26280,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(step,[status(thm)],[t26279,t361]) ).
cnf(t4246,plain,
join(composition(top,top),composition(top,converse(X1))) = composition(top,top),
inference(orient,[status(thm)],[t26280]) ).
cnf(t4262,plain,
composition(top,top) = join(composition(top,top),composition(top,one)),
inference(cp,[status(thm)],[t4246,t171]) ).
cnf(t26281,plain,
composition(top,top) = join(composition(top,top),top),
inference(step,[status(thm)],[t4262,t16]) ).
cnf(t26282,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t26281,t349]) ).
cnf(t4275,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t26282]) ).
cnf(t4280,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t53,t4275]) ).
cnf(t26290,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t4280,t94]) ).
cnf(t26291,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t26290,t94]) ).
cnf(t26292,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t26291,t361]) ).
cnf(t26293,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t26292,t94]) ).
cnf(t15,axiom,
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))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,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)],[t15]) ).
cnf(t63,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t45,t59]) ).
cnf(t1754,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t63]) ).
cnf(t319,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t310,t42]) ).
cnf(t26100,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t319,t355]) ).
cnf(t399,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t26100]) ).
cnf(t1758,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t1754,t399]) ).
cnf(t26180,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t1758,t42]) ).
cnf(t1809,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t26180]) ).
cnf(t1842,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t1809,t59]) ).
cnf(t26181,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t1842,t20]) ).
cnf(t26182,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t26181,t20]) ).
cnf(t1855,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t26182]) ).
cnf(t1885,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t1855,t42]) ).
cnf(t1888,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t1885]) ).
cnf(t55,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t53,t16]) ).
cnf(t1143,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t55]) ).
cnf(t1153,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1143,t20]) ).
cnf(t1171,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1153]) ).
cnf(t1899,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t1888,t1171]) ).
cnf(t26193,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t1899,t42]) ).
cnf(t2236,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t26193]) ).
cnf(t2251,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t82,t2236]) ).
cnf(t26194,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t2251,t94]) ).
cnf(t2257,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t26194]) ).
cnf(t2278,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)],[t32,t2257]) ).
cnf(t26195,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)],[t2278,t20]) ).
cnf(t26196,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)],[t26195,t171]) ).
cnf(t26197,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)],[t26196,t16]) ).
cnf(t26198,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)],[t26197,t89]) ).
cnf(t26199,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)],[t26198,t2257]) ).
cnf(t26200,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)],[t26199,t16]) ).
cnf(t26201,plain,
composition(zero,zero) = join(meet(X1,complement(X1)),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t26200,t20]) ).
cnf(t26202,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t26201,t89]) ).
cnf(t26203,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),converse(one))),zero)),
inference(step,[status(thm)],[t26202,t20]) ).
cnf(t26204,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(X1),one)),zero)),
inference(step,[status(thm)],[t26203,t171]) ).
cnf(t26205,plain,
composition(zero,zero) = join(zero,composition(meet(X1,complement(X1)),zero)),
inference(step,[status(thm)],[t26204,t16]) ).
cnf(t26206,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t26205,t89]) ).
cnf(t2279,plain,
join(zero,composition(zero,zero)) = composition(zero,zero),
inference(orient,[status(thm)],[t26206]) ).
cnf(t2282,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(cp,[status(thm)],[t45,t2279]) ).
cnf(t2384,plain,
join(zero,join(composition(zero,zero),X1)) = join(composition(zero,zero),X1),
inference(orient,[status(thm)],[t2282]) ).
cnf(t2392,plain,
join(composition(zero,zero),composition(X1,zero)) = join(zero,composition(join(zero,X1),zero)),
inference(cp,[status(thm)],[t2384,t23]) ).
cnf(t26215,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(zero,X1),zero)),
inference(step,[status(thm)],[t2392,t23]) ).
cnf(t2455,plain,
join(zero,composition(join(zero,X1),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t26215]) ).
cnf(t51,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t50,t45]) ).
cnf(t468,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t51]) ).
cnf(t485,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t468,t42]) ).
cnf(t569,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t485]) ).
cnf(t581,plain,
top = join(complement(X1),join(X1,complement(top))),
inference(cp,[status(thm)],[t569,t50]) ).
cnf(t26111,plain,
top = join(complement(X1),join(X1,zero)),
inference(step,[status(thm)],[t581,t94]) ).
cnf(t601,plain,
join(complement(X1),join(X1,zero)) = top,
inference(orient,[status(thm)],[t26111]) ).
cnf(t608,plain,
top = join(complement(X1),join(zero,X1)),
inference(cp,[status(thm)],[t601,t42]) ).
cnf(t610,plain,
join(complement(X1),join(zero,X1)) = top,
inference(orient,[status(thm)],[t608]) ).
cnf(t99,plain,
complement(top) = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(cp,[status(thm)],[t53,t94]) ).
cnf(t26139,plain,
zero = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(step,[status(thm)],[t99,t94]) ).
cnf(t1344,plain,
join(zero,composition(converse(X1),complement(composition(X1,top)))) = zero,
inference(orient,[status(thm)],[t26139]) ).
cnf(t1349,plain,
zero = join(zero,composition(top,complement(composition(top,top)))),
inference(cp,[status(thm)],[t1344,t361]) ).
cnf(t1366,plain,
join(zero,composition(top,complement(composition(top,top)))) = zero,
inference(orient,[status(thm)],[t1349]) ).
cnf(t1368,plain,
top = join(complement(composition(top,complement(composition(top,top)))),zero),
inference(cp,[status(thm)],[t610,t1366]) ).
cnf(t26160,plain,
top = join(zero,complement(composition(top,complement(composition(top,top))))),
inference(step,[status(thm)],[t1368,t42]) ).
cnf(t1608,plain,
join(zero,complement(composition(top,complement(composition(top,top))))) = top,
inference(orient,[status(thm)],[t26160]) ).
cnf(t2458,plain,
composition(join(zero,complement(composition(top,complement(composition(top,top))))),zero) = join(zero,composition(top,zero)),
inference(cp,[status(thm)],[t2455,t1608]) ).
cnf(t26216,plain,
composition(top,zero) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t2458,t1608]) ).
cnf(t2484,plain,
join(zero,composition(top,zero)) = composition(top,zero),
inference(orient,[status(thm)],[t26216]) ).
cnf(t26294,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t26293,t2484]) ).
cnf(t4286,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t26294]) ).
cnf(t4287,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t387,t4286]) ).
cnf(t4303,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t4287]) ).
cnf(t10105,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t10053,t4303]) ).
cnf(t26542,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t10105,t4303]) ).
cnf(t26543,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t26542,t42]) ).
cnf(t11080,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t26543]) ).
cnf(t2474,plain,
composition(join(zero,X1),zero) = join(zero,composition(join(X1,zero),zero)),
inference(cp,[status(thm)],[t2455,t42]) ).
cnf(t2565,plain,
join(zero,composition(join(X1,zero),zero)) = composition(join(zero,X1),zero),
inference(orient,[status(thm)],[t2474]) ).
cnf(t4288,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t23,t4286]) ).
cnf(t26300,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t4288,t355]) ).
cnf(t26301,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t26300,t4286]) ).
cnf(t4322,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t26301]) ).
cnf(t26304,plain,
zero = composition(join(zero,X1),zero),
inference(step,[status(thm)],[t2565,t4322]) ).
cnf(t4340,plain,
zero = composition(join(zero,X1),zero),
inference(rw,[status(thm)],[t26304]) ).
cnf(t4372,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t4340]) ).
cnf(t4375,plain,
zero = composition(join(X1,zero),zero),
inference(cp,[status(thm)],[t4372,t42]) ).
cnf(t4389,plain,
composition(join(X1,zero),zero) = zero,
inference(orient,[status(thm)],[t4375]) ).
cnf(t4391,plain,
composition(join(join(X1,zero),X2),zero) = join(zero,composition(X2,zero)),
inference(cp,[status(thm)],[t23,t4389]) ).
cnf(t26330,plain,
composition(join(X1,join(zero,X2)),zero) = join(zero,composition(X2,zero)),
inference(step,[status(thm)],[t4391,t45]) ).
cnf(t26331,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(step,[status(thm)],[t26330,t4322]) ).
cnf(t4675,plain,
composition(join(X1,join(zero,X2)),zero) = zero,
inference(orient,[status(thm)],[t26331]) ).
cnf(t172,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t59,t171]) ).
cnf(t188,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t172]) ).
cnf(t194,plain,
composition(converse(X1),join(one,X2)) = converse(composition(join(one,converse(X2)),X1)),
inference(cp,[status(thm)],[t148,t188]) ).
cnf(t3851,plain,
converse(composition(join(one,converse(X1)),X2)) = composition(converse(X2),join(one,X1)),
inference(orient,[status(thm)],[t194]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t25,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t23,t21]) ).
cnf(t870,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t25]) ).
cnf(t4278,plain,
composition(join(X1,composition(X2,top)),top) = join(composition(X1,top),composition(X2,top)),
inference(cp,[status(thm)],[t870,t4275]) ).
cnf(t26416,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(step,[status(thm)],[t4278,t23]) ).
cnf(t6191,plain,
composition(join(X1,composition(X2,top)),top) = composition(join(X1,X2),top),
inference(orient,[status(thm)],[t26416]) ).
cnf(t6203,plain,
composition(join(X1,one),top) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t6191,t182]) ).
cnf(t26417,plain,
composition(join(X1,one),top) = composition(top,top),
inference(step,[status(thm)],[t6203,t349]) ).
cnf(t26418,plain,
composition(join(X1,one),top) = top,
inference(step,[status(thm)],[t26417,t4275]) ).
cnf(t6226,plain,
composition(join(X1,one),top) = top,
inference(orient,[status(thm)],[t26418]) ).
cnf(t6228,plain,
top = composition(join(one,X1),top),
inference(cp,[status(thm)],[t6226,t42]) ).
cnf(t6249,plain,
composition(join(one,X1),top) = top,
inference(orient,[status(thm)],[t6228]) ).
cnf(t6264,plain,
composition(converse(top),join(one,X1)) = converse(top),
inference(cp,[status(thm)],[t3851,t6249]) ).
cnf(t26421,plain,
composition(top,join(one,X1)) = converse(top),
inference(step,[status(thm)],[t6264,t361]) ).
cnf(t26422,plain,
composition(top,join(one,X1)) = top,
inference(step,[status(thm)],[t26421,t361]) ).
cnf(t6283,plain,
composition(top,join(one,X1)) = top,
inference(orient,[status(thm)],[t26422]) ).
cnf(t6284,plain,
top = composition(top,join(X1,one)),
inference(cp,[status(thm)],[t6283,t42]) ).
cnf(t6298,plain,
composition(top,join(X1,one)) = top,
inference(orient,[status(thm)],[t6284]) ).
cnf(t6305,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t53,t6298]) ).
cnf(t26444,plain,
complement(join(X1,one)) = join(complement(join(X1,one)),composition(top,complement(top))),
inference(step,[status(thm)],[t6305,t361]) ).
cnf(t26445,plain,
complement(join(X1,one)) = join(composition(top,complement(top)),complement(join(X1,one))),
inference(step,[status(thm)],[t26444,t42]) ).
cnf(t26446,plain,
complement(join(X1,one)) = join(composition(top,zero),complement(join(X1,one))),
inference(step,[status(thm)],[t26445,t94]) ).
cnf(t26447,plain,
complement(join(X1,one)) = join(zero,complement(join(X1,one))),
inference(step,[status(thm)],[t26446,t4286]) ).
cnf(t7080,plain,
join(zero,complement(join(X1,one))) = complement(join(X1,one)),
inference(orient,[status(thm)],[t26447]) ).
cnf(t7089,plain,
zero = composition(join(X1,complement(join(X2,one))),zero),
inference(cp,[status(thm)],[t4675,t7080]) ).
cnf(t7349,plain,
composition(join(X1,complement(join(X2,one))),zero) = zero,
inference(orient,[status(thm)],[t7089]) ).
cnf(t15310,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t7349,t15096]) ).
cnf(t15315,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t15310]) ).
cnf(t15322,plain,
converse(zero) = join(converse(zero),zero),
inference(cp,[status(thm)],[t11080,t15315]) ).
cnf(t26664,plain,
converse(zero) = join(zero,converse(zero)),
inference(step,[status(thm)],[t15322,t42]) ).
cnf(t15476,plain,
join(zero,converse(zero)) = converse(zero),
inference(orient,[status(thm)],[t26664]) ).
cnf(t15486,plain,
join(converse(zero),zero) = converse(converse(zero)),
inference(cp,[status(thm)],[t274,t15476]) ).
cnf(t26665,plain,
join(zero,converse(zero)) = converse(converse(zero)),
inference(step,[status(thm)],[t15486,t42]) ).
cnf(t26666,plain,
converse(zero) = converse(converse(zero)),
inference(step,[status(thm)],[t26665,t15476]) ).
cnf(t26667,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t26666,t20]) ).
cnf(t15489,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t26667]) ).
cnf(t15492,plain,
converse(composition(X1,zero)) = composition(zero,converse(X1)),
inference(cp,[status(thm)],[t26,t15489]) ).
cnf(t26699,plain,
converse(zero) = composition(zero,converse(X1)),
inference(step,[status(thm)],[t15492,t15315]) ).
cnf(t26700,plain,
zero = composition(zero,converse(X1)),
inference(step,[status(thm)],[t26699,t15489]) ).
cnf(t15573,plain,
composition(zero,converse(X1)) = zero,
inference(orient,[status(thm)],[t26700]) ).
cnf(t15590,plain,
zero = composition(zero,X1),
inference(cp,[status(thm)],[t15573,t20]) ).
cnf(t15611,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t15590]) ).
cnf(t15622,plain,
complement(X1) = join(complement(X1),composition(converse(zero),complement(zero))),
inference(cp,[status(thm)],[t53,t15611]) ).
cnf(t26701,plain,
complement(X1) = join(complement(X1),composition(zero,complement(zero))),
inference(step,[status(thm)],[t15622,t15489]) ).
cnf(t26702,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t26701,t15611]) ).
cnf(t26703,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t26702,t42]) ).
cnf(t15624,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t26703]) ).
cnf(t26716,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t115,t15624]) ).
cnf(t15665,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t26716]) ).
cnf(t15666,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t15665]) ).
cnf(t15797,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t15791,t42]) ).
cnf(t15829,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t15797]) ).
cnf(t15839,plain,
X1 = join(meet(X1,zero),complement(complement(X1))),
inference(cp,[status(thm)],[t15096,t15829]) ).
cnf(t1925,plain,
join(complement(X1),join(join(X2,X1),X3)) = join(top,X3),
inference(cp,[status(thm)],[t45,t1888]) ).
cnf(t26190,plain,
join(complement(X1),join(X2,join(X1,X3))) = join(top,X3),
inference(step,[status(thm)],[t1925,t45]) ).
cnf(t26191,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(step,[status(thm)],[t26190,t355]) ).
cnf(t2143,plain,
join(complement(X1),join(X2,join(X1,X3))) = top,
inference(orient,[status(thm)],[t26191]) ).
cnf(t7090,plain,
top = join(complement(zero),join(X1,complement(join(X2,one)))),
inference(cp,[status(thm)],[t2143,t7080]) ).
cnf(t9242,plain,
join(complement(zero),join(X1,complement(join(X2,one)))) = top,
inference(orient,[status(thm)],[t7090]) ).
cnf(t15309,plain,
top = join(complement(zero),X1),
inference(cp,[status(thm)],[t9242,t15096]) ).
cnf(t15374,plain,
join(complement(zero),X1) = top,
inference(orient,[status(thm)],[t15309]) ).
cnf(t15375,plain,
top = complement(zero),
inference(cp,[status(thm)],[t15374,t53]) ).
cnf(t15417,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t15375]) ).
cnf(t15422,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t82,t15417]) ).
cnf(t26661,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t15422,t349]) ).
cnf(t26662,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t26661,t94]) ).
cnf(t15465,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t26662]) ).
cnf(t26757,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t15839,t15465]) ).
cnf(t26758,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t26757,t15624]) ).
cnf(t26759,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t26758,t15666]) ).
cnf(t15879,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t26759]) ).
cnf(t26760,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t15666,t15879]) ).
cnf(t15880,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t26760]) ).
cnf(t22572,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t22548,t15880]) ).
cnf(t23348,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t22572]) ).
cnf(t38,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)],[t32,t20]) ).
cnf(t26497,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)],[t38,t20]) ).
cnf(t9048,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)],[t26497]) ).
cnf(t2267,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t2257,t20]) ).
cnf(t2291,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t2267]) ).
cnf(t2310,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t2291,t228]) ).
cnf(t3088,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t2310]) ).
cnf(t26756,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(step,[status(thm)],[t3088,t15843]) ).
cnf(t15878,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(rw,[status(thm)],[t26756]) ).
cnf(t17383,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t15878]) ).
cnf(t17398,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)],[t9048,t17383]) ).
cnf(t26798,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)],[t17398,t17383]) ).
cnf(t26799,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)],[t26798,t15611]) ).
cnf(t26800,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)],[t26799,t103]) ).
cnf(t26801,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t26800,t182]) ).
cnf(t26802,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t26801,t103]) ).
cnf(t26803,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t26802,t15611]) ).
cnf(t26804,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t26803,t15829]) ).
cnf(t17429,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t26804]) ).
cnf(t23385,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t23348,t17429]) ).
cnf(t26890,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t23385,t42]) ).
cnf(t26891,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t26890,t15829]) ).
cnf(t24066,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t26891]) ).
cnf(t24071,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t24066,t15880]) ).
cnf(t26098,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t293,t361]) ).
cnf(t364,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t26098]) ).
cnf(t16286,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t16239,t364]) ).
cnf(t26860,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t16286,t94]) ).
cnf(t21659,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t26860]) ).
cnf(t22553,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t22548,t21659]) ).
cnf(t26872,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t22553,t15880]) ).
cnf(t26873,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t26872,t15829]) ).
cnf(t22741,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t26873]) ).
cnf(t22760,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t22741,t20]) ).
cnf(t23901,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t22760]) ).
cnf(t26892,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t24071,t23901]) ).
cnf(t24118,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t26892]) ).
cnf(t24123,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t24118,t15880]) ).
cnf(t24189,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t24123]) ).
cnf(t24203,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t24189,t257]) ).
cnf(t24914,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t24203]) ).
cnf(t117,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t115,t82]) ).
cnf(t3403,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t117]) ).
cnf(t26731,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t3403,t15791]) ).
cnf(t15792,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t26731]) ).
cnf(t26766,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t15792,t15879]) ).
cnf(t15907,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t26766]) ).
cnf(t16509,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t15907]) ).
cnf(t24216,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t16509,t24189]) ).
cnf(t25487,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t24216]) ).
cnf(t25535,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t24914,t25487]) ).
cnf(t26920,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t25535,t16239]) ).
cnf(t26921,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t26920,t24118]) ).
cnf(t26922,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t26921,t15880]) ).
cnf(t25547,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t26922]) ).
cnf(t25591,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(cp,[status(thm)],[t25547,t20]) ).
cnf(t25975,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(orient,[status(thm)],[t25591]) ).
cnf(goal_0,negated_conjecture,
meet(converse(sk1),converse(sk2)) != converse(meet(sk1,sk2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
converse(meet(sk1,sk2)) != converse(meet(sk1,sk2)),
inference(rw,[status(thm)],[goal_0,t25975]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL005-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.38 % Computer : n020.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Thu Sep 24 07:07:55 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 17.13/7.61 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.13/7.61 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------