%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : HWV031-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:40:21 PM UTC 2026
% Result : Unsatisfiable 92.83s 22.45s
% Output : CNFRefutation 92.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 31
% Syntax : Number of formulae : 371 ( 58 unt; 0 def)
% Number of atoms : 1018 ( 343 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 1082 ( 435 ~; 647 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 397 ( 0 sgn 397 !; 0 ?; 348 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : plus(X0,n1) != n0,
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_1) ).
fof(f2,axiom,
! [X0] : gt(plus(X0,n1),n0),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_2) ).
fof(f3,axiom,
! [X0] :
( gt(X0,minus(X0,n1))
| ~ gt(X0,n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_3) ).
fof(f4,axiom,
! [X2,X0,X1] :
( def_10(X1,X0)
| plus(X2,X1) = X0
| minus(X0,X1) != X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_4) ).
fof(f5,axiom,
! [X2,X0,X1] :
( def_10(X1,X0)
| plus(X2,X1) != X0
| minus(X0,X1) = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_5) ).
fof(f6,axiom,
! [X0,X1] :
( ~ gt(X1,X0)
| ~ def_10(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_6) ).
fof(f7,axiom,
! [X0,X1] :
( X1 != X0
| ~ def_10(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_7) ).
fof(f8,plain,
! [X0,X1] :
( X0 != X1
| ~ def_10(X0,X1) ),
inference(reorient_equations,[],[f7]) ).
fof(f9,axiom,
! [X0,X1] :
( gt(plus(X0,n1),plus(X1,n1))
| ~ gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_8) ).
fof(f10,axiom,
! [X0,X1] :
( ~ gt(plus(X0,n1),plus(X1,n1))
| gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_9) ).
fof(f13,axiom,
! [X0,X1] :
( X0 = X1
| gt(X0,X1)
| ~ gt(plus(X0,n1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_11) ).
fof(f14,axiom,
! [X0,X1] :
( gt(X1,X0)
| X1 = X0
| gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_12) ).
fof(f15,plain,
! [X0,X1] :
( gt(X1,X0)
| X0 = X1
| gt(X0,X1) ),
inference(reorient_equations,[],[f14]) ).
fof(f16,axiom,
! [X2,X0,X1] :
( ~ gt(X1,X2)
| gt(X0,X2)
| ~ gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_13) ).
fof(f17,axiom,
! [X0,X1] :
( gt(X0,plus(X1,n1))
| plus(X1,n1) = X0
| ~ gt(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_14) ).
fof(f18,axiom,
! [X0] :
( gt(X0,n0)
| X0 = n0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_15) ).
fof(f19,plain,
! [X0] :
( gt(X0,n0)
| n0 = X0 ),
inference(reorient_equations,[],[f18]) ).
fof(f22,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_17) ).
fof(f24,axiom,
! [X0] : plus(n0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_19) ).
fof(f25,axiom,
n1 = plus(n0,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_20) ).
fof(f35,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = n0
| ~ p_Reset(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_27) ).
fof(f36,plain,
! [X0] :
( n0 = wr_level(plus(X0,n1))
| ~ p_Reset(X0) ),
inference(reorient_equations,[],[f35]) ).
fof(f52,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = plus(wr_level(X0),n1)
| ~ gt(minus(fifo_length,n1),wr_level(X0))
| ~ gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_40) ).
fof(f53,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = n0
| gt(minus(fifo_length,n1),wr_level(X0))
| ~ gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_41) ).
fof(f54,plain,
! [X0] :
( n0 = wr_level(plus(X0,n1))
| gt(minus(fifo_length,n1),wr_level(X0))
| ~ gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(reorient_equations,[],[f53]) ).
fof(f56,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = wr_level(X0)
| gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_43) ).
fof(f85,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = plus(wr_level(X0),n1)
| ~ gt(minus(fifo_length,n1),wr_level(X0))
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_67) ).
fof(f86,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = n0
| gt(minus(fifo_length,n1),wr_level(X0))
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_68) ).
fof(f87,plain,
! [X0] :
( n0 = wr_level(plus(X0,n1))
| gt(minus(fifo_length,n1),wr_level(X0))
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(reorient_equations,[],[f86]) ).
fof(f88,axiom,
! [X0] :
( wr_level(plus(X0,n1)) = wr_level(X0)
| p_Wr(X0)
| p_Reset(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV003-0.ax',axiom_69) ).
fof(f113,negated_conjecture,
~ gt(plus(wr_level(x_139),n1),fifo_length),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_1) ).
fof(f114,negated_conjecture,
gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_2) ).
fof(f115,negated_conjecture,
gt(fifo_length,n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_3) ).
fof(f116,plain,
! [X0,X1] :
( def_10(X1,X0)
| plus(minus(X0,X1),X1) = X0 ),
inference(equality_resolution,[],[f4]) ).
fof(f117,plain,
! [X2,X1] :
( def_10(X1,plus(X2,X1))
| minus(plus(X2,X1),X1) = X2 ),
inference(equality_resolution,[],[f5]) ).
fof(f118,plain,
! [X1] : ~ def_10(X1,X1),
inference(equality_resolution,[],[f8]) ).
tcf(c_142,plain,
! [X0: $i] : plus(X0,n1) != n0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_143,plain,
! [X0: $i] : gt(plus(X0,n1),n0),
inference(cnf_transformation,[],[f2]) ).
tcf(c_144,plain,
! [X0: $i] :
( gt(X0,minus(X0,n1))
| ~ gt(X0,n0) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i] :
( def_10(X1,X0)
| ( plus(minus(X0,X1),X1) = X0 ) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] :
( def_10(X1,plus(X0,X1))
| ( minus(plus(X0,X1),X1) = X0 ) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_147,plain,
! [X0: $i,X1: $i] :
( ~ def_10(X1,X0)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_148,plain,
! [X0: $i] : ~ def_10(X0,X0),
inference(cnf_transformation,[],[f118]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i] :
( gt(plus(X0,n1),plus(X1,n1))
| ~ gt(X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_150,plain,
! [X0: $i,X1: $i] :
( gt(X0,X1)
| ~ gt(plus(X0,n1),plus(X1,n1)) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i] :
( gt(X0,X1)
| ( X0 = X1 )
| ~ gt(plus(X0,n1),X1) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X0,X2)
| ~ gt(X1,X2)
| ~ gt(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i] :
( gt(X0,plus(X1,n1))
| ( plus(X1,n1) = X0 )
| ~ gt(X0,X1) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_156,plain,
! [X0: $i] :
( gt(X0,n0)
| ( X0 = n0 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_158,plain,
! [X0: $i] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f22]) ).
tcf(c_160,plain,
! [X0: $i] : plus(n0,X0) = X0,
inference(cnf_transformation,[],[f24]) ).
tcf(c_161,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[],[f25]) ).
tcf(c_167,plain,
! [X0: $i] :
( ( wr_level(plus(X0,n1)) = n0 )
| ~ p_Reset(X0) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_180,plain,
! [X0: $i] :
( p_Rd(X0)
| p_Reset(X0)
| ( wr_level(plus(X0,n1)) = plus(wr_level(X0),n1) )
| ~ p_Wr(X0)
| ~ gt(fifo_length,int_level(X0))
| ~ gt(minus(fifo_length,n1),wr_level(X0)) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_181,plain,
! [X0: $i] :
( p_Rd(X0)
| p_Reset(X0)
| gt(minus(fifo_length,n1),wr_level(X0))
| ( wr_level(plus(X0,n1)) = n0 )
| ~ p_Wr(X0)
| ~ gt(fifo_length,int_level(X0)) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_183,plain,
! [X0: $i] :
( p_Rd(X0)
| p_Reset(X0)
| gt(fifo_length,int_level(X0))
| ( wr_level(plus(X0,n1)) = wr_level(X0) )
| ~ p_Wr(X0) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_207,plain,
! [X0: $i] :
( p_Reset(X0)
| ( wr_level(plus(X0,n1)) = plus(wr_level(X0),n1) )
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| ~ gt(minus(fifo_length,n1),wr_level(X0)) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_208,plain,
! [X0: $i] :
( p_Reset(X0)
| gt(minus(fifo_length,n1),wr_level(X0))
| ( wr_level(plus(X0,n1)) = n0 )
| ~ p_Rd(X0)
| ~ p_Wr(X0) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_209,plain,
! [X0: $i] :
( p_Wr(X0)
| p_Reset(X0)
| ( wr_level(plus(X0,n1)) = wr_level(X0) ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_231,negated_conjecture,
~ gt(plus(wr_level(x_139),n1),fifo_length),
inference(cnf_transformation,[],[f113]) ).
tcf(c_232,negated_conjecture,
gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length),
inference(cnf_transformation,[],[f114]) ).
tcf(c_233,negated_conjecture,
gt(fifo_length,n0),
inference(cnf_transformation,[],[f115]) ).
tcf(c_234,plain,
~ gt(n1,n1),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_235,plain,
~ def_10(n1,n1),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_251,plain,
( gt(n1,n1)
| ( n1 = n1 ) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_371,plain,
! [X0: $i] :
( p_Rd(X0)
| p_Reset(X0)
| gt(fifo_length,int_level(X0))
| ( wr_level(plus(X0,n1)) = wr_level(X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_183,c_209,c_183]) ).
tcf(c_382,plain,
! [X0: $i] :
( ~ p_Wr(X0)
| ~ p_Rd(X0)
| ( wr_level(plus(X0,n1)) = n0 )
| gt(minus(fifo_length,n1),wr_level(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_208,c_167,c_208]) ).
tcf(c_383,plain,
! [X0: $i] :
( gt(minus(fifo_length,n1),wr_level(X0))
| ( wr_level(plus(X0,n1)) = n0 )
| ~ p_Rd(X0)
| ~ p_Wr(X0) ),
inference(renaming,[status(thm)],[c_382]) ).
tcf(c_417,plain,
! [X0: $i] :
( gt(minus(fifo_length,n1),wr_level(X0))
| ( wr_level(plus(X0,n1)) = n0 )
| ~ p_Wr(X0)
| ~ gt(fifo_length,int_level(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_181,c_167,c_181,c_383]) ).
tcf(c_429,plain,
! [X0: $i] :
( ~ gt(minus(fifo_length,n1),wr_level(X0))
| ~ gt(fifo_length,int_level(X0))
| ~ p_Wr(X0)
| ( wr_level(plus(X0,n1)) = plus(wr_level(X0),n1) )
| p_Reset(X0) ),
inference(global_subsumption_just,[status(thm)],[c_180,c_207,c_180]) ).
tcf(c_430,plain,
! [X0: $i] :
( p_Reset(X0)
| ( wr_level(plus(X0,n1)) = plus(wr_level(X0),n1) )
| ~ p_Wr(X0)
| ~ gt(fifo_length,int_level(X0))
| ~ gt(minus(fifo_length,n1),wr_level(X0)) ),
inference(renaming,[status(thm)],[c_429]) ).
tcf(c_9164,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_9166,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9169,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( gt(X0,X2)
| ~ gt(X1,X3)
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_9171,plain,
! [X0: $i,X1: $i,X2: $i] :
( def_10(X2,X0)
| ~ def_10(X2,X1)
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_10197,plain,
( gt(fifo_length,minus(fifo_length,n1))
| ~ gt(fifo_length,n0) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_10203,plain,
( gt(plus(fifo_length,n1),plus(n0,n1))
| ~ gt(fifo_length,n0) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_10212,plain,
! [X0: $i] :
( gt(X0,fifo_length)
| ~ gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length)
| ~ gt(X0,plus(wr_level(plus(x_139,n1)),n1)) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_10214,plain,
! [X0: $i] :
( gt(X0,n0)
| ~ gt(fifo_length,n0)
| ~ gt(X0,fifo_length) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_10222,plain,
! [X0: $i,X1: $i] :
( gt(X0,X1)
| ~ gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length)
| ( X1 != fifo_length )
| ( X0 != plus(wr_level(plus(x_139,n1)),n1) ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_10224,plain,
! [X0: $i,X1: $i] :
( gt(X0,X1)
| ~ gt(fifo_length,n0)
| ( X1 != n0 )
| ( X0 != fifo_length ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_10226,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X0,X2)
| ~ gt(plus(X1,n1),n0)
| ( X2 != n0 )
| ( X0 != plus(X1,n1) ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_10231,plain,
( gt(plus(fifo_length,n1),plus(minus(fifo_length,n1),n1))
| ~ gt(fifo_length,minus(fifo_length,n1)) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_10232,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| ~ gt(X0,fifo_length)
| ~ gt(fifo_length,minus(fifo_length,n1)) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_10234,plain,
! [X0: $i,X1: $i] :
( gt(X0,X1)
| ~ gt(fifo_length,minus(fifo_length,n1))
| ( X1 != minus(fifo_length,n1) )
| ( X0 != fifo_length ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_10236,plain,
gt(n1,n0),
inference(superposition,[status(thm)],[c_160,c_143]) ).
tcf(c_10257,plain,
! [X0: $i] :
( gt(X0,plus(n0,n1))
| ~ gt(X0,plus(fifo_length,n1))
| ~ gt(plus(fifo_length,n1),plus(n0,n1)) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_10258,plain,
( gt(n1,plus(n0,n1))
| ~ gt(n1,plus(fifo_length,n1))
| ~ gt(plus(fifo_length,n1),plus(n0,n1)) ),
inference(instantiation,[status(thm)],[c_10257]) ).
tcf(c_10259,plain,
! [X0: $i,X1: $i] :
( gt(X0,X1)
| ~ gt(plus(fifo_length,n1),plus(n0,n1))
| ( X1 != plus(n0,n1) )
| ( X0 != plus(fifo_length,n1) ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_10260,plain,
( gt(n1,n1)
| ~ gt(plus(fifo_length,n1),plus(n0,n1))
| ( n1 != plus(n0,n1) )
| ( n1 != plus(fifo_length,n1) ) ),
inference(instantiation,[status(thm)],[c_10259]) ).
tcf(c_10262,plain,
! [X0: $i] :
( gt(X0,plus(fifo_length,n1))
| ( plus(fifo_length,n1) = X0 )
| ~ gt(X0,fifo_length) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_10265,plain,
( gt(n1,plus(fifo_length,n1))
| ( plus(fifo_length,n1) = n1 )
| ~ gt(n1,fifo_length) ),
inference(instantiation,[status(thm)],[c_10262]) ).
tcf(c_10267,plain,
( gt(fifo_length,fifo_length)
| ~ gt(fifo_length,plus(wr_level(plus(x_139,n1)),n1))
| ~ gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length) ),
inference(instantiation,[status(thm)],[c_10212]) ).
tcf(c_10268,plain,
~ gt(fifo_length,fifo_length),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_10306,plain,
( gt(fifo_length,plus(wr_level(x_139),n1))
| ( plus(wr_level(x_139),n1) = fifo_length ) ),
inference(superposition,[status(thm)],[c_153,c_231]) ).
tcf(c_10311,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,fifo_length)
| ( X0 = fifo_length ) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_10312,plain,
! [X0: $i] :
( gt(X0,fifo_length)
| ( X0 = fifo_length )
| ~ gt(plus(X0,n1),fifo_length) ),
inference(instantiation,[status(thm)],[c_152]) ).
tcf(c_10316,plain,
( gt(fifo_length,n1)
| gt(n1,fifo_length)
| ( n1 = fifo_length ) ),
inference(instantiation,[status(thm)],[c_10311]) ).
tcf(c_10321,plain,
! [X0: $i] :
( def_10(X0,fifo_length)
| ( plus(minus(fifo_length,X0),X0) = fifo_length ) ),
inference(instantiation,[status(thm)],[c_145]) ).
tcf(c_10323,plain,
( def_10(n1,fifo_length)
| ( plus(minus(fifo_length,n1),n1) = fifo_length ) ),
inference(instantiation,[status(thm)],[c_10321]) ).
tcf(c_10329,plain,
fifo_length = fifo_length,
inference(instantiation,[status(thm)],[c_9164]) ).
tcf(c_10331,plain,
! [X0: $i,X1: $i] :
( ( X0 = fifo_length )
| ( fifo_length != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_9166]) ).
tcf(c_10386,plain,
! [X0: $i] :
( gt(plus(X0,n1),plus(n0,n1))
| ~ gt(X0,n0) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_10388,plain,
! [X0: $i,X1: $i] :
( gt(X0,n0)
| ~ gt(X1,n0)
| ~ gt(X0,X1) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_10389,plain,
( gt(n0,n0)
| ( n0 = n0 ) ),
inference(instantiation,[status(thm)],[c_156]) ).
tcf(c_10390,plain,
~ gt(n0,n0),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_10391,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X0,X2)
| ~ gt(X1,n0)
| ( X2 != n0 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_10414,plain,
! [X0: $i] :
( gt(plus(X0,n1),n1)
| ~ gt(X0,n0) ),
inference(superposition,[status(thm)],[c_160,c_149]) ).
tcf(c_10436,plain,
! [X0: $i] :
( gt(n0,X0)
| ~ gt(n1,plus(X0,n1)) ),
inference(superposition,[status(thm)],[c_160,c_150]) ).
tcf(c_10445,plain,
! [X0: $i] :
( gt(plus(X0,n1),plus(minus(X0,n1),n1))
| ~ gt(X0,minus(X0,n1)) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_10455,plain,
! [X0: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_232,c_154]) ).
tcf(c_10456,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ~ gt(n0,X0) ),
inference(superposition,[status(thm)],[c_233,c_154]) ).
tcf(c_10457,plain,
! [X0: $i,X1: $i] :
( gt(plus(X1,n1),X0)
| ~ gt(n0,X0) ),
inference(superposition,[status(thm)],[c_143,c_154]) ).
tcf(c_10458,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| ( X1 = n0 )
| ~ gt(n0,X0) ),
inference(superposition,[status(thm)],[c_156,c_154]) ).
tcf(c_10462,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X2,X1)
| gt(X0,X2)
| ( X0 = X2 )
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_153,c_154]) ).
tcf(c_10464,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ( plus(wr_level(x_139),n1) = fifo_length )
| ~ gt(plus(wr_level(x_139),n1),X0) ),
inference(superposition,[status(thm)],[c_10306,c_154]) ).
tcf(c_10477,plain,
! [X0: $i] :
( gt(X0,plus(wr_level(plus(x_139,n1)),n1))
| ( X0 = plus(wr_level(plus(x_139,n1)),n1) )
| ~ gt(plus(X0,n1),plus(wr_level(plus(x_139,n1)),n1)) ),
inference(instantiation,[status(thm)],[c_152]) ).
tcf(c_10495,plain,
! [X0: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ~ gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length)
| ( X0 != fifo_length )
| ( plus(wr_level(plus(x_139,n1)),n1) != plus(wr_level(plus(x_139,n1)),n1) ) ),
inference(instantiation,[status(thm)],[c_10222]) ).
tcf(c_10496,plain,
plus(wr_level(plus(x_139,n1)),n1) = plus(wr_level(plus(x_139,n1)),n1),
inference(instantiation,[status(thm)],[c_9164]) ).
tcf(c_10498,plain,
! [X0: $i,X1: $i] :
( ( X1 = plus(wr_level(plus(x_139,n1)),n1) )
| ( X1 != X0 )
| ( plus(wr_level(plus(x_139,n1)),n1) != X0 ) ),
inference(instantiation,[status(thm)],[c_9166]) ).
tcf(c_10546,plain,
! [X0: $i] :
( gt(X0,n0)
| ~ gt(fifo_length,n0)
| ( n0 != n0 )
| ( X0 != fifo_length ) ),
inference(instantiation,[status(thm)],[c_10224]) ).
tcf(c_10662,plain,
! [X0: $i,X1: $i] :
( ( n0 = X0 )
| ( n0 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_9166]) ).
tcf(c_10697,plain,
! [X0: $i,X1: $i] :
( gt(plus(X0,n1),X1)
| ~ gt(plus(X0,n1),n0)
| ( X1 != n0 )
| ( plus(X0,n1) != plus(X0,n1) ) ),
inference(instantiation,[status(thm)],[c_10226]) ).
tcf(c_10698,plain,
! [X0: $i] : plus(X0,n1) = plus(X0,n1),
inference(instantiation,[status(thm)],[c_9164]) ).
tcf(c_10700,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = plus(X0,n1) )
| ( X2 != X1 )
| ( plus(X0,n1) != X1 ) ),
inference(instantiation,[status(thm)],[c_9166]) ).
tcf(c_10719,plain,
! [X0: $i] : ~ gt(n0,plus(X0,n1)),
inference(superposition,[status(thm)],[c_10457,c_158]) ).
tcf(c_10907,plain,
! [X0: $i] :
( gt(wr_level(plus(x_139,n1)),X0)
| ~ gt(fifo_length,plus(X0,n1)) ),
inference(superposition,[status(thm)],[c_10455,c_150]) ).
tcf(c_10922,plain,
! [X0: $i] :
( gt(X0,n0)
| ~ gt(X0,fifo_length) ),
inference(resolution,[status(thm)],[c_154,c_233]) ).
tcf(c_11194,plain,
( gt(wr_level(plus(x_139,n1)),fifo_length)
| ( wr_level(plus(x_139,n1)) = fifo_length ) ),
inference(resolution,[status(thm)],[c_152,c_232]) ).
tcf(c_11216,plain,
! [X0: $i,X1: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(fifo_length,X0)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_10455,c_154]) ).
tcf(c_11462,plain,
! [X0: $i] :
( gt(fifo_length,plus(X0,n1))
| gt(plus(X0,n1),fifo_length)
| ( plus(X0,n1) = fifo_length ) ),
inference(instantiation,[status(thm)],[c_10311]) ).
tcf(c_11478,plain,
! [X0: $i,X1: $i] :
( def_10(X1,X0)
| ~ def_10(X1,fifo_length)
| ( X0 != fifo_length ) ),
inference(instantiation,[status(thm)],[c_9171]) ).
tcf(c_11479,plain,
( def_10(n1,n1)
| ~ def_10(n1,fifo_length)
| ( n1 != fifo_length ) ),
inference(instantiation,[status(thm)],[c_11478]) ).
tcf(c_11485,plain,
! [X0: $i] :
( gt(wr_level(plus(x_139,n1)),X0)
| ~ gt(plus(wr_level(plus(x_139,n1)),n1),plus(X0,n1)) ),
inference(instantiation,[status(thm)],[c_150]) ).
tcf(c_11519,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X0,X2)
| ~ gt(plus(X1,n1),plus(n0,n1))
| ( X2 != plus(n0,n1) )
| ( X0 != plus(X1,n1) ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_11543,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X0,X2)
| ~ gt(X1,plus(n0,n1))
| ( X2 != plus(n0,n1) )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_11544,plain,
( gt(n1,n1)
| ~ gt(n1,plus(n0,n1))
| ( n1 != n1 )
| ( n1 != plus(n0,n1) ) ),
inference(instantiation,[status(thm)],[c_11543]) ).
tcf(c_11550,plain,
! [X0: $i,X1: $i] :
( gt(X1,n0)
| gt(X0,X1)
| ( X1 = n0 )
| ( X0 = n0 ) ),
inference(superposition,[status(thm)],[c_153,c_10458]) ).
tcf(c_11642,plain,
( gt(plus(wr_level(plus(x_139,n1)),n1),plus(wr_level(plus(x_139,n1)),n1))
| ~ gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length)
| ( plus(wr_level(plus(x_139,n1)),n1) != fifo_length )
| ( plus(wr_level(plus(x_139,n1)),n1) != plus(wr_level(plus(x_139,n1)),n1) ) ),
inference(instantiation,[status(thm)],[c_10495]) ).
tcf(c_11643,plain,
~ gt(plus(wr_level(plus(x_139,n1)),n1),plus(wr_level(plus(x_139,n1)),n1)),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_11644,plain,
! [X0: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),plus(X0,n1))
| ~ gt(plus(wr_level(plus(x_139,n1)),n1),fifo_length)
| ( plus(X0,n1) != fifo_length )
| ( plus(wr_level(plus(x_139,n1)),n1) != plus(wr_level(plus(x_139,n1)),n1) ) ),
inference(instantiation,[status(thm)],[c_10495]) ).
tcf(c_11738,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| ~ gt(fifo_length,minus(fifo_length,n1))
| ( X0 != fifo_length )
| ( minus(fifo_length,n1) != minus(fifo_length,n1) ) ),
inference(instantiation,[status(thm)],[c_10234]) ).
tcf(c_11739,plain,
minus(fifo_length,n1) = minus(fifo_length,n1),
inference(instantiation,[status(thm)],[c_9164]) ).
tcf(c_11871,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,plus(wr_level(x_139),n1))
| ( plus(wr_level(x_139),n1) = fifo_length )
| ( plus(wr_level(x_139),n1) = X0 ) ),
inference(superposition,[status(thm)],[c_153,c_10464]) ).
tcf(c_11949,plain,
! [X0: $i] :
( gt(wr_level(plus(x_139,n1)),X0)
| ~ gt(fifo_length,plus(X0,n1)) ),
inference(superposition,[status(thm)],[c_10455,c_150]) ).
tcf(c_11968,plain,
! [X0: $i,X1: $i] :
( gt(plus(X0,n1),X1)
| ~ gt(n1,X1)
| ~ gt(X0,n0) ),
inference(superposition,[status(thm)],[c_10414,c_154]) ).
tcf(c_11969,plain,
! [X0: $i,X1: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(fifo_length,X0)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_10455,c_154]) ).
tcf(c_12022,plain,
! [X0: $i,X1: $i] :
( gt(wr_level(plus(x_139,n1)),X1)
| ~ gt(X0,X1)
| ~ gt(fifo_length,plus(X0,n1)) ),
inference(superposition,[status(thm)],[c_11949,c_154]) ).
tcf(c_12040,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ( X0 = X1 )
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_153,c_11969]) ).
tcf(c_12056,plain,
! [X0: $i,X1: $i] :
( gt(plus(X0,n1),fifo_length)
| gt(wr_level(plus(x_139,n1)),X1)
| ( plus(X0,n1) = fifo_length )
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_153,c_12022]) ).
tcf(c_12195,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ( X0 = n0 ) ),
inference(superposition,[status(thm)],[c_233,c_12040]) ).
tcf(c_12197,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ( minus(fifo_length,n1) = X0 )
| ~ gt(fifo_length,n0) ),
inference(superposition,[status(thm)],[c_144,c_12040]) ).
tcf(c_12205,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ( minus(fifo_length,n1) = X0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_12197,c_233]) ).
tcf(c_12210,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X0) ),
inference(global_subsumption_just,[status(thm)],[c_12195,c_232,c_10311,c_10455,c_10495,c_10496,c_10922]) ).
tcf(c_12335,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(wr_level(plus(x_139,n1)),X0)
| ( wr_level(plus(x_139,n1)) = X0 ) ),
inference(superposition,[status(thm)],[c_12210,c_152]) ).
tcf(c_12342,plain,
! [X0: $i] :
( gt(n0,X0)
| ( X0 = n0 )
| ~ gt(n1,X0) ),
inference(superposition,[status(thm)],[c_160,c_152]) ).
tcf(c_12356,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = plus(wr_level(plus(x_139,n1)),n1) )
| ( X2 != plus(X0,X1) )
| ( plus(wr_level(plus(x_139,n1)),n1) != plus(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_10498]) ).
tcf(c_12361,plain,
! [X0: $i] :
( ( plus(wr_level(plus(x_139,n1)),n1) = fifo_length )
| ( fifo_length != X0 )
| ( plus(wr_level(plus(x_139,n1)),n1) != X0 ) ),
inference(instantiation,[status(thm)],[c_10331]) ).
tcf(c_12399,plain,
! [X0: $i,X1: $i] :
( gt(X1,n0)
| ( X1 = X0 )
| ( X0 != n0 ) ),
inference(resolution,[status(thm)],[c_9166,c_156]) ).
tcf(c_12413,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_9166,c_9164]) ).
tcf(c_12444,plain,
! [X0: $i,X1: $i] :
( ( X1 = wr_level(plus(x_139,n1)) )
| ( X1 != X0 )
| ( wr_level(plus(x_139,n1)) != X0 ) ),
inference(instantiation,[status(thm)],[c_9166]) ).
tcf(c_12445,plain,
( ( n1 = wr_level(plus(x_139,n1)) )
| ( n1 != n1 )
| ( wr_level(plus(x_139,n1)) != n1 ) ),
inference(instantiation,[status(thm)],[c_12444]) ).
tcf(c_12451,plain,
( gt(wr_level(plus(x_139,n1)),plus(fifo_length,n1))
| ( plus(fifo_length,n1) = wr_level(plus(x_139,n1)) )
| ~ gt(wr_level(plus(x_139,n1)),fifo_length) ),
inference(instantiation,[status(thm)],[c_10262]) ).
tcf(c_12489,plain,
( ~ gt(n1,fifo_length)
| ~ gt(wr_level(x_139),n0) ),
inference(superposition,[status(thm)],[c_11968,c_231]) ).
tcf(c_12609,plain,
( ( wr_level(x_139) = n0 )
| ~ gt(n1,fifo_length) ),
inference(superposition,[status(thm)],[c_156,c_12489]) ).
tcf(c_12618,plain,
! [X0: $i] :
( gt(n0,plus(X0,n1))
| ~ gt(n0,X0) ),
inference(resolution,[status(thm)],[c_155,c_142]) ).
tcf(c_12648,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0) ),
inference(global_subsumption_just,[status(thm)],[c_12205,c_233,c_232,c_10197,c_10232,c_10311,c_10455,c_10495,c_10496]) ).
tcf(c_12721,plain,
( gt(fifo_length,n1)
| ( n1 = fifo_length )
| ( wr_level(x_139) = n0 ) ),
inference(superposition,[status(thm)],[c_153,c_12609]) ).
tcf(c_13071,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X0,X2)
| ~ gt(plus(X1,n1),plus(minus(X1,n1),n1))
| ( X2 != plus(minus(X1,n1),n1) )
| ( X0 != plus(X1,n1) ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_13129,plain,
! [X0: $i] :
( ( n0 = X0 )
| ( n0 != n0 )
| ( X0 != n0 ) ),
inference(instantiation,[status(thm)],[c_10662]) ).
tcf(c_13166,plain,
! [X0: $i,X1: $i] :
( gt(X0,n0)
| ~ gt(X1,n0)
| ( n0 != n0 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_10391]) ).
tcf(c_13251,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(wr_level(plus(x_139,n1)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_12335,c_233,c_232,c_10214,c_10312,c_10389,c_10390,c_10496,c_10546,c_10907,c_11462,c_11485,c_11644]) ).
tcf(c_13259,plain,
gt(wr_level(plus(x_139,n1)),n0),
inference(superposition,[status(thm)],[c_13251,c_158]) ).
tcf(c_13295,plain,
! [X0: $i] :
( gt(fifo_length,plus(X0,n1))
| ( plus(X0,n1) = n0 )
| ~ gt(n0,X0) ),
inference(superposition,[status(thm)],[c_155,c_10456]) ).
tcf(c_13299,plain,
! [X0: $i] :
( gt(fifo_length,plus(X0,n1))
| ~ gt(n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_13295,c_142]) ).
tcf(c_13329,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X2,X1)
| ~ gt(X2,plus(X0,n1))
| ~ gt(plus(X0,n1),X1) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_13561,plain,
! [X0: $i] :
( ( X0 = plus(n0,n1) )
| ( X0 != n1 )
| ( plus(n0,n1) != n1 ) ),
inference(instantiation,[status(thm)],[c_10700]) ).
tcf(c_13563,plain,
( ( n1 = plus(n0,n1) )
| ( n1 != n1 )
| ( plus(n0,n1) != n1 ) ),
inference(instantiation,[status(thm)],[c_13561]) ).
tcf(c_13564,plain,
! [X0: $i,X1: $i] :
( ( X1 = plus(minus(X0,n1),n1) )
| ( X1 != X0 )
| ( plus(minus(X0,n1),n1) != X0 ) ),
inference(instantiation,[status(thm)],[c_10700]) ).
tcf(c_13565,plain,
! [X0: $i] :
( def_10(n1,X0)
| ( plus(minus(X0,n1),n1) = X0 ) ),
inference(instantiation,[status(thm)],[c_145]) ).
tcf(c_13568,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( plus(X0,n1) = X2 )
| ( X2 != X1 )
| ( plus(X0,n1) != X1 ) ),
inference(instantiation,[status(thm)],[c_9166]) ).
tcf(c_13572,plain,
! [X0: $i,X1: $i] :
( ( X1 = plus(X0,n1) )
| ( X1 != fifo_length )
| ( plus(X0,n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_10700]) ).
tcf(c_13580,plain,
! [X0: $i,X1: $i] :
( ( X1 = plus(fifo_length,n1) )
| ( X1 != X0 )
| ( plus(fifo_length,n1) != X0 ) ),
inference(instantiation,[status(thm)],[c_10700]) ).
tcf(c_13581,plain,
( ( n1 = plus(fifo_length,n1) )
| ( n1 != n1 )
| ( plus(fifo_length,n1) != n1 ) ),
inference(instantiation,[status(thm)],[c_13580]) ).
tcf(c_13796,plain,
! [X0: $i] :
( gt(fifo_length,plus(X0,n1))
| ( plus(X0,n1) = fifo_length )
| ~ gt(fifo_length,X0) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_13827,plain,
! [X0: $i,X1: $i] :
( ( fifo_length = X0 )
| ( fifo_length != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_9166]) ).
tcf(c_14070,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( gt(X3,X2)
| gt(X2,X3)
| gt(X0,X3)
| ~ gt(X1,X2)
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_9169,c_153]) ).
tcf(c_14114,plain,
! [X0: $i] :
( gt(X0,plus(fifo_length,n1))
| ~ gt(X0,wr_level(plus(x_139,n1)))
| ~ gt(wr_level(plus(x_139,n1)),plus(fifo_length,n1)) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_14115,plain,
( gt(n1,plus(fifo_length,n1))
| ~ gt(n1,wr_level(plus(x_139,n1)))
| ~ gt(wr_level(plus(x_139,n1)),plus(fifo_length,n1)) ),
inference(instantiation,[status(thm)],[c_14114]) ).
tcf(c_14309,plain,
! [X0: $i] : ~ gt(n0,X0),
inference(global_subsumption_just,[status(thm)],[c_13299,c_10719,c_12618]) ).
tcf(c_14312,plain,
! [X0: $i] :
( ( X0 = n0 )
| ~ gt(n1,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[c_12342,c_14309]) ).
tcf(c_14315,plain,
! [X0: $i] : ~ gt(n1,plus(X0,n1)),
inference(backward_subsumption_resolution,[status(thm)],[c_10436,c_14309]) ).
tcf(c_14342,plain,
( gt(fifo_length,n1)
| ( n1 = fifo_length ) ),
inference(global_subsumption_just,[status(thm)],[c_12721,c_233,c_234,c_161,c_251,c_10203,c_10258,c_10260,c_10265,c_10316,c_11544,c_13563,c_13581]) ).
tcf(c_14350,plain,
( ( n1 = fifo_length )
| ~ def_10(n1,fifo_length) ),
inference(superposition,[status(thm)],[c_14342,c_147]) ).
tcf(c_14394,plain,
( gt(fifo_length,n1)
| ( plus(wr_level(x_139),n1) = fifo_length )
| ( plus(wr_level(x_139),n1) = n1 ) ),
inference(superposition,[status(thm)],[c_11871,c_14315]) ).
tcf(c_14427,plain,
! [X0: $i] :
( gt(wr_level(plus(x_139,n1)),X0)
| gt(plus(plus(wr_level(plus(x_139,n1)),n1),n1),fifo_length)
| ( plus(plus(wr_level(plus(x_139,n1)),n1),n1) = fifo_length )
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_10455,c_12056]) ).
tcf(c_14594,plain,
! [X0: $i] :
( gt(wr_level(plus(x_139,n1)),X0)
| ~ gt(fifo_length,X0) ),
inference(global_subsumption_just,[status(thm)],[c_14427,c_232,c_10496,c_10907,c_11485,c_11644,c_13796]) ).
tcf(c_14880,plain,
! [X0: $i] :
( gt(plus(fifo_length,n1),X0)
| ~ gt(plus(fifo_length,n1),plus(n0,n1))
| ( X0 != plus(n0,n1) )
| ( plus(fifo_length,n1) != plus(fifo_length,n1) ) ),
inference(instantiation,[status(thm)],[c_10259]) ).
tcf(c_14881,plain,
plus(fifo_length,n1) = plus(fifo_length,n1),
inference(instantiation,[status(thm)],[c_10698]) ).
tcf(c_14882,plain,
( gt(plus(fifo_length,n1),n1)
| ~ gt(plus(fifo_length,n1),plus(n0,n1))
| ( n1 != plus(n0,n1) )
| ( plus(fifo_length,n1) != plus(fifo_length,n1) ) ),
inference(instantiation,[status(thm)],[c_14880]) ).
tcf(c_14943,plain,
! [X0: $i] : ~ gt(n1,plus(X0,n1)),
inference(backward_subsumption_resolution,[status(thm)],[c_10436,c_14309]) ).
tcf(c_15024,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,plus(wr_level(x_139),n1))
| ( plus(wr_level(x_139),n1) = fifo_length )
| ( plus(wr_level(x_139),n1) = X0 ) ),
inference(superposition,[status(thm)],[c_153,c_10464]) ).
tcf(c_15046,plain,
( gt(fifo_length,n1)
| ( plus(wr_level(x_139),n1) = fifo_length )
| ( plus(wr_level(x_139),n1) = n1 ) ),
inference(superposition,[status(thm)],[c_15024,c_14943]) ).
tcf(c_15052,plain,
( ( plus(wr_level(x_139),n1) = fifo_length )
| ( plus(wr_level(x_139),n1) = n1 )
| ~ def_10(n1,fifo_length) ),
inference(superposition,[status(thm)],[c_15046,c_147]) ).
tcf(c_15063,plain,
~ def_10(n1,fifo_length),
inference(global_subsumption_just,[status(thm)],[c_15052,c_235,c_11479,c_14350]) ).
tcf(c_15114,plain,
! [X0: $i,X1: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(fifo_length,X0)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_10455,c_154]) ).
tcf(c_15140,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ( X0 = X1 )
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_153,c_15114]) ).
tcf(c_15273,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ( X0 = n0 ) ),
inference(superposition,[status(thm)],[c_233,c_15140]) ).
tcf(c_15275,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ( minus(fifo_length,n1) = X0 )
| ~ gt(fifo_length,n0) ),
inference(superposition,[status(thm)],[c_144,c_15140]) ).
tcf(c_15283,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ( minus(fifo_length,n1) = X0 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15275,c_233]) ).
tcf(c_15284,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X0) ),
inference(global_subsumption_just,[status(thm)],[c_15273,c_12210]) ).
tcf(c_15293,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0) ),
inference(global_subsumption_just,[status(thm)],[c_15283,c_12648]) ).
tcf(c_15298,plain,
! [X0: $i,X1: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_15293,c_154]) ).
tcf(c_15321,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(wr_level(plus(x_139,n1)),X0)
| ( wr_level(plus(x_139,n1)) = X0 ) ),
inference(superposition,[status(thm)],[c_15284,c_152]) ).
tcf(c_15418,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(wr_level(plus(x_139,n1)),X0) ),
inference(global_subsumption_just,[status(thm)],[c_15321,c_13251]) ).
tcf(c_15424,plain,
! [X0: $i,X1: $i] :
( gt(X0,n0)
| gt(wr_level(plus(x_139,n1)),X1)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_15418,c_154]) ).
tcf(c_15436,plain,
! [X0: $i,X1: $i] :
( gt(plus(X0,n1),minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),plus(X1,n1))
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_149,c_15298]) ).
tcf(c_15484,plain,
! [X0: $i] :
( gt(X0,n1)
| ( plus(n0,n1) = X0 )
| ~ gt(X0,n0) ),
inference(superposition,[status(thm)],[c_160,c_155]) ).
tcf(c_15489,plain,
! [X0: $i,X1: $i] :
( ( plus(X0,n1) = X1 )
| ~ gt(X1,X0)
| ~ def_10(plus(X0,n1),X1) ),
inference(superposition,[status(thm)],[c_155,c_147]) ).
tcf(c_15522,plain,
! [X0: $i] :
( gt(X0,n1)
| ( X0 = n1 )
| ~ gt(X0,n0) ),
inference(demodulation,[status(thm)],[c_15484,c_160]) ).
tcf(c_15529,plain,
( gt(fifo_length,n1)
| ( n1 = fifo_length ) ),
inference(superposition,[status(thm)],[c_233,c_15522]) ).
tcf(c_15539,plain,
( gt(wr_level(plus(x_139,n1)),n1)
| ( wr_level(plus(x_139,n1)) = n1 ) ),
inference(superposition,[status(thm)],[c_13259,c_15522]) ).
tcf(c_15549,plain,
( gt(fifo_length,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),n1)
| ( n1 = fifo_length ) ),
inference(superposition,[status(thm)],[c_15529,c_15298]) ).
tcf(c_15552,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ( n1 = fifo_length )
| ~ gt(n1,X0) ),
inference(superposition,[status(thm)],[c_15529,c_154]) ).
tcf(c_15569,plain,
gt(fifo_length,minus(fifo_length,n1)),
inference(global_subsumption_just,[status(thm)],[c_15549,c_233,c_10197]) ).
tcf(c_15574,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ~ gt(minus(fifo_length,n1),X0) ),
inference(superposition,[status(thm)],[c_15569,c_154]) ).
tcf(c_15702,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,minus(fifo_length,n1))
| ( minus(fifo_length,n1) = X0 ) ),
inference(superposition,[status(thm)],[c_153,c_15574]) ).
tcf(c_15723,plain,
! [X0: $i,X1: $i] :
( gt(X0,n0)
| gt(X1,X0)
| gt(wr_level(plus(x_139,n1)),X1)
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_153,c_15424]) ).
tcf(c_16085,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,minus(fifo_length,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_15702,c_233,c_10197,c_10232,c_10311,c_11738,c_11739]) ).
tcf(c_16412,plain,
! [X0: $i,X1: $i] :
( ( X1 = plus(n0,n1) )
| ( X1 != X0 )
| ( plus(n0,n1) != X0 ) ),
inference(instantiation,[status(thm)],[c_10700]) ).
tcf(c_16524,plain,
! [X0: $i] :
( ~ gt(X0,n0)
| ~ def_10(n1,plus(X0,n1)) ),
inference(superposition,[status(thm)],[c_10414,c_147]) ).
tcf(c_16589,plain,
! [X0: $i] :
( ( plus(n0,n1) = X0 )
| ~ def_10(n1,X0)
| ~ gt(X0,n0) ),
inference(superposition,[status(thm)],[c_160,c_15489]) ).
tcf(c_16628,plain,
! [X0: $i,X1: $i] :
( gt(X0,wr_level(plus(x_139,n1)))
| ~ gt(X1,n0)
| ( X0 != X1 )
| ( wr_level(plus(x_139,n1)) != n0 ) ),
inference(instantiation,[status(thm)],[c_10391]) ).
tcf(c_16629,plain,
( gt(n1,wr_level(plus(x_139,n1)))
| ~ gt(n1,n0)
| ( n1 != n1 )
| ( wr_level(plus(x_139,n1)) != n0 ) ),
inference(instantiation,[status(thm)],[c_16628]) ).
tcf(c_16960,plain,
! [X0: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),plus(X0,n1))
| ~ gt(wr_level(plus(x_139,n1)),X0) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_16963,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| ~ gt(X1,wr_level(plus(x_139,n1)))
| ~ gt(wr_level(plus(x_139,n1)),X0) ),
inference(instantiation,[status(thm)],[c_154]) ).
tcf(c_16964,plain,
( gt(n1,n1)
| ~ gt(n1,wr_level(plus(x_139,n1)))
| ~ gt(wr_level(plus(x_139,n1)),n1) ),
inference(instantiation,[status(thm)],[c_16963]) ).
tcf(c_17131,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,n0)
| gt(wr_level(plus(x_139,n1)),n1)
| ( n1 = fifo_length )
| ( X0 = n1 ) ),
inference(superposition,[status(thm)],[c_15723,c_15552]) ).
tcf(c_17828,plain,
! [X0: $i] :
( gt(n0,n0)
| ~ gt(X0,n0)
| ( n0 != n0 )
| ( n0 != X0 ) ),
inference(instantiation,[status(thm)],[c_13166]) ).
tcf(c_18228,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,n0) ),
inference(global_subsumption_just,[status(thm)],[c_17131,c_233,c_10214,c_10311,c_10389,c_10390,c_10546]) ).
tcf(c_18622,plain,
( ( plus(wr_level(plus(x_139,n1)),n1) = fifo_length )
| ( fifo_length != plus(wr_level(plus(x_139,n1)),n1) )
| ( plus(wr_level(plus(x_139,n1)),n1) != plus(wr_level(plus(x_139,n1)),n1) ) ),
inference(instantiation,[status(thm)],[c_12361]) ).
tcf(c_19131,plain,
! [X0: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),plus(X0,n1))
| gt(plus(plus(wr_level(plus(x_139,n1)),n1),n1),minus(fifo_length,n1))
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_10455,c_15436]) ).
tcf(c_19451,plain,
( gt(wr_level(plus(x_139,n1)),fifo_length)
| ( fifo_length = wr_level(plus(x_139,n1)) ) ),
inference(resolution,[status(thm)],[c_12413,c_11194]) ).
tcf(c_20039,plain,
! [X0: $i,X1: $i] :
( gt(X1,n0)
| gt(X0,n0)
| ( X0 = X1 ) ),
inference(resolution,[status(thm)],[c_12399,c_156]) ).
tcf(c_20139,plain,
! [X0: $i,X1: $i] :
( gt(X0,fifo_length)
| gt(wr_level(plus(x_139,n1)),fifo_length)
| ~ gt(X1,wr_level(plus(x_139,n1)))
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_19451,c_9169]) ).
tcf(c_20140,plain,
( gt(n1,fifo_length)
| gt(wr_level(plus(x_139,n1)),fifo_length)
| ~ gt(n1,wr_level(plus(x_139,n1)))
| ( n1 != n1 ) ),
inference(instantiation,[status(thm)],[c_20139]) ).
tcf(c_20309,plain,
! [X0: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),plus(X0,n1))
| ~ gt(fifo_length,X0) ),
inference(global_subsumption_just,[status(thm)],[c_19131,c_14594,c_16960]) ).
tcf(c_20325,plain,
! [X0: $i,X1: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(fifo_length,X0)
| ~ gt(plus(X0,n1),X1) ),
inference(superposition,[status(thm)],[c_20309,c_154]) ).
tcf(c_20658,plain,
! [X0: $i] :
( ( minus(plus(X0,n1),n1) = X0 )
| ~ gt(X0,n0) ),
inference(superposition,[status(thm)],[c_146,c_16524]) ).
tcf(c_20796,plain,
! [X0: $i] : minus(plus(plus(X0,n1),n1),n1) = plus(X0,n1),
inference(superposition,[status(thm)],[c_143,c_20658]) ).
tcf(c_21354,plain,
! [X0: $i] : ~ gt(n1,plus(X0,n1)),
inference(backward_subsumption_resolution,[status(thm)],[c_10436,c_14309]) ).
tcf(c_21359,plain,
minus(plus(n1,n1),n1) = n1,
inference(superposition,[status(thm)],[c_160,c_20796]) ).
tcf(c_21445,plain,
! [X0: $i] :
( gt(plus(X0,n1),n1)
| ( plus(X0,n1) = n1 ) ),
inference(superposition,[status(thm)],[c_153,c_21354]) ).
tcf(c_21539,plain,
! [X0: $i,X1: $i] :
( gt(plus(X1,n1),X0)
| ( plus(X1,n1) = n1 )
| ~ gt(n1,X0) ),
inference(superposition,[status(thm)],[c_21445,c_154]) ).
tcf(c_21540,plain,
! [X0: $i,X1: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(fifo_length,X0)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_10455,c_154]) ).
tcf(c_21587,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ( X0 = X1 )
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_153,c_21540]) ).
tcf(c_21717,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ( X0 = n0 ) ),
inference(superposition,[status(thm)],[c_233,c_21587]) ).
tcf(c_21728,plain,
! [X0: $i] :
( gt(X0,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X0) ),
inference(global_subsumption_just,[status(thm)],[c_21717,c_12210]) ).
tcf(c_21733,plain,
! [X0: $i,X1: $i] :
( gt(X0,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_21728,c_154]) ).
tcf(c_21797,plain,
( gt(wr_level(plus(x_139,n1)),fifo_length)
| ( wr_level(plus(x_139,n1)) = fifo_length ) ),
inference(superposition,[status(thm)],[c_232,c_152]) ).
tcf(c_21875,plain,
! [X0: $i,X1: $i] :
( gt(X0,n0)
| gt(X1,X0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_153,c_21733]) ).
tcf(c_22007,plain,
( ( plus(wr_level(x_139),n1) = n1 )
| ~ gt(n1,fifo_length) ),
inference(superposition,[status(thm)],[c_21539,c_231]) ).
tcf(c_22017,plain,
~ gt(n1,fifo_length),
inference(global_subsumption_just,[status(thm)],[c_22007,c_233,c_234,c_161,c_251,c_10203,c_10258,c_10260,c_10265,c_11544,c_13563,c_13581]) ).
tcf(c_22019,plain,
( gt(fifo_length,n1)
| ( n1 = fifo_length ) ),
inference(superposition,[status(thm)],[c_153,c_22017]) ).
tcf(c_22026,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ( n1 = fifo_length )
| ~ gt(n1,X0) ),
inference(superposition,[status(thm)],[c_22019,c_154]) ).
tcf(c_22166,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ~ gt(n1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_22026,c_10389,c_10390,c_13129,c_14312,c_17828,c_18228]) ).
tcf(c_22443,plain,
! [X0: $i,X1: $i] :
( gt(X0,n0)
| gt(X1,X0)
| ( X0 = X1 ) ),
inference(global_subsumption_just,[status(thm)],[c_21875,c_153,c_10388,c_20039]) ).
tcf(c_22459,plain,
! [X0: $i,X1: $i] :
( gt(X1,n0)
| gt(X0,fifo_length)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ( X1 = n0 )
| ( X0 = fifo_length ) ),
inference(superposition,[status(thm)],[c_22443,c_21587]) ).
tcf(c_22472,plain,
! [X0: $i,X1: $i] :
( gt(X1,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ( X0 = X1 )
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_22443,c_21540]) ).
tcf(c_22703,plain,
! [X0: $i,X1: $i] :
( gt(X1,n0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(fifo_length,X0) ),
inference(global_subsumption_just,[status(thm)],[c_22472,c_233,c_143,c_10214,c_10389,c_10390,c_10546,c_10697,c_10698,c_11216,c_11550,c_13129,c_17828,c_20325,c_22459]) ).
tcf(c_23284,plain,
( gt(plus(n1,n1),n1)
| ~ gt(plus(n1,n1),n0) ),
inference(superposition,[status(thm)],[c_21359,c_144]) ).
tcf(c_23285,plain,
gt(plus(n1,n1),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_23284,c_143]) ).
tcf(c_23294,plain,
! [X0: $i] :
( gt(plus(n1,n1),X0)
| ~ gt(n1,X0) ),
inference(superposition,[status(thm)],[c_23285,c_154]) ).
tcf(c_24741,plain,
( p_Rd(x_139)
| p_Reset(x_139)
| gt(fifo_length,int_level(x_139))
| ( wr_level(plus(x_139,n1)) = wr_level(x_139) ) ),
inference(instantiation,[status(thm)],[c_371]) ).
tcf(c_24742,plain,
( p_Wr(x_139)
| p_Reset(x_139)
| ( wr_level(plus(x_139,n1)) = wr_level(x_139) ) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_24794,plain,
! [X0: $i,X1: $i] :
( gt(plus(n1,n1),X1)
| ~ gt(n1,X0)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_23294,c_154]) ).
tcf(c_25038,plain,
! [X0: $i] :
( ( X0 = plus(minus(fifo_length,n1),n1) )
| ( X0 != fifo_length )
| ( plus(minus(fifo_length,n1),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_13572]) ).
tcf(c_25108,plain,
! [X0: $i] :
( ( X0 = plus(fifo_length,n1) )
| ( X0 != wr_level(plus(x_139,n1)) )
| ( plus(fifo_length,n1) != wr_level(plus(x_139,n1)) ) ),
inference(instantiation,[status(thm)],[c_13580]) ).
tcf(c_25109,plain,
( ( n1 = plus(fifo_length,n1) )
| ( n1 != wr_level(plus(x_139,n1)) )
| ( plus(fifo_length,n1) != wr_level(plus(x_139,n1)) ) ),
inference(instantiation,[status(thm)],[c_25108]) ).
tcf(c_25612,plain,
! [X0: $i] :
( ( fifo_length = X0 )
| ( fifo_length != fifo_length )
| ( X0 != fifo_length ) ),
inference(instantiation,[status(thm)],[c_13827]) ).
tcf(c_25932,plain,
( gt(plus(n1,n1),fifo_length)
| ( wr_level(plus(x_139,n1)) = fifo_length )
| ~ gt(n1,wr_level(plus(x_139,n1))) ),
inference(superposition,[status(thm)],[c_21797,c_24794]) ).
tcf(c_26274,plain,
( ( fifo_length = plus(wr_level(plus(x_139,n1)),n1) )
| ( fifo_length != plus(minus(fifo_length,n1),n1) )
| ( plus(wr_level(plus(x_139,n1)),n1) != plus(minus(fifo_length,n1),n1) ) ),
inference(instantiation,[status(thm)],[c_12356]) ).
tcf(c_26276,plain,
~ gt(n1,wr_level(plus(x_139,n1))),
inference(global_subsumption_just,[status(thm)],[c_25932,c_233,c_234,c_161,c_251,c_10203,c_10258,c_10260,c_10265,c_11544,c_12445,c_12451,c_13563,c_13581,c_14115,c_15539,c_16964,c_20140,c_25109]) ).
tcf(c_28498,plain,
! [X0: $i,X1: $i] :
( gt(plus(X0,n1),X1)
| ~ gt(plus(X0,n1),plus(n0,n1))
| ( X1 != plus(n0,n1) )
| ( plus(X0,n1) != plus(X0,n1) ) ),
inference(instantiation,[status(thm)],[c_11519]) ).
tcf(c_29727,plain,
! [X0: $i,X1: $i] :
( gt(plus(X0,n1),X1)
| ~ gt(plus(X0,n1),plus(minus(X0,n1),n1))
| ( X1 != plus(minus(X0,n1),n1) )
| ( plus(X0,n1) != plus(X0,n1) ) ),
inference(instantiation,[status(thm)],[c_13071]) ).
tcf(c_31567,plain,
( gt(fifo_length,plus(wr_level(plus(x_139,n1)),n1))
| ( fifo_length = plus(wr_level(plus(x_139,n1)),n1) )
| ~ gt(plus(fifo_length,n1),plus(wr_level(plus(x_139,n1)),n1)) ),
inference(instantiation,[status(thm)],[c_10477]) ).
tcf(c_33124,plain,
( ( fifo_length = plus(minus(fifo_length,n1),n1) )
| ( fifo_length != fifo_length )
| ( plus(minus(fifo_length,n1),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_25038]) ).
tcf(c_35858,plain,
! [X0: $i] :
( gt(plus(fifo_length,n1),X0)
| ~ gt(plus(minus(fifo_length,n1),n1),X0)
| ~ gt(plus(fifo_length,n1),plus(minus(fifo_length,n1),n1)) ),
inference(instantiation,[status(thm)],[c_13329]) ).
tcf(c_37478,plain,
! [X0: $i,X1: $i] :
( gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(fifo_length,X0)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_10455,c_154]) ).
tcf(c_37551,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ( X0 = X1 )
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_153,c_37478]) ).
tcf(c_37798,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(fifo_length,X0) ),
inference(global_subsumption_just,[status(thm)],[c_37551,c_144,c_153,c_10386,c_10389,c_10390,c_10445,c_10698,c_11216,c_12413,c_13166,c_13564,c_13565,c_16412,c_16589,c_20325,c_22703,c_28498,c_29727]) ).
tcf(c_37805,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0)
| ~ gt(fifo_length,n0) ),
inference(superposition,[status(thm)],[c_144,c_37798]) ).
tcf(c_37813,plain,
! [X0: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_37805,c_233]) ).
tcf(c_37827,plain,
! [X0: $i,X1: $i] :
( gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_37813,c_154]) ).
tcf(c_37857,plain,
! [X0: $i] :
( gt(X0,n1)
| ( plus(n0,n1) = X0 )
| ~ gt(X0,n0) ),
inference(superposition,[status(thm)],[c_160,c_155]) ).
tcf(c_37970,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X1)
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_153,c_37827]) ).
tcf(c_38134,plain,
! [X0: $i] :
( gt(X0,n1)
| ( X0 = n1 )
| ~ gt(X0,n0) ),
inference(demodulation,[status(thm)],[c_37857,c_160]) ).
tcf(c_38141,plain,
( gt(fifo_length,n1)
| ( n1 = fifo_length ) ),
inference(superposition,[status(thm)],[c_233,c_38134]) ).
tcf(c_38179,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ( n1 = fifo_length )
| ~ gt(n1,X0) ),
inference(superposition,[status(thm)],[c_38141,c_154]) ).
tcf(c_38180,plain,
( ( n1 = fifo_length )
| ~ def_10(n1,fifo_length) ),
inference(superposition,[status(thm)],[c_38141,c_147]) ).
tcf(c_38183,plain,
~ def_10(n1,fifo_length),
inference(global_subsumption_just,[status(thm)],[c_38180,c_235,c_11479,c_14350]) ).
tcf(c_38185,plain,
plus(minus(fifo_length,n1),n1) = fifo_length,
inference(superposition,[status(thm)],[c_145,c_38183]) ).
tcf(c_38186,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ~ gt(n1,X0) ),
inference(global_subsumption_just,[status(thm)],[c_38179,c_22166]) ).
tcf(c_38242,plain,
! [X0: $i] :
( gt(plus(X0,n1),fifo_length)
| ~ gt(X0,minus(fifo_length,n1)) ),
inference(superposition,[status(thm)],[c_38185,c_149]) ).
tcf(c_38803,plain,
! [X0: $i,X1: $i] :
( gt(X1,X0)
| gt(X0,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X1) ),
inference(global_subsumption_just,[status(thm)],[c_37970,c_16085,c_37798]) ).
tcf(c_38804,plain,
! [X0: $i,X1: $i] :
( gt(X0,X1)
| gt(X1,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0) ),
inference(renaming,[status(thm)],[c_38803]) ).
tcf(c_38859,plain,
! [X0: $i] :
( gt(X0,n1)
| gt(fifo_length,minus(fifo_length,n1))
| gt(plus(wr_level(plus(x_139,n1)),n1),X0) ),
inference(superposition,[status(thm)],[c_38804,c_38186]) ).
tcf(c_38886,plain,
gt(fifo_length,minus(fifo_length,n1)),
inference(global_subsumption_just,[status(thm)],[c_38859,c_233,c_10197]) ).
tcf(c_38896,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| ~ gt(minus(fifo_length,n1),X0) ),
inference(superposition,[status(thm)],[c_38886,c_154]) ).
tcf(c_39132,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,minus(fifo_length,n1))
| ( minus(fifo_length,n1) = X0 ) ),
inference(superposition,[status(thm)],[c_153,c_38896]) ).
tcf(c_40535,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,minus(fifo_length,n1)) ),
inference(global_subsumption_just,[status(thm)],[c_39132,c_16085]) ).
tcf(c_41117,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(plus(X0,n1),fifo_length) ),
inference(superposition,[status(thm)],[c_40535,c_38242]) ).
tcf(c_41282,plain,
gt(fifo_length,wr_level(x_139)),
inference(superposition,[status(thm)],[c_41117,c_231]) ).
tcf(c_49380,plain,
( gt(plus(fifo_length,n1),plus(wr_level(plus(x_139,n1)),n1))
| ~ gt(plus(fifo_length,n1),plus(minus(fifo_length,n1),n1))
| ~ gt(plus(minus(fifo_length,n1),n1),plus(wr_level(plus(x_139,n1)),n1)) ),
inference(instantiation,[status(thm)],[c_35858]) ).
tcf(c_50768,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X2,X1)
| gt(X1,X2)
| gt(X0,X2)
| ~ gt(X0,X1) ),
inference(resolution,[status(thm)],[c_14070,c_9164]) ).
tcf(c_61866,plain,
( ( fifo_length = plus(wr_level(x_139),n1) )
| ( fifo_length != fifo_length )
| ( plus(wr_level(x_139),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_25612]) ).
tcf(c_61867,plain,
( ( plus(wr_level(x_139),n1) = plus(minus(fifo_length,n1),n1) )
| ( plus(wr_level(x_139),n1) != fifo_length )
| ( plus(minus(fifo_length,n1),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_25038]) ).
tcf(c_61880,plain,
! [X0: $i] :
( ( plus(wr_level(x_139),n1) = X0 )
| ( X0 != fifo_length )
| ( plus(wr_level(x_139),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_13568]) ).
tcf(c_61882,plain,
( ( plus(wr_level(x_139),n1) = n1 )
| ( n1 != fifo_length )
| ( plus(wr_level(x_139),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_61880]) ).
tcf(c_69097,plain,
! [X0: $i] : ~ gt(n1,plus(X0,n1)),
inference(backward_subsumption_resolution,[status(thm)],[c_10436,c_14309]) ).
tcf(c_69163,plain,
! [X0: $i] :
( gt(plus(plus(X0,n1),n1),plus(X0,n1))
| ~ gt(plus(plus(X0,n1),n1),n0) ),
inference(superposition,[status(thm)],[c_20796,c_144]) ).
tcf(c_69164,plain,
! [X0: $i] : gt(plus(plus(X0,n1),n1),plus(X0,n1)),
inference(forward_subsumption_resolution,[status(thm)],[c_69163,c_143]) ).
tcf(c_69195,plain,
( gt(fifo_length,plus(wr_level(x_139),n1))
| ( plus(wr_level(x_139),n1) = fifo_length ) ),
inference(superposition,[status(thm)],[c_153,c_231]) ).
tcf(c_69201,plain,
! [X0: $i] :
( gt(fifo_length,X0)
| gt(X0,plus(wr_level(x_139),n1))
| ( plus(wr_level(x_139),n1) = fifo_length )
| ( plus(wr_level(x_139),n1) = X0 ) ),
inference(superposition,[status(thm)],[c_153,c_10464]) ).
tcf(c_69230,plain,
( gt(fifo_length,n1)
| ( plus(wr_level(x_139),n1) = fifo_length )
| ( plus(wr_level(x_139),n1) = n1 ) ),
inference(superposition,[status(thm)],[c_69201,c_69097]) ).
tcf(c_69233,plain,
( gt(fifo_length,n1)
| ( plus(wr_level(x_139),n1) = n1 ) ),
inference(global_subsumption_just,[status(thm)],[c_69230,c_14342,c_14394,c_61882]) ).
tcf(c_69237,plain,
( ( plus(wr_level(x_139),n1) = n1 )
| ~ def_10(n1,fifo_length) ),
inference(superposition,[status(thm)],[c_69233,c_147]) ).
tcf(c_69248,plain,
~ def_10(n1,fifo_length),
inference(global_subsumption_just,[status(thm)],[c_69237,c_235,c_11479,c_14350]) ).
tcf(c_69261,plain,
plus(minus(fifo_length,n1),n1) = fifo_length,
inference(superposition,[status(thm)],[c_145,c_69248]) ).
tcf(c_70679,plain,
minus(plus(fifo_length,n1),n1) = fifo_length,
inference(superposition,[status(thm)],[c_69261,c_20796]) ).
tcf(c_70736,plain,
( gt(plus(fifo_length,n1),fifo_length)
| ~ gt(plus(fifo_length,n1),n0) ),
inference(superposition,[status(thm)],[c_70679,c_144]) ).
tcf(c_70737,plain,
gt(plus(fifo_length,n1),fifo_length),
inference(forward_subsumption_resolution,[status(thm)],[c_70736,c_143]) ).
tcf(c_70950,plain,
! [X0: $i] :
( gt(plus(fifo_length,n1),X0)
| ~ gt(fifo_length,X0) ),
inference(superposition,[status(thm)],[c_70737,c_154]) ).
tcf(c_70973,plain,
! [X0: $i] :
( gt(X0,n1)
| ( X0 = n1 )
| ~ gt(X0,n0) ),
inference(superposition,[status(thm)],[c_10414,c_152]) ).
tcf(c_71378,plain,
! [X0: $i] : gt(plus(X0,n1),X0),
inference(superposition,[status(thm)],[c_69164,c_150]) ).
tcf(c_71394,plain,
! [X0: $i,X1: $i] :
( gt(plus(X0,n1),X1)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_71378,c_154]) ).
tcf(c_72089,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(plus(X0,n1),X2)
| ~ gt(X1,X2)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_71394,c_154]) ).
tcf(c_75299,plain,
( gt(plus(fifo_length,n1),n1)
| ( plus(fifo_length,n1) = n1 )
| ~ gt(fifo_length,n0) ),
inference(superposition,[status(thm)],[c_70950,c_70973]) ).
tcf(c_75327,plain,
( gt(plus(fifo_length,n1),n1)
| ( plus(fifo_length,n1) = n1 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_75299,c_233]) ).
tcf(c_75404,plain,
gt(plus(fifo_length,n1),n1),
inference(global_subsumption_just,[status(thm)],[c_75327,c_233,c_234,c_161,c_251,c_10203,c_13563,c_14882,c_14881]) ).
tcf(c_101939,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X2,X1)
| gt(X0,X2)
| ~ gt(X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_10462,c_154,c_50768]) ).
tcf(c_102120,plain,
! [X0: $i] :
( gt(X0,n1)
| gt(plus(fifo_length,n1),X0) ),
inference(superposition,[status(thm)],[c_75404,c_101939]) ).
tcf(c_104958,plain,
! [X0: $i,X1: $i] :
( gt(X0,n1)
| gt(plus(plus(fifo_length,n1),n1),X1)
| ~ gt(X0,X1) ),
inference(superposition,[status(thm)],[c_102120,c_72089]) ).
tcf(c_110735,plain,
( p_Reset(x_139)
| ( wr_level(plus(x_139,n1)) = plus(wr_level(x_139),n1) )
| ~ p_Rd(x_139)
| ~ p_Wr(x_139)
| ~ gt(minus(fifo_length,n1),wr_level(x_139)) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_110739,plain,
( gt(minus(fifo_length,n1),wr_level(x_139))
| ( wr_level(plus(x_139,n1)) = n0 )
| ~ p_Rd(x_139)
| ~ p_Wr(x_139) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_111484,plain,
( p_Reset(x_139)
| ( wr_level(plus(x_139,n1)) = plus(wr_level(x_139),n1) )
| ~ p_Wr(x_139)
| ~ gt(fifo_length,int_level(x_139))
| ~ gt(minus(fifo_length,n1),wr_level(x_139)) ),
inference(instantiation,[status(thm)],[c_430]) ).
tcf(c_111487,plain,
( gt(minus(fifo_length,n1),wr_level(x_139))
| ( wr_level(plus(x_139,n1)) = n0 )
| ~ p_Wr(x_139)
| ~ gt(fifo_length,int_level(x_139)) ),
inference(instantiation,[status(thm)],[c_417]) ).
tcf(c_118909,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( gt(X0,X2)
| ~ gt(plus(X1,n1),X3)
| ( X2 != X3 )
| ( X0 != plus(X1,n1) ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_118910,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(X0,X1)
| ~ gt(fifo_length,X2)
| ( X1 != X2 )
| ( X0 != fifo_length ) ),
inference(instantiation,[status(thm)],[c_9169]) ).
tcf(c_119720,plain,
! [X0: $i,X1: $i] :
( gt(plus(minus(fifo_length,n1),n1),X0)
| ~ gt(fifo_length,X1)
| ( X0 != X1 )
| ( plus(minus(fifo_length,n1),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_118910]) ).
tcf(c_119790,plain,
! [X0: $i] :
( gt(plus(minus(fifo_length,n1),n1),plus(wr_level(X0),n1))
| ~ gt(minus(fifo_length,n1),wr_level(X0)) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_119870,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( gt(plus(X0,n1),X2)
| ~ gt(plus(X1,n1),X3)
| ( X2 != X3 )
| ( plus(X0,n1) != plus(X1,n1) ) ),
inference(instantiation,[status(thm)],[c_118909]) ).
tcf(c_121501,plain,
! [X0: $i] :
( gt(plus(minus(fifo_length,n1),n1),wr_level(plus(x_139,n1)))
| ~ gt(fifo_length,X0)
| ( wr_level(plus(x_139,n1)) != X0 )
| ( plus(minus(fifo_length,n1),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_119720]) ).
tcf(c_124944,plain,
! [X0: $i,X1: $i] :
( gt(plus(minus(fifo_length,X0),X0),plus(X1,n1))
| ( plus(X1,n1) = plus(minus(fifo_length,X0),X0) )
| ~ gt(plus(minus(fifo_length,X0),X0),X1) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_127315,plain,
( gt(plus(minus(fifo_length,n1),n1),wr_level(plus(x_139,n1)))
| ~ gt(fifo_length,plus(wr_level(x_139),n1))
| ( wr_level(plus(x_139,n1)) != plus(wr_level(x_139),n1) )
| ( plus(minus(fifo_length,n1),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_121501]) ).
tcf(c_127318,plain,
( gt(plus(minus(fifo_length,n1),n1),wr_level(plus(x_139,n1)))
| ~ gt(fifo_length,wr_level(x_139))
| ( wr_level(plus(x_139,n1)) != wr_level(x_139) )
| ( plus(minus(fifo_length,n1),n1) != fifo_length ) ),
inference(instantiation,[status(thm)],[c_121501]) ).
tcf(c_139751,plain,
( gt(plus(minus(fifo_length,n1),n1),plus(wr_level(plus(x_139,n1)),n1))
| ( plus(wr_level(plus(x_139,n1)),n1) = plus(minus(fifo_length,n1),n1) )
| ~ gt(plus(minus(fifo_length,n1),n1),wr_level(plus(x_139,n1))) ),
inference(instantiation,[status(thm)],[c_124944]) ).
tcf(c_147681,plain,
( ( wr_level(plus(x_139,n1)) = n0 )
| ~ p_Reset(x_139) ),
inference(instantiation,[status(thm)],[c_167]) ).
tcf(c_164329,plain,
( gt(fifo_length,n1)
| gt(plus(plus(fifo_length,n1),n1),plus(wr_level(x_139),n1))
| ( plus(wr_level(x_139),n1) = fifo_length ) ),
inference(superposition,[status(thm)],[c_69195,c_104958]) ).
tcf(c_165329,plain,
plus(wr_level(x_139),n1) = fifo_length,
inference(global_subsumption_just,[status(thm)],[c_164329,c_233,c_234,c_235,c_161,c_232,c_251,c_10197,c_10203,c_10231,c_10236,c_10258,c_10260,c_10265,c_10267,c_10268,c_10306,c_10323,c_10329,c_10496,c_11479,c_11544,c_11642,c_11643,c_12445,c_12451,c_13563,c_13581,c_14115,c_14350,c_15539,c_16629,c_16964,c_18622,c_20140,c_24742,c_24741,c_25109,c_26274,c_31567,c_33124,c_41282,c_49380,c_110739,c_110735,c_111487,c_111484,c_127315,c_127318,c_139751,c_147681]) ).
tcf(c_215937,plain,
! [X0: $i,X1: $i,X2: $i] :
( gt(minus(fifo_length,n1),wr_level(X2))
| gt(X0,wr_level(plus(X2,n1)))
| ~ p_Wr(X2)
| ~ gt(X1,n0)
| ~ gt(fifo_length,int_level(X2))
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_417,c_9169]) ).
tcf(c_244151,plain,
! [X0: $i,X1: $i] :
( gt(plus(wr_level(x_139),n1),fifo_length)
| ~ gt(plus(X0,n1),X1)
| ( fifo_length != X1 )
| ( plus(wr_level(x_139),n1) != plus(X0,n1) ) ),
inference(instantiation,[status(thm)],[c_119870]) ).
tcf(c_245161,plain,
! [X0: $i] :
( gt(wr_level(plus(x_139,n1)),fifo_length)
| gt(minus(fifo_length,n1),wr_level(X0))
| gt(wr_level(plus(x_139,n1)),wr_level(plus(X0,n1)))
| ~ p_Wr(X0)
| ~ gt(fifo_length,n0)
| ~ gt(fifo_length,int_level(X0)) ),
inference(resolution,[status(thm)],[c_215937,c_11194]) ).
tcf(c_247447,plain,
! [X0: $i] :
( gt(wr_level(plus(x_139,n1)),fifo_length)
| gt(minus(fifo_length,n1),wr_level(X0))
| gt(wr_level(plus(x_139,n1)),wr_level(plus(X0,n1)))
| ~ p_Wr(X0)
| ~ gt(fifo_length,int_level(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_245161,c_233,c_245161]) ).
tcf(c_247473,plain,
( gt(minus(fifo_length,n1),wr_level(x_139))
| gt(wr_level(plus(x_139,n1)),fifo_length)
| ~ p_Wr(x_139)
| ~ gt(fifo_length,int_level(x_139)) ),
inference(resolution,[status(thm)],[c_247447,c_158]) ).
tcf(c_247553,plain,
gt(minus(fifo_length,n1),wr_level(x_139)),
inference(global_subsumption_just,[status(thm)],[c_247473,c_233,c_234,c_232,c_251,c_10197,c_10231,c_10236,c_10267,c_10268,c_10323,c_10329,c_10496,c_11642,c_11643,c_15063,c_16629,c_18622,c_24742,c_24741,c_26274,c_26276,c_31567,c_33124,c_41282,c_49380,c_110739,c_111487,c_127318,c_139751,c_147681]) ).
tcf(c_258036,plain,
! [X0: $i] :
( gt(plus(wr_level(x_139),n1),fifo_length)
| ~ gt(plus(X0,n1),plus(wr_level(x_139),n1))
| ( fifo_length != plus(wr_level(x_139),n1) )
| ( plus(wr_level(x_139),n1) != plus(X0,n1) ) ),
inference(instantiation,[status(thm)],[c_244151]) ).
tcf(c_296230,plain,
( gt(plus(minus(fifo_length,n1),n1),plus(wr_level(x_139),n1))
| ~ gt(minus(fifo_length,n1),wr_level(x_139)) ),
inference(instantiation,[status(thm)],[c_119790]) ).
tcf(c_316220,plain,
( gt(plus(wr_level(x_139),n1),fifo_length)
| ~ gt(plus(minus(fifo_length,n1),n1),plus(wr_level(x_139),n1))
| ( fifo_length != plus(wr_level(x_139),n1) )
| ( plus(wr_level(x_139),n1) != plus(minus(fifo_length,n1),n1) ) ),
inference(instantiation,[status(thm)],[c_258036]) ).
tcf(c_316222,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_316220,c_296230,c_247553,c_165329,c_61866,c_61867,c_15063,c_10329,c_10323,c_231]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV031-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 16:28:38 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 92.83/22.45 % SZS status Started for theBenchmark.p
% 92.83/22.45 % SZS status Unsatisfiable for theBenchmark.p
% 92.83/22.45
% 92.83/22.45 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 92.83/22.45
% 92.83/22.45 % ------ iProver source info
% 92.83/22.45
% 92.83/22.45 % git: date: 2026-07-19 20:42:38 +0200
% 92.83/22.45 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 92.83/22.45 % git: non_committed_changes: false
% 92.83/22.45
% 92.83/22.45 % ------ Parsing...% successful
% 92.83/22.45
% 92.83/22.45
% 92.83/22.45 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 92.83/22.45
% 92.83/22.45 % ------ Preprocessing... sup_sim: 0 sf_s rm: 21 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe_e %
% 92.83/22.45
% 92.83/22.45 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 92.83/22.45
% 92.83/22.45 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 92.83/22.45 % ------ Proving...
% 92.83/22.45 % ------ Problem Properties
% 92.83/22.45
% 92.83/22.45 %
% 92.83/22.45 % clauses 52
% 92.83/22.45 % conjectures 3
% 92.83/22.45 % EPR 7
% 92.83/22.45 % Horn 22
% 92.83/22.45 % unary 8
% 92.83/22.45 % binary 14
% 92.83/22.45 % lits 152
% 92.83/22.45 % lits eq 32
% 92.83/22.45 % fd_pure 0
% 92.83/22.45 % fd_pseudo 0
% 92.83/22.45 % fd_cond 1
% 92.83/22.45 % fd_pseudo_cond 4
% 92.83/22.45 % AC symbols 0
% 92.83/22.45
% 92.83/22.45 % ------ Input Options Time Limit: Unbounded
% 92.83/22.45
% 92.83/22.45
% 92.83/22.45 % ------
% 92.83/22.45 % Current options:
% 92.83/22.45 % ------
% 92.83/22.45
% 92.83/22.45
% 92.83/22.45 %
% 92.83/22.45
% 92.83/22.45 % ------ Proving...
% 92.83/22.45 %
% 92.83/22.45
% 92.83/22.45 % SZS status Unsatisfiable for theBenchmark.p
% 92.83/22.45
% 92.83/22.45 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 92.83/22.46
% 92.83/22.46
%------------------------------------------------------------------------------