%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : COM003_1 : TPTP v9.2.0. Released v5.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.AKXHS4Ka8T 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:32 PM UTC 2025
% Result : Theorem 0.49s 1.01s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.10 % Problem : COM003_1 : TPTP v9.2.0. Released v5.0.0.
% 0.02/0.11 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.AKXHS4Ka8T true
% 0.10/0.32 % Computer : n007.cluster.edu
% 0.10/0.32 % Model : x86_64 x86_64
% 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.32 % Memory : 8042.1875MB
% 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.32 % CPULimit : 300
% 0.10/0.32 % WCLimit : 300
% 0.10/0.32 % DateTime : Wed Oct 1 13:50:53 EDT 2025
% 0.10/0.32 % CPUTime :
% 0.10/0.32 % Running portfolio for 300 s
% 0.10/0.32 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.32 % Number of cores: 8
% 0.10/0.32 % Python version: Python 3.6.8
% 0.10/0.32 % Running in FO mode
% 0.47/0.62 % Total configuration time : 435
% 0.47/0.62 % Estimated wc time : 1092
% 0.47/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.48/0.84 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.48/0.86 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.48/0.87 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.48/0.87 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.48/0.87 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.49/0.87 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 0.49/0.88 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.49/1.01 % Solved by fo/fo6_bce.sh.
% 0.49/1.01 % BCE start: 26
% 0.49/1.01 % BCE eliminated: 0
% 0.49/1.01 % PE start: 26
% 0.49/1.01 logic: neq
% 0.49/1.01 % PE eliminated: 7
% 0.49/1.01 % done 69 iterations in 0.082s
% 0.49/1.01 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 0.49/1.01 % SZS output start Refutation
% 0.49/1.01 thf(algorithm_type, type, algorithm: $tType).
% 0.49/1.01 thf(program_type, type, program: $tType).
% 0.49/1.01 thf(input_type, type, input: $tType).
% 0.49/1.01 thf(output_type, type, output: $tType).
% 0.49/1.01 thf(bad_type, type, bad: output).
% 0.49/1.01 thf(sk__2_type, type, sk__2: algorithm > input).
% 0.49/1.01 thf(sk__7_type, type, sk__7: algorithm).
% 0.49/1.01 thf(as_input_type, type, as_input: program > input).
% 0.49/1.01 thf(halts3_type, type, halts3: program > program > input > $o).
% 0.49/1.01 thf(zip_tseitin_7_type, type, zip_tseitin_7: program > program > $o).
% 0.49/1.01 thf(sk__1_type, type, sk__1: algorithm > program).
% 0.49/1.01 thf(decides_type, type, decides: algorithm > program > input > $o).
% 0.49/1.01 thf(outputs_type, type, outputs: program > output > $o).
% 0.49/1.01 thf(halts2_type, type, halts2: program > input > $o).
% 0.49/1.01 thf(zip_tseitin_2_type, type, zip_tseitin_2: program > program > $o).
% 0.49/1.01 thf(sk__4_type, type, sk__4: program > program).
% 0.49/1.01 thf(sk__3_type, type, sk__3: program).
% 0.49/1.01 thf(sk__5_type, type, sk__5: program).
% 0.49/1.01 thf(good_type, type, good: output).
% 0.49/1.01 thf(zip_tseitin_6_type, type, zip_tseitin_6: program > program > $o).
% 0.49/1.01 thf(sk__type, type, sk_: program).
% 0.49/1.01 thf(algorithm_of_type, type, algorithm_of: program > algorithm).
% 0.49/1.01 thf(sk__6_type, type, sk__6: program > program).
% 0.49/1.01 thf(zip_tseitin_3_type, type, zip_tseitin_3: program > program > $o).
% 0.49/1.01 thf(zip_tseitin_4_type, type, zip_tseitin_4: program > program > $o).
% 0.49/1.01 thf(zip_tseitin_0_type, type, zip_tseitin_0: program > program > $o).
% 0.49/1.01 thf(zip_tseitin_8_type, type, zip_tseitin_8: program > program > $o).
% 0.49/1.01 thf(zip_tseitin_1_type, type, zip_tseitin_1: program > program > $o).
% 0.49/1.01 thf(zip_tseitin_5_type, type, zip_tseitin_5: program > program > $o).
% 0.49/1.01 thf(prove_this, conjecture,
% 0.49/1.01 (~( ?[X1:algorithm]: ( ![Y1:program,Z1:input]: ( decides @ X1 @ Y1 @ Z1 ) ) ))).
% 0.49/1.01 thf(zf_stmt_0, negated_conjecture,
% 0.49/1.01 (?[X1:algorithm]: ( ![Y1:program,Z1:input]: ( decides @ X1 @ Y1 @ Z1 ) )),
% 0.49/1.01 inference('cnf.neg', [status(esa)], [prove_this])).
% 0.49/1.01 thf(zip_derived_cl25, plain,
% 0.49/1.01 (![X0 : program, X1 : input]: (decides @ sk__7 @ X0 @ X1)),
% 0.49/1.01 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.49/1.01 thf(p1, axiom,
% 0.49/1.01 (( ?[X:algorithm]: ( ![Y:program,Z:input]: ( decides @ X @ Y @ Z ) ) ) =>
% 0.49/1.01 ( ?[W:program]:
% 0.49/1.01 ( ![Y:program,Z:input]: ( decides @ ( algorithm_of @ W ) @ Y @ Z ) ) ))).
% 0.49/1.01 thf(zip_derived_cl0, plain,
% 0.49/1.01 (![X0 : program, X1 : input, X2 : algorithm]:
% 0.49/1.01 ( (decides @ (algorithm_of @ sk_) @ X0 @ X1)
% 0.49/1.01 | ~ (decides @ X2 @ (sk__1 @ X2) @ (sk__2 @ X2)))),
% 0.49/1.01 inference('cnf', [status(esa)], [p1])).
% 0.49/1.01 thf(zip_derived_cl65, plain,
% 0.49/1.01 (![X0 : input, X1 : program]: (decides @ (algorithm_of @ sk_) @ X1 @ X0)),
% 0.49/1.01 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl0])).
% 0.49/1.01 thf(p2, axiom,
% 0.49/1.01 (![W:program,Y:program,Z:input]:
% 0.49/1.01 ( ( decides @ ( algorithm_of @ W ) @ Y @ Z ) =>
% 0.49/1.01 ( ![Y:program,Z:input]:
% 0.49/1.01 ( ( ( ~( halts2 @ Y @ Z ) ) =>
% 0.49/1.01 ( ( halts3 @ W @ Y @ Z ) & ( outputs @ W @ bad ) ) ) &
% 0.49/1.01 ( ( halts2 @ Y @ Z ) =>
% 0.49/1.01 ( ( halts3 @ W @ Y @ Z ) & ( outputs @ W @ good ) ) ) ) ) ))).
% 0.49/1.01 thf(zip_derived_cl1, plain,
% 0.49/1.01 (![X0 : program, X1 : input, X2 : program, X3 : program, X4 : input]:
% 0.49/1.01 ( (halts2 @ X0 @ X1)
% 0.49/1.01 | (outputs @ X2 @ bad)
% 0.49/1.01 | ~ (decides @ (algorithm_of @ X2) @ X3 @ X4))),
% 0.49/1.01 inference('cnf', [status(esa)], [p2])).
% 0.49/1.01 thf(zip_derived_cl68, plain,
% 0.49/1.01 (![X2 : input, X3 : program]:
% 0.49/1.01 ( (halts2 @ X3 @ X2) | (outputs @ sk_ @ bad))),
% 0.49/1.01 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl1])).
% 0.49/1.01 thf(p3, axiom,
% 0.49/1.01 (( ?[W:program]:
% 0.49/1.01 ( ![Y:program]:
% 0.49/1.01 ( ( ( halts2 @ Y @ ( as_input @ Y ) ) =>
% 0.49/1.01 ( ( outputs @ W @ good ) & ( halts3 @ W @ Y @ ( as_input @ Y ) ) ) ) &
% 0.49/1.01 ( ( ~( halts2 @ Y @ ( as_input @ Y ) ) ) =>
% 0.49/1.01 ( ( outputs @ W @ bad ) & ( halts3 @ W @ Y @ ( as_input @ Y ) ) ) ) ) ) ) =>
% 0.49/1.01 ( ?[V:program]:
% 0.49/1.01 ( ![Y:program]:
% 0.49/1.01 ( ( ( halts2 @ Y @ ( as_input @ Y ) ) =>
% 0.49/1.01 ( ( outputs @ V @ good ) & ( halts2 @ V @ ( as_input @ Y ) ) ) ) &
% 0.49/1.02 ( ( ~( halts2 @ Y @ ( as_input @ Y ) ) ) =>
% 0.49/1.02 ( ( outputs @ V @ bad ) & ( halts2 @ V @ ( as_input @ Y ) ) ) ) ) ) ))).
% 0.49/1.02 thf(zf_stmt_1, axiom,
% 0.49/1.02 (![Y:program,W:program]:
% 0.49/1.02 ( ( ( ~( halts2 @ Y @ ( as_input @ Y ) ) ) =>
% 0.49/1.02 ( ( halts3 @ W @ Y @ ( as_input @ Y ) ) & ( outputs @ W @ bad ) ) ) =>
% 0.49/1.02 ( zip_tseitin_1 @ Y @ W ) ))).
% 0.49/1.02 thf(zip_derived_cl7, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_1 @ X0 @ X1)
% 0.49/1.02 | ~ (halts3 @ X1 @ X0 @ (as_input @ X0))
% 0.49/1.02 | ~ (outputs @ X1 @ bad))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.49/1.02 thf(zf_stmt_2, axiom,
% 0.49/1.02 (![Y:program,W:program]:
% 0.49/1.02 ( ( ( halts2 @ Y @ ( as_input @ Y ) ) =>
% 0.49/1.02 ( ( halts3 @ W @ Y @ ( as_input @ Y ) ) & ( outputs @ W @ good ) ) ) =>
% 0.49/1.02 ( zip_tseitin_0 @ Y @ W ) ))).
% 0.49/1.02 thf(zip_derived_cl6, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_0 @ X0 @ X1) | (halts2 @ X0 @ (as_input @ X0)))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.49/1.02 thf(zf_stmt_3, type, zip_tseitin_4 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_4, axiom,
% 0.49/1.02 (![Y:program,V:program]:
% 0.49/1.02 ( ( zip_tseitin_4 @ Y @ V ) =>
% 0.49/1.02 ( ( ( ~( halts2 @ Y @ ( as_input @ Y ) ) ) => ( zip_tseitin_3 @ Y @ V ) ) &
% 0.49/1.02 ( ( halts2 @ Y @ ( as_input @ Y ) ) => ( zip_tseitin_2 @ Y @ V ) ) ) ))).
% 0.49/1.02 thf(zf_stmt_5, type, zip_tseitin_3 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_6, axiom,
% 0.49/1.02 (![Y:program,V:program]:
% 0.49/1.02 ( ( zip_tseitin_3 @ Y @ V ) =>
% 0.49/1.02 ( ( halts2 @ V @ ( as_input @ Y ) ) & ( outputs @ V @ bad ) ) ))).
% 0.49/1.02 thf(zf_stmt_7, type, zip_tseitin_2 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_8, axiom,
% 0.49/1.02 (![Y:program,V:program]:
% 0.49/1.02 ( ( zip_tseitin_2 @ Y @ V ) =>
% 0.49/1.02 ( ( halts2 @ V @ ( as_input @ Y ) ) & ( outputs @ V @ good ) ) ))).
% 0.49/1.02 thf(zf_stmt_9, type, zip_tseitin_1 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_10, type, zip_tseitin_0 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_11, axiom,
% 0.49/1.02 (( ?[W:program]:
% 0.49/1.02 ( ![Y:program]:
% 0.49/1.02 ( ( zip_tseitin_1 @ Y @ W ) & ( zip_tseitin_0 @ Y @ W ) ) ) ) =>
% 0.49/1.02 ( ?[V:program]: ( ![Y:program]: ( zip_tseitin_4 @ Y @ V ) ) ))).
% 0.49/1.02 thf(zip_derived_cl15, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_4 @ X0 @ sk__3)
% 0.49/1.02 | ~ (zip_tseitin_0 @ (sk__4 @ X1) @ X1)
% 0.49/1.02 | ~ (zip_tseitin_1 @ (sk__4 @ X1) @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.49/1.02 thf(zip_derived_cl33, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ (sk__4 @ X0) @ (as_input @ (sk__4 @ X0)))
% 0.49/1.02 | ~ (zip_tseitin_1 @ (sk__4 @ X0) @ X0)
% 0.49/1.02 | (zip_tseitin_4 @ X1 @ sk__3))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl6, zip_derived_cl15])).
% 0.49/1.02 thf(zip_derived_cl37, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (outputs @ X1 @ bad)
% 0.49/1.02 | ~ (halts3 @ X1 @ (sk__4 @ X1) @ (as_input @ (sk__4 @ X1)))
% 0.49/1.02 | (zip_tseitin_4 @ X0 @ sk__3)
% 0.49/1.02 | (halts2 @ (sk__4 @ X1) @ (as_input @ (sk__4 @ X1))))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl7, zip_derived_cl33])).
% 0.49/1.02 thf(zip_derived_cl89, plain,
% 0.49/1.02 (![X0 : input, X1 : program, X2 : program]:
% 0.49/1.02 ( (halts2 @ X1 @ X0)
% 0.49/1.02 | ~ (halts3 @ sk_ @ (sk__4 @ sk_) @ (as_input @ (sk__4 @ sk_)))
% 0.49/1.02 | (zip_tseitin_4 @ X2 @ sk__3)
% 0.49/1.02 | (halts2 @ (sk__4 @ sk_) @ (as_input @ (sk__4 @ sk_))))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl68, zip_derived_cl37])).
% 0.49/1.02 thf(zip_derived_cl65, plain,
% 0.49/1.02 (![X0 : input, X1 : program]: (decides @ (algorithm_of @ sk_) @ X1 @ X0)),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl0])).
% 0.49/1.02 thf(zip_derived_cl2, plain,
% 0.49/1.02 (![X0 : program, X1 : input, X2 : program, X3 : program, X4 : input]:
% 0.49/1.02 ( (halts2 @ X0 @ X1)
% 0.49/1.02 | (halts3 @ X2 @ X0 @ X1)
% 0.49/1.02 | ~ (decides @ (algorithm_of @ X2) @ X3 @ X4))),
% 0.49/1.02 inference('cnf', [status(esa)], [p2])).
% 0.49/1.02 thf(zip_derived_cl4, plain,
% 0.49/1.02 (![X0 : program, X1 : input, X2 : program, X3 : program, X4 : input]:
% 0.49/1.02 (~ (halts2 @ X0 @ X1)
% 0.49/1.02 | (halts3 @ X2 @ X0 @ X1)
% 0.49/1.02 | ~ (decides @ (algorithm_of @ X2) @ X3 @ X4))),
% 0.49/1.02 inference('cnf', [status(esa)], [p2])).
% 0.49/1.02 thf(zip_derived_cl70, plain,
% 0.49/1.02 (![X0 : program, X1 : input, X2 : program, X3 : program, X4 : input]:
% 0.49/1.02 (~ (decides @ (algorithm_of @ X2) @ X3 @ X4)
% 0.49/1.02 | (halts3 @ X2 @ X0 @ X1))),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl2, zip_derived_cl4])).
% 0.49/1.02 thf(zip_derived_cl71, plain,
% 0.49/1.02 (![X2 : input, X3 : program]: (halts3 @ sk_ @ X3 @ X2)),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl70])).
% 0.49/1.02 thf(zip_derived_cl90, plain,
% 0.49/1.02 (![X0 : input, X1 : program, X2 : program]:
% 0.49/1.02 ( (halts2 @ X1 @ X0)
% 0.49/1.02 | (zip_tseitin_4 @ X2 @ sk__3)
% 0.49/1.02 | (halts2 @ (sk__4 @ sk_) @ (as_input @ (sk__4 @ sk_))))),
% 0.49/1.02 inference('demod', [status(thm)], [zip_derived_cl89, zip_derived_cl71])).
% 0.49/1.02 thf(zip_derived_cl112, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (halts2 @ (sk__4 @ sk_) @ (as_input @ (sk__4 @ sk_)))
% 0.49/1.02 | (zip_tseitin_4 @ X0 @ sk__3))),
% 0.49/1.02 inference('condensation', [status(thm)], [zip_derived_cl90])).
% 0.49/1.02 thf(zip_derived_cl65, plain,
% 0.49/1.02 (![X0 : input, X1 : program]: (decides @ (algorithm_of @ sk_) @ X1 @ X0)),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl0])).
% 0.49/1.02 thf(zip_derived_cl3, plain,
% 0.49/1.02 (![X0 : program, X1 : input, X2 : program, X3 : program, X4 : input]:
% 0.49/1.02 (~ (halts2 @ X0 @ X1)
% 0.49/1.02 | (outputs @ X2 @ good)
% 0.49/1.02 | ~ (decides @ (algorithm_of @ X2) @ X3 @ X4))),
% 0.49/1.02 inference('cnf', [status(esa)], [p2])).
% 0.49/1.02 thf(zip_derived_cl67, plain,
% 0.49/1.02 (![X2 : input, X3 : program]:
% 0.49/1.02 (~ (halts2 @ X3 @ X2) | (outputs @ sk_ @ good))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl3])).
% 0.49/1.02 thf(zip_derived_cl113, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (zip_tseitin_4 @ X0 @ sk__3) | (outputs @ sk_ @ good))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl112, zip_derived_cl67])).
% 0.49/1.02 thf(zip_derived_cl13, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (zip_tseitin_3 @ X0 @ X1)
% 0.49/1.02 | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.49/1.02 thf(zip_derived_cl11, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ X0 @ (as_input @ X1)) | ~ (zip_tseitin_3 @ X1 @ X0))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.49/1.02 thf(zip_derived_cl28, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (zip_tseitin_4 @ X0 @ X1)
% 0.49/1.02 | (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (halts2 @ X1 @ (as_input @ X0)))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl13, zip_derived_cl11])).
% 0.49/1.02 thf(zip_derived_cl14, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (zip_tseitin_2 @ X0 @ X1)
% 0.49/1.02 | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.49/1.02 thf(zip_derived_cl9, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ X0 @ (as_input @ X1)) | ~ (zip_tseitin_2 @ X1 @ X0))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.49/1.02 thf(zip_derived_cl26, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (zip_tseitin_4 @ X0 @ X1)
% 0.49/1.02 | ~ (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (halts2 @ X1 @ (as_input @ X0)))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl14, zip_derived_cl9])).
% 0.49/1.02 thf(zip_derived_cl78, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ X1 @ (as_input @ X0)) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl28, zip_derived_cl26])).
% 0.49/1.02 thf(zip_derived_cl118, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (outputs @ sk_ @ good) | (halts2 @ sk__3 @ (as_input @ X0)))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl113, zip_derived_cl78])).
% 0.49/1.02 thf(zip_derived_cl67, plain,
% 0.49/1.02 (![X2 : input, X3 : program]:
% 0.49/1.02 (~ (halts2 @ X3 @ X2) | (outputs @ sk_ @ good))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl3])).
% 0.49/1.02 thf(zip_derived_cl122, plain, ( (outputs @ sk_ @ good)),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl118, zip_derived_cl67])).
% 0.49/1.02 thf(zip_derived_cl7, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_1 @ X0 @ X1)
% 0.49/1.02 | ~ (halts3 @ X1 @ X0 @ (as_input @ X0))
% 0.49/1.02 | ~ (outputs @ X1 @ bad))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.49/1.02 thf(zip_derived_cl5, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_0 @ X0 @ X1)
% 0.49/1.02 | ~ (halts3 @ X1 @ X0 @ (as_input @ X0))
% 0.49/1.02 | ~ (outputs @ X1 @ good))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.49/1.02 thf(zip_derived_cl15, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_4 @ X0 @ sk__3)
% 0.49/1.02 | ~ (zip_tseitin_0 @ (sk__4 @ X1) @ X1)
% 0.49/1.02 | ~ (zip_tseitin_1 @ (sk__4 @ X1) @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.49/1.02 thf(zip_derived_cl32, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (outputs @ X0 @ good)
% 0.49/1.02 | ~ (halts3 @ X0 @ (sk__4 @ X0) @ (as_input @ (sk__4 @ X0)))
% 0.49/1.02 | ~ (zip_tseitin_1 @ (sk__4 @ X0) @ X0)
% 0.49/1.02 | (zip_tseitin_4 @ X1 @ sk__3))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl5, zip_derived_cl15])).
% 0.49/1.02 thf(zip_derived_cl36, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (outputs @ X1 @ bad)
% 0.49/1.02 | ~ (halts3 @ X1 @ (sk__4 @ X1) @ (as_input @ (sk__4 @ X1)))
% 0.49/1.02 | (zip_tseitin_4 @ X0 @ sk__3)
% 0.49/1.02 | ~ (halts3 @ X1 @ (sk__4 @ X1) @ (as_input @ (sk__4 @ X1)))
% 0.49/1.02 | ~ (outputs @ X1 @ good))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl7, zip_derived_cl32])).
% 0.49/1.02 thf(zip_derived_cl81, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (outputs @ X1 @ good)
% 0.49/1.02 | (zip_tseitin_4 @ X0 @ sk__3)
% 0.49/1.02 | ~ (halts3 @ X1 @ (sk__4 @ X1) @ (as_input @ (sk__4 @ X1)))
% 0.49/1.02 | ~ (outputs @ X1 @ bad))),
% 0.49/1.02 inference('simplify', [status(thm)], [zip_derived_cl36])).
% 0.49/1.02 thf(zip_derived_cl126, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (zip_tseitin_4 @ X0 @ sk__3)
% 0.49/1.02 | ~ (halts3 @ sk_ @ (sk__4 @ sk_) @ (as_input @ (sk__4 @ sk_)))
% 0.49/1.02 | ~ (outputs @ sk_ @ bad))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl122, zip_derived_cl81])).
% 0.49/1.02 thf(zip_derived_cl71, plain,
% 0.49/1.02 (![X2 : input, X3 : program]: (halts3 @ sk_ @ X3 @ X2)),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl70])).
% 0.49/1.02 thf(zip_derived_cl68, plain,
% 0.49/1.02 (![X2 : input, X3 : program]:
% 0.49/1.02 ( (halts2 @ X3 @ X2) | (outputs @ sk_ @ bad))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl1])).
% 0.49/1.02 thf(zip_derived_cl67, plain,
% 0.49/1.02 (![X2 : input, X3 : program]:
% 0.49/1.02 (~ (halts2 @ X3 @ X2) | (outputs @ sk_ @ good))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl3])).
% 0.49/1.02 thf(zip_derived_cl72, plain,
% 0.49/1.02 (( (outputs @ sk_ @ bad) | (outputs @ sk_ @ good))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl68, zip_derived_cl67])).
% 0.49/1.02 thf(p4, axiom,
% 0.49/1.02 (( ?[V:program]:
% 0.49/1.02 ( ![Y:program]:
% 0.49/1.02 ( ( ( halts2 @ Y @ ( as_input @ Y ) ) =>
% 0.49/1.02 ( ( outputs @ V @ good ) & ( halts2 @ V @ ( as_input @ Y ) ) ) ) &
% 0.49/1.02 ( ( ~( halts2 @ Y @ ( as_input @ Y ) ) ) =>
% 0.49/1.02 ( ( outputs @ V @ bad ) & ( halts2 @ V @ ( as_input @ Y ) ) ) ) ) ) ) =>
% 0.49/1.02 ( ?[U:program]:
% 0.49/1.02 ( ![Y:program]:
% 0.49/1.02 ( ( ( halts2 @ Y @ ( as_input @ Y ) ) =>
% 0.49/1.02 ( ~( halts2 @ U @ ( as_input @ Y ) ) ) ) &
% 0.49/1.02 ( ( ~( halts2 @ Y @ ( as_input @ Y ) ) ) =>
% 0.49/1.02 ( ( outputs @ U @ bad ) & ( halts2 @ U @ ( as_input @ Y ) ) ) ) ) ) ))).
% 0.49/1.02 thf(zf_stmt_12, axiom,
% 0.49/1.02 (![Y:program,V:program]:
% 0.49/1.02 ( ( ( ~( halts2 @ Y @ ( as_input @ Y ) ) ) =>
% 0.49/1.02 ( ( halts2 @ V @ ( as_input @ Y ) ) & ( outputs @ V @ bad ) ) ) =>
% 0.49/1.02 ( zip_tseitin_6 @ Y @ V ) ))).
% 0.49/1.02 thf(zip_derived_cl19, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_6 @ X0 @ X1) | ~ (halts2 @ X0 @ (as_input @ X0)))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_12])).
% 0.49/1.02 thf(zf_stmt_13, axiom,
% 0.49/1.02 (![Y:program,V:program]:
% 0.49/1.02 ( ( ( halts2 @ Y @ ( as_input @ Y ) ) =>
% 0.49/1.02 ( ( halts2 @ V @ ( as_input @ Y ) ) & ( outputs @ V @ good ) ) ) =>
% 0.49/1.02 ( zip_tseitin_5 @ Y @ V ) ))).
% 0.49/1.02 thf(zip_derived_cl16, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_5 @ X0 @ X1)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ X0))
% 0.49/1.02 | ~ (outputs @ X1 @ good))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_13])).
% 0.49/1.02 thf(zf_stmt_14, type, zip_tseitin_8 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_15, axiom,
% 0.49/1.02 (![Y:program,U:program]:
% 0.49/1.02 ( ( zip_tseitin_8 @ Y @ U ) =>
% 0.49/1.02 ( ( ( ~( halts2 @ Y @ ( as_input @ Y ) ) ) => ( zip_tseitin_7 @ Y @ U ) ) &
% 0.49/1.02 ( ( halts2 @ Y @ ( as_input @ Y ) ) =>
% 0.49/1.02 ( ~( halts2 @ U @ ( as_input @ Y ) ) ) ) ) ))).
% 0.49/1.02 thf(zf_stmt_16, type, zip_tseitin_7 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_17, axiom,
% 0.49/1.02 (![Y:program,U:program]:
% 0.49/1.02 ( ( zip_tseitin_7 @ Y @ U ) =>
% 0.49/1.02 ( ( halts2 @ U @ ( as_input @ Y ) ) & ( outputs @ U @ bad ) ) ))).
% 0.49/1.02 thf(zf_stmt_18, type, zip_tseitin_6 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_19, type, zip_tseitin_5 : program > program > $o).
% 0.49/1.02 thf(zf_stmt_20, axiom,
% 0.49/1.02 (( ?[V:program]:
% 0.49/1.02 ( ![Y:program]:
% 0.49/1.02 ( ( zip_tseitin_6 @ Y @ V ) & ( zip_tseitin_5 @ Y @ V ) ) ) ) =>
% 0.49/1.02 ( ?[U:program]: ( ![Y:program]: ( zip_tseitin_8 @ Y @ U ) ) ))).
% 0.49/1.02 thf(zip_derived_cl24, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | ~ (zip_tseitin_5 @ (sk__6 @ X1) @ X1)
% 0.49/1.02 | ~ (zip_tseitin_6 @ (sk__6 @ X1) @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_20])).
% 0.49/1.02 thf(zip_derived_cl34, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (outputs @ X0 @ good)
% 0.49/1.02 | ~ (halts2 @ X0 @ (as_input @ (sk__6 @ X0)))
% 0.49/1.02 | ~ (zip_tseitin_6 @ (sk__6 @ X0) @ X0)
% 0.49/1.02 | (zip_tseitin_8 @ X1 @ sk__5))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl16, zip_derived_cl24])).
% 0.49/1.02 thf(zip_derived_cl42, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (halts2 @ (sk__6 @ X1) @ (as_input @ (sk__6 @ X1)))
% 0.49/1.02 | (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ (sk__6 @ X1)))
% 0.49/1.02 | ~ (outputs @ X1 @ good))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl19, zip_derived_cl34])).
% 0.49/1.02 thf(zip_derived_cl86, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (outputs @ sk_ @ bad)
% 0.49/1.02 | ~ (halts2 @ (sk__6 @ sk_) @ (as_input @ (sk__6 @ sk_)))
% 0.49/1.02 | (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | ~ (halts2 @ sk_ @ (as_input @ (sk__6 @ sk_))))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl72, zip_derived_cl42])).
% 0.49/1.02 thf(zip_derived_cl68, plain,
% 0.49/1.02 (![X2 : input, X3 : program]:
% 0.49/1.02 ( (halts2 @ X3 @ X2) | (outputs @ sk_ @ bad))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl1])).
% 0.49/1.02 thf(zip_derived_cl106, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 (~ (halts2 @ sk_ @ (as_input @ (sk__6 @ sk_)))
% 0.49/1.02 | (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | (outputs @ sk_ @ bad))),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl86, zip_derived_cl68])).
% 0.49/1.02 thf(zip_derived_cl68, plain,
% 0.49/1.02 (![X2 : input, X3 : program]:
% 0.49/1.02 ( (halts2 @ X3 @ X2) | (outputs @ sk_ @ bad))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl1])).
% 0.49/1.02 thf(zip_derived_cl107, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (outputs @ sk_ @ bad) | (zip_tseitin_8 @ X0 @ sk__5))),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl106, zip_derived_cl68])).
% 0.49/1.02 thf(zip_derived_cl68, plain,
% 0.49/1.02 (![X2 : input, X3 : program]:
% 0.49/1.02 ( (halts2 @ X3 @ X2) | (outputs @ sk_ @ bad))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl1])).
% 0.49/1.02 thf(zip_derived_cl23, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ X0))
% 0.49/1.02 | ~ (zip_tseitin_8 @ X0 @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_15])).
% 0.49/1.02 thf(zip_derived_cl73, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (outputs @ sk_ @ bad)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ X0))
% 0.49/1.02 | ~ (zip_tseitin_8 @ X0 @ X1))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl68, zip_derived_cl23])).
% 0.49/1.02 thf(zip_derived_cl68, plain,
% 0.49/1.02 (![X2 : input, X3 : program]:
% 0.49/1.02 ( (halts2 @ X3 @ X2) | (outputs @ sk_ @ bad))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl65, zip_derived_cl1])).
% 0.49/1.02 thf(zip_derived_cl77, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (zip_tseitin_8 @ X0 @ X1) | (outputs @ sk_ @ bad))),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl73, zip_derived_cl68])).
% 0.49/1.02 thf(zip_derived_cl108, plain, ( (outputs @ sk_ @ bad)),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl107, zip_derived_cl77])).
% 0.49/1.02 thf(zip_derived_cl129, plain,
% 0.49/1.02 (![X0 : program]: (zip_tseitin_4 @ X0 @ sk__3)),
% 0.49/1.02 inference('demod', [status(thm)],
% 0.49/1.02 [zip_derived_cl126, zip_derived_cl71, zip_derived_cl108])).
% 0.49/1.02 thf(zip_derived_cl13, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (zip_tseitin_3 @ X0 @ X1)
% 0.49/1.02 | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.49/1.02 thf(zip_derived_cl12, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (outputs @ X0 @ bad) | ~ (zip_tseitin_3 @ X1 @ X0))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.49/1.02 thf(zip_derived_cl29, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (zip_tseitin_4 @ X1 @ X0)
% 0.49/1.02 | (halts2 @ X1 @ (as_input @ X1))
% 0.49/1.02 | (outputs @ X0 @ bad))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl13, zip_derived_cl12])).
% 0.49/1.02 thf(zip_derived_cl131, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (halts2 @ X0 @ (as_input @ X0)) | (outputs @ sk__3 @ bad))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl129, zip_derived_cl29])).
% 0.49/1.02 thf(zip_derived_cl129, plain,
% 0.49/1.02 (![X0 : program]: (zip_tseitin_4 @ X0 @ sk__3)),
% 0.49/1.02 inference('demod', [status(thm)],
% 0.49/1.02 [zip_derived_cl126, zip_derived_cl71, zip_derived_cl108])).
% 0.49/1.02 thf(zip_derived_cl129, plain,
% 0.49/1.02 (![X0 : program]: (zip_tseitin_4 @ X0 @ sk__3)),
% 0.49/1.02 inference('demod', [status(thm)],
% 0.49/1.02 [zip_derived_cl126, zip_derived_cl71, zip_derived_cl108])).
% 0.49/1.02 thf(zip_derived_cl78, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ X1 @ (as_input @ X0)) | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl28, zip_derived_cl26])).
% 0.49/1.02 thf(zip_derived_cl130, plain,
% 0.49/1.02 (![X0 : program]: (halts2 @ sk__3 @ (as_input @ X0))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl129, zip_derived_cl78])).
% 0.49/1.02 thf(zip_derived_cl14, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (zip_tseitin_2 @ X0 @ X1)
% 0.49/1.02 | ~ (zip_tseitin_4 @ X0 @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.49/1.02 thf(zip_derived_cl10, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (outputs @ X0 @ good) | ~ (zip_tseitin_2 @ X1 @ X0))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.49/1.02 thf(zip_derived_cl27, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (zip_tseitin_4 @ X1 @ X0)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ X1))
% 0.49/1.02 | (outputs @ X0 @ good))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl14, zip_derived_cl10])).
% 0.49/1.02 thf(zip_derived_cl133, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 (~ (zip_tseitin_4 @ sk__3 @ X0) | (outputs @ X0 @ good))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl130, zip_derived_cl27])).
% 0.49/1.02 thf(zip_derived_cl135, plain, ( (outputs @ sk__3 @ good)),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl129, zip_derived_cl133])).
% 0.49/1.02 thf(zip_derived_cl42, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (halts2 @ (sk__6 @ X1) @ (as_input @ (sk__6 @ X1)))
% 0.49/1.02 | (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ (sk__6 @ X1)))
% 0.49/1.02 | ~ (outputs @ X1 @ good))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl19, zip_derived_cl34])).
% 0.49/1.02 thf(zip_derived_cl136, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 (~ (halts2 @ (sk__6 @ sk__3) @ (as_input @ (sk__6 @ sk__3)))
% 0.49/1.02 | (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | ~ (halts2 @ sk__3 @ (as_input @ (sk__6 @ sk__3))))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl135, zip_derived_cl42])).
% 0.49/1.02 thf(zip_derived_cl130, plain,
% 0.49/1.02 (![X0 : program]: (halts2 @ sk__3 @ (as_input @ X0))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl129, zip_derived_cl78])).
% 0.49/1.02 thf(zip_derived_cl138, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 (~ (halts2 @ (sk__6 @ sk__3) @ (as_input @ (sk__6 @ sk__3)))
% 0.49/1.02 | (zip_tseitin_8 @ X0 @ sk__5))),
% 0.49/1.02 inference('demod', [status(thm)], [zip_derived_cl136, zip_derived_cl130])).
% 0.49/1.02 thf(zip_derived_cl143, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (outputs @ sk__3 @ bad) | (zip_tseitin_8 @ X0 @ sk__5))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl131, zip_derived_cl138])).
% 0.49/1.02 thf(zip_derived_cl135, plain, ( (outputs @ sk__3 @ good)),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl129, zip_derived_cl133])).
% 0.49/1.02 thf(zip_derived_cl18, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (zip_tseitin_6 @ X0 @ X1)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ X0))
% 0.49/1.02 | ~ (outputs @ X1 @ bad))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_12])).
% 0.49/1.02 thf(zip_derived_cl34, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (outputs @ X0 @ good)
% 0.49/1.02 | ~ (halts2 @ X0 @ (as_input @ (sk__6 @ X0)))
% 0.49/1.02 | ~ (zip_tseitin_6 @ (sk__6 @ X0) @ X0)
% 0.49/1.02 | (zip_tseitin_8 @ X1 @ sk__5))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl16, zip_derived_cl24])).
% 0.49/1.02 thf(zip_derived_cl40, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (outputs @ X1 @ bad)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ (sk__6 @ X1)))
% 0.49/1.02 | (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ (sk__6 @ X1)))
% 0.49/1.02 | ~ (outputs @ X1 @ good))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl18, zip_derived_cl34])).
% 0.49/1.02 thf(zip_derived_cl79, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (outputs @ X1 @ good)
% 0.49/1.02 | (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ (sk__6 @ X1)))
% 0.49/1.02 | ~ (outputs @ X1 @ bad))),
% 0.49/1.02 inference('simplify', [status(thm)], [zip_derived_cl40])).
% 0.49/1.02 thf(zip_derived_cl137, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (zip_tseitin_8 @ X0 @ sk__5)
% 0.49/1.02 | ~ (halts2 @ sk__3 @ (as_input @ (sk__6 @ sk__3)))
% 0.49/1.02 | ~ (outputs @ sk__3 @ bad))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl135, zip_derived_cl79])).
% 0.49/1.02 thf(zip_derived_cl130, plain,
% 0.49/1.02 (![X0 : program]: (halts2 @ sk__3 @ (as_input @ X0))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl129, zip_derived_cl78])).
% 0.49/1.02 thf(zip_derived_cl139, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (zip_tseitin_8 @ X0 @ sk__5) | ~ (outputs @ sk__3 @ bad))),
% 0.49/1.02 inference('demod', [status(thm)], [zip_derived_cl137, zip_derived_cl130])).
% 0.49/1.02 thf(zip_derived_cl150, plain,
% 0.49/1.02 (![X0 : program]: (zip_tseitin_8 @ X0 @ sk__5)),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl143, zip_derived_cl139])).
% 0.49/1.02 thf(zip_derived_cl150, plain,
% 0.49/1.02 (![X0 : program]: (zip_tseitin_8 @ X0 @ sk__5)),
% 0.49/1.02 inference('clc', [status(thm)], [zip_derived_cl143, zip_derived_cl139])).
% 0.49/1.02 thf(zip_derived_cl22, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (zip_tseitin_7 @ X0 @ X1)
% 0.49/1.02 | ~ (zip_tseitin_8 @ X0 @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_15])).
% 0.49/1.02 thf(zip_derived_cl20, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 ( (halts2 @ X0 @ (as_input @ X1)) | ~ (zip_tseitin_7 @ X1 @ X0))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.49/1.02 thf(zip_derived_cl30, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (zip_tseitin_8 @ X0 @ X1)
% 0.49/1.02 | (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (halts2 @ X1 @ (as_input @ X0)))),
% 0.49/1.02 inference('dp-resolution', [status(thm)],
% 0.49/1.02 [zip_derived_cl22, zip_derived_cl20])).
% 0.49/1.02 thf(zip_derived_cl151, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 ( (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | (halts2 @ sk__5 @ (as_input @ X0)))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl150, zip_derived_cl30])).
% 0.49/1.02 thf(zip_derived_cl169, plain, ( (halts2 @ sk__5 @ (as_input @ sk__5))),
% 0.49/1.02 inference('eq_fact', [status(thm)], [zip_derived_cl151])).
% 0.49/1.02 thf(zip_derived_cl23, plain,
% 0.49/1.02 (![X0 : program, X1 : program]:
% 0.49/1.02 (~ (halts2 @ X0 @ (as_input @ X0))
% 0.49/1.02 | ~ (halts2 @ X1 @ (as_input @ X0))
% 0.49/1.02 | ~ (zip_tseitin_8 @ X0 @ X1))),
% 0.49/1.02 inference('cnf', [status(esa)], [zf_stmt_15])).
% 0.49/1.02 thf(zip_derived_cl171, plain,
% 0.49/1.02 (![X0 : program]:
% 0.49/1.02 (~ (halts2 @ X0 @ (as_input @ sk__5)) | ~ (zip_tseitin_8 @ sk__5 @ X0))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl169, zip_derived_cl23])).
% 0.49/1.02 thf(zip_derived_cl173, plain, (~ (halts2 @ sk__5 @ (as_input @ sk__5))),
% 0.49/1.02 inference('s_sup-', [status(thm)], [zip_derived_cl150, zip_derived_cl171])).
% 0.49/1.02 thf(zip_derived_cl169, plain, ( (halts2 @ sk__5 @ (as_input @ sk__5))),
% 0.49/1.02 inference('eq_fact', [status(thm)], [zip_derived_cl151])).
% 0.49/1.02 thf(zip_derived_cl174, plain, ($false),
% 0.49/1.02 inference('demod', [status(thm)], [zip_derived_cl173, zip_derived_cl169])).
% 0.49/1.02
% 0.49/1.02 % SZS output end Refutation
% 0.49/1.02
% 0.49/1.02
% 0.49/1.02 % Terminating...
% 2.07/1.20 % Runner terminated.
% 2.10/1.21 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------