%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL016-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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:44 PM UTC 2026
% Result : Unsatisfiable 61.92s 8.22s
% Output : CNFRefutation 61.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 120
% Number of leaves : 21
% Syntax : Number of clauses : 412 ( 412 unt; 0 nHn; 189 RR)
% Number of literals : 412 ( 411 equ; 46 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 : 20 ( 20 usr; 14 con; 0-2 aty)
% Number of variables : 344 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t89,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t19,axiom,
sFlat6 = composition(sk1,sk2),
introduced(definition) ).
cnf(t36,plain,
composition(sk1,sk2) = sFlat6,
inference(orient,[status(thm)],[t19]) ).
cnf(t16,axiom,
sFlat3 = composition(sk1,sk3),
introduced(definition) ).
cnf(t32,plain,
composition(sk1,sk3) = sFlat3,
inference(orient,[status(thm)],[t16]) ).
cnf(t17,axiom,
sFlat4 = complement(composition(sk1,sk3)),
introduced(definition) ).
cnf(t19247,plain,
sFlat4 = complement(sFlat3),
inference(step,[status(thm)],[t17,t32]) ).
cnf(t61,plain,
complement(sFlat3) = sFlat4,
inference(orient,[status(thm)],[t19247]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t72,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t90,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t72,t89]) ).
cnf(t19305,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t90,t72]) ).
cnf(t123,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t19305]) ).
cnf(t20,axiom,
sFlat7 = meet(composition(sk1,sk2),complement(composition(sk1,sk3))),
introduced(definition) ).
cnf(t19253,plain,
sFlat7 = meet(sFlat6,complement(composition(sk1,sk3))),
inference(step,[status(thm)],[t20,t36]) ).
cnf(t19254,plain,
sFlat7 = meet(sFlat6,complement(sFlat3)),
inference(step,[status(thm)],[t19253,t32]) ).
cnf(t19255,plain,
sFlat7 = meet(sFlat6,sFlat4),
inference(step,[status(thm)],[t19254,t61]) ).
cnf(t86,plain,
meet(sFlat6,sFlat4) = sFlat7,
inference(orient,[status(thm)],[t19255]) ).
cnf(t126,plain,
meet(sFlat6,sFlat4) = sFlat7,
inference(rw,[status(thm)],[t86]) ).
cnf(t19310,plain,
meet(sFlat4,sFlat6) = sFlat7,
inference(step,[status(thm)],[t126,t123]) ).
cnf(t134,plain,
meet(sFlat4,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t19310]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t13,axiom,
sFlat0 = complement(sk3),
introduced(definition) ).
cnf(t66,plain,
complement(sk3) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t68,plain,
X1 = join(complement(join(complement(X1),sFlat0)),complement(join(complement(X1),sk3))),
inference(cp,[status(thm)],[t26,t66]) ).
cnf(t77,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(meet(X1,X2),complement(X3))),
inference(cp,[status(thm)],[t72,t72]) ).
cnf(t1065,plain,
complement(join(meet(X1,X2),complement(X3))) = meet(join(complement(X1),complement(X2)),X3),
inference(orient,[status(thm)],[t77]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t92,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t96,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t72,t92]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t81,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t19303,plain,
zero = complement(top),
inference(step,[status(thm)],[t96,t81]) ).
cnf(t112,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t19303]) ).
cnf(t1083,plain,
meet(join(complement(X1),complement(X2)),top) = complement(join(meet(X1,X2),zero)),
inference(cp,[status(thm)],[t1065,t112]) ).
cnf(t19512,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(meet(X1,X2),zero)),
inference(step,[status(thm)],[t1083,t123]) ).
cnf(t19513,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t19512,t89]) ).
cnf(t3048,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t19513]) ).
cnf(t3105,plain,
complement(join(zero,meet(X1,top))) = meet(top,join(complement(X1),zero)),
inference(cp,[status(thm)],[t3048,t112]) ).
cnf(t19249,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t26,t72]) ).
cnf(t80,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t19249]) ).
cnf(t1940,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t80]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t97,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t100,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t97,t92]) ).
cnf(t385,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t100]) ).
cnf(t389,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t385,t89]) ).
cnf(t490,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t389]) ).
cnf(t2018,plain,
join(top,meet(X1,X2)) = join(join(complement(X1),X2),X1),
inference(cp,[status(thm)],[t490,t1940]) ).
cnf(t19441,plain,
join(top,meet(X1,X2)) = join(complement(X1),join(X2,X1)),
inference(step,[status(thm)],[t2018,t97]) ).
cnf(t99,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t97,t89]) ).
cnf(t313,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t99]) ).
cnf(t19442,plain,
join(top,meet(X1,X2)) = join(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t19441,t313]) ).
cnf(t19443,plain,
join(top,meet(X1,X2)) = join(top,X2),
inference(step,[status(thm)],[t19442,t385]) ).
cnf(t2137,plain,
join(top,meet(X1,X2)) = join(top,X2),
inference(orient,[status(thm)],[t19443]) ).
cnf(t2157,plain,
join(top,X1) = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t2137,t123]) ).
cnf(t19446,plain,
join(top,X1) = join(top,X2),
inference(step,[status(thm)],[t2157,t2137]) ).
cnf(t2161,plain,
join(top,X1) = join(top,X2),
inference(orient,[status(thm)],[t19446]) ).
cnf(t2169,plain,
join(top,X1) = top,
inference(cp,[status(thm)],[t2161,t92]) ).
cnf(t2223,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t2169]) ).
cnf(t2235,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t2223,t89]) ).
cnf(t2278,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t2235]) ).
cnf(t2282,plain,
X1 = join(meet(X1,top),complement(top)),
inference(cp,[status(thm)],[t1940,t2278]) ).
cnf(t19472,plain,
X1 = join(complement(top),meet(X1,top)),
inference(step,[status(thm)],[t2282,t89]) ).
cnf(t19473,plain,
X1 = join(zero,meet(X1,top)),
inference(step,[status(thm)],[t19472,t112]) ).
cnf(t2349,plain,
join(zero,meet(X1,top)) = X1,
inference(orient,[status(thm)],[t19473]) ).
cnf(t19522,plain,
complement(X1) = meet(top,join(complement(X1),zero)),
inference(step,[status(thm)],[t3105,t2349]) ).
cnf(t19523,plain,
complement(X1) = meet(top,join(zero,complement(X1))),
inference(step,[status(thm)],[t19522,t89]) ).
cnf(t3124,plain,
meet(top,join(zero,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t19523]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t53,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t54,plain,
complement(X1) = join(composition(X2,complement(composition(converse(X2),X1))),complement(X1)),
inference(cp,[status(thm)],[t53,t29]) ).
cnf(t19656,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(step,[status(thm)],[t54,t89]) ).
cnf(t5232,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t19656]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t47,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t49,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t47,t29]) ).
cnf(t210,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t49]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t211,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t210,t25]) ).
cnf(t19318,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t211,t29]) ).
cnf(t220,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t19318]) ).
cnf(t221,plain,
one = converse(one),
inference(cp,[status(thm)],[t220,t25]) ).
cnf(t258,plain,
converse(one) = one,
inference(orient,[status(thm)],[t221]) ).
cnf(t19322,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t220,t258]) ).
cnf(t265,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t19322]) ).
cnf(t266,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t265]) ).
cnf(t5265,plain,
complement(X1) = join(complement(X1),complement(composition(converse(one),X1))),
inference(cp,[status(thm)],[t5232,t266]) ).
cnf(t19657,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t5265,t258]) ).
cnf(t19658,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t19657,t266]) ).
cnf(t5305,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t19658]) ).
cnf(t5364,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t72,t5305]) ).
cnf(t5416,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t5364]) ).
cnf(t5439,plain,
complement(complement(X1)) = meet(top,join(zero,meet(X1,X1))),
inference(cp,[status(thm)],[t3124,t5416]) ).
cnf(t1941,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t1940,t81]) ).
cnf(t19429,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t1941,t72]) ).
cnf(t2019,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t19429]) ).
cnf(t19685,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t5439,t2019]) ).
cnf(t5492,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t19685]) ).
cnf(t5369,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t1940,t5305]) ).
cnf(t19742,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t5369,t81]) ).
cnf(t27,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(join(complement(X1),complement(X2))),join(complement(X1),X2)))),
inference(cp,[status(thm)],[t26,t26]) ).
cnf(t19319,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(join(complement(X1),X2),complement(join(complement(X1),complement(X2)))))),
inference(step,[status(thm)],[t27,t89]) ).
cnf(t19320,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,complement(join(complement(X1),complement(X2))))))),
inference(step,[status(thm)],[t19319,t97]) ).
cnf(t19321,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t19320,t72]) ).
cnf(t225,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t19321]) ).
cnf(t5421,plain,
join(complement(X1),complement(X1)) = join(complement(X1),complement(join(complement(X1),join(X1,complement(complement(X1)))))),
inference(cp,[status(thm)],[t225,t5416]) ).
cnf(t19694,plain,
complement(X1) = join(complement(X1),complement(join(complement(X1),join(X1,complement(complement(X1)))))),
inference(step,[status(thm)],[t5421,t5305]) ).
cnf(t19461,plain,
join(X1,join(X2,complement(X1))) = top,
inference(step,[status(thm)],[t490,t2223]) ).
cnf(t2230,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t19461]) ).
cnf(t19695,plain,
complement(X1) = join(complement(X1),complement(top)),
inference(step,[status(thm)],[t19694,t2230]) ).
cnf(t19696,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t19695,t112]) ).
cnf(t19697,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t19696,t89]) ).
cnf(t5620,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t19697]) ).
cnf(t19743,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t19742,t5620]) ).
cnf(t19744,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t19743,t5492]) ).
cnf(t5873,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t19744]) ).
cnf(t19753,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t5492,t5873]) ).
cnf(t5882,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t19753]) ).
cnf(t19686,plain,
meet(X1,X1) = meet(top,X1),
inference(step,[status(thm)],[t5416,t5492]) ).
cnf(t5564,plain,
meet(X1,X1) = meet(top,X1),
inference(rw,[status(thm)],[t19686]) ).
cnf(t5566,plain,
meet(X1,X1) = meet(top,X1),
inference(orient,[status(thm)],[t5564]) ).
cnf(t5577,plain,
meet(X1,X1) = meet(X1,top),
inference(cp,[status(thm)],[t5566,t123]) ).
cnf(t5599,plain,
meet(X1,X1) = meet(X1,top),
inference(orient,[status(thm)],[t5577]) ).
cnf(t19755,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t5566,t5873]) ).
cnf(t5891,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t19755]) ).
cnf(t5903,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t5891]) ).
cnf(t19767,plain,
X1 = meet(X1,top),
inference(step,[status(thm)],[t5599,t5903]) ).
cnf(t5913,plain,
X1 = meet(X1,top),
inference(rw,[status(thm)],[t19767]) ).
cnf(t5932,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t5913]) ).
cnf(t5934,plain,
meet(join(complement(X1),complement(top)),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t1065,t5932]) ).
cnf(t19825,plain,
meet(join(complement(X1),zero),X2) = complement(join(X1,complement(X2))),
inference(step,[status(thm)],[t5934,t112]) ).
cnf(t1958,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t1940,t72]) ).
cnf(t19482,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t1958,t89]) ).
cnf(t2477,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t19482]) ).
cnf(t5905,plain,
X1 = join(X1,meet(X1,complement(X1))),
inference(cp,[status(thm)],[t2477,t5903]) ).
cnf(t19769,plain,
X1 = join(X1,zero),
inference(step,[status(thm)],[t5905,t81]) ).
cnf(t5915,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t19769]) ).
cnf(t19826,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(step,[status(thm)],[t19825,t5915]) ).
cnf(t6694,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t19826]) ).
cnf(t6710,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t5882,t6694]) ).
cnf(t7182,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t6710]) ).
cnf(t7195,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t7182,t5882]) ).
cnf(t7954,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t7195]) ).
cnf(t20156,plain,
X1 = complement(meet(join(complement(X1),sFlat0),join(complement(X1),sk3))),
inference(step,[status(thm)],[t68,t7954]) ).
cnf(t20157,plain,
X1 = complement(meet(join(sFlat0,complement(X1)),join(complement(X1),sk3))),
inference(step,[status(thm)],[t20156,t89]) ).
cnf(t20158,plain,
X1 = complement(meet(join(sFlat0,complement(X1)),join(sk3,complement(X1)))),
inference(step,[status(thm)],[t20157,t89]) ).
cnf(t11023,plain,
complement(meet(join(sFlat0,complement(X1)),join(sk3,complement(X1)))) = X1,
inference(orient,[status(thm)],[t20158]) ).
cnf(t73,plain,
meet(sFlat3,X1) = complement(join(sFlat4,complement(X1))),
inference(cp,[status(thm)],[t72,t61]) ).
cnf(t147,plain,
complement(join(sFlat4,complement(X1))) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t73]) ).
cnf(t150,plain,
meet(sFlat3,sFlat3) = complement(join(sFlat4,sFlat4)),
inference(cp,[status(thm)],[t147,t61]) ).
cnf(t163,plain,
complement(join(sFlat4,sFlat4)) = meet(sFlat3,sFlat3),
inference(orient,[status(thm)],[t150]) ).
cnf(t230,plain,
join(complement(join(sFlat4,sFlat4)),complement(X1)) = join(meet(sFlat3,sFlat3),complement(join(complement(join(sFlat4,sFlat4)),join(X1,meet(join(sFlat4,sFlat4),X1))))),
inference(cp,[status(thm)],[t225,t163]) ).
cnf(t20667,plain,
join(meet(sFlat3,sFlat3),complement(X1)) = join(meet(sFlat3,sFlat3),complement(join(complement(join(sFlat4,sFlat4)),join(X1,meet(join(sFlat4,sFlat4),X1))))),
inference(step,[status(thm)],[t230,t163]) ).
cnf(t20668,plain,
join(meet(sFlat3,sFlat3),complement(X1)) = join(meet(sFlat3,sFlat3),complement(join(meet(sFlat3,sFlat3),join(X1,meet(join(sFlat4,sFlat4),X1))))),
inference(step,[status(thm)],[t20667,t163]) ).
cnf(t5422,plain,
meet(sFlat3,sFlat3) = complement(sFlat4),
inference(cp,[status(thm)],[t5416,t61]) ).
cnf(t5474,plain,
meet(sFlat3,sFlat3) = complement(sFlat4),
inference(orient,[status(thm)],[t5422]) ).
cnf(t5481,plain,
sFlat3 = join(complement(sFlat4),meet(sFlat3,complement(sFlat3))),
inference(cp,[status(thm)],[t2477,t5474]) ).
cnf(t19723,plain,
sFlat3 = join(complement(sFlat4),zero),
inference(step,[status(thm)],[t5481,t81]) ).
cnf(t19724,plain,
sFlat3 = join(zero,complement(sFlat4)),
inference(step,[status(thm)],[t19723,t89]) ).
cnf(t19725,plain,
sFlat3 = complement(sFlat4),
inference(step,[status(thm)],[t19724,t5620]) ).
cnf(t5777,plain,
complement(sFlat4) = sFlat3,
inference(orient,[status(thm)],[t19725]) ).
cnf(t19726,plain,
meet(sFlat3,sFlat3) = sFlat3,
inference(step,[status(thm)],[t5474,t5777]) ).
cnf(t5778,plain,
meet(sFlat3,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t19726]) ).
cnf(t20669,plain,
join(sFlat3,complement(X1)) = join(meet(sFlat3,sFlat3),complement(join(meet(sFlat3,sFlat3),join(X1,meet(join(sFlat4,sFlat4),X1))))),
inference(step,[status(thm)],[t20668,t5778]) ).
cnf(t20670,plain,
join(sFlat3,complement(X1)) = join(sFlat3,complement(join(meet(sFlat3,sFlat3),join(X1,meet(join(sFlat4,sFlat4),X1))))),
inference(step,[status(thm)],[t20669,t5778]) ).
cnf(t20671,plain,
join(sFlat3,complement(X1)) = join(sFlat3,complement(join(sFlat3,join(X1,meet(join(sFlat4,sFlat4),X1))))),
inference(step,[status(thm)],[t20670,t5778]) ).
cnf(t5333,plain,
complement(sFlat3) = join(sFlat4,complement(sFlat3)),
inference(cp,[status(thm)],[t5305,t61]) ).
cnf(t19659,plain,
sFlat4 = join(sFlat4,complement(sFlat3)),
inference(step,[status(thm)],[t5333,t61]) ).
cnf(t19660,plain,
sFlat4 = join(sFlat4,sFlat4),
inference(step,[status(thm)],[t19659,t61]) ).
cnf(t5378,plain,
join(sFlat4,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t19660]) ).
cnf(t20672,plain,
join(sFlat3,complement(X1)) = join(sFlat3,complement(join(sFlat3,join(X1,meet(sFlat4,X1))))),
inference(step,[status(thm)],[t20671,t5378]) ).
cnf(t19040,plain,
join(sFlat3,complement(join(sFlat3,join(X1,meet(sFlat4,X1))))) = join(sFlat3,complement(X1)),
inference(orient,[status(thm)],[t20672]) ).
cnf(t19062,plain,
join(sFlat3,complement(X1)) = join(sFlat3,complement(join(sFlat3,join(X1,meet(X1,sFlat4))))),
inference(cp,[status(thm)],[t19040,t123]) ).
cnf(t6708,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t6694,t5882]) ).
cnf(t7100,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t6708]) ).
cnf(t7101,plain,
complement(join(X1,X1)) = complement(X1),
inference(cp,[status(thm)],[t7100,t5903]) ).
cnf(t7132,plain,
complement(join(X1,X1)) = complement(X1),
inference(orient,[status(thm)],[t7101]) ).
cnf(t7142,plain,
join(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t5882,t7132]) ).
cnf(t19866,plain,
join(X1,X1) = X1,
inference(step,[status(thm)],[t7142,t5882]) ).
cnf(t7170,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t19866]) ).
cnf(t102,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t97,t89]) ).
cnf(t19324,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t102,t97]) ).
cnf(t319,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t19324]) ).
cnf(t7172,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t7170,t319]) ).
cnf(t19880,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t7172,t97]) ).
cnf(t19881,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t19880,t7170]) ).
cnf(t7335,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t19881]) ).
cnf(t7341,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t7335,t1940]) ).
cnf(t19892,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t7341,t1940]) ).
cnf(t19893,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t19892,t89]) ).
cnf(t7373,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t19893]) ).
cnf(t20687,plain,
join(sFlat3,complement(X1)) = join(sFlat3,complement(join(sFlat3,X1))),
inference(step,[status(thm)],[t19062,t7373]) ).
cnf(t19098,plain,
join(sFlat3,complement(join(sFlat3,X1))) = join(sFlat3,complement(X1)),
inference(orient,[status(thm)],[t20687]) ).
cnf(t78,plain,
meet(X1,join(complement(X2),complement(X3))) = complement(join(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t72,t72]) ).
cnf(t1108,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,join(complement(X2),complement(X3))),
inference(orient,[status(thm)],[t78]) ).
cnf(t18,axiom,
sFlat5 = meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),
introduced(definition) ).
cnf(t19250,plain,
sFlat5 = meet(composition(sk1,meet(sk2,sFlat0)),complement(composition(sk1,sk3))),
inference(step,[status(thm)],[t18,t66]) ).
cnf(t19251,plain,
sFlat5 = meet(composition(sk1,meet(sk2,sFlat0)),complement(sFlat3)),
inference(step,[status(thm)],[t19250,t32]) ).
cnf(t19252,plain,
sFlat5 = meet(composition(sk1,meet(sk2,sFlat0)),sFlat4),
inference(step,[status(thm)],[t19251,t61]) ).
cnf(t85,plain,
meet(composition(sk1,meet(sk2,sFlat0)),sFlat4) = sFlat5,
inference(orient,[status(thm)],[t19252]) ).
cnf(t14,axiom,
sFlat1 = meet(sk2,complement(sk3)),
introduced(definition) ).
cnf(t19256,plain,
sFlat1 = meet(sk2,sFlat0),
inference(step,[status(thm)],[t14,t66]) ).
cnf(t87,plain,
meet(sk2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t19256]) ).
cnf(t19257,plain,
meet(composition(sk1,sFlat1),sFlat4) = sFlat5,
inference(step,[status(thm)],[t85,t87]) ).
cnf(t88,plain,
meet(composition(sk1,sFlat1),sFlat4) = sFlat5,
inference(rw,[status(thm)],[t19257]) ).
cnf(t19313,plain,
meet(sFlat4,composition(sk1,sFlat1)) = sFlat5,
inference(step,[status(thm)],[t88,t123]) ).
cnf(t15,axiom,
sFlat2 = composition(sk1,meet(sk2,complement(sk3))),
introduced(definition) ).
cnf(t34,plain,
composition(sk1,meet(sk2,complement(sk3))) = sFlat2,
inference(orient,[status(thm)],[t15]) ).
cnf(t19248,plain,
composition(sk1,meet(sk2,sFlat0)) = sFlat2,
inference(step,[status(thm)],[t34,t66]) ).
cnf(t71,plain,
composition(sk1,meet(sk2,sFlat0)) = sFlat2,
inference(rw,[status(thm)],[t19248]) ).
cnf(t19311,plain,
composition(sk1,meet(sFlat0,sk2)) = sFlat2,
inference(step,[status(thm)],[t71,t123]) ).
cnf(t125,plain,
meet(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t87]) ).
cnf(t19309,plain,
meet(sFlat0,sk2) = sFlat1,
inference(step,[status(thm)],[t125,t123]) ).
cnf(t133,plain,
meet(sFlat0,sk2) = sFlat1,
inference(orient,[status(thm)],[t19309]) ).
cnf(t19312,plain,
composition(sk1,sFlat1) = sFlat2,
inference(step,[status(thm)],[t19311,t133]) ).
cnf(t135,plain,
composition(sk1,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t19312]) ).
cnf(t19314,plain,
meet(sFlat4,sFlat2) = sFlat5,
inference(step,[status(thm)],[t19313,t135]) ).
cnf(t19315,plain,
meet(sFlat2,sFlat4) = sFlat5,
inference(step,[status(thm)],[t19314,t123]) ).
cnf(t139,plain,
meet(sFlat2,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t19315]) ).
cnf(t1129,plain,
meet(X1,join(complement(sFlat2),complement(sFlat4))) = complement(join(complement(X1),sFlat5)),
inference(cp,[status(thm)],[t1108,t139]) ).
cnf(t19428,plain,
meet(X1,join(complement(sFlat2),complement(sFlat4))) = complement(join(sFlat5,complement(X1))),
inference(step,[status(thm)],[t1129,t89]) ).
cnf(t1936,plain,
meet(X1,join(complement(sFlat2),complement(sFlat4))) = complement(join(sFlat5,complement(X1))),
inference(orient,[status(thm)],[t19428]) ).
cnf(t2020,plain,
join(complement(sFlat2),complement(sFlat4)) = join(zero,complement(join(sFlat5,complement(join(complement(sFlat2),complement(sFlat4)))))),
inference(cp,[status(thm)],[t2019,t1936]) ).
cnf(t19488,plain,
join(complement(sFlat2),complement(sFlat4)) = join(zero,complement(join(sFlat5,meet(sFlat2,sFlat4)))),
inference(step,[status(thm)],[t2020,t72]) ).
cnf(t19489,plain,
join(complement(sFlat2),complement(sFlat4)) = join(zero,complement(join(sFlat5,sFlat5))),
inference(step,[status(thm)],[t19488,t139]) ).
cnf(t2542,plain,
join(zero,complement(join(sFlat5,sFlat5))) = join(complement(sFlat2),complement(sFlat4)),
inference(orient,[status(thm)],[t19489]) ).
cnf(t19710,plain,
complement(join(sFlat5,sFlat5)) = join(complement(sFlat2),complement(sFlat4)),
inference(step,[status(thm)],[t2542,t5620]) ).
cnf(t5657,plain,
complement(join(sFlat5,sFlat5)) = join(complement(sFlat2),complement(sFlat4)),
inference(rw,[status(thm)],[t19710]) ).
cnf(t2515,plain,
X1 = join(meet(X1,sk3),meet(X1,sFlat0)),
inference(cp,[status(thm)],[t2477,t66]) ).
cnf(t19484,plain,
X1 = join(meet(X1,sFlat0),meet(X1,sk3)),
inference(step,[status(thm)],[t2515,t89]) ).
cnf(t2528,plain,
join(meet(X1,sFlat0),meet(X1,sk3)) = X1,
inference(orient,[status(thm)],[t19484]) ).
cnf(t3129,plain,
complement(join(sFlat5,sFlat5)) = meet(top,join(complement(sFlat2),complement(sFlat4))),
inference(cp,[status(thm)],[t3124,t2542]) ).
cnf(t19556,plain,
complement(join(sFlat5,sFlat5)) = complement(join(zero,meet(sFlat2,sFlat4))),
inference(step,[status(thm)],[t3129,t3048]) ).
cnf(t19557,plain,
complement(join(sFlat5,sFlat5)) = complement(join(zero,sFlat5)),
inference(step,[status(thm)],[t19556,t139]) ).
cnf(t19558,plain,
complement(join(sFlat5,sFlat5)) = complement(join(sFlat5,zero)),
inference(step,[status(thm)],[t19557,t89]) ).
cnf(t3207,plain,
complement(join(sFlat5,zero)) = complement(join(sFlat5,sFlat5)),
inference(orient,[status(thm)],[t19558]) ).
cnf(t3210,plain,
meet(join(sFlat5,zero),X1) = complement(join(complement(join(sFlat5,sFlat5)),complement(X1))),
inference(cp,[status(thm)],[t72,t3207]) ).
cnf(t19582,plain,
meet(join(sFlat5,zero),X1) = meet(join(sFlat5,sFlat5),X1),
inference(step,[status(thm)],[t3210,t72]) ).
cnf(t3376,plain,
meet(join(sFlat5,zero),X1) = meet(join(sFlat5,sFlat5),X1),
inference(orient,[status(thm)],[t19582]) ).
cnf(t3378,plain,
join(sFlat5,zero) = join(meet(join(sFlat5,sFlat5),sFlat0),meet(join(sFlat5,zero),sk3)),
inference(cp,[status(thm)],[t2528,t3376]) ).
cnf(t19583,plain,
join(sFlat5,zero) = join(meet(join(sFlat5,sFlat5),sFlat0),meet(join(sFlat5,sFlat5),sk3)),
inference(step,[status(thm)],[t3378,t3376]) ).
cnf(t19584,plain,
join(sFlat5,zero) = join(sFlat5,sFlat5),
inference(step,[status(thm)],[t19583,t2528]) ).
cnf(t3391,plain,
join(sFlat5,zero) = join(sFlat5,sFlat5),
inference(orient,[status(thm)],[t19584]) ).
cnf(t19770,plain,
sFlat5 = join(sFlat5,sFlat5),
inference(step,[status(thm)],[t3391,t5915]) ).
cnf(t5931,plain,
sFlat5 = join(sFlat5,sFlat5),
inference(rw,[status(thm)],[t19770]) ).
cnf(t5966,plain,
join(sFlat5,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t5931]) ).
cnf(t19849,plain,
complement(sFlat5) = join(complement(sFlat2),complement(sFlat4)),
inference(step,[status(thm)],[t5657,t5966]) ).
cnf(t19850,plain,
complement(sFlat5) = join(complement(sFlat2),sFlat3),
inference(step,[status(thm)],[t19849,t5777]) ).
cnf(t19851,plain,
complement(sFlat5) = join(sFlat3,complement(sFlat2)),
inference(step,[status(thm)],[t19850,t89]) ).
cnf(t7014,plain,
join(sFlat3,complement(sFlat2)) = complement(sFlat5),
inference(orient,[status(thm)],[t19851]) ).
cnf(t19107,plain,
join(sFlat3,complement(complement(sFlat2))) = join(sFlat3,complement(complement(sFlat5))),
inference(cp,[status(thm)],[t19098,t7014]) ).
cnf(t20693,plain,
join(sFlat3,sFlat2) = join(sFlat3,complement(complement(sFlat5))),
inference(step,[status(thm)],[t19107,t5882]) ).
cnf(t20694,plain,
join(sFlat2,sFlat3) = join(sFlat3,complement(complement(sFlat5))),
inference(step,[status(thm)],[t20693,t89]) ).
cnf(t20695,plain,
join(sFlat2,sFlat3) = join(sFlat3,sFlat5),
inference(step,[status(thm)],[t20694,t5882]) ).
cnf(t19144,plain,
join(sFlat3,sFlat5) = join(sFlat2,sFlat3),
inference(orient,[status(thm)],[t20695]) ).
cnf(t19146,plain,
join(sFlat3,complement(sFlat5)) = join(sFlat3,complement(join(sFlat2,sFlat3))),
inference(cp,[status(thm)],[t19098,t19144]) ).
cnf(t7346,plain,
join(sFlat3,complement(sFlat2)) = join(sFlat3,complement(sFlat5)),
inference(cp,[status(thm)],[t7335,t7014]) ).
cnf(t19887,plain,
complement(sFlat5) = join(sFlat3,complement(sFlat5)),
inference(step,[status(thm)],[t7346,t7014]) ).
cnf(t7357,plain,
join(sFlat3,complement(sFlat5)) = complement(sFlat5),
inference(orient,[status(thm)],[t19887]) ).
cnf(t20696,plain,
complement(sFlat5) = join(sFlat3,complement(join(sFlat2,sFlat3))),
inference(step,[status(thm)],[t19146,t7357]) ).
cnf(t6706,plain,
meet(complement(X1),sFlat4) = complement(join(X1,sFlat3)),
inference(cp,[status(thm)],[t6694,t5777]) ).
cnf(t19828,plain,
meet(sFlat4,complement(X1)) = complement(join(X1,sFlat3)),
inference(step,[status(thm)],[t6706,t123]) ).
cnf(t6751,plain,
complement(join(X1,sFlat3)) = meet(sFlat4,complement(X1)),
inference(orient,[status(thm)],[t19828]) ).
cnf(t20697,plain,
complement(sFlat5) = join(sFlat3,meet(sFlat4,complement(sFlat2))),
inference(step,[status(thm)],[t20696,t6751]) ).
cnf(t19055,plain,
join(sFlat3,complement(sFlat6)) = join(sFlat3,complement(join(sFlat3,join(sFlat6,sFlat7)))),
inference(cp,[status(thm)],[t19040,t134]) ).
cnf(t7197,plain,
join(sFlat3,complement(X1)) = complement(meet(sFlat4,X1)),
inference(cp,[status(thm)],[t7182,t61]) ).
cnf(t7237,plain,
complement(meet(sFlat4,X1)) = join(sFlat3,complement(X1)),
inference(orient,[status(thm)],[t7197]) ).
cnf(t7238,plain,
join(sFlat3,complement(sFlat6)) = complement(sFlat7),
inference(cp,[status(thm)],[t7237,t134]) ).
cnf(t7312,plain,
join(sFlat3,complement(sFlat6)) = complement(sFlat7),
inference(orient,[status(thm)],[t7238]) ).
cnf(t20681,plain,
complement(sFlat7) = join(sFlat3,complement(join(sFlat3,join(sFlat6,sFlat7)))),
inference(step,[status(thm)],[t19055,t7312]) ).
cnf(t2487,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t2477,t123]) ).
cnf(t3505,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t2487]) ).
cnf(t7313,plain,
top = join(sFlat6,complement(sFlat7)),
inference(cp,[status(thm)],[t2230,t7312]) ).
cnf(t7364,plain,
join(sFlat6,complement(sFlat7)) = top,
inference(orient,[status(thm)],[t7313]) ).
cnf(t7365,plain,
meet(complement(sFlat6),sFlat7) = complement(top),
inference(cp,[status(thm)],[t6694,t7364]) ).
cnf(t19943,plain,
meet(sFlat7,complement(sFlat6)) = complement(top),
inference(step,[status(thm)],[t7365,t123]) ).
cnf(t19944,plain,
meet(sFlat7,complement(sFlat6)) = zero,
inference(step,[status(thm)],[t19943,t112]) ).
cnf(t8018,plain,
meet(sFlat7,complement(sFlat6)) = zero,
inference(orient,[status(thm)],[t19944]) ).
cnf(t8019,plain,
sFlat7 = join(zero,meet(complement(complement(sFlat6)),sFlat7)),
inference(cp,[status(thm)],[t3505,t8018]) ).
cnf(t19771,plain,
join(zero,X1) = X1,
inference(step,[status(thm)],[t2349,t5932]) ).
cnf(t5937,plain,
join(zero,X1) = X1,
inference(rw,[status(thm)],[t19771]) ).
cnf(t5940,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t5937]) ).
cnf(t19945,plain,
sFlat7 = meet(complement(complement(sFlat6)),sFlat7),
inference(step,[status(thm)],[t8019,t5940]) ).
cnf(t19946,plain,
sFlat7 = meet(sFlat7,complement(complement(sFlat6))),
inference(step,[status(thm)],[t19945,t123]) ).
cnf(t19947,plain,
sFlat7 = meet(sFlat7,sFlat6),
inference(step,[status(thm)],[t19946,t5882]) ).
cnf(t19948,plain,
sFlat7 = meet(sFlat6,sFlat7),
inference(step,[status(thm)],[t19947,t123]) ).
cnf(t8022,plain,
meet(sFlat6,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t19948]) ).
cnf(t8023,plain,
sFlat6 = join(sFlat6,sFlat7),
inference(cp,[status(thm)],[t7373,t8022]) ).
cnf(t8138,plain,
join(sFlat6,sFlat7) = sFlat6,
inference(orient,[status(thm)],[t8023]) ).
cnf(t20682,plain,
complement(sFlat7) = join(sFlat3,complement(join(sFlat3,sFlat6))),
inference(step,[status(thm)],[t20681,t8138]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t106,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t214,plain,
converse(join(composition(converse(X1),X2),X3)) = join(composition(converse(X2),X1),converse(X3)),
inference(cp,[status(thm)],[t106,t210]) ).
cnf(t4089,plain,
converse(join(composition(converse(X1),X2),X3)) = join(composition(converse(X2),X1),converse(X3)),
inference(orient,[status(thm)],[t214]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t38,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t51,plain,
composition(join(X1,converse(X2)),converse(X3)) = join(composition(X1,converse(X3)),converse(composition(X3,X2))),
inference(cp,[status(thm)],[t38,t47]) ).
cnf(t3801,plain,
join(composition(X1,converse(X2)),converse(composition(X2,X3))) = composition(join(X1,converse(X3)),converse(X2)),
inference(orient,[status(thm)],[t51]) ).
cnf(t4095,plain,
join(composition(converse(converse(X1)),X2),converse(converse(composition(X1,X3)))) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(cp,[status(thm)],[t4089,t3801]) ).
cnf(t19608,plain,
join(composition(X1,X2),converse(converse(composition(X1,X3)))) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t4095,t29]) ).
cnf(t19609,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t19608,t29]) ).
cnf(t48,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t47,t29]) ).
cnf(t203,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t48]) ).
cnf(t19610,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,converse(join(converse(X2),converse(X3)))),
inference(step,[status(thm)],[t19609,t203]) ).
cnf(t107,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t106,t29]) ).
cnf(t285,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t107]) ).
cnf(t19611,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t19610,t285]) ).
cnf(t19612,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t19611,t29]) ).
cnf(t4150,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t19612]) ).
cnf(t4204,plain,
composition(sk1,join(X1,sk2)) = join(composition(sk1,X1),sFlat6),
inference(cp,[status(thm)],[t4150,t36]) ).
cnf(t19616,plain,
composition(sk1,join(X1,sk2)) = join(sFlat6,composition(sk1,X1)),
inference(step,[status(thm)],[t4204,t89]) ).
cnf(t4421,plain,
composition(sk1,join(X1,sk2)) = join(sFlat6,composition(sk1,X1)),
inference(orient,[status(thm)],[t19616]) ).
cnf(t74,plain,
meet(sk3,X1) = complement(join(sFlat0,complement(X1))),
inference(cp,[status(thm)],[t72,t66]) ).
cnf(t175,plain,
complement(join(sFlat0,complement(X1))) = meet(sk3,X1),
inference(orient,[status(thm)],[t74]) ).
cnf(t182,plain,
meet(sk3,sk3) = complement(join(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t175,t66]) ).
cnf(t196,plain,
complement(join(sFlat0,sFlat0)) = meet(sk3,sk3),
inference(orient,[status(thm)],[t182]) ).
cnf(t226,plain,
join(complement(join(sFlat0,sFlat0)),complement(X1)) = join(meet(sk3,sk3),complement(join(complement(join(sFlat0,sFlat0)),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(cp,[status(thm)],[t225,t196]) ).
cnf(t20459,plain,
join(meet(sk3,sk3),complement(X1)) = join(meet(sk3,sk3),complement(join(complement(join(sFlat0,sFlat0)),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t226,t196]) ).
cnf(t20460,plain,
join(meet(sk3,sk3),complement(X1)) = join(meet(sk3,sk3),complement(join(meet(sk3,sk3),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t20459,t196]) ).
cnf(t20461,plain,
join(sk3,complement(X1)) = join(meet(sk3,sk3),complement(join(meet(sk3,sk3),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t20460,t5903]) ).
cnf(t20462,plain,
join(sk3,complement(X1)) = join(sk3,complement(join(meet(sk3,sk3),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t20461,t5903]) ).
cnf(t20463,plain,
join(sk3,complement(X1)) = join(sk3,complement(join(sk3,join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t20462,t5903]) ).
cnf(t5334,plain,
complement(sk3) = join(sFlat0,complement(sk3)),
inference(cp,[status(thm)],[t5305,t66]) ).
cnf(t19668,plain,
sFlat0 = join(sFlat0,complement(sk3)),
inference(step,[status(thm)],[t5334,t66]) ).
cnf(t19669,plain,
sFlat0 = join(sFlat0,sFlat0),
inference(step,[status(thm)],[t19668,t66]) ).
cnf(t5390,plain,
join(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t19669]) ).
cnf(t20464,plain,
join(sk3,complement(X1)) = join(sk3,complement(join(sk3,join(X1,meet(sFlat0,X1))))),
inference(step,[status(thm)],[t20463,t5390]) ).
cnf(t15546,plain,
join(sk3,complement(join(sk3,join(X1,meet(sFlat0,X1))))) = join(sk3,complement(X1)),
inference(orient,[status(thm)],[t20464]) ).
cnf(t15562,plain,
join(sk3,complement(X1)) = join(sk3,complement(join(sk3,join(X1,meet(X1,sFlat0))))),
inference(cp,[status(thm)],[t15546,t123]) ).
cnf(t20476,plain,
join(sk3,complement(X1)) = join(sk3,complement(join(sk3,X1))),
inference(step,[status(thm)],[t15562,t7373]) ).
cnf(t15667,plain,
join(sk3,complement(join(sk3,X1))) = join(sk3,complement(X1)),
inference(orient,[status(thm)],[t20476]) ).
cnf(t7198,plain,
join(sk3,complement(X1)) = complement(meet(sFlat0,X1)),
inference(cp,[status(thm)],[t7182,t66]) ).
cnf(t7274,plain,
complement(meet(sFlat0,X1)) = join(sk3,complement(X1)),
inference(orient,[status(thm)],[t7198]) ).
cnf(t7276,plain,
join(sk3,complement(sk2)) = complement(sFlat1),
inference(cp,[status(thm)],[t7274,t133]) ).
cnf(t7315,plain,
join(sk3,complement(sk2)) = complement(sFlat1),
inference(orient,[status(thm)],[t7276]) ).
cnf(t15672,plain,
join(sk3,complement(complement(sk2))) = join(sk3,complement(complement(sFlat1))),
inference(cp,[status(thm)],[t15667,t7315]) ).
cnf(t20477,plain,
join(sk3,sk2) = join(sk3,complement(complement(sFlat1))),
inference(step,[status(thm)],[t15672,t5882]) ).
cnf(t20478,plain,
join(sk3,sk2) = join(sk3,sFlat1),
inference(step,[status(thm)],[t20477,t5882]) ).
cnf(t20479,plain,
join(sk3,sk2) = join(sFlat1,sk3),
inference(step,[status(thm)],[t20478,t89]) ).
cnf(t15701,plain,
join(sk3,sk2) = join(sFlat1,sk3),
inference(orient,[status(thm)],[t20479]) ).
cnf(t15703,plain,
join(sFlat6,composition(sk1,sk3)) = composition(sk1,join(sFlat1,sk3)),
inference(cp,[status(thm)],[t4421,t15701]) ).
cnf(t20480,plain,
join(sFlat6,sFlat3) = composition(sk1,join(sFlat1,sk3)),
inference(step,[status(thm)],[t15703,t32]) ).
cnf(t20481,plain,
join(sFlat3,sFlat6) = composition(sk1,join(sFlat1,sk3)),
inference(step,[status(thm)],[t20480,t89]) ).
cnf(t4177,plain,
composition(sk1,join(sFlat1,X1)) = join(sFlat2,composition(sk1,X1)),
inference(cp,[status(thm)],[t4150,t135]) ).
cnf(t4316,plain,
composition(sk1,join(sFlat1,X1)) = join(sFlat2,composition(sk1,X1)),
inference(orient,[status(thm)],[t4177]) ).
cnf(t20482,plain,
join(sFlat3,sFlat6) = join(sFlat2,composition(sk1,sk3)),
inference(step,[status(thm)],[t20481,t4316]) ).
cnf(t20483,plain,
join(sFlat3,sFlat6) = join(sFlat2,sFlat3),
inference(step,[status(thm)],[t20482,t32]) ).
cnf(t15712,plain,
join(sFlat3,sFlat6) = join(sFlat2,sFlat3),
inference(orient,[status(thm)],[t20483]) ).
cnf(t20683,plain,
complement(sFlat7) = join(sFlat3,complement(join(sFlat2,sFlat3))),
inference(step,[status(thm)],[t20682,t15712]) ).
cnf(t20684,plain,
complement(sFlat7) = join(sFlat3,meet(sFlat4,complement(sFlat2))),
inference(step,[status(thm)],[t20683,t6751]) ).
cnf(t19087,plain,
join(sFlat3,meet(sFlat4,complement(sFlat2))) = complement(sFlat7),
inference(orient,[status(thm)],[t20684]) ).
cnf(t20698,plain,
complement(sFlat5) = complement(sFlat7),
inference(step,[status(thm)],[t20697,t19087]) ).
cnf(t19153,plain,
complement(sFlat7) = complement(sFlat5),
inference(orient,[status(thm)],[t20698]) ).
cnf(t19201,plain,
sFlat7 = complement(meet(join(sFlat0,complement(sFlat5)),join(sk3,complement(sFlat7)))),
inference(cp,[status(thm)],[t11023,t19153]) ).
cnf(t20706,plain,
sFlat7 = complement(meet(join(sFlat0,complement(sFlat5)),join(sk3,complement(sFlat5)))),
inference(step,[status(thm)],[t19201,t19153]) ).
cnf(t20707,plain,
sFlat7 = sFlat5,
inference(step,[status(thm)],[t20706,t11023]) ).
cnf(t19215,plain,
sFlat7 = sFlat5,
inference(orient,[status(thm)],[t20707]) ).
cnf(t20708,plain,
meet(sFlat4,sFlat6) = sFlat5,
inference(step,[status(thm)],[t134,t19215]) ).
cnf(t19216,plain,
meet(sFlat4,sFlat6) = sFlat5,
inference(orient,[status(thm)],[t20708]) ).
cnf(goal_0,negated_conjecture,
tuple(join(meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
tuple(join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[goal_0,t89]) ).
cnf(g0_1,plain,
tuple(join(meet(sFlat6,complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_0,t36]) ).
cnf(g0_2,plain,
tuple(join(meet(sFlat6,complement(sFlat3)),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_1,t32]) ).
cnf(g0_3,plain,
tuple(join(meet(sFlat6,sFlat4),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_2,t61]) ).
cnf(g0_4,plain,
tuple(join(meet(sFlat4,sFlat6),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_3,t123]) ).
cnf(g0_5,plain,
tuple(join(sFlat5,meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_4,t19216]) ).
cnf(g0_6,plain,
tuple(join(sFlat5,meet(complement(composition(sk1,sk3)),composition(sk1,meet(sk2,complement(sk3))))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_5,t123]) ).
cnf(g0_7,plain,
tuple(join(sFlat5,meet(complement(sFlat3),composition(sk1,meet(sk2,complement(sk3))))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_6,t32]) ).
cnf(g0_8,plain,
tuple(join(sFlat5,meet(sFlat4,composition(sk1,meet(sk2,complement(sk3))))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_7,t61]) ).
cnf(g0_9,plain,
tuple(join(sFlat5,meet(sFlat4,composition(sk1,meet(sk2,sFlat0)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_8,t66]) ).
cnf(g0_10,plain,
tuple(join(sFlat5,meet(sFlat4,composition(sk1,meet(sFlat0,sk2)))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_9,t123]) ).
cnf(g0_11,plain,
tuple(join(sFlat5,meet(sFlat4,composition(sk1,sFlat1))),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_10,t133]) ).
cnf(g0_12,plain,
tuple(join(sFlat5,meet(sFlat4,sFlat2)),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_11,t135]) ).
cnf(g0_13,plain,
tuple(join(sFlat5,meet(sFlat2,sFlat4)),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_12,t123]) ).
cnf(g0_14,plain,
tuple(join(sFlat5,sFlat5),join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_13,t139]) ).
cnf(g0_15,plain,
tuple(sFlat5,join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_14,t7170]) ).
cnf(g0_16,plain,
tuple(sFlat5,join(meet(sFlat6,complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_15,t36]) ).
cnf(g0_17,plain,
tuple(sFlat5,join(meet(sFlat6,complement(sFlat3)),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_16,t32]) ).
cnf(g0_18,plain,
tuple(sFlat5,join(meet(sFlat6,sFlat4),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_17,t61]) ).
cnf(g0_19,plain,
tuple(sFlat5,join(meet(sFlat4,sFlat6),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_18,t123]) ).
cnf(g0_20,plain,
tuple(sFlat5,join(sFlat5,meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_19,t19216]) ).
cnf(g0_21,plain,
tuple(sFlat5,join(sFlat5,meet(complement(composition(sk1,sk3)),composition(sk1,meet(sk2,complement(sk3)))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_20,t123]) ).
cnf(g0_22,plain,
tuple(sFlat5,join(sFlat5,meet(complement(sFlat3),composition(sk1,meet(sk2,complement(sk3)))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_21,t32]) ).
cnf(g0_23,plain,
tuple(sFlat5,join(sFlat5,meet(sFlat4,composition(sk1,meet(sk2,complement(sk3)))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_22,t61]) ).
cnf(g0_24,plain,
tuple(sFlat5,join(sFlat5,meet(sFlat4,composition(sk1,meet(sk2,sFlat0))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_23,t66]) ).
cnf(g0_25,plain,
tuple(sFlat5,join(sFlat5,meet(sFlat4,composition(sk1,meet(sFlat0,sk2))))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_24,t123]) ).
cnf(g0_26,plain,
tuple(sFlat5,join(sFlat5,meet(sFlat4,composition(sk1,sFlat1)))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_25,t133]) ).
cnf(g0_27,plain,
tuple(sFlat5,join(sFlat5,meet(sFlat4,sFlat2))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_26,t135]) ).
cnf(g0_28,plain,
tuple(sFlat5,join(sFlat5,meet(sFlat2,sFlat4))) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_27,t123]) ).
cnf(g0_29,plain,
tuple(sFlat5,join(sFlat5,sFlat5)) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_28,t139]) ).
cnf(g0_30,plain,
tuple(sFlat5,sFlat5) != tuple(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_29,t7170]) ).
cnf(g0_31,plain,
tuple(sFlat5,sFlat5) != tuple(meet(sFlat6,complement(composition(sk1,sk3))),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_30,t36]) ).
cnf(g0_32,plain,
tuple(sFlat5,sFlat5) != tuple(meet(sFlat6,complement(sFlat3)),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_31,t32]) ).
cnf(g0_33,plain,
tuple(sFlat5,sFlat5) != tuple(meet(sFlat6,sFlat4),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_32,t61]) ).
cnf(g0_34,plain,
tuple(sFlat5,sFlat5) != tuple(meet(sFlat4,sFlat6),meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_33,t123]) ).
cnf(g0_35,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(composition(sk1,meet(sk2,complement(sk3))),complement(composition(sk1,sk3)))),
inference(rw,[status(thm)],[g0_34,t19216]) ).
cnf(g0_36,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(complement(composition(sk1,sk3)),composition(sk1,meet(sk2,complement(sk3))))),
inference(rw,[status(thm)],[g0_35,t123]) ).
cnf(g0_37,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(complement(sFlat3),composition(sk1,meet(sk2,complement(sk3))))),
inference(rw,[status(thm)],[g0_36,t32]) ).
cnf(g0_38,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(sFlat4,composition(sk1,meet(sk2,complement(sk3))))),
inference(rw,[status(thm)],[g0_37,t61]) ).
cnf(g0_39,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(sFlat4,composition(sk1,meet(sk2,sFlat0)))),
inference(rw,[status(thm)],[g0_38,t66]) ).
cnf(g0_40,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(sFlat4,composition(sk1,meet(sFlat0,sk2)))),
inference(rw,[status(thm)],[g0_39,t123]) ).
cnf(g0_41,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(sFlat4,composition(sk1,sFlat1))),
inference(rw,[status(thm)],[g0_40,t133]) ).
cnf(g0_42,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(sFlat4,sFlat2)),
inference(rw,[status(thm)],[g0_41,t135]) ).
cnf(g0_43,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,meet(sFlat2,sFlat4)),
inference(rw,[status(thm)],[g0_42,t123]) ).
cnf(g0_44,plain,
tuple(sFlat5,sFlat5) != tuple(sFlat5,sFlat5),
inference(rw,[status(thm)],[g0_43,t139]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_44]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL016-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n005.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 07:12:17 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 61.92/8.22 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 61.92/8.22 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------