%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM294_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.bosbWKF0I8 true
% Computer : n019.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 12.91s 2.46s
% Output : Refutation 12.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM294_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.bosbWKF0I8 true
% 0.15/0.33 % Computer : n019.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 20:28:29 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 % Running portfolio for 300 s
% 0.15/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Number of cores: 8
% 0.15/0.34 % Python version: Python 3.6.8
% 0.15/0.34 % Running in FO mode
% 0.44/0.62 % Total configuration time : 435
% 0.44/0.62 % Estimated wc time : 1092
% 0.44/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.52/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.53/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.53/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.53/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.53/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.53/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.53/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 12.91/2.46 % Solved by fo/fo3_bce.sh.
% 12.91/2.46 % BCE start: 416
% 12.91/2.46 % BCE eliminated: 0
% 12.91/2.46 % PE start: 416
% 12.91/2.46 logic: eq
% 12.91/2.46 % PE eliminated: -50
% 12.91/2.46 % done 835 iterations in 1.741s
% 12.91/2.46 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 12.91/2.46 % SZS output start Refutation
% 12.91/2.46 thf(vOptQuery_type, type, vOptQuery: $tType).
% 12.91/2.46 thf(vQuery_type, type, vQuery: $tType).
% 12.91/2.46 thf(vTStore_type, type, vTStore: $tType).
% 12.91/2.46 thf(vTable_type, type, vTable: $tType).
% 12.91/2.46 thf(vTTContext_type, type, vTTContext: $tType).
% 12.91/2.46 thf(vTType_type, type, vTType: $tType).
% 12.91/2.46 thf(vtvalue_type, type, vtvalue: vTable > vQuery).
% 12.91/2.46 thf(sk__245_type, type, sk__245: vTType).
% 12.91/2.46 thf(sk__114_type, type, sk__114: vQuery > vQuery > vTable).
% 12.91/2.46 thf(vq2_type, type, vq2: vQuery).
% 12.91/2.46 thf(vptcheck_type, type, vptcheck: vTTContext > vQuery > vTType > $o).
% 12.91/2.46 thf(sk__112_type, type, sk__112: vQuery > vQuery > vTable).
% 12.91/2.46 thf(visSomeQuery_type, type, visSomeQuery: vOptQuery > $o).
% 12.91/2.46 thf(zip_tseitin_23_type, type, zip_tseitin_23: vTable > vTable > vQuery >
% 12.91/2.46 vQuery > $o).
% 12.91/2.46 thf(sk__246_type, type, sk__246: vQuery).
% 12.91/2.46 thf(vreduce_type, type, vreduce: vQuery > vTStore > vOptQuery).
% 12.91/2.46 thf(vq1_type, type, vq1: vQuery).
% 12.91/2.46 thf(sk__244_type, type, sk__244: vTTContext).
% 12.91/2.46 thf(vUnion_type, type, vUnion: vQuery > vQuery > vQuery).
% 12.91/2.46 thf(sk__113_type, type, sk__113: vQuery > vQuery > vQuery).
% 12.91/2.46 thf(vgetQuery_type, type, vgetQuery: vOptQuery > vQuery).
% 12.91/2.46 thf(sk__100_type, type, sk__100: vOptQuery > vQuery).
% 12.91/2.46 thf(zip_tseitin_22_type, type, zip_tseitin_22: vQuery > vTable > vQuery >
% 12.91/2.46 vQuery > $o).
% 12.91/2.46 thf(sk__115_type, type, sk__115: vQuery > vQuery > vTable).
% 12.91/2.46 thf(vstoreContextConsistent_type, type, vstoreContextConsistent: vTStore >
% 12.91/2.46 vTTContext > $o).
% 12.91/2.46 thf(vsomeQuery_type, type, vsomeQuery: vQuery > vOptQuery).
% 12.91/2.46 thf(sk__243_type, type, sk__243: vTStore).
% 12.91/2.46 thf('isSomeQuery-true-INV', axiom,
% 12.91/2.46 (![VOptQuery0:vOptQuery]:
% 12.91/2.46 ( ( visSomeQuery @ VOptQuery0 ) =>
% 12.91/2.46 ( ?[VwildcardName0:vQuery]:
% 12.91/2.46 ( ( VOptQuery0 ) = ( vsomeQuery @ VwildcardName0 ) ) ) ))).
% 12.91/2.46 thf(zip_derived_cl186, plain,
% 12.91/2.46 (![X0 : vOptQuery]:
% 12.91/2.46 (((X0) = (vsomeQuery @ (sk__100 @ X0))) | ~ (visSomeQuery @ X0))),
% 12.91/2.46 inference('cnf', [status(esa)], [isSomeQuery-true-INV])).
% 12.91/2.46 thf('getQuery-0', axiom,
% 12.91/2.46 (![Vq:vQuery]: ( ( vgetQuery @ ( vsomeQuery @ Vq ) ) = ( Vq ) ))).
% 12.91/2.46 thf(zip_derived_cl47, plain,
% 12.91/2.46 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 12.91/2.46 inference('cnf', [status(esa)], [getQuery-0])).
% 12.91/2.46 thf(zip_derived_cl5226, plain,
% 12.91/2.46 (![X0 : vOptQuery]:
% 12.91/2.46 (((vgetQuery @ X0) = (sk__100 @ X0)) | ~ (visSomeQuery @ X0))),
% 12.91/2.46 inference('sup+', [status(thm)], [zip_derived_cl186, zip_derived_cl47])).
% 12.91/2.46 thf(zip_derived_cl186, plain,
% 12.91/2.46 (![X0 : vOptQuery]:
% 12.91/2.46 (((X0) = (vsomeQuery @ (sk__100 @ X0))) | ~ (visSomeQuery @ X0))),
% 12.91/2.46 inference('cnf', [status(esa)], [isSomeQuery-true-INV])).
% 12.91/2.46 thf(zip_derived_cl5290, plain,
% 12.91/2.46 (![X0 : vOptQuery]:
% 12.91/2.46 (((X0) = (vsomeQuery @ (vgetQuery @ X0)))
% 12.91/2.46 | ~ (visSomeQuery @ X0)
% 12.91/2.46 | ~ (visSomeQuery @ X0))),
% 12.91/2.46 inference('sup+', [status(thm)], [zip_derived_cl5226, zip_derived_cl186])).
% 12.91/2.46 thf(zip_derived_cl5293, plain,
% 12.91/2.46 (![X0 : vOptQuery]:
% 12.91/2.46 (~ (visSomeQuery @ X0) | ((X0) = (vsomeQuery @ (vgetQuery @ X0))))),
% 12.91/2.46 inference('simplify', [status(thm)], [zip_derived_cl5290])).
% 12.91/2.46 thf('Preservation-Union-q1-isSomeQuery-True', conjecture,
% 12.91/2.46 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 12.91/2.46 ( ( ( visSomeQuery @ ( vreduce @ vq1 @ Vts ) ) &
% 12.91/2.46 ( ![Vt00:vTable]: ( ( vq1 ) != ( vtvalue @ Vt00 ) ) ) &
% 12.91/2.46 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 12.91/2.46 ( vptcheck @ Vttc @ ( vUnion @ vq1 @ vq2 ) @ Vtt ) &
% 12.91/2.46 ( ( vreduce @ ( vUnion @ vq1 @ vq2 ) @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 12.91/2.46 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 12.91/2.46 thf(zf_stmt_0, negated_conjecture,
% 12.91/2.46 (~( ![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 12.91/2.46 ( ( ( visSomeQuery @ ( vreduce @ vq1 @ Vts ) ) &
% 12.91/2.46 ( ![Vt00:vTable]: ( ( vq1 ) != ( vtvalue @ Vt00 ) ) ) &
% 12.91/2.46 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 12.91/2.46 ( vptcheck @ Vttc @ ( vUnion @ vq1 @ vq2 ) @ Vtt ) &
% 12.91/2.46 ( ( vreduce @ ( vUnion @ vq1 @ vq2 ) @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 12.91/2.46 ( vptcheck @ Vttc @ Vqr @ Vtt ) ) )),
% 12.91/2.46 inference('cnf.neg', [status(esa)],
% 12.91/2.46 [Preservation-Union-q1-isSomeQuery-True])).
% 12.91/2.46 thf(zip_derived_cl414, plain,
% 12.91/2.46 ( (vstoreContextConsistent @ sk__243 @ sk__244)),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf(TUnion_inv1, axiom,
% 12.91/2.46 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 12.91/2.46 ( ( vptcheck @ VTTC @ ( vUnion @ Vq1 @ Vq2 ) @ VTT ) =>
% 12.91/2.46 ( vptcheck @ VTTC @ Vq1 @ VTT ) ))).
% 12.91/2.46 thf(zip_derived_cl402, plain,
% 12.91/2.46 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 12.91/2.46 ( (vptcheck @ X0 @ X1 @ X2)
% 12.91/2.46 | ~ (vptcheck @ X0 @ (vUnion @ X1 @ X3) @ X2))),
% 12.91/2.46 inference('cnf', [status(esa)], [TUnion_inv1])).
% 12.91/2.46 thf(zip_derived_cl415, plain,
% 12.91/2.46 ( (vptcheck @ sk__244 @ (vUnion @ vq1 @ vq2) @ sk__245)),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf(zip_derived_cl5490, plain, ( (vptcheck @ sk__244 @ vq1 @ sk__245)),
% 12.91/2.46 inference('sup+', [status(thm)], [zip_derived_cl402, zip_derived_cl415])).
% 12.91/2.46 thf('Preservation-Union-IH0', axiom,
% 12.91/2.46 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 12.91/2.46 ( ( ( vstoreContextConsistent @ Vts @ Vttc ) &
% 12.91/2.46 ( vptcheck @ Vttc @ vq1 @ Vtt ) &
% 12.91/2.46 ( ( vreduce @ vq1 @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 12.91/2.46 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 12.91/2.46 thf(zip_derived_cl408, plain,
% 12.91/2.46 (![X0 : vTTContext, X1 : vTType, X2 : vTStore, X3 : vQuery]:
% 12.91/2.46 (~ (vptcheck @ X0 @ vq1 @ X1)
% 12.91/2.46 | ~ (vstoreContextConsistent @ X2 @ X0)
% 12.91/2.46 | ((vreduce @ vq1 @ X2) != (vsomeQuery @ X3))
% 12.91/2.46 | (vptcheck @ X0 @ X3 @ X1))),
% 12.91/2.46 inference('cnf', [status(esa)], [Preservation-Union-IH0])).
% 12.91/2.46 thf(zip_derived_cl5755, plain,
% 12.91/2.46 (![X0 : vQuery, X1 : vTStore]:
% 12.91/2.46 ( (vptcheck @ sk__244 @ X0 @ sk__245)
% 12.91/2.46 | ((vreduce @ vq1 @ X1) != (vsomeQuery @ X0))
% 12.91/2.46 | ~ (vstoreContextConsistent @ X1 @ sk__244))),
% 12.91/2.46 inference('sup-', [status(thm)], [zip_derived_cl5490, zip_derived_cl408])).
% 12.91/2.46 thf(zip_derived_cl5757, plain,
% 12.91/2.46 (![X0 : vQuery]:
% 12.91/2.46 (((vreduce @ vq1 @ sk__243) != (vsomeQuery @ X0))
% 12.91/2.46 | (vptcheck @ sk__244 @ X0 @ sk__245))),
% 12.91/2.46 inference('sup-', [status(thm)], [zip_derived_cl414, zip_derived_cl5755])).
% 12.91/2.46 thf(zip_derived_cl412, plain, ( (visSomeQuery @ (vreduce @ vq1 @ sk__243))),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf('reduce-7', axiom,
% 12.91/2.46 (![Vq1:vQuery,Vq2:vQuery,Vts:vTStore]:
% 12.91/2.46 ( ( ( visSomeQuery @ ( vreduce @ Vq1 @ Vts ) ) &
% 12.91/2.46 ( ![Vt00:vTable,Vq200:vQuery]:
% 12.91/2.46 ( ( ( Vq1 ) != ( vtvalue @ Vt00 ) ) | ( ( Vq2 ) != ( Vq200 ) ) ) ) &
% 12.91/2.46 ( ![Vt100:vTable,Vt200:vTable]:
% 12.91/2.46 ( ( ( Vq1 ) != ( vtvalue @ Vt100 ) ) |
% 12.91/2.46 ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) ) ) ) =>
% 12.91/2.46 ( ( vreduce @ ( vUnion @ Vq1 @ Vq2 ) @ Vts ) =
% 12.91/2.46 ( vsomeQuery @
% 12.91/2.46 ( vUnion @ ( vgetQuery @ ( vreduce @ Vq1 @ Vts ) ) @ Vq2 ) ) ) ))).
% 12.91/2.46 thf(zf_stmt_1, axiom,
% 12.91/2.46 (![Vt200:vTable,Vt100:vTable,Vq2:vQuery,Vq1:vQuery]:
% 12.91/2.46 ( ( ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) |
% 12.91/2.46 ( ( Vq1 ) != ( vtvalue @ Vt100 ) ) ) =>
% 12.91/2.46 ( zip_tseitin_23 @ Vt200 @ Vt100 @ Vq2 @ Vq1 ) ))).
% 12.91/2.46 thf(zip_derived_cl216, plain,
% 12.91/2.46 (![X0 : vTable, X1 : vTable, X2 : vQuery, X3 : vQuery]:
% 12.91/2.46 ( (zip_tseitin_23 @ X0 @ X1 @ X2 @ X3) | ((X3) = (vtvalue @ X1)))),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_1])).
% 12.91/2.46 thf(zf_stmt_2, axiom,
% 12.91/2.46 (![Vq200:vQuery,Vt00:vTable,Vq2:vQuery,Vq1:vQuery]:
% 12.91/2.46 ( ( ( ( Vq2 ) != ( Vq200 ) ) | ( ( Vq1 ) != ( vtvalue @ Vt00 ) ) ) =>
% 12.91/2.46 ( zip_tseitin_22 @ Vq200 @ Vt00 @ Vq2 @ Vq1 ) ))).
% 12.91/2.46 thf(zip_derived_cl214, plain,
% 12.91/2.46 (![X0 : vQuery, X1 : vTable, X2 : vQuery, X3 : vQuery]:
% 12.91/2.46 ( (zip_tseitin_22 @ X0 @ X1 @ X2 @ X3) | ((X3) = (vtvalue @ X1)))),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_2])).
% 12.91/2.46 thf(zf_stmt_3, type, zip_tseitin_23 : vTable > vTable > vQuery > vQuery > $o).
% 12.91/2.46 thf(zf_stmt_4, type, zip_tseitin_22 : vQuery > vTable > vQuery > vQuery > $o).
% 12.91/2.46 thf(zf_stmt_5, axiom,
% 12.91/2.46 (![Vq1:vQuery,Vq2:vQuery,Vts:vTStore]:
% 12.91/2.46 ( ( ( ![Vt100:vTable,Vt200:vTable]:
% 12.91/2.46 ( zip_tseitin_23 @ Vt200 @ Vt100 @ Vq2 @ Vq1 ) ) &
% 12.91/2.46 ( ![Vt00:vTable,Vq200:vQuery]:
% 12.91/2.46 ( zip_tseitin_22 @ Vq200 @ Vt00 @ Vq2 @ Vq1 ) ) &
% 12.91/2.46 ( visSomeQuery @ ( vreduce @ Vq1 @ Vts ) ) ) =>
% 12.91/2.46 ( ( vreduce @ ( vUnion @ Vq1 @ Vq2 ) @ Vts ) =
% 12.91/2.46 ( vsomeQuery @
% 12.91/2.46 ( vUnion @ ( vgetQuery @ ( vreduce @ Vq1 @ Vts ) ) @ Vq2 ) ) ) ))).
% 12.91/2.46 thf(zip_derived_cl217, plain,
% 12.91/2.46 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 12.91/2.46 (~ (zip_tseitin_22 @ (sk__113 @ X0 @ X1) @ (sk__112 @ X0 @ X1) @ X0 @
% 12.91/2.46 X1)
% 12.91/2.46 | ~ (zip_tseitin_23 @ (sk__115 @ X0 @ X1) @ (sk__114 @ X0 @ X1) @
% 12.91/2.46 X0 @ X1)
% 12.91/2.46 | ~ (visSomeQuery @ (vreduce @ X1 @ X2))
% 12.91/2.46 | ((vreduce @ (vUnion @ X1 @ X0) @ X2)
% 12.91/2.46 = (vsomeQuery @ (vUnion @ (vgetQuery @ (vreduce @ X1 @ X2)) @ X0))))),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_5])).
% 12.91/2.46 thf(zip_derived_cl1363, plain,
% 12.91/2.46 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 12.91/2.46 (((X0) = (vtvalue @ (sk__112 @ X1 @ X0)))
% 12.91/2.46 | ((vreduce @ (vUnion @ X0 @ X1) @ X2)
% 12.91/2.46 = (vsomeQuery @ (vUnion @ (vgetQuery @ (vreduce @ X0 @ X2)) @ X1)))
% 12.91/2.46 | ~ (visSomeQuery @ (vreduce @ X0 @ X2))
% 12.91/2.46 | ~ (zip_tseitin_23 @ (sk__115 @ X1 @ X0) @ (sk__114 @ X1 @ X0) @
% 12.91/2.46 X1 @ X0))),
% 12.91/2.46 inference('dp-resolution', [status(thm)],
% 12.91/2.46 [zip_derived_cl214, zip_derived_cl217])).
% 12.91/2.46 thf(zip_derived_cl1414, plain,
% 12.91/2.46 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 12.91/2.46 (((X0) = (vtvalue @ (sk__114 @ X1 @ X0)))
% 12.91/2.46 | ~ (visSomeQuery @ (vreduce @ X0 @ X2))
% 12.91/2.46 | ((vreduce @ (vUnion @ X0 @ X1) @ X2)
% 12.91/2.46 = (vsomeQuery @ (vUnion @ (vgetQuery @ (vreduce @ X0 @ X2)) @ X1)))
% 12.91/2.46 | ((X0) = (vtvalue @ (sk__112 @ X1 @ X0))))),
% 12.91/2.46 inference('dp-resolution', [status(thm)],
% 12.91/2.46 [zip_derived_cl216, zip_derived_cl1363])).
% 12.91/2.46 thf(zip_derived_cl6884, plain,
% 12.91/2.46 (![X0 : vQuery]:
% 12.91/2.46 (((vq1) = (vtvalue @ (sk__112 @ X0 @ vq1)))
% 12.91/2.46 | ((vreduce @ (vUnion @ vq1 @ X0) @ sk__243)
% 12.91/2.46 = (vsomeQuery @
% 12.91/2.46 (vUnion @ (vgetQuery @ (vreduce @ vq1 @ sk__243)) @ X0)))
% 12.91/2.46 | ((vq1) = (vtvalue @ (sk__114 @ X0 @ vq1))))),
% 12.91/2.46 inference('sup-', [status(thm)], [zip_derived_cl412, zip_derived_cl1414])).
% 12.91/2.46 thf(zip_derived_cl413, plain, (![X0 : vTable]: ((vq1) != (vtvalue @ X0))),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf(zip_derived_cl413, plain, (![X0 : vTable]: ((vq1) != (vtvalue @ X0))),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf(zip_derived_cl6909, plain,
% 12.91/2.46 (![X0 : vQuery]:
% 12.91/2.46 ((vreduce @ (vUnion @ vq1 @ X0) @ sk__243)
% 12.91/2.46 = (vsomeQuery @
% 12.91/2.46 (vUnion @ (vgetQuery @ (vreduce @ vq1 @ sk__243)) @ X0)))),
% 12.91/2.46 inference('simplify_reflect-', [status(thm)],
% 12.91/2.46 [zip_derived_cl6884, zip_derived_cl413, zip_derived_cl413])).
% 12.91/2.46 thf(zip_derived_cl411, plain,
% 12.91/2.46 (((vreduce @ (vUnion @ vq1 @ vq2) @ sk__243) = (vsomeQuery @ sk__246))),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf(zip_derived_cl6977, plain,
% 12.91/2.46 (((vsomeQuery @ (vUnion @ (vgetQuery @ (vreduce @ vq1 @ sk__243)) @ vq2))
% 12.91/2.46 = (vsomeQuery @ sk__246))),
% 12.91/2.46 inference('sup+', [status(thm)], [zip_derived_cl6909, zip_derived_cl411])).
% 12.91/2.46 thf(zip_derived_cl47, plain,
% 12.91/2.46 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 12.91/2.46 inference('cnf', [status(esa)], [getQuery-0])).
% 12.91/2.46 thf(zip_derived_cl6990, plain,
% 12.91/2.46 (((vgetQuery @ (vsomeQuery @ sk__246))
% 12.91/2.46 = (vUnion @ (vgetQuery @ (vreduce @ vq1 @ sk__243)) @ vq2))),
% 12.91/2.46 inference('sup+', [status(thm)], [zip_derived_cl6977, zip_derived_cl47])).
% 12.91/2.46 thf(zip_derived_cl47, plain,
% 12.91/2.46 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 12.91/2.46 inference('cnf', [status(esa)], [getQuery-0])).
% 12.91/2.46 thf(zip_derived_cl7002, plain,
% 12.91/2.46 (((sk__246) = (vUnion @ (vgetQuery @ (vreduce @ vq1 @ sk__243)) @ vq2))),
% 12.91/2.46 inference('demod', [status(thm)], [zip_derived_cl6990, zip_derived_cl47])).
% 12.91/2.46 thf(TUnion, axiom,
% 12.91/2.46 (![VTTC:vTTContext,Vq1:vQuery,VTT:vTType,Vq2:vQuery]:
% 12.91/2.46 ( ( ( vptcheck @ VTTC @ Vq1 @ VTT ) & ( vptcheck @ VTTC @ Vq2 @ VTT ) ) =>
% 12.91/2.46 ( vptcheck @ VTTC @ ( vUnion @ Vq1 @ Vq2 ) @ VTT ) ))).
% 12.91/2.46 thf(zip_derived_cl395, plain,
% 12.91/2.46 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 12.91/2.46 (~ (vptcheck @ X0 @ X1 @ X2)
% 12.91/2.46 | ~ (vptcheck @ X0 @ X3 @ X2)
% 12.91/2.46 | (vptcheck @ X0 @ (vUnion @ X1 @ X3) @ X2))),
% 12.91/2.46 inference('cnf', [status(esa)], [TUnion])).
% 12.91/2.46 thf(zip_derived_cl7020, plain,
% 12.91/2.46 (![X0 : vTType, X1 : vTTContext]:
% 12.91/2.46 ( (vptcheck @ X1 @ sk__246 @ X0)
% 12.91/2.46 | ~ (vptcheck @ X1 @ vq2 @ X0)
% 12.91/2.46 | ~ (vptcheck @ X1 @ (vgetQuery @ (vreduce @ vq1 @ sk__243)) @ X0))),
% 12.91/2.46 inference('sup+', [status(thm)], [zip_derived_cl7002, zip_derived_cl395])).
% 12.91/2.46 thf(zip_derived_cl7684, plain,
% 12.91/2.46 ((((vreduce @ vq1 @ sk__243)
% 12.91/2.46 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__243))))
% 12.91/2.46 | ~ (vptcheck @ sk__244 @ vq2 @ sk__245)
% 12.91/2.46 | (vptcheck @ sk__244 @ sk__246 @ sk__245))),
% 12.91/2.46 inference('sup-', [status(thm)], [zip_derived_cl5757, zip_derived_cl7020])).
% 12.91/2.46 thf(TUnion_inv2, axiom,
% 12.91/2.46 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 12.91/2.46 ( ( vptcheck @ VTTC @ ( vUnion @ Vq1 @ Vq2 ) @ VTT ) =>
% 12.91/2.46 ( vptcheck @ VTTC @ Vq2 @ VTT ) ))).
% 12.91/2.46 thf(zip_derived_cl403, plain,
% 12.91/2.46 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 12.91/2.46 ( (vptcheck @ X0 @ X1 @ X2)
% 12.91/2.46 | ~ (vptcheck @ X0 @ (vUnion @ X3 @ X1) @ X2))),
% 12.91/2.46 inference('cnf', [status(esa)], [TUnion_inv2])).
% 12.91/2.46 thf(zip_derived_cl415, plain,
% 12.91/2.46 ( (vptcheck @ sk__244 @ (vUnion @ vq1 @ vq2) @ sk__245)),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf(zip_derived_cl5494, plain, ( (vptcheck @ sk__244 @ vq2 @ sk__245)),
% 12.91/2.46 inference('sup+', [status(thm)], [zip_derived_cl403, zip_derived_cl415])).
% 12.91/2.46 thf(zip_derived_cl7686, plain,
% 12.91/2.46 ((((vreduce @ vq1 @ sk__243)
% 12.91/2.46 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__243))))
% 12.91/2.46 | (vptcheck @ sk__244 @ sk__246 @ sk__245))),
% 12.91/2.46 inference('demod', [status(thm)],
% 12.91/2.46 [zip_derived_cl7684, zip_derived_cl5494])).
% 12.91/2.46 thf(zip_derived_cl410, plain, (~ (vptcheck @ sk__244 @ sk__246 @ sk__245)),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf(zip_derived_cl7692, plain,
% 12.91/2.46 (((vreduce @ vq1 @ sk__243)
% 12.91/2.46 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__243))))),
% 12.91/2.46 inference('clc', [status(thm)], [zip_derived_cl7686, zip_derived_cl410])).
% 12.91/2.46 thf(zip_derived_cl7693, plain,
% 12.91/2.46 ((((vreduce @ vq1 @ sk__243) != (vreduce @ vq1 @ sk__243))
% 12.91/2.46 | ~ (visSomeQuery @ (vreduce @ vq1 @ sk__243)))),
% 12.91/2.46 inference('sup-', [status(thm)], [zip_derived_cl5293, zip_derived_cl7692])).
% 12.91/2.46 thf(zip_derived_cl412, plain, ( (visSomeQuery @ (vreduce @ vq1 @ sk__243))),
% 12.91/2.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 12.91/2.46 thf(zip_derived_cl7695, plain,
% 12.91/2.46 (((vreduce @ vq1 @ sk__243) != (vreduce @ vq1 @ sk__243))),
% 12.91/2.46 inference('demod', [status(thm)], [zip_derived_cl7693, zip_derived_cl412])).
% 12.91/2.46 thf(zip_derived_cl7696, plain, ($false),
% 12.91/2.46 inference('simplify', [status(thm)], [zip_derived_cl7695])).
% 12.91/2.46
% 12.91/2.46 % SZS output end Refutation
% 12.91/2.46
% 12.91/2.46
% 12.91/2.46 % Terminating...
% 13.59/2.57 % Runner terminated.
% 13.59/2.57 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------