%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM214_1 : TPTP v9.3.0. Released v9.3.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 : Tue May 5 06:23:00 PM UTC 2026
% Result : Theorem 176.33s 176.50s
% Output : Proof 176.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM214_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.16/0.33 % Computer : n001.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 18:50:05 EDT 2026
% 0.16/0.34 % CPUTime :
% 176.33/176.50 % SZS status Theorem
% 176.33/176.50 % SZS output start Proof
% 176.33/176.50 tff(vSucc_type, type, (
% 176.33/176.50 vSucc: vTerm > vTerm)).
% 176.33/176.50 tff(tptp_fun_Vt30_14_type, type, (
% 176.33/176.50 tptp_fun_Vt30_14: ( vTerm * vTerm ) > vTerm)).
% 176.33/176.50 tff(tptp_fun_Vt_62_type, type, (
% 176.33/176.50 tptp_fun_Vt_62: vTerm)).
% 176.33/176.50 tff(vFalse_type, type, (
% 176.33/176.50 vFalse: vTerm)).
% 176.33/176.50 tff(vplusop_type, type, (
% 176.33/176.50 vplusop: ( vTerm * vTerm ) > vTerm)).
% 176.33/176.50 tff(vZero_type, type, (
% 176.33/176.50 vZero: vTerm)).
% 176.33/176.50 tff(vptchecksimple_type, type, (
% 176.33/176.50 vptchecksimple: ( vTerm * vTy ) > $o)).
% 176.33/176.50 tff(vNat_type, type, (
% 176.33/176.50 vNat: vTy)).
% 176.33/176.50 tff(1,assumption,(vFalse = vplusop(Vt!62, vFalse)), introduced(assumption)).
% 176.33/176.50 tff(2,plain,
% 176.33/176.50 (vplusop(Vt!62, vFalse) = vFalse),
% 176.33/176.50 inference(symmetry,[status(thm)],[1])).
% 176.33/176.50 tff(3,plain,
% 176.33/176.50 (vptchecksimple(vplusop(Vt!62, vFalse), vNat) <=> vptchecksimple(vFalse, vNat)),
% 176.33/176.50 inference(monotonicity,[status(thm)],[2])).
% 176.33/176.50 tff(4,plain,
% 176.33/176.50 (vptchecksimple(vFalse, vNat) <=> vptchecksimple(vplusop(Vt!62, vFalse), vNat)),
% 176.33/176.50 inference(symmetry,[status(thm)],[3])).
% 176.33/176.50 tff(5,plain,
% 176.33/176.50 ((~![Vt: vTerm] : ((~(vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat))) | vptchecksimple(vplusop(Vt, vFalse), vNat))) <=> (~![Vt: vTerm] : ((~(vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat))) | vptchecksimple(vplusop(Vt, vFalse), vNat)))),
% 176.33/176.50 inference(rewrite,[status(thm)],[])).
% 176.33/176.50 tff(6,plain,
% 176.33/176.50 ((~![Vt: vTerm] : ((vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat)) => vptchecksimple(vplusop(Vt, vFalse), vNat))) <=> (~![Vt: vTerm] : ((~(vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat))) | vptchecksimple(vplusop(Vt, vFalse), vNat)))),
% 176.33/176.50 inference(rewrite,[status(thm)],[])).
% 176.33/176.50 tff(7,axiom,(~![Vt: vTerm] : ((vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat)) => vptchecksimple(vplusop(Vt, vFalse), vNat))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''PlusPreservation-False'')).
% 176.33/176.50 tff(8,plain,
% 176.33/176.50 (~![Vt: vTerm] : ((~(vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat))) | vptchecksimple(vplusop(Vt, vFalse), vNat))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[7, 6])).
% 176.33/176.50 tff(9,plain,
% 176.33/176.50 (~![Vt: vTerm] : ((~(vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat))) | vptchecksimple(vplusop(Vt, vFalse), vNat))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[8, 5])).
% 176.33/176.50 tff(10,plain,
% 176.33/176.50 (~![Vt: vTerm] : ((~(vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat))) | vptchecksimple(vplusop(Vt, vFalse), vNat))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[9, 5])).
% 176.33/176.50 tff(11,plain,
% 176.33/176.50 (~![Vt: vTerm] : ((~(vptchecksimple(Vt, vNat) & vptchecksimple(vFalse, vNat))) | vptchecksimple(vplusop(Vt, vFalse), vNat))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[10, 5])).
% 176.33/176.50 tff(12,plain,(
% 176.33/176.50 ~((~(vptchecksimple(Vt!62, vNat) & vptchecksimple(vFalse, vNat))) | vptchecksimple(vplusop(Vt!62, vFalse), vNat))),
% 176.33/176.50 inference(skolemize,[status(sab)],[11])).
% 176.33/176.50 tff(13,plain,
% 176.33/176.50 (vptchecksimple(Vt!62, vNat) & vptchecksimple(vFalse, vNat)),
% 176.33/176.50 inference(or_elim,[status(thm)],[12])).
% 176.33/176.50 tff(14,plain,
% 176.33/176.50 (vptchecksimple(vFalse, vNat)),
% 176.33/176.50 inference(and_elim,[status(thm)],[13])).
% 176.33/176.50 tff(15,plain,
% 176.33/176.50 (vptchecksimple(vplusop(Vt!62, vFalse), vNat)),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[14, 4])).
% 176.33/176.50 tff(16,plain,
% 176.33/176.50 (~vptchecksimple(vplusop(Vt!62, vFalse), vNat)),
% 176.33/176.50 inference(or_elim,[status(thm)],[12])).
% 176.33/176.50 tff(17,plain,
% 176.33/176.50 ($false),
% 176.33/176.50 inference(unit_resolution,[status(thm)],[16, 15])).
% 176.33/176.50 tff(18,plain,(~(vFalse = vplusop(Vt!62, vFalse))), inference(lemma,lemma(discharge,[]))).
% 176.33/176.50 tff(19,plain,
% 176.33/176.50 (((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero)) | (vFalse = vplusop(Vt!62, vFalse))),
% 176.33/176.50 inference(tautology,[status(thm)],[])).
% 176.33/176.50 tff(20,plain,
% 176.33/176.50 ((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero)),
% 176.33/176.50 inference(unit_resolution,[status(thm)],[19, 18])).
% 176.33/176.50 tff(21,plain,
% 176.33/176.50 ((~(vFalse = vZero)) <=> (~(vFalse = vZero))),
% 176.33/176.50 inference(rewrite,[status(thm)],[])).
% 176.33/176.50 tff(22,axiom,(~(vFalse = vZero)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''DIFF-False-Zero'')).
% 176.33/176.50 tff(23,plain,
% 176.33/176.50 (~(vFalse = vZero)),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[22, 21])).
% 176.33/176.50 tff(24,plain,
% 176.33/176.50 (((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse)))) | (vFalse = vZero)),
% 176.33/176.50 inference(tautology,[status(thm)],[])).
% 176.33/176.50 tff(25,plain,
% 176.33/176.50 ((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse)))),
% 176.33/176.50 inference(unit_resolution,[status(thm)],[24, 23])).
% 176.33/176.50 tff(26,plain,
% 176.33/176.50 (^[VTerm0: vTerm, VTerm1: vTerm] : rewrite(((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))) <=> ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))))))))),
% 176.33/176.50 inference(bind,[status(th)],[])).
% 176.33/176.50 tff(27,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))) <=> ![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))),
% 176.33/176.50 inference(quant_intro,[status(thm)],[26])).
% 176.33/176.50 tff(28,plain,
% 176.33/176.50 (^[VTerm0: vTerm, VTerm1: vTerm] : refl(((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))) <=> ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))))),
% 176.33/176.50 inference(bind,[status(th)],[])).
% 176.33/176.50 tff(29,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))) <=> ![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1))))))),
% 176.33/176.50 inference(quant_intro,[status(thm)],[28])).
% 176.33/176.50 tff(30,plain,
% 176.33/176.50 (^[VTerm0: vTerm, VTerm1: vTerm] : rewrite(((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))) <=> ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))))),
% 176.33/176.50 inference(bind,[status(th)],[])).
% 176.33/176.50 tff(31,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))) <=> ![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1))))))),
% 176.33/176.50 inference(quant_intro,[status(thm)],[30])).
% 176.33/176.50 tff(32,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))) <=> ![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1))))))),
% 176.33/176.50 inference(transitivity,[status(thm)],[31, 29])).
% 176.33/176.50 tff(33,plain,
% 176.33/176.50 (^[VTerm0: vTerm, VTerm1: vTerm] : rewrite((((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0)))) & (VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1)))) <=> ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1)))))))),
% 176.33/176.50 inference(bind,[status(th)],[])).
% 176.33/176.50 tff(34,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0)))) & (VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1)))) <=> ![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1))))))),
% 176.33/176.50 inference(quant_intro,[status(thm)],[33])).
% 176.33/176.50 tff(35,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1)))) <=> ![VTerm0: vTerm, VTerm1: vTerm] : (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))),
% 176.33/176.50 inference(rewrite,[status(thm)],[])).
% 176.33/176.50 tff(36,plain,
% 176.33/176.50 (^[VTerm0: vTerm, VTerm1: vTerm] : trans(monotonicity(rewrite((?[Vt20: vTerm] : (((VTerm0 = Vt20) & (VTerm1 = vZero)) & (vplusop(VTerm0, VTerm1) = Vt20)) | ?[Vt30: vTerm, Vt21: vTerm] : (((VTerm0 = Vt21) & (VTerm1 = vSucc(Vt30))) & (vplusop(VTerm0, VTerm1) = vSucc(vplusop(Vt21, Vt30))))) <=> (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30))))), trans(quant_intro(proof_bind(^[Vt31: vTerm, Vt22: vTerm] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) <=> ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))))), ((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) <=> (((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)))), rewrite((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) <=> ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22))), ((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) <=> ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22)))), (((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) <=> (((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)))), rewrite((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) <=> ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31))), (((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) <=> ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31)))), ((((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31)) <=> (((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31)))), rewrite((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31)) <=> ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31) & (vplusop(VTerm0, VTerm1) = Vt31))), ((((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31)) <=> ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31) & (vplusop(VTerm0, VTerm1) = Vt31))))), (?[Vt31: vTerm, Vt22: vTerm] : (((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31)) <=> ?[Vt31: vTerm, Vt22: vTerm] : ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31) & (vplusop(VTerm0, VTerm1) = Vt31)))), trans(der(?[Vt31: vTerm, Vt22: vTerm] : ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31) & (vplusop(VTerm0, VTerm1) = Vt31)) <=> ?[Vt31: vTerm, Vt22: vTerm] : ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1)))), elim_unused(?[Vt31: vTerm, Vt22: vTerm] : ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))) <=> ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1)))), (?[Vt31: vTerm, Vt22: vTerm] : ((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000))) & (VTerm0 = Vt22) & (VTerm1 = Vt31) & (vplusop(VTerm0, VTerm1) = Vt31)) <=> ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))), (?[Vt31: vTerm, Vt22: vTerm] : (((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31)) <=> ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))), (((?[Vt20: vTerm] : (((VTerm0 = Vt20) & (VTerm1 = vZero)) & (vplusop(VTerm0, VTerm1) = Vt20)) | ?[Vt30: vTerm, Vt21: vTerm] : (((VTerm0 = Vt21) & (VTerm1 = vSucc(Vt30))) & (vplusop(VTerm0, VTerm1) = vSucc(vplusop(Vt21, Vt30))))) | ?[Vt31: vTerm, Vt22: vTerm] : (((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31))) <=> ((((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30)))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1)))))), rewrite(((((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30)))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1)))) <=> (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))), (((?[Vt20: vTerm] : (((VTerm0 = Vt20) & (VTerm1 = vZero)) & (vplusop(VTerm0, VTerm1) = Vt20)) | ?[Vt30: vTerm, Vt21: vTerm] : (((VTerm0 = Vt21) & (VTerm1 = vSucc(Vt30))) & (vplusop(VTerm0, VTerm1) = vSucc(vplusop(Vt21, Vt30))))) | ?[Vt31: vTerm, Vt22: vTerm] : (((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31))) <=> (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))))),
% 176.33/176.50 inference(bind,[status(th)],[])).
% 176.33/176.50 tff(37,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : ((?[Vt20: vTerm] : (((VTerm0 = Vt20) & (VTerm1 = vZero)) & (vplusop(VTerm0, VTerm1) = Vt20)) | ?[Vt30: vTerm, Vt21: vTerm] : (((VTerm0 = Vt21) & (VTerm1 = vSucc(Vt30))) & (vplusop(VTerm0, VTerm1) = vSucc(vplusop(Vt21, Vt30))))) | ?[Vt31: vTerm, Vt22: vTerm] : (((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31))) <=> ![VTerm0: vTerm, VTerm1: vTerm] : (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))),
% 176.33/176.50 inference(quant_intro,[status(thm)],[36])).
% 176.33/176.50 tff(38,axiom,(![VTerm0: vTerm, VTerm1: vTerm] : ((?[Vt20: vTerm] : (((VTerm0 = Vt20) & (VTerm1 = vZero)) & (vplusop(VTerm0, VTerm1) = Vt20)) | ?[Vt30: vTerm, Vt21: vTerm] : (((VTerm0 = Vt21) & (VTerm1 = vSucc(Vt30))) & (vplusop(VTerm0, VTerm1) = vSucc(vplusop(Vt21, Vt30))))) | ?[Vt31: vTerm, Vt22: vTerm] : (((((~(Vt31 = vZero)) & ![Vt3000: vTerm] : (~(Vt31 = vSucc(Vt3000)))) & (VTerm0 = Vt22)) & (VTerm1 = Vt31)) & (vplusop(VTerm0, VTerm1) = Vt31)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''plusop-INV'')).
% 176.33/176.50 tff(39,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[38, 37])).
% 176.33/176.50 tff(40,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ?[Vt30: vTerm] : ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, Vt30))) & (VTerm1 = vSucc(Vt30))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[39, 35])).
% 176.33/176.50 tff(41,plain,(
% 176.33/176.50 ![VTerm0: vTerm, VTerm1: vTerm] : (((VTerm0 = vplusop(VTerm0, VTerm1)) & (VTerm1 = vZero)) | ((vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0)))) & (VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))) | ((~(vplusop(VTerm0, VTerm1) = vZero)) & ![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000))) & (VTerm1 = vplusop(VTerm0, VTerm1))))),
% 176.33/176.50 inference(skolemize,[status(sab)],[40])).
% 176.33/176.50 tff(42,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1))))))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[41, 34])).
% 176.33/176.50 tff(43,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))) | (~(VTerm1 = vplusop(VTerm0, VTerm1))))))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[42, 32])).
% 176.33/176.50 tff(44,plain,
% 176.33/176.50 (![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[43, 27])).
% 176.33/176.50 tff(45,plain,
% 176.33/176.50 (((~![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))) | ((~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))))) | (~((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero))))) <=> ((~![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))) | (~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))))) | (~((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero))))),
% 176.33/176.50 inference(rewrite,[status(thm)],[])).
% 176.33/176.50 tff(46,plain,
% 176.33/176.50 (((~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))) | (~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))))) | (~((vplusop(Vt!62, vFalse) = vZero) | (~(vFalse = vplusop(Vt!62, vFalse))) | (~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000))))))) <=> ((~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))))) | (~((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero))))),
% 176.33/176.50 inference(rewrite,[status(thm)],[])).
% 176.33/176.50 tff(47,plain,
% 176.33/176.50 (((~![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))) | ((~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))) | (~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))))) | (~((vplusop(Vt!62, vFalse) = vZero) | (~(vFalse = vplusop(Vt!62, vFalse))) | (~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))))))) <=> ((~![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))) | ((~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))))) | (~((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero)))))),
% 176.33/176.50 inference(monotonicity,[status(thm)],[46])).
% 176.33/176.50 tff(48,plain,
% 176.33/176.50 (((~![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))) | ((~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))) | (~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))))) | (~((vplusop(Vt!62, vFalse) = vZero) | (~(vFalse = vplusop(Vt!62, vFalse))) | (~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))))))) <=> ((~![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))) | (~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))))) | (~((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero))))),
% 176.33/176.50 inference(transitivity,[status(thm)],[47, 45])).
% 176.33/176.50 tff(49,plain,
% 176.33/176.50 ((~![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))) | ((~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))) | (~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))))) | (~((vplusop(Vt!62, vFalse) = vZero) | (~(vFalse = vplusop(Vt!62, vFalse))) | (~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))))))),
% 176.33/176.50 inference(quant_inst,[status(thm)],[])).
% 176.33/176.50 tff(50,plain,
% 176.33/176.50 ((~![VTerm0: vTerm, VTerm1: vTerm] : ((~((~(VTerm1 = vZero)) | (~(VTerm0 = vplusop(VTerm0, VTerm1))))) | (~((~(vplusop(VTerm0, VTerm1) = vSucc(vplusop(VTerm0, tptp_fun_Vt30_14(VTerm1, VTerm0))))) | (~(VTerm1 = vSucc(tptp_fun_Vt30_14(VTerm1, VTerm0)))))) | (~((vplusop(VTerm0, VTerm1) = vZero) | (~(VTerm1 = vplusop(VTerm0, VTerm1))) | (~![Vt3000: vTerm] : (~(vplusop(VTerm0, VTerm1) = vSucc(Vt3000)))))))) | (~((~(vFalse = vZero)) | (~(Vt!62 = vplusop(Vt!62, vFalse))))) | (~((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))))) | (~((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero)))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[49, 48])).
% 176.33/176.50 tff(51,plain,
% 176.33/176.50 ((~((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))))) | (~((~![Vt3000: vTerm] : (~(vplusop(Vt!62, vFalse) = vSucc(Vt3000)))) | (~(vFalse = vplusop(Vt!62, vFalse))) | (vplusop(Vt!62, vFalse) = vZero)))),
% 176.33/176.50 inference(unit_resolution,[status(thm)],[50, 44, 25])).
% 176.33/176.50 tff(52,plain,
% 176.33/176.50 (~((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62))))))),
% 176.33/176.50 inference(unit_resolution,[status(thm)],[51, 20])).
% 176.33/176.50 tff(53,plain,
% 176.33/176.50 (((~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))) | (~(vplusop(Vt!62, vFalse) = vSucc(vplusop(Vt!62, tptp_fun_Vt30_14(vFalse, Vt!62)))))) | (vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62)))),
% 176.33/176.50 inference(tautology,[status(thm)],[])).
% 176.33/176.50 tff(54,plain,
% 176.33/176.50 (vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62))),
% 176.33/176.50 inference(unit_resolution,[status(thm)],[53, 52])).
% 176.33/176.50 tff(55,plain,
% 176.33/176.50 (^[VTerm0: vTerm] : refl((~(vFalse = vSucc(VTerm0))) <=> (~(vFalse = vSucc(VTerm0))))),
% 176.33/176.50 inference(bind,[status(th)],[])).
% 176.33/176.50 tff(56,plain,
% 176.33/176.50 (![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0))) <=> ![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0)))),
% 176.33/176.50 inference(quant_intro,[status(thm)],[55])).
% 176.33/176.50 tff(57,plain,
% 176.33/176.50 (![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0))) <=> ![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0)))),
% 176.33/176.50 inference(rewrite,[status(thm)],[])).
% 176.33/176.50 tff(58,axiom,(![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''DIFF-False-Succ'')).
% 176.33/176.50 tff(59,plain,
% 176.33/176.50 (![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0)))),
% 176.33/176.50 inference(modus_ponens,[status(thm)],[58, 57])).
% 176.33/176.50 tff(60,plain,(
% 176.33/176.50 ![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0)))),
% 176.33/176.50 inference(skolemize,[status(sab)],[59])).
% 176.33/176.50 tff(61,plain,
% 176.33/176.50 (![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0)))),
% 176.33/176.53 inference(modus_ponens,[status(thm)],[60, 56])).
% 176.33/176.53 tff(62,plain,
% 176.33/176.53 ((~![VTerm0: vTerm] : (~(vFalse = vSucc(VTerm0)))) | (~(vFalse = vSucc(tptp_fun_Vt30_14(vFalse, Vt!62))))),
% 176.33/176.53 inference(quant_inst,[status(thm)],[])).
% 176.33/176.53 tff(63,plain,
% 176.33/176.53 ($false),
% 176.33/176.53 inference(unit_resolution,[status(thm)],[62, 61, 54])).
% 176.33/176.53 % SZS output end Proof
% 176.33/176.53 % E exiting
%------------------------------------------------------------------------------