%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV030+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:11:45 PM UTC 2026
% Result : Theorem 25.59s 9.04s
% Output : Proof 25.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 1
% Syntax : Number of formulae : 198 ( 18 unt; 0 def)
% Number of atoms : 1196 ( 145 equ)
% Maximal formula atoms : 34 ( 6 avg)
% Number of connectives : 1812 ( 814 ~; 898 |; 86 &)
% ( 0 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 30 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 16 con; 0-3 aty)
% Number of variables : 27 ( 0 sgn 18 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,conjecture,
( ( ! [C] :
( ( leq(C,minus(pv1376,n1))
& leq(n0,C) )
=> a_select2(s_values7_init,C) = init )
& ! [A] :
( ( leq(A,n2)
& leq(n0,A) )
=> ! [B] :
( ( leq(B,n3)
& leq(n0,B) )
=> a_select3(simplex7_init,B,A) = init ) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init )
=> ( ! [F] :
( ( leq(F,minus(pv1376,n1))
& leq(n0,F) )
=> a_select2(s_values7_init,F) = init )
& ! [D] :
( ( leq(D,n2)
& leq(n0,D) )
=> ! [E] :
( ( leq(E,n3)
& leq(n0,E) )
=> a_select3(simplex7_init,E,D) = init ) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gauss_init_0033) ).
fof(f52_neg,negated_conjecture,
~ ( ( ! [C] :
( ( leq(C,minus(pv1376,n1))
& leq(n0,C) )
=> a_select2(s_values7_init,C) = init )
& ! [A] :
( ( leq(A,n2)
& leq(n0,A) )
=> ! [B] :
( ( leq(B,n3)
& leq(n0,B) )
=> a_select3(simplex7_init,B,A) = init ) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init )
=> ( ! [F] :
( ( leq(F,minus(pv1376,n1))
& leq(n0,F) )
=> a_select2(s_values7_init,F) = init )
& ! [D] :
( ( leq(D,n2)
& leq(n0,D) )
=> ! [E] :
( ( leq(E,n3)
& leq(n0,E) )
=> a_select3(simplex7_init,E,D) = init ) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,plain,
( ( ? [F] :
( a_select2(s_values7_init,F) != init
& leq(F,minus(pv1376,n1))
& leq(n0,F) )
| ? [D] :
( ? [E] :
( a_select3(simplex7_init,E,D) != init
& leq(E,n3)
& leq(n0,E) )
& leq(D,n2)
& leq(n0,D) )
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,minus(pv1376,n1))
| ~ leq(n0,C) )
& ! [A] :
( ! [B] :
( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B) )
| ~ leq(A,n2)
| ~ leq(n0,A) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ),
inference(nnf_transformation,[status(thm)],[f52_neg]) ).
fof(f52_sk,plain,
! [A,B,C] :
( ( ( a_select2(s_values7_init,sk29) != init
& leq(sk29,minus(pv1376,n1))
& leq(n0,sk29) )
| ( a_select3(simplex7_init,sk28,sk27) != init
& leq(sk28,n3)
& leq(n0,sk28)
& leq(sk27,n2)
& leq(n0,sk27) )
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init )
& ( a_select2(s_values7_init,C) = init
| ~ leq(C,minus(pv1376,n1))
| ~ leq(n0,C) )
& ( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B)
| ~ leq(A,n2)
| ~ leq(n0,A) )
& leq(pv1376,n3)
& leq(pv20,minus(n330,n1))
& leq(pv19,minus(n410,n1))
& leq(pv7,minus(n410,n1))
& leq(n0,pv1376)
& leq(n0,pv20)
& leq(n0,pv19)
& leq(n0,pv7)
& init = init ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27,sk28,sk29])],[f52_nnf]) ).
cnf(c267,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p500,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c267]) ).
cnf(c256,plain,
leq(n0,pv7),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p501,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p500,c256]) ).
cnf(c257,plain,
leq(n0,pv19),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p502,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p501,c257]) ).
cnf(c258,plain,
leq(n0,pv20),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p503,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p502,c258]) ).
cnf(c259,plain,
leq(n0,pv1376),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p504,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p503,c259]) ).
cnf(c260,plain,
leq(pv7,minus(n410,n1)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p505,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p504,c260]) ).
cnf(c261,plain,
leq(pv19,minus(n410,n1)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p506,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p505,c261]) ).
cnf(c262,plain,
leq(pv20,minus(n330,n1)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p507,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p506,c262]) ).
cnf(c263,plain,
leq(pv1376,n3),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p508,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p507,c263]) ).
cnf(c266,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p333,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c266]) ).
cnf(p334,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p333,c256]) ).
cnf(p335,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p334,c257]) ).
cnf(p336,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p335,c258]) ).
cnf(p337,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p336,c259]) ).
cnf(p338,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p337,c260]) ).
cnf(p339,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p338,c261]) ).
cnf(p340,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p339,c262]) ).
cnf(p341,plain,
( leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p340,c263]) ).
cnf(c265,plain,
( a_select2(s_values7_init,X2) = init
| ~ leq(X2,minus(pv1376,n1))
| ~ leq(n0,X2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p342,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,minus(pv1376,n1))
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p341,c265]) ).
cnf(p509,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p508,p342]) ).
cnf(p510,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p509]) ).
cnf(c268,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p491,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c268]) ).
cnf(p492,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p491,c256]) ).
cnf(p493,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p492,c257]) ).
cnf(p494,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p493,c258]) ).
cnf(p495,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p494,c259]) ).
cnf(p496,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p495,c260]) ).
cnf(p497,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p496,c261]) ).
cnf(p498,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p497,c262]) ).
cnf(p499,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p498,c263]) ).
cnf(p511,plain,
( leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p510,p499]) ).
cnf(p512,plain,
leq(n0,sk27),
inference(factoring,[status(thm)],[p511]) ).
cnf(c264,plain,
( a_select3(simplex7_init,X1,X0) = init
| ~ leq(X1,n3)
| ~ leq(n0,X1)
| ~ leq(X0,n2)
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p514,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| ~ leq(sk27,n2) ),
inference(resolution,[status(thm)],[p512,c264]) ).
cnf(c269,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p456,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c269]) ).
cnf(p483,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p456,c256]) ).
cnf(p484,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p483,c257]) ).
cnf(p485,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p484,c258]) ).
cnf(p486,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p485,c259]) ).
cnf(p487,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p486,c260]) ).
cnf(p488,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p487,c261]) ).
cnf(p489,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p488,c262]) ).
cnf(p490,plain,
( leq(n0,sk29)
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p489,c263]) ).
cnf(p517,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p514,p490]) ).
cnf(c273,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p432,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c273]) ).
cnf(p433,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p432,c256]) ).
cnf(p434,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p433,c257]) ).
cnf(p435,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p434,c258]) ).
cnf(p436,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p435,c259]) ).
cnf(p437,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p436,c260]) ).
cnf(p438,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p437,c261]) ).
cnf(p439,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p438,c262]) ).
cnf(p440,plain,
( leq(sk29,minus(pv1376,n1))
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p439,c263]) ).
cnf(c272,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p409,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c272]) ).
cnf(p410,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p409,c256]) ).
cnf(p411,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p410,c257]) ).
cnf(p412,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p411,c258]) ).
cnf(p413,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p412,c259]) ).
cnf(p414,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p413,c260]) ).
cnf(p415,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p414,c261]) ).
cnf(p416,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p415,c262]) ).
cnf(p417,plain,
( leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p416,c263]) ).
cnf(p418,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,minus(pv1376,n1))
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p417,c265]) ).
cnf(p442,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p440,p418]) ).
cnf(p447,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p442]) ).
cnf(c274,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p400,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c274]) ).
cnf(p401,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p400,c256]) ).
cnf(p402,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p401,c257]) ).
cnf(p403,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p402,c258]) ).
cnf(p404,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p403,c259]) ).
cnf(p405,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p404,c260]) ).
cnf(p406,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p405,c261]) ).
cnf(p407,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p406,c262]) ).
cnf(p408,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p407,c263]) ).
cnf(p448,plain,
( leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p447,p408]) ).
cnf(p450,plain,
leq(n0,sk28),
inference(factoring,[status(thm)],[p448]) ).
cnf(p523,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3) ),
inference(resolution,[status(thm)],[p517,p450]) ).
cnf(c275,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p391,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c275]) ).
cnf(p392,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p391,c256]) ).
cnf(p393,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p392,c257]) ).
cnf(p394,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p393,c258]) ).
cnf(p395,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p394,c259]) ).
cnf(p396,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p395,c260]) ).
cnf(p397,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p396,c261]) ).
cnf(p398,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p397,c262]) ).
cnf(p399,plain,
( leq(n0,sk29)
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p398,c263]) ).
cnf(p525,plain,
( leq(n0,sk29)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init ),
inference(resolution,[status(thm)],[p523,p399]) ).
cnf(p526,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init ),
inference(factoring,[status(thm)],[p525]) ).
cnf(c278,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p361,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c278]) ).
cnf(p362,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p361,c256]) ).
cnf(p363,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p362,c257]) ).
cnf(p364,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p363,c258]) ).
cnf(p365,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p364,c259]) ).
cnf(p366,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p365,c260]) ).
cnf(p367,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p366,c261]) ).
cnf(p368,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p367,c262]) ).
cnf(p369,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(resolution,[status(thm)],[p368,c263]) ).
cnf(p529,plain,
( leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p526,p369]) ).
cnf(p530,plain,
leq(n0,sk29),
inference(factoring,[status(thm)],[p529]) ).
cnf(p531,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,minus(pv1376,n1)) ),
inference(resolution,[status(thm)],[p530,c265]) ).
cnf(c270,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p452,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c270]) ).
cnf(p453,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p452,c256]) ).
cnf(p454,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p453,c257]) ).
cnf(p455,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p454,c258]) ).
cnf(p475,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p455,c259]) ).
cnf(p476,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p475,c260]) ).
cnf(p477,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p476,c261]) ).
cnf(p478,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p477,c262]) ).
cnf(p479,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p478,c263]) ).
cnf(p535,plain,
( leq(sk27,n2)
| a_select2(s_values7_init,sk29) = init ),
inference(resolution,[status(thm)],[p531,p479]) ).
cnf(c271,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p423,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c271]) ).
cnf(p424,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p423,c256]) ).
cnf(p425,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p424,c257]) ).
cnf(p426,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p425,c258]) ).
cnf(p427,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p426,c259]) ).
cnf(p428,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p427,c260]) ).
cnf(p429,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p428,c261]) ).
cnf(p430,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p429,c262]) ).
cnf(p431,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p430,c263]) ).
cnf(p539,plain,
( leq(sk27,n2)
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p535,p431]) ).
cnf(p540,plain,
leq(sk27,n2),
inference(factoring,[status(thm)],[p539]) ).
cnf(p542,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p540,p514]) ).
cnf(p548,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3) ),
inference(resolution,[status(thm)],[p542,p450]) ).
cnf(c276,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p379,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c276]) ).
cnf(p380,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p379,c256]) ).
cnf(p381,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p380,c257]) ).
cnf(p382,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p381,c258]) ).
cnf(p383,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p382,c259]) ).
cnf(p384,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p383,c260]) ).
cnf(p385,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p384,c261]) ).
cnf(p386,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p385,c262]) ).
cnf(p387,plain,
( leq(sk29,minus(pv1376,n1))
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p386,c263]) ).
cnf(p534,plain,
( leq(sk28,n3)
| a_select2(s_values7_init,sk29) = init ),
inference(resolution,[status(thm)],[p531,p387]) ).
cnf(c277,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p370,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c277]) ).
cnf(p371,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p370,c256]) ).
cnf(p372,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p371,c257]) ).
cnf(p373,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p372,c258]) ).
cnf(p374,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p373,c259]) ).
cnf(p375,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p374,c260]) ).
cnf(p376,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p375,c261]) ).
cnf(p377,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3)
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p376,c262]) ).
cnf(p378,plain,
( a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p377,c263]) ).
cnf(p536,plain,
( leq(sk28,n3)
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p534,p378]) ).
cnf(p538,plain,
leq(sk28,n3),
inference(factoring,[status(thm)],[p536]) ).
cnf(p551,plain,
a_select3(simplex7_init,sk28,sk27) = init,
inference(resolution,[status(thm)],[p548,p538]) ).
cnf(c279,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p343,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c279]) ).
cnf(p344,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p343,c256]) ).
cnf(p345,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p344,c257]) ).
cnf(p346,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p345,c258]) ).
cnf(p347,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p346,c259]) ).
cnf(p348,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p347,c260]) ).
cnf(p349,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p348,c261]) ).
cnf(p350,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p349,c262]) ).
cnf(p351,plain,
( leq(sk29,minus(pv1376,n1))
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(resolution,[status(thm)],[p350,c263]) ).
cnf(p552,plain,
( leq(sk29,minus(pv1376,n1))
| init != init ),
inference(demodulation,[status(thm)],[p551,p351]) ).
cnf(p554,plain,
leq(sk29,minus(pv1376,n1)),
inference(equality_resolution,[status(thm)],[p552]) ).
cnf(p555,plain,
a_select2(s_values7_init,sk29) = init,
inference(resolution,[status(thm)],[p554,p531]) ).
cnf(c280,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7)
| init != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p352,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19)
| ~ leq(n0,pv7) ),
inference(equality_resolution,[status(thm)],[c280]) ).
cnf(p353,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20)
| ~ leq(n0,pv19) ),
inference(resolution,[status(thm)],[p352,c256]) ).
cnf(p354,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376)
| ~ leq(n0,pv20) ),
inference(resolution,[status(thm)],[p353,c257]) ).
cnf(p355,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1))
| ~ leq(n0,pv1376) ),
inference(resolution,[status(thm)],[p354,c258]) ).
cnf(p356,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1))
| ~ leq(pv7,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p355,c259]) ).
cnf(p357,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1))
| ~ leq(pv19,minus(n410,n1)) ),
inference(resolution,[status(thm)],[p356,c260]) ).
cnf(p358,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3)
| ~ leq(pv20,minus(n330,n1)) ),
inference(resolution,[status(thm)],[p357,c261]) ).
cnf(p359,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init
| ~ leq(pv1376,n3) ),
inference(resolution,[status(thm)],[p358,c262]) ).
cnf(p360,plain,
( a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(resolution,[status(thm)],[p359,c263]) ).
cnf(p553,plain,
( a_select2(s_values7_init,sk29) != init
| init != init ),
inference(demodulation,[status(thm)],[p551,p360]) ).
cnf(p556,plain,
( init != init
| init != init ),
inference(demodulation,[status(thm)],[p555,p553]) ).
cnf(p557,plain,
init != init,
inference(factoring,[status(thm)],[p556]) ).
cnf(p558,plain,
$false,
inference(equality_resolution,[status(thm)],[p557]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV030+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.58 % Computer : n004.cluster.edu
% 0.10/5.58 % Model : x86_64 x86_64
% 0.10/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.58 % Memory : 8046.5625MB
% 0.10/5.58 % OS : Linux 6.8.0-71-generic
% 0.10/5.58 % CPULimit : 300
% 0.10/5.58 % WCLimit : 300
% 0.10/5.58 % DateTime : Thu Sep 24 18:22:41 UTC 2026
% 0.10/5.58 % CPUTime :
% 0.10/5.58 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 25.59/9.04 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 25.59/9.04 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------