%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV125+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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 : Tue Sep 29 01:20:17 PM UTC 2026
% Result : Theorem 3.98s 0.92s
% Output : Refutation 3.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 103
% Syntax : Number of formulae : 526 ( 170 unt; 63 def)
% Number of atoms : 5166 ( 93 equ)
% Maximal formula atoms : 654 ( 9 avg)
% Number of connectives : 7126 (2486 ~;2469 |;1956 &)
% ( 66 <=>; 149 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 86 ( 84 usr; 82 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 16 con; 0-2 aty)
% Number of variables : 80 ( 4 sgn 80 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0] : ~ gt(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
fof(f4,axiom,
! [X0] : leq(X0,X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',reflexivity_leq) ).
fof(f5,axiom,
! [X0,X1,X2] :
( ( leq(X0,X1)
& leq(X1,X2) )
=> leq(X0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',transitivity_leq) ).
fof(f7,axiom,
! [X0,X1] :
( geq(X0,X1)
<=> leq(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_geq) ).
fof(f8,axiom,
! [X0,X1] :
( gt(X1,X0)
=> leq(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt1) ).
fof(f9,axiom,
! [X0,X1] :
( ( leq(X0,X1)
& X0 != X1 )
=> gt(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt2) ).
fof(f10,axiom,
! [X0,X1] :
( leq(X0,pred(X1))
<=> gt(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt_pred) ).
fof(f13,axiom,
! [X0,X1] :
( leq(X0,X1)
<=> gt(succ(X1),X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_succ_gt_equiv) ).
fof(f29,axiom,
! [X0] : plus(X0,n1) = succ(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_1_r) ).
fof(f30,axiom,
! [X0] : plus(n1,X0) = succ(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_1_l) ).
fof(f39,axiom,
! [X0] : minus(X0,n1) = pred(X0),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',pred_minus_1) ).
fof(f41,axiom,
! [X0] : succ(pred(X0)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_pred) ).
fof(f51,axiom,
true,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',ttrue) ).
fof(f53,conjecture,
( ( geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0) )
=> ! [X0] :
( ( geq(n7,n0)
& geq(minus(n1000,n1),n0) )
=> ! [X1] :
( ( true
=> true )
& ( true
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n0,minus(n1000,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv21)
& leq(pv5,n588)
& leq(pv21,minus(n6,n1)) )
=> ( leq(n0,n0)
& leq(n0,pv5)
& leq(n0,pv21)
& leq(pv5,n588)
& leq(pv21,n5)
& leq(pv21,minus(n6,n1)) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) )
=> ( ( pv31 != pv32
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) ) )
& ( pv31 = pv32
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) ) ) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
=> ( leq(n0,pv5)
& leq(pv5,n588) ) )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> true )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n2,n7)
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n5,n7)
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n2,n7)
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n5,n7)
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) ) ) ) ) )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> ( leq(n0,pv5)
& leq(pv5,n588) ) )
& ( ( leq(n0,pv23)
& leq(pv23,minus(n6,n1)) )
=> ( leq(n0,a_select2(sigma,pv23))
=> true ) )
& ( geq(minus(n6,n1),n0)
=> ( geq(minus(n6,n1),n0)
=> ( ( geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0) )
=> true ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thruster_array_0001) ).
fof(f54,negated_conjecture,
~ ( ( geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0) )
=> ! [X0] :
( ( geq(n7,n0)
& geq(minus(n1000,n1),n0) )
=> ! [X1] :
( ( true
=> true )
& ( true
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n0,minus(n1000,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv21)
& leq(pv5,n588)
& leq(pv21,minus(n6,n1)) )
=> ( leq(n0,n0)
& leq(n0,pv5)
& leq(n0,pv21)
& leq(pv5,n588)
& leq(pv21,n5)
& leq(pv21,minus(n6,n1)) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) )
=> ( ( pv31 != pv32
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) ) )
& ( pv31 = pv32
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) ) ) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
=> ( leq(n0,pv5)
& leq(pv5,n588) ) )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> true )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n2,n7)
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n5,n7)
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n2,n7)
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n5,n7)
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) ) ) ) ) )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> ( leq(n0,pv5)
& leq(pv5,n588) ) )
& ( ( leq(n0,pv23)
& leq(pv23,minus(n6,n1)) )
=> ( leq(n0,a_select2(sigma,pv23))
=> true ) )
& ( geq(minus(n6,n1),n0)
=> ( geq(minus(n6,n1),n0)
=> ( ( geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0) )
=> true ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f55,axiom,
gt(n1000,n588),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1000_588) ).
fof(f57,axiom,
gt(n5,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_4) ).
fof(f58,axiom,
gt(n6,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_4) ).
fof(f59,axiom,
gt(n7,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_7_4) ).
fof(f62,axiom,
gt(n6,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_5) ).
fof(f63,axiom,
gt(n7,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_7_5) ).
fof(f66,axiom,
gt(n7,n6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_7_6) ).
fof(f81,axiom,
gt(n4,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_0) ).
fof(f82,axiom,
gt(n5,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_0) ).
fof(f83,axiom,
gt(n6,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_0) ).
fof(f85,axiom,
gt(n1,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_0) ).
fof(f86,axiom,
gt(n2,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_0) ).
fof(f88,axiom,
gt(n3,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_0) ).
fof(f90,axiom,
gt(n4,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_1) ).
fof(f91,axiom,
gt(n5,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_1) ).
fof(f92,axiom,
gt(n6,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_1) ).
fof(f93,axiom,
gt(n7,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_7_1) ).
fof(f98,axiom,
gt(n4,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_2) ).
fof(f99,axiom,
gt(n5,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_2) ).
fof(f100,axiom,
gt(n6,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_2) ).
fof(f101,axiom,
gt(n7,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_7_2) ).
fof(f105,axiom,
gt(n4,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_3) ).
fof(f106,axiom,
gt(n5,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_3) ).
fof(f107,axiom,
gt(n6,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_6_3) ).
fof(f108,axiom,
gt(n7,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_7_3) ).
fof(f112,axiom,
! [X0] :
( ( leq(n0,X0)
& leq(X0,n6) )
=> ( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_6) ).
fof(f131,plain,
~ ( ( geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0) )
=> ( ( geq(n7,n0)
& geq(minus(n1000,n1),n0) )
=> ( ( true
=> true )
& ( true
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n0,minus(n1000,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv21)
& leq(pv5,n588)
& leq(pv21,minus(n6,n1)) )
=> ( leq(n0,n0)
& leq(n0,pv5)
& leq(n0,pv21)
& leq(pv5,n588)
& leq(pv21,n5)
& leq(pv21,minus(n6,n1)) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) )
=> ( ( pv31 != pv32
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) ) )
& ( pv31 = pv32
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) ) ) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
=> ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) ) )
& ( ( leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
=> ( leq(n0,pv5)
& leq(pv5,n588) ) )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> true )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n2,n7)
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n5,n7)
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n2,n7)
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n5,n7)
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n1,minus(n4,n1))
& leq(n2,minus(n4,n1))
& leq(n3,minus(n4,n1))
& leq(pv5,minus(n1000,n1))
& ( ~ gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) )
& ( gt(pv5,n0)
=> ( leq(n0,n0)
& leq(n0,n1)
& leq(n0,n2)
& leq(n0,n3)
& leq(n0,n4)
& leq(n0,n5)
& leq(n0,n6)
& leq(n0,n7)
& leq(n0,pv5)
& leq(n0,minus(n4,n1))
& leq(n0,minus(n6,n1))
& leq(n1,n7)
& leq(n1,minus(n4,n1))
& leq(n1,minus(n6,n1))
& leq(n2,n7)
& leq(n2,minus(n4,n1))
& leq(n2,minus(n6,n1))
& leq(n3,n7)
& leq(n3,minus(n4,n1))
& leq(n3,minus(n6,n1))
& leq(n4,n7)
& leq(n4,minus(n6,n1))
& leq(n5,n7)
& leq(n5,minus(n6,n1))
& leq(n6,n7)
& leq(n7,n7)
& leq(pv5,n588)
& leq(pv5,minus(n1000,n1)) ) ) ) ) ) ) ) ) ) )
& ( ( leq(n0,pv5)
& leq(pv5,n588) )
=> ( leq(n0,pv5)
& leq(pv5,n588) ) )
& ( ( leq(n0,pv23)
& leq(pv23,minus(n6,n1)) )
=> ( leq(n0,a_select2(sigma,pv23))
=> true ) )
& ( geq(minus(n6,n1),n0)
=> ( geq(minus(n6,n1),n0)
=> ( ( geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0) )
=> true ) ) ) ) ) ),
inference(rectify,[],[f54]) ).
fof(f132,plain,
! [X0,X1] :
( geq(X0,X1)
=> leq(X1,X0) ),
inference(unused_predicate_definition_removal,[],[f7]) ).
fof(f135,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(ennf_transformation,[],[f5]) ).
fof(f136,plain,
! [X0,X1,X2] :
( leq(X0,X2)
| ~ leq(X0,X1)
| ~ leq(X1,X2) ),
inference(flattening,[],[f135]) ).
fof(f137,plain,
! [X0,X1] :
( leq(X1,X0)
| ~ geq(X0,X1) ),
inference(ennf_transformation,[],[f132]) ).
fof(f138,plain,
! [X0,X1] :
( leq(X0,X1)
| ~ gt(X1,X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f139,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(ennf_transformation,[],[f9]) ).
fof(f140,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(flattening,[],[f139]) ).
fof(f174,plain,
( ( ( ~ true
& true )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7) )
& true )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,pv5)
| ~ leq(n0,pv21)
| ~ leq(pv5,n588)
| ~ leq(pv21,n5)
| ~ leq(pv21,minus(n6,n1)) )
& leq(n0,pv5)
& leq(n0,pv21)
& leq(pv5,n588)
& leq(pv21,minus(n6,n1)) )
| ( ( ( ( ~ leq(n0,pv5)
| ~ leq(n0,pv31)
| ~ leq(n0,pv32)
| ~ leq(pv5,n588)
| ~ leq(pv31,minus(n6,n1))
| ~ leq(pv32,minus(n6,n1)) )
& pv31 != pv32 )
| ( ( ~ leq(n0,pv5)
| ~ leq(n0,pv31)
| ~ leq(n0,pv32)
| ~ leq(pv5,n588)
| ~ leq(pv31,minus(n6,n1))
| ~ leq(pv32,minus(n6,n1)) )
& pv31 = pv32 ) )
& leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) )
| ( ( ~ leq(n0,pv5)
| ~ leq(n0,pv31)
| ~ leq(pv5,n588)
| ~ leq(pv31,minus(n6,n1)) )
& leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
| ( ( ~ leq(n0,pv5)
| ~ leq(pv5,n588) )
& leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
| ( ~ true
& leq(n0,pv5)
& leq(pv5,n588) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ( ( ( ( ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n2,n7)
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,minus(n1000,n1))
| ( ( ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,minus(n1000,n1))
| ( ( ( ( ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n2,n7)
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,minus(n1000,n1))
| ( ( ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& leq(n0,pv5)
& leq(pv5,n588) )
| ( ( ~ leq(n0,pv5)
| ~ leq(pv5,n588) )
& leq(n0,pv5)
& leq(pv5,n588) )
| ( ~ true
& leq(n0,a_select2(sigma,pv23))
& leq(n0,pv23)
& leq(pv23,minus(n6,n1)) )
| ( ~ true
& geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0)
& geq(minus(n6,n1),n0)
& geq(minus(n6,n1),n0) ) )
& geq(n7,n0)
& geq(minus(n1000,n1),n0)
& geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0) ),
inference(ennf_transformation,[],[f131]) ).
fof(f175,plain,
( ( ( ~ true
& true )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7) )
& true )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,pv5)
| ~ leq(n0,pv21)
| ~ leq(pv5,n588)
| ~ leq(pv21,n5)
| ~ leq(pv21,minus(n6,n1)) )
& leq(n0,pv5)
& leq(n0,pv21)
& leq(pv5,n588)
& leq(pv21,minus(n6,n1)) )
| ( ( ( ( ~ leq(n0,pv5)
| ~ leq(n0,pv31)
| ~ leq(n0,pv32)
| ~ leq(pv5,n588)
| ~ leq(pv31,minus(n6,n1))
| ~ leq(pv32,minus(n6,n1)) )
& pv31 != pv32 )
| ( ( ~ leq(n0,pv5)
| ~ leq(n0,pv31)
| ~ leq(n0,pv32)
| ~ leq(pv5,n588)
| ~ leq(pv31,minus(n6,n1))
| ~ leq(pv32,minus(n6,n1)) )
& pv31 = pv32 ) )
& leq(n0,pv5)
& leq(n0,pv31)
& leq(n0,pv32)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1))
& leq(pv32,minus(n6,n1)) )
| ( ( ~ leq(n0,pv5)
| ~ leq(n0,pv31)
| ~ leq(pv5,n588)
| ~ leq(pv31,minus(n6,n1)) )
& leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
| ( ( ~ leq(n0,pv5)
| ~ leq(pv5,n588) )
& leq(n0,pv5)
& leq(n0,pv31)
& leq(pv5,n588)
& leq(pv31,minus(n6,n1)) )
| ( ~ true
& leq(n0,pv5)
& leq(pv5,n588) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ( ( ( ( ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n2,n7)
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,minus(n1000,n1))
| ( ( ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,minus(n1000,n1))
| ( ( ( ( ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n2,n7)
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n5,n7)
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,minus(n1000,n1))
| ( ( ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& ~ gt(pv5,n0) )
| ( ( ~ leq(n0,n0)
| ~ leq(n0,n1)
| ~ leq(n0,n2)
| ~ leq(n0,n3)
| ~ leq(n0,n4)
| ~ leq(n0,n5)
| ~ leq(n0,n6)
| ~ leq(n0,n7)
| ~ leq(n0,pv5)
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n6,n7)
| ~ leq(n7,n7)
| ~ leq(pv5,n588)
| ~ leq(pv5,minus(n1000,n1)) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& gt(pv5,n0) ) )
& leq(n0,pv5)
& leq(pv5,n588) )
| ( ( ~ leq(n0,pv5)
| ~ leq(pv5,n588) )
& leq(n0,pv5)
& leq(pv5,n588) )
| ( ~ true
& leq(n0,a_select2(sigma,pv23))
& leq(n0,pv23)
& leq(pv23,minus(n6,n1)) )
| ( ~ true
& geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0)
& geq(minus(n6,n1),n0)
& geq(minus(n6,n1),n0) ) )
& geq(n7,n0)
& geq(minus(n1000,n1),n0)
& geq(minus(n4,n1),n0)
& geq(minus(n1000,n1),n0) ),
inference(flattening,[],[f174]) ).
fof(f180,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6
| ~ leq(n0,X0)
| ~ leq(X0,n6) ),
inference(ennf_transformation,[],[f112]) ).
fof(f181,plain,
! [X0] :
( X0 = n0
| X0 = n1
| X0 = n2
| X0 = n3
| X0 = n4
| X0 = n5
| X0 = n6
| ~ leq(n0,X0)
| ~ leq(X0,n6) ),
inference(flattening,[],[f180]) ).
fof(f192,plain,
! [X0] : ~ gt(X0,X0),
inference(cnf_transformation,[],[f3]) ).
fof(f193,plain,
! [X0] : leq(X0,X0),
inference(cnf_transformation,[],[f4]) ).
fof(f194,plain,
! [X2,X0,X1] :
( ~ leq(X0,X1)
| ~ leq(X1,X2)
| leq(X0,X2) ),
inference(cnf_transformation,[],[f136]) ).
fof(f195,plain,
! [X0,X1] :
( ~ geq(X0,X1)
| leq(X1,X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f196,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,X1) ),
inference(cnf_transformation,[],[f138]) ).
fof(f197,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f140]) ).
fof(f198,plain,
! [X0,X1] :
( ~ gt(X1,X0)
| leq(X0,pred(X1)) ),
inference(cnf_transformation,[],[f10]) ).
fof(f199,plain,
! [X0,X1] :
( gt(X1,X0)
| ~ leq(X0,pred(X1)) ),
inference(cnf_transformation,[],[f10]) ).
fof(f203,plain,
! [X0,X1] :
( gt(succ(X1),X0)
| ~ leq(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f319,plain,
! [X0] : succ(X0) = plus(X0,n1),
inference(cnf_transformation,[],[f29]) ).
fof(f320,plain,
! [X0] : succ(X0) = plus(n1,X0),
inference(cnf_transformation,[],[f30]) ).
fof(f329,plain,
! [X0] : minus(X0,n1) = pred(X0),
inference(cnf_transformation,[],[f39]) ).
fof(f331,plain,
! [X0] : succ(pred(X0)) = X0,
inference(cnf_transformation,[],[f41]) ).
fof(f348,plain,
true,
inference(cnf_transformation,[],[f51]) ).
fof(f351,plain,
( ~ leq(n3,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP45 ),
inference(cnf_transformation,[],[f175]) ).
fof(f354,plain,
( ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP44 ),
inference(cnf_transformation,[],[f175]) ).
fof(f357,plain,
( ~ leq(n3,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP43 ),
inference(cnf_transformation,[],[f175]) ).
fof(f360,plain,
( ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP42 ),
inference(cnf_transformation,[],[f175]) ).
fof(f363,plain,
( ~ leq(n3,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP41 ),
inference(cnf_transformation,[],[f175]) ).
fof(f365,plain,
( ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP47 ),
inference(cnf_transformation,[],[f175]) ).
fof(f367,plain,
( ~ leq(n3,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP40 ),
inference(cnf_transformation,[],[f175]) ).
fof(f370,plain,
( ~ leq(pv5,n588)
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP46 ),
inference(cnf_transformation,[],[f175]) ).
fof(f376,plain,
( sP46
| sP40
| ~ leq(pv5,n588)
| sP47
| sP41
| ~ leq(n5,minus(n6,n1))
| ~ leq(n4,minus(n6,n1))
| sP42
| sP43
| ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,n7)
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,n7)
| ~ leq(n2,n7)
| ~ leq(n1,n7)
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| sP44
| sP45
| ~ leq(pv5,minus(n1000,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,pv5)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP32 ),
inference(cnf_transformation,[],[f175]) ).
fof(f405,plain,
( ~ leq(pv32,minus(n6,n1))
| ~ leq(pv31,minus(n6,n1))
| ~ leq(pv5,n588)
| ~ leq(n0,pv32)
| ~ leq(n0,pv31)
| ~ leq(n0,pv5)
| ~ sP36 ),
inference(cnf_transformation,[],[f175]) ).
fof(f407,plain,
( ~ leq(n7,n7)
| ~ leq(n6,n7)
| ~ leq(n5,minus(n6,n1))
| ~ leq(n5,n7)
| ~ leq(n4,minus(n6,n1))
| ~ leq(n4,n7)
| ~ leq(n3,minus(n6,n1))
| ~ leq(n3,minus(n4,n1))
| ~ leq(n3,n7)
| ~ leq(n2,minus(n6,n1))
| ~ leq(n2,minus(n4,n1))
| ~ leq(n2,n7)
| ~ leq(n1,minus(n6,n1))
| ~ leq(n1,minus(n4,n1))
| ~ leq(n1,n7)
| ~ leq(n0,minus(n1000,n1))
| ~ leq(n0,minus(n6,n1))
| ~ leq(n0,minus(n4,n1))
| ~ leq(n0,n7)
| ~ leq(n0,n6)
| ~ leq(n0,n5)
| ~ leq(n0,n4)
| ~ leq(n0,n3)
| ~ leq(n0,n2)
| ~ leq(n0,n1)
| ~ leq(n0,n0)
| ~ sP38 ),
inference(cnf_transformation,[],[f175]) ).
fof(f408,plain,
( ~ leq(pv21,minus(n6,n1))
| ~ leq(pv21,n5)
| ~ leq(pv5,n588)
| ~ leq(n0,pv21)
| ~ leq(n0,pv5)
| ~ leq(n0,n0)
| ~ sP37 ),
inference(cnf_transformation,[],[f175]) ).
fof(f409,plain,
( ~ leq(pv31,minus(n6,n1))
| ~ leq(pv5,n588)
| ~ leq(n0,pv31)
| ~ leq(n0,pv5)
| ~ sP35 ),
inference(cnf_transformation,[],[f175]) ).
fof(f410,plain,
( ~ leq(pv5,n588)
| ~ leq(n0,pv5)
| ~ sP34 ),
inference(cnf_transformation,[],[f175]) ).
fof(f411,plain,
( ~ leq(pv5,n588)
| ~ leq(n0,pv5)
| ~ sP31 ),
inference(cnf_transformation,[],[f175]) ).
fof(f413,plain,
( ~ true
| ~ sP39 ),
inference(cnf_transformation,[],[f175]) ).
fof(f415,plain,
( leq(pv21,minus(n6,n1))
| ~ sP37 ),
inference(cnf_transformation,[],[f175]) ).
fof(f416,plain,
( leq(pv5,n588)
| ~ sP37 ),
inference(cnf_transformation,[],[f175]) ).
fof(f417,plain,
( leq(n0,pv21)
| ~ sP37 ),
inference(cnf_transformation,[],[f175]) ).
fof(f418,plain,
( leq(n0,pv5)
| ~ sP37 ),
inference(cnf_transformation,[],[f175]) ).
fof(f419,plain,
( leq(pv32,minus(n6,n1))
| ~ sP36 ),
inference(cnf_transformation,[],[f175]) ).
fof(f420,plain,
( leq(pv31,minus(n6,n1))
| ~ sP36 ),
inference(cnf_transformation,[],[f175]) ).
fof(f421,plain,
( leq(pv5,n588)
| ~ sP36 ),
inference(cnf_transformation,[],[f175]) ).
fof(f422,plain,
( leq(n0,pv32)
| ~ sP36 ),
inference(cnf_transformation,[],[f175]) ).
fof(f423,plain,
( leq(n0,pv31)
| ~ sP36 ),
inference(cnf_transformation,[],[f175]) ).
fof(f424,plain,
( leq(n0,pv5)
| ~ sP36 ),
inference(cnf_transformation,[],[f175]) ).
fof(f425,plain,
( leq(pv31,minus(n6,n1))
| ~ sP35 ),
inference(cnf_transformation,[],[f175]) ).
fof(f426,plain,
( leq(pv5,n588)
| ~ sP35 ),
inference(cnf_transformation,[],[f175]) ).
fof(f427,plain,
( leq(n0,pv31)
| ~ sP35 ),
inference(cnf_transformation,[],[f175]) ).
fof(f428,plain,
( leq(n0,pv5)
| ~ sP35 ),
inference(cnf_transformation,[],[f175]) ).
fof(f430,plain,
( leq(pv5,n588)
| ~ sP34 ),
inference(cnf_transformation,[],[f175]) ).
fof(f432,plain,
( leq(n0,pv5)
| ~ sP34 ),
inference(cnf_transformation,[],[f175]) ).
fof(f435,plain,
( ~ true
| ~ sP33 ),
inference(cnf_transformation,[],[f175]) ).
fof(f436,plain,
( leq(pv5,n588)
| ~ sP32 ),
inference(cnf_transformation,[],[f175]) ).
fof(f437,plain,
( leq(n0,pv5)
| ~ sP32 ),
inference(cnf_transformation,[],[f175]) ).
fof(f438,plain,
( leq(pv5,n588)
| ~ sP31 ),
inference(cnf_transformation,[],[f175]) ).
fof(f439,plain,
( leq(n0,pv5)
| ~ sP31 ),
inference(cnf_transformation,[],[f175]) ).
fof(f443,plain,
( ~ true
| sP31
| sP32
| sP33
| sP34
| sP35
| sP36
| sP37
| sP38
| sP39 ),
inference(cnf_transformation,[],[f175]) ).
fof(f460,plain,
geq(minus(n1000,n1),n0),
inference(cnf_transformation,[],[f175]) ).
fof(f461,plain,
geq(minus(n4,n1),n0),
inference(cnf_transformation,[],[f175]) ).
fof(f463,plain,
geq(n7,n0),
inference(cnf_transformation,[],[f175]) ).
fof(f464,plain,
gt(n1000,n588),
inference(cnf_transformation,[],[f55]) ).
fof(f466,plain,
gt(n5,n4),
inference(cnf_transformation,[],[f57]) ).
fof(f467,plain,
gt(n6,n4),
inference(cnf_transformation,[],[f58]) ).
fof(f468,plain,
gt(n7,n4),
inference(cnf_transformation,[],[f59]) ).
fof(f471,plain,
gt(n6,n5),
inference(cnf_transformation,[],[f62]) ).
fof(f472,plain,
gt(n7,n5),
inference(cnf_transformation,[],[f63]) ).
fof(f475,plain,
gt(n7,n6),
inference(cnf_transformation,[],[f66]) ).
fof(f490,plain,
gt(n4,n0),
inference(cnf_transformation,[],[f81]) ).
fof(f491,plain,
gt(n5,n0),
inference(cnf_transformation,[],[f82]) ).
fof(f492,plain,
gt(n6,n0),
inference(cnf_transformation,[],[f83]) ).
fof(f494,plain,
gt(n1,n0),
inference(cnf_transformation,[],[f85]) ).
fof(f495,plain,
gt(n2,n0),
inference(cnf_transformation,[],[f86]) ).
fof(f497,plain,
gt(n3,n0),
inference(cnf_transformation,[],[f88]) ).
fof(f499,plain,
gt(n4,n1),
inference(cnf_transformation,[],[f90]) ).
fof(f500,plain,
gt(n5,n1),
inference(cnf_transformation,[],[f91]) ).
fof(f501,plain,
gt(n6,n1),
inference(cnf_transformation,[],[f92]) ).
fof(f502,plain,
gt(n7,n1),
inference(cnf_transformation,[],[f93]) ).
fof(f507,plain,
gt(n4,n2),
inference(cnf_transformation,[],[f98]) ).
fof(f508,plain,
gt(n5,n2),
inference(cnf_transformation,[],[f99]) ).
fof(f509,plain,
gt(n6,n2),
inference(cnf_transformation,[],[f100]) ).
fof(f510,plain,
gt(n7,n2),
inference(cnf_transformation,[],[f101]) ).
fof(f514,plain,
gt(n4,n3),
inference(cnf_transformation,[],[f105]) ).
fof(f515,plain,
gt(n5,n3),
inference(cnf_transformation,[],[f106]) ).
fof(f516,plain,
gt(n6,n3),
inference(cnf_transformation,[],[f107]) ).
fof(f517,plain,
gt(n7,n3),
inference(cnf_transformation,[],[f108]) ).
fof(f521,plain,
! [X0] :
( ~ leq(X0,n6)
| ~ leq(n0,X0)
| n6 = X0
| n5 = X0
| n4 = X0
| n3 = X0
| n2 = X0
| n1 = X0
| n0 = X0 ),
inference(cnf_transformation,[],[f181]) ).
fof(f532,plain,
! [X0,X1] :
( ~ leq(X0,minus(X1,n1))
| gt(X1,X0) ),
inference(definition_unfolding,[],[f199,f329]) ).
fof(f533,plain,
! [X0,X1] :
( leq(X0,minus(X1,n1))
| ~ gt(X1,X0) ),
inference(definition_unfolding,[],[f198,f329]) ).
fof(f536,plain,
! [X0,X1] :
( gt(plus(X1,n1),X0)
| ~ leq(X0,X1) ),
inference(definition_unfolding,[],[f203,f319]) ).
fof(f539,plain,
! [X0] : plus(X0,n1) = plus(n1,X0),
inference(definition_unfolding,[],[f320,f319]) ).
fof(f549,plain,
! [X0] : plus(minus(X0,n1),n1) = X0,
inference(definition_unfolding,[],[f331,f319,f329]) ).
fof(f563,definition,
( spl48_1
<=> sP45 ),
introduced(definition,[new_symbols(definition,[spl48_1])],[avatar_definition]) ).
fof(f567,definition,
( spl48_2
<=> leq(n0,n0) ),
introduced(definition,[new_symbols(definition,[spl48_2])],[avatar_definition]) ).
fof(f569,plain,
( ~ leq(n0,n0)
| spl48_2 ),
inference(avatar_component_clause,[],[f567]) ).
fof(f571,definition,
( spl48_3
<=> leq(n0,n1) ),
introduced(definition,[new_symbols(definition,[spl48_3])],[avatar_definition]) ).
fof(f573,plain,
( ~ leq(n0,n1)
| spl48_3 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl48_4
<=> leq(n0,n2) ),
introduced(definition,[new_symbols(definition,[spl48_4])],[avatar_definition]) ).
fof(f577,plain,
( ~ leq(n0,n2)
| spl48_4 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f579,definition,
( spl48_5
<=> leq(n0,n3) ),
introduced(definition,[new_symbols(definition,[spl48_5])],[avatar_definition]) ).
fof(f581,plain,
( ~ leq(n0,n3)
| spl48_5 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f583,definition,
( spl48_6
<=> leq(n0,n4) ),
introduced(definition,[new_symbols(definition,[spl48_6])],[avatar_definition]) ).
fof(f585,plain,
( ~ leq(n0,n4)
| spl48_6 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f587,definition,
( spl48_7
<=> leq(n0,n5) ),
introduced(definition,[new_symbols(definition,[spl48_7])],[avatar_definition]) ).
fof(f588,plain,
( leq(n0,n5)
| ~ spl48_7 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f589,plain,
( ~ leq(n0,n5)
| spl48_7 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f591,definition,
( spl48_8
<=> leq(n0,n6) ),
introduced(definition,[new_symbols(definition,[spl48_8])],[avatar_definition]) ).
fof(f593,plain,
( ~ leq(n0,n6)
| spl48_8 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f595,definition,
( spl48_9
<=> leq(n0,n7) ),
introduced(definition,[new_symbols(definition,[spl48_9])],[avatar_definition]) ).
fof(f597,plain,
( ~ leq(n0,n7)
| spl48_9 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f599,definition,
( spl48_10
<=> leq(n0,pv5) ),
introduced(definition,[new_symbols(definition,[spl48_10])],[avatar_definition]) ).
fof(f603,definition,
( spl48_11
<=> leq(n0,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_11])],[avatar_definition]) ).
fof(f605,plain,
( ~ leq(n0,minus(n6,n1))
| spl48_11 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f607,definition,
( spl48_12
<=> leq(n1,n7) ),
introduced(definition,[new_symbols(definition,[spl48_12])],[avatar_definition]) ).
fof(f609,plain,
( ~ leq(n1,n7)
| spl48_12 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f611,definition,
( spl48_13
<=> leq(n1,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_13])],[avatar_definition]) ).
fof(f613,plain,
( ~ leq(n1,minus(n6,n1))
| spl48_13 ),
inference(avatar_component_clause,[],[f611]) ).
fof(f615,definition,
( spl48_14
<=> leq(n2,n7) ),
introduced(definition,[new_symbols(definition,[spl48_14])],[avatar_definition]) ).
fof(f617,plain,
( ~ leq(n2,n7)
| spl48_14 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f619,definition,
( spl48_15
<=> leq(n2,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_15])],[avatar_definition]) ).
fof(f621,plain,
( ~ leq(n2,minus(n6,n1))
| spl48_15 ),
inference(avatar_component_clause,[],[f619]) ).
fof(f623,definition,
( spl48_16
<=> leq(n3,n7) ),
introduced(definition,[new_symbols(definition,[spl48_16])],[avatar_definition]) ).
fof(f625,plain,
( ~ leq(n3,n7)
| spl48_16 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f627,definition,
( spl48_17
<=> leq(n3,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_17])],[avatar_definition]) ).
fof(f629,plain,
( ~ leq(n3,minus(n6,n1))
| spl48_17 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f631,definition,
( spl48_18
<=> leq(n4,n7) ),
introduced(definition,[new_symbols(definition,[spl48_18])],[avatar_definition]) ).
fof(f633,plain,
( ~ leq(n4,n7)
| spl48_18 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f635,definition,
( spl48_19
<=> leq(n4,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_19])],[avatar_definition]) ).
fof(f637,plain,
( ~ leq(n4,minus(n6,n1))
| spl48_19 ),
inference(avatar_component_clause,[],[f635]) ).
fof(f639,definition,
( spl48_20
<=> leq(n5,n7) ),
introduced(definition,[new_symbols(definition,[spl48_20])],[avatar_definition]) ).
fof(f641,plain,
( ~ leq(n5,n7)
| spl48_20 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f643,definition,
( spl48_21
<=> leq(n5,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_21])],[avatar_definition]) ).
fof(f645,plain,
( ~ leq(n5,minus(n6,n1))
| spl48_21 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f647,definition,
( spl48_22
<=> leq(n6,n7) ),
introduced(definition,[new_symbols(definition,[spl48_22])],[avatar_definition]) ).
fof(f649,plain,
( ~ leq(n6,n7)
| spl48_22 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f651,definition,
( spl48_23
<=> leq(n7,n7) ),
introduced(definition,[new_symbols(definition,[spl48_23])],[avatar_definition]) ).
fof(f653,plain,
( ~ leq(n7,n7)
| spl48_23 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f655,definition,
( spl48_24
<=> leq(pv5,n588) ),
introduced(definition,[new_symbols(definition,[spl48_24])],[avatar_definition]) ).
fof(f656,plain,
( leq(pv5,n588)
| ~ spl48_24 ),
inference(avatar_component_clause,[],[f655]) ).
fof(f659,definition,
( spl48_25
<=> leq(pv5,minus(n1000,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_25])],[avatar_definition]) ).
fof(f661,plain,
( ~ leq(pv5,minus(n1000,n1))
| spl48_25 ),
inference(avatar_component_clause,[],[f659]) ).
fof(f668,definition,
( spl48_27
<=> leq(n0,minus(n4,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_27])],[avatar_definition]) ).
fof(f670,plain,
( ~ leq(n0,minus(n4,n1))
| spl48_27 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f672,definition,
( spl48_28
<=> leq(n1,minus(n4,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_28])],[avatar_definition]) ).
fof(f674,plain,
( ~ leq(n1,minus(n4,n1))
| spl48_28 ),
inference(avatar_component_clause,[],[f672]) ).
fof(f676,definition,
( spl48_29
<=> leq(n2,minus(n4,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_29])],[avatar_definition]) ).
fof(f678,plain,
( ~ leq(n2,minus(n4,n1))
| spl48_29 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f680,definition,
( spl48_30
<=> leq(n3,minus(n4,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_30])],[avatar_definition]) ).
fof(f682,plain,
( ~ leq(n3,minus(n4,n1))
| spl48_30 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f683,plain,
( ~ spl48_1
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30 ),
inference(avatar_split_clause,[],[f351,f680,f676,f672,f668,f659,f655,f651,f647,f643,f639,f635,f631,f627,f623,f619,f615,f611,f607,f603,f599,f595,f591,f587,f583,f579,f575,f571,f567,f563]) ).
fof(f686,definition,
( spl48_31
<=> sP44 ),
introduced(definition,[new_symbols(definition,[spl48_31])],[avatar_definition]) ).
fof(f690,plain,
( ~ spl48_31
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_10
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_25
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24 ),
inference(avatar_split_clause,[],[f354,f655,f651,f647,f643,f639,f635,f631,f627,f623,f619,f615,f611,f607,f603,f595,f591,f587,f583,f659,f680,f676,f672,f668,f599,f579,f575,f571,f567,f686]) ).
fof(f693,definition,
( spl48_32
<=> sP43 ),
introduced(definition,[new_symbols(definition,[spl48_32])],[avatar_definition]) ).
fof(f697,plain,
( ~ spl48_32
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30 ),
inference(avatar_split_clause,[],[f357,f680,f676,f672,f668,f659,f655,f651,f647,f643,f639,f635,f631,f627,f623,f619,f615,f611,f607,f603,f599,f595,f591,f587,f583,f579,f575,f571,f567,f693]) ).
fof(f700,definition,
( spl48_33
<=> sP42 ),
introduced(definition,[new_symbols(definition,[spl48_33])],[avatar_definition]) ).
fof(f704,plain,
( ~ spl48_33
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_10
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_25
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24 ),
inference(avatar_split_clause,[],[f360,f655,f651,f647,f643,f639,f635,f631,f627,f623,f619,f615,f611,f607,f603,f595,f591,f587,f583,f659,f680,f676,f672,f668,f599,f579,f575,f571,f567,f700]) ).
fof(f707,definition,
( spl48_34
<=> sP41 ),
introduced(definition,[new_symbols(definition,[spl48_34])],[avatar_definition]) ).
fof(f711,plain,
( ~ spl48_34
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30 ),
inference(avatar_split_clause,[],[f363,f680,f676,f672,f668,f659,f655,f651,f647,f643,f639,f635,f631,f627,f623,f619,f615,f611,f607,f603,f599,f595,f591,f587,f583,f579,f575,f571,f567,f707]) ).
fof(f714,definition,
( spl48_35
<=> sP47 ),
introduced(definition,[new_symbols(definition,[spl48_35])],[avatar_definition]) ).
fof(f717,plain,
( ~ spl48_35
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25 ),
inference(avatar_split_clause,[],[f365,f659,f655,f651,f647,f643,f639,f635,f631,f627,f623,f619,f615,f611,f607,f603,f599,f595,f591,f587,f583,f579,f575,f571,f567,f714]) ).
fof(f719,definition,
( spl48_36
<=> sP40 ),
introduced(definition,[new_symbols(definition,[spl48_36])],[avatar_definition]) ).
fof(f723,plain,
( ~ spl48_36
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30 ),
inference(avatar_split_clause,[],[f367,f680,f676,f672,f668,f659,f655,f651,f647,f643,f639,f635,f631,f627,f623,f619,f615,f611,f607,f603,f599,f595,f591,f587,f583,f579,f575,f571,f567,f719]) ).
fof(f726,definition,
( spl48_37
<=> sP46 ),
introduced(definition,[new_symbols(definition,[spl48_37])],[avatar_definition]) ).
fof(f730,plain,
( ~ spl48_37
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_10
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_25
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24 ),
inference(avatar_split_clause,[],[f370,f655,f651,f647,f643,f639,f635,f631,f627,f623,f619,f615,f611,f607,f603,f595,f591,f587,f583,f659,f680,f676,f672,f668,f599,f579,f575,f571,f567,f726]) ).
fof(f734,definition,
( spl48_38
<=> sP32 ),
introduced(definition,[new_symbols(definition,[spl48_38])],[avatar_definition]) ).
fof(f740,plain,
( ~ spl48_38
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_10
| ~ spl48_27
| ~ spl48_11
| ~ spl48_28
| ~ spl48_13
| ~ spl48_29
| ~ spl48_15
| ~ spl48_30
| ~ spl48_25
| spl48_1
| spl48_31
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_12
| ~ spl48_14
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_20
| ~ spl48_22
| ~ spl48_23
| spl48_32
| spl48_33
| ~ spl48_19
| ~ spl48_21
| spl48_34
| spl48_35
| ~ spl48_24
| spl48_36
| spl48_37 ),
inference(avatar_split_clause,[],[f376,f726,f719,f655,f714,f707,f643,f635,f700,f693,f651,f647,f639,f631,f627,f623,f615,f607,f595,f591,f587,f583,f686,f563,f659,f680,f619,f676,f611,f672,f603,f668,f599,f579,f575,f571,f567,f734]) ).
fof(f769,definition,
( spl48_39
<=> sP36 ),
introduced(definition,[new_symbols(definition,[spl48_39])],[avatar_definition]) ).
fof(f773,definition,
( spl48_40
<=> leq(n0,pv31) ),
introduced(definition,[new_symbols(definition,[spl48_40])],[avatar_definition]) ).
fof(f777,definition,
( spl48_41
<=> leq(n0,pv32) ),
introduced(definition,[new_symbols(definition,[spl48_41])],[avatar_definition]) ).
fof(f781,definition,
( spl48_42
<=> leq(pv31,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_42])],[avatar_definition]) ).
fof(f785,definition,
( spl48_43
<=> leq(pv32,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_43])],[avatar_definition]) ).
fof(f793,plain,
( ~ spl48_39
| ~ spl48_10
| ~ spl48_40
| ~ spl48_41
| ~ spl48_24
| ~ spl48_42
| ~ spl48_43 ),
inference(avatar_split_clause,[],[f405,f785,f781,f655,f777,f773,f599,f769]) ).
fof(f796,definition,
( spl48_45
<=> sP38 ),
introduced(definition,[new_symbols(definition,[spl48_45])],[avatar_definition]) ).
fof(f800,definition,
( spl48_46
<=> leq(n0,minus(n1000,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_46])],[avatar_definition]) ).
fof(f802,plain,
( ~ leq(n0,minus(n1000,n1))
| spl48_46 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f803,plain,
( ~ spl48_45
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_27
| ~ spl48_11
| ~ spl48_46
| ~ spl48_12
| ~ spl48_28
| ~ spl48_13
| ~ spl48_14
| ~ spl48_29
| ~ spl48_15
| ~ spl48_16
| ~ spl48_30
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23 ),
inference(avatar_split_clause,[],[f407,f651,f647,f643,f639,f635,f631,f627,f680,f623,f619,f676,f615,f611,f672,f607,f800,f603,f668,f595,f591,f587,f583,f579,f575,f571,f567,f796]) ).
fof(f805,definition,
( spl48_47
<=> sP37 ),
introduced(definition,[new_symbols(definition,[spl48_47])],[avatar_definition]) ).
fof(f809,definition,
( spl48_48
<=> leq(n0,pv21) ),
introduced(definition,[new_symbols(definition,[spl48_48])],[avatar_definition]) ).
fof(f810,plain,
( leq(n0,pv21)
| ~ spl48_48 ),
inference(avatar_component_clause,[],[f809]) ).
fof(f813,definition,
( spl48_49
<=> leq(pv21,n5) ),
introduced(definition,[new_symbols(definition,[spl48_49])],[avatar_definition]) ).
fof(f815,plain,
( ~ leq(pv21,n5)
| spl48_49 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f817,definition,
( spl48_50
<=> leq(pv21,minus(n6,n1)) ),
introduced(definition,[new_symbols(definition,[spl48_50])],[avatar_definition]) ).
fof(f818,plain,
( leq(pv21,minus(n6,n1))
| ~ spl48_50 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f820,plain,
( ~ spl48_47
| ~ spl48_2
| ~ spl48_10
| ~ spl48_48
| ~ spl48_24
| ~ spl48_49
| ~ spl48_50 ),
inference(avatar_split_clause,[],[f408,f817,f813,f655,f809,f599,f567,f805]) ).
fof(f822,definition,
( spl48_51
<=> sP35 ),
introduced(definition,[new_symbols(definition,[spl48_51])],[avatar_definition]) ).
fof(f825,plain,
( ~ spl48_51
| ~ spl48_10
| ~ spl48_40
| ~ spl48_24
| ~ spl48_42 ),
inference(avatar_split_clause,[],[f409,f781,f655,f773,f599,f822]) ).
fof(f827,definition,
( spl48_52
<=> sP34 ),
introduced(definition,[new_symbols(definition,[spl48_52])],[avatar_definition]) ).
fof(f830,plain,
( ~ spl48_52
| ~ spl48_10
| ~ spl48_24 ),
inference(avatar_split_clause,[],[f410,f655,f599,f827]) ).
fof(f832,definition,
( spl48_53
<=> sP31 ),
introduced(definition,[new_symbols(definition,[spl48_53])],[avatar_definition]) ).
fof(f835,plain,
( ~ spl48_53
| ~ spl48_10
| ~ spl48_24 ),
inference(avatar_split_clause,[],[f411,f655,f599,f832]) ).
fof(f837,definition,
( spl48_54
<=> sP39 ),
introduced(definition,[new_symbols(definition,[spl48_54])],[avatar_definition]) ).
fof(f841,definition,
( spl48_55
<=> true ),
introduced(definition,[new_symbols(definition,[spl48_55])],[avatar_definition]) ).
fof(f842,plain,
( ~ true
| spl48_55 ),
inference(avatar_component_clause,[],[f841]) ).
fof(f845,plain,
( ~ spl48_54
| ~ spl48_55 ),
inference(avatar_split_clause,[],[f413,f841,f837]) ).
fof(f847,plain,
( ~ spl48_47
| spl48_50 ),
inference(avatar_split_clause,[],[f415,f817,f805]) ).
fof(f848,plain,
( ~ spl48_47
| spl48_24 ),
inference(avatar_split_clause,[],[f416,f655,f805]) ).
fof(f849,plain,
( ~ spl48_47
| spl48_48 ),
inference(avatar_split_clause,[],[f417,f809,f805]) ).
fof(f850,plain,
( ~ spl48_47
| spl48_10 ),
inference(avatar_split_clause,[],[f418,f599,f805]) ).
fof(f851,plain,
( ~ spl48_39
| spl48_43 ),
inference(avatar_split_clause,[],[f419,f785,f769]) ).
fof(f852,plain,
( ~ spl48_39
| spl48_42 ),
inference(avatar_split_clause,[],[f420,f781,f769]) ).
fof(f853,plain,
( ~ spl48_39
| spl48_24 ),
inference(avatar_split_clause,[],[f421,f655,f769]) ).
fof(f854,plain,
( ~ spl48_39
| spl48_41 ),
inference(avatar_split_clause,[],[f422,f777,f769]) ).
fof(f855,plain,
( ~ spl48_39
| spl48_40 ),
inference(avatar_split_clause,[],[f423,f773,f769]) ).
fof(f856,plain,
( ~ spl48_39
| spl48_10 ),
inference(avatar_split_clause,[],[f424,f599,f769]) ).
fof(f857,plain,
( ~ spl48_51
| spl48_42 ),
inference(avatar_split_clause,[],[f425,f781,f822]) ).
fof(f858,plain,
( ~ spl48_51
| spl48_24 ),
inference(avatar_split_clause,[],[f426,f655,f822]) ).
fof(f859,plain,
( ~ spl48_51
| spl48_40 ),
inference(avatar_split_clause,[],[f427,f773,f822]) ).
fof(f860,plain,
( ~ spl48_51
| spl48_10 ),
inference(avatar_split_clause,[],[f428,f599,f822]) ).
fof(f862,plain,
( ~ spl48_52
| spl48_24 ),
inference(avatar_split_clause,[],[f430,f655,f827]) ).
fof(f864,plain,
( ~ spl48_52
| spl48_10 ),
inference(avatar_split_clause,[],[f432,f599,f827]) ).
fof(f866,definition,
( spl48_56
<=> sP33 ),
introduced(definition,[new_symbols(definition,[spl48_56])],[avatar_definition]) ).
fof(f871,plain,
( ~ spl48_56
| ~ spl48_55 ),
inference(avatar_split_clause,[],[f435,f841,f866]) ).
fof(f872,plain,
( ~ spl48_38
| spl48_24 ),
inference(avatar_split_clause,[],[f436,f655,f734]) ).
fof(f873,plain,
( ~ spl48_38
| spl48_10 ),
inference(avatar_split_clause,[],[f437,f599,f734]) ).
fof(f874,plain,
( ~ spl48_53
| spl48_24 ),
inference(avatar_split_clause,[],[f438,f655,f832]) ).
fof(f875,plain,
( ~ spl48_53
| spl48_10 ),
inference(avatar_split_clause,[],[f439,f599,f832]) ).
fof(f891,plain,
( spl48_54
| spl48_45
| spl48_47
| spl48_39
| spl48_51
| spl48_52
| spl48_56
| spl48_38
| spl48_53
| ~ spl48_55 ),
inference(avatar_split_clause,[],[f443,f841,f832,f734,f866,f827,f822,f769,f805,f796,f837]) ).
fof(f925,plain,
( $false
| spl48_55 ),
inference(forward_subsumption_resolution,[],[f348,f842]) ).
fof(f926,plain,
spl48_55,
inference(avatar_contradiction_clause,[],[f925]) ).
fof(f943,plain,
! [X0,X1] :
( gt(plus(n1,X0),X1)
| ~ leq(X1,X0) ),
inference(superposition,[],[f536,f539]) ).
fof(f964,plain,
! [X0] : ~ leq(plus(n1,X0),X0),
inference(resolution,[],[f943,f192]) ).
fof(f1004,plain,
leq(n0,n7),
inference(resolution,[],[f195,f463]) ).
fof(f1005,plain,
leq(n0,minus(n1000,n1)),
inference(resolution,[],[f195,f460]) ).
fof(f1006,plain,
leq(n0,minus(n4,n1)),
inference(resolution,[],[f195,f461]) ).
fof(f1007,plain,
( $false
| spl48_46 ),
inference(forward_subsumption_resolution,[],[f1005,f802]) ).
fof(f1008,plain,
spl48_46,
inference(avatar_contradiction_clause,[],[f1007]) ).
fof(f1027,plain,
leq(n0,n1),
inference(resolution,[],[f196,f494]) ).
fof(f1028,plain,
leq(n0,n2),
inference(resolution,[],[f196,f495]) ).
fof(f1029,plain,
leq(n0,n3),
inference(resolution,[],[f196,f497]) ).
fof(f1030,plain,
leq(n0,n4),
inference(resolution,[],[f196,f490]) ).
fof(f1031,plain,
leq(n0,n5),
inference(resolution,[],[f196,f491]) ).
fof(f1034,plain,
leq(n0,n6),
inference(resolution,[],[f196,f492]) ).
fof(f1054,plain,
leq(n1,n5),
inference(resolution,[],[f196,f500]) ).
fof(f1056,plain,
leq(n1,n7),
inference(resolution,[],[f196,f502]) ).
fof(f1061,plain,
leq(n2,n5),
inference(resolution,[],[f196,f508]) ).
fof(f1063,plain,
leq(n2,n7),
inference(resolution,[],[f196,f510]) ).
fof(f1067,plain,
leq(n3,n5),
inference(resolution,[],[f196,f515]) ).
fof(f1069,plain,
leq(n3,n7),
inference(resolution,[],[f196,f517]) ).
fof(f1072,plain,
leq(n4,n5),
inference(resolution,[],[f196,f466]) ).
fof(f1074,plain,
leq(n4,n7),
inference(resolution,[],[f196,f468]) ).
fof(f1078,plain,
leq(n5,n7),
inference(resolution,[],[f196,f472]) ).
fof(f1084,plain,
leq(n6,n7),
inference(resolution,[],[f196,f475]) ).
fof(f1086,plain,
leq(n588,n1000),
inference(resolution,[],[f196,f464]) ).
fof(f1087,plain,
( $false
| spl48_3 ),
inference(forward_subsumption_resolution,[],[f1027,f573]) ).
fof(f1088,plain,
spl48_3,
inference(avatar_contradiction_clause,[],[f1087]) ).
fof(f1089,plain,
( $false
| spl48_2 ),
inference(forward_subsumption_resolution,[],[f569,f193]) ).
fof(f1090,plain,
spl48_2,
inference(avatar_contradiction_clause,[],[f1089]) ).
fof(f1118,plain,
( $false
| spl48_4 ),
inference(forward_subsumption_resolution,[],[f1028,f577]) ).
fof(f1119,plain,
spl48_4,
inference(avatar_contradiction_clause,[],[f1118]) ).
fof(f1127,plain,
( $false
| spl48_5 ),
inference(forward_subsumption_resolution,[],[f1029,f581]) ).
fof(f1128,plain,
spl48_5,
inference(avatar_contradiction_clause,[],[f1127]) ).
fof(f1137,plain,
( $false
| spl48_6 ),
inference(forward_subsumption_resolution,[],[f1030,f585]) ).
fof(f1138,plain,
spl48_6,
inference(avatar_contradiction_clause,[],[f1137]) ).
fof(f1173,plain,
( $false
| spl48_7 ),
inference(forward_subsumption_resolution,[],[f1031,f589]) ).
fof(f1174,plain,
spl48_7,
inference(avatar_contradiction_clause,[],[f1173]) ).
fof(f1188,plain,
( $false
| spl48_8 ),
inference(forward_subsumption_resolution,[],[f1034,f593]) ).
fof(f1189,plain,
spl48_8,
inference(avatar_contradiction_clause,[],[f1188]) ).
fof(f1190,plain,
( $false
| spl48_9 ),
inference(forward_subsumption_resolution,[],[f597,f1004]) ).
fof(f1191,plain,
spl48_9,
inference(avatar_contradiction_clause,[],[f1190]) ).
fof(f1299,plain,
! [X0] : plus(n1,minus(X0,n1)) = X0,
inference(forward_demodulation,[],[f549,f539]) ).
fof(f1748,plain,
! [X0] : ~ leq(X0,minus(X0,n1)),
inference(superposition,[],[f964,f1299]) ).
fof(f3473,plain,
( ~ gt(n6,n0)
| spl48_11 ),
inference(resolution,[],[f533,f605]) ).
fof(f3502,plain,
( $false
| spl48_11 ),
inference(forward_subsumption_resolution,[],[f3473,f492]) ).
fof(f3503,plain,
spl48_11,
inference(avatar_contradiction_clause,[],[f3502]) ).
fof(f3506,plain,
( $false
| spl48_12 ),
inference(forward_subsumption_resolution,[],[f609,f1056]) ).
fof(f3507,plain,
spl48_12,
inference(avatar_contradiction_clause,[],[f3506]) ).
fof(f3511,plain,
( ~ gt(n6,n1)
| spl48_13 ),
inference(resolution,[],[f613,f533]) ).
fof(f3512,plain,
( $false
| spl48_13 ),
inference(forward_subsumption_resolution,[],[f3511,f501]) ).
fof(f3513,plain,
spl48_13,
inference(avatar_contradiction_clause,[],[f3512]) ).
fof(f3514,plain,
( $false
| spl48_14 ),
inference(forward_subsumption_resolution,[],[f617,f1063]) ).
fof(f3515,plain,
spl48_14,
inference(avatar_contradiction_clause,[],[f3514]) ).
fof(f3528,plain,
( ~ gt(n6,n2)
| spl48_15 ),
inference(resolution,[],[f621,f533]) ).
fof(f3529,plain,
( $false
| spl48_15 ),
inference(forward_subsumption_resolution,[],[f3528,f509]) ).
fof(f3530,plain,
spl48_15,
inference(avatar_contradiction_clause,[],[f3529]) ).
fof(f3531,plain,
( $false
| spl48_16 ),
inference(forward_subsumption_resolution,[],[f625,f1069]) ).
fof(f3532,plain,
spl48_16,
inference(avatar_contradiction_clause,[],[f3531]) ).
fof(f3567,plain,
( ~ gt(n6,n3)
| spl48_17 ),
inference(resolution,[],[f629,f533]) ).
fof(f3568,plain,
( $false
| spl48_17 ),
inference(forward_subsumption_resolution,[],[f3567,f516]) ).
fof(f3569,plain,
spl48_17,
inference(avatar_contradiction_clause,[],[f3568]) ).
fof(f3570,plain,
( $false
| spl48_18 ),
inference(forward_subsumption_resolution,[],[f633,f1074]) ).
fof(f3571,plain,
spl48_18,
inference(avatar_contradiction_clause,[],[f3570]) ).
fof(f3573,plain,
( ~ gt(n6,n4)
| spl48_19 ),
inference(resolution,[],[f637,f533]) ).
fof(f3574,plain,
( $false
| spl48_19 ),
inference(forward_subsumption_resolution,[],[f3573,f467]) ).
fof(f3575,plain,
spl48_19,
inference(avatar_contradiction_clause,[],[f3574]) ).
fof(f3576,plain,
( $false
| spl48_20 ),
inference(forward_subsumption_resolution,[],[f641,f1078]) ).
fof(f3577,plain,
spl48_20,
inference(avatar_contradiction_clause,[],[f3576]) ).
fof(f3587,plain,
( ~ gt(n6,n5)
| spl48_21 ),
inference(resolution,[],[f645,f533]) ).
fof(f3588,plain,
( $false
| spl48_21 ),
inference(forward_subsumption_resolution,[],[f3587,f471]) ).
fof(f3589,plain,
spl48_21,
inference(avatar_contradiction_clause,[],[f3588]) ).
fof(f3590,plain,
( $false
| spl48_22 ),
inference(forward_subsumption_resolution,[],[f649,f1084]) ).
fof(f3591,plain,
spl48_22,
inference(avatar_contradiction_clause,[],[f3590]) ).
fof(f3592,plain,
( $false
| spl48_23 ),
inference(forward_subsumption_resolution,[],[f653,f193]) ).
fof(f3593,plain,
spl48_23,
inference(avatar_contradiction_clause,[],[f3592]) ).
fof(f3594,plain,
( $false
| spl48_27 ),
inference(forward_subsumption_resolution,[],[f670,f1006]) ).
fof(f3595,plain,
spl48_27,
inference(avatar_contradiction_clause,[],[f3594]) ).
fof(f3597,plain,
( ~ gt(n4,n1)
| spl48_28 ),
inference(resolution,[],[f674,f533]) ).
fof(f3598,plain,
( $false
| spl48_28 ),
inference(forward_subsumption_resolution,[],[f3597,f499]) ).
fof(f3599,plain,
spl48_28,
inference(avatar_contradiction_clause,[],[f3598]) ).
fof(f3603,plain,
( ~ gt(n4,n2)
| spl48_29 ),
inference(resolution,[],[f678,f533]) ).
fof(f3604,plain,
( $false
| spl48_29 ),
inference(forward_subsumption_resolution,[],[f3603,f507]) ).
fof(f3605,plain,
spl48_29,
inference(avatar_contradiction_clause,[],[f3604]) ).
fof(f3608,plain,
( ~ gt(n4,n3)
| spl48_30 ),
inference(resolution,[],[f682,f533]) ).
fof(f3609,plain,
( $false
| spl48_30 ),
inference(forward_subsumption_resolution,[],[f3608,f514]) ).
fof(f3610,plain,
spl48_30,
inference(avatar_contradiction_clause,[],[f3609]) ).
fof(f3627,plain,
( ~ gt(n1000,pv5)
| spl48_25 ),
inference(resolution,[],[f661,f533]) ).
fof(f4379,definition,
( spl48_73
<=> n1000 = pv5 ),
introduced(definition,[new_symbols(definition,[spl48_73])],[avatar_definition]) ).
fof(f4381,plain,
( n1000 = pv5
| ~ spl48_73 ),
inference(avatar_component_clause,[],[f4379]) ).
fof(f4655,plain,
( gt(n6,pv21)
| ~ spl48_50 ),
inference(resolution,[],[f818,f532]) ).
fof(f4656,plain,
( leq(pv21,n6)
| ~ spl48_50 ),
inference(resolution,[],[f4655,f196]) ).
fof(f6341,plain,
( ! [X0] :
( ~ leq(n588,X0)
| leq(pv5,X0) )
| ~ spl48_24 ),
inference(resolution,[],[f194,f656]) ).
fof(f6343,plain,
( ! [X0] :
( leq(pv21,X0)
| ~ leq(n6,X0) )
| ~ spl48_50 ),
inference(resolution,[],[f194,f4656]) ).
fof(f6863,plain,
( ~ leq(pv5,n1000)
| n1000 = pv5
| spl48_25 ),
inference(resolution,[],[f197,f3627]) ).
fof(f6868,definition,
( spl48_77
<=> leq(pv5,n1000) ),
introduced(definition,[new_symbols(definition,[spl48_77])],[avatar_definition]) ).
fof(f6870,plain,
( ~ leq(pv5,n1000)
| spl48_77 ),
inference(avatar_component_clause,[],[f6868]) ).
fof(f6871,plain,
( spl48_73
| ~ spl48_77
| spl48_25 ),
inference(avatar_split_clause,[],[f6863,f659,f6868,f4379]) ).
fof(f7910,plain,
( leq(pv5,n1000)
| ~ spl48_24 ),
inference(resolution,[],[f6341,f1086]) ).
fof(f7941,plain,
( $false
| ~ spl48_24
| spl48_77 ),
inference(forward_subsumption_resolution,[],[f7910,f6870]) ).
fof(f7942,plain,
( ~ spl48_24
| spl48_77 ),
inference(avatar_contradiction_clause,[],[f7941]) ).
fof(f7944,plain,
( gt(pv5,n588)
| ~ spl48_73 ),
inference(superposition,[],[f464,f4381]) ).
fof(f7967,plain,
( leq(n588,pv5)
| ~ spl48_73 ),
inference(superposition,[],[f1086,f4381]) ).
fof(f8062,plain,
( ! [X0] :
( leq(n588,X0)
| ~ leq(pv5,X0) )
| ~ spl48_73 ),
inference(resolution,[],[f7967,f194]) ).
fof(f8271,definition,
( spl48_94
<=> n0 = pv21 ),
introduced(definition,[new_symbols(definition,[spl48_94])],[avatar_definition]) ).
fof(f8273,plain,
( n0 = pv21
| ~ spl48_94 ),
inference(avatar_component_clause,[],[f8271]) ).
fof(f8275,definition,
( spl48_95
<=> n1 = pv21 ),
introduced(definition,[new_symbols(definition,[spl48_95])],[avatar_definition]) ).
fof(f8277,plain,
( n1 = pv21
| ~ spl48_95 ),
inference(avatar_component_clause,[],[f8275]) ).
fof(f8295,definition,
( spl48_96
<=> n6 = pv21 ),
introduced(definition,[new_symbols(definition,[spl48_96])],[avatar_definition]) ).
fof(f8297,plain,
( n6 = pv21
| ~ spl48_96 ),
inference(avatar_component_clause,[],[f8295]) ).
fof(f9985,definition,
( spl48_121
<=> n2 = pv21 ),
introduced(definition,[new_symbols(definition,[spl48_121])],[avatar_definition]) ).
fof(f9987,plain,
( n2 = pv21
| ~ spl48_121 ),
inference(avatar_component_clause,[],[f9985]) ).
fof(f10209,plain,
( ~ leq(pv5,minus(n588,n1))
| ~ spl48_73 ),
inference(resolution,[],[f8062,f1748]) ).
fof(f10211,plain,
( ~ gt(n588,pv5)
| ~ spl48_73 ),
inference(resolution,[],[f10209,f533]) ).
fof(f10212,plain,
( ~ leq(pv5,n588)
| pv5 = n588
| ~ spl48_73 ),
inference(resolution,[],[f10211,f197]) ).
fof(f10215,plain,
( pv5 = n588
| ~ spl48_24
| ~ spl48_73 ),
inference(forward_subsumption_resolution,[],[f10212,f656]) ).
fof(f10242,plain,
( gt(pv5,pv5)
| ~ spl48_24
| ~ spl48_73 ),
inference(superposition,[],[f7944,f10215]) ).
fof(f10252,plain,
( $false
| ~ spl48_24
| ~ spl48_73 ),
inference(forward_subsumption_resolution,[],[f10242,f192]) ).
fof(f10253,plain,
( ~ spl48_24
| ~ spl48_73 ),
inference(avatar_contradiction_clause,[],[f10252]) ).
fof(f11778,definition,
( spl48_140
<=> n3 = pv21 ),
introduced(definition,[new_symbols(definition,[spl48_140])],[avatar_definition]) ).
fof(f11780,plain,
( n3 = pv21
| ~ spl48_140 ),
inference(avatar_component_clause,[],[f11778]) ).
fof(f12454,definition,
( spl48_142
<=> n4 = pv21 ),
introduced(definition,[new_symbols(definition,[spl48_142])],[avatar_definition]) ).
fof(f12456,plain,
( n4 = pv21
| ~ spl48_142 ),
inference(avatar_component_clause,[],[f12454]) ).
fof(f14027,plain,
( ~ leq(n0,pv21)
| n6 = pv21
| n5 = pv21
| n4 = pv21
| n3 = pv21
| n2 = pv21
| n1 = pv21
| n0 = pv21
| ~ leq(n6,n6)
| ~ spl48_50 ),
inference(resolution,[],[f521,f6343]) ).
fof(f14032,plain,
( n6 = pv21
| n5 = pv21
| n4 = pv21
| n3 = pv21
| n2 = pv21
| n1 = pv21
| n0 = pv21
| ~ leq(n6,n6)
| ~ spl48_48
| ~ spl48_50 ),
inference(forward_subsumption_resolution,[],[f14027,f810]) ).
fof(f14102,plain,
( n6 = pv21
| n5 = pv21
| n4 = pv21
| n3 = pv21
| n2 = pv21
| n1 = pv21
| n0 = pv21
| ~ spl48_48
| ~ spl48_50 ),
inference(forward_subsumption_resolution,[],[f14032,f193]) ).
fof(f14104,definition,
( spl48_186
<=> n5 = pv21 ),
introduced(definition,[new_symbols(definition,[spl48_186])],[avatar_definition]) ).
fof(f14106,plain,
( n5 = pv21
| ~ spl48_186 ),
inference(avatar_component_clause,[],[f14104]) ).
fof(f14138,plain,
( spl48_94
| spl48_95
| spl48_121
| spl48_140
| spl48_142
| spl48_186
| spl48_96
| ~ spl48_48
| ~ spl48_50 ),
inference(avatar_split_clause,[],[f14102,f817,f809,f8295,f14104,f12454,f11778,f9985,f8275,f8271]) ).
fof(f14140,plain,
( ~ leq(n5,n5)
| spl48_49
| ~ spl48_186 ),
inference(superposition,[],[f815,f14106]) ).
fof(f14174,plain,
( $false
| spl48_49
| ~ spl48_186 ),
inference(forward_subsumption_resolution,[],[f14140,f193]) ).
fof(f14175,plain,
( spl48_49
| ~ spl48_186 ),
inference(avatar_contradiction_clause,[],[f14174]) ).
fof(f14177,plain,
( ~ leq(n4,n5)
| spl48_49
| ~ spl48_142 ),
inference(superposition,[],[f815,f12456]) ).
fof(f14221,plain,
( $false
| spl48_49
| ~ spl48_142 ),
inference(forward_subsumption_resolution,[],[f14177,f1072]) ).
fof(f14222,plain,
( spl48_49
| ~ spl48_142 ),
inference(avatar_contradiction_clause,[],[f14221]) ).
fof(f14224,plain,
( ~ leq(n3,n5)
| spl48_49
| ~ spl48_140 ),
inference(superposition,[],[f815,f11780]) ).
fof(f14262,plain,
( $false
| spl48_49
| ~ spl48_140 ),
inference(forward_subsumption_resolution,[],[f14224,f1067]) ).
fof(f14263,plain,
( spl48_49
| ~ spl48_140 ),
inference(avatar_contradiction_clause,[],[f14262]) ).
fof(f14265,plain,
( ~ leq(n2,n5)
| spl48_49
| ~ spl48_121 ),
inference(superposition,[],[f815,f9987]) ).
fof(f14309,plain,
( $false
| spl48_49
| ~ spl48_121 ),
inference(forward_subsumption_resolution,[],[f14265,f1061]) ).
fof(f14310,plain,
( spl48_49
| ~ spl48_121 ),
inference(avatar_contradiction_clause,[],[f14309]) ).
fof(f14458,plain,
( leq(n6,minus(n6,n1))
| ~ spl48_50
| ~ spl48_96 ),
inference(superposition,[],[f818,f8297]) ).
fof(f14508,plain,
( $false
| ~ spl48_50
| ~ spl48_96 ),
inference(forward_subsumption_resolution,[],[f14458,f1748]) ).
fof(f14509,plain,
( ~ spl48_50
| ~ spl48_96 ),
inference(avatar_contradiction_clause,[],[f14508]) ).
fof(f14511,plain,
( ~ leq(n1,n5)
| spl48_49
| ~ spl48_95 ),
inference(superposition,[],[f815,f8277]) ).
fof(f14561,plain,
( $false
| spl48_49
| ~ spl48_95 ),
inference(forward_subsumption_resolution,[],[f14511,f1054]) ).
fof(f14562,plain,
( spl48_49
| ~ spl48_95 ),
inference(avatar_contradiction_clause,[],[f14561]) ).
fof(f14564,plain,
( ~ leq(n0,n5)
| spl48_49
| ~ spl48_94 ),
inference(superposition,[],[f815,f8273]) ).
fof(f14617,plain,
( $false
| ~ spl48_7
| spl48_49
| ~ spl48_94 ),
inference(forward_subsumption_resolution,[],[f14564,f588]) ).
fof(f14618,plain,
( ~ spl48_7
| spl48_49
| ~ spl48_94 ),
inference(avatar_contradiction_clause,[],[f14617]) ).
cnf(s2,plain,
( ~ spl48_1
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30 ),
inference(sat_conversion,[],[f683]) ).
cnf(s5,plain,
( ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_31 ),
inference(sat_conversion,[],[f690]) ).
cnf(s8,plain,
( ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_32 ),
inference(sat_conversion,[],[f697]) ).
cnf(s11,plain,
( ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_33 ),
inference(sat_conversion,[],[f704]) ).
cnf(s14,plain,
( ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_34 ),
inference(sat_conversion,[],[f711]) ).
cnf(s16,plain,
( ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_35 ),
inference(sat_conversion,[],[f717]) ).
cnf(s18,plain,
( ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_36 ),
inference(sat_conversion,[],[f723]) ).
cnf(s21,plain,
( ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_37 ),
inference(sat_conversion,[],[f730]) ).
cnf(s27,plain,
( spl48_1
| ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_10
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_24
| ~ spl48_25
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| spl48_31
| spl48_32
| spl48_33
| spl48_34
| spl48_35
| spl48_36
| spl48_37
| ~ spl48_38 ),
inference(sat_conversion,[],[f740]) ).
cnf(s56,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_39
| ~ spl48_40
| ~ spl48_41
| ~ spl48_42
| ~ spl48_43 ),
inference(sat_conversion,[],[f793]) ).
cnf(s58,plain,
( ~ spl48_2
| ~ spl48_3
| ~ spl48_4
| ~ spl48_5
| ~ spl48_6
| ~ spl48_7
| ~ spl48_8
| ~ spl48_9
| ~ spl48_11
| ~ spl48_12
| ~ spl48_13
| ~ spl48_14
| ~ spl48_15
| ~ spl48_16
| ~ spl48_17
| ~ spl48_18
| ~ spl48_19
| ~ spl48_20
| ~ spl48_21
| ~ spl48_22
| ~ spl48_23
| ~ spl48_27
| ~ spl48_28
| ~ spl48_29
| ~ spl48_30
| ~ spl48_45
| ~ spl48_46 ),
inference(sat_conversion,[],[f803]) ).
cnf(s59,plain,
( ~ spl48_2
| ~ spl48_10
| ~ spl48_24
| ~ spl48_47
| ~ spl48_48
| ~ spl48_49
| ~ spl48_50 ),
inference(sat_conversion,[],[f820]) ).
cnf(s60,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_40
| ~ spl48_42
| ~ spl48_51 ),
inference(sat_conversion,[],[f825]) ).
cnf(s61,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_52 ),
inference(sat_conversion,[],[f830]) ).
cnf(s62,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_53 ),
inference(sat_conversion,[],[f835]) ).
cnf(s64,plain,
( ~ spl48_54
| ~ spl48_55 ),
inference(sat_conversion,[],[f845]) ).
cnf(s66,plain,
( ~ spl48_47
| spl48_50 ),
inference(sat_conversion,[],[f847]) ).
cnf(s67,plain,
( spl48_24
| ~ spl48_47 ),
inference(sat_conversion,[],[f848]) ).
cnf(s68,plain,
( ~ spl48_47
| spl48_48 ),
inference(sat_conversion,[],[f849]) ).
cnf(s69,plain,
( spl48_10
| ~ spl48_47 ),
inference(sat_conversion,[],[f850]) ).
cnf(s70,plain,
( ~ spl48_39
| spl48_43 ),
inference(sat_conversion,[],[f851]) ).
cnf(s71,plain,
( ~ spl48_39
| spl48_42 ),
inference(sat_conversion,[],[f852]) ).
cnf(s72,plain,
( spl48_24
| ~ spl48_39 ),
inference(sat_conversion,[],[f853]) ).
cnf(s73,plain,
( ~ spl48_39
| spl48_41 ),
inference(sat_conversion,[],[f854]) ).
cnf(s74,plain,
( ~ spl48_39
| spl48_40 ),
inference(sat_conversion,[],[f855]) ).
cnf(s75,plain,
( spl48_10
| ~ spl48_39 ),
inference(sat_conversion,[],[f856]) ).
cnf(s76,plain,
( spl48_42
| ~ spl48_51 ),
inference(sat_conversion,[],[f857]) ).
cnf(s77,plain,
( spl48_24
| ~ spl48_51 ),
inference(sat_conversion,[],[f858]) ).
cnf(s78,plain,
( spl48_40
| ~ spl48_51 ),
inference(sat_conversion,[],[f859]) ).
cnf(s79,plain,
( spl48_10
| ~ spl48_51 ),
inference(sat_conversion,[],[f860]) ).
cnf(s81,plain,
( spl48_24
| ~ spl48_52 ),
inference(sat_conversion,[],[f862]) ).
cnf(s83,plain,
( spl48_10
| ~ spl48_52 ),
inference(sat_conversion,[],[f864]) ).
cnf(s86,plain,
( ~ spl48_55
| ~ spl48_56 ),
inference(sat_conversion,[],[f871]) ).
cnf(s87,plain,
( spl48_24
| ~ spl48_38 ),
inference(sat_conversion,[],[f872]) ).
cnf(s88,plain,
( spl48_10
| ~ spl48_38 ),
inference(sat_conversion,[],[f873]) ).
cnf(s89,plain,
( spl48_24
| ~ spl48_53 ),
inference(sat_conversion,[],[f874]) ).
cnf(s90,plain,
( spl48_10
| ~ spl48_53 ),
inference(sat_conversion,[],[f875]) ).
cnf(s94,plain,
( spl48_38
| spl48_39
| spl48_45
| spl48_47
| spl48_51
| spl48_52
| spl48_53
| spl48_54
| ~ spl48_55
| spl48_56 ),
inference(sat_conversion,[],[f891]) ).
cnf(s111,plain,
spl48_55,
inference(sat_conversion,[],[f926]) ).
cnf(s114,plain,
spl48_46,
inference(sat_conversion,[],[f1008]) ).
cnf(s115,plain,
spl48_3,
inference(sat_conversion,[],[f1088]) ).
cnf(s116,plain,
spl48_2,
inference(sat_conversion,[],[f1090]) ).
cnf(s117,plain,
spl48_4,
inference(sat_conversion,[],[f1119]) ).
cnf(s118,plain,
spl48_5,
inference(sat_conversion,[],[f1128]) ).
cnf(s119,plain,
spl48_6,
inference(sat_conversion,[],[f1138]) ).
cnf(s120,plain,
spl48_7,
inference(sat_conversion,[],[f1174]) ).
cnf(s121,plain,
spl48_8,
inference(sat_conversion,[],[f1189]) ).
cnf(s122,plain,
spl48_9,
inference(sat_conversion,[],[f1191]) ).
cnf(s126,plain,
spl48_11,
inference(sat_conversion,[],[f3503]) ).
cnf(s127,plain,
spl48_12,
inference(sat_conversion,[],[f3507]) ).
cnf(s128,plain,
spl48_13,
inference(sat_conversion,[],[f3513]) ).
cnf(s129,plain,
spl48_14,
inference(sat_conversion,[],[f3515]) ).
cnf(s130,plain,
spl48_15,
inference(sat_conversion,[],[f3530]) ).
cnf(s131,plain,
spl48_16,
inference(sat_conversion,[],[f3532]) ).
cnf(s132,plain,
spl48_17,
inference(sat_conversion,[],[f3569]) ).
cnf(s133,plain,
spl48_18,
inference(sat_conversion,[],[f3571]) ).
cnf(s134,plain,
spl48_19,
inference(sat_conversion,[],[f3575]) ).
cnf(s135,plain,
spl48_20,
inference(sat_conversion,[],[f3577]) ).
cnf(s136,plain,
spl48_21,
inference(sat_conversion,[],[f3589]) ).
cnf(s137,plain,
spl48_22,
inference(sat_conversion,[],[f3591]) ).
cnf(s138,plain,
spl48_23,
inference(sat_conversion,[],[f3593]) ).
cnf(s139,plain,
spl48_27,
inference(sat_conversion,[],[f3595]) ).
cnf(s140,plain,
spl48_28,
inference(sat_conversion,[],[f3599]) ).
cnf(s141,plain,
spl48_29,
inference(sat_conversion,[],[f3605]) ).
cnf(s142,plain,
spl48_30,
inference(sat_conversion,[],[f3610]) ).
cnf(s148,plain,
( spl48_25
| spl48_73
| ~ spl48_77 ),
inference(sat_conversion,[],[f6871]) ).
cnf(s156,plain,
( ~ spl48_24
| spl48_77 ),
inference(sat_conversion,[],[f7942]) ).
cnf(s187,plain,
( ~ spl48_24
| ~ spl48_73 ),
inference(sat_conversion,[],[f10253]) ).
cnf(s222,plain,
( ~ spl48_48
| ~ spl48_50
| spl48_94
| spl48_95
| spl48_96
| spl48_121
| spl48_140
| spl48_142
| spl48_186 ),
inference(sat_conversion,[],[f14138]) ).
cnf(s223,plain,
( spl48_49
| ~ spl48_186 ),
inference(sat_conversion,[],[f14175]) ).
cnf(s224,plain,
( spl48_49
| ~ spl48_142 ),
inference(sat_conversion,[],[f14222]) ).
cnf(s225,plain,
( spl48_49
| ~ spl48_140 ),
inference(sat_conversion,[],[f14263]) ).
cnf(s226,plain,
( spl48_49
| ~ spl48_121 ),
inference(sat_conversion,[],[f14310]) ).
cnf(s229,plain,
( ~ spl48_50
| ~ spl48_96 ),
inference(sat_conversion,[],[f14509]) ).
cnf(s230,plain,
( spl48_49
| ~ spl48_95 ),
inference(sat_conversion,[],[f14562]) ).
cnf(s231,plain,
( ~ spl48_7
| spl48_49
| ~ spl48_94 ),
inference(sat_conversion,[],[f14618]) ).
cnf(s238,plain,
( spl48_38
| spl48_39
| spl48_45
| spl48_47
| spl48_51
| spl48_52
| spl48_53
| spl48_54
| spl48_56 ),
inference(rat,[],[s94,s111]) ).
cnf(s242,plain,
~ spl48_56,
inference(rat,[],[s86,s111]) ).
cnf(s243,plain,
~ spl48_54,
inference(rat,[],[s64,s111]) ).
cnf(s244,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_47
| ~ spl48_48
| ~ spl48_49
| ~ spl48_50 ),
inference(rat,[],[s59,s116]) ).
cnf(s245,plain,
~ spl48_45,
inference(rat,[],[s58,s114,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s267,plain,
( spl48_1
| ~ spl48_10
| ~ spl48_24
| ~ spl48_25
| spl48_31
| spl48_32
| spl48_33
| spl48_34
| spl48_35
| spl48_36
| spl48_37
| ~ spl48_38 ),
inference(rat,[],[s27,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s272,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_25
| ~ spl48_37 ),
inference(rat,[],[s21,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s275,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_25
| ~ spl48_36 ),
inference(rat,[],[s18,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s277,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_25
| ~ spl48_35 ),
inference(rat,[],[s16,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s279,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_25
| ~ spl48_34 ),
inference(rat,[],[s14,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s282,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_25
| ~ spl48_33 ),
inference(rat,[],[s11,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s285,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_25
| ~ spl48_32 ),
inference(rat,[],[s8,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s288,plain,
( ~ spl48_10
| ~ spl48_24
| ~ spl48_25
| ~ spl48_31 ),
inference(rat,[],[s5,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s291,plain,
( ~ spl48_1
| ~ spl48_10
| ~ spl48_24
| ~ spl48_25 ),
inference(rat,[],[s2,s142,s141,s140,s139,s138,s137,s136,s135,s134,s133,s132,s131,s130,s129,s128,s127,s126,s122,s121,s120,s119,s118,s117,s115,s116]) ).
cnf(s293,plain,
spl48_10,
inference(rat,[],[s238,s69,s75,s79,s83,s88,s90,s245,s243,s242]) ).
cnf(s294,plain,
spl48_24,
inference(rat,[],[s238,s67,s72,s77,s81,s87,s89,s245,s243,s242]) ).
cnf(s295,plain,
~ spl48_73,
inference(rat,[],[s187,s294]) ).
cnf(s296,plain,
spl48_77,
inference(rat,[],[s156,s294]) ).
cnf(s297,plain,
~ spl48_53,
inference(rat,[],[s62,s293,s294]) ).
cnf(s298,plain,
~ spl48_52,
inference(rat,[],[s61,s293,s294]) ).
cnf(s299,plain,
spl48_25,
inference(rat,[],[s148,s296,s295]) ).
cnf(s300,plain,
~ spl48_37,
inference(rat,[],[s272,s293,s294,s299]) ).
cnf(s301,plain,
~ spl48_36,
inference(rat,[],[s275,s293,s294,s299]) ).
cnf(s302,plain,
~ spl48_35,
inference(rat,[],[s277,s293,s294,s299]) ).
cnf(s303,plain,
~ spl48_34,
inference(rat,[],[s279,s293,s294,s299]) ).
cnf(s304,plain,
~ spl48_33,
inference(rat,[],[s282,s293,s294,s299]) ).
cnf(s305,plain,
~ spl48_32,
inference(rat,[],[s285,s293,s294,s299]) ).
cnf(s306,plain,
~ spl48_31,
inference(rat,[],[s288,s293,s294,s299]) ).
cnf(s307,plain,
( ~ spl48_48
| ~ spl48_50
| ~ spl48_47 ),
inference(rat,[],[s222,s223,s224,s225,s226,s230,s231,s229,s244,s294,s293,s120]) ).
cnf(s308,plain,
~ spl48_47,
inference(rat,[],[s307,s66,s68]) ).
cnf(s309,plain,
~ spl48_51,
inference(rat,[],[s60,s76,s78,s293,s294]) ).
cnf(s310,plain,
~ spl48_39,
inference(rat,[],[s56,s70,s71,s73,s74,s293,s294]) ).
cnf(s311,plain,
~ spl48_1,
inference(rat,[],[s291,s299,s293,s294]) ).
cnf(s312,plain,
~ spl48_38,
inference(rat,[],[s267,s305,s300,s301,s302,s303,s304,s299,s294,s293,s311,s306]) ).
cnf(s313,plain,
$false,
inference(rat,[],[s238,s242,s243,s297,s298,s308,s312,s245,s310,s309]) ).
fof(f14626,plain,
$false,
inference(avatar_sat_refutation,[],[s313]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV125+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 % Computer : n006.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 09:58:10 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.25/0.28 Running first-order model finding
% 0.25/0.28 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.98/0.92 % (3859607)Will run a generic schedule for satisfiability detection.
% 3.98/0.92 % (3859614)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2727407050:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.98/0.92 % (3859613)% WARNING: option uhcvi not known.
% 3.98/0.92 % (3859616)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2497584146:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.98/0.92 % (3859613)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3434674447:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.98/0.92 % (3859612)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1481631246_2999 on theBenchmark for (2999ds/0Mi)
% 3.98/0.92 % (3859615)dis+10_1_sil=32000:sp=arity:random_seed=890074291:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.98/0.92 % (3859617)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1324434145:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.98/0.92 % (3859618)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=528576999:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.98/0.92 % (3859617)Instruction limit reached!
% 3.98/0.92 % (3859617)------------------------------
% 3.98/0.92 % (3859617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.92 % (3859617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.92 % (3859617)CaDiCaL version: 2.1.3
% 3.98/0.92 % (3859617)Termination reason: Instruction limit
% 3.98/0.92 % (3859617)Termination phase: Saturation
% 3.98/0.92 % (3859617)Time elapsed: 0.091 s
% 3.98/0.92 % (3859617)Peak memory usage: 12 MB
% 3.98/0.92 % (3859617)Instructions burned: 132 (million)
% 3.98/0.92 % (3859615)Instruction limit reached!
% 3.98/0.92 % (3859615)------------------------------
% 3.98/0.92 % (3859615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.92 % (3859615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.92 % (3859615)CaDiCaL version: 2.1.3
% 3.98/0.92 % (3859615)Termination reason: Instruction limit
% 3.98/0.92 % (3859615)Termination phase: Saturation
% 3.98/0.92 % (3859615)Time elapsed: 0.097 s
% 3.98/0.92 % (3859615)Peak memory usage: 13 MB
% 3.98/0.92 % (3859615)Instructions burned: 106 (million)
% 3.98/0.92 % (3859616)Instruction limit reached!
% 3.98/0.92 % (3859616)------------------------------
% 3.98/0.92 % (3859616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.92 % (3859616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.92 % (3859616)CaDiCaL version: 2.1.3
% 3.98/0.92 % (3859616)Termination reason: Instruction limit
% 3.98/0.92 % (3859616)Termination phase: Saturation
% 3.98/0.92 % (3859616)Time elapsed: 0.098 s
% 3.98/0.92 % (3859616)Peak memory usage: 13 MB
% 3.98/0.92 % (3859616)Instructions burned: 119 (million)
% 3.98/0.92 % (3859629)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=314651412:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.98/0.92 % (3859627)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3291244823:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 3.98/0.92 % (3859628)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4207023495:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 3.98/0.92 % (3859618)Instruction limit reached!
% 3.98/0.92 % (3859618)------------------------------
% 3.98/0.92 % (3859618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.92 % (3859618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.92 % (3859618)CaDiCaL version: 2.1.3
% 3.98/0.92 % (3859618)Termination reason: Instruction limit
% 3.98/0.92 % (3859618)Termination phase: Saturation
% 3.98/0.92 % (3859618)Time elapsed: 0.166 s
% 3.98/0.92 % (3859618)Peak memory usage: 14 MB
% 3.98/0.92 % (3859618)Instructions burned: 159 (million)
% 3.98/0.92 % (3859633)ott-21_1_sil=16000:fs=off:random_seed=3086169715:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 3.98/0.92 % (3859628)Instruction limit reached!
% 3.98/0.92 % (3859628)------------------------------
% 3.98/0.92 % (3859628)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.92 % (3859628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.92 % (3859628)CaDiCaL version: 2.1.3
% 3.98/0.92 % (3859628)Termination reason: Instruction limit
% 3.98/0.92 % (3859628)Termination phase: Saturation
% 3.98/0.92 % (3859628)Time elapsed: 0.122 s
% 3.98/0.92 % (3859628)Peak memory usage: 14 MB
% 3.98/0.92 % (3859628)Instructions burned: 132 (million)
% 3.98/0.92 % (3859636)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2723966208:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 3.98/0.92 % TRYING [1]
% 3.98/0.92 % TRYING [2]
% 3.98/0.92 % (3859633)Instruction limit reached!
% 3.98/0.92 % (3859633)------------------------------
% 3.98/0.92 % (3859633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.92 % (3859633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.92 % (3859633)CaDiCaL version: 2.1.3
% 3.98/0.92 % (3859633)Termination reason: Instruction limit
% 3.98/0.92 % (3859633)Termination phase: Saturation
% 3.98/0.92 % (3859633)Time elapsed: 0.161 s
% 3.98/0.92 % (3859633)Peak memory usage: 13 MB
% 3.98/0.92 % (3859633)Instructions burned: 180 (million)
% 3.98/0.92 % TRYING [3]
% 3.98/0.92 % (3859638)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1334664436:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 3.98/0.92 % TRYING [4]
% 3.98/0.92 % (3859629) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3859607-3859629"...
% 3.98/0.92 % (3859629)...printing done.
% 3.98/0.92 % (3859629)Refutation found. Thanks to Tanya!
% 3.98/0.92 % SZS status Theorem for theBenchmark
% 3.98/0.92 % SZS output start Proof for theBenchmark
% See solution above
% 3.98/0.92 % (3859629)------------------------------
% 3.98/0.92 % (3859629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.98/0.92 % (3859629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.98/0.92 % (3859629)CaDiCaL version: 2.1.3
% 3.98/0.92 % (3859629)Termination reason: Refutation
% 3.98/0.92 % (3859629)Time elapsed: 0.457 s
% 3.98/0.92 % (3859629)Peak memory usage: 17 MB
% 3.98/0.92 % (3859629)Instructions burned: 457 (million)
% 3.98/0.92 % (3859607)Success in time 0.633 s
% 3.98/0.92 % Vampire exiting
%------------------------------------------------------------------------------