%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM296_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.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:07 PM UTC 2026
% Result : Theorem 0.30s 0.66s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.21 % Problem : COM296_1 : TPTP v9.3.0. Released v9.3.0.
% 0.03/0.21 % Command : run_E %s %d THM
% 0.13/0.44 % Computer : n009.cluster.edu
% 0.13/0.44 % Model : x86_64 x86_64
% 0.13/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.44 % Memory : 8042.1875MB
% 0.13/0.44 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.44 % CPULimit : 300
% 0.13/0.44 % WCLimit : 300
% 0.13/0.44 % DateTime : Mon May 4 20:29:57 EDT 2026
% 0.15/0.45 % CPUTime :
% 0.30/0.66 % SZS status Theorem
% 0.30/0.66 % SZS output start Proof
% 0.30/0.66 tff(vwelltypedRawtable_type, type, (
% 0.30/0.66 vwelltypedRawtable: ( vTType * vRawTable ) > $o)).
% 0.30/0.66 tff(vrawUnion_type, type, (
% 0.30/0.66 vrawUnion: ( vRawTable * vRawTable ) > vRawTable)).
% 0.30/0.66 tff(vgetRaw_type, type, (
% 0.30/0.66 vgetRaw: vTable > vRawTable)).
% 0.30/0.66 tff(tptp_fun_Vt2_309_type, type, (
% 0.30/0.66 tptp_fun_Vt2_309: vTable)).
% 0.30/0.66 tff(tptp_fun_VwildcardName00_48_type, type, (
% 0.30/0.66 tptp_fun_VwildcardName00_48: vTable > vRawTable)).
% 0.30/0.66 tff(tptp_fun_Vt_311_type, type, (
% 0.30/0.66 tptp_fun_Vt_311: vTable)).
% 0.30/0.66 tff(tptp_fun_Vtt_307_type, type, (
% 0.30/0.66 tptp_fun_Vtt_307: vTType)).
% 0.30/0.66 tff(tptp_fun_VwildcardName00_47_type, type, (
% 0.30/0.66 tptp_fun_VwildcardName00_47: vTable > vAttrL)).
% 0.30/0.66 tff(vgetAttrL_type, type, (
% 0.30/0.66 vgetAttrL: vTable > vAttrL)).
% 0.30/0.66 tff(vtable_type, type, (
% 0.30/0.66 vtable: ( vAttrL * vRawTable ) > vTable)).
% 0.30/0.66 tff(vmatchingAttrL_type, type, (
% 0.30/0.66 vmatchingAttrL: ( vTType * vAttrL ) > $o)).
% 0.30/0.66 tff(vwelltypedtable_type, type, (
% 0.30/0.66 vwelltypedtable: ( vTType * vTable ) > $o)).
% 0.30/0.66 tff(vptcheck_type, type, (
% 0.30/0.66 vptcheck: ( vTTContext * vQuery * vTType ) > $o)).
% 0.30/0.66 tff(vtvalue_type, type, (
% 0.30/0.66 vtvalue: vTable > vQuery)).
% 0.30/0.66 tff(tptp_fun_Vttc_310_type, type, (
% 0.30/0.66 tptp_fun_Vttc_310: vTTContext)).
% 0.30/0.66 tff(vUnion_type, type, (
% 0.30/0.66 vUnion: ( vQuery * vQuery ) > vQuery)).
% 0.30/0.66 tff(vq2_type, type, (
% 0.30/0.66 vq2: vQuery)).
% 0.30/0.66 tff(vq1_type, type, (
% 0.30/0.66 vq1: vQuery)).
% 0.30/0.66 tff(vsomeQuery_type, type, (
% 0.30/0.66 vsomeQuery: vQuery > vOptQuery)).
% 0.30/0.66 tff(tptp_fun_Vqr_312_type, type, (
% 0.30/0.66 tptp_fun_Vqr_312: vQuery)).
% 0.30/0.66 tff(vreduce_type, type, (
% 0.30/0.66 vreduce: ( vQuery * vTStore ) > vOptQuery)).
% 0.30/0.66 tff(tptp_fun_Vts_308_type, type, (
% 0.30/0.66 tptp_fun_Vts_308: vTStore)).
% 0.30/0.66 tff(vstoreContextConsistent_type, type, (
% 0.30/0.66 vstoreContextConsistent: ( vTStore * vTTContext ) > $o)).
% 0.30/0.66 tff(vgetQuery_type, type, (
% 0.30/0.66 vgetQuery: vOptQuery > vQuery)).
% 0.30/0.66 tff(1,plain,
% 0.30/0.66 (^[VTable0: vTable] : refl((VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0))) <=> (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(2,plain,
% 0.30/0.66 (![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0))) <=> ![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[1])).
% 0.30/0.66 tff(3,plain,
% 0.30/0.66 (![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0))) <=> ![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))),
% 0.30/0.66 inference(rewrite,[status(thm)],[])).
% 0.30/0.66 tff(4,plain,
% 0.30/0.66 (^[VTable0: vTable] : trans(der(?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((VTable0 = vtable(VwildcardName00, Vrt0)) & (vgetRaw(VTable0) = Vrt0)) <=> ?[VwildcardName00: vAttrL, Vrt0: vRawTable] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))), elim_unused(?[VwildcardName00: vAttrL, Vrt0: vRawTable] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0))) <=> ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))), (?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((VTable0 = vtable(VwildcardName00, Vrt0)) & (vgetRaw(VTable0) = Vrt0)) <=> ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(5,plain,
% 0.30/0.66 (![VTable0: vTable] : ?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((VTable0 = vtable(VwildcardName00, Vrt0)) & (vgetRaw(VTable0) = Vrt0)) <=> ![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[4])).
% 0.30/0.66 tff(6,axiom,(![VTable0: vTable] : ?[VwildcardName00: vAttrL, Vrt0: vRawTable] : ((VTable0 = vtable(VwildcardName00, Vrt0)) & (vgetRaw(VTable0) = Vrt0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getRaw-INV'')).
% 0.30/0.66 tff(7,plain,
% 0.30/0.66 (![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.30/0.66 tff(8,plain,
% 0.30/0.66 (![VTable0: vTable] : ?[VwildcardName00: vAttrL] : (VTable0 = vtable(VwildcardName00, vgetRaw(VTable0)))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.30/0.66 tff(9,plain,(
% 0.30/0.66 ![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))),
% 0.30/0.66 inference(skolemize,[status(sab)],[8])).
% 0.30/0.66 tff(10,plain,
% 0.30/0.66 (![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.30/0.66 tff(11,plain,
% 0.30/0.66 ((~![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))) | (Vt!311 = vtable(tptp_fun_VwildcardName00_47(Vt!311), vgetRaw(Vt!311)))),
% 0.30/0.66 inference(quant_inst,[status(thm)],[])).
% 0.30/0.66 tff(12,plain,
% 0.30/0.66 (Vt!311 = vtable(tptp_fun_VwildcardName00_47(Vt!311), vgetRaw(Vt!311))),
% 0.30/0.66 inference(unit_resolution,[status(thm)],[11, 10])).
% 0.30/0.66 tff(13,plain,
% 0.30/0.66 (^[VTable0: vTable] : refl((VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0))) <=> (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(14,plain,
% 0.30/0.66 (![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0))) <=> ![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0)))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[13])).
% 0.30/0.66 tff(15,plain,
% 0.30/0.66 (![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00)) <=> ![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))),
% 0.30/0.66 inference(rewrite,[status(thm)],[])).
% 0.30/0.66 tff(16,plain,
% 0.30/0.66 (^[VTable0: vTable] : trans(der(?[Val0: vAttrL, VwildcardName00: vRawTable] : ((VTable0 = vtable(Val0, VwildcardName00)) & (vgetAttrL(VTable0) = Val0)) <=> ?[Val0: vAttrL, VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))), elim_unused(?[Val0: vAttrL, VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00)) <=> ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))), (?[Val0: vAttrL, VwildcardName00: vRawTable] : ((VTable0 = vtable(Val0, VwildcardName00)) & (vgetAttrL(VTable0) = Val0)) <=> ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(17,plain,
% 0.30/0.66 (![VTable0: vTable] : ?[Val0: vAttrL, VwildcardName00: vRawTable] : ((VTable0 = vtable(Val0, VwildcardName00)) & (vgetAttrL(VTable0) = Val0)) <=> ![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[16])).
% 0.30/0.66 tff(18,axiom,(![VTable0: vTable] : ?[Val0: vAttrL, VwildcardName00: vRawTable] : ((VTable0 = vtable(Val0, VwildcardName00)) & (vgetAttrL(VTable0) = Val0))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getAttrL-INV'')).
% 0.30/0.66 tff(19,plain,
% 0.30/0.66 (![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.30/0.66 tff(20,plain,
% 0.30/0.66 (![VTable0: vTable] : ?[VwildcardName00: vRawTable] : (VTable0 = vtable(vgetAttrL(VTable0), VwildcardName00))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[19, 15])).
% 0.30/0.66 tff(21,plain,(
% 0.30/0.66 ![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0)))),
% 0.30/0.66 inference(skolemize,[status(sab)],[20])).
% 0.30/0.66 tff(22,plain,
% 0.30/0.66 (![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0)))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[21, 14])).
% 0.30/0.66 tff(23,plain,
% 0.30/0.66 ((~![VTable0: vTable] : (VTable0 = vtable(vgetAttrL(VTable0), tptp_fun_VwildcardName00_48(VTable0)))) | (Vt!311 = vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)))),
% 0.30/0.66 inference(quant_inst,[status(thm)],[])).
% 0.30/0.66 tff(24,plain,
% 0.30/0.66 (Vt!311 = vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311))),
% 0.30/0.66 inference(unit_resolution,[status(thm)],[23, 22])).
% 0.30/0.66 tff(25,plain,
% 0.30/0.66 (vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)) = Vt!311),
% 0.30/0.66 inference(symmetry,[status(thm)],[24])).
% 0.30/0.66 tff(26,plain,
% 0.30/0.66 (vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)) = vtable(tptp_fun_VwildcardName00_47(Vt!311), vgetRaw(Vt!311))),
% 0.30/0.66 inference(transitivity,[status(thm)],[25, 12])).
% 0.30/0.66 tff(27,plain,
% 0.30/0.66 (^[VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : refl(((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1))))) <=> ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1))))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(28,plain,
% 0.30/0.66 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1))))) <=> ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[27])).
% 0.30/0.66 tff(29,plain,
% 0.30/0.66 (^[VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : rewrite(((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1))))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(30,plain,
% 0.30/0.66 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[29])).
% 0.30/0.66 tff(31,plain,
% 0.30/0.66 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.30/0.66 inference(rewrite,[status(thm)],[])).
% 0.30/0.66 tff(32,plain,
% 0.30/0.66 (^[VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : rewrite(((vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1)) => ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(33,plain,
% 0.30/0.66 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1)) => ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1))) <=> ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[32])).
% 0.30/0.66 tff(34,axiom,(![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1)) => ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''EQ-table'')).
% 0.30/0.66 tff(35,plain,
% 0.30/0.66 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.30/0.66 tff(36,plain,
% 0.30/0.66 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[35, 31])).
% 0.30/0.66 tff(37,plain,(
% 0.30/0.66 ![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | ((VAttrL0 = VAttrL1) & (VRawTable0 = VRawTable1)))),
% 0.30/0.66 inference(skolemize,[status(sab)],[36])).
% 0.30/0.66 tff(38,plain,
% 0.30/0.66 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[37, 30])).
% 0.30/0.66 tff(39,plain,
% 0.30/0.66 (![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[38, 28])).
% 0.30/0.66 tff(40,plain,
% 0.30/0.66 (((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | ((~(vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)) = vtable(tptp_fun_VwildcardName00_47(Vt!311), vgetRaw(Vt!311)))) | (~((~(vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311))) | (~(tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311))))))) <=> ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | (~(vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)) = vtable(tptp_fun_VwildcardName00_47(Vt!311), vgetRaw(Vt!311)))) | (~((~(vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311))) | (~(tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311))))))),
% 0.30/0.66 inference(rewrite,[status(thm)],[])).
% 0.30/0.66 tff(41,plain,
% 0.30/0.66 ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | ((~(vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)) = vtable(tptp_fun_VwildcardName00_47(Vt!311), vgetRaw(Vt!311)))) | (~((~(vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311))) | (~(tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311))))))),
% 0.30/0.66 inference(quant_inst,[status(thm)],[])).
% 0.30/0.66 tff(42,plain,
% 0.30/0.66 ((~![VAttrL0: vAttrL, VRawTable0: vRawTable, VAttrL1: vAttrL, VRawTable1: vRawTable] : ((~(vtable(VAttrL0, VRawTable0) = vtable(VAttrL1, VRawTable1))) | (~((~(VAttrL0 = VAttrL1)) | (~(VRawTable0 = VRawTable1)))))) | (~(vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)) = vtable(tptp_fun_VwildcardName00_47(Vt!311), vgetRaw(Vt!311)))) | (~((~(vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311))) | (~(tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311)))))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.30/0.66 tff(43,plain,
% 0.30/0.66 (~((~(vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311))) | (~(tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311))))),
% 0.30/0.66 inference(unit_resolution,[status(thm)],[42, 39, 26])).
% 0.30/0.66 tff(44,plain,
% 0.30/0.66 (((~(vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311))) | (~(tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311)))) | (tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311))),
% 0.30/0.66 inference(tautology,[status(thm)],[])).
% 0.30/0.66 tff(45,plain,
% 0.30/0.66 (tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311)),
% 0.30/0.66 inference(unit_resolution,[status(thm)],[44, 43])).
% 0.30/0.66 tff(46,plain,
% 0.30/0.66 (vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309)) = vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))),
% 0.30/0.66 inference(monotonicity,[status(thm)],[45])).
% 0.30/0.66 tff(47,plain,
% 0.30/0.66 (vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))) <=> vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))),
% 0.30/0.66 inference(monotonicity,[status(thm)],[46])).
% 0.30/0.66 tff(48,plain,
% 0.30/0.66 (vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))) <=> vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309)))),
% 0.30/0.66 inference(symmetry,[status(thm)],[47])).
% 0.30/0.66 tff(49,plain,
% 0.30/0.66 ((~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))) <=> (~vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.66 inference(monotonicity,[status(thm)],[48])).
% 0.30/0.66 tff(50,plain,
% 0.30/0.66 (^[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : refl((~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1)))) <=> (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1)))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(51,plain,
% 0.30/0.66 (![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1)))) <=> ![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[50])).
% 0.30/0.66 tff(52,plain,
% 0.30/0.66 (^[Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : trans(trans(monotonicity(rewrite((vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1)) <=> (~((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))))), ((vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1))) <=> (vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (~((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))))))), rewrite((vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (~((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))))) <=> (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))), ((vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1))) <=> (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1)))))), rewrite((~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1)))) <=> (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))), ((vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1))) <=> (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))))),
% 0.30/0.66 inference(bind,[status(th)],[])).
% 0.30/0.66 tff(53,plain,
% 0.30/0.66 (![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1))) <=> ![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))),
% 0.30/0.66 inference(quant_intro,[status(thm)],[52])).
% 0.30/0.66 tff(54,plain,
% 0.30/0.66 (![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1))) <=> ![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.30/0.66 inference(rewrite,[status(thm)],[])).
% 0.30/0.66 tff(55,axiom,(![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''welltypedtable-0'')).
% 0.30/0.66 tff(56,plain,
% 0.30/0.66 (![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.30/0.66 tff(57,plain,(
% 0.30/0.66 ![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (vwelltypedtable(Vtt, vtable(Val, Vt1)) <=> (vmatchingAttrL(Vtt, Val) & vwelltypedRawtable(Vtt, Vt1)))),
% 0.30/0.66 inference(skolemize,[status(sab)],[56])).
% 0.30/0.66 tff(58,plain,
% 0.30/0.66 (![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[57, 53])).
% 0.30/0.66 tff(59,plain,
% 0.30/0.66 (![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))),
% 0.30/0.66 inference(modus_ponens,[status(thm)],[58, 51])).
% 0.30/0.66 tff(60,plain,
% 0.30/0.66 ((~![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))) | (~(((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311)))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)))))),
% 0.30/0.66 inference(quant_inst,[status(thm)],[])).
% 0.30/0.66 tff(61,plain,
% 0.30/0.66 (~(((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311)))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311))))),
% 0.30/0.66 inference(unit_resolution,[status(thm)],[60, 59])).
% 0.30/0.66 tff(62,plain,
% 0.30/0.66 (((~(vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311))) | (~(tptp_fun_VwildcardName00_48(Vt!311) = vgetRaw(Vt!311)))) | (vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311))),
% 0.30/0.66 inference(tautology,[status(thm)],[])).
% 0.30/0.66 tff(63,plain,
% 0.30/0.66 (vgetAttrL(Vt!311) = tptp_fun_VwildcardName00_47(Vt!311)),
% 0.30/0.66 inference(unit_resolution,[status(thm)],[62, 43])).
% 0.30/0.66 tff(64,plain,
% 0.30/0.66 (tptp_fun_VwildcardName00_47(Vt!311) = vgetAttrL(Vt!311)),
% 0.30/0.66 inference(symmetry,[status(thm)],[63])).
% 0.30/0.66 tff(65,plain,
% 0.30/0.66 (vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)) = vtable(vgetAttrL(Vt!311), tptp_fun_VwildcardName00_48(Vt!311))),
% 0.30/0.66 inference(monotonicity,[status(thm)],[64])).
% 0.30/0.66 tff(66,plain,
% 0.30/0.66 (vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)) = Vt!311),
% 0.30/0.66 inference(transitivity,[status(thm)],[65, 25])).
% 0.30/0.66 tff(67,plain,
% 0.30/0.66 (vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311))) <=> vwelltypedtable(Vtt!307, Vt!311)),
% 0.30/0.66 inference(monotonicity,[status(thm)],[66])).
% 0.30/0.66 tff(68,plain,
% 0.30/0.66 (vwelltypedtable(Vtt!307, Vt!311) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)))),
% 0.30/0.66 inference(symmetry,[status(thm)],[67])).
% 0.30/0.66 tff(69,plain,
% 0.30/0.66 ((~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((~((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))) <=> (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((~((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt)))),
% 0.30/0.66 inference(rewrite,[status(thm)],[])).
% 0.30/0.66 tff(70,plain,
% 0.30/0.66 ((~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((((((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt))) & vstoreContextConsistent(Vts, Vttc)) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt)) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr))) => vptcheck(Vttc, Vqr, Vtt))) <=> (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((~((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt)))),
% 0.30/0.66 inference(rewrite,[status(thm)],[])).
% 0.30/0.66 tff(71,axiom,(~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((((((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt))) & vstoreContextConsistent(Vts, Vttc)) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt)) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr))) => vptcheck(Vttc, Vqr, Vtt))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Preservation-Union-tvalue-tvalue'')).
% 0.30/0.67 tff(72,plain,
% 0.30/0.67 (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((~((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[71, 70])).
% 0.30/0.67 tff(73,plain,
% 0.30/0.67 (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((~((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[72, 69])).
% 0.30/0.67 tff(74,plain,
% 0.30/0.67 (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((~((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[73, 69])).
% 0.30/0.67 tff(75,plain,
% 0.30/0.67 (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vt2: vTable, Vts: vTStore, Vtt: vTType] : ((~((vq2 = vtvalue(Vt2)) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vUnion(vq1, vq2), Vtt) & (vreduce(vUnion(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[74, 69])).
% 0.30/0.67 tff(76,plain,(
% 0.30/0.67 ~((~((vq2 = vtvalue(Vt2!309)) & (vq1 = vtvalue(Vt!311)) & vstoreContextConsistent(Vts!308, Vttc!310) & vptcheck(Vttc!310, vUnion(vq1, vq2), Vtt!307) & (vreduce(vUnion(vq1, vq2), Vts!308) = vsomeQuery(Vqr!312)))) | vptcheck(Vttc!310, Vqr!312, Vtt!307))),
% 0.30/0.67 inference(skolemize,[status(sab)],[75])).
% 0.30/0.67 tff(77,plain,
% 0.30/0.67 ((vq2 = vtvalue(Vt2!309)) & (vq1 = vtvalue(Vt!311)) & vstoreContextConsistent(Vts!308, Vttc!310) & vptcheck(Vttc!310, vUnion(vq1, vq2), Vtt!307) & (vreduce(vUnion(vq1, vq2), Vts!308) = vsomeQuery(Vqr!312))),
% 0.30/0.67 inference(or_elim,[status(thm)],[76])).
% 0.30/0.67 tff(78,plain,
% 0.30/0.67 (vq2 = vtvalue(Vt2!309)),
% 0.30/0.67 inference(and_elim,[status(thm)],[77])).
% 0.30/0.67 tff(79,plain,
% 0.30/0.67 (vtvalue(Vt2!309) = vq2),
% 0.30/0.67 inference(symmetry,[status(thm)],[78])).
% 0.30/0.67 tff(80,plain,
% 0.30/0.67 (vq1 = vtvalue(Vt!311)),
% 0.30/0.67 inference(and_elim,[status(thm)],[77])).
% 0.30/0.67 tff(81,plain,
% 0.30/0.67 (vtvalue(Vt!311) = vq1),
% 0.30/0.67 inference(symmetry,[status(thm)],[80])).
% 0.30/0.67 tff(82,plain,
% 0.30/0.67 (vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)) = vUnion(vq1, vq2)),
% 0.30/0.67 inference(monotonicity,[status(thm)],[81, 79])).
% 0.30/0.67 tff(83,plain,
% 0.30/0.67 (vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307) <=> vptcheck(Vttc!310, vUnion(vq1, vq2), Vtt!307)),
% 0.30/0.67 inference(monotonicity,[status(thm)],[82])).
% 0.30/0.67 tff(84,plain,
% 0.30/0.67 (vptcheck(Vttc!310, vUnion(vq1, vq2), Vtt!307) <=> vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)),
% 0.30/0.67 inference(symmetry,[status(thm)],[83])).
% 0.30/0.67 tff(85,plain,
% 0.30/0.67 (vptcheck(Vttc!310, vUnion(vq1, vq2), Vtt!307)),
% 0.30/0.67 inference(and_elim,[status(thm)],[77])).
% 0.30/0.67 tff(86,plain,
% 0.30/0.67 (vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[85, 84])).
% 0.30/0.67 tff(87,plain,
% 0.30/0.67 (^[VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : refl(((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT)) <=> ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT)))),
% 0.30/0.67 inference(bind,[status(th)],[])).
% 0.30/0.67 tff(88,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT)) <=> ![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))),
% 0.30/0.67 inference(quant_intro,[status(thm)],[87])).
% 0.30/0.67 tff(89,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT)) <=> ![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(90,plain,
% 0.30/0.67 (^[VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : rewrite((vptcheck(VTTC, vUnion(Vq1, Vq2), VTT) => vptcheck(VTTC, Vq1, VTT)) <=> ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT)))),
% 0.30/0.67 inference(bind,[status(th)],[])).
% 0.30/0.67 tff(91,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : (vptcheck(VTTC, vUnion(Vq1, Vq2), VTT) => vptcheck(VTTC, Vq1, VTT)) <=> ![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))),
% 0.30/0.67 inference(quant_intro,[status(thm)],[90])).
% 0.30/0.67 tff(92,axiom,(![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : (vptcheck(VTTC, vUnion(Vq1, Vq2), VTT) => vptcheck(VTTC, Vq1, VTT))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''TUnion_inv1'')).
% 0.30/0.67 tff(93,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.30/0.67 tff(94,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[93, 89])).
% 0.30/0.67 tff(95,plain,(
% 0.30/0.67 ![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))),
% 0.30/0.67 inference(skolemize,[status(sab)],[94])).
% 0.30/0.67 tff(96,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[95, 88])).
% 0.30/0.67 tff(97,plain,
% 0.30/0.67 (((~![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))) | ((~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307))) <=> ((~![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))) | (~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307))),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(98,plain,
% 0.30/0.67 ((~![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))) | ((~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307))),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(99,plain,
% 0.30/0.67 ((~![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq1, VTT))) | (~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307)),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[98, 97])).
% 0.30/0.67 tff(100,plain,
% 0.30/0.67 ((~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307)),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[99, 96])).
% 0.30/0.67 tff(101,plain,
% 0.30/0.67 (vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307)),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[100, 86])).
% 0.30/0.67 tff(102,plain,
% 0.30/0.67 (^[VTTC: vTTContext, Vt: vTable, VTT: vTType] : refl(((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt)) <=> ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt)))),
% 0.30/0.67 inference(bind,[status(th)],[])).
% 0.30/0.67 tff(103,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt)) <=> ![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))),
% 0.30/0.67 inference(quant_intro,[status(thm)],[102])).
% 0.30/0.67 tff(104,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt)) <=> ![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(105,plain,
% 0.30/0.67 (^[VTTC: vTTContext, Vt: vTable, VTT: vTType] : rewrite((vptcheck(VTTC, vtvalue(Vt), VTT) => vwelltypedtable(VTT, Vt)) <=> ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt)))),
% 0.30/0.67 inference(bind,[status(th)],[])).
% 0.30/0.67 tff(106,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vt: vTable, VTT: vTType] : (vptcheck(VTTC, vtvalue(Vt), VTT) => vwelltypedtable(VTT, Vt)) <=> ![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))),
% 0.30/0.67 inference(quant_intro,[status(thm)],[105])).
% 0.30/0.67 tff(107,axiom,(![VTTC: vTTContext, Vt: vTable, VTT: vTType] : (vptcheck(VTTC, vtvalue(Vt), VTT) => vwelltypedtable(VTT, Vt))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Ttvalue_inv'')).
% 0.30/0.67 tff(108,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[107, 106])).
% 0.30/0.67 tff(109,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[108, 104])).
% 0.30/0.67 tff(110,plain,(
% 0.30/0.67 ![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))),
% 0.30/0.67 inference(skolemize,[status(sab)],[109])).
% 0.30/0.67 tff(111,plain,
% 0.30/0.67 (![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[110, 103])).
% 0.30/0.67 tff(112,plain,
% 0.30/0.67 (((~![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))) | ((~vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307)) | vwelltypedtable(Vtt!307, Vt!311))) <=> ((~![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))) | (~vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307)) | vwelltypedtable(Vtt!307, Vt!311))),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(113,plain,
% 0.30/0.67 ((~![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))) | ((~vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307)) | vwelltypedtable(Vtt!307, Vt!311))),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(114,plain,
% 0.30/0.67 ((~![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))) | (~vptcheck(Vttc!310, vtvalue(Vt!311), Vtt!307)) | vwelltypedtable(Vtt!307, Vt!311)),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[113, 112])).
% 0.30/0.67 tff(115,plain,
% 0.30/0.67 (vwelltypedtable(Vtt!307, Vt!311)),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[114, 111, 101])).
% 0.30/0.67 tff(116,plain,
% 0.30/0.67 (vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[115, 68])).
% 0.30/0.67 tff(117,plain,
% 0.30/0.67 ((((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311)))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311)))) | (~((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))))) | (~vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), tptp_fun_VwildcardName00_48(Vt!311))))),
% 0.30/0.67 inference(tautology,[status(thm)],[])).
% 0.30/0.67 tff(118,plain,
% 0.30/0.67 (~((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[117, 116, 61])).
% 0.30/0.67 tff(119,plain,
% 0.30/0.67 (((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311)))) | vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))),
% 0.30/0.67 inference(tautology,[status(thm)],[])).
% 0.30/0.67 tff(120,plain,
% 0.30/0.67 (vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[119, 118])).
% 0.30/0.67 tff(121,plain,
% 0.30/0.67 ((~![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))) | (~(((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))))),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(122,plain,
% 0.30/0.67 (~(((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[121, 59])).
% 0.30/0.67 tff(123,plain,
% 0.30/0.67 (vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))) = vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))),
% 0.30/0.67 inference(monotonicity,[status(thm)],[64])).
% 0.30/0.67 tff(124,plain,
% 0.30/0.67 (vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))) <=> vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(monotonicity,[status(thm)],[123])).
% 0.30/0.67 tff(125,plain,
% 0.30/0.67 (vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(symmetry,[status(thm)],[124])).
% 0.30/0.67 tff(126,plain,
% 0.30/0.67 ((~vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) <=> (~vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))))),
% 0.30/0.67 inference(monotonicity,[status(thm)],[125])).
% 0.30/0.67 tff(127,plain,
% 0.30/0.67 (![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq) <=> ![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq)),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(128,plain,
% 0.30/0.67 (![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq) <=> ![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq)),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(129,axiom,(![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq)), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''getQuery-0'')).
% 0.30/0.67 tff(130,plain,
% 0.30/0.67 (![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq)),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[129, 128])).
% 0.30/0.67 tff(131,plain,(
% 0.30/0.67 ![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq)),
% 0.30/0.67 inference(skolemize,[status(sab)],[130])).
% 0.30/0.67 tff(132,plain,
% 0.30/0.67 (![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq)),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[131, 127])).
% 0.30/0.67 tff(133,plain,
% 0.30/0.67 ((~![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq)) | (vgetQuery(vsomeQuery(Vqr!312)) = Vqr!312)),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(134,plain,
% 0.30/0.67 (vgetQuery(vsomeQuery(Vqr!312)) = Vqr!312),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[133, 132])).
% 0.30/0.67 tff(135,plain,
% 0.30/0.67 (vreduce(vUnion(vq1, vq2), Vts!308) = vsomeQuery(Vqr!312)),
% 0.30/0.67 inference(and_elim,[status(thm)],[77])).
% 0.30/0.67 tff(136,plain,
% 0.30/0.67 (vreduce(vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vts!308) = vreduce(vUnion(vq1, vq2), Vts!308)),
% 0.30/0.67 inference(monotonicity,[status(thm)],[82])).
% 0.30/0.67 tff(137,plain,
% 0.30/0.67 (^[Vt1: vTable, Vt2: vTable, Vts: vTStore] : refl((vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2)))))) <=> (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2)))))))),
% 0.30/0.67 inference(bind,[status(th)],[])).
% 0.30/0.67 tff(138,plain,
% 0.30/0.67 (![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2)))))) <=> ![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2))))))),
% 0.30/0.67 inference(quant_intro,[status(thm)],[137])).
% 0.30/0.67 tff(139,plain,
% 0.30/0.67 (![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2)))))) <=> ![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2))))))),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(140,axiom,(![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''reduce-4'')).
% 0.30/0.67 tff(141,plain,
% 0.30/0.67 (![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2))))))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[140, 139])).
% 0.30/0.67 tff(142,plain,(
% 0.30/0.67 ![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2))))))),
% 0.30/0.67 inference(skolemize,[status(sab)],[141])).
% 0.30/0.67 tff(143,plain,
% 0.30/0.67 (![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2))))))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[142, 138])).
% 0.30/0.67 tff(144,plain,
% 0.30/0.67 ((~![Vt1: vTable, Vt2: vTable, Vts: vTStore] : (vreduce(vUnion(vtvalue(Vt1), vtvalue(Vt2)), Vts) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt1), vrawUnion(vgetRaw(Vt1), vgetRaw(Vt2))))))) | (vreduce(vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vts!308) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))))),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(145,plain,
% 0.30/0.67 (vreduce(vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vts!308) = vsomeQuery(vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[144, 143])).
% 0.30/0.67 tff(146,plain,
% 0.30/0.67 (vsomeQuery(vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) = vreduce(vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vts!308)),
% 0.30/0.67 inference(symmetry,[status(thm)],[145])).
% 0.30/0.67 tff(147,plain,
% 0.30/0.67 (vsomeQuery(vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) = vsomeQuery(Vqr!312)),
% 0.30/0.67 inference(transitivity,[status(thm)],[146, 136, 135])).
% 0.30/0.67 tff(148,plain,
% 0.30/0.67 (vgetQuery(vsomeQuery(vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))))) = vgetQuery(vsomeQuery(Vqr!312))),
% 0.30/0.67 inference(monotonicity,[status(thm)],[147])).
% 0.30/0.67 tff(149,plain,
% 0.30/0.67 ((~![Vq: vQuery] : (vgetQuery(vsomeQuery(Vq)) = Vq)) | (vgetQuery(vsomeQuery(vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))))) = vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))))),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(150,plain,
% 0.30/0.67 (vgetQuery(vsomeQuery(vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))))) = vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[149, 132])).
% 0.30/0.67 tff(151,plain,
% 0.30/0.67 (vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))) = vgetQuery(vsomeQuery(vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))))),
% 0.30/0.67 inference(symmetry,[status(thm)],[150])).
% 0.30/0.67 tff(152,plain,
% 0.30/0.67 (vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))) = Vqr!312),
% 0.30/0.67 inference(transitivity,[status(thm)],[151, 148, 134])).
% 0.30/0.67 tff(153,plain,
% 0.30/0.67 (vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307) <=> vptcheck(Vttc!310, Vqr!312, Vtt!307)),
% 0.30/0.67 inference(monotonicity,[status(thm)],[152])).
% 0.30/0.67 tff(154,plain,
% 0.30/0.67 (vptcheck(Vttc!310, Vqr!312, Vtt!307) <=> vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307)),
% 0.30/0.67 inference(symmetry,[status(thm)],[153])).
% 0.30/0.67 tff(155,plain,
% 0.30/0.67 ((~vptcheck(Vttc!310, Vqr!312, Vtt!307)) <=> (~vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307))),
% 0.30/0.67 inference(monotonicity,[status(thm)],[154])).
% 0.30/0.67 tff(156,plain,
% 0.30/0.67 (~vptcheck(Vttc!310, Vqr!312, Vtt!307)),
% 0.30/0.67 inference(or_elim,[status(thm)],[76])).
% 0.30/0.67 tff(157,plain,
% 0.30/0.67 (~vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307)),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[156, 155])).
% 0.30/0.67 tff(158,plain,
% 0.30/0.67 (^[VTT: vTType, Vt: vTable, VTTC: vTTContext] : refl(((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT)) <=> ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT)))),
% 0.30/0.67 inference(bind,[status(th)],[])).
% 0.30/0.67 tff(159,plain,
% 0.30/0.67 (![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT)) <=> ![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))),
% 0.30/0.67 inference(quant_intro,[status(thm)],[158])).
% 0.30/0.67 tff(160,plain,
% 0.30/0.67 (![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT)) <=> ![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(161,plain,
% 0.30/0.67 (^[VTT: vTType, Vt: vTable, VTTC: vTTContext] : rewrite((vwelltypedtable(VTT, Vt) => vptcheck(VTTC, vtvalue(Vt), VTT)) <=> ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT)))),
% 0.30/0.67 inference(bind,[status(th)],[])).
% 0.30/0.67 tff(162,plain,
% 0.30/0.67 (![VTT: vTType, Vt: vTable, VTTC: vTTContext] : (vwelltypedtable(VTT, Vt) => vptcheck(VTTC, vtvalue(Vt), VTT)) <=> ![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))),
% 0.30/0.67 inference(quant_intro,[status(thm)],[161])).
% 0.30/0.67 tff(163,axiom,(![VTT: vTType, Vt: vTable, VTTC: vTTContext] : (vwelltypedtable(VTT, Vt) => vptcheck(VTTC, vtvalue(Vt), VTT))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Ttvalue'')).
% 0.30/0.67 tff(164,plain,
% 0.30/0.67 (![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[163, 162])).
% 0.30/0.67 tff(165,plain,
% 0.30/0.67 (![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[164, 160])).
% 0.30/0.67 tff(166,plain,(
% 0.30/0.67 ![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))),
% 0.30/0.67 inference(skolemize,[status(sab)],[165])).
% 0.30/0.67 tff(167,plain,
% 0.30/0.67 (![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[166, 159])).
% 0.30/0.67 tff(168,plain,
% 0.30/0.67 (((~![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))) | ((~vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) | vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307))) <=> ((~![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))) | (~vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) | vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307))),
% 0.30/0.67 inference(rewrite,[status(thm)],[])).
% 0.30/0.67 tff(169,plain,
% 0.30/0.67 ((~![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))) | ((~vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) | vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307))),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(170,plain,
% 0.30/0.67 ((~![VTT: vTType, Vt: vTable, VTTC: vTTContext] : ((~vwelltypedtable(VTT, Vt)) | vptcheck(VTTC, vtvalue(Vt), VTT))) | (~vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) | vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307)),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[169, 168])).
% 0.30/0.67 tff(171,plain,
% 0.30/0.67 ((~vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) | vptcheck(Vttc!310, vtvalue(vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))), Vtt!307)),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[170, 167])).
% 0.30/0.67 tff(172,plain,
% 0.30/0.67 (~vwelltypedtable(Vtt!307, vtable(vgetAttrL(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[171, 157])).
% 0.30/0.67 tff(173,plain,
% 0.30/0.67 (~vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[172, 126])).
% 0.30/0.67 tff(174,plain,
% 0.30/0.67 ((((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) | ((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))) | vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt!311), vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(tautology,[status(thm)],[])).
% 0.30/0.67 tff(175,plain,
% 0.30/0.67 ((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[174, 173, 122])).
% 0.30/0.67 tff(176,plain,
% 0.30/0.67 ((~((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))))) | (~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(tautology,[status(thm)],[])).
% 0.30/0.67 tff(177,plain,
% 0.30/0.67 (~vwelltypedRawtable(Vtt!307, vrawUnion(vgetRaw(Vt!311), vgetRaw(Vt2!309)))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[176, 175, 120])).
% 0.30/0.67 tff(178,plain,
% 0.30/0.67 (~vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309)))),
% 0.30/0.67 inference(modus_ponens,[status(thm)],[177, 49])).
% 0.30/0.67 tff(179,plain,
% 0.30/0.67 (((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt!311))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311)))) | vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))),
% 0.30/0.67 inference(tautology,[status(thm)],[])).
% 0.30/0.67 tff(180,plain,
% 0.30/0.67 (vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[179, 118])).
% 0.30/0.67 tff(181,plain,
% 0.30/0.67 ((~![Vtt: vTType, Val: vAttrL, Vt1: vRawTable] : (~(((~vmatchingAttrL(Vtt, Val)) | (~vwelltypedRawtable(Vtt, Vt1))) <=> vwelltypedtable(Vtt, vtable(Val, Vt1))))) | (~(((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309)))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309)))))),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(182,plain,
% 0.30/0.67 (~(((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309)))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309))))),
% 0.30/0.67 inference(unit_resolution,[status(thm)],[181, 59])).
% 0.30/0.67 tff(183,plain,
% 0.30/0.67 ((~![VTable0: vTable] : (VTable0 = vtable(tptp_fun_VwildcardName00_47(VTable0), vgetRaw(VTable0)))) | (Vt2!309 = vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309)))),
% 0.30/0.67 inference(quant_inst,[status(thm)],[])).
% 0.30/0.67 tff(184,plain,
% 0.30/0.67 (Vt2!309 = vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309))),
% 0.30/0.68 inference(unit_resolution,[status(thm)],[183, 10])).
% 0.30/0.68 tff(185,plain,
% 0.30/0.68 (vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309)) = Vt2!309),
% 0.30/0.68 inference(symmetry,[status(thm)],[184])).
% 0.30/0.68 tff(186,plain,
% 0.30/0.68 (vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309))) <=> vwelltypedtable(Vtt!307, Vt2!309)),
% 0.30/0.68 inference(monotonicity,[status(thm)],[185])).
% 0.30/0.68 tff(187,plain,
% 0.30/0.68 (vwelltypedtable(Vtt!307, Vt2!309) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309)))),
% 0.30/0.68 inference(symmetry,[status(thm)],[186])).
% 0.30/0.68 tff(188,plain,
% 0.30/0.68 (^[VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : refl(((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT)) <=> ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT)))),
% 0.30/0.68 inference(bind,[status(th)],[])).
% 0.30/0.68 tff(189,plain,
% 0.30/0.68 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT)) <=> ![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))),
% 0.30/0.68 inference(quant_intro,[status(thm)],[188])).
% 0.30/0.68 tff(190,plain,
% 0.30/0.68 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT)) <=> ![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))),
% 0.30/0.68 inference(rewrite,[status(thm)],[])).
% 0.30/0.68 tff(191,plain,
% 0.30/0.68 (^[VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : rewrite((vptcheck(VTTC, vUnion(Vq1, Vq2), VTT) => vptcheck(VTTC, Vq2, VTT)) <=> ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT)))),
% 0.30/0.68 inference(bind,[status(th)],[])).
% 0.30/0.68 tff(192,plain,
% 0.30/0.68 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : (vptcheck(VTTC, vUnion(Vq1, Vq2), VTT) => vptcheck(VTTC, Vq2, VTT)) <=> ![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))),
% 0.30/0.68 inference(quant_intro,[status(thm)],[191])).
% 0.30/0.68 tff(193,axiom,(![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : (vptcheck(VTTC, vUnion(Vq1, Vq2), VTT) => vptcheck(VTTC, Vq2, VTT))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''TUnion_inv2'')).
% 0.30/0.68 tff(194,plain,
% 0.30/0.68 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[193, 192])).
% 0.30/0.68 tff(195,plain,
% 0.30/0.68 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[194, 190])).
% 0.30/0.68 tff(196,plain,(
% 0.30/0.68 ![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))),
% 0.30/0.68 inference(skolemize,[status(sab)],[195])).
% 0.30/0.68 tff(197,plain,
% 0.30/0.68 (![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[196, 189])).
% 0.30/0.68 tff(198,plain,
% 0.30/0.68 (((~![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))) | ((~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307))) <=> ((~![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))) | (~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307))),
% 0.30/0.68 inference(rewrite,[status(thm)],[])).
% 0.30/0.68 tff(199,plain,
% 0.30/0.68 ((~![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))) | ((~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307))),
% 0.30/0.68 inference(quant_inst,[status(thm)],[])).
% 0.30/0.68 tff(200,plain,
% 0.30/0.68 ((~![VTTC: vTTContext, Vq1: vQuery, Vq2: vQuery, VTT: vTType] : ((~vptcheck(VTTC, vUnion(Vq1, Vq2), VTT)) | vptcheck(VTTC, Vq2, VTT))) | (~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307)),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[199, 198])).
% 0.30/0.68 tff(201,plain,
% 0.30/0.68 ((~vptcheck(Vttc!310, vUnion(vtvalue(Vt!311), vtvalue(Vt2!309)), Vtt!307)) | vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307)),
% 0.30/0.68 inference(unit_resolution,[status(thm)],[200, 197])).
% 0.30/0.68 tff(202,plain,
% 0.30/0.68 (vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307)),
% 0.30/0.68 inference(unit_resolution,[status(thm)],[201, 86])).
% 0.30/0.68 tff(203,plain,
% 0.30/0.68 (((~![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))) | ((~vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307)) | vwelltypedtable(Vtt!307, Vt2!309))) <=> ((~![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))) | (~vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307)) | vwelltypedtable(Vtt!307, Vt2!309))),
% 0.30/0.68 inference(rewrite,[status(thm)],[])).
% 0.30/0.68 tff(204,plain,
% 0.30/0.68 ((~![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))) | ((~vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307)) | vwelltypedtable(Vtt!307, Vt2!309))),
% 0.30/0.68 inference(quant_inst,[status(thm)],[])).
% 0.30/0.68 tff(205,plain,
% 0.30/0.68 ((~![VTTC: vTTContext, Vt: vTable, VTT: vTType] : ((~vptcheck(VTTC, vtvalue(Vt), VTT)) | vwelltypedtable(VTT, Vt))) | (~vptcheck(Vttc!310, vtvalue(Vt2!309), Vtt!307)) | vwelltypedtable(Vtt!307, Vt2!309)),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[204, 203])).
% 0.30/0.68 tff(206,plain,
% 0.30/0.68 (vwelltypedtable(Vtt!307, Vt2!309)),
% 0.30/0.68 inference(unit_resolution,[status(thm)],[205, 111, 202])).
% 0.30/0.68 tff(207,plain,
% 0.30/0.68 (vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309)))),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[206, 187])).
% 0.30/0.68 tff(208,plain,
% 0.30/0.68 ((((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309)))) <=> vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309)))) | (~((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))))) | (~vwelltypedtable(Vtt!307, vtable(tptp_fun_VwildcardName00_47(Vt2!309), vgetRaw(Vt2!309))))),
% 0.30/0.68 inference(tautology,[status(thm)],[])).
% 0.30/0.68 tff(209,plain,
% 0.30/0.68 (~((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))))),
% 0.30/0.68 inference(unit_resolution,[status(thm)],[208, 207, 182])).
% 0.30/0.68 tff(210,plain,
% 0.30/0.68 (((~vmatchingAttrL(Vtt!307, tptp_fun_VwildcardName00_47(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309)))) | vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))),
% 0.30/0.68 inference(tautology,[status(thm)],[])).
% 0.30/0.68 tff(211,plain,
% 0.30/0.68 (vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))),
% 0.30/0.68 inference(unit_resolution,[status(thm)],[210, 209])).
% 0.30/0.68 tff(212,plain,
% 0.30/0.68 (^[Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : refl((vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))) <=> (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))))),
% 0.30/0.68 inference(bind,[status(th)],[])).
% 0.30/0.68 tff(213,plain,
% 0.30/0.68 (![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))) <=> ![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))),
% 0.30/0.68 inference(quant_intro,[status(thm)],[212])).
% 0.30/0.68 tff(214,plain,
% 0.30/0.68 (^[Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : trans(monotonicity(trans(monotonicity(rewrite((vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1)) <=> (~((~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))))), ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) <=> (~(~((~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))))))), rewrite((~(~((~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))))) <=> ((~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))), ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) <=> ((~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))))), (((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))) <=> (((~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))))), rewrite((((~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))) <=> (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))), (((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))) <=> (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))))),
% 0.30/0.68 inference(bind,[status(th)],[])).
% 0.30/0.68 tff(215,plain,
% 0.30/0.68 (![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))) <=> ![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))),
% 0.30/0.68 inference(quant_intro,[status(thm)],[214])).
% 0.30/0.68 tff(216,plain,
% 0.30/0.68 (![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))) <=> ![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)))),
% 0.30/0.68 inference(rewrite,[status(thm)],[])).
% 0.30/0.68 tff(217,plain,
% 0.30/0.68 (^[Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : rewrite(((vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1)) => vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))) <=> ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))))),
% 0.30/0.68 inference(bind,[status(th)],[])).
% 0.30/0.68 tff(218,plain,
% 0.30/0.68 (![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1)) => vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1))) <=> ![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)))),
% 0.30/0.68 inference(quant_intro,[status(thm)],[217])).
% 0.30/0.68 tff(219,axiom,(![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1)) => vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','rawUnionPreservesWellTypedRaw')).
% 0.30/0.68 tff(220,plain,
% 0.30/0.68 (![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)))),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[219, 218])).
% 0.30/0.68 tff(221,plain,
% 0.30/0.68 (![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)))),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[220, 216])).
% 0.30/0.68 tff(222,plain,(
% 0.30/0.68 ![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : ((~(vwelltypedRawtable(Vtt, Vrt) & vwelltypedRawtable(Vtt, Vrt1))) | vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)))),
% 0.30/0.68 inference(skolemize,[status(sab)],[221])).
% 0.30/0.68 tff(223,plain,
% 0.30/0.68 (![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[222, 215])).
% 0.30/0.68 tff(224,plain,
% 0.30/0.68 (![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))),
% 0.30/0.68 inference(modus_ponens,[status(thm)],[223, 213])).
% 0.30/0.68 tff(225,plain,
% 0.30/0.68 (((~![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))) | ((~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))) | vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))) | vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.68 inference(rewrite,[status(thm)],[])).
% 0.30/0.68 tff(226,plain,
% 0.30/0.68 ((vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311)))) <=> ((~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))) | vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.68 inference(rewrite,[status(thm)],[])).
% 0.30/0.68 tff(227,plain,
% 0.30/0.68 (((~![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))) | (vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))) | ((~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))) | vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309)))))),
% 0.30/0.68 inference(monotonicity,[status(thm)],[226])).
% 0.30/0.68 tff(228,plain,
% 0.30/0.68 (((~![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))) | (vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))))) <=> ((~![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))) | vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))))),
% 0.30/0.68 inference(transitivity,[status(thm)],[227, 225])).
% 0.30/0.68 tff(229,plain,
% 0.30/0.68 ((~![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))) | (vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))))),
% 0.30/0.68 inference(quant_inst,[status(thm)],[])).
% 0.30/0.68 tff(230,plain,
% 0.30/0.68 ((~![Vtt: vTType, Vrt: vRawTable, Vrt1: vRawTable] : (vwelltypedRawtable(Vtt, vrawUnion(Vrt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt1)) | (~vwelltypedRawtable(Vtt, Vrt)))) | (~vwelltypedRawtable(Vtt!307, vgetRaw(Vt2!309))) | (~vwelltypedRawtable(Vtt!307, tptp_fun_VwildcardName00_48(Vt!311))) | vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309)))),
% 0.38/0.70 inference(modus_ponens,[status(thm)],[229, 228])).
% 0.38/0.70 tff(231,plain,
% 0.38/0.70 (vwelltypedRawtable(Vtt!307, vrawUnion(tptp_fun_VwildcardName00_48(Vt!311), vgetRaw(Vt2!309)))),
% 0.38/0.70 inference(unit_resolution,[status(thm)],[230, 224, 211, 180])).
% 0.38/0.70 tff(232,plain,
% 0.38/0.70 ($false),
% 0.38/0.70 inference(unit_resolution,[status(thm)],[231, 178])).
% 0.38/0.70 % SZS output end Proof
% 0.38/0.70 % E exiting
%------------------------------------------------------------------------------