%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW448-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 01:30:21 PM UTC 2026
% Result : Unsatisfiable 247.11s 35.87s
% Output : Refutation 248.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 19
% Syntax : Number of formulae : 226 ( 60 unt; 12 def)
% Number of atoms : 773 ( 76 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 740 ( 193 ~; 535 |; 0 &)
% ( 12 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 12 ( 3 avg)
% Number of predicates : 15 ( 13 usr; 13 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 95 ( 0 sgn 95 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : sep(X0,sep(X1,X2)) = sep(X1,sep(X0,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associative_commutative) ).
fof(f2,axiom,
! [X0,X1] : sep(lseg(X0,X0),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',normalization) ).
fof(f6,axiom,
! [X2,X3,X0,X1] : ~ heap(sep(next(X0,X1),sep(next(X0,X2),X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wellformedness_3) ).
fof(f9,axiom,
! [X2,X3,X0,X1] :
( ~ heap(sep(next(X0,X1),sep(lseg(X1,X2),X3)))
| X0 = X1
| heap(sep(lseg(X0,X2),X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unfolding_2) ).
fof(f12,axiom,
! [X2,X3,X0,X1,X4] :
( ~ heap(sep(lseg(X0,X1),sep(lseg(X1,X2),sep(lseg(X2,X3),X4))))
| X2 = X3
| heap(sep(lseg(X0,X2),sep(lseg(X2,X3),X4))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',unfolding_5) ).
fof(f13,axiom,
heap(sep(next(x5,x10),sep(lseg(x9,x7),sep(next(x2,x7),sep(next(x4,x7),sep(next(x6,x4),sep(next(x7,x3),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',premise_1) ).
fof(f14,negated_conjecture,
~ heap(sep(lseg(x3,x5),sep(lseg(x8,x4),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x5,x3),emp)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conclusion_1) ).
fof(f29,plain,
! [X2,X3,X0,X1,X4] : ~ heap(sep(next(X1,X4),sep(X0,sep(next(X1,X2),X3)))),
inference(superposition,[],[f6,f1]) ).
fof(f33,plain,
~ heap(sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x8,x4),sep(lseg(x6,x7),sep(lseg(x5,x3),emp)))))),
inference(superposition,[],[f14,f1]) ).
fof(f37,plain,
~ heap(sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),sep(lseg(x5,x3),emp)))))),
inference(forward_demodulation,[],[f33,f1]) ).
fof(f41,plain,
~ heap(sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x5,x3),sep(lseg(x8,x4),emp)))))),
inference(forward_demodulation,[],[f37,f1]) ).
fof(f45,plain,
~ heap(sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x5,x3),sep(lseg(x6,x7),sep(lseg(x8,x4),emp)))))),
inference(forward_demodulation,[],[f41,f1]) ).
fof(f49,plain,
~ heap(sep(lseg(x3,x5),sep(lseg(x5,x3),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp)))))),
inference(forward_demodulation,[],[f45,f1]) ).
fof(f53,plain,
~ heap(sep(lseg(x5,x3),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp)))))),
inference(forward_demodulation,[],[f49,f1]) ).
fof(f71,plain,
! [X2,X0,X1] :
( heap(sep(lseg(X1,X2),X0))
| X1 = X2
| ~ heap(sep(next(X1,X2),X0)) ),
inference(superposition,[],[f9,f2]) ).
fof(f74,plain,
! [X2,X3,X0,X1] :
( ~ heap(sep(lseg(X0,X1),sep(next(X2,X0),X3)))
| X0 = X2
| heap(sep(lseg(X2,X1),X3)) ),
inference(superposition,[],[f9,f1]) ).
fof(f89,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ heap(sep(lseg(X4,X5),sep(lseg(X5,X1),sep(X0,sep(lseg(X1,X2),X3)))))
| X1 = X2
| heap(sep(lseg(X4,X1),sep(X0,sep(lseg(X1,X2),X3)))) ),
inference(superposition,[],[f12,f1]) ).
fof(f95,plain,
! [X2,X3,X0,X1,X4] :
( ~ heap(sep(lseg(X0,X1),sep(lseg(X2,X0),sep(lseg(X1,X3),X4))))
| X1 = X3
| heap(sep(lseg(X2,X1),sep(lseg(X1,X3),X4))) ),
inference(superposition,[],[f12,f1]) ).
fof(f105,plain,
heap(sep(next(x5,x10),sep(next(x2,x7),sep(lseg(x9,x7),sep(next(x4,x7),sep(next(x6,x4),sep(next(x7,x3),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f13,f1]) ).
fof(f106,plain,
heap(sep(next(x2,x7),sep(next(x5,x10),sep(lseg(x9,x7),sep(next(x4,x7),sep(next(x6,x4),sep(next(x7,x3),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f105,f1]) ).
fof(f107,plain,
heap(sep(next(x2,x7),sep(next(x5,x10),sep(next(x4,x7),sep(lseg(x9,x7),sep(next(x6,x4),sep(next(x7,x3),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f106,f1]) ).
fof(f108,plain,
heap(sep(next(x2,x7),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x7,x3),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f107,f1]) ).
fof(f109,plain,
heap(sep(next(x2,x7),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(next(x7,x3),sep(lseg(x9,x7),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f108,f1]) ).
fof(f110,plain,
heap(sep(next(x2,x7),sep(next(x5,x10),sep(next(x4,x7),sep(next(x7,x3),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f109,f1]) ).
fof(f111,plain,
heap(sep(next(x2,x7),sep(next(x5,x10),sep(next(x7,x3),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f110,f1]) ).
fof(f112,plain,
heap(sep(next(x2,x7),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x1,x2),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f111,f1]) ).
fof(f113,plain,
heap(sep(next(x2,x7),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(next(x1,x2),sep(lseg(x9,x7),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f112,f1]) ).
fof(f114,plain,
heap(sep(next(x2,x7),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x1,x2),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f113,f1]) ).
fof(f115,plain,
heap(sep(next(x2,x7),sep(next(x7,x3),sep(next(x5,x10),sep(next(x1,x2),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f114,f1]) ).
fof(f116,plain,
heap(sep(next(x2,x7),sep(next(x7,x3),sep(next(x1,x2),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f115,f1]) ).
fof(f117,plain,
heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x10,x1),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f116,f1]) ).
fof(f118,plain,
heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(next(x10,x1),sep(lseg(x9,x7),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f117,f1]) ).
fof(f119,plain,
heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x10,x1),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f118,f1]) ).
fof(f120,plain,
heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x10,x1),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f119,f1]) ).
fof(f121,plain,
heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x10,x1),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f120,f1]) ).
fof(f122,plain,
heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x10,x1),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f121,f1]) ).
fof(f123,plain,
heap(sep(next(x2,x7),sep(next(x10,x1),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f122,f1]) ).
fof(f124,plain,
heap(sep(next(x10,x1),sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x9,x7),sep(next(x8,x4),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f123,f1]) ).
fof(f125,plain,
heap(sep(next(x10,x1),sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),sep(next(x3,x5),emp))))))))))),
inference(forward_demodulation,[],[f124,f1]) ).
fof(f126,plain,
heap(sep(next(x10,x1),sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(next(x3,x5),sep(lseg(x9,x7),emp))))))))))),
inference(forward_demodulation,[],[f125,f1]) ).
fof(f127,plain,
heap(sep(next(x10,x1),sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x6,x4),sep(next(x3,x5),sep(next(x8,x4),sep(lseg(x9,x7),emp))))))))))),
inference(forward_demodulation,[],[f126,f1]) ).
fof(f128,plain,
heap(sep(next(x10,x1),sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp))))))))))),
inference(forward_demodulation,[],[f127,f1]) ).
fof(f134,plain,
! [X2,X3,X0,X1,X4,X5] : ~ heap(sep(next(X1,X4),sep(X5,sep(X0,sep(next(X1,X2),X3))))),
inference(superposition,[],[f29,f1]) ).
fof(f139,plain,
! [X2,X3,X0,X1,X4] : ~ heap(sep(X0,sep(next(X1,X2),sep(next(X1,X3),X4)))),
inference(superposition,[],[f29,f1]) ).
fof(f141,plain,
! [X2,X3,X0,X1,X4,X5] : ~ heap(sep(X4,sep(next(X1,X5),sep(X0,sep(next(X1,X2),X3))))),
inference(superposition,[],[f139,f1]) ).
fof(f171,plain,
! [X2,X3,X0,X1,X6,X4,X5] : ~ heap(sep(next(X1,X4),sep(X5,sep(X6,sep(X0,sep(next(X1,X2),X3)))))),
inference(superposition,[],[f134,f1]) ).
fof(f193,plain,
! [X2,X3,X0,X1,X4,X5] : ~ heap(sep(X5,sep(X0,sep(next(X1,X2),sep(next(X1,X3),X4))))),
inference(superposition,[],[f141,f1]) ).
fof(f213,plain,
! [X2,X3,X0,X1] :
( ~ heap(sep(next(X1,X2),sep(X0,X3)))
| X1 = X2
| heap(sep(X0,sep(lseg(X1,X2),X3))) ),
inference(superposition,[],[f71,f1]) ).
fof(f223,definition,
( spl0_2
<=> x5 = x3 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f224,plain,
( x5 != x3
| spl0_2 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f225,plain,
( x5 = x3
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f268,plain,
! [X2,X3,X0,X1] :
( ~ heap(sep(next(X0,X2),sep(next(X1,X0),X3)))
| heap(sep(lseg(X1,X2),X3))
| X0 = X2
| X0 = X1 ),
inference(resolution,[],[f74,f71]) ).
fof(f269,plain,
! [X2,X3,X0,X1,X4] :
( ~ heap(sep(lseg(X2,X4),sep(X0,sep(next(X1,X2),X3))))
| X1 = X2
| heap(sep(lseg(X1,X4),sep(X0,X3))) ),
inference(superposition,[],[f74,f1]) ).
fof(f275,plain,
! [X2,X3,X0,X1,X6,X4,X5] : ~ heap(sep(X4,sep(X5,sep(next(X1,X6),sep(X0,sep(next(X1,X2),X3)))))),
inference(superposition,[],[f193,f1]) ).
fof(f488,plain,
( x10 = x1
| heap(sep(next(x2,x7),sep(lseg(x10,x1),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp))))))))))) ),
inference(resolution,[],[f213,f128]) ).
fof(f495,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(lseg(x10,x1),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| x10 = x1 ),
inference(forward_demodulation,[],[f488,f1]) ).
fof(f496,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(lseg(x10,x1),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| x10 = x1 ),
inference(forward_demodulation,[],[f495,f1]) ).
fof(f497,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(lseg(x10,x1),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| x10 = x1 ),
inference(forward_demodulation,[],[f496,f1]) ).
fof(f498,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(lseg(x10,x1),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| x10 = x1 ),
inference(forward_demodulation,[],[f497,f1]) ).
fof(f499,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(lseg(x10,x1),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| x10 = x1 ),
inference(forward_demodulation,[],[f498,f1]) ).
fof(f500,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(lseg(x10,x1),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| x10 = x1 ),
inference(forward_demodulation,[],[f499,f1]) ).
fof(f501,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| x10 = x1 ),
inference(forward_demodulation,[],[f500,f1]) ).
fof(f503,definition,
( spl0_4
<=> x10 = x1 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f505,plain,
( x10 = x1
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f507,definition,
( spl0_5
<=> heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f509,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f507]) ).
fof(f510,plain,
( spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f501,f507,f503]) ).
fof(f511,plain,
( heap(sep(next(x10,x10),sep(next(x2,x7),sep(next(x10,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_4 ),
inference(superposition,[],[f128,f505]) ).
fof(f512,plain,
( $false
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f511,f29]) ).
fof(f513,plain,
~ spl0_4,
inference(avatar_contradiction_clause,[],[f512]) ).
fof(f514,plain,
( x7 = x2
| heap(sep(next(x1,x2),sep(lseg(x2,x7),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_5 ),
inference(resolution,[],[f509,f213]) ).
fof(f515,plain,
( heap(sep(next(x1,x2),sep(next(x7,x3),sep(lseg(x2,x7),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| x7 = x2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f514,f1]) ).
fof(f516,plain,
( heap(sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(lseg(x2,x7),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| x7 = x2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f515,f1]) ).
fof(f517,plain,
( heap(sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(lseg(x2,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| x7 = x2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f516,f1]) ).
fof(f518,plain,
( heap(sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(lseg(x2,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| x7 = x2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f517,f1]) ).
fof(f519,plain,
( heap(sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(lseg(x2,x7),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| x7 = x2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f518,f1]) ).
fof(f520,plain,
( heap(sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x2,x7),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| x7 = x2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f519,f1]) ).
fof(f521,plain,
( heap(sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| x7 = x2
| ~ spl0_5 ),
inference(forward_demodulation,[],[f520,f1]) ).
fof(f523,definition,
( spl0_6
<=> x7 = x2 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f524,plain,
( x7 != x2
| spl0_6 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( x7 = x2
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl0_7
<=> heap(sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp))))))))))) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f529,plain,
( heap(sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f530,plain,
( spl0_6
| spl0_7
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f521,f507,f527,f523]) ).
fof(f533,plain,
( heap(sep(next(x10,x1),sep(next(x2,x2),sep(next(x1,x2),sep(next(x2,x3),sep(next(x5,x10),sep(next(x4,x2),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x2),emp)))))))))))
| ~ spl0_6 ),
inference(superposition,[],[f128,f525]) ).
fof(f539,plain,
( $false
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f533,f141]) ).
fof(f540,plain,
~ spl0_6,
inference(avatar_contradiction_clause,[],[f539]) ).
fof(f547,plain,
( x2 = x1
| heap(sep(next(x7,x3),sep(lseg(x1,x2),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_7 ),
inference(resolution,[],[f529,f213]) ).
fof(f548,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(lseg(x1,x2),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| x2 = x1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f547,f1]) ).
fof(f549,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(lseg(x1,x2),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| x2 = x1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f548,f1]) ).
fof(f550,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(lseg(x1,x2),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| x2 = x1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f549,f1]) ).
fof(f551,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(lseg(x1,x2),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| x2 = x1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f550,f1]) ).
fof(f552,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x1,x2),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| x2 = x1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f551,f1]) ).
fof(f553,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x2),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| x2 = x1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f552,f1]) ).
fof(f554,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x1,x2),sep(lseg(x9,x7),emp)))))))))))
| x2 = x1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f553,f1]) ).
fof(f556,definition,
( spl0_8
<=> x2 = x1 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f557,plain,
( x2 != x1
| spl0_8 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f558,plain,
( x2 = x1
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f560,definition,
( spl0_9
<=> heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x1,x2),sep(lseg(x9,x7),emp))))))))))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f562,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x1,x2),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f560]) ).
fof(f563,plain,
( spl0_8
| spl0_9
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f554,f527,f560,f556]) ).
fof(f567,plain,
( heap(sep(next(x10,x2),sep(next(x2,x7),sep(next(x2,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_8 ),
inference(superposition,[],[f128,f558]) ).
fof(f568,plain,
( $false
| ~ spl0_8 ),
inference(forward_subsumption_resolution,[],[f567,f139]) ).
fof(f569,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f568]) ).
fof(f581,definition,
( spl0_10
<=> x7 = x3 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f582,plain,
( x7 != x3
| spl0_10 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( x7 = x3
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f594,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x7),sep(next(x5,x10),sep(next(x4,x7),sep(next(x7,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_5
| ~ spl0_10 ),
inference(superposition,[],[f509,f583]) ).
fof(f601,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x7),sep(next(x5,x10),sep(next(x7,x5),sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_5
| ~ spl0_10 ),
inference(forward_demodulation,[],[f594,f1]) ).
fof(f605,plain,
( $false
| ~ spl0_5
| ~ spl0_10 ),
inference(forward_subsumption_resolution,[],[f601,f275]) ).
fof(f606,plain,
( ~ spl0_5
| ~ spl0_10 ),
inference(avatar_contradiction_clause,[],[f605]) ).
fof(f621,definition,
( spl0_12
<=> x5 = x10 ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f622,plain,
( x5 != x10
| spl0_12 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f623,plain,
( x5 = x10
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f631,plain,
( heap(sep(next(x10,x1),sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x10,x10),sep(next(x4,x7),sep(next(x3,x10),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_12 ),
inference(superposition,[],[f128,f623]) ).
fof(f641,plain,
( $false
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f631,f171]) ).
fof(f642,plain,
~ spl0_12,
inference(avatar_contradiction_clause,[],[f641]) ).
fof(f661,definition,
( spl0_14
<=> x7 = x4 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f662,plain,
( x7 != x4
| spl0_14 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f663,plain,
( x7 = x4
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f674,plain,
( heap(sep(next(x2,x7),sep(next(x1,x2),sep(next(x7,x3),sep(next(x5,x10),sep(next(x7,x7),sep(next(x3,x5),sep(next(x6,x7),sep(next(x8,x7),sep(lseg(x10,x1),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_5
| ~ spl0_14 ),
inference(superposition,[],[f509,f663]) ).
fof(f684,plain,
( $false
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f674,f275]) ).
fof(f685,plain,
( ~ spl0_5
| ~ spl0_14 ),
inference(avatar_contradiction_clause,[],[f684]) ).
fof(f717,definition,
( spl0_17
<=> x4 = x6 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f718,plain,
( x4 != x6
| spl0_17 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f719,plain,
( x4 = x6
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f732,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x4,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x1,x2),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_9
| ~ spl0_17 ),
inference(superposition,[],[f562,f719]) ).
fof(f742,plain,
( $false
| ~ spl0_9
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f732,f275]) ).
fof(f743,plain,
( ~ spl0_9
| ~ spl0_17 ),
inference(avatar_contradiction_clause,[],[f742]) ).
fof(f766,plain,
( heap(sep(next(x1,x2),sep(next(x7,x5),sep(next(x5,x10),sep(next(x4,x7),sep(next(x5,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x2,x7),sep(lseg(x9,x7),emp)))))))))))
| ~ spl0_2
| ~ spl0_7 ),
inference(superposition,[],[f529,f225]) ).
fof(f777,plain,
( $false
| ~ spl0_2
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f766,f275]) ).
fof(f778,plain,
( ~ spl0_2
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f777]) ).
fof(f813,definition,
( spl0_19
<=> x4 = x8 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f814,plain,
( x4 != x8
| spl0_19 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f815,plain,
( x4 = x8
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f905,plain,
( heap(sep(lseg(x1,x7),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| x7 = x2
| x2 = x1
| ~ spl0_5 ),
inference(resolution,[],[f268,f509]) ).
fof(f910,plain,
( heap(sep(lseg(x1,x7),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| x2 = x1
| ~ spl0_5
| spl0_6 ),
inference(forward_subsumption_resolution,[],[f905,f524]) ).
fof(f911,plain,
( heap(sep(lseg(x1,x7),sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(forward_subsumption_resolution,[],[f910,f557]) ).
fof(f912,plain,
( heap(sep(next(x7,x3),sep(lseg(x1,x7),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(forward_demodulation,[],[f911,f1]) ).
fof(f913,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(lseg(x1,x7),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(forward_demodulation,[],[f912,f1]) ).
fof(f914,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(lseg(x1,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(forward_demodulation,[],[f913,f1]) ).
fof(f915,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(lseg(x1,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(forward_demodulation,[],[f914,f1]) ).
fof(f916,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(lseg(x1,x7),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(forward_demodulation,[],[f915,f1]) ).
fof(f917,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x1,x7),sep(lseg(x10,x1),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(forward_demodulation,[],[f916,f1]) ).
fof(f918,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(forward_demodulation,[],[f917,f1]) ).
fof(f919,plain,
( x7 = x3
| heap(sep(next(x5,x10),sep(lseg(x7,x3),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8 ),
inference(resolution,[],[f918,f213]) ).
fof(f920,plain,
( heap(sep(next(x5,x10),sep(lseg(x7,x3),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f919,f582]) ).
fof(f921,plain,
( heap(sep(next(x5,x10),sep(next(x4,x7),sep(lseg(x7,x3),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10 ),
inference(forward_demodulation,[],[f920,f1]) ).
fof(f922,plain,
( heap(sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(lseg(x7,x3),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10 ),
inference(forward_demodulation,[],[f921,f1]) ).
fof(f923,plain,
( heap(sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(lseg(x7,x3),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10 ),
inference(forward_demodulation,[],[f922,f1]) ).
fof(f924,plain,
( heap(sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x7,x3),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10 ),
inference(forward_demodulation,[],[f923,f1]) ).
fof(f925,plain,
( heap(sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x7,x3),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10 ),
inference(forward_demodulation,[],[f924,f1]) ).
fof(f926,plain,
( heap(sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10 ),
inference(forward_demodulation,[],[f925,f1]) ).
fof(f927,plain,
( x5 = x10
| heap(sep(next(x4,x7),sep(lseg(x5,x10),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10 ),
inference(resolution,[],[f926,f213]) ).
fof(f928,plain,
( heap(sep(next(x4,x7),sep(lseg(x5,x10),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f927,f622]) ).
fof(f929,plain,
( heap(sep(next(x4,x7),sep(next(x3,x5),sep(lseg(x5,x10),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f928,f1]) ).
fof(f930,plain,
( heap(sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(lseg(x5,x10),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f929,f1]) ).
fof(f931,plain,
( heap(sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x5,x10),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f930,f1]) ).
fof(f932,plain,
( heap(sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x5,x10),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f931,f1]) ).
fof(f933,plain,
( heap(sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x5,x10),sep(lseg(x7,x3),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f932,f1]) ).
fof(f934,plain,
( heap(sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f933,f1]) ).
fof(f989,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x6,x4),sep(next(x4,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| ~ spl0_19 ),
inference(superposition,[],[f918,f815]) ).
fof(f1001,plain,
( heap(sep(next(x7,x3),sep(next(x5,x10),sep(next(x4,x7),sep(next(x3,x5),sep(next(x4,x4),sep(next(x6,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| ~ spl0_19 ),
inference(forward_demodulation,[],[f989,f1]) ).
fof(f1020,plain,
( $false
| ~ spl0_5
| spl0_6
| spl0_8
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f1001,f275]) ).
fof(f1021,plain,
( ~ spl0_5
| spl0_6
| spl0_8
| ~ spl0_19 ),
inference(avatar_contradiction_clause,[],[f1020]) ).
fof(f1058,plain,
! [X2,X3,X0,X1] :
( ~ heap(sep(X0,sep(next(X1,X2),X3)))
| X1 = X2
| heap(sep(lseg(X1,X2),sep(X0,X3))) ),
inference(superposition,[],[f269,f2]) ).
fof(f1592,plain,
( x5 = x3
| heap(sep(lseg(x3,x5),sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(resolution,[],[f1058,f934]) ).
fof(f1604,plain,
( heap(sep(lseg(x3,x5),sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_subsumption_resolution,[],[f1592,f224]) ).
fof(f1617,plain,
( heap(sep(next(x4,x7),sep(lseg(x3,x5),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f1604,f1]) ).
fof(f1630,plain,
( heap(sep(next(x4,x7),sep(next(x6,x4),sep(lseg(x3,x5),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f1617,f1]) ).
fof(f1643,plain,
( heap(sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x3,x5),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f1630,f1]) ).
fof(f1656,plain,
( heap(sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x3,x5),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f1643,f1]) ).
fof(f1669,plain,
( heap(sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x3,x5),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f1656,f1]) ).
fof(f1682,plain,
( heap(sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x3,x5),sep(lseg(x5,x10),sep(lseg(x9,x7),emp))))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f1669,f1]) ).
fof(f1695,plain,
( heap(sep(next(x4,x7),sep(next(x6,x4),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),emp))))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(forward_demodulation,[],[f1682,f1]) ).
fof(f1736,plain,
( heap(sep(lseg(x6,x7),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),emp)))))))))
| x7 = x4
| x4 = x6
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12 ),
inference(resolution,[],[f1695,f268]) ).
fof(f1741,plain,
( heap(sep(lseg(x6,x7),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),emp)))))))))
| x4 = x6
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f1736,f662]) ).
fof(f1744,plain,
( heap(sep(lseg(x6,x7),sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(forward_subsumption_resolution,[],[f1741,f718]) ).
fof(f1747,plain,
( heap(sep(next(x8,x4),sep(lseg(x6,x7),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(forward_demodulation,[],[f1744,f1]) ).
fof(f1750,plain,
( heap(sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x6,x7),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(forward_demodulation,[],[f1747,f1]) ).
fof(f1753,plain,
( heap(sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x6,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(forward_demodulation,[],[f1750,f1]) ).
fof(f1756,plain,
( heap(sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x6,x7),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(forward_demodulation,[],[f1753,f1]) ).
fof(f1758,plain,
( heap(sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x6,x7),sep(lseg(x3,x5),sep(lseg(x9,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(forward_demodulation,[],[f1756,f1]) ).
fof(f1760,plain,
( heap(sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x6,x7),sep(lseg(x9,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(forward_demodulation,[],[f1758,f1]) ).
fof(f1762,plain,
( heap(sep(next(x8,x4),sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(forward_demodulation,[],[f1760,f1]) ).
fof(f1781,plain,
( x4 = x8
| heap(sep(lseg(x10,x1),sep(lseg(x8,x4),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17 ),
inference(resolution,[],[f1762,f213]) ).
fof(f1782,plain,
( heap(sep(lseg(x10,x1),sep(lseg(x8,x4),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1781,f814]) ).
fof(f1783,plain,
( heap(sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x8,x4),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_demodulation,[],[f1782,f1]) ).
fof(f1784,plain,
( heap(sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x8,x4),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_demodulation,[],[f1783,f1]) ).
fof(f1785,plain,
( heap(sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x8,x4),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_demodulation,[],[f1784,f1]) ).
fof(f1786,plain,
( heap(sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x8,x4),sep(lseg(x9,x7),sep(lseg(x6,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_demodulation,[],[f1785,f1]) ).
fof(f1787,plain,
( heap(sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x8,x4),sep(lseg(x6,x7),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_demodulation,[],[f1786,f1]) ).
fof(f1788,plain,
( heap(sep(lseg(x10,x1),sep(lseg(x1,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp)))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_demodulation,[],[f1787,f1]) ).
fof(f1814,plain,
( x7 = x3
| heap(sep(lseg(x10,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(resolution,[],[f1788,f12]) ).
fof(f1815,plain,
( heap(sep(lseg(x10,x7),sep(lseg(x7,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp))))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1814,f582]) ).
fof(f1834,plain,
( x5 = x3
| heap(sep(lseg(x10,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp)))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(resolution,[],[f1815,f89]) ).
fof(f1837,plain,
( heap(sep(lseg(x10,x3),sep(lseg(x5,x10),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp)))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1834,f224]) ).
fof(f1856,plain,
( x5 = x3
| heap(sep(lseg(x5,x3),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(resolution,[],[f1837,f95]) ).
fof(f1861,plain,
( heap(sep(lseg(x5,x3),sep(lseg(x3,x5),sep(lseg(x9,x7),sep(lseg(x6,x7),sep(lseg(x8,x4),emp))))))
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1856,f224]) ).
fof(f1862,plain,
( $false
| spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(forward_subsumption_resolution,[],[f1861,f53]) ).
fof(f1863,plain,
( spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(avatar_contradiction_clause,[],[f1862]) ).
cnf(s3,plain,
( spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f510]) ).
cnf(s4,plain,
~ spl0_4,
inference(sat_conversion,[],[f513]) ).
cnf(s5,plain,
( ~ spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f530]) ).
cnf(s7,plain,
~ spl0_6,
inference(sat_conversion,[],[f540]) ).
cnf(s8,plain,
( ~ spl0_7
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f563]) ).
cnf(s9,plain,
~ spl0_8,
inference(sat_conversion,[],[f569]) ).
cnf(s14,plain,
( ~ spl0_5
| ~ spl0_10 ),
inference(sat_conversion,[],[f606]) ).
cnf(s16,plain,
~ spl0_12,
inference(sat_conversion,[],[f642]) ).
cnf(s20,plain,
( ~ spl0_5
| ~ spl0_14 ),
inference(sat_conversion,[],[f685]) ).
cnf(s25,plain,
( ~ spl0_9
| ~ spl0_17 ),
inference(sat_conversion,[],[f743]) ).
cnf(s28,plain,
( ~ spl0_2
| ~ spl0_7 ),
inference(sat_conversion,[],[f778]) ).
cnf(s36,plain,
( ~ spl0_5
| spl0_6
| spl0_8
| ~ spl0_19 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s45,plain,
( spl0_2
| ~ spl0_5
| spl0_6
| spl0_8
| spl0_10
| spl0_12
| spl0_14
| spl0_17
| spl0_19 ),
inference(sat_conversion,[],[f1863]) ).
cnf(s48,plain,
( ~ spl0_7
| spl0_9 ),
inference(rat,[],[s8,s9]) ).
cnf(s49,plain,
( ~ spl0_5
| spl0_7 ),
inference(rat,[],[s5,s7]) ).
cnf(s50,plain,
spl0_5,
inference(rat,[],[s3,s4]) ).
cnf(s51,plain,
~ spl0_19,
inference(rat,[],[s36,s7,s9,s50]) ).
cnf(s52,plain,
~ spl0_14,
inference(rat,[],[s20,s50]) ).
cnf(s53,plain,
~ spl0_10,
inference(rat,[],[s14,s50]) ).
cnf(s54,plain,
spl0_7,
inference(rat,[],[s49,s50]) ).
cnf(s55,plain,
~ spl0_2,
inference(rat,[],[s28,s54]) ).
cnf(s56,plain,
spl0_9,
inference(rat,[],[s48,s54]) ).
cnf(s57,plain,
spl0_17,
inference(rat,[],[s45,s51,s53,s52,s16,s50,s9,s7,s55]) ).
cnf(s58,plain,
$false,
inference(rat,[],[s25,s57,s56]) ).
fof(f1864,plain,
$false,
inference(avatar_sat_refutation,[],[s58]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW448-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 % Computer : n009.cluster.edu
% 0.10/0.24 % Model : x86_64 x86_64
% 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.24 % Memory : 8046.5625MB
% 0.10/0.24 % OS : Linux 6.8.0-71-generic
% 0.10/0.24 % CPULimit : 300
% 0.10/0.24 % WCLimit : 300
% 0.10/0.24 % DateTime : Mon Sep 28 13:56:45 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.29 Running first-order theorem proving
% 0.22/0.29 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
% 18.84/3.52 % (3037004)Input is clausal, will run a generic CNF schedule.
% 18.84/3.52 % (3037009)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=92112893:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 18.84/3.52 % (3037014)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3563741485:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 18.84/3.52 % (3037010)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3458244969:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 18.84/3.52 % (3037011)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1678257018:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 18.84/3.52 % (3037013)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2254119721:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 18.84/3.52 % (3037012)lrs+10_1_sil=8000:sp=occurrence:random_seed=2356941615:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 18.84/3.52 % (3037015)dis-21_1_sil=8000:lcm=predicate:random_seed=1167581676: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)
% 18.84/3.52 % (3037015)Refutation not found, incomplete strategy
% 18.84/3.52 % (3037015)------------------------------
% 18.84/3.52 % (3037015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.52 % (3037015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.52 % (3037015)CaDiCaL version: 2.1.3
% 18.84/3.52 % (3037015)Termination reason: Refutation not found, incomplete strategy
% 18.84/3.52 % (3037015)Time elapsed: 0.002 s
% 18.84/3.52 % (3037015)Peak memory usage: 88 MB
% 18.84/3.52 % (3037015)Instructions burned: 1 (million)
% 18.84/3.52 % (3037014)Instruction limit reached!
% 18.84/3.52 % (3037014)------------------------------
% 18.84/3.52 % (3037014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.52 % (3037014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.52 % (3037014)CaDiCaL version: 2.1.3
% 18.84/3.52 % (3037014)Termination reason: Instruction limit
% 18.84/3.52 % (3037014)Termination phase: Saturation
% 18.84/3.52 % (3037014)Time elapsed: 0.168 s
% 18.84/3.52 % (3037014)Peak memory usage: 89 MB
% 18.84/3.52 % (3037014)Instructions burned: 180 (million)
% 18.84/3.52 % (3037012)Instruction limit reached!
% 18.84/3.52 % (3037012)------------------------------
% 18.84/3.52 % (3037012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.52 % (3037012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.52 % (3037012)CaDiCaL version: 2.1.3
% 18.84/3.52 % (3037012)Termination reason: Instruction limit
% 18.84/3.52 % (3037012)Termination phase: Saturation
% 18.84/3.52 % (3037012)Time elapsed: 0.101 s
% 18.84/3.52 % (3037012)Peak memory usage: 88 MB
% 18.84/3.52 % (3037012)Instructions burned: 107 (million)
% 18.84/3.52 % (3037013)Instruction limit reached!
% 18.84/3.52 % (3037013)------------------------------
% 18.84/3.52 % (3037013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.52 % (3037013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.52 % (3037013)CaDiCaL version: 2.1.3
% 18.84/3.52 % (3037013)Termination reason: Instruction limit
% 18.84/3.52 % (3037013)Termination phase: Saturation
% 18.84/3.52 % (3037013)Time elapsed: 0.107 s
% 18.84/3.52 % (3037013)Peak memory usage: 89 MB
% 18.84/3.52 % (3037013)Instructions burned: 114 (million)
% 18.84/3.52 % (3037023)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=254854021:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 18.84/3.52 % (3037023)Refutation not found, incomplete strategy
% 18.84/3.52 % (3037023)------------------------------
% 18.84/3.52 % (3037023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/3.52 % (3037023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/3.52 % (3037023)CaDiCaL version: 2.1.3
% 18.84/3.52 % (3037023)Termination reason: Refutation not found, incomplete strategy
% 18.84/3.52 % (3037023)Time elapsed: 0.004 s
% 18.84/3.52 % (3037023)Peak memory usage: 87 MB
% 18.84/3.52 % (3037023)Instructions burned: 2 (million)
% 18.84/3.52 % (3037025)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=52723426:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 32.91/5.51 % (3037024)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2241275094:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 32.91/5.51 % (3037025)Refutation not found, incomplete strategy
% 32.91/5.51 % (3037025)------------------------------
% 32.91/5.51 % (3037025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.51 % (3037025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.51 % (3037025)CaDiCaL version: 2.1.3
% 32.91/5.51 % (3037025)Termination reason: Refutation not found, incomplete strategy
% 32.91/5.51 % (3037025)Time elapsed: 0.003 s
% 32.91/5.51 % (3037025)Peak memory usage: 87 MB
% 32.91/5.51 % (3037025)Instructions burned: 2 (million)
% 32.91/5.51 % (3037024)Refutation not found, incomplete strategy
% 32.91/5.51 % (3037024)------------------------------
% 32.91/5.51 % (3037024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.51 % (3037024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.51 % (3037024)CaDiCaL version: 2.1.3
% 32.91/5.51 % (3037024)Termination reason: Refutation not found, incomplete strategy
% 32.91/5.51 % (3037024)Time elapsed: 0.004 s
% 32.91/5.51 % (3037024)Peak memory usage: 88 MB
% 32.91/5.51 % (3037024)Instructions burned: 3 (million)
% 32.91/5.51 % (3037015)------------------------------
% 32.91/5.51 % (3037015)------------------------------
% 32.91/5.51 % (3037029)lrs+10_64_to=lpo:sil=8000:random_seed=2444076693:i=126:bd=preordered_2992 on theBenchmark for (2992ds/126Mi)
% 32.91/5.51 % (3037029)Instruction limit reached!
% 32.91/5.51 % (3037029)------------------------------
% 32.91/5.51 % (3037029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.51 % (3037029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.51 % (3037029)CaDiCaL version: 2.1.3
% 32.91/5.51 % (3037029)Termination reason: Instruction limit
% 32.91/5.51 % (3037029)Termination phase: Saturation
% 32.91/5.51 % (3037029)Time elapsed: 0.062 s
% 32.91/5.51 % (3037029)Peak memory usage: 88 MB
% 32.91/5.51 % (3037029)Instructions burned: 126 (million)
% 32.91/5.51 % (3037025)------------------------------
% 32.91/5.51 % (3037025)------------------------------
% 32.91/5.51 % (3037023)------------------------------
% 32.91/5.51 % (3037023)------------------------------
% 32.91/5.51 % (3037024)------------------------------
% 32.91/5.51 % (3037024)------------------------------
% 32.91/5.51 % (3037031)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1684178250:avsq=on:i=194:fgj=on:bd=preordered_2989 on theBenchmark for (2989ds/194Mi)
% 32.91/5.51 % (3037031)Instruction limit reached!
% 32.91/5.51 % (3037031)------------------------------
% 32.91/5.51 % (3037031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.51 % (3037031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.51 % (3037031)CaDiCaL version: 2.1.3
% 32.91/5.51 % (3037031)Termination reason: Instruction limit
% 32.91/5.51 % (3037031)Termination phase: Saturation
% 32.91/5.51 % (3037031)Time elapsed: 0.074 s
% 32.91/5.51 % (3037031)Peak memory usage: 89 MB
% 32.91/5.51 % (3037031)Instructions burned: 194 (million)
% 32.91/5.51 % (3037032)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1659027447:i=157:gtg=all_2989 on theBenchmark for (2989ds/157Mi)
% 32.91/5.51 % (3037033)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1680176663:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 32.91/5.51 % (3037034)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3389284099:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 32.91/5.51 % (3037034)Instruction limit reached!
% 32.91/5.51 % (3037034)------------------------------
% 32.91/5.51 % (3037034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.91/5.51 % (3037034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.91/5.51 % (3037034)CaDiCaL version: 2.1.3
% 32.91/5.51 % (3037034)Termination reason: Instruction limit
% 32.91/5.51 % (3037034)Termination phase: Saturation
% 32.91/5.51 % (3037034)Time elapsed: 0.105 s
% 32.91/5.51 % (3037034)Peak memory usage: 89 MB
% 32.91/5.51 % (3037034)Instructions burned: 107 (million)
% 51.95/8.18 % (3037032)Instruction limit reached!
% 51.95/8.18 % (3037032)------------------------------
% 51.95/8.18 % (3037032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.95/8.18 % (3037032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.95/8.18 % (3037032)CaDiCaL version: 2.1.3
% 51.95/8.18 % (3037032)Termination reason: Instruction limit
% 51.95/8.18 % (3037032)Termination phase: Saturation
% 51.95/8.18 % (3037032)Time elapsed: 0.161 s
% 51.95/8.18 % (3037032)Peak memory usage: 90 MB
% 51.95/8.18 % (3037032)Instructions burned: 157 (million)
% 51.95/8.18 % (3037036)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2540248592:i=107_2986 on theBenchmark for (2986ds/107Mi)
% 51.95/8.18 % (3037036)Refutation not found, incomplete strategy
% 51.95/8.18 % (3037036)------------------------------
% 51.95/8.18 % (3037036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.95/8.18 % (3037036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.95/8.18 % (3037036)CaDiCaL version: 2.1.3
% 51.95/8.18 % (3037036)Termination reason: Refutation not found, incomplete strategy
% 51.95/8.18 % (3037036)Time elapsed: 0.002 s
% 51.95/8.18 % (3037036)Peak memory usage: 87 MB
% 51.95/8.18 % (3037036)Instructions burned: 2 (million)
% 51.95/8.18 % (3037040)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=241674131:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2985 on theBenchmark for (2985ds/242Mi)
% 51.95/8.18 % (3037036)------------------------------
% 51.95/8.18 % (3037036)------------------------------
% 51.95/8.18 % (3037041)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3985768859:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 51.95/8.18 % (3037040)Instruction limit reached!
% 51.95/8.18 % (3037040)------------------------------
% 51.95/8.18 % (3037040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.95/8.18 % (3037040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.95/8.18 % (3037040)CaDiCaL version: 2.1.3
% 51.95/8.18 % (3037040)Termination reason: Instruction limit
% 51.95/8.18 % (3037040)Termination phase: Saturation
% 51.95/8.18 % (3037040)Time elapsed: 0.253 s
% 51.95/8.18 % (3037040)Peak memory usage: 90 MB
% 51.95/8.18 % (3037040)Instructions burned: 242 (million)
% 51.95/8.18 % (3037044)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1688979585:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 51.95/8.18 % (3037044)Instruction limit reached!
% 51.95/8.18 % (3037044)------------------------------
% 51.95/8.18 % (3037044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.95/8.18 % (3037044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.95/8.18 % (3037044)CaDiCaL version: 2.1.3
% 51.95/8.18 % (3037044)Termination reason: Instruction limit
% 51.95/8.18 % (3037044)Termination phase: Saturation
% 51.95/8.18 % (3037044)Time elapsed: 0.065 s
% 51.95/8.18 % (3037044)Peak memory usage: 89 MB
% 51.95/8.18 % (3037044)Instructions burned: 135 (million)
% 51.95/8.18 % (3037046)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2969280223:i=499:bd=all_2980 on theBenchmark for (2980ds/499Mi)
% 51.95/8.18 % (3037048)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1995522865:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 51.95/8.18 % (3037048)Instruction limit reached!
% 51.95/8.18 % (3037048)------------------------------
% 51.95/8.18 % (3037048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.95/8.18 % (3037048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.95/8.18 % (3037048)CaDiCaL version: 2.1.3
% 51.95/8.18 % (3037048)Termination reason: Instruction limit
% 51.95/8.18 % (3037048)Termination phase: Saturation
% 51.95/8.18 % (3037048)Time elapsed: 0.096 s
% 51.95/8.18 % (3037048)Peak memory usage: 90 MB
% 51.95/8.18 % (3037048)Instructions burned: 194 (million)
% 51.95/8.18 % (3037051)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2359071857:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 51.95/8.18 % (3037046)Instruction limit reached!
% 51.95/8.18 % (3037046)------------------------------
% 51.95/8.18 % (3037046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.95/8.18 % (3037046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.63/12.29 % (3037046)CaDiCaL version: 2.1.3
% 80.63/12.29 % (3037046)Termination reason: Instruction limit
% 80.63/12.29 % (3037046)Termination phase: Saturation
% 80.63/12.29 % (3037046)Time elapsed: 0.446 s
% 80.63/12.29 % (3037046)Peak memory usage: 90 MB
% 80.63/12.29 % (3037046)Instructions burned: 500 (million)
% 80.63/12.29 % (3037051)Instruction limit reached!
% 80.63/12.29 % (3037051)------------------------------
% 80.63/12.29 % (3037051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.63/12.29 % (3037051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.63/12.29 % (3037051)CaDiCaL version: 2.1.3
% 80.63/12.29 % (3037051)Termination reason: Instruction limit
% 80.63/12.29 % (3037051)Termination phase: Saturation
% 80.63/12.29 % (3037051)Time elapsed: 0.126 s
% 80.63/12.29 % (3037051)Peak memory usage: 90 MB
% 80.63/12.29 % (3037051)Instructions burned: 264 (million)
% 80.63/12.29 % (3037053)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3888285938:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 80.63/12.29 % (3037054)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3996333767:i=3256:kws=precedence:bd=preordered:av=off_2972 on theBenchmark for (2972ds/3256Mi)
% 80.63/12.29 % (3037053)Instruction limit reached!
% 80.63/12.29 % (3037053)------------------------------
% 80.63/12.29 % (3037053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.63/12.29 % (3037053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.63/12.29 % (3037053)CaDiCaL version: 2.1.3
% 80.63/12.29 % (3037053)Termination reason: Instruction limit
% 80.63/12.29 % (3037053)Termination phase: Saturation
% 80.63/12.29 % (3037053)Time elapsed: 0.138 s
% 80.63/12.29 % (3037053)Peak memory usage: 88 MB
% 80.63/12.29 % (3037053)Instructions burned: 157 (million)
% 80.63/12.29 % (3037057)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2149036153:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 80.63/12.29 % (3037057)Instruction limit reached!
% 80.63/12.29 % (3037057)------------------------------
% 80.63/12.29 % (3037057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.63/12.29 % (3037057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.63/12.29 % (3037057)CaDiCaL version: 2.1.3
% 80.63/12.29 % (3037057)Termination reason: Instruction limit
% 80.63/12.29 % (3037057)Termination phase: Saturation
% 80.63/12.29 % (3037057)Time elapsed: 0.507 s
% 80.63/12.29 % (3037057)Peak memory usage: 91 MB
% 80.63/12.29 % (3037057)Instructions burned: 537 (million)
% 80.63/12.29 % (3037059)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1675790749:i=180:bd=preordered:av=off_2960 on theBenchmark for (2960ds/180Mi)
% 80.63/12.29 % (3037059)Instruction limit reached!
% 80.63/12.29 % (3037059)------------------------------
% 80.63/12.29 % (3037059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.63/12.29 % (3037059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.63/12.29 % (3037059)CaDiCaL version: 2.1.3
% 80.63/12.29 % (3037059)Termination reason: Instruction limit
% 80.63/12.29 % (3037059)Termination phase: Saturation
% 80.63/12.29 % (3037059)Time elapsed: 0.166 s
% 80.63/12.29 % (3037059)Peak memory usage: 89 MB
% 80.63/12.29 % (3037059)Instructions burned: 181 (million)
% 80.63/12.29 % (3037033)Instruction limit reached!
% 80.63/12.29 % (3037033)------------------------------
% 80.63/12.29 % (3037033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.63/12.29 % (3037033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.63/12.29 % (3037033)CaDiCaL version: 2.1.3
% 80.63/12.29 % (3037033)Termination reason: Instruction limit
% 80.63/12.29 % (3037033)Termination phase: Saturation
% 80.63/12.29 % (3037033)Time elapsed: 3.228 s
% 80.63/12.29 % (3037033)Peak memory usage: 142 MB
% 80.63/12.29 % (3037033)Instructions burned: 3394 (million)
% 80.63/12.29 % (3037061)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=4192933784:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2956 on theBenchmark for (2956ds/10307Mi)
% 80.63/12.29 % (3037054)Instruction limit reached!
% 80.63/12.29 % (3037054)------------------------------
% 80.63/12.29 % (3037054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.63/12.29 % (3037054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.70/16.39 % (3037054)CaDiCaL version: 2.1.3
% 109.70/16.39 % (3037054)Termination reason: Instruction limit
% 109.70/16.39 % (3037054)Termination phase: Saturation
% 109.70/16.39 % (3037054)Time elapsed: 1.660 s
% 109.70/16.39 % (3037054)Peak memory usage: 145 MB
% 109.70/16.39 % (3037054)Instructions burned: 3258 (million)
% 109.70/16.39 % (3037062)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=2628272139:i=412:gtgl=4:gtg=exists_all_2954 on theBenchmark for (2954ds/412Mi)
% 109.70/16.39 % (3037064)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2690173246:s2pl=no:i=8478:s2at=4:nm=6_2953 on theBenchmark for (2953ds/8478Mi)
% 109.70/16.39 % (3037062)Instruction limit reached!
% 109.70/16.39 % (3037062)------------------------------
% 109.70/16.39 % (3037062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.70/16.39 % (3037062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.70/16.39 % (3037062)CaDiCaL version: 2.1.3
% 109.70/16.39 % (3037062)Termination reason: Instruction limit
% 109.70/16.39 % (3037062)Termination phase: Saturation
% 109.70/16.39 % (3037062)Time elapsed: 0.399 s
% 109.70/16.39 % (3037062)Peak memory usage: 94 MB
% 109.70/16.39 % (3037062)Instructions burned: 412 (million)
% 109.70/16.39 % (3037067)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=2601611884:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2947 on theBenchmark for (2947ds/303Mi)
% 109.70/16.39 % (3037067)Refutation not found, incomplete strategy
% 109.70/16.39 % (3037067)------------------------------
% 109.70/16.39 % (3037067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.70/16.39 % (3037067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.70/16.39 % (3037067)CaDiCaL version: 2.1.3
% 109.70/16.39 % (3037067)Termination reason: Refutation not found, incomplete strategy
% 109.70/16.39 % (3037067)Time elapsed: 0.002 s
% 109.70/16.39 % (3037067)Peak memory usage: 88 MB
% 109.70/16.39 % (3037067)Instructions burned: 1 (million)
% 109.70/16.39 % (3037067)------------------------------
% 109.70/16.39 % (3037067)------------------------------
% 109.70/16.39 % (3037069)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2263572858:st=4:i=720:sd=3:fsr=off:ss=axioms_2941 on theBenchmark for (2941ds/720Mi)
% 109.70/16.39 % (3037069)Refutation not found, incomplete strategy
% 109.70/16.39 % (3037069)------------------------------
% 109.70/16.39 % (3037069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.70/16.39 % (3037069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.70/16.39 % (3037069)CaDiCaL version: 2.1.3
% 109.70/16.39 % (3037069)Termination reason: Refutation not found, incomplete strategy
% 109.70/16.39 % (3037069)Time elapsed: 0.003 s
% 109.70/16.39 % (3037069)Peak memory usage: 88 MB
% 109.70/16.39 % (3037069)Instructions burned: 2 (million)
% 109.70/16.39 % (3037069)------------------------------
% 109.70/16.39 % (3037069)------------------------------
% 109.70/16.39 % (3037041)Instruction limit reached!
% 109.70/16.39 % (3037041)------------------------------
% 109.70/16.39 % (3037041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.70/16.39 % (3037041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 109.70/16.39 % (3037041)CaDiCaL version: 2.1.3
% 109.70/16.39 % (3037041)Termination reason: Instruction limit
% 109.70/16.39 % (3037041)Termination phase: Saturation
% 109.70/16.39 % (3037041)Time elapsed: 4.919 s
% 109.70/16.39 % (3037041)Peak memory usage: 155 MB
% 109.70/16.39 % (3037041)Instructions burned: 5208 (million)
% 109.70/16.39 % (3037071)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=474022982:i=598:bs=on:bd=preordered:av=off:ss=axioms_2935 on theBenchmark for (2935ds/598Mi)
% 109.70/16.39 % (3037072)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3353116131:i=2989:sd=3:ss=axioms:sgt=60_2932 on theBenchmark for (2932ds/2989Mi)
% 109.70/16.39 % (3037071)Instruction limit reached!
% 109.70/16.39 % (3037071)------------------------------
% 109.70/16.39 % (3037071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 109.70/16.39 % (3037071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.59/23.63 % (3037071)CaDiCaL version: 2.1.3
% 161.59/23.63 % (3037071)Termination reason: Instruction limit
% 161.59/23.63 % (3037071)Termination phase: Saturation
% 161.59/23.63 % (3037071)Time elapsed: 0.553 s
% 161.59/23.63 % (3037071)Peak memory usage: 93 MB
% 161.59/23.63 % (3037071)Instructions burned: 599 (million)
% 161.59/23.63 % (3037075)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2096987682:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2926 on theBenchmark for (2926ds/1997Mi)
% 161.59/23.63 % (3037075)Instruction limit reached!
% 161.59/23.63 % (3037075)------------------------------
% 161.59/23.63 % (3037075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.59/23.63 % (3037075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.59/23.63 % (3037075)CaDiCaL version: 2.1.3
% 161.59/23.63 % (3037075)Termination reason: Instruction limit
% 161.59/23.63 % (3037075)Termination phase: Saturation
% 161.59/23.63 % (3037075)Time elapsed: 2.034 s
% 161.59/23.63 % (3037075)Peak memory usage: 138 MB
% 161.59/23.63 % (3037075)Instructions burned: 1997 (million)
% 161.59/23.63 % (3037072)Instruction limit reached!
% 161.59/23.63 % (3037072)------------------------------
% 161.59/23.63 % (3037072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.59/23.63 % (3037072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.59/23.63 % (3037072)CaDiCaL version: 2.1.3
% 161.59/23.63 % (3037072)Termination reason: Instruction limit
% 161.59/23.63 % (3037072)Termination phase: Saturation
% 161.59/23.63 % (3037072)Time elapsed: 2.924 s
% 161.59/23.63 % (3037072)Peak memory usage: 146 MB
% 161.59/23.63 % (3037072)Instructions burned: 2989 (million)
% 161.59/23.63 % (3037077)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2542228473:i=2088:bd=preordered:av=off_2903 on theBenchmark for (2903ds/2088Mi)
% 161.59/23.63 % (3037061)Instruction limit reached!
% 161.59/23.63 % (3037061)------------------------------
% 161.59/23.63 % (3037061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.59/23.63 % (3037061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.59/23.63 % (3037061)CaDiCaL version: 2.1.3
% 161.59/23.63 % (3037061)Termination reason: Instruction limit
% 161.59/23.63 % (3037061)Termination phase: Saturation
% 161.59/23.63 % (3037061)Time elapsed: 5.312 s
% 161.59/23.63 % (3037061)Peak memory usage: 167 MB
% 161.59/23.63 % (3037061)Instructions burned: 10307 (million)
% 161.59/23.63 % (3037080)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2204392123:i=433:bd=preordered_2900 on theBenchmark for (2900ds/433Mi)
% 161.59/23.63 % (3037080)Refutation not found, incomplete strategy
% 161.59/23.63 % (3037080)------------------------------
% 161.59/23.63 % (3037080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.59/23.63 % (3037080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.59/23.63 % (3037080)CaDiCaL version: 2.1.3
% 161.59/23.63 % (3037080)Termination reason: Refutation not found, incomplete strategy
% 161.59/23.63 % (3037080)Time elapsed: 0.003 s
% 161.59/23.63 % (3037080)Peak memory usage: 88 MB
% 161.59/23.63 % (3037080)Instructions burned: 4 (million)
% 161.59/23.63 % (3037078)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1646962956:i=1098:nicw=on_2900 on theBenchmark for (2900ds/1098Mi)
% 161.59/23.63 % (3037080)------------------------------
% 161.59/23.63 % (3037080)------------------------------
% 161.59/23.63 % (3037083)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1742315854:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2895 on theBenchmark for (2895ds/2942Mi)
% 161.59/23.63 % (3037078)Instruction limit reached!
% 161.59/23.63 % (3037078)------------------------------
% 161.59/23.63 % (3037078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 161.59/23.63 % (3037078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 161.59/23.63 % (3037078)CaDiCaL version: 2.1.3
% 161.59/23.63 % (3037078)Termination reason: Instruction limit
% 161.59/23.63 % (3037078)Termination phase: Saturation
% 161.59/23.63 % (3037078)Time elapsed: 0.927 s
% 161.59/23.63 % (3037078)Peak memory usage: 93 MB
% 161.59/23.63 % (3037078)Instructions burned: 1099 (million)
% 161.59/23.63 % (3037087)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1015088501:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2888 on theBenchmark for (2888ds/6922Mi)
% 195.01/28.35 % (3037077)Instruction limit reached!
% 195.01/28.35 % (3037077)------------------------------
% 195.01/28.35 % (3037077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.01/28.35 % (3037077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.01/28.35 % (3037077)CaDiCaL version: 2.1.3
% 195.01/28.35 % (3037077)Termination reason: Instruction limit
% 195.01/28.35 % (3037077)Termination phase: Saturation
% 195.01/28.35 % (3037077)Time elapsed: 2.143 s
% 195.01/28.35 % (3037077)Peak memory usage: 137 MB
% 195.01/28.35 % (3037077)Instructions burned: 2089 (million)
% 195.01/28.35 % (3037083)Instruction limit reached!
% 195.01/28.35 % (3037083)------------------------------
% 195.01/28.35 % (3037083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.01/28.35 % (3037083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.01/28.35 % (3037083)CaDiCaL version: 2.1.3
% 195.01/28.35 % (3037083)Termination reason: Instruction limit
% 195.01/28.35 % (3037083)Termination phase: Saturation
% 195.01/28.35 % (3037083)Time elapsed: 1.703 s
% 195.01/28.35 % (3037083)Peak memory usage: 142 MB
% 195.01/28.35 % (3037083)Instructions burned: 2943 (million)
% 195.01/28.35 % (3037089)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=2484385545:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2879 on theBenchmark for (2879ds/596Mi)
% 195.01/28.35 % (3037089)Refutation not found, incomplete strategy
% 195.01/28.35 % (3037089)------------------------------
% 195.01/28.35 % (3037089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.01/28.35 % (3037089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.01/28.35 % (3037089)CaDiCaL version: 2.1.3
% 195.01/28.35 % (3037089)Termination reason: Refutation not found, incomplete strategy
% 195.01/28.35 % (3037089)Time elapsed: 0.004 s
% 195.01/28.35 % (3037089)Peak memory usage: 88 MB
% 195.01/28.35 % (3037089)Instructions burned: 3 (million)
% 195.01/28.35 % (3037090)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3616570891:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2876 on theBenchmark for (2876ds/4123Mi)
% 195.01/28.35 % (3037089)------------------------------
% 195.01/28.35 % (3037089)------------------------------
% 195.01/28.35 % (3037093)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2683257485:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2872 on theBenchmark for (2872ds/16411Mi)
% 195.01/28.35 % (3037064)Instruction limit reached!
% 195.01/28.35 % (3037064)------------------------------
% 195.01/28.35 % (3037064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.01/28.35 % (3037064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.01/28.35 % (3037064)CaDiCaL version: 2.1.3
% 195.01/28.35 % (3037064)Termination reason: Instruction limit
% 195.01/28.35 % (3037064)Termination phase: Saturation
% 195.01/28.35 % (3037064)Time elapsed: 8.478 s
% 195.01/28.35 % (3037064)Peak memory usage: 190 MB
% 195.01/28.35 % (3037064)Instructions burned: 8478 (million)
% 195.01/28.35 % (3037095)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3270081871:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2865 on theBenchmark for (2865ds/1670Mi)
% 195.01/28.35 % (3037090)Instruction limit reached!
% 195.01/28.35 % (3037090)------------------------------
% 195.01/28.35 % (3037090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 195.01/28.35 % (3037090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 195.01/28.35 % (3037090)CaDiCaL version: 2.1.3
% 195.01/28.35 % (3037090)Termination reason: Instruction limit
% 195.01/28.35 % (3037090)Termination phase: Saturation
% 195.01/28.35 % (3037090)Time elapsed: 2.360 s
% 195.01/28.35 % (3037090)Peak memory usage: 157 MB
% 195.01/28.35 % (3037090)Instructions burned: 4123 (million)
% 195.01/28.35 % (3037097)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=1874865509:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2850 on theBenchmark for (2850ds/1722Mi)
% 195.01/28.35 % (3037095)Instruction limit reached!
% 195.01/28.35 % (3037095)------------------------------
% 195.01/28.35 % (3037095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.36/31.24 % (3037095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.36/31.24 % (3037095)CaDiCaL version: 2.1.3
% 215.36/31.24 % (3037095)Termination reason: Instruction limit
% 215.36/31.24 % (3037095)Termination phase: Saturation
% 215.36/31.24 % (3037095)Time elapsed: 1.773 s
% 215.36/31.24 % (3037095)Peak memory usage: 135 MB
% 215.36/31.24 % (3037095)Instructions burned: 1670 (million)
% 215.36/31.24 % (3037099)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=265447973:cts=off:cond=on:i=9530:bs=on:fsd=on_2844 on theBenchmark for (2844ds/9530Mi)
% 215.36/31.24 % (3037097)Instruction limit reached!
% 215.36/31.24 % (3037097)------------------------------
% 215.36/31.24 % (3037097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.36/31.24 % (3037097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.36/31.24 % (3037097)CaDiCaL version: 2.1.3
% 215.36/31.24 % (3037097)Termination reason: Instruction limit
% 215.36/31.24 % (3037097)Termination phase: Saturation
% 215.36/31.24 % (3037097)Time elapsed: 0.949 s
% 215.36/31.24 % (3037097)Peak memory usage: 135 MB
% 215.36/31.24 % (3037097)Instructions burned: 1723 (million)
% 215.36/31.24 % (3037101)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1328016297:st=2:i=4495:sd=10:ss=included_2838 on theBenchmark for (2838ds/4495Mi)
% 215.36/31.24 % (3037087)Instruction limit reached!
% 215.36/31.24 % (3037087)------------------------------
% 215.36/31.24 % (3037087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.36/31.24 % (3037087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.36/31.24 % (3037087)CaDiCaL version: 2.1.3
% 215.36/31.24 % (3037087)Termination reason: Instruction limit
% 215.36/31.24 % (3037087)Termination phase: Saturation
% 215.36/31.24 % (3037087)Time elapsed: 6.028 s
% 215.36/31.24 % (3037087)Peak memory usage: 137 MB
% 215.36/31.24 % (3037087)Instructions burned: 6922 (million)
% 215.36/31.24 % (3037103)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=63671665:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2825 on theBenchmark for (2825ds/4920Mi)
% 215.36/31.24 % (3037101)Instruction limit reached!
% 215.36/31.24 % (3037101)------------------------------
% 215.36/31.24 % (3037101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.36/31.24 % (3037101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.36/31.24 % (3037101)CaDiCaL version: 2.1.3
% 215.36/31.24 % (3037101)Termination reason: Instruction limit
% 215.36/31.24 % (3037101)Termination phase: Saturation
% 215.36/31.24 % (3037101)Time elapsed: 2.258 s
% 215.36/31.24 % (3037101)Peak memory usage: 141 MB
% 215.36/31.24 % (3037101)Instructions burned: 4497 (million)
% 215.36/31.24 % (3037105)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2128105432:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2813 on theBenchmark for (2813ds/2083Mi)
% 215.36/31.24 % (3037105)Instruction limit reached!
% 215.36/31.24 % (3037105)------------------------------
% 215.36/31.24 % (3037105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.36/31.24 % (3037105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.36/31.24 % (3037105)CaDiCaL version: 2.1.3
% 215.36/31.24 % (3037105)Termination reason: Instruction limit
% 215.36/31.24 % (3037105)Termination phase: Saturation
% 215.36/31.24 % (3037105)Time elapsed: 1.147 s
% 215.36/31.24 % (3037105)Peak memory usage: 134 MB
% 215.36/31.24 % (3037105)Instructions burned: 2084 (million)
% 215.36/31.24 % (3037107)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=615859093:i=4629:av=off:gsp=on_2799 on theBenchmark for (2799ds/4629Mi)
% 215.36/31.24 % (3037103)Instruction limit reached!
% 215.36/31.24 % (3037103)------------------------------
% 215.36/31.24 % (3037103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 215.36/31.24 % (3037103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.36/31.24 % (3037103)CaDiCaL version: 2.1.3
% 215.36/31.24 % (3037103)Termination reason: Instruction limit
% 215.36/31.24 % (3037103)Termination phase: Saturation
% 215.36/31.24 % (3037103)Time elapsed: 5.027 s
% 215.36/31.24 % (3037103)Peak memory usage: 161 MB
% 241.58/34.94 % (3037103)Instructions burned: 4920 (million)
% 241.58/34.94 % (3037107)Instruction limit reached!
% 241.58/34.94 % (3037107)------------------------------
% 241.58/34.94 % (3037107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 241.58/34.94 % (3037107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.58/34.94 % (3037107)CaDiCaL version: 2.1.3
% 241.58/34.94 % (3037107)Termination reason: Instruction limit
% 241.58/34.94 % (3037107)Termination phase: Saturation
% 241.58/34.94 % (3037107)Time elapsed: 2.601 s
% 241.58/34.94 % (3037107)Peak memory usage: 154 MB
% 241.58/34.94 % (3037107)Instructions burned: 4630 (million)
% 241.58/34.94 % (3037109)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=731606392:i=1258:av=off_2772 on theBenchmark for (2772ds/1258Mi)
% 241.58/34.94 % (3037110)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2071413306:i=7343:av=off:ss=included_2771 on theBenchmark for (2771ds/7343Mi)
% 241.58/34.94 % (3037109)Instruction limit reached!
% 241.58/34.94 % (3037109)------------------------------
% 241.58/34.94 % (3037109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 241.58/34.94 % (3037109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.58/34.94 % (3037109)CaDiCaL version: 2.1.3
% 241.58/34.94 % (3037109)Termination reason: Instruction limit
% 241.58/34.94 % (3037109)Termination phase: Saturation
% 241.58/34.94 % (3037109)Time elapsed: 1.175 s
% 241.58/34.94 % (3037109)Peak memory usage: 96 MB
% 241.58/34.94 % (3037109)Instructions burned: 1258 (million)
% 241.58/34.94 % (3037115)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=533664526:i=1325:sd=2:ss=axioms:sgt=16_2757 on theBenchmark for (2757ds/1325Mi)
% 241.58/34.94 % (3037115)Refutation not found, incomplete strategy
% 241.58/34.94 % (3037115)------------------------------
% 241.58/34.94 % (3037115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 241.58/34.94 % (3037115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.58/34.94 % (3037115)CaDiCaL version: 2.1.3
% 241.58/34.94 % (3037115)Termination reason: Refutation not found, incomplete strategy
% 241.58/34.94 % (3037115)Time elapsed: 0.003 s
% 241.58/34.94 % (3037115)Peak memory usage: 88 MB
% 241.58/34.94 % (3037115)Instructions burned: 2 (million)
% 241.58/34.94 % (3037115)------------------------------
% 241.58/34.94 % (3037115)------------------------------
% 241.58/34.94 % (3037117)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=1194675274:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2750 on theBenchmark for (2750ds/2646Mi)
% 241.58/34.94 % (3037099)Instruction limit reached!
% 241.58/34.94 % (3037099)------------------------------
% 241.58/34.94 % (3037099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 241.58/34.94 % (3037099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.58/34.94 % (3037099)CaDiCaL version: 2.1.3
% 241.58/34.94 % (3037099)Termination reason: Instruction limit
% 241.58/34.94 % (3037099)Termination phase: Saturation
% 241.58/34.94 % (3037099)Time elapsed: 9.546 s
% 241.58/34.94 % (3037099)Peak memory usage: 188 MB
% 241.58/34.94 % (3037099)Instructions burned: 9531 (million)
% 241.58/34.94 % (3037119)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2041234634:i=1489:sd=2:ep=R:ss=axioms_2746 on theBenchmark for (2746ds/1489Mi)
% 241.58/34.94 % (3037119)Refutation not found, incomplete strategy
% 241.58/34.94 % (3037119)------------------------------
% 241.58/34.94 % (3037119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 241.58/34.94 % (3037119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 241.58/34.94 % (3037119)CaDiCaL version: 2.1.3
% 241.58/34.94 % (3037119)Termination reason: Refutation not found, incomplete strategy
% 241.58/34.94 % (3037119)Time elapsed: 0.924 s
% 241.58/34.94 % (3037119)Peak memory usage: 127 MB
% 241.58/34.94 % (3037119)Instructions burned: 896 (million)
% 241.58/34.94 % (3037119)------------------------------
% 241.58/34.94 % (3037119)------------------------------
% 241.58/34.94 % (3037123)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=3256992251:i=1503_2731 on theBenchmark for (2731ds/1503Mi)
% 241.58/34.94 % (3037117)Instruction limit reached!
% 241.58/34.94 % (3037117)------------------------------
% 241.58/34.94 % (3037117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.86 % (3037117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.86 % (3037117)CaDiCaL version: 2.1.3
% 247.11/35.86 % (3037117)Termination reason: Instruction limit
% 247.11/35.86 % (3037117)Termination phase: Saturation
% 247.11/35.86 % (3037117)Time elapsed: 2.186 s
% 247.11/35.86 % (3037117)Peak memory usage: 142 MB
% 247.11/35.86 % (3037117)Instructions burned: 2648 (million)
% 247.11/35.86 % (3037123)Refutation not found, incomplete strategy
% 247.11/35.86 % (3037123)------------------------------
% 247.11/35.86 % (3037123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.86 % (3037123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.86 % (3037123)CaDiCaL version: 2.1.3
% 247.11/35.86 % (3037123)Termination reason: Refutation not found, incomplete strategy
% 247.11/35.86 % (3037123)Time elapsed: 0.569 s
% 247.11/35.86 % (3037123)Peak memory usage: 128 MB
% 247.11/35.86 % (3037123)Instructions burned: 870 (million)
% 247.11/35.86 % (3037227)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=599182358:i=13942:kws=frequency_2725 on theBenchmark for (2725ds/13942Mi)
% 247.11/35.86 % (3037123)------------------------------
% 247.11/35.86 % (3037123)------------------------------
% 247.11/35.86 % (3037280)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=4180223223:i=3604:fsr=off:er=filter_2721 on theBenchmark for (2721ds/3604Mi)
% 247.11/35.86 % (3037110)Instruction limit reached!
% 247.11/35.86 % (3037110)------------------------------
% 247.11/35.86 % (3037110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.86 % (3037110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.86 % (3037110)CaDiCaL version: 2.1.3
% 247.11/35.86 % (3037110)Termination reason: Instruction limit
% 247.11/35.86 % (3037110)Termination phase: Saturation
% 247.11/35.86 % (3037110)Time elapsed: 5.099 s
% 247.11/35.86 % (3037110)Peak memory usage: 165 MB
% 247.11/35.86 % (3037110)Instructions burned: 7345 (million)
% 247.11/35.86 % (3037282)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=4164128411:i=1876:sd=1:ss=included:sgt=32_2717 on theBenchmark for (2717ds/1876Mi)
% 247.11/35.86 % (3037282)Instruction limit reached!
% 247.11/35.86 % (3037282)------------------------------
% 247.11/35.86 % (3037282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.86 % (3037282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.86 % (3037282)CaDiCaL version: 2.1.3
% 247.11/35.86 % (3037282)Termination reason: Instruction limit
% 247.11/35.86 % (3037282)Termination phase: Saturation
% 247.11/35.86 % (3037282)Time elapsed: 1.131 s
% 247.11/35.86 % (3037282)Peak memory usage: 136 MB
% 247.11/35.86 % (3037282)Instructions burned: 1876 (million)
% 247.11/35.86 % (3037284)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2706831170:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2704 on theBenchmark for (2704ds/1932Mi)
% 247.11/35.86 % (3037280)Instruction limit reached!
% 247.11/35.86 % (3037280)------------------------------
% 247.11/35.86 % (3037280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.86 % (3037280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.86 % (3037280)CaDiCaL version: 2.1.3
% 247.11/35.86 % (3037280)Termination reason: Instruction limit
% 247.11/35.86 % (3037280)Termination phase: Saturation
% 247.11/35.86 % (3037280)Time elapsed: 2.133 s
% 247.11/35.86 % (3037280)Peak memory usage: 147 MB
% 247.11/35.86 % (3037280)Instructions burned: 3605 (million)
% 247.11/35.86 % (3037286)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=385369738:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2698 on theBenchmark for (2698ds/1980Mi)
% 247.11/35.86 % (3037284)Refutation not found, incomplete strategy
% 247.11/35.86 % (3037284)------------------------------
% 247.11/35.86 % (3037284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.86 % (3037284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.86 % (3037284)CaDiCaL version: 2.1.3
% 247.11/35.86 % (3037284)Termination reason: Refutation not found, incomplete strategy
% 247.11/35.86 % (3037284)Time elapsed: 0.683 s
% 247.11/35.87 % (3037284)Peak memory usage: 127 MB
% 247.11/35.87 % (3037284)Instructions burned: 878 (million)
% 247.11/35.87 % (3037284)------------------------------
% 247.11/35.87 % (3037284)------------------------------
% 247.11/35.87 % (3037093)Instruction limit reached!
% 247.11/35.87 % (3037093)------------------------------
% 247.11/35.87 % (3037093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.87 % (3037093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.87 % (3037093)CaDiCaL version: 2.1.3
% 247.11/35.87 % (3037093)Termination reason: Instruction limit
% 247.11/35.87 % (3037093)Termination phase: Saturation
% 247.11/35.87 % (3037093)Time elapsed: 17.596 s
% 247.11/35.87 % (3037093)Peak memory usage: 168 MB
% 247.11/35.87 % (3037093)Instructions burned: 16412 (million)
% 247.11/35.87 % (3037288)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=297165501:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2694 on theBenchmark for (2694ds/3902Mi)
% 247.11/35.87 % (3037289)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=158079877:avsq=on:i=3916:aac=none:amm=off_2693 on theBenchmark for (2693ds/3916Mi)
% 247.11/35.87 % (3037288)Refutation not found, incomplete strategy
% 247.11/35.87 % (3037288)------------------------------
% 247.11/35.87 % (3037288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.87 % (3037288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.87 % (3037288)CaDiCaL version: 2.1.3
% 247.11/35.87 % (3037288)Termination reason: Refutation not found, incomplete strategy
% 247.11/35.87 % (3037288)Time elapsed: 0.578 s
% 247.11/35.87 % (3037288)Peak memory usage: 128 MB
% 247.11/35.87 % (3037288)Instructions burned: 876 (million)
% 247.11/35.87 % (3037288)------------------------------
% 247.11/35.87 % (3037288)------------------------------
% 247.11/35.87 % (3037286)Instruction limit reached!
% 247.11/35.87 % (3037286)------------------------------
% 247.11/35.87 % (3037286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.87 % (3037286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.87 % (3037286)CaDiCaL version: 2.1.3
% 247.11/35.87 % (3037286)Termination reason: Instruction limit
% 247.11/35.87 % (3037286)Termination phase: Saturation
% 247.11/35.87 % (3037286)Time elapsed: 1.248 s
% 247.11/35.87 % (3037286)Peak memory usage: 136 MB
% 247.11/35.87 % (3037286)Instructions burned: 1981 (million)
% 247.11/35.87 % (3037292)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=2268620522:cond=on:i=3940:av=off:er=known_2684 on theBenchmark for (2684ds/3940Mi)
% 247.11/35.87 % (3037293)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1107687909:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2684 on theBenchmark for (2684ds/3980Mi)
% 247.11/35.87 % (3037289)Instruction limit reached!
% 247.11/35.87 % (3037289)------------------------------
% 247.11/35.87 % (3037289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.87 % (3037289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.87 % (3037289)CaDiCaL version: 2.1.3
% 247.11/35.87 % (3037289)Termination reason: Instruction limit
% 247.11/35.87 % (3037289)Termination phase: Saturation
% 247.11/35.87 % (3037289)Time elapsed: 2.183 s
% 247.11/35.87 % (3037289)Peak memory usage: 123 MB
% 247.11/35.87 % (3037289)Instructions burned: 3917 (million)
% 247.11/35.87 % (3037296)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=1547823521:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2669 on theBenchmark for (2669ds/2087Mi)
% 247.11/35.87 % (3037292)Instruction limit reached!
% 247.11/35.87 % (3037292)------------------------------
% 247.11/35.87 % (3037292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.87 % (3037292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.87 % (3037292)CaDiCaL version: 2.1.3
% 247.11/35.87 % (3037292)Termination reason: Instruction limit
% 247.11/35.87 % (3037292)Termination phase: Saturation
% 247.11/35.87 % (3037292)Time elapsed: 2.169 s
% 247.11/35.87 % (3037292)Peak memory usage: 152 MB
% 247.11/35.87 % (3037292)Instructions burned: 3940 (million)
% 247.11/35.87 % (3037299)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1597239384:cts=off:cond=on:i=4272:bs=on:fsd=on_2660 on theBenchmark for (2660ds/4272Mi)
% 247.11/35.87 % (3037293)Instruction limit reached!
% 247.11/35.87 % (3037293)------------------------------
% 247.11/35.87 % (3037293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.87 % (3037293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.87 % (3037293)CaDiCaL version: 2.1.3
% 247.11/35.87 % (3037293)Termination reason: Instruction limit
% 247.11/35.87 % (3037293)Termination phase: Saturation
% 247.11/35.87 % (3037293)Time elapsed: 2.618 s
% 247.11/35.87 % (3037293)Peak memory usage: 156 MB
% 247.11/35.87 % (3037293)Instructions burned: 3981 (million)
% 247.11/35.87 % (3037296)Instruction limit reached!
% 247.11/35.87 % (3037296)------------------------------
% 247.11/35.87 % (3037296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 247.11/35.87 % (3037296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 247.11/35.87 % (3037296)CaDiCaL version: 2.1.3
% 247.11/35.87 % (3037296)Termination reason: Instruction limit
% 247.11/35.87 % (3037296)Termination phase: Saturation
% 247.11/35.87 % (3037296)Time elapsed: 1.277 s
% 247.11/35.87 % (3037296)Peak memory usage: 140 MB
% 247.11/35.87 % (3037296)Instructions burned: 2088 (million)
% 247.11/35.87 % (3037301)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=212304107:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2656 on theBenchmark for (2656ds/2197Mi)
% 247.11/35.87 % (3037302)dis+21_1_sil=8000:spb=goal_then_units:random_seed=3204466996:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2655 on theBenchmark for (2655ds/6508Mi)
% 247.11/35.87 % (3037302)First to succeed.
% 247.11/35.87 % (3037302)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3037004"
% 247.11/35.87 % (3037302)Refutation found. Thanks to Tanya!
% 247.11/35.87 % SZS status Unsatisfiable for theBenchmark
% 247.11/35.87 % SZS output start Proof for theBenchmark
% See solution above
% 248.60/36.06 % (3037302)------------------------------
% 248.60/36.06 % (3037302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 248.60/36.06 % (3037302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 248.60/36.06 % (3037302)CaDiCaL version: 2.1.3
% 248.60/36.06 % (3037302)Termination reason: Refutation
% 248.60/36.06 % (3037302)Time elapsed: 0.070 s
% 248.60/36.06 % (3037302)Peak memory usage: 90 MB
% 248.60/36.06 % (3037302)Instructions burned: 122 (million)
% 248.60/36.06 % (3037302)------------------------------
% 248.60/36.06 % (3037302)------------------------------
% 248.60/36.06 % (3037004)Success in time 34.982 s
% 248.60/36.06 % Vampire exiting
%------------------------------------------------------------------------------