%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV042+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 : n001.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:57 PM UTC 2026
% Result : Theorem 27.86s 4.42s
% Output : Proof 27.86s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f52,conjecture,
( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [D] :
( ( leq(D,minus(plus(n1,n2),n1))
& leq(n0,D) )
=> a_select2(s_center7_init,D) = init )
& ! [C] :
( ( leq(C,n3)
& 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 ) ) )
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [H] :
( ( leq(H,n2)
& leq(n0,H) )
=> a_select2(s_center7_init,H) = init )
& ! [G] :
( ( leq(G,n3)
& leq(n0,G) )
=> a_select2(s_values7_init,G) = init )
& ! [E] :
( ( leq(E,n2)
& leq(n0,E) )
=> ! [F] :
( ( leq(F,n3)
& leq(n0,F) )
=> a_select3(simplex7_init,F,E) = init ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gauss_init_0081) ).
fof(f52_neg,negated_conjecture,
~ ( ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [D] :
( ( leq(D,minus(plus(n1,n2),n1))
& leq(n0,D) )
=> a_select2(s_center7_init,D) = init )
& ! [C] :
( ( leq(C,n3)
& 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 ) ) )
=> ( ( gt(loopcounter,n1)
=> ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init ) )
& ! [H] :
( ( leq(H,n2)
& leq(n0,H) )
=> a_select2(s_center7_init,H) = init )
& ! [G] :
( ( leq(G,n3)
& leq(n0,G) )
=> a_select2(s_values7_init,G) = init )
& ! [E] :
( ( leq(E,n2)
& leq(n0,E) )
=> ! [F] :
( ( leq(F,n3)
& leq(n0,F) )
=> a_select3(simplex7_init,F,E) = init ) ) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,plain,
( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| ? [H] :
( a_select2(s_center7_init,H) != init
& leq(H,n2)
& leq(n0,H) )
| ? [G] :
( a_select2(s_values7_init,G) != init
& leq(G,n3)
& leq(n0,G) )
| ? [E] :
( ? [F] :
( a_select3(simplex7_init,F,E) != init
& leq(F,n3)
& leq(n0,F) )
& leq(E,n2)
& leq(n0,E) ) )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ! [D] :
( a_select2(s_center7_init,D) = init
| ~ leq(D,minus(plus(n1,n2),n1))
| ~ leq(n0,D) )
& ! [C] :
( a_select2(s_values7_init,C) = init
| ~ leq(C,n3)
| ~ leq(n0,C) )
& ! [A] :
( ! [B] :
( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B) )
| ~ leq(A,n2)
| ~ leq(n0,A) ) ),
inference(nnf_transformation,[status(thm)],[f52_neg]) ).
fof(f52_sk,plain,
! [A,B,C,D] :
( ( ( ( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init )
& gt(loopcounter,n1) )
| ( a_select2(s_center7_init,sk30) != init
& leq(sk30,n2)
& leq(n0,sk30) )
| ( a_select2(s_values7_init,sk29) != init
& leq(sk29,n3)
& leq(n0,sk29) )
| ( a_select3(simplex7_init,sk28,sk27) != init
& leq(sk28,n3)
& leq(n0,sk28)
& leq(sk27,n2)
& leq(n0,sk27) ) )
& ( ( pvar1402_init = init
& pvar1401_init = init
& pvar1400_init = init )
| ~ gt(loopcounter,n1) )
& ( a_select2(s_center7_init,D) = init
| ~ leq(D,minus(plus(n1,n2),n1))
| ~ leq(n0,D) )
& ( a_select2(s_values7_init,C) = init
| ~ leq(C,n3)
| ~ leq(n0,C) )
& ( a_select3(simplex7_init,B,A) = init
| ~ leq(B,n3)
| ~ leq(n0,B)
| ~ leq(A,n2)
| ~ leq(n0,A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27,sk28,sk29,sk30])],[f52_nnf]) ).
cnf(c263,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(c257,plain,
( a_select2(s_center7_init,X3) = init
| ~ leq(X3,minus(plus(n1,n2),n1))
| ~ leq(n0,X3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(c261,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p421,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27)
| a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2) ),
inference(resolution,[status(thm)],[c257,c261]) ).
cnf(p902,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[c263,p421]) ).
cnf(p917,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p902]) ).
cnf(p920,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p917]) ).
cnf(p922,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p920]) ).
cnf(c265,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p924,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27)
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p922,c265]) ).
cnf(p929,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p924]) ).
cnf(p932,plain,
( gt(loopcounter,n1)
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p929]) ).
cnf(p934,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p932]) ).
cnf(c256,plain,
( a_select2(s_values7_init,X2) = init
| ~ leq(X2,n3)
| ~ leq(n0,X2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p938,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p934,c256]) ).
cnf(c267,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p943,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk27)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p938,c267]) ).
cnf(p970,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p943]) ).
cnf(p972,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p970]) ).
cnf(c273,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p985,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk27)
| leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p972,c273]) ).
cnf(p1005,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p985]) ).
cnf(p1008,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1005]) ).
cnf(p1010,plain,
( leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1008]) ).
cnf(p1012,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1010,c257]) ).
cnf(c269,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1020,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(n0,sk27)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1012,c269]) ).
cnf(p1108,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1020]) ).
cnf(p1110,plain,
( leq(sk29,n3)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1108]) ).
cnf(c271,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1115,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(n0,sk27)
| leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1110,c271]) ).
cnf(p1133,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1115]) ).
cnf(p1136,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1133]) ).
cnf(p1138,plain,
( leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1136]) ).
cnf(p1140,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk27)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1138,p938]) ).
cnf(p1144,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1140]) ).
cnf(p1146,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1144]) ).
cnf(c275,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1155,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(n0,sk27)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1146,c275]) ).
cnf(p1169,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1155]) ).
cnf(p1171,plain,
( leq(sk30,n2)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1169]) ).
cnf(p1173,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk27)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1171,p1012]) ).
cnf(p1181,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1173]) ).
cnf(p1183,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1181]) ).
cnf(c277,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1156,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk27)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1146,c277]) ).
cnf(p1178,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1156]) ).
cnf(p1180,plain,
( a_select2(s_center7_init,sk30) != init
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1178]) ).
cnf(p1184,plain,
( gt(loopcounter,n1)
| leq(n0,sk27)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1183,p1180]) ).
cnf(p1185,plain,
( gt(loopcounter,n1)
| gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1184]) ).
cnf(p1187,plain,
( gt(loopcounter,n1)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1185]) ).
cnf(c255,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(p1188,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| ~ leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1187,c255]) ).
cnf(c279,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1199,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1188,c279]) ).
cnf(p1201,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1199]) ).
cnf(c297,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p542,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[c297,c257]) ).
cnf(c299,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p552,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p542,c299]) ).
cnf(p680,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p552]) ).
cnf(p683,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p680]) ).
cnf(p685,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p683]) ).
cnf(c301,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p686,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28)
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p685,c301]) ).
cnf(p688,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p686]) ).
cnf(p691,plain,
( gt(loopcounter,n1)
| gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p688]) ).
cnf(p693,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p691]) ).
cnf(p697,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p693,c256]) ).
cnf(c303,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p702,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk28)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p697,c303]) ).
cnf(p725,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p702]) ).
cnf(p727,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p725]) ).
cnf(c309,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p735,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk28)
| leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p727,c309]) ).
cnf(p758,plain,
( leq(n0,sk30)
| leq(n0,sk28)
| leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p735]) ).
cnf(p762,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p758]) ).
cnf(p764,plain,
( leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p762]) ).
cnf(p766,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p764,c257]) ).
cnf(c305,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p774,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(n0,sk28)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p766,c305]) ).
cnf(p780,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p774]) ).
cnf(p795,plain,
( leq(sk29,n3)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p780]) ).
cnf(c307,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p799,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(n0,sk28)
| leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p795,c307]) ).
cnf(p816,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p799]) ).
cnf(p819,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p816]) ).
cnf(p821,plain,
( leq(sk29,n3)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p819]) ).
cnf(p823,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk28)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p821,p697]) ).
cnf(p826,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p823]) ).
cnf(p828,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p826]) ).
cnf(c311,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p833,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(n0,sk28)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p828,c311]) ).
cnf(p851,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p833]) ).
cnf(p853,plain,
( leq(sk30,n2)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p851]) ).
cnf(p855,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk28)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p853,p766]) ).
cnf(p862,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p855]) ).
cnf(p864,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p862]) ).
cnf(c313,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p835,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk28)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p828,c313]) ).
cnf(p859,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p835]) ).
cnf(p861,plain,
( a_select2(s_center7_init,sk30) != init
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p859]) ).
cnf(p865,plain,
( gt(loopcounter,n1)
| leq(n0,sk28)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p864,p861]) ).
cnf(p866,plain,
( gt(loopcounter,n1)
| gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p865]) ).
cnf(p868,plain,
( gt(loopcounter,n1)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p866]) ).
cnf(p1207,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1201,p868]) ).
cnf(p1213,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1207]) ).
cnf(c315,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1214,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1213,c315]) ).
cnf(p1215,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1214]) ).
cnf(p1218,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1215]) ).
cnf(p1220,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1218]) ).
cnf(c333,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1238,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk30)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1220,c333]) ).
cnf(p1247,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk30)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1238]) ).
cnf(p1250,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1247]) ).
cnf(p1252,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1250]) ).
cnf(p1254,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1252,c257]) ).
cnf(c281,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1264,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(sk27,n2)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1254,c281]) ).
cnf(p1313,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1264]) ).
cnf(p1315,plain,
( leq(sk27,n2)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1313]) ).
cnf(c283,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1319,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(sk27,n2)
| leq(sk27,n2)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1315,c283]) ).
cnf(p1324,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| leq(sk27,n2)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1319]) ).
cnf(p1327,plain,
( leq(sk27,n2)
| leq(sk27,n2)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1324]) ).
cnf(p1329,plain,
( leq(sk27,n2)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1327]) ).
cnf(p1333,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| gt(loopcounter,n1)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1329,p1188]) ).
cnf(p1336,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1333]) ).
cnf(p1342,plain,
( gt(loopcounter,n1)
| a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1336,p868]) ).
cnf(p1349,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1342]) ).
cnf(c317,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1263,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(sk28,n3)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1254,c317]) ).
cnf(p1283,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1263]) ).
cnf(p1285,plain,
( leq(sk28,n3)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1283]) ).
cnf(c319,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1289,plain,
( gt(loopcounter,n1)
| leq(n0,sk29)
| leq(sk28,n3)
| leq(sk28,n3)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1285,c319]) ).
cnf(p1298,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| leq(sk28,n3)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1289]) ).
cnf(p1301,plain,
( leq(sk28,n3)
| leq(sk28,n3)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1298]) ).
cnf(p1303,plain,
( leq(sk28,n3)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1301]) ).
cnf(p1350,plain,
( leq(n0,sk29)
| gt(loopcounter,n1)
| a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1349,p1303]) ).
cnf(p1351,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1350]) ).
cnf(p1353,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1351]) ).
cnf(c335,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1354,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1353,c335]) ).
cnf(p1366,plain,
( leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1354]) ).
cnf(p1368,plain,
( leq(sk30,n2)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1366]) ).
cnf(p1370,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| gt(loopcounter,n1)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1368,p1254]) ).
cnf(p1376,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1370]) ).
cnf(p1378,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1376]) ).
cnf(c337,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1356,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1353,c337]) ).
cnf(p1373,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1356]) ).
cnf(p1375,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1373]) ).
cnf(p1379,plain,
( leq(n0,sk29)
| gt(loopcounter,n1)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1378,p1375]) ).
cnf(p1380,plain,
( leq(n0,sk29)
| leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1379]) ).
cnf(p1382,plain,
( leq(n0,sk29)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1380]) ).
cnf(p1386,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1382,c256]) ).
cnf(c285,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1392,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk27,n2)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1386,c285]) ).
cnf(p1412,plain,
( leq(n0,sk30)
| leq(sk27,n2)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1392]) ).
cnf(c291,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1413,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk27,n2)
| leq(n0,sk30)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1412,c291]) ).
cnf(p1440,plain,
( leq(n0,sk30)
| leq(sk27,n2)
| leq(n0,sk30)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1413]) ).
cnf(p1443,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1440]) ).
cnf(p1445,plain,
( leq(n0,sk30)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1443]) ).
cnf(p1449,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| gt(loopcounter,n1)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1445,p1188]) ).
cnf(p1452,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1449]) ).
cnf(p1458,plain,
( gt(loopcounter,n1)
| a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1452,p868]) ).
cnf(p1465,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1458]) ).
cnf(c321,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1391,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk28,n3)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1386,c321]) ).
cnf(p1399,plain,
( leq(n0,sk30)
| leq(sk28,n3)
| a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1391]) ).
cnf(c327,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1402,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk28,n3)
| leq(n0,sk30)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1399,c327]) ).
cnf(p1425,plain,
( leq(n0,sk30)
| leq(sk28,n3)
| leq(n0,sk30)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1402]) ).
cnf(p1428,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1425]) ).
cnf(p1430,plain,
( leq(n0,sk30)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1428]) ).
cnf(p1466,plain,
( leq(n0,sk30)
| gt(loopcounter,n1)
| a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1465,p1430]) ).
cnf(p1468,plain,
( leq(n0,sk30)
| a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1466]) ).
cnf(p1470,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1468]) ).
cnf(c345,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1480,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1470,c345]) ).
cnf(p1496,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1480]) ).
cnf(p1498,plain,
( a_select2(s_values7_init,sk29) != init
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1496]) ).
cnf(c339,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1471,plain,
( gt(loopcounter,n1)
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1470,c339]) ).
cnf(p1483,plain,
( leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1471]) ).
cnf(p1485,plain,
( leq(sk29,n3)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1483]) ).
cnf(p1487,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1485,p1386]) ).
cnf(p1492,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1487]) ).
cnf(p1499,plain,
( leq(n0,sk30)
| gt(loopcounter,n1)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1498,p1492]) ).
cnf(p1500,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1499]) ).
cnf(p1502,plain,
( leq(n0,sk30)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1500]) ).
cnf(p1504,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1502,c257]) ).
cnf(c287,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1512,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(sk27,n2)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1504,c287]) ).
cnf(p1520,plain,
( leq(sk29,n3)
| leq(sk27,n2)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1512]) ).
cnf(c289,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1521,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(sk27,n2)
| leq(sk29,n3)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1520,c289]) ).
cnf(p1586,plain,
( leq(sk29,n3)
| leq(sk27,n2)
| leq(sk29,n3)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1521]) ).
cnf(p1589,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1586]) ).
cnf(p1591,plain,
( leq(sk29,n3)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1589]) ).
cnf(p1593,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1591,p1386]) ).
cnf(p1597,plain,
( a_select2(s_values7_init,sk29) = init
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1593]) ).
cnf(c295,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1599,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(sk27,n2)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1597,c295]) ).
cnf(p1613,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk27,n2)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1599]) ).
cnf(p1615,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1613]) ).
cnf(c293,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1598,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(sk27,n2)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1597,c293]) ).
cnf(p1605,plain,
( leq(sk30,n2)
| leq(sk27,n2)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1598]) ).
cnf(p1607,plain,
( leq(sk30,n2)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1605]) ).
cnf(p1609,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1607,p1504]) ).
cnf(p1612,plain,
( a_select2(s_center7_init,sk30) = init
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1609]) ).
cnf(p1616,plain,
( leq(sk27,n2)
| gt(loopcounter,n1)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1615,p1612]) ).
cnf(p1617,plain,
( leq(sk27,n2)
| leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1616]) ).
cnf(p1619,plain,
( leq(sk27,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1617]) ).
cnf(p1623,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| gt(loopcounter,n1)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1619,p1188]) ).
cnf(p1626,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1623]) ).
cnf(p1632,plain,
( gt(loopcounter,n1)
| a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1626,p868]) ).
cnf(p1640,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1632]) ).
cnf(c323,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1511,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(sk28,n3)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1504,c323]) ).
cnf(p1515,plain,
( leq(sk29,n3)
| leq(sk28,n3)
| a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1511]) ).
cnf(c325,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1517,plain,
( gt(loopcounter,n1)
| leq(sk29,n3)
| leq(sk28,n3)
| leq(sk29,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1515,c325]) ).
cnf(p1525,plain,
( leq(sk29,n3)
| leq(sk28,n3)
| leq(sk29,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1517]) ).
cnf(p1528,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1525]) ).
cnf(p1530,plain,
( leq(sk29,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1528]) ).
cnf(p1532,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1530,p1386]) ).
cnf(p1536,plain,
( a_select2(s_values7_init,sk29) = init
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1532]) ).
cnf(c331,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1544,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(sk28,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1536,c331]) ).
cnf(p1570,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk28,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1544]) ).
cnf(p1572,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1570]) ).
cnf(c329,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1539,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(sk28,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1536,c329]) ).
cnf(p1548,plain,
( leq(sk30,n2)
| leq(sk28,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1539]) ).
cnf(p1550,plain,
( leq(sk30,n2)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1548]) ).
cnf(p1552,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1550,p1504]) ).
cnf(p1555,plain,
( a_select2(s_center7_init,sk30) = init
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1552]) ).
cnf(p1573,plain,
( leq(sk28,n3)
| gt(loopcounter,n1)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1572,p1555]) ).
cnf(p1574,plain,
( leq(sk28,n3)
| leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1573]) ).
cnf(p1576,plain,
( leq(sk28,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1574]) ).
cnf(p1641,plain,
( gt(loopcounter,n1)
| a_select3(simplex7_init,sk28,sk27) = init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1640,p1576]) ).
cnf(p1642,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1641]) ).
cnf(c349,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1650,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1642,c349]) ).
cnf(p1684,plain,
( a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1650]) ).
cnf(c341,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1643,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1642,c341]) ).
cnf(p1651,plain,
( leq(sk30,n2)
| leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1643]) ).
cnf(p1653,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1651,p1504]) ).
cnf(p1658,plain,
( a_select2(s_center7_init,sk30) = init
| leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1653]) ).
cnf(c343,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1648,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1642,c343]) ).
cnf(p1656,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1648]) ).
cnf(p1659,plain,
( leq(sk29,n3)
| gt(loopcounter,n1)
| leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1658,p1656]) ).
cnf(p1660,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1659]) ).
cnf(p1662,plain,
( leq(sk29,n3)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1660]) ).
cnf(p1664,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1662,p1386]) ).
cnf(p1668,plain,
( a_select2(s_values7_init,sk29) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1664]) ).
cnf(p1685,plain,
( gt(loopcounter,n1)
| a_select2(s_center7_init,sk30) != init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1684,p1668]) ).
cnf(p1686,plain,
( a_select2(s_center7_init,sk30) != init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1685]) ).
cnf(c347,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1649,plain,
( gt(loopcounter,n1)
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1642,c347]) ).
cnf(p1657,plain,
( leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1649]) ).
cnf(p1669,plain,
( leq(sk30,n2)
| gt(loopcounter,n1)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1668,p1657]) ).
cnf(p1670,plain,
( leq(sk30,n2)
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1669]) ).
cnf(p1672,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1670,p1504]) ).
cnf(p1675,plain,
( a_select2(s_center7_init,sk30) = init
| gt(loopcounter,n1) ),
inference(factoring,[status(thm)],[p1672]) ).
cnf(p1687,plain,
( gt(loopcounter,n1)
| gt(loopcounter,n1) ),
inference(resolution,[status(thm)],[p1686,p1675]) ).
cnf(p1688,plain,
gt(loopcounter,n1),
inference(factoring,[status(thm)],[p1687]) ).
cnf(c258,plain,
( pvar1400_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1782,plain,
pvar1400_init = init,
inference(resolution,[status(thm)],[p1688,c258]) ).
cnf(c260,plain,
( pvar1402_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1736,plain,
pvar1402_init = init,
inference(resolution,[status(thm)],[p1688,c260]) ).
cnf(c259,plain,
( pvar1401_init = init
| ~ gt(loopcounter,n1) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1690,plain,
pvar1401_init = init,
inference(resolution,[status(thm)],[p1688,c259]) ).
cnf(c346,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1733,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c346]) ).
cnf(p1779,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1733]) ).
cnf(p1825,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1779]) ).
cnf(p2423,plain,
( init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p1825]) ).
cnf(p2424,plain,
( init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p2423]) ).
cnf(p2425,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(equality_resolution,[status(thm)],[p2424]) ).
cnf(c338,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1729,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c338]) ).
cnf(p1775,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1729]) ).
cnf(p1821,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1775]) ).
cnf(p2349,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p1821]) ).
cnf(p2350,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p2349]) ).
cnf(p2351,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(equality_resolution,[status(thm)],[p2350]) ).
cnf(c314,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1717,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c314]) ).
cnf(p1763,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1717]) ).
cnf(p1809,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1763]) ).
cnf(p2241,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1809]) ).
cnf(p2242,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2241]) ).
cnf(p2243,plain,
( a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p2242]) ).
cnf(c310,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1715,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c310]) ).
cnf(p1761,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1715]) ).
cnf(p1807,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1761]) ).
cnf(p2086,plain,
( init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1807]) ).
cnf(p2087,plain,
( init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2086]) ).
cnf(p2088,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p2087]) ).
cnf(c302,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1711,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c302]) ).
cnf(p1757,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1711]) ).
cnf(p1803,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1757]) ).
cnf(p2046,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1803]) ).
cnf(p2047,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2046]) ).
cnf(p2048,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p2047]) ).
cnf(c300,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1710,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c300]) ).
cnf(p1756,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1710]) ).
cnf(p1802,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1756]) ).
cnf(p1895,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1802]) ).
cnf(p1896,plain,
( init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1895]) ).
cnf(p1897,plain,
( leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p1896]) ).
cnf(c298,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1709,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c298]) ).
cnf(p1755,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1709]) ).
cnf(p1801,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1755]) ).
cnf(p1877,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1801]) ).
cnf(p1878,plain,
( init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1877]) ).
cnf(p1879,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p1878]) ).
cnf(p1881,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p1879,c257]) ).
cnf(p1899,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| leq(n0,sk28)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p1897,p1881]) ).
cnf(p1901,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1899]) ).
cnf(p1903,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1901]) ).
cnf(p2049,plain,
( leq(n0,sk29)
| leq(n0,sk28)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2048,p1903]) ).
cnf(p2050,plain,
( leq(n0,sk29)
| leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2049]) ).
cnf(p2052,plain,
( leq(n0,sk29)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2050]) ).
cnf(p2056,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,n3)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2052,c256]) ).
cnf(c304,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1712,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c304]) ).
cnf(p1758,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1712]) ).
cnf(p1804,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1758]) ).
cnf(p1904,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1804]) ).
cnf(p1905,plain,
( init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1904]) ).
cnf(p1906,plain,
( leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p1905]) ).
cnf(p2062,plain,
( leq(n0,sk30)
| leq(n0,sk28)
| a_select2(s_values7_init,sk29) = init
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2056,p1906]) ).
cnf(p2075,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) = init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2062]) ).
cnf(p2089,plain,
( leq(n0,sk30)
| leq(n0,sk28)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2088,p2075]) ).
cnf(p2090,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2089]) ).
cnf(p2092,plain,
( leq(n0,sk30)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2090]) ).
cnf(p2094,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2092,c257]) ).
cnf(c306,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1713,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c306]) ).
cnf(p1759,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1713]) ).
cnf(p1805,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1759]) ).
cnf(p1908,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1805]) ).
cnf(p1909,plain,
( init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1908]) ).
cnf(p1910,plain,
( leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p1909]) ).
cnf(p2102,plain,
( leq(sk29,n3)
| leq(n0,sk28)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2094,p1910]) ).
cnf(p2106,plain,
( leq(sk29,n3)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2102]) ).
cnf(c308,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1714,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c308]) ).
cnf(p1760,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1714]) ).
cnf(p1806,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1760]) ).
cnf(p2083,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1806]) ).
cnf(p2084,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2083]) ).
cnf(p2085,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p2084]) ).
cnf(p2108,plain,
( leq(sk29,n3)
| leq(n0,sk28)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2106,p2085]) ).
cnf(p2115,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2108]) ).
cnf(p2117,plain,
( leq(sk29,n3)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2115]) ).
cnf(p2119,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2117,p2056]) ).
cnf(p2123,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2119]) ).
cnf(p2244,plain,
( leq(n0,sk28)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2243,p2123]) ).
cnf(p2245,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2244]) ).
cnf(c312,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1716,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1690,c312]) ).
cnf(p1762,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1736,p1716]) ).
cnf(p1808,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(demodulation,[status(thm)],[p1782,p1762]) ).
cnf(p2134,plain,
( init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p1808]) ).
cnf(p2135,plain,
( init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2134]) ).
cnf(p2136,plain,
( leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk28) ),
inference(equality_resolution,[status(thm)],[p2135]) ).
cnf(p2137,plain,
( leq(n0,sk28)
| leq(sk30,n2)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2136,p2123]) ).
cnf(p2138,plain,
( leq(sk30,n2)
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2137]) ).
cnf(p2140,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2138,p2094]) ).
cnf(p2143,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk28) ),
inference(factoring,[status(thm)],[p2140]) ).
cnf(p2246,plain,
( leq(n0,sk28)
| leq(n0,sk28) ),
inference(resolution,[status(thm)],[p2245,p2143]) ).
cnf(p2247,plain,
leq(n0,sk28),
inference(factoring,[status(thm)],[p2246]) ).
cnf(c278,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1699,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c278]) ).
cnf(p1745,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1699]) ).
cnf(p1791,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1745]) ).
cnf(p2184,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1791]) ).
cnf(p2185,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p2184]) ).
cnf(p2186,plain,
( a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p2185]) ).
cnf(c274,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1697,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c274]) ).
cnf(p1743,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1697]) ).
cnf(p1789,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1743]) ).
cnf(p1972,plain,
( init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1789]) ).
cnf(p1973,plain,
( init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1972]) ).
cnf(p1974,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p1973]) ).
cnf(c266,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1693,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c266]) ).
cnf(p1739,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1693]) ).
cnf(p1785,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1739]) ).
cnf(p1933,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1785]) ).
cnf(p1934,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1933]) ).
cnf(p1935,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p1934]) ).
cnf(c264,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1692,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c264]) ).
cnf(p1738,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1692]) ).
cnf(p1784,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1738]) ).
cnf(p1841,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1784]) ).
cnf(p1842,plain,
( init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1841]) ).
cnf(p1843,plain,
( leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p1842]) ).
cnf(c262,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1691,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c262]) ).
cnf(p1737,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1691]) ).
cnf(p1783,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1737]) ).
cnf(p1830,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1783]) ).
cnf(p1831,plain,
( init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1830]) ).
cnf(p1832,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p1831]) ).
cnf(p1834,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1832,c257]) ).
cnf(p1845,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| leq(n0,sk27)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1843,p1834]) ).
cnf(p1847,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1845]) ).
cnf(p1849,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1847]) ).
cnf(p1936,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1935,p1849]) ).
cnf(p1938,plain,
( leq(n0,sk29)
| leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1936]) ).
cnf(p1940,plain,
( leq(n0,sk29)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1938]) ).
cnf(p1944,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,n3)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1940,c256]) ).
cnf(c268,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1694,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c268]) ).
cnf(p1740,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1694]) ).
cnf(p1786,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1740]) ).
cnf(p1850,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1786]) ).
cnf(p1851,plain,
( init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1850]) ).
cnf(p1852,plain,
( leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p1851]) ).
cnf(p1949,plain,
( leq(n0,sk30)
| leq(n0,sk27)
| a_select2(s_values7_init,sk29) = init
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1944,p1852]) ).
cnf(p1965,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) = init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1949]) ).
cnf(p1975,plain,
( leq(n0,sk30)
| leq(n0,sk27)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1974,p1965]) ).
cnf(p1976,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1975]) ).
cnf(p1978,plain,
( leq(n0,sk30)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1976]) ).
cnf(p1980,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1978,c257]) ).
cnf(c270,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1695,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c270]) ).
cnf(p1741,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1695]) ).
cnf(p1787,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1741]) ).
cnf(p1854,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1787]) ).
cnf(p1855,plain,
( init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1854]) ).
cnf(p1856,plain,
( leq(sk30,n2)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p1855]) ).
cnf(p1987,plain,
( leq(sk29,n3)
| leq(n0,sk27)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1980,p1856]) ).
cnf(p1991,plain,
( leq(sk29,n3)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1987]) ).
cnf(c272,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1696,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c272]) ).
cnf(p1742,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1696]) ).
cnf(p1788,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1742]) ).
cnf(p1969,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1788]) ).
cnf(p1970,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1969]) ).
cnf(p1971,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p1970]) ).
cnf(p1992,plain,
( leq(sk29,n3)
| leq(n0,sk27)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1991,p1971]) ).
cnf(p1993,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1992]) ).
cnf(p1995,plain,
( leq(sk29,n3)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1993]) ).
cnf(p1997,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p1995,p1944]) ).
cnf(p2001,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1997]) ).
cnf(p2187,plain,
( leq(n0,sk27)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p2186,p2001]) ).
cnf(p2189,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p2187]) ).
cnf(c276,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1698,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1690,c276]) ).
cnf(p1744,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1736,p1698]) ).
cnf(p1790,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(demodulation,[status(thm)],[p1782,p1744]) ).
cnf(p2005,plain,
( init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p1790]) ).
cnf(p2006,plain,
( init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p2005]) ).
cnf(p2007,plain,
( leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(n0,sk27) ),
inference(equality_resolution,[status(thm)],[p2006]) ).
cnf(p2008,plain,
( leq(n0,sk27)
| leq(sk30,n2)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p2007,p2001]) ).
cnf(p2009,plain,
( leq(sk30,n2)
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p2008]) ).
cnf(p2011,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p2009,p1980]) ).
cnf(p2014,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p2011]) ).
cnf(p2190,plain,
( leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p2189,p2014]) ).
cnf(p2192,plain,
leq(n0,sk27),
inference(factoring,[status(thm)],[p2190]) ).
cnf(p2193,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| ~ leq(sk27,n2) ),
inference(resolution,[status(thm)],[p2192,c255]) ).
cnf(c280,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1700,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c280]) ).
cnf(p1746,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1700]) ).
cnf(p1792,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1746]) ).
cnf(p1859,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1792]) ).
cnf(p1860,plain,
( init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1859]) ).
cnf(p1861,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p1860]) ).
cnf(p2204,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p2193,p1861]) ).
cnf(p2256,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2247,p2204]) ).
cnf(c316,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1718,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c316]) ).
cnf(p1764,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1718]) ).
cnf(p1810,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1764]) ).
cnf(p1913,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1810]) ).
cnf(p1914,plain,
( init != init
| leq(n0,sk30)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1913]) ).
cnf(p1915,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p1914]) ).
cnf(p2261,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init ),
inference(resolution,[status(thm)],[p2256,p1915]) ).
cnf(p2262,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init ),
inference(factoring,[status(thm)],[p2261]) ).
cnf(p2264,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init ),
inference(factoring,[status(thm)],[p2262]) ).
cnf(c334,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1727,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c334]) ).
cnf(p1773,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1727]) ).
cnf(p1819,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1773]) ).
cnf(p2172,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p1819]) ).
cnf(p2173,plain,
( init != init
| leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p2172]) ).
cnf(p2174,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(equality_resolution,[status(thm)],[p2173]) ).
cnf(p2265,plain,
( leq(n0,sk30)
| leq(n0,sk29)
| leq(n0,sk30)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2264,p2174]) ).
cnf(p2269,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2265]) ).
cnf(p2271,plain,
( leq(n0,sk30)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2269]) ).
cnf(p2273,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2271,c257]) ).
cnf(c282,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1701,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c282]) ).
cnf(p1747,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1701]) ).
cnf(p1793,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1747]) ).
cnf(p1863,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1793]) ).
cnf(p1864,plain,
( init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1863]) ).
cnf(p1865,plain,
( leq(sk30,n2)
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p1864]) ).
cnf(p2280,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2273,p1865]) ).
cnf(p2284,plain,
( leq(sk27,n2)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2280]) ).
cnf(c284,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1702,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c284]) ).
cnf(p1748,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1702]) ).
cnf(p1794,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1748]) ).
cnf(p2031,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1794]) ).
cnf(p2032,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2031]) ).
cnf(p2033,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p2032]) ).
cnf(p2285,plain,
( leq(n0,sk29)
| leq(sk27,n2)
| leq(sk27,n2)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2284,p2033]) ).
cnf(p2289,plain,
( leq(sk27,n2)
| leq(sk27,n2)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2285]) ).
cnf(p2291,plain,
( leq(sk27,n2)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2289]) ).
cnf(p2295,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2291,p2193]) ).
cnf(p2313,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2295,p2247]) ).
cnf(c318,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1719,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c318]) ).
cnf(p1765,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1719]) ).
cnf(p1811,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1765]) ).
cnf(p1917,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1811]) ).
cnf(p1918,plain,
( init != init
| leq(sk30,n2)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1917]) ).
cnf(p1919,plain,
( leq(sk30,n2)
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p1918]) ).
cnf(p2282,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2273,p1919]) ).
cnf(p2296,plain,
( leq(sk28,n3)
| a_select2(s_center7_init,sk30) = init
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2282]) ).
cnf(c320,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1720,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c320]) ).
cnf(p1766,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1720]) ).
cnf(p1812,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1766]) ).
cnf(p2160,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1812]) ).
cnf(p2161,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2160]) ).
cnf(p2162,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk29)
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p2161]) ).
cnf(p2297,plain,
( leq(n0,sk29)
| leq(sk28,n3)
| leq(sk28,n3)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2296,p2162]) ).
cnf(p2299,plain,
( leq(sk28,n3)
| leq(sk28,n3)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2297]) ).
cnf(p2301,plain,
( leq(sk28,n3)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2299]) ).
cnf(p2319,plain,
( leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2313,p2301]) ).
cnf(p2320,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2319]) ).
cnf(p2352,plain,
( leq(n0,sk29)
| a_select2(s_center7_init,sk30) != init
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2351,p2320]) ).
cnf(p2353,plain,
( a_select2(s_center7_init,sk30) != init
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2352]) ).
cnf(c336,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1728,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c336]) ).
cnf(p1774,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1728]) ).
cnf(p1820,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1774]) ).
cnf(p2175,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p1820]) ).
cnf(p2176,plain,
( init != init
| leq(sk30,n2)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p2175]) ).
cnf(p2177,plain,
( leq(sk30,n2)
| leq(n0,sk29)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(equality_resolution,[status(thm)],[p2176]) ).
cnf(p2321,plain,
( leq(sk30,n2)
| leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2320,p2177]) ).
cnf(p2323,plain,
( leq(sk30,n2)
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2321]) ).
cnf(p2325,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2323,p2273]) ).
cnf(p2327,plain,
( a_select2(s_center7_init,sk30) = init
| leq(n0,sk29) ),
inference(factoring,[status(thm)],[p2325]) ).
cnf(p2354,plain,
( leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p2353,p2327]) ).
cnf(p2355,plain,
leq(n0,sk29),
inference(factoring,[status(thm)],[p2354]) ).
cnf(p2359,plain,
( a_select2(s_values7_init,sk29) = init
| ~ leq(sk29,n3) ),
inference(resolution,[status(thm)],[p2355,c256]) ).
cnf(c286,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1703,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c286]) ).
cnf(p1749,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1703]) ).
cnf(p1795,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1749]) ).
cnf(p1868,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1795]) ).
cnf(p1869,plain,
( init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1868]) ).
cnf(p1870,plain,
( leq(n0,sk30)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p1869]) ).
cnf(p2364,plain,
( leq(n0,sk30)
| leq(sk27,n2)
| a_select2(s_values7_init,sk29) = init ),
inference(resolution,[status(thm)],[p2359,p1870]) ).
cnf(c292,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1706,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c292]) ).
cnf(p1752,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1706]) ).
cnf(p1798,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1752]) ).
cnf(p2040,plain,
( init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1798]) ).
cnf(p2041,plain,
( init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2040]) ).
cnf(p2042,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p2041]) ).
cnf(p2372,plain,
( leq(n0,sk30)
| leq(sk27,n2)
| leq(n0,sk30)
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p2364,p2042]) ).
cnf(p2381,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2372]) ).
cnf(p2383,plain,
( leq(n0,sk30)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2381]) ).
cnf(p2387,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p2383,p2193]) ).
cnf(p2402,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p2387,p2247]) ).
cnf(c322,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1721,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c322]) ).
cnf(p1767,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1721]) ).
cnf(p1813,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1767]) ).
cnf(p1923,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1813]) ).
cnf(p1924,plain,
( init != init
| leq(n0,sk30)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1923]) ).
cnf(p1925,plain,
( leq(n0,sk30)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p1924]) ).
cnf(p2365,plain,
( leq(n0,sk30)
| leq(sk28,n3)
| a_select2(s_values7_init,sk29) = init ),
inference(resolution,[status(thm)],[p2359,p1925]) ).
cnf(c328,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1724,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c328]) ).
cnf(p1770,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1724]) ).
cnf(p1816,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1770]) ).
cnf(p2166,plain,
( init != init
| init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1816]) ).
cnf(p2167,plain,
( init != init
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2166]) ).
cnf(p2168,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p2167]) ).
cnf(p2378,plain,
( leq(n0,sk30)
| leq(sk28,n3)
| leq(n0,sk30)
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2365,p2168]) ).
cnf(p2388,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2378]) ).
cnf(p2390,plain,
( leq(n0,sk30)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2388]) ).
cnf(p2408,plain,
( leq(n0,sk30)
| a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p2402,p2390]) ).
cnf(p2409,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p2408]) ).
cnf(p2426,plain,
( leq(n0,sk30)
| leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init ),
inference(resolution,[status(thm)],[p2425,p2409]) ).
cnf(p2427,plain,
( leq(n0,sk30)
| a_select2(s_values7_init,sk29) != init ),
inference(factoring,[status(thm)],[p2426]) ).
cnf(c340,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1730,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c340]) ).
cnf(p1776,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(n0,sk30)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1730]) ).
cnf(p1822,plain,
( init != init
| init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1776]) ).
cnf(p2178,plain,
( init != init
| init != init
| leq(n0,sk30)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p1822]) ).
cnf(p2179,plain,
( init != init
| leq(n0,sk30)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p2178]) ).
cnf(p2180,plain,
( leq(n0,sk30)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(equality_resolution,[status(thm)],[p2179]) ).
cnf(p2410,plain,
( leq(n0,sk30)
| leq(sk29,n3)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p2409,p2180]) ).
cnf(p2412,plain,
( leq(sk29,n3)
| leq(n0,sk30) ),
inference(factoring,[status(thm)],[p2410]) ).
cnf(p2414,plain,
( a_select2(s_values7_init,sk29) = init
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p2412,p2359]) ).
cnf(p2428,plain,
( leq(n0,sk30)
| leq(n0,sk30) ),
inference(resolution,[status(thm)],[p2427,p2414]) ).
cnf(p2429,plain,
leq(n0,sk30),
inference(factoring,[status(thm)],[p2428]) ).
cnf(p2431,plain,
( a_select2(s_center7_init,sk30) = init
| ~ leq(sk30,n2) ),
inference(resolution,[status(thm)],[p2429,c257]) ).
cnf(c324,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1722,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c324]) ).
cnf(p1768,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1722]) ).
cnf(p1814,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1768]) ).
cnf(p1927,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1814]) ).
cnf(p1928,plain,
( init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1927]) ).
cnf(p1929,plain,
( leq(sk30,n2)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p1928]) ).
cnf(p2439,plain,
( leq(sk29,n3)
| leq(sk28,n3)
| a_select2(s_center7_init,sk30) = init ),
inference(resolution,[status(thm)],[p2431,p1929]) ).
cnf(c326,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1723,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c326]) ).
cnf(p1769,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1723]) ).
cnf(p1815,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1769]) ).
cnf(p2163,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1815]) ).
cnf(p2164,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2163]) ).
cnf(p2165,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p2164]) ).
cnf(p2442,plain,
( leq(sk29,n3)
| leq(sk28,n3)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2439,p2165]) ).
cnf(p2481,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2442]) ).
cnf(p2483,plain,
( leq(sk29,n3)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2481]) ).
cnf(p2485,plain,
( a_select2(s_values7_init,sk29) = init
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2483,p2359]) ).
cnf(c332,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1726,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c332]) ).
cnf(p1772,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1726]) ).
cnf(p1818,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1772]) ).
cnf(p2346,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1818]) ).
cnf(p2347,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2346]) ).
cnf(p2348,plain,
( a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p2347]) ).
cnf(p2491,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk28,n3)
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2485,p2348]) ).
cnf(p2496,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2491]) ).
cnf(c330,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1725,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1690,c330]) ).
cnf(p1771,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1736,p1725]) ).
cnf(p1817,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(demodulation,[status(thm)],[p1782,p1771]) ).
cnf(p2169,plain,
( init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p1817]) ).
cnf(p2170,plain,
( init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2169]) ).
cnf(p2171,plain,
( leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk28,n3) ),
inference(equality_resolution,[status(thm)],[p2170]) ).
cnf(p2490,plain,
( leq(sk30,n2)
| leq(sk28,n3)
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2485,p2171]) ).
cnf(p2492,plain,
( leq(sk30,n2)
| leq(sk28,n3) ),
inference(factoring,[status(thm)],[p2490]) ).
cnf(p2494,plain,
( a_select2(s_center7_init,sk30) = init
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2492,p2431]) ).
cnf(p2497,plain,
( leq(sk28,n3)
| leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2496,p2494]) ).
cnf(p2498,plain,
leq(sk28,n3),
inference(factoring,[status(thm)],[p2497]) ).
cnf(c288,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1704,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c288]) ).
cnf(p1750,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1704]) ).
cnf(p1796,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1750]) ).
cnf(p1872,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1796]) ).
cnf(p1873,plain,
( init != init
| leq(sk30,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1872]) ).
cnf(p1874,plain,
( leq(sk30,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p1873]) ).
cnf(p2438,plain,
( leq(sk29,n3)
| leq(sk27,n2)
| a_select2(s_center7_init,sk30) = init ),
inference(resolution,[status(thm)],[p2431,p1874]) ).
cnf(c290,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1705,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c290]) ).
cnf(p1751,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1705]) ).
cnf(p1797,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1751]) ).
cnf(p2037,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1797]) ).
cnf(p2038,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2037]) ).
cnf(p2039,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p2038]) ).
cnf(p2440,plain,
( leq(sk29,n3)
| leq(sk27,n2)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p2438,p2039]) ).
cnf(p2445,plain,
( leq(sk29,n3)
| leq(sk29,n3)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2440]) ).
cnf(p2447,plain,
( leq(sk29,n3)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2445]) ).
cnf(p2449,plain,
( a_select2(s_values7_init,sk29) = init
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p2447,p2359]) ).
cnf(c296,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1708,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c296]) ).
cnf(p1754,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1708]) ).
cnf(p1800,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1754]) ).
cnf(p2215,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1800]) ).
cnf(p2216,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2215]) ).
cnf(p2217,plain,
( a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p2216]) ).
cnf(p2455,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk27,n2)
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p2449,p2217]) ).
cnf(p2461,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2455]) ).
cnf(c294,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1707,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1690,c294]) ).
cnf(p1753,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1736,p1707]) ).
cnf(p1799,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(demodulation,[status(thm)],[p1782,p1753]) ).
cnf(p2043,plain,
( init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p1799]) ).
cnf(p2044,plain,
( init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2043]) ).
cnf(p2045,plain,
( leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| leq(sk27,n2) ),
inference(equality_resolution,[status(thm)],[p2044]) ).
cnf(p2453,plain,
( leq(sk30,n2)
| leq(sk27,n2)
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p2449,p2045]) ).
cnf(p2457,plain,
( leq(sk30,n2)
| leq(sk27,n2) ),
inference(factoring,[status(thm)],[p2453]) ).
cnf(p2459,plain,
( a_select2(s_center7_init,sk30) = init
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p2457,p2431]) ).
cnf(p2462,plain,
( leq(sk27,n2)
| leq(sk27,n2) ),
inference(resolution,[status(thm)],[p2461,p2459]) ).
cnf(p2463,plain,
leq(sk27,n2),
inference(factoring,[status(thm)],[p2462]) ).
cnf(p2467,plain,
( a_select3(simplex7_init,X0,sk27) = init
| ~ leq(X0,n3)
| ~ leq(n0,X0) ),
inference(resolution,[status(thm)],[p2463,p2193]) ).
cnf(p2474,plain,
( a_select3(simplex7_init,sk28,sk27) = init
| ~ leq(sk28,n3) ),
inference(resolution,[status(thm)],[p2467,p2247]) ).
cnf(p2504,plain,
a_select3(simplex7_init,sk28,sk27) = init,
inference(resolution,[status(thm)],[p2498,p2474]) ).
cnf(c344,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1732,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c344]) ).
cnf(p1778,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1732]) ).
cnf(p1824,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1778]) ).
cnf(p2420,plain,
( init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p1824]) ).
cnf(p2421,plain,
( init != init
| a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p2420]) ).
cnf(p2422,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(equality_resolution,[status(thm)],[p2421]) ).
cnf(p2508,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk29,n3)
| init != init ),
inference(demodulation,[status(thm)],[p2504,p2422]) ).
cnf(p2513,plain,
( a_select2(s_center7_init,sk30) != init
| leq(sk29,n3) ),
inference(equality_resolution,[status(thm)],[p2508]) ).
cnf(c342,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1731,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c342]) ).
cnf(p1777,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1731]) ).
cnf(p1823,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1777]) ).
cnf(p2181,plain,
( init != init
| init != init
| leq(sk30,n2)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p1823]) ).
cnf(p2182,plain,
( init != init
| leq(sk30,n2)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(factoring,[status(thm)],[p2181]) ).
cnf(p2183,plain,
( leq(sk30,n2)
| leq(sk29,n3)
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(equality_resolution,[status(thm)],[p2182]) ).
cnf(p2507,plain,
( leq(sk30,n2)
| leq(sk29,n3)
| init != init ),
inference(demodulation,[status(thm)],[p2504,p2183]) ).
cnf(p2509,plain,
( leq(sk30,n2)
| leq(sk29,n3) ),
inference(equality_resolution,[status(thm)],[p2507]) ).
cnf(p2511,plain,
( a_select2(s_center7_init,sk30) = init
| leq(sk29,n3) ),
inference(resolution,[status(thm)],[p2509,p2431]) ).
cnf(p2514,plain,
( leq(sk29,n3)
| leq(sk29,n3) ),
inference(resolution,[status(thm)],[p2513,p2511]) ).
cnf(p2515,plain,
leq(sk29,n3),
inference(factoring,[status(thm)],[p2514]) ).
cnf(p2517,plain,
a_select2(s_values7_init,sk29) = init,
inference(resolution,[status(thm)],[p2515,p2359]) ).
cnf(c348,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1734,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c348]) ).
cnf(p1780,plain,
( init != init
| init != init
| pvar1400_init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1734]) ).
cnf(p1826,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1780]) ).
cnf(p2505,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| a_select2(s_values7_init,sk29) != init
| init != init ),
inference(demodulation,[status(thm)],[p2504,p1826]) ).
cnf(p2518,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| init != init
| init != init ),
inference(demodulation,[status(thm)],[p2517,p2505]) ).
cnf(p2524,plain,
( init != init
| init != init
| init != init
| leq(sk30,n2)
| init != init ),
inference(factoring,[status(thm)],[p2518]) ).
cnf(p2525,plain,
( init != init
| init != init
| leq(sk30,n2)
| init != init ),
inference(factoring,[status(thm)],[p2524]) ).
cnf(p2526,plain,
( init != init
| leq(sk30,n2)
| init != init ),
inference(factoring,[status(thm)],[p2525]) ).
cnf(p2527,plain,
( leq(sk30,n2)
| init != init ),
inference(factoring,[status(thm)],[p2526]) ).
cnf(p2528,plain,
leq(sk30,n2),
inference(equality_resolution,[status(thm)],[p2527]) ).
cnf(p2530,plain,
a_select2(s_center7_init,sk30) = init,
inference(resolution,[status(thm)],[p2528,p2431]) ).
cnf(c350,plain,
( pvar1402_init != init
| pvar1401_init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p1735,plain,
( pvar1402_init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1690,c350]) ).
cnf(p1781,plain,
( init != init
| init != init
| pvar1400_init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1736,p1735]) ).
cnf(p1827,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| a_select3(simplex7_init,sk28,sk27) != init ),
inference(demodulation,[status(thm)],[p1782,p1781]) ).
cnf(p2506,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| a_select2(s_values7_init,sk29) != init
| init != init ),
inference(demodulation,[status(thm)],[p2504,p1827]) ).
cnf(p2519,plain,
( init != init
| init != init
| init != init
| a_select2(s_center7_init,sk30) != init
| init != init
| init != init ),
inference(demodulation,[status(thm)],[p2517,p2506]) ).
cnf(p2531,plain,
( init != init
| init != init
| init != init
| init != init
| init != init
| init != init ),
inference(demodulation,[status(thm)],[p2530,p2519]) ).
cnf(p2549,plain,
( init != init
| init != init
| init != init
| init != init
| init != init ),
inference(factoring,[status(thm)],[p2531]) ).
cnf(p2550,plain,
( init != init
| init != init
| init != init
| init != init ),
inference(factoring,[status(thm)],[p2549]) ).
cnf(p2551,plain,
( init != init
| init != init
| init != init ),
inference(factoring,[status(thm)],[p2550]) ).
cnf(p2552,plain,
( init != init
| init != init ),
inference(factoring,[status(thm)],[p2551]) ).
cnf(p2553,plain,
init != init,
inference(factoring,[status(thm)],[p2552]) ).
cnf(p2554,plain,
$false,
inference(equality_resolution,[status(thm)],[p2553]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV042+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.34 % Computer : n001.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Thu Sep 24 18:28:39 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 27.86/4.42 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.86/4.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------