%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : DAT338^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 : n022.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:31 AM UTC 2026
% Result : Theorem 1.79s 1.43s
% Output : Refutation 1.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 4
% Syntax : Number of formulae : 31 ( 29 unt; 0 typ; 0 def)
% Number of atoms : 89 ( 27 equ; 0 cnn)
% Maximal formula atoms : 2 ( 2 avg)
% Number of connectives : 247 ( 5 ~; 0 |; 0 &; 224 @)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 15 ( 11 usr; 5 con; 0-4 aty)
% ( 8 !!; 0 ??; 0 @@+; 0 @@-)
% Number of variables : 28 ( 11 ^; 17 !; 0 ?; 28 :)
% 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_30,type,
ph1:
!>[X0: $tType] : X0 ).
thf(f256,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f255]) ).
thf(f255,plain,
$true = $false,
inference(forward_demodulation,[status(thm)],[f254,f94]) ).
thf(f94,plain,
( ( listStar @ zero @ ( app @ zero @ zero @ nil @ nil ) @ nil )
= $false ),
inference(not_proxy_clausification,[status(thm)],[f84]) ).
thf(f84,plain,
( ( ~ ( listStar @ zero @ ( app @ zero @ zero @ nil @ nil ) @ nil ) )
= $true ),
inference(backward_demodulation,[status(thm)],[f68,f83]) ).
thf(f83,plain,
! [X1: nat] :
( ( plus @ zero @ X1 )
= X1 ),
inference(equality_proxy_clausification,[status(thm)],[f82]) ).
thf(f82,plain,
! [X1: nat] :
( ( ( plus @ zero @ X1 )
= X1 )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f81]) ).
thf(f81,plain,
! [X1: nat] :
( ( ^ [Y0: nat] :
( ( plus @ zero @ Y0 )
= Y0 )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f69]) ).
thf(f69,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( plus @ zero @ Y0 )
= Y0 ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f41]) ).
thf(f41,plain,
( ( !! @ nat
@ ^ [Y0: nat] :
( ( plus @ zero @ Y0 )
= Y0 ) )
= $true ),
inference(fool_elimination,[status(thm)],[f40]) ).
thf(f40,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.xVPkMCFDQR/DTF2THF_12734.p',ax1) ).
thf(f68,plain,
( ( ~ ( listStar @ ( plus @ zero @ zero ) @ ( app @ zero @ zero @ nil @ nil ) @ nil ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f39]) ).
thf(f39,plain,
( ( ~ ( listStar @ ( plus @ zero @ zero ) @ ( app @ zero @ zero @ nil @ nil ) @ nil ) )
= $true ),
inference(fool_elimination,[status(thm)],[f38]) ).
thf(f38,plain,
~ ( listStar @ ( plus @ zero @ zero ) @ ( app @ zero @ zero @ nil @ nil ) @ nil ),
inference(rectify,[status(thm)],[f18]) ).
thf(f18,negated_conjecture,
~ ( listStar @ ( plus @ zero @ zero ) @ ( app @ zero @ zero @ nil @ nil ) @ nil ),
inference(negated_conjecture,[status(cth)],[f17]) ).
thf(f17,conjecture,
listStar @ ( plus @ zero @ zero ) @ ( app @ zero @ zero @ nil @ nil ) @ nil,
file('/export/starexec/sandbox2/tmp/tmp.xVPkMCFDQR/DTF2THF_12734.p',list_app_nil_base) ).
thf(f254,plain,
( ( listStar @ zero @ ( app @ zero @ zero @ nil @ nil ) @ nil )
= $true ),
inference(boolean_simplification,[status(thm)],[f252]) ).
thf(f252,plain,
( ( $true
=> ( listStar @ zero @ ( app @ zero @ zero @ nil @ nil ) @ nil ) )
= $true ),
inference(superposition,[status(thm)],[f242,f60]) ).
thf(f60,plain,
( ( listStar @ zero @ nil @ nil )
= $true ),
inference(cnf_transformation,[status(thm)],[f53]) ).
thf(f53,plain,
( ( listStar @ zero @ nil @ nil )
= $true ),
inference(fool_elimination,[status(thm)],[f52]) ).
thf(f52,plain,
listStar @ zero @ nil @ nil,
inference(rectify,[status(thm)],[f5]) ).
thf(f5,axiom,
listStar @ zero @ nil @ nil,
file('/export/starexec/sandbox2/tmp/tmp.xVPkMCFDQR/DTF2THF_12734.p',nil_tp_ax) ).
thf(f242,plain,
! [X2: nat,X1: list] :
( ( ( listStar @ X2 @ X1 @ X1 )
=> ( listStar @ X2 @ ( app @ zero @ X2 @ nil @ X1 ) @ X1 ) )
= $true ),
inference(forward_demodulation,[status(thm)],[f238,f83]) ).
thf(f238,plain,
! [X2: nat,X1: list] :
( ( ( listStar @ X2 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ X2 ) @ ( app @ zero @ X2 @ nil @ X1 ) @ X1 ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f236]) ).
thf(f236,plain,
! [X2: nat,X1: list] :
( ( ^ [Y0: nat] :
( ( listStar @ Y0 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ Y0 ) @ ( app @ zero @ Y0 @ nil @ X1 ) @ X1 ) )
@ X2 )
= $true ),
inference(pi_clausification,[status(thm)],[f229]) ).
thf(f229,plain,
! [X1: list] :
( ( !! @ nat
@ ^ [Y0: nat] :
( ( listStar @ Y0 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ Y0 ) @ ( app @ zero @ Y0 @ nil @ X1 ) @ X1 ) ) )
= $true ),
inference(beta_eta_normalization,[status(thm)],[f228]) ).
thf(f228,plain,
! [X1: list] :
( ( ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ nil @ Y0 ) @ Y0 ) ) )
@ X1 )
= $true ),
inference(pi_clausification,[status(thm)],[f64]) ).
thf(f64,plain,
( ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ nil @ Y0 ) @ Y0 ) ) ) )
= $true ),
inference(cnf_transformation,[status(thm)],[f23]) ).
thf(f23,plain,
( ( !! @ list
@ ^ [Y0: list] :
( !! @ nat
@ ^ [Y1: nat] :
( ( listStar @ Y1 @ Y0 @ Y0 )
=> ( listStar @ ( plus @ zero @ Y1 ) @ ( app @ zero @ Y1 @ nil @ Y0 ) @ Y0 ) ) ) )
= $true ),
inference(fool_elimination,[status(thm)],[f22]) ).
thf(f22,plain,
! [X0: nat,X1: list] :
( ( listStar @ X0 @ X1 @ X1 )
=> ( listStar @ ( plus @ zero @ X0 ) @ ( app @ zero @ X0 @ nil @ X1 ) @ X1 ) ),
inference(rectify,[status(thm)],[f14]) ).
thf(f14,axiom,
! [X6: nat,X2: list] :
( ( listStar @ X6 @ X2 @ X2 )
=> ( listStar @ ( plus @ zero @ X6 ) @ ( app @ zero @ X6 @ nil @ X2 ) @ X2 ) ),
file('/export/starexec/sandbox2/tmp/tmp.xVPkMCFDQR/DTF2THF_12734.p',ax3) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : DAT338^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.35 % Computer : n022.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Tue Feb 24 06:15:36 EST 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 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.46 thf(spec,logic,$$dhol).
% 0.28/0.46 %------------------------------------------------------------------------------
% 0.28/0.46 % File : DAT338^1 : TPTP v9.2.1. Released v9.2.0.
% 0.28/0.46 % Domain : Data Structures
% 0.28/0.46 % Problem : Nil is a right-neutral element of app, base case
% 0.28/0.46 % Version : Especial.
% 0.28/0.46 % English : Nil is a right-neutral element of app. The proof is by induction
% 0.28/0.46 % with a separate problem file for the base and step case as well as
% 0.28/0.46 % the correct instantiation of the induction axiom for lists. The
% 0.28/0.46 % main file uses the conjectures of the other files as lemmas in
% 0.28/0.46 % order to prove the final result. To simplify proof search, the
% 0.28/0.46 % lemmas in the problem file for the induction step have been
% 0.28/0.46 % preselected.
% 0.28/0.46
% 0.28/0.46 % Refs : [RRB23] Rothgang et al. (2023), Theorem Proving in Dependently
% 0.28/0.46 % : [Rot25] Rothgang (2025), Email to Geoff Sutcliffe
% 0.28/0.46 % : [RK+25] Ranalter et al. (2025), The Dependently Typed Higher-O
% 0.28/0.46 % Source : [Rot25]
% 0.28/0.46 % Names : ListAppNil/list-app-nil-base.p [Rot25]
% 0.28/0.46
% 0.28/0.46 % Status : Theorem
% 0.28/0.46 % Rating : ? v9.2.0
% 0.28/0.46 % Syntax : Number of formulae : 19 ( 7 unt; 9 typ; 0 def)
% 0.28/0.46 % Number of atoms : 9 ( 9 equ; 0 cnn)
% 0.28/0.46 % Maximal formula atoms : 2 ( 0 avg)
% 0.28/0.46 % Number of connectives : 80 ( 3 ~; 0 |; 0 &; 70 @)
% 0.28/0.46 % ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% 0.28/0.46 % Maximal formula depth : 12 ( 5 avg)
% 0.28/0.46 % Number of types : 3 ( 2 usr)
% 0.28/0.46 % Number of type decls : 9 ( 0 !>P; 3 !>D)
% 0.28/0.46 % Number of type conns : 10 ( 10 >; 0 *; 0 +; 0 <<)
% 0.28/0.46 % Number of symbols : 8 ( 7 usr; 2 con; 0-4 aty)
% 0.28/0.46 % Number of variables : 27 ( 0 ^; 23 !; 0 ?; 27 :)
% 0.28/0.46 % ( 4 !>; 0 ?*; 0 @-; 0 @+)
% 0.28/0.46 % SPC : DH0_THM_EQU_NAR
% 0.28/0.46
% 0.28/0.46 % Comments :
% 0.28/0.46 %------------------------------------------------------------------------------
% 0.28/0.46 thf(elem_type,type,
% 0.28/0.46 elem: $tType ).
% 0.28/0.46
% 0.28/0.46 thf(nat_type,type,
% 0.28/0.46 nat: $tType ).
% 0.28/0.46
% 0.28/0.46 thf(zero_type,type,
% 0.28/0.46 zero: nat ).
% 0.28/0.46
% 0.28/0.46 thf(suc_type,type,
% 0.28/0.46 suc: nat > nat ).
% 0.28/0.46
% 0.28/0.46 thf(plus_type,type,
% 0.28/0.46 plus: nat > nat > nat ).
% 0.28/0.46
% 0.28/0.46 thf(list_type,type,
% 0.28/0.46 list: nat > $tType ).
% 0.28/0.46
% 0.28/0.46 thf(nil_type,type,
% 0.28/0.46 nil: list @ zero ).
% 0.28/0.46
% 0.28/0.46 thf(cons_type,type,
% 0.28/0.46 cons:
% 0.28/0.46 !>[N: nat] : ( elem > ( list @ N ) > ( list @ ( suc @ N ) ) ) ).
% 0.28/0.46
% 0.28/0.46 thf(app_type,type,
% 0.28/0.46 app:
% 0.28/0.46 !>[N: nat,M: nat] : ( ( list @ N ) > ( list @ M ) > ( list @ ( plus @ N @ M ) ) ) ).
% 0.28/0.46
% 0.28/0.46 thf(peano1,axiom,
% 0.28/0.46 ! [N: nat] :
% 0.28/0.46 ( ( suc @ N )
% 0.28/0.46 != zero ) ).
% 0.28/0.46
% 0.28/0.46 thf(peano2,axiom,
% 0.28/0.46 ! [N: nat,M: nat] :
% 0.28/0.46 ( ( N != M )
% 0.28/0.46 => ( ( suc @ N )
% 0.28/0.46 != ( suc @ M ) ) ) ).
% 0.28/0.46
% 0.28/0.46 thf(peano3,axiom,
% 0.28/0.46 ! [P: nat > $o] :
% 0.28/0.46 ( ( P @ zero )
% 0.28/0.46 => ( ! [M: nat] :
% 0.28/0.46 ( ( P @ M )
% 0.28/0.46 => ( P @ ( suc @ M ) ) )
% 0.28/0.46 => ! [N: nat] : ( P @ N ) ) ) ).
% 0.28/0.46
% 0.28/0.46 thf(list_induct,axiom,
% 0.28/0.46 ! [P: !>[N: nat] : ( ( list @ N ) > $o )] :
% 0.28/0.46 ( ( P @ zero @ nil )
% 0.28/0.46 => ( ! [M: nat,X: elem,Y: list @ M] :
% 0.28/0.46 ( ( P @ M @ Y )
% 0.28/0.46 => ( P @ ( suc @ M ) @ ( cons @ M @ X @ Y ) ) )
% 0.28/0.46 => ! [N: nat,X: list @ N] : ( P @ N @ X ) ) ) ).
% 0.28/0.46
% 0.28/0.46 thf(ax1,axiom,
% 0.28/0.46 ! [N: nat] :
% 0.28/0.46 ( ( plus @ zero @ N )
% 0.28/0.46 = N ) ).
% 0.28/0.46
% 0.28/0.46 thf(ax2,axiom,
% 0.28/0.46 ! [N: nat,M: nat] :
% 0.28/0.46 ( ( plus @ ( suc @ N ) @ M )
% 0.28/0.46 = ( suc @ ( plus @ N @ M ) ) ) ).
% 0.28/0.46
% 0.28/0.46 thf(ax3,axiom,
% 0.28/0.46 ! [N: nat,X: list @ N] :
% 0.28/0.46 ( ( app @ zero @ N @ nil @ X )
% 0.28/0.46 = X ) ).
% 0.28/0.46
% 0.28/0.46 thf(ax4,axiom,
% 0.28/0.46 ! [N: nat,M: nat,X: elem,Y: list @ N,Z: list @ M] :
% 0.28/0.46 ( ( app @ ( suc @ N ) @ M @ ( cons @ N @ X @ Y ) @ Z )
% 0.28/0.46 = ( cons @ ( plus @ N @ M ) @ X @ ( app @ N @ M @ Y @ Z ) ) ) ).
% 0.28/0.46
% 0.28/0.46 thf(plus_zero_r,axiom,
% 0.28/0.46 ! [M: nat] :
% 0.28/0.46 ( ( plus @ M @ zero )
% 0.28/0.46 = M ) ).
% 0.28/0.46
% 0.28/0.46 thf(list_app_nil_base,conjecture,
% 0.28/0.46 ( ( app @ zero @ zero @ nil @ nil )
% 0.28/0.46 = nil ) ).
% 0.28/0.46
% 0.28/0.46 %------------------------------------------------------------------------------
% 0.28/0.46 ------------------------
% 1.68/1.35 ---- Embedded in THF ---
% 1.68/1.35 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.68/1.35 %%% Generated on Tue Feb 24 06:15:37 EST 2026
% 1.68/1.35 %%% using '$$dhol' embedding, version 1.3.0.
% 1.68/1.35 %%% Logic specification used:
% 1.68/1.35 %%% thf(spec, logic, $$dhol).
% 1.68/1.35
% 1.68/1.35 % SZS output start ListOfTHF for /export/starexec/sandbox2/tmp/tmp.xVPkMCFDQR/DTF2DTF12734.p
% See solution above
% 1.68/1.35 ------------------------
% 1.68/1.36 ---- Cleaned THF ---
% 1.68/1.36 thf(is_per_type,type,
% 1.68/1.36 isPer:
% 1.68/1.36 !>[A: $tType] : ( ( A > A > $o ) > $o ) ).
% 1.68/1.36
% 1.68/1.36 thf(is_per,definition,
% 1.68/1.36 ! [A: $tType,AStar: A > A > $o] :
% 1.68/1.36 ( ( isPer @ A @ AStar )
% 1.68/1.36 <=> ( ! [X: A,Y: A] :
% 1.68/1.36 ( ( AStar @ X @ Y )
% 1.68/1.36 => ( AStar @ Y @ X ) )
% 1.68/1.36 & ! [X: A,Y: A,Z: A] :
% 1.68/1.36 ( ( AStar @ X @ Y )
% 1.68/1.36 => ( ( AStar @ Y @ Z )
% 1.68/1.36 => ( AStar @ X @ Z ) ) ) ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(elem_type,type,
% 1.68/1.36 elem: $tType ).
% 1.68/1.36
% 1.68/1.36 thf(elemStar,type,
% 1.68/1.36 elemStar: elem > elem > $o ).
% 1.68/1.36
% 1.68/1.36 thf(elemStar_is_eq,axiom,
% 1.68/1.36 ! [X: elem,Y: elem] :
% 1.68/1.36 ( ( elemStar @ X @ Y )
% 1.68/1.36 <=> ( X = Y ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(nat_type,type,
% 1.68/1.36 nat: $tType ).
% 1.68/1.36
% 1.68/1.36 thf(natStar,type,
% 1.68/1.36 natStar: nat > nat > $o ).
% 1.68/1.36
% 1.68/1.36 thf(natStar_is_eq,axiom,
% 1.68/1.36 ! [X: nat,Y: nat] :
% 1.68/1.36 ( ( natStar @ X @ Y )
% 1.68/1.36 <=> ( X = Y ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(zero_type,type,
% 1.68/1.36 zero: nat ).
% 1.68/1.36
% 1.68/1.36 thf(suc_type,type,
% 1.68/1.36 suc: nat > nat ).
% 1.68/1.36
% 1.68/1.36 thf(plus_type,type,
% 1.68/1.36 plus: nat > nat > nat ).
% 1.68/1.36
% 1.68/1.36 thf(list_type,type,
% 1.68/1.36 list: $tType ).
% 1.68/1.36
% 1.68/1.36 thf(listStar,type,
% 1.68/1.36 listStar: nat > list > list > $o ).
% 1.68/1.36
% 1.68/1.36 thf('\'listStar\'_is_per',axiom,
% 1.68/1.36 ! [C: nat] : ( isPer @ list @ ( listStar @ C ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(nil_type,type,
% 1.68/1.36 nil: list ).
% 1.68/1.36
% 1.68/1.36 thf(nil_tp_ax,axiom,
% 1.68/1.36 listStar @ zero @ nil @ nil ).
% 1.68/1.36
% 1.68/1.36 thf(cons_type,type,
% 1.68/1.36 cons: nat > elem > list > list ).
% 1.68/1.36
% 1.68/1.36 thf(cons_tp_ax,axiom,
% 1.68/1.36 ! [N: nat,D: elem,D0: list,D0_prime: list] :
% 1.68/1.36 ( ( listStar @ N @ D0 @ D0_prime )
% 1.68/1.36 => ( listStar @ ( suc @ N ) @ ( cons @ N @ D @ D0 ) @ ( cons @ N @ D @ D0_prime ) ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(app_type,type,
% 1.68/1.36 app: nat > nat > list > list > list ).
% 1.68/1.36
% 1.68/1.36 thf(app_tp_ax,axiom,
% 1.68/1.36 ! [N: nat,M: nat,D: list,D_prime: list] :
% 1.68/1.36 ( ( listStar @ N @ D @ D_prime )
% 1.68/1.36 => ! [D0: list,D0_prime: list] :
% 1.68/1.36 ( ( listStar @ M @ D0 @ D0_prime )
% 1.68/1.36 => ( listStar @ ( plus @ N @ M ) @ ( app @ N @ M @ D @ D0 ) @ ( app @ N @ M @ D_prime @ D0_prime ) ) ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(peano1,axiom,
% 1.68/1.36 ! [N: nat] :
% 1.68/1.36 ( ( suc @ N )
% 1.68/1.36 != zero ) ).
% 1.68/1.36
% 1.68/1.36 thf(peano2,axiom,
% 1.68/1.36 ! [N: nat,M: nat] :
% 1.68/1.36 ( ( N != M )
% 1.68/1.36 => ( ( suc @ N )
% 1.68/1.36 != ( suc @ M ) ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(peano3,axiom,
% 1.68/1.36 ! [P: nat > $o] :
% 1.68/1.36 ( ( P @ zero )
% 1.68/1.36 => ( ! [M: nat] :
% 1.68/1.36 ( ( P @ M )
% 1.68/1.36 => ( P @ ( suc @ M ) ) )
% 1.68/1.36 => ! [N: nat] : ( P @ N ) ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(list_induct,axiom,
% 1.68/1.36 ! [P: nat > list > $o] :
% 1.68/1.36 ( ! [N: nat,D: list,D_prime: list] :
% 1.68/1.36 ( ( listStar @ N @ D @ D_prime )
% 1.68/1.36 => ( ( P @ N @ D )
% 1.68/1.36 = ( P @ N @ D_prime ) ) )
% 1.68/1.36 => ( ( P @ zero @ nil )
% 1.68/1.36 => ( ! [M: nat,X: elem,Y: list] :
% 1.68/1.36 ( ( listStar @ M @ Y @ Y )
% 1.68/1.36 => ( ( P @ M @ Y )
% 1.68/1.36 => ( P @ ( suc @ M ) @ ( cons @ M @ X @ Y ) ) ) )
% 1.68/1.36 => ! [N: nat,X: list] :
% 1.68/1.36 ( ( listStar @ N @ X @ X )
% 1.68/1.36 => ( P @ N @ X ) ) ) ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(ax1,axiom,
% 1.68/1.36 ! [N: nat] :
% 1.68/1.36 ( ( plus @ zero @ N )
% 1.68/1.36 = N ) ).
% 1.68/1.36
% 1.68/1.36 thf(ax2,axiom,
% 1.68/1.36 ! [N: nat,M: nat] :
% 1.68/1.36 ( ( plus @ ( suc @ N ) @ M )
% 1.68/1.36 = ( suc @ ( plus @ N @ M ) ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(ax3,axiom,
% 1.68/1.36 ! [N: nat,X: list] :
% 1.68/1.36 ( ( listStar @ N @ X @ X )
% 1.68/1.36 => ( listStar @ ( plus @ zero @ N ) @ ( app @ zero @ N @ nil @ X ) @ X ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(ax4,axiom,
% 1.68/1.36 ! [N: nat,M: nat,X: elem,Y: list,Z: list] :
% 1.68/1.36 ( ( listStar @ N @ Y @ Y )
% 1.68/1.36 => ( ( listStar @ M @ Z @ Z )
% 1.68/1.36 => ( listStar @ ( plus @ ( suc @ N ) @ M ) @ ( app @ ( suc @ N ) @ M @ ( cons @ N @ X @ Y ) @ Z ) @ ( cons @ ( plus @ N @ M ) @ X @ ( app @ N @ M @ Y @ Z ) ) ) ) ) ).
% 1.68/1.36
% 1.68/1.36 thf(plus_zero_r,axiom,
% 1.68/1.36 ! [M: nat] :
% 1.68/1.36 ( ( plus @ M @ zero )
% 1.68/1.36 = M ) ).
% 1.68/1.36
% 1.68/1.36 thf(list_app_nil_base,conjecture,
% 1.68/1.36 listStar @ ( plus @ zero @ zero ) @ ( app @ zero @ zero @ nil @ nil ) @ nil ).
% 1.68/1.36 ------------------------
% 1.68/1.37 % (13062)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_12734 for (2999ds/27Mi)
% 1.68/1.37 % (13060)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/183Mi)
% 1.68/1.38 % (13061)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_12734 for (2999ds/4Mi)
% 1.68/1.38 % (13063)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/2Mi)
% 1.68/1.38 % (13064)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_12734 for (2999ds/2Mi)
% 1.68/1.38 % (13065)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_12734 for (2999ds/275Mi)
% 1.68/1.38 % (13066)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/18Mi)
% 1.68/1.38 % (13063)Instruction limit reached!
% 1.68/1.38 % (13063)------------------------------
% 1.68/1.38 % (13063)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.38 % (13063)Termination reason: Unknown
% 1.68/1.38 % (13063)Termination phase: shuffling
% 1.68/1.38
% 1.68/1.38 % (13063)Memory used [KB]: 1023
% 1.68/1.38 % (13063)Time elapsed: 0.003 s
% 1.68/1.38 % (13063)Instructions burned: 2 (million)
% 1.68/1.38 % (13063)------------------------------
% 1.68/1.38 % (13063)------------------------------
% 1.68/1.38 % (13064)Instruction limit reached!
% 1.68/1.38 % (13064)------------------------------
% 1.68/1.38 % (13064)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.38 % (13064)Termination reason: Unknown
% 1.68/1.38 % (13064)Termination phase: shuffling
% 1.68/1.38
% 1.68/1.38 % (13064)Memory used [KB]: 1023
% 1.68/1.38 % (13064)Time elapsed: 0.003 s
% 1.68/1.38 % (13064)Instructions burned: 2 (million)
% 1.68/1.38 % (13064)------------------------------
% 1.68/1.38 % (13064)------------------------------
% 1.68/1.38 % (13061)Instruction limit reached!
% 1.68/1.38 % (13061)------------------------------
% 1.68/1.38 % (13061)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.38 % (13061)Termination reason: Unknown
% 1.68/1.38 % (13061)Termination phase: shuffling
% 1.68/1.38
% 1.68/1.38 % (13061)Memory used [KB]: 1023
% 1.68/1.38 % (13061)Time elapsed: 0.004 s
% 1.68/1.38 % (13061)Instructions burned: 4 (million)
% 1.68/1.38 % (13061)------------------------------
% 1.68/1.38 % (13061)------------------------------
% 1.68/1.38 % (13062)Instruction limit reached!
% 1.68/1.38 % (13062)------------------------------
% 1.68/1.38 % (13062)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.38 % (13062)Termination reason: Unknown
% 1.68/1.38 % (13062)Termination phase: Saturation
% 1.68/1.38
% 1.68/1.38 % (13062)Memory used [KB]: 5756
% 1.68/1.38 % (13062)Time elapsed: 0.011 s
% 1.68/1.38 % (13062)Instructions burned: 28 (million)
% 1.68/1.38 % (13062)------------------------------
% 1.68/1.38 % (13062)------------------------------
% 1.68/1.39 % (13065)Refutation not found, incomplete strategy
% 1.68/1.39 % (13065)------------------------------
% 1.68/1.39 % (13065)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.39 % (13065)Termination reason: Refutation not found, incomplete strategy
% 1.68/1.39
% 1.68/1.39
% 1.68/1.39 % (13065)Memory used [KB]: 5500
% 1.68/1.39 % (13065)Time elapsed: 0.005 s
% 1.68/1.39 % (13065)Instructions burned: 5 (million)
% 1.68/1.39 % (13065)------------------------------
% 1.68/1.39 % (13065)------------------------------
% 1.68/1.39 % (13066)Instruction limit reached!
% 1.68/1.39 % (13066)------------------------------
% 1.68/1.39 % (13066)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.39 % (13066)Termination reason: Unknown
% 1.68/1.39 % (13066)Termination phase: Saturation
% 1.68/1.39
% 1.68/1.39 % (13066)Memory used [KB]: 5628
% 1.68/1.39 % (13066)Time elapsed: 0.013 s
% 1.68/1.39 % (13066)Instructions burned: 18 (million)
% 1.68/1.39 % (13066)------------------------------
% 1.68/1.39 % (13066)------------------------------
% 1.68/1.39 % (13070)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_12734 for (2999ds/3Mi)
% 1.68/1.39 % (13070)Instruction limit reached!
% 1.68/1.39 % (13070)------------------------------
% 1.68/1.39 % (13070)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.68/1.39 % (13070)Termination reason: Unknown
% 1.68/1.39 % (13070)Termination phase: Preprocessing 2
% 1.68/1.39
% 1.68/1.39 % (13070)Memory used [KB]: 1023
% 1.68/1.39 % (13070)Time elapsed: 0.002 s
% 1.68/1.39 % (13070)Instructions burned: 4 (million)
% 1.68/1.39 % (13070)------------------------------
% 1.68/1.39 % (13070)------------------------------
% 1.79/1.40 % (13067)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/3Mi)
% 1.79/1.40 % (13068)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_12734 for (2999ds/37Mi)
% 1.79/1.40 % (13069)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_12734 for (2999ds/15Mi)
% 1.79/1.40 % (13067)Instruction limit reached!
% 1.79/1.40 % (13067)------------------------------
% 1.79/1.40 % (13067)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.40 % (13067)Termination reason: Unknown
% 1.79/1.40 % (13067)Termination phase: Preprocessing 3
% 1.79/1.40
% 1.79/1.40 % (13067)Memory used [KB]: 1023
% 1.79/1.40 % (13067)Time elapsed: 0.004 s
% 1.79/1.40 % (13067)Instructions burned: 4 (million)
% 1.79/1.40 % (13067)------------------------------
% 1.79/1.40 % (13067)------------------------------
% 1.79/1.40 % (13073)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/16Mi)
% 1.79/1.40 % (13071)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_12734 for (2999ds/1041Mi)
% 1.79/1.41 % (13073)Instruction limit reached!
% 1.79/1.41 % (13073)------------------------------
% 1.79/1.41 % (13073)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.41 % (13073)Termination reason: Unknown
% 1.79/1.41 % (13073)Termination phase: Saturation
% 1.79/1.41
% 1.79/1.41 % (13073)Memory used [KB]: 5628
% 1.79/1.41 % (13073)Time elapsed: 0.006 s
% 1.79/1.41 % (13073)Instructions burned: 16 (million)
% 1.79/1.41 % (13073)------------------------------
% 1.79/1.41 % (13073)------------------------------
% 1.79/1.41 % (13069)Instruction limit reached!
% 1.79/1.41 % (13069)------------------------------
% 1.79/1.41 % (13069)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.41 % (13069)Termination reason: Unknown
% 1.79/1.41 % (13069)Termination phase: Saturation
% 1.79/1.41
% 1.79/1.41 % (13069)Memory used [KB]: 5756
% 1.79/1.41 % (13069)Time elapsed: 0.011 s
% 1.79/1.41 % (13069)Instructions burned: 15 (million)
% 1.79/1.41 % (13069)------------------------------
% 1.79/1.41 % (13069)------------------------------
% 1.79/1.41 % (13072)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/7Mi)
% 1.79/1.41 % (13072)Instruction limit reached!
% 1.79/1.41 % (13072)------------------------------
% 1.79/1.41 % (13072)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.41 % (13072)Termination reason: Unknown
% 1.79/1.41 % (13072)Termination phase: Property scanning
% 1.79/1.41
% 1.79/1.41 % (13072)Memory used [KB]: 1023
% 1.79/1.41 % (13072)Time elapsed: 0.006 s
% 1.79/1.41 % (13072)Instructions burned: 7 (million)
% 1.79/1.41 % (13072)------------------------------
% 1.79/1.41 % (13072)------------------------------
% 1.79/1.42 % (13075)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_12734 for (2999ds/3Mi)
% 1.79/1.42 % (13075)Instruction limit reached!
% 1.79/1.42 % (13075)------------------------------
% 1.79/1.42 % (13075)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.42 % (13075)Termination reason: Unknown
% 1.79/1.42 % (13075)Termination phase: Preprocessing 1
% 1.79/1.42
% 1.79/1.42 % (13075)Memory used [KB]: 1023
% 1.79/1.42 % (13075)Time elapsed: 0.002 s
% 1.79/1.42 % (13075)Instructions burned: 4 (million)
% 1.79/1.42 % (13075)------------------------------
% 1.79/1.42 % (13075)------------------------------
% 1.79/1.42 % (13074)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_12734 for (2999ds/3Mi)
% 1.79/1.42 % (13068)Instruction limit reached!
% 1.79/1.42 % (13068)------------------------------
% 1.79/1.42 % (13068)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.42 % (13068)Termination reason: Unknown
% 1.79/1.42 % (13068)Termination phase: Saturation
% 1.79/1.42
% 1.79/1.42 % (13068)Memory used [KB]: 5756
% 1.79/1.42 % (13068)Time elapsed: 0.023 s
% 1.79/1.42 % (13068)Instructions burned: 38 (million)
% 1.79/1.42 % (13068)------------------------------
% 1.79/1.42 % (13068)------------------------------
% 1.79/1.42 % (13074)Instruction limit reached!
% 1.79/1.42 % (13074)------------------------------
% 1.79/1.42 % (13074)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.42 % (13074)Termination reason: Unknown
% 1.79/1.42 % (13074)Termination phase: Preprocessing 1
% 1.79/1.42
% 1.79/1.42 % (13074)Memory used [KB]: 1023
% 1.79/1.42 % (13074)Time elapsed: 0.004 s
% 1.79/1.42 % (13074)Instructions burned: 4 (million)
% 1.79/1.42 % (13074)------------------------------
% 1.79/1.42 % (13074)------------------------------
% 1.79/1.43 % (13076)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/7Mi)
% 1.79/1.43 % (13078)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/4Mi)
% 1.79/1.43 % (13076)Instruction limit reached!
% 1.79/1.43 % (13076)------------------------------
% 1.79/1.43 % (13076)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.43 % (13076)Termination reason: Unknown
% 1.79/1.43 % (13076)Termination phase: Saturation
% 1.79/1.43
% 1.79/1.43 % (13076)Memory used [KB]: 5500
% 1.79/1.43 % (13076)Time elapsed: 0.005 s
% 1.79/1.43 % (13076)Instructions burned: 9 (million)
% 1.79/1.43 % (13076)------------------------------
% 1.79/1.43 % (13076)------------------------------
% 1.79/1.43 % (13078)Instruction limit reached!
% 1.79/1.43 % (13078)------------------------------
% 1.79/1.43 % (13078)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.43 % (13078)Termination reason: Unknown
% 1.79/1.43 % (13078)Termination phase: Preprocessing 2
% 1.79/1.43
% 1.79/1.43 % (13078)Memory used [KB]: 1023
% 1.79/1.43 % (13078)Time elapsed: 0.002 s
% 1.79/1.43 % (13078)Instructions burned: 4 (million)
% 1.79/1.43 % (13078)------------------------------
% 1.79/1.43 % (13078)------------------------------
% 1.79/1.43 % (13077)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_12734 for (2999ds/3Mi)
% 1.79/1.43 % (13071)First to succeed.
% 1.79/1.43 % (13077)Instruction limit reached!
% 1.79/1.43 % (13077)------------------------------
% 1.79/1.43 % (13077)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.43 % (13077)Termination reason: Unknown
% 1.79/1.43 % (13077)Termination phase: Property scanning
% 1.79/1.43
% 1.79/1.43 % (13077)Memory used [KB]: 1023
% 1.79/1.43 % (13077)Time elapsed: 0.004 s
% 1.79/1.43 % (13077)Instructions burned: 4 (million)
% 1.79/1.43 % (13077)------------------------------
% 1.79/1.43 % (13077)------------------------------
% 1.79/1.43 % (13071)Refutation found. Thanks to Tanya!
% 1.79/1.43 % SZS status Theorem for DTF2THF_12734
% 1.79/1.43 % SZS output start Proof for DTF2THF_12734
% 1.79/1.43 thf(type_def_6, type, elem: $tType).
% 1.79/1.43 thf(type_def_7, type, nat: $tType).
% 1.79/1.43 thf(type_def_8, type, list: $tType).
% 1.79/1.43 thf(func_def_0, type, isPer: !>[X0: $tType]:((X0 > X0 > $o) > $o)).
% 1.79/1.43 thf(func_def_2, type, elem: $tType).
% 1.79/1.43 thf(func_def_3, type, elemStar: elem > elem > $o).
% 1.79/1.43 thf(func_def_4, type, nat: $tType).
% 1.79/1.43 thf(func_def_5, type, natStar: nat > nat > $o).
% 1.79/1.43 thf(func_def_6, type, zero: nat).
% 1.79/1.43 thf(func_def_7, type, suc: nat > nat).
% 1.79/1.43 thf(func_def_8, type, plus: nat > nat > nat).
% 1.79/1.43 thf(func_def_9, type, list: $tType).
% 1.79/1.43 thf(func_def_10, type, listStar: nat > list > list > $o).
% 1.79/1.43 thf(func_def_11, type, nil: list).
% 1.79/1.43 thf(func_def_12, type, cons: nat > elem > list > list).
% 1.79/1.43 thf(func_def_13, type, app: nat > nat > list > list > list).
% 1.79/1.43 thf(func_def_30, type, ph1: !>[X0: $tType]:(X0)).
% 1.79/1.43 thf(f256,plain,(
% 1.79/1.43 $false),
% 1.79/1.43 inference(trivial_inequality_removal,[status(thm)],[f255])).
% 1.79/1.43 thf(f255,plain,(
% 1.79/1.43 ($true = $false)),
% 1.79/1.43 inference(forward_demodulation,[status(thm)],[f254,f94])).
% 1.79/1.44 thf(f94,plain,(
% 1.79/1.44 ((listStar @ zero @ (app @ zero @ zero @ nil @ nil) @ nil) = $false)),
% 1.79/1.44 inference(not_proxy_clausification,[status(thm)],[f84])).
% 1.79/1.44 thf(f84,plain,(
% 1.79/1.44 ((~ (listStar @ zero @ (app @ zero @ zero @ nil @ nil) @ nil)) = $true)),
% 1.79/1.44 inference(backward_demodulation,[status(thm)],[f68,f83])).
% 1.79/1.44 thf(f83,plain,(
% 1.79/1.44 ( ! [X1 : nat] : (((plus @ zero @ X1) = X1)) )),
% 1.79/1.44 inference(equality_proxy_clausification,[status(thm)],[f82])).
% 1.79/1.44 thf(f82,plain,(
% 1.79/1.44 ( ! [X1 : nat] : ((((plus @ zero @ X1) = X1) = $true)) )),
% 1.79/1.44 inference(beta_eta_normalization,[status(thm)],[f81])).
% 1.79/1.44 thf(f81,plain,(
% 1.79/1.44 ( ! [X1 : nat] : ((((^[Y0 : nat]: ((plus @ zero @ Y0) = Y0)) @ X1) = $true)) )),
% 1.79/1.44 inference(pi_clausification,[status(thm)],[f69])).
% 1.79/1.44 thf(f69,plain,(
% 1.79/1.44 ((!! @ nat @ (^[Y0 : nat]: ((plus @ zero @ Y0) = Y0))) = $true)),
% 1.79/1.44 inference(cnf_transformation,[status(thm)],[f41])).
% 1.79/1.44 thf(f41,plain,(
% 1.79/1.44 ((!! @ nat @ (^[Y0 : nat]: ((plus @ zero @ Y0) = Y0))) = $true)),
% 1.79/1.44 inference(fool_elimination,[status(thm)],[f40])).
% 1.79/1.44 thf(f40,plain,(
% 1.79/1.44 ! [X0 : nat] : ((plus @ zero @ X0) = X0)),
% 1.79/1.44 inference(rectify,[status(thm)],[f12])).
% 1.79/1.44 thf(f12,axiom,(
% 1.79/1.44 ! [X6 : nat] : ((plus @ zero @ X6) = X6)),
% 1.79/1.44 file('/export/starexec/sandbox2/tmp/tmp.xVPkMCFDQR/DTF2THF_12734.p',ax1)).
% 1.79/1.44 thf(f68,plain,(
% 1.79/1.44 ((~ (listStar @ (plus @ zero @ zero) @ (app @ zero @ zero @ nil @ nil) @ nil)) = $true)),
% 1.79/1.44 inference(cnf_transformation,[status(thm)],[f39])).
% 1.79/1.44 thf(f39,plain,(
% 1.79/1.44 ((~ (listStar @ (plus @ zero @ zero) @ (app @ zero @ zero @ nil @ nil) @ nil)) = $true)),
% 1.79/1.44 inference(fool_elimination,[status(thm)],[f38])).
% 1.79/1.44 thf(f38,plain,(
% 1.79/1.44 ~(listStar @ (plus @ zero @ zero) @ (app @ zero @ zero @ nil @ nil) @ nil)),
% 1.79/1.44 inference(rectify,[status(thm)],[f18])).
% 1.79/1.44 thf(f18,negated_conjecture,(
% 1.79/1.44 ~(listStar @ (plus @ zero @ zero) @ (app @ zero @ zero @ nil @ nil) @ nil)),
% 1.79/1.44 inference(negated_conjecture,[status(cth)],[f17])).
% 1.79/1.44 thf(f17,conjecture,(
% 1.79/1.44 (listStar @ (plus @ zero @ zero) @ (app @ zero @ zero @ nil @ nil) @ nil)),
% 1.79/1.44 file('/export/starexec/sandbox2/tmp/tmp.xVPkMCFDQR/DTF2THF_12734.p',list_app_nil_base)).
% 1.79/1.44 thf(f254,plain,(
% 1.79/1.44 ((listStar @ zero @ (app @ zero @ zero @ nil @ nil) @ nil) = $true)),
% 1.79/1.44 inference(boolean_simplification,[status(thm)],[f252])).
% 1.79/1.44 thf(f252,plain,(
% 1.79/1.44 (($true => (listStar @ zero @ (app @ zero @ zero @ nil @ nil) @ nil)) = $true)),
% 1.79/1.44 inference(superposition,[status(thm)],[f242,f60])).
% 1.79/1.44 thf(f60,plain,(
% 1.79/1.44 ((listStar @ zero @ nil @ nil) = $true)),
% 1.79/1.44 inference(cnf_transformation,[status(thm)],[f53])).
% 1.79/1.44 thf(f53,plain,(
% 1.79/1.44 ((listStar @ zero @ nil @ nil) = $true)),
% 1.79/1.44 inference(fool_elimination,[status(thm)],[f52])).
% 1.79/1.44 thf(f52,plain,(
% 1.79/1.44 (listStar @ zero @ nil @ nil)),
% 1.79/1.44 inference(rectify,[status(thm)],[f5])).
% 1.79/1.44 thf(f5,axiom,(
% 1.79/1.44 (listStar @ zero @ nil @ nil)),
% 1.79/1.44 file('/export/starexec/sandbox2/tmp/tmp.xVPkMCFDQR/DTF2THF_12734.p',nil_tp_ax)).
% 1.79/1.44 thf(f242,plain,(
% 1.79/1.44 ( ! [X2 : nat,X1 : list] : ((((listStar @ X2 @ X1 @ X1) => (listStar @ X2 @ (app @ zero @ X2 @ nil @ X1) @ X1)) = $true)) )),
% 1.79/1.44 inference(forward_demodulation,[status(thm)],[f238,f83])).
% 1.79/1.44 thf(f238,plain,(
% 1.79/1.44 ( ! [X2 : nat,X1 : list] : ((((listStar @ X2 @ X1 @ X1) => (listStar @ (plus @ zero @ X2) @ (app @ zero @ X2 @ nil @ X1) @ X1)) = $true)) )),
% 1.79/1.44 inference(beta_eta_normalization,[status(thm)],[f236])).
% 1.79/1.44 thf(f236,plain,(
% 1.79/1.44 ( ! [X2 : nat,X1 : list] : ((((^[Y0 : nat]: ((listStar @ Y0 @ X1 @ X1) => (listStar @ (plus @ zero @ Y0) @ (app @ zero @ Y0 @ nil @ X1) @ X1))) @ X2) = $true)) )),
% 1.79/1.44 inference(pi_clausification,[status(thm)],[f229])).
% 1.79/1.44 thf(f229,plain,(
% 1.79/1.44 ( ! [X1 : list] : (((!! @ nat @ (^[Y0 : nat]: ((listStar @ Y0 @ X1 @ X1) => (listStar @ (plus @ zero @ Y0) @ (app @ zero @ Y0 @ nil @ X1) @ X1)))) = $true)) )),
% 1.79/1.44 inference(beta_eta_normalization,[status(thm)],[f228])).
% 1.79/1.44 thf(f228,plain,(
% 1.79/1.44 ( ! [X1 : list] : ((((^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ nil @ Y0) @ Y0))))) @ X1) = $true)) )),
% 1.79/1.44 inference(pi_clausification,[status(thm)],[f64])).
% 1.79/1.44 thf(f64,plain,(
% 1.79/1.44 ((!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ nil @ Y0) @ Y0)))))) = $true)),
% 1.79/1.44 inference(cnf_transformation,[status(thm)],[f23])).
% 1.79/1.44 thf(f23,plain,(
% 1.79/1.44 ((!! @ list @ (^[Y0 : list]: (!! @ nat @ (^[Y1 : nat]: ((listStar @ Y1 @ Y0 @ Y0) => (listStar @ (plus @ zero @ Y1) @ (app @ zero @ Y1 @ nil @ Y0) @ Y0)))))) = $true)),
% 1.79/1.44 inference(fool_elimination,[status(thm)],[f22])).
% 1.79/1.44 thf(f22,plain,(
% 1.79/1.44 ! [X0 : nat,X1 : list] : ((listStar @ X0 @ X1 @ X1) => (listStar @ (plus @ zero @ X0) @ (app @ zero @ X0 @ nil @ X1) @ X1))),
% 1.79/1.44 inference(rectify,[status(thm)],[f14])).
% 1.79/1.44 thf(f14,axiom,(
% 1.79/1.44 ! [X6 : nat,X2 : list] : ((listStar @ X6 @ X2 @ X2) => (listStar @ (plus @ zero @ X6) @ (app @ zero @ X6 @ nil @ X2) @ X2))),
% 1.79/1.44 file('/export/starexec/sandbox2/tmp/tmp.xVPkMCFDQR/DTF2THF_12734.p',ax3)).
% 1.79/1.44 % SZS output end Proof for DTF2THF_12734
% 1.79/1.44 % (13071)------------------------------
% 1.79/1.44 % (13071)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.79/1.44 % (13071)Termination reason: Refutation
% 1.79/1.44
% 1.79/1.44 % (13071)Memory used [KB]: 5884
% 1.79/1.44 % (13071)Time elapsed: 0.031 s
% 1.79/1.44 % (13071)Instructions burned: 46 (million)
% 1.79/1.44 % (13071)------------------------------
% 1.79/1.44 % (13071)------------------------------
% 1.79/1.44 % (13059)Success in time 0.063 s
%------------------------------------------------------------------------------