%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV915-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 01:19:47 PM UTC 2026
% Result : Unsatisfiable 57.78s 8.98s
% Output : Refutation 59.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 13
% Syntax : Number of formulae : 49 ( 26 unt; 0 def)
% Number of atoms : 87 ( 10 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 71 ( 33 ~; 38 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 17 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 33 ( 33 usr; 14 con; 0-6 aty)
% Number of variables : 161 ( 161 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f20,axiom,
! [X2,X3,X0,X1] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xexport__s__1(X0,X1,X3,X2))),tc_Com_Ostate,tc_bool,tc_bool)),X1),X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_export__s_0) ).
fof(f89,axiom,
! [X0,X1] : c_Collect(X0,X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f287,axiom,
! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_Collect(c_COMBK(c_False,tc_bool,X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__def_0) ).
fof(f404,axiom,
! [X0,X1] : c_Collect(hAPP(c_fequal(X0),X1),X0) = hAPP(c_Set_Oinsert(X1,X0),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_singleton__conv2_0) ).
fof(f405,plain,
! [X0,X1] : hAPP(c_Set_Oinsert(X1,X0),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) = c_Collect(hAPP(c_fequal(X0),X1),X0),
inference(reorient_equations,[],[f404]) ).
fof(f437,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| hBOOL(hAPP(hAPP(X4,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X6,X4)))
| ~ hBOOL(hAPP(hAPP(X6,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conseq_1) ).
fof(f442,axiom,
! [X2,X3,X0,X1] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conseq_0) ).
fof(f446,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(X3,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X4,X5)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conseq_2) ).
fof(f453,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),X1),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),X2)),tc_Com_Ostate,tc_bool,tc_bool)),hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),X1),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),X3),X1,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(X4)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),X5))),c_Com_Ocom_OLocal(X4,X5,X6),X7,X1),tc_Hoare__Mirabelle_Otriple(X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_bool))),X1)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X3,X6,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),X1),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),X7),X1,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(X4)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(X2,X4))),X1),tc_Hoare__Mirabelle_Otriple(X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_bool))),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_hoare__derivs_OLocal_0) ).
fof(f486,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(hAPP(hAPP(c_COMBB(X0,X1,X2),X3),X4),X5) = hAPP(X3,hAPP(X4,X5)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBB__def_0) ).
fof(f487,plain,
! [X2,X3,X0,X1,X4,X5] : hAPP(X3,hAPP(X4,X5)) = hAPP(hAPP(hAPP(c_COMBB(X0,X1,X2),X3),X4),X5),
inference(reorient_equations,[],[f486]) ).
fof(f488,axiom,
! [X2,X3,X0,X1,X4,X5] : hAPP(hAPP(c_COMBC(X0,X1,X2,X3),X4),X5) = hAPP(hAPP(X0,X5),X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_COMBC__def_0) ).
fof(f495,negated_conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f496,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),c_Com_Ocom_OLocal(v_Y,v_a,v_c),v_Q,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f497,negated_conjecture,
! [X2,X0,X1] :
( hBOOL(hAPP(hAPP(v_Q,X0),hAPP(hAPP(hAPP(c_Natural_Oupdate,X1),c_Com_Ovname_OLoc(v_Y)),X2)))
| ~ hBOOL(hAPP(hAPP(v_Q,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f531,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(hAPP(v_Q,X0),hAPP(hAPP(hAPP(c_Natural_Oupdate,X1),c_Com_Ovname_OLoc(v_Y)),X2)))
| hBOOL(hAPP(hAPP(v_Q,X0),X1)) ),
inference(consistent_polarity_flipping,[],[f497]) ).
fof(f539,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| hBOOL(hAPP(hAPP(X3,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X4,X5)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(consistent_polarity_flipping,[],[f446]) ).
fof(f543,plain,
! [X2,X3,X0,X1] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2))) ),
inference(consistent_polarity_flipping,[],[f442]) ).
fof(f548,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a)
| ~ hBOOL(hAPP(hAPP(X4,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X6,X4)))
| hBOOL(hAPP(hAPP(X6,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(consistent_polarity_flipping,[],[f437]) ).
fof(f777,plain,
! [X0,X1] : hAPP(c_Set_Oinsert(X1,X0),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))) = hAPP(c_fequal(X0),X1),
inference(forward_demodulation,[],[f405,f89]) ).
fof(f783,plain,
! [X0] : c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_COMBK(c_False,tc_bool,X0),
inference(forward_demodulation,[],[f287,f89]) ).
fof(f830,plain,
! [X2,X3,X0,X1] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xexport__s__1(X0,X1,X3,X2))),tc_Com_Ostate,tc_bool,tc_bool)),X1),X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(backward_demodulation,[],[f20,f777]) ).
fof(f835,plain,
! [X2,X3,X0,X1,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)
| hBOOL(hAPP(hAPP(X3,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X4,X5)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(backward_demodulation,[],[f539,f777]) ).
fof(f839,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(hAPP(X1,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a) ),
inference(backward_demodulation,[],[f543,f777]) ).
fof(f844,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)
| ~ hBOOL(hAPP(hAPP(X4,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X6,X4)))
| hBOOL(hAPP(hAPP(X6,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2)))
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) ),
inference(backward_demodulation,[],[f548,f777]) ).
fof(f846,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(X1)),c_Hoare__Mirabelle_Otriple_Otriple(X3,X6,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),X1),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),X7),X1,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(X4)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(X2,X4))),X1)),X1)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),X1),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),X2)),tc_Com_Ostate,tc_bool,tc_bool)),hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),X1),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),X3),X1,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(X4)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),X5))),c_Com_Ocom_OLocal(X4,X5,X6),X7,X1),tc_Hoare__Mirabelle_Otriple(X1)),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_bool))),X1) ),
inference(backward_demodulation,[],[f453,f777]) ).
fof(f851,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),c_Com_Ocom_OLocal(v_Y,v_a,v_c),v_Q,t_a)),t_a),
inference(backward_demodulation,[],[f496,f777]) ).
fof(f853,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,v_Q,t_a)),t_a),
inference(backward_demodulation,[],[f495,f777]) ).
fof(f888,plain,
! [X0,X1] : hAPP(c_fequal(X0),X1) = hAPP(c_Set_Oinsert(X1,X0),c_COMBK(c_False,tc_bool,X0)),
inference(backward_demodulation,[],[f777,f783]) ).
fof(f899,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),X1),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),X2)),tc_Com_Ostate,tc_bool,tc_bool)),hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),X1),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),X3),X1,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(X4)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),X5))),c_Com_Ocom_OLocal(X4,X5,X6),X7,X1),tc_Hoare__Mirabelle_Otriple(X1)),c_COMBK(c_False,tc_bool,tc_Hoare__Mirabelle_Otriple(X1))),X1)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(X1)),c_Hoare__Mirabelle_Otriple_Otriple(X3,X6,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),X1),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),X7),X1,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(X4)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(X2,X4))),X1)),X1) ),
inference(forward_demodulation,[],[f846,f783]) ).
fof(f901,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_COMBK(c_False,tc_bool,tc_Hoare__Mirabelle_Otriple(t_a))),t_a)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)
| ~ hBOOL(hAPP(hAPP(X4,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X6,X4)))
| hBOOL(hAPP(hAPP(X6,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2))) ),
inference(forward_demodulation,[],[f844,f783]) ).
fof(f908,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_COMBK(c_False,tc_bool,tc_Hoare__Mirabelle_Otriple(t_a))),t_a)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)
| hBOOL(hAPP(hAPP(X3,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X4,X5))) ),
inference(forward_demodulation,[],[f835,f783]) ).
fof(f912,plain,
! [X2,X3,X0,X1] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_Set_Oinsert(c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xexport__s__1(X0,X1,X3,X2))),tc_Com_Ostate,tc_bool,tc_bool)),X1),X2,X3,t_a),tc_Hoare__Mirabelle_Otriple(t_a)),c_COMBK(c_False,tc_bool,tc_Hoare__Mirabelle_Otriple(t_a))),t_a)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a) ),
inference(forward_demodulation,[],[f830,f783]) ).
fof(f937,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(X1)),c_Hoare__Mirabelle_Otriple_Otriple(X3,X6,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),X1),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),X7),X1,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(X4)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(X2,X4))),X1)),X1)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(X1)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),X1),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),X2)),tc_Com_Ostate,tc_bool,tc_bool)),hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),X1),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),X3),X1,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(X4)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),X5))),c_Com_Ocom_OLocal(X4,X5,X6),X7,X1)),X1) ),
inference(forward_demodulation,[],[f899,f888]) ).
fof(f939,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ hBOOL(hAPP(hAPP(X4,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X6,X4)))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X6,X2,X4,t_a)),t_a)
| hBOOL(hAPP(hAPP(X6,X5),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(X0,X1,X3,X2))) ),
inference(forward_demodulation,[],[f901,f888]) ).
fof(f946,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X4,X2,X5,t_a)),t_a)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a)
| hBOOL(hAPP(hAPP(X3,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(X0,X1,X3,X2)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(X0,X1,X3,X2,X4,X5))) ),
inference(forward_demodulation,[],[f908,f888]) ).
fof(f950,plain,
! [X2,X3,X0,X1] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xexport__s__1(X0,X1,X3,X2))),tc_Com_Ostate,tc_bool,tc_bool)),X1),X2,X3,t_a)),t_a)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(X1,X2,X3,t_a)),t_a) ),
inference(forward_demodulation,[],[f912,f888]) ).
fof(f999,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_Com_Ostate,tc_bool),t_a),c_COMBS(hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Com_Ostate),c_and),hAPP(c_fequal(tc_Com_Ostate),v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)))),tc_Com_Ostate,tc_bool,tc_bool)),hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a))),c_Com_Ocom_OLocal(v_Y,v_a,v_c),v_Q,t_a)),t_a),
inference(unit_resulting_resolution,[],[f950,f851]) ).
fof(f1278,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,hAPP(c_fequal(tc_Hoare__Mirabelle_Otriple(t_a)),c_Hoare__Mirabelle_Otriple_Otriple(v_P,v_c,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),t_a)),t_a),
inference(unit_resulting_resolution,[],[f937,f999]) ).
fof(f1289,plain,
hBOOL(hAPP(hAPP(hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c,v_P,v_Q))),
inference(unit_resulting_resolution,[],[f946,f853,f1278]) ).
fof(f1306,plain,
hBOOL(hAPP(hAPP(hAPP(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c,v_P,v_Q))),
inference(forward_demodulation,[],[f1289,f488]) ).
fof(f1320,plain,
hBOOL(hAPP(hAPP(hAPP(c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate),hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c))),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c,v_P,v_Q))),
inference(forward_demodulation,[],[f1306,f487]) ).
fof(f1333,plain,
hBOOL(hAPP(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c)),hAPP(hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c,v_P,v_Q)))),
inference(forward_demodulation,[],[f1320,f487]) ).
fof(f1344,plain,
hBOOL(hAPP(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c)),hAPP(hAPP(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c,v_P,v_Q)),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y)))),
inference(forward_demodulation,[],[f1333,f488]) ).
fof(f1355,plain,
hBOOL(hAPP(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c)),hAPP(hAPP(hAPP(c_Natural_Oupdate,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c,v_P,v_Q)),c_Com_Ovname_OLoc(v_Y)),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y)))),
inference(forward_demodulation,[],[f1344,f488]) ).
fof(f1713,plain,
~ hBOOL(hAPP(hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c))),
inference(unit_resulting_resolution,[],[f839,f1278]) ).
fof(f2419,plain,
hBOOL(hAPP(hAPP(v_Q,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__3(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c,v_P,v_Q))),
inference(unit_resulting_resolution,[],[f531,f1355]) ).
fof(f2423,plain,
hBOOL(hAPP(hAPP(v_P,v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__1(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c)),v_sko__Hoare__Mirabelle__Xhoare__derivs__Xconseq__2(v_G,v_P,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_Q),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBC(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),c_Natural_Ogetlocs(v_sko__Hoare__Mirabelle__Xexport__s__1(v_G,hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_Com_Ostate,tc_bool),tc_fun(tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),t_a),c_COMBB(tc_Com_Ostate,tc_bool,tc_Com_Ostate)),v_P),t_a,tc_fun(tc_Com_Ostate,tc_Com_Ostate),tc_fun(tc_Com_Ostate,tc_bool)),hAPP(c_COMBS(hAPP(c_COMBC(c_Natural_Oupdate,tc_Com_Ostate,tc_Com_Ovname,tc_fun(tc_nat,tc_Com_Ostate)),c_Com_Ovname_OLoc(v_Y)),tc_Com_Ostate,tc_nat,tc_Com_Ostate),v_a)),v_Q,c_Com_Ocom_OLocal(v_Y,v_a,v_c)),v_Y))),v_c))),
inference(unit_resulting_resolution,[],[f939,f853,f1278,f2419]) ).
fof(f2426,plain,
$false,
inference(forward_subsumption_resolution,[],[f2423,f1713]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV915-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n008.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 12:54:10 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.85/2.12 % (2232159)Input is clausal, will run a generic CNF schedule.
% 9.85/2.12 % (2232164)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=3042326345:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 9.85/2.12 % (2232169)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2189836306:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 9.85/2.12 % (2232170)dis-21_1_sil=8000:lcm=predicate:random_seed=520529269: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)
% 9.85/2.12 % (2232166)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1952590094:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 9.85/2.12 % (2232167)lrs+10_1_sil=8000:sp=occurrence:random_seed=2337326712:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 9.85/2.12 % (2232168)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1095582771:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 9.85/2.12 % (2232165)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3697065975:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 9.85/2.12 % (2232170)Instruction limit reached!
% 9.85/2.12 % (2232170)------------------------------
% 9.85/2.12 % (2232170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.12 % (2232170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.12 % (2232170)CaDiCaL version: 2.1.3
% 9.85/2.12 % (2232170)Termination reason: Instruction limit
% 9.85/2.12 % (2232170)Termination phase: Saturation
% 9.85/2.12 % (2232170)Time elapsed: 0.048 s
% 9.85/2.12 % (2232170)Peak memory usage: 88 MB
% 9.85/2.12 % (2232170)Instructions burned: 119 (million)
% 9.85/2.12 % (2232168)Instruction limit reached!
% 9.85/2.12 % (2232168)------------------------------
% 9.85/2.12 % (2232168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.12 % (2232168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.12 % (2232168)CaDiCaL version: 2.1.3
% 9.85/2.12 % (2232168)Termination reason: Instruction limit
% 9.85/2.12 % (2232168)Termination phase: Saturation
% 9.85/2.12 % (2232168)Time elapsed: 0.051 s
% 9.85/2.12 % (2232168)Peak memory usage: 88 MB
% 9.85/2.12 % (2232168)Instructions burned: 116 (million)
% 9.85/2.12 % (2232167)Instruction limit reached!
% 9.85/2.12 % (2232167)------------------------------
% 9.85/2.12 % (2232167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.12 % (2232167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.12 % (2232167)CaDiCaL version: 2.1.3
% 9.85/2.12 % (2232167)Termination reason: Instruction limit
% 9.85/2.12 % (2232167)Termination phase: Saturation
% 9.85/2.12 % (2232167)Time elapsed: 0.069 s
% 9.85/2.12 % (2232167)Peak memory usage: 89 MB
% 9.85/2.12 % (2232167)Instructions burned: 107 (million)
% 9.85/2.12 % (2232169)Instruction limit reached!
% 9.85/2.12 % (2232169)------------------------------
% 9.85/2.12 % (2232169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.85/2.12 % (2232169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.85/2.12 % (2232169)CaDiCaL version: 2.1.3
% 9.85/2.12 % (2232169)Termination reason: Instruction limit
% 9.85/2.12 % (2232169)Termination phase: Saturation
% 9.85/2.12 % (2232169)Time elapsed: 0.112 s
% 9.85/2.12 % (2232169)Peak memory usage: 89 MB
% 9.85/2.12 % (2232169)Instructions burned: 181 (million)
% 9.85/2.12 % (2232179)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=892535594: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)
% 9.85/2.12 % (2232178)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=2576720152:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 9.85/2.12 % (2232180)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3534277373:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 9.85/2.12 % (2232178)Instruction limit reached!
% 9.85/2.12 % (2232178)------------------------------
% 9.85/2.12 % (2232178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.41/3.76 % (2232178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.41/3.76 % (2232178)CaDiCaL version: 2.1.3
% 21.41/3.76 % (2232178)Termination reason: Instruction limit
% 21.41/3.76 % (2232178)Termination phase: Saturation
% 21.41/3.76 % (2232178)Time elapsed: 0.084 s
% 21.41/3.76 % (2232178)Peak memory usage: 89 MB
% 21.41/3.76 % (2232178)Instructions burned: 145 (million)
% 21.41/3.76 % (2232181)lrs+10_64_to=lpo:sil=8000:random_seed=1134374880:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 21.41/3.76 % (2232179)Instruction limit reached!
% 21.41/3.76 % (2232179)------------------------------
% 21.41/3.76 % (2232179)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.41/3.76 % (2232179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.41/3.76 % (2232179)CaDiCaL version: 2.1.3
% 21.41/3.76 % (2232179)Termination reason: Instruction limit
% 21.41/3.76 % (2232179)Termination phase: Saturation
% 21.41/3.76 % (2232179)Time elapsed: 0.103 s
% 21.41/3.76 % (2232179)Peak memory usage: 90 MB
% 21.41/3.76 % (2232179)Instructions burned: 189 (million)
% 21.41/3.76 % (2232180)Instruction limit reached!
% 21.41/3.76 % (2232180)------------------------------
% 21.41/3.76 % (2232180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.41/3.76 % (2232180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.41/3.76 % (2232180)CaDiCaL version: 2.1.3
% 21.41/3.76 % (2232180)Termination reason: Instruction limit
% 21.41/3.76 % (2232180)Termination phase: Saturation
% 21.41/3.76 % (2232180)Time elapsed: 0.128 s
% 21.41/3.76 % (2232180)Peak memory usage: 91 MB
% 21.41/3.76 % (2232180)Instructions burned: 220 (million)
% 21.41/3.76 % (2232181)Instruction limit reached!
% 21.41/3.76 % (2232181)------------------------------
% 21.41/3.76 % (2232181)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.41/3.76 % (2232181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.41/3.76 % (2232181)CaDiCaL version: 2.1.3
% 21.41/3.76 % (2232181)Termination reason: Instruction limit
% 21.41/3.76 % (2232181)Termination phase: Saturation
% 21.41/3.76 % (2232181)Time elapsed: 0.075 s
% 21.41/3.76 % (2232181)Peak memory usage: 90 MB
% 21.41/3.76 % (2232181)Instructions burned: 127 (million)
% 21.41/3.76 % (2232187)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2252552430:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 21.41/3.76 % (2232186)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1678846566:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 21.41/3.76 % (2232187)Instruction limit reached!
% 21.41/3.76 % (2232187)------------------------------
% 21.41/3.76 % (2232187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.41/3.76 % (2232187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.41/3.76 % (2232187)CaDiCaL version: 2.1.3
% 21.41/3.76 % (2232187)Termination reason: Instruction limit
% 21.41/3.76 % (2232187)Termination phase: Saturation
% 21.41/3.76 % (2232187)Time elapsed: 0.055 s
% 21.41/3.76 % (2232187)Peak memory usage: 91 MB
% 21.41/3.76 % (2232187)Instructions burned: 157 (million)
% 21.41/3.76 % (2232188)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2531928606:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 21.41/3.76 % (2232189)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=2106624893:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 21.41/3.76 % (2232186)Instruction limit reached!
% 21.41/3.76 % (2232186)------------------------------
% 21.41/3.76 % (2232186)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.41/3.76 % (2232186)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.41/3.76 % (2232186)CaDiCaL version: 2.1.3
% 21.41/3.76 % (2232186)Termination reason: Instruction limit
% 21.41/3.76 % (2232186)Termination phase: Saturation
% 21.41/3.76 % (2232186)Time elapsed: 0.114 s
% 21.41/3.76 % (2232186)Peak memory usage: 90 MB
% 21.41/3.76 % (2232186)Instructions burned: 200 (million)
% 21.41/3.76 % (2232189)Instruction limit reached!
% 21.41/3.76 % (2232189)------------------------------
% 21.41/3.76 % (2232189)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.41/3.76 % (2232189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.41/3.76 % (2232189)CaDiCaL version: 2.1.3
% 38.97/6.18 % (2232189)Termination reason: Instruction limit
% 38.97/6.18 % (2232189)Termination phase: Saturation
% 38.97/6.18 % (2232189)Time elapsed: 0.058 s
% 38.97/6.18 % (2232189)Peak memory usage: 89 MB
% 38.97/6.18 % (2232189)Instructions burned: 106 (million)
% 38.97/6.18 % (2232192)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1630379639:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 38.97/6.18 % (2232192)Instruction limit reached!
% 38.97/6.18 % (2232192)------------------------------
% 38.97/6.18 % (2232192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.97/6.18 % (2232192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.97/6.18 % (2232192)CaDiCaL version: 2.1.3
% 38.97/6.18 % (2232192)Termination reason: Instruction limit
% 38.97/6.18 % (2232192)Termination phase: Saturation
% 38.97/6.18 % (2232192)Time elapsed: 0.034 s
% 38.97/6.18 % (2232192)Peak memory usage: 90 MB
% 38.97/6.18 % (2232192)Instructions burned: 108 (million)
% 38.97/6.18 % (2232195)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1755663102:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 38.97/6.18 % (2232196)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1962641655:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 38.97/6.18 % (2232198)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=720801291:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 38.97/6.18 % (2232198)Instruction limit reached!
% 38.97/6.18 % (2232198)------------------------------
% 38.97/6.18 % (2232198)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.97/6.18 % (2232198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.97/6.18 % (2232198)CaDiCaL version: 2.1.3
% 38.97/6.18 % (2232198)Termination reason: Instruction limit
% 38.97/6.18 % (2232198)Termination phase: Saturation
% 38.97/6.18 % (2232198)Time elapsed: 0.034 s
% 38.97/6.18 % (2232198)Peak memory usage: 89 MB
% 38.97/6.18 % (2232198)Instructions burned: 141 (million)
% 38.97/6.18 % (2232195)Instruction limit reached!
% 38.97/6.18 % (2232195)------------------------------
% 38.97/6.18 % (2232195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.97/6.18 % (2232195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.97/6.18 % (2232195)CaDiCaL version: 2.1.3
% 38.97/6.18 % (2232195)Termination reason: Instruction limit
% 38.97/6.18 % (2232195)Termination phase: Saturation
% 38.97/6.18 % (2232195)Time elapsed: 0.151 s
% 38.97/6.18 % (2232195)Peak memory usage: 90 MB
% 38.97/6.18 % (2232195)Instructions burned: 242 (million)
% 38.97/6.18 % (2232202)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=174520473:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 38.97/6.18 % (2232203)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=721268949:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 38.97/6.18 % (2232203)Instruction limit reached!
% 38.97/6.18 % (2232203)------------------------------
% 38.97/6.18 % (2232203)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.97/6.18 % (2232203)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.97/6.18 % (2232203)CaDiCaL version: 2.1.3
% 38.97/6.18 % (2232203)Termination reason: Instruction limit
% 38.97/6.18 % (2232203)Termination phase: Saturation
% 38.97/6.18 % (2232203)Time elapsed: 0.061 s
% 38.97/6.18 % (2232203)Peak memory usage: 90 MB
% 38.97/6.18 % (2232203)Instructions burned: 194 (million)
% 38.97/6.18 % (2232206)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4122772056:i=264:kws=precedence:fsr=off_2987 on theBenchmark for (2987ds/264Mi)
% 38.97/6.18 % (2232206)Instruction limit reached!
% 38.97/6.18 % (2232206)------------------------------
% 38.97/6.18 % (2232206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.97/6.18 % (2232206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.97/6.18 % (2232206)CaDiCaL version: 2.1.3
% 38.97/6.18 % (2232206)Termination reason: Instruction limit
% 38.97/6.18 % (2232206)Termination phase: Saturation
% 38.97/6.18 % (2232206)Time elapsed: 0.064 s
% 38.97/6.18 % (2232206)Peak memory usage: 90 MB
% 38.97/6.18 % (2232206)Instructions burned: 267 (million)
% 38.97/6.18 % (2232202)Instruction limit reached!
% 38.97/6.18 % (2232202)------------------------------
% 47.15/7.48 % (2232202)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.15/7.48 % (2232202)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.15/7.48 % (2232202)CaDiCaL version: 2.1.3
% 47.15/7.48 % (2232202)Termination reason: Instruction limit
% 47.15/7.48 % (2232202)Termination phase: Saturation
% 47.15/7.48 % (2232202)Time elapsed: 0.311 s
% 47.15/7.48 % (2232202)Peak memory usage: 94 MB
% 47.15/7.48 % (2232202)Instructions burned: 502 (million)
% 47.15/7.48 % (2232208)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3223643637:cond=on:i=156:bs=on:gtg=exists_all:er=known_2986 on theBenchmark for (2986ds/156Mi)
% 47.15/7.48 % (2232208)Instruction limit reached!
% 47.15/7.48 % (2232208)------------------------------
% 47.15/7.48 % (2232208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.15/7.48 % (2232208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.15/7.48 % (2232208)CaDiCaL version: 2.1.3
% 47.15/7.48 % (2232208)Termination reason: Instruction limit
% 47.15/7.48 % (2232208)Termination phase: Saturation
% 47.15/7.48 % (2232208)Time elapsed: 0.052 s
% 47.15/7.48 % (2232208)Peak memory usage: 90 MB
% 47.15/7.48 % (2232208)Instructions burned: 158 (million)
% 47.15/7.48 % (2232209)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=566220473:i=3256:kws=precedence:bd=preordered:av=off_2985 on theBenchmark for (2985ds/3256Mi)
% 47.15/7.48 % (2232211)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2536389217:i=537:av=off:ss=included_2984 on theBenchmark for (2984ds/537Mi)
% 47.15/7.48 % (2232211)Instruction limit reached!
% 47.15/7.48 % (2232211)------------------------------
% 47.15/7.48 % (2232211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.15/7.48 % (2232211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.15/7.48 % (2232211)CaDiCaL version: 2.1.3
% 47.15/7.48 % (2232211)Termination reason: Instruction limit
% 47.15/7.48 % (2232211)Termination phase: Saturation
% 47.15/7.48 % (2232211)Time elapsed: 0.142 s
% 47.15/7.48 % (2232211)Peak memory usage: 90 MB
% 47.15/7.48 % (2232211)Instructions burned: 539 (million)
% 47.15/7.48 % (2232214)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2780370750:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 47.15/7.48 % (2232214)Instruction limit reached!
% 47.15/7.48 % (2232214)------------------------------
% 47.15/7.48 % (2232214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.15/7.48 % (2232214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.15/7.48 % (2232214)CaDiCaL version: 2.1.3
% 47.15/7.48 % (2232214)Termination reason: Instruction limit
% 47.15/7.48 % (2232214)Termination phase: Saturation
% 47.15/7.48 % (2232214)Time elapsed: 0.054 s
% 47.15/7.48 % (2232214)Peak memory usage: 90 MB
% 47.15/7.48 % (2232214)Instructions burned: 182 (million)
% 47.15/7.48 % (2232216)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=886904821:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2979 on theBenchmark for (2979ds/10307Mi)
% 47.15/7.48 % (2232188)Instruction limit reached!
% 47.15/7.48 % (2232188)------------------------------
% 47.15/7.48 % (2232188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.15/7.48 % (2232188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.15/7.48 % (2232188)CaDiCaL version: 2.1.3
% 47.15/7.48 % (2232188)Termination reason: Instruction limit
% 47.15/7.48 % (2232188)Termination phase: Saturation
% 47.15/7.48 % (2232188)Time elapsed: 2.027 s
% 47.15/7.48 % (2232188)Peak memory usage: 151 MB
% 47.15/7.48 % (2232188)Instructions burned: 3394 (million)
% 47.15/7.48 % (2232218)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=1152145415:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 47.15/7.48 % (2232218)Instruction limit reached!
% 47.15/7.48 % (2232218)------------------------------
% 47.15/7.48 % (2232218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.15/7.48 % (2232218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.15/7.48 % (2232218)CaDiCaL version: 2.1.3
% 47.15/7.48 % (2232218)Termination reason: Instruction limit
% 47.15/7.48 % (2232218)Termination phase: Saturation
% 57.78/8.98 % (2232218)Time elapsed: 0.227 s
% 57.78/8.98 % (2232218)Peak memory usage: 91 MB
% 57.78/8.98 % (2232218)Instructions burned: 414 (million)
% 57.78/8.98 % (2232220)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=1989262477:s2pl=no:i=8478:s2at=4:nm=6_2969 on theBenchmark for (2969ds/8478Mi)
% 57.78/8.98 % (2232209)Instruction limit reached!
% 57.78/8.98 % (2232209)------------------------------
% 57.78/8.98 % (2232209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232209)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232209)Termination reason: Instruction limit
% 57.78/8.98 % (2232209)Termination phase: Saturation
% 57.78/8.98 % (2232209)Time elapsed: 1.913 s
% 57.78/8.98 % (2232209)Peak memory usage: 151 MB
% 57.78/8.98 % (2232209)Instructions burned: 3258 (million)
% 57.78/8.98 % (2232222)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=2660006480:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2964 on theBenchmark for (2964ds/303Mi)
% 57.78/8.98 % (2232222)Instruction limit reached!
% 57.78/8.98 % (2232222)------------------------------
% 57.78/8.98 % (2232222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232222)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232222)Termination reason: Instruction limit
% 57.78/8.98 % (2232222)Termination phase: Saturation
% 57.78/8.98 % (2232222)Time elapsed: 0.162 s
% 57.78/8.98 % (2232222)Peak memory usage: 91 MB
% 57.78/8.98 % (2232222)Instructions burned: 304 (million)
% 57.78/8.98 % (2232196)Instruction limit reached!
% 57.78/8.98 % (2232196)------------------------------
% 57.78/8.98 % (2232196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232196)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232196)Termination reason: Instruction limit
% 57.78/8.98 % (2232196)Termination phase: Saturation
% 57.78/8.98 % (2232196)Time elapsed: 2.974 s
% 57.78/8.98 % (2232196)Peak memory usage: 166 MB
% 57.78/8.98 % (2232196)Instructions burned: 5208 (million)
% 57.78/8.98 % (2232224)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3146854132:st=4:i=720:sd=3:fsr=off:ss=axioms_2961 on theBenchmark for (2961ds/720Mi)
% 57.78/8.98 % (2232225)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=319571902:i=598:bs=on:bd=preordered:av=off:ss=axioms_2960 on theBenchmark for (2960ds/598Mi)
% 57.78/8.98 % (2232224)Instruction limit reached!
% 57.78/8.98 % (2232224)------------------------------
% 57.78/8.98 % (2232224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232224)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232224)Termination reason: Instruction limit
% 57.78/8.98 % (2232224)Termination phase: Saturation
% 57.78/8.98 % (2232224)Time elapsed: 0.394 s
% 57.78/8.98 % (2232224)Peak memory usage: 94 MB
% 57.78/8.98 % (2232224)Instructions burned: 721 (million)
% 57.78/8.98 % (2232225)Instruction limit reached!
% 57.78/8.98 % (2232225)------------------------------
% 57.78/8.98 % (2232225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232225)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232225)Termination reason: Instruction limit
% 57.78/8.98 % (2232225)Termination phase: Saturation
% 57.78/8.98 % (2232225)Time elapsed: 0.374 s
% 57.78/8.98 % (2232225)Peak memory usage: 95 MB
% 57.78/8.98 % (2232225)Instructions burned: 598 (million)
% 57.78/8.98 % (2232228)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3228743221:i=2989:sd=3:ss=axioms:sgt=60_2955 on theBenchmark for (2955ds/2989Mi)
% 57.78/8.98 % (2232229)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=205988541:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2955 on theBenchmark for (2955ds/1997Mi)
% 57.78/8.98 % (2232216)Instruction limit reached!
% 57.78/8.98 % (2232216)------------------------------
% 57.78/8.98 % (2232216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232216)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232216)Termination reason: Instruction limit
% 57.78/8.98 % (2232216)Termination phase: Saturation
% 57.78/8.98 % (2232216)Time elapsed: 3.351 s
% 57.78/8.98 % (2232216)Peak memory usage: 221 MB
% 57.78/8.98 % (2232216)Instructions burned: 10309 (million)
% 57.78/8.98 % (2232232)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=203647781:i=2088:bd=preordered:av=off_2944 on theBenchmark for (2944ds/2088Mi)
% 57.78/8.98 % (2232229)Instruction limit reached!
% 57.78/8.98 % (2232229)------------------------------
% 57.78/8.98 % (2232229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232229)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232229)Termination reason: Instruction limit
% 57.78/8.98 % (2232229)Termination phase: Saturation
% 57.78/8.98 % (2232229)Time elapsed: 1.194 s
% 57.78/8.98 % (2232229)Peak memory usage: 139 MB
% 57.78/8.98 % (2232229)Instructions burned: 1999 (million)
% 57.78/8.98 % (2232234)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1477667491:i=1098:nicw=on_2941 on theBenchmark for (2941ds/1098Mi)
% 57.78/8.98 % (2232228)Instruction limit reached!
% 57.78/8.98 % (2232228)------------------------------
% 57.78/8.98 % (2232228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232228)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232228)Termination reason: Instruction limit
% 57.78/8.98 % (2232228)Termination phase: Saturation
% 57.78/8.98 % (2232228)Time elapsed: 1.760 s
% 57.78/8.98 % (2232228)Peak memory usage: 145 MB
% 57.78/8.98 % (2232228)Instructions burned: 2991 (million)
% 57.78/8.98 % (2232232)Instruction limit reached!
% 57.78/8.98 % (2232232)------------------------------
% 57.78/8.98 % (2232232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232232)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232232)Termination reason: Instruction limit
% 57.78/8.98 % (2232232)Termination phase: Saturation
% 57.78/8.98 % (2232232)Time elapsed: 0.705 s
% 57.78/8.98 % (2232232)Peak memory usage: 141 MB
% 57.78/8.98 % (2232232)Instructions burned: 2090 (million)
% 57.78/8.98 % (2232237)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2760628512:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2936 on theBenchmark for (2936ds/2942Mi)
% 57.78/8.98 % (2232236)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=2823939024:i=433:bd=preordered_2936 on theBenchmark for (2936ds/433Mi)
% 57.78/8.98 % (2232234)Instruction limit reached!
% 57.78/8.98 % (2232234)------------------------------
% 57.78/8.98 % (2232234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232234)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232234)Termination reason: Instruction limit
% 57.78/8.98 % (2232234)Termination phase: Saturation
% 57.78/8.98 % (2232234)Time elapsed: 0.678 s
% 57.78/8.98 % (2232234)Peak memory usage: 100 MB
% 57.78/8.98 % (2232234)Instructions burned: 1098 (million)
% 57.78/8.98 % (2232240)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4007590104:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2933 on theBenchmark for (2933ds/6922Mi)
% 57.78/8.98 % (2232236)Instruction limit reached!
% 57.78/8.98 % (2232236)------------------------------
% 57.78/8.98 % (2232236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232236)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232236)Termination reason: Instruction limit
% 57.78/8.98 % (2232236)Termination phase: Saturation
% 57.78/8.98 % (2232236)Time elapsed: 0.250 s
% 57.78/8.98 % (2232236)Peak memory usage: 93 MB
% 57.78/8.98 % (2232236)Instructions burned: 434 (million)
% 57.78/8.98 % (2232242)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=3779452077:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2931 on theBenchmark for (2931ds/596Mi)
% 57.78/8.98 % (2232242)Instruction limit reached!
% 57.78/8.98 % (2232242)------------------------------
% 57.78/8.98 % (2232242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232242)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232242)Termination reason: Instruction limit
% 57.78/8.98 % (2232242)Termination phase: Saturation
% 57.78/8.98 % (2232242)Time elapsed: 0.337 s
% 57.78/8.98 % (2232242)Peak memory usage: 96 MB
% 57.78/8.98 % (2232242)Instructions burned: 598 (million)
% 57.78/8.98 % (2232244)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=132710927:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2926 on theBenchmark for (2926ds/4123Mi)
% 57.78/8.98 % (2232237)Instruction limit reached!
% 57.78/8.98 % (2232237)------------------------------
% 57.78/8.98 % (2232237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 57.78/8.98 % (2232237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.78/8.98 % (2232237)CaDiCaL version: 2.1.3
% 57.78/8.98 % (2232237)Termination reason: Instruction limit
% 57.78/8.98 % (2232237)Termination phase: Saturation
% 57.78/8.98 % (2232237)Time elapsed: 1.010 s
% 57.78/8.98 % (2232237)Peak memory usage: 149 MB
% 57.78/8.98 % (2232237)Instructions burned: 2943 (million)
% 57.78/8.98 % (2232246)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1185837757:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2924 on theBenchmark for (2924ds/16411Mi)
% 57.78/8.98 % (2232240)First to succeed.
% 57.78/8.98 % (2232240)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2232159"
% 57.78/8.98 % (2232240)Refutation found. Thanks to Tanya!
% 57.78/8.98 % SZS status Unsatisfiable for theBenchmark
% 57.78/8.98 % SZS output start Proof for theBenchmark
% See solution above
% 59.07/9.09 % (2232240)------------------------------
% 59.07/9.09 % (2232240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 59.07/9.09 % (2232240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 59.07/9.09 % (2232240)CaDiCaL version: 2.1.3
% 59.07/9.09 % (2232240)Termination reason: Refutation
% 59.07/9.09 % (2232240)Time elapsed: 1.233 s
% 59.07/9.09 % (2232240)Peak memory usage: 141 MB
% 59.07/9.09 % (2232240)Instructions burned: 2026 (million)
% 59.07/9.09 % (2232240)------------------------------
% 59.07/9.09 % (2232240)------------------------------
% 59.07/9.09 % (2232159)Success in time 8.311 s
% 59.07/9.09 % Vampire exiting
%------------------------------------------------------------------------------