%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL017-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/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:34:45 PM UTC 2026
% Result : Unsatisfiable 59.39s 7.95s
% Output : CNFRefutation 59.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 23
% Syntax : Number of clauses : 457 ( 457 unt; 0 nHn; 214 RR)
% Number of literals : 457 ( 456 equ; 15 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; 15 con; 0-2 aty)
% Number of variables : 354 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t85,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t17,axiom,
sFlat4 = composition(sk1,sk3),
introduced(definition) ).
cnf(t62,plain,
composition(sk1,sk3) = sFlat4,
inference(orient,[status(thm)],[t17]) ).
cnf(t13,axiom,
sFlat0 = complement(sk3),
introduced(definition) ).
cnf(t51,plain,
complement(sk3) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t5,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t86,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t42,t85]) ).
cnf(t22151,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t86,t42]) ).
cnf(t129,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t22151]) ).
cnf(t14,axiom,
sFlat1 = meet(sk2,complement(sk3)),
introduced(definition) ).
cnf(t22147,plain,
sFlat1 = meet(sk2,sFlat0),
inference(step,[status(thm)],[t14,t51]) ).
cnf(t109,plain,
meet(sk2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t22147]) ).
cnf(t131,plain,
meet(sk2,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t109]) ).
cnf(t22153,plain,
meet(sFlat0,sk2) = sFlat1,
inference(step,[status(thm)],[t131,t129]) ).
cnf(t133,plain,
meet(sFlat0,sk2) = sFlat1,
inference(orient,[status(thm)],[t22153]) ).
cnf(t15,axiom,
sFlat2 = composition(sk1,meet(sk2,complement(sk3))),
introduced(definition) ).
cnf(t22139,plain,
sFlat2 = composition(sk1,meet(sk2,sFlat0)),
inference(step,[status(thm)],[t15,t51]) ).
cnf(t73,plain,
composition(sk1,meet(sk2,sFlat0)) = sFlat2,
inference(orient,[status(thm)],[t22139]) ).
cnf(t22148,plain,
composition(sk1,sFlat1) = sFlat2,
inference(step,[status(thm)],[t73,t109]) ).
cnf(t110,plain,
composition(sk1,sFlat1) = sFlat2,
inference(rw,[status(thm)],[t22148]) ).
cnf(t120,plain,
composition(sk1,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t110]) ).
cnf(t16,axiom,
sFlat3 = complement(composition(sk1,meet(sk2,complement(sk3)))),
introduced(definition) ).
cnf(t36,plain,
complement(composition(sk1,meet(sk2,complement(sk3)))) = sFlat3,
inference(orient,[status(thm)],[t16]) ).
cnf(t22137,plain,
complement(composition(sk1,meet(sk2,sFlat0))) = sFlat3,
inference(step,[status(thm)],[t36,t51]) ).
cnf(t55,plain,
complement(composition(sk1,meet(sk2,sFlat0))) = sFlat3,
inference(rw,[status(thm)],[t22137]) ).
cnf(t22169,plain,
complement(composition(sk1,meet(sFlat0,sk2))) = sFlat3,
inference(step,[status(thm)],[t55,t129]) ).
cnf(t22170,plain,
complement(composition(sk1,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t22169,t133]) ).
cnf(t22171,plain,
complement(sFlat2) = sFlat3,
inference(step,[status(thm)],[t22170,t120]) ).
cnf(t389,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t22171]) ).
cnf(t18,axiom,
sFlat5 = join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)),
introduced(definition) ).
cnf(t22143,plain,
sFlat5 = join(composition(sk1,sk3),complement(composition(sk1,meet(sk2,complement(sk3))))),
inference(step,[status(thm)],[t18,t85]) ).
cnf(t22144,plain,
sFlat5 = join(sFlat4,complement(composition(sk1,meet(sk2,complement(sk3))))),
inference(step,[status(thm)],[t22143,t62]) ).
cnf(t22145,plain,
sFlat5 = join(sFlat4,complement(composition(sk1,meet(sk2,sFlat0)))),
inference(step,[status(thm)],[t22144,t51]) ).
cnf(t22146,plain,
sFlat5 = join(sFlat4,complement(sFlat2)),
inference(step,[status(thm)],[t22145,t73]) ).
cnf(t100,plain,
join(sFlat4,complement(sFlat2)) = sFlat5,
inference(orient,[status(thm)],[t22146]) ).
cnf(t22172,plain,
join(sFlat4,sFlat3) = sFlat5,
inference(step,[status(thm)],[t100,t389]) ).
cnf(t399,plain,
join(sFlat4,sFlat3) = sFlat5,
inference(rw,[status(thm)],[t22172]) ).
cnf(t22173,plain,
join(sFlat3,sFlat4) = sFlat5,
inference(step,[status(thm)],[t399,t85]) ).
cnf(t403,plain,
join(sFlat3,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t22173]) ).
cnf(t19,axiom,
sFlat6 = composition(sk1,sk2),
introduced(definition) ).
cnf(t67,plain,
composition(sk1,sk2) = sFlat6,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sFlat7 = complement(composition(sk1,sk2)),
introduced(definition) ).
cnf(t30,plain,
complement(composition(sk1,sk2)) = sFlat7,
inference(orient,[status(thm)],[t20]) ).
cnf(t22138,plain,
complement(sFlat6) = sFlat7,
inference(step,[status(thm)],[t30,t67]) ).
cnf(t72,plain,
complement(sFlat6) = sFlat7,
inference(rw,[status(thm)],[t22138]) ).
cnf(t111,plain,
complement(sFlat6) = sFlat7,
inference(orient,[status(thm)],[t72]) ).
cnf(t21,axiom,
sFlat8 = join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
introduced(definition) ).
cnf(t22140,plain,
sFlat8 = join(composition(sk1,sk3),complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t21,t85]) ).
cnf(t22141,plain,
sFlat8 = join(sFlat4,complement(composition(sk1,sk2))),
inference(step,[status(thm)],[t22140,t62]) ).
cnf(t22142,plain,
sFlat8 = join(sFlat4,complement(sFlat6)),
inference(step,[status(thm)],[t22141,t67]) ).
cnf(t98,plain,
join(sFlat4,complement(sFlat6)) = sFlat8,
inference(orient,[status(thm)],[t22142]) ).
cnf(t22149,plain,
join(sFlat4,sFlat7) = sFlat8,
inference(step,[status(thm)],[t98,t111]) ).
cnf(t116,plain,
join(sFlat4,sFlat7) = sFlat8,
inference(rw,[status(thm)],[t22149]) ).
cnf(t127,plain,
join(sFlat4,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t116]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t22136,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t23,t42]) ).
cnf(t50,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t22136]) ).
cnf(t2607,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t50]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t28,plain,
complement(X1) = join(composition(X2,complement(composition(converse(X2),X1))),complement(X1)),
inference(cp,[status(thm)],[t27,t26]) ).
cnf(t22220,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(step,[status(thm)],[t28,t85]) ).
cnf(t1167,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t22220]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t78,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t80,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t78,t26]) ).
cnf(t212,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t80]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t213,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t212,t22]) ).
cnf(t22159,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t213,t26]) ).
cnf(t222,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t22159]) ).
cnf(t8,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t56,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t57,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t56,t22]) ).
cnf(t142,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t57]) ).
cnf(t224,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t222,t142]) ).
cnf(t22161,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t224,t222]) ).
cnf(t235,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t22161]) ).
cnf(t1192,plain,
complement(X1) = join(complement(X1),complement(composition(converse(one),X1))),
inference(cp,[status(thm)],[t1167,t235]) ).
cnf(t223,plain,
one = converse(one),
inference(cp,[status(thm)],[t222,t22]) ).
cnf(t227,plain,
converse(one) = one,
inference(orient,[status(thm)],[t223]) ).
cnf(t22221,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t1192,t227]) ).
cnf(t22222,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t22221,t235]) ).
cnf(t1212,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t22222]) ).
cnf(t2631,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t2607,t1212]) ).
cnf(t22433,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t2631,t85]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t106,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t22434,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t22433,t106]) ).
cnf(t22435,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t22434,t85]) ).
cnf(t2733,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t22435]) ).
cnf(t24,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)],[t23,t23]) ).
cnf(t22162,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)],[t24,t85]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t92,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t22163,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)],[t22162,t92]) ).
cnf(t22164,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t22163,t42]) ).
cnf(t251,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t22164]) ).
cnf(t1261,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t42,t1212]) ).
cnf(t1301,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t1261]) ).
cnf(t1302,plain,
join(complement(X1),complement(X1)) = join(complement(X1),complement(join(complement(X1),join(X1,complement(complement(X1)))))),
inference(cp,[status(thm)],[t251,t1301]) ).
cnf(t22474,plain,
complement(X1) = join(complement(X1),complement(join(complement(X1),join(X1,complement(complement(X1)))))),
inference(step,[status(thm)],[t1302,t1212]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t88,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t95,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t92,t88]) ).
cnf(t434,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t95]) ).
cnf(t438,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t434,t85]) ).
cnf(t525,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t438]) ).
cnf(t22475,plain,
complement(X1) = join(complement(X1),complement(join(top,X1))),
inference(step,[status(thm)],[t22474,t525]) ).
cnf(t3634,plain,
join(complement(X1),complement(join(top,X1))) = complement(X1),
inference(orient,[status(thm)],[t22475]) ).
cnf(t3683,plain,
complement(X1) = join(complement(X1),complement(join(X1,top))),
inference(cp,[status(thm)],[t3634,t85]) ).
cnf(t93,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t92,t88]) ).
cnf(t743,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t93]) ).
cnf(t1263,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t525,t1212]) ).
cnf(t22247,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t1263,t88]) ).
cnf(t1332,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t22247]) ).
cnf(t1351,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t743,t1332]) ).
cnf(t1358,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t1351]) ).
cnf(t22476,plain,
complement(X1) = join(complement(X1),complement(top)),
inference(step,[status(thm)],[t3683,t1358]) ).
cnf(t91,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t42,t88]) ).
cnf(t22154,plain,
zero = complement(top),
inference(step,[status(thm)],[t91,t106]) ).
cnf(t134,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t22154]) ).
cnf(t22477,plain,
complement(X1) = join(complement(X1),zero),
inference(step,[status(thm)],[t22476,t134]) ).
cnf(t22478,plain,
complement(X1) = join(zero,complement(X1)),
inference(step,[status(thm)],[t22477,t85]) ).
cnf(t3694,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t22478]) ).
cnf(t22494,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t2733,t3694]) ).
cnf(t3740,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t22494]) ).
cnf(t3911,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t3740]) ).
cnf(t38,plain,
X1 = join(complement(join(complement(X1),sFlat3)),complement(join(complement(X1),composition(sk1,meet(sk2,complement(sk3)))))),
inference(cp,[status(thm)],[t23,t36]) ).
cnf(t3938,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t3911,t42]) ).
cnf(t5637,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t3938]) ).
cnf(t22650,plain,
X1 = complement(meet(join(complement(X1),sFlat3),join(complement(X1),composition(sk1,meet(sk2,complement(sk3)))))),
inference(step,[status(thm)],[t38,t5637]) ).
cnf(t22651,plain,
X1 = complement(meet(join(sFlat3,complement(X1)),join(complement(X1),composition(sk1,meet(sk2,complement(sk3)))))),
inference(step,[status(thm)],[t22650,t85]) ).
cnf(t22652,plain,
X1 = complement(meet(join(sFlat3,complement(X1)),join(complement(X1),composition(sk1,meet(sk2,sFlat0))))),
inference(step,[status(thm)],[t22651,t51]) ).
cnf(t22653,plain,
X1 = complement(meet(join(sFlat3,complement(X1)),join(complement(X1),composition(sk1,meet(sFlat0,sk2))))),
inference(step,[status(thm)],[t22652,t129]) ).
cnf(t22654,plain,
X1 = complement(meet(join(sFlat3,complement(X1)),join(complement(X1),composition(sk1,sFlat1)))),
inference(step,[status(thm)],[t22653,t133]) ).
cnf(t22655,plain,
X1 = complement(meet(join(sFlat3,complement(X1)),join(complement(X1),sFlat2))),
inference(step,[status(thm)],[t22654,t120]) ).
cnf(t22656,plain,
X1 = complement(meet(join(sFlat3,complement(X1)),join(sFlat2,complement(X1)))),
inference(step,[status(thm)],[t22655,t85]) ).
cnf(t22657,plain,
X1 = complement(meet(join(sFlat2,complement(X1)),join(sFlat3,complement(X1)))),
inference(step,[status(thm)],[t22656,t129]) ).
cnf(t5750,plain,
complement(meet(join(sFlat2,complement(X1)),join(sFlat3,complement(X1)))) = X1,
inference(orient,[status(thm)],[t22657]) ).
cnf(t5767,plain,
complement(X1) = complement(meet(join(sFlat2,X1),join(sFlat3,complement(complement(X1))))),
inference(cp,[status(thm)],[t5750,t3911]) ).
cnf(t23257,plain,
complement(X1) = complement(meet(join(sFlat2,X1),join(sFlat3,X1))),
inference(step,[status(thm)],[t5767,t3911]) ).
cnf(t13201,plain,
complement(meet(join(sFlat2,X1),join(sFlat3,X1))) = complement(X1),
inference(orient,[status(thm)],[t23257]) ).
cnf(t3945,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t1212,t3911]) ).
cnf(t22533,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t3945,t3911]) ).
cnf(t22534,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t22533,t3911]) ).
cnf(t3985,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t22534]) ).
cnf(t97,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t92,t85]) ).
cnf(t22166,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t97,t92]) ).
cnf(t320,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t22166]) ).
cnf(t3987,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t3985,t320]) ).
cnf(t22612,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t3987,t92]) ).
cnf(t22613,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t22612,t3985]) ).
cnf(t4908,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t22613]) ).
cnf(t2626,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t2607,t42]) ).
cnf(t22441,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t2626,t85]) ).
cnf(t2804,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t22441]) ).
cnf(t2817,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t2804,t129]) ).
cnf(t3295,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t2817]) ).
cnf(t4917,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t4908,t3295]) ).
cnf(t22621,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t4917,t3295]) ).
cnf(t22622,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t22621,t85]) ).
cnf(t5096,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t22622]) ).
cnf(t31,plain,
composition(sk1,sk2) = join(complement(join(sFlat7,complement(X1))),complement(join(complement(composition(sk1,sk2)),X1))),
inference(cp,[status(thm)],[t23,t30]) ).
cnf(t22316,plain,
sFlat6 = join(complement(join(sFlat7,complement(X1))),complement(join(complement(composition(sk1,sk2)),X1))),
inference(step,[status(thm)],[t31,t67]) ).
cnf(t114,plain,
meet(sFlat6,X1) = complement(join(sFlat7,complement(X1))),
inference(cp,[status(thm)],[t42,t111]) ).
cnf(t177,plain,
complement(join(sFlat7,complement(X1))) = meet(sFlat6,X1),
inference(orient,[status(thm)],[t114]) ).
cnf(t22317,plain,
sFlat6 = join(meet(sFlat6,X1),complement(join(complement(composition(sk1,sk2)),X1))),
inference(step,[status(thm)],[t22316,t177]) ).
cnf(t22318,plain,
sFlat6 = join(meet(sFlat6,X1),complement(join(complement(sFlat6),X1))),
inference(step,[status(thm)],[t22317,t67]) ).
cnf(t22319,plain,
sFlat6 = join(meet(sFlat6,X1),complement(join(sFlat7,X1))),
inference(step,[status(thm)],[t22318,t111]) ).
cnf(t1733,plain,
join(meet(sFlat6,X1),complement(join(sFlat7,X1))) = sFlat6,
inference(orient,[status(thm)],[t22319]) ).
cnf(t112,plain,
zero = meet(sFlat6,sFlat7),
inference(cp,[status(thm)],[t106,t111]) ).
cnf(t124,plain,
meet(sFlat6,sFlat7) = zero,
inference(orient,[status(thm)],[t112]) ).
cnf(t1735,plain,
sFlat6 = join(zero,complement(join(sFlat7,sFlat7))),
inference(cp,[status(thm)],[t1733,t124]) ).
cnf(t1232,plain,
complement(sFlat6) = join(sFlat7,complement(sFlat6)),
inference(cp,[status(thm)],[t1212,t111]) ).
cnf(t22226,plain,
sFlat7 = join(sFlat7,complement(sFlat6)),
inference(step,[status(thm)],[t1232,t111]) ).
cnf(t22227,plain,
sFlat7 = join(sFlat7,sFlat7),
inference(step,[status(thm)],[t22226,t111]) ).
cnf(t1270,plain,
join(sFlat7,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t22227]) ).
cnf(t22334,plain,
sFlat6 = join(zero,complement(sFlat7)),
inference(step,[status(thm)],[t1735,t1270]) ).
cnf(t1787,plain,
join(zero,complement(sFlat7)) = sFlat6,
inference(orient,[status(thm)],[t22334]) ).
cnf(t22493,plain,
complement(sFlat7) = sFlat6,
inference(step,[status(thm)],[t1787,t3694]) ).
cnf(t3739,plain,
complement(sFlat7) = sFlat6,
inference(rw,[status(thm)],[t22493]) ).
cnf(t3864,plain,
complement(sFlat7) = sFlat6,
inference(orient,[status(thm)],[t3739]) ).
cnf(t3874,plain,
meet(sFlat7,X1) = complement(join(sFlat6,complement(X1))),
inference(cp,[status(thm)],[t42,t3864]) ).
cnf(t5563,plain,
complement(join(sFlat6,complement(X1))) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t3874]) ).
cnf(t5579,plain,
meet(sFlat7,complement(X1)) = complement(join(sFlat6,X1)),
inference(cp,[status(thm)],[t5563,t3911]) ).
cnf(t5996,plain,
complement(join(sFlat6,X1)) = meet(sFlat7,complement(X1)),
inference(orient,[status(thm)],[t5579]) ).
cnf(t181,plain,
meet(sFlat6,sFlat6) = complement(join(sFlat7,sFlat7)),
inference(cp,[status(thm)],[t177,t111]) ).
cnf(t198,plain,
complement(join(sFlat7,sFlat7)) = meet(sFlat6,sFlat6),
inference(orient,[status(thm)],[t181]) ).
cnf(t252,plain,
join(complement(join(sFlat7,sFlat7)),complement(X1)) = join(meet(sFlat6,sFlat6),complement(join(complement(join(sFlat7,sFlat7)),join(X1,meet(join(sFlat7,sFlat7),X1))))),
inference(cp,[status(thm)],[t251,t198]) ).
cnf(t23573,plain,
complement(meet(join(sFlat7,sFlat7),X1)) = join(meet(sFlat6,sFlat6),complement(join(complement(join(sFlat7,sFlat7)),join(X1,meet(join(sFlat7,sFlat7),X1))))),
inference(step,[status(thm)],[t252,t5637]) ).
cnf(t23574,plain,
complement(meet(sFlat7,X1)) = join(meet(sFlat6,sFlat6),complement(join(complement(join(sFlat7,sFlat7)),join(X1,meet(join(sFlat7,sFlat7),X1))))),
inference(step,[status(thm)],[t23573,t1270]) ).
cnf(t5584,plain,
join(sFlat6,complement(X1)) = complement(meet(sFlat7,X1)),
inference(cp,[status(thm)],[t3911,t5563]) ).
cnf(t6049,plain,
complement(meet(sFlat7,X1)) = join(sFlat6,complement(X1)),
inference(orient,[status(thm)],[t5584]) ).
cnf(t23575,plain,
join(sFlat6,complement(X1)) = join(meet(sFlat6,sFlat6),complement(join(complement(join(sFlat7,sFlat7)),join(X1,meet(join(sFlat7,sFlat7),X1))))),
inference(step,[status(thm)],[t23574,t6049]) ).
cnf(t22228,plain,
complement(sFlat7) = meet(sFlat6,sFlat6),
inference(step,[status(thm)],[t198,t1270]) ).
cnf(t1275,plain,
complement(sFlat7) = meet(sFlat6,sFlat6),
inference(rw,[status(thm)],[t22228]) ).
cnf(t1297,plain,
meet(sFlat6,sFlat6) = complement(sFlat7),
inference(orient,[status(thm)],[t1275]) ).
cnf(t22520,plain,
meet(sFlat6,sFlat6) = sFlat6,
inference(step,[status(thm)],[t1297,t3864]) ).
cnf(t3865,plain,
meet(sFlat6,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t22520]) ).
cnf(t23576,plain,
join(sFlat6,complement(X1)) = join(sFlat6,complement(join(complement(join(sFlat7,sFlat7)),join(X1,meet(join(sFlat7,sFlat7),X1))))),
inference(step,[status(thm)],[t23575,t3865]) ).
cnf(t3948,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t42,t3911]) ).
cnf(t5828,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t3948]) ).
cnf(t23577,plain,
join(sFlat6,complement(X1)) = join(sFlat6,meet(join(sFlat7,sFlat7),complement(join(X1,meet(join(sFlat7,sFlat7),X1))))),
inference(step,[status(thm)],[t23576,t5828]) ).
cnf(t23578,plain,
join(sFlat6,complement(X1)) = join(sFlat6,meet(sFlat7,complement(join(X1,meet(join(sFlat7,sFlat7),X1))))),
inference(step,[status(thm)],[t23577,t1270]) ).
cnf(t23579,plain,
join(sFlat6,complement(X1)) = join(sFlat6,meet(sFlat7,complement(join(X1,meet(sFlat7,X1))))),
inference(step,[status(thm)],[t23578,t1270]) ).
cnf(t19158,plain,
join(sFlat6,meet(sFlat7,complement(join(X1,meet(sFlat7,X1))))) = join(sFlat6,complement(X1)),
inference(orient,[status(thm)],[t23579]) ).
cnf(t19179,plain,
join(sFlat6,complement(X1)) = join(sFlat6,meet(sFlat7,complement(join(X1,meet(X1,sFlat7))))),
inference(cp,[status(thm)],[t19158,t129]) ).
cnf(t23613,plain,
join(sFlat6,complement(X1)) = join(sFlat6,meet(sFlat7,complement(X1))),
inference(step,[status(thm)],[t19179,t5096]) ).
cnf(t19231,plain,
join(sFlat6,meet(sFlat7,complement(X1))) = join(sFlat6,complement(X1)),
inference(orient,[status(thm)],[t23613]) ).
cnf(t19265,plain,
meet(sFlat7,complement(meet(sFlat7,complement(X1)))) = complement(join(sFlat6,complement(X1))),
inference(cp,[status(thm)],[t5996,t19231]) ).
cnf(t23616,plain,
meet(sFlat7,join(sFlat6,complement(complement(X1)))) = complement(join(sFlat6,complement(X1))),
inference(step,[status(thm)],[t19265,t6049]) ).
cnf(t23617,plain,
meet(sFlat7,join(sFlat6,X1)) = complement(join(sFlat6,complement(X1))),
inference(step,[status(thm)],[t23616,t3911]) ).
cnf(t23618,plain,
meet(sFlat7,join(sFlat6,X1)) = meet(sFlat7,X1),
inference(step,[status(thm)],[t23617,t5563]) ).
cnf(t19292,plain,
meet(sFlat7,join(sFlat6,X1)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t23618]) ).
cnf(t19327,plain,
meet(sFlat7,X1) = meet(sFlat7,join(X1,sFlat6)),
inference(cp,[status(thm)],[t19292,t85]) ).
cnf(t19361,plain,
meet(sFlat7,join(X1,sFlat6)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t19327]) ).
cnf(t392,plain,
meet(sFlat2,X1) = complement(join(sFlat3,complement(X1))),
inference(cp,[status(thm)],[t42,t389]) ).
cnf(t585,plain,
complement(join(sFlat3,complement(X1))) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t392]) ).
cnf(t3971,plain,
meet(sFlat2,complement(X1)) = complement(join(sFlat3,X1)),
inference(cp,[status(thm)],[t585,t3911]) ).
cnf(t4596,plain,
complement(join(sFlat3,X1)) = meet(sFlat2,complement(X1)),
inference(orient,[status(thm)],[t3971]) ).
cnf(t101,plain,
join(sFlat4,join(complement(sFlat2),X1)) = join(sFlat5,X1),
inference(cp,[status(thm)],[t92,t100]) ).
cnf(t22180,plain,
join(sFlat4,join(sFlat3,X1)) = join(sFlat5,X1),
inference(step,[status(thm)],[t101,t389]) ).
cnf(t22181,plain,
join(sFlat3,join(sFlat4,X1)) = join(sFlat5,X1),
inference(step,[status(thm)],[t22180,t320]) ).
cnf(t483,plain,
join(sFlat3,join(sFlat4,X1)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t22181]) ).
cnf(t4599,plain,
meet(sFlat2,complement(join(sFlat4,X1))) = complement(join(sFlat5,X1)),
inference(cp,[status(thm)],[t4596,t483]) ).
cnf(t6631,plain,
meet(sFlat2,complement(join(sFlat4,X1))) = complement(join(sFlat5,X1)),
inference(orient,[status(thm)],[t4599]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t102,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t217,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t102,t212]) ).
cnf(t8314,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t217]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t59,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t81,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t59,t78]) ).
cnf(t13388,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t81]) ).
cnf(t13461,plain,
join(converse(converse(composition(X1,X2))),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(cp,[status(thm)],[t8314,t13388]) ).
cnf(t23281,plain,
join(composition(X1,X2),composition(converse(converse(X1)),X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t13461,t26]) ).
cnf(t23282,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(composition(join(converse(X2),converse(X3)),converse(X1))),
inference(step,[status(thm)],[t23281,t26]) ).
cnf(t103,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t102,t26]) ).
cnf(t238,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t103]) ).
cnf(t247,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(cp,[status(thm)],[t78,t238]) ).
cnf(t8463,plain,
converse(composition(join(converse(X1),X2),X3)) = composition(converse(X3),join(X1,converse(X2))),
inference(orient,[status(thm)],[t247]) ).
cnf(t23283,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(converse(converse(X1)),join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t23282,t8463]) ).
cnf(t23284,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,converse(converse(X3)))),
inference(step,[status(thm)],[t23283,t26]) ).
cnf(t23285,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t23284,t26]) ).
cnf(t13467,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t23285]) ).
cnf(t13551,plain,
composition(sk1,join(X1,sk2)) = join(composition(sk1,X1),sFlat6),
inference(cp,[status(thm)],[t13467,t67]) ).
cnf(t23288,plain,
composition(sk1,join(X1,sk2)) = join(sFlat6,composition(sk1,X1)),
inference(step,[status(thm)],[t13551,t85]) ).
cnf(t13735,plain,
composition(sk1,join(X1,sk2)) = join(sFlat6,composition(sk1,X1)),
inference(orient,[status(thm)],[t23288]) ).
cnf(t52,plain,
meet(sk3,X1) = complement(join(sFlat0,complement(X1))),
inference(cp,[status(thm)],[t42,t51]) ).
cnf(t143,plain,
complement(join(sFlat0,complement(X1))) = meet(sk3,X1),
inference(orient,[status(thm)],[t52]) ).
cnf(t146,plain,
meet(sk3,sk3) = complement(join(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t143,t51]) ).
cnf(t165,plain,
complement(join(sFlat0,sFlat0)) = meet(sk3,sk3),
inference(orient,[status(thm)],[t146]) ).
cnf(t255,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)],[t251,t165]) ).
cnf(t23729,plain,
complement(meet(join(sFlat0,sFlat0),X1)) = join(meet(sk3,sk3),complement(join(complement(join(sFlat0,sFlat0)),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t255,t5637]) ).
cnf(t1233,plain,
complement(sk3) = join(sFlat0,complement(sk3)),
inference(cp,[status(thm)],[t1212,t51]) ).
cnf(t22229,plain,
sFlat0 = join(sFlat0,complement(sk3)),
inference(step,[status(thm)],[t1233,t51]) ).
cnf(t22230,plain,
sFlat0 = join(sFlat0,sFlat0),
inference(step,[status(thm)],[t22229,t51]) ).
cnf(t1276,plain,
join(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t22230]) ).
cnf(t23730,plain,
complement(meet(sFlat0,X1)) = join(meet(sk3,sk3),complement(join(complement(join(sFlat0,sFlat0)),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t23729,t1276]) ).
cnf(t22231,plain,
complement(sFlat0) = meet(sk3,sk3),
inference(step,[status(thm)],[t165,t1276]) ).
cnf(t1278,plain,
complement(sFlat0) = meet(sk3,sk3),
inference(rw,[status(thm)],[t22231]) ).
cnf(t1299,plain,
meet(sk3,sk3) = complement(sFlat0),
inference(orient,[status(thm)],[t1278]) ).
cnf(t2618,plain,
sk3 = join(complement(sFlat0),complement(join(complement(sk3),sk3))),
inference(cp,[status(thm)],[t2607,t1299]) ).
cnf(t22429,plain,
sk3 = join(complement(sFlat0),complement(join(sk3,complement(sk3)))),
inference(step,[status(thm)],[t2618,t85]) ).
cnf(t22430,plain,
sk3 = join(complement(sFlat0),complement(top)),
inference(step,[status(thm)],[t22429,t88]) ).
cnf(t22431,plain,
sk3 = join(complement(sFlat0),zero),
inference(step,[status(thm)],[t22430,t134]) ).
cnf(t22432,plain,
sk3 = join(zero,complement(sFlat0)),
inference(step,[status(thm)],[t22431,t85]) ).
cnf(t2732,plain,
join(zero,complement(sFlat0)) = sk3,
inference(orient,[status(thm)],[t22432]) ).
cnf(t22491,plain,
complement(sFlat0) = sk3,
inference(step,[status(thm)],[t2732,t3694]) ).
cnf(t3737,plain,
complement(sFlat0) = sk3,
inference(rw,[status(thm)],[t22491]) ).
cnf(t3770,plain,
complement(sFlat0) = sk3,
inference(orient,[status(thm)],[t3737]) ).
cnf(t5659,plain,
complement(meet(sFlat0,X1)) = join(sk3,complement(X1)),
inference(cp,[status(thm)],[t5637,t3770]) ).
cnf(t6076,plain,
complement(meet(sFlat0,X1)) = join(sk3,complement(X1)),
inference(orient,[status(thm)],[t5659]) ).
cnf(t23731,plain,
join(sk3,complement(X1)) = join(meet(sk3,sk3),complement(join(complement(join(sFlat0,sFlat0)),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t23730,t6076]) ).
cnf(t22500,plain,
meet(sk3,sk3) = sk3,
inference(step,[status(thm)],[t1299,t3770]) ).
cnf(t3771,plain,
meet(sk3,sk3) = sk3,
inference(orient,[status(thm)],[t22500]) ).
cnf(t23732,plain,
join(sk3,complement(X1)) = join(sk3,complement(join(complement(join(sFlat0,sFlat0)),join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t23731,t3771]) ).
cnf(t23733,plain,
join(sk3,complement(X1)) = join(sk3,meet(join(sFlat0,sFlat0),complement(join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t23732,t5828]) ).
cnf(t23734,plain,
join(sk3,complement(X1)) = join(sk3,meet(sFlat0,complement(join(X1,meet(join(sFlat0,sFlat0),X1))))),
inference(step,[status(thm)],[t23733,t1276]) ).
cnf(t23735,plain,
join(sk3,complement(X1)) = join(sk3,meet(sFlat0,complement(join(X1,meet(sFlat0,X1))))),
inference(step,[status(thm)],[t23734,t1276]) ).
cnf(t21783,plain,
join(sk3,meet(sFlat0,complement(join(X1,meet(sFlat0,X1))))) = join(sk3,complement(X1)),
inference(orient,[status(thm)],[t23735]) ).
cnf(t21807,plain,
join(sk3,complement(X1)) = join(sk3,meet(sFlat0,complement(join(X1,meet(X1,sFlat0))))),
inference(cp,[status(thm)],[t21783,t129]) ).
cnf(t23755,plain,
join(sk3,complement(X1)) = join(sk3,meet(sFlat0,complement(X1))),
inference(step,[status(thm)],[t21807,t5096]) ).
cnf(t21843,plain,
join(sk3,meet(sFlat0,complement(X1))) = join(sk3,complement(X1)),
inference(orient,[status(thm)],[t23755]) ).
cnf(t21873,plain,
join(sk3,complement(complement(X1))) = join(sk3,meet(sFlat0,X1)),
inference(cp,[status(thm)],[t21843,t3911]) ).
cnf(t23757,plain,
join(sk3,X1) = join(sk3,meet(sFlat0,X1)),
inference(step,[status(thm)],[t21873,t3911]) ).
cnf(t21879,plain,
join(sk3,meet(sFlat0,X1)) = join(sk3,X1),
inference(orient,[status(thm)],[t23757]) ).
cnf(t21884,plain,
join(sk3,sk2) = join(sk3,sFlat1),
inference(cp,[status(thm)],[t21879,t133]) ).
cnf(t23762,plain,
join(sk3,sk2) = join(sFlat1,sk3),
inference(step,[status(thm)],[t21884,t85]) ).
cnf(t21899,plain,
join(sk3,sk2) = join(sFlat1,sk3),
inference(orient,[status(thm)],[t23762]) ).
cnf(t21900,plain,
join(sFlat6,composition(sk1,sk3)) = composition(sk1,join(sFlat1,sk3)),
inference(cp,[status(thm)],[t13735,t21899]) ).
cnf(t23763,plain,
join(sFlat6,sFlat4) = composition(sk1,join(sFlat1,sk3)),
inference(step,[status(thm)],[t21900,t62]) ).
cnf(t23764,plain,
join(sFlat4,sFlat6) = composition(sk1,join(sFlat1,sk3)),
inference(step,[status(thm)],[t23763,t85]) ).
cnf(t13509,plain,
composition(sk1,join(sFlat1,X1)) = join(sFlat2,composition(sk1,X1)),
inference(cp,[status(thm)],[t13467,t120]) ).
cnf(t13563,plain,
composition(sk1,join(sFlat1,X1)) = join(sFlat2,composition(sk1,X1)),
inference(orient,[status(thm)],[t13509]) ).
cnf(t23765,plain,
join(sFlat4,sFlat6) = join(sFlat2,composition(sk1,sk3)),
inference(step,[status(thm)],[t23764,t13563]) ).
cnf(t23766,plain,
join(sFlat4,sFlat6) = join(sFlat2,sFlat4),
inference(step,[status(thm)],[t23765,t62]) ).
cnf(t21908,plain,
join(sFlat4,sFlat6) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t23766]) ).
cnf(t21922,plain,
complement(join(sFlat5,sFlat6)) = meet(sFlat2,complement(join(sFlat2,sFlat4))),
inference(cp,[status(thm)],[t6631,t21908]) ).
cnf(t3947,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t42,t3911]) ).
cnf(t5693,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t3947]) ).
cnf(t5715,plain,
meet(complement(X1),sFlat7) = complement(join(X1,sFlat6)),
inference(cp,[status(thm)],[t5693,t3864]) ).
cnf(t22685,plain,
meet(sFlat7,complement(X1)) = complement(join(X1,sFlat6)),
inference(step,[status(thm)],[t5715,t129]) ).
cnf(t6158,plain,
complement(join(X1,sFlat6)) = meet(sFlat7,complement(X1)),
inference(orient,[status(thm)],[t22685]) ).
cnf(t23778,plain,
meet(sFlat7,complement(sFlat5)) = meet(sFlat2,complement(join(sFlat2,sFlat4))),
inference(step,[status(thm)],[t21922,t6158]) ).
cnf(t4610,plain,
meet(sFlat2,complement(join(X1,X2))) = complement(join(X1,join(sFlat3,X2))),
inference(cp,[status(thm)],[t4596,t320]) ).
cnf(t6332,plain,
complement(join(X1,join(sFlat3,X2))) = meet(sFlat2,complement(join(X1,X2))),
inference(orient,[status(thm)],[t4610]) ).
cnf(t6346,plain,
meet(sFlat2,complement(join(X1,sFlat4))) = complement(join(X1,sFlat5)),
inference(cp,[status(thm)],[t6332,t403]) ).
cnf(t6715,plain,
meet(sFlat2,complement(join(X1,sFlat4))) = complement(join(X1,sFlat5)),
inference(orient,[status(thm)],[t6346]) ).
cnf(t23779,plain,
meet(sFlat7,complement(sFlat5)) = complement(join(sFlat2,sFlat5)),
inference(step,[status(thm)],[t23778,t6715]) ).
cnf(t137,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t42,t134]) ).
cnf(t360,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t137]) ).
cnf(t394,plain,
meet(top,sFlat2) = complement(join(zero,sFlat3)),
inference(cp,[status(thm)],[t360,t389]) ).
cnf(t22174,plain,
meet(sFlat2,top) = complement(join(zero,sFlat3)),
inference(step,[status(thm)],[t394,t129]) ).
cnf(t22175,plain,
meet(sFlat2,top) = complement(join(sFlat3,zero)),
inference(step,[status(thm)],[t22174,t85]) ).
cnf(t404,plain,
complement(join(sFlat3,zero)) = meet(sFlat2,top),
inference(orient,[status(thm)],[t22175]) ).
cnf(t1303,plain,
meet(sFlat2,sFlat2) = complement(sFlat3),
inference(cp,[status(thm)],[t1301,t389]) ).
cnf(t1330,plain,
meet(sFlat2,sFlat2) = complement(sFlat3),
inference(orient,[status(thm)],[t1303]) ).
cnf(t1331,plain,
join(complement(sFlat2),complement(sFlat2)) = join(complement(sFlat2),complement(join(complement(sFlat2),join(sFlat2,complement(sFlat3))))),
inference(cp,[status(thm)],[t251,t1330]) ).
cnf(t22303,plain,
complement(sFlat2) = join(complement(sFlat2),complement(join(complement(sFlat2),join(sFlat2,complement(sFlat3))))),
inference(step,[status(thm)],[t1331,t1212]) ).
cnf(t22304,plain,
sFlat3 = join(complement(sFlat2),complement(join(complement(sFlat2),join(sFlat2,complement(sFlat3))))),
inference(step,[status(thm)],[t22303,t389]) ).
cnf(t22305,plain,
sFlat3 = join(sFlat3,complement(join(complement(sFlat2),join(sFlat2,complement(sFlat3))))),
inference(step,[status(thm)],[t22304,t389]) ).
cnf(t22306,plain,
sFlat3 = join(sFlat3,complement(join(sFlat2,join(complement(sFlat2),complement(sFlat3))))),
inference(step,[status(thm)],[t22305,t320]) ).
cnf(t22307,plain,
sFlat3 = join(sFlat3,complement(join(top,complement(sFlat3)))),
inference(step,[status(thm)],[t22306,t434]) ).
cnf(t22308,plain,
sFlat3 = join(sFlat3,complement(top)),
inference(step,[status(thm)],[t22307,t1332]) ).
cnf(t22309,plain,
sFlat3 = join(sFlat3,zero),
inference(step,[status(thm)],[t22308,t134]) ).
cnf(t1606,plain,
join(sFlat3,zero) = sFlat3,
inference(orient,[status(thm)],[t22309]) ).
cnf(t22310,plain,
complement(sFlat3) = meet(sFlat2,top),
inference(step,[status(thm)],[t404,t1606]) ).
cnf(t1607,plain,
complement(sFlat3) = meet(sFlat2,top),
inference(rw,[status(thm)],[t22310]) ).
cnf(t1608,plain,
meet(sFlat2,top) = complement(sFlat3),
inference(orient,[status(thm)],[t1607]) ).
cnf(t2621,plain,
sFlat2 = join(complement(sFlat3),complement(join(complement(sFlat2),top))),
inference(cp,[status(thm)],[t2607,t1608]) ).
cnf(t22418,plain,
sFlat2 = join(complement(sFlat3),complement(top)),
inference(step,[status(thm)],[t2621,t1358]) ).
cnf(t22419,plain,
sFlat2 = join(complement(sFlat3),zero),
inference(step,[status(thm)],[t22418,t134]) ).
cnf(t22420,plain,
sFlat2 = join(zero,complement(sFlat3)),
inference(step,[status(thm)],[t22419,t85]) ).
cnf(t2692,plain,
join(zero,complement(sFlat3)) = sFlat2,
inference(orient,[status(thm)],[t22420]) ).
cnf(t22492,plain,
complement(sFlat3) = sFlat2,
inference(step,[status(thm)],[t2692,t3694]) ).
cnf(t3738,plain,
complement(sFlat3) = sFlat2,
inference(rw,[status(thm)],[t22492]) ).
cnf(t3817,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t3738]) ).
cnf(t3825,plain,
meet(sFlat3,X1) = complement(join(sFlat2,complement(X1))),
inference(cp,[status(thm)],[t42,t3817]) ).
cnf(t5326,plain,
complement(join(sFlat2,complement(X1))) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t3825]) ).
cnf(t5340,plain,
meet(sFlat3,complement(X1)) = complement(join(sFlat2,X1)),
inference(cp,[status(thm)],[t5326,t3911]) ).
cnf(t5464,plain,
complement(join(sFlat2,X1)) = meet(sFlat3,complement(X1)),
inference(orient,[status(thm)],[t5340]) ).
cnf(t23780,plain,
meet(sFlat7,complement(sFlat5)) = meet(sFlat3,complement(sFlat5)),
inference(step,[status(thm)],[t23779,t5464]) ).
cnf(t526,plain,
join(top,sFlat4) = join(sFlat5,complement(sFlat3)),
inference(cp,[status(thm)],[t525,t483]) ).
cnf(t22186,plain,
join(sFlat4,top) = join(sFlat5,complement(sFlat3)),
inference(step,[status(thm)],[t526,t85]) ).
cnf(t551,plain,
join(sFlat5,complement(sFlat3)) = join(sFlat4,top),
inference(orient,[status(thm)],[t22186]) ).
cnf(t22259,plain,
join(sFlat5,complement(sFlat3)) = top,
inference(step,[status(thm)],[t551,t1358]) ).
cnf(t1363,plain,
join(sFlat5,complement(sFlat3)) = top,
inference(orient,[status(thm)],[t22259]) ).
cnf(t22517,plain,
join(sFlat5,sFlat2) = top,
inference(step,[status(thm)],[t1363,t3817]) ).
cnf(t3862,plain,
join(sFlat5,sFlat2) = top,
inference(rw,[status(thm)],[t22517]) ).
cnf(t22565,plain,
join(sFlat2,sFlat5) = top,
inference(step,[status(thm)],[t3862,t85]) ).
cnf(t4107,plain,
join(sFlat2,sFlat5) = top,
inference(orient,[status(thm)],[t22565]) ).
cnf(t5465,plain,
meet(sFlat3,complement(sFlat5)) = complement(top),
inference(cp,[status(thm)],[t5464,t4107]) ).
cnf(t22678,plain,
meet(sFlat3,complement(sFlat5)) = zero,
inference(step,[status(thm)],[t5465,t134]) ).
cnf(t5941,plain,
meet(sFlat3,complement(sFlat5)) = zero,
inference(orient,[status(thm)],[t22678]) ).
cnf(t23781,plain,
meet(sFlat7,complement(sFlat5)) = zero,
inference(step,[status(thm)],[t23780,t5941]) ).
cnf(t21947,plain,
meet(sFlat7,complement(sFlat5)) = zero,
inference(orient,[status(thm)],[t23781]) ).
cnf(t21952,plain,
join(sFlat6,complement(complement(sFlat5))) = complement(zero),
inference(cp,[status(thm)],[t6049,t21947]) ).
cnf(t23784,plain,
join(sFlat6,sFlat5) = complement(zero),
inference(step,[status(thm)],[t21952,t3911]) ).
cnf(t23785,plain,
join(sFlat5,sFlat6) = complement(zero),
inference(step,[status(thm)],[t23784,t85]) ).
cnf(t3705,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t3694,t88]) ).
cnf(t3744,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t3705]) ).
cnf(t23786,plain,
join(sFlat5,sFlat6) = top,
inference(step,[status(thm)],[t23785,t3744]) ).
cnf(t21961,plain,
join(sFlat5,sFlat6) = top,
inference(orient,[status(thm)],[t23786]) ).
cnf(t21962,plain,
meet(sFlat7,sFlat5) = meet(sFlat7,top),
inference(cp,[status(thm)],[t19361,t21961]) ).
cnf(t23787,plain,
meet(sFlat5,sFlat7) = meet(sFlat7,top),
inference(step,[status(thm)],[t21962,t129]) ).
cnf(t1788,plain,
meet(top,sFlat7) = complement(sFlat6),
inference(cp,[status(thm)],[t360,t1787]) ).
cnf(t22335,plain,
meet(sFlat7,top) = complement(sFlat6),
inference(step,[status(thm)],[t1788,t129]) ).
cnf(t22336,plain,
meet(sFlat7,top) = sFlat7,
inference(step,[status(thm)],[t22335,t111]) ).
cnf(t1789,plain,
meet(sFlat7,top) = sFlat7,
inference(orient,[status(thm)],[t22336]) ).
cnf(t23788,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(step,[status(thm)],[t23787,t1789]) ).
cnf(t21963,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t23788]) ).
cnf(t21965,plain,
sFlat5 = join(sFlat5,sFlat7),
inference(cp,[status(thm)],[t5096,t21963]) ).
cnf(t485,plain,
join(sFlat5,sFlat7) = join(sFlat3,sFlat8),
inference(cp,[status(thm)],[t483,t127]) ).
cnf(t488,plain,
join(sFlat5,sFlat7) = join(sFlat3,sFlat8),
inference(orient,[status(thm)],[t485]) ).
cnf(t23789,plain,
sFlat5 = join(sFlat3,sFlat8),
inference(step,[status(thm)],[t21965,t488]) ).
cnf(t21973,plain,
join(sFlat3,sFlat8) = sFlat5,
inference(orient,[status(thm)],[t23789]) ).
cnf(t21981,plain,
complement(sFlat8) = complement(meet(join(sFlat2,sFlat8),sFlat5)),
inference(cp,[status(thm)],[t13201,t21973]) ).
cnf(t23794,plain,
complement(sFlat8) = complement(meet(sFlat5,join(sFlat2,sFlat8))),
inference(step,[status(thm)],[t21981,t129]) ).
cnf(t5346,plain,
join(sFlat2,complement(X1)) = complement(meet(sFlat3,X1)),
inference(cp,[status(thm)],[t3911,t5326]) ).
cnf(t5524,plain,
complement(meet(sFlat3,X1)) = join(sFlat2,complement(X1)),
inference(orient,[status(thm)],[t5346]) ).
cnf(t3972,plain,
meet(sFlat6,complement(X1)) = complement(join(sFlat7,X1)),
inference(cp,[status(thm)],[t177,t3911]) ).
cnf(t4697,plain,
complement(join(sFlat7,X1)) = meet(sFlat6,complement(X1)),
inference(orient,[status(thm)],[t3972]) ).
cnf(t4715,plain,
meet(sFlat6,complement(join(X1,X2))) = complement(join(X1,join(sFlat7,X2))),
inference(cp,[status(thm)],[t4697,t320]) ).
cnf(t12915,plain,
complement(join(X1,join(sFlat7,X2))) = meet(sFlat6,complement(join(X1,X2))),
inference(orient,[status(thm)],[t4715]) ).
cnf(t128,plain,
join(sFlat4,join(sFlat7,X1)) = join(sFlat8,X1),
inference(cp,[status(thm)],[t92,t127]) ).
cnf(t357,plain,
join(sFlat4,join(sFlat7,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t128]) ).
cnf(t12922,plain,
meet(sFlat6,complement(join(sFlat4,X1))) = complement(join(sFlat8,X1)),
inference(cp,[status(thm)],[t12915,t357]) ).
cnf(t15616,plain,
meet(sFlat6,complement(join(sFlat4,X1))) = complement(join(sFlat8,X1)),
inference(orient,[status(thm)],[t12922]) ).
cnf(t21916,plain,
complement(join(sFlat8,sFlat6)) = meet(sFlat6,complement(join(sFlat2,sFlat4))),
inference(cp,[status(thm)],[t15616,t21908]) ).
cnf(t23767,plain,
meet(sFlat7,complement(sFlat8)) = meet(sFlat6,complement(join(sFlat2,sFlat4))),
inference(step,[status(thm)],[t21916,t6158]) ).
cnf(t113,plain,
top = join(sFlat6,sFlat7),
inference(cp,[status(thm)],[t88,t111]) ).
cnf(t125,plain,
join(sFlat6,sFlat7) = top,
inference(orient,[status(thm)],[t113]) ).
cnf(t126,plain,
join(sFlat6,join(sFlat7,X1)) = join(top,X1),
inference(cp,[status(thm)],[t92,t125]) ).
cnf(t354,plain,
join(sFlat6,join(sFlat7,X1)) = join(top,X1),
inference(orient,[status(thm)],[t126]) ).
cnf(t1272,plain,
join(sFlat8,sFlat7) = join(sFlat4,sFlat7),
inference(cp,[status(thm)],[t357,t1270]) ).
cnf(t22232,plain,
join(sFlat7,sFlat8) = join(sFlat4,sFlat7),
inference(step,[status(thm)],[t1272,t85]) ).
cnf(t22233,plain,
join(sFlat7,sFlat8) = sFlat8,
inference(step,[status(thm)],[t22232,t127]) ).
cnf(t1279,plain,
join(sFlat7,sFlat8) = sFlat8,
inference(orient,[status(thm)],[t22233]) ).
cnf(t1282,plain,
join(top,sFlat8) = join(sFlat6,sFlat8),
inference(cp,[status(thm)],[t354,t1279]) ).
cnf(t22269,plain,
join(sFlat8,top) = join(sFlat6,sFlat8),
inference(step,[status(thm)],[t1282,t85]) ).
cnf(t22270,plain,
top = join(sFlat6,sFlat8),
inference(step,[status(thm)],[t22269,t1358]) ).
cnf(t1384,plain,
join(sFlat6,sFlat8) = top,
inference(orient,[status(thm)],[t22270]) ).
cnf(t6000,plain,
meet(sFlat7,complement(sFlat8)) = complement(top),
inference(cp,[status(thm)],[t5996,t1384]) ).
cnf(t22682,plain,
meet(sFlat7,complement(sFlat8)) = zero,
inference(step,[status(thm)],[t6000,t134]) ).
cnf(t6048,plain,
meet(sFlat7,complement(sFlat8)) = zero,
inference(orient,[status(thm)],[t22682]) ).
cnf(t23768,plain,
zero = meet(sFlat6,complement(join(sFlat2,sFlat4))),
inference(step,[status(thm)],[t23767,t6048]) ).
cnf(t94,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t92,t85]) ).
cnf(t314,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t94]) ).
cnf(t4716,plain,
meet(sFlat6,complement(join(X1,X2))) = complement(join(X1,join(X2,sFlat7))),
inference(cp,[status(thm)],[t4697,t314]) ).
cnf(t13022,plain,
complement(join(X1,join(X2,sFlat7))) = meet(sFlat6,complement(join(X1,X2))),
inference(orient,[status(thm)],[t4716]) ).
cnf(t13029,plain,
meet(sFlat6,complement(join(X1,sFlat4))) = complement(join(X1,sFlat8)),
inference(cp,[status(thm)],[t13022,t127]) ).
cnf(t15743,plain,
meet(sFlat6,complement(join(X1,sFlat4))) = complement(join(X1,sFlat8)),
inference(orient,[status(thm)],[t13029]) ).
cnf(t23769,plain,
zero = complement(join(sFlat2,sFlat8)),
inference(step,[status(thm)],[t23768,t15743]) ).
cnf(t23770,plain,
zero = meet(sFlat3,complement(sFlat8)),
inference(step,[status(thm)],[t23769,t5464]) ).
cnf(t21927,plain,
meet(sFlat3,complement(sFlat8)) = zero,
inference(orient,[status(thm)],[t23770]) ).
cnf(t21930,plain,
join(sFlat2,complement(complement(sFlat8))) = complement(zero),
inference(cp,[status(thm)],[t5524,t21927]) ).
cnf(t23773,plain,
join(sFlat2,sFlat8) = complement(zero),
inference(step,[status(thm)],[t21930,t3911]) ).
cnf(t23774,plain,
join(sFlat2,sFlat8) = top,
inference(step,[status(thm)],[t23773,t3744]) ).
cnf(t21939,plain,
join(sFlat2,sFlat8) = top,
inference(orient,[status(thm)],[t23774]) ).
cnf(t23795,plain,
complement(sFlat8) = complement(meet(sFlat5,top)),
inference(step,[status(thm)],[t23794,t21939]) ).
cnf(t22495,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t360,t3694]) ).
cnf(t3741,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t22495]) ).
cnf(t22542,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t3741,t3911]) ).
cnf(t4037,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t22542]) ).
cnf(t4042,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t4037,t129]) ).
cnf(t4092,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t4042]) ).
cnf(t23796,plain,
complement(sFlat8) = complement(sFlat5),
inference(step,[status(thm)],[t23795,t4092]) ).
cnf(t21985,plain,
complement(sFlat8) = complement(sFlat5),
inference(orient,[status(thm)],[t23796]) ).
cnf(t22000,plain,
sFlat8 = complement(complement(sFlat5)),
inference(cp,[status(thm)],[t3911,t21985]) ).
cnf(t23820,plain,
sFlat8 = sFlat5,
inference(step,[status(thm)],[t22000,t3911]) ).
cnf(t22061,plain,
sFlat8 = sFlat5,
inference(orient,[status(thm)],[t23820]) ).
cnf(t23821,plain,
join(sFlat4,sFlat7) = sFlat5,
inference(step,[status(thm)],[t127,t22061]) ).
cnf(t22062,plain,
join(sFlat4,sFlat7) = sFlat5,
inference(orient,[status(thm)],[t23821]) ).
cnf(goal_0,negated_conjecture,
join(complement(composition(sk1,meet(sk2,complement(sk3)))),composition(sk1,sk3)) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(composition(sk1,sk3),complement(composition(sk1,meet(sk2,complement(sk3))))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[goal_0,t85]) ).
cnf(g0_1,plain,
join(sFlat4,complement(composition(sk1,meet(sk2,complement(sk3))))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_0,t62]) ).
cnf(g0_2,plain,
join(sFlat4,complement(composition(sk1,meet(sk2,sFlat0)))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_1,t51]) ).
cnf(g0_3,plain,
join(sFlat4,complement(composition(sk1,meet(sFlat0,sk2)))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_2,t129]) ).
cnf(g0_4,plain,
join(sFlat4,complement(composition(sk1,sFlat1))) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_3,t133]) ).
cnf(g0_5,plain,
join(sFlat4,complement(sFlat2)) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_4,t120]) ).
cnf(g0_6,plain,
join(sFlat4,sFlat3) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_5,t389]) ).
cnf(g0_7,plain,
join(sFlat3,sFlat4) != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_6,t85]) ).
cnf(g0_8,plain,
sFlat5 != join(complement(composition(sk1,sk2)),composition(sk1,sk3)),
inference(rw,[status(thm)],[g0_7,t403]) ).
cnf(g0_9,plain,
sFlat5 != join(composition(sk1,sk3),complement(composition(sk1,sk2))),
inference(rw,[status(thm)],[g0_8,t85]) ).
cnf(g0_10,plain,
sFlat5 != join(sFlat4,complement(composition(sk1,sk2))),
inference(rw,[status(thm)],[g0_9,t62]) ).
cnf(g0_11,plain,
sFlat5 != join(sFlat4,complement(sFlat6)),
inference(rw,[status(thm)],[g0_10,t67]) ).
cnf(g0_12,plain,
sFlat5 != join(sFlat4,sFlat7),
inference(rw,[status(thm)],[g0_11,t111]) ).
cnf(g0_13,plain,
sFlat5 != sFlat5,
inference(rw,[status(thm)],[g0_12,t22062]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_13]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL017-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 07:16:18 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 59.39/7.95 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 59.39/7.95 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------