%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : PUZ005-1 : TPTP v9.2.0. Released v1.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.KL28k1zTwR true
% Computer : n029.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:27 PM UTC 2025
% Result : Unsatisfiable 1.25s 0.74s
% Output : Refutation 1.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : PUZ005-1 : TPTP v9.2.0. Released v1.0.0.
% 0.00/0.11 % Command : python3 /export/starexec/sandbox2/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox2/tmp/tmp.KL28k1zTwR true
% 0.11/0.31 % Computer : n029.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Wed Oct 1 15:10:23 EDT 2025
% 0.11/0.31 % CPUTime :
% 0.11/0.31 % Running portfolio for 300 s
% 0.11/0.31 % File : /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.31 % Number of cores: 8
% 0.16/0.31 % Python version: Python 3.6.8
% 0.16/0.32 % Running in FO mode
% 0.17/0.57 % Total configuration time : 435
% 0.17/0.57 % Estimated wc time : 1092
% 0.17/0.57 % Estimated cpu time (7 cpus) : 156.0
% 0.97/0.65 % /export/starexec/sandbox2/solver/bin/fo/fo6_bce.sh running for 75s
% 0.97/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo3_bce.sh running for 75s
% 0.97/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo1_av.sh running for 75s
% 0.97/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo7.sh running for 63s
% 0.97/0.67 % /export/starexec/sandbox2/solver/bin/fo/fo13.sh running for 50s
% 0.97/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo4.sh running for 50s
% 0.97/0.68 % /export/starexec/sandbox2/solver/bin/fo/fo5.sh running for 50s
% 1.25/0.71 % /export/starexec/sandbox2/solver/bin/fo/fo1_lcnf.sh running for 50s
% 1.25/0.74 % Solved by fo/fo6_bce.sh.
% 1.25/0.74 % BCE start: 51
% 1.25/0.74 % BCE eliminated: 0
% 1.25/0.74 % PE start: 51
% 1.25/0.74 logic: neq
% 1.25/0.74 % PE eliminated: 2
% 1.25/0.74 % done 114 iterations in 0.067s
% 1.25/0.74 % SZS status Theorem for '/export/starexec/sandbox2/benchmark/theBenchmark.p'
% 1.25/0.74 % SZS output start Refutation
% 1.25/0.74 thf(thursday_type, type, thursday: $i > $o).
% 1.25/0.74 thf(friday_type, type, friday: $i > $o).
% 1.25/0.74 thf(admits_type, type, admits: $i > $i > $i > $o).
% 1.25/0.74 thf(member_type, type, member: $i > $i > $o).
% 1.25/0.74 thf(today_type, type, today: $i).
% 1.25/0.74 thf(monday_type, type, monday: $i > $o).
% 1.25/0.74 thf(lion_type, type, lion: $i).
% 1.25/0.74 thf(saturday_type, type, saturday: $i > $o).
% 1.25/0.74 thf(tuesday_type, type, tuesday: $i > $o).
% 1.25/0.74 thf(unicorn_type, type, unicorn: $i).
% 1.25/0.74 thf(yesterday_type, type, yesterday: $i > $i).
% 1.25/0.74 thf(sunday_type, type, sunday: $i > $o).
% 1.25/0.74 thf(wednesday_type, type, wednesday: $i > $o).
% 1.25/0.74 thf(lying_days_type, type, lying_days: $i > $i).
% 1.25/0.74 thf(admissions6, axiom, (admits @ unicorn @ today @ ( yesterday @ today ))).
% 1.25/0.74 thf(zip_derived_cl49, plain,
% 1.25/0.74 ( (admits @ unicorn @ today @ (yesterday @ today))),
% 1.25/0.74 inference('cnf', [status(esa)], [admissions6])).
% 1.25/0.74 thf(admissions1, axiom,
% 1.25/0.74 (( member @ X @ ( lying_days @ T ) ) | ( ~( admits @ T @ X @ Y ) ) |
% 1.25/0.74 ( member @ Y @ ( lying_days @ T ) ))).
% 1.25/0.74 thf(zip_derived_cl44, plain,
% 1.25/0.74 (![X0 : $i, X1 : $i, X2 : $i]:
% 1.25/0.74 ( (member @ X0 @ (lying_days @ X1))
% 1.25/0.74 | ~ (admits @ X1 @ X0 @ X2)
% 1.25/0.74 | (member @ X2 @ (lying_days @ X1)))),
% 1.25/0.74 inference('cnf', [status(esa)], [admissions1])).
% 1.25/0.74 thf(zip_derived_cl63, plain,
% 1.25/0.74 (( (member @ (yesterday @ today) @ (lying_days @ unicorn))
% 1.25/0.74 | (member @ today @ (lying_days @ unicorn)))),
% 1.25/0.74 inference('dp-resolution', [status(thm)],
% 1.25/0.74 [zip_derived_cl49, zip_derived_cl44])).
% 1.25/0.74 thf(unicorns_lying_days, axiom,
% 1.25/0.74 (( ~( member @ X @ ( lying_days @ unicorn ) ) ) | ( thursday @ X ) |
% 1.25/0.74 ( friday @ X ) | ( saturday @ X ))).
% 1.25/0.74 thf(zip_derived_cl37, plain,
% 1.25/0.74 (![X0 : $i]:
% 1.25/0.74 (~ (member @ X0 @ (lying_days @ unicorn))
% 1.25/0.74 | (thursday @ X0)
% 1.25/0.74 | (friday @ X0)
% 1.25/0.74 | (saturday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [unicorns_lying_days])).
% 1.25/0.74 thf(zip_derived_cl367, plain,
% 1.25/0.74 (( (member @ today @ (lying_days @ unicorn))
% 1.25/0.74 | (thursday @ (yesterday @ today))
% 1.25/0.74 | (friday @ (yesterday @ today))
% 1.25/0.74 | (saturday @ (yesterday @ today)))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl63, zip_derived_cl37])).
% 1.25/0.74 thf(thursday_yesterday, axiom,
% 1.25/0.74 (( ~( thursday @ ( yesterday @ X ) ) ) | ( friday @ X ))).
% 1.25/0.74 thf(zip_derived_cl25, plain,
% 1.25/0.74 (![X0 : $i]: (~ (thursday @ (yesterday @ X0)) | (friday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [thursday_yesterday])).
% 1.25/0.74 thf(unicorn_lies_on_friday, axiom,
% 1.25/0.74 (( ~( friday @ X ) ) | ( member @ X @ ( lying_days @ unicorn ) ))).
% 1.25/0.74 thf(zip_derived_cl42, plain,
% 1.25/0.74 (![X0 : $i]: (~ (friday @ X0) | (member @ X0 @ (lying_days @ unicorn)))),
% 1.25/0.74 inference('cnf', [status(esa)], [unicorn_lies_on_friday])).
% 1.25/0.74 thf(zip_derived_cl49, plain,
% 1.25/0.74 ( (admits @ unicorn @ today @ (yesterday @ today))),
% 1.25/0.74 inference('cnf', [status(esa)], [admissions6])).
% 1.25/0.74 thf(admissions3, axiom,
% 1.25/0.74 (( ~( member @ X @ ( lying_days @ T ) ) ) | ( ~( admits @ T @ X @ Y ) ) |
% 1.25/0.74 ( ~( member @ Y @ ( lying_days @ T ) ) ))).
% 1.25/0.74 thf(zip_derived_cl46, plain,
% 1.25/0.74 (![X0 : $i, X1 : $i, X2 : $i]:
% 1.25/0.74 (~ (member @ X0 @ (lying_days @ X1))
% 1.25/0.74 | ~ (admits @ X1 @ X0 @ X2)
% 1.25/0.74 | ~ (member @ X2 @ (lying_days @ X1)))),
% 1.25/0.74 inference('cnf', [status(esa)], [admissions3])).
% 1.25/0.74 thf(zip_derived_cl64, plain,
% 1.25/0.74 ((~ (member @ (yesterday @ today) @ (lying_days @ unicorn))
% 1.25/0.74 | ~ (member @ today @ (lying_days @ unicorn)))),
% 1.25/0.74 inference('dp-resolution', [status(thm)],
% 1.25/0.74 [zip_derived_cl49, zip_derived_cl46])).
% 1.25/0.74 thf(zip_derived_cl377, plain,
% 1.25/0.74 ((~ (friday @ today)
% 1.25/0.74 | ~ (member @ (yesterday @ today) @ (lying_days @ unicorn)))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl42, zip_derived_cl64])).
% 1.25/0.74 thf(zip_derived_cl381, plain,
% 1.25/0.74 ((~ (thursday @ (yesterday @ today))
% 1.25/0.74 | ~ (member @ (yesterday @ today) @ (lying_days @ unicorn)))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl25, zip_derived_cl377])).
% 1.25/0.74 thf(unicorn_lies_on_thursday, axiom,
% 1.25/0.74 (( ~( thursday @ X ) ) | ( member @ X @ ( lying_days @ unicorn ) ))).
% 1.25/0.74 thf(zip_derived_cl41, plain,
% 1.25/0.74 (![X0 : $i]:
% 1.25/0.74 (~ (thursday @ X0) | (member @ X0 @ (lying_days @ unicorn)))),
% 1.25/0.74 inference('cnf', [status(esa)], [unicorn_lies_on_thursday])).
% 1.25/0.74 thf(zip_derived_cl382, plain, (~ (thursday @ (yesterday @ today))),
% 1.25/0.74 inference('clc', [status(thm)], [zip_derived_cl381, zip_derived_cl41])).
% 1.25/0.74 thf(zip_derived_cl442, plain,
% 1.25/0.74 (( (member @ today @ (lying_days @ unicorn))
% 1.25/0.74 | (friday @ (yesterday @ today))
% 1.25/0.74 | (saturday @ (yesterday @ today)))),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl367, zip_derived_cl382])).
% 1.25/0.74 thf(saturday_yesterday, axiom,
% 1.25/0.74 (( ~( saturday @ ( yesterday @ X ) ) ) | ( sunday @ X ))).
% 1.25/0.74 thf(zip_derived_cl27, plain,
% 1.25/0.74 (![X0 : $i]: (~ (saturday @ (yesterday @ X0)) | (sunday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [saturday_yesterday])).
% 1.25/0.74 thf(monday_not_sunday, axiom, (( ~( monday @ X ) ) | ( ~( sunday @ X ) ))).
% 1.25/0.74 thf(zip_derived_cl6, plain,
% 1.25/0.74 (![X0 : $i]: (~ (monday @ X0) | ~ (sunday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [monday_not_sunday])).
% 1.25/0.74 thf(zip_derived_cl332, plain,
% 1.25/0.74 (![X0 : $i]: (~ (saturday @ (yesterday @ X0)) | ~ (monday @ X0))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl27, zip_derived_cl6])).
% 1.25/0.74 thf(zip_derived_cl448, plain,
% 1.25/0.74 (( (friday @ (yesterday @ today))
% 1.25/0.74 | (member @ today @ (lying_days @ unicorn))
% 1.25/0.74 | ~ (monday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl442, zip_derived_cl332])).
% 1.25/0.74 thf(admissions5, axiom, (admits @ lion @ today @ ( yesterday @ today ))).
% 1.25/0.74 thf(zip_derived_cl48, plain,
% 1.25/0.74 ( (admits @ lion @ today @ (yesterday @ today))),
% 1.25/0.74 inference('cnf', [status(esa)], [admissions5])).
% 1.25/0.74 thf(zip_derived_cl44, plain,
% 1.25/0.74 (![X0 : $i, X1 : $i, X2 : $i]:
% 1.25/0.74 ( (member @ X0 @ (lying_days @ X1))
% 1.25/0.74 | ~ (admits @ X1 @ X0 @ X2)
% 1.25/0.74 | (member @ X2 @ (lying_days @ X1)))),
% 1.25/0.74 inference('cnf', [status(esa)], [admissions1])).
% 1.25/0.74 thf(zip_derived_cl61, plain,
% 1.25/0.74 (( (member @ (yesterday @ today) @ (lying_days @ lion))
% 1.25/0.74 | (member @ today @ (lying_days @ lion)))),
% 1.25/0.74 inference('dp-resolution', [status(thm)],
% 1.25/0.74 [zip_derived_cl48, zip_derived_cl44])).
% 1.25/0.74 thf(lions_lying_days, axiom,
% 1.25/0.74 (( ~( member @ X @ ( lying_days @ lion ) ) ) | ( monday @ X ) |
% 1.25/0.74 ( tuesday @ X ) | ( wednesday @ X ))).
% 1.25/0.74 thf(zip_derived_cl36, plain,
% 1.25/0.74 (![X0 : $i]:
% 1.25/0.74 (~ (member @ X0 @ (lying_days @ lion))
% 1.25/0.74 | (monday @ X0)
% 1.25/0.74 | (tuesday @ X0)
% 1.25/0.74 | (wednesday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [lions_lying_days])).
% 1.25/0.74 thf(zip_derived_cl363, plain,
% 1.25/0.74 (( (member @ today @ (lying_days @ lion))
% 1.25/0.74 | (monday @ (yesterday @ today))
% 1.25/0.74 | (tuesday @ (yesterday @ today))
% 1.25/0.74 | (wednesday @ (yesterday @ today)))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl61, zip_derived_cl36])).
% 1.25/0.74 thf(wednesday_yesterday, axiom,
% 1.25/0.74 (( ~( wednesday @ ( yesterday @ X ) ) ) | ( thursday @ X ))).
% 1.25/0.74 thf(zip_derived_cl24, plain,
% 1.25/0.74 (![X0 : $i]: (~ (wednesday @ (yesterday @ X0)) | (thursday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [wednesday_yesterday])).
% 1.25/0.74 thf(zip_derived_cl399, plain,
% 1.25/0.74 (( (tuesday @ (yesterday @ today))
% 1.25/0.74 | (monday @ (yesterday @ today))
% 1.25/0.74 | (member @ today @ (lying_days @ lion))
% 1.25/0.74 | (thursday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl363, zip_derived_cl24])).
% 1.25/0.74 thf(prove_today_is_thursday, conjecture, (thursday @ today)).
% 1.25/0.74 thf(zf_stmt_0, negated_conjecture, (~( thursday @ today )),
% 1.25/0.74 inference('cnf.neg', [status(esa)], [prove_today_is_thursday])).
% 1.25/0.74 thf(zip_derived_cl50, plain, (~ (thursday @ today)),
% 1.25/0.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 1.25/0.74 thf(zip_derived_cl402, plain,
% 1.25/0.74 (( (tuesday @ (yesterday @ today))
% 1.25/0.74 | (monday @ (yesterday @ today))
% 1.25/0.74 | (member @ today @ (lying_days @ lion)))),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl399, zip_derived_cl50])).
% 1.25/0.74 thf(tuesday_yesterday, axiom,
% 1.25/0.74 (( ~( tuesday @ ( yesterday @ X ) ) ) | ( wednesday @ X ))).
% 1.25/0.74 thf(zip_derived_cl23, plain,
% 1.25/0.74 (![X0 : $i]: (~ (tuesday @ (yesterday @ X0)) | (wednesday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [tuesday_yesterday])).
% 1.25/0.74 thf(zip_derived_cl405, plain,
% 1.25/0.74 (( (member @ today @ (lying_days @ lion))
% 1.25/0.74 | (monday @ (yesterday @ today))
% 1.25/0.74 | (wednesday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl402, zip_derived_cl23])).
% 1.25/0.74 thf(lion_lies_on_wednesday, axiom,
% 1.25/0.74 (( ~( wednesday @ X ) ) | ( member @ X @ ( lying_days @ lion ) ))).
% 1.25/0.74 thf(zip_derived_cl40, plain,
% 1.25/0.74 (![X0 : $i]: (~ (wednesday @ X0) | (member @ X0 @ (lying_days @ lion)))),
% 1.25/0.74 inference('cnf', [status(esa)], [lion_lies_on_wednesday])).
% 1.25/0.74 thf(zip_derived_cl413, plain,
% 1.25/0.74 (( (monday @ (yesterday @ today))
% 1.25/0.74 | (member @ today @ (lying_days @ lion)))),
% 1.25/0.74 inference('clc', [status(thm)], [zip_derived_cl405, zip_derived_cl40])).
% 1.25/0.74 thf(monday_yesterday, axiom,
% 1.25/0.74 (( ~( monday @ ( yesterday @ X ) ) ) | ( tuesday @ X ))).
% 1.25/0.74 thf(zip_derived_cl22, plain,
% 1.25/0.74 (![X0 : $i]: (~ (monday @ (yesterday @ X0)) | (tuesday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [monday_yesterday])).
% 1.25/0.74 thf(zip_derived_cl415, plain,
% 1.25/0.74 (( (member @ today @ (lying_days @ lion)) | (tuesday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl413, zip_derived_cl22])).
% 1.25/0.74 thf(lion_lies_on_tuesday, axiom,
% 1.25/0.74 (( ~( tuesday @ X ) ) | ( member @ X @ ( lying_days @ lion ) ))).
% 1.25/0.74 thf(zip_derived_cl39, plain,
% 1.25/0.74 (![X0 : $i]: (~ (tuesday @ X0) | (member @ X0 @ (lying_days @ lion)))),
% 1.25/0.74 inference('cnf', [status(esa)], [lion_lies_on_tuesday])).
% 1.25/0.74 thf(zip_derived_cl423, plain, ( (member @ today @ (lying_days @ lion))),
% 1.25/0.74 inference('clc', [status(thm)], [zip_derived_cl415, zip_derived_cl39])).
% 1.25/0.74 thf(zip_derived_cl36, plain,
% 1.25/0.74 (![X0 : $i]:
% 1.25/0.74 (~ (member @ X0 @ (lying_days @ lion))
% 1.25/0.74 | (monday @ X0)
% 1.25/0.74 | (tuesday @ X0)
% 1.25/0.74 | (wednesday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [lions_lying_days])).
% 1.25/0.74 thf(zip_derived_cl425, plain,
% 1.25/0.74 (( (monday @ today) | (tuesday @ today) | (wednesday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl423, zip_derived_cl36])).
% 1.25/0.74 thf(yesterday_monday, axiom,
% 1.25/0.74 (( monday @ ( yesterday @ X ) ) | ( ~( tuesday @ X ) ))).
% 1.25/0.74 thf(zip_derived_cl29, plain,
% 1.25/0.74 (![X0 : $i]: ( (monday @ (yesterday @ X0)) | ~ (tuesday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [yesterday_monday])).
% 1.25/0.74 thf(lion_lies_on_monday, axiom,
% 1.25/0.74 (( ~( monday @ X ) ) | ( member @ X @ ( lying_days @ lion ) ))).
% 1.25/0.74 thf(zip_derived_cl38, plain,
% 1.25/0.74 (![X0 : $i]: (~ (monday @ X0) | (member @ X0 @ (lying_days @ lion)))),
% 1.25/0.74 inference('cnf', [status(esa)], [lion_lies_on_monday])).
% 1.25/0.74 thf(zip_derived_cl48, plain,
% 1.25/0.74 ( (admits @ lion @ today @ (yesterday @ today))),
% 1.25/0.74 inference('cnf', [status(esa)], [admissions5])).
% 1.25/0.74 thf(zip_derived_cl46, plain,
% 1.25/0.74 (![X0 : $i, X1 : $i, X2 : $i]:
% 1.25/0.74 (~ (member @ X0 @ (lying_days @ X1))
% 1.25/0.74 | ~ (admits @ X1 @ X0 @ X2)
% 1.25/0.74 | ~ (member @ X2 @ (lying_days @ X1)))),
% 1.25/0.74 inference('cnf', [status(esa)], [admissions3])).
% 1.25/0.74 thf(zip_derived_cl62, plain,
% 1.25/0.74 ((~ (member @ (yesterday @ today) @ (lying_days @ lion))
% 1.25/0.74 | ~ (member @ today @ (lying_days @ lion)))),
% 1.25/0.74 inference('dp-resolution', [status(thm)],
% 1.25/0.74 [zip_derived_cl48, zip_derived_cl46])).
% 1.25/0.74 thf(zip_derived_cl423, plain, ( (member @ today @ (lying_days @ lion))),
% 1.25/0.74 inference('clc', [status(thm)], [zip_derived_cl415, zip_derived_cl39])).
% 1.25/0.74 thf(zip_derived_cl424, plain,
% 1.25/0.74 (~ (member @ (yesterday @ today) @ (lying_days @ lion))),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl62, zip_derived_cl423])).
% 1.25/0.74 thf(zip_derived_cl426, plain, (~ (monday @ (yesterday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl38, zip_derived_cl424])).
% 1.25/0.74 thf(zip_derived_cl429, plain, (~ (tuesday @ today)),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl29, zip_derived_cl426])).
% 1.25/0.74 thf(zip_derived_cl430, plain, (( (monday @ today) | (wednesday @ today))),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl425, zip_derived_cl429])).
% 1.25/0.74 thf(yesterday_tuesday, axiom,
% 1.25/0.74 (( tuesday @ ( yesterday @ X ) ) | ( ~( wednesday @ X ) ))).
% 1.25/0.74 thf(zip_derived_cl30, plain,
% 1.25/0.74 (![X0 : $i]: ( (tuesday @ (yesterday @ X0)) | ~ (wednesday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [yesterday_tuesday])).
% 1.25/0.74 thf(zip_derived_cl39, plain,
% 1.25/0.74 (![X0 : $i]: (~ (tuesday @ X0) | (member @ X0 @ (lying_days @ lion)))),
% 1.25/0.74 inference('cnf', [status(esa)], [lion_lies_on_tuesday])).
% 1.25/0.74 thf(zip_derived_cl424, plain,
% 1.25/0.74 (~ (member @ (yesterday @ today) @ (lying_days @ lion))),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl62, zip_derived_cl423])).
% 1.25/0.74 thf(zip_derived_cl427, plain, (~ (tuesday @ (yesterday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl39, zip_derived_cl424])).
% 1.25/0.74 thf(zip_derived_cl435, plain, (~ (wednesday @ today)),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl30, zip_derived_cl427])).
% 1.25/0.74 thf(zip_derived_cl438, plain, ( (monday @ today)),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl430, zip_derived_cl435])).
% 1.25/0.74 thf(zip_derived_cl458, plain,
% 1.25/0.74 (( (friday @ (yesterday @ today))
% 1.25/0.74 | (member @ today @ (lying_days @ unicorn)))),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl448, zip_derived_cl438])).
% 1.25/0.74 thf(yesterday_sunday, axiom,
% 1.25/0.74 (( sunday @ ( yesterday @ X ) ) | ( ~( monday @ X ) ))).
% 1.25/0.74 thf(zip_derived_cl35, plain,
% 1.25/0.74 (![X0 : $i]: ( (sunday @ (yesterday @ X0)) | ~ (monday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [yesterday_sunday])).
% 1.25/0.74 thf(friday_not_sunday, axiom, (( ~( friday @ X ) ) | ( ~( sunday @ X ) ))).
% 1.25/0.74 thf(zip_derived_cl20, plain,
% 1.25/0.74 (![X0 : $i]: (~ (friday @ X0) | ~ (sunday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [friday_not_sunday])).
% 1.25/0.74 thf(zip_derived_cl354, plain,
% 1.25/0.74 (![X0 : $i]: (~ (monday @ X0) | ~ (friday @ (yesterday @ X0)))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl35, zip_derived_cl20])).
% 1.25/0.74 thf(zip_derived_cl468, plain,
% 1.25/0.74 (( (member @ today @ (lying_days @ unicorn)) | ~ (monday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl458, zip_derived_cl354])).
% 1.25/0.74 thf(zip_derived_cl438, plain, ( (monday @ today)),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl430, zip_derived_cl435])).
% 1.25/0.74 thf(zip_derived_cl470, plain, ( (member @ today @ (lying_days @ unicorn))),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl468, zip_derived_cl438])).
% 1.25/0.74 thf(zip_derived_cl37, plain,
% 1.25/0.74 (![X0 : $i]:
% 1.25/0.74 (~ (member @ X0 @ (lying_days @ unicorn))
% 1.25/0.74 | (thursday @ X0)
% 1.25/0.74 | (friday @ X0)
% 1.25/0.74 | (saturday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [unicorns_lying_days])).
% 1.25/0.74 thf(zip_derived_cl472, plain,
% 1.25/0.74 (( (thursday @ today) | (friday @ today) | (saturday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl470, zip_derived_cl37])).
% 1.25/0.74 thf(zip_derived_cl50, plain, (~ (thursday @ today)),
% 1.25/0.74 inference('cnf', [status(esa)], [zf_stmt_0])).
% 1.25/0.74 thf(zip_derived_cl473, plain, (( (friday @ today) | (saturday @ today))),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl472, zip_derived_cl50])).
% 1.25/0.74 thf(monday_not_saturday, axiom,
% 1.25/0.74 (( ~( monday @ X ) ) | ( ~( saturday @ X ) ))).
% 1.25/0.74 thf(zip_derived_cl5, plain,
% 1.25/0.74 (![X0 : $i]: (~ (monday @ X0) | ~ (saturday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [monday_not_saturday])).
% 1.25/0.74 thf(zip_derived_cl474, plain, (( (friday @ today) | ~ (monday @ today))),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl473, zip_derived_cl5])).
% 1.25/0.74 thf(zip_derived_cl438, plain, ( (monday @ today)),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl430, zip_derived_cl435])).
% 1.25/0.74 thf(zip_derived_cl480, plain, ( (friday @ today)),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl474, zip_derived_cl438])).
% 1.25/0.74 thf(monday_not_friday, axiom, (( ~( monday @ X ) ) | ( ~( friday @ X ) ))).
% 1.25/0.74 thf(zip_derived_cl4, plain,
% 1.25/0.74 (![X0 : $i]: (~ (monday @ X0) | ~ (friday @ X0))),
% 1.25/0.74 inference('cnf', [status(esa)], [monday_not_friday])).
% 1.25/0.74 thf(zip_derived_cl485, plain, (~ (monday @ today)),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl480, zip_derived_cl4])).
% 1.25/0.74 thf(zip_derived_cl438, plain, ( (monday @ today)),
% 1.25/0.74 inference('s_sup-', [status(thm)], [zip_derived_cl430, zip_derived_cl435])).
% 1.25/0.74 thf(zip_derived_cl490, plain, ($false),
% 1.25/0.74 inference('demod', [status(thm)], [zip_derived_cl485, zip_derived_cl438])).
% 1.25/0.74
% 1.25/0.74 % SZS output end Refutation
% 1.25/0.74
% 1.25/0.74
% 1.25/0.74 % Terminating...
% 1.57/0.79 % Runner terminated.
% 1.57/0.81 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------