%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV053+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.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:12:08 PM UTC 2026
% Result : Theorem 25.68s 4.11s
% Output : Proof 25.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 2
% Syntax : Number of formulae : 98 ( 19 unt; 0 def)
% Number of atoms : 437 ( 97 equ)
% Maximal formula atoms : 21 ( 4 avg)
% Number of connectives : 593 ( 254 ~; 279 |; 50 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 14 con; 0-3 aty)
% Number of variables : 45 ( 7 sgn 27 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f52,conjecture,
( ( ! [C,D] :
( ( leq(C,minus(pv10,n1))
& leq(n0,C) )
=> sum(n0,minus(n5,n1),a_select3(q,C,D)) = n1 )
& ! [A,B] :
( ( leq(A,minus(pv12,n1))
& leq(n0,A) )
=> a_select3(q,pv10,A) = divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))))) )
& leq(pv12,minus(n5,n1))
& leq(pv10,minus(n135300,n1))
& leq(n0,pv12)
& leq(n0,pv10) )
=> ( ! [G,H] :
( ( leq(G,minus(pv10,n1))
& leq(n0,G) )
=> sum(n0,minus(n5,n1),a_select3(q,G,H)) = n1 )
& ! [E,F] :
( ( leq(E,minus(pv12,n1))
& leq(n0,E) )
=> a_select3(q,pv10,E) = divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10)))))) )
& leq(pv12,minus(n5,n1))
& leq(pv10,minus(n135300,n1))
& leq(n0,pv12)
& leq(n0,pv10)
& n0 = sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cl5_nebula_norm_0031) ).
fof(f52_neg,negated_conjecture,
~ ( ( ! [C,D] :
( ( leq(C,minus(pv10,n1))
& leq(n0,C) )
=> sum(n0,minus(n5,n1),a_select3(q,C,D)) = n1 )
& ! [A,B] :
( ( leq(A,minus(pv12,n1))
& leq(n0,A) )
=> a_select3(q,pv10,A) = divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10)))))) )
& leq(pv12,minus(n5,n1))
& leq(pv10,minus(n135300,n1))
& leq(n0,pv12)
& leq(n0,pv10) )
=> ( ! [G,H] :
( ( leq(G,minus(pv10,n1))
& leq(n0,G) )
=> sum(n0,minus(n5,n1),a_select3(q,G,H)) = n1 )
& ! [E,F] :
( ( leq(E,minus(pv12,n1))
& leq(n0,E) )
=> a_select3(q,pv10,E) = divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10)))))) )
& leq(pv12,minus(n5,n1))
& leq(pv10,minus(n135300,n1))
& leq(n0,pv12)
& leq(n0,pv10)
& n0 = sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f52_nnf,plain,
( ( ? [G,H] :
( sum(n0,minus(n5,n1),a_select3(q,G,H)) != n1
& leq(G,minus(pv10,n1))
& leq(n0,G) )
| ? [E,F] :
( a_select3(q,pv10,E) != divide(sqrt(times(minus(a_select3(center,E,n0),a_select2(x,pv10)),minus(a_select3(center,E,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,F,n0),a_select2(x,pv10)),minus(a_select3(center,F,n0),a_select2(x,pv10))))))
& leq(E,minus(pv12,n1))
& leq(n0,E) )
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) )
& ! [C,D] :
( sum(n0,minus(n5,n1),a_select3(q,C,D)) = n1
| ~ leq(C,minus(pv10,n1))
| ~ leq(n0,C) )
& ! [A,B] :
( a_select3(q,pv10,A) = divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10))))))
| ~ leq(A,minus(pv12,n1))
| ~ leq(n0,A) )
& leq(pv12,minus(n5,n1))
& leq(pv10,minus(n135300,n1))
& leq(n0,pv12)
& leq(n0,pv10) ),
inference(nnf_transformation,[status(thm)],[f52_neg]) ).
fof(f52_sk,plain,
! [A,B,C,D] :
( ( ( sum(n0,minus(n5,n1),a_select3(q,sk29,sk30)) != n1
& leq(sk29,minus(pv10,n1))
& leq(n0,sk29) )
| ( a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
& leq(sk27,minus(pv12,n1))
& leq(n0,sk27) )
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) )
& ( sum(n0,minus(n5,n1),a_select3(q,C,D)) = n1
| ~ leq(C,minus(pv10,n1))
| ~ leq(n0,C) )
& ( a_select3(q,pv10,A) = divide(sqrt(times(minus(a_select3(center,A,n0),a_select2(x,pv10)),minus(a_select3(center,A,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,B,n0),a_select2(x,pv10)),minus(a_select3(center,B,n0),a_select2(x,pv10))))))
| ~ leq(A,minus(pv12,n1))
| ~ leq(n0,A) )
& leq(pv12,minus(n5,n1))
& leq(pv10,minus(n135300,n1))
& leq(n0,pv12)
& leq(n0,pv10) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk27,sk28,sk29,sk30])],[f52_nnf]) ).
cnf(c259,plain,
( a_select3(q,pv10,X0) = divide(sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10))))))
| ~ leq(X0,minus(pv12,n1))
| ~ leq(n0,X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
fof(f38,axiom,
! [X] : minus(X,n1) = pred(X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pred_minus_1) ).
fof(f38_nnf,plain,
! [X] : minus(X,n1) = pred(X),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X] : minus(X,n1) = pred(X),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c234,plain,
minus(X0,n1) = pred(X0),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(c263,plain,
( sum(n0,minus(n5,n1),a_select3(q,sk29,sk30)) != n1
| leq(n0,sk27)
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p323,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c263]) ).
cnf(p352,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p323]) ).
cnf(c255,plain,
leq(n0,pv10),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p353,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p352,c255]) ).
cnf(c256,plain,
leq(n0,pv12),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p354,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p353,c256]) ).
cnf(c257,plain,
leq(pv10,minus(n135300,n1)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p316,plain,
leq(pv10,pred(n135300)),
inference(superposition,[status(thm)],[c234,c257]) ).
cnf(p355,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(n0,sk27)
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p354,p316]) ).
cnf(c258,plain,
leq(pv12,minus(n5,n1)),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p317,plain,
leq(pv12,pred(n5)),
inference(superposition,[status(thm)],[c234,c258]) ).
cnf(p356,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p355,p317]) ).
cnf(c262,plain,
( leq(sk29,minus(pv10,n1))
| leq(n0,sk27)
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p324,plain,
( leq(sk29,pred(pv10))
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c262]) ).
cnf(p340,plain,
( leq(sk29,pred(pv10))
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p324]) ).
cnf(p341,plain,
( leq(sk29,pred(pv10))
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p340,c255]) ).
cnf(p342,plain,
( leq(sk29,pred(pv10))
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p341,c256]) ).
cnf(p343,plain,
( leq(sk29,pred(pv10))
| leq(n0,sk27)
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p342,p316]) ).
cnf(p344,plain,
( leq(sk29,pred(pv10))
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p343,p317]) ).
cnf(c261,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p325,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c261]) ).
cnf(p329,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p325]) ).
cnf(p330,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p329,c255]) ).
cnf(p331,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p330,c256]) ).
cnf(p332,plain,
( leq(n0,sk29)
| leq(n0,sk27)
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p331,p316]) ).
cnf(p333,plain,
( leq(n0,sk29)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p332,p317]) ).
cnf(c260,plain,
( sum(n0,minus(n5,n1),a_select3(q,X2,X3)) = n1
| ~ leq(X2,minus(pv10,n1))
| ~ leq(n0,X2) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p334,plain,
( sum(n0,pred(n5),a_select3(q,sk29,X0)) = n1
| ~ leq(sk29,pred(pv10))
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p333,c260]) ).
cnf(p345,plain,
( sum(n0,pred(n5),a_select3(q,sk29,X0)) = n1
| leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p344,p334]) ).
cnf(p346,plain,
( sum(n0,pred(n5),a_select3(q,sk29,X0)) = n1
| leq(n0,sk27) ),
inference(factoring,[status(thm)],[p345]) ).
cnf(p357,plain,
( leq(n0,sk27)
| leq(n0,sk27) ),
inference(resolution,[status(thm)],[p356,p346]) ).
cnf(p358,plain,
leq(n0,sk27),
inference(factoring,[status(thm)],[p357]) ).
cnf(p416,plain,
( a_select3(q,pv10,sk27) = divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10))))))
| ~ leq(sk27,pred(pv12)) ),
inference(resolution,[status(thm)],[c259,p358]) ).
cnf(c264,plain,
( leq(n0,sk29)
| leq(sk27,minus(pv12,n1))
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p322,plain,
( leq(n0,sk29)
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c264]) ).
cnf(p335,plain,
( leq(n0,sk29)
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p322]) ).
cnf(p336,plain,
( leq(n0,sk29)
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p335,c255]) ).
cnf(p337,plain,
( leq(n0,sk29)
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p336,c256]) ).
cnf(p338,plain,
( leq(n0,sk29)
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p337,p316]) ).
cnf(p339,plain,
( leq(n0,sk29)
| leq(sk27,pred(pv12)) ),
inference(resolution,[status(thm)],[p338,p317]) ).
cnf(p417,plain,
( leq(n0,sk29)
| a_select3(q,pv10,sk27) = divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))))) ),
inference(resolution,[status(thm)],[p416,p339]) ).
cnf(c267,plain,
( leq(n0,sk29)
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p319,plain,
( leq(n0,sk29)
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c267]) ).
cnf(p365,plain,
( leq(n0,sk29)
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p319]) ).
cnf(p366,plain,
( leq(n0,sk29)
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p365,c255]) ).
cnf(p367,plain,
( leq(n0,sk29)
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p366,c256]) ).
cnf(p368,plain,
( leq(n0,sk29)
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p367,p316]) ).
cnf(p369,plain,
( leq(n0,sk29)
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10)))))) ),
inference(resolution,[status(thm)],[p368,p317]) ).
cnf(p418,plain,
( leq(n0,sk29)
| leq(n0,sk29) ),
inference(resolution,[status(thm)],[p417,p369]) ).
cnf(p421,plain,
leq(n0,sk29),
inference(factoring,[status(thm)],[p418]) ).
cnf(p422,plain,
( sum(n0,pred(n5),a_select3(q,sk29,X0)) = n1
| ~ leq(sk29,pred(pv10)) ),
inference(resolution,[status(thm)],[p421,c260]) ).
cnf(c265,plain,
( leq(sk29,minus(pv10,n1))
| leq(sk27,minus(pv12,n1))
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p321,plain,
( leq(sk29,pred(pv10))
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c265]) ).
cnf(p347,plain,
( leq(sk29,pred(pv10))
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p321]) ).
cnf(p348,plain,
( leq(sk29,pred(pv10))
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p347,c255]) ).
cnf(p349,plain,
( leq(sk29,pred(pv10))
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p348,c256]) ).
cnf(p350,plain,
( leq(sk29,pred(pv10))
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p349,p316]) ).
cnf(p351,plain,
( leq(sk29,pred(pv10))
| leq(sk27,pred(pv12)) ),
inference(resolution,[status(thm)],[p350,p317]) ).
cnf(p424,plain,
( leq(sk27,pred(pv12))
| sum(n0,pred(n5),a_select3(q,sk29,X0)) = n1 ),
inference(resolution,[status(thm)],[p422,p351]) ).
cnf(c266,plain,
( sum(n0,minus(n5,n1),a_select3(q,sk29,sk30)) != n1
| leq(sk27,minus(pv12,n1))
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p320,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c266]) ).
cnf(p360,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p320]) ).
cnf(p361,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p360,c255]) ).
cnf(p362,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p361,c256]) ).
cnf(p363,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(sk27,pred(pv12))
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p362,p316]) ).
cnf(p364,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| leq(sk27,pred(pv12)) ),
inference(resolution,[status(thm)],[p363,p317]) ).
cnf(p425,plain,
( leq(sk27,pred(pv12))
| leq(sk27,pred(pv12)) ),
inference(resolution,[status(thm)],[p424,p364]) ).
cnf(p426,plain,
leq(sk27,pred(pv12)),
inference(factoring,[status(thm)],[p425]) ).
cnf(p427,plain,
a_select3(q,pv10,sk27) = divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,X0,n0),a_select2(x,pv10)),minus(a_select3(center,X0,n0),a_select2(x,pv10)))))),
inference(resolution,[status(thm)],[p426,p416]) ).
cnf(c268,plain,
( leq(sk29,minus(pv10,n1))
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p318,plain,
( leq(sk29,pred(pv10))
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c268]) ).
cnf(p370,plain,
( leq(sk29,pred(pv10))
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p318]) ).
cnf(p371,plain,
( leq(sk29,pred(pv10))
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p370,c255]) ).
cnf(p372,plain,
( leq(sk29,pred(pv10))
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p371,c256]) ).
cnf(p373,plain,
( leq(sk29,pred(pv10))
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p372,p316]) ).
cnf(p374,plain,
( leq(sk29,pred(pv10))
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10)))))) ),
inference(resolution,[status(thm)],[p373,p317]) ).
cnf(p428,plain,
leq(sk29,pred(pv10)),
inference(resolution,[status(thm)],[p427,p374]) ).
cnf(p430,plain,
sum(n0,pred(n5),a_select3(q,sk29,X0)) = n1,
inference(resolution,[status(thm)],[p428,p422]) ).
cnf(c269,plain,
( sum(n0,minus(n5,n1),a_select3(q,sk29,sk30)) != n1
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,minus(n5,n1),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,minus(n5,n1))
| ~ leq(pv10,minus(n135300,n1))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != sum(n0,minus(n0,n1),sqrt(times(minus(a_select3(center,pv71,n0),a_select2(x,pv10)),minus(a_select3(center,pv71,n0),a_select2(x,pv10))))) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(p375,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10)
| n0 != n0 ),
inference(superposition,[status(thm)],[c234,c269]) ).
cnf(p376,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12)
| ~ leq(n0,pv10) ),
inference(equality_resolution,[status(thm)],[p375]) ).
cnf(p377,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300))
| ~ leq(n0,pv12) ),
inference(resolution,[status(thm)],[p376,c255]) ).
cnf(p378,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5))
| ~ leq(pv10,pred(n135300)) ),
inference(resolution,[status(thm)],[p377,c256]) ).
cnf(p379,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10))))))
| ~ leq(pv12,pred(n5)) ),
inference(resolution,[status(thm)],[p378,p316]) ).
cnf(p380,plain,
( sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1
| a_select3(q,pv10,sk27) != divide(sqrt(times(minus(a_select3(center,sk27,n0),a_select2(x,pv10)),minus(a_select3(center,sk27,n0),a_select2(x,pv10)))),sum(n0,pred(n5),sqrt(times(minus(a_select3(center,sk28,n0),a_select2(x,pv10)),minus(a_select3(center,sk28,n0),a_select2(x,pv10)))))) ),
inference(resolution,[status(thm)],[p379,p317]) ).
cnf(p429,plain,
sum(n0,pred(n5),a_select3(q,sk29,sk30)) != n1,
inference(resolution,[status(thm)],[p427,p380]) ).
cnf(p431,plain,
n1 != n1,
inference(demodulation,[status(thm)],[p430,p429]) ).
cnf(p432,plain,
$false,
inference(equality_resolution,[status(thm)],[p431]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV053+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 18:24:34 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 25.68/4.11 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.68/4.11 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------