%------------------------------------------------------------------------------
% File : Zipperpin---2.1.9999
% Problem : NLP001-1 : TPTP v9.2.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.qYS6eao9aA true
% Computer : n009.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:44:57 PM UTC 2025
% Result : Unsatisfiable 0.54s 0.75s
% Output : Refutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : NLP001-1 : TPTP v9.2.0. Released v2.4.0.
% 0.10/0.13 % Command : python3 /export/starexec/sandbox/solver/bin/portfolio.lams.parallel.py %s %d /export/starexec/sandbox/tmp/tmp.qYS6eao9aA true
% 0.13/0.34 % Computer : n009.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 1 11:41:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % Running portfolio for 300 s
% 0.13/0.34 % File : /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Number of cores: 8
% 0.13/0.34 % Python version: Python 3.6.8
% 0.13/0.35 % Running in FO mode
% 0.52/0.62 % Total configuration time : 435
% 0.52/0.62 % Estimated wc time : 1092
% 0.52/0.62 % Estimated cpu time (7 cpus) : 156.0
% 0.54/0.71 % /export/starexec/sandbox/solver/bin/fo/fo6_bce.sh running for 75s
% 0.54/0.72 % /export/starexec/sandbox/solver/bin/fo/fo3_bce.sh running for 75s
% 0.54/0.74 % /export/starexec/sandbox/solver/bin/fo/fo1_av.sh running for 75s
% 0.54/0.75 % Solved by fo/fo6_bce.sh.
% 0.54/0.75 % BCE start: 30
% 0.54/0.75 % BCE eliminated: 0
% 0.54/0.75 % PE start: 30
% 0.54/0.75 logic: neq
% 0.54/0.75 % PE eliminated: 28
% 0.54/0.75 % done 1 iterations in 0.021s
% 0.54/0.75 % SZS status Theorem for '/export/starexec/sandbox/benchmark/theBenchmark.p'
% 0.54/0.75 % SZS output start Refutation
% 0.54/0.75 thf(skc10_type, type, skc10: $i).
% 0.54/0.75 thf(barrel_type, type, barrel: $i > $i > $o).
% 0.54/0.75 thf(in_type, type, in: $i > $i > $o).
% 0.54/0.75 thf(skc15_type, type, skc15: $i).
% 0.54/0.75 thf(down_type, type, down: $i > $i > $o).
% 0.54/0.75 thf(white_type, type, white: $i > $o).
% 0.54/0.75 thf(way_type, type, way: $i > $o).
% 0.54/0.75 thf(skc8_type, type, skc8: $i).
% 0.54/0.75 thf(hollywood_type, type, hollywood: $i > $o).
% 0.54/0.75 thf(skc14_type, type, skc14: $i).
% 0.54/0.75 thf(skc11_type, type, skc11: $i).
% 0.54/0.75 thf(skc12_type, type, skc12: $i).
% 0.54/0.75 thf(event_type, type, event: $i > $o).
% 0.54/0.75 thf(city_type, type, city: $i > $o).
% 0.54/0.75 thf(skc9_type, type, skc9: $i).
% 0.54/0.75 thf(chevy_type, type, chevy: $i > $o).
% 0.54/0.75 thf(car_type, type, car: $i > $o).
% 0.54/0.75 thf(dirty_type, type, dirty: $i > $o).
% 0.54/0.75 thf(old_type, type, old: $i > $o).
% 0.54/0.75 thf(street_type, type, street: $i > $o).
% 0.54/0.75 thf(ssSkC0_type, type, ssSkC0: $o).
% 0.54/0.75 thf(skc13_type, type, skc13: $i).
% 0.54/0.75 thf(lonely_type, type, lonely: $i > $o).
% 0.54/0.75 thf(clause28, conjecture, (~( ( in @ skc10 @ skc11 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_0, negated_conjecture,
% 0.54/0.75 (( in @ skc10 @ skc11 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause28])).
% 0.54/0.75 thf(zip_derived_cl27, plain, (( (in @ skc10 @ skc11) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_0])).
% 0.54/0.75 thf(clause27, conjecture, (~( ( down @ skc10 @ skc8 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_1, negated_conjecture,
% 0.54/0.75 (( down @ skc10 @ skc8 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause27])).
% 0.54/0.75 thf(zip_derived_cl26, plain, (( (down @ skc10 @ skc8) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_1])).
% 0.54/0.75 thf(clause26, conjecture, (~( ( barrel @ skc10 @ skc9 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_2, negated_conjecture,
% 0.54/0.75 (( barrel @ skc10 @ skc9 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause26])).
% 0.54/0.75 thf(zip_derived_cl25, plain, (( (barrel @ skc10 @ skc9) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_2])).
% 0.54/0.75 thf(clause22, conjecture, (~( ( city @ skc11 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_3, negated_conjecture, (( city @ skc11 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause22])).
% 0.54/0.75 thf(zip_derived_cl21, plain, (( (city @ skc11) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_3])).
% 0.54/0.75 thf(clause17, conjecture, (~( ( way @ skc8 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_4, negated_conjecture, (( way @ skc8 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause17])).
% 0.54/0.75 thf(zip_derived_cl16, plain, (( (way @ skc8) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_4])).
% 0.54/0.75 thf(clause19, conjecture, (~( ( dirty @ skc9 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_5, negated_conjecture, (( dirty @ skc9 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause19])).
% 0.54/0.75 thf(zip_derived_cl18, plain, (( (dirty @ skc9) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_5])).
% 0.54/0.75 thf(clause20, conjecture, (~( ( white @ skc9 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_6, negated_conjecture, (( white @ skc9 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause20])).
% 0.54/0.75 thf(zip_derived_cl19, plain, (( (white @ skc9) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_6])).
% 0.54/0.75 thf(clause21, conjecture, (~( ( car @ skc9 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_7, negated_conjecture, (( car @ skc9 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause21])).
% 0.54/0.75 thf(zip_derived_cl20, plain, (( (car @ skc9) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_7])).
% 0.54/0.75 thf(clause8, conjecture, (~( lonely @ skc8 ))).
% 0.54/0.75 thf(zf_stmt_8, negated_conjecture, (lonely @ skc8),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause8])).
% 0.54/0.75 thf(zip_derived_cl7, plain, ( (lonely @ skc8)),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_8])).
% 0.54/0.75 thf(clause7, conjecture, (~( chevy @ skc9 ))).
% 0.54/0.75 thf(zf_stmt_9, negated_conjecture, (chevy @ skc9),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause7])).
% 0.54/0.75 thf(zip_derived_cl6, plain, ( (chevy @ skc9)),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_9])).
% 0.54/0.75 thf(clause18, conjecture, (~( ( old @ skc9 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_10, negated_conjecture, (( old @ skc9 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause18])).
% 0.54/0.75 thf(zip_derived_cl17, plain, (( (old @ skc9) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_10])).
% 0.54/0.75 thf(clause6, conjecture, (~( event @ skc10 ))).
% 0.54/0.75 thf(zf_stmt_11, negated_conjecture, (event @ skc10),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause6])).
% 0.54/0.75 thf(zip_derived_cl5, plain, ( (event @ skc10)),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_11])).
% 0.54/0.75 thf(clause5, conjecture, (~( hollywood @ skc11 ))).
% 0.54/0.75 thf(zf_stmt_12, negated_conjecture, (hollywood @ skc11),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause5])).
% 0.54/0.75 thf(zip_derived_cl4, plain, ( (hollywood @ skc11)),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_12])).
% 0.54/0.75 thf(clause16, conjecture, (~( ( street @ skc8 ) | ( ~( ssSkC0 ) ) ))).
% 0.54/0.75 thf(zf_stmt_13, negated_conjecture, (( street @ skc8 ) | ( ~( ssSkC0 ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause16])).
% 0.54/0.75 thf(zip_derived_cl15, plain, (( (street @ skc8) | ~ (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_13])).
% 0.54/0.75 thf(clause30, conjecture,
% 0.54/0.75 (~( ( ~( ssSkC0 ) ) | ( ~( hollywood @ X ) ) | ( ~( city @ X ) ) |
% 0.54/0.75 ( ~( in @ W @ X ) ) | ( ~( down @ W @ V ) ) |
% 0.54/0.75 ( ~( barrel @ W @ U ) ) | ( ~( event @ W ) ) | ( ~( street @ V ) ) |
% 0.54/0.75 ( ~( way @ V ) ) | ( ~( lonely @ V ) ) | ( ~( old @ U ) ) |
% 0.54/0.75 ( ~( dirty @ U ) ) | ( ~( white @ U ) ) | ( ~( car @ U ) ) |
% 0.54/0.75 ( ~( chevy @ U ) ) ))).
% 0.54/0.75 thf(zf_stmt_14, negated_conjecture,
% 0.54/0.75 (( ~( ssSkC0 ) ) | ( ~( hollywood @ X ) ) | ( ~( city @ X ) ) |
% 0.54/0.75 ( ~( in @ W @ X ) ) | ( ~( down @ W @ V ) ) | ( ~( barrel @ W @ U ) ) |
% 0.54/0.75 ( ~( event @ W ) ) | ( ~( street @ V ) ) | ( ~( way @ V ) ) |
% 0.54/0.75 ( ~( lonely @ V ) ) | ( ~( old @ U ) ) | ( ~( dirty @ U ) ) |
% 0.54/0.75 ( ~( white @ U ) ) | ( ~( car @ U ) ) | ( ~( chevy @ U ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause30])).
% 0.54/0.75 thf(zip_derived_cl29, plain,
% 0.54/0.75 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.54/0.75 (~ (ssSkC0)
% 0.54/0.75 | ~ (hollywood @ X0)
% 0.54/0.75 | ~ (city @ X0)
% 0.54/0.75 | ~ (in @ X1 @ X0)
% 0.54/0.75 | ~ (down @ X1 @ X2)
% 0.54/0.75 | ~ (barrel @ X1 @ X3)
% 0.54/0.75 | ~ (event @ X1)
% 0.54/0.75 | ~ (street @ X2)
% 0.54/0.75 | ~ (way @ X2)
% 0.54/0.75 | ~ (lonely @ X2)
% 0.54/0.75 | ~ (old @ X3)
% 0.54/0.75 | ~ (dirty @ X3)
% 0.54/0.75 | ~ (white @ X3)
% 0.54/0.75 | ~ (car @ X3)
% 0.54/0.75 | ~ (chevy @ X3))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_14])).
% 0.54/0.75 thf(zip_derived_cl41, plain,
% 0.54/0.75 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.75 (~ (ssSkC0)
% 0.54/0.75 | ~ (chevy @ X0)
% 0.54/0.75 | ~ (car @ X0)
% 0.54/0.75 | ~ (white @ X0)
% 0.54/0.75 | ~ (dirty @ X0)
% 0.54/0.75 | ~ (old @ X0)
% 0.54/0.75 | ~ (lonely @ skc8)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (event @ X1)
% 0.54/0.75 | ~ (barrel @ X1 @ X0)
% 0.54/0.75 | ~ (down @ X1 @ skc8)
% 0.54/0.75 | ~ (in @ X1 @ X2)
% 0.54/0.75 | ~ (city @ X2)
% 0.54/0.75 | ~ (hollywood @ X2)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl15, zip_derived_cl29])).
% 0.54/0.75 thf(zip_derived_cl47, plain,
% 0.54/0.75 (![X0 : $i, X1 : $i]:
% 0.54/0.75 (~ (ssSkC0)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (in @ X0 @ skc11)
% 0.54/0.75 | ~ (down @ X0 @ skc8)
% 0.54/0.75 | ~ (barrel @ X0 @ X1)
% 0.54/0.75 | ~ (event @ X0)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (lonely @ skc8)
% 0.54/0.75 | ~ (old @ X1)
% 0.54/0.75 | ~ (dirty @ X1)
% 0.54/0.75 | ~ (white @ X1)
% 0.54/0.75 | ~ (car @ X1)
% 0.54/0.75 | ~ (chevy @ X1)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl4, zip_derived_cl41])).
% 0.54/0.75 thf(zip_derived_cl59, plain,
% 0.54/0.75 (![X0 : $i]:
% 0.54/0.75 (~ (ssSkC0)
% 0.54/0.75 | ~ (chevy @ X0)
% 0.54/0.75 | ~ (car @ X0)
% 0.54/0.75 | ~ (white @ X0)
% 0.54/0.75 | ~ (dirty @ X0)
% 0.54/0.75 | ~ (old @ X0)
% 0.54/0.75 | ~ (lonely @ skc8)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (barrel @ skc10 @ X0)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl5, zip_derived_cl47])).
% 0.54/0.75 thf(zip_derived_cl83, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (barrel @ skc10 @ skc9)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (lonely @ skc8)
% 0.54/0.75 | ~ (dirty @ skc9)
% 0.54/0.75 | ~ (white @ skc9)
% 0.54/0.75 | ~ (car @ skc9)
% 0.54/0.75 | ~ (chevy @ skc9)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl17, zip_derived_cl59])).
% 0.54/0.75 thf(zip_derived_cl91, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (car @ skc9)
% 0.54/0.75 | ~ (white @ skc9)
% 0.54/0.75 | ~ (dirty @ skc9)
% 0.54/0.75 | ~ (lonely @ skc8)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (barrel @ skc10 @ skc9)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl6, zip_derived_cl83])).
% 0.54/0.75 thf(zip_derived_cl107, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (barrel @ skc10 @ skc9)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (dirty @ skc9)
% 0.54/0.75 | ~ (white @ skc9)
% 0.54/0.75 | ~ (car @ skc9)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl7, zip_derived_cl91])).
% 0.54/0.75 thf(zip_derived_cl123, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (white @ skc9)
% 0.54/0.75 | ~ (dirty @ skc9)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (barrel @ skc10 @ skc9)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl20, zip_derived_cl107])).
% 0.54/0.75 thf(zip_derived_cl131, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (barrel @ skc10 @ skc9)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (dirty @ skc9)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl19, zip_derived_cl123])).
% 0.54/0.75 thf(zip_derived_cl139, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (way @ skc8)
% 0.54/0.75 | ~ (barrel @ skc10 @ skc9)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl18, zip_derived_cl131])).
% 0.54/0.75 thf(zip_derived_cl147, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (city @ skc11)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (barrel @ skc10 @ skc9)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl16, zip_derived_cl139])).
% 0.54/0.75 thf(zip_derived_cl155, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (barrel @ skc10 @ skc9)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl21, zip_derived_cl147])).
% 0.54/0.75 thf(zip_derived_cl157, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (down @ skc10 @ skc8)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl25, zip_derived_cl155])).
% 0.54/0.75 thf(zip_derived_cl159, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (in @ skc10 @ skc11)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl26, zip_derived_cl157])).
% 0.54/0.75 thf(zip_derived_cl161, plain,
% 0.54/0.75 ((~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0)
% 0.54/0.75 | ~ (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl27, zip_derived_cl159])).
% 0.54/0.75 thf(zip_derived_cl162, plain, (~ (ssSkC0)),
% 0.54/0.75 inference('simplify', [status(thm)], [zip_derived_cl161])).
% 0.54/0.75 thf(clause25, conjecture, (~( ( in @ skc14 @ skc15 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_15, negated_conjecture, (( in @ skc14 @ skc15 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause25])).
% 0.54/0.75 thf(zip_derived_cl24, plain, (( (in @ skc14 @ skc15) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_15])).
% 0.54/0.75 thf(clause24, conjecture, (~( ( down @ skc14 @ skc13 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_16, negated_conjecture, (( down @ skc14 @ skc13 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause24])).
% 0.54/0.75 thf(zip_derived_cl23, plain, (( (down @ skc14 @ skc13) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_16])).
% 0.54/0.75 thf(clause23, conjecture, (~( ( barrel @ skc14 @ skc12 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_17, negated_conjecture,
% 0.54/0.75 (( barrel @ skc14 @ skc12 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause23])).
% 0.54/0.75 thf(zip_derived_cl22, plain, (( (barrel @ skc14 @ skc12) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_17])).
% 0.54/0.75 thf(clause15, conjecture, (~( ( city @ skc15 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_18, negated_conjecture, (( city @ skc15 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause15])).
% 0.54/0.75 thf(zip_derived_cl14, plain, (( (city @ skc15) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_18])).
% 0.54/0.75 thf(clause14, conjecture, (~( ( way @ skc13 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_19, negated_conjecture, (( way @ skc13 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause14])).
% 0.54/0.75 thf(zip_derived_cl13, plain, (( (way @ skc13) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_19])).
% 0.54/0.75 thf(clause12, conjecture, (~( ( dirty @ skc12 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_20, negated_conjecture, (( dirty @ skc12 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause12])).
% 0.54/0.75 thf(zip_derived_cl11, plain, (( (dirty @ skc12) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_20])).
% 0.54/0.75 thf(clause11, conjecture, (~( ( white @ skc12 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_21, negated_conjecture, (( white @ skc12 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause11])).
% 0.54/0.75 thf(zip_derived_cl10, plain, (( (white @ skc12) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_21])).
% 0.54/0.75 thf(clause10, conjecture, (~( ( car @ skc12 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_22, negated_conjecture, (( car @ skc12 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause10])).
% 0.54/0.75 thf(zip_derived_cl9, plain, (( (car @ skc12) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_22])).
% 0.54/0.75 thf(clause13, conjecture, (~( ( lonely @ skc13 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_23, negated_conjecture, (( lonely @ skc13 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause13])).
% 0.54/0.75 thf(zip_derived_cl12, plain, (( (lonely @ skc13) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_23])).
% 0.54/0.75 thf(clause9, conjecture, (~( ( chevy @ skc12 ) | ( ssSkC0 ) ))).
% 0.54/0.75 thf(zf_stmt_24, negated_conjecture, (( chevy @ skc12 ) | ( ssSkC0 )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause9])).
% 0.54/0.75 thf(zip_derived_cl8, plain, (( (chevy @ skc12) | (ssSkC0))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_24])).
% 0.54/0.75 thf(clause4, conjecture, (~( old @ skc12 ))).
% 0.54/0.75 thf(zf_stmt_25, negated_conjecture, (old @ skc12),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause4])).
% 0.54/0.75 thf(zip_derived_cl3, plain, ( (old @ skc12)),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_25])).
% 0.54/0.75 thf(clause2, conjecture, (~( event @ skc14 ))).
% 0.54/0.75 thf(zf_stmt_26, negated_conjecture, (event @ skc14),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause2])).
% 0.54/0.75 thf(zip_derived_cl1, plain, ( (event @ skc14)),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_26])).
% 0.54/0.75 thf(clause1, conjecture, (~( hollywood @ skc15 ))).
% 0.54/0.75 thf(zf_stmt_27, negated_conjecture, (hollywood @ skc15),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause1])).
% 0.54/0.75 thf(zip_derived_cl0, plain, ( (hollywood @ skc15)),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_27])).
% 0.54/0.75 thf(clause3, conjecture, (~( street @ skc13 ))).
% 0.54/0.75 thf(zf_stmt_28, negated_conjecture, (street @ skc13),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause3])).
% 0.54/0.75 thf(zip_derived_cl2, plain, ( (street @ skc13)),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_28])).
% 0.54/0.75 thf(clause29, conjecture,
% 0.54/0.75 (~( ( ssSkC0 ) | ( ~( hollywood @ X ) ) | ( ~( city @ X ) ) |
% 0.54/0.75 ( ~( in @ W @ X ) ) | ( ~( down @ W @ U ) ) |
% 0.54/0.75 ( ~( barrel @ W @ V ) ) | ( ~( event @ W ) ) | ( ~( chevy @ V ) ) |
% 0.54/0.75 ( ~( car @ V ) ) | ( ~( white @ V ) ) | ( ~( dirty @ V ) ) |
% 0.54/0.75 ( ~( old @ V ) ) | ( ~( lonely @ U ) ) | ( ~( way @ U ) ) |
% 0.54/0.75 ( ~( street @ U ) ) ))).
% 0.54/0.75 thf(zf_stmt_29, negated_conjecture,
% 0.54/0.75 (( ssSkC0 ) | ( ~( hollywood @ X ) ) | ( ~( city @ X ) ) |
% 0.54/0.75 ( ~( in @ W @ X ) ) | ( ~( down @ W @ U ) ) | ( ~( barrel @ W @ V ) ) |
% 0.54/0.75 ( ~( event @ W ) ) | ( ~( chevy @ V ) ) | ( ~( car @ V ) ) |
% 0.54/0.75 ( ~( white @ V ) ) | ( ~( dirty @ V ) ) | ( ~( old @ V ) ) |
% 0.54/0.75 ( ~( lonely @ U ) ) | ( ~( way @ U ) ) | ( ~( street @ U ) )),
% 0.54/0.75 inference('cnf.neg', [status(esa)], [clause29])).
% 0.54/0.75 thf(zip_derived_cl28, plain,
% 0.54/0.75 (![X0 : $i, X1 : $i, X2 : $i, X3 : $i]:
% 0.54/0.75 ( (ssSkC0)
% 0.54/0.75 | ~ (hollywood @ X0)
% 0.54/0.75 | ~ (city @ X0)
% 0.54/0.75 | ~ (in @ X1 @ X0)
% 0.54/0.75 | ~ (down @ X1 @ X2)
% 0.54/0.75 | ~ (barrel @ X1 @ X3)
% 0.54/0.75 | ~ (event @ X1)
% 0.54/0.75 | ~ (chevy @ X3)
% 0.54/0.75 | ~ (car @ X3)
% 0.54/0.75 | ~ (white @ X3)
% 0.54/0.75 | ~ (dirty @ X3)
% 0.54/0.75 | ~ (old @ X3)
% 0.54/0.75 | ~ (lonely @ X2)
% 0.54/0.75 | ~ (way @ X2)
% 0.54/0.75 | ~ (street @ X2))),
% 0.54/0.75 inference('cnf', [status(esa)], [zf_stmt_29])).
% 0.54/0.75 thf(zip_derived_cl38, plain,
% 0.54/0.75 (![X0 : $i, X1 : $i, X2 : $i]:
% 0.54/0.75 (~ (way @ skc13)
% 0.54/0.75 | ~ (lonely @ skc13)
% 0.54/0.75 | ~ (old @ X0)
% 0.54/0.75 | ~ (dirty @ X0)
% 0.54/0.75 | ~ (white @ X0)
% 0.54/0.75 | ~ (car @ X0)
% 0.54/0.75 | ~ (chevy @ X0)
% 0.54/0.75 | ~ (event @ X1)
% 0.54/0.75 | ~ (barrel @ X1 @ X0)
% 0.54/0.75 | ~ (down @ X1 @ skc13)
% 0.54/0.75 | ~ (in @ X1 @ X2)
% 0.54/0.75 | ~ (city @ X2)
% 0.54/0.75 | ~ (hollywood @ X2)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl2, zip_derived_cl28])).
% 0.54/0.75 thf(zip_derived_cl42, plain,
% 0.54/0.75 (![X0 : $i, X1 : $i]:
% 0.54/0.75 ( (ssSkC0)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | ~ (in @ X0 @ skc15)
% 0.54/0.75 | ~ (down @ X0 @ skc13)
% 0.54/0.75 | ~ (barrel @ X0 @ X1)
% 0.54/0.75 | ~ (event @ X0)
% 0.54/0.75 | ~ (chevy @ X1)
% 0.54/0.75 | ~ (car @ X1)
% 0.54/0.75 | ~ (white @ X1)
% 0.54/0.75 | ~ (dirty @ X1)
% 0.54/0.75 | ~ (old @ X1)
% 0.54/0.75 | ~ (lonely @ skc13)
% 0.54/0.75 | ~ (way @ skc13))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl0, zip_derived_cl38])).
% 0.54/0.75 thf(zip_derived_cl48, plain,
% 0.54/0.75 (![X0 : $i]:
% 0.54/0.75 (~ (way @ skc13)
% 0.54/0.75 | ~ (lonely @ skc13)
% 0.54/0.75 | ~ (old @ X0)
% 0.54/0.75 | ~ (dirty @ X0)
% 0.54/0.75 | ~ (white @ X0)
% 0.54/0.75 | ~ (car @ X0)
% 0.54/0.75 | ~ (chevy @ X0)
% 0.54/0.75 | ~ (barrel @ skc14 @ X0)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl1, zip_derived_cl42])).
% 0.54/0.75 thf(zip_derived_cl60, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (barrel @ skc14 @ skc12)
% 0.54/0.75 | ~ (chevy @ skc12)
% 0.54/0.75 | ~ (car @ skc12)
% 0.54/0.75 | ~ (white @ skc12)
% 0.54/0.75 | ~ (dirty @ skc12)
% 0.54/0.75 | ~ (lonely @ skc13)
% 0.54/0.75 | ~ (way @ skc13))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl3, zip_derived_cl48])).
% 0.54/0.75 thf(zip_derived_cl92, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | ~ (way @ skc13)
% 0.54/0.75 | ~ (lonely @ skc13)
% 0.54/0.75 | ~ (dirty @ skc12)
% 0.54/0.75 | ~ (white @ skc12)
% 0.54/0.75 | ~ (car @ skc12)
% 0.54/0.75 | ~ (barrel @ skc14 @ skc12)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl8, zip_derived_cl60])).
% 0.54/0.75 thf(zip_derived_cl112, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (barrel @ skc14 @ skc12)
% 0.54/0.75 | ~ (car @ skc12)
% 0.54/0.75 | ~ (white @ skc12)
% 0.54/0.75 | ~ (dirty @ skc12)
% 0.54/0.75 | ~ (way @ skc13)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl12, zip_derived_cl92])).
% 0.54/0.75 thf(zip_derived_cl116, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | ~ (way @ skc13)
% 0.54/0.75 | ~ (dirty @ skc12)
% 0.54/0.75 | ~ (white @ skc12)
% 0.54/0.75 | ~ (barrel @ skc14 @ skc12)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl9, zip_derived_cl112])).
% 0.54/0.75 thf(zip_derived_cl124, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (barrel @ skc14 @ skc12)
% 0.54/0.75 | ~ (dirty @ skc12)
% 0.54/0.75 | ~ (way @ skc13)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl10, zip_derived_cl116])).
% 0.54/0.75 thf(zip_derived_cl132, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | ~ (way @ skc13)
% 0.54/0.75 | ~ (barrel @ skc14 @ skc12)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl11, zip_derived_cl124])).
% 0.54/0.75 thf(zip_derived_cl140, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | ~ (city @ skc15)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (barrel @ skc14 @ skc12)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl13, zip_derived_cl132])).
% 0.54/0.75 thf(zip_derived_cl148, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | ~ (barrel @ skc14 @ skc12)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl14, zip_derived_cl140])).
% 0.54/0.75 thf(zip_derived_cl156, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | ~ (down @ skc14 @ skc13)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl22, zip_derived_cl148])).
% 0.54/0.75 thf(zip_derived_cl158, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | ~ (in @ skc14 @ skc15)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl23, zip_derived_cl156])).
% 0.54/0.75 thf(zip_derived_cl160, plain,
% 0.54/0.75 (( (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0)
% 0.54/0.75 | (ssSkC0))),
% 0.54/0.75 inference('dp-resolution', [status(thm)],
% 0.54/0.75 [zip_derived_cl24, zip_derived_cl158])).
% 0.54/0.75 thf(zip_derived_cl163, plain, ( (ssSkC0)),
% 0.54/0.75 inference('simplify', [status(thm)], [zip_derived_cl160])).
% 0.54/0.75 thf(zip_derived_cl164, plain, ($false),
% 0.54/0.75 inference('demod', [status(thm)], [zip_derived_cl162, zip_derived_cl163])).
% 0.54/0.75
% 0.54/0.75 % SZS output end Refutation
% 0.54/0.75
% 0.54/0.75
% 0.54/0.75 % /export/starexec/sandbox/solver/bin/fo/fo7.sh running for 63s
% 0.54/0.75 % Terminating...
% 0.58/0.84 % Runner terminated.
% 0.58/0.85 % Zipperpin 1.5 exiting
%------------------------------------------------------------------------------