%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM285_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.1QgXMFFcI8 true
% Computer : n008.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:24 PM UTC 2026
% Result : Theorem 15.28s 2.89s
% Output : Refutation 15.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.14 % Problem : COM285_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.15 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.1QgXMFFcI8 true
% 0.17/0.36 % Computer : n008.cluster.edu
% 0.17/0.36 % Model : x86_64 x86_64
% 0.17/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.36 % Memory : 8042.1875MB
% 0.17/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.36 % CPULimit : 300
% 0.17/0.36 % WCLimit : 300
% 0.17/0.36 % DateTime : Mon May 4 20:19:13 EDT 2026
% 0.17/0.36 % CPUTime :
% 0.17/0.36 % Running portfolio for 300 s
% 0.17/0.36 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.36 % Number of cores: 8
% 0.17/0.37 % Python version: Python 3.6.8
% 0.17/0.37 % Running in FO mode
% 0.53/0.69 % Total configuration time : 435
% 0.53/0.69 % Estimated wc time : 1092
% 0.53/0.69 % Estimated cpu time (7 cpus) : 156.0
% 0.57/0.77 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.57/0.78 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.57/0.80 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.59/0.80 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.59/0.80 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.59/0.80 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.59/0.81 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 15.28/2.89 % Solved by fo/fo3_bce.sh.
% 15.28/2.89 % BCE start: 399
% 15.28/2.89 % BCE eliminated: 0
% 15.28/2.89 % PE start: 399
% 15.28/2.89 logic: eq
% 15.28/2.89 % PE eliminated: -44
% 15.28/2.89 % done 1047 iterations in 2.087s
% 15.28/2.89 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 15.28/2.89 % SZS output start Refutation
% 15.28/2.89 thf(vOptQuery_type, type, vOptQuery: $tType).
% 15.28/2.89 thf(vQuery_type, type, vQuery: $tType).
% 15.28/2.89 thf(vTStore_type, type, vTStore: $tType).
% 15.28/2.89 thf(vTable_type, type, vTable: $tType).
% 15.28/2.89 thf(vTTContext_type, type, vTTContext: $tType).
% 15.28/2.89 thf(vTType_type, type, vTType: $tType).
% 15.28/2.89 thf(vtvalue_type, type, vtvalue: vTable > vQuery).
% 15.28/2.89 thf(sk__127_type, type, sk__127: vQuery > vQuery > vTable).
% 15.28/2.89 thf(sk__236_type, type, sk__236: vTType).
% 15.28/2.89 thf(vq2_type, type, vq2: vQuery).
% 15.28/2.89 thf(vptcheck_type, type, vptcheck: vTTContext > vQuery > vTType > $o).
% 15.28/2.89 thf(zip_tseitin_28_type, type, zip_tseitin_28: vTable > vTable > vQuery >
% 15.28/2.89 vQuery > $o).
% 15.28/2.89 thf(vnoQuery_type, type, vnoQuery: vOptQuery).
% 15.28/2.89 thf(vDifference_type, type, vDifference: vQuery > vQuery > vQuery).
% 15.28/2.89 thf(sk__129_type, type, sk__129: vQuery > vQuery > vTable).
% 15.28/2.89 thf(visSomeQuery_type, type, visSomeQuery: vOptQuery > $o).
% 15.28/2.89 thf(sk__128_type, type, sk__128: vQuery > vQuery > vQuery).
% 15.28/2.89 thf(sk__91_type, type, sk__91: vOptQuery > vQuery).
% 15.28/2.89 thf(sk__130_type, type, sk__130: vQuery > vQuery > vTable).
% 15.28/2.89 thf(vreduce_type, type, vreduce: vQuery > vTStore > vOptQuery).
% 15.28/2.89 thf(vq1_type, type, vq1: vQuery).
% 15.28/2.89 thf(zip_tseitin_27_type, type, zip_tseitin_27: vQuery > vTable > vQuery >
% 15.28/2.89 vQuery > $o).
% 15.28/2.89 thf(vgetQuery_type, type, vgetQuery: vOptQuery > vQuery).
% 15.28/2.89 thf(sk__237_type, type, sk__237: vQuery).
% 15.28/2.89 thf(sk__235_type, type, sk__235: vTTContext).
% 15.28/2.89 thf(sk__16_type, type, sk__16: vOptQuery > vQuery).
% 15.28/2.89 thf(vstoreContextConsistent_type, type, vstoreContextConsistent: vTStore >
% 15.28/2.89 vTTContext > $o).
% 15.28/2.89 thf(vsomeQuery_type, type, vsomeQuery: vQuery > vOptQuery).
% 15.28/2.89 thf(sk__234_type, type, sk__234: vTStore).
% 15.28/2.89 thf('dom-OptQuery', axiom,
% 15.28/2.89 (![VX:vOptQuery]:
% 15.28/2.89 ( ( ?[VQuery0:vQuery]: ( ( VX ) = ( vsomeQuery @ VQuery0 ) ) ) |
% 15.28/2.89 ( ( VX ) = ( vnoQuery ) ) ))).
% 15.28/2.89 thf(zip_derived_cl34, plain,
% 15.28/2.89 (![X0 : vOptQuery]:
% 15.28/2.89 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 15.28/2.89 inference('cnf', [status(esa)], [dom-OptQuery])).
% 15.28/2.89 thf('getQuery-0', axiom,
% 15.28/2.89 (![Vq:vQuery]: ( ( vgetQuery @ ( vsomeQuery @ Vq ) ) = ( Vq ) ))).
% 15.28/2.89 thf(zip_derived_cl47, plain,
% 15.28/2.89 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 15.28/2.89 inference('cnf', [status(esa)], [getQuery-0])).
% 15.28/2.89 thf(zip_derived_cl4998, plain,
% 15.28/2.89 (![X0 : vOptQuery]:
% 15.28/2.89 (((vgetQuery @ X0) = (sk__16 @ X0)) | ((X0) = (vnoQuery)))),
% 15.28/2.89 inference('sup+', [status(thm)], [zip_derived_cl34, zip_derived_cl47])).
% 15.28/2.89 thf(zip_derived_cl34, plain,
% 15.28/2.89 (![X0 : vOptQuery]:
% 15.28/2.89 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 15.28/2.89 inference('cnf', [status(esa)], [dom-OptQuery])).
% 15.28/2.89 thf(zip_derived_cl5023, plain,
% 15.28/2.89 (![X0 : vOptQuery]:
% 15.28/2.89 (((X0) = (vsomeQuery @ (vgetQuery @ X0)))
% 15.28/2.89 | ((X0) = (vnoQuery))
% 15.28/2.89 | ((X0) = (vnoQuery)))),
% 15.28/2.89 inference('sup+', [status(thm)], [zip_derived_cl4998, zip_derived_cl34])).
% 15.28/2.89 thf(zip_derived_cl5026, plain,
% 15.28/2.89 (![X0 : vOptQuery]:
% 15.28/2.89 (((X0) = (vnoQuery)) | ((X0) = (vsomeQuery @ (vgetQuery @ X0))))),
% 15.28/2.89 inference('simplify', [status(thm)], [zip_derived_cl5023])).
% 15.28/2.89 thf('Preservation-Difference-q1-isSomeQuery-True', conjecture,
% 15.28/2.89 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 15.28/2.89 ( ( ( visSomeQuery @ ( vreduce @ vq1 @ Vts ) ) &
% 15.28/2.89 ( ![Vt00:vTable]: ( ( vq1 ) != ( vtvalue @ Vt00 ) ) ) &
% 15.28/2.89 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 15.28/2.89 ( vptcheck @ Vttc @ ( vDifference @ vq1 @ vq2 ) @ Vtt ) &
% 15.28/2.89 ( ( vreduce @ ( vDifference @ vq1 @ vq2 ) @ Vts ) =
% 15.28/2.89 ( vsomeQuery @ Vqr ) ) ) =>
% 15.28/2.89 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 15.28/2.89 thf(zf_stmt_0, negated_conjecture,
% 15.28/2.89 (~( ![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 15.28/2.89 ( ( ( visSomeQuery @ ( vreduce @ vq1 @ Vts ) ) &
% 15.28/2.89 ( ![Vt00:vTable]: ( ( vq1 ) != ( vtvalue @ Vt00 ) ) ) &
% 15.28/2.89 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 15.28/2.89 ( vptcheck @ Vttc @ ( vDifference @ vq1 @ vq2 ) @ Vtt ) &
% 15.28/2.89 ( ( vreduce @ ( vDifference @ vq1 @ vq2 ) @ Vts ) =
% 15.28/2.89 ( vsomeQuery @ Vqr ) ) ) =>
% 15.28/2.89 ( vptcheck @ Vttc @ Vqr @ Vtt ) ) )),
% 15.28/2.89 inference('cnf.neg', [status(esa)],
% 15.28/2.89 [Preservation-Difference-q1-isSomeQuery-True])).
% 15.28/2.89 thf(zip_derived_cl397, plain,
% 15.28/2.89 ( (vstoreContextConsistent @ sk__234 @ sk__235)),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf(TDifference_inv1, axiom,
% 15.28/2.89 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 15.28/2.89 ( ( vptcheck @ VTTC @ ( vDifference @ Vq1 @ Vq2 ) @ VTT ) =>
% 15.28/2.89 ( vptcheck @ VTTC @ Vq1 @ VTT ) ))).
% 15.28/2.89 thf(zip_derived_cl389, plain,
% 15.28/2.89 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 15.28/2.89 ( (vptcheck @ X0 @ X1 @ X2)
% 15.28/2.89 | ~ (vptcheck @ X0 @ (vDifference @ X1 @ X3) @ X2))),
% 15.28/2.89 inference('cnf', [status(esa)], [TDifference_inv1])).
% 15.28/2.89 thf(zip_derived_cl398, plain,
% 15.28/2.89 ( (vptcheck @ sk__235 @ (vDifference @ vq1 @ vq2) @ sk__236)),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf(zip_derived_cl5282, plain, ( (vptcheck @ sk__235 @ vq1 @ sk__236)),
% 15.28/2.89 inference('sup+', [status(thm)], [zip_derived_cl389, zip_derived_cl398])).
% 15.28/2.89 thf('Preservation-Difference-IH0', axiom,
% 15.28/2.89 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 15.28/2.89 ( ( ( vstoreContextConsistent @ Vts @ Vttc ) &
% 15.28/2.89 ( vptcheck @ Vttc @ vq1 @ Vtt ) &
% 15.28/2.89 ( ( vreduce @ vq1 @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 15.28/2.89 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 15.28/2.89 thf(zip_derived_cl391, plain,
% 15.28/2.89 (![X0 : vTTContext, X1 : vTType, X2 : vTStore, X3 : vQuery]:
% 15.28/2.89 (~ (vptcheck @ X0 @ vq1 @ X1)
% 15.28/2.89 | ~ (vstoreContextConsistent @ X2 @ X0)
% 15.28/2.89 | ((vreduce @ vq1 @ X2) != (vsomeQuery @ X3))
% 15.28/2.89 | (vptcheck @ X0 @ X3 @ X1))),
% 15.28/2.89 inference('cnf', [status(esa)], [Preservation-Difference-IH0])).
% 15.28/2.89 thf(zip_derived_cl5528, plain,
% 15.28/2.89 (![X0 : vQuery, X1 : vTStore]:
% 15.28/2.89 ( (vptcheck @ sk__235 @ X0 @ sk__236)
% 15.28/2.89 | ((vreduce @ vq1 @ X1) != (vsomeQuery @ X0))
% 15.28/2.89 | ~ (vstoreContextConsistent @ X1 @ sk__235))),
% 15.28/2.89 inference('sup-', [status(thm)], [zip_derived_cl5282, zip_derived_cl391])).
% 15.28/2.89 thf(zip_derived_cl5530, plain,
% 15.28/2.89 (![X0 : vQuery]:
% 15.28/2.89 (((vreduce @ vq1 @ sk__234) != (vsomeQuery @ X0))
% 15.28/2.89 | (vptcheck @ sk__235 @ X0 @ sk__236))),
% 15.28/2.89 inference('sup-', [status(thm)], [zip_derived_cl397, zip_derived_cl5528])).
% 15.28/2.89 thf(zip_derived_cl395, plain, ( (visSomeQuery @ (vreduce @ vq1 @ sk__234))),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf('reduce-17', axiom,
% 15.28/2.89 (![Vq1:vQuery,Vq2:vQuery,Vts:vTStore]:
% 15.28/2.89 ( ( ( visSomeQuery @ ( vreduce @ Vq1 @ Vts ) ) &
% 15.28/2.89 ( ![Vt00:vTable,Vq200:vQuery]:
% 15.28/2.89 ( ( ( Vq1 ) != ( vtvalue @ Vt00 ) ) | ( ( Vq2 ) != ( Vq200 ) ) ) ) &
% 15.28/2.89 ( ![Vt100:vTable,Vt200:vTable]:
% 15.28/2.89 ( ( ( Vq1 ) != ( vtvalue @ Vt100 ) ) |
% 15.28/2.89 ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) ) ) ) =>
% 15.28/2.89 ( ( vreduce @ ( vDifference @ Vq1 @ Vq2 ) @ Vts ) =
% 15.28/2.89 ( vsomeQuery @
% 15.28/2.89 ( vDifference @ ( vgetQuery @ ( vreduce @ Vq1 @ Vts ) ) @ Vq2 ) ) ) ))).
% 15.28/2.89 thf(zf_stmt_1, axiom,
% 15.28/2.89 (![Vt200:vTable,Vt100:vTable,Vq2:vQuery,Vq1:vQuery]:
% 15.28/2.89 ( ( ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) |
% 15.28/2.89 ( ( Vq1 ) != ( vtvalue @ Vt100 ) ) ) =>
% 15.28/2.89 ( zip_tseitin_28 @ Vt200 @ Vt100 @ Vq2 @ Vq1 ) ))).
% 15.28/2.89 thf(zip_derived_cl229, plain,
% 15.28/2.89 (![X0 : vTable, X1 : vTable, X2 : vQuery, X3 : vQuery]:
% 15.28/2.89 ( (zip_tseitin_28 @ X0 @ X1 @ X2 @ X3) | ((X3) = (vtvalue @ X1)))),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_1])).
% 15.28/2.89 thf(zf_stmt_2, axiom,
% 15.28/2.89 (![Vq200:vQuery,Vt00:vTable,Vq2:vQuery,Vq1:vQuery]:
% 15.28/2.89 ( ( ( ( Vq2 ) != ( Vq200 ) ) | ( ( Vq1 ) != ( vtvalue @ Vt00 ) ) ) =>
% 15.28/2.89 ( zip_tseitin_27 @ Vq200 @ Vt00 @ Vq2 @ Vq1 ) ))).
% 15.28/2.89 thf(zip_derived_cl227, plain,
% 15.28/2.89 (![X0 : vQuery, X1 : vTable, X2 : vQuery, X3 : vQuery]:
% 15.28/2.89 ( (zip_tseitin_27 @ X0 @ X1 @ X2 @ X3) | ((X3) = (vtvalue @ X1)))),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_2])).
% 15.28/2.89 thf(zf_stmt_3, type, zip_tseitin_28 : vTable > vTable > vQuery > vQuery > $o).
% 15.28/2.89 thf(zf_stmt_4, type, zip_tseitin_27 : vQuery > vTable > vQuery > vQuery > $o).
% 15.28/2.89 thf(zf_stmt_5, axiom,
% 15.28/2.89 (![Vq1:vQuery,Vq2:vQuery,Vts:vTStore]:
% 15.28/2.89 ( ( ( ![Vt100:vTable,Vt200:vTable]:
% 15.28/2.89 ( zip_tseitin_28 @ Vt200 @ Vt100 @ Vq2 @ Vq1 ) ) &
% 15.28/2.89 ( ![Vt00:vTable,Vq200:vQuery]:
% 15.28/2.89 ( zip_tseitin_27 @ Vq200 @ Vt00 @ Vq2 @ Vq1 ) ) &
% 15.28/2.89 ( visSomeQuery @ ( vreduce @ Vq1 @ Vts ) ) ) =>
% 15.28/2.89 ( ( vreduce @ ( vDifference @ Vq1 @ Vq2 ) @ Vts ) =
% 15.28/2.89 ( vsomeQuery @
% 15.28/2.89 ( vDifference @ ( vgetQuery @ ( vreduce @ Vq1 @ Vts ) ) @ Vq2 ) ) ) ))).
% 15.28/2.89 thf(zip_derived_cl230, plain,
% 15.28/2.89 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 15.28/2.89 (~ (zip_tseitin_27 @ (sk__128 @ X0 @ X1) @ (sk__127 @ X0 @ X1) @ X0 @
% 15.28/2.89 X1)
% 15.28/2.89 | ~ (zip_tseitin_28 @ (sk__130 @ X0 @ X1) @ (sk__129 @ X0 @ X1) @
% 15.28/2.89 X0 @ X1)
% 15.28/2.89 | ~ (visSomeQuery @ (vreduce @ X1 @ X2))
% 15.28/2.89 | ((vreduce @ (vDifference @ X1 @ X0) @ X2)
% 15.28/2.89 = (vsomeQuery @
% 15.28/2.89 (vDifference @ (vgetQuery @ (vreduce @ X1 @ X2)) @ X0))))),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_5])).
% 15.28/2.89 thf(zip_derived_cl1314, plain,
% 15.28/2.89 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 15.28/2.89 (((X0) = (vtvalue @ (sk__127 @ X1 @ X0)))
% 15.28/2.89 | ((vreduce @ (vDifference @ X0 @ X1) @ X2)
% 15.28/2.89 = (vsomeQuery @
% 15.28/2.89 (vDifference @ (vgetQuery @ (vreduce @ X0 @ X2)) @ X1)))
% 15.28/2.89 | ~ (visSomeQuery @ (vreduce @ X0 @ X2))
% 15.28/2.89 | ~ (zip_tseitin_28 @ (sk__130 @ X1 @ X0) @ (sk__129 @ X1 @ X0) @
% 15.28/2.89 X1 @ X0))),
% 15.28/2.89 inference('dp-resolution', [status(thm)],
% 15.28/2.89 [zip_derived_cl227, zip_derived_cl230])).
% 15.28/2.89 thf(zip_derived_cl1370, plain,
% 15.28/2.89 (![X0 : vQuery, X1 : vQuery, X2 : vTStore]:
% 15.28/2.89 (((X0) = (vtvalue @ (sk__129 @ X1 @ X0)))
% 15.28/2.89 | ~ (visSomeQuery @ (vreduce @ X0 @ X2))
% 15.28/2.89 | ((vreduce @ (vDifference @ X0 @ X1) @ X2)
% 15.28/2.89 = (vsomeQuery @
% 15.28/2.89 (vDifference @ (vgetQuery @ (vreduce @ X0 @ X2)) @ X1)))
% 15.28/2.89 | ((X0) = (vtvalue @ (sk__127 @ X1 @ X0))))),
% 15.28/2.89 inference('dp-resolution', [status(thm)],
% 15.28/2.89 [zip_derived_cl229, zip_derived_cl1314])).
% 15.28/2.89 thf(zip_derived_cl8911, plain,
% 15.28/2.89 (![X0 : vQuery]:
% 15.28/2.89 (((vq1) = (vtvalue @ (sk__127 @ X0 @ vq1)))
% 15.28/2.89 | ((vreduce @ (vDifference @ vq1 @ X0) @ sk__234)
% 15.28/2.89 = (vsomeQuery @
% 15.28/2.89 (vDifference @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ X0)))
% 15.28/2.89 | ((vq1) = (vtvalue @ (sk__129 @ X0 @ vq1))))),
% 15.28/2.89 inference('sup-', [status(thm)], [zip_derived_cl395, zip_derived_cl1370])).
% 15.28/2.89 thf(zip_derived_cl396, plain, (![X0 : vTable]: ((vq1) != (vtvalue @ X0))),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf(zip_derived_cl396, plain, (![X0 : vTable]: ((vq1) != (vtvalue @ X0))),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf(zip_derived_cl8948, plain,
% 15.28/2.89 (![X0 : vQuery]:
% 15.28/2.89 ((vreduce @ (vDifference @ vq1 @ X0) @ sk__234)
% 15.28/2.89 = (vsomeQuery @
% 15.28/2.89 (vDifference @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ X0)))),
% 15.28/2.89 inference('simplify_reflect-', [status(thm)],
% 15.28/2.89 [zip_derived_cl8911, zip_derived_cl396, zip_derived_cl396])).
% 15.28/2.89 thf(zip_derived_cl394, plain,
% 15.28/2.89 (((vreduce @ (vDifference @ vq1 @ vq2) @ sk__234)
% 15.28/2.89 = (vsomeQuery @ sk__237))),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf(zip_derived_cl9070, plain,
% 15.28/2.89 (((vsomeQuery @
% 15.28/2.89 (vDifference @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ vq2))
% 15.28/2.89 = (vsomeQuery @ sk__237))),
% 15.28/2.89 inference('sup+', [status(thm)], [zip_derived_cl8948, zip_derived_cl394])).
% 15.28/2.89 thf(zip_derived_cl47, plain,
% 15.28/2.89 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 15.28/2.89 inference('cnf', [status(esa)], [getQuery-0])).
% 15.28/2.89 thf(zip_derived_cl9097, plain,
% 15.28/2.89 (((vgetQuery @ (vsomeQuery @ sk__237))
% 15.28/2.89 = (vDifference @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ vq2))),
% 15.28/2.89 inference('sup+', [status(thm)], [zip_derived_cl9070, zip_derived_cl47])).
% 15.28/2.89 thf(zip_derived_cl47, plain,
% 15.28/2.89 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 15.28/2.89 inference('cnf', [status(esa)], [getQuery-0])).
% 15.28/2.89 thf(zip_derived_cl9109, plain,
% 15.28/2.89 (((sk__237)
% 15.28/2.89 = (vDifference @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ vq2))),
% 15.28/2.89 inference('demod', [status(thm)], [zip_derived_cl9097, zip_derived_cl47])).
% 15.28/2.89 thf(TDifference, axiom,
% 15.28/2.89 (![VTTC:vTTContext,Vq1:vQuery,VTT:vTType,Vq2:vQuery]:
% 15.28/2.89 ( ( ( vptcheck @ VTTC @ Vq1 @ VTT ) & ( vptcheck @ VTTC @ Vq2 @ VTT ) ) =>
% 15.28/2.89 ( vptcheck @ VTTC @ ( vDifference @ Vq1 @ Vq2 ) @ VTT ) ))).
% 15.28/2.89 thf(zip_derived_cl380, plain,
% 15.28/2.89 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 15.28/2.89 (~ (vptcheck @ X0 @ X1 @ X2)
% 15.28/2.89 | ~ (vptcheck @ X0 @ X3 @ X2)
% 15.28/2.89 | (vptcheck @ X0 @ (vDifference @ X1 @ X3) @ X2))),
% 15.28/2.89 inference('cnf', [status(esa)], [TDifference])).
% 15.28/2.89 thf(zip_derived_cl9278, plain,
% 15.28/2.89 (![X0 : vTType, X1 : vTTContext]:
% 15.28/2.89 ( (vptcheck @ X1 @ sk__237 @ X0)
% 15.28/2.89 | ~ (vptcheck @ X1 @ vq2 @ X0)
% 15.28/2.89 | ~ (vptcheck @ X1 @ (vgetQuery @ (vreduce @ vq1 @ sk__234)) @ X0))),
% 15.28/2.89 inference('sup+', [status(thm)], [zip_derived_cl9109, zip_derived_cl380])).
% 15.28/2.89 thf(zip_derived_cl9815, plain,
% 15.28/2.89 ((((vreduce @ vq1 @ sk__234)
% 15.28/2.89 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__234))))
% 15.28/2.89 | ~ (vptcheck @ sk__235 @ vq2 @ sk__236)
% 15.28/2.89 | (vptcheck @ sk__235 @ sk__237 @ sk__236))),
% 15.28/2.89 inference('sup-', [status(thm)], [zip_derived_cl5530, zip_derived_cl9278])).
% 15.28/2.89 thf(TDifference_inv2, axiom,
% 15.28/2.89 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 15.28/2.89 ( ( vptcheck @ VTTC @ ( vDifference @ Vq1 @ Vq2 ) @ VTT ) =>
% 15.28/2.89 ( vptcheck @ VTTC @ Vq2 @ VTT ) ))).
% 15.28/2.89 thf(zip_derived_cl390, plain,
% 15.28/2.89 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 15.28/2.89 ( (vptcheck @ X0 @ X1 @ X2)
% 15.28/2.89 | ~ (vptcheck @ X0 @ (vDifference @ X3 @ X1) @ X2))),
% 15.28/2.89 inference('cnf', [status(esa)], [TDifference_inv2])).
% 15.28/2.89 thf(zip_derived_cl398, plain,
% 15.28/2.89 ( (vptcheck @ sk__235 @ (vDifference @ vq1 @ vq2) @ sk__236)),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf(zip_derived_cl5297, plain, ( (vptcheck @ sk__235 @ vq2 @ sk__236)),
% 15.28/2.89 inference('sup+', [status(thm)], [zip_derived_cl390, zip_derived_cl398])).
% 15.28/2.89 thf(zip_derived_cl9817, plain,
% 15.28/2.89 ((((vreduce @ vq1 @ sk__234)
% 15.28/2.89 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__234))))
% 15.28/2.89 | (vptcheck @ sk__235 @ sk__237 @ sk__236))),
% 15.28/2.89 inference('demod', [status(thm)],
% 15.28/2.89 [zip_derived_cl9815, zip_derived_cl5297])).
% 15.28/2.89 thf(zip_derived_cl393, plain, (~ (vptcheck @ sk__235 @ sk__237 @ sk__236)),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf(zip_derived_cl9823, plain,
% 15.28/2.89 (((vreduce @ vq1 @ sk__234)
% 15.28/2.89 != (vsomeQuery @ (vgetQuery @ (vreduce @ vq1 @ sk__234))))),
% 15.28/2.89 inference('clc', [status(thm)], [zip_derived_cl9817, zip_derived_cl393])).
% 15.28/2.89 thf(zip_derived_cl9824, plain,
% 15.28/2.89 ((((vreduce @ vq1 @ sk__234) != (vreduce @ vq1 @ sk__234))
% 15.28/2.89 | ((vreduce @ vq1 @ sk__234) = (vnoQuery)))),
% 15.28/2.89 inference('sup-', [status(thm)], [zip_derived_cl5026, zip_derived_cl9823])).
% 15.28/2.89 thf(zip_derived_cl9826, plain, (((vreduce @ vq1 @ sk__234) = (vnoQuery))),
% 15.28/2.89 inference('simplify', [status(thm)], [zip_derived_cl9824])).
% 15.28/2.89 thf('isSomeQuery-true-INV', axiom,
% 15.28/2.89 (![VOptQuery0:vOptQuery]:
% 15.28/2.89 ( ( visSomeQuery @ VOptQuery0 ) =>
% 15.28/2.89 ( ?[VwildcardName0:vQuery]:
% 15.28/2.89 ( ( VOptQuery0 ) = ( vsomeQuery @ VwildcardName0 ) ) ) ))).
% 15.28/2.89 thf(zip_derived_cl169, plain,
% 15.28/2.89 (![X0 : vOptQuery]:
% 15.28/2.89 (((X0) = (vsomeQuery @ (sk__91 @ X0))) | ~ (visSomeQuery @ X0))),
% 15.28/2.89 inference('cnf', [status(esa)], [isSomeQuery-true-INV])).
% 15.28/2.89 thf('DIFF-noQuery-someQuery', axiom,
% 15.28/2.89 (![VQuery0:vQuery]: ( ( vnoQuery ) != ( vsomeQuery @ VQuery0 ) ))).
% 15.28/2.89 thf(zip_derived_cl36, plain,
% 15.28/2.89 (![X0 : vQuery]: ((vnoQuery) != (vsomeQuery @ X0))),
% 15.28/2.89 inference('cnf', [status(esa)], [DIFF-noQuery-someQuery])).
% 15.28/2.89 thf(zip_derived_cl4977, plain,
% 15.28/2.89 (![X0 : vOptQuery]: (((vnoQuery) != (X0)) | ~ (visSomeQuery @ X0))),
% 15.28/2.89 inference('sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl36])).
% 15.28/2.89 thf(zip_derived_cl395, plain, ( (visSomeQuery @ (vreduce @ vq1 @ sk__234))),
% 15.28/2.89 inference('cnf', [status(esa)], [zf_stmt_0])).
% 15.28/2.89 thf(zip_derived_cl4983, plain, (((vnoQuery) != (vreduce @ vq1 @ sk__234))),
% 15.28/2.89 inference('sup+', [status(thm)], [zip_derived_cl4977, zip_derived_cl395])).
% 15.28/2.89 thf(zip_derived_cl9827, plain, ($false),
% 15.28/2.89 inference('simplify_reflect-', [status(thm)],
% 15.28/2.89 [zip_derived_cl9826, zip_derived_cl4983])).
% 15.28/2.89
% 15.28/2.89 % SZS output end Refutation
% 15.28/2.89
% 15.28/2.89
% 15.28/2.89 % Terminating...
% 15.98/3.02 % Runner terminated.
% 15.98/3.02 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------