%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NLP117+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n012.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 : Sat Jun 21 05:18:03 AM UTC 2025
% Result : Theorem 0.12s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : NLP117+1 : TPTP v9.0.0. Released v2.4.0.
% 0.10/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 23:44:40 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.38 % SZS status Theorem
% 0.12/0.38 % SZS output start Proof
% 0.12/0.38 tff(down_type, type, (
% 0.12/0.38 down: ( $i * $i * $i ) > $o)).
% 0.12/0.38 tff(tptp_fun_X1_6_type, type, (
% 0.12/0.38 tptp_fun_X1_6: $i)).
% 0.12/0.38 tff(agent_type, type, (
% 0.12/0.38 agent: ( $i * $i * $i ) > $o)).
% 0.12/0.38 tff(lonely_type, type, (
% 0.12/0.38 lonely: ( $i * $i ) > $o)).
% 0.12/0.38 tff(street_type, type, (
% 0.12/0.38 street: ( $i * $i ) > $o)).
% 0.12/0.38 tff(old_type, type, (
% 0.12/0.38 old: ( $i * $i ) > $o)).
% 0.12/0.38 tff(dirty_type, type, (
% 0.12/0.38 dirty: ( $i * $i ) > $o)).
% 0.12/0.38 tff(white_type, type, (
% 0.12/0.38 white: ( $i * $i ) > $o)).
% 0.12/0.38 tff(chevy_type, type, (
% 0.12/0.38 chevy: ( $i * $i ) > $o)).
% 0.12/0.38 tff(barrel_type, type, (
% 0.12/0.38 barrel: ( $i * $i ) > $o)).
% 0.12/0.38 tff(in_type, type, (
% 0.12/0.38 in: ( $i * $i * $i ) > $o)).
% 0.12/0.38 tff(placename_type, type, (
% 0.12/0.38 placename: ( $i * $i ) > $o)).
% 0.12/0.38 tff(event_type, type, (
% 0.12/0.38 event: ( $i * $i ) > $o)).
% 0.12/0.38 tff(present_type, type, (
% 0.12/0.38 present: ( $i * $i ) > $o)).
% 0.12/0.38 tff(hollywood_placename_type, type, (
% 0.12/0.38 hollywood_placename: ( $i * $i ) > $o)).
% 0.12/0.38 tff(city_type, type, (
% 0.12/0.38 city: ( $i * $i ) > $o)).
% 0.12/0.38 tff(of_type, type, (
% 0.12/0.38 of: ( $i * $i * $i ) > $o)).
% 0.12/0.38 tff(actual_world_type, type, (
% 0.12/0.38 actual_world: $i > $o)).
% 0.12/0.38 tff(tptp_fun_X2_11_type, type, (
% 0.12/0.38 tptp_fun_X2_11: $i)).
% 0.12/0.38 tff(tptp_fun_X6_7_type, type, (
% 0.12/0.38 tptp_fun_X6_7: $i)).
% 0.12/0.38 tff(tptp_fun_X4_9_type, type, (
% 0.12/0.38 tptp_fun_X4_9: $i)).
% 0.12/0.38 tff(tptp_fun_X5_8_type, type, (
% 0.12/0.38 tptp_fun_X5_8: $i)).
% 0.12/0.38 tff(tptp_fun_X3_10_type, type, (
% 0.12/0.38 tptp_fun_X3_10: $i)).
% 0.12/0.38 tff(tptp_fun_V_5_type, type, (
% 0.12/0.38 tptp_fun_V_5: $i)).
% 0.12/0.38 tff(tptp_fun_Z_1_type, type, (
% 0.12/0.38 tptp_fun_Z_1: $i)).
% 0.12/0.38 tff(tptp_fun_U_0_type, type, (
% 0.12/0.38 tptp_fun_U_0: $i)).
% 0.12/0.38 tff(tptp_fun_Y_2_type, type, (
% 0.12/0.38 tptp_fun_Y_2: $i)).
% 0.12/0.38 tff(tptp_fun_X_3_type, type, (
% 0.12/0.38 tptp_fun_X_3: $i)).
% 0.12/0.38 tff(tptp_fun_W_4_type, type, (
% 0.12/0.38 tptp_fun_W_4: $i)).
% 0.12/0.38 tff(1,assumption,(~((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))))), introduced(assumption)).
% 0.12/0.38 tff(2,plain,
% 0.12/0.38 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | ![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(3,plain,
% 0.12/0.38 (![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.12/0.38 tff(4,plain,
% 0.12/0.38 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | actual_world(U!0)),
% 0.12/0.38 inference(tautology,[status(thm)],[])).
% 0.12/0.38 tff(5,plain,
% 0.12/0.38 (actual_world(U!0)),
% 0.12/0.38 inference(unit_resolution,[status(thm)],[4, 1])).
% 0.12/0.38 tff(6,plain,
% 0.12/0.38 (((~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))) | ((~actual_world(U!0)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6))))) <=> ((~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))) | (~actual_world(U!0)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6))))),
% 0.12/0.38 inference(rewrite,[status(thm)],[])).
% 0.12/0.38 tff(7,plain,
% 0.12/0.38 ((~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))) | ((~actual_world(U!0)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6))))),
% 0.12/0.38 inference(quant_inst,[status(thm)],[])).
% 0.12/0.38 tff(8,plain,
% 0.12/0.38 ((~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))) | (~actual_world(U!0)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[7, 6])).
% 0.12/0.39 tff(9,plain,
% 0.12/0.39 (![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[8, 5, 3])).
% 0.12/0.39 tff(10,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | in(U!0, Z!1, V!5)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(11,plain,
% 0.12/0.39 (in(U!0, Z!1, V!5)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[10, 1])).
% 0.12/0.39 tff(12,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | down(U!0, Z!1, Y!2)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(13,plain,
% 0.12/0.39 (down(U!0, Z!1, Y!2)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[12, 1])).
% 0.12/0.39 tff(14,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | barrel(U!0, Z!1)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(15,plain,
% 0.12/0.39 (barrel(U!0, Z!1)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[14, 1])).
% 0.12/0.39 tff(16,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | present(U!0, Z!1)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(17,plain,
% 0.12/0.39 (present(U!0, Z!1)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[16, 1])).
% 0.12/0.39 tff(18,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | agent(U!0, Z!1, X!3)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(19,plain,
% 0.12/0.39 (agent(U!0, Z!1, X!3)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[18, 1])).
% 0.12/0.39 tff(20,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | event(U!0, Z!1)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(21,plain,
% 0.12/0.39 (event(U!0, Z!1)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[20, 1])).
% 0.12/0.39 tff(22,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | lonely(U!0, Y!2)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(23,plain,
% 0.12/0.39 (lonely(U!0, Y!2)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[22, 1])).
% 0.12/0.39 tff(24,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | street(U!0, Y!2)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(25,plain,
% 0.12/0.39 (street(U!0, Y!2)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[24, 1])).
% 0.12/0.39 tff(26,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | old(U!0, X!3)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(27,plain,
% 0.12/0.39 (old(U!0, X!3)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[26, 1])).
% 0.12/0.39 tff(28,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | dirty(U!0, X!3)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(29,plain,
% 0.12/0.39 (dirty(U!0, X!3)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[28, 1])).
% 0.12/0.39 tff(30,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | white(U!0, X!3)),
% 0.12/0.39 inference(tautology,[status(thm)],[])).
% 0.12/0.39 tff(31,plain,
% 0.12/0.39 (white(U!0, X!3)),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[30, 1])).
% 0.12/0.39 tff(32,plain,
% 0.12/0.39 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | chevy(U!0, X!3)),
% 0.12/0.40 inference(tautology,[status(thm)],[])).
% 0.12/0.40 tff(33,plain,
% 0.12/0.40 (chevy(U!0, X!3)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[32, 1])).
% 0.12/0.40 tff(34,plain,
% 0.12/0.40 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | placename(U!0, W!4)),
% 0.12/0.40 inference(tautology,[status(thm)],[])).
% 0.12/0.40 tff(35,plain,
% 0.12/0.40 (placename(U!0, W!4)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[34, 1])).
% 0.12/0.40 tff(36,plain,
% 0.12/0.40 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | hollywood_placename(U!0, W!4)),
% 0.12/0.40 inference(tautology,[status(thm)],[])).
% 0.12/0.40 tff(37,plain,
% 0.12/0.40 (hollywood_placename(U!0, W!4)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[36, 1])).
% 0.12/0.40 tff(38,plain,
% 0.12/0.40 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | city(U!0, V!5)),
% 0.12/0.40 inference(tautology,[status(thm)],[])).
% 0.12/0.40 tff(39,plain,
% 0.12/0.40 (city(U!0, V!5)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[38, 1])).
% 0.12/0.40 tff(40,plain,
% 0.12/0.40 (((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))) | of(U!0, W!4, V!5)),
% 0.12/0.40 inference(tautology,[status(thm)],[])).
% 0.12/0.40 tff(41,plain,
% 0.12/0.40 (of(U!0, W!4, V!5)),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[40, 1])).
% 0.12/0.40 tff(42,plain,
% 0.12/0.40 (((~![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))) | ((~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)))) <=> ((~![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(43,plain,
% 0.12/0.40 (((~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~present(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~event(U!0, Z!1)) | (~old(U!0, X!3)) | (~dirty(U!0, X!3)) | (~white(U!0, X!3)) | (~chevy(U!0, X!3)) | (~lonely(U!0, Y!2)) | (~street(U!0, Y!2)) | (~placename(U!0, W!4)) | (~in(U!0, Z!1, V!5)) | (~down(U!0, Z!1, Y!2)) | (~barrel(U!0, Z!1))) <=> ((~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(44,plain,
% 0.12/0.40 (((~![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))) | ((~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~present(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~event(U!0, Z!1)) | (~old(U!0, X!3)) | (~dirty(U!0, X!3)) | (~white(U!0, X!3)) | (~chevy(U!0, X!3)) | (~lonely(U!0, Y!2)) | (~street(U!0, Y!2)) | (~placename(U!0, W!4)) | (~in(U!0, Z!1, V!5)) | (~down(U!0, Z!1, Y!2)) | (~barrel(U!0, Z!1)))) <=> ((~![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))) | ((~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[43])).
% 0.20/0.41 tff(45,plain,
% 0.20/0.41 (((~![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))) | ((~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~present(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~event(U!0, Z!1)) | (~old(U!0, X!3)) | (~dirty(U!0, X!3)) | (~white(U!0, X!3)) | (~chevy(U!0, X!3)) | (~lonely(U!0, Y!2)) | (~street(U!0, Y!2)) | (~placename(U!0, W!4)) | (~in(U!0, Z!1, V!5)) | (~down(U!0, Z!1, Y!2)) | (~barrel(U!0, Z!1)))) <=> ((~![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)))),
% 0.20/0.41 inference(transitivity,[status(thm)],[44, 42])).
% 0.20/0.41 tff(46,plain,
% 0.20/0.41 ((~![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))) | ((~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~present(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~event(U!0, Z!1)) | (~old(U!0, X!3)) | (~dirty(U!0, X!3)) | (~white(U!0, X!3)) | (~chevy(U!0, X!3)) | (~lonely(U!0, Y!2)) | (~street(U!0, Y!2)) | (~placename(U!0, W!4)) | (~in(U!0, Z!1, V!5)) | (~down(U!0, Z!1, Y!2)) | (~barrel(U!0, Z!1)))),
% 0.20/0.41 inference(quant_inst,[status(thm)],[])).
% 0.20/0.41 tff(47,plain,
% 0.20/0.41 ((~![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(U!0, X3, X2)) | (~city(U!0, X2)) | (~hollywood_placename(U!0, X3)) | (~present(U!0, X6)) | (~agent(U!0, X6, X5)) | (~event(U!0, X6)) | (~old(U!0, X5)) | (~dirty(U!0, X5)) | (~white(U!0, X5)) | (~chevy(U!0, X5)) | (~lonely(U!0, X4)) | (~street(U!0, X4)) | (~placename(U!0, X3)) | (~in(U!0, X6, X2)) | (~down(U!0, X6, X4)) | (~barrel(U!0, X6)))) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.20/0.41 tff(48,plain,
% 0.20/0.41 ($false),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[47, 41, 39, 37, 35, 33, 31, 29, 27, 25, 23, 21, 19, 17, 15, 13, 11, 9])).
% 0.20/0.41 tff(49,plain,((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6)))))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.41 tff(50,plain,
% 0.20/0.41 (((~((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))))) | (~((~actual_world(X1!6)) | (~of(X1!6, X3!10, X2!11)) | (~city(X1!6, X2!11)) | (~hollywood_placename(X1!6, X3!10)) | (~placename(X1!6, X3!10)) | (~street(X1!6, X4!9)) | (~lonely(X1!6, X4!9)) | (~chevy(X1!6, X5!8)) | (~white(X1!6, X5!8)) | (~dirty(X1!6, X5!8)) | (~old(X1!6, X5!8)) | (~event(X1!6, X6!7)) | (~agent(X1!6, X6!7, X5!8)) | (~present(X1!6, X6!7)) | (~barrel(X1!6, X6!7)) | (~down(X1!6, X6!7, X4!9)) | (~in(X1!6, X6!7, X2!11)) | (~![U: $i] : ((~actual_world(U)) | ![V: $i, W: $i, X: $i, Y: $i, Z: $i] : ((~of(U, W, V)) | (~city(U, V)) | (~hollywood_placename(U, W)) | (~present(U, Z)) | (~event(U, Z)) | (~placename(U, W)) | (~in(U, Z, V)) | (~barrel(U, Z)) | (~chevy(U, X)) | (~white(U, X)) | (~dirty(U, X)) | (~old(U, X)) | (~street(U, Y)) | (~lonely(U, Y)) | (~agent(U, Z, X)) | (~down(U, Z, Y)))))))) <=> ((~((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))))) | (~((~actual_world(X1!6)) | (~of(X1!6, X3!10, X2!11)) | (~city(X1!6, X2!11)) | (~hollywood_placename(X1!6, X3!10)) | (~placename(X1!6, X3!10)) | (~street(X1!6, X4!9)) | (~lonely(X1!6, X4!9)) | (~chevy(X1!6, X5!8)) | (~white(X1!6, X5!8)) | (~dirty(X1!6, X5!8)) | (~old(X1!6, X5!8)) | (~event(X1!6, X6!7)) | (~agent(X1!6, X6!7, X5!8)) | (~present(X1!6, X6!7)) | (~barrel(X1!6, X6!7)) | (~down(X1!6, X6!7, X4!9)) | (~in(X1!6, X6!7, X2!11)) | (~![U: $i] : ((~actual_world(U)) | ![V: $i, W: $i, X: $i, Y: $i, Z: $i] : ((~of(U, W, V)) | (~city(U, V)) | (~hollywood_placename(U, W)) | (~present(U, Z)) | (~event(U, Z)) | (~placename(U, W)) | (~in(U, Z, V)) | (~barrel(U, Z)) | (~chevy(U, X)) | (~white(U, X)) | (~dirty(U, X)) | (~old(U, X)) | (~street(U, Y)) | (~lonely(U, Y)) | (~agent(U, Z, X)) | (~down(U, Z, Y))))))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(51,plain,
% 0.20/0.41 (((actual_world(U!0) & of(U!0, W!4, V!5) & city(U!0, V!5) & hollywood_placename(U!0, W!4) & placename(U!0, W!4) & chevy(U!0, X!3) & white(U!0, X!3) & dirty(U!0, X!3) & old(U!0, X!3) & street(U!0, Y!2) & lonely(U!0, Y!2) & event(U!0, Z!1) & agent(U!0, Z!1, X!3) & present(U!0, Z!1) & barrel(U!0, Z!1) & down(U!0, Z!1, Y!2) & in(U!0, Z!1, V!5) & ![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (~(of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2))))) | (actual_world(X1!6) & of(X1!6, X3!10, X2!11) & city(X1!6, X2!11) & hollywood_placename(X1!6, X3!10) & placename(X1!6, X3!10) & street(X1!6, X4!9) & lonely(X1!6, X4!9) & chevy(X1!6, X5!8) & white(X1!6, X5!8) & dirty(X1!6, X5!8) & old(X1!6, X5!8) & event(X1!6, X6!7) & agent(X1!6, X6!7, X5!8) & present(X1!6, X6!7) & barrel(X1!6, X6!7) & down(X1!6, X6!7, X4!9) & in(X1!6, X6!7, X2!11) & ![U: $i] : ((~actual_world(U)) | ![V: $i, W: $i, X: $i, Y: $i, Z: $i] : (~(of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))) <=> ((~((~actual_world(U!0)) | (~of(U!0, W!4, V!5)) | (~city(U!0, V!5)) | (~hollywood_placename(U!0, W!4)) | (~placename(U!0, W!4)) | (~chevy(U!0, X!3)) | (~white(U!0, X!3)) | (~dirty(U!0, X!3)) | (~old(U!0, X!3)) | (~street(U!0, Y!2)) | (~lonely(U!0, Y!2)) | (~event(U!0, Z!1)) | (~agent(U!0, Z!1, X!3)) | (~present(U!0, Z!1)) | (~barrel(U!0, Z!1)) | (~down(U!0, Z!1, Y!2)) | (~in(U!0, Z!1, V!5)) | (~![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : ((~of(X1, X3, X2)) | (~city(X1, X2)) | (~hollywood_placename(X1, X3)) | (~present(X1, X6)) | (~agent(X1, X6, X5)) | (~event(X1, X6)) | (~old(X1, X5)) | (~dirty(X1, X5)) | (~white(X1, X5)) | (~chevy(X1, X5)) | (~lonely(X1, X4)) | (~street(X1, X4)) | (~placename(X1, X3)) | (~in(X1, X6, X2)) | (~down(X1, X6, X4)) | (~barrel(X1, X6))))))) | (~((~actual_world(X1!6)) | (~of(X1!6, X3!10, X2!11)) | (~city(X1!6, X2!11)) | (~hollywood_placename(X1!6, X3!10)) | (~placename(X1!6, X3!10)) | (~street(X1!6, X4!9)) | (~lonely(X1!6, X4!9)) | (~chevy(X1!6, X5!8)) | (~white(X1!6, X5!8)) | (~dirty(X1!6, X5!8)) | (~old(X1!6, X5!8)) | (~event(X1!6, X6!7)) | (~agent(X1!6, X6!7, X5!8)) | (~present(X1!6, X6!7)) | (~barrel(X1!6, X6!7)) | (~down(X1!6, X6!7, X4!9)) | (~in(X1!6, X6!7, X2!11)) | (~![U: $i] : ((~actual_world(U)) | ![V: $i, W: $i, X: $i, Y: $i, Z: $i] : ((~of(U, W, V)) | (~city(U, V)) | (~hollywood_placename(U, W)) | (~present(U, Z)) | (~event(U, Z)) | (~placename(U, W)) | (~in(U, Z, V)) | (~barrel(U, Z)) | (~chevy(U, X)) | (~white(U, X)) | (~dirty(U, X)) | (~old(U, X)) | (~street(U, Y)) | (~lonely(U, Y)) | (~agent(U, Z, X)) | (~down(U, Z, Y))))))))),
% 0.20/0.42 inference(rewrite,[status(thm)],[])).
% 0.20/0.42 tff(52,plain,
% 0.20/0.42 ((((actual_world(U!0) & (of(U!0, W!4, V!5) & city(U!0, V!5) & hollywood_placename(U!0, W!4) & placename(U!0, W!4) & chevy(U!0, X!3) & white(U!0, X!3) & dirty(U!0, X!3) & old(U!0, X!3) & street(U!0, Y!2) & lonely(U!0, Y!2) & event(U!0, Z!1) & agent(U!0, Z!1, X!3) & present(U!0, Z!1) & barrel(U!0, Z!1) & down(U!0, Z!1, Y!2) & in(U!0, Z!1, V!5))) & ![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (~(of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2))))) | ((actual_world(X1!6) & (of(X1!6, X3!10, X2!11) & city(X1!6, X2!11) & hollywood_placename(X1!6, X3!10) & placename(X1!6, X3!10) & street(X1!6, X4!9) & lonely(X1!6, X4!9) & chevy(X1!6, X5!8) & white(X1!6, X5!8) & dirty(X1!6, X5!8) & old(X1!6, X5!8) & event(X1!6, X6!7) & agent(X1!6, X6!7, X5!8) & present(X1!6, X6!7) & barrel(X1!6, X6!7) & down(X1!6, X6!7, X4!9) & in(X1!6, X6!7, X2!11))) & ![U: $i] : ((~actual_world(U)) | ![V: $i, W: $i, X: $i, Y: $i, Z: $i] : (~(of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))) <=> ((actual_world(U!0) & of(U!0, W!4, V!5) & city(U!0, V!5) & hollywood_placename(U!0, W!4) & placename(U!0, W!4) & chevy(U!0, X!3) & white(U!0, X!3) & dirty(U!0, X!3) & old(U!0, X!3) & street(U!0, Y!2) & lonely(U!0, Y!2) & event(U!0, Z!1) & agent(U!0, Z!1, X!3) & present(U!0, Z!1) & barrel(U!0, Z!1) & down(U!0, Z!1, Y!2) & in(U!0, Z!1, V!5) & ![X1: $i] : ((~actual_world(X1)) | ![X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (~(of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2))))) | (actual_world(X1!6) & of(X1!6, X3!10, X2!11) & city(X1!6, X2!11) & hollywood_placename(X1!6, X3!10) & placename(X1!6, X3!10) & street(X1!6, X4!9) & lonely(X1!6, X4!9) & chevy(X1!6, X5!8) & white(X1!6, X5!8) & dirty(X1!6, X5!8) & old(X1!6, X5!8) & event(X1!6, X6!7) & agent(X1!6, X6!7, X5!8) & present(X1!6, X6!7) & barrel(X1!6, X6!7) & down(X1!6, X6!7, X4!9) & in(X1!6, X6!7, X2!11) & ![U: $i] : ((~actual_world(U)) | ![V: $i, W: $i, X: $i, Y: $i, Z: $i] : (~(of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V))))))),
% 0.20/0.42 inference(rewrite,[status(thm)],[])).
% 0.20/0.42 tff(53,plain,
% 0.20/0.42 (((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) <=> ((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2))))),
% 0.20/0.42 inference(rewrite,[status(thm)],[])).
% 0.20/0.42 tff(54,plain,
% 0.20/0.42 ((((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V))))) <=> (((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))),
% 0.20/0.42 inference(monotonicity,[status(thm)],[53])).
% 0.20/0.42 tff(55,plain,
% 0.20/0.42 ((~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))) <=> (~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V))))))),
% 0.20/0.42 inference(monotonicity,[status(thm)],[54])).
% 0.20/0.42 tff(56,plain,
% 0.20/0.42 ((~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))) <=> (~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V))))))),
% 0.20/0.42 inference(rewrite,[status(thm)],[])).
% 0.20/0.42 tff(57,plain,
% 0.20/0.42 ((~(~(~((?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (((((((((((((((of(U, W, V) & city(U, V)) & hollywood_placename(U, W)) & placename(U, W)) & chevy(U, X)) & white(U, X)) & dirty(U, X)) & old(U, X)) & street(U, Y)) & lonely(U, Y)) & event(U, Z)) & agent(U, Z, X)) & present(U, Z)) & barrel(U, Z)) & down(U, Z, Y)) & in(U, Z, V))) => ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (((((((((((((((of(X1, X3, X2) & city(X1, X2)) & hollywood_placename(X1, X3)) & placename(X1, X3)) & street(X1, X4)) & lonely(X1, X4)) & chevy(X1, X5)) & white(X1, X5)) & dirty(X1, X5)) & old(X1, X5)) & event(X1, X6)) & agent(X1, X6, X5)) & present(X1, X6)) & barrel(X1, X6)) & down(X1, X6, X4)) & in(X1, X6, X2)))) & (?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (((((((((((((((of(X1, X3, X2) & city(X1, X2)) & hollywood_placename(X1, X3)) & placename(X1, X3)) & street(X1, X4)) & lonely(X1, X4)) & chevy(X1, X5)) & white(X1, X5)) & dirty(X1, X5)) & old(X1, X5)) & event(X1, X6)) & agent(X1, X6, X5)) & present(X1, X6)) & barrel(X1, X6)) & down(X1, X6, X4)) & in(X1, X6, X2))) => ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (((((((((((((((of(U, W, V) & city(U, V)) & hollywood_placename(U, W)) & placename(U, W)) & chevy(U, X)) & white(U, X)) & dirty(U, X)) & old(U, X)) & street(U, Y)) & lonely(U, Y)) & event(U, Z)) & agent(U, Z, X)) & present(U, Z)) & barrel(U, Z)) & down(U, Z, Y)) & in(U, Z, V)))))))) <=> (~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V))))))),
% 0.20/0.43 inference(rewrite,[status(thm)],[])).
% 0.20/0.43 tff(58,axiom,(~(~(~((?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (((((((((((((((of(U, W, V) & city(U, V)) & hollywood_placename(U, W)) & placename(U, W)) & chevy(U, X)) & white(U, X)) & dirty(U, X)) & old(U, X)) & street(U, Y)) & lonely(U, Y)) & event(U, Z)) & agent(U, Z, X)) & present(U, Z)) & barrel(U, Z)) & down(U, Z, Y)) & in(U, Z, V))) => ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (((((((((((((((of(X1, X3, X2) & city(X1, X2)) & hollywood_placename(X1, X3)) & placename(X1, X3)) & street(X1, X4)) & lonely(X1, X4)) & chevy(X1, X5)) & white(X1, X5)) & dirty(X1, X5)) & old(X1, X5)) & event(X1, X6)) & agent(X1, X6, X5)) & present(X1, X6)) & barrel(X1, X6)) & down(X1, X6, X4)) & in(X1, X6, X2)))) & (?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (((((((((((((((of(X1, X3, X2) & city(X1, X2)) & hollywood_placename(X1, X3)) & placename(X1, X3)) & street(X1, X4)) & lonely(X1, X4)) & chevy(X1, X5)) & white(X1, X5)) & dirty(X1, X5)) & old(X1, X5)) & event(X1, X6)) & agent(X1, X6, X5)) & present(X1, X6)) & barrel(X1, X6)) & down(X1, X6, X4)) & in(X1, X6, X2))) => ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (((((((((((((((of(U, W, V) & city(U, V)) & hollywood_placename(U, W)) & placename(U, W)) & chevy(U, X)) & white(U, X)) & dirty(U, X)) & old(U, X)) & street(U, Y)) & lonely(U, Y)) & event(U, Z)) & agent(U, Z, X)) & present(U, Z)) & barrel(U, Z)) & down(U, Z, Y)) & in(U, Z, V)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','co1')).
% 0.20/0.43 tff(59,plain,
% 0.20/0.43 (~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.20/0.43 tff(60,plain,
% 0.20/0.43 (~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[59, 55])).
% 0.20/0.43 tff(61,plain,
% 0.20/0.43 (~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[60, 56])).
% 0.20/0.45 tff(62,plain,
% 0.20/0.45 (~(((~?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))) | ?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) & ((~?[X1: $i] : (actual_world(X1) & ?[X2: $i, X3: $i, X4: $i, X5: $i, X6: $i] : (of(X1, X3, X2) & city(X1, X2) & hollywood_placename(X1, X3) & placename(X1, X3) & street(X1, X4) & lonely(X1, X4) & chevy(X1, X5) & white(X1, X5) & dirty(X1, X5) & old(X1, X5) & event(X1, X6) & agent(X1, X6, X5) & present(X1, X6) & barrel(X1, X6) & down(X1, X6, X4) & in(X1, X6, X2)))) | ?[U: $i] : (actual_world(U) & ?[V: $i, W: $i, X: $i, Y: $i, Z: $i] : (of(U, W, V) & city(U, V) & hollywood_placename(U, W) & placename(U, W) & chevy(U, X) & white(U, X) & dirty(U, X) & old(U, X) & street(U, Y) & lonely(U, Y) & event(U, Z) & agent(U, Z, X) & present(U, Z) & barrel(U, Z) & down(U, Z, Y) & in(U, Z, V)))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[61, 55])).
% 0.20/0.45 unexpected number of arguments: (let ((a!1 (exists ((U $i))
% 0.20/0.45 (let ((a!1 (exists ((V $i) (W $i) (X $i) (Y $i) (Z $i))
% 0.20/0.45 (and (of U W V)
% 0.20/0.45 (city U V)
% 0.20/0.45 (hollywood_placename U W)
% 0.20/0.45 (placename U W)
% 0.20/0.45 (chevy U X)
% 0.20/0.45 (white U X)
% 0.20/0.45 (dirty U X)
% 0.20/0.45 (old U X)
% 0.20/0.45 (street U Y)
% 0.20/0.45 (lonely U Y)
% 0.20/0.45 (event U Z)
% 0.20/0.45 (agent U Z X)
% 0.20/0.45 (present U Z)
% 0.20/0.45 (barrel U Z)
% 0.20/0.45 (down U Z Y)
% 0.20/0.45 (in U Z V)))))
% 0.20/0.45 (and (actual_world U) a!1))))
% 0.20/0.45 (a!2 (exists ((V $i) (W $i) (X $i) (Y $i) (Z $i))
% 0.20/0.45 (and (of U!0 W V)
% 0.20/0.45 (city U!0 V)
% 0.20/0.45 (hollywood_placename U!0 W)
% 0.20/0.45 (placename U!0 W)
% 0.20/0.45 (chevy U!0 X)
% 0.20/0.45 (white U!0 X)
% 0.20/0.45 (dirty U!0 X)
% 0.20/0.45 (old U!0 X)
% 0.20/0.45 (street U!0 Y)
% 0.20/0.45 (lonely U!0 Y)
% 0.20/0.45 (event U!0 Z)
% 0.20/0.45 (agent U!0 Z X)
% 0.20/0.45 (present U!0 Z)
% 0.20/0.45 (barrel U!0 Z)
% 0.20/0.45 (down U!0 Z Y)
% 0.20/0.45 (in U!0 Z V))))
% 0.20/0.45 (a!4 (and (of U!0 W!4 V!5)
% 0.20/0.45 (city U!0 V!5)
% 0.20/0.45 (hollywood_placename U!0 W!4)
% 0.20/0.45 (placename U!0 W!4)
% 0.20/0.45 (chevy U!0 X!3)
% 0.20/0.45 (white U!0 X!3)
% 0.20/0.45 (dirty U!0 X!3)
% 0.20/0.45 (old U!0 X!3)
% 0.20/0.45 (street U!0 Y!2)
% 0.20/0.45 (lonely U!0 Y!2)
% 0.20/0.45 (event U!0 Z!1)
% 0.20/0.45 (agent U!0 Z!1 X!3)
% 0.20/0.45 (present U!0 Z!1)
% 0.20/0.45 (barrel U!0 Z!1)
% 0.20/0.45 (down U!0 Z!1 Y!2)
% 0.20/0.45 (in U!0 Z!1 V!5)))
% 0.20/0.45 (a!8 (lambda ((X1 $i))
% 0.20/0.45 (let ((a!1 (refl (~ (not (actual_world X1))
% 0.20/0.45 (not (actual_world X1)))))
% 0.20/0.45 (a!2 (lambda ((X2 $i) (X3 $i) (X4 $i) (X5 $i) (X6 $i))
% 0.20/0.45 (let ((a!1 (and (of X1 X3 X2)
% 0.20/0.45 (city X1 X2)
% 0.20/0.45 (hollywood_placename X1 X3)
% 0.20/0.45 (placename X1 X3)
% 0.20/0.45 (street X1 X4)
% 0.20/0.45 (lonely X1 X4)
% 0.20/0.45 (chevy X1 X5)
% 0.20/0.45 (white X1 X5)
% 0.20/0.45 (dirty X1 X5)
% 0.20/0.45 (old X1 X5)
% 0.20/0.45 (event X1 X6)
% 0.20/0.45 (agent X1 X6 X5)
% 0.20/0.45 (present X1 X6)
% 0.20/0.45 (barrel X1 X6)
% 0.20/0.45 (down X1 X6 X4)
% 0.20/0.45 (in X1 X6 X2))))
% 0.20/0.45 (refl (~ (not a!1) (not a!1))))))
% 0.20/0.45 (a!3 (exists ((X2 $i) (X3 $i) (X4 $i) (X5 $i) (X6 $i))
% 0.20/0.45 (and (of X1 X3 X2)
% 0.20/0.45 (city X1 X2)
% 0.20/0.45 (hollywood_placename X1 X3)
% 0.20/0.45 (placename X1 X3)
% 0.20/0.45 (street X1 X4)
% 0.20/0.45 (lonely X1 X4)
% 0.20/0.45 (chevy X1 X5)
% 0.20/0.45 (white X1 X5)
% 0.20/0.45 (dirty X1 X5)
% 0.20/0.45 (old X1 X5)
% 0.20/0.45 (event X1 X6)
% 0.20/0.45 (agent X1 X6 X5)
% 0.20/0.45 (present X1 X6)
% 0.20/0.45 (barrel X1 X6)
% 0.20/0.45 (down X1 X6 X4)
% 0.20/0.45 (in X1 X6 X2))))
% 0.20/0.45 (a!4 (forall ((X2 $i) (X3 $i) (X4 $i) (X5 $i) (X6 $i))
% 0.20/0.45 (let ((a!1 (and (of X1 X3 X2)
% 0.20/0.45 (city X1 X2)
% 0.20/0.45 (hollywood_placename X1 X3)
% 0.20/0.45 (placename X1 X3)
% 0.20/0.45 (street X1 X4)
% 0.20/0.45 (lonely X1 X4)
% 0.20/0.45 (chevy X1 X5)
% 0.20/0.45 (white X1 X5)
% 0.20/0.45 (dirty X1 X5)
% 0.20/0.45 (old X1 X5)
% 0.20/0.45 (event X1 X6)
% 0.20/0.45 (agent X1 X6 X5)
% 0.20/0.45 (present X1 X6)
% 0.20/0.45 (barrel X1 X6)
% 0.20/0.45 (down X1 X6 X4)
% 0.20/0.45 (in X1 X6 X2))))
% 0.20/0.45 (not a!1)))))
% 0.20/0.45 (let ((a!5 (~ (not (and (actual_world X1) a!3))
% 0.20/0.45 (or (not (actual_world X1)) a!4))))
% 0.20/0.45 (nnf-neg a!1 (nnf-neg (proof-bind a!2) (~ (not a!3) a!4)) a!5)))))
% 0.20/0.45 (a!9 (exists ((X1 $i))
% 0.20/0.45 (let ((a!1 (exists ((X2 $i) (X3 $i) (X4 $i) (X5 $i) (X6 $i))
% 0.20/0.45 (and (of X1 X3 X2)
% 0.20/0.45 (city X1 X2)
% 0.20/0.45 (hollywood_placename X1 X3)
% 0.20/0.45 (placename X1 X3)
% 0.20/0.45 (street X1 X4)
% 0.20/0.45 (lonely X1 X4)
% 0.20/0.45 (chevy X1 X5)
% 0.20/0.45 (white X1 X5)
% 0.20/0.45 (dirty X1 X5)
% 0.20/0.45 (old X1 X5)
% 0.20/0.45 (event X1 X6)
% 0.20/0.45 (agent X1 X6 X5)
% 0.20/0.45 (present X1 X6)
% 0.20/0.45 (barrel X1 X6)
% 0.20/0.45 (down X1 X6 X4)
% 0.20/0.45 (in X1 X6 X2)))))
% 0.20/0.45 (and (actual_world X1) a!1))))
% 0.20/0.45 (a!10 (forall ((X1 $i))
% 0.20/0.45 (let ((a!1 (forall ((X2 $i) (X3 $i) (X4 $i) (X5 $i) (X6 $i))
% 0.20/0.45 (let ((a!1 (and (of X1 X3 X2)
% 0.20/0.45 (city X1 X2)
% 0.20/0.45 (hollywood_placename X1 X3)
% 0.20/0.45 (placename X1 X3)
% 0.20/0.45 (street X1 X4)
% 0.20/0.45 (lonely X1 X4)
% 0.20/0.45 (chevy X1 X5)
% 0.20/0.45 (white X1 X5)
% 0.20/0.45 (dirty X1 X5)
% 0.20/0.45 (old X1 X5)
% 0.20/0.45 (event X1 X6)
% 0.20/0.45 (agent X1 X6 X5)
% 0.20/0.45 (present X1 X6)
% 0.20/0.45 (barrel X1 X6)
% 0.20/0.45 (down X1 X6 X4)
% 0.20/0.45 (in X1 X6 X2))))
% 0.20/0.45 (not a!1)))))
% 0.20/0.45 (or (not (actual_world X1)) a!1))))
% 0.20/0.45 (a!13 (exists ((X2 $i) (X3 $i) (X4 $i) (X5 $i) (X6 $i))
% 0.20/0.45 (and (of X1!6 X3 X2)
% 0.20/0.45 (city X1!6 X2)
% 0.20/0.45 (hollywood_placename X1!6 X3)
% 0.20/0.45 (placename X1!6 X3)
% 0.20/0.45 (street X1!6 X4)
% 0.20/0.45 (lonely X1!6 X4)
% 0.20/0.45 (chevy X1!6 X5)
% 0.20/0.45 (white X1!6 X5)
% 0.20/0.45 (dirty X1!6 X5)
% 0.20/0.45 (old X1!6 X5)
% 0.20/0.45 (event X1!6 X6)
% 0.20/0.45 (agent X1!6 X6 X5)
% 0.20/0.45 (present X1!6 X6)
% 0.20/0.45 (barrel X1!6 X6)
% 0.20/0.45 (down X1!6 X6 X4)
% 0.20/0.45 (in X1!6 X6 X2))))
% 0.20/0.45 (a!15 (and (of X1!6 X3!10 X2!11)
% 0.20/0.45 (city X1!6 X2!11)
% 0.20/0.45 (hollywood_placename X1!6 X3!10)
% 0.20/0.45 (placename X1!6 X3!10)
% 0.20/0.45 (street X1!6 X4!9)
% 0.20/0.45 (lonely X1!6 X4!9)
% 0.20/0.45 (chevy X1!6 X5!8)
% 0.20/0.45 (white X1!6 X5!8)
% 0.20/0.45 (dirty X1!6 X5!8)
% 0.20/0.45 (old X1!6 X5!8)
% 0.20/0.45 (event X1!6 X6!7)
% 0.20/0.45 (agent X1!6 X6!7 X5!8)
% 0.20/0.45 (present X1!6 X6!7)
% 0.20/0.45 (barrel X1!6 X6!7)
% 0.20/0.45 (down X1!6 X6!7 X4!9)
% 0.20/0.45 (in X1!6 X6!7 X2!11)))
% 0.20/0.45 (a!19 (lambda ((U $i))
% 0.20/0.45 (let ((a!1 (refl (~ (not (actual_world U)) (not (actual_world U)))))
% 0.20/0.45 (a!2 (lambda ((V $i) (W $i) (X $i) (Y $i) (Z $i))
% 0.20/0.45 (let ((a!1 (and (of U W V)
% 0.20/0.45 (city U V)
% 0.20/0.45 (hollywood_placename U W)
% 0.20/0.45 (placename U W)
% 0.20/0.45 (chevy U X)
% 0.20/0.45 (white U X)
% 0.20/0.45 (dirty U X)
% 0.20/0.45 (old U X)
% 0.20/0.45 (street U Y)
% 0.20/0.45 (lonely U Y)
% 0.20/0.45 (event U Z)
% 0.20/0.45 (agent U Z X)
% 0.20/0.45 (present U Z)
% 0.20/0.45 (barrel U Z)
% 0.20/0.45 (down U Z Y)
% 0.20/0.45 (in U Z V))))
% 0.20/0.45 (refl (~ (not a!1) (not a!1))))))
% 0.20/0.45 (a!3 (exists ((V $i) (W $i) (X $i) (Y $i) (Z $i))
% 0.20/0.45 (and (of U W V)
% 0.20/0.45 (city U V)
% 0.20/0.45 (hollywood_placename U W)
% 0.20/0.45 (placename U W)
% 0.20/0.45 (chevy U X)
% 0.20/0.45 (white U X)
% 0.20/0.45 (dirty U X)
% 0.20/0.45 (old U X)
% 0.20/0.45 (street U Y)
% 0.20/0.45 (lonely U Y)
% 0.20/0.45 (event U Z)
% 0.20/0.45 (agent U Z X)
% 0.20/0.45 (present U Z)
% 0.20/0.45 (barrel U Z)
% 0.20/0.45 (down U Z Y)
% 0.20/0.45 (in U Z V))))
% 0.20/0.45 (a!4 (forall ((V $i) (W $i) (X $i) (Y $i) (Z $i))
% 0.20/0.45 (let ((a!1 (and (of U W V)
% 0.20/0.45 (city U V)
% 0.20/0.45 (hollywood_placename U W)
% 0.20/0.45 (placename U W)
% 0.20/0.45 (chevy U X)
% 0.20/0.45 (white U X)
% 0.20/0.45 (dirty U X)
% 0.20/0.45 (old U X)
% 0.20/0.45 (street U Y)
% 0.20/0.45 (lonely U Y)
% 0.20/0.45 (event U Z)
% 0.20/0.45 (agent U Z X)
% 0.20/0.45 (present U Z)
% 0.20/0.45 (barrel U Z)
% 0.20/0.45 (down U Z Y)
% 0.20/0.45 (in U Z V))))
% 0.20/0.45 (not a!1)))))
% 0.20/0.45 (let ((a!5 (~ (not (and (actual_world U) a!3))
% 0.20/0.45 (or (not (actual_world U)) a!4))))
% 0.20/0.45 (nnf-neg a!1 (nnf-neg (proof-bind a!2) (~ (not a!3) a!4)) a!5)))))
% 0.20/0.45 (a!20 (forall ((U $i))
% 0.20/0.45 (let ((a!1 (forall ((V $i) (W $i) (X $i) (Y $i) (Z $i))
% 0.20/0.45 (let ((a!1 (and (of U W V)
% 0.20/0.45 (city U V)
% 0.20/0.45 (hollywood_placename U W)
% 0.20/0.45 (placename U W)
% 0.20/0.45 (chevy U X)
% 0.20/0.45 (white U X)
% 0.20/0.45 (dirty U X)
% 0.20/0.45 (old U X)
% 0.20/0.45 (street U Y)
% 0.20/0.45 (lonely U Y)
% 0.20/0.45 (event U Z)
% 0.20/0.45 (agent U Z X)
% 0.20/0.45 (present U Z)
% 0.20/0.45 (barrel U Z)
% 0.20/0.45 (down U Z Y)
% 0.20/0.45 (in U Z V))))
% 0.20/0.45 (not a!1)))))
% 0.20/0.45 (or (not (actual_world U)) a!1)))))
% 0.20/0.45 (let ((a!3 (sk (~ a!1 (and (actual_world U!0) a!2))))
% 0.20/0.45 (a!5 (monotonicity (refl (~ (actual_world U!0) (actual_world U!0)))
% 0.20/0.45 (sk (~ a!2 a!4))
% 0.20/0.45 (~ (and (actual_world U!0) a!2)
% 0.20/0.45 (and (actual_world U!0) a!4))))
% 0.20/0.45 (a!11 (~ (not (or (not a!1) a!9)) (and (and (actual_world U!0) a!4) a!10)))
% 0.20/0.45 (a!14 (sk (~ a!9 (and (actual_world X1!6) a!13))))
% 0.20/0.45 (a!16 (monotonicity (refl (~ (actual_world X1!6) (actual_world X1!6)))
% 0.20/0.45 (sk (~ a!13 a!15))
% 0.20/0.45 (~ (and (actual_world X1!6) a!13)
% 0.20/0.45 (and (actual_world X1!6) a!15))))
% 0.20/0.45 (a!21 (~ (not (or (not a!9) a!1))
% 0.20/0.45 (and (and (actual_world X1!6) a!15) a!20)))
% 0.20/0.45 (a!23 (not (and (or (not a!1) a!9) (or (not a!9) a!1))))
% 0.20/0.45 (a!24 (or (and (and (actual_world U!0) a!4) a!10)
% 0.20/0.45 (and (and (actual_world X1!6) a!15) a!20))))
% 0.20/0.45 (let ((a!6 (trans a!3 a!5 (~ a!1 (and (actual_world U!0) a!4))))
% 0.20/0.45 (a!17 (trans a!14 a!16 (~ a!9 (and (actual_world X1!6) a!15)))))
% 0.20/0.45 (let ((a!7 (nnf-neg a!6 (~ (not (not a!1)) (and (actual_world U!0) a!4))))
% 0.20/0.45 (a!18 (nnf-neg a!17 (~ (not (not a!9)) (and (actual_world X1!6) a!15)))))
% 0.20/0.45 (let ((a!12 (nnf-neg a!7 (nnf-neg (proof-bind a!8) (~ (not a!9) a!10)) a!11))
% 0.20/0.45 (a!22 (nnf-neg a!18 (nnf-neg (proof-bind a!19) (~ (not a!1) a!20)) a!21)))
% 0.20/0.45 (nnf-neg a!12 a!22 (~ a!23 a!24)))))))
% 0.20/0.45 Proof display could not be completed: unexpected number of arguments
% 0.20/0.46 % E exiting
%------------------------------------------------------------------------------