%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM287_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.gp6Blu40zV true
% Computer : n001.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 89.90s 13.51s
% Output : Refutation 89.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.15 % Problem : COM287_1 : TPTP v9.3.0. Released v9.3.0.
% 0.10/0.16 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.gp6Blu40zV true
% 0.19/0.39 % Computer : n001.cluster.edu
% 0.19/0.39 % Model : x86_64 x86_64
% 0.19/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.39 % Memory : 8042.1875MB
% 0.19/0.39 % OS : Linux 3.10.0-693.el7.x86_64
% 0.19/0.39 % CPULimit : 300
% 0.19/0.39 % WCLimit : 300
% 0.19/0.39 % DateTime : Mon May 4 20:21:18 EDT 2026
% 0.19/0.39 % CPUTime :
% 0.19/0.39 % Running portfolio for 300 s
% 0.19/0.39 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.39 % Number of cores: 8
% 0.19/0.39 % Python version: Python 3.6.8
% 0.19/0.40 % Running in FO mode
% 0.59/0.70 % Total configuration time : 435
% 0.59/0.70 % Estimated wc time : 1092
% 0.59/0.70 % Estimated cpu time (7 cpus) : 156.0
% 0.59/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.59/0.77 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.59/0.78 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.59/0.79 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.61/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.61/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.61/0.81 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 89.90/13.51 % Solved by fo/fo3_bce.sh.
% 89.90/13.51 % BCE start: 400
% 89.90/13.51 % BCE eliminated: 0
% 89.90/13.51 % PE start: 400
% 89.90/13.51 logic: eq
% 89.90/13.51 % PE eliminated: -44
% 89.90/13.51 % done 5739 iterations in 12.719s
% 89.90/13.51 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 89.90/13.51 % SZS output start Refutation
% 89.90/13.51 thf(vOptQuery_type, type, vOptQuery: $tType).
% 89.90/13.51 thf(vQuery_type, type, vQuery: $tType).
% 89.90/13.51 thf(vTStore_type, type, vTStore: $tType).
% 89.90/13.51 thf(vTable_type, type, vTable: $tType).
% 89.90/13.51 thf(vTTContext_type, type, vTTContext: $tType).
% 89.90/13.51 thf(vTType_type, type, vTType: $tType).
% 89.90/13.51 thf(vSelect_type, type, vSelect: $tType).
% 89.90/13.51 thf(vName_type, type, vName: $tType).
% 89.90/13.51 thf(vPred_type, type, vPred: $tType).
% 89.90/13.51 thf(sk__90_type, type, sk__90: vQuery > vPred).
% 89.90/13.51 thf(vtvalue_type, type, vtvalue: vTable > vQuery).
% 89.90/13.51 thf(sk__124_type, type, sk__124: vQuery > vTable).
% 89.90/13.51 thf(sk__235_type, type, sk__235: vTable).
% 89.90/13.51 thf(vq2_type, type, vq2: vQuery).
% 89.90/13.51 thf(vptcheck_type, type, vptcheck: vTTContext > vQuery > vTType > $o).
% 89.90/13.51 thf(sk__85_type, type, sk__85: vQuery > vQuery).
% 89.90/13.51 thf(vnoQuery_type, type, vnoQuery: vOptQuery).
% 89.90/13.51 thf(sk__238_type, type, sk__238: vTType).
% 89.90/13.51 thf(sk__91_type, type, sk__91: vOptQuery > vQuery).
% 89.90/13.51 thf(vDifference_type, type, vDifference: vQuery > vQuery > vQuery).
% 89.90/13.51 thf(visSomeQuery_type, type, visSomeQuery: vOptQuery > $o).
% 89.90/13.51 thf(sk__83_type, type, sk__83: vQuery > vQuery).
% 89.90/13.51 thf(vreduce_type, type, vreduce: vQuery > vTStore > vOptQuery).
% 89.90/13.51 thf(vq1_type, type, vq1: vQuery).
% 89.90/13.51 thf(sk__236_type, type, sk__236: vTTContext).
% 89.90/13.51 thf(vUnion_type, type, vUnion: vQuery > vQuery > vQuery).
% 89.90/13.51 thf(sk__88_type, type, sk__88: vQuery > vSelect).
% 89.90/13.51 thf(vgetQuery_type, type, vgetQuery: vOptQuery > vQuery).
% 89.90/13.51 thf(sk__16_type, type, sk__16: vOptQuery > vQuery).
% 89.90/13.51 thf(visValue_type, type, visValue: vQuery > $o).
% 89.90/13.51 thf(vIntersection_type, type, vIntersection: vQuery > vQuery > vQuery).
% 89.90/13.51 thf(sk__237_type, type, sk__237: vTStore).
% 89.90/13.51 thf(sk__86_type, type, sk__86: vQuery > vQuery).
% 89.90/13.51 thf(sk__82_type, type, sk__82: vQuery > vQuery).
% 89.90/13.51 thf(sk__234_type, type, sk__234: vQuery).
% 89.90/13.51 thf(sk__84_type, type, sk__84: vQuery > vQuery).
% 89.90/13.51 thf(vstoreContextConsistent_type, type, vstoreContextConsistent: vTStore >
% 89.90/13.51 vTTContext > $o).
% 89.90/13.51 thf(vsomeQuery_type, type, vsomeQuery: vQuery > vOptQuery).
% 89.90/13.51 thf(sk__89_type, type, sk__89: vQuery > vName).
% 89.90/13.51 thf(sk__87_type, type, sk__87: vQuery > vQuery).
% 89.90/13.51 thf(vselectFromWhere_type, type, vselectFromWhere: vSelect > vName > vPred > vQuery).
% 89.90/13.51 thf('Preservation-Difference-tvalue-q2-isSomeQuery-True', conjecture,
% 89.90/13.51 (![Vqr:vQuery,Vt:vTable,Vttc:vTTContext,Vts:vTStore,Vtt:vTType]:
% 89.90/13.51 ( ( ( visSomeQuery @ ( vreduce @ vq2 @ Vts ) ) &
% 89.90/13.51 ( ![Vt200:vTable]: ( ( vq2 ) != ( vtvalue @ Vt200 ) ) ) &
% 89.90/13.51 ( ( vq1 ) = ( vtvalue @ Vt ) ) &
% 89.90/13.51 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 89.90/13.51 ( vptcheck @ Vttc @ ( vDifference @ vq1 @ vq2 ) @ Vtt ) &
% 89.90/13.51 ( ( vreduce @ ( vDifference @ vq1 @ vq2 ) @ Vts ) =
% 89.90/13.51 ( vsomeQuery @ Vqr ) ) ) =>
% 89.90/13.51 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 89.90/13.51 thf(zf_stmt_0, negated_conjecture,
% 89.90/13.51 (~( ![Vqr:vQuery,Vt:vTable,Vttc:vTTContext,Vts:vTStore,Vtt:vTType]:
% 89.90/13.51 ( ( ( visSomeQuery @ ( vreduce @ vq2 @ Vts ) ) &
% 89.90/13.51 ( ![Vt200:vTable]: ( ( vq2 ) != ( vtvalue @ Vt200 ) ) ) &
% 89.90/13.51 ( ( vq1 ) = ( vtvalue @ Vt ) ) &
% 89.90/13.51 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 89.90/13.51 ( vptcheck @ Vttc @ ( vDifference @ vq1 @ vq2 ) @ Vtt ) &
% 89.90/13.51 ( ( vreduce @ ( vDifference @ vq1 @ vq2 ) @ Vts ) =
% 89.90/13.51 ( vsomeQuery @ Vqr ) ) ) =>
% 89.90/13.51 ( vptcheck @ Vttc @ Vqr @ Vtt ) ) )),
% 89.90/13.51 inference('cnf.neg', [status(esa)],
% 89.90/13.51 [Preservation-Difference-tvalue-q2-isSomeQuery-True])).
% 89.90/13.51 thf(zip_derived_cl393, plain, (~ (vptcheck @ sk__236 @ sk__234 @ sk__238)),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(zip_derived_cl398, plain,
% 89.90/13.51 ( (vstoreContextConsistent @ sk__237 @ sk__236)),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(TDifference_inv2, axiom,
% 89.90/13.51 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 89.90/13.51 ( ( vptcheck @ VTTC @ ( vDifference @ Vq1 @ Vq2 ) @ VTT ) =>
% 89.90/13.51 ( vptcheck @ VTTC @ Vq2 @ VTT ) ))).
% 89.90/13.51 thf(zip_derived_cl390, plain,
% 89.90/13.51 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 89.90/13.51 ( (vptcheck @ X0 @ X1 @ X2)
% 89.90/13.51 | ~ (vptcheck @ X0 @ (vDifference @ X3 @ X1) @ X2))),
% 89.90/13.51 inference('cnf', [status(esa)], [TDifference_inv2])).
% 89.90/13.51 thf(zip_derived_cl394, plain,
% 89.90/13.51 ( (vptcheck @ sk__236 @ (vDifference @ vq1 @ vq2) @ sk__238)),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(zip_derived_cl5339, plain, ( (vptcheck @ sk__236 @ vq2 @ sk__238)),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl390, zip_derived_cl394])).
% 89.90/13.51 thf('Preservation-Difference-IH1', axiom,
% 89.90/13.51 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 89.90/13.51 ( ( ( vstoreContextConsistent @ Vts @ Vttc ) &
% 89.90/13.51 ( vptcheck @ Vttc @ vq2 @ Vtt ) &
% 89.90/13.51 ( ( vreduce @ vq2 @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 89.90/13.51 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 89.90/13.51 thf(zip_derived_cl392, plain,
% 89.90/13.51 (![X0 : vTTContext, X1 : vTType, X2 : vTStore, X3 : vQuery]:
% 89.90/13.51 (~ (vptcheck @ X0 @ vq2 @ X1)
% 89.90/13.51 | ~ (vstoreContextConsistent @ X2 @ X0)
% 89.90/13.51 | ((vreduce @ vq2 @ X2) != (vsomeQuery @ X3))
% 89.90/13.51 | (vptcheck @ X0 @ X3 @ X1))),
% 89.90/13.51 inference('cnf', [status(esa)], [Preservation-Difference-IH1])).
% 89.90/13.51 thf(zip_derived_cl5569, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vTStore]:
% 89.90/13.51 ( (vptcheck @ sk__236 @ X0 @ sk__238)
% 89.90/13.51 | ((vreduce @ vq2 @ X1) != (vsomeQuery @ X0))
% 89.90/13.51 | ~ (vstoreContextConsistent @ X1 @ sk__236))),
% 89.90/13.51 inference('sup-', [status(thm)], [zip_derived_cl5339, zip_derived_cl392])).
% 89.90/13.51 thf(zip_derived_cl5571, plain,
% 89.90/13.51 (![X0 : vQuery]:
% 89.90/13.51 (((vreduce @ vq2 @ sk__237) != (vsomeQuery @ X0))
% 89.90/13.51 | (vptcheck @ sk__236 @ X0 @ sk__238))),
% 89.90/13.51 inference('sup-', [status(thm)], [zip_derived_cl398, zip_derived_cl5569])).
% 89.90/13.51 thf(zip_derived_cl397, plain, (((vq1) = (vtvalue @ sk__235))),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf('reduce-15', axiom,
% 89.90/13.51 (![Vt:vTable,Vq2:vQuery,Vts:vTStore]:
% 89.90/13.51 ( ( ( ![Vt100:vTable,Vt200:vTable]:
% 89.90/13.51 ( ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) | ( ( Vt ) != ( Vt100 ) ) ) ) &
% 89.90/13.51 ( visSomeQuery @ ( vreduce @ Vq2 @ Vts ) ) ) =>
% 89.90/13.51 ( ( vreduce @ ( vDifference @ ( vtvalue @ Vt ) @ Vq2 ) @ Vts ) =
% 89.90/13.51 ( vsomeQuery @
% 89.90/13.51 ( vDifference @
% 89.90/13.51 ( vtvalue @ Vt ) @ ( vgetQuery @ ( vreduce @ Vq2 @ Vts ) ) ) ) ) ))).
% 89.90/13.51 thf(zip_derived_cl223, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vTStore, X2 : vTable]:
% 89.90/13.51 (((X0) = (vtvalue @ (sk__124 @ X0)))
% 89.90/13.51 | ~ (visSomeQuery @ (vreduce @ X0 @ X1))
% 89.90/13.51 | ((vreduce @ (vDifference @ (vtvalue @ X2) @ X0) @ X1)
% 89.90/13.51 = (vsomeQuery @
% 89.90/13.51 (vDifference @ (vtvalue @ X2) @
% 89.90/13.51 (vgetQuery @ (vreduce @ X0 @ X1))))))),
% 89.90/13.51 inference('cnf', [status(esa)], [reduce-15])).
% 89.90/13.51 thf(zip_derived_cl6069, plain,
% 89.90/13.51 (![X0 : vTStore, X1 : vQuery]:
% 89.90/13.51 (((vreduce @ (vDifference @ vq1 @ X1) @ X0)
% 89.90/13.51 = (vsomeQuery @
% 89.90/13.51 (vDifference @ (vtvalue @ sk__235) @
% 89.90/13.51 (vgetQuery @ (vreduce @ X1 @ X0)))))
% 89.90/13.51 | ~ (visSomeQuery @ (vreduce @ X1 @ X0))
% 89.90/13.51 | ((X1) = (vtvalue @ (sk__124 @ X1))))),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl397, zip_derived_cl223])).
% 89.90/13.51 thf(zip_derived_cl397, plain, (((vq1) = (vtvalue @ sk__235))),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(zip_derived_cl6071, plain,
% 89.90/13.51 (![X0 : vTStore, X1 : vQuery]:
% 89.90/13.51 (((vreduce @ (vDifference @ vq1 @ X1) @ X0)
% 89.90/13.51 = (vsomeQuery @
% 89.90/13.51 (vDifference @ vq1 @ (vgetQuery @ (vreduce @ X1 @ X0)))))
% 89.90/13.51 | ~ (visSomeQuery @ (vreduce @ X1 @ X0))
% 89.90/13.51 | ((X1) = (vtvalue @ (sk__124 @ X1))))),
% 89.90/13.51 inference('demod', [status(thm)], [zip_derived_cl6069, zip_derived_cl397])).
% 89.90/13.51 thf(zip_derived_cl399, plain,
% 89.90/13.51 (((vreduce @ (vDifference @ vq1 @ vq2) @ sk__237)
% 89.90/13.51 = (vsomeQuery @ sk__234))),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(zip_derived_cl48156, plain,
% 89.90/13.51 ((((vsomeQuery @
% 89.90/13.51 (vDifference @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))
% 89.90/13.51 = (vsomeQuery @ sk__234))
% 89.90/13.51 | ((vq2) = (vtvalue @ (sk__124 @ vq2)))
% 89.90/13.51 | ~ (visSomeQuery @ (vreduce @ vq2 @ sk__237)))),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl6071, zip_derived_cl399])).
% 89.90/13.51 thf(zip_derived_cl395, plain, ( (visSomeQuery @ (vreduce @ vq2 @ sk__237))),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(zip_derived_cl48286, plain,
% 89.90/13.51 ((((vsomeQuery @
% 89.90/13.51 (vDifference @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))
% 89.90/13.51 = (vsomeQuery @ sk__234))
% 89.90/13.51 | ((vq2) = (vtvalue @ (sk__124 @ vq2))))),
% 89.90/13.51 inference('demod', [status(thm)],
% 89.90/13.51 [zip_derived_cl48156, zip_derived_cl395])).
% 89.90/13.51 thf(zip_derived_cl396, plain, (![X0 : vTable]: ((vq2) != (vtvalue @ X0))),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(zip_derived_cl48287, plain,
% 89.90/13.51 (((vsomeQuery @
% 89.90/13.51 (vDifference @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))
% 89.90/13.51 = (vsomeQuery @ sk__234))),
% 89.90/13.51 inference('simplify_reflect-', [status(thm)],
% 89.90/13.51 [zip_derived_cl48286, zip_derived_cl396])).
% 89.90/13.51 thf('getQuery-0', axiom,
% 89.90/13.51 (![Vq:vQuery]: ( ( vgetQuery @ ( vsomeQuery @ Vq ) ) = ( Vq ) ))).
% 89.90/13.51 thf(zip_derived_cl47, plain,
% 89.90/13.51 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 89.90/13.51 inference('cnf', [status(esa)], [getQuery-0])).
% 89.90/13.51 thf(zip_derived_cl48290, plain,
% 89.90/13.51 (((vgetQuery @ (vsomeQuery @ sk__234))
% 89.90/13.51 = (vDifference @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl48287, zip_derived_cl47])).
% 89.90/13.51 thf(zip_derived_cl47, plain,
% 89.90/13.51 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 89.90/13.51 inference('cnf', [status(esa)], [getQuery-0])).
% 89.90/13.51 thf(zip_derived_cl48312, plain,
% 89.90/13.51 (((sk__234)
% 89.90/13.51 = (vDifference @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))),
% 89.90/13.51 inference('demod', [status(thm)], [zip_derived_cl48290, zip_derived_cl47])).
% 89.90/13.51 thf('isValue-false-INV', axiom,
% 89.90/13.51 (![VQuery0:vQuery]:
% 89.90/13.51 ( ( ~( visValue @ VQuery0 ) ) =>
% 89.90/13.51 ( ( ?[VwildcardName0:vSelect,VwildcardName1:vName,VwildcardName2:vPred]:
% 89.90/13.51 ( ( VQuery0 ) =
% 89.90/13.51 ( vselectFromWhere @
% 89.90/13.51 VwildcardName0 @ VwildcardName1 @ VwildcardName2 ) ) ) |
% 89.90/13.51 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 89.90/13.51 ( ( VQuery0 ) = ( vUnion @ VwildcardName0 @ VwildcardName1 ) ) ) |
% 89.90/13.51 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 89.90/13.51 ( ( VQuery0 ) = ( vIntersection @ VwildcardName0 @ VwildcardName1 ) ) ) |
% 89.90/13.51 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 89.90/13.51 ( ( VQuery0 ) = ( vDifference @ VwildcardName0 @ VwildcardName1 ) ) ) ) ))).
% 89.90/13.51 thf(zip_derived_cl166, plain,
% 89.90/13.51 (![X0 : vQuery]:
% 89.90/13.51 (((X0) = (vDifference @ (sk__82 @ X0) @ (sk__83 @ X0)))
% 89.90/13.51 | ((X0) = (vIntersection @ (sk__84 @ X0) @ (sk__85 @ X0)))
% 89.90/13.51 | ((X0) = (vUnion @ (sk__86 @ X0) @ (sk__87 @ X0)))
% 89.90/13.51 | ((X0)
% 89.90/13.51 = (vselectFromWhere @ (sk__88 @ X0) @ (sk__89 @ X0) @
% 89.90/13.51 (sk__90 @ X0)))
% 89.90/13.51 | (visValue @ X0))),
% 89.90/13.51 inference('cnf', [status(esa)], [isValue-false-INV])).
% 89.90/13.51 thf('isValue-4', axiom,
% 89.90/13.51 (![VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 89.90/13.51 ( ~( visValue @ ( vDifference @ VwildcardName0 @ VwildcardName1 ) ) ))).
% 89.90/13.51 thf(zip_derived_cl164, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery]: ~ (visValue @ (vDifference @ X0 @ X1))),
% 89.90/13.51 inference('cnf', [status(esa)], [isValue-4])).
% 89.90/13.51 thf(zip_derived_cl1418, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery]:
% 89.90/13.51 (((vDifference @ X1 @ X0)
% 89.90/13.51 = (vselectFromWhere @ (sk__88 @ (vDifference @ X1 @ X0)) @
% 89.90/13.51 (sk__89 @ (vDifference @ X1 @ X0)) @
% 89.90/13.51 (sk__90 @ (vDifference @ X1 @ X0))))
% 89.90/13.51 | ((vDifference @ X1 @ X0)
% 89.90/13.51 = (vUnion @ (sk__86 @ (vDifference @ X1 @ X0)) @
% 89.90/13.51 (sk__87 @ (vDifference @ X1 @ X0))))
% 89.90/13.51 | ((vDifference @ X1 @ X0)
% 89.90/13.51 = (vIntersection @ (sk__84 @ (vDifference @ X1 @ X0)) @
% 89.90/13.51 (sk__85 @ (vDifference @ X1 @ X0))))
% 89.90/13.51 | ((vDifference @ X1 @ X0)
% 89.90/13.51 = (vDifference @ (sk__82 @ (vDifference @ X1 @ X0)) @
% 89.90/13.51 (sk__83 @ (vDifference @ X1 @ X0)))))),
% 89.90/13.51 inference('dp-resolution', [status(thm)],
% 89.90/13.51 [zip_derived_cl166, zip_derived_cl164])).
% 89.90/13.51 thf('DIFF-Intersection-Difference', axiom,
% 89.90/13.51 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 89.90/13.51 ( ( vIntersection @ VQuery0 @ VQuery1 ) !=
% 89.90/13.51 ( vDifference @ VQuery2 @ VQuery3 ) ))).
% 89.90/13.51 thf(zip_derived_cl21, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 89.90/13.51 ((vIntersection @ X2 @ X3) != (vDifference @ X0 @ X1))),
% 89.90/13.51 inference('cnf', [status(esa)], [DIFF-Intersection-Difference])).
% 89.90/13.51 thf('DIFF-Union-Difference', axiom,
% 89.90/13.51 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 89.90/13.51 ( ( vUnion @ VQuery0 @ VQuery1 ) != ( vDifference @ VQuery2 @ VQuery3 ) ))).
% 89.90/13.51 thf(zip_derived_cl20, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 89.90/13.51 ((vUnion @ X2 @ X3) != (vDifference @ X0 @ X1))),
% 89.90/13.51 inference('cnf', [status(esa)], [DIFF-Union-Difference])).
% 89.90/13.51 thf('DIFF-selectFromWhere-Difference', axiom,
% 89.90/13.51 (![VName0:vName,VPred0:vPred,VSelect0:vSelect,VQuery1:vQuery,VQuery0:vQuery]:
% 89.90/13.51 ( ( vselectFromWhere @ VSelect0 @ VName0 @ VPred0 ) !=
% 89.90/13.51 ( vDifference @ VQuery0 @ VQuery1 ) ))).
% 89.90/13.51 thf(zip_derived_cl18, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery, X2 : vSelect, X3 : vName, X4 : vPred]:
% 89.90/13.51 ((vselectFromWhere @ X2 @ X3 @ X4) != (vDifference @ X0 @ X1))),
% 89.90/13.51 inference('cnf', [status(esa)], [DIFF-selectFromWhere-Difference])).
% 89.90/13.51 thf(zip_derived_cl10774, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery]:
% 89.90/13.51 ((vDifference @ X1 @ X0)
% 89.90/13.51 = (vDifference @ (sk__82 @ (vDifference @ X1 @ X0)) @
% 89.90/13.51 (sk__83 @ (vDifference @ X1 @ X0))))),
% 89.90/13.51 inference('simplify_reflect-', [status(thm)],
% 89.90/13.51 [zip_derived_cl1418, zip_derived_cl21, zip_derived_cl20,
% 89.90/13.51 zip_derived_cl18])).
% 89.90/13.51 thf(zip_derived_cl10774, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery]:
% 89.90/13.51 ((vDifference @ X1 @ X0)
% 89.90/13.51 = (vDifference @ (sk__82 @ (vDifference @ X1 @ X0)) @
% 89.90/13.51 (sk__83 @ (vDifference @ X1 @ X0))))),
% 89.90/13.51 inference('simplify_reflect-', [status(thm)],
% 89.90/13.51 [zip_derived_cl1418, zip_derived_cl21, zip_derived_cl20,
% 89.90/13.51 zip_derived_cl18])).
% 89.90/13.51 thf('EQ-Difference', axiom,
% 89.90/13.51 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 89.90/13.51 ( ( ( vDifference @ VQuery0 @ VQuery1 ) =
% 89.90/13.51 ( vDifference @ VQuery2 @ VQuery3 ) ) =>
% 89.90/13.51 ( ( ( VQuery0 ) = ( VQuery2 ) ) & ( ( VQuery1 ) = ( VQuery3 ) ) ) ))).
% 89.90/13.51 thf(zip_derived_cl10, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 89.90/13.51 (((X1) = (X0)) | ((vDifference @ X1 @ X3) != (vDifference @ X0 @ X2)))),
% 89.90/13.51 inference('cnf', [status(esa)], [EQ-Difference])).
% 89.90/13.51 thf(zip_derived_cl10775, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 89.90/13.51 (((vDifference @ X3 @ X2) != (vDifference @ X1 @ X0))
% 89.90/13.51 | ((X3) = (sk__82 @ (vDifference @ X1 @ X0))))),
% 89.90/13.51 inference('sup-', [status(thm)], [zip_derived_cl10774, zip_derived_cl10])).
% 89.90/13.51 thf(zip_derived_cl11248, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery]: ((X0) = (sk__82 @ (vDifference @ X0 @ X1)))),
% 89.90/13.51 inference('eq_res', [status(thm)], [zip_derived_cl10775])).
% 89.90/13.51 thf(zip_derived_cl11327, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery]:
% 89.90/13.51 ((vDifference @ X1 @ X0)
% 89.90/13.51 = (vDifference @ X1 @ (sk__83 @ (vDifference @ X1 @ X0))))),
% 89.90/13.51 inference('demod', [status(thm)],
% 89.90/13.51 [zip_derived_cl10774, zip_derived_cl11248])).
% 89.90/13.51 thf(zip_derived_cl11, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 89.90/13.51 (((X1) = (X0)) | ((vDifference @ X3 @ X1) != (vDifference @ X2 @ X0)))),
% 89.90/13.51 inference('cnf', [status(esa)], [EQ-Difference])).
% 89.90/13.51 thf(zip_derived_cl22026, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 89.90/13.51 (((vDifference @ X3 @ X2) != (vDifference @ X1 @ X0))
% 89.90/13.51 | ((X2) = (sk__83 @ (vDifference @ X1 @ X0))))),
% 89.90/13.51 inference('sup-', [status(thm)], [zip_derived_cl11327, zip_derived_cl11])).
% 89.90/13.51 thf(zip_derived_cl22177, plain,
% 89.90/13.51 (![X0 : vQuery, X1 : vQuery]: ((X0) = (sk__83 @ (vDifference @ X1 @ X0)))),
% 89.90/13.51 inference('eq_res', [status(thm)], [zip_derived_cl22026])).
% 89.90/13.51 thf(zip_derived_cl49982, plain,
% 89.90/13.51 (((vgetQuery @ (vreduce @ vq2 @ sk__237)) = (sk__83 @ sk__234))),
% 89.90/13.51 inference('sup+', [status(thm)],
% 89.90/13.51 [zip_derived_cl48312, zip_derived_cl22177])).
% 89.90/13.51 thf('dom-OptQuery', axiom,
% 89.90/13.51 (![VX:vOptQuery]:
% 89.90/13.51 ( ( ?[VQuery0:vQuery]: ( ( VX ) = ( vsomeQuery @ VQuery0 ) ) ) |
% 89.90/13.51 ( ( VX ) = ( vnoQuery ) ) ))).
% 89.90/13.51 thf(zip_derived_cl34, plain,
% 89.90/13.51 (![X0 : vOptQuery]:
% 89.90/13.51 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 89.90/13.51 inference('cnf', [status(esa)], [dom-OptQuery])).
% 89.90/13.51 thf(zip_derived_cl47, plain,
% 89.90/13.51 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 89.90/13.51 inference('cnf', [status(esa)], [getQuery-0])).
% 89.90/13.51 thf(zip_derived_cl5025, plain,
% 89.90/13.51 (![X0 : vOptQuery]:
% 89.90/13.51 (((vgetQuery @ X0) = (sk__16 @ X0)) | ((X0) = (vnoQuery)))),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl34, zip_derived_cl47])).
% 89.90/13.51 thf(zip_derived_cl34, plain,
% 89.90/13.51 (![X0 : vOptQuery]:
% 89.90/13.51 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 89.90/13.51 inference('cnf', [status(esa)], [dom-OptQuery])).
% 89.90/13.51 thf(zip_derived_cl5053, plain,
% 89.90/13.51 (![X0 : vOptQuery]:
% 89.90/13.51 (((X0) = (vsomeQuery @ (vgetQuery @ X0)))
% 89.90/13.51 | ((X0) = (vnoQuery))
% 89.90/13.51 | ((X0) = (vnoQuery)))),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl5025, zip_derived_cl34])).
% 89.90/13.51 thf(zip_derived_cl5056, plain,
% 89.90/13.51 (![X0 : vOptQuery]:
% 89.90/13.51 (((X0) = (vnoQuery)) | ((X0) = (vsomeQuery @ (vgetQuery @ X0))))),
% 89.90/13.51 inference('simplify', [status(thm)], [zip_derived_cl5053])).
% 89.90/13.51 thf(zip_derived_cl52086, plain,
% 89.90/13.51 ((((vreduce @ vq2 @ sk__237) = (vsomeQuery @ (sk__83 @ sk__234)))
% 89.90/13.51 | ((vreduce @ vq2 @ sk__237) = (vnoQuery)))),
% 89.90/13.51 inference('sup+', [status(thm)],
% 89.90/13.51 [zip_derived_cl49982, zip_derived_cl5056])).
% 89.90/13.51 thf('isSomeQuery-true-INV', axiom,
% 89.90/13.51 (![VOptQuery0:vOptQuery]:
% 89.90/13.51 ( ( visSomeQuery @ VOptQuery0 ) =>
% 89.90/13.51 ( ?[VwildcardName0:vQuery]:
% 89.90/13.51 ( ( VOptQuery0 ) = ( vsomeQuery @ VwildcardName0 ) ) ) ))).
% 89.90/13.51 thf(zip_derived_cl169, plain,
% 89.90/13.51 (![X0 : vOptQuery]:
% 89.90/13.51 (((X0) = (vsomeQuery @ (sk__91 @ X0))) | ~ (visSomeQuery @ X0))),
% 89.90/13.51 inference('cnf', [status(esa)], [isSomeQuery-true-INV])).
% 89.90/13.51 thf('DIFF-noQuery-someQuery', axiom,
% 89.90/13.51 (![VQuery0:vQuery]: ( ( vnoQuery ) != ( vsomeQuery @ VQuery0 ) ))).
% 89.90/13.51 thf(zip_derived_cl36, plain,
% 89.90/13.51 (![X0 : vQuery]: ((vnoQuery) != (vsomeQuery @ X0))),
% 89.90/13.51 inference('cnf', [status(esa)], [DIFF-noQuery-someQuery])).
% 89.90/13.51 thf(zip_derived_cl5005, plain,
% 89.90/13.51 (![X0 : vOptQuery]: (((vnoQuery) != (X0)) | ~ (visSomeQuery @ X0))),
% 89.90/13.51 inference('sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl36])).
% 89.90/13.51 thf(zip_derived_cl395, plain, ( (visSomeQuery @ (vreduce @ vq2 @ sk__237))),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(zip_derived_cl5011, plain, (((vnoQuery) != (vreduce @ vq2 @ sk__237))),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl5005, zip_derived_cl395])).
% 89.90/13.51 thf(zip_derived_cl52095, plain,
% 89.90/13.51 (((vreduce @ vq2 @ sk__237) = (vsomeQuery @ (sk__83 @ sk__234)))),
% 89.90/13.51 inference('simplify_reflect-', [status(thm)],
% 89.90/13.51 [zip_derived_cl52086, zip_derived_cl5011])).
% 89.90/13.51 thf(zip_derived_cl52596, plain,
% 89.90/13.51 (![X0 : vQuery]:
% 89.90/13.51 (((vsomeQuery @ (sk__83 @ sk__234)) != (vsomeQuery @ X0))
% 89.90/13.51 | (vptcheck @ sk__236 @ X0 @ sk__238))),
% 89.90/13.51 inference('demod', [status(thm)],
% 89.90/13.51 [zip_derived_cl5571, zip_derived_cl52095])).
% 89.90/13.51 thf(zip_derived_cl48312, plain,
% 89.90/13.51 (((sk__234)
% 89.90/13.51 = (vDifference @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__237))))),
% 89.90/13.51 inference('demod', [status(thm)], [zip_derived_cl48290, zip_derived_cl47])).
% 89.90/13.51 thf(zip_derived_cl49982, plain,
% 89.90/13.51 (((vgetQuery @ (vreduce @ vq2 @ sk__237)) = (sk__83 @ sk__234))),
% 89.90/13.51 inference('sup+', [status(thm)],
% 89.90/13.51 [zip_derived_cl48312, zip_derived_cl22177])).
% 89.90/13.51 thf(zip_derived_cl52085, plain,
% 89.90/13.51 (((sk__234) = (vDifference @ vq1 @ (sk__83 @ sk__234)))),
% 89.90/13.51 inference('demod', [status(thm)],
% 89.90/13.51 [zip_derived_cl48312, zip_derived_cl49982])).
% 89.90/13.51 thf(TDifference, axiom,
% 89.90/13.51 (![VTTC:vTTContext,Vq1:vQuery,VTT:vTType,Vq2:vQuery]:
% 89.90/13.51 ( ( ( vptcheck @ VTTC @ Vq1 @ VTT ) & ( vptcheck @ VTTC @ Vq2 @ VTT ) ) =>
% 89.90/13.51 ( vptcheck @ VTTC @ ( vDifference @ Vq1 @ Vq2 ) @ VTT ) ))).
% 89.90/13.51 thf(zip_derived_cl380, plain,
% 89.90/13.51 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 89.90/13.51 (~ (vptcheck @ X0 @ X1 @ X2)
% 89.90/13.51 | ~ (vptcheck @ X0 @ X3 @ X2)
% 89.90/13.51 | (vptcheck @ X0 @ (vDifference @ X1 @ X3) @ X2))),
% 89.90/13.51 inference('cnf', [status(esa)], [TDifference])).
% 89.90/13.51 thf(zip_derived_cl52239, plain,
% 89.90/13.51 (![X0 : vTType, X1 : vTTContext]:
% 89.90/13.51 ( (vptcheck @ X1 @ sk__234 @ X0)
% 89.90/13.51 | ~ (vptcheck @ X1 @ (sk__83 @ sk__234) @ X0)
% 89.90/13.51 | ~ (vptcheck @ X1 @ vq1 @ X0))),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl52085, zip_derived_cl380])).
% 89.90/13.51 thf(zip_derived_cl67352, plain,
% 89.90/13.51 ((((vsomeQuery @ (sk__83 @ sk__234)) != (vsomeQuery @ (sk__83 @ sk__234)))
% 89.90/13.51 | ~ (vptcheck @ sk__236 @ vq1 @ sk__238)
% 89.90/13.51 | (vptcheck @ sk__236 @ sk__234 @ sk__238))),
% 89.90/13.51 inference('sup-', [status(thm)],
% 89.90/13.51 [zip_derived_cl52596, zip_derived_cl52239])).
% 89.90/13.51 thf(TDifference_inv1, axiom,
% 89.90/13.51 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 89.90/13.51 ( ( vptcheck @ VTTC @ ( vDifference @ Vq1 @ Vq2 ) @ VTT ) =>
% 89.90/13.51 ( vptcheck @ VTTC @ Vq1 @ VTT ) ))).
% 89.90/13.51 thf(zip_derived_cl389, plain,
% 89.90/13.51 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 89.90/13.51 ( (vptcheck @ X0 @ X1 @ X2)
% 89.90/13.51 | ~ (vptcheck @ X0 @ (vDifference @ X1 @ X3) @ X2))),
% 89.90/13.51 inference('cnf', [status(esa)], [TDifference_inv1])).
% 89.90/13.51 thf(zip_derived_cl394, plain,
% 89.90/13.51 ( (vptcheck @ sk__236 @ (vDifference @ vq1 @ vq2) @ sk__238)),
% 89.90/13.51 inference('cnf', [status(esa)], [zf_stmt_0])).
% 89.90/13.51 thf(zip_derived_cl5326, plain, ( (vptcheck @ sk__236 @ vq1 @ sk__238)),
% 89.90/13.51 inference('sup+', [status(thm)], [zip_derived_cl389, zip_derived_cl394])).
% 89.90/13.51 thf(zip_derived_cl67353, plain,
% 89.90/13.51 ((((vsomeQuery @ (sk__83 @ sk__234)) != (vsomeQuery @ (sk__83 @ sk__234)))
% 89.90/13.51 | (vptcheck @ sk__236 @ sk__234 @ sk__238))),
% 89.90/13.51 inference('demod', [status(thm)],
% 89.90/13.51 [zip_derived_cl67352, zip_derived_cl5326])).
% 89.90/13.51 thf(zip_derived_cl67354, plain, ( (vptcheck @ sk__236 @ sk__234 @ sk__238)),
% 89.90/13.51 inference('simplify', [status(thm)], [zip_derived_cl67353])).
% 89.90/13.51 thf(zip_derived_cl67357, plain, ($false),
% 89.90/13.51 inference('demod', [status(thm)],
% 89.90/13.51 [zip_derived_cl393, zip_derived_cl67354])).
% 89.90/13.51
% 89.90/13.51 % SZS output end Refutation
% 89.90/13.51
% 89.90/13.51
% 89.90/13.51 % Terminating...
% 89.90/13.54 % Runner terminated.
% 89.90/13.55 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------