%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL377-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:11 AM UTC 2026
% Result : Unsatisfiable 27.91s 5.03s
% Output : Refutation 29.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 11
% Syntax : Number of formulae : 109 ( 52 unt; 6 def)
% Number of atoms : 182 ( 12 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 149 ( 76 ~; 73 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 202 ( 202 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f2,axiom,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_1) ).
fof(f3,axiom,
! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_2) ).
fof(f4,axiom,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cn_3) ).
fof(f5,negated_conjecture,
~ is_a_theorem(implies(implies(x,implies(y,implies(z,u))),implies(implies(z,x),implies(y,implies(z,u))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cn_34) ).
fof(f6,definition,
sF0 = implies(z,u),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f7,plain,
implies(z,u) = sF0,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF1 = implies(y,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f9,plain,
implies(y,sF0) = sF1,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF2 = implies(x,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f11,plain,
implies(x,sF1) = sF2,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF3 = implies(z,x),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f13,plain,
implies(z,x) = sF3,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF4 = implies(sF3,sF1),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f15,plain,
implies(sF3,sF1) = sF4,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF5 = implies(sF2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f17,plain,
implies(sF2,sF4) = sF5,
inference(reorient_equations,[],[f16]) ).
fof(f18,plain,
~ is_a_theorem(sF5),
inference(definition_folding,[],[f5,f17,f15,f9,f7,f13,f11,f9,f7]) ).
fof(f19,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,X2),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f1,f2]) ).
fof(f24,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f19,f1]) ).
fof(f27,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(implies(X2,X3),implies(X1,X3))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f24,f2]) ).
fof(f28,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X0,implies(X3,X2)))
| ~ is_a_theorem(implies(X3,X1)) ),
inference(resolution,[],[f24,f19]) ).
fof(f44,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X2,implies(X0,X3))))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) ),
inference(resolution,[],[f28,f2]) ).
fof(f50,plain,
! [X2,X3,X0,X1,X4] :
( is_a_theorem(implies(X3,implies(X0,implies(X4,X2))))
| ~ is_a_theorem(implies(X3,implies(X4,X1)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f44,f24]) ).
fof(f105,plain,
! [X0,X1] :
( is_a_theorem(implies(not(X0),X1))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f4,f1]) ).
fof(f115,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(not(X1),X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f3,f24]) ).
fof(f118,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,X1),X1))
| ~ is_a_theorem(implies(not(X1),X0)) ),
inference(resolution,[],[f115,f19]) ).
fof(f120,plain,
! [X0] : is_a_theorem(implies(X0,X0)),
inference(resolution,[],[f115,f4]) ).
fof(f121,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(not(implies(X1,X2)),implies(X3,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X3)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f115,f50]) ).
fof(f213,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(X0,X3)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X2,implies(X0,X1))) ),
inference(resolution,[],[f105,f121]) ).
fof(f221,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(not(X0),X1))
| ~ is_a_theorem(implies(X1,X0))
| is_a_theorem(X0) ),
inference(resolution,[],[f118,f1]) ).
fof(f254,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(X2,implies(X3,X4)))
| is_a_theorem(implies(X2,implies(X0,X1)))
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X0,implies(X4,X5))) ),
inference(resolution,[],[f213,f50]) ).
fof(f298,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(X1,implies(X3,X4)))
| ~ is_a_theorem(implies(X1,X2))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f254,f4]) ).
fof(f319,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(X2,implies(X0,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f298,f4]) ).
fof(f341,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(X3,X0)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X2,implies(X3,X1))) ),
inference(resolution,[],[f319,f121]) ).
fof(f358,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X3),implies(implies(X3,X1),X2)))
| ~ is_a_theorem(implies(implies(X0,X1),X2)) ),
inference(resolution,[],[f341,f2]) ).
fof(f368,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X3,implies(X4,X2)))
| ~ is_a_theorem(implies(X3,implies(X0,X5)))
| ~ is_a_theorem(implies(X4,implies(X5,X1))) ),
inference(resolution,[],[f341,f50]) ).
fof(f415,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(not(X2),X3)))
| is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X1,implies(X3,X2))) ),
inference(resolution,[],[f368,f3]) ).
fof(f432,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(implies(X0,X3))
| is_a_theorem(implies(implies(X3,X1),X2)) ),
inference(resolution,[],[f358,f1]) ).
fof(f478,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X2,X0)))
| is_a_theorem(implies(X0,implies(X1,X0))) ),
inference(resolution,[],[f415,f4]) ).
fof(f496,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
inference(resolution,[],[f478,f4]) ).
fof(f517,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f496,f415]) ).
fof(f525,plain,
is_a_theorem(implies(sF0,sF1)),
inference(superposition,[],[f496,f9]) ).
fof(f560,plain,
! [X0,X1] : is_a_theorem(implies(not(X0),implies(X0,X1))),
inference(resolution,[],[f517,f4]) ).
fof(f563,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X1))),
inference(resolution,[],[f517,f496]) ).
fof(f565,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),X1))),
inference(resolution,[],[f517,f120]) ).
fof(f588,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X0),X1))
| is_a_theorem(X1) ),
inference(resolution,[],[f563,f221]) ).
fof(f592,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| is_a_theorem(X0) ),
inference(resolution,[],[f560,f221]) ).
fof(f642,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X3,X3),implies(X2,X0)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) ),
inference(resolution,[],[f588,f27]) ).
fof(f709,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))),
inference(resolution,[],[f642,f496]) ).
fof(f740,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X1),X2)))
| is_a_theorem(implies(X0,implies(X3,X2))) ),
inference(resolution,[],[f709,f24]) ).
fof(f763,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X2)))),
inference(resolution,[],[f740,f563]) ).
fof(f783,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(implies(X3,X3),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f763,f415]) ).
fof(f792,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X1)),X2))
| is_a_theorem(X2) ),
inference(resolution,[],[f763,f221]) ).
fof(f1460,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X0),X1),X2))
| ~ is_a_theorem(implies(implies(X3,X1),X2)) ),
inference(resolution,[],[f792,f358]) ).
fof(f1498,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(X3,implies(implies(X4,X4),X1)))
| ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X3,X2)) ),
inference(resolution,[],[f1460,f24]) ).
fof(f1539,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f1498,f496]) ).
fof(f1562,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,X1),implies(X2,X1)))),
inference(resolution,[],[f1539,f2]) ).
fof(f1584,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X0)))),
inference(resolution,[],[f1539,f496]) ).
fof(f1602,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X1)))),
inference(resolution,[],[f1562,f783]) ).
fof(f1613,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,implies(X2,X1)))),
inference(resolution,[],[f1562,f517]) ).
fof(f1647,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X3,implies(X1,X2))) ),
inference(resolution,[],[f1602,f341]) ).
fof(f1663,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X0)),X2))
| is_a_theorem(X2) ),
inference(resolution,[],[f1602,f221]) ).
fof(f1665,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),
inference(resolution,[],[f1602,f642]) ).
fof(f1717,plain,
! [X0] : is_a_theorem(implies(sF4,implies(X0,sF5))),
inference(superposition,[],[f1584,f17]) ).
fof(f1853,plain,
! [X0] : is_a_theorem(implies(implies(X0,sF1),implies(X0,sF4))),
inference(superposition,[],[f1613,f15]) ).
fof(f2142,plain,
is_a_theorem(implies(implies(sF2,sF1),sF5)),
inference(superposition,[],[f1853,f17]) ).
fof(f2143,plain,
! [X0] : is_a_theorem(implies(X0,implies(sF1,sF5))),
inference(resolution,[],[f2142,f1647]) ).
fof(f2144,plain,
is_a_theorem(implies(sF1,sF5)),
inference(resolution,[],[f2142,f1539]) ).
fof(f2152,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,sF1))
| is_a_theorem(implies(X0,sF5)) ),
inference(resolution,[],[f2144,f24]) ).
fof(f2240,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X2),X3))
| ~ is_a_theorem(implies(implies(X1,X2),X3)) ),
inference(resolution,[],[f1663,f358]) ).
fof(f2279,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X0)))
| is_a_theorem(implies(X2,X0)) ),
inference(resolution,[],[f2240,f592]) ).
fof(f2589,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),X0)),
inference(resolution,[],[f2279,f565]) ).
fof(f2623,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(implies(X2,X0),X0)) ),
inference(resolution,[],[f2589,f432]) ).
fof(f2627,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X2),X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f2589,f24]) ).
fof(f2674,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X2),X1))
| is_a_theorem(implies(implies(X0,X1),X1)) ),
inference(resolution,[],[f2627,f358]) ).
fof(f2772,plain,
! [X0] :
( is_a_theorem(implies(implies(y,X0),X0))
| ~ is_a_theorem(implies(sF1,X0)) ),
inference(superposition,[],[f2674,f9]) ).
fof(f2774,plain,
! [X0] :
( is_a_theorem(implies(implies(z,X0),X0))
| ~ is_a_theorem(implies(sF0,X0)) ),
inference(superposition,[],[f2674,f7]) ).
fof(f2775,plain,
! [X0] :
( is_a_theorem(implies(implies(sF2,X0),X0))
| ~ is_a_theorem(implies(sF5,X0)) ),
inference(superposition,[],[f2674,f17]) ).
fof(f2776,plain,
! [X0] :
( is_a_theorem(implies(implies(sF3,X0),X0))
| ~ is_a_theorem(implies(sF4,X0)) ),
inference(superposition,[],[f2674,f15]) ).
fof(f2863,plain,
( ~ is_a_theorem(implies(sF1,sF1))
| is_a_theorem(implies(implies(y,sF1),sF5)) ),
inference(resolution,[],[f2772,f2152]) ).
fof(f2865,plain,
is_a_theorem(implies(implies(y,sF1),sF5)),
inference(forward_subsumption_resolution,[],[f2863,f120]) ).
fof(f2868,plain,
is_a_theorem(implies(implies(y,sF5),sF5)),
inference(resolution,[],[f2865,f2674]) ).
fof(f2883,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(y,sF5)))
| is_a_theorem(implies(X0,sF5)) ),
inference(resolution,[],[f2868,f24]) ).
fof(f2993,plain,
( ~ is_a_theorem(implies(sF0,sF1))
| is_a_theorem(implies(implies(z,sF1),sF5)) ),
inference(resolution,[],[f2774,f2152]) ).
fof(f2996,plain,
is_a_theorem(implies(implies(z,sF1),sF5)),
inference(forward_subsumption_resolution,[],[f2993,f525]) ).
fof(f3001,plain,
is_a_theorem(implies(implies(z,sF5),sF5)),
inference(resolution,[],[f2996,f2674]) ).
fof(f3016,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(z,sF5)))
| is_a_theorem(implies(X0,sF5)) ),
inference(resolution,[],[f3001,f24]) ).
fof(f3125,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X0)),implies(X2,X0))),
inference(resolution,[],[f2623,f1665]) ).
fof(f3326,plain,
( ~ is_a_theorem(implies(sF4,implies(z,sF5)))
| is_a_theorem(implies(implies(sF3,implies(z,sF5)),sF5)) ),
inference(resolution,[],[f2776,f3016]) ).
fof(f3338,plain,
is_a_theorem(implies(implies(sF3,implies(z,sF5)),sF5)),
inference(forward_subsumption_resolution,[],[f3326,f1717]) ).
fof(f3341,plain,
is_a_theorem(implies(implies(sF3,sF5),sF5)),
inference(resolution,[],[f3338,f2674]) ).
fof(f3347,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF3,implies(z,sF5))))
| is_a_theorem(implies(X0,sF5)) ),
inference(resolution,[],[f3338,f24]) ).
fof(f3358,plain,
( ~ is_a_theorem(implies(sF3,sF5))
| is_a_theorem(sF5) ),
inference(resolution,[],[f3341,f1]) ).
fof(f3359,plain,
~ is_a_theorem(implies(sF3,sF5)),
inference(forward_subsumption_resolution,[],[f3358,f18]) ).
fof(f3472,plain,
! [X0] :
( ~ is_a_theorem(implies(sF3,implies(X0,sF5)))
| is_a_theorem(implies(implies(z,X0),sF5)) ),
inference(resolution,[],[f3347,f44]) ).
fof(f4343,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X3,X1))))
| is_a_theorem(implies(X0,implies(X3,X1))) ),
inference(resolution,[],[f3125,f24]) ).
fof(f4374,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X3),implies(X1,X2)))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[],[f4343,f44]) ).
fof(f7094,plain,
! [X0] : is_a_theorem(implies(implies(X0,sF1),implies(X0,sF5))),
inference(resolution,[],[f2143,f4374]) ).
fof(f7183,plain,
is_a_theorem(implies(sF2,implies(x,sF5))),
inference(superposition,[],[f7094,f11]) ).
fof(f7976,plain,
( ~ is_a_theorem(implies(sF5,implies(y,sF5)))
| is_a_theorem(implies(implies(sF2,implies(y,sF5)),sF5)) ),
inference(resolution,[],[f2775,f2883]) ).
fof(f8009,plain,
is_a_theorem(implies(implies(sF2,implies(y,sF5)),sF5)),
inference(forward_subsumption_resolution,[],[f7976,f496]) ).
fof(f8030,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF2,implies(y,sF5))))
| is_a_theorem(implies(X0,sF5)) ),
inference(resolution,[],[f8009,f24]) ).
fof(f8040,plain,
! [X0] :
( ~ is_a_theorem(implies(sF2,implies(X0,sF5)))
| is_a_theorem(implies(implies(y,X0),sF5)) ),
inference(resolution,[],[f8030,f44]) ).
fof(f8137,plain,
is_a_theorem(implies(implies(y,x),sF5)),
inference(resolution,[],[f8040,f7183]) ).
fof(f8150,plain,
! [X0] : is_a_theorem(implies(X0,implies(x,sF5))),
inference(resolution,[],[f8137,f1647]) ).
fof(f8238,plain,
is_a_theorem(implies(implies(z,x),sF5)),
inference(resolution,[],[f8150,f3472]) ).
fof(f8240,plain,
is_a_theorem(implies(sF3,sF5)),
inference(forward_demodulation,[],[f8238,f13]) ).
fof(f8241,plain,
$false,
inference(forward_subsumption_resolution,[],[f8240,f3359]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL377-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.38 % Computer : n005.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sun Sep 27 15:37:47 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.42 Running first-order theorem proving
% 0.09/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.30/3.32 % (4153423)Input is clausal, will run a generic CNF schedule.
% 17.30/3.32 % (4153478)lrs+10_1_sil=8000:sp=occurrence:random_seed=2399673718:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 17.30/3.32 % (4153476)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=438212847:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 17.30/3.32 % (4153477)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2195511160:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 17.30/3.32 % (4153475)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=2777748025:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 17.30/3.32 % (4153478)Instruction limit reached!
% 17.30/3.32 % (4153478)------------------------------
% 17.30/3.32 % (4153478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.30/3.32 % (4153478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.30/3.32 % (4153478)CaDiCaL version: 2.1.3
% 17.30/3.32 % (4153478)Termination reason: Instruction limit
% 17.30/3.32 % (4153478)Termination phase: Saturation
% 17.30/3.32 % (4153478)Time elapsed: 0.039 s
% 17.30/3.32 % (4153478)Peak memory usage: 89 MB
% 17.30/3.32 % (4153478)Instructions burned: 109 (million)
% 17.30/3.32 % (4153481)dis-21_1_sil=8000:lcm=predicate:random_seed=339522205:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 17.30/3.32 % (4153480)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2913295086:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 17.30/3.32 % (4153479)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=454688842:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 17.30/3.32 % (4153481)Instruction limit reached!
% 17.30/3.32 % (4153481)------------------------------
% 17.30/3.32 % (4153481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.30/3.32 % (4153481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.30/3.32 % (4153481)CaDiCaL version: 2.1.3
% 17.30/3.32 % (4153481)Termination reason: Instruction limit
% 17.30/3.32 % (4153481)Termination phase: Saturation
% 17.30/3.32 % (4153481)Time elapsed: 0.072 s
% 17.30/3.32 % (4153481)Peak memory usage: 88 MB
% 17.30/3.32 % (4153481)Instructions burned: 118 (million)
% 17.30/3.32 % (4153486)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=1423521517:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 17.30/3.32 % (4153486)Refutation not found, incomplete strategy
% 17.30/3.32 % (4153486)------------------------------
% 17.30/3.32 % (4153486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.30/3.32 % (4153486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.30/3.32 % (4153486)CaDiCaL version: 2.1.3
% 17.30/3.32 % (4153486)Termination reason: Refutation not found, incomplete strategy
% 17.30/3.32 % (4153486)Time elapsed: 0.0000 s
% 17.30/3.32 % (4153486)Peak memory usage: 87 MB
% 17.30/3.32 % (4153479)Instruction limit reached!
% 17.30/3.32 % (4153479)------------------------------
% 17.30/3.32 % (4153479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.30/3.32 % (4153479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.30/3.32 % (4153479)CaDiCaL version: 2.1.3
% 17.30/3.32 % (4153479)Termination reason: Instruction limit
% 17.30/3.32 % (4153479)Termination phase: Saturation
% 17.30/3.32 % (4153479)Time elapsed: 0.083 s
% 17.30/3.32 % (4153479)Peak memory usage: 88 MB
% 17.30/3.32 % (4153479)Instructions burned: 115 (million)
% 17.30/3.32 % (4153480)Instruction limit reached!
% 17.30/3.32 % (4153480)------------------------------
% 17.30/3.32 % (4153480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.30/3.32 % (4153480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.30/3.32 % (4153480)CaDiCaL version: 2.1.3
% 17.30/3.32 % (4153480)Termination reason: Instruction limit
% 17.30/3.32 % (4153480)Termination phase: Saturation
% 17.30/3.32 % (4153480)Time elapsed: 0.118 s
% 17.30/3.32 % (4153480)Peak memory usage: 89 MB
% 17.30/3.32 % (4153480)Instructions burned: 180 (million)
% 17.30/3.32 % (4153490)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1811379337: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)
% 27.91/5.03 % (4153486)------------------------------
% 27.91/5.03 % (4153486)------------------------------
% 27.91/5.03 % (4153493)lrs+10_64_to=lpo:sil=8000:random_seed=1753540396:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 27.91/5.03 % (4153492)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3359388203:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 27.91/5.03 % (4153492)Refutation not found, incomplete strategy
% 27.91/5.03 % (4153492)------------------------------
% 27.91/5.03 % (4153492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153492)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153492)Termination reason: Refutation not found, incomplete strategy
% 27.91/5.03 % (4153492)Time elapsed: 0.001 s
% 27.91/5.03 % (4153492)Peak memory usage: 87 MB
% 27.91/5.03 % (4153490)Instruction limit reached!
% 27.91/5.03 % (4153490)------------------------------
% 27.91/5.03 % (4153490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153490)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153490)Termination reason: Instruction limit
% 27.91/5.03 % (4153490)Termination phase: Saturation
% 27.91/5.03 % (4153490)Time elapsed: 0.131 s
% 27.91/5.03 % (4153490)Peak memory usage: 88 MB
% 27.91/5.03 % (4153490)Instructions burned: 190 (million)
% 27.91/5.03 % (4153493)Instruction limit reached!
% 27.91/5.03 % (4153493)------------------------------
% 27.91/5.03 % (4153493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153493)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153493)Termination reason: Instruction limit
% 27.91/5.03 % (4153493)Termination phase: Saturation
% 27.91/5.03 % (4153493)Time elapsed: 0.118 s
% 27.91/5.03 % (4153493)Peak memory usage: 88 MB
% 27.91/5.03 % (4153493)Instructions burned: 127 (million)
% 27.91/5.03 % (4153496)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3111662306:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 27.91/5.03 % (4153496)Instruction limit reached!
% 27.91/5.03 % (4153496)------------------------------
% 27.91/5.03 % (4153496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153496)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153496)Termination reason: Instruction limit
% 27.91/5.03 % (4153496)Termination phase: Saturation
% 27.91/5.03 % (4153496)Time elapsed: 0.119 s
% 27.91/5.03 % (4153496)Peak memory usage: 90 MB
% 27.91/5.03 % (4153496)Instructions burned: 194 (million)
% 27.91/5.03 % (4153506)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2534973171:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 27.91/5.03 % (4153492)------------------------------
% 27.91/5.03 % (4153492)------------------------------
% 27.91/5.03 % (4153507)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3234329743:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 27.91/5.03 % (4153506)Instruction limit reached!
% 27.91/5.03 % (4153506)------------------------------
% 27.91/5.03 % (4153506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153506)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153506)Termination reason: Instruction limit
% 27.91/5.03 % (4153506)Termination phase: Saturation
% 27.91/5.03 % (4153506)Time elapsed: 0.164 s
% 27.91/5.03 % (4153506)Peak memory usage: 91 MB
% 27.91/5.03 % (4153506)Instructions burned: 157 (million)
% 27.91/5.03 % (4153517)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=1109661383:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 27.91/5.03 % (4153517)Instruction limit reached!
% 27.91/5.03 % (4153517)------------------------------
% 27.91/5.03 % (4153517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153517)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153517)Termination reason: Instruction limit
% 27.91/5.03 % (4153517)Termination phase: Saturation
% 27.91/5.03 % (4153517)Time elapsed: 0.039 s
% 27.91/5.03 % (4153517)Peak memory usage: 88 MB
% 27.91/5.03 % (4153517)Instructions burned: 106 (million)
% 27.91/5.03 % (4153520)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2023790242:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 27.91/5.03 % (4153520)Refutation not found, incomplete strategy
% 27.91/5.03 % (4153520)------------------------------
% 27.91/5.03 % (4153520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153520)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153520)Termination reason: Refutation not found, incomplete strategy
% 27.91/5.03 % (4153520)Time elapsed: 0.001 s
% 27.91/5.03 % (4153520)Peak memory usage: 86 MB
% 27.91/5.03 % (4153528)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1836685612:cond=fast:i=5208:av=off_2989 on theBenchmark for (2989ds/5208Mi)
% 27.91/5.03 % (4153523)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3987857941:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 27.91/5.03 % (4153520)------------------------------
% 27.91/5.03 % (4153520)------------------------------
% 27.91/5.03 % (4153523)Instruction limit reached!
% 27.91/5.03 % (4153523)------------------------------
% 27.91/5.03 % (4153523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153523)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153523)Termination reason: Instruction limit
% 27.91/5.03 % (4153523)Termination phase: Saturation
% 27.91/5.03 % (4153523)Time elapsed: 0.263 s
% 27.91/5.03 % (4153523)Peak memory usage: 89 MB
% 27.91/5.03 % (4153523)Instructions burned: 243 (million)
% 27.91/5.03 % (4153540)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=53088906:i=134:sd=2:doe=on:ss=axioms:sgt=14_2985 on theBenchmark for (2985ds/134Mi)
% 27.91/5.03 % (4153541)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1391925688:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 27.91/5.03 % (4153540)Instruction limit reached!
% 27.91/5.03 % (4153540)------------------------------
% 27.91/5.03 % (4153540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153540)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153540)Termination reason: Instruction limit
% 27.91/5.03 % (4153540)Termination phase: Saturation
% 27.91/5.03 % (4153540)Time elapsed: 0.155 s
% 27.91/5.03 % (4153540)Peak memory usage: 89 MB
% 27.91/5.03 % (4153540)Instructions burned: 134 (million)
% 27.91/5.03 % (4153541)Instruction limit reached!
% 27.91/5.03 % (4153541)------------------------------
% 27.91/5.03 % (4153541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153541)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153541)Termination reason: Instruction limit
% 27.91/5.03 % (4153541)Termination phase: Saturation
% 27.91/5.03 % (4153541)Time elapsed: 0.383 s
% 27.91/5.03 % (4153541)Peak memory usage: 94 MB
% 27.91/5.03 % (4153541)Instructions burned: 499 (million)
% 27.91/5.03 % (4153551)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1455473107:i=191:fgj=on:bd=all_2980 on theBenchmark for (2980ds/191Mi)
% 27.91/5.03 % (4153551)Instruction limit reached!
% 27.91/5.03 % (4153551)------------------------------
% 27.91/5.03 % (4153551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153551)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153551)Termination reason: Instruction limit
% 27.91/5.03 % (4153551)Termination phase: Saturation
% 27.91/5.03 % (4153551)Time elapsed: 0.194 s
% 27.91/5.03 % (4153551)Peak memory usage: 91 MB
% 27.91/5.03 % (4153551)Instructions burned: 192 (million)
% 27.91/5.03 % (4153556)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3734369613:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 27.91/5.03 % (4153557)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=413032903:cond=on:i=156:bs=on:gtg=exists_all:er=known_2976 on theBenchmark for (2976ds/156Mi)
% 27.91/5.03 % (4153556)Instruction limit reached!
% 27.91/5.03 % (4153556)------------------------------
% 27.91/5.03 % (4153556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153556)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153556)Termination reason: Instruction limit
% 27.91/5.03 % (4153556)Termination phase: Saturation
% 27.91/5.03 % (4153556)Time elapsed: 0.284 s
% 27.91/5.03 % (4153556)Peak memory usage: 91 MB
% 27.91/5.03 % (4153556)Instructions burned: 264 (million)
% 27.91/5.03 % (4153557)Instruction limit reached!
% 27.91/5.03 % (4153557)------------------------------
% 27.91/5.03 % (4153557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153557)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153557)Termination reason: Instruction limit
% 27.91/5.03 % (4153557)Termination phase: Saturation
% 27.91/5.03 % (4153557)Time elapsed: 0.124 s
% 27.91/5.03 % (4153557)Peak memory usage: 89 MB
% 27.91/5.03 % (4153557)Instructions burned: 156 (million)
% 27.91/5.03 % (4153564)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=666044035:i=3256:kws=precedence:bd=preordered:av=off_2972 on theBenchmark for (2972ds/3256Mi)
% 27.91/5.03 % (4153565)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2312137684:i=537:av=off:ss=included_2971 on theBenchmark for (2971ds/537Mi)
% 27.91/5.03 % (4153507)Instruction limit reached!
% 27.91/5.03 % (4153507)------------------------------
% 27.91/5.03 % (4153507)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153507)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153507)Termination reason: Instruction limit
% 27.91/5.03 % (4153507)Termination phase: Saturation
% 27.91/5.03 % (4153507)Time elapsed: 2.266 s
% 27.91/5.03 % (4153507)Peak memory usage: 149 MB
% 27.91/5.03 % (4153507)Instructions burned: 3398 (million)
% 27.91/5.03 % (4153573)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2943272097:i=180:bd=preordered:av=off_2968 on theBenchmark for (2968ds/180Mi)
% 27.91/5.03 % (4153573)Instruction limit reached!
% 27.91/5.03 % (4153573)------------------------------
% 27.91/5.03 % (4153573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153573)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153573)Termination reason: Instruction limit
% 27.91/5.03 % (4153573)Termination phase: Saturation
% 27.91/5.03 % (4153573)Time elapsed: 0.075 s
% 27.91/5.03 % (4153573)Peak memory usage: 88 MB
% 27.91/5.03 % (4153573)Instructions burned: 183 (million)
% 27.91/5.03 % (4153579)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=1136419112:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2965 on theBenchmark for (2965ds/10307Mi)
% 27.91/5.03 % (4153565)Instruction limit reached!
% 27.91/5.03 % (4153565)------------------------------
% 27.91/5.03 % (4153565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.91/5.03 % (4153565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.91/5.03 % (4153565)CaDiCaL version: 2.1.3
% 27.91/5.03 % (4153565)Termination reason: Instruction limit
% 27.91/5.03 % (4153565)Termination phase: Saturation
% 27.91/5.03 % (4153565)Time elapsed: 0.569 s
% 27.91/5.03 % (4153565)Peak memory usage: 92 MB
% 27.91/5.03 % (4153565)Instructions burned: 537 (million)
% 27.91/5.03 % (4153528)First to succeed.
% 27.91/5.03 % (4153528)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4153423"
% 27.91/5.03 % (4153583)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=1421997186:i=412:gtgl=4:gtg=exists_all_2963 on theBenchmark for (2963ds/412Mi)
% 27.91/5.03 % (4153476)Also succeeded, but the first one will report.
% 27.91/5.03 % (4153528)Refutation found. Thanks to Tanya!
% 27.91/5.03 % SZS status Unsatisfiable for theBenchmark
% 27.91/5.03 % SZS output start Proof for theBenchmark
% See solution above
% 29.98/5.30 % (4153528)------------------------------
% 29.98/5.30 % (4153528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.98/5.30 % (4153528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.98/5.30 % (4153528)CaDiCaL version: 2.1.3
% 29.98/5.30 % (4153528)Termination reason: Refutation
% 29.98/5.30 % (4153528)Time elapsed: 2.489 s
% 29.98/5.30 % (4153528)Peak memory usage: 143 MB
% 29.98/5.30 % (4153528)Instructions burned: 2731 (million)
% 29.98/5.30 % (4153528)------------------------------
% 29.98/5.30 % (4153528)------------------------------
% 29.98/5.30 % (4153423)Success in time 4.159 s
% 29.98/5.30 % Vampire exiting
%------------------------------------------------------------------------------