%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL329-3 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:59 AM UTC 2026
% Result : Unsatisfiable 137.30s 36.19s
% Output : Refutation 249.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 25
% Syntax : Number of formulae : 173 ( 51 unt; 14 def)
% Number of atoms : 354 ( 4 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 346 ( 165 ~; 167 |; 0 &)
% ( 14 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 12 ( 3 avg)
% Number of predicates : 18 ( 16 usr; 15 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 218 ( 0 sgn 218 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : axiom(implies(or(X0,X0),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_2) ).
fof(f2,axiom,
! [X0,X1] : axiom(implies(X0,or(X1,X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_3) ).
fof(f3,axiom,
! [X0,X1] : axiom(implies(or(X0,X1),or(X1,X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_4) ).
fof(f4,axiom,
! [X2,X0,X1] : axiom(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_5) ).
fof(f5,axiom,
! [X2,X0,X1] : axiom(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1_6) ).
fof(f6,axiom,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',implies_definition) ).
fof(f7,axiom,
! [X0] :
( ~ axiom(X0)
| theorem(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_1) ).
fof(f8,axiom,
! [X0,X1] :
( theorem(X0)
| ~ theorem(implies(X1,X0))
| ~ theorem(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rule_2) ).
fof(f9,axiom,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',and_defn) ).
fof(f10,axiom,
! [X0,X1] : equivalent(X0,X1) = and(implies(X0,X1),implies(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equivalent_defn) ).
fof(f11,negated_conjecture,
~ theorem(equivalent(not(or(and(p,q),and(not(p),not(q)))),or(and(p,not(q)),and(q,not(p))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f12,plain,
! [X0,X1] : equivalent(X0,X1) = not(or(not(or(not(X0),X1)),not(or(not(X1),X0)))),
inference(definition_unfolding,[],[f10,f9,f6,f6]) ).
fof(f13,plain,
~ theorem(not(or(not(or(not(not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))),not(or(not(or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p)))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))))))),
inference(definition_unfolding,[],[f11,f12,f9,f9,f9,f9]) ).
fof(f14,plain,
! [X2,X0,X1] : axiom(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(definition_unfolding,[],[f5,f6,f6,f6]) ).
fof(f15,plain,
! [X2,X0,X1] : axiom(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(definition_unfolding,[],[f4,f6]) ).
fof(f16,plain,
! [X0,X1] : axiom(or(not(or(X0,X1)),or(X1,X0))),
inference(definition_unfolding,[],[f3,f6]) ).
fof(f17,plain,
! [X0,X1] : axiom(or(not(X0),or(X1,X0))),
inference(definition_unfolding,[],[f2,f6]) ).
fof(f18,plain,
! [X0] : axiom(or(not(or(X0,X0)),X0)),
inference(definition_unfolding,[],[f1,f6]) ).
fof(f19,plain,
! [X0,X1] :
( ~ theorem(or(not(X1),X0))
| theorem(X0)
| ~ theorem(X1) ),
inference(definition_unfolding,[],[f8,f6]) ).
fof(f20,plain,
! [X2,X0,X1] : theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),or(X2,X1)))),
inference(resolution,[],[f7,f14]) ).
fof(f21,plain,
! [X0,X1] : theorem(or(not(or(X0,X1)),or(X1,X0))),
inference(resolution,[],[f7,f16]) ).
fof(f22,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,or(X1,X2))),or(X1,or(X0,X2)))),
inference(resolution,[],[f15,f7]) ).
fof(f23,plain,
! [X0] : theorem(or(not(or(X0,X0)),X0)),
inference(resolution,[],[f18,f7]) ).
fof(f24,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X0,X2)))
| ~ theorem(or(not(X1),X2)) ),
inference(resolution,[],[f19,f20]) ).
fof(f25,plain,
! [X0,X1] :
( ~ theorem(or(X1,X0))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f19,f21]) ).
fof(f26,plain,
! [X0,X1] : theorem(or(not(X0),or(X1,X0))),
inference(resolution,[],[f17,f7]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ theorem(or(X1,or(X0,X2)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f22,f19]) ).
fof(f30,plain,
! [X2,X0,X1] : theorem(or(not(or(X0,X1)),or(not(or(not(X1),X2)),or(X0,X2)))),
inference(resolution,[],[f29,f20]) ).
fof(f31,plain,
! [X0,X1] : theorem(or(X0,or(not(or(X1,X0)),X1))),
inference(resolution,[],[f29,f21]) ).
fof(f33,plain,
! [X0,X1] : theorem(or(X0,or(not(X1),X1))),
inference(resolution,[],[f29,f26]) ).
fof(f35,plain,
! [X0,X1] :
( theorem(or(not(or(X0,not(X1))),X0))
| ~ theorem(X1) ),
inference(resolution,[],[f31,f19]) ).
fof(f37,plain,
! [X2,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(X2,X1)))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f30,f19]) ).
fof(f39,plain,
! [X2,X0,X1] :
( ~ theorem(or(not(X0),X1))
| theorem(or(X2,X1))
| ~ theorem(or(X2,X0)) ),
inference(resolution,[],[f24,f19]) ).
fof(f41,plain,
! [X2,X3,X0,X1] :
( theorem(or(X0,or(not(or(X1,X2)),or(X1,X3))))
| ~ theorem(or(X0,or(not(X2),X3))) ),
inference(resolution,[],[f39,f20]) ).
fof(f42,plain,
! [X2,X0,X1] :
( ~ theorem(or(X0,or(X2,X1)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f39,f21]) ).
fof(f43,plain,
! [X2,X3,X0,X1] :
( theorem(or(X0,or(not(or(not(X1),X2)),or(X3,X2))))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f39,f30]) ).
fof(f44,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X0,or(X1,X3)))
| theorem(or(X0,or(X1,X2)))
| ~ theorem(or(not(X3),X2)) ),
inference(resolution,[],[f39,f24]) ).
fof(f47,plain,
! [X0,X1] :
( ~ theorem(or(X0,or(X1,X1)))
| theorem(or(X0,X1)) ),
inference(resolution,[],[f39,f23]) ).
fof(f54,plain,
! [X0,X1] : theorem(or(not(X0),or(X0,X1))),
inference(resolution,[],[f42,f26]) ).
fof(f65,plain,
! [X0,X1] : theorem(or(X0,or(not(X0),X1))),
inference(resolution,[],[f54,f29]) ).
fof(f67,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(not(X0),X1)),or(not(or(X2,X0)),X3)))
| ~ theorem(or(not(or(X2,X1)),X3)) ),
inference(resolution,[],[f44,f20]) ).
fof(f68,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X1,X2)))
| ~ theorem(or(not(X0),X2)) ),
inference(resolution,[],[f44,f21]) ).
fof(f77,plain,
! [X0,X1] :
( ~ theorem(or(X1,not(X0)))
| theorem(X1)
| ~ theorem(X0) ),
inference(resolution,[],[f35,f19]) ).
fof(f83,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(or(X0,X1)),X2))
| theorem(or(not(or(X0,X3)),X2))
| ~ theorem(or(not(X3),X1)) ),
inference(resolution,[],[f67,f19]) ).
fof(f91,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(X1)))),
inference(resolution,[],[f33,f42]) ).
fof(f94,plain,
! [X0,X1] :
( theorem(or(X0,not(X0)))
| ~ theorem(X1) ),
inference(resolution,[],[f91,f19]) ).
fof(f97,plain,
! [X0,X1] : theorem(or(X0,or(X1,not(X0)))),
inference(resolution,[],[f91,f29]) ).
fof(f99,definition,
( spl0_1
<=> ! [X1] : ~ theorem(X1) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f100,plain,
( ! [X1] : ~ theorem(X1)
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f99]) ).
fof(f102,definition,
( spl0_2
<=> ! [X0] : theorem(or(X0,not(X0))) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f103,plain,
( ! [X0] : theorem(or(X0,not(X0)))
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f102]) ).
fof(f104,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f94,f102,f99]) ).
fof(f105,plain,
( ! [X0,X1] :
( theorem(or(X0,not(not(X1))))
| ~ theorem(or(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f103,f39]) ).
fof(f108,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(X0),or(not(X1),X2)))
| theorem(or(not(or(X3,X1)),or(X3,X2)))
| ~ theorem(X0) ),
inference(resolution,[],[f41,f19]) ).
fof(f113,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(not(X0),or(X1,X2)))
| theorem(or(not(or(not(X2),X3)),or(X1,X3)))
| ~ theorem(X0) ),
inference(resolution,[],[f43,f19]) ).
fof(f138,plain,
! [X0,X1] :
( theorem(or(not(or(X0,X1)),X1))
| ~ theorem(or(not(X0),X1)) ),
inference(resolution,[],[f68,f47]) ).
fof(f146,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(not(or(X0,X1)),X2)),or(X3,X2)))
| ~ theorem(or(X0,or(X3,X1))) ),
inference(resolution,[],[f113,f22]) ).
fof(f155,plain,
! [X2,X0,X1] :
( theorem(or(not(or(not(not(X0)),X1)),or(X0,X1)))
| ~ theorem(X2) ),
inference(resolution,[],[f113,f91]) ).
fof(f157,definition,
( spl0_3
<=> ! [X0,X1] : theorem(or(not(or(not(not(X0)),X1)),or(X0,X1))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f158,plain,
( ! [X0,X1] : theorem(or(not(or(not(not(X0)),X1)),or(X0,X1)))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f159,plain,
( spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f155,f157,f99]) ).
fof(f170,plain,
( ! [X0,X1] :
( theorem(or(not(not(X1)),X0))
| ~ theorem(or(X0,X1)) )
| ~ spl0_2 ),
inference(resolution,[],[f105,f25]) ).
fof(f178,plain,
! [X0,X1] : theorem(or(or(X0,not(X1)),X1)),
inference(resolution,[],[f97,f25]) ).
fof(f179,plain,
( $false
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f178,f100]) ).
fof(f180,plain,
~ spl0_1,
inference(avatar_contradiction_clause,[],[f179]) ).
fof(f190,plain,
! [X2,X3,X0,X1] :
( ~ theorem(or(X2,or(not(X1),X3)))
| theorem(or(X2,or(X0,X3)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f37,f39]) ).
fof(f236,plain,
! [X0,X1] : theorem(or(or(not(X0),X1),X0)),
inference(resolution,[],[f65,f25]) ).
fof(f247,plain,
! [X2,X0,X1] :
( theorem(or(not(not(X0)),or(X1,X2)))
| ~ theorem(or(X1,X0)) ),
inference(resolution,[],[f190,f54]) ).
fof(f336,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X1)),or(X0,not(not(X1)))))
| ~ theorem(X2) ),
inference(resolution,[],[f108,f91]) ).
fof(f340,definition,
( spl0_4
<=> ! [X0,X1] : theorem(or(not(or(X0,X1)),or(X0,not(not(X1))))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f341,plain,
( ! [X0,X1] : theorem(or(not(or(X0,X1)),or(X0,not(not(X1)))))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f340]) ).
fof(f342,plain,
( spl0_1
| spl0_4 ),
inference(avatar_split_clause,[],[f336,f340,f99]) ).
fof(f347,plain,
( ! [X2,X0,X1] :
( theorem(or(X0,or(X1,not(not(X2)))))
| ~ theorem(or(X0,or(X1,X2))) )
| ~ spl0_4 ),
inference(resolution,[],[f341,f39]) ).
fof(f357,plain,
! [X2,X0,X1] :
( theorem(or(not(or(X0,X2)),X1))
| ~ theorem(or(not(X0),X1))
| ~ theorem(or(not(X2),X1)) ),
inference(resolution,[],[f138,f83]) ).
fof(f388,plain,
! [X2,X0,X1] :
( theorem(or(not(not(X1)),or(X2,X0)))
| ~ theorem(or(X0,X1)) ),
inference(resolution,[],[f247,f42]) ).
fof(f434,plain,
! [X2,X3,X0,X1,X4] :
( ~ theorem(or(X3,or(not(or(X0,X2)),X4)))
| theorem(or(X3,or(X1,X4)))
| ~ theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f146,f39]) ).
fof(f456,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(not(or(X0,X1))),or(X2,X3)))
| ~ theorem(or(X0,or(X2,X1))) ),
inference(resolution,[],[f434,f54]) ).
fof(f463,plain,
! [X2,X0,X1] :
( ~ theorem(or(X2,or(X1,X0)))
| theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f434,f31]) ).
fof(f502,plain,
( ! [X2,X0,X1] :
( theorem(or(not(not(X0)),or(X1,X2)))
| ~ theorem(or(X2,or(X1,X0))) )
| ~ spl0_4 ),
inference(resolution,[],[f463,f347]) ).
fof(f513,plain,
! [X2,X0,X1] :
( theorem(or(not(not(or(X0,X2))),X1))
| ~ theorem(or(X0,or(X1,X2))) ),
inference(resolution,[],[f456,f47]) ).
fof(f515,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ theorem(or(X0,or(not(or(X1,X2)),X3)))
| theorem(or(not(not(or(X0,X3))),or(X4,X5)))
| ~ theorem(or(X1,or(X4,X2))) ),
inference(resolution,[],[f456,f434]) ).
fof(f539,plain,
( ! [X0,X1] :
( ~ theorem(or(X0,or(X0,X1)))
| theorem(or(not(not(X1)),X0)) )
| ~ spl0_4 ),
inference(resolution,[],[f502,f47]) ).
fof(f689,plain,
( ! [X0,X1] :
( ~ theorem(or(not(not(X0)),X1))
| theorem(or(X0,X1)) )
| ~ spl0_3 ),
inference(resolution,[],[f158,f19]) ).
fof(f830,plain,
! [X0,X1] :
( theorem(not(or(not(X0),not(X1))))
| ~ theorem(X0)
| ~ theorem(X1) ),
inference(resolution,[],[f77,f35]) ).
fof(f837,plain,
( ~ theorem(or(not(not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p)))))))
| ~ theorem(or(not(or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p)))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q)))))))) ),
inference(resolution,[],[f830,f13]) ).
fof(f839,definition,
( spl0_5
<=> theorem(or(not(or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p)))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f841,plain,
( ~ theorem(or(not(or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p)))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))))
| spl0_5 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f843,definition,
( spl0_6
<=> theorem(or(not(not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f845,plain,
( ~ theorem(or(not(not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p)))))))
| spl0_6 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f846,plain,
( ~ spl0_5
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f837,f843,f839]) ).
fof(f979,definition,
( spl0_8
<=> theorem(or(not(not(or(not(q),not(not(p))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f981,plain,
( ~ theorem(or(not(not(or(not(q),not(not(p))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))))
| spl0_8 ),
inference(avatar_component_clause,[],[f979]) ).
fof(f1077,plain,
( ~ theorem(or(not(not(or(not(p),not(not(q))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))))
| ~ theorem(or(not(not(or(not(q),not(not(p))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))))
| spl0_5 ),
inference(resolution,[],[f357,f841]) ).
fof(f1087,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(or(X0,X3)),or(X2,X1)))
| ~ theorem(or(not(X3),or(X1,X2)))
| ~ theorem(or(not(X0),or(X1,X2))) ),
inference(resolution,[],[f357,f42]) ).
fof(f1088,plain,
! [X2,X3,X0,X1] :
( theorem(or(X1,or(not(or(X0,X3)),X2)))
| ~ theorem(or(not(X3),or(X1,X2)))
| ~ theorem(or(not(X0),or(X1,X2))) ),
inference(resolution,[],[f357,f29]) ).
fof(f1099,definition,
( spl0_9
<=> theorem(or(not(not(or(not(p),not(not(q))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f1101,plain,
( ~ theorem(or(not(not(or(not(p),not(not(q))))),not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q))))))))
| spl0_9 ),
inference(avatar_component_clause,[],[f1099]) ).
fof(f1102,plain,
( ~ spl0_8
| ~ spl0_9
| spl0_5 ),
inference(avatar_split_clause,[],[f1077,f839,f1099,f979]) ).
fof(f1103,plain,
( ~ theorem(or(not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q)))))),or(not(q),not(not(p)))))
| ~ spl0_2
| spl0_8 ),
inference(resolution,[],[f981,f170]) ).
fof(f1125,plain,
( ~ theorem(or(not(not(or(not(p),not(q)))),or(not(q),not(not(p)))))
| ~ theorem(or(not(not(or(not(not(p)),not(not(q))))),or(not(q),not(not(p)))))
| ~ spl0_2
| spl0_8 ),
inference(resolution,[],[f1103,f357]) ).
fof(f1130,definition,
( spl0_10
<=> theorem(or(not(not(or(not(not(p)),not(not(q))))),or(not(q),not(not(p))))) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f1132,plain,
( ~ theorem(or(not(not(or(not(not(p)),not(not(q))))),or(not(q),not(not(p)))))
| spl0_10 ),
inference(avatar_component_clause,[],[f1130]) ).
fof(f1134,definition,
( spl0_11
<=> theorem(or(not(not(or(not(p),not(q)))),or(not(q),not(not(p))))) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f1136,plain,
( ~ theorem(or(not(not(or(not(p),not(q)))),or(not(q),not(not(p)))))
| spl0_11 ),
inference(avatar_component_clause,[],[f1134]) ).
fof(f1137,plain,
( ~ spl0_10
| ~ spl0_11
| ~ spl0_2
| spl0_8 ),
inference(avatar_split_clause,[],[f1125,f979,f102,f1134,f1130]) ).
fof(f1691,plain,
( ~ theorem(or(not(or(not(or(not(p),not(q))),not(or(not(not(p)),not(not(q)))))),or(not(p),not(not(q)))))
| ~ spl0_2
| spl0_9 ),
inference(resolution,[],[f1101,f170]) ).
fof(f1693,plain,
( ~ theorem(or(not(not(or(not(not(p)),not(not(q))))),or(not(not(q)),not(p))))
| ~ theorem(or(not(not(or(not(p),not(q)))),or(not(not(q)),not(p))))
| ~ spl0_2
| spl0_9 ),
inference(resolution,[],[f1691,f1087]) ).
fof(f1712,definition,
( spl0_21
<=> theorem(or(not(not(or(not(p),not(q)))),or(not(not(q)),not(p)))) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f1714,plain,
( ~ theorem(or(not(not(or(not(p),not(q)))),or(not(not(q)),not(p))))
| spl0_21 ),
inference(avatar_component_clause,[],[f1712]) ).
fof(f1716,definition,
( spl0_22
<=> theorem(or(not(not(or(not(not(p)),not(not(q))))),or(not(not(q)),not(p)))) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f1718,plain,
( ~ theorem(or(not(not(or(not(not(p)),not(not(q))))),or(not(not(q)),not(p))))
| spl0_22 ),
inference(avatar_component_clause,[],[f1716]) ).
fof(f1719,plain,
( ~ spl0_21
| ~ spl0_22
| ~ spl0_2
| spl0_9 ),
inference(avatar_split_clause,[],[f1693,f1099,f102,f1716,f1712]) ).
fof(f1722,plain,
( ~ theorem(or(not(not(p)),or(not(p),not(q))))
| spl0_11 ),
inference(resolution,[],[f1136,f388]) ).
fof(f1733,plain,
( $false
| spl0_11 ),
inference(forward_subsumption_resolution,[],[f1722,f54]) ).
fof(f1734,plain,
spl0_11,
inference(avatar_contradiction_clause,[],[f1733]) ).
fof(f2185,plain,
( ~ theorem(or(not(q),or(not(not(p)),not(not(q)))))
| spl0_10 ),
inference(resolution,[],[f1132,f247]) ).
fof(f2196,plain,
( $false
| spl0_10 ),
inference(forward_subsumption_resolution,[],[f2185,f97]) ).
fof(f2197,plain,
spl0_10,
inference(avatar_contradiction_clause,[],[f2196]) ).
fof(f2417,plain,
( ~ theorem(or(not(not(q)),or(not(p),not(q))))
| spl0_21 ),
inference(resolution,[],[f1714,f247]) ).
fof(f2429,plain,
( $false
| spl0_21 ),
inference(forward_subsumption_resolution,[],[f2417,f26]) ).
fof(f2430,plain,
spl0_21,
inference(avatar_contradiction_clause,[],[f2429]) ).
fof(f4814,plain,
! [X2,X3,X0,X1] :
( theorem(or(not(not(or(X0,X1))),or(X2,X3)))
| ~ theorem(or(X1,or(X2,X0))) ),
inference(resolution,[],[f515,f31]) ).
fof(f4876,plain,
( ! [X2,X3,X0,X1] :
( theorem(or(or(X2,X0),or(X1,X3)))
| ~ theorem(or(X0,or(X1,X2))) )
| ~ spl0_3 ),
inference(resolution,[],[f4814,f689]) ).
fof(f4911,plain,
( ! [X2,X3,X0,X1] :
( theorem(or(or(X2,X0),or(X3,X1)))
| ~ theorem(or(X0,or(X1,X2))) )
| ~ spl0_3 ),
inference(resolution,[],[f4876,f42]) ).
fof(f5208,plain,
( ~ theorem(or(not(p),or(not(not(p)),not(not(q)))))
| spl0_22 ),
inference(resolution,[],[f1718,f388]) ).
fof(f5226,plain,
( $false
| spl0_22 ),
inference(forward_subsumption_resolution,[],[f5208,f65]) ).
fof(f5227,plain,
spl0_22,
inference(avatar_contradiction_clause,[],[f5226]) ).
fof(f7848,plain,
( ~ theorem(or(not(or(not(p),not(q))),or(or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))),not(or(not(not(p)),not(not(q)))))))
| spl0_6 ),
inference(resolution,[],[f513,f845]) ).
fof(f7900,plain,
( ~ theorem(or(not(not(q)),or(not(or(not(not(p)),not(not(q)))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| ~ theorem(or(not(not(p)),or(not(or(not(not(p)),not(not(q)))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| spl0_6 ),
inference(resolution,[],[f7848,f1087]) ).
fof(f7929,definition,
( spl0_190
<=> theorem(or(not(not(p)),or(not(or(not(not(p)),not(not(q)))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_190])],[avatar_definition]) ).
fof(f7931,plain,
( ~ theorem(or(not(not(p)),or(not(or(not(not(p)),not(not(q)))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| spl0_190 ),
inference(avatar_component_clause,[],[f7929]) ).
fof(f7933,definition,
( spl0_191
<=> theorem(or(not(not(q)),or(not(or(not(not(p)),not(not(q)))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f7935,plain,
( ~ theorem(or(not(not(q)),or(not(or(not(not(p)),not(not(q)))),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| spl0_191 ),
inference(avatar_component_clause,[],[f7933]) ).
fof(f7936,plain,
( ~ spl0_190
| ~ spl0_191
| spl0_6 ),
inference(avatar_split_clause,[],[f7900,f843,f7933,f7929]) ).
fof(f7957,plain,
( ~ theorem(or(not(not(not(q))),or(not(not(q)),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| ~ theorem(or(not(not(not(p))),or(not(not(q)),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| spl0_191 ),
inference(resolution,[],[f7935,f1088]) ).
fof(f7961,plain,
( ~ theorem(or(not(not(not(p))),or(not(not(q)),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| spl0_191 ),
inference(forward_subsumption_resolution,[],[f7957,f54]) ).
fof(f8248,plain,
( ~ theorem(or(not(not(not(q))),or(not(not(p)),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| ~ theorem(or(not(not(not(p))),or(not(not(p)),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| spl0_190 ),
inference(resolution,[],[f7931,f1088]) ).
fof(f8252,plain,
( ~ theorem(or(not(not(not(q))),or(not(not(p)),or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))))))
| spl0_190 ),
inference(forward_subsumption_resolution,[],[f8248,f54]) ).
fof(f9440,plain,
( ! [X2,X0,X1] :
( theorem(or(not(not(X0)),or(X1,X2)))
| ~ theorem(or(X2,or(X0,X1))) )
| ~ spl0_3
| ~ spl0_4 ),
inference(resolution,[],[f539,f4911]) ).
fof(f9550,plain,
( ~ theorem(or(or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))),or(not(q),not(not(p)))))
| ~ spl0_3
| ~ spl0_4
| spl0_190 ),
inference(resolution,[],[f9440,f8252]) ).
fof(f9604,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| spl0_190 ),
inference(forward_subsumption_resolution,[],[f9550,f178]) ).
fof(f9605,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_190 ),
inference(avatar_contradiction_clause,[],[f9604]) ).
fof(f9677,plain,
( ~ theorem(or(or(not(or(not(p),not(not(q)))),not(or(not(q),not(not(p))))),or(not(p),not(not(q)))))
| ~ spl0_3
| ~ spl0_4
| spl0_191 ),
inference(resolution,[],[f7961,f9440]) ).
fof(f9685,plain,
( $false
| ~ spl0_3
| ~ spl0_4
| spl0_191 ),
inference(forward_subsumption_resolution,[],[f9677,f236]) ).
fof(f9686,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_191 ),
inference(avatar_contradiction_clause,[],[f9685]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f104]) ).
cnf(s2,plain,
( spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f159]) ).
cnf(s3,plain,
~ spl0_1,
inference(sat_conversion,[],[f180]) ).
cnf(s4,plain,
( spl0_1
| spl0_4 ),
inference(sat_conversion,[],[f342]) ).
cnf(s5,plain,
( ~ spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f846]) ).
cnf(s7,plain,
( spl0_5
| ~ spl0_8
| ~ spl0_9 ),
inference(sat_conversion,[],[f1102]) ).
cnf(s8,plain,
( ~ spl0_2
| spl0_8
| ~ spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f1137]) ).
cnf(s18,plain,
( ~ spl0_2
| spl0_9
| ~ spl0_21
| ~ spl0_22 ),
inference(sat_conversion,[],[f1719]) ).
cnf(s20,plain,
spl0_11,
inference(sat_conversion,[],[f1734]) ).
cnf(s29,plain,
spl0_10,
inference(sat_conversion,[],[f2197]) ).
cnf(s42,plain,
spl0_21,
inference(sat_conversion,[],[f2430]) ).
cnf(s165,plain,
spl0_22,
inference(sat_conversion,[],[f5227]) ).
cnf(s287,plain,
( spl0_6
| ~ spl0_190
| ~ spl0_191 ),
inference(sat_conversion,[],[f7936]) ).
cnf(s325,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_190 ),
inference(sat_conversion,[],[f9605]) ).
cnf(s334,plain,
( ~ spl0_3
| ~ spl0_4
| spl0_191 ),
inference(sat_conversion,[],[f9686]) ).
cnf(s350,plain,
( ~ spl0_2
| spl0_9 ),
inference(rat,[],[s18,s165,s42]) ).
cnf(s357,plain,
( ~ spl0_2
| spl0_8 ),
inference(rat,[],[s8,s20,s29]) ).
cnf(s370,plain,
spl0_4,
inference(rat,[],[s4,s3]) ).
cnf(s375,plain,
spl0_3,
inference(rat,[],[s2,s3]) ).
cnf(s376,plain,
spl0_191,
inference(rat,[],[s334,s370,s375]) ).
cnf(s377,plain,
spl0_190,
inference(rat,[],[s325,s370,s375]) ).
cnf(s381,plain,
spl0_6,
inference(rat,[],[s287,s376,s377]) ).
cnf(s382,plain,
~ spl0_5,
inference(rat,[],[s5,s381]) ).
cnf(s383,plain,
spl0_2,
inference(rat,[],[s1,s3]) ).
cnf(s386,plain,
spl0_9,
inference(rat,[],[s350,s383]) ).
cnf(s387,plain,
spl0_8,
inference(rat,[],[s357,s383]) ).
cnf(s391,plain,
$false,
inference(rat,[],[s7,s382,s386,s387]) ).
fof(f9687,plain,
$false,
inference(avatar_sat_refutation,[],[s391]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL329-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n002.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 15:37:22 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.50/3.17 % (3687889)Input is clausal, will run a generic CNF schedule.
% 16.50/3.17 % (3687967)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1918623291:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 16.50/3.17 % (3687973)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3110562128:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 16.50/3.17 % (3687971)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1019260748:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 16.50/3.17 % (3687970)lrs+10_1_sil=8000:sp=occurrence:random_seed=3557907509:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 16.50/3.17 % (3687965)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=1699061399:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 16.50/3.17 % (3687974)dis-21_1_sil=8000:lcm=predicate:random_seed=3472486748: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)
% 16.50/3.17 % (3687968)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2299894899:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 16.50/3.17 % (3687974)Instruction limit reached!
% 16.50/3.17 % (3687974)------------------------------
% 16.50/3.17 % (3687974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.50/3.17 % (3687974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.50/3.17 % (3687974)CaDiCaL version: 2.1.3
% 16.50/3.17 % (3687974)Termination reason: Instruction limit
% 16.50/3.17 % (3687974)Termination phase: Saturation
% 16.50/3.17 % (3687974)Time elapsed: 0.056 s
% 16.50/3.17 % (3687974)Peak memory usage: 87 MB
% 16.50/3.17 % (3687974)Instructions burned: 118 (million)
% 16.50/3.17 % (3687970)Instruction limit reached!
% 16.50/3.17 % (3687970)------------------------------
% 16.50/3.17 % (3687970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.50/3.17 % (3687970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.50/3.17 % (3687970)CaDiCaL version: 2.1.3
% 16.50/3.17 % (3687970)Termination reason: Instruction limit
% 16.50/3.17 % (3687970)Termination phase: Saturation
% 16.50/3.17 % (3687970)Time elapsed: 0.070 s
% 16.50/3.17 % (3687970)Peak memory usage: 89 MB
% 16.50/3.17 % (3687970)Instructions burned: 107 (million)
% 16.50/3.17 % (3687971)Instruction limit reached!
% 16.50/3.17 % (3687971)------------------------------
% 16.50/3.17 % (3687971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.50/3.17 % (3687971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.50/3.17 % (3687971)CaDiCaL version: 2.1.3
% 16.50/3.17 % (3687971)Termination reason: Instruction limit
% 16.50/3.17 % (3687971)Termination phase: Saturation
% 16.50/3.17 % (3687971)Time elapsed: 0.072 s
% 16.50/3.17 % (3687971)Peak memory usage: 88 MB
% 16.50/3.17 % (3687971)Instructions burned: 115 (million)
% 16.50/3.17 % (3687973)Instruction limit reached!
% 16.50/3.17 % (3687973)------------------------------
% 16.50/3.17 % (3687973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.50/3.17 % (3687973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.50/3.17 % (3687973)CaDiCaL version: 2.1.3
% 16.50/3.17 % (3687973)Termination reason: Instruction limit
% 16.50/3.17 % (3687973)Termination phase: Saturation
% 16.50/3.17 % (3687973)Time elapsed: 0.109 s
% 16.50/3.17 % (3687973)Peak memory usage: 89 MB
% 16.50/3.17 % (3687973)Instructions burned: 181 (million)
% 16.50/3.17 % (3687990)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=2394976600:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 16.50/3.17 % (3687990)Refutation not found, incomplete strategy
% 16.50/3.17 % (3687990)------------------------------
% 16.50/3.17 % (3687990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.50/3.17 % (3687990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.50/3.17 % (3687990)CaDiCaL version: 2.1.3
% 16.50/3.17 % (3687990)Termination reason: Refutation not found, incomplete strategy
% 16.50/3.17 % (3687990)Time elapsed: 0.001 s
% 16.50/3.17 % (3687990)Peak memory usage: 88 MB
% 16.50/3.17 % (3687992)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2959726785:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 28.27/5.03 % (3687991)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1908638856:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 28.27/5.03 % (3687991)Refutation not found, incomplete strategy
% 28.27/5.03 % (3687991)------------------------------
% 28.27/5.03 % (3687991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.27/5.03 % (3687991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.27/5.03 % (3687991)CaDiCaL version: 2.1.3
% 28.27/5.03 % (3687991)Termination reason: Refutation not found, incomplete strategy
% 28.27/5.03 % (3687991)Time elapsed: 0.001 s
% 28.27/5.03 % (3687991)Peak memory usage: 87 MB
% 28.27/5.03 % (3687992)Refutation not found, incomplete strategy
% 28.27/5.03 % (3687992)------------------------------
% 28.27/5.03 % (3687992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.27/5.03 % (3687992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.27/5.03 % (3687992)CaDiCaL version: 2.1.3
% 28.27/5.03 % (3687992)Termination reason: Refutation not found, incomplete strategy
% 28.27/5.03 % (3687992)Time elapsed: 0.002 s
% 28.27/5.03 % (3687992)Peak memory usage: 88 MB
% 28.27/5.03 % (3687992)Instructions burned: 2 (million)
% 28.27/5.03 % (3687997)lrs+10_64_to=lpo:sil=8000:random_seed=2916029180:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 28.27/5.03 % (3687997)Instruction limit reached!
% 28.27/5.03 % (3687997)------------------------------
% 28.27/5.03 % (3687997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.27/5.03 % (3687997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.27/5.03 % (3687997)CaDiCaL version: 2.1.3
% 28.27/5.03 % (3687997)Termination reason: Instruction limit
% 28.27/5.03 % (3687997)Termination phase: Saturation
% 28.27/5.03 % (3687997)Time elapsed: 0.073 s
% 28.27/5.03 % (3687997)Peak memory usage: 89 MB
% 28.27/5.03 % (3687997)Instructions burned: 127 (million)
% 28.27/5.03 % (3687990)------------------------------
% 28.27/5.03 % (3687990)------------------------------
% 28.27/5.03 % (3687992)------------------------------
% 28.27/5.03 % (3687992)------------------------------
% 28.27/5.03 % (3687991)------------------------------
% 28.27/5.03 % (3687991)------------------------------
% 28.27/5.03 % (3688017)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3216290876:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 28.27/5.03 % (3688022)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2981641356:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 28.27/5.03 % (3688031)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=1364581513:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 28.27/5.03 % (3688028)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1006395562:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 28.27/5.03 % (3688017)Instruction limit reached!
% 28.27/5.03 % (3688017)------------------------------
% 28.27/5.03 % (3688017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.27/5.03 % (3688017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.27/5.03 % (3688017)CaDiCaL version: 2.1.3
% 28.27/5.03 % (3688017)Termination reason: Instruction limit
% 28.27/5.03 % (3688017)Termination phase: Saturation
% 28.27/5.03 % (3688017)Time elapsed: 0.122 s
% 28.27/5.03 % (3688017)Peak memory usage: 90 MB
% 28.27/5.03 % (3688017)Instructions burned: 195 (million)
% 28.27/5.03 % (3688031)Instruction limit reached!
% 28.27/5.03 % (3688031)------------------------------
% 28.27/5.03 % (3688031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.27/5.03 % (3688031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.27/5.03 % (3688031)CaDiCaL version: 2.1.3
% 28.27/5.03 % (3688031)Termination reason: Instruction limit
% 28.27/5.03 % (3688031)Termination phase: Saturation
% 28.27/5.03 % (3688031)Time elapsed: 0.056 s
% 28.27/5.03 % (3688031)Peak memory usage: 88 MB
% 28.27/5.03 % (3688031)Instructions burned: 107 (million)
% 28.27/5.03 % (3688022)Instruction limit reached!
% 28.27/5.03 % (3688022)------------------------------
% 28.27/5.03 % (3688022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.64/6.58 % (3688022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.64/6.58 % (3688022)CaDiCaL version: 2.1.3
% 39.64/6.58 % (3688022)Termination reason: Instruction limit
% 39.64/6.58 % (3688022)Termination phase: Saturation
% 39.64/6.58 % (3688022)Time elapsed: 0.104 s
% 39.64/6.58 % (3688022)Peak memory usage: 91 MB
% 39.64/6.58 % (3688022)Instructions burned: 158 (million)
% 39.64/6.58 % (3688038)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3481696294:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 39.64/6.58 % (3688038)Refutation not found, incomplete strategy
% 39.64/6.58 % (3688038)------------------------------
% 39.64/6.58 % (3688038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.64/6.58 % (3688038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.64/6.58 % (3688038)CaDiCaL version: 2.1.3
% 39.64/6.58 % (3688038)Termination reason: Refutation not found, incomplete strategy
% 39.64/6.58 % (3688038)Time elapsed: 0.001 s
% 39.64/6.58 % (3688038)Peak memory usage: 87 MB
% 39.64/6.58 % (3688039)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3654268561:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 39.64/6.58 % (3688040)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2459156050:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 39.64/6.58 % (3688039)Instruction limit reached!
% 39.64/6.58 % (3688039)------------------------------
% 39.64/6.58 % (3688039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.64/6.58 % (3688039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.64/6.58 % (3688039)CaDiCaL version: 2.1.3
% 39.64/6.58 % (3688039)Termination reason: Instruction limit
% 39.64/6.58 % (3688039)Termination phase: Saturation
% 39.64/6.58 % (3688039)Time elapsed: 0.140 s
% 39.64/6.58 % (3688039)Peak memory usage: 91 MB
% 39.64/6.58 % (3688039)Instructions burned: 242 (million)
% 39.64/6.58 % (3688038)------------------------------
% 39.64/6.58 % (3688038)------------------------------
% 39.64/6.58 % (3688044)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2179761729:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 39.64/6.58 % (3688053)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3783860324:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 39.64/6.58 % (3688044)Instruction limit reached!
% 39.64/6.58 % (3688044)------------------------------
% 39.64/6.58 % (3688044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.64/6.58 % (3688044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.64/6.58 % (3688044)CaDiCaL version: 2.1.3
% 39.64/6.58 % (3688044)Termination reason: Instruction limit
% 39.64/6.58 % (3688044)Termination phase: Saturation
% 39.64/6.58 % (3688044)Time elapsed: 0.141 s
% 39.64/6.58 % (3688044)Peak memory usage: 89 MB
% 39.64/6.58 % (3688044)Instructions burned: 135 (million)
% 39.64/6.58 % (3688067)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2549328406:i=191:fgj=on:bd=all_2984 on theBenchmark for (2984ds/191Mi)
% 39.64/6.58 % (3688053)Instruction limit reached!
% 39.64/6.58 % (3688053)------------------------------
% 39.64/6.58 % (3688053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.64/6.58 % (3688053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.64/6.58 % (3688053)CaDiCaL version: 2.1.3
% 39.64/6.58 % (3688053)Termination reason: Instruction limit
% 39.64/6.58 % (3688053)Termination phase: Saturation
% 39.64/6.58 % (3688053)Time elapsed: 0.494 s
% 39.64/6.58 % (3688053)Peak memory usage: 93 MB
% 39.64/6.58 % (3688053)Instructions burned: 500 (million)
% 39.64/6.58 % (3688067)Instruction limit reached!
% 39.64/6.58 % (3688067)------------------------------
% 39.64/6.58 % (3688067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.64/6.58 % (3688067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.64/6.58 % (3688067)CaDiCaL version: 2.1.3
% 39.64/6.58 % (3688067)Termination reason: Instruction limit
% 39.64/6.58 % (3688067)Termination phase: Saturation
% 39.64/6.58 % (3688067)Time elapsed: 0.197 s
% 39.64/6.58 % (3688067)Peak memory usage: 93 MB
% 39.64/6.58 % (3688067)Instructions burned: 191 (million)
% 39.64/6.58 % (3688078)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3740047744:i=264:kws=precedence:fsr=off_2979 on theBenchmark for (2979ds/264Mi)
% 66.09/10.14 % (3688082)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3909241750:cond=on:i=156:bs=on:gtg=exists_all:er=known_2979 on theBenchmark for (2979ds/156Mi)
% 66.09/10.14 % (3688082)Instruction limit reached!
% 66.09/10.14 % (3688082)------------------------------
% 66.09/10.14 % (3688082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.09/10.14 % (3688082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.09/10.14 % (3688082)CaDiCaL version: 2.1.3
% 66.09/10.14 % (3688082)Termination reason: Instruction limit
% 66.09/10.14 % (3688082)Termination phase: Saturation
% 66.09/10.14 % (3688082)Time elapsed: 0.142 s
% 66.09/10.14 % (3688082)Peak memory usage: 88 MB
% 66.09/10.14 % (3688082)Instructions burned: 156 (million)
% 66.09/10.14 % (3688078)Instruction limit reached!
% 66.09/10.14 % (3688078)------------------------------
% 66.09/10.14 % (3688078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.09/10.14 % (3688078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.09/10.14 % (3688078)CaDiCaL version: 2.1.3
% 66.09/10.14 % (3688078)Termination reason: Instruction limit
% 66.09/10.14 % (3688078)Termination phase: Saturation
% 66.09/10.14 % (3688078)Time elapsed: 0.269 s
% 66.09/10.14 % (3688078)Peak memory usage: 92 MB
% 66.09/10.14 % (3688078)Instructions burned: 264 (million)
% 66.09/10.14 % (3688092)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=2994584219:i=3256:kws=precedence:bd=preordered:av=off_2974 on theBenchmark for (2974ds/3256Mi)
% 66.09/10.14 % (3688094)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1315802258:i=537:av=off:ss=included_2974 on theBenchmark for (2974ds/537Mi)
% 66.09/10.14 % (3688094)Instruction limit reached!
% 66.09/10.14 % (3688094)------------------------------
% 66.09/10.14 % (3688094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.09/10.14 % (3688094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.09/10.14 % (3688094)CaDiCaL version: 2.1.3
% 66.09/10.14 % (3688094)Termination reason: Instruction limit
% 66.09/10.14 % (3688094)Termination phase: Saturation
% 66.09/10.14 % (3688094)Time elapsed: 0.436 s
% 66.09/10.14 % (3688094)Peak memory usage: 92 MB
% 66.09/10.14 % (3688094)Instructions burned: 537 (million)
% 66.09/10.14 % (3688102)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1406094129:i=180:bd=preordered:av=off_2966 on theBenchmark for (2966ds/180Mi)
% 66.09/10.14 % (3688102)Instruction limit reached!
% 66.09/10.14 % (3688102)------------------------------
% 66.09/10.14 % (3688102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.09/10.14 % (3688102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.09/10.14 % (3688102)CaDiCaL version: 2.1.3
% 66.09/10.14 % (3688102)Termination reason: Instruction limit
% 66.09/10.14 % (3688102)Termination phase: Saturation
% 66.09/10.14 % (3688102)Time elapsed: 0.099 s
% 66.09/10.14 % (3688102)Peak memory usage: 88 MB
% 66.09/10.14 % (3688102)Instructions burned: 181 (million)
% 66.09/10.14 % (3688105)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=3285135801:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2964 on theBenchmark for (2964ds/10307Mi)
% 66.09/10.14 % (3688028)Instruction limit reached!
% 66.09/10.14 % (3688028)------------------------------
% 66.09/10.14 % (3688028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.09/10.14 % (3688028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.09/10.14 % (3688028)CaDiCaL version: 2.1.3
% 66.09/10.14 % (3688028)Termination reason: Instruction limit
% 66.09/10.14 % (3688028)Termination phase: Saturation
% 66.09/10.14 % (3688028)Time elapsed: 2.998 s
% 66.09/10.14 % (3688028)Peak memory usage: 149 MB
% 66.09/10.14 % (3688028)Instructions burned: 3394 (million)
% 66.09/10.14 % (3688146)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=2156243318:i=412:gtgl=4:gtg=exists_all_2962 on theBenchmark for (2962ds/412Mi)
% 66.09/10.14 % (3688146)Instruction limit reached!
% 66.09/10.14 % (3688146)------------------------------
% 66.09/10.14 % (3688146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.09/10.14 % (3688146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.53/13.46 % (3688146)CaDiCaL version: 2.1.3
% 88.53/13.46 % (3688146)Termination reason: Instruction limit
% 88.53/13.46 % (3688146)Termination phase: Saturation
% 88.53/13.46 % (3688146)Time elapsed: 0.240 s
% 88.53/13.46 % (3688146)Peak memory usage: 93 MB
% 88.53/13.46 % (3688146)Instructions burned: 413 (million)
% 88.53/13.46 % (3688200)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=532802810:s2pl=no:i=8478:s2at=4:nm=6_2958 on theBenchmark for (2958ds/8478Mi)
% 88.53/13.46 % (3688092)Instruction limit reached!
% 88.53/13.46 % (3688092)------------------------------
% 88.53/13.46 % (3688092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.53/13.46 % (3688092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.53/13.46 % (3688092)CaDiCaL version: 2.1.3
% 88.53/13.46 % (3688092)Termination reason: Instruction limit
% 88.53/13.46 % (3688092)Termination phase: Saturation
% 88.53/13.46 % (3688092)Time elapsed: 2.119 s
% 88.53/13.46 % (3688092)Peak memory usage: 151 MB
% 88.53/13.46 % (3688092)Instructions burned: 3258 (million)
% 88.53/13.46 % (3688040)Instruction limit reached!
% 88.53/13.46 % (3688040)------------------------------
% 88.53/13.46 % (3688040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.53/13.46 % (3688040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.53/13.46 % (3688040)CaDiCaL version: 2.1.3
% 88.53/13.46 % (3688040)Termination reason: Instruction limit
% 88.53/13.46 % (3688040)Termination phase: Saturation
% 88.53/13.46 % (3688040)Time elapsed: 3.898 s
% 88.53/13.46 % (3688040)Peak memory usage: 167 MB
% 88.53/13.46 % (3688040)Instructions burned: 5209 (million)
% 88.53/13.46 % (3688249)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=4151094762:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2951 on theBenchmark for (2951ds/303Mi)
% 88.53/13.46 % (3688249)Refutation not found, incomplete strategy
% 88.53/13.46 % (3688249)------------------------------
% 88.53/13.46 % (3688249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.53/13.46 % (3688249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.53/13.46 % (3688249)CaDiCaL version: 2.1.3
% 88.53/13.46 % (3688249)Termination reason: Refutation not found, incomplete strategy
% 88.53/13.46 % (3688249)Time elapsed: 0.002 s
% 88.53/13.46 % (3688249)Peak memory usage: 88 MB
% 88.53/13.46 % (3688249)Instructions burned: 1 (million)
% 88.53/13.46 % (3688257)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=638810821:st=4:i=720:sd=3:fsr=off:ss=axioms_2950 on theBenchmark for (2950ds/720Mi)
% 88.53/13.46 % (3688257)Refutation not found, incomplete strategy
% 88.53/13.46 % (3688257)------------------------------
% 88.53/13.46 % (3688257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.53/13.46 % (3688257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.53/13.46 % (3688257)CaDiCaL version: 2.1.3
% 88.53/13.46 % (3688257)Termination reason: Refutation not found, incomplete strategy
% 88.53/13.46 % (3688257)Time elapsed: 0.002 s
% 88.53/13.46 % (3688257)Peak memory usage: 88 MB
% 88.53/13.46 % (3688257)Instructions burned: 2 (million)
% 88.53/13.46 % (3688249)------------------------------
% 88.53/13.46 % (3688249)------------------------------
% 88.53/13.46 % (3688257)------------------------------
% 88.53/13.46 % (3688257)------------------------------
% 88.53/13.46 % (3688262)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3867458382:i=598:bs=on:bd=preordered:av=off:ss=axioms_2947 on theBenchmark for (2947ds/598Mi)
% 88.53/13.46 % (3688268)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1622452754:i=2989:sd=3:ss=axioms:sgt=60_2946 on theBenchmark for (2946ds/2989Mi)
% 88.53/13.46 % (3688262)Instruction limit reached!
% 88.53/13.46 % (3688262)------------------------------
% 88.53/13.46 % (3688262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 88.53/13.46 % (3688262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.53/13.46 % (3688262)CaDiCaL version: 2.1.3
% 88.53/13.46 % (3688262)Termination reason: Instruction limit
% 88.53/13.46 % (3688262)Termination phase: Saturation
% 88.53/13.46 % (3688262)Time elapsed: 0.327 s
% 88.53/13.46 % (3688262)Peak memory usage: 95 MB
% 88.53/13.46 % (3688262)Instructions burned: 598 (million)
% 132.57/19.61 % (3688271)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=309758814:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2942 on theBenchmark for (2942ds/1997Mi)
% 132.57/19.61 % (3688271)Instruction limit reached!
% 132.57/19.61 % (3688271)------------------------------
% 132.57/19.61 % (3688271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.57/19.61 % (3688271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.57/19.61 % (3688271)CaDiCaL version: 2.1.3
% 132.57/19.61 % (3688271)Termination reason: Instruction limit
% 132.57/19.61 % (3688271)Termination phase: Saturation
% 132.57/19.61 % (3688271)Time elapsed: 1.249 s
% 132.57/19.61 % (3688271)Peak memory usage: 137 MB
% 132.57/19.61 % (3688271)Instructions burned: 1999 (million)
% 132.57/19.61 % (3688273)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=2260677106:i=2088:bd=preordered:av=off_2928 on theBenchmark for (2928ds/2088Mi)
% 132.57/19.61 % (3688268)Instruction limit reached!
% 132.57/19.61 % (3688268)------------------------------
% 132.57/19.61 % (3688268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.57/19.61 % (3688268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.57/19.61 % (3688268)CaDiCaL version: 2.1.3
% 132.57/19.61 % (3688268)Termination reason: Instruction limit
% 132.57/19.61 % (3688268)Termination phase: Saturation
% 132.57/19.61 % (3688268)Time elapsed: 1.893 s
% 132.57/19.61 % (3688268)Peak memory usage: 146 MB
% 132.57/19.61 % (3688268)Instructions burned: 2989 (million)
% 132.57/19.61 % (3688275)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3764686235:i=1098:nicw=on_2925 on theBenchmark for (2925ds/1098Mi)
% 132.57/19.61 % (3688275)Instruction limit reached!
% 132.57/19.61 % (3688275)------------------------------
% 132.57/19.61 % (3688275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.57/19.61 % (3688275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.57/19.61 % (3688275)CaDiCaL version: 2.1.3
% 132.57/19.61 % (3688275)Termination reason: Instruction limit
% 132.57/19.61 % (3688275)Termination phase: Saturation
% 132.57/19.61 % (3688275)Time elapsed: 0.527 s
% 132.57/19.61 % (3688275)Peak memory usage: 100 MB
% 132.57/19.61 % (3688275)Instructions burned: 1099 (million)
% 132.57/19.61 % (3688277)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=48443693:i=433:bd=preordered_2918 on theBenchmark for (2918ds/433Mi)
% 132.57/19.61 % (3688277)Instruction limit reached!
% 132.57/19.61 % (3688277)------------------------------
% 132.57/19.61 % (3688277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.57/19.61 % (3688277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.57/19.61 % (3688277)CaDiCaL version: 2.1.3
% 132.57/19.61 % (3688277)Termination reason: Instruction limit
% 132.57/19.61 % (3688277)Termination phase: Saturation
% 132.57/19.61 % (3688277)Time elapsed: 0.250 s
% 132.57/19.61 % (3688277)Peak memory usage: 94 MB
% 132.57/19.61 % (3688277)Instructions burned: 434 (million)
% 132.57/19.61 % (3688273)Instruction limit reached!
% 132.57/19.61 % (3688273)------------------------------
% 132.57/19.61 % (3688273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 132.57/19.61 % (3688273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 132.57/19.61 % (3688273)CaDiCaL version: 2.1.3
% 132.57/19.61 % (3688273)Termination reason: Instruction limit
% 132.57/19.61 % (3688273)Termination phase: Saturation
% 132.57/19.61 % (3688273)Time elapsed: 1.292 s
% 132.57/19.61 % (3688273)Peak memory usage: 139 MB
% 132.57/19.61 % (3688273)Instructions burned: 2089 (million)
% 132.57/19.61 % (3688279)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3185370961:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2914 on theBenchmark for (2914ds/2942Mi)
% 132.57/19.61 % (3688280)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2300636232:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2913 on theBenchmark for (2913ds/6922Mi)
% 132.57/19.61 % (3688200)Instruction limit reached!
% 132.57/19.61 % (3688200)------------------------------
% 132.57/19.61 % (3688200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.89/22.58 % (3688200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.89/22.58 % (3688200)CaDiCaL version: 2.1.3
% 152.89/22.58 % (3688200)Termination reason: Instruction limit
% 152.89/22.58 % (3688200)Termination phase: Saturation
% 152.89/22.58 % (3688200)Time elapsed: 4.935 s
% 152.89/22.58 % (3688200)Peak memory usage: 204 MB
% 152.89/22.58 % (3688200)Instructions burned: 8480 (million)
% 152.89/22.58 % (3688283)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=2749398264:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2907 on theBenchmark for (2907ds/596Mi)
% 152.89/22.58 % (3688105)Instruction limit reached!
% 152.89/22.58 % (3688105)------------------------------
% 152.89/22.58 % (3688105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.89/22.58 % (3688105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.89/22.58 % (3688105)CaDiCaL version: 2.1.3
% 152.89/22.58 % (3688105)Termination reason: Instruction limit
% 152.89/22.58 % (3688105)Termination phase: Saturation
% 152.89/22.58 % (3688105)Time elapsed: 5.882 s
% 152.89/22.58 % (3688105)Peak memory usage: 173 MB
% 152.89/22.58 % (3688105)Instructions burned: 10307 (million)
% 152.89/22.58 % (3688283)Instruction limit reached!
% 152.89/22.58 % (3688283)------------------------------
% 152.89/22.58 % (3688283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.89/22.58 % (3688283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.89/22.58 % (3688283)CaDiCaL version: 2.1.3
% 152.89/22.58 % (3688283)Termination reason: Instruction limit
% 152.89/22.58 % (3688283)Termination phase: Saturation
% 152.89/22.58 % (3688283)Time elapsed: 0.330 s
% 152.89/22.58 % (3688283)Peak memory usage: 98 MB
% 152.89/22.58 % (3688283)Instructions burned: 598 (million)
% 152.89/22.58 % (3688285)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=3062239296:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2903 on theBenchmark for (2903ds/4123Mi)
% 152.89/22.58 % (3688287)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3505246954:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2902 on theBenchmark for (2902ds/16411Mi)
% 152.89/22.58 % (3688279)Instruction limit reached!
% 152.89/22.58 % (3688279)------------------------------
% 152.89/22.58 % (3688279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.89/22.58 % (3688279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.89/22.58 % (3688279)CaDiCaL version: 2.1.3
% 152.89/22.58 % (3688279)Termination reason: Instruction limit
% 152.89/22.58 % (3688279)Termination phase: Saturation
% 152.89/22.58 % (3688279)Time elapsed: 1.885 s
% 152.89/22.58 % (3688279)Peak memory usage: 138 MB
% 152.89/22.58 % (3688279)Instructions burned: 2942 (million)
% 152.89/22.58 % (3688289)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1819294656:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2894 on theBenchmark for (2894ds/1670Mi)
% 152.89/22.58 % (3688289)Instruction limit reached!
% 152.89/22.58 % (3688289)------------------------------
% 152.89/22.58 % (3688289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.89/22.58 % (3688289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.89/22.58 % (3688289)CaDiCaL version: 2.1.3
% 152.89/22.58 % (3688289)Termination reason: Instruction limit
% 152.89/22.58 % (3688289)Termination phase: Saturation
% 152.89/22.58 % (3688289)Time elapsed: 1.042 s
% 152.89/22.58 % (3688289)Peak memory usage: 136 MB
% 152.89/22.58 % (3688289)Instructions burned: 1670 (million)
% 152.89/22.58 % (3688291)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=3286035925:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2882 on theBenchmark for (2882ds/1722Mi)
% 152.89/22.58 % (3688280)Instruction limit reached!
% 152.89/22.58 % (3688280)------------------------------
% 152.89/22.58 % (3688280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 152.89/22.58 % (3688280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 152.89/22.58 % (3688280)CaDiCaL version: 2.1.3
% 152.89/22.58 % (3688280)Termination reason: Instruction limit
% 152.89/22.58 % (3688280)Termination phase: Saturation
% 152.89/22.58 % (3688280)Time elapsed: 3.801 s
% 152.89/22.58 % (3688280)Peak memory usage: 187 MB
% 152.89/22.58 % (3688280)Instructions burned: 6923 (million)
% 171.71/25.18 % (3688285)Instruction limit reached!
% 171.71/25.18 % (3688285)------------------------------
% 171.71/25.18 % (3688285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.71/25.18 % (3688285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.71/25.18 % (3688285)CaDiCaL version: 2.1.3
% 171.71/25.18 % (3688285)Termination reason: Instruction limit
% 171.71/25.18 % (3688285)Termination phase: Saturation
% 171.71/25.18 % (3688285)Time elapsed: 2.894 s
% 171.71/25.18 % (3688285)Peak memory usage: 159 MB
% 171.71/25.18 % (3688285)Instructions burned: 4123 (million)
% 171.71/25.18 % (3688443)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=1253751310:cts=off:cond=on:i=9530:bs=on:fsd=on_2873 on theBenchmark for (2873ds/9530Mi)
% 171.71/25.18 % (3688444)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1563202933:st=2:i=4495:sd=10:ss=included_2873 on theBenchmark for (2873ds/4495Mi)
% 171.71/25.18 % (3688291)Instruction limit reached!
% 171.71/25.18 % (3688291)------------------------------
% 171.71/25.18 % (3688291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.71/25.18 % (3688291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.71/25.18 % (3688291)CaDiCaL version: 2.1.3
% 171.71/25.18 % (3688291)Termination reason: Instruction limit
% 171.71/25.18 % (3688291)Termination phase: Saturation
% 171.71/25.18 % (3688291)Time elapsed: 1.170 s
% 171.71/25.18 % (3688291)Peak memory usage: 134 MB
% 171.71/25.18 % (3688291)Instructions burned: 1724 (million)
% 171.71/25.18 % (3688542)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=378186558:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2868 on theBenchmark for (2868ds/4920Mi)
% 171.71/25.18 % (3688444)Instruction limit reached!
% 171.71/25.18 % (3688444)------------------------------
% 171.71/25.18 % (3688444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.71/25.18 % (3688444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.71/25.18 % (3688444)CaDiCaL version: 2.1.3
% 171.71/25.18 % (3688444)Termination reason: Instruction limit
% 171.71/25.18 % (3688444)Termination phase: Saturation
% 171.71/25.18 % (3688444)Time elapsed: 3.825 s
% 171.71/25.18 % (3688444)Peak memory usage: 158 MB
% 171.71/25.18 % (3688444)Instructions burned: 4495 (million)
% 171.71/25.18 % (3688607)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=412107405:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2833 on theBenchmark for (2833ds/2083Mi)
% 171.71/25.18 % (3688542)Instruction limit reached!
% 171.71/25.18 % (3688542)------------------------------
% 171.71/25.18 % (3688542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.71/25.18 % (3688542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.71/25.18 % (3688542)CaDiCaL version: 2.1.3
% 171.71/25.18 % (3688542)Termination reason: Instruction limit
% 171.71/25.18 % (3688542)Termination phase: Saturation
% 171.71/25.18 % (3688542)Time elapsed: 4.277 s
% 171.71/25.18 % (3688542)Peak memory usage: 163 MB
% 171.71/25.18 % (3688542)Instructions burned: 4920 (million)
% 171.71/25.18 % (3688616)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=3472328892:i=4629:av=off:gsp=on_2824 on theBenchmark for (2824ds/4629Mi)
% 171.71/25.18 % (3688616)Refutation not found, incomplete strategy
% 171.71/25.18 % (3688616)------------------------------
% 171.71/25.18 % (3688616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.71/25.18 % (3688616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.71/25.18 % (3688616)CaDiCaL version: 2.1.3
% 171.71/25.18 % (3688616)Termination reason: Refutation not found, incomplete strategy
% 171.71/25.18 % (3688616)Time elapsed: 0.705 s
% 171.71/25.18 % (3688616)Peak memory usage: 127 MB
% 171.71/25.18 % (3688616)Instructions burned: 892 (million)
% 171.71/25.18 % (3688607)Instruction limit reached!
% 171.71/25.18 % (3688607)------------------------------
% 171.71/25.18 % (3688607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 171.71/25.18 % (3688607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 171.71/25.18 % (3688607)CaDiCaL version: 2.1.3
% 196.14/28.64 % (3688607)Termination reason: Instruction limit
% 196.14/28.64 % (3688607)Termination phase: Saturation
% 196.14/28.64 % (3688607)Time elapsed: 1.759 s
% 196.14/28.64 % (3688607)Peak memory usage: 135 MB
% 196.14/28.64 % (3688607)Instructions burned: 2083 (million)
% 196.14/28.64 % (3688616)------------------------------
% 196.14/28.64 % (3688616)------------------------------
% 196.14/28.64 % (3688659)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=3651262203:i=1258:av=off_2812 on theBenchmark for (2812ds/1258Mi)
% 196.14/28.64 % (3688660)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3686947353:i=7343:av=off:ss=included_2811 on theBenchmark for (2811ds/7343Mi)
% 196.14/28.64 % (3688659)Instruction limit reached!
% 196.14/28.64 % (3688659)------------------------------
% 196.14/28.64 % (3688659)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.14/28.64 % (3688659)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.14/28.64 % (3688659)CaDiCaL version: 2.1.3
% 196.14/28.64 % (3688659)Termination reason: Instruction limit
% 196.14/28.64 % (3688659)Termination phase: Saturation
% 196.14/28.64 % (3688659)Time elapsed: 0.730 s
% 196.14/28.64 % (3688659)Peak memory usage: 102 MB
% 196.14/28.64 % (3688659)Instructions burned: 1261 (million)
% 196.14/28.64 % (3688663)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=4134843060:i=1325:sd=2:ss=axioms:sgt=16_2803 on theBenchmark for (2803ds/1325Mi)
% 196.14/28.64 % (3688663)Refutation not found, incomplete strategy
% 196.14/28.64 % (3688663)------------------------------
% 196.14/28.64 % (3688663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.14/28.64 % (3688663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.14/28.64 % (3688663)CaDiCaL version: 2.1.3
% 196.14/28.64 % (3688663)Termination reason: Refutation not found, incomplete strategy
% 196.14/28.64 % (3688663)Time elapsed: 0.001 s
% 196.14/28.64 % (3688663)Peak memory usage: 87 MB
% 196.14/28.64 % (3688663)------------------------------
% 196.14/28.64 % (3688663)------------------------------
% 196.14/28.64 % (3688665)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=914186741:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2799 on theBenchmark for (2799ds/2646Mi)
% 196.14/28.64 % (3688443)Instruction limit reached!
% 196.14/28.64 % (3688443)------------------------------
% 196.14/28.64 % (3688443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.14/28.64 % (3688443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.14/28.64 % (3688443)CaDiCaL version: 2.1.3
% 196.14/28.64 % (3688443)Termination reason: Instruction limit
% 196.14/28.64 % (3688443)Termination phase: Saturation
% 196.14/28.64 % (3688443)Time elapsed: 7.606 s
% 196.14/28.64 % (3688443)Peak memory usage: 165 MB
% 196.14/28.64 % (3688443)Instructions burned: 9530 (million)
% 196.14/28.64 % (3688667)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=454144439:i=1489:sd=2:ep=R:ss=axioms_2796 on theBenchmark for (2796ds/1489Mi)
% 196.14/28.64 % (3688667)Refutation not found, incomplete strategy
% 196.14/28.64 % (3688667)------------------------------
% 196.14/28.64 % (3688667)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.14/28.64 % (3688667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.14/28.64 % (3688667)CaDiCaL version: 2.1.3
% 196.14/28.64 % (3688667)Termination reason: Refutation not found, incomplete strategy
% 196.14/28.64 % (3688667)Time elapsed: 0.591 s
% 196.14/28.64 % (3688667)Peak memory usage: 128 MB
% 196.14/28.64 % (3688667)Instructions burned: 892 (million)
% 196.14/28.64 % (3688667)------------------------------
% 196.14/28.64 % (3688667)------------------------------
% 196.14/28.64 % (3688735)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=1561839749:i=1503_2786 on theBenchmark for (2786ds/1503Mi)
% 196.14/28.64 % (3688287)Instruction limit reached!
% 196.14/28.64 % (3688287)------------------------------
% 196.14/28.64 % (3688287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 196.14/28.64 % (3688287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.14/28.64 % (3688287)CaDiCaL version: 2.1.3
% 196.14/28.64 % (3688287)Termination reason: Instruction limit
% 196.14/28.64 % (3688287)Termination phase: Saturation
% 196.14/28.64 % (3688287)Time elapsed: 11.778 s
% 242.09/35.06 % (3688287)Peak memory usage: 250 MB
% 242.09/35.06 % (3688287)Instructions burned: 16412 (million)
% 242.09/35.06 % (3688784)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3263094034:i=13942:kws=frequency_2782 on theBenchmark for (2782ds/13942Mi)
% 242.09/35.06 % (3688665)Instruction limit reached!
% 242.09/35.06 % (3688665)------------------------------
% 242.09/35.06 % (3688665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.09/35.06 % (3688665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.09/35.06 % (3688665)CaDiCaL version: 2.1.3
% 242.09/35.06 % (3688665)Termination reason: Instruction limit
% 242.09/35.06 % (3688665)Termination phase: Saturation
% 242.09/35.06 % (3688665)Time elapsed: 1.708 s
% 242.09/35.06 % (3688665)Peak memory usage: 138 MB
% 242.09/35.06 % (3688665)Instructions burned: 2646 (million)
% 242.09/35.06 % (3688786)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=3164731664:i=3604:fsr=off:er=filter_2780 on theBenchmark for (2780ds/3604Mi)
% 242.09/35.06 % (3688735)Refutation not found, incomplete strategy
% 242.09/35.06 % (3688735)------------------------------
% 242.09/35.06 % (3688735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.09/35.06 % (3688735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.09/35.06 % (3688735)CaDiCaL version: 2.1.3
% 242.09/35.06 % (3688735)Termination reason: Refutation not found, incomplete strategy
% 242.09/35.06 % (3688735)Time elapsed: 0.586 s
% 242.09/35.06 % (3688735)Peak memory usage: 128 MB
% 242.09/35.06 % (3688735)Instructions burned: 885 (million)
% 242.09/35.06 % (3688735)------------------------------
% 242.09/35.06 % (3688735)------------------------------
% 242.09/35.06 % (3688788)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=858937326:i=1876:sd=1:ss=included:sgt=32_2776 on theBenchmark for (2776ds/1876Mi)
% 242.09/35.06 % (3688788)Instruction limit reached!
% 242.09/35.06 % (3688788)------------------------------
% 242.09/35.06 % (3688788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.09/35.06 % (3688788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.09/35.06 % (3688788)CaDiCaL version: 2.1.3
% 242.09/35.06 % (3688788)Termination reason: Instruction limit
% 242.09/35.06 % (3688788)Termination phase: Saturation
% 242.09/35.06 % (3688788)Time elapsed: 1.149 s
% 242.09/35.06 % (3688788)Peak memory usage: 136 MB
% 242.09/35.06 % (3688788)Instructions burned: 1876 (million)
% 242.09/35.06 % (3688660)Instruction limit reached!
% 242.09/35.06 % (3688660)------------------------------
% 242.09/35.06 % (3688660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.09/35.06 % (3688660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.09/35.06 % (3688660)CaDiCaL version: 2.1.3
% 242.09/35.06 % (3688660)Termination reason: Instruction limit
% 242.09/35.06 % (3688660)Termination phase: Saturation
% 242.09/35.06 % (3688660)Time elapsed: 4.803 s
% 242.09/35.06 % (3688660)Peak memory usage: 185 MB
% 242.09/35.06 % (3688660)Instructions burned: 7343 (million)
% 242.09/35.06 % (3688790)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=835065936:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2762 on theBenchmark for (2762ds/1932Mi)
% 242.09/35.06 % (3688791)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=2541332157:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2761 on theBenchmark for (2761ds/1980Mi)
% 242.09/35.06 % (3688786)Instruction limit reached!
% 242.09/35.06 % (3688786)------------------------------
% 242.09/35.06 % (3688786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 242.09/35.06 % (3688786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 242.09/35.06 % (3688786)CaDiCaL version: 2.1.3
% 242.09/35.06 % (3688786)Termination reason: Instruction limit
% 242.09/35.06 % (3688786)Termination phase: Saturation
% 242.09/35.06 % (3688786)Time elapsed: 2.046 s
% 242.09/35.06 % (3688786)Peak memory usage: 154 MB
% 242.09/35.06 % (3688786)Instructions burned: 3605 (million)
% 242.09/35.06 % (3688794)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=4285259786:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2758 on theBenchmark for (2758ds/3902Mi)
% 137.30/36.19 % (3688794)Refutation not found, incomplete strategy
% 137.30/36.19 % (3688794)------------------------------
% 137.30/36.19 % (3688794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688794)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688794)Termination reason: Refutation not found, incomplete strategy
% 137.30/36.19 % (3688794)Time elapsed: 0.593 s
% 137.30/36.19 % (3688794)Peak memory usage: 127 MB
% 137.30/36.19 % (3688794)Instructions burned: 893 (million)
% 137.30/36.19 % (3688790)Instruction limit reached!
% 137.30/36.19 % (3688790)------------------------------
% 137.30/36.19 % (3688790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688790)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688790)Termination reason: Instruction limit
% 137.30/36.19 % (3688790)Termination phase: Saturation
% 137.30/36.19 % (3688790)Time elapsed: 1.171 s
% 137.30/36.19 % (3688790)Peak memory usage: 138 MB
% 137.30/36.19 % (3688790)Instructions burned: 1933 (million)
% 137.30/36.19 % (3688794)------------------------------
% 137.30/36.19 % (3688794)------------------------------
% 137.30/36.19 % (3688796)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2366723653:avsq=on:i=3916:aac=none:amm=off_2749 on theBenchmark for (2749ds/3916Mi)
% 137.30/36.19 % (3688791)Instruction limit reached!
% 137.30/36.19 % (3688791)------------------------------
% 137.30/36.19 % (3688791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688791)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688791)Termination reason: Instruction limit
% 137.30/36.19 % (3688791)Termination phase: Saturation
% 137.30/36.19 % (3688791)Time elapsed: 1.265 s
% 137.30/36.19 % (3688791)Peak memory usage: 137 MB
% 137.30/36.19 % (3688791)Instructions burned: 1980 (million)
% 137.30/36.19 % (3688797)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=1020832854:cond=on:i=3940:av=off:er=known_2748 on theBenchmark for (2748ds/3940Mi)
% 137.30/36.19 % (3688799)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=1809271172:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2747 on theBenchmark for (2747ds/3980Mi)
% 137.30/36.19 % (3688796)Instruction limit reached!
% 137.30/36.19 % (3688796)------------------------------
% 137.30/36.19 % (3688796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688796)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688796)Termination reason: Instruction limit
% 137.30/36.19 % (3688796)Termination phase: Saturation
% 137.30/36.19 % (3688796)Time elapsed: 2.313 s
% 137.30/36.19 % (3688796)Peak memory usage: 119 MB
% 137.30/36.19 % (3688796)Instructions burned: 3916 (million)
% 137.30/36.19 % (3688797)Instruction limit reached!
% 137.30/36.19 % (3688797)------------------------------
% 137.30/36.19 % (3688797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688797)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688797)Termination reason: Instruction limit
% 137.30/36.19 % (3688797)Termination phase: Saturation
% 137.30/36.19 % (3688797)Time elapsed: 2.332 s
% 137.30/36.19 % (3688797)Peak memory usage: 155 MB
% 137.30/36.19 % (3688797)Instructions burned: 3942 (million)
% 137.30/36.19 % (3688952)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=962167229:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2724 on theBenchmark for (2724ds/2087Mi)
% 137.30/36.19 % (3688799)Instruction limit reached!
% 137.30/36.19 % (3688799)------------------------------
% 137.30/36.19 % (3688799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688799)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688799)Termination reason: Instruction limit
% 137.30/36.19 % (3688799)Termination phase: Saturation
% 137.30/36.19 % (3688799)Time elapsed: 2.371 s
% 137.30/36.19 % (3688799)Peak memory usage: 153 MB
% 137.30/36.19 % (3688799)Instructions burned: 3980 (million)
% 137.30/36.19 % (3688953)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=3832150228:cts=off:cond=on:i=4272:bs=on:fsd=on_2723 on theBenchmark for (2723ds/4272Mi)
% 137.30/36.19 % (3688956)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=4071353353:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2722 on theBenchmark for (2722ds/2197Mi)
% 137.30/36.19 % (3688952)Instruction limit reached!
% 137.30/36.19 % (3688952)------------------------------
% 137.30/36.19 % (3688952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688952)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688952)Termination reason: Instruction limit
% 137.30/36.19 % (3688952)Termination phase: Saturation
% 137.30/36.19 % (3688952)Time elapsed: 1.355 s
% 137.30/36.19 % (3688952)Peak memory usage: 141 MB
% 137.30/36.19 % (3688952)Instructions burned: 2088 (million)
% 137.30/36.19 % (3689080)dis+21_1_sil=8000:spb=goal_then_units:random_seed=1910895714:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2709 on theBenchmark for (2709ds/6508Mi)
% 137.30/36.19 % (3688956)Instruction limit reached!
% 137.30/36.19 % (3688956)------------------------------
% 137.30/36.19 % (3688956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688956)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688956)Termination reason: Instruction limit
% 137.30/36.19 % (3688956)Termination phase: Saturation
% 137.30/36.19 % (3688956)Time elapsed: 1.744 s
% 137.30/36.19 % (3688956)Peak memory usage: 140 MB
% 137.30/36.19 % (3688956)Instructions burned: 2198 (million)
% 137.30/36.19 % (3689096)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=933412689:i=2330:fgj=on:av=off:fsr=off_2702 on theBenchmark for (2702ds/2330Mi)
% 137.30/36.19 % (3688953)Instruction limit reached!
% 137.30/36.19 % (3688953)------------------------------
% 137.30/36.19 % (3688953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688953)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688953)Termination reason: Instruction limit
% 137.30/36.19 % (3688953)Termination phase: Saturation
% 137.30/36.19 % (3688953)Time elapsed: 3.709 s
% 137.30/36.19 % (3688953)Peak memory usage: 151 MB
% 137.30/36.19 % (3688953)Instructions burned: 4272 (million)
% 137.30/36.19 % (3688784)Instruction limit reached!
% 137.30/36.19 % (3688784)------------------------------
% 137.30/36.19 % (3688784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3688784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3688784)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3688784)Termination reason: Instruction limit
% 137.30/36.19 % (3688784)Termination phase: Saturation
% 137.30/36.19 % (3688784)Time elapsed: 9.720 s
% 137.30/36.19 % (3688784)Peak memory usage: 238 MB
% 137.30/36.19 % (3688784)Instructions burned: 13942 (million)
% 137.30/36.19 % (3689122)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=2822285417:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2684 on theBenchmark for (2684ds/7592Mi)
% 137.30/36.19 % (3689124)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=2911280633:i=2693:kws=precedence:ins=1:av=off_2683 on theBenchmark for (2683ds/2693Mi)
% 137.30/36.19 % (3689096)Instruction limit reached!
% 137.30/36.19 % (3689096)------------------------------
% 137.30/36.19 % (3689096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3689096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3689096)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3689096)Termination reason: Instruction limit
% 137.30/36.19 % (3689096)Termination phase: Saturation
% 137.30/36.19 % (3689096)Time elapsed: 2.267 s
% 137.30/36.19 % (3689096)Peak memory usage: 140 MB
% 137.30/36.19 % (3689096)Instructions burned: 2331 (million)
% 137.30/36.19 % (3689130)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=3541974728:i=28651:sd=4:ss=included:sgt=64_2677 on theBenchmark for (2677ds/28651Mi)
% 137.30/36.19 % (3689124)Instruction limit reached!
% 137.30/36.19 % (3689124)------------------------------
% 137.30/36.19 % (3689124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3689124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3689124)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3689124)Termination reason: Instruction limit
% 137.30/36.19 % (3689124)Termination phase: Saturation
% 137.30/36.19 % (3689124)Time elapsed: 2.248 s
% 137.30/36.19 % (3689124)Peak memory usage: 144 MB
% 137.30/36.19 % (3689124)Instructions burned: 2694 (million)
% 137.30/36.19 % (3689178)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=4284242899:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2657 on theBenchmark for (2657ds/2700Mi)
% 137.30/36.19 % (3689080)Instruction limit reached!
% 137.30/36.19 % (3689080)------------------------------
% 137.30/36.19 % (3689080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 137.30/36.19 % (3689080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.30/36.19 % (3689080)CaDiCaL version: 2.1.3
% 137.30/36.19 % (3689080)Termination reason: Instruction limit
% 137.30/36.19 % (3689080)Termination phase: Saturation
% 137.30/36.19 % (3689080)Time elapsed: 5.413 s
% 137.30/36.19 % (3689080)Peak memory usage: 137 MB
% 137.30/36.19 % (3689080)Instructions burned: 6508 (million)
% 137.30/36.19 % (3689130)First to succeed.
% 137.30/36.19 % (3689130)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3687889"
% 137.30/36.19 % (3689180)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=1021244851:i=3196:nm=4_2652 on theBenchmark for (2652ds/3196Mi)
% 137.30/36.19 % (3689130)Refutation found. Thanks to Tanya!
% 137.30/36.19 % SZS status Unsatisfiable for theBenchmark
% 137.30/36.19 % SZS output start Proof for theBenchmark
% See solution above
% 249.62/36.38 % (3689130)------------------------------
% 249.62/36.38 % (3689130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 249.62/36.38 % (3689130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 249.62/36.38 % (3689130)CaDiCaL version: 2.1.3
% 249.62/36.38 % (3689130)Termination reason: Refutation
% 249.62/36.38 % (3689130)Time elapsed: 2.375 s
% 249.62/36.38 % (3689130)Peak memory usage: 151 MB
% 249.62/36.38 % (3689130)Instructions burned: 3477 (million)
% 249.62/36.38 % (3689130)------------------------------
% 249.62/36.38 % (3689130)------------------------------
% 249.62/36.38 % (3687889)Success in time 35.331 s
% 249.62/36.38 % Vampire exiting
%------------------------------------------------------------------------------