%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL084-2 : TPTP v9.3.1. Bugfixed v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:51:09 AM UTC 2026
% Result : Unsatisfiable 94.98s 14.28s
% Output : Refutation 95.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 10
% Syntax : Number of formulae : 111 ( 20 unt; 6 def)
% Number of atoms : 328 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 427 ( 210 ~; 211 |; 0 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 7 usr; 7 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 313 ( 0 sgn 313 !; 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] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X2,X0),implies(X3,X0)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ic_JLukasiewicz) ).
fof(f3,axiom,
! [X0] : is_a_theorem(implies(X0,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ic_1) ).
fof(f4,negated_conjecture,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_ic_4) ).
fof(f5,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(implies(X2,X0),implies(X3,X0))) ),
inference(resolution,[],[f1,f2]) ).
fof(f7,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,[],[f5,f2]) ).
fof(f8,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,X0))),
inference(resolution,[],[f5,f3]) ).
fof(f9,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(X1,X2)),implies(X3,implies(X1,X2)))),
inference(resolution,[],[f8,f5]) ).
fof(f12,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X1)),implies(X1,X3)))
| is_a_theorem(implies(X4,implies(X1,X3))) ),
inference(resolution,[],[f7,f1]) ).
fof(f13,plain,
! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),implies(X3,X1)),implies(X4,implies(X3,X1)))),
inference(resolution,[],[f9,f5]) ).
fof(f15,plain,
! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),implies(X3,implies(X2,X4))),implies(X5,implies(X3,implies(X2,X4))))),
inference(resolution,[],[f13,f5]) ).
fof(f16,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X3,X1)))
| is_a_theorem(implies(X4,implies(X3,X1))) ),
inference(resolution,[],[f13,f1]) ).
fof(f18,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X1)))),
inference(resolution,[],[f12,f8]) ).
fof(f22,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(X1,implies(X2,X1))) ),
inference(resolution,[],[f18,f1]) ).
fof(f24,definition,
( spl0_1
<=> ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X1))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f25,plain,
( ! [X2,X1] : is_a_theorem(implies(X1,implies(X2,X1)))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f24]) ).
fof(f27,definition,
( spl0_2
<=> ! [X0] : ~ is_a_theorem(X0) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f28,plain,
( ! [X0] : ~ is_a_theorem(X0)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f27]) ).
fof(f29,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f22,f27,f24]) ).
fof(f30,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(X0,implies(implies(implies(implies(X1,X2),X3),X2),implies(X1,X2)))),
inference(resolution,[],[f16,f2]) ).
fof(f32,plain,
( $false
| ~ spl0_2 ),
inference(forward_subsumption_resolution,[],[f30,f28]) ).
fof(f33,plain,
~ spl0_2,
inference(avatar_contradiction_clause,[],[f32]) ).
fof(f35,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),X1),implies(X3,X1)))
| ~ spl0_1 ),
inference(resolution,[],[f25,f5]) ).
fof(f40,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(implies(implies(X1,X2),X3),X2),implies(X1,X2))) ),
inference(resolution,[],[f30,f1]) ).
fof(f42,definition,
( spl0_3
<=> ! [X2,X1,X3] : is_a_theorem(implies(implies(implies(implies(X1,X2),X3),X2),implies(X1,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f43,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(implies(implies(implies(X1,X2),X3),X2),implies(X1,X2)))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f42]) ).
fof(f44,plain,
( spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f40,f27,f42]) ).
fof(f46,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(implies(X0,X1),X2)),implies(X3,implies(implies(X0,X1),X2))))
| ~ spl0_3 ),
inference(resolution,[],[f43,f5]) ).
fof(f50,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(implies(X0,X1),X2)))
| is_a_theorem(implies(X3,implies(implies(X0,X1),X2))) )
| ~ spl0_3 ),
inference(resolution,[],[f46,f1]) ).
fof(f121,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(implies(X1,X2),X1),X1)))
| ~ spl0_3 ),
inference(resolution,[],[f50,f8]) ).
fof(f141,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(implies(X1,X2),X1),X1)) )
| ~ spl0_3 ),
inference(resolution,[],[f121,f1]) ).
fof(f143,definition,
( spl0_5
<=> ! [X2,X1] : is_a_theorem(implies(implies(implies(X1,X2),X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f144,plain,
( ! [X2,X1] : is_a_theorem(implies(implies(implies(X1,X2),X1),X1))
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f145,plain,
( spl0_5
| spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f141,f42,f27,f143]) ).
fof(f147,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X2,implies(X0,X1))))
| ~ spl0_5 ),
inference(resolution,[],[f144,f5]) ).
fof(f153,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,implies(X1,X2)),implies(X1,X2))))
| ~ spl0_3
| ~ spl0_5 ),
inference(resolution,[],[f147,f50]) ).
fof(f208,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2))) )
| ~ spl0_3
| ~ spl0_5 ),
inference(resolution,[],[f153,f1]) ).
fof(f210,definition,
( spl0_6
<=> ! [X2,X1] : is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f211,plain,
( ! [X2,X1] : is_a_theorem(implies(implies(X1,implies(X1,X2)),implies(X1,X2)))
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f212,plain,
( spl0_6
| spl0_2
| ~ spl0_3
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f208,f143,f42,f27,f210]) ).
fof(f215,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X0,X1)) )
| ~ spl0_6 ),
inference(resolution,[],[f211,f1]) ).
fof(f245,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),X1),X1))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f35,f215]) ).
fof(f294,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X3,implies(X2,X4))))
| is_a_theorem(implies(X5,implies(X3,implies(X2,X4)))) ),
inference(resolution,[],[f15,f1]) ).
fof(f297,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(X0,implies(implies(implies(X1,X2),X3),implies(X2,X3)))),
inference(resolution,[],[f294,f2]) ).
fof(f334,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(implies(X1,X2),X3),implies(X2,X3))) ),
inference(resolution,[],[f297,f1]) ).
fof(f336,definition,
( spl0_7
<=> ! [X2,X1,X3] : is_a_theorem(implies(implies(implies(X1,X2),X3),implies(X2,X3))) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f337,plain,
( ! [X2,X3,X1] : is_a_theorem(implies(implies(implies(X1,X2),X3),implies(X2,X3)))
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f338,plain,
( spl0_7
| spl0_2 ),
inference(avatar_split_clause,[],[f334,f27,f336]) ).
fof(f346,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X1,X2)) )
| ~ spl0_7 ),
inference(resolution,[],[f337,f1]) ).
fof(f347,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),implies(X2,X1))))
| ~ spl0_7 ),
inference(resolution,[],[f346,f2]) ).
fof(f385,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(implies(implies(X0,X1),X2),implies(X3,X2)),X0),implies(X4,X0)))
| ~ spl0_7 ),
inference(resolution,[],[f347,f5]) ).
fof(f1207,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,implies(X0,X2))),implies(X3,implies(X1,implies(X0,X2)))))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f245,f5]) ).
fof(f1240,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,implies(X0,X2))),implies(X1,implies(X0,X2))))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1207,f215]) ).
fof(f1274,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X0,X2))))
| is_a_theorem(implies(X1,implies(X0,X2))) )
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1240,f1]) ).
fof(f1275,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X1,X2),X0),X1)))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1274,f2]) ).
fof(f1305,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(implies(implies(X0,X1),X2),X0),X2),implies(X3,X2)))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1275,f5]) ).
fof(f1307,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(implies(X1,X2),X0),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1275,f1]) ).
fof(f1330,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(implies(X1,X2),X0))
| is_a_theorem(X1) )
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1307,f1]) ).
fof(f1337,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X1,X4),X0)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) )
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1330,f2]) ).
fof(f1586,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,X1),implies(implies(implies(X2,X3),X1),X2)),implies(X4,implies(implies(implies(X2,X3),X1),X2))))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1305,f5]) ).
fof(f1610,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(implies(implies(X1,X2),X3),X1)),implies(X4,X3)),implies(X5,implies(X4,X3))))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1586,f5]) ).
fof(f1689,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(implies(X2,X3),X1),X2)))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1610,f1337]) ).
fof(f1739,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(implies(implies(X2,X3),X1),X2)) )
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1689,f1]) ).
fof(f1746,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),X0),implies(implies(X0,X1),implies(X2,X1))))
| ~ spl0_1
| ~ spl0_6 ),
inference(resolution,[],[f1739,f2]) ).
fof(f2714,plain,
( ! [X2,X3,X0,X1,X4,X5] : is_a_theorem(implies(implies(implies(X0,X1),implies(implies(implies(X1,X2),X3),implies(X4,X3))),implies(X5,implies(implies(implies(X1,X2),X3),implies(X4,X3)))))
| ~ spl0_7 ),
inference(resolution,[],[f385,f5]) ).
fof(f4063,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] : is_a_theorem(implies(implies(implies(X0,implies(implies(implies(X1,X2),X3),implies(X4,X3))),implies(X5,X1)),implies(X6,implies(X5,X1))))
| ~ spl0_7 ),
inference(resolution,[],[f2714,f5]) ).
fof(f4082,plain,
( ! [X2,X3,X0,X1,X4] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X3)),implies(implies(implies(X1,X4),X3),implies(X2,X3))))
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4063,f1337]) ).
fof(f4157,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| is_a_theorem(implies(implies(implies(X1,X4),X3),implies(X2,X3))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4082,f1]) ).
fof(f4198,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X3)),implies(implies(X0,X3),implies(X2,X3))))
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4157,f1746]) ).
fof(f4215,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X3,X2)))
| ~ is_a_theorem(implies(X0,implies(X3,X2))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4157,f1307]) ).
fof(f4287,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))
| is_a_theorem(implies(implies(X0,X3),implies(X2,X3))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4198,f1]) ).
fof(f4451,plain,
( ! [X2,X3,X0,X1,X4] :
( is_a_theorem(implies(implies(implies(X1,X2),implies(X0,X3)),implies(X4,implies(X0,X3))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4215,f5]) ).
fof(f4711,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( is_a_theorem(implies(implies(implies(X3,implies(X0,X4)),implies(X1,X2)),implies(X5,implies(X1,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4451,f5]) ).
fof(f4924,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X1,X2),X3),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4711,f1337]) ).
fof(f5051,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X1,X2),X3))
| ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X0,X3)) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f4924,f1]) ).
fof(f5060,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X3)))
| is_a_theorem(implies(X0,implies(implies(X3,X1),implies(X4,X1)))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5051,f2]) ).
fof(f5097,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(implies(X1,X2),X3),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5051,f43]) ).
fof(f5117,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X1,X2))))
| is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5051,f211]) ).
fof(f5325,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X2,X0),X0)))
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5117,f2]) ).
fof(f5402,plain,
( ! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1)))
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5117,f347]) ).
fof(f5440,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X3)))
| is_a_theorem(implies(X0,implies(implies(X3,X1),X1))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5325,f5051]) ).
fof(f5545,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X0,X2),X1),X1)))
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5402,f4287]) ).
fof(f6270,plain,
( ! [X2,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X2),X1),X1))
| ~ is_a_theorem(implies(X0,X1)) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5545,f1]) ).
fof(f6592,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(implies(X0,X2),X1))
| is_a_theorem(X1) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f6270,f1]) ).
fof(f6666,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(implies(implies(X0,X1),X2),X3),implies(implies(X2,X0),implies(X4,X0))))
| is_a_theorem(implies(implies(X2,X0),implies(X4,X0))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f6592,f2]) ).
fof(f6787,plain,
( ! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(implies(X1,X3),X0)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f6666,f4451]) ).
fof(f6896,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(implies(X1,X0),implies(X1,X2))))
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f6787,f5545]) ).
fof(f6969,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(implies(X2,X1),implies(X2,X3))))
| ~ is_a_theorem(implies(X0,implies(X1,implies(X2,X3)))) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f6896,f5051]) ).
fof(f10981,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,implies(X0,X2)),implies(X0,X2))))
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5440,f5545]) ).
fof(f11250,plain,
( ! [X2,X3,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X0,X2),X1),implies(X3,X1))))
| ~ spl0_1
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f10981,f5060]) ).
fof(f11788,plain,
( ! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,implies(X2,X1))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f5097,f11250]) ).
fof(f11872,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(X1,implies(X3,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f11788,f5051]) ).
fof(f12529,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X1,implies(X0,X2))) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f11872,f1274]) ).
fof(f28369,plain,
( ! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X2,X1),implies(X0,implies(X2,X3))))
| ~ is_a_theorem(implies(X0,implies(X1,implies(X2,X3)))) )
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f6969,f12529]) ).
fof(f28415,plain,
( ~ is_a_theorem(implies(implies(b,c),implies(b,implies(a,c))))
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(resolution,[],[f28369,f4]) ).
fof(f28528,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f28415,f11788]) ).
fof(f28529,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f28528]) ).
cnf(s1,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f29]) ).
cnf(s2,plain,
~ spl0_2,
inference(sat_conversion,[],[f33]) ).
cnf(s3,plain,
( spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f44]) ).
cnf(s5,plain,
( spl0_2
| ~ spl0_3
| spl0_5 ),
inference(sat_conversion,[],[f145]) ).
cnf(s6,plain,
( spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f212]) ).
cnf(s7,plain,
( spl0_2
| spl0_7 ),
inference(sat_conversion,[],[f338]) ).
cnf(s27,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_6
| ~ spl0_7 ),
inference(sat_conversion,[],[f28529]) ).
cnf(s28,plain,
spl0_7,
inference(rat,[],[s7,s2]) ).
cnf(s30,plain,
spl0_3,
inference(rat,[],[s3,s2]) ).
cnf(s31,plain,
spl0_5,
inference(rat,[],[s5,s2,s30]) ).
cnf(s32,plain,
spl0_6,
inference(rat,[],[s6,s30,s2,s31]) ).
cnf(s33,plain,
~ spl0_1,
inference(rat,[],[s27,s28,s30,s32]) ).
cnf(s34,plain,
$false,
inference(rat,[],[s1,s2,s33]) ).
fof(f28530,plain,
$false,
inference(avatar_sat_refutation,[],[s34]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL084-2 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n013.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 15:20:36 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 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
% 14.71/3.02 % (340936)Input is clausal, will run a generic CNF schedule.
% 14.71/3.02 % (341046)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2245721177:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 14.71/3.02 % (341043)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4010815860:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 14.71/3.02 % (341042)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=1889484316:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 14.71/3.02 % (341045)lrs+10_1_sil=8000:sp=occurrence:random_seed=820003549:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 14.71/3.02 % (341044)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1185088484:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 14.71/3.02 % (341047)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1003362109:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 14.71/3.02 % (341046)Instruction limit reached!
% 14.71/3.02 % (341046)------------------------------
% 14.71/3.02 % (341046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.71/3.02 % (341046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/3.02 % (341046)CaDiCaL version: 2.1.3
% 14.71/3.02 % (341046)Termination reason: Instruction limit
% 14.71/3.02 % (341046)Termination phase: Saturation
% 14.71/3.02 % (341046)Time elapsed: 0.040 s
% 14.71/3.02 % (341046)Peak memory usage: 88 MB
% 14.71/3.02 % (341046)Instructions burned: 117 (million)
% 14.71/3.02 % (341048)dis-21_1_sil=8000:lcm=predicate:random_seed=1258074254: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)
% 14.71/3.02 % (341045)Instruction limit reached!
% 14.71/3.02 % (341045)------------------------------
% 14.71/3.02 % (341045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.71/3.02 % (341045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/3.02 % (341045)CaDiCaL version: 2.1.3
% 14.71/3.02 % (341045)Termination reason: Instruction limit
% 14.71/3.02 % (341045)Termination phase: Saturation
% 14.71/3.02 % (341045)Time elapsed: 0.066 s
% 14.71/3.02 % (341045)Peak memory usage: 88 MB
% 14.71/3.02 % (341045)Instructions burned: 107 (million)
% 14.71/3.02 % (341048)Instruction limit reached!
% 14.71/3.02 % (341048)------------------------------
% 14.71/3.02 % (341048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.71/3.02 % (341048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/3.02 % (341048)CaDiCaL version: 2.1.3
% 14.71/3.02 % (341048)Termination reason: Instruction limit
% 14.71/3.02 % (341048)Termination phase: Saturation
% 14.71/3.02 % (341048)Time elapsed: 0.069 s
% 14.71/3.02 % (341048)Peak memory usage: 88 MB
% 14.71/3.02 % (341048)Instructions burned: 118 (million)
% 14.71/3.02 % (341047)Instruction limit reached!
% 14.71/3.02 % (341047)------------------------------
% 14.71/3.02 % (341047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.71/3.02 % (341047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/3.02 % (341047)CaDiCaL version: 2.1.3
% 14.71/3.02 % (341047)Termination reason: Instruction limit
% 14.71/3.02 % (341047)Termination phase: Saturation
% 14.71/3.02 % (341047)Time elapsed: 0.130 s
% 14.71/3.02 % (341047)Peak memory usage: 89 MB
% 14.71/3.02 % (341047)Instructions burned: 181 (million)
% 14.71/3.02 % (341059)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=904149301:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 14.71/3.02 % (341059)Refutation not found, incomplete strategy
% 14.71/3.02 % (341059)------------------------------
% 14.71/3.02 % (341059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.71/3.02 % (341059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.71/3.02 % (341059)CaDiCaL version: 2.1.3
% 14.71/3.02 % (341059)Termination reason: Refutation not found, incomplete strategy
% 14.71/3.02 % (341059)Time elapsed: 0.001 s
% 14.71/3.02 % (341059)Peak memory usage: 87 MB
% 14.71/3.02 % (341070)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2326865489:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 26.11/4.58 % (341071)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3477838737:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 26.11/4.58 % (341071)Refutation not found, incomplete strategy
% 26.11/4.58 % (341071)------------------------------
% 26.11/4.58 % (341071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/4.58 % (341071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.58 % (341071)CaDiCaL version: 2.1.3
% 26.11/4.58 % (341071)Termination reason: Refutation not found, incomplete strategy
% 26.11/4.58 % (341071)Time elapsed: 0.001 s
% 26.11/4.58 % (341071)Peak memory usage: 87 MB
% 26.11/4.58 % (341072)lrs+10_64_to=lpo:sil=8000:random_seed=349562259:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 26.11/4.58 % (341070)Instruction limit reached!
% 26.11/4.58 % (341070)------------------------------
% 26.11/4.58 % (341070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/4.58 % (341070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.58 % (341070)CaDiCaL version: 2.1.3
% 26.11/4.58 % (341070)Termination reason: Instruction limit
% 26.11/4.58 % (341070)Termination phase: Saturation
% 26.11/4.58 % (341070)Time elapsed: 0.110 s
% 26.11/4.58 % (341070)Peak memory usage: 89 MB
% 26.11/4.58 % (341070)Instructions burned: 190 (million)
% 26.11/4.58 % (341072)Instruction limit reached!
% 26.11/4.58 % (341072)------------------------------
% 26.11/4.58 % (341072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/4.58 % (341072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.58 % (341072)CaDiCaL version: 2.1.3
% 26.11/4.58 % (341072)Termination reason: Instruction limit
% 26.11/4.58 % (341072)Termination phase: Saturation
% 26.11/4.58 % (341072)Time elapsed: 0.072 s
% 26.11/4.58 % (341072)Peak memory usage: 88 MB
% 26.11/4.58 % (341072)Instructions burned: 127 (million)
% 26.11/4.58 % (341059)------------------------------
% 26.11/4.58 % (341059)------------------------------
% 26.11/4.58 % (341071)------------------------------
% 26.11/4.58 % (341071)------------------------------
% 26.11/4.58 % (341077)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2146932298:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 26.11/4.58 % (341078)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2729461502:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 26.11/4.58 % (341089)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=905822633:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 26.11/4.58 % (341087)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1218679725:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 26.11/4.58 % (341077)Instruction limit reached!
% 26.11/4.58 % (341077)------------------------------
% 26.11/4.58 % (341077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/4.58 % (341077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.58 % (341077)CaDiCaL version: 2.1.3
% 26.11/4.58 % (341077)Termination reason: Instruction limit
% 26.11/4.58 % (341077)Termination phase: Saturation
% 26.11/4.58 % (341077)Time elapsed: 0.213 s
% 26.11/4.58 % (341077)Peak memory usage: 89 MB
% 26.11/4.58 % (341077)Instructions burned: 195 (million)
% 26.11/4.58 % (341078)Instruction limit reached!
% 26.11/4.58 % (341078)------------------------------
% 26.11/4.58 % (341078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/4.58 % (341078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.58 % (341078)CaDiCaL version: 2.1.3
% 26.11/4.58 % (341078)Termination reason: Instruction limit
% 26.11/4.58 % (341078)Termination phase: Saturation
% 26.11/4.58 % (341078)Time elapsed: 0.175 s
% 26.11/4.58 % (341078)Peak memory usage: 90 MB
% 26.11/4.58 % (341078)Instructions burned: 157 (million)
% 26.11/4.58 % (341089)Instruction limit reached!
% 26.11/4.58 % (341089)------------------------------
% 26.11/4.58 % (341089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/4.58 % (341089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/4.58 % (341089)CaDiCaL version: 2.1.3
% 26.11/4.58 % (341089)Termination reason: Instruction limit
% 45.36/7.28 % (341089)Termination phase: Saturation
% 45.36/7.28 % (341089)Time elapsed: 0.100 s
% 45.36/7.28 % (341089)Peak memory usage: 88 MB
% 45.36/7.28 % (341089)Instructions burned: 106 (million)
% 45.36/7.28 % (341102)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=776264008:i=107_2990 on theBenchmark for (2990ds/107Mi)
% 45.36/7.28 % (341102)Refutation not found, incomplete strategy
% 45.36/7.28 % (341102)------------------------------
% 45.36/7.28 % (341102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.28 % (341102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.28 % (341102)CaDiCaL version: 2.1.3
% 45.36/7.28 % (341102)Termination reason: Refutation not found, incomplete strategy
% 45.36/7.28 % (341102)Time elapsed: 0.001 s
% 45.36/7.28 % (341102)Peak memory usage: 86 MB
% 45.36/7.28 % (341104)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2387397599:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 45.36/7.28 % (341103)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3808341212:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 45.36/7.28 % (341103)Instruction limit reached!
% 45.36/7.28 % (341103)------------------------------
% 45.36/7.28 % (341103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.28 % (341103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.28 % (341103)CaDiCaL version: 2.1.3
% 45.36/7.28 % (341103)Termination reason: Instruction limit
% 45.36/7.28 % (341103)Termination phase: Saturation
% 45.36/7.28 % (341103)Time elapsed: 0.159 s
% 45.36/7.28 % (341103)Peak memory usage: 90 MB
% 45.36/7.28 % (341103)Instructions burned: 243 (million)
% 45.36/7.28 % (341102)------------------------------
% 45.36/7.28 % (341102)------------------------------
% 45.36/7.28 % (341109)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2664964747:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi)
% 45.36/7.28 % (341109)Instruction limit reached!
% 45.36/7.28 % (341109)------------------------------
% 45.36/7.28 % (341109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.28 % (341109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.28 % (341109)CaDiCaL version: 2.1.3
% 45.36/7.28 % (341109)Termination reason: Instruction limit
% 45.36/7.28 % (341109)Termination phase: Saturation
% 45.36/7.28 % (341109)Time elapsed: 0.087 s
% 45.36/7.28 % (341109)Peak memory usage: 89 MB
% 45.36/7.28 % (341109)Instructions burned: 135 (million)
% 45.36/7.28 % (341111)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=382712807:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 45.36/7.28 % (341113)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3612089812:i=191:fgj=on:bd=all_2983 on theBenchmark for (2983ds/191Mi)
% 45.36/7.28 % (341113)Instruction limit reached!
% 45.36/7.28 % (341113)------------------------------
% 45.36/7.28 % (341113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.28 % (341113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.28 % (341113)CaDiCaL version: 2.1.3
% 45.36/7.28 % (341113)Termination reason: Instruction limit
% 45.36/7.28 % (341113)Termination phase: Saturation
% 45.36/7.28 % (341113)Time elapsed: 0.117 s
% 45.36/7.28 % (341113)Peak memory usage: 90 MB
% 45.36/7.28 % (341113)Instructions burned: 192 (million)
% 45.36/7.28 % (341111)Instruction limit reached!
% 45.36/7.28 % (341111)------------------------------
% 45.36/7.28 % (341111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.36/7.28 % (341111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.36/7.28 % (341111)CaDiCaL version: 2.1.3
% 45.36/7.28 % (341111)Termination reason: Instruction limit
% 45.36/7.28 % (341111)Termination phase: Saturation
% 45.36/7.28 % (341111)Time elapsed: 0.293 s
% 45.36/7.28 % (341111)Peak memory usage: 91 MB
% 45.36/7.28 % (341111)Instructions burned: 500 (million)
% 45.36/7.28 % (341216)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1592024407:i=264:kws=precedence:fsr=off_2980 on theBenchmark for (2980ds/264Mi)
% 45.36/7.28 % (341222)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1858274897:cond=on:i=156:bs=on:gtg=exists_all:er=known_2979 on theBenchmark for (2979ds/156Mi)
% 62.53/9.83 % (341216)Instruction limit reached!
% 62.53/9.83 % (341216)------------------------------
% 62.53/9.83 % (341216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.53/9.83 % (341216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.53/9.83 % (341216)CaDiCaL version: 2.1.3
% 62.53/9.83 % (341216)Termination reason: Instruction limit
% 62.53/9.83 % (341216)Termination phase: Saturation
% 62.53/9.83 % (341216)Time elapsed: 0.165 s
% 62.53/9.83 % (341216)Peak memory usage: 90 MB
% 62.53/9.83 % (341216)Instructions burned: 264 (million)
% 62.53/9.83 % (341222)Instruction limit reached!
% 62.53/9.83 % (341222)------------------------------
% 62.53/9.83 % (341222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.53/9.83 % (341222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.53/9.83 % (341222)CaDiCaL version: 2.1.3
% 62.53/9.83 % (341222)Termination reason: Instruction limit
% 62.53/9.83 % (341222)Termination phase: Saturation
% 62.53/9.83 % (341222)Time elapsed: 0.100 s
% 62.53/9.83 % (341222)Peak memory usage: 88 MB
% 62.53/9.83 % (341222)Instructions burned: 157 (million)
% 62.53/9.83 % (341272)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=1847168160:i=3256:kws=precedence:bd=preordered:av=off_2977 on theBenchmark for (2977ds/3256Mi)
% 62.53/9.83 % (341273)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1469324417:i=537:av=off:ss=included_2977 on theBenchmark for (2977ds/537Mi)
% 62.53/9.83 % (341273)Instruction limit reached!
% 62.53/9.83 % (341273)------------------------------
% 62.53/9.83 % (341273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.53/9.83 % (341273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.53/9.83 % (341273)CaDiCaL version: 2.1.3
% 62.53/9.83 % (341273)Termination reason: Instruction limit
% 62.53/9.83 % (341273)Termination phase: Saturation
% 62.53/9.83 % (341273)Time elapsed: 0.316 s
% 62.53/9.83 % (341273)Peak memory usage: 91 MB
% 62.53/9.83 % (341273)Instructions burned: 539 (million)
% 62.53/9.83 % (341277)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1339481653:i=180:bd=preordered:av=off_2972 on theBenchmark for (2972ds/180Mi)
% 62.53/9.83 % (341277)Instruction limit reached!
% 62.53/9.83 % (341277)------------------------------
% 62.53/9.83 % (341277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.53/9.83 % (341277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.53/9.83 % (341277)CaDiCaL version: 2.1.3
% 62.53/9.83 % (341277)Termination reason: Instruction limit
% 62.53/9.83 % (341277)Termination phase: Saturation
% 62.53/9.83 % (341277)Time elapsed: 0.104 s
% 62.53/9.83 % (341277)Peak memory usage: 88 MB
% 62.53/9.83 % (341277)Instructions burned: 181 (million)
% 62.53/9.83 % (341087)Instruction limit reached!
% 62.53/9.83 % (341087)------------------------------
% 62.53/9.83 % (341087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.53/9.83 % (341087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.53/9.83 % (341087)CaDiCaL version: 2.1.3
% 62.53/9.83 % (341087)Termination reason: Instruction limit
% 62.53/9.83 % (341087)Termination phase: Saturation
% 62.53/9.83 % (341087)Time elapsed: 2.252 s
% 62.53/9.83 % (341087)Peak memory usage: 149 MB
% 62.53/9.83 % (341087)Instructions burned: 3395 (million)
% 62.53/9.83 % (341279)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=3707627850:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/10307Mi)
% 62.53/9.83 % (341280)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=2154199470:i=412:gtgl=4:gtg=exists_all_2968 on theBenchmark for (2968ds/412Mi)
% 62.53/9.83 % (341280)Instruction limit reached!
% 62.53/9.83 % (341280)------------------------------
% 62.53/9.83 % (341280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 62.53/9.83 % (341280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.53/9.83 % (341280)CaDiCaL version: 2.1.3
% 62.53/9.83 % (341280)Termination reason: Instruction limit
% 62.53/9.83 % (341280)Termination phase: Saturation
% 62.53/9.83 % (341280)Time elapsed: 0.249 s
% 62.53/9.83 % (341280)Peak memory usage: 94 MB
% 62.53/9.83 % (341280)Instructions burned: 414 (million)
% 85.24/12.99 % (341283)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=638900736:s2pl=no:i=8478:s2at=4:nm=6_2964 on theBenchmark for (2964ds/8478Mi)
% 85.24/12.99 % (341272)Instruction limit reached!
% 85.24/12.99 % (341272)------------------------------
% 85.24/12.99 % (341272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.24/12.99 % (341272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.24/12.99 % (341272)CaDiCaL version: 2.1.3
% 85.24/12.99 % (341272)Termination reason: Instruction limit
% 85.24/12.99 % (341272)Termination phase: Saturation
% 85.24/12.99 % (341272)Time elapsed: 1.742 s
% 85.24/12.99 % (341272)Peak memory usage: 136 MB
% 85.24/12.99 % (341272)Instructions burned: 3257 (million)
% 85.24/12.99 % (341285)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=2648170870:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2958 on theBenchmark for (2958ds/303Mi)
% 85.24/12.99 % (341104)Instruction limit reached!
% 85.24/12.99 % (341104)------------------------------
% 85.24/12.99 % (341104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.24/12.99 % (341104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.24/12.99 % (341104)CaDiCaL version: 2.1.3
% 85.24/12.99 % (341104)Termination reason: Instruction limit
% 85.24/12.99 % (341104)Termination phase: Saturation
% 85.24/12.99 % (341104)Time elapsed: 3.124 s
% 85.24/12.99 % (341104)Peak memory usage: 161 MB
% 85.24/12.99 % (341104)Instructions burned: 5209 (million)
% 85.24/12.99 % (341285)Instruction limit reached!
% 85.24/12.99 % (341285)------------------------------
% 85.24/12.99 % (341285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.24/12.99 % (341285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.24/12.99 % (341285)CaDiCaL version: 2.1.3
% 85.24/12.99 % (341285)Termination reason: Instruction limit
% 85.24/12.99 % (341285)Termination phase: Saturation
% 85.24/12.99 % (341285)Time elapsed: 0.159 s
% 85.24/12.99 % (341285)Peak memory usage: 90 MB
% 85.24/12.99 % (341285)Instructions burned: 304 (million)
% 85.24/12.99 % (341287)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3383224829:st=4:i=720:sd=3:fsr=off:ss=axioms_2956 on theBenchmark for (2956ds/720Mi)
% 85.24/12.99 % (341288)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3982174150:i=598:bs=on:bd=preordered:av=off:ss=axioms_2955 on theBenchmark for (2955ds/598Mi)
% 85.24/12.99 % (341287)Instruction limit reached!
% 85.24/12.99 % (341287)------------------------------
% 85.24/12.99 % (341287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.24/12.99 % (341287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.24/12.99 % (341287)CaDiCaL version: 2.1.3
% 85.24/12.99 % (341287)Termination reason: Instruction limit
% 85.24/12.99 % (341287)Termination phase: Saturation
% 85.24/12.99 % (341287)Time elapsed: 0.416 s
% 85.24/12.99 % (341287)Peak memory usage: 94 MB
% 85.24/12.99 % (341287)Instructions burned: 720 (million)
% 85.24/12.99 % (341288)Instruction limit reached!
% 85.24/12.99 % (341288)------------------------------
% 85.24/12.99 % (341288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.24/12.99 % (341288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.24/12.99 % (341288)CaDiCaL version: 2.1.3
% 85.24/12.99 % (341288)Termination reason: Instruction limit
% 85.24/12.99 % (341288)Termination phase: Saturation
% 85.24/12.99 % (341288)Time elapsed: 0.322 s
% 85.24/12.99 % (341288)Peak memory usage: 94 MB
% 85.24/12.99 % (341288)Instructions burned: 598 (million)
% 85.24/12.99 % (341291)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4084779459:i=2989:sd=3:ss=axioms:sgt=60_2950 on theBenchmark for (2950ds/2989Mi)
% 85.24/12.99 % (341292)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=239411307:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2950 on theBenchmark for (2950ds/1997Mi)
% 85.24/12.99 % (341292)Instruction limit reached!
% 85.24/12.99 % (341292)------------------------------
% 85.24/12.99 % (341292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 85.24/12.99 % (341292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341292)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341292)Termination reason: Instruction limit
% 94.98/14.28 % (341292)Termination phase: Saturation
% 94.98/14.28 % (341292)Time elapsed: 1.308 s
% 94.98/14.28 % (341292)Peak memory usage: 133 MB
% 94.98/14.28 % (341292)Instructions burned: 1997 (million)
% 94.98/14.28 % (341295)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=1491166732:i=2088:bd=preordered:av=off_2935 on theBenchmark for (2935ds/2088Mi)
% 94.98/14.28 % (341291)Instruction limit reached!
% 94.98/14.28 % (341291)------------------------------
% 94.98/14.28 % (341291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341291)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341291)Termination reason: Instruction limit
% 94.98/14.28 % (341291)Termination phase: Saturation
% 94.98/14.28 % (341291)Time elapsed: 1.836 s
% 94.98/14.28 % (341291)Peak memory usage: 147 MB
% 94.98/14.28 % (341291)Instructions burned: 2990 (million)
% 94.98/14.28 % (341297)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1017745540:i=1098:nicw=on_2930 on theBenchmark for (2930ds/1098Mi)
% 94.98/14.28 % (341297)Instruction limit reached!
% 94.98/14.28 % (341297)------------------------------
% 94.98/14.28 % (341297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341297)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341297)Termination reason: Instruction limit
% 94.98/14.28 % (341297)Termination phase: Saturation
% 94.98/14.28 % (341297)Time elapsed: 0.600 s
% 94.98/14.28 % (341297)Peak memory usage: 93 MB
% 94.98/14.28 % (341297)Instructions burned: 1098 (million)
% 94.98/14.28 % (341295)Instruction limit reached!
% 94.98/14.28 % (341295)------------------------------
% 94.98/14.28 % (341295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341295)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341295)Termination reason: Instruction limit
% 94.98/14.28 % (341295)Termination phase: Saturation
% 94.98/14.28 % (341295)Time elapsed: 1.233 s
% 94.98/14.28 % (341295)Peak memory usage: 130 MB
% 94.98/14.28 % (341295)Instructions burned: 2088 (million)
% 94.98/14.28 % (341299)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4051814420:i=433:bd=preordered_2922 on theBenchmark for (2922ds/433Mi)
% 94.98/14.28 % (341300)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2198891971:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2921 on theBenchmark for (2921ds/2942Mi)
% 94.98/14.28 % (341299)Instruction limit reached!
% 94.98/14.28 % (341299)------------------------------
% 94.98/14.28 % (341299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341299)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341299)Termination reason: Instruction limit
% 94.98/14.28 % (341299)Termination phase: Saturation
% 94.98/14.28 % (341299)Time elapsed: 0.277 s
% 94.98/14.28 % (341299)Peak memory usage: 93 MB
% 94.98/14.28 % (341299)Instructions burned: 439 (million)
% 94.98/14.28 % (341303)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1571128177:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2918 on theBenchmark for (2918ds/6922Mi)
% 94.98/14.28 % (341283)Instruction limit reached!
% 94.98/14.28 % (341283)------------------------------
% 94.98/14.28 % (341283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341283)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341283)Termination reason: Instruction limit
% 94.98/14.28 % (341283)Termination phase: Saturation
% 94.98/14.28 % (341283)Time elapsed: 4.742 s
% 94.98/14.28 % (341283)Peak memory usage: 194 MB
% 94.98/14.28 % (341283)Instructions burned: 8479 (million)
% 94.98/14.28 % (341305)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=4066546751:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2915 on theBenchmark for (2915ds/596Mi)
% 94.98/14.28 % (341305)Instruction limit reached!
% 94.98/14.28 % (341305)------------------------------
% 94.98/14.28 % (341305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341305)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341305)Termination reason: Instruction limit
% 94.98/14.28 % (341305)Termination phase: Saturation
% 94.98/14.28 % (341305)Time elapsed: 0.338 s
% 94.98/14.28 % (341305)Peak memory usage: 98 MB
% 94.98/14.28 % (341305)Instructions burned: 598 (million)
% 94.98/14.28 % (341307)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=2298537177:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2910 on theBenchmark for (2910ds/4123Mi)
% 94.98/14.28 % (341279)Instruction limit reached!
% 94.98/14.28 % (341279)------------------------------
% 94.98/14.28 % (341279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341279)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341279)Termination reason: Instruction limit
% 94.98/14.28 % (341279)Termination phase: Saturation
% 94.98/14.28 % (341279)Time elapsed: 6.488 s
% 94.98/14.28 % (341279)Peak memory usage: 185 MB
% 94.98/14.28 % (341279)Instructions burned: 10308 (million)
% 94.98/14.28 % (341309)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3182741021:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2903 on theBenchmark for (2903ds/16411Mi)
% 94.98/14.28 % (341300)Instruction limit reached!
% 94.98/14.28 % (341300)------------------------------
% 94.98/14.28 % (341300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341300)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341300)Termination reason: Instruction limit
% 94.98/14.28 % (341300)Termination phase: Saturation
% 94.98/14.28 % (341300)Time elapsed: 1.886 s
% 94.98/14.28 % (341300)Peak memory usage: 140 MB
% 94.98/14.28 % (341300)Instructions burned: 2942 (million)
% 94.98/14.28 % (341311)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1342106616:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2901 on theBenchmark for (2901ds/1670Mi)
% 94.98/14.28 % (341311)Instruction limit reached!
% 94.98/14.28 % (341311)------------------------------
% 94.98/14.28 % (341311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341311)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341311)Termination reason: Instruction limit
% 94.98/14.28 % (341311)Termination phase: Saturation
% 94.98/14.28 % (341311)Time elapsed: 1.025 s
% 94.98/14.28 % (341311)Peak memory usage: 136 MB
% 94.98/14.28 % (341311)Instructions burned: 1671 (million)
% 94.98/14.28 % (341313)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=2105546012:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2889 on theBenchmark for (2889ds/1722Mi)
% 94.98/14.28 % (341307)Instruction limit reached!
% 94.98/14.28 % (341307)------------------------------
% 94.98/14.28 % (341307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341307)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341307)Termination reason: Instruction limit
% 94.98/14.28 % (341307)Termination phase: Saturation
% 94.98/14.28 % (341307)Time elapsed: 2.332 s
% 94.98/14.28 % (341307)Peak memory usage: 154 MB
% 94.98/14.28 % (341307)Instructions burned: 4124 (million)
% 94.98/14.28 % (341315)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=3240683801:cts=off:cond=on:i=9530:bs=on:fsd=on_2885 on theBenchmark for (2885ds/9530Mi)
% 94.98/14.28 % (341303)Instruction limit reached!
% 94.98/14.28 % (341303)------------------------------
% 94.98/14.28 % (341303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341303)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341303)Termination reason: Instruction limit
% 94.98/14.28 % (341303)Termination phase: Saturation
% 94.98/14.28 % (341303)Time elapsed: 3.825 s
% 94.98/14.28 % (341303)Peak memory usage: 174 MB
% 94.98/14.28 % (341303)Instructions burned: 6922 (million)
% 94.98/14.28 % (341317)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1973618269:st=2:i=4495:sd=10:ss=included_2878 on theBenchmark for (2878ds/4495Mi)
% 94.98/14.28 % (341313)Instruction limit reached!
% 94.98/14.28 % (341313)------------------------------
% 94.98/14.28 % (341313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.98/14.28 % (341313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.98/14.28 % (341313)CaDiCaL version: 2.1.3
% 94.98/14.28 % (341313)Termination reason: Instruction limit
% 94.98/14.28 % (341313)Termination phase: Saturation
% 94.98/14.28 % (341313)Time elapsed: 1.231 s
% 94.98/14.28 % (341313)Peak memory usage: 134 MB
% 94.98/14.28 % (341313)Instructions burned: 1723 (million)
% 94.98/14.28 % (341319)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=1900885821:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2874 on theBenchmark for (2874ds/4920Mi)
% 94.98/14.28 % (341309)First to succeed.
% 94.98/14.28 % (341309)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-340936"
% 94.98/14.28 % (341309)Refutation found. Thanks to Tanya!
% 94.98/14.28 % SZS status Unsatisfiable for theBenchmark
% 94.98/14.28 % SZS output start Proof for theBenchmark
% See solution above
% 95.60/14.47 % (341309)------------------------------
% 95.60/14.47 % (341309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.60/14.47 % (341309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.60/14.47 % (341309)CaDiCaL version: 2.1.3
% 95.60/14.47 % (341309)Termination reason: Refutation
% 95.60/14.47 % (341309)Time elapsed: 3.304 s
% 95.60/14.47 % (341309)Peak memory usage: 169 MB
% 95.60/14.47 % (341309)Instructions burned: 5487 (million)
% 95.60/14.47 % (341309)------------------------------
% 95.60/14.47 % (341309)------------------------------
% 95.60/14.47 % (340936)Success in time 13.427 s
% 95.60/14.47 % Vampire exiting
%------------------------------------------------------------------------------