%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUM283-1.005 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Thu Sep 24 01:38:52 PM UTC 2026
% Result : Unsatisfiable 8.33s 6.57s
% Output : CNFRefutation 8.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 152
% Number of leaves : 7
% Syntax : Number of formulae : 166 ( 35 unt; 0 def)
% Number of atoms : 448 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 715 ( 433 ~; 282 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 97 ( 21 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-1 aty)
% Number of variables : 450 ( 450 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : sum(X,n0,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( sum(X,s(Y),s(Z))
| ~ sum(X,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : product(s(n0),X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [R,Y,Z,X] :
( product(s(X),Y,Z)
| ~ product(X,Y,R)
| ~ sum(R,Y,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,axiom,
factorial(n0,s(n0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Z,Y] :
( factorial(s(X),Y)
| ~ product(s(X),Z,Y)
| ~ factorial(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
! [Result] : ~ factorial(s(s(s(s(s(n0))))),Result),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,plain,
! [X0] : sum(X0,n0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f9,plain,
! [X0,X1,X2] :
( sum(X0,s(X1),s(X2))
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f10,plain,
! [X0] : product(s(n0),X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f11,plain,
! [Y,Z,X] :
( product(s(X),Y,Z)
| ! [R] :
( ~ product(X,Y,R)
| ~ sum(R,Y,Z) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f12,plain,
! [X0,X1,X2,X3] :
( product(s(X3),X1,X2)
| ~ product(X3,X1,X0)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f13,plain,
factorial(n0,s(n0)),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f14,plain,
! [X,Y] :
( factorial(s(X),Y)
| ! [Z] :
( ~ product(s(X),Z,Y)
| ~ factorial(X,Z) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f15,plain,
! [X0,X1,X2] :
( factorial(s(X0),X2)
| ~ product(s(X0),X1,X2)
| ~ factorial(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f16,plain,
! [X0] : ~ factorial(s(s(s(s(s(n0))))),X0),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f17,plain,
! [X0,X1] :
( ~ product(s(s(s(s(s(n0))))),X0,X1)
| ~ factorial(s(s(s(s(n0)))),X0) ),
inference(resolution,[status(thm)],[f15,f16]) ).
fof(f18,plain,
! [X0,X1,X2] :
( ~ product(s(s(s(s(n0)))),X2,X0)
| ~ factorial(s(s(s(n0))),X2)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f17,f15]) ).
fof(f19,plain,
! [X0,X1,X2,X3] :
( ~ product(s(s(s(n0))),X3,X2)
| ~ factorial(s(s(n0)),X3)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f18,f15]) ).
fof(f20,plain,
! [X0,X1,X2,X3,X4] :
( ~ product(s(s(n0)),X4,X3)
| ~ factorial(s(n0),X4)
| ~ product(s(s(s(n0))),X3,X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f19,f15]) ).
fof(f21,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ product(s(n0),X5,X4)
| ~ factorial(n0,X5)
| ~ product(s(s(n0)),X4,X3)
| ~ product(s(s(s(n0))),X3,X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f20,f15]) ).
fof(f22,plain,
! [X0,X1,X2,X3,X4] :
( ~ product(s(n0),s(n0),X4)
| ~ product(s(s(n0)),X4,X3)
| ~ product(s(s(s(n0))),X3,X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f21,f13]) ).
fof(f23,plain,
! [X0,X1,X2,X3] :
( ~ product(s(s(n0)),s(n0),X3)
| ~ product(s(s(s(n0))),X3,X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f22,f10]) ).
fof(f25,plain,
! [X0,X1,X2,X3,X4] :
( ~ product(s(n0),s(n0),X4)
| ~ sum(X4,s(n0),X3)
| ~ product(s(s(s(n0))),X3,X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f23,f12]) ).
fof(f26,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(n0),s(n0),X3)
| ~ product(s(s(s(n0))),X3,X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f25,f10]) ).
fof(f28,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(n0),n0,X3)
| ~ product(s(s(s(n0))),s(X3),X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f26,f9]) ).
fof(f29,plain,
! [X0,X1,X2] :
( ~ product(s(s(s(n0))),s(s(n0)),X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f28,f8]) ).
fof(f30,plain,
! [X0,X1,X2,X3] :
( ~ product(s(s(n0)),s(s(n0)),X3)
| ~ sum(X3,s(s(n0)),X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f29,f12]) ).
fof(f31,plain,
! [X0,X1,X2,X3,X4] :
( ~ product(s(n0),s(s(n0)),X4)
| ~ sum(X4,s(s(n0)),X3)
| ~ sum(X3,s(s(n0)),X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f30,f12]) ).
fof(f32,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(n0)),s(s(n0)),X3)
| ~ sum(X3,s(s(n0)),X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f31,f10]) ).
fof(f34,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(n0)),s(n0),X3)
| ~ sum(s(X3),s(s(n0)),X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f32,f9]) ).
fof(f35,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(n0)),n0,X3)
| ~ sum(s(s(X3)),s(s(n0)),X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f34,f9]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(n0)))),s(s(n0)),X2)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f35,f8]) ).
fof(f37,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(n0)))),s(n0),X2)
| ~ product(s(s(s(s(n0)))),s(X2),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f36,f9]) ).
fof(f38,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(n0)))),n0,X2)
| ~ product(s(s(s(s(n0)))),s(s(X2)),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f37,f9]) ).
fof(f39,plain,
! [X0,X1] :
( ~ product(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f38,f8]) ).
fof(f40,plain,
! [X0,X1,X2] :
( ~ product(s(s(s(n0))),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f39,f12]) ).
fof(f41,plain,
! [X0,X1,X2,X3] :
( ~ product(s(s(n0)),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(X3,s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f40,f12]) ).
fof(f42,plain,
! [X0,X1,X2,X3,X4] :
( ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ sum(X4,s(s(s(s(s(s(n0)))))),X3)
| ~ sum(X3,s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f41,f12]) ).
fof(f43,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(X3,s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f42,f10]) ).
fof(f45,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0))))),X3)
| ~ sum(s(X3),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f43,f9]) ).
fof(f46,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(s(s(s(n0)))),X3)
| ~ sum(s(s(X3)),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f45,f9]) ).
fof(f47,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(s(s(n0))),X3)
| ~ sum(s(s(s(X3))),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f46,f9]) ).
fof(f48,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),X3)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f47,f9]) ).
fof(f49,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X3)
| ~ sum(s(s(s(s(s(X3))))),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f48,f9]) ).
fof(f50,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(n0)))))),n0,X3)
| ~ sum(s(s(s(s(s(s(X3)))))),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f49,f9]) ).
fof(f51,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f50,f8]) ).
fof(f52,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(s(n0))))),X2)
| ~ sum(s(X2),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f51,f9]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(s(n0)))),X2)
| ~ sum(s(s(X2)),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f52,f9]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(s(n0))),X2)
| ~ sum(s(s(s(X2))),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f53,f9]) ).
fof(f55,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(s(n0)),X2)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f54,f9]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),s(n0),X2)
| ~ sum(s(s(s(s(s(X2))))),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f55,f9]) ).
fof(f57,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),n0,X2)
| ~ sum(s(s(s(s(s(s(X2)))))),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f56,f9]) ).
fof(f58,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(s(s(s(s(n0))))),X0,X1) ),
inference(resolution,[status(thm)],[f57,f8]) ).
fof(f59,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(s(s(s(s(n0))))),X0)
| ~ product(s(s(s(s(s(n0))))),s(X0),X1) ),
inference(resolution,[status(thm)],[f58,f9]) ).
fof(f60,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(s(s(s(n0)))),X0)
| ~ product(s(s(s(s(s(n0))))),s(s(X0)),X1) ),
inference(resolution,[status(thm)],[f59,f9]) ).
fof(f61,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(s(s(n0))),X0)
| ~ product(s(s(s(s(s(n0))))),s(s(s(X0))),X1) ),
inference(resolution,[status(thm)],[f60,f9]) ).
fof(f62,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(s(n0)),X0)
| ~ product(s(s(s(s(s(n0))))),s(s(s(s(X0)))),X1) ),
inference(resolution,[status(thm)],[f61,f9]) ).
fof(f63,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),s(n0),X0)
| ~ product(s(s(s(s(s(n0))))),s(s(s(s(s(X0))))),X1) ),
inference(resolution,[status(thm)],[f62,f9]) ).
fof(f64,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),n0,X0)
| ~ product(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))),X1) ),
inference(resolution,[status(thm)],[f63,f9]) ).
fof(f65,plain,
! [X0] : ~ product(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0),
inference(resolution,[status(thm)],[f64,f8]) ).
fof(f66,plain,
! [X0,X1] :
( ~ product(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f65,f12]) ).
fof(f67,plain,
! [X0,X1,X2] :
( ~ product(s(s(s(n0))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f66,f12]) ).
fof(f68,plain,
! [X0,X1,X2,X3] :
( ~ product(s(s(n0)),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X3)
| ~ sum(X3,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f67,f12]) ).
fof(f69,plain,
! [X0,X1,X2,X3,X4] :
( ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X4)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X3)
| ~ sum(X3,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f68,f12]) ).
fof(f70,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X3)
| ~ sum(X3,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f69,f10]) ).
fof(f72,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))),X3)
| ~ sum(s(X3),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f70,f9]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))),X3)
| ~ sum(s(s(X3)),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f72,f9]) ).
fof(f74,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))),X3)
| ~ sum(s(s(s(X3))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f73,f9]) ).
fof(f75,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))),X3)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f74,f9]) ).
fof(f76,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))),X3)
| ~ sum(s(s(s(s(s(X3))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f75,f9]) ).
fof(f77,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),X3)
| ~ sum(s(s(s(s(s(s(X3)))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f76,f9]) ).
fof(f78,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(X3))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f77,f9]) ).
fof(f79,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(X3)))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f78,f9]) ).
fof(f80,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(X3))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f79,f9]) ).
fof(f81,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(X3)))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f80,f9]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f81,f9]) ).
fof(f83,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f82,f9]) ).
fof(f84,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f83,f9]) ).
fof(f85,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(n0)))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f84,f9]) ).
fof(f86,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(n0))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f85,f9]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(n0)))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f86,f9]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(s(n0))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f87,f9]) ).
fof(f89,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f88,f9]) ).
fof(f90,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(s(n0))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f89,f9]) ).
fof(f91,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(s(n0)))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f90,f9]) ).
fof(f92,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(s(n0))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f91,f9]) ).
fof(f93,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(s(n0)),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f92,f9]) ).
fof(f94,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),s(n0),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f93,f9]) ).
fof(f95,plain,
! [X0,X1,X2,X3] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),n0,X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f94,f9]) ).
fof(f96,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f95,f8]) ).
fof(f97,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))),X2)
| ~ sum(s(X2),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f96,f9]) ).
fof(f98,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))),X2)
| ~ sum(s(s(X2)),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f97,f9]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))),X2)
| ~ sum(s(s(s(X2))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f98,f9]) ).
fof(f100,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))),X2)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f99,f9]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))),X2)
| ~ sum(s(s(s(s(s(X2))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f100,f9]) ).
fof(f102,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(X2)))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f101,f9]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(X2))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f102,f9]) ).
fof(f104,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(X2)))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f103,f9]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(X2))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f104,f9]) ).
fof(f106,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(X2)))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f105,f9]) ).
fof(f107,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f106,f9]) ).
fof(f108,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f107,f9]) ).
fof(f109,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f108,f9]) ).
fof(f110,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(n0)))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f109,f9]) ).
fof(f111,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(n0))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f110,f9]) ).
fof(f112,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(n0)))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f111,f9]) ).
fof(f113,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(n0))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f112,f9]) ).
fof(f114,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f113,f9]) ).
fof(f115,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(n0))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f114,f9]) ).
fof(f116,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(n0)))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f115,f9]) ).
fof(f117,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(n0))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f116,f9]) ).
fof(f118,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(s(n0)),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f117,f9]) ).
fof(f119,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),s(n0),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f118,f9]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))),n0,X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f119,f9]) ).
fof(f121,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f120,f8]) ).
fof(f122,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))),X0)
| ~ sum(s(X0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f121,f9]) ).
fof(f123,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))),X0)
| ~ sum(s(s(X0)),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f122,f9]) ).
fof(f124,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))),X0)
| ~ sum(s(s(s(X0))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f123,f9]) ).
fof(f125,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))),X0)
| ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f124,f9]) ).
fof(f126,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))),X0)
| ~ sum(s(s(s(s(s(X0))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f125,f9]) ).
fof(f127,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),X0)
| ~ sum(s(s(s(s(s(s(X0)))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f126,f9]) ).
fof(f128,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(X0))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f127,f9]) ).
fof(f129,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(X0)))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f128,f9]) ).
fof(f130,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(X0))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f129,f9]) ).
fof(f131,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(X0)))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f130,f9]) ).
fof(f132,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f131,f9]) ).
fof(f133,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f132,f9]) ).
fof(f134,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f133,f9]) ).
fof(f135,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(n0)))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f134,f9]) ).
fof(f136,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(n0))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f135,f9]) ).
fof(f137,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f136,f9]) ).
fof(f138,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(n0))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f137,f9]) ).
fof(f139,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(n0)))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f138,f9]) ).
fof(f140,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(n0))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f139,f9]) ).
fof(f141,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(n0)))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f140,f9]) ).
fof(f142,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(n0))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f141,f9]) ).
fof(f143,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(n0)),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f142,f9]) ).
fof(f144,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(n0),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f143,f9]) ).
fof(f145,plain,
! [X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),n0,X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X1) ),
inference(resolution,[status(thm)],[f144,f9]) ).
fof(f146,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))),X0),
inference(resolution,[status(thm)],[f145,f8]) ).
fof(f147,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))))),X0),
inference(resolution,[status(thm)],[f146,f9]) ).
fof(f148,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))),X0),
inference(resolution,[status(thm)],[f147,f9]) ).
fof(f149,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))))),X0),
inference(resolution,[status(thm)],[f148,f9]) ).
fof(f150,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))),X0),
inference(resolution,[status(thm)],[f149,f9]) ).
fof(f151,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))))),X0),
inference(resolution,[status(thm)],[f150,f9]) ).
fof(f152,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))),X0),
inference(resolution,[status(thm)],[f151,f9]) ).
fof(f153,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))))),X0),
inference(resolution,[status(thm)],[f152,f9]) ).
fof(f154,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))),X0),
inference(resolution,[status(thm)],[f153,f9]) ).
fof(f155,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))))),X0),
inference(resolution,[status(thm)],[f154,f9]) ).
fof(f156,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))),X0),
inference(resolution,[status(thm)],[f155,f9]) ).
fof(f157,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(s(n0))))))))))))),X0),
inference(resolution,[status(thm)],[f156,f9]) ).
fof(f158,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))),X0),
inference(resolution,[status(thm)],[f157,f9]) ).
fof(f159,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(s(n0))))))))))),X0),
inference(resolution,[status(thm)],[f158,f9]) ).
fof(f160,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(s(n0)))))))))),X0),
inference(resolution,[status(thm)],[f159,f9]) ).
fof(f161,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(s(n0))))))))),X0),
inference(resolution,[status(thm)],[f160,f9]) ).
fof(f162,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(s(n0)))))))),X0),
inference(resolution,[status(thm)],[f161,f9]) ).
fof(f163,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(s(n0))))))),X0),
inference(resolution,[status(thm)],[f162,f9]) ).
fof(f164,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(s(n0)))))),X0),
inference(resolution,[status(thm)],[f163,f9]) ).
fof(f165,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(s(n0))))),X0),
inference(resolution,[status(thm)],[f164,f9]) ).
fof(f166,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(s(n0)))),X0),
inference(resolution,[status(thm)],[f165,f9]) ).
fof(f167,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(s(n0))),X0),
inference(resolution,[status(thm)],[f166,f9]) ).
fof(f168,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(s(n0)),X0),
inference(resolution,[status(thm)],[f167,f9]) ).
fof(f169,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),s(n0),X0),
inference(resolution,[status(thm)],[f168,f9]) ).
fof(f170,plain,
! [X0] : ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(n0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),n0,X0),
inference(resolution,[status(thm)],[f169,f9]) ).
fof(f171,plain,
$false,
inference(resolution,[status(thm)],[f170,f8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM283-1.005 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/5.43 % Computer : n015.cluster.edu
% 0.15/5.43 % Model : x86_64 x86_64
% 0.15/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.43 % Memory : 8046.5625MB
% 0.15/5.43 % OS : Linux 6.8.0-71-generic
% 0.15/5.43 % CPULimit : 300
% 0.15/5.43 % WCLimit : 300
% 0.15/5.43 % DateTime : Mon Sep 21 02:23:26 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.15/5.44 % Drodi V4.1.1
% 8.33/6.57 % Refutation found
% 8.33/6.57 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 8.33/6.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.12/7.80 % Elapsed time: 2.144635 seconds
% 7.12/7.80 % CPU time: 8.404504 seconds
% 7.12/7.80 % Total memory used: 115.599 MB
% 7.12/7.80 % Net memory used: 106.578 MB
%------------------------------------------------------------------------------