%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : GEO462+1 : TPTP v9.2.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.0df1zER4vd true
% Computer : n018.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:34:47 PM UTC 2025
% Result : Theorem 113.60s 16.82s
% Output : Refutation 113.60s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO462+1 : TPTP v9.2.0. Released v7.0.0.
% 0.03/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.0df1zER4vd true
% 0.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 1 17:31:38 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.34 % Running portfolio for 300 s
% 0.12/0.34 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.35 % Number of cores: 8
% 0.12/0.35 % Python version: Python 3.6.8
% 0.20/0.35 % Running in FO mode
% 0.52/0.64 % Total configuration time : 435
% 0.52/0.64 % Estimated wc time : 1092
% 0.52/0.64 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/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.73 % /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.76 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 113.60/16.82 % Solved by fo/fo4.sh.
% 113.60/16.82 % done 5044 iterations in 16.027s
% 113.60/16.82 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 113.60/16.82 % SZS output start Refutation
% 113.60/16.82 thf(in_type, type, in: $i).
% 113.60/16.82 thf(numeral_type, type, numeral: $i).
% 113.60/16.82 thf(empty_type, type, empty: $i).
% 113.60/16.82 thf(fun_type, type, fun: $i > $i > $i).
% 113.60/16.82 thf(zip_tseitin_33_type, type, zip_tseitin_33: $i > $i > $i > $i > $o).
% 113.60/16.82 thf(u_0_type, type, u_0: $i).
% 113.60/16.82 thf(num_type, type, num: $i).
% 113.60/16.82 thf(sk__195_type, type, sk__195: $i).
% 113.60/16.82 thf(bool_type, type, bool: $i).
% 113.60/16.82 thf(zip_tseitin_34_type, type, zip_tseitin_34: $i > $i > $i > $i > $o).
% 113.60/16.82 thf(s_type, type, s: $i > $i > $i).
% 113.60/16.82 thf(p_type, type, p: $i > $o).
% 113.60/16.82 thf(r__type, type, r_: $i).
% 113.60/16.82 thf(vec_type, type, vec: $i).
% 113.60/16.82 thf(vectoru_add_type, type, vectoru_add: $i).
% 113.60/16.82 thf(i_type, type, i: $i > $i > $i).
% 113.60/16.82 thf(real_type, type, real: $i).
% 113.60/16.82 thf(subspace_type, type, subspace: $i).
% 113.60/16.82 thf(cart_type, type, cart: $i > $i > $i).
% 113.60/16.82 thf(sk__194_type, type, sk__194: $i).
% 113.60/16.82 thf(aSUBSPACEu_IMPu_NONEMPTY, conjecture,
% 113.60/16.82 (![Q121443:$i,S0:$i]:
% 113.60/16.82 ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121443 ) @ bool ) @ bool ) @
% 113.60/16.82 subspace ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121443 ) @ bool ) @ S0 ) ) ) ) =>
% 113.60/16.82 ( ( s @ ( fun @ ( cart @ real @ Q121443 ) @ bool ) @ S0 ) !=
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121443 ) @ bool ) @ empty ) ) ))).
% 113.60/16.82 thf(zf_stmt_0, negated_conjecture,
% 113.60/16.82 (~( ![Q121443:$i,S0:$i]:
% 113.60/16.82 ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121443 ) @ bool ) @ bool ) @
% 113.60/16.82 subspace ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121443 ) @ bool ) @ S0 ) ) ) ) =>
% 113.60/16.82 ( ( s @ ( fun @ ( cart @ real @ Q121443 ) @ bool ) @ S0 ) !=
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121443 ) @ bool ) @ empty ) ) ) )),
% 113.60/16.82 inference('cnf.neg', [status(esa)], [aSUBSPACEu_IMPu_NONEMPTY])).
% 113.60/16.82 thf(zip_derived_cl402, plain,
% 113.60/16.82 (((s @ (fun @ (cart @ real @ sk__194) @ bool) @ sk__195)
% 113.60/16.82 = (s @ (fun @ (cart @ real @ sk__194) @ bool) @ empty))),
% 113.60/16.82 inference('cnf', [status(esa)], [zf_stmt_0])).
% 113.60/16.82 thf(asubspace, axiom,
% 113.60/16.82 (![Q121390:$i,S0:$i]:
% 113.60/16.82 ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 subspace ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) <=>
% 113.60/16.82 ( ( ![C0:$i,X:$i]:
% 113.60/16.82 ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ X ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) =>
% 113.60/16.82 ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( cart @ real @ Q121390 ) ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 real @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( cart @ real @ Q121390 ) ) ) @
% 113.60/16.82 r_ ) @
% 113.60/16.82 ( s @ real @ C0 ) ) ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ X ) ) ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) ) ) &
% 113.60/16.82 ( ![X:$i,Y:$i]:
% 113.60/16.82 ( ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @
% 113.60/16.82 bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ Y ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) &
% 113.60/16.82 ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @
% 113.60/16.82 bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ X ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) ) =>
% 113.60/16.82 ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( cart @ real @ Q121390 ) ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( cart @ real @ Q121390 ) ) ) @
% 113.60/16.82 vectoru_add ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ X ) ) ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ Y ) ) ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) ) ) &
% 113.60/16.82 ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @ ( fun @ num @ ( cart @ real @ Q121390 ) ) @ vec ) @
% 113.60/16.82 ( s @
% 113.60/16.82 num @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @ ( fun @ num @ num ) @ numeral ) @
% 113.60/16.82 ( s @ num @ u_0 ) ) ) ) ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) ) ))).
% 113.60/16.82 thf(zf_stmt_1, type, zip_tseitin_34 : $i > $i > $i > $i > $o).
% 113.60/16.82 thf(zf_stmt_2, axiom,
% 113.60/16.82 (![Y:$i,X:$i,S0:$i,Q121390:$i]:
% 113.60/16.82 ( ( zip_tseitin_34 @ Y @ X @ S0 @ Q121390 ) <=>
% 113.60/16.82 ( ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ X ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) &
% 113.60/16.82 ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ Y ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) ) =>
% 113.60/16.82 ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( cart @ real @ Q121390 ) ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( cart @ real @ Q121390 ) ) ) @
% 113.60/16.82 vectoru_add ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ X ) ) ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ Y ) ) ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) ) ))).
% 113.60/16.82 thf(zf_stmt_3, type, zip_tseitin_33 : $i > $i > $i > $i > $o).
% 113.60/16.82 thf(zf_stmt_4, axiom,
% 113.60/16.82 (![X:$i,C0:$i,S0:$i,Q121390:$i]:
% 113.60/16.82 ( ( zip_tseitin_33 @ X @ C0 @ S0 @ Q121390 ) <=>
% 113.60/16.82 ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ X ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) =>
% 113.60/16.82 ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( cart @ real @ Q121390 ) ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 real @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( cart @ real @ Q121390 ) ) ) @
% 113.60/16.82 r_ ) @
% 113.60/16.82 ( s @ real @ C0 ) ) ) @
% 113.60/16.82 ( s @ ( cart @ real @ Q121390 ) @ X ) ) ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) ) ))).
% 113.60/16.82 thf(zf_stmt_5, axiom,
% 113.60/16.82 (![Q121390:$i,S0:$i]:
% 113.60/16.82 ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 subspace ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) <=>
% 113.60/16.82 ( ( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( fun @
% 113.60/16.82 ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ bool ) ) @
% 113.60/16.82 in ) @
% 113.60/16.82 ( s @
% 113.60/16.82 ( cart @ real @ Q121390 ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @ ( fun @ num @ ( cart @ real @ Q121390 ) ) @ vec ) @
% 113.60/16.82 ( s @
% 113.60/16.82 num @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @ ( fun @ num @ num ) @ numeral ) @
% 113.60/16.82 ( s @ num @ u_0 ) ) ) ) ) ) ) @
% 113.60/16.82 ( s @ ( fun @ ( cart @ real @ Q121390 ) @ bool ) @ S0 ) ) ) ) &
% 113.60/16.82 ( ![X:$i,Y:$i]: ( zip_tseitin_34 @ Y @ X @ S0 @ Q121390 ) ) &
% 113.60/16.82 ( ![C0:$i,X:$i]: ( zip_tseitin_33 @ X @ C0 @ S0 @ Q121390 ) ) ) ))).
% 113.60/16.82 thf(zip_derived_cl395, plain,
% 113.60/16.82 (![X0 : $i, X1 : $i]:
% 113.60/16.82 ( (p @
% 113.60/16.82 (s @ bool @
% 113.60/16.82 (i @
% 113.60/16.82 (s @ (fun @ (fun @ (cart @ real @ X0) @ bool) @ bool) @
% 113.60/16.82 (i @
% 113.60/16.82 (s @
% 113.60/16.82 (fun @ (cart @ real @ X0) @
% 113.60/16.82 (fun @ (fun @ (cart @ real @ X0) @ bool) @ bool)) @
% 113.60/16.82 in) @
% 113.60/16.82 (s @ (cart @ real @ X0) @
% 113.60/16.82 (i @ (s @ (fun @ num @ (cart @ real @ X0)) @ vec) @
% 113.60/16.82 (s @ num @
% 113.60/16.82 (i @ (s @ (fun @ num @ num) @ numeral) @ (s @ num @ u_0))))))) @
% 113.60/16.82 (s @ (fun @ (cart @ real @ X0) @ bool) @ X1))))
% 113.60/16.82 | ~ (p @
% 113.60/16.82 (s @ bool @
% 113.60/16.82 (i @
% 113.60/16.82 (s @ (fun @ (fun @ (cart @ real @ X0) @ bool) @ bool) @
% 113.60/16.82 subspace) @
% 113.60/16.82 (s @ (fun @ (cart @ real @ X0) @ bool) @ X1)))))),
% 113.60/16.82 inference('cnf', [status(esa)], [zf_stmt_5])).
% 113.60/16.82 thf(aNOTu_INu_EMPTY, axiom,
% 113.60/16.82 (![A:$i,X:$i]:
% 113.60/16.82 ( ~( p @
% 113.60/16.82 ( s @
% 113.60/16.82 bool @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @
% 113.60/16.82 ( fun @ ( fun @ A @ bool ) @ bool ) @
% 113.60/16.82 ( i @
% 113.60/16.82 ( s @ ( fun @ A @ ( fun @ ( fun @ A @ bool ) @ bool ) ) @ in ) @
% 113.60/16.82 ( s @ A @ X ) ) ) @
% 113.60/16.82 ( s @ ( fun @ A @ bool ) @ empty ) ) ) ) ))).
% 113.60/16.82 thf(zip_derived_cl316, plain,
% 113.60/16.82 (![X0 : $i, X1 : $i]:
% 113.60/16.82 ~ (p @
% 113.60/16.82 (s @ bool @
% 113.60/16.82 (i @
% 113.60/16.82 (s @ (fun @ (fun @ X0 @ bool) @ bool) @
% 113.60/16.82 (i @ (s @ (fun @ X0 @ (fun @ (fun @ X0 @ bool) @ bool)) @ in) @
% 113.60/16.82 (s @ X0 @ X1))) @
% 113.60/16.82 (s @ (fun @ X0 @ bool) @ empty))))),
% 113.60/16.82 inference('cnf', [status(esa)], [aNOTu_INu_EMPTY])).
% 113.60/16.82 thf(zip_derived_cl53400, plain,
% 113.60/16.82 (![X0 : $i]:
% 113.60/16.82 ~ (p @
% 113.60/16.82 (s @ bool @
% 113.60/16.82 (i @
% 113.60/16.82 (s @ (fun @ (fun @ (cart @ real @ X0) @ bool) @ bool) @ subspace) @
% 113.60/16.82 (s @ (fun @ (cart @ real @ X0) @ bool) @ empty))))),
% 113.60/16.82 inference('sup-', [status(thm)], [zip_derived_cl395, zip_derived_cl316])).
% 113.60/16.82 thf(zip_derived_cl53576, plain,
% 113.60/16.82 (~ (p @
% 113.60/16.82 (s @ bool @
% 113.60/16.82 (i @
% 113.60/16.82 (s @ (fun @ (fun @ (cart @ real @ sk__194) @ bool) @ bool) @
% 113.60/16.82 subspace) @
% 113.60/16.82 (s @ (fun @ (cart @ real @ sk__194) @ bool) @ sk__195))))),
% 113.60/16.82 inference('sup-', [status(thm)], [zip_derived_cl402, zip_derived_cl53400])).
% 113.60/16.82 thf(zip_derived_cl401, plain,
% 113.60/16.82 ( (p @
% 113.60/16.82 (s @ bool @
% 113.60/16.82 (i @
% 113.60/16.82 (s @ (fun @ (fun @ (cart @ real @ sk__194) @ bool) @ bool) @
% 113.60/16.82 subspace) @
% 113.60/16.82 (s @ (fun @ (cart @ real @ sk__194) @ bool) @ sk__195))))),
% 113.60/16.82 inference('cnf', [status(esa)], [zf_stmt_0])).
% 113.60/16.82 thf(zip_derived_cl53577, plain, ($false),
% 113.60/16.82 inference('demod', [status(thm)],
% 113.60/16.82 [zip_derived_cl53576, zip_derived_cl401])).
% 113.60/16.82
% 113.60/16.82 % SZS output end Refutation
% 113.60/16.82
% 113.60/16.82
% 113.60/16.82 % Terminating...
% 113.97/16.89 % Runner terminated.
% 113.97/16.90 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------