%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NLP094+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n015.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:17:58 AM UTC 2025
% Result : Theorem 0.17s 0.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NLP094+1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.11 % Command : run_E %s %d THM
% 0.10/0.31 % Computer : n015.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Thu Jun 19 23:45:10 EDT 2025
% 0.10/0.31 % CPUTime :
% 0.17/0.35 % SZS status Theorem
% 0.17/0.35 % SZS output start Proof
% 0.17/0.35 tff(see_type, type, (
% 0.17/0.35 see: ( $i * $i ) > $o)).
% 0.17/0.35 tff(tptp_fun_X8_8_type, type, (
% 0.17/0.35 tptp_fun_X8_8: $i > $i)).
% 0.17/0.35 tff(tptp_fun_V_13_type, type, (
% 0.17/0.35 tptp_fun_V_13: $i > $i)).
% 0.17/0.35 tff(tptp_fun_X2_7_type, type, (
% 0.17/0.35 tptp_fun_X2_7: $i)).
% 0.17/0.35 tff(nonreflexive_type, type, (
% 0.17/0.35 nonreflexive: ( $i * $i ) > $o)).
% 0.17/0.35 tff(past_type, type, (
% 0.17/0.35 past: ( $i * $i ) > $o)).
% 0.17/0.35 tff(patient_type, type, (
% 0.17/0.35 patient: ( $i * $i * $i ) > $o)).
% 0.17/0.35 tff(tptp_fun_X6_10_type, type, (
% 0.17/0.35 tptp_fun_X6_10: $i > $i)).
% 0.17/0.35 tff(agent_type, type, (
% 0.17/0.35 agent: ( $i * $i * $i ) > $o)).
% 0.17/0.35 tff(event_type, type, (
% 0.17/0.35 event: ( $i * $i ) > $o)).
% 0.17/0.35 tff(drink_type, type, (
% 0.17/0.35 drink: ( $i * $i ) > $o)).
% 0.17/0.35 tff(tptp_fun_X7_9_type, type, (
% 0.17/0.35 tptp_fun_X7_9: $i > $i)).
% 0.17/0.35 tff(tptp_fun_X5_11_type, type, (
% 0.17/0.35 tptp_fun_X5_11: $i > $i)).
% 0.17/0.35 tff(human_person_type, type, (
% 0.17/0.35 human_person: ( $i * $i ) > $o)).
% 0.17/0.35 tff(coffee_type, type, (
% 0.17/0.35 coffee: ( $i * $i ) > $o)).
% 0.17/0.35 tff(in_type, type, (
% 0.17/0.35 in: ( $i * $i * $i ) > $o)).
% 0.17/0.35 tff(tptp_fun_W_12_type, type, (
% 0.17/0.35 tptp_fun_W_12: $i > $i)).
% 0.17/0.36 tff(restaurant_type, type, (
% 0.17/0.36 restaurant: ( $i * $i ) > $o)).
% 0.17/0.36 tff(customer_type, type, (
% 0.17/0.36 customer: ( $i * $i ) > $o)).
% 0.17/0.36 tff(actual_world_type, type, (
% 0.17/0.36 actual_world: $i > $o)).
% 0.17/0.36 tff(tptp_fun_X3_6_type, type, (
% 0.17/0.36 tptp_fun_X3_6: $i > $i)).
% 0.17/0.36 tff(tptp_fun_X4_5_type, type, (
% 0.17/0.36 tptp_fun_X4_5: $i > $i)).
% 0.17/0.36 tff(tptp_fun_U_0_type, type, (
% 0.17/0.36 tptp_fun_U_0: $i)).
% 0.17/0.36 tff(tptp_fun_X_4_type, type, (
% 0.17/0.36 tptp_fun_X_4: $i > $i)).
% 0.17/0.36 tff(tptp_fun_X1_1_type, type, (
% 0.17/0.36 tptp_fun_X1_1: $i > $i)).
% 0.17/0.36 tff(tptp_fun_Z_2_type, type, (
% 0.17/0.36 tptp_fun_Z_2: $i > $i)).
% 0.17/0.36 tff(tptp_fun_Y_3_type, type, (
% 0.17/0.36 tptp_fun_Y_3: $i > $i)).
% 0.17/0.36 tff(1,assumption,(~((~actual_world(U!0)) | (~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))))), introduced(assumption)).
% 0.17/0.36 tff(2,plain,
% 0.17/0.36 (((~actual_world(U!0)) | (~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8))))))))) | ![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))),
% 0.17/0.36 inference(tautology,[status(thm)],[])).
% 0.17/0.36 tff(3,plain,
% 0.17/0.36 (![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.17/0.36 tff(4,plain,
% 0.17/0.36 (((~actual_world(U!0)) | (~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8))))))))) | actual_world(U!0)),
% 0.17/0.36 inference(tautology,[status(thm)],[])).
% 0.17/0.36 tff(5,plain,
% 0.17/0.36 (actual_world(U!0)),
% 0.17/0.36 inference(unit_resolution,[status(thm)],[4, 1])).
% 0.17/0.36 tff(6,plain,
% 0.17/0.36 (((~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))) | ((~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))))))) <=> ((~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))) | (~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))))))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(7,plain,
% 0.17/0.36 (((~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~past(U!0, X8)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8))))))) <=> ((~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))))))),
% 0.17/0.36 inference(rewrite,[status(thm)],[])).
% 0.17/0.36 tff(8,plain,
% 0.17/0.36 (((~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))) | ((~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~past(U!0, X8)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))))))) <=> ((~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))) | ((~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8))))))))),
% 0.17/0.36 inference(monotonicity,[status(thm)],[7])).
% 0.17/0.36 tff(9,plain,
% 0.17/0.36 (((~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))) | ((~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~past(U!0, X8)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))))))) <=> ((~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))) | (~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))))))),
% 0.17/0.36 inference(transitivity,[status(thm)],[8, 6])).
% 0.17/0.36 tff(10,plain,
% 0.17/0.36 ((~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))) | ((~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~past(U!0, X8)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))))))),
% 0.17/0.36 inference(quant_inst,[status(thm)],[])).
% 0.17/0.36 tff(11,plain,
% 0.17/0.36 ((~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))) | (~actual_world(U!0)) | (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8))))))),
% 0.17/0.37 inference(modus_ponens,[status(thm)],[10, 9])).
% 0.17/0.37 tff(12,plain,
% 0.17/0.37 (~((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[11, 5, 3])).
% 0.17/0.37 tff(13,plain,
% 0.17/0.37 (((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8))))) | in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(14,plain,
% 0.17/0.37 (in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[13, 12])).
% 0.17/0.37 tff(15,plain,
% 0.17/0.37 (((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8))))) | restaurant(U!0, tptp_fun_X4_5(U!0))),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(16,plain,
% 0.17/0.37 (restaurant(U!0, tptp_fun_X4_5(U!0))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[15, 12])).
% 0.17/0.37 tff(17,plain,
% 0.17/0.37 (((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8))))) | customer(U!0, tptp_fun_X3_6(U!0))),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(18,plain,
% 0.17/0.37 (customer(U!0, tptp_fun_X3_6(U!0))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[17, 12])).
% 0.17/0.37 tff(19,plain,
% 0.17/0.37 (((~actual_world(U!0)) | (~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8))))))))) | ![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))),
% 0.17/0.37 inference(tautology,[status(thm)],[])).
% 0.17/0.37 tff(20,plain,
% 0.17/0.37 (![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))),
% 0.17/0.37 inference(unit_resolution,[status(thm)],[19, 1])).
% 0.17/0.37 tff(21,plain,
% 0.17/0.37 (((~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | ((~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))))) <=> ((~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))))),
% 0.17/0.37 inference(rewrite,[status(thm)],[])).
% 0.17/0.37 tff(22,plain,
% 0.17/0.37 (((~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0)))) <=> ((~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))))),
% 0.17/0.37 inference(rewrite,[status(thm)],[])).
% 0.17/0.37 tff(23,plain,
% 0.17/0.37 ((~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) <=> (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))))),
% 0.17/0.38 inference(rewrite,[status(thm)],[])).
% 0.17/0.38 tff(24,plain,
% 0.17/0.38 (((~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0)))) <=> ((~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))))),
% 0.17/0.38 inference(monotonicity,[status(thm)],[23])).
% 0.17/0.38 tff(25,plain,
% 0.17/0.38 (((~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0)))) <=> ((~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))))),
% 0.17/0.38 inference(transitivity,[status(thm)],[24, 22])).
% 0.17/0.38 tff(26,plain,
% 0.17/0.38 (((~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | ((~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))))) <=> ((~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | ((~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))))))),
% 0.17/0.38 inference(monotonicity,[status(thm)],[25])).
% 0.17/0.38 tff(27,plain,
% 0.17/0.38 (((~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | ((~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))))) <=> ((~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))))),
% 0.17/0.38 inference(transitivity,[status(thm)],[26, 21])).
% 0.17/0.38 tff(28,plain,
% 0.17/0.38 ((~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | ((~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))))),
% 0.17/0.39 inference(quant_inst,[status(thm)],[])).
% 0.17/0.39 tff(29,plain,
% 0.17/0.39 ((~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~customer(U!0, tptp_fun_X3_6(U!0))) | (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))))),
% 0.17/0.39 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.17/0.39 tff(30,plain,
% 0.17/0.39 (~((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[29, 20, 18, 16, 14])).
% 0.17/0.39 tff(31,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(32,plain,
% 0.17/0.39 (human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[31, 30])).
% 0.17/0.39 tff(33,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(34,plain,
% 0.17/0.39 (see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[33, 30])).
% 0.17/0.39 tff(35,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(36,plain,
% 0.17/0.39 (nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[35, 30])).
% 0.17/0.39 tff(37,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(38,plain,
% 0.17/0.39 (agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[37, 30])).
% 0.17/0.39 tff(39,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(40,plain,
% 0.17/0.39 (patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[39, 30])).
% 0.17/0.39 tff(41,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(42,plain,
% 0.17/0.39 (agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[41, 30])).
% 0.17/0.39 tff(43,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(44,plain,
% 0.17/0.39 (patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[43, 30])).
% 0.17/0.39 tff(45,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(46,plain,
% 0.17/0.39 (past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[45, 30])).
% 0.17/0.39 tff(47,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(48,plain,
% 0.17/0.39 (nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[47, 30])).
% 0.17/0.39 tff(49,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(50,plain,
% 0.17/0.39 (drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[49, 30])).
% 0.17/0.39 tff(51,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(tautology,[status(thm)],[])).
% 0.17/0.39 tff(52,plain,
% 0.17/0.39 (event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))),
% 0.17/0.39 inference(unit_resolution,[status(thm)],[51, 30])).
% 0.17/0.39 tff(53,plain,
% 0.17/0.39 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))),
% 0.17/0.40 inference(tautology,[status(thm)],[])).
% 0.17/0.40 tff(54,plain,
% 0.17/0.40 (past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))),
% 0.17/0.40 inference(unit_resolution,[status(thm)],[53, 30])).
% 0.17/0.40 tff(55,plain,
% 0.17/0.40 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))),
% 0.17/0.40 inference(tautology,[status(thm)],[])).
% 0.17/0.40 tff(56,plain,
% 0.17/0.40 (coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))),
% 0.17/0.40 inference(unit_resolution,[status(thm)],[55, 30])).
% 0.17/0.40 tff(57,plain,
% 0.17/0.40 (((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))) | event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))),
% 0.17/0.40 inference(tautology,[status(thm)],[])).
% 0.17/0.40 tff(58,plain,
% 0.17/0.40 (event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))),
% 0.17/0.40 inference(unit_resolution,[status(thm)],[57, 30])).
% 0.17/0.40 tff(59,plain,
% 0.17/0.40 (((~customer(U!0, tptp_fun_X3_6(U!0))) | (~restaurant(U!0, tptp_fun_X4_5(U!0))) | (~in(U!0, tptp_fun_X3_6(U!0), tptp_fun_X4_5(U!0))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8))))) | ![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))),
% 0.17/0.40 inference(tautology,[status(thm)],[])).
% 0.17/0.40 tff(60,plain,
% 0.17/0.40 (![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))),
% 0.17/0.40 inference(unit_resolution,[status(thm)],[59, 12])).
% 0.17/0.40 tff(61,plain,
% 0.17/0.40 (((~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))) | ((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))) <=> ((~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))) | (~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))),
% 0.17/0.40 inference(rewrite,[status(thm)],[])).
% 0.17/0.40 tff(62,plain,
% 0.17/0.40 (((~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0))))) <=> ((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))),
% 0.17/0.40 inference(rewrite,[status(thm)],[])).
% 0.17/0.40 tff(63,plain,
% 0.17/0.40 (((~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))) | ((~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))))) <=> ((~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))) | ((~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))))),
% 0.17/0.40 inference(monotonicity,[status(thm)],[62])).
% 0.17/0.40 tff(64,plain,
% 0.17/0.40 (((~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))) | ((~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))))) <=> ((~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))) | (~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))))),
% 0.17/0.41 inference(transitivity,[status(thm)],[63, 61])).
% 0.17/0.41 tff(65,plain,
% 0.17/0.41 ((~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))) | ((~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))))),
% 0.17/0.41 inference(quant_inst,[status(thm)],[])).
% 0.17/0.41 tff(66,plain,
% 0.17/0.41 ((~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(U!0, X5)) | (~human_person(U!0, X6)) | (~event(U!0, X7)) | (~agent(U!0, X7, X6)) | (~patient(U!0, X7, X5)) | (~past(U!0, X7)) | (~nonreflexive(U!0, X7)) | (~drink(U!0, X7)) | (~event(U!0, X8)) | (~past(U!0, X8)) | (~agent(U!0, X8, tptp_fun_X3_6(U!0))) | (~patient(U!0, X8, X6)) | (~nonreflexive(U!0, X8)) | (~see(U!0, X8)))) | (~event(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~coffee(U!0, tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~event(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~drink(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~nonreflexive(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~past(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_Y_3(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_Z_2(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~patient(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X_4(tptp_fun_X3_6(U!0)))) | (~agent(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)), tptp_fun_X3_6(U!0))) | (~nonreflexive(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~see(U!0, tptp_fun_X1_1(tptp_fun_X3_6(U!0)))) | (~human_person(U!0, tptp_fun_X_4(tptp_fun_X3_6(U!0))))),
% 0.17/0.41 inference(modus_ponens,[status(thm)],[65, 64])).
% 0.17/0.41 tff(67,plain,
% 0.17/0.41 ($false),
% 0.17/0.41 inference(unit_resolution,[status(thm)],[66, 60, 58, 56, 54, 52, 50, 48, 46, 44, 42, 40, 38, 36, 34, 32])).
% 0.17/0.41 tff(68,plain,((~actual_world(U!0)) | (~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8))))))))), inference(lemma,lemma(discharge,[]))).
% 0.17/0.41 tff(69,plain,
% 0.17/0.41 (((~((~actual_world(U!0)) | (~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))))) | (~((~actual_world(X2!7)) | (~![X3: $i, X4: $i] : ((~customer(X2!7, X3)) | (~restaurant(X2!7, X4)) | (~in(X2!7, X3, X4)) | (~((~coffee(X2!7, tptp_fun_X5_11(X3))) | (~human_person(X2!7, tptp_fun_X6_10(X3))) | (~event(X2!7, tptp_fun_X7_9(X3))) | (~agent(X2!7, tptp_fun_X7_9(X3), tptp_fun_X6_10(X3))) | (~patient(X2!7, tptp_fun_X7_9(X3), tptp_fun_X5_11(X3))) | (~past(X2!7, tptp_fun_X7_9(X3))) | (~nonreflexive(X2!7, tptp_fun_X7_9(X3))) | (~drink(X2!7, tptp_fun_X7_9(X3))) | (~event(X2!7, tptp_fun_X8_8(X3))) | (~agent(X2!7, tptp_fun_X8_8(X3), X3)) | (~patient(X2!7, tptp_fun_X8_8(X3), tptp_fun_X6_10(X3))) | (~past(X2!7, tptp_fun_X8_8(X3))) | (~nonreflexive(X2!7, tptp_fun_X8_8(X3))) | (~see(X2!7, tptp_fun_X8_8(X3))))))) | (~![U: $i] : ((~actual_world(U)) | (~((~customer(U, tptp_fun_V_13(U))) | (~restaurant(U, tptp_fun_W_12(U))) | (~in(U, tptp_fun_V_13(U), tptp_fun_W_12(U))) | (~![X: $i, Y: $i, Z: $i, X1: $i] : ((~event(U, Z)) | (~past(U, Z)) | (~nonreflexive(U, Z)) | (~drink(U, Z)) | (~event(U, X1)) | (~past(U, X1)) | (~nonreflexive(U, X1)) | (~see(U, X1)) | (~human_person(U, X)) | (~coffee(U, Y)) | (~agent(U, Z, X)) | (~patient(U, Z, Y)) | (~agent(U, X1, tptp_fun_V_13(U))) | (~patient(U, X1, X))))))))))) <=> ((~((~actual_world(U!0)) | (~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))))) | (~((~actual_world(X2!7)) | (~![X3: $i, X4: $i] : ((~customer(X2!7, X3)) | (~restaurant(X2!7, X4)) | (~in(X2!7, X3, X4)) | (~((~coffee(X2!7, tptp_fun_X5_11(X3))) | (~human_person(X2!7, tptp_fun_X6_10(X3))) | (~event(X2!7, tptp_fun_X7_9(X3))) | (~agent(X2!7, tptp_fun_X7_9(X3), tptp_fun_X6_10(X3))) | (~patient(X2!7, tptp_fun_X7_9(X3), tptp_fun_X5_11(X3))) | (~past(X2!7, tptp_fun_X7_9(X3))) | (~nonreflexive(X2!7, tptp_fun_X7_9(X3))) | (~drink(X2!7, tptp_fun_X7_9(X3))) | (~event(X2!7, tptp_fun_X8_8(X3))) | (~agent(X2!7, tptp_fun_X8_8(X3), X3)) | (~patient(X2!7, tptp_fun_X8_8(X3), tptp_fun_X6_10(X3))) | (~past(X2!7, tptp_fun_X8_8(X3))) | (~nonreflexive(X2!7, tptp_fun_X8_8(X3))) | (~see(X2!7, tptp_fun_X8_8(X3))))))) | (~![U: $i] : ((~actual_world(U)) | (~((~customer(U, tptp_fun_V_13(U))) | (~restaurant(U, tptp_fun_W_12(U))) | (~in(U, tptp_fun_V_13(U), tptp_fun_W_12(U))) | (~![X: $i, Y: $i, Z: $i, X1: $i] : ((~event(U, Z)) | (~past(U, Z)) | (~nonreflexive(U, Z)) | (~drink(U, Z)) | (~event(U, X1)) | (~past(U, X1)) | (~nonreflexive(U, X1)) | (~see(U, X1)) | (~human_person(U, X)) | (~coffee(U, Y)) | (~agent(U, Z, X)) | (~patient(U, Z, Y)) | (~agent(U, X1, tptp_fun_V_13(U))) | (~patient(U, X1, X)))))))))))),
% 0.17/0.41 inference(rewrite,[status(thm)],[])).
% 0.17/0.41 tff(70,plain,
% 0.17/0.41 (((actual_world(U!0) & ![V: $i, W: $i] : ((~(customer(U!0, V) & restaurant(U!0, W) & in(U!0, V, W))) | (human_person(U!0, tptp_fun_X_4(V)) & coffee(U!0, tptp_fun_Y_3(V)) & event(U!0, tptp_fun_Z_2(V)) & agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V)) & patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V)) & past(U!0, tptp_fun_Z_2(V)) & nonreflexive(U!0, tptp_fun_Z_2(V)) & drink(U!0, tptp_fun_Z_2(V)) & event(U!0, tptp_fun_X1_1(V)) & agent(U!0, tptp_fun_X1_1(V), V) & patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V)) & past(U!0, tptp_fun_X1_1(V)) & nonreflexive(U!0, tptp_fun_X1_1(V)) & see(U!0, tptp_fun_X1_1(V)))) & ![X2: $i] : ((~actual_world(X2)) | (customer(X2, tptp_fun_X3_6(X2)) & restaurant(X2, tptp_fun_X4_5(X2)) & in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2)) & ![X5: $i, X6: $i, X7: $i, X8: $i] : (~(coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, tptp_fun_X3_6(X2)) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8)))))) | (actual_world(X2!7) & ![X3: $i, X4: $i] : ((~(customer(X2!7, X3) & restaurant(X2!7, X4) & in(X2!7, X3, X4))) | (coffee(X2!7, tptp_fun_X5_11(X3)) & human_person(X2!7, tptp_fun_X6_10(X3)) & event(X2!7, tptp_fun_X7_9(X3)) & agent(X2!7, tptp_fun_X7_9(X3), tptp_fun_X6_10(X3)) & patient(X2!7, tptp_fun_X7_9(X3), tptp_fun_X5_11(X3)) & past(X2!7, tptp_fun_X7_9(X3)) & nonreflexive(X2!7, tptp_fun_X7_9(X3)) & drink(X2!7, tptp_fun_X7_9(X3)) & event(X2!7, tptp_fun_X8_8(X3)) & agent(X2!7, tptp_fun_X8_8(X3), X3) & patient(X2!7, tptp_fun_X8_8(X3), tptp_fun_X6_10(X3)) & past(X2!7, tptp_fun_X8_8(X3)) & nonreflexive(X2!7, tptp_fun_X8_8(X3)) & see(X2!7, tptp_fun_X8_8(X3)))) & ![U: $i] : ((~actual_world(U)) | (customer(U, tptp_fun_V_13(U)) & restaurant(U, tptp_fun_W_12(U)) & in(U, tptp_fun_V_13(U), tptp_fun_W_12(U)) & ![X: $i, Y: $i, Z: $i, X1: $i] : (~(human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, tptp_fun_V_13(U)) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))) <=> ((~((~actual_world(U!0)) | (~![V: $i, W: $i] : ((~((~event(U!0, tptp_fun_Z_2(V))) | (~coffee(U!0, tptp_fun_Y_3(V))) | (~past(U!0, tptp_fun_X1_1(V))) | (~event(U!0, tptp_fun_X1_1(V))) | (~drink(U!0, tptp_fun_Z_2(V))) | (~nonreflexive(U!0, tptp_fun_Z_2(V))) | (~past(U!0, tptp_fun_Z_2(V))) | (~patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V))) | (~agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V))) | (~patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V))) | (~agent(U!0, tptp_fun_X1_1(V), V)) | (~nonreflexive(U!0, tptp_fun_X1_1(V))) | (~see(U!0, tptp_fun_X1_1(V))) | (~human_person(U!0, tptp_fun_X_4(V))))) | (~restaurant(U!0, W)) | (~customer(U!0, V)) | (~in(U!0, V, W)))) | (~![X2: $i] : ((~actual_world(X2)) | (~((~customer(X2, tptp_fun_X3_6(X2))) | (~restaurant(X2, tptp_fun_X4_5(X2))) | (~in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) | (~![X5: $i, X6: $i, X7: $i, X8: $i] : ((~coffee(X2, X5)) | (~human_person(X2, X6)) | (~event(X2, X7)) | (~agent(X2, X7, X6)) | (~patient(X2, X7, X5)) | (~past(X2, X7)) | (~nonreflexive(X2, X7)) | (~drink(X2, X7)) | (~event(X2, X8)) | (~agent(X2, X8, tptp_fun_X3_6(X2))) | (~patient(X2, X8, X6)) | (~past(X2, X8)) | (~nonreflexive(X2, X8)) | (~see(X2, X8)))))))))) | (~((~actual_world(X2!7)) | (~![X3: $i, X4: $i] : ((~customer(X2!7, X3)) | (~restaurant(X2!7, X4)) | (~in(X2!7, X3, X4)) | (~((~coffee(X2!7, tptp_fun_X5_11(X3))) | (~human_person(X2!7, tptp_fun_X6_10(X3))) | (~event(X2!7, tptp_fun_X7_9(X3))) | (~agent(X2!7, tptp_fun_X7_9(X3), tptp_fun_X6_10(X3))) | (~patient(X2!7, tptp_fun_X7_9(X3), tptp_fun_X5_11(X3))) | (~past(X2!7, tptp_fun_X7_9(X3))) | (~nonreflexive(X2!7, tptp_fun_X7_9(X3))) | (~drink(X2!7, tptp_fun_X7_9(X3))) | (~event(X2!7, tptp_fun_X8_8(X3))) | (~agent(X2!7, tptp_fun_X8_8(X3), X3)) | (~patient(X2!7, tptp_fun_X8_8(X3), tptp_fun_X6_10(X3))) | (~past(X2!7, tptp_fun_X8_8(X3))) | (~nonreflexive(X2!7, tptp_fun_X8_8(X3))) | (~see(X2!7, tptp_fun_X8_8(X3))))))) | (~![U: $i] : ((~actual_world(U)) | (~((~customer(U, tptp_fun_V_13(U))) | (~restaurant(U, tptp_fun_W_12(U))) | (~in(U, tptp_fun_V_13(U), tptp_fun_W_12(U))) | (~![X: $i, Y: $i, Z: $i, X1: $i] : ((~event(U, Z)) | (~past(U, Z)) | (~nonreflexive(U, Z)) | (~drink(U, Z)) | (~event(U, X1)) | (~past(U, X1)) | (~nonreflexive(U, X1)) | (~see(U, X1)) | (~human_person(U, X)) | (~coffee(U, Y)) | (~agent(U, Z, X)) | (~patient(U, Z, Y)) | (~agent(U, X1, tptp_fun_V_13(U))) | (~patient(U, X1, X)))))))))))),
% 0.17/0.41 inference(rewrite,[status(thm)],[])).
% 0.17/0.41 tff(71,plain,
% 0.17/0.41 ((((actual_world(U!0) & ![V: $i, W: $i] : ((~(customer(U!0, V) & restaurant(U!0, W) & in(U!0, V, W))) | (human_person(U!0, tptp_fun_X_4(V)) & coffee(U!0, tptp_fun_Y_3(V)) & event(U!0, tptp_fun_Z_2(V)) & agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V)) & patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V)) & past(U!0, tptp_fun_Z_2(V)) & nonreflexive(U!0, tptp_fun_Z_2(V)) & drink(U!0, tptp_fun_Z_2(V)) & event(U!0, tptp_fun_X1_1(V)) & agent(U!0, tptp_fun_X1_1(V), V) & patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V)) & past(U!0, tptp_fun_X1_1(V)) & nonreflexive(U!0, tptp_fun_X1_1(V)) & see(U!0, tptp_fun_X1_1(V))))) & ![X2: $i] : ((~actual_world(X2)) | ((customer(X2, tptp_fun_X3_6(X2)) & restaurant(X2, tptp_fun_X4_5(X2)) & in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2))) & ![X5: $i, X6: $i, X7: $i, X8: $i] : (~(coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, tptp_fun_X3_6(X2)) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8)))))) | ((actual_world(X2!7) & ![X3: $i, X4: $i] : ((~(customer(X2!7, X3) & restaurant(X2!7, X4) & in(X2!7, X3, X4))) | (coffee(X2!7, tptp_fun_X5_11(X3)) & human_person(X2!7, tptp_fun_X6_10(X3)) & event(X2!7, tptp_fun_X7_9(X3)) & agent(X2!7, tptp_fun_X7_9(X3), tptp_fun_X6_10(X3)) & patient(X2!7, tptp_fun_X7_9(X3), tptp_fun_X5_11(X3)) & past(X2!7, tptp_fun_X7_9(X3)) & nonreflexive(X2!7, tptp_fun_X7_9(X3)) & drink(X2!7, tptp_fun_X7_9(X3)) & event(X2!7, tptp_fun_X8_8(X3)) & agent(X2!7, tptp_fun_X8_8(X3), X3) & patient(X2!7, tptp_fun_X8_8(X3), tptp_fun_X6_10(X3)) & past(X2!7, tptp_fun_X8_8(X3)) & nonreflexive(X2!7, tptp_fun_X8_8(X3)) & see(X2!7, tptp_fun_X8_8(X3))))) & ![U: $i] : ((~actual_world(U)) | ((customer(U, tptp_fun_V_13(U)) & restaurant(U, tptp_fun_W_12(U)) & in(U, tptp_fun_V_13(U), tptp_fun_W_12(U))) & ![X: $i, Y: $i, Z: $i, X1: $i] : (~(human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, tptp_fun_V_13(U)) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))) <=> ((actual_world(U!0) & ![V: $i, W: $i] : ((~(customer(U!0, V) & restaurant(U!0, W) & in(U!0, V, W))) | (human_person(U!0, tptp_fun_X_4(V)) & coffee(U!0, tptp_fun_Y_3(V)) & event(U!0, tptp_fun_Z_2(V)) & agent(U!0, tptp_fun_Z_2(V), tptp_fun_X_4(V)) & patient(U!0, tptp_fun_Z_2(V), tptp_fun_Y_3(V)) & past(U!0, tptp_fun_Z_2(V)) & nonreflexive(U!0, tptp_fun_Z_2(V)) & drink(U!0, tptp_fun_Z_2(V)) & event(U!0, tptp_fun_X1_1(V)) & agent(U!0, tptp_fun_X1_1(V), V) & patient(U!0, tptp_fun_X1_1(V), tptp_fun_X_4(V)) & past(U!0, tptp_fun_X1_1(V)) & nonreflexive(U!0, tptp_fun_X1_1(V)) & see(U!0, tptp_fun_X1_1(V)))) & ![X2: $i] : ((~actual_world(X2)) | (customer(X2, tptp_fun_X3_6(X2)) & restaurant(X2, tptp_fun_X4_5(X2)) & in(X2, tptp_fun_X3_6(X2), tptp_fun_X4_5(X2)) & ![X5: $i, X6: $i, X7: $i, X8: $i] : (~(coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, tptp_fun_X3_6(X2)) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8)))))) | (actual_world(X2!7) & ![X3: $i, X4: $i] : ((~(customer(X2!7, X3) & restaurant(X2!7, X4) & in(X2!7, X3, X4))) | (coffee(X2!7, tptp_fun_X5_11(X3)) & human_person(X2!7, tptp_fun_X6_10(X3)) & event(X2!7, tptp_fun_X7_9(X3)) & agent(X2!7, tptp_fun_X7_9(X3), tptp_fun_X6_10(X3)) & patient(X2!7, tptp_fun_X7_9(X3), tptp_fun_X5_11(X3)) & past(X2!7, tptp_fun_X7_9(X3)) & nonreflexive(X2!7, tptp_fun_X7_9(X3)) & drink(X2!7, tptp_fun_X7_9(X3)) & event(X2!7, tptp_fun_X8_8(X3)) & agent(X2!7, tptp_fun_X8_8(X3), X3) & patient(X2!7, tptp_fun_X8_8(X3), tptp_fun_X6_10(X3)) & past(X2!7, tptp_fun_X8_8(X3)) & nonreflexive(X2!7, tptp_fun_X8_8(X3)) & see(X2!7, tptp_fun_X8_8(X3)))) & ![U: $i] : ((~actual_world(U)) | (customer(U, tptp_fun_V_13(U)) & restaurant(U, tptp_fun_W_12(U)) & in(U, tptp_fun_V_13(U), tptp_fun_W_12(U)) & ![X: $i, Y: $i, Z: $i, X1: $i] : (~(human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, tptp_fun_V_13(U)) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1)))))))),
% 0.17/0.42 inference(rewrite,[status(thm)],[])).
% 0.17/0.42 tff(72,plain,
% 0.17/0.42 (((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) <=> ((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8)))))),
% 0.17/0.42 inference(rewrite,[status(thm)],[])).
% 0.17/0.42 tff(73,plain,
% 0.17/0.42 ((((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1)))))) <=> (((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))),
% 0.17/0.42 inference(monotonicity,[status(thm)],[72])).
% 0.17/0.42 tff(74,plain,
% 0.17/0.42 ((~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))) <=> (~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1)))))))),
% 0.17/0.42 inference(monotonicity,[status(thm)],[73])).
% 0.17/0.42 tff(75,plain,
% 0.17/0.42 ((~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))) <=> (~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1)))))))),
% 0.17/0.42 inference(rewrite,[status(thm)],[])).
% 0.17/0.42 tff(76,plain,
% 0.17/0.42 ((~(~(~((?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : (((customer(U, V) & restaurant(U, W)) & in(U, V, W)) => ?[X: $i, Y: $i, Z: $i, X1: $i] : (((((((((((((human_person(U, X) & coffee(U, Y)) & event(U, Z)) & agent(U, Z, X)) & patient(U, Z, Y)) & past(U, Z)) & nonreflexive(U, Z)) & drink(U, Z)) & event(U, X1)) & agent(U, X1, V)) & patient(U, X1, X)) & past(U, X1)) & nonreflexive(U, X1)) & see(U, X1)))) => ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : (((customer(X2, X3) & restaurant(X2, X4)) & in(X2, X3, X4)) => ?[X5: $i, X6: $i, X7: $i, X8: $i] : (((((((((((((coffee(X2, X5) & human_person(X2, X6)) & event(X2, X7)) & agent(X2, X7, X6)) & patient(X2, X7, X5)) & past(X2, X7)) & nonreflexive(X2, X7)) & drink(X2, X7)) & event(X2, X8)) & agent(X2, X8, X3)) & patient(X2, X8, X6)) & past(X2, X8)) & nonreflexive(X2, X8)) & see(X2, X8))))) & (?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : (((customer(X2, X3) & restaurant(X2, X4)) & in(X2, X3, X4)) => ?[X5: $i, X6: $i, X7: $i, X8: $i] : (((((((((((((coffee(X2, X5) & human_person(X2, X6)) & event(X2, X7)) & agent(X2, X7, X6)) & patient(X2, X7, X5)) & past(X2, X7)) & nonreflexive(X2, X7)) & drink(X2, X7)) & event(X2, X8)) & agent(X2, X8, X3)) & patient(X2, X8, X6)) & past(X2, X8)) & nonreflexive(X2, X8)) & see(X2, X8)))) => ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : (((customer(U, V) & restaurant(U, W)) & in(U, V, W)) => ?[X: $i, Y: $i, Z: $i, X1: $i] : (((((((((((((human_person(U, X) & coffee(U, Y)) & event(U, Z)) & agent(U, Z, X)) & patient(U, Z, Y)) & past(U, Z)) & nonreflexive(U, Z)) & drink(U, Z)) & event(U, X1)) & agent(U, X1, V)) & patient(U, X1, X)) & past(U, X1)) & nonreflexive(U, X1)) & see(U, X1))))))))) <=> (~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1)))))))),
% 0.17/0.42 inference(rewrite,[status(thm)],[])).
% 0.17/0.42 tff(77,axiom,(~(~(~((?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : (((customer(U, V) & restaurant(U, W)) & in(U, V, W)) => ?[X: $i, Y: $i, Z: $i, X1: $i] : (((((((((((((human_person(U, X) & coffee(U, Y)) & event(U, Z)) & agent(U, Z, X)) & patient(U, Z, Y)) & past(U, Z)) & nonreflexive(U, Z)) & drink(U, Z)) & event(U, X1)) & agent(U, X1, V)) & patient(U, X1, X)) & past(U, X1)) & nonreflexive(U, X1)) & see(U, X1)))) => ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : (((customer(X2, X3) & restaurant(X2, X4)) & in(X2, X3, X4)) => ?[X5: $i, X6: $i, X7: $i, X8: $i] : (((((((((((((coffee(X2, X5) & human_person(X2, X6)) & event(X2, X7)) & agent(X2, X7, X6)) & patient(X2, X7, X5)) & past(X2, X7)) & nonreflexive(X2, X7)) & drink(X2, X7)) & event(X2, X8)) & agent(X2, X8, X3)) & patient(X2, X8, X6)) & past(X2, X8)) & nonreflexive(X2, X8)) & see(X2, X8))))) & (?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : (((customer(X2, X3) & restaurant(X2, X4)) & in(X2, X3, X4)) => ?[X5: $i, X6: $i, X7: $i, X8: $i] : (((((((((((((coffee(X2, X5) & human_person(X2, X6)) & event(X2, X7)) & agent(X2, X7, X6)) & patient(X2, X7, X5)) & past(X2, X7)) & nonreflexive(X2, X7)) & drink(X2, X7)) & event(X2, X8)) & agent(X2, X8, X3)) & patient(X2, X8, X6)) & past(X2, X8)) & nonreflexive(X2, X8)) & see(X2, X8)))) => ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : (((customer(U, V) & restaurant(U, W)) & in(U, V, W)) => ?[X: $i, Y: $i, Z: $i, X1: $i] : (((((((((((((human_person(U, X) & coffee(U, Y)) & event(U, Z)) & agent(U, Z, X)) & patient(U, Z, Y)) & past(U, Z)) & nonreflexive(U, Z)) & drink(U, Z)) & event(U, X1)) & agent(U, X1, V)) & patient(U, X1, X)) & past(U, X1)) & nonreflexive(U, X1)) & see(U, X1))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','co1')).
% 0.17/0.42 tff(78,plain,
% 0.17/0.42 (~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.17/0.43 tff(79,plain,
% 0.17/0.43 (~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[78, 74])).
% 0.17/0.43 tff(80,plain,
% 0.17/0.43 (~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))),
% 0.17/0.43 inference(modus_ponens,[status(thm)],[79, 75])).
% 0.17/0.43 tff(81,plain,
% 0.17/0.43 (~(((~?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))) | ?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) & ((~?[X2: $i] : (actual_world(X2) & ![X3: $i, X4: $i] : ((~(customer(X2, X3) & restaurant(X2, X4) & in(X2, X3, X4))) | ?[X5: $i, X6: $i, X7: $i, X8: $i] : (coffee(X2, X5) & human_person(X2, X6) & event(X2, X7) & agent(X2, X7, X6) & patient(X2, X7, X5) & past(X2, X7) & nonreflexive(X2, X7) & drink(X2, X7) & event(X2, X8) & agent(X2, X8, X3) & patient(X2, X8, X6) & past(X2, X8) & nonreflexive(X2, X8) & see(X2, X8))))) | ?[U: $i] : (actual_world(U) & ![V: $i, W: $i] : ((~(customer(U, V) & restaurant(U, W) & in(U, V, W))) | ?[X: $i, Y: $i, Z: $i, X1: $i] : (human_person(U, X) & coffee(U, Y) & event(U, Z) & agent(U, Z, X) & patient(U, Z, Y) & past(U, Z) & nonreflexive(U, Z) & drink(U, Z) & event(U, X1) & agent(U, X1, V) & patient(U, X1, X) & past(U, X1) & nonreflexive(U, X1) & see(U, X1))))))),
% 0.17/0.46 inference(modus_ponens,[status(thm)],[80, 74])).
% 0.17/0.46 unexpected number of arguments: (let ((a!1 (exists ((U $i))
% 0.17/0.46 (let ((a!1 (forall ((V $i) (W $i))
% 0.17/0.46 (let ((a!1 (not (and (customer U V)
% 0.17/0.46 (restaurant U W)
% 0.17/0.46 (in U V W)))))
% 0.17/0.46 (or a!1
% 0.17/0.46 (exists ((X $i) (Y $i) (Z $i) (X1 $i))
% 0.17/0.46 (and (human_person U X)
% 0.17/0.46 (coffee U Y)
% 0.17/0.46 (event U Z)
% 0.17/0.46 (agent U Z X)
% 0.17/0.46 (patient U Z Y)
% 0.17/0.46 (past U Z)
% 0.17/0.46 (nonreflexive U Z)
% 0.17/0.46 (drink U Z)
% 0.17/0.46 (event U X1)
% 0.17/0.46 (agent U X1 V)
% 0.17/0.46 (patient U X1 X)
% 0.17/0.46 (past U X1)
% 0.17/0.46 (nonreflexive U X1)
% 0.17/0.46 (see U X1))))))))
% 0.17/0.46 (and (actual_world U) a!1))))
% 0.17/0.46 (a!2 (forall ((V $i) (W $i))
% 0.17/0.46 (let ((a!1 (not (and (customer U!0 V)
% 0.17/0.46 (restaurant U!0 W)
% 0.17/0.46 (in U!0 V W))))
% 0.17/0.46 (a!2 (exists ((X $i) (Y $i) (Z $i) (X1 $i))
% 0.17/0.46 (and (human_person U!0 X)
% 0.17/0.46 (coffee U!0 Y)
% 0.17/0.46 (event U!0 Z)
% 0.17/0.46 (agent U!0 Z X)
% 0.17/0.46 (patient U!0 Z Y)
% 0.17/0.46 (past U!0 Z)
% 0.17/0.46 (nonreflexive U!0 Z)
% 0.17/0.46 (drink U!0 Z)
% 0.17/0.46 (event U!0 X1)
% 0.17/0.46 (agent U!0 X1 V)
% 0.17/0.46 (patient U!0 X1 X)
% 0.17/0.46 (past U!0 X1)
% 0.17/0.46 (nonreflexive U!0 X1)
% 0.17/0.46 (see U!0 X1)))))
% 0.17/0.46 (or a!1 a!2))))
% 0.17/0.46 (a!4 (lambda ((V $i) (W $i))
% 0.17/0.46 (let ((a!1 (not (and (customer U!0 V)
% 0.17/0.46 (restaurant U!0 W)
% 0.17/0.46 (in U!0 V W))))
% 0.17/0.46 (a!2 (exists ((X $i) (Y $i) (Z $i) (X1 $i))
% 0.17/0.46 (and (human_person U!0 X)
% 0.17/0.46 (coffee U!0 Y)
% 0.17/0.46 (event U!0 Z)
% 0.17/0.46 (agent U!0 Z X)
% 0.17/0.46 (patient U!0 Z Y)
% 0.17/0.46 (past U!0 Z)
% 0.17/0.46 (nonreflexive U!0 Z)
% 0.17/0.46 (drink U!0 Z)
% 0.17/0.46 (event U!0 X1)
% 0.17/0.46 (agent U!0 X1 V)
% 0.17/0.46 (patient U!0 X1 X)
% 0.17/0.46 (past U!0 X1)
% 0.17/0.46 (nonreflexive U!0 X1)
% 0.17/0.46 (see U!0 X1))))
% 0.17/0.46 (a!3 (and (human_person U!0 (X!4 V))
% 0.17/0.46 (coffee U!0 (Y!3 V))
% 0.17/0.46 (event U!0 (Z!2 V))
% 0.17/0.46 (agent U!0 (Z!2 V) (X!4 V))
% 0.17/0.46 (patient U!0 (Z!2 V) (Y!3 V))
% 0.17/0.46 (past U!0 (Z!2 V))
% 0.17/0.46 (nonreflexive U!0 (Z!2 V))
% 0.17/0.46 (drink U!0 (Z!2 V))
% 0.17/0.46 (event U!0 (X1!1 V))
% 0.17/0.46 (agent U!0 (X1!1 V) V)
% 0.17/0.46 (patient U!0 (X1!1 V) (X!4 V))
% 0.17/0.46 (past U!0 (X1!1 V))
% 0.17/0.46 (nonreflexive U!0 (X1!1 V))
% 0.17/0.46 (see U!0 (X1!1 V)))))
% 0.17/0.46 (monotonicity (refl (~ a!1 a!1))
% 0.17/0.46 (sk (~ a!2 a!3))
% 0.17/0.46 (~ (or a!1 a!2) (or a!1 a!3))))))
% 0.17/0.46 (a!5 (forall ((V $i) (W $i))
% 0.17/0.46 (let ((a!1 (not (and (customer U!0 V)
% 0.17/0.46 (restaurant U!0 W)
% 0.17/0.46 (in U!0 V W))))
% 0.17/0.46 (a!2 (and (human_person U!0 (X!4 V))
% 0.17/0.46 (coffee U!0 (Y!3 V))
% 0.17/0.46 (event U!0 (Z!2 V))
% 0.17/0.46 (agent U!0 (Z!2 V) (X!4 V))
% 0.17/0.46 (patient U!0 (Z!2 V) (Y!3 V))
% 0.17/0.46 (past U!0 (Z!2 V))
% 0.17/0.46 (nonreflexive U!0 (Z!2 V))
% 0.17/0.46 (drink U!0 (Z!2 V))
% 0.17/0.46 (event U!0 (X1!1 V))
% 0.17/0.46 (agent U!0 (X1!1 V) V)
% 0.17/0.46 (patient U!0 (X1!1 V) (X!4 V))
% 0.17/0.46 (past U!0 (X1!1 V))
% 0.17/0.46 (nonreflexive U!0 (X1!1 V))
% 0.17/0.46 (see U!0 (X1!1 V)))))
% 0.17/0.46 (or a!1 a!2))))
% 0.17/0.46 (a!9 (lambda ((X2 $i))
% 0.17/0.46 (let ((a!1 (refl (~ (not (actual_world X2))
% 0.17/0.46 (not (actual_world X2)))))
% 0.17/0.46 (a!2 (forall ((X3 $i) (X4 $i))
% 0.17/0.46 (let ((a!1 (not (and (customer X2 X3)
% 0.17/0.46 (restaurant X2 X4)
% 0.17/0.46 (in X2 X3 X4)))))
% 0.17/0.46 (or a!1
% 0.17/0.46 (exists ((X5 $i) (X6 $i) (X7 $i) (X8 $i))
% 0.17/0.46 (and (coffee X2 X5)
% 0.17/0.46 (human_person X2 X6)
% 0.17/0.46 (event X2 X7)
% 0.17/0.46 (agent X2 X7 X6)
% 0.17/0.46 (patient X2 X7 X5)
% 0.17/0.46 (past X2 X7)
% 0.17/0.46 (nonreflexive X2 X7)
% 0.17/0.46 (drink X2 X7)
% 0.17/0.46 (event X2 X8)
% 0.17/0.46 (agent X2 X8 X3)
% 0.17/0.46 (patient X2 X8 X6)
% 0.17/0.46 (past X2 X8)
% 0.17/0.46 (nonreflexive X2 X8)
% 0.17/0.46 (see X2 X8)))))))
% 0.17/0.46 (a!3 (and (customer X2 (X3!6 X2))
% 0.17/0.46 (restaurant X2 (X4!5 X2))
% 0.17/0.46 (in X2 (X3!6 X2) (X4!5 X2))))
% 0.17/0.46 (a!4 (exists ((X5 $i) (X6 $i) (X7 $i) (X8 $i))
% 0.17/0.46 (and (coffee X2 X5)
% 0.17/0.46 (human_person X2 X6)
% 0.17/0.46 (event X2 X7)
% 0.17/0.46 (agent X2 X7 X6)
% 0.17/0.46 (patient X2 X7 X5)
% 0.17/0.46 (past X2 X7)
% 0.17/0.46 (nonreflexive X2 X7)
% 0.17/0.46 (drink X2 X7)
% 0.17/0.46 (event X2 X8)
% 0.17/0.46 (agent X2 X8 (X3!6 X2))
% 0.17/0.46 (patient X2 X8 X6)
% 0.17/0.46 (past X2 X8)
% 0.17/0.46 (nonreflexive X2 X8)
% 0.17/0.46 (see X2 X8))))
% 0.17/0.46 (a!6 (lambda ((X5 $i) (X6 $i) (X7 $i) (X8 $i))
% 0.17/0.46 (let ((a!1 (and (coffee X2 X5)
% 0.17/0.46 (human_person X2 X6)
% 0.17/0.46 (event X2 X7)
% 0.17/0.46 (agent X2 X7 X6)
% 0.17/0.46 (patient X2 X7 X5)
% 0.17/0.46 (past X2 X7)
% 0.17/0.46 (nonreflexive X2 X7)
% 0.17/0.46 (drink X2 X7)
% 0.17/0.46 (event X2 X8)
% 0.17/0.46 (agent X2 X8 (X3!6 X2))
% 0.17/0.46 (patient X2 X8 X6)
% 0.17/0.46 (past X2 X8)
% 0.17/0.46 (nonreflexive X2 X8)
% 0.17/0.46 (see X2 X8))))
% 0.17/0.46 (refl (~ (not a!1) (not a!1))))))
% 0.17/0.46 (a!7 (forall ((X5 $i) (X6 $i) (X7 $i) (X8 $i))
% 0.17/0.46 (let ((a!1 (and (coffee X2 X5)
% 0.17/0.46 (human_person X2 X6)
% 0.17/0.46 (event X2 X7)
% 0.17/0.46 (agent X2 X7 X6)
% 0.17/0.46 (patient X2 X7 X5)
% 0.17/0.46 (past X2 X7)
% 0.17/0.46 (nonreflexive X2 X7)
% 0.17/0.46 (drink X2 X7)
% 0.17/0.46 (event X2 X8)
% 0.17/0.46 (agent X2 X8 (X3!6 X2))
% 0.17/0.46 (patient X2 X8 X6)
% 0.17/0.46 (past X2 X8)
% 0.17/0.46 (nonreflexive X2 X8)
% 0.17/0.46 (see X2 X8))))
% 0.17/0.46 (not a!1)))))
% 0.17/0.46 (let ((a!5 (~ (not a!2) (not (or (not a!3) a!4))))
% 0.17/0.46 (a!8 (~ (not (or (not a!3) a!4)) (and a!3 a!7)))
% 0.17/0.46 (a!10 (~ (not (and (actual_world X2) a!2))
% 0.17/0.46 (or (not (actual_world X2)) (and a!3 a!7)))))
% 0.17/0.46 (let ((a!9 (nnf-neg (refl (~ a!3 a!3))
% 0.17/0.46 (nnf-neg (proof-bind a!6) (~ (not a!4) a!7))
% 0.17/0.46 a!8)))
% 0.17/0.46 (nnf-neg a!1
% 0.17/0.46 (trans (sk a!5) a!9 (~ (not a!2) (and a!3 a!7)))
% 0.17/0.46 a!10))))))
% 0.17/0.46 (a!10 (exists ((X2 $i))
% 0.17/0.46 (let ((a!1 (forall ((X3 $i) (X4 $i))
% 0.17/0.46 (let ((a!1 (not (and (customer X2 X3)
% 0.17/0.46 (restaurant X2 X4)
% 0.17/0.46 (in X2 X3 X4)))))
% 0.17/0.46 (or a!1
% 0.17/0.46 (exists ((X5 $i) (X6 $i) (X7 $i) (X8 $i))
% 0.17/0.46 (and (coffee X2 X5)
% 0.17/0.46 (human_person X2 X6)
% 0.17/0.46 (event X2 X7)
% 0.17/0.46 (agent X2 X7 X6)
% 0.17/0.46 (patient X2 X7 X5)
% 0.17/0.46 (past X2 X7)
% 0.17/0.46 (nonreflexive X2 X7)
% 0.17/0.46 (drink X2 X7)
% 0.17/0.46 (event X2 X8)
% 0.17/0.46 (agent X2 X8 X3)
% 0.17/0.46 (patient X2 X8 X6)
% 0.17/0.46 (past X2 X8)
% 0.17/0.46 (nonreflexive X2 X8)
% 0.17/0.46 (see X2 X8))))))))
% 0.17/0.46 (and (actual_world X2) a!1))))
% 0.17/0.46 (a!11 (forall ((X2 $i))
% 0.17/0.46 (let ((a!1 (and (customer X2 (X3!6 X2))
% 0.17/0.46 (restaurant X2 (X4!5 X2))
% 0.17/0.46 (in X2 (X3!6 X2) (X4!5 X2))))
% 0.17/0.46 (a!2 (forall ((X5 $i) (X6 $i) (X7 $i) (X8 $i))
% 0.17/0.46 (let ((a!1 (and (coffee X2 X5)
% 0.17/0.46 (human_person X2 X6)
% 0.17/0.46 (event X2 X7)
% 0.17/0.46 (agent X2 X7 X6)
% 0.17/0.46 (patient X2 X7 X5)
% 0.17/0.46 (past X2 X7)
% 0.17/0.46 (nonreflexive X2 X7)
% 0.17/0.46 (drink X2 X7)
% 0.17/0.46 (event X2 X8)
% 0.17/0.46 (agent X2 X8 (X3!6 X2))
% 0.17/0.46 (patient X2 X8 X6)
% 0.17/0.46 (past X2 X8)
% 0.17/0.46 (nonreflexive X2 X8)
% 0.17/0.46 (see X2 X8))))
% 0.17/0.46 (not a!1)))))
% 0.17/0.46 (or (not (actual_world X2)) (and a!1 a!2)))))
% 0.17/0.46 (a!14 (forall ((X3 $i) (X4 $i))
% 0.17/0.46 (let ((a!1 (not (and (customer X2!7 X3)
% 0.17/0.46 (restaurant X2!7 X4)
% 0.17/0.46 (in X2!7 X3 X4))))
% 0.17/0.46 (a!2 (exists ((X5 $i) (X6 $i) (X7 $i) (X8 $i))
% 0.17/0.46 (and (coffee X2!7 X5)
% 0.17/0.46 (human_person X2!7 X6)
% 0.17/0.46 (event X2!7 X7)
% 0.17/0.46 (agent X2!7 X7 X6)
% 0.17/0.46 (patient X2!7 X7 X5)
% 0.17/0.46 (past X2!7 X7)
% 0.17/0.46 (nonreflexive X2!7 X7)
% 0.17/0.46 (drink X2!7 X7)
% 0.17/0.46 (event X2!7 X8)
% 0.17/0.46 (agent X2!7 X8 X3)
% 0.17/0.46 (patient X2!7 X8 X6)
% 0.17/0.46 (past X2!7 X8)
% 0.17/0.46 (nonreflexive X2!7 X8)
% 0.17/0.46 (see X2!7 X8)))))
% 0.17/0.46 (or a!1 a!2))))
% 0.17/0.46 (a!16 (lambda ((X3 $i) (X4 $i))
% 0.17/0.46 (let ((a!1 (not (and (customer X2!7 X3)
% 0.17/0.46 (restaurant X2!7 X4)
% 0.17/0.46 (in X2!7 X3 X4))))
% 0.17/0.46 (a!2 (exists ((X5 $i) (X6 $i) (X7 $i) (X8 $i))
% 0.17/0.46 (and (coffee X2!7 X5)
% 0.17/0.46 (human_person X2!7 X6)
% 0.17/0.46 (event X2!7 X7)
% 0.17/0.46 (agent X2!7 X7 X6)
% 0.17/0.46 (patient X2!7 X7 X5)
% 0.17/0.46 (past X2!7 X7)
% 0.17/0.46 (nonreflexive X2!7 X7)
% 0.17/0.46 (drink X2!7 X7)
% 0.17/0.46 (event X2!7 X8)
% 0.17/0.46 (agent X2!7 X8 X3)
% 0.17/0.46 (patient X2!7 X8 X6)
% 0.17/0.46 (past X2!7 X8)
% 0.17/0.46 (nonreflexive X2!7 X8)
% 0.17/0.46 (see X2!7 X8))))
% 0.17/0.46 (a!3 (and (coffee X2!7 (X5!11 X3))
% 0.17/0.46 (human_person X2!7 (X6!10 X3))
% 0.17/0.46 (event X2!7 (X7!9 X3))
% 0.17/0.46 (agent X2!7 (X7!9 X3) (X6!10 X3))
% 0.17/0.46 (patient X2!7 (X7!9 X3) (X5!11 X3))
% 0.17/0.46 (past X2!7 (X7!9 X3))
% 0.17/0.46 (nonreflexive X2!7 (X7!9 X3))
% 0.17/0.46 (drink X2!7 (X7!9 X3))
% 0.17/0.46 (event X2!7 (X8!8 X3))
% 0.17/0.46 (agent X2!7 (X8!8 X3) X3)
% 0.17/0.46 (patient X2!7 (X8!8 X3) (X6!10 X3))
% 0.17/0.46 (past X2!7 (X8!8 X3))
% 0.17/0.46 (nonreflexive X2!7 (X8!8 X3))
% 0.17/0.46 (see X2!7 (X8!8 X3)))))
% 0.17/0.46 (monotonicity (refl (~ a!1 a!1))
% 0.17/0.46 (sk (~ a!2 a!3))
% 0.17/0.46 (~ (or a!1 a!2) (or a!1 a!3))))))
% 0.17/0.46 (a!17 (forall ((X3 $i) (X4 $i))
% 0.17/0.46 (let ((a!1 (not (and (customer X2!7 X3)
% 0.17/0.46 (restaurant X2!7 X4)
% 0.17/0.46 (in X2!7 X3 X4))))
% 0.17/0.46 (a!2 (and (coffee X2!7 (X5!11 X3))
% 0.17/0.46 (human_person X2!7 (X6!10 X3))
% 0.17/0.46 (event X2!7 (X7!9 X3))
% 0.17/0.46 (agent X2!7 (X7!9 X3) (X6!10 X3))
% 0.17/0.46 (patient X2!7 (X7!9 X3) (X5!11 X3))
% 0.17/0.46 (past X2!7 (X7!9 X3))
% 0.17/0.46 (nonreflexive X2!7 (X7!9 X3))
% 0.17/0.46 (drink X2!7 (X7!9 X3))
% 0.17/0.46 (event X2!7 (X8!8 X3))
% 0.17/0.46 (agent X2!7 (X8!8 X3) X3)
% 0.17/0.46 (patient X2!7 (X8!8 X3) (X6!10 X3))
% 0.17/0.46 (past X2!7 (X8!8 X3))
% 0.17/0.46 (nonreflexive X2!7 (X8!8 X3))
% 0.17/0.46 (see X2!7 (X8!8 X3)))))
% 0.17/0.46 (or a!1 a!2))))
% 0.17/0.46 (a!21 (lambda ((U $i))
% 0.17/0.46 (let ((a!1 (refl (~ (not (actual_world U)) (not (actual_world U)))))
% 0.17/0.46 (a!2 (forall ((V $i) (W $i))
% 0.17/0.46 (let ((a!1 (not (and (customer U V)
% 0.17/0.46 (restaurant U W)
% 0.17/0.46 (in U V W)))))
% 0.17/0.46 (or a!1
% 0.17/0.46 (exists ((X $i) (Y $i) (Z $i) (X1 $i))
% 0.17/0.46 (and (human_person U X)
% 0.17/0.46 (coffee U Y)
% 0.17/0.46 (event U Z)
% 0.17/0.46 (agent U Z X)
% 0.17/0.46 (patient U Z Y)
% 0.17/0.46 (past U Z)
% 0.17/0.46 (nonreflexive U Z)
% 0.17/0.46 (drink U Z)
% 0.17/0.46 (event U X1)
% 0.17/0.46 (agent U X1 V)
% 0.17/0.46 (patient U X1 X)
% 0.17/0.46 (past U X1)
% 0.17/0.46 (nonreflexive U X1)
% 0.17/0.46 (see U X1)))))))
% 0.17/0.46 (a!3 (and (customer U (V!13 U))
% 0.17/0.46 (restaurant U (W!12 U))
% 0.17/0.46 (in U (V!13 U) (W!12 U))))
% 0.17/0.46 (a!4 (exists ((X $i) (Y $i) (Z $i) (X1 $i))
% 0.17/0.46 (and (human_person U X)
% 0.17/0.46 (coffee U Y)
% 0.17/0.46 (event U Z)
% 0.17/0.46 (agent U Z X)
% 0.17/0.46 (patient U Z Y)
% 0.17/0.46 (past U Z)
% 0.17/0.46 (nonreflexive U Z)
% 0.17/0.46 (drink U Z)
% 0.17/0.46 (event U X1)
% 0.17/0.46 (agent U X1 (V!13 U))
% 0.17/0.46 (patient U X1 X)
% 0.17/0.46 (past U X1)
% 0.17/0.46 (nonreflexive U X1)
% 0.17/0.46 (see U X1))))
% 0.17/0.46 (a!6 (lambda ((X $i) (Y $i) (Z $i) (X1 $i))
% 0.17/0.46 (let ((a!1 (and (human_person U X)
% 0.17/0.46 (coffee U Y)
% 0.17/0.46 (event U Z)
% 0.17/0.46 (agent U Z X)
% 0.17/0.46 (patient U Z Y)
% 0.17/0.46 (past U Z)
% 0.17/0.46 (nonreflexive U Z)
% 0.17/0.46 (drink U Z)
% 0.17/0.46 (event U X1)
% 0.17/0.46 (agent U X1 (V!13 U))
% 0.17/0.46 (patient U X1 X)
% 0.17/0.46 (past U X1)
% 0.17/0.46 (nonreflexive U X1)
% 0.17/0.46 (see U X1))))
% 0.17/0.46 (refl (~ (not a!1) (not a!1))))))
% 0.17/0.46 (a!7 (forall ((X $i) (Y $i) (Z $i) (X1 $i))
% 0.17/0.46 (let ((a!1 (and (human_person U X)
% 0.17/0.46 (coffee U Y)
% 0.17/0.46 (event U Z)
% 0.17/0.46 (agent U Z X)
% 0.17/0.46 (patient U Z Y)
% 0.17/0.46 (past U Z)
% 0.17/0.46 (nonreflexive U Z)
% 0.17/0.46 (drink U Z)
% 0.17/0.46 (event U X1)
% 0.17/0.46 (agent U X1 (V!13 U))
% 0.17/0.46 (patient U X1 X)
% 0.17/0.46 (past U X1)
% 0.17/0.46 (nonreflexive U X1)
% 0.17/0.46 (see U X1))))
% 0.17/0.46 (not a!1)))))
% 0.17/0.46 (let ((a!5 (~ (not a!2) (not (or (not a!3) a!4))))
% 0.17/0.46 (a!8 (~ (not (or (not a!3) a!4)) (and a!3 a!7)))
% 0.17/0.46 (a!10 (~ (not (and (actual_world U) a!2))
% 0.17/0.46 (or (not (actual_world U)) (and a!3 a!7)))))
% 0.17/0.46 (let ((a!9 (nnf-neg (refl (~ a!3 a!3))
% 0.17/0.46 (nnf-neg (proof-bind a!6) (~ (not a!4) a!7))
% 0.17/0.46 a!8)))
% 0.17/0.46 (nnf-neg a!1
% 0.17/0.46 (trans (sk a!5) a!9 (~ (not a!2) (and a!3 a!7)))
% 0.17/0.46 a!10))))))
% 0.17/0.46 (a!22 (forall ((U $i))
% 0.17/0.46 (let ((a!1 (and (customer U (V!13 U))
% 0.17/0.46 (restaurant U (W!12 U))
% 0.17/0.46 (in U (V!13 U) (W!12 U))))
% 0.17/0.46 (a!2 (forall ((X $i) (Y $i) (Z $i) (X1 $i))
% 0.17/0.46 (let ((a!1 (and (human_person U X)
% 0.17/0.46 (coffee U Y)
% 0.17/0.46 (event U Z)
% 0.17/0.46 (agent U Z X)
% 0.17/0.46 (patient U Z Y)
% 0.17/0.46 (past U Z)
% 0.17/0.46 (nonreflexive U Z)
% 0.17/0.46 (drink U Z)
% 0.17/0.46 (event U X1)
% 0.17/0.46 (agent U X1 (V!13 U))
% 0.17/0.46 (patient U X1 X)
% 0.17/0.46 (past U X1)
% 0.17/0.46 (nonreflexive U X1)
% 0.17/0.46 (see U X1))))
% 0.17/0.46 (not a!1)))))
% 0.17/0.46 (or (not (actual_world U)) (and a!1 a!2))))))
% 0.17/0.46 (let ((a!3 (sk (~ a!1 (and (actual_world U!0) a!2))))
% 0.17/0.46 (a!6 (monotonicity (refl (~ (actual_world U!0) (actual_world U!0)))
% 0.17/0.46 (nnf-pos (proof-bind a!4) (~ a!2 a!5))
% 0.17/0.46 (~ (and (actual_world U!0) a!2)
% 0.17/0.46 (and (actual_world U!0) a!5))))
% 0.17/0.46 (a!12 (~ (not (or (not a!1) a!10))
% 0.17/0.46 (and (and (actual_world U!0) a!5) a!11)))
% 0.17/0.46 (a!15 (sk (~ a!10 (and (actual_world X2!7) a!14))))
% 0.17/0.46 (a!18 (monotonicity (refl (~ (actual_world X2!7) (actual_world X2!7)))
% 0.17/0.46 (nnf-pos (proof-bind a!16) (~ a!14 a!17))
% 0.17/0.46 (~ (and (actual_world X2!7) a!14)
% 0.17/0.46 (and (actual_world X2!7) a!17))))
% 0.17/0.46 (a!23 (~ (not (or (not a!10) a!1))
% 0.17/0.46 (and (and (actual_world X2!7) a!17) a!22)))
% 0.17/0.46 (a!25 (not (and (or (not a!1) a!10) (or (not a!10) a!1))))
% 0.17/0.46 (a!26 (or (and (and (actual_world U!0) a!5) a!11)
% 0.17/0.46 (and (and (actual_world X2!7) a!17) a!22))))
% 0.17/0.46 (let ((a!7 (trans a!3 a!6 (~ a!1 (and (actual_world U!0) a!5))))
% 0.17/0.46 (a!19 (trans a!15 a!18 (~ a!10 (and (actual_world X2!7) a!17)))))
% 0.17/0.46 (let ((a!8 (nnf-neg a!7 (~ (not (not a!1)) (and (actual_world U!0) a!5))))
% 0.17/0.46 (a!20 (nnf-neg a!19 (~ (not (not a!10)) (and (actual_world X2!7) a!17)))))
% 0.17/0.46 (let ((a!13 (nnf-neg a!8 (nnf-neg (proof-bind a!9) (~ (not a!10) a!11)) a!12))
% 0.17/0.46 (a!24 (nnf-neg a!20 (nnf-neg (proof-bind a!21) (~ (not a!1) a!22)) a!23)))
% 0.17/0.46 (nnf-neg a!13 a!24 (~ a!25 a!26)))))))
% 0.17/0.46 Proof display could not be completed: unexpected number of arguments
% 0.17/0.46 % E exiting
%------------------------------------------------------------------------------