%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT017-1 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.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:55:00 PM UTC 2026
% Result : Unsatisfiable 8.31s 6.82s
% Output : CNFRefutation 8.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 25
% Syntax : Number of clauses : 295 ( 295 unt; 0 nHn; 262 RR)
% Number of literals : 295 ( 294 equ; 47 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 21 con; 0-2 aty)
% Number of variables : 47 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t10,axiom,
sFlat1 = complement(complement(a)),
introduced(definition) ).
cnf(t0,axiom,
complement(complement(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t1852,plain,
sFlat1 = a,
inference(step,[status(thm)],[t10,t32]) ).
cnf(t39,plain,
a = sFlat1,
inference(orient,[status(thm)],[t1852]) ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t97,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t23,axiom,
sFlat14 = complement(complement(b)),
introduced(definition) ).
cnf(t1855,plain,
sFlat14 = b,
inference(step,[status(thm)],[t23,t32]) ).
cnf(t41,plain,
b = sFlat14,
inference(orient,[status(thm)],[t1855]) ).
cnf(t24,axiom,
sFlat15 = join(complement(complement(a)),complement(complement(b))),
introduced(definition) ).
cnf(t1931,plain,
sFlat15 = join(complement(complement(b)),complement(complement(a))),
inference(step,[status(thm)],[t24,t97]) ).
cnf(t1932,plain,
sFlat15 = join(b,complement(complement(a))),
inference(step,[status(thm)],[t1931,t32]) ).
cnf(t1933,plain,
sFlat15 = join(sFlat14,complement(complement(a))),
inference(step,[status(thm)],[t1932,t41]) ).
cnf(t1934,plain,
sFlat15 = join(sFlat14,a),
inference(step,[status(thm)],[t1933,t32]) ).
cnf(t1935,plain,
sFlat15 = join(sFlat14,sFlat1),
inference(step,[status(thm)],[t1934,t39]) ).
cnf(t1936,plain,
sFlat15 = join(sFlat1,sFlat14),
inference(step,[status(thm)],[t1935,t97]) ).
cnf(t126,plain,
join(sFlat1,sFlat14) = sFlat15,
inference(orient,[status(thm)],[t1936]) ).
cnf(t14,axiom,
sFlat5 = join(a,b),
introduced(definition) ).
cnf(t2060,plain,
sFlat5 = join(b,a),
inference(step,[status(thm)],[t14,t97]) ).
cnf(t2061,plain,
sFlat5 = join(sFlat14,a),
inference(step,[status(thm)],[t2060,t41]) ).
cnf(t2062,plain,
sFlat5 = join(sFlat14,sFlat1),
inference(step,[status(thm)],[t2061,t39]) ).
cnf(t2063,plain,
sFlat5 = join(sFlat1,sFlat14),
inference(step,[status(thm)],[t2062,t97]) ).
cnf(t2064,plain,
sFlat5 = sFlat15,
inference(step,[status(thm)],[t2063,t126]) ).
cnf(t151,plain,
sFlat15 = sFlat5,
inference(orient,[status(thm)],[t2064]) ).
cnf(t2065,plain,
join(sFlat1,sFlat14) = sFlat5,
inference(step,[status(thm)],[t126,t151]) ).
cnf(t152,plain,
join(sFlat1,sFlat14) = sFlat5,
inference(orient,[status(thm)],[t2065]) ).
cnf(t25,axiom,
sFlat16 = complement(join(complement(complement(a)),complement(complement(b)))),
introduced(definition) ).
cnf(t1864,plain,
sFlat16 = complement(join(a,complement(complement(b)))),
inference(step,[status(thm)],[t25,t32]) ).
cnf(t1865,plain,
sFlat16 = complement(join(sFlat1,complement(complement(b)))),
inference(step,[status(thm)],[t1864,t39]) ).
cnf(t1866,plain,
sFlat16 = complement(join(sFlat1,b)),
inference(step,[status(thm)],[t1865,t32]) ).
cnf(t1867,plain,
sFlat16 = complement(join(sFlat1,sFlat14)),
inference(step,[status(thm)],[t1866,t41]) ).
cnf(t54,plain,
complement(join(sFlat1,sFlat14)) = sFlat16,
inference(orient,[status(thm)],[t1867]) ).
cnf(t15,axiom,
sFlat6 = complement(join(a,b)),
introduced(definition) ).
cnf(t1907,plain,
sFlat6 = complement(join(sFlat1,b)),
inference(step,[status(thm)],[t15,t39]) ).
cnf(t1908,plain,
sFlat6 = complement(join(sFlat1,sFlat14)),
inference(step,[status(thm)],[t1907,t41]) ).
cnf(t1909,plain,
sFlat6 = sFlat16,
inference(step,[status(thm)],[t1908,t54]) ).
cnf(t83,plain,
sFlat16 = sFlat6,
inference(orient,[status(thm)],[t1909]) ).
cnf(t1910,plain,
complement(join(sFlat1,sFlat14)) = sFlat6,
inference(step,[status(thm)],[t54,t83]) ).
cnf(t84,plain,
complement(join(sFlat1,sFlat14)) = sFlat6,
inference(orient,[status(thm)],[t1910]) ).
cnf(t1937,plain,
complement(sFlat15) = sFlat6,
inference(step,[status(thm)],[t84,t126]) ).
cnf(t128,plain,
complement(sFlat15) = sFlat6,
inference(rw,[status(thm)],[t1937]) ).
cnf(t2069,plain,
complement(sFlat5) = sFlat6,
inference(step,[status(thm)],[t128,t151]) ).
cnf(t168,plain,
complement(sFlat5) = sFlat6,
inference(orient,[status(thm)],[t2069]) ).
cnf(t11,axiom,
sFlat2 = complement(b),
introduced(definition) ).
cnf(t1913,plain,
sFlat2 = complement(sFlat14),
inference(step,[status(thm)],[t11,t41]) ).
cnf(t91,plain,
complement(sFlat14) = sFlat2,
inference(orient,[status(thm)],[t1913]) ).
cnf(t21,axiom,
sFlat12 = join(complement(complement(a)),complement(b)),
introduced(definition) ).
cnf(t1954,plain,
sFlat12 = join(complement(b),complement(complement(a))),
inference(step,[status(thm)],[t21,t97]) ).
cnf(t1955,plain,
sFlat12 = join(complement(sFlat14),complement(complement(a))),
inference(step,[status(thm)],[t1954,t41]) ).
cnf(t1956,plain,
sFlat12 = join(sFlat2,complement(complement(a))),
inference(step,[status(thm)],[t1955,t91]) ).
cnf(t1957,plain,
sFlat12 = join(sFlat2,a),
inference(step,[status(thm)],[t1956,t32]) ).
cnf(t1958,plain,
sFlat12 = join(sFlat2,sFlat1),
inference(step,[status(thm)],[t1957,t39]) ).
cnf(t1959,plain,
sFlat12 = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t1958,t97]) ).
cnf(t131,plain,
join(sFlat1,sFlat2) = sFlat12,
inference(orient,[status(thm)],[t1959]) ).
cnf(t12,axiom,
sFlat3 = join(a,complement(b)),
introduced(definition) ).
cnf(t2022,plain,
sFlat3 = join(sFlat1,complement(b)),
inference(step,[status(thm)],[t12,t39]) ).
cnf(t2023,plain,
sFlat3 = join(sFlat1,complement(sFlat14)),
inference(step,[status(thm)],[t2022,t41]) ).
cnf(t2024,plain,
sFlat3 = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t2023,t91]) ).
cnf(t2025,plain,
sFlat3 = sFlat12,
inference(step,[status(thm)],[t2024,t131]) ).
cnf(t145,plain,
sFlat12 = sFlat3,
inference(orient,[status(thm)],[t2025]) ).
cnf(t2026,plain,
join(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t131,t145]) ).
cnf(t146,plain,
join(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t2026]) ).
cnf(t22,axiom,
sFlat13 = complement(join(complement(complement(a)),complement(b))),
introduced(definition) ).
cnf(t1879,plain,
sFlat13 = complement(join(a,complement(b))),
inference(step,[status(thm)],[t22,t32]) ).
cnf(t1880,plain,
sFlat13 = complement(join(sFlat1,complement(b))),
inference(step,[status(thm)],[t1879,t39]) ).
cnf(t1881,plain,
sFlat13 = complement(join(sFlat1,complement(sFlat14))),
inference(step,[status(thm)],[t1880,t41]) ).
cnf(t65,plain,
complement(join(sFlat1,complement(sFlat14))) = sFlat13,
inference(orient,[status(thm)],[t1881]) ).
cnf(t13,axiom,
sFlat4 = complement(join(a,complement(b))),
introduced(definition) ).
cnf(t1901,plain,
sFlat4 = complement(join(sFlat1,complement(b))),
inference(step,[status(thm)],[t13,t39]) ).
cnf(t1902,plain,
sFlat4 = complement(join(sFlat1,complement(sFlat14))),
inference(step,[status(thm)],[t1901,t41]) ).
cnf(t1903,plain,
sFlat4 = sFlat13,
inference(step,[status(thm)],[t1902,t65]) ).
cnf(t79,plain,
sFlat13 = sFlat4,
inference(orient,[status(thm)],[t1903]) ).
cnf(t1904,plain,
complement(join(sFlat1,complement(sFlat14))) = sFlat4,
inference(step,[status(thm)],[t65,t79]) ).
cnf(t80,plain,
complement(join(sFlat1,complement(sFlat14))) = sFlat4,
inference(orient,[status(thm)],[t1904]) ).
cnf(t1914,plain,
complement(join(sFlat1,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t80,t91]) ).
cnf(t96,plain,
complement(join(sFlat1,sFlat2)) = sFlat4,
inference(rw,[status(thm)],[t1914]) ).
cnf(t2076,plain,
complement(sFlat3) = sFlat4,
inference(step,[status(thm)],[t96,t146]) ).
cnf(t198,plain,
complement(sFlat3) = sFlat4,
inference(orient,[status(thm)],[t2076]) ).
cnf(t27,axiom,
sFlat18 = complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))),
introduced(definition) ).
cnf(t1883,plain,
sFlat18 = complement(join(complement(join(a,complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))),
inference(step,[status(thm)],[t27,t32]) ).
cnf(t1884,plain,
sFlat18 = complement(join(complement(join(sFlat1,complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))),
inference(step,[status(thm)],[t1883,t39]) ).
cnf(t1885,plain,
sFlat18 = complement(join(complement(join(sFlat1,complement(sFlat14))),complement(join(complement(complement(a)),complement(complement(b)))))),
inference(step,[status(thm)],[t1884,t41]) ).
cnf(t1886,plain,
sFlat18 = complement(join(sFlat13,complement(join(complement(complement(a)),complement(complement(b)))))),
inference(step,[status(thm)],[t1885,t65]) ).
cnf(t1887,plain,
sFlat18 = complement(join(sFlat13,complement(join(a,complement(complement(b)))))),
inference(step,[status(thm)],[t1886,t32]) ).
cnf(t1888,plain,
sFlat18 = complement(join(sFlat13,complement(join(sFlat1,complement(complement(b)))))),
inference(step,[status(thm)],[t1887,t39]) ).
cnf(t1889,plain,
sFlat18 = complement(join(sFlat13,complement(join(sFlat1,b)))),
inference(step,[status(thm)],[t1888,t32]) ).
cnf(t1890,plain,
sFlat18 = complement(join(sFlat13,complement(join(sFlat1,sFlat14)))),
inference(step,[status(thm)],[t1889,t41]) ).
cnf(t1891,plain,
sFlat18 = complement(join(sFlat13,sFlat16)),
inference(step,[status(thm)],[t1890,t54]) ).
cnf(t71,plain,
complement(join(sFlat13,sFlat16)) = sFlat18,
inference(orient,[status(thm)],[t1891]) ).
cnf(t72,plain,
join(sFlat13,sFlat16) = complement(sFlat18),
inference(cp,[status(thm)],[t32,t71]) ).
cnf(t2073,plain,
join(sFlat4,sFlat16) = complement(sFlat18),
inference(step,[status(thm)],[t72,t79]) ).
cnf(t2074,plain,
join(sFlat4,sFlat6) = complement(sFlat18),
inference(step,[status(thm)],[t2073,t83]) ).
cnf(t17,axiom,
sFlat8 = complement(join(complement(join(a,complement(b))),complement(join(a,b)))),
introduced(definition) ).
cnf(t1892,plain,
sFlat8 = complement(join(complement(join(sFlat1,complement(b))),complement(join(a,b)))),
inference(step,[status(thm)],[t17,t39]) ).
cnf(t1893,plain,
sFlat8 = complement(join(complement(join(sFlat1,complement(sFlat14))),complement(join(a,b)))),
inference(step,[status(thm)],[t1892,t41]) ).
cnf(t1894,plain,
sFlat8 = complement(join(sFlat13,complement(join(a,b)))),
inference(step,[status(thm)],[t1893,t65]) ).
cnf(t1895,plain,
sFlat8 = complement(join(sFlat13,complement(join(sFlat1,b)))),
inference(step,[status(thm)],[t1894,t39]) ).
cnf(t1896,plain,
sFlat8 = complement(join(sFlat13,complement(join(sFlat1,sFlat14)))),
inference(step,[status(thm)],[t1895,t41]) ).
cnf(t1897,plain,
sFlat8 = complement(join(sFlat13,sFlat16)),
inference(step,[status(thm)],[t1896,t54]) ).
cnf(t1898,plain,
sFlat8 = sFlat18,
inference(step,[status(thm)],[t1897,t71]) ).
cnf(t76,plain,
sFlat18 = sFlat8,
inference(orient,[status(thm)],[t1898]) ).
cnf(t2075,plain,
join(sFlat4,sFlat6) = complement(sFlat8),
inference(step,[status(thm)],[t2074,t76]) ).
cnf(t196,plain,
join(sFlat4,sFlat6) = complement(sFlat8),
inference(orient,[status(thm)],[t2075]) ).
cnf(t26,axiom,
sFlat17 = join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b))))),
introduced(definition) ).
cnf(t1992,plain,
sFlat17 = join(complement(join(complement(b),complement(complement(a)))),complement(join(complement(complement(a)),complement(complement(b))))),
inference(step,[status(thm)],[t26,t97]) ).
cnf(t1993,plain,
sFlat17 = join(complement(join(complement(sFlat14),complement(complement(a)))),complement(join(complement(complement(a)),complement(complement(b))))),
inference(step,[status(thm)],[t1992,t41]) ).
cnf(t1994,plain,
sFlat17 = join(complement(join(sFlat2,complement(complement(a)))),complement(join(complement(complement(a)),complement(complement(b))))),
inference(step,[status(thm)],[t1993,t91]) ).
cnf(t1995,plain,
sFlat17 = join(complement(join(sFlat2,a)),complement(join(complement(complement(a)),complement(complement(b))))),
inference(step,[status(thm)],[t1994,t32]) ).
cnf(t1996,plain,
sFlat17 = join(complement(join(sFlat2,sFlat1)),complement(join(complement(complement(a)),complement(complement(b))))),
inference(step,[status(thm)],[t1995,t39]) ).
cnf(t1997,plain,
sFlat17 = join(complement(join(sFlat1,sFlat2)),complement(join(complement(complement(a)),complement(complement(b))))),
inference(step,[status(thm)],[t1996,t97]) ).
cnf(t1998,plain,
sFlat17 = join(complement(sFlat12),complement(join(complement(complement(a)),complement(complement(b))))),
inference(step,[status(thm)],[t1997,t131]) ).
cnf(t1999,plain,
sFlat17 = join(complement(sFlat12),complement(join(complement(complement(b)),complement(complement(a))))),
inference(step,[status(thm)],[t1998,t97]) ).
cnf(t2000,plain,
sFlat17 = join(complement(sFlat12),complement(join(b,complement(complement(a))))),
inference(step,[status(thm)],[t1999,t32]) ).
cnf(t2001,plain,
sFlat17 = join(complement(sFlat12),complement(join(sFlat14,complement(complement(a))))),
inference(step,[status(thm)],[t2000,t41]) ).
cnf(t2002,plain,
sFlat17 = join(complement(sFlat12),complement(join(sFlat14,a))),
inference(step,[status(thm)],[t2001,t32]) ).
cnf(t2003,plain,
sFlat17 = join(complement(sFlat12),complement(join(sFlat14,sFlat1))),
inference(step,[status(thm)],[t2002,t39]) ).
cnf(t2004,plain,
sFlat17 = join(complement(sFlat12),complement(join(sFlat1,sFlat14))),
inference(step,[status(thm)],[t2003,t97]) ).
cnf(t2005,plain,
sFlat17 = join(complement(sFlat12),complement(sFlat15)),
inference(step,[status(thm)],[t2004,t126]) ).
cnf(t138,plain,
join(complement(sFlat12),complement(sFlat15)) = sFlat17,
inference(orient,[status(thm)],[t2005]) ).
cnf(t16,axiom,
sFlat7 = join(complement(join(a,complement(b))),complement(join(a,b))),
introduced(definition) ).
cnf(t2008,plain,
sFlat7 = join(complement(join(a,b)),complement(join(a,complement(b)))),
inference(step,[status(thm)],[t16,t97]) ).
cnf(t2009,plain,
sFlat7 = join(complement(join(b,a)),complement(join(a,complement(b)))),
inference(step,[status(thm)],[t2008,t97]) ).
cnf(t2010,plain,
sFlat7 = join(complement(join(sFlat14,a)),complement(join(a,complement(b)))),
inference(step,[status(thm)],[t2009,t41]) ).
cnf(t2011,plain,
sFlat7 = join(complement(join(sFlat14,sFlat1)),complement(join(a,complement(b)))),
inference(step,[status(thm)],[t2010,t39]) ).
cnf(t2012,plain,
sFlat7 = join(complement(join(sFlat1,sFlat14)),complement(join(a,complement(b)))),
inference(step,[status(thm)],[t2011,t97]) ).
cnf(t2013,plain,
sFlat7 = join(complement(sFlat15),complement(join(a,complement(b)))),
inference(step,[status(thm)],[t2012,t126]) ).
cnf(t2014,plain,
sFlat7 = join(complement(sFlat15),complement(join(sFlat1,complement(b)))),
inference(step,[status(thm)],[t2013,t39]) ).
cnf(t2015,plain,
sFlat7 = join(complement(sFlat15),complement(join(sFlat1,complement(sFlat14)))),
inference(step,[status(thm)],[t2014,t41]) ).
cnf(t2016,plain,
sFlat7 = join(complement(sFlat15),complement(join(sFlat1,sFlat2))),
inference(step,[status(thm)],[t2015,t91]) ).
cnf(t2017,plain,
sFlat7 = join(complement(sFlat15),complement(sFlat12)),
inference(step,[status(thm)],[t2016,t131]) ).
cnf(t2018,plain,
sFlat7 = join(complement(sFlat12),complement(sFlat15)),
inference(step,[status(thm)],[t2017,t97]) ).
cnf(t2019,plain,
sFlat7 = sFlat17,
inference(step,[status(thm)],[t2018,t138]) ).
cnf(t142,plain,
sFlat17 = sFlat7,
inference(orient,[status(thm)],[t2019]) ).
cnf(t2020,plain,
join(complement(sFlat12),complement(sFlat15)) = sFlat7,
inference(step,[status(thm)],[t138,t142]) ).
cnf(t143,plain,
join(complement(sFlat12),complement(sFlat15)) = sFlat7,
inference(orient,[status(thm)],[t2020]) ).
cnf(t2028,plain,
join(complement(sFlat3),complement(sFlat15)) = sFlat7,
inference(step,[status(thm)],[t143,t145]) ).
cnf(t148,plain,
join(complement(sFlat3),complement(sFlat15)) = sFlat7,
inference(rw,[status(thm)],[t2028]) ).
cnf(t2081,plain,
join(sFlat4,complement(sFlat15)) = sFlat7,
inference(step,[status(thm)],[t148,t198]) ).
cnf(t2082,plain,
join(sFlat4,complement(sFlat5)) = sFlat7,
inference(step,[status(thm)],[t2081,t151]) ).
cnf(t2083,plain,
join(sFlat4,sFlat6) = sFlat7,
inference(step,[status(thm)],[t2082,t168]) ).
cnf(t2084,plain,
complement(sFlat8) = sFlat7,
inference(step,[status(thm)],[t2083,t196]) ).
cnf(t215,plain,
complement(sFlat8) = sFlat7,
inference(orient,[status(thm)],[t2084]) ).
cnf(t2085,plain,
join(sFlat4,sFlat6) = sFlat7,
inference(step,[status(thm)],[t196,t215]) ).
cnf(t216,plain,
join(sFlat4,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t2085]) ).
cnf(t19,axiom,
sFlat10 = join(complement(complement(a)),complement(complement(join(complement(join(a,complement(b))),complement(join(a,b)))))),
introduced(definition) ).
cnf(t1919,plain,
sFlat10 = join(a,complement(complement(join(complement(join(a,complement(b))),complement(join(a,b)))))),
inference(step,[status(thm)],[t19,t32]) ).
cnf(t1920,plain,
sFlat10 = join(sFlat1,complement(complement(join(complement(join(a,complement(b))),complement(join(a,b)))))),
inference(step,[status(thm)],[t1919,t39]) ).
cnf(t1921,plain,
sFlat10 = join(sFlat1,join(complement(join(a,complement(b))),complement(join(a,b)))),
inference(step,[status(thm)],[t1920,t32]) ).
cnf(t1922,plain,
sFlat10 = join(sFlat1,join(complement(join(a,b)),complement(join(a,complement(b))))),
inference(step,[status(thm)],[t1921,t97]) ).
cnf(t1923,plain,
sFlat10 = join(sFlat1,join(complement(join(b,a)),complement(join(a,complement(b))))),
inference(step,[status(thm)],[t1922,t97]) ).
cnf(t1924,plain,
sFlat10 = join(sFlat1,join(complement(join(sFlat14,a)),complement(join(a,complement(b))))),
inference(step,[status(thm)],[t1923,t41]) ).
cnf(t1925,plain,
sFlat10 = join(sFlat1,join(complement(join(sFlat14,sFlat1)),complement(join(a,complement(b))))),
inference(step,[status(thm)],[t1924,t39]) ).
cnf(t1926,plain,
sFlat10 = join(sFlat1,join(complement(join(sFlat1,sFlat14)),complement(join(a,complement(b))))),
inference(step,[status(thm)],[t1925,t97]) ).
cnf(t1927,plain,
sFlat10 = join(sFlat1,join(sFlat6,complement(join(a,complement(b))))),
inference(step,[status(thm)],[t1926,t84]) ).
cnf(t1928,plain,
sFlat10 = join(sFlat1,join(sFlat6,complement(join(sFlat1,complement(b))))),
inference(step,[status(thm)],[t1927,t39]) ).
cnf(t1929,plain,
sFlat10 = join(sFlat1,join(sFlat6,complement(join(sFlat1,complement(sFlat14))))),
inference(step,[status(thm)],[t1928,t41]) ).
cnf(t1930,plain,
sFlat10 = join(sFlat1,join(sFlat6,complement(join(sFlat1,sFlat2)))),
inference(step,[status(thm)],[t1929,t91]) ).
cnf(t124,plain,
join(sFlat1,join(sFlat6,complement(join(sFlat1,sFlat2)))) = sFlat10,
inference(orient,[status(thm)],[t1930]) ).
cnf(t1960,plain,
join(sFlat1,join(sFlat6,complement(sFlat12))) = sFlat10,
inference(step,[status(thm)],[t124,t131]) ).
cnf(t133,plain,
join(sFlat1,join(sFlat6,complement(sFlat12))) = sFlat10,
inference(rw,[status(thm)],[t1960]) ).
cnf(t2185,plain,
join(sFlat1,join(sFlat6,complement(sFlat3))) = sFlat10,
inference(step,[status(thm)],[t133,t145]) ).
cnf(t2186,plain,
join(sFlat1,join(sFlat6,sFlat4)) = sFlat10,
inference(step,[status(thm)],[t2185,t198]) ).
cnf(t2187,plain,
join(sFlat1,join(sFlat4,sFlat6)) = sFlat10,
inference(step,[status(thm)],[t2186,t97]) ).
cnf(t2188,plain,
join(sFlat1,sFlat7) = sFlat10,
inference(step,[status(thm)],[t2187,t216]) ).
cnf(t847,plain,
join(sFlat1,sFlat7) = sFlat10,
inference(orient,[status(thm)],[t2188]) ).
cnf(t20,axiom,
sFlat11 = complement(join(complement(complement(a)),complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),
introduced(definition) ).
cnf(t1857,plain,
sFlat11 = complement(join(a,complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),
inference(step,[status(thm)],[t20,t32]) ).
cnf(t1858,plain,
sFlat11 = complement(join(sFlat1,complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),
inference(step,[status(thm)],[t1857,t39]) ).
cnf(t1859,plain,
sFlat11 = complement(join(sFlat1,join(complement(join(a,complement(b))),complement(join(a,b))))),
inference(step,[status(thm)],[t1858,t32]) ).
cnf(t1860,plain,
sFlat11 = complement(join(sFlat1,join(complement(join(sFlat1,complement(b))),complement(join(a,b))))),
inference(step,[status(thm)],[t1859,t39]) ).
cnf(t1861,plain,
sFlat11 = complement(join(sFlat1,join(complement(join(sFlat1,complement(sFlat14))),complement(join(a,b))))),
inference(step,[status(thm)],[t1860,t41]) ).
cnf(t1862,plain,
sFlat11 = complement(join(sFlat1,join(complement(join(sFlat1,complement(sFlat14))),complement(join(sFlat1,b))))),
inference(step,[status(thm)],[t1861,t39]) ).
cnf(t1863,plain,
sFlat11 = complement(join(sFlat1,join(complement(join(sFlat1,complement(sFlat14))),complement(join(sFlat1,sFlat14))))),
inference(step,[status(thm)],[t1862,t41]) ).
cnf(t49,plain,
complement(join(sFlat1,join(complement(join(sFlat1,complement(sFlat14))),complement(join(sFlat1,sFlat14))))) = sFlat11,
inference(orient,[status(thm)],[t1863]) ).
cnf(t1868,plain,
complement(join(sFlat1,join(complement(join(sFlat1,complement(sFlat14))),sFlat16))) = sFlat11,
inference(step,[status(thm)],[t49,t54]) ).
cnf(t59,plain,
complement(join(sFlat1,join(complement(join(sFlat1,complement(sFlat14))),sFlat16))) = sFlat11,
inference(rw,[status(thm)],[t1868]) ).
cnf(t2301,plain,
complement(join(sFlat1,join(sFlat16,complement(join(sFlat1,complement(sFlat14)))))) = sFlat11,
inference(step,[status(thm)],[t59,t97]) ).
cnf(t2302,plain,
complement(join(sFlat1,join(sFlat6,complement(join(sFlat1,complement(sFlat14)))))) = sFlat11,
inference(step,[status(thm)],[t2301,t83]) ).
cnf(t2303,plain,
complement(join(sFlat1,join(sFlat6,complement(join(sFlat1,sFlat2))))) = sFlat11,
inference(step,[status(thm)],[t2302,t91]) ).
cnf(t2304,plain,
complement(join(sFlat1,join(sFlat6,complement(sFlat3)))) = sFlat11,
inference(step,[status(thm)],[t2303,t146]) ).
cnf(t2305,plain,
complement(join(sFlat1,join(sFlat6,sFlat4))) = sFlat11,
inference(step,[status(thm)],[t2304,t198]) ).
cnf(t2306,plain,
complement(join(sFlat1,join(sFlat4,sFlat6))) = sFlat11,
inference(step,[status(thm)],[t2305,t97]) ).
cnf(t2307,plain,
complement(join(sFlat1,sFlat7)) = sFlat11,
inference(step,[status(thm)],[t2306,t216]) ).
cnf(t2308,plain,
complement(sFlat10) = sFlat11,
inference(step,[status(thm)],[t2307,t847]) ).
cnf(t1717,plain,
complement(sFlat10) = sFlat11,
inference(orient,[status(thm)],[t2308]) ).
cnf(t218,plain,
sFlat8 = complement(sFlat7),
inference(cp,[status(thm)],[t32,t215]) ).
cnf(t245,plain,
complement(sFlat7) = sFlat8,
inference(orient,[status(thm)],[t218]) ).
cnf(u1,axiom,
join(X,meet(X,Y)) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
meet(X,Y) = complement(join(complement(X),complement(Y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4,plain,
join(X1,complement(join(complement(X1),complement(X2)))) = X1,
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t33,plain,
join(X1,complement(join(complement(X1),complement(X2)))) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t35,plain,
X1 = join(X1,complement(join(complement(X1),X2))),
inference(cp,[status(thm)],[t33,t32]) ).
cnf(t472,plain,
join(X1,complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t35]) ).
cnf(t476,plain,
sFlat8 = join(sFlat8,complement(join(sFlat7,X1))),
inference(cp,[status(thm)],[t472,t215]) ).
cnf(t1276,plain,
join(sFlat8,complement(join(sFlat7,X1))) = sFlat8,
inference(orient,[status(thm)],[t476]) ).
cnf(t1280,plain,
sFlat8 = join(sFlat8,complement(join(X1,sFlat7))),
inference(cp,[status(thm)],[t1276,t97]) ).
cnf(t1837,plain,
join(sFlat8,complement(join(X1,sFlat7))) = sFlat8,
inference(orient,[status(thm)],[t1280]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t106,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t9,axiom,
sFlat0 = complement(a),
introduced(definition) ).
cnf(t1912,plain,
sFlat0 = complement(sFlat1),
inference(step,[status(thm)],[t9,t39]) ).
cnf(t86,plain,
complement(sFlat1) = sFlat0,
inference(orient,[status(thm)],[t1912]) ).
cnf(t87,plain,
sFlat1 = complement(sFlat0),
inference(cp,[status(thm)],[t32,t86]) ).
cnf(t155,plain,
complement(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t87]) ).
cnf(t482,plain,
sFlat0 = join(sFlat0,complement(join(sFlat1,X1))),
inference(cp,[status(thm)],[t472,t155]) ).
cnf(t1380,plain,
join(sFlat0,complement(join(sFlat1,X1))) = sFlat0,
inference(orient,[status(thm)],[t482]) ).
cnf(t132,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat12,X1),
inference(cp,[status(thm)],[t106,t131]) ).
cnf(t2098,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat3,X1),
inference(step,[status(thm)],[t132,t145]) ).
cnf(t289,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t2098]) ).
cnf(t36,plain,
X1 = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t33,t33]) ).
cnf(t2070,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t36,t32]) ).
cnf(t181,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t2070]) ).
cnf(t294,plain,
join(sFlat3,sFlat2) = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t289,t181]) ).
cnf(t2101,plain,
join(sFlat2,sFlat3) = join(sFlat1,sFlat2),
inference(step,[status(thm)],[t294,t97]) ).
cnf(t2102,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(step,[status(thm)],[t2101,t146]) ).
cnf(t302,plain,
join(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t2102]) ).
cnf(t303,plain,
join(sFlat3,sFlat3) = join(sFlat1,sFlat3),
inference(cp,[status(thm)],[t289,t302]) ).
cnf(t2103,plain,
sFlat3 = join(sFlat1,sFlat3),
inference(step,[status(thm)],[t303,t181]) ).
cnf(t305,plain,
join(sFlat1,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t2103]) ).
cnf(t1394,plain,
sFlat0 = join(sFlat0,complement(sFlat3)),
inference(cp,[status(thm)],[t1380,t305]) ).
cnf(t2261,plain,
sFlat0 = join(sFlat0,sFlat4),
inference(step,[status(thm)],[t1394,t198]) ).
cnf(t1412,plain,
join(sFlat0,sFlat4) = sFlat0,
inference(orient,[status(thm)],[t2261]) ).
cnf(t1418,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat0,X1),
inference(cp,[status(thm)],[t106,t1412]) ).
cnf(t1431,plain,
join(sFlat0,join(sFlat4,X1)) = join(sFlat0,X1),
inference(orient,[status(thm)],[t1418]) ).
cnf(t1434,plain,
join(sFlat0,sFlat6) = join(sFlat0,sFlat7),
inference(cp,[status(thm)],[t1431,t216]) ).
cnf(t183,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t106,t181]) ).
cnf(t317,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t183]) ).
cnf(t322,plain,
join(sFlat1,sFlat14) = join(sFlat1,sFlat5),
inference(cp,[status(thm)],[t317,t152]) ).
cnf(t2108,plain,
sFlat5 = join(sFlat1,sFlat5),
inference(step,[status(thm)],[t322,t152]) ).
cnf(t329,plain,
join(sFlat1,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t2108]) ).
cnf(t1393,plain,
sFlat0 = join(sFlat0,complement(sFlat5)),
inference(cp,[status(thm)],[t1380,t329]) ).
cnf(t2260,plain,
sFlat0 = join(sFlat0,sFlat6),
inference(step,[status(thm)],[t1393,t168]) ).
cnf(t1405,plain,
join(sFlat0,sFlat6) = sFlat0,
inference(orient,[status(thm)],[t2260]) ).
cnf(t2262,plain,
sFlat0 = join(sFlat0,sFlat7),
inference(step,[status(thm)],[t1434,t1405]) ).
cnf(t1438,plain,
join(sFlat0,sFlat7) = sFlat0,
inference(orient,[status(thm)],[t2262]) ).
cnf(t1838,plain,
sFlat8 = join(sFlat8,complement(sFlat0)),
inference(cp,[status(thm)],[t1837,t1438]) ).
cnf(t2322,plain,
sFlat8 = join(sFlat8,sFlat1),
inference(step,[status(thm)],[t1838,t155]) ).
cnf(t2323,plain,
sFlat8 = join(sFlat1,sFlat8),
inference(step,[status(thm)],[t2322,t97]) ).
cnf(t1845,plain,
join(sFlat1,sFlat8) = sFlat8,
inference(orient,[status(thm)],[t2323]) ).
cnf(t858,plain,
join(sFlat1,join(sFlat7,X1)) = join(sFlat10,X1),
inference(cp,[status(thm)],[t106,t847]) ).
cnf(t966,plain,
join(sFlat1,join(sFlat7,X1)) = join(sFlat10,X1),
inference(orient,[status(thm)],[t858]) ).
cnf(t1,axiom,
join(complement(X1),X1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1915,plain,
join(X1,complement(X1)) = n1,
inference(step,[status(thm)],[t1,t97]) ).
cnf(t114,plain,
join(X1,complement(X1)) = n1,
inference(orient,[status(thm)],[t1915]) ).
cnf(t1719,plain,
n1 = join(sFlat10,sFlat11),
inference(cp,[status(thm)],[t114,t1717]) ).
cnf(t1732,plain,
join(sFlat10,sFlat11) = n1,
inference(orient,[status(thm)],[t1719]) ).
cnf(u4,negated_conjecture,
join(a,join(meet(complement(a),meet(join(a,complement(b)),join(a,b))),meet(complement(a),join(meet(complement(a),b),meet(complement(a),complement(b)))))) != n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
join(a,join(complement(join(complement(complement(a)),complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(definition_unfolding,[status(thm)],[u4,d0]) ).
cnf(g0_0,plain,
join(sFlat1,join(complement(join(complement(complement(a)),complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[goal_0,t39]) ).
cnf(g0_1,plain,
join(sFlat1,join(complement(join(a,complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_0,t32]) ).
cnf(g0_2,plain,
join(sFlat1,join(complement(join(sFlat1,complement(complement(join(complement(join(a,complement(b))),complement(join(a,b))))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_1,t39]) ).
cnf(g0_3,plain,
join(sFlat1,join(complement(join(sFlat1,join(complement(join(a,complement(b))),complement(join(a,b))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_2,t32]) ).
cnf(g0_4,plain,
join(sFlat1,join(complement(join(sFlat1,join(complement(join(a,b)),complement(join(a,complement(b)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_3,t97]) ).
cnf(g0_5,plain,
join(sFlat1,join(complement(join(sFlat1,join(complement(join(b,a)),complement(join(a,complement(b)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_4,t97]) ).
cnf(g0_6,plain,
join(sFlat1,join(complement(join(sFlat1,join(complement(join(sFlat14,a)),complement(join(a,complement(b)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_5,t41]) ).
cnf(g0_7,plain,
join(sFlat1,join(complement(join(sFlat1,join(complement(join(sFlat14,sFlat1)),complement(join(a,complement(b)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_6,t39]) ).
cnf(g0_8,plain,
join(sFlat1,join(complement(join(sFlat1,join(complement(join(sFlat1,sFlat14)),complement(join(a,complement(b)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_7,t97]) ).
cnf(g0_9,plain,
join(sFlat1,join(complement(join(sFlat1,join(complement(sFlat5),complement(join(a,complement(b)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_8,t152]) ).
cnf(g0_10,plain,
join(sFlat1,join(complement(join(sFlat1,join(sFlat6,complement(join(a,complement(b)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_9,t168]) ).
cnf(g0_11,plain,
join(sFlat1,join(complement(join(sFlat1,join(sFlat6,complement(join(sFlat1,complement(b)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_10,t39]) ).
cnf(g0_12,plain,
join(sFlat1,join(complement(join(sFlat1,join(sFlat6,complement(join(sFlat1,complement(sFlat14)))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_11,t41]) ).
cnf(g0_13,plain,
join(sFlat1,join(complement(join(sFlat1,join(sFlat6,complement(join(sFlat1,sFlat2))))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_12,t91]) ).
cnf(g0_14,plain,
join(sFlat1,join(complement(join(sFlat1,join(sFlat6,complement(sFlat3)))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_13,t146]) ).
cnf(g0_15,plain,
join(sFlat1,join(complement(join(sFlat1,join(sFlat6,sFlat4))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_14,t198]) ).
cnf(g0_16,plain,
join(sFlat1,join(complement(join(sFlat1,join(sFlat4,sFlat6))),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_15,t97]) ).
cnf(g0_17,plain,
join(sFlat1,join(complement(join(sFlat1,sFlat7)),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_16,t216]) ).
cnf(g0_18,plain,
join(sFlat1,join(complement(sFlat10),complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_17,t847]) ).
cnf(g0_19,plain,
join(sFlat1,join(sFlat11,complement(join(complement(complement(a)),complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_18,t1717]) ).
cnf(g0_20,plain,
join(sFlat1,join(sFlat11,complement(join(a,complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_19,t32]) ).
cnf(g0_21,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(complement(join(complement(complement(a)),complement(b))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_20,t39]) ).
cnf(g0_22,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(complement(join(complement(b),complement(complement(a)))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_21,t97]) ).
cnf(g0_23,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(complement(join(complement(sFlat14),complement(complement(a)))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_22,t41]) ).
cnf(g0_24,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(complement(join(sFlat2,complement(complement(a)))),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_23,t91]) ).
cnf(g0_25,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(complement(join(sFlat2,a)),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_24,t32]) ).
cnf(g0_26,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(complement(join(sFlat2,sFlat1)),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_25,t39]) ).
cnf(g0_27,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(complement(join(sFlat1,sFlat2)),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_26,t97]) ).
cnf(g0_28,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(complement(sFlat3),complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_27,t146]) ).
cnf(g0_29,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,complement(join(complement(complement(a)),complement(complement(b)))))))))) != n1,
inference(rw,[status(thm)],[g0_28,t198]) ).
cnf(g0_30,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,complement(join(complement(complement(b)),complement(complement(a)))))))))) != n1,
inference(rw,[status(thm)],[g0_29,t97]) ).
cnf(g0_31,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,complement(join(b,complement(complement(a)))))))))) != n1,
inference(rw,[status(thm)],[g0_30,t32]) ).
cnf(g0_32,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,complement(join(sFlat14,complement(complement(a)))))))))) != n1,
inference(rw,[status(thm)],[g0_31,t41]) ).
cnf(g0_33,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,complement(join(sFlat14,a)))))))) != n1,
inference(rw,[status(thm)],[g0_32,t32]) ).
cnf(g0_34,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,complement(join(sFlat14,sFlat1)))))))) != n1,
inference(rw,[status(thm)],[g0_33,t39]) ).
cnf(g0_35,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,complement(join(sFlat1,sFlat14)))))))) != n1,
inference(rw,[status(thm)],[g0_34,t97]) ).
cnf(g0_36,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,complement(sFlat5))))))) != n1,
inference(rw,[status(thm)],[g0_35,t152]) ).
cnf(g0_37,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(join(sFlat4,sFlat6)))))) != n1,
inference(rw,[status(thm)],[g0_36,t168]) ).
cnf(g0_38,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,complement(sFlat7))))) != n1,
inference(rw,[status(thm)],[g0_37,t216]) ).
cnf(g0_39,plain,
join(sFlat1,join(sFlat11,complement(join(sFlat1,sFlat8)))) != n1,
inference(rw,[status(thm)],[g0_38,t245]) ).
cnf(g0_40,plain,
join(sFlat1,join(sFlat11,complement(sFlat8))) != n1,
inference(rw,[status(thm)],[g0_39,t1845]) ).
cnf(g0_41,plain,
join(sFlat1,join(sFlat11,sFlat7)) != n1,
inference(rw,[status(thm)],[g0_40,t215]) ).
cnf(g0_42,plain,
join(sFlat1,join(sFlat7,sFlat11)) != n1,
inference(rw,[status(thm)],[g0_41,t97]) ).
cnf(g0_43,plain,
join(sFlat10,sFlat11) != n1,
inference(rw,[status(thm)],[g0_42,t966]) ).
cnf(g0_44,plain,
n1 != n1,
inference(rw,[status(thm)],[g0_43,t1732]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_44]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT017-1 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.36 % Computer : n003.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Wed Sep 23 20:03:41 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.31/6.82 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.31/6.82 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------