%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM289_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.dv36E0pW0S true
% Computer : n020.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 14.70s 2.71s
% Output : Refutation 14.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : COM289_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.dv36E0pW0S true
% 0.18/0.35 % Computer : n020.cluster.edu
% 0.18/0.35 % Model : x86_64 x86_64
% 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.35 % Memory : 8042.1875MB
% 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35 % CPULimit : 300
% 0.18/0.35 % WCLimit : 300
% 0.18/0.35 % DateTime : Mon May 4 20:22:49 EDT 2026
% 0.18/0.35 % CPUTime :
% 0.18/0.35 % Running portfolio for 300 s
% 0.18/0.35 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.35 % Number of cores: 8
% 0.21/0.36 % Python version: Python 3.6.8
% 0.21/0.36 % Running in FO mode
% 0.55/0.66 % Total configuration time : 435
% 0.55/0.66 % Estimated wc time : 1092
% 0.55/0.66 % Estimated cpu time (7 cpus) : 156.0
% 0.57/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.57/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 14.70/2.71 % Solved by fo/fo3_bce.sh.
% 14.70/2.71 % BCE start: 399
% 14.70/2.71 % BCE eliminated: 0
% 14.70/2.71 % PE start: 399
% 14.70/2.71 logic: eq
% 14.70/2.71 % PE eliminated: -44
% 14.70/2.71 % done 967 iterations in 1.931s
% 14.70/2.71 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 14.70/2.71 % SZS output start Refutation
% 14.70/2.71 thf(vOptQuery_type, type, vOptQuery: $tType).
% 14.70/2.71 thf(vQuery_type, type, vQuery: $tType).
% 14.70/2.71 thf(vTStore_type, type, vTStore: $tType).
% 14.70/2.71 thf(vTable_type, type, vTable: $tType).
% 14.70/2.71 thf(vTTContext_type, type, vTTContext: $tType).
% 14.70/2.71 thf(vTType_type, type, vTType: $tType).
% 14.70/2.71 thf(vtvalue_type, type, vtvalue: vTable > vQuery).
% 14.70/2.71 thf(sk__236_type, type, sk__236: vTType).
% 14.70/2.71 thf(vq2_type, type, vq2: vQuery).
% 14.70/2.71 thf(vptcheck_type, type, vptcheck: vTTContext > vQuery > vTType > $o).
% 14.70/2.71 thf(vnoQuery_type, type, vnoQuery: vOptQuery).
% 14.70/2.71 thf(sk__117_type, type, sk__117: vQuery > vQuery > vTable).
% 14.70/2.71 thf(visSomeQuery_type, type, visSomeQuery: vOptQuery > $o).
% 14.70/2.71 thf(sk__91_type, type, sk__91: vOptQuery > vQuery).
% 14.70/2.71 thf(zip_tseitin_23_type, type, zip_tseitin_23: vQuery > vTable > vQuery >
% 14.70/2.71 vQuery > $o).
% 14.70/2.71 thf(vreduce_type, type, vreduce: vQuery > vTStore > vOptQuery).
% 14.70/2.71 thf(vq1_type, type, vq1: vQuery).
% 14.70/2.71 thf(sk__116_type, type, sk__116: vQuery > vQuery > vQuery).
% 14.70/2.71 thf(zip_tseitin_24_type, type, zip_tseitin_24: vTable > vTable > vQuery >
% 14.70/2.71 vQuery > $o).
% 14.70/2.71 thf(sk__118_type, type, sk__118: vQuery > vQuery > vTable).
% 14.70/2.71 thf(vgetQuery_type, type, vgetQuery: vOptQuery > vQuery).
% 14.70/2.71 thf(vIntersection_type, type, vIntersection: vQuery > vQuery > vQuery).
% 14.70/2.71 thf(sk__237_type, type, sk__237: vQuery).
% 14.70/2.71 thf(sk__235_type, type, sk__235: vTTContext).
% 14.70/2.71 thf(sk__16_type, type, sk__16: vOptQuery > vQuery).
% 14.70/2.71 thf(vstoreContextConsistent_type, type, vstoreContextConsistent: vTStore >
% 14.70/2.71 vTTContext > $o).
% 14.70/2.71 thf(vsomeQuery_type, type, vsomeQuery: vQuery > vOptQuery).
% 14.70/2.71 thf(sk__115_type, type, sk__115: vQuery > vQuery > vTable).
% 14.70/2.71 thf(sk__234_type, type, sk__234: vTStore).
% 14.70/2.71 thf('dom-OptQuery', axiom,
% 14.70/2.71 (![VX:vOptQuery]:
% 14.70/2.71 ( ( ?[VQuery0:vQuery]: ( ( VX ) = ( vsomeQuery @ VQuery0 ) ) ) |
% 14.70/2.71 ( ( VX ) = ( vnoQuery ) ) ))).
% 14.70/2.71 thf(zip_derived_cl34, plain,
% 14.70/2.71 (![X0 : vOptQuery]:
% 14.70/2.71 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 14.70/2.71 inference('cnf', [status(esa)], [dom-OptQuery])).
% 14.70/2.71 thf('getQuery-0', axiom,
% 14.70/2.71 (![Vq:vQuery]: ( ( vgetQuery @ ( vsomeQuery @ Vq ) ) = ( Vq ) ))).
% 14.70/2.71 thf(zip_derived_cl47, plain,
% 14.70/2.71 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 14.70/2.71 inference('cnf', [status(esa)], [getQuery-0])).
% 14.70/2.71 thf(zip_derived_cl4998, plain,
% 14.70/2.71 (![X0 : vOptQuery]:
% 14.70/2.71 (((vgetQuery @ X0) = (sk__16 @ X0)) | ((X0) = (vnoQuery)))),
% 14.70/2.71 inference('sup+', [status(thm)], [zip_derived_cl34, zip_derived_cl47])).
% 14.70/2.71 thf(zip_derived_cl34, plain,
% 14.70/2.71 (![X0 : vOptQuery]:
% 14.70/2.71 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 14.70/2.71 inference('cnf', [status(esa)], [dom-OptQuery])).
% 14.70/2.71 thf(zip_derived_cl5023, plain,
% 14.70/2.71 (![X0 : vOptQuery]:
% 14.70/2.71 (((X0) = (vsomeQuery @ (vgetQuery @ X0)))
% 14.70/2.71 | ((X0) = (vnoQuery))
% 14.70/2.71 | ((X0) = (vnoQuery)))),
% 14.70/2.71 inference('sup+', [status(thm)], [zip_derived_cl4998, zip_derived_cl34])).
% 14.70/2.71 thf(zip_derived_cl5026, plain,
% 14.70/2.71 (![X0 : vOptQuery]:
% 14.70/2.71 (((X0) = (vnoQuery)) | ((X0) = (vsomeQuery @ (vgetQuery @ X0))))),
% 14.70/2.71 inference('simplify', [status(thm)], [zip_derived_cl5023])).
% 14.70/2.71 thf('Preservation-Intersection-q1-isSomeQuery-True', conjecture,
% 14.70/2.71 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 14.70/2.71 ( ( ( visSomeQuery @ ( vreduce @ vq1 @ Vts ) ) &
% 14.70/2.71 ( ![Vt00:vTable]: ( ( vq1 ) != ( vtvalue @ Vt00 ) ) ) &
% 14.70/2.71 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 14.70/2.71 ( vptcheck @ Vttc @ ( vIntersection @ vq1 @ vq2 ) @ Vtt ) &
% 14.70/2.71 ( ( vreduce @ ( vIntersection @ vq1 @ vq2 ) @ Vts ) =
% 14.70/2.71 ( vsomeQuery @ Vqr ) ) ) =>
% 14.70/2.71 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 14.70/2.71 thf(zf_stmt_0, negated_conjecture,
% 14.70/2.71 (~( ![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 14.70/2.71 ( ( ( visSomeQuery @ ( vreduce @ vq1 @ Vts ) ) &
% 14.70/2.71 ( ![Vt00:vTable]: ( ( vq1 ) != ( vtvalue @ Vt00 ) ) ) &
% 14.70/2.71 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 14.70/2.71 ( vptcheck @ Vttc @ ( vIntersection @ vq1 @ vq2 ) @ Vtt ) &
% 14.70/2.71 ( ( vreduce @ ( vIntersection @ vq1 @ vq2 ) @ Vts ) =
% 14.70/2.71 ( vsomeQuery @ Vqr ) ) ) =>
% 14.70/2.71 ( vptcheck @ Vttc @ Vqr @ Vtt ) ) )),
% 14.70/2.71 inference('cnf.neg', [status(esa)],
% 14.70/2.71 [Preservation-Intersection-q1-isSomeQuery-True])).
% 14.70/2.71 thf(zip_derived_cl397, plain,
% 14.70/2.71 ( (vstoreContextConsistent @ sk__234 @ sk__235)),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf(TIntersection_inv1, axiom,
% 14.70/2.71 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 14.70/2.71 ( ( vptcheck @ VTTC @ ( vIntersection @ Vq1 @ Vq2 ) @ VTT ) =>
% 14.70/2.71 ( vptcheck @ VTTC @ Vq1 @ VTT ) ))).
% 14.70/2.71 thf(zip_derived_cl387, plain,
% 14.70/2.71 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 14.70/2.71 ( (vptcheck @ X0 @ X1 @ X2)
% 14.70/2.71 | ~ (vptcheck @ X0 @ (vIntersection @ X1 @ X3) @ X2))),
% 14.70/2.71 inference('cnf', [status(esa)], [TIntersection_inv1])).
% 14.70/2.71 thf(zip_derived_cl398, plain,
% 14.70/2.71 ( (vptcheck @ sk__235 @ (vIntersection @ vq1 @ vq2) @ sk__236)),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf(zip_derived_cl5282, plain, ( (vptcheck @ sk__235 @ vq1 @ sk__236)),
% 14.70/2.71 inference('sup+', [status(thm)], [zip_derived_cl387, zip_derived_cl398])).
% 14.70/2.71 thf('Preservation-Intersection-IH0', axiom,
% 14.70/2.71 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 14.70/2.71 ( ( ( vstoreContextConsistent @ Vts @ Vttc ) &
% 14.70/2.71 ( vptcheck @ Vttc @ vq1 @ Vtt ) &
% 14.70/2.71 ( ( vreduce @ vq1 @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 14.70/2.71 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 14.70/2.71 thf(zip_derived_cl391, plain,
% 14.70/2.71 (![X0 : vTTContext, X1 : vTType, X2 : vTStore, X3 : vQuery]:
% 14.70/2.71 (~ (vptcheck @ X0 @ vq1 @ X1)
% 14.70/2.71 | ~ (vstoreContextConsistent @ X2 @ X0)
% 14.70/2.71 | ((vreduce @ vq1 @ X2) != (vsomeQuery @ X3))
% 14.70/2.71 | (vptcheck @ X0 @ X3 @ X1))),
% 14.70/2.71 inference('cnf', [status(esa)], [Preservation-Intersection-IH0])).
% 14.70/2.71 thf(zip_derived_cl5516, plain,
% 14.70/2.71 (![X0 : vQuery, X1 : vTStore]:
% 14.70/2.71 ( (vptcheck @ sk__235 @ X0 @ sk__236)
% 14.70/2.71 | ((vreduce @ vq1 @ X1) != (vsomeQuery @ X0))
% 14.70/2.71 | ~ (vstoreContextConsistent @ X1 @ sk__235))),
% 14.70/2.71 inference('sup-', [status(thm)], [zip_derived_cl5282, zip_derived_cl391])).
% 14.70/2.71 thf(zip_derived_cl5518, plain,
% 14.70/2.71 (![X0 : vQuery]:
% 14.70/2.71 (((vreduce @ vq1 @ sk__234) != (vsomeQuery @ X0))
% 14.70/2.71 | (vptcheck @ sk__235 @ X0 @ sk__236))),
% 14.70/2.71 inference('sup-', [status(thm)], [zip_derived_cl397, zip_derived_cl5516])).
% 14.70/2.71 thf(zip_derived_cl395, plain, ( (visSomeQuery @ (vreduce @ vq1 @ sk__234))),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf('reduce-12', axiom,
% 14.70/2.71 (![Vq1:vQuery,Vq2:vQuery,Vts:vTStore]:
% 14.70/2.71 ( ( ( visSomeQuery @ ( vreduce @ Vq1 @ Vts ) ) &
% 14.70/2.71 ( ![Vt00:vTable,Vq200:vQuery]:
% 14.70/2.71 ( ( ( Vq1 ) != ( vtvalue @ Vt00 ) ) | ( ( Vq2 ) != ( Vq200 ) ) ) ) &
% 14.70/2.71 ( ![Vt100:vTable,Vt200:vTable]:
% 14.70/2.71 ( ( ( Vq1 ) != ( vtvalue @ Vt100 ) ) |
% 14.70/2.71 ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) ) ) ) =>
% 14.70/2.71 ( ( vreduce @ ( vIntersection @ Vq1 @ Vq2 ) @ Vts ) =
% 14.70/2.71 ( vsomeQuery @
% 14.70/2.71 ( vIntersection @ ( vgetQuery @ ( vreduce @ Vq1 @ Vts ) ) @ Vq2 ) ) ) ))).
% 14.70/2.71 thf(zf_stmt_1, axiom,
% 14.70/2.71 (![Vt200:vTable,Vt100:vTable,Vq2:vQuery,Vq1:vQuery]:
% 14.70/2.71 ( ( ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) |
% 14.70/2.71 ( ( Vq1 ) != ( vtvalue @ Vt100 ) ) ) =>
% 14.70/2.71 ( zip_tseitin_24 @ Vt200 @ Vt100 @ Vq2 @ Vq1 ) ))).
% 14.70/2.71 thf(zip_derived_cl214, plain,
% 14.70/2.71 (![X0 : vTable, X1 : vTable, X2 : vQuery, X3 : vQuery]:
% 14.70/2.71 ( (zip_tseitin_24 @ X0 @ X1 @ X2 @ X3) | ((X3) = (vtvalue @ X1)))),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_1])).
% 14.70/2.71 thf(zf_stmt_2, axiom,
% 14.70/2.71 (![Vq200:vQuery,Vt00:vTable,Vq2:vQuery,Vq1:vQuery]:
% 14.70/2.71 ( ( ( ( Vq2 ) != ( Vq200 ) ) | ( ( Vq1 ) != ( vtvalue @ Vt00 ) ) ) =>
% 14.70/2.71 ( zip_tseitin_23 @ Vq200 @ Vt00 @ Vq2 @ Vq1 ) ))).
% 14.70/2.71 thf(zip_derived_cl212, plain,
% 14.70/2.71 (![X0 : vQuery, X1 : vTable, X2 : vQuery, X3 : vQuery]:
% 14.70/2.71 ( (zip_tseitin_23 @ X0 @ X1 @ X2 @ X3) | ((X3) = (vtvalue @ X1)))),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_2])).
% 14.70/2.71 thf(zf_stmt_3, type, zip_tseitin_24 : vTable > vTable > vQuery > vQuery > $o).
% 14.70/2.71 thf(zf_stmt_4, type, zip_tseitin_23 : vQuery > vTable > vQuery > vQuery > $o).
% 14.70/2.71 thf(zf_stmt_5, axiom,
% 14.70/2.71 (![Vq1:vQuery,Vq2:vQuery,Vts:vTStore]:
% 14.70/2.71 ( ( ( ![Vt100:vTable,Vt200:vTable]:
% 14.70/2.71 ( zip_tseitin_24 @ Vt200 @ Vt100 @ Vq2 @ Vq1 ) ) &
% 14.70/2.71 ( ![Vt00:vTable,Vq200:vQuery]:
% 14.70/2.71 ( zip_tseitin_23 @ Vq200 @ Vt00 @ Vq2 @ Vq1 ) ) &
% 14.70/2.71 ( visSomeQuery @ ( vreduce @ Vq1 @ Vts ) ) ) =>
% 14.70/2.71 ( ( vreduce @ ( vIntersection @ Vq1 @ Vq2 ) @ Vts ) =
% 14.70/2.71 ( vsomeQuery @
% 14.70/2.71 ( vIntersection @ ( vgetQuery @ ( vreduce @ Vq1 @ Vts ) ) @ Vq2 ) ) ) ))).
% 14.70/2.71 thf(zip_derived_cl215, plain,
% 14.70/2.71 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 14.70/2.71 (~ (zip_tseitin_23 @ (sk__116 @ X0 @ X1) @ (sk__115 @ X0 @ X1) @ X0 @
% 14.70/2.71 X1)
% 14.70/2.71 | ~ (zip_tseitin_24 @ (sk__118 @ X0 @ X1) @ (sk__117 @ X0 @ X1) @
% 14.70/2.71 X0 @ X1)
% 14.70/2.71 | ~ (visSomeQuery @ (vreduce @ X1 @ X2))
% 14.70/2.71 | ((vreduce @ (vIntersection @ X1 @ X0) @ X2)
% 14.70/2.71 = (vsomeQuery @
% 14.70/2.71 (vIntersection @ (vgetQuery @ (vreduce @ X1 @ X2)) @ X0))))),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_5])).
% 14.70/2.71 thf(zip_derived_cl1310, plain,
% 14.70/2.71 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 14.70/2.71 (((X0) = (vtvalue @ (sk__115 @ X1 @ X0)))
% 14.70/2.71 | ((vreduce @ (vIntersection @ X0 @ X1) @ X2)
% 14.70/2.71 = (vsomeQuery @
% 14.70/2.71 (vIntersection @ (vgetQuery @ (vreduce @ X0 @ X2)) @ X1)))
% 14.70/2.71 | ~ (visSomeQuery @ (vreduce @ X0 @ X2))
% 14.70/2.71 | ~ (zip_tseitin_24 @ (sk__118 @ X1 @ X0) @ (sk__117 @ X1 @ X0) @
% 14.70/2.71 X1 @ X0))),
% 14.70/2.71 inference('dp-resolution', [status(thm)],
% 14.70/2.71 [zip_derived_cl212, zip_derived_cl215])).
% 14.70/2.71 thf(zip_derived_cl1362, plain,
% 14.70/2.71 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 14.70/2.71 (((X0) = (vtvalue @ (sk__117 @ X1 @ X0)))
% 14.70/2.71 | ~ (visSomeQuery @ (vreduce @ X0 @ X2))
% 14.70/2.71 | ((vreduce @ (vIntersection @ X0 @ X1) @ X2)
% 14.70/2.71 = (vsomeQuery @
% 14.70/2.71 (vIntersection @ (vgetQuery @ (vreduce @ X0 @ X2)) @ X1)))
% 14.70/2.71 | ((X0) = (vtvalue @ (sk__115 @ X1 @ X0))))),
% 14.70/2.71 inference('dp-resolution', [status(thm)],
% 14.70/2.71 [zip_derived_cl214, zip_derived_cl1310])).
% 14.70/2.71 thf(zip_derived_cl7629, plain,
% 14.70/2.71 (![X0 : vQuery]:
% 14.70/2.71 (((vq1) = (vtvalue @ (sk__115 @ X0 @ vq1)))
% 14.70/2.71 | ((vreduce @ (vIntersection @ vq1 @ X0) @ sk__234)
% 14.70/2.71 = (vsomeQuery @
% 14.70/2.71 (vIntersection @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ X0)))
% 14.70/2.71 | ((vq1) = (vtvalue @ (sk__117 @ X0 @ vq1))))),
% 14.70/2.71 inference('sup-', [status(thm)], [zip_derived_cl395, zip_derived_cl1362])).
% 14.70/2.71 thf(zip_derived_cl396, plain, (![X0 : vTable]: ((vq1) != (vtvalue @ X0))),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf(zip_derived_cl396, plain, (![X0 : vTable]: ((vq1) != (vtvalue @ X0))),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf(zip_derived_cl7660, plain,
% 14.70/2.71 (![X0 : vQuery]:
% 14.70/2.71 ((vreduce @ (vIntersection @ vq1 @ X0) @ sk__234)
% 14.70/2.71 = (vsomeQuery @
% 14.70/2.71 (vIntersection @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ X0)))),
% 14.70/2.71 inference('simplify_reflect-', [status(thm)],
% 14.70/2.71 [zip_derived_cl7629, zip_derived_cl396, zip_derived_cl396])).
% 14.70/2.71 thf(zip_derived_cl394, plain,
% 14.70/2.71 (((vreduce @ (vIntersection @ vq1 @ vq2) @ sk__234)
% 14.70/2.71 = (vsomeQuery @ sk__237))),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf(zip_derived_cl7755, plain,
% 14.70/2.71 (((vsomeQuery @
% 14.70/2.71 (vIntersection @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ vq2))
% 14.70/2.71 = (vsomeQuery @ sk__237))),
% 14.70/2.71 inference('sup+', [status(thm)], [zip_derived_cl7660, zip_derived_cl394])).
% 14.70/2.71 thf(zip_derived_cl47, plain,
% 14.70/2.71 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 14.70/2.71 inference('cnf', [status(esa)], [getQuery-0])).
% 14.70/2.71 thf(zip_derived_cl7775, plain,
% 14.70/2.71 (((vgetQuery @ (vsomeQuery @ sk__237))
% 14.70/2.71 = (vIntersection @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ vq2))),
% 14.70/2.71 inference('sup+', [status(thm)], [zip_derived_cl7755, zip_derived_cl47])).
% 14.70/2.71 thf(zip_derived_cl47, plain,
% 14.70/2.71 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 14.70/2.71 inference('cnf', [status(esa)], [getQuery-0])).
% 14.70/2.71 thf(zip_derived_cl7787, plain,
% 14.70/2.71 (((sk__237)
% 14.70/2.71 = (vIntersection @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ vq2))),
% 14.70/2.71 inference('demod', [status(thm)], [zip_derived_cl7775, zip_derived_cl47])).
% 14.70/2.71 thf(TIntersection, axiom,
% 14.70/2.71 (![VTTC:vTTContext,Vq1:vQuery,VTT:vTType,Vq2:vQuery]:
% 14.70/2.71 ( ( ( vptcheck @ VTTC @ Vq1 @ VTT ) & ( vptcheck @ VTTC @ Vq2 @ VTT ) ) =>
% 14.70/2.71 ( vptcheck @ VTTC @ ( vIntersection @ Vq1 @ Vq2 ) @ VTT ) ))).
% 14.70/2.71 thf(zip_derived_cl379, plain,
% 14.70/2.71 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 14.70/2.71 (~ (vptcheck @ X0 @ X1 @ X2)
% 14.70/2.71 | ~ (vptcheck @ X0 @ X3 @ X2)
% 14.70/2.71 | (vptcheck @ X0 @ (vIntersection @ X1 @ X3) @ X2))),
% 14.70/2.71 inference('cnf', [status(esa)], [TIntersection])).
% 14.70/2.71 thf(zip_derived_cl7927, plain,
% 14.70/2.71 (![X0 : vTType, X1 : vTTContext]:
% 14.70/2.71 ( (vptcheck @ X1 @ sk__237 @ X0)
% 14.70/2.71 | ~ (vptcheck @ X1 @ vq2 @ X0)
% 14.70/2.71 | ~ (vptcheck @ X1 @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ X0))),
% 14.70/2.71 inference('sup+', [status(thm)], [zip_derived_cl7787, zip_derived_cl379])).
% 14.70/2.71 thf(zip_derived_cl8689, plain,
% 14.70/2.71 ((((vreduce @ vq1 @ sk__234)
% 14.70/2.71 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__234))))
% 14.70/2.71 | ~ (vptcheck @ sk__235 @ vq2 @ sk__236)
% 14.70/2.71 | (vptcheck @ sk__235 @ sk__237 @ sk__236))),
% 14.70/2.71 inference('sup-', [status(thm)], [zip_derived_cl5518, zip_derived_cl7927])).
% 14.70/2.71 thf(TIntersection_inv2, axiom,
% 14.70/2.71 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 14.70/2.71 ( ( vptcheck @ VTTC @ ( vIntersection @ Vq1 @ Vq2 ) @ VTT ) =>
% 14.70/2.71 ( vptcheck @ VTTC @ Vq2 @ VTT ) ))).
% 14.70/2.71 thf(zip_derived_cl388, plain,
% 14.70/2.71 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 14.70/2.71 ( (vptcheck @ X0 @ X1 @ X2)
% 14.70/2.71 | ~ (vptcheck @ X0 @ (vIntersection @ X3 @ X1) @ X2))),
% 14.70/2.71 inference('cnf', [status(esa)], [TIntersection_inv2])).
% 14.70/2.71 thf(zip_derived_cl398, plain,
% 14.70/2.71 ( (vptcheck @ sk__235 @ (vIntersection @ vq1 @ vq2) @ sk__236)),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf(zip_derived_cl5284, plain, ( (vptcheck @ sk__235 @ vq2 @ sk__236)),
% 14.70/2.71 inference('sup+', [status(thm)], [zip_derived_cl388, zip_derived_cl398])).
% 14.70/2.71 thf(zip_derived_cl8691, plain,
% 14.70/2.71 ((((vreduce @ vq1 @ sk__234)
% 14.70/2.71 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__234))))
% 14.70/2.71 | (vptcheck @ sk__235 @ sk__237 @ sk__236))),
% 14.70/2.71 inference('demod', [status(thm)],
% 14.70/2.71 [zip_derived_cl8689, zip_derived_cl5284])).
% 14.70/2.71 thf(zip_derived_cl393, plain, (~ (vptcheck @ sk__235 @ sk__237 @ sk__236)),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf(zip_derived_cl8697, plain,
% 14.70/2.71 (((vreduce @ vq1 @ sk__234)
% 14.70/2.71 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__234))))),
% 14.70/2.71 inference('clc', [status(thm)], [zip_derived_cl8691, zip_derived_cl393])).
% 14.70/2.71 thf(zip_derived_cl8698, plain,
% 14.70/2.71 ((((vreduce @ vq1 @ sk__234) != (vreduce @ vq1 @ sk__234))
% 14.70/2.71 | ((vreduce @ vq1 @ sk__234) = (vnoQuery)))),
% 14.70/2.71 inference('sup-', [status(thm)], [zip_derived_cl5026, zip_derived_cl8697])).
% 14.70/2.71 thf(zip_derived_cl8700, plain, (((vreduce @ vq1 @ sk__234) = (vnoQuery))),
% 14.70/2.71 inference('simplify', [status(thm)], [zip_derived_cl8698])).
% 14.70/2.71 thf('isSomeQuery-true-INV', axiom,
% 14.70/2.71 (![VOptQuery0:vOptQuery]:
% 14.70/2.71 ( ( visSomeQuery @ VOptQuery0 ) =>
% 14.70/2.71 ( ?[VwildcardName0:vQuery]:
% 14.70/2.71 ( ( VOptQuery0 ) = ( vsomeQuery @ VwildcardName0 ) ) ) ))).
% 14.70/2.71 thf(zip_derived_cl169, plain,
% 14.70/2.71 (![X0 : vOptQuery]:
% 14.70/2.71 (((X0) = (vsomeQuery @ (sk__91 @ X0))) | ~ (visSomeQuery @ X0))),
% 14.70/2.71 inference('cnf', [status(esa)], [isSomeQuery-true-INV])).
% 14.70/2.71 thf('DIFF-noQuery-someQuery', axiom,
% 14.70/2.71 (![VQuery0:vQuery]: ( ( vnoQuery ) != ( vsomeQuery @ VQuery0 ) ))).
% 14.70/2.71 thf(zip_derived_cl36, plain,
% 14.70/2.71 (![X0 : vQuery]: ((vnoQuery) != (vsomeQuery @ X0))),
% 14.70/2.71 inference('cnf', [status(esa)], [DIFF-noQuery-someQuery])).
% 14.70/2.71 thf(zip_derived_cl4977, plain,
% 14.70/2.71 (![X0 : vOptQuery]: (((vnoQuery) != (X0)) | ~ (visSomeQuery @ X0))),
% 14.70/2.71 inference('sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl36])).
% 14.70/2.71 thf(zip_derived_cl395, plain, ( (visSomeQuery @ (vreduce @ vq1 @ sk__234))),
% 14.70/2.71 inference('cnf', [status(esa)], [zf_stmt_0])).
% 14.70/2.71 thf(zip_derived_cl4983, plain, (((vnoQuery) != (vreduce @ vq1 @ sk__234))),
% 14.70/2.71 inference('sup+', [status(thm)], [zip_derived_cl4977, zip_derived_cl395])).
% 14.70/2.71 thf(zip_derived_cl8701, plain, ($false),
% 14.70/2.71 inference('simplify_reflect-', [status(thm)],
% 14.70/2.71 [zip_derived_cl8700, zip_derived_cl4983])).
% 14.70/2.71
% 14.70/2.71 % SZS output end Refutation
% 14.70/2.71
% 14.70/2.71
% 14.70/2.71 % Terminating...
% 14.70/2.77 % Runner terminated.
% 14.70/2.79 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------