%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL012-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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:43 PM UTC 2026
% Result : Unsatisfiable 22.05s 3.60s
% Output : CNFRefutation 22.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 21
% Syntax : Number of clauses : 259 ( 259 unt; 0 nHn; 79 RR)
% Number of literals : 259 ( 258 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 11 con; 0-2 aty)
% Number of variables : 276 ( 51 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t71,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t20,axiom,
sFlat4 = complement(sk1),
introduced(definition) ).
cnf(t129,plain,
complement(sk1) = sFlat4,
inference(orient,[status(thm)],[t20]) ).
cnf(t16,axiom,
sFlat0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t54,plain,
composition(sk1,sk2) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sFlat1 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t25560,plain,
sFlat1 = complement(sFlat0),
inference(step,[status(thm)],[t17,t54]) ).
cnf(t116,plain,
complement(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t25560]) ).
cnf(t18,axiom,
sFlat2 = converse(sk2),
introduced(definition) ).
cnf(t63,plain,
converse(sk2) = sFlat2,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sFlat3 = composition(complement(composition(sk1,sk2)),converse(sk2)),
introduced(definition) ).
cnf(t38,plain,
composition(complement(composition(sk1,sk2)),converse(sk2)) = sFlat3,
inference(orient,[status(thm)],[t19]) ).
cnf(t25555,plain,
composition(complement(sFlat0),converse(sk2)) = sFlat3,
inference(step,[status(thm)],[t38,t54]) ).
cnf(t59,plain,
composition(complement(sFlat0),converse(sk2)) = sFlat3,
inference(rw,[status(thm)],[t25555]) ).
cnf(t25565,plain,
composition(sFlat1,converse(sk2)) = sFlat3,
inference(step,[status(thm)],[t59,t116]) ).
cnf(t25566,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t25565,t63]) ).
cnf(t166,plain,
composition(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t25566]) ).
cnf(t21,axiom,
sFlat5 = join(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1)),
introduced(definition) ).
cnf(t25557,plain,
sFlat5 = join(complement(sk1),composition(complement(composition(sk1,sk2)),converse(sk2))),
inference(step,[status(thm)],[t21,t71]) ).
cnf(t25558,plain,
sFlat5 = join(complement(sk1),composition(complement(sFlat0),converse(sk2))),
inference(step,[status(thm)],[t25557,t54]) ).
cnf(t25559,plain,
sFlat5 = join(complement(sk1),composition(complement(sFlat0),sFlat2)),
inference(step,[status(thm)],[t25558,t63]) ).
cnf(t92,plain,
join(complement(sk1),composition(complement(sFlat0),sFlat2)) = sFlat5,
inference(orient,[status(thm)],[t25559]) ).
cnf(t25561,plain,
join(complement(sk1),composition(sFlat1,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t92,t116]) ).
cnf(t119,plain,
join(complement(sk1),composition(sFlat1,sFlat2)) = sFlat5,
inference(rw,[status(thm)],[t25561]) ).
cnf(t25578,plain,
join(sFlat4,composition(sFlat1,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t119,t129]) ).
cnf(t25579,plain,
join(sFlat4,sFlat3) = sFlat5,
inference(step,[status(thm)],[t25578,t166]) ).
cnf(t25580,plain,
join(sFlat3,sFlat4) = sFlat5,
inference(step,[status(thm)],[t25579,t71]) ).
cnf(t496,plain,
join(sFlat3,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t25580]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t120,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25556,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t11,t71]) ).
cnf(t84,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t25556]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,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(t23,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t31,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t29,t23]) ).
cnf(t516,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t31]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t517,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t516,t22]) ).
cnf(t25582,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t517,t23]) ).
cnf(t533,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t25582]) ).
cnf(t534,plain,
one = converse(one),
inference(cp,[status(thm)],[t533,t22]) ).
cnf(t543,plain,
converse(one) = one,
inference(orient,[status(thm)],[t534]) ).
cnf(t25583,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t533,t543]) ).
cnf(t553,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t25583]) ).
cnf(t554,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t553]) ).
cnf(t557,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t84,t554]) ).
cnf(t25585,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t557,t543]) ).
cnf(t25586,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t25585,t554]) ).
cnf(t587,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t25586]) ).
cnf(t615,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t120,t587]) ).
cnf(t647,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t615]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t74,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t24]) ).
cnf(t26400,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t74,t71]) ).
cnf(t26401,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t26400,t120]) ).
cnf(t26402,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t26401,t71]) ).
cnf(t15252,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t26402]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t134,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t15253,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t15252,t134]) ).
cnf(t26458,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t15253,t120]) ).
cnf(t15735,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t26458]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t75,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t81,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t121,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t120,t81]) ).
cnf(t25563,plain,
zero = complement(top),
inference(step,[status(thm)],[t121,t134]) ).
cnf(t157,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t25563]) ).
cnf(t595,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t587,t157]) ).
cnf(t25587,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t595,t157]) ).
cnf(t25588,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t25587,t157]) ).
cnf(t616,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t25588]) ).
cnf(t617,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t75,t616]) ).
cnf(t662,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t617]) ).
cnf(t15740,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t662,t15735]) ).
cnf(t26460,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t15740,t15735]) ).
cnf(t15760,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t26460]) ).
cnf(t26469,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t15735,t15760]) ).
cnf(t15847,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t26469]) ).
cnf(t16052,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t15847]) ).
cnf(t26524,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t647,t16052]) ).
cnf(t16097,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t26524]) ).
cnf(t16221,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t16097]) ).
cnf(t131,plain,
meet(sk1,X1) = complement(join(sFlat4,complement(X1))),
inference(cp,[status(thm)],[t120,t129]) ).
cnf(t402,plain,
complement(join(sFlat4,complement(X1))) = meet(sk1,X1),
inference(orient,[status(thm)],[t131]) ).
cnf(t659,plain,
meet(sk1,complement(X1)) = complement(join(sFlat4,meet(X1,X1))),
inference(cp,[status(thm)],[t402,t647]) ).
cnf(t1628,plain,
complement(join(sFlat4,meet(X1,X1))) = meet(sk1,complement(X1)),
inference(orient,[status(thm)],[t659]) ).
cnf(t26533,plain,
complement(join(sFlat4,X1)) = meet(sk1,complement(X1)),
inference(step,[status(thm)],[t1628,t16052]) ).
cnf(t16106,plain,
complement(join(sFlat4,X1)) = meet(sk1,complement(X1)),
inference(rw,[status(thm)],[t26533]) ).
cnf(t16824,plain,
complement(join(sFlat4,X1)) = meet(sk1,complement(X1)),
inference(orient,[status(thm)],[t16106]) ).
cnf(t16868,plain,
meet(sk1,complement(X1)) = complement(join(X1,sFlat4)),
inference(cp,[status(thm)],[t16824,t71]) ).
cnf(t18064,plain,
complement(join(X1,sFlat4)) = meet(sk1,complement(X1)),
inference(orient,[status(thm)],[t16868]) ).
cnf(t18066,plain,
meet(sk1,complement(sFlat3)) = complement(sFlat5),
inference(cp,[status(thm)],[t18064,t496]) ).
cnf(t18118,plain,
meet(sk1,complement(sFlat3)) = complement(sFlat5),
inference(orient,[status(thm)],[t18066]) ).
cnf(t18128,plain,
sk1 = join(complement(sFlat5),complement(join(complement(sk1),complement(sFlat3)))),
inference(cp,[status(thm)],[t15252,t18118]) ).
cnf(t26646,plain,
sk1 = join(complement(sFlat5),meet(sk1,sFlat3)),
inference(step,[status(thm)],[t18128,t120]) ).
cnf(t122,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t120,t71]) ).
cnf(t25571,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t122,t120]) ).
cnf(t315,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t25571]) ).
cnf(t26647,plain,
sk1 = join(complement(sFlat5),meet(sFlat3,sk1)),
inference(step,[status(thm)],[t26646,t315]) ).
cnf(t20169,plain,
join(complement(sFlat5),meet(sFlat3,sk1)) = sk1,
inference(orient,[status(thm)],[t26647]) ).
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(t42,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(t50,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)],[t42,t23]) ).
cnf(t26070,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)],[t50,t23]) ).
cnf(t10198,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)],[t26070]) ).
cnf(t657,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t120,t647]) ).
cnf(t5515,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t657]) ).
cnf(t26528,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t5515,t16052]) ).
cnf(t16101,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t26528]) ).
cnf(t20968,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t16101]) ).
cnf(t83,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t75,t81]) ).
cnf(t1234,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t83]) ).
cnf(t1257,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t1234,t71]) ).
cnf(t655,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t81,t647]) ).
cnf(t824,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t655]) ).
cnf(t1252,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t1234,t824]) ).
cnf(t1254,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t1234,t587]) ).
cnf(t25670,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t1254,t81]) ).
cnf(t1282,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t25670]) ).
cnf(t1290,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t1282,t120]) ).
cnf(t1321,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t1290]) ).
cnf(t25679,plain,
top = join(X1,top),
inference(step,[status(thm)],[t1252,t1321]) ).
cnf(t1328,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t25679]) ).
cnf(t1329,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t1328,t71]) ).
cnf(t1342,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t1329]) ).
cnf(t25718,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t1257,t1342]) ).
cnf(t1443,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t25718]) ).
cnf(t21008,plain,
meet(X1,complement(join(X2,complement(complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t20968,t1443]) ).
cnf(t26717,plain,
meet(X1,complement(join(X2,X1))) = complement(top),
inference(step,[status(thm)],[t21008,t16221]) ).
cnf(t26718,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(step,[status(thm)],[t26717,t157]) ).
cnf(t21103,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t26718]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t55,plain,
composition(join(sk1,X1),sk2) = join(sFlat0,composition(X1,sk2)),
inference(cp,[status(thm)],[t33,t54]) ).
cnf(t960,plain,
composition(join(sk1,X1),sk2) = join(sFlat0,composition(X1,sk2)),
inference(orient,[status(thm)],[t55]) ).
cnf(t598,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t587,t120]) ).
cnf(t25746,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t598,t120]) ).
cnf(t25747,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t25746,t120]) ).
cnf(t1835,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t25747]) ).
cnf(t1836,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t1835,t315]) ).
cnf(t1902,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t1836]) ).
cnf(t16053,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t1902,t16052]) ).
cnf(t26552,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t16053,t16052]) ).
cnf(t26553,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t26552,t16052]) ).
cnf(t16158,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t26553]) ).
cnf(t16176,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t75,t16158]) ).
cnf(t18739,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t16176]) ).
cnf(t18795,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t18739,t15252]) ).
cnf(t26626,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t18795,t15252]) ).
cnf(t26627,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t26626,t71]) ).
cnf(t18840,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t26627]) ).
cnf(t18850,plain,
join(sFlat0,composition(meet(sk1,X1),sk2)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t960,t18840]) ).
cnf(t26851,plain,
join(sFlat0,composition(meet(sk1,X1),sk2)) = sFlat0,
inference(step,[status(thm)],[t18850,t54]) ).
cnf(t23456,plain,
join(sFlat0,composition(meet(sk1,X1),sk2)) = sFlat0,
inference(orient,[status(thm)],[t26851]) ).
cnf(t23460,plain,
zero = meet(composition(meet(sk1,X1),sk2),complement(sFlat0)),
inference(cp,[status(thm)],[t21103,t23456]) ).
cnf(t26996,plain,
zero = meet(complement(sFlat0),composition(meet(sk1,X1),sk2)),
inference(step,[status(thm)],[t23460,t315]) ).
cnf(t26997,plain,
zero = meet(sFlat1,composition(meet(sk1,X1),sk2)),
inference(step,[status(thm)],[t26996,t116]) ).
cnf(t25430,plain,
meet(sFlat1,composition(meet(sk1,X1),sk2)) = zero,
inference(orient,[status(thm)],[t26997]) ).
cnf(t25445,plain,
composition(meet(sFlat1,composition(meet(sk1,X1),sk2)),meet(converse(sk2),composition(converse(sFlat1),meet(sk1,X1)))) = join(meet(composition(sFlat1,converse(sk2)),meet(sk1,X1)),composition(zero,meet(converse(sk2),composition(converse(sFlat1),meet(sk1,X1))))),
inference(cp,[status(thm)],[t10198,t25430]) ).
cnf(t26998,plain,
composition(zero,meet(converse(sk2),composition(converse(sFlat1),meet(sk1,X1)))) = join(meet(composition(sFlat1,converse(sk2)),meet(sk1,X1)),composition(zero,meet(converse(sk2),composition(converse(sFlat1),meet(sk1,X1))))),
inference(step,[status(thm)],[t25445,t25430]) ).
cnf(t162,plain,
complement(top) = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(cp,[status(thm)],[t84,t157]) ).
cnf(t25960,plain,
zero = join(zero,composition(converse(X1),complement(composition(X1,top)))),
inference(step,[status(thm)],[t162,t157]) ).
cnf(t9002,plain,
join(zero,composition(converse(X1),complement(composition(X1,top)))) = zero,
inference(orient,[status(thm)],[t25960]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t60,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t61,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t60,t23]) ).
cnf(t834,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t61]) ).
cnf(t838,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t834,t81]) ).
cnf(t892,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t838]) ).
cnf(t1357,plain,
top = converse(top),
inference(cp,[status(thm)],[t1342,t892]) ).
cnf(t1366,plain,
converse(top) = top,
inference(orient,[status(thm)],[t1357]) ).
cnf(t9016,plain,
zero = join(zero,composition(top,complement(composition(top,top)))),
inference(cp,[status(thm)],[t9002,t1366]) ).
cnf(t9042,plain,
join(zero,composition(top,complement(composition(top,top)))) = zero,
inference(orient,[status(thm)],[t9016]) ).
cnf(t26507,plain,
composition(top,complement(composition(top,top))) = zero,
inference(step,[status(thm)],[t9042,t15760]) ).
cnf(t15880,plain,
composition(top,complement(composition(top,top))) = zero,
inference(rw,[status(thm)],[t26507]) ).
cnf(t20073,plain,
composition(top,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t15880]) ).
cnf(t20075,plain,
composition(join(top,X1),complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(cp,[status(thm)],[t33,t20073]) ).
cnf(t26673,plain,
composition(top,complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t20075,t1342]) ).
cnf(t26674,plain,
zero = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t26673,t20073]) ).
cnf(t26675,plain,
zero = composition(X1,complement(composition(top,top))),
inference(step,[status(thm)],[t26674,t15760]) ).
cnf(t20589,plain,
composition(X1,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t26675]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t20591,plain,
zero = composition(X1,composition(X2,complement(composition(top,top)))),
inference(cp,[status(thm)],[t20589,t27]) ).
cnf(t26676,plain,
zero = composition(X1,zero),
inference(step,[status(thm)],[t20591,t20589]) ).
cnf(t20631,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t26676]) ).
cnf(t20638,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t516,t20631]) ).
cnf(t25715,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t892,t1366]) ).
cnf(t1373,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t25715]) ).
cnf(t15777,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t15760,t1373]) ).
cnf(t16330,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t15777]) ).
cnf(t16331,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t23,t16330]) ).
cnf(t26562,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t16331,t1366]) ).
cnf(t16379,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t26562]) ).
cnf(t16380,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t16221,t16379]) ).
cnf(t26563,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t16380,t157]) ).
cnf(t16399,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t26563]) ).
cnf(t26687,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t20638,t16399]) ).
cnf(t26688,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t26687,t16399]) ).
cnf(t20658,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t26688]) ).
cnf(t26999,plain,
zero = join(meet(composition(sFlat1,converse(sk2)),meet(sk1,X1)),composition(zero,meet(converse(sk2),composition(converse(sFlat1),meet(sk1,X1))))),
inference(step,[status(thm)],[t26998,t20658]) ).
cnf(t27000,plain,
zero = join(meet(composition(sFlat1,sFlat2),meet(sk1,X1)),composition(zero,meet(converse(sk2),composition(converse(sFlat1),meet(sk1,X1))))),
inference(step,[status(thm)],[t26999,t63]) ).
cnf(t27001,plain,
zero = join(meet(sFlat3,meet(sk1,X1)),composition(zero,meet(converse(sk2),composition(converse(sFlat1),meet(sk1,X1))))),
inference(step,[status(thm)],[t27000,t166]) ).
cnf(t27002,plain,
zero = join(meet(sFlat3,meet(sk1,X1)),zero),
inference(step,[status(thm)],[t27001,t20658]) ).
cnf(t15780,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t15760,t71]) ).
cnf(t16019,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t15780]) ).
cnf(t27003,plain,
zero = meet(sFlat3,meet(sk1,X1)),
inference(step,[status(thm)],[t27002,t16019]) ).
cnf(t25446,plain,
meet(sFlat3,meet(sk1,X1)) = zero,
inference(orient,[status(thm)],[t27003]) ).
cnf(t21000,plain,
meet(X1,complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t20968,t18840]) ).
cnf(t656,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t120,t647]) ).
cnf(t5424,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t656]) ).
cnf(t26529,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t5424,t16052]) ).
cnf(t16102,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t26529]) ).
cnf(t21644,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t16102]) ).
cnf(t21683,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t16221,t21644]) ).
cnf(t21877,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t21683]) ).
cnf(t26865,plain,
meet(X1,join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t21000,t21877]) ).
cnf(t26866,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t26865,t16221]) ).
cnf(t24076,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t26866]) ).
cnf(t24099,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t24076,t16221]) ).
cnf(t24129,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t24099]) ).
cnf(t24175,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t24129,t71]) ).
cnf(t24240,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t24175]) ).
cnf(t18844,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t18840,t315]) ).
cnf(t18903,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t18844]) ).
cnf(t24245,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t24240,t18903]) ).
cnf(t26868,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t24245,t315]) ).
cnf(t24416,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t26868]) ).
cnf(t25447,plain,
zero = meet(sk1,sFlat3),
inference(cp,[status(thm)],[t25446,t24416]) ).
cnf(t27004,plain,
zero = meet(sFlat3,sk1),
inference(step,[status(thm)],[t25447,t315]) ).
cnf(t25460,plain,
meet(sFlat3,sk1) = zero,
inference(orient,[status(thm)],[t27004]) ).
cnf(t27005,plain,
join(complement(sFlat5),zero) = sk1,
inference(step,[status(thm)],[t20169,t25460]) ).
cnf(t27006,plain,
complement(sFlat5) = sk1,
inference(step,[status(thm)],[t27005,t16019]) ).
cnf(t25467,plain,
complement(sFlat5) = sk1,
inference(rw,[status(thm)],[t27006]) ).
cnf(t25468,plain,
complement(sFlat5) = sk1,
inference(orient,[status(thm)],[t25467]) ).
cnf(t25477,plain,
sFlat5 = complement(sk1),
inference(cp,[status(thm)],[t16221,t25468]) ).
cnf(t27018,plain,
sFlat5 = sFlat4,
inference(step,[status(thm)],[t25477,t129]) ).
cnf(t25507,plain,
sFlat5 = sFlat4,
inference(orient,[status(thm)],[t27018]) ).
cnf(t27019,plain,
join(sFlat3,sFlat4) = sFlat4,
inference(step,[status(thm)],[t496,t25507]) ).
cnf(t25508,plain,
join(sFlat3,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t27019]) ).
cnf(goal_0,negated_conjecture,
join(composition(complement(composition(sk1,sk2)),converse(sk2)),complement(sk1)) != complement(sk1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(complement(sk1),composition(complement(composition(sk1,sk2)),converse(sk2))) != complement(sk1),
inference(rw,[status(thm)],[goal_0,t71]) ).
cnf(g0_1,plain,
join(sFlat4,composition(complement(composition(sk1,sk2)),converse(sk2))) != complement(sk1),
inference(rw,[status(thm)],[g0_0,t129]) ).
cnf(g0_2,plain,
join(sFlat4,composition(complement(sFlat0),converse(sk2))) != complement(sk1),
inference(rw,[status(thm)],[g0_1,t54]) ).
cnf(g0_3,plain,
join(sFlat4,composition(sFlat1,converse(sk2))) != complement(sk1),
inference(rw,[status(thm)],[g0_2,t116]) ).
cnf(g0_4,plain,
join(sFlat4,composition(sFlat1,sFlat2)) != complement(sk1),
inference(rw,[status(thm)],[g0_3,t63]) ).
cnf(g0_5,plain,
join(sFlat4,sFlat3) != complement(sk1),
inference(rw,[status(thm)],[g0_4,t166]) ).
cnf(g0_6,plain,
join(sFlat3,sFlat4) != complement(sk1),
inference(rw,[status(thm)],[g0_5,t71]) ).
cnf(g0_7,plain,
sFlat4 != complement(sk1),
inference(rw,[status(thm)],[g0_6,t25508]) ).
cnf(g0_8,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_7,t129]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL012-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.37 % Computer : n014.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Thu Sep 24 07:11:49 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.05/3.60 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.05/3.60 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------