%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW437-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:20 PM UTC 2026
% Result : Unsatisfiable 6.24s 1.68s
% Output : Refutation 7.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 10
% Syntax : Number of formulae : 133 ( 30 unt; 4 def)
% Number of atoms : 326 ( 64 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 367 ( 174 ~; 189 |; 0 &)
% ( 4 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 92 ( 0 sgn 92 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : sep(X0,sep(X1,X2)) = sep(X1,sep(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associative_commutative) ).
fof(f2,axiom,
! [X0,X1] : sep(lseg(X0,X0),X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',normalization) ).
fof(f8,axiom,
! [X2,X3,X0,X1] :
( ~ heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wellformedness_5) ).
fof(f19,axiom,
x3 != x8,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_6) ).
fof(f24,axiom,
x7 != x16,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_10) ).
fof(f53,axiom,
heap(sep(lseg(x5,x1),sep(lseg(x12,x8),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',premise_27) ).
fof(f58,plain,
! [X2,X3,X0,X1] : sep(X1,sep(X3,sep(X0,X2))) = sep(X3,sep(X0,sep(X1,X2))),
inference(superposition,[],[f1,f1]) ).
fof(f70,plain,
heap(sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x2,x6),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(superposition,[],[f53,f1]) ).
fof(f71,plain,
heap(sep(lseg(x2,x6),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x16,x7),sep(lseg(x16,x3),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f70,f58]) ).
fof(f83,plain,
heap(sep(lseg(x2,x6),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f71,f1]) ).
fof(f95,plain,
heap(sep(lseg(x2,x6),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x10,x15),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f83,f58]) ).
fof(f107,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x10,x5),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f95,f58]) ).
fof(f119,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x10,x5),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f107,f58]) ).
fof(f131,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f119,f58]) ).
fof(f143,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x16,x3),sep(lseg(x3,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f131,f58]) ).
fof(f155,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),sep(lseg(x3,x16),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f143,f1]) ).
fof(f167,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x16,x3),sep(lseg(x3,x16),sep(lseg(x16,x7),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f155,f58]) ).
fof(f179,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),sep(lseg(x11,x8),emp)))))))))))),
inference(forward_demodulation,[],[f167,f1]) ).
fof(f191,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x11,x8),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))),
inference(forward_demodulation,[],[f179,f58]) ).
fof(f203,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x11,x8),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))),
inference(forward_demodulation,[],[f191,f58]) ).
fof(f215,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x12,x8),sep(lseg(x11,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))),
inference(forward_demodulation,[],[f203,f58]) ).
fof(f227,plain,
heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))),
inference(forward_demodulation,[],[f215,f1]) ).
fof(f282,plain,
! [X2,X3,X0,X1] : sep(X0,sep(X1,sep(X2,X3))) = sep(X0,sep(X2,sep(X1,X3))),
inference(superposition,[],[f1,f58]) ).
fof(f297,plain,
! [X2,X3,X0,X1,X4] :
( ~ heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f8,f58]) ).
fof(f398,plain,
( x15 = x10
| x10 = x5 ),
inference(resolution,[],[f297,f227]) ).
fof(f405,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ heap(sep(X5,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4)))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f297,f58]) ).
fof(f413,definition,
( spl0_1
<=> x10 = x5 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f415,plain,
( x10 = x5
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f413]) ).
fof(f417,definition,
( spl0_2
<=> x15 = x10 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f419,plain,
( x15 = x10
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f417]) ).
fof(f420,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f398,f417,f413]) ).
fof(f421,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x15,x15),sep(lseg(x15,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_2 ),
inference(backward_demodulation,[],[f227,f419]) ).
fof(f427,plain,
( heap(sep(lseg(x15,x15),sep(lseg(x2,x6),sep(lseg(x15,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f421,f1]) ).
fof(f429,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x15,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f427,f2]) ).
fof(f431,plain,
( heap(sep(lseg(x15,x5),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_2 ),
inference(forward_demodulation,[],[f429,f1]) ).
fof(f447,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f405,f58]) ).
fof(f465,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X7,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4)))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f447,f58]) ).
fof(f466,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X7,sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4)))))))
| X0 = X3
| X0 = X1 ),
inference(superposition,[],[f447,f58]) ).
fof(f488,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X7,sep(X8,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f465,f58]) ).
fof(f510,plain,
( x12 = x3
| x16 = x3
| ~ spl0_2 ),
inference(resolution,[],[f488,f431]) ).
fof(f517,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X7,sep(X8,sep(X9,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4)))))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f488,f58]) ).
fof(f545,definition,
( spl0_3
<=> x16 = x3 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f546,plain,
( x16 != x3
| spl0_3 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f547,plain,
( x16 = x3
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f549,definition,
( spl0_4
<=> x12 = x3 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f550,plain,
( x12 != x3
| spl0_4 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f551,plain,
( x12 = x3
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f552,plain,
( spl0_3
| spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f510,f417,f549,f545]) ).
fof(f554,plain,
( x7 != x3
| ~ spl0_3 ),
inference(backward_demodulation,[],[f24,f547]) ).
fof(f558,plain,
( heap(sep(lseg(x15,x5),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x3),sep(lseg(x3,x3),sep(lseg(x3,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(backward_demodulation,[],[f431,f547]) ).
fof(f559,plain,
( heap(sep(lseg(x15,x5),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x3),sep(lseg(x3,x7),sep(lseg(x7,x1),emp))))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f558,f2]) ).
fof(f560,plain,
( heap(sep(lseg(x15,x5),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x7),sep(lseg(x7,x1),emp)))))))))
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_demodulation,[],[f559,f2]) ).
fof(f561,plain,
( x12 = x3
| x7 = x3
| ~ spl0_2
| ~ spl0_3 ),
inference(resolution,[],[f560,f488]) ).
fof(f562,plain,
( x12 = x3
| ~ spl0_2
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f561,f554]) ).
fof(f563,plain,
( spl0_4
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f562,f545,f417,f549]) ).
fof(f565,plain,
( x12 != x8
| ~ spl0_4 ),
inference(backward_demodulation,[],[f19,f551]) ).
fof(f568,plain,
( x16 = x12
| ~ spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f547,f551]) ).
fof(f569,plain,
( x7 != x12
| ~ spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f554,f551]) ).
fof(f573,plain,
( heap(sep(lseg(x15,x5),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x12),sep(lseg(x12,x7),sep(lseg(x7,x1),emp)))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f560,f551]) ).
fof(f574,plain,
( heap(sep(lseg(x15,x5),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x12),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x7),sep(lseg(x7,x1),emp)))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f573,f58]) ).
fof(f575,plain,
( heap(sep(lseg(x15,x5),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f574,f2]) ).
fof(f618,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ heap(sep(X5,sep(X6,sep(X7,sep(X8,sep(X9,sep(X10,sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))))))))
| X1 = X2
| X1 = X3 ),
inference(superposition,[],[f517,f58]) ).
fof(f941,plain,
! [X2,X3,X0,X1,X4,X5] : sep(X4,sep(X5,sep(X0,sep(X1,sep(X2,X3))))) = sep(X4,sep(X2,sep(X5,sep(X0,sep(X1,X3))))),
inference(superposition,[],[f282,f58]) ).
fof(f948,plain,
! [X2,X3,X0,X1,X4] : sep(X4,sep(X0,sep(X1,sep(X2,X3)))) = sep(X4,sep(X0,sep(X2,sep(X1,X3)))),
inference(superposition,[],[f282,f58]) ).
fof(f1445,plain,
( x7 = x12
| x12 = x8
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4 ),
inference(resolution,[],[f466,f575]) ).
fof(f1499,plain,
( x12 = x8
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1445,f569]) ).
fof(f1500,plain,
( $false
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1499,f565]) ).
fof(f1501,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f1500]) ).
fof(f1503,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x12),sep(lseg(x12,x3),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f227,f568]) ).
fof(f1508,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x12,x3),sep(lseg(x3,x12),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1503,f948]) ).
fof(f1511,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x3),sep(lseg(x3,x12),sep(lseg(x3,x12),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1508,f948]) ).
fof(f1513,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x12),sep(lseg(x12,x12),sep(lseg(x12,x12),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1511,f551]) ).
fof(f1515,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x12,x12),sep(lseg(x5,x1),sep(lseg(x12,x12),sep(lseg(x12,x12),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1513,f948]) ).
fof(f1517,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x12),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x12),sep(lseg(x12,x12),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1515,f948]) ).
fof(f1519,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x12),sep(lseg(x12,x12),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x12),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1517,f941]) ).
fof(f1521,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x12),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x12),sep(lseg(x12,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1519,f2]) ).
fof(f1523,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x12),sep(lseg(x12,x12),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1521,f941]) ).
fof(f1525,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x12),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1523,f2]) ).
fof(f1527,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x7),sep(lseg(x7,x1),emp)))))))))
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1525,f2]) ).
fof(f1529,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x5,x15),sep(lseg(x5,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x7),sep(lseg(x7,x1),emp)))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1527,f415]) ).
fof(f1531,plain,
( heap(sep(lseg(x5,x15),sep(lseg(x2,x6),sep(lseg(x5,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x7),sep(lseg(x7,x1),emp)))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1529,f1]) ).
fof(f1533,plain,
( heap(sep(lseg(x5,x15),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x7),sep(lseg(x7,x1),emp))))))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1531,f2]) ).
fof(f1544,plain,
( x7 = x12
| x12 = x8
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(resolution,[],[f1533,f466]) ).
fof(f1545,plain,
( x12 = x8
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1544,f569]) ).
fof(f1546,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1545,f565]) ).
fof(f1547,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f1546]) ).
fof(f1548,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x3),sep(lseg(x3,x3),sep(lseg(x3,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f227,f547]) ).
fof(f1551,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x3),sep(lseg(x3,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1548,f2]) ).
fof(f1553,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x7),sep(lseg(x7,x1),emp))))))))))
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1551,f2]) ).
fof(f1555,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x5,x15),sep(lseg(x5,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x7),sep(lseg(x7,x1),emp))))))))))
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1553,f415]) ).
fof(f1557,plain,
( heap(sep(lseg(x5,x15),sep(lseg(x2,x6),sep(lseg(x5,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x7),sep(lseg(x7,x1),emp))))))))))
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1555,f1]) ).
fof(f1559,plain,
( heap(sep(lseg(x5,x15),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x7),sep(lseg(x7,x1),emp)))))))))
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1557,f2]) ).
fof(f1561,plain,
( x12 = x3
| x7 = x3
| ~ spl0_1
| ~ spl0_3 ),
inference(resolution,[],[f1559,f488]) ).
fof(f1562,plain,
( x7 = x3
| ~ spl0_1
| ~ spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1561,f550]) ).
fof(f1563,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f1562,f554]) ).
fof(f1564,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_4 ),
inference(avatar_contradiction_clause,[],[f1563]) ).
fof(f1565,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x5,x15),sep(lseg(x5,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f227,f415]) ).
fof(f1567,plain,
( heap(sep(lseg(x5,x15),sep(lseg(x2,x6),sep(lseg(x5,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1565,f1]) ).
fof(f1569,plain,
( heap(sep(lseg(x5,x15),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x3,x12),sep(lseg(x3,x16),sep(lseg(x16,x3),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1567,f2]) ).
fof(f1572,plain,
( x16 = x3
| x7 = x16
| ~ spl0_1 ),
inference(resolution,[],[f1569,f618]) ).
fof(f1573,plain,
( x7 = x16
| ~ spl0_1
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f1572,f546]) ).
fof(f1575,plain,
( $false
| ~ spl0_1
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f1573,f24]) ).
fof(f1576,plain,
( ~ spl0_1
| spl0_3 ),
inference(avatar_contradiction_clause,[],[f1575]) ).
fof(f1581,plain,
( x12 != x8
| ~ spl0_4 ),
inference(backward_demodulation,[],[f19,f551]) ).
fof(f1584,plain,
( x16 != x12
| spl0_3
| ~ spl0_4 ),
inference(backward_demodulation,[],[f546,f551]) ).
fof(f1588,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x12),sep(lseg(x12,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f227,f551]) ).
fof(f1590,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x12,x12),sep(lseg(x5,x1),sep(lseg(x12,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1588,f948]) ).
fof(f1592,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x12),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1590,f948]) ).
fof(f1594,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x10,x15),sep(lseg(x10,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1592,f2]) ).
fof(f1596,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x15,x15),sep(lseg(x15,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1594,f419]) ).
fof(f1598,plain,
( heap(sep(lseg(x15,x15),sep(lseg(x2,x6),sep(lseg(x15,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),emp)))))))))))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1596,f1]) ).
fof(f1600,plain,
( heap(sep(lseg(x2,x6),sep(lseg(x15,x5),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1598,f2]) ).
fof(f1602,plain,
( heap(sep(lseg(x15,x5),sep(lseg(x2,x6),sep(lseg(x11,x8),sep(lseg(x12,x8),sep(lseg(x5,x1),sep(lseg(x12,x16),sep(lseg(x16,x12),sep(lseg(x16,x7),sep(lseg(x7,x1),emp))))))))))
| ~ spl0_2
| ~ spl0_4 ),
inference(forward_demodulation,[],[f1600,f1]) ).
fof(f1604,plain,
( x16 = x12
| x12 = x8
| ~ spl0_2
| ~ spl0_4 ),
inference(resolution,[],[f1602,f466]) ).
fof(f1607,plain,
( x12 = x8
| ~ spl0_2
| spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1604,f1584]) ).
fof(f1610,plain,
( $false
| ~ spl0_2
| spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f1607,f1581]) ).
fof(f1611,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_4 ),
inference(avatar_contradiction_clause,[],[f1610]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f420]) ).
cnf(s2,plain,
( ~ spl0_2
| spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f552]) ).
cnf(s3,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f563]) ).
cnf(s4,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s5,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s6,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f1564]) ).
cnf(s7,plain,
( ~ spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s10,plain,
( ~ spl0_2
| spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f1611]) ).
cnf(s11,plain,
( spl0_3
| ~ spl0_2 ),
inference(rat,[],[s2,s10]) ).
cnf(s12,plain,
( ~ spl0_3
| ~ spl0_2 ),
inference(rat,[],[s4,s3]) ).
cnf(s13,plain,
~ spl0_2,
inference(rat,[],[s12,s11]) ).
cnf(s14,plain,
spl0_1,
inference(rat,[],[s1,s13]) ).
cnf(s15,plain,
spl0_3,
inference(rat,[],[s7,s14]) ).
cnf(s16,plain,
spl0_4,
inference(rat,[],[s6,s15,s14]) ).
cnf(s17,plain,
$false,
inference(rat,[],[s5,s15,s16,s14]) ).
fof(f1612,plain,
$false,
inference(avatar_sat_refutation,[],[s17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW437-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n004.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 13:55:07 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.24/1.68 % (365481)Input is clausal, will run a generic CNF schedule.
% 6.24/1.68 % (365486)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=2971310014:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.24/1.68 % (365488)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1945290023:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.24/1.68 % (365489)lrs+10_1_sil=8000:sp=occurrence:random_seed=1260836137:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.24/1.68 % (365491)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2165160415:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.24/1.68 % (365490)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3161358717:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.24/1.68 % (365487)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2798501123:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.24/1.68 % (365492)dis-21_1_sil=8000:lcm=predicate:random_seed=1507169283: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)
% 6.24/1.68 % (365492)Refutation not found, incomplete strategy
% 6.24/1.68 % (365492)------------------------------
% 6.24/1.68 % (365492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365492)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365492)Termination reason: Refutation not found, incomplete strategy
% 6.24/1.68 % (365492)Time elapsed: 0.012 s
% 6.24/1.68 % (365492)Peak memory usage: 88 MB
% 6.24/1.68 % (365492)Instructions burned: 21 (million)
% 6.24/1.68 % (365489)Instruction limit reached!
% 6.24/1.68 % (365489)------------------------------
% 6.24/1.68 % (365489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365489)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365489)Termination reason: Instruction limit
% 6.24/1.68 % (365489)Termination phase: Saturation
% 6.24/1.68 % (365489)Time elapsed: 0.055 s
% 6.24/1.68 % (365489)Peak memory usage: 88 MB
% 6.24/1.68 % (365489)Instructions burned: 107 (million)
% 6.24/1.68 % (365490)Instruction limit reached!
% 6.24/1.68 % (365490)------------------------------
% 6.24/1.68 % (365490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365490)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365490)Termination reason: Instruction limit
% 6.24/1.68 % (365490)Termination phase: Saturation
% 6.24/1.68 % (365490)Time elapsed: 0.066 s
% 6.24/1.68 % (365490)Peak memory usage: 88 MB
% 6.24/1.68 % (365490)Instructions burned: 115 (million)
% 6.24/1.68 % (365491)Instruction limit reached!
% 6.24/1.68 % (365491)------------------------------
% 6.24/1.68 % (365491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365491)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365491)Termination reason: Instruction limit
% 6.24/1.68 % (365491)Termination phase: Saturation
% 6.24/1.68 % (365491)Time elapsed: 0.102 s
% 6.24/1.68 % (365491)Peak memory usage: 89 MB
% 6.24/1.68 % (365491)Instructions burned: 180 (million)
% 6.24/1.68 % (365500)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=3561855119:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.24/1.68 % (365500)Refutation not found, incomplete strategy
% 6.24/1.68 % (365500)------------------------------
% 6.24/1.68 % (365500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365500)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365500)Termination reason: Refutation not found, incomplete strategy
% 6.24/1.68 % (365500)Time elapsed: 0.003 s
% 6.24/1.68 % (365500)Peak memory usage: 88 MB
% 6.24/1.68 % (365500)Instructions burned: 4 (million)
% 6.24/1.68 % (365501)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1866552296:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 6.24/1.68 % (365502)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2424779119:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.24/1.68 % (365502)Refutation not found, incomplete strategy
% 6.24/1.68 % (365502)------------------------------
% 6.24/1.68 % (365502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365502)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365502)Termination reason: Refutation not found, incomplete strategy
% 6.24/1.68 % (365502)Time elapsed: 0.002 s
% 6.24/1.68 % (365502)Peak memory usage: 88 MB
% 6.24/1.68 % (365502)Instructions burned: 3 (million)
% 6.24/1.68 % (365492)------------------------------
% 6.24/1.68 % (365492)------------------------------
% 6.24/1.68 % (365501)Instruction limit reached!
% 6.24/1.68 % (365501)------------------------------
% 6.24/1.68 % (365501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365501)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365501)Termination reason: Instruction limit
% 6.24/1.68 % (365501)Termination phase: Saturation
% 6.24/1.68 % (365501)Time elapsed: 0.112 s
% 6.24/1.68 % (365501)Peak memory usage: 91 MB
% 6.24/1.68 % (365501)Instructions burned: 190 (million)
% 6.24/1.68 % (365506)lrs+10_64_to=lpo:sil=8000:random_seed=4198524857:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 6.24/1.68 % (365507)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=453350871:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 6.24/1.68 % (365500)------------------------------
% 6.24/1.68 % (365500)------------------------------
% 6.24/1.68 % (365502)------------------------------
% 6.24/1.68 % (365502)------------------------------
% 6.24/1.68 % (365506)Instruction limit reached!
% 6.24/1.68 % (365506)------------------------------
% 6.24/1.68 % (365506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365506)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365506)Termination reason: Instruction limit
% 6.24/1.68 % (365506)Termination phase: Saturation
% 6.24/1.68 % (365506)Time elapsed: 0.072 s
% 6.24/1.68 % (365506)Peak memory usage: 88 MB
% 6.24/1.68 % (365506)Instructions burned: 126 (million)
% 6.24/1.68 % (365507)Instruction limit reached!
% 6.24/1.68 % (365507)------------------------------
% 6.24/1.68 % (365507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365507)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365507)Termination reason: Instruction limit
% 6.24/1.68 % (365507)Termination phase: Saturation
% 6.24/1.68 % (365507)Time elapsed: 0.060 s
% 6.24/1.68 % (365507)Peak memory usage: 89 MB
% 6.24/1.68 % (365507)Instructions burned: 196 (million)
% 6.24/1.68 % (365510)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4028545137:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.24/1.68 % (365513)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3659010415:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 6.24/1.68 % (365513)Refutation not found, incomplete strategy
% 6.24/1.68 % (365513)------------------------------
% 6.24/1.68 % (365513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365513)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365513)Termination reason: Refutation not found, incomplete strategy
% 6.24/1.68 % (365513)Time elapsed: 0.001 s
% 6.24/1.68 % (365513)Peak memory usage: 87 MB
% 6.24/1.68 % (365513)Instructions burned: 3 (million)
% 6.24/1.68 % (365511)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2093354936:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 6.24/1.68 % (365512)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=464034026:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 6.24/1.68 % (365510)Instruction limit reached!
% 6.24/1.68 % (365510)------------------------------
% 6.24/1.68 % (365510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365510)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365510)Termination reason: Instruction limit
% 6.24/1.68 % (365510)Termination phase: Saturation
% 6.24/1.68 % (365510)Time elapsed: 0.089 s
% 6.24/1.68 % (365510)Peak memory usage: 89 MB
% 6.24/1.68 % (365510)Instructions burned: 159 (million)
% 6.24/1.68 % (365512)Instruction limit reached!
% 6.24/1.68 % (365512)------------------------------
% 6.24/1.68 % (365512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.24/1.68 % (365512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.68 % (365512)CaDiCaL version: 2.1.3
% 6.24/1.68 % (365512)Termination reason: Instruction limit
% 6.24/1.68 % (365512)Termination phase: Saturation
% 6.24/1.68 % (365512)Time elapsed: 0.059 s
% 6.24/1.68 % (365512)Peak memory usage: 88 MB
% 6.24/1.68 % (365512)Instructions burned: 106 (million)
% 6.24/1.68 % (365488)First to succeed.
% 6.24/1.68 % (365488)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-365481"
% 6.24/1.68 % (365513)------------------------------
% 6.24/1.68 % (365513)------------------------------
% 6.24/1.68 % (365519)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3476966863:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 6.24/1.68 % (365518)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1063524668:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 6.24/1.68 % (365487)Also succeeded, but the first one will report.
% 6.24/1.68 % (365488)Refutation found. Thanks to Tanya!
% 6.24/1.68 % SZS status Unsatisfiable for theBenchmark
% 6.24/1.68 % SZS output start Proof for theBenchmark
% See solution above
% 7.80/1.87 % (365488)------------------------------
% 7.80/1.87 % (365488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.80/1.87 % (365488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.80/1.87 % (365488)CaDiCaL version: 2.1.3
% 7.80/1.87 % (365488)Termination reason: Refutation
% 7.80/1.87 % (365488)Time elapsed: 0.701 s
% 7.80/1.87 % (365488)Peak memory usage: 130 MB
% 7.80/1.87 % (365488)Instructions burned: 1125 (million)
% 7.80/1.87 % (365488)------------------------------
% 7.80/1.87 % (365488)------------------------------
% 7.80/1.87 % (365481)Success in time 1.021 s
% 7.80/1.87 % Vampire exiting
%------------------------------------------------------------------------------