%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM290_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.cPEFC7jnM2 true
% Computer : n026.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:25 PM UTC 2026
% Result : Theorem 79.18s 11.97s
% Output : Refutation 79.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : COM290_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.cPEFC7jnM2 true
% 0.16/0.35 % Computer : n026.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.35 % DateTime : Mon May 4 20:23:23 EDT 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 % Running portfolio for 300 s
% 0.16/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.35 % Number of cores: 8
% 0.18/0.35 % Python version: Python 3.6.8
% 0.18/0.36 % Running in FO mode
% 0.54/0.65 % Total configuration time : 435
% 0.54/0.65 % Estimated wc time : 1092
% 0.54/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.75 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.76 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.76 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.77 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.77 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.77 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.78 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 79.18/11.97 % Solved by fo/fo3_bce.sh.
% 79.18/11.97 % BCE start: 400
% 79.18/11.97 % BCE eliminated: 0
% 79.18/11.97 % PE start: 400
% 79.18/11.97 logic: eq
% 79.18/11.97 % PE eliminated: -44
% 79.18/11.97 % done 5258 iterations in 11.185s
% 79.18/11.97 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 79.18/11.97 % SZS output start Refutation
% 79.18/11.97 thf(vOptQuery_type, type, vOptQuery: $tType).
% 79.18/11.97 thf(vQuery_type, type, vQuery: $tType).
% 79.18/11.97 thf(vTStore_type, type, vTStore: $tType).
% 79.18/11.97 thf(vTable_type, type, vTable: $tType).
% 79.18/11.97 thf(vTTContext_type, type, vTTContext: $tType).
% 79.18/11.97 thf(vTType_type, type, vTType: $tType).
% 79.18/11.97 thf(vSelect_type, type, vSelect: $tType).
% 79.18/11.97 thf(vName_type, type, vName: $tType).
% 79.18/11.97 thf(vPred_type, type, vPred: $tType).
% 79.18/11.97 thf(sk__90_type, type, sk__90: vQuery > vPred).
% 79.18/11.97 thf(vtvalue_type, type, vtvalue: vTable > vQuery).
% 79.18/11.97 thf(sk__235_type, type, sk__235: vTable).
% 79.18/11.97 thf(vq2_type, type, vq2: vQuery).
% 79.18/11.97 thf(vptcheck_type, type, vptcheck: vTTContext > vQuery > vTType > $o).
% 79.18/11.97 thf(sk__85_type, type, sk__85: vQuery > vQuery).
% 79.18/11.97 thf(vnoQuery_type, type, vnoQuery: vOptQuery).
% 79.18/11.97 thf(sk__238_type, type, sk__238: vTType).
% 79.18/11.97 thf(sk__91_type, type, sk__91: vOptQuery > vQuery).
% 79.18/11.97 thf(vDifference_type, type, vDifference: vQuery > vQuery > vQuery).
% 79.18/11.97 thf(sk__112_type, type, sk__112: vQuery > vTable).
% 79.18/11.97 thf(visSomeQuery_type, type, visSomeQuery: vOptQuery > $o).
% 79.18/11.97 thf(sk__83_type, type, sk__83: vQuery > vQuery).
% 79.18/11.97 thf(vreduce_type, type, vreduce: vQuery > vTStore > vOptQuery).
% 79.18/11.97 thf(vq1_type, type, vq1: vQuery).
% 79.18/11.97 thf(sk__236_type, type, sk__236: vTTContext).
% 79.18/11.97 thf(vUnion_type, type, vUnion: vQuery > vQuery > vQuery).
% 79.18/11.97 thf(sk__88_type, type, sk__88: vQuery > vSelect).
% 79.18/11.97 thf(vgetQuery_type, type, vgetQuery: vOptQuery > vQuery).
% 79.18/11.97 thf(sk__16_type, type, sk__16: vOptQuery > vQuery).
% 79.18/11.97 thf(visValue_type, type, visValue: vQuery > $o).
% 79.18/11.97 thf(vIntersection_type, type, vIntersection: vQuery > vQuery > vQuery).
% 79.18/11.97 thf(sk__237_type, type, sk__237: vTStore).
% 79.18/11.97 thf(sk__86_type, type, sk__86: vQuery > vQuery).
% 79.18/11.97 thf(sk__82_type, type, sk__82: vQuery > vQuery).
% 79.18/11.97 thf(sk__234_type, type, sk__234: vQuery).
% 79.18/11.97 thf(sk__84_type, type, sk__84: vQuery > vQuery).
% 79.18/11.97 thf(vstoreContextConsistent_type, type, vstoreContextConsistent: vTStore >
% 79.18/11.97 vTTContext > $o).
% 79.18/11.97 thf(vsomeQuery_type, type, vsomeQuery: vQuery > vOptQuery).
% 79.18/11.97 thf(sk__89_type, type, sk__89: vQuery > vName).
% 79.18/11.97 thf(sk__87_type, type, sk__87: vQuery > vQuery).
% 79.18/11.97 thf(vselectFromWhere_type, type, vselectFromWhere: vSelect > vName > vPred > vQuery).
% 79.18/11.97 thf('Preservation-Intersection-tvalue-q2-isSomeQuery-True', conjecture,
% 79.18/11.97 (![Vqr:vQuery,Vt:vTable,Vttc:vTTContext,Vts:vTStore,Vtt:vTType]:
% 79.18/11.97 ( ( ( visSomeQuery @ ( vreduce @ vq2 @ Vts ) ) &
% 79.18/11.97 ( ![Vt200:vTable]: ( ( vq2 ) != ( vtvalue @ Vt200 ) ) ) &
% 79.18/11.97 ( ( vq1 ) = ( vtvalue @ Vt ) ) &
% 79.18/11.97 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 79.18/11.97 ( vptcheck @ Vttc @ ( vIntersection @ vq1 @ vq2 ) @ Vtt ) &
% 79.18/11.97 ( ( vreduce @ ( vIntersection @ vq1 @ vq2 ) @ Vts ) =
% 79.18/11.97 ( vsomeQuery @ Vqr ) ) ) =>
% 79.18/11.97 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 79.18/11.97 thf(zf_stmt_0, negated_conjecture,
% 79.18/11.97 (~( ![Vqr:vQuery,Vt:vTable,Vttc:vTTContext,Vts:vTStore,Vtt:vTType]:
% 79.18/11.97 ( ( ( visSomeQuery @ ( vreduce @ vq2 @ Vts ) ) &
% 79.18/11.97 ( ![Vt200:vTable]: ( ( vq2 ) != ( vtvalue @ Vt200 ) ) ) &
% 79.18/11.97 ( ( vq1 ) = ( vtvalue @ Vt ) ) &
% 79.18/11.97 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 79.18/11.97 ( vptcheck @ Vttc @ ( vIntersection @ vq1 @ vq2 ) @ Vtt ) &
% 79.18/11.97 ( ( vreduce @ ( vIntersection @ vq1 @ vq2 ) @ Vts ) =
% 79.18/11.97 ( vsomeQuery @ Vqr ) ) ) =>
% 79.18/11.97 ( vptcheck @ Vttc @ Vqr @ Vtt ) ) )),
% 79.18/11.97 inference('cnf.neg', [status(esa)],
% 79.18/11.97 [Preservation-Intersection-tvalue-q2-isSomeQuery-True])).
% 79.18/11.97 thf(zip_derived_cl393, plain, (~ (vptcheck @ sk__236 @ sk__234 @ sk__238)),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(zip_derived_cl398, plain,
% 79.18/11.97 ( (vstoreContextConsistent @ sk__237 @ sk__236)),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(TIntersection_inv2, axiom,
% 79.18/11.97 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 79.18/11.97 ( ( vptcheck @ VTTC @ ( vIntersection @ Vq1 @ Vq2 ) @ VTT ) =>
% 79.18/11.97 ( vptcheck @ VTTC @ Vq2 @ VTT ) ))).
% 79.18/11.97 thf(zip_derived_cl388, plain,
% 79.18/11.97 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 79.18/11.97 ( (vptcheck @ X0 @ X1 @ X2)
% 79.18/11.97 | ~ (vptcheck @ X0 @ (vIntersection @ X3 @ X1) @ X2))),
% 79.18/11.97 inference('cnf', [status(esa)], [TIntersection_inv2])).
% 79.18/11.97 thf(zip_derived_cl394, plain,
% 79.18/11.97 ( (vptcheck @ sk__236 @ (vIntersection @ vq1 @ vq2) @ sk__238)),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(zip_derived_cl5330, plain, ( (vptcheck @ sk__236 @ vq2 @ sk__238)),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl388, zip_derived_cl394])).
% 79.18/11.97 thf('Preservation-Intersection-IH1', axiom,
% 79.18/11.97 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 79.18/11.97 ( ( ( vstoreContextConsistent @ Vts @ Vttc ) &
% 79.18/11.97 ( vptcheck @ Vttc @ vq2 @ Vtt ) &
% 79.18/11.97 ( ( vreduce @ vq2 @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 79.18/11.97 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 79.18/11.97 thf(zip_derived_cl392, plain,
% 79.18/11.97 (![X0 : vTTContext, X1 : vTType, X2 : vTStore, X3 : vQuery]:
% 79.18/11.97 (~ (vptcheck @ X0 @ vq2 @ X1)
% 79.18/11.97 | ~ (vstoreContextConsistent @ X2 @ X0)
% 79.18/11.97 | ((vreduce @ vq2 @ X2) != (vsomeQuery @ X3))
% 79.18/11.97 | (vptcheck @ X0 @ X3 @ X1))),
% 79.18/11.97 inference('cnf', [status(esa)], [Preservation-Intersection-IH1])).
% 79.18/11.97 thf(zip_derived_cl5555, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vTStore]:
% 79.18/11.97 ( (vptcheck @ sk__236 @ X0 @ sk__238)
% 79.18/11.97 | ((vreduce @ vq2 @ X1) != (vsomeQuery @ X0))
% 79.18/11.97 | ~ (vstoreContextConsistent @ X1 @ sk__236))),
% 79.18/11.97 inference('sup-', [status(thm)], [zip_derived_cl5330, zip_derived_cl392])).
% 79.18/11.97 thf(zip_derived_cl5571, plain,
% 79.18/11.97 (![X0 : vQuery]:
% 79.18/11.97 (((vreduce @ vq2 @ sk__237) != (vsomeQuery @ X0))
% 79.18/11.97 | (vptcheck @ sk__236 @ X0 @ sk__238))),
% 79.18/11.97 inference('sup-', [status(thm)], [zip_derived_cl398, zip_derived_cl5555])).
% 79.18/11.97 thf(zip_derived_cl397, plain, (((vq1) = (vtvalue @ sk__235))),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf('reduce-10', axiom,
% 79.18/11.97 (![Vt:vTable,Vq2:vQuery,Vts:vTStore]:
% 79.18/11.97 ( ( ( ![Vt100:vTable,Vt200:vTable]:
% 79.18/11.97 ( ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) | ( ( Vt ) != ( Vt100 ) ) ) ) &
% 79.18/11.97 ( visSomeQuery @ ( vreduce @ Vq2 @ Vts ) ) ) =>
% 79.18/11.97 ( ( vreduce @ ( vIntersection @ ( vtvalue @ Vt ) @ Vq2 ) @ Vts ) =
% 79.18/11.97 ( vsomeQuery @
% 79.18/11.97 ( vIntersection @
% 79.18/11.97 ( vtvalue @ Vt ) @ ( vgetQuery @ ( vreduce @ Vq2 @ Vts ) ) ) ) ) ))).
% 79.18/11.97 thf(zip_derived_cl208, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vTStore, X2 : vTable]:
% 79.18/11.97 (((X0) = (vtvalue @ (sk__112 @ X0)))
% 79.18/11.97 | ~ (visSomeQuery @ (vreduce @ X0 @ X1))
% 79.18/11.97 | ((vreduce @ (vIntersection @ (vtvalue @ X2) @ X0) @ X1)
% 79.18/11.97 = (vsomeQuery @
% 79.18/11.97 (vIntersection @ (vtvalue @ X2) @
% 79.18/11.97 (vgetQuery @ (vreduce @ X0 @ X1))))))),
% 79.18/11.97 inference('cnf', [status(esa)], [reduce-10])).
% 79.18/11.97 thf(zip_derived_cl5786, plain,
% 79.18/11.97 (![X0 : vTStore, X1 : vQuery]:
% 79.18/11.97 (((vreduce @ (vIntersection @ vq1 @ X1) @ X0)
% 79.18/11.97 = (vsomeQuery @
% 79.18/11.97 (vIntersection @ (vtvalue @ sk__235) @
% 79.18/11.97 (vgetQuery @ (vreduce @ X1 @ X0)))))
% 79.18/11.97 | ~ (visSomeQuery @ (vreduce @ X1 @ X0))
% 79.18/11.97 | ((X1) = (vtvalue @ (sk__112 @ X1))))),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl397, zip_derived_cl208])).
% 79.18/11.97 thf(zip_derived_cl397, plain, (((vq1) = (vtvalue @ sk__235))),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(zip_derived_cl5787, plain,
% 79.18/11.97 (![X0 : vTStore, X1 : vQuery]:
% 79.18/11.97 (((vreduce @ (vIntersection @ vq1 @ X1) @ X0)
% 79.18/11.97 = (vsomeQuery @
% 79.18/11.97 (vIntersection @ vq1 @ (vgetQuery @ (vreduce @ X1 @ X0)))))
% 79.18/11.97 | ~ (visSomeQuery @ (vreduce @ X1 @ X0))
% 79.18/11.97 | ((X1) = (vtvalue @ (sk__112 @ X1))))),
% 79.18/11.97 inference('demod', [status(thm)], [zip_derived_cl5786, zip_derived_cl397])).
% 79.18/11.97 thf(zip_derived_cl399, plain,
% 79.18/11.97 (((vreduce @ (vIntersection @ vq1 @ vq2) @ sk__237)
% 79.18/11.97 = (vsomeQuery @ sk__234))),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(zip_derived_cl35509, plain,
% 79.18/11.97 ((((vsomeQuery @
% 79.18/11.97 (vIntersection @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))
% 79.18/11.97 = (vsomeQuery @ sk__234))
% 79.18/11.97 | ((vq2) = (vtvalue @ (sk__112 @ vq2)))
% 79.18/11.97 | ~ (visSomeQuery @ (vreduce @ vq2 @ sk__237)))),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl5787, zip_derived_cl399])).
% 79.18/11.97 thf(zip_derived_cl395, plain, ( (visSomeQuery @ (vreduce @ vq2 @ sk__237))),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(zip_derived_cl35637, plain,
% 79.18/11.97 ((((vsomeQuery @
% 79.18/11.97 (vIntersection @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))
% 79.18/11.97 = (vsomeQuery @ sk__234))
% 79.18/11.97 | ((vq2) = (vtvalue @ (sk__112 @ vq2))))),
% 79.18/11.97 inference('demod', [status(thm)],
% 79.18/11.97 [zip_derived_cl35509, zip_derived_cl395])).
% 79.18/11.97 thf(zip_derived_cl396, plain, (![X0 : vTable]: ((vq2) != (vtvalue @ X0))),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(zip_derived_cl35638, plain,
% 79.18/11.97 (((vsomeQuery @
% 79.18/11.97 (vIntersection @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))
% 79.18/11.97 = (vsomeQuery @ sk__234))),
% 79.18/11.97 inference('simplify_reflect-', [status(thm)],
% 79.18/11.97 [zip_derived_cl35637, zip_derived_cl396])).
% 79.18/11.97 thf('getQuery-0', axiom,
% 79.18/11.97 (![Vq:vQuery]: ( ( vgetQuery @ ( vsomeQuery @ Vq ) ) = ( Vq ) ))).
% 79.18/11.97 thf(zip_derived_cl47, plain,
% 79.18/11.97 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 79.18/11.97 inference('cnf', [status(esa)], [getQuery-0])).
% 79.18/11.97 thf(zip_derived_cl35641, plain,
% 79.18/11.97 (((vgetQuery @ (vsomeQuery @ sk__234))
% 79.18/11.97 = (vIntersection @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl35638, zip_derived_cl47])).
% 79.18/11.97 thf(zip_derived_cl47, plain,
% 79.18/11.97 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 79.18/11.97 inference('cnf', [status(esa)], [getQuery-0])).
% 79.18/11.97 thf(zip_derived_cl35663, plain,
% 79.18/11.97 (((sk__234)
% 79.18/11.97 = (vIntersection @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))),
% 79.18/11.97 inference('demod', [status(thm)], [zip_derived_cl35641, zip_derived_cl47])).
% 79.18/11.97 thf('isValue-false-INV', axiom,
% 79.18/11.97 (![VQuery0:vQuery]:
% 79.18/11.97 ( ( ~( visValue @ VQuery0 ) ) =>
% 79.18/11.97 ( ( ?[VwildcardName0:vSelect,VwildcardName1:vName,VwildcardName2:vPred]:
% 79.18/11.97 ( ( VQuery0 ) =
% 79.18/11.97 ( vselectFromWhere @
% 79.18/11.97 VwildcardName0 @ VwildcardName1 @ VwildcardName2 ) ) ) |
% 79.18/11.97 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 79.18/11.97 ( ( VQuery0 ) = ( vUnion @ VwildcardName0 @ VwildcardName1 ) ) ) |
% 79.18/11.97 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 79.18/11.97 ( ( VQuery0 ) = ( vIntersection @ VwildcardName0 @ VwildcardName1 ) ) ) |
% 79.18/11.97 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 79.18/11.97 ( ( VQuery0 ) = ( vDifference @ VwildcardName0 @ VwildcardName1 ) ) ) ) ))).
% 79.18/11.97 thf(zip_derived_cl166, plain,
% 79.18/11.97 (![X0 : vQuery]:
% 79.18/11.97 (((X0) = (vDifference @ (sk__82 @ X0) @ (sk__83 @ X0)))
% 79.18/11.97 | ((X0) = (vIntersection @ (sk__84 @ X0) @ (sk__85 @ X0)))
% 79.18/11.97 | ((X0) = (vUnion @ (sk__86 @ X0) @ (sk__87 @ X0)))
% 79.18/11.97 | ((X0)
% 79.18/11.97 = (vselectFromWhere @ (sk__88 @ X0) @ (sk__89 @ X0) @
% 79.18/11.97 (sk__90 @ X0)))
% 79.18/11.97 | (visValue @ X0))),
% 79.18/11.97 inference('cnf', [status(esa)], [isValue-false-INV])).
% 79.18/11.97 thf('isValue-3', axiom,
% 79.18/11.97 (![VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 79.18/11.97 ( ~( visValue @ ( vIntersection @ VwildcardName0 @ VwildcardName1 ) ) ))).
% 79.18/11.97 thf(zip_derived_cl163, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery]: ~ (visValue @ (vIntersection @ X0 @ X1))),
% 79.18/11.97 inference('cnf', [status(esa)], [isValue-3])).
% 79.18/11.97 thf(zip_derived_cl1417, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery]:
% 79.18/11.97 (((vIntersection @ X1 @ X0)
% 79.18/11.97 = (vselectFromWhere @ (sk__88 @ (vIntersection @ X1 @ X0)) @
% 79.18/11.97 (sk__89 @ (vIntersection @ X1 @ X0)) @
% 79.18/11.97 (sk__90 @ (vIntersection @ X1 @ X0))))
% 79.18/11.97 | ((vIntersection @ X1 @ X0)
% 79.18/11.97 = (vUnion @ (sk__86 @ (vIntersection @ X1 @ X0)) @
% 79.18/11.97 (sk__87 @ (vIntersection @ X1 @ X0))))
% 79.18/11.97 | ((vIntersection @ X1 @ X0)
% 79.18/11.97 = (vIntersection @ (sk__84 @ (vIntersection @ X1 @ X0)) @
% 79.18/11.97 (sk__85 @ (vIntersection @ X1 @ X0))))
% 79.18/11.97 | ((vIntersection @ X1 @ X0)
% 79.18/11.97 = (vDifference @ (sk__82 @ (vIntersection @ X1 @ X0)) @
% 79.18/11.97 (sk__83 @ (vIntersection @ X1 @ X0)))))),
% 79.18/11.97 inference('dp-resolution', [status(thm)],
% 79.18/11.97 [zip_derived_cl166, zip_derived_cl163])).
% 79.18/11.97 thf('DIFF-Intersection-Difference', axiom,
% 79.18/11.97 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 79.18/11.97 ( ( vIntersection @ VQuery0 @ VQuery1 ) !=
% 79.18/11.97 ( vDifference @ VQuery2 @ VQuery3 ) ))).
% 79.18/11.97 thf(zip_derived_cl21, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 79.18/11.97 ((vIntersection @ X2 @ X3) != (vDifference @ X0 @ X1))),
% 79.18/11.97 inference('cnf', [status(esa)], [DIFF-Intersection-Difference])).
% 79.18/11.97 thf('DIFF-Union-Intersection', axiom,
% 79.18/11.97 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 79.18/11.97 ( ( vUnion @ VQuery0 @ VQuery1 ) != ( vIntersection @ VQuery2 @ VQuery3 ) ))).
% 79.18/11.97 thf(zip_derived_cl19, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 79.18/11.97 ((vUnion @ X2 @ X3) != (vIntersection @ X0 @ X1))),
% 79.18/11.97 inference('cnf', [status(esa)], [DIFF-Union-Intersection])).
% 79.18/11.97 thf('DIFF-selectFromWhere-Intersection', axiom,
% 79.18/11.97 (![VName0:vName,VPred0:vPred,VSelect0:vSelect,VQuery1:vQuery,VQuery0:vQuery]:
% 79.18/11.97 ( ( vselectFromWhere @ VSelect0 @ VName0 @ VPred0 ) !=
% 79.18/11.97 ( vIntersection @ VQuery0 @ VQuery1 ) ))).
% 79.18/11.97 thf(zip_derived_cl17, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery, X2 : vSelect, X3 : vName, X4 : vPred]:
% 79.18/11.97 ((vselectFromWhere @ X2 @ X3 @ X4) != (vIntersection @ X0 @ X1))),
% 79.18/11.97 inference('cnf', [status(esa)], [DIFF-selectFromWhere-Intersection])).
% 79.18/11.97 thf(zip_derived_cl10572, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery]:
% 79.18/11.97 ((vIntersection @ X1 @ X0)
% 79.18/11.97 = (vIntersection @ (sk__84 @ (vIntersection @ X1 @ X0)) @
% 79.18/11.97 (sk__85 @ (vIntersection @ X1 @ X0))))),
% 79.18/11.97 inference('simplify_reflect-', [status(thm)],
% 79.18/11.97 [zip_derived_cl1417, zip_derived_cl21, zip_derived_cl19,
% 79.18/11.97 zip_derived_cl17])).
% 79.18/11.97 thf(zip_derived_cl10572, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery]:
% 79.18/11.97 ((vIntersection @ X1 @ X0)
% 79.18/11.97 = (vIntersection @ (sk__84 @ (vIntersection @ X1 @ X0)) @
% 79.18/11.97 (sk__85 @ (vIntersection @ X1 @ X0))))),
% 79.18/11.97 inference('simplify_reflect-', [status(thm)],
% 79.18/11.97 [zip_derived_cl1417, zip_derived_cl21, zip_derived_cl19,
% 79.18/11.97 zip_derived_cl17])).
% 79.18/11.97 thf('EQ-Intersection', axiom,
% 79.18/11.97 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 79.18/11.97 ( ( ( vIntersection @ VQuery0 @ VQuery1 ) =
% 79.18/11.97 ( vIntersection @ VQuery2 @ VQuery3 ) ) =>
% 79.18/11.97 ( ( ( VQuery0 ) = ( VQuery2 ) ) & ( ( VQuery1 ) = ( VQuery3 ) ) ) ))).
% 79.18/11.97 thf(zip_derived_cl8, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 79.18/11.97 (((X1) = (X0))
% 79.18/11.97 | ((vIntersection @ X1 @ X3) != (vIntersection @ X0 @ X2)))),
% 79.18/11.97 inference('cnf', [status(esa)], [EQ-Intersection])).
% 79.18/11.97 thf(zip_derived_cl10573, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 79.18/11.97 (((vIntersection @ X3 @ X2) != (vIntersection @ X1 @ X0))
% 79.18/11.97 | ((X3) = (sk__84 @ (vIntersection @ X1 @ X0))))),
% 79.18/11.97 inference('sup-', [status(thm)], [zip_derived_cl10572, zip_derived_cl8])).
% 79.18/11.97 thf(zip_derived_cl11093, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery]:
% 79.18/11.97 ((X0) = (sk__84 @ (vIntersection @ X0 @ X1)))),
% 79.18/11.97 inference('eq_res', [status(thm)], [zip_derived_cl10573])).
% 79.18/11.97 thf(zip_derived_cl11113, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery]:
% 79.18/11.97 ((vIntersection @ X1 @ X0)
% 79.18/11.97 = (vIntersection @ X1 @ (sk__85 @ (vIntersection @ X1 @ X0))))),
% 79.18/11.97 inference('demod', [status(thm)],
% 79.18/11.97 [zip_derived_cl10572, zip_derived_cl11093])).
% 79.18/11.97 thf(zip_derived_cl9, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 79.18/11.97 (((X1) = (X0))
% 79.18/11.97 | ((vIntersection @ X3 @ X1) != (vIntersection @ X2 @ X0)))),
% 79.18/11.97 inference('cnf', [status(esa)], [EQ-Intersection])).
% 79.18/11.97 thf(zip_derived_cl20527, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 79.18/11.97 (((vIntersection @ X3 @ X2) != (vIntersection @ X1 @ X0))
% 79.18/11.97 | ((X2) = (sk__85 @ (vIntersection @ X1 @ X0))))),
% 79.18/11.97 inference('sup-', [status(thm)], [zip_derived_cl11113, zip_derived_cl9])).
% 79.18/11.97 thf(zip_derived_cl20577, plain,
% 79.18/11.97 (![X0 : vQuery, X1 : vQuery]:
% 79.18/11.97 ((X0) = (sk__85 @ (vIntersection @ X1 @ X0)))),
% 79.18/11.97 inference('eq_res', [status(thm)], [zip_derived_cl20527])).
% 79.18/11.97 thf(zip_derived_cl36553, plain,
% 79.18/11.97 (((vgetQuery @ (vreduce @ vq2 @ sk__237)) = (sk__85 @ sk__234))),
% 79.18/11.97 inference('sup+', [status(thm)],
% 79.18/11.97 [zip_derived_cl35663, zip_derived_cl20577])).
% 79.18/11.97 thf('dom-OptQuery', axiom,
% 79.18/11.97 (![VX:vOptQuery]:
% 79.18/11.97 ( ( ?[VQuery0:vQuery]: ( ( VX ) = ( vsomeQuery @ VQuery0 ) ) ) |
% 79.18/11.97 ( ( VX ) = ( vnoQuery ) ) ))).
% 79.18/11.97 thf(zip_derived_cl34, plain,
% 79.18/11.97 (![X0 : vOptQuery]:
% 79.18/11.97 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 79.18/11.97 inference('cnf', [status(esa)], [dom-OptQuery])).
% 79.18/11.97 thf(zip_derived_cl47, plain,
% 79.18/11.97 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 79.18/11.97 inference('cnf', [status(esa)], [getQuery-0])).
% 79.18/11.97 thf(zip_derived_cl5025, plain,
% 79.18/11.97 (![X0 : vOptQuery]:
% 79.18/11.97 (((vgetQuery @ X0) = (sk__16 @ X0)) | ((X0) = (vnoQuery)))),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl34, zip_derived_cl47])).
% 79.18/11.97 thf(zip_derived_cl34, plain,
% 79.18/11.97 (![X0 : vOptQuery]:
% 79.18/11.97 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 79.18/11.97 inference('cnf', [status(esa)], [dom-OptQuery])).
% 79.18/11.97 thf(zip_derived_cl5053, plain,
% 79.18/11.97 (![X0 : vOptQuery]:
% 79.18/11.97 (((X0) = (vsomeQuery @ (vgetQuery @ X0)))
% 79.18/11.97 | ((X0) = (vnoQuery))
% 79.18/11.97 | ((X0) = (vnoQuery)))),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl5025, zip_derived_cl34])).
% 79.18/11.97 thf(zip_derived_cl5056, plain,
% 79.18/11.97 (![X0 : vOptQuery]:
% 79.18/11.97 (((X0) = (vnoQuery)) | ((X0) = (vsomeQuery @ (vgetQuery @ X0))))),
% 79.18/11.97 inference('simplify', [status(thm)], [zip_derived_cl5053])).
% 79.18/11.97 thf(zip_derived_cl37942, plain,
% 79.18/11.97 ((((vreduce @ vq2 @ sk__237) = (vsomeQuery @ (sk__85 @ sk__234)))
% 79.18/11.97 | ((vreduce @ vq2 @ sk__237) = (vnoQuery)))),
% 79.18/11.97 inference('sup+', [status(thm)],
% 79.18/11.97 [zip_derived_cl36553, zip_derived_cl5056])).
% 79.18/11.97 thf('isSomeQuery-true-INV', axiom,
% 79.18/11.97 (![VOptQuery0:vOptQuery]:
% 79.18/11.97 ( ( visSomeQuery @ VOptQuery0 ) =>
% 79.18/11.97 ( ?[VwildcardName0:vQuery]:
% 79.18/11.97 ( ( VOptQuery0 ) = ( vsomeQuery @ VwildcardName0 ) ) ) ))).
% 79.18/11.97 thf(zip_derived_cl169, plain,
% 79.18/11.97 (![X0 : vOptQuery]:
% 79.18/11.97 (((X0) = (vsomeQuery @ (sk__91 @ X0))) | ~ (visSomeQuery @ X0))),
% 79.18/11.97 inference('cnf', [status(esa)], [isSomeQuery-true-INV])).
% 79.18/11.97 thf('DIFF-noQuery-someQuery', axiom,
% 79.18/11.97 (![VQuery0:vQuery]: ( ( vnoQuery ) != ( vsomeQuery @ VQuery0 ) ))).
% 79.18/11.97 thf(zip_derived_cl36, plain,
% 79.18/11.97 (![X0 : vQuery]: ((vnoQuery) != (vsomeQuery @ X0))),
% 79.18/11.97 inference('cnf', [status(esa)], [DIFF-noQuery-someQuery])).
% 79.18/11.97 thf(zip_derived_cl5005, plain,
% 79.18/11.97 (![X0 : vOptQuery]: (((vnoQuery) != (X0)) | ~ (visSomeQuery @ X0))),
% 79.18/11.97 inference('sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl36])).
% 79.18/11.97 thf(zip_derived_cl395, plain, ( (visSomeQuery @ (vreduce @ vq2 @ sk__237))),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(zip_derived_cl5011, plain, (((vnoQuery) != (vreduce @ vq2 @ sk__237))),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl5005, zip_derived_cl395])).
% 79.18/11.97 thf(zip_derived_cl37951, plain,
% 79.18/11.97 (((vreduce @ vq2 @ sk__237) = (vsomeQuery @ (sk__85 @ sk__234)))),
% 79.18/11.97 inference('simplify_reflect-', [status(thm)],
% 79.18/11.97 [zip_derived_cl37942, zip_derived_cl5011])).
% 79.18/11.97 thf(zip_derived_cl38090, plain,
% 79.18/11.97 (![X0 : vQuery]:
% 79.18/11.97 (((vsomeQuery @ (sk__85 @ sk__234)) != (vsomeQuery @ X0))
% 79.18/11.97 | (vptcheck @ sk__236 @ X0 @ sk__238))),
% 79.18/11.97 inference('demod', [status(thm)],
% 79.18/11.97 [zip_derived_cl5571, zip_derived_cl37951])).
% 79.18/11.97 thf(zip_derived_cl35663, plain,
% 79.18/11.97 (((sk__234)
% 79.18/11.97 = (vIntersection @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))),
% 79.18/11.97 inference('demod', [status(thm)], [zip_derived_cl35641, zip_derived_cl47])).
% 79.18/11.97 thf(zip_derived_cl36553, plain,
% 79.18/11.97 (((vgetQuery @ (vreduce @ vq2 @ sk__237)) = (sk__85 @ sk__234))),
% 79.18/11.97 inference('sup+', [status(thm)],
% 79.18/11.97 [zip_derived_cl35663, zip_derived_cl20577])).
% 79.18/11.97 thf(zip_derived_cl37941, plain,
% 79.18/11.97 (((sk__234) = (vIntersection @ vq1 @ (sk__85 @ sk__234)))),
% 79.18/11.97 inference('demod', [status(thm)],
% 79.18/11.97 [zip_derived_cl35663, zip_derived_cl36553])).
% 79.18/11.97 thf(TIntersection, axiom,
% 79.18/11.97 (![VTTC:vTTContext,Vq1:vQuery,VTT:vTType,Vq2:vQuery]:
% 79.18/11.97 ( ( ( vptcheck @ VTTC @ Vq1 @ VTT ) & ( vptcheck @ VTTC @ Vq2 @ VTT ) ) =>
% 79.18/11.97 ( vptcheck @ VTTC @ ( vIntersection @ Vq1 @ Vq2 ) @ VTT ) ))).
% 79.18/11.97 thf(zip_derived_cl379, plain,
% 79.18/11.97 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 79.18/11.97 (~ (vptcheck @ X0 @ X1 @ X2)
% 79.18/11.97 | ~ (vptcheck @ X0 @ X3 @ X2)
% 79.18/11.97 | (vptcheck @ X0 @ (vIntersection @ X1 @ X3) @ X2))),
% 79.18/11.97 inference('cnf', [status(esa)], [TIntersection])).
% 79.18/11.97 thf(zip_derived_cl38029, plain,
% 79.18/11.97 (![X0 : vTType, X1 : vTTContext]:
% 79.18/11.97 ( (vptcheck @ X1 @ sk__234 @ X0)
% 79.18/11.97 | ~ (vptcheck @ X1 @ (sk__85 @ sk__234) @ X0)
% 79.18/11.97 | ~ (vptcheck @ X1 @ vq1 @ X0))),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl37941, zip_derived_cl379])).
% 79.18/11.97 thf(zip_derived_cl56212, plain,
% 79.18/11.97 ((((vsomeQuery @ (sk__85 @ sk__234)) != (vsomeQuery @ (sk__85 @ sk__234)))
% 79.18/11.97 | ~ (vptcheck @ sk__236 @ vq1 @ sk__238)
% 79.18/11.97 | (vptcheck @ sk__236 @ sk__234 @ sk__238))),
% 79.18/11.97 inference('sup-', [status(thm)],
% 79.18/11.97 [zip_derived_cl38090, zip_derived_cl38029])).
% 79.18/11.97 thf(TIntersection_inv1, axiom,
% 79.18/11.97 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 79.18/11.97 ( ( vptcheck @ VTTC @ ( vIntersection @ Vq1 @ Vq2 ) @ VTT ) =>
% 79.18/11.97 ( vptcheck @ VTTC @ Vq1 @ VTT ) ))).
% 79.18/11.97 thf(zip_derived_cl387, plain,
% 79.18/11.97 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 79.18/11.97 ( (vptcheck @ X0 @ X1 @ X2)
% 79.18/11.97 | ~ (vptcheck @ X0 @ (vIntersection @ X1 @ X3) @ X2))),
% 79.18/11.97 inference('cnf', [status(esa)], [TIntersection_inv1])).
% 79.18/11.97 thf(zip_derived_cl394, plain,
% 79.18/11.97 ( (vptcheck @ sk__236 @ (vIntersection @ vq1 @ vq2) @ sk__238)),
% 79.18/11.97 inference('cnf', [status(esa)], [zf_stmt_0])).
% 79.18/11.97 thf(zip_derived_cl5313, plain, ( (vptcheck @ sk__236 @ vq1 @ sk__238)),
% 79.18/11.97 inference('sup+', [status(thm)], [zip_derived_cl387, zip_derived_cl394])).
% 79.18/11.97 thf(zip_derived_cl56213, plain,
% 79.18/11.97 ((((vsomeQuery @ (sk__85 @ sk__234)) != (vsomeQuery @ (sk__85 @ sk__234)))
% 79.18/11.97 | (vptcheck @ sk__236 @ sk__234 @ sk__238))),
% 79.18/11.97 inference('demod', [status(thm)],
% 79.18/11.97 [zip_derived_cl56212, zip_derived_cl5313])).
% 79.18/11.97 thf(zip_derived_cl56214, plain, ( (vptcheck @ sk__236 @ sk__234 @ sk__238)),
% 79.18/11.97 inference('simplify', [status(thm)], [zip_derived_cl56213])).
% 79.18/11.97 thf(zip_derived_cl56217, plain, ($false),
% 79.18/11.97 inference('demod', [status(thm)],
% 79.18/11.97 [zip_derived_cl393, zip_derived_cl56214])).
% 79.18/11.97
% 79.18/11.97 % SZS output end Refutation
% 79.18/11.97
% 79.18/11.97
% 79.18/11.97 % Terminating...
% 80.09/12.08 % Runner terminated.
% 80.09/12.09 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------