%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : COM286_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n021.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:06 PM UTC 2026
% Result : Theorem 0.31s 0.51s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM286_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.16/0.33 % Computer : n021.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 20:20:56 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.31/0.51 % SZS status Theorem
% 0.31/0.51 % SZS output start Proof
% 0.31/0.51 tff(vtvalue_type, type, (
% 0.31/0.51 vtvalue: vTable > vQuery)).
% 0.31/0.51 tff(tptp_fun_Vt200_207_type, type, (
% 0.31/0.51 tptp_fun_Vt200_207: vQuery > vTable)).
% 0.31/0.51 tff(vq2_type, type, (
% 0.31/0.51 vq2: vQuery)).
% 0.31/0.51 tff(vnoQuery_type, type, (
% 0.31/0.51 vnoQuery: vOptQuery)).
% 0.31/0.51 tff(vreduce_type, type, (
% 0.31/0.51 vreduce: ( vQuery * vTStore ) > vOptQuery)).
% 0.31/0.51 tff(tptp_fun_Vts_308_type, type, (
% 0.31/0.51 tptp_fun_Vts_308: vTStore)).
% 0.31/0.51 tff(vDifference_type, type, (
% 0.31/0.51 vDifference: ( vQuery * vQuery ) > vQuery)).
% 0.31/0.51 tff(tptp_fun_Vt_310_type, type, (
% 0.31/0.51 tptp_fun_Vt_310: vTable)).
% 0.31/0.51 tff(vsomeQuery_type, type, (
% 0.31/0.51 vsomeQuery: vQuery > vOptQuery)).
% 0.31/0.51 tff(tptp_fun_Vqr_311_type, type, (
% 0.31/0.51 tptp_fun_Vqr_311: vQuery)).
% 0.31/0.51 tff(vq1_type, type, (
% 0.31/0.51 vq1: vQuery)).
% 0.31/0.51 tff(vptcheck_type, type, (
% 0.31/0.51 vptcheck: ( vTTContext * vQuery * vTType ) > $o)).
% 0.31/0.51 tff(tptp_fun_Vtt_307_type, type, (
% 0.31/0.51 tptp_fun_Vtt_307: vTType)).
% 0.31/0.51 tff(tptp_fun_Vttc_309_type, type, (
% 0.31/0.51 tptp_fun_Vttc_309: vTTContext)).
% 0.31/0.51 tff(vstoreContextConsistent_type, type, (
% 0.31/0.51 vstoreContextConsistent: ( vTStore * vTTContext ) > $o)).
% 0.31/0.51 tff(visSomeQuery_type, type, (
% 0.31/0.51 visSomeQuery: vOptQuery > $o)).
% 0.31/0.51 tff(1,plain,
% 0.31/0.51 ((vsomeQuery(Vqr!311) = vnoQuery) <=> (vnoQuery = vsomeQuery(Vqr!311))),
% 0.31/0.51 inference(commutativity,[status(thm)],[])).
% 0.31/0.51 tff(2,plain,
% 0.31/0.51 ((((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311))) & (~vptcheck(Vttc!309, Vqr!311, Vtt!307))) <=> ((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311)) & (~vptcheck(Vttc!309, Vqr!311, Vtt!307)))),
% 0.31/0.51 inference(rewrite,[status(thm)],[])).
% 0.31/0.51 tff(3,plain,
% 0.31/0.51 (((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311))) <=> ((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311)))),
% 0.31/0.51 inference(rewrite,[status(thm)],[])).
% 0.31/0.51 tff(4,plain,
% 0.31/0.51 ((((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311))) & (~vptcheck(Vttc!309, Vqr!311, Vtt!307))) <=> (((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311))) & (~vptcheck(Vttc!309, Vqr!311, Vtt!307)))),
% 0.31/0.51 inference(monotonicity,[status(thm)],[3])).
% 0.31/0.51 tff(5,plain,
% 0.31/0.51 ((((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311))) & (~vptcheck(Vttc!309, Vqr!311, Vtt!307))) <=> ((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311)) & (~vptcheck(Vttc!309, Vqr!311, Vtt!307)))),
% 0.31/0.51 inference(transitivity,[status(thm)],[4, 2])).
% 0.31/0.51 tff(6,plain,
% 0.31/0.51 ((~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : ((~((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))) <=> (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : ((~((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt)))),
% 0.31/0.51 inference(rewrite,[status(thm)],[])).
% 0.31/0.51 tff(7,plain,
% 0.31/0.51 ((~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : (((((((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200)))) & (vq1 = vtvalue(Vt))) & vstoreContextConsistent(Vts, Vttc)) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt)) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr))) => vptcheck(Vttc, Vqr, Vtt))) <=> (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : ((~((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt)))),
% 0.31/0.51 inference(rewrite,[status(thm)],[])).
% 0.31/0.51 tff(8,axiom,(~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : (((((((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200)))) & (vq1 = vtvalue(Vt))) & vstoreContextConsistent(Vts, Vttc)) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt)) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr))) => vptcheck(Vttc, Vqr, Vtt))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''Preservation-Difference-tvalue-q2-isSomeQuery-False'')).
% 0.31/0.51 tff(9,plain,
% 0.31/0.51 (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : ((~((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[8, 7])).
% 0.31/0.51 tff(10,plain,
% 0.31/0.51 (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : ((~((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[9, 6])).
% 0.31/0.51 tff(11,plain,
% 0.31/0.51 (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : ((~((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[10, 6])).
% 0.31/0.51 tff(12,plain,
% 0.31/0.51 (~![Vqr: vQuery, Vt: vTable, Vttc: vTTContext, Vts: vTStore, Vtt: vTType] : ((~((~visSomeQuery(vreduce(vq2, Vts))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt)) & vstoreContextConsistent(Vts, Vttc) & vptcheck(Vttc, vDifference(vq1, vq2), Vtt) & (vreduce(vDifference(vq1, vq2), Vts) = vsomeQuery(Vqr)))) | vptcheck(Vttc, Vqr, Vtt))),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[11, 6])).
% 0.31/0.51 tff(13,plain,
% 0.31/0.51 ((~visSomeQuery(vreduce(vq2, Vts!308))) & ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) & (vq1 = vtvalue(Vt!310)) & vstoreContextConsistent(Vts!308, Vttc!309) & vptcheck(Vttc!309, vDifference(vq1, vq2), Vtt!307) & (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311)) & (~vptcheck(Vttc!309, Vqr!311, Vtt!307))),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[12, 5])).
% 0.31/0.51 tff(14,plain,
% 0.31/0.51 (vreduce(vDifference(vq1, vq2), Vts!308) = vsomeQuery(Vqr!311)),
% 0.31/0.51 inference(and_elim,[status(thm)],[13])).
% 0.31/0.51 tff(15,plain,
% 0.31/0.51 (vq1 = vtvalue(Vt!310)),
% 0.31/0.51 inference(and_elim,[status(thm)],[13])).
% 0.31/0.51 tff(16,plain,
% 0.31/0.51 (vtvalue(Vt!310) = vq1),
% 0.31/0.51 inference(symmetry,[status(thm)],[15])).
% 0.31/0.51 tff(17,plain,
% 0.31/0.51 (vDifference(vtvalue(Vt!310), vq2) = vDifference(vq1, vq2)),
% 0.31/0.51 inference(monotonicity,[status(thm)],[16])).
% 0.31/0.51 tff(18,plain,
% 0.31/0.51 (vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vreduce(vDifference(vq1, vq2), Vts!308)),
% 0.31/0.51 inference(monotonicity,[status(thm)],[17])).
% 0.31/0.51 tff(19,plain,
% 0.31/0.51 (vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vsomeQuery(Vqr!311)),
% 0.31/0.51 inference(transitivity,[status(thm)],[18, 14])).
% 0.31/0.51 tff(20,plain,
% 0.31/0.51 ((vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery) <=> (vsomeQuery(Vqr!311) = vnoQuery)),
% 0.31/0.51 inference(monotonicity,[status(thm)],[19])).
% 0.31/0.51 tff(21,plain,
% 0.31/0.51 ((vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery) <=> (vnoQuery = vsomeQuery(Vqr!311))),
% 0.31/0.51 inference(transitivity,[status(thm)],[20, 1])).
% 0.31/0.51 tff(22,plain,
% 0.31/0.51 ((vnoQuery = vsomeQuery(Vqr!311)) <=> (vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery)),
% 0.31/0.51 inference(symmetry,[status(thm)],[21])).
% 0.31/0.51 tff(23,plain,
% 0.31/0.51 ((~(vnoQuery = vsomeQuery(Vqr!311))) <=> (~(vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery))),
% 0.31/0.51 inference(monotonicity,[status(thm)],[22])).
% 0.31/0.51 tff(24,plain,
% 0.31/0.51 (^[VQuery0: vQuery] : refl((~(vnoQuery = vsomeQuery(VQuery0))) <=> (~(vnoQuery = vsomeQuery(VQuery0))))),
% 0.31/0.51 inference(bind,[status(th)],[])).
% 0.31/0.51 tff(25,plain,
% 0.31/0.51 (![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0))) <=> ![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0)))),
% 0.31/0.51 inference(quant_intro,[status(thm)],[24])).
% 0.31/0.51 tff(26,plain,
% 0.31/0.51 (![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0))) <=> ![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0)))),
% 0.31/0.51 inference(rewrite,[status(thm)],[])).
% 0.31/0.51 tff(27,axiom,(![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''DIFF-noQuery-someQuery'')).
% 0.31/0.51 tff(28,plain,
% 0.31/0.51 (![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0)))),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.31/0.51 tff(29,plain,(
% 0.31/0.51 ![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0)))),
% 0.31/0.51 inference(skolemize,[status(sab)],[28])).
% 0.31/0.51 tff(30,plain,
% 0.31/0.51 (![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0)))),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[29, 25])).
% 0.31/0.51 tff(31,plain,
% 0.31/0.51 ((~![VQuery0: vQuery] : (~(vnoQuery = vsomeQuery(VQuery0)))) | (~(vnoQuery = vsomeQuery(Vqr!311)))),
% 0.31/0.51 inference(quant_inst,[status(thm)],[])).
% 0.31/0.51 tff(32,plain,
% 0.31/0.51 (~(vnoQuery = vsomeQuery(Vqr!311))),
% 0.31/0.51 inference(unit_resolution,[status(thm)],[31, 30])).
% 0.31/0.51 tff(33,plain,
% 0.31/0.51 (~(vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery)),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[32, 23])).
% 0.31/0.51 tff(34,plain,
% 0.31/0.51 (~visSomeQuery(vreduce(vq2, Vts!308))),
% 0.31/0.51 inference(and_elim,[status(thm)],[13])).
% 0.31/0.51 tff(35,plain,
% 0.31/0.51 (^[Vt: vTable, Vq2: vQuery, Vts: vTStore] : refl((visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2)))) <=> (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2)))))),
% 0.31/0.51 inference(bind,[status(th)],[])).
% 0.31/0.51 tff(36,plain,
% 0.31/0.51 (![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2)))) <=> ![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))),
% 0.31/0.51 inference(quant_intro,[status(thm)],[35])).
% 0.31/0.51 tff(37,plain,
% 0.31/0.51 (^[Vt: vTable, Vq2: vQuery, Vts: vTStore] : trans(monotonicity(rewrite(((Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))) | visSomeQuery(vreduce(Vq2, Vts))) <=> (visSomeQuery(vreduce(Vq2, Vts)) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))), ((((Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))) | visSomeQuery(vreduce(Vq2, Vts))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> ((visSomeQuery(vreduce(Vq2, Vts)) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2)))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)))), rewrite(((visSomeQuery(vreduce(Vq2, Vts)) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2)))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))), ((((Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))) | visSomeQuery(vreduce(Vq2, Vts))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))))),
% 0.31/0.51 inference(bind,[status(th)],[])).
% 0.31/0.51 tff(38,plain,
% 0.31/0.51 (![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (((Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))) | visSomeQuery(vreduce(Vq2, Vts))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> ![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))),
% 0.31/0.51 inference(quant_intro,[status(thm)],[37])).
% 0.31/0.51 tff(39,plain,
% 0.31/0.51 (![Vt: vTable, Vq2: vQuery, Vts: vTStore] : ((~(![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts))))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> ![Vt: vTable, Vq2: vQuery, Vts: vTStore] : ((~(![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts))))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery))),
% 0.31/0.51 inference(rewrite,[status(thm)],[])).
% 0.31/0.51 tff(40,plain,
% 0.31/0.51 (^[Vt: vTable, Vq2: vQuery, Vts: vTStore] : trans(monotonicity(rewrite((![Vt100: vTable, Vt200: vTable] : ((~(Vt = Vt100)) | (~(Vq2 = vtvalue(Vt200)))) & (~visSomeQuery(vreduce(Vq2, Vts)))) <=> (![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts))))), (((![Vt100: vTable, Vt200: vTable] : ((~(Vt = Vt100)) | (~(Vq2 = vtvalue(Vt200)))) & (~visSomeQuery(vreduce(Vq2, Vts)))) => (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> ((![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts)))) => (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)))), rewrite(((![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts)))) => (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> ((~(![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts))))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery))), (((![Vt100: vTable, Vt200: vTable] : ((~(Vt = Vt100)) | (~(Vq2 = vtvalue(Vt200)))) & (~visSomeQuery(vreduce(Vq2, Vts)))) => (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> ((~(![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts))))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery))))),
% 0.31/0.51 inference(bind,[status(th)],[])).
% 0.31/0.51 tff(41,plain,
% 0.31/0.51 (![Vt: vTable, Vq2: vQuery, Vts: vTStore] : ((![Vt100: vTable, Vt200: vTable] : ((~(Vt = Vt100)) | (~(Vq2 = vtvalue(Vt200)))) & (~visSomeQuery(vreduce(Vq2, Vts)))) => (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery)) <=> ![Vt: vTable, Vq2: vQuery, Vts: vTStore] : ((~(![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts))))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery))),
% 0.31/0.51 inference(quant_intro,[status(thm)],[40])).
% 0.31/0.51 tff(42,axiom,(![Vt: vTable, Vq2: vQuery, Vts: vTStore] : ((![Vt100: vTable, Vt200: vTable] : ((~(Vt = Vt100)) | (~(Vq2 = vtvalue(Vt200)))) & (~visSomeQuery(vreduce(Vq2, Vts)))) => (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery))), file('/export/starexec/sandbox/benchmark/theBenchmark.p',''reduce-16'')).
% 0.31/0.51 tff(43,plain,
% 0.31/0.51 (![Vt: vTable, Vq2: vQuery, Vts: vTStore] : ((~(![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts))))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery))),
% 0.31/0.51 inference(modus_ponens,[status(thm)],[42, 41])).
% 0.31/0.54 tff(44,plain,
% 0.31/0.54 (![Vt: vTable, Vq2: vQuery, Vts: vTStore] : ((~(![Vt200: vTable] : (~(Vq2 = vtvalue(Vt200))) & (~visSomeQuery(vreduce(Vq2, Vts))))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery))),
% 0.31/0.54 inference(modus_ponens,[status(thm)],[43, 39])).
% 0.31/0.54 tff(45,plain,(
% 0.31/0.54 ![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (((Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))) | visSomeQuery(vreduce(Vq2, Vts))) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery))),
% 0.31/0.54 inference(skolemize,[status(sab)],[44])).
% 0.31/0.54 tff(46,plain,
% 0.31/0.54 (![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))),
% 0.31/0.54 inference(modus_ponens,[status(thm)],[45, 38])).
% 0.31/0.54 tff(47,plain,
% 0.31/0.54 (![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))),
% 0.31/0.54 inference(modus_ponens,[status(thm)],[46, 36])).
% 0.31/0.54 tff(48,plain,
% 0.31/0.54 (((~![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))) | (visSomeQuery(vreduce(vq2, Vts!308)) | (vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery) | (vq2 = vtvalue(tptp_fun_Vt200_207(vq2))))) <=> ((~![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))) | visSomeQuery(vreduce(vq2, Vts!308)) | (vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery) | (vq2 = vtvalue(tptp_fun_Vt200_207(vq2))))),
% 0.31/0.54 inference(rewrite,[status(thm)],[])).
% 0.31/0.54 tff(49,plain,
% 0.31/0.54 ((~![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))) | (visSomeQuery(vreduce(vq2, Vts!308)) | (vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery) | (vq2 = vtvalue(tptp_fun_Vt200_207(vq2))))),
% 0.31/0.54 inference(quant_inst,[status(thm)],[])).
% 0.31/0.54 tff(50,plain,
% 0.31/0.54 ((~![Vt: vTable, Vq2: vQuery, Vts: vTStore] : (visSomeQuery(vreduce(Vq2, Vts)) | (vreduce(vDifference(vtvalue(Vt), Vq2), Vts) = vnoQuery) | (Vq2 = vtvalue(tptp_fun_Vt200_207(Vq2))))) | visSomeQuery(vreduce(vq2, Vts!308)) | (vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery) | (vq2 = vtvalue(tptp_fun_Vt200_207(vq2)))),
% 0.31/0.54 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.31/0.54 tff(51,plain,
% 0.31/0.54 ((vreduce(vDifference(vtvalue(Vt!310), vq2), Vts!308) = vnoQuery) | (vq2 = vtvalue(tptp_fun_Vt200_207(vq2)))),
% 0.31/0.54 inference(unit_resolution,[status(thm)],[50, 47, 34])).
% 0.31/0.54 tff(52,plain,
% 0.31/0.54 (vq2 = vtvalue(tptp_fun_Vt200_207(vq2))),
% 0.31/0.54 inference(unit_resolution,[status(thm)],[51, 33])).
% 0.31/0.54 tff(53,plain,
% 0.31/0.54 (^[Vt200: vTable] : refl((~(vq2 = vtvalue(Vt200))) <=> (~(vq2 = vtvalue(Vt200))))),
% 0.31/0.54 inference(bind,[status(th)],[])).
% 0.31/0.54 tff(54,plain,
% 0.31/0.54 (![Vt200: vTable] : (~(vq2 = vtvalue(Vt200))) <=> ![Vt200: vTable] : (~(vq2 = vtvalue(Vt200)))),
% 0.31/0.54 inference(quant_intro,[status(thm)],[53])).
% 0.31/0.54 tff(55,plain,
% 0.31/0.54 (![Vt200: vTable] : (~(vq2 = vtvalue(Vt200)))),
% 0.31/0.54 inference(and_elim,[status(thm)],[13])).
% 0.31/0.54 tff(56,plain,
% 0.31/0.54 (![Vt200: vTable] : (~(vq2 = vtvalue(Vt200)))),
% 0.31/0.54 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.31/0.54 tff(57,plain,
% 0.31/0.54 ((~![Vt200: vTable] : (~(vq2 = vtvalue(Vt200)))) | (~(vq2 = vtvalue(tptp_fun_Vt200_207(vq2))))),
% 0.31/0.54 inference(quant_inst,[status(thm)],[])).
% 0.31/0.54 tff(58,plain,
% 0.31/0.54 ($false),
% 0.31/0.54 inference(unit_resolution,[status(thm)],[57, 56, 52])).
% 0.31/0.54 % SZS output end Proof
% 0.31/0.54 % E exiting
%------------------------------------------------------------------------------