%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM306_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.7EKBSEWejl true
% Computer : n023.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 173.86s 25.46s
% Output : Refutation 173.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM306_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.7EKBSEWejl true
% 0.16/0.34 % Computer : n023.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Mon May 4 20:43:08 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 % Running portfolio for 300 s
% 0.16/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Number of cores: 8
% 0.16/0.34 % Python version: Python 3.6.8
% 0.16/0.34 % Running in FO mode
% 0.54/0.63 % Total configuration time : 435
% 0.54/0.63 % Estimated wc time : 1092
% 0.54/0.63 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.70 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.55/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.55/0.73 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.55/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 173.86/25.46 % Solved by fo/fo6_bce.sh.
% 173.86/25.46 % BCE start: 961
% 173.86/25.46 % BCE eliminated: 0
% 173.86/25.46 % PE start: 961
% 173.86/25.46 logic: eq
% 173.86/25.46 % PE eliminated: -186
% 173.86/25.46 % done 11362 iterations in 24.753s
% 173.86/25.46 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 173.86/25.46 % SZS output start Refutation
% 173.86/25.46 thf(vOptRawTable_type, type, vOptRawTable: $tType).
% 173.86/25.46 thf(vAttrL_type, type, vAttrL: $tType).
% 173.86/25.46 thf(vTable_type, type, vTable: $tType).
% 173.86/25.46 thf(vRawTable_type, type, vRawTable: $tType).
% 173.86/25.46 thf(vTType_type, type, vTType: $tType).
% 173.86/25.46 thf(vOptTType_type, type, vOptTType: $tType).
% 173.86/25.46 thf(vSelect_type, type, vSelect: $tType).
% 173.86/25.46 thf(vOptTable_type, type, vOptTable: $tType).
% 173.86/25.46 thf(vsomeTable_type, type, vsomeTable: vTable > vOptTable).
% 173.86/25.46 thf(vlist_type, type, vlist: vAttrL > vSelect).
% 173.86/25.46 thf(vmatchingAttrL_type, type, vmatchingAttrL: vTType > vAttrL > $o).
% 173.86/25.46 thf(vgetAttrL_type, type, vgetAttrL: vTable > vAttrL).
% 173.86/25.46 thf(sk__548_type, type, sk__548: vTType).
% 173.86/25.46 thf(vwelltypedtable_type, type, vwelltypedtable: vTType > vTable > $o).
% 173.86/25.46 thf(vnoRawTable_type, type, vnoRawTable: vOptRawTable).
% 173.86/25.46 thf(sk__50_type, type, sk__50: vTable > vRawTable).
% 173.86/25.46 thf(sk__544_type, type, sk__544: vAttrL > vRawTable > vAttrL > vRawTable).
% 173.86/25.46 thf(vprojectCols_type, type, vprojectCols: vAttrL > vAttrL > vRawTable > vOptRawTable).
% 173.86/25.46 thf(visSomeRawTable_type, type, visSomeRawTable: vOptRawTable > $o).
% 173.86/25.46 thf(vprojectTable_type, type, vprojectTable: vSelect > vTable > vOptTable).
% 173.86/25.46 thf(vgetRaw_type, type, vgetRaw: vTable > vRawTable).
% 173.86/25.46 thf(vprojectTypeAttrL_type, type, vprojectTypeAttrL: vAttrL > vTType > vOptTType).
% 173.86/25.46 thf(sk__546_type, type, sk__546: vTable).
% 173.86/25.46 thf(vprojectType_type, type, vprojectType: vSelect > vTType > vOptTType).
% 173.86/25.46 thf(sk__547_type, type, sk__547: vTType).
% 173.86/25.46 thf(vtable_type, type, vtable: vAttrL > vRawTable > vTable).
% 173.86/25.46 thf(sk__545_type, type, sk__545: vAttrL).
% 173.86/25.46 thf(vwelltypedRawtable_type, type, vwelltypedRawtable: vTType > vRawTable > $o).
% 173.86/25.46 thf(sk__49_type, type, sk__49: vTable > vAttrL).
% 173.86/25.46 thf(vsomeTType_type, type, vsomeTType: vTType > vOptTType).
% 173.86/25.46 thf(vsomeRawTable_type, type, vsomeRawTable: vRawTable > vOptRawTable).
% 173.86/25.46 thf('projectTableProgress-list-isSomeRawTable-False', conjecture,
% 173.86/25.46 (![Val:vAttrL,Vt:vTable,Vtt:vTType,Vtt2:vTType]:
% 173.86/25.46 ( ( ( ~( visSomeRawTable @
% 173.86/25.46 ( vprojectCols @ Val @ ( vgetAttrL @ Vt ) @ ( vgetRaw @ Vt ) ) ) ) &
% 173.86/25.46 ( vwelltypedtable @ Vtt @ Vt ) &
% 173.86/25.46 ( ( vprojectType @ ( vlist @ Val ) @ Vtt ) = ( vsomeTType @ Vtt2 ) ) ) =>
% 173.86/25.46 ( ?[Vt200:vTable]:
% 173.86/25.46 ( ( vprojectTable @ ( vlist @ Val ) @ Vt ) = ( vsomeTable @ Vt200 ) ) ) ))).
% 173.86/25.46 thf(zf_stmt_0, negated_conjecture,
% 173.86/25.46 (~( ![Val:vAttrL,Vt:vTable,Vtt:vTType,Vtt2:vTType]:
% 173.86/25.46 ( ( ( ~( visSomeRawTable @
% 173.86/25.46 ( vprojectCols @ Val @ ( vgetAttrL @ Vt ) @ ( vgetRaw @ Vt ) ) ) ) &
% 173.86/25.46 ( vwelltypedtable @ Vtt @ Vt ) &
% 173.86/25.46 ( ( vprojectType @ ( vlist @ Val ) @ Vtt ) = ( vsomeTType @ Vtt2 ) ) ) =>
% 173.86/25.46 ( ?[Vt200:vTable]:
% 173.86/25.46 ( ( vprojectTable @ ( vlist @ Val ) @ Vt ) = ( vsomeTable @ Vt200 ) ) ) ) )),
% 173.86/25.46 inference('cnf.neg', [status(esa)],
% 173.86/25.46 [projectTableProgress-list-isSomeRawTable-False])).
% 173.86/25.46 thf(zip_derived_cl959, plain, ( (vwelltypedtable @ sk__547 @ sk__546)),
% 173.86/25.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 173.86/25.46 thf('getRaw-INV', axiom,
% 173.86/25.46 (![VTable0:vTable]:
% 173.86/25.46 ( ?[VwildcardName00:vAttrL,Vrt0:vRawTable]:
% 173.86/25.46 ( ( ( vgetRaw @ VTable0 ) = ( Vrt0 ) ) &
% 173.86/25.46 ( ( VTable0 ) = ( vtable @ VwildcardName00 @ Vrt0 ) ) ) ))).
% 173.86/25.46 thf(zip_derived_cl123, plain,
% 173.86/25.46 (![X0 : vTable]: ((X0) = (vtable @ (sk__49 @ X0) @ (sk__50 @ X0)))),
% 173.86/25.46 inference('cnf', [status(esa)], [getRaw-INV])).
% 173.86/25.46 thf(zip_derived_cl124, plain,
% 173.86/25.46 (![X0 : vTable]: ((vgetRaw @ X0) = (sk__50 @ X0))),
% 173.86/25.46 inference('cnf', [status(esa)], [getRaw-INV])).
% 173.86/25.46 thf(zip_derived_cl10352, plain,
% 173.86/25.46 (![X0 : vTable]: ((X0) = (vtable @ (sk__49 @ X0) @ (vgetRaw @ X0)))),
% 173.86/25.46 inference('demod', [status(thm)], [zip_derived_cl123, zip_derived_cl124])).
% 173.86/25.46 thf(zip_derived_cl10352, plain,
% 173.86/25.46 (![X0 : vTable]: ((X0) = (vtable @ (sk__49 @ X0) @ (vgetRaw @ X0)))),
% 173.86/25.46 inference('demod', [status(thm)], [zip_derived_cl123, zip_derived_cl124])).
% 173.86/25.46 thf('getAttrL-0', axiom,
% 173.86/25.46 (![Val:vAttrL,VwildcardName0:vRawTable]:
% 173.86/25.46 ( ( vgetAttrL @ ( vtable @ Val @ VwildcardName0 ) ) = ( Val ) ))).
% 173.86/25.46 thf(zip_derived_cl125, plain,
% 173.86/25.46 (![X0 : vAttrL, X1 : vRawTable]:
% 173.86/25.46 ((vgetAttrL @ (vtable @ X0 @ X1)) = (X0))),
% 173.86/25.46 inference('cnf', [status(esa)], [getAttrL-0])).
% 173.86/25.46 thf(zip_derived_cl10363, plain,
% 173.86/25.46 (![X0 : vTable]: ((vgetAttrL @ X0) = (sk__49 @ X0))),
% 173.86/25.46 inference('s_sup+', [status(thm)],
% 173.86/25.46 [zip_derived_cl10352, zip_derived_cl125])).
% 173.86/25.46 thf(zip_derived_cl10380, plain,
% 173.86/25.46 (![X0 : vTable]: ((X0) = (vtable @ (vgetAttrL @ X0) @ (vgetRaw @ X0)))),
% 173.86/25.46 inference('demod', [status(thm)],
% 173.86/25.46 [zip_derived_cl10352, zip_derived_cl10363])).
% 173.86/25.46 thf('welltypedtable-0', axiom,
% 173.86/25.46 (![Vtt:vTType,Val:vAttrL,Vt1:vRawTable]:
% 173.86/25.46 ( ( vwelltypedtable @ Vtt @ ( vtable @ Val @ Vt1 ) ) <=>
% 173.86/25.46 ( ( vmatchingAttrL @ Vtt @ Val ) & ( vwelltypedRawtable @ Vtt @ Vt1 ) ) ))).
% 173.86/25.46 thf(zip_derived_cl190, plain,
% 173.86/25.46 (![X0 : vTType, X1 : vAttrL, X2 : vRawTable]:
% 173.86/25.46 ( (vmatchingAttrL @ X0 @ X1)
% 173.86/25.46 | ~ (vwelltypedtable @ X0 @ (vtable @ X1 @ X2)))),
% 173.86/25.46 inference('cnf', [status(esa)], [welltypedtable-0])).
% 173.86/25.46 thf(zip_derived_cl10503, plain,
% 173.86/25.46 (![X0 : vTable, X1 : vTType]:
% 173.86/25.46 ( (vmatchingAttrL @ X1 @ (vgetAttrL @ X0))
% 173.86/25.46 | ~ (vwelltypedtable @ X1 @ X0))),
% 173.86/25.46 inference('s_sup-', [status(thm)],
% 173.86/25.46 [zip_derived_cl10380, zip_derived_cl190])).
% 173.86/25.46 thf(zip_derived_cl959, plain, ( (vwelltypedtable @ sk__547 @ sk__546)),
% 173.86/25.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 173.86/25.46 thf(zip_derived_cl10380, plain,
% 173.86/25.46 (![X0 : vTable]: ((X0) = (vtable @ (vgetAttrL @ X0) @ (vgetRaw @ X0)))),
% 173.86/25.46 inference('demod', [status(thm)],
% 173.86/25.46 [zip_derived_cl10352, zip_derived_cl10363])).
% 173.86/25.46 thf(zip_derived_cl191, plain,
% 173.86/25.46 (![X0 : vTType, X1 : vRawTable, X2 : vAttrL]:
% 173.86/25.46 ( (vwelltypedRawtable @ X0 @ X1)
% 173.86/25.46 | ~ (vwelltypedtable @ X0 @ (vtable @ X2 @ X1)))),
% 173.86/25.46 inference('cnf', [status(esa)], [welltypedtable-0])).
% 173.86/25.46 thf(zip_derived_cl10511, plain,
% 173.86/25.46 (![X0 : vTable, X1 : vTType]:
% 173.86/25.46 ( (vwelltypedRawtable @ X1 @ (vgetRaw @ X0))
% 173.86/25.46 | ~ (vwelltypedtable @ X1 @ X0))),
% 173.86/25.46 inference('s_sup-', [status(thm)],
% 173.86/25.46 [zip_derived_cl10380, zip_derived_cl191])).
% 173.86/25.46 thf(zip_derived_cl957, plain,
% 173.86/25.46 (((vprojectType @ (vlist @ sk__545) @ sk__547) = (vsomeTType @ sk__548))),
% 173.86/25.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 173.86/25.46 thf('projectType-1', axiom,
% 173.86/25.46 (![Val:vAttrL,Vtt1:vTType]:
% 173.86/25.46 ( ( vprojectType @ ( vlist @ Val ) @ Vtt1 ) =
% 173.86/25.46 ( vprojectTypeAttrL @ Val @ Vtt1 ) ))).
% 173.86/25.46 thf(zip_derived_cl813, plain,
% 173.86/25.46 (![X0 : vAttrL, X1 : vTType]:
% 173.86/25.46 ((vprojectType @ (vlist @ X0) @ X1) = (vprojectTypeAttrL @ X0 @ X1))),
% 173.86/25.46 inference('cnf', [status(esa)], [projectType-1])).
% 173.86/25.46 thf(zip_derived_cl10817, plain,
% 173.86/25.46 (((vsomeTType @ sk__548) = (vprojectTypeAttrL @ sk__545 @ sk__547))),
% 173.86/25.46 inference('s_sup+', [status(thm)], [zip_derived_cl957, zip_derived_cl813])).
% 173.86/25.46 thf(projectColsProgress, axiom,
% 173.86/25.46 (![Valt:vAttrL,Vrt:vRawTable,Vtt2:vTType,Val:vAttrL,Vtt:vTType]:
% 173.86/25.46 ( ( ( vwelltypedRawtable @ Vtt @ Vrt ) &
% 173.86/25.46 ( vmatchingAttrL @ Vtt @ Valt ) &
% 173.86/25.46 ( ( vprojectTypeAttrL @ Val @ Vtt ) = ( vsomeTType @ Vtt2 ) ) ) =>
% 173.86/25.46 ( ?[Vrt2:vRawTable]:
% 173.86/25.46 ( ( vprojectCols @ Val @ Valt @ Vrt ) = ( vsomeRawTable @ Vrt2 ) ) ) ))).
% 173.86/25.46 thf(zip_derived_cl954, plain,
% 173.86/25.46 (![X0 : vAttrL, X1 : vRawTable, X2 : vAttrL, X3 : vTType, X4 : vTType]:
% 173.86/25.46 (((vprojectCols @ X0 @ X2 @ X1)
% 173.86/25.46 = (vsomeRawTable @ (sk__544 @ X0 @ X1 @ X2)))
% 173.86/25.46 | ~ (vwelltypedRawtable @ X3 @ X1)
% 173.86/25.46 | ~ (vmatchingAttrL @ X3 @ X2)
% 173.86/25.46 | ((vprojectTypeAttrL @ X0 @ X3) != (vsomeTType @ X4)))),
% 173.86/25.46 inference('cnf', [status(esa)], [projectColsProgress])).
% 173.86/25.46 thf(zip_derived_cl14408, plain,
% 173.86/25.46 (![X0 : vTType, X1 : vRawTable, X2 : vAttrL]:
% 173.86/25.46 (((vprojectCols @ sk__545 @ X2 @ X1)
% 173.86/25.46 = (vsomeRawTable @ (sk__544 @ sk__545 @ X1 @ X2)))
% 173.86/25.46 | ~ (vwelltypedRawtable @ sk__547 @ X1)
% 173.86/25.46 | ~ (vmatchingAttrL @ sk__547 @ X2)
% 173.86/25.46 | ((vsomeTType @ sk__548) != (vsomeTType @ X0)))),
% 173.86/25.46 inference('s_sup-', [status(thm)],
% 173.86/25.46 [zip_derived_cl10817, zip_derived_cl954])).
% 173.86/25.46 thf(zip_derived_cl31762, plain,
% 173.86/25.46 (![X0 : vTable, X1 : vAttrL, X2 : vTType]:
% 173.86/25.46 (~ (vwelltypedtable @ sk__547 @ X0)
% 173.86/25.46 | ((vprojectCols @ sk__545 @ X1 @ (vgetRaw @ X0))
% 173.86/25.46 = (vsomeRawTable @ (sk__544 @ sk__545 @ (vgetRaw @ X0) @ X1)))
% 173.86/25.46 | ~ (vmatchingAttrL @ sk__547 @ X1)
% 173.86/25.46 | ((vsomeTType @ sk__548) != (vsomeTType @ X2)))),
% 173.86/25.46 inference('s_sup-', [status(thm)],
% 173.86/25.46 [zip_derived_cl10511, zip_derived_cl14408])).
% 173.86/25.46 thf(zip_derived_cl33098, plain,
% 173.86/25.46 (![X0 : vAttrL, X1 : vTType]:
% 173.86/25.46 (((vprojectCols @ sk__545 @ X0 @ (vgetRaw @ sk__546))
% 173.86/25.46 = (vsomeRawTable @ (sk__544 @ sk__545 @ (vgetRaw @ sk__546) @ X0)))
% 173.86/25.46 | ~ (vmatchingAttrL @ sk__547 @ X0)
% 173.86/25.46 | ((vsomeTType @ sk__548) != (vsomeTType @ X1)))),
% 173.86/25.46 inference('s_sup-', [status(thm)],
% 173.86/25.46 [zip_derived_cl959, zip_derived_cl31762])).
% 173.86/25.46 thf(zip_derived_cl40714, plain,
% 173.86/25.46 (![X0 : vTable, X1 : vTType]:
% 173.86/25.46 (~ (vwelltypedtable @ sk__547 @ X0)
% 173.86/25.46 | ((vprojectCols @ sk__545 @ (vgetAttrL @ X0) @ (vgetRaw @ sk__546))
% 173.86/25.46 = (vsomeRawTable @
% 173.86/25.46 (sk__544 @ sk__545 @ (vgetRaw @ sk__546) @ (vgetAttrL @ X0))))
% 173.86/25.46 | ((vsomeTType @ sk__548) != (vsomeTType @ X1)))),
% 173.86/25.46 inference('s_sup-', [status(thm)],
% 173.86/25.46 [zip_derived_cl10503, zip_derived_cl33098])).
% 173.86/25.46 thf(zip_derived_cl76800, plain,
% 173.86/25.46 (![X0 : vTType]:
% 173.86/25.46 (((vprojectCols @ sk__545 @ (vgetAttrL @ sk__546) @
% 173.86/25.46 (vgetRaw @ sk__546))
% 173.86/25.46 = (vsomeRawTable @
% 173.86/25.46 (sk__544 @ sk__545 @ (vgetRaw @ sk__546) @ (vgetAttrL @ sk__546))))
% 173.86/25.46 | ((vsomeTType @ sk__548) != (vsomeTType @ X0)))),
% 173.86/25.46 inference('s_sup-', [status(thm)],
% 173.86/25.46 [zip_derived_cl959, zip_derived_cl40714])).
% 173.86/25.46 thf('isSomeRawTable-false-INV', axiom,
% 173.86/25.46 (![VOptRawTable0:vOptRawTable]:
% 173.86/25.46 ( ( ~( visSomeRawTable @ VOptRawTable0 ) ) =>
% 173.86/25.46 ( ( VOptRawTable0 ) = ( vnoRawTable ) ) ))).
% 173.86/25.46 thf(zip_derived_cl238, plain,
% 173.86/25.46 (![X0 : vOptRawTable]: (((X0) = (vnoRawTable)) | (visSomeRawTable @ X0))),
% 173.86/25.46 inference('cnf', [status(esa)], [isSomeRawTable-false-INV])).
% 173.86/25.46 thf(zip_derived_cl958, plain,
% 173.86/25.46 (~ (visSomeRawTable @
% 173.86/25.46 (vprojectCols @ sk__545 @ (vgetAttrL @ sk__546) @ (vgetRaw @ sk__546)))),
% 173.86/25.46 inference('cnf', [status(esa)], [zf_stmt_0])).
% 173.86/25.46 thf(zip_derived_cl10201, plain,
% 173.86/25.46 (((vprojectCols @ sk__545 @ (vgetAttrL @ sk__546) @ (vgetRaw @ sk__546))
% 173.86/25.46 = (vnoRawTable))),
% 173.86/25.46 inference('s_sup-', [status(thm)], [zip_derived_cl238, zip_derived_cl958])).
% 173.86/25.46 thf(zip_derived_cl76805, plain,
% 173.86/25.46 (![X0 : vTType]:
% 173.86/25.46 (((vnoRawTable)
% 173.86/25.46 = (vsomeRawTable @
% 173.86/25.46 (sk__544 @ sk__545 @ (vgetRaw @ sk__546) @ (vgetAttrL @ sk__546))))
% 173.86/25.46 | ((vsomeTType @ sk__548) != (vsomeTType @ X0)))),
% 173.86/25.46 inference('demod', [status(thm)],
% 173.86/25.46 [zip_derived_cl76800, zip_derived_cl10201])).
% 173.86/25.46 thf('DIFF-noRawTable-someRawTable', axiom,
% 173.86/25.46 (![VRawTable0:vRawTable]:
% 173.86/25.46 ( ( vnoRawTable ) != ( vsomeRawTable @ VRawTable0 ) ))).
% 173.86/25.46 thf(zip_derived_cl39, plain,
% 173.86/25.46 (![X0 : vRawTable]: ((vnoRawTable) != (vsomeRawTable @ X0))),
% 173.86/25.46 inference('cnf', [status(esa)], [DIFF-noRawTable-someRawTable])).
% 173.86/25.46 thf(zip_derived_cl76806, plain,
% 173.86/25.46 (![X0 : vTType]: ((vsomeTType @ sk__548) != (vsomeTType @ X0))),
% 173.86/25.46 inference('simplify_reflect-', [status(thm)],
% 173.86/25.46 [zip_derived_cl76805, zip_derived_cl39])).
% 173.86/25.46 thf(zip_derived_cl76834, plain, ($false),
% 173.86/25.46 inference('eq_res', [status(thm)], [zip_derived_cl76806])).
% 173.86/25.46
% 173.86/25.46 % SZS output end Refutation
% 173.86/25.46
% 173.86/25.46
% 173.86/25.46 % Terminating...
% 174.57/25.58 % Runner terminated.
% 174.57/25.59 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------