%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN116-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 : Sun Sep 27 09:37:05 AM UTC 2026
% Result : Unsatisfiable 6.72s 1.33s
% Output : CNFRefutation 6.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 21
% Syntax : Number of formulae : 214 ( 214 unt; 0 def)
% Number of atoms : 214 ( 213 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-4 aty)
% Number of variables : 208 ( 92 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(axiom_1,axiom,
s0(d) = true,
file('theBenchmark.p',axiom_1) ).
cnf(c_2,plain,
s0(d) = true,
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_3,plain,
true = s0(d),
inference(copy,[status(thm)],[c_2]) ).
fof(axiom_2,axiom,
q0(e,d) = true,
file('theBenchmark.p',axiom_2) ).
cnf(c_4,plain,
q0(e,d) = true,
inference(clausify,[status(thm)],[axiom_2]) ).
cnf(c_1895,plain,
q0(e,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_4]) ).
cnf(c_5,plain,
s0(d) = q0(e,d),
inference(copy,[status(thm)],[c_1895]) ).
fof(axiom_5,axiom,
s0(b) = true,
file('theBenchmark.p',axiom_5) ).
cnf(c_10,plain,
s0(b) = true,
inference(clausify,[status(thm)],[axiom_5]) ).
cnf(c_1896,plain,
s0(b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_10]) ).
cnf(c_11,plain,
s0(b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1896]) ).
fof(axiom_6,axiom,
q0(b,b) = true,
file('theBenchmark.p',axiom_6) ).
cnf(c_12,plain,
q0(b,b) = true,
inference(clausify,[status(thm)],[axiom_6]) ).
cnf(c_1897,plain,
q0(b,b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_12]) ).
cnf(c_1898,plain,
q0(b,b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1897]) ).
cnf(c_13,plain,
q0(e,d) = q0(b,b),
inference(copy,[status(thm)],[c_1898]) ).
fof(axiom_10,axiom,
p0(b,d) = true,
file('theBenchmark.p',axiom_10) ).
cnf(c_20,plain,
p0(b,d) = true,
inference(clausify,[status(thm)],[axiom_10]) ).
cnf(c_1899,plain,
p0(b,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_20]) ).
cnf(c_1900,plain,
p0(b,d) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1899]) ).
cnf(c_1901,plain,
p0(b,d) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_1900]) ).
cnf(c_21,plain,
q0(b,b) = p0(b,d),
inference(copy,[status(thm)],[c_1901]) ).
fof(axiom_13,axiom,
r0(e) = true,
file('theBenchmark.p',axiom_13) ).
cnf(c_26,plain,
r0(e) = true,
inference(clausify,[status(thm)],[axiom_13]) ).
cnf(c_1902,plain,
r0(e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_26]) ).
cnf(c_1903,plain,
r0(e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1902]) ).
cnf(c_1904,plain,
r0(e) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_1903]) ).
cnf(c_27,plain,
r0(e) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_1904]) ).
fof(axiom_14,axiom,
! [VAR_0] : p0(b,VAR_0) = true,
file('theBenchmark.p',axiom_14) ).
cnf(c_28,plain,
p0(b,A) = true,
inference(clausify,[status(thm)],[axiom_14]) ).
cnf(c_1905,plain,
p0(b,A) = s0(d),
inference(paramod,[status(thm)],[c_3,c_28]) ).
cnf(c_1906,plain,
p0(b,A) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1905]) ).
cnf(c_1907,plain,
p0(b,A) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_1906]) ).
cnf(c_1908,plain,
p0(b,A) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_1907]) ).
cnf(c_29,plain,
p0(b,d) = p0(b,A),
inference(copy,[status(thm)],[c_1908]) ).
fof(axiom_17,axiom,
! [VAR_0] : q0(VAR_0,d) = true,
file('theBenchmark.p',axiom_17) ).
cnf(c_34,plain,
q0(A,d) = true,
inference(clausify,[status(thm)],[axiom_17]) ).
cnf(c_1909,plain,
q0(A,d) = s0(d),
inference(paramod,[status(thm)],[c_3,c_34]) ).
cnf(c_1910,plain,
q0(A,d) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1909]) ).
cnf(c_1911,plain,
q0(A,d) = q0(b,b),
inference(paramod,[status(thm)],[c_13,c_1910]) ).
cnf(c_35,plain,
q0(A,d) = p0(b,d),
inference(paramod,[status(thm)],[c_21,c_1911]) ).
fof(axiom_28,axiom,
k0(e) = true,
file('theBenchmark.p',axiom_28) ).
cnf(c_54,plain,
k0(e) = true,
inference(clausify,[status(thm)],[axiom_28]) ).
cnf(c_1912,plain,
k0(e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_54]) ).
cnf(c_1913,plain,
k0(e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1912]) ).
cnf(c_55,plain,
k0(e) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1913]) ).
fof(axiom_30,axiom,
n0(e,e) = true,
file('theBenchmark.p',axiom_30) ).
cnf(c_58,plain,
n0(e,e) = true,
inference(clausify,[status(thm)],[axiom_30]) ).
cnf(c_1914,plain,
n0(e,e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_58]) ).
cnf(c_1915,plain,
n0(e,e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1914]) ).
cnf(c_59,plain,
n0(e,e) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1915]) ).
fof(axiom_32,axiom,
k0(b) = true,
file('theBenchmark.p',axiom_32) ).
cnf(c_62,plain,
k0(b) = true,
inference(clausify,[status(thm)],[axiom_32]) ).
cnf(c_1916,plain,
k0(b) = s0(d),
inference(paramod,[status(thm)],[c_3,c_62]) ).
cnf(c_1917,plain,
k0(b) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1916]) ).
cnf(c_63,plain,
k0(b) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1917]) ).
fof(rule_001,axiom,
! [VAR_0,VAR_1] : ifeq(n0(VAR_0,VAR_1),true,k1(VAR_1),true) = true,
file('theBenchmark.p',rule_001) ).
cnf(c_76,plain,
ifeq(n0(A,B),true,k1(B),true) = true,
inference(clausify,[status(thm)],[rule_001]) ).
cnf(c_1918,plain,
ifeq(n0(A,B),s0(d),k1(B),true) = true,
inference(paramod,[status(thm)],[c_3,c_76]) ).
cnf(c_1919,plain,
ifeq(n0(A,B),q0(e,d),k1(B),true) = true,
inference(paramod,[status(thm)],[c_5,c_1918]) ).
cnf(c_1920,plain,
ifeq(n0(A,B),p0(b,d),k1(B),true) = true,
inference(paramod,[status(thm)],[c_35,c_1919]) ).
cnf(c_1921,plain,
ifeq(n0(A,B),p0(b,d),k1(B),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_1920]) ).
cnf(c_1922,plain,
ifeq(n0(A,B),p0(b,d),k1(B),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_1921]) ).
cnf(c_1923,plain,
ifeq(n0(A,B),p0(b,d),k1(B),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_1922]) ).
cnf(c_1924,plain,
ifeq(n0(A,B),p0(b,d),k1(B),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_1923]) ).
cnf(c_1925,plain,
ifeq(n0(A,B),p0(b,d),k1(B),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1924]) ).
cnf(c_77,plain,
ifeq(n0(A,B),p0(b,d),k1(B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1925]) ).
fof(rule_002,axiom,
! [VAR_0,VAR_1] : ifeq(n0(VAR_0,VAR_1),true,l1(VAR_1,VAR_1),true) = true,
file('theBenchmark.p',rule_002) ).
cnf(c_78,plain,
ifeq(n0(A,B),true,l1(B,B),true) = true,
inference(clausify,[status(thm)],[rule_002]) ).
cnf(c_1926,plain,
ifeq(n0(A,B),s0(d),l1(B,B),true) = true,
inference(paramod,[status(thm)],[c_3,c_78]) ).
cnf(c_1927,plain,
ifeq(n0(A,B),q0(e,d),l1(B,B),true) = true,
inference(paramod,[status(thm)],[c_5,c_1926]) ).
cnf(c_1928,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),true) = true,
inference(paramod,[status(thm)],[c_35,c_1927]) ).
cnf(c_1929,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_1928]) ).
cnf(c_1930,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_1929]) ).
cnf(c_1931,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_1930]) ).
cnf(c_1932,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_1931]) ).
cnf(c_1933,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1932]) ).
cnf(c_79,plain,
ifeq(n0(A,B),p0(b,d),l1(B,B),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1933]) ).
fof(rule_061,axiom,
! [VAR_0] : ifeq(k0(VAR_0),true,ifeq(s0(VAR_0),true,n1(VAR_0,VAR_0,VAR_0),true),true) = true,
file('theBenchmark.p',rule_061) ).
cnf(c_191,plain,
ifeq(k0(A),true,ifeq(s0(A),true,n1(A,A,A),true),true) = true,
inference(clausify,[status(thm)],[rule_061]) ).
cnf(c_1934,plain,
ifeq(k0(A),s0(d),ifeq(s0(A),true,n1(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_191]) ).
cnf(c_1935,plain,
ifeq(k0(A),q0(e,d),ifeq(s0(A),true,n1(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_1934]) ).
cnf(c_1936,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),true,n1(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_1935]) ).
cnf(c_1937,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),s0(d),n1(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_1936]) ).
cnf(c_1938,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),q0(e,d),n1(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_1937]) ).
cnf(c_1939,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_1938]) ).
cnf(c_1940,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_1939]) ).
cnf(c_1941,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_1940]) ).
cnf(c_1942,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_1941]) ).
cnf(c_1943,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_1942]) ).
cnf(c_1944,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_1943]) ).
cnf(c_1945,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_1944]) ).
cnf(c_1946,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_1945]) ).
cnf(c_1947,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1946]) ).
cnf(c_192,plain,
ifeq(k0(A),p0(b,d),ifeq(s0(A),p0(b,d),n1(A,A,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1947]) ).
fof(rule_090,axiom,
ifeq(k0(e),true,ifeq(r0(e),true,p1(e,e,e),true),true) = true,
file('theBenchmark.p',rule_090) ).
cnf(c_246,plain,
ifeq(k0(e),true,ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(clausify,[status(thm)],[rule_090]) ).
cnf(c_1948,plain,
ifeq(p0(b,d),true,ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_55,c_246]) ).
cnf(c_1949,plain,
ifeq(p0(b,d),s0(d),ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_1948]) ).
cnf(c_1950,plain,
ifeq(p0(b,d),q0(e,d),ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_1949]) ).
cnf(c_1951,plain,
ifeq(p0(b,d),p0(b,d),ifeq(r0(e),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_1950]) ).
cnf(c_1952,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),true,p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_27,c_1951]) ).
cnf(c_1953,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),s0(d),p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_1952]) ).
cnf(c_1954,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),q0(e,d),p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_1953]) ).
cnf(c_1955,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(e,e,e),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_1954]) ).
cnf(c_1956,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(e,e,e),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_1955]) ).
cnf(c_1957,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(e,e,e),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_1956]) ).
cnf(c_1958,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p1(e,e,e),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_1957]) ).
cnf(c_1959,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),true) = true,
inference(paramod,[status(thm)],[c_1,c_1958]) ).
cnf(c_1960,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_1959]) ).
cnf(c_1961,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_1960]) ).
cnf(c_1962,plain,
ifeq(p0(b,d),p0(b,d),p1(e,e,e),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_1961]) ).
cnf(c_1963,plain,
p1(e,e,e) = true,
inference(paramod,[status(thm)],[c_1,c_1962]) ).
cnf(c_1964,plain,
p1(e,e,e) = s0(d),
inference(paramod,[status(thm)],[c_3,c_1963]) ).
cnf(c_1965,plain,
p1(e,e,e) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1964]) ).
cnf(c_247,plain,
p1(e,e,e) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1965]) ).
fof(rule_137,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(p1(VAR_0,VAR_1,VAR_2),true,n2(VAR_2),true) = true,
file('theBenchmark.p',rule_137) ).
cnf(c_335,plain,
ifeq(p1(A,B,C),true,n2(C),true) = true,
inference(clausify,[status(thm)],[rule_137]) ).
cnf(c_1966,plain,
ifeq(p1(A,B,C),s0(d),n2(C),true) = true,
inference(paramod,[status(thm)],[c_3,c_335]) ).
cnf(c_1967,plain,
ifeq(p1(A,B,C),q0(e,d),n2(C),true) = true,
inference(paramod,[status(thm)],[c_5,c_1966]) ).
cnf(c_1968,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),true) = true,
inference(paramod,[status(thm)],[c_35,c_1967]) ).
cnf(c_1969,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_1968]) ).
cnf(c_1970,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_1969]) ).
cnf(c_1971,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_1970]) ).
cnf(c_1972,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_1971]) ).
cnf(c_1973,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1972]) ).
cnf(c_336,plain,
ifeq(p1(A,B,C),p0(b,d),n2(C),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1973]) ).
fof(rule_249,axiom,
! [VAR_0] : ifeq(n2(VAR_0),true,ifeq(k1(VAR_0),true,p3(VAR_0,VAR_0,VAR_0),true),true) = true,
file('theBenchmark.p',rule_249) ).
cnf(c_555,plain,
ifeq(n2(A),true,ifeq(k1(A),true,p3(A,A,A),true),true) = true,
inference(clausify,[status(thm)],[rule_249]) ).
cnf(c_1974,plain,
ifeq(n2(A),s0(d),ifeq(k1(A),true,p3(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_555]) ).
cnf(c_1975,plain,
ifeq(n2(A),q0(e,d),ifeq(k1(A),true,p3(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_1974]) ).
cnf(c_1976,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),true,p3(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_1975]) ).
cnf(c_1977,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),s0(d),p3(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_1976]) ).
cnf(c_1978,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),q0(e,d),p3(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_1977]) ).
cnf(c_1979,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_1978]) ).
cnf(c_1980,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_1979]) ).
cnf(c_1981,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_1980]) ).
cnf(c_1982,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_1981]) ).
cnf(c_1983,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_1982]) ).
cnf(c_1984,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_1983]) ).
cnf(c_1985,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_1984]) ).
cnf(c_1986,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_1985]) ).
cnf(c_1987,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_1986]) ).
cnf(c_556,plain,
ifeq(n2(A),p0(b,d),ifeq(k1(A),p0(b,d),p3(A,A,A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_1987]) ).
fof(rule_299,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq(p3(VAR_0,VAR_1,VAR_2),true,ifeq(l1(VAR_3,VAR_1),true,s4(VAR_3),true),true) = true,
file('theBenchmark.p',rule_299) ).
cnf(c_651,plain,
ifeq(p3(A,B,C),true,ifeq(l1(D,B),true,s4(D),true),true) = true,
inference(clausify,[status(thm)],[rule_299]) ).
cnf(c_1988,plain,
ifeq(p3(A,B,C),s0(d),ifeq(l1(D,B),true,s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_651]) ).
cnf(c_1989,plain,
ifeq(p3(A,B,C),q0(e,d),ifeq(l1(D,B),true,s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_1988]) ).
cnf(c_1990,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),true,s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_1989]) ).
cnf(c_1991,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),s0(d),s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_1990]) ).
cnf(c_1992,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),q0(e,d),s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_1991]) ).
cnf(c_1993,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_1992]) ).
cnf(c_1994,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_1993]) ).
cnf(c_1995,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_1994]) ).
cnf(c_1996,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_1995]) ).
cnf(c_1997,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_1996]) ).
cnf(c_1998,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_1997]) ).
cnf(c_1999,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_1998]) ).
cnf(c_2000,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_1999]) ).
cnf(c_2001,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_2000]) ).
cnf(c_652,plain,
ifeq(p3(A,B,C),p0(b,d),ifeq(l1(D,B),p0(b,d),s4(D),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_2001]) ).
fof(rule_301,axiom,
ifeq(s4(e),true,ifeq(n1(b,b,b),true,k5(b),true),true) = true,
file('theBenchmark.p',rule_301) ).
cnf(c_655,plain,
ifeq(s4(e),true,ifeq(n1(b,b,b),true,k5(b),true),true) = true,
inference(clausify,[status(thm)],[rule_301]) ).
cnf(c_2002,plain,
ifeq(s4(e),s0(d),ifeq(n1(b,b,b),true,k5(b),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_655]) ).
cnf(c_2003,plain,
ifeq(s4(e),q0(e,d),ifeq(n1(b,b,b),true,k5(b),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_2002]) ).
cnf(c_2004,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),true,k5(b),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_2003]) ).
cnf(c_2005,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),s0(d),k5(b),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_2004]) ).
cnf(c_2006,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),q0(e,d),k5(b),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_2005]) ).
cnf(c_2007,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),true),true) = true,
inference(paramod,[status(thm)],[c_35,c_2006]) ).
cnf(c_2008,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),s0(d)),true) = true,
inference(paramod,[status(thm)],[c_3,c_2007]) ).
cnf(c_2009,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),q0(e,d)),true) = true,
inference(paramod,[status(thm)],[c_5,c_2008]) ).
cnf(c_2010,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),p0(b,d)),true) = true,
inference(paramod,[status(thm)],[c_35,c_2009]) ).
cnf(c_2011,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),p0(b,d)),s0(d)) = true,
inference(paramod,[status(thm)],[c_3,c_2010]) ).
cnf(c_2012,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),p0(b,d)),q0(e,d)) = true,
inference(paramod,[status(thm)],[c_5,c_2011]) ).
cnf(c_2013,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),p0(b,d)),p0(b,d)) = true,
inference(paramod,[status(thm)],[c_35,c_2012]) ).
cnf(c_2014,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),p0(b,d)),p0(b,d)) = s0(d),
inference(paramod,[status(thm)],[c_3,c_2013]) ).
cnf(c_2015,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),p0(b,d)),p0(b,d)) = q0(e,d),
inference(paramod,[status(thm)],[c_5,c_2014]) ).
cnf(c_656,plain,
ifeq(s4(e),p0(b,d),ifeq(n1(b,b,b),p0(b,d),k5(b),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_2015]) ).
fof(prove_this,axiom,
k5(b) != true,
file('theBenchmark.p',prove_this) ).
cnf(c_715,plain,
k5(b) != true,
inference(clausify,[status(thm)],[prove_this]) ).
cnf(c_2016,plain,
k5(b) != s0(d),
inference(paramod,[status(thm)],[c_3,c_715]) ).
cnf(c_2017,plain,
k5(b) != q0(e,d),
inference(paramod,[status(thm)],[c_5,c_2016]) ).
cnf(c_716,plain,
k5(b) != p0(b,d),
inference(paramod,[status(thm)],[c_35,c_2017]) ).
cnf(c_718,plain,
s0(b) = p0(b,d),
inference(paramod,[status(thm)],[c_35,c_11]) ).
cnf(c_725,plain,
p0(b,A) = p0(b,B),
inference(paramod,[status(thm)],[c_29,c_29]) ).
cnf(c_2018,plain,
ifeq(p0(b,d),p0(b,d),k1(e),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_59,c_77]) ).
cnf(c_728,plain,
k1(e) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2018]) ).
cnf(c_2019,plain,
ifeq(p0(b,d),p0(b,d),l1(e,e),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_59,c_79]) ).
cnf(c_736,plain,
l1(e,e) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2019]) ).
cnf(c_2020,plain,
ifeq(p0(b,d),p0(b,d),ifeq(s0(b),p0(b,d),n1(b,b,b),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_63,c_192]) ).
cnf(c_2021,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),n1(b,b,b),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_718,c_2020]) ).
cnf(c_2022,plain,
ifeq(p0(b,d),p0(b,d),n1(b,b,b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2021]) ).
cnf(c_821,plain,
n1(b,b,b) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2022]) ).
cnf(c_2023,plain,
ifeq(s4(e),p0(b,d),ifeq(p0(b,d),p0(b,d),k5(b),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_821,c_656]) ).
cnf(c_824,plain,
ifeq(s4(e),p0(b,d),k5(b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2023]) ).
cnf(c_2024,plain,
ifeq(p0(b,d),p0(b,d),n2(e),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_247,c_336]) ).
cnf(c_925,plain,
n2(e) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2024]) ).
cnf(c_1125,plain,
k5(b) != p0(b,A),
inference(paramod,[status(thm)],[c_725,c_716]) ).
cnf(c_2025,plain,
ifeq(n2(e),p0(b,d),ifeq(p0(b,d),p0(b,d),p3(e,e,e),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_728,c_556]) ).
cnf(c_2026,plain,
ifeq(p0(b,d),p0(b,d),ifeq(p0(b,d),p0(b,d),p3(e,e,e),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_925,c_2025]) ).
cnf(c_2027,plain,
ifeq(p0(b,d),p0(b,d),p3(e,e,e),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2026]) ).
cnf(c_1141,plain,
p3(e,e,e) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2027]) ).
cnf(c_2028,plain,
ifeq(p0(b,d),p0(b,d),ifeq(l1(A,e),p0(b,d),s4(A),p0(b,d)),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1141,c_652]) ).
cnf(c_1267,plain,
ifeq(l1(A,e),p0(b,d),s4(A),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2028]) ).
cnf(c_1285,plain,
ifeq(s4(e),p0(b,A),k5(b),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_824]) ).
cnf(c_1392,plain,
ifeq(s4(e),p0(b,A),k5(b),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_725,c_1285]) ).
cnf(c_2029,plain,
ifeq(p0(b,d),p0(b,d),s4(e),p0(b,d)) = p0(b,d),
inference(paramod,[status(thm)],[c_736,c_1267]) ).
cnf(c_1647,plain,
s4(e) = p0(b,d),
inference(paramod,[status(thm)],[c_1,c_2029]) ).
cnf(c_1650,plain,
ifeq(p0(b,d),p0(b,A),k5(b),p0(b,B)) = p0(b,d),
inference(paramod,[status(thm)],[c_1647,c_1392]) ).
cnf(c_2030,plain,
p0(b,d) = k5(b),
inference(paramod,[status(thm)],[c_1650,c_1]) ).
cnf(c_1893,plain,
k5(b) = p0(b,d),
inference(copy,[status(thm)],[c_2030]) ).
cnf(c_1894,plain,
$false,
inference(resolve,[status(thm)],[c_1893,c_1125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN116-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 17:17:58 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2303453 was started by sandbox2 on n001,
% 0.09/0.37 % Sat Sep 26 17:17:58 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 6.72/1.33
% 6.72/1.33 % given #500 (A,wt=24): 873 ifeq(n0(A,B),p0(b,d),q1(b,B,b),p0(b,d)) = p0(b,d). [para(37(a,1),251(a,1,1)),rewrite([1(21)])].
% 6.72/1.33
% 6.72/1.33 % SZS status Unsatisfiable for theBenchmark
% 6.72/1.33
% 6.72/1.33 % Proof 1 at 0.53 (+ 0.07) seconds.
% 6.72/1.33 % Length of proof is 57.
% 6.72/1.33 % Level of proof is 14.
% 6.72/1.33 % Maximum clause weight is 35.000.
% 6.72/1.33 % Given clauses 622.
% 6.72/1.33
% 6.72/1.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------