%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM225_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n016.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 : Tue May 5 06:23:01 PM UTC 2026
% Result : Theorem 105.17s 105.48s
% Output : Proof 105.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM225_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.15/0.33 % Computer : n016.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 19:08:23 EDT 2026
% 0.15/0.33 % CPUTime :
% 105.17/105.48 % SZS status Theorem
% 105.17/105.48 % SZS output start Proof
% 105.17/105.48 tff(vSucc_type, type, (
% 105.17/105.48 vSucc: vTerm > vTerm)).
% 105.17/105.48 tff(tptp_fun_Vnv00_62_type, type, (
% 105.17/105.48 tptp_fun_Vnv00_62: vTerm)).
% 105.17/105.48 tff(vt1_type, type, (
% 105.17/105.48 vt1: vTerm)).
% 105.17/105.48 tff(visSomeTerm_type, type, (
% 105.17/105.48 visSomeTerm: vOptTerm > $o)).
% 105.17/105.48 tff(vreduce_type, type, (
% 105.17/105.48 vreduce: vTerm > vOptTerm)).
% 105.17/105.48 tff(tptp_fun_Vnv00_15_type, type, (
% 105.17/105.48 tptp_fun_Vnv00_15: vTerm > vTerm)).
% 105.17/105.48 tff(vptchecksimple_type, type, (
% 105.17/105.48 vptchecksimple: ( vTerm * vTy ) > $o)).
% 105.17/105.48 tff(tptp_fun_VT_64_type, type, (
% 105.17/105.48 tptp_fun_VT_64: vTy)).
% 105.17/105.48 tff(tptp_fun_Vtres_63_type, type, (
% 105.17/105.48 tptp_fun_Vtres_63: vTerm)).
% 105.17/105.48 tff(vsomeTerm_type, type, (
% 105.17/105.48 vsomeTerm: vTerm > vOptTerm)).
% 105.17/105.48 tff(vPred_type, type, (
% 105.17/105.48 vPred: vTerm > vTerm)).
% 105.17/105.48 tff(vZero_type, type, (
% 105.17/105.48 vZero: vTerm)).
% 105.17/105.48 tff(vnoTerm_type, type, (
% 105.17/105.48 vnoTerm: vOptTerm)).
% 105.17/105.48 tff(1,assumption,(vt1 = vSucc(tptp_fun_Vnv00_15(vt1))), introduced(assumption)).
% 105.17/105.48 tff(2,plain,
% 105.17/105.48 (^[Vnv0: vTerm] : refl((~(vt1 = vSucc(Vnv0))) <=> (~(vt1 = vSucc(Vnv0))))),
% 105.17/105.48 inference(bind,[status(th)],[])).
% 105.17/105.48 tff(3,plain,
% 105.17/105.48 (![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) <=> ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0)))),
% 105.17/105.48 inference(quant_intro,[status(thm)],[2])).
% 105.17/105.48 tff(4,plain,
% 105.17/105.48 ((((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))) & (~vptchecksimple(Vtres!63, VT!64))) <=> ((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63)) & (~vptchecksimple(Vtres!63, VT!64)))),
% 105.17/105.48 inference(rewrite,[status(thm)],[])).
% 105.17/105.48 tff(5,plain,
% 105.17/105.48 (((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))) <=> ((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63)))),
% 105.17/105.48 inference(rewrite,[status(thm)],[])).
% 105.17/105.48 tff(6,plain,
% 105.17/105.48 ((((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))) & (~vptchecksimple(Vtres!63, VT!64))) <=> (((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))) & (~vptchecksimple(Vtres!63, VT!64)))),
% 105.17/105.48 inference(monotonicity,[status(thm)],[5])).
% 105.17/105.48 tff(7,plain,
% 105.17/105.48 ((((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))) & (~vptchecksimple(Vtres!63, VT!64))) <=> ((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63)) & (~vptchecksimple(Vtres!63, VT!64)))),
% 105.17/105.48 inference(transitivity,[status(thm)],[6, 4])).
% 105.17/105.48 tff(8,plain,
% 105.17/105.48 ((~![VT: vTy, Vtres: vTerm] : ((~((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))) <=> (~![VT: vTy, Vtres: vTerm] : ((~((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)))),
% 105.17/105.48 inference(rewrite,[status(thm)],[])).
% 105.17/105.48 tff(9,plain,
% 105.17/105.48 ((~![VT: vTy, Vtres: vTerm] : (((((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0)))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT))) <=> (~![VT: vTy, Vtres: vTerm] : ((~((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)))),
% 105.17/105.48 inference(rewrite,[status(thm)],[])).
% 105.17/105.48 tff(10,axiom,(~![VT: vTy, Vtres: vTerm] : (((((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0)))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''Preservation-Pred-t1'')).
% 105.17/105.48 tff(11,plain,
% 105.17/105.48 (~![VT: vTy, Vtres: vTerm] : ((~((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[10, 9])).
% 105.17/105.48 tff(12,plain,
% 105.17/105.48 (~![VT: vTy, Vtres: vTerm] : ((~((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[11, 8])).
% 105.17/105.48 tff(13,plain,
% 105.17/105.48 (~![VT: vTy, Vtres: vTerm] : ((~((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[12, 8])).
% 105.17/105.48 tff(14,plain,
% 105.17/105.48 (~![VT: vTy, Vtres: vTerm] : ((~((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[13, 8])).
% 105.17/105.48 tff(15,plain,
% 105.17/105.48 ((~(vt1 = vZero)) & ![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0))) & vptchecksimple(vPred(vt1), VT!64) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63)) & (~vptchecksimple(Vtres!63, VT!64))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[14, 7])).
% 105.17/105.48 tff(16,plain,
% 105.17/105.48 (![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0)))),
% 105.17/105.48 inference(and_elim,[status(thm)],[15])).
% 105.17/105.48 tff(17,plain,
% 105.17/105.48 (![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0)))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[16, 3])).
% 105.17/105.48 tff(18,plain,
% 105.17/105.48 ((~![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0)))) | (~(vt1 = vSucc(tptp_fun_Vnv00_15(vt1))))),
% 105.17/105.48 inference(quant_inst,[status(thm)],[])).
% 105.17/105.48 tff(19,plain,
% 105.17/105.48 ($false),
% 105.17/105.48 inference(unit_resolution,[status(thm)],[18, 17, 1])).
% 105.17/105.48 tff(20,plain,(~(vt1 = vSucc(tptp_fun_Vnv00_15(vt1)))), inference(lemma,lemma(discharge,[]))).
% 105.17/105.48 tff(21,plain,
% 105.17/105.48 ((vnoTerm = vreduce(vPred(vt1))) <=> (vreduce(vPred(vt1)) = vnoTerm)),
% 105.17/105.48 inference(commutativity,[status(thm)],[])).
% 105.17/105.48 tff(22,plain,
% 105.17/105.48 (vreduce(vPred(vt1)) = vsomeTerm(Vtres!63)),
% 105.17/105.48 inference(and_elim,[status(thm)],[15])).
% 105.17/105.48 tff(23,plain,
% 105.17/105.48 (vsomeTerm(Vtres!63) = vreduce(vPred(vt1))),
% 105.17/105.48 inference(symmetry,[status(thm)],[22])).
% 105.17/105.48 tff(24,plain,
% 105.17/105.48 ((vnoTerm = vsomeTerm(Vtres!63)) <=> (vnoTerm = vreduce(vPred(vt1)))),
% 105.17/105.48 inference(monotonicity,[status(thm)],[23])).
% 105.17/105.48 tff(25,plain,
% 105.17/105.48 ((vnoTerm = vsomeTerm(Vtres!63)) <=> (vreduce(vPred(vt1)) = vnoTerm)),
% 105.17/105.48 inference(transitivity,[status(thm)],[24, 21])).
% 105.17/105.48 tff(26,plain,
% 105.17/105.48 ((~(vnoTerm = vsomeTerm(Vtres!63))) <=> (~(vreduce(vPred(vt1)) = vnoTerm))),
% 105.17/105.48 inference(monotonicity,[status(thm)],[25])).
% 105.17/105.48 tff(27,plain,
% 105.17/105.48 (^[VTerm0: vTerm] : refl((~(vnoTerm = vsomeTerm(VTerm0))) <=> (~(vnoTerm = vsomeTerm(VTerm0))))),
% 105.17/105.48 inference(bind,[status(th)],[])).
% 105.17/105.48 tff(28,plain,
% 105.17/105.48 (![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0))) <=> ![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0)))),
% 105.17/105.48 inference(quant_intro,[status(thm)],[27])).
% 105.17/105.48 tff(29,plain,
% 105.17/105.48 (![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0))) <=> ![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0)))),
% 105.17/105.48 inference(rewrite,[status(thm)],[])).
% 105.17/105.48 tff(30,axiom,(![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''DIFF-noTerm-someTerm'')).
% 105.17/105.48 tff(31,plain,
% 105.17/105.48 (![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0)))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[30, 29])).
% 105.17/105.48 tff(32,plain,(
% 105.17/105.48 ![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0)))),
% 105.17/105.48 inference(skolemize,[status(sab)],[31])).
% 105.17/105.48 tff(33,plain,
% 105.17/105.48 (![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0)))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[32, 28])).
% 105.17/105.48 tff(34,plain,
% 105.17/105.48 ((~![VTerm0: vTerm] : (~(vnoTerm = vsomeTerm(VTerm0)))) | (~(vnoTerm = vsomeTerm(Vtres!63)))),
% 105.17/105.48 inference(quant_inst,[status(thm)],[])).
% 105.17/105.48 tff(35,plain,
% 105.17/105.48 (~(vnoTerm = vsomeTerm(Vtres!63))),
% 105.17/105.48 inference(unit_resolution,[status(thm)],[34, 33])).
% 105.17/105.48 tff(36,plain,
% 105.17/105.48 (~(vreduce(vPred(vt1)) = vnoTerm)),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[35, 26])).
% 105.17/105.48 tff(37,plain,
% 105.17/105.48 (~(vt1 = vZero)),
% 105.17/105.48 inference(and_elim,[status(thm)],[15])).
% 105.17/105.48 tff(38,plain,
% 105.17/105.48 (^[Vt1: vTerm] : refl(((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1)))) <=> ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1)))))),
% 105.17/105.48 inference(bind,[status(th)],[])).
% 105.17/105.48 tff(39,plain,
% 105.17/105.48 (![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1)))) <=> ![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))),
% 105.17/105.48 inference(quant_intro,[status(thm)],[38])).
% 105.17/105.48 tff(40,plain,
% 105.17/105.48 (^[Vt1: vTerm] : trans(monotonicity(rewrite(((Vt1 = vZero) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))) | visSomeTerm(vreduce(Vt1))) <=> ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))), ((((Vt1 = vZero) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))) | visSomeTerm(vreduce(Vt1))) | (vreduce(vPred(Vt1)) = vnoTerm)) <=> (((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1)))) | (vreduce(vPred(Vt1)) = vnoTerm)))), rewrite((((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1)))) | (vreduce(vPred(Vt1)) = vnoTerm)) <=> ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))), ((((Vt1 = vZero) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))) | visSomeTerm(vreduce(Vt1))) | (vreduce(vPred(Vt1)) = vnoTerm)) <=> ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))))),
% 105.17/105.48 inference(bind,[status(th)],[])).
% 105.17/105.48 tff(41,plain,
% 105.17/105.48 (![Vt1: vTerm] : (((Vt1 = vZero) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))) | visSomeTerm(vreduce(Vt1))) | (vreduce(vPred(Vt1)) = vnoTerm)) <=> ![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))),
% 105.17/105.48 inference(quant_intro,[status(thm)],[40])).
% 105.17/105.48 tff(42,plain,
% 105.17/105.48 (![Vt1: vTerm] : ((~((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1))))) | (vreduce(vPred(Vt1)) = vnoTerm)) <=> ![Vt1: vTerm] : ((~((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1))))) | (vreduce(vPred(Vt1)) = vnoTerm))),
% 105.17/105.48 inference(rewrite,[status(thm)],[])).
% 105.17/105.48 tff(43,plain,
% 105.17/105.48 (^[Vt1: vTerm] : trans(monotonicity(trans(monotonicity(rewrite(((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) <=> ((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))))), ((((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) & (~visSomeTerm(vreduce(Vt1)))) <=> (((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) & (~visSomeTerm(vreduce(Vt1)))))), rewrite((((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) & (~visSomeTerm(vreduce(Vt1)))) <=> ((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1))))), ((((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) & (~visSomeTerm(vreduce(Vt1)))) <=> ((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1)))))), (((((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) & (~visSomeTerm(vreduce(Vt1)))) => (vreduce(vPred(Vt1)) = vnoTerm)) <=> (((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1)))) => (vreduce(vPred(Vt1)) = vnoTerm)))), rewrite((((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1)))) => (vreduce(vPred(Vt1)) = vnoTerm)) <=> ((~((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1))))) | (vreduce(vPred(Vt1)) = vnoTerm))), (((((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) & (~visSomeTerm(vreduce(Vt1)))) => (vreduce(vPred(Vt1)) = vnoTerm)) <=> ((~((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1))))) | (vreduce(vPred(Vt1)) = vnoTerm))))),
% 105.17/105.48 inference(bind,[status(th)],[])).
% 105.17/105.48 tff(44,plain,
% 105.17/105.48 (![Vt1: vTerm] : ((((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) & (~visSomeTerm(vreduce(Vt1)))) => (vreduce(vPred(Vt1)) = vnoTerm)) <=> ![Vt1: vTerm] : ((~((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1))))) | (vreduce(vPred(Vt1)) = vnoTerm))),
% 105.17/105.48 inference(quant_intro,[status(thm)],[43])).
% 105.17/105.48 tff(45,axiom,(![Vt1: vTerm] : ((((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00)))) & (~visSomeTerm(vreduce(Vt1)))) => (vreduce(vPred(Vt1)) = vnoTerm))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''reduce-11'')).
% 105.17/105.48 tff(46,plain,
% 105.17/105.48 (![Vt1: vTerm] : ((~((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1))))) | (vreduce(vPred(Vt1)) = vnoTerm))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[45, 44])).
% 105.17/105.48 tff(47,plain,
% 105.17/105.48 (![Vt1: vTerm] : ((~((~(Vt1 = vZero)) & ![Vnv00: vTerm] : (~(Vt1 = vSucc(Vnv00))) & (~visSomeTerm(vreduce(Vt1))))) | (vreduce(vPred(Vt1)) = vnoTerm))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[46, 42])).
% 105.17/105.48 tff(48,plain,(
% 105.17/105.48 ![Vt1: vTerm] : (((Vt1 = vZero) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))) | visSomeTerm(vreduce(Vt1))) | (vreduce(vPred(Vt1)) = vnoTerm))),
% 105.17/105.48 inference(skolemize,[status(sab)],[47])).
% 105.17/105.48 tff(49,plain,
% 105.17/105.48 (![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[48, 41])).
% 105.17/105.48 tff(50,plain,
% 105.17/105.48 (![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))),
% 105.17/105.48 inference(modus_ponens,[status(thm)],[49, 39])).
% 105.17/105.48 tff(51,plain,
% 105.17/105.48 (((~![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))) | (visSomeTerm(vreduce(vt1)) | (vt1 = vZero) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1))))) <=> ((~![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))) | visSomeTerm(vreduce(vt1)) | (vt1 = vZero) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1))))),
% 105.17/105.48 inference(rewrite,[status(thm)],[])).
% 105.17/105.48 tff(52,plain,
% 105.17/105.48 (((vt1 = vZero) | visSomeTerm(vreduce(vt1)) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1)))) <=> (visSomeTerm(vreduce(vt1)) | (vt1 = vZero) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1))))),
% 105.17/105.48 inference(rewrite,[status(thm)],[])).
% 105.17/105.48 tff(53,plain,
% 105.17/105.48 (((~![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))) | ((vt1 = vZero) | visSomeTerm(vreduce(vt1)) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1))))) <=> ((~![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))) | (visSomeTerm(vreduce(vt1)) | (vt1 = vZero) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1)))))),
% 105.17/105.48 inference(monotonicity,[status(thm)],[52])).
% 105.17/105.48 tff(54,plain,
% 105.17/105.48 (((~![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))) | ((vt1 = vZero) | visSomeTerm(vreduce(vt1)) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1))))) <=> ((~![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))) | visSomeTerm(vreduce(vt1)) | (vt1 = vZero) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1))))),
% 105.17/105.48 inference(transitivity,[status(thm)],[53, 51])).
% 105.17/105.48 tff(55,plain,
% 105.17/105.48 ((~![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))) | ((vt1 = vZero) | visSomeTerm(vreduce(vt1)) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1))))),
% 105.17/105.48 inference(quant_inst,[status(thm)],[])).
% 105.17/105.48 tff(56,plain,
% 105.17/105.48 ((~![Vt1: vTerm] : ((Vt1 = vZero) | visSomeTerm(vreduce(Vt1)) | (vreduce(vPred(Vt1)) = vnoTerm) | (Vt1 = vSucc(tptp_fun_Vnv00_15(Vt1))))) | visSomeTerm(vreduce(vt1)) | (vt1 = vZero) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1)))),
% 105.17/105.49 inference(modus_ponens,[status(thm)],[55, 54])).
% 105.17/105.49 tff(57,plain,
% 105.17/105.49 (visSomeTerm(vreduce(vt1)) | (vreduce(vPred(vt1)) = vnoTerm) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1)))),
% 105.17/105.49 inference(unit_resolution,[status(thm)],[56, 50, 37])).
% 105.17/105.49 tff(58,plain,
% 105.17/105.49 (visSomeTerm(vreduce(vt1)) | (vt1 = vSucc(tptp_fun_Vnv00_15(vt1)))),
% 105.17/105.49 inference(unit_resolution,[status(thm)],[57, 36])).
% 105.17/105.49 tff(59,plain,
% 105.17/105.49 (visSomeTerm(vreduce(vt1))),
% 105.17/105.49 inference(unit_resolution,[status(thm)],[58, 20])).
% 105.17/105.49 tff(60,plain,
% 105.17/105.49 (~vptchecksimple(Vtres!63, VT!64)),
% 105.17/105.49 inference(and_elim,[status(thm)],[15])).
% 105.17/105.49 tff(61,plain,
% 105.17/105.49 (vptchecksimple(vPred(vt1), VT!64)),
% 105.17/105.49 inference(and_elim,[status(thm)],[15])).
% 105.17/105.49 tff(62,plain,
% 105.17/105.49 (^[VT: vTy, Vtres: vTerm] : refl((vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) <=> (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))))),
% 105.17/105.49 inference(bind,[status(th)],[])).
% 105.17/105.49 tff(63,plain,
% 105.17/105.49 (![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) <=> ![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))),
% 105.17/105.49 inference(quant_intro,[status(thm)],[62])).
% 105.17/105.49 tff(64,plain,
% 105.17/105.49 (^[VT: vTy, Vtres: vTerm] : trans(monotonicity(rewrite(((~visSomeTerm(vreduce(vt1))) | (vt1 = vZero) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) <=> ((vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))), ((((~visSomeTerm(vreduce(vt1))) | (vt1 = vZero) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> (((vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)))), rewrite((((vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))), ((((~visSomeTerm(vreduce(vt1))) | (vt1 = vZero) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))))),
% 105.17/105.49 inference(bind,[status(th)],[])).
% 105.17/105.49 tff(65,plain,
% 105.17/105.49 (![VT: vTy, Vtres: vTerm] : (((~visSomeTerm(vreduce(vt1))) | (vt1 = vZero) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> ![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))),
% 105.17/105.49 inference(quant_intro,[status(thm)],[64])).
% 105.17/105.49 tff(66,plain,
% 105.17/105.49 (![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT)) <=> ![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.49 inference(rewrite,[status(thm)],[])).
% 105.17/105.49 tff(67,plain,
% 105.17/105.49 (^[VT: vTy, Vtres: vTerm] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) <=> (visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))))), ((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) <=> ((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)))), rewrite(((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) <=> (visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT))), ((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) <=> (visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT)))), (((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) <=> ((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))))), rewrite(((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) <=> (visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))), (((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) <=> (visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))))), ((((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT)) <=> ((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT)))), rewrite(((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT)) <=> ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))), ((((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT)) <=> ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))))),
% 105.17/105.49 inference(bind,[status(th)],[])).
% 105.17/105.49 tff(68,plain,
% 105.17/105.49 (![VT: vTy, Vtres: vTerm] : (((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT)) <=> ![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.49 inference(quant_intro,[status(thm)],[67])).
% 105.17/105.49 tff(69,axiom,(![VT: vTy, Vtres: vTerm] : (((((visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero))) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00)))) & vptchecksimple(vPred(vt1), VT)) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres))) => vptchecksimple(Vtres, VT))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''Preservation-Pred-t1-isSomeTerm-True'')).
% 105.17/105.49 tff(70,plain,
% 105.17/105.49 (![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.49 inference(modus_ponens,[status(thm)],[69, 68])).
% 105.17/105.49 tff(71,plain,
% 105.17/105.49 (![VT: vTy, Vtres: vTerm] : ((~(visSomeTerm(vreduce(vt1)) & (~(vt1 = vZero)) & ![Vnv00: vTerm] : (~(vt1 = vSucc(Vnv00))) & vptchecksimple(vPred(vt1), VT) & (vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.49 inference(modus_ponens,[status(thm)],[70, 66])).
% 105.17/105.49 tff(72,plain,(
% 105.17/105.49 ![VT: vTy, Vtres: vTerm] : (((~visSomeTerm(vreduce(vt1))) | (vt1 = vZero) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres)))) | vptchecksimple(Vtres, VT))),
% 105.17/105.49 inference(skolemize,[status(sab)],[71])).
% 105.17/105.49 tff(73,plain,
% 105.17/105.49 (![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))),
% 105.17/105.49 inference(modus_ponens,[status(thm)],[72, 65])).
% 105.17/105.49 tff(74,plain,
% 105.17/105.49 (![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))),
% 105.17/105.49 inference(modus_ponens,[status(thm)],[73, 63])).
% 105.17/105.49 tff(75,plain,
% 105.17/105.49 (((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))) | ((vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | vptchecksimple(Vtres!63, VT!64) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))))) <=> ((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | vptchecksimple(Vtres!63, VT!64) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))))),
% 105.17/105.49 inference(rewrite,[status(thm)],[])).
% 105.17/105.49 tff(76,plain,
% 105.17/105.49 ((vptchecksimple(Vtres!63, VT!64) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63)))) <=> ((vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | vptchecksimple(Vtres!63, VT!64) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))))),
% 105.17/105.49 inference(rewrite,[status(thm)],[])).
% 105.17/105.49 tff(77,plain,
% 105.17/105.49 (((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))) | (vptchecksimple(Vtres!63, VT!64) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))))) <=> ((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))) | ((vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | vptchecksimple(Vtres!63, VT!64) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63)))))),
% 105.28/105.51 inference(monotonicity,[status(thm)],[76])).
% 105.28/105.51 tff(78,plain,
% 105.28/105.51 (((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))) | (vptchecksimple(Vtres!63, VT!64) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))))) <=> ((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | vptchecksimple(Vtres!63, VT!64) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))))),
% 105.28/105.51 inference(transitivity,[status(thm)],[77, 75])).
% 105.28/105.51 tff(79,plain,
% 105.28/105.51 ((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))) | (vptchecksimple(Vtres!63, VT!64) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63))))),
% 105.28/105.51 inference(quant_inst,[status(thm)],[])).
% 105.28/105.51 tff(80,plain,
% 105.28/105.51 ((~![VT: vTy, Vtres: vTerm] : (vptchecksimple(Vtres, VT) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | (~vptchecksimple(vPred(vt1), VT)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres))))) | (vt1 = vZero) | (~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62)) | vptchecksimple(Vtres!63, VT!64) | (~vptchecksimple(vPred(vt1), VT!64)) | (~(vreduce(vPred(vt1)) = vsomeTerm(Vtres!63)))),
% 105.28/105.51 inference(modus_ponens,[status(thm)],[79, 78])).
% 105.28/105.51 tff(81,plain,
% 105.28/105.51 ((~visSomeTerm(vreduce(vt1))) | (vt1 = vSucc(Vnv00!62))),
% 105.28/105.51 inference(unit_resolution,[status(thm)],[80, 74, 37, 61, 22, 60])).
% 105.28/105.51 tff(82,plain,
% 105.28/105.51 (vt1 = vSucc(Vnv00!62)),
% 105.28/105.51 inference(unit_resolution,[status(thm)],[81, 59])).
% 105.28/105.51 tff(83,plain,
% 105.28/105.51 ((~![Vnv0: vTerm] : (~(vt1 = vSucc(Vnv0)))) | (~(vt1 = vSucc(Vnv00!62)))),
% 105.28/105.51 inference(quant_inst,[status(thm)],[])).
% 105.28/105.51 tff(84,plain,
% 105.28/105.51 ($false),
% 105.28/105.51 inference(unit_resolution,[status(thm)],[83, 17, 82])).
% 105.28/105.51 % SZS output end Proof
% 105.28/105.51 % E exiting
%------------------------------------------------------------------------------