%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GEO449+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 09:52:41 AM UTC 2026
% Result : Theorem 32.68s 6.28s
% Output : Refutation 33.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 32
% Syntax : Number of formulae : 113 ( 94 unt; 28 def)
% Number of atoms : 132 ( 110 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 38 ( 19 ~; 14 |; 2 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 46 ( 46 usr; 42 con; 0-2 aty)
% Number of variables : 114 ( 109 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f200,axiom,
! [X0] : s(num,i(s(fun(num,num),numeral),s(num,X0))) = s(num,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aNUMERAL) ).
fof(f2771,axiom,
! [X0,X1] : s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(real,fun(cart(real,X0),cart(real,X0))),r_),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(cart(real,X0),X1))) = s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aVECTORu_MULu_LZERO) ).
fof(f3063,axiom,
! [X0,X1,X2,X3,X4,X5,X6] :
( p(s(bool,i(s(fun(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),bool),bilinear),s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3))))
=> s(cart(real,X0),i(s(fun(cart(real,X2),cart(real,X0)),i(s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3),s(cart(real,X1),X5))),s(cart(real,X2),i(s(fun(cart(real,X2),cart(real,X2)),i(s(fun(real,fun(cart(real,X2),cart(real,X2))),r_),s(real,X4))),s(cart(real,X2),X6))))) = s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(real,fun(cart(real,X0),cart(real,X0))),r_),s(real,X4))),s(cart(real,X0),i(s(fun(cart(real,X2),cart(real,X0)),i(s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3),s(cart(real,X1),X5))),s(cart(real,X2),X6))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aBILINEARu_RMUL) ).
fof(f3067,conjecture,
! [X0,X1,X2,X3,X4] :
( p(s(bool,i(s(fun(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),bool),bilinear),s(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),X3))))
=> s(cart(real,X2),i(s(fun(cart(real,X1),cart(real,X2)),i(s(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),X3),s(cart(real,X0),X4))),s(cart(real,X1),i(s(fun(num,cart(real,X1)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))) = s(cart(real,X2),i(s(fun(num,cart(real,X2)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',aBILINEARu_RZERO) ).
fof(f3068,negated_conjecture,
~ ! [X0,X1,X2,X3,X4] :
( p(s(bool,i(s(fun(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),bool),bilinear),s(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),X3))))
=> s(cart(real,X2),i(s(fun(cart(real,X1),cart(real,X2)),i(s(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),X3),s(cart(real,X0),X4))),s(cart(real,X1),i(s(fun(num,cart(real,X1)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))) = s(cart(real,X2),i(s(fun(num,cart(real,X2)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) ),
inference(negated_conjecture,[status(cth)],[f3067]) ).
fof(f5671,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( s(cart(real,X0),i(s(fun(cart(real,X2),cart(real,X0)),i(s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3),s(cart(real,X1),X5))),s(cart(real,X2),i(s(fun(cart(real,X2),cart(real,X2)),i(s(fun(real,fun(cart(real,X2),cart(real,X2))),r_),s(real,X4))),s(cart(real,X2),X6))))) = s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(real,fun(cart(real,X0),cart(real,X0))),r_),s(real,X4))),s(cart(real,X0),i(s(fun(cart(real,X2),cart(real,X0)),i(s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3),s(cart(real,X1),X5))),s(cart(real,X2),X6)))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),bool),bilinear),s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3)))) ),
inference(ennf_transformation,[],[f3063]) ).
fof(f5675,plain,
? [X0,X1,X2,X3,X4] :
( s(cart(real,X2),i(s(fun(num,cart(real,X2)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) != s(cart(real,X2),i(s(fun(cart(real,X1),cart(real,X2)),i(s(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),X3),s(cart(real,X0),X4))),s(cart(real,X1),i(s(fun(num,cart(real,X1)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))
& p(s(bool,i(s(fun(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),bool),bilinear),s(fun(cart(real,X0),fun(cart(real,X1),cart(real,X2))),X3)))) ),
inference(ennf_transformation,[],[f3068]) ).
fof(f9433,plain,
( s(cart(real,sK3879),i(s(fun(num,cart(real,sK3879)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) != s(cart(real,sK3879),i(s(fun(cart(real,sK3878),cart(real,sK3879)),i(s(fun(cart(real,sK3877),fun(cart(real,sK3878),cart(real,sK3879))),sK3880),s(cart(real,sK3877),sK3881))),s(cart(real,sK3878),i(s(fun(num,cart(real,sK3878)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0)))))))
& p(s(bool,i(s(fun(fun(cart(real,sK3877),fun(cart(real,sK3878),cart(real,sK3879))),bool),bilinear),s(fun(cart(real,sK3877),fun(cart(real,sK3878),cart(real,sK3879))),sK3880)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3877,sK3878,sK3879,sK3880,sK3881]),skolemize(X0,sK3877),skolemize(X1,sK3878),skolemize(X2,sK3879),skolemize(X3,sK3880),skolemize(X4,sK3881)],[f5675]) ).
fof(f10086,plain,
! [X0] : s(num,X0) = s(num,i(s(fun(num,num),numeral),s(num,X0))),
inference(cnf_transformation,[],[f200]) ).
fof(f15833,plain,
! [X0,X1] : s(cart(real,X0),i(s(fun(num,cart(real,X0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) = s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(real,fun(cart(real,X0),cart(real,X0))),r_),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(cart(real,X0),X1))),
inference(cnf_transformation,[],[f2771]) ).
fof(f16330,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),bool),bilinear),s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3))))
| s(cart(real,X0),i(s(fun(cart(real,X0),cart(real,X0)),i(s(fun(real,fun(cart(real,X0),cart(real,X0))),r_),s(real,X4))),s(cart(real,X0),i(s(fun(cart(real,X2),cart(real,X0)),i(s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3),s(cart(real,X1),X5))),s(cart(real,X2),X6))))) = s(cart(real,X0),i(s(fun(cart(real,X2),cart(real,X0)),i(s(fun(cart(real,X1),fun(cart(real,X2),cart(real,X0))),X3),s(cart(real,X1),X5))),s(cart(real,X2),i(s(fun(cart(real,X2),cart(real,X2)),i(s(fun(real,fun(cart(real,X2),cart(real,X2))),r_),s(real,X4))),s(cart(real,X2),X6))))) ),
inference(cnf_transformation,[],[f5671]) ).
fof(f16334,plain,
p(s(bool,i(s(fun(fun(cart(real,sK3877),fun(cart(real,sK3878),cart(real,sK3879))),bool),bilinear),s(fun(cart(real,sK3877),fun(cart(real,sK3878),cart(real,sK3879))),sK3880)))),
inference(cnf_transformation,[],[f9433]) ).
fof(f16335,plain,
s(cart(real,sK3879),i(s(fun(num,cart(real,sK3879)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) != s(cart(real,sK3879),i(s(fun(cart(real,sK3878),cart(real,sK3879)),i(s(fun(cart(real,sK3877),fun(cart(real,sK3878),cart(real,sK3879))),sK3880),s(cart(real,sK3877),sK3881))),s(cart(real,sK3878),i(s(fun(num,cart(real,sK3878)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),
inference(cnf_transformation,[],[f9433]) ).
fof(f16336,definition,
sF3882 = cart(real,sK3879),
introduced(definition,[new_symbols(definition,[sF3882])],[function_definition]) ).
fof(f16337,plain,
cart(real,sK3879) = sF3882,
inference(reorient_equations,[],[f16336]) ).
fof(f16338,definition,
sF3883 = fun(num,sF3882),
introduced(definition,[new_symbols(definition,[sF3883])],[function_definition]) ).
fof(f16339,plain,
fun(num,sF3882) = sF3883,
inference(reorient_equations,[],[f16338]) ).
fof(f16340,definition,
sF3884 = s(sF3883,vec),
introduced(definition,[new_symbols(definition,[sF3884])],[function_definition]) ).
fof(f16341,plain,
s(sF3883,vec) = sF3884,
inference(reorient_equations,[],[f16340]) ).
fof(f16342,definition,
sF3885 = fun(num,num),
introduced(definition,[new_symbols(definition,[sF3885])],[function_definition]) ).
fof(f16343,plain,
fun(num,num) = sF3885,
inference(reorient_equations,[],[f16342]) ).
fof(f16344,definition,
sF3886 = s(sF3885,numeral),
introduced(definition,[new_symbols(definition,[sF3886])],[function_definition]) ).
fof(f16345,plain,
s(sF3885,numeral) = sF3886,
inference(reorient_equations,[],[f16344]) ).
fof(f16346,definition,
sF3887 = s(num,u_0),
introduced(definition,[new_symbols(definition,[sF3887])],[function_definition]) ).
fof(f16347,plain,
s(num,u_0) = sF3887,
inference(reorient_equations,[],[f16346]) ).
fof(f16348,definition,
sF3888 = i(sF3886,sF3887),
introduced(definition,[new_symbols(definition,[sF3888])],[function_definition]) ).
fof(f16349,plain,
i(sF3886,sF3887) = sF3888,
inference(reorient_equations,[],[f16348]) ).
fof(f16350,definition,
sF3889 = s(num,sF3888),
introduced(definition,[new_symbols(definition,[sF3889])],[function_definition]) ).
fof(f16351,plain,
s(num,sF3888) = sF3889,
inference(reorient_equations,[],[f16350]) ).
fof(f16352,definition,
sF3890 = i(sF3884,sF3889),
introduced(definition,[new_symbols(definition,[sF3890])],[function_definition]) ).
fof(f16353,plain,
i(sF3884,sF3889) = sF3890,
inference(reorient_equations,[],[f16352]) ).
fof(f16354,definition,
sF3891 = s(sF3882,sF3890),
introduced(definition,[new_symbols(definition,[sF3891])],[function_definition]) ).
fof(f16355,plain,
s(sF3882,sF3890) = sF3891,
inference(reorient_equations,[],[f16354]) ).
fof(f16356,definition,
sF3892 = cart(real,sK3878),
introduced(definition,[new_symbols(definition,[sF3892])],[function_definition]) ).
fof(f16357,plain,
cart(real,sK3878) = sF3892,
inference(reorient_equations,[],[f16356]) ).
fof(f16358,definition,
sF3893 = fun(sF3892,sF3882),
introduced(definition,[new_symbols(definition,[sF3893])],[function_definition]) ).
fof(f16359,plain,
fun(sF3892,sF3882) = sF3893,
inference(reorient_equations,[],[f16358]) ).
fof(f16360,definition,
sF3894 = cart(real,sK3877),
introduced(definition,[new_symbols(definition,[sF3894])],[function_definition]) ).
fof(f16361,plain,
cart(real,sK3877) = sF3894,
inference(reorient_equations,[],[f16360]) ).
fof(f16362,definition,
sF3895 = fun(sF3894,sF3893),
introduced(definition,[new_symbols(definition,[sF3895])],[function_definition]) ).
fof(f16363,plain,
fun(sF3894,sF3893) = sF3895,
inference(reorient_equations,[],[f16362]) ).
fof(f16364,definition,
sF3896 = s(sF3895,sK3880),
introduced(definition,[new_symbols(definition,[sF3896])],[function_definition]) ).
fof(f16365,plain,
s(sF3895,sK3880) = sF3896,
inference(reorient_equations,[],[f16364]) ).
fof(f16366,definition,
sF3897 = s(sF3894,sK3881),
introduced(definition,[new_symbols(definition,[sF3897])],[function_definition]) ).
fof(f16367,plain,
s(sF3894,sK3881) = sF3897,
inference(reorient_equations,[],[f16366]) ).
fof(f16368,definition,
sF3898 = i(sF3896,sF3897),
introduced(definition,[new_symbols(definition,[sF3898])],[function_definition]) ).
fof(f16369,plain,
i(sF3896,sF3897) = sF3898,
inference(reorient_equations,[],[f16368]) ).
fof(f16370,definition,
sF3899 = s(sF3893,sF3898),
introduced(definition,[new_symbols(definition,[sF3899])],[function_definition]) ).
fof(f16371,plain,
s(sF3893,sF3898) = sF3899,
inference(reorient_equations,[],[f16370]) ).
fof(f16372,definition,
sF3900 = fun(num,sF3892),
introduced(definition,[new_symbols(definition,[sF3900])],[function_definition]) ).
fof(f16373,plain,
fun(num,sF3892) = sF3900,
inference(reorient_equations,[],[f16372]) ).
fof(f16374,definition,
sF3901 = s(sF3900,vec),
introduced(definition,[new_symbols(definition,[sF3901])],[function_definition]) ).
fof(f16375,plain,
s(sF3900,vec) = sF3901,
inference(reorient_equations,[],[f16374]) ).
fof(f16376,definition,
sF3902 = i(sF3901,sF3889),
introduced(definition,[new_symbols(definition,[sF3902])],[function_definition]) ).
fof(f16377,plain,
i(sF3901,sF3889) = sF3902,
inference(reorient_equations,[],[f16376]) ).
fof(f16378,definition,
sF3903 = s(sF3892,sF3902),
introduced(definition,[new_symbols(definition,[sF3903])],[function_definition]) ).
fof(f16379,plain,
s(sF3892,sF3902) = sF3903,
inference(reorient_equations,[],[f16378]) ).
fof(f16380,definition,
sF3904 = i(sF3899,sF3903),
introduced(definition,[new_symbols(definition,[sF3904])],[function_definition]) ).
fof(f16381,plain,
i(sF3899,sF3903) = sF3904,
inference(reorient_equations,[],[f16380]) ).
fof(f16382,definition,
sF3905 = s(sF3882,sF3904),
introduced(definition,[new_symbols(definition,[sF3905])],[function_definition]) ).
fof(f16383,plain,
s(sF3882,sF3904) = sF3905,
inference(reorient_equations,[],[f16382]) ).
fof(f16384,plain,
sF3891 != sF3905,
inference(definition_folding,[],[f16335,f16383,f16381,f16379,f16377,f16351,f16349,f16347,f16345,f16343,f16375,f16373,f16357,f16357,f16371,f16369,f16367,f16361,f16365,f16363,f16359,f16337,f16357,f16361,f16359,f16337,f16357,f16337,f16355,f16353,f16351,f16349,f16347,f16345,f16343,f16341,f16339,f16337,f16337]) ).
fof(f16385,definition,
sF3906 = fun(sF3895,bool),
introduced(definition,[new_symbols(definition,[sF3906])],[function_definition]) ).
fof(f16386,plain,
fun(sF3895,bool) = sF3906,
inference(reorient_equations,[],[f16385]) ).
fof(f16387,definition,
sF3907 = s(sF3906,bilinear),
introduced(definition,[new_symbols(definition,[sF3907])],[function_definition]) ).
fof(f16388,plain,
s(sF3906,bilinear) = sF3907,
inference(reorient_equations,[],[f16387]) ).
fof(f16389,definition,
sF3908 = i(sF3907,sF3896),
introduced(definition,[new_symbols(definition,[sF3908])],[function_definition]) ).
fof(f16390,plain,
i(sF3907,sF3896) = sF3908,
inference(reorient_equations,[],[f16389]) ).
fof(f16391,definition,
sF3909 = s(bool,sF3908),
introduced(definition,[new_symbols(definition,[sF3909])],[function_definition]) ).
fof(f16392,plain,
s(bool,sF3908) = sF3909,
inference(reorient_equations,[],[f16391]) ).
fof(f16393,plain,
p(sF3909),
inference(definition_folding,[],[f16334,f16392,f16390,f16365,f16363,f16359,f16337,f16357,f16361,f16388,f16386,f16363,f16359,f16337,f16357,f16361]) ).
fof(f18666,plain,
sF3887 = s(num,i(s(fun(num,num),numeral),sF3887)),
inference(superposition,[],[f10086,f16347]) ).
fof(f18670,plain,
sF3887 = s(num,i(s(sF3885,numeral),sF3887)),
inference(forward_demodulation,[],[f18666,f16343]) ).
fof(f18673,plain,
sF3887 = s(num,i(sF3886,sF3887)),
inference(forward_demodulation,[],[f18670,f16345]) ).
fof(f18674,plain,
sF3887 = s(num,sF3888),
inference(forward_demodulation,[],[f18673,f16349]) ).
fof(f18675,plain,
sF3887 = sF3889,
inference(forward_demodulation,[],[f18674,f16351]) ).
fof(f18712,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X0),fun(sF3892,cart(real,X1))),bool),bilinear),s(fun(cart(real,X0),fun(sF3892,cart(real,X1))),X2))))
| s(cart(real,X1),i(s(fun(cart(real,X1),cart(real,X1)),i(s(fun(real,fun(cart(real,X1),cart(real,X1))),r_),s(real,X3))),s(cart(real,X1),i(s(fun(sF3892,cart(real,X1)),i(s(fun(cart(real,X0),fun(sF3892,cart(real,X1))),X2),s(cart(real,X0),X4))),s(sF3892,X5))))) = s(cart(real,X1),i(s(fun(sF3892,cart(real,X1)),i(s(fun(cart(real,X0),fun(sF3892,cart(real,X1))),X2),s(cart(real,X0),X4))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X3))),s(sF3892,X5))))) ),
inference(superposition,[],[f16330,f16357]) ).
fof(f18876,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X0),fun(sF3892,sF3882)),bool),bilinear),s(fun(cart(real,X0),fun(sF3892,sF3882)),X1))))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X2))),s(sF3882,i(s(fun(sF3892,sF3882),i(s(fun(cart(real,X0),fun(sF3892,sF3882)),X1),s(cart(real,X0),X3))),s(sF3892,X4))))) = s(sF3882,i(s(fun(sF3892,sF3882),i(s(fun(cart(real,X0),fun(sF3892,sF3882)),X1),s(cart(real,X0),X3))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X2))),s(sF3892,X4))))) ),
inference(superposition,[],[f18712,f16337]) ).
fof(f18879,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X0),sF3893),bool),bilinear),s(fun(cart(real,X0),sF3893),X1))))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X2))),s(sF3882,i(s(fun(sF3892,sF3882),i(s(fun(cart(real,X0),fun(sF3892,sF3882)),X1),s(cart(real,X0),X3))),s(sF3892,X4))))) = s(sF3882,i(s(fun(sF3892,sF3882),i(s(fun(cart(real,X0),fun(sF3892,sF3882)),X1),s(cart(real,X0),X3))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X2))),s(sF3892,X4))))) ),
inference(forward_demodulation,[],[f18876,f16359]) ).
fof(f18880,plain,
! [X2,X3,X0,X1,X4] :
( ~ p(s(bool,i(s(fun(fun(cart(real,X0),sF3893),bool),bilinear),s(fun(cart(real,X0),sF3893),X1))))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X2))),s(sF3882,i(s(sF3893,i(s(fun(cart(real,X0),sF3893),X1),s(cart(real,X0),X3))),s(sF3892,X4))))) = s(sF3882,i(s(sF3893,i(s(fun(cart(real,X0),sF3893),X1),s(cart(real,X0),X3))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X2))),s(sF3892,X4))))) ),
inference(forward_demodulation,[],[f18879,f16359]) ).
fof(f19044,plain,
! [X0] : s(sF3882,i(s(fun(num,sF3882),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) = s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(sF3882,X0))),
inference(superposition,[],[f15833,f16337]) ).
fof(f19045,plain,
! [X0] : s(sF3892,i(s(fun(num,sF3892),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))) = s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(sF3892,X0))),
inference(superposition,[],[f15833,f16357]) ).
fof(f19049,plain,
! [X0] : s(sF3892,i(s(fun(num,sF3892),vec),s(num,u_0))) = s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(sF3892,X0))),
inference(forward_demodulation,[],[f19045,f10086]) ).
fof(f19050,plain,
! [X0] : s(sF3882,i(s(fun(num,sF3882),vec),s(num,u_0))) = s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,i(s(fun(num,real),realu_ofu_num),s(num,u_0))))),s(sF3882,X0))),
inference(forward_demodulation,[],[f19044,f10086]) ).
fof(f19055,plain,
! [X0] : s(sF3892,i(s(fun(num,sF3892),vec),sF3887)) = s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3887)))),s(sF3892,X0))),
inference(forward_demodulation,[],[f19049,f16347]) ).
fof(f19056,plain,
! [X0] : s(sF3882,i(s(fun(num,sF3882),vec),sF3887)) = s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3887)))),s(sF3882,X0))),
inference(forward_demodulation,[],[f19050,f16347]) ).
fof(f19061,plain,
! [X0] : s(sF3892,i(s(fun(num,sF3892),vec),sF3889)) = s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3892,X0))),
inference(forward_demodulation,[],[f19055,f18675]) ).
fof(f19062,plain,
! [X0] : s(sF3882,i(s(fun(num,sF3882),vec),sF3889)) = s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3882,X0))),
inference(forward_demodulation,[],[f19056,f18675]) ).
fof(f19065,plain,
! [X0] : s(sF3892,i(s(sF3900,vec),sF3889)) = s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3892,X0))),
inference(forward_demodulation,[],[f19061,f16373]) ).
fof(f19066,plain,
! [X0] : s(sF3882,i(s(sF3883,vec),sF3889)) = s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3882,X0))),
inference(forward_demodulation,[],[f19062,f16339]) ).
fof(f19069,plain,
! [X0] : s(sF3892,i(sF3901,sF3889)) = s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3892,X0))),
inference(forward_demodulation,[],[f19065,f16375]) ).
fof(f19070,plain,
! [X0] : s(sF3882,i(sF3884,sF3889)) = s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3882,X0))),
inference(forward_demodulation,[],[f19066,f16341]) ).
fof(f19071,plain,
! [X0] : s(sF3892,sF3902) = s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3892,X0))),
inference(forward_demodulation,[],[f19069,f16377]) ).
fof(f19072,plain,
! [X0] : s(sF3882,sF3890) = s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3882,X0))),
inference(forward_demodulation,[],[f19070,f16353]) ).
fof(f19073,plain,
! [X0] : sF3903 = s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3892,X0))),
inference(forward_demodulation,[],[f19071,f16379]) ).
fof(f19074,plain,
! [X0] : sF3891 = s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3882,X0))),
inference(forward_demodulation,[],[f19072,f16355]) ).
fof(f19243,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(s(fun(fun(sF3894,sF3893),bool),bilinear),s(fun(sF3894,sF3893),X0))))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X1))),s(sF3882,i(s(sF3893,i(s(fun(sF3894,sF3893),X0),s(sF3894,X2))),s(sF3892,X3))))) = s(sF3882,i(s(sF3893,i(s(fun(sF3894,sF3893),X0),s(sF3894,X2))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X1))),s(sF3892,X3))))) ),
inference(superposition,[],[f18880,f16361]) ).
fof(f19244,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(s(fun(sF3895,bool),bilinear),s(sF3895,X0))))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X1))),s(sF3882,i(s(sF3893,i(s(fun(sF3894,sF3893),X0),s(sF3894,X2))),s(sF3892,X3))))) = s(sF3882,i(s(sF3893,i(s(fun(sF3894,sF3893),X0),s(sF3894,X2))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X1))),s(sF3892,X3))))) ),
inference(forward_demodulation,[],[f19243,f16363]) ).
fof(f19245,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(s(sF3906,bilinear),s(sF3895,X0))))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X1))),s(sF3882,i(s(sF3893,i(s(fun(sF3894,sF3893),X0),s(sF3894,X2))),s(sF3892,X3))))) = s(sF3882,i(s(sF3893,i(s(fun(sF3894,sF3893),X0),s(sF3894,X2))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X1))),s(sF3892,X3))))) ),
inference(forward_demodulation,[],[f19244,f16386]) ).
fof(f19246,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(sF3907,s(sF3895,X0))))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X1))),s(sF3882,i(s(sF3893,i(s(fun(sF3894,sF3893),X0),s(sF3894,X2))),s(sF3892,X3))))) = s(sF3882,i(s(sF3893,i(s(fun(sF3894,sF3893),X0),s(sF3894,X2))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X1))),s(sF3892,X3))))) ),
inference(forward_demodulation,[],[f19245,f16388]) ).
fof(f19247,plain,
! [X2,X3,X0,X1] :
( ~ p(s(bool,i(sF3907,s(sF3895,X0))))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X1))),s(sF3882,i(s(sF3893,i(s(sF3895,X0),s(sF3894,X2))),s(sF3892,X3))))) = s(sF3882,i(s(sF3893,i(s(sF3895,X0),s(sF3894,X2))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X1))),s(sF3892,X3))))) ),
inference(forward_demodulation,[],[f19246,f16363]) ).
fof(f19248,plain,
! [X2,X0,X1] :
( ~ p(s(bool,i(sF3907,sF3896)))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X0))),s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X1))),s(sF3892,X2))))) = s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X1))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X0))),s(sF3892,X2))))) ),
inference(superposition,[],[f19247,f16365]) ).
fof(f19249,plain,
! [X2,X0,X1] :
( ~ p(s(bool,sF3908))
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X0))),s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X1))),s(sF3892,X2))))) = s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X1))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X0))),s(sF3892,X2))))) ),
inference(forward_demodulation,[],[f19248,f16390]) ).
fof(f19250,plain,
! [X2,X0,X1] :
( ~ p(sF3909)
| s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X0))),s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X1))),s(sF3892,X2))))) = s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X1))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X0))),s(sF3892,X2))))) ),
inference(forward_demodulation,[],[f19249,f16392]) ).
fof(f19251,plain,
! [X2,X0,X1] : s(sF3882,i(s(fun(sF3882,sF3882),i(s(fun(real,fun(sF3882,sF3882)),r_),s(real,X0))),s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X1))),s(sF3892,X2))))) = s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X1))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,X0))),s(sF3892,X2))))),
inference(forward_subsumption_resolution,[],[f19250,f16393]) ).
fof(f19483,plain,
! [X0,X1] : sF3891 = s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X0))),s(sF3892,i(s(fun(sF3892,sF3892),i(s(fun(real,fun(sF3892,sF3892)),r_),s(real,i(s(fun(num,real),realu_ofu_num),sF3889)))),s(sF3892,X1))))),
inference(superposition,[],[f19074,f19251]) ).
fof(f19490,plain,
! [X0] : sF3891 = s(sF3882,i(s(sF3893,i(sF3896,s(sF3894,X0))),sF3903)),
inference(forward_demodulation,[],[f19483,f19073]) ).
fof(f19496,plain,
sF3891 = s(sF3882,i(s(sF3893,i(sF3896,sF3897)),sF3903)),
inference(superposition,[],[f19490,f16367]) ).
fof(f19501,plain,
sF3891 = s(sF3882,i(s(sF3893,sF3898),sF3903)),
inference(forward_demodulation,[],[f19496,f16369]) ).
fof(f19502,plain,
sF3891 = s(sF3882,i(sF3899,sF3903)),
inference(forward_demodulation,[],[f19501,f16371]) ).
fof(f19503,plain,
sF3891 = s(sF3882,sF3904),
inference(forward_demodulation,[],[f19502,f16381]) ).
fof(f19504,plain,
sF3891 = sF3905,
inference(forward_demodulation,[],[f19503,f16383]) ).
fof(f19505,plain,
$false,
inference(forward_subsumption_resolution,[],[f19504,f16384]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO449+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n015.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 08:17:45 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/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
% 12.24/3.45 % (1339817)Detected formulas, will run a generic FOF schedule.
% 12.24/3.45 % (1339822)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=1529720347:i=141193_2990 on theBenchmark for (2990ds/141193Mi)
% 12.24/3.45 % (1339826)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2839570703:i=119:av=off:ss=axioms_2990 on theBenchmark for (2990ds/119Mi)
% 12.24/3.45 % (1339823)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=244890318:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2990 on theBenchmark for (2990ds/134677Mi)
% 12.24/3.45 % (1339828)dis-21_1_sil=8000:lcm=predicate:random_seed=1507914012:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2990 on theBenchmark for (2990ds/129Mi)
% 12.24/3.45 % (1339824)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3491747356:i=141695:sd=1:nm=32:gsp=on:ss=included_2990 on theBenchmark for (2990ds/141695Mi)
% 12.24/3.45 % (1339827)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2338999809:s2a=on:i=139:gtg=position_2990 on theBenchmark for (2990ds/139Mi)
% 12.24/3.45 % (1339825)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2061790851:i=109:sd=1:ins=1:gsp=on:ss=axioms_2990 on theBenchmark for (2990ds/109Mi)
% 12.24/3.45 % (1339827)Instruction limit reached!
% 12.24/3.45 % (1339827)------------------------------
% 12.24/3.45 % (1339827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.45 % (1339827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.45 % (1339827)CaDiCaL version: 2.1.3
% 12.24/3.45 % (1339827)Termination reason: Instruction limit
% 12.24/3.45 % (1339827)Termination phase: Property scanning
% 12.24/3.45 % (1339827)Time elapsed: 0.048 s
% 12.24/3.45 % (1339827)Peak memory usage: 89 MB
% 12.24/3.45 % (1339827)Instructions burned: 140 (million)
% 12.24/3.45 % (1339825)Instruction limit reached!
% 12.24/3.45 % (1339825)------------------------------
% 12.24/3.45 % (1339825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.45 % (1339825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.45 % (1339825)CaDiCaL version: 2.1.3
% 12.24/3.45 % (1339825)Termination reason: Instruction limit
% 12.24/3.45 % (1339825)Termination phase: Property scanning
% 12.24/3.45 % (1339825)Time elapsed: 0.055 s
% 12.24/3.45 % (1339825)Peak memory usage: 92 MB
% 12.24/3.45 % (1339825)Instructions burned: 111 (million)
% 12.24/3.45 % (1339828)Instruction limit reached!
% 12.24/3.45 % (1339828)------------------------------
% 12.24/3.45 % (1339828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.45 % (1339828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.45 % (1339828)CaDiCaL version: 2.1.3
% 12.24/3.45 % (1339828)Termination reason: Instruction limit
% 12.24/3.45 % (1339828)Termination phase: Preprocessing 1
% 12.24/3.45 % (1339828)Time elapsed: 0.063 s
% 12.24/3.45 % (1339828)Peak memory usage: 90 MB
% 12.24/3.45 % (1339828)Instructions burned: 129 (million)
% 12.24/3.45 % (1339826)Instruction limit reached!
% 12.24/3.45 % (1339826)------------------------------
% 12.24/3.45 % (1339826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/3.46 % (1339826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/3.46 % (1339826)CaDiCaL version: 2.1.3
% 12.24/3.46 % (1339826)Termination reason: Instruction limit
% 12.24/3.46 % (1339826)Termination phase: Preprocessing 1
% 12.24/3.46 % (1339826)Time elapsed: 0.063 s
% 12.24/3.46 % (1339826)Peak memory usage: 90 MB
% 12.24/3.46 % (1339826)Instructions burned: 120 (million)
% 12.24/3.46 % (1339836)lrs+10_1_sil=8000:sp=occurrence:random_seed=1539052757:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 12.24/3.46 % (1339837)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2852690431:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 12.24/3.46 % (1339838)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2895569687:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 12.24/3.46 % (1339839)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=293137558:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 12.24/3.46 % (1339837)Instruction limit reached!
% 19.05/4.38 % (1339837)------------------------------
% 19.05/4.38 % (1339837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.05/4.38 % (1339837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/4.38 % (1339837)CaDiCaL version: 2.1.3
% 19.05/4.38 % (1339837)Termination reason: Instruction limit
% 19.05/4.38 % (1339837)Termination phase: Property scanning
% 19.05/4.38 % (1339837)Time elapsed: 0.054 s
% 19.05/4.38 % (1339837)Peak memory usage: 90 MB
% 19.05/4.38 % (1339837)Instructions burned: 158 (million)
% 19.05/4.38 % (1339839)Instruction limit reached!
% 19.05/4.38 % (1339839)------------------------------
% 19.05/4.38 % (1339839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.05/4.38 % (1339839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/4.38 % (1339839)CaDiCaL version: 2.1.3
% 19.05/4.38 % (1339839)Termination reason: Instruction limit
% 19.05/4.38 % (1339839)Termination phase: Property scanning
% 19.05/4.38 % (1339839)Time elapsed: 0.086 s
% 19.05/4.38 % (1339839)Peak memory usage: 90 MB
% 19.05/4.38 % (1339839)Instructions burned: 251 (million)
% 19.05/4.38 % (1339836)Instruction limit reached!
% 19.05/4.38 % (1339836)------------------------------
% 19.05/4.38 % (1339836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.05/4.38 % (1339836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/4.38 % (1339836)CaDiCaL version: 2.1.3
% 19.05/4.38 % (1339836)Termination reason: Instruction limit
% 19.05/4.38 % (1339836)Termination phase: Property scanning
% 19.05/4.38 % (1339836)Time elapsed: 0.135 s
% 19.05/4.38 % (1339836)Peak memory usage: 95 MB
% 19.05/4.38 % (1339836)Instructions burned: 287 (million)
% 19.05/4.38 % (1339838)Instruction limit reached!
% 19.05/4.38 % (1339838)------------------------------
% 19.05/4.38 % (1339838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.05/4.38 % (1339838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/4.38 % (1339838)CaDiCaL version: 2.1.3
% 19.05/4.38 % (1339838)Termination reason: Instruction limit
% 19.05/4.38 % (1339838)Termination phase: Saturation
% 19.05/4.38 % (1339838)Time elapsed: 0.179 s
% 19.05/4.38 % (1339838)Peak memory usage: 96 MB
% 19.05/4.38 % (1339838)Instructions burned: 325 (million)
% 19.05/4.38 % (1339844)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4170870593:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 19.05/4.38 % (1339845)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1826707648:i=2350_2986 on theBenchmark for (2986ds/2350Mi)
% 19.05/4.38 % (1339846)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=201838385:cts=off:i=113:fsr=off:ss=included:sgt=4_2985 on theBenchmark for (2985ds/113Mi)
% 19.05/4.38 % (1339844)Instruction limit reached!
% 19.05/4.38 % (1339844)------------------------------
% 19.05/4.38 % (1339844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.05/4.38 % (1339844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/4.38 % (1339844)CaDiCaL version: 2.1.3
% 19.05/4.38 % (1339844)Termination reason: Instruction limit
% 19.05/4.38 % (1339844)Termination phase: Preprocessing 3
% 19.05/4.38 % (1339844)Time elapsed: 0.146 s
% 19.05/4.38 % (1339844)Peak memory usage: 95 MB
% 19.05/4.38 % (1339844)Instructions burned: 296 (million)
% 19.05/4.38 % (1339846)Instruction limit reached!
% 19.05/4.38 % (1339846)------------------------------
% 19.05/4.38 % (1339846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.05/4.38 % (1339846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/4.38 % (1339846)CaDiCaL version: 2.1.3
% 19.05/4.38 % (1339846)Termination reason: Instruction limit
% 19.05/4.38 % (1339846)Termination phase: Preprocessing 1
% 19.05/4.38 % (1339846)Time elapsed: 0.061 s
% 19.05/4.38 % (1339846)Peak memory usage: 90 MB
% 19.05/4.38 % (1339846)Instructions burned: 114 (million)
% 19.05/4.38 % (1339848)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3355143271:i=127:av=off:fsr=off:sup=off_2985 on theBenchmark for (2985ds/127Mi)
% 19.05/4.38 % (1339848)Instruction limit reached!
% 19.05/4.38 % (1339848)------------------------------
% 19.05/4.38 % (1339848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.05/4.38 % (1339848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.05/4.38 % (1339848)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339848)Termination reason: Instruction limit
% 32.68/6.28 % (1339848)Termination phase: Preprocessing 3
% 32.68/6.28 % (1339848)Time elapsed: 0.070 s
% 32.68/6.28 % (1339848)Peak memory usage: 93 MB
% 32.68/6.28 % (1339848)Instructions burned: 127 (million)
% 32.68/6.28 % (1339852)lrs+10_1_sil=8000:sp=occurrence:random_seed=2652685063:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 32.68/6.28 % (1339851)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1940351771:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2983 on theBenchmark for (2983ds/114Mi)
% 32.68/6.28 % (1339851)Instruction limit reached!
% 32.68/6.28 % (1339851)------------------------------
% 32.68/6.28 % (1339851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339851)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339851)Termination reason: Instruction limit
% 32.68/6.28 % (1339851)Termination phase: Property scanning
% 32.68/6.28 % (1339851)Time elapsed: 0.040 s
% 32.68/6.28 % (1339851)Peak memory usage: 89 MB
% 32.68/6.28 % (1339851)Instructions burned: 115 (million)
% 32.68/6.28 % (1339854)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3661897974:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 32.68/6.28 % (1339857)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1846300467:i=5202:ss=axioms:sgt=16_2981 on theBenchmark for (2981ds/5202Mi)
% 32.68/6.28 % (1339854)Instruction limit reached!
% 32.68/6.28 % (1339854)------------------------------
% 32.68/6.28 % (1339854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339854)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339854)Termination reason: Instruction limit
% 32.68/6.28 % (1339854)Termination phase: Property scanning
% 32.68/6.28 % (1339854)Time elapsed: 0.198 s
% 32.68/6.28 % (1339854)Peak memory usage: 96 MB
% 32.68/6.28 % (1339854)Instructions burned: 438 (million)
% 32.68/6.28 % (1339852)Instruction limit reached!
% 32.68/6.28 % (1339852)------------------------------
% 32.68/6.28 % (1339852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339852)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339852)Termination reason: Instruction limit
% 32.68/6.28 % (1339852)Termination phase: Saturation
% 32.68/6.28 % (1339852)Time elapsed: 0.382 s
% 32.68/6.28 % (1339852)Peak memory usage: 101 MB
% 32.68/6.28 % (1339852)Instructions burned: 909 (million)
% 32.68/6.28 % (1339860)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=596407108:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2978 on theBenchmark for (2978ds/134Mi)
% 32.68/6.28 % (1339860)Instruction limit reached!
% 32.68/6.28 % (1339860)------------------------------
% 32.68/6.28 % (1339860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339860)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339860)Termination reason: Instruction limit
% 32.68/6.28 % (1339860)Termination phase: NewCNF
% 32.68/6.28 % (1339860)Time elapsed: 0.078 s
% 32.68/6.28 % (1339860)Peak memory usage: 92 MB
% 32.68/6.28 % (1339860)Instructions burned: 134 (million)
% 32.68/6.28 % (1339861)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=960353932:st=8:i=592:sd=3:ep=RST:ss=axioms_2978 on theBenchmark for (2978ds/592Mi)
% 32.68/6.28 % (1339845)Instruction limit reached!
% 32.68/6.28 % (1339845)------------------------------
% 32.68/6.28 % (1339845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339845)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339845)Termination reason: Instruction limit
% 32.68/6.28 % (1339845)Termination phase: Property scanning
% 32.68/6.28 % (1339845)Time elapsed: 0.870 s
% 32.68/6.28 % (1339845)Peak memory usage: 104 MB
% 32.68/6.28 % (1339845)Instructions burned: 2350 (million)
% 32.68/6.28 % (1339863)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3181732572:st=3:i=13193:sd=3:ss=axioms_2976 on theBenchmark for (2976ds/13193Mi)
% 32.68/6.28 % (1339865)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=791738552:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2975 on theBenchmark for (2975ds/125Mi)
% 32.68/6.28 % (1339865)Instruction limit reached!
% 32.68/6.28 % (1339865)------------------------------
% 32.68/6.28 % (1339865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339865)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339865)Termination reason: Instruction limit
% 32.68/6.28 % (1339865)Termination phase: Property scanning
% 32.68/6.28 % (1339865)Time elapsed: 0.045 s
% 32.68/6.28 % (1339865)Peak memory usage: 90 MB
% 32.68/6.28 % (1339865)Instructions burned: 127 (million)
% 32.68/6.28 % (1339861)Instruction limit reached!
% 32.68/6.28 % (1339861)------------------------------
% 32.68/6.28 % (1339861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339861)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339861)Termination reason: Instruction limit
% 32.68/6.28 % (1339861)Termination phase: Preprocessing 3
% 32.68/6.28 % (1339861)Time elapsed: 0.305 s
% 32.68/6.28 % (1339861)Peak memory usage: 102 MB
% 32.68/6.28 % (1339861)Instructions burned: 593 (million)
% 32.68/6.28 % (1339868)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3258210946:i=134:gtgl=5:slsql=off:gtg=exists_sym_2973 on theBenchmark for (2973ds/134Mi)
% 32.68/6.28 % (1339869)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=4248270991:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/141Mi)
% 32.68/6.28 % (1339868)Instruction limit reached!
% 32.68/6.28 % (1339868)------------------------------
% 32.68/6.28 % (1339868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339868)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339868)Termination reason: Instruction limit
% 32.68/6.28 % (1339868)Termination phase: Property scanning
% 32.68/6.28 % (1339868)Time elapsed: 0.049 s
% 32.68/6.28 % (1339868)Peak memory usage: 90 MB
% 32.68/6.28 % (1339868)Instructions burned: 135 (million)
% 32.68/6.28 % (1339869)Instruction limit reached!
% 32.68/6.28 % (1339869)------------------------------
% 32.68/6.28 % (1339869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339869)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339869)Termination reason: Instruction limit
% 32.68/6.28 % (1339869)Termination phase: Saturation
% 32.68/6.28 % (1339869)Time elapsed: 0.073 s
% 32.68/6.28 % (1339869)Peak memory usage: 94 MB
% 32.68/6.28 % (1339869)Instructions burned: 141 (million)
% 32.68/6.28 % (1339872)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2119589170:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2971 on theBenchmark for (2971ds/431Mi)
% 32.68/6.28 % (1339873)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1668508817:i=6060:aac=none:ins=25_2970 on theBenchmark for (2970ds/6060Mi)
% 32.68/6.28 % (1339872)Instruction limit reached!
% 32.68/6.28 % (1339872)------------------------------
% 32.68/6.28 % (1339872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339872)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339872)Termination reason: Instruction limit
% 32.68/6.28 % (1339872)Termination phase: Saturation
% 32.68/6.28 % (1339872)Time elapsed: 0.216 s
% 32.68/6.28 % (1339872)Peak memory usage: 96 MB
% 32.68/6.28 % (1339872)Instructions burned: 432 (million)
% 32.68/6.28 % (1339876)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=434354988:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2967 on theBenchmark for (2967ds/150Mi)
% 32.68/6.28 % (1339876)Instruction limit reached!
% 32.68/6.28 % (1339876)------------------------------
% 32.68/6.28 % (1339876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339876)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339876)Termination reason: Instruction limit
% 32.68/6.28 % (1339876)Termination phase: Preprocessing 1
% 32.68/6.28 % (1339876)Time elapsed: 0.081 s
% 32.68/6.28 % (1339876)Peak memory usage: 91 MB
% 32.68/6.28 % (1339876)Instructions burned: 151 (million)
% 32.68/6.28 % (1339878)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1981361552:i=14155:bd=all_2964 on theBenchmark for (2964ds/14155Mi)
% 32.68/6.28 % (1339857)Instruction limit reached!
% 32.68/6.28 % (1339857)------------------------------
% 32.68/6.28 % (1339857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.68/6.28 % (1339857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.68/6.28 % (1339857)CaDiCaL version: 2.1.3
% 32.68/6.28 % (1339857)Termination reason: Instruction limit
% 32.68/6.28 % (1339857)Termination phase: Saturation
% 32.68/6.28 % (1339857)Time elapsed: 2.882 s
% 32.68/6.28 % (1339857)Peak memory usage: 189 MB
% 32.68/6.28 % (1339857)Instructions burned: 5204 (million)
% 32.68/6.28 % (1339880)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2085739565:i=667:av=off:fsr=off_2950 on theBenchmark for (2950ds/667Mi)
% 32.68/6.28 % (1339822)First to succeed.
% 32.68/6.28 % (1339822)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1339817"
% 32.68/6.28 % (1339822)Refutation found. Thanks to Tanya!
% 32.68/6.28 % SZS status Theorem for theBenchmark
% 32.68/6.28 % SZS output start Proof for theBenchmark
% See solution above
% 33.30/6.47 % (1339822)------------------------------
% 33.30/6.47 % (1339822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.30/6.47 % (1339822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.30/6.47 % (1339822)CaDiCaL version: 2.1.3
% 33.30/6.47 % (1339822)Termination reason: Refutation
% 33.30/6.47 % (1339822)Time elapsed: 4.165 s
% 33.30/6.47 % (1339822)Peak memory usage: 276 MB
% 33.30/6.47 % (1339822)Instructions burned: 13782 (million)
% 33.30/6.47 % (1339822)------------------------------
% 33.30/6.47 % (1339822)------------------------------
% 33.30/6.47 % (1339817)Success in time 5.416 s
% 33.30/6.47 % Vampire exiting
%------------------------------------------------------------------------------