%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM130+1 : TPTP v9.2.0. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.PTFrQGbST7 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 : Thu Oct 2 04:30:43 PM UTC 2025
% Result : Theorem 3.02s 1.31s
% Output : Refutation 3.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : COM130+1 : TPTP v9.2.0. Released v6.4.0.
% 0.00/0.11 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.PTFrQGbST7 true
% 0.10/0.31 % Computer : n007.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Wed Oct 1 13:50:38 EDT 2025
% 0.16/0.31 % CPUTime :
% 0.16/0.31 % Running portfolio for 300 s
% 0.16/0.31 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.31 % Number of cores: 8
% 0.16/0.32 % Python version: Python 3.6.8
% 0.16/0.32 % Running in FO mode
% 0.52/0.61 % Total configuration time : 435
% 0.52/0.61 % Estimated wc time : 1092
% 0.52/0.61 % Estimated cpu time (7 cpus) : 156.0
% 0.68/0.74 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.71/0.80 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.71/0.83 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.71/0.83 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.71/0.85 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.71/0.85 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.71/0.85 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 3.02/1.31 % Solved by fo/fo13.sh.
% 3.02/1.31 % done 224 iterations in 0.377s
% 3.02/1.31 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 3.02/1.31 % SZS output start Refutation
% 3.02/1.31 thf(sk__76_type, type, sk__76: $i).
% 3.02/1.31 thf(vabs_type, type, vabs: $i > $i > $i > $i).
% 3.02/1.31 thf(sk__78_type, type, sk__78: $i).
% 3.02/1.31 thf(sk__77_type, type, sk__77: $i).
% 3.02/1.31 thf(vsubst_type, type, vsubst: $i > $i > $i > $i).
% 3.02/1.31 thf(sk__80_type, type, sk__80: $i).
% 3.02/1.31 thf(vbind_type, type, vbind: $i > $i > $i > $i).
% 3.02/1.31 thf(sk__79_type, type, sk__79: $i).
% 3.02/1.31 thf(vtcheck_type, type, vtcheck: $i > $i > $i > $o).
% 3.02/1.31 thf(sk__74_type, type, sk__74: $i).
% 3.02/1.31 thf(visFreeVar_type, type, visFreeVar: $i > $i > $o).
% 3.02/1.31 thf(sk__75_type, type, sk__75: $i).
% 3.02/1.31 thf(sk__81_type, type, sk__81: $i).
% 3.02/1.31 thf('T-subst-abs-1', conjecture,
% 3.02/1.31 (![VT:$i,VC:$i,Vx:$i,Ve:$i,Vy:$i,VS:$i,Ve1:$i,VT2:$i]:
% 3.02/1.31 ( ( ( ( Vx ) = ( Vy ) ) & ( vtcheck @ VC @ Ve @ VT ) &
% 3.02/1.31 ( vtcheck @ ( vbind @ Vx @ VT @ VC ) @ ( vabs @ Vy @ VS @ Ve1 ) @ VT2 ) ) =>
% 3.02/1.31 ( vtcheck @ VC @ ( vsubst @ Vx @ Ve @ ( vabs @ Vy @ VS @ Ve1 ) ) @ VT2 ) ))).
% 3.02/1.31 thf(zf_stmt_0, negated_conjecture,
% 3.02/1.31 (~( ![VT:$i,VC:$i,Vx:$i,Ve:$i,Vy:$i,VS:$i,Ve1:$i,VT2:$i]:
% 3.02/1.31 ( ( ( ( Vx ) = ( Vy ) ) & ( vtcheck @ VC @ Ve @ VT ) &
% 3.02/1.31 ( vtcheck @
% 3.02/1.31 ( vbind @ Vx @ VT @ VC ) @ ( vabs @ Vy @ VS @ Ve1 ) @ VT2 ) ) =>
% 3.02/1.31 ( vtcheck @
% 3.02/1.31 VC @ ( vsubst @ Vx @ Ve @ ( vabs @ Vy @ VS @ Ve1 ) ) @ VT2 ) ) )),
% 3.02/1.31 inference('cnf.neg', [status(esa)], [T-subst-abs-1])).
% 3.02/1.31 thf(zip_derived_cl156, plain,
% 3.02/1.31 ( (vtcheck @ (vbind @ sk__76 @ sk__74 @ sk__75) @
% 3.02/1.31 (vabs @ sk__78 @ sk__79 @ sk__80) @ sk__81)),
% 3.02/1.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.02/1.31 thf(zip_derived_cl157, plain, (((sk__76) = (sk__78))),
% 3.02/1.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.02/1.31 thf(zip_derived_cl160, plain,
% 3.02/1.31 ( (vtcheck @ (vbind @ sk__76 @ sk__74 @ sk__75) @
% 3.02/1.31 (vabs @ sk__76 @ sk__79 @ sk__80) @ sk__81)),
% 3.02/1.31 inference('demod', [status(thm)], [zip_derived_cl156, zip_derived_cl157])).
% 3.02/1.31 thf('T-Strong', axiom,
% 3.02/1.31 (![Vx:$i,VS:$i,VC:$i,Ve:$i,VT:$i]:
% 3.02/1.31 ( ( ( ~( visFreeVar @ Vx @ Ve ) ) &
% 3.02/1.31 ( vtcheck @ ( vbind @ Vx @ VS @ VC ) @ Ve @ VT ) ) =>
% 3.02/1.31 ( vtcheck @ VC @ Ve @ VT ) ))).
% 3.02/1.31 thf(zip_derived_cl152, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 3.02/1.31 ( (visFreeVar @ X0 @ X1)
% 3.02/1.31 | ~ (vtcheck @ (vbind @ X0 @ X2 @ X3) @ X1 @ X4)
% 3.02/1.31 | (vtcheck @ X3 @ X1 @ X4))),
% 3.02/1.31 inference('cnf', [status(esa)], [T-Strong])).
% 3.02/1.31 thf(zip_derived_cl371, plain,
% 3.02/1.31 (( (visFreeVar @ sk__76 @ (vabs @ sk__76 @ sk__79 @ sk__80))
% 3.02/1.31 | (vtcheck @ sk__75 @ (vabs @ sk__76 @ sk__79 @ sk__80) @ sk__81))),
% 3.02/1.31 inference('s_sup-', [status(thm)], [zip_derived_cl160, zip_derived_cl152])).
% 3.02/1.31 thf(zip_derived_cl155, plain,
% 3.02/1.31 (~ (vtcheck @ sk__75 @
% 3.02/1.31 (vsubst @ sk__76 @ sk__77 @ (vabs @ sk__78 @ sk__79 @ sk__80)) @
% 3.02/1.31 sk__81)),
% 3.02/1.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.02/1.31 thf(zip_derived_cl157, plain, (((sk__76) = (sk__78))),
% 3.02/1.31 inference('cnf', [status(esa)], [zf_stmt_0])).
% 3.02/1.31 thf(zip_derived_cl159, plain,
% 3.02/1.31 (~ (vtcheck @ sk__75 @
% 3.02/1.31 (vsubst @ sk__76 @ sk__77 @ (vabs @ sk__76 @ sk__79 @ sk__80)) @
% 3.02/1.31 sk__81)),
% 3.02/1.31 inference('demod', [status(thm)], [zip_derived_cl155, zip_derived_cl157])).
% 3.02/1.31 thf(subst3, axiom,
% 3.02/1.31 (![Ve:$i,Vx:$i,VVar0:$i,VExp0:$i,VExp1:$i,RESULT:$i,Vy:$i,VT:$i,Ve1:$i]:
% 3.02/1.31 ( ( ( ( VVar0 ) = ( Vx ) ) & ( ( VExp0 ) = ( Ve ) ) &
% 3.02/1.31 ( ( VExp1 ) = ( vabs @ Vy @ VT @ Ve1 ) ) ) =>
% 3.02/1.31 ( ( ( Vx ) = ( Vy ) ) =>
% 3.02/1.31 ( ( ( RESULT ) = ( vsubst @ VVar0 @ VExp0 @ VExp1 ) ) =>
% 3.02/1.31 ( ( RESULT ) = ( vabs @ Vy @ VT @ Ve1 ) ) ) ) ))).
% 3.02/1.31 thf(zip_derived_cl57, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i,
% 3.02/1.31 X7 : $i, X8 : $i]:
% 3.02/1.31 (((X1) != (X0))
% 3.02/1.31 | ((X5) != (vsubst @ X2 @ X3 @ X4))
% 3.02/1.31 | ((X3) != (X6))
% 3.02/1.31 | ((X2) != (X1))
% 3.02/1.31 | ((X4) != (vabs @ X0 @ X7 @ X8))
% 3.02/1.31 | ((X5) = (vabs @ X0 @ X7 @ X8)))),
% 3.02/1.31 inference('cnf', [status(esa)], [subst3])).
% 3.02/1.31 thf(zip_derived_cl293, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i, X7 : $i]:
% 3.02/1.31 (((X0) = (vabs @ X3 @ X2 @ X1))
% 3.02/1.31 | ((X4) != (vabs @ X3 @ X2 @ X1))
% 3.02/1.31 | ((X5) != (X3))
% 3.02/1.31 | ((X6) != (X7))
% 3.02/1.31 | ((X0) != (vsubst @ X5 @ X6 @ X4)))),
% 3.02/1.31 inference('eq_res', [status(thm)], [zip_derived_cl57])).
% 3.02/1.31 thf(zip_derived_cl294, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i]:
% 3.02/1.31 (((X0) != (vsubst @ X3 @ X2 @ X1))
% 3.02/1.31 | ((X2) != (X4))
% 3.02/1.31 | ((X1) != (vabs @ X3 @ X6 @ X5))
% 3.02/1.31 | ((X0) = (vabs @ X3 @ X6 @ X5)))),
% 3.02/1.31 inference('eq_res', [status(thm)], [zip_derived_cl293])).
% 3.02/1.31 thf(zip_derived_cl295, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 3.02/1.31 (((X0) = (vabs @ X3 @ X2 @ X1))
% 3.02/1.31 | ((X4) != (vabs @ X3 @ X2 @ X1))
% 3.02/1.31 | ((X0) != (vsubst @ X3 @ X5 @ X4)))),
% 3.02/1.31 inference('eq_res', [status(thm)], [zip_derived_cl294])).
% 3.02/1.31 thf(zip_derived_cl296, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 3.02/1.31 (((X0) != (vsubst @ X3 @ X4 @ (vabs @ X3 @ X2 @ X1)))
% 3.02/1.31 | ((X0) = (vabs @ X3 @ X2 @ X1)))),
% 3.02/1.31 inference('eq_res', [status(thm)], [zip_derived_cl295])).
% 3.02/1.31 thf(zip_derived_cl298, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 3.02/1.31 ((vsubst @ X2 @ X3 @ (vabs @ X2 @ X1 @ X0)) = (vabs @ X2 @ X1 @ X0))),
% 3.02/1.31 inference('eq_res', [status(thm)], [zip_derived_cl296])).
% 3.02/1.31 thf(zip_derived_cl326, plain,
% 3.02/1.31 (~ (vtcheck @ sk__75 @ (vabs @ sk__76 @ sk__79 @ sk__80) @ sk__81)),
% 3.02/1.31 inference('demod', [status(thm)], [zip_derived_cl159, zip_derived_cl298])).
% 3.02/1.31 thf(zip_derived_cl372, plain,
% 3.02/1.31 ( (visFreeVar @ sk__76 @ (vabs @ sk__76 @ sk__79 @ sk__80))),
% 3.02/1.31 inference('demod', [status(thm)], [zip_derived_cl371, zip_derived_cl326])).
% 3.02/1.31 thf(isFreeVar1, axiom,
% 3.02/1.31 (![VT:$i,VVar0:$i,VExp0:$i,Vx:$i,Vv:$i,Ve:$i]:
% 3.02/1.31 ( ( ( ( VVar0 ) = ( Vv ) ) & ( ( VExp0 ) = ( vabs @ Vx @ VT @ Ve ) ) ) =>
% 3.02/1.31 ( ( ( ( ( Vx ) != ( Vv ) ) & ( visFreeVar @ Vv @ Ve ) ) =>
% 3.02/1.31 ( visFreeVar @ VVar0 @ VExp0 ) ) &
% 3.02/1.31 ( ( visFreeVar @ VVar0 @ VExp0 ) =>
% 3.02/1.31 ( ( ( Vx ) != ( Vv ) ) & ( visFreeVar @ Vv @ Ve ) ) ) ) ))).
% 3.02/1.31 thf(zip_derived_cl17, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i]:
% 3.02/1.31 (((X1) != (X0))
% 3.02/1.31 | ((X5) != (vabs @ X2 @ X3 @ X4))
% 3.02/1.31 | ((X2) != (X0))
% 3.02/1.31 | ~ (visFreeVar @ X1 @ X5))),
% 3.02/1.31 inference('cnf', [status(esa)], [isFreeVar1])).
% 3.02/1.31 thf(zip_derived_cl192, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i]:
% 3.02/1.31 (~ (visFreeVar @ X1 @ X0)
% 3.02/1.31 | ((X2) != (X1))
% 3.02/1.31 | ((X0) != (vabs @ X2 @ X4 @ X3)))),
% 3.02/1.31 inference('eq_res', [status(thm)], [zip_derived_cl17])).
% 3.02/1.31 thf(zip_derived_cl205, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 3.02/1.31 (((X0) != (vabs @ X3 @ X2 @ X1)) | ~ (visFreeVar @ X3 @ X0))),
% 3.02/1.31 inference('eq_res', [status(thm)], [zip_derived_cl192])).
% 3.02/1.31 thf(zip_derived_cl206, plain,
% 3.02/1.31 (![X0 : $i, X1 : $i, X2 : $i]:
% 3.02/1.31 ~ (visFreeVar @ X2 @ (vabs @ X2 @ X1 @ X0))),
% 3.02/1.31 inference('eq_res', [status(thm)], [zip_derived_cl205])).
% 3.02/1.31 thf(zip_derived_cl373, plain, ($false),
% 3.02/1.31 inference('s_sup-', [status(thm)], [zip_derived_cl372, zip_derived_cl206])).
% 3.02/1.31
% 3.02/1.31 % SZS output end Refutation
% 3.02/1.31
% 3.02/1.31
% 3.02/1.31 % Terminating...
% 3.27/1.46 % Runner terminated.
% 3.27/1.48 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------