%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : NUM727^1 : TPTP v9.2.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n006.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 09:24:26 AM UTC 2026
% Result : Theorem 1.65s 1.86s
% Output : Refutation 1.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 6
% Syntax : Number of formulae : 56 ( 54 unt; 0 typ; 0 def)
% Number of atoms : 171 ( 100 equ; 0 cnn)
% Maximal formula atoms : 2 ( 3 avg)
% Number of connectives : 518 ( 13 ~; 0 |; 0 &; 464 @)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Number of types : 2 ( 2 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 11 ( 7 usr; 6 con; 0-2 aty)
% ( 30 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 101 ( 38 ^; 63 !; 0 ?; 101 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
frac: $tType ).
thf(type_def_6,type,
nat: $tType ).
thf(func_def_0,type,
frac: $tType ).
thf(func_def_1,type,
x: frac ).
thf(func_def_2,type,
y: frac ).
thf(func_def_3,type,
z: frac ).
thf(func_def_4,type,
nat: $tType ).
thf(func_def_5,type,
ts: nat > nat > nat ).
thf(func_def_6,type,
num: frac > nat ).
thf(func_def_7,type,
den: frac > nat ).
thf(func_def_20,type,
ph1:
!>[X0: $tType] : X0 ).
thf(f152,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f151]) ).
thf(f151,plain,
$false = $true,
inference(boolean_simplification,[status(thm)],[f150]) ).
thf(f150,plain,
( $true = ( ~ $true ) ),
inference(boolean_simplification,[status(thm)],[f149]) ).
thf(f149,plain,
( ( ( ts @ ( num @ x ) @ ( ts @ ( num @ y ) @ ( den @ z ) ) )
!= ( ts @ ( num @ x ) @ ( ts @ ( num @ y ) @ ( den @ z ) ) ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f148,f23]) ).
thf(f23,plain,
( ( ts @ ( num @ y ) @ ( den @ z ) )
= ( ts @ ( num @ z ) @ ( den @ y ) ) ),
inference(cnf_transformation,[status(thm)],[f14]) ).
thf(f14,plain,
( ( ts @ ( num @ y ) @ ( den @ z ) )
= ( ts @ ( num @ z ) @ ( den @ y ) ) ),
inference(fool_elimination,[status(thm)],[f2]) ).
thf(f2,axiom,
( ( ts @ ( num @ y ) @ ( den @ z ) )
= ( ts @ ( num @ z ) @ ( den @ y ) ) ),
file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',f) ).
thf(f148,plain,
( ( ( ts @ ( num @ x ) @ ( ts @ ( num @ y ) @ ( den @ z ) ) )
!= ( ts @ ( num @ x ) @ ( ts @ ( num @ z ) @ ( den @ y ) ) ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f147,f32]) ).
thf(f32,plain,
! [X2: nat,X1: nat] :
( ( ts @ X1 @ X2 )
= ( ts @ X2 @ X1 ) ),
inference(equality_proxy_clausification,[status(thm)],[f31]) ).
thf(f31,plain,
! [X2: nat,X1: nat] :
( ( ( ts @ X2 @ X1 )
= ( ts @ X1 @ X2 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f30]) ).
thf(f30,plain,
! [X2: nat,X1: nat] :
( ( ^ [Y0: nat] :
( ( ts @ Y0 @ X1 )
= ( ts @ X1 @ Y0 ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f29]) ).
thf(f29,plain,
! [X1: nat] :
( ( !! @ nat
@ ^ [Y0: nat] :
( ( ts @ Y0 @ X1 )
= ( ts @ X1 @ Y0 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f28]) ).
thf(f28,plain,
! [X1: nat] :
( $true
= ( ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ts @ Y1 @ Y0 )
= ( ts @ Y0 @ Y1 ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f22]) ).
thf(f22,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ts @ Y1 @ Y0 )
= ( ts @ Y0 @ Y1 ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f13]) ).
thf(f13,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ts @ Y1 @ Y0 )
= ( ts @ Y0 @ Y1 ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f12]) ).
thf(f12,plain,
! [X0: nat,X1: nat] :
( ( ts @ X0 @ X1 )
= ( ts @ X1 @ X0 ) ),
inference(rectify,[status(thm)],[f4]) ).
thf(f4,axiom,
! [X1: nat,X0: nat] :
( ( ts @ X0 @ X1 )
= ( ts @ X1 @ X0 ) ),
file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',satz29) ).
thf(f147,plain,
( ( ( ts @ ( num @ x ) @ ( ts @ ( num @ y ) @ ( den @ z ) ) )
!= ( ts @ ( num @ x ) @ ( ts @ ( den @ y ) @ ( num @ z ) ) ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f140,f95]) ).
thf(f95,plain,
! [X2: nat,X0: nat,X1: nat] :
( ( ts @ X0 @ ( ts @ X1 @ X2 ) )
= ( ts @ X2 @ ( ts @ X0 @ X1 ) ) ),
inference(superposition,[status(thm)],[f32,f63]) ).
thf(f63,plain,
! [X2: nat,X3: nat,X1: nat] :
( ( ts @ X2 @ ( ts @ X3 @ X1 ) )
= ( ts @ ( ts @ X2 @ X3 ) @ X1 ) ),
inference(equality_proxy_clausification,[status(thm)],[f62]) ).
thf(f62,plain,
! [X2: nat,X3: nat,X1: nat] :
( ( ( ts @ ( ts @ X2 @ X3 ) @ X1 )
= ( ts @ X2 @ ( ts @ X3 @ X1 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f61]) ).
thf(f61,plain,
! [X2: nat,X3: nat,X1: nat] :
( ( ^ [Y0: nat] :
( ( ts @ ( ts @ X2 @ Y0 ) @ X1 )
= ( ts @ X2 @ ( ts @ Y0 @ X1 ) ) )
@ X3 )
= $true ),
inference(pi_clausification,[status(thm)],[f60]) ).
thf(f60,plain,
! [X2: nat,X1: nat] :
( ( !! @ nat
@ ^ [Y0: nat] :
( ( ts @ ( ts @ X2 @ Y0 ) @ X1 )
= ( ts @ X2 @ ( ts @ Y0 @ X1 ) ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f59]) ).
thf(f59,plain,
! [X2: nat,X1: nat] :
( ( ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ts @ ( ts @ Y0 @ Y1 ) @ X1 )
= ( ts @ Y0 @ ( ts @ Y1 @ X1 ) ) ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f58]) ).
thf(f58,plain,
! [X1: nat] :
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ts @ ( ts @ Y0 @ Y1 ) @ X1 )
= ( ts @ Y0 @ ( ts @ Y1 @ X1 ) ) ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f57]) ).
thf(f57,plain,
! [X1: nat] :
( $true
= ( ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( !! @ nat
@ ^ [Y2: nat] :
( ( ts @ ( ts @ Y1 @ Y2 ) @ Y0 )
= ( ts @ Y1 @ ( ts @ Y2 @ Y0 ) ) ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f19]) ).
thf(f19,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( !! @ nat
@ ^ [Y2: nat] :
( ( ts @ ( ts @ Y1 @ Y2 ) @ Y0 )
= ( ts @ Y1 @ ( ts @ Y2 @ Y0 ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
thf(f10,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( !! @ nat
@ ^ [Y2: nat] :
( ( ts @ ( ts @ Y1 @ Y2 ) @ Y0 )
= ( ts @ Y1 @ ( ts @ Y2 @ Y0 ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f9]) ).
thf(f9,plain,
! [X0: nat,X1: nat,X2: nat] :
( ( ts @ ( ts @ X1 @ X0 ) @ X2 )
= ( ts @ X1 @ ( ts @ X0 @ X2 ) ) ),
inference(rectify,[status(thm)],[f5]) ).
thf(f5,axiom,
! [X1: nat,X0: nat,X2: nat] :
( ( ts @ ( ts @ X0 @ X1 ) @ X2 )
= ( ts @ X0 @ ( ts @ X1 @ X2 ) ) ),
file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',satz31) ).
thf(f140,plain,
( $true
= ( ( ts @ ( num @ x ) @ ( ts @ ( num @ y ) @ ( den @ z ) ) )
!= ( ts @ ( num @ z ) @ ( ts @ ( num @ x ) @ ( den @ y ) ) ) ) ),
inference(superposition,[status(thm)],[f138,f20]) ).
thf(f20,plain,
( ( ts @ ( num @ x ) @ ( den @ y ) )
= ( ts @ ( num @ y ) @ ( den @ x ) ) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
thf(f11,plain,
( ( ts @ ( num @ x ) @ ( den @ y ) )
= ( ts @ ( num @ y ) @ ( den @ x ) ) ),
inference(fool_elimination,[status(thm)],[f1]) ).
thf(f1,axiom,
( ( ts @ ( num @ x ) @ ( den @ y ) )
= ( ts @ ( num @ y ) @ ( den @ x ) ) ),
file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',e) ).
thf(f138,plain,
! [X0: nat] :
( ( ( ts @ ( num @ x ) @ ( ts @ X0 @ ( den @ z ) ) )
!= ( ts @ ( num @ z ) @ ( ts @ X0 @ ( den @ x ) ) ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f137,f95]) ).
thf(f137,plain,
! [X0: nat] :
( ( ( ts @ ( num @ x ) @ ( ts @ X0 @ ( den @ z ) ) )
!= ( ts @ ( den @ x ) @ ( ts @ ( num @ z ) @ X0 ) ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f136,f89]) ).
thf(f89,plain,
! [X2: nat,X0: nat,X1: nat] :
( ( ts @ X0 @ ( ts @ X1 @ X2 ) )
= ( ts @ ( ts @ X1 @ X0 ) @ X2 ) ),
inference(superposition,[status(thm)],[f63,f32]) ).
thf(f136,plain,
! [X0: nat] :
( ( ( ts @ ( num @ x ) @ ( ts @ X0 @ ( den @ z ) ) )
!= ( ts @ ( ts @ ( num @ z ) @ ( den @ x ) ) @ X0 ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f135,f95]) ).
thf(f135,plain,
! [X0: nat] :
( $true
= ( ( ts @ ( den @ z ) @ ( ts @ ( num @ x ) @ X0 ) )
!= ( ts @ ( ts @ ( num @ z ) @ ( den @ x ) ) @ X0 ) ) ),
inference(forward_demodulation,[status(thm)],[f134,f89]) ).
thf(f134,plain,
! [X0: nat] :
( ( ( ts @ ( ts @ ( num @ x ) @ ( den @ z ) ) @ X0 )
!= ( ts @ ( ts @ ( num @ z ) @ ( den @ x ) ) @ X0 ) )
= $true ),
inference(boolean_simplification,[status(thm)],[f118]) ).
thf(f118,plain,
! [X0: nat] :
( $true
= ( ( ( ts @ ( ts @ ( num @ x ) @ ( den @ z ) ) @ X0 )
= ( ts @ ( ts @ ( num @ z ) @ ( den @ x ) ) @ X0 ) )
=> $false ) ),
inference(superposition,[status(thm)],[f116,f24]) ).
thf(f24,plain,
( ( ( ts @ ( num @ x ) @ ( den @ z ) )
= ( ts @ ( num @ z ) @ ( den @ x ) ) )
= $false ),
inference(not_proxy_clausification,[status(thm)],[f18]) ).
thf(f18,plain,
( ( ( ts @ ( num @ x ) @ ( den @ z ) )
!= ( ts @ ( num @ z ) @ ( den @ x ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f15]) ).
thf(f15,plain,
( ( ( ts @ ( num @ x ) @ ( den @ z ) )
!= ( ts @ ( num @ z ) @ ( den @ x ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f7]) ).
thf(f7,negated_conjecture,
( ( ts @ ( num @ x ) @ ( den @ z ) )
!= ( ts @ ( num @ z ) @ ( den @ x ) ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
thf(f6,conjecture,
( ( ts @ ( num @ x ) @ ( den @ z ) )
= ( ts @ ( num @ z ) @ ( den @ x ) ) ),
file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',satz39) ).
thf(f116,plain,
! [X2: nat,X3: nat,X1: nat] :
( $true
= ( ( ( ts @ X3 @ X2 )
= ( ts @ X1 @ X2 ) )
=> ( X3 = X1 ) ) ),
inference(beta_eta_normalization,[status(thm)],[f115]) ).
thf(f115,plain,
! [X2: nat,X3: nat,X1: nat] :
( ( ^ [Y0: nat] :
( ( ( ts @ Y0 @ X2 )
= ( ts @ X1 @ X2 ) )
=> ( Y0 = X1 ) )
@ X3 )
= $true ),
inference(pi_clausification,[status(thm)],[f114]) ).
thf(f114,plain,
! [X2: nat,X1: nat] :
( ( !! @ nat
@ ^ [Y0: nat] :
( ( ( ts @ Y0 @ X2 )
= ( ts @ X1 @ X2 ) )
=> ( Y0 = X1 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f113]) ).
thf(f113,plain,
! [X2: nat,X1: nat] :
( ( ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ( ts @ Y1 @ Y0 )
= ( ts @ X1 @ Y0 ) )
=> ( Y1 = X1 ) ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f112]) ).
thf(f112,plain,
! [X1: nat] :
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( ( ( ts @ Y1 @ Y0 )
= ( ts @ X1 @ Y0 ) )
=> ( Y1 = X1 ) ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f111]) ).
thf(f111,plain,
! [X1: nat] :
( $true
= ( ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( !! @ nat
@ ^ [Y2: nat] :
( ( ( ts @ Y2 @ Y1 )
= ( ts @ Y0 @ Y1 ) )
=> ( Y2 = Y0 ) ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f21]) ).
thf(f21,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( !! @ nat
@ ^ [Y2: nat] :
( ( ( ts @ Y2 @ Y1 )
= ( ts @ Y0 @ Y1 ) )
=> ( Y2 = Y0 ) ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f17]) ).
thf(f17,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( !! @ nat
@ ^ [Y1: nat] :
( !! @ nat
@ ^ [Y2: nat] :
( ( ( ts @ Y2 @ Y1 )
= ( ts @ Y0 @ Y1 ) )
=> ( Y2 = Y0 ) ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f16]) ).
thf(f16,plain,
! [X0: nat,X1: nat,X2: nat] :
( ( ( ts @ X0 @ X1 )
= ( ts @ X2 @ X1 ) )
=> ( X0 = X2 ) ),
inference(rectify,[status(thm)],[f3]) ).
thf(f3,axiom,
! [X1: nat,X2: nat,X0: nat] :
( ( ( ts @ X0 @ X2 )
= ( ts @ X1 @ X2 ) )
=> ( X0 = X1 ) ),
file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',satz33b) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : NUM727^1 : TPTP v9.2.1. Released v3.7.0.
% 0.00/0.10 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.29 % Computer : n006.cluster.edu
% 0.11/0.29 % Model : x86_64 x86_64
% 0.11/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.29 % Memory : 8042.1875MB
% 0.11/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.29 % CPULimit : 300
% 0.11/0.29 % WCLimit : 300
% 0.11/0.29 % DateTime : Tue Feb 24 11:12:00 EST 2026
% 0.11/0.30 % CPUTime :
% 0.11/0.30 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.39 ---- Original DTF file ---
% 0.16/0.39 thf(spec,logic,$$dhol).
% 0.16/0.39 %------------------------------------------------------------------------------
% 0.16/0.39 % File : NUM727^1 : TPTP v9.2.1. Released v3.7.0.
% 0.16/0.39 % Domain : Number Theory
% 0.16/0.39 % Problem : Landau theorem 39
% 0.16/0.39 % Version : Especial.
% 0.16/0.39 % English : ts (num x) (den z) = ts (num z) (den x)
% 0.16/0.39
% 0.16/0.39 % Refs : [Lan30] Landau (1930), Grundlagen der Analysis
% 0.16/0.39 % : [vBJ79] van Benthem Jutting (1979), Checking Landau's "Grundla
% 0.16/0.39 % : [Bro09] Brown (2009), Email to Geoff Sutcliffe
% 0.16/0.39 % Source : [Bro09]
% 0.16/0.39 % Names : satz39 [Lan30]
% 0.16/0.39
% 0.16/0.39 % Status : Theorem
% 0.16/0.39 % : Without extensionality : Theorem
% 0.16/0.39 % Rating : 0.11 v9.1.0, 0.12 v9.0.0, 0.20 v8.2.0, 0.23 v8.1.0, 0.18 v7.5.0, 0.14 v7.4.0, 0.44 v7.3.0, 0.56 v7.2.0, 0.50 v7.1.0, 0.62 v7.0.0, 0.57 v6.4.0, 0.67 v6.3.0, 0.60 v6.2.0, 0.43 v6.1.0, 0.57 v5.5.0, 0.67 v5.4.0, 0.80 v5.2.0, 1.00 v5.0.0, 0.80 v4.1.0, 1.00 v3.7.0
% 0.16/0.39 % Syntax : Number of formulae : 14 ( 5 unt; 8 typ; 0 def)
% 0.16/0.39 % Number of atoms : 7 ( 7 equ; 0 cnn)
% 0.16/0.39 % Maximal formula atoms : 2 ( 1 avg)
% 0.16/0.39 % Number of connectives : 41 ( 0 ~; 0 |; 0 &; 40 @)
% 0.16/0.39 % ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% 0.16/0.39 % Maximal formula depth : 5 ( 3 avg)
% 0.16/0.39 % Number of types : 2 ( 2 usr)
% 0.16/0.39 % Number of type conns : 4 ( 4 >; 0 *; 0 +; 0 <<)
% 0.16/0.39 % Number of symbols : 7 ( 6 usr; 3 con; 0-2 aty)
% 0.16/0.39 % Number of variables : 8 ( 0 ^; 8 !; 0 ?; 8 :)
% 0.16/0.39 % SPC : TH0_THM_EQU_NAR
% 0.16/0.39
% 0.16/0.39 % Comments :
% 0.16/0.39 %------------------------------------------------------------------------------
% 0.16/0.39 thf(frac_type,type,
% 0.16/0.39 frac: $tType ).
% 0.16/0.39
% 0.16/0.39 thf(x,type,
% 0.16/0.39 x: frac ).
% 0.16/0.39
% 0.16/0.39 thf(y,type,
% 0.16/0.39 y: frac ).
% 0.16/0.39
% 0.16/0.39 thf(z,type,
% 0.16/0.39 z: frac ).
% 0.16/0.39
% 0.16/0.39 thf(nat_type,type,
% 0.16/0.39 nat: $tType ).
% 0.16/0.39
% 0.16/0.39 thf(ts,type,
% 0.16/0.39 ts: nat > nat > nat ).
% 0.16/0.39
% 0.16/0.39 thf(num,type,
% 0.16/0.39 num: frac > nat ).
% 0.16/0.39
% 0.16/0.39 thf(den,type,
% 0.16/0.39 den: frac > nat ).
% 0.16/0.39
% 0.16/0.39 thf(e,axiom,
% 0.16/0.39 ( ( ts @ ( num @ x ) @ ( den @ y ) )
% 0.16/0.39 = ( ts @ ( num @ y ) @ ( den @ x ) ) ) ).
% 0.16/0.39
% 0.16/0.39 thf(f,axiom,
% 0.16/0.39 ( ( ts @ ( num @ y ) @ ( den @ z ) )
% 0.16/0.39 = ( ts @ ( num @ z ) @ ( den @ y ) ) ) ).
% 0.16/0.39
% 0.16/0.39 thf(satz33b,axiom,
% 0.16/0.39 ! [Xx: nat,Xy: nat,Xz: nat] :
% 0.16/0.39 ( ( ( ts @ Xx @ Xz )
% 0.16/0.39 = ( ts @ Xy @ Xz ) )
% 0.16/0.39 => ( Xx = Xy ) ) ).
% 0.16/0.39
% 0.16/0.39 thf(satz29,axiom,
% 0.16/0.39 ! [Xx: nat,Xy: nat] :
% 0.16/0.39 ( ( ts @ Xx @ Xy )
% 0.16/0.39 = ( ts @ Xy @ Xx ) ) ).
% 0.16/0.39
% 0.16/0.39 thf(satz31,axiom,
% 0.16/0.39 ! [Xx: nat,Xy: nat,Xz: nat] :
% 0.16/0.39 ( ( ts @ ( ts @ Xx @ Xy ) @ Xz )
% 0.16/0.39 = ( ts @ Xx @ ( ts @ Xy @ Xz ) ) ) ).
% 0.16/0.39
% 0.16/0.39 thf(satz39,conjecture,
% 0.16/0.39 ( ( ts @ ( num @ x ) @ ( den @ z ) )
% 0.16/0.39 = ( ts @ ( num @ z ) @ ( den @ x ) ) ) ).
% 0.16/0.39
% 0.16/0.39 %------------------------------------------------------------------------------
% 0.16/0.39 ------------------------
% 1.59/1.32 ---- Embedded in THF ---
% 1.59/1.32 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.59/1.32 %%% Generated on Tue Feb 24 11:12:01 EST 2026
% 1.59/1.32 %%% using '$$dhol' embedding, version 1.3.0.
% 1.59/1.32 %%% Logic specification used:
% 1.59/1.32 %%% thf(spec, logic, $$dhol).
% 1.59/1.32
% 1.59/1.32 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2DTF2852.p
% See solution above
% 1.59/1.32 ------------------------
% 1.59/1.33 ---- Cleaned THF ---
% 1.59/1.33 thf(frac_type,type,
% 1.59/1.33 frac: $tType ).
% 1.59/1.33
% 1.59/1.33 thf(x,type,
% 1.59/1.33 x: frac ).
% 1.59/1.33
% 1.59/1.33 thf(y,type,
% 1.59/1.33 y: frac ).
% 1.59/1.33
% 1.59/1.33 thf(z,type,
% 1.59/1.33 z: frac ).
% 1.59/1.33
% 1.59/1.33 thf(nat_type,type,
% 1.59/1.33 nat: $tType ).
% 1.59/1.33
% 1.59/1.33 thf(ts,type,
% 1.59/1.33 ts: nat > nat > nat ).
% 1.59/1.33
% 1.59/1.33 thf(num,type,
% 1.59/1.33 num: frac > nat ).
% 1.59/1.33
% 1.59/1.33 thf(den,type,
% 1.59/1.33 den: frac > nat ).
% 1.59/1.33
% 1.59/1.33 thf(e,axiom,
% 1.59/1.33 ( ( ts @ ( num @ x ) @ ( den @ y ) )
% 1.59/1.33 = ( ts @ ( num @ y ) @ ( den @ x ) ) ) ).
% 1.59/1.33
% 1.59/1.33 thf(f,axiom,
% 1.59/1.33 ( ( ts @ ( num @ y ) @ ( den @ z ) )
% 1.59/1.33 = ( ts @ ( num @ z ) @ ( den @ y ) ) ) ).
% 1.59/1.33
% 1.59/1.33 thf(satz33b,axiom,
% 1.59/1.33 ! [Xx: nat,Xy: nat,Xz: nat] :
% 1.59/1.33 ( ( ( ts @ Xx @ Xz )
% 1.59/1.33 = ( ts @ Xy @ Xz ) )
% 1.59/1.33 => ( Xx = Xy ) ) ).
% 1.59/1.33
% 1.59/1.33 thf(satz29,axiom,
% 1.59/1.33 ! [Xx: nat,Xy: nat] :
% 1.59/1.33 ( ( ts @ Xx @ Xy )
% 1.59/1.33 = ( ts @ Xy @ Xx ) ) ).
% 1.59/1.33
% 1.59/1.33 thf(satz31,axiom,
% 1.59/1.33 ! [Xx: nat,Xy: nat,Xz: nat] :
% 1.59/1.33 ( ( ts @ ( ts @ Xx @ Xy ) @ Xz )
% 1.59/1.33 = ( ts @ Xx @ ( ts @ Xy @ Xz ) ) ) ).
% 1.59/1.33
% 1.59/1.33 thf(satz39,conjecture,
% 1.59/1.33 ( ( ts @ ( num @ x ) @ ( den @ z ) )
% 1.59/1.33 = ( ts @ ( num @ z ) @ ( den @ x ) ) ) ).
% 1.59/1.33 ------------------------
% 1.59/1.35 % (2953)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_2852 for (2999ds/27Mi)
% 1.59/1.35 % (2954)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/2Mi)
% 1.59/1.35 % (2952)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_2852 for (2999ds/4Mi)
% 1.59/1.35 % (2951)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/183Mi)
% 1.59/1.35 % (2957)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/18Mi)
% 1.59/1.35 % (2956)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_2852 for (2999ds/275Mi)
% 1.59/1.35 % (2955)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_2852 for (2999ds/2Mi)
% 1.59/1.35 % (2954)Instruction limit reached!
% 1.59/1.35 % (2954)------------------------------
% 1.59/1.35 % (2954)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.35 % (2954)Termination reason: Unknown
% 1.59/1.35 % (2954)Termination phase: Saturation
% 1.59/1.35
% 1.59/1.35 % (2955)Instruction limit reached!
% 1.59/1.35 % (2955)------------------------------
% 1.59/1.35 % (2955)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.35 % (2955)Termination reason: Unknown
% 1.59/1.35 % (2955)Termination phase: Saturation
% 1.59/1.35
% 1.59/1.35 % (2955)Memory used [KB]: 895
% 1.59/1.35 % (2955)Time elapsed: 0.003 s
% 1.59/1.35 % (2955)Instructions burned: 2 (million)
% 1.59/1.35 % (2955)------------------------------
% 1.59/1.35 % (2955)------------------------------
% 1.59/1.35 % (2954)Memory used [KB]: 5373
% 1.59/1.35 % (2954)Time elapsed: 0.003 s
% 1.59/1.35 % (2954)Instructions burned: 2 (million)
% 1.59/1.35 % (2954)------------------------------
% 1.59/1.35 % (2954)------------------------------
% 1.59/1.35 % (2956)Refutation not found, incomplete strategy
% 1.59/1.35 % (2956)------------------------------
% 1.59/1.35 % (2956)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.35 % (2956)Termination reason: Refutation not found, incomplete strategy
% 1.59/1.35
% 1.59/1.35
% 1.59/1.35 % (2956)Memory used [KB]: 5500
% 1.59/1.35 % (2956)Time elapsed: 0.003 s
% 1.59/1.35 % (2956)Instructions burned: 2 (million)
% 1.59/1.35 % (2956)------------------------------
% 1.59/1.35 % (2956)------------------------------
% 1.59/1.35 % (2952)Instruction limit reached!
% 1.59/1.35 % (2952)------------------------------
% 1.59/1.35 % (2952)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.35 % (2952)Termination reason: Unknown
% 1.59/1.35 % (2952)Termination phase: Saturation
% 1.59/1.35
% 1.59/1.35 % (2952)Memory used [KB]: 5500
% 1.59/1.35 % (2952)Time elapsed: 0.004 s
% 1.59/1.35 % (2952)Instructions burned: 4 (million)
% 1.59/1.35 % (2952)------------------------------
% 1.59/1.35 % (2952)------------------------------
% 1.59/1.36 % (2957)Instruction limit reached!
% 1.59/1.36 % (2957)------------------------------
% 1.59/1.36 % (2957)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.36 % (2957)Termination reason: Unknown
% 1.59/1.36 % (2957)Termination phase: Saturation
% 1.59/1.36
% 1.59/1.36 % (2957)Memory used [KB]: 5500
% 1.59/1.36 % (2957)Time elapsed: 0.012 s
% 1.59/1.36 % (2957)Instructions burned: 19 (million)
% 1.59/1.36 % (2957)------------------------------
% 1.59/1.36 % (2957)------------------------------
% 1.59/1.36 % (2953)Instruction limit reached!
% 1.59/1.36 % (2953)------------------------------
% 1.59/1.36 % (2953)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.36 % (2953)Termination reason: Unknown
% 1.59/1.36 % (2953)Termination phase: Saturation
% 1.59/1.36
% 1.59/1.36 % (2953)Memory used [KB]: 5500
% 1.59/1.36 % (2953)Time elapsed: 0.016 s
% 1.59/1.36 % (2953)Instructions burned: 27 (million)
% 1.59/1.36 % (2953)------------------------------
% 1.59/1.36 % (2953)------------------------------
% 1.59/1.37 % (2958)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/3Mi)
% 1.59/1.37 % (2959)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_2852 for (2999ds/37Mi)
% 1.59/1.37 % (2961)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_2852 for (2999ds/3Mi)
% 1.59/1.37 % (2960)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_2852 for (2999ds/15Mi)
% 1.59/1.37 % (2958)Instruction limit reached!
% 1.59/1.37 % (2958)------------------------------
% 1.59/1.37 % (2958)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.37 % (2958)Termination reason: Unknown
% 1.59/1.37 % (2958)Termination phase: Saturation
% 1.59/1.37
% 1.59/1.37 % (2958)Memory used [KB]: 5500
% 1.59/1.37 % (2958)Time elapsed: 0.003 s
% 1.59/1.37 % (2958)Instructions burned: 3 (million)
% 1.59/1.37 % (2958)------------------------------
% 1.59/1.37 % (2958)------------------------------
% 1.59/1.37 % (2960)Refutation not found, incomplete strategy
% 1.59/1.37 % (2960)------------------------------
% 1.59/1.37 % (2960)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.37 % (2961)Instruction limit reached!
% 1.59/1.37 % (2961)------------------------------
% 1.59/1.37 % (2961)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.37 % (2961)Termination reason: Unknown
% 1.59/1.37 % (2961)Termination phase: Saturation
% 1.59/1.37
% 1.59/1.37 % (2961)Memory used [KB]: 5500
% 1.59/1.37 % (2961)Time elapsed: 0.003 s
% 1.59/1.37 % (2961)Instructions burned: 3 (million)
% 1.59/1.37 % (2961)------------------------------
% 1.59/1.37 % (2961)------------------------------
% 1.59/1.37 % (2960)Termination reason: Refutation not found, incomplete strategy
% 1.59/1.37
% 1.59/1.37
% 1.59/1.37 % (2960)Memory used [KB]: 5500
% 1.59/1.37 % (2960)Time elapsed: 0.003 s
% 1.59/1.37 % (2960)Instructions burned: 3 (million)
% 1.59/1.37 % (2960)------------------------------
% 1.59/1.37 % (2960)------------------------------
% 1.59/1.37 % (2962)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_2852 for (2999ds/1041Mi)
% 1.59/1.38 % (2963)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/7Mi)
% 1.59/1.38 % (2963)Instruction limit reached!
% 1.59/1.38 % (2963)------------------------------
% 1.59/1.38 % (2963)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.38 % (2963)Termination reason: Unknown
% 1.59/1.38 % (2963)Termination phase: Saturation
% 1.59/1.38
% 1.59/1.38 % (2963)Memory used [KB]: 1023
% 1.59/1.38 % (2963)Time elapsed: 0.006 s
% 1.59/1.38 % (2963)Instructions burned: 8 (million)
% 1.59/1.38 % (2963)------------------------------
% 1.59/1.38 % (2963)------------------------------
% 1.59/1.38 % (2964)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/16Mi)
% 1.59/1.38 % (2965)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_2852 for (2999ds/3Mi)
% 1.59/1.38 % (2966)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_2852 for (2999ds/3Mi)
% 1.59/1.39 % (2959)Instruction limit reached!
% 1.59/1.39 % (2959)------------------------------
% 1.59/1.39 % (2959)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.39 % (2959)Termination reason: Unknown
% 1.59/1.39 % (2959)Termination phase: Saturation
% 1.59/1.39 % (2965)Instruction limit reached!
% 1.59/1.39 % (2965)------------------------------
% 1.59/1.39 % (2965)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.39 % (2965)Termination reason: Unknown
% 1.59/1.39 % (2965)Termination phase: Saturation
% 1.59/1.39
% 1.59/1.39 % (2965)Memory used [KB]: 5500
% 1.59/1.39 % (2965)Time elapsed: 0.003 s
% 1.59/1.39 % (2965)Instructions burned: 3 (million)
% 1.59/1.39 % (2965)------------------------------
% 1.59/1.39 % (2965)------------------------------
% 1.59/1.39
% 1.59/1.39 % (2959)Memory used [KB]: 5628
% 1.59/1.39 % (2959)Time elapsed: 0.021 s
% 1.59/1.39 % (2959)Instructions burned: 38 (million)
% 1.59/1.39 % (2959)------------------------------
% 1.59/1.39 % (2959)------------------------------
% 1.59/1.39 % (2966)Instruction limit reached!
% 1.59/1.39 % (2966)------------------------------
% 1.59/1.39 % (2966)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.39 % (2966)Termination reason: Unknown
% 1.59/1.39 % (2966)Termination phase: Saturation
% 1.59/1.39
% 1.59/1.39 % (2966)Memory used [KB]: 1023
% 1.59/1.39 % (2966)Time elapsed: 0.003 s
% 1.59/1.39 % (2966)Instructions burned: 3 (million)
% 1.59/1.39 % (2966)------------------------------
% 1.59/1.39 % (2966)------------------------------
% 1.59/1.39 % (2964)Instruction limit reached!
% 1.59/1.39 % (2964)------------------------------
% 1.59/1.39 % (2964)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.59/1.39 % (2964)Termination reason: Unknown
% 1.59/1.39 % (2964)Termination phase: Saturation
% 1.59/1.39
% 1.59/1.39 % (2964)Memory used [KB]: 5628
% 1.59/1.39 % (2964)Time elapsed: 0.011 s
% 1.59/1.39 % (2964)Instructions burned: 17 (million)
% 1.59/1.39 % (2964)------------------------------
% 1.59/1.39 % (2964)------------------------------
% 1.65/1.40 % (2967)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/7Mi)
% 1.65/1.40 % (2967)Refutation not found, incomplete strategy
% 1.65/1.40 % (2967)------------------------------
% 1.65/1.40 % (2967)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.40 % (2967)Termination reason: Refutation not found, incomplete strategy
% 1.65/1.40
% 1.65/1.40
% 1.65/1.40 % (2967)Memory used [KB]: 5500
% 1.65/1.40 % (2967)Time elapsed: 0.003 s
% 1.65/1.40 % (2967)Instructions burned: 3 (million)
% 1.65/1.40 % (2967)------------------------------
% 1.65/1.40 % (2967)------------------------------
% 1.65/1.40 % (2968)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/3Mi)
% 1.65/1.40 % (2969)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/4Mi)
% 1.65/1.40 % (2970)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/18Mi)
% 1.65/1.40 % (2968)Instruction limit reached!
% 1.65/1.40 % (2968)------------------------------
% 1.65/1.40 % (2968)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.40 % (2968)Termination reason: Unknown
% 1.65/1.40 % (2968)Termination phase: Saturation
% 1.65/1.40
% 1.65/1.40 % (2968)Memory used [KB]: 5500
% 1.65/1.40 % (2968)Time elapsed: 0.003 s
% 1.65/1.40 % (2968)Instructions burned: 3 (million)
% 1.65/1.40 % (2968)------------------------------
% 1.65/1.40 % (2968)------------------------------
% 1.65/1.40 % (2969)Instruction limit reached!
% 1.65/1.40 % (2969)------------------------------
% 1.65/1.40 % (2969)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.40 % (2969)Termination reason: Unknown
% 1.65/1.40 % (2969)Termination phase: Saturation
% 1.65/1.40
% 1.65/1.40 % (2969)Memory used [KB]: 5500
% 1.65/1.40 % (2969)Time elapsed: 0.004 s
% 1.65/1.40 % (2969)Instructions burned: 5 (million)
% 1.65/1.40 % (2969)------------------------------
% 1.65/1.40 % (2969)------------------------------
% 1.65/1.41 % (2971)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/710Mi)
% 1.65/1.41 % (2970)Instruction limit reached!
% 1.65/1.41 % (2970)------------------------------
% 1.65/1.41 % (2970)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.41 % (2970)Termination reason: Unknown
% 1.65/1.41 % (2970)Termination phase: Saturation
% 1.65/1.41
% 1.65/1.41 % (2970)Memory used [KB]: 5500
% 1.65/1.41 % (2970)Time elapsed: 0.011 s
% 1.65/1.41 % (2970)Instructions burned: 19 (million)
% 1.65/1.41 % (2970)------------------------------
% 1.65/1.41 % (2970)------------------------------
% 1.65/1.42 % (2972)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/6Mi)
% 1.65/1.42 % (2973)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_2852 for (2999ds/902Mi)
% 1.65/1.42 % (2974)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_2852 for (2999ds/21Mi)
% 1.65/1.42 % (2973)Refutation not found, incomplete strategy
% 1.65/1.42 % (2973)------------------------------
% 1.65/1.42 % (2973)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.42 % (2973)Termination reason: Refutation not found, incomplete strategy
% 1.65/1.42
% 1.65/1.42
% 1.65/1.42 % (2973)Memory used [KB]: 5500
% 1.65/1.42 % (2973)Time elapsed: 0.002 s
% 1.65/1.42 % (2973)Instructions burned: 2 (million)
% 1.65/1.42 % (2973)------------------------------
% 1.65/1.42 % (2973)------------------------------
% 1.65/1.42 % (2972)Instruction limit reached!
% 1.65/1.42 % (2972)------------------------------
% 1.65/1.42 % (2972)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.42 % (2972)Termination reason: Unknown
% 1.65/1.42 % (2972)Termination phase: Saturation
% 1.65/1.42
% 1.65/1.42 % (2972)Memory used [KB]: 5500
% 1.65/1.42 % (2972)Time elapsed: 0.005 s
% 1.65/1.42 % (2972)Instructions burned: 7 (million)
% 1.65/1.42 % (2972)------------------------------
% 1.65/1.42 % (2972)------------------------------
% 1.65/1.43 % (2975)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/5Mi)
% 1.65/1.43 % (2975)Instruction limit reached!
% 1.65/1.43 % (2975)------------------------------
% 1.65/1.43 % (2975)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.43 % (2975)Termination reason: Unknown
% 1.65/1.43 % (2975)Termination phase: Saturation
% 1.65/1.43
% 1.65/1.43 % (2975)Memory used [KB]: 5500
% 1.65/1.43 % (2975)Time elapsed: 0.004 s
% 1.65/1.43 % (2975)Instructions burned: 5 (million)
% 1.65/1.43 % (2975)------------------------------
% 1.65/1.43 % (2975)------------------------------
% 1.65/1.43 % (2974)Instruction limit reached!
% 1.65/1.43 % (2974)------------------------------
% 1.65/1.43 % (2974)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.43 % (2974)Termination reason: Unknown
% 1.65/1.43 % (2974)Termination phase: Saturation
% 1.65/1.43
% 1.65/1.43 % (2974)Memory used [KB]: 5628
% 1.65/1.43 % (2974)Time elapsed: 0.013 s
% 1.65/1.43 % (2974)Instructions burned: 21 (million)
% 1.65/1.43 % (2974)------------------------------
% 1.65/1.43 % (2974)------------------------------
% 1.65/1.44 % (2976)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_2852 for (2999ds/6Mi)
% 1.65/1.44 % (2977)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/377Mi)
% 1.65/1.44 % (2976)Refutation not found, incomplete strategy
% 1.65/1.44 % (2976)------------------------------
% 1.65/1.44 % (2976)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.44 % (2976)Termination reason: Refutation not found, incomplete strategy
% 1.65/1.44
% 1.65/1.44
% 1.65/1.44 % (2976)Memory used [KB]: 5500
% 1.65/1.44 % (2976)Time elapsed: 0.003 s
% 1.65/1.44 % (2976)Instructions burned: 2 (million)
% 1.65/1.44 % (2976)------------------------------
% 1.65/1.44 % (2976)------------------------------
% 1.65/1.44 % (2951)Instruction limit reached!
% 1.65/1.44 % (2951)------------------------------
% 1.65/1.44 % (2951)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.44 % (2951)Termination reason: Unknown
% 1.65/1.44 % (2951)Termination phase: Saturation
% 1.65/1.44
% 1.65/1.44 % (2951)Memory used [KB]: 6140
% 1.65/1.44 % (2951)Time elapsed: 0.092 s
% 1.65/1.44 % (2951)Instructions burned: 183 (million)
% 1.65/1.44 % (2951)------------------------------
% 1.65/1.44 % (2951)------------------------------
% 1.65/1.45 % (2978)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_2852 for (2999ds/779Mi)
% 1.65/1.45 % (2979)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_2852 for (2999ds/19Mi)
% 1.65/1.45 % (2979)Refutation not found, incomplete strategy
% 1.65/1.45 % (2979)------------------------------
% 1.65/1.45 % (2979)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.45 % (2979)Termination reason: Refutation not found, incomplete strategy
% 1.65/1.45
% 1.65/1.45
% 1.65/1.45 % (2979)Memory used [KB]: 5500
% 1.65/1.45 % (2979)Time elapsed: 0.003 s
% 1.65/1.45 % (2979)Instructions burned: 3 (million)
% 1.65/1.45 % (2979)------------------------------
% 1.65/1.45 % (2979)------------------------------
% 1.65/1.45 % (2981)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/17Mi)
% 1.65/1.45 % (2980)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_2852 for (2999ds/879Mi)
% 1.65/1.46 % (2981)Instruction limit reached!
% 1.65/1.46 % (2981)------------------------------
% 1.65/1.46 % (2981)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.46 % (2981)Termination reason: Unknown
% 1.65/1.46 % (2981)Termination phase: Saturation
% 1.65/1.46
% 1.65/1.46 % (2981)Memory used [KB]: 5500
% 1.65/1.46 % (2981)Time elapsed: 0.011 s
% 1.65/1.46 % (2981)Instructions burned: 18 (million)
% 1.65/1.46 % (2981)------------------------------
% 1.65/1.46 % (2981)------------------------------
% 1.65/1.47 % (2982)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_2852 for (2998ds/3Mi)
% 1.65/1.47 % (2982)Instruction limit reached!
% 1.65/1.47 % (2982)------------------------------
% 1.65/1.47 % (2982)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.47 % (2982)Termination reason: Unknown
% 1.65/1.47 % (2982)Termination phase: Saturation
% 1.65/1.47
% 1.65/1.47 % (2982)Memory used [KB]: 1023
% 1.65/1.47 % (2982)Time elapsed: 0.003 s
% 1.65/1.47 % (2982)Instructions burned: 3 (million)
% 1.65/1.47 % (2982)------------------------------
% 1.65/1.47 % (2982)------------------------------
% 1.65/1.48 % (2983)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_2852 for (2998ds/30Mi)
% 1.65/1.48 % (2984)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_2852 for (2998ds/127Mi)
% 1.65/1.50 % (2983)Instruction limit reached!
% 1.65/1.50 % (2983)------------------------------
% 1.65/1.50 % (2983)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.50 % (2983)Termination reason: Unknown
% 1.65/1.50 % (2983)Termination phase: Saturation
% 1.65/1.50
% 1.65/1.50 % (2983)Memory used [KB]: 5628
% 1.65/1.50 % (2983)Time elapsed: 0.039 s
% 1.65/1.50 % (2983)Instructions burned: 30 (million)
% 1.65/1.50 % (2983)------------------------------
% 1.65/1.50 % (2983)------------------------------
% 1.65/1.51 % (2985)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_2852 for (2998ds/100Mi)
% 1.65/1.55 % (2984)Instruction limit reached!
% 1.65/1.55 % (2984)------------------------------
% 1.65/1.55 % (2984)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.55 % (2984)Termination reason: Unknown
% 1.65/1.55 % (2984)Termination phase: Saturation
% 1.65/1.55
% 1.65/1.55 % (2984)Memory used [KB]: 5628
% 1.65/1.55 % (2984)Time elapsed: 0.084 s
% 1.65/1.55 % (2984)Instructions burned: 128 (million)
% 1.65/1.55 % (2984)------------------------------
% 1.65/1.55 % (2984)------------------------------
% 1.65/1.56 % (2985)Instruction limit reached!
% 1.65/1.56 % (2985)------------------------------
% 1.65/1.56 % (2985)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.56 % (2985)Termination reason: Unknown
% 1.65/1.56 % (2985)Termination phase: Saturation
% 1.65/1.56
% 1.65/1.56 % (2985)Memory used [KB]: 5628
% 1.65/1.56 % (2985)Time elapsed: 0.073 s
% 1.65/1.56 % (2985)Instructions burned: 101 (million)
% 1.65/1.56 % (2985)------------------------------
% 1.65/1.56 % (2985)------------------------------
% 1.65/1.56 % (2986)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_2852 for (2997ds/3Mi)
% 1.65/1.56 % (2986)Instruction limit reached!
% 1.65/1.56 % (2986)------------------------------
% 1.65/1.56 % (2986)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.56 % (2986)Termination reason: Unknown
% 1.65/1.56 % (2986)Termination phase: Saturation
% 1.65/1.56
% 1.65/1.56 % (2986)Memory used [KB]: 5500
% 1.65/1.56 % (2986)Time elapsed: 0.004 s
% 1.65/1.56 % (2986)Instructions burned: 3 (million)
% 1.65/1.56 % (2986)------------------------------
% 1.65/1.56 % (2986)------------------------------
% 1.65/1.58 % (2987)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_2852 for (2997ds/20Mi)
% 1.65/1.58 % (2988)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_2852 for (2997ds/86Mi)
% 1.65/1.59 % (2987)Instruction limit reached!
% 1.65/1.59 % (2987)------------------------------
% 1.65/1.59 % (2987)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.59 % (2987)Termination reason: Unknown
% 1.65/1.59 % (2987)Termination phase: Saturation
% 1.65/1.59
% 1.65/1.59 % (2987)Memory used [KB]: 5500
% 1.65/1.59 % (2987)Time elapsed: 0.012 s
% 1.65/1.59 % (2987)Instructions burned: 20 (million)
% 1.65/1.59 % (2987)------------------------------
% 1.65/1.59 % (2987)------------------------------
% 1.65/1.60 % (2989)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_2852 for (2997ds/107Mi)
% 1.65/1.61 % (2977)Instruction limit reached!
% 1.65/1.61 % (2977)------------------------------
% 1.65/1.61 % (2977)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.61 % (2977)Termination reason: Unknown
% 1.65/1.61 % (2977)Termination phase: Saturation
% 1.65/1.61
% 1.65/1.61 % (2977)Memory used [KB]: 5884
% 1.65/1.61 % (2977)Time elapsed: 0.177 s
% 1.65/1.61 % (2977)Instructions burned: 378 (million)
% 1.65/1.61 % (2977)------------------------------
% 1.65/1.61 % (2977)------------------------------
% 1.65/1.62 % (2988)Instruction limit reached!
% 1.65/1.62 % (2988)------------------------------
% 1.65/1.62 % (2988)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.62 % (2988)Termination reason: Unknown
% 1.65/1.62 % (2988)Termination phase: Saturation
% 1.65/1.62
% 1.65/1.62 % (2988)Memory used [KB]: 5756
% 1.65/1.62 % (2988)Time elapsed: 0.044 s
% 1.65/1.62 % (2988)Instructions burned: 87 (million)
% 1.65/1.62 % (2988)------------------------------
% 1.65/1.62 % (2988)------------------------------
% 1.65/1.63 % (2990)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_2852 for (2997ds/39Mi)
% 1.65/1.64 % (2991)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_2852 for (2997ds/448Mi)
% 1.65/1.65 % (2990)Instruction limit reached!
% 1.65/1.65 % (2990)------------------------------
% 1.65/1.65 % (2990)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.65 % (2990)Termination reason: Unknown
% 1.65/1.65 % (2990)Termination phase: Saturation
% 1.65/1.65
% 1.65/1.65 % (2990)Memory used [KB]: 5628
% 1.65/1.65 % (2990)Time elapsed: 0.022 s
% 1.65/1.65 % (2990)Instructions burned: 40 (million)
% 1.65/1.65 % (2990)------------------------------
% 1.65/1.65 % (2990)------------------------------
% 1.65/1.66 % (2989)Instruction limit reached!
% 1.65/1.66 % (2989)------------------------------
% 1.65/1.66 % (2989)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.66 % (2989)Termination reason: Unknown
% 1.65/1.66 % (2989)Termination phase: Saturation
% 1.65/1.66
% 1.65/1.66 % (2989)Memory used [KB]: 5756
% 1.65/1.66 % (2989)Time elapsed: 0.054 s
% 1.65/1.66 % (2989)Instructions burned: 107 (million)
% 1.65/1.66 % (2989)------------------------------
% 1.65/1.66 % (2989)------------------------------
% 1.65/1.67 % (2992)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_2852 for (2996ds/46Mi)
% 1.65/1.67 % (2993)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_2852 for (2996ds/98Mi)
% 1.65/1.69 % (2992)Instruction limit reached!
% 1.65/1.69 % (2992)------------------------------
% 1.65/1.69 % (2992)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.69 % (2992)Termination reason: Unknown
% 1.65/1.69 % (2992)Termination phase: Saturation
% 1.65/1.69
% 1.65/1.69 % (2992)Memory used [KB]: 5628
% 1.65/1.69 % (2992)Time elapsed: 0.028 s
% 1.65/1.69 % (2992)Instructions burned: 47 (million)
% 1.65/1.69 % (2992)------------------------------
% 1.65/1.69 % (2992)------------------------------
% 1.65/1.71 % (2994)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_2852 for (2996ds/507Mi)
% 1.65/1.71 % (2994)Refutation not found, incomplete strategy
% 1.65/1.71 % (2994)------------------------------
% 1.65/1.71 % (2994)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.71 % (2994)Termination reason: Refutation not found, incomplete strategy
% 1.65/1.71
% 1.65/1.71
% 1.65/1.71 % (2994)Memory used [KB]: 5500
% 1.65/1.71 % (2994)Time elapsed: 0.004 s
% 1.65/1.71 % (2994)Instructions burned: 3 (million)
% 1.65/1.71 % (2994)------------------------------
% 1.65/1.71 % (2994)------------------------------
% 1.65/1.72 % (2993)Instruction limit reached!
% 1.65/1.72 % (2993)------------------------------
% 1.65/1.72 % (2993)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.72 % (2993)Termination reason: Unknown
% 1.65/1.72 % (2993)Termination phase: Saturation
% 1.65/1.72
% 1.65/1.72 % (2993)Memory used [KB]: 1151
% 1.65/1.72 % (2993)Time elapsed: 0.048 s
% 1.65/1.72 % (2993)Instructions burned: 99 (million)
% 1.65/1.72 % (2993)------------------------------
% 1.65/1.72 % (2993)------------------------------
% 1.65/1.73 % (2995)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_2852 for (2996ds/149Mi)
% 1.65/1.74 % (2996)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_2852 for (2996ds/39Mi)
% 1.65/1.74 % (2971)Instruction limit reached!
% 1.65/1.74 % (2971)------------------------------
% 1.65/1.74 % (2971)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.74 % (2971)Termination reason: Unknown
% 1.65/1.74 % (2971)Termination phase: Saturation
% 1.65/1.74
% 1.65/1.74 % (2971)Memory used [KB]: 6396
% 1.65/1.74 % (2971)Time elapsed: 0.337 s
% 1.65/1.74 % (2971)Instructions burned: 711 (million)
% 1.65/1.74 % (2971)------------------------------
% 1.65/1.74 % (2971)------------------------------
% 1.65/1.75 % (2996)Instruction limit reached!
% 1.65/1.75 % (2996)------------------------------
% 1.65/1.75 % (2996)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.75 % (2996)Termination reason: Unknown
% 1.65/1.75 % (2996)Termination phase: Saturation
% 1.65/1.75
% 1.65/1.75 % (2996)Memory used [KB]: 5628
% 1.65/1.75 % (2996)Time elapsed: 0.021 s
% 1.65/1.75 % (2996)Instructions burned: 39 (million)
% 1.65/1.75 % (2996)------------------------------
% 1.65/1.75 % (2996)------------------------------
% 1.65/1.76 % (2997)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_2852 for (2995ds/6Mi)
% 1.65/1.77 % (2997)Instruction limit reached!
% 1.65/1.77 % (2997)------------------------------
% 1.65/1.77 % (2997)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.77 % (2997)Termination reason: Unknown
% 1.65/1.77 % (2997)Termination phase: Saturation
% 1.65/1.77
% 1.65/1.77 % (2997)Memory used [KB]: 9978
% 1.65/1.77 % (2997)Time elapsed: 0.006 s
% 1.65/1.77 % (2997)Instructions burned: 7 (million)
% 1.65/1.77 % (2997)------------------------------
% 1.65/1.77 % (2997)------------------------------
% 1.65/1.77 % (2998)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_2852 for (2995ds/1087Mi)
% 1.65/1.78 % (2999)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_2852 for (2995ds/47Mi)
% 1.65/1.80 % (2995)Instruction limit reached!
% 1.65/1.80 % (2995)------------------------------
% 1.65/1.80 % (2995)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.80 % (2995)Termination reason: Unknown
% 1.65/1.80 % (2995)Termination phase: Saturation
% 1.65/1.80
% 1.65/1.80 % (2995)Memory used [KB]: 5756
% 1.65/1.80 % (2995)Time elapsed: 0.078 s
% 1.65/1.80 % (2995)Instructions burned: 150 (million)
% 1.65/1.80 % (2995)------------------------------
% 1.65/1.80 % (2995)------------------------------
% 1.65/1.80 % (2999)Instruction limit reached!
% 1.65/1.80 % (2999)------------------------------
% 1.65/1.80 % (2999)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.80 % (2999)Termination reason: Unknown
% 1.65/1.80 % (2999)Termination phase: Saturation
% 1.65/1.80
% 1.65/1.80 % (2999)Memory used [KB]: 5628
% 1.65/1.80 % (2999)Time elapsed: 0.025 s
% 1.65/1.80 % (2999)Instructions burned: 48 (million)
% 1.65/1.80 % (2999)------------------------------
% 1.65/1.80 % (2999)------------------------------
% 1.65/1.81 % (2978)Instruction limit reached!
% 1.65/1.81 % (2978)------------------------------
% 1.65/1.81 % (2978)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.81 % (2978)Termination reason: Unknown
% 1.65/1.81 % (2978)Termination phase: Saturation
% 1.65/1.81
% 1.65/1.81 % (2978)Memory used [KB]: 6140
% 1.65/1.81 % (2978)Time elapsed: 0.365 s
% 1.65/1.81 % (2978)Instructions burned: 780 (million)
% 1.65/1.81 % (2978)------------------------------
% 1.65/1.81 % (2978)------------------------------
% 1.65/1.82 % (3000)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_2852 for (2995ds/44Mi)
% 1.65/1.82 % (3001)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_2852 for (2995ds/432Mi)
% 1.65/1.83 % (3002)lrs+10_7:1_cnfonf=lazy_gen:fe=off:nwc=5.0:plsq=on:i=62:si=on:rtra=on_0 on DTF2THF_2852 for (2995ds/62Mi)
% 1.65/1.84 % (3000)Instruction limit reached!
% 1.65/1.84 % (3000)------------------------------
% 1.65/1.84 % (3000)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.84 % (3000)Termination reason: Unknown
% 1.65/1.84 % (3000)Termination phase: Saturation
% 1.65/1.84
% 1.65/1.84 % (3000)Memory used [KB]: 1151
% 1.65/1.84 % (3000)Time elapsed: 0.023 s
% 1.65/1.84 % (3000)Instructions burned: 44 (million)
% 1.65/1.84 % (3000)------------------------------
% 1.65/1.84 % (3000)------------------------------
% 1.65/1.85 % (2991)Instruction limit reached!
% 1.65/1.85 % (2991)------------------------------
% 1.65/1.85 % (2991)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.85 % (2991)Termination reason: Unknown
% 1.65/1.85 % (2991)Termination phase: Saturation
% 1.65/1.85
% 1.65/1.85 % (2991)Memory used [KB]: 5884
% 1.65/1.85 % (2991)Time elapsed: 0.208 s
% 1.65/1.85 % (2991)Instructions burned: 449 (million)
% 1.65/1.85 % (2991)------------------------------
% 1.65/1.85 % (2991)------------------------------
% 1.65/1.85 % (2980)Instruction limit reached!
% 1.65/1.85 % (2980)------------------------------
% 1.65/1.85 % (2980)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.85 % (2980)Termination reason: Unknown
% 1.65/1.85 % (2980)Termination phase: Saturation
% 1.65/1.85
% 1.65/1.85 % (2980)Memory used [KB]: 6140
% 1.65/1.85 % (2980)Time elapsed: 0.394 s
% 1.65/1.85 % (2980)Instructions burned: 879 (million)
% 1.65/1.85 % (2980)------------------------------
% 1.65/1.85 % (2980)------------------------------
% 1.65/1.85 % (3002)First to succeed.
% 1.65/1.86 % (3002)Refutation found. Thanks to Tanya!
% 1.65/1.86 % SZS status Theorem for DTF2THF_2852
% 1.65/1.86 % SZS output start Proof for DTF2THF_2852
% 1.65/1.86 thf(type_def_5, type, frac: $tType).
% 1.65/1.86 thf(type_def_6, type, nat: $tType).
% 1.65/1.86 thf(func_def_0, type, frac: $tType).
% 1.65/1.86 thf(func_def_1, type, x: frac).
% 1.65/1.86 thf(func_def_2, type, y: frac).
% 1.65/1.86 thf(func_def_3, type, z: frac).
% 1.65/1.86 thf(func_def_4, type, nat: $tType).
% 1.65/1.86 thf(func_def_5, type, ts: nat > nat > nat).
% 1.65/1.86 thf(func_def_6, type, num: frac > nat).
% 1.65/1.86 thf(func_def_7, type, den: frac > nat).
% 1.65/1.86 thf(func_def_20, type, ph1: !>[X0: $tType]:(X0)).
% 1.65/1.86 thf(f152,plain,(
% 1.65/1.86 $false),
% 1.65/1.86 inference(trivial_inequality_removal,[status(thm)],[f151])).
% 1.65/1.86 thf(f151,plain,(
% 1.65/1.86 ($false = $true)),
% 1.65/1.86 inference(boolean_simplification,[status(thm)],[f150])).
% 1.65/1.86 thf(f150,plain,(
% 1.65/1.86 ($true = (~ $true))),
% 1.65/1.86 inference(boolean_simplification,[status(thm)],[f149])).
% 1.65/1.86 thf(f149,plain,(
% 1.65/1.86 ((~ ((ts @ (num @ x) @ (ts @ (num @ y) @ (den @ z))) = (ts @ (num @ x) @ (ts @ (num @ y) @ (den @ z))))) = $true)),
% 1.65/1.86 inference(forward_demodulation,[status(thm)],[f148,f23])).
% 1.65/1.86 thf(f23,plain,(
% 1.65/1.86 ((ts @ (num @ y) @ (den @ z)) = (ts @ (num @ z) @ (den @ y)))),
% 1.65/1.86 inference(cnf_transformation,[status(thm)],[f14])).
% 1.65/1.86 thf(f14,plain,(
% 1.65/1.86 ((ts @ (num @ y) @ (den @ z)) = (ts @ (num @ z) @ (den @ y)))),
% 1.65/1.86 inference(fool_elimination,[status(thm)],[f2])).
% 1.65/1.86 thf(f2,axiom,(
% 1.65/1.86 ((ts @ (num @ y) @ (den @ z)) = (ts @ (num @ z) @ (den @ y)))),
% 1.65/1.86 file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',f)).
% 1.65/1.86 thf(f148,plain,(
% 1.65/1.86 ((~ ((ts @ (num @ x) @ (ts @ (num @ y) @ (den @ z))) = (ts @ (num @ x) @ (ts @ (num @ z) @ (den @ y))))) = $true)),
% 1.65/1.86 inference(forward_demodulation,[status(thm)],[f147,f32])).
% 1.65/1.86 thf(f32,plain,(
% 1.65/1.86 ( ! [X2 : nat,X1 : nat] : (((ts @ X1 @ X2) = (ts @ X2 @ X1))) )),
% 1.65/1.86 inference(equality_proxy_clausification,[status(thm)],[f31])).
% 1.65/1.86 thf(f31,plain,(
% 1.65/1.86 ( ! [X2 : nat,X1 : nat] : ((((ts @ X2 @ X1) = (ts @ X1 @ X2)) = $true)) )),
% 1.65/1.86 inference(beta_eta_normalization,[status(thm)],[f30])).
% 1.65/1.86 thf(f30,plain,(
% 1.65/1.86 ( ! [X2 : nat,X1 : nat] : ((((^[Y0 : nat]: ((ts @ Y0 @ X1) = (ts @ X1 @ Y0))) @ X2) = $true)) )),
% 1.65/1.86 inference(pi_clausification,[status(thm)],[f29])).
% 1.65/1.86 thf(f29,plain,(
% 1.65/1.86 ( ! [X1 : nat] : (((!! @ nat @ (^[Y0 : nat]: ((ts @ Y0 @ X1) = (ts @ X1 @ Y0)))) = $true)) )),
% 1.65/1.86 inference(beta_eta_normalization,[status(thm)],[f28])).
% 1.65/1.86 thf(f28,plain,(
% 1.65/1.86 ( ! [X1 : nat] : (($true = ((^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: ((ts @ Y1 @ Y0) = (ts @ Y0 @ Y1))))) @ X1))) )),
% 1.65/1.86 inference(pi_clausification,[status(thm)],[f22])).
% 1.65/1.86 thf(f22,plain,(
% 1.65/1.86 ((!! @ nat @ (^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: ((ts @ Y1 @ Y0) = (ts @ Y0 @ Y1)))))) = $true)),
% 1.65/1.86 inference(cnf_transformation,[status(thm)],[f13])).
% 1.65/1.86 thf(f13,plain,(
% 1.65/1.86 ((!! @ nat @ (^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: ((ts @ Y1 @ Y0) = (ts @ Y0 @ Y1)))))) = $true)),
% 1.65/1.86 inference(fool_elimination,[status(thm)],[f12])).
% 1.65/1.86 thf(f12,plain,(
% 1.65/1.86 ! [X0 : nat,X1 : nat] : ((ts @ X0 @ X1) = (ts @ X1 @ X0))),
% 1.65/1.86 inference(rectify,[status(thm)],[f4])).
% 1.65/1.86 thf(f4,axiom,(
% 1.65/1.86 ! [X1 : nat,X0 : nat] : ((ts @ X0 @ X1) = (ts @ X1 @ X0))),
% 1.65/1.86 file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',satz29)).
% 1.65/1.86 thf(f147,plain,(
% 1.65/1.86 ((~ ((ts @ (num @ x) @ (ts @ (num @ y) @ (den @ z))) = (ts @ (num @ x) @ (ts @ (den @ y) @ (num @ z))))) = $true)),
% 1.65/1.86 inference(forward_demodulation,[status(thm)],[f140,f95])).
% 1.65/1.86 thf(f95,plain,(
% 1.65/1.86 ( ! [X2 : nat,X0 : nat,X1 : nat] : (((ts @ X0 @ (ts @ X1 @ X2)) = (ts @ X2 @ (ts @ X0 @ X1)))) )),
% 1.65/1.86 inference(superposition,[status(thm)],[f32,f63])).
% 1.65/1.86 thf(f63,plain,(
% 1.65/1.86 ( ! [X2 : nat,X3 : nat,X1 : nat] : (((ts @ X2 @ (ts @ X3 @ X1)) = (ts @ (ts @ X2 @ X3) @ X1))) )),
% 1.65/1.86 inference(equality_proxy_clausification,[status(thm)],[f62])).
% 1.65/1.86 thf(f62,plain,(
% 1.65/1.86 ( ! [X2 : nat,X3 : nat,X1 : nat] : ((((ts @ (ts @ X2 @ X3) @ X1) = (ts @ X2 @ (ts @ X3 @ X1))) = $true)) )),
% 1.65/1.86 inference(beta_eta_normalization,[status(thm)],[f61])).
% 1.65/1.86 thf(f61,plain,(
% 1.65/1.86 ( ! [X2 : nat,X3 : nat,X1 : nat] : ((((^[Y0 : nat]: ((ts @ (ts @ X2 @ Y0) @ X1) = (ts @ X2 @ (ts @ Y0 @ X1)))) @ X3) = $true)) )),
% 1.65/1.86 inference(pi_clausification,[status(thm)],[f60])).
% 1.65/1.86 thf(f60,plain,(
% 1.65/1.86 ( ! [X2 : nat,X1 : nat] : (((!! @ nat @ (^[Y0 : nat]: ((ts @ (ts @ X2 @ Y0) @ X1) = (ts @ X2 @ (ts @ Y0 @ X1))))) = $true)) )),
% 1.65/1.86 inference(beta_eta_normalization,[status(thm)],[f59])).
% 1.65/1.86 thf(f59,plain,(
% 1.65/1.86 ( ! [X2 : nat,X1 : nat] : ((((^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: ((ts @ (ts @ Y0 @ Y1) @ X1) = (ts @ Y0 @ (ts @ Y1 @ X1)))))) @ X2) = $true)) )),
% 1.65/1.86 inference(pi_clausification,[status(thm)],[f58])).
% 1.65/1.86 thf(f58,plain,(
% 1.65/1.86 ( ! [X1 : nat] : (((!! @ nat @ (^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: ((ts @ (ts @ Y0 @ Y1) @ X1) = (ts @ Y0 @ (ts @ Y1 @ X1))))))) = $true)) )),
% 1.65/1.86 inference(beta_eta_normalization,[status(thm)],[f57])).
% 1.65/1.86 thf(f57,plain,(
% 1.65/1.86 ( ! [X1 : nat] : (($true = ((^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: (!! @ nat @ (^[Y2 : nat]: ((ts @ (ts @ Y1 @ Y2) @ Y0) = (ts @ Y1 @ (ts @ Y2 @ Y0)))))))) @ X1))) )),
% 1.65/1.86 inference(pi_clausification,[status(thm)],[f19])).
% 1.65/1.86 thf(f19,plain,(
% 1.65/1.86 ($true = (!! @ nat @ (^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: (!! @ nat @ (^[Y2 : nat]: ((ts @ (ts @ Y1 @ Y2) @ Y0) = (ts @ Y1 @ (ts @ Y2 @ Y0))))))))))),
% 1.65/1.86 inference(cnf_transformation,[status(thm)],[f10])).
% 1.65/1.86 thf(f10,plain,(
% 1.65/1.86 ($true = (!! @ nat @ (^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: (!! @ nat @ (^[Y2 : nat]: ((ts @ (ts @ Y1 @ Y2) @ Y0) = (ts @ Y1 @ (ts @ Y2 @ Y0))))))))))),
% 1.65/1.86 inference(fool_elimination,[status(thm)],[f9])).
% 1.65/1.86 thf(f9,plain,(
% 1.65/1.86 ! [X0 : nat,X1 : nat,X2 : nat] : ((ts @ (ts @ X1 @ X0) @ X2) = (ts @ X1 @ (ts @ X0 @ X2)))),
% 1.65/1.86 inference(rectify,[status(thm)],[f5])).
% 1.65/1.86 thf(f5,axiom,(
% 1.65/1.86 ! [X1 : nat,X0 : nat,X2 : nat] : ((ts @ (ts @ X0 @ X1) @ X2) = (ts @ X0 @ (ts @ X1 @ X2)))),
% 1.65/1.86 file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',satz31)).
% 1.65/1.86 thf(f140,plain,(
% 1.65/1.86 ($true = (~ ((ts @ (num @ x) @ (ts @ (num @ y) @ (den @ z))) = (ts @ (num @ z) @ (ts @ (num @ x) @ (den @ y))))))),
% 1.65/1.86 inference(superposition,[status(thm)],[f138,f20])).
% 1.65/1.86 thf(f20,plain,(
% 1.65/1.86 ((ts @ (num @ x) @ (den @ y)) = (ts @ (num @ y) @ (den @ x)))),
% 1.65/1.86 inference(cnf_transformation,[status(thm)],[f11])).
% 1.65/1.86 thf(f11,plain,(
% 1.65/1.86 ((ts @ (num @ x) @ (den @ y)) = (ts @ (num @ y) @ (den @ x)))),
% 1.65/1.86 inference(fool_elimination,[status(thm)],[f1])).
% 1.65/1.86 thf(f1,axiom,(
% 1.65/1.86 ((ts @ (num @ x) @ (den @ y)) = (ts @ (num @ y) @ (den @ x)))),
% 1.65/1.86 file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',e)).
% 1.65/1.86 thf(f138,plain,(
% 1.65/1.86 ( ! [X0 : nat] : (((~ ((ts @ (num @ x) @ (ts @ X0 @ (den @ z))) = (ts @ (num @ z) @ (ts @ X0 @ (den @ x))))) = $true)) )),
% 1.65/1.86 inference(forward_demodulation,[status(thm)],[f137,f95])).
% 1.65/1.86 thf(f137,plain,(
% 1.65/1.86 ( ! [X0 : nat] : (((~ ((ts @ (num @ x) @ (ts @ X0 @ (den @ z))) = (ts @ (den @ x) @ (ts @ (num @ z) @ X0)))) = $true)) )),
% 1.65/1.86 inference(forward_demodulation,[status(thm)],[f136,f89])).
% 1.65/1.86 thf(f89,plain,(
% 1.65/1.86 ( ! [X2 : nat,X0 : nat,X1 : nat] : (((ts @ X0 @ (ts @ X1 @ X2)) = (ts @ (ts @ X1 @ X0) @ X2))) )),
% 1.65/1.86 inference(superposition,[status(thm)],[f63,f32])).
% 1.65/1.86 thf(f136,plain,(
% 1.65/1.86 ( ! [X0 : nat] : (((~ ((ts @ (num @ x) @ (ts @ X0 @ (den @ z))) = (ts @ (ts @ (num @ z) @ (den @ x)) @ X0))) = $true)) )),
% 1.65/1.86 inference(forward_demodulation,[status(thm)],[f135,f95])).
% 1.65/1.86 thf(f135,plain,(
% 1.65/1.86 ( ! [X0 : nat] : (($true = (~ ((ts @ (den @ z) @ (ts @ (num @ x) @ X0)) = (ts @ (ts @ (num @ z) @ (den @ x)) @ X0))))) )),
% 1.65/1.86 inference(forward_demodulation,[status(thm)],[f134,f89])).
% 1.65/1.86 thf(f134,plain,(
% 1.65/1.86 ( ! [X0 : nat] : (((~ ((ts @ (ts @ (num @ x) @ (den @ z)) @ X0) = (ts @ (ts @ (num @ z) @ (den @ x)) @ X0))) = $true)) )),
% 1.65/1.86 inference(boolean_simplification,[status(thm)],[f118])).
% 1.65/1.86 thf(f118,plain,(
% 1.65/1.86 ( ! [X0 : nat] : (($true = (((ts @ (ts @ (num @ x) @ (den @ z)) @ X0) = (ts @ (ts @ (num @ z) @ (den @ x)) @ X0)) => $false))) )),
% 1.65/1.86 inference(superposition,[status(thm)],[f116,f24])).
% 1.65/1.86 thf(f24,plain,(
% 1.65/1.86 (((ts @ (num @ x) @ (den @ z)) = (ts @ (num @ z) @ (den @ x))) = $false)),
% 1.65/1.86 inference(not_proxy_clausification,[status(thm)],[f18])).
% 1.65/1.86 thf(f18,plain,(
% 1.65/1.86 ((~ ((ts @ (num @ x) @ (den @ z)) = (ts @ (num @ z) @ (den @ x)))) = $true)),
% 1.65/1.86 inference(cnf_transformation,[status(thm)],[f15])).
% 1.65/1.86 thf(f15,plain,(
% 1.65/1.86 ((~ ((ts @ (num @ x) @ (den @ z)) = (ts @ (num @ z) @ (den @ x)))) = $true)),
% 1.65/1.86 inference(fool_elimination,[status(thm)],[f7])).
% 1.65/1.86 thf(f7,negated_conjecture,(
% 1.65/1.86 ~((ts @ (num @ x) @ (den @ z)) = (ts @ (num @ z) @ (den @ x)))),
% 1.65/1.86 inference(negated_conjecture,[status(cth)],[f6])).
% 1.65/1.86 thf(f6,conjecture,(
% 1.65/1.86 ((ts @ (num @ x) @ (den @ z)) = (ts @ (num @ z) @ (den @ x)))),
% 1.65/1.86 file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',satz39)).
% 1.65/1.86 thf(f116,plain,(
% 1.65/1.86 ( ! [X2 : nat,X3 : nat,X1 : nat] : (($true = (((ts @ X3 @ X2) = (ts @ X1 @ X2)) => (X3 = X1)))) )),
% 1.65/1.86 inference(beta_eta_normalization,[status(thm)],[f115])).
% 1.65/1.86 thf(f115,plain,(
% 1.65/1.86 ( ! [X2 : nat,X3 : nat,X1 : nat] : ((((^[Y0 : nat]: (((ts @ Y0 @ X2) = (ts @ X1 @ X2)) => (Y0 = X1))) @ X3) = $true)) )),
% 1.65/1.86 inference(pi_clausification,[status(thm)],[f114])).
% 1.65/1.86 thf(f114,plain,(
% 1.65/1.86 ( ! [X2 : nat,X1 : nat] : (((!! @ nat @ (^[Y0 : nat]: (((ts @ Y0 @ X2) = (ts @ X1 @ X2)) => (Y0 = X1)))) = $true)) )),
% 1.65/1.86 inference(beta_eta_normalization,[status(thm)],[f113])).
% 1.65/1.86 thf(f113,plain,(
% 1.65/1.86 ( ! [X2 : nat,X1 : nat] : ((((^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: (((ts @ Y1 @ Y0) = (ts @ X1 @ Y0)) => (Y1 = X1))))) @ X2) = $true)) )),
% 1.65/1.86 inference(pi_clausification,[status(thm)],[f112])).
% 1.65/1.86 thf(f112,plain,(
% 1.65/1.86 ( ! [X1 : nat] : (((!! @ nat @ (^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: (((ts @ Y1 @ Y0) = (ts @ X1 @ Y0)) => (Y1 = X1)))))) = $true)) )),
% 1.65/1.86 inference(beta_eta_normalization,[status(thm)],[f111])).
% 1.65/1.86 thf(f111,plain,(
% 1.65/1.86 ( ! [X1 : nat] : (($true = ((^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: (!! @ nat @ (^[Y2 : nat]: (((ts @ Y2 @ Y1) = (ts @ Y0 @ Y1)) => (Y2 = Y0))))))) @ X1))) )),
% 1.65/1.86 inference(pi_clausification,[status(thm)],[f21])).
% 1.65/1.86 thf(f21,plain,(
% 1.65/1.86 ((!! @ nat @ (^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: (!! @ nat @ (^[Y2 : nat]: (((ts @ Y2 @ Y1) = (ts @ Y0 @ Y1)) => (Y2 = Y0)))))))) = $true)),
% 1.65/1.86 inference(cnf_transformation,[status(thm)],[f17])).
% 1.65/1.86 thf(f17,plain,(
% 1.65/1.86 ((!! @ nat @ (^[Y0 : nat]: (!! @ nat @ (^[Y1 : nat]: (!! @ nat @ (^[Y2 : nat]: (((ts @ Y2 @ Y1) = (ts @ Y0 @ Y1)) => (Y2 = Y0)))))))) = $true)),
% 1.65/1.86 inference(fool_elimination,[status(thm)],[f16])).
% 1.65/1.86 thf(f16,plain,(
% 1.65/1.86 ! [X0 : nat,X1 : nat,X2 : nat] : (((ts @ X0 @ X1) = (ts @ X2 @ X1)) => (X0 = X2))),
% 1.65/1.86 inference(rectify,[status(thm)],[f3])).
% 1.65/1.86 thf(f3,axiom,(
% 1.65/1.86 ! [X1 : nat,X2 : nat,X0 : nat] : (((ts @ X0 @ X2) = (ts @ X1 @ X2)) => (X0 = X1))),
% 1.65/1.86 file('/export/starexec/sandbox/tmp/tmp.BEY8L6hb46/DTF2THF_2852.p',satz33b)).
% 1.65/1.86 % SZS output end Proof for DTF2THF_2852
% 1.65/1.86 % (3002)------------------------------
% 1.65/1.86 % (3002)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.65/1.86 % (3002)Termination reason: Refutation
% 1.65/1.86
% 1.65/1.86 % (3002)Memory used [KB]: 5756
% 1.65/1.86 % (3002)Time elapsed: 0.031 s
% 1.65/1.86 % (3002)Instructions burned: 54 (million)
% 1.65/1.86 % (3002)------------------------------
% 1.65/1.86 % (3002)------------------------------
% 1.65/1.86 % (2950)Success in time 0.518 s
%------------------------------------------------------------------------------