%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM295_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.CrAMWJ2rM8 true
% Computer : n022.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 68.10s 10.38s
% Output : Refutation 68.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM295_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.CrAMWJ2rM8 true
% 0.15/0.34 % Computer : n022.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 20:29:51 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.35 % Python version: Python 3.6.8
% 0.15/0.35 % Running in FO mode
% 0.54/0.65 % Total configuration time : 435
% 0.54/0.65 % Estimated wc time : 1092
% 0.54/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.54/0.75 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 68.10/10.38 % Solved by fo/fo3_bce.sh.
% 68.10/10.38 % BCE start: 417
% 68.10/10.38 % BCE eliminated: 0
% 68.10/10.38 % PE start: 417
% 68.10/10.38 logic: eq
% 68.10/10.38 % PE eliminated: -50
% 68.10/10.38 % done 5247 iterations in 9.606s
% 68.10/10.38 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 68.10/10.38 % SZS output start Refutation
% 68.10/10.38 thf(vOptQuery_type, type, vOptQuery: $tType).
% 68.10/10.38 thf(vQuery_type, type, vQuery: $tType).
% 68.10/10.38 thf(vTStore_type, type, vTStore: $tType).
% 68.10/10.38 thf(vTable_type, type, vTable: $tType).
% 68.10/10.38 thf(vTTContext_type, type, vTTContext: $tType).
% 68.10/10.38 thf(vTType_type, type, vTType: $tType).
% 68.10/10.38 thf(vSelect_type, type, vSelect: $tType).
% 68.10/10.38 thf(vName_type, type, vName: $tType).
% 68.10/10.38 thf(vPred_type, type, vPred: $tType).
% 68.10/10.38 thf(vtvalue_type, type, vtvalue: vTable > vQuery).
% 68.10/10.38 thf(sk__244_type, type, sk__244: vTable).
% 68.10/10.38 thf(sk__92_type, type, sk__92: vQuery > vQuery).
% 68.10/10.38 thf(sk__95_type, type, sk__95: vQuery > vQuery).
% 68.10/10.38 thf(vq2_type, type, vq2: vQuery).
% 68.10/10.38 thf(vptcheck_type, type, vptcheck: vTTContext > vQuery > vTType > $o).
% 68.10/10.38 thf(sk__109_type, type, sk__109: vQuery > vTable).
% 68.10/10.38 thf(sk__98_type, type, sk__98: vQuery > vName).
% 68.10/10.38 thf(vnoQuery_type, type, vnoQuery: vOptQuery).
% 68.10/10.38 thf(sk__96_type, type, sk__96: vQuery > vQuery).
% 68.10/10.38 thf(vDifference_type, type, vDifference: vQuery > vQuery > vQuery).
% 68.10/10.38 thf(sk__247_type, type, sk__247: vTType).
% 68.10/10.38 thf(sk__245_type, type, sk__245: vTTContext).
% 68.10/10.38 thf(visSomeQuery_type, type, visSomeQuery: vOptQuery > $o).
% 68.10/10.38 thf(sk__91_type, type, sk__91: vQuery > vQuery).
% 68.10/10.38 thf(sk__99_type, type, sk__99: vQuery > vPred).
% 68.10/10.38 thf(sk__246_type, type, sk__246: vTStore).
% 68.10/10.38 thf(vreduce_type, type, vreduce: vQuery > vTStore > vOptQuery).
% 68.10/10.38 thf(vq1_type, type, vq1: vQuery).
% 68.10/10.38 thf(sk__93_type, type, sk__93: vQuery > vQuery).
% 68.10/10.38 thf(sk__243_type, type, sk__243: vQuery).
% 68.10/10.38 thf(sk__97_type, type, sk__97: vQuery > vSelect).
% 68.10/10.38 thf(vUnion_type, type, vUnion: vQuery > vQuery > vQuery).
% 68.10/10.38 thf(vgetQuery_type, type, vgetQuery: vOptQuery > vQuery).
% 68.10/10.38 thf(visValue_type, type, visValue: vQuery > $o).
% 68.10/10.38 thf(vIntersection_type, type, vIntersection: vQuery > vQuery > vQuery).
% 68.10/10.38 thf(sk__16_type, type, sk__16: vOptQuery > vQuery).
% 68.10/10.38 thf(sk__94_type, type, sk__94: vQuery > vQuery).
% 68.10/10.38 thf(vstoreContextConsistent_type, type, vstoreContextConsistent: vTStore >
% 68.10/10.38 vTTContext > $o).
% 68.10/10.38 thf(vsomeQuery_type, type, vsomeQuery: vQuery > vOptQuery).
% 68.10/10.38 thf(sk__100_type, type, sk__100: vOptQuery > vQuery).
% 68.10/10.38 thf(vselectFromWhere_type, type, vselectFromWhere: vSelect > vName > vPred > vQuery).
% 68.10/10.38 thf('Preservation-Union-tvalue-q2-isSomeQuery-True', conjecture,
% 68.10/10.38 (![Vqr:vQuery,Vt:vTable,Vttc:vTTContext,Vts:vTStore,Vtt:vTType]:
% 68.10/10.38 ( ( ( visSomeQuery @ ( vreduce @ vq2 @ Vts ) ) &
% 68.10/10.38 ( ![Vt200:vTable]: ( ( vq2 ) != ( vtvalue @ Vt200 ) ) ) &
% 68.10/10.38 ( ( vq1 ) = ( vtvalue @ Vt ) ) &
% 68.10/10.38 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 68.10/10.38 ( vptcheck @ Vttc @ ( vUnion @ vq1 @ vq2 ) @ Vtt ) &
% 68.10/10.38 ( ( vreduce @ ( vUnion @ vq1 @ vq2 ) @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 68.10/10.38 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 68.10/10.38 thf(zf_stmt_0, negated_conjecture,
% 68.10/10.38 (~( ![Vqr:vQuery,Vt:vTable,Vttc:vTTContext,Vts:vTStore,Vtt:vTType]:
% 68.10/10.38 ( ( ( visSomeQuery @ ( vreduce @ vq2 @ Vts ) ) &
% 68.10/10.38 ( ![Vt200:vTable]: ( ( vq2 ) != ( vtvalue @ Vt200 ) ) ) &
% 68.10/10.38 ( ( vq1 ) = ( vtvalue @ Vt ) ) &
% 68.10/10.38 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 68.10/10.38 ( vptcheck @ Vttc @ ( vUnion @ vq1 @ vq2 ) @ Vtt ) &
% 68.10/10.38 ( ( vreduce @ ( vUnion @ vq1 @ vq2 ) @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 68.10/10.38 ( vptcheck @ Vttc @ Vqr @ Vtt ) ) )),
% 68.10/10.38 inference('cnf.neg', [status(esa)],
% 68.10/10.38 [Preservation-Union-tvalue-q2-isSomeQuery-True])).
% 68.10/10.38 thf(zip_derived_cl410, plain, (~ (vptcheck @ sk__245 @ sk__243 @ sk__247)),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(zip_derived_cl415, plain,
% 68.10/10.38 ( (vstoreContextConsistent @ sk__246 @ sk__245)),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(TUnion_inv2, axiom,
% 68.10/10.38 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 68.10/10.38 ( ( vptcheck @ VTTC @ ( vUnion @ Vq1 @ Vq2 ) @ VTT ) =>
% 68.10/10.38 ( vptcheck @ VTTC @ Vq2 @ VTT ) ))).
% 68.10/10.38 thf(zip_derived_cl403, plain,
% 68.10/10.38 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 68.10/10.38 ( (vptcheck @ X0 @ X1 @ X2)
% 68.10/10.38 | ~ (vptcheck @ X0 @ (vUnion @ X3 @ X1) @ X2))),
% 68.10/10.38 inference('cnf', [status(esa)], [TUnion_inv2])).
% 68.10/10.38 thf(zip_derived_cl411, plain,
% 68.10/10.38 ( (vptcheck @ sk__245 @ (vUnion @ vq1 @ vq2) @ sk__247)),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(zip_derived_cl5546, plain, ( (vptcheck @ sk__245 @ vq2 @ sk__247)),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl403, zip_derived_cl411])).
% 68.10/10.38 thf('Preservation-Union-IH1', axiom,
% 68.10/10.38 (![Vts:vTStore,Vttc:vTTContext,Vtt:vTType,Vqr:vQuery]:
% 68.10/10.38 ( ( ( vstoreContextConsistent @ Vts @ Vttc ) &
% 68.10/10.38 ( vptcheck @ Vttc @ vq2 @ Vtt ) &
% 68.10/10.38 ( ( vreduce @ vq2 @ Vts ) = ( vsomeQuery @ Vqr ) ) ) =>
% 68.10/10.38 ( vptcheck @ Vttc @ Vqr @ Vtt ) ))).
% 68.10/10.38 thf(zip_derived_cl409, plain,
% 68.10/10.38 (![X0 : vTTContext, X1 : vTType, X2 : vTStore, X3 : vQuery]:
% 68.10/10.38 (~ (vptcheck @ X0 @ vq2 @ X1)
% 68.10/10.38 | ~ (vstoreContextConsistent @ X2 @ X0)
% 68.10/10.38 | ((vreduce @ vq2 @ X2) != (vsomeQuery @ X3))
% 68.10/10.38 | (vptcheck @ X0 @ X3 @ X1))),
% 68.10/10.38 inference('cnf', [status(esa)], [Preservation-Union-IH1])).
% 68.10/10.38 thf(zip_derived_cl5822, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vTStore]:
% 68.10/10.38 ( (vptcheck @ sk__245 @ X0 @ sk__247)
% 68.10/10.38 | ((vreduce @ vq2 @ X1) != (vsomeQuery @ X0))
% 68.10/10.38 | ~ (vstoreContextConsistent @ X1 @ sk__245))),
% 68.10/10.38 inference('sup-', [status(thm)], [zip_derived_cl5546, zip_derived_cl409])).
% 68.10/10.38 thf(zip_derived_cl5824, plain,
% 68.10/10.38 (![X0 : vQuery]:
% 68.10/10.38 (((vreduce @ vq2 @ sk__246) != (vsomeQuery @ X0))
% 68.10/10.38 | (vptcheck @ sk__245 @ X0 @ sk__247))),
% 68.10/10.38 inference('sup-', [status(thm)], [zip_derived_cl415, zip_derived_cl5822])).
% 68.10/10.38 thf(zip_derived_cl414, plain, (((vq1) = (vtvalue @ sk__244))),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf('reduce-5', axiom,
% 68.10/10.38 (![Vt:vTable,Vq2:vQuery,Vts:vTStore]:
% 68.10/10.38 ( ( ( ![Vt100:vTable,Vt200:vTable]:
% 68.10/10.38 ( ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) | ( ( Vt ) != ( Vt100 ) ) ) ) &
% 68.10/10.38 ( visSomeQuery @ ( vreduce @ Vq2 @ Vts ) ) ) =>
% 68.10/10.38 ( ( vreduce @ ( vUnion @ ( vtvalue @ Vt ) @ Vq2 ) @ Vts ) =
% 68.10/10.38 ( vsomeQuery @
% 68.10/10.38 ( vUnion @
% 68.10/10.38 ( vtvalue @ Vt ) @ ( vgetQuery @ ( vreduce @ Vq2 @ Vts ) ) ) ) ) ))).
% 68.10/10.38 thf(zip_derived_cl210, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vTStore, X2 : vTable]:
% 68.10/10.38 (((X0) = (vtvalue @ (sk__109 @ X0)))
% 68.10/10.38 | ~ (visSomeQuery @ (vreduce @ X0 @ X1))
% 68.10/10.38 | ((vreduce @ (vUnion @ (vtvalue @ X2) @ X0) @ X1)
% 68.10/10.38 = (vsomeQuery @
% 68.10/10.38 (vUnion @ (vtvalue @ X2) @ (vgetQuery @ (vreduce @ X0 @ X1))))))),
% 68.10/10.38 inference('cnf', [status(esa)], [reduce-5])).
% 68.10/10.38 thf(zip_derived_cl5867, plain,
% 68.10/10.38 (![X0 : vTStore, X1 : vQuery]:
% 68.10/10.38 (((vreduce @ (vUnion @ vq1 @ X1) @ X0)
% 68.10/10.38 = (vsomeQuery @
% 68.10/10.38 (vUnion @ (vtvalue @ sk__244) @
% 68.10/10.38 (vgetQuery @ (vreduce @ X1 @ X0)))))
% 68.10/10.38 | ~ (visSomeQuery @ (vreduce @ X1 @ X0))
% 68.10/10.38 | ((X1) = (vtvalue @ (sk__109 @ X1))))),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl414, zip_derived_cl210])).
% 68.10/10.38 thf(zip_derived_cl414, plain, (((vq1) = (vtvalue @ sk__244))),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(zip_derived_cl5868, plain,
% 68.10/10.38 (![X0 : vTStore, X1 : vQuery]:
% 68.10/10.38 (((vreduce @ (vUnion @ vq1 @ X1) @ X0)
% 68.10/10.38 = (vsomeQuery @ (vUnion @ vq1 @ (vgetQuery @ (vreduce @ X1 @ X0)))))
% 68.10/10.38 | ~ (visSomeQuery @ (vreduce @ X1 @ X0))
% 68.10/10.38 | ((X1) = (vtvalue @ (sk__109 @ X1))))),
% 68.10/10.38 inference('demod', [status(thm)], [zip_derived_cl5867, zip_derived_cl414])).
% 68.10/10.38 thf(zip_derived_cl416, plain,
% 68.10/10.38 (((vreduce @ (vUnion @ vq1 @ vq2) @ sk__246) = (vsomeQuery @ sk__243))),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(zip_derived_cl28088, plain,
% 68.10/10.38 ((((vsomeQuery @ (vUnion @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__246))))
% 68.10/10.38 = (vsomeQuery @ sk__243))
% 68.10/10.38 | ((vq2) = (vtvalue @ (sk__109 @ vq2)))
% 68.10/10.38 | ~ (visSomeQuery @ (vreduce @ vq2 @ sk__246)))),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl5868, zip_derived_cl416])).
% 68.10/10.38 thf(zip_derived_cl412, plain, ( (visSomeQuery @ (vreduce @ vq2 @ sk__246))),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(zip_derived_cl28129, plain,
% 68.10/10.38 ((((vsomeQuery @ (vUnion @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__246))))
% 68.10/10.38 = (vsomeQuery @ sk__243))
% 68.10/10.38 | ((vq2) = (vtvalue @ (sk__109 @ vq2))))),
% 68.10/10.38 inference('demod', [status(thm)],
% 68.10/10.38 [zip_derived_cl28088, zip_derived_cl412])).
% 68.10/10.38 thf(zip_derived_cl413, plain, (![X0 : vTable]: ((vq2) != (vtvalue @ X0))),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(zip_derived_cl28130, plain,
% 68.10/10.38 (((vsomeQuery @ (vUnion @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__246))))
% 68.10/10.38 = (vsomeQuery @ sk__243))),
% 68.10/10.38 inference('simplify_reflect-', [status(thm)],
% 68.10/10.38 [zip_derived_cl28129, zip_derived_cl413])).
% 68.10/10.38 thf('getQuery-0', axiom,
% 68.10/10.38 (![Vq:vQuery]: ( ( vgetQuery @ ( vsomeQuery @ Vq ) ) = ( Vq ) ))).
% 68.10/10.38 thf(zip_derived_cl47, plain,
% 68.10/10.38 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 68.10/10.38 inference('cnf', [status(esa)], [getQuery-0])).
% 68.10/10.38 thf(zip_derived_cl28133, plain,
% 68.10/10.38 (((vgetQuery @ (vsomeQuery @ sk__243))
% 68.10/10.38 = (vUnion @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__246))))),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl28130, zip_derived_cl47])).
% 68.10/10.38 thf(zip_derived_cl47, plain,
% 68.10/10.38 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 68.10/10.38 inference('cnf', [status(esa)], [getQuery-0])).
% 68.10/10.38 thf(zip_derived_cl28155, plain,
% 68.10/10.38 (((sk__243) = (vUnion @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__246))))),
% 68.10/10.38 inference('demod', [status(thm)], [zip_derived_cl28133, zip_derived_cl47])).
% 68.10/10.38 thf('isValue-false-INV', axiom,
% 68.10/10.38 (![VQuery0:vQuery]:
% 68.10/10.38 ( ( ~( visValue @ VQuery0 ) ) =>
% 68.10/10.38 ( ( ?[VwildcardName0:vSelect,VwildcardName1:vName,VwildcardName2:vPred]:
% 68.10/10.38 ( ( VQuery0 ) =
% 68.10/10.38 ( vselectFromWhere @
% 68.10/10.38 VwildcardName0 @ VwildcardName1 @ VwildcardName2 ) ) ) |
% 68.10/10.38 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 68.10/10.38 ( ( VQuery0 ) = ( vUnion @ VwildcardName0 @ VwildcardName1 ) ) ) |
% 68.10/10.38 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 68.10/10.38 ( ( VQuery0 ) = ( vIntersection @ VwildcardName0 @ VwildcardName1 ) ) ) |
% 68.10/10.38 ( ?[VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 68.10/10.38 ( ( VQuery0 ) = ( vDifference @ VwildcardName0 @ VwildcardName1 ) ) ) ) ))).
% 68.10/10.38 thf(zip_derived_cl183, plain,
% 68.10/10.38 (![X0 : vQuery]:
% 68.10/10.38 (((X0) = (vDifference @ (sk__91 @ X0) @ (sk__92 @ X0)))
% 68.10/10.38 | ((X0) = (vIntersection @ (sk__93 @ X0) @ (sk__94 @ X0)))
% 68.10/10.38 | ((X0) = (vUnion @ (sk__95 @ X0) @ (sk__96 @ X0)))
% 68.10/10.38 | ((X0)
% 68.10/10.38 = (vselectFromWhere @ (sk__97 @ X0) @ (sk__98 @ X0) @
% 68.10/10.38 (sk__99 @ X0)))
% 68.10/10.38 | (visValue @ X0))),
% 68.10/10.38 inference('cnf', [status(esa)], [isValue-false-INV])).
% 68.10/10.38 thf('isValue-2', axiom,
% 68.10/10.38 (![VwildcardName0:vQuery,VwildcardName1:vQuery]:
% 68.10/10.38 ( ~( visValue @ ( vUnion @ VwildcardName0 @ VwildcardName1 ) ) ))).
% 68.10/10.38 thf(zip_derived_cl179, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery]: ~ (visValue @ (vUnion @ X0 @ X1))),
% 68.10/10.38 inference('cnf', [status(esa)], [isValue-2])).
% 68.10/10.38 thf(zip_derived_cl1476, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery]:
% 68.10/10.38 (((vUnion @ X1 @ X0)
% 68.10/10.38 = (vselectFromWhere @ (sk__97 @ (vUnion @ X1 @ X0)) @
% 68.10/10.38 (sk__98 @ (vUnion @ X1 @ X0)) @ (sk__99 @ (vUnion @ X1 @ X0))))
% 68.10/10.38 | ((vUnion @ X1 @ X0)
% 68.10/10.38 = (vUnion @ (sk__95 @ (vUnion @ X1 @ X0)) @
% 68.10/10.38 (sk__96 @ (vUnion @ X1 @ X0))))
% 68.10/10.38 | ((vUnion @ X1 @ X0)
% 68.10/10.38 = (vIntersection @ (sk__93 @ (vUnion @ X1 @ X0)) @
% 68.10/10.38 (sk__94 @ (vUnion @ X1 @ X0))))
% 68.10/10.38 | ((vUnion @ X1 @ X0)
% 68.10/10.38 = (vDifference @ (sk__91 @ (vUnion @ X1 @ X0)) @
% 68.10/10.38 (sk__92 @ (vUnion @ X1 @ X0)))))),
% 68.10/10.38 inference('dp-resolution', [status(thm)],
% 68.10/10.38 [zip_derived_cl183, zip_derived_cl179])).
% 68.10/10.38 thf('DIFF-Union-Difference', axiom,
% 68.10/10.38 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 68.10/10.38 ( ( vUnion @ VQuery0 @ VQuery1 ) != ( vDifference @ VQuery2 @ VQuery3 ) ))).
% 68.10/10.38 thf(zip_derived_cl20, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 68.10/10.38 ((vUnion @ X2 @ X3) != (vDifference @ X0 @ X1))),
% 68.10/10.38 inference('cnf', [status(esa)], [DIFF-Union-Difference])).
% 68.10/10.38 thf('DIFF-Union-Intersection', axiom,
% 68.10/10.38 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 68.10/10.38 ( ( vUnion @ VQuery0 @ VQuery1 ) != ( vIntersection @ VQuery2 @ VQuery3 ) ))).
% 68.10/10.38 thf(zip_derived_cl19, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 68.10/10.38 ((vUnion @ X2 @ X3) != (vIntersection @ X0 @ X1))),
% 68.10/10.38 inference('cnf', [status(esa)], [DIFF-Union-Intersection])).
% 68.10/10.38 thf('DIFF-selectFromWhere-Union', axiom,
% 68.10/10.38 (![VName0:vName,VPred0:vPred,VSelect0:vSelect,VQuery1:vQuery,VQuery0:vQuery]:
% 68.10/10.38 ( ( vselectFromWhere @ VSelect0 @ VName0 @ VPred0 ) !=
% 68.10/10.38 ( vUnion @ VQuery0 @ VQuery1 ) ))).
% 68.10/10.38 thf(zip_derived_cl16, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery, X2 : vSelect, X3 : vName, X4 : vPred]:
% 68.10/10.38 ((vselectFromWhere @ X2 @ X3 @ X4) != (vUnion @ X0 @ X1))),
% 68.10/10.38 inference('cnf', [status(esa)], [DIFF-selectFromWhere-Union])).
% 68.10/10.38 thf(zip_derived_cl11285, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery]:
% 68.10/10.38 ((vUnion @ X1 @ X0)
% 68.10/10.38 = (vUnion @ (sk__95 @ (vUnion @ X1 @ X0)) @
% 68.10/10.38 (sk__96 @ (vUnion @ X1 @ X0))))),
% 68.10/10.38 inference('simplify_reflect-', [status(thm)],
% 68.10/10.38 [zip_derived_cl1476, zip_derived_cl20, zip_derived_cl19,
% 68.10/10.38 zip_derived_cl16])).
% 68.10/10.38 thf(zip_derived_cl11285, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery]:
% 68.10/10.38 ((vUnion @ X1 @ X0)
% 68.10/10.38 = (vUnion @ (sk__95 @ (vUnion @ X1 @ X0)) @
% 68.10/10.38 (sk__96 @ (vUnion @ X1 @ X0))))),
% 68.10/10.38 inference('simplify_reflect-', [status(thm)],
% 68.10/10.38 [zip_derived_cl1476, zip_derived_cl20, zip_derived_cl19,
% 68.10/10.38 zip_derived_cl16])).
% 68.10/10.38 thf('EQ-Union', axiom,
% 68.10/10.38 (![VQuery0:vQuery,VQuery1:vQuery,VQuery2:vQuery,VQuery3:vQuery]:
% 68.10/10.38 ( ( ( vUnion @ VQuery0 @ VQuery1 ) = ( vUnion @ VQuery2 @ VQuery3 ) ) =>
% 68.10/10.38 ( ( ( VQuery0 ) = ( VQuery2 ) ) & ( ( VQuery1 ) = ( VQuery3 ) ) ) ))).
% 68.10/10.38 thf(zip_derived_cl6, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 68.10/10.38 (((X1) = (X0)) | ((vUnion @ X1 @ X3) != (vUnion @ X0 @ X2)))),
% 68.10/10.38 inference('cnf', [status(esa)], [EQ-Union])).
% 68.10/10.38 thf(zip_derived_cl11286, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 68.10/10.38 (((vUnion @ X3 @ X2) != (vUnion @ X1 @ X0))
% 68.10/10.38 | ((X3) = (sk__95 @ (vUnion @ X1 @ X0))))),
% 68.10/10.38 inference('sup-', [status(thm)], [zip_derived_cl11285, zip_derived_cl6])).
% 68.10/10.38 thf(zip_derived_cl11481, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery]: ((X0) = (sk__95 @ (vUnion @ X0 @ X1)))),
% 68.10/10.38 inference('eq_res', [status(thm)], [zip_derived_cl11286])).
% 68.10/10.38 thf(zip_derived_cl11563, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery]:
% 68.10/10.38 ((vUnion @ X1 @ X0) = (vUnion @ X1 @ (sk__96 @ (vUnion @ X1 @ X0))))),
% 68.10/10.38 inference('demod', [status(thm)],
% 68.10/10.38 [zip_derived_cl11285, zip_derived_cl11481])).
% 68.10/10.38 thf(zip_derived_cl7, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 68.10/10.38 (((X1) = (X0)) | ((vUnion @ X3 @ X1) != (vUnion @ X2 @ X0)))),
% 68.10/10.38 inference('cnf', [status(esa)], [EQ-Union])).
% 68.10/10.38 thf(zip_derived_cl19709, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery, X2 : vQuery, X3 : vQuery]:
% 68.10/10.38 (((vUnion @ X3 @ X2) != (vUnion @ X1 @ X0))
% 68.10/10.38 | ((X2) = (sk__96 @ (vUnion @ X1 @ X0))))),
% 68.10/10.38 inference('sup-', [status(thm)], [zip_derived_cl11563, zip_derived_cl7])).
% 68.10/10.38 thf(zip_derived_cl19788, plain,
% 68.10/10.38 (![X0 : vQuery, X1 : vQuery]: ((X0) = (sk__96 @ (vUnion @ X1 @ X0)))),
% 68.10/10.38 inference('eq_res', [status(thm)], [zip_derived_cl19709])).
% 68.10/10.38 thf(zip_derived_cl28204, plain,
% 68.10/10.38 (((vgetQuery @ (vreduce @ vq2 @ sk__246)) = (sk__96 @ sk__243))),
% 68.10/10.38 inference('sup+', [status(thm)],
% 68.10/10.38 [zip_derived_cl28155, zip_derived_cl19788])).
% 68.10/10.38 thf('dom-OptQuery', axiom,
% 68.10/10.38 (![VX:vOptQuery]:
% 68.10/10.38 ( ( ?[VQuery0:vQuery]: ( ( VX ) = ( vsomeQuery @ VQuery0 ) ) ) |
% 68.10/10.38 ( ( VX ) = ( vnoQuery ) ) ))).
% 68.10/10.38 thf(zip_derived_cl34, plain,
% 68.10/10.38 (![X0 : vOptQuery]:
% 68.10/10.38 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 68.10/10.38 inference('cnf', [status(esa)], [dom-OptQuery])).
% 68.10/10.38 thf(zip_derived_cl47, plain,
% 68.10/10.38 (![X0 : vQuery]: ((vgetQuery @ (vsomeQuery @ X0)) = (X0))),
% 68.10/10.38 inference('cnf', [status(esa)], [getQuery-0])).
% 68.10/10.38 thf(zip_derived_cl5276, plain,
% 68.10/10.38 (![X0 : vOptQuery]:
% 68.10/10.38 (((vgetQuery @ X0) = (sk__16 @ X0)) | ((X0) = (vnoQuery)))),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl34, zip_derived_cl47])).
% 68.10/10.38 thf(zip_derived_cl34, plain,
% 68.10/10.38 (![X0 : vOptQuery]:
% 68.10/10.38 (((X0) = (vsomeQuery @ (sk__16 @ X0))) | ((X0) = (vnoQuery)))),
% 68.10/10.38 inference('cnf', [status(esa)], [dom-OptQuery])).
% 68.10/10.38 thf(zip_derived_cl5298, plain,
% 68.10/10.38 (![X0 : vOptQuery]:
% 68.10/10.38 (((X0) = (vsomeQuery @ (vgetQuery @ X0)))
% 68.10/10.38 | ((X0) = (vnoQuery))
% 68.10/10.38 | ((X0) = (vnoQuery)))),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl5276, zip_derived_cl34])).
% 68.10/10.38 thf(zip_derived_cl5301, plain,
% 68.10/10.38 (![X0 : vOptQuery]:
% 68.10/10.38 (((X0) = (vnoQuery)) | ((X0) = (vsomeQuery @ (vgetQuery @ X0))))),
% 68.10/10.38 inference('simplify', [status(thm)], [zip_derived_cl5298])).
% 68.10/10.38 thf(zip_derived_cl29107, plain,
% 68.10/10.38 ((((vreduce @ vq2 @ sk__246) = (vsomeQuery @ (sk__96 @ sk__243)))
% 68.10/10.38 | ((vreduce @ vq2 @ sk__246) = (vnoQuery)))),
% 68.10/10.38 inference('sup+', [status(thm)],
% 68.10/10.38 [zip_derived_cl28204, zip_derived_cl5301])).
% 68.10/10.38 thf('isSomeQuery-true-INV', axiom,
% 68.10/10.38 (![VOptQuery0:vOptQuery]:
% 68.10/10.38 ( ( visSomeQuery @ VOptQuery0 ) =>
% 68.10/10.38 ( ?[VwildcardName0:vQuery]:
% 68.10/10.38 ( ( VOptQuery0 ) = ( vsomeQuery @ VwildcardName0 ) ) ) ))).
% 68.10/10.38 thf(zip_derived_cl186, plain,
% 68.10/10.38 (![X0 : vOptQuery]:
% 68.10/10.38 (((X0) = (vsomeQuery @ (sk__100 @ X0))) | ~ (visSomeQuery @ X0))),
% 68.10/10.38 inference('cnf', [status(esa)], [isSomeQuery-true-INV])).
% 68.10/10.38 thf('DIFF-noQuery-someQuery', axiom,
% 68.10/10.38 (![VQuery0:vQuery]: ( ( vnoQuery ) != ( vsomeQuery @ VQuery0 ) ))).
% 68.10/10.38 thf(zip_derived_cl36, plain,
% 68.10/10.38 (![X0 : vQuery]: ((vnoQuery) != (vsomeQuery @ X0))),
% 68.10/10.38 inference('cnf', [status(esa)], [DIFF-noQuery-someQuery])).
% 68.10/10.38 thf(zip_derived_cl5253, plain,
% 68.10/10.38 (![X0 : vOptQuery]: (((vnoQuery) != (X0)) | ~ (visSomeQuery @ X0))),
% 68.10/10.38 inference('sup-', [status(thm)], [zip_derived_cl186, zip_derived_cl36])).
% 68.10/10.38 thf(zip_derived_cl412, plain, ( (visSomeQuery @ (vreduce @ vq2 @ sk__246))),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(zip_derived_cl5259, plain, (((vnoQuery) != (vreduce @ vq2 @ sk__246))),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl5253, zip_derived_cl412])).
% 68.10/10.38 thf(zip_derived_cl29116, plain,
% 68.10/10.38 (((vreduce @ vq2 @ sk__246) = (vsomeQuery @ (sk__96 @ sk__243)))),
% 68.10/10.38 inference('simplify_reflect-', [status(thm)],
% 68.10/10.38 [zip_derived_cl29107, zip_derived_cl5259])).
% 68.10/10.38 thf(zip_derived_cl29234, plain,
% 68.10/10.38 (![X0 : vQuery]:
% 68.10/10.38 (((vsomeQuery @ (sk__96 @ sk__243)) != (vsomeQuery @ X0))
% 68.10/10.38 | (vptcheck @ sk__245 @ X0 @ sk__247))),
% 68.10/10.38 inference('demod', [status(thm)],
% 68.10/10.38 [zip_derived_cl5824, zip_derived_cl29116])).
% 68.10/10.38 thf(zip_derived_cl28155, plain,
% 68.10/10.38 (((sk__243) = (vUnion @ vq1 @ (vgetQuery @ (vreduce @ vq2 @ sk__246))))),
% 68.10/10.38 inference('demod', [status(thm)], [zip_derived_cl28133, zip_derived_cl47])).
% 68.10/10.38 thf(zip_derived_cl28204, plain,
% 68.10/10.38 (((vgetQuery @ (vreduce @ vq2 @ sk__246)) = (sk__96 @ sk__243))),
% 68.10/10.38 inference('sup+', [status(thm)],
% 68.10/10.38 [zip_derived_cl28155, zip_derived_cl19788])).
% 68.10/10.38 thf(zip_derived_cl29106, plain,
% 68.10/10.38 (((sk__243) = (vUnion @ vq1 @ (sk__96 @ sk__243)))),
% 68.10/10.38 inference('demod', [status(thm)],
% 68.10/10.38 [zip_derived_cl28155, zip_derived_cl28204])).
% 68.10/10.38 thf(TUnion, axiom,
% 68.10/10.38 (![VTTC:vTTContext,Vq1:vQuery,VTT:vTType,Vq2:vQuery]:
% 68.10/10.38 ( ( ( vptcheck @ VTTC @ Vq1 @ VTT ) & ( vptcheck @ VTTC @ Vq2 @ VTT ) ) =>
% 68.10/10.38 ( vptcheck @ VTTC @ ( vUnion @ Vq1 @ Vq2 ) @ VTT ) ))).
% 68.10/10.38 thf(zip_derived_cl395, plain,
% 68.10/10.38 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 68.10/10.38 (~ (vptcheck @ X0 @ X1 @ X2)
% 68.10/10.38 | ~ (vptcheck @ X0 @ X3 @ X2)
% 68.10/10.38 | (vptcheck @ X0 @ (vUnion @ X1 @ X3) @ X2))),
% 68.10/10.38 inference('cnf', [status(esa)], [TUnion])).
% 68.10/10.38 thf(zip_derived_cl29122, plain,
% 68.10/10.38 (![X0 : vTType, X1 : vTTContext]:
% 68.10/10.38 ( (vptcheck @ X1 @ sk__243 @ X0)
% 68.10/10.38 | ~ (vptcheck @ X1 @ (sk__96 @ sk__243) @ X0)
% 68.10/10.38 | ~ (vptcheck @ X1 @ vq1 @ X0))),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl29106, zip_derived_cl395])).
% 68.10/10.38 thf(zip_derived_cl57525, plain,
% 68.10/10.38 ((((vsomeQuery @ (sk__96 @ sk__243)) != (vsomeQuery @ (sk__96 @ sk__243)))
% 68.10/10.38 | ~ (vptcheck @ sk__245 @ vq1 @ sk__247)
% 68.10/10.38 | (vptcheck @ sk__245 @ sk__243 @ sk__247))),
% 68.10/10.38 inference('sup-', [status(thm)],
% 68.10/10.38 [zip_derived_cl29234, zip_derived_cl29122])).
% 68.10/10.38 thf(TUnion_inv1, axiom,
% 68.10/10.38 (![VTTC:vTTContext,Vq1:vQuery,Vq2:vQuery,VTT:vTType]:
% 68.10/10.38 ( ( vptcheck @ VTTC @ ( vUnion @ Vq1 @ Vq2 ) @ VTT ) =>
% 68.10/10.38 ( vptcheck @ VTTC @ Vq1 @ VTT ) ))).
% 68.10/10.38 thf(zip_derived_cl402, plain,
% 68.10/10.38 (![X0 : vTTContext, X1 : vQuery, X2 : vTType, X3 : vQuery]:
% 68.10/10.38 ( (vptcheck @ X0 @ X1 @ X2)
% 68.10/10.38 | ~ (vptcheck @ X0 @ (vUnion @ X1 @ X3) @ X2))),
% 68.10/10.38 inference('cnf', [status(esa)], [TUnion_inv1])).
% 68.10/10.38 thf(zip_derived_cl411, plain,
% 68.10/10.38 ( (vptcheck @ sk__245 @ (vUnion @ vq1 @ vq2) @ sk__247)),
% 68.10/10.38 inference('cnf', [status(esa)], [zf_stmt_0])).
% 68.10/10.38 thf(zip_derived_cl5537, plain, ( (vptcheck @ sk__245 @ vq1 @ sk__247)),
% 68.10/10.38 inference('sup+', [status(thm)], [zip_derived_cl402, zip_derived_cl411])).
% 68.10/10.38 thf(zip_derived_cl57526, plain,
% 68.10/10.38 ((((vsomeQuery @ (sk__96 @ sk__243)) != (vsomeQuery @ (sk__96 @ sk__243)))
% 68.10/10.38 | (vptcheck @ sk__245 @ sk__243 @ sk__247))),
% 68.10/10.38 inference('demod', [status(thm)],
% 68.10/10.38 [zip_derived_cl57525, zip_derived_cl5537])).
% 68.10/10.38 thf(zip_derived_cl57527, plain, ( (vptcheck @ sk__245 @ sk__243 @ sk__247)),
% 68.10/10.38 inference('simplify', [status(thm)], [zip_derived_cl57526])).
% 68.10/10.38 thf(zip_derived_cl57530, plain, ($false),
% 68.10/10.38 inference('demod', [status(thm)],
% 68.10/10.38 [zip_derived_cl410, zip_derived_cl57527])).
% 68.10/10.38
% 68.10/10.38 % SZS output end Refutation
% 68.10/10.38
% 68.10/10.38
% 68.10/10.38 % Terminating...
% 68.81/10.48 % Runner terminated.
% 68.81/10.49 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------