%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL424-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:52:22 AM UTC 2026
% Result : Unsatisfiable 155.90s 40.20s
% Output : Refutation 276.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 13
% Syntax : Number of formulae : 179 ( 34 unt; 10 def)
% Number of atoms : 556 ( 0 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 736 ( 359 ~; 367 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 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 : 389 ( 0 sgn 389 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',mer21) ).
fof(f3,negated_conjecture,
( ~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c))))
| ~ is_a_theorem(implies(implies(not(a),a),a))
| ~ is_a_theorem(implies(a,implies(not(a),b))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_luka_3_basis) ).
fof(f5,definition,
( spl0_1
<=> is_a_theorem(implies(a,implies(not(a),b))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f7,plain,
( ~ is_a_theorem(implies(a,implies(not(a),b)))
| spl0_1 ),
inference(avatar_component_clause,[],[f5]) ).
fof(f9,definition,
( spl0_2
<=> is_a_theorem(implies(implies(not(a),a),a)) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f11,plain,
( ~ is_a_theorem(implies(implies(not(a),a),a))
| spl0_2 ),
inference(avatar_component_clause,[],[f9]) ).
fof(f13,definition,
( spl0_3
<=> is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f15,plain,
( ~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c))))
| spl0_3 ),
inference(avatar_component_clause,[],[f13]) ).
fof(f16,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f3,f13,f9,f5]) ).
fof(f17,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(f18,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,[],[f17,f2]) ).
fof(f19,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(not(X1),X2)),X3),implies(X1,X3))),
inference(resolution,[],[f18,f17]) ).
fof(f21,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))),
inference(resolution,[],[f19,f17]) ).
fof(f23,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),not(X1)),implies(X2,not(X1)))),
inference(resolution,[],[f21,f17]) ).
fof(f24,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X0),X1))
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f21,f1]) ).
fof(f29,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X2)))),
inference(resolution,[],[f24,f21]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,X2))) ),
inference(resolution,[],[f29,f1]) ).
fof(f45,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(X1,X1)),X2),implies(X3,X2))),
inference(resolution,[],[f29,f17]) ).
fof(f49,definition,
( spl0_4
<=> ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f50,plain,
( ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X2)))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f52,definition,
( spl0_5
<=> ! [X0] : ~ is_a_theorem(X0) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f53,plain,
( ! [X0] : ~ is_a_theorem(X0)
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f52]) ).
fof(f54,plain,
( spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f43,f52,f49]) ).
fof(f56,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),
inference(resolution,[],[f45,f17]) ).
fof(f61,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(not(X0),not(X1)),X0),X2),implies(X1,X2))),
inference(resolution,[],[f56,f17]) ).
fof(f64,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f56,f1]) ).
fof(f66,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,[],[f61,f17]) ).
fof(f69,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(not(X0),not(X1)),X0),X2))
| is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f61,f1]) ).
fof(f71,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
inference(resolution,[],[f69,f21]) ).
fof(f72,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,not(not(X0))))),
inference(resolution,[],[f69,f23]) ).
fof(f73,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))),
inference(resolution,[],[f69,f56]) ).
fof(f76,plain,
! [X0,X1] :
( is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f71,f1]) ).
fof(f85,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(implies(X1,X1)),X2))),
inference(resolution,[],[f73,f24]) ).
fof(f87,plain,
( $false
| spl0_1 ),
inference(resolution,[],[f73,f7]) ).
fof(f88,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f87]) ).
fof(f89,plain,
( ! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,X1)) )
| ~ spl0_4 ),
inference(resolution,[],[f50,f1]) ).
fof(f96,definition,
( spl0_6
<=> ! [X1] : is_a_theorem(implies(X1,X1)) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f97,plain,
( ! [X1] : is_a_theorem(implies(X1,X1))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f98,plain,
( spl0_6
| spl0_5
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f89,f49,f52,f96]) ).
fof(f99,plain,
( $false
| ~ spl0_5 ),
inference(resolution,[],[f53,f2]) ).
fof(f125,plain,
~ spl0_5,
inference(avatar_contradiction_clause,[],[f99]) ).
fof(f127,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_6 ),
inference(resolution,[],[f97,f17]) ).
fof(f154,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f76,f17]) ).
fof(f161,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,[],[f154,f17]) ).
fof(f165,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f154,f1]) ).
fof(f213,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(implies(X0,X1),implies(not(X2),not(X3))),X2),X0))
| is_a_theorem(implies(X3,X0)) )
| ~ spl0_6 ),
inference(resolution,[],[f127,f1]) ).
fof(f283,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,[],[f161,f56]) ).
fof(f290,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X3,X2)))
| ~ is_a_theorem(implies(not(X1),not(X3))) ),
inference(resolution,[],[f161,f76]) ).
fof(f292,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))) ),
inference(resolution,[],[f290,f17]) ).
fof(f300,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(not(X0),not(X1)))
| ~ is_a_theorem(implies(implies(X2,X0),X3))
| is_a_theorem(implies(X1,X3)) ),
inference(resolution,[],[f290,f1]) ).
fof(f316,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,[],[f283,f1]) ).
fof(f343,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,[],[f66,f161]) ).
fof(f354,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,[],[f343,f1]) ).
fof(f355,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,[],[f354,f2]) ).
fof(f384,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(not(X0),not(not(X0))),implies(X1,X0)))
| ~ spl0_6 ),
inference(resolution,[],[f354,f97]) ).
fof(f390,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,[],[f355,f1]) ).
fof(f393,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),not(not(X2))),implies(X2,not(not(X2)))))
| ~ spl0_6 ),
inference(resolution,[],[f384,f161]) ).
fof(f400,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(implies(X1,X2)),not(X2)))),
inference(resolution,[],[f316,f73]) ).
fof(f812,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(implies(X2,X3)),X2))),
inference(resolution,[],[f72,f161]) ).
fof(f950,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(implies(X1,X2)),X1))),
inference(resolution,[],[f812,f69]) ).
fof(f966,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(not(implies(X1,X2)),X1)) ),
inference(resolution,[],[f950,f1]) ).
fof(f988,definition,
( spl0_10
<=> ! [X2,X1] : is_a_theorem(implies(not(implies(X1,X2)),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f989,plain,
( ! [X2,X1] : is_a_theorem(implies(not(implies(X1,X2)),X1))
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f988]) ).
fof(f990,plain,
( spl0_10
| spl0_5 ),
inference(avatar_split_clause,[],[f966,f52,f988]) ).
fof(f991,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(not(not(X0)),X1)))
| ~ spl0_10 ),
inference(resolution,[],[f989,f390]) ).
fof(f1013,plain,
( ! [X0,X1] :
( is_a_theorem(implies(not(not(X0)),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_10 ),
inference(resolution,[],[f991,f1]) ).
fof(f1019,plain,
( ! [X0,X1] :
( ~ is_a_theorem(not(not(X0)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1) )
| ~ spl0_10 ),
inference(resolution,[],[f1013,f1]) ).
fof(f1056,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(not(implies(X1,X1)),X2)) ),
inference(resolution,[],[f85,f1]) ).
fof(f1079,definition,
( spl0_11
<=> ! [X2,X1] : is_a_theorem(implies(not(implies(X1,X1)),X2)) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f1080,plain,
( ! [X2,X1] : is_a_theorem(implies(not(implies(X1,X1)),X2))
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f1079]) ).
fof(f1081,plain,
( spl0_11
| spl0_5 ),
inference(avatar_split_clause,[],[f1056,f52,f1079]) ).
fof(f1709,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(not(implies(X1,X2)),not(X2))) ),
inference(resolution,[],[f400,f1]) ).
fof(f1738,definition,
( spl0_14
<=> ! [X2,X1] : is_a_theorem(implies(not(implies(X1,X2)),not(X2))) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f1739,plain,
( ! [X2,X1] : is_a_theorem(implies(not(implies(X1,X2)),not(X2)))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f1738]) ).
fof(f1740,plain,
( spl0_14
| spl0_5 ),
inference(avatar_split_clause,[],[f1709,f52,f1738]) ).
fof(f1741,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,not(X0)),implies(X1,not(X0))))
| ~ spl0_14 ),
inference(resolution,[],[f1739,f390]) ).
fof(f1759,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,not(X0)))
| is_a_theorem(implies(X1,not(X0))) )
| ~ spl0_14 ),
inference(resolution,[],[f1741,f1]) ).
fof(f1762,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,not(not(implies(X1,X1)))))
| ~ spl0_11
| ~ spl0_14 ),
inference(resolution,[],[f1759,f1080]) ).
fof(f1767,plain,
( ! [X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(not(not(implies(X1,X1)))) )
| ~ spl0_11
| ~ spl0_14 ),
inference(resolution,[],[f1762,f1]) ).
fof(f1797,definition,
( spl0_15
<=> ! [X1] : is_a_theorem(not(not(implies(X1,X1)))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f1798,plain,
( ! [X1] : is_a_theorem(not(not(implies(X1,X1))))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f1797]) ).
fof(f1799,plain,
( spl0_15
| spl0_5
| ~ spl0_11
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f1767,f1738,f1079,f52,f1797]) ).
fof(f2079,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X0),X1))
| is_a_theorem(X1) )
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f1798,f1019]) ).
fof(f2617,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(X1,not(not(X1)))))
| ~ spl0_6 ),
inference(resolution,[],[f393,f69]) ).
fof(f2618,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,not(not(X0))),X1),implies(X2,X1)))
| ~ spl0_6 ),
inference(resolution,[],[f393,f17]) ).
fof(f2631,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(not(X1)),X2)))
| ~ spl0_6 ),
inference(resolution,[],[f2617,f161]) ).
fof(f2634,plain,
( ! [X0] : is_a_theorem(implies(X0,not(not(X0))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f2617,f2079]) ).
fof(f2670,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,not(not(implies(X1,X0)))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f2634,f64]) ).
fof(f2689,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(not(not(X1)),X2)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f2634,f300]) ).
fof(f2731,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,not(X1)),implies(X2,X1)),implies(X3,implies(X2,X1))))
| ~ spl0_6 ),
inference(resolution,[],[f2631,f161]) ).
fof(f2814,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,not(not(X0))),X1))
| is_a_theorem(implies(X2,X1)) )
| ~ spl0_6 ),
inference(resolution,[],[f2618,f1]) ).
fof(f2981,plain,
( ! [X0,X1] : is_a_theorem(implies(not(not(X0)),not(not(implies(X1,X0)))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f2689,f2634]) ).
fof(f3424,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_6 ),
inference(resolution,[],[f2731,f1]) ).
fof(f3426,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(implies(X1,not(X2))),X2)))
| ~ spl0_6 ),
inference(resolution,[],[f3424,f73]) ).
fof(f4713,plain,
( ! [X0,X1] : is_a_theorem(implies(not(implies(X0,not(X1))),X1))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f3426,f2079]) ).
fof(f4752,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4713,f292]) ).
fof(f4776,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(not(X1),not(not(implies(X1,X2))))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4752,f2814]) ).
fof(f4798,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(not(X0),X2)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4752,f1]) ).
fof(f4954,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(not(X0),not(not(implies(X1,implies(X0,X2))))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4798,f2670]) ).
fof(f4955,plain,
( ! [X0,X1] : is_a_theorem(implies(not(X0),not(not(implies(X0,X1)))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4798,f2634]) ).
fof(f4964,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),X2),X1),implies(X0,X1)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4955,f390]) ).
fof(f4975,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,X0)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4964,f17]) ).
fof(f5099,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(implies(X2,implies(X3,X0))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4975,f165]) ).
fof(f5100,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(implies(X2,X0)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f4975,f1]) ).
fof(f5111,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(not(X2),not(X1)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5100,f290]) ).
fof(f5188,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(X0,implies(X1,not(X2))))
| ~ is_a_theorem(implies(X2,not(X1))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5111,f1013]) ).
fof(f5223,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(X1,implies(X2,X3))))
| ~ is_a_theorem(implies(not(X3),not(X2))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5099,f290]) ).
fof(f5331,plain,
( ! [X2,X3,X0,X1,X4] :
( is_a_theorem(implies(implies(implies(X2,implies(X1,X0)),X3),implies(X4,X3)))
| ~ is_a_theorem(implies(not(X0),not(X1))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5223,f17]) ).
fof(f5396,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X2,implies(X1,X0)),X3))
| ~ is_a_theorem(implies(not(X0),not(X1)))
| is_a_theorem(implies(X4,X3)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5331,f1]) ).
fof(f5537,plain,
( ! [X2,X3,X0,X1,X4] :
( is_a_theorem(implies(X2,implies(implies(implies(X1,X0),X3),implies(X4,X3))))
| ~ is_a_theorem(implies(not(X0),not(X1))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5396,f2]) ).
fof(f5648,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X1,X0),X2),implies(X3,X2)))
| ~ is_a_theorem(implies(not(X0),not(X1))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5537,f2079]) ).
fof(f5735,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(not(X0),not(X1)))
| ~ is_a_theorem(implies(implies(X1,X0),X2))
| is_a_theorem(implies(X3,X2)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5648,f1]) ).
fof(f5747,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,not(X1)),X2))
| is_a_theorem(implies(X3,X2))
| ~ is_a_theorem(implies(X1,not(X0))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5735,f1013]) ).
fof(f7626,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,not(X1)))
| is_a_theorem(implies(X1,not(X0))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5188,f2079]) ).
fof(f16358,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X3,X2))))
| ~ is_a_theorem(implies(not(X1),not(not(implies(X3,X2))))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f5747,f355]) ).
fof(f16481,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_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f16358,f2079]) ).
fof(f16573,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(not(X0),X0),implies(X1,X0)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f16481,f2981]) ).
fof(f16575,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X2,implies(X0,X1))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f16481,f4954]) ).
fof(f16643,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X2,implies(X0,X1))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f16575,f1]) ).
fof(f16699,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,not(X1)),not(X1))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f16643,f1741]) ).
fof(f16701,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,implies(X1,X2)),implies(X1,X2))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f16643,f16575]) ).
fof(f17269,plain,
( ! [X0] : is_a_theorem(implies(implies(X0,not(X0)),not(X0)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f16699,f2079]) ).
fof(f17377,plain,
( ! [X0] : is_a_theorem(implies(X0,not(implies(X0,not(X0)))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f17269,f7626]) ).
fof(f17820,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f16701,f2079]) ).
fof(f17951,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f17820,f1]) ).
fof(f18007,plain,
( ! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X1))
| ~ is_a_theorem(X0) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f17951,f154]) ).
fof(f18188,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(not(X0),not(X2))))
| is_a_theorem(implies(X2,X0)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18007,f213]) ).
fof(f18206,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_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18007,f17]) ).
fof(f18614,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(not(X0),implies(X1,X0)),implies(X2,implies(X1,X0))))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18206,f2631]) ).
fof(f18673,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(not(implies(X0,X2)),X1)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18206,f4776]) ).
fof(f18705,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| ~ is_a_theorem(implies(not(X0),not(X2))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18206,f76]) ).
fof(f18788,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(not(implies(X0,X2)),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18673,f1]) ).
fof(f18887,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_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18705,f1]) ).
fof(f19033,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(not(X0),implies(X1,X0)),implies(X1,X0)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18614,f17951]) ).
fof(f19564,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),implies(X1,X0)))
| is_a_theorem(implies(X1,X0)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f19033,f1]) ).
fof(f20452,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X0,X2))))
| is_a_theorem(implies(X1,implies(X0,X2))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f18788,f19564]) ).
fof(f21014,plain,
( ! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(resolution,[],[f16573,f17951]) ).
fof(f25255,plain,
( ! [X0,X1] :
( is_a_theorem(implies(implies(not(X0),not(not(X0))),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f17377,f18887]) ).
fof(f25375,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_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f25255,f18206]) ).
fof(f25409,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_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f25375,f18206]) ).
fof(f25412,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(not(X1),not(not(X1)))))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f25375,f18188]) ).
fof(f26546,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X2,implies(X3,X3)),not(not(X0))),X1)))
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f25409,f45]) ).
fof(f26946,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_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f26546,f1]) ).
fof(f27393,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,X2),implies(not(not(X0)),X2)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f26946,f17]) ).
fof(f27483,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(not(X1),implies(not(not(X0)),X2)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f27393,f4798]) ).
fof(f29655,plain,
( ! [X0,X1] :
( is_a_theorem(implies(not(X1),not(X0)))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f27483,f25412]) ).
fof(f29678,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X0,X2)) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f29655,f18887]) ).
fof(f29889,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_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f29678,f2]) ).
fof(f33457,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X3,X2))))
| ~ is_a_theorem(X0) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f29889,f154]) ).
fof(f36182,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,X2),implies(implies(X0,X1),X2)))
| ~ is_a_theorem(X0) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f33457,f20452]) ).
fof(f52226,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(not(X2),not(X3))))
| is_a_theorem(implies(implies(X2,X4),implies(implies(X4,X0),implies(X3,X0)))) )
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f36182,f29889]) ).
fof(f54413,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ spl0_4
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f52226,f50]) ).
fof(f54538,plain,
( $false
| spl0_3
| ~ spl0_4
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(resolution,[],[f54413,f15]) ).
fof(f54565,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f54538]) ).
fof(f54566,plain,
( $false
| spl0_2
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f11,f21014]) ).
fof(f54567,plain,
( spl0_2
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(avatar_contradiction_clause,[],[f54566]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f16]) ).
cnf(s2,plain,
( spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f54]) ).
cnf(s3,plain,
spl0_1,
inference(sat_conversion,[],[f88]) ).
cnf(s4,plain,
( ~ spl0_4
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f98]) ).
cnf(s17,plain,
~ spl0_5,
inference(sat_conversion,[],[f125]) ).
cnf(s21,plain,
( spl0_5
| spl0_10 ),
inference(sat_conversion,[],[f990]) ).
cnf(s22,plain,
( spl0_5
| spl0_11 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s25,plain,
( spl0_5
| spl0_14 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s26,plain,
( spl0_5
| ~ spl0_11
| ~ spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f1799]) ).
cnf(s269,plain,
( spl0_3
| ~ spl0_4
| ~ spl0_6
| ~ spl0_10
| ~ spl0_14
| ~ spl0_15 ),
inference(sat_conversion,[],[f54565]) ).
cnf(s270,plain,
( spl0_2
| ~ spl0_6
| ~ spl0_10
| ~ spl0_15 ),
inference(sat_conversion,[],[f54567]) ).
cnf(s271,plain,
spl0_14,
inference(rat,[],[s25,s17]) ).
cnf(s272,plain,
spl0_11,
inference(rat,[],[s22,s17]) ).
cnf(s273,plain,
spl0_10,
inference(rat,[],[s21,s17]) ).
cnf(s274,plain,
spl0_15,
inference(rat,[],[s26,s271,s17,s272]) ).
cnf(s275,plain,
( ~ spl0_4
| spl0_6 ),
inference(rat,[],[s4,s17]) ).
cnf(s276,plain,
spl0_4,
inference(rat,[],[s2,s17]) ).
cnf(s277,plain,
spl0_6,
inference(rat,[],[s275,s276]) ).
cnf(s278,plain,
spl0_2,
inference(rat,[],[s270,s274,s273,s277]) ).
cnf(s297,plain,
spl0_3,
inference(rat,[],[s269,s274,s271,s273,s276,s277]) ).
cnf(s298,plain,
$false,
inference(rat,[],[s1,s297,s278,s3]) ).
fof(f54568,plain,
$false,
inference(avatar_sat_refutation,[],[s298]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL424-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.20/0.47 % Computer : n019.cluster.edu
% 0.20/0.47 % Model : x86_64 x86_64
% 0.20/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.47 % Memory : 8046.5625MB
% 0.20/0.47 % OS : Linux 6.8.0-71-generic
% 0.20/0.47 % CPULimit : 300
% 0.20/0.47 % WCLimit : 300
% 0.20/0.47 % DateTime : Sun Sep 27 15:42:18 UTC 2026
% 0.20/0.47 % CPUTime :
% 0.20/0.47 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.26/0.53 Running first-order theorem proving
% 0.26/0.53 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
% 19.54/3.99 % (3227033)Input is clausal, will run a generic CNF schedule.
% 19.54/3.99 % (3227042)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=689821726:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 19.54/3.99 % (3227042)Instruction limit reached!
% 19.54/3.99 % (3227042)------------------------------
% 19.54/3.99 % (3227042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.99 % (3227042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.99 % (3227042)CaDiCaL version: 2.1.3
% 19.54/3.99 % (3227042)Termination reason: Instruction limit
% 19.54/3.99 % (3227042)Termination phase: Saturation
% 19.54/3.99 % (3227042)Time elapsed: 0.058 s
% 19.54/3.99 % (3227042)Peak memory usage: 88 MB
% 19.54/3.99 % (3227042)Instructions burned: 114 (million)
% 19.54/3.99 % (3227041)lrs+10_1_sil=8000:sp=occurrence:random_seed=1020410100:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 19.54/3.99 % (3227040)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=933772667:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 19.54/3.99 % (3227039)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=677087092:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 19.54/3.99 % (3227038)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=2665396486:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 19.54/3.99 % (3227044)dis-21_1_sil=8000:lcm=predicate:random_seed=1401061900: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)
% 19.54/3.99 % (3227043)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3365184982:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 19.54/3.99 % (3227041)Instruction limit reached!
% 19.54/3.99 % (3227041)------------------------------
% 19.54/3.99 % (3227041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.99 % (3227041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.99 % (3227041)CaDiCaL version: 2.1.3
% 19.54/3.99 % (3227041)Termination reason: Instruction limit
% 19.54/3.99 % (3227041)Termination phase: Saturation
% 19.54/3.99 % (3227041)Time elapsed: 0.104 s
% 19.54/3.99 % (3227041)Peak memory usage: 89 MB
% 19.54/3.99 % (3227041)Instructions burned: 108 (million)
% 19.54/3.99 % (3227044)Instruction limit reached!
% 19.54/3.99 % (3227044)------------------------------
% 19.54/3.99 % (3227044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.99 % (3227044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.99 % (3227044)CaDiCaL version: 2.1.3
% 19.54/3.99 % (3227044)Termination reason: Instruction limit
% 19.54/3.99 % (3227044)Termination phase: Saturation
% 19.54/3.99 % (3227044)Time elapsed: 0.112 s
% 19.54/3.99 % (3227044)Peak memory usage: 88 MB
% 19.54/3.99 % (3227044)Instructions burned: 117 (million)
% 19.54/3.99 % (3227043)Instruction limit reached!
% 19.54/3.99 % (3227043)------------------------------
% 19.54/3.99 % (3227043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.99 % (3227043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.99 % (3227043)CaDiCaL version: 2.1.3
% 19.54/3.99 % (3227043)Termination reason: Instruction limit
% 19.54/3.99 % (3227043)Termination phase: Saturation
% 19.54/3.99 % (3227043)Time elapsed: 0.172 s
% 19.54/3.99 % (3227043)Peak memory usage: 89 MB
% 19.54/3.99 % (3227043)Instructions burned: 180 (million)
% 19.54/3.99 % (3227046)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=764637732:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 19.54/3.99 % (3227046)Refutation not found, incomplete strategy
% 19.54/3.99 % (3227046)------------------------------
% 19.54/3.99 % (3227046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.54/3.99 % (3227046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.54/3.99 % (3227046)CaDiCaL version: 2.1.3
% 19.54/3.99 % (3227046)Termination reason: Refutation not found, incomplete strategy
% 19.54/3.99 % (3227046)Time elapsed: 0.001 s
% 19.54/3.99 % (3227046)Peak memory usage: 88 MB
% 19.54/3.99 % (3227053)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=470472638:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 32.53/5.83 % (3227054)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2145071323:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 32.53/5.83 % (3227054)Refutation not found, incomplete strategy
% 32.53/5.83 % (3227054)------------------------------
% 32.53/5.83 % (3227054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.53/5.83 % (3227054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.83 % (3227054)CaDiCaL version: 2.1.3
% 32.53/5.83 % (3227054)Termination reason: Refutation not found, incomplete strategy
% 32.53/5.83 % (3227054)Time elapsed: 0.001 s
% 32.53/5.83 % (3227054)Peak memory usage: 87 MB
% 32.53/5.83 % (3227046)------------------------------
% 32.53/5.83 % (3227046)------------------------------
% 32.53/5.83 % (3227055)lrs+10_64_to=lpo:sil=8000:random_seed=3309609792:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 32.53/5.83 % (3227053)Instruction limit reached!
% 32.53/5.83 % (3227053)------------------------------
% 32.53/5.83 % (3227053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.53/5.83 % (3227053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.83 % (3227053)CaDiCaL version: 2.1.3
% 32.53/5.83 % (3227053)Termination reason: Instruction limit
% 32.53/5.83 % (3227053)Termination phase: Saturation
% 32.53/5.83 % (3227053)Time elapsed: 0.153 s
% 32.53/5.83 % (3227053)Peak memory usage: 88 MB
% 32.53/5.83 % (3227053)Instructions burned: 189 (million)
% 32.53/5.83 % (3227055)Instruction limit reached!
% 32.53/5.83 % (3227055)------------------------------
% 32.53/5.83 % (3227055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.53/5.83 % (3227055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.83 % (3227055)CaDiCaL version: 2.1.3
% 32.53/5.83 % (3227055)Termination reason: Instruction limit
% 32.53/5.83 % (3227055)Termination phase: Saturation
% 32.53/5.83 % (3227055)Time elapsed: 0.120 s
% 32.53/5.83 % (3227055)Peak memory usage: 89 MB
% 32.53/5.83 % (3227055)Instructions burned: 127 (million)
% 32.53/5.83 % (3227059)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3788894424:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 32.53/5.83 % (3227059)Instruction limit reached!
% 32.53/5.83 % (3227059)------------------------------
% 32.53/5.83 % (3227059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.53/5.83 % (3227059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.83 % (3227059)CaDiCaL version: 2.1.3
% 32.53/5.83 % (3227059)Termination reason: Instruction limit
% 32.53/5.83 % (3227059)Termination phase: Saturation
% 32.53/5.83 % (3227059)Time elapsed: 0.097 s
% 32.53/5.83 % (3227059)Peak memory usage: 90 MB
% 32.53/5.83 % (3227059)Instructions burned: 195 (million)
% 32.53/5.83 % (3227054)------------------------------
% 32.53/5.83 % (3227054)------------------------------
% 32.53/5.83 % (3227061)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=178374197:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 32.53/5.83 % (3227062)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3445529058:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 32.53/5.83 % (3227064)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=1724574644:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 32.53/5.83 % (3227061)Instruction limit reached!
% 32.53/5.83 % (3227061)------------------------------
% 32.53/5.83 % (3227061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.53/5.83 % (3227061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.53/5.83 % (3227061)CaDiCaL version: 2.1.3
% 32.53/5.83 % (3227061)Termination reason: Instruction limit
% 32.53/5.83 % (3227061)Termination phase: Saturation
% 32.53/5.83 % (3227061)Time elapsed: 0.162 s
% 32.53/5.83 % (3227061)Peak memory usage: 91 MB
% 32.53/5.83 % (3227061)Instructions burned: 158 (million)
% 32.53/5.83 % (3227064)Instruction limit reached!
% 32.53/5.83 % (3227064)------------------------------
% 32.53/5.83 % (3227064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.53/5.83 % (3227064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.76/8.31 % (3227064)CaDiCaL version: 2.1.3
% 50.76/8.31 % (3227064)Termination reason: Instruction limit
% 50.76/8.31 % (3227064)Termination phase: Saturation
% 50.76/8.31 % (3227064)Time elapsed: 0.047 s
% 50.76/8.31 % (3227064)Peak memory usage: 89 MB
% 50.76/8.31 % (3227064)Instructions burned: 108 (million)
% 50.76/8.31 % (3227065)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=454652989:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 50.76/8.31 % (3227065)Refutation not found, incomplete strategy
% 50.76/8.31 % (3227065)------------------------------
% 50.76/8.31 % (3227065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.76/8.31 % (3227065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.76/8.31 % (3227065)CaDiCaL version: 2.1.3
% 50.76/8.31 % (3227065)Termination reason: Refutation not found, incomplete strategy
% 50.76/8.31 % (3227065)Time elapsed: 0.001 s
% 50.76/8.31 % (3227065)Peak memory usage: 87 MB
% 50.76/8.31 % (3227070)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2438195771:cond=fast:i=5208:av=off_2987 on theBenchmark for (2987ds/5208Mi)
% 50.76/8.31 % (3227069)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3634645544:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 50.76/8.31 % (3227065)------------------------------
% 50.76/8.31 % (3227065)------------------------------
% 50.76/8.31 % (3227069)Instruction limit reached!
% 50.76/8.31 % (3227069)------------------------------
% 50.76/8.31 % (3227069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.76/8.31 % (3227069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.76/8.31 % (3227069)CaDiCaL version: 2.1.3
% 50.76/8.31 % (3227069)Termination reason: Instruction limit
% 50.76/8.31 % (3227069)Termination phase: Saturation
% 50.76/8.31 % (3227069)Time elapsed: 0.227 s
% 50.76/8.31 % (3227069)Peak memory usage: 89 MB
% 50.76/8.31 % (3227069)Instructions burned: 242 (million)
% 50.76/8.31 % (3227074)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1288504387:i=134:sd=2:doe=on:ss=axioms:sgt=14_2982 on theBenchmark for (2982ds/134Mi)
% 50.76/8.31 % (3227075)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=959462784:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 50.76/8.31 % (3227074)Instruction limit reached!
% 50.76/8.31 % (3227074)------------------------------
% 50.76/8.31 % (3227074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.76/8.31 % (3227074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.76/8.31 % (3227074)CaDiCaL version: 2.1.3
% 50.76/8.31 % (3227074)Termination reason: Instruction limit
% 50.76/8.31 % (3227074)Termination phase: Saturation
% 50.76/8.31 % (3227074)Time elapsed: 0.133 s
% 50.76/8.31 % (3227074)Peak memory usage: 89 MB
% 50.76/8.31 % (3227074)Instructions burned: 134 (million)
% 50.76/8.31 % (3227078)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1297034871:i=191:fgj=on:bd=all_2978 on theBenchmark for (2978ds/191Mi)
% 50.76/8.31 % (3227075)Instruction limit reached!
% 50.76/8.31 % (3227075)------------------------------
% 50.76/8.31 % (3227075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.76/8.31 % (3227075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.76/8.31 % (3227075)CaDiCaL version: 2.1.3
% 50.76/8.31 % (3227075)Termination reason: Instruction limit
% 50.76/8.31 % (3227075)Termination phase: Saturation
% 50.76/8.31 % (3227075)Time elapsed: 0.456 s
% 50.76/8.31 % (3227075)Peak memory usage: 92 MB
% 50.76/8.31 % (3227075)Instructions burned: 500 (million)
% 50.76/8.31 % (3227078)Instruction limit reached!
% 50.76/8.31 % (3227078)------------------------------
% 50.76/8.31 % (3227078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 50.76/8.31 % (3227078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 50.76/8.31 % (3227078)CaDiCaL version: 2.1.3
% 50.76/8.31 % (3227078)Termination reason: Instruction limit
% 50.76/8.31 % (3227078)Termination phase: Saturation
% 50.76/8.31 % (3227078)Time elapsed: 0.193 s
% 50.76/8.31 % (3227078)Peak memory usage: 90 MB
% 50.76/8.31 % (3227078)Instructions burned: 191 (million)
% 50.76/8.31 % (3227080)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=477477411:i=264:kws=precedence:fsr=off_2975 on theBenchmark for (2975ds/264Mi)
% 80.86/12.58 % (3227081)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2833817474:cond=on:i=156:bs=on:gtg=exists_all:er=known_2973 on theBenchmark for (2973ds/156Mi)
% 80.86/12.58 % (3227080)Instruction limit reached!
% 80.86/12.58 % (3227080)------------------------------
% 80.86/12.58 % (3227080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.86/12.58 % (3227080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.86/12.58 % (3227080)CaDiCaL version: 2.1.3
% 80.86/12.58 % (3227080)Termination reason: Instruction limit
% 80.86/12.58 % (3227080)Termination phase: Saturation
% 80.86/12.58 % (3227080)Time elapsed: 0.271 s
% 80.86/12.58 % (3227080)Peak memory usage: 89 MB
% 80.86/12.58 % (3227080)Instructions burned: 264 (million)
% 80.86/12.58 % (3227081)Instruction limit reached!
% 80.86/12.58 % (3227081)------------------------------
% 80.86/12.58 % (3227081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.86/12.58 % (3227081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.86/12.58 % (3227081)CaDiCaL version: 2.1.3
% 80.86/12.58 % (3227081)Termination reason: Instruction limit
% 80.86/12.58 % (3227081)Termination phase: Saturation
% 80.86/12.58 % (3227081)Time elapsed: 0.123 s
% 80.86/12.58 % (3227081)Peak memory usage: 89 MB
% 80.86/12.58 % (3227081)Instructions burned: 157 (million)
% 80.86/12.58 % (3227084)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=3064431703:i=3256:kws=precedence:bd=preordered:av=off_2969 on theBenchmark for (2969ds/3256Mi)
% 80.86/12.58 % (3227085)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=302149093:i=537:av=off:ss=included_2969 on theBenchmark for (2969ds/537Mi)
% 80.86/12.58 % (3227085)Instruction limit reached!
% 80.86/12.58 % (3227085)------------------------------
% 80.86/12.58 % (3227085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.86/12.58 % (3227085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.86/12.58 % (3227085)CaDiCaL version: 2.1.3
% 80.86/12.58 % (3227085)Termination reason: Instruction limit
% 80.86/12.58 % (3227085)Termination phase: Saturation
% 80.86/12.58 % (3227085)Time elapsed: 0.413 s
% 80.86/12.58 % (3227085)Peak memory usage: 89 MB
% 80.86/12.58 % (3227085)Instructions burned: 538 (million)
% 80.86/12.58 % (3227088)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=917314420:i=180:bd=preordered:av=off_2962 on theBenchmark for (2962ds/180Mi)
% 80.86/12.58 % (3227070)Instruction limit reached!
% 80.86/12.58 % (3227070)------------------------------
% 80.86/12.58 % (3227070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.86/12.58 % (3227070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.86/12.58 % (3227070)CaDiCaL version: 2.1.3
% 80.86/12.58 % (3227070)Termination reason: Instruction limit
% 80.86/12.58 % (3227070)Termination phase: Saturation
% 80.86/12.58 % (3227070)Time elapsed: 2.701 s
% 80.86/12.58 % (3227070)Peak memory usage: 166 MB
% 80.86/12.58 % (3227070)Instructions burned: 5210 (million)
% 80.86/12.58 % (3227088)Instruction limit reached!
% 80.86/12.58 % (3227088)------------------------------
% 80.86/12.58 % (3227088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.86/12.58 % (3227088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 80.86/12.58 % (3227088)CaDiCaL version: 2.1.3
% 80.86/12.58 % (3227088)Termination reason: Instruction limit
% 80.86/12.58 % (3227088)Termination phase: Saturation
% 80.86/12.58 % (3227088)Time elapsed: 0.148 s
% 80.86/12.58 % (3227088)Peak memory usage: 87 MB
% 80.86/12.58 % (3227088)Instructions burned: 181 (million)
% 80.86/12.58 % (3227091)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=4254741312:i=412:gtgl=4:gtg=exists_all_2957 on theBenchmark for (2957ds/412Mi)
% 80.86/12.58 % (3227090)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=4033358565:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2957 on theBenchmark for (2957ds/10307Mi)
% 80.86/12.58 % (3227091)Instruction limit reached!
% 80.86/12.58 % (3227091)------------------------------
% 80.86/12.58 % (3227091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 80.86/12.58 % (3227091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.11/17.36 % (3227091)CaDiCaL version: 2.1.3
% 114.11/17.36 % (3227091)Termination reason: Instruction limit
% 114.11/17.36 % (3227091)Termination phase: Saturation
% 114.11/17.36 % (3227091)Time elapsed: 0.200 s
% 114.11/17.36 % (3227091)Peak memory usage: 94 MB
% 114.11/17.36 % (3227091)Instructions burned: 412 (million)
% 114.11/17.36 % (3227062)Instruction limit reached!
% 114.11/17.36 % (3227062)------------------------------
% 114.11/17.36 % (3227062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.11/17.36 % (3227062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.11/17.36 % (3227062)CaDiCaL version: 2.1.3
% 114.11/17.36 % (3227062)Termination reason: Instruction limit
% 114.11/17.36 % (3227062)Termination phase: Saturation
% 114.11/17.36 % (3227062)Time elapsed: 3.499 s
% 114.11/17.36 % (3227062)Peak memory usage: 150 MB
% 114.11/17.36 % (3227062)Instructions burned: 3394 (million)
% 114.11/17.36 % (3227094)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=1493488401:s2pl=no:i=8478:s2at=4:nm=6_2953 on theBenchmark for (2953ds/8478Mi)
% 114.11/17.36 % (3227095)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=2189251662:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2953 on theBenchmark for (2953ds/303Mi)
% 114.11/17.36 % (3227095)Instruction limit reached!
% 114.11/17.36 % (3227095)------------------------------
% 114.11/17.36 % (3227095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.11/17.36 % (3227095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.11/17.36 % (3227095)CaDiCaL version: 2.1.3
% 114.11/17.36 % (3227095)Termination reason: Instruction limit
% 114.11/17.36 % (3227095)Termination phase: Saturation
% 114.11/17.36 % (3227095)Time elapsed: 0.242 s
% 114.11/17.36 % (3227095)Peak memory usage: 90 MB
% 114.11/17.36 % (3227095)Instructions burned: 304 (million)
% 114.11/17.36 % (3227098)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1131986710:st=4:i=720:sd=3:fsr=off:ss=axioms_2948 on theBenchmark for (2948ds/720Mi)
% 114.11/17.36 % (3227098)Instruction limit reached!
% 114.11/17.36 % (3227098)------------------------------
% 114.11/17.36 % (3227098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.11/17.36 % (3227098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.11/17.36 % (3227098)CaDiCaL version: 2.1.3
% 114.11/17.36 % (3227098)Termination reason: Instruction limit
% 114.11/17.36 % (3227098)Termination phase: Saturation
% 114.11/17.36 % (3227098)Time elapsed: 0.559 s
% 114.11/17.36 % (3227098)Peak memory usage: 89 MB
% 114.11/17.36 % (3227098)Instructions burned: 720 (million)
% 114.11/17.36 % (3227100)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3596650727:i=598:bs=on:bd=preordered:av=off:ss=axioms_2939 on theBenchmark for (2939ds/598Mi)
% 114.11/17.36 % (3227084)Instruction limit reached!
% 114.11/17.36 % (3227084)------------------------------
% 114.11/17.36 % (3227084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.11/17.36 % (3227084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.11/17.36 % (3227084)CaDiCaL version: 2.1.3
% 114.11/17.36 % (3227084)Termination reason: Instruction limit
% 114.11/17.36 % (3227084)Termination phase: Saturation
% 114.11/17.36 % (3227084)Time elapsed: 3.086 s
% 114.11/17.36 % (3227084)Peak memory usage: 158 MB
% 114.11/17.36 % (3227084)Instructions burned: 3256 (million)
% 114.11/17.36 % (3227102)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=228202033:i=2989:sd=3:ss=axioms:sgt=60_2935 on theBenchmark for (2935ds/2989Mi)
% 114.11/17.36 % (3227100)Instruction limit reached!
% 114.11/17.36 % (3227100)------------------------------
% 114.11/17.36 % (3227100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 114.11/17.36 % (3227100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 114.11/17.36 % (3227100)CaDiCaL version: 2.1.3
% 114.11/17.36 % (3227100)Termination reason: Instruction limit
% 114.11/17.36 % (3227100)Termination phase: Saturation
% 114.11/17.36 % (3227100)Time elapsed: 0.518 s
% 114.11/17.36 % (3227100)Peak memory usage: 94 MB
% 114.11/17.36 % (3227100)Instructions burned: 598 (million)
% 114.11/17.36 % (3227104)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=299463270:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2931 on theBenchmark for (2931ds/1997Mi)
% 159.59/23.74 % (3227104)Instruction limit reached!
% 159.59/23.74 % (3227104)------------------------------
% 159.59/23.74 % (3227104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.59/23.74 % (3227104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.59/23.74 % (3227104)CaDiCaL version: 2.1.3
% 159.59/23.74 % (3227104)Termination reason: Instruction limit
% 159.59/23.74 % (3227104)Termination phase: Saturation
% 159.59/23.74 % (3227104)Time elapsed: 1.978 s
% 159.59/23.74 % (3227104)Peak memory usage: 133 MB
% 159.59/23.74 % (3227104)Instructions burned: 1997 (million)
% 159.59/23.74 % (3227094)Instruction limit reached!
% 159.59/23.74 % (3227094)------------------------------
% 159.59/23.74 % (3227094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.59/23.74 % (3227094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.59/23.74 % (3227094)CaDiCaL version: 2.1.3
% 159.59/23.74 % (3227094)Termination reason: Instruction limit
% 159.59/23.74 % (3227094)Termination phase: Saturation
% 159.59/23.74 % (3227094)Time elapsed: 4.279 s
% 159.59/23.74 % (3227094)Peak memory usage: 194 MB
% 159.59/23.74 % (3227094)Instructions burned: 8480 (million)
% 159.59/23.74 % (3227107)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=768289082:i=1098:nicw=on_2908 on theBenchmark for (2908ds/1098Mi)
% 159.59/23.74 % (3227106)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=1550312441:i=2088:bd=preordered:av=off_2909 on theBenchmark for (2909ds/2088Mi)
% 159.59/23.74 % (3227102)Instruction limit reached!
% 159.59/23.74 % (3227102)------------------------------
% 159.59/23.74 % (3227102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.59/23.74 % (3227102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.59/23.74 % (3227102)CaDiCaL version: 2.1.3
% 159.59/23.74 % (3227102)Termination reason: Instruction limit
% 159.59/23.74 % (3227102)Termination phase: Saturation
% 159.59/23.74 % (3227102)Time elapsed: 3.060 s
% 159.59/23.74 % (3227102)Peak memory usage: 147 MB
% 159.59/23.74 % (3227102)Instructions burned: 2991 (million)
% 159.59/23.74 % (3227107)Instruction limit reached!
% 159.59/23.74 % (3227107)------------------------------
% 159.59/23.74 % (3227107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.59/23.74 % (3227107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.59/23.74 % (3227107)CaDiCaL version: 2.1.3
% 159.59/23.74 % (3227107)Termination reason: Instruction limit
% 159.59/23.74 % (3227107)Termination phase: Saturation
% 159.59/23.74 % (3227107)Time elapsed: 0.511 s
% 159.59/23.74 % (3227107)Peak memory usage: 99 MB
% 159.59/23.74 % (3227107)Instructions burned: 1099 (million)
% 159.59/23.74 % (3227111)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4197719329:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2901 on theBenchmark for (2901ds/2942Mi)
% 159.59/23.74 % (3227110)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2768818163:i=433:bd=preordered_2901 on theBenchmark for (2901ds/433Mi)
% 159.59/23.74 % (3227110)Instruction limit reached!
% 159.59/23.74 % (3227110)------------------------------
% 159.59/23.74 % (3227110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.59/23.74 % (3227110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.59/23.74 % (3227110)CaDiCaL version: 2.1.3
% 159.59/23.74 % (3227110)Termination reason: Instruction limit
% 159.59/23.74 % (3227110)Termination phase: Saturation
% 159.59/23.74 % (3227110)Time elapsed: 0.410 s
% 159.59/23.74 % (3227110)Peak memory usage: 92 MB
% 159.59/23.74 % (3227110)Instructions burned: 434 (million)
% 159.59/23.74 % (3227114)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=115657040:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2895 on theBenchmark for (2895ds/6922Mi)
% 159.59/23.74 % (3227106)Instruction limit reached!
% 159.59/23.74 % (3227106)------------------------------
% 159.59/23.74 % (3227106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.59/23.74 % (3227106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.59/23.74 % (3227106)CaDiCaL version: 2.1.3
% 159.59/23.74 % (3227106)Termination reason: Instruction limit
% 159.59/23.74 % (3227106)Termination phase: Saturation
% 176.35/26.11 % (3227106)Time elapsed: 2.028 s
% 176.35/26.11 % (3227106)Peak memory usage: 133 MB
% 176.35/26.11 % (3227106)Instructions burned: 2089 (million)
% 176.35/26.11 % (3227116)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=1136270633:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2886 on theBenchmark for (2886ds/596Mi)
% 176.35/26.11 % (3227111)Instruction limit reached!
% 176.35/26.11 % (3227111)------------------------------
% 176.35/26.11 % (3227111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.35/26.11 % (3227111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.35/26.11 % (3227111)CaDiCaL version: 2.1.3
% 176.35/26.11 % (3227111)Termination reason: Instruction limit
% 176.35/26.11 % (3227111)Termination phase: Saturation
% 176.35/26.11 % (3227111)Time elapsed: 1.661 s
% 176.35/26.11 % (3227111)Peak memory usage: 141 MB
% 176.35/26.11 % (3227111)Instructions burned: 2943 (million)
% 176.35/26.11 % (3227118)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=4101173886:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2882 on theBenchmark for (2882ds/4123Mi)
% 176.35/26.11 % (3227116)Instruction limit reached!
% 176.35/26.11 % (3227116)------------------------------
% 176.35/26.11 % (3227116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.35/26.11 % (3227116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.35/26.11 % (3227116)CaDiCaL version: 2.1.3
% 176.35/26.11 % (3227116)Termination reason: Instruction limit
% 176.35/26.11 % (3227116)Termination phase: Saturation
% 176.35/26.11 % (3227116)Time elapsed: 0.482 s
% 176.35/26.11 % (3227116)Peak memory usage: 93 MB
% 176.35/26.11 % (3227116)Instructions burned: 597 (million)
% 176.35/26.11 % (3227120)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2260878523:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2878 on theBenchmark for (2878ds/16411Mi)
% 176.35/26.11 % (3227118)Instruction limit reached!
% 176.35/26.11 % (3227118)------------------------------
% 176.35/26.11 % (3227118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.35/26.11 % (3227118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.35/26.11 % (3227118)CaDiCaL version: 2.1.3
% 176.35/26.11 % (3227118)Termination reason: Instruction limit
% 176.35/26.11 % (3227118)Termination phase: Saturation
% 176.35/26.11 % (3227118)Time elapsed: 2.147 s
% 176.35/26.11 % (3227118)Peak memory usage: 158 MB
% 176.35/26.11 % (3227118)Instructions burned: 4123 (million)
% 176.35/26.11 % (3227122)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3584051685:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2858 on theBenchmark for (2858ds/1670Mi)
% 176.35/26.11 % (3227090)Instruction limit reached!
% 176.35/26.11 % (3227090)------------------------------
% 176.35/26.11 % (3227090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.35/26.11 % (3227090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.35/26.11 % (3227090)CaDiCaL version: 2.1.3
% 176.35/26.11 % (3227090)Termination reason: Instruction limit
% 176.35/26.11 % (3227090)Termination phase: Saturation
% 176.35/26.11 % (3227090)Time elapsed: 10.271 s
% 176.35/26.11 % (3227090)Peak memory usage: 186 MB
% 176.35/26.11 % (3227090)Instructions burned: 10307 (million)
% 176.35/26.11 % (3227133)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=2518125052:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2852 on theBenchmark for (2852ds/1722Mi)
% 176.35/26.11 % (3227122)Instruction limit reached!
% 176.35/26.11 % (3227122)------------------------------
% 176.35/26.11 % (3227122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 176.35/26.11 % (3227122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.35/26.11 % (3227122)CaDiCaL version: 2.1.3
% 176.35/26.11 % (3227122)Termination reason: Instruction limit
% 176.35/26.11 % (3227122)Termination phase: Saturation
% 176.35/26.11 % (3227122)Time elapsed: 1.521 s
% 176.35/26.11 % (3227122)Peak memory usage: 137 MB
% 176.35/26.11 % (3227122)Instructions burned: 1835 (million)
% 176.35/26.11 % (3227143)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=2494417347:cts=off:cond=on:i=9530:bs=on:fsd=on_2841 on theBenchmark for (2841ds/9530Mi)
% 192.46/28.40 % (3227133)Instruction limit reached!
% 192.46/28.40 % (3227133)------------------------------
% 192.46/28.40 % (3227133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.46/28.40 % (3227133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.46/28.40 % (3227133)CaDiCaL version: 2.1.3
% 192.46/28.40 % (3227133)Termination reason: Instruction limit
% 192.46/28.40 % (3227133)Termination phase: Saturation
% 192.46/28.40 % (3227133)Time elapsed: 1.794 s
% 192.46/28.40 % (3227133)Peak memory usage: 134 MB
% 192.46/28.40 % (3227133)Instructions burned: 1723 (million)
% 192.46/28.40 % (3227145)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3585984563:st=2:i=4495:sd=10:ss=included_2831 on theBenchmark for (2831ds/4495Mi)
% 192.46/28.40 % (3227114)Instruction limit reached!
% 192.46/28.40 % (3227114)------------------------------
% 192.46/28.40 % (3227114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.46/28.40 % (3227114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.46/28.40 % (3227114)CaDiCaL version: 2.1.3
% 192.46/28.40 % (3227114)Termination reason: Instruction limit
% 192.46/28.40 % (3227114)Termination phase: Saturation
% 192.46/28.40 % (3227114)Time elapsed: 6.456 s
% 192.46/28.40 % (3227114)Peak memory usage: 179 MB
% 192.46/28.40 % (3227114)Instructions burned: 6923 (million)
% 192.46/28.40 % (3227147)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=3822623933:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2827 on theBenchmark for (2827ds/4920Mi)
% 192.46/28.40 % (3227143)Instruction limit reached!
% 192.46/28.40 % (3227143)------------------------------
% 192.46/28.40 % (3227143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.46/28.40 % (3227143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.46/28.40 % (3227143)CaDiCaL version: 2.1.3
% 192.46/28.40 % (3227143)Termination reason: Instruction limit
% 192.46/28.40 % (3227143)Termination phase: Saturation
% 192.46/28.40 % (3227143)Time elapsed: 5.391 s
% 192.46/28.40 % (3227143)Peak memory usage: 161 MB
% 192.46/28.40 % (3227143)Instructions burned: 9531 (million)
% 192.46/28.40 % (3227145)Instruction limit reached!
% 192.46/28.40 % (3227145)------------------------------
% 192.46/28.40 % (3227145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.46/28.40 % (3227145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.46/28.40 % (3227145)CaDiCaL version: 2.1.3
% 192.46/28.40 % (3227145)Termination reason: Instruction limit
% 192.46/28.40 % (3227145)Termination phase: Saturation
% 192.46/28.40 % (3227145)Time elapsed: 4.544 s
% 192.46/28.40 % (3227145)Peak memory usage: 160 MB
% 192.46/28.40 % (3227145)Instructions burned: 4495 (million)
% 192.46/28.40 % (3227149)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=2239871907:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2784 on theBenchmark for (2784ds/2083Mi)
% 192.46/28.40 % (3227150)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=4127542118:i=4629:av=off:gsp=on_2783 on theBenchmark for (2783ds/4629Mi)
% 192.46/28.40 % (3227147)Instruction limit reached!
% 192.46/28.40 % (3227147)------------------------------
% 192.46/28.40 % (3227147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.46/28.40 % (3227147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.46/28.40 % (3227147)CaDiCaL version: 2.1.3
% 192.46/28.40 % (3227147)Termination reason: Instruction limit
% 192.46/28.40 % (3227147)Termination phase: Saturation
% 192.46/28.40 % (3227147)Time elapsed: 4.681 s
% 192.46/28.40 % (3227147)Peak memory usage: 162 MB
% 192.46/28.40 % (3227147)Instructions burned: 4921 (million)
% 192.46/28.40 % (3227197)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=915040807:i=1258:av=off_2777 on theBenchmark for (2777ds/1258Mi)
% 192.46/28.40 % (3227150)Refutation not found, incomplete strategy
% 192.46/28.40 % (3227150)------------------------------
% 192.46/28.40 % (3227150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 192.46/28.40 % (3227150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.46/28.40 % (3227150)CaDiCaL version: 2.1.3
% 192.46/28.40 % (3227150)Termination reason: Refutation not found, incomplete strategy
% 219.48/32.19 % (3227150)Time elapsed: 0.622 s
% 219.48/32.19 % (3227150)Peak memory usage: 127 MB
% 219.48/32.19 % (3227150)Instructions burned: 856 (million)
% 219.48/32.19 % (3227149)Instruction limit reached!
% 219.48/32.19 % (3227149)------------------------------
% 219.48/32.19 % (3227149)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 219.48/32.19 % (3227149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.48/32.19 % (3227149)CaDiCaL version: 2.1.3
% 219.48/32.19 % (3227149)Termination reason: Instruction limit
% 219.48/32.19 % (3227149)Termination phase: Saturation
% 219.48/32.19 % (3227149)Time elapsed: 0.822 s
% 219.48/32.19 % (3227149)Peak memory usage: 137 MB
% 219.48/32.19 % (3227149)Instructions burned: 2088 (million)
% 219.48/32.19 % (3227313)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=2821203236:i=7343:av=off:ss=included_2774 on theBenchmark for (2774ds/7343Mi)
% 219.48/32.19 % (3227150)------------------------------
% 219.48/32.19 % (3227150)------------------------------
% 219.48/32.19 % (3227315)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=3618490975:i=1325:sd=2:ss=axioms:sgt=16_2772 on theBenchmark for (2772ds/1325Mi)
% 219.48/32.19 % (3227315)Refutation not found, incomplete strategy
% 219.48/32.19 % (3227315)------------------------------
% 219.48/32.19 % (3227315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 219.48/32.19 % (3227315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.48/32.19 % (3227315)CaDiCaL version: 2.1.3
% 219.48/32.19 % (3227315)Termination reason: Refutation not found, incomplete strategy
% 219.48/32.19 % (3227315)Time elapsed: 0.001 s
% 219.48/32.19 % (3227315)Peak memory usage: 87 MB
% 219.48/32.19 % (3227197)Instruction limit reached!
% 219.48/32.19 % (3227197)------------------------------
% 219.48/32.19 % (3227197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 219.48/32.19 % (3227197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.48/32.19 % (3227197)CaDiCaL version: 2.1.3
% 219.48/32.19 % (3227197)Termination reason: Instruction limit
% 219.48/32.19 % (3227197)Termination phase: Saturation
% 219.48/32.19 % (3227197)Time elapsed: 0.693 s
% 219.48/32.19 % (3227197)Peak memory usage: 116 MB
% 219.48/32.19 % (3227197)Instructions burned: 1259 (million)
% 219.48/32.19 % (3227315)------------------------------
% 219.48/32.19 % (3227315)------------------------------
% 219.48/32.19 % (3227317)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=4058745420: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)
% 219.48/32.19 % (3227318)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=306471853:i=1489:sd=2:ep=R:ss=axioms_2768 on theBenchmark for (2768ds/1489Mi)
% 219.48/32.19 % (3227317)Instruction limit reached!
% 219.48/32.19 % (3227317)------------------------------
% 219.48/32.19 % (3227317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 219.48/32.19 % (3227317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.48/32.19 % (3227317)CaDiCaL version: 2.1.3
% 219.48/32.19 % (3227317)Termination reason: Instruction limit
% 219.48/32.19 % (3227317)Termination phase: Saturation
% 219.48/32.19 % (3227317)Time elapsed: 0.982 s
% 219.48/32.19 % (3227317)Peak memory usage: 141 MB
% 219.48/32.19 % (3227317)Instructions burned: 2649 (million)
% 219.48/32.19 % (3227321)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=52964613:i=1503_2758 on theBenchmark for (2758ds/1503Mi)
% 219.48/32.19 % (3227318)Instruction limit reached!
% 219.48/32.19 % (3227318)------------------------------
% 219.48/32.19 % (3227318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 219.48/32.19 % (3227318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.48/32.19 % (3227318)CaDiCaL version: 2.1.3
% 219.48/32.19 % (3227318)Termination reason: Instruction limit
% 219.48/32.19 % (3227318)Termination phase: Saturation
% 219.48/32.19 % (3227318)Time elapsed: 0.989 s
% 219.48/32.19 % (3227318)Peak memory usage: 130 MB
% 219.48/32.19 % (3227318)Instructions burned: 1489 (million)
% 219.48/32.19 % (3227323)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=4113239067:i=13942:kws=frequency_2756 on theBenchmark for (2756ds/13942Mi)
% 219.48/32.19 % (3227321)Instruction limit reached!
% 219.48/32.19 % (3227321)------------------------------
% 238.56/35.02 % (3227321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.56/35.02 % (3227321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.56/35.02 % (3227321)CaDiCaL version: 2.1.3
% 238.56/35.02 % (3227321)Termination reason: Instruction limit
% 238.56/35.02 % (3227321)Termination phase: Saturation
% 238.56/35.02 % (3227321)Time elapsed: 0.585 s
% 238.56/35.02 % (3227321)Peak memory usage: 130 MB
% 238.56/35.02 % (3227321)Instructions burned: 1506 (million)
% 238.56/35.02 % (3227325)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=2050871083:i=3604:fsr=off:er=filter_2750 on theBenchmark for (2750ds/3604Mi)
% 238.56/35.02 % (3227120)Instruction limit reached!
% 238.56/35.02 % (3227120)------------------------------
% 238.56/35.02 % (3227120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.56/35.02 % (3227120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.56/35.02 % (3227120)CaDiCaL version: 2.1.3
% 238.56/35.02 % (3227120)Termination reason: Instruction limit
% 238.56/35.02 % (3227120)Termination phase: Saturation
% 238.56/35.02 % (3227120)Time elapsed: 13.375 s
% 238.56/35.02 % (3227120)Peak memory usage: 280 MB
% 238.56/35.02 % (3227120)Instructions burned: 16417 (million)
% 238.56/35.02 % (3227327)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1338169149:i=1876:sd=1:ss=included:sgt=32_2741 on theBenchmark for (2741ds/1876Mi)
% 238.56/35.02 % (3227325)Instruction limit reached!
% 238.56/35.02 % (3227325)------------------------------
% 238.56/35.02 % (3227325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.56/35.02 % (3227325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.56/35.02 % (3227325)CaDiCaL version: 2.1.3
% 238.56/35.02 % (3227325)Termination reason: Instruction limit
% 238.56/35.02 % (3227325)Termination phase: Saturation
% 238.56/35.02 % (3227325)Time elapsed: 1.127 s
% 238.56/35.02 % (3227325)Peak memory usage: 163 MB
% 238.56/35.02 % (3227325)Instructions burned: 3608 (million)
% 238.56/35.02 % (3227329)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=1497106649:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2738 on theBenchmark for (2738ds/1932Mi)
% 238.56/35.02 % (3227313)Instruction limit reached!
% 238.56/35.02 % (3227313)------------------------------
% 238.56/35.02 % (3227313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.56/35.02 % (3227313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.56/35.02 % (3227313)CaDiCaL version: 2.1.3
% 238.56/35.02 % (3227313)Termination reason: Instruction limit
% 238.56/35.02 % (3227313)Termination phase: Saturation
% 238.56/35.02 % (3227313)Time elapsed: 4.026 s
% 238.56/35.02 % (3227313)Peak memory usage: 186 MB
% 238.56/35.02 % (3227313)Instructions burned: 7344 (million)
% 238.56/35.02 % (3227329)Instruction limit reached!
% 238.56/35.02 % (3227329)------------------------------
% 238.56/35.02 % (3227329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.56/35.02 % (3227329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.56/35.02 % (3227329)CaDiCaL version: 2.1.3
% 238.56/35.02 % (3227329)Termination reason: Instruction limit
% 238.56/35.02 % (3227329)Termination phase: Saturation
% 238.56/35.02 % (3227329)Time elapsed: 0.622 s
% 238.56/35.02 % (3227329)Peak memory usage: 137 MB
% 238.56/35.02 % (3227329)Instructions burned: 1933 (million)
% 238.56/35.02 % (3227331)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=1214430907:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2732 on theBenchmark for (2732ds/1980Mi)
% 238.56/35.02 % (3227332)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=2064219370:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2730 on theBenchmark for (2730ds/3902Mi)
% 238.56/35.02 % (3227327)Instruction limit reached!
% 238.56/35.02 % (3227327)------------------------------
% 238.56/35.02 % (3227327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 238.56/35.02 % (3227327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 238.56/35.02 % (3227327)CaDiCaL version: 2.1.3
% 238.56/35.02 % (3227327)Termination reason: Instruction limit
% 238.56/35.02 % (3227327)Termination phase: Saturation
% 272.50/39.68 % (3227327)Time elapsed: 1.205 s
% 272.50/39.68 % (3227327)Peak memory usage: 136 MB
% 272.50/39.68 % (3227327)Instructions burned: 1876 (million)
% 272.50/39.68 % (3227335)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=2082858246:avsq=on:i=3916:aac=none:amm=off_2728 on theBenchmark for (2728ds/3916Mi)
% 272.50/39.68 % (3227331)Instruction limit reached!
% 272.50/39.68 % (3227331)------------------------------
% 272.50/39.68 % (3227331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 272.50/39.68 % (3227331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 272.50/39.68 % (3227331)CaDiCaL version: 2.1.3
% 272.50/39.68 % (3227331)Termination reason: Instruction limit
% 272.50/39.68 % (3227331)Termination phase: Saturation
% 272.50/39.68 % (3227331)Time elapsed: 1.225 s
% 272.50/39.68 % (3227331)Peak memory usage: 133 MB
% 272.50/39.68 % (3227331)Instructions burned: 1981 (million)
% 272.50/39.68 % (3227394)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=3164108448:cond=on:i=3940:av=off:er=known_2718 on theBenchmark for (2718ds/3940Mi)
% 272.50/39.68 % (3227332)Instruction limit reached!
% 272.50/39.68 % (3227332)------------------------------
% 272.50/39.68 % (3227332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 272.50/39.68 % (3227332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 272.50/39.68 % (3227332)CaDiCaL version: 2.1.3
% 272.50/39.68 % (3227332)Termination reason: Instruction limit
% 272.50/39.68 % (3227332)Termination phase: Saturation
% 272.50/39.68 % (3227332)Time elapsed: 1.420 s
% 272.50/39.68 % (3227332)Peak memory usage: 139 MB
% 272.50/39.68 % (3227332)Instructions burned: 3904 (million)
% 272.50/39.68 % (3227501)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=3318650689:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2715 on theBenchmark for (2715ds/3980Mi)
% 272.50/39.68 % (3227335)Instruction limit reached!
% 272.50/39.68 % (3227335)------------------------------
% 272.50/39.68 % (3227335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 272.50/39.68 % (3227335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 272.50/39.68 % (3227335)CaDiCaL version: 2.1.3
% 272.50/39.68 % (3227335)Termination reason: Instruction limit
% 272.50/39.68 % (3227335)Termination phase: Saturation
% 272.50/39.68 % (3227335)Time elapsed: 2.390 s
% 272.50/39.68 % (3227335)Peak memory usage: 123 MB
% 272.50/39.68 % (3227335)Instructions burned: 3916 (million)
% 272.50/39.68 % (3227618)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=1505619534:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2702 on theBenchmark for (2702ds/2087Mi)
% 272.50/39.68 % (3227501)Instruction limit reached!
% 272.50/39.68 % (3227501)------------------------------
% 272.50/39.68 % (3227501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 272.50/39.68 % (3227501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 272.50/39.68 % (3227501)CaDiCaL version: 2.1.3
% 272.50/39.68 % (3227501)Termination reason: Instruction limit
% 272.50/39.68 % (3227501)Termination phase: Saturation
% 272.50/39.68 % (3227501)Time elapsed: 1.622 s
% 272.50/39.68 % (3227501)Peak memory usage: 155 MB
% 272.50/39.68 % (3227501)Instructions burned: 3981 (million)
% 272.50/39.68 % (3227620)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=1170203838:cts=off:cond=on:i=4272:bs=on:fsd=on_2697 on theBenchmark for (2697ds/4272Mi)
% 272.50/39.68 % (3227394)Instruction limit reached!
% 272.50/39.68 % (3227394)------------------------------
% 272.50/39.68 % (3227394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 272.50/39.68 % (3227394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 272.50/39.68 % (3227394)CaDiCaL version: 2.1.3
% 272.50/39.68 % (3227394)Termination reason: Instruction limit
% 272.50/39.68 % (3227394)Termination phase: Saturation
% 272.50/39.68 % (3227394)Time elapsed: 2.476 s
% 272.50/39.68 % (3227394)Peak memory usage: 155 MB
% 272.50/39.68 % (3227394)Instructions burned: 3941 (million)
% 272.50/39.68 % (3227622)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=604916824:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2691 on theBenchmark for (2691ds/2197Mi)
% 155.90/40.19 % (3227618)Instruction limit reached!
% 155.90/40.19 % (3227618)------------------------------
% 155.90/40.19 % (3227618)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227618)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227618)Termination reason: Instruction limit
% 155.90/40.19 % (3227618)Termination phase: Saturation
% 155.90/40.19 % (3227618)Time elapsed: 1.297 s
% 155.90/40.19 % (3227618)Peak memory usage: 138 MB
% 155.90/40.19 % (3227618)Instructions burned: 2088 (million)
% 155.90/40.19 % (3227624)dis+21_1_sil=8000:spb=goal_then_units:random_seed=190559745:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2687 on theBenchmark for (2687ds/6508Mi)
% 155.90/40.19 % (3227620)Instruction limit reached!
% 155.90/40.19 % (3227620)------------------------------
% 155.90/40.19 % (3227620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227620)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227620)Termination reason: Instruction limit
% 155.90/40.19 % (3227620)Termination phase: Saturation
% 155.90/40.19 % (3227620)Time elapsed: 1.461 s
% 155.90/40.19 % (3227620)Peak memory usage: 150 MB
% 155.90/40.19 % (3227620)Instructions burned: 4274 (million)
% 155.90/40.19 % (3227626)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=2997192229:i=2330:fgj=on:av=off:fsr=off_2681 on theBenchmark for (2681ds/2330Mi)
% 155.90/40.19 % (3227622)Instruction limit reached!
% 155.90/40.19 % (3227622)------------------------------
% 155.90/40.19 % (3227622)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227622)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227622)Termination reason: Instruction limit
% 155.90/40.19 % (3227622)Termination phase: Saturation
% 155.90/40.19 % (3227622)Time elapsed: 1.313 s
% 155.90/40.19 % (3227622)Peak memory usage: 139 MB
% 155.90/40.19 % (3227622)Instructions burned: 2199 (million)
% 155.90/40.19 % (3227628)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=3446249845:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2676 on theBenchmark for (2676ds/7592Mi)
% 155.90/40.19 % (3227626)Instruction limit reached!
% 155.90/40.19 % (3227626)------------------------------
% 155.90/40.19 % (3227626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227626)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227626)Termination reason: Instruction limit
% 155.90/40.19 % (3227626)Termination phase: Saturation
% 155.90/40.19 % (3227626)Time elapsed: 0.788 s
% 155.90/40.19 % (3227626)Peak memory usage: 138 MB
% 155.90/40.19 % (3227626)Instructions burned: 2331 (million)
% 155.90/40.19 % (3227630)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=3754183749:i=2693:kws=precedence:ins=1:av=off_2672 on theBenchmark for (2672ds/2693Mi)
% 155.90/40.19 % (3227323)Instruction limit reached!
% 155.90/40.19 % (3227323)------------------------------
% 155.90/40.19 % (3227323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227323)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227323)Termination reason: Instruction limit
% 155.90/40.19 % (3227323)Termination phase: Saturation
% 155.90/40.19 % (3227323)Time elapsed: 8.566 s
% 155.90/40.19 % (3227323)Peak memory usage: 251 MB
% 155.90/40.19 % (3227323)Instructions burned: 13943 (million)
% 155.90/40.19 % (3227632)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=1982205677:i=28651:sd=4:ss=included:sgt=64_2669 on theBenchmark for (2669ds/28651Mi)
% 155.90/40.19 % (3227630)Instruction limit reached!
% 155.90/40.19 % (3227630)------------------------------
% 155.90/40.19 % (3227630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227630)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227630)Termination reason: Instruction limit
% 155.90/40.19 % (3227630)Termination phase: Saturation
% 155.90/40.19 % (3227630)Time elapsed: 0.910 s
% 155.90/40.19 % (3227630)Peak memory usage: 148 MB
% 155.90/40.19 % (3227630)Instructions burned: 2694 (million)
% 155.90/40.19 % (3227635)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=2128951879:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2661 on theBenchmark for (2661ds/2700Mi)
% 155.90/40.19 % (3227635)Instruction limit reached!
% 155.90/40.19 % (3227635)------------------------------
% 155.90/40.19 % (3227635)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227635)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227635)Termination reason: Instruction limit
% 155.90/40.19 % (3227635)Termination phase: Saturation
% 155.90/40.19 % (3227635)Time elapsed: 0.956 s
% 155.90/40.19 % (3227635)Peak memory usage: 141 MB
% 155.90/40.19 % (3227635)Instructions burned: 2701 (million)
% 155.90/40.19 % (3227637)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=3381434292:i=3196:nm=4_2650 on theBenchmark for (2650ds/3196Mi)
% 155.90/40.19 % (3227624)Instruction limit reached!
% 155.90/40.19 % (3227624)------------------------------
% 155.90/40.19 % (3227624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227624)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227624)Termination reason: Instruction limit
% 155.90/40.19 % (3227624)Termination phase: Saturation
% 155.90/40.19 % (3227624)Time elapsed: 3.691 s
% 155.90/40.19 % (3227624)Peak memory usage: 148 MB
% 155.90/40.19 % (3227624)Instructions burned: 6508 (million)
% 155.90/40.19 % (3227639)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=1555997860:cts=off:i=3254:av=off_2649 on theBenchmark for (2649ds/3254Mi)
% 155.90/40.19 % (3227628)Instruction limit reached!
% 155.90/40.19 % (3227628)------------------------------
% 155.90/40.19 % (3227628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.19 % (3227628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.19 % (3227628)CaDiCaL version: 2.1.3
% 155.90/40.19 % (3227628)Termination reason: Instruction limit
% 155.90/40.19 % (3227628)Termination phase: Saturation
% 155.90/40.20 % (3227628)Time elapsed: 3.597 s
% 155.90/40.20 % (3227628)Peak memory usage: 150 MB
% 155.90/40.20 % (3227628)Instructions burned: 7593 (million)
% 155.90/40.20 % (3227637)Instruction limit reached!
% 155.90/40.20 % (3227637)------------------------------
% 155.90/40.20 % (3227637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.20 % (3227637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.20 % (3227637)CaDiCaL version: 2.1.3
% 155.90/40.20 % (3227637)Termination reason: Instruction limit
% 155.90/40.20 % (3227637)Termination phase: Saturation
% 155.90/40.20 % (3227637)Time elapsed: 1.150 s
% 155.90/40.20 % (3227637)Peak memory usage: 136 MB
% 155.90/40.20 % (3227637)Instructions burned: 3198 (million)
% 155.90/40.20 % (3227641)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1063282631:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2639 on theBenchmark for (2639ds/3264Mi)
% 155.90/40.20 % (3227642)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=2749271898:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2637 on theBenchmark for (2637ds/9708Mi)
% 155.90/40.20 % (3227639)Instruction limit reached!
% 155.90/40.20 % (3227639)------------------------------
% 155.90/40.20 % (3227639)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.20 % (3227639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.20 % (3227639)CaDiCaL version: 2.1.3
% 155.90/40.20 % (3227639)Termination reason: Instruction limit
% 155.90/40.20 % (3227639)Termination phase: Saturation
% 155.90/40.20 % (3227639)Time elapsed: 2.044 s
% 155.90/40.20 % (3227639)Peak memory usage: 147 MB
% 155.90/40.20 % (3227639)Instructions burned: 3255 (million)
% 155.90/40.20 % (3227645)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=953939793:i=21997:s2at=5:gtg=all_2626 on theBenchmark for (2626ds/21997Mi)
% 155.90/40.20 % (3227641)Instruction limit reached!
% 155.90/40.20 % (3227641)------------------------------
% 155.90/40.20 % (3227641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.90/40.20 % (3227641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.90/40.20 % (3227641)CaDiCaL version: 2.1.3
% 155.90/40.20 % (3227641)Termination reason: Instruction limit
% 155.90/40.20 % (3227641)Termination phase: Saturation
% 155.90/40.20 % (3227641)Time elapsed: 2.227 s
% 155.90/40.20 % (3227641)Peak memory usage: 144 MB
% 155.90/40.20 % (3227641)Instructions burned: 3265 (million)
% 155.90/40.20 % (3227647)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3027405385:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2615 on theBenchmark for (2615ds/7551Mi)
% 155.90/40.20 % (3227632)First to succeed.
% 155.90/40.20 % (3227632)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3227033"
% 155.90/40.20 % (3227632)Refutation found. Thanks to Tanya!
% 155.90/40.20 % SZS status Unsatisfiable for theBenchmark
% 155.90/40.20 % SZS output start Proof for theBenchmark
% See solution above
% 276.67/40.43 % (3227632)------------------------------
% 276.67/40.43 % (3227632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 276.67/40.43 % (3227632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 276.67/40.43 % (3227632)CaDiCaL version: 2.1.3
% 276.67/40.43 % (3227632)Termination reason: Refutation
% 276.67/40.43 % (3227632)Time elapsed: 5.400 s
% 276.67/40.43 % (3227632)Peak memory usage: 207 MB
% 276.67/40.43 % (3227632)Instructions burned: 9088 (million)
% 276.67/40.43 % (3227632)------------------------------
% 276.67/40.43 % (3227632)------------------------------
% 276.67/40.43 % (3227033)Success in time 38.979 s
% 276.67/40.43 % Vampire exiting
%------------------------------------------------------------------------------