%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL036-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 : n016.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:58 PM UTC 2026
% Result : Unsatisfiable 103.22s 23.67s
% Output : CNFRefutation 103.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 76
% Number of leaves : 25
% Syntax : Number of clauses : 293 ( 293 unt; 0 nHn; 167 RR)
% Number of literals : 293 ( 292 equ; 33 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 : 183 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t13,axiom,
sFlat0 = complement(sk2),
introduced(definition) ).
cnf(t76,plain,
complement(sk2) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat1 = converse(sk1),
introduced(definition) ).
cnf(t123,plain,
converse(sk1) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat2 = complement(converse(sk1)),
introduced(definition) ).
cnf(t60,plain,
complement(converse(sk1)) = sFlat2,
inference(orient,[status(thm)],[t15]) ).
cnf(t35409,plain,
complement(sFlat1) = sFlat2,
inference(step,[status(thm)],[t60,t123]) ).
cnf(t129,plain,
complement(sFlat1) = sFlat2,
inference(rw,[status(thm)],[t35409]) ).
cnf(t154,plain,
complement(sFlat1) = sFlat2,
inference(orient,[status(thm)],[t129]) ).
cnf(t16,axiom,
sFlat3 = join(complement(sk2),complement(converse(sk1))),
introduced(definition) ).
cnf(t35396,plain,
sFlat3 = join(sFlat0,complement(converse(sk1))),
inference(step,[status(thm)],[t16,t76]) ).
cnf(t35397,plain,
sFlat3 = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t35396,t60]) ).
cnf(t106,plain,
join(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t35397]) ).
cnf(t17,axiom,
sFlat4 = complement(join(complement(sk2),complement(converse(sk1)))),
introduced(definition) ).
cnf(t51,plain,
complement(join(complement(sk2),complement(converse(sk1)))) = sFlat4,
inference(orient,[status(thm)],[t17]) ).
cnf(t35389,plain,
complement(join(complement(sk2),sFlat2)) = sFlat4,
inference(step,[status(thm)],[t51,t60]) ).
cnf(t67,plain,
complement(join(complement(sk2),sFlat2)) = sFlat4,
inference(rw,[status(thm)],[t35389]) ).
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(t35428,plain,
complement(join(sFlat2,complement(sk2))) = sFlat4,
inference(step,[status(thm)],[t67,t90]) ).
cnf(t35429,plain,
complement(join(sFlat2,sFlat0)) = sFlat4,
inference(step,[status(thm)],[t35428,t76]) ).
cnf(t35430,plain,
complement(join(sFlat0,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t35429,t90]) ).
cnf(t35431,plain,
complement(sFlat3) = sFlat4,
inference(step,[status(thm)],[t35430,t106]) ).
cnf(t173,plain,
complement(sFlat3) = sFlat4,
inference(orient,[status(thm)],[t35431]) ).
cnf(t18,axiom,
sFlat5 = composition(complement(join(complement(sk2),complement(converse(sk1)))),sk3),
introduced(definition) ).
cnf(t35417,plain,
sFlat5 = composition(complement(join(sFlat0,complement(converse(sk1)))),sk3),
inference(step,[status(thm)],[t18,t76]) ).
cnf(t35418,plain,
sFlat5 = composition(complement(join(sFlat0,complement(sFlat1))),sk3),
inference(step,[status(thm)],[t35417,t123]) ).
cnf(t139,plain,
composition(complement(join(sFlat0,complement(sFlat1))),sk3) = sFlat5,
inference(orient,[status(thm)],[t35418]) ).
cnf(t35421,plain,
composition(complement(join(sFlat0,sFlat2)),sk3) = sFlat5,
inference(step,[status(thm)],[t139,t154]) ).
cnf(t35422,plain,
composition(complement(sFlat3),sk3) = sFlat5,
inference(step,[status(thm)],[t35421,t106]) ).
cnf(t157,plain,
composition(complement(sFlat3),sk3) = sFlat5,
inference(rw,[status(thm)],[t35422]) ).
cnf(t168,plain,
composition(complement(sFlat3),sk3) = sFlat5,
inference(orient,[status(thm)],[t157]) ).
cnf(t35432,plain,
composition(sFlat4,sk3) = sFlat5,
inference(step,[status(thm)],[t168,t173]) ).
cnf(t175,plain,
composition(sFlat4,sk3) = sFlat5,
inference(rw,[status(thm)],[t35432]) ).
cnf(t178,plain,
composition(sFlat4,sk3) = sFlat5,
inference(orient,[status(thm)],[t175]) ).
cnf(t20,axiom,
sFlat7 = complement(sk3),
introduced(definition) ).
cnf(t83,plain,
complement(sk3) = sFlat7,
inference(orient,[status(thm)],[t20]) ).
cnf(t19,axiom,
sFlat6 = complement(sk1),
introduced(definition) ).
cnf(t68,plain,
complement(sk1) = sFlat6,
inference(orient,[status(thm)],[t19]) ).
cnf(t21,axiom,
sFlat8 = join(complement(sk1),complement(sk3)),
introduced(definition) ).
cnf(t35392,plain,
sFlat8 = join(complement(sk3),complement(sk1)),
inference(step,[status(thm)],[t21,t90]) ).
cnf(t35393,plain,
sFlat8 = join(sFlat7,complement(sk1)),
inference(step,[status(thm)],[t35392,t83]) ).
cnf(t35394,plain,
sFlat8 = join(sFlat7,sFlat6),
inference(step,[status(thm)],[t35393,t68]) ).
cnf(t35395,plain,
sFlat8 = join(sFlat6,sFlat7),
inference(step,[status(thm)],[t35394,t90]) ).
cnf(t104,plain,
join(sFlat6,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t35395]) ).
cnf(t22,axiom,
sFlat9 = complement(join(complement(sk1),complement(sk3))),
introduced(definition) ).
cnf(t42,plain,
complement(join(complement(sk1),complement(sk3))) = sFlat9,
inference(orient,[status(thm)],[t22]) ).
cnf(t35390,plain,
complement(join(sFlat6,complement(sk3))) = sFlat9,
inference(step,[status(thm)],[t42,t68]) ).
cnf(t75,plain,
complement(join(sFlat6,complement(sk3))) = sFlat9,
inference(rw,[status(thm)],[t35390]) ).
cnf(t35433,plain,
complement(join(sFlat6,sFlat7)) = sFlat9,
inference(step,[status(thm)],[t75,t83]) ).
cnf(t35434,plain,
complement(sFlat8) = sFlat9,
inference(step,[status(thm)],[t35433,t104]) ).
cnf(t182,plain,
complement(sFlat8) = sFlat9,
inference(orient,[status(thm)],[t35434]) ).
cnf(t23,axiom,
sFlat10 = composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
introduced(definition) ).
cnf(t35410,plain,
sFlat10 = composition(complement(join(sFlat0,complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(step,[status(thm)],[t23,t76]) ).
cnf(t35411,plain,
sFlat10 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(complement(sk1),complement(sk3)))),
inference(step,[status(thm)],[t35410,t123]) ).
cnf(t35412,plain,
sFlat10 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(complement(sk3),complement(sk1)))),
inference(step,[status(thm)],[t35411,t90]) ).
cnf(t35413,plain,
sFlat10 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(sFlat7,complement(sk1)))),
inference(step,[status(thm)],[t35412,t83]) ).
cnf(t35414,plain,
sFlat10 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(sFlat7,sFlat6))),
inference(step,[status(thm)],[t35413,t68]) ).
cnf(t35415,plain,
sFlat10 = composition(complement(join(sFlat0,complement(sFlat1))),complement(join(sFlat6,sFlat7))),
inference(step,[status(thm)],[t35414,t90]) ).
cnf(t35416,plain,
sFlat10 = composition(complement(join(sFlat0,complement(sFlat1))),complement(sFlat8)),
inference(step,[status(thm)],[t35415,t104]) ).
cnf(t135,plain,
composition(complement(join(sFlat0,complement(sFlat1))),complement(sFlat8)) = sFlat10,
inference(orient,[status(thm)],[t35416]) ).
cnf(t35419,plain,
composition(complement(join(sFlat0,sFlat2)),complement(sFlat8)) = sFlat10,
inference(step,[status(thm)],[t135,t154]) ).
cnf(t35420,plain,
composition(complement(sFlat3),complement(sFlat8)) = sFlat10,
inference(step,[status(thm)],[t35419,t106]) ).
cnf(t156,plain,
composition(complement(sFlat3),complement(sFlat8)) = sFlat10,
inference(rw,[status(thm)],[t35420]) ).
cnf(t35435,plain,
composition(sFlat4,complement(sFlat8)) = sFlat10,
inference(step,[status(thm)],[t156,t173]) ).
cnf(t35436,plain,
composition(sFlat4,sFlat9) = sFlat10,
inference(step,[status(thm)],[t35435,t182]) ).
cnf(t186,plain,
composition(sFlat4,sFlat9) = sFlat10,
inference(orient,[status(thm)],[t35436]) ).
cnf(t2,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t10,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t113,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t6,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t118,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t121,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t113,t118]) ).
cnf(t4496,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t121]) ).
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(t35455,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t92,t90]) ).
cnf(t586,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t35455]) ).
cnf(t1,axiom,
composition(sk1,top) = sk1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t143,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t1]) ).
cnf(t620,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t586,t143]) ).
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(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(t35391,plain,
complement(top) = zero,
inference(step,[status(thm)],[t33,t93]) ).
cnf(t98,plain,
complement(top) = zero,
inference(rw,[status(thm)],[t35391]) ).
cnf(t147,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t98]) ).
cnf(t35458,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t620,t147]) ).
cnf(t35459,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t35458,t147]) ).
cnf(t35460,plain,
zero = join(zero,composition(sFlat1,complement(sk1))),
inference(step,[status(thm)],[t35459,t123]) ).
cnf(t35461,plain,
zero = join(zero,composition(sFlat1,sFlat6)),
inference(step,[status(thm)],[t35460,t68]) ).
cnf(t630,plain,
join(zero,composition(sFlat1,sFlat6)) = zero,
inference(orient,[status(thm)],[t35461]) ).
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(t120,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t118,t28]) ).
cnf(t489,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t120]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t490,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t489,t29]) ).
cnf(t35451,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t490,t28]) ).
cnf(t509,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t35451]) ).
cnf(t510,plain,
one = converse(one),
inference(cp,[status(thm)],[t509,t29]) ).
cnf(t514,plain,
converse(one) = one,
inference(orient,[status(thm)],[t510]) ).
cnf(t596,plain,
complement(X1) = join(complement(X1),composition(one,complement(composition(one,X1)))),
inference(cp,[status(thm)],[t586,t514]) ).
cnf(t35452,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t509,t514]) ).
cnf(t523,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t35452]) ).
cnf(t524,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t523]) ).
cnf(t35468,plain,
complement(X1) = join(complement(X1),complement(composition(one,X1))),
inference(step,[status(thm)],[t596,t524]) ).
cnf(t35469,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t35468,t524]) ).
cnf(t640,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t35469]) ).
cnf(t644,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t640,t147]) ).
cnf(t35476,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t644,t147]) ).
cnf(t35477,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t35476,t147]) ).
cnf(t672,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t35477]) ).
cnf(t673,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t99,t672]) ).
cnf(t860,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t673]) ).
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(t35442,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t91,t90]) ).
cnf(t254,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t35442]) ).
cnf(t656,plain,
X1 = join(complement(complement(X1)),complement(join(complement(X1),complement(complement(X1))))),
inference(cp,[status(thm)],[t254,t640]) ).
cnf(t35529,plain,
X1 = join(complement(complement(X1)),complement(top)),
inference(step,[status(thm)],[t656,t93]) ).
cnf(t35530,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t35529,t147]) ).
cnf(t35531,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t35530,t90]) ).
cnf(t752,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t35531]) ).
cnf(t867,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t860,t752]) ).
cnf(t35594,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t867,t752]) ).
cnf(t978,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t35594]) ).
cnf(t35601,plain,
composition(sFlat1,sFlat6) = zero,
inference(step,[status(thm)],[t630,t978]) ).
cnf(t1000,plain,
composition(sFlat1,sFlat6) = zero,
inference(rw,[status(thm)],[t35601]) ).
cnf(t1090,plain,
composition(sFlat1,sFlat6) = zero,
inference(orient,[status(thm)],[t1000]) ).
cnf(t1093,plain,
composition(join(sFlat1,X1),sFlat6) = join(zero,composition(X1,sFlat6)),
inference(cp,[status(thm)],[t113,t1090]) ).
cnf(t35730,plain,
composition(join(sFlat1,X1),sFlat6) = composition(X1,sFlat6),
inference(step,[status(thm)],[t1093,t978]) ).
cnf(t1612,plain,
composition(join(sFlat1,X1),sFlat6) = composition(X1,sFlat6),
inference(orient,[status(thm)],[t35730]) ).
cnf(t35603,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t752,t978]) ).
cnf(t1002,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t35603]) ).
cnf(t1096,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t1002]) ).
cnf(t1097,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t640,t1096]) ).
cnf(t35647,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t1097,t1096]) ).
cnf(t35648,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t35647,t1096]) ).
cnf(t1131,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t35648]) ).
cnf(t1149,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t99,t1131]) ).
cnf(t1758,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t1149]) ).
cnf(t1765,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = join(complement(join(complement(X1),X2)),X1),
inference(cp,[status(thm)],[t1758,t254]) ).
cnf(t35913,plain,
X1 = join(complement(join(complement(X1),X2)),X1),
inference(step,[status(thm)],[t1765,t254]) ).
cnf(t35914,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(step,[status(thm)],[t35913,t90]) ).
cnf(t3509,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t35914]) ).
cnf(t3526,plain,
sFlat1 = join(sFlat1,complement(join(sFlat2,X1))),
inference(cp,[status(thm)],[t3509,t154]) ).
cnf(t3662,plain,
join(sFlat1,complement(join(sFlat2,X1))) = sFlat1,
inference(orient,[status(thm)],[t3526]) ).
cnf(t107,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t99,t106]) ).
cnf(t301,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t107]) ).
cnf(t303,plain,
join(sFlat3,X1) = join(sFlat0,join(X1,sFlat2)),
inference(cp,[status(thm)],[t301,t90]) ).
cnf(t368,plain,
join(sFlat0,join(X1,sFlat2)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t303]) ).
cnf(t643,plain,
complement(sFlat1) = join(sFlat2,complement(sFlat1)),
inference(cp,[status(thm)],[t640,t154]) ).
cnf(t35474,plain,
sFlat2 = join(sFlat2,complement(sFlat1)),
inference(step,[status(thm)],[t643,t154]) ).
cnf(t35475,plain,
sFlat2 = join(sFlat2,sFlat2),
inference(step,[status(thm)],[t35474,t154]) ).
cnf(t666,plain,
join(sFlat2,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t35475]) ).
cnf(t668,plain,
join(sFlat3,sFlat2) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t368,t666]) ).
cnf(t35492,plain,
join(sFlat2,sFlat3) = join(sFlat0,sFlat2),
inference(step,[status(thm)],[t668,t90]) ).
cnf(t35493,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(step,[status(thm)],[t35492,t106]) ).
cnf(t697,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t35493]) ).
cnf(t3665,plain,
sFlat1 = join(sFlat1,complement(sFlat3)),
inference(cp,[status(thm)],[t3662,t697]) ).
cnf(t35915,plain,
sFlat1 = join(sFlat1,sFlat4),
inference(step,[status(thm)],[t3665,t173]) ).
cnf(t3680,plain,
join(sFlat1,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t35915]) ).
cnf(t3684,plain,
composition(sFlat4,sFlat6) = composition(sFlat1,sFlat6),
inference(cp,[status(thm)],[t1612,t3680]) ).
cnf(t35916,plain,
composition(sFlat4,sFlat6) = zero,
inference(step,[status(thm)],[t3684,t1090]) ).
cnf(t3692,plain,
composition(sFlat4,sFlat6) = zero,
inference(orient,[status(thm)],[t35916]) ).
cnf(t4544,plain,
composition(join(converse(sFlat6),X1),converse(sFlat4)) = join(converse(zero),composition(X1,converse(sFlat4))),
inference(cp,[status(thm)],[t4496,t3692]) ).
cnf(t7,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t108,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t7]) ).
cnf(t111,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t108,t28]) ).
cnf(t441,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t111]) ).
cnf(t992,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t441,t978]) ).
cnf(t35709,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t992,t28]) ).
cnf(t1237,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t35709]) ).
cnf(t36934,plain,
composition(join(converse(sFlat6),X1),converse(sFlat4)) = composition(X1,converse(sFlat4)),
inference(step,[status(thm)],[t4544,t1237]) ).
cnf(t23977,plain,
composition(join(converse(sFlat6),X1),converse(sFlat4)) = composition(X1,converse(sFlat4)),
inference(orient,[status(thm)],[t36934]) ).
cnf(t23990,plain,
composition(converse(X1),converse(sFlat4)) = composition(converse(join(sFlat6,X1)),converse(sFlat4)),
inference(cp,[status(thm)],[t23977,t108]) ).
cnf(t36954,plain,
converse(composition(sFlat4,X1)) = composition(converse(join(sFlat6,X1)),converse(sFlat4)),
inference(step,[status(thm)],[t23990,t118]) ).
cnf(t36955,plain,
converse(composition(sFlat4,X1)) = converse(composition(sFlat4,join(sFlat6,X1))),
inference(step,[status(thm)],[t36954,t118]) ).
cnf(t24114,plain,
converse(composition(sFlat4,join(sFlat6,X1))) = converse(composition(sFlat4,X1)),
inference(orient,[status(thm)],[t36955]) ).
cnf(t24179,plain,
composition(sFlat4,join(sFlat6,X1)) = converse(converse(composition(sFlat4,X1))),
inference(cp,[status(thm)],[t28,t24114]) ).
cnf(t36957,plain,
composition(sFlat4,join(sFlat6,X1)) = composition(sFlat4,X1),
inference(step,[status(thm)],[t24179,t28]) ).
cnf(t24293,plain,
composition(sFlat4,join(sFlat6,X1)) = composition(sFlat4,X1),
inference(orient,[status(thm)],[t36957]) ).
cnf(t256,plain,
X1 = join(complement(join(X2,complement(X1))),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t254,t90]) ).
cnf(t26870,plain,
join(complement(join(X1,complement(X2))),complement(join(complement(X2),complement(X1)))) = X2,
inference(orient,[status(thm)],[t256]) ).
cnf(t257,plain,
sFlat8 = join(complement(join(sFlat9,X1)),complement(join(complement(sFlat8),complement(X1)))),
inference(cp,[status(thm)],[t254,t182]) ).
cnf(t37118,plain,
sFlat8 = join(complement(join(sFlat9,X1)),complement(join(sFlat9,complement(X1)))),
inference(step,[status(thm)],[t257,t182]) ).
cnf(t29232,plain,
join(complement(join(sFlat9,X1)),complement(join(sFlat9,complement(X1)))) = sFlat8,
inference(orient,[status(thm)],[t37118]) ).
cnf(t29290,plain,
join(sFlat9,X1) = join(complement(join(join(sFlat9,complement(X1)),complement(join(sFlat9,X1)))),complement(sFlat8)),
inference(cp,[status(thm)],[t26870,t29232]) ).
cnf(t37127,plain,
join(sFlat9,X1) = join(complement(sFlat8),complement(join(join(sFlat9,complement(X1)),complement(join(sFlat9,X1))))),
inference(step,[status(thm)],[t29290,t90]) ).
cnf(t37128,plain,
join(sFlat9,X1) = join(sFlat9,complement(join(join(sFlat9,complement(X1)),complement(join(sFlat9,X1))))),
inference(step,[status(thm)],[t37127,t182]) ).
cnf(t37129,plain,
join(sFlat9,X1) = join(sFlat9,complement(join(sFlat9,join(complement(X1),complement(join(sFlat9,X1)))))),
inference(step,[status(thm)],[t37128,t99]) ).
cnf(t101,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t99,t90]) ).
cnf(t1324,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t101]) ).
cnf(t1337,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t1324,t1131]) ).
cnf(t1818,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(orient,[status(thm)],[t1337]) ).
cnf(t3512,plain,
X1 = join(X1,complement(join(X2,complement(X1)))),
inference(cp,[status(thm)],[t3509,t1818]) ).
cnf(t5659,plain,
join(X1,complement(join(X2,complement(X1)))) = X1,
inference(orient,[status(thm)],[t3512]) ).
cnf(t5695,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t5659,t1096]) ).
cnf(t6924,plain,
join(complement(X1),complement(join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t5695]) ).
cnf(t37130,plain,
join(sFlat9,X1) = join(sFlat9,complement(join(sFlat9,complement(X1)))),
inference(step,[status(thm)],[t37129,t6924]) ).
cnf(t29360,plain,
join(sFlat9,complement(join(sFlat9,complement(X1)))) = join(sFlat9,X1),
inference(orient,[status(thm)],[t37130]) ).
cnf(t29363,plain,
join(sFlat9,complement(X1)) = join(sFlat9,complement(join(sFlat9,X1))),
inference(cp,[status(thm)],[t29360,t1096]) ).
cnf(t29536,plain,
join(sFlat9,complement(join(sFlat9,X1))) = join(sFlat9,complement(X1)),
inference(orient,[status(thm)],[t29363]) ).
cnf(t263,plain,
sk1 = join(complement(join(sFlat6,X1)),complement(join(complement(sk1),complement(X1)))),
inference(cp,[status(thm)],[t254,t68]) ).
cnf(t37447,plain,
sk1 = join(complement(join(sFlat6,X1)),complement(join(sFlat6,complement(X1)))),
inference(step,[status(thm)],[t263,t68]) ).
cnf(t35218,plain,
join(complement(join(sFlat6,X1)),complement(join(sFlat6,complement(X1)))) = sk1,
inference(orient,[status(thm)],[t37447]) ).
cnf(t35257,plain,
sk1 = join(complement(sFlat8),complement(join(sFlat6,complement(sFlat7)))),
inference(cp,[status(thm)],[t35218,t104]) ).
cnf(t37448,plain,
sk1 = join(sFlat9,complement(join(sFlat6,complement(sFlat7)))),
inference(step,[status(thm)],[t35257,t182]) ).
cnf(t756,plain,
sk3 = join(zero,complement(sFlat7)),
inference(cp,[status(thm)],[t752,t83]) ).
cnf(t766,plain,
join(zero,complement(sFlat7)) = sk3,
inference(orient,[status(thm)],[t756]) ).
cnf(t35597,plain,
complement(sFlat7) = sk3,
inference(step,[status(thm)],[t766,t978]) ).
cnf(t996,plain,
complement(sFlat7) = sk3,
inference(rw,[status(thm)],[t35597]) ).
cnf(t1024,plain,
complement(sFlat7) = sk3,
inference(orient,[status(thm)],[t996]) ).
cnf(t37449,plain,
sk1 = join(sFlat9,complement(join(sFlat6,sk3))),
inference(step,[status(thm)],[t37448,t1024]) ).
cnf(t35308,plain,
join(sFlat9,complement(join(sFlat6,sk3))) = sk1,
inference(orient,[status(thm)],[t37449]) ).
cnf(t35311,plain,
join(sFlat9,complement(complement(join(sFlat6,sk3)))) = join(sFlat9,complement(sk1)),
inference(cp,[status(thm)],[t29536,t35308]) ).
cnf(t37450,plain,
join(sFlat9,join(sFlat6,sk3)) = join(sFlat9,complement(sk1)),
inference(step,[status(thm)],[t35311,t1096]) ).
cnf(t103,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t99,t90]) ).
cnf(t35836,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t103,t99]) ).
cnf(t2365,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t35836]) ).
cnf(t3527,plain,
sk3 = join(sk3,complement(join(sFlat7,X1))),
inference(cp,[status(thm)],[t3509,t83]) ).
cnf(t3925,plain,
join(sk3,complement(join(sFlat7,X1))) = sk3,
inference(orient,[status(thm)],[t3527]) ).
cnf(t105,plain,
join(sFlat6,join(sFlat7,X1)) = join(sFlat8,X1),
inference(cp,[status(thm)],[t99,t104]) ).
cnf(t293,plain,
join(sFlat6,join(sFlat7,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t105]) ).
cnf(t296,plain,
join(sFlat8,X1) = join(sFlat6,join(X1,sFlat7)),
inference(cp,[status(thm)],[t293,t90]) ).
cnf(t354,plain,
join(sFlat6,join(X1,sFlat7)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t296]) ).
cnf(t645,plain,
complement(sk3) = join(sFlat7,complement(sk3)),
inference(cp,[status(thm)],[t640,t83]) ).
cnf(t35478,plain,
sFlat7 = join(sFlat7,complement(sk3)),
inference(step,[status(thm)],[t645,t83]) ).
cnf(t35479,plain,
sFlat7 = join(sFlat7,sFlat7),
inference(step,[status(thm)],[t35478,t83]) ).
cnf(t674,plain,
join(sFlat7,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t35479]) ).
cnf(t675,plain,
join(sFlat8,sFlat7) = join(sFlat6,sFlat7),
inference(cp,[status(thm)],[t354,t674]) ).
cnf(t35494,plain,
join(sFlat7,sFlat8) = join(sFlat6,sFlat7),
inference(step,[status(thm)],[t675,t90]) ).
cnf(t35495,plain,
join(sFlat7,sFlat8) = sFlat8,
inference(step,[status(thm)],[t35494,t104]) ).
cnf(t701,plain,
join(sFlat7,sFlat8) = sFlat8,
inference(orient,[status(thm)],[t35495]) ).
cnf(t3928,plain,
sk3 = join(sk3,complement(sFlat8)),
inference(cp,[status(thm)],[t3925,t701]) ).
cnf(t35921,plain,
sk3 = join(sk3,sFlat9),
inference(step,[status(thm)],[t3928,t182]) ).
cnf(t35922,plain,
sk3 = join(sFlat9,sk3),
inference(step,[status(thm)],[t35921,t90]) ).
cnf(t3939,plain,
join(sFlat9,sk3) = sk3,
inference(orient,[status(thm)],[t35922]) ).
cnf(t3942,plain,
join(sFlat9,join(X1,sk3)) = join(X1,sk3),
inference(cp,[status(thm)],[t2365,t3939]) ).
cnf(t3969,plain,
join(sFlat9,join(X1,sk3)) = join(X1,sk3),
inference(orient,[status(thm)],[t3942]) ).
cnf(t37451,plain,
join(sFlat6,sk3) = join(sFlat9,complement(sk1)),
inference(step,[status(thm)],[t37450,t3969]) ).
cnf(t37452,plain,
join(sFlat6,sk3) = join(sFlat9,sFlat6),
inference(step,[status(thm)],[t37451,t68]) ).
cnf(t37453,plain,
join(sFlat6,sk3) = join(sFlat6,sFlat9),
inference(step,[status(thm)],[t37452,t90]) ).
cnf(t35325,plain,
join(sFlat6,sk3) = join(sFlat6,sFlat9),
inference(orient,[status(thm)],[t37453]) ).
cnf(t35326,plain,
composition(sFlat4,sk3) = composition(sFlat4,join(sFlat6,sFlat9)),
inference(cp,[status(thm)],[t24293,t35325]) ).
cnf(t37454,plain,
sFlat5 = composition(sFlat4,join(sFlat6,sFlat9)),
inference(step,[status(thm)],[t35326,t178]) ).
cnf(t37455,plain,
sFlat5 = composition(sFlat4,sFlat9),
inference(step,[status(thm)],[t37454,t24293]) ).
cnf(t37456,plain,
sFlat5 = sFlat10,
inference(step,[status(thm)],[t37455,t186]) ).
cnf(t35345,plain,
sFlat10 = sFlat5,
inference(orient,[status(thm)],[t37456]) ).
cnf(t37457,plain,
composition(sFlat4,sFlat9) = sFlat5,
inference(step,[status(thm)],[t186,t35345]) ).
cnf(t35346,plain,
composition(sFlat4,sFlat9) = sFlat5,
inference(orient,[status(thm)],[t37457]) ).
cnf(u1,negated_conjecture,
join(composition(meet(sk2,converse(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(complement(join(complement(sk2),complement(converse(sk1)))),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,
join(composition(complement(join(sFlat0,complement(converse(sk1)))),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(rw,[status(thm)],[goal_0,t76]) ).
cnf(g0_1,plain,
join(composition(complement(join(sFlat0,complement(sFlat1))),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(rw,[status(thm)],[g0_0,t123]) ).
cnf(g0_2,plain,
join(composition(complement(join(sFlat0,sFlat2)),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(rw,[status(thm)],[g0_1,t154]) ).
cnf(g0_3,plain,
join(composition(complement(sFlat3),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(rw,[status(thm)],[g0_2,t106]) ).
cnf(g0_4,plain,
join(composition(sFlat4,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(rw,[status(thm)],[g0_3,t173]) ).
cnf(g0_5,plain,
join(sFlat5,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(rw,[status(thm)],[g0_4,t178]) ).
cnf(g0_6,plain,
join(sFlat5,composition(complement(join(sFlat0,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)],[g0_5,t76]) ).
cnf(g0_7,plain,
join(sFlat5,composition(complement(join(sFlat0,complement(sFlat1))),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_6,t123]) ).
cnf(g0_8,plain,
join(sFlat5,composition(complement(join(sFlat0,sFlat2)),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_7,t154]) ).
cnf(g0_9,plain,
join(sFlat5,composition(complement(sFlat3),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_8,t106]) ).
cnf(g0_10,plain,
join(sFlat5,composition(sFlat4,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_9,t173]) ).
cnf(g0_11,plain,
join(sFlat5,composition(sFlat4,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_10,t90]) ).
cnf(g0_12,plain,
join(sFlat5,composition(sFlat4,complement(join(sFlat7,complement(sk1))))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_11,t83]) ).
cnf(g0_13,plain,
join(sFlat5,composition(sFlat4,complement(join(sFlat7,sFlat6)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_12,t68]) ).
cnf(g0_14,plain,
join(sFlat5,composition(sFlat4,complement(join(sFlat6,sFlat7)))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_13,t90]) ).
cnf(g0_15,plain,
join(sFlat5,composition(sFlat4,complement(sFlat8))) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_14,t104]) ).
cnf(g0_16,plain,
join(sFlat5,composition(sFlat4,sFlat9)) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_15,t182]) ).
cnf(g0_17,plain,
join(sFlat5,sFlat5) != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_16,t35346]) ).
cnf(g0_18,plain,
sFlat5 != composition(complement(join(complement(sk2),complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_17,t1131]) ).
cnf(g0_19,plain,
sFlat5 != composition(complement(join(sFlat0,complement(converse(sk1)))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_18,t76]) ).
cnf(g0_20,plain,
sFlat5 != composition(complement(join(sFlat0,complement(sFlat1))),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_19,t123]) ).
cnf(g0_21,plain,
sFlat5 != composition(complement(join(sFlat0,sFlat2)),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_20,t154]) ).
cnf(g0_22,plain,
sFlat5 != composition(complement(sFlat3),complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_21,t106]) ).
cnf(g0_23,plain,
sFlat5 != composition(sFlat4,complement(join(complement(sk1),complement(sk3)))),
inference(rw,[status(thm)],[g0_22,t173]) ).
cnf(g0_24,plain,
sFlat5 != composition(sFlat4,complement(join(complement(sk3),complement(sk1)))),
inference(rw,[status(thm)],[g0_23,t90]) ).
cnf(g0_25,plain,
sFlat5 != composition(sFlat4,complement(join(sFlat7,complement(sk1)))),
inference(rw,[status(thm)],[g0_24,t83]) ).
cnf(g0_26,plain,
sFlat5 != composition(sFlat4,complement(join(sFlat7,sFlat6))),
inference(rw,[status(thm)],[g0_25,t68]) ).
cnf(g0_27,plain,
sFlat5 != composition(sFlat4,complement(join(sFlat6,sFlat7))),
inference(rw,[status(thm)],[g0_26,t90]) ).
cnf(g0_28,plain,
sFlat5 != composition(sFlat4,complement(sFlat8)),
inference(rw,[status(thm)],[g0_27,t104]) ).
cnf(g0_29,plain,
sFlat5 != composition(sFlat4,sFlat9),
inference(rw,[status(thm)],[g0_28,t182]) ).
cnf(g0_30,plain,
sFlat5 != sFlat5,
inference(rw,[status(thm)],[g0_29,t35346]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL036-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/10.37 % Computer : n016.cluster.edu
% 0.08/10.37 % Model : x86_64 x86_64
% 0.08/10.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.37 % Memory : 8046.5625MB
% 0.08/10.37 % OS : Linux 6.8.0-71-generic
% 0.08/10.37 % CPULimit : 300
% 0.08/10.37 % WCLimit : 300
% 0.08/10.37 % DateTime : Thu Sep 24 07:35:54 UTC 2026
% 0.08/10.37 % CPUTime :
% 0.08/10.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 103.22/23.67 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 103.22/23.67 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------