%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : DAT387^1 : TPTP v9.2.1. Released v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n031.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:45:37 AM UTC 2026
% Result : Theorem 1.83s 1.89s
% Output : Refutation 1.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 7
% Syntax : Number of formulae : 93 ( 54 unt; 0 typ; 0 def)
% Number of atoms : 471 ( 137 equ; 0 cnn)
% Maximal formula atoms : 4 ( 5 avg)
% Number of connectives : 1474 ( 4 ~; 43 |; 9 &;1264 @)
% ( 2 <=>; 75 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 56 ( 56 >; 0 *; 0 +; 0 <<)
% Number of symbols : 25 ( 21 usr; 7 con; 0-4 aty)
% ( 77 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 233 ( 92 ^; 141 !; 0 ?; 233 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_6,type,
elem: $tType ).
thf(type_def_7,type,
nat: $tType ).
thf(type_def_8,type,
list: $tType ).
thf(func_def_0,type,
isPer:
!>[X0: $tType] : ( ( X0 > X0 > $o ) > $o ) ).
thf(func_def_2,type,
elem: $tType ).
thf(func_def_3,type,
elemStar: elem > elem > $o ).
thf(func_def_4,type,
nat: $tType ).
thf(func_def_5,type,
natStar: nat > nat > $o ).
thf(func_def_6,type,
zero: nat ).
thf(func_def_7,type,
suc: nat > nat ).
thf(func_def_8,type,
plus: nat > nat > nat ).
thf(func_def_9,type,
list: $tType ).
thf(func_def_10,type,
listStar: nat > list > list > $o ).
thf(func_def_11,type,
nil: list ).
thf(func_def_12,type,
cons: nat > elem > list > list ).
thf(func_def_13,type,
app: nat > nat > list > list > list ).
thf(func_def_14,type,
rev: nat > list > list ).
thf(func_def_31,type,
ph1:
!>[X0: $tType] : X0 ).
thf(func_def_32,type,
sK2: list ).
thf(func_def_33,type,
sK3: nat ).
thf(func_def_34,type,
inv_suc_4: nat > nat ).
thf(func_def_35,type,
sK5: ( nat > $o ) > nat ).
thf(func_def_36,type,
sK6:
!>[X0: $tType] : ( ( X0 > X0 > $o ) > X0 ) ).
thf(func_def_37,type,
sK7:
!>[X0: $tType] : ( ( X0 > X0 > $o ) > X0 ) ).
thf(func_def_38,type,
sK8:
!>[X0: $tType] : ( ( X0 > X0 > $o ) > X0 ) ).
thf(func_def_39,type,
sK9:
!>[X0: $tType] : ( ( X0 > X0 > $o ) > X0 ) ).
thf(func_def_40,type,
sK10:
!>[X0: $tType] : ( ( X0 > X0 > $o ) > X0 ) ).
thf(f710,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f709]) ).
thf(f709,plain,
$true = $false,
inference(backward_demodulation,[status(thm)],[f89,f704]) ).
thf(f704,plain,
( ( listStar @ sK3 @ sK2 @ sK2 )
= $false ),
inference(trivial_inequality_removal,[status(thm)],[f701]) ).
thf(f701,plain,
( ( $true = $false )
| ( ( listStar @ sK3 @ sK2 @ sK2 )
= $false ) ),
inference(superposition,[status(thm)],[f422,f686]) ).
thf(f686,plain,
( ( listStar @ sK3 @ ( rev @ sK3 @ sK2 ) @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false ),
inference(trivial_inequality_removal,[status(thm)],[f685]) ).
thf(f685,plain,
( ( $true = $false )
| ( ( listStar @ sK3 @ ( rev @ sK3 @ sK2 ) @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false ) ),
inference(forward_demodulation,[status(thm)],[f684,f89]) ).
thf(f684,plain,
( ( ( listStar @ sK3 @ sK2 @ sK2 )
= $false )
| ( ( listStar @ sK3 @ ( rev @ sK3 @ sK2 ) @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false ) ),
inference(trivial_inequality_removal,[status(thm)],[f669]) ).
thf(f669,plain,
( ( ( listStar @ sK3 @ sK2 @ sK2 )
= $false )
| ( ( listStar @ sK3 @ ( rev @ sK3 @ sK2 ) @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false )
| ( $true = $false ) ),
inference(superposition,[status(thm)],[f284,f660]) ).
thf(f660,plain,
! [X0: list] :
( ( ( listStar @ sK3 @ ( rev @ sK3 @ ( app @ zero @ sK3 @ ( rev @ zero @ nil ) @ sK2 ) ) @ X0 )
= $false )
| ( ( listStar @ sK3 @ X0 @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false ) ),
inference(trivial_inequality_removal,[status(thm)],[f659]) ).
thf(f659,plain,
! [X0: list] :
( ( ( listStar @ sK3 @ ( rev @ sK3 @ ( app @ zero @ sK3 @ ( rev @ zero @ nil ) @ sK2 ) ) @ X0 )
= $false )
| ( $true = $false )
| ( ( listStar @ sK3 @ X0 @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false ) ),
inference(forward_demodulation,[status(thm)],[f644,f81]) ).
thf(f81,plain,
! [X1: nat] :
( ( isPer @ list @ ( listStar @ X1 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f80]) ).
thf(f80,plain,
! [X1: nat] :
( $true
= ( ^ [Y0: nat] : ( isPer @ list @ ( listStar @ Y0 ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f60]) ).
thf(f60,plain,
( ( !! @ nat
@ ^ [Y0: nat] : ( isPer @ list @ ( listStar @ Y0 ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f52]) ).
thf(f52,plain,
( ( !! @ nat
@ ^ [Y0: nat] : ( isPer @ list @ ( listStar @ Y0 ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f51]) ).
thf(f51,plain,
! [X0: nat] : ( isPer @ list @ ( listStar @ X0 ) ),
inference(rectify,[status(thm)],[f4]) ).
thf(f4,axiom,
! [X5: nat] : ( isPer @ list @ ( listStar @ X5 ) ),
file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p','\'listStar\'_is_per') ).
thf(f644,plain,
! [X0: list] :
( ( ( listStar @ sK3 @ ( rev @ sK3 @ ( app @ zero @ sK3 @ ( rev @ zero @ nil ) @ sK2 ) ) @ X0 )
= $false )
| ( ( isPer @ list @ ( listStar @ sK3 ) )
= $false )
| ( ( listStar @ sK3 @ X0 @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false ) ),
inference(trivial_inequality_removal,[status(thm)],[f618]) ).
thf(f618,plain,
! [X0: list] :
( ( ( isPer @ list @ ( listStar @ sK3 ) )
= $false )
| ( ( listStar @ sK3 @ X0 @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false )
| ( ( listStar @ sK3 @ ( rev @ sK3 @ ( app @ zero @ sK3 @ ( rev @ zero @ nil ) @ sK2 ) ) @ X0 )
= $false )
| ( $true = $false ) ),
inference(superposition,[status(thm)],[f610,f96]) ).
thf(f96,plain,
( ( listStar @ sK3 @ ( rev @ sK3 @ ( app @ zero @ sK3 @ ( rev @ zero @ nil ) @ sK2 ) ) @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false ),
inference(backward_demodulation,[status(thm)],[f88,f95]) ).
thf(f95,plain,
! [X1: nat] :
( ( plus @ zero @ X1 )
= X1 ),
inference(equality_proxy_clausification,[status(thm)],[f94]) ).
thf(f94,plain,
! [X1: nat] :
( $true
= ( ( plus @ zero @ X1 )
= X1 ) ),
inference(beta_eta_normalization,[status(thm)],[f93]) ).
thf(f93,plain,
! [X1: nat] :
( $true
= ( ^ [Y0: nat] :
( ( plus @ zero @ Y0 )
= Y0 )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f70]) ).
thf(f70,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( ( plus @ zero @ Y0 )
= Y0 ) ) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
thf(f26,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( ( plus @ zero @ Y0 )
= Y0 ) ) ),
inference(fool_elimination,[status(thm)],[f25]) ).
thf(f25,plain,
! [X0: nat] :
( ( plus @ zero @ X0 )
= X0 ),
inference(rectify,[status(thm)],[f12]) ).
thf(f12,axiom,
! [X6: nat] :
( ( plus @ zero @ X6 )
= X6 ),
file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',ax1) ).
thf(f88,plain,
( ( listStar @ ( plus @ zero @ sK3 ) @ ( rev @ ( plus @ zero @ sK3 ) @ ( app @ zero @ sK3 @ ( rev @ zero @ nil ) @ sK2 ) ) @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) )
= $false ),
inference(binary_proxy_clausification,[status(thm)],[f87]) ).
thf(f87,plain,
( ( ( listStar @ sK3 @ sK2 @ sK2 )
=> ( listStar @ ( plus @ zero @ sK3 ) @ ( rev @ ( plus @ zero @ sK3 ) @ ( app @ zero @ sK3 @ ( rev @ zero @ nil ) @ sK2 ) ) @ ( app @ sK3 @ zero @ ( rev @ sK3 @ sK2 ) @ nil ) ) )
= $false ),
inference(beta_eta_normalization,[status(thm)],[f86]) ).
thf(f86,plain,
( ( ^ [Y0: nat] :
( ( listStar @ Y0 @ sK2 @ sK2 )
=> ( listStar @ ( plus @ zero @ Y0 ) @ ( rev @ ( plus @ zero @ Y0 ) @ ( app @ zero @ Y0 @ ( rev @ zero @ nil ) @ sK2 ) ) @ ( app @ Y0 @ zero @ ( rev @ Y0 @ sK2 ) @ nil ) ) )
@ sK3 )
= $false ),
inference(sigma_clausification,[status(thm)],[f79]) ).
thf(f79,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( listStar @ Y0 @ sK2 @ sK2 )
=> ( listStar @ ( plus @ zero @ Y0 ) @ ( rev @ ( plus @ zero @ Y0 ) @ ( app @ zero @ Y0 @ ( rev @ zero @ nil ) @ sK2 ) ) @ ( app @ Y0 @ zero @ ( rev @ Y0 @ sK2 ) @ nil ) ) ) )
= $false ),
inference(beta_eta_normalization,[status(thm)],[f78]) ).
thf(f78,plain,
( ( ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( rev @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ ( rev @ zero @ nil ) @ Y0 ) ) @ ( app @ Y1 @ zero @ ( rev @ Y1 @ Y0 ) @ nil ) ) ) )
@ sK2 )
= $false ),
inference(sigma_clausification,[status(thm)],[f77]) ).
thf(f77,plain,
( ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( rev @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ ( rev @ zero @ nil ) @ Y0 ) ) @ ( app @ Y1 @ zero @ ( rev @ Y1 @ Y0 ) @ nil ) ) ) ) )
= $false ),
inference(not_proxy_clausification,[status(thm)],[f74]) ).
thf(f74,plain,
( $true
= ( ~ ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( rev @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ ( rev @ zero @ nil ) @ Y0 ) ) @ ( app @ Y1 @ zero @ ( rev @ Y1 @ Y0 ) @ nil ) ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f28]) ).
thf(f28,plain,
( $true
= ( ~ ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( rev @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ ( rev @ zero @ nil ) @ Y0 ) ) @ ( app @ Y1 @ zero @ ( rev @ Y1 @ Y0 ) @ nil ) ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f27]) ).
thf(f27,plain,
~ ! [X0: nat,X1: list] :
( ( listStar @ X0 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ X0 ) @ ( rev @ ( plus @ zero @ X0 ) @ ( app @ zero @ X0 @ ( rev @ zero @ nil ) @ X1 ) ) @ ( app @ X0 @ zero @ ( rev @ X0 @ X1 ) @ nil ) ) ),
inference(rectify,[status(thm)],[f19]) ).
thf(f19,negated_conjecture,
~ ! [X13: nat,X14: list] :
( ( listStar @ X13 @ X14 @ X14 )
=> ( listStar @ ( plus @ zero @ X13 ) @ ( rev @ ( plus @ zero @ X13 ) @ ( app @ zero @ X13 @ ( rev @ zero @ nil ) @ X14 ) ) @ ( app @ X13 @ zero @ ( rev @ X13 @ X14 ) @ nil ) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
thf(f18,conjecture,
! [X13: nat,X14: list] :
( ( listStar @ X13 @ X14 @ X14 )
=> ( listStar @ ( plus @ zero @ X13 ) @ ( rev @ ( plus @ zero @ X13 ) @ ( app @ zero @ X13 @ ( rev @ zero @ nil ) @ X14 ) ) @ ( app @ X13 @ zero @ ( rev @ X13 @ X14 ) @ nil ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',list_rev_invol_lem_base) ).
thf(f610,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o,X4: X0] :
( ( $true
= ( X1 @ X4 @ X2 ) )
| ( ( isPer @ X0 @ X1 )
= $false )
| ( ( X1 @ X3 @ X2 )
= $false )
| ( $false
= ( X1 @ X4 @ X3 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f609]) ).
thf(f609,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o,X4: X0] :
( ( $true
= ( ( X1 @ X3 @ X2 )
=> ( X1 @ X4 @ X2 ) ) )
| ( ( isPer @ X0 @ X1 )
= $false )
| ( $false
= ( X1 @ X4 @ X3 ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f608]) ).
thf(f608,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o,X4: X0] :
( ( $true
= ( ( X1 @ X4 @ X3 )
=> ( ( X1 @ X3 @ X2 )
=> ( X1 @ X4 @ X2 ) ) ) )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f607]) ).
thf(f607,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o,X4: X0] :
( ( ( ^ [Y0: X0] :
( ( X1 @ Y0 @ X3 )
=> ( ( X1 @ X3 @ X2 )
=> ( X1 @ Y0 @ X2 ) ) )
@ X4 )
= $true )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(pi_clausification,[status(thm)],[f606]) ).
thf(f606,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o] :
( ( $true
= ( !! @ X0
@ ^ [Y0: X0] :
( ( X1 @ Y0 @ X3 )
=> ( ( X1 @ X3 @ X2 )
=> ( X1 @ Y0 @ X2 ) ) ) ) )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f601]) ).
thf(f601,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o] :
( ( ( isPer @ X0 @ X1 )
= $false )
| ( $true
= ( ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( X1 @ Y1 @ Y0 )
=> ( ( X1 @ Y0 @ X2 )
=> ( X1 @ Y1 @ X2 ) ) ) )
@ X3 ) ) ),
inference(pi_clausification,[status(thm)],[f580]) ).
thf(f580,plain,
! [X0: $tType,X2: X0,X1: X0 > X0 > $o] :
( ( ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( X1 @ Y1 @ Y0 )
=> ( ( X1 @ Y0 @ X2 )
=> ( X1 @ Y1 @ X2 ) ) ) ) )
= $true )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f576]) ).
thf(f576,plain,
! [X0: $tType,X2: X0,X1: X0 > X0 > $o] :
( ( ( isPer @ X0 @ X1 )
= $false )
| ( $true
= ( ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( X1 @ Y2 @ Y1 )
=> ( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y2 @ Y0 ) ) ) ) )
@ X2 ) ) ),
inference(pi_clausification,[status(thm)],[f346]) ).
thf(f346,plain,
! [X0: $tType,X1: X0 > X0 > $o] :
( ( $true
= ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( X1 @ Y2 @ Y1 )
=> ( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y2 @ Y0 ) ) ) ) ) ) )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f344]) ).
thf(f344,plain,
! [X0: $tType,X1: X0 > X0 > $o] :
( ( ( isPer @ X0 @ X1 )
= $false )
| ( $true
= ( ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y0 @ Y1 ) ) ) )
& ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( X1 @ Y2 @ Y1 )
=> ( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y2 @ Y0 ) ) ) ) ) ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f342]) ).
thf(f342,plain,
! [X0: $tType,X1: X0 > X0 > $o] :
( ( isPer @ X0 @ X1 )
= ( ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y0 @ Y1 ) ) ) )
& ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( X1 @ Y2 @ Y1 )
=> ( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y2 @ Y0 ) ) ) ) ) ) ) ),
inference(binary_proxy_clausification,[status(thm)],[f341]) ).
thf(f341,plain,
! [X0: $tType,X1: X0 > X0 > $o] :
( $true
= ( ( ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y0 @ Y1 ) ) ) )
& ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( X1 @ Y2 @ Y1 )
=> ( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y2 @ Y0 ) ) ) ) ) ) )
= ( isPer @ X0 @ X1 ) ) ),
inference(beta_eta_normalization,[status(thm)],[f340]) ).
thf(f340,plain,
! [X0: $tType,X1: X0 > X0 > $o] :
( $true
= ( ^ [Y0: X0 > X0 > $o] :
( ( ( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( Y0 @ Y2 @ Y1 )
=> ( Y0 @ Y1 @ Y2 ) ) ) )
& ( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( !! @ X0
@ ^ [Y3: X0] :
( ( Y0 @ Y3 @ Y2 )
=> ( ( Y0 @ Y2 @ Y1 )
=> ( Y0 @ Y3 @ Y1 ) ) ) ) ) ) )
= ( isPer @ X0 @ Y0 ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f67]) ).
thf(f67,plain,
! [X0: $tType] :
( $true
= ( !! @ ( X0 > X0 > $o )
@ ^ [Y0: X0 > X0 > $o] :
( ( ( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( Y0 @ Y2 @ Y1 )
=> ( Y0 @ Y1 @ Y2 ) ) ) )
& ( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( !! @ X0
@ ^ [Y3: X0] :
( ( Y0 @ Y3 @ Y2 )
=> ( ( Y0 @ Y2 @ Y1 )
=> ( Y0 @ Y3 @ Y1 ) ) ) ) ) ) )
= ( isPer @ X0 @ Y0 ) ) ) ),
inference(cnf_transformation,[status(thm)],[f57]) ).
thf(f57,plain,
! [X0: $tType] :
( $true
= ( !! @ ( X0 > X0 > $o )
@ ^ [Y0: X0 > X0 > $o] :
( ( ( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( Y0 @ Y2 @ Y1 )
=> ( Y0 @ Y1 @ Y2 ) ) ) )
& ( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( !! @ X0
@ ^ [Y3: X0] :
( ( Y0 @ Y3 @ Y2 )
=> ( ( Y0 @ Y2 @ Y1 )
=> ( Y0 @ Y3 @ Y1 ) ) ) ) ) ) )
= ( isPer @ X0 @ Y0 ) ) ) ),
inference(closure,[status(thm)],[f36]) ).
thf(f36,plain,
! [X0: $tType] :
( $true
= ( !! @ ( X0 > X0 > $o )
@ ^ [Y0: X0 > X0 > $o] :
( ( ( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( ( Y0 @ Y2 @ Y1 )
=> ( Y0 @ Y1 @ Y2 ) ) ) )
& ( !! @ X0
@ ^ [Y1: X0] :
( !! @ X0
@ ^ [Y2: X0] :
( !! @ X0
@ ^ [Y3: X0] :
( ( Y0 @ Y3 @ Y2 )
=> ( ( Y0 @ Y2 @ Y1 )
=> ( Y0 @ Y3 @ Y1 ) ) ) ) ) ) )
= ( isPer @ X0 @ Y0 ) ) ) ),
inference(fool_elimination,[status(thm)],[f35]) ).
thf(f35,plain,
! [X0: $tType,X1: X0 > X0 > $o] :
( ( ! [X2: X0,X3: X0,X4: X0] :
( ( X1 @ X2 @ X3 )
=> ( ( X1 @ X3 @ X4 )
=> ( X1 @ X2 @ X4 ) ) )
& ! [X5: X0,X6: X0] :
( ( X1 @ X5 @ X6 )
=> ( X1 @ X6 @ X5 ) ) )
<=> ( isPer @ X0 @ X1 ) ),
inference(rectify,[status(thm)],[f1]) ).
thf(f1,axiom,
! [X0: $tType,X1: X0 > X0 > $o] :
( ( ! [X2: X0,X3: X0,X4: X0] :
( ( X1 @ X2 @ X3 )
=> ( ( X1 @ X3 @ X4 )
=> ( X1 @ X2 @ X4 ) ) )
& ! [X2: X0,X3: X0] :
( ( X1 @ X2 @ X3 )
=> ( X1 @ X3 @ X2 ) ) )
<=> ( isPer @ X0 @ X1 ) ),
file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',is_per) ).
thf(f284,plain,
! [X2: nat,X1: list] :
( ( $true
= ( listStar @ X2 @ ( rev @ X2 @ ( app @ zero @ X2 @ ( rev @ zero @ nil ) @ X1 ) ) @ ( rev @ X2 @ X1 ) ) )
| ( ( listStar @ X2 @ X1 @ X1 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f283]) ).
thf(f283,plain,
! [X2: nat,X1: list] :
( ( ( listStar @ X2 @ X1 @ X1 )
=> ( listStar @ X2 @ ( rev @ X2 @ ( app @ zero @ X2 @ ( rev @ zero @ nil ) @ X1 ) ) @ ( rev @ X2 @ X1 ) ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f282,f95]) ).
thf(f282,plain,
! [X2: nat,X1: list] :
( $true
= ( ( listStar @ X2 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ X2 ) @ ( rev @ ( plus @ zero @ X2 ) @ ( app @ zero @ X2 @ ( rev @ zero @ nil ) @ X1 ) ) @ ( rev @ X2 @ X1 ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f281]) ).
thf(f281,plain,
! [X2: nat,X1: list] :
( $true
= ( ^ [Y0: nat] :
( ( listStar @ Y0 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ Y0 ) @ ( rev @ ( plus @ zero @ Y0 ) @ ( app @ zero @ Y0 @ ( rev @ zero @ nil ) @ X1 ) ) @ ( rev @ Y0 @ X1 ) ) )
@ X2 ) ),
inference(pi_clausification,[status(thm)],[f232]) ).
thf(f232,plain,
! [X1: list] :
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( ( listStar @ Y0 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ Y0 ) @ ( rev @ ( plus @ zero @ Y0 ) @ ( app @ zero @ Y0 @ ( rev @ zero @ nil ) @ X1 ) ) @ ( rev @ Y0 @ X1 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f231]) ).
thf(f231,plain,
! [X1: list] :
( ( ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( rev @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ ( rev @ zero @ nil ) @ Y0 ) ) @ ( rev @ Y1 @ Y0 ) ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f58]) ).
thf(f58,plain,
( $true
= ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( rev @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ ( rev @ zero @ nil ) @ Y0 ) ) @ ( rev @ Y1 @ Y0 ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
thf(f22,plain,
( $true
= ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( rev @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ ( rev @ zero @ nil ) @ Y0 ) ) @ ( rev @ Y1 @ Y0 ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f21]) ).
thf(f21,plain,
! [X0: nat,X1: list] :
( ( listStar @ X0 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ X0 ) @ ( rev @ ( plus @ zero @ X0 ) @ ( app @ zero @ X0 @ ( rev @ zero @ nil ) @ X1 ) ) @ ( rev @ X0 @ X1 ) ) ),
inference(rectify,[status(thm)],[f16]) ).
thf(f16,axiom,
! [X13: nat,X14: list] :
( ( listStar @ X13 @ X14 @ X14 )
=> ( listStar @ ( plus @ zero @ X13 ) @ ( rev @ ( plus @ zero @ X13 ) @ ( app @ zero @ X13 @ ( rev @ zero @ nil ) @ X14 ) ) @ ( rev @ X13 @ X14 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',list_rev_invol_lem_base_step1) ).
thf(f422,plain,
! [X0: nat,X1: list] :
( ( $true
= ( listStar @ X0 @ ( rev @ X0 @ X1 ) @ ( app @ X0 @ zero @ ( rev @ X0 @ X1 ) @ nil ) ) )
| ( $false
= ( listStar @ X0 @ X1 @ X1 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f421]) ).
thf(f421,plain,
! [X0: nat,X1: list] :
( ( $true = $false )
| ( $true
= ( listStar @ X0 @ ( rev @ X0 @ X1 ) @ ( app @ X0 @ zero @ ( rev @ X0 @ X1 ) @ nil ) ) )
| ( $false
= ( listStar @ X0 @ X1 @ X1 ) ) ),
inference(forward_demodulation,[status(thm)],[f403,f81]) ).
thf(f403,plain,
! [X0: nat,X1: list] :
( ( $true
= ( listStar @ X0 @ ( rev @ X0 @ X1 ) @ ( app @ X0 @ zero @ ( rev @ X0 @ X1 ) @ nil ) ) )
| ( ( isPer @ list @ ( listStar @ X0 ) )
= $false )
| ( $false
= ( listStar @ X0 @ X1 @ X1 ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f381]) ).
thf(f381,plain,
! [X0: nat,X1: list] :
( ( ( isPer @ list @ ( listStar @ X0 ) )
= $false )
| ( $false
= ( listStar @ X0 @ X1 @ X1 ) )
| ( $true = $false )
| ( $true
= ( listStar @ X0 @ ( rev @ X0 @ X1 ) @ ( app @ X0 @ zero @ ( rev @ X0 @ X1 ) @ nil ) ) ) ),
inference(superposition,[status(thm)],[f173,f352]) ).
thf(f352,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o] :
( ( ( X1 @ X3 @ X2 )
= $false )
| ( ( isPer @ X0 @ X1 )
= $false )
| ( ( X1 @ X2 @ X3 )
= $true ) ),
inference(binary_proxy_clausification,[status(thm)],[f351]) ).
thf(f351,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o] :
( ( $true
= ( ( X1 @ X3 @ X2 )
=> ( X1 @ X2 @ X3 ) ) )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f350]) ).
thf(f350,plain,
! [X0: $tType,X2: X0,X3: X0,X1: X0 > X0 > $o] :
( ( $true
= ( ^ [Y0: X0] :
( ( X1 @ Y0 @ X2 )
=> ( X1 @ X2 @ Y0 ) )
@ X3 ) )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(pi_clausification,[status(thm)],[f349]) ).
thf(f349,plain,
! [X0: $tType,X2: X0,X1: X0 > X0 > $o] :
( ( $true
= ( !! @ X0
@ ^ [Y0: X0] :
( ( X1 @ Y0 @ X2 )
=> ( X1 @ X2 @ Y0 ) ) ) )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(beta_eta_normalization,[status(thm)],[f348]) ).
thf(f348,plain,
! [X0: $tType,X2: X0,X1: X0 > X0 > $o] :
( ( ( isPer @ X0 @ X1 )
= $false )
| ( $true
= ( ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y0 @ Y1 ) ) )
@ X2 ) ) ),
inference(pi_clausification,[status(thm)],[f347]) ).
thf(f347,plain,
! [X0: $tType,X1: X0 > X0 > $o] :
( ( $true
= ( !! @ X0
@ ^ [Y0: X0] :
( !! @ X0
@ ^ [Y1: X0] :
( ( X1 @ Y1 @ Y0 )
=> ( X1 @ Y0 @ Y1 ) ) ) ) )
| ( ( isPer @ X0 @ X1 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f344]) ).
thf(f173,plain,
! [X2: nat,X1: list] :
( ( ( listStar @ X2 @ ( app @ X2 @ zero @ ( rev @ X2 @ X1 ) @ nil ) @ ( rev @ X2 @ X1 ) )
= $true )
| ( ( listStar @ X2 @ X1 @ X1 )
= $false ) ),
inference(binary_proxy_clausification,[status(thm)],[f172]) ).
thf(f172,plain,
! [X2: nat,X1: list] :
( ( ( listStar @ X2 @ X1 @ X1 )
=> ( listStar @ X2 @ ( app @ X2 @ zero @ ( rev @ X2 @ X1 ) @ nil ) @ ( rev @ X2 @ X1 ) ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f171,f92]) ).
thf(f92,plain,
! [X1: nat] :
( ( plus @ X1 @ zero )
= X1 ),
inference(equality_proxy_clausification,[status(thm)],[f91]) ).
thf(f91,plain,
! [X1: nat] :
( $true
= ( ( plus @ X1 @ zero )
= X1 ) ),
inference(beta_eta_normalization,[status(thm)],[f90]) ).
thf(f90,plain,
! [X1: nat] :
( $true
= ( ^ [Y0: nat] :
( ( plus @ Y0 @ zero )
= Y0 )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f62]) ).
thf(f62,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( ( plus @ Y0 @ zero )
= Y0 ) ) ),
inference(cnf_transformation,[status(thm)],[f40]) ).
thf(f40,plain,
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( ( plus @ Y0 @ zero )
= Y0 ) ) ),
inference(fool_elimination,[status(thm)],[f39]) ).
thf(f39,plain,
! [X0: nat] :
( ( plus @ X0 @ zero )
= X0 ),
inference(rectify,[status(thm)],[f14]) ).
thf(f14,axiom,
! [X10: nat] :
( ( plus @ X10 @ zero )
= X10 ),
file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',plus_zero_r) ).
thf(f171,plain,
! [X2: nat,X1: list] :
( $true
= ( ( listStar @ X2 @ X1 @ X1 )
=> ( listStar @ ( plus @ X2 @ zero ) @ ( app @ X2 @ zero @ ( rev @ X2 @ X1 ) @ nil ) @ ( rev @ X2 @ X1 ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f170]) ).
thf(f170,plain,
! [X2: nat,X1: list] :
( $true
= ( ^ [Y0: nat] :
( ( listStar @ Y0 @ X1 @ X1 )
=> ( listStar @ ( plus @ Y0 @ zero ) @ ( app @ Y0 @ zero @ ( rev @ Y0 @ X1 ) @ nil ) @ ( rev @ Y0 @ X1 ) ) )
@ X2 ) ),
inference(pi_clausification,[status(thm)],[f150]) ).
thf(f150,plain,
! [X1: list] :
( $true
= ( !! @ nat
@ ^ [Y0: nat] :
( ( listStar @ Y0 @ X1 @ X1 )
=> ( listStar @ ( plus @ Y0 @ zero ) @ ( app @ Y0 @ zero @ ( rev @ Y0 @ X1 ) @ nil ) @ ( rev @ Y0 @ X1 ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f149]) ).
thf(f149,plain,
! [X1: list] :
( $true
= ( ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ Y1 @ zero ) @ ( app @ Y1 @ zero @ ( rev @ Y1 @ Y0 ) @ nil ) @ ( rev @ Y1 @ Y0 ) ) ) )
@ X1 ) ),
inference(pi_clausification,[status(thm)],[f72]) ).
thf(f72,plain,
( $true
= ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ Y1 @ zero ) @ ( app @ Y1 @ zero @ ( rev @ Y1 @ Y0 ) @ nil ) @ ( rev @ Y1 @ Y0 ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
thf(f44,plain,
( $true
= ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ Y1 @ zero ) @ ( app @ Y1 @ zero @ ( rev @ Y1 @ Y0 ) @ nil ) @ ( rev @ Y1 @ Y0 ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f43]) ).
thf(f43,plain,
! [X0: nat,X1: list] :
( ( listStar @ X0 @ X1 @ X1 )
=> ( listStar @ ( plus @ X0 @ zero ) @ ( app @ X0 @ zero @ ( rev @ X0 @ X1 ) @ nil ) @ ( rev @ X0 @ X1 ) ) ),
inference(rectify,[status(thm)],[f17]) ).
thf(f17,axiom,
! [X13: nat,X14: list] :
( ( listStar @ X13 @ X14 @ X14 )
=> ( listStar @ ( plus @ X13 @ zero ) @ ( app @ X13 @ zero @ ( rev @ X13 @ X14 ) @ nil ) @ ( rev @ X13 @ X14 ) ) ),
file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',list_rev_invol_lem_base_step2) ).
thf(f89,plain,
( $true
= ( listStar @ sK3 @ sK2 @ sK2 ) ),
inference(binary_proxy_clausification,[status(thm)],[f87]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : DAT387^1 : TPTP v9.2.1. Released v9.2.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.34 % Computer : n031.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue Feb 24 06:19:03 EST 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 Running /export/starexec/sandbox2/solver/bin/run_DT2H2X /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.28/0.46 ---- Original DTF file ---
% 0.28/0.47 thf(spec,logic,$$dhol).
% 0.28/0.47 %------------------------------------------------------------------------------
% 0.28/0.47 % File : DAT387^1 : TPTP v9.2.1. Released v9.2.0.
% 0.28/0.47 % Domain : Data Structures
% 0.28/0.47 % Problem : List involution lemma, base step 3
% 0.28/0.47 % Version : Especial.
% 0.28/0.47 % English : List involution lemma. The proof is by induction with a separate
% 0.28/0.47 % problem file for the base and step case (with multiple subcases)
% 0.28/0.47 % as well as the correct instantiation of the induction axiom for
% 0.28/0.47 % lists. The main file uses the conjectures of the other files as
% 0.28/0.47 % lemmas in order to prove the final result. To simplify proof
% 0.28/0.47 % search, the axioms in each problem file have been preselected.
% 0.28/0.47 % For the actual induction proof, it is sufficient to consider the
% 0.28/0.47 % "step" problem files.
% 0.28/0.47
% 0.28/0.47 % Refs : [RRB23] Rothgang et al. (2023), Theorem Proving in Dependently
% 0.28/0.47 % : [Rot25] Rothgang (2025), Email to Geoff Sutcliffe
% 0.28/0.47 % : [RK+25] Ranalter et al. (2025), The Dependently Typed Higher-O
% 0.28/0.47 % Source : [Rot25]
% 0.28/0.47 % Names : ListReversalInvolutionLemma/list-rev-invol-lem-base-step3.p [Rot25]
% 0.28/0.47
% 0.28/0.47 % Status : Theorem
% 0.28/0.47 % Rating : ? v9.2.0
% 0.28/0.47 % Syntax : Number of formulae : 20 ( 8 unt; 10 typ; 0 def)
% 0.28/0.47 % Number of atoms : 10 ( 10 equ; 0 cnn)
% 0.28/0.47 % Maximal formula atoms : 2 ( 1 avg)
% 0.28/0.47 % Number of connectives : 79 ( 3 ~; 0 |; 0 &; 72 @)
% 0.28/0.47 % ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% 0.28/0.47 % Maximal formula depth : 8 ( 3 avg)
% 0.28/0.47 % Number of types : 3 ( 2 usr)
% 0.28/0.47 % Number of type decls : 10 ( 0 !>P; 3 !>D)
% 0.28/0.47 % Number of type conns : 10 ( 10 >; 0 *; 0 +; 0 <<)
% 0.28/0.47 % Number of symbols : 9 ( 8 usr; 2 con; 0-4 aty)
% 0.28/0.47 % Number of variables : 21 ( 0 ^; 17 !; 0 ?; 21 :)
% 0.28/0.47 % ( 4 !>; 0 ?*; 0 @-; 0 @+)
% 0.28/0.47 % SPC : DH0_THM_EQU_NAR
% 0.28/0.47
% 0.28/0.47 % Comments :
% 0.28/0.47 %------------------------------------------------------------------------------
% 0.28/0.47 thf(elem_type,type,
% 0.28/0.47 elem: $tType ).
% 0.28/0.47
% 0.28/0.47 thf(nat_type,type,
% 0.28/0.47 nat: $tType ).
% 0.28/0.47
% 0.28/0.47 thf(zero_type,type,
% 0.28/0.47 zero: nat ).
% 0.28/0.47
% 0.28/0.47 thf(suc_type,type,
% 0.28/0.47 suc: nat > nat ).
% 0.28/0.47
% 0.28/0.47 thf(plus_type,type,
% 0.28/0.47 plus: nat > nat > nat ).
% 0.28/0.47
% 0.28/0.47 thf(list_type,type,
% 0.28/0.47 list: nat > $tType ).
% 0.28/0.47
% 0.28/0.47 thf(nil_type,type,
% 0.28/0.47 nil: list @ zero ).
% 0.28/0.47
% 0.28/0.47 thf(cons_type,type,
% 0.28/0.47 cons:
% 0.28/0.47 !>[N: nat] : ( elem > ( list @ N ) > ( list @ ( suc @ N ) ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(app_type,type,
% 0.28/0.47 app:
% 0.28/0.47 !>[N: nat,M: nat] : ( ( list @ N ) > ( list @ M ) > ( list @ ( plus @ N @ M ) ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(rev_type,type,
% 0.28/0.47 rev:
% 0.28/0.47 !>[N: nat] : ( ( list @ N ) > ( list @ N ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(peano1,axiom,
% 0.28/0.47 ! [N: nat] :
% 0.28/0.47 ( ( suc @ N )
% 0.28/0.47 != zero ) ).
% 0.28/0.47
% 0.28/0.47 thf(peano2,axiom,
% 0.28/0.47 ! [N: nat,M: nat] :
% 0.28/0.47 ( ( N != M )
% 0.28/0.47 => ( ( suc @ N )
% 0.28/0.47 != ( suc @ M ) ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(peano3,axiom,
% 0.28/0.47 ! [P: nat > $o] :
% 0.28/0.47 ( ( P @ zero )
% 0.28/0.47 => ( ! [M: nat] :
% 0.28/0.47 ( ( P @ M )
% 0.28/0.47 => ( P @ ( suc @ M ) ) )
% 0.28/0.47 => ! [N: nat] : ( P @ N ) ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(ax1,axiom,
% 0.28/0.47 ! [N: nat] :
% 0.28/0.47 ( ( plus @ zero @ N )
% 0.28/0.47 = N ) ).
% 0.28/0.47
% 0.28/0.47 thf(ax2,axiom,
% 0.28/0.47 ! [N: nat,M: nat] :
% 0.28/0.47 ( ( plus @ ( suc @ N ) @ M )
% 0.28/0.47 = ( suc @ ( plus @ N @ M ) ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(plus_zero_r,axiom,
% 0.28/0.47 ! [M: nat] :
% 0.28/0.47 ( ( plus @ M @ zero )
% 0.28/0.47 = M ) ).
% 0.28/0.47
% 0.28/0.47 thf(plus1r,axiom,
% 0.28/0.47 ! [N: nat] :
% 0.28/0.47 ( ( suc @ N )
% 0.28/0.47 = ( plus @ N @ ( suc @ zero ) ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(list_rev_invol_lem_base_step1,axiom,
% 0.28/0.47 ! [M2: nat,L2: list @ M2] :
% 0.28/0.47 ( ( rev @ ( plus @ zero @ M2 ) @ ( app @ zero @ M2 @ ( rev @ zero @ nil ) @ L2 ) )
% 0.28/0.47 = ( rev @ M2 @ L2 ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(list_rev_invol_lem_base_step2,axiom,
% 0.28/0.47 ! [M2: nat,L2: list @ M2] :
% 0.28/0.47 ( ( app @ M2 @ zero @ ( rev @ M2 @ L2 ) @ nil )
% 0.28/0.47 = ( rev @ M2 @ L2 ) ) ).
% 0.28/0.47
% 0.28/0.47 thf(list_rev_invol_lem_base,conjecture,
% 0.28/0.47 ! [M2: nat,L2: list @ M2] :
% 0.28/0.47 ( ( rev @ ( plus @ zero @ M2 ) @ ( app @ zero @ M2 @ ( rev @ zero @ nil ) @ L2 ) )
% 0.28/0.47 = ( app @ M2 @ zero @ ( rev @ M2 @ L2 ) @ nil ) ) ).
% 0.28/0.47
% 0.28/0.47 %------------------------------------------------------------------------------
% 0.28/0.47 ------------------------
% 1.71/1.35 ---- Embedded in THF ---
% 1.71/1.35 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.71/1.35 %%% Generated on Tue Feb 24 06:19:04 EST 2026
% 1.71/1.35 %%% using '$$dhol' embedding, version 1.3.0.
% 1.71/1.35 %%% Logic specification used:
% 1.71/1.35 %%% thf(spec, logic, $$dhol).
% 1.71/1.35
% 1.71/1.35 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2DTF10562.p
% See solution above
% 1.71/1.35 ------------------------
% 1.71/1.36 ---- Cleaned THF ---
% 1.71/1.36 thf(is_per_type,type,
% 1.71/1.36 isPer:
% 1.71/1.36 !>[A: $tType] : ( ( A > A > $o ) > $o ) ).
% 1.71/1.36
% 1.71/1.36 thf(is_per,definition,
% 1.71/1.36 ! [A: $tType,AStar: A > A > $o] :
% 1.71/1.36 ( ( isPer @ A @ AStar )
% 1.71/1.36 <=> ( ! [X: A,Y: A] :
% 1.71/1.36 ( ( AStar @ X @ Y )
% 1.71/1.36 => ( AStar @ Y @ X ) )
% 1.71/1.36 & ! [X: A,Y: A,Z: A] :
% 1.71/1.36 ( ( AStar @ X @ Y )
% 1.71/1.36 => ( ( AStar @ Y @ Z )
% 1.71/1.36 => ( AStar @ X @ Z ) ) ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(elem_type,type,
% 1.71/1.36 elem: $tType ).
% 1.71/1.36
% 1.71/1.36 thf(elemStar,type,
% 1.71/1.36 elemStar: elem > elem > $o ).
% 1.71/1.36
% 1.71/1.36 thf(elemStar_is_eq,axiom,
% 1.71/1.36 ! [X: elem,Y: elem] :
% 1.71/1.36 ( ( elemStar @ X @ Y )
% 1.71/1.36 <=> ( X = Y ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(nat_type,type,
% 1.71/1.36 nat: $tType ).
% 1.71/1.36
% 1.71/1.36 thf(natStar,type,
% 1.71/1.36 natStar: nat > nat > $o ).
% 1.71/1.36
% 1.71/1.36 thf(natStar_is_eq,axiom,
% 1.71/1.36 ! [X: nat,Y: nat] :
% 1.71/1.36 ( ( natStar @ X @ Y )
% 1.71/1.36 <=> ( X = Y ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(zero_type,type,
% 1.71/1.36 zero: nat ).
% 1.71/1.36
% 1.71/1.36 thf(suc_type,type,
% 1.71/1.36 suc: nat > nat ).
% 1.71/1.36
% 1.71/1.36 thf(plus_type,type,
% 1.71/1.36 plus: nat > nat > nat ).
% 1.71/1.36
% 1.71/1.36 thf(list_type,type,
% 1.71/1.36 list: $tType ).
% 1.71/1.36
% 1.71/1.36 thf(listStar,type,
% 1.71/1.36 listStar: nat > list > list > $o ).
% 1.71/1.36
% 1.71/1.36 thf('\'listStar\'_is_per',axiom,
% 1.71/1.36 ! [C: nat] : ( isPer @ list @ ( listStar @ C ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(nil_type,type,
% 1.71/1.36 nil: list ).
% 1.71/1.36
% 1.71/1.36 thf(nil_tp_ax,axiom,
% 1.71/1.36 listStar @ zero @ nil @ nil ).
% 1.71/1.36
% 1.71/1.36 thf(cons_type,type,
% 1.71/1.36 cons: nat > elem > list > list ).
% 1.71/1.36
% 1.71/1.36 thf(cons_tp_ax,axiom,
% 1.71/1.36 ! [N: nat,D: elem,D0: list,D0_prime: list] :
% 1.71/1.36 ( ( listStar @ N @ D0 @ D0_prime )
% 1.71/1.36 => ( listStar @ ( suc @ N ) @ ( cons @ N @ D @ D0 ) @ ( cons @ N @ D @ D0_prime ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(app_type,type,
% 1.71/1.36 app: nat > nat > list > list > list ).
% 1.71/1.36
% 1.71/1.36 thf(app_tp_ax,axiom,
% 1.71/1.36 ! [N: nat,M: nat,D: list,D_prime: list] :
% 1.71/1.36 ( ( listStar @ N @ D @ D_prime )
% 1.71/1.36 => ! [D0: list,D0_prime: list] :
% 1.71/1.36 ( ( listStar @ M @ D0 @ D0_prime )
% 1.71/1.36 => ( listStar @ ( plus @ N @ M ) @ ( app @ N @ M @ D @ D0 ) @ ( app @ N @ M @ D_prime @ D0_prime ) ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(rev_type,type,
% 1.71/1.36 rev: nat > list > list ).
% 1.71/1.36
% 1.71/1.36 thf(rev_tp_ax,axiom,
% 1.71/1.36 ! [N: nat,D: list,D_prime: list] :
% 1.71/1.36 ( ( listStar @ N @ D @ D_prime )
% 1.71/1.36 => ( listStar @ N @ ( rev @ N @ D ) @ ( rev @ N @ D_prime ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(peano1,axiom,
% 1.71/1.36 ! [N: nat] :
% 1.71/1.36 ( ( suc @ N )
% 1.71/1.36 != zero ) ).
% 1.71/1.36
% 1.71/1.36 thf(peano2,axiom,
% 1.71/1.36 ! [N: nat,M: nat] :
% 1.71/1.36 ( ( N != M )
% 1.71/1.36 => ( ( suc @ N )
% 1.71/1.36 != ( suc @ M ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(peano3,axiom,
% 1.71/1.36 ! [P: nat > $o] :
% 1.71/1.36 ( ( P @ zero )
% 1.71/1.36 => ( ! [M: nat] :
% 1.71/1.36 ( ( P @ M )
% 1.71/1.36 => ( P @ ( suc @ M ) ) )
% 1.71/1.36 => ! [N: nat] : ( P @ N ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(ax1,axiom,
% 1.71/1.36 ! [N: nat] :
% 1.71/1.36 ( ( plus @ zero @ N )
% 1.71/1.36 = N ) ).
% 1.71/1.36
% 1.71/1.36 thf(ax2,axiom,
% 1.71/1.36 ! [N: nat,M: nat] :
% 1.71/1.36 ( ( plus @ ( suc @ N ) @ M )
% 1.71/1.36 = ( suc @ ( plus @ N @ M ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(plus_zero_r,axiom,
% 1.71/1.36 ! [M: nat] :
% 1.71/1.36 ( ( plus @ M @ zero )
% 1.71/1.36 = M ) ).
% 1.71/1.36
% 1.71/1.36 thf(plus1r,axiom,
% 1.71/1.36 ! [N: nat] :
% 1.71/1.36 ( ( suc @ N )
% 1.71/1.36 = ( plus @ N @ ( suc @ zero ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(list_rev_invol_lem_base_step1,axiom,
% 1.71/1.36 ! [M2: nat,L2: list] :
% 1.71/1.36 ( ( listStar @ M2 @ L2 @ L2 )
% 1.71/1.36 => ( listStar @ ( plus @ zero @ M2 ) @ ( rev @ ( plus @ zero @ M2 ) @ ( app @ zero @ M2 @ ( rev @ zero @ nil ) @ L2 ) ) @ ( rev @ M2 @ L2 ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(list_rev_invol_lem_base_step2,axiom,
% 1.71/1.36 ! [M2: nat,L2: list] :
% 1.71/1.36 ( ( listStar @ M2 @ L2 @ L2 )
% 1.71/1.36 => ( listStar @ ( plus @ M2 @ zero ) @ ( app @ M2 @ zero @ ( rev @ M2 @ L2 ) @ nil ) @ ( rev @ M2 @ L2 ) ) ) ).
% 1.71/1.36
% 1.71/1.36 thf(list_rev_invol_lem_base,conjecture,
% 1.71/1.36 ! [M2: nat,L2: list] :
% 1.71/1.36 ( ( listStar @ M2 @ L2 @ L2 )
% 1.71/1.36 => ( listStar @ ( plus @ zero @ M2 ) @ ( rev @ ( plus @ zero @ M2 ) @ ( app @ zero @ M2 @ ( rev @ zero @ nil ) @ L2 ) ) @ ( app @ M2 @ zero @ ( rev @ M2 @ L2 ) @ nil ) ) ) ).
% 1.71/1.36 ------------------------
% 1.71/1.38 % (10828)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_10562 for (2999ds/27Mi)
% 1.71/1.38 % (10830)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_10562 for (2999ds/2Mi)
% 1.71/1.38 % (10830)Instruction limit reached!
% 1.71/1.38 % (10830)------------------------------
% 1.71/1.38 % (10830)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.71/1.38 % (10830)Termination reason: Unknown
% 1.71/1.38 % (10830)Termination phase: shuffling
% 1.71/1.38
% 1.71/1.38 % (10830)Memory used [KB]: 1023
% 1.71/1.38 % (10830)Time elapsed: 0.002 s
% 1.71/1.38 % (10830)Instructions burned: 3 (million)
% 1.71/1.38 % (10830)------------------------------
% 1.71/1.38 % (10830)------------------------------
% 1.71/1.38 % (10826)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/183Mi)
% 1.71/1.38 % (10827)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_10562 for (2999ds/4Mi)
% 1.71/1.38 % (10829)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/2Mi)
% 1.71/1.39 % (10831)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_10562 for (2999ds/275Mi)
% 1.71/1.39 % (10832)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/18Mi)
% 1.71/1.39 % (10829)Instruction limit reached!
% 1.71/1.39 % (10829)------------------------------
% 1.71/1.39 % (10829)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.71/1.39 % (10829)Termination reason: Unknown
% 1.71/1.39 % (10829)Termination phase: shuffling
% 1.71/1.39
% 1.71/1.39 % (10829)Memory used [KB]: 1023
% 1.71/1.39 % (10829)Time elapsed: 0.003 s
% 1.71/1.39 % (10829)Instructions burned: 2 (million)
% 1.71/1.39 % (10829)------------------------------
% 1.71/1.39 % (10829)------------------------------
% 1.71/1.39 % (10827)Instruction limit reached!
% 1.71/1.39 % (10827)------------------------------
% 1.71/1.39 % (10827)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.71/1.39 % (10827)Termination reason: Unknown
% 1.71/1.39 % (10827)Termination phase: Property scanning
% 1.71/1.39
% 1.71/1.39 % (10827)Memory used [KB]: 1023
% 1.71/1.39 % (10827)Time elapsed: 0.004 s
% 1.71/1.39 % (10827)Instructions burned: 4 (million)
% 1.71/1.39 % (10827)------------------------------
% 1.71/1.39 % (10827)------------------------------
% 1.71/1.39 % (10828)Instruction limit reached!
% 1.71/1.39 % (10828)------------------------------
% 1.71/1.39 % (10828)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.71/1.39 % (10828)Termination reason: Unknown
% 1.71/1.39 % (10828)Termination phase: Saturation
% 1.71/1.39
% 1.71/1.39 % (10828)Memory used [KB]: 5756
% 1.71/1.39 % (10828)Time elapsed: 0.012 s
% 1.71/1.39 % (10828)Instructions burned: 29 (million)
% 1.71/1.39 % (10828)------------------------------
% 1.71/1.39 % (10828)------------------------------
% 1.71/1.39 % (10834)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/3Mi)
% 1.71/1.39 % (10831)Refutation not found, incomplete strategy
% 1.71/1.39 % (10831)------------------------------
% 1.71/1.39 % (10831)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.71/1.39 % (10831)Termination reason: Refutation not found, incomplete strategy
% 1.71/1.39
% 1.71/1.39
% 1.71/1.39 % (10831)Memory used [KB]: 5500
% 1.71/1.39 % (10831)Time elapsed: 0.006 s
% 1.71/1.39 % (10831)Instructions burned: 6 (million)
% 1.71/1.39 % (10831)------------------------------
% 1.71/1.39 % (10831)------------------------------
% 1.71/1.39 % (10834)Instruction limit reached!
% 1.71/1.39 % (10834)------------------------------
% 1.71/1.39 % (10834)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.71/1.39 % (10834)Termination reason: Unknown
% 1.71/1.39 % (10834)Termination phase: Preprocessing 3
% 1.71/1.39
% 1.71/1.39 % (10834)Memory used [KB]: 1023
% 1.71/1.39 % (10834)Time elapsed: 0.003 s
% 1.71/1.39 % (10834)Instructions burned: 4 (million)
% 1.71/1.39 % (10834)------------------------------
% 1.71/1.39 % (10834)------------------------------
% 1.71/1.40 % (10832)Instruction limit reached!
% 1.71/1.40 % (10832)------------------------------
% 1.71/1.40 % (10832)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.71/1.40 % (10832)Termination reason: Unknown
% 1.71/1.40 % (10832)Termination phase: Saturation
% 1.71/1.40
% 1.71/1.40 % (10832)Memory used [KB]: 5628
% 1.71/1.40 % (10832)Time elapsed: 0.013 s
% 1.71/1.40 % (10832)Instructions burned: 18 (million)
% 1.71/1.40 % (10832)------------------------------
% 1.71/1.40 % (10832)------------------------------
% 1.83/1.40 % (10839)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/7Mi)
% 1.83/1.40 % (10839)Instruction limit reached!
% 1.83/1.40 % (10839)------------------------------
% 1.83/1.40 % (10839)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.40 % (10839)Termination reason: Unknown
% 1.83/1.40 % (10839)Termination phase: Saturation
% 1.83/1.40
% 1.83/1.40 % (10839)Memory used [KB]: 1023
% 1.83/1.40 % (10839)Time elapsed: 0.004 s
% 1.83/1.40 % (10839)Instructions burned: 7 (million)
% 1.83/1.40 % (10839)------------------------------
% 1.83/1.40 % (10839)------------------------------
% 1.83/1.40 % (10835)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_10562 for (2999ds/37Mi)
% 1.83/1.40 % (10836)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_10562 for (2999ds/15Mi)
% 1.83/1.41 % (10837)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_10562 for (2999ds/3Mi)
% 1.83/1.41 % (10838)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_10562 for (2999ds/1041Mi)
% 1.83/1.41 % (10837)Instruction limit reached!
% 1.83/1.41 % (10837)------------------------------
% 1.83/1.41 % (10837)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.41 % (10837)Termination reason: Unknown
% 1.83/1.41 % (10837)Termination phase: Property scanning
% 1.83/1.41
% 1.83/1.41 % (10837)Memory used [KB]: 1023
% 1.83/1.41 % (10837)Time elapsed: 0.004 s
% 1.83/1.41 % (10837)Instructions burned: 3 (million)
% 1.83/1.41 % (10837)------------------------------
% 1.83/1.41 % (10837)------------------------------
% 1.83/1.41 % (10841)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_10562 for (2999ds/3Mi)
% 1.83/1.41 % (10836)Instruction limit reached!
% 1.83/1.41 % (10836)------------------------------
% 1.83/1.41 % (10836)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.41 % (10836)Termination reason: Unknown
% 1.83/1.41 % (10836)Termination phase: Saturation
% 1.83/1.41
% 1.83/1.41 % (10836)Memory used [KB]: 5756
% 1.83/1.41 % (10836)Time elapsed: 0.011 s
% 1.83/1.41 % (10836)Instructions burned: 15 (million)
% 1.83/1.41 % (10836)------------------------------
% 1.83/1.41 % (10836)------------------------------
% 1.83/1.41 % (10841)Instruction limit reached!
% 1.83/1.41 % (10841)------------------------------
% 1.83/1.41 % (10841)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.41 % (10841)Termination reason: Unknown
% 1.83/1.41 % (10841)Termination phase: Preprocessing 3
% 1.83/1.41
% 1.83/1.41 % (10841)Memory used [KB]: 1023
% 1.83/1.41 % (10841)Time elapsed: 0.003 s
% 1.83/1.41 % (10841)Instructions burned: 4 (million)
% 1.83/1.41 % (10841)------------------------------
% 1.83/1.41 % (10841)------------------------------
% 1.83/1.41 % (10840)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/16Mi)
% 1.83/1.42 % (10840)Instruction limit reached!
% 1.83/1.42 % (10840)------------------------------
% 1.83/1.42 % (10840)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.42 % (10840)Termination reason: Unknown
% 1.83/1.42 % (10840)Termination phase: Saturation
% 1.83/1.42
% 1.83/1.42 % (10840)Memory used [KB]: 5756
% 1.83/1.42 % (10840)Time elapsed: 0.012 s
% 1.83/1.42 % (10840)Instructions burned: 16 (million)
% 1.83/1.42 % (10840)------------------------------
% 1.83/1.42 % (10840)------------------------------
% 1.83/1.42 % (10844)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/3Mi)
% 1.83/1.43 % (10844)Instruction limit reached!
% 1.83/1.43 % (10844)------------------------------
% 1.83/1.43 % (10844)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.43 % (10844)Termination reason: Unknown
% 1.83/1.43 % (10844)Termination phase: Property scanning
% 1.83/1.43
% 1.83/1.43 % (10844)Memory used [KB]: 1023
% 1.83/1.43 % (10844)Time elapsed: 0.003 s
% 1.83/1.43 % (10844)Instructions burned: 5 (million)
% 1.83/1.43 % (10844)------------------------------
% 1.83/1.43 % (10844)------------------------------
% 1.83/1.43 % (10835)Instruction limit reached!
% 1.83/1.43 % (10835)------------------------------
% 1.83/1.43 % (10835)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.43 % (10835)Termination reason: Unknown
% 1.83/1.43 % (10835)Termination phase: Saturation
% 1.83/1.43
% 1.83/1.43 % (10835)Memory used [KB]: 5884
% 1.83/1.43 % (10835)Time elapsed: 0.024 s
% 1.83/1.43 % (10835)Instructions burned: 38 (million)
% 1.83/1.43 % (10835)------------------------------
% 1.83/1.43 % (10835)------------------------------
% 1.83/1.43 % (10842)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_10562 for (2999ds/3Mi)
% 1.83/1.43 % (10842)Instruction limit reached!
% 1.83/1.43 % (10842)------------------------------
% 1.83/1.43 % (10842)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.43 % (10842)Termination reason: Unknown
% 1.83/1.43 % (10842)Termination phase: shuffling
% 1.83/1.43
% 1.83/1.43 % (10842)Memory used [KB]: 1023
% 1.83/1.43 % (10842)Time elapsed: 0.004 s
% 1.83/1.43 % (10842)Instructions burned: 4 (million)
% 1.83/1.43 % (10842)------------------------------
% 1.83/1.43 % (10842)------------------------------
% 1.83/1.43 % (10843)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/7Mi)
% 1.83/1.43 % (10843)Instruction limit reached!
% 1.83/1.43 % (10843)------------------------------
% 1.83/1.43 % (10843)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.43 % (10843)Termination reason: Unknown
% 1.83/1.43 % (10843)Termination phase: Saturation
% 1.83/1.43
% 1.83/1.43 % (10843)Memory used [KB]: 5500
% 1.83/1.43 % (10843)Time elapsed: 0.006 s
% 1.83/1.43 % (10843)Instructions burned: 7 (million)
% 1.83/1.43 % (10843)------------------------------
% 1.83/1.43 % (10843)------------------------------
% 1.83/1.44 % (10846)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/18Mi)
% 1.83/1.44 % (10847)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/710Mi)
% 1.83/1.44 % (10845)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/4Mi)
% 1.83/1.44 % (10846)Instruction limit reached!
% 1.83/1.44 % (10846)------------------------------
% 1.83/1.44 % (10846)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.44 % (10846)Termination reason: Unknown
% 1.83/1.44 % (10846)Termination phase: Saturation
% 1.83/1.44
% 1.83/1.44 % (10846)Memory used [KB]: 5628
% 1.83/1.44 % (10846)Time elapsed: 0.008 s
% 1.83/1.44 % (10846)Instructions burned: 18 (million)
% 1.83/1.44 % (10846)------------------------------
% 1.83/1.44 % (10846)------------------------------
% 1.83/1.44 % (10845)Instruction limit reached!
% 1.83/1.44 % (10845)------------------------------
% 1.83/1.44 % (10845)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.44 % (10845)Termination reason: Unknown
% 1.83/1.44 % (10845)Termination phase: Preprocessing 3
% 1.83/1.44
% 1.83/1.44 % (10845)Memory used [KB]: 1023
% 1.83/1.44 % (10845)Time elapsed: 0.004 s
% 1.83/1.44 % (10845)Instructions burned: 4 (million)
% 1.83/1.44 % (10845)------------------------------
% 1.83/1.44 % (10845)------------------------------
% 1.83/1.45 % (10848)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/6Mi)
% 1.83/1.45 % (10848)Instruction limit reached!
% 1.83/1.45 % (10848)------------------------------
% 1.83/1.45 % (10848)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.45 % (10848)Termination reason: Unknown
% 1.83/1.45 % (10848)Termination phase: Saturation
% 1.83/1.45
% 1.83/1.45 % (10848)Memory used [KB]: 5500
% 1.83/1.45 % (10848)Time elapsed: 0.006 s
% 1.83/1.45 % (10848)Instructions burned: 7 (million)
% 1.83/1.45 % (10848)------------------------------
% 1.83/1.45 % (10848)------------------------------
% 1.83/1.45 % (10850)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_10562 for (2999ds/21Mi)
% 1.83/1.45 % (10849)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_10562 for (2999ds/902Mi)
% 1.83/1.46 % (10850)Instruction limit reached!
% 1.83/1.46 % (10850)------------------------------
% 1.83/1.46 % (10850)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.46 % (10850)Termination reason: Unknown
% 1.83/1.46 % (10850)Termination phase: Saturation
% 1.83/1.46
% 1.83/1.46 % (10850)Memory used [KB]: 5756
% 1.83/1.46 % (10850)Time elapsed: 0.010 s
% 1.83/1.46 % (10850)Instructions burned: 23 (million)
% 1.83/1.46 % (10850)------------------------------
% 1.83/1.46 % (10850)------------------------------
% 1.83/1.46 % (10851)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/5Mi)
% 1.83/1.46 % (10851)Instruction limit reached!
% 1.83/1.46 % (10851)------------------------------
% 1.83/1.46 % (10851)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.46 % (10851)Termination reason: Unknown
% 1.83/1.46 % (10851)Termination phase: Property scanning
% 1.83/1.46
% 1.83/1.46 % (10851)Memory used [KB]: 1023
% 1.83/1.46 % (10851)Time elapsed: 0.004 s
% 1.83/1.46 % (10851)Instructions burned: 5 (million)
% 1.83/1.46 % (10851)------------------------------
% 1.83/1.46 % (10851)------------------------------
% 1.83/1.47 % (10852)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_10562 for (2999ds/6Mi)
% 1.83/1.47 % (10852)Instruction limit reached!
% 1.83/1.47 % (10852)------------------------------
% 1.83/1.47 % (10852)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.47 % (10852)Termination reason: Unknown
% 1.83/1.47 % (10852)Termination phase: SInE selection
% 1.83/1.47
% 1.83/1.47 % (10852)Memory used [KB]: 1023
% 1.83/1.47 % (10852)Time elapsed: 0.005 s
% 1.83/1.47 % (10852)Instructions burned: 6 (million)
% 1.83/1.47 % (10852)------------------------------
% 1.83/1.47 % (10852)------------------------------
% 1.83/1.47 % (10853)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_10562 for (2999ds/377Mi)
% 1.83/1.48 % (10854)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_10562 for (2999ds/779Mi)
% 1.83/1.49 % (10826)Instruction limit reached!
% 1.83/1.49 % (10826)------------------------------
% 1.83/1.49 % (10826)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.49 % (10826)Termination reason: Unknown
% 1.83/1.49 % (10826)Termination phase: Saturation
% 1.83/1.49
% 1.83/1.49 % (10826)Memory used [KB]: 6268
% 1.83/1.49 % (10826)Time elapsed: 0.103 s
% 1.83/1.49 % (10826)Instructions burned: 185 (million)
% 1.83/1.49 % (10826)------------------------------
% 1.83/1.49 % (10826)------------------------------
% 1.83/1.49 % (10855)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_10562 for (2999ds/19Mi)
% 1.83/1.50 % (10856)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_10562 for (2998ds/879Mi)
% 1.83/1.50 % (10855)Instruction limit reached!
% 1.83/1.50 % (10855)------------------------------
% 1.83/1.50 % (10855)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.50 % (10855)Termination reason: Unknown
% 1.83/1.50 % (10855)Termination phase: Saturation
% 1.83/1.50
% 1.83/1.50 % (10855)Memory used [KB]: 5756
% 1.83/1.50 % (10855)Time elapsed: 0.014 s
% 1.83/1.50 % (10855)Instructions burned: 20 (million)
% 1.83/1.50 % (10855)------------------------------
% 1.83/1.50 % (10855)------------------------------
% 1.83/1.52 % (10857)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_10562 for (2998ds/17Mi)
% 1.83/1.52 % (10857)Instruction limit reached!
% 1.83/1.52 % (10857)------------------------------
% 1.83/1.52 % (10857)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.52 % (10857)Termination reason: Unknown
% 1.83/1.52 % (10857)Termination phase: Saturation
% 1.83/1.52
% 1.83/1.52 % (10857)Memory used [KB]: 5756
% 1.83/1.52 % (10857)Time elapsed: 0.031 s
% 1.83/1.52 % (10857)Instructions burned: 19 (million)
% 1.83/1.52 % (10857)------------------------------
% 1.83/1.52 % (10857)------------------------------
% 1.83/1.53 % (10858)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_10562 for (2998ds/3Mi)
% 1.83/1.53 % (10858)Instruction limit reached!
% 1.83/1.53 % (10858)------------------------------
% 1.83/1.53 % (10858)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.53 % (10858)Termination reason: Unknown
% 1.83/1.53 % (10858)Termination phase: Property scanning
% 1.83/1.53
% 1.83/1.53 % (10858)Memory used [KB]: 1023
% 1.83/1.53 % (10858)Time elapsed: 0.002 s
% 1.83/1.53 % (10858)Instructions burned: 3 (million)
% 1.83/1.53 % (10858)------------------------------
% 1.83/1.53 % (10858)------------------------------
% 1.83/1.54 % (10859)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_10562 for (2998ds/30Mi)
% 1.83/1.56 % (10859)Instruction limit reached!
% 1.83/1.56 % (10859)------------------------------
% 1.83/1.56 % (10859)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.56 % (10859)Termination reason: Unknown
% 1.83/1.56 % (10859)Termination phase: Saturation
% 1.83/1.56
% 1.83/1.56 % (10859)Memory used [KB]: 5756
% 1.83/1.56 % (10859)Time elapsed: 0.034 s
% 1.83/1.56 % (10859)Instructions burned: 32 (million)
% 1.83/1.56 % (10859)------------------------------
% 1.83/1.56 % (10859)------------------------------
% 1.83/1.57 % (10860)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_10562 for (2998ds/127Mi)
% 1.83/1.60 % (10853)Instruction limit reached!
% 1.83/1.60 % (10853)------------------------------
% 1.83/1.60 % (10853)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.60 % (10853)Termination reason: Unknown
% 1.83/1.60 % (10853)Termination phase: Saturation
% 1.83/1.60
% 1.83/1.60 % (10853)Memory used [KB]: 6140
% 1.83/1.60 % (10853)Time elapsed: 0.131 s
% 1.83/1.60 % (10853)Instructions burned: 377 (million)
% 1.83/1.60 % (10853)------------------------------
% 1.83/1.60 % (10853)------------------------------
% 1.83/1.61 % (10861)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_10562 for (2997ds/100Mi)
% 1.83/1.61 % (10860)Instruction limit reached!
% 1.83/1.61 % (10860)------------------------------
% 1.83/1.61 % (10860)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.61 % (10860)Termination reason: Unknown
% 1.83/1.61 % (10860)Termination phase: Saturation
% 1.83/1.61
% 1.83/1.61 % (10860)Memory used [KB]: 6268
% 1.83/1.61 % (10860)Time elapsed: 0.067 s
% 1.83/1.61 % (10860)Instructions burned: 128 (million)
% 1.83/1.61 % (10860)------------------------------
% 1.83/1.61 % (10860)------------------------------
% 1.83/1.62 % (10862)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_10562 for (2997ds/3Mi)
% 1.83/1.62 % (10862)Instruction limit reached!
% 1.83/1.62 % (10862)------------------------------
% 1.83/1.62 % (10862)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.62 % (10862)Termination reason: Unknown
% 1.83/1.62 % (10862)Termination phase: Property scanning
% 1.83/1.62
% 1.83/1.62 % (10862)Memory used [KB]: 1023
% 1.83/1.62 % (10862)Time elapsed: 0.003 s
% 1.83/1.62 % (10862)Instructions burned: 4 (million)
% 1.83/1.62 % (10862)------------------------------
% 1.83/1.62 % (10862)------------------------------
% 1.83/1.63 % (10863)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_10562 for (2997ds/20Mi)
% 1.83/1.64 % (10863)Instruction limit reached!
% 1.83/1.64 % (10863)------------------------------
% 1.83/1.64 % (10863)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.64 % (10863)Termination reason: Unknown
% 1.83/1.64 % (10863)Termination phase: Saturation
% 1.83/1.64
% 1.83/1.64 % (10863)Memory used [KB]: 5628
% 1.83/1.64 % (10863)Time elapsed: 0.009 s
% 1.83/1.64 % (10863)Instructions burned: 20 (million)
% 1.83/1.64 % (10863)------------------------------
% 1.83/1.64 % (10863)------------------------------
% 1.83/1.64 % (10861)Instruction limit reached!
% 1.83/1.64 % (10861)------------------------------
% 1.83/1.64 % (10861)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.64 % (10861)Termination reason: Unknown
% 1.83/1.64 % (10861)Termination phase: Saturation
% 1.83/1.64
% 1.83/1.64 % (10861)Memory used [KB]: 6012
% 1.83/1.64 % (10861)Time elapsed: 0.058 s
% 1.83/1.64 % (10861)Instructions burned: 102 (million)
% 1.83/1.64 % (10861)------------------------------
% 1.83/1.64 % (10861)------------------------------
% 1.83/1.65 % (10864)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_10562 for (2997ds/86Mi)
% 1.83/1.65 % (10865)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_10562 for (2997ds/107Mi)
% 1.83/1.66 % (10847)Refutation not found, non-redundant clauses discarded% (10847)------------------------------
% 1.83/1.66 % (10847)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.66 % (10847)Termination reason: Refutation not found, non-redundant clauses discarded
% 1.83/1.66
% 1.83/1.66 % (10847)Memory used [KB]: 7803
% 1.83/1.66 % (10847)Time elapsed: 0.227 s
% 1.83/1.66 % (10847)Instructions burned: 708 (million)
% 1.83/1.66 % (10847)------------------------------
% 1.83/1.66 % (10847)------------------------------
% 1.83/1.67 % (10866)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_10562 for (2996ds/39Mi)
% 1.83/1.68 % (10864)Instruction limit reached!
% 1.83/1.68 % (10864)------------------------------
% 1.83/1.68 % (10864)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.68 % (10864)Termination reason: Unknown
% 1.83/1.68 % (10864)Termination phase: Saturation
% 1.83/1.68
% 1.83/1.68 % (10864)Memory used [KB]: 6140
% 1.83/1.68 % (10864)Time elapsed: 0.031 s
% 1.83/1.68 % (10864)Instructions burned: 88 (million)
% 1.83/1.68 % (10864)------------------------------
% 1.83/1.68 % (10864)------------------------------
% 1.83/1.69 % (10867)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_10562 for (2996ds/448Mi)
% 1.83/1.69 % (10866)Instruction limit reached!
% 1.83/1.69 % (10866)------------------------------
% 1.83/1.69 % (10866)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.69 % (10866)Termination reason: Unknown
% 1.83/1.69 % (10866)Termination phase: Saturation
% 1.83/1.69
% 1.83/1.69 % (10866)Memory used [KB]: 5756
% 1.83/1.69 % (10866)Time elapsed: 0.016 s
% 1.83/1.69 % (10866)Instructions burned: 40 (million)
% 1.83/1.69 % (10866)------------------------------
% 1.83/1.69 % (10866)------------------------------
% 1.83/1.69 % (10865)Instruction limit reached!
% 1.83/1.69 % (10865)------------------------------
% 1.83/1.69 % (10865)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.69 % (10865)Termination reason: Unknown
% 1.83/1.69 % (10865)Termination phase: Saturation
% 1.83/1.69
% 1.83/1.69 % (10865)Memory used [KB]: 6140
% 1.83/1.69 % (10865)Time elapsed: 0.039 s
% 1.83/1.69 % (10865)Instructions burned: 109 (million)
% 1.83/1.69 % (10865)------------------------------
% 1.83/1.69 % (10865)------------------------------
% 1.83/1.70 % (10868)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_10562 for (2996ds/46Mi)
% 1.83/1.70 % (10869)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_10562 for (2996ds/98Mi)
% 1.83/1.71 % (10854)Instruction limit reached!
% 1.83/1.71 % (10854)------------------------------
% 1.83/1.71 % (10854)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.71 % (10854)Termination reason: Unknown
% 1.83/1.71 % (10854)Termination phase: Saturation
% 1.83/1.71
% 1.83/1.71 % (10854)Memory used [KB]: 6908
% 1.83/1.71 % (10854)Time elapsed: 0.239 s
% 1.83/1.71 % (10854)Instructions burned: 780 (million)
% 1.83/1.71 % (10854)------------------------------
% 1.83/1.71 % (10854)------------------------------
% 1.83/1.71 % (10868)Instruction limit reached!
% 1.83/1.71 % (10868)------------------------------
% 1.83/1.71 % (10868)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.71 % (10868)Termination reason: Unknown
% 1.83/1.71 % (10868)Termination phase: Saturation
% 1.83/1.71
% 1.83/1.71 % (10868)Memory used [KB]: 5756
% 1.83/1.71 % (10868)Time elapsed: 0.019 s
% 1.83/1.71 % (10868)Instructions burned: 47 (million)
% 1.83/1.71 % (10868)------------------------------
% 1.83/1.71 % (10868)------------------------------
% 1.83/1.72 % (10870)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_10562 for (2996ds/507Mi)
% 1.83/1.73 % (10871)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_10562 for (2996ds/149Mi)
% 1.83/1.73 % (10869)Instruction limit reached!
% 1.83/1.73 % (10869)------------------------------
% 1.83/1.73 % (10869)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.73 % (10869)Termination reason: Unknown
% 1.83/1.73 % (10869)Termination phase: Saturation
% 1.83/1.73
% 1.83/1.73 % (10869)Memory used [KB]: 1535
% 1.83/1.73 % (10869)Time elapsed: 0.032 s
% 1.83/1.73 % (10869)Instructions burned: 99 (million)
% 1.83/1.73 % (10869)------------------------------
% 1.83/1.73 % (10869)------------------------------
% 1.83/1.74 % (10872)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_10562 for (2996ds/39Mi)
% 1.83/1.75 % (10872)Instruction limit reached!
% 1.83/1.75 % (10872)------------------------------
% 1.83/1.75 % (10872)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.75 % (10872)Termination reason: Unknown
% 1.83/1.75 % (10872)Termination phase: Saturation
% 1.83/1.75
% 1.83/1.75 % (10872)Memory used [KB]: 5756
% 1.83/1.75 % (10872)Time elapsed: 0.014 s
% 1.83/1.75 % (10872)Instructions burned: 39 (million)
% 1.83/1.75 % (10872)------------------------------
% 1.83/1.75 % (10872)------------------------------
% 1.83/1.76 % (10873)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_10562 for (2996ds/6Mi)
% 1.83/1.76 % (10849)Instruction limit reached!
% 1.83/1.76 % (10849)------------------------------
% 1.83/1.76 % (10849)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.76 % (10849)Termination reason: Unknown
% 1.83/1.76 % (10849)Termination phase: Saturation
% 1.83/1.76
% 1.83/1.76 % (10849)Memory used [KB]: 6524
% 1.83/1.76 % (10849)Time elapsed: 0.314 s
% 1.83/1.76 % (10849)Instructions burned: 903 (million)
% 1.83/1.76 % (10849)------------------------------
% 1.83/1.76 % (10849)------------------------------
% 1.83/1.77 % (10873)Instruction limit reached!
% 1.83/1.77 % (10873)------------------------------
% 1.83/1.77 % (10873)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.77 % (10873)Termination reason: Unknown
% 1.83/1.77 % (10873)Termination phase: Saturation
% 1.83/1.77
% 1.83/1.77 % (10873)Memory used [KB]: 9978
% 1.83/1.77 % (10873)Time elapsed: 0.003 s
% 1.83/1.77 % (10873)Instructions burned: 7 (million)
% 1.83/1.77 % (10873)------------------------------
% 1.83/1.77 % (10873)------------------------------
% 1.83/1.77 % (10874)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_10562 for (2996ds/1087Mi)
% 1.83/1.77 % (10875)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_10562 for (2996ds/47Mi)
% 1.83/1.78 % (10871)Instruction limit reached!
% 1.83/1.78 % (10871)------------------------------
% 1.83/1.78 % (10871)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.78 % (10871)Termination reason: Unknown
% 1.83/1.78 % (10871)Termination phase: Saturation
% 1.83/1.78
% 1.83/1.78 % (10871)Memory used [KB]: 6140
% 1.83/1.78 % (10871)Time elapsed: 0.052 s
% 1.83/1.78 % (10871)Instructions burned: 149 (million)
% 1.83/1.78 % (10871)------------------------------
% 1.83/1.78 % (10871)------------------------------
% 1.83/1.79 % (10876)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_10562 for (2995ds/44Mi)
% 1.83/1.79 % (10838)Instruction limit reached!
% 1.83/1.79 % (10838)------------------------------
% 1.83/1.79 % (10838)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.79 % (10838)Termination reason: Unknown
% 1.83/1.79 % (10838)Termination phase: Saturation
% 1.83/1.79
% 1.83/1.79 % (10838)Memory used [KB]: 9210
% 1.83/1.79 % (10838)Time elapsed: 0.382 s
% 1.83/1.79 % (10838)Instructions burned: 1043 (million)
% 1.83/1.79 % (10838)------------------------------
% 1.83/1.79 % (10838)------------------------------
% 1.83/1.79 % (10856)Instruction limit reached!
% 1.83/1.79 % (10856)------------------------------
% 1.83/1.79 % (10856)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.79 % (10856)Termination reason: Unknown
% 1.83/1.79 % (10856)Termination phase: Saturation
% 1.83/1.79
% 1.83/1.79 % (10856)Memory used [KB]: 7675
% 1.83/1.79 % (10856)Time elapsed: 0.294 s
% 1.83/1.79 % (10856)Instructions burned: 879 (million)
% 1.83/1.79 % (10856)------------------------------
% 1.83/1.79 % (10856)------------------------------
% 1.83/1.79 % (10875)Instruction limit reached!
% 1.83/1.79 % (10875)------------------------------
% 1.83/1.79 % (10875)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.79 % (10875)Termination reason: Unknown
% 1.83/1.79 % (10875)Termination phase: Saturation
% 1.83/1.79
% 1.83/1.79 % (10875)Memory used [KB]: 5756
% 1.83/1.79 % (10875)Time elapsed: 0.016 s
% 1.83/1.79 % (10875)Instructions burned: 47 (million)
% 1.83/1.79 % (10875)------------------------------
% 1.83/1.79 % (10875)------------------------------
% 1.83/1.80 % (10877)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_10562 for (2995ds/432Mi)
% 1.83/1.80 % (10878)lrs+10_7:1_cnfonf=lazy_gen:fe=off:nwc=5.0:plsq=on:i=62:si=on:rtra=on_0 on DTF2THF_10562 for (2995ds/62Mi)
% 1.83/1.80 % (10876)Instruction limit reached!
% 1.83/1.80 % (10876)------------------------------
% 1.83/1.80 % (10876)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.80 % (10876)Termination reason: Unknown
% 1.83/1.80 % (10876)Termination phase: Saturation
% 1.83/1.80
% 1.83/1.80 % (10876)Memory used [KB]: 1407
% 1.83/1.80 % (10876)Time elapsed: 0.015 s
% 1.83/1.80 % (10876)Instructions burned: 44 (million)
% 1.83/1.80 % (10876)------------------------------
% 1.83/1.80 % (10876)------------------------------
% 1.83/1.80 % (10879)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_10562 for (2995ds/31Mi)
% 1.83/1.81 % (10880)dis+10_1:128_hud=1:i=96:si=on:rtra=on_0 on DTF2THF_10562 for (2995ds/96Mi)
% 1.83/1.81 % (10879)Instruction limit reached!
% 1.83/1.81 % (10879)------------------------------
% 1.83/1.81 % (10879)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.81 % (10879)Termination reason: Unknown
% 1.83/1.81 % (10879)Termination phase: Saturation
% 1.83/1.81
% 1.83/1.81 % (10879)Memory used [KB]: 5756
% 1.83/1.81 % (10879)Time elapsed: 0.011 s
% 1.83/1.81 % (10879)Instructions burned: 32 (million)
% 1.83/1.81 % (10879)------------------------------
% 1.83/1.81 % (10879)------------------------------
% 1.83/1.82 % (10881)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_10562 for (2995ds/453Mi)
% 1.83/1.82 % (10878)Instruction limit reached!
% 1.83/1.82 % (10878)------------------------------
% 1.83/1.82 % (10878)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.82 % (10878)Termination reason: Unknown
% 1.83/1.82 % (10878)Termination phase: Saturation
% 1.83/1.82
% 1.83/1.82 % (10878)Memory used [KB]: 6012
% 1.83/1.82 % (10878)Time elapsed: 0.023 s
% 1.83/1.82 % (10878)Instructions burned: 63 (million)
% 1.83/1.82 % (10878)------------------------------
% 1.83/1.82 % (10878)------------------------------
% 1.83/1.83 % (10882)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_10562 for (2995ds/71Mi)
% 1.83/1.84 % (10867)Instruction limit reached!
% 1.83/1.84 % (10867)------------------------------
% 1.83/1.84 % (10867)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.84 % (10867)Termination reason: Unknown
% 1.83/1.84 % (10867)Termination phase: Saturation
% 1.83/1.84
% 1.83/1.84 % (10867)Memory used [KB]: 6908
% 1.83/1.84 % (10867)Time elapsed: 0.150 s
% 1.83/1.84 % (10867)Instructions burned: 448 (million)
% 1.83/1.84 % (10867)------------------------------
% 1.83/1.84 % (10867)------------------------------
% 1.83/1.84 % (10880)Instruction limit reached!
% 1.83/1.84 % (10880)------------------------------
% 1.83/1.84 % (10880)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.84 % (10880)Termination reason: Unknown
% 1.83/1.84 % (10880)Termination phase: Saturation
% 1.83/1.84
% 1.83/1.84 % (10880)Memory used [KB]: 6012
% 1.83/1.84 % (10880)Time elapsed: 0.031 s
% 1.83/1.84 % (10880)Instructions burned: 98 (million)
% 1.83/1.84 % (10880)------------------------------
% 1.83/1.84 % (10880)------------------------------
% 1.83/1.85 % (10883)dis+1002_1:1_bd=off:fsr=off:ntd=on:s2a=on:ss=axioms:i=83:si=on:rtra=on_0 on DTF2THF_10562 for (2995ds/83Mi)
% 1.83/1.85 % (10884)lrs+10_1:128_cnfonf=lazy_not_gen_be_off:hud=1:ins=1:i=11:si=on:rtra=on_0 on DTF2THF_10562 for (2995ds/11Mi)
% 1.83/1.85 % (10883)Refutation not found, incomplete strategy
% 1.83/1.85 % (10883)------------------------------
% 1.83/1.85 % (10883)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.85 % (10883)Termination reason: Refutation not found, incomplete strategy
% 1.83/1.85
% 1.83/1.85
% 1.83/1.85 % (10883)Memory used [KB]: 5628
% 1.83/1.85 % (10883)Time elapsed: 0.006 s
% 1.83/1.85 % (10883)Instructions burned: 12 (million)
% 1.83/1.85 % (10883)------------------------------
% 1.83/1.85 % (10883)------------------------------
% 1.83/1.85 % (10884)Instruction limit reached!
% 1.83/1.85 % (10884)------------------------------
% 1.83/1.85 % (10884)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.85 % (10884)Termination reason: Unknown
% 1.83/1.85 % (10884)Termination phase: Saturation
% 1.83/1.85
% 1.83/1.85 % (10884)Memory used [KB]: 5628
% 1.83/1.85 % (10884)Time elapsed: 0.005 s
% 1.83/1.85 % (10884)Instructions burned: 14 (million)
% 1.83/1.85 % (10884)------------------------------
% 1.83/1.85 % (10884)------------------------------
% 1.83/1.85 % (10882)Instruction limit reached!
% 1.83/1.85 % (10882)------------------------------
% 1.83/1.85 % (10882)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.85 % (10882)Termination reason: Unknown
% 1.83/1.85 % (10882)Termination phase: Saturation
% 1.83/1.85
% 1.83/1.85 % (10882)Memory used [KB]: 6012
% 1.83/1.85 % (10882)Time elapsed: 0.027 s
% 1.83/1.85 % (10882)Instructions burned: 73 (million)
% 1.83/1.85 % (10882)------------------------------
% 1.83/1.85 % (10882)------------------------------
% 1.83/1.86 % (10885)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_10562 for (2995ds/41Mi)
% 1.83/1.86 % (10886)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_10562 for (2995ds/6Mi)
% 1.83/1.86 % (10886)Instruction limit reached!
% 1.83/1.86 % (10886)------------------------------
% 1.83/1.86 % (10886)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.86 % (10886)Termination reason: Unknown
% 1.83/1.86 % (10886)Termination phase: Saturation
% 1.83/1.86
% 1.83/1.86 % (10886)Memory used [KB]: 5500
% 1.83/1.86 % (10886)Time elapsed: 0.004 s
% 1.83/1.86 % (10886)Instructions burned: 7 (million)
% 1.83/1.86 % (10886)------------------------------
% 1.83/1.86 % (10886)------------------------------
% 1.83/1.86 % (10887)dis+10_1:1_avsq=on:cnfonf=off:e2e=on:nm=32:i=150:si=on:rtra=on_0 on DTF2THF_10562 for (2995ds/150Mi)
% 1.83/1.87 % (10885)Instruction limit reached!
% 1.83/1.87 % (10885)------------------------------
% 1.83/1.87 % (10885)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.87 % (10885)Termination reason: Unknown
% 1.83/1.87 % (10885)Termination phase: Saturation
% 1.83/1.87
% 1.83/1.87 % (10885)Memory used [KB]: 5884
% 1.83/1.87 % (10885)Time elapsed: 0.014 s
% 1.83/1.87 % (10885)Instructions burned: 42 (million)
% 1.83/1.87 % (10885)------------------------------
% 1.83/1.87 % (10885)------------------------------
% 1.83/1.87 % (10888)ott+1010_1:1_au=on:s2a=on:sd=7:ss=axioms:st=1.5:i=343:si=on:rtra=on_0 on DTF2THF_10562 for (2995ds/343Mi)
% 1.83/1.88 % (10870)Instruction limit reached!
% 1.83/1.88 % (10870)------------------------------
% 1.83/1.88 % (10870)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.88 % (10870)Termination reason: Unknown
% 1.83/1.88 % (10870)Termination phase: Saturation
% 1.83/1.88
% 1.83/1.88 % (10870)Memory used [KB]: 6268
% 1.83/1.88 % (10870)Time elapsed: 0.154 s
% 1.83/1.88 % (10870)Instructions burned: 507 (million)
% 1.83/1.88 % (10870)------------------------------
% 1.83/1.88 % (10870)------------------------------
% 1.83/1.88 % (10889)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_10562 for (2995ds/109Mi)
% 1.83/1.89 % (10881)First to succeed.
% 1.83/1.89 % (10890)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_10562 for (2994ds/253Mi)
% 1.83/1.89 % (10881)Refutation found. Thanks to Tanya!
% 1.83/1.89 % SZS status Theorem for DTF2THF_10562
% 1.83/1.89 % SZS output start Proof for DTF2THF_10562
% 1.83/1.89 thf(type_def_6, type, elem: $tType).
% 1.83/1.89 thf(type_def_7, type, nat: $tType).
% 1.83/1.89 thf(type_def_8, type, list: $tType).
% 1.83/1.89 thf(func_def_0, type, isPer: !>[X0: $tType]:((X0 > X0 > $o) > $o)).
% 1.83/1.89 thf(func_def_2, type, elem: $tType).
% 1.83/1.89 thf(func_def_3, type, elemStar: elem > elem > $o).
% 1.83/1.89 thf(func_def_4, type, nat: $tType).
% 1.83/1.89 thf(func_def_5, type, natStar: nat > nat > $o).
% 1.83/1.89 thf(func_def_6, type, zero: nat).
% 1.83/1.89 thf(func_def_7, type, suc: nat > nat).
% 1.83/1.89 thf(func_def_8, type, plus: nat > nat > nat).
% 1.83/1.89 thf(func_def_9, type, list: $tType).
% 1.83/1.89 thf(func_def_10, type, listStar: nat > list > list > $o).
% 1.83/1.89 thf(func_def_11, type, nil: list).
% 1.83/1.89 thf(func_def_12, type, cons: nat > elem > list > list).
% 1.83/1.89 thf(func_def_13, type, app: nat > nat > list > list > list).
% 1.83/1.89 thf(func_def_14, type, rev: nat > list > list).
% 1.83/1.89 thf(func_def_31, type, ph1: !>[X0: $tType]:(X0)).
% 1.83/1.89 thf(func_def_32, type, sK2: list).
% 1.83/1.89 thf(func_def_33, type, sK3: nat).
% 1.83/1.89 thf(func_def_34, type, inv_suc_4: nat > nat).
% 1.83/1.89 thf(func_def_35, type, sK5: (nat > $o) > nat).
% 1.83/1.89 thf(func_def_36, type, sK6: !>[X0: $tType]:((X0 > X0 > $o) > X0)).
% 1.83/1.89 thf(func_def_37, type, sK7: !>[X0: $tType]:((X0 > X0 > $o) > X0)).
% 1.83/1.89 thf(func_def_38, type, sK8: !>[X0: $tType]:((X0 > X0 > $o) > X0)).
% 1.83/1.89 thf(func_def_39, type, sK9: !>[X0: $tType]:((X0 > X0 > $o) > X0)).
% 1.83/1.89 thf(func_def_40, type, sK10: !>[X0: $tType]:((X0 > X0 > $o) > X0)).
% 1.83/1.89 thf(f710,plain,(
% 1.83/1.89 $false),
% 1.83/1.89 inference(trivial_inequality_removal,[status(thm)],[f709])).
% 1.83/1.89 thf(f709,plain,(
% 1.83/1.89 ($true = $false)),
% 1.83/1.89 inference(backward_demodulation,[status(thm)],[f89,f704])).
% 1.83/1.89 thf(f704,plain,(
% 1.83/1.89 ((listStar @ sK3 @ sK2 @ sK2) = $false)),
% 1.83/1.89 inference(trivial_inequality_removal,[status(thm)],[f701])).
% 1.83/1.89 thf(f701,plain,(
% 1.83/1.89 ($true = $false) | ((listStar @ sK3 @ sK2 @ sK2) = $false)),
% 1.83/1.89 inference(superposition,[status(thm)],[f422,f686])).
% 1.83/1.89 thf(f686,plain,(
% 1.83/1.89 ((listStar @ sK3 @ (rev @ sK3 @ sK2) @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false)),
% 1.83/1.89 inference(trivial_inequality_removal,[status(thm)],[f685])).
% 1.83/1.89 thf(f685,plain,(
% 1.83/1.89 ($true = $false) | ((listStar @ sK3 @ (rev @ sK3 @ sK2) @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false)),
% 1.83/1.89 inference(forward_demodulation,[status(thm)],[f684,f89])).
% 1.83/1.89 thf(f684,plain,(
% 1.83/1.89 ((listStar @ sK3 @ sK2 @ sK2) = $false) | ((listStar @ sK3 @ (rev @ sK3 @ sK2) @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false)),
% 1.83/1.89 inference(trivial_inequality_removal,[status(thm)],[f669])).
% 1.83/1.89 thf(f669,plain,(
% 1.83/1.89 ((listStar @ sK3 @ sK2 @ sK2) = $false) | ((listStar @ sK3 @ (rev @ sK3 @ sK2) @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false) | ($true = $false)),
% 1.83/1.89 inference(superposition,[status(thm)],[f284,f660])).
% 1.83/1.89 thf(f660,plain,(
% 1.83/1.89 ( ! [X0 : list] : (((listStar @ sK3 @ (rev @ sK3 @ (app @ zero @ sK3 @ (rev @ zero @ nil) @ sK2)) @ X0) = $false) | ((listStar @ sK3 @ X0 @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false)) )),
% 1.83/1.89 inference(trivial_inequality_removal,[status(thm)],[f659])).
% 1.83/1.89 thf(f659,plain,(
% 1.83/1.89 ( ! [X0 : list] : (((listStar @ sK3 @ (rev @ sK3 @ (app @ zero @ sK3 @ (rev @ zero @ nil) @ sK2)) @ X0) = $false) | ($true = $false) | ((listStar @ sK3 @ X0 @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false)) )),
% 1.83/1.89 inference(forward_demodulation,[status(thm)],[f644,f81])).
% 1.83/1.89 thf(f81,plain,(
% 1.83/1.89 ( ! [X1 : nat] : (((isPer @ list @ (listStar @ X1)) = $true)) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f80])).
% 1.83/1.89 thf(f80,plain,(
% 1.83/1.89 ( ! [X1 : nat] : (($true = ((^[Y0 : nat]: (isPer @ list @ (listStar @ Y0))) @ X1))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f60])).
% 1.83/1.89 thf(f60,plain,(
% 1.83/1.89 ((!! @ nat @ (^[Y0 : nat]: (isPer @ list @ (listStar @ Y0)))) = $true)),
% 1.83/1.89 inference(cnf_transformation,[status(thm)],[f52])).
% 1.83/1.89 thf(f52,plain,(
% 1.83/1.89 ((!! @ nat @ (^[Y0 : nat]: (isPer @ list @ (listStar @ Y0)))) = $true)),
% 1.83/1.89 inference(fool_elimination,[status(thm)],[f51])).
% 1.83/1.89 thf(f51,plain,(
% 1.83/1.89 ! [X0 : nat] : (isPer @ list @ (listStar @ X0))),
% 1.83/1.89 inference(rectify,[status(thm)],[f4])).
% 1.83/1.89 thf(f4,axiom,(
% 1.83/1.89 ! [X5 : nat] : (isPer @ list @ (listStar @ X5))),
% 1.83/1.89 file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p','\'listStar\'_is_per')).
% 1.83/1.89 thf(f644,plain,(
% 1.83/1.89 ( ! [X0 : list] : (((listStar @ sK3 @ (rev @ sK3 @ (app @ zero @ sK3 @ (rev @ zero @ nil) @ sK2)) @ X0) = $false) | ((isPer @ list @ (listStar @ sK3)) = $false) | ((listStar @ sK3 @ X0 @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false)) )),
% 1.83/1.89 inference(trivial_inequality_removal,[status(thm)],[f618])).
% 1.83/1.89 thf(f618,plain,(
% 1.83/1.89 ( ! [X0 : list] : (((isPer @ list @ (listStar @ sK3)) = $false) | ((listStar @ sK3 @ X0 @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false) | ((listStar @ sK3 @ (rev @ sK3 @ (app @ zero @ sK3 @ (rev @ zero @ nil) @ sK2)) @ X0) = $false) | ($true = $false)) )),
% 1.83/1.89 inference(superposition,[status(thm)],[f610,f96])).
% 1.83/1.89 thf(f96,plain,(
% 1.83/1.89 ((listStar @ sK3 @ (rev @ sK3 @ (app @ zero @ sK3 @ (rev @ zero @ nil) @ sK2)) @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false)),
% 1.83/1.89 inference(backward_demodulation,[status(thm)],[f88,f95])).
% 1.83/1.89 thf(f95,plain,(
% 1.83/1.89 ( ! [X1 : nat] : (((plus @ zero @ X1) = X1)) )),
% 1.83/1.89 inference(equality_proxy_clausification,[status(thm)],[f94])).
% 1.83/1.89 thf(f94,plain,(
% 1.83/1.89 ( ! [X1 : nat] : (($true = ((plus @ zero @ X1) = X1))) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f93])).
% 1.83/1.89 thf(f93,plain,(
% 1.83/1.89 ( ! [X1 : nat] : (($true = ((^[Y0 : nat]: ((plus @ zero @ Y0) = Y0)) @ X1))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f70])).
% 1.83/1.89 thf(f70,plain,(
% 1.83/1.89 ($true = (!! @ nat @ (^[Y0 : nat]: ((plus @ zero @ Y0) = Y0))))),
% 1.83/1.89 inference(cnf_transformation,[status(thm)],[f26])).
% 1.83/1.89 thf(f26,plain,(
% 1.83/1.89 ($true = (!! @ nat @ (^[Y0 : nat]: ((plus @ zero @ Y0) = Y0))))),
% 1.83/1.89 inference(fool_elimination,[status(thm)],[f25])).
% 1.83/1.89 thf(f25,plain,(
% 1.83/1.89 ! [X0 : nat] : ((plus @ zero @ X0) = X0)),
% 1.83/1.89 inference(rectify,[status(thm)],[f12])).
% 1.83/1.89 thf(f12,axiom,(
% 1.83/1.89 ! [X6 : nat] : ((plus @ zero @ X6) = X6)),
% 1.83/1.89 file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',ax1)).
% 1.83/1.89 thf(f88,plain,(
% 1.83/1.89 ((listStar @ (plus @ zero @ sK3) @ (rev @ (plus @ zero @ sK3) @ (app @ zero @ sK3 @ (rev @ zero @ nil) @ sK2)) @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil)) = $false)),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f87])).
% 1.83/1.89 thf(f87,plain,(
% 1.83/1.89 (((listStar @ sK3 @ sK2 @ sK2) => (listStar @ (plus @ zero @ sK3) @ (rev @ (plus @ zero @ sK3) @ (app @ zero @ sK3 @ (rev @ zero @ nil) @ sK2)) @ (app @ sK3 @ zero @ (rev @ sK3 @ sK2) @ nil))) = $false)),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f86])).
% 1.83/1.89 thf(f86,plain,(
% 1.83/1.89 (((^[Y0 : nat]: ((listStar @ Y0 @ sK2 @ sK2) => (listStar @ (plus @ zero @ Y0) @ (rev @ (plus @ zero @ Y0) @ (app @ zero @ Y0 @ (rev @ zero @ nil) @ sK2)) @ (app @ Y0 @ zero @ (rev @ Y0 @ sK2) @ nil)))) @ sK3) = $false)),
% 1.83/1.89 inference(sigma_clausification,[status(thm)],[f79])).
% 1.83/1.89 thf(f79,plain,(
% 1.83/1.89 ((!! @ nat @ (^[Y0 : nat]: ((listStar @ Y0 @ sK2 @ sK2) => (listStar @ (plus @ zero @ Y0) @ (rev @ (plus @ zero @ Y0) @ (app @ zero @ Y0 @ (rev @ zero @ nil) @ sK2)) @ (app @ Y0 @ zero @ (rev @ Y0 @ sK2) @ nil))))) = $false)),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f78])).
% 1.83/1.89 thf(f78,plain,(
% 1.83/1.89 (((^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (rev @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ (rev @ zero @ nil) @ Y0)) @ (app @ Y1 @ zero @ (rev @ Y1 @ Y0) @ nil)))))) @ sK2) = $false)),
% 1.83/1.89 inference(sigma_clausification,[status(thm)],[f77])).
% 1.83/1.89 thf(f77,plain,(
% 1.83/1.89 ((!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (rev @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ (rev @ zero @ nil) @ Y0)) @ (app @ Y1 @ zero @ (rev @ Y1 @ Y0) @ nil))))))) = $false)),
% 1.83/1.89 inference(not_proxy_clausification,[status(thm)],[f74])).
% 1.83/1.89 thf(f74,plain,(
% 1.83/1.89 ($true = (~ (!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (rev @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ (rev @ zero @ nil) @ Y0)) @ (app @ Y1 @ zero @ (rev @ Y1 @ Y0) @ nil)))))))))),
% 1.83/1.89 inference(cnf_transformation,[status(thm)],[f28])).
% 1.83/1.89 thf(f28,plain,(
% 1.83/1.89 ($true = (~ (!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (rev @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ (rev @ zero @ nil) @ Y0)) @ (app @ Y1 @ zero @ (rev @ Y1 @ Y0) @ nil)))))))))),
% 1.83/1.89 inference(fool_elimination,[status(thm)],[f27])).
% 1.83/1.89 thf(f27,plain,(
% 1.83/1.89 ~! [X0 : nat,X1 : list] : ((listStar @ X0 @ X1 @ X1) => (listStar @ (plus @ zero @ X0) @ (rev @ (plus @ zero @ X0) @ (app @ zero @ X0 @ (rev @ zero @ nil) @ X1)) @ (app @ X0 @ zero @ (rev @ X0 @ X1) @ nil)))),
% 1.83/1.89 inference(rectify,[status(thm)],[f19])).
% 1.83/1.89 thf(f19,negated_conjecture,(
% 1.83/1.89 ~! [X13 : nat,X14 : list] : ((listStar @ X13 @ X14 @ X14) => (listStar @ (plus @ zero @ X13) @ (rev @ (plus @ zero @ X13) @ (app @ zero @ X13 @ (rev @ zero @ nil) @ X14)) @ (app @ X13 @ zero @ (rev @ X13 @ X14) @ nil)))),
% 1.83/1.89 inference(negated_conjecture,[status(cth)],[f18])).
% 1.83/1.89 thf(f18,conjecture,(
% 1.83/1.89 ! [X13 : nat,X14 : list] : ((listStar @ X13 @ X14 @ X14) => (listStar @ (plus @ zero @ X13) @ (rev @ (plus @ zero @ X13) @ (app @ zero @ X13 @ (rev @ zero @ nil) @ X14)) @ (app @ X13 @ zero @ (rev @ X13 @ X14) @ nil)))),
% 1.83/1.89 file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',list_rev_invol_lem_base)).
% 1.83/1.89 thf(f610,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o,X4 : X0] : (($true = (X1 @ X4 @ X2)) | ((isPer @ X0 @ X1) = $false) | ((X1 @ X3 @ X2) = $false) | ($false = (X1 @ X4 @ X3))) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f609])).
% 1.83/1.89 thf(f609,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o,X4 : X0] : (($true = ((X1 @ X3 @ X2) => (X1 @ X4 @ X2))) | ((isPer @ X0 @ X1) = $false) | ($false = (X1 @ X4 @ X3))) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f608])).
% 1.83/1.89 thf(f608,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o,X4 : X0] : (($true = ((X1 @ X4 @ X3) => ((X1 @ X3 @ X2) => (X1 @ X4 @ X2)))) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f607])).
% 1.83/1.89 thf(f607,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o,X4 : X0] : ((((^[Y0 : X0]: ((X1 @ Y0 @ X3) => ((X1 @ X3 @ X2) => (X1 @ Y0 @ X2)))) @ X4) = $true) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f606])).
% 1.83/1.89 thf(f606,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o] : (($true = (!! @ X0 @ (^[Y0 : X0]: ((X1 @ Y0 @ X3) => ((X1 @ X3 @ X2) => (X1 @ Y0 @ X2)))))) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f601])).
% 1.83/1.89 thf(f601,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o] : (((isPer @ X0 @ X1) = $false) | ($true = ((^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((X1 @ Y1 @ Y0) => ((X1 @ Y0 @ X2) => (X1 @ Y1 @ X2)))))) @ X3))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f580])).
% 1.83/1.89 thf(f580,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X1 : X0 > X0 > $o] : (((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((X1 @ Y1 @ Y0) => ((X1 @ Y0 @ X2) => (X1 @ Y1 @ X2))))))) = $true) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f576])).
% 1.83/1.89 thf(f576,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X1 : X0 > X0 > $o] : (((isPer @ X0 @ X1) = $false) | ($true = ((^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((X1 @ Y2 @ Y1) => ((X1 @ Y1 @ Y0) => (X1 @ Y2 @ Y0)))))))) @ X2))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f346])).
% 1.83/1.89 thf(f346,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X1 : X0 > X0 > $o] : (($true = (!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((X1 @ Y2 @ Y1) => ((X1 @ Y1 @ Y0) => (X1 @ Y2 @ Y0)))))))))) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f344])).
% 1.83/1.89 thf(f344,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X1 : X0 > X0 > $o] : (((isPer @ X0 @ X1) = $false) | ($true = ((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((X1 @ Y1 @ Y0) => (X1 @ Y0 @ Y1)))))) & (!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((X1 @ Y2 @ Y1) => ((X1 @ Y1 @ Y0) => (X1 @ Y2 @ Y0)))))))))))) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f342])).
% 1.83/1.89 thf(f342,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X1 : X0 > X0 > $o] : (((isPer @ X0 @ X1) = ((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((X1 @ Y1 @ Y0) => (X1 @ Y0 @ Y1)))))) & (!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((X1 @ Y2 @ Y1) => ((X1 @ Y1 @ Y0) => (X1 @ Y2 @ Y0)))))))))))) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f341])).
% 1.83/1.89 thf(f341,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X1 : X0 > X0 > $o] : (($true = (((!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((X1 @ Y1 @ Y0) => (X1 @ Y0 @ Y1)))))) & (!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((X1 @ Y2 @ Y1) => ((X1 @ Y1 @ Y0) => (X1 @ Y2 @ Y0)))))))))) = (isPer @ X0 @ X1)))) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f340])).
% 1.83/1.89 thf(f340,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X1 : X0 > X0 > $o] : (($true = ((^[Y0 : X0 > X0 > $o]: (((!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((Y0 @ Y2 @ Y1) => (Y0 @ Y1 @ Y2)))))) & (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: (!! @ X0 @ (^[Y3 : X0]: ((Y0 @ Y3 @ Y2) => ((Y0 @ Y2 @ Y1) => (Y0 @ Y3 @ Y1)))))))))) = (isPer @ X0 @ Y0))) @ X1))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f67])).
% 1.83/1.89 thf(f67,plain,(
% 1.83/1.89 ( ! [X0 : $tType] : (($true = (!! @ (X0 > X0 > $o) @ (^[Y0 : X0 > X0 > $o]: (((!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((Y0 @ Y2 @ Y1) => (Y0 @ Y1 @ Y2)))))) & (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: (!! @ X0 @ (^[Y3 : X0]: ((Y0 @ Y3 @ Y2) => ((Y0 @ Y2 @ Y1) => (Y0 @ Y3 @ Y1)))))))))) = (isPer @ X0 @ Y0)))))) )),
% 1.83/1.89 inference(cnf_transformation,[status(thm)],[f57])).
% 1.83/1.89 thf(f57,plain,(
% 1.83/1.89 ! [X0 : $tType] : ($true = (!! @ (X0 > X0 > $o) @ (^[Y0 : X0 > X0 > $o]: (((!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((Y0 @ Y2 @ Y1) => (Y0 @ Y1 @ Y2)))))) & (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: (!! @ X0 @ (^[Y3 : X0]: ((Y0 @ Y3 @ Y2) => ((Y0 @ Y2 @ Y1) => (Y0 @ Y3 @ Y1)))))))))) = (isPer @ X0 @ Y0)))))),
% 1.83/1.89 inference(closure,[status(thm)],[f36])).
% 1.83/1.89 thf(f36,plain,(
% 1.83/1.89 ( ! [X0 : $tType] : (($true = (!! @ (X0 > X0 > $o) @ (^[Y0 : X0 > X0 > $o]: (((!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: ((Y0 @ Y2 @ Y1) => (Y0 @ Y1 @ Y2)))))) & (!! @ X0 @ (^[Y1 : X0]: (!! @ X0 @ (^[Y2 : X0]: (!! @ X0 @ (^[Y3 : X0]: ((Y0 @ Y3 @ Y2) => ((Y0 @ Y2 @ Y1) => (Y0 @ Y3 @ Y1)))))))))) = (isPer @ X0 @ Y0)))))) )),
% 1.83/1.89 inference(fool_elimination,[status(thm)],[f35])).
% 1.83/1.89 thf(f35,plain,(
% 1.83/1.89 ! [X0 : $tType,X1 : X0 > X0 > $o] : ((! [X2 : X0,X3 : X0,X4 : X0] : ((X1 @ X2 @ X3) => ((X1 @ X3 @ X4) => (X1 @ X2 @ X4))) & ! [X5 : X0,X6 : X0] : ((X1 @ X5 @ X6) => (X1 @ X6 @ X5))) <=> (isPer @ X0 @ X1))),
% 1.83/1.89 inference(rectify,[status(thm)],[f1])).
% 1.83/1.89 thf(f1,axiom,(
% 1.83/1.89 ! [X0 : $tType,X1 : X0 > X0 > $o] : ((! [X2 : X0,X3 : X0,X4 : X0] : ((X1 @ X2 @ X3) => ((X1 @ X3 @ X4) => (X1 @ X2 @ X4))) & ! [X2 : X0,X3 : X0] : ((X1 @ X2 @ X3) => (X1 @ X3 @ X2))) <=> (isPer @ X0 @ X1))),
% 1.83/1.89 file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',is_per)).
% 1.83/1.89 thf(f284,plain,(
% 1.83/1.89 ( ! [X2 : nat,X1 : list] : (($true = (listStar @ X2 @ (rev @ X2 @ (app @ zero @ X2 @ (rev @ zero @ nil) @ X1)) @ (rev @ X2 @ X1))) | ((listStar @ X2 @ X1 @ X1) = $false)) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f283])).
% 1.83/1.89 thf(f283,plain,(
% 1.83/1.89 ( ! [X2 : nat,X1 : list] : ((((listStar @ X2 @ X1 @ X1) => (listStar @ X2 @ (rev @ X2 @ (app @ zero @ X2 @ (rev @ zero @ nil) @ X1)) @ (rev @ X2 @ X1))) = $true)) )),
% 1.83/1.89 inference(forward_demodulation,[status(thm)],[f282,f95])).
% 1.83/1.89 thf(f282,plain,(
% 1.83/1.89 ( ! [X2 : nat,X1 : list] : (($true = ((listStar @ X2 @ X1 @ X1) => (listStar @ (plus @ zero @ X2) @ (rev @ (plus @ zero @ X2) @ (app @ zero @ X2 @ (rev @ zero @ nil) @ X1)) @ (rev @ X2 @ X1))))) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f281])).
% 1.83/1.89 thf(f281,plain,(
% 1.83/1.89 ( ! [X2 : nat,X1 : list] : (($true = ((^[Y0 : nat]: ((listStar @ Y0 @ X1 @ X1) => (listStar @ (plus @ zero @ Y0) @ (rev @ (plus @ zero @ Y0) @ (app @ zero @ Y0 @ (rev @ zero @ nil) @ X1)) @ (rev @ Y0 @ X1)))) @ X2))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f232])).
% 1.83/1.89 thf(f232,plain,(
% 1.83/1.89 ( ! [X1 : list] : (($true = (!! @ nat @ (^[Y0 : nat]: ((listStar @ Y0 @ X1 @ X1) => (listStar @ (plus @ zero @ Y0) @ (rev @ (plus @ zero @ Y0) @ (app @ zero @ Y0 @ (rev @ zero @ nil) @ X1)) @ (rev @ Y0 @ X1))))))) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f231])).
% 1.83/1.89 thf(f231,plain,(
% 1.83/1.89 ( ! [X1 : list] : ((((^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (rev @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ (rev @ zero @ nil) @ Y0)) @ (rev @ Y1 @ Y0)))))) @ X1) = $true)) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f58])).
% 1.83/1.89 thf(f58,plain,(
% 1.83/1.89 ($true = (!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (rev @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ (rev @ zero @ nil) @ Y0)) @ (rev @ Y1 @ Y0))))))))),
% 1.83/1.89 inference(cnf_transformation,[status(thm)],[f22])).
% 1.83/1.89 thf(f22,plain,(
% 1.83/1.89 ($true = (!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (rev @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ (rev @ zero @ nil) @ Y0)) @ (rev @ Y1 @ Y0))))))))),
% 1.83/1.89 inference(fool_elimination,[status(thm)],[f21])).
% 1.83/1.89 thf(f21,plain,(
% 1.83/1.89 ! [X0 : nat,X1 : list] : ((listStar @ X0 @ X1 @ X1) => (listStar @ (plus @ zero @ X0) @ (rev @ (plus @ zero @ X0) @ (app @ zero @ X0 @ (rev @ zero @ nil) @ X1)) @ (rev @ X0 @ X1)))),
% 1.83/1.89 inference(rectify,[status(thm)],[f16])).
% 1.83/1.89 thf(f16,axiom,(
% 1.83/1.89 ! [X13 : nat,X14 : list] : ((listStar @ X13 @ X14 @ X14) => (listStar @ (plus @ zero @ X13) @ (rev @ (plus @ zero @ X13) @ (app @ zero @ X13 @ (rev @ zero @ nil) @ X14)) @ (rev @ X13 @ X14)))),
% 1.83/1.89 file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',list_rev_invol_lem_base_step1)).
% 1.83/1.89 thf(f422,plain,(
% 1.83/1.89 ( ! [X0 : nat,X1 : list] : (($true = (listStar @ X0 @ (rev @ X0 @ X1) @ (app @ X0 @ zero @ (rev @ X0 @ X1) @ nil))) | ($false = (listStar @ X0 @ X1 @ X1))) )),
% 1.83/1.89 inference(trivial_inequality_removal,[status(thm)],[f421])).
% 1.83/1.89 thf(f421,plain,(
% 1.83/1.89 ( ! [X0 : nat,X1 : list] : (($true = $false) | ($true = (listStar @ X0 @ (rev @ X0 @ X1) @ (app @ X0 @ zero @ (rev @ X0 @ X1) @ nil))) | ($false = (listStar @ X0 @ X1 @ X1))) )),
% 1.83/1.89 inference(forward_demodulation,[status(thm)],[f403,f81])).
% 1.83/1.89 thf(f403,plain,(
% 1.83/1.89 ( ! [X0 : nat,X1 : list] : (($true = (listStar @ X0 @ (rev @ X0 @ X1) @ (app @ X0 @ zero @ (rev @ X0 @ X1) @ nil))) | ((isPer @ list @ (listStar @ X0)) = $false) | ($false = (listStar @ X0 @ X1 @ X1))) )),
% 1.83/1.89 inference(trivial_inequality_removal,[status(thm)],[f381])).
% 1.83/1.89 thf(f381,plain,(
% 1.83/1.89 ( ! [X0 : nat,X1 : list] : (((isPer @ list @ (listStar @ X0)) = $false) | ($false = (listStar @ X0 @ X1 @ X1)) | ($true = $false) | ($true = (listStar @ X0 @ (rev @ X0 @ X1) @ (app @ X0 @ zero @ (rev @ X0 @ X1) @ nil)))) )),
% 1.83/1.89 inference(superposition,[status(thm)],[f173,f352])).
% 1.83/1.89 thf(f352,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o] : (((X1 @ X3 @ X2) = $false) | ((isPer @ X0 @ X1) = $false) | ((X1 @ X2 @ X3) = $true)) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f351])).
% 1.83/1.89 thf(f351,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o] : (($true = ((X1 @ X3 @ X2) => (X1 @ X2 @ X3))) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f350])).
% 1.83/1.89 thf(f350,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X3 : X0,X1 : X0 > X0 > $o] : (($true = ((^[Y0 : X0]: ((X1 @ Y0 @ X2) => (X1 @ X2 @ Y0))) @ X3)) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f349])).
% 1.83/1.89 thf(f349,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X1 : X0 > X0 > $o] : (($true = (!! @ X0 @ (^[Y0 : X0]: ((X1 @ Y0 @ X2) => (X1 @ X2 @ Y0))))) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f348])).
% 1.83/1.89 thf(f348,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X2 : X0,X1 : X0 > X0 > $o] : (((isPer @ X0 @ X1) = $false) | ($true = ((^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((X1 @ Y1 @ Y0) => (X1 @ Y0 @ Y1))))) @ X2))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f347])).
% 1.83/1.89 thf(f347,plain,(
% 1.83/1.89 ( ! [X0 : $tType,X1 : X0 > X0 > $o] : (($true = (!! @ X0 @ (^[Y0 : X0]: (!! @ X0 @ (^[Y1 : X0]: ((X1 @ Y1 @ Y0) => (X1 @ Y0 @ Y1))))))) | ((isPer @ X0 @ X1) = $false)) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f344])).
% 1.83/1.89 thf(f173,plain,(
% 1.83/1.89 ( ! [X2 : nat,X1 : list] : (((listStar @ X2 @ (app @ X2 @ zero @ (rev @ X2 @ X1) @ nil) @ (rev @ X2 @ X1)) = $true) | ((listStar @ X2 @ X1 @ X1) = $false)) )),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f172])).
% 1.83/1.89 thf(f172,plain,(
% 1.83/1.89 ( ! [X2 : nat,X1 : list] : ((((listStar @ X2 @ X1 @ X1) => (listStar @ X2 @ (app @ X2 @ zero @ (rev @ X2 @ X1) @ nil) @ (rev @ X2 @ X1))) = $true)) )),
% 1.83/1.89 inference(forward_demodulation,[status(thm)],[f171,f92])).
% 1.83/1.89 thf(f92,plain,(
% 1.83/1.89 ( ! [X1 : nat] : (((plus @ X1 @ zero) = X1)) )),
% 1.83/1.89 inference(equality_proxy_clausification,[status(thm)],[f91])).
% 1.83/1.89 thf(f91,plain,(
% 1.83/1.89 ( ! [X1 : nat] : (($true = ((plus @ X1 @ zero) = X1))) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f90])).
% 1.83/1.89 thf(f90,plain,(
% 1.83/1.89 ( ! [X1 : nat] : (($true = ((^[Y0 : nat]: ((plus @ Y0 @ zero) = Y0)) @ X1))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f62])).
% 1.83/1.89 thf(f62,plain,(
% 1.83/1.89 ($true = (!! @ nat @ (^[Y0 : nat]: ((plus @ Y0 @ zero) = Y0))))),
% 1.83/1.89 inference(cnf_transformation,[status(thm)],[f40])).
% 1.83/1.89 thf(f40,plain,(
% 1.83/1.89 ($true = (!! @ nat @ (^[Y0 : nat]: ((plus @ Y0 @ zero) = Y0))))),
% 1.83/1.89 inference(fool_elimination,[status(thm)],[f39])).
% 1.83/1.89 thf(f39,plain,(
% 1.83/1.89 ! [X0 : nat] : ((plus @ X0 @ zero) = X0)),
% 1.83/1.89 inference(rectify,[status(thm)],[f14])).
% 1.83/1.89 thf(f14,axiom,(
% 1.83/1.89 ! [X10 : nat] : ((plus @ X10 @ zero) = X10)),
% 1.83/1.89 file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',plus_zero_r)).
% 1.83/1.89 thf(f171,plain,(
% 1.83/1.89 ( ! [X2 : nat,X1 : list] : (($true = ((listStar @ X2 @ X1 @ X1) => (listStar @ (plus @ X2 @ zero) @ (app @ X2 @ zero @ (rev @ X2 @ X1) @ nil) @ (rev @ X2 @ X1))))) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f170])).
% 1.83/1.89 thf(f170,plain,(
% 1.83/1.89 ( ! [X2 : nat,X1 : list] : (($true = ((^[Y0 : nat]: ((listStar @ Y0 @ X1 @ X1) => (listStar @ (plus @ Y0 @ zero) @ (app @ Y0 @ zero @ (rev @ Y0 @ X1) @ nil) @ (rev @ Y0 @ X1)))) @ X2))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f150])).
% 1.83/1.89 thf(f150,plain,(
% 1.83/1.89 ( ! [X1 : list] : (($true = (!! @ nat @ (^[Y0 : nat]: ((listStar @ Y0 @ X1 @ X1) => (listStar @ (plus @ Y0 @ zero) @ (app @ Y0 @ zero @ (rev @ Y0 @ X1) @ nil) @ (rev @ Y0 @ X1))))))) )),
% 1.83/1.89 inference(beta_eta_normalization,[status(thm)],[f149])).
% 1.83/1.89 thf(f149,plain,(
% 1.83/1.89 ( ! [X1 : list] : (($true = ((^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ Y1 @ zero) @ (app @ Y1 @ zero @ (rev @ Y1 @ Y0) @ nil) @ (rev @ Y1 @ Y0)))))) @ X1))) )),
% 1.83/1.89 inference(pi_clausification,[status(thm)],[f72])).
% 1.83/1.89 thf(f72,plain,(
% 1.83/1.89 ($true = (!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ Y1 @ zero) @ (app @ Y1 @ zero @ (rev @ Y1 @ Y0) @ nil) @ (rev @ Y1 @ Y0))))))))),
% 1.83/1.89 inference(cnf_transformation,[status(thm)],[f44])).
% 1.83/1.89 thf(f44,plain,(
% 1.83/1.89 ($true = (!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ Y1 @ zero) @ (app @ Y1 @ zero @ (rev @ Y1 @ Y0) @ nil) @ (rev @ Y1 @ Y0))))))))),
% 1.83/1.89 inference(fool_elimination,[status(thm)],[f43])).
% 1.83/1.89 thf(f43,plain,(
% 1.83/1.89 ! [X0 : nat,X1 : list] : ((listStar @ X0 @ X1 @ X1) => (listStar @ (plus @ X0 @ zero) @ (app @ X0 @ zero @ (rev @ X0 @ X1) @ nil) @ (rev @ X0 @ X1)))),
% 1.83/1.89 inference(rectify,[status(thm)],[f17])).
% 1.83/1.89 thf(f17,axiom,(
% 1.83/1.89 ! [X13 : nat,X14 : list] : ((listStar @ X13 @ X14 @ X14) => (listStar @ (plus @ X13 @ zero) @ (app @ X13 @ zero @ (rev @ X13 @ X14) @ nil) @ (rev @ X13 @ X14)))),
% 1.83/1.89 file('/export/starexec/sandbox2/tmp/tmp.AA59i5yks9/DTF2THF_10562.p',list_rev_invol_lem_base_step2)).
% 1.83/1.89 thf(f89,plain,(
% 1.83/1.89 ($true = (listStar @ sK3 @ sK2 @ sK2))),
% 1.83/1.89 inference(binary_proxy_clausification,[status(thm)],[f87])).
% 1.83/1.89 % SZS output end Proof for DTF2THF_10562
% 1.83/1.89 % (10881)------------------------------
% 1.83/1.89 % (10881)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.83/1.89 % (10881)Termination reason: Refutation
% 1.83/1.89
% 1.83/1.89 % (10881)Memory used [KB]: 6268
% 1.83/1.89 % (10881)Time elapsed: 0.070 s
% 1.83/1.89 % (10881)Instructions burned: 216 (million)
% 1.83/1.89 % (10881)------------------------------
% 1.83/1.89 % (10881)------------------------------
% 1.83/1.89 % (10825)Success in time 0.513 s
%------------------------------------------------------------------------------