%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL028-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n007.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:50:58 AM UTC 2026
% Result : Unsatisfiable 116.24s 19.88s
% Output : Refutation 136.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 89
% Number of leaves : 15
% Syntax : Number of formulae : 194 ( 72 unt; 10 def)
% Number of atoms : 370 ( 18 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 357 ( 181 ~; 175 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 14 con; 0-2 aty)
% Number of variables : 455 ( 0 sgn 455 !; 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,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c0_2) ).
fof(f3,axiom,
! [X0] : is_a_theorem(implies(implies(implies(X0,falsehood),falsehood),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c0_5) ).
fof(f4,axiom,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(implies(X0,X1),implies(X0,X2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c0_6) ).
fof(f5,negated_conjecture,
~ is_a_theorem(implies(implies(implies(implies(implies(a,b),implies(c,falsehood)),e),falsehood),implies(implies(falsehood,a),implies(c,a)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_c0_CAMeredith) ).
fof(f6,definition,
sF0 = implies(a,b),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f7,plain,
implies(a,b) = sF0,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF1 = implies(c,falsehood),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f9,plain,
implies(c,falsehood) = sF1,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF2 = implies(sF0,sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f11,plain,
implies(sF0,sF1) = sF2,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF3 = implies(sF2,e),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f13,plain,
implies(sF2,e) = sF3,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF4 = implies(sF3,falsehood),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f15,plain,
implies(sF3,falsehood) = sF4,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF5 = implies(falsehood,a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f17,plain,
implies(falsehood,a) = sF5,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF6 = implies(c,a),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f19,plain,
implies(c,a) = sF6,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF7 = implies(sF5,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f21,plain,
implies(sF5,sF6) = sF7,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF8 = implies(sF4,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f23,plain,
implies(sF4,sF7) = sF8,
inference(reorient_equations,[],[f22]) ).
fof(f24,plain,
~ is_a_theorem(sF8),
inference(definition_folding,[],[f5,f23,f21,f19,f17,f15,f13,f11,f9,f7]) ).
fof(f25,plain,
! [X0,X1] :
( is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f1,f2]) ).
fof(f26,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f1,f4]) ).
fof(f82,plain,
is_a_theorem(implies(a,sF6)),
inference(superposition,[],[f2,f19]) ).
fof(f127,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f26,f1]) ).
fof(f159,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X2,X0))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f25,f127]) ).
fof(f176,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f159,f2]) ).
fof(f197,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))),
inference(resolution,[],[f176,f4]) ).
fof(f198,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f176,f26]) ).
fof(f199,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,X0)))),
inference(resolution,[],[f176,f2]) ).
fof(f213,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X2,X0),implies(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f197,f1]) ).
fof(f242,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,implies(X1,X2)),X3))
| is_a_theorem(implies(X2,X3)) ),
inference(resolution,[],[f199,f159]) ).
fof(f252,plain,
! [X0] : is_a_theorem(implies(sF7,implies(X0,sF8))),
inference(superposition,[],[f199,f23]) ).
fof(f276,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X1))),
inference(resolution,[],[f198,f2]) ).
fof(f279,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))),
inference(resolution,[],[f198,f197]) ).
fof(f294,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X0),X1))
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f276,f159]) ).
fof(f422,plain,
! [X0] : is_a_theorem(implies(falsehood,X0)),
inference(resolution,[],[f3,f176]) ).
fof(f483,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(implies(X3,X0),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f242,f26]) ).
fof(f499,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(X1,implies(X0,X2)),implies(X1,X2)))),
inference(resolution,[],[f483,f4]) ).
fof(f517,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,implies(X2,X1)))),
inference(resolution,[],[f499,f483]) ).
fof(f519,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X0,X2))))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f499,f127]) ).
fof(f569,plain,
! [X0] : is_a_theorem(implies(implies(X0,sF7),implies(X0,sF8))),
inference(superposition,[],[f517,f23]) ).
fof(f601,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X0,X1),X0),X1))),
inference(resolution,[],[f519,f197]) ).
fof(f603,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(implies(X0,X1),X2)))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[],[f519,f213]) ).
fof(f620,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,falsehood),implies(X0,X1))),
inference(resolution,[],[f603,f422]) ).
fof(f647,plain,
is_a_theorem(implies(implies(c,falsehood),sF6)),
inference(superposition,[],[f620,f19]) ).
fof(f653,plain,
is_a_theorem(implies(sF1,sF6)),
inference(forward_demodulation,[],[f647,f9]) ).
fof(f681,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X0),X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f601,f1]) ).
fof(f695,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X0))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1) ),
inference(resolution,[],[f681,f1]) ).
fof(f710,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X0),X1))
| is_a_theorem(X1) ),
inference(resolution,[],[f695,f276]) ).
fof(f736,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(implies(X1,X1),X2)),implies(X0,X2))),
inference(resolution,[],[f710,f499]) ).
fof(f738,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(implies(implies(X1,X1),X2),X2))),
inference(resolution,[],[f736,f294]) ).
fof(f746,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X1,X1),X2)))
| is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f736,f1]) ).
fof(f760,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))),
inference(resolution,[],[f746,f4]) ).
fof(f763,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X0),X1),X2))
| ~ is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f746,f213]) ).
fof(f864,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X2),X0))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X1) ),
inference(resolution,[],[f763,f1]) ).
fof(f882,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(X2)
| ~ is_a_theorem(implies(X0,implies(X0,X1))) ),
inference(resolution,[],[f864,f26]) ).
fof(f884,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(falsehood,X0),X1))
| is_a_theorem(X1) ),
inference(resolution,[],[f864,f620]) ).
fof(f909,plain,
! [X0] :
( ~ is_a_theorem(implies(sF5,X0))
| is_a_theorem(X0) ),
inference(superposition,[],[f884,f17]) ).
fof(f915,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,implies(sF5,X1)),implies(X0,X1))),
inference(resolution,[],[f909,f499]) ).
fof(f921,plain,
! [X0,X1] : is_a_theorem(implies(implies(sF5,X0),implies(X1,X0))),
inference(resolution,[],[f915,f176]) ).
fof(f930,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(X0,implies(sF5,X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f915,f1]) ).
fof(f1212,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(X2,X0)))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) ),
inference(resolution,[],[f882,f279]) ).
fof(f1214,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X2)))
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f882,f213]) ).
fof(f1228,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(X2,X3)))
| is_a_theorem(implies(X0,implies(X1,implies(X2,X3)))) ),
inference(resolution,[],[f882,f199]) ).
fof(f1313,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),
inference(resolution,[],[f1212,f199]) ).
fof(f1587,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(X2,implies(X3,X2))))),
inference(resolution,[],[f1228,f199]) ).
fof(f1618,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,implies(X3,X2)),X1))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f1587,f1214]) ).
fof(f1667,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X3,X1),X2))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f1618,f213]) ).
fof(f1729,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(X1,implies(X2,X3))))
| ~ is_a_theorem(implies(X1,X3)) ),
inference(resolution,[],[f1667,f213]) ).
fof(f1771,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X3,X1),X2))
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f1729,f1214]) ).
fof(f1818,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X1,X3))))
| ~ is_a_theorem(implies(X0,implies(X2,X3))) ),
inference(resolution,[],[f1771,f4]) ).
fof(f1827,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X3,X3),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f1771,f736]) ).
fof(f1916,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(implies(X2,X0),implies(X2,implies(X2,X1)))) ),
inference(resolution,[],[f1818,f603]) ).
fof(f1930,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X3,X1),implies(X0,implies(X3,X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f1818,f198]) ).
fof(f1971,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,implies(X0,implies(X2,X1))))),
inference(resolution,[],[f1916,f199]) ).
fof(f2030,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X3,X1))
| is_a_theorem(implies(X0,implies(X3,X2))) ),
inference(resolution,[],[f1930,f1]) ).
fof(f2240,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X1,implies(X2,X3)),implies(X0,implies(X1,X3))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f2030,f4]) ).
fof(f2308,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X2,X3)))
| ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X0,implies(X1,X3))) ),
inference(resolution,[],[f2240,f1]) ).
fof(f2369,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X0,implies(X1,X3)))
| ~ is_a_theorem(implies(X2,X3)) ),
inference(resolution,[],[f2308,f25]) ).
fof(f2739,plain,
! [X2,X0,X1] : is_a_theorem(implies(X0,implies(X1,implies(implies(X0,X2),X2)))),
inference(resolution,[],[f1827,f499]) ).
fof(f2749,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X2,implies(X0,X1)))),
inference(resolution,[],[f1827,f4]) ).
fof(f2815,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X1,implies(X1,X2))),implies(X0,implies(X1,X2)))),
inference(resolution,[],[f2749,f603]) ).
fof(f2858,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(X0,implies(implies(X1,X2),X2)))),
inference(resolution,[],[f2739,f603]) ).
fof(f2981,plain,
! [X0] : is_a_theorem(implies(implies(X0,implies(sF4,sF8)),implies(X0,sF8))),
inference(superposition,[],[f2815,f23]) ).
fof(f3005,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X0,implies(implies(X1,X2),X2))) ),
inference(resolution,[],[f2858,f882]) ).
fof(f3360,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,implies(sF4,sF8)))
| is_a_theorem(implies(X0,sF8)) ),
inference(resolution,[],[f2981,f1]) ).
fof(f3362,plain,
! [X0] :
( is_a_theorem(implies(implies(sF4,X0),sF8))
| ~ is_a_theorem(implies(X0,sF8)) ),
inference(resolution,[],[f3360,f213]) ).
fof(f3398,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,sF8))
| ~ is_a_theorem(implies(sF4,X0))
| is_a_theorem(sF8) ),
inference(resolution,[],[f3362,f1]) ).
fof(f3400,plain,
! [X0] :
( ~ is_a_theorem(implies(sF4,X0))
| ~ is_a_theorem(implies(X0,sF8)) ),
inference(forward_subsumption_resolution,[],[f3398,f24]) ).
fof(f3564,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X3,X2))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2)))
| ~ is_a_theorem(implies(X1,X3)) ),
inference(resolution,[],[f2369,f213]) ).
fof(f3569,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X2)))
| ~ is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f2369,f760]) ).
fof(f3822,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X2,implies(X2,X3))))
| is_a_theorem(implies(implies(X0,X1),implies(X0,implies(X2,X3)))) ),
inference(resolution,[],[f3564,f760]) ).
fof(f3969,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X0,implies(X1,X3))))
| ~ is_a_theorem(implies(X2,implies(X1,X3))) ),
inference(resolution,[],[f3822,f213]) ).
fof(f4016,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,X0),implies(X1,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f3969,f710]) ).
fof(f4109,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X1,X0))
| is_a_theorem(implies(X1,X2)) ),
inference(resolution,[],[f4016,f1]) ).
fof(f4168,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X0,implies(X1,X2))))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[],[f4109,f4]) ).
fof(f4213,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X1,X2))))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[],[f4168,f26]) ).
fof(f4217,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(implies(X0,X1),X2)))
| is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X2))) ),
inference(resolution,[],[f4168,f3569]) ).
fof(f4263,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(implies(X0,X1),implies(X2,X1)))),
inference(resolution,[],[f4213,f1971]) ).
fof(f4266,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X0),implies(implies(X0,X1),X2)))
| ~ is_a_theorem(implies(X1,implies(X0,X2))) ),
inference(resolution,[],[f4213,f213]) ).
fof(f4316,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X3,implies(X1,implies(implies(X1,X0),X2))))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f4266,f1667]) ).
fof(f4328,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X1,X0),implies(implies(implies(X1,X0),X1),X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f4266,f198]) ).
fof(f4912,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,implies(X2,X1)))),
inference(resolution,[],[f4217,f199]) ).
fof(f5622,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(X1,X0),X2),X3))
| is_a_theorem(implies(X1,X3))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f4316,f1214]) ).
fof(f5714,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X3)))
| is_a_theorem(implies(X0,implies(implies(X0,X1),X2)))
| ~ is_a_theorem(implies(X3,X2)) ),
inference(resolution,[],[f5622,f213]) ).
fof(f6608,definition,
( spl9_48
<=> is_a_theorem(implies(sF1,sF8)) ),
introduced(definition,[new_symbols(definition,[spl9_48])],[avatar_definition]) ).
fof(f6609,plain,
( ~ is_a_theorem(implies(sF1,sF8))
| spl9_48 ),
inference(avatar_component_clause,[],[f6608]) ).
fof(f6610,plain,
( is_a_theorem(implies(sF1,sF8))
| ~ spl9_48 ),
inference(avatar_component_clause,[],[f6608]) ).
fof(f7264,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(implies(X1,X0),X1),X2))
| ~ is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f4328,f1]) ).
fof(f7284,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X2)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X3,X2))
| ~ is_a_theorem(implies(X3,X0)) ),
inference(resolution,[],[f7264,f1771]) ).
fof(f8620,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X3,X1),X2))
| is_a_theorem(implies(X0,implies(implies(X0,X1),X2))) ),
inference(resolution,[],[f5714,f199]) ).
fof(f8784,plain,
! [X2,X3,X0,X1] : is_a_theorem(implies(X0,implies(implies(X0,implies(X1,X2)),implies(implies(X3,X1),implies(X3,X2))))),
inference(resolution,[],[f8620,f4]) ).
fof(f8912,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X0,X1),implies(X1,X2)),implies(X0,X2)))),
inference(resolution,[],[f8784,f519]) ).
fof(f9255,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),implies(X1,X2)),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f8912,f1]) ).
fof(f9417,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X1,X2)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f9255,f1]) ).
fof(f10575,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X0,X1)))
| is_a_theorem(implies(X2,X3))
| ~ is_a_theorem(implies(X2,X0))
| ~ is_a_theorem(implies(X1,X3)) ),
inference(resolution,[],[f7284,f213]) ).
fof(f10710,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(sF5,X2)))
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f10575,f921]) ).
fof(f13780,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(X2,X1))
| is_a_theorem(implies(implies(sF5,X0),X1))
| ~ is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f10710,f213]) ).
fof(f13930,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(sF5,X0),implies(implies(X1,X2),implies(X1,X3))))
| ~ is_a_theorem(implies(X0,implies(X1,implies(X2,X3)))) ),
inference(resolution,[],[f13780,f4]) ).
fof(f14048,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X1,X3))))
| ~ is_a_theorem(implies(X0,implies(X1,implies(X2,X3)))) ),
inference(resolution,[],[f13930,f176]) ).
fof(f15180,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X2,X3))))
| ~ is_a_theorem(X0)
| is_a_theorem(implies(implies(X1,X2),implies(X1,X3))) ),
inference(resolution,[],[f14048,f1]) ).
fof(f15283,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(X2,X3))))
| is_a_theorem(implies(implies(X0,X2),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f15180,f26]) ).
fof(f15378,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X3,X2)))
| ~ is_a_theorem(implies(X0,implies(X1,X3)))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X2))) ),
inference(resolution,[],[f15283,f1818]) ).
fof(f15486,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(X1,implies(implies(X2,X2),X3))))
| is_a_theorem(implies(implies(X0,X1),implies(X0,X3))) ),
inference(resolution,[],[f15378,f738]) ).
fof(f15772,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(implies(X1,X1),X2)),implies(X0,X3)))
| ~ is_a_theorem(implies(X0,implies(X2,X3))) ),
inference(resolution,[],[f15486,f1818]) ).
fof(f16333,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X3,X3),X1)))
| ~ is_a_theorem(implies(X0,implies(X1,X2)))
| is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f15772,f1]) ).
fof(f16458,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X3,X3),X1))
| is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f16333,f25]) ).
fof(f16580,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X2,X3),X1)))
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X2,X3)) ),
inference(resolution,[],[f16458,f213]) ).
fof(f16706,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X2),X3))
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X2,X3)) ),
inference(resolution,[],[f16580,f213]) ).
fof(f17236,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(implies(X2,X3))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(X3) ),
inference(resolution,[],[f16706,f1]) ).
fof(f17389,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(implies(X0,X3))
| is_a_theorem(X2)
| ~ is_a_theorem(implies(X3,X1)) ),
inference(resolution,[],[f17236,f213]) ).
fof(f17578,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X3)))
| is_a_theorem(implies(X0,implies(X2,X3)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f17389,f4912]) ).
fof(f17623,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X1,X3))
| ~ is_a_theorem(implies(X2,X3)) ),
inference(resolution,[],[f17389,f1313]) ).
fof(f17764,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X3),X1))
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X2,implies(X0,X3))) ),
inference(resolution,[],[f17623,f26]) ).
fof(f17834,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X3,X1),X2))
| is_a_theorem(implies(implies(X0,X1),X2))
| ~ is_a_theorem(implies(X3,X0)) ),
inference(resolution,[],[f17623,f9255]) ).
fof(f17887,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X1,falsehood),implies(X0,falsehood)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f17764,f3]) ).
fof(f17902,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X1,implies(X0,X3)))
| is_a_theorem(implies(X0,implies(X1,X2)))
| ~ is_a_theorem(implies(X3,X2)) ),
inference(resolution,[],[f17764,f213]) ).
fof(f19277,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X1,X2)))
| ~ is_a_theorem(implies(X1,X0)) ),
inference(resolution,[],[f17834,f760]) ).
fof(f32431,plain,
! [X0] : is_a_theorem(implies(implies(implies(X0,falsehood),X0),X0)),
inference(resolution,[],[f17887,f601]) ).
fof(f32494,plain,
! [X0,X1] :
( ~ is_a_theorem(implies(implies(X1,falsehood),X0))
| is_a_theorem(implies(implies(X0,X1),X1)) ),
inference(resolution,[],[f32431,f17834]) ).
fof(f32971,plain,
! [X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),X0)),
inference(resolution,[],[f32494,f620]) ).
fof(f33095,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X1,X2),X0))
| is_a_theorem(implies(implies(X0,X1),X1)) ),
inference(resolution,[],[f32971,f17834]) ).
fof(f33422,plain,
! [X2,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X2),X2))
| ~ is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f33095,f19277]) ).
fof(f33457,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X0)),implies(X2,X0))),
inference(resolution,[],[f33095,f1313]) ).
fof(f34211,plain,
! [X0] :
( is_a_theorem(implies(implies(sF0,X0),X0))
| ~ is_a_theorem(implies(a,X0)) ),
inference(superposition,[],[f33422,f7]) ).
fof(f43688,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),X2))
| is_a_theorem(implies(X3,X0))
| ~ is_a_theorem(implies(X2,implies(X3,X0))) ),
inference(resolution,[],[f33457,f17389]) ).
fof(f43969,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,implies(X1,X3)),implies(X0,X1)))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f43688,f2]) ).
fof(f44082,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(implies(X0,X1),X2),X1),implies(X0,X1))),
inference(resolution,[],[f43969,f4263]) ).
fof(f44349,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(implies(X2,X1),X3),X0))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) ),
inference(resolution,[],[f44082,f17834]) ).
fof(f45136,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,X0))),
inference(resolution,[],[f44349,f1313]) ).
fof(f45325,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X1,X3),X0))
| is_a_theorem(implies(implies(X0,X1),implies(X2,X1))) ),
inference(resolution,[],[f45136,f17834]) ).
fof(f45357,plain,
! [X2,X0,X1] : is_a_theorem(implies(implies(implies(X0,X1),X0),implies(implies(X0,X2),X2))),
inference(resolution,[],[f45136,f3005]) ).
fof(f45409,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X0,implies(implies(X2,X3),X2)))
| is_a_theorem(implies(X0,implies(X1,X2))) ),
inference(resolution,[],[f45136,f17578]) ).
fof(f45537,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X3,X0)))
| ~ is_a_theorem(implies(X2,X0)) ),
inference(resolution,[],[f45409,f213]) ).
fof(f45739,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X1,X2),X3))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X4,X1))
| ~ is_a_theorem(implies(X3,X0)) ),
inference(resolution,[],[f45537,f17389]) ).
fof(f46022,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X3,X4),X0))
| is_a_theorem(implies(X2,X1))
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X3,X1)) ),
inference(resolution,[],[f45739,f19277]) ).
fof(f46482,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X3,X2)))
| ~ is_a_theorem(implies(X0,X2)) ),
inference(resolution,[],[f45325,f19277]) ).
fof(f51647,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(implies(X0,X2),X0),X3)))
| ~ is_a_theorem(implies(X1,X3)) ),
inference(resolution,[],[f45357,f17902]) ).
fof(f53525,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(X2,implies(implies(X0,X3),X1)))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X2,X1)) ),
inference(resolution,[],[f46482,f4109]) ).
fof(f53694,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(implies(implies(implies(X0,X2),X3),X1))
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X3,X1)) ),
inference(resolution,[],[f53525,f213]) ).
fof(f54132,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(sF3,X0),X1))
| ~ is_a_theorem(implies(sF2,X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(superposition,[],[f53694,f13]) ).
fof(f58359,plain,
! [X0] :
( is_a_theorem(implies(sF4,X0))
| ~ is_a_theorem(implies(sF2,X0))
| ~ is_a_theorem(implies(falsehood,X0)) ),
inference(superposition,[],[f54132,f15]) ).
fof(f58360,plain,
! [X0] :
( ~ is_a_theorem(implies(sF2,X0))
| is_a_theorem(implies(sF4,X0)) ),
inference(forward_subsumption_resolution,[],[f58359,f422]) ).
fof(f58536,plain,
! [X0] : is_a_theorem(implies(sF4,implies(X0,sF2))),
inference(resolution,[],[f58360,f2]) ).
fof(f58661,plain,
is_a_theorem(implies(sF4,sF2)),
inference(resolution,[],[f58536,f930]) ).
fof(f63160,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(implies(implies(X2,X3),X1))
| ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(implies(X2,X0),X1)) ),
inference(resolution,[],[f51647,f53525]) ).
fof(f63476,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(c,X1),X0))
| ~ is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(implies(sF1,X0)) ),
inference(superposition,[],[f63160,f9]) ).
fof(f64831,plain,
~ is_a_theorem(implies(sF2,sF8)),
inference(resolution,[],[f58661,f3400]) ).
fof(f71760,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(implies(implies(X4,X2),X1))
| ~ is_a_theorem(implies(implies(X2,X3),X1))
| is_a_theorem(implies(X0,X1)) ),
inference(resolution,[],[f46022,f1313]) ).
fof(f74311,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(sF6,X1),X0))
| ~ is_a_theorem(implies(sF7,X0))
| is_a_theorem(implies(X2,X0)) ),
inference(superposition,[],[f71760,f21]) ).
fof(f74911,plain,
! [X0] :
( ~ is_a_theorem(implies(sF7,implies(sF6,sF8)))
| is_a_theorem(implies(X0,implies(sF6,sF8))) ),
inference(resolution,[],[f74311,f569]) ).
fof(f74994,plain,
! [X0] : is_a_theorem(implies(X0,implies(sF6,sF8))),
inference(forward_subsumption_resolution,[],[f74911,f252]) ).
fof(f75098,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,sF6))
| is_a_theorem(implies(X0,sF8)) ),
inference(resolution,[],[f74994,f9417]) ).
fof(f75471,plain,
( is_a_theorem(implies(implies(sF0,sF6),sF8))
| ~ is_a_theorem(implies(a,sF6)) ),
inference(resolution,[],[f75098,f34211]) ).
fof(f75499,plain,
! [X0] :
( is_a_theorem(implies(implies(c,X0),sF8))
| ~ is_a_theorem(implies(X0,sF6))
| ~ is_a_theorem(implies(sF1,sF6)) ),
inference(resolution,[],[f75098,f63476]) ).
fof(f75523,plain,
! [X0] :
( is_a_theorem(implies(implies(c,X0),sF8))
| ~ is_a_theorem(implies(X0,sF6)) ),
inference(forward_subsumption_resolution,[],[f75499,f653]) ).
fof(f75529,plain,
is_a_theorem(implies(implies(sF0,sF6),sF8)),
inference(forward_subsumption_resolution,[],[f75471,f82]) ).
fof(f76105,plain,
( is_a_theorem(implies(sF1,sF8))
| ~ is_a_theorem(implies(falsehood,sF6)) ),
inference(superposition,[],[f75523,f9]) ).
fof(f76641,plain,
! [X0] :
( is_a_theorem(implies(implies(sF0,X0),sF8))
| ~ is_a_theorem(implies(X0,sF8)) ),
inference(resolution,[],[f75529,f63160]) ).
fof(f76883,plain,
( is_a_theorem(implies(sF2,sF8))
| ~ is_a_theorem(implies(sF1,sF8)) ),
inference(superposition,[],[f76641,f11]) ).
fof(f76884,plain,
~ is_a_theorem(implies(sF1,sF8)),
inference(forward_subsumption_resolution,[],[f76883,f64831]) ).
fof(f76896,plain,
( $false
| ~ spl9_48 ),
inference(forward_subsumption_resolution,[],[f76884,f6610]) ).
fof(f76897,plain,
~ spl9_48,
inference(avatar_contradiction_clause,[],[f76896]) ).
fof(f76902,plain,
( ~ is_a_theorem(implies(falsehood,sF6))
| spl9_48 ),
inference(forward_subsumption_resolution,[],[f76105,f6609]) ).
fof(f76905,plain,
( $false
| spl9_48 ),
inference(forward_subsumption_resolution,[],[f76902,f422]) ).
fof(f76906,plain,
spl9_48,
inference(avatar_contradiction_clause,[],[f76905]) ).
cnf(s1218,plain,
~ spl9_48,
inference(sat_conversion,[],[f76897]) ).
cnf(s1222,plain,
spl9_48,
inference(sat_conversion,[],[f76906]) ).
cnf(s1223,plain,
$false,
inference(rat,[],[s1218,s1222]) ).
fof(f76907,plain,
$false,
inference(avatar_sat_refutation,[],[s1223]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL028-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n007.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 15:15:55 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.41 Running first-order theorem proving
% 0.15/0.41 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
% 13.87/2.82 % (1570651)Input is clausal, will run a generic CNF schedule.
% 13.87/2.82 % (1570671)dis-21_1_sil=8000:lcm=predicate:random_seed=1492939722:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 13.87/2.82 % (1570671)Instruction limit reached!
% 13.87/2.82 % (1570671)------------------------------
% 13.87/2.82 % (1570671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.82 % (1570671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.82 % (1570671)CaDiCaL version: 2.1.3
% 13.87/2.82 % (1570671)Termination reason: Instruction limit
% 13.87/2.82 % (1570671)Termination phase: Saturation
% 13.87/2.82 % (1570671)Time elapsed: 0.061 s
% 13.87/2.82 % (1570671)Peak memory usage: 89 MB
% 13.87/2.82 % (1570671)Instructions burned: 119 (million)
% 13.87/2.82 % (1570666)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4093625838:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 13.87/2.82 % (1570668)lrs+10_1_sil=8000:sp=occurrence:random_seed=2382074723:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 13.87/2.82 % (1570670)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3434180302:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 13.87/2.82 % (1570665)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=1999389218:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 13.87/2.82 % (1570667)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1898889126:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 13.87/2.82 % (1570669)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1850578264:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 13.87/2.82 % (1570668)Instruction limit reached!
% 13.87/2.82 % (1570668)------------------------------
% 13.87/2.82 % (1570668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.82 % (1570668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.82 % (1570668)CaDiCaL version: 2.1.3
% 13.87/2.82 % (1570668)Termination reason: Instruction limit
% 13.87/2.82 % (1570668)Termination phase: Saturation
% 13.87/2.82 % (1570668)Time elapsed: 0.110 s
% 13.87/2.82 % (1570668)Peak memory usage: 89 MB
% 13.87/2.82 % (1570668)Instructions burned: 107 (million)
% 13.87/2.82 % (1570669)Instruction limit reached!
% 13.87/2.82 % (1570669)------------------------------
% 13.87/2.82 % (1570669)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.82 % (1570669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.82 % (1570669)CaDiCaL version: 2.1.3
% 13.87/2.82 % (1570669)Termination reason: Instruction limit
% 13.87/2.82 % (1570669)Termination phase: Saturation
% 13.87/2.82 % (1570669)Time elapsed: 0.095 s
% 13.87/2.82 % (1570669)Peak memory usage: 88 MB
% 13.87/2.82 % (1570669)Instructions burned: 115 (million)
% 13.87/2.82 % (1570676)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=2987447935:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 13.87/2.82 % (1570676)Refutation not found, incomplete strategy
% 13.87/2.82 % (1570676)------------------------------
% 13.87/2.82 % (1570676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.82 % (1570676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.82 % (1570676)CaDiCaL version: 2.1.3
% 13.87/2.82 % (1570676)Termination reason: Refutation not found, incomplete strategy
% 13.87/2.82 % (1570676)Time elapsed: 0.001 s
% 13.87/2.82 % (1570676)Peak memory usage: 87 MB
% 13.87/2.82 % (1570670)Instruction limit reached!
% 13.87/2.82 % (1570670)------------------------------
% 13.87/2.82 % (1570670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.87/2.82 % (1570670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.87/2.82 % (1570670)CaDiCaL version: 2.1.3
% 13.87/2.82 % (1570670)Termination reason: Instruction limit
% 13.87/2.82 % (1570670)Termination phase: Saturation
% 13.87/2.82 % (1570670)Time elapsed: 0.164 s
% 13.87/2.82 % (1570670)Peak memory usage: 89 MB
% 13.87/2.82 % (1570670)Instructions burned: 180 (million)
% 13.87/2.82 % (1570684)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3102614750: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)
% 33.87/5.56 % (1570685)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=304166196:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 33.87/5.56 % (1570685)Refutation not found, incomplete strategy
% 33.87/5.56 % (1570685)------------------------------
% 33.87/5.56 % (1570685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.56 % (1570685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.56 % (1570685)CaDiCaL version: 2.1.3
% 33.87/5.56 % (1570685)Termination reason: Refutation not found, incomplete strategy
% 33.87/5.56 % (1570685)Time elapsed: 0.001 s
% 33.87/5.56 % (1570685)Peak memory usage: 87 MB
% 33.87/5.56 % (1570687)lrs+10_64_to=lpo:sil=8000:random_seed=662130972:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 33.87/5.56 % (1570676)------------------------------
% 33.87/5.56 % (1570676)------------------------------
% 33.87/5.56 % (1570684)Instruction limit reached!
% 33.87/5.56 % (1570684)------------------------------
% 33.87/5.56 % (1570684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.56 % (1570684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.56 % (1570684)CaDiCaL version: 2.1.3
% 33.87/5.56 % (1570684)Termination reason: Instruction limit
% 33.87/5.56 % (1570684)Termination phase: Saturation
% 33.87/5.56 % (1570684)Time elapsed: 0.163 s
% 33.87/5.56 % (1570684)Peak memory usage: 89 MB
% 33.87/5.56 % (1570684)Instructions burned: 189 (million)
% 33.87/5.56 % (1570687)Instruction limit reached!
% 33.87/5.56 % (1570687)------------------------------
% 33.87/5.56 % (1570687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.56 % (1570687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.56 % (1570687)CaDiCaL version: 2.1.3
% 33.87/5.56 % (1570687)Termination reason: Instruction limit
% 33.87/5.56 % (1570687)Termination phase: Saturation
% 33.87/5.56 % (1570687)Time elapsed: 0.107 s
% 33.87/5.56 % (1570687)Peak memory usage: 88 MB
% 33.87/5.56 % (1570687)Instructions burned: 127 (million)
% 33.87/5.56 % (1570696)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3932976342:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 33.87/5.56 % (1570697)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3476258280:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 33.87/5.56 % (1570685)------------------------------
% 33.87/5.56 % (1570685)------------------------------
% 33.87/5.56 % (1570698)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3216757092:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 33.87/5.56 % (1570697)Instruction limit reached!
% 33.87/5.56 % (1570697)------------------------------
% 33.87/5.56 % (1570697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.56 % (1570697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.56 % (1570697)CaDiCaL version: 2.1.3
% 33.87/5.56 % (1570697)Termination reason: Instruction limit
% 33.87/5.56 % (1570697)Termination phase: Saturation
% 33.87/5.56 % (1570697)Time elapsed: 0.102 s
% 33.87/5.56 % (1570697)Peak memory usage: 91 MB
% 33.87/5.56 % (1570697)Instructions burned: 159 (million)
% 33.87/5.56 % (1570696)Instruction limit reached!
% 33.87/5.56 % (1570696)------------------------------
% 33.87/5.56 % (1570696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.56 % (1570696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.56 % (1570696)CaDiCaL version: 2.1.3
% 33.87/5.56 % (1570696)Termination reason: Instruction limit
% 33.87/5.56 % (1570696)Termination phase: Saturation
% 33.87/5.56 % (1570696)Time elapsed: 0.204 s
% 33.87/5.56 % (1570696)Peak memory usage: 89 MB
% 33.87/5.56 % (1570696)Instructions burned: 194 (million)
% 33.87/5.56 % (1570707)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1939316097:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 33.87/5.56 % (1570707)Refutation not found, incomplete strategy
% 33.87/5.56 % (1570707)------------------------------
% 33.87/5.56 % (1570707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.87/5.56 % (1570707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.87/5.56 % (1570707)CaDiCaL version: 2.1.3
% 53.67/8.31 % (1570707)Termination reason: Refutation not found, incomplete strategy
% 53.67/8.31 % (1570707)Time elapsed: 0.001 s
% 53.67/8.31 % (1570707)Peak memory usage: 86 MB
% 53.67/8.31 % (1570705)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=1402435030:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2991 on theBenchmark for (2991ds/106Mi)
% 53.67/8.31 % (1570705)Instruction limit reached!
% 53.67/8.31 % (1570705)------------------------------
% 53.67/8.31 % (1570705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.67/8.31 % (1570705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.67/8.31 % (1570705)CaDiCaL version: 2.1.3
% 53.67/8.31 % (1570705)Termination reason: Instruction limit
% 53.67/8.31 % (1570705)Termination phase: Saturation
% 53.67/8.31 % (1570705)Time elapsed: 0.083 s
% 53.67/8.31 % (1570705)Peak memory usage: 88 MB
% 53.67/8.31 % (1570705)Instructions burned: 106 (million)
% 53.67/8.31 % (1570708)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=510355432:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 53.67/8.31 % (1570707)------------------------------
% 53.67/8.31 % (1570707)------------------------------
% 53.67/8.31 % (1570713)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2608084518:cond=fast:i=5208:av=off_2988 on theBenchmark for (2988ds/5208Mi)
% 53.67/8.31 % (1570715)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2303579348:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 53.67/8.31 % (1570708)Instruction limit reached!
% 53.67/8.31 % (1570708)------------------------------
% 53.67/8.31 % (1570708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.67/8.31 % (1570708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.67/8.31 % (1570708)CaDiCaL version: 2.1.3
% 53.67/8.31 % (1570708)Termination reason: Instruction limit
% 53.67/8.31 % (1570708)Termination phase: Saturation
% 53.67/8.31 % (1570708)Time elapsed: 0.255 s
% 53.67/8.31 % (1570708)Peak memory usage: 89 MB
% 53.67/8.31 % (1570708)Instructions burned: 243 (million)
% 53.67/8.31 % (1570715)Instruction limit reached!
% 53.67/8.31 % (1570715)------------------------------
% 53.67/8.31 % (1570715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.67/8.31 % (1570715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.67/8.31 % (1570715)CaDiCaL version: 2.1.3
% 53.67/8.31 % (1570715)Termination reason: Instruction limit
% 53.67/8.31 % (1570715)Termination phase: Saturation
% 53.67/8.31 % (1570715)Time elapsed: 0.076 s
% 53.67/8.31 % (1570715)Peak memory usage: 89 MB
% 53.67/8.31 % (1570715)Instructions burned: 135 (million)
% 53.67/8.31 % (1570720)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=194439449:i=191:fgj=on:bd=all_2984 on theBenchmark for (2984ds/191Mi)
% 53.67/8.31 % (1570719)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2692524522:i=499:bd=all_2985 on theBenchmark for (2985ds/499Mi)
% 53.67/8.31 % (1570720)Instruction limit reached!
% 53.67/8.31 % (1570720)------------------------------
% 53.67/8.31 % (1570720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.67/8.31 % (1570720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.67/8.31 % (1570720)CaDiCaL version: 2.1.3
% 53.67/8.31 % (1570720)Termination reason: Instruction limit
% 53.67/8.31 % (1570720)Termination phase: Saturation
% 53.67/8.31 % (1570720)Time elapsed: 0.105 s
% 53.67/8.31 % (1570720)Peak memory usage: 90 MB
% 53.67/8.31 % (1570720)Instructions burned: 192 (million)
% 53.67/8.31 % (1570725)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3867749280:i=264:kws=precedence:fsr=off_2982 on theBenchmark for (2982ds/264Mi)
% 53.67/8.31 % (1570725)Instruction limit reached!
% 53.67/8.31 % (1570725)------------------------------
% 53.67/8.31 % (1570725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 53.67/8.31 % (1570725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.67/8.31 % (1570725)CaDiCaL version: 2.1.3
% 53.67/8.31 % (1570725)Termination reason: Instruction limit
% 53.67/8.31 % (1570725)Termination phase: Saturation
% 53.67/8.31 % (1570725)Time elapsed: 0.139 s
% 53.67/8.31 % (1570725)Peak memory usage: 91 MB
% 53.67/8.31 % (1570725)Instructions burned: 266 (million)
% 75.71/11.57 % (1570719)Instruction limit reached!
% 75.71/11.57 % (1570719)------------------------------
% 75.71/11.57 % (1570719)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.71/11.57 % (1570719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.71/11.57 % (1570719)CaDiCaL version: 2.1.3
% 75.71/11.57 % (1570719)Termination reason: Instruction limit
% 75.71/11.57 % (1570719)Termination phase: Saturation
% 75.71/11.57 % (1570719)Time elapsed: 0.423 s
% 75.71/11.57 % (1570719)Peak memory usage: 91 MB
% 75.71/11.57 % (1570719)Instructions burned: 499 (million)
% 75.71/11.57 % (1570729)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4219554353:cond=on:i=156:bs=on:gtg=exists_all:er=known_2979 on theBenchmark for (2979ds/156Mi)
% 75.71/11.57 % (1570729)Instruction limit reached!
% 75.71/11.57 % (1570729)------------------------------
% 75.71/11.57 % (1570729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.71/11.57 % (1570729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.71/11.57 % (1570729)CaDiCaL version: 2.1.3
% 75.71/11.57 % (1570729)Termination reason: Instruction limit
% 75.71/11.57 % (1570729)Termination phase: Saturation
% 75.71/11.57 % (1570729)Time elapsed: 0.085 s
% 75.71/11.57 % (1570729)Peak memory usage: 89 MB
% 75.71/11.57 % (1570729)Instructions burned: 156 (million)
% 75.71/11.57 % (1570730)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=3605770913:i=3256:kws=precedence:bd=preordered:av=off_2978 on theBenchmark for (2978ds/3256Mi)
% 75.71/11.57 % (1570733)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2515619904:i=537:av=off:ss=included_2977 on theBenchmark for (2977ds/537Mi)
% 75.71/11.57 % (1570733)Instruction limit reached!
% 75.71/11.57 % (1570733)------------------------------
% 75.71/11.57 % (1570733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.71/11.57 % (1570733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.71/11.57 % (1570733)CaDiCaL version: 2.1.3
% 75.71/11.57 % (1570733)Termination reason: Instruction limit
% 75.71/11.57 % (1570733)Termination phase: Saturation
% 75.71/11.57 % (1570733)Time elapsed: 0.299 s
% 75.71/11.57 % (1570733)Peak memory usage: 91 MB
% 75.71/11.57 % (1570733)Instructions burned: 538 (million)
% 75.71/11.57 % (1570739)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1209112744:i=180:bd=preordered:av=off_2972 on theBenchmark for (2972ds/180Mi)
% 75.71/11.57 % (1570739)Instruction limit reached!
% 75.71/11.57 % (1570739)------------------------------
% 75.71/11.57 % (1570739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.71/11.57 % (1570739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.71/11.57 % (1570739)CaDiCaL version: 2.1.3
% 75.71/11.57 % (1570739)Termination reason: Instruction limit
% 75.71/11.57 % (1570739)Termination phase: Saturation
% 75.71/11.57 % (1570739)Time elapsed: 0.091 s
% 75.71/11.57 % (1570739)Peak memory usage: 89 MB
% 75.71/11.57 % (1570739)Instructions burned: 180 (million)
% 75.71/11.57 % (1570743)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=2816804382:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2970 on theBenchmark for (2970ds/10307Mi)
% 75.71/11.57 % (1570698)Instruction limit reached!
% 75.71/11.57 % (1570698)------------------------------
% 75.71/11.57 % (1570698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.71/11.57 % (1570698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.71/11.57 % (1570698)CaDiCaL version: 2.1.3
% 75.71/11.57 % (1570698)Termination reason: Instruction limit
% 75.71/11.57 % (1570698)Termination phase: Saturation
% 75.71/11.57 % (1570698)Time elapsed: 3.261 s
% 75.71/11.57 % (1570698)Peak memory usage: 149 MB
% 75.71/11.57 % (1570698)Instructions burned: 3394 (million)
% 75.71/11.57 % (1570751)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=2983541995:i=412:gtgl=4:gtg=exists_all_2958 on theBenchmark for (2958ds/412Mi)
% 75.71/11.57 % (1570751)Instruction limit reached!
% 75.71/11.57 % (1570751)------------------------------
% 75.71/11.57 % (1570751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.71/11.57 % (1570751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.73/16.79 % (1570751)CaDiCaL version: 2.1.3
% 112.73/16.79 % (1570751)Termination reason: Instruction limit
% 112.73/16.79 % (1570751)Termination phase: Saturation
% 112.73/16.79 % (1570751)Time elapsed: 0.419 s
% 112.73/16.79 % (1570751)Peak memory usage: 93 MB
% 112.73/16.79 % (1570751)Instructions burned: 412 (million)
% 112.73/16.79 % (1570755)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=2462655660:s2pl=no:i=8478:s2at=4:nm=6_2952 on theBenchmark for (2952ds/8478Mi)
% 112.73/16.79 % (1570730)Instruction limit reached!
% 112.73/16.79 % (1570730)------------------------------
% 112.73/16.79 % (1570730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.73/16.79 % (1570730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.73/16.79 % (1570730)CaDiCaL version: 2.1.3
% 112.73/16.79 % (1570730)Termination reason: Instruction limit
% 112.73/16.79 % (1570730)Termination phase: Saturation
% 112.73/16.79 % (1570730)Time elapsed: 3.062 s
% 112.73/16.79 % (1570730)Peak memory usage: 151 MB
% 112.73/16.79 % (1570730)Instructions burned: 3256 (million)
% 112.73/16.79 % (1570757)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=2189686180:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2945 on theBenchmark for (2945ds/303Mi)
% 112.73/16.79 % (1570757)Instruction limit reached!
% 112.73/16.79 % (1570757)------------------------------
% 112.73/16.79 % (1570757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.73/16.79 % (1570757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.73/16.79 % (1570757)CaDiCaL version: 2.1.3
% 112.73/16.79 % (1570757)Termination reason: Instruction limit
% 112.73/16.79 % (1570757)Termination phase: Saturation
% 112.73/16.79 % (1570757)Time elapsed: 0.276 s
% 112.73/16.79 % (1570757)Peak memory usage: 90 MB
% 112.73/16.79 % (1570757)Instructions burned: 304 (million)
% 112.73/16.79 % (1570759)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1289358405:st=4:i=720:sd=3:fsr=off:ss=axioms_2940 on theBenchmark for (2940ds/720Mi)
% 112.73/16.79 % (1570713)Instruction limit reached!
% 112.73/16.79 % (1570713)------------------------------
% 112.73/16.79 % (1570713)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.73/16.79 % (1570713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.73/16.79 % (1570713)CaDiCaL version: 2.1.3
% 112.73/16.79 % (1570713)Termination reason: Instruction limit
% 112.73/16.79 % (1570713)Termination phase: Saturation
% 112.73/16.79 % (1570713)Time elapsed: 5.280 s
% 112.73/16.79 % (1570713)Peak memory usage: 162 MB
% 112.73/16.79 % (1570713)Instructions burned: 5208 (million)
% 112.73/16.79 % (1570763)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=344408821:i=598:bs=on:bd=preordered:av=off:ss=axioms_2933 on theBenchmark for (2933ds/598Mi)
% 112.73/16.79 % (1570759)Instruction limit reached!
% 112.73/16.79 % (1570759)------------------------------
% 112.73/16.79 % (1570759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.73/16.79 % (1570759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.73/16.79 % (1570759)CaDiCaL version: 2.1.3
% 112.73/16.79 % (1570759)Termination reason: Instruction limit
% 112.73/16.79 % (1570759)Termination phase: Saturation
% 112.73/16.79 % (1570759)Time elapsed: 0.725 s
% 112.73/16.79 % (1570759)Peak memory usage: 96 MB
% 112.73/16.79 % (1570759)Instructions burned: 721 (million)
% 112.73/16.79 % (1570766)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=604854850:i=2989:sd=3:ss=axioms:sgt=60_2931 on theBenchmark for (2931ds/2989Mi)
% 112.73/16.79 % (1570763)Instruction limit reached!
% 112.73/16.79 % (1570763)------------------------------
% 112.73/16.79 % (1570763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 112.73/16.79 % (1570763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 112.73/16.79 % (1570763)CaDiCaL version: 2.1.3
% 112.73/16.79 % (1570763)Termination reason: Instruction limit
% 112.73/16.79 % (1570763)Termination phase: Saturation
% 112.73/16.79 % (1570763)Time elapsed: 0.525 s
% 112.73/16.79 % (1570763)Peak memory usage: 95 MB
% 112.73/16.79 % (1570763)Instructions burned: 599 (million)
% 112.73/16.79 % (1570770)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=1682560069:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2926 on theBenchmark for (2926ds/1997Mi)
% 116.24/19.88 % (1570743)Instruction limit reached!
% 116.24/19.88 % (1570743)------------------------------
% 116.24/19.88 % (1570743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570743)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570743)Termination reason: Instruction limit
% 116.24/19.88 % (1570743)Termination phase: Saturation
% 116.24/19.88 % (1570743)Time elapsed: 5.391 s
% 116.24/19.88 % (1570743)Peak memory usage: 164 MB
% 116.24/19.88 % (1570743)Instructions burned: 10307 (million)
% 116.24/19.88 % (1570775)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=2520129236:i=2088:bd=preordered:av=off_2914 on theBenchmark for (2914ds/2088Mi)
% 116.24/19.88 % (1570770)Instruction limit reached!
% 116.24/19.88 % (1570770)------------------------------
% 116.24/19.88 % (1570770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570770)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570770)Termination reason: Instruction limit
% 116.24/19.88 % (1570770)Termination phase: Saturation
% 116.24/19.88 % (1570770)Time elapsed: 2.017 s
% 116.24/19.88 % (1570770)Peak memory usage: 134 MB
% 116.24/19.88 % (1570770)Instructions burned: 1997 (million)
% 116.24/19.88 % (1570778)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3812253850:i=1098:nicw=on_2904 on theBenchmark for (2904ds/1098Mi)
% 116.24/19.88 % (1570775)Instruction limit reached!
% 116.24/19.88 % (1570775)------------------------------
% 116.24/19.88 % (1570775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570775)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570775)Termination reason: Instruction limit
% 116.24/19.88 % (1570775)Termination phase: Saturation
% 116.24/19.88 % (1570775)Time elapsed: 1.164 s
% 116.24/19.88 % (1570775)Peak memory usage: 136 MB
% 116.24/19.88 % (1570775)Instructions burned: 2088 (million)
% 116.24/19.88 % (1570781)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1740230437:i=433:bd=preordered_2901 on theBenchmark for (2901ds/433Mi)
% 116.24/19.88 % (1570781)Instruction limit reached!
% 116.24/19.88 % (1570781)------------------------------
% 116.24/19.88 % (1570781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570781)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570781)Termination reason: Instruction limit
% 116.24/19.88 % (1570781)Termination phase: Saturation
% 116.24/19.88 % (1570781)Time elapsed: 0.233 s
% 116.24/19.88 % (1570781)Peak memory usage: 93 MB
% 116.24/19.88 % (1570781)Instructions burned: 433 (million)
% 116.24/19.88 % (1570766)Instruction limit reached!
% 116.24/19.88 % (1570766)------------------------------
% 116.24/19.88 % (1570766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570766)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570766)Termination reason: Instruction limit
% 116.24/19.88 % (1570766)Termination phase: Saturation
% 116.24/19.88 % (1570766)Time elapsed: 3.225 s
% 116.24/19.88 % (1570766)Peak memory usage: 145 MB
% 116.24/19.88 % (1570766)Instructions burned: 2990 (million)
% 116.24/19.88 % (1570783)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4067944026:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2897 on theBenchmark for (2897ds/2942Mi)
% 116.24/19.88 % (1570784)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2305483850:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2896 on theBenchmark for (2896ds/6922Mi)
% 116.24/19.88 % (1570778)Instruction limit reached!
% 116.24/19.88 % (1570778)------------------------------
% 116.24/19.88 % (1570778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570778)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570778)Termination reason: Instruction limit
% 116.24/19.88 % (1570778)Termination phase: Saturation
% 116.24/19.88 % (1570778)Time elapsed: 1.015 s
% 116.24/19.88 % (1570778)Peak memory usage: 98 MB
% 116.24/19.88 % (1570778)Instructions burned: 1099 (million)
% 116.24/19.88 % (1570787)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=2499584799:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2891 on theBenchmark for (2891ds/596Mi)
% 116.24/19.88 % (1570787)Instruction limit reached!
% 116.24/19.88 % (1570787)------------------------------
% 116.24/19.88 % (1570787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570787)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570787)Termination reason: Instruction limit
% 116.24/19.88 % (1570787)Termination phase: Saturation
% 116.24/19.88 % (1570787)Time elapsed: 0.563 s
% 116.24/19.88 % (1570787)Peak memory usage: 97 MB
% 116.24/19.88 % (1570787)Instructions burned: 597 (million)
% 116.24/19.88 % (1570789)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=2736235091:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2884 on theBenchmark for (2884ds/4123Mi)
% 116.24/19.88 % (1570783)Instruction limit reached!
% 116.24/19.88 % (1570783)------------------------------
% 116.24/19.88 % (1570783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570783)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570783)Termination reason: Instruction limit
% 116.24/19.88 % (1570783)Termination phase: Saturation
% 116.24/19.88 % (1570783)Time elapsed: 1.599 s
% 116.24/19.88 % (1570783)Peak memory usage: 138 MB
% 116.24/19.88 % (1570783)Instructions burned: 2943 (million)
% 116.24/19.88 % (1570791)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1209973791:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2879 on theBenchmark for (2879ds/16411Mi)
% 116.24/19.88 % (1570755)Instruction limit reached!
% 116.24/19.88 % (1570755)------------------------------
% 116.24/19.88 % (1570755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570755)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570755)Termination reason: Instruction limit
% 116.24/19.88 % (1570755)Termination phase: Saturation
% 116.24/19.88 % (1570755)Time elapsed: 8.251 s
% 116.24/19.88 % (1570755)Peak memory usage: 195 MB
% 116.24/19.88 % (1570755)Instructions burned: 8478 (million)
% 116.24/19.88 % (1570797)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3104832113:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2867 on theBenchmark for (2867ds/1670Mi)
% 116.24/19.88 % (1570797)Instruction limit reached!
% 116.24/19.88 % (1570797)------------------------------
% 116.24/19.88 % (1570797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570797)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570797)Termination reason: Instruction limit
% 116.24/19.88 % (1570797)Termination phase: Saturation
% 116.24/19.88 % (1570797)Time elapsed: 1.718 s
% 116.24/19.88 % (1570797)Peak memory usage: 136 MB
% 116.24/19.88 % (1570797)Instructions burned: 1671 (million)
% 116.24/19.88 % (1570801)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=4185038924:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2847 on theBenchmark for (2847ds/1722Mi)
% 116.24/19.88 % (1570789)Instruction limit reached!
% 116.24/19.88 % (1570789)------------------------------
% 116.24/19.88 % (1570789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570789)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570789)Termination reason: Instruction limit
% 116.24/19.88 % (1570789)Termination phase: Saturation
% 116.24/19.88 % (1570789)Time elapsed: 3.981 s
% 116.24/19.88 % (1570789)Peak memory usage: 159 MB
% 116.24/19.88 % (1570789)Instructions burned: 4124 (million)
% 116.24/19.88 % (1570805)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=288369843:cts=off:cond=on:i=9530:bs=on:fsd=on_2841 on theBenchmark for (2841ds/9530Mi)
% 116.24/19.88 % (1570801)Instruction limit reached!
% 116.24/19.88 % (1570801)------------------------------
% 116.24/19.88 % (1570801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570801)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570801)Termination reason: Instruction limit
% 116.24/19.88 % (1570801)Termination phase: Saturation
% 116.24/19.88 % (1570801)Time elapsed: 1.793 s
% 116.24/19.88 % (1570801)Peak memory usage: 136 MB
% 116.24/19.88 % (1570801)Instructions burned: 1722 (million)
% 116.24/19.88 % (1570784)Instruction limit reached!
% 116.24/19.88 % (1570784)------------------------------
% 116.24/19.88 % (1570784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 116.24/19.88 % (1570784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 116.24/19.88 % (1570784)CaDiCaL version: 2.1.3
% 116.24/19.88 % (1570784)Termination reason: Instruction limit
% 116.24/19.88 % (1570784)Termination phase: Saturation
% 116.24/19.88 % (1570784)Time elapsed: 6.801 s
% 116.24/19.88 % (1570784)Peak memory usage: 183 MB
% 116.24/19.88 % (1570784)Instructions burned: 6923 (million)
% 116.24/19.88 % (1570811)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=421728047:st=2:i=4495:sd=10:ss=included_2827 on theBenchmark for (2827ds/4495Mi)
% 116.24/19.88 % (1570812)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=1271738597:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2826 on theBenchmark for (2826ds/4920Mi)
% 116.24/19.88 % (1570665)First to succeed.
% 116.24/19.88 % (1570665)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1570651"
% 116.24/19.88 % (1570665)Refutation found. Thanks to Tanya!
% 116.24/19.88 % SZS status Unsatisfiable for theBenchmark
% 116.24/19.88 % SZS output start Proof for theBenchmark
% See solution above
% 136.14/20.12 % (1570665)------------------------------
% 136.14/20.12 % (1570665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 136.14/20.12 % (1570665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.14/20.12 % (1570665)CaDiCaL version: 2.1.3
% 136.14/20.12 % (1570665)Termination reason: Refutation
% 136.14/20.12 % (1570665)Time elapsed: 18.423 s
% 136.14/20.12 % (1570665)Peak memory usage: 239 MB
% 136.14/20.12 % (1570665)Instructions burned: 17936 (million)
% 136.14/20.12 % (1570665)------------------------------
% 136.14/20.12 % (1570665)------------------------------
% 136.14/20.12 % (1570651)Success in time 19.115 s
% 136.14/20.12 % Vampire exiting
%------------------------------------------------------------------------------