%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV017-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /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 : Thu Sep 24 12:45:58 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.55s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 88
% Syntax : Number of formulae : 296 ( 41 unt; 51 def)
% Number of atoms : 744 ( 148 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 701 ( 253 ~; 397 |; 0 &)
% ( 51 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 61 ( 59 usr; 52 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 150 ( 150 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X_0] : plus(X_0,n1) != n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X_1] : gt(plus(X_1,n1),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X_2] :
( gt(X_2,minus(X_2,n1))
| ~ gt(X_2,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [Y_12,X_11] :
( ~ gt(plus(Y_12,n1),plus(X_11,n1))
| gt(Y_12,X_11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [Y_18,X_17] :
( gt(X_17,Y_18)
| X_17 = Y_18
| gt(Y_18,X_17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Z_21,Y_20,X_19] :
( ~ gt(Y_20,X_19)
| gt(Z_21,X_19)
| ~ gt(Z_21,Y_20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [Y_24,X_23] :
( gt(Y_24,plus(X_23,n1))
| plus(X_23,n1) = Y_24
| ~ gt(Y_24,X_23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X_25] :
( gt(X_25,n0)
| X_25 = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [X_26] :
( X_26 = plus(y_27(X_26),n1)
| X_26 = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [X_28] : ~ gt(X_28,X_28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [X_31] : plus(n0,X_31) = X_31,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X_t_32] : level(X_t_32) = int_level(X_t_32),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X_t_33] :
( p_Full(X_t_33)
| int_level(X_t_33) != fifo_length ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X_t_34] :
( ~ p_Full(X_t_34)
| int_level(X_t_34) = fifo_length ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [X_t_35] :
( p_Empty(X_t_35)
| int_level(X_t_35) != n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X_t_36] :
( ~ p_Empty(X_t_36)
| int_level(X_t_36) = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [X_t_37] :
( int_level(plus(X_t_37,n1)) = n0
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [X_t_37,X_k1_38,X_k2_39] :
( ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1)
| ~ gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [X_t_42,X_k1_57,X_k2_58] :
( p_Mem(X_k1_57,X_k2_58,X_t_42)
| ~ p_Mem(X_k1_57,X_k2_58,plus(X_t_42,n1))
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = plus(int_level(X_t_42),n1)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [X_t_42,X_k1_87] :
( p_Data_in(X_k1_87,X_t_42)
| ~ p_Mem(wr_level(X_t_42),X_k1_87,plus(X_t_42,n1))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [X_t_42,X_k1_87] :
( ~ p_Data_in(X_k1_87,X_t_42)
| p_Mem(wr_level(X_t_42),X_k1_87,plus(X_t_42,n1))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [X_t_42] :
( wr_level(plus(X_t_42,n1)) = wr_level(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = minus(int_level(X_t_42),n1)
| ~ gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,axiom,
! [X_t_42,X_k1_128,X_k2_129] :
( p_Mem(X_k1_128,X_k2_129,X_t_42)
| ~ p_Mem(X_k1_128,X_k2_129,plus(X_t_42,n1))
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
! [X_t_42,X_k1_128,X_k2_129] :
( ~ p_Mem(X_k1_128,X_k2_129,X_t_42)
| p_Mem(X_k1_128,X_k2_129,plus(X_t_42,n1))
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,negated_conjecture,
~ gt(level(t_139),fifo_length),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,negated_conjecture,
p_Rd(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,negated_conjecture,
~ p_Wr(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,negated_conjecture,
~ p_Reset(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,negated_conjecture,
p_Full(plus(t_139,n1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,negated_conjecture,
gt(fifo_length,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,plain,
! [X0] : plus(X0,n1) != n0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f98,plain,
! [X0] : gt(plus(X0,n1),n0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f99,plain,
! [X0] :
( gt(X0,minus(X0,n1))
| ~ gt(X0,n0) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f107,plain,
! [X0,X1] :
( ~ gt(plus(X0,n1),plus(X1,n1))
| gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f110,plain,
! [X0,X1] :
( gt(X1,X0)
| X1 = X0
| gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f111,plain,
! [Y_20,X_19] :
( ~ gt(Y_20,X_19)
| ! [Z_21] :
( gt(Z_21,X_19)
| ~ gt(Z_21,Y_20) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ gt(X1,X2)
| gt(X0,X2)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [X0,X1] :
( gt(X0,plus(X1,n1))
| plus(X1,n1) = X0
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f114,plain,
! [X0] :
( gt(X0,n0)
| X0 = n0 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f115,plain,
! [X0] :
( X0 = plus(y_27(X0),n1)
| X0 = n0 ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f116,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f118,plain,
! [X0] : plus(n0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f120,plain,
! [X0] : level(X0) = int_level(X0),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f121,plain,
! [X0] :
( p_Full(X0)
| int_level(X0) != fifo_length ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f122,plain,
! [X0] :
( ~ p_Full(X0)
| int_level(X0) = fifo_length ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f123,plain,
! [X0] :
( p_Empty(X0)
| int_level(X0) != n0 ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f124,plain,
! [X0] :
( ~ p_Empty(X0)
| int_level(X0) = n0 ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f125,plain,
! [X0] :
( int_level(plus(X0,n1)) = n0
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f130,plain,
! [X_t_37] :
( ! [X_k1_38,X_k2_39] : ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f131,plain,
! [X0,X1,X2] :
( ~ p_Mem(X1,X2,plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f136,plain,
! [X0] :
( int_level(plus(X0,n1)) = plus(int_level(X0),n1)
| ~ gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f145,plain,
! [X0] :
( int_level(plus(X0,n1)) = int_level(X0)
| gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f146,plain,
! [X0,X1,X2] :
( p_Mem(X1,X2,X0)
| ~ p_Mem(X1,X2,plus(X0,n1))
| gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f154,plain,
! [X0] :
( int_level(plus(X0,n1)) = int_level(X0)
| ~ gt(int_level(X0),n0)
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f160,plain,
! [X0] :
( int_level(plus(X0,n1)) = plus(int_level(X0),n1)
| gt(int_level(X0),n0)
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f164,plain,
! [X0,X1] :
( p_Data_in(X1,X0)
| ~ p_Mem(wr_level(X0),X1,plus(X0,n1))
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f165,plain,
! [X0,X1] :
( ~ p_Data_in(X1,X0)
| p_Mem(wr_level(X0),X1,plus(X0,n1))
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f170,plain,
! [X0] :
( wr_level(plus(X0,n1)) = wr_level(X0)
| p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f172,plain,
! [X0] :
( int_level(plus(X0,n1)) = minus(int_level(X0),n1)
| ~ gt(int_level(X0),n0)
| ~ p_Rd(X0)
| p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f179,plain,
! [X0] :
( int_level(plus(X0,n1)) = int_level(X0)
| gt(int_level(X0),n0)
| ~ p_Rd(X0)
| p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f183,plain,
! [X0] :
( int_level(plus(X0,n1)) = int_level(X0)
| p_Rd(X0)
| p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f188,plain,
! [X0,X1,X2] :
( p_Mem(X1,X2,X0)
| ~ p_Mem(X1,X2,plus(X0,n1))
| p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f189,plain,
! [X0,X1,X2] :
( ~ p_Mem(X1,X2,X0)
| p_Mem(X1,X2,plus(X0,n1))
| p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f192,plain,
~ gt(level(t_139),fifo_length),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f193,plain,
p_Rd(t_139),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f194,plain,
~ p_Wr(t_139),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f195,plain,
~ p_Reset(t_139),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f196,plain,
p_Full(plus(t_139,n1)),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f197,plain,
gt(fifo_length,n0),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f206,plain,
! [X0,X1,X2] :
( p_Mem(X1,X2,X0)
| ~ p_Mem(X1,X2,plus(X0,n1))
| gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f146,f131]) ).
fof(f219,plain,
! [X0,X1] :
( p_Data_in(X1,X0)
| ~ p_Mem(wr_level(X0),X1,plus(X0,n1))
| ~ p_Rd(X0)
| ~ p_Wr(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f164,f131]) ).
fof(f241,plain,
! [X0] :
( int_level(plus(X0,n1)) = int_level(X0)
| gt(fifo_length,int_level(X0))
| p_Rd(X0)
| p_Reset(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f145,f183]) ).
fof(f242,plain,
! [X0] :
( int_level(plus(X0,n1)) = int_level(X0)
| gt(int_level(X0),n0)
| p_Wr(X0)
| p_Reset(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f179,f183]) ).
fof(f252,plain,
! [X0,X1,X2] :
( p_Mem(X1,X2,X0)
| ~ p_Mem(X1,X2,plus(X0,n1))
| gt(fifo_length,int_level(X0))
| p_Rd(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f206,f253]) ).
fof(f253,plain,
! [X0,X1,X2] :
( p_Mem(X1,X2,X0)
| ~ p_Mem(X1,X2,plus(X0,n1))
| p_Wr(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f188,f131]) ).
fof(f257,plain,
~ gt(int_level(t_139),fifo_length),
inference(forward_demodulation,[status(thm)],[f120,f192]) ).
fof(f265,plain,
! [X0] :
( ~ gt(plus(X0,n1),n1)
| gt(X0,n0) ),
inference(paramodulation,[status(thm)],[f118,f107]) ).
fof(f266,plain,
! [X0] :
( ~ gt(n1,plus(X0,n1))
| gt(n0,X0) ),
inference(paramodulation,[status(thm)],[f118,f107]) ).
fof(f269,plain,
gt(n1,n0),
inference(paramodulation,[status(thm)],[f118,f98]) ).
fof(f284,plain,
( int_level(t_139) = fifo_length
| gt(fifo_length,int_level(t_139)) ),
inference(resolution,[status(thm)],[f110,f257]) ).
fof(f287,definition,
( sQ0_spl
<=> gt(fifo_length,int_level(t_139)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f290,definition,
( sQ1_spl
<=> int_level(t_139) = fifo_length ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f291,plain,
( ~ sQ1_spl
| int_level(t_139) = fifo_length ),
inference(component_clause,[status(thm)],[f290]) ).
fof(f292,plain,
( sQ1_spl
| int_level(t_139) != fifo_length ),
inference(component_clause,[status(thm)],[f290]) ).
fof(f293,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f284,f287,f290]) ).
fof(f299,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[f112,f116]) ).
fof(f304,plain,
gt(fifo_length,minus(fifo_length,n1)),
inference(resolution,[status(thm)],[f197,f99]) ).
fof(f322,plain,
! [X0] :
( ~ gt(n0,X0)
| X0 = n0 ),
inference(resolution,[status(thm)],[f114,f299]) ).
fof(f331,definition,
( sQ2_spl
<=> gt(fifo_length,n0) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f333,plain,
( sQ2_spl
| ~ gt(fifo_length,n0) ),
inference(component_clause,[status(thm)],[f331]) ).
fof(f334,definition,
( sQ3_spl
<=> n0 = fifo_length ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f336,plain,
( sQ3_spl
| n0 != fifo_length ),
inference(component_clause,[status(thm)],[f334]) ).
fof(f338,plain,
( n0 = n0
| n0 = n0 ),
inference(resolution,[status(thm)],[f322,f114]) ).
fof(f339,plain,
! [X0] :
( plus(X0,n1) = n0
| ~ gt(n0,X0)
| plus(X0,n1) = n0 ),
inference(resolution,[status(thm)],[f322,f113]) ).
fof(f342,definition,
( sQ4_spl
<=> n0 = n0 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f345,plain,
sQ4_spl,
inference(split_clause,[status(thm)],[f338,f342]) ).
fof(f346,plain,
! [X0] :
( ~ gt(n0,X0)
| plus(X0,n1) = n0 ),
inference(duplicate_literals_removal,[status(thm)],[f339]) ).
fof(f347,plain,
! [X0] : ~ gt(n1,plus(X0,n1)),
inference(backward_subsumption_resolution,[status(thm)],[f266,f348]) ).
fof(f348,plain,
! [X0] : ~ gt(n0,X0),
inference(forward_subsumption_resolution,[status(thm)],[f346,f97]) ).
fof(f358,plain,
! [X0] :
( X0 = plus(y_27(X0),n1)
| gt(fifo_length,X0) ),
inference(paramodulation,[status(thm)],[f115,f197]) ).
fof(f368,plain,
int_level(plus(t_139,n1)) = fifo_length,
inference(resolution,[status(thm)],[f122,f196]) ).
fof(f370,plain,
! [X0] :
( int_level(X0) = plus(y_27(int_level(X0)),n1)
| p_Empty(X0)
| n0 != n0 ),
inference(paramodulation,[status(thm)],[f115,f123]) ).
fof(f371,definition,
! [X0] :
( sQ6_spl
<=> ( int_level(X0) = plus(y_27(int_level(X0)),n1)
| p_Empty(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f374,plain,
( sQ6_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f370,f342,f371]) ).
fof(f381,definition,
( sQ8_spl
<=> fifo_length = plus(y_27(fifo_length),n1) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f394,definition,
( sQ10_spl
<=> int_level(t_139) = n0 ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f395,plain,
( ~ sQ10_spl
| int_level(t_139) = n0 ),
inference(component_clause,[status(thm)],[f394]) ).
fof(f401,definition,
( sQ12_spl
<=> int_level(t_139) = plus(y_27(int_level(t_139)),n1) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f408,definition,
( sQ14_spl
<=> t_139 = plus(y_27(t_139),n1) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f414,plain,
( fifo_length = plus(y_27(fifo_length),n1)
| gt(n0,minus(fifo_length,n1)) ),
inference(paramodulation,[status(thm)],[f115,f304]) ).
fof(f417,definition,
( sQ15_spl
<=> gt(n0,minus(fifo_length,n1)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f418,plain,
( ~ sQ15_spl
| gt(n0,minus(fifo_length,n1)) ),
inference(component_clause,[status(thm)],[f417]) ).
fof(f420,plain,
( sQ8_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f414,f417,f381]) ).
fof(f441,plain,
! [X0] :
( plus(X0,n1) = plus(y_27(plus(X0,n1)),n1)
| ~ gt(n1,n0) ),
inference(paramodulation,[status(thm)],[f115,f347]) ).
fof(f443,definition,
( sQ19_spl
<=> gt(n1,n0) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f445,plain,
( sQ19_spl
| ~ gt(n1,n0) ),
inference(component_clause,[status(thm)],[f443]) ).
fof(f446,definition,
! [X0] :
( sQ20_spl
<=> plus(X0,n1) = plus(y_27(plus(X0,n1)),n1) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f441,f443,f446]) ).
fof(f450,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f445,f269]) ).
fof(f451,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f450]) ).
fof(f456,plain,
! [X0] :
( int_level(X0) = plus(y_27(int_level(X0)),n1)
| int_level(plus(X0,n1)) = plus(int_level(X0),n1)
| ~ gt(fifo_length,n0)
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(paramodulation,[status(thm)],[f115,f136]) ).
fof(f457,definition,
( sQ21_spl
<=> p_Reset(t_139) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f458,plain,
( ~ sQ21_spl
| p_Reset(t_139) ),
inference(component_clause,[status(thm)],[f457]) ).
fof(f460,definition,
( sQ22_spl
<=> p_Wr(t_139) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( ~ sQ22_spl
| p_Wr(t_139) ),
inference(component_clause,[status(thm)],[f460]) ).
fof(f463,definition,
( sQ23_spl
<=> p_Rd(t_139) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f465,plain,
( sQ23_spl
| ~ p_Rd(t_139) ),
inference(component_clause,[status(thm)],[f463]) ).
fof(f474,definition,
! [X0] :
( sQ26_spl
<=> ( int_level(X0) = plus(y_27(int_level(X0)),n1)
| int_level(plus(X0,n1)) = plus(int_level(X0),n1)
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( ~ sQ2_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f456,f474,f331]) ).
fof(f493,definition,
( sQ28_spl
<=> gt(n0,n0) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( ~ sQ28_spl
| gt(n0,n0) ),
inference(component_clause,[status(thm)],[f493]) ).
fof(f501,plain,
! [X0] :
( int_level(X0) = plus(y_27(int_level(X0)),n1)
| int_level(plus(X0,n1)) = plus(int_level(X0),n1)
| gt(n0,n0)
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(paramodulation,[status(thm)],[f115,f160]) ).
fof(f504,definition,
! [X0] :
( sQ29_spl
<=> ( int_level(X0) = plus(y_27(int_level(X0)),n1)
| int_level(plus(X0,n1)) = plus(int_level(X0),n1)
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( sQ28_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f501,f504,f493]) ).
fof(f510,definition,
( sQ30_spl
<=> int_level(plus(t_139,n1)) = int_level(t_139) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f511,plain,
( ~ sQ30_spl
| int_level(plus(t_139,n1)) = int_level(t_139) ),
inference(component_clause,[status(thm)],[f510]) ).
fof(f515,plain,
( ~ sQ1_spl
| int_level(t_139) = plus(y_27(int_level(t_139)),n1)
| n0 = fifo_length ),
inference(paramodulation,[status(thm)],[f115,f291]) ).
fof(f516,plain,
( ~ sQ1_spl
| t_139 = plus(y_27(t_139),n1)
| int_level(n0) = fifo_length ),
inference(paramodulation,[status(thm)],[f115,f291]) ).
fof(f522,plain,
( ~ sQ1_spl
| sQ12_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f515,f334,f401,f290]) ).
fof(f523,definition,
( sQ31_spl
<=> int_level(n0) = fifo_length ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f524,plain,
( ~ sQ31_spl
| int_level(n0) = fifo_length ),
inference(component_clause,[status(thm)],[f523]) ).
fof(f525,plain,
( sQ31_spl
| int_level(n0) != fifo_length ),
inference(component_clause,[status(thm)],[f523]) ).
fof(f526,plain,
( ~ sQ1_spl
| sQ14_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f516,f523,f408,f290]) ).
fof(f529,definition,
( sQ32_spl
<=> gt(fifo_length,fifo_length) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f537,definition,
( sQ34_spl
<=> fifo_length = fifo_length ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f539,plain,
( sQ34_spl
| fifo_length != fifo_length ),
inference(component_clause,[status(thm)],[f537]) ).
fof(f544,plain,
( ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f458,f195]) ).
fof(f545,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f544]) ).
fof(f548,plain,
( sQ34_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f539]) ).
fof(f549,plain,
sQ34_spl,
inference(contradiction_clause,[status(thm)],[f548]) ).
fof(f550,plain,
( ~ sQ30_spl
| fifo_length = int_level(t_139) ),
inference(forward_demodulation,[status(thm)],[f368,f511]) ).
fof(f558,plain,
( sQ1_spl
| ~ sQ30_spl
| fifo_length != fifo_length ),
inference(forward_demodulation,[status(thm)],[f550,f292]) ).
fof(f559,plain,
( sQ1_spl
| ~ sQ30_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f558]) ).
fof(f560,plain,
( sQ1_spl
| ~ sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f559]) ).
fof(f569,definition,
( sQ36_spl
<=> gt(n0,int_level(t_139)) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f570,plain,
( ~ sQ36_spl
| gt(n0,int_level(t_139)) ),
inference(component_clause,[status(thm)],[f569]) ).
fof(f578,plain,
( sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f333,f197]) ).
fof(f579,plain,
sQ2_spl,
inference(contradiction_clause,[status(thm)],[f578]) ).
fof(f591,definition,
( sQ39_spl
<=> gt(int_level(t_139),n0) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f592,plain,
( ~ sQ39_spl
| gt(int_level(t_139),n0) ),
inference(component_clause,[status(thm)],[f591]) ).
fof(f593,plain,
( sQ39_spl
| ~ gt(int_level(t_139),n0) ),
inference(component_clause,[status(thm)],[f591]) ).
fof(f622,plain,
( int_level(plus(t_139,n1)) = plus(y_27(int_level(plus(t_139,n1))),n1)
| n0 = fifo_length ),
inference(paramodulation,[status(thm)],[f115,f368]) ).
fof(f623,plain,
( plus(t_139,n1) = plus(y_27(plus(t_139,n1)),n1)
| int_level(n0) = fifo_length ),
inference(paramodulation,[status(thm)],[f115,f368]) ).
fof(f626,plain,
( int_level(plus(plus(t_139,n1),n1)) = int_level(plus(t_139,n1))
| ~ gt(fifo_length,n0)
| ~ p_Rd(plus(t_139,n1))
| ~ p_Wr(plus(t_139,n1))
| p_Reset(plus(t_139,n1)) ),
inference(paramodulation,[status(thm)],[f368,f154]) ).
fof(f627,plain,
( int_level(plus(plus(t_139,n1),n1)) = plus(int_level(plus(t_139,n1)),n1)
| ~ gt(fifo_length,fifo_length)
| p_Rd(plus(t_139,n1))
| ~ p_Wr(plus(t_139,n1))
| p_Reset(plus(t_139,n1)) ),
inference(paramodulation,[status(thm)],[f368,f136]) ).
fof(f628,plain,
( p_Empty(plus(t_139,n1))
| fifo_length != n0 ),
inference(paramodulation,[status(thm)],[f368,f123]) ).
fof(f629,plain,
( p_Full(plus(t_139,n1))
| fifo_length != fifo_length ),
inference(paramodulation,[status(thm)],[f368,f121]) ).
fof(f630,definition,
( sQ46_spl
<=> int_level(plus(t_139,n1)) = plus(y_27(int_level(plus(t_139,n1))),n1) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f633,plain,
( sQ46_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f622,f334,f630]) ).
fof(f634,definition,
( sQ47_spl
<=> plus(t_139,n1) = plus(y_27(plus(t_139,n1)),n1) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( sQ47_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f623,f523,f634]) ).
fof(f638,definition,
( sQ48_spl
<=> int_level(plus(n0,n1)) = fifo_length ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f639,plain,
( ~ sQ48_spl
| int_level(plus(n0,n1)) = fifo_length ),
inference(component_clause,[status(thm)],[f638]) ).
fof(f642,definition,
( sQ49_spl
<=> p_Reset(plus(t_139,n1)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f643,plain,
( ~ sQ49_spl
| p_Reset(plus(t_139,n1)) ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,definition,
( sQ50_spl
<=> p_Wr(plus(t_139,n1)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f647,plain,
( sQ50_spl
| ~ p_Wr(plus(t_139,n1)) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,definition,
( sQ51_spl
<=> p_Rd(plus(t_139,n1)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f649,plain,
( ~ sQ51_spl
| p_Rd(plus(t_139,n1)) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,definition,
( sQ52_spl
<=> int_level(plus(plus(t_139,n1),n1)) = plus(int_level(plus(t_139,n1)),n1) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f652,plain,
( ~ sQ52_spl
| int_level(plus(plus(t_139,n1),n1)) = plus(int_level(plus(t_139,n1)),n1) ),
inference(component_clause,[status(thm)],[f651]) ).
fof(f655,definition,
( sQ53_spl
<=> int_level(plus(plus(t_139,n1),n1)) = int_level(plus(t_139,n1)) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f656,plain,
( ~ sQ53_spl
| int_level(plus(plus(t_139,n1),n1)) = int_level(plus(t_139,n1)) ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f658,plain,
( sQ53_spl
| ~ sQ2_spl
| ~ sQ51_spl
| ~ sQ50_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f626,f642,f645,f648,f331,f655]) ).
fof(f659,plain,
( sQ52_spl
| ~ sQ32_spl
| sQ51_spl
| ~ sQ50_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f627,f642,f645,f648,f529,f651]) ).
fof(f660,definition,
( sQ54_spl
<=> p_Empty(plus(t_139,n1)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f661,plain,
( ~ sQ54_spl
| p_Empty(plus(t_139,n1)) ),
inference(component_clause,[status(thm)],[f660]) ).
fof(f663,plain,
( sQ54_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f628,f334,f660]) ).
fof(f664,definition,
( sQ55_spl
<=> p_Full(plus(t_139,n1)) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f667,plain,
( sQ55_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f629,f537,f664]) ).
fof(f672,plain,
( gt(fifo_length,minus(fifo_length,n1))
| n0 = plus(y_27(n0),n1) ),
inference(resolution,[status(thm)],[f358,f99]) ).
fof(f678,definition,
( sQ56_spl
<=> n0 = plus(y_27(n0),n1) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( ~ sQ56_spl
| n0 = plus(y_27(n0),n1) ),
inference(component_clause,[status(thm)],[f678]) ).
fof(f681,definition,
( sQ57_spl
<=> gt(fifo_length,minus(fifo_length,n1)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f684,plain,
( sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f672,f678,f681]) ).
fof(f685,definition,
! [X0] :
( sQ58_spl
<=> ( X0 = plus(y_27(X0),n1)
| gt(n0,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f686,plain,
! [X0] :
( ~ sQ58_spl
| X0 = plus(y_27(X0),n1)
| gt(n0,X0) ),
inference(component_clause,[status(thm)],[f685]) ).
fof(f689,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f679,f97]) ).
fof(f690,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f689]) ).
fof(f692,plain,
( sQ1_spl
| t_139 = plus(y_27(t_139),n1)
| int_level(n0) != fifo_length ),
inference(paramodulation,[status(thm)],[f115,f292]) ).
fof(f694,plain,
( sQ1_spl
| sQ14_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f692,f523,f408,f290]) ).
fof(f697,plain,
( ~ sQ31_spl
| int_level(n0) = plus(y_27(int_level(n0)),n1)
| n0 = fifo_length ),
inference(paramodulation,[status(thm)],[f115,f524]) ).
fof(f703,plain,
( ~ sQ31_spl
| p_Full(n0)
| fifo_length != fifo_length ),
inference(paramodulation,[status(thm)],[f524,f121]) ).
fof(f704,definition,
( sQ59_spl
<=> int_level(n0) = plus(y_27(int_level(n0)),n1) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f707,plain,
( ~ sQ31_spl
| sQ59_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f697,f334,f704,f523]) ).
fof(f718,definition,
( sQ63_spl
<=> int_level(plus(n0,n1)) = int_level(n0) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f719,plain,
( ~ sQ63_spl
| int_level(plus(n0,n1)) = int_level(n0) ),
inference(component_clause,[status(thm)],[f718]) ).
fof(f727,definition,
( sQ65_spl
<=> p_Full(n0) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f728,plain,
( ~ sQ65_spl
| p_Full(n0) ),
inference(component_clause,[status(thm)],[f727]) ).
fof(f730,plain,
( ~ sQ31_spl
| sQ65_spl
| ~ sQ34_spl ),
inference(split_clause,[status(thm)],[f703,f537,f727,f523]) ).
fof(f736,plain,
( int_level(plus(plus(t_139,n1),n1)) = int_level(plus(t_139,n1))
| gt(fifo_length,fifo_length)
| p_Rd(plus(t_139,n1))
| p_Reset(plus(t_139,n1)) ),
inference(paramodulation,[status(thm)],[f368,f241]) ).
fof(f747,plain,
( sQ53_spl
| sQ32_spl
| sQ51_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f736,f642,f648,f529,f655]) ).
fof(f752,plain,
! [X0] :
( int_level(X0) = plus(y_27(int_level(X0)),n1)
| int_level(plus(X0,n1)) = int_level(X0)
| gt(n0,n0)
| p_Wr(X0)
| p_Reset(X0) ),
inference(paramodulation,[status(thm)],[f115,f242]) ).
fof(f755,definition,
! [X0] :
( sQ68_spl
<=> ( int_level(X0) = plus(y_27(int_level(X0)),n1)
| int_level(plus(X0,n1)) = int_level(X0)
| p_Wr(X0)
| p_Reset(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ28_spl
| sQ68_spl ),
inference(split_clause,[status(thm)],[f752,f755,f493]) ).
fof(f768,plain,
! [X0,X1] :
( p_Mem(X0,X1,plus(t_139,n1))
| ~ p_Mem(X0,X1,plus(plus(t_139,n1),n1))
| gt(fifo_length,fifo_length)
| p_Rd(plus(t_139,n1)) ),
inference(paramodulation,[status(thm)],[f368,f252]) ).
fof(f779,definition,
! [X0,X1] :
( sQ71_spl
<=> ( p_Mem(X0,X1,plus(t_139,n1))
| ~ p_Mem(X0,X1,plus(plus(t_139,n1),n1)) ) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f782,plain,
( sQ71_spl
| sQ32_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f768,f648,f529,f779]) ).
fof(f783,plain,
( ~ sQ53_spl
| int_level(plus(plus(t_139,n1),n1)) = fifo_length ),
inference(forward_demodulation,[status(thm)],[f368,f656]) ).
fof(f791,plain,
( sQ31_spl
| ~ sQ63_spl
| int_level(n1) != fifo_length ),
inference(backward_demodulation,[status(thm)],[f792,f525]) ).
fof(f792,plain,
( ~ sQ63_spl
| int_level(n1) = int_level(n0) ),
inference(forward_demodulation,[status(thm)],[f118,f719]) ).
fof(f797,plain,
( ~ sQ49_spl
| int_level(plus(plus(t_139,n1),n1)) = n0 ),
inference(resolution,[status(thm)],[f643,f125]) ).
fof(f800,plain,
( ~ sQ49_spl
| ~ sQ53_spl
| fifo_length = n0 ),
inference(forward_demodulation,[status(thm)],[f783,f797]) ).
fof(f801,plain,
( ~ sQ49_spl
| ~ sQ53_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f800,f336]) ).
fof(f802,plain,
( ~ sQ49_spl
| ~ sQ53_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f801]) ).
fof(f838,plain,
! [X0] :
( ~ sQ58_spl
| X0 = plus(y_27(X0),n1) ),
inference(forward_subsumption_resolution,[status(thm)],[f686,f348]) ).
fof(f839,plain,
( ~ sQ48_spl
| int_level(n1) = fifo_length ),
inference(forward_demodulation,[status(thm)],[f118,f639]) ).
fof(f840,plain,
( ~ sQ48_spl
| sQ31_spl
| ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f839,f791]) ).
fof(f841,plain,
( ~ sQ48_spl
| sQ31_spl
| ~ sQ63_spl ),
inference(contradiction_clause,[status(thm)],[f840]) ).
fof(f842,plain,
( ~ sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f570,f348]) ).
fof(f843,plain,
~ sQ36_spl,
inference(contradiction_clause,[status(thm)],[f842]) ).
fof(f844,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f418,f348]) ).
fof(f845,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f844]) ).
fof(f855,plain,
( ~ sQ52_spl
| ~ sQ49_spl
| n0 = plus(int_level(plus(t_139,n1)),n1) ),
inference(forward_demodulation,[status(thm)],[f797,f652]) ).
fof(f856,plain,
( ~ sQ52_spl
| ~ sQ49_spl
| n0 = plus(fifo_length,n1) ),
inference(forward_demodulation,[status(thm)],[f368,f855]) ).
fof(f857,plain,
( ~ sQ52_spl
| ~ sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f856,f97]) ).
fof(f858,plain,
( ~ sQ52_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f857]) ).
fof(f932,plain,
( wr_level(plus(t_139,n1)) = wr_level(t_139)
| p_Reset(t_139) ),
inference(resolution,[status(thm)],[f170,f194]) ).
fof(f934,definition,
( sQ75_spl
<=> wr_level(plus(t_139,n1)) = wr_level(t_139) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f937,plain,
( sQ75_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f932,f457,f934]) ).
fof(f978,plain,
( ~ sQ65_spl
| int_level(n0) = fifo_length ),
inference(resolution,[status(thm)],[f122,f728]) ).
fof(f980,plain,
( ~ sQ65_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f978,f523,f727]) ).
fof(f1006,plain,
! [X0,X1] :
( ~ p_Mem(X0,X1,t_139)
| p_Mem(X0,X1,plus(t_139,n1))
| p_Reset(t_139) ),
inference(resolution,[status(thm)],[f189,f194]) ).
fof(f1008,definition,
! [X0,X1] :
( sQ77_spl
<=> ( ~ p_Mem(X0,X1,t_139)
| p_Mem(X0,X1,plus(t_139,n1)) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1011,plain,
( sQ77_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f1006,f457,f1008]) ).
fof(f1044,plain,
( ~ gt(n1,n1)
| gt(n0,n0) ),
inference(paramodulation,[status(thm)],[f118,f265]) ).
fof(f1046,definition,
( sQ81_spl
<=> gt(n1,n1) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f1049,plain,
( ~ sQ81_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1044,f493,f1046]) ).
fof(f1050,plain,
( ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f494,f348]) ).
fof(f1051,plain,
~ sQ28_spl,
inference(contradiction_clause,[status(thm)],[f1050]) ).
fof(f1058,plain,
( ~ sQ54_spl
| int_level(plus(t_139,n1)) = n0 ),
inference(resolution,[status(thm)],[f661,f124]) ).
fof(f1062,plain,
( ~ sQ54_spl
| gt(n0,n0) ),
inference(backward_demodulation,[status(thm)],[f1100,f197]) ).
fof(f1100,plain,
( ~ sQ54_spl
| fifo_length = n0 ),
inference(forward_demodulation,[status(thm)],[f368,f1058]) ).
fof(f1103,plain,
( ~ sQ54_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f1062,f493,f660]) ).
fof(f1122,plain,
( ~ sQ58_spl
| $false ),
inference(resolution,[status(thm)],[f838,f97]) ).
fof(f1143,plain,
~ sQ58_spl,
inference(contradiction_clause,[status(thm)],[f1122]) ).
fof(f1144,plain,
! [X0,X1] :
( sQ50_spl
| ~ p_Mem(X0,X1,plus(t_139,n1))
| p_Mem(X0,X1,plus(plus(t_139,n1),n1))
| p_Reset(plus(t_139,n1)) ),
inference(resolution,[status(thm)],[f647,f189]) ).
fof(f1146,plain,
( sQ50_spl
| wr_level(plus(plus(t_139,n1),n1)) = wr_level(plus(t_139,n1))
| p_Reset(plus(t_139,n1)) ),
inference(resolution,[status(thm)],[f647,f170]) ).
fof(f1147,definition,
! [X0,X1] :
( sQ82_spl
<=> ( ~ p_Mem(X0,X1,plus(t_139,n1))
| p_Mem(X0,X1,plus(plus(t_139,n1),n1)) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f1150,plain,
( sQ50_spl
| sQ82_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1144,f642,f1147,f645]) ).
fof(f1151,definition,
( sQ83_spl
<=> wr_level(plus(plus(t_139,n1),n1)) = wr_level(plus(t_139,n1)) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1154,plain,
( sQ50_spl
| sQ83_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1146,f642,f1151,f645]) ).
fof(f1206,plain,
( sQ39_spl
| int_level(plus(t_139,n1)) = int_level(t_139)
| p_Wr(t_139)
| p_Reset(t_139) ),
inference(resolution,[status(thm)],[f593,f242]) ).
fof(f1208,plain,
( sQ39_spl
| int_level(t_139) = n0 ),
inference(resolution,[status(thm)],[f593,f114]) ).
fof(f1215,plain,
( sQ39_spl
| sQ30_spl
| sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f1206,f457,f460,f510,f591]) ).
fof(f1217,plain,
( sQ39_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f1208,f394,f591]) ).
fof(f1231,plain,
( ~ sQ10_spl
| ~ sQ1_spl
| fifo_length = n0 ),
inference(forward_demodulation,[status(thm)],[f291,f395]) ).
fof(f1232,plain,
( ~ sQ10_spl
| ~ sQ1_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1231,f336]) ).
fof(f1233,plain,
( ~ sQ10_spl
| ~ sQ1_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f1232]) ).
fof(f1234,plain,
( ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f461,f194]) ).
fof(f1235,plain,
~ sQ22_spl,
inference(contradiction_clause,[status(thm)],[f1234]) ).
fof(f1290,plain,
! [X0] :
( ~ sQ51_spl
| ~ p_Data_in(X0,plus(t_139,n1))
| p_Mem(wr_level(plus(t_139,n1)),X0,plus(plus(t_139,n1),n1))
| ~ p_Wr(plus(t_139,n1))
| p_Reset(plus(t_139,n1)) ),
inference(resolution,[status(thm)],[f649,f165]) ).
fof(f1291,plain,
! [X0] :
( ~ sQ51_spl
| p_Data_in(X0,plus(t_139,n1))
| ~ p_Mem(wr_level(plus(t_139,n1)),X0,plus(plus(t_139,n1),n1))
| ~ p_Wr(plus(t_139,n1)) ),
inference(resolution,[status(thm)],[f649,f219]) ).
fof(f1292,definition,
! [X0] :
( sQ85_spl
<=> ( ~ p_Data_in(X0,plus(t_139,n1))
| p_Mem(wr_level(plus(t_139,n1)),X0,plus(plus(t_139,n1),n1)) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1295,plain,
( ~ sQ51_spl
| sQ85_spl
| ~ sQ50_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1290,f642,f645,f1292,f648]) ).
fof(f1296,definition,
! [X0] :
( sQ86_spl
<=> ( p_Data_in(X0,plus(t_139,n1))
| ~ p_Mem(wr_level(plus(t_139,n1)),X0,plus(plus(t_139,n1),n1)) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1299,plain,
( ~ sQ51_spl
| sQ86_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f1291,f645,f1296,f648]) ).
fof(f1305,plain,
( ~ sQ39_spl
| int_level(plus(t_139,n1)) = minus(int_level(t_139),n1)
| ~ p_Rd(t_139)
| p_Wr(t_139)
| p_Reset(t_139) ),
inference(resolution,[status(thm)],[f592,f172]) ).
fof(f1306,plain,
( ~ sQ39_spl
| gt(int_level(t_139),minus(int_level(t_139),n1)) ),
inference(resolution,[status(thm)],[f592,f99]) ).
fof(f1318,definition,
( sQ89_spl
<=> int_level(plus(t_139,n1)) = minus(int_level(t_139),n1) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f1319,plain,
( ~ sQ89_spl
| int_level(plus(t_139,n1)) = minus(int_level(t_139),n1) ),
inference(component_clause,[status(thm)],[f1318]) ).
fof(f1321,plain,
( ~ sQ39_spl
| sQ89_spl
| ~ sQ23_spl
| sQ22_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f1305,f457,f460,f463,f1318,f591]) ).
fof(f1322,plain,
( ~ sQ39_spl
| ~ sQ89_spl
| gt(int_level(t_139),fifo_length) ),
inference(backward_demodulation,[status(thm)],[f1323,f1306]) ).
fof(f1323,plain,
( ~ sQ89_spl
| fifo_length = minus(int_level(t_139),n1) ),
inference(forward_demodulation,[status(thm)],[f368,f1319]) ).
fof(f1327,plain,
( ~ sQ39_spl
| ~ sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1322,f257]) ).
fof(f1328,plain,
( ~ sQ39_spl
| ~ sQ89_spl ),
inference(contradiction_clause,[status(thm)],[f1327]) ).
fof(f1342,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f465,f193]) ).
fof(f1343,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f1342]) ).
fof(f1344,plain,
$false,
inference(sat_refutation,[status(thm)],[f293,f345,f374,f420,f449,f451,f477,f507,f522,f526,f545,f549,f560,f579,f633,f637,f658,f659,f663,f667,f684,f690,f694,f707,f730,f747,f758,f782,f802,f841,f843,f845,f858,f937,f980,f1011,f1049,f1051,f1103,f1143,f1150,f1154,f1215,f1217,f1233,f1235,f1295,f1299,f1321,f1328,f1343]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV017-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n016.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 20:53:22 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.13/0.55 % Refutation found
% 0.13/0.55 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.13/0.58 % Elapsed time: 0.214361 seconds
% 1.13/0.58 % CPU time: 1.381022 seconds
% 1.13/0.58 % Total memory used: 124.298 MB
% 1.13/0.58 % Net memory used: 121.188 MB
%------------------------------------------------------------------------------