%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM299_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.RZKBoksbn3 true
% Computer : n007.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:26 PM UTC 2026
% Result : Theorem 21.29s 3.69s
% Output : Refutation 21.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : COM299_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.RZKBoksbn3 true
% 0.15/0.33 % Computer : n007.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 20:33:23 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.34 % Running portfolio for 300 s
% 0.15/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.34 % Number of cores: 8
% 0.15/0.34 % Python version: Python 3.6.8
% 0.15/0.34 % Running in FO mode
% 0.46/0.61 % Total configuration time : 435
% 0.46/0.61 % Estimated wc time : 1092
% 0.46/0.61 % Estimated cpu time (7 cpus) : 156.0
% 0.53/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.53/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.53/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.53/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.53/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.53/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.53/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 21.29/3.69 % Solved by fo/fo6_bce.sh.
% 21.29/3.69 % BCE start: 963
% 21.29/3.69 % BCE eliminated: 0
% 21.29/3.69 % PE start: 963
% 21.29/3.69 logic: eq
% 21.29/3.69 % PE eliminated: -186
% 21.29/3.69 % done 1570 iterations in 2.969s
% 21.29/3.69 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 21.29/3.69 % SZS output start Refutation
% 21.29/3.69 thf(vOptQuery_type, type, vOptQuery: $tType).
% 21.29/3.69 thf(vQuery_type, type, vQuery: $tType).
% 21.29/3.69 thf(vTStore_type, type, vTStore: $tType).
% 21.29/3.69 thf(vTable_type, type, vTable: $tType).
% 21.29/3.69 thf(vTTContext_type, type, vTTContext: $tType).
% 21.29/3.69 thf(vTType_type, type, vTType: $tType).
% 21.29/3.69 thf(sk__546_type, type, sk__546: vTStore).
% 21.29/3.69 thf(vtvalue_type, type, vtvalue: vTable > vQuery).
% 21.29/3.69 thf(vq2_type, type, vq2: vQuery).
% 21.29/3.69 thf(vptcheck_type, type, vptcheck: vTTContext > vQuery > vTType > $o).
% 21.29/3.69 thf(vnoQuery_type, type, vnoQuery: vOptQuery).
% 21.29/3.69 thf(sk__24_type, type, sk__24: vOptQuery > vQuery).
% 21.29/3.69 thf(sk__334_type, type, sk__334: vQuery > vTable).
% 21.29/3.69 thf(visSomeQuery_type, type, visSomeQuery: vOptQuery > $o).
% 21.29/3.69 thf(vreduce_type, type, vreduce: vQuery > vTStore > vOptQuery).
% 21.29/3.69 thf(vq1_type, type, vq1: vQuery).
% 21.29/3.69 thf(vUnion_type, type, vUnion: vQuery > vQuery > vQuery).
% 21.29/3.69 thf(vgetQuery_type, type, vgetQuery: vOptQuery > vQuery).
% 21.29/3.69 thf(visValue_type, type, visValue: vQuery > $o).
% 21.29/3.69 thf(vstoreContextConsistent_type, type, vstoreContextConsistent: vTStore >
% 21.29/3.69 vTTContext > $o).
% 21.29/3.69 thf(sk__547_type, type, sk__547: vTable).
% 21.29/3.69 thf(vsomeQuery_type, type, vsomeQuery: vQuery > vOptQuery).
% 21.29/3.69 thf('Progress-Union-tvalue-q2-isSomeQuery-True', conjecture,
% 21.29/3.69 (![Vts:vTStore,Vt:vTable,Vttc:vTTContext]:
% 21.29/3.69 ( ( ( visSomeQuery @ ( vreduce @ vq2 @ Vts ) ) &
% 21.29/3.69 ( ![Vt200:vTable]: ( ( vq2 ) != ( vtvalue @ Vt200 ) ) ) &
% 21.29/3.69 ( ( vq1 ) = ( vtvalue @ Vt ) ) &
% 21.29/3.69 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 21.29/3.69 ( ~( visValue @ ( vUnion @ vq1 @ vq2 ) ) ) &
% 21.29/3.69 ( ?[Vtt100:vTType]:
% 21.29/3.69 ( vptcheck @ Vttc @ ( vUnion @ vq1 @ vq2 ) @ Vtt100 ) ) ) =>
% 21.29/3.69 ( ?[Vqr00:vQuery]:
% 21.29/3.69 ( ( vreduce @ ( vUnion @ vq1 @ vq2 ) @ Vts ) = ( vsomeQuery @ Vqr00 ) ) ) ))).
% 21.29/3.69 thf(zf_stmt_0, negated_conjecture,
% 21.29/3.69 (~( ![Vts:vTStore,Vt:vTable,Vttc:vTTContext]:
% 21.29/3.69 ( ( ( visSomeQuery @ ( vreduce @ vq2 @ Vts ) ) &
% 21.29/3.69 ( ![Vt200:vTable]: ( ( vq2 ) != ( vtvalue @ Vt200 ) ) ) &
% 21.29/3.69 ( ( vq1 ) = ( vtvalue @ Vt ) ) &
% 21.29/3.69 ( vstoreContextConsistent @ Vts @ Vttc ) &
% 21.29/3.69 ( ~( visValue @ ( vUnion @ vq1 @ vq2 ) ) ) &
% 21.29/3.69 ( ?[Vtt100:vTType]:
% 21.29/3.69 ( vptcheck @ Vttc @ ( vUnion @ vq1 @ vq2 ) @ Vtt100 ) ) ) =>
% 21.29/3.69 ( ?[Vqr00:vQuery]:
% 21.29/3.69 ( ( vreduce @ ( vUnion @ vq1 @ vq2 ) @ Vts ) =
% 21.29/3.69 ( vsomeQuery @ Vqr00 ) ) ) ) )),
% 21.29/3.69 inference('cnf.neg', [status(esa)],
% 21.29/3.69 [Progress-Union-tvalue-q2-isSomeQuery-True])).
% 21.29/3.69 thf(zip_derived_cl960, plain, (((vq1) = (vtvalue @ sk__547))),
% 21.29/3.69 inference('cnf', [status(esa)], [zf_stmt_0])).
% 21.29/3.69 thf(zip_derived_cl958, plain, ( (visSomeQuery @ (vreduce @ vq2 @ sk__546))),
% 21.29/3.69 inference('cnf', [status(esa)], [zf_stmt_0])).
% 21.29/3.69 thf('reduce-5', axiom,
% 21.29/3.69 (![Vt:vTable,Vq2:vQuery,Vts:vTStore]:
% 21.29/3.69 ( ( ( ![Vt100:vTable,Vt200:vTable]:
% 21.29/3.69 ( ( ( Vq2 ) != ( vtvalue @ Vt200 ) ) | ( ( Vt ) != ( Vt100 ) ) ) ) &
% 21.29/3.69 ( visSomeQuery @ ( vreduce @ Vq2 @ Vts ) ) ) =>
% 21.29/3.69 ( ( vreduce @ ( vUnion @ ( vtvalue @ Vt ) @ Vq2 ) @ Vts ) =
% 21.29/3.69 ( vsomeQuery @
% 21.29/3.69 ( vUnion @
% 21.29/3.69 ( vtvalue @ Vt ) @ ( vgetQuery @ ( vreduce @ Vq2 @ Vts ) ) ) ) ) ))).
% 21.29/3.69 thf(zip_derived_cl617, plain,
% 21.29/3.69 (![X0 : vQuery, X1 : vTStore, X2 : vTable]:
% 21.29/3.69 (((X0) = (vtvalue @ (sk__334 @ X0)))
% 21.29/3.69 | ~ (visSomeQuery @ (vreduce @ X0 @ X1))
% 21.29/3.69 | ((vreduce @ (vUnion @ (vtvalue @ X2) @ X0) @ X1)
% 21.29/3.69 = (vsomeQuery @
% 21.29/3.69 (vUnion @ (vtvalue @ X2) @ (vgetQuery @ (vreduce @ X0 @ X1))))))),
% 21.29/3.69 inference('cnf', [status(esa)], [reduce-5])).
% 21.29/3.69 thf('DIFF-noQuery-someQuery', axiom,
% 21.29/3.69 (![VQuery0:vQuery]: ( ( vnoQuery ) != ( vsomeQuery @ VQuery0 ) ))).
% 21.29/3.69 thf(zip_derived_cl55, plain,
% 21.29/3.69 (![X0 : vQuery]: ((vnoQuery) != (vsomeQuery @ X0))),
% 21.29/3.69 inference('cnf', [status(esa)], [DIFF-noQuery-someQuery])).
% 21.29/3.69 thf(zip_derived_cl12866, plain,
% 21.29/3.69 (![X0 : vTStore, X1 : vQuery, X2 : vTable]:
% 21.29/3.69 (~ (visSomeQuery @ (vreduce @ X1 @ X0))
% 21.29/3.69 | ((X1) = (vtvalue @ (sk__334 @ X1)))
% 21.29/3.69 | ((vnoQuery) != (vreduce @ (vUnion @ (vtvalue @ X2) @ X1) @ X0)))),
% 21.29/3.69 inference('s_sup-', [status(thm)], [zip_derived_cl617, zip_derived_cl55])).
% 21.29/3.69 thf(zip_derived_cl14366, plain,
% 21.29/3.69 (![X0 : vTable]:
% 21.29/3.69 (((vq2) = (vtvalue @ (sk__334 @ vq2)))
% 21.29/3.69 | ((vnoQuery)
% 21.29/3.69 != (vreduce @ (vUnion @ (vtvalue @ X0) @ vq2) @ sk__546)))),
% 21.29/3.69 inference('s_sup-', [status(thm)],
% 21.29/3.69 [zip_derived_cl958, zip_derived_cl12866])).
% 21.29/3.69 thf(zip_derived_cl959, plain, (![X0 : vTable]: ((vq2) != (vtvalue @ X0))),
% 21.29/3.69 inference('cnf', [status(esa)], [zf_stmt_0])).
% 21.29/3.69 thf(zip_derived_cl14381, plain,
% 21.29/3.69 (![X0 : vTable]:
% 21.29/3.69 ((vnoQuery) != (vreduce @ (vUnion @ (vtvalue @ X0) @ vq2) @ sk__546))),
% 21.29/3.69 inference('simplify_reflect-', [status(thm)],
% 21.29/3.69 [zip_derived_cl14366, zip_derived_cl959])).
% 21.29/3.69 thf(zip_derived_cl14413, plain,
% 21.29/3.69 (((vnoQuery) != (vreduce @ (vUnion @ vq1 @ vq2) @ sk__546))),
% 21.29/3.69 inference('s_sup-', [status(thm)],
% 21.29/3.69 [zip_derived_cl960, zip_derived_cl14381])).
% 21.29/3.69 thf('dom-OptQuery', axiom,
% 21.29/3.69 (![VX:vOptQuery]:
% 21.29/3.69 ( ( ?[VQuery0:vQuery]: ( ( VX ) = ( vsomeQuery @ VQuery0 ) ) ) |
% 21.29/3.69 ( ( VX ) = ( vnoQuery ) ) ))).
% 21.29/3.69 thf(zip_derived_cl53, plain,
% 21.29/3.69 (![X0 : vOptQuery]:
% 21.29/3.69 (((X0) = (vsomeQuery @ (sk__24 @ X0))) | ((X0) = (vnoQuery)))),
% 21.29/3.69 inference('cnf', [status(esa)], [dom-OptQuery])).
% 21.29/3.69 thf(zip_derived_cl962, plain,
% 21.29/3.69 (![X1 : vQuery]:
% 21.29/3.69 ((vreduce @ (vUnion @ vq1 @ vq2) @ sk__546) != (vsomeQuery @ X1))),
% 21.29/3.69 inference('cnf', [status(esa)], [zf_stmt_0])).
% 21.29/3.69 thf(zip_derived_cl10312, plain,
% 21.29/3.69 (![X0 : vOptQuery]:
% 21.29/3.69 (((X0) = (vnoQuery))
% 21.29/3.69 | ((vreduce @ (vUnion @ vq1 @ vq2) @ sk__546) != (X0)))),
% 21.29/3.69 inference('s_sup-', [status(thm)], [zip_derived_cl53, zip_derived_cl962])).
% 21.29/3.69 thf(zip_derived_cl10318, plain,
% 21.29/3.69 (((vreduce @ (vUnion @ vq1 @ vq2) @ sk__546) = (vnoQuery))),
% 21.29/3.69 inference('eq_res', [status(thm)], [zip_derived_cl10312])).
% 21.29/3.69 thf(zip_derived_cl14416, plain, (((vnoQuery) != (vnoQuery))),
% 21.29/3.69 inference('demod', [status(thm)],
% 21.29/3.69 [zip_derived_cl14413, zip_derived_cl10318])).
% 21.29/3.69 thf(zip_derived_cl14417, plain, ($false),
% 21.29/3.69 inference('simplify', [status(thm)], [zip_derived_cl14416])).
% 21.29/3.69
% 21.29/3.69 % SZS output end Refutation
% 21.29/3.69
% 21.29/3.69
% 21.29/3.69 % Terminating...
% 22.00/3.75 % Runner terminated.
% 22.00/3.76 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------