%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM023+4 : TPTP v9.2.0. Released v4.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.e3szWNHZeu true
% Computer : n014.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:37 PM UTC 2025
% Result : Theorem 0.49s 0.92s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : COM023+4 : TPTP v9.2.0. Released v4.0.0.
% 0.07/0.13 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.e3szWNHZeu true
% 0.12/0.34 % Computer : n014.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 13:47:08 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.34 % Number of cores: 8
% 0.12/0.34 % Python version: Python 3.6.8
% 0.12/0.34 % Running in FO mode
% 0.43/0.58 % Total configuration time : 435
% 0.43/0.58 % Estimated wc time : 1092
% 0.43/0.58 % Estimated cpu time (7 cpus) : 156.0
% 0.48/0.64 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.48/0.66 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.48/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.48/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.49/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.49/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.49/0.69 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.49/0.92 % Solved by fo/fo13.sh.
% 0.49/0.92 % done 252 iterations in 0.205s
% 0.49/0.92 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.49/0.92 % SZS output start Refutation
% 0.49/0.92 thf(aElement0_type, type, aElement0: $i > $o).
% 0.49/0.92 thf(zip_tseitin_4_type, type, zip_tseitin_4: $i > $i > $i > $o).
% 0.49/0.92 thf(zip_tseitin_3_type, type, zip_tseitin_3: $i > $i > $o).
% 0.49/0.92 thf(isConfluent0_type, type, isConfluent0: $i > $o).
% 0.49/0.92 thf(zip_tseitin_0_type, type, zip_tseitin_0: $i > $i > $o).
% 0.49/0.92 thf(sk__18_type, type, sk__18: $i > $i > $i).
% 0.49/0.92 thf(zip_tseitin_2_type, type, zip_tseitin_2: $i > $i > $i > $o).
% 0.49/0.92 thf(zip_tseitin_6_type, type, zip_tseitin_6: $i > $i > $i > $o).
% 0.49/0.92 thf(zip_tseitin_1_type, type, zip_tseitin_1: $i > $i > $o).
% 0.49/0.92 thf(sdtmndtasgtdt0_type, type, sdtmndtasgtdt0: $i > $i > $i > $o).
% 0.49/0.92 thf(sk__19_type, type, sk__19: $i).
% 0.49/0.92 thf(zip_tseitin_5_type, type, zip_tseitin_5: $i > $i > $o).
% 0.49/0.92 thf(sk__22_type, type, sk__22: $i).
% 0.49/0.92 thf(aReductOfIn0_type, type, aReductOfIn0: $i > $i > $i > $o).
% 0.49/0.92 thf(xR_type, type, xR: $i).
% 0.49/0.92 thf(sk__20_type, type, sk__20: $i).
% 0.49/0.92 thf(sdtmndtplgtdt0_type, type, sdtmndtplgtdt0: $i > $i > $i > $o).
% 0.49/0.92 thf(m__, conjecture,
% 0.49/0.92 (( isConfluent0 @ xR ) |
% 0.49/0.92 ( ![W0:$i,W1:$i,W2:$i]:
% 0.49/0.92 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) & ( aElement0 @ W2 ) &
% 0.49/0.92 ( ( ( W0 ) = ( W1 ) ) |
% 0.49/0.92 ( ( ( aReductOfIn0 @ W1 @ W0 @ xR ) |
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W3 @ xR @ W1 ) &
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W0 @ xR ) & ( aElement0 @ W3 ) ) ) ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W0 @ xR @ W1 ) ) ) &
% 0.49/0.92 ( sdtmndtasgtdt0 @ W0 @ xR @ W1 ) &
% 0.49/0.92 ( ( ( W0 ) = ( W2 ) ) |
% 0.49/0.92 ( ( ( aReductOfIn0 @ W2 @ W0 @ xR ) |
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W3 @ xR @ W2 ) &
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W0 @ xR ) & ( aElement0 @ W3 ) ) ) ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W0 @ xR @ W2 ) ) ) &
% 0.49/0.92 ( sdtmndtasgtdt0 @ W0 @ xR @ W2 ) ) =>
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( ( sdtmndtasgtdt0 @ W2 @ xR @ W3 ) |
% 0.49/0.92 ( sdtmndtplgtdt0 @ W2 @ xR @ W3 ) |
% 0.49/0.92 ( ?[W4:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W4 @ xR @ W3 ) &
% 0.49/0.92 ( aReductOfIn0 @ W4 @ W2 @ xR ) & ( aElement0 @ W4 ) ) ) |
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W2 @ xR ) | ( ( W2 ) = ( W3 ) ) ) &
% 0.49/0.92 ( ( sdtmndtasgtdt0 @ W1 @ xR @ W3 ) |
% 0.49/0.92 ( sdtmndtplgtdt0 @ W1 @ xR @ W3 ) |
% 0.49/0.92 ( ?[W4:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W4 @ xR @ W3 ) &
% 0.49/0.92 ( aReductOfIn0 @ W4 @ W1 @ xR ) & ( aElement0 @ W4 ) ) ) |
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W1 @ xR ) | ( ( W1 ) = ( W3 ) ) ) &
% 0.49/0.92 ( aElement0 @ W3 ) ) ) ) ))).
% 0.49/0.92 thf(zf_stmt_0, negated_conjecture,
% 0.49/0.92 (~( ( isConfluent0 @ xR ) |
% 0.49/0.92 ( ![W0:$i,W1:$i,W2:$i]:
% 0.49/0.92 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) & ( aElement0 @ W2 ) &
% 0.49/0.92 ( ( ( W0 ) = ( W1 ) ) |
% 0.49/0.92 ( ( ( aReductOfIn0 @ W1 @ W0 @ xR ) |
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W3 @ xR @ W1 ) &
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W0 @ xR ) & ( aElement0 @ W3 ) ) ) ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W0 @ xR @ W1 ) ) ) &
% 0.49/0.92 ( sdtmndtasgtdt0 @ W0 @ xR @ W1 ) &
% 0.49/0.92 ( ( ( W0 ) = ( W2 ) ) |
% 0.49/0.92 ( ( ( aReductOfIn0 @ W2 @ W0 @ xR ) |
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W3 @ xR @ W2 ) &
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W0 @ xR ) & ( aElement0 @ W3 ) ) ) ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W0 @ xR @ W2 ) ) ) &
% 0.49/0.92 ( sdtmndtasgtdt0 @ W0 @ xR @ W2 ) ) =>
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( ( sdtmndtasgtdt0 @ W2 @ xR @ W3 ) |
% 0.49/0.92 ( sdtmndtplgtdt0 @ W2 @ xR @ W3 ) |
% 0.49/0.92 ( ?[W4:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W4 @ xR @ W3 ) &
% 0.49/0.92 ( aReductOfIn0 @ W4 @ W2 @ xR ) & ( aElement0 @ W4 ) ) ) |
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W2 @ xR ) | ( ( W2 ) = ( W3 ) ) ) &
% 0.49/0.92 ( ( sdtmndtasgtdt0 @ W1 @ xR @ W3 ) |
% 0.49/0.92 ( sdtmndtplgtdt0 @ W1 @ xR @ W3 ) |
% 0.49/0.92 ( ?[W4:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W4 @ xR @ W3 ) &
% 0.49/0.92 ( aReductOfIn0 @ W4 @ W1 @ xR ) & ( aElement0 @ W4 ) ) ) |
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W1 @ xR ) | ( ( W1 ) = ( W3 ) ) ) &
% 0.49/0.92 ( aElement0 @ W3 ) ) ) ) ) )),
% 0.49/0.92 inference('cnf.neg', [status(esa)], [m__])).
% 0.49/0.92 thf(zip_derived_cl98, plain, ( (sdtmndtasgtdt0 @ sk__19 @ xR @ sk__22)),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.49/0.92 thf(m__715, axiom,
% 0.49/0.92 (![W0:$i,W1:$i,W2:$i]:
% 0.49/0.92 ( ( ( ( sdtmndtasgtdt0 @ W0 @ xR @ W2 ) |
% 0.49/0.92 ( sdtmndtplgtdt0 @ W0 @ xR @ W2 ) |
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( aElement0 @ W3 ) & ( aReductOfIn0 @ W3 @ W0 @ xR ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W3 @ xR @ W2 ) ) ) |
% 0.49/0.92 ( aReductOfIn0 @ W2 @ W0 @ xR ) | ( ( W0 ) = ( W2 ) ) ) &
% 0.49/0.92 ( ( sdtmndtasgtdt0 @ W0 @ xR @ W1 ) |
% 0.49/0.92 ( sdtmndtplgtdt0 @ W0 @ xR @ W1 ) |
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( aElement0 @ W3 ) & ( aReductOfIn0 @ W3 @ W0 @ xR ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W3 @ xR @ W1 ) ) ) |
% 0.49/0.92 ( aReductOfIn0 @ W1 @ W0 @ xR ) | ( ( W0 ) = ( W1 ) ) ) &
% 0.49/0.92 ( aElement0 @ W2 ) & ( aElement0 @ W1 ) & ( aElement0 @ W0 ) ) =>
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( aElement0 @ W3 ) &
% 0.49/0.92 ( ( ( W1 ) = ( W3 ) ) |
% 0.49/0.92 ( ( ( aReductOfIn0 @ W3 @ W1 @ xR ) |
% 0.49/0.92 ( ?[W4:$i]:
% 0.49/0.92 ( ( aElement0 @ W4 ) & ( aReductOfIn0 @ W4 @ W1 @ xR ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W4 @ xR @ W3 ) ) ) ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W1 @ xR @ W3 ) ) ) &
% 0.49/0.92 ( sdtmndtasgtdt0 @ W1 @ xR @ W3 ) &
% 0.49/0.92 ( ( ( W2 ) = ( W3 ) ) |
% 0.49/0.92 ( ( ( aReductOfIn0 @ W3 @ W2 @ xR ) |
% 0.49/0.92 ( ?[W4:$i]:
% 0.49/0.92 ( ( aElement0 @ W4 ) & ( aReductOfIn0 @ W4 @ W2 @ xR ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W4 @ xR @ W3 ) ) ) ) &
% 0.49/0.92 ( sdtmndtplgtdt0 @ W2 @ xR @ W3 ) ) ) &
% 0.49/0.92 ( sdtmndtasgtdt0 @ W2 @ xR @ W3 ) ) ) ))).
% 0.49/0.92 thf(zf_stmt_1, axiom,
% 0.49/0.92 (![W2:$i,W0:$i]:
% 0.49/0.92 ( ( ( ( W0 ) = ( W2 ) ) | ( aReductOfIn0 @ W2 @ W0 @ xR ) |
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W3 @ xR @ W2 ) &
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W0 @ xR ) & ( aElement0 @ W3 ) ) ) |
% 0.49/0.92 ( sdtmndtplgtdt0 @ W0 @ xR @ W2 ) | ( sdtmndtasgtdt0 @ W0 @ xR @ W2 ) ) =>
% 0.49/0.92 ( zip_tseitin_0 @ W2 @ W0 ) ))).
% 0.49/0.92 thf(zip_derived_cl64, plain,
% 0.49/0.92 (![X0 : $i, X1 : $i]:
% 0.49/0.92 ( (zip_tseitin_0 @ X0 @ X1) | ~ (sdtmndtasgtdt0 @ X1 @ xR @ X0))),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.49/0.92 thf(zip_derived_cl192, plain, ( (zip_tseitin_0 @ sk__22 @ sk__19)),
% 0.49/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl98, zip_derived_cl64])).
% 0.49/0.92 thf(zip_derived_cl86, plain, ( (sdtmndtasgtdt0 @ sk__19 @ xR @ sk__20)),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.49/0.92 thf(zf_stmt_2, axiom,
% 0.49/0.92 (![W1:$i,W0:$i]:
% 0.49/0.92 ( ( ( ( W0 ) = ( W1 ) ) | ( aReductOfIn0 @ W1 @ W0 @ xR ) |
% 0.49/0.92 ( ?[W3:$i]:
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W3 @ xR @ W1 ) &
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W0 @ xR ) & ( aElement0 @ W3 ) ) ) |
% 0.49/0.92 ( sdtmndtplgtdt0 @ W0 @ xR @ W1 ) | ( sdtmndtasgtdt0 @ W0 @ xR @ W1 ) ) =>
% 0.49/0.92 ( zip_tseitin_1 @ W1 @ W0 ) ))).
% 0.49/0.92 thf(zip_derived_cl69, plain,
% 0.49/0.92 (![X0 : $i, X1 : $i]:
% 0.49/0.92 ( (zip_tseitin_1 @ X0 @ X1) | ~ (sdtmndtasgtdt0 @ X1 @ xR @ X0))),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.49/0.92 thf(zip_derived_cl204, plain, ( (zip_tseitin_1 @ sk__20 @ sk__19)),
% 0.49/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl86, zip_derived_cl69])).
% 0.49/0.92 thf(zf_stmt_3, type, zip_tseitin_6 : $i > $i > $i > $o).
% 0.49/0.92 thf(zf_stmt_4, axiom,
% 0.49/0.92 (![W3:$i,W2:$i,W1:$i]:
% 0.49/0.92 ( ( zip_tseitin_6 @ W3 @ W2 @ W1 ) =>
% 0.49/0.92 ( ( sdtmndtasgtdt0 @ W2 @ xR @ W3 ) &
% 0.49/0.92 ( ( zip_tseitin_5 @ W3 @ W2 ) | ( ( W2 ) = ( W3 ) ) ) &
% 0.49/0.92 ( sdtmndtasgtdt0 @ W1 @ xR @ W3 ) &
% 0.49/0.92 ( ( zip_tseitin_3 @ W3 @ W1 ) | ( ( W1 ) = ( W3 ) ) ) &
% 0.49/0.92 ( aElement0 @ W3 ) ) ))).
% 0.49/0.92 thf(zf_stmt_5, type, zip_tseitin_5 : $i > $i > $o).
% 0.49/0.92 thf(zf_stmt_6, axiom,
% 0.49/0.92 (![W3:$i,W2:$i]:
% 0.49/0.92 ( ( zip_tseitin_5 @ W3 @ W2 ) =>
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W2 @ xR @ W3 ) &
% 0.49/0.92 ( ( ?[W4:$i]: ( zip_tseitin_4 @ W4 @ W3 @ W2 ) ) |
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W2 @ xR ) ) ) ))).
% 0.49/0.92 thf(zf_stmt_7, type, zip_tseitin_4 : $i > $i > $i > $o).
% 0.49/0.92 thf(zf_stmt_8, axiom,
% 0.49/0.92 (![W4:$i,W3:$i,W2:$i]:
% 0.49/0.92 ( ( zip_tseitin_4 @ W4 @ W3 @ W2 ) =>
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W4 @ xR @ W3 ) & ( aReductOfIn0 @ W4 @ W2 @ xR ) &
% 0.49/0.92 ( aElement0 @ W4 ) ) ))).
% 0.49/0.92 thf(zf_stmt_9, type, zip_tseitin_3 : $i > $i > $o).
% 0.49/0.92 thf(zf_stmt_10, axiom,
% 0.49/0.92 (![W3:$i,W1:$i]:
% 0.49/0.92 ( ( zip_tseitin_3 @ W3 @ W1 ) =>
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W1 @ xR @ W3 ) &
% 0.49/0.92 ( ( ?[W4:$i]: ( zip_tseitin_2 @ W4 @ W3 @ W1 ) ) |
% 0.49/0.92 ( aReductOfIn0 @ W3 @ W1 @ xR ) ) ) ))).
% 0.49/0.92 thf(zf_stmt_11, type, zip_tseitin_2 : $i > $i > $i > $o).
% 0.49/0.92 thf(zf_stmt_12, axiom,
% 0.49/0.92 (![W4:$i,W3:$i,W1:$i]:
% 0.49/0.92 ( ( zip_tseitin_2 @ W4 @ W3 @ W1 ) =>
% 0.49/0.92 ( ( sdtmndtplgtdt0 @ W4 @ xR @ W3 ) & ( aReductOfIn0 @ W4 @ W1 @ xR ) &
% 0.49/0.92 ( aElement0 @ W4 ) ) ))).
% 0.49/0.92 thf(zf_stmt_13, type, zip_tseitin_1 : $i > $i > $o).
% 0.49/0.92 thf(zf_stmt_14, type, zip_tseitin_0 : $i > $i > $o).
% 0.49/0.92 thf(zf_stmt_15, axiom,
% 0.49/0.92 (![W0:$i,W1:$i,W2:$i]:
% 0.49/0.92 ( ( ( aElement0 @ W0 ) & ( aElement0 @ W1 ) & ( aElement0 @ W2 ) &
% 0.49/0.92 ( zip_tseitin_1 @ W1 @ W0 ) & ( zip_tseitin_0 @ W2 @ W0 ) ) =>
% 0.49/0.92 ( ?[W3:$i]: ( zip_tseitin_6 @ W3 @ W2 @ W1 ) ) ))).
% 0.49/0.92 thf(zip_derived_cl85, plain,
% 0.49/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.49/0.92 (~ (zip_tseitin_1 @ X0 @ X1)
% 0.49/0.92 | ~ (aElement0 @ X0)
% 0.49/0.92 | ~ (aElement0 @ X1)
% 0.49/0.92 | ~ (aElement0 @ X2)
% 0.49/0.92 | ~ (zip_tseitin_0 @ X2 @ X1)
% 0.49/0.92 | (zip_tseitin_6 @ (sk__18 @ X2 @ X0) @ X2 @ X0))),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_15])).
% 0.49/0.92 thf(zip_derived_cl768, plain,
% 0.49/0.92 (![X0 : $i]:
% 0.49/0.92 (~ (aElement0 @ sk__20)
% 0.49/0.92 | ~ (aElement0 @ sk__19)
% 0.49/0.92 | ~ (aElement0 @ X0)
% 0.49/0.92 | ~ (zip_tseitin_0 @ X0 @ sk__19)
% 0.49/0.92 | (zip_tseitin_6 @ (sk__18 @ X0 @ sk__20) @ X0 @ sk__20))),
% 0.49/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl204, zip_derived_cl85])).
% 0.49/0.92 thf(zip_derived_cl91, plain, ( (aElement0 @ sk__20)),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.49/0.92 thf(zip_derived_cl92, plain, ( (aElement0 @ sk__19)),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.49/0.92 thf(zip_derived_cl777, plain,
% 0.49/0.92 (![X0 : $i]:
% 0.49/0.92 (~ (aElement0 @ X0)
% 0.49/0.92 | ~ (zip_tseitin_0 @ X0 @ sk__19)
% 0.49/0.92 | (zip_tseitin_6 @ (sk__18 @ X0 @ sk__20) @ X0 @ sk__20))),
% 0.49/0.92 inference('demod', [status(thm)],
% 0.49/0.92 [zip_derived_cl768, zip_derived_cl91, zip_derived_cl92])).
% 0.49/0.92 thf(zip_derived_cl786, plain,
% 0.49/0.92 ((~ (aElement0 @ sk__22)
% 0.49/0.92 | (zip_tseitin_6 @ (sk__18 @ sk__22 @ sk__20) @ sk__22 @ sk__20))),
% 0.49/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl192, zip_derived_cl777])).
% 0.49/0.92 thf(zip_derived_cl93, plain, ( (aElement0 @ sk__22)),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.49/0.92 thf(zip_derived_cl790, plain,
% 0.49/0.92 ( (zip_tseitin_6 @ (sk__18 @ sk__22 @ sk__20) @ sk__22 @ sk__20)),
% 0.49/0.92 inference('demod', [status(thm)], [zip_derived_cl786, zip_derived_cl93])).
% 0.49/0.92 thf(zip_derived_cl80, plain,
% 0.49/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.49/0.92 ( (sdtmndtasgtdt0 @ X0 @ xR @ X1) | ~ (zip_tseitin_6 @ X1 @ X0 @ X2))),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.49/0.92 thf(zip_derived_cl913, plain,
% 0.49/0.92 ( (sdtmndtasgtdt0 @ sk__22 @ xR @ (sk__18 @ sk__22 @ sk__20))),
% 0.49/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl790, zip_derived_cl80])).
% 0.49/0.92 thf(zip_derived_cl103, plain,
% 0.49/0.92 (![X0 : $i]:
% 0.49/0.92 (~ (sdtmndtasgtdt0 @ sk__22 @ xR @ X0)
% 0.49/0.92 | ~ (sdtmndtasgtdt0 @ sk__20 @ xR @ X0)
% 0.49/0.92 | ~ (aElement0 @ X0))),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.49/0.92 thf(zip_derived_cl929, plain,
% 0.49/0.92 ((~ (sdtmndtasgtdt0 @ sk__20 @ xR @ (sk__18 @ sk__22 @ sk__20))
% 0.49/0.92 | ~ (aElement0 @ (sk__18 @ sk__22 @ sk__20)))),
% 0.49/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl913, zip_derived_cl103])).
% 0.49/0.92 thf(zip_derived_cl790, plain,
% 0.49/0.92 ( (zip_tseitin_6 @ (sk__18 @ sk__22 @ sk__20) @ sk__22 @ sk__20)),
% 0.49/0.92 inference('demod', [status(thm)], [zip_derived_cl786, zip_derived_cl93])).
% 0.49/0.92 thf(zip_derived_cl84, plain,
% 0.49/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.49/0.92 ( (aElement0 @ X0) | ~ (zip_tseitin_6 @ X0 @ X1 @ X2))),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.49/0.92 thf(zip_derived_cl915, plain, ( (aElement0 @ (sk__18 @ sk__22 @ sk__20))),
% 0.49/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl790, zip_derived_cl84])).
% 0.49/0.92 thf(zip_derived_cl940, plain,
% 0.49/0.92 (~ (sdtmndtasgtdt0 @ sk__20 @ xR @ (sk__18 @ sk__22 @ sk__20))),
% 0.49/0.92 inference('demod', [status(thm)], [zip_derived_cl929, zip_derived_cl915])).
% 0.49/0.92 thf(zip_derived_cl790, plain,
% 0.49/0.92 ( (zip_tseitin_6 @ (sk__18 @ sk__22 @ sk__20) @ sk__22 @ sk__20)),
% 0.49/0.92 inference('demod', [status(thm)], [zip_derived_cl786, zip_derived_cl93])).
% 0.49/0.92 thf(zip_derived_cl82, plain,
% 0.49/0.92 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.49/0.92 ( (sdtmndtasgtdt0 @ X0 @ xR @ X1) | ~ (zip_tseitin_6 @ X1 @ X2 @ X0))),
% 0.49/0.92 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.49/0.92 thf(zip_derived_cl916, plain,
% 0.49/0.92 ( (sdtmndtasgtdt0 @ sk__20 @ xR @ (sk__18 @ sk__22 @ sk__20))),
% 0.49/0.92 inference('s_sup-', [status(thm)], [zip_derived_cl790, zip_derived_cl82])).
% 0.49/0.92 thf(zip_derived_cl958, plain, ($false),
% 0.49/0.92 inference('demod', [status(thm)], [zip_derived_cl940, zip_derived_cl916])).
% 0.49/0.92
% 0.49/0.92 % SZS output end Refutation
% 0.49/0.92
% 0.49/0.92
% 0.49/0.92 % Terminating...
% 0.51/0.99 % Runner terminated.
% 1.66/1.00 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------