%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL034-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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:56 PM UTC 2026
% Result : Unsatisfiable 47.36s 7.23s
% Output : CNFRefutation 47.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 21
% Syntax : Number of clauses : 292 ( 292 unt; 0 nHn; 91 RR)
% Number of literals : 292 ( 291 equ; 12 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 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 : 302 ( 72 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t47,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t117,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t113,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t49985,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t113]) ).
cnf(t130,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t49985]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t2,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t42,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t40,t24]) ).
cnf(t423,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t42]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t424,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t423,t23]) ).
cnf(t50005,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t424,t24]) ).
cnf(t441,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t50005]) ).
cnf(t442,plain,
one = converse(one),
inference(cp,[status(thm)],[t441,t23]) ).
cnf(t453,plain,
converse(one) = one,
inference(orient,[status(thm)],[t442]) ).
cnf(t50006,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t441,t453]) ).
cnf(t463,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t50006]) ).
cnf(t465,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t463]) ).
cnf(t468,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t130,t465]) ).
cnf(t50012,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t468,t453]) ).
cnf(t50013,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t50012,t465]) ).
cnf(t498,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t50013]) ).
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t64,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t499,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t498,t64]) ).
cnf(t50075,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t499,t64]) ).
cnf(t50076,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t50075,t64]) ).
cnf(t1079,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t50076]) ).
cnf(t116,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t64,t113]) ).
cnf(t49998,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t116,t64]) ).
cnf(t314,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t49998]) ).
cnf(t1082,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t1079,t314]) ).
cnf(t1300,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t1082]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t49981,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t25,t64]) ).
cnf(t67,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t49981]) ).
cnf(t6086,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t67]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t6087,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t6086,t68]) ).
cnf(t50326,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t6087,t64]) ).
cnf(t6195,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t50326]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t125,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t129,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t64,t125]) ).
cnf(t49989,plain,
zero = complement(top),
inference(step,[status(thm)],[t129,t68]) ).
cnf(t157,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t49989]) ).
cnf(t502,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t498,t157]) ).
cnf(t50014,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t502,t157]) ).
cnf(t50015,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t50014,t157]) ).
cnf(t509,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t50015]) ).
cnf(t510,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t117,t509]) ).
cnf(t528,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t510]) ).
cnf(t6199,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t528,t6195]) ).
cnf(t50328,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t6199,t6195]) ).
cnf(t6214,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t50328]) ).
cnf(t50329,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t6195,t6214]) ).
cnf(t6282,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t50329]) ).
cnf(t6370,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t6282]) ).
cnf(t6371,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t1300,t6370]) ).
cnf(t50404,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t6371,t6370]) ).
cnf(t50405,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t50404,t6370]) ).
cnf(t6560,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t50405]) ).
cnf(t6568,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t117,t6560]) ).
cnf(t6789,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t6568]) ).
cnf(t6814,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t6789,t6086]) ).
cnf(t50428,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t6814,t6086]) ).
cnf(t50429,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t50428,t113]) ).
cnf(t6832,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t50429]) ).
cnf(t17,axiom,
sFlat0 = meet(sk1,sk3),
introduced(definition) ).
cnf(t95,plain,
meet(sk1,sk3) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t320,plain,
meet(sk1,sk3) = sFlat0,
inference(rw,[status(thm)],[t95]) ).
cnf(t50001,plain,
meet(sk3,sk1) = sFlat0,
inference(step,[status(thm)],[t320,t314]) ).
cnf(t325,plain,
meet(sk3,sk1) = sFlat0,
inference(orient,[status(thm)],[t50001]) ).
cnf(t18,axiom,
sFlat1 = composition(sk2,meet(sk1,sk3)),
introduced(definition) ).
cnf(t59,plain,
composition(sk2,meet(sk1,sk3)) = sFlat1,
inference(orient,[status(thm)],[t18]) ).
cnf(t49982,plain,
composition(sk2,sFlat0) = sFlat1,
inference(step,[status(thm)],[t59,t95]) ).
cnf(t96,plain,
composition(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t49982]) ).
cnf(t163,plain,
composition(sk2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t96]) ).
cnf(t19,axiom,
sFlat2 = converse(sk1),
introduced(definition) ).
cnf(t102,plain,
converse(sk1) = sFlat2,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sFlat3 = meet(sk2,converse(sk1)),
introduced(definition) ).
cnf(t98,plain,
meet(sk2,converse(sk1)) = sFlat3,
inference(orient,[status(thm)],[t20]) ).
cnf(t49984,plain,
meet(sk2,sFlat2) = sFlat3,
inference(step,[status(thm)],[t98,t102]) ).
cnf(t112,plain,
meet(sk2,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t49984]) ).
cnf(t171,plain,
meet(sk2,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t112]) ).
cnf(t319,plain,
meet(sk2,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t171]) ).
cnf(t50000,plain,
meet(sFlat2,sk2) = sFlat3,
inference(step,[status(thm)],[t319,t314]) ).
cnf(t324,plain,
meet(sFlat2,sk2) = sFlat3,
inference(orient,[status(thm)],[t50000]) ).
cnf(t21,axiom,
sFlat4 = composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
introduced(definition) ).
cnf(t37,plain,
composition(meet(sk2,converse(sk1)),meet(sk1,sk3)) = sFlat4,
inference(orient,[status(thm)],[t21]) ).
cnf(t49983,plain,
composition(meet(sk2,converse(sk1)),sFlat0) = sFlat4,
inference(step,[status(thm)],[t37,t95]) ).
cnf(t97,plain,
composition(meet(sk2,converse(sk1)),sFlat0) = sFlat4,
inference(rw,[status(thm)],[t49983]) ).
cnf(t50002,plain,
composition(meet(sk2,sFlat2),sFlat0) = sFlat4,
inference(step,[status(thm)],[t97,t102]) ).
cnf(t50003,plain,
composition(meet(sFlat2,sk2),sFlat0) = sFlat4,
inference(step,[status(thm)],[t50002,t314]) ).
cnf(t50004,plain,
composition(sFlat3,sFlat0) = sFlat4,
inference(step,[status(thm)],[t50003,t324]) ).
cnf(t393,plain,
composition(sFlat3,sFlat0) = sFlat4,
inference(orient,[status(thm)],[t50004]) ).
cnf(t16,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(t30,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t16]) ).
cnf(t128,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t117,t125]) ).
cnf(t684,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t128]) ).
cnf(t694,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t684,t113]) ).
cnf(t508,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t64,t498]) ).
cnf(t515,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t508]) ).
cnf(t522,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t125,t515]) ).
cnf(t535,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t522]) ).
cnf(t689,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t684,t535]) ).
cnf(t691,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t684,t498]) ).
cnf(t50025,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t691,t125]) ).
cnf(t708,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t50025]) ).
cnf(t709,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t708,t64]) ).
cnf(t718,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t709]) ).
cnf(t50030,plain,
top = join(X1,top),
inference(step,[status(thm)],[t689,t718]) ).
cnf(t732,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t50030]) ).
cnf(t737,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t732,t113]) ).
cnf(t747,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t737]) ).
cnf(t50059,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t694,t747]) ).
cnf(t975,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t50059]) ).
cnf(t6191,plain,
top = join(join(complement(X1),X2),X1),
inference(cp,[status(thm)],[t975,t6086]) ).
cnf(t50520,plain,
top = join(complement(X1),join(X2,X1)),
inference(step,[status(thm)],[t6191,t117]) ).
cnf(t7633,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t50520]) ).
cnf(t6836,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t6832,t314]) ).
cnf(t6893,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t6836]) ).
cnf(t7639,plain,
top = join(complement(meet(X1,X2)),X2),
inference(cp,[status(thm)],[t7633,t6893]) ).
cnf(t50636,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t7639,t113]) ).
cnf(t9300,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t50636]) ).
cnf(t9327,plain,
meet(X1,meet(X2,complement(X1))) = complement(top),
inference(cp,[status(thm)],[t64,t9300]) ).
cnf(t50681,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t9327,t157]) ).
cnf(t9938,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t50681]) ).
cnf(t50388,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t515,t6370]) ).
cnf(t6392,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t50388]) ).
cnf(t6597,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t6392]) ).
cnf(t9939,plain,
zero = meet(complement(X1),meet(X2,X1)),
inference(cp,[status(thm)],[t9938,t6597]) ).
cnf(t10038,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t9939]) ).
cnf(t7784,plain,
X1 = join(meet(X1,join(X2,X1)),complement(top)),
inference(cp,[status(thm)],[t6086,t7633]) ).
cnf(t50523,plain,
X1 = join(complement(top),meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t7784,t113]) ).
cnf(t50524,plain,
X1 = join(zero,meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t50523,t157]) ).
cnf(t50525,plain,
X1 = meet(X1,join(X2,X1)),
inference(step,[status(thm)],[t50524,t6214]) ).
cnf(t7804,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t50525]) ).
cnf(t10044,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t10038,t7804]) ).
cnf(t50685,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t10044,t314]) ).
cnf(t10218,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t50685]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t99,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t104,plain,
converse(join(sk1,X1)) = join(sFlat2,converse(X1)),
inference(cp,[status(thm)],[t99,t102]) ).
cnf(t184,plain,
converse(join(sk1,X1)) = join(sFlat2,converse(X1)),
inference(orient,[status(thm)],[t104]) ).
cnf(t103,plain,
sk1 = converse(sFlat2),
inference(cp,[status(thm)],[t24,t102]) ).
cnf(t147,plain,
converse(sFlat2) = sk1,
inference(orient,[status(thm)],[t103]) ).
cnf(t148,plain,
converse(join(sFlat2,X1)) = join(sk1,converse(X1)),
inference(cp,[status(thm)],[t99,t147]) ).
cnf(t253,plain,
converse(join(sFlat2,X1)) = join(sk1,converse(X1)),
inference(orient,[status(thm)],[t148]) ).
cnf(t107,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat2),
inference(cp,[status(thm)],[t40,t102]) ).
cnf(t220,plain,
converse(composition(sk1,X1)) = composition(converse(X1),sFlat2),
inference(orient,[status(thm)],[t107]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t54,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t221,plain,
composition(converse(top),sFlat2) = converse(sk1),
inference(cp,[status(thm)],[t220,t54]) ).
cnf(t49994,plain,
composition(converse(top),sFlat2) = sFlat2,
inference(step,[status(thm)],[t221,t102]) ).
cnf(t233,plain,
composition(converse(top),sFlat2) = sFlat2,
inference(orient,[status(thm)],[t49994]) ).
cnf(t100,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t99,t24]) ).
cnf(t544,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t100]) ).
cnf(t548,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t544,t125]) ).
cnf(t598,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t548]) ).
cnf(t750,plain,
top = converse(top),
inference(cp,[status(thm)],[t747,t598]) ).
cnf(t758,plain,
converse(top) = top,
inference(orient,[status(thm)],[t750]) ).
cnf(t50047,plain,
composition(top,sFlat2) = sFlat2,
inference(step,[status(thm)],[t233,t758]) ).
cnf(t774,plain,
composition(top,sFlat2) = sFlat2,
inference(rw,[status(thm)],[t50047]) ).
cnf(t775,plain,
composition(top,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t774]) ).
cnf(t776,plain,
composition(join(top,X1),sFlat2) = join(sFlat2,composition(X1,sFlat2)),
inference(cp,[status(thm)],[t47,t775]) ).
cnf(t50048,plain,
composition(top,sFlat2) = join(sFlat2,composition(X1,sFlat2)),
inference(step,[status(thm)],[t776,t747]) ).
cnf(t50049,plain,
sFlat2 = join(sFlat2,composition(X1,sFlat2)),
inference(step,[status(thm)],[t50048,t775]) ).
cnf(t781,plain,
join(sFlat2,composition(X1,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t50049]) ).
cnf(t785,plain,
join(sk1,converse(composition(X1,sFlat2))) = converse(sFlat2),
inference(cp,[status(thm)],[t253,t781]) ).
cnf(t150,plain,
converse(composition(X1,sFlat2)) = composition(sk1,converse(X1)),
inference(cp,[status(thm)],[t40,t147]) ).
cnf(t278,plain,
converse(composition(X1,sFlat2)) = composition(sk1,converse(X1)),
inference(orient,[status(thm)],[t150]) ).
cnf(t50056,plain,
join(sk1,composition(sk1,converse(X1))) = converse(sFlat2),
inference(step,[status(thm)],[t785,t278]) ).
cnf(t50057,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(step,[status(thm)],[t50056,t147]) ).
cnf(t939,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(orient,[status(thm)],[t50057]) ).
cnf(t956,plain,
sk1 = join(sk1,composition(sk1,X1)),
inference(cp,[status(thm)],[t939,t24]) ).
cnf(t962,plain,
join(sk1,composition(sk1,X1)) = sk1,
inference(orient,[status(thm)],[t956]) ).
cnf(t963,plain,
join(sk1,join(composition(sk1,X1),X2)) = join(sk1,X2),
inference(cp,[status(thm)],[t117,t962]) ).
cnf(t1284,plain,
join(sk1,join(composition(sk1,X1),X2)) = join(sk1,X2),
inference(orient,[status(thm)],[t963]) ).
cnf(t1289,plain,
join(sk1,X1) = join(sk1,join(X1,composition(sk1,X2))),
inference(cp,[status(thm)],[t1284,t113]) ).
cnf(t1321,plain,
join(sk1,join(X1,composition(sk1,X2))) = join(sk1,X1),
inference(orient,[status(thm)],[t1289]) ).
cnf(t1323,plain,
join(sk1,composition(X1,X2)) = join(sk1,composition(join(X1,sk1),X2)),
inference(cp,[status(thm)],[t1321,t47]) ).
cnf(t4997,plain,
join(sk1,composition(join(X1,sk1),X2)) = join(sk1,composition(X1,X2)),
inference(orient,[status(thm)],[t1323]) ).
cnf(t6895,plain,
sk1 = join(sk1,sFlat0),
inference(cp,[status(thm)],[t6893,t325]) ).
cnf(t50432,plain,
sk1 = join(sFlat0,sk1),
inference(step,[status(thm)],[t6895,t113]) ).
cnf(t6936,plain,
join(sFlat0,sk1) = sk1,
inference(orient,[status(thm)],[t50432]) ).
cnf(t6942,plain,
join(sk1,composition(sFlat0,X1)) = join(sk1,composition(sk1,X1)),
inference(cp,[status(thm)],[t4997,t6936]) ).
cnf(t50492,plain,
join(sk1,composition(sFlat0,X1)) = sk1,
inference(step,[status(thm)],[t6942,t962]) ).
cnf(t7033,plain,
join(sk1,composition(sFlat0,X1)) = sk1,
inference(orient,[status(thm)],[t50492]) ).
cnf(t7036,plain,
join(sFlat2,converse(composition(sFlat0,X1))) = converse(sk1),
inference(cp,[status(thm)],[t184,t7033]) ).
cnf(t50623,plain,
join(sFlat2,converse(composition(sFlat0,X1))) = sFlat2,
inference(step,[status(thm)],[t7036,t102]) ).
cnf(t9007,plain,
join(sFlat2,converse(composition(sFlat0,X1))) = sFlat2,
inference(orient,[status(thm)],[t50623]) ).
cnf(t41,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t40,t24]) ).
cnf(t404,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t41]) ).
cnf(t9011,plain,
sFlat2 = join(sFlat2,composition(X1,converse(sFlat0))),
inference(cp,[status(thm)],[t9007,t404]) ).
cnf(t9701,plain,
join(sFlat2,composition(X1,converse(sFlat0))) = sFlat2,
inference(orient,[status(thm)],[t9011]) ).
cnf(t10301,plain,
zero = meet(composition(X1,converse(sFlat0)),complement(sFlat2)),
inference(cp,[status(thm)],[t10218,t9701]) ).
cnf(t50958,plain,
zero = meet(complement(sFlat2),composition(X1,converse(sFlat0))),
inference(step,[status(thm)],[t10301,t314]) ).
cnf(t15264,plain,
meet(complement(sFlat2),composition(X1,converse(sFlat0))) = zero,
inference(orient,[status(thm)],[t50958]) ).
cnf(t15270,plain,
composition(meet(complement(sFlat2),composition(X1,converse(sFlat0))),meet(sFlat0,composition(converse(complement(sFlat2)),X1))) = join(meet(composition(complement(sFlat2),sFlat0),X1),composition(zero,meet(sFlat0,composition(converse(complement(sFlat2)),X1)))),
inference(cp,[status(thm)],[t30,t15264]) ).
cnf(t50959,plain,
composition(zero,meet(sFlat0,composition(converse(complement(sFlat2)),X1))) = join(meet(composition(complement(sFlat2),sFlat0),X1),composition(zero,meet(sFlat0,composition(converse(complement(sFlat2)),X1)))),
inference(step,[status(thm)],[t15270,t15264]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t778,plain,
composition(top,composition(sFlat2,X1)) = composition(sFlat2,X1),
inference(cp,[status(thm)],[t28,t775]) ).
cnf(t917,plain,
composition(top,composition(sFlat2,X1)) = composition(sFlat2,X1),
inference(orient,[status(thm)],[t778]) ).
cnf(t135,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t130,t54]) ).
cnf(t50068,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t135,t157]) ).
cnf(t50069,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t50068,t157]) ).
cnf(t50070,plain,
zero = join(zero,composition(sFlat2,complement(sk1))),
inference(step,[status(thm)],[t50069,t102]) ).
cnf(t1070,plain,
join(zero,composition(sFlat2,complement(sk1))) = zero,
inference(orient,[status(thm)],[t50070]) ).
cnf(t50368,plain,
composition(sFlat2,complement(sk1)) = zero,
inference(step,[status(thm)],[t1070,t6214]) ).
cnf(t6317,plain,
composition(sFlat2,complement(sk1)) = zero,
inference(rw,[status(thm)],[t50368]) ).
cnf(t6714,plain,
composition(sFlat2,complement(sk1)) = zero,
inference(orient,[status(thm)],[t6317]) ).
cnf(t6716,plain,
composition(sFlat2,complement(sk1)) = composition(top,zero),
inference(cp,[status(thm)],[t917,t6714]) ).
cnf(t50414,plain,
zero = composition(top,zero),
inference(step,[status(thm)],[t6716,t6714]) ).
cnf(t6730,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t50414]) ).
cnf(t6732,plain,
composition(join(top,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t47,t6730]) ).
cnf(t50417,plain,
composition(top,zero) = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t6732,t747]) ).
cnf(t50418,plain,
zero = join(zero,composition(X1,zero)),
inference(step,[status(thm)],[t50417,t6730]) ).
cnf(t50419,plain,
zero = composition(X1,zero),
inference(step,[status(thm)],[t50418,t6214]) ).
cnf(t6751,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t50419]) ).
cnf(t6755,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t423,t6751]) ).
cnf(t50045,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t598,t758]) ).
cnf(t765,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t50045]) ).
cnf(t6223,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t6214,t765]) ).
cnf(t6645,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t6223]) ).
cnf(t6646,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t24,t6645]) ).
cnf(t50412,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t6646,t758]) ).
cnf(t6681,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t50412]) ).
cnf(t6682,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t6597,t6681]) ).
cnf(t50413,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t6682,t157]) ).
cnf(t6689,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t50413]) ).
cnf(t50424,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t6755,t6689]) ).
cnf(t50425,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t50424,t6689]) ).
cnf(t6770,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t50425]) ).
cnf(t50960,plain,
zero = join(meet(composition(complement(sFlat2),sFlat0),X1),composition(zero,meet(sFlat0,composition(converse(complement(sFlat2)),X1)))),
inference(step,[status(thm)],[t50959,t6770]) ).
cnf(t50961,plain,
zero = join(meet(composition(complement(sFlat2),sFlat0),X1),zero),
inference(step,[status(thm)],[t50960,t6770]) ).
cnf(t6226,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t6214,t113]) ).
cnf(t6337,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t6226]) ).
cnf(t50962,plain,
zero = meet(composition(complement(sFlat2),sFlat0),X1),
inference(step,[status(thm)],[t50961,t6337]) ).
cnf(t15276,plain,
meet(composition(complement(sFlat2),sFlat0),X1) = zero,
inference(orient,[status(thm)],[t50962]) ).
cnf(t15277,plain,
zero = composition(complement(sFlat2),sFlat0),
inference(cp,[status(thm)],[t15276,t6370]) ).
cnf(t15300,plain,
composition(complement(sFlat2),sFlat0) = zero,
inference(orient,[status(thm)],[t15277]) ).
cnf(t15301,plain,
composition(join(complement(sFlat2),X1),sFlat0) = join(zero,composition(X1,sFlat0)),
inference(cp,[status(thm)],[t47,t15300]) ).
cnf(t50964,plain,
composition(join(complement(sFlat2),X1),sFlat0) = composition(X1,sFlat0),
inference(step,[status(thm)],[t15301,t6214]) ).
cnf(t15341,plain,
composition(join(complement(sFlat2),X1),sFlat0) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t50964]) ).
cnf(t6912,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t117,t6893]) ).
cnf(t26377,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t6912]) ).
cnf(t525,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t64,t515]) ).
cnf(t3252,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t525]) ).
cnf(t50391,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t3252,t6370]) ).
cnf(t6395,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t50391]) ).
cnf(t10612,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t6395]) ).
cnf(t50740,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t6086,t10612]) ).
cnf(t10669,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t50740]) ).
cnf(t46773,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t10669]) ).
cnf(t46999,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t26377,t46773]) ).
cnf(t49690,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t46999]) ).
cnf(t49808,plain,
composition(meet(X1,complement(complement(sFlat2))),sFlat0) = composition(join(complement(sFlat2),X1),sFlat0),
inference(cp,[status(thm)],[t15341,t49690]) ).
cnf(t51828,plain,
composition(meet(X1,sFlat2),sFlat0) = composition(join(complement(sFlat2),X1),sFlat0),
inference(step,[status(thm)],[t49808,t6597]) ).
cnf(t51829,plain,
composition(meet(X1,sFlat2),sFlat0) = composition(X1,sFlat0),
inference(step,[status(thm)],[t51828,t15341]) ).
cnf(t49845,plain,
composition(meet(X1,sFlat2),sFlat0) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t51829]) ).
cnf(t49846,plain,
composition(X1,sFlat0) = composition(meet(sFlat2,X1),sFlat0),
inference(cp,[status(thm)],[t49845,t314]) ).
cnf(t49919,plain,
composition(meet(sFlat2,X1),sFlat0) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t49846]) ).
cnf(t49921,plain,
composition(sk2,sFlat0) = composition(sFlat3,sFlat0),
inference(cp,[status(thm)],[t49919,t324]) ).
cnf(t51832,plain,
sFlat1 = composition(sFlat3,sFlat0),
inference(step,[status(thm)],[t49921,t163]) ).
cnf(t51833,plain,
sFlat1 = sFlat4,
inference(step,[status(thm)],[t51832,t393]) ).
cnf(t49957,plain,
sFlat4 = sFlat1,
inference(orient,[status(thm)],[t51833]) ).
cnf(t51834,plain,
composition(sFlat3,sFlat0) = sFlat1,
inference(step,[status(thm)],[t393,t49957]) ).
cnf(t49958,plain,
composition(sFlat3,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t51834]) ).
cnf(goal_0,negated_conjecture,
join(composition(sk2,meet(sk1,sk3)),composition(meet(sk2,converse(sk1)),meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
composition(join(sk2,meet(sk2,converse(sk1))),meet(sk1,sk3)) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[goal_0,t47]) ).
cnf(g0_1,plain,
composition(sk2,meet(sk1,sk3)) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_0,t6832]) ).
cnf(g0_2,plain,
composition(sk2,meet(sk3,sk1)) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_1,t314]) ).
cnf(g0_3,plain,
composition(sk2,sFlat0) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_2,t325]) ).
cnf(g0_4,plain,
sFlat1 != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_3,t163]) ).
cnf(g0_5,plain,
sFlat1 != composition(meet(sk2,sFlat2),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_4,t102]) ).
cnf(g0_6,plain,
sFlat1 != composition(meet(sFlat2,sk2),meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_5,t314]) ).
cnf(g0_7,plain,
sFlat1 != composition(sFlat3,meet(sk1,sk3)),
inference(rw,[status(thm)],[g0_6,t324]) ).
cnf(g0_8,plain,
sFlat1 != composition(sFlat3,meet(sk3,sk1)),
inference(rw,[status(thm)],[g0_7,t314]) ).
cnf(g0_9,plain,
sFlat1 != composition(sFlat3,sFlat0),
inference(rw,[status(thm)],[g0_8,t325]) ).
cnf(g0_10,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_9,t49958]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL034-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.36 % Computer : n011.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Thu Sep 24 07:29:59 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 47.36/7.23 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 47.36/7.23 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------