%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL031-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:35:53 PM UTC 2026
% Result : Unsatisfiable 83.43s 11.07s
% Output : CNFRefutation 83.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 20
% Syntax : Number of clauses : 156 ( 156 unt; 0 nHn; 61 RR)
% Number of literals : 156 ( 155 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 163 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t44,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t11,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t46,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t6,axiom,
join(composition(converse(sk2),sk2),one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22384,plain,
join(one,composition(converse(sk2),sk2)) = one,
inference(step,[status(thm)],[t6,t44]) ).
cnf(t64,plain,
join(one,composition(converse(sk2),sk2)) = one,
inference(orient,[status(thm)],[t22384]) ).
cnf(t65,plain,
join(one,join(composition(converse(sk2),sk2),X1)) = join(one,X1),
inference(cp,[status(thm)],[t46,t64]) ).
cnf(t1915,plain,
join(one,join(composition(converse(sk2),sk2),X1)) = join(one,X1),
inference(orient,[status(thm)],[t65]) ).
cnf(t12,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t1916,plain,
join(one,composition(X1,sk2)) = join(one,composition(join(converse(sk2),X1),sk2)),
inference(cp,[status(thm)],[t1915,t26]) ).
cnf(t22242,plain,
join(one,composition(join(converse(sk2),X1),sk2)) = join(one,composition(X1,sk2)),
inference(orient,[status(thm)],[t1916]) ).
cnf(t9,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t8,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t31,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t29,t23]) ).
cnf(t212,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t31]) ).
cnf(t222,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t66,t212]) ).
cnf(t6014,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t222]) ).
cnf(t10,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t28,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t26,t24]) ).
cnf(t2542,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t15,axiom,
sFlat0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t39,plain,
composition(sk1,sk2) = sFlat0,
inference(orient,[status(thm)],[t15]) ).
cnf(t2603,plain,
composition(join(X1,composition(X2,sk1)),sk2) = join(composition(X1,sk2),composition(X2,sFlat0)),
inference(cp,[status(thm)],[t2542,t39]) ).
cnf(t11314,plain,
composition(join(X1,composition(X2,sk1)),sk2) = join(composition(X1,sk2),composition(X2,sFlat0)),
inference(orient,[status(thm)],[t2603]) ).
cnf(t5,axiom,
join(composition(converse(sk1),sk1),one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22383,plain,
join(one,composition(converse(sk1),sk1)) = one,
inference(step,[status(thm)],[t5,t44]) ).
cnf(t62,plain,
join(one,composition(converse(sk1),sk1)) = one,
inference(orient,[status(thm)],[t22383]) ).
cnf(t11317,plain,
join(composition(one,sk2),composition(converse(sk1),sFlat0)) = composition(one,sk2),
inference(cp,[status(thm)],[t11314,t62]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,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,t19]) ).
cnf(t22400,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t213,t23]) ).
cnf(t228,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t22400]) ).
cnf(t25,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t24,t19]) ).
cnf(t187,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t25]) ).
cnf(t230,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t228,t187]) ).
cnf(t22402,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t230,t228]) ).
cnf(t244,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t22402]) ).
cnf(t22886,plain,
join(sk2,composition(converse(sk1),sFlat0)) = composition(one,sk2),
inference(step,[status(thm)],[t11317,t244]) ).
cnf(t22887,plain,
join(sk2,composition(converse(sk1),sFlat0)) = sk2,
inference(step,[status(thm)],[t22886,t244]) ).
cnf(t11340,plain,
join(sk2,composition(converse(sk1),sFlat0)) = sk2,
inference(orient,[status(thm)],[t22887]) ).
cnf(t11345,plain,
join(converse(sk2),composition(converse(sFlat0),sk1)) = converse(sk2),
inference(cp,[status(thm)],[t6014,t11340]) ).
cnf(t16,axiom,
sFlat1 = converse(composition(sk1,sk2)),
introduced(definition) ).
cnf(t22385,plain,
sFlat1 = converse(sFlat0),
inference(step,[status(thm)],[t16,t39]) ).
cnf(t70,plain,
converse(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t22385]) ).
cnf(t22888,plain,
join(converse(sk2),composition(sFlat1,sk1)) = converse(sk2),
inference(step,[status(thm)],[t11345,t70]) ).
cnf(t11346,plain,
join(converse(sk2),composition(sFlat1,sk1)) = converse(sk2),
inference(orient,[status(thm)],[t22888]) ).
cnf(t22244,plain,
join(one,composition(composition(sFlat1,sk1),sk2)) = join(one,composition(converse(sk2),sk2)),
inference(cp,[status(thm)],[t22242,t11346]) ).
cnf(t23170,plain,
join(one,composition(sFlat1,composition(sk1,sk2))) = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t22244,t24]) ).
cnf(t23171,plain,
join(one,composition(sFlat1,sFlat0)) = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t23170,t39]) ).
cnf(t17,axiom,
sFlat2 = composition(converse(composition(sk1,sk2)),composition(sk1,sk2)),
introduced(definition) ).
cnf(t35,plain,
composition(converse(composition(sk1,sk2)),composition(sk1,sk2)) = sFlat2,
inference(orient,[status(thm)],[t17]) ).
cnf(t22377,plain,
composition(converse(sFlat0),composition(sk1,sk2)) = sFlat2,
inference(step,[status(thm)],[t35,t39]) ).
cnf(t22378,plain,
composition(converse(sFlat0),sFlat0) = sFlat2,
inference(step,[status(thm)],[t22377,t39]) ).
cnf(t43,plain,
composition(converse(sFlat0),sFlat0) = sFlat2,
inference(rw,[status(thm)],[t22378]) ).
cnf(t22391,plain,
composition(sFlat1,sFlat0) = sFlat2,
inference(step,[status(thm)],[t43,t70]) ).
cnf(t103,plain,
composition(sFlat1,sFlat0) = sFlat2,
inference(orient,[status(thm)],[t22391]) ).
cnf(t23172,plain,
join(one,sFlat2) = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t23171,t103]) ).
cnf(t23173,plain,
join(sFlat2,one) = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t23172,t44]) ).
cnf(t18,axiom,
sFlat3 = join(composition(converse(composition(sk1,sk2)),composition(sk1,sk2)),one),
introduced(definition) ).
cnf(t22380,plain,
sFlat3 = join(one,composition(converse(composition(sk1,sk2)),composition(sk1,sk2))),
inference(step,[status(thm)],[t18,t44]) ).
cnf(t22381,plain,
sFlat3 = join(one,composition(converse(sFlat0),composition(sk1,sk2))),
inference(step,[status(thm)],[t22380,t39]) ).
cnf(t22382,plain,
sFlat3 = join(one,composition(converse(sFlat0),sFlat0)),
inference(step,[status(thm)],[t22381,t39]) ).
cnf(t60,plain,
join(one,composition(converse(sFlat0),sFlat0)) = sFlat3,
inference(orient,[status(thm)],[t22382]) ).
cnf(t22386,plain,
join(one,composition(sFlat1,sFlat0)) = sFlat3,
inference(step,[status(thm)],[t60,t70]) ).
cnf(t77,plain,
join(one,composition(sFlat1,sFlat0)) = sFlat3,
inference(rw,[status(thm)],[t22386]) ).
cnf(t22396,plain,
join(one,sFlat2) = sFlat3,
inference(step,[status(thm)],[t77,t103]) ).
cnf(t22397,plain,
join(sFlat2,one) = sFlat3,
inference(step,[status(thm)],[t22396,t44]) ).
cnf(t152,plain,
join(sFlat2,one) = sFlat3,
inference(orient,[status(thm)],[t22397]) ).
cnf(t23174,plain,
sFlat3 = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t23173,t152]) ).
cnf(t23175,plain,
sFlat3 = one,
inference(step,[status(thm)],[t23174,t64]) ).
cnf(t22316,plain,
one = sFlat3,
inference(orient,[status(thm)],[t23175]) ).
cnf(t13,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22379,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t44]) ).
cnf(t53,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t22379]) ).
cnf(t247,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t53,t244]) ).
cnf(t229,plain,
one = converse(one),
inference(cp,[status(thm)],[t228,t19]) ).
cnf(t235,plain,
converse(one) = one,
inference(orient,[status(thm)],[t229]) ).
cnf(t22413,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t247,t235]) ).
cnf(t22414,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t22413,t244]) ).
cnf(t439,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t22414]) ).
cnf(t7,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t78,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
cnf(t440,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t439,t78]) ).
cnf(t22552,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t440,t78]) ).
cnf(t22553,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t22552,t78]) ).
cnf(t1985,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t22553]) ).
cnf(t14,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t45,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t20]) ).
cnf(t22715,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t45,t44]) ).
cnf(t22716,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t22715,t78]) ).
cnf(t22717,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t22716,t44]) ).
cnf(t9715,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t22717]) ).
cnf(t9726,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t9715,t78]) ).
cnf(t22731,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t9726,t44]) ).
cnf(t9838,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t22731]) ).
cnf(t80,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t78,t44]) ).
cnf(t22387,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t80,t78]) ).
cnf(t93,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t22387]) ).
cnf(t9843,plain,
X1 = join(meet(X1,X2),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t9838,t93]) ).
cnf(t9905,plain,
join(meet(X1,X2),meet(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t9843]) ).
cnf(t3,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t85,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t448,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t78,t439]) ).
cnf(t453,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t448]) ).
cnf(t457,plain,
zero = meet(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t85,t453]) ).
cnf(t986,plain,
meet(complement(X1),meet(X1,X1)) = zero,
inference(orient,[status(thm)],[t457]) ).
cnf(t9909,plain,
meet(X1,X1) = join(meet(meet(X1,X1),X1),zero),
inference(cp,[status(thm)],[t9905,t986]) ).
cnf(t22739,plain,
meet(X1,X1) = join(zero,meet(meet(X1,X1),X1)),
inference(step,[status(thm)],[t9909,t44]) ).
cnf(t22740,plain,
meet(X1,X1) = join(zero,meet(X1,meet(X1,X1))),
inference(step,[status(thm)],[t22739,t93]) ).
cnf(t9919,plain,
join(zero,meet(X1,meet(X1,X1))) = meet(X1,X1),
inference(orient,[status(thm)],[t22740]) ).
cnf(t9924,plain,
meet(X1,X1) = join(zero,meet(X1,complement(complement(X1)))),
inference(cp,[status(thm)],[t9919,t453]) ).
cnf(t2,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t50,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t9755,plain,
X1 = join(meet(X1,complement(complement(X1))),complement(top)),
inference(cp,[status(thm)],[t9715,t50]) ).
cnf(t22728,plain,
X1 = join(complement(top),meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t9755,t44]) ).
cnf(t79,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t78,t50]) ).
cnf(t22388,plain,
zero = complement(top),
inference(step,[status(thm)],[t79,t85]) ).
cnf(t94,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t22388]) ).
cnf(t22729,plain,
X1 = join(zero,meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t22728,t94]) ).
cnf(t9815,plain,
join(zero,meet(X1,complement(complement(X1)))) = X1,
inference(orient,[status(thm)],[t22729]) ).
cnf(t22748,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t9924,t9815]) ).
cnf(t9947,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t22748]) ).
cnf(t9949,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t1985,t9947]) ).
cnf(t22758,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t9949,t9947]) ).
cnf(t22759,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t22758,t9947]) ).
cnf(t9966,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t22759]) ).
cnf(t49,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t46,t44]) ).
cnf(t22407,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t49,t46]) ).
cnf(t333,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t22407]) ).
cnf(t9968,plain,
join(X1,X2) = join(X1,join(join(X1,X2),X2)),
inference(cp,[status(thm)],[t9966,t333]) ).
cnf(t22810,plain,
join(X1,X2) = join(X1,join(X1,join(X2,X2))),
inference(step,[status(thm)],[t9968,t46]) ).
cnf(t22811,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(step,[status(thm)],[t22810,t9966]) ).
cnf(t10375,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t22811]) ).
cnf(t10380,plain,
join(sFlat2,one) = join(sFlat2,sFlat3),
inference(cp,[status(thm)],[t10375,t152]) ).
cnf(t22812,plain,
sFlat3 = join(sFlat2,sFlat3),
inference(step,[status(thm)],[t10380,t152]) ).
cnf(t10384,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t22812]) ).
cnf(goal_0,negated_conjecture,
join(composition(converse(composition(sk1,sk2)),composition(sk1,sk2)),one) != one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(one,composition(converse(composition(sk1,sk2)),composition(sk1,sk2))) != one,
inference(rw,[status(thm)],[goal_0,t44]) ).
cnf(g0_1,plain,
join(sFlat3,composition(converse(composition(sk1,sk2)),composition(sk1,sk2))) != one,
inference(rw,[status(thm)],[g0_0,t22316]) ).
cnf(g0_2,plain,
join(sFlat3,composition(converse(sFlat0),composition(sk1,sk2))) != one,
inference(rw,[status(thm)],[g0_1,t39]) ).
cnf(g0_3,plain,
join(sFlat3,composition(sFlat1,composition(sk1,sk2))) != one,
inference(rw,[status(thm)],[g0_2,t70]) ).
cnf(g0_4,plain,
join(sFlat3,composition(sFlat1,sFlat0)) != one,
inference(rw,[status(thm)],[g0_3,t39]) ).
cnf(g0_5,plain,
join(sFlat3,sFlat2) != one,
inference(rw,[status(thm)],[g0_4,t103]) ).
cnf(g0_6,plain,
join(sFlat2,sFlat3) != one,
inference(rw,[status(thm)],[g0_5,t44]) ).
cnf(g0_7,plain,
sFlat3 != one,
inference(rw,[status(thm)],[g0_6,t10384]) ).
cnf(g0_8,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_7,t22316]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL031-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n018.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 07:29:03 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 83.43/11.07 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 83.43/11.07 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------