%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM283-1.005 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:12:03 PM UTC 2026
% Result : Unsatisfiable 3.10s 1.60s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 150
% Number of leaves : 7
% Syntax : Number of formulae : 157 ( 6 unt; 0 def)
% Number of atoms : 1144 ( 0 equ)
% Maximal formula atoms : 15 ( 7 avg)
% Number of connectives : 2124 (1137 ~; 987 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 16 avg)
% Maximal term depth : 25 ( 6 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 : 1144 (1144 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : sum(X0,n0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_0) ).
fof(f2,axiom,
! [X2,X0,X1] :
( sum(X0,s(X1),s(X2))
| ~ sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add) ).
fof(f3,axiom,
! [X0] : product(s(n0),X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',times1) ).
fof(f4,axiom,
! [X2,X3,X0,X1] :
( product(s(X3),X1,X2)
| ~ product(X3,X1,X0)
| ~ sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',times) ).
fof(f5,axiom,
factorial(n0,s(n0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',factorial_0) ).
fof(f6,axiom,
! [X2,X0,X1] :
( factorial(s(X0),X2)
| ~ product(s(X0),X1,X2)
| ~ factorial(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',factorial) ).
fof(f7,negated_conjecture,
! [X0] : ~ factorial(s(s(s(s(s(n0))))),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_factorial) ).
fof(f8,plain,
! [X0,X1] :
( ~ product(s(s(s(s(s(n0))))),X0,X1)
| ~ factorial(s(s(s(s(n0)))),X0) ),
inference(resolution,[],[f6,f7]) ).
fof(f9,plain,
! [X2,X0,X1] :
( ~ factorial(s(s(s(s(n0)))),X0)
| ~ sum(X1,X0,X2)
| ~ product(s(s(s(s(n0)))),X0,X1) ),
inference(resolution,[],[f4,f8]) ).
fof(f10,plain,
! [X2,X3,X0,X1] :
( ~ factorial(s(s(s(n0))),X3)
| ~ product(s(s(s(s(n0)))),X1,X0)
| ~ product(s(s(s(s(n0)))),X3,X1)
| ~ sum(X0,X1,X2) ),
inference(resolution,[],[f9,f6]) ).
fof(f11,plain,
! [X2,X3,X0,X1,X4] :
( ~ factorial(s(s(n0)),X4)
| ~ product(s(s(s(s(n0)))),X2,X0)
| ~ sum(X1,X0,X3)
| ~ product(s(s(s(n0))),X4,X2)
| ~ product(s(s(s(s(n0)))),X0,X1) ),
inference(resolution,[],[f10,f6]) ).
fof(f12,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ factorial(s(n0),X5)
| ~ sum(X2,X1,X3)
| ~ product(s(s(s(n0))),X4,X0)
| ~ product(s(s(s(s(n0)))),X1,X2)
| ~ product(s(s(n0)),X5,X4)
| ~ product(s(s(s(s(n0)))),X0,X1) ),
inference(resolution,[],[f11,f6]) ).
fof(f13,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ factorial(n0,X6)
| ~ product(s(s(s(n0))),X3,X4)
| ~ product(s(s(s(s(n0)))),X1,X0)
| ~ product(s(s(n0)),X5,X3)
| ~ product(s(s(s(s(n0)))),X4,X1)
| ~ product(s(n0),X6,X5)
| ~ sum(X0,X1,X2) ),
inference(resolution,[],[f12,f6]) ).
fof(f14,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(s(s(s(s(n0)))),X2,X3)
| ~ product(s(s(s(n0))),X0,X1)
| ~ product(s(s(n0)),X4,X0)
| ~ product(s(s(s(s(n0)))),X1,X2)
| ~ product(s(n0),s(n0),X4)
| ~ sum(X3,X2,X5) ),
inference(resolution,[],[f13,f5]) ).
fof(f15,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ product(s(s(s(s(n0)))),X1,X3)
| ~ product(s(s(n0)),X2,X0)
| ~ product(s(s(s(n0))),X0,X1)
| ~ product(s(n0),s(n0),X2)
| ~ sum(X4,X3,X5)
| ~ product(s(s(s(n0))),X3,X6)
| ~ sum(X6,X3,X4) ),
inference(resolution,[],[f14,f4]) ).
fof(f16,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ product(s(s(s(n0))),X1,X2)
| ~ product(s(s(n0)),X0,X1)
| ~ product(s(n0),s(n0),X0)
| ~ sum(X3,X4,X5)
| ~ product(s(s(s(n0))),X4,X6)
| ~ sum(X6,X4,X3)
| ~ product(s(s(s(n0))),X2,X7)
| ~ sum(X7,X2,X4) ),
inference(resolution,[],[f15,f4]) ).
fof(f17,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ product(s(s(s(n0))),X3,X5)
| ~ product(s(n0),s(n0),X0)
| ~ sum(X2,X3,X4)
| ~ product(s(s(n0)),X0,X1)
| ~ sum(X5,X3,X2)
| ~ product(s(s(s(n0))),X6,X7)
| ~ sum(X7,X6,X3)
| ~ product(s(s(n0)),X1,X8)
| ~ sum(X8,X1,X6) ),
inference(resolution,[],[f16,f4]) ).
fof(f18,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ product(s(s(s(n0))),X6,X7)
| ~ sum(X1,X2,X3)
| ~ product(s(s(n0)),X0,X4)
| ~ sum(X5,X2,X1)
| ~ product(s(n0),s(n0),X0)
| ~ sum(X7,X6,X2)
| ~ product(s(s(n0)),X4,X8)
| ~ sum(X8,X4,X6)
| ~ product(s(s(n0)),X2,X9)
| ~ sum(X9,X2,X5) ),
inference(resolution,[],[f17,f4]) ).
fof(f19,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ product(s(s(n0)),X3,X4)
| ~ sum(X0,X1,X2)
| ~ sum(X5,X1,X0)
| ~ product(s(n0),s(n0),X3)
| ~ sum(X6,X7,X1)
| ~ product(s(s(n0)),X4,X8)
| ~ sum(X8,X4,X7)
| ~ product(s(s(n0)),X1,X9)
| ~ sum(X9,X1,X5)
| ~ product(s(s(n0)),X7,X10)
| ~ sum(X10,X7,X6) ),
inference(resolution,[],[f18,f4]) ).
fof(f20,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ product(s(s(n0)),X7,X8)
| ~ sum(X3,X1,X0)
| ~ product(s(n0),s(n0),X4)
| ~ sum(X5,X6,X1)
| ~ sum(X0,X1,X2)
| ~ sum(X8,X7,X6)
| ~ product(s(s(n0)),X1,X9)
| ~ sum(X9,X1,X3)
| ~ product(s(s(n0)),X6,X10)
| ~ sum(X10,X6,X5)
| ~ product(s(n0),X4,X11)
| ~ sum(X11,X4,X7) ),
inference(resolution,[],[f19,f4]) ).
fof(f21,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ product(s(s(n0)),X5,X10)
| ~ product(s(n0),s(n0),X3)
| ~ sum(X4,X5,X1)
| ~ sum(X2,X1,X6)
| ~ sum(X7,X8,X5)
| ~ product(s(s(n0)),X1,X9)
| ~ sum(X9,X1,X0)
| ~ sum(X0,X1,X2)
| ~ sum(X10,X5,X4)
| ~ product(s(n0),X3,X11)
| ~ sum(X11,X3,X8)
| ~ product(s(n0),X8,X12)
| ~ sum(X12,X8,X7) ),
inference(resolution,[],[f20,f4]) ).
fof(f22,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ product(s(s(n0)),X3,X8)
| ~ sum(X1,X2,X3)
| ~ sum(X4,X3,X5)
| ~ sum(X6,X7,X2)
| ~ product(s(n0),s(n0),X0)
| ~ sum(X8,X3,X9)
| ~ sum(X9,X3,X4)
| ~ sum(X10,X2,X1)
| ~ product(s(n0),X0,X11)
| ~ sum(X11,X0,X7)
| ~ product(s(n0),X7,X12)
| ~ sum(X12,X7,X6)
| ~ product(s(n0),X2,X13)
| ~ sum(X13,X2,X10) ),
inference(resolution,[],[f21,f4]) ).
fof(f23,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ product(s(n0),s(n0),X7)
| ~ sum(X3,X2,X4)
| ~ sum(X5,X6,X1)
| ~ sum(X0,X1,X2)
| ~ sum(X8,X2,X9)
| ~ sum(X9,X2,X3)
| ~ sum(X10,X1,X0)
| ~ product(s(n0),X7,X11)
| ~ sum(X11,X7,X6)
| ~ product(s(n0),X6,X12)
| ~ sum(X12,X6,X5)
| ~ product(s(n0),X1,X13)
| ~ sum(X13,X1,X10)
| ~ product(s(n0),X2,X14)
| ~ sum(X14,X2,X8) ),
inference(resolution,[],[f22,f4]) ).
fof(f24,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ sum(X10,s(n0),X4)
| ~ sum(X3,X4,X5)
| ~ sum(X6,X5,X1)
| ~ sum(X7,X1,X8)
| ~ sum(X8,X1,X0)
| ~ sum(X9,X5,X6)
| ~ product(s(n0),s(n0),X10)
| ~ sum(X0,X1,X2)
| ~ product(s(n0),X4,X11)
| ~ sum(X11,X4,X3)
| ~ product(s(n0),X5,X12)
| ~ sum(X12,X5,X9)
| ~ product(s(n0),X1,X13)
| ~ sum(X13,X1,X7) ),
inference(resolution,[],[f23,f3]) ).
fof(f26,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ sum(X9,n0,X1)
| ~ sum(X3,X2,X4)
| ~ sum(X5,X4,X6)
| ~ sum(X6,X4,X7)
| ~ sum(X8,X2,X3)
| ~ product(s(n0),s(n0),X9)
| ~ sum(X7,X4,X10)
| ~ product(s(n0),s(X1),X11)
| ~ sum(X11,s(X1),X0)
| ~ product(s(n0),X2,X12)
| ~ sum(X12,X2,X8)
| ~ product(s(n0),X4,X13)
| ~ sum(X13,X4,X5)
| ~ sum(X0,s(X1),X2) ),
inference(resolution,[],[f24,f2]) ).
fof(f27,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(X10,s(X7),X1)
| ~ sum(X3,X2,X4)
| ~ sum(X4,X2,X5)
| ~ sum(X6,X1,X0)
| ~ product(s(n0),s(n0),X7)
| ~ sum(X5,X2,X8)
| ~ product(s(n0),s(X7),X9)
| ~ sum(X9,s(X7),X10)
| ~ product(s(n0),X1,X11)
| ~ sum(X11,X1,X6)
| ~ product(s(n0),X2,X12)
| ~ sum(X12,X2,X3)
| ~ sum(X0,X1,X2) ),
inference(resolution,[],[f26,f1]) ).
fof(f28,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(X11,s(X5),X4)
| ~ sum(X2,X1,X3)
| ~ sum(X4,s(X5),X6)
| ~ product(s(n0),s(n0),X7)
| ~ sum(X3,X1,X8)
| ~ product(s(n0),s(X7),X9)
| ~ sum(X9,s(X7),X10)
| ~ product(s(n0),s(X5),X11)
| ~ sum(X0,X1,X2)
| ~ product(s(n0),X1,X12)
| ~ sum(X12,X1,X0)
| ~ sum(X6,s(X5),X1)
| ~ sum(X10,X7,X5) ),
inference(resolution,[],[f27,f2]) ).
fof(f29,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(s(X3),s(X4),X5)
| ~ sum(X0,X1,X2)
| ~ product(s(n0),s(n0),X6)
| ~ sum(X2,X1,X7)
| ~ product(s(n0),s(X6),X8)
| ~ sum(X8,s(X6),X9)
| ~ product(s(n0),s(X4),X10)
| ~ sum(X11,X1,X0)
| ~ product(s(n0),X1,X12)
| ~ sum(X12,X1,X11)
| ~ sum(X5,s(X4),X1)
| ~ sum(X9,X6,X4)
| ~ sum(X10,X4,X3) ),
inference(resolution,[],[f28,f2]) ).
fof(f30,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(s(X11),s(X7),X1)
| ~ product(s(n0),s(n0),X3)
| ~ sum(X2,X1,X4)
| ~ product(s(n0),s(X3),X5)
| ~ sum(X5,s(X3),X6)
| ~ product(s(n0),s(X7),X8)
| ~ sum(X9,X1,X0)
| ~ product(s(n0),X1,X10)
| ~ sum(X10,X1,X9)
| ~ sum(X0,X1,X2)
| ~ sum(X6,X3,X7)
| ~ sum(X8,X7,X12)
| ~ sum(s(X12),X7,X11) ),
inference(resolution,[],[f29,f2]) ).
fof(f31,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(X1,s(X2),X3)
| ~ product(s(n0),s(n0),X0)
| ~ product(s(n0),s(X0),X4)
| ~ sum(X4,s(X0),X5)
| ~ product(s(n0),s(X6),X7)
| ~ sum(X8,s(X2),X9)
| ~ product(s(n0),s(X2),X10)
| ~ sum(X10,s(X2),X8)
| ~ sum(X9,s(X2),X1)
| ~ sum(X5,X0,X6)
| ~ sum(X7,X6,X11)
| ~ sum(s(X11),X6,X12)
| ~ sum(s(X12),X6,X2) ),
inference(resolution,[],[f30,f2]) ).
fof(f32,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(X1,s(X0),X2)
| ~ product(s(n0),s(X0),X1)
| ~ product(s(n0),s(n0),X0)
| ~ product(s(n0),s(X3),X4)
| ~ sum(X5,s(X6),X7)
| ~ product(s(n0),s(X6),X8)
| ~ sum(X8,s(X6),X5)
| ~ sum(X7,s(X6),X9)
| ~ sum(X2,X0,X3)
| ~ sum(X4,X3,X10)
| ~ sum(s(X10),X3,X11)
| ~ sum(s(X11),X3,X6)
| ~ sum(X9,X6,X12) ),
inference(resolution,[],[f31,f2]) ).
fof(f33,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(X4,s(X5),X6)
| ~ product(s(n0),s(n0),X0)
| ~ product(s(n0),s(X2),X3)
| ~ product(s(n0),s(X0),X1)
| ~ product(s(n0),s(X5),X7)
| ~ sum(X7,s(X5),X4)
| ~ sum(X6,s(X5),X8)
| ~ sum(s(X9),X0,X2)
| ~ sum(X3,X2,X10)
| ~ sum(s(X10),X2,X11)
| ~ sum(s(X11),X2,X5)
| ~ sum(X8,X5,X12)
| ~ sum(X1,X0,X9) ),
inference(resolution,[],[f32,f2]) ).
fof(f34,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(s(X7),s(X4),X8)
| ~ product(s(n0),s(X1),X2)
| ~ product(s(n0),s(X0),X3)
| ~ product(s(n0),s(X4),X5)
| ~ sum(X5,s(X4),X6)
| ~ product(s(n0),s(n0),X0)
| ~ sum(s(X9),X0,X1)
| ~ sum(X2,X1,X10)
| ~ sum(s(X10),X1,X11)
| ~ sum(s(X11),X1,X4)
| ~ sum(X8,X4,X12)
| ~ sum(X3,X0,X9)
| ~ sum(X6,X4,X7) ),
inference(resolution,[],[f33,f2]) ).
fof(f35,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ sum(X5,s(X4),X6)
| ~ product(s(n0),s(X2),X3)
| ~ product(s(n0),s(X4),X5)
| ~ product(s(n0),s(X0),X1)
| ~ product(s(n0),s(n0),X2)
| ~ sum(s(X7),X2,X0)
| ~ sum(X1,X0,X8)
| ~ sum(s(X8),X0,X9)
| ~ sum(s(X9),X0,X4)
| ~ sum(s(X10),X4,X11)
| ~ sum(X3,X2,X7)
| ~ sum(X6,X4,X12)
| ~ sum(s(X12),X4,X10) ),
inference(resolution,[],[f34,f2]) ).
fof(f36,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ product(s(n0),s(n0),X0)
| ~ product(s(n0),s(X2),X3)
| ~ product(s(n0),s(X4),X5)
| ~ product(s(n0),s(X0),X1)
| ~ sum(s(X6),X0,X4)
| ~ sum(X5,X4,X7)
| ~ sum(s(X7),X4,X8)
| ~ sum(s(X8),X4,X2)
| ~ sum(s(X9),X2,X10)
| ~ sum(X1,X0,X6)
| ~ sum(s(X11),X2,X12)
| ~ sum(s(X12),X2,X9)
| ~ sum(X3,X2,X11) ),
inference(resolution,[],[f35,f2]) ).
fof(f37,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X5),s(n0),X2)
| ~ product(s(n0),s(X2),X3)
| ~ product(s(n0),s(s(n0)),X4)
| ~ product(s(n0),s(X0),X1)
| ~ sum(X3,X2,X6)
| ~ sum(s(X6),X2,X7)
| ~ sum(s(X7),X2,X0)
| ~ sum(s(X8),X0,X9)
| ~ sum(X4,s(n0),X5)
| ~ sum(s(X10),X0,X11)
| ~ sum(s(X11),X0,X8)
| ~ sum(X1,X0,X10) ),
inference(resolution,[],[f36,f3]) ).
fof(f39,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X9),n0,X0)
| ~ product(s(n0),s(s(n0)),X2)
| ~ product(s(n0),s(X3),X4)
| ~ sum(X1,s(X0),X5)
| ~ sum(s(X5),s(X0),X6)
| ~ sum(s(X6),s(X0),X3)
| ~ sum(s(X7),X3,X8)
| ~ sum(X2,s(n0),X9)
| ~ sum(s(X10),X3,X11)
| ~ sum(s(X11),X3,X7)
| ~ sum(X4,X3,X10)
| ~ product(s(n0),s(s(X0)),X1) ),
inference(resolution,[],[f37,f2]) ).
fof(f40,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X5),s(s(X4)),X6)
| ~ product(s(n0),s(X1),X2)
| ~ sum(X3,s(s(X4)),X5)
| ~ product(s(n0),s(s(n0)),X0)
| ~ sum(s(X6),s(s(X4)),X1)
| ~ sum(s(X7),X1,X8)
| ~ sum(X0,s(n0),X4)
| ~ sum(s(X9),X1,X10)
| ~ sum(s(X10),X1,X7)
| ~ sum(X2,X1,X9)
| ~ product(s(n0),s(s(s(X4))),X3) ),
inference(resolution,[],[f39,f1]) ).
fof(f41,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(s(X6)),s(s(X3)),X0)
| ~ sum(X2,s(s(X3)),X4)
| ~ product(s(n0),s(s(n0)),X5)
| ~ product(s(n0),s(X0),X1)
| ~ sum(s(X7),X0,X8)
| ~ sum(X5,s(n0),X3)
| ~ sum(s(X9),X0,X10)
| ~ sum(s(X10),X0,X7)
| ~ sum(X1,X0,X9)
| ~ product(s(n0),s(s(s(X3))),X2)
| ~ sum(s(X4),s(X3),X6) ),
inference(resolution,[],[f40,f2]) ).
fof(f42,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(s(X10)),s(X1),X4)
| ~ product(s(n0),s(s(n0)),X3)
| ~ product(s(n0),s(s(X4)),X5)
| ~ sum(s(X6),s(X4),X7)
| ~ sum(X3,s(n0),X1)
| ~ sum(s(X8),s(X4),X9)
| ~ sum(s(X9),s(X4),X6)
| ~ sum(X5,s(X4),X8)
| ~ product(s(n0),s(s(s(X1))),X0)
| ~ sum(s(X2),s(X1),X10)
| ~ sum(X0,s(s(X1)),X2) ),
inference(resolution,[],[f41,f2]) ).
fof(f43,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X9),s(X5),X10)
| ~ product(s(n0),s(s(s(X1))),X2)
| ~ sum(s(X3),s(s(X1)),X4)
| ~ sum(X0,s(n0),X5)
| ~ sum(s(X6),s(s(X1)),X7)
| ~ sum(s(X7),s(s(X1)),X3)
| ~ sum(X2,s(s(X1)),X6)
| ~ product(s(n0),s(s(s(X5))),X8)
| ~ product(s(n0),s(s(n0)),X0)
| ~ sum(X8,s(s(X5)),X9)
| ~ sum(s(s(X10)),X5,X1) ),
inference(resolution,[],[f42,f2]) ).
fof(f44,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X2),s(s(X0)),X3)
| ~ product(s(n0),s(s(s(X0))),X1)
| ~ sum(X4,s(n0),X5)
| ~ sum(s(X6),s(s(X0)),X7)
| ~ sum(s(X7),s(s(X0)),X2)
| ~ sum(X1,s(s(X0)),X6)
| ~ product(s(n0),s(s(s(X5))),X8)
| ~ product(s(n0),s(s(n0)),X4)
| ~ sum(X8,s(s(X5)),X9)
| ~ sum(s(s(s(X10))),X5,X0)
| ~ sum(s(X9),X5,X10) ),
inference(resolution,[],[f43,f2]) ).
fof(f45,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X6),s(X0),X10)
| ~ sum(X2,s(n0),X3)
| ~ sum(s(X4),s(s(X0)),X5)
| ~ sum(s(X5),s(s(X0)),X6)
| ~ sum(X1,s(s(X0)),X4)
| ~ product(s(n0),s(s(s(X3))),X7)
| ~ product(s(n0),s(s(n0)),X2)
| ~ sum(X7,s(s(X3)),X8)
| ~ sum(s(s(s(X9))),X3,X0)
| ~ sum(s(X8),X3,X9)
| ~ product(s(n0),s(s(s(X0))),X1) ),
inference(resolution,[],[f44,f2]) ).
fof(f46,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X2),s(s(X3)),X4)
| ~ sum(X0,s(n0),X1)
| ~ sum(s(X4),s(s(X3)),X5)
| ~ sum(X6,s(s(X3)),X2)
| ~ product(s(n0),s(s(s(X1))),X7)
| ~ product(s(n0),s(s(n0)),X0)
| ~ sum(X7,s(s(X1)),X8)
| ~ sum(s(s(s(X9))),X1,X3)
| ~ sum(s(X8),X1,X9)
| ~ product(s(n0),s(s(s(X3))),X6)
| ~ sum(s(X5),X3,X10) ),
inference(resolution,[],[f45,f2]) ).
fof(f47,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(s(X2)),s(s(X3)),X4)
| ~ sum(X0,s(n0),X1)
| ~ sum(X5,s(s(X3)),X6)
| ~ product(s(n0),s(s(s(X1))),X7)
| ~ product(s(n0),s(s(n0)),X0)
| ~ sum(X7,s(s(X1)),X8)
| ~ sum(s(s(s(X9))),X1,X3)
| ~ sum(s(X8),X1,X9)
| ~ product(s(n0),s(s(s(X3))),X5)
| ~ sum(s(X4),X3,X10)
| ~ sum(s(X6),s(X3),X2) ),
inference(resolution,[],[f46,f2]) ).
fof(f48,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(s(X10)),s(X3),X8)
| ~ sum(X2,s(s(X3)),X4)
| ~ product(s(n0),s(s(s(X1))),X5)
| ~ product(s(n0),s(s(n0)),X0)
| ~ sum(X5,s(s(X1)),X6)
| ~ sum(s(s(s(X7))),X1,X3)
| ~ sum(s(X6),X1,X7)
| ~ product(s(n0),s(s(s(X3))),X2)
| ~ sum(s(s(X8)),X3,X9)
| ~ sum(s(X4),s(X3),X10)
| ~ sum(X0,s(n0),X1) ),
inference(resolution,[],[f47,f2]) ).
fof(f49,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X2),s(X1),X10)
| ~ product(s(n0),s(s(s(X3))),X4)
| ~ product(s(n0),s(s(n0)),X5)
| ~ sum(X4,s(s(X3)),X6)
| ~ sum(s(s(s(X7))),X3,X1)
| ~ sum(s(X6),X3,X7)
| ~ product(s(n0),s(s(s(X1))),X0)
| ~ sum(s(s(s(X8))),X1,X9)
| ~ sum(X0,s(s(X1)),X2)
| ~ sum(X5,s(n0),X3)
| ~ sum(s(s(X10)),X1,X8) ),
inference(resolution,[],[f48,f2]) ).
fof(f50,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(X2,s(n0),X0)
| ~ product(s(n0),s(s(n0)),X2)
| ~ sum(X1,s(s(X0)),X3)
| ~ sum(s(s(s(X4))),X0,X5)
| ~ sum(s(X3),X0,X4)
| ~ product(s(n0),s(s(s(X5))),X6)
| ~ sum(s(s(s(X7))),X5,X8)
| ~ sum(X6,s(s(X5)),X9)
| ~ product(s(n0),s(s(s(X0))),X1)
| ~ sum(s(s(s(X10))),X5,X7)
| ~ sum(s(X9),X5,X10) ),
inference(resolution,[],[f49,f2]) ).
fof(f51,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(s(s(X4))),s(X2),X5)
| ~ sum(X1,s(s(s(X2))),X3)
| ~ product(s(n0),s(s(n0)),X0)
| ~ sum(s(X3),s(X2),X4)
| ~ product(s(n0),s(s(s(X5))),X6)
| ~ sum(s(s(s(X7))),X5,X8)
| ~ sum(X6,s(s(X5)),X9)
| ~ product(s(n0),s(s(s(s(X2)))),X1)
| ~ sum(s(s(s(X10))),X5,X7)
| ~ sum(s(X9),X5,X10)
| ~ sum(X0,n0,X2) ),
inference(resolution,[],[f50,f2]) ).
fof(f52,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(s(s(X7))),s(X5),X8)
| ~ product(s(n0),s(s(n0)),X3)
| ~ sum(s(X2),s(X1),X4)
| ~ product(s(n0),s(s(s(s(X5)))),X6)
| ~ sum(X0,s(s(s(X1))),X2)
| ~ sum(X6,s(s(s(X5))),X9)
| ~ product(s(n0),s(s(s(s(X1)))),X0)
| ~ sum(s(s(s(X10))),s(X5),X7)
| ~ sum(s(X9),s(X5),X10)
| ~ sum(X3,n0,X1)
| ~ sum(s(s(s(X4))),X1,X5) ),
inference(resolution,[],[f51,f2]) ).
fof(f53,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(s(s(X8))),s(X4),X9)
| ~ sum(s(X1),s(X2),X3)
| ~ product(s(n0),s(s(s(s(X4)))),X5)
| ~ sum(X6,s(s(s(X2))),X1)
| ~ sum(X5,s(s(s(X4))),X7)
| ~ product(s(n0),s(s(s(s(X2)))),X6)
| ~ product(s(n0),s(s(n0)),X0)
| ~ sum(s(X7),s(X4),X8)
| ~ sum(X0,n0,X2)
| ~ sum(s(s(s(X3))),X2,X4)
| ~ sum(s(s(s(X9))),X4,X10) ),
inference(resolution,[],[f52,f2]) ).
fof(f54,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X0),s(X1),X2)
| ~ product(s(n0),s(s(s(s(X3)))),X4)
| ~ sum(X5,s(s(s(X1))),X0)
| ~ sum(X4,s(s(s(X3))),X6)
| ~ product(s(n0),s(s(s(s(X1)))),X5)
| ~ product(s(n0),s(s(n0)),X7)
| ~ sum(s(X6),s(X3),X8)
| ~ sum(X7,n0,X1)
| ~ sum(s(s(s(X2))),X1,X3)
| ~ sum(s(s(s(s(X9)))),X3,X10)
| ~ sum(s(s(s(X8))),X3,X9) ),
inference(resolution,[],[f53,f2]) ).
fof(f55,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(s(X5),s(X0),X7)
| ~ sum(X2,s(s(s(X3))),X4)
| ~ sum(X1,s(s(s(X0))),X5)
| ~ product(s(n0),s(s(s(s(X3)))),X2)
| ~ product(s(n0),s(s(n0)),X6)
| ~ product(s(n0),s(s(s(s(X0)))),X1)
| ~ sum(X6,n0,X3)
| ~ sum(s(s(s(s(X8)))),X3,X0)
| ~ sum(s(s(s(s(X9)))),X0,X10)
| ~ sum(s(s(s(X7))),X0,X9)
| ~ sum(s(X4),X3,X8) ),
inference(resolution,[],[f54,f2]) ).
fof(f56,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(X6,n0,X1)
| ~ sum(X3,s(s(s(X4))),X5)
| ~ product(s(n0),s(s(s(s(X1)))),X0)
| ~ product(s(n0),s(s(n0)),X6)
| ~ product(s(n0),s(s(s(s(X4)))),X3)
| ~ sum(X0,s(s(s(X1))),X2)
| ~ sum(s(s(s(s(X7)))),X1,X4)
| ~ sum(s(s(s(s(X8)))),X4,X9)
| ~ sum(s(s(s(s(X10)))),X4,X8)
| ~ sum(s(X2),X1,X7)
| ~ sum(s(X5),X4,X10) ),
inference(resolution,[],[f55,f2]) ).
fof(f57,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(X0,s(s(s(X1))),X2)
| ~ product(s(n0),s(s(s(s(X3)))),X4)
| ~ product(s(n0),s(s(n0)),X3)
| ~ product(s(n0),s(s(s(s(X1)))),X0)
| ~ sum(X4,s(s(s(X3))),X5)
| ~ sum(s(s(s(s(X6)))),X3,X1)
| ~ sum(s(s(s(s(X7)))),X1,X8)
| ~ sum(s(s(s(s(X9)))),X1,X7)
| ~ sum(s(X5),X3,X6)
| ~ sum(s(X2),X1,X9) ),
inference(resolution,[],[f56,f1]) ).
fof(f58,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(X3,s(s(X2)),X9)
| ~ product(s(n0),s(s(n0)),X0)
| ~ product(s(n0),s(s(s(s(X2)))),X3)
| ~ sum(X1,s(s(s(X0))),X4)
| ~ sum(s(s(s(s(X5)))),X0,X2)
| ~ sum(s(s(s(s(X6)))),X2,X7)
| ~ sum(s(s(s(s(X8)))),X2,X6)
| ~ sum(s(X4),X0,X5)
| ~ sum(s(s(X9)),X2,X8)
| ~ product(s(n0),s(s(s(s(X0)))),X1) ),
inference(resolution,[],[f57,f2]) ).
fof(f59,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(X3,s(s(s(X0))),X4)
| ~ product(s(n0),s(s(s(s(X1)))),X2)
| ~ product(s(n0),s(s(n0)),X0)
| ~ sum(s(s(s(s(X5)))),X0,X1)
| ~ sum(s(s(s(s(X6)))),X1,X7)
| ~ sum(s(s(s(s(X8)))),X1,X6)
| ~ sum(s(X4),X0,X5)
| ~ sum(s(s(s(X9))),X1,X8)
| ~ product(s(n0),s(s(s(s(X0)))),X3)
| ~ sum(X2,s(X1),X9) ),
inference(resolution,[],[f58,f2]) ).
fof(f60,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(X9,s(s(X2)),X7)
| ~ product(s(n0),s(s(n0)),X2)
| ~ sum(s(s(s(s(X3)))),X2,X0)
| ~ sum(s(s(s(s(X4)))),X0,X5)
| ~ sum(s(s(s(s(X6)))),X0,X4)
| ~ sum(s(s(X7)),X2,X3)
| ~ sum(s(s(s(X8))),X0,X6)
| ~ product(s(n0),s(s(s(s(X2)))),X9)
| ~ sum(X1,s(X0),X8)
| ~ product(s(n0),s(s(s(s(X0)))),X1) ),
inference(resolution,[],[f59,f2]) ).
fof(f61,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(X8,s(X0),X6)
| ~ sum(s(s(s(s(X1)))),X0,X2)
| ~ sum(s(s(s(s(X3)))),X2,X4)
| ~ sum(s(s(s(s(X5)))),X2,X3)
| ~ sum(s(s(s(X6))),X0,X1)
| ~ sum(s(s(s(X7))),X2,X5)
| ~ product(s(n0),s(s(s(s(X0)))),X8)
| ~ sum(X9,s(X2),X7)
| ~ product(s(n0),s(s(s(s(X2)))),X9)
| ~ product(s(n0),s(s(n0)),X0) ),
inference(resolution,[],[f60,f2]) ).
fof(f62,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ sum(X9,s(X2),X7)
| ~ sum(s(s(s(s(X3)))),X2,X4)
| ~ sum(s(s(s(s(X5)))),X2,X3)
| ~ sum(s(s(s(s(X6)))),X1,X0)
| ~ sum(s(s(s(X7))),X2,X5)
| ~ product(s(n0),s(s(s(s(X1)))),X8)
| ~ sum(s(s(s(s(X0)))),X1,X2)
| ~ product(s(n0),s(s(s(s(X2)))),X9)
| ~ product(s(n0),s(s(n0)),X1)
| ~ sum(X8,X1,X6) ),
inference(resolution,[],[f61,f2]) ).
fof(f63,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ product(s(n0),s(s(n0)),X5)
| ~ sum(s(s(s(s(X3)))),X1,X0)
| ~ sum(s(s(s(s(X4)))),X5,X6)
| ~ sum(s(s(s(s(X7)))),X1,X3)
| ~ product(s(n0),s(s(s(s(X5)))),X8)
| ~ sum(s(s(s(s(X6)))),X5,X1)
| ~ product(s(n0),s(s(s(s(X1)))),X9)
| ~ sum(s(s(s(s(X0)))),X1,X2)
| ~ sum(X8,X5,X4)
| ~ sum(X9,X1,X7) ),
inference(resolution,[],[f62,f2]) ).
fof(f64,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ sum(s(s(s(s(X3)))),s(s(n0)),X4)
| ~ sum(s(s(s(s(X0)))),X1,X2)
| ~ sum(s(s(s(s(X5)))),X1,X0)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X6)
| ~ sum(s(s(s(s(X4)))),s(s(n0)),X1)
| ~ product(s(n0),s(s(s(s(X1)))),X7)
| ~ sum(s(s(s(s(X2)))),X1,X8)
| ~ sum(X6,s(s(n0)),X3)
| ~ sum(X7,X1,X5) ),
inference(resolution,[],[f63,f3]) ).
fof(f66,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ sum(s(s(s(s(s(X5))))),s(s(n0)),X1)
| ~ sum(s(s(s(s(X3)))),X1,X0)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ sum(s(s(s(s(X0)))),X1,X2)
| ~ product(s(n0),s(s(s(s(X1)))),X6)
| ~ sum(s(s(s(s(X2)))),X1,X7)
| ~ sum(X4,s(s(n0)),X8)
| ~ sum(X6,X1,X3)
| ~ sum(s(s(s(s(X8)))),s(n0),X5) ),
inference(resolution,[],[f64,f2]) ).
fof(f67,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ sum(s(s(s(s(s(X8))))),s(n0),X1)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(s(s(s(s(X2)))),s(X1),X4)
| ~ product(s(n0),s(s(s(s(s(X1))))),X5)
| ~ sum(s(s(s(s(X4)))),s(X1),X6)
| ~ sum(X3,s(s(n0)),X7)
| ~ sum(X5,s(X1),X0)
| ~ sum(s(s(s(s(X7)))),s(n0),X8)
| ~ sum(s(s(s(s(X0)))),s(X1),X2) ),
inference(resolution,[],[f66,f2]) ).
fof(f68,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ sum(s(s(s(s(s(X8))))),n0,X2)
| ~ sum(s(s(s(s(X1)))),s(s(X2)),X3)
| ~ product(s(n0),s(s(s(s(s(s(X2)))))),X4)
| ~ sum(s(s(s(s(X3)))),s(s(X2)),X5)
| ~ sum(X0,s(s(n0)),X6)
| ~ sum(X4,s(s(X2)),X7)
| ~ sum(s(s(s(s(X6)))),s(n0),X8)
| ~ sum(s(s(s(s(X7)))),s(s(X2)),X1)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f67,f2]) ).
fof(f69,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ sum(s(s(s(s(X6)))),s(n0),X1)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(X1))))))))))),X3)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(X1))))))),X4)
| ~ sum(X5,s(s(n0)),X6)
| ~ sum(X3,s(s(s(s(s(s(s(X1))))))),X7)
| ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(X1))))))),X2)
| ~ sum(s(s(s(s(X7)))),s(s(s(s(s(s(s(X1))))))),X0)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X5) ),
inference(resolution,[],[f68,f1]) ).
fof(f70,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ sum(s(s(s(s(X5)))),n0,X0)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(X0)))))))),X3)
| ~ sum(X4,s(s(n0)),X5)
| ~ sum(X1,s(s(s(s(s(s(s(s(X0)))))))),X6)
| ~ sum(s(s(s(s(X7)))),s(s(s(s(s(s(s(s(X0)))))))),X2)
| ~ sum(s(s(s(s(X6)))),s(s(s(s(s(s(s(s(X0)))))))),X7)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X1) ),
inference(resolution,[],[f69,f2]) ).
fof(f71,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ sum(s(s(s(s(X6)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X0)
| ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X4) ),
inference(resolution,[],[f70,f1]) ).
fof(f72,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(s(s(s(s(X1))))))))))),X6)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ sum(s(s(s(s(X4)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X2)
| ~ sum(X0,s(s(n0)),X1) ),
inference(resolution,[],[f71,f2]) ).
fof(f73,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X4)))),s(s(s(s(s(s(s(s(s(s(X1)))))))))),X6)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X4)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X0)
| ~ sum(X5,s(s(n0)),X1)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f72,f2]) ).
fof(f74,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(X1))))))))),X6)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X0)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X5)
| ~ sum(X4,s(s(n0)),X1)
| ~ sum(X5,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f73,f2]) ).
fof(f75,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(s(X1)))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X4)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X0)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f74,f2]) ).
fof(f76,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(X1))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X2)
| ~ sum(X0,s(s(n0)),X1)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ sum(s(s(s(s(X4)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f75,f2]) ).
fof(f77,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(X0)))))),X6)
| ~ sum(X2,s(s(n0)),X0)
| ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X3)
| ~ sum(s(s(s(s(X4)))),s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X5)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X2)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1) ),
inference(resolution,[],[f76,f2]) ).
fof(f78,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(s(s(s(X1))))),X6)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ sum(s(s(s(s(X4)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X2)
| ~ sum(X0,s(s(n0)),X1) ),
inference(resolution,[],[f77,f2]) ).
fof(f79,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X4)))),s(s(s(s(X1)))),X6)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X4)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X0)
| ~ sum(X5,s(s(n0)),X1)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f78,f2]) ).
fof(f80,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X2)))),s(s(s(X1))),X6)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X0)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X5)
| ~ sum(X4,s(s(n0)),X1)
| ~ sum(X5,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f79,f2]) ).
fof(f81,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(X1)),X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X4)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X0)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f80,f2]) ).
fof(f82,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(X1),X6)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X2)
| ~ sum(X0,s(s(n0)),X1)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ sum(s(s(s(s(X4)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f81,f2]) ).
fof(f83,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X4)))),s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X5)
| ~ sum(X2,s(s(n0)),X0)
| ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X2)
| ~ sum(s(s(s(s(X5)))),X0,X6) ),
inference(resolution,[],[f82,f2]) ).
fof(f84,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X4)))),s(s(s(s(s(s(s(s(s(s(s(X1))))))))))),X5)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X2)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0)
| ~ sum(s(s(s(s(s(X5))))),X1,X6)
| ~ sum(X0,s(s(n0)),X1) ),
inference(resolution,[],[f83,f2]) ).
fof(f85,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(X1)))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X0)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ sum(s(s(s(s(s(s(X5)))))),X1,X6)
| ~ sum(X4,s(s(n0)),X1)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f84,f2]) ).
fof(f86,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(X0))))))))),X5)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ sum(s(s(s(s(s(s(s(X5))))))),X0,X6)
| ~ sum(X4,s(s(n0)),X0)
| ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X2)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1) ),
inference(resolution,[],[f85,f2]) ).
fof(f87,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(X1)))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(X4)))))))),X1,X5)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X6,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X6)
| ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f86,f2]) ).
fof(f88,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X6)))),s(s(s(s(s(s(s(X2))))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(X1))))))))),X2,X3)
| ~ sum(X0,s(s(n0)),X2)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),X4)
| ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f87,f2]) ).
fof(f89,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X6)))),s(s(s(s(s(s(X1)))))),X0)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X4)
| ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(X0)))))))))),X1,X2) ),
inference(resolution,[],[f88,f2]) ).
fof(f90,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X4)))),s(s(s(s(s(X1))))),X5)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X2)
| ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(X5))))))))))),X1,X6)
| ~ sum(X0,s(s(n0)),X1) ),
inference(resolution,[],[f89,f2]) ).
fof(f91,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X3)))),s(s(s(s(X1)))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X0)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(X5)))))))))))),X1,X6)
| ~ sum(X4,s(s(n0)),X1)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f90,f2]) ).
fof(f92,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X3)))),s(s(s(X0))),X5)
| ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(X5))))))))))))),X0,X6)
| ~ sum(X4,s(s(n0)),X0)
| ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X2)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1) ),
inference(resolution,[],[f91,f2]) ).
fof(f93,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X2)))),s(s(X1)),X4)
| ~ product(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(X4)))))))))))))),X1,X5)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X6,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X6)
| ~ sum(s(s(s(s(X0)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f92,f2]) ).
fof(f94,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X6)))),s(X2),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))),X2,X3)
| ~ sum(X0,s(s(n0)),X2)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),X4)
| ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f93,f2]) ).
fof(f95,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X6)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1,X2)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(s(s(s(s(X6)))),X1,X0) ),
inference(resolution,[],[f94,f2]) ).
fof(f96,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X3)))),s(s(s(s(s(s(s(s(s(s(s(X1))))))))))),X6)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))),X1,X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0)
| ~ sum(s(s(s(s(s(X6))))),X1,X4)
| ~ sum(X0,s(s(n0)),X1) ),
inference(resolution,[],[f95,f2]) ).
fof(f97,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X2)))),s(s(s(s(s(s(s(s(s(s(X1)))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))),X1,X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X5)
| ~ sum(s(s(s(s(s(s(X6)))))),X1,X3)
| ~ sum(X5,s(s(n0)),X1)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f96,f2]) ).
fof(f98,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X6)))),s(s(s(s(s(s(s(s(s(X0))))))))),X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),X0,X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ sum(s(s(s(s(s(s(s(X5))))))),X0,X2)
| ~ sum(X4,s(s(n0)),X0)
| ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1) ),
inference(resolution,[],[f97,f2]) ).
fof(f99,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X6)))),s(s(s(s(s(s(s(s(X1)))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(X4)))))))),X1,X0)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X5,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1,X2) ),
inference(resolution,[],[f98,f2]) ).
fof(f100,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(s(X2))))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(X1))))))))),X2,X3)
| ~ sum(X0,s(s(n0)),X2)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))),X2,X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f99,f2]) ).
fof(f101,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(s(s(s(s(s(X1)))))),X0)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),X1,X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(X0)))))))))),X1,X2) ),
inference(resolution,[],[f100,f2]) ).
fof(f102,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X3)))),s(s(s(s(s(X1))))),X6)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))),X1,X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(X6))))))))))),X1,X4)
| ~ sum(X0,s(s(n0)),X1) ),
inference(resolution,[],[f101,f2]) ).
fof(f103,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X2)))),s(s(s(s(X1)))),X6)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))),X1,X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(X6)))))))))))),X1,X3)
| ~ sum(X5,s(s(n0)),X1)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X2) ),
inference(resolution,[],[f102,f2]) ).
fof(f104,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X6)))),s(s(s(X0))),X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),X0,X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(X5))))))))))))),X0,X2)
| ~ sum(X4,s(s(n0)),X0)
| ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1) ),
inference(resolution,[],[f103,f2]) ).
fof(f105,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X6)))),s(s(X1)),X4)
| ~ product(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(X4)))))))))))))),X1,X0)
| ~ sum(X3,s(s(n0)),X1)
| ~ sum(X5,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X6)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1,X2) ),
inference(resolution,[],[f104,f2]) ).
fof(f106,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X5)))),s(X2),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))),X2,X3)
| ~ sum(X0,s(s(n0)),X2)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))),X2,X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f105,f2]) ).
fof(f107,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(X3,s(s(n0)),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),X1,X2)
| ~ sum(X4,s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),X1,X6)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(s(s(s(s(X5)))),X1,X0) ),
inference(resolution,[],[f106,f2]) ).
fof(f108,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))),s(X1),X2)
| ~ sum(X3,s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))),X4)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))),s(X1),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X6)
| ~ sum(s(s(s(s(X4)))),s(X1),X0)
| ~ sum(X6,s(n0),X1) ),
inference(resolution,[],[f107,f2]) ).
fof(f109,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))))))))),s(X1),X4)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))),X2)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X5)
| ~ sum(s(s(s(s(X2)))),s(X1),X6)
| ~ sum(X5,s(n0),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X6)))))))))))))))),X1,X3) ),
inference(resolution,[],[f108,f2]) ).
fof(f110,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X2)))),s(X0),X4)
| ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))),X2)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))),X1)
| ~ sum(X3,s(n0),X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))),X0,X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X5))))))))))))))))),X0,X6) ),
inference(resolution,[],[f109,f2]) ).
fof(f111,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(X3,s(n0),X1)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4))))))))))))))))),X1,X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X5))))))))))))))))),X1,X6)
| ~ sum(s(s(s(s(X2)))),X1,X4) ),
inference(resolution,[],[f110,f2]) ).
fof(f112,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4))))))))))))))))),s(X1),X5)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))),X3)
| ~ product(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(X5))))))))))))))))),s(X1),X6)
| ~ sum(s(s(s(s(X3)))),s(X1),X4)
| ~ sum(X0,n0,X1) ),
inference(resolution,[],[f111,f2]) ).
fof(f113,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))))),s(X0),X5)
| ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))),X2)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1)
| ~ sum(s(s(s(s(X2)))),s(X0),X6)
| ~ sum(X3,n0,X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X6))))))))))))))))),X0,X4) ),
inference(resolution,[],[f112,f2]) ).
fof(f114,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(s(s(s(s(X2)))),s(X1),X4)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))),X2)
| ~ sum(X3,n0,X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4))))))))))))))))),X1,X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X5)))))))))))))))))),X1,X6) ),
inference(resolution,[],[f113,f2]) ).
fof(f115,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sum(X0,n0,X1)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X2)
| ~ sum(X2,s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))),X3)
| ~ product(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(X4)))))))))))))))))),X1,X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X5)))))))))))))))))),X1,X6)
| ~ sum(s(s(s(s(X3)))),X1,X4) ),
inference(resolution,[],[f114,f2]) ).
fof(f116,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))),X2)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1)
| ~ product(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(X3)))))))))))))))))),X0,X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))))),X0,X5)
| ~ sum(s(s(s(s(X2)))),X0,X3) ),
inference(resolution,[],[f115,f1]) ).
fof(f117,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X1,s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))),X5)
| ~ product(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(X2)))))))))))))))))),X0,X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))),X0,X4)
| ~ sum(s(s(s(s(s(X5))))),X0,X2)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1) ),
inference(resolution,[],[f116,f2]) ).
fof(f118,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X5,s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X0,X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),X0,X3)
| ~ sum(s(s(s(s(s(s(X4)))))),X0,X1)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f117,f2]) ).
fof(f119,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X5,s(s(s(s(s(s(s(s(s(s(s(X1))))))))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),X1,X3)
| ~ sum(s(s(s(s(s(s(s(X4))))))),X1,X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1,X2) ),
inference(resolution,[],[f118,f2]) ).
fof(f120,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X5,s(s(s(s(s(s(s(s(s(s(X1)))))))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(X3)))))))),X1,X4)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))))),X1,X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1,X2) ),
inference(resolution,[],[f119,f2]) ).
fof(f121,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X3,s(s(s(s(s(s(s(s(s(X1))))))))),X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),X1,X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))))),X1,X5)
| ~ sum(s(s(s(s(s(s(s(s(s(X0))))))))),X1,X2) ),
inference(resolution,[],[f120,f2]) ).
fof(f122,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X1,s(s(s(s(s(s(s(s(X0)))))))),X5)
| ~ product(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(X2)))))))))))))))))),X0,X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))),X0,X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(X5)))))))))),X0,X2)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1) ),
inference(resolution,[],[f121,f2]) ).
fof(f123,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X5,s(s(s(s(s(s(s(X0))))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X0,X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),X0,X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(X4))))))))))),X0,X1)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f122,f2]) ).
fof(f124,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X5,s(s(s(s(s(s(X1)))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),X1,X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))),X1,X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1,X2) ),
inference(resolution,[],[f123,f2]) ).
fof(f125,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X5,s(s(s(s(s(X1))))),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(X3))))))))))))),X1,X4)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))))),X1,X0)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1,X2) ),
inference(resolution,[],[f124,f2]) ).
fof(f126,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X3,s(s(s(s(X1)))),X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X3)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),X1,X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))))),X1,X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))),X1,X2) ),
inference(resolution,[],[f125,f2]) ).
fof(f127,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X1,s(s(s(X0))),X5)
| ~ product(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(X2)))))))))))))))))),X0,X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))),X0,X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X5))))))))))))))),X0,X2)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1) ),
inference(resolution,[],[f126,f2]) ).
fof(f128,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X5,s(s(X0)),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X0,X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),X0,X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))),X0,X1)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f127,f2]) ).
fof(f129,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(X5,s(X1),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2)))))))))))))))))),X1,X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4))))))))))))))))),X1,X0)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X5)
| ~ product(s(n0),s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1,X2) ),
inference(resolution,[],[f128,f2]) ).
fof(f130,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ product(s(n0),s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))),X1,X4)
| ~ product(s(n0),s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),X5)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))),X1,X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))))),X1,X0)
| ~ sum(X5,X1,X3) ),
inference(resolution,[],[f129,f2]) ).
fof(f131,plain,
! [X2,X3,X0,X1,X4] :
( ~ 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(n0)))))),X1)
| ~ 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)))))))))))))))))))))))),X2)
| ~ 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(n0)))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(s(n0)))))),X3)
| ~ sum(X2,s(s(s(s(s(s(n0)))))),X0) ),
inference(resolution,[],[f130,f3]) ).
fof(f133,plain,
! [X2,X3,X0,X1,X4] :
( ~ 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(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(s(n0)))))),X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4)))))))))))))))))),s(s(s(s(s(n0))))),X3) ),
inference(resolution,[],[f131,f2]) ).
fof(f134,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X4))))))))))))))))))),s(s(s(s(s(n0))))),X0)
| ~ 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)))))))))))))))))))))))),X2)
| ~ sum(X2,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(n0))))),X4)
| ~ 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(n0)))))),X1) ),
inference(resolution,[],[f133,f2]) ).
fof(f135,plain,
! [X2,X3,X0,X1,X4] :
( ~ 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(n0)))))),X4)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(n0))))),X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ 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(n0)))),X3) ),
inference(resolution,[],[f134,f2]) ).
fof(f136,plain,
! [X2,X3,X0,X1,X4] :
( ~ 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(n0))))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(n0))))),X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ 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(n0)))),X3)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1) ),
inference(resolution,[],[f135,f2]) ).
fof(f137,plain,
! [X2,X3,X0,X1,X4] :
( ~ 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(n0)))),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)))))))))))))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))),s(s(s(s(n0)))),X3)
| ~ sum(X2,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(n0))))),X1) ),
inference(resolution,[],[f136,f2]) ).
fof(f138,plain,
! [X2,X3,X0,X1,X4] :
( ~ 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(n0))),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))),s(s(s(s(n0)))),X2)
| ~ sum(X0,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(n0))))),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f137,f2]) ).
fof(f139,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))))),s(s(n0)),X4)
| ~ sum(X2,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(n0))))),X0)
| ~ 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)))))))))))))))))))))))),X2)
| ~ 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(n0)))),X1) ),
inference(resolution,[],[f138,f2]) ).
fof(f140,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))))),s(n0),X4)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(n0))))),X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ 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(n0)))),X3)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1) ),
inference(resolution,[],[f139,f2]) ).
fof(f141,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X3)))))))))))))))))))),n0,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)))))))))))))))))))))))),X2)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))),s(s(s(s(n0)))),X3)
| ~ sum(X2,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(n0))))),X1) ),
inference(resolution,[],[f140,f2]) ).
fof(f142,plain,
! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))),s(s(s(s(n0)))),X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ sum(X0,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(n0))))),X1) ),
inference(resolution,[],[f141,f1]) ).
fof(f143,plain,
! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))))))))),s(s(s(n0))),X3)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(n0))))),X2)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f142,f2]) ).
fof(f144,plain,
! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))))))))),s(s(n0)),X3)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(n0))))),X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1) ),
inference(resolution,[],[f143,f2]) ).
fof(f145,plain,
! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1))))))))))))))))))),s(n0),X3)
| ~ 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)))))))))))))))))))))))),X2)
| ~ sum(X2,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(n0))))),X1) ),
inference(resolution,[],[f144,f2]) ).
fof(f146,plain,
! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X2))))))))))))))))))),n0,X3)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1)
| ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(n0))))),X2)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f145,f2]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(s(n0))))),X2)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f146,f1]) ).
fof(f148,plain,
! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(s(n0)))),X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1) ),
inference(resolution,[],[f147,f2]) ).
fof(f149,plain,
! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(s(n0))),X2)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f148,f2]) ).
fof(f150,plain,
! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(s(n0)),X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1) ),
inference(resolution,[],[f149,f2]) ).
fof(f151,plain,
! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),s(n0),X2)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f150,f2]) ).
fof(f152,plain,
! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X1)))))))))))))))))),n0,X2)
| ~ 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)))))))))))))))))))))))),X0)
| ~ sum(X0,s(s(s(s(s(s(n0)))))),X1) ),
inference(resolution,[],[f151,f2]) ).
fof(f153,plain,
! [X0,X1] :
( ~ sum(X0,s(s(s(s(s(s(n0)))))),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f152,f1]) ).
fof(f154,plain,
! [X0,X1] :
( ~ sum(X0,s(s(s(s(s(n0))))),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f153,f2]) ).
fof(f155,plain,
! [X0,X1] :
( ~ sum(X0,s(s(s(s(n0)))),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f154,f2]) ).
fof(f156,plain,
! [X0,X1] :
( ~ sum(X0,s(s(s(n0))),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f155,f2]) ).
fof(f157,plain,
! [X0,X1] :
( ~ sum(X0,s(s(n0)),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f156,f2]) ).
fof(f158,plain,
! [X0,X1] :
( ~ sum(X0,s(n0),X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f157,f2]) ).
fof(f159,plain,
! [X0,X1] :
( ~ sum(X0,n0,X1)
| ~ 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)))))))))))))))))))))))),X0) ),
inference(resolution,[],[f158,f2]) ).
fof(f160,plain,
! [X0] : ~ 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)))))))))))))))))))))))),X0),
inference(resolution,[],[f159,f1]) ).
fof(f161,plain,
$false,
inference(resolution,[],[f160,f3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM283-1.005 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n013.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 19:26:36 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.10/1.60 % (502832)Input is clausal, will run a generic CNF schedule.
% 3.10/1.60 % (502841)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3839299699:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.10/1.60 % (502841)Instruction limit reached!
% 3.10/1.60 % (502841)------------------------------
% 3.10/1.60 % (502841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.60 % (502841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.60 % (502841)CaDiCaL version: 2.1.3
% 3.10/1.60 % (502841)Termination reason: Instruction limit
% 3.10/1.60 % (502841)Termination phase: Saturation
% 3.10/1.60 % (502841)Time elapsed: 0.031 s
% 3.10/1.60 % (502841)Peak memory usage: 88 MB
% 3.10/1.60 % (502841)Instructions burned: 118 (million)
% 3.10/1.60 % (502839)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2544338636:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.10/1.60 % (502838)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1879565960:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.10/1.60 % (502840)lrs+10_1_sil=8000:sp=occurrence:random_seed=2233628404:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.10/1.60 % (502843)dis-21_1_sil=8000:lcm=predicate:random_seed=2608026367:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.10/1.60 % (502837)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1200931336:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.10/1.60 % (502842)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2062595521:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.10/1.60 % (502840)Instruction limit reached!
% 3.10/1.60 % (502840)------------------------------
% 3.10/1.60 % (502840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.60 % (502843)Instruction limit reached!
% 3.10/1.60 % (502843)------------------------------
% 3.10/1.60 % (502843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.60 % (502843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.60 % (502843)CaDiCaL version: 2.1.3
% 3.10/1.60 % (502840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.60 % (502843)Termination reason: Instruction limit
% 3.10/1.60 % (502843)Termination phase: Saturation
% 3.10/1.60 % (502840)CaDiCaL version: 2.1.3
% 3.10/1.60 % (502843)Time elapsed: 0.063 s
% 3.10/1.60 % (502843)Peak memory usage: 88 MB
% 3.10/1.60 % (502840)Termination reason: Instruction limit
% 3.10/1.60 % (502840)Termination phase: Saturation
% 3.10/1.60 % (502840)Time elapsed: 0.063 s
% 3.10/1.60 % (502843)Instructions burned: 119 (million)
% 3.10/1.60 % (502840)Peak memory usage: 89 MB
% 3.10/1.60 % (502840)Instructions burned: 108 (million)
% 3.10/1.60 % (502842)Instruction limit reached!
% 3.10/1.60 % (502842)------------------------------
% 3.10/1.60 % (502842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.60 % (502842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.60 % (502842)CaDiCaL version: 2.1.3
% 3.10/1.60 % (502842)Termination reason: Instruction limit
% 3.10/1.60 % (502842)Termination phase: Saturation
% 3.10/1.60 % (502842)Time elapsed: 0.107 s
% 3.10/1.60 % (502842)Peak memory usage: 89 MB
% 3.10/1.60 % (502842)Instructions burned: 182 (million)
% 3.10/1.60 % (502846)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=140037397:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.10/1.60 % (502846)Refutation not found, incomplete strategy
% 3.10/1.60 % (502846)------------------------------
% 3.10/1.60 % (502846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.60 % (502846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.60 % (502846)CaDiCaL version: 2.1.3
% 3.10/1.60 % (502846)Termination reason: Refutation not found, incomplete strategy
% 3.10/1.60 % (502846)Time elapsed: 0.0000 s
% 3.10/1.60 % (502846)Peak memory usage: 87 MB
% 3.10/1.60 % (502853)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3217805904:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.10/1.60 % (502854)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3851063026:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 3.10/1.60 % (502854)Refutation not found, incomplete strategy
% 3.10/1.60 % (502854)------------------------------
% 3.10/1.60 % (502854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.60 % (502854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.60 % (502854)CaDiCaL version: 2.1.3
% 3.10/1.60 % (502854)Termination reason: Refutation not found, incomplete strategy
% 3.10/1.60 % (502854)Time elapsed: 0.001 s
% 3.10/1.60 % (502854)Peak memory usage: 87 MB
% 3.10/1.60 % (502853)Refutation not found, incomplete strategy
% 3.10/1.60 % (502853)------------------------------
% 3.10/1.60 % (502853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.60 % (502853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.60 % (502853)CaDiCaL version: 2.1.3
% 3.10/1.60 % (502853)Termination reason: Refutation not found, incomplete strategy
% 3.10/1.60 % (502853)Time elapsed: 0.001 s
% 3.10/1.60 % (502853)Peak memory usage: 87 MB
% 3.10/1.60 % (502846)------------------------------
% 3.10/1.60 % (502846)------------------------------
% 3.10/1.60 % (502856)lrs+10_64_to=lpo:sil=8000:random_seed=529180207:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 3.10/1.60 % (502856)Instruction limit reached!
% 3.10/1.60 % (502856)------------------------------
% 3.10/1.60 % (502856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.10/1.60 % (502856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.10/1.60 % (502856)CaDiCaL version: 2.1.3
% 3.10/1.60 % (502856)Termination reason: Instruction limit
% 3.10/1.60 % (502856)Termination phase: Saturation
% 3.10/1.60 % (502856)Time elapsed: 0.069 s
% 3.10/1.60 % (502856)Peak memory usage: 88 MB
% 3.10/1.60 % (502856)Instructions burned: 127 (million)
% 3.10/1.60 % (502860)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3853650731:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 3.10/1.60 % (502860)First to succeed.
% 3.10/1.60 % (502860)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-502832"
% 3.10/1.60 % (502853)------------------------------
% 3.10/1.60 % (502853)------------------------------
% 3.10/1.60 % (502854)------------------------------
% 3.10/1.60 % (502854)------------------------------
% 3.10/1.60 % (502861)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1440324978:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 3.10/1.60 % (502860)Refutation found. Thanks to Tanya!
% 3.10/1.60 % SZS status Unsatisfiable for theBenchmark
% 3.10/1.60 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/1.80 % (502860)------------------------------
% 0.17/1.80 % (502860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.17/1.80 % (502860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/1.80 % (502860)CaDiCaL version: 2.1.3
% 0.17/1.80 % (502860)Termination reason: Refutation
% 0.17/1.80 % (502860)Time elapsed: 0.017 s
% 0.17/1.80 % (502860)Peak memory usage: 88 MB
% 0.17/1.80 % (502860)Instructions burned: 59 (million)
% 0.17/1.80 % (502860)------------------------------
% 0.17/1.80 % (502860)------------------------------
% 0.17/1.80 % (502832)Success in time 0.738 s
% 0.17/1.80 % Vampire exiting
%------------------------------------------------------------------------------