%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP008^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 08:53:13 AM UTC 2026
% Result : Theorem 31.59s 5.79s
% Output : Refutation 31.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP008^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.13/0.13 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.34 % Computer : n010.cluster.edu
% 0.18/0.34 % Model : x86_64 x86_64
% 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34 % Memory : 8042.1875MB
% 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34 % CPULimit : 300
% 0.18/0.34 % WCLimit : 300
% 0.18/0.34 % DateTime : Tue Feb 24 08:18:48 EST 2026
% 0.18/0.35 % CPUTime :
% 0.18/0.35 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.28/0.47 ---- Original DTF file ---
% 0.28/0.48 thf(spec,logic,$$dhol).
% 0.28/0.48 %------------------------------------------------------------------------------
% 0.28/0.48 % File : ITP008^3 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.28/0.48 % Domain : Interactive Theorem Proving
% 0.28/0.48 % Problem : HOL4 syntactic export of thm_2Ewellorder_2EWIN__WF2.p, bushy mode
% 0.28/0.48 % Version : [BG+19] axioms.
% 0.28/0.48 % English :
% 0.28/0.48
% 0.28/0.48 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall
% 0.28/0.48 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe
% 0.28/0.48 % Source : [BG+19]
% 0.28/0.48 % Names : thm_2Ewellorder_2EWIN__WF2.p [Gau19]
% 0.28/0.48 % : HL403501^3.p [TPAP]
% 0.28/0.48
% 0.28/0.48 % Status : Theorem
% 0.28/0.48 % Rating : 0.67 v8.2.0, 1.00 v8.1.0, 0.75 v7.5.0
% 0.28/0.48 % Syntax : Number of formulae : 30 ( 8 unt; 18 typ; 0 def)
% 0.28/0.48 % Number of atoms : 22 ( 4 equ; 1 cnn)
% 0.28/0.48 % Maximal formula atoms : 4 ( 1 avg)
% 0.28/0.48 % Number of connectives : 95 ( 1 ~; 1 |; 1 &; 84 @)
% 0.28/0.48 % ( 7 <=>; 1 =>; 0 <=; 0 <~>)
% 0.28/0.48 % Maximal formula depth : 12 ( 7 avg)
% 0.28/0.48 % Number of types : 2 ( 1 usr)
% 0.28/0.48 % Number of type conns : 42 ( 42 >; 0 *; 0 +; 0 <<)
% 0.28/0.48 % Number of symbols : 19 ( 17 usr; 1 con; 0-6 aty)
% 0.28/0.48 % Number of variables : 48 ( 4 ^; 30 !; 1 ?; 48 :)
% 0.28/0.48 % ( 13 !>; 0 ?*; 0 @-; 0 @+)
% 0.28/0.48 % SPC : TH1_THM_EQU_NAR
% 0.28/0.48
% 0.28/0.48 % Comments :
% 0.28/0.48 % Bugfixes : v7.5.0 - Bugfixes in axioms and export.
% 0.28/0.48 %------------------------------------------------------------------------------
% 0.28/0.48 thf(tyop_2Emin_2Ebool,type,
% 0.28/0.48 tyop_2Emin_2Ebool: $tType ).
% 0.28/0.48
% 0.28/0.48 thf(tyop_2Emin_2Efun,type,
% 0.28/0.48 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 0.28/0.48
% 0.28/0.48 thf(tyop_2Epair_2Eprod,type,
% 0.28/0.48 tyop_2Epair_2Eprod: $tType > $tType > $tType ).
% 0.28/0.48
% 0.28/0.48 thf(tyop_2Ewellorder_2Ewellorder,type,
% 0.28/0.48 tyop_2Ewellorder_2Ewellorder: $tType > $tType ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Ebool_2E_21,type,
% 0.28/0.48 c_2Ebool_2E_21:
% 0.28/0.48 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Epair_2E_2C,type,
% 0.28/0.48 c_2Epair_2E_2C:
% 0.28/0.48 !>[A_27a: $tType,A_27b: $tType] : ( A_27a > A_27b > ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Ebool_2E_2F_5C,type,
% 0.28/0.48 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Emin_2E_3D,type,
% 0.28/0.48 c_2Emin_2E_3D:
% 0.28/0.48 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Emin_2E_3D_3D_3E,type,
% 0.28/0.48 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Ebool_2E_3F,type,
% 0.28/0.48 c_2Ebool_2E_3F:
% 0.28/0.48 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Epair_2ECURRY,type,
% 0.28/0.48 c_2Epair_2ECURRY:
% 0.28/0.48 !>[A_27a: $tType,A_27b: $tType,A_27c: $tType] : ( ( ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) > A_27c ) > A_27a > A_27b > A_27c ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Ebool_2EIN,type,
% 0.28/0.48 c_2Ebool_2EIN:
% 0.28/0.48 !>[A_27a: $tType] : ( A_27a > ( A_27a > $o ) > $o ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Erelation_2EWF,type,
% 0.28/0.48 c_2Erelation_2EWF:
% 0.28/0.48 !>[A_27a: $tType] : ( ( A_27a > A_27a > $o ) > $o ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Ebool_2E_5C_2F,type,
% 0.28/0.48 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Eset__relation_2Estrict,type,
% 0.28/0.48 c_2Eset__relation_2Estrict:
% 0.28/0.48 !>[A_27a: $tType] : ( ( ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o ) > ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Ewellorder_2Ewellfounded,type,
% 0.28/0.48 c_2Ewellorder_2Ewellfounded:
% 0.28/0.48 !>[A_27a: $tType] : ( ( ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o ) > $o ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Ewellorder_2Ewellorder__REP,type,
% 0.28/0.48 c_2Ewellorder_2Ewellorder__REP:
% 0.28/0.48 !>[A_27a: $tType] : ( ( tyop_2Ewellorder_2Ewellorder @ A_27a ) > ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o ) ).
% 0.28/0.48
% 0.28/0.48 thf(c_2Ebool_2E_7E,type,
% 0.28/0.48 c_2Ebool_2E_7E: $o > $o ).
% 0.28/0.48
% 0.28/0.48 thf(logicdef_2E_2F_5C,axiom,
% 0.28/0.48 ! [V0: $o,V1: $o] :
% 0.28/0.48 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 0.28/0.48 <=> ( V0
% 0.28/0.48 & V1 ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(logicdef_2E_5C_2F,axiom,
% 0.28/0.48 ! [V0: $o,V1: $o] :
% 0.28/0.48 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 0.28/0.48 <=> ( V0
% 0.28/0.48 | V1 ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(logicdef_2E_7E,axiom,
% 0.28/0.48 ! [V0: $o] :
% 0.28/0.48 ( ( c_2Ebool_2E_7E @ V0 )
% 0.28/0.48 <=> ( (~) @ V0 ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(logicdef_2E_3D_3D_3E,axiom,
% 0.28/0.48 ! [V0: $o,V1: $o] :
% 0.28/0.48 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 0.28/0.48 <=> ( V0
% 0.28/0.48 => V1 ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(logicdef_2E_3D,axiom,
% 0.28/0.48 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 0.28/0.48 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 0.28/0.48 <=> ( V0 = V1 ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(quantdef_2E_21,axiom,
% 0.28/0.48 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.28/0.48 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 0.28/0.48 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(quantdef_2E_3F,axiom,
% 0.28/0.48 ! [A_27a: $tType,V0f: A_27a > $o] :
% 0.28/0.48 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 0.28/0.48 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(thm_2Ebool_2EETA__AX,axiom,
% 0.28/0.48 ! [A_27a: $tType,A_27b: $tType,V0t: A_27a > A_27b] :
% 0.28/0.48 ( ( ^ [V1x: A_27a] : ( V0t @ V1x ) )
% 0.28/0.48 = V0t ) ).
% 0.28/0.48
% 0.28/0.48 thf(thm_2Epair_2ECURRY__DEF,axiom,
% 0.28/0.48 ! [A_27a: $tType,A_27b: $tType,A_27c: $tType,V0f: ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) > A_27c,V1x: A_27a,V2y: A_27b] :
% 0.28/0.48 ( ( c_2Epair_2ECURRY @ A_27a @ A_27b @ A_27c @ V0f @ V1x @ V2y )
% 0.28/0.48 = ( V0f @ ( c_2Epair_2E_2C @ A_27a @ A_27b @ V1x @ V2y ) ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(thm_2Ewellorder_2Ewellfounded__WF,axiom,
% 0.28/0.48 ! [A_27a: $tType,V0R: ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o] :
% 0.28/0.48 ( ( c_2Ewellorder_2Ewellfounded @ A_27a @ V0R )
% 0.28/0.48 = ( c_2Erelation_2EWF @ A_27a @ ( c_2Epair_2ECURRY @ A_27a @ A_27a @ $o @ V0R ) ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(thm_2Ewellorder_2EWIN__WF,axiom,
% 0.28/0.48 ! [A_27a: $tType,V0w: tyop_2Ewellorder_2Ewellorder @ A_27a] :
% 0.28/0.48 ( c_2Ewellorder_2Ewellfounded @ A_27a
% 0.28/0.48 @ ^ [V1p: tyop_2Epair_2Eprod @ A_27a @ A_27a] : ( c_2Ebool_2EIN @ ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) @ V1p @ ( c_2Eset__relation_2Estrict @ A_27a @ ( c_2Ewellorder_2Ewellorder__REP @ A_27a @ V0w ) ) ) ) ).
% 0.28/0.48
% 0.28/0.48 thf(thm_2Ewellorder_2EWIN__WF2,conjecture,
% 0.28/0.48 ! [A_27a: $tType,V0w: tyop_2Ewellorder_2Ewellorder @ A_27a] :
% 0.28/0.48 ( c_2Erelation_2EWF @ A_27a
% 0.28/0.48 @ ^ [V1x: A_27a,V2y: A_27a] : ( c_2Ebool_2EIN @ ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) @ ( c_2Epair_2E_2C @ A_27a @ A_27a @ V1x @ V2y ) @ ( c_2Eset__relation_2Estrict @ A_27a @ ( c_2Ewellorder_2Ewellorder__REP @ A_27a @ V0w ) ) ) ) ).
% 0.28/0.48
% 0.28/0.48 %------------------------------------------------------------------------------
% 0.28/0.48 ------------------------
% 1.54/1.29 ---- Embedded in THF ---
% 1.54/1.30 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.54/1.30 %%% Generated on Tue Feb 24 08:18:49 EST 2026
% 1.54/1.30 %%% using '$$dhol' embedding, version 1.3.0.
% 1.54/1.30 %%% Logic specification used:
% 1.54/1.30 %%% thf(spec, logic, $$dhol).
% 1.54/1.30
% 1.54/1.30 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.HpJsg7gn6n/DTF2DTF17586.p
% 1.54/1.30 thf(tyop_2Emin_2Ebool, type, tyop_2Emin_2Ebool: $tType).
% 1.54/1.30 thf(tyop_2Emin_2Efun, type, tyop_2Emin_2Efun: ($tType > ($tType > $tType))).
% 1.54/1.30 thf(tyop_2Epair_2Eprod, type, tyop_2Epair_2Eprod: ($tType > ($tType > $tType))).
% 1.54/1.30 thf(tyop_2Ewellorder_2Ewellorder, type, tyop_2Ewellorder_2Ewellorder: ($tType > $tType)).
% 1.54/1.30 thf(c_2Ebool_2E_21, type, c_2Ebool_2E_21: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 1.54/1.30 thf(c_2Epair_2E_2C, type, c_2Epair_2E_2C: (!> [A_27a:$tType,A_27b:$tType]: ((A_27a > (A_27b > ((tyop_2Epair_2Eprod @ A_27a) @ A_27b)))))).
% 1.54/1.30 thf(c_2Ebool_2E_2F_5C, type, c_2Ebool_2E_2F_5C: ($o > ($o > $o))).
% 1.54/1.30 thf(c_2Emin_2E_3D, type, c_2Emin_2E_3D: (!> [A_27a:$tType]: ((A_27a > (A_27a > $o))))).
% 1.54/1.30 thf(c_2Emin_2E_3D_3D_3E, type, c_2Emin_2E_3D_3D_3E: ($o > ($o > $o))).
% 1.54/1.30 thf(c_2Ebool_2E_3F, type, c_2Ebool_2E_3F: (!> [A_27a:$tType]: (((A_27a > $o) > $o)))).
% 1.54/1.30 thf(c_2Epair_2ECURRY, type, c_2Epair_2ECURRY: (!> [A_27a:$tType,A_27b:$tType,A_27c:$tType]: (((((tyop_2Epair_2Eprod @ A_27a) @ A_27b) > A_27c) > (A_27a > (A_27b > A_27c)))))).
% 1.54/1.30 thf(c_2Ebool_2EIN, type, c_2Ebool_2EIN: (!> [A_27a:$tType]: ((A_27a > ((A_27a > $o) > $o))))).
% 1.54/1.30 thf(c_2Erelation_2EWF, type, c_2Erelation_2EWF: (!> [A_27a:$tType]: (((A_27a > (A_27a > $o)) > $o)))).
% 1.54/1.30 thf(c_2Ebool_2E_5C_2F, type, c_2Ebool_2E_5C_2F: ($o > ($o > $o))).
% 1.54/1.30 thf(c_2Eset__relation_2Estrict, type, c_2Eset__relation_2Estrict: (!> [A_27a:$tType]: (((((tyop_2Epair_2Eprod @ A_27a) @ A_27a) > $o) > (((tyop_2Epair_2Eprod @ A_27a) @ A_27a) > $o))))).
% 1.54/1.30 thf(c_2Ewellorder_2Ewellfounded, type, c_2Ewellorder_2Ewellfounded: (!> [A_27a:$tType]: (((((tyop_2Epair_2Eprod @ A_27a) @ A_27a) > $o) > $o)))).
% 1.54/1.30 thf(c_2Ewellorder_2Ewellorder__REP, type, c_2Ewellorder_2Ewellorder__REP: (!> [A_27a:$tType]: (((tyop_2Ewellorder_2Ewellorder @ A_27a) > (((tyop_2Epair_2Eprod @ A_27a) @ A_27a) > $o))))).
% 1.54/1.30 thf(c_2Ebool_2E_7E, type, c_2Ebool_2E_7E: ($o > $o)).
% 1.54/1.30 thf(logicdef_2E_2F_5C, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_2F_5C @ V0) @ V1) <=> (V0 & V1))))).
% 1.54/1.30 thf(logicdef_2E_5C_2F, axiom, (! [V0:$o,V1:$o]: ((((c_2Ebool_2E_5C_2F @ V0) @ V1) <=> (V0 | V1))))).
% 1.54/1.30 thf(logicdef_2E_7E, axiom, (! [V0:$o]: (((c_2Ebool_2E_7E @ V0) <=> ((~) @ V0))))).
% 1.54/1.30 thf(logicdef_2E_3D_3D_3E, axiom, (! [V0:$o,V1:$o]: ((((c_2Emin_2E_3D_3D_3E @ V0) @ V1) <=> (V0 => V1))))).
% 1.54/1.30 thf(logicdef_2E_3D, axiom, (! [A_27a:$tType,V0:A_27a,V1:A_27a]: (((((c_2Emin_2E_3D @ A_27a) @ V0) @ V1) <=> (V0 = V1))))).
% 1.54/1.30 thf(quantdef_2E_21, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_21 @ A_27a) @ V0f) <=> (! [V1x:A_27a]: ((V0f @ V1x))))))).
% 1.54/1.30 thf(quantdef_2E_3F, axiom, (! [A_27a:$tType,V0f:(A_27a > $o)]: ((((c_2Ebool_2E_3F @ A_27a) @ V0f) <=> (? [V1x:A_27a]: ((V0f @ V1x))))))).
% 1.54/1.30 thf(thm_2Ebool_2EETA__AX, axiom, (! [A_27a:$tType,A_27b:$tType,V0t:(A_27a > A_27b)]: (((^ [V1x:A_27a]: ((V0t @ V1x))) = V0t)))).
% 1.54/1.30 thf(thm_2Epair_2ECURRY__DEF, axiom, (! [A_27a:$tType,A_27b:$tType,A_27c:$tType,V0f:(((tyop_2Epair_2Eprod @ A_27a) @ A_27b) > A_27c),V1x:A_27a,V2y:A_27b]: ((((((((c_2Epair_2ECURRY @ A_27a) @ A_27b) @ A_27c) @ V0f) @ V1x) @ V2y) = (V0f @ ((((c_2Epair_2E_2C @ A_27a) @ A_27b) @ V1x) @ V2y)))))).
% 1.54/1.30 thf(thm_2Ewellorder_2Ewellfounded__WF, axiom, (! [A_27a:$tType,V0R:(((tyop_2Epair_2Eprod @ A_27a) @ A_27a) > $o)]: ((((c_2Ewellorder_2Ewellfounded @ A_27a) @ V0R) = ((c_2Erelation_2EWF @ A_27a) @ ((((c_2Epair_2ECURRY @ A_27a) @ A_27a) @ $o) @ V0R)))))).
% 1.54/1.30 thf(thm_2Ewellorder_2EWIN__WF, axiom, (! [A_27a:$tType,V0w:(tyop_2Ewellorder_2Ewellorder @ A_27a)]: (((c_2Ewellorder_2Ewellfounded @ A_27a) @ (^ [V1p:((tyop_2Epair_2Eprod @ A_27a) @ A_27a)]: ((((c_2Ebool_2EIN @ ((tyop_2Epair_2Eprod @ A_27a) @ A_27a)) @ V1p) @ ((c_2Eset__relation_2Estrict @ A_27a) @ ((c_2Ewellorder_2Ewellorder__REP @ A_27a) @ V0w))))))))).
% 1.54/1.30 thf(thm_2Ewellorder_2EWIN__WF2, conjecture, (! [A_27a:$tType,V0w:(tyop_2Ewellorder_2Ewellorder @ A_27a)]: (((c_2Erelation_2EWF @ A_27a) @ (^ [V1x:A_27a,V2y:A_27a]: ((((c_2Ebool_2EIN @ ((tyop_2Epair_2Eprod @ A_27a) @ A_27a)) @ ((((c_2Epair_2E_2C @ A_27a) @ A_27a) @ V1x) @ V2y)) @ ((c_2Eset__relation_2Estrict @ A_27a) @ ((c_2Ewellorder_2Ewellorder__REP @ A_27a) @ V0w))))))))).
% 1.54/1.30 % SZS output end ListOfTHF for /export/starexec/sandbox/tmp/tmp.HpJsg7gn6n/DTF2DTF17586.p
% 1.54/1.30 ------------------------
% 1.74/1.30 ---- Cleaned THF ---
% 1.74/1.31 thf(tyop_2Emin_2Ebool,type,
% 1.74/1.31 tyop_2Emin_2Ebool: $tType ).
% 1.74/1.31
% 1.74/1.31 thf(tyop_2Emin_2Efun,type,
% 1.74/1.31 tyop_2Emin_2Efun: $tType > $tType > $tType ).
% 1.74/1.31
% 1.74/1.31 thf(tyop_2Epair_2Eprod,type,
% 1.74/1.31 tyop_2Epair_2Eprod: $tType > $tType > $tType ).
% 1.74/1.31
% 1.74/1.31 thf(tyop_2Ewellorder_2Ewellorder,type,
% 1.74/1.31 tyop_2Ewellorder_2Ewellorder: $tType > $tType ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Ebool_2E_21,type,
% 1.74/1.31 c_2Ebool_2E_21:
% 1.74/1.31 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Epair_2E_2C,type,
% 1.74/1.31 c_2Epair_2E_2C:
% 1.74/1.31 !>[A_27a: $tType,A_27b: $tType] : ( A_27a > A_27b > ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Ebool_2E_2F_5C,type,
% 1.74/1.31 c_2Ebool_2E_2F_5C: $o > $o > $o ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Emin_2E_3D,type,
% 1.74/1.31 c_2Emin_2E_3D:
% 1.74/1.31 !>[A_27a: $tType] : ( A_27a > A_27a > $o ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Emin_2E_3D_3D_3E,type,
% 1.74/1.31 c_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Ebool_2E_3F,type,
% 1.74/1.31 c_2Ebool_2E_3F:
% 1.74/1.31 !>[A_27a: $tType] : ( ( A_27a > $o ) > $o ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Epair_2ECURRY,type,
% 1.74/1.31 c_2Epair_2ECURRY:
% 1.74/1.31 !>[A_27a: $tType,A_27b: $tType,A_27c: $tType] : ( ( ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) > A_27c ) > A_27a > A_27b > A_27c ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Ebool_2EIN,type,
% 1.74/1.31 c_2Ebool_2EIN:
% 1.74/1.31 !>[A_27a: $tType] : ( A_27a > ( A_27a > $o ) > $o ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Erelation_2EWF,type,
% 1.74/1.31 c_2Erelation_2EWF:
% 1.74/1.31 !>[A_27a: $tType] : ( ( A_27a > A_27a > $o ) > $o ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Ebool_2E_5C_2F,type,
% 1.74/1.31 c_2Ebool_2E_5C_2F: $o > $o > $o ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Eset__relation_2Estrict,type,
% 1.74/1.31 c_2Eset__relation_2Estrict:
% 1.74/1.31 !>[A_27a: $tType] : ( ( ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o ) > ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Ewellorder_2Ewellfounded,type,
% 1.74/1.31 c_2Ewellorder_2Ewellfounded:
% 1.74/1.31 !>[A_27a: $tType] : ( ( ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o ) > $o ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Ewellorder_2Ewellorder__REP,type,
% 1.74/1.31 c_2Ewellorder_2Ewellorder__REP:
% 1.74/1.31 !>[A_27a: $tType] : ( ( tyop_2Ewellorder_2Ewellorder @ A_27a ) > ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o ) ).
% 1.74/1.31
% 1.74/1.31 thf(c_2Ebool_2E_7E,type,
% 1.74/1.31 c_2Ebool_2E_7E: $o > $o ).
% 1.74/1.31
% 1.74/1.31 thf(logicdef_2E_2F_5C,axiom,
% 1.74/1.31 ! [V0: $o,V1: $o] :
% 1.74/1.31 ( ( c_2Ebool_2E_2F_5C @ V0 @ V1 )
% 1.74/1.31 <=> ( V0
% 1.74/1.31 & V1 ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(logicdef_2E_5C_2F,axiom,
% 1.74/1.31 ! [V0: $o,V1: $o] :
% 1.74/1.31 ( ( c_2Ebool_2E_5C_2F @ V0 @ V1 )
% 1.74/1.31 <=> ( V0
% 1.74/1.31 | V1 ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(logicdef_2E_7E,axiom,
% 1.74/1.31 ! [V0: $o] :
% 1.74/1.31 ( ( c_2Ebool_2E_7E @ V0 )
% 1.74/1.31 <=> ( (~) @ V0 ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(logicdef_2E_3D_3D_3E,axiom,
% 1.74/1.31 ! [V0: $o,V1: $o] :
% 1.74/1.31 ( ( c_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 1.74/1.31 <=> ( V0
% 1.74/1.31 => V1 ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(logicdef_2E_3D,axiom,
% 1.74/1.31 ! [A_27a: $tType,V0: A_27a,V1: A_27a] :
% 1.74/1.31 ( ( c_2Emin_2E_3D @ A_27a @ V0 @ V1 )
% 1.74/1.31 <=> ( V0 = V1 ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(quantdef_2E_21,axiom,
% 1.74/1.31 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.74/1.31 ( ( c_2Ebool_2E_21 @ A_27a @ V0f )
% 1.74/1.31 <=> ! [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(quantdef_2E_3F,axiom,
% 1.74/1.31 ! [A_27a: $tType,V0f: A_27a > $o] :
% 1.74/1.31 ( ( c_2Ebool_2E_3F @ A_27a @ V0f )
% 1.74/1.31 <=> ? [V1x: A_27a] : ( V0f @ V1x ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(thm_2Ebool_2EETA__AX,axiom,
% 1.74/1.31 ! [A_27a: $tType,A_27b: $tType,V0t: A_27a > A_27b] :
% 1.74/1.31 ( ( ^ [V1x: A_27a] : ( V0t @ V1x ) )
% 1.74/1.31 = V0t ) ).
% 1.74/1.31
% 1.74/1.31 thf(thm_2Epair_2ECURRY__DEF,axiom,
% 1.74/1.31 ! [A_27a: $tType,A_27b: $tType,A_27c: $tType,V0f: ( tyop_2Epair_2Eprod @ A_27a @ A_27b ) > A_27c,V1x: A_27a,V2y: A_27b] :
% 1.74/1.31 ( ( c_2Epair_2ECURRY @ A_27a @ A_27b @ A_27c @ V0f @ V1x @ V2y )
% 1.74/1.31 = ( V0f @ ( c_2Epair_2E_2C @ A_27a @ A_27b @ V1x @ V2y ) ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(thm_2Ewellorder_2Ewellfounded__WF,axiom,
% 1.74/1.31 ! [A_27a: $tType,V0R: ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) > $o] :
% 1.74/1.31 ( ( c_2Ewellorder_2Ewellfounded @ A_27a @ V0R )
% 1.74/1.31 = ( c_2Erelation_2EWF @ A_27a @ ( c_2Epair_2ECURRY @ A_27a @ A_27a @ $o @ V0R ) ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(thm_2Ewellorder_2EWIN__WF,axiom,
% 1.74/1.31 ! [A_27a: $tType,V0w: tyop_2Ewellorder_2Ewellorder @ A_27a] :
% 1.74/1.31 ( c_2Ewellorder_2Ewellfounded @ A_27a
% 1.74/1.31 @ ^ [V1p: tyop_2Epair_2Eprod @ A_27a @ A_27a] : ( c_2Ebool_2EIN @ ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) @ V1p @ ( c_2Eset__relation_2Estrict @ A_27a @ ( c_2Ewellorder_2Ewellorder__REP @ A_27a @ V0w ) ) ) ) ).
% 1.74/1.31
% 1.74/1.31 thf(thm_2Ewellorder_2EWIN__WF2,conjecture,
% 1.74/1.31 ! [A_27a: $tType,V0w: tyop_2Ewellorder_2Ewellorder @ A_27a] :
% 1.74/1.31 ( c_2Erelation_2EWF @ A_27a
% 1.74/1.31 @ ^ [V1x: A_27a,V2y: A_27a] : ( c_2Ebool_2EIN @ ( tyop_2Epair_2Eprod @ A_27a @ A_27a ) @ ( c_2Epair_2E_2C @ A_27a @ A_27a @ V1x @ V2y ) @ ( c_2Eset__relation_2Estrict @ A_27a @ ( c_2Ewellorder_2Ewellorder__REP @ A_27a @ V0w ) ) ) ) ).
% 1.74/1.31 ------------------------
% 1.74/1.32 % (17705)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/275Mi)
% 1.74/1.32 % (17700)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/183Mi)
% 1.74/1.32 % (17701)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/4Mi)
% 1.74/1.32 % (17705)Refutation not found, incomplete strategy
% 1.74/1.32 % (17705)------------------------------
% 1.74/1.32 % (17705)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.32 % (17705)Termination reason: Refutation not found, incomplete strategy
% 1.74/1.32
% 1.74/1.32
% 1.74/1.32 % (17705)Memory used [KB]: 5500
% 1.74/1.32 % (17705)Time elapsed: 0.003 s
% 1.74/1.32 % (17705)Instructions burned: 3 (million)
% 1.74/1.32 % (17705)------------------------------
% 1.74/1.32 % (17705)------------------------------
% 1.74/1.32 % (17701)Instruction limit reached!
% 1.74/1.32 % (17701)------------------------------
% 1.74/1.32 % (17701)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.32 % (17701)Termination reason: Unknown
% 1.74/1.32 % (17701)Termination phase: Property scanning
% 1.74/1.32
% 1.74/1.32 % (17701)Memory used [KB]: 1023
% 1.74/1.32 % (17701)Time elapsed: 0.003 s
% 1.74/1.32 % (17701)Instructions burned: 4 (million)
% 1.74/1.32 % (17701)------------------------------
% 1.74/1.32 % (17701)------------------------------
% 1.74/1.33 % (17702)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/27Mi)
% 1.74/1.33 % (17703)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/2Mi)
% 1.74/1.33 % (17704)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/2Mi)
% 1.74/1.33 % (17706)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/18Mi)
% 1.74/1.33 % (17703)Instruction limit reached!
% 1.74/1.33 % (17703)------------------------------
% 1.74/1.33 % (17703)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.33 % (17703)Termination reason: Unknown
% 1.74/1.33 % (17703)Termination phase: Preprocessing 1
% 1.74/1.33 % (17704)Instruction limit reached!
% 1.74/1.33 % (17704)------------------------------
% 1.74/1.33 % (17704)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.33 % (17704)Termination reason: Unknown
% 1.74/1.33 % (17704)Termination phase: shuffling
% 1.74/1.33
% 1.74/1.33 % (17704)Memory used [KB]: 1023
% 1.74/1.33 % (17704)Time elapsed: 0.003 s
% 1.74/1.33 % (17704)Instructions burned: 2 (million)
% 1.74/1.33 % (17704)------------------------------
% 1.74/1.33 % (17704)------------------------------
% 1.74/1.33
% 1.74/1.33 % (17703)Memory used [KB]: 1023
% 1.74/1.33 % (17703)Time elapsed: 0.003 s
% 1.74/1.33 % (17703)Instructions burned: 2 (million)
% 1.74/1.33 % (17703)------------------------------
% 1.74/1.33 % (17703)------------------------------
% 1.74/1.33 % (17707)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/3Mi)
% 1.74/1.33 % (17707)Instruction limit reached!
% 1.74/1.33 % (17707)------------------------------
% 1.74/1.33 % (17707)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.33 % (17707)Termination reason: Unknown
% 1.74/1.33 % (17707)Termination phase: Property scanning
% 1.74/1.33
% 1.74/1.33 % (17707)Memory used [KB]: 1023
% 1.74/1.33 % (17707)Time elapsed: 0.002 s
% 1.74/1.33 % (17707)Instructions burned: 3 (million)
% 1.74/1.33 % (17707)------------------------------
% 1.74/1.33 % (17707)------------------------------
% 1.74/1.33 % (17708)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/37Mi)
% 1.74/1.34 % Exception at run slice level
% 1.74/1.34 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.74/1.34 % (17706)Instruction limit reached!
% 1.74/1.34 % (17706)------------------------------
% 1.74/1.34 % (17706)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.34 % (17706)Termination reason: Unknown
% 1.74/1.34 % (17706)Termination phase: Saturation
% 1.74/1.34
% 1.74/1.34 % (17706)Memory used [KB]: 5628
% 1.74/1.34 % (17706)Time elapsed: 0.014 s
% 1.74/1.34 % (17706)Instructions burned: 18 (million)
% 1.74/1.34 % (17706)------------------------------
% 1.74/1.34 % (17706)------------------------------
% 1.74/1.34 % (17711)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/1041Mi)
% 1.74/1.34 % Exception at run slice level
% 1.74/1.34 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.74/1.35 % (17712)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/7Mi)
% 1.74/1.35 % (17702)Instruction limit reached!
% 1.74/1.35 % (17702)------------------------------
% 1.74/1.35 % (17702)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.35 % (17710)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/3Mi)
% 1.74/1.35 % (17702)Termination reason: Unknown
% 1.74/1.35 % (17702)Termination phase: Saturation
% 1.74/1.35
% 1.74/1.35 % (17702)Memory used [KB]: 5756
% 1.74/1.35 % (17702)Time elapsed: 0.021 s
% 1.74/1.35 % (17702)Instructions burned: 28 (million)
% 1.74/1.35 % (17702)------------------------------
% 1.74/1.35 % (17702)------------------------------
% 1.74/1.35 % (17712)Instruction limit reached!
% 1.74/1.35 % (17712)------------------------------
% 1.74/1.35 % (17712)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.35 % (17712)Termination reason: Unknown
% 1.74/1.35 % (17712)Termination phase: Saturation
% 1.74/1.35
% 1.74/1.35 % (17712)Memory used [KB]: 1151
% 1.74/1.35 % (17712)Time elapsed: 0.005 s
% 1.74/1.35 % (17712)Instructions burned: 8 (million)
% 1.74/1.35 % (17712)------------------------------
% 1.74/1.35 % (17712)------------------------------
% 1.74/1.35 % (17710)Instruction limit reached!
% 1.74/1.35 % (17710)------------------------------
% 1.74/1.35 % (17710)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.35 % (17710)Termination reason: Unknown
% 1.74/1.35 % (17710)Termination phase: Saturation
% 1.74/1.35
% 1.74/1.35 % (17710)Memory used [KB]: 1023
% 1.74/1.35 % (17710)Time elapsed: 0.004 s
% 1.74/1.35 % (17710)Instructions burned: 3 (million)
% 1.74/1.35 % (17710)------------------------------
% 1.74/1.35 % (17710)------------------------------
% 1.74/1.35 % (17709)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/15Mi)
% 1.74/1.35 % (17714)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/3Mi)
% 1.74/1.35 % (17714)Instruction limit reached!
% 1.74/1.35 % (17714)------------------------------
% 1.74/1.35 % (17714)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.35 % (17714)Termination reason: Unknown
% 1.74/1.35 % (17714)Termination phase: Property scanning
% 1.74/1.35
% 1.74/1.35 % (17714)Memory used [KB]: 1023
% 1.74/1.35 % (17714)Time elapsed: 0.002 s
% 1.74/1.35 % (17714)Instructions burned: 3 (million)
% 1.74/1.35 % (17714)------------------------------
% 1.74/1.35 % (17714)------------------------------
% 1.74/1.36 % (17716)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/7Mi)
% 1.74/1.36 % (17713)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/16Mi)
% 1.74/1.36 % (17709)Instruction limit reached!
% 1.74/1.36 % (17709)------------------------------
% 1.74/1.36 % (17709)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.36 % (17709)Termination reason: Unknown
% 1.74/1.36 % (17709)Termination phase: Saturation
% 1.74/1.36
% 1.74/1.36 % (17709)Memory used [KB]: 5756
% 1.74/1.36 % (17709)Time elapsed: 0.013 s
% 1.74/1.36 % (17709)Instructions burned: 16 (million)
% 1.74/1.36 % (17709)------------------------------
% 1.74/1.36 % (17709)------------------------------
% 1.74/1.36 % (17716)Instruction limit reached!
% 1.74/1.36 % (17716)------------------------------
% 1.74/1.36 % (17716)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.36 % (17716)Termination reason: Unknown
% 1.74/1.36 % (17716)Termination phase: Saturation
% 1.74/1.36
% 1.74/1.36 % (17716)Memory used [KB]: 5628
% 1.74/1.36 % (17716)Time elapsed: 0.005 s
% 1.74/1.36 % (17716)Instructions burned: 8 (million)
% 1.74/1.36 % (17716)------------------------------
% 1.74/1.36 % (17716)------------------------------
% 1.74/1.36 % (17718)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/4Mi)
% 1.74/1.37 % (17718)Instruction limit reached!
% 1.74/1.37 % (17718)------------------------------
% 1.74/1.37 % (17718)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.37 % (17718)Termination reason: Unknown
% 1.74/1.37 % (17718)Termination phase: Saturation
% 1.74/1.37
% 1.74/1.37 % (17718)Memory used [KB]: 5500
% 1.74/1.37 % (17718)Time elapsed: 0.003 s
% 1.74/1.37 % (17715)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/3Mi)
% 1.74/1.37 % (17718)Instructions burned: 5 (million)
% 1.74/1.37 % (17718)------------------------------
% 1.74/1.37 % (17718)------------------------------
% 1.74/1.37 % (17717)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/3Mi)
% 1.74/1.37 % (17715)Instruction limit reached!
% 1.74/1.37 % (17715)------------------------------
% 1.74/1.37 % (17715)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.37 % (17715)Termination reason: Unknown
% 1.74/1.37 % (17715)Termination phase: Property scanning
% 1.74/1.37
% 1.74/1.37 % (17715)Memory used [KB]: 1023
% 1.74/1.37 % (17715)Time elapsed: 0.004 s
% 1.74/1.37 % (17715)Instructions burned: 4 (million)
% 1.74/1.37 % (17715)------------------------------
% 1.74/1.37 % (17715)------------------------------
% 1.74/1.37 % Exception at run slice level
% 1.74/1.37 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.74/1.37 % (17713)Instruction limit reached!
% 1.74/1.37 % (17713)------------------------------
% 1.74/1.37 % (17713)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.37 % (17713)Termination reason: Unknown
% 1.74/1.37 % (17713)Termination phase: Saturation
% 1.74/1.37
% 1.74/1.37 % (17713)Memory used [KB]: 5756
% 1.74/1.37 % (17713)Time elapsed: 0.013 s
% 1.74/1.37 % (17713)Instructions burned: 16 (million)
% 1.74/1.37 % (17713)------------------------------
% 1.74/1.37 % (17713)------------------------------
% 1.74/1.37 % (17720)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/710Mi)
% 1.74/1.37 % (17721)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/6Mi)
% 1.74/1.38 % (17721)Instruction limit reached!
% 1.74/1.38 % (17721)------------------------------
% 1.74/1.38 % (17721)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.38 % (17721)Termination reason: Unknown
% 1.74/1.38 % (17721)Termination phase: Saturation
% 1.74/1.38
% 1.74/1.38 % (17721)Memory used [KB]: 5500
% 1.74/1.38 % (17721)Time elapsed: 0.003 s
% 1.74/1.38 % (17721)Instructions burned: 6 (million)
% 1.74/1.38 % (17721)------------------------------
% 1.74/1.38 % (17721)------------------------------
% 1.74/1.38 % (17719)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/18Mi)
% 1.74/1.38 % (17700)Instruction limit reached!
% 1.74/1.38 % (17700)------------------------------
% 1.74/1.38 % (17700)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.38 % (17700)Termination reason: Unknown
% 1.74/1.38 % (17700)Termination phase: Saturation
% 1.74/1.38
% 1.74/1.38 % (17700)Memory used [KB]: 6780
% 1.74/1.38 % (17700)Time elapsed: 0.062 s
% 1.74/1.38 % (17700)Instructions burned: 183 (million)
% 1.74/1.38 % (17700)------------------------------
% 1.74/1.38 % (17700)------------------------------
% 1.74/1.38 % (17722)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/902Mi)
% 1.74/1.39 % (17723)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/21Mi)
% 1.74/1.39 % (17725)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/6Mi)
% 1.74/1.39 % Exception at run slice level
% 1.74/1.39 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.74/1.39 % (17724)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/5Mi)
% 1.74/1.39 % (17722)Refutation not found, incomplete strategy
% 1.74/1.39 % (17722)------------------------------
% 1.74/1.39 % (17722)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.39 % (17722)Termination reason: Refutation not found, incomplete strategy
% 1.74/1.39
% 1.74/1.39
% 1.74/1.39 % (17722)Memory used [KB]: 5500
% 1.74/1.39 % (17722)Time elapsed: 0.005 s
% 1.74/1.39 % (17722)Instructions burned: 4 (million)
% 1.74/1.39 % (17722)------------------------------
% 1.74/1.39 % (17722)------------------------------
% 1.74/1.39 % Exception at run slice level
% 1.74/1.39 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.74/1.39 % (17719)Instruction limit reached!
% 1.74/1.39 % (17719)------------------------------
% 1.74/1.39 % (17719)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.74/1.39 % (17719)Termination reason: Unknown
% 1.74/1.39 % (17719)Termination phase: Saturation
% 1.74/1.39
% 1.74/1.39 % (17719)Memory used [KB]: 5628
% 1.74/1.39 % (17719)Time elapsed: 0.014 s
% 1.74/1.39 % (17719)Instructions burned: 18 (million)
% 1.74/1.39 % (17719)------------------------------
% 1.74/1.39 % (17719)------------------------------
% 1.74/1.39 % (17726)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/377Mi)
% 1.76/1.40 % (17727)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/779Mi)
% 1.76/1.40 % Exception at run slice level
% 1.76/1.40 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.40 % (17723)Instruction limit reached!
% 1.76/1.40 % (17723)------------------------------
% 1.76/1.40 % (17723)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.40 % (17723)Termination reason: Unknown
% 1.76/1.40 % (17723)Termination phase: Saturation
% 1.76/1.40
% 1.76/1.40 % (17723)Memory used [KB]: 5628
% 1.76/1.40 % (17723)Time elapsed: 0.016 s
% 1.76/1.40 % (17723)Instructions burned: 21 (million)
% 1.76/1.40 % (17723)------------------------------
% 1.76/1.40 % (17723)------------------------------
% 1.76/1.41 % (17728)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/19Mi)
% 1.76/1.41 % (17729)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/879Mi)
% 1.76/1.41 % (17731)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/3Mi)
% 1.76/1.41 % Exception at run slice level
% 1.76/1.41 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.41 % (17731)Instruction limit reached!
% 1.76/1.41 % (17731)------------------------------
% 1.76/1.41 % (17731)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.41 % (17731)Termination reason: Unknown
% 1.76/1.41 % (17731)Termination phase: Equality resolution with deletion
% 1.76/1.41
% 1.76/1.41 % (17731)Memory used [KB]: 1023
% 1.76/1.41 % (17731)Time elapsed: 0.002 s
% 1.76/1.41 % (17731)Instructions burned: 3 (million)
% 1.76/1.41 % (17731)------------------------------
% 1.76/1.41 % (17731)------------------------------
% 1.76/1.41 % (17730)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/17Mi)
% 1.76/1.42 % (17734)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/100Mi)
% 1.76/1.42 % (17732)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/30Mi)
% 1.76/1.42 % (17733)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_17586 for (2999ds/127Mi)
% 1.76/1.42 % (17730)Instruction limit reached!
% 1.76/1.42 % (17730)------------------------------
% 1.76/1.42 % (17730)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.42 % (17730)Termination reason: Unknown
% 1.76/1.42 % (17730)Termination phase: Saturation
% 1.76/1.42
% 1.76/1.42 % (17730)Memory used [KB]: 5628
% 1.76/1.42 % (17730)Time elapsed: 0.014 s
% 1.76/1.42 % (17730)Instructions burned: 18 (million)
% 1.76/1.42 % (17730)------------------------------
% 1.76/1.42 % (17730)------------------------------
% 1.76/1.44 % (17732)Instruction limit reached!
% 1.76/1.44 % (17732)------------------------------
% 1.76/1.44 % (17732)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.44 % (17732)Termination reason: Unknown
% 1.76/1.44 % (17732)Termination phase: Saturation
% 1.76/1.44
% 1.76/1.44 % (17732)Memory used [KB]: 5756
% 1.76/1.44 % (17732)Time elapsed: 0.021 s
% 1.76/1.44 % (17732)Instructions burned: 30 (million)
% 1.76/1.44 % (17732)------------------------------
% 1.76/1.44 % (17732)------------------------------
% 1.76/1.44 % (17735)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=3:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/3Mi)
% 1.76/1.44 % Exception at run slice level
% 1.76/1.44 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.45 % (17734)Instruction limit reached!
% 1.76/1.45 % (17734)------------------------------
% 1.76/1.45 % (17734)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.45 % (17734)Termination reason: Unknown
% 1.76/1.45 % (17734)Termination phase: Saturation
% 1.76/1.45
% 1.76/1.45 % (17734)Memory used [KB]: 5884
% 1.76/1.45 % (17734)Time elapsed: 0.035 s
% 1.76/1.45 % (17734)Instructions burned: 102 (million)
% 1.76/1.45 % (17734)------------------------------
% 1.76/1.45 % (17734)------------------------------
% 1.76/1.45 % (17737)dis+1002_1:1_cbe=off:hud=5:nm=4:plsq=on:plsqr=7,1:prag=on:sp=const_max:tnu=1:i=86:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/86Mi)
% 1.76/1.45 % (17736)lrs+10_8:1_au=on:avsq=on:e2e=on:ins=3:s2a=on:s2at=3.0:ss=axioms:i=20:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/20Mi)
% 1.76/1.46 % (17738)lrs+1010_1:1_au=on:cbe=off:nm=2:ntd=on:sd=2:ss=axioms:st=5.0:i=107:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/107Mi)
% 1.76/1.46 % (17736)Instruction limit reached!
% 1.76/1.46 % (17736)------------------------------
% 1.76/1.46 % (17736)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.46 % (17736)Termination reason: Unknown
% 1.76/1.46 % (17736)Termination phase: Saturation
% 1.76/1.46
% 1.76/1.46 % (17736)Memory used [KB]: 5756
% 1.76/1.46 % (17736)Time elapsed: 0.011 s
% 1.76/1.46 % (17736)Instructions burned: 21 (million)
% 1.76/1.46 % (17736)------------------------------
% 1.76/1.46 % (17736)------------------------------
% 1.76/1.46 % (17733)Instruction limit reached!
% 1.76/1.46 % (17733)------------------------------
% 1.76/1.46 % (17733)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.46 % (17733)Termination reason: Unknown
% 1.76/1.46 % (17733)Termination phase: Saturation
% 1.76/1.46
% 1.76/1.46 % (17733)Memory used [KB]: 6268
% 1.76/1.46 % (17733)Time elapsed: 0.046 s
% 1.76/1.46 % (17733)Instructions burned: 129 (million)
% 1.76/1.46 % (17733)------------------------------
% 1.76/1.46 % (17733)------------------------------
% 1.76/1.47 % (17739)lrs+2_1:1024_cnfonf=lazy_gen:fe=off:hud=15:plsq=on:plsqc=1:plsqr=32,1:i=39:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/39Mi)
% 1.76/1.47 % Exception at run slice level
% 1.76/1.47 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.47 % (17740)dis+10_1:1_cnfonf=lazy_not_gen:fsr=off:kws=precedence:nwc=5.0:s2a=on:ss=axioms:st=1.5:i=448:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/448Mi)
% 1.76/1.48 % Exception at run slice level
% 1.76/1.48 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.48 % (17737)Instruction limit reached!
% 1.76/1.48 % (17737)------------------------------
% 1.76/1.48 % (17737)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.48 % (17737)Termination reason: Unknown
% 1.76/1.48 % (17737)Termination phase: Saturation
% 1.76/1.48
% 1.76/1.48 % (17737)Memory used [KB]: 5884
% 1.76/1.48 % (17737)Time elapsed: 0.032 s
% 1.76/1.48 % (17737)Instructions burned: 88 (million)
% 1.76/1.48 % (17737)------------------------------
% 1.76/1.48 % (17737)------------------------------
% 1.76/1.48 % (17741)lrs+10_1:512_au=on:fde=unused:lma=on:nm=32:plsq=on:plsqc=1:plsqr=16121663,131072:sfv=off:sp=const_max:ss=axioms:st=3.0:tgt=full:i=46:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/46Mi)
% 1.76/1.49 % (17742)lrs+10_1:10_au=on:av=off:cbe=off:cnfonf=lazy_pi_sigma_gen:ntd=on:plsq=on:plsqc=1:plsqr=32,1:i=98:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/98Mi)
% 1.76/1.49 % Exception at run slice level
% 1.76/1.49 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.49 % (17743)ott+1002_1:1_apa=on:au=on:bd=off:cnfonf=off:fd=off:sos=on:sp=weighted_frequency:i=507:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/507Mi)
% 1.76/1.49 % (17738)Instruction limit reached!
% 1.76/1.49 % (17738)------------------------------
% 1.76/1.49 % (17738)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.49 % (17738)Termination reason: Unknown
% 1.76/1.49 % (17738)Termination phase: Saturation
% 1.76/1.49
% 1.76/1.49 % (17738)Memory used [KB]: 6140
% 1.76/1.49 % (17738)Time elapsed: 0.035 s
% 1.76/1.49 % (17738)Instructions burned: 108 (million)
% 1.76/1.49 % (17738)------------------------------
% 1.76/1.49 % (17738)------------------------------
% 1.76/1.50 % (17743)Refutation not found, incomplete strategy
% 1.76/1.50 % (17743)------------------------------
% 1.76/1.50 % (17743)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.50 % (17743)Termination reason: Refutation not found, incomplete strategy
% 1.76/1.50
% 1.76/1.50
% 1.76/1.50 % (17743)Memory used [KB]: 5628
% 1.76/1.50 % (17743)Time elapsed: 0.004 s
% 1.76/1.50 % (17743)Instructions burned: 6 (million)
% 1.76/1.50 % (17743)------------------------------
% 1.76/1.50 % (17743)------------------------------
% 1.76/1.50 % (17744)dis+1010_2:3_amm=off:fd=preordered:ixr=off:nm=0:pe=on:piset=equals:prag=on:sac=on:tgt=ground:i=149:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/149Mi)
% 1.76/1.50 % (17741)Instruction limit reached!
% 1.76/1.50 % (17741)------------------------------
% 1.76/1.50 % (17741)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.50 % (17741)Termination reason: Unknown
% 1.76/1.50 % (17741)Termination phase: Saturation
% 1.76/1.50
% 1.76/1.50 % (17741)Memory used [KB]: 5884
% 1.76/1.50 % (17741)Time elapsed: 0.019 s
% 1.76/1.50 % (17741)Instructions burned: 47 (million)
% 1.76/1.50 % (17741)------------------------------
% 1.76/1.50 % (17741)------------------------------
% 1.76/1.50 % (17745)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/39Mi)
% 1.76/1.51 % (17746)lrs+1004_1:1_cnfonf=lazy_pi_sigma_gen:fe=off:gs=on:hud=10:prag=on:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/6Mi)
% 1.76/1.51 % Exception at run slice level
% 1.76/1.51 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.51 % (17747)dis+1002_1:1_aac=none:au=on:e2e=on:nm=2:nwc=10.0:sd=1:ss=axioms:st=3.0:i=1087:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/1087Mi)
% 1.76/1.52 % (17745)Instruction limit reached!
% 1.76/1.52 % (17745)------------------------------
% 1.76/1.52 % (17745)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.52 % (17748)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/47Mi)
% 1.76/1.52 % (17745)Termination reason: Unknown
% 1.76/1.52 % (17745)Termination phase: Saturation
% 1.76/1.52
% 1.76/1.52 % (17745)Memory used [KB]: 5756
% 1.76/1.52 % (17745)Time elapsed: 0.015 s
% 1.76/1.52 % (17745)Instructions burned: 41 (million)
% 1.76/1.52 % (17745)------------------------------
% 1.76/1.52 % (17745)------------------------------
% 1.76/1.53 % (17749)lrs+1010_1:128_av=off:cbe=off:cnfonf=lazy_simp:fsr=off:ntd=on:ss=axioms:st=1.5:i=44:si=on:rtra=on_0 on DTF2THF_17586 for (2998ds/44Mi)
% 1.76/1.53 % (17726)Instruction limit reached!
% 1.76/1.53 % (17726)------------------------------
% 1.76/1.53 % (17726)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.53 % (17726)Termination reason: Unknown
% 1.76/1.53 % (17726)Termination phase: Saturation
% 1.76/1.53
% 1.76/1.53 % (17726)Memory used [KB]: 6268
% 1.76/1.53 % (17726)Time elapsed: 0.136 s
% 1.76/1.53 % (17726)Instructions burned: 378 (million)
% 1.76/1.53 % (17726)------------------------------
% 1.76/1.53 % (17726)------------------------------
% 1.76/1.53 % Exception at run slice level
% 1.76/1.53 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.54 % (17748)Instruction limit reached!
% 1.76/1.54 % (17748)------------------------------
% 1.76/1.54 % (17748)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.54 % (17748)Termination reason: Unknown
% 1.76/1.54 % (17748)Termination phase: Saturation
% 1.76/1.54
% 1.76/1.54 % (17748)Memory used [KB]: 5756
% 1.76/1.54 % (17748)Time elapsed: 0.020 s
% 1.76/1.54 % (17748)Instructions burned: 49 (million)
% 1.76/1.54 % (17748)------------------------------
% 1.76/1.54 % (17748)------------------------------
% 1.76/1.54 % (17751)lrs+10_7:1_cnfonf=lazy_gen:fe=off:nwc=5.0:plsq=on:i=62:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/62Mi)
% 1.76/1.54 % (17750)dis+10_1:1_av=off:bd=off:cnfonf=lazy_gen:fe=off:hud=10:plsq=on:plsqc=1:plsqr=32,1:prag=on:tnu=1:i=432:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/432Mi)
% 1.76/1.54 % Exception at run slice level
% 1.76/1.54 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.54 % Exception at run slice level
% 1.76/1.54 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.55 % (17752)lrs+1010_1:16_add=large:amm=off:anc=all_dependent:chr=on:fd=off:ins=2:sp=const_max:tnu=5:uhcvi=on:i=31:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/31Mi)
% 1.76/1.55 % (17744)Instruction limit reached!
% 1.76/1.55 % (17744)------------------------------
% 1.76/1.55 % (17744)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.55 % (17744)Termination reason: Unknown
% 1.76/1.55 % (17744)Termination phase: Saturation
% 1.76/1.55
% 1.76/1.55 % (17744)Memory used [KB]: 6012
% 1.76/1.55 % (17744)Time elapsed: 0.053 s
% 1.76/1.55 % (17744)Instructions burned: 151 (million)
% 1.76/1.55 % (17744)------------------------------
% 1.76/1.55 % (17744)------------------------------
% 1.76/1.55 % (17753)dis+10_1:128_hud=1:i=96:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/96Mi)
% 1.76/1.55 % (17754)lrs+1002_1:4_au=on:cbe=off:cnfonf=lazy_pi_sigma_gen:hud=15:inj=on:nwc=4.0:s2a=on:sac=on:sp=reverse_arity:i=453:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/453Mi)
% 1.76/1.55 % Exception at run slice level
% 1.76/1.55 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.56 % (17755)lrs-1004_1:1_au=on:bsd=on:cbe=off:cnfonf=off:fe=axiom:fsd=on:i=71:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/71Mi)
% 1.76/1.56 % (17752)Instruction limit reached!
% 1.76/1.56 % (17752)------------------------------
% 1.76/1.56 % (17752)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.56 % (17752)Termination reason: Unknown
% 1.76/1.56 % (17752)Termination phase: Saturation
% 1.76/1.56
% 1.76/1.56 % (17752)Memory used [KB]: 5756
% 1.76/1.56 % (17752)Time elapsed: 0.013 s
% 1.76/1.56 % (17752)Instructions burned: 33 (million)
% 1.76/1.56 % (17752)------------------------------
% 1.76/1.56 % (17752)------------------------------
% 1.76/1.56 % (17756)dis+1002_1:1_bd=off:fsr=off:ntd=on:s2a=on:ss=axioms:i=83:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/83Mi)
% 1.76/1.57 % (17757)lrs+10_1:128_cnfonf=lazy_not_gen_be_off:hud=1:ins=1:i=11:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/11Mi)
% 1.76/1.57 % Exception at run slice level
% 1.76/1.57 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.58 % (17753)Instruction limit reached!
% 1.76/1.58 % (17753)------------------------------
% 1.76/1.58 % (17753)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.58 % (17753)Termination reason: Unknown
% 1.76/1.58 % (17753)Termination phase: Saturation
% 1.76/1.58
% 1.76/1.58 % (17753)Memory used [KB]: 5884
% 1.76/1.58 % (17753)Time elapsed: 0.032 s
% 1.76/1.58 % (17753)Instructions burned: 96 (million)
% 1.76/1.58 % (17753)------------------------------
% 1.76/1.58 % (17753)------------------------------
% 1.76/1.58 % (17758)lrs+1010_1:1_au=on:cbe=off:cnfonf=lazy_not_gen_be_off:fsr=off:spb=non_intro:i=41:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/41Mi)
% 1.76/1.58 % Exception at run slice level
% 1.76/1.58 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.58 % (17755)Instruction limit reached!
% 1.76/1.58 % (17755)------------------------------
% 1.76/1.58 % (17755)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.58 % (17755)Termination reason: Unknown
% 1.76/1.58 % (17755)Termination phase: Saturation
% 1.76/1.58
% 1.76/1.58 % (17755)Memory used [KB]: 6012
% 1.76/1.58 % (17755)Time elapsed: 0.027 s
% 1.76/1.58 % (17755)Instructions burned: 72 (million)
% 1.76/1.58 % (17755)------------------------------
% 1.76/1.58 % (17755)------------------------------
% 1.76/1.59 % (17756)Instruction limit reached!
% 1.76/1.59 % (17756)------------------------------
% 1.76/1.59 % (17756)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.59 % (17756)Termination reason: Unknown
% 1.76/1.59 % (17756)Termination phase: Saturation
% 1.76/1.59
% 1.76/1.59 % (17756)Memory used [KB]: 5884
% 1.76/1.59 % (17756)Time elapsed: 0.029 s
% 1.76/1.59 % (17756)Instructions burned: 83 (million)
% 1.76/1.59 % (17756)------------------------------
% 1.76/1.59 % (17756)------------------------------
% 1.76/1.59 % (17759)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/6Mi)
% 1.76/1.59 % (17760)dis+10_1:1_avsq=on:cnfonf=off:e2e=on:nm=32:i=150:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/150Mi)
% 1.76/1.59 % (17759)Instruction limit reached!
% 1.76/1.59 % (17759)------------------------------
% 1.76/1.59 % (17759)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.59 % (17759)Termination reason: Unknown
% 1.76/1.59 % (17759)Termination phase: Saturation
% 1.76/1.59
% 1.76/1.59 % (17759)Memory used [KB]: 5628
% 1.76/1.59 % (17759)Time elapsed: 0.004 s
% 1.76/1.59 % (17759)Instructions burned: 8 (million)
% 1.76/1.59 % (17759)------------------------------
% 1.76/1.59 % (17759)------------------------------
% 1.76/1.59 % (17761)ott+1010_1:1_au=on:s2a=on:sd=7:ss=axioms:st=1.5:i=343:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/343Mi)
% 1.76/1.60 % (17762)ott+1010_1:4_cbe=off:chr=on:hfsq=on:hfsqr=1,16:hud=3:sac=on:sp=unary_frequency:ss=axioms:st=5.0:tnu=2:i=109:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/109Mi)
% 1.76/1.60 % (17763)dis+10_1:1_au=on:c=on:e2e=on:fsr=off:sos=all:sp=const_frequency:ss=axioms:i=253:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/253Mi)
% 1.76/1.60 % (17763)Refutation not found, incomplete strategy
% 1.76/1.60 % (17763)------------------------------
% 1.76/1.60 % (17763)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.60 % (17763)Termination reason: Refutation not found, incomplete strategy
% 1.76/1.60
% 1.76/1.60
% 1.76/1.60 % (17763)Memory used [KB]: 5500
% 1.76/1.60 % (17763)Time elapsed: 0.002 s
% 1.76/1.60 % (17763)Instructions burned: 2 (million)
% 1.76/1.60 % (17763)------------------------------
% 1.76/1.60 % (17763)------------------------------
% 1.76/1.61 % (17720)Instruction limit reached!
% 1.76/1.61 % (17720)------------------------------
% 1.76/1.61 % (17720)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.61 % (17720)Termination reason: Unknown
% 1.76/1.61 % (17720)Termination phase: Saturation
% 1.76/1.61
% 1.76/1.61 % (17720)Memory used [KB]: 8699
% 1.76/1.61 % (17720)Time elapsed: 0.240 s
% 1.76/1.61 % (17720)Instructions burned: 710 (million)
% 1.76/1.61 % (17720)------------------------------
% 1.76/1.61 % (17720)------------------------------
% 1.76/1.61 % (17764)lrs+10_1:1_au=on:cnfonf=off:sd=1:sgt=16:ss=axioms:i=140:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/140Mi)
% 1.76/1.62 % (17765)dis+1010_16:1_acc=model:au=on:avsq=on:cond=fast:plsq=on:plsqc=2:plsqr=9267,262144:i=614:si=on:rtra=on_0 on DTF2THF_17586 for (2997ds/614Mi)
% 1.76/1.63 % (17762)Instruction limit reached!
% 1.76/1.63 % (17762)------------------------------
% 1.76/1.63 % (17762)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.63 % (17762)Termination reason: Unknown
% 1.76/1.63 % (17762)Termination phase: Saturation
% 1.76/1.63
% 1.76/1.63 % (17762)Memory used [KB]: 6268
% 1.76/1.63 % (17762)Time elapsed: 0.056 s
% 1.76/1.63 % (17762)Instructions burned: 110 (million)
% 1.76/1.63 % (17762)------------------------------
% 1.76/1.63 % (17762)------------------------------
% 1.76/1.64 % (17766)lrs+1002_1:1_e2e=on:fde=unused:fe=axiom:prag=on:sd=1:sos=on:ss=axioms:st=2.0:i=202:si=on:rtra=on_0 on DTF2THF_17586 for (2996ds/202Mi)
% 1.76/1.64 % (17760)Instruction limit reached!
% 1.76/1.64 % (17760)------------------------------
% 1.76/1.64 % (17760)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.64 % (17760)Termination reason: Unknown
% 1.76/1.64 % (17760)Termination phase: Saturation
% 1.76/1.64
% 1.76/1.64 % (17760)Memory used [KB]: 6268
% 1.76/1.64 % (17760)Time elapsed: 0.054 s
% 1.76/1.64 % (17760)Instructions burned: 151 (million)
% 1.76/1.64 % (17760)------------------------------
% 1.76/1.64 % (17760)------------------------------
% 1.76/1.64 % (17766)Refutation not found, incomplete strategy
% 1.76/1.64 % (17766)------------------------------
% 1.76/1.64 % (17766)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.64 % (17766)Termination reason: Refutation not found, incomplete strategy
% 1.76/1.64
% 1.76/1.64
% 1.76/1.64 % (17766)Memory used [KB]: 5500
% 1.76/1.64 % (17766)Time elapsed: 0.003 s
% 1.76/1.64 % (17766)Instructions burned: 3 (million)
% 1.76/1.64 % (17766)------------------------------
% 1.76/1.64 % (17766)------------------------------
% 1.76/1.65 % (17771)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=283:si=on:rtra=on_0 on DTF2THF_17586 for (2996ds/283Mi)
% 1.76/1.65 % (17770)dis+1002_1:1_au=on:cs=on:ins=3:kws=inv_frequency:nwc=10.0:ss=axioms:st=3.0:i=339:si=on:rtra=on_0 on DTF2THF_17586 for (2996ds/339Mi)
% 1.76/1.65 % Exception at run slice level
% 1.76/1.65 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.66 % (17764)Instruction limit reached!
% 1.76/1.66 % (17764)------------------------------
% 1.76/1.66 % (17764)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.66 % (17764)Termination reason: Unknown
% 1.76/1.66 % (17764)Termination phase: Saturation
% 1.76/1.66
% 1.76/1.66 % (17764)Memory used [KB]: 6268
% 1.76/1.66 % (17764)Time elapsed: 0.068 s
% 1.76/1.66 % (17764)Instructions burned: 141 (million)
% 1.76/1.66 % (17764)------------------------------
% 1.76/1.66 % (17764)------------------------------
% 1.76/1.66 % (17772)dis+2_1:1_cha=on:hud=7:nwc=3.0:prag=on:tnu=2:i=134:si=on:rtra=on_0 on DTF2THF_17586 for (2996ds/134Mi)
% 1.76/1.67 % (17773)dis+1010_1:64_cnfonf=lazy_simp:fd=off:i=298:si=on:rtra=on_0 on DTF2THF_17586 for (2996ds/298Mi)
% 1.76/1.67 % Exception at run slice level
% 1.76/1.67 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.68 % (17788)lrs+2_1:8_erd=off:plsq=on:plsqr=32,1:sos=on:i=192:si=on:rtra=on_0 on DTF2THF_17586 for (2996ds/192Mi)
% 1.76/1.71 % (17772)Instruction limit reached!
% 1.76/1.71 % (17772)------------------------------
% 1.76/1.71 % (17772)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.71 % (17729)Instruction limit reached!
% 1.76/1.71 % (17729)------------------------------
% 1.76/1.71 % (17729)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.71 % (17729)Termination reason: Unknown
% 1.76/1.71 % (17729)Termination phase: Saturation
% 1.76/1.71
% 1.76/1.71 % (17729)Memory used [KB]: 9083
% 1.76/1.71 % (17729)Time elapsed: 0.304 s
% 1.76/1.71 % (17729)Instructions burned: 879 (million)
% 1.76/1.71 % (17729)------------------------------
% 1.76/1.71 % (17729)------------------------------
% 1.76/1.71 % (17772)Termination reason: Unknown
% 1.76/1.71 % (17772)Termination phase: Saturation
% 1.76/1.71
% 1.76/1.71 % (17772)Memory used [KB]: 6012
% 1.76/1.71 % (17772)Time elapsed: 0.069 s
% 1.76/1.71 % (17772)Instructions burned: 136 (million)
% 1.76/1.71 % (17772)------------------------------
% 1.76/1.71 % (17772)------------------------------
% 1.76/1.72 % (17761)Instruction limit reached!
% 1.76/1.72 % (17761)------------------------------
% 1.76/1.72 % (17761)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.72 % (17761)Termination reason: Unknown
% 1.76/1.72 % (17761)Termination phase: Saturation
% 1.76/1.72
% 1.76/1.72 % (17761)Memory used [KB]: 7036
% 1.76/1.72 % (17761)Time elapsed: 0.126 s
% 1.76/1.72 % (17761)Instructions burned: 343 (million)
% 1.76/1.72 % (17761)------------------------------
% 1.76/1.72 % (17761)------------------------------
% 1.76/1.72 % (17789)lrs+10_1:1_bd=off:hud=1:nm=0:prag=on:sd=2:sgt=32:sos=all:ss=axioms:i=258:si=on:rtra=on_0 on DTF2THF_17586 for (2996ds/258Mi)
% 1.76/1.72 % (17790)lrs+1002_1:1024_au=on:cond=fast:ntd=on:piset=and:plsq=on:plsqc=1:plsqr=183491,1048576:sac=on:tgt=ground:i=90:si=on:rtra=on_0 on DTF2THF_17586 for (2996ds/90Mi)
% 1.76/1.73 % (17791)dis+1004_16:1_avsq=on:avsqr=1,16:cnfonf=lazy_gen:cs=on:fe=off:tgt=ground:tnu=1:i=231:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/231Mi)
% 1.76/1.73 % Exception at run slice level
% 1.76/1.73 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.74 % (17788)Instruction limit reached!
% 1.76/1.74 % (17788)------------------------------
% 1.76/1.74 % (17788)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.74 % (17788)Termination reason: Unknown
% 1.76/1.74 % (17788)Termination phase: Saturation
% 1.76/1.74
% 1.76/1.74 % (17788)Memory used [KB]: 6652
% 1.76/1.74 % (17788)Time elapsed: 0.061 s
% 1.76/1.74 % (17788)Instructions burned: 194 (million)
% 1.76/1.74 % (17788)------------------------------
% 1.76/1.74 % (17788)------------------------------
% 1.76/1.74 % (17792)lrs+1002_1:1_au=on:s2a=on:sgt=32:slsq=on:slsqc=1:slsql=off:ss=axioms:i=458:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/458Mi)
% 1.76/1.75 % (17793)lrs+1010_1:16_add=large:amm=off:anc=all_dependent:chr=on:fd=off:ins=2:sp=const_max:tnu=5:uhcvi=on:i=31:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/31Mi)
% 1.76/1.75 % (17790)Instruction limit reached!
% 1.76/1.75 % (17790)------------------------------
% 1.76/1.75 % (17790)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.75 % (17790)Termination reason: Unknown
% 1.76/1.75 % (17790)Termination phase: Saturation
% 1.76/1.75
% 1.76/1.75 % (17790)Memory used [KB]: 5884
% 1.76/1.75 % (17790)Time elapsed: 0.033 s
% 1.76/1.75 % (17790)Instructions burned: 92 (million)
% 1.76/1.75 % (17790)------------------------------
% 1.76/1.75 % (17790)------------------------------
% 1.76/1.76 % (17793)Instruction limit reached!
% 1.76/1.76 % (17793)------------------------------
% 1.76/1.76 % (17793)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.76 % (17793)Termination reason: Unknown
% 1.76/1.76 % (17793)Termination phase: Saturation
% 1.76/1.76
% 1.76/1.76 % (17793)Memory used [KB]: 5756
% 1.76/1.76 % (17793)Time elapsed: 0.012 s
% 1.76/1.76 % (17793)Instructions burned: 32 (million)
% 1.76/1.76 % (17793)------------------------------
% 1.76/1.76 % (17793)------------------------------
% 1.76/1.76 % (17794)lrs+10_1:1_cnfonf=lazy_gen:kws=inv_precedence:nwc=10.0:s2a=on:sp=weighted_frequency:ss=axioms:i=297:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/297Mi)
% 1.76/1.76 % Exception at run slice level
% 1.76/1.76 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.77 % (17770)Instruction limit reached!
% 1.76/1.77 % (17770)------------------------------
% 1.76/1.77 % (17770)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.77 % (17770)Termination reason: Unknown
% 1.76/1.77 % (17770)Termination phase: Saturation
% 1.76/1.77
% 1.76/1.77 % (17770)Memory used [KB]: 6524
% 1.76/1.77 % (17770)Time elapsed: 0.136 s
% 1.76/1.77 % (17770)Instructions burned: 341 (million)
% 1.76/1.77 % (17770)------------------------------
% 1.76/1.77 % (17770)------------------------------
% 1.76/1.77 % (17795)dis+2_1:4_amm=off:au=on:cbe=off:cnfonf=lazy_gen:hfaw=0:hfsq=on:hfsql=off:plsq=on:plsqc=1:plsqr=35,4:sac=on:i=987:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/987Mi)
% 1.76/1.77 % Exception at run slice level
% 1.76/1.77 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.77 % (17796)lrs+10_1:1024_avsq=on:avsqc=4:avsqr=584411,1048576:bd=off:bet=on:br=off:chr=on:fsd=on:fsdmm=1:hud=10:nm=0:ntd=on:nwc=9.0:piset=or:plsq=on:plsqc=2:plsql=on:plsqr=852219,1048576:rawr=on:sp=const_frequency:spb=units:i=182:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/182Mi)
% 1.76/1.78 % (17797)dis+10_1:1_au=on:e2e=on:fde=none:nwc=10.0:s2a=on:s2at=2.0:i=182:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/182Mi)
% 1.76/1.78 % (17798)dis+10_1:8_cha=on:cnfonf=lazy_pi_sigma_gen:fe=axiom:hud=5:plsq=on:plsqr=32,1:prag=on:sos=all:i=154:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/154Mi)
% 1.76/1.78 % Exception at run slice level
% 1.76/1.78 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.79 % (17799)dis+1003_1:64_atotf=0.4:au=on:fsr=off:hflw=5:hfsq=on:hfsqc=20:hfsql=off:plsq=on:plsqc=1:plsqr=32,1:i=79:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/79Mi)
% 1.76/1.80 % (17789)Instruction limit reached!
% 1.76/1.80 % (17789)------------------------------
% 1.76/1.80 % (17789)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.80 % (17789)Termination reason: Unknown
% 1.76/1.80 % (17789)Termination phase: Saturation
% 1.76/1.80
% 1.76/1.80 % (17789)Memory used [KB]: 6396
% 1.76/1.80 % (17789)Time elapsed: 0.083 s
% 1.76/1.80 % (17789)Instructions burned: 261 (million)
% 1.76/1.80 % (17789)------------------------------
% 1.76/1.80 % (17789)------------------------------
% 1.76/1.81 % (17800)dis+1010_5:2_anc=all_dependent:awrs=converge:bd=off:bet=on:c=on:cha=on:cnfonf=lazy_not_gen_be_off:fe=axiom:hud=5:kws=precedence:piset=and:prag=on:s2a=on:sac=on:slsq=on:slsqc=1:sp=reverse_arity:ss=axioms:st=1.5:i=216:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/216Mi)
% 1.76/1.81 % Exception at run slice level
% 1.76/1.81 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.82 % (17799)Instruction limit reached!
% 1.76/1.82 % (17799)------------------------------
% 1.76/1.82 % (17799)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.82 % (17799)Termination reason: Unknown
% 1.76/1.82 % (17799)Termination phase: Saturation
% 1.76/1.82
% 1.76/1.82 % (17799)Memory used [KB]: 5884
% 1.76/1.82 % (17799)Time elapsed: 0.028 s
% 1.76/1.82 % (17799)Instructions burned: 81 (million)
% 1.76/1.82 % (17799)------------------------------
% 1.76/1.82 % (17799)------------------------------
% 1.76/1.82 % (17801)lrs+1002_1:1_fe=off:hud=10:ins=2:sac=on:sp=const_frequency:i=114:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/114Mi)
% 1.76/1.82 % (17765)Instruction limit reached!
% 1.76/1.82 % (17765)------------------------------
% 1.76/1.82 % (17765)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.82 % (17765)Termination reason: Unknown
% 1.76/1.82 % (17765)Termination phase: Saturation
% 1.76/1.82
% 1.76/1.82 % (17765)Memory used [KB]: 7036
% 1.76/1.82 % (17765)Time elapsed: 0.226 s
% 1.76/1.82 % (17765)Instructions burned: 614 (million)
% 1.76/1.82 % (17765)------------------------------
% 1.76/1.82 % (17765)------------------------------
% 1.76/1.83 % (17802)dis+1002_1:1_acc=on:au=on:bd=off:e2e=on:sgt=8:ss=axioms:i=922:si=on:rtra=on_0 on DTF2THF_17586 for (2995ds/922Mi)
% 1.76/1.83 % (17796)Instruction limit reached!
% 1.76/1.83 % (17796)------------------------------
% 1.76/1.83 % (17796)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.83 % (17796)Termination reason: Unknown
% 1.76/1.83 % (17796)Termination phase: Saturation
% 1.76/1.83
% 1.76/1.83 % (17796)Memory used [KB]: 6396
% 1.76/1.83 % (17796)Time elapsed: 0.057 s
% 1.76/1.83 % (17796)Instructions burned: 183 (million)
% 1.76/1.83 % (17796)------------------------------
% 1.76/1.83 % (17796)------------------------------
% 1.76/1.83 % (17797)Instruction limit reached!
% 1.76/1.83 % (17797)------------------------------
% 1.76/1.83 % (17797)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.83 % (17797)Termination reason: Unknown
% 1.76/1.83 % (17797)Termination phase: Saturation
% 1.76/1.83
% 1.76/1.83 % (17797)Memory used [KB]: 6140
% 1.76/1.83 % (17797)Time elapsed: 0.057 s
% 1.76/1.83 % (17797)Instructions burned: 182 (million)
% 1.76/1.83 % (17797)------------------------------
% 1.76/1.83 % (17797)------------------------------
% 1.76/1.83 % (17803)lrs+10_1:128_au=on:bd=off:cnfonf=lazy_not_gen_be_off:nwc=10.0:piset=and:i=182:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/182Mi)
% 1.76/1.83 % Exception at run slice level
% 1.76/1.83 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.84 % (17804)ott+1010_1:1024_au=on:av=off:c=on:cnfonf=conj_eager:piset=equals:s2a=on:sp=occurrence:spb=units:ss=axioms:i=164:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/164Mi)
% 1.76/1.84 % (17804)Refutation not found, incomplete strategy
% 1.76/1.84 % (17804)------------------------------
% 1.76/1.84 % (17804)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.84 % (17804)Termination reason: Refutation not found, incomplete strategy
% 1.76/1.84
% 1.76/1.84
% 1.76/1.84 % (17804)Memory used [KB]: 1151
% 1.76/1.84 % (17804)Time elapsed: 0.004 s
% 1.76/1.84 % (17804)Instructions burned: 6 (million)
% 1.76/1.84 % (17804)------------------------------
% 1.76/1.84 % (17804)------------------------------
% 1.76/1.84 % (17805)lrs+1004_1:1_cnfonf=lazy_pi_sigma_gen:fe=off:gs=on:hud=10:prag=on:tnu=1:i=50:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/50Mi)
% 1.76/1.84 % Exception at run slice level
% 1.76/1.84 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.84 % (17806)dis-30_1:1_acc=on:bd=off:fsr=off:plsq=on:plsqr=32,1:i=368:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/368Mi)
% 1.76/1.85 % (17807)dis+2_1:1_bd=off:e2e=on:hud=1:nm=3:piset=or:prag=on:s2a=on:sp=const_max:i=1021:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/1021Mi)
% 1.76/1.85 % (17808)dis+10_1:1_cnfonf=lazy_gen:fe=off:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=267:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/267Mi)
% 1.76/1.85 % Exception at run slice level
% 1.76/1.85 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.86 % (17747)Instruction limit reached!
% 1.76/1.86 % (17747)------------------------------
% 1.76/1.86 % (17747)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.86 % (17747)Termination reason: Unknown
% 1.76/1.86 % (17747)Termination phase: Saturation
% 1.76/1.86
% 1.76/1.86 % (17747)Memory used [KB]: 8059
% 1.76/1.86 % (17747)Time elapsed: 0.347 s
% 1.76/1.86 % (17747)Instructions burned: 1090 (million)
% 1.76/1.86 % (17747)------------------------------
% 1.76/1.86 % (17747)------------------------------
% 1.76/1.86 % (17801)Instruction limit reached!
% 1.76/1.86 % (17801)------------------------------
% 1.76/1.86 % (17801)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.86 % (17801)Termination reason: Unknown
% 1.76/1.86 % (17801)Termination phase: Saturation
% 1.76/1.86
% 1.76/1.86 % (17801)Memory used [KB]: 6012
% 1.76/1.86 % (17801)Time elapsed: 0.037 s
% 1.76/1.86 % (17801)Instructions burned: 115 (million)
% 1.76/1.86 % (17801)------------------------------
% 1.76/1.86 % (17801)------------------------------
% 1.76/1.86 % (17809)dis+21_1:5_au=on:ntd=on:nwc=5.0:s2a=on:ss=axioms:st=5.0:i=204:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/204Mi)
% 1.76/1.87 % (17810)dis+2_1:1024_atotf=0.0802881:au=on:bs=unit_only:cnfonf=lazy_not_gen_be_off:fde=none:nwc=10.0:prag=on:i=26:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/26Mi)
% 1.76/1.87 % (17811)dis+1002_1:1_bd=preordered:c=on:cbe=off:cnfonf=lazy_not_gen_be_off:hud=10:ixr=off:prag=on:i=53:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/53Mi)
% 1.76/1.87 % Exception at run slice level
% 1.76/1.87 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.87 % Exception at run slice level
% 1.76/1.87 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.88 % (17812)dis+1002_1:1_aac=none:au=on:e2e=on:nm=2:nwc=10.0:sd=1:ss=axioms:st=3.0:i=4436:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/4436Mi)
% 1.76/1.88 % (17813)dis+1010_1:1_acc=model:avsq=on:ixr=off:prag=on:s2a=on:sac=on:i=1539:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/1539Mi)
% 1.76/1.88 % (17792)Instruction limit reached!
% 1.76/1.88 % (17792)------------------------------
% 1.76/1.88 % (17792)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.89 % (17792)Termination reason: Unknown
% 1.76/1.89 % (17792)Termination phase: Saturation
% 1.76/1.89
% 1.76/1.89 % (17792)Memory used [KB]: 7419
% 1.76/1.89 % (17792)Time elapsed: 0.146 s
% 1.76/1.89 % (17792)Instructions burned: 460 (million)
% 1.76/1.89 % (17792)------------------------------
% 1.76/1.89 % (17792)------------------------------
% 1.76/1.90 % (17814)lrs+2_1:1_bd=off:e2e=on:fde=none:kws=inv_precedence:plsq=on:plsqr=32,1:sos=on:i=408:si=on:rtra=on_0 on DTF2THF_17586 for (2994ds/408Mi)
% 1.76/1.92 % (17809)Instruction limit reached!
% 1.76/1.92 % (17809)------------------------------
% 1.76/1.92 % (17809)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.92 % (17809)Termination reason: Unknown
% 1.76/1.92 % (17809)Termination phase: Saturation
% 1.76/1.92
% 1.76/1.92 % (17809)Memory used [KB]: 6268
% 1.76/1.92 % (17809)Time elapsed: 0.063 s
% 1.76/1.92 % (17809)Instructions burned: 205 (million)
% 1.76/1.92 % (17809)------------------------------
% 1.76/1.92 % (17809)------------------------------
% 1.76/1.93 % (17815)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=5205:si=on:rtra=on_0 on DTF2THF_17586 for (2993ds/5205Mi)
% 1.76/1.93 % Exception at run slice level
% 1.76/1.93 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 1.76/1.94 % (17816)dis+1010_1:4_au=on:av=off:cbe=off:nwc=10.0:s2a=on:s2at=3.0:sd=2:ss=axioms:st=5.0:i=1913:si=on:rtra=on_0 on DTF2THF_17586 for (2993ds/1913Mi)
% 1.76/1.96 % (17806)Instruction limit reached!
% 1.76/1.96 % (17806)------------------------------
% 1.76/1.96 % (17806)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.76/1.96 % (17806)Termination reason: Unknown
% 1.76/1.96 % (17806)Termination phase: Saturation
% 1.76/1.96
% 1.76/1.96 % (17806)Memory used [KB]: 7164
% 1.76/1.96 % (17806)Time elapsed: 0.115 s
% 1.76/1.96 % (17806)Instructions burned: 369 (million)
% 1.76/1.96 % (17806)------------------------------
% 1.76/1.96 % (17806)------------------------------
% 1.76/1.97 % (17817)lrs+2_1:1_bd=off:cbe=off:piset=equals:sd=1:sgt=20:sos=all:ss=axioms:i=4350:si=on:rtra=on_0 on DTF2THF_17586 for (2993ds/4350Mi)
% 6.58/2.02 % (17814)Instruction limit reached!
% 6.58/2.02 % (17814)------------------------------
% 6.58/2.02 % (17814)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 6.58/2.02 % (17814)Termination reason: Unknown
% 6.58/2.02 % (17814)Termination phase: Saturation
% 6.58/2.02
% 6.58/2.02 % (17814)Memory used [KB]: 7164
% 6.58/2.02 % (17814)Time elapsed: 0.127 s
% 6.58/2.02 % (17814)Instructions burned: 408 (million)
% 6.58/2.02 % (17814)------------------------------
% 6.58/2.02 % (17814)------------------------------
% 6.58/2.03 % (17818)ott+1010_1:4_cbe=off:chr=on:hfsq=on:hfsqr=1,16:hud=3:sac=on:sp=unary_frequency:ss=axioms:st=5.0:tnu=2:i=68:si=on:rtra=on_0 on DTF2THF_17586 for (2993ds/68Mi)
% 6.58/2.05 % (17818)Instruction limit reached!
% 6.58/2.05 % (17818)------------------------------
% 6.58/2.05 % (17818)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 6.58/2.05 % (17818)Termination reason: Unknown
% 6.58/2.05 % (17818)Termination phase: Saturation
% 6.58/2.05
% 6.58/2.05 % (17818)Memory used [KB]: 6012
% 6.58/2.05 % (17818)Time elapsed: 0.023 s
% 6.58/2.05 % (17818)Instructions burned: 68 (million)
% 6.58/2.05 % (17818)------------------------------
% 6.58/2.05 % (17818)------------------------------
% 6.58/2.06 % (17819)dis+10_1:1_au=on:nwc=5.0:s2a=on:s2at=2.0:sac=on:sd=7:ss=axioms:st=2.0:i=358:si=on:rtra=on_0 on DTF2THF_17586 for (2992ds/358Mi)
% 6.58/2.10 % (17802)Instruction limit reached!
% 6.58/2.10 % (17802)------------------------------
% 6.58/2.10 % (17802)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 6.58/2.10 % (17802)Termination reason: Unknown
% 6.58/2.10 % (17802)Termination phase: Saturation
% 6.58/2.10
% 6.58/2.10 % (17802)Memory used [KB]: 7419
% 6.58/2.10 % (17802)Time elapsed: 0.277 s
% 6.58/2.10 % (17802)Instructions burned: 924 (million)
% 6.58/2.10 % (17802)------------------------------
% 6.58/2.10 % (17802)------------------------------
% 7.22/2.11 % (17820)lrs+1010_1:16_add=large:amm=off:anc=all_dependent:chr=on:fd=off:ins=2:sp=const_max:tnu=5:uhcvi=on:i=31:si=on:rtra=on_0 on DTF2THF_17586 for (2992ds/31Mi)
% 7.22/2.12 % (17820)Instruction limit reached!
% 7.22/2.12 % (17820)------------------------------
% 7.22/2.12 % (17820)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 7.22/2.12 % (17820)Termination reason: Unknown
% 7.22/2.12 % (17820)Termination phase: Saturation
% 7.22/2.12
% 7.22/2.12 % (17820)Memory used [KB]: 5756
% 7.22/2.12 % (17820)Time elapsed: 0.013 s
% 7.22/2.12 % (17820)Instructions burned: 33 (million)
% 7.22/2.12 % (17820)------------------------------
% 7.22/2.12 % (17820)------------------------------
% 7.22/2.13 % (17821)lrs+10_1:1_cnfonf=lazy_simp:sgt=5:sos=on:ss=axioms:i=279:si=on:rtra=on_0 on DTF2THF_17586 for (2992ds/279Mi)
% 7.22/2.13 % Exception at run slice level
% 7.22/2.13 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 7.22/2.14 % (17822)lrs+10_8:1_au=on:fde=none:slsq=on:i=258:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/258Mi)
% 7.22/2.17 % (17819)Instruction limit reached!
% 7.22/2.17 % (17819)------------------------------
% 7.22/2.17 % (17819)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 7.22/2.17 % (17819)Termination reason: Unknown
% 7.22/2.17 % (17819)Termination phase: Saturation
% 7.22/2.17
% 7.22/2.17 % (17819)Memory used [KB]: 6396
% 7.22/2.17 % (17819)Time elapsed: 0.110 s
% 7.22/2.17 % (17819)Instructions burned: 360 (million)
% 7.22/2.17 % (17819)------------------------------
% 7.22/2.17 % (17819)------------------------------
% 7.22/2.17 % (17807)Instruction limit reached!
% 7.22/2.17 % (17807)------------------------------
% 7.22/2.17 % (17807)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 7.22/2.17 % (17807)Termination reason: Unknown
% 7.22/2.17 % (17807)Termination phase: Saturation
% 7.22/2.17
% 7.22/2.17 % (17807)Memory used [KB]: 8699
% 7.22/2.17 % (17807)Time elapsed: 0.335 s
% 7.22/2.17 % (17807)Instructions burned: 1022 (million)
% 7.22/2.17 % (17807)------------------------------
% 7.22/2.17 % (17807)------------------------------
% 7.22/2.18 % (17823)dis+2_1:1024_atotf=0.0802881:au=on:bs=unit_only:cnfonf=lazy_not_gen_be_off:fde=none:nwc=10.0:prag=on:i=26:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/26Mi)
% 7.22/2.18 % (17824)lrs+1010_1:1_au=on:cbe=off:cnfonf=lazy_not_be_gen:ntd=on:pe=on:i=995:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/995Mi)
% 7.22/2.18 % Exception at run slice level% Exception at run slice level
% 7.22/2.18 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 7.22/2.18
% 7.22/2.18 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 7.22/2.19 % (17826)lrs+1010_1:128_au=on:cnfonf=lazy_pi_sigma_gen:hflw=4:hfsq=on:hfsqc=20:hfsql=off:i=253:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/253Mi)
% 7.22/2.19 % (17825)dis+10_1:8_amm=sco:cbe=off:hflw=5:hfsq=on:hfsqc=14:hfsql=off:hfsqr=4,1:hud=5:ile=on:lma=on:nm=2:ntd=on:prag=on:sac=on:sp=frequency:i=373:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/373Mi)
% 7.22/2.19 % Exception at run slice level
% 7.22/2.19 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 7.81/2.20 % (17827)lrs+1002_1:14_au=on:bd=off:e2e=on:fde=unused:sac=on:sos=on:i=832:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/832Mi)
% 7.81/2.20 % (17827)Refutation not found, incomplete strategy
% 7.81/2.20 % (17827)------------------------------
% 7.81/2.20 % (17827)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 7.81/2.20 % (17827)Termination reason: Refutation not found, incomplete strategy
% 7.81/2.20
% 7.81/2.20
% 7.81/2.20 % (17827)Memory used [KB]: 5500
% 7.81/2.20 % (17827)Time elapsed: 0.003 s
% 7.81/2.20 % (17827)Instructions burned: 5 (million)
% 7.81/2.20 % (17827)------------------------------
% 7.81/2.20 % (17827)------------------------------
% 7.81/2.21 % (17828)lrs+1010_1:1_chr=on:cnfonf=lazy_not_be_gen:gs=on:hud=5:plsq=on:plsqc=1:plsqr=5,1:prag=on:rawr=on:i=668:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/668Mi)
% 7.81/2.21 % Exception at run slice level
% 7.81/2.21 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 7.81/2.22 % (17829)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=40:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/40Mi)
% 7.81/2.22 % Exception at run slice level
% 7.81/2.22 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 7.81/2.23 % (17822)Instruction limit reached!
% 7.81/2.23 % (17822)------------------------------
% 7.81/2.23 % (17822)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 7.81/2.23 % (17822)Termination reason: Unknown
% 7.81/2.23 % (17822)Termination phase: Saturation
% 7.81/2.23
% 7.81/2.23 % (17822)Memory used [KB]: 6780
% 7.81/2.23 % (17822)Time elapsed: 0.107 s
% 7.81/2.23 % (17822)Instructions burned: 261 (million)
% 7.81/2.23 % (17822)------------------------------
% 7.81/2.23 % (17822)------------------------------
% 7.81/2.23 % (17830)lrs+1010_1:1_cnfonf=lazy_pi_sigma_gen:fd=off:ntd=on:sd=1:sgt=32:sos=on:ss=axioms:i=294:si=on:rtra=on_0 on DTF2THF_17586 for (2991ds/294Mi)
% 7.81/2.24 % Exception at run slice level
% 7.81/2.24 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 7.81/2.24 % (17831)dis+1010_1:1_avsq=on:fe=off:fsr=off:hud=10:plsq=on:plsqr=32,1:prag=on:i=187:si=on:rtra=on_0 on DTF2THF_17586 for (2990ds/187Mi)
% 7.81/2.24 % (17832)lrs+1010_2:3_au=on:fsr=off:sd=4:ss=axioms:st=1.5:i=371:si=on:rtra=on_0 on DTF2THF_17586 for (2990ds/371Mi)
% 8.35/2.30 % (17831)Instruction limit reached!
% 8.35/2.30 % (17831)------------------------------
% 8.35/2.30 % (17831)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 8.35/2.30 % (17831)Termination reason: Unknown
% 8.35/2.30 % (17831)Termination phase: Saturation
% 8.35/2.30
% 8.35/2.30 % (17831)Memory used [KB]: 6396
% 8.35/2.30 % (17831)Time elapsed: 0.059 s
% 8.35/2.30 % (17831)Instructions burned: 189 (million)
% 8.35/2.30 % (17831)------------------------------
% 8.35/2.30 % (17831)------------------------------
% 8.35/2.31 % (17833)dis+1003_1:1_au=on:bd=preordered:fde=none:ixr=off:nwc=10.0:i=1827:si=on:rtra=on_0 on DTF2THF_17586 for (2990ds/1827Mi)
% 8.35/2.32 % (17825)Instruction limit reached!
% 8.35/2.32 % (17825)------------------------------
% 8.35/2.32 % (17825)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 8.35/2.32 % (17825)Termination reason: Unknown
% 8.35/2.32 % (17825)Termination phase: Saturation
% 8.35/2.32
% 8.35/2.32 % (17825)Memory used [KB]: 6908
% 8.35/2.32 % (17825)Time elapsed: 0.150 s
% 8.35/2.32 % (17825)Instructions burned: 375 (million)
% 8.35/2.32 % (17825)------------------------------
% 8.35/2.32 % (17825)------------------------------
% 8.35/2.33 % (17834)lrs+10_1:1_av=off:bd=off:cnfonf=lazy_gen:fe=off:hud=10:plsq=on:plsqc=1:plsqr=32,1:tnu=1:i=70:si=on:rtra=on_0 on DTF2THF_17586 for (2989ds/70Mi)
% 8.35/2.33 % Exception at run slice level
% 8.35/2.33 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 8.35/2.34 % (17835)lrs+10_1:20_bd=off:cnfonf=lazy_not_be_gen:fe=axiom:hud=10:ins=1:nm=20:prag=on:sos=on:i=316:si=on:rtra=on_0 on DTF2THF_17586 for (2989ds/316Mi)
% 8.35/2.34 % Exception at run slice level
% 8.35/2.34 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 8.35/2.34 % (17813)Instruction limit reached!
% 8.35/2.34 % (17813)------------------------------
% 8.35/2.34 % (17813)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 8.35/2.34 % (17813)Termination reason: Unknown
% 8.35/2.34 % (17813)Termination phase: Saturation
% 8.35/2.34
% 8.35/2.34 % (17813)Memory used [KB]: 9210
% 8.35/2.34 % (17813)Time elapsed: 0.466 s
% 8.35/2.34 % (17813)Instructions burned: 1540 (million)
% 8.35/2.34 % (17813)------------------------------
% 8.35/2.34 % (17813)------------------------------
% 8.35/2.35 % (17836)ott+1010_1:1_cnfonf=lazy_gen:fe=off:plsq=on:plsqc=1:plsqr=3548551,65536:s2a=on:i=932:si=on:rtra=on_0 on DTF2THF_17586 for (2989ds/932Mi)
% 8.35/2.35 % Exception at run slice level
% 8.35/2.35 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 8.35/2.35 % (17837)lrs+1010_1:128_au=on:bd=preordered:cnfonf=lazy_pi_sigma_gen:plsq=on:plsqc=1:plsqr=32,1:sos=all:sp=occurrence:i=4714:si=on:rtra=on_0 on DTF2THF_17586 for (2989ds/4714Mi)
% 8.35/2.35 % Exception at run slice level
% 8.35/2.35 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 8.35/2.36 % (17838)dis+10_1:1_au=on:e2e=on:fde=none:nwc=10.0:s2a=on:s2at=2.0:i=8250:si=on:rtra=on_0 on DTF2THF_17586 for (2989ds/8250Mi)
% 8.35/2.36 % (17832)Instruction limit reached!
% 8.35/2.36 % (17832)------------------------------
% 8.35/2.36 % (17832)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 8.35/2.36 % (17832)Termination reason: Unknown
% 8.35/2.36 % (17832)Termination phase: Saturation
% 8.35/2.36
% 8.35/2.36 % (17832)Memory used [KB]: 7419
% 8.35/2.36 % (17832)Time elapsed: 0.117 s
% 8.35/2.36 % (17832)Instructions burned: 374 (million)
% 8.35/2.36 % (17832)------------------------------
% 8.35/2.36 % (17832)------------------------------
% 8.35/2.36 % (17839)lrs+1002_1:1_apa=on:cnfonf=off:fd=off:flr=on:hud=1:lcm=reverse:prag=on:sd=1:sos=on:ss=axioms:i=770:si=on:rtra=on_0 on DTF2THF_17586 for (2989ds/770Mi)
% 8.35/2.37 % (17840)ott+1010_5:1_av=off:fe=off:ins=1:kws=precedence:sp=reverse_arity:i=794:si=on:rtra=on_0 on DTF2THF_17586 for (2989ds/794Mi)
% 9.36/2.52 % (17816)Instruction limit reached!
% 9.36/2.52 % (17816)------------------------------
% 9.36/2.52 % (17816)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 9.36/2.52 % (17816)Termination reason: Unknown
% 9.36/2.52 % (17816)Termination phase: Saturation
% 9.36/2.52
% 9.36/2.52 % (17816)Memory used [KB]: 4093
% 9.36/2.52 % (17816)Time elapsed: 0.589 s
% 9.36/2.52 % (17816)Instructions burned: 1914 (million)
% 9.36/2.52 % (17816)------------------------------
% 9.36/2.52 % (17816)------------------------------
% 9.36/2.53 % (17841)dis+1002_1:1_au=on:avsq=on:avsqr=1,16:cond=on:sp=frequency:i=464:si=on:rtra=on_0 on DTF2THF_17586 for (2987ds/464Mi)
% 9.60/2.60 % (17839)Instruction limit reached!
% 9.60/2.60 % (17839)------------------------------
% 9.60/2.60 % (17839)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 9.60/2.60 % (17839)Termination reason: Unknown
% 9.60/2.60 % (17839)Termination phase: Saturation
% 9.60/2.60
% 9.60/2.60 % (17839)Memory used [KB]: 8187
% 9.60/2.60 % (17839)Time elapsed: 0.238 s
% 9.60/2.60 % (17839)Instructions burned: 771 (million)
% 9.60/2.60 % (17839)------------------------------
% 9.60/2.60 % (17839)------------------------------
% 9.60/2.61 % (17842)ott+21_1:3_avsq=on:bd=off:cnfonf=lazy_gen:fe=off:hud=10:ixr=off:plsq=on:plsqc=1:plsqr=32,1:prag=on:tnu=1:i=1376:si=on:rtra=on_0 on DTF2THF_17586 for (2987ds/1376Mi)
% 9.60/2.61 % Exception at run slice level
% 9.60/2.61 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 9.60/2.62 % (17843)dis+10_1:1_etr=on:plsq=on:plsqc=1:plsqr=32,1:i=906:si=on:rtra=on_0 on DTF2THF_17586 for (2987ds/906Mi)
% 9.60/2.62 % (17840)Instruction limit reached!
% 9.60/2.62 % (17840)------------------------------
% 9.60/2.62 % (17840)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 9.60/2.62 % (17840)Termination reason: Unknown
% 9.60/2.62 % (17840)Termination phase: Saturation
% 9.60/2.62
% 9.60/2.62 % (17840)Memory used [KB]: 3070
% 9.60/2.62 % (17840)Time elapsed: 0.251 s
% 9.60/2.62 % (17840)Instructions burned: 795 (million)
% 9.60/2.62 % (17840)------------------------------
% 9.60/2.62 % (17840)------------------------------
% 9.60/2.63 % (17844)lrs+1002_1:16_bd=off:e2e=on:fde=unused:kws=precedence:sac=on:sos=on:ss=axioms:i=434:si=on:rtra=on_0 on DTF2THF_17586 for (2986ds/434Mi)
% 9.60/2.68 % (17841)Instruction limit reached!
% 9.60/2.68 % (17841)------------------------------
% 9.60/2.68 % (17841)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 9.60/2.68 % (17841)Termination reason: Unknown
% 9.60/2.68 % (17841)Termination phase: Saturation
% 9.60/2.68
% 9.60/2.68 % (17841)Memory used [KB]: 6652
% 9.60/2.68 % (17841)Time elapsed: 0.151 s
% 9.60/2.68 % (17841)Instructions burned: 465 (million)
% 9.60/2.68 % (17841)------------------------------
% 9.60/2.68 % (17841)------------------------------
% 9.60/2.69 % (17848)lrs+10_5:4_cnfonf=conj_eager:fe=axiom:hflw=5:hfsq=on:hfsqc=10:hfsql=off:hud=10:plsq=on:sgt=5:spb=goal_then_units:ss=axioms:i=865:si=on:rtra=on_0 on DTF2THF_17586 for (2986ds/865Mi)
% 10.47/2.77 % (17844)Instruction limit reached!
% 10.47/2.77 % (17844)------------------------------
% 10.47/2.77 % (17844)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 10.47/2.77 % (17844)Termination reason: Unknown
% 10.47/2.77 % (17844)Termination phase: Saturation
% 10.47/2.77
% 10.47/2.77 % (17844)Memory used [KB]: 7164
% 10.47/2.77 % (17844)Time elapsed: 0.141 s
% 10.47/2.77 % (17844)Instructions burned: 436 (million)
% 10.47/2.77 % (17844)------------------------------
% 10.47/2.77 % (17844)------------------------------
% 10.47/2.78 % (17863)dis+1002_1:1_cnfonf=lazy_simp:hud=5:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=593:si=on:rtra=on_0 on DTF2THF_17586 for (2985ds/593Mi)
% 10.47/2.78 % Exception at run slice level
% 10.47/2.78 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 10.47/2.79 % (17864)dis+10_1:1_sd=2:sgt=20:slsq=on:ss=axioms:st=6.0:i=443:si=on:rtra=on_0 on DTF2THF_17586 for (2985ds/443Mi)
% 10.82/2.87 % (17833)Instruction limit reached!
% 10.82/2.87 % (17833)------------------------------
% 10.82/2.87 % (17833)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 10.82/2.87 % (17833)Termination reason: Unknown
% 10.82/2.87 % (17833)Termination phase: Saturation
% 10.82/2.87
% 10.82/2.87 % (17833)Memory used [KB]: 9083
% 10.82/2.87 % (17833)Time elapsed: 0.565 s
% 10.82/2.87 % (17833)Instructions burned: 1827 (million)
% 10.82/2.87 % (17833)------------------------------
% 10.82/2.87 % (17833)------------------------------
% 10.82/2.88 % (17865)dis+10_1:1_atotf=0.1:cbe=off:sd=3:ss=axioms:st=2.0:i=594:si=on:rtra=on_0 on DTF2THF_17586 for (2984ds/594Mi)
% 11.59/2.92 % (17843)Instruction limit reached!
% 11.59/2.92 % (17843)------------------------------
% 11.59/2.92 % (17843)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 11.59/2.92 % (17843)Termination reason: Unknown
% 11.59/2.92 % (17843)Termination phase: Saturation
% 11.59/2.92
% 11.59/2.92 % (17843)Memory used [KB]: 12537
% 11.59/2.92 % (17843)Time elapsed: 0.305 s
% 11.59/2.92 % (17843)Instructions burned: 907 (million)
% 11.59/2.92 % (17843)------------------------------
% 11.59/2.92 % (17843)------------------------------
% 11.59/2.93 % (17864)Instruction limit reached!
% 11.59/2.93 % (17864)------------------------------
% 11.59/2.93 % (17864)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 11.59/2.93 % (17864)Termination reason: Unknown
% 11.59/2.93 % (17864)Termination phase: Saturation
% 11.59/2.93
% 11.59/2.93 % (17864)Memory used [KB]: 7291
% 11.59/2.93 % (17864)Time elapsed: 0.141 s
% 11.59/2.93 % (17864)Instructions burned: 443 (million)
% 11.59/2.93 % (17864)------------------------------
% 11.59/2.93 % (17864)------------------------------
% 11.59/2.93 % (17866)ott+10_1:1024_anc=none:bd=off:e2e=on:fde=none:fsr=off:hud=10:ixr=off:nm=4:nwc=5.0:spb=goal:i=327:si=on:rtra=on_0 on DTF2THF_17586 for (2983ds/327Mi)
% 11.59/2.94 % (17867)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=5411:si=on:rtra=on_0 on DTF2THF_17586 for (2983ds/5411Mi)
% 11.59/2.94 % (17867)Refutation not found, incomplete strategy
% 11.59/2.94 % (17867)------------------------------
% 11.59/2.94 % (17867)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 11.59/2.94 % (17867)Termination reason: Refutation not found, incomplete strategy
% 11.59/2.94
% 11.59/2.94
% 11.59/2.94 % (17867)Memory used [KB]: 5500
% 11.59/2.94 % (17867)Time elapsed: 0.003 s
% 11.59/2.94 % (17867)Instructions burned: 1 (million)
% 11.59/2.94 % (17867)------------------------------
% 11.59/2.94 % (17867)------------------------------
% 11.59/2.94 % (17848)Instruction limit reached!
% 11.59/2.94 % (17848)------------------------------
% 11.59/2.94 % (17848)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 11.59/2.94 % (17848)Termination reason: Unknown
% 11.59/2.94 % (17848)Termination phase: Saturation
% 11.59/2.94
% 11.59/2.94 % (17848)Memory used [KB]: 10618
% 11.59/2.94 % (17848)Time elapsed: 0.260 s
% 11.59/2.94 % (17848)Instructions burned: 866 (million)
% 11.59/2.94 % (17848)------------------------------
% 11.59/2.94 % (17848)------------------------------
% 11.59/2.95 % (17868)lrs+10_1:20_au=on:c=on:cbe=off:cnfonf=lazy_gen:ins=1:plsq=on:plsqc=1:plsqr=46,31:sac=on:i=1762:si=on:rtra=on_0 on DTF2THF_17586 for (2983ds/1762Mi)
% 11.59/2.95 % Exception at run slice level
% 11.59/2.95 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 11.59/2.95 % (17869)dis+1003_1:64_cha=on:cnfonf=lazy_gen:hud=9:nwc=8.0:prag=on:i=96:si=on:rtra=on_0 on DTF2THF_17586 for (2983ds/96Mi)
% 11.59/2.96 % Exception at run slice level
% 11.59/2.96 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 11.59/2.96 % (17870)lrs+21_1:1_hud=5:kws=inv_frequency:nm=16:nwc=2.0:prag=on:sos=on:ss=axioms:i=503:si=on:rtra=on_0 on DTF2THF_17586 for (2983ds/503Mi)
% 11.59/2.96 % (17871)lrs+1002_1:1024_au=on:cond=fast:ntd=on:piset=and:plsq=on:plsqc=1:plsqr=183491,1048576:sac=on:tgt=ground:i=90:si=on:rtra=on_0 on DTF2THF_17586 for (2983ds/90Mi)
% 11.59/3.00 % (17871)Instruction limit reached!
% 11.59/3.00 % (17871)------------------------------
% 11.59/3.00 % (17871)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 11.59/3.00 % (17871)Termination reason: Unknown
% 11.59/3.00 % (17871)Termination phase: Saturation
% 11.59/3.00
% 11.59/3.00 % (17871)Memory used [KB]: 5884
% 11.59/3.00 % (17871)Time elapsed: 0.032 s
% 11.59/3.00 % (17871)Instructions burned: 91 (million)
% 11.59/3.00 % (17871)------------------------------
% 11.59/3.00 % (17871)------------------------------
% 11.59/3.01 % (17872)lrs+10_1:64_hud=5:plsq=on:plsqr=2011171,524288:i=593:si=on:rtra=on_0 on DTF2THF_17586 for (2983ds/593Mi)
% 13.53/3.03 % (17866)Instruction limit reached!
% 13.53/3.03 % (17866)------------------------------
% 13.53/3.03 % (17866)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 13.53/3.03 % (17866)Termination reason: Unknown
% 13.53/3.03 % (17866)Termination phase: Saturation
% 13.53/3.03
% 13.53/3.03 % (17866)Memory used [KB]: 7036
% 13.53/3.03 % (17866)Time elapsed: 0.099 s
% 13.53/3.03 % (17866)Instructions burned: 328 (million)
% 13.53/3.03 % (17866)------------------------------
% 13.53/3.03 % (17866)------------------------------
% 13.53/3.04 % (17873)dis-1002_1:1_alpa=false:apa=on:au=on:bd=off:cnfonf=off:e2e=on:er=filter:fde=unused:plsq=on:plsqr=9699663,1048576:s2a=on:sos=on:sp=unary_first:i=1512:si=on:rtra=on_0 on DTF2THF_17586 for (2982ds/1512Mi)
% 13.53/3.04 % (17873)Refutation not found, incomplete strategy
% 13.53/3.04 % (17873)------------------------------
% 13.53/3.04 % (17873)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 13.53/3.04 % (17873)Termination reason: Refutation not found, incomplete strategy
% 13.53/3.04
% 13.53/3.04
% 13.53/3.04 % (17873)Memory used [KB]: 5628
% 13.53/3.04 % (17873)Time elapsed: 0.004 s
% 13.53/3.04 % (17873)Instructions burned: 6 (million)
% 13.53/3.04 % (17873)------------------------------
% 13.53/3.04 % (17873)------------------------------
% 13.53/3.05 % (17874)lrs+1002_1:128_cbe=off:cnfonf=lazy_not_gen_be_off:ins=1:i=569:si=on:rtra=on_0 on DTF2THF_17586 for (2982ds/569Mi)
% 13.53/3.05 % Exception at run slice level
% 13.53/3.05 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 13.53/3.06 % (17865)Instruction limit reached!
% 13.53/3.06 % (17865)------------------------------
% 13.53/3.06 % (17865)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 13.53/3.06 % (17865)Termination reason: Unknown
% 13.53/3.06 % (17865)Termination phase: Saturation
% 13.53/3.06
% 13.53/3.06 % (17865)Memory used [KB]: 7931
% 13.53/3.06 % (17865)Time elapsed: 0.180 s
% 13.53/3.06 % (17865)Instructions burned: 597 (million)
% 13.53/3.06 % (17865)------------------------------
% 13.53/3.06 % (17865)------------------------------
% 13.53/3.06 % (17875)ott+1002_1:1_bd=off:cnfonf=off:e2e=on:fd=off:fe=axiom:hud=5:prag=on:sos=on:i=501:si=on:rtra=on_0 on DTF2THF_17586 for (2982ds/501Mi)
% 13.53/3.07 % (17875)Refutation not found, incomplete strategy
% 13.53/3.07 % (17875)------------------------------
% 13.53/3.07 % (17875)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 13.53/3.07 % (17875)Termination reason: Refutation not found, incomplete strategy
% 13.53/3.07
% 13.53/3.07
% 13.53/3.07 % (17875)Memory used [KB]: 5628
% 13.53/3.07 % (17875)Time elapsed: 0.004 s
% 13.53/3.07 % (17875)Instructions burned: 8 (million)
% 13.53/3.07 % (17875)------------------------------
% 13.53/3.07 % (17875)------------------------------
% 13.53/3.07 % (17876)lrs+1010_1:3_cnfonf=conj_eager:fsr=off:prag=on:sd=4:sgt=10:ss=axioms:i=562:si=on:rtra=on_0 on DTF2THF_17586 for (2982ds/562Mi)
% 13.53/3.08 % (17877)lrs+10_1:1_au=on:cnfonf=off:fde=unused:kws=precedence:tgt=full:i=406:si=on:rtra=on_0 on DTF2THF_17586 for (2982ds/406Mi)
% 14.16/3.12 % (17870)Instruction limit reached!
% 14.16/3.12 % (17870)------------------------------
% 14.16/3.12 % (17870)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 14.16/3.12 % (17870)Termination reason: Unknown
% 14.16/3.12 % (17870)Termination phase: Saturation
% 14.16/3.12
% 14.16/3.12 % (17870)Memory used [KB]: 7419
% 14.16/3.12 % (17870)Time elapsed: 0.157 s
% 14.16/3.12 % (17870)Instructions burned: 505 (million)
% 14.16/3.12 % (17870)------------------------------
% 14.16/3.12 % (17870)------------------------------
% 14.16/3.13 % (17878)dis+1004_1:128_au=on:cbe=off:e2e=on:sac=on:i=582:si=on:rtra=on_0 on DTF2THF_17586 for (2982ds/582Mi)
% 14.16/3.19 % (17872)Instruction limit reached!
% 14.16/3.19 % (17872)------------------------------
% 14.16/3.19 % (17872)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 14.16/3.19 % (17872)Termination reason: Unknown
% 14.16/3.19 % (17872)Termination phase: Saturation
% 14.16/3.19
% 14.16/3.19 % (17872)Memory used [KB]: 7419
% 14.16/3.19 % (17872)Time elapsed: 0.186 s
% 14.16/3.19 % (17872)Instructions burned: 595 (million)
% 14.16/3.19 % (17872)------------------------------
% 14.16/3.19 % (17872)------------------------------
% 14.51/3.20 % (17812)Instruction limit reached!
% 14.51/3.20 % (17812)------------------------------
% 14.51/3.20 % (17812)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 14.51/3.20 % (17812)Termination reason: Unknown
% 14.51/3.20 % (17812)Termination phase: Saturation
% 14.51/3.20
% 14.51/3.20 % (17812)Memory used [KB]: 12153
% 14.51/3.20 % (17812)Time elapsed: 1.336 s
% 14.51/3.20 % (17812)Instructions burned: 4437 (million)
% 14.51/3.20 % (17812)------------------------------
% 14.51/3.20 % (17812)------------------------------
% 14.51/3.20 % (17879)lrs+2_1:1_au=on:bd=off:bsr=unit_only:sd=2:sgt=32:sos=all:ss=axioms:i=456:si=on:rtra=on_0 on DTF2THF_17586 for (2981ds/456Mi)
% 14.51/3.21 % (17877)Instruction limit reached!
% 14.51/3.21 % (17877)------------------------------
% 14.51/3.21 % (17877)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 14.51/3.21 % (17877)Termination reason: Unknown
% 14.51/3.21 % (17877)Termination phase: Saturation
% 14.51/3.21
% 14.51/3.21 % (17877)Memory used [KB]: 7036
% 14.51/3.21 % (17877)Time elapsed: 0.133 s
% 14.51/3.21 % (17877)Instructions burned: 407 (million)
% 14.51/3.21 % (17877)------------------------------
% 14.51/3.21 % (17877)------------------------------
% 14.51/3.21 % (17880)lrs+1010_1:1_au=on:cbe=off:cnfonf=conj_eager:tgt=ground:i=393:si=on:rtra=on_0 on DTF2THF_17586 for (2981ds/393Mi)
% 14.51/3.22 % (17881)lrs+1010_1:6_au=on:cnfonf=conj_eager:nwc=10.0:pe=on:prag=on:s2a=on:ss=axioms:st=1.5:i=1335:si=on:rtra=on_0 on DTF2THF_17586 for (2981ds/1335Mi)
% 14.51/3.22 % (17881)Refutation not found, incomplete strategy
% 14.51/3.22 % (17881)------------------------------
% 14.51/3.22 % (17881)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 14.51/3.22 % (17881)Termination reason: Refutation not found, incomplete strategy
% 14.51/3.22
% 14.51/3.22
% 14.51/3.22 % (17881)Memory used [KB]: 5628
% 14.51/3.22 % (17881)Time elapsed: 0.004 s
% 14.51/3.22 % (17881)Instructions burned: 7 (million)
% 14.51/3.22 % (17881)------------------------------
% 14.51/3.22 % (17881)------------------------------
% 14.51/3.23 % (17882)dis+1010_16:1_acc=model:au=on:avsq=on:cond=fast:plsq=on:plsqc=2:plsqr=9267,262144:i=3373:si=on:rtra=on_0 on DTF2THF_17586 for (2981ds/3373Mi)
% 14.51/3.25 % (17876)Instruction limit reached!
% 14.51/3.25 % (17876)------------------------------
% 14.51/3.25 % (17876)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 14.51/3.25 % (17876)Termination reason: Unknown
% 14.51/3.25 % (17876)Termination phase: Saturation
% 14.51/3.25
% 14.51/3.25 % (17876)Memory used [KB]: 7419
% 14.51/3.25 % (17876)Time elapsed: 0.180 s
% 14.51/3.25 % (17876)Instructions burned: 564 (million)
% 14.51/3.25 % (17876)------------------------------
% 14.51/3.25 % (17876)------------------------------
% 14.51/3.26 % (17883)dis+10_1:1024_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=32,1:spb=goal_then_units:i=474:si=on:rtra=on_0 on DTF2THF_17586 for (2980ds/474Mi)
% 14.51/3.26 % Exception at run slice level
% 14.51/3.26 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 14.51/3.27 % (17884)lrs+1002_1:16_amm=sco:cnfonf=lazy_pi_sigma_gen:fe=off:nm=60:piset=all_but_not_eq:plsq=on:plsqc=1:plsqr=2,1:rawr=on:sp=occurrence:ss=included:st=-1.0:i=157:si=on:rtra=on_0 on DTF2THF_17586 for (2980ds/157Mi)
% 14.51/3.27 % Exception at run slice level
% 14.51/3.27 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 14.51/3.28 % (17885)dis+1010_1:1_amm=off:cs=on:kws=precedence:nwc=10.0:piset=all:s2a=on:sac=on:sp=unary_frequency:spb=goal:ss=axioms:st=3.0:i=590:si=on:rtra=on_0 on DTF2THF_17586 for (2980ds/590Mi)
% 15.09/3.31 % (17817)Instruction limit reached!
% 15.09/3.31 % (17817)------------------------------
% 15.09/3.31 % (17817)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 15.09/3.31 % (17817)Termination reason: Unknown
% 15.09/3.31 % (17817)Termination phase: Saturation
% 15.09/3.31
% 15.09/3.31 % (17817)Memory used [KB]: 17654
% 15.09/3.31 % (17817)Time elapsed: 1.341 s
% 15.09/3.31 % (17817)Instructions burned: 4351 (million)
% 15.09/3.31 % (17817)------------------------------
% 15.09/3.31 % (17817)------------------------------
% 15.09/3.32 % (17878)Instruction limit reached!
% 15.09/3.32 % (17878)------------------------------
% 15.09/3.32 % (17878)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 15.09/3.32 % (17878)Termination reason: Unknown
% 15.09/3.32 % (17878)Termination phase: Saturation
% 15.09/3.32
% 15.09/3.32 % (17878)Memory used [KB]: 6268
% 15.09/3.32 % (17878)Time elapsed: 0.211 s
% 15.09/3.32 % (17878)Instructions burned: 582 (million)
% 15.09/3.32 % (17878)------------------------------
% 15.09/3.32 % (17878)------------------------------
% 15.09/3.32 % (17886)dis+10_1:1024_kws=precedence:prag=on:rawr=on:sos=all:sp=unary_first:i=104:si=on:rtra=on_0 on DTF2THF_17586 for (2980ds/104Mi)
% 15.09/3.33 % (17887)lrs+1010_1:10_au=on:bd=off:cnfonf=lazy_pi_sigma_gen:sp=occurrence:i=414:si=on:rtra=on_0 on DTF2THF_17586 for (2979ds/414Mi)
% 15.09/3.33 % Exception at run slice level
% 15.09/3.33 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 15.09/3.34 % (17880)Instruction limit reached!
% 15.09/3.34 % (17880)------------------------------
% 15.09/3.34 % (17880)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 15.09/3.34 % (17880)Termination reason: Unknown
% 15.09/3.34 % (17880)Termination phase: Saturation
% 15.09/3.34
% 15.09/3.34 % (17880)Memory used [KB]: 6524
% 15.09/3.34 % (17880)Time elapsed: 0.149 s
% 15.09/3.34 % (17880)Instructions burned: 393 (million)
% 15.09/3.34 % (17880)------------------------------
% 15.09/3.34 % (17880)------------------------------
% 15.09/3.34 % (17888)dis+10_1:1_av=off:bsd=on:bsr=unit_only:fd=off:hud=8:nm=16:prag=on:i=715:si=on:rtra=on_0 on DTF2THF_17586 for (2979ds/715Mi)
% 15.09/3.34 % (17879)Instruction limit reached!
% 15.09/3.34 % (17879)------------------------------
% 15.09/3.34 % (17879)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 15.09/3.34 % (17879)Termination reason: Unknown
% 15.09/3.34 % (17879)Termination phase: Saturation
% 15.09/3.34
% 15.09/3.34 % (17879)Memory used [KB]: 7291
% 15.09/3.34 % (17879)Time elapsed: 0.161 s
% 15.09/3.34 % (17879)Instructions burned: 459 (million)
% 15.09/3.34 % (17879)------------------------------
% 15.09/3.34 % (17879)------------------------------
% 15.09/3.35 % (17889)dis+21_1:5_au=on:ntd=on:nwc=5.0:s2a=on:ss=axioms:st=5.0:i=961:si=on:rtra=on_0 on DTF2THF_17586 for (2979ds/961Mi)
% 15.09/3.35 % (17890)lrs-1002_1:128_abs=on:bd=preordered:cbe=off:e2e=on:fde=unused:fe=off:tgt=full:i=1213:si=on:rtra=on_0 on DTF2THF_17586 for (2979ds/1213Mi)
% 15.09/3.35 % (17886)Instruction limit reached!
% 15.09/3.35 % (17886)------------------------------
% 15.09/3.35 % (17886)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 15.09/3.35 % (17886)Termination reason: Unknown
% 15.09/3.35 % (17886)Termination phase: Saturation
% 15.09/3.35
% 15.09/3.35 % (17886)Memory used [KB]: 6012
% 15.09/3.35 % (17886)Time elapsed: 0.034 s
% 15.09/3.35 % (17886)Instructions burned: 104 (million)
% 15.09/3.35 % (17886)------------------------------
% 15.09/3.35 % (17886)------------------------------
% 15.09/3.36 % (17891)lrs+1002_1:12_bd=off:hud=1:ntd=on:piset=equals:prag=on:i=1979:si=on:rtra=on_0 on DTF2THF_17586 for (2979ds/1979Mi)
% 15.75/3.46 % (17885)Instruction limit reached!
% 15.75/3.46 % (17885)------------------------------
% 15.75/3.46 % (17885)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 15.75/3.46 % (17885)Termination reason: Unknown
% 15.75/3.46 % (17885)Termination phase: Saturation
% 15.75/3.46
% 15.75/3.46 % (17885)Memory used [KB]: 7291
% 15.75/3.46 % (17885)Time elapsed: 0.178 s
% 15.75/3.46 % (17885)Instructions burned: 592 (million)
% 15.75/3.46 % (17885)------------------------------
% 15.75/3.46 % (17885)------------------------------
% 15.75/3.47 % (17892)dis+1002_1:1_amm=off:au=on:bsd=on:cbe=off:cnfonf=lazy_gen:sp=unary_frequency:i=481:si=on:rtra=on_0 on DTF2THF_17586 for (2978ds/481Mi)
% 15.75/3.47 % Exception at run slice level
% 15.75/3.47 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 15.75/3.48 % (17893)dis+10_8:1_apa=on:cnfonf=off:e2e=on:plsq=on:plsqc=1:plsqr=32,1:ss=axioms:i=783:si=on:rtra=on_0 on DTF2THF_17586 for (2978ds/783Mi)
% 16.04/3.55 % (17888)Instruction limit reached!
% 16.04/3.55 % (17888)------------------------------
% 16.04/3.55 % (17888)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 16.04/3.55 % (17888)Termination reason: Unknown
% 16.04/3.55 % (17888)Termination phase: Saturation
% 16.04/3.55
% 16.04/3.55 % (17888)Memory used [KB]: 3709
% 16.04/3.55 % (17888)Time elapsed: 0.215 s
% 16.04/3.55 % (17888)Instructions burned: 718 (million)
% 16.04/3.55 % (17888)------------------------------
% 16.04/3.55 % (17888)------------------------------
% 16.04/3.56 % (17894)lrs+1010_1:1_avsq=on:avsqr=1,16:kws=inv_arity:nwc=5.0:sd=1:ss=axioms:i=432:si=on:rtra=on_0 on DTF2THF_17586 for (2977ds/432Mi)
% 16.36/3.63 % (17889)Instruction limit reached!
% 16.36/3.63 % (17889)------------------------------
% 16.36/3.63 % (17889)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 16.36/3.63 % (17889)Termination reason: Unknown
% 16.36/3.63 % (17889)Termination phase: Saturation
% 16.36/3.63
% 16.36/3.63 % (17889)Memory used [KB]: 7291
% 16.36/3.63 % (17889)Time elapsed: 0.288 s
% 16.36/3.63 % (17889)Instructions burned: 964 (million)
% 16.36/3.63 % (17889)------------------------------
% 16.36/3.63 % (17889)------------------------------
% 16.36/3.64 % (17895)lrs+1010_1:1_atotf=0.5:au=on:cbe=off:cnfonf=lazy_not_be_gen:fe=off:nwc=5.0:spb=units:i=1670:si=on:rtra=on_0 on DTF2THF_17586 for (2976ds/1670Mi)
% 16.36/3.64 % Exception at run slice level
% 16.36/3.64 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 16.36/3.65 % (17896)dis+2_1:1_au=on:hfaw=0:hfsq=on:sp=weighted_frequency:i=90:si=on:rtra=on_0 on DTF2THF_17586 for (2976ds/90Mi)
% 16.36/3.69 % (17896)Instruction limit reached!
% 16.36/3.69 % (17896)------------------------------
% 16.36/3.69 % (17896)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 16.36/3.69 % (17896)Termination reason: Unknown
% 16.36/3.69 % (17896)Termination phase: Saturation
% 16.36/3.69
% 16.36/3.69 % (17896)Memory used [KB]: 5884
% 16.36/3.69 % (17896)Time elapsed: 0.033 s
% 16.36/3.69 % (17896)Instructions burned: 90 (million)
% 16.36/3.69 % (17896)------------------------------
% 16.36/3.69 % (17896)------------------------------
% 16.36/3.70 % (17897)dis+10_1:1_au=on:cnfonf=lazy_gen:ixr=off:plsq=on:plsqc=1:plsqr=32,1:i=346:si=on:rtra=on_0 on DTF2THF_17586 for (2976ds/346Mi)
% 16.36/3.70 % (17894)Instruction limit reached!
% 16.36/3.70 % (17894)------------------------------
% 16.36/3.70 % (17894)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 16.36/3.70 % (17894)Termination reason: Unknown
% 16.36/3.70 % (17894)Termination phase: Saturation
% 16.36/3.70
% 16.36/3.70 % (17894)Memory used [KB]: 7291
% 16.36/3.70 % (17894)Time elapsed: 0.136 s
% 16.36/3.70 % (17894)Instructions burned: 434 (million)
% 16.36/3.70 % (17894)------------------------------
% 16.36/3.70 % (17894)------------------------------
% 16.82/3.70 % Exception at run slice level
% 16.82/3.70 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 16.82/3.71 % (17899)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=6454:si=on:rtra=on_0 on DTF2THF_17586 for (2976ds/6454Mi)
% 16.82/3.71 % (17898)dis+1002_1:1_cnfonf=lazy_not_gen:hud=10:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=401:si=on:rtra=on_0 on DTF2THF_17586 for (2976ds/401Mi)
% 16.82/3.71 % Exception at run slice level
% 16.82/3.71 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 16.82/3.71 % (17893)Instruction limit reached!
% 16.82/3.71 % (17893)------------------------------
% 16.82/3.71 % (17893)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 16.82/3.71 % (17893)Termination reason: Unknown
% 16.82/3.71 % (17893)Termination phase: Saturation
% 16.82/3.71
% 16.82/3.71 % (17893)Memory used [KB]: 8443
% 16.82/3.71 % (17893)Time elapsed: 0.238 s
% 16.82/3.71 % (17893)Instructions burned: 785 (million)
% 16.82/3.71 % (17893)------------------------------
% 16.82/3.71 % (17893)------------------------------
% 16.82/3.72 % (17890)Instruction limit reached!
% 16.82/3.72 % (17890)------------------------------
% 16.82/3.72 % (17890)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 16.82/3.72 % (17890)Termination reason: Unknown
% 16.82/3.72 % (17890)Termination phase: Saturation
% 16.82/3.72
% 16.82/3.72 % (17890)Memory used [KB]: 7803
% 16.82/3.72 % (17890)Time elapsed: 0.376 s
% 16.82/3.72 % (17890)Instructions burned: 1214 (million)
% 16.82/3.72 % (17890)------------------------------
% 16.82/3.72 % (17890)------------------------------
% 16.82/3.72 % (17903)dis+1010_1:1_avsq=on:fe=off:fsr=off:hud=10:kws=arity:prag=on:i=283:si=on:rtra=on_0 on DTF2THF_17586 for (2976ds/283Mi)
% 16.82/3.72 % (17904)ott+10_1:1_aac=none:apa=on:au=on:cnfonf=off:ntd=on:nwc=12.0:sos=on:i=865:si=on:rtra=on_0 on DTF2THF_17586 for (2976ds/865Mi)
% 16.82/3.73 % (17905)lrs+1002_3:4_au=on:av=off:cnfonf=off:fd=off:fsr=off:ins=2:sd=1:sos=on:ss=axioms:i=4528:si=on:rtra=on_0 on DTF2THF_17586 for (2975ds/4528Mi)
% 16.82/3.74 % (17905)Refutation not found, incomplete strategy
% 16.82/3.74 % (17905)------------------------------
% 16.82/3.74 % (17905)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 16.82/3.74 % (17905)Termination reason: Refutation not found, incomplete strategy
% 16.82/3.74
% 16.82/3.74
% 16.82/3.74 % (17905)Memory used [KB]: 1023
% 16.82/3.74 % (17905)Time elapsed: 0.003 s
% 16.82/3.74 % (17905)Instructions burned: 2 (million)
% 16.82/3.74 % (17905)------------------------------
% 16.82/3.74 % (17905)------------------------------
% 16.82/3.75 % (17920)dis+1002_1:1_cbe=off:hud=5:nm=4:plsq=on:plsqr=7,1:prag=on:sp=const_max:tnu=1:i=1001:si=on:rtra=on_0 on DTF2THF_17586 for (2975ds/1001Mi)
% 17.72/3.81 % (17903)Instruction limit reached!
% 17.72/3.81 % (17903)------------------------------
% 17.72/3.81 % (17903)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 17.72/3.81 % (17903)Termination reason: Unknown
% 17.72/3.81 % (17903)Termination phase: Saturation
% 17.72/3.81
% 17.72/3.81 % (17903)Memory used [KB]: 6524
% 17.72/3.81 % (17903)Time elapsed: 0.088 s
% 17.72/3.81 % (17903)Instructions burned: 284 (million)
% 17.72/3.81 % (17903)------------------------------
% 17.72/3.81 % (17903)------------------------------
% 17.72/3.82 % (17921)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=102:si=on:rtra=on_0 on DTF2THF_17586 for (2975ds/102Mi)
% 17.72/3.85 % (17921)Instruction limit reached!
% 17.72/3.85 % (17921)------------------------------
% 17.72/3.85 % (17921)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 17.72/3.85 % (17921)Termination reason: Unknown
% 17.72/3.85 % (17921)Termination phase: Saturation
% 17.72/3.85
% 17.72/3.85 % (17921)Memory used [KB]: 5884
% 17.72/3.85 % (17921)Time elapsed: 0.036 s
% 17.72/3.85 % (17921)Instructions burned: 103 (million)
% 17.72/3.85 % (17921)------------------------------
% 17.72/3.85 % (17921)------------------------------
% 17.72/3.86 % (17922)ott+1010_3:1_nm=20:s2a=on:s2at=3.0:sp=const_frequency:i=952:si=on:rtra=on_0 on DTF2THF_17586 for (2974ds/952Mi)
% 17.97/3.97 % (17891)Instruction limit reached!
% 17.97/3.97 % (17891)------------------------------
% 17.97/3.97 % (17891)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 17.97/3.97 % (17891)Termination reason: Unknown
% 17.97/3.97 % (17891)Termination phase: Saturation
% 17.97/3.97
% 17.97/3.97 % (17891)Memory used [KB]: 9210
% 17.97/3.97 % (17891)Time elapsed: 0.611 s
% 17.97/3.97 % (17891)Instructions burned: 1980 (million)
% 17.97/3.97 % (17891)------------------------------
% 17.97/3.97 % (17891)------------------------------
% 17.97/3.98 % (17904)Instruction limit reached!
% 17.97/3.98 % (17904)------------------------------
% 17.97/3.98 % (17904)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 17.97/3.98 % (17904)Termination reason: Unknown
% 17.97/3.98 % (17904)Termination phase: Saturation
% 17.97/3.98
% 17.97/3.98 % (17904)Memory used [KB]: 6908
% 17.97/3.98 % (17904)Time elapsed: 0.253 s
% 17.97/3.98 % (17904)Instructions burned: 867 (million)
% 17.97/3.98 % (17904)------------------------------
% 17.97/3.98 % (17904)------------------------------
% 17.97/3.98 % (17923)lrs+1010_1:1024_add=large:c=on:cbe=off:cnfonf=lazy_gen:fde=none:nm=30:piset=and:sac=on:uhcvi=on:i=578:si=on:rtra=on_0 on DTF2THF_17586 for (2973ds/578Mi)
% 17.97/3.98 % Exception at run slice level
% 17.97/3.98 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 17.97/3.99 % (17924)dis+1010_1:4_avsq=on:avsqr=16,1:bet=on:cbe=off:cnfonf=lazy_not_be_gen:hud=5:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=643:si=on:rtra=on_0 on DTF2THF_17586 for (2973ds/643Mi)
% 17.97/3.99 % Exception at run slice level
% 17.97/3.99 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 17.97/3.99 % (17925)lrs+1010_1:1_cnfonf=off:ntd=on:nwc=3.0:s2a=on:sp=const_frequency:i=865:si=on:rtra=on_0 on DTF2THF_17586 for (2973ds/865Mi)
% 17.97/4.00 % (17926)lrs+10_1:1_au=on:erd=off:s2a=on:s2at=3.0:sos=all:i=1174:si=on:rtra=on_0 on DTF2THF_17586 for (2973ds/1174Mi)
% 20.52/4.05 % (17920)Instruction limit reached!
% 20.52/4.05 % (17920)------------------------------
% 20.52/4.05 % (17920)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 20.52/4.05 % (17920)Termination reason: Unknown
% 20.52/4.05 % (17920)Termination phase: Saturation
% 20.52/4.05
% 20.52/4.05 % (17920)Memory used [KB]: 9466
% 20.52/4.05 % (17920)Time elapsed: 0.308 s
% 20.52/4.05 % (17920)Instructions burned: 1002 (million)
% 20.52/4.05 % (17920)------------------------------
% 20.52/4.05 % (17920)------------------------------
% 20.52/4.06 % (17927)ott+1010_1:32_apa=on:atotf=0.3:au=on:c=on:cnfonf=off:fe=off:fsr=off:nm=6:piset=or:sac=on:sos=on:i=644:si=on:rtra=on_0 on DTF2THF_17586 for (2972ds/644Mi)
% 20.52/4.07 % (17927)Refutation not found, incomplete strategy
% 20.52/4.07 % (17927)------------------------------
% 20.52/4.07 % (17927)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 20.52/4.07 % (17927)Termination reason: Refutation not found, incomplete strategy
% 20.52/4.07
% 20.52/4.07
% 20.52/4.07 % (17927)Memory used [KB]: 5628
% 20.52/4.07 % (17927)Time elapsed: 0.004 s
% 20.52/4.07 % (17927)Instructions burned: 7 (million)
% 20.52/4.07 % (17927)------------------------------
% 20.52/4.07 % (17927)------------------------------
% 20.52/4.08 % (17928)lrs+10_1:1_alpa=true:au=on:cs=on:tgt=ground:i=1201:si=on:rtra=on_0 on DTF2THF_17586 for (2972ds/1201Mi)
% 21.18/4.19 % (17922)Instruction limit reached!
% 21.18/4.19 % (17922)------------------------------
% 21.18/4.19 % (17922)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 21.18/4.19 % (17922)Termination reason: Unknown
% 21.18/4.19 % (17922)Termination phase: Saturation
% 21.18/4.19
% 21.18/4.19 % (17922)Memory used [KB]: 8827
% 21.18/4.19 % (17922)Time elapsed: 0.325 s
% 21.18/4.19 % (17922)Instructions burned: 954 (million)
% 21.18/4.19 % (17922)------------------------------
% 21.18/4.19 % (17922)------------------------------
% 21.69/4.20 % (17929)lrs+1666_1:64_cnfonf=lazy_simp:hud=5:plsq=on:plsql=on:plsqr=152565,524288:tnu=2:i=1046:si=on:rtra=on_0 on DTF2THF_17586 for (2971ds/1046Mi)
% 21.69/4.20 % Exception at run slice level
% 21.69/4.20 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 21.69/4.22 % (17930)lrs+1010_1:1_c=on:cnfonf=lazy_simp:fsr=off:hud=5:kws=arity:nm=32:plsq=on:plsqc=1:plsqr=642,29:prag=on:i=222:si=on:rtra=on_0 on DTF2THF_17586 for (2971ds/222Mi)
% 21.69/4.22 % Exception at run slice level
% 21.69/4.22 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 21.69/4.23 % (17931)ott+1010_1:4_cbe=off:chr=on:hfsq=on:hfsqr=1,16:hud=3:sac=on:sp=unary_frequency:ss=axioms:st=5.0:tnu=2:i=68:si=on:rtra=on_0 on DTF2THF_17586 for (2971ds/68Mi)
% 21.69/4.26 % (17931)Instruction limit reached!
% 21.69/4.26 % (17931)------------------------------
% 21.69/4.26 % (17931)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 21.69/4.26 % (17931)Termination reason: Unknown
% 21.69/4.26 % (17931)Termination phase: Saturation
% 21.69/4.26
% 21.69/4.26 % (17931)Memory used [KB]: 6012
% 21.69/4.26 % (17931)Time elapsed: 0.046 s
% 21.69/4.26 % (17931)Instructions burned: 70 (million)
% 21.69/4.26 % (17931)------------------------------
% 21.69/4.26 % (17931)------------------------------
% 21.69/4.26 % (17925)Instruction limit reached!
% 21.69/4.26 % (17925)------------------------------
% 21.69/4.26 % (17925)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 21.69/4.26 % (17925)Termination reason: Unknown
% 21.69/4.26 % (17925)Termination phase: Saturation
% 21.69/4.26
% 21.69/4.26 % (17925)Memory used [KB]: 9083
% 21.69/4.26 % (17925)Time elapsed: 0.271 s
% 21.69/4.26 % (17925)Instructions burned: 866 (million)
% 21.69/4.26 % (17925)------------------------------
% 21.69/4.26 % (17925)------------------------------
% 21.69/4.27 % (17932)lrs+1010_1:1_chr=on:cnfonf=lazy_not_be_gen:gs=on:hud=5:plsq=on:plsqc=1:plsqr=5,1:prag=on:rawr=on:i=454:si=on:rtra=on_0 on DTF2THF_17586 for (2970ds/454Mi)
% 21.69/4.27 % Exception at run slice level
% 21.69/4.27 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 21.69/4.27 % (17933)dis+1002_1:1_cnfonf=lazy_simp:hud=5:plsq=on:plsqc=1:plsqr=32,1:prag=on:i=360:si=on:rtra=on_0 on DTF2THF_17586 for (2970ds/360Mi)
% 21.69/4.27 % Exception at run slice level
% 21.69/4.27 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 21.69/4.28 % (17934)lrs+1002_1:16_amm=sco:cnfonf=lazy_pi_sigma_gen:fe=off:nm=60:piset=all_but_not_eq:plsq=on:plsqc=1:plsqr=2,1:rawr=on:sp=occurrence:ss=included:st=-1.0:i=157:si=on:rtra=on_0 on DTF2THF_17586 for (2970ds/157Mi)
% 21.69/4.28 % Exception at run slice level
% 21.69/4.28 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 21.69/4.28 % (17935)ott+1004_1:24_anc=none:cbe=off:cnfonf=lazy_not_gen:fe=off:piset=not:prag=on:rp=on:i=5061:si=on:rtra=on_0 on DTF2THF_17586 for (2970ds/5061Mi)
% 21.69/4.28 % Exception at run slice level
% 21.69/4.28 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 21.69/4.29 % (17936)lrs+1002_1:8_av=off:fd=off:hud=5:tnu=1:i=2401:si=on:rtra=on_0 on DTF2THF_17586 for (2970ds/2401Mi)
% 21.69/4.29 % (17882)Instruction limit reached!
% 21.69/4.29 % (17882)------------------------------
% 21.69/4.29 % (17882)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 21.69/4.29 % (17882)Termination reason: Unknown
% 21.69/4.29 % (17882)Termination phase: Saturation
% 21.69/4.29
% 21.69/4.29 % (17882)Memory used [KB]: 10362
% 21.69/4.29 % (17882)Time elapsed: 1.084 s
% 21.69/4.29 % (17882)Instructions burned: 3374 (million)
% 21.69/4.29 % (17882)------------------------------
% 21.69/4.29 % (17882)------------------------------
% 21.69/4.29 % (17937)dis+10_1:1_av=off:e2e=on:nm=4:s2a=on:i=5798:si=on:rtra=on_0 on DTF2THF_17586 for (2970ds/5798Mi)
% 22.28/4.30 % (17938)dis+10_1:1_au=on:cnfonf=lazy_gen:ixr=off:plsq=on:plsqc=1:plsqr=32,1:i=346:si=on:rtra=on_0 on DTF2THF_17586 for (2970ds/346Mi)
% 22.28/4.30 % Exception at run slice level
% 22.28/4.30 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 22.28/4.31 % (17939)lrs+1002_1:1_av=off:bd=off:bet=on:e2e=on:fde=unused:fe=off:plsq=on:prag=on:sos=on:i=1321:si=on:rtra=on_0 on DTF2THF_17586 for (2970ds/1321Mi)
% 22.28/4.32 % (17939)Refutation not found, incomplete strategy
% 22.28/4.32 % (17939)------------------------------
% 22.28/4.32 % (17939)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 22.28/4.32 % (17939)Termination reason: Refutation not found, incomplete strategy
% 22.28/4.32
% 22.28/4.32
% 22.28/4.32 % (17939)Memory used [KB]: 1151
% 22.28/4.32 % (17939)Time elapsed: 0.003 s
% 22.28/4.32 % (17939)Instructions burned: 4 (million)
% 22.28/4.32 % (17939)------------------------------
% 22.28/4.32 % (17939)------------------------------
% 22.28/4.33 % (17940)lrs+10_1:1_cnfonf=lazy_gen:kws=inv_precedence:nwc=10.0:i=1312:si=on:rtra=on_0 on DTF2THF_17586 for (2969ds/1312Mi)
% 22.28/4.33 % Exception at run slice level
% 22.28/4.33 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 22.28/4.34 % (17941)ott+2_8:1_add=large:c=on:cnfonf=off:e2e=on:er=filter:hud=5:plsq=on:plsqr=1,1:ss=axioms:i=672:si=on:rtra=on_0 on DTF2THF_17586 for (2969ds/672Mi)
% 22.28/4.34 % (17926)Instruction limit reached!
% 22.28/4.34 % (17926)------------------------------
% 22.28/4.34 % (17926)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 22.28/4.34 % (17926)Termination reason: Unknown
% 22.28/4.34 % (17926)Termination phase: Saturation
% 22.28/4.34
% 22.28/4.34 % (17926)Memory used [KB]: 8955
% 22.28/4.34 % (17926)Time elapsed: 0.346 s
% 22.28/4.34 % (17926)Instructions burned: 1174 (million)
% 22.28/4.34 % (17926)------------------------------
% 22.28/4.34 % (17926)------------------------------
% 22.28/4.35 % (17942)dis+10_1:1_au=on:c=on:e2e=on:fsr=off:sos=all:sp=const_frequency:ss=axioms:i=1897:si=on:rtra=on_0 on DTF2THF_17586 for (2969ds/1897Mi)
% 22.28/4.35 % (17942)Refutation not found, incomplete strategy
% 22.28/4.35 % (17942)------------------------------
% 22.28/4.35 % (17942)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 22.28/4.35 % (17942)Termination reason: Refutation not found, incomplete strategy
% 22.28/4.35
% 22.28/4.35
% 22.28/4.35 % (17942)Memory used [KB]: 5500
% 22.28/4.35 % (17942)Time elapsed: 0.003 s
% 22.28/4.35 % (17942)Instructions burned: 3 (million)
% 22.28/4.35 % (17942)------------------------------
% 22.28/4.35 % (17942)------------------------------
% 22.28/4.36 % (17943)lrs+10_1:40_av=off:fde=unused:ntd=on:plsq=on:plsqc=2:plsqr=411915,1048576:sp=unary_frequency:tgt=full:i=1202:si=on:rtra=on_0 on DTF2THF_17586 for (2969ds/1202Mi)
% 22.57/4.46 % (17928)Instruction limit reached!
% 22.57/4.46 % (17928)------------------------------
% 22.57/4.46 % (17928)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 22.57/4.46 % (17928)Termination reason: Unknown
% 22.57/4.46 % (17928)Termination phase: Saturation
% 22.57/4.46
% 22.57/4.46 % (17928)Memory used [KB]: 7803
% 22.57/4.46 % (17928)Time elapsed: 0.383 s
% 22.57/4.46 % (17928)Instructions burned: 1201 (million)
% 22.57/4.46 % (17928)------------------------------
% 22.57/4.46 % (17928)------------------------------
% 22.57/4.47 % (17944)dis+21_1:1_au=on:cnfonf=lazy_pi_sigma_gen:hfsq=on:hfsqc=40:hfsqr=8,1:ntd=on:sos=on:sp=occurrence:ss=axioms:i=1493:si=on:rtra=on_0 on DTF2THF_17586 for (2968ds/1493Mi)
% 22.57/4.47 % Exception at run slice level
% 22.57/4.47 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 22.57/4.48 % (17945)dis+1010_3:1_av=off:fde=unused:hud=10:nwc=10.0:s2a=on:ss=axioms:i=7679:si=on:rtra=on_0 on DTF2THF_17586 for (2968ds/7679Mi)
% 23.17/4.54 % (17941)Instruction limit reached!
% 23.17/4.54 % (17941)------------------------------
% 23.17/4.54 % (17941)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 23.17/4.54 % (17941)Termination reason: Unknown
% 23.17/4.54 % (17941)Termination phase: Saturation
% 23.17/4.54
% 23.17/4.54 % (17941)Memory used [KB]: 8443
% 23.17/4.54 % (17941)Time elapsed: 0.207 s
% 23.17/4.54 % (17941)Instructions burned: 672 (million)
% 23.17/4.54 % (17941)------------------------------
% 23.17/4.54 % (17941)------------------------------
% 23.17/4.55 % (17946)lrs+2_1:1024_anc=all:cnfonf=off:cs=on:e2e=on:nm=20:s2at=1.5:slsq=on:slsqr=1,2:spb=goal:i=340:si=on:rtra=on_0 on DTF2THF_17586 for (2967ds/340Mi)
% 23.59/4.66 % (17946)Instruction limit reached!
% 23.59/4.66 % (17946)------------------------------
% 23.59/4.66 % (17946)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 23.59/4.66 % (17946)Termination reason: Unknown
% 23.59/4.66 % (17946)Termination phase: Saturation
% 23.59/4.66
% 23.59/4.66 % (17946)Memory used [KB]: 7036
% 23.59/4.66 % (17946)Time elapsed: 0.111 s
% 23.59/4.66 % (17946)Instructions burned: 340 (million)
% 23.59/4.66 % (17946)------------------------------
% 23.59/4.66 % (17946)------------------------------
% 23.59/4.67 % (17947)dis+1002_1:1_acc=model:au=on:nwc=5.0:sd=5:ss=axioms:st=2.5:i=3672:si=on:rtra=on_0 on DTF2THF_17586 for (2966ds/3672Mi)
% 23.92/4.72 % (17943)Instruction limit reached!
% 23.92/4.72 % (17943)------------------------------
% 23.92/4.72 % (17943)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 23.92/4.72 % (17943)Termination reason: Unknown
% 23.92/4.72 % (17943)Termination phase: Saturation
% 23.92/4.72
% 23.92/4.72 % (17943)Memory used [KB]: 2302
% 23.92/4.72 % (17943)Time elapsed: 0.363 s
% 23.92/4.72 % (17943)Instructions burned: 1205 (million)
% 23.92/4.72 % (17943)------------------------------
% 23.92/4.72 % (17943)------------------------------
% 23.92/4.73 % (17948)dis-1002_3:1_acc=model:bd=off:bsd=on:bsdmm=1:cnfonf=lazy_not_be_gen:fd=off:fe=off:ntd=on:nwc=10.0:piset=equals:plsq=on:plsqc=1:plsqr=32,1:sp=const_max:uhcvi=on:i=1535:si=on:rtra=on_0 on DTF2THF_17586 for (2965ds/1535Mi)
% 23.92/4.74 % Exception at run slice level
% 23.92/4.74 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 23.92/4.75 % (17949)dis+10_16:1_hud=1:plsq=on:plsqc=1:plsqr=32,1:prag=on:sd=1:sgt=64:ss=axioms:i=4637:si=on:rtra=on_0 on DTF2THF_17586 for (2965ds/4637Mi)
% 24.50/4.80 % (17838)Instruction limit reached!
% 24.50/4.80 % (17838)------------------------------
% 24.50/4.80 % (17838)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 24.50/4.80 % (17838)Termination reason: Unknown
% 24.50/4.80 % (17838)Termination phase: Saturation
% 24.50/4.80
% 24.50/4.80 % (17838)Memory used [KB]: 17398
% 24.50/4.80 % (17838)Time elapsed: 2.439 s
% 24.50/4.80 % (17838)Instructions burned: 8252 (million)
% 24.50/4.80 % (17838)------------------------------
% 24.50/4.80 % (17838)------------------------------
% 24.50/4.81 % (17967)lrs+10_1:1_fde=unused:prag=on:sd=2:sgt=32:ss=axioms:i=3174:si=on:rtra=on_0 on DTF2THF_17586 for (2965ds/3174Mi)
% 27.50/5.02 % (17936)Instruction limit reached!
% 27.50/5.02 % (17936)------------------------------
% 27.50/5.02 % (17936)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 27.50/5.02 % (17936)Termination reason: Unknown
% 27.50/5.02 % (17936)Termination phase: Saturation
% 27.50/5.02
% 27.50/5.02 % (17936)Memory used [KB]: 12153
% 27.50/5.02 % (17936)Time elapsed: 0.733 s
% 27.50/5.02 % (17936)Instructions burned: 2403 (million)
% 27.50/5.02 % (17936)------------------------------
% 27.50/5.02 % (17936)------------------------------
% 27.50/5.03 % (17968)lrs+1010_1:10_au=on:bd=off:cnfonf=lazy_pi_sigma_gen:sp=occurrence:i=307:si=on:rtra=on_0 on DTF2THF_17586 for (2962ds/307Mi)
% 27.50/5.03 % Exception at run slice level
% 27.50/5.03 User error: Vampire does not support full TH1. This benchmark is either outside of the TH1 fragment, or outside of the fragment supported by Vampire
% 27.50/5.04 % (17969)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=3619:si=on:rtra=on_0 on DTF2THF_17586 for (2962ds/3619Mi)
% 27.50/5.04 % (17969)Refutation not found, incomplete strategy
% 27.50/5.04 % (17969)------------------------------
% 27.50/5.04 % (17969)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 27.50/5.04 % (17969)Termination reason: Refutation not found, incomplete strategy
% 27.50/5.04
% 27.50/5.04
% 27.50/5.04 % (17969)Memory used [KB]: 5500
% 27.50/5.04 % (17969)Time elapsed: 0.003 s
% 27.50/5.04 % (17969)Instructions burned: 4 (million)
% 27.50/5.04 % (17969)------------------------------
% 27.50/5.04 % (17969)------------------------------
% 27.50/5.05 % (17970)lrs+1002_1:1_au=on:cbe=off:fde=none:ins=1:sp=const_max:i=2325:si=on:rtra=on_0 on DTF2THF_17586 for (2962ds/2325Mi)
% 31.02/5.64 % (17899)Instruction limit reached!
% 31.02/5.64 % (17899)------------------------------
% 31.02/5.64 % (17899)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 31.02/5.64 % (17899)Termination reason: Unknown
% 31.02/5.64 % (17899)Termination phase: Saturation
% 31.02/5.64
% 31.02/5.64 % (17899)Memory used [KB]: 21492
% 31.02/5.64 % (17899)Time elapsed: 1.940 s
% 31.02/5.64 % (17899)Instructions burned: 6454 (million)
% 31.02/5.64 % (17899)------------------------------
% 31.02/5.64 % (17899)------------------------------
% 31.02/5.66 % (17971)dis+1002_1:1_au=on:sac=on:sd=5:slsq=on:slsqr=1,4:ss=axioms:st=2.0:i=2341:si=on:rtra=on_0 on DTF2THF_17586 for (2956ds/2341Mi)
% 31.59/5.75 % (17947)Instruction limit reached!
% 31.59/5.75 % (17947)------------------------------
% 31.59/5.75 % (17947)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 31.59/5.75 % (17947)Termination reason: Unknown
% 31.59/5.75 % (17947)Termination phase: Saturation
% 31.59/5.75
% 31.59/5.75 % (17947)Memory used [KB]: 11641
% 31.59/5.75 % (17947)Time elapsed: 1.084 s
% 31.59/5.75 % (17947)Instructions burned: 3673 (million)
% 31.59/5.75 % (17947)------------------------------
% 31.59/5.75 % (17947)------------------------------
% 31.59/5.76 % (17972)lrs+1010_1:16_apa=on:bsd=on:cnfonf=off:hud=10:sac=on:sos=on:ss=axioms:i=7257:si=on:rtra=on_0 on DTF2THF_17586 for (2955ds/7257Mi)
% 31.59/5.79 % (17970)Instruction limit reached!
% 31.59/5.79 % (17970)------------------------------
% 31.59/5.79 % (17970)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 31.59/5.79 % (17970)Termination reason: Unknown
% 31.59/5.79 % (17970)Termination phase: Saturation
% 31.59/5.79
% 31.59/5.79 % (17970)Memory used [KB]: 12537
% 31.59/5.79 % (17970)Time elapsed: 0.736 s
% 31.59/5.79 % (17970)Instructions burned: 2326 (million)
% 31.59/5.79 % (17970)------------------------------
% 31.59/5.79 % (17970)------------------------------
% 31.59/5.79 % (17972)First to succeed.
% 31.59/5.79 % (17972)Refutation found. Thanks to Tanya!
% 31.59/5.79 % SZS status Theorem for DTF2THF_17586
% 31.59/5.79 % SZS output start Proof for DTF2THF_17586
% 31.59/5.79 thf(type_def_6, type, tyop_2Epair_2Eprod: ($tType * $tType) > $tType).
% 31.59/5.79 thf(type_def_7, type, tyop_2Ewellorder_2Ewellorder: ($tType) > $tType).
% 31.59/5.79 thf(type_def_8, type, sK2: $tType).
% 31.59/5.79 thf(func_def_0, type, tyop_2Emin_2Ebool: $tType).
% 31.59/5.79 thf(func_def_1, type, tyop_2Emin_2Efun: ($tType * $tType) > $tType).
% 31.59/5.79 thf(func_def_2, type, tyop_2Epair_2Eprod: ($tType * $tType) > $tType).
% 31.59/5.79 thf(func_def_3, type, tyop_2Ewellorder_2Ewellorder: ($tType) > $tType).
% 31.59/5.79 thf(func_def_4, type, c_2Ebool_2E_21: !>[X0: $tType]:((X0 > $o) > $o)).
% 31.59/5.79 thf(func_def_5, type, c_2Epair_2E_2C: !>[X0: $tType, X1: $tType]:(X0 > X1 > tyop_2Epair_2Eprod @ X0 @ X1)).
% 31.59/5.79 thf(func_def_6, type, c_2Ebool_2E_2F_5C: $o > $o > $o).
% 31.59/5.79 thf(func_def_7, type, c_2Emin_2E_3D: !>[X0: $tType]:(X0 > X0 > $o)).
% 31.59/5.79 thf(func_def_8, type, c_2Emin_2E_3D_3D_3E: $o > $o > $o).
% 31.59/5.79 thf(func_def_9, type, c_2Ebool_2E_3F: !>[X0: $tType]:((X0 > $o) > $o)).
% 31.59/5.79 thf(func_def_10, type, c_2Epair_2ECURRY: !>[X0: $tType, X1: $tType, X2: $tType]:((tyop_2Epair_2Eprod @ X0 @ X1 > X2) > X0 > X1 > X2)).
% 31.59/5.79 thf(func_def_11, type, c_2Ebool_2EIN: !>[X0: $tType]:(X0 > (X0 > $o) > $o)).
% 31.59/5.79 thf(func_def_12, type, c_2Erelation_2EWF: !>[X0: $tType]:((X0 > X0 > $o) > $o)).
% 31.59/5.79 thf(func_def_13, type, c_2Ebool_2E_5C_2F: $o > $o > $o).
% 31.59/5.79 thf(func_def_14, type, c_2Eset__relation_2Estrict: !>[X0: $tType]:((tyop_2Epair_2Eprod @ X0 @ X0 > $o) > tyop_2Epair_2Eprod @ X0 @ X0 > $o)).
% 31.59/5.79 thf(func_def_15, type, c_2Ewellorder_2Ewellfounded: !>[X0: $tType]:((tyop_2Epair_2Eprod @ X0 @ X0 > $o) > $o)).
% 31.59/5.79 thf(func_def_16, type, c_2Ewellorder_2Ewellorder__REP: !>[X0: $tType]:(tyop_2Ewellorder_2Ewellorder @ X0 > tyop_2Epair_2Eprod @ X0 @ X0 > $o)).
% 31.59/5.79 thf(func_def_17, type, c_2Ebool_2E_7E: $o > $o).
% 31.59/5.79 thf(func_def_25, type, sK0: !>[X0: $tType]:((X0 > $o) > X0)).
% 31.59/5.79 thf(func_def_26, type, sK1: !>[X0: $tType]:((X0 > $o) > X0)).
% 31.59/5.79 thf(func_def_33, type, sK3: tyop_2Ewellorder_2Ewellorder @ sK2).
% 31.59/5.79 thf(func_def_35, type, ph5: !>[X0: $tType]:(X0)).
% 31.59/5.79 thf(func_def_40, type, sK6: (tyop_2Epair_2Eprod @ sK2 @ sK2 > $o) > sK2).
% 31.59/5.79 thf(func_def_41, type, sK7: (tyop_2Epair_2Eprod @ sK2 @ sK2 > $o) > sK2).
% 31.59/5.79 thf(f107,plain,(
% 31.59/5.79 $false),
% 31.59/5.79 inference(subsumption_resolution,[status(thm)],[f105,f62])).
% 31.59/5.79 thf(f62,plain,(
% 31.59/5.79 ( ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (((c_2Ewellorder_2Ewellfounded @ X0 @ (^[Y0 : tyop_2Epair_2Eprod @ X0 @ X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ Y0 @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))) = $true)) )),
% 31.59/5.79 inference(cnf_transformation,[status(thm)],[f36])).
% 31.59/5.79 thf(f36,plain,(
% 31.59/5.79 ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : ((c_2Ewellorder_2Ewellfounded @ X0 @ (^[Y0 : tyop_2Epair_2Eprod @ X0 @ X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ Y0 @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))) = $true)),
% 31.59/5.79 inference(fool_elimination,[status(thm)],[f35])).
% 31.59/5.79 thf(f35,plain,(
% 31.59/5.79 ! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Ewellorder_2Ewellfounded @ X0 @ (^[X2 : tyop_2Epair_2Eprod @ X0 @ X0] : (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ X2 @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1)))))),
% 31.59/5.79 inference(rectify,[status(thm)],[f11])).
% 31.59/5.79 thf(f11,axiom,(
% 31.59/5.79 ! [X0 : $tType,X10 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Ewellorder_2Ewellfounded @ X0 @ (^[X11 : tyop_2Epair_2Eprod @ X0 @ X0] : (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ X11 @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X10)))))),
% 31.59/5.79 file('/export/starexec/sandbox/tmp/tmp.HpJsg7gn6n/DTF2THF_17586.p',thm_2Ewellorder_2EWIN__WF)).
% 31.59/5.79 thf(f105,plain,(
% 31.59/5.79 ((c_2Ewellorder_2Ewellfounded @ sK2 @ (^[Y0 : tyop_2Epair_2Eprod @ sK2 @ sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ Y0 @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3))))) != $true)),
% 31.59/5.79 inference(beta_eta_normalization,[status(thm)],[f99])).
% 31.59/5.79 thf(f99,plain,(
% 31.59/5.79 ((c_2Ewellorder_2Ewellfounded @ sK2 @ (^[Y0 : tyop_2Epair_2Eprod @ sK2 @ sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ ((^[Y1 : tyop_2Epair_2Eprod @ sK2 @ sK2]: (Y1)) @ Y0) @ ((^[Y1 : tyop_2Epair_2Eprod @ sK2 @ sK2]: ((^[Y2 : tyop_2Epair_2Eprod @ sK2 @ sK2]: (c_2Eset__relation_2Estrict @ sK2 @ ((^[Y3 : tyop_2Epair_2Eprod @ sK2 @ sK2]: ((^[Y4 : tyop_2Epair_2Eprod @ sK2 @ sK2]: ((^[Y5 : tyop_2Epair_2Eprod @ sK2 @ sK2]: (c_2Ewellorder_2Ewellorder__REP @ sK2 @ ((^[Y6 : tyop_2Epair_2Eprod @ sK2 @ sK2]: ((^[Y7 : tyop_2Epair_2Eprod @ sK2 @ sK2]: ((^[Y8 : tyop_2Epair_2Eprod @ sK2 @ sK2]: (sK3)))))) @ Y3 @ Y4 @ Y5) @ ((^[Y6 : tyop_2Epair_2Eprod @ sK2 @ sK2]: ((^[Y7 : tyop_2Epair_2Eprod @ sK2 @ sK2]: ((^[Y8 : tyop_2Epair_2Eprod @ sK2 @ sK2]: (Y8)))))) @ Y3 @ Y4 @ Y5))))))) @ Y1 @ Y2) @ ((^[Y3 : tyop_2Epair_2Eprod @ sK2 @ sK2]: ((^[Y4 : tyop_2Epair_2Eprod @ sK2 @ sK2]: (Y4)))) @ Y1 @ Y2))))) @ Y0)))) != $true)),
% 31.59/5.79 inference(equality_resolution,[status(thm)],[f83])).
% 31.59/5.79 thf(f83,plain,(
% 31.59/5.79 ( ! [X0 : tyop_2Epair_2Eprod @ sK2 @ sK2 > $o] : (((X0 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ (sK6 @ X0) @ (sK7 @ X0))) != (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ (sK6 @ X0) @ (sK7 @ X0)) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3)))) | ((c_2Ewellorder_2Ewellfounded @ sK2 @ X0) != $true)) )),
% 31.59/5.79 inference(superposition,[status(thm)],[f81,f59])).
% 31.59/5.79 thf(f59,plain,(
% 31.59/5.79 ( ! [X1 : $tType,X0 : $tType,X2 : $tType,X3 : tyop_2Epair_2Eprod @ X0 @ X1 > X2,X4 : X0,X5 : X1] : (((c_2Epair_2ECURRY @ X0 @ X1 @ X2 @ X3 @ X4 @ X5) = (X3 @ (c_2Epair_2E_2C @ X0 @ X1 @ X4 @ X5)))) )),
% 31.59/5.79 inference(cnf_transformation,[status(thm)],[f34])).
% 31.59/5.79 thf(f34,plain,(
% 31.59/5.79 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : tyop_2Epair_2Eprod @ X0 @ X1 > X2,X4 : X0,X5 : X1] : ((c_2Epair_2ECURRY @ X0 @ X1 @ X2 @ X3 @ X4 @ X5) = (X3 @ (c_2Epair_2E_2C @ X0 @ X1 @ X4 @ X5)))),
% 31.59/5.79 inference(fool_elimination,[status(thm)],[f33])).
% 31.59/5.79 thf(f33,plain,(
% 31.59/5.79 ! [X0 : $tType,X1 : $tType,X2 : $tType,X3 : tyop_2Epair_2Eprod @ X0 @ X1 > X2,X4 : X0,X5 : X1] : ((c_2Epair_2ECURRY @ X0 @ X1 @ X2 @ X3 @ X4 @ X5) = (X3 @ (c_2Epair_2E_2C @ X0 @ X1 @ X4 @ X5)))),
% 31.59/5.79 inference(rectify,[status(thm)],[f9])).
% 31.59/5.79 thf(f9,axiom,(
% 31.59/5.79 ! [X0 : $tType,X1 : $tType,X2 : $tType,X5 : tyop_2Epair_2Eprod @ X0 @ X1 > X2,X6 : X0,X8 : X1] : ((c_2Epair_2ECURRY @ X0 @ X1 @ X2 @ X5 @ X6 @ X8) = (X5 @ (c_2Epair_2E_2C @ X0 @ X1 @ X6 @ X8)))),
% 31.59/5.79 file('/export/starexec/sandbox/tmp/tmp.HpJsg7gn6n/DTF2THF_17586.p',thm_2Epair_2ECURRY__DEF)).
% 31.59/5.79 thf(f81,plain,(
% 31.59/5.79 ( ! [X0 : tyop_2Epair_2Eprod @ sK2 @ sK2 > $o] : (((c_2Epair_2ECURRY @ sK2 @ sK2 @ $o @ X0 @ (sK6 @ X0) @ (sK7 @ X0)) != (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ (sK6 @ X0) @ (sK7 @ X0)) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3)))) | ((c_2Ewellorder_2Ewellfounded @ sK2 @ X0) != $true)) )),
% 31.59/5.79 inference(beta_eta_normalization,[status(thm)],[f73])).
% 31.59/5.79 thf(f73,plain,(
% 31.59/5.79 ( ! [X0 : tyop_2Epair_2Eprod @ sK2 @ sK2 > $o] : (((c_2Ewellorder_2Ewellfounded @ sK2 @ X0) != $true) | ((c_2Epair_2ECURRY @ sK2 @ sK2 @ $o @ X0 @ (sK6 @ X0) @ (sK7 @ X0)) != ((^[Y0 : sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ (sK6 @ X0) @ Y0) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3)))) @ (sK7 @ X0)))) )),
% 31.59/5.79 inference(negative_extensionality,[status(thm)],[f71])).
% 31.59/5.79 thf(f71,plain,(
% 31.59/5.79 ( ! [X0 : tyop_2Epair_2Eprod @ sK2 @ sK2 > $o] : (((^[Y0 : sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ (sK6 @ X0) @ Y0) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3)))) != (c_2Epair_2ECURRY @ sK2 @ sK2 @ $o @ X0 @ (sK6 @ X0))) | ((c_2Ewellorder_2Ewellfounded @ sK2 @ X0) != $true)) )),
% 31.59/5.79 inference(beta_eta_normalization,[status(thm)],[f67])).
% 31.59/5.79 thf(f67,plain,(
% 31.59/5.79 ( ! [X0 : tyop_2Epair_2Eprod @ sK2 @ sK2 > $o] : (((c_2Ewellorder_2Ewellfounded @ sK2 @ X0) != $true) | ((c_2Epair_2ECURRY @ sK2 @ sK2 @ $o @ X0 @ (sK6 @ X0)) != ((^[Y0 : sK2]: ((^[Y1 : sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3)))))) @ (sK6 @ X0)))) )),
% 31.59/5.79 inference(negative_extensionality,[status(thm)],[f66])).
% 31.59/5.79 thf(f66,plain,(
% 31.59/5.79 ( ! [X0 : tyop_2Epair_2Eprod @ sK2 @ sK2 > $o] : (((^[Y0 : sK2]: ((^[Y1 : sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3)))))) != (c_2Epair_2ECURRY @ sK2 @ sK2 @ $o @ X0)) | ((c_2Ewellorder_2Ewellfounded @ sK2 @ X0) != $true)) )),
% 31.59/5.79 inference(constrained_superposition,[status(thm)],[f63,f60])).
% 31.59/5.79 thf(f60,plain,(
% 31.59/5.79 ( ! [X0 : $tType,X1 : tyop_2Epair_2Eprod @ X0 @ X0 > $o] : (((c_2Ewellorder_2Ewellfounded @ X0 @ X1) = (c_2Erelation_2EWF @ X0 @ (c_2Epair_2ECURRY @ X0 @ X0 @ $o @ X1)))) )),
% 31.59/5.79 inference(cnf_transformation,[status(thm)],[f28])).
% 31.59/5.79 thf(f28,plain,(
% 31.59/5.79 ! [X0 : $tType,X1 : tyop_2Epair_2Eprod @ X0 @ X0 > $o] : ((c_2Ewellorder_2Ewellfounded @ X0 @ X1) = (c_2Erelation_2EWF @ X0 @ (c_2Epair_2ECURRY @ X0 @ X0 @ $o @ X1)))),
% 31.59/5.79 inference(fool_elimination,[status(thm)],[f27])).
% 31.59/5.79 thf(f27,plain,(
% 31.59/5.79 ! [X0 : $tType,X1 : tyop_2Epair_2Eprod @ X0 @ X0 > $o] : ((c_2Ewellorder_2Ewellfounded @ X0 @ X1) = (c_2Erelation_2EWF @ X0 @ (c_2Epair_2ECURRY @ X0 @ X0 @ $o @ X1)))),
% 31.59/5.79 inference(rectify,[status(thm)],[f10])).
% 31.59/5.79 thf(f10,axiom,(
% 31.59/5.79 ! [X0 : $tType,X9 : tyop_2Epair_2Eprod @ X0 @ X0 > $o] : ((c_2Ewellorder_2Ewellfounded @ X0 @ X9) = (c_2Erelation_2EWF @ X0 @ (c_2Epair_2ECURRY @ X0 @ X0 @ $o @ X9)))),
% 31.59/5.79 file('/export/starexec/sandbox/tmp/tmp.HpJsg7gn6n/DTF2THF_17586.p',thm_2Ewellorder_2Ewellfounded__WF)).
% 31.59/5.79 thf(f63,plain,(
% 31.59/5.79 ((c_2Erelation_2EWF @ sK2 @ (^[Y0 : sK2]: ((^[Y1 : sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3))))))) != $true)),
% 31.59/5.79 inference(cnf_transformation,[status(thm)],[f58])).
% 31.59/5.79 thf(f58,plain,(
% 31.59/5.79 ((c_2Erelation_2EWF @ sK2 @ (^[Y0 : sK2]: ((^[Y1 : sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3))))))) != $true)),
% 31.59/5.79 inference(skolemisation,[status(esa),new_symbols(skolem,[sK2,sK3])],[f56,f57])).
% 31.59/5.79 thf(f57,plain,(
% 31.59/5.79 ? [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : ((c_2Erelation_2EWF @ X0 @ (^[Y0 : X0]: ((^[Y1 : X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))))) != $true) => ((c_2Erelation_2EWF @ sK2 @ (^[Y0 : sK2]: ((^[Y1 : sK2]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ sK2 @ sK2 @ (c_2Epair_2E_2C @ sK2 @ sK2 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ sK2 @ (c_2Ewellorder_2Ewellorder__REP @ sK2 @ sK3))))))) != $true)),
% 31.59/5.79 introduced(definition,[],[choice_axiom])).
% 31.59/5.79 thf(f56,plain,(
% 31.59/5.79 ? [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : ((c_2Erelation_2EWF @ X0 @ (^[Y0 : X0]: ((^[Y1 : X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))))) != $true)),
% 31.59/5.79 inference(ennf_transformation,[status(thm)],[f24])).
% 31.59/5.79 thf(f24,plain,(
% 31.59/5.79 ~! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : ((c_2Erelation_2EWF @ X0 @ (^[Y0 : X0]: ((^[Y1 : X0]: (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ Y0 @ Y1) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1))))))) = $true)),
% 31.59/5.79 inference(fool_elimination,[status(thm)],[f23])).
% 31.59/5.79 thf(f23,plain,(
% 31.59/5.79 ~! [X0 : $tType,X1 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Erelation_2EWF @ X0 @ (^[X2 : X0, X3 : X0] : (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ X2 @ X3) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X1)))))),
% 31.59/5.79 inference(rectify,[status(thm)],[f13])).
% 31.59/5.79 thf(f13,negated_conjecture,(
% 31.59/5.79 ~! [X0 : $tType,X10 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Erelation_2EWF @ X0 @ (^[X6 : X0, X8 : X0] : (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ X6 @ X8) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X10)))))),
% 31.59/5.79 inference(negated_conjecture,[status(cth)],[f12])).
% 31.59/5.79 thf(f12,conjecture,(
% 31.59/5.79 ! [X0 : $tType,X10 : tyop_2Ewellorder_2Ewellorder @ X0] : (c_2Erelation_2EWF @ X0 @ (^[X6 : X0, X8 : X0] : (c_2Ebool_2EIN @ tyop_2Epair_2Eprod @ X0 @ X0 @ (c_2Epair_2E_2C @ X0 @ X0 @ X6 @ X8) @ (c_2Eset__relation_2Estrict @ X0 @ (c_2Ewellorder_2Ewellorder__REP @ X0 @ X10)))))),
% 31.59/5.79 file('/export/starexec/sandbox/tmp/tmp.HpJsg7gn6n/DTF2THF_17586.p',thm_2Ewellorder_2EWIN__WF2)).
% 31.59/5.79 % SZS output end Proof for DTF2THF_17586
% 31.59/5.79 % (17972)------------------------------
% 31.59/5.79 % (17972)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 31.59/5.79 % (17972)Termination reason: Refutation
% 31.59/5.79
% 31.59/5.79 % (17972)Memory used [KB]: 6012
% 31.59/5.79 % (17972)Time elapsed: 0.027 s
% 31.59/5.79 % (17972)Instructions burned: 83 (million)
% 31.59/5.79 % (17972)------------------------------
% 31.59/5.79 % (17972)------------------------------
% 31.59/5.79 % (17699)Success in time 4.469 s
%------------------------------------------------------------------------------