%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT241-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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 01:56:23 PM UTC 2026
% Result : Unsatisfiable 55.62s 7.58s
% Output : CNFRefutation 55.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 18
% Syntax : Number of clauses : 147 ( 147 unt; 0 nHn; 33 RR)
% Number of literals : 147 ( 146 equ; 5 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 : 11 ( 11 usr; 7 con; 0-4 aty)
% Number of variables : 232 ( 60 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
sFlat0 = complement(b),
introduced(definition) ).
cnf(t86,plain,
complement(b) = sFlat0,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat1 = complement(a),
introduced(definition) ).
cnf(t81,plain,
complement(a) = sFlat1,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sFlat2 = join(complement(b),complement(a)),
introduced(definition) ).
cnf(t77,plain,
join(complement(b),complement(a)) = sFlat2,
inference(orient,[status(thm)],[t16]) ).
cnf(t22745,plain,
join(complement(b),sFlat1) = sFlat2,
inference(step,[status(thm)],[t77,t81]) ).
cnf(t85,plain,
join(complement(b),sFlat1) = sFlat2,
inference(rw,[status(thm)],[t22745]) ).
cnf(t6,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t62,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t22756,plain,
join(sFlat1,complement(b)) = sFlat2,
inference(step,[status(thm)],[t85,t62]) ).
cnf(t22757,plain,
join(sFlat1,sFlat0) = sFlat2,
inference(step,[status(thm)],[t22756,t86]) ).
cnf(t22758,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(step,[status(thm)],[t22757,t62]) ).
cnf(t119,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t22758]) ).
cnf(t12,axiom,
ifeq(join(X1,X2),one,ifeq(meet(X1,X2),zero,complement(X1),X2),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
ifeq(join(X1,X2),one,ifeq(meet(X1,X2),zero,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t13,axiom,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t37,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t13]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t63,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t7,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t65,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(cp,[status(thm)],[t63,t20]) ).
cnf(t1699,plain,
join(X1,join(X2,meet(join(X1,X2),X3))) = join(X1,X2),
inference(orient,[status(thm)],[t65]) ).
cnf(t8,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t1703,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t1699,t27]) ).
cnf(t3065,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t1703]) ).
cnf(t3100,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X2,meet(X1,X3)))))) = meet(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t37,t3065]) ).
cnf(t68,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t63,t20]) ).
cnf(t659,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t68]) ).
cnf(t665,plain,
join(X1,X2) = join(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t659,t62]) ).
cnf(t852,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t665]) ).
cnf(t23170,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t3100,t852]) ).
cnf(t14316,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t23170]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t73,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t14385,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),meet(X2,one))),
inference(cp,[status(thm)],[t14316,t73]) ).
cnf(t9,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t75,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t18,t73]) ).
cnf(t92,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t75]) ).
cnf(t23246,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t14385,t92]) ).
cnf(t20289,plain,
meet(X1,join(complement(X1),meet(X1,X2))) = meet(X1,join(complement(X1),X2)),
inference(orient,[status(thm)],[t23246]) ).
cnf(t11,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t33,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t28,t18]) ).
cnf(t604,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t33]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t49,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t610,plain,
meet(X1,complement(join(X1,X2))) = meet(X1,zero),
inference(cp,[status(thm)],[t604,t49]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t32,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t28,t17]) ).
cnf(t128,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t32]) ).
cnf(t130,plain,
meet(X1,complement(X1)) = meet(X1,zero),
inference(cp,[status(thm)],[t128,t49]) ).
cnf(t22759,plain,
zero = meet(X1,zero),
inference(step,[status(thm)],[t130,t49]) ).
cnf(t137,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t22759]) ).
cnf(t22818,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(step,[status(thm)],[t610,t137]) ).
cnf(t635,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t22818]) ).
cnf(t20342,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = meet(X1,join(complement(X1),zero)),
inference(cp,[status(thm)],[t20289,t635]) ).
cnf(t52,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t20,t49]) ).
cnf(t90,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t52]) ).
cnf(t23311,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t20342,t90]) ).
cnf(t23312,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = zero,
inference(step,[status(thm)],[t23311,t49]) ).
cnf(t22492,plain,
meet(X1,join(complement(X1),complement(join(X1,X2)))) = zero,
inference(orient,[status(thm)],[t23312]) ).
cnf(t22514,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(join(X1,join(complement(X1),complement(join(X1,X2)))),one,ifeq(zero,zero,complement(X1),join(complement(X1),complement(join(X1,X2)))),join(complement(X1),complement(join(X1,X2)))),
inference(cp,[status(thm)],[t22,t22492]) ).
cnf(t76,plain,
join(X1,join(complement(X1),X2)) = join(one,X2),
inference(cp,[status(thm)],[t63,t73]) ).
cnf(t327,plain,
join(X1,join(complement(X1),X2)) = join(one,X2),
inference(orient,[status(thm)],[t76]) ).
cnf(t87,plain,
one = join(b,sFlat0),
inference(cp,[status(thm)],[t73,t86]) ).
cnf(t22751,plain,
one = join(sFlat0,b),
inference(step,[status(thm)],[t87,t62]) ).
cnf(t109,plain,
join(sFlat0,b) = one,
inference(orient,[status(thm)],[t22751]) ).
cnf(t110,plain,
join(sFlat0,join(b,X1)) = join(one,X1),
inference(cp,[status(thm)],[t63,t109]) ).
cnf(t203,plain,
join(sFlat0,join(b,X1)) = join(one,X1),
inference(orient,[status(thm)],[t110]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t67,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t63,t19]) ).
cnf(t140,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t67]) ).
cnf(t206,plain,
join(one,join(b,X1)) = join(sFlat0,join(b,X1)),
inference(cp,[status(thm)],[t203,t140]) ).
cnf(t22789,plain,
join(one,join(b,X1)) = join(one,X1),
inference(step,[status(thm)],[t206,t203]) ).
cnf(t410,plain,
join(one,join(b,X1)) = join(one,X1),
inference(orient,[status(thm)],[t22789]) ).
cnf(t2024,plain,
join(one,join(b,X1)) = join(one,X1),
inference(rw,[status(thm)],[t410]) ).
cnf(t66,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t63,t62]) ).
cnf(t175,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t66]) ).
cnf(t339,plain,
join(join(complement(X1),X2),join(X3,X1)) = join(X3,join(one,X2)),
inference(cp,[status(thm)],[t175,t327]) ).
cnf(t22916,plain,
join(complement(X1),join(X2,join(X3,X1))) = join(X3,join(one,X2)),
inference(step,[status(thm)],[t339,t63]) ).
cnf(t338,plain,
join(one,join(complement(complement(X1)),X2)) = join(X1,join(one,X2)),
inference(cp,[status(thm)],[t327,t327]) ).
cnf(t330,plain,
join(one,join(complement(X1),X2)) = join(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t327,t140]) ).
cnf(t22795,plain,
join(one,join(complement(X1),X2)) = join(one,X2),
inference(step,[status(thm)],[t330,t327]) ).
cnf(t495,plain,
join(one,join(complement(X1),X2)) = join(one,X2),
inference(orient,[status(thm)],[t22795]) ).
cnf(t22837,plain,
join(one,X2) = join(X1,join(one,X2)),
inference(step,[status(thm)],[t338,t495]) ).
cnf(t1034,plain,
join(X1,join(one,X2)) = join(one,X2),
inference(orient,[status(thm)],[t22837]) ).
cnf(t22917,plain,
join(complement(X1),join(X2,join(X3,X1))) = join(one,X2),
inference(step,[status(thm)],[t22916,t1034]) ).
cnf(t1951,plain,
join(complement(X1),join(X2,join(X3,X1))) = join(one,X2),
inference(orient,[status(thm)],[t22917]) ).
cnf(t1953,plain,
join(one,X1) = join(complement(meet(X1,X2)),join(X1,X3)),
inference(cp,[status(thm)],[t1951,t852]) ).
cnf(t69,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t63,t62]) ).
cnf(t22763,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t69,t63]) ).
cnf(t178,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t22763]) ).
cnf(t22921,plain,
join(one,X1) = join(X1,join(complement(meet(X1,X2)),X3)),
inference(step,[status(thm)],[t1953,t178]) ).
cnf(t663,plain,
join(X1,join(complement(meet(X1,X2)),X3)) = join(X1,join(one,X3)),
inference(cp,[status(thm)],[t659,t327]) ).
cnf(t22920,plain,
join(X1,join(complement(meet(X1,X2)),X3)) = join(one,X3),
inference(step,[status(thm)],[t663,t1034]) ).
cnf(t2000,plain,
join(X1,join(complement(meet(X1,X2)),X3)) = join(one,X3),
inference(orient,[status(thm)],[t22920]) ).
cnf(t22922,plain,
join(one,X1) = join(one,X3),
inference(step,[status(thm)],[t22921,t2000]) ).
cnf(t2015,plain,
join(one,X1) = join(one,X2),
inference(orient,[status(thm)],[t22922]) ).
cnf(t22935,plain,
join(one,sFlat0) = join(one,X1),
inference(step,[status(thm)],[t2024,t2015]) ).
cnf(t22936,plain,
join(sFlat0,one) = join(one,X1),
inference(step,[status(thm)],[t22935,t62]) ).
cnf(t142,plain,
join(X1,complement(X1)) = join(X1,one),
inference(cp,[status(thm)],[t140,t73]) ).
cnf(t22760,plain,
one = join(X1,one),
inference(step,[status(thm)],[t142,t73]) ).
cnf(t149,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t22760]) ).
cnf(t22937,plain,
one = join(one,X1),
inference(step,[status(thm)],[t22936,t149]) ).
cnf(t2027,plain,
join(one,X1) = one,
inference(orient,[status(thm)],[t22937]) ).
cnf(t22942,plain,
join(X1,join(complement(X1),X2)) = one,
inference(step,[status(thm)],[t327,t2027]) ).
cnf(t2032,plain,
join(X1,join(complement(X1),X2)) = one,
inference(orient,[status(thm)],[t22942]) ).
cnf(t23313,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(one,one,ifeq(zero,zero,complement(X1),join(complement(X1),complement(join(X1,X2)))),join(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t22514,t2032]) ).
cnf(t5,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t23314,plain,
join(complement(X1),complement(join(X1,X2))) = ifeq(zero,zero,complement(X1),join(complement(X1),complement(join(X1,X2)))),
inference(step,[status(thm)],[t23313,t21]) ).
cnf(t23315,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(step,[status(thm)],[t23314,t21]) ).
cnf(t22558,plain,
join(complement(X1),complement(join(X1,X2))) = complement(X1),
inference(orient,[status(thm)],[t23315]) ).
cnf(t22559,plain,
complement(a) = join(sFlat1,complement(join(a,X1))),
inference(cp,[status(thm)],[t22558,t81]) ).
cnf(t23316,plain,
sFlat1 = join(sFlat1,complement(join(a,X1))),
inference(step,[status(thm)],[t22559,t81]) ).
cnf(t22600,plain,
join(sFlat1,complement(join(a,X1))) = sFlat1,
inference(orient,[status(thm)],[t23316]) ).
cnf(t2,axiom,
meet(b,a) = a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t56,plain,
meet(b,a) = a,
inference(orient,[status(thm)],[t2]) ).
cnf(t58,plain,
b = join(b,a),
inference(cp,[status(thm)],[t20,t56]) ).
cnf(t96,plain,
join(b,a) = b,
inference(orient,[status(thm)],[t58]) ).
cnf(t97,plain,
join(b,join(a,X1)) = join(b,X1),
inference(cp,[status(thm)],[t63,t96]) ).
cnf(t179,plain,
join(b,join(a,X1)) = join(b,X1),
inference(orient,[status(thm)],[t97]) ).
cnf(t1723,plain,
join(b,join(X1,meet(join(a,X1),X2))) = join(b,join(a,X1)),
inference(cp,[status(thm)],[t179,t1699]) ).
cnf(t23053,plain,
join(b,join(X1,meet(join(a,X1),X2))) = join(b,X1),
inference(step,[status(thm)],[t1723,t179]) ).
cnf(t5860,plain,
join(b,join(X1,meet(join(a,X1),X2))) = join(b,X1),
inference(orient,[status(thm)],[t23053]) ).
cnf(t5863,plain,
join(b,X1) = join(X1,join(b,meet(join(a,X1),X2))),
inference(cp,[status(thm)],[t5860,t178]) ).
cnf(t12388,plain,
join(X1,join(b,meet(join(a,X1),X2))) = join(b,X1),
inference(orient,[status(thm)],[t5863]) ).
cnf(t22603,plain,
sFlat1 = join(sFlat1,complement(join(b,a))),
inference(cp,[status(thm)],[t22600,t12388]) ).
cnf(t23317,plain,
sFlat1 = join(sFlat1,complement(b)),
inference(step,[status(thm)],[t22603,t96]) ).
cnf(t23318,plain,
sFlat1 = join(sFlat1,sFlat0),
inference(step,[status(thm)],[t23317,t86]) ).
cnf(t23319,plain,
sFlat1 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t23318,t62]) ).
cnf(t23320,plain,
sFlat1 = sFlat2,
inference(step,[status(thm)],[t23319,t119]) ).
cnf(t22631,plain,
sFlat2 = sFlat1,
inference(orient,[status(thm)],[t23320]) ).
cnf(t23321,plain,
join(sFlat0,sFlat1) = sFlat1,
inference(step,[status(thm)],[t119,t22631]) ).
cnf(t22632,plain,
join(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t23321]) ).
cnf(goal_0,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(sFlat0,complement(a)) != complement(a),
inference(rw,[status(thm)],[goal_0,t86]) ).
cnf(g0_1,plain,
join(sFlat0,sFlat1) != complement(a),
inference(rw,[status(thm)],[g0_0,t81]) ).
cnf(g0_2,plain,
sFlat1 != complement(a),
inference(rw,[status(thm)],[g0_1,t22632]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t81]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT241-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.17/0.43 % Computer : n017.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Wed Sep 23 20:34:59 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 55.62/7.58 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 55.62/7.58 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------