%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PUZ037-3 : TPTP v9.2.0. Released v2.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.UAl1LVkpLQ true
% Computer : n022.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:49:34 PM UTC 2025
% Result : Unsatisfiable 129.50s 19.15s
% Output : Refutation 129.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : PUZ037-3 : TPTP v9.2.0. Released v2.3.0.
% 0.11/0.14 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.UAl1LVkpLQ true
% 0.13/0.35 % Computer : n022.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 1 15:09:38 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.13/0.35 % Running portfolio for 300 s
% 0.13/0.35 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.36 % Number of cores: 8
% 0.13/0.36 % Python version: Python 3.6.8
% 0.13/0.36 % Running in FO mode
% 0.50/0.60 % Total configuration time : 435
% 0.50/0.60 % Estimated wc time : 1092
% 0.50/0.60 % Estimated cpu time (7 cpus) : 156.0
% 0.52/0.72 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo13.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo5.sh running for 50s
% 0.52/0.73 % /export/starexec/sandbox/solver/bin/fo/fo4.sh running for 50s
% 129.50/19.15 % Solved by fo/fo6_bce.sh.
% 129.50/19.15 % BCE start: 20
% 129.50/19.15 % BCE eliminated: 0
% 129.50/19.15 % PE start: 20
% 129.50/19.15 logic: neq
% 129.50/19.15 % PE eliminated: 0
% 129.50/19.15 % done 1621 iterations in 18.401s
% 129.50/19.15 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 129.50/19.15 % SZS output start Refutation
% 129.50/19.15 thf(state_type, type, state: $i > $i > $i > $i > $i > $i > $i > $i > $i >
% 129.50/19.15 $i > $i > $i > $i > $i > $i > $i > $i > $i >
% 129.50/19.15 $i > $i > $i > $i > $i > $i > $i > $i > $i >
% 129.50/19.15 $i > $i > $i > $i > $i > $i > $i > $i > $i >
% 129.50/19.15 $i > $i > $i > $i > $i > $i > $i > $i > $i >
% 129.50/19.15 $i > $i > $i > $i > $i > $i > $i > $i > $i > $o).
% 129.50/19.15 thf(g_type, type, g: $i).
% 129.50/19.15 thf(b_type, type, b: $i).
% 129.50/19.15 thf(y_type, type, y: $i).
% 129.50/19.15 thf(w_type, type, w: $i).
% 129.50/19.15 thf(o_type, type, o: $i).
% 129.50/19.15 thf(r_type, type, r: $i).
% 129.50/19.15 thf(make_like_this, conjecture,
% 129.50/19.15 (state @
% 129.50/19.15 b @ b @ b @ b @ b @ b @ b @ b @ b @ r @ r @ r @ g @ g @ g @ o @ o @ o @
% 129.50/19.15 y @ y @ y @ r @ r @ r @ g @ g @ g @ o @ o @ o @ y @ y @ y @ r @ r @ r @
% 129.50/19.15 g @ g @ g @ o @ o @ o @ y @ y @ y @ w @ w @ w @ w @ w @ w @ w @ w @ w)).
% 129.50/19.15 thf(zf_stmt_0, negated_conjecture,
% 129.50/19.15 (~( state @
% 129.50/19.15 b @ b @ b @ b @ b @ b @ b @ b @ b @ r @ r @ r @ g @ g @ g @ o @ o @
% 129.50/19.15 o @ y @ y @ y @ r @ r @ r @ g @ g @ g @ o @ o @ o @ y @ y @ y @ r @
% 129.50/19.15 r @ r @ g @ g @ g @ o @ o @ o @ y @ y @ y @ w @ w @ w @ w @ w @ w @
% 129.50/19.15 w @ w @ w )),
% 129.50/19.15 inference('cnf.neg', [status(esa)], [make_like_this])).
% 129.50/19.15 thf(zip_derived_cl0, plain,
% 129.50/19.15 (~ (state @ b @ b @ b @ b @ b @ b @ b @ b @ b @ r @ r @ r @ g @ g @ g @
% 129.50/19.15 o @ o @ o @ y @ y @ y @ r @ r @ r @ g @ g @ g @ o @ o @ o @ y @ y @
% 129.50/19.15 y @ r @ r @ r @ g @ g @ g @ o @ o @ o @ y @ y @ y @ w @ w @ w @ w @
% 129.50/19.15 w @ w @ w @ w @ w)),
% 129.50/19.15 inference('cnf', [status(esa)], [zf_stmt_0])).
% 129.50/19.15 thf(start_with_this, axiom,
% 129.50/19.15 (state @
% 129.50/19.15 b @ r @ r @ w @ w @ w @ y @ b @ b @ g @ y @ r @ b @ g @ g @ o @ g @ y @
% 129.50/19.15 w @ w @ r @ g @ o @ r @ b @ g @ g @ o @ r @ b @ y @ y @ r @ g @ o @ g @
% 129.50/19.15 o @ o @ o @ y @ r @ b @ y @ y @ r @ w @ w @ w @ b @ b @ y @ w @ o @ o)).
% 129.50/19.15 thf(zip_derived_cl1, plain,
% 129.50/19.15 ( (state @ b @ r @ r @ w @ w @ w @ y @ b @ b @ g @ y @ r @ b @ g @ g @
% 129.50/19.15 o @ g @ y @ w @ w @ r @ g @ o @ r @ b @ g @ g @ o @ r @ b @ y @ y @
% 129.50/19.15 r @ g @ o @ g @ o @ o @ o @ y @ r @ b @ y @ y @ r @ w @ w @ w @ b @
% 129.50/19.15 b @ y @ w @ o @ o)),
% 129.50/19.15 inference('cnf', [status(esa)], [start_with_this])).
% 129.50/19.15 thf(bzy, axiom,
% 129.50/19.15 (( ~( state @
% 129.50/19.15 Y1 @ Y2 @ Y3 @ A1 @ A2 @ A3 @ A4 @ A5 @ A6 @ X9 @ A7 @ A8 @ A9 @
% 129.50/19.15 B1 @ B2 @ B3 @ B4 @ X1 @ W1 @ W8 @ W7 @ X8 @ B5 @ B6 @ B7 @ B8 @
% 129.50/19.15 B9 @ C1 @ C2 @ X2 @ W2 @ C3 @ W6 @ X7 @ C4 @ C5 @ C6 @ C7 @ C8 @
% 129.50/19.15 C9 @ D1 @ X3 @ W3 @ W4 @ W5 @ D2 @ D3 @ D4 @ D5 @ D6 @ D7 @ X6 @
% 129.50/19.15 X5 @ X4 ) ) |
% 129.50/19.15 ( state @
% 129.50/19.15 X1 @ X2 @ X3 @ A1 @ A2 @ A3 @ A4 @ A5 @ A6 @ Y3 @ A7 @ A8 @ A9 @ B1 @
% 129.50/19.15 B2 @ B3 @ B4 @ X4 @ W3 @ W2 @ W1 @ Y2 @ B5 @ B6 @ B7 @ B8 @ B9 @ C1 @
% 129.50/19.15 C2 @ X5 @ W4 @ C3 @ W8 @ Y1 @ C4 @ C5 @ C6 @ C7 @ C8 @ C9 @ D1 @ X6 @
% 129.50/19.15 W5 @ W6 @ W7 @ D2 @ D3 @ D4 @ D5 @ D6 @ D7 @ X9 @ X8 @ X7 ))).
% 129.50/19.15 thf(zip_derived_cl7, plain,
% 129.50/19.15 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i,
% 129.50/19.15 X7 : $i, X8 : $i, X9 : $i, X10 : $i, X11 : $i, X12 : $i, X13 : $i,
% 129.50/19.15 X14 : $i, X15 : $i, X16 : $i, X17 : $i, X18 : $i, X19 : $i, X20 : $i,
% 129.50/19.15 X21 : $i, X22 : $i, X23 : $i, X24 : $i, X25 : $i, X26 : $i, X27 : $i,
% 129.50/19.15 X28 : $i, X29 : $i, X30 : $i, X31 : $i, X32 : $i, X33 : $i, X34 : $i,
% 129.50/19.15 X35 : $i, X36 : $i, X37 : $i, X38 : $i, X39 : $i, X40 : $i, X41 : $i,
% 129.50/19.15 X42 : $i, X43 : $i, X44 : $i, X45 : $i, X46 : $i, X47 : $i, X48 : $i,
% 129.50/19.15 X49 : $i, X50 : $i, X51 : $i, X52 : $i, X53 : $i]:
% 129.50/19.15 (~ (state @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @
% 129.50/19.15 X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @
% 129.50/19.15 X22 @ X23 @ X24 @ X25 @ X26 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @
% 129.50/19.15 X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X39 @ X40 @ X41 @ X42 @ X43 @
% 129.50/19.15 X44 @ X45 @ X46 @ X47 @ X48 @ X49 @ X50 @ X51 @ X52 @ X53)
% 129.50/19.15 | (state @ X17 @ X29 @ X41 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X2 @
% 129.50/19.15 X10 @ X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X53 @ X42 @ X30 @
% 129.50/19.15 X18 @ X1 @ X22 @ X23 @ X24 @ X25 @ X26 @ X27 @ X28 @ X52 @ X43 @
% 129.50/19.15 X31 @ X19 @ X0 @ X34 @ X35 @ X36 @ X37 @ X38 @ X39 @ X40 @ X51 @
% 129.50/19.15 X44 @ X32 @ X20 @ X45 @ X46 @ X47 @ X48 @ X49 @ X50 @ X9 @ X21 @
% 129.50/19.15 X33))),
% 129.50/19.15 inference('cnf', [status(esa)], [bzy])).
% 129.50/19.15 thf(zip_derived_cl72, plain,
% 129.50/19.15 ( (state @ y @ b @ b @ w @ w @ w @ y @ b @ b @ r @ y @ r @ b @ g @ g @
% 129.50/19.15 o @ g @ o @ y @ y @ w @ r @ o @ r @ b @ g @ g @ o @ r @ o @ y @ y @
% 129.50/19.15 w @ b @ o @ g @ o @ o @ o @ y @ r @ w @ r @ r @ r @ w @ w @ w @ b @
% 129.50/19.15 b @ y @ g @ g @ g)),
% 129.50/19.15 inference('s_sup-', [status(thm)], [zip_derived_cl1, zip_derived_cl7])).
% 129.50/19.15 thf(mzy, axiom,
% 129.50/19.15 (( ~( state @
% 129.50/19.15 A1 @ A2 @ A3 @ Y1 @ Y2 @ Y3 @ A4 @ A5 @ A6 @ A7 @ X9 @ A8 @ A9 @
% 129.50/19.15 B1 @ B2 @ B3 @ X1 @ B4 @ B5 @ B6 @ B7 @ B8 @ X8 @ B9 @ C1 @ C2 @
% 129.50/19.15 C3 @ C4 @ X2 @ C5 @ C6 @ C7 @ C8 @ C9 @ X7 @ D1 @ D2 @ D3 @ D4 @
% 129.50/19.15 D5 @ X3 @ D6 @ D7 @ D8 @ D9 @ E1 @ E2 @ E3 @ X6 @ X5 @ X4 @ E4 @
% 129.50/19.15 E5 @ E6 ) ) |
% 129.50/19.15 ( state @
% 129.50/19.15 A1 @ A2 @ A3 @ X1 @ X2 @ X3 @ A4 @ A5 @ A6 @ A7 @ Y3 @ A8 @ A9 @ B1 @
% 129.50/19.15 B2 @ B3 @ X4 @ B4 @ B5 @ B6 @ B7 @ B8 @ Y2 @ B9 @ C1 @ C2 @ C3 @ C4 @
% 129.50/19.15 X5 @ C5 @ C6 @ C7 @ C8 @ C9 @ Y1 @ D1 @ D2 @ D3 @ D4 @ D5 @ X6 @ D6 @
% 129.50/19.15 D7 @ D8 @ D9 @ E1 @ E2 @ E3 @ X9 @ X8 @ X7 @ E4 @ E5 @ E6 ))).
% 129.50/19.15 thf(zip_derived_cl6, plain,
% 129.50/19.15 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i,
% 129.50/19.15 X7 : $i, X8 : $i, X9 : $i, X10 : $i, X11 : $i, X12 : $i, X13 : $i,
% 129.50/19.15 X14 : $i, X15 : $i, X16 : $i, X17 : $i, X18 : $i, X19 : $i, X20 : $i,
% 129.50/19.15 X21 : $i, X22 : $i, X23 : $i, X24 : $i, X25 : $i, X26 : $i, X27 : $i,
% 129.50/19.15 X28 : $i, X29 : $i, X30 : $i, X31 : $i, X32 : $i, X33 : $i, X34 : $i,
% 129.50/19.15 X35 : $i, X36 : $i, X37 : $i, X38 : $i, X39 : $i, X40 : $i, X41 : $i,
% 129.50/19.15 X42 : $i, X43 : $i, X44 : $i, X45 : $i, X46 : $i, X47 : $i, X48 : $i,
% 129.50/19.15 X49 : $i, X50 : $i, X51 : $i, X52 : $i, X53 : $i]:
% 129.50/19.15 (~ (state @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @
% 129.50/19.15 X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @
% 129.50/19.15 X22 @ X23 @ X24 @ X25 @ X26 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @
% 129.50/19.15 X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X39 @ X40 @ X41 @ X42 @ X43 @
% 129.50/19.15 X44 @ X45 @ X46 @ X47 @ X48 @ X49 @ X50 @ X51 @ X52 @ X53)
% 129.50/19.15 | (state @ X0 @ X1 @ X2 @ X16 @ X28 @ X40 @ X6 @ X7 @ X8 @ X9 @
% 129.50/19.15 X5 @ X11 @ X12 @ X13 @ X14 @ X15 @ X50 @ X17 @ X18 @ X19 @ X20 @
% 129.50/19.15 X21 @ X4 @ X23 @ X24 @ X25 @ X26 @ X27 @ X49 @ X29 @ X30 @ X31 @
% 129.50/19.15 X32 @ X33 @ X3 @ X35 @ X36 @ X37 @ X38 @ X39 @ X48 @ X41 @ X42 @
% 129.50/19.15 X43 @ X44 @ X45 @ X46 @ X47 @ X10 @ X22 @ X34 @ X51 @ X52 @ X53))),
% 129.50/19.15 inference('cnf', [status(esa)], [mzy])).
% 129.50/19.15 thf(zip_derived_cl94, plain,
% 129.50/19.15 ( (state @ y @ b @ b @ g @ r @ r @ y @ b @ b @ r @ w @ r @ b @ g @ g @
% 129.50/19.15 o @ y @ o @ y @ y @ w @ r @ w @ r @ b @ g @ g @ o @ b @ o @ y @ y @
% 129.50/19.15 w @ b @ w @ g @ o @ o @ o @ y @ b @ w @ r @ r @ r @ w @ w @ w @ y @
% 129.50/19.15 o @ o @ g @ g @ g)),
% 129.50/19.15 inference('s_sup-', [status(thm)], [zip_derived_cl72, zip_derived_cl6])).
% 129.50/19.15 thf(zip_derived_cl6, plain,
% 129.50/19.15 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i,
% 129.50/19.15 X7 : $i, X8 : $i, X9 : $i, X10 : $i, X11 : $i, X12 : $i, X13 : $i,
% 129.50/19.15 X14 : $i, X15 : $i, X16 : $i, X17 : $i, X18 : $i, X19 : $i, X20 : $i,
% 129.50/19.15 X21 : $i, X22 : $i, X23 : $i, X24 : $i, X25 : $i, X26 : $i, X27 : $i,
% 129.50/19.15 X28 : $i, X29 : $i, X30 : $i, X31 : $i, X32 : $i, X33 : $i, X34 : $i,
% 129.50/19.15 X35 : $i, X36 : $i, X37 : $i, X38 : $i, X39 : $i, X40 : $i, X41 : $i,
% 129.50/19.15 X42 : $i, X43 : $i, X44 : $i, X45 : $i, X46 : $i, X47 : $i, X48 : $i,
% 129.50/19.15 X49 : $i, X50 : $i, X51 : $i, X52 : $i, X53 : $i]:
% 129.50/19.15 (~ (state @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @
% 129.50/19.15 X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @
% 129.50/19.15 X22 @ X23 @ X24 @ X25 @ X26 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @
% 129.50/19.15 X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X39 @ X40 @ X41 @ X42 @ X43 @
% 129.50/19.15 X44 @ X45 @ X46 @ X47 @ X48 @ X49 @ X50 @ X51 @ X52 @ X53)
% 129.50/19.15 | (state @ X0 @ X1 @ X2 @ X16 @ X28 @ X40 @ X6 @ X7 @ X8 @ X9 @
% 129.50/19.15 X5 @ X11 @ X12 @ X13 @ X14 @ X15 @ X50 @ X17 @ X18 @ X19 @ X20 @
% 129.50/19.15 X21 @ X4 @ X23 @ X24 @ X25 @ X26 @ X27 @ X49 @ X29 @ X30 @ X31 @
% 129.50/19.15 X32 @ X33 @ X3 @ X35 @ X36 @ X37 @ X38 @ X39 @ X48 @ X41 @ X42 @
% 129.50/19.15 X43 @ X44 @ X45 @ X46 @ X47 @ X10 @ X22 @ X34 @ X51 @ X52 @ X53))),
% 129.50/19.15 inference('cnf', [status(esa)], [mzy])).
% 129.50/19.15 thf(zip_derived_cl1320, plain,
% 129.50/19.15 ( (state @ y @ b @ b @ y @ b @ b @ y @ b @ b @ r @ r @ r @ b @ g @ g @
% 129.50/19.15 o @ o @ o @ y @ y @ w @ r @ r @ r @ b @ g @ g @ o @ o @ o @ y @ y @
% 129.50/19.15 w @ b @ g @ g @ o @ o @ o @ y @ y @ w @ r @ r @ r @ w @ w @ w @ w @
% 129.50/19.15 w @ w @ g @ g @ g)),
% 129.50/19.15 inference('s_sup-', [status(thm)], [zip_derived_cl94, zip_derived_cl6])).
% 129.50/19.15 thf(byx, axiom,
% 129.50/19.15 (( ~( state @
% 129.50/19.15 A1 @ A2 @ A3 @ A4 @ A5 @ A6 @ A7 @ A8 @ A9 @ B1 @ B2 @ B3 @ B4 @
% 129.50/19.15 B5 @ B6 @ B7 @ B8 @ B9 @ C1 @ C2 @ C3 @ C4 @ C5 @ C6 @ C7 @ C8 @
% 129.50/19.15 C9 @ D1 @ D2 @ D3 @ D4 @ D5 @ D6 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @
% 129.50/19.15 X7 @ X8 @ X9 @ Y1 @ Y2 @ Y3 @ W1 @ W2 @ W3 @ W8 @ D7 @ W4 @ W7 @
% 129.50/19.15 W6 @ W5 ) ) |
% 129.50/19.15 ( state @
% 129.50/19.15 A1 @ A2 @ A3 @ A4 @ A5 @ A6 @ A7 @ A8 @ A9 @ B1 @ B2 @ B3 @ B4 @ B5 @
% 129.50/19.15 B6 @ B7 @ B8 @ B9 @ C1 @ C2 @ C3 @ C4 @ C5 @ C6 @ C7 @ C8 @ C9 @ D1 @
% 129.50/19.15 D2 @ D3 @ D4 @ D5 @ D6 @ Y1 @ Y2 @ Y3 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @
% 129.50/19.15 X7 @ X8 @ X9 @ W7 @ W8 @ W1 @ W6 @ D7 @ W2 @ W5 @ W4 @ W3 ))).
% 129.50/19.15 thf(zip_derived_cl13, plain,
% 129.50/19.15 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i,
% 129.50/19.15 X7 : $i, X8 : $i, X9 : $i, X10 : $i, X11 : $i, X12 : $i, X13 : $i,
% 129.50/19.15 X14 : $i, X15 : $i, X16 : $i, X17 : $i, X18 : $i, X19 : $i, X20 : $i,
% 129.50/19.15 X21 : $i, X22 : $i, X23 : $i, X24 : $i, X25 : $i, X26 : $i, X27 : $i,
% 129.50/19.15 X28 : $i, X29 : $i, X30 : $i, X31 : $i, X32 : $i, X33 : $i, X34 : $i,
% 129.50/19.15 X35 : $i, X36 : $i, X37 : $i, X38 : $i, X39 : $i, X40 : $i, X41 : $i,
% 129.50/19.15 X42 : $i, X43 : $i, X44 : $i, X45 : $i, X46 : $i, X47 : $i, X48 : $i,
% 129.50/19.15 X49 : $i, X50 : $i, X51 : $i, X52 : $i, X53 : $i]:
% 129.50/19.15 (~ (state @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @
% 129.50/19.15 X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @
% 129.50/19.15 X22 @ X23 @ X24 @ X25 @ X26 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @
% 129.50/19.15 X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X39 @ X40 @ X41 @ X42 @ X43 @
% 129.50/19.15 X44 @ X45 @ X46 @ X47 @ X48 @ X49 @ X50 @ X51 @ X52 @ X53)
% 129.50/19.15 | (state @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @
% 129.50/19.15 X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @
% 129.50/19.15 X21 @ X22 @ X23 @ X24 @ X25 @ X26 @ X27 @ X28 @ X29 @ X30 @
% 129.50/19.15 X31 @ X32 @ X42 @ X43 @ X44 @ X33 @ X34 @ X35 @ X36 @ X37 @
% 129.50/19.15 X38 @ X39 @ X40 @ X41 @ X51 @ X48 @ X45 @ X52 @ X49 @ X46 @
% 129.50/19.15 X53 @ X50 @ X47))),
% 129.50/19.15 inference('cnf', [status(esa)], [byx])).
% 129.50/19.15 thf(zip_derived_cl21739, plain,
% 129.50/19.15 ( (state @ y @ b @ b @ y @ b @ b @ y @ b @ b @ r @ r @ r @ b @ g @ g @
% 129.50/19.15 o @ o @ o @ y @ y @ w @ r @ r @ r @ b @ g @ g @ o @ o @ o @ y @ y @
% 129.50/19.15 w @ r @ r @ r @ b @ g @ g @ o @ o @ o @ y @ y @ w @ g @ w @ w @ g @
% 129.50/19.15 w @ w @ g @ w @ w)),
% 129.50/19.15 inference('s_sup-', [status(thm)], [zip_derived_cl1320, zip_derived_cl13])).
% 129.50/19.15 thf(lzx, axiom,
% 129.50/19.15 (( ~( state @
% 129.50/19.15 Y1 @ A1 @ A2 @ Y2 @ A3 @ A4 @ Y3 @ A5 @ A6 @ W7 @ W8 @ W1 @ X1 @
% 129.50/19.15 A7 @ A8 @ A9 @ B1 @ B2 @ B3 @ B4 @ X9 @ W6 @ B5 @ W2 @ X2 @ B6 @
% 129.50/19.15 B7 @ B8 @ B9 @ C1 @ C2 @ C3 @ X8 @ W5 @ W4 @ W3 @ X3 @ C4 @ C5 @
% 129.50/19.15 C6 @ C7 @ C8 @ C9 @ D1 @ X7 @ X4 @ D2 @ D3 @ X5 @ D4 @ D5 @ X6 @
% 129.50/19.15 D6 @ D7 ) ) |
% 129.50/19.15 ( state @
% 129.50/19.15 X1 @ A1 @ A2 @ X2 @ A3 @ A4 @ X3 @ A5 @ A6 @ W1 @ W2 @ W3 @ X4 @ A7 @
% 129.50/19.15 A8 @ A9 @ B1 @ B2 @ B3 @ B4 @ Y3 @ W8 @ B5 @ W4 @ X5 @ B6 @ B7 @ B8 @
% 129.50/19.15 B9 @ C1 @ C2 @ C3 @ Y2 @ W7 @ W6 @ W5 @ X6 @ C4 @ C5 @ C6 @ C7 @ C8 @
% 129.50/19.15 C9 @ D1 @ Y1 @ X7 @ D2 @ D3 @ X8 @ D4 @ D5 @ X9 @ D6 @ D7 ))).
% 129.50/19.15 thf(zip_derived_cl8, plain,
% 129.50/19.15 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i, X4 : $i, X5 : $i, X6 : $i,
% 129.50/19.15 X7 : $i, X8 : $i, X9 : $i, X10 : $i, X11 : $i, X12 : $i, X13 : $i,
% 129.50/19.15 X14 : $i, X15 : $i, X16 : $i, X17 : $i, X18 : $i, X19 : $i, X20 : $i,
% 129.50/19.15 X21 : $i, X22 : $i, X23 : $i, X24 : $i, X25 : $i, X26 : $i, X27 : $i,
% 129.50/19.15 X28 : $i, X29 : $i, X30 : $i, X31 : $i, X32 : $i, X33 : $i, X34 : $i,
% 129.50/19.15 X35 : $i, X36 : $i, X37 : $i, X38 : $i, X39 : $i, X40 : $i, X41 : $i,
% 129.50/19.15 X42 : $i, X43 : $i, X44 : $i, X45 : $i, X46 : $i, X47 : $i, X48 : $i,
% 129.50/19.15 X49 : $i, X50 : $i, X51 : $i, X52 : $i, X53 : $i]:
% 129.50/19.15 (~ (state @ X0 @ X1 @ X2 @ X3 @ X4 @ X5 @ X6 @ X7 @ X8 @ X9 @ X10 @
% 129.50/19.15 X11 @ X12 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X20 @ X21 @
% 129.50/19.15 X22 @ X23 @ X24 @ X25 @ X26 @ X27 @ X28 @ X29 @ X30 @ X31 @ X32 @
% 129.50/19.15 X33 @ X34 @ X35 @ X36 @ X37 @ X38 @ X39 @ X40 @ X41 @ X42 @ X43 @
% 129.50/19.15 X44 @ X45 @ X46 @ X47 @ X48 @ X49 @ X50 @ X51 @ X52 @ X53)
% 129.50/19.15 | (state @ X12 @ X1 @ X2 @ X24 @ X4 @ X5 @ X36 @ X7 @ X8 @ X11 @
% 129.50/19.15 X23 @ X35 @ X45 @ X13 @ X14 @ X15 @ X16 @ X17 @ X18 @ X19 @ X6 @
% 129.50/19.15 X10 @ X22 @ X34 @ X48 @ X25 @ X26 @ X27 @ X28 @ X29 @ X30 @
% 129.50/19.15 X31 @ X3 @ X9 @ X21 @ X33 @ X51 @ X37 @ X38 @ X39 @ X40 @ X41 @
% 129.50/19.15 X42 @ X43 @ X0 @ X44 @ X46 @ X47 @ X32 @ X49 @ X50 @ X20 @ X52 @
% 129.50/19.15 X53))),
% 129.50/19.15 inference('cnf', [status(esa)], [lzx])).
% 129.50/19.15 thf(zip_derived_cl21770, plain,
% 129.50/19.15 ( (state @ b @ b @ b @ b @ b @ b @ b @ b @ b @ r @ r @ r @ g @ g @ g @
% 129.50/19.15 o @ o @ o @ y @ y @ y @ r @ r @ r @ g @ g @ g @ o @ o @ o @ y @ y @
% 129.50/19.15 y @ r @ r @ r @ g @ g @ g @ o @ o @ o @ y @ y @ y @ w @ w @ w @ w @
% 129.50/19.15 w @ w @ w @ w @ w)),
% 129.50/19.15 inference('s_sup-', [status(thm)], [zip_derived_cl21739, zip_derived_cl8])).
% 129.50/19.15 thf(zip_derived_cl21782, plain, ($false),
% 129.50/19.15 inference('demod', [status(thm)], [zip_derived_cl0, zip_derived_cl21770])).
% 129.50/19.15
% 129.50/19.15 % SZS output end Refutation
% 129.50/19.15
% 129.50/19.15
% 129.50/19.15 % Terminating...
% 130.14/19.26 % Runner terminated.
% 130.14/19.27 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------