%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV022-2 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:34:22 AM UTC 2026
% Result : Unsatisfiable 142.63s 34.40s
% Output : CNFRefutation 142.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 26
% Syntax : Number of formulae : 126 ( 46 unt; 0 def)
% Number of atoms : 250 ( 110 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 199 ( 75 ~; 124 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-2 aty)
% Number of variables : 106 ( 4 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_63,axiom,
! [VAR_0,VAR_1,VAR_2] :
( f_SUB_(VAR_1,VAR_0) = VAR_2
| f_ADD_(VAR_2,VAR_0) != VAR_1
| def_89(VAR_0,VAR_1) ),
file('theBenchmark.p',axiom_63) ).
cnf(c_2,plain,
( f_SUB_(B,A) = C
| f_ADD_(C,A) != B
| def_89(A,B) ),
inference(clausify,[status(thm)],[axiom_63]) ).
fof(axiom_65,axiom,
! [VAR_0,VAR_1] :
( ~ def_89(VAR_1,VAR_0)
| p_LES_EQU_(VAR_0,VAR_1) ),
file('theBenchmark.p',axiom_65) ).
cnf(c_4,plain,
( ~ def_89(B,A)
| p_LES_EQU_(A,B) ),
inference(clausify,[status(thm)],[axiom_65]) ).
cnf(c_6,plain,
( f_SUB_(A,B) = C
| f_ADD_(C,B) != A
| p_LES_EQU_(A,B) ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
fof(quest_5,axiom,
fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) != fwork_DOTfifo_DOTrtl_DOTfifo__length_,
file('theBenchmark.p',quest_5) ).
cnf(c_9,plain,
fwork_DOTfifo_DOTrtl_DOTlevel_(f_ADD_(t_206,n1)) != fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(clausify,[status(thm)],[quest_5]) ).
fof(quest_4,axiom,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)),
file('theBenchmark.p',quest_4) ).
cnf(c_10,plain,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206)),
inference(clausify,[status(thm)],[quest_4]) ).
fof(quest_3,axiom,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)),
file('theBenchmark.p',quest_3) ).
cnf(c_11,plain,
~ p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206)),
inference(clausify,[status(thm)],[quest_3]) ).
fof(quest_2,axiom,
p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)),
file('theBenchmark.p',quest_2) ).
cnf(c_12,plain,
p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206)),
inference(clausify,[status(thm)],[quest_2]) ).
fof(quest_1,axiom,
f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_,
file('theBenchmark.p',quest_1) ).
cnf(c_13,plain,
f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(clausify,[status(thm)],[quest_1]) ).
cnf(c_14,plain,
fwork_DOTfifo_DOTrtl_DOTfifo__length_ = f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1),
inference(copy,[status(thm)],[c_13]) ).
fof(axiom_132,axiom,
! [VAR_0,VAR_1] :
( p__pred_(f__gt_(VAR_0,VAR_1))
| p_LES_EQU_(VAR_0,VAR_1) ),
file('theBenchmark.p',axiom_132) ).
cnf(c_17,plain,
( p__pred_(f__gt_(A,B))
| p_LES_EQU_(A,B) ),
inference(clausify,[status(thm)],[axiom_132]) ).
fof(axiom_131,axiom,
! [VAR_0,VAR_1] :
( ~ p__pred_(f__gt_(VAR_0,VAR_1))
| ~ p_LES_EQU_(VAR_0,VAR_1) ),
file('theBenchmark.p',axiom_131) ).
cnf(c_18,plain,
( ~ p__pred_(f__gt_(A,B))
| ~ p_LES_EQU_(A,B) ),
inference(clausify,[status(thm)],[axiom_131]) ).
fof(axiom_128,axiom,
! [VAR_0,VAR_1] :
( p__pred_(f__lt_(VAR_1,VAR_0))
| p_LES_EQU_(VAR_0,VAR_1) ),
file('theBenchmark.p',axiom_128) ).
cnf(c_21,plain,
( p__pred_(f__lt_(B,A))
| p_LES_EQU_(A,B) ),
inference(clausify,[status(thm)],[axiom_128]) ).
fof(axiom_127,axiom,
! [VAR_0,VAR_1] :
( ~ p__pred_(f__lt_(VAR_1,VAR_0))
| ~ p_LES_EQU_(VAR_0,VAR_1) ),
file('theBenchmark.p',axiom_127) ).
cnf(c_22,plain,
( ~ p__pred_(f__lt_(B,A))
| ~ p_LES_EQU_(A,B) ),
inference(clausify,[status(thm)],[axiom_127]) ).
fof(axiom_80,axiom,
f__length_(f__empty_) = n0,
file('theBenchmark.p',axiom_80) ).
cnf(c_80,plain,
f__length_(f__empty_) = n0,
inference(clausify,[status(thm)],[axiom_80]) ).
cnf(c_81,plain,
n0 = f__length_(f__empty_),
inference(copy,[status(thm)],[c_80]) ).
fof(axiom_77,axiom,
! [VAR_0] : f_ADD_(n0,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_77) ).
cnf(c_86,plain,
f_ADD_(n0,A) = A,
inference(clausify,[status(thm)],[axiom_77]) ).
fof(axiom_76,axiom,
! [VAR_0,VAR_1] :
( f_ADD_(VAR_0,n1) != f_ADD_(VAR_1,n1)
| VAR_0 = VAR_1 ),
file('theBenchmark.p',axiom_76) ).
cnf(c_87,plain,
( f_ADD_(A,n1) != f_ADD_(B,n1)
| A = B ),
inference(clausify,[status(thm)],[axiom_76]) ).
fof(axiom_75,axiom,
! [VAR_0] : p_LES_EQU_(VAR_0,VAR_0),
file('theBenchmark.p',axiom_75) ).
cnf(c_88,plain,
p_LES_EQU_(A,A),
inference(clausify,[status(thm)],[axiom_75]) ).
fof(axiom_74,axiom,
! [VAR_0] :
( VAR_0 = n0
| VAR_0 = f_ADD_(y_105(VAR_0),n1) ),
file('theBenchmark.p',axiom_74) ).
cnf(c_89,plain,
( A = n0
| A = f_ADD_(y_105(A),n1) ),
inference(clausify,[status(thm)],[axiom_74]) ).
cnf(c_11747,plain,
( A = n0
| f_ADD_(y_105(A),n1) = A ),
inference(copy,[status(thm)],[c_89]) ).
cnf(c_90,plain,
( n0 = A
| f_ADD_(y_105(A),n1) = A ),
inference(copy,[status(thm)],[c_11747]) ).
fof(axiom_71,axiom,
! [VAR_0,VAR_1,VAR_2] :
( p_LES_EQU_(VAR_0,VAR_2)
| p_LES_EQU_(VAR_2,VAR_1)
| ~ p_LES_EQU_(VAR_0,VAR_1) ),
file('theBenchmark.p',axiom_71) ).
cnf(c_94,plain,
( p_LES_EQU_(A,C)
| p_LES_EQU_(C,B)
| ~ p_LES_EQU_(A,B) ),
inference(clausify,[status(thm)],[axiom_71]) ).
fof(axiom_70,axiom,
! [VAR_0,VAR_1] :
( ~ p_LES_EQU_(VAR_1,VAR_0)
| ~ p_LES_EQU_(VAR_0,VAR_1)
| VAR_0 = VAR_1 ),
file('theBenchmark.p',axiom_70) ).
cnf(c_95,plain,
( ~ p_LES_EQU_(B,A)
| ~ p_LES_EQU_(A,B)
| A = B ),
inference(clausify,[status(thm)],[axiom_70]) ).
fof(axiom_67,axiom,
! [VAR_0,VAR_1] :
( ~ p_LES_EQU_(VAR_0,VAR_1)
| p_LES_EQU_(f_ADD_(VAR_0,n1),f_ADD_(VAR_1,n1)) ),
file('theBenchmark.p',axiom_67) ).
cnf(c_98,plain,
( ~ p_LES_EQU_(A,B)
| p_LES_EQU_(f_ADD_(A,n1),f_ADD_(B,n1)) ),
inference(clausify,[status(thm)],[axiom_67]) ).
fof(axiom_66,axiom,
! [VAR_0,VAR_1] :
( p_LES_EQU_(VAR_0,VAR_1)
| ~ p_LES_EQU_(f_ADD_(VAR_0,n1),f_ADD_(VAR_1,n1)) ),
file('theBenchmark.p',axiom_66) ).
cnf(c_99,plain,
( p_LES_EQU_(A,B)
| ~ p_LES_EQU_(f_ADD_(A,n1),f_ADD_(B,n1)) ),
inference(clausify,[status(thm)],[axiom_66]) ).
fof(axiom_61,axiom,
! [VAR_0] :
( p_LES_EQU_(VAR_0,n0)
| ~ p_LES_EQU_(VAR_0,f_SUB_(VAR_0,n1)) ),
file('theBenchmark.p',axiom_61) ).
cnf(c_100,plain,
( p_LES_EQU_(A,n0)
| ~ p_LES_EQU_(A,f_SUB_(A,n1)) ),
inference(clausify,[status(thm)],[axiom_61]) ).
fof(axiom_60,axiom,
! [VAR_0] : ~ p_LES_EQU_(f_ADD_(VAR_0,n1),n0),
file('theBenchmark.p',axiom_60) ).
cnf(c_101,plain,
~ p_LES_EQU_(f_ADD_(A,n1),n0),
inference(clausify,[status(thm)],[axiom_60]) ).
fof(axiom_59,axiom,
! [VAR_0] : f_ADD_(VAR_0,n1) != n0,
file('theBenchmark.p',axiom_59) ).
cnf(c_102,plain,
f_ADD_(A,n1) != n0,
inference(clausify,[status(thm)],[axiom_59]) ).
fof(axiom_23,axiom,
! [VAR_0] :
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(VAR_0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(VAR_0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(VAR_0))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(VAR_0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(VAR_0,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(VAR_0) ),
file('theBenchmark.p',axiom_23) ).
cnf(c_144,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(A))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(A))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(A))
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(A))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(A,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(A) ),
inference(clausify,[status(thm)],[axiom_23]) ).
fof(axiom_18,axiom,
! [VAR_0] :
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(VAR_0))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(VAR_0))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(VAR_0))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(VAR_0))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(VAR_0,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(VAR_0),n1) ),
file('theBenchmark.p',axiom_18) ).
cnf(c_151,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(A))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(A))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(A))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(A))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(A,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(A),n1) ),
inference(clausify,[status(thm)],[axiom_18]) ).
fof(axiom_5,axiom,
! [VAR_0] : fwork_DOTfifo_DOTrtl_DOTlevel_(VAR_0) = fwork_DOTfifo_DOTrtl_DOTint__level_(VAR_0),
file('theBenchmark.p',axiom_5) ).
cnf(c_164,plain,
fwork_DOTfifo_DOTrtl_DOTlevel_(A) = fwork_DOTfifo_DOTrtl_DOTint__level_(A),
inference(clausify,[status(thm)],[axiom_5]) ).
cnf(c_11748,plain,
( n1 != f_ADD_(A,n1)
| n0 = A ),
inference(paramod,[status(thm)],[c_86,c_87]) ).
cnf(c_487,plain,
( f_ADD_(A,n1) != n1
| n0 = A ),
inference(copy,[status(thm)],[c_11748]) ).
cnf(c_11749,plain,
( A != f_ADD_(B,n1)
| y_105(A) = B
| n0 = A ),
inference(paramod,[status(thm)],[c_90,c_87]) ).
cnf(c_506,plain,
( f_ADD_(B,n1) != A
| y_105(A) = B
| n0 = A ),
inference(copy,[status(thm)],[c_11749]) ).
cnf(c_519,plain,
( p_LES_EQU_(B,A)
| p_LES_EQU_(A,B) ),
inference(resolve,[status(thm)],[c_94,c_88]) ).
cnf(c_536,plain,
( p__pred_(f__lt_(B,A))
| p_LES_EQU_(f_ADD_(A,n1),f_ADD_(B,n1)) ),
inference(resolve,[status(thm)],[c_98,c_21]) ).
cnf(c_543,plain,
( p_LES_EQU_(A,n0)
| ~ p_LES_EQU_(f_ADD_(A,n1),n1) ),
inference(paramod,[status(thm)],[c_86,c_99]) ).
cnf(c_554,plain,
~ p_LES_EQU_(n1,n0),
inference(paramod,[status(thm)],[c_86,c_101]) ).
cnf(c_555,plain,
f_ADD_(A,n1) != f__length_(f__empty_),
inference(paramod,[status(thm)],[c_81,c_102]) ).
cnf(c_11750,plain,
n1 != n0,
inference(paramod,[status(thm)],[c_86,c_102]) ).
cnf(c_557,plain,
n0 != n1,
inference(copy,[status(thm)],[c_11750]) ).
cnf(c_11751,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) ),
inference(resolve,[status(thm)],[c_151,c_12]) ).
cnf(c_11752,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) ),
inference(resolve,[status(thm)],[c_10,c_11751]) ).
cnf(c_808,plain,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) ),
inference(resolve,[status(thm)],[c_11,c_11752]) ).
cnf(c_849,plain,
fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) != fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(paramod,[status(thm)],[c_164,c_9]) ).
cnf(c_850,plain,
fwork_DOTfifo_DOTrtl_DOTfifo__length_ = f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),
inference(paramod,[status(thm)],[c_164,c_14]) ).
cnf(c_1041,plain,
( p_LES_EQU_(B,C)
| p_LES_EQU_(C,A)
| p_LES_EQU_(A,B) ),
inference(resolve,[status(thm)],[c_519,c_94]) ).
cnf(c_11753,plain,
( A != f__length_(f__empty_)
| n0 = A ),
inference(paramod,[status(thm)],[c_90,c_555]) ).
cnf(c_1478,plain,
( f__length_(f__empty_) != A
| n0 = A ),
inference(copy,[status(thm)],[c_11753]) ).
cnf(c_1521,plain,
( ~ p__pred_(f__gt_(B,C))
| p_LES_EQU_(C,A)
| p_LES_EQU_(A,B) ),
inference(resolve,[status(thm)],[c_1041,c_18]) ).
cnf(c_1799,plain,
fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) != f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1),
inference(paramod,[status(thm)],[c_14,c_849]) ).
cnf(c_2102,plain,
fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) != f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),
inference(paramod,[status(thm)],[c_164,c_1799]) ).
cnf(c_2103,plain,
p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)),
inference(resolve,[status(thm)],[c_2102,c_808]) ).
cnf(c_11754,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| p__pred_(fwork_DOTfifo_DOTrtl_DOTrd_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
inference(resolve,[status(thm)],[c_2103,c_144]) ).
cnf(c_11755,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| ~ p__pred_(fwork_DOTfifo_DOTrtl_DOTwr_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
inference(resolve,[status(thm)],[c_10,c_11754]) ).
cnf(c_11756,plain,
( p__pred_(fwork_DOTfifo_DOTrtl_DOTreset_(t_206))
| fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
inference(resolve,[status(thm)],[c_12,c_11755]) ).
cnf(c_2105,plain,
fwork_DOTfifo_DOTrtl_DOTint__level_(f_ADD_(t_206,n1)) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),
inference(resolve,[status(thm)],[c_11,c_11756]) ).
cnf(c_2110,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(resolve,[status(thm)],[c_2103,c_95]) ).
cnf(c_11757,plain,
( n0 = n1
| n0 = y_105(n1) ),
inference(resolve,[status(thm)],[c_487,c_90]) ).
cnf(c_11758,plain,
( n0 = n1
| y_105(n1) = n0 ),
inference(copy,[status(thm)],[c_11757]) ).
cnf(c_2171,plain,
y_105(n1) = n0,
inference(resolve,[status(thm)],[c_557,c_11758]) ).
cnf(c_2180,plain,
y_105(n1) = f__length_(f__empty_),
inference(paramod,[status(thm)],[c_81,c_2171]) ).
cnf(c_11759,plain,
( A != f__length_(f__empty_)
| n0 = A ),
inference(copy,[status(thm)],[c_1478]) ).
cnf(c_2182,plain,
n0 = y_105(n1),
inference(resolve,[status(thm)],[c_2180,c_11759]) ).
cnf(c_2186,plain,
f_ADD_(y_105(n1),A) = A,
inference(paramod,[status(thm)],[c_2182,c_86]) ).
cnf(c_2188,plain,
~ p_LES_EQU_(f_ADD_(A,n1),y_105(n1)),
inference(paramod,[status(thm)],[c_2182,c_101]) ).
cnf(c_2239,plain,
( p_LES_EQU_(y_105(A),n0)
| ~ p_LES_EQU_(A,n1)
| n0 = A ),
inference(paramod,[status(thm)],[c_90,c_543]) ).
cnf(c_3969,plain,
( p__pred_(f__gt_(A,n1))
| p_LES_EQU_(y_105(A),n0)
| n0 = A ),
inference(resolve,[status(thm)],[c_2239,c_17]) ).
cnf(c_4400,plain,
( p__pred_(f__lt_(n0,A))
| p_LES_EQU_(f_ADD_(A,n1),n1) ),
inference(paramod,[status(thm)],[c_86,c_536]) ).
cnf(c_11760,plain,
( f_SUB_(A,B) = C
| A != f_ADD_(C,B)
| p_LES_EQU_(A,B) ),
inference(copy,[status(thm)],[c_6]) ).
cnf(c_4662,plain,
( f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) ),
inference(resolve,[status(thm)],[c_850,c_11760]) ).
cnf(c_4670,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1))
| fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(paramod,[status(thm)],[c_850,c_2110]) ).
cnf(c_4697,plain,
( ~ p__pred_(f__gt_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) ),
inference(resolve,[status(thm)],[c_4662,c_18]) ).
cnf(c_8285,plain,
( p_LES_EQU_(A,y_105(n1))
| ~ p_LES_EQU_(f_ADD_(A,n1),n1) ),
inference(paramod,[status(thm)],[c_2186,c_99]) ).
cnf(c_8319,plain,
( p__pred_(f__lt_(n0,A))
| p_LES_EQU_(A,y_105(n1)) ),
inference(resolve,[status(thm)],[c_8285,c_4400]) ).
cnf(c_8342,plain,
( p_LES_EQU_(A,B)
| p_LES_EQU_(B,y_105(n1))
| p__pred_(f__lt_(n0,A)) ),
inference(resolve,[status(thm)],[c_8319,c_94]) ).
cnf(c_11761,plain,
f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1) = fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(copy,[status(thm)],[c_850]) ).
cnf(c_11762,plain,
( y_105(fwork_DOTfifo_DOTrtl_DOTfifo__length_) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| n0 = fwork_DOTfifo_DOTrtl_DOTfifo__length_ ),
inference(resolve,[status(thm)],[c_506,c_11761]) ).
cnf(c_10789,plain,
( y_105(fwork_DOTfifo_DOTrtl_DOTfifo__length_) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(copy,[status(thm)],[c_11762]) ).
cnf(c_11763,plain,
( p__pred_(f__gt_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n0)
| n0 = fwork_DOTfifo_DOTrtl_DOTfifo__length_
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(paramod,[status(thm)],[c_10789,c_3969]) ).
cnf(c_11764,plain,
( p__pred_(f__gt_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n0)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(copy,[status(thm)],[c_11763]) ).
cnf(c_10796,plain,
( p__pred_(f__gt_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n0)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(copy,[status(thm)],[c_11764]) ).
cnf(c_10820,plain,
( ~ p__pred_(f__lt_(n0,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)))
| p__pred_(f__gt_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(resolve,[status(thm)],[c_10796,c_22]) ).
cnf(c_11153,plain,
fwork_DOTfifo_DOTrtl_DOTint__level_(t_206) != fwork_DOTfifo_DOTrtl_DOTfifo__length_,
inference(paramod,[status(thm)],[c_2105,c_849]) ).
cnf(c_11206,plain,
~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1)),
inference(resolve,[status(thm)],[c_11153,c_4670]) ).
cnf(c_11765,plain,
( p_LES_EQU_(f_ADD_(fwork_DOTfifo_DOTrtl_DOTint__level_(t_206),n1),y_105(n1))
| p__pred_(f__lt_(n0,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))) ),
inference(resolve,[status(thm)],[c_11206,c_8342]) ).
cnf(c_11246,plain,
p__pred_(f__lt_(n0,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))),
inference(resolve,[status(thm)],[c_2188,c_11765]) ).
cnf(c_11259,plain,
( p__pred_(f__gt_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1))
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(resolve,[status(thm)],[c_11246,c_10820]) ).
cnf(c_11301,plain,
( f_SUB_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n1) = fwork_DOTfifo_DOTrtl_DOTint__level_(t_206)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(resolve,[status(thm)],[c_11259,c_4697]) ).
cnf(c_11317,plain,
( p_LES_EQU_(n1,A)
| p_LES_EQU_(A,fwork_DOTfifo_DOTrtl_DOTfifo__length_)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(resolve,[status(thm)],[c_11259,c_1521]) ).
cnf(c_11352,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,A)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = A
| p_LES_EQU_(n1,A)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(resolve,[status(thm)],[c_11317,c_95]) ).
cnf(c_11766,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)
| p_LES_EQU_(n1,n0)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(factor,[status(thm)],[c_11352]) ).
cnf(c_11365,plain,
( ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(resolve,[status(thm)],[c_554,c_11766]) ).
cnf(c_11767,plain,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)
| ~ p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,fwork_DOTfifo_DOTrtl_DOTint__level_(t_206))
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(paramod,[status(thm)],[c_11301,c_100]) ).
cnf(c_11733,plain,
( p_LES_EQU_(fwork_DOTfifo_DOTrtl_DOTfifo__length_,n0)
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(resolve,[status(thm)],[c_2103,c_11767]) ).
cnf(c_11768,plain,
( fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0
| fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0 ),
inference(resolve,[status(thm)],[c_11733,c_11365]) ).
cnf(c_11736,plain,
fwork_DOTfifo_DOTrtl_DOTfifo__length_ = n0,
inference(copy,[status(thm)],[c_11768]) ).
cnf(c_11769,plain,
n0 = f_ADD_(fwork_DOTfifo_DOTrtl_DOTlevel_(t_206),n1),
inference(paramod,[status(thm)],[c_11736,c_14]) ).
cnf(c_11746,plain,
$false,
inference(resolve,[status(thm)],[c_102,c_11769]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV022-2 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.07/15.42 % CPULimit : 300
% 0.07/15.42 % WCLimit : 300
% 0.07/15.42 % DateTime : Fri Sep 25 16:03:00 UTC 2026
% 0.07/15.43 % CPUTime :
% 0.07/15.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/15.43 % Process 1428099 was started by sandbox on n008,
% 0.07/15.43 % Fri Sep 25 16:03:00 2026
% 0.07/15.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/15.43
% 0.07/15.43 % From the command line: assign(max_seconds, 300).
% 142.63/34.40
% 142.63/34.40 % given #500 (T,wt=21): 536 p_LES_EQU_(f_ADD_(A,n1),f_ADD_(B,n1)) | p__pred_(f__lt_(B,A)). [resolve(98,b,21,a)].
% 142.63/34.40
% 142.63/34.40 % given #1000 (T,wt=21): 4562 p__pred_(f__gt_(A,n0)) | f_ADD_(n0,n1) = f_ADD_(A,n1). [resolve(4550,a,517,b),unit_del(c,101)].
% 142.63/34.40
% 142.63/34.40 % SZS status Unsatisfiable for theBenchmark
% 142.63/34.40
% 142.63/34.40 % Proof 1 at 2.27 (+ 0.61) seconds.
% 142.63/34.40 % Length of proof is 77.
% 142.63/34.40 % Level of proof is 15.
% 142.63/34.40 % Maximum clause weight is 37.000.
% 142.63/34.40 % Given clauses 1388.
% 142.63/34.40
% 142.63/34.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------