%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM281_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.1LJb0wZeSn true
% Computer : n029.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 5.82s 1.46s
% Output : Refutation 5.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : COM281_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.14 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.1LJb0wZeSn true
% 0.17/0.35 % Computer : n029.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Mon May 4 20:15:29 EDT 2026
% 0.17/0.36 % CPUTime :
% 0.17/0.36 % Running portfolio for 300 s
% 0.17/0.36 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.36 % Number of cores: 8
% 0.17/0.36 % Python version: Python 3.6.8
% 0.17/0.36 % Running in FO mode
% 0.54/0.64 % Total configuration time : 435
% 0.54/0.64 % Estimated wc time : 1092
% 0.54/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.55/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.55/0.72 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 5.82/1.46 % Solved by fo/fo7.sh.
% 5.82/1.46 % done 1407 iterations in 0.686s
% 5.82/1.46 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 5.82/1.46 % SZS output start Refutation
% 5.82/1.46 thf(vTType_type, type, vTType: $tType).
% 5.82/1.46 thf(vRawTable_type, type, vRawTable: $tType).
% 5.82/1.46 thf(vAttrL_type, type, vAttrL: $tType).
% 5.82/1.46 thf(vPred_type, type, vPred: $tType).
% 5.82/1.46 thf(vTable_type, type, vTable: $tType).
% 5.82/1.46 thf(sk__24_type, type, sk__24: vTable > vAttrL).
% 5.82/1.46 thf(sk__281_type, type, sk__281: vTType).
% 5.82/1.46 thf(vmatchingAttrL_type, type, vmatchingAttrL: vTType > vAttrL > $o).
% 5.82/1.46 thf(sk__55_type, type, sk__55: vTable > vTType > vRawTable).
% 5.82/1.46 thf(sk__23_type, type, sk__23: vTable > vRawTable).
% 5.82/1.46 thf(sk__53_type, type, sk__53: vTable > vTType > vTType).
% 5.82/1.46 thf(vgetAttrL_type, type, vgetAttrL: vTable > vAttrL).
% 5.82/1.46 thf(vwelltypedtable_type, type, vwelltypedtable: vTType > vTable > $o).
% 5.82/1.46 thf(vfilterRows_type, type, vfilterRows: vRawTable > vAttrL > vPred > vRawTable).
% 5.82/1.46 thf(sk__54_type, type, sk__54: vTable > vTType > vAttrL).
% 5.82/1.46 thf(vgetRaw_type, type, vgetRaw: vTable > vRawTable).
% 5.82/1.46 thf(sk__17_type, type, sk__17: vTable > vAttrL).
% 5.82/1.46 thf(sk__25_type, type, sk__25: vTable > vRawTable).
% 5.82/1.46 thf(vfilterTable_type, type, vfilterTable: vTable > vPred > vTable).
% 5.82/1.46 thf(vtable_type, type, vtable: vAttrL > vRawTable > vTable).
% 5.82/1.46 thf(sk__22_type, type, sk__22: vTable > vAttrL).
% 5.82/1.46 thf(vwelltypedRawtable_type, type, vwelltypedRawtable: vTType > vRawTable > $o).
% 5.82/1.46 thf(sk__18_type, type, sk__18: vTable > vRawTable).
% 5.82/1.46 thf(sk__283_type, type, sk__283: vPred).
% 5.82/1.46 thf(sk__282_type, type, sk__282: vTable).
% 5.82/1.46 thf(filterRowsPreservesTable, axiom,
% 5.82/1.46 (![Vtt:vTType,Vrt:vRawTable,Val:vAttrL,Vp:vPred]:
% 5.82/1.46 ( ( vwelltypedRawtable @ Vtt @ Vrt ) =>
% 5.82/1.46 ( vwelltypedRawtable @ Vtt @ ( vfilterRows @ Vrt @ Val @ Vp ) ) ))).
% 5.82/1.46 thf(zip_derived_cl470, plain,
% 5.82/1.46 (![X0 : vTType, X1 : vRawTable, X2 : vAttrL, X3 : vPred]:
% 5.82/1.46 (~ (vwelltypedRawtable @ X0 @ X1)
% 5.82/1.46 | (vwelltypedRawtable @ X0 @ (vfilterRows @ X1 @ X2 @ X3)))),
% 5.82/1.46 inference('cnf', [status(esa)], [filterRowsPreservesTable])).
% 5.82/1.46 thf('welltypedtable-false-INV', axiom,
% 5.82/1.46 (![VTType0:vTType,VTable0:vTable]:
% 5.82/1.46 ( ( ~( vwelltypedtable @ VTType0 @ VTable0 ) ) =>
% 5.82/1.46 ( ?[Vtt:vTType,Val:vAttrL,Vt1:vRawTable]:
% 5.82/1.46 ( ( ~( ( vmatchingAttrL @ Vtt @ Val ) &
% 5.82/1.46 ( vwelltypedRawtable @ Vtt @ Vt1 ) ) ) &
% 5.82/1.46 ( ( VTable0 ) = ( vtable @ Val @ Vt1 ) ) & ( ( VTType0 ) = ( Vtt ) ) ) ) ))).
% 5.82/1.46 thf(zip_derived_cl102, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vTType]:
% 5.82/1.46 (~ (vwelltypedRawtable @ (sk__53 @ X0 @ X1) @ (sk__55 @ X0 @ X1))
% 5.82/1.46 | ~ (vmatchingAttrL @ (sk__53 @ X0 @ X1) @ (sk__54 @ X0 @ X1))
% 5.82/1.46 | (vwelltypedtable @ X1 @ X0))),
% 5.82/1.46 inference('cnf', [status(esa)], [welltypedtable-false-INV])).
% 5.82/1.46 thf(filterPreservesType, conjecture,
% 5.82/1.46 (![Vtt:vTType,Vt:vTable,Vp:vPred]:
% 5.82/1.46 ( ( vwelltypedtable @ Vtt @ Vt ) =>
% 5.82/1.46 ( vwelltypedtable @ Vtt @ ( vfilterTable @ Vt @ Vp ) ) ))).
% 5.82/1.46 thf(zf_stmt_0, negated_conjecture,
% 5.82/1.46 (~( ![Vtt:vTType,Vt:vTable,Vp:vPred]:
% 5.82/1.46 ( ( vwelltypedtable @ Vtt @ Vt ) =>
% 5.82/1.46 ( vwelltypedtable @ Vtt @ ( vfilterTable @ Vt @ Vp ) ) ) )),
% 5.82/1.46 inference('cnf.neg', [status(esa)], [filterPreservesType])).
% 5.82/1.46 thf(zip_derived_cl471, plain,
% 5.82/1.46 (~ (vwelltypedtable @ sk__281 @ (vfilterTable @ sk__282 @ sk__283))),
% 5.82/1.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.82/1.46 thf(zip_derived_cl1348, plain,
% 5.82/1.46 ((~ (vmatchingAttrL @
% 5.82/1.46 (sk__53 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281) @
% 5.82/1.46 (sk__54 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281))
% 5.82/1.46 | ~ (vwelltypedRawtable @
% 5.82/1.46 (sk__53 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281) @
% 5.82/1.46 (sk__55 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl102, zip_derived_cl471])).
% 5.82/1.46 thf(zip_derived_cl100, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vTType]:
% 5.82/1.46 (((X1) = (sk__53 @ X0 @ X1)) | (vwelltypedtable @ X1 @ X0))),
% 5.82/1.46 inference('cnf', [status(esa)], [welltypedtable-false-INV])).
% 5.82/1.46 thf(zip_derived_cl471, plain,
% 5.82/1.46 (~ (vwelltypedtable @ sk__281 @ (vfilterTable @ sk__282 @ sk__283))),
% 5.82/1.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.82/1.46 thf(zip_derived_cl953, plain,
% 5.82/1.46 (((sk__281) = (sk__53 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl471])).
% 5.82/1.46 thf(zip_derived_cl101, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vTType]:
% 5.82/1.46 (((X0) = (vtable @ (sk__54 @ X0 @ X1) @ (sk__55 @ X0 @ X1)))
% 5.82/1.46 | (vwelltypedtable @ X1 @ X0))),
% 5.82/1.46 inference('cnf', [status(esa)], [welltypedtable-false-INV])).
% 5.82/1.46 thf(zip_derived_cl471, plain,
% 5.82/1.46 (~ (vwelltypedtable @ sk__281 @ (vfilterTable @ sk__282 @ sk__283))),
% 5.82/1.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.82/1.46 thf(zip_derived_cl1192, plain,
% 5.82/1.46 (((vfilterTable @ sk__282 @ sk__283)
% 5.82/1.46 = (vtable @ (sk__54 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281) @
% 5.82/1.46 (sk__55 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl101, zip_derived_cl471])).
% 5.82/1.46 thf('dom-Table', axiom,
% 5.82/1.46 (![VX:vTable]:
% 5.82/1.46 ( ?[VAttrL0:vAttrL,VRawTable0:vRawTable]:
% 5.82/1.46 ( ( VX ) = ( vtable @ VAttrL0 @ VRawTable0 ) ) ))).
% 5.82/1.46 thf(zip_derived_cl37, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (sk__17 @ X0) @ (sk__18 @ X0)))),
% 5.82/1.46 inference('cnf', [status(esa)], [dom-Table])).
% 5.82/1.46 thf('EQ-table', axiom,
% 5.82/1.46 (![VAttrL0:vAttrL,VRawTable0:vRawTable,VAttrL1:vAttrL,VRawTable1:vRawTable]:
% 5.82/1.46 ( ( ( vtable @ VAttrL0 @ VRawTable0 ) = ( vtable @ VAttrL1 @ VRawTable1 ) ) =>
% 5.82/1.46 ( ( ( VAttrL0 ) = ( VAttrL1 ) ) & ( ( VRawTable0 ) = ( VRawTable1 ) ) ) ))).
% 5.82/1.46 thf(zip_derived_cl38, plain,
% 5.82/1.46 (![X0 : vAttrL, X1 : vAttrL, X2 : vRawTable, X3 : vRawTable]:
% 5.82/1.46 (((X1) = (X0)) | ((vtable @ X1 @ X3) != (vtable @ X0 @ X2)))),
% 5.82/1.46 inference('cnf', [status(esa)], [EQ-table])).
% 5.82/1.46 thf(zip_derived_cl505, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vRawTable, X2 : vAttrL]:
% 5.82/1.46 (((vtable @ X2 @ X1) != (X0)) | ((X2) = (sk__17 @ X0)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl38])).
% 5.82/1.46 thf(zip_derived_cl525, plain,
% 5.82/1.46 (![X0 : vAttrL, X1 : vRawTable]: ((X0) = (sk__17 @ (vtable @ X0 @ X1)))),
% 5.82/1.46 inference('eq_res', [status(thm)], [zip_derived_cl505])).
% 5.82/1.46 thf(zip_derived_cl1274, plain,
% 5.82/1.46 (((sk__54 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281)
% 5.82/1.46 = (sk__17 @ (vfilterTable @ sk__282 @ sk__283)))),
% 5.82/1.46 inference('sup+', [status(thm)], [zip_derived_cl1192, zip_derived_cl525])).
% 5.82/1.46 thf('getAttrL-INV', axiom,
% 5.82/1.46 (![VTable0:vTable]:
% 5.82/1.46 ( ?[Val0:vAttrL,VwildcardName00:vRawTable]:
% 5.82/1.46 ( ( ( vgetAttrL @ VTable0 ) = ( Val0 ) ) &
% 5.82/1.46 ( ( VTable0 ) = ( vtable @ Val0 @ VwildcardName00 ) ) ) ))).
% 5.82/1.46 thf(zip_derived_cl53, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (sk__24 @ X0) @ (sk__25 @ X0)))),
% 5.82/1.46 inference('cnf', [status(esa)], [getAttrL-INV])).
% 5.82/1.46 thf(zip_derived_cl54, plain,
% 5.82/1.46 (![X0 : vTable]: ((vgetAttrL @ X0) = (sk__24 @ X0))),
% 5.82/1.46 inference('cnf', [status(esa)], [getAttrL-INV])).
% 5.82/1.46 thf(zip_derived_cl514, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (vgetAttrL @ X0) @ (sk__25 @ X0)))),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl53, zip_derived_cl54])).
% 5.82/1.46 thf(zip_derived_cl505, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vRawTable, X2 : vAttrL]:
% 5.82/1.46 (((vtable @ X2 @ X1) != (X0)) | ((X2) = (sk__17 @ X0)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl38])).
% 5.82/1.46 thf(zip_derived_cl522, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vTable]:
% 5.82/1.46 (((X0) != (X1)) | ((vgetAttrL @ X0) = (sk__17 @ X1)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl514, zip_derived_cl505])).
% 5.82/1.46 thf(zip_derived_cl526, plain,
% 5.82/1.46 (![X0 : vTable]: ((vgetAttrL @ X0) = (sk__17 @ X0))),
% 5.82/1.46 inference('eq_res', [status(thm)], [zip_derived_cl522])).
% 5.82/1.46 thf(zip_derived_cl1284, plain,
% 5.82/1.46 (((sk__54 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281)
% 5.82/1.46 = (vgetAttrL @ (vfilterTable @ sk__282 @ sk__283)))),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl1274, zip_derived_cl526])).
% 5.82/1.46 thf(zip_derived_cl953, plain,
% 5.82/1.46 (((sk__281) = (sk__53 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl100, zip_derived_cl471])).
% 5.82/1.46 thf(zip_derived_cl1192, plain,
% 5.82/1.46 (((vfilterTable @ sk__282 @ sk__283)
% 5.82/1.46 = (vtable @ (sk__54 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281) @
% 5.82/1.46 (sk__55 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl101, zip_derived_cl471])).
% 5.82/1.46 thf('getRaw-0', axiom,
% 5.82/1.46 (![VwildcardName0:vAttrL,Vrt:vRawTable]:
% 5.82/1.46 ( ( vgetRaw @ ( vtable @ VwildcardName0 @ Vrt ) ) = ( Vrt ) ))).
% 5.82/1.46 thf(zip_derived_cl49, plain,
% 5.82/1.46 (![X0 : vRawTable, X1 : vAttrL]: ((vgetRaw @ (vtable @ X1 @ X0)) = (X0))),
% 5.82/1.46 inference('cnf', [status(esa)], [getRaw-0])).
% 5.82/1.46 thf(zip_derived_cl1268, plain,
% 5.82/1.46 (((vgetRaw @ (vfilterTable @ sk__282 @ sk__283))
% 5.82/1.46 = (sk__55 @ (vfilterTable @ sk__282 @ sk__283) @ sk__281))),
% 5.82/1.46 inference('sup+', [status(thm)], [zip_derived_cl1192, zip_derived_cl49])).
% 5.82/1.46 thf(zip_derived_cl1349, plain,
% 5.82/1.46 ((~ (vmatchingAttrL @ sk__281 @
% 5.82/1.46 (vgetAttrL @ (vfilterTable @ sk__282 @ sk__283)))
% 5.82/1.46 | ~ (vwelltypedRawtable @ sk__281 @
% 5.82/1.46 (vgetRaw @ (vfilterTable @ sk__282 @ sk__283))))),
% 5.82/1.46 inference('demod', [status(thm)],
% 5.82/1.46 [zip_derived_cl1348, zip_derived_cl953, zip_derived_cl1284,
% 5.82/1.46 zip_derived_cl953, zip_derived_cl1268])).
% 5.82/1.46 thf('getRaw-INV', axiom,
% 5.82/1.46 (![VTable0:vTable]:
% 5.82/1.46 ( ?[VwildcardName00:vAttrL,Vrt0:vRawTable]:
% 5.82/1.46 ( ( ( vgetRaw @ VTable0 ) = ( Vrt0 ) ) &
% 5.82/1.46 ( ( VTable0 ) = ( vtable @ VwildcardName00 @ Vrt0 ) ) ) ))).
% 5.82/1.46 thf(zip_derived_cl50, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (sk__22 @ X0) @ (sk__23 @ X0)))),
% 5.82/1.46 inference('cnf', [status(esa)], [getRaw-INV])).
% 5.82/1.46 thf(zip_derived_cl51, plain,
% 5.82/1.46 (![X0 : vTable]: ((vgetRaw @ X0) = (sk__23 @ X0))),
% 5.82/1.46 inference('cnf', [status(esa)], [getRaw-INV])).
% 5.82/1.46 thf(zip_derived_cl509, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (sk__22 @ X0) @ (vgetRaw @ X0)))),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl50, zip_derived_cl51])).
% 5.82/1.46 thf(zip_derived_cl509, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (sk__22 @ X0) @ (vgetRaw @ X0)))),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl50, zip_derived_cl51])).
% 5.82/1.46 thf(zip_derived_cl505, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vRawTable, X2 : vAttrL]:
% 5.82/1.46 (((vtable @ X2 @ X1) != (X0)) | ((X2) = (sk__17 @ X0)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl37, zip_derived_cl38])).
% 5.82/1.46 thf(zip_derived_cl524, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vTable]:
% 5.82/1.46 (((X0) != (X1)) | ((sk__22 @ X0) = (sk__17 @ X1)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl509, zip_derived_cl505])).
% 5.82/1.46 thf(zip_derived_cl528, plain,
% 5.82/1.46 (![X0 : vTable]: ((sk__22 @ X0) = (sk__17 @ X0))),
% 5.82/1.46 inference('eq_res', [status(thm)], [zip_derived_cl524])).
% 5.82/1.46 thf(zip_derived_cl526, plain,
% 5.82/1.46 (![X0 : vTable]: ((vgetAttrL @ X0) = (sk__17 @ X0))),
% 5.82/1.46 inference('eq_res', [status(thm)], [zip_derived_cl522])).
% 5.82/1.46 thf(zip_derived_cl529, plain,
% 5.82/1.46 (![X0 : vTable]: ((sk__22 @ X0) = (vgetAttrL @ X0))),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl528, zip_derived_cl526])).
% 5.82/1.46 thf(zip_derived_cl530, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (vgetAttrL @ X0) @ (vgetRaw @ X0)))),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl509, zip_derived_cl529])).
% 5.82/1.46 thf('filterTable-0', axiom,
% 5.82/1.46 (![Val:vAttrL,Vrt:vRawTable,Vp:vPred]:
% 5.82/1.46 ( ( vfilterTable @ ( vtable @ Val @ Vrt ) @ Vp ) =
% 5.82/1.46 ( vtable @ Val @ ( vfilterRows @ Vrt @ Val @ Vp ) ) ))).
% 5.82/1.46 thf(zip_derived_cl262, plain,
% 5.82/1.46 (![X0 : vAttrL, X1 : vRawTable, X2 : vPred]:
% 5.82/1.46 ((vfilterTable @ (vtable @ X0 @ X1) @ X2)
% 5.82/1.46 = (vtable @ X0 @ (vfilterRows @ X1 @ X0 @ X2)))),
% 5.82/1.46 inference('cnf', [status(esa)], [filterTable-0])).
% 5.82/1.46 thf(zip_derived_cl1288, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vPred]:
% 5.82/1.46 ((vfilterTable @ X0 @ X1)
% 5.82/1.46 = (vtable @ (vgetAttrL @ X0) @
% 5.82/1.46 (vfilterRows @ (vgetRaw @ X0) @ (vgetAttrL @ X0) @ X1)))),
% 5.82/1.46 inference('sup+', [status(thm)], [zip_derived_cl530, zip_derived_cl262])).
% 5.82/1.46 thf('getAttrL-0', axiom,
% 5.82/1.46 (![Val:vAttrL,VwildcardName0:vRawTable]:
% 5.82/1.46 ( ( vgetAttrL @ ( vtable @ Val @ VwildcardName0 ) ) = ( Val ) ))).
% 5.82/1.46 thf(zip_derived_cl52, plain,
% 5.82/1.46 (![X0 : vAttrL, X1 : vRawTable]:
% 5.82/1.46 ((vgetAttrL @ (vtable @ X0 @ X1)) = (X0))),
% 5.82/1.46 inference('cnf', [status(esa)], [getAttrL-0])).
% 5.82/1.46 thf(zip_derived_cl472, plain, ( (vwelltypedtable @ sk__281 @ sk__282)),
% 5.82/1.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.82/1.46 thf(zip_derived_cl530, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (vgetAttrL @ X0) @ (vgetRaw @ X0)))),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl509, zip_derived_cl529])).
% 5.82/1.46 thf('welltypedtable-0', axiom,
% 5.82/1.46 (![Vtt:vTType,Val:vAttrL,Vt1:vRawTable]:
% 5.82/1.46 ( ( vwelltypedtable @ Vtt @ ( vtable @ Val @ Vt1 ) ) <=>
% 5.82/1.46 ( ( vmatchingAttrL @ Vtt @ Val ) & ( vwelltypedRawtable @ Vtt @ Vt1 ) ) ))).
% 5.82/1.46 thf(zip_derived_cl93, plain,
% 5.82/1.46 (![X0 : vTType, X1 : vAttrL, X2 : vRawTable]:
% 5.82/1.46 ( (vmatchingAttrL @ X0 @ X1)
% 5.82/1.46 | ~ (vwelltypedtable @ X0 @ (vtable @ X1 @ X2)))),
% 5.82/1.46 inference('cnf', [status(esa)], [welltypedtable-0])).
% 5.82/1.46 thf(zip_derived_cl561, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vTType]:
% 5.82/1.46 (~ (vwelltypedtable @ X1 @ X0)
% 5.82/1.46 | (vmatchingAttrL @ X1 @ (vgetAttrL @ X0)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl530, zip_derived_cl93])).
% 5.82/1.46 thf(zip_derived_cl599, plain,
% 5.82/1.46 ( (vmatchingAttrL @ sk__281 @ (vgetAttrL @ sk__282))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl472, zip_derived_cl561])).
% 5.82/1.46 thf(zip_derived_cl1288, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vPred]:
% 5.82/1.46 ((vfilterTable @ X0 @ X1)
% 5.82/1.46 = (vtable @ (vgetAttrL @ X0) @
% 5.82/1.46 (vfilterRows @ (vgetRaw @ X0) @ (vgetAttrL @ X0) @ X1)))),
% 5.82/1.46 inference('sup+', [status(thm)], [zip_derived_cl530, zip_derived_cl262])).
% 5.82/1.46 thf(zip_derived_cl49, plain,
% 5.82/1.46 (![X0 : vRawTable, X1 : vAttrL]: ((vgetRaw @ (vtable @ X1 @ X0)) = (X0))),
% 5.82/1.46 inference('cnf', [status(esa)], [getRaw-0])).
% 5.82/1.46 thf(zip_derived_cl1360, plain,
% 5.82/1.46 (~ (vwelltypedRawtable @ sk__281 @
% 5.82/1.46 (vfilterRows @ (vgetRaw @ sk__282) @ (vgetAttrL @ sk__282) @ sk__283))),
% 5.82/1.46 inference('demod', [status(thm)],
% 5.82/1.46 [zip_derived_cl1349, zip_derived_cl1288, zip_derived_cl52,
% 5.82/1.46 zip_derived_cl599, zip_derived_cl1288, zip_derived_cl49])).
% 5.82/1.46 thf(zip_derived_cl3980, plain,
% 5.82/1.46 (~ (vwelltypedRawtable @ sk__281 @ (vgetRaw @ sk__282))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl470, zip_derived_cl1360])).
% 5.82/1.46 thf(zip_derived_cl472, plain, ( (vwelltypedtable @ sk__281 @ sk__282)),
% 5.82/1.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 5.82/1.46 thf(zip_derived_cl530, plain,
% 5.82/1.46 (![X0 : vTable]: ((X0) = (vtable @ (vgetAttrL @ X0) @ (vgetRaw @ X0)))),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl509, zip_derived_cl529])).
% 5.82/1.46 thf(zip_derived_cl94, plain,
% 5.82/1.46 (![X0 : vTType, X1 : vRawTable, X2 : vAttrL]:
% 5.82/1.46 ( (vwelltypedRawtable @ X0 @ X1)
% 5.82/1.46 | ~ (vwelltypedtable @ X0 @ (vtable @ X2 @ X1)))),
% 5.82/1.46 inference('cnf', [status(esa)], [welltypedtable-0])).
% 5.82/1.46 thf(zip_derived_cl562, plain,
% 5.82/1.46 (![X0 : vTable, X1 : vTType]:
% 5.82/1.46 (~ (vwelltypedtable @ X1 @ X0)
% 5.82/1.46 | (vwelltypedRawtable @ X1 @ (vgetRaw @ X0)))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl530, zip_derived_cl94])).
% 5.82/1.46 thf(zip_derived_cl600, plain,
% 5.82/1.46 ( (vwelltypedRawtable @ sk__281 @ (vgetRaw @ sk__282))),
% 5.82/1.46 inference('sup-', [status(thm)], [zip_derived_cl472, zip_derived_cl562])).
% 5.82/1.46 thf(zip_derived_cl3985, plain, ($false),
% 5.82/1.46 inference('demod', [status(thm)], [zip_derived_cl3980, zip_derived_cl600])).
% 5.82/1.46
% 5.82/1.46 % SZS output end Refutation
% 5.82/1.46
% 5.82/1.46
% 5.82/1.46 % Terminating...
% 6.51/1.55 % Runner terminated.
% 6.51/1.57 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------