%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : NLP001^7 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:16:17 AM UTC 2026
% Result : Theorem 64.66s 31.54s
% Output : Refutation 65.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NLP001^7 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.09/0.20 % Computer : n013.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 11:28:36 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.88/0.79 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.59/1.08 % [INFO] Parsing done (283ms).
% 1.59/1.09 % [INFO] Running in sequential loop mode.
% 2.55/1.50 % [INFO] eprover registered as external prover.
% 2.55/1.51 % [INFO] Scanning for conjecture ...
% 3.05/1.72 % [INFO] Found a conjecture (or negated_conjecture) and 4 axioms. Running axiom selection ...
% 3.05/1.77 % [INFO] Axiom selection finished. Selected 4 axioms (removed 0 axioms).
% 3.05/1.78 % [INFO] Problem is higher-order (TPTP THF).
% 3.05/1.78 % [INFO] Type checking passed.
% 3.05/1.79 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 64.66/31.53 % [INFO] Killing All external provers ...
% 64.66/31.54 % Time passed: 31187ms (effective reasoning time: 30435ms)
% 64.66/31.54 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 64.66/31.54 % Axioms used in derivation (0):
% 64.66/31.54 % No. of inferences in proof: 148
% 64.66/31.54 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 31187 ms resp. 30435 ms w/o parsing
% 65.43/31.72 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 65.43/31.72 thf(mu_type, type, mu: $tType).
% 65.43/31.72 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 65.43/31.72 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 65.43/31.72 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 65.43/31.72 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 65.43/31.72 thf(exists_in_world_decl, type, exists_in_world: (mu > ($i > $o))).
% 65.43/31.72 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 65.43/31.72 thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 65.43/31.72 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 65.43/31.72 thf(in_decl, type, in: (mu > (mu > ($i > $o)))).
% 65.43/31.72 thf(down_decl, type, down: (mu > (mu > ($i > $o)))).
% 65.43/31.72 thf(barrel_decl, type, barrel: (mu > (mu > ($i > $o)))).
% 65.43/31.72 thf(old_decl, type, old: (mu > ($i > $o))).
% 65.43/31.72 thf(dirty_decl, type, dirty: (mu > ($i > $o))).
% 65.43/31.72 thf(white_decl, type, white: (mu > ($i > $o))).
% 65.43/31.72 thf(car_decl, type, car: (mu > ($i > $o))).
% 65.43/31.72 thf(chevy_decl, type, chevy: (mu > ($i > $o))).
% 65.43/31.72 thf(lonely_decl, type, lonely: (mu > ($i > $o))).
% 65.43/31.72 thf(way_decl, type, way: (mu > ($i > $o))).
% 65.43/31.72 thf(street_decl, type, street: (mu > ($i > $o))).
% 65.43/31.72 thf(event_decl, type, event: (mu > ($i > $o))).
% 65.43/31.72 thf(city_decl, type, city: (mu > ($i > $o))).
% 65.43/31.72 thf(hollywood_decl, type, hollywood: (mu > ($i > $o))).
% 65.43/31.72 thf(sk1_decl, type, sk1: $o).
% 65.43/31.72 thf(sk2_decl, type, sk2: $i).
% 65.43/31.72 thf(sk3_decl, type, sk3: mu).
% 65.43/31.72 thf(sk4_decl, type, sk4: mu).
% 65.43/31.72 thf(sk5_decl, type, sk5: mu).
% 65.43/31.72 thf(sk6_decl, type, sk6: mu).
% 65.43/31.72 thf(sk7_decl, type, sk7: $i).
% 65.43/31.72 thf(sk8_decl, type, sk8: mu).
% 65.43/31.72 thf(sk9_decl, type, sk9: mu).
% 65.43/31.72 thf(sk10_decl, type, sk10: mu).
% 65.43/31.72 thf(sk11_decl, type, sk11: mu).
% 65.43/31.72 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 65.43/31.72 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 65.43/31.72 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 65.43/31.72 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 65.43/31.72 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: ((exists_in_world @ C @ B) => (A @ C @ B))) ).
% 65.43/31.72 thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o))]: (mnot @ (mforall_ind @ (^ [B:mu]: (mnot @ (A @ B)))))) ).
% 65.43/31.72 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 65.43/31.72 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (street @ D @ A) | ~ (way @ D @ A) | ~ (lonely @ D @ A) | ~ (chevy @ E @ A) | ~ (car @ E @ A) | ~ (white @ E @ A) | ~ (dirty @ E @ A) | ~ (old @ E @ A) | ~ (barrel @ C @ E @ A) | ~ (down @ C @ D @ A) | ~ (in @ C @ B @ A))))))))) | ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (chevy @ D @ A) | ~ (car @ D @ A) | ~ (white @ D @ A) | ~ (dirty @ D @ A) | ~ (old @ D @ A) | ~ (street @ E @ A) | ~ (way @ E @ A) | ~ (lonely @ E @ A) | ~ (barrel @ C @ D @ A) | ~ (down @ C @ E @ A) | ~ (in @ C @ B @ A)))))))))))) ).
% 65.43/31.72 thf(sk3_def, definition, sk3 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk2) => (! [B:mu]: ((exists_in_world @ B @ sk2) => (! [C:mu]: ((exists_in_world @ C @ sk2) => (! [D:mu]: ((exists_in_world @ D @ sk2) => (~ (hollywood @ A @ sk2) | ~ (city @ A @ sk2) | ~ (event @ B @ sk2) | ~ (street @ C @ sk2) | ~ (way @ C @ sk2) | ~ (lonely @ C @ sk2) | ~ (chevy @ D @ sk2) | ~ (car @ D @ sk2) | ~ (white @ D @ sk2) | ~ (dirty @ D @ sk2) | ~ (old @ D @ sk2) | ~ (barrel @ B @ D @ sk2) | ~ (down @ B @ C @ sk2) | ~ (in @ B @ A @ sk2)))))))))) ).
% 65.43/31.72 thf(sk4_def, definition, sk4 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk2) => (! [B:mu]: ((exists_in_world @ B @ sk2) => (! [C:mu]: ((exists_in_world @ C @ sk2) => (~ (hollywood @ sk3 @ sk2) | ~ (city @ sk3 @ sk2) | ~ (event @ A @ sk2) | ~ (street @ B @ sk2) | ~ (way @ B @ sk2) | ~ (lonely @ B @ sk2) | ~ (chevy @ C @ sk2) | ~ (car @ C @ sk2) | ~ (white @ C @ sk2) | ~ (dirty @ C @ sk2) | ~ (old @ C @ sk2) | ~ (barrel @ A @ C @ sk2) | ~ (down @ A @ B @ sk2) | ~ (in @ A @ sk3 @ sk2)))))))) ).
% 65.43/31.72 thf(sk5_def, definition, sk5 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk2) => (! [B:mu]: ((exists_in_world @ B @ sk2) => (~ (hollywood @ sk3 @ sk2) | ~ (city @ sk3 @ sk2) | ~ (event @ sk4 @ sk2) | ~ (street @ A @ sk2) | ~ (way @ A @ sk2) | ~ (lonely @ A @ sk2) | ~ (chevy @ B @ sk2) | ~ (car @ B @ sk2) | ~ (white @ B @ sk2) | ~ (dirty @ B @ sk2) | ~ (old @ B @ sk2) | ~ (barrel @ sk4 @ B @ sk2) | ~ (down @ sk4 @ A @ sk2) | ~ (in @ sk4 @ sk3 @ sk2)))))) ).
% 65.43/31.72 thf(sk6_def, definition, sk6 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk2) => (~ (hollywood @ sk3 @ sk2) | ~ (city @ sk3 @ sk2) | ~ (event @ sk4 @ sk2) | ~ (street @ sk5 @ sk2) | ~ (way @ sk5 @ sk2) | ~ (lonely @ sk5 @ sk2) | ~ (chevy @ A @ sk2) | ~ (car @ A @ sk2) | ~ (white @ A @ sk2) | ~ (dirty @ A @ sk2) | ~ (old @ A @ sk2) | ~ (barrel @ sk4 @ A @ sk2) | ~ (down @ sk4 @ sk5 @ sk2) | ~ (in @ sk4 @ sk3 @ sk2)))) ).
% 65.43/31.72 thf(sk7_def, definition, sk7 = (@+ [A:$i]: ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (chevy @ D @ A) | ~ (car @ D @ A) | ~ (white @ D @ A) | ~ (dirty @ D @ A) | ~ (old @ D @ A) | ~ (street @ E @ A) | ~ (way @ E @ A) | ~ (lonely @ E @ A) | ~ (barrel @ C @ D @ A) | ~ (down @ C @ E @ A) | ~ (in @ C @ B @ A))))))))) | ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (street @ D @ A) | ~ (way @ D @ A) | ~ (lonely @ D @ A) | ~ (chevy @ E @ A) | ~ (car @ E @ A) | ~ (white @ E @ A) | ~ (dirty @ E @ A) | ~ (old @ E @ A) | ~ (barrel @ C @ E @ A) | ~ (down @ C @ D @ A) | ~ (in @ C @ B @ A)))))))))))) ).
% 65.43/31.72 thf(sk8_def, definition, sk8 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk7) => (! [B:mu]: ((exists_in_world @ B @ sk7) => (! [C:mu]: ((exists_in_world @ C @ sk7) => (! [D:mu]: ((exists_in_world @ D @ sk7) => (~ (hollywood @ A @ sk7) | ~ (city @ A @ sk7) | ~ (event @ B @ sk7) | ~ (chevy @ C @ sk7) | ~ (car @ C @ sk7) | ~ (white @ C @ sk7) | ~ (dirty @ C @ sk7) | ~ (old @ C @ sk7) | ~ (street @ D @ sk7) | ~ (way @ D @ sk7) | ~ (lonely @ D @ sk7) | ~ (barrel @ B @ C @ sk7) | ~ (down @ B @ D @ sk7) | ~ (in @ B @ A @ sk7)))))))))) ).
% 65.43/31.72 thf(sk9_def, definition, sk9 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk7) => (! [B:mu]: ((exists_in_world @ B @ sk7) => (! [C:mu]: ((exists_in_world @ C @ sk7) => (~ (hollywood @ sk8 @ sk7) | ~ (city @ sk8 @ sk7) | ~ (event @ A @ sk7) | ~ (chevy @ B @ sk7) | ~ (car @ B @ sk7) | ~ (white @ B @ sk7) | ~ (dirty @ B @ sk7) | ~ (old @ B @ sk7) | ~ (street @ C @ sk7) | ~ (way @ C @ sk7) | ~ (lonely @ C @ sk7) | ~ (barrel @ A @ B @ sk7) | ~ (down @ A @ C @ sk7) | ~ (in @ A @ sk8 @ sk7)))))))) ).
% 65.43/31.72 thf(sk10_def, definition, sk10 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk7) => (! [B:mu]: ((exists_in_world @ B @ sk7) => (~ (hollywood @ sk8 @ sk7) | ~ (city @ sk8 @ sk7) | ~ (event @ sk9 @ sk7) | ~ (chevy @ A @ sk7) | ~ (car @ A @ sk7) | ~ (white @ A @ sk7) | ~ (dirty @ A @ sk7) | ~ (old @ A @ sk7) | ~ (street @ B @ sk7) | ~ (way @ B @ sk7) | ~ (lonely @ B @ sk7) | ~ (barrel @ sk9 @ A @ sk7) | ~ (down @ sk9 @ B @ sk7) | ~ (in @ sk9 @ sk8 @ sk7)))))) ).
% 65.43/31.72 thf(sk11_def, definition, sk11 = (@+ [A:mu]: ~ ((exists_in_world @ A @ sk7) => (~ (hollywood @ sk8 @ sk7) | ~ (city @ sk8 @ sk7) | ~ (event @ sk9 @ sk7) | ~ (chevy @ sk10 @ sk7) | ~ (car @ sk10 @ sk7) | ~ (white @ sk10 @ sk7) | ~ (dirty @ sk10 @ sk7) | ~ (old @ sk10 @ sk7) | ~ (street @ A @ sk7) | ~ (way @ A @ sk7) | ~ (lonely @ A @ sk7) | ~ (barrel @ sk9 @ sk10 @ sk7) | ~ (down @ sk9 @ A @ sk7) | ~ (in @ sk9 @ sk8 @ sk7)))) ).
% 65.43/31.72 thf(1,conjecture,((mvalid @ (mand @ (mimplies @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (hollywood @ A) @ (mand @ (city @ A) @ (mand @ (event @ B) @ (mand @ (street @ C) @ (mand @ (way @ C) @ (mand @ (lonely @ C) @ (mand @ (chevy @ D) @ (mand @ (car @ D) @ (mand @ (white @ D) @ (mand @ (dirty @ D) @ (mand @ (old @ D) @ (mand @ (barrel @ B @ D) @ (mand @ (down @ B @ C) @ (in @ B @ A)))))))))))))))))))))) @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (hollywood @ A) @ (mand @ (city @ A) @ (mand @ (event @ B) @ (mand @ (chevy @ C) @ (mand @ (car @ C) @ (mand @ (white @ C) @ (mand @ (dirty @ C) @ (mand @ (old @ C) @ (mand @ (street @ D) @ (mand @ (way @ D) @ (mand @ (lonely @ D) @ (mand @ (barrel @ B @ C) @ (mand @ (down @ B @ D) @ (in @ B @ A))))))))))))))))))))))) @ (mimplies @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (hollywood @ A) @ (mand @ (city @ A) @ (mand @ (event @ B) @ (mand @ (chevy @ C) @ (mand @ (car @ C) @ (mand @ (white @ C) @ (mand @ (dirty @ C) @ (mand @ (old @ C) @ (mand @ (street @ D) @ (mand @ (way @ D) @ (mand @ (lonely @ D) @ (mand @ (barrel @ B @ C) @ (mand @ (down @ B @ D) @ (in @ B @ A)))))))))))))))))))))) @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (hollywood @ A) @ (mand @ (city @ A) @ (mand @ (event @ B) @ (mand @ (street @ C) @ (mand @ (way @ C) @ (mand @ (lonely @ C) @ (mand @ (chevy @ D) @ (mand @ (car @ D) @ (mand @ (white @ D) @ (mand @ (dirty @ D) @ (mand @ (old @ D) @ (mand @ (barrel @ B @ D) @ (mand @ (down @ B @ C) @ (in @ B @ A)))))))))))))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
% 65.43/31.72 thf(2,negated_conjecture,((~ (mvalid @ (mand @ (mimplies @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (hollywood @ A) @ (mand @ (city @ A) @ (mand @ (event @ B) @ (mand @ (street @ C) @ (mand @ (way @ C) @ (mand @ (lonely @ C) @ (mand @ (chevy @ D) @ (mand @ (car @ D) @ (mand @ (white @ D) @ (mand @ (dirty @ D) @ (mand @ (old @ D) @ (mand @ (barrel @ B @ D) @ (mand @ (down @ B @ C) @ (in @ B @ A)))))))))))))))))))))) @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (hollywood @ A) @ (mand @ (city @ A) @ (mand @ (event @ B) @ (mand @ (chevy @ C) @ (mand @ (car @ C) @ (mand @ (white @ C) @ (mand @ (dirty @ C) @ (mand @ (old @ C) @ (mand @ (street @ D) @ (mand @ (way @ D) @ (mand @ (lonely @ D) @ (mand @ (barrel @ B @ C) @ (mand @ (down @ B @ D) @ (in @ B @ A))))))))))))))))))))))) @ (mimplies @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (hollywood @ A) @ (mand @ (city @ A) @ (mand @ (event @ B) @ (mand @ (chevy @ C) @ (mand @ (car @ C) @ (mand @ (white @ C) @ (mand @ (dirty @ C) @ (mand @ (old @ C) @ (mand @ (street @ D) @ (mand @ (way @ D) @ (mand @ (lonely @ D) @ (mand @ (barrel @ B @ C) @ (mand @ (down @ B @ D) @ (in @ B @ A)))))))))))))))))))))) @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (^ [B:mu]: (mexists_ind @ (^ [C:mu]: (mexists_ind @ (^ [D:mu]: (mand @ (hollywood @ A) @ (mand @ (city @ A) @ (mand @ (event @ B) @ (mand @ (street @ C) @ (mand @ (way @ C) @ (mand @ (lonely @ C) @ (mand @ (chevy @ D) @ (mand @ (car @ D) @ (mand @ (white @ D) @ (mand @ (dirty @ D) @ (mand @ (old @ D) @ (mand @ (barrel @ B @ D) @ (mand @ (down @ B @ C) @ (in @ B @ A))))))))))))))))))))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 65.43/31.72 thf(7,plain,((~ (! [A:$i]: ~ (~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (street @ D @ A) | ~ (way @ D @ A) | ~ (lonely @ D @ A) | ~ (chevy @ E @ A) | ~ (car @ E @ A) | ~ (white @ E @ A) | ~ (dirty @ E @ A) | ~ (old @ E @ A) | ~ (barrel @ C @ E @ A) | ~ (down @ C @ D @ A) | ~ (in @ C @ B @ A))))))))) | ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (chevy @ D @ A) | ~ (car @ D @ A) | ~ (white @ D @ A) | ~ (dirty @ D @ A) | ~ (old @ D @ A) | ~ (street @ E @ A) | ~ (way @ E @ A) | ~ (lonely @ E @ A) | ~ (barrel @ C @ D @ A) | ~ (down @ C @ E @ A) | ~ (in @ C @ B @ A))))))))))) | ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (chevy @ D @ A) | ~ (car @ D @ A) | ~ (white @ D @ A) | ~ (dirty @ D @ A) | ~ (old @ D @ A) | ~ (street @ E @ A) | ~ (way @ E @ A) | ~ (lonely @ E @ A) | ~ (barrel @ C @ D @ A) | ~ (down @ C @ E @ A) | ~ (in @ C @ B @ A))))))))) | ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (street @ D @ A) | ~ (way @ D @ A) | ~ (lonely @ D @ A) | ~ (chevy @ E @ A) | ~ (car @ E @ A) | ~ (white @ E @ A) | ~ (dirty @ E @ A) | ~ (old @ E @ A) | ~ (barrel @ C @ E @ A) | ~ (down @ C @ D @ A) | ~ (in @ C @ B @ A))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 65.43/31.72 thf(8,plain,((~ (~ (~ (! [A:$i]: (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (street @ D @ A) | ~ (way @ D @ A) | ~ (lonely @ D @ A) | ~ (chevy @ E @ A) | ~ (car @ E @ A) | ~ (white @ E @ A) | ~ (dirty @ E @ A) | ~ (old @ E @ A) | ~ (barrel @ C @ E @ A) | ~ (down @ C @ D @ A) | ~ (in @ C @ B @ A))))))))) | ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (chevy @ D @ A) | ~ (car @ D @ A) | ~ (white @ D @ A) | ~ (dirty @ D @ A) | ~ (old @ D @ A) | ~ (street @ E @ A) | ~ (way @ E @ A) | ~ (lonely @ E @ A) | ~ (barrel @ C @ D @ A) | ~ (down @ C @ E @ A) | ~ (in @ C @ B @ A)))))))))))) | ~ (! [A:$i]: (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (chevy @ D @ A) | ~ (car @ D @ A) | ~ (white @ D @ A) | ~ (dirty @ D @ A) | ~ (old @ D @ A) | ~ (street @ E @ A) | ~ (way @ E @ A) | ~ (lonely @ E @ A) | ~ (barrel @ C @ D @ A) | ~ (down @ C @ E @ A) | ~ (in @ C @ B @ A))))))))) | ~ (! [B:mu]: ((exists_in_world @ B @ A) => (! [C:mu]: ((exists_in_world @ C @ A) => (! [D:mu]: ((exists_in_world @ D @ A) => (! [E:mu]: ((exists_in_world @ E @ A) => (~ (hollywood @ B @ A) | ~ (city @ B @ A) | ~ (event @ C @ A) | ~ (street @ D @ A) | ~ (way @ D @ A) | ~ (lonely @ D @ A) | ~ (chevy @ E @ A) | ~ (car @ E @ A) | ~ (white @ E @ A) | ~ (dirty @ E @ A) | ~ (old @ E @ A) | ~ (barrel @ C @ E @ A) | ~ (down @ C @ D @ A) | ~ (in @ C @ B @ A)))))))))))))))),inference(miniscope,[status(thm)],[7])).
% 65.43/31.72 thf(9,plain,(! [H:mu,G:mu,F:mu,E:mu,D:mu,C:mu,B:mu,A:mu] : ((((exists_in_world @ sk3 @ sk2) | (sk1)) & ((exists_in_world @ sk4 @ sk2) | (sk1)) & ((exists_in_world @ sk5 @ sk2) | (sk1)) & ((exists_in_world @ sk6 @ sk2) | (sk1)) & ((hollywood @ sk3 @ sk2) | (sk1)) & ((city @ sk3 @ sk2) | (sk1)) & ((event @ sk4 @ sk2) | (sk1)) & ((street @ sk5 @ sk2) | (sk1)) & ((way @ sk5 @ sk2) | (sk1)) & ((lonely @ sk5 @ sk2) | (sk1)) & ((chevy @ sk6 @ sk2) | (sk1)) & ((car @ sk6 @ sk2) | (sk1)) & ((white @ sk6 @ sk2) | (sk1)) & ((dirty @ sk6 @ sk2) | (sk1)) & ((old @ sk6 @ sk2) | (sk1)) & ((barrel @ sk4 @ sk6 @ sk2) | (sk1)) & ((down @ sk4 @ sk5 @ sk2) | (sk1)) & ((in @ sk4 @ sk3 @ sk2) | (sk1)) & (~ (exists_in_world @ A @ sk2) | ~ (exists_in_world @ B @ sk2) | ~ (exists_in_world @ C @ sk2) | ~ (exists_in_world @ D @ sk2) | ~ (hollywood @ A @ sk2) | ~ (city @ A @ sk2) | ~ (event @ B @ sk2) | ~ (chevy @ C @ sk2) | ~ (car @ C @ sk2) | ~ (white @ C @ sk2) | ~ (dirty @ C @ sk2) | ~ (old @ C @ sk2) | ~ (street @ D @ sk2) | ~ (way @ D @ sk2) | ~ (lonely @ D @ sk2) | ~ (barrel @ B @ C @ sk2) | ~ (down @ B @ D @ sk2) | ~ (in @ B @ A @ sk2) | (sk1)) & (~ (sk1) | (exists_in_world @ sk8 @ sk7)) & (~ (sk1) | (exists_in_world @ sk9 @ sk7)) & (~ (sk1) | (exists_in_world @ sk10 @ sk7)) & (~ (sk1) | (exists_in_world @ sk11 @ sk7)) & (~ (sk1) | (hollywood @ sk8 @ sk7)) & (~ (sk1) | (city @ sk8 @ sk7)) & (~ (sk1) | (event @ sk9 @ sk7)) & (~ (sk1) | (chevy @ sk10 @ sk7)) & (~ (sk1) | (car @ sk10 @ sk7)) & (~ (sk1) | (white @ sk10 @ sk7)) & (~ (sk1) | (dirty @ sk10 @ sk7)) & (~ (sk1) | (old @ sk10 @ sk7)) & (~ (sk1) | (street @ sk11 @ sk7)) & (~ (sk1) | (way @ sk11 @ sk7)) & (~ (sk1) | (lonely @ sk11 @ sk7)) & (~ (sk1) | (barrel @ sk9 @ sk10 @ sk7)) & (~ (sk1) | (down @ sk9 @ sk11 @ sk7)) & (~ (sk1) | (in @ sk9 @ sk8 @ sk7)) & (~ (sk1) | ~ (exists_in_world @ E @ sk7) | ~ (exists_in_world @ F @ sk7) | ~ (exists_in_world @ G @ sk7) | ~ (exists_in_world @ H @ sk7) | ~ (hollywood @ E @ sk7) | ~ (city @ E @ sk7) | ~ (event @ F @ sk7) | ~ (street @ G @ sk7) | ~ (way @ G @ sk7) | ~ (lonely @ G @ sk7) | ~ (chevy @ H @ sk7) | ~ (car @ H @ sk7) | ~ (white @ H @ sk7) | ~ (dirty @ H @ sk7) | ~ (old @ H @ sk7) | ~ (barrel @ F @ H @ sk7) | ~ (down @ F @ G @ sk7) | ~ (in @ F @ E @ sk7))))),inference(cnf,[status(esa)],[8])).
% 65.43/31.72 thf(19,plain,((in @ sk4 @ sk3 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(36,plain,(~ (sk1) | (street @ sk11 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(23,plain,(~ (sk1) | (old @ sk10 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(26,plain,(~ (sk1) | (hollywood @ sk8 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(43,plain,(~ (sk1) | (exists_in_world @ sk11 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(31,plain,(~ (sk1) | (lonely @ sk11 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(39,plain,(~ (sk1) | (chevy @ sk10 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(22,plain,(~ (sk1) | (way @ sk11 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(34,plain,(~ (sk1) | (exists_in_world @ sk9 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(32,plain,(~ (sk1) | (white @ sk10 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(17,plain,(~ (sk1) | (dirty @ sk10 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(13,plain,(~ (sk1) | (city @ sk8 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(29,plain,(~ (sk1) | (exists_in_world @ sk8 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(42,plain,(~ (sk1) | (car @ sk10 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(10,plain,(~ (sk1) | (event @ sk9 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(35,plain,(~ (sk1) | (barrel @ sk9 @ sk10 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(14,plain,(~ (sk1) | (in @ sk9 @ sk8 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(40,plain,(~ (sk1) | (down @ sk9 @ sk11 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(15,plain,(~ (sk1) | (exists_in_world @ sk10 @ sk7)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(46,plain,(! [D:mu,C:mu,B:mu,A:mu] : (~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ B @ sk7)) | (~ (exists_in_world @ C @ sk7)) | (~ (exists_in_world @ D @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ B @ sk7)) | (~ (street @ C @ sk7)) | (~ (way @ C @ sk7)) | (~ (lonely @ C @ sk7)) | (~ (chevy @ D @ sk7)) | (~ (car @ D @ sk7)) | (~ (white @ D @ sk7)) | (~ (dirty @ D @ sk7)) | (~ (old @ D @ sk7)) | (~ (barrel @ B @ D @ sk7)) | (~ (down @ B @ C @ sk7)) | (~ (in @ B @ A @ sk7)))),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(48,plain,(! [D:mu,C:mu,B:mu,A:mu] : (~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ B @ sk7)) | (~ (exists_in_world @ C @ sk7)) | (~ (exists_in_world @ D @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ B @ sk7)) | (~ (street @ C @ sk7)) | (~ (way @ C @ sk7)) | (~ (lonely @ C @ sk7)) | (~ (chevy @ D @ sk7)) | (~ (car @ D @ sk7)) | (~ (white @ D @ sk7)) | (~ (dirty @ D @ sk7)) | (~ (old @ D @ sk7)) | (~ (barrel @ B @ D @ sk7)) | (~ (down @ B @ C @ sk7)) | (~ (in @ B @ A @ sk7)))),inference(simp,[status(thm)],[46])).
% 65.43/31.72 thf(127,plain,(! [D:mu,C:mu,B:mu,A:mu] : (~ (sk1) | ~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ B @ sk7)) | (~ (exists_in_world @ C @ sk7)) | ~ (($true)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ B @ sk7)) | (~ (street @ C @ sk7)) | (~ (way @ C @ sk7)) | (~ (lonely @ C @ sk7)) | (~ (chevy @ D @ sk7)) | (~ (car @ D @ sk7)) | (~ (white @ D @ sk7)) | (~ (dirty @ D @ sk7)) | (~ (old @ D @ sk7)) | (~ (barrel @ B @ D @ sk7)) | (~ (down @ B @ C @ sk7)) | (~ (in @ B @ A @ sk7)) | ((exists_in_world @ sk10 @ sk7) != (exists_in_world @ D @ sk7)))),inference(paramod_ordered,[status(thm)],[15,48])).
% 65.43/31.72 thf(128,plain,(! [D:mu,C:mu,B:mu,A:mu] : (~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ B @ sk7)) | (~ (exists_in_world @ C @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ B @ sk7)) | (~ (street @ C @ sk7)) | (~ (way @ C @ sk7)) | (~ (lonely @ C @ sk7)) | (~ (chevy @ D @ sk7)) | (~ (car @ D @ sk7)) | (~ (white @ D @ sk7)) | (~ (dirty @ D @ sk7)) | (~ (old @ D @ sk7)) | (~ (barrel @ B @ D @ sk7)) | (~ (down @ B @ C @ sk7)) | (~ (in @ B @ A @ sk7)) | ((exists_in_world @ sk10 @ sk7) != (exists_in_world @ D @ sk7)))),inference(simp,[status(thm)],[127])).
% 65.43/31.72 thf(129,plain,(! [C:mu,B:mu,A:mu] : (~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ B @ sk7)) | (~ (exists_in_world @ C @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ B @ sk7)) | (~ (street @ C @ sk7)) | (~ (way @ C @ sk7)) | (~ (lonely @ C @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | (~ (barrel @ B @ sk10 @ sk7)) | (~ (down @ B @ C @ sk7)) | (~ (in @ B @ A @ sk7)))),inference(pattern_uni,[status(thm)],[128:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk10))]])).
% 65.43/31.72 thf(6344,plain,(! [C:mu,B:mu,A:mu] : (~ (sk1) | ~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ B @ sk7)) | (~ (exists_in_world @ C @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ B @ sk7)) | (~ (street @ C @ sk7)) | (~ (way @ C @ sk7)) | (~ (lonely @ C @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | (~ (barrel @ B @ sk10 @ sk7)) | ~ (($true)) | (~ (in @ B @ A @ sk7)) | ((down @ sk9 @ sk11 @ sk7) != (down @ B @ C @ sk7)))),inference(paramod_ordered,[status(thm)],[40,129])).
% 65.43/31.72 thf(6345,plain,(! [C:mu,B:mu,A:mu] : (~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ B @ sk7)) | (~ (exists_in_world @ C @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ B @ sk7)) | (~ (street @ C @ sk7)) | (~ (way @ C @ sk7)) | (~ (lonely @ C @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | (~ (barrel @ B @ sk10 @ sk7)) | (~ (in @ B @ A @ sk7)) | ((down @ sk9 @ sk11 @ sk7) != (down @ B @ C @ sk7)))),inference(simp,[status(thm)],[6344])).
% 65.43/31.72 thf(6346,plain,(! [A:mu] : (~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ sk9 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | (~ (barrel @ sk9 @ sk10 @ sk7)) | (~ (in @ sk9 @ A @ sk7)))),inference(pattern_uni,[status(thm)],[6345:[bind(A, $thf(A)),bind(B, $thf(sk9)),bind(C, $thf(sk11))]])).
% 65.43/31.72 thf(38263,plain,(! [A:mu] : (~ (sk1) | ~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ sk9 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | (~ (barrel @ sk9 @ sk10 @ sk7)) | ~ (($true)) | ((in @ sk9 @ sk8 @ sk7) != (in @ sk9 @ A @ sk7)))),inference(paramod_ordered,[status(thm)],[14,6346])).
% 65.43/31.72 thf(38264,plain,(! [A:mu] : (~ (sk1) | (~ (exists_in_world @ A @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ A @ sk7)) | (~ (city @ A @ sk7)) | (~ (event @ sk9 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | (~ (barrel @ sk9 @ sk10 @ sk7)) | ((in @ sk9 @ sk8 @ sk7) != (in @ sk9 @ A @ sk7)))),inference(simp,[status(thm)],[38263])).
% 65.43/31.72 thf(38265,plain,(~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (event @ sk9 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | (~ (barrel @ sk9 @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[38264:[bind(A, $thf(sk8))]])).
% 65.43/31.72 thf(39886,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (event @ sk9 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ~ (($true)) | ((barrel @ sk9 @ sk10 @ sk7) != (barrel @ sk9 @ sk10 @ sk7))),inference(paramod_ordered,[status(thm)],[35,38265])).
% 65.43/31.72 thf(39887,plain,(~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (event @ sk9 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((barrel @ sk9 @ sk10 @ sk7) != (barrel @ sk9 @ sk10 @ sk7))),inference(simp,[status(thm)],[39886])).
% 65.43/31.72 thf(39888,plain,(~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (event @ sk9 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[39887:[]])).
% 65.43/31.72 thf(40042,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | ~ (($true)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((event @ sk9 @ sk7) != (event @ sk9 @ sk7))),inference(paramod_ordered,[status(thm)],[10,39888])).
% 65.43/31.72 thf(40043,plain,(~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((event @ sk9 @ sk7) != (event @ sk9 @ sk7))),inference(simp,[status(thm)],[40042])).
% 65.43/31.72 thf(40044,plain,(~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (car @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[40043:[]])).
% 65.43/31.72 thf(41762,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | ~ (($true)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((car @ sk10 @ sk7) != (car @ sk10 @ sk7))),inference(paramod_ordered,[status(thm)],[42,40044])).
% 65.43/31.72 thf(41763,plain,(~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((car @ sk10 @ sk7) != (car @ sk10 @ sk7))),inference(simp,[status(thm)],[41762])).
% 65.43/31.72 thf(41764,plain,(~ (sk1) | (~ (exists_in_world @ sk8 @ sk7)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[41763:[]])).
% 65.43/31.72 thf(42159,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((exists_in_world @ sk8 @ sk7) != (exists_in_world @ sk8 @ sk7))),inference(paramod_ordered,[status(thm)],[29,41764])).
% 65.43/31.72 thf(42160,plain,(~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((exists_in_world @ sk8 @ sk7) != (exists_in_world @ sk8 @ sk7))),inference(simp,[status(thm)],[42159])).
% 65.43/31.72 thf(42161,plain,(~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (city @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[42160:[]])).
% 65.43/31.72 thf(43320,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | ~ (($true)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((city @ sk8 @ sk7) != (city @ sk8 @ sk7))),inference(paramod_ordered,[status(thm)],[13,42161])).
% 65.43/31.72 thf(43321,plain,(~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((city @ sk8 @ sk7) != (city @ sk8 @ sk7))),inference(simp,[status(thm)],[43320])).
% 65.43/31.72 thf(43322,plain,(~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (dirty @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[43321:[]])).
% 65.43/31.72 thf(43577,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | ~ (($true)) | (~ (old @ sk10 @ sk7)) | ((dirty @ sk10 @ sk7) != (dirty @ sk10 @ sk7))),inference(paramod_ordered,[status(thm)],[17,43322])).
% 65.43/31.72 thf(43578,plain,(~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((dirty @ sk10 @ sk7) != (dirty @ sk10 @ sk7))),inference(simp,[status(thm)],[43577])).
% 65.43/31.72 thf(43579,plain,(~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (white @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[43578:[]])).
% 65.43/31.72 thf(44359,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | ~ (($true)) | (~ (old @ sk10 @ sk7)) | ((white @ sk10 @ sk7) != (white @ sk10 @ sk7))),inference(paramod_ordered,[status(thm)],[32,43579])).
% 65.43/31.72 thf(44360,plain,(~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((white @ sk10 @ sk7) != (white @ sk10 @ sk7))),inference(simp,[status(thm)],[44359])).
% 65.43/31.72 thf(44361,plain,(~ (sk1) | (~ (exists_in_world @ sk9 @ sk7)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[44360:[]])).
% 65.43/31.72 thf(44608,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((exists_in_world @ sk9 @ sk7) != (exists_in_world @ sk9 @ sk7))),inference(paramod_ordered,[status(thm)],[34,44361])).
% 65.43/31.72 thf(44609,plain,(~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((exists_in_world @ sk9 @ sk7) != (exists_in_world @ sk9 @ sk7))),inference(simp,[status(thm)],[44608])).
% 65.43/31.72 thf(44610,plain,(~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (way @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[44609:[]])).
% 65.43/31.72 thf(44810,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | ~ (($true)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((way @ sk11 @ sk7) != (way @ sk11 @ sk7))),inference(paramod_ordered,[status(thm)],[22,44610])).
% 65.43/31.72 thf(44811,plain,(~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((way @ sk11 @ sk7) != (way @ sk11 @ sk7))),inference(simp,[status(thm)],[44810])).
% 65.43/31.72 thf(44812,plain,(~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (chevy @ sk10 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[44811:[]])).
% 65.43/31.72 thf(44953,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | ~ (($true)) | (~ (old @ sk10 @ sk7)) | ((chevy @ sk10 @ sk7) != (chevy @ sk10 @ sk7))),inference(paramod_ordered,[status(thm)],[39,44812])).
% 65.43/31.72 thf(44954,plain,(~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((chevy @ sk10 @ sk7) != (chevy @ sk10 @ sk7))),inference(simp,[status(thm)],[44953])).
% 65.43/31.72 thf(44955,plain,(~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (lonely @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[44954:[]])).
% 65.43/31.72 thf(45091,plain,(~ (sk1) | ~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | ~ (($true)) | (~ (old @ sk10 @ sk7)) | ((lonely @ sk11 @ sk7) != (lonely @ sk11 @ sk7))),inference(paramod_ordered,[status(thm)],[31,44955])).
% 65.43/31.72 thf(45092,plain,(~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((lonely @ sk11 @ sk7) != (lonely @ sk11 @ sk7))),inference(simp,[status(thm)],[45091])).
% 65.43/31.72 thf(45093,plain,(~ (sk1) | (~ (exists_in_world @ sk11 @ sk7)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[45092:[]])).
% 65.43/31.72 thf(45220,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((exists_in_world @ sk11 @ sk7) != (exists_in_world @ sk11 @ sk7))),inference(paramod_ordered,[status(thm)],[43,45093])).
% 65.43/31.72 thf(45221,plain,(~ (sk1) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((exists_in_world @ sk11 @ sk7) != (exists_in_world @ sk11 @ sk7))),inference(simp,[status(thm)],[45220])).
% 65.43/31.72 thf(45222,plain,(~ (sk1) | (~ (hollywood @ sk8 @ sk7)) | (~ (street @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[45221:[]])).
% 65.43/31.72 thf(45700,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | (~ (street @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((hollywood @ sk8 @ sk7) != (hollywood @ sk8 @ sk7))),inference(paramod_ordered,[status(thm)],[26,45222])).
% 65.43/31.72 thf(45701,plain,(~ (sk1) | (~ (street @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7)) | ((hollywood @ sk8 @ sk7) != (hollywood @ sk8 @ sk7))),inference(simp,[status(thm)],[45700])).
% 65.43/31.72 thf(45702,plain,(~ (sk1) | (~ (street @ sk11 @ sk7)) | (~ (old @ sk10 @ sk7))),inference(pattern_uni,[status(thm)],[45701:[]])).
% 65.43/31.72 thf(45715,plain,(~ (sk1) | ~ (sk1) | (~ (street @ sk11 @ sk7)) | ~ (($true)) | ((old @ sk10 @ sk7) != (old @ sk10 @ sk7))),inference(paramod_ordered,[status(thm)],[23,45702])).
% 65.43/31.72 thf(45716,plain,(~ (sk1) | (~ (street @ sk11 @ sk7)) | ((old @ sk10 @ sk7) != (old @ sk10 @ sk7))),inference(simp,[status(thm)],[45715])).
% 65.43/31.72 thf(45717,plain,(~ (sk1) | (~ (street @ sk11 @ sk7))),inference(pattern_uni,[status(thm)],[45716:[]])).
% 65.43/31.72 thf(45723,plain,(~ (sk1) | ~ (sk1) | ~ (($true)) | ((street @ sk11 @ sk7) != (street @ sk11 @ sk7))),inference(paramod_ordered,[status(thm)],[36,45717])).
% 65.43/31.72 thf(45724,plain,(~ (sk1) | ((street @ sk11 @ sk7) != (street @ sk11 @ sk7))),inference(simp,[status(thm)],[45723])).
% 65.43/31.72 thf(45725,plain,(~ (sk1)),inference(pattern_uni,[status(thm)],[45724:[]])).
% 65.43/31.72 thf(45842,plain,((in @ sk4 @ sk3 @ sk2) | ($false)),inference(rewrite,[status(thm)],[19,45725])).
% 65.43/31.72 thf(45843,plain,((in @ sk4 @ sk3 @ sk2)),inference(simp,[status(thm)],[45842])).
% 65.43/31.72 thf(20,plain,((down @ sk4 @ sk5 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45744,plain,((down @ sk4 @ sk5 @ sk2) | ($false)),inference(rewrite,[status(thm)],[20,45725])).
% 65.43/31.72 thf(45745,plain,((down @ sk4 @ sk5 @ sk2)),inference(simp,[status(thm)],[45744])).
% 65.43/31.72 thf(37,plain,((barrel @ sk4 @ sk6 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(12,plain,(! [D:mu,C:mu,B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (event @ B @ sk2)) | (~ (chevy @ C @ sk2)) | (~ (car @ C @ sk2)) | (~ (white @ C @ sk2)) | (~ (dirty @ C @ sk2)) | (~ (old @ C @ sk2)) | (~ (street @ D @ sk2)) | (~ (way @ D @ sk2)) | (~ (lonely @ D @ sk2)) | (~ (barrel @ B @ C @ sk2)) | (~ (down @ B @ D @ sk2)) | (~ (in @ B @ A @ sk2)) | sk1)),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(1263,plain,(! [D:mu,C:mu,B:mu,A:mu] : (sk1 | (~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (event @ B @ sk2)) | (~ (chevy @ C @ sk2)) | (~ (car @ C @ sk2)) | (~ (white @ C @ sk2)) | (~ (dirty @ C @ sk2)) | (~ (old @ C @ sk2)) | (~ (street @ D @ sk2)) | (~ (way @ D @ sk2)) | (~ (lonely @ D @ sk2)) | ~ (($true)) | (~ (down @ B @ D @ sk2)) | (~ (in @ B @ A @ sk2)) | sk1 | ((barrel @ sk4 @ sk6 @ sk2) != (barrel @ B @ C @ sk2)))),inference(paramod_ordered,[status(thm)],[37,12])).
% 65.43/31.72 thf(1264,plain,(! [D:mu,C:mu,B:mu,A:mu] : (sk1 | (~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (exists_in_world @ C @ sk2)) | (~ (exists_in_world @ D @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (event @ B @ sk2)) | (~ (chevy @ C @ sk2)) | (~ (car @ C @ sk2)) | (~ (white @ C @ sk2)) | (~ (dirty @ C @ sk2)) | (~ (old @ C @ sk2)) | (~ (street @ D @ sk2)) | (~ (way @ D @ sk2)) | (~ (lonely @ D @ sk2)) | (~ (down @ B @ D @ sk2)) | (~ (in @ B @ A @ sk2)) | ((barrel @ sk4 @ sk6 @ sk2) != (barrel @ B @ C @ sk2)))),inference(simp,[status(thm)],[1263])).
% 65.43/31.72 thf(1265,plain,(! [B:mu,A:mu] : (sk1 | (~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ sk4 @ sk2)) | (~ (exists_in_world @ sk6 @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (event @ sk4 @ sk2)) | (~ (chevy @ sk6 @ sk2)) | (~ (car @ sk6 @ sk2)) | (~ (white @ sk6 @ sk2)) | (~ (dirty @ sk6 @ sk2)) | (~ (old @ sk6 @ sk2)) | (~ (street @ B @ sk2)) | (~ (way @ B @ sk2)) | (~ (lonely @ B @ sk2)) | (~ (down @ sk4 @ B @ sk2)) | (~ (in @ sk4 @ A @ sk2)))),inference(pattern_uni,[status(thm)],[1264:[bind(A, $thf(A)),bind(B, $thf(sk4)),bind(C, $thf(sk6))]])).
% 65.43/31.72 thf(1276,plain,(! [B:mu,A:mu] : (sk1 | (~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ sk4 @ sk2)) | (~ (exists_in_world @ sk6 @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (event @ sk4 @ sk2)) | (~ (chevy @ sk6 @ sk2)) | (~ (car @ sk6 @ sk2)) | (~ (white @ sk6 @ sk2)) | (~ (dirty @ sk6 @ sk2)) | (~ (old @ sk6 @ sk2)) | (~ (street @ B @ sk2)) | (~ (way @ B @ sk2)) | (~ (lonely @ B @ sk2)) | (~ (down @ sk4 @ B @ sk2)) | (~ (in @ sk4 @ A @ sk2)))),inference(simp,[status(thm)],[1265])).
% 65.43/31.72 thf(11,plain,((old @ sk6 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45826,plain,((old @ sk6 @ sk2) | ($false)),inference(rewrite,[status(thm)],[11,45725])).
% 65.43/31.72 thf(45827,plain,((old @ sk6 @ sk2)),inference(simp,[status(thm)],[45826])).
% 65.43/31.72 thf(18,plain,((dirty @ sk6 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45812,plain,((dirty @ sk6 @ sk2) | ($false)),inference(rewrite,[status(thm)],[18,45725])).
% 65.43/31.72 thf(45813,plain,((dirty @ sk6 @ sk2)),inference(simp,[status(thm)],[45812])).
% 65.43/31.72 thf(44,plain,((exists_in_world @ sk6 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45798,plain,((exists_in_world @ sk6 @ sk2) | ($false)),inference(rewrite,[status(thm)],[44,45725])).
% 65.43/31.72 thf(45799,plain,((exists_in_world @ sk6 @ sk2)),inference(simp,[status(thm)],[45798])).
% 65.43/31.72 thf(28,plain,((chevy @ sk6 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45768,plain,((chevy @ sk6 @ sk2) | ($false)),inference(rewrite,[status(thm)],[28,45725])).
% 65.43/31.72 thf(45769,plain,((chevy @ sk6 @ sk2)),inference(simp,[status(thm)],[45768])).
% 65.43/31.72 thf(27,plain,((car @ sk6 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45800,plain,((car @ sk6 @ sk2) | ($false)),inference(rewrite,[status(thm)],[27,45725])).
% 65.43/31.72 thf(45801,plain,((car @ sk6 @ sk2)),inference(simp,[status(thm)],[45800])).
% 65.43/31.72 thf(41,plain,((event @ sk4 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45786,plain,((event @ sk4 @ sk2) | ($false)),inference(rewrite,[status(thm)],[41,45725])).
% 65.43/31.72 thf(45787,plain,((event @ sk4 @ sk2)),inference(simp,[status(thm)],[45786])).
% 65.43/31.72 thf(16,plain,((white @ sk6 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45820,plain,((white @ sk6 @ sk2) | ($false)),inference(rewrite,[status(thm)],[16,45725])).
% 65.43/31.72 thf(45821,plain,((white @ sk6 @ sk2)),inference(simp,[status(thm)],[45820])).
% 65.43/31.72 thf(47,plain,((exists_in_world @ sk4 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45852,plain,((exists_in_world @ sk4 @ sk2) | ($false)),inference(rewrite,[status(thm)],[47,45725])).
% 65.43/31.72 thf(45853,plain,((exists_in_world @ sk4 @ sk2)),inference(simp,[status(thm)],[45852])).
% 65.43/31.72 thf(59894,plain,(! [B:mu,A:mu] : (($false) | (~ (exists_in_world @ A @ sk2)) | ~ (($true)) | ~ (($true)) | (~ (exists_in_world @ B @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (street @ B @ sk2)) | (~ (way @ B @ sk2)) | (~ (lonely @ B @ sk2)) | (~ (down @ sk4 @ B @ sk2)) | (~ (in @ sk4 @ A @ sk2)))),inference(rewrite,[status(thm)],[1276,45827,45813,45799,45769,45801,45787,45725,45821,45853])).
% 65.43/31.72 thf(59895,plain,(! [B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (street @ B @ sk2)) | (~ (way @ B @ sk2)) | (~ (lonely @ B @ sk2)) | (~ (down @ sk4 @ B @ sk2)) | (~ (in @ sk4 @ A @ sk2)))),inference(simp,[status(thm)],[59894])).
% 65.43/31.72 thf(60091,plain,(! [B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (street @ B @ sk2)) | (~ (way @ B @ sk2)) | (~ (lonely @ B @ sk2)) | ~ (($true)) | (~ (in @ sk4 @ A @ sk2)) | ((down @ sk4 @ sk5 @ sk2) != (down @ sk4 @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[45745,59895])).
% 65.43/31.72 thf(60092,plain,(! [B:mu,A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ B @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (street @ B @ sk2)) | (~ (way @ B @ sk2)) | (~ (lonely @ B @ sk2)) | (~ (in @ sk4 @ A @ sk2)) | ((down @ sk4 @ sk5 @ sk2) != (down @ sk4 @ B @ sk2)))),inference(simp,[status(thm)],[60091])).
% 65.43/31.72 thf(60093,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (exists_in_world @ sk5 @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (street @ sk5 @ sk2)) | (~ (way @ sk5 @ sk2)) | (~ (lonely @ sk5 @ sk2)) | (~ (in @ sk4 @ A @ sk2)))),inference(pattern_uni,[status(thm)],[60092:[bind(A, $thf(A)),bind(B, $thf(sk5))]])).
% 65.43/31.72 thf(21,plain,((lonely @ sk5 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45760,plain,((lonely @ sk5 @ sk2) | ($false)),inference(rewrite,[status(thm)],[21,45725])).
% 65.43/31.72 thf(45761,plain,((lonely @ sk5 @ sk2)),inference(simp,[status(thm)],[45760])).
% 65.43/31.72 thf(45,plain,((street @ sk5 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45794,plain,((street @ sk5 @ sk2) | ($false)),inference(rewrite,[status(thm)],[45,45725])).
% 65.43/31.72 thf(45795,plain,((street @ sk5 @ sk2)),inference(simp,[status(thm)],[45794])).
% 65.43/31.72 thf(24,plain,((way @ sk5 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45734,plain,((way @ sk5 @ sk2) | ($false)),inference(rewrite,[status(thm)],[24,45725])).
% 65.43/31.72 thf(45735,plain,((way @ sk5 @ sk2)),inference(simp,[status(thm)],[45734])).
% 65.43/31.72 thf(25,plain,((exists_in_world @ sk5 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45738,plain,((exists_in_world @ sk5 @ sk2) | ($false)),inference(rewrite,[status(thm)],[25,45725])).
% 65.43/31.72 thf(45739,plain,((exists_in_world @ sk5 @ sk2)),inference(simp,[status(thm)],[45738])).
% 65.43/31.72 thf(65295,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | ~ (($true)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | ~ (($true)) | ~ (($true)) | ~ (($true)) | (~ (in @ sk4 @ A @ sk2)))),inference(rewrite,[status(thm)],[60093,45761,45795,45735,45739])).
% 65.43/31.72 thf(65296,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | (~ (in @ sk4 @ A @ sk2)))),inference(simp,[status(thm)],[65295])).
% 65.43/31.72 thf(65304,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | ~ (($true)) | ((in @ sk4 @ sk3 @ sk2) != (in @ sk4 @ A @ sk2)))),inference(paramod_ordered,[status(thm)],[45843,65296])).
% 65.43/31.72 thf(65305,plain,(! [A:mu] : ((~ (exists_in_world @ A @ sk2)) | (~ (hollywood @ A @ sk2)) | (~ (city @ A @ sk2)) | ((in @ sk4 @ sk3 @ sk2) != (in @ sk4 @ A @ sk2)))),inference(simp,[status(thm)],[65304])).
% 65.43/31.72 thf(65306,plain,((~ (exists_in_world @ sk3 @ sk2)) | (~ (hollywood @ sk3 @ sk2)) | (~ (city @ sk3 @ sk2))),inference(pattern_uni,[status(thm)],[65305:[bind(A, $thf(sk3))]])).
% 65.43/31.72 thf(33,plain,((city @ sk3 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45766,plain,((city @ sk3 @ sk2) | ($false)),inference(rewrite,[status(thm)],[33,45725])).
% 65.43/31.72 thf(45767,plain,((city @ sk3 @ sk2)),inference(simp,[status(thm)],[45766])).
% 65.43/31.72 thf(38,plain,((exists_in_world @ sk3 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45770,plain,((exists_in_world @ sk3 @ sk2) | ($false)),inference(rewrite,[status(thm)],[38,45725])).
% 65.43/31.72 thf(45771,plain,((exists_in_world @ sk3 @ sk2)),inference(simp,[status(thm)],[45770])).
% 65.43/31.72 thf(30,plain,((hollywood @ sk3 @ sk2) | sk1),inference(cnfConj,[status(thm)],[9])).
% 65.43/31.72 thf(45838,plain,((hollywood @ sk3 @ sk2) | ($false)),inference(rewrite,[status(thm)],[30,45725])).
% 65.43/31.72 thf(45839,plain,((hollywood @ sk3 @ sk2)),inference(simp,[status(thm)],[45838])).
% 65.43/31.72 thf(65412,plain,(~ (($true)) | ~ (($true)) | ~ (($true))),inference(rewrite,[status(thm)],[65306,45767,45771,45839])).
% 65.43/31.72 thf(65413,plain,(($false)),inference(simp,[status(thm)],[65412])).
% 65.43/31.72 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 65.43/31.72 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------