%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL073-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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 11:51:06 AM UTC 2026
% Result : Unsatisfiable 154.79s 41.93s
% Output : Refutation 288.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 13
% Syntax : Number of formulae : 171 ( 33 unt; 10 def)
% Number of atoms : 616 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 869 ( 424 ~; 435 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 12 ( 11 usr; 11 prp; 0-1 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 382 ( 0 sgn 382 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(implies(implies(X0,X1),implies(not(X2),not(X3))),X2),X4),implies(implies(X4,X0),implies(X3,X0)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_CAMeredith) ).
fof(f3,negated_conjecture,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_1) ).
fof(f4,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(implies(implies(X0,X1),implies(not(X2),not(X3))),X2),X4))
| is_a_theorem(implies(implies(X4,X0),implies(X3,X0))) ),
inference(resolution,[],[f1,f2]) ).
fof(f5,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),implies(X1,X3)),implies(X4,implies(X1,X3)))),
inference(resolution,[],[f4,f2]) ).
fof(f6,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(not(X1),X2)),X3),implies(X1,X3))),
inference(resolution,[],[f5,f4]) ).
fof(f8,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))),
inference(resolution,[],[f6,f4]) ).
fof(f10,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),not(X1)),implies(X2,not(X1)))),
inference(resolution,[],[f8,f4]) ).
fof(f11,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X0),X1))
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f8,f1]) ).
fof(f16,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X2)))),
inference(resolution,[],[f11,f8]) ).
fof(f18,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(X1,X1)),X2),implies(X3,X2))),
inference(resolution,[],[f16,f4]) ).
fof(f20,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,X2))) ),
inference(resolution,[],[f16,f1]) ).
fof(f22,definition,
( spl0_1
<=> ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f23,plain,
( ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X2)))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f22]) ).
fof(f25,definition,
( spl0_2
<=> ! [X0] : ~ is_a_theorem(X0) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f26,plain,
( ! [X0] : ~ is_a_theorem(X0)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f25]) ).
fof(f27,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f20,f25,f22]) ).
fof(f29,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),
inference(resolution,[],[f18,f4]) ).
fof(f34,plain,
( $false
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f29,f26]) ).
fof(f35,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f34]) ).
fof(f37,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(not(X0),not(X1)),X0),X2),implies(X1,X2))),
inference(resolution,[],[f29,f4]) ).
fof(f39,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f29,f1]) ).
fof(f41,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),not(implies(not(X1),not(X2)))),implies(X2,not(implies(not(X1),not(X2)))))),
inference(resolution,[],[f37,f4]) ).
fof(f42,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(implies(not(X2),not(X1)),X2)))),
inference(resolution,[],[f37,f11]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(not(X0),not(X1)),X0),X2))
| is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f37,f1]) ).
fof(f47,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(implies(not(X2),not(X1)),X2))) ),
inference(resolution,[],[f42,f1]) ).
fof(f49,definition,
( spl0_3
<=> ! [X2,X1] : is_a_theorem(implies(X1,implies(implies(not(X2),not(X1)),X2))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f50,plain,
( ! [X2,X1] : is_a_theorem(implies(X1,implies(implies(not(X2),not(X1)),X2)))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f51,plain,
( spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f47,f25,f49]) ).
fof(f54,plain,
( ! [X0,X1] :
( is_a_theorem(implies(implies(not(X1),not(X0)),X1))
| ~ is_a_theorem(X0) )
| ~ spl0_3 ),
inference(resolution,[],[f50,f1]) ).
fof(f58,plain,
( ! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,X1)) )
| ~ spl0_1 ),
inference(resolution,[],[f23,f1]) ).
fof(f60,definition,
( spl0_4
<=> ! [X1] : is_a_theorem(implies(X1,X1)) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f61,plain,
( ! [X1] : is_a_theorem(implies(X1,X1))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f60]) ).
fof(f62,plain,
( spl0_4
| spl0_2
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f58,f22,f25,f60]) ).
fof(f63,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(implies(implies(X0,X1),implies(not(X2),not(X3))),X2),X0),implies(X3,X0)))
| ~ spl0_4 ),
inference(resolution,[],[f61,f4]) ).
fof(f66,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),implies(X2,X1)))),
inference(resolution,[],[f39,f2]) ).
fof(f77,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0)))
| ~ spl0_4 ),
inference(resolution,[],[f39,f61]) ).
fof(f81,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f66,f1]) ).
fof(f86,plain,
( ! [X0,X1] :
( is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(X0) )
| ~ spl0_4 ),
inference(resolution,[],[f77,f1]) ).
fof(f90,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(not(X2),not(X3))))
| is_a_theorem(implies(implies(implies(X4,X2),X0),implies(X3,X0))) ),
inference(resolution,[],[f81,f4]) ).
fof(f133,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))),
inference(resolution,[],[f43,f29]) ).
fof(f185,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(X1,X2)),implies(X3,implies(X1,X2))))
| ~ spl0_4 ),
inference(resolution,[],[f63,f4]) ).
fof(f194,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X1,X2)))
| is_a_theorem(implies(X3,implies(X1,X2))) )
| ~ spl0_4 ),
inference(resolution,[],[f185,f1]) ).
fof(f213,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,not(not(X0))))),
inference(resolution,[],[f10,f43]) ).
fof(f222,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,not(X1))),implies(X3,implies(X2,not(X1))))),
inference(resolution,[],[f90,f29]) ).
fof(f223,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X3)),implies(implies(not(X3),not(not(X1))),implies(X2,X3)))),
inference(resolution,[],[f90,f41]) ).
fof(f262,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,not(X1))))
| is_a_theorem(implies(X3,implies(X2,not(X1)))) ),
inference(resolution,[],[f222,f1]) ).
fof(f308,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,not(not(implies(X2,X1))))))
| ~ spl0_4 ),
inference(resolution,[],[f213,f194]) ).
fof(f309,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(implies(X2,X3)),X2))),
inference(resolution,[],[f213,f90]) ).
fof(f347,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(not(implies(X2,X3)),X2)) ),
inference(resolution,[],[f309,f1]) ).
fof(f381,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(not(implies(X0,X1)),X0))
| ~ is_a_theorem(X2) )
| ~ spl0_3 ),
inference(resolution,[],[f347,f54]) ).
fof(f384,definition,
( spl0_7
<=> ! [X0,X1] : is_a_theorem(implies(not(implies(X0,X1)),X0)) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f385,plain,
( ! [X0,X1] : is_a_theorem(implies(not(implies(X0,X1)),X0))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f384]) ).
fof(f386,plain,
( spl0_2
| spl0_7
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f381,f49,f384,f25]) ).
fof(f528,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X2,X0),X3),implies(X1,X3)))
| ~ is_a_theorem(implies(not(X0),not(X1))) )
| ~ spl0_4 ),
inference(resolution,[],[f86,f90]) ).
fof(f761,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| is_a_theorem(implies(implies(not(X3),not(not(X1))),implies(X2,X3))) ),
inference(resolution,[],[f223,f1]) ).
fof(f762,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(not(implies(X0,X1)),not(not(X2))),implies(implies(X2,X1),implies(X0,X1)))),
inference(resolution,[],[f761,f2]) ).
fof(f806,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(not(X0),not(not(X0))),implies(X1,X0)))
| ~ spl0_4 ),
inference(resolution,[],[f761,f61]) ).
fof(f815,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(implies(X0,X1)),not(not(X2))))
| is_a_theorem(implies(implies(X2,X1),implies(X0,X1))) ),
inference(resolution,[],[f762,f1]) ).
fof(f818,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),not(not(X2))),implies(X2,not(not(X2)))))
| ~ spl0_4 ),
inference(resolution,[],[f806,f90]) ).
fof(f857,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(not(not(X0)),X1)))
| ~ spl0_7 ),
inference(resolution,[],[f815,f385]) ).
fof(f876,plain,
( ! [X0,X1] :
( is_a_theorem(implies(not(not(X0)),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_7 ),
inference(resolution,[],[f857,f1]) ).
fof(f880,plain,
( ! [X0,X1] :
( ~ is_a_theorem(not(not(X0)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1) )
| ~ spl0_7 ),
inference(resolution,[],[f876,f1]) ).
fof(f1200,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,not(not(implies(X2,X1))))) )
| ~ spl0_4 ),
inference(resolution,[],[f308,f1]) ).
fof(f1202,definition,
( spl0_9
<=> ! [X2,X1] : is_a_theorem(implies(X1,not(not(implies(X2,X1))))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f1203,plain,
( ! [X2,X1] : is_a_theorem(implies(X1,not(not(implies(X2,X1)))))
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1204,plain,
( spl0_9
| spl0_2
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f1200,f60,f25,f1202]) ).
fof(f1385,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,not(not(X1)))))
| ~ spl0_4 ),
inference(resolution,[],[f818,f43]) ).
fof(f1497,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(not(X1)),X2)))
| ~ spl0_4 ),
inference(resolution,[],[f1385,f90]) ).
fof(f1522,plain,
( ! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,not(not(X1)))) )
| ~ spl0_4 ),
inference(resolution,[],[f1385,f1]) ).
fof(f1524,definition,
( spl0_10
<=> ! [X1] : is_a_theorem(implies(X1,not(not(X1)))) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f1525,plain,
( ! [X1] : is_a_theorem(implies(X1,not(not(X1))))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f1524]) ).
fof(f1526,plain,
( spl0_10
| spl0_2
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f1522,f60,f25,f1524]) ).
fof(f1528,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,not(not(implies(X1,X1)))))
| ~ spl0_10 ),
inference(resolution,[],[f1525,f11]) ).
fof(f1569,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(not(not(implies(X0,X0))),X1),implies(X2,X1)))
| ~ spl0_10 ),
inference(resolution,[],[f1528,f4]) ).
fof(f1583,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,not(X1)),implies(X2,X1)),implies(X3,implies(X2,X1))))
| ~ spl0_4 ),
inference(resolution,[],[f1497,f90]) ).
fof(f1603,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(not(not(X1)),X2)) )
| ~ spl0_4 ),
inference(resolution,[],[f1497,f1]) ).
fof(f1670,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(not(not(X0)),not(not(implies(X1,implies(X2,X0))))))
| ~ spl0_4
| ~ spl0_9 ),
inference(resolution,[],[f1603,f1203]) ).
fof(f1693,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,not(X1)),implies(X2,X1)))
| is_a_theorem(implies(X3,implies(X2,X1))) )
| ~ spl0_4 ),
inference(resolution,[],[f1583,f1]) ).
fof(f1697,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(implies(X1,not(X2))),X2)))
| ~ spl0_4 ),
inference(resolution,[],[f1693,f133]) ).
fof(f1877,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(not(implies(X0,X0))),X1))
| is_a_theorem(implies(X2,X1)) )
| ~ spl0_10 ),
inference(resolution,[],[f1569,f1]) ).
fof(f1921,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,not(not(not(not(implies(X1,X1)))))))
| ~ spl0_10 ),
inference(resolution,[],[f1877,f1525]) ).
fof(f2052,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(not(implies(X1,not(X2))),X2)) )
| ~ spl0_4 ),
inference(resolution,[],[f1697,f1]) ).
fof(f2056,definition,
( spl0_13
<=> ! [X2,X1] : is_a_theorem(implies(not(implies(X1,not(X2))),X2)) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f2057,plain,
( ! [X2,X1] : is_a_theorem(implies(not(implies(X1,not(X2))),X2))
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f2056]) ).
fof(f2058,plain,
( spl0_13
| spl0_2
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f2052,f60,f25,f2056]) ).
fof(f2511,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(implies(X1,X2)),not(X2)))),
inference(resolution,[],[f262,f133]) ).
fof(f3056,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(not(implies(X1,X2)),not(X2))) ),
inference(resolution,[],[f2511,f1]) ).
fof(f3060,definition,
( spl0_31
<=> ! [X2,X1] : is_a_theorem(implies(not(implies(X1,X2)),not(X2))) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f3061,plain,
( ! [X2,X1] : is_a_theorem(implies(not(implies(X1,X2)),not(X2)))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f3060]) ).
fof(f3062,plain,
( spl0_31
| spl0_2 ),
inference(avatar_split_clause,[],[f3056,f25,f3060]) ).
fof(f3063,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,not(X0)),implies(X1,not(X0))))
| ~ spl0_31 ),
inference(resolution,[],[f3061,f815]) ).
fof(f3782,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(not(implies(not(X0),not(X1))),not(X2)))
| is_a_theorem(implies(implies(implies(X2,X0),X3),implies(X1,X3))) )
| ~ spl0_4 ),
inference(resolution,[],[f528,f4]) ).
fof(f5017,plain,
( ! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(not(not(not(not(implies(X1,X1)))))) )
| ~ spl0_10 ),
inference(resolution,[],[f1921,f1]) ).
fof(f5069,definition,
( spl0_40
<=> ! [X1] : is_a_theorem(not(not(not(not(implies(X1,X1)))))) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f5070,plain,
( ! [X1] : is_a_theorem(not(not(not(not(implies(X1,X1))))))
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f5069]) ).
fof(f5071,plain,
( spl0_40
| spl0_2
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f5017,f1524,f25,f5069]) ).
fof(f8255,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(not(not(implies(X0,X0))),X1))
| is_a_theorem(X1) )
| ~ spl0_7
| ~ spl0_40 ),
inference(resolution,[],[f880,f5070]) ).
fof(f12203,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2)))
| ~ spl0_4
| ~ spl0_13 ),
inference(resolution,[],[f3782,f2057]) ).
fof(f12278,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(not(X0),X2)) )
| ~ spl0_4
| ~ spl0_13 ),
inference(resolution,[],[f12203,f1]) ).
fof(f12433,plain,
( ! [X0,X1] : is_a_theorem(implies(not(X0),not(not(implies(X0,X1)))))
| ~ spl0_4
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f12278,f1525]) ).
fof(f12435,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(not(X0),not(not(implies(X1,implies(X0,X2))))))
| ~ spl0_4
| ~ spl0_9
| ~ spl0_13 ),
inference(resolution,[],[f12278,f1203]) ).
fof(f12446,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),X2),X1),implies(X0,X1)))
| ~ spl0_4
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f12433,f815]) ).
fof(f12496,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,X0)))
| ~ spl0_4
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f12446,f4]) ).
fof(f12651,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(implies(X2,X0)) )
| ~ spl0_4
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f12496,f1]) ).
fof(f12680,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(X2),not(X1)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_4
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f12651,f528]) ).
fof(f13019,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(X0,implies(X1,not(X2))))
| ~ is_a_theorem(implies(X2,not(X1))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f12680,f876]) ).
fof(f26099,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X2,X1),X3),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,not(not(X1)))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f13019,f90]) ).
fof(f26226,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,not(X1)))
| is_a_theorem(implies(X1,not(X0))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f13019,f8255]) ).
fof(f26825,plain,
( ! [X2,X3,X0,X1,X4] :
( is_a_theorem(implies(implies(implies(X2,X0),implies(X3,X1)),implies(X4,implies(X3,X1))))
| ~ is_a_theorem(implies(not(X0),not(not(X1)))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f26099,f90]) ).
fof(f31397,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X2,X0),implies(X3,X1)))
| ~ is_a_theorem(implies(not(X0),not(not(X1))))
| is_a_theorem(implies(X4,implies(X3,X1))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f26825,f1]) ).
fof(f31420,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X3,implies(implies(X0,X2),implies(X1,X2))))
| ~ is_a_theorem(implies(not(X0),not(not(implies(X1,X2))))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10
| ~ spl0_13 ),
inference(resolution,[],[f31397,f2]) ).
fof(f31788,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(X0),not(not(implies(X1,X2)))))
| is_a_theorem(implies(implies(X0,X2),implies(X1,X2))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f31420,f8255]) ).
fof(f31936,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(not(X0),implies(X1,X0)),implies(X2,implies(X1,X0))))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f31788,f1670]) ).
fof(f31941,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X2,implies(X0,X1))))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f31788,f12435]) ).
fof(f32051,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X2,implies(X0,X1))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f31941,f1]) ).
fof(f32071,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(implies(X1,X2),X1),X1)))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f32051,f12496]) ).
fof(f32126,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,implies(X1,X2)),implies(X1,X2))))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f32051,f31941]) ).
fof(f33059,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),X0))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f32071,f8255]) ).
fof(f33135,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(X0) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f33059,f1]) ).
fof(f33772,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f32126,f8255]) ).
fof(f33844,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f33772,f1]) ).
fof(f33915,plain,
( ! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X1))
| ~ is_a_theorem(X0) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f33844,f81]) ).
fof(f33916,plain,
( ! [X0] : is_a_theorem(implies(implies(X0,not(X0)),not(X0)))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f33844,f3063]) ).
fof(f33926,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(not(X0),implies(X1,X0)),implies(X1,X0)))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f33844,f31936]) ).
fof(f34122,plain,
( ! [X0] : is_a_theorem(implies(X0,not(implies(X0,not(X0)))))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f33916,f26226]) ).
fof(f34231,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(not(X2),not(X3))))
| is_a_theorem(implies(implies(X2,X0),implies(X3,X0))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f33915,f4]) ).
fof(f34757,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(implies(not(X0),not(X2))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f34231,f86]) ).
fof(f35367,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(X0),not(X1)))
| ~ is_a_theorem(implies(X0,X2))
| is_a_theorem(implies(X1,X2)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f34757,f1]) ).
fof(f35376,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(not(implies(X0,X2)),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f35367,f12433]) ).
fof(f35966,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),implies(X1,X0)))
| is_a_theorem(implies(X1,X0)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f33926,f1]) ).
fof(f36128,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,implies(X1,X2))))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_40 ),
inference(resolution,[],[f35966,f35376]) ).
fof(f38331,plain,
( ! [X0,X1] :
( is_a_theorem(implies(implies(not(X0),not(not(X0))),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f34122,f35367]) ).
fof(f41673,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,not(X0)),implies(X2,not(X0))))
| ~ is_a_theorem(implies(X0,implies(not(X1),not(X2)))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f38331,f34231]) ).
fof(f41717,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(not(X1),not(not(X2)))))
| is_a_theorem(implies(implies(X2,X1),implies(X0,X1))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f41673,f34231]) ).
fof(f41719,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X3,X2),X1),implies(X0,X1)))
| ~ is_a_theorem(implies(X0,implies(not(X1),not(not(X2))))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f41673,f90]) ).
fof(f43077,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X2,implies(X3,X3)),not(not(X0))),X1)))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f41717,f18]) ).
fof(f43711,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X2,implies(X3,X3)),not(not(X0))),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f43077,f1]) ).
fof(f44296,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,X2),implies(not(not(X0)),X2)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f43711,f4]) ).
fof(f44401,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(not(X1),implies(not(not(X0)),X2)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f44296,f12278]) ).
fof(f46888,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(not(X1),not(not(X1)))))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f41719,f33135]) ).
fof(f49591,plain,
( ! [X0,X1] :
( is_a_theorem(implies(not(X1),not(X0)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f44401,f46888]) ).
fof(f49611,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X0,X2)) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f49591,f35367]) ).
fof(f49901,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(X0,implies(implies(implies(implies(X1,X2),implies(not(X3),not(X4))),X3),X5)))
| is_a_theorem(implies(X0,implies(implies(X5,X1),implies(X4,X1)))) )
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f49611,f2]) ).
fof(f52648,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,implies(X1,X1)),X2),implies(implies(X2,X3),implies(X4,X3))))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f49901,f18]) ).
fof(f53321,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X2,implies(X3,X3)),X0),X1)))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f52648,f36128]) ).
fof(f80135,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f53321,f49901]) ).
fof(f80183,plain,
( $false
| ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(resolution,[],[f80135,f3]) ).
fof(f80338,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(avatar_contradiction_clause,[],[f80183]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f27]) ).
cnf(s3,plain,
~ spl0_2,
inference(sat_conversion,[],[f35]) ).
cnf(s4,plain,
( spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f51]) ).
cnf(s5,plain,
( ~ spl0_1
| spl0_2
| spl0_4 ),
inference(sat_conversion,[],[f62]) ).
cnf(s7,plain,
( spl0_2
| ~ spl0_3
| spl0_7 ),
inference(sat_conversion,[],[f386]) ).
cnf(s9,plain,
( spl0_2
| ~ spl0_4
| spl0_9 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s10,plain,
( spl0_2
| ~ spl0_4
| spl0_10 ),
inference(sat_conversion,[],[f1526]) ).
cnf(s13,plain,
( spl0_2
| ~ spl0_4
| spl0_13 ),
inference(sat_conversion,[],[f2058]) ).
cnf(s34,plain,
( spl0_2
| spl0_31 ),
inference(sat_conversion,[],[f3062]) ).
cnf(s43,plain,
( spl0_2
| ~ spl0_10
| spl0_40 ),
inference(sat_conversion,[],[f5071]) ).
cnf(s167,plain,
( ~ spl0_4
| ~ spl0_7
| ~ spl0_9
| ~ spl0_10
| ~ spl0_13
| ~ spl0_31
| ~ spl0_40 ),
inference(sat_conversion,[],[f80338]) ).
cnf(s178,plain,
spl0_31,
inference(rat,[],[s34,s3]) ).
cnf(s180,plain,
spl0_3,
inference(rat,[],[s4,s3]) ).
cnf(s183,plain,
spl0_7,
inference(rat,[],[s7,s3,s180]) ).
cnf(s184,plain,
spl0_1,
inference(rat,[],[s1,s3]) ).
cnf(s185,plain,
spl0_4,
inference(rat,[],[s5,s3,s184]) ).
cnf(s225,plain,
spl0_13,
inference(rat,[],[s13,s3,s185]) ).
cnf(s226,plain,
spl0_10,
inference(rat,[],[s10,s3,s185]) ).
cnf(s227,plain,
spl0_9,
inference(rat,[],[s9,s3,s185]) ).
cnf(s237,plain,
spl0_40,
inference(rat,[],[s43,s3,s226]) ).
cnf(s243,plain,
$false,
inference(rat,[],[s167,s237,s178,s225,s185,s183,s226,s227]) ).
fof(f80339,plain,
$false,
inference(avatar_sat_refutation,[],[s243]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL073-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.46 % Computer : n017.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Sun Sep 27 15:15:50 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.46 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.52 Running first-order theorem proving
% 0.24/0.52 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
% 17.92/3.88 % (2717077)Input is clausal, will run a generic CNF schedule.
% 17.92/3.88 % (2717082)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=4235070946:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.92/3.88 % (2717085)lrs+10_1_sil=8000:sp=occurrence:random_seed=1762958130:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.92/3.88 % (2717088)dis-21_1_sil=8000:lcm=predicate:random_seed=963326632: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)
% 17.92/3.88 % (2717084)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=9530466:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.92/3.88 % (2717087)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3317750092:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.92/3.88 % (2717086)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3838560148:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.92/3.88 % (2717083)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1547201021:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.92/3.88 % (2717086)Refutation not found, incomplete strategy
% 17.92/3.88 % (2717086)------------------------------
% 17.92/3.88 % (2717086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.88 % (2717086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.88 % (2717086)CaDiCaL version: 2.1.3
% 17.92/3.88 % (2717086)Termination reason: Refutation not found, incomplete strategy
% 17.92/3.88 % (2717086)Time elapsed: 0.001 s
% 17.92/3.88 % (2717086)Peak memory usage: 87 MB
% 17.92/3.88 % (2717088)Instruction limit reached!
% 17.92/3.88 % (2717088)------------------------------
% 17.92/3.88 % (2717088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.88 % (2717088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.88 % (2717088)CaDiCaL version: 2.1.3
% 17.92/3.88 % (2717088)Termination reason: Instruction limit
% 17.92/3.88 % (2717088)Termination phase: Saturation
% 17.92/3.88 % (2717088)Time elapsed: 0.101 s
% 17.92/3.88 % (2717088)Peak memory usage: 88 MB
% 17.92/3.88 % (2717088)Instructions burned: 117 (million)
% 17.92/3.88 % (2717085)Instruction limit reached!
% 17.92/3.88 % (2717085)------------------------------
% 17.92/3.88 % (2717085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.88 % (2717085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.88 % (2717085)CaDiCaL version: 2.1.3
% 17.92/3.88 % (2717085)Termination reason: Instruction limit
% 17.92/3.88 % (2717085)Termination phase: Saturation
% 17.92/3.88 % (2717085)Time elapsed: 0.105 s
% 17.92/3.88 % (2717085)Peak memory usage: 89 MB
% 17.92/3.88 % (2717085)Instructions burned: 107 (million)
% 17.92/3.88 % (2717087)Instruction limit reached!
% 17.92/3.88 % (2717087)------------------------------
% 17.92/3.88 % (2717087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.88 % (2717087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.88 % (2717087)CaDiCaL version: 2.1.3
% 17.92/3.88 % (2717087)Termination reason: Instruction limit
% 17.92/3.88 % (2717087)Termination phase: Saturation
% 17.92/3.88 % (2717087)Time elapsed: 0.186 s
% 17.92/3.88 % (2717087)Peak memory usage: 89 MB
% 17.92/3.88 % (2717087)Instructions burned: 180 (million)
% 17.92/3.88 % (2717096)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=1619924575:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 17.92/3.88 % (2717096)Refutation not found, incomplete strategy
% 17.92/3.88 % (2717096)------------------------------
% 17.92/3.88 % (2717096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.92/3.88 % (2717096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.92/3.88 % (2717096)CaDiCaL version: 2.1.3
% 17.92/3.88 % (2717096)Termination reason: Refutation not found, incomplete strategy
% 17.92/3.88 % (2717096)Time elapsed: 0.001 s
% 17.92/3.88 % (2717096)Peak memory usage: 87 MB
% 17.92/3.88 % (2717086)------------------------------
% 17.92/3.88 % (2717086)------------------------------
% 17.92/3.88 % (2717097)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3346002009: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)
% 30.98/6.06 % (2717098)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1310217412:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 30.98/6.06 % (2717098)Refutation not found, incomplete strategy
% 30.98/6.06 % (2717098)------------------------------
% 30.98/6.06 % (2717098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.98/6.06 % (2717098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.98/6.06 % (2717098)CaDiCaL version: 2.1.3
% 30.98/6.06 % (2717098)Termination reason: Refutation not found, incomplete strategy
% 30.98/6.06 % (2717098)Time elapsed: 0.001 s
% 30.98/6.06 % (2717098)Peak memory usage: 87 MB
% 30.98/6.06 % (2717097)Instruction limit reached!
% 30.98/6.06 % (2717097)------------------------------
% 30.98/6.06 % (2717097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.98/6.06 % (2717097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.98/6.06 % (2717097)CaDiCaL version: 2.1.3
% 30.98/6.06 % (2717097)Termination reason: Instruction limit
% 30.98/6.06 % (2717097)Termination phase: Saturation
% 30.98/6.06 % (2717097)Time elapsed: 0.166 s
% 30.98/6.06 % (2717097)Peak memory usage: 90 MB
% 30.98/6.06 % (2717097)Instructions burned: 189 (million)
% 30.98/6.06 % (2717101)lrs+10_64_to=lpo:sil=8000:random_seed=3072256365:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 30.98/6.06 % (2717101)Instruction limit reached!
% 30.98/6.06 % (2717101)------------------------------
% 30.98/6.06 % (2717101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.98/6.06 % (2717101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.98/6.06 % (2717101)CaDiCaL version: 2.1.3
% 30.98/6.06 % (2717101)Termination reason: Instruction limit
% 30.98/6.06 % (2717101)Termination phase: Saturation
% 30.98/6.06 % (2717101)Time elapsed: 0.067 s
% 30.98/6.06 % (2717101)Peak memory usage: 89 MB
% 30.98/6.06 % (2717101)Instructions burned: 127 (million)
% 30.98/6.06 % (2717096)------------------------------
% 30.98/6.06 % (2717096)------------------------------
% 30.98/6.06 % (2717103)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3873155834:avsq=on:i=194:fgj=on:bd=preordered_2991 on theBenchmark for (2991ds/194Mi)
% 30.98/6.06 % (2717098)------------------------------
% 30.98/6.06 % (2717098)------------------------------
% 30.98/6.06 % (2717105)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2722972224:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 30.98/6.06 % (2717105)Instruction limit reached!
% 30.98/6.06 % (2717105)------------------------------
% 30.98/6.06 % (2717105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.98/6.06 % (2717105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.98/6.06 % (2717105)CaDiCaL version: 2.1.3
% 30.98/6.06 % (2717105)Termination reason: Instruction limit
% 30.98/6.06 % (2717105)Termination phase: Saturation
% 30.98/6.06 % (2717105)Time elapsed: 0.086 s
% 30.98/6.06 % (2717105)Peak memory usage: 91 MB
% 30.98/6.06 % (2717105)Instructions burned: 158 (million)
% 30.98/6.06 % (2717106)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1591225146:i=3394:sd=4:ss=included:sgt=64_2989 on theBenchmark for (2989ds/3394Mi)
% 30.98/6.06 % (2717103)Instruction limit reached!
% 30.98/6.06 % (2717103)------------------------------
% 30.98/6.06 % (2717103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.98/6.06 % (2717103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.98/6.06 % (2717103)CaDiCaL version: 2.1.3
% 30.98/6.06 % (2717103)Termination reason: Instruction limit
% 30.98/6.06 % (2717103)Termination phase: Saturation
% 30.98/6.06 % (2717103)Time elapsed: 0.203 s
% 30.98/6.06 % (2717103)Peak memory usage: 90 MB
% 30.98/6.06 % (2717103)Instructions burned: 194 (million)
% 30.98/6.06 % (2717108)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=1779820493:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2988 on theBenchmark for (2988ds/106Mi)
% 30.98/6.06 % (2717108)Instruction limit reached!
% 30.98/6.06 % (2717108)------------------------------
% 30.98/6.06 % (2717108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.98/6.06 % (2717108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.25/8.61 % (2717108)CaDiCaL version: 2.1.3
% 52.25/8.61 % (2717108)Termination reason: Instruction limit
% 52.25/8.61 % (2717108)Termination phase: Saturation
% 52.25/8.61 % (2717108)Time elapsed: 0.092 s
% 52.25/8.61 % (2717108)Peak memory usage: 88 MB
% 52.25/8.61 % (2717108)Instructions burned: 106 (million)
% 52.25/8.61 % (2717110)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2005482393:i=107_2986 on theBenchmark for (2986ds/107Mi)
% 52.25/8.61 % (2717110)Refutation not found, incomplete strategy
% 52.25/8.61 % (2717110)------------------------------
% 52.25/8.61 % (2717110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.25/8.61 % (2717110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.25/8.61 % (2717110)CaDiCaL version: 2.1.3
% 52.25/8.61 % (2717110)Termination reason: Refutation not found, incomplete strategy
% 52.25/8.61 % (2717110)Time elapsed: 0.001 s
% 52.25/8.61 % (2717110)Peak memory usage: 87 MB
% 52.25/8.61 % (2717112)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1785743227:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2986 on theBenchmark for (2986ds/242Mi)
% 52.25/8.62 % (2717110)------------------------------
% 52.25/8.62 % (2717110)------------------------------
% 52.25/8.62 % (2717115)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1129435601:cond=fast:i=5208:av=off_2984 on theBenchmark for (2984ds/5208Mi)
% 52.25/8.62 % (2717112)Instruction limit reached!
% 52.25/8.62 % (2717112)------------------------------
% 52.25/8.62 % (2717112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.25/8.62 % (2717112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.25/8.62 % (2717112)CaDiCaL version: 2.1.3
% 52.25/8.62 % (2717112)Termination reason: Instruction limit
% 52.25/8.62 % (2717112)Termination phase: Saturation
% 52.25/8.62 % (2717112)Time elapsed: 0.226 s
% 52.25/8.62 % (2717112)Peak memory usage: 89 MB
% 52.25/8.62 % (2717112)Instructions burned: 243 (million)
% 52.25/8.62 % (2717117)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2073588213:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 52.25/8.62 % (2717117)Instruction limit reached!
% 52.25/8.62 % (2717117)------------------------------
% 52.25/8.62 % (2717117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.25/8.62 % (2717117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.25/8.62 % (2717117)CaDiCaL version: 2.1.3
% 52.25/8.62 % (2717117)Termination reason: Instruction limit
% 52.25/8.62 % (2717117)Termination phase: Saturation
% 52.25/8.62 % (2717117)Time elapsed: 0.075 s
% 52.25/8.62 % (2717117)Peak memory usage: 89 MB
% 52.25/8.62 % (2717117)Instructions burned: 135 (million)
% 52.25/8.62 % (2717119)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3393826622:i=499:bd=all_2981 on theBenchmark for (2981ds/499Mi)
% 52.25/8.62 % (2717121)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1538206073:i=191:fgj=on:bd=all_2979 on theBenchmark for (2979ds/191Mi)
% 52.25/8.62 % (2717121)Instruction limit reached!
% 52.25/8.62 % (2717121)------------------------------
% 52.25/8.62 % (2717121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.25/8.62 % (2717121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.25/8.62 % (2717121)CaDiCaL version: 2.1.3
% 52.25/8.62 % (2717121)Termination reason: Instruction limit
% 52.25/8.62 % (2717121)Termination phase: Saturation
% 52.25/8.62 % (2717121)Time elapsed: 0.103 s
% 52.25/8.62 % (2717121)Peak memory usage: 91 MB
% 52.25/8.62 % (2717121)Instructions burned: 192 (million)
% 52.25/8.62 % (2717119)Instruction limit reached!
% 52.25/8.62 % (2717119)------------------------------
% 52.25/8.62 % (2717119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.25/8.62 % (2717119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.25/8.62 % (2717119)CaDiCaL version: 2.1.3
% 52.25/8.62 % (2717119)Termination reason: Instruction limit
% 52.25/8.62 % (2717119)Termination phase: Saturation
% 52.25/8.62 % (2717119)Time elapsed: 0.453 s
% 52.25/8.62 % (2717119)Peak memory usage: 91 MB
% 52.25/8.62 % (2717119)Instructions burned: 499 (million)
% 52.25/8.62 % (2717124)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2658798014:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 83.07/13.03 % (2717124)Instruction limit reached!
% 83.07/13.03 % (2717124)------------------------------
% 83.07/13.03 % (2717124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.07/13.03 % (2717124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.07/13.03 % (2717124)CaDiCaL version: 2.1.3
% 83.07/13.03 % (2717124)Termination reason: Instruction limit
% 83.07/13.03 % (2717124)Termination phase: Saturation
% 83.07/13.03 % (2717124)Time elapsed: 0.140 s
% 83.07/13.03 % (2717124)Peak memory usage: 91 MB
% 83.07/13.03 % (2717124)Instructions burned: 265 (million)
% 83.07/13.03 % (2717125)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1442029703:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 83.07/13.03 % (2717127)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=4249807321:i=3256:kws=precedence:bd=preordered:av=off_2972 on theBenchmark for (2972ds/3256Mi)
% 83.07/13.03 % (2717125)Instruction limit reached!
% 83.07/13.03 % (2717125)------------------------------
% 83.07/13.03 % (2717125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.07/13.03 % (2717125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.07/13.03 % (2717125)CaDiCaL version: 2.1.3
% 83.07/13.03 % (2717125)Termination reason: Instruction limit
% 83.07/13.03 % (2717125)Termination phase: Saturation
% 83.07/13.03 % (2717125)Time elapsed: 0.165 s
% 83.07/13.03 % (2717125)Peak memory usage: 89 MB
% 83.07/13.03 % (2717125)Instructions burned: 158 (million)
% 83.07/13.03 % (2717130)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3125141354:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 83.07/13.03 % (2717130)Instruction limit reached!
% 83.07/13.03 % (2717130)------------------------------
% 83.07/13.03 % (2717130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.07/13.03 % (2717130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.07/13.03 % (2717130)CaDiCaL version: 2.1.3
% 83.07/13.03 % (2717130)Termination reason: Instruction limit
% 83.07/13.03 % (2717130)Termination phase: Saturation
% 83.07/13.03 % (2717130)Time elapsed: 0.514 s
% 83.07/13.03 % (2717130)Peak memory usage: 92 MB
% 83.07/13.03 % (2717130)Instructions burned: 537 (million)
% 83.07/13.03 % (2717132)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3812438569:i=180:bd=preordered:av=off_2961 on theBenchmark for (2961ds/180Mi)
% 83.07/13.03 % (2717132)Instruction limit reached!
% 83.07/13.03 % (2717132)------------------------------
% 83.07/13.03 % (2717132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.07/13.03 % (2717132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.07/13.03 % (2717132)CaDiCaL version: 2.1.3
% 83.07/13.03 % (2717132)Termination reason: Instruction limit
% 83.07/13.03 % (2717132)Termination phase: Saturation
% 83.07/13.03 % (2717132)Time elapsed: 0.163 s
% 83.07/13.03 % (2717132)Peak memory usage: 88 MB
% 83.07/13.03 % (2717132)Instructions burned: 180 (million)
% 83.07/13.03 % (2717134)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=2169182554:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2956 on theBenchmark for (2956ds/10307Mi)
% 83.07/13.03 % (2717127)Instruction limit reached!
% 83.07/13.03 % (2717127)------------------------------
% 83.07/13.03 % (2717127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.07/13.03 % (2717127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.07/13.03 % (2717127)CaDiCaL version: 2.1.3
% 83.07/13.03 % (2717127)Termination reason: Instruction limit
% 83.07/13.03 % (2717127)Termination phase: Saturation
% 83.07/13.03 % (2717127)Time elapsed: 1.649 s
% 83.07/13.03 % (2717127)Peak memory usage: 154 MB
% 83.07/13.03 % (2717127)Instructions burned: 3257 (million)
% 83.07/13.03 % (2717106)Instruction limit reached!
% 83.07/13.03 % (2717106)------------------------------
% 83.07/13.03 % (2717106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 83.07/13.03 % (2717106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 83.07/13.03 % (2717106)CaDiCaL version: 2.1.3
% 83.07/13.03 % (2717106)Termination reason: Instruction limit
% 83.07/13.03 % (2717106)Termination phase: Saturation
% 83.07/13.03 % (2717106)Time elapsed: 3.469 s
% 83.07/13.03 % (2717106)Peak memory usage: 151 MB
% 114.94/17.47 % (2717106)Instructions burned: 3394 (million)
% 114.94/17.47 % (2717136)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=2794306633:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 114.94/17.47 % (2717137)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=172516486:s2pl=no:i=8478:s2at=4:nm=6_2951 on theBenchmark for (2951ds/8478Mi)
% 114.94/17.47 % (2717136)Instruction limit reached!
% 114.94/17.47 % (2717136)------------------------------
% 114.94/17.47 % (2717136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.47 % (2717136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.47 % (2717136)CaDiCaL version: 2.1.3
% 114.94/17.47 % (2717136)Termination reason: Instruction limit
% 114.94/17.47 % (2717136)Termination phase: Saturation
% 114.94/17.47 % (2717136)Time elapsed: 0.222 s
% 114.94/17.47 % (2717136)Peak memory usage: 93 MB
% 114.94/17.47 % (2717136)Instructions burned: 412 (million)
% 114.94/17.47 % (2717140)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=1470157306:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2948 on theBenchmark for (2948ds/303Mi)
% 114.94/17.47 % (2717140)Instruction limit reached!
% 114.94/17.47 % (2717140)------------------------------
% 114.94/17.47 % (2717140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.47 % (2717140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.47 % (2717140)CaDiCaL version: 2.1.3
% 114.94/17.47 % (2717140)Termination reason: Instruction limit
% 114.94/17.47 % (2717140)Termination phase: Saturation
% 114.94/17.47 % (2717140)Time elapsed: 0.135 s
% 114.94/17.47 % (2717140)Peak memory usage: 90 MB
% 114.94/17.47 % (2717140)Instructions burned: 303 (million)
% 114.94/17.47 % (2717142)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2747441102:st=4:i=720:sd=3:fsr=off:ss=axioms_2945 on theBenchmark for (2945ds/720Mi)
% 114.94/17.47 % (2717142)Instruction limit reached!
% 114.94/17.47 % (2717142)------------------------------
% 114.94/17.47 % (2717142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.47 % (2717142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.47 % (2717142)CaDiCaL version: 2.1.3
% 114.94/17.47 % (2717142)Termination reason: Instruction limit
% 114.94/17.47 % (2717142)Termination phase: Saturation
% 114.94/17.47 % (2717142)Time elapsed: 0.615 s
% 114.94/17.47 % (2717142)Peak memory usage: 102 MB
% 114.94/17.47 % (2717142)Instructions burned: 721 (million)
% 114.94/17.47 % (2717144)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2145500983:i=598:bs=on:bd=preordered:av=off:ss=axioms_2936 on theBenchmark for (2936ds/598Mi)
% 114.94/17.47 % (2717144)Refutation not found, incomplete strategy
% 114.94/17.47 % (2717144)------------------------------
% 114.94/17.47 % (2717144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.47 % (2717144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.47 % (2717144)CaDiCaL version: 2.1.3
% 114.94/17.47 % (2717144)Termination reason: Refutation not found, incomplete strategy
% 114.94/17.47 % (2717144)Time elapsed: 0.002 s
% 114.94/17.47 % (2717144)Peak memory usage: 87 MB
% 114.94/17.47 % (2717144)Instructions burned: 1 (million)
% 114.94/17.47 % (2717115)Instruction limit reached!
% 114.94/17.47 % (2717115)------------------------------
% 114.94/17.47 % (2717115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.94/17.47 % (2717115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.94/17.47 % (2717115)CaDiCaL version: 2.1.3
% 114.94/17.47 % (2717115)Termination reason: Instruction limit
% 114.94/17.47 % (2717115)Termination phase: Saturation
% 114.94/17.47 % (2717115)Time elapsed: 5.186 s
% 114.94/17.47 % (2717115)Peak memory usage: 161 MB
% 114.94/17.47 % (2717115)Instructions burned: 5209 (million)
% 114.94/17.47 % (2717144)------------------------------
% 114.94/17.47 % (2717144)------------------------------
% 114.94/17.47 % (2717146)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1820508133:i=2989:sd=3:ss=axioms:sgt=60_2929 on theBenchmark for (2929ds/2989Mi)
% 114.94/17.47 % (2717147)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=3068557011:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2929 on theBenchmark for (2929ds/1997Mi)
% 163.00/24.17 % (2717147)Instruction limit reached!
% 163.00/24.17 % (2717147)------------------------------
% 163.00/24.17 % (2717147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.00/24.17 % (2717147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.00/24.17 % (2717147)CaDiCaL version: 2.1.3
% 163.00/24.17 % (2717147)Termination reason: Instruction limit
% 163.00/24.17 % (2717147)Termination phase: Saturation
% 163.00/24.17 % (2717147)Time elapsed: 2.141 s
% 163.00/24.17 % (2717147)Peak memory usage: 138 MB
% 163.00/24.17 % (2717147)Instructions burned: 1997 (million)
% 163.00/24.17 % (2717150)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=1424188336:i=2088:bd=preordered:av=off_2904 on theBenchmark for (2904ds/2088Mi)
% 163.00/24.17 % (2717146)Instruction limit reached!
% 163.00/24.17 % (2717146)------------------------------
% 163.00/24.17 % (2717146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.00/24.17 % (2717146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.00/24.17 % (2717146)CaDiCaL version: 2.1.3
% 163.00/24.17 % (2717146)Termination reason: Instruction limit
% 163.00/24.17 % (2717146)Termination phase: Saturation
% 163.00/24.17 % (2717146)Time elapsed: 3.028 s
% 163.00/24.17 % (2717146)Peak memory usage: 147 MB
% 163.00/24.17 % (2717146)Instructions burned: 2990 (million)
% 163.00/24.17 % (2717152)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1297256461:i=1098:nicw=on_2896 on theBenchmark for (2896ds/1098Mi)
% 163.00/24.17 % (2717134)Instruction limit reached!
% 163.00/24.17 % (2717134)------------------------------
% 163.00/24.17 % (2717134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.00/24.17 % (2717134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.00/24.17 % (2717134)CaDiCaL version: 2.1.3
% 163.00/24.17 % (2717134)Termination reason: Instruction limit
% 163.00/24.17 % (2717134)Termination phase: Saturation
% 163.00/24.17 % (2717134)Time elapsed: 6.295 s
% 163.00/24.17 % (2717134)Peak memory usage: 194 MB
% 163.00/24.17 % (2717134)Instructions burned: 10309 (million)
% 163.00/24.17 % (2717154)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2599604636:i=433:bd=preordered_2890 on theBenchmark for (2890ds/433Mi)
% 163.00/24.17 % (2717154)Instruction limit reached!
% 163.00/24.17 % (2717154)------------------------------
% 163.00/24.17 % (2717154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.00/24.17 % (2717154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.00/24.17 % (2717154)CaDiCaL version: 2.1.3
% 163.00/24.17 % (2717154)Termination reason: Instruction limit
% 163.00/24.17 % (2717154)Termination phase: Saturation
% 163.00/24.17 % (2717154)Time elapsed: 0.220 s
% 163.00/24.17 % (2717154)Peak memory usage: 92 MB
% 163.00/24.17 % (2717154)Instructions burned: 433 (million)
% 163.00/24.17 % (2717156)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1294544989:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2886 on theBenchmark for (2886ds/2942Mi)
% 163.00/24.17 % (2717152)Instruction limit reached!
% 163.00/24.17 % (2717152)------------------------------
% 163.00/24.17 % (2717152)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.00/24.17 % (2717152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.00/24.17 % (2717152)CaDiCaL version: 2.1.3
% 163.00/24.17 % (2717152)Termination reason: Instruction limit
% 163.00/24.17 % (2717152)Termination phase: Saturation
% 163.00/24.17 % (2717152)Time elapsed: 0.982 s
% 163.00/24.17 % (2717152)Peak memory usage: 96 MB
% 163.00/24.17 % (2717152)Instructions burned: 1098 (million)
% 163.00/24.17 % (2717150)Instruction limit reached!
% 163.00/24.17 % (2717150)------------------------------
% 163.00/24.17 % (2717150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.00/24.17 % (2717150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.00/24.17 % (2717150)CaDiCaL version: 2.1.3
% 163.00/24.17 % (2717150)Termination reason: Instruction limit
% 163.00/24.17 % (2717150)Termination phase: Saturation
% 163.00/24.17 % (2717150)Time elapsed: 1.982 s
% 163.00/24.17 % (2717150)Peak memory usage: 131 MB
% 163.00/24.17 % (2717150)Instructions burned: 2088 (million)
% 177.50/26.22 % (2717158)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=702674942:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2883 on theBenchmark for (2883ds/6922Mi)
% 177.50/26.22 % (2717159)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=2688587830:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2882 on theBenchmark for (2882ds/596Mi)
% 177.50/26.22 % (2717159)Instruction limit reached!
% 177.50/26.22 % (2717159)------------------------------
% 177.50/26.22 % (2717159)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 177.50/26.22 % (2717159)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.50/26.22 % (2717159)CaDiCaL version: 2.1.3
% 177.50/26.22 % (2717159)Termination reason: Instruction limit
% 177.50/26.22 % (2717159)Termination phase: Saturation
% 177.50/26.22 % (2717159)Time elapsed: 0.481 s
% 177.50/26.22 % (2717159)Peak memory usage: 93 MB
% 177.50/26.22 % (2717159)Instructions burned: 596 (million)
% 177.50/26.22 % (2717162)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=1262957645:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2874 on theBenchmark for (2874ds/4123Mi)
% 177.50/26.22 % (2717137)Instruction limit reached!
% 177.50/26.22 % (2717137)------------------------------
% 177.50/26.22 % (2717137)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 177.50/26.22 % (2717137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.50/26.22 % (2717137)CaDiCaL version: 2.1.3
% 177.50/26.22 % (2717137)Termination reason: Instruction limit
% 177.50/26.22 % (2717137)Termination phase: Saturation
% 177.50/26.22 % (2717137)Time elapsed: 7.936 s
% 177.50/26.22 % (2717137)Peak memory usage: 194 MB
% 177.50/26.22 % (2717137)Instructions burned: 8478 (million)
% 177.50/26.22 % (2717156)Instruction limit reached!
% 177.50/26.22 % (2717156)------------------------------
% 177.50/26.22 % (2717156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 177.50/26.22 % (2717156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.50/26.22 % (2717156)CaDiCaL version: 2.1.3
% 177.50/26.22 % (2717156)Termination reason: Instruction limit
% 177.50/26.22 % (2717156)Termination phase: Saturation
% 177.50/26.22 % (2717156)Time elapsed: 1.699 s
% 177.50/26.22 % (2717156)Peak memory usage: 140 MB
% 177.50/26.22 % (2717156)Instructions burned: 2942 (million)
% 177.50/26.22 % (2717164)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3237328933:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2869 on theBenchmark for (2869ds/16411Mi)
% 177.50/26.22 % (2717165)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1089752812:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2867 on theBenchmark for (2867ds/1670Mi)
% 177.50/26.22 % (2717165)Instruction limit reached!
% 177.50/26.22 % (2717165)------------------------------
% 177.50/26.22 % (2717165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 177.50/26.22 % (2717165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.50/26.22 % (2717165)CaDiCaL version: 2.1.3
% 177.50/26.22 % (2717165)Termination reason: Instruction limit
% 177.50/26.22 % (2717165)Termination phase: Saturation
% 177.50/26.22 % (2717165)Time elapsed: 1.025 s
% 177.50/26.22 % (2717165)Peak memory usage: 135 MB
% 177.50/26.22 % (2717165)Instructions burned: 1671 (million)
% 177.50/26.22 % (2717185)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=3271845068:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2854 on theBenchmark for (2854ds/1722Mi)
% 177.50/26.22 % (2717185)Instruction limit reached!
% 177.50/26.22 % (2717185)------------------------------
% 177.50/26.22 % (2717185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 177.50/26.22 % (2717185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 177.50/26.22 % (2717185)CaDiCaL version: 2.1.3
% 177.50/26.22 % (2717185)Termination reason: Instruction limit
% 177.50/26.22 % (2717185)Termination phase: Saturation
% 177.50/26.22 % (2717185)Time elapsed: 1.117 s
% 177.50/26.22 % (2717185)Peak memory usage: 135 MB
% 177.50/26.22 % (2717185)Instructions burned: 1723 (million)
% 177.50/26.22 % (2717187)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=612045665:cts=off:cond=on:i=9530:bs=on:fsd=on_2840 on theBenchmark for (2840ds/9530Mi)
% 192.95/28.47 % (2717162)Instruction limit reached!
% 192.95/28.47 % (2717162)------------------------------
% 192.95/28.47 % (2717162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.95/28.47 % (2717162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.95/28.47 % (2717162)CaDiCaL version: 2.1.3
% 192.95/28.47 % (2717162)Termination reason: Instruction limit
% 192.95/28.47 % (2717162)Termination phase: Saturation
% 192.95/28.47 % (2717162)Time elapsed: 3.900 s
% 192.95/28.47 % (2717162)Peak memory usage: 157 MB
% 192.95/28.47 % (2717162)Instructions burned: 4123 (million)
% 192.95/28.47 % (2717189)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=776646881:st=2:i=4495:sd=10:ss=included_2832 on theBenchmark for (2832ds/4495Mi)
% 192.95/28.47 % (2717158)Instruction limit reached!
% 192.95/28.47 % (2717158)------------------------------
% 192.95/28.47 % (2717158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.95/28.47 % (2717158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.95/28.47 % (2717158)CaDiCaL version: 2.1.3
% 192.95/28.47 % (2717158)Termination reason: Instruction limit
% 192.95/28.47 % (2717158)Termination phase: Saturation
% 192.95/28.47 % (2717158)Time elapsed: 6.520 s
% 192.95/28.47 % (2717158)Peak memory usage: 181 MB
% 192.95/28.47 % (2717158)Instructions burned: 6922 (million)
% 192.95/28.47 % (2717191)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=2891913892:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2815 on theBenchmark for (2815ds/4920Mi)
% 192.95/28.47 % (2717189)Instruction limit reached!
% 192.95/28.47 % (2717189)------------------------------
% 192.95/28.47 % (2717189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.95/28.47 % (2717189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.95/28.47 % (2717189)CaDiCaL version: 2.1.3
% 192.95/28.47 % (2717189)Termination reason: Instruction limit
% 192.95/28.47 % (2717189)Termination phase: Saturation
% 192.95/28.47 % (2717189)Time elapsed: 4.500 s
% 192.95/28.47 % (2717189)Peak memory usage: 161 MB
% 192.95/28.47 % (2717189)Instructions burned: 4496 (million)
% 192.95/28.47 % (2717195)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=3015121973:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2784 on theBenchmark for (2784ds/2083Mi)
% 192.95/28.47 % (2717187)Instruction limit reached!
% 192.95/28.47 % (2717187)------------------------------
% 192.95/28.47 % (2717187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.95/28.47 % (2717187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.95/28.47 % (2717187)CaDiCaL version: 2.1.3
% 192.95/28.47 % (2717187)Termination reason: Instruction limit
% 192.95/28.47 % (2717187)Termination phase: Saturation
% 192.95/28.47 % (2717187)Time elapsed: 5.554 s
% 192.95/28.47 % (2717187)Peak memory usage: 195 MB
% 192.95/28.47 % (2717187)Instructions burned: 9532 (million)
% 192.95/28.47 % (2717200)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=4206633891:i=4629:av=off:gsp=on_2782 on theBenchmark for (2782ds/4629Mi)
% 192.95/28.47 % (2717200)Refutation not found, incomplete strategy
% 192.95/28.47 % (2717200)------------------------------
% 192.95/28.47 % (2717200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.95/28.47 % (2717200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.95/28.47 % (2717200)CaDiCaL version: 2.1.3
% 192.95/28.47 % (2717200)Termination reason: Refutation not found, incomplete strategy
% 192.95/28.47 % (2717200)Time elapsed: 0.339 s
% 192.95/28.47 % (2717200)Peak memory usage: 127 MB
% 192.95/28.47 % (2717200)Instructions burned: 856 (million)
% 192.95/28.47 % (2717200)------------------------------
% 192.95/28.47 % (2717200)------------------------------
% 192.95/28.47 % (2717355)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2006223035:i=1258:av=off_2776 on theBenchmark for (2776ds/1258Mi)
% 192.95/28.47 % (2717355)Instruction limit reached!
% 192.95/28.47 % (2717355)------------------------------
% 192.95/28.47 % (2717355)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 216.92/31.84 % (2717355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.92/31.84 % (2717355)CaDiCaL version: 2.1.3
% 216.92/31.84 % (2717355)Termination reason: Instruction limit
% 216.92/31.84 % (2717355)Termination phase: Saturation
% 216.92/31.84 % (2717355)Time elapsed: 0.395 s
% 216.92/31.84 % (2717355)Peak memory usage: 123 MB
% 216.92/31.84 % (2717355)Instructions burned: 1258 (million)
% 216.92/31.84 % (2717191)Instruction limit reached!
% 216.92/31.84 % (2717191)------------------------------
% 216.92/31.84 % (2717191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 216.92/31.84 % (2717191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.92/31.84 % (2717191)CaDiCaL version: 2.1.3
% 216.92/31.84 % (2717191)Termination reason: Instruction limit
% 216.92/31.84 % (2717191)Termination phase: Saturation
% 216.92/31.84 % (2717191)Time elapsed: 4.165 s
% 216.92/31.84 % (2717191)Peak memory usage: 160 MB
% 216.92/31.84 % (2717191)Instructions burned: 4922 (million)
% 216.92/31.84 % (2717357)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1852748272:i=7343:av=off:ss=included_2770 on theBenchmark for (2770ds/7343Mi)
% 216.92/31.84 % (2717195)Instruction limit reached!
% 216.92/31.84 % (2717195)------------------------------
% 216.92/31.84 % (2717195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 216.92/31.84 % (2717195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.92/31.84 % (2717195)CaDiCaL version: 2.1.3
% 216.92/31.84 % (2717195)Termination reason: Instruction limit
% 216.92/31.84 % (2717195)Termination phase: Saturation
% 216.92/31.84 % (2717195)Time elapsed: 1.309 s
% 216.92/31.84 % (2717195)Peak memory usage: 136 MB
% 216.92/31.84 % (2717195)Instructions burned: 2084 (million)
% 216.92/31.84 % (2717358)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=1643332398:i=1325:sd=2:ss=axioms:sgt=16_2770 on theBenchmark for (2770ds/1325Mi)
% 216.92/31.84 % (2717358)Refutation not found, incomplete strategy
% 216.92/31.84 % (2717358)------------------------------
% 216.92/31.84 % (2717358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 216.92/31.84 % (2717358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.92/31.84 % (2717358)CaDiCaL version: 2.1.3
% 216.92/31.84 % (2717358)Termination reason: Refutation not found, incomplete strategy
% 216.92/31.84 % (2717358)Time elapsed: 0.001 s
% 216.92/31.84 % (2717358)Peak memory usage: 87 MB
% 216.92/31.84 % (2717360)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=2870738610:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2769 on theBenchmark for (2769ds/2646Mi)
% 216.92/31.84 % (2717358)------------------------------
% 216.92/31.84 % (2717358)------------------------------
% 216.92/31.84 % (2717363)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=1329241170:i=1489:sd=2:ep=R:ss=axioms_2766 on theBenchmark for (2766ds/1489Mi)
% 216.92/31.84 % (2717363)Refutation not found, incomplete strategy
% 216.92/31.84 % (2717363)------------------------------
% 216.92/31.84 % (2717363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 216.92/31.84 % (2717363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.92/31.84 % (2717363)CaDiCaL version: 2.1.3
% 216.92/31.84 % (2717363)Termination reason: Refutation not found, incomplete strategy
% 216.92/31.84 % (2717363)Time elapsed: 0.564 s
% 216.92/31.84 % (2717363)Peak memory usage: 127 MB
% 216.92/31.84 % (2717363)Instructions burned: 851 (million)
% 216.92/31.84 % (2717363)------------------------------
% 216.92/31.84 % (2717363)------------------------------
% 216.92/31.84 % (2717365)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=4052020232:i=1503_2756 on theBenchmark for (2756ds/1503Mi)
% 216.92/31.84 % (2717360)Instruction limit reached!
% 216.92/31.84 % (2717360)------------------------------
% 216.92/31.84 % (2717360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 216.92/31.84 % (2717360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 216.92/31.84 % (2717360)CaDiCaL version: 2.1.3
% 216.92/31.84 % (2717360)Termination reason: Instruction limit
% 216.92/31.84 % (2717360)Termination phase: Saturation
% 216.92/31.84 % (2717360)Time elapsed: 1.554 s
% 216.92/31.84 % (2717360)Peak memory usage: 143 MB
% 216.92/31.84 % (2717360)Instructions burned: 2647 (million)
% 216.92/31.84 % (2717367)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=1513868831:i=13942:kws=frequency_2752 on theBenchmark for (2752ds/13942Mi)
% 246.31/35.90 % (2717357)Instruction limit reached!
% 246.31/35.90 % (2717357)------------------------------
% 246.31/35.90 % (2717357)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.31/35.90 % (2717357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.31/35.90 % (2717357)CaDiCaL version: 2.1.3
% 246.31/35.90 % (2717357)Termination reason: Instruction limit
% 246.31/35.90 % (2717357)Termination phase: Saturation
% 246.31/35.90 % (2717357)Time elapsed: 2.311 s
% 246.31/35.90 % (2717357)Peak memory usage: 187 MB
% 246.31/35.90 % (2717357)Instructions burned: 7346 (million)
% 246.31/35.90 % (2717369)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=2834533750:i=3604:fsr=off:er=filter_2746 on theBenchmark for (2746ds/3604Mi)
% 246.31/35.90 % (2717365)Instruction limit reached!
% 246.31/35.90 % (2717365)------------------------------
% 246.31/35.90 % (2717365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.31/35.90 % (2717365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.31/35.90 % (2717365)CaDiCaL version: 2.1.3
% 246.31/35.90 % (2717365)Termination reason: Instruction limit
% 246.31/35.90 % (2717365)Termination phase: Saturation
% 246.31/35.90 % (2717365)Time elapsed: 0.984 s
% 246.31/35.90 % (2717365)Peak memory usage: 132 MB
% 246.31/35.90 % (2717365)Instructions burned: 1504 (million)
% 246.31/35.90 % (2717371)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2676650893:i=1876:sd=1:ss=included:sgt=32_2744 on theBenchmark for (2744ds/1876Mi)
% 246.31/35.90 % (2717164)Instruction limit reached!
% 246.31/35.90 % (2717164)------------------------------
% 246.31/35.90 % (2717164)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.31/35.90 % (2717164)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.31/35.90 % (2717164)CaDiCaL version: 2.1.3
% 246.31/35.90 % (2717164)Termination reason: Instruction limit
% 246.31/35.90 % (2717164)Termination phase: Saturation
% 246.31/35.90 % (2717164)Time elapsed: 13.130 s
% 246.31/35.90 % (2717164)Peak memory usage: 277 MB
% 246.31/35.90 % (2717164)Instructions burned: 16413 (million)
% 246.31/35.90 % (2717369)Instruction limit reached!
% 246.31/35.90 % (2717369)------------------------------
% 246.31/35.90 % (2717369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.31/35.90 % (2717369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.31/35.90 % (2717369)CaDiCaL version: 2.1.3
% 246.31/35.90 % (2717369)Termination reason: Instruction limit
% 246.31/35.90 % (2717369)Termination phase: Saturation
% 246.31/35.90 % (2717369)Time elapsed: 1.052 s
% 246.31/35.90 % (2717369)Peak memory usage: 161 MB
% 246.31/35.90 % (2717369)Instructions burned: 3604 (million)
% 246.31/35.90 % (2717373)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=608122537:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2735 on theBenchmark for (2735ds/1932Mi)
% 246.31/35.90 % (2717374)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=1442905920:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2734 on theBenchmark for (2734ds/1980Mi)
% 246.31/35.90 % (2717371)Instruction limit reached!
% 246.31/35.90 % (2717371)------------------------------
% 246.31/35.90 % (2717371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 246.31/35.90 % (2717371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 246.31/35.90 % (2717371)CaDiCaL version: 2.1.3
% 246.31/35.90 % (2717371)Termination reason: Instruction limit
% 246.31/35.90 % (2717371)Termination phase: Saturation
% 246.31/35.90 % (2717371)Time elapsed: 1.201 s
% 246.31/35.90 % (2717371)Peak memory usage: 136 MB
% 246.31/35.90 % (2717371)Instructions burned: 1877 (million)
% 246.31/35.90 % (2717377)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=1815211284:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2731 on theBenchmark for (2731ds/3902Mi)
% 246.31/35.90 % (2717373)Refutation not found, incomplete strategy
% 246.31/35.90 % (2717373)------------------------------
% 246.31/35.90 % (2717373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.56/38.52 % (2717373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.56/38.52 % (2717373)CaDiCaL version: 2.1.3
% 264.56/38.52 % (2717373)Termination reason: Refutation not found, incomplete strategy
% 264.56/38.52 % (2717373)Time elapsed: 0.562 s
% 264.56/38.52 % (2717373)Peak memory usage: 127 MB
% 264.56/38.52 % (2717373)Instructions burned: 851 (million)
% 264.56/38.52 % (2717374)Instruction limit reached!
% 264.56/38.52 % (2717374)------------------------------
% 264.56/38.52 % (2717374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.56/38.52 % (2717374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.56/38.52 % (2717374)CaDiCaL version: 2.1.3
% 264.56/38.52 % (2717374)Termination reason: Instruction limit
% 264.56/38.52 % (2717374)Termination phase: Saturation
% 264.56/38.52 % (2717374)Time elapsed: 0.639 s
% 264.56/38.52 % (2717374)Peak memory usage: 131 MB
% 264.56/38.52 % (2717374)Instructions burned: 1981 (million)
% 264.56/38.52 % (2717379)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=581206634:avsq=on:i=3916:aac=none:amm=off_2727 on theBenchmark for (2727ds/3916Mi)
% 264.56/38.52 % (2717373)------------------------------
% 264.56/38.52 % (2717373)------------------------------
% 264.56/38.52 % (2717381)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3344760002:cond=on:i=3940:av=off:er=known_2725 on theBenchmark for (2725ds/3940Mi)
% 264.56/38.52 % (2717379)Instruction limit reached!
% 264.56/38.52 % (2717379)------------------------------
% 264.56/38.52 % (2717379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.56/38.52 % (2717379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.56/38.52 % (2717379)CaDiCaL version: 2.1.3
% 264.56/38.52 % (2717379)Termination reason: Instruction limit
% 264.56/38.52 % (2717379)Termination phase: Saturation
% 264.56/38.52 % (2717379)Time elapsed: 1.322 s
% 264.56/38.52 % (2717379)Peak memory usage: 123 MB
% 264.56/38.52 % (2717379)Instructions burned: 3916 (million)
% 264.56/38.52 % (2717633)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1393582869:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2712 on theBenchmark for (2712ds/3980Mi)
% 264.56/38.52 % (2717377)Instruction limit reached!
% 264.56/38.52 % (2717377)------------------------------
% 264.56/38.52 % (2717377)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.56/38.52 % (2717377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.56/38.52 % (2717377)CaDiCaL version: 2.1.3
% 264.56/38.52 % (2717377)Termination reason: Instruction limit
% 264.56/38.52 % (2717377)Termination phase: Saturation
% 264.56/38.52 % (2717377)Time elapsed: 2.694 s
% 264.56/38.52 % (2717377)Peak memory usage: 154 MB
% 264.56/38.52 % (2717377)Instructions burned: 3903 (million)
% 264.56/38.52 % (2717637)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=2200722877:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2702 on theBenchmark for (2702ds/2087Mi)
% 264.56/38.52 % (2717381)Instruction limit reached!
% 264.56/38.52 % (2717381)------------------------------
% 264.56/38.52 % (2717381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.56/38.52 % (2717381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.56/38.52 % (2717381)CaDiCaL version: 2.1.3
% 264.56/38.52 % (2717381)Termination reason: Instruction limit
% 264.56/38.52 % (2717381)Termination phase: Saturation
% 264.56/38.52 % (2717381)Time elapsed: 2.497 s
% 264.56/38.52 % (2717381)Peak memory usage: 154 MB
% 264.56/38.52 % (2717381)Instructions burned: 3940 (million)
% 264.56/38.52 % (2717639)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=1879217590:cts=off:cond=on:i=4272:bs=on:fsd=on_2698 on theBenchmark for (2698ds/4272Mi)
% 264.56/38.52 % (2717633)Instruction limit reached!
% 264.56/38.52 % (2717633)------------------------------
% 264.56/38.52 % (2717633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 264.56/38.52 % (2717633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 264.56/38.52 % (2717633)CaDiCaL version: 2.1.3
% 264.56/38.52 % (2717633)Termination reason: Instruction limit
% 264.56/38.52 % (2717633)Termination phase: Saturation
% 264.56/38.52 % (2717633)Time elapsed: 1.601 s
% 154.79/41.93 % (2717633)Peak memory usage: 156 MB
% 154.79/41.93 % (2717633)Instructions burned: 3983 (million)
% 154.79/41.93 % (2717710)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2141520765:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2694 on theBenchmark for (2694ds/2197Mi)
% 154.79/41.93 % (2717637)Instruction limit reached!
% 154.79/41.93 % (2717637)------------------------------
% 154.79/41.93 % (2717637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717637)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717637)Termination reason: Instruction limit
% 154.79/41.93 % (2717637)Termination phase: Saturation
% 154.79/41.93 % (2717637)Time elapsed: 1.337 s
% 154.79/41.93 % (2717637)Peak memory usage: 137 MB
% 154.79/41.93 % (2717637)Instructions burned: 2089 (million)
% 154.79/41.93 % (2717797)dis+21_1_sil=8000:spb=goal_then_units:random_seed=3951129876:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2687 on theBenchmark for (2687ds/6508Mi)
% 154.79/41.93 % (2717710)Instruction limit reached!
% 154.79/41.93 % (2717710)------------------------------
% 154.79/41.93 % (2717710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717710)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717710)Termination reason: Instruction limit
% 154.79/41.93 % (2717710)Termination phase: Saturation
% 154.79/41.93 % (2717710)Time elapsed: 0.738 s
% 154.79/41.93 % (2717710)Peak memory usage: 139 MB
% 154.79/41.93 % (2717710)Instructions burned: 2200 (million)
% 154.79/41.93 % (2717799)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=2322834540:i=2330:fgj=on:av=off:fsr=off_2685 on theBenchmark for (2685ds/2330Mi)
% 154.79/41.93 % (2717799)Instruction limit reached!
% 154.79/41.93 % (2717799)------------------------------
% 154.79/41.93 % (2717799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717799)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717799)Termination reason: Instruction limit
% 154.79/41.93 % (2717799)Termination phase: Saturation
% 154.79/41.93 % (2717799)Time elapsed: 0.883 s
% 154.79/41.93 % (2717799)Peak memory usage: 139 MB
% 154.79/41.93 % (2717799)Instructions burned: 2333 (million)
% 154.79/41.93 % (2717801)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2307001782:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2675 on theBenchmark for (2675ds/7592Mi)
% 154.79/41.93 % (2717639)Instruction limit reached!
% 154.79/41.93 % (2717639)------------------------------
% 154.79/41.93 % (2717639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717639)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717639)Termination reason: Instruction limit
% 154.79/41.93 % (2717639)Termination phase: Saturation
% 154.79/41.93 % (2717639)Time elapsed: 2.672 s
% 154.79/41.93 % (2717639)Peak memory usage: 155 MB
% 154.79/41.93 % (2717639)Instructions burned: 4273 (million)
% 154.79/41.93 % (2717803)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=1732076472:i=2693:kws=precedence:ins=1:av=off_2669 on theBenchmark for (2669ds/2693Mi)
% 154.79/41.93 % (2717367)Instruction limit reached!
% 154.79/41.93 % (2717367)------------------------------
% 154.79/41.93 % (2717367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717367)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717367)Termination reason: Instruction limit
% 154.79/41.93 % (2717367)Termination phase: Saturation
% 154.79/41.93 % (2717367)Time elapsed: 8.452 s
% 154.79/41.93 % (2717367)Peak memory usage: 236 MB
% 154.79/41.93 % (2717367)Instructions burned: 13944 (million)
% 154.79/41.93 % (2717805)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=268837375:i=28651:sd=4:ss=included:sgt=64_2665 on theBenchmark for (2665ds/28651Mi)
% 154.79/41.93 % (2717801)Instruction limit reached!
% 154.79/41.93 % (2717801)------------------------------
% 154.79/41.93 % (2717801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717801)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717801)Termination reason: Instruction limit
% 154.79/41.93 % (2717801)Termination phase: Saturation
% 154.79/41.93 % (2717801)Time elapsed: 2.031 s
% 154.79/41.93 % (2717801)Peak memory usage: 151 MB
% 154.79/41.93 % (2717801)Instructions burned: 7595 (million)
% 154.79/41.93 % (2717809)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=2640065542:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2653 on theBenchmark for (2653ds/2700Mi)
% 154.79/41.93 % (2717803)Instruction limit reached!
% 154.79/41.93 % (2717803)------------------------------
% 154.79/41.93 % (2717803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717803)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717803)Termination reason: Instruction limit
% 154.79/41.93 % (2717803)Termination phase: Saturation
% 154.79/41.93 % (2717803)Time elapsed: 1.710 s
% 154.79/41.93 % (2717803)Peak memory usage: 146 MB
% 154.79/41.93 % (2717803)Instructions burned: 2695 (million)
% 154.79/41.93 % (2717811)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=1947677848:i=3196:nm=4_2651 on theBenchmark for (2651ds/3196Mi)
% 154.79/41.93 % (2717797)Instruction limit reached!
% 154.79/41.93 % (2717797)------------------------------
% 154.79/41.93 % (2717797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717797)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717797)Termination reason: Instruction limit
% 154.79/41.93 % (2717797)Termination phase: Saturation
% 154.79/41.93 % (2717797)Time elapsed: 3.727 s
% 154.79/41.93 % (2717797)Peak memory usage: 146 MB
% 154.79/41.93 % (2717797)Instructions burned: 6508 (million)
% 154.79/41.93 % (2717813)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=291120025:cts=off:i=3254:av=off_2648 on theBenchmark for (2648ds/3254Mi)
% 154.79/41.93 % (2717809)Instruction limit reached!
% 154.79/41.93 % (2717809)------------------------------
% 154.79/41.93 % (2717809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717809)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717809)Termination reason: Instruction limit
% 154.79/41.93 % (2717809)Termination phase: Saturation
% 154.79/41.93 % (2717809)Time elapsed: 0.977 s
% 154.79/41.93 % (2717809)Peak memory usage: 143 MB
% 154.79/41.93 % (2717809)Instructions burned: 2702 (million)
% 154.79/41.93 % (2717815)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=3462133479:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2642 on theBenchmark for (2642ds/3264Mi)
% 154.79/41.93 % (2717811)Instruction limit reached!
% 154.79/41.93 % (2717811)------------------------------
% 154.79/41.93 % (2717811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717811)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717811)Termination reason: Instruction limit
% 154.79/41.93 % (2717811)Termination phase: Saturation
% 154.79/41.93 % (2717811)Time elapsed: 2.068 s
% 154.79/41.93 % (2717811)Peak memory usage: 148 MB
% 154.79/41.93 % (2717811)Instructions burned: 3197 (million)
% 154.79/41.93 % (2717815)Instruction limit reached!
% 154.79/41.93 % (2717815)------------------------------
% 154.79/41.93 % (2717815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717815)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717815)Termination reason: Instruction limit
% 154.79/41.93 % (2717815)Termination phase: Saturation
% 154.79/41.93 % (2717815)Time elapsed: 1.255 s
% 154.79/41.93 % (2717815)Peak memory usage: 144 MB
% 154.79/41.93 % (2717815)Instructions burned: 3266 (million)
% 154.79/41.93 % (2717818)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=2197584977:i=21997:s2at=5:gtg=all_2628 on theBenchmark for (2628ds/21997Mi)
% 154.79/41.93 % (2717817)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=1992425691:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2628 on theBenchmark for (2628ds/9708Mi)
% 154.79/41.93 % (2717813)Instruction limit reached!
% 154.79/41.93 % (2717813)------------------------------
% 154.79/41.93 % (2717813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.79/41.93 % (2717813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.79/41.93 % (2717813)CaDiCaL version: 2.1.3
% 154.79/41.93 % (2717813)Termination reason: Instruction limit
% 154.79/41.93 % (2717813)Termination phase: Saturation
% 154.79/41.93 % (2717813)Time elapsed: 2.021 s
% 154.79/41.93 % (2717813)Peak memory usage: 146 MB
% 154.79/41.93 % (2717813)Instructions burned: 3254 (million)
% 154.79/41.93 % (2717821)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2208884746:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2626 on theBenchmark for (2626ds/7551Mi)
% 154.79/41.93 % (2717805)First to succeed.
% 154.79/41.93 % (2717805)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2717077"
% 154.79/41.93 % (2717805)Refutation found. Thanks to Tanya!
% 154.79/41.93 % SZS status Unsatisfiable for theBenchmark
% 154.79/41.93 % SZS output start Proof for theBenchmark
% See solution above
% 288.95/42.04 % (2717805)------------------------------
% 288.95/42.04 % (2717805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 288.95/42.04 % (2717805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 288.95/42.04 % (2717805)CaDiCaL version: 2.1.3
% 288.95/42.04 % (2717805)Termination reason: Refutation
% 288.95/42.04 % (2717805)Time elapsed: 6.719 s
% 288.95/42.04 % (2717805)Peak memory usage: 227 MB
% 288.95/42.04 % (2717805)Instructions burned: 11334 (million)
% 288.95/42.04 % (2717805)------------------------------
% 288.95/42.04 % (2717805)------------------------------
% 288.95/42.04 % (2717077)Success in time 40.675 s
% 288.95/42.04 % Vampire exiting
%------------------------------------------------------------------------------