%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM147+1 : TPTP v9.0.0. Released v6.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n012.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:01:08 AM UTC 2025
% Result : Theorem 0.23s 0.44s
% Output : Proof 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : COM147+1 : TPTP v9.0.0. Released v6.4.0.
% 0.04/0.14 % Command : run_E %s %d THM
% 0.15/0.36 % Computer : n012.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu Jun 19 12:24:11 EDT 2025
% 0.23/0.36 % CPUTime :
% 0.23/0.44 % SZS status Theorem
% 0.23/0.44 % SZS output start Proof
% 0.23/0.44 tff(visValue_type, type, (
% 0.23/0.44 visValue: $i > $o)).
% 0.23/0.44 tff(vabs_type, type, (
% 0.23/0.44 vabs: ( $i * $i * $i ) > $i)).
% 0.23/0.44 tff(ve1_type, type, (
% 0.23/0.44 ve1: $i)).
% 0.23/0.44 tff(tptp_fun_VS_51_type, type, (
% 0.23/0.44 tptp_fun_VS_51: $i)).
% 0.23/0.44 tff(tptp_fun_Vx_52_type, type, (
% 0.23/0.44 tptp_fun_Vx_52: $i)).
% 0.23/0.44 tff(vsomeExp_type, type, (
% 0.23/0.44 vsomeExp: $i > $i)).
% 0.23/0.44 tff(vreduce_type, type, (
% 0.23/0.44 vreduce: $i > $i)).
% 0.23/0.44 tff(vtcheck_type, type, (
% 0.23/0.44 vtcheck: ( $i * $i * $i ) > $o)).
% 0.23/0.44 tff(tptp_fun_VTin_53_type, type, (
% 0.23/0.44 tptp_fun_VTin_53: $i)).
% 0.23/0.44 tff(vempty_type, type, (
% 0.23/0.44 vempty: $i)).
% 0.23/0.44 tff(1,plain,
% 0.23/0.44 (((vtcheck(vempty, vabs(Vx!52, VS!51, ve1), VTin!53) & (~visValue(vabs(Vx!52, VS!51, ve1)))) & ![Veout: $i] : (~(vreduce(vabs(Vx!52, VS!51, ve1)) = vsomeExp(Veout)))) <=> (vtcheck(vempty, vabs(Vx!52, VS!51, ve1), VTin!53) & (~visValue(vabs(Vx!52, VS!51, ve1))) & ![Veout: $i] : (~(vreduce(vabs(Vx!52, VS!51, ve1)) = vsomeExp(Veout))))),
% 0.23/0.44 inference(rewrite,[status(thm)],[])).
% 0.23/0.44 tff(2,plain,
% 0.23/0.44 ((~![VTin: $i, Vx: $i, VS: $i] : ((~(vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1))))) | ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout)))) <=> (~![VTin: $i, Vx: $i, VS: $i] : ((~(vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1))))) | ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout))))),
% 0.23/0.44 inference(rewrite,[status(thm)],[])).
% 0.23/0.44 tff(3,plain,
% 0.23/0.44 ((~![VTin: $i, Vx: $i, VS: $i] : ((vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1)))) => ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout)))) <=> (~![VTin: $i, Vx: $i, VS: $i] : ((~(vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1))))) | ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout))))),
% 0.23/0.44 inference(rewrite,[status(thm)],[])).
% 0.23/0.44 tff(4,axiom,(~![VTin: $i, Vx: $i, VS: $i] : ((vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1)))) => ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p',''T-Progress-T-abs'')).
% 0.23/0.44 tff(5,plain,
% 0.23/0.44 (~![VTin: $i, Vx: $i, VS: $i] : ((~(vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1))))) | ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout)))),
% 0.23/0.44 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.23/0.44 tff(6,plain,
% 0.23/0.44 (~![VTin: $i, Vx: $i, VS: $i] : ((~(vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1))))) | ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout)))),
% 0.23/0.44 inference(modus_ponens,[status(thm)],[5, 2])).
% 0.23/0.44 tff(7,plain,
% 0.23/0.44 (~![VTin: $i, Vx: $i, VS: $i] : ((~(vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1))))) | ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout)))),
% 0.23/0.44 inference(modus_ponens,[status(thm)],[6, 2])).
% 0.23/0.44 tff(8,plain,
% 0.23/0.44 (~![VTin: $i, Vx: $i, VS: $i] : ((~(vtcheck(vempty, vabs(Vx, VS, ve1), VTin) & (~visValue(vabs(Vx, VS, ve1))))) | ?[Veout: $i] : (vreduce(vabs(Vx, VS, ve1)) = vsomeExp(Veout)))),
% 0.23/0.44 inference(modus_ponens,[status(thm)],[7, 2])).
% 0.23/0.44 tff(9,plain,
% 0.23/0.44 (vtcheck(vempty, vabs(Vx!52, VS!51, ve1), VTin!53) & (~visValue(vabs(Vx!52, VS!51, ve1))) & ![Veout: $i] : (~(vreduce(vabs(Vx!52, VS!51, ve1)) = vsomeExp(Veout)))),
% 0.23/0.44 inference(modus_ponens,[status(thm)],[8, 1])).
% 0.23/0.44 tff(10,plain,
% 0.23/0.44 (~visValue(vabs(Vx!52, VS!51, ve1))),
% 0.23/0.44 inference(and_elim,[status(thm)],[9])).
% 0.23/0.44 tff(11,plain,
% 0.23/0.44 (^[Vx: $i, VS: $i, Ve: $i] : refl(visValue(vabs(Vx, VS, Ve)) <=> visValue(vabs(Vx, VS, Ve)))),
% 0.23/0.44 inference(bind,[status(th)],[])).
% 0.23/0.44 tff(12,plain,
% 0.23/0.44 (![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve)) <=> ![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.44 inference(quant_intro,[status(thm)],[11])).
% 0.23/0.44 tff(13,plain,
% 0.23/0.44 (![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve)) <=> ![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.44 inference(rewrite,[status(thm)],[])).
% 0.23/0.44 tff(14,plain,
% 0.23/0.44 (![Vx: $i, VS: $i, Ve: $i, VExp0: $i] : visValue(vabs(Vx, VS, Ve)) <=> ![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.44 inference(elim_unused_vars,[status(thm)],[])).
% 0.23/0.45 tff(15,plain,
% 0.23/0.45 (![Vx: $i, VS: $i, Ve: $i, VExp0: $i] : (visValue(VExp0) | (~(VExp0 = vabs(Vx, VS, Ve)))) <=> ![Vx: $i, VS: $i, Ve: $i, VExp0: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.45 inference(destructive_equality_resolution,[status(thm)],[])).
% 0.23/0.45 tff(16,plain,
% 0.23/0.45 (![Vx: $i, VS: $i, Ve: $i, VExp0: $i] : (visValue(VExp0) | (~(VExp0 = vabs(Vx, VS, Ve)))) <=> ![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.45 inference(transitivity,[status(thm)],[15, 14])).
% 0.23/0.45 tff(17,plain,
% 0.23/0.45 (^[Vx: $i, VS: $i, Ve: $i, VExp0: $i] : rewrite(((VExp0 = vabs(Vx, VS, Ve)) => visValue(VExp0)) <=> (visValue(VExp0) | (~(VExp0 = vabs(Vx, VS, Ve)))))),
% 0.23/0.45 inference(bind,[status(th)],[])).
% 0.23/0.45 tff(18,plain,
% 0.23/0.45 (![Vx: $i, VS: $i, Ve: $i, VExp0: $i] : ((VExp0 = vabs(Vx, VS, Ve)) => visValue(VExp0)) <=> ![Vx: $i, VS: $i, Ve: $i, VExp0: $i] : (visValue(VExp0) | (~(VExp0 = vabs(Vx, VS, Ve))))),
% 0.23/0.45 inference(quant_intro,[status(thm)],[17])).
% 0.23/0.45 tff(19,plain,
% 0.23/0.45 (![Vx: $i, VS: $i, Ve: $i, VExp0: $i] : ((VExp0 = vabs(Vx, VS, Ve)) => visValue(VExp0)) <=> ![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.45 inference(transitivity,[status(thm)],[18, 16])).
% 0.23/0.45 tff(20,axiom,(![Vx: $i, VS: $i, Ve: $i, VExp0: $i] : ((VExp0 = vabs(Vx, VS, Ve)) => visValue(VExp0))), file('/export/starexec/sandbox2/benchmark/Axioms/COM001+0.ax','isValue0')).
% 0.23/0.45 tff(21,plain,
% 0.23/0.45 (![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.45 inference(modus_ponens,[status(thm)],[20, 19])).
% 0.23/0.45 tff(22,plain,
% 0.23/0.45 (![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.45 inference(modus_ponens,[status(thm)],[21, 13])).
% 0.23/0.45 tff(23,plain,(
% 0.23/0.45 ![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.45 inference(skolemize,[status(sab)],[22])).
% 0.23/0.45 tff(24,plain,
% 0.23/0.45 (![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))),
% 0.23/0.45 inference(modus_ponens,[status(thm)],[23, 12])).
% 0.23/0.45 tff(25,plain,
% 0.23/0.45 ((~![Vx: $i, VS: $i, Ve: $i] : visValue(vabs(Vx, VS, Ve))) | visValue(vabs(Vx!52, VS!51, ve1))),
% 0.23/0.45 inference(quant_inst,[status(thm)],[])).
% 0.23/0.45 tff(26,plain,
% 0.23/0.45 ($false),
% 0.23/0.45 inference(unit_resolution,[status(thm)],[25, 24, 10])).
% 0.23/0.45 % SZS output end Proof
% 0.23/0.45 % E exiting
%------------------------------------------------------------------------------