%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP236_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n001.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 : Sat Jun 21 05:12:13 AM UTC 2025
% Result : Theorem 33.79s 33.99s
% Output : Proof 34.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ITP236_1 : TPTP v9.0.0. Released v8.0.0.
% 0.11/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n001.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 18:37:34 EDT 2025
% 0.12/0.34 % CPUTime :
% 33.79/33.99 % SZS status Theorem
% 33.79/33.99 % SZS output start Proof
% 33.79/33.99 tff(thesis_type, type, (
% 33.79/33.99 thesis: $o)).
% 33.79/33.99 tff(pp_type, type, (
% 33.79/33.99 pp: bool > $o)).
% 33.79/33.99 tff(aa_nat_bool_type, type, (
% 33.79/33.99 aa_nat_bool: ( fun_nat_bool * nat ) > bool)).
% 33.79/33.99 tff(aa_VEB4832260192069861672t_bool_type, type, (
% 33.79/33.99 aa_VEB4832260192069861672t_bool: ( fun_VE3763956218935105199t_bool * vEBT_VEBT ) > fun_nat_bool)).
% 33.79/33.99 tff(nth_VEBT_VEBT_type, type, (
% 33.79/33.99 nth_VEBT_VEBT: ( list_VEBT_VEBT * nat ) > vEBT_VEBT)).
% 33.79/33.99 tff(maxs_type, type, (
% 33.79/33.99 maxs: nat)).
% 33.79/33.99 tff(treeList_type, type, (
% 33.79/33.99 treeList: list_VEBT_VEBT)).
% 33.79/33.99 tff(vEBT_V8194947554948674370ptions_type, type, (
% 33.79/33.99 vEBT_V8194947554948674370ptions: fun_VE3763956218935105199t_bool)).
% 33.79/33.99 tff(tptp_fun_X_1_0_type, type, (
% 33.79/33.99 tptp_fun_X_1_0: nat)).
% 33.79/33.99 tff(1,plain,
% 33.79/33.99 ((~thesis) <=> (~thesis)),
% 33.79/33.99 inference(rewrite,[status(thm)],[])).
% 33.79/33.99 tff(2,axiom,(~thesis), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','conj_1')).
% 33.79/33.99 tff(3,plain,
% 33.79/33.99 (~thesis),
% 33.79/33.99 inference(modus_ponens,[status(thm)],[2, 1])).
% 33.79/33.99 tff(4,plain,
% 33.79/33.99 (^[X2: nat] : refl((thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2)))) <=> (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2)))))),
% 33.79/33.99 inference(bind,[status(th)],[])).
% 33.79/33.99 tff(5,plain,
% 33.79/33.99 (![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2)))) <=> ![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))),
% 33.79/33.99 inference(quant_intro,[status(thm)],[4])).
% 33.79/33.99 tff(6,plain,
% 33.79/33.99 (![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2)))) <=> ![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))),
% 33.79/33.99 inference(rewrite,[status(thm)],[])).
% 33.79/33.99 tff(7,plain,
% 33.79/33.99 (^[X2: nat] : rewrite((pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2)) => thesis) <=> (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2)))))),
% 33.79/33.99 inference(bind,[status(th)],[])).
% 33.79/33.99 tff(8,plain,
% 33.79/33.99 (![X2: nat] : (pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2)) => thesis) <=> ![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))),
% 33.79/33.99 inference(quant_intro,[status(thm)],[7])).
% 33.79/33.99 tff(9,axiom,(![X2: nat] : (pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2)) => thesis)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','conj_0')).
% 33.79/33.99 tff(10,plain,
% 33.79/33.99 (![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))),
% 33.79/33.99 inference(modus_ponens,[status(thm)],[9, 8])).
% 33.79/33.99 tff(11,plain,
% 33.79/33.99 (![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))),
% 33.79/33.99 inference(modus_ponens,[status(thm)],[10, 6])).
% 33.79/33.99 tff(12,plain,(
% 33.79/33.99 ![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))),
% 33.79/33.99 inference(skolemize,[status(sab)],[11])).
% 33.79/33.99 tff(13,plain,
% 33.79/33.99 (![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))),
% 33.79/33.99 inference(modus_ponens,[status(thm)],[12, 5])).
% 33.79/33.99 tff(14,plain,
% 33.79/33.99 (?[X_1: nat] : pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1)) <=> ?[X_1: nat] : pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1))),
% 34.51/34.78 inference(rewrite,[status(thm)],[])).
% 34.51/34.78 tff(15,axiom,(?[X_1: nat] : pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_0__092_060open_062_092_060exists_062x_O_Aboth__member__options_A_ItreeList_A_B_Amaxs_J_Ax_092_060close_062')).
% 34.51/34.78 tff(16,plain,
% 34.51/34.78 (?[X_1: nat] : pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1))),
% 34.51/34.78 inference(modus_ponens,[status(thm)],[15, 14])).
% 34.51/34.78 tff(17,plain,(
% 34.51/34.78 pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1!0))),
% 34.51/34.78 inference(skolemize,[status(sab)],[16])).
% 34.51/34.78 tff(18,plain,
% 34.51/34.78 (((~![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))) | (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1!0))))) <=> ((~![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))) | thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1!0))))),
% 34.51/34.79 inference(rewrite,[status(thm)],[])).
% 34.51/34.79 tff(19,plain,
% 34.51/34.79 ((~![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))) | (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1!0))))),
% 34.51/34.79 inference(quant_inst,[status(thm)],[])).
% 34.51/34.79 tff(20,plain,
% 34.51/34.79 ((~![X2: nat] : (thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X2))))) | thesis | (~pp(aa_nat_bool(aa_VEB4832260192069861672t_bool(vEBT_V8194947554948674370ptions, nth_VEBT_VEBT(treeList, maxs)), X_1!0)))),
% 34.51/34.79 inference(modus_ponens,[status(thm)],[19, 18])).
% 34.51/34.79 tff(21,plain,
% 34.51/34.79 ($false),
% 34.51/34.79 inference(unit_resolution,[status(thm)],[20, 17, 13, 3])).
% 34.51/34.79 % SZS output end Proof
% 34.62/34.82 % E exiting
%------------------------------------------------------------------------------