%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL028-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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:28 PM UTC 2026
% Result : Unsatisfiable 69.46s 9.21s
% Output : CNFRefutation 69.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 99
% Number of leaves : 19
% Syntax : Number of clauses : 610 ( 610 unt; 0 nHn; 269 RR)
% Number of literals : 610 ( 609 equ; 4 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 : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 517 ( 71 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t7,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t98,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
cnf(t6,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t51,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t100,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t98,t51]) ).
cnf(t65013,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t100,t98]) ).
cnf(t120,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t65013]) ).
cnf(t18,axiom,
sFlat0 = meet(sk1,sk2),
introduced(definition) ).
cnf(t110,plain,
meet(sk1,sk2) = sFlat0,
inference(orient,[status(thm)],[t18]) ).
cnf(t125,plain,
meet(sk1,sk2) = sFlat0,
inference(rw,[status(thm)],[t110]) ).
cnf(t65015,plain,
meet(sk2,sk1) = sFlat0,
inference(step,[status(thm)],[t125,t120]) ).
cnf(t129,plain,
meet(sk2,sk1) = sFlat0,
inference(orient,[status(thm)],[t65015]) ).
cnf(t19,axiom,
sFlat1 = composition(sk1,sk2),
introduced(definition) ).
cnf(t46,plain,
composition(sk1,sk2) = sFlat1,
inference(orient,[status(thm)],[t19]) ).
cnf(t11,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t54,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t13,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t65010,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t51]) ).
cnf(t62,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t65010]) ).
cnf(t8,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t37,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t39,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t37,t24]) ).
cnf(t210,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t39]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,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,t20]) ).
cnf(t65020,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t211,t24]) ).
cnf(t223,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t65020]) ).
cnf(t224,plain,
one = converse(one),
inference(cp,[status(thm)],[t223,t20]) ).
cnf(t233,plain,
converse(one) = one,
inference(orient,[status(thm)],[t224]) ).
cnf(t65021,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t223,t233]) ).
cnf(t243,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t65021]) ).
cnf(t244,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t243]) ).
cnf(t247,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t62,t244]) ).
cnf(t65025,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t247,t233]) ).
cnf(t65026,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t65025,t244]) ).
cnf(t294,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t65026]) ).
cnf(t295,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t294,t98]) ).
cnf(t65114,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t295,t98]) ).
cnf(t65115,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t65114,t98]) ).
cnf(t911,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t65115]) ).
cnf(t14,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t53,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t21]) ).
cnf(t65240,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t53,t51]) ).
cnf(t65241,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t65240,t98]) ).
cnf(t65242,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t65241,t51]) ).
cnf(t2291,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t65242]) ).
cnf(t5,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t105,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t2292,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t2291,t105]) ).
cnf(t65243,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t2292,t98]) ).
cnf(t2367,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t65243]) ).
cnf(t4,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t59,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t99,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t98,t59]) ).
cnf(t65011,plain,
zero = complement(top),
inference(step,[status(thm)],[t99,t105]) ).
cnf(t111,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t65011]) ).
cnf(t298,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t294,t111]) ).
cnf(t65027,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t298,t111]) ).
cnf(t65028,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t65027,t111]) ).
cnf(t305,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t65028]) ).
cnf(t306,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t54,t305]) ).
cnf(t330,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t306]) ).
cnf(t2371,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t330,t2367]) ).
cnf(t65245,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t2371,t2367]) ).
cnf(t2381,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t65245]) ).
cnf(t65246,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t2367,t2381]) ).
cnf(t2418,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t65246]) ).
cnf(t2480,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t2418]) ).
cnf(t2481,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t911,t2480]) ).
cnf(t65302,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t2481,t2480]) ).
cnf(t65303,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t65302,t2480]) ).
cnf(t2500,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t65303]) ).
cnf(t2502,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t54,t2500]) ).
cnf(t2615,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t2502]) ).
cnf(t2627,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t2615,t2291]) ).
cnf(t65308,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t2627,t2291]) ).
cnf(t65309,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t65308,t51]) ).
cnf(t2631,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t65309]) ).
cnf(t2634,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t2631,t120]) ).
cnf(t2667,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t2634]) ).
cnf(t2675,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t54,t2667]) ).
cnf(t9540,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t2675]) ).
cnf(t304,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t98,t294]) ).
cnf(t317,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t304]) ).
cnf(t65291,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t317,t2480]) ).
cnf(t2487,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t65291]) ).
cnf(t2509,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t2487]) ).
cnf(t2510,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t2509,t98]) ).
cnf(t3800,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t2510]) ).
cnf(t3803,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t3800,t2509]) ).
cnf(t4050,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t3803]) ).
cnf(t4056,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t2509,t4050]) ).
cnf(t4418,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t4056]) ).
cnf(t65451,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t2291,t4418]) ).
cnf(t4464,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t65451]) ).
cnf(t26666,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t4464]) ).
cnf(t26891,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t9540,t26666]) ).
cnf(t27919,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t26891]) ).
cnf(t27963,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t27919,t120]) ).
cnf(t28653,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t27963]) ).
cnf(t28693,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t28653,t2509]) ).
cnf(t32929,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t28693]) ).
cnf(t17,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/sandbox/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)],[t17]) ).
cnf(t3802,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t3800,t2509]) ).
cnf(t4033,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t3802]) ).
cnf(t4037,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t2509,t4033]) ).
cnf(t4070,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t4037]) ).
cnf(t61,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t54,t59]) ).
cnf(t491,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t61]) ).
cnf(t505,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t491,t51]) ).
cnf(t325,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t59,t317]) ).
cnf(t341,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t325]) ).
cnf(t500,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t491,t341]) ).
cnf(t502,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t491,t294]) ).
cnf(t65051,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t502,t59]) ).
cnf(t521,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t65051]) ).
cnf(t522,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t521,t98]) ).
cnf(t546,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t522]) ).
cnf(t65055,plain,
top = join(X1,top),
inference(step,[status(thm)],[t500,t546]) ).
cnf(t556,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t65055]) ).
cnf(t557,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t556,t51]) ).
cnf(t563,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t557]) ).
cnf(t65087,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t505,t563]) ).
cnf(t669,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t65087]) ).
cnf(t3821,plain,
top = join(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t669,t3800]) ).
cnf(t3993,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t3821]) ).
cnf(t4072,plain,
meet(complement(X1),meet(X2,X1)) = complement(top),
inference(cp,[status(thm)],[t4070,t3993]) ).
cnf(t65420,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(step,[status(thm)],[t4072,t111]) ).
cnf(t4260,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t65420]) ).
cnf(t4421,plain,
meet(X1,complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t4418,t2631]) ).
cnf(t65453,plain,
meet(X1,join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t4421,t4033]) ).
cnf(t65454,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t65453,t2509]) ).
cnf(t4755,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t65454]) ).
cnf(t4763,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t4755,t2509]) ).
cnf(t4777,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t4763]) ).
cnf(t4802,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t4777,t51]) ).
cnf(t4898,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t4802]) ).
cnf(t4974,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t4260,t4898]) ).
cnf(t65475,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t4974,t120]) ).
cnf(t5246,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t65475]) ).
cnf(t64,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t62,t20]) ).
cnf(t5907,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t64]) ).
cnf(t5932,plain,
zero = meet(composition(converse(X1),complement(X1)),complement(complement(one))),
inference(cp,[status(thm)],[t5246,t5907]) ).
cnf(t65577,plain,
zero = meet(complement(complement(one)),composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t5932,t120]) ).
cnf(t65578,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t65577,t2509]) ).
cnf(t7248,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t65578]) ).
cnf(t7264,plain,
zero = meet(one,composition(converse(complement(X1)),X1)),
inference(cp,[status(thm)],[t7248,t2509]) ).
cnf(t7498,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t7264]) ).
cnf(t7506,plain,
composition(meet(one,composition(converse(complement(converse(X1))),converse(X1))),meet(X1,composition(converse(one),converse(complement(converse(X1)))))) = join(meet(composition(one,X1),converse(complement(converse(X1)))),composition(zero,meet(X1,composition(converse(one),converse(complement(converse(X1))))))),
inference(cp,[status(thm)],[t30,t7498]) ).
cnf(t65605,plain,
composition(zero,meet(X1,composition(converse(one),converse(complement(converse(X1)))))) = join(meet(composition(one,X1),converse(complement(converse(X1)))),composition(zero,meet(X1,composition(converse(one),converse(complement(converse(X1))))))),
inference(step,[status(thm)],[t7506,t7498]) ).
cnf(t12,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t63,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(cp,[status(thm)],[t62,t24]) ).
cnf(t5362,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t63]) ).
cnf(t5368,plain,
complement(top) = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(cp,[status(thm)],[t5362,t111]) ).
cnf(t65550,plain,
zero = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(step,[status(thm)],[t5368,t111]) ).
cnf(t65551,plain,
zero = composition(X1,complement(composition(converse(X1),top))),
inference(step,[status(thm)],[t65550,t2381]) ).
cnf(t6962,plain,
composition(X1,complement(composition(converse(X1),top))) = zero,
inference(orient,[status(thm)],[t65551]) ).
cnf(t9,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t89,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t91,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t89,t24]) ).
cnf(t346,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t91]) ).
cnf(t348,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t346,t59]) ).
cnf(t392,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t348]) ).
cnf(t572,plain,
top = converse(top),
inference(cp,[status(thm)],[t563,t392]) ).
cnf(t575,plain,
converse(top) = top,
inference(orient,[status(thm)],[t572]) ).
cnf(t6970,plain,
zero = composition(top,complement(composition(top,top))),
inference(cp,[status(thm)],[t6962,t575]) ).
cnf(t7003,plain,
composition(top,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t6970]) ).
cnf(t7005,plain,
composition(join(top,X1),complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(cp,[status(thm)],[t27,t7003]) ).
cnf(t65552,plain,
composition(top,complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t7005,t563]) ).
cnf(t65553,plain,
zero = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t65552,t7003]) ).
cnf(t65554,plain,
zero = composition(X1,complement(composition(top,top))),
inference(step,[status(thm)],[t65553,t2381]) ).
cnf(t7016,plain,
composition(X1,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t65554]) ).
cnf(t10,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t7018,plain,
zero = composition(X1,composition(X2,complement(composition(top,top)))),
inference(cp,[status(thm)],[t7016,t25]) ).
cnf(t65555,plain,
zero = composition(X1,zero),
inference(step,[status(thm)],[t7018,t7016]) ).
cnf(t7032,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t65555]) ).
cnf(t7037,plain,
composition(converse(zero),X1) = converse(zero),
inference(cp,[status(thm)],[t210,t7032]) ).
cnf(t65070,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t392,t575]) ).
cnf(t578,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t65070]) ).
cnf(t2390,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t2381,t578]) ).
cnf(t2529,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t2390]) ).
cnf(t2530,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t24,t2529]) ).
cnf(t65305,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t2530,t575]) ).
cnf(t2551,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t65305]) ).
cnf(t2552,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t2509,t2551]) ).
cnf(t65306,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t2552,t111]) ).
cnf(t2557,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t65306]) ).
cnf(t65562,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t7037,t2557]) ).
cnf(t65563,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t65562,t2557]) ).
cnf(t7041,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t65563]) ).
cnf(t65606,plain,
zero = join(meet(composition(one,X1),converse(complement(converse(X1)))),composition(zero,meet(X1,composition(converse(one),converse(complement(converse(X1))))))),
inference(step,[status(thm)],[t65605,t7041]) ).
cnf(t65607,plain,
zero = join(meet(X1,converse(complement(converse(X1)))),composition(zero,meet(X1,composition(converse(one),converse(complement(converse(X1))))))),
inference(step,[status(thm)],[t65606,t244]) ).
cnf(t65608,plain,
zero = join(meet(X1,converse(complement(converse(X1)))),zero),
inference(step,[status(thm)],[t65607,t7041]) ).
cnf(t2393,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t2381,t51]) ).
cnf(t2466,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t2393]) ).
cnf(t65609,plain,
zero = meet(X1,converse(complement(converse(X1)))),
inference(step,[status(thm)],[t65608,t2466]) ).
cnf(t7509,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t65609]) ).
cnf(t7517,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(cp,[status(thm)],[t7509,t24]) ).
cnf(t7522,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t7517]) ).
cnf(t33021,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t32929,t7522]) ).
cnf(t66031,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t33021,t51]) ).
cnf(t66032,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t66031,t2466]) ).
cnf(t37137,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t66032]) ).
cnf(t37142,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t37137,t2509]) ).
cnf(t4430,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t4418,t578]) ).
cnf(t65840,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t4430,t111]) ).
cnf(t26651,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t65840]) ).
cnf(t28685,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t28653,t26651]) ).
cnf(t65903,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t28685,t2509]) ).
cnf(t65904,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t65903,t2466]) ).
cnf(t30160,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t65904]) ).
cnf(t30174,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t30160,t24]) ).
cnf(t35513,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t30174]) ).
cnf(t66033,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t37142,t35513]) ).
cnf(t37179,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t66033]) ).
cnf(t37184,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t37179,t2509]) ).
cnf(t37248,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t37184]) ).
cnf(t37259,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t37248,t346]) ).
cnf(t38243,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t37259]) ).
cnf(t37274,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t3800,t37248]) ).
cnf(t38659,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t37274]) ).
cnf(t38696,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t38243,t38659]) ).
cnf(t66135,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t38696,t4418]) ).
cnf(t66136,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t66135,t37179]) ).
cnf(t66137,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t66136,t2509]) ).
cnf(t38713,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t66137]) ).
cnf(t38746,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(cp,[status(thm)],[t38713,t24]) ).
cnf(t38931,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(orient,[status(thm)],[t38746]) ).
cnf(t248,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(converse(one),X1))) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(converse(one),X1)))),
inference(cp,[status(thm)],[t30,t244]) ).
cnf(t66422,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(one,X1))) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(converse(one),X1)))),
inference(step,[status(thm)],[t248,t233]) ).
cnf(t66423,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(converse(one),X1)))),
inference(step,[status(thm)],[t66422,t244]) ).
cnf(t66424,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,composition(one,X1)))),
inference(step,[status(thm)],[t66423,t233]) ).
cnf(t66425,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = join(meet(X2,X1),composition(meet(one,composition(X1,converse(X2))),meet(X2,X1))),
inference(step,[status(thm)],[t66424,t244]) ).
cnf(t246,plain,
composition(join(X1,one),X2) = join(composition(X1,X2),X2),
inference(cp,[status(thm)],[t27,t244]) ).
cnf(t66392,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(step,[status(thm)],[t246,t51]) ).
cnf(t58140,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t66392]) ).
cnf(t66426,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = composition(join(meet(one,composition(X1,converse(X2))),one),meet(X2,X1)),
inference(step,[status(thm)],[t66425,t58140]) ).
cnf(t66427,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = composition(join(one,meet(one,composition(X1,converse(X2)))),meet(X2,X1)),
inference(step,[status(thm)],[t66426,t51]) ).
cnf(t66428,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = composition(one,meet(X2,X1)),
inference(step,[status(thm)],[t66427,t2631]) ).
cnf(t66429,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = meet(X2,X1),
inference(step,[status(thm)],[t66428,t244]) ).
cnf(t61150,plain,
composition(meet(one,composition(X1,converse(X2))),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t66429]) ).
cnf(t47,plain,
composition(join(sk1,X1),sk2) = join(sFlat1,composition(X1,sk2)),
inference(cp,[status(thm)],[t27,t46]) ).
cnf(t411,plain,
composition(join(sk1,X1),sk2) = join(sFlat1,composition(X1,sk2)),
inference(orient,[status(thm)],[t47]) ).
cnf(t2,axiom,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t94,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t413,plain,
join(sFlat1,composition(one,sk2)) = composition(one,sk2),
inference(cp,[status(thm)],[t411,t94]) ).
cnf(t65039,plain,
join(sFlat1,sk2) = composition(one,sk2),
inference(step,[status(thm)],[t413,t244]) ).
cnf(t65040,plain,
join(sFlat1,sk2) = sk2,
inference(step,[status(thm)],[t65039,t244]) ).
cnf(t425,plain,
join(sFlat1,sk2) = sk2,
inference(orient,[status(thm)],[t65040]) ).
cnf(t427,plain,
join(sFlat1,join(sk2,X1)) = join(sk2,X1),
inference(cp,[status(thm)],[t54,t425]) ).
cnf(t431,plain,
join(sFlat1,join(sk2,X1)) = join(sk2,X1),
inference(orient,[status(thm)],[t427]) ).
cnf(t3,axiom,
join(sk2,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t96,plain,
join(sk2,one) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t97,plain,
join(sk2,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t54,t96]) ).
cnf(t144,plain,
join(sk2,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t97]) ).
cnf(t434,plain,
join(sk2,join(one,X1)) = join(sFlat1,join(one,X1)),
inference(cp,[status(thm)],[t431,t144]) ).
cnf(t65048,plain,
join(one,X1) = join(sFlat1,join(one,X1)),
inference(step,[status(thm)],[t434,t144]) ).
cnf(t455,plain,
join(sFlat1,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t65048]) ).
cnf(t456,plain,
join(one,X1) = join(sFlat1,join(X1,one)),
inference(cp,[status(thm)],[t455,t51]) ).
cnf(t471,plain,
join(sFlat1,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t456]) ).
cnf(t492,plain,
join(top,one) = join(one,complement(sFlat1)),
inference(cp,[status(thm)],[t491,t471]) ).
cnf(t531,plain,
join(one,complement(sFlat1)) = join(top,one),
inference(orient,[status(thm)],[t492]) ).
cnf(t65062,plain,
join(one,complement(sFlat1)) = top,
inference(step,[status(thm)],[t531,t563]) ).
cnf(t566,plain,
join(one,complement(sFlat1)) = top,
inference(orient,[status(thm)],[t65062]) ).
cnf(t4102,plain,
meet(complement(one),sFlat1) = complement(top),
inference(cp,[status(thm)],[t4070,t566]) ).
cnf(t65380,plain,
meet(sFlat1,complement(one)) = complement(top),
inference(step,[status(thm)],[t4102,t120]) ).
cnf(t65381,plain,
meet(sFlat1,complement(one)) = zero,
inference(step,[status(thm)],[t65380,t111]) ).
cnf(t4200,plain,
meet(sFlat1,complement(one)) = zero,
inference(orient,[status(thm)],[t65381]) ).
cnf(t4202,plain,
sFlat1 = join(zero,complement(join(complement(sFlat1),complement(one)))),
inference(cp,[status(thm)],[t2291,t4200]) ).
cnf(t65382,plain,
sFlat1 = complement(join(complement(sFlat1),complement(one))),
inference(step,[status(thm)],[t4202,t2381]) ).
cnf(t65383,plain,
sFlat1 = meet(sFlat1,one),
inference(step,[status(thm)],[t65382,t98]) ).
cnf(t4203,plain,
meet(sFlat1,one) = sFlat1,
inference(orient,[status(thm)],[t65383]) ).
cnf(t61583,plain,
meet(sFlat1,one) = composition(meet(one,composition(one,converse(sFlat1))),sFlat1),
inference(cp,[status(thm)],[t61150,t4203]) ).
cnf(t66502,plain,
sFlat1 = composition(meet(one,composition(one,converse(sFlat1))),sFlat1),
inference(step,[status(thm)],[t61583,t4203]) ).
cnf(t66503,plain,
sFlat1 = composition(meet(one,converse(sFlat1)),sFlat1),
inference(step,[status(thm)],[t66502,t244]) ).
cnf(t235,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t89,t233]) ).
cnf(t65022,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t235,t51]) ).
cnf(t261,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t65022]) ).
cnf(t433,plain,
join(sk2,one) = join(sFlat1,one),
inference(cp,[status(thm)],[t431,t96]) ).
cnf(t65043,plain,
one = join(sFlat1,one),
inference(step,[status(thm)],[t433,t96]) ).
cnf(t438,plain,
join(sFlat1,one) = one,
inference(orient,[status(thm)],[t65043]) ).
cnf(t439,plain,
join(one,converse(sFlat1)) = converse(one),
inference(cp,[status(thm)],[t261,t438]) ).
cnf(t65044,plain,
join(one,converse(sFlat1)) = one,
inference(step,[status(thm)],[t439,t233]) ).
cnf(t443,plain,
join(one,converse(sFlat1)) = one,
inference(orient,[status(thm)],[t65044]) ).
cnf(t445,plain,
join(one,join(converse(sFlat1),X1)) = join(one,X1),
inference(cp,[status(thm)],[t54,t443]) ).
cnf(t658,plain,
join(one,join(converse(sFlat1),X1)) = join(one,X1),
inference(orient,[status(thm)],[t445]) ).
cnf(t661,plain,
join(one,complement(converse(sFlat1))) = join(one,top),
inference(cp,[status(thm)],[t658,t59]) ).
cnf(t65085,plain,
join(one,complement(converse(sFlat1))) = top,
inference(step,[status(thm)],[t661,t556]) ).
cnf(t664,plain,
join(one,complement(converse(sFlat1))) = top,
inference(orient,[status(thm)],[t65085]) ).
cnf(t4098,plain,
meet(complement(one),converse(sFlat1)) = complement(top),
inference(cp,[status(thm)],[t4070,t664]) ).
cnf(t65405,plain,
meet(converse(sFlat1),complement(one)) = complement(top),
inference(step,[status(thm)],[t4098,t120]) ).
cnf(t65406,plain,
meet(converse(sFlat1),complement(one)) = zero,
inference(step,[status(thm)],[t65405,t111]) ).
cnf(t4242,plain,
meet(converse(sFlat1),complement(one)) = zero,
inference(orient,[status(thm)],[t65406]) ).
cnf(t4244,plain,
converse(sFlat1) = join(zero,complement(join(complement(converse(sFlat1)),complement(one)))),
inference(cp,[status(thm)],[t2291,t4242]) ).
cnf(t65407,plain,
converse(sFlat1) = complement(join(complement(converse(sFlat1)),complement(one))),
inference(step,[status(thm)],[t4244,t2381]) ).
cnf(t65408,plain,
converse(sFlat1) = meet(converse(sFlat1),one),
inference(step,[status(thm)],[t65407,t98]) ).
cnf(t65409,plain,
converse(sFlat1) = meet(one,converse(sFlat1)),
inference(step,[status(thm)],[t65408,t120]) ).
cnf(t4245,plain,
meet(one,converse(sFlat1)) = converse(sFlat1),
inference(orient,[status(thm)],[t65409]) ).
cnf(t66504,plain,
sFlat1 = composition(converse(sFlat1),sFlat1),
inference(step,[status(thm)],[t66503,t4245]) ).
cnf(t61959,plain,
composition(converse(sFlat1),sFlat1) = sFlat1,
inference(orient,[status(thm)],[t66504]) ).
cnf(t61977,plain,
composition(converse(sFlat1),sFlat1) = converse(sFlat1),
inference(cp,[status(thm)],[t210,t61959]) ).
cnf(t66505,plain,
sFlat1 = converse(sFlat1),
inference(step,[status(thm)],[t61977,t61959]) ).
cnf(t61990,plain,
converse(sFlat1) = sFlat1,
inference(orient,[status(thm)],[t66505]) ).
cnf(t61991,plain,
converse(meet(sFlat1,X1)) = meet(sFlat1,converse(X1)),
inference(cp,[status(thm)],[t38931,t61990]) ).
cnf(t63278,plain,
converse(meet(sFlat1,X1)) = meet(sFlat1,converse(X1)),
inference(orient,[status(thm)],[t61991]) ).
cnf(t48,plain,
composition(join(X1,sk1),sk2) = join(composition(X1,sk2),sFlat1),
inference(cp,[status(thm)],[t27,t46]) ).
cnf(t65049,plain,
composition(join(X1,sk1),sk2) = join(sFlat1,composition(X1,sk2)),
inference(step,[status(thm)],[t48,t51]) ).
cnf(t479,plain,
composition(join(X1,sk1),sk2) = join(sFlat1,composition(X1,sk2)),
inference(orient,[status(thm)],[t65049]) ).
cnf(t2669,plain,
sk1 = join(sk1,sFlat0),
inference(cp,[status(thm)],[t2667,t129]) ).
cnf(t65315,plain,
sk1 = join(sFlat0,sk1),
inference(step,[status(thm)],[t2669,t51]) ).
cnf(t2685,plain,
join(sFlat0,sk1) = sk1,
inference(orient,[status(thm)],[t65315]) ).
cnf(t2687,plain,
join(sFlat1,composition(sFlat0,sk2)) = composition(sk1,sk2),
inference(cp,[status(thm)],[t479,t2685]) ).
cnf(t65316,plain,
join(sFlat1,composition(sFlat0,sk2)) = sFlat1,
inference(step,[status(thm)],[t2687,t46]) ).
cnf(t2689,plain,
join(sFlat1,composition(sFlat0,sk2)) = sFlat1,
inference(orient,[status(thm)],[t65316]) ).
cnf(t4908,plain,
composition(sFlat0,sk2) = meet(composition(sFlat0,sk2),sFlat1),
inference(cp,[status(thm)],[t4898,t2689]) ).
cnf(t65457,plain,
composition(sFlat0,sk2) = meet(sFlat1,composition(sFlat0,sk2)),
inference(step,[status(thm)],[t4908,t120]) ).
cnf(t5080,plain,
meet(sFlat1,composition(sFlat0,sk2)) = composition(sFlat0,sk2),
inference(orient,[status(thm)],[t65457]) ).
cnf(t63313,plain,
meet(sFlat1,converse(composition(sFlat0,sk2))) = converse(composition(sFlat0,sk2)),
inference(cp,[status(thm)],[t63278,t5080]) ).
cnf(t234,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t89,t233]) ).
cnf(t250,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t234]) ).
cnf(t262,plain,
join(one,converse(sk2)) = converse(one),
inference(cp,[status(thm)],[t261,t96]) ).
cnf(t65023,plain,
join(one,converse(sk2)) = one,
inference(step,[status(thm)],[t262,t233]) ).
cnf(t288,plain,
join(one,converse(sk2)) = one,
inference(orient,[status(thm)],[t65023]) ).
cnf(t290,plain,
join(one,join(converse(sk2),X1)) = join(one,X1),
inference(cp,[status(thm)],[t54,t288]) ).
cnf(t634,plain,
join(one,join(converse(sk2),X1)) = join(one,X1),
inference(orient,[status(thm)],[t290]) ).
cnf(t635,plain,
join(one,converse(X1)) = join(one,converse(join(sk2,X1))),
inference(cp,[status(thm)],[t634,t89]) ).
cnf(t816,plain,
join(one,converse(join(sk2,X1))) = join(one,converse(X1)),
inference(orient,[status(thm)],[t635]) ).
cnf(t818,plain,
join(one,converse(converse(join(sk2,X1)))) = converse(join(one,converse(X1))),
inference(cp,[status(thm)],[t250,t816]) ).
cnf(t65105,plain,
join(one,join(sk2,X1)) = converse(join(one,converse(X1))),
inference(step,[status(thm)],[t818,t24]) ).
cnf(t65106,plain,
join(one,join(sk2,X1)) = join(one,converse(converse(X1))),
inference(step,[status(thm)],[t65105,t250]) ).
cnf(t65107,plain,
join(one,join(sk2,X1)) = join(one,X1),
inference(step,[status(thm)],[t65106,t24]) ).
cnf(t821,plain,
join(one,join(sk2,X1)) = join(one,X1),
inference(orient,[status(thm)],[t65107]) ).
cnf(t2633,plain,
sk2 = join(sk2,sFlat0),
inference(cp,[status(thm)],[t2631,t129]) ).
cnf(t65310,plain,
sk2 = join(sFlat0,sk2),
inference(step,[status(thm)],[t2633,t51]) ).
cnf(t2650,plain,
join(sFlat0,sk2) = sk2,
inference(orient,[status(thm)],[t65310]) ).
cnf(t2653,plain,
join(sFlat0,join(sk2,X1)) = join(sk2,X1),
inference(cp,[status(thm)],[t54,t2650]) ).
cnf(t2894,plain,
join(sFlat0,join(sk2,X1)) = join(sk2,X1),
inference(orient,[status(thm)],[t2653]) ).
cnf(t2899,plain,
join(sk2,complement(sFlat0)) = top,
inference(cp,[status(thm)],[t2894,t669]) ).
cnf(t2906,plain,
join(sk2,complement(sFlat0)) = top,
inference(orient,[status(thm)],[t2899]) ).
cnf(t2908,plain,
join(one,complement(sFlat0)) = join(one,top),
inference(cp,[status(thm)],[t821,t2906]) ).
cnf(t65325,plain,
join(one,complement(sFlat0)) = top,
inference(step,[status(thm)],[t2908,t556]) ).
cnf(t2913,plain,
join(one,complement(sFlat0)) = top,
inference(orient,[status(thm)],[t65325]) ).
cnf(t4086,plain,
meet(complement(one),sFlat0) = complement(top),
inference(cp,[status(thm)],[t4070,t2913]) ).
cnf(t65372,plain,
meet(sFlat0,complement(one)) = complement(top),
inference(step,[status(thm)],[t4086,t120]) ).
cnf(t65373,plain,
meet(sFlat0,complement(one)) = zero,
inference(step,[status(thm)],[t65372,t111]) ).
cnf(t4187,plain,
meet(sFlat0,complement(one)) = zero,
inference(orient,[status(thm)],[t65373]) ).
cnf(t4189,plain,
sFlat0 = join(zero,complement(join(complement(sFlat0),complement(one)))),
inference(cp,[status(thm)],[t2291,t4187]) ).
cnf(t65374,plain,
sFlat0 = complement(join(complement(sFlat0),complement(one))),
inference(step,[status(thm)],[t4189,t2381]) ).
cnf(t65375,plain,
sFlat0 = meet(sFlat0,one),
inference(step,[status(thm)],[t65374,t98]) ).
cnf(t4190,plain,
meet(sFlat0,one) = sFlat0,
inference(orient,[status(thm)],[t65375]) ).
cnf(t61551,plain,
meet(sFlat0,one) = composition(meet(one,composition(one,converse(sFlat0))),sFlat0),
inference(cp,[status(thm)],[t61150,t4190]) ).
cnf(t66463,plain,
sFlat0 = composition(meet(one,composition(one,converse(sFlat0))),sFlat0),
inference(step,[status(thm)],[t61551,t4190]) ).
cnf(t66464,plain,
sFlat0 = composition(meet(one,converse(sFlat0)),sFlat0),
inference(step,[status(thm)],[t66463,t244]) ).
cnf(t681,plain,
join(X1,converse(join(X2,complement(converse(X1))))) = converse(top),
inference(cp,[status(thm)],[t346,t669]) ).
cnf(t65125,plain,
join(X1,converse(join(X2,complement(converse(X1))))) = top,
inference(step,[status(thm)],[t681,t575]) ).
cnf(t1094,plain,
join(X1,converse(join(X2,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t65125]) ).
cnf(t1096,plain,
top = join(X1,join(X2,converse(complement(converse(X1))))),
inference(cp,[status(thm)],[t1094,t346]) ).
cnf(t1554,plain,
join(X1,join(X2,converse(complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t1096]) ).
cnf(t2896,plain,
join(sk2,converse(complement(converse(sFlat0)))) = top,
inference(cp,[status(thm)],[t2894,t1554]) ).
cnf(t3699,plain,
join(sk2,converse(complement(converse(sFlat0)))) = top,
inference(orient,[status(thm)],[t2896]) ).
cnf(t3702,plain,
join(one,converse(converse(complement(converse(sFlat0))))) = join(one,converse(top)),
inference(cp,[status(thm)],[t816,t3699]) ).
cnf(t65366,plain,
join(one,complement(converse(sFlat0))) = join(one,converse(top)),
inference(step,[status(thm)],[t3702,t24]) ).
cnf(t65367,plain,
join(one,complement(converse(sFlat0))) = join(one,top),
inference(step,[status(thm)],[t65366,t575]) ).
cnf(t65368,plain,
join(one,complement(converse(sFlat0))) = top,
inference(step,[status(thm)],[t65367,t556]) ).
cnf(t3708,plain,
join(one,complement(converse(sFlat0))) = top,
inference(orient,[status(thm)],[t65368]) ).
cnf(t4085,plain,
meet(complement(one),converse(sFlat0)) = complement(top),
inference(cp,[status(thm)],[t4070,t3708]) ).
cnf(t65400,plain,
meet(converse(sFlat0),complement(one)) = complement(top),
inference(step,[status(thm)],[t4085,t120]) ).
cnf(t65401,plain,
meet(converse(sFlat0),complement(one)) = zero,
inference(step,[status(thm)],[t65400,t111]) ).
cnf(t4236,plain,
meet(converse(sFlat0),complement(one)) = zero,
inference(orient,[status(thm)],[t65401]) ).
cnf(t4238,plain,
converse(sFlat0) = join(zero,complement(join(complement(converse(sFlat0)),complement(one)))),
inference(cp,[status(thm)],[t2291,t4236]) ).
cnf(t65402,plain,
converse(sFlat0) = complement(join(complement(converse(sFlat0)),complement(one))),
inference(step,[status(thm)],[t4238,t2381]) ).
cnf(t65403,plain,
converse(sFlat0) = meet(converse(sFlat0),one),
inference(step,[status(thm)],[t65402,t98]) ).
cnf(t65404,plain,
converse(sFlat0) = meet(one,converse(sFlat0)),
inference(step,[status(thm)],[t65403,t120]) ).
cnf(t4239,plain,
meet(one,converse(sFlat0)) = converse(sFlat0),
inference(orient,[status(thm)],[t65404]) ).
cnf(t66465,plain,
sFlat0 = composition(converse(sFlat0),sFlat0),
inference(step,[status(thm)],[t66464,t4239]) ).
cnf(t61782,plain,
composition(converse(sFlat0),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t66465]) ).
cnf(t61800,plain,
composition(converse(sFlat0),sFlat0) = converse(sFlat0),
inference(cp,[status(thm)],[t210,t61782]) ).
cnf(t66466,plain,
sFlat0 = converse(sFlat0),
inference(step,[status(thm)],[t61800,t61782]) ).
cnf(t61813,plain,
converse(sFlat0) = sFlat0,
inference(orient,[status(thm)],[t66466]) ).
cnf(t61820,plain,
converse(composition(sFlat0,X1)) = composition(converse(X1),sFlat0),
inference(cp,[status(thm)],[t37,t61813]) ).
cnf(t63233,plain,
converse(composition(sFlat0,X1)) = composition(converse(X1),sFlat0),
inference(orient,[status(thm)],[t61820]) ).
cnf(t66624,plain,
meet(sFlat1,composition(converse(sk2),sFlat0)) = converse(composition(sFlat0,sk2)),
inference(step,[status(thm)],[t63313,t63233]) ).
cnf(t146,plain,
join(one,X1) = join(sk2,join(X1,one)),
inference(cp,[status(thm)],[t144,t51]) ).
cnf(t179,plain,
join(sk2,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t146]) ).
cnf(t497,plain,
join(top,one) = join(one,complement(sk2)),
inference(cp,[status(thm)],[t491,t179]) ).
cnf(t536,plain,
join(one,complement(sk2)) = join(top,one),
inference(orient,[status(thm)],[t497]) ).
cnf(t65064,plain,
join(one,complement(sk2)) = top,
inference(step,[status(thm)],[t536,t563]) ).
cnf(t568,plain,
join(one,complement(sk2)) = top,
inference(orient,[status(thm)],[t65064]) ).
cnf(t4103,plain,
meet(complement(one),sk2) = complement(top),
inference(cp,[status(thm)],[t4070,t568]) ).
cnf(t65384,plain,
meet(sk2,complement(one)) = complement(top),
inference(step,[status(thm)],[t4103,t120]) ).
cnf(t65385,plain,
meet(sk2,complement(one)) = zero,
inference(step,[status(thm)],[t65384,t111]) ).
cnf(t4207,plain,
meet(sk2,complement(one)) = zero,
inference(orient,[status(thm)],[t65385]) ).
cnf(t4209,plain,
sk2 = join(zero,complement(join(complement(sk2),complement(one)))),
inference(cp,[status(thm)],[t2291,t4207]) ).
cnf(t65386,plain,
sk2 = complement(join(complement(sk2),complement(one))),
inference(step,[status(thm)],[t4209,t2381]) ).
cnf(t65387,plain,
sk2 = meet(sk2,one),
inference(step,[status(thm)],[t65386,t98]) ).
cnf(t4210,plain,
meet(sk2,one) = sk2,
inference(orient,[status(thm)],[t65387]) ).
cnf(t61605,plain,
meet(sk2,one) = composition(meet(one,composition(one,converse(sk2))),sk2),
inference(cp,[status(thm)],[t61150,t4210]) ).
cnf(t66544,plain,
sk2 = composition(meet(one,composition(one,converse(sk2))),sk2),
inference(step,[status(thm)],[t61605,t4210]) ).
cnf(t66545,plain,
sk2 = composition(meet(one,converse(sk2)),sk2),
inference(step,[status(thm)],[t66544,t244]) ).
cnf(t637,plain,
join(one,complement(converse(sk2))) = join(one,top),
inference(cp,[status(thm)],[t634,t59]) ).
cnf(t65081,plain,
join(one,complement(converse(sk2))) = top,
inference(step,[status(thm)],[t637,t556]) ).
cnf(t640,plain,
join(one,complement(converse(sk2))) = top,
inference(orient,[status(thm)],[t65081]) ).
cnf(t4099,plain,
meet(complement(one),converse(sk2)) = complement(top),
inference(cp,[status(thm)],[t4070,t640]) ).
cnf(t65410,plain,
meet(converse(sk2),complement(one)) = complement(top),
inference(step,[status(thm)],[t4099,t120]) ).
cnf(t65411,plain,
meet(converse(sk2),complement(one)) = zero,
inference(step,[status(thm)],[t65410,t111]) ).
cnf(t4248,plain,
meet(converse(sk2),complement(one)) = zero,
inference(orient,[status(thm)],[t65411]) ).
cnf(t4250,plain,
converse(sk2) = join(zero,complement(join(complement(converse(sk2)),complement(one)))),
inference(cp,[status(thm)],[t2291,t4248]) ).
cnf(t65412,plain,
converse(sk2) = complement(join(complement(converse(sk2)),complement(one))),
inference(step,[status(thm)],[t4250,t2381]) ).
cnf(t65413,plain,
converse(sk2) = meet(converse(sk2),one),
inference(step,[status(thm)],[t65412,t98]) ).
cnf(t65414,plain,
converse(sk2) = meet(one,converse(sk2)),
inference(step,[status(thm)],[t65413,t120]) ).
cnf(t4251,plain,
meet(one,converse(sk2)) = converse(sk2),
inference(orient,[status(thm)],[t65414]) ).
cnf(t66546,plain,
sk2 = composition(converse(sk2),sk2),
inference(step,[status(thm)],[t66545,t4251]) ).
cnf(t62138,plain,
composition(converse(sk2),sk2) = sk2,
inference(orient,[status(thm)],[t66546]) ).
cnf(t62155,plain,
composition(converse(sk2),sk2) = converse(sk2),
inference(cp,[status(thm)],[t210,t62138]) ).
cnf(t66547,plain,
sk2 = converse(sk2),
inference(step,[status(thm)],[t62155,t62138]) ).
cnf(t62168,plain,
converse(sk2) = sk2,
inference(orient,[status(thm)],[t66547]) ).
cnf(t66625,plain,
meet(sFlat1,composition(sk2,sFlat0)) = converse(composition(sFlat0,sk2)),
inference(step,[status(thm)],[t66624,t62168]) ).
cnf(t66626,plain,
meet(sFlat1,composition(sk2,sFlat0)) = composition(converse(sk2),sFlat0),
inference(step,[status(thm)],[t66625,t63233]) ).
cnf(t66627,plain,
meet(sFlat1,composition(sk2,sFlat0)) = composition(sk2,sFlat0),
inference(step,[status(thm)],[t66626,t62168]) ).
cnf(t64764,plain,
meet(sFlat1,composition(sk2,sFlat0)) = composition(sk2,sFlat0),
inference(orient,[status(thm)],[t66627]) ).
cnf(t249,plain,
composition(meet(X1,composition(one,converse(X2))),meet(X2,composition(converse(X1),one))) = join(meet(composition(X1,X2),one),composition(meet(X1,converse(X2)),meet(X2,composition(converse(X1),one)))),
inference(cp,[status(thm)],[t30,t244]) ).
cnf(t66616,plain,
composition(meet(X1,converse(X2)),meet(X2,composition(converse(X1),one))) = join(meet(composition(X1,X2),one),composition(meet(X1,converse(X2)),meet(X2,composition(converse(X1),one)))),
inference(step,[status(thm)],[t249,t244]) ).
cnf(t66617,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(composition(X1,X2),one),composition(meet(X1,converse(X2)),meet(X2,composition(converse(X1),one)))),
inference(step,[status(thm)],[t66616,t20]) ).
cnf(t66618,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,composition(converse(X1),one)))),
inference(step,[status(thm)],[t66617,t120]) ).
cnf(t66619,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t66618,t20]) ).
cnf(t64434,plain,
join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,converse(X1)))) = composition(meet(X1,converse(X2)),meet(X2,converse(X1))),
inference(orient,[status(thm)],[t66619]) ).
cnf(t2637,plain,
join(one,meet(sk2,X1)) = join(one,sk2),
inference(cp,[status(thm)],[t821,t2631]) ).
cnf(t65323,plain,
join(one,meet(sk2,X1)) = join(sk2,one),
inference(step,[status(thm)],[t2637,t51]) ).
cnf(t65324,plain,
join(one,meet(sk2,X1)) = one,
inference(step,[status(thm)],[t65323,t96]) ).
cnf(t2880,plain,
join(one,meet(sk2,X1)) = one,
inference(orient,[status(thm)],[t65324]) ).
cnf(t4931,plain,
meet(sk2,X1) = meet(meet(sk2,X1),one),
inference(cp,[status(thm)],[t4898,t2880]) ).
cnf(t65461,plain,
meet(sk2,X1) = meet(one,meet(sk2,X1)),
inference(step,[status(thm)],[t4931,t120]) ).
cnf(t5108,plain,
meet(one,meet(sk2,X1)) = meet(sk2,X1),
inference(orient,[status(thm)],[t65461]) ).
cnf(t245,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t27,t244]) ).
cnf(t54730,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t245]) ).
cnf(t638,plain,
join(one,X1) = join(one,join(X1,converse(sk2))),
inference(cp,[status(thm)],[t634,t51]) ).
cnf(t687,plain,
join(one,join(X1,converse(sk2))) = join(one,X1),
inference(orient,[status(thm)],[t638]) ).
cnf(t688,plain,
join(one,converse(X1)) = join(one,converse(join(X1,sk2))),
inference(cp,[status(thm)],[t687,t89]) ).
cnf(t899,plain,
join(one,converse(join(X1,sk2))) = join(one,converse(X1)),
inference(orient,[status(thm)],[t688]) ).
cnf(t2654,plain,
join(one,converse(sFlat0)) = join(one,converse(sk2)),
inference(cp,[status(thm)],[t899,t2650]) ).
cnf(t65314,plain,
join(one,converse(sFlat0)) = one,
inference(step,[status(thm)],[t2654,t288]) ).
cnf(t2662,plain,
join(one,converse(sFlat0)) = one,
inference(orient,[status(thm)],[t65314]) ).
cnf(t54920,plain,
join(X1,composition(converse(sFlat0),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t54730,t2662]) ).
cnf(t66331,plain,
join(X1,composition(converse(sFlat0),X1)) = X1,
inference(step,[status(thm)],[t54920,t244]) ).
cnf(t55261,plain,
join(X1,composition(converse(sFlat0),X1)) = X1,
inference(orient,[status(thm)],[t66331]) ).
cnf(t55390,plain,
join(X1,converse(composition(converse(sFlat0),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t346,t55261]) ).
cnf(t66332,plain,
join(X1,composition(converse(converse(X1)),sFlat0)) = converse(converse(X1)),
inference(step,[status(thm)],[t55390,t210]) ).
cnf(t66333,plain,
join(X1,composition(X1,sFlat0)) = converse(converse(X1)),
inference(step,[status(thm)],[t66332,t24]) ).
cnf(t66334,plain,
join(X1,composition(X1,sFlat0)) = X1,
inference(step,[status(thm)],[t66333,t24]) ).
cnf(t55402,plain,
join(X1,composition(X1,sFlat0)) = X1,
inference(orient,[status(thm)],[t66334]) ).
cnf(t55469,plain,
composition(X1,sFlat0) = meet(composition(X1,sFlat0),X1),
inference(cp,[status(thm)],[t4898,t55402]) ).
cnf(t66338,plain,
composition(X1,sFlat0) = meet(X1,composition(X1,sFlat0)),
inference(step,[status(thm)],[t55469,t120]) ).
cnf(t55661,plain,
meet(X1,composition(X1,sFlat0)) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t66338]) ).
cnf(t55748,plain,
meet(sk2,composition(sk2,sFlat0)) = meet(one,composition(sk2,sFlat0)),
inference(cp,[status(thm)],[t5108,t55661]) ).
cnf(t66346,plain,
composition(sk2,sFlat0) = meet(one,composition(sk2,sFlat0)),
inference(step,[status(thm)],[t55748,t55661]) ).
cnf(t56831,plain,
meet(one,composition(sk2,sFlat0)) = composition(sk2,sFlat0),
inference(orient,[status(thm)],[t66346]) ).
cnf(t64435,plain,
composition(meet(sk2,converse(sFlat0)),meet(sFlat0,converse(sk2))) = join(composition(sk2,sFlat0),composition(meet(sk2,converse(sFlat0)),meet(sFlat0,converse(sk2)))),
inference(cp,[status(thm)],[t64434,t56831]) ).
cnf(t66629,plain,
composition(meet(sk2,sFlat0),meet(sFlat0,converse(sk2))) = join(composition(sk2,sFlat0),composition(meet(sk2,converse(sFlat0)),meet(sFlat0,converse(sk2)))),
inference(step,[status(thm)],[t64435,t61813]) ).
cnf(t66630,plain,
composition(meet(sk2,sFlat0),meet(sFlat0,sk2)) = join(composition(sk2,sFlat0),composition(meet(sk2,converse(sFlat0)),meet(sFlat0,converse(sk2)))),
inference(step,[status(thm)],[t66629,t62168]) ).
cnf(t4110,plain,
meet(complement(sk2),sFlat0) = complement(top),
inference(cp,[status(thm)],[t4070,t2906]) ).
cnf(t65392,plain,
meet(sFlat0,complement(sk2)) = complement(top),
inference(step,[status(thm)],[t4110,t120]) ).
cnf(t65393,plain,
meet(sFlat0,complement(sk2)) = zero,
inference(step,[status(thm)],[t65392,t111]) ).
cnf(t4222,plain,
meet(sFlat0,complement(sk2)) = zero,
inference(orient,[status(thm)],[t65393]) ).
cnf(t4224,plain,
sFlat0 = join(zero,complement(join(complement(sFlat0),complement(sk2)))),
inference(cp,[status(thm)],[t2291,t4222]) ).
cnf(t65394,plain,
sFlat0 = complement(join(complement(sFlat0),complement(sk2))),
inference(step,[status(thm)],[t4224,t2381]) ).
cnf(t65395,plain,
sFlat0 = meet(sFlat0,sk2),
inference(step,[status(thm)],[t65394,t98]) ).
cnf(t4225,plain,
meet(sFlat0,sk2) = sFlat0,
inference(orient,[status(thm)],[t65395]) ).
cnf(t66631,plain,
composition(meet(sk2,sFlat0),sFlat0) = join(composition(sk2,sFlat0),composition(meet(sk2,converse(sFlat0)),meet(sFlat0,converse(sk2)))),
inference(step,[status(thm)],[t66630,t4225]) ).
cnf(t66632,plain,
composition(meet(sk2,sFlat0),sFlat0) = join(composition(sk2,sFlat0),composition(meet(sk2,sFlat0),meet(sFlat0,converse(sk2)))),
inference(step,[status(thm)],[t66631,t61813]) ).
cnf(t66633,plain,
composition(meet(sk2,sFlat0),sFlat0) = join(composition(sk2,sFlat0),composition(meet(sk2,sFlat0),meet(sFlat0,sk2))),
inference(step,[status(thm)],[t66632,t62168]) ).
cnf(t66634,plain,
composition(meet(sk2,sFlat0),sFlat0) = join(composition(sk2,sFlat0),composition(meet(sk2,sFlat0),sFlat0)),
inference(step,[status(thm)],[t66633,t4225]) ).
cnf(t66635,plain,
composition(meet(sk2,sFlat0),sFlat0) = composition(join(sk2,meet(sk2,sFlat0)),sFlat0),
inference(step,[status(thm)],[t66634,t27]) ).
cnf(t2640,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t54,t2631]) ).
cnf(t8073,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t2640]) ).
cnf(t2903,plain,
join(sk2,X1) = join(sFlat0,join(X1,sk2)),
inference(cp,[status(thm)],[t2894,t51]) ).
cnf(t2962,plain,
join(sFlat0,join(X1,sk2)) = join(sk2,X1),
inference(orient,[status(thm)],[t2903]) ).
cnf(t8076,plain,
join(sFlat0,sk2) = join(sk2,meet(sFlat0,X1)),
inference(cp,[status(thm)],[t8073,t2962]) ).
cnf(t65633,plain,
sk2 = join(sk2,meet(sFlat0,X1)),
inference(step,[status(thm)],[t8076,t2650]) ).
cnf(t8201,plain,
join(sk2,meet(sFlat0,X1)) = sk2,
inference(orient,[status(thm)],[t65633]) ).
cnf(t4901,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t4898,t2667]) ).
cnf(t65456,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t4901,t120]) ).
cnf(t5046,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t65456]) ).
cnf(t8222,plain,
sk2 = join(sk2,meet(X1,sFlat0)),
inference(cp,[status(thm)],[t8201,t5046]) ).
cnf(t8276,plain,
join(sk2,meet(X1,sFlat0)) = sk2,
inference(orient,[status(thm)],[t8222]) ).
cnf(t66636,plain,
composition(meet(sk2,sFlat0),sFlat0) = composition(sk2,sFlat0),
inference(step,[status(thm)],[t66635,t8276]) ).
cnf(t66637,plain,
composition(meet(sFlat0,sk2),sFlat0) = composition(sk2,sFlat0),
inference(step,[status(thm)],[t66636,t120]) ).
cnf(t66638,plain,
composition(sFlat0,sFlat0) = composition(sk2,sFlat0),
inference(step,[status(thm)],[t66637,t4225]) ).
cnf(t66467,plain,
composition(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t61782,t61813]) ).
cnf(t61867,plain,
composition(sFlat0,sFlat0) = sFlat0,
inference(rw,[status(thm)],[t66467]) ).
cnf(t61882,plain,
composition(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t61867]) ).
cnf(t66639,plain,
sFlat0 = composition(sk2,sFlat0),
inference(step,[status(thm)],[t66638,t61882]) ).
cnf(t64873,plain,
composition(sk2,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t66639]) ).
cnf(t66640,plain,
meet(sFlat1,sFlat0) = composition(sk2,sFlat0),
inference(step,[status(thm)],[t64764,t64873]) ).
cnf(t66641,plain,
meet(sFlat1,sFlat0) = sFlat0,
inference(step,[status(thm)],[t66640,t64873]) ).
cnf(t64897,plain,
meet(sFlat1,sFlat0) = sFlat0,
inference(rw,[status(thm)],[t66641]) ).
cnf(t66694,plain,
meet(sFlat0,sFlat1) = sFlat0,
inference(step,[status(thm)],[t64897,t120]) ).
cnf(t58,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t54,t51]) ).
cnf(t65452,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t58,t54]) ).
cnf(t4465,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t65452]) ).
cnf(t4803,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t4777,t4465]) ).
cnf(t6160,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t4803]) ).
cnf(t241,plain,
composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2))) = join(meet(composition(X1,one),X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t30,t233]) ).
cnf(t66274,plain,
composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2))) = join(meet(composition(X1,one),X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t241,t233]) ).
cnf(t66275,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(composition(X1,one),X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t66274,t20]) ).
cnf(t66276,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t66275,t20]) ).
cnf(t66277,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t66276,t20]) ).
cnf(t51526,plain,
join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))) = composition(meet(X1,X2),meet(one,composition(converse(X1),X2))),
inference(orient,[status(thm)],[t66277]) ).
cnf(t263,plain,
join(one,converse(sk1)) = converse(one),
inference(cp,[status(thm)],[t261,t94]) ).
cnf(t65024,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t263,t233]) ).
cnf(t291,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t65024]) ).
cnf(t293,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(cp,[status(thm)],[t54,t291]) ).
cnf(t645,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(orient,[status(thm)],[t293]) ).
cnf(t648,plain,
join(one,complement(converse(sk1))) = join(one,top),
inference(cp,[status(thm)],[t645,t59]) ).
cnf(t65083,plain,
join(one,complement(converse(sk1))) = top,
inference(step,[status(thm)],[t648,t556]) ).
cnf(t651,plain,
join(one,complement(converse(sk1))) = top,
inference(orient,[status(thm)],[t65083]) ).
cnf(t4100,plain,
meet(complement(one),converse(sk1)) = complement(top),
inference(cp,[status(thm)],[t4070,t651]) ).
cnf(t65415,plain,
meet(converse(sk1),complement(one)) = complement(top),
inference(step,[status(thm)],[t4100,t120]) ).
cnf(t65416,plain,
meet(converse(sk1),complement(one)) = zero,
inference(step,[status(thm)],[t65415,t111]) ).
cnf(t4254,plain,
meet(converse(sk1),complement(one)) = zero,
inference(orient,[status(thm)],[t65416]) ).
cnf(t4256,plain,
converse(sk1) = join(zero,complement(join(complement(converse(sk1)),complement(one)))),
inference(cp,[status(thm)],[t2291,t4254]) ).
cnf(t65417,plain,
converse(sk1) = complement(join(complement(converse(sk1)),complement(one))),
inference(step,[status(thm)],[t4256,t2381]) ).
cnf(t65418,plain,
converse(sk1) = meet(converse(sk1),one),
inference(step,[status(thm)],[t65417,t98]) ).
cnf(t65419,plain,
converse(sk1) = meet(one,converse(sk1)),
inference(step,[status(thm)],[t65418,t120]) ).
cnf(t4257,plain,
meet(one,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t65419]) ).
cnf(t51804,plain,
composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1)))) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(cp,[status(thm)],[t51526,t4257]) ).
cnf(t66278,plain,
composition(converse(sk1),meet(one,composition(converse(one),converse(sk1)))) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t51804,t4257]) ).
cnf(t66279,plain,
composition(converse(sk1),meet(one,converse(composition(sk1,one)))) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t66278,t37]) ).
cnf(t66280,plain,
composition(converse(sk1),meet(one,converse(sk1))) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t66279,t20]) ).
cnf(t66281,plain,
composition(converse(sk1),converse(sk1)) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t66280,t4257]) ).
cnf(t66282,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(meet(one,converse(sk1)),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t66281,t37]) ).
cnf(t66283,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,composition(converse(one),converse(sk1))))),
inference(step,[status(thm)],[t66282,t4257]) ).
cnf(t66284,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,converse(composition(sk1,one))))),
inference(step,[status(thm)],[t66283,t37]) ).
cnf(t66285,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),meet(one,converse(sk1)))),
inference(step,[status(thm)],[t66284,t20]) ).
cnf(t66286,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),composition(converse(sk1),converse(sk1))),
inference(step,[status(thm)],[t66285,t4257]) ).
cnf(t66287,plain,
converse(composition(sk1,sk1)) = join(converse(sk1),converse(composition(sk1,sk1))),
inference(step,[status(thm)],[t66286,t37]) ).
cnf(t66288,plain,
converse(composition(sk1,sk1)) = converse(join(sk1,composition(sk1,sk1))),
inference(step,[status(thm)],[t66287,t89]) ).
cnf(t52375,plain,
converse(join(sk1,composition(sk1,sk1))) = converse(composition(sk1,sk1)),
inference(orient,[status(thm)],[t66288]) ).
cnf(t52376,plain,
join(sk1,composition(sk1,sk1)) = converse(converse(composition(sk1,sk1))),
inference(cp,[status(thm)],[t24,t52375]) ).
cnf(t66289,plain,
join(sk1,composition(sk1,sk1)) = composition(sk1,sk1),
inference(step,[status(thm)],[t52376,t24]) ).
cnf(t52429,plain,
join(sk1,composition(sk1,sk1)) = composition(sk1,sk1),
inference(orient,[status(thm)],[t66289]) ).
cnf(t52447,plain,
join(sFlat1,composition(composition(sk1,sk1),sk2)) = composition(composition(sk1,sk1),sk2),
inference(cp,[status(thm)],[t411,t52429]) ).
cnf(t66291,plain,
join(sFlat1,composition(sk1,composition(sk1,sk2))) = composition(composition(sk1,sk1),sk2),
inference(step,[status(thm)],[t52447,t25]) ).
cnf(t66292,plain,
join(sFlat1,composition(sk1,sFlat1)) = composition(composition(sk1,sk1),sk2),
inference(step,[status(thm)],[t66291,t46]) ).
cnf(t66293,plain,
join(sFlat1,composition(sk1,sFlat1)) = composition(sk1,composition(sk1,sk2)),
inference(step,[status(thm)],[t66292,t25]) ).
cnf(t66294,plain,
join(sFlat1,composition(sk1,sFlat1)) = composition(sk1,sFlat1),
inference(step,[status(thm)],[t66293,t46]) ).
cnf(t52586,plain,
join(sFlat1,composition(sk1,sFlat1)) = composition(sk1,sFlat1),
inference(orient,[status(thm)],[t66294]) ).
cnf(t52601,plain,
sFlat1 = meet(sFlat1,join(X1,composition(sk1,sFlat1))),
inference(cp,[status(thm)],[t6160,t52586]) ).
cnf(t53145,plain,
meet(sFlat1,join(X1,composition(sk1,sFlat1))) = sFlat1,
inference(orient,[status(thm)],[t52601]) ).
cnf(t54971,plain,
join(X1,composition(converse(sFlat1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t54730,t443]) ).
cnf(t66350,plain,
join(X1,composition(converse(sFlat1),X1)) = X1,
inference(step,[status(thm)],[t54971,t244]) ).
cnf(t56955,plain,
join(X1,composition(converse(sFlat1),X1)) = X1,
inference(orient,[status(thm)],[t66350]) ).
cnf(t57082,plain,
join(X1,converse(composition(converse(sFlat1),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t346,t56955]) ).
cnf(t66351,plain,
join(X1,composition(converse(converse(X1)),sFlat1)) = converse(converse(X1)),
inference(step,[status(thm)],[t57082,t210]) ).
cnf(t66352,plain,
join(X1,composition(X1,sFlat1)) = converse(converse(X1)),
inference(step,[status(thm)],[t66351,t24]) ).
cnf(t66353,plain,
join(X1,composition(X1,sFlat1)) = X1,
inference(step,[status(thm)],[t66352,t24]) ).
cnf(t57094,plain,
join(X1,composition(X1,sFlat1)) = X1,
inference(orient,[status(thm)],[t66353]) ).
cnf(t57165,plain,
sFlat1 = meet(sFlat1,sk1),
inference(cp,[status(thm)],[t53145,t57094]) ).
cnf(t4118,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t4070,t2509]) ).
cnf(t5472,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t4118]) ).
cnf(t27936,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t27919,t5472]) ).
cnf(t30891,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t27936]) ).
cnf(t31269,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t4418,t30891]) ).
cnf(t65909,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t31269,t2509]) ).
cnf(t65910,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t65909,t98]) ).
cnf(t31290,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t65910]) ).
cnf(t4491,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,X1),
inference(cp,[status(thm)],[t4465,t2667]) ).
cnf(t10590,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t4491]) ).
cnf(t28669,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t28653,t5472]) ).
cnf(t32340,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t28669]) ).
cnf(t26841,plain,
sk2 = join(sFlat0,meet(sk2,complement(sk1))),
inference(cp,[status(thm)],[t26666,t129]) ).
cnf(t26924,plain,
join(sFlat0,meet(sk2,complement(sk1))) = sk2,
inference(orient,[status(thm)],[t26841]) ).
cnf(t26936,plain,
join(sFlat0,complement(sk1)) = join(complement(sk1),sk2),
inference(cp,[status(thm)],[t10590,t26924]) ).
cnf(t65842,plain,
join(sFlat0,complement(sk1)) = join(sk2,complement(sk1)),
inference(step,[status(thm)],[t26936,t51]) ).
cnf(t26945,plain,
join(sk2,complement(sk1)) = join(sFlat0,complement(sk1)),
inference(orient,[status(thm)],[t65842]) ).
cnf(t26962,plain,
join(sk2,complement(sk1)) = join(sFlat1,join(sFlat0,complement(sk1))),
inference(cp,[status(thm)],[t431,t26945]) ).
cnf(t65907,plain,
join(sFlat0,complement(sk1)) = join(sFlat1,join(sFlat0,complement(sk1))),
inference(step,[status(thm)],[t26962,t26945]) ).
cnf(t65908,plain,
join(sFlat0,complement(sk1)) = join(sFlat0,join(sFlat1,complement(sk1))),
inference(step,[status(thm)],[t65907,t4465]) ).
cnf(t30645,plain,
join(sFlat0,join(sFlat1,complement(sk1))) = join(sFlat0,complement(sk1)),
inference(orient,[status(thm)],[t65908]) ).
cnf(t32387,plain,
join(sFlat0,complement(join(sFlat1,complement(sk1)))) = join(sFlat0,complement(join(sFlat0,complement(sk1)))),
inference(cp,[status(thm)],[t32340,t30645]) ).
cnf(t65920,plain,
join(sFlat0,meet(complement(sFlat1),sk1)) = join(sFlat0,complement(join(sFlat0,complement(sk1)))),
inference(step,[status(thm)],[t32387,t4070]) ).
cnf(t65921,plain,
join(sFlat0,meet(sk1,complement(sFlat1))) = join(sFlat0,complement(join(sFlat0,complement(sk1)))),
inference(step,[status(thm)],[t65920,t120]) ).
cnf(t65922,plain,
join(sFlat0,meet(sk1,complement(sFlat1))) = join(sFlat0,complement(complement(sk1))),
inference(step,[status(thm)],[t65921,t32340]) ).
cnf(t65923,plain,
join(sFlat0,meet(sk1,complement(sFlat1))) = join(sFlat0,sk1),
inference(step,[status(thm)],[t65922,t2509]) ).
cnf(t65924,plain,
join(sFlat0,meet(sk1,complement(sFlat1))) = sk1,
inference(step,[status(thm)],[t65923,t2685]) ).
cnf(t32776,plain,
join(sFlat0,meet(sk1,complement(sFlat1))) = sk1,
inference(orient,[status(thm)],[t65924]) ).
cnf(t32791,plain,
join(sFlat0,complement(sFlat1)) = join(complement(sFlat1),sk1),
inference(cp,[status(thm)],[t10590,t32776]) ).
cnf(t65925,plain,
join(sFlat0,complement(sFlat1)) = join(sk1,complement(sFlat1)),
inference(step,[status(thm)],[t32791,t51]) ).
cnf(t32798,plain,
join(sk1,complement(sFlat1)) = join(sFlat0,complement(sFlat1)),
inference(orient,[status(thm)],[t65925]) ).
cnf(t32810,plain,
meet(sFlat1,sk1) = meet(sFlat1,join(sFlat0,complement(sFlat1))),
inference(cp,[status(thm)],[t31290,t32798]) ).
cnf(t65926,plain,
meet(sFlat1,sk1) = meet(sFlat1,sFlat0),
inference(step,[status(thm)],[t32810,t31290]) ).
cnf(t65927,plain,
meet(sFlat1,sk1) = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t65926,t120]) ).
cnf(t32820,plain,
meet(sFlat1,sk1) = meet(sFlat0,sFlat1),
inference(orient,[status(thm)],[t65927]) ).
cnf(t66354,plain,
sFlat1 = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t57165,t32820]) ).
cnf(t57225,plain,
meet(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t66354]) ).
cnf(t66695,plain,
sFlat1 = sFlat0,
inference(step,[status(thm)],[t66694,t57225]) ).
cnf(t64956,plain,
sFlat1 = sFlat0,
inference(orient,[status(thm)],[t66695]) ).
cnf(t66696,plain,
composition(sk1,sk2) = sFlat0,
inference(step,[status(thm)],[t46,t64956]) ).
cnf(t64957,plain,
composition(sk1,sk2) = sFlat0,
inference(orient,[status(thm)],[t66696]) ).
cnf(goal_0,negated_conjecture,
meet(sk1,sk2) != composition(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(sk2,sk1) != composition(sk1,sk2),
inference(rw,[status(thm)],[goal_0,t120]) ).
cnf(g0_1,plain,
sFlat0 != composition(sk1,sk2),
inference(rw,[status(thm)],[g0_0,t129]) ).
cnf(g0_2,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_1,t64957]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL028-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 07:25:48 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 69.46/9.21 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 69.46/9.21 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------