%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL021-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 : n004.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:56 AM UTC 2026
% Result : Unsatisfiable 94.55s 14.60s
% Output : Refutation 94.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 3
% Syntax : Number of formulae : 115 ( 16 unt; 0 def)
% Number of atoms : 256 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 285 ( 144 ~; 141 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 6 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 344 ( 344 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ~ is_a_theorem(equivalent(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(equivalent(X0,equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X0),X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xhn) ).
fof(f3,negated_conjecture,
~ is_a_theorem(equivalent(a,equivalent(equivalent(b,c),equivalent(equivalent(a,c),b)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_xhk) ).
fof(f4,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X0),X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f1,f2]) ).
fof(f5,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X2,X0),X1))
| ~ is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f4,f1]) ).
fof(f6,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,X2))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(X0) ),
inference(resolution,[],[f5,f1]) ).
fof(f7,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X1,X2),X0)))
| ~ is_a_theorem(equivalent(X3,X2))
| is_a_theorem(X3) ),
inference(resolution,[],[f6,f2]) ).
fof(f10,plain,
! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(X0)
| ~ is_a_theorem(X1) ),
inference(resolution,[],[f7,f4]) ).
fof(f12,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,X0),X1)))
| is_a_theorem(X0) ),
inference(resolution,[],[f10,f2]) ).
fof(f13,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,X2),X0))
| is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f10,f4]) ).
fof(f19,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X1,equivalent(X2,X3)),X0)),X2))
| ~ is_a_theorem(X3) ),
inference(resolution,[],[f13,f2]) ).
fof(f23,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,X0)),X1)))
| ~ is_a_theorem(X3) ),
inference(resolution,[],[f19,f10]) ).
fof(f27,plain,
! [X3,X0] :
( is_a_theorem(equivalent(X3,X0))
| ~ is_a_theorem(X0)
| ~ is_a_theorem(X3) ),
inference(forward_literal_rewriting,[],[f23,f12]) ).
fof(f32,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X1),X2))
| ~ is_a_theorem(equivalent(X2,X0))
| is_a_theorem(X1) ),
inference(resolution,[],[f27,f12]) ).
fof(f48,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X1,equivalent(X2,X3)),X0)),X2))
| is_a_theorem(X3) ),
inference(resolution,[],[f32,f2]) ).
fof(f61,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X3,equivalent(X1,X0)),X2))
| ~ is_a_theorem(equivalent(X1,equivalent(X2,X3)))
| is_a_theorem(X0) ),
inference(resolution,[],[f48,f5]) ).
fof(f176,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(equivalent(X2,equivalent(X3,equivalent(X0,X4))),X1)),X3)))
| is_a_theorem(X4) ),
inference(resolution,[],[f61,f2]) ).
fof(f178,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X1,equivalent(X3,X0))))
| is_a_theorem(X3)
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f61,f19]) ).
fof(f212,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(X1,X0),X2))))
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f178,f2]) ).
fof(f219,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(equivalent(X2,X1),X0)))
| is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f212,f10]) ).
fof(f229,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X1,X0),X1),X2))
| is_a_theorem(X0)
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f219,f212]) ).
fof(f237,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X1,X0)))
| is_a_theorem(X0)
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f229,f4]) ).
fof(f243,plain,
! [X2,X0,X1] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(X2,X0),X2)) ),
inference(resolution,[],[f229,f27]) ).
fof(f244,plain,
! [X2,X0,X1] :
( is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(equivalent(equivalent(X2,X0),X2)) ),
inference(duplicate_literal_removal,[],[f243]) ).
fof(f245,plain,
! [X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X1),X0))
| is_a_theorem(X1) ),
inference(condensation,[],[f244]) ).
fof(f251,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X0),X2)),X1))
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f245,f19]) ).
fof(f255,plain,
! [X0,X1] :
( is_a_theorem(equivalent(equivalent(X1,X1),X0))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f251,f245]) ).
fof(f282,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X1,equivalent(X2,X2)))
| is_a_theorem(X1) ),
inference(resolution,[],[f255,f6]) ).
fof(f287,plain,
! [X2,X3,X0,X1,X4] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(equivalent(X1,equivalent(X2,equivalent(equivalent(X3,X3),X4))),X0)),X2))
| is_a_theorem(X4) ),
inference(resolution,[],[f255,f176]) ).
fof(f290,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(equivalent(X1,equivalent(X2,X2)))
| is_a_theorem(X1) ),
inference(duplicate_literal_removal,[],[f282]) ).
fof(f291,plain,
! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,X1)))
| is_a_theorem(X0) ),
inference(condensation,[],[f290]) ).
fof(f293,plain,
! [X3,X4] :
( ~ is_a_theorem(equivalent(equivalent(X3,X3),X4))
| is_a_theorem(X4) ),
inference(forward_literal_rewriting,[],[f287,f19]) ).
fof(f516,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,equivalent(X0,X1)),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f237,f212]) ).
fof(f545,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X1)
| is_a_theorem(equivalent(X2,equivalent(X2,X0)))
| ~ is_a_theorem(X1) ),
inference(resolution,[],[f516,f10]) ).
fof(f561,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| ~ is_a_theorem(X1)
| is_a_theorem(equivalent(X2,equivalent(X2,X0))) ),
inference(duplicate_literal_removal,[],[f545]) ).
fof(f562,plain,
! [X0,X1] :
( is_a_theorem(equivalent(X1,equivalent(X1,X0)))
| ~ is_a_theorem(X0) ),
inference(condensation,[],[f561]) ).
fof(f597,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X1,X2),X0),X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X2) ),
inference(resolution,[],[f562,f32]) ).
fof(f659,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,equivalent(X2,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f597,f5]) ).
fof(f661,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(X0)
| is_a_theorem(X1)
| ~ is_a_theorem(equivalent(X2,equivalent(X2,X1))) ),
inference(duplicate_literal_removal,[],[f659]) ).
fof(f662,plain,
! [X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X0,X1)))
| is_a_theorem(X1) ),
inference(condensation,[],[f661]) ).
fof(f665,plain,
! [X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X0)),X1)),
inference(resolution,[],[f662,f2]) ).
fof(f683,plain,
! [X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(X1,X0)))
| ~ is_a_theorem(X1) ),
inference(resolution,[],[f665,f10]) ).
fof(f775,plain,
! [X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(X1,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f683,f293]) ).
fof(f821,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X3,X3),X0)))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| is_a_theorem(X2) ),
inference(resolution,[],[f775,f61]) ).
fof(f1050,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X0),equivalent(X1,X2)))
| is_a_theorem(X2) ),
inference(resolution,[],[f821,f2]) ).
fof(f1081,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X1,X0),X1)),X2))
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f1050,f212]) ).
fof(f1227,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),X0),X2),X1))
| is_a_theorem(X2) ),
inference(resolution,[],[f1081,f12]) ).
fof(f2559,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X1,equivalent(X2,X0)),equivalent(X1,X2)))
| ~ is_a_theorem(X0) ),
inference(resolution,[],[f19,f1227]) ).
fof(f2617,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(X2,X0)))
| ~ is_a_theorem(X0)
| is_a_theorem(equivalent(X1,X2)) ),
inference(resolution,[],[f2559,f1]) ).
fof(f2624,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X1,equivalent(X2,X0)))
| ~ is_a_theorem(equivalent(equivalent(X0,X1),X2)) ),
inference(resolution,[],[f2617,f2]) ).
fof(f2662,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X0,X1)),equivalent(X1,X2)))
| is_a_theorem(X2) ),
inference(resolution,[],[f2624,f12]) ).
fof(f2668,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X1)),X2))
| is_a_theorem(equivalent(X2,X0)) ),
inference(resolution,[],[f2624,f293]) ).
fof(f2702,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X2)))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X3)))
| is_a_theorem(X3) ),
inference(resolution,[],[f2624,f821]) ).
fof(f2712,plain,
~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(a,c),b),a),equivalent(b,c))),
inference(resolution,[],[f2624,f3]) ).
fof(f2716,plain,
! [X3,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,X3)))
| ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(X3) ),
inference(forward_literal_rewriting,[],[f2702,f775]) ).
fof(f2970,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X2,X0),X1))
| ~ is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(resolution,[],[f2716,f2]) ).
fof(f2976,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(equivalent(X1,X0),X2))
| ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X2) ),
inference(resolution,[],[f2716,f212]) ).
fof(f3041,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X1),X2)))
| is_a_theorem(equivalent(X2,X0)) ),
inference(resolution,[],[f2970,f291]) ).
fof(f3071,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(X2,X0))
| is_a_theorem(X1) ),
inference(resolution,[],[f2970,f1]) ).
fof(f3084,plain,
! [X0,X1] : is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X0),X1)),
inference(resolution,[],[f3041,f2]) ).
fof(f3095,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(equivalent(X2,X2),X0),X1)))),
inference(resolution,[],[f3041,f665]) ).
fof(f3108,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(equivalent(equivalent(X3,X3),X0),X1)))
| is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(resolution,[],[f3041,f2970]) ).
fof(f3120,plain,
! [X0,X1] : is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X0,X1)))),
inference(forward_literal_rewriting,[],[f3084,f2624]) ).
fof(f3123,plain,
! [X0,X1] : is_a_theorem(equivalent(equivalent(X0,equivalent(X0,X1)),X1)),
inference(resolution,[],[f3120,f2662]) ).
fof(f3162,plain,
! [X0,X1] : is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X1,X0))),
inference(forward_literal_rewriting,[],[f3123,f2624]) ).
fof(f3168,plain,
! [X0,X1] : is_a_theorem(equivalent(X1,equivalent(equivalent(X1,X0),X0))),
inference(forward_literal_rewriting,[],[f3162,f2624]) ).
fof(f3299,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),X1))
| is_a_theorem(equivalent(X2,X0)) ),
inference(resolution,[],[f3071,f2]) ).
fof(f3302,plain,
! [X0,X1] :
( is_a_theorem(equivalent(X1,X0))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(resolution,[],[f3071,f3168]) ).
fof(f3338,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(X1,equivalent(X0,X1))))
| is_a_theorem(equivalent(X2,X0)) ),
inference(forward_literal_rewriting,[],[f3299,f2970]) ).
fof(f3471,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(equivalent(X2,equivalent(X1,X2)),X0)) ),
inference(resolution,[],[f3338,f3302]) ).
fof(f3478,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,X1),X2))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X3,equivalent(X2,X3)),X0))) ),
inference(resolution,[],[f3338,f2970]) ).
fof(f3485,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X3,equivalent(X2,X3)),X0)))
| is_a_theorem(equivalent(X1,equivalent(X2,X0))) ),
inference(forward_literal_rewriting,[],[f3478,f2624]) ).
fof(f3492,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X0,X2)))
| is_a_theorem(equivalent(X0,X1)) ),
inference(forward_literal_rewriting,[],[f3471,f2970]) ).
fof(f3509,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(equivalent(X0,X2),X1)))
| is_a_theorem(equivalent(X0,X1)) ),
inference(forward_literal_rewriting,[],[f3492,f2970]) ).
fof(f3593,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X2),X1),X2)) ),
inference(resolution,[],[f3509,f3302]) ).
fof(f3605,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(X2,equivalent(X0,X2))))
| is_a_theorem(equivalent(X0,X1)) ),
inference(forward_literal_rewriting,[],[f3593,f2970]) ).
fof(f3631,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(equivalent(equivalent(X2,equivalent(X0,X2)),X1)) ),
inference(resolution,[],[f3605,f3302]) ).
fof(f3647,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2)))
| is_a_theorem(equivalent(X0,X1)) ),
inference(forward_literal_rewriting,[],[f3631,f2970]) ).
fof(f3652,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(equivalent(X1,X2),X0)))
| is_a_theorem(equivalent(X0,X1)) ),
inference(forward_literal_rewriting,[],[f3647,f2970]) ).
fof(f3800,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(equivalent(equivalent(equivalent(X2,X2),X0),X1)) ),
inference(resolution,[],[f3095,f2716]) ).
fof(f3806,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X1),X2),equivalent(X0,X2)))),
inference(resolution,[],[f3095,f3509]) ).
fof(f3829,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(X1,equivalent(X2,X2))))
| ~ is_a_theorem(equivalent(X0,X1)) ),
inference(forward_literal_rewriting,[],[f3800,f2624]) ).
fof(f4118,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X3,equivalent(X1,X0)))
| is_a_theorem(X3) ),
inference(resolution,[],[f2976,f6]) ).
fof(f4123,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X0,X1))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equivalent(X3,equivalent(X1,X0)))
| is_a_theorem(X3) ),
inference(duplicate_literal_removal,[],[f4118]) ).
fof(f4124,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(X1,X0)))
| ~ is_a_theorem(equivalent(X0,X1))
| is_a_theorem(X2) ),
inference(condensation,[],[f4123]) ).
fof(f4499,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X1),X2)))
| is_a_theorem(equivalent(X0,X2)) ),
inference(resolution,[],[f3806,f2716]) ).
fof(f4588,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(equivalent(X0,X1),X2))
| ~ is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X3,X3),X2),X0))) ),
inference(resolution,[],[f4499,f2970]) ).
fof(f4595,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X3,X3),X2),X0)))
| is_a_theorem(equivalent(X1,equivalent(X2,X0))) ),
inference(forward_literal_rewriting,[],[f4588,f2624]) ).
fof(f5465,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(equivalent(X3,X3),X1),X2),X0)) ),
inference(resolution,[],[f4595,f3302]) ).
fof(f5488,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(X0,equivalent(equivalent(X3,X3),X1))))
| is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(forward_literal_rewriting,[],[f5465,f2970]) ).
fof(f5701,plain,
! [X2,X3,X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(X3,X3),X1)),X2)) ),
inference(resolution,[],[f5488,f3302]) ).
fof(f5719,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X3,X3),X1),equivalent(X2,X0)))
| is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(forward_literal_rewriting,[],[f5701,f2970]) ).
fof(f5736,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X0),equivalent(X3,X3))))
| is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(forward_literal_rewriting,[],[f5719,f2970]) ).
fof(f5744,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(X1,equivalent(X2,X0))) ),
inference(forward_literal_rewriting,[],[f5736,f3829]) ).
fof(f5785,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(X1,X0))
| is_a_theorem(X2) ),
inference(resolution,[],[f5744,f4124]) ).
fof(f6419,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X1),X2))
| is_a_theorem(equivalent(equivalent(X1,X2),X0)) ),
inference(resolution,[],[f5785,f2]) ).
fof(f6480,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(X2,X0)))
| is_a_theorem(equivalent(equivalent(X1,X2),X0)) ),
inference(forward_literal_rewriting,[],[f6419,f2970]) ).
fof(f6489,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X2,equivalent(X0,X1)))
| ~ is_a_theorem(equivalent(X1,equivalent(X2,X0))) ),
inference(forward_literal_rewriting,[],[f6480,f2624]) ).
fof(f7347,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(X1,equivalent(equivalent(equivalent(X1,X2),X0),X2)))),
inference(resolution,[],[f3485,f2]) ).
fof(f7355,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X2,equivalent(X0,equivalent(X3,equivalent(X1,X3)))))
| is_a_theorem(equivalent(X0,equivalent(X1,X2))) ),
inference(resolution,[],[f3485,f6489]) ).
fof(f7466,plain,
! [X2,X0,X1] :
( is_a_theorem(equivalent(X0,equivalent(X1,X2)))
| ~ is_a_theorem(equivalent(X1,equivalent(X0,X2))) ),
inference(resolution,[],[f7355,f212]) ).
fof(f7644,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X1,X2)))
| is_a_theorem(equivalent(X2,X0)) ),
inference(resolution,[],[f7466,f3652]) ).
fof(f7672,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(equivalent(X0,X0),X1),equivalent(X2,X3)))
| is_a_theorem(equivalent(X1,equivalent(X3,X2))) ),
inference(resolution,[],[f7466,f3108]) ).
fof(f7696,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X2,X3),equivalent(X0,X0))))
| is_a_theorem(equivalent(X1,equivalent(X3,X2))) ),
inference(forward_literal_rewriting,[],[f7672,f2970]) ).
fof(f7717,plain,
! [X2,X0,X1] :
( ~ is_a_theorem(equivalent(X1,equivalent(equivalent(X1,X2),X0)))
| is_a_theorem(equivalent(X2,X0)) ),
inference(forward_literal_rewriting,[],[f7644,f2970]) ).
fof(f7737,plain,
! [X2,X3,X1] :
( is_a_theorem(equivalent(X1,equivalent(X3,X2)))
| ~ is_a_theorem(equivalent(X1,equivalent(X2,X3))) ),
inference(forward_literal_rewriting,[],[f7696,f3829]) ).
fof(f7944,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X1)),equivalent(X2,X3)))
| is_a_theorem(equivalent(equivalent(X3,X2),X0)) ),
inference(resolution,[],[f7737,f2668]) ).
fof(f8068,plain,
! [X2,X3,X0,X1] :
( ~ is_a_theorem(equivalent(equivalent(X1,X1),equivalent(equivalent(X2,X3),X0)))
| is_a_theorem(equivalent(equivalent(X3,X2),X0)) ),
inference(forward_literal_rewriting,[],[f7944,f2970]) ).
fof(f8099,plain,
! [X2,X3,X0] :
( ~ is_a_theorem(equivalent(equivalent(X2,X3),X0))
| is_a_theorem(equivalent(equivalent(X3,X2),X0)) ),
inference(forward_literal_rewriting,[],[f8068,f255]) ).
fof(f8111,plain,
! [X2,X3,X0] :
( ~ is_a_theorem(equivalent(X3,equivalent(X0,X2)))
| is_a_theorem(equivalent(equivalent(X3,X2),X0)) ),
inference(forward_literal_rewriting,[],[f8099,f2970]) ).
fof(f8117,plain,
! [X2,X3,X0] :
( is_a_theorem(equivalent(X2,equivalent(X0,X3)))
| ~ is_a_theorem(equivalent(X3,equivalent(X0,X2))) ),
inference(forward_literal_rewriting,[],[f8111,f2624]) ).
fof(f8341,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(equivalent(X1,X0),X2),X1),X2))),
inference(resolution,[],[f7347,f7717]) ).
fof(f8350,plain,
! [X2,X0,X1] : is_a_theorem(equivalent(X0,equivalent(X2,equivalent(equivalent(equivalent(X1,X0),X2),X1)))),
inference(forward_literal_rewriting,[],[f8341,f7737]) ).
fof(f8420,plain,
~ is_a_theorem(equivalent(c,equivalent(b,equivalent(equivalent(equivalent(a,c),b),a)))),
inference(resolution,[],[f8117,f2712]) ).
fof(f8603,plain,
$false,
inference(forward_subsumption_resolution,[],[f8420,f8350]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL021-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.20/0.47 % Computer : n004.cluster.edu
% 0.20/0.47 % Model : x86_64 x86_64
% 0.20/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.47 % Memory : 8046.5625MB
% 0.20/0.47 % OS : Linux 6.8.0-71-generic
% 0.20/0.48 % CPULimit : 300
% 0.20/0.48 % WCLimit : 300
% 0.20/0.48 % DateTime : Sun Sep 27 15:17:37 UTC 2026
% 0.20/0.48 % CPUTime :
% 0.20/0.48 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.54 Running first-order theorem proving
% 0.25/0.54 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
% 16.95/3.76 % (3648801)Input is clausal, will run a generic CNF schedule.
% 16.95/3.76 % (3648810)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2075613334:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 16.95/3.76 % (3648810)Instruction limit reached!
% 16.95/3.76 % (3648810)------------------------------
% 16.95/3.76 % (3648810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.76 % (3648810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.76 % (3648810)CaDiCaL version: 2.1.3
% 16.95/3.76 % (3648810)Termination reason: Instruction limit
% 16.95/3.76 % (3648810)Termination phase: Saturation
% 16.95/3.76 % (3648810)Time elapsed: 0.056 s
% 16.95/3.76 % (3648810)Peak memory usage: 88 MB
% 16.95/3.76 % (3648810)Instructions burned: 114 (million)
% 16.95/3.76 % (3648809)lrs+10_1_sil=8000:sp=occurrence:random_seed=2169816965:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 16.95/3.76 % (3648808)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4116529277:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 16.95/3.76 % (3648806)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=1548255048:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 16.95/3.76 % (3648807)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=178271363:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 16.95/3.76 % (3648812)dis-21_1_sil=8000:lcm=predicate:random_seed=2807918620:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 16.95/3.76 % (3648811)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1305754188:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 16.95/3.76 % (3648809)Instruction limit reached!
% 16.95/3.76 % (3648809)------------------------------
% 16.95/3.76 % (3648809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.76 % (3648809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.76 % (3648809)CaDiCaL version: 2.1.3
% 16.95/3.76 % (3648809)Termination reason: Instruction limit
% 16.95/3.76 % (3648809)Termination phase: Saturation
% 16.95/3.76 % (3648809)Time elapsed: 0.095 s
% 16.95/3.76 % (3648809)Peak memory usage: 88 MB
% 16.95/3.76 % (3648809)Instructions burned: 107 (million)
% 16.95/3.76 % (3648812)Instruction limit reached!
% 16.95/3.76 % (3648812)------------------------------
% 16.95/3.76 % (3648812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.76 % (3648812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.76 % (3648812)CaDiCaL version: 2.1.3
% 16.95/3.76 % (3648812)Termination reason: Instruction limit
% 16.95/3.76 % (3648812)Termination phase: Saturation
% 16.95/3.76 % (3648812)Time elapsed: 0.111 s
% 16.95/3.76 % (3648812)Peak memory usage: 88 MB
% 16.95/3.76 % (3648812)Instructions burned: 117 (million)
% 16.95/3.76 % (3648811)Instruction limit reached!
% 16.95/3.76 % (3648811)------------------------------
% 16.95/3.76 % (3648811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.76 % (3648811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.76 % (3648811)CaDiCaL version: 2.1.3
% 16.95/3.76 % (3648811)Termination reason: Instruction limit
% 16.95/3.76 % (3648811)Termination phase: Saturation
% 16.95/3.76 % (3648811)Time elapsed: 0.178 s
% 16.95/3.76 % (3648811)Peak memory usage: 89 MB
% 16.95/3.76 % (3648811)Instructions burned: 181 (million)
% 16.95/3.76 % (3648818)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=1836507622:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 16.95/3.76 % (3648818)Refutation not found, incomplete strategy
% 16.95/3.76 % (3648818)------------------------------
% 16.95/3.76 % (3648818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.95/3.76 % (3648818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.95/3.76 % (3648818)CaDiCaL version: 2.1.3
% 16.95/3.76 % (3648818)Termination reason: Refutation not found, incomplete strategy
% 16.95/3.76 % (3648818)Time elapsed: 0.001 s
% 16.95/3.76 % (3648818)Peak memory usage: 87 MB
% 16.95/3.76 % (3648821)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1753793980:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 36.15/6.36 % (3648822)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4032391502:st=4:i=219:sd=3:ss=axioms_2995 on theBenchmark for (2995ds/219Mi)
% 36.15/6.36 % (3648822)Refutation not found, incomplete strategy
% 36.15/6.36 % (3648822)------------------------------
% 36.15/6.36 % (3648822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.15/6.36 % (3648822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.15/6.36 % (3648822)CaDiCaL version: 2.1.3
% 36.15/6.36 % (3648822)Termination reason: Refutation not found, incomplete strategy
% 36.15/6.36 % (3648822)Time elapsed: 0.001 s
% 36.15/6.36 % (3648822)Peak memory usage: 87 MB
% 36.15/6.36 % (3648818)------------------------------
% 36.15/6.36 % (3648818)------------------------------
% 36.15/6.36 % (3648823)lrs+10_64_to=lpo:sil=8000:random_seed=1857159185:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 36.15/6.36 % (3648821)Instruction limit reached!
% 36.15/6.36 % (3648821)------------------------------
% 36.15/6.36 % (3648821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.15/6.36 % (3648821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.15/6.36 % (3648821)CaDiCaL version: 2.1.3
% 36.15/6.36 % (3648821)Termination reason: Instruction limit
% 36.15/6.36 % (3648821)Termination phase: Saturation
% 36.15/6.36 % (3648821)Time elapsed: 0.176 s
% 36.15/6.36 % (3648821)Peak memory usage: 89 MB
% 36.15/6.36 % (3648821)Instructions burned: 190 (million)
% 36.15/6.36 % (3648823)Instruction limit reached!
% 36.15/6.36 % (3648823)------------------------------
% 36.15/6.36 % (3648823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.15/6.36 % (3648823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.15/6.36 % (3648823)CaDiCaL version: 2.1.3
% 36.15/6.36 % (3648823)Termination reason: Instruction limit
% 36.15/6.36 % (3648823)Termination phase: Saturation
% 36.15/6.36 % (3648823)Time elapsed: 0.120 s
% 36.15/6.36 % (3648823)Peak memory usage: 88 MB
% 36.15/6.36 % (3648823)Instructions burned: 127 (million)
% 36.15/6.36 % (3648827)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=227820745:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 36.15/6.36 % (3648822)------------------------------
% 36.15/6.36 % (3648822)------------------------------
% 36.15/6.36 % (3648827)Instruction limit reached!
% 36.15/6.36 % (3648827)------------------------------
% 36.15/6.36 % (3648827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.15/6.36 % (3648827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.15/6.36 % (3648827)CaDiCaL version: 2.1.3
% 36.15/6.36 % (3648827)Termination reason: Instruction limit
% 36.15/6.36 % (3648827)Termination phase: Saturation
% 36.15/6.36 % (3648827)Time elapsed: 0.114 s
% 36.15/6.36 % (3648827)Peak memory usage: 89 MB
% 36.15/6.36 % (3648827)Instructions burned: 201 (million)
% 36.15/6.36 % (3648829)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3754322072:i=157:gtg=all_2991 on theBenchmark for (2991ds/157Mi)
% 36.15/6.36 % (3648830)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2549953312:i=3394:sd=4:ss=included:sgt=64_2991 on theBenchmark for (2991ds/3394Mi)
% 36.15/6.36 % (3648829)Instruction limit reached!
% 36.15/6.36 % (3648829)------------------------------
% 36.15/6.36 % (3648829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.15/6.36 % (3648829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.15/6.36 % (3648829)CaDiCaL version: 2.1.3
% 36.15/6.36 % (3648829)Termination reason: Instruction limit
% 36.15/6.36 % (3648829)Termination phase: Saturation
% 36.15/6.36 % (3648829)Time elapsed: 0.162 s
% 36.15/6.36 % (3648829)Peak memory usage: 90 MB
% 36.15/6.36 % (3648829)Instructions burned: 157 (million)
% 36.15/6.36 % (3648833)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4162299588:i=107_2989 on theBenchmark for (2989ds/107Mi)
% 36.15/6.36 % (3648833)Refutation not found, incomplete strategy
% 36.15/6.36 % (3648833)------------------------------
% 36.15/6.36 % (3648833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.15/6.36 % (3648833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.15/6.36 % (3648833)CaDiCaL version: 2.1.3
% 51.68/8.60 % (3648833)Termination reason: Refutation not found, incomplete strategy
% 51.68/8.60 % (3648833)Time elapsed: 0.001 s
% 51.68/8.60 % (3648833)Peak memory usage: 87 MB
% 51.68/8.60 % (3648832)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=2900896123:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 51.68/8.60 % (3648832)Instruction limit reached!
% 51.68/8.60 % (3648832)------------------------------
% 51.68/8.60 % (3648832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.68/8.60 % (3648832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.68/8.60 % (3648832)CaDiCaL version: 2.1.3
% 51.68/8.60 % (3648832)Termination reason: Instruction limit
% 51.68/8.60 % (3648832)Termination phase: Saturation
% 51.68/8.60 % (3648832)Time elapsed: 0.095 s
% 51.68/8.60 % (3648832)Peak memory usage: 88 MB
% 51.68/8.60 % (3648832)Instructions burned: 106 (million)
% 51.68/8.60 % (3648833)------------------------------
% 51.68/8.60 % (3648833)------------------------------
% 51.68/8.60 % (3648836)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3647800978:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 51.68/8.60 % (3648839)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3195555320:cond=fast:i=5208:av=off_2985 on theBenchmark for (2985ds/5208Mi)
% 51.68/8.60 % (3648840)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2856571880:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 51.68/8.60 % (3648836)Instruction limit reached!
% 51.68/8.60 % (3648836)------------------------------
% 51.68/8.60 % (3648836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.68/8.60 % (3648836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.68/8.60 % (3648836)CaDiCaL version: 2.1.3
% 51.68/8.60 % (3648836)Termination reason: Instruction limit
% 51.68/8.60 % (3648836)Termination phase: Saturation
% 51.68/8.60 % (3648836)Time elapsed: 0.205 s
% 51.68/8.60 % (3648836)Peak memory usage: 89 MB
% 51.68/8.60 % (3648836)Instructions burned: 243 (million)
% 51.68/8.60 % (3648840)Instruction limit reached!
% 51.68/8.60 % (3648840)------------------------------
% 51.68/8.60 % (3648840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.68/8.60 % (3648840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.68/8.60 % (3648840)CaDiCaL version: 2.1.3
% 51.68/8.60 % (3648840)Termination reason: Instruction limit
% 51.68/8.60 % (3648840)Termination phase: Saturation
% 51.68/8.60 % (3648840)Time elapsed: 0.077 s
% 51.68/8.60 % (3648840)Peak memory usage: 89 MB
% 51.68/8.60 % (3648840)Instructions burned: 136 (million)
% 51.68/8.60 % (3648844)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1781674942:i=499:bd=all_2982 on theBenchmark for (2982ds/499Mi)
% 51.68/8.60 % (3648845)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=833356073:i=191:fgj=on:bd=all_2981 on theBenchmark for (2981ds/191Mi)
% 51.68/8.60 % (3648845)Instruction limit reached!
% 51.68/8.60 % (3648845)------------------------------
% 51.68/8.60 % (3648845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.68/8.60 % (3648845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.68/8.60 % (3648845)CaDiCaL version: 2.1.3
% 51.68/8.60 % (3648845)Termination reason: Instruction limit
% 51.68/8.60 % (3648845)Termination phase: Saturation
% 51.68/8.60 % (3648845)Time elapsed: 0.098 s
% 51.68/8.60 % (3648845)Peak memory usage: 89 MB
% 51.68/8.60 % (3648845)Instructions burned: 194 (million)
% 51.68/8.60 % (3648844)Instruction limit reached!
% 51.68/8.60 % (3648844)------------------------------
% 51.68/8.60 % (3648844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.68/8.60 % (3648844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.68/8.60 % (3648844)CaDiCaL version: 2.1.3
% 51.68/8.60 % (3648844)Termination reason: Instruction limit
% 51.68/8.60 % (3648844)Termination phase: Saturation
% 51.68/8.60 % (3648844)Time elapsed: 0.435 s
% 51.68/8.60 % (3648844)Peak memory usage: 90 MB
% 51.68/8.60 % (3648844)Instructions burned: 500 (million)
% 51.68/8.60 % (3648848)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3000129657:i=264:kws=precedence:fsr=off_2978 on theBenchmark for (2978ds/264Mi)
% 84.65/13.17 % (3648848)Instruction limit reached!
% 84.65/13.17 % (3648848)------------------------------
% 84.65/13.17 % (3648848)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/13.17 % (3648848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/13.17 % (3648848)CaDiCaL version: 2.1.3
% 84.65/13.17 % (3648848)Termination reason: Instruction limit
% 84.65/13.17 % (3648848)Termination phase: Saturation
% 84.65/13.17 % (3648848)Time elapsed: 0.162 s
% 84.65/13.17 % (3648848)Peak memory usage: 91 MB
% 84.65/13.17 % (3648848)Instructions burned: 264 (million)
% 84.65/13.17 % (3648849)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2035801663:cond=on:i=156:bs=on:gtg=exists_all:er=known_2975 on theBenchmark for (2975ds/156Mi)
% 84.65/13.17 % (3648849)Instruction limit reached!
% 84.65/13.17 % (3648849)------------------------------
% 84.65/13.17 % (3648849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/13.17 % (3648849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/13.17 % (3648849)CaDiCaL version: 2.1.3
% 84.65/13.17 % (3648849)Termination reason: Instruction limit
% 84.65/13.17 % (3648849)Termination phase: Saturation
% 84.65/13.17 % (3648849)Time elapsed: 0.157 s
% 84.65/13.17 % (3648849)Peak memory usage: 89 MB
% 84.65/13.17 % (3648849)Instructions burned: 157 (million)
% 84.65/13.17 % (3648851)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=3137886981:i=3256:kws=precedence:bd=preordered:av=off_2973 on theBenchmark for (2973ds/3256Mi)
% 84.65/13.17 % (3648853)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2544561557:i=537:av=off:ss=included_2970 on theBenchmark for (2970ds/537Mi)
% 84.65/13.17 % (3648853)Instruction limit reached!
% 84.65/13.17 % (3648853)------------------------------
% 84.65/13.17 % (3648853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/13.17 % (3648853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/13.17 % (3648853)CaDiCaL version: 2.1.3
% 84.65/13.17 % (3648853)Termination reason: Instruction limit
% 84.65/13.17 % (3648853)Termination phase: Saturation
% 84.65/13.17 % (3648853)Time elapsed: 0.454 s
% 84.65/13.17 % (3648853)Peak memory usage: 90 MB
% 84.65/13.17 % (3648853)Instructions burned: 538 (million)
% 84.65/13.17 % (3648856)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3762056533:i=180:bd=preordered:av=off_2963 on theBenchmark for (2963ds/180Mi)
% 84.65/13.17 % (3648856)Instruction limit reached!
% 84.65/13.17 % (3648856)------------------------------
% 84.65/13.17 % (3648856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/13.17 % (3648856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/13.17 % (3648856)CaDiCaL version: 2.1.3
% 84.65/13.17 % (3648856)Termination reason: Instruction limit
% 84.65/13.17 % (3648856)Termination phase: Saturation
% 84.65/13.17 % (3648856)Time elapsed: 0.159 s
% 84.65/13.17 % (3648856)Peak memory usage: 88 MB
% 84.65/13.17 % (3648856)Instructions burned: 181 (million)
% 84.65/13.17 % (3648858)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=3743670355:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2958 on theBenchmark for (2958ds/10307Mi)
% 84.65/13.17 % (3648830)Instruction limit reached!
% 84.65/13.17 % (3648830)------------------------------
% 84.65/13.17 % (3648830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/13.17 % (3648830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 84.65/13.17 % (3648830)CaDiCaL version: 2.1.3
% 84.65/13.17 % (3648830)Termination reason: Instruction limit
% 84.65/13.17 % (3648830)Termination phase: Saturation
% 84.65/13.17 % (3648830)Time elapsed: 3.510 s
% 84.65/13.17 % (3648830)Peak memory usage: 148 MB
% 84.65/13.17 % (3648830)Instructions burned: 3394 (million)
% 84.65/13.17 % (3648860)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=2320402807:i=412:gtgl=4:gtg=exists_all_2953 on theBenchmark for (2953ds/412Mi)
% 84.65/13.17 % (3648839)Instruction limit reached!
% 84.65/13.17 % (3648839)------------------------------
% 84.65/13.17 % (3648839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 84.65/13.17 % (3648839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.10/14.60 % (3648839)CaDiCaL version: 2.1.3
% 94.10/14.60 % (3648839)Termination reason: Instruction limit
% 94.10/14.60 % (3648839)Termination phase: Saturation
% 94.10/14.60 % (3648839)Time elapsed: 3.337 s
% 94.10/14.60 % (3648839)Peak memory usage: 161 MB
% 94.10/14.60 % (3648839)Instructions burned: 5210 (million)
% 94.10/14.60 % (3648862)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=3693946665:s2pl=no:i=8478:s2at=4:nm=6_2949 on theBenchmark for (2949ds/8478Mi)
% 94.10/14.60 % (3648860)Instruction limit reached!
% 94.10/14.60 % (3648860)------------------------------
% 94.10/14.60 % (3648860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.10/14.60 % (3648860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.10/14.60 % (3648860)CaDiCaL version: 2.1.3
% 94.10/14.60 % (3648860)Termination reason: Instruction limit
% 94.10/14.60 % (3648860)Termination phase: Saturation
% 94.10/14.60 % (3648860)Time elapsed: 0.430 s
% 94.10/14.60 % (3648860)Peak memory usage: 94 MB
% 94.10/14.60 % (3648860)Instructions burned: 412 (million)
% 94.10/14.60 % (3648864)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=1920793264: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)
% 94.10/14.60 % (3648864)Instruction limit reached!
% 94.10/14.60 % (3648864)------------------------------
% 94.10/14.60 % (3648864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.10/14.60 % (3648864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.10/14.60 % (3648864)CaDiCaL version: 2.1.3
% 94.10/14.60 % (3648864)Termination reason: Instruction limit
% 94.10/14.60 % (3648864)Termination phase: Saturation
% 94.10/14.60 % (3648864)Time elapsed: 0.270 s
% 94.10/14.60 % (3648864)Peak memory usage: 90 MB
% 94.10/14.60 % (3648864)Instructions burned: 304 (million)
% 94.10/14.60 % (3648851)Instruction limit reached!
% 94.10/14.60 % (3648851)------------------------------
% 94.10/14.60 % (3648851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.10/14.60 % (3648851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.10/14.60 % (3648851)CaDiCaL version: 2.1.3
% 94.10/14.60 % (3648851)Termination reason: Instruction limit
% 94.10/14.60 % (3648851)Termination phase: Saturation
% 94.10/14.60 % (3648851)Time elapsed: 3.303 s
% 94.10/14.60 % (3648851)Peak memory usage: 145 MB
% 94.10/14.60 % (3648851)Instructions burned: 3257 (million)
% 94.10/14.60 % (3648866)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=8235169:st=4:i=720:sd=3:fsr=off:ss=axioms_2939 on theBenchmark for (2939ds/720Mi)
% 94.10/14.60 % (3648867)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4153723278:i=598:bs=on:bd=preordered:av=off:ss=axioms_2937 on theBenchmark for (2937ds/598Mi)
% 94.10/14.60 % (3648866)Instruction limit reached!
% 94.10/14.60 % (3648866)------------------------------
% 94.10/14.60 % (3648866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.10/14.60 % (3648866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.10/14.60 % (3648866)CaDiCaL version: 2.1.3
% 94.10/14.60 % (3648866)Termination reason: Instruction limit
% 94.10/14.60 % (3648866)Termination phase: Saturation
% 94.10/14.60 % (3648866)Time elapsed: 0.630 s
% 94.10/14.60 % (3648866)Peak memory usage: 94 MB
% 94.10/14.60 % (3648866)Instructions burned: 720 (million)
% 94.10/14.60 % (3648867)Instruction limit reached!
% 94.10/14.60 % (3648867)------------------------------
% 94.10/14.60 % (3648867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.10/14.60 % (3648867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.10/14.60 % (3648867)CaDiCaL version: 2.1.3
% 94.10/14.60 % (3648867)Termination reason: Instruction limit
% 94.10/14.60 % (3648867)Termination phase: Saturation
% 94.10/14.60 % (3648867)Time elapsed: 0.521 s
% 94.10/14.60 % (3648867)Peak memory usage: 94 MB
% 94.10/14.60 % (3648867)Instructions burned: 599 (million)
% 94.10/14.60 % (3648870)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1510205223:i=2989:sd=3:ss=axioms:sgt=60_2930 on theBenchmark for (2930ds/2989Mi)
% 94.10/14.60 % (3648871)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=3359353316:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2929 on theBenchmark for (2929ds/1997Mi)
% 94.10/14.60 % (3648871)Instruction limit reached!
% 94.10/14.60 % (3648871)------------------------------
% 94.10/14.60 % (3648871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.10/14.60 % (3648871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.10/14.60 % (3648871)CaDiCaL version: 2.1.3
% 94.10/14.60 % (3648871)Termination reason: Instruction limit
% 94.10/14.60 % (3648871)Termination phase: Saturation
% 94.10/14.60 % (3648871)Time elapsed: 2.175 s
% 94.10/14.60 % (3648871)Peak memory usage: 136 MB
% 94.10/14.60 % (3648871)Instructions burned: 1998 (million)
% 94.10/14.60 % (3648862)Instruction limit reached!
% 94.10/14.60 % (3648862)------------------------------
% 94.10/14.60 % (3648862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.10/14.60 % (3648862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.10/14.60 % (3648862)CaDiCaL version: 2.1.3
% 94.10/14.60 % (3648862)Termination reason: Instruction limit
% 94.10/14.60 % (3648862)Termination phase: Saturation
% 94.10/14.60 % (3648862)Time elapsed: 4.152 s
% 94.10/14.60 % (3648862)Peak memory usage: 197 MB
% 94.55/14.60 % (3648862)Instructions burned: 8479 (million)
% 94.55/14.60 % (3648874)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=2664166613:i=2088:bd=preordered:av=off_2904 on theBenchmark for (2904ds/2088Mi)
% 94.55/14.60 % (3648875)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1016021345:i=1098:nicw=on_2904 on theBenchmark for (2904ds/1098Mi)
% 94.55/14.60 % (3648870)Instruction limit reached!
% 94.55/14.60 % (3648870)------------------------------
% 94.55/14.60 % (3648870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.55/14.60 % (3648870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.55/14.60 % (3648870)CaDiCaL version: 2.1.3
% 94.55/14.60 % (3648870)Termination reason: Instruction limit
% 94.55/14.60 % (3648870)Termination phase: Saturation
% 94.55/14.60 % (3648870)Time elapsed: 2.988 s
% 94.55/14.60 % (3648870)Peak memory usage: 146 MB
% 94.55/14.60 % (3648870)Instructions burned: 2990 (million)
% 94.55/14.60 % (3648875)Instruction limit reached!
% 94.55/14.60 % (3648875)------------------------------
% 94.55/14.60 % (3648875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.55/14.60 % (3648875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.55/14.60 % (3648875)CaDiCaL version: 2.1.3
% 94.55/14.60 % (3648875)Termination reason: Instruction limit
% 94.55/14.60 % (3648875)Termination phase: Saturation
% 94.55/14.60 % (3648875)Time elapsed: 0.486 s
% 94.55/14.60 % (3648875)Peak memory usage: 98 MB
% 94.55/14.60 % (3648875)Instructions burned: 1098 (million)
% 94.55/14.60 % (3648878)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4101172902:i=433:bd=preordered_2897 on theBenchmark for (2897ds/433Mi)
% 94.55/14.60 % (3648879)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3213992684: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)
% 94.55/14.60 % (3648878)Instruction limit reached!
% 94.55/14.60 % (3648878)------------------------------
% 94.55/14.60 % (3648878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.55/14.60 % (3648878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.55/14.60 % (3648878)CaDiCaL version: 2.1.3
% 94.55/14.60 % (3648878)Termination reason: Instruction limit
% 94.55/14.60 % (3648878)Termination phase: Saturation
% 94.55/14.60 % (3648878)Time elapsed: 0.221 s
% 94.55/14.60 % (3648878)Peak memory usage: 93 MB
% 94.55/14.60 % (3648878)Instructions burned: 434 (million)
% 94.55/14.60 % (3648882)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=3883290031:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2892 on theBenchmark for (2892ds/6922Mi)
% 94.55/14.60 % (3648874)Instruction limit reached!
% 94.55/14.60 % (3648874)------------------------------
% 94.55/14.60 % (3648874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.55/14.60 % (3648874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.55/14.60 % (3648874)CaDiCaL version: 2.1.3
% 94.55/14.60 % (3648874)Termination reason: Instruction limit
% 94.55/14.60 % (3648874)Termination phase: Saturation
% 94.55/14.60 % (3648874)Time elapsed: 2.131 s
% 94.55/14.60 % (3648874)Peak memory usage: 135 MB
% 94.55/14.60 % (3648874)Instructions burned: 2088 (million)
% 94.55/14.60 % (3648884)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=461182494:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2880 on theBenchmark for (2880ds/596Mi)
% 94.55/14.60 % (3648884)Instruction limit reached!
% 94.55/14.60 % (3648884)------------------------------
% 94.55/14.60 % (3648884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.55/14.60 % (3648884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.55/14.60 % (3648884)CaDiCaL version: 2.1.3
% 94.55/14.60 % (3648884)Termination reason: Instruction limit
% 94.55/14.60 % (3648884)Termination phase: Saturation
% 94.55/14.60 % (3648884)Time elapsed: 0.484 s
% 94.55/14.60 % (3648884)Peak memory usage: 95 MB
% 94.55/14.60 % (3648884)Instructions burned: 596 (million)
% 94.55/14.60 % (3648879)First to succeed.
% 94.55/14.60 % (3648879)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3648801"
% 94.55/14.60 % (3648886)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=830751624:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2873 on theBenchmark for (2873ds/4123Mi)
% 94.55/14.60 % (3648879)Refutation found. Thanks to Tanya!
% 94.55/14.60 % SZS status Unsatisfiable for theBenchmark
% 94.55/14.60 % SZS output start Proof for theBenchmark
% See solution above
% 94.85/14.98 % (3648879)------------------------------
% 94.85/14.98 % (3648879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.85/14.98 % (3648879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.85/14.98 % (3648879)CaDiCaL version: 2.1.3
% 94.85/14.98 % (3648879)Termination reason: Refutation
% 94.85/14.98 % (3648879)Time elapsed: 2.251 s
% 94.85/14.98 % (3648879)Peak memory usage: 137 MB
% 94.85/14.98 % (3648879)Instructions burned: 2105 (million)
% 94.85/14.98 % (3648879)------------------------------
% 94.85/14.98 % (3648879)------------------------------
% 94.85/14.98 % (3648801)Success in time 13.323 s
% 94.85/14.98 % Vampire exiting
%------------------------------------------------------------------------------