%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM224_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.mB4C8vv2eX true
% Computer : n010.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:19 PM UTC 2026
% Result : Theorem 0.58s 0.85s
% Output : Refutation 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : COM224_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.mB4C8vv2eX true
% 0.16/0.34 % Computer : n010.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 19:08:06 EDT 2026
% 0.16/0.35 % CPUTime :
% 0.16/0.35 % Running portfolio for 300 s
% 0.16/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.35 % Number of cores: 8
% 0.16/0.35 % Python version: Python 3.6.8
% 0.16/0.35 % Running in FO mode
% 0.56/0.65 % Total configuration time : 435
% 0.56/0.65 % Estimated wc time : 1092
% 0.56/0.65 % Estimated cpu time (7 cpus) : 156.0
% 0.56/0.71 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.56/0.74 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.56/0.74 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.56/0.76 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.56/0.77 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 0.58/0.85 % Solved by fo/fo1_av.sh.
% 0.58/0.85 % done 242 iterations in 0.090s
% 0.58/0.85 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.58/0.85 % SZS output start Refutation
% 0.58/0.85 thf(vTy_type, type, vTy: $tType).
% 0.58/0.85 thf(vTerm_type, type, vTerm: $tType).
% 0.58/0.85 thf(vOptTerm_type, type, vOptTerm: $tType).
% 0.58/0.85 thf(vB_type, type, vB: vTy).
% 0.58/0.85 thf(vSucc_type, type, vSucc: vTerm > vTerm).
% 0.58/0.85 thf(sk__99_type, type, sk__99: vTerm).
% 0.58/0.85 thf(vt1_type, type, vt1: vTerm).
% 0.58/0.85 thf(vreduce_type, type, vreduce: vTerm > vOptTerm).
% 0.58/0.85 thf(vsomeTerm_type, type, vsomeTerm: vTerm > vOptTerm).
% 0.58/0.85 thf(vptchecksimple_type, type, vptchecksimple: vTerm > vTy > $o).
% 0.58/0.85 thf(vZero_type, type, vZero: vTerm).
% 0.58/0.85 thf(vPred_type, type, vPred: vTerm > vTerm).
% 0.58/0.85 thf(vNat_type, type, vNat: vTy).
% 0.58/0.85 thf(vgetTerm_type, type, vgetTerm: vOptTerm > vTerm).
% 0.58/0.85 thf(sk__98_type, type, sk__98: vTy).
% 0.58/0.85 thf(visNV_type, type, visNV: vTerm > $o).
% 0.58/0.85 thf(sk__97_type, type, sk__97: vTerm).
% 0.58/0.85 thf('dom-Ty', axiom,
% 0.58/0.85 (![VX:vTy]: ( ( ( VX ) = ( vNat ) ) | ( ( VX ) = ( vB ) ) ))).
% 0.58/0.85 thf(zip_derived_cl40, plain,
% 0.58/0.85 (![X0 : vTy]: (((X0) = (vNat)) | ((X0) = (vB)))),
% 0.58/0.85 inference('cnf', [status(esa)], [dom-Ty])).
% 0.58/0.85 thf(zip_derived_cl40, plain,
% 0.58/0.85 (![X0 : vTy]: (((X0) = (vNat)) | ((X0) = (vB)))),
% 0.58/0.85 inference('cnf', [status(esa)], [dom-Ty])).
% 0.58/0.85 thf('Preservation-Pred-Succ-isNV-True', conjecture,
% 0.58/0.85 (![Vnv:vTerm,VT:vTy,Vtres:vTerm]:
% 0.58/0.85 ( ( ( visNV @ Vnv ) & ( ( vt1 ) != ( vZero ) ) &
% 0.58/0.85 ( ( vt1 ) = ( vSucc @ Vnv ) ) &
% 0.58/0.85 ( vptchecksimple @ ( vPred @ vt1 ) @ VT ) &
% 0.58/0.85 ( ( vreduce @ ( vPred @ vt1 ) ) = ( vsomeTerm @ Vtres ) ) ) =>
% 0.58/0.85 ( vptchecksimple @ Vtres @ VT ) ))).
% 0.58/0.85 thf(zf_stmt_0, negated_conjecture,
% 0.58/0.85 (~( ![Vnv:vTerm,VT:vTy,Vtres:vTerm]:
% 0.58/0.85 ( ( ( visNV @ Vnv ) & ( ( vt1 ) != ( vZero ) ) &
% 0.58/0.85 ( ( vt1 ) = ( vSucc @ Vnv ) ) &
% 0.58/0.85 ( vptchecksimple @ ( vPred @ vt1 ) @ VT ) &
% 0.58/0.85 ( ( vreduce @ ( vPred @ vt1 ) ) = ( vsomeTerm @ Vtres ) ) ) =>
% 0.58/0.85 ( vptchecksimple @ Vtres @ VT ) ) )),
% 0.58/0.85 inference('cnf.neg', [status(esa)], [Preservation-Pred-Succ-isNV-True])).
% 0.58/0.85 thf(zip_derived_cl263, plain, (~ (vptchecksimple @ sk__99 @ sk__98)),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.58/0.85 thf(zip_derived_cl293, plain,
% 0.58/0.85 ((((sk__98) = (vNat)) | ~ (vptchecksimple @ sk__99 @ vB))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl40, zip_derived_cl263])).
% 0.58/0.85 thf(zip_derived_cl476, plain,
% 0.58/0.85 ((((sk__98) = (vNat))) <= ((((sk__98) = (vNat))))),
% 0.58/0.85 inference('split', [status(esa)], [zip_derived_cl293])).
% 0.58/0.85 thf(zip_derived_cl263, plain, (~ (vptchecksimple @ sk__99 @ sk__98)),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.58/0.85 thf(zip_derived_cl480, plain,
% 0.58/0.85 ((~ (vptchecksimple @ sk__99 @ vNat)) <= ((((sk__98) = (vNat))))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl476, zip_derived_cl263])).
% 0.58/0.85 thf(zip_derived_cl482, plain,
% 0.58/0.85 ((![X0 : vTy]: (((X0) = (vB)) | ~ (vptchecksimple @ sk__99 @ X0)))
% 0.58/0.85 <= ((((sk__98) = (vNat))))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl40, zip_derived_cl480])).
% 0.58/0.85 thf(zip_derived_cl40, plain,
% 0.58/0.85 (![X0 : vTy]: (((X0) = (vNat)) | ((X0) = (vB)))),
% 0.58/0.85 inference('cnf', [status(esa)], [dom-Ty])).
% 0.58/0.85 thf(zip_derived_cl268, plain, ( (vptchecksimple @ (vPred @ vt1) @ sk__98)),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.58/0.85 thf(zip_derived_cl309, plain,
% 0.58/0.85 ((((sk__98) = (vNat)) | (vptchecksimple @ (vPred @ vt1) @ vB))),
% 0.58/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl40, zip_derived_cl268])).
% 0.58/0.85 thf(zip_derived_cl490, plain,
% 0.58/0.85 (( (vptchecksimple @ (vPred @ vt1) @ vB))
% 0.58/0.85 <= (( (vptchecksimple @ (vPred @ vt1) @ vB)))),
% 0.58/0.85 inference('split', [status(esa)], [zip_derived_cl309])).
% 0.58/0.85 thf(TPred_inv2, axiom,
% 0.58/0.85 (![Vt1:vTerm,VT:vTy]:
% 0.58/0.85 ( ( vptchecksimple @ ( vPred @ Vt1 ) @ VT ) => ( ( VT ) = ( vNat ) ) ))).
% 0.58/0.85 thf(zip_derived_cl253, plain,
% 0.58/0.85 (![X0 : vTy, X1 : vTerm]:
% 0.58/0.85 (((X0) = (vNat)) | ~ (vptchecksimple @ (vPred @ X1) @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [TPred_inv2])).
% 0.58/0.85 thf(zip_derived_cl498, plain,
% 0.58/0.85 ((((vB) = (vNat))) <= (( (vptchecksimple @ (vPred @ vt1) @ vB)))),
% 0.58/0.85 inference('s_sup-', [status(thm)], [zip_derived_cl490, zip_derived_cl253])).
% 0.58/0.85 thf('DIFF-B-Nat', axiom, (( vB ) != ( vNat ))).
% 0.58/0.85 thf(zip_derived_cl41, plain, (((vB) != (vNat))),
% 0.58/0.85 inference('cnf', [status(esa)], [DIFF-B-Nat])).
% 0.58/0.85 thf('0', plain, (~ ( (vptchecksimple @ (vPred @ vt1) @ vB))),
% 0.58/0.85 inference('simplify_reflect-', [status(thm)],
% 0.58/0.85 [zip_derived_cl498, zip_derived_cl41])).
% 0.58/0.85 thf('1', plain,
% 0.58/0.85 ((((sk__98) = (vNat))) | ( (vptchecksimple @ (vPred @ vt1) @ vB))),
% 0.58/0.85 inference('split', [status(esa)], [zip_derived_cl309])).
% 0.58/0.85 thf('2', plain, ((((sk__98) = (vNat)))),
% 0.58/0.85 inference('sat_resolution*', [status(thm)], ['0', '1'])).
% 0.58/0.85 thf(zip_derived_cl505, plain,
% 0.58/0.85 (![X0 : vTy]: (((X0) = (vB)) | ~ (vptchecksimple @ sk__99 @ X0))),
% 0.58/0.85 inference('simpl_trail', [status(thm)], [zip_derived_cl482, '2'])).
% 0.58/0.85 thf(zip_derived_cl264, plain,
% 0.58/0.85 (((vreduce @ (vPred @ vt1)) = (vsomeTerm @ sk__99))),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.58/0.85 thf(zip_derived_cl267, plain, (((vt1) = (vSucc @ sk__97))),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.58/0.85 thf('reduce-7', axiom,
% 0.58/0.85 (![Vnv:vTerm]:
% 0.58/0.85 ( ( visNV @ Vnv ) =>
% 0.58/0.85 ( ( vreduce @ ( vPred @ ( vSucc @ Vnv ) ) ) = ( vsomeTerm @ Vnv ) ) ))).
% 0.58/0.85 thf(zip_derived_cl105, plain,
% 0.58/0.85 (![X0 : vTerm]:
% 0.58/0.85 (((vreduce @ (vPred @ (vSucc @ X0))) = (vsomeTerm @ X0))
% 0.58/0.85 | ~ (visNV @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [reduce-7])).
% 0.58/0.85 thf(zip_derived_cl517, plain,
% 0.58/0.85 ((((vreduce @ (vPred @ vt1)) = (vsomeTerm @ sk__97)) | ~ (visNV @ sk__97))),
% 0.58/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl267, zip_derived_cl105])).
% 0.58/0.85 thf(zip_derived_cl265, plain, ( (visNV @ sk__97)),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.58/0.85 thf(zip_derived_cl519, plain,
% 0.58/0.85 (((vreduce @ (vPred @ vt1)) = (vsomeTerm @ sk__97))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl517, zip_derived_cl265])).
% 0.58/0.85 thf(zip_derived_cl534, plain,
% 0.58/0.85 (((vsomeTerm @ sk__97) = (vsomeTerm @ sk__99))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl264, zip_derived_cl519])).
% 0.58/0.85 thf('getTerm-0', axiom,
% 0.58/0.85 (![Vt:vTerm]: ( ( vgetTerm @ ( vsomeTerm @ Vt ) ) = ( Vt ) ))).
% 0.58/0.85 thf(zip_derived_cl42, plain,
% 0.58/0.85 (![X0 : vTerm]: ((vgetTerm @ (vsomeTerm @ X0)) = (X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [getTerm-0])).
% 0.58/0.85 thf(zip_derived_cl543, plain,
% 0.58/0.85 (((vgetTerm @ (vsomeTerm @ sk__97)) = (sk__99))),
% 0.58/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl534, zip_derived_cl42])).
% 0.58/0.85 thf(zip_derived_cl42, plain,
% 0.58/0.85 (![X0 : vTerm]: ((vgetTerm @ (vsomeTerm @ X0)) = (X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [getTerm-0])).
% 0.58/0.85 thf(zip_derived_cl546, plain, (((sk__97) = (sk__99))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl543, zip_derived_cl42])).
% 0.58/0.85 thf(zip_derived_cl548, plain,
% 0.58/0.85 (![X0 : vTy]: (((X0) = (vB)) | ~ (vptchecksimple @ sk__97 @ X0))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl505, zip_derived_cl546])).
% 0.58/0.85 thf(isNVisNat, axiom,
% 0.58/0.85 (![Vt:vTerm]: ( ( visNV @ Vt ) => ( vptchecksimple @ Vt @ vNat ) ))).
% 0.58/0.85 thf(zip_derived_cl262, plain,
% 0.58/0.85 (![X0 : vTerm]: ( (vptchecksimple @ X0 @ vNat) | ~ (visNV @ X0))),
% 0.58/0.85 inference('cnf', [status(esa)], [isNVisNat])).
% 0.58/0.85 thf(zip_derived_cl583, plain, ((((vNat) = (vB)) | ~ (visNV @ sk__97))),
% 0.58/0.85 inference('s_sup+', [status(thm)], [zip_derived_cl548, zip_derived_cl262])).
% 0.58/0.85 thf(zip_derived_cl265, plain, ( (visNV @ sk__97)),
% 0.58/0.85 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.58/0.85 thf(zip_derived_cl589, plain, (((vNat) = (vB))),
% 0.58/0.85 inference('demod', [status(thm)], [zip_derived_cl583, zip_derived_cl265])).
% 0.58/0.85 thf(zip_derived_cl41, plain, (((vB) != (vNat))),
% 0.58/0.85 inference('cnf', [status(esa)], [DIFF-B-Nat])).
% 0.58/0.85 thf(zip_derived_cl590, plain, ($false),
% 0.58/0.85 inference('simplify_reflect-', [status(thm)],
% 0.58/0.85 [zip_derived_cl589, zip_derived_cl41])).
% 0.58/0.85
% 0.58/0.85 % SZS output end Refutation
% 0.58/0.85
% 0.58/0.85
% 0.58/0.85 % Terminating...
% 0.61/0.96 % Runner terminated.
% 0.61/0.97 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------