%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL034-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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:56 PM UTC 2026
% Result : Unsatisfiable 11.93s 8.51s
% Output : CNFRefutation 11.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 73
% Number of leaves : 25
% Syntax : Number of clauses : 346 ( 346 unt; 0 nHn; 210 RR)
% Number of literals : 346 ( 345 equ; 23 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 17 con; 0-2 aty)
% Number of variables : 185 ( 21 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t108,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t9,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t99,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t11,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t92,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(rw,[status(thm)],[t30]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t90,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t23388,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t92,t90]) ).
cnf(t589,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t23388]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t132,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t2,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t134,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t132,t29]) ).
cnf(t495,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t134]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t496,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t495,t28]) ).
cnf(t23385,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t496,t29]) ).
cnf(t515,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t23385]) ).
cnf(t516,plain,
one = converse(one),
inference(cp,[status(thm)],[t515,t28]) ).
cnf(t520,plain,
converse(one) = one,
inference(orient,[status(thm)],[t516]) ).
cnf(t599,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t589,t520]) ).
cnf(t23386,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t515,t520]) ).
cnf(t529,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t23386]) ).
cnf(t530,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t529]) ).
cnf(t23402,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t599,t530]) ).
cnf(t23403,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t23402,t530]) ).
cnf(t647,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t23403]) ).
cnf(t12,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t91,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t25]) ).
cnf(t23374,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t91,t90]) ).
cnf(t256,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t23374]) ).
cnf(t663,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t256,t647]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t93,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t23444,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t663,t93]) ).
cnf(u0,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t33,plain,
complement(join(complement(X1),complement(complement(X1)))) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t23325,plain,
complement(top) = zero,
inference(step,[status(thm)],[t33,t93]) ).
cnf(t98,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t23325]) ).
cnf(t149,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t98]) ).
cnf(t23445,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t23444,t149]) ).
cnf(t23446,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t23445,t90]) ).
cnf(t740,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t23446]) ).
cnf(t651,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t647,t149]) ).
cnf(t23410,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t651,t149]) ).
cnf(t23411,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t23410,t149]) ).
cnf(t679,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t23411]) ).
cnf(t680,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t99,t679]) ).
cnf(t1106,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t680]) ).
cnf(t1112,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t1106,t740]) ).
cnf(t23591,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t1112,t740]) ).
cnf(t1127,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t23591]) ).
cnf(t23599,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t740,t1127]) ).
cnf(t1144,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t23599]) ).
cnf(t1200,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1144]) ).
cnf(t1201,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t647,t1200]) ).
cnf(t23615,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1201,t1200]) ).
cnf(t23616,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t23615,t1200]) ).
cnf(t1220,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t23616]) ).
cnf(t1226,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t99,t1220]) ).
cnf(t1735,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1226]) ).
cnf(t1742,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t1735,t256]) ).
cnf(t23821,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t1742,t256]) ).
cnf(t23822,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t23821,t90]) ).
cnf(t3485,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t23822]) ).
cnf(t14,axiom,
sFlat1 = complement(sk3),
introduced(definition) ).
cnf(t83,plain,
complement(sk3) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t13,axiom,
sFlat0 = complement(sk1),
introduced(definition) ).
cnf(t60,plain,
complement(sk1) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t15,axiom,
sFlat2 = join(complement(sk1),complement(sk3)),
introduced(definition) ).
cnf(t23326,plain,
sFlat2 = join(complement(sk3),complement(sk1)),
inference(step,[status(thm)],[t15,t90]) ).
cnf(t23327,plain,
sFlat2 = join(sFlat1,complement(sk1)),
inference(step,[status(thm)],[t23326,t83]) ).
cnf(t23328,plain,
sFlat2 = join(sFlat1,sFlat0),
inference(step,[status(thm)],[t23327,t60]) ).
cnf(t23329,plain,
sFlat2 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t23328,t90]) ).
cnf(t104,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t23329]) ).
cnf(t16,axiom,
sFlat3 = complement(join(complement(sk1),complement(sk3))),
introduced(definition) ).
cnf(t42,plain,
complement(join(complement(sk1),complement(sk3))) = sFlat3,
inference(orient,[status(thm)],[t16]) ).
cnf(t23323,plain,
complement(join(sFlat0,complement(sk3))) = sFlat3,
inference(step,[status(thm)],[t42,t60]) ).
cnf(t67,plain,
complement(join(sFlat0,complement(sk3))) = sFlat3,
inference(rw,[status(thm)],[t23323]) ).
cnf(t23359,plain,
complement(join(sFlat0,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t67,t83]) ).
cnf(t23360,plain,
complement(sFlat2) = sFlat3,
inference(step,[status(thm)],[t23359,t104]) ).
cnf(t168,plain,
complement(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t23360]) ).
cnf(t17,axiom,
sFlat4 = composition(sk2,complement(join(complement(sk1),complement(sk3)))),
introduced(definition) ).
cnf(t23349,plain,
sFlat4 = composition(sk2,complement(join(complement(sk3),complement(sk1)))),
inference(step,[status(thm)],[t17,t90]) ).
cnf(t23350,plain,
sFlat4 = composition(sk2,complement(join(sFlat1,complement(sk1)))),
inference(step,[status(thm)],[t23349,t83]) ).
cnf(t23351,plain,
sFlat4 = composition(sk2,complement(join(sFlat1,sFlat0))),
inference(step,[status(thm)],[t23350,t60]) ).
cnf(t23352,plain,
sFlat4 = composition(sk2,complement(join(sFlat0,sFlat1))),
inference(step,[status(thm)],[t23351,t90]) ).
cnf(t23353,plain,
sFlat4 = composition(sk2,complement(sFlat2)),
inference(step,[status(thm)],[t23352,t104]) ).
cnf(t138,plain,
composition(sk2,complement(sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t23353]) ).
cnf(t23361,plain,
composition(sk2,sFlat3) = sFlat4,
inference(step,[status(thm)],[t138,t168]) ).
cnf(t170,plain,
composition(sk2,sFlat3) = sFlat4,
inference(rw,[status(thm)],[t23361]) ).
cnf(t175,plain,
composition(sk2,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t170]) ).
cnf(t18,axiom,
sFlat5 = complement(sk2),
introduced(definition) ).
cnf(t76,plain,
complement(sk2) = sFlat5,
inference(orient,[status(thm)],[t18]) ).
cnf(t19,axiom,
sFlat6 = converse(sk1),
introduced(definition) ).
cnf(t142,plain,
converse(sk1) = sFlat6,
inference(orient,[status(thm)],[t19]) ).
cnf(t20,axiom,
sFlat7 = complement(converse(sk1)),
introduced(definition) ).
cnf(t68,plain,
complement(converse(sk1)) = sFlat7,
inference(orient,[status(thm)],[t20]) ).
cnf(t23354,plain,
complement(sFlat6) = sFlat7,
inference(step,[status(thm)],[t68,t142]) ).
cnf(t148,plain,
complement(sFlat6) = sFlat7,
inference(rw,[status(thm)],[t23354]) ).
cnf(t156,plain,
complement(sFlat6) = sFlat7,
inference(orient,[status(thm)],[t148]) ).
cnf(t21,axiom,
sFlat8 = join(complement(sk2),complement(converse(sk1))),
introduced(definition) ).
cnf(t23330,plain,
sFlat8 = join(sFlat5,complement(converse(sk1))),
inference(step,[status(thm)],[t21,t76]) ).
cnf(t23331,plain,
sFlat8 = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t23330,t68]) ).
cnf(t106,plain,
join(sFlat5,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t23331]) ).
cnf(t22,axiom,
sFlat9 = complement(join(complement(sk2),complement(converse(sk1)))),
introduced(definition) ).
cnf(t51,plain,
complement(join(complement(sk2),complement(converse(sk1)))) = sFlat9,
inference(orient,[status(thm)],[t22]) ).
cnf(t23324,plain,
complement(join(complement(sk2),sFlat7)) = sFlat9,
inference(step,[status(thm)],[t51,t68]) ).
cnf(t75,plain,
complement(join(complement(sk2),sFlat7)) = sFlat9,
inference(rw,[status(thm)],[t23324]) ).
cnf(t23364,plain,
complement(join(sFlat7,complement(sk2))) = sFlat9,
inference(step,[status(thm)],[t75,t90]) ).
cnf(t23365,plain,
complement(join(sFlat7,sFlat5)) = sFlat9,
inference(step,[status(thm)],[t23364,t76]) ).
cnf(t23366,plain,
complement(join(sFlat5,sFlat7)) = sFlat9,
inference(step,[status(thm)],[t23365,t90]) ).
cnf(t23367,plain,
complement(sFlat8) = sFlat9,
inference(step,[status(thm)],[t23366,t106]) ).
cnf(t183,plain,
complement(sFlat8) = sFlat9,
inference(orient,[status(thm)],[t23367]) ).
cnf(t23,axiom,
sFlat10 = composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
introduced(definition) ).
cnf(t23341,plain,
sFlat10 = composition(complement(join(sFlat5,complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(step,[status(thm)],[t23,t76]) ).
cnf(t23342,plain,
sFlat10 = composition(complement(join(sFlat5,sFlat7)),complement(join(complement(sk1),complement(sk3)))),
inference(step,[status(thm)],[t23341,t68]) ).
cnf(t23343,plain,
sFlat10 = composition(complement(sFlat8),complement(join(complement(sk1),complement(sk3)))),
inference(step,[status(thm)],[t23342,t106]) ).
cnf(t23344,plain,
sFlat10 = composition(complement(sFlat8),complement(join(complement(sk3),complement(sk1)))),
inference(step,[status(thm)],[t23343,t90]) ).
cnf(t23345,plain,
sFlat10 = composition(complement(sFlat8),complement(join(sFlat1,complement(sk1)))),
inference(step,[status(thm)],[t23344,t83]) ).
cnf(t23346,plain,
sFlat10 = composition(complement(sFlat8),complement(join(sFlat1,sFlat0))),
inference(step,[status(thm)],[t23345,t60]) ).
cnf(t23347,plain,
sFlat10 = composition(complement(sFlat8),complement(join(sFlat0,sFlat1))),
inference(step,[status(thm)],[t23346,t90]) ).
cnf(t23348,plain,
sFlat10 = composition(complement(sFlat8),complement(sFlat2)),
inference(step,[status(thm)],[t23347,t104]) ).
cnf(t124,plain,
composition(complement(sFlat8),complement(sFlat2)) = sFlat10,
inference(orient,[status(thm)],[t23348]) ).
cnf(t23362,plain,
composition(complement(sFlat8),sFlat3) = sFlat10,
inference(step,[status(thm)],[t124,t168]) ).
cnf(t171,plain,
composition(complement(sFlat8),sFlat3) = sFlat10,
inference(rw,[status(thm)],[t23362]) ).
cnf(t179,plain,
composition(complement(sFlat8),sFlat3) = sFlat10,
inference(orient,[status(thm)],[t171]) ).
cnf(t23368,plain,
composition(sFlat9,sFlat3) = sFlat10,
inference(step,[status(thm)],[t179,t183]) ).
cnf(t185,plain,
composition(sFlat9,sFlat3) = sFlat10,
inference(rw,[status(thm)],[t23368]) ).
cnf(t188,plain,
composition(sFlat9,sFlat3) = sFlat10,
inference(orient,[status(thm)],[t185]) ).
cnf(t178,plain,
composition(join(X1,sk2),sFlat3) = join(composition(X1,sFlat3),sFlat4),
inference(cp,[status(thm)],[t108,t175]) ).
cnf(t23712,plain,
composition(join(X1,sk2),sFlat3) = join(sFlat4,composition(X1,sFlat3)),
inference(step,[status(thm)],[t178,t90]) ).
cnf(t2228,plain,
composition(join(X1,sk2),sFlat3) = join(sFlat4,composition(X1,sFlat3)),
inference(orient,[status(thm)],[t23712]) ).
cnf(t258,plain,
X1 = join(complement(join(X2,complement(X1))),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t256,t90]) ).
cnf(t19928,plain,
join(complement(join(X1,complement(X2))),complement(join(complement(X2),complement(X1)))) = X2,
inference(orient,[status(thm)],[t258]) ).
cnf(t261,plain,
sFlat6 = join(complement(join(sFlat7,X1)),complement(join(complement(sFlat6),complement(X1)))),
inference(cp,[status(thm)],[t256,t156]) ).
cnf(t24887,plain,
sFlat6 = join(complement(join(sFlat7,X1)),complement(join(sFlat7,complement(X1)))),
inference(step,[status(thm)],[t261,t156]) ).
cnf(t22676,plain,
join(complement(join(sFlat7,X1)),complement(join(sFlat7,complement(X1)))) = sFlat6,
inference(orient,[status(thm)],[t24887]) ).
cnf(t22744,plain,
join(sFlat7,X1) = join(complement(join(join(sFlat7,complement(X1)),complement(join(sFlat7,X1)))),complement(sFlat6)),
inference(cp,[status(thm)],[t19928,t22676]) ).
cnf(t24889,plain,
join(sFlat7,X1) = join(complement(sFlat6),complement(join(join(sFlat7,complement(X1)),complement(join(sFlat7,X1))))),
inference(step,[status(thm)],[t22744,t90]) ).
cnf(t24890,plain,
join(sFlat7,X1) = join(sFlat7,complement(join(join(sFlat7,complement(X1)),complement(join(sFlat7,X1))))),
inference(step,[status(thm)],[t24889,t156]) ).
cnf(t24891,plain,
join(sFlat7,X1) = join(sFlat7,complement(join(sFlat7,join(complement(X1),complement(join(sFlat7,X1)))))),
inference(step,[status(thm)],[t24890,t99]) ).
cnf(t101,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t99,t90]) ).
cnf(t1298,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t101]) ).
cnf(t1311,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t1298,t1220]) ).
cnf(t1791,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(orient,[status(thm)],[t1311]) ).
cnf(t3488,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(cp,[status(thm)],[t3485,t1791]) ).
cnf(t5363,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t3488]) ).
cnf(t5399,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t5363,t1200]) ).
cnf(t6452,plain,
join(complement(X1),complement(join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t5399]) ).
cnf(t24892,plain,
join(sFlat7,X1) = join(sFlat7,complement(join(sFlat7,complement(X1)))),
inference(step,[status(thm)],[t24891,t6452]) ).
cnf(t22790,plain,
join(sFlat7,complement(join(sFlat7,complement(X1)))) = join(sFlat7,X1),
inference(orient,[status(thm)],[t24892]) ).
cnf(t745,plain,
sk2 = join(zero,complement(sFlat5)),
inference(cp,[status(thm)],[t740,t76]) ).
cnf(t756,plain,
join(zero,complement(sFlat5)) = sk2,
inference(orient,[status(thm)],[t745]) ).
cnf(t23593,plain,
complement(sFlat5) = sk2,
inference(step,[status(thm)],[t756,t1127]) ).
cnf(t1138,plain,
complement(sFlat5) = sk2,
inference(rw,[status(thm)],[t23593]) ).
cnf(t1152,plain,
complement(sFlat5) = sk2,
inference(orient,[status(thm)],[t1138]) ).
cnf(t22796,plain,
join(sFlat7,sFlat5) = join(sFlat7,complement(join(sFlat7,sk2))),
inference(cp,[status(thm)],[t22790,t1152]) ).
cnf(t24896,plain,
join(sFlat5,sFlat7) = join(sFlat7,complement(join(sFlat7,sk2))),
inference(step,[status(thm)],[t22796,t90]) ).
cnf(t24897,plain,
sFlat8 = join(sFlat7,complement(join(sFlat7,sk2))),
inference(step,[status(thm)],[t24896,t106]) ).
cnf(t22846,plain,
join(sFlat7,complement(join(sFlat7,sk2))) = sFlat8,
inference(orient,[status(thm)],[t24897]) ).
cnf(t22854,plain,
join(sFlat7,join(sFlat7,sk2)) = join(sFlat7,complement(sFlat8)),
inference(cp,[status(thm)],[t22790,t22846]) ).
cnf(t650,plain,
complement(sFlat6) = join(sFlat7,complement(sFlat6)),
inference(cp,[status(thm)],[t647,t156]) ).
cnf(t23408,plain,
sFlat7 = join(sFlat7,complement(sFlat6)),
inference(step,[status(thm)],[t650,t156]) ).
cnf(t23409,plain,
sFlat7 = join(sFlat7,sFlat7),
inference(step,[status(thm)],[t23408,t156]) ).
cnf(t673,plain,
join(sFlat7,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t23409]) ).
cnf(t678,plain,
join(sFlat7,join(sFlat7,X1)) = join(sFlat7,X1),
inference(cp,[status(thm)],[t99,t673]) ).
cnf(t817,plain,
join(sFlat7,join(sFlat7,X1)) = join(sFlat7,X1),
inference(orient,[status(thm)],[t678]) ).
cnf(t24898,plain,
join(sFlat7,sk2) = join(sFlat7,complement(sFlat8)),
inference(step,[status(thm)],[t22854,t817]) ).
cnf(t24899,plain,
join(sFlat7,sk2) = join(sFlat7,sFlat9),
inference(step,[status(thm)],[t24898,t183]) ).
cnf(t22864,plain,
join(sFlat7,sk2) = join(sFlat7,sFlat9),
inference(orient,[status(thm)],[t24899]) ).
cnf(t22865,plain,
join(sFlat4,composition(sFlat7,sFlat3)) = composition(join(sFlat7,sFlat9),sFlat3),
inference(cp,[status(thm)],[t2228,t22864]) ).
cnf(t191,plain,
composition(join(X1,sFlat9),sFlat3) = join(composition(X1,sFlat3),sFlat10),
inference(cp,[status(thm)],[t108,t188]) ).
cnf(t23731,plain,
composition(join(X1,sFlat9),sFlat3) = join(sFlat10,composition(X1,sFlat3)),
inference(step,[status(thm)],[t191,t90]) ).
cnf(t2565,plain,
composition(join(X1,sFlat9),sFlat3) = join(sFlat10,composition(X1,sFlat3)),
inference(orient,[status(thm)],[t23731]) ).
cnf(t24902,plain,
join(sFlat4,composition(sFlat7,sFlat3)) = join(sFlat10,composition(sFlat7,sFlat3)),
inference(step,[status(thm)],[t22865,t2565]) ).
cnf(t22890,plain,
join(sFlat10,composition(sFlat7,sFlat3)) = join(sFlat4,composition(sFlat7,sFlat3)),
inference(orient,[status(thm)],[t24902]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t128,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t626,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t589,t128]) ).
cnf(t23396,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t626,t149]) ).
cnf(t23397,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t23396,t149]) ).
cnf(t23398,plain,
zero = join(zero,composition(sFlat6,complement(sk1))),
inference(step,[status(thm)],[t23397,t142]) ).
cnf(t23399,plain,
zero = join(zero,composition(sFlat6,sFlat0)),
inference(step,[status(thm)],[t23398,t60]) ).
cnf(t641,plain,
join(zero,composition(sFlat6,sFlat0)) = zero,
inference(orient,[status(thm)],[t23399]) ).
cnf(t23598,plain,
composition(sFlat6,sFlat0) = zero,
inference(step,[status(thm)],[t641,t1127]) ).
cnf(t1143,plain,
composition(sFlat6,sFlat0) = zero,
inference(rw,[status(thm)],[t23598]) ).
cnf(t1195,plain,
composition(sFlat6,sFlat0) = zero,
inference(orient,[status(thm)],[t1143]) ).
cnf(t1198,plain,
composition(join(sFlat6,X1),sFlat0) = join(zero,composition(X1,sFlat0)),
inference(cp,[status(thm)],[t108,t1195]) ).
cnf(t23653,plain,
composition(join(sFlat6,X1),sFlat0) = composition(X1,sFlat0),
inference(step,[status(thm)],[t1198,t1127]) ).
cnf(t1630,plain,
composition(join(sFlat6,X1),sFlat0) = composition(X1,sFlat0),
inference(orient,[status(thm)],[t23653]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t114,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t147,plain,
converse(join(X1,sk1)) = join(converse(X1),sFlat6),
inference(cp,[status(thm)],[t114,t142]) ).
cnf(t23372,plain,
converse(join(X1,sk1)) = join(sFlat6,converse(X1)),
inference(step,[status(thm)],[t147,t90]) ).
cnf(t224,plain,
converse(join(X1,sk1)) = join(sFlat6,converse(X1)),
inference(orient,[status(thm)],[t23372]) ).
cnf(t3505,plain,
sk1 = join(sk1,complement(join(sFlat0,X1))),
inference(cp,[status(thm)],[t3485,t60]) ).
cnf(t3935,plain,
join(sk1,complement(join(sFlat0,X1))) = sk1,
inference(orient,[status(thm)],[t3505]) ).
cnf(t742,plain,
sFlat2 = join(zero,complement(sFlat3)),
inference(cp,[status(thm)],[t740,t168]) ).
cnf(t750,plain,
join(zero,complement(sFlat3)) = sFlat2,
inference(orient,[status(thm)],[t742]) ).
cnf(t23596,plain,
complement(sFlat3) = sFlat2,
inference(step,[status(thm)],[t750,t1127]) ).
cnf(t1141,plain,
complement(sFlat3) = sFlat2,
inference(rw,[status(thm)],[t23596]) ).
cnf(t1173,plain,
complement(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t1141]) ).
cnf(t1174,plain,
complement(sFlat3) = join(sFlat2,complement(sFlat3)),
inference(cp,[status(thm)],[t647,t1173]) ).
cnf(t23605,plain,
sFlat2 = join(sFlat2,complement(sFlat3)),
inference(step,[status(thm)],[t1174,t1173]) ).
cnf(t23606,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t23605,t1173]) ).
cnf(t105,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t99,t104]) ).
cnf(t295,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t105]) ).
cnf(t298,plain,
join(sFlat2,X1) = join(sFlat0,join(X1,sFlat1)),
inference(cp,[status(thm)],[t295,t90]) ).
cnf(t356,plain,
join(sFlat0,join(X1,sFlat1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t298]) ).
cnf(t652,plain,
complement(sk3) = join(sFlat1,complement(sk3)),
inference(cp,[status(thm)],[t647,t83]) ).
cnf(t23412,plain,
sFlat1 = join(sFlat1,complement(sk3)),
inference(step,[status(thm)],[t652,t83]) ).
cnf(t23413,plain,
sFlat1 = join(sFlat1,sFlat1),
inference(step,[status(thm)],[t23412,t83]) ).
cnf(t681,plain,
join(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t23413]) ).
cnf(t682,plain,
join(sFlat2,sFlat1) = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t356,t681]) ).
cnf(t23428,plain,
join(sFlat1,sFlat2) = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t682,t90]) ).
cnf(t23429,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t23428,t104]) ).
cnf(t708,plain,
join(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t23429]) ).
cnf(t709,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t295,t708]) ).
cnf(t738,plain,
join(sFlat2,sFlat2) = join(sFlat0,sFlat2),
inference(orient,[status(thm)],[t709]) ).
cnf(t23607,plain,
sFlat2 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t23606,t738]) ).
cnf(t1212,plain,
join(sFlat0,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t23607]) ).
cnf(t3938,plain,
sk1 = join(sk1,complement(sFlat2)),
inference(cp,[status(thm)],[t3935,t1212]) ).
cnf(t23853,plain,
sk1 = join(sk1,sFlat3),
inference(step,[status(thm)],[t3938,t168]) ).
cnf(t23854,plain,
sk1 = join(sFlat3,sk1),
inference(step,[status(thm)],[t23853,t90]) ).
cnf(t3954,plain,
join(sFlat3,sk1) = sk1,
inference(orient,[status(thm)],[t23854]) ).
cnf(t3956,plain,
join(sFlat6,converse(sFlat3)) = converse(sk1),
inference(cp,[status(thm)],[t224,t3954]) ).
cnf(t23855,plain,
join(sFlat6,converse(sFlat3)) = sFlat6,
inference(step,[status(thm)],[t3956,t142]) ).
cnf(t3962,plain,
join(sFlat6,converse(sFlat3)) = sFlat6,
inference(orient,[status(thm)],[t23855]) ).
cnf(t3964,plain,
composition(converse(sFlat3),sFlat0) = composition(sFlat6,sFlat0),
inference(cp,[status(thm)],[t1630,t3962]) ).
cnf(t23856,plain,
composition(converse(sFlat3),sFlat0) = zero,
inference(step,[status(thm)],[t3964,t1195]) ).
cnf(t3971,plain,
composition(converse(sFlat3),sFlat0) = zero,
inference(orient,[status(thm)],[t23856]) ).
cnf(t3976,plain,
composition(converse(sFlat0),sFlat3) = converse(zero),
inference(cp,[status(thm)],[t495,t3971]) ).
cnf(t116,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t114,t29]) ).
cnf(t429,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t116]) ).
cnf(t432,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t429,t93]) ).
cnf(t560,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t432]) ).
cnf(t100,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(cp,[status(thm)],[t99,t93]) ).
cnf(t854,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t100]) ).
cnf(t885,plain,
top = join(complement(X1),join(complement(X1),complement(complement(X1)))),
inference(cp,[status(thm)],[t854,t647]) ).
cnf(t23529,plain,
top = join(complement(X1),top),
inference(step,[status(thm)],[t885,t93]) ).
cnf(t23530,plain,
top = join(top,complement(X1)),
inference(step,[status(thm)],[t23529,t90]) ).
cnf(t982,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t23530]) ).
cnf(t991,plain,
top = join(X1,top),
inference(cp,[status(thm)],[t854,t982]) ).
cnf(t993,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t991]) ).
cnf(t994,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t993,t90]) ).
cnf(t1002,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t994]) ).
cnf(t1035,plain,
top = converse(top),
inference(cp,[status(thm)],[t1002,t560]) ).
cnf(t1041,plain,
converse(top) = top,
inference(orient,[status(thm)],[t1035]) ).
cnf(t23572,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t560,t1041]) ).
cnf(t1048,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t23572]) ).
cnf(t1129,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t1127,t1048]) ).
cnf(t1233,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t1129]) ).
cnf(t1234,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t29,t1233]) ).
cnf(t23619,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t1234,t1041]) ).
cnf(t1245,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t23619]) ).
cnf(t1246,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t1200,t1245]) ).
cnf(t23620,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t1246,t149]) ).
cnf(t1250,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t23620]) ).
cnf(t23857,plain,
composition(converse(sFlat0),sFlat3) = zero,
inference(step,[status(thm)],[t3976,t1250]) ).
cnf(t3978,plain,
composition(converse(sFlat0),sFlat3) = zero,
inference(orient,[status(thm)],[t23857]) ).
cnf(t3980,plain,
composition(join(converse(sFlat0),X1),sFlat3) = join(zero,composition(X1,sFlat3)),
inference(cp,[status(thm)],[t108,t3978]) ).
cnf(t23896,plain,
composition(join(converse(sFlat0),X1),sFlat3) = composition(X1,sFlat3),
inference(step,[status(thm)],[t3980,t1127]) ).
cnf(t4739,plain,
composition(join(converse(sFlat0),X1),sFlat3) = composition(X1,sFlat3),
inference(orient,[status(thm)],[t23896]) ).
cnf(t4740,plain,
composition(converse(X1),sFlat3) = composition(converse(join(sFlat0,X1)),sFlat3),
inference(cp,[status(thm)],[t4739,t114]) ).
cnf(t6231,plain,
composition(converse(join(sFlat0,X1)),sFlat3) = composition(converse(X1),sFlat3),
inference(orient,[status(thm)],[t4740]) ).
cnf(t746,plain,
sk1 = join(zero,complement(sFlat0)),
inference(cp,[status(thm)],[t740,t60]) ).
cnf(t758,plain,
join(zero,complement(sFlat0)) = sk1,
inference(orient,[status(thm)],[t746]) ).
cnf(t23592,plain,
complement(sFlat0) = sk1,
inference(step,[status(thm)],[t758,t1127]) ).
cnf(t1137,plain,
complement(sFlat0) = sk1,
inference(rw,[status(thm)],[t23592]) ).
cnf(t1147,plain,
complement(sFlat0) = sk1,
inference(orient,[status(thm)],[t1137]) ).
cnf(t3499,plain,
sFlat0 = join(sFlat0,complement(join(sk1,X1))),
inference(cp,[status(thm)],[t3485,t1147]) ).
cnf(t3593,plain,
join(sFlat0,complement(join(sk1,X1))) = sFlat0,
inference(orient,[status(thm)],[t3499]) ).
cnf(t6234,plain,
composition(converse(complement(join(sk1,X1))),sFlat3) = composition(converse(sFlat0),sFlat3),
inference(cp,[status(thm)],[t6231,t3593]) ).
cnf(t24007,plain,
composition(converse(complement(join(sk1,X1))),sFlat3) = zero,
inference(step,[status(thm)],[t6234,t3978]) ).
cnf(t6270,plain,
composition(converse(complement(join(sk1,X1))),sFlat3) = zero,
inference(orient,[status(thm)],[t24007]) ).
cnf(t143,plain,
sk1 = converse(sFlat6),
inference(cp,[status(thm)],[t29,t142]) ).
cnf(t151,plain,
converse(sFlat6) = sk1,
inference(orient,[status(thm)],[t143]) ).
cnf(t154,plain,
converse(join(sFlat6,X1)) = join(sk1,converse(X1)),
inference(cp,[status(thm)],[t114,t151]) ).
cnf(t247,plain,
converse(join(sFlat6,X1)) = join(sk1,converse(X1)),
inference(orient,[status(thm)],[t154]) ).
cnf(t22793,plain,
join(sFlat7,complement(X1)) = join(sFlat7,complement(join(sFlat7,X1))),
inference(cp,[status(thm)],[t22790,t1200]) ).
cnf(t23079,plain,
join(sFlat7,complement(join(sFlat7,X1))) = join(sFlat7,complement(X1)),
inference(orient,[status(thm)],[t22793]) ).
cnf(t23107,plain,
join(sFlat7,complement(converse(complement(converse(sFlat7))))) = join(sFlat7,complement(top)),
inference(cp,[status(thm)],[t23079,t1048]) ).
cnf(t24923,plain,
join(sFlat7,complement(converse(complement(converse(sFlat7))))) = join(sFlat7,zero),
inference(step,[status(thm)],[t23107,t149]) ).
cnf(t1130,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t1127,t90]) ).
cnf(t1189,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t1130]) ).
cnf(t24924,plain,
join(sFlat7,complement(converse(complement(converse(sFlat7))))) = sFlat7,
inference(step,[status(thm)],[t24923,t1189]) ).
cnf(t23127,plain,
join(sFlat7,complement(converse(complement(converse(sFlat7))))) = sFlat7,
inference(orient,[status(thm)],[t24924]) ).
cnf(t23134,plain,
complement(complement(converse(complement(converse(sFlat7))))) = join(complement(complement(converse(complement(converse(sFlat7))))),complement(sFlat7)),
inference(cp,[status(thm)],[t6452,t23127]) ).
cnf(t24934,plain,
converse(complement(converse(sFlat7))) = join(complement(complement(converse(complement(converse(sFlat7))))),complement(sFlat7)),
inference(step,[status(thm)],[t23134,t1200]) ).
cnf(t24935,plain,
converse(complement(converse(sFlat7))) = join(complement(sFlat7),complement(complement(converse(complement(converse(sFlat7)))))),
inference(step,[status(thm)],[t24934,t90]) ).
cnf(t743,plain,
sFlat6 = join(zero,complement(sFlat7)),
inference(cp,[status(thm)],[t740,t156]) ).
cnf(t752,plain,
join(zero,complement(sFlat7)) = sFlat6,
inference(orient,[status(thm)],[t743]) ).
cnf(t23595,plain,
complement(sFlat7) = sFlat6,
inference(step,[status(thm)],[t752,t1127]) ).
cnf(t1140,plain,
complement(sFlat7) = sFlat6,
inference(rw,[status(thm)],[t23595]) ).
cnf(t1166,plain,
complement(sFlat7) = sFlat6,
inference(orient,[status(thm)],[t1140]) ).
cnf(t24936,plain,
converse(complement(converse(sFlat7))) = join(sFlat6,complement(complement(converse(complement(converse(sFlat7)))))),
inference(step,[status(thm)],[t24935,t1166]) ).
cnf(t24937,plain,
converse(complement(converse(sFlat7))) = join(sFlat6,converse(complement(converse(sFlat7)))),
inference(step,[status(thm)],[t24936,t1200]) ).
cnf(t23227,plain,
join(sFlat6,converse(complement(converse(sFlat7)))) = converse(complement(converse(sFlat7))),
inference(orient,[status(thm)],[t24937]) ).
cnf(t23233,plain,
join(sk1,converse(converse(complement(converse(sFlat7))))) = converse(converse(complement(converse(sFlat7)))),
inference(cp,[status(thm)],[t247,t23227]) ).
cnf(t24941,plain,
join(sk1,complement(converse(sFlat7))) = converse(converse(complement(converse(sFlat7)))),
inference(step,[status(thm)],[t23233,t29]) ).
cnf(t24942,plain,
join(sk1,complement(converse(sFlat7))) = complement(converse(sFlat7)),
inference(step,[status(thm)],[t24941,t29]) ).
cnf(t23271,plain,
join(sk1,complement(converse(sFlat7))) = complement(converse(sFlat7)),
inference(orient,[status(thm)],[t24942]) ).
cnf(t23299,plain,
zero = composition(converse(complement(complement(converse(sFlat7)))),sFlat3),
inference(cp,[status(thm)],[t6270,t23271]) ).
cnf(t24943,plain,
zero = composition(converse(converse(sFlat7)),sFlat3),
inference(step,[status(thm)],[t23299,t1200]) ).
cnf(t24944,plain,
zero = composition(sFlat7,sFlat3),
inference(step,[status(thm)],[t24943,t29]) ).
cnf(t23304,plain,
composition(sFlat7,sFlat3) = zero,
inference(orient,[status(thm)],[t24944]) ).
cnf(t24945,plain,
join(sFlat10,zero) = join(sFlat4,composition(sFlat7,sFlat3)),
inference(step,[status(thm)],[t22890,t23304]) ).
cnf(t24946,plain,
sFlat10 = join(sFlat4,composition(sFlat7,sFlat3)),
inference(step,[status(thm)],[t24945,t1189]) ).
cnf(t24947,plain,
sFlat10 = join(sFlat4,zero),
inference(step,[status(thm)],[t24946,t23304]) ).
cnf(t24948,plain,
sFlat10 = sFlat4,
inference(step,[status(thm)],[t24947,t1189]) ).
cnf(t23309,plain,
sFlat10 = sFlat4,
inference(rw,[status(thm)],[t24948]) ).
cnf(t23310,plain,
sFlat10 = sFlat4,
inference(orient,[status(thm)],[t23309]) ).
cnf(t24949,plain,
composition(sFlat9,sFlat3) = sFlat4,
inference(step,[status(thm)],[t188,t23310]) ).
cnf(t23311,plain,
composition(sFlat9,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t24949]) ).
cnf(u1,negated_conjecture,
join(composition(sk2,meet(sk1,sk3)),composition(meet(sk2,converse(sk1)),meet(sk1,sk3))) != composition(meet(sk2,converse(sk1)),meet(sk1,sk3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
join(composition(sk2,complement(join(complement(sk1),complement(sk3)))),composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3))))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(g0_0,plain,
composition(join(sk2,complement(join(complement(sk2),complement(converse(sk1))))),complement(join(complement(sk1),complement(sk3)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[goal_0,t108]) ).
cnf(g0_1,plain,
composition(sk2,complement(join(complement(sk1),complement(sk3)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_0,t3485]) ).
cnf(g0_2,plain,
composition(sk2,complement(join(complement(sk3),complement(sk1)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_1,t90]) ).
cnf(g0_3,plain,
composition(sk2,complement(join(sFlat1,complement(sk1)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_2,t83]) ).
cnf(g0_4,plain,
composition(sk2,complement(join(sFlat1,sFlat0))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_3,t60]) ).
cnf(g0_5,plain,
composition(sk2,complement(join(sFlat0,sFlat1))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_4,t90]) ).
cnf(g0_6,plain,
composition(sk2,complement(sFlat2)) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_5,t104]) ).
cnf(g0_7,plain,
composition(sk2,sFlat3) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_6,t168]) ).
cnf(g0_8,plain,
sFlat4 != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_7,t175]) ).
cnf(g0_9,plain,
sFlat4 != composition(complement(join(sFlat5,complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_8,t76]) ).
cnf(g0_10,plain,
sFlat4 != composition(complement(join(sFlat5,complement(sFlat6))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_9,t142]) ).
cnf(g0_11,plain,
sFlat4 != composition(complement(join(sFlat5,sFlat7)),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_10,t156]) ).
cnf(g0_12,plain,
sFlat4 != composition(complement(sFlat8),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_11,t106]) ).
cnf(g0_13,plain,
sFlat4 != composition(sFlat9,complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_12,t183]) ).
cnf(g0_14,plain,
sFlat4 != composition(sFlat9,complement(join(complement(sk3),complement(sk1)))),
inference(rw,[status(thm)],[g0_13,t90]) ).
cnf(g0_15,plain,
sFlat4 != composition(sFlat9,complement(join(sFlat1,complement(sk1)))),
inference(rw,[status(thm)],[g0_14,t83]) ).
cnf(g0_16,plain,
sFlat4 != composition(sFlat9,complement(join(sFlat1,sFlat0))),
inference(rw,[status(thm)],[g0_15,t60]) ).
cnf(g0_17,plain,
sFlat4 != composition(sFlat9,complement(join(sFlat0,sFlat1))),
inference(rw,[status(thm)],[g0_16,t90]) ).
cnf(g0_18,plain,
sFlat4 != composition(sFlat9,complement(sFlat2)),
inference(rw,[status(thm)],[g0_17,t104]) ).
cnf(g0_19,plain,
sFlat4 != composition(sFlat9,sFlat3),
inference(rw,[status(thm)],[g0_18,t168]) ).
cnf(g0_20,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_19,t23311]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL034-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.43 % Computer : n011.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Thu Sep 24 07:29:43 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 11.93/8.51 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.93/8.51 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------