%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP276_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:32 AM UTC 2025
% Result : Theorem 6.84s 7.00s
% Output : Proof 7.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : ITP276_1 : TPTP v9.0.0. Released v8.0.0.
% 0.10/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n001.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 19 18:45:19 EDT 2025
% 0.11/0.32 % CPUTime :
% 6.84/7.00 % SZS status Theorem
% 6.84/7.00 % SZS output start Proof
% 6.84/7.00 tff(vEBT_Leaf_type, type, (
% 6.84/7.00 vEBT_Leaf: ( bool * bool ) > vEBT_VEBT)).
% 6.84/7.00 tff(b_type, type, (
% 6.84/7.00 b: bool)).
% 6.84/7.00 tff(a_type, type, (
% 6.84/7.00 a: bool)).
% 6.84/7.00 tff(vEBT_Node_type, type, (
% 6.84/7.00 vEBT_Node: ( option4927543243414619207at_nat * nat * list_VEBT_VEBT * vEBT_VEBT ) > vEBT_VEBT)).
% 6.84/7.00 tff(tptp_fun_Summary3_1073_type, type, (
% 6.84/7.00 tptp_fun_Summary3_1073: vEBT_VEBT)).
% 6.84/7.00 tff(tptp_fun_TreeList3_1074_type, type, (
% 6.84/7.00 tptp_fun_TreeList3_1074: list_VEBT_VEBT)).
% 6.84/7.00 tff(aa_nat_nat_type, type, (
% 6.84/7.00 aa_nat_nat: ( fun_nat_nat * nat ) > nat)).
% 6.84/7.00 tff(zero_zero_nat_type, type, (
% 6.84/7.00 zero_zero_nat: nat)).
% 6.84/7.00 tff(suc_type, type, (
% 6.84/7.00 suc: fun_nat_nat)).
% 6.84/7.00 tff(tptp_fun_Info_1072_type, type, (
% 6.84/7.00 tptp_fun_Info_1072: option4927543243414619207at_nat)).
% 6.84/7.00 tff(sa_type, type, (
% 6.84/7.00 sa: vEBT_VEBT)).
% 6.84/7.00 tff(deg_type, type, (
% 6.84/7.00 deg: nat)).
% 6.84/7.00 tff(pp_type, type, (
% 6.84/7.00 pp: bool > $o)).
% 6.84/7.00 tff(aa_set8260762808118238015T_bool_type, type, (
% 6.84/7.00 aa_set8260762808118238015T_bool: ( fun_se448528567104302406T_bool * set_VEBT_VEBT ) > bool)).
% 6.84/7.00 tff(set_VEBT_VEBT2_type, type, (
% 6.84/7.00 set_VEBT_VEBT2: list_VEBT_VEBT > set_VEBT_VEBT)).
% 6.84/7.00 tff(aa_VEB289770264548726718T_bool_type, type, (
% 6.84/7.00 aa_VEB289770264548726718T_bool: ( fun_VE7346385682144900493T_bool * vEBT_VEBT ) > fun_se448528567104302406T_bool)).
% 6.84/7.00 tff(member_VEBT_VEBT_type, type, (
% 6.84/7.00 member_VEBT_VEBT: fun_VE7346385682144900493T_bool)).
% 6.84/7.00 tff(aa_nat_bool_type, type, (
% 6.84/7.00 aa_nat_bool: ( fun_nat_bool * nat ) > bool)).
% 6.84/7.00 tff(na_type, type, (
% 6.84/7.00 na: nat)).
% 6.84/7.00 tff(vEBT_invar_vebt_type, type, (
% 6.84/7.00 vEBT_invar_vebt: vEBT_VEBT > fun_nat_bool)).
% 6.84/7.00 tff(m_type, type, (
% 6.84/7.00 m: nat)).
% 6.84/7.00 tff(aa_nat_fun_nat_nat_type, type, (
% 6.84/7.00 aa_nat_fun_nat_nat: ( fun_nat_fun_nat_nat * nat ) > fun_nat_nat)).
% 6.84/7.00 tff(aa_num_nat_type, type, (
% 6.84/7.00 aa_num_nat: ( fun_num_nat * num ) > nat)).
% 6.84/7.00 tff(aa_num_num_type, type, (
% 6.84/7.00 aa_num_num: ( fun_num_num * num ) > num)).
% 6.84/7.00 tff(one_type, type, (
% 6.84/7.00 one: num)).
% 6.84/7.00 tff(bit0_type, type, (
% 6.84/7.00 bit0: fun_num_num)).
% 6.84/7.00 tff(numeral_numeral_nat_type, type, (
% 6.84/7.00 numeral_numeral_nat: fun_num_nat)).
% 6.84/7.00 tff(power_power_nat_type, type, (
% 6.84/7.00 power_power_nat: fun_nat_fun_nat_nat)).
% 6.84/7.00 tff(size_s6755466524823107622T_VEBT_type, type, (
% 6.84/7.00 size_s6755466524823107622T_VEBT: list_VEBT_VEBT > nat)).
% 6.84/7.00 tff(plus_plus_nat_type, type, (
% 6.84/7.00 plus_plus_nat: fun_nat_fun_nat_nat)).
% 6.84/7.00 tff(1,plain,
% 6.84/7.00 ((sa = vEBT_Leaf(a, b)) <=> (sa = vEBT_Leaf(a, b))),
% 6.84/7.00 inference(rewrite,[status(thm)],[])).
% 6.84/7.00 tff(2,axiom,(sa = vEBT_Leaf(a, b)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_274__C1_C_I1_J')).
% 6.84/7.00 tff(3,plain,
% 6.84/7.00 (sa = vEBT_Leaf(a, b)),
% 6.84/7.00 inference(modus_ponens,[status(thm)],[2, 1])).
% 6.84/7.00 tff(4,plain,
% 6.84/7.00 (((sa = vEBT_Node(Info!1072, deg, TreeList3!1074, Summary3!1073)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3!1074) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3!1073), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3!1074)))))) <=> ((sa = vEBT_Node(Info!1072, deg, TreeList3!1074, Summary3!1073)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3!1074) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3!1073), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3!1074))))))),
% 6.84/7.00 inference(rewrite,[status(thm)],[])).
% 6.84/7.00 tff(5,plain,
% 6.84/7.00 ((~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3)))))))) <=> (~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3))))))))),
% 6.84/7.00 inference(rewrite,[status(thm)],[])).
% 6.84/7.00 tff(6,plain,
% 6.84/7.00 ((~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~(((((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m))) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m))) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m))) & ![X5: vEBT_VEBT] : (pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3))) => pp(aa_nat_bool(vEBT_invar_vebt(X5), na)))))) <=> (~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3))))))))),
% 6.84/7.00 inference(rewrite,[status(thm)],[])).
% 6.84/7.00 tff(7,axiom,(~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~(((((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m))) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m))) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m))) & ![X5: vEBT_VEBT] : (pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3))) => pp(aa_nat_bool(vEBT_invar_vebt(X5), na)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_2970__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062treeList_H_Asummary_H_Ainfo_O_As_A_061_ANode_Ainfo_Adeg_AtreeList_H_Asummary_H_A_092_060and_062_Adeg_A_061_An_A_L_Am_A_092_060and_062_Alength_AtreeList_H_A_061_A2_A_094_Am_A_092_060and_062_Ainvar__vebt_Asummary_H_Am_A_092_060and_062_A_I_092_060forall_062t_092_060in_062set_AtreeList_H_O_Ainvar__vebt_At_An_J_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062')).
% 6.84/7.00 tff(8,plain,
% 6.84/7.00 (~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3)))))))),
% 6.84/7.00 inference(modus_ponens,[status(thm)],[7, 6])).
% 6.84/7.00 tff(9,plain,
% 6.84/7.00 (~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3)))))))),
% 6.84/7.00 inference(modus_ponens,[status(thm)],[8, 5])).
% 6.84/7.00 tff(10,plain,
% 6.84/7.00 (~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3)))))))),
% 6.84/7.00 inference(modus_ponens,[status(thm)],[9, 5])).
% 6.84/7.00 tff(11,plain,
% 6.84/7.00 (~![TreeList3: list_VEBT_VEBT, Summary3: vEBT_VEBT, Info: option4927543243414619207at_nat] : (~((sa = vEBT_Node(Info, deg, TreeList3, Summary3)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3)))))))),
% 6.84/7.00 inference(modus_ponens,[status(thm)],[10, 5])).
% 6.84/7.00 tff(12,plain,(
% 6.84/7.00 $oeq((~(~((sa = vEBT_Node(Info!1072, deg, TreeList3!1074, Summary3!1073)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3!1074) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3!1073), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3!1074)))))))), ((sa = vEBT_Node(Info!1072, deg, TreeList3!1074, Summary3!1073)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3!1074) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3!1073), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3!1074)))))))),
% 6.84/7.00 inference(transitivity,[status(sab)],[11])).
% 6.84/7.00 tff(13,plain,
% 6.84/7.00 ((sa = vEBT_Node(Info!1072, deg, TreeList3!1074, Summary3!1073)) & (deg = aa_nat_nat(aa_nat_fun_nat_nat(plus_plus_nat, na), m)) & (size_s6755466524823107622T_VEBT(TreeList3!1074) = aa_nat_nat(aa_nat_fun_nat_nat(power_power_nat, aa_num_nat(numeral_numeral_nat, aa_num_num(bit0, one))), m)) & pp(aa_nat_bool(vEBT_invar_vebt(Summary3!1073), m)) & ![X5: vEBT_VEBT] : (pp(aa_nat_bool(vEBT_invar_vebt(X5), na)) | (~pp(aa_set8260762808118238015T_bool(aa_VEB289770264548726718T_bool(member_VEBT_VEBT, X5), set_VEBT_VEBT2(TreeList3!1074)))))),
% 6.84/7.00 inference(modus_ponens,[status(thm)],[12, 4])).
% 6.84/7.00 tff(14,plain,
% 6.84/7.00 (sa = vEBT_Node(Info!1072, deg, TreeList3!1074, Summary3!1073)),
% 6.84/7.00 inference(and_elim,[status(thm)],[13])).
% 6.84/7.00 tff(15,plain,
% 6.84/7.00 (vEBT_Node(Info!1072, deg, TreeList3!1074, Summary3!1073) = sa),
% 6.84/7.00 inference(symmetry,[status(thm)],[14])).
% 6.84/7.00 tff(16,plain,
% 6.84/7.00 ((deg = aa_nat_nat(suc, zero_zero_nat)) <=> (deg = aa_nat_nat(suc, zero_zero_nat))),
% 6.84/7.00 inference(rewrite,[status(thm)],[])).
% 6.84/7.00 tff(17,axiom,(deg = aa_nat_nat(suc, zero_zero_nat)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_75__C1_C_I2_J')).
% 7.56/7.73 tff(18,plain,
% 7.56/7.73 (deg = aa_nat_nat(suc, zero_zero_nat)),
% 7.56/7.73 inference(modus_ponens,[status(thm)],[17, 16])).
% 7.56/7.73 tff(19,plain,
% 7.56/7.73 (aa_nat_nat(suc, zero_zero_nat) = deg),
% 7.56/7.73 inference(symmetry,[status(thm)],[18])).
% 7.56/7.73 tff(20,plain,
% 7.56/7.73 (vEBT_Node(Info!1072, aa_nat_nat(suc, zero_zero_nat), TreeList3!1074, Summary3!1073) = vEBT_Node(Info!1072, deg, TreeList3!1074, Summary3!1073)),
% 7.56/7.73 inference(monotonicity,[status(thm)],[19])).
% 7.56/7.73 tff(21,plain,
% 7.56/7.73 (vEBT_Node(Info!1072, aa_nat_nat(suc, zero_zero_nat), TreeList3!1074, Summary3!1073) = vEBT_Leaf(a, b)),
% 7.56/7.73 inference(transitivity,[status(thm)],[20, 15, 3])).
% 7.56/7.73 tff(22,plain,
% 7.56/7.73 (^[X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : refl((~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22))) <=> (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22))))),
% 7.56/7.73 inference(bind,[status(th)],[])).
% 7.56/7.73 tff(23,plain,
% 7.56/7.73 (![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22))) <=> ![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22)))),
% 7.56/7.73 inference(quant_intro,[status(thm)],[22])).
% 7.56/7.73 tff(24,plain,
% 7.56/7.73 (![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22))) <=> ![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22)))),
% 7.56/7.73 inference(rewrite,[status(thm)],[])).
% 7.56/7.73 tff(25,axiom,(![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','fact_984_VEBT_Odistinct_I1_J')).
% 7.56/7.73 tff(26,plain,
% 7.56/7.73 (![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22)))),
% 7.56/7.73 inference(modus_ponens,[status(thm)],[25, 24])).
% 7.56/7.73 tff(27,plain,(
% 7.56/7.73 ![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22)))),
% 7.56/7.73 inference(skolemize,[status(sab)],[26])).
% 7.56/7.73 tff(28,plain,
% 7.56/7.73 (![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22)))),
% 7.56/7.73 inference(modus_ponens,[status(thm)],[27, 23])).
% 7.56/7.73 tff(29,plain,
% 7.56/7.73 ((~![X11: option4927543243414619207at_nat, X12: nat, X13: list_VEBT_VEBT, X14: vEBT_VEBT, X21: bool, X22: bool] : (~(vEBT_Node(X11, X12, X13, X14) = vEBT_Leaf(X21, X22)))) | (~(vEBT_Node(Info!1072, aa_nat_nat(suc, zero_zero_nat), TreeList3!1074, Summary3!1073) = vEBT_Leaf(a, b)))),
% 7.56/7.73 inference(quant_inst,[status(thm)],[])).
% 7.56/7.73 tff(30,plain,
% 7.56/7.73 (~(vEBT_Node(Info!1072, aa_nat_nat(suc, zero_zero_nat), TreeList3!1074, Summary3!1073) = vEBT_Leaf(a, b))),
% 7.56/7.73 inference(unit_resolution,[status(thm)],[29, 28])).
% 7.56/7.73 tff(31,plain,
% 7.56/7.73 ($false),
% 7.56/7.73 inference(unit_resolution,[status(thm)],[30, 21])).
% 7.56/7.73 % SZS output end Proof
% 7.56/7.77 % E exiting
%------------------------------------------------------------------------------