%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : PUZ001+2 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n010.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:23:06 AM UTC 2025
% Result : Theorem 1.08s 1.23s
% Output : Proof 1.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : PUZ001+2 : TPTP v9.0.0. Released v4.0.0.
% 0.06/0.12 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n010.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 02:40:56 EDT 2025
% 0.11/0.33 % CPUTime :
% 1.08/1.23 % SZS status Theorem
% 1.08/1.23 % SZS output start Proof
% 1.08/1.23 tff(predicate2_type, type, (
% 1.08/1.23 predicate2: ( $i * $i * $i * $i ) > $o)).
% 1.08/1.23 tff(tptp_fun_A1_7_type, type, (
% 1.08/1.23 tptp_fun_A1_7: $i > $i)).
% 1.08/1.23 tff(tptp_fun__Butler__type, type, (
% 1.08/1.23 tptp_fun__Butler_: $i)).
% 1.08/1.23 tff(hate_type, type, (
% 1.08/1.23 hate: $i)).
% 1.08/1.23 tff(tptp_fun_Y_6_type, type, (
% 1.08/1.23 tptp_fun_Y_6: $i > $i)).
% 1.08/1.23 tff(tptp_fun__AuntAgatha__type, type, (
% 1.08/1.23 tptp_fun__AuntAgatha_: $i)).
% 1.08/1.23 tff(tptp_fun_S_4_type, type, (
% 1.08/1.23 tptp_fun_S_4: $i > $i)).
% 1.08/1.23 tff(tptp_fun_A_2_type, type, (
% 1.08/1.23 tptp_fun_A_2: $i)).
% 1.08/1.23 tff(kill_type, type, (
% 1.08/1.23 kill: $i)).
% 1.08/1.23 tff(tptp_fun_C_0_type, type, (
% 1.08/1.23 tptp_fun_C_0: $i)).
% 1.08/1.23 tff(tptp_fun_V_5_type, type, (
% 1.08/1.23 tptp_fun_V_5: $i > $i)).
% 1.08/1.23 tff(property2_type, type, (
% 1.08/1.23 property2: ( $i * $i * $i * $i ) > $o)).
% 1.08/1.23 tff(comp_than_type, type, (
% 1.08/1.23 comp_than: $i)).
% 1.08/1.23 tff(rich_type, type, (
% 1.08/1.23 rich: $i)).
% 1.08/1.23 tff(tptp_fun__Charles__type, type, (
% 1.08/1.23 tptp_fun__Charles_: $i)).
% 1.08/1.23 tff(tptp_fun_I_3_type, type, (
% 1.08/1.23 tptp_fun_I_3: ( $i * $i ) > $i)).
% 1.08/1.23 tff(modifier_pp_type, type, (
% 1.08/1.23 modifier_pp: ( $i * $i * $i ) > $o)).
% 1.08/1.24 tff(tptp_fun__DreadburyMansion__type, type, (
% 1.08/1.24 tptp_fun__DreadburyMansion_: $i)).
% 1.08/1.24 tff(in_type, type, (
% 1.08/1.24 in: $i)).
% 1.08/1.24 tff(predicate1_type, type, (
% 1.08/1.24 predicate1: ( $i * $i * $i ) > $o)).
% 1.08/1.24 tff(live_type, type, (
% 1.08/1.24 live: $i)).
% 1.08/1.24 tff(tptp_fun_B_1_type, type, (
% 1.08/1.24 tptp_fun_B_1: $i)).
% 1.08/1.24 tff(1,assumption,(A!2 = |'AuntAgatha'|), introduced(assumption)).
% 1.08/1.24 tff(2,plain,
% 1.08/1.24 (predicate2(C!0, kill, A!2, |'AuntAgatha'|) <=> predicate2(C!0, kill, |'AuntAgatha'|, |'AuntAgatha'|)),
% 1.08/1.24 inference(monotonicity,[status(thm)],[1])).
% 1.08/1.24 tff(3,plain,
% 1.08/1.24 (predicate2(C!0, kill, |'AuntAgatha'|, |'AuntAgatha'|) <=> predicate2(C!0, kill, A!2, |'AuntAgatha'|)),
% 1.08/1.24 inference(symmetry,[status(thm)],[2])).
% 1.08/1.24 tff(4,plain,
% 1.08/1.24 ((~predicate2(C!0, kill, |'AuntAgatha'|, |'AuntAgatha'|)) <=> (~predicate2(C!0, kill, A!2, |'AuntAgatha'|))),
% 1.08/1.24 inference(monotonicity,[status(thm)],[3])).
% 1.08/1.24 tff(5,plain,
% 1.08/1.24 (^[A: $i] : refl((~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)) <=> (~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)))),
% 1.08/1.24 inference(bind,[status(th)],[])).
% 1.08/1.24 tff(6,plain,
% 1.08/1.24 (![A: $i] : (~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)) <=> ![A: $i] : (~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|))),
% 1.08/1.24 inference(quant_intro,[status(thm)],[5])).
% 1.08/1.24 tff(7,plain,
% 1.08/1.24 ((~?[A: $i] : predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)) <=> (~?[A: $i] : predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|))),
% 1.08/1.24 inference(rewrite,[status(thm)],[])).
% 1.08/1.24 tff(8,axiom,(~?[A: $i] : predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove')).
% 1.08/1.24 tff(9,plain,
% 1.08/1.24 (~?[A: $i] : predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)),
% 1.08/1.24 inference(modus_ponens,[status(thm)],[8, 7])).
% 1.08/1.24 tff(10,plain,
% 1.08/1.24 (~?[A: $i] : predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)),
% 1.08/1.24 inference(modus_ponens,[status(thm)],[9, 7])).
% 1.08/1.24 tff(11,plain,
% 1.08/1.24 (~?[A: $i] : predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)),
% 1.08/1.24 inference(modus_ponens,[status(thm)],[10, 7])).
% 1.08/1.24 tff(12,plain,
% 1.08/1.24 (~?[A: $i] : predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)),
% 1.08/1.24 inference(modus_ponens,[status(thm)],[11, 7])).
% 1.08/1.24 tff(13,plain,
% 1.08/1.24 (^[A: $i] : refl($oeq((~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|)), (~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|))))),
% 1.08/1.24 inference(bind,[status(th)],[])).
% 1.08/1.24 tff(14,plain,(
% 1.08/1.24 ![A: $i] : (~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|))),
% 1.08/1.24 inference(nnf-neg,[status(sab)],[12, 13])).
% 1.08/1.24 tff(15,plain,
% 1.08/1.24 (![A: $i] : (~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|))),
% 1.08/1.24 inference(modus_ponens,[status(thm)],[14, 6])).
% 1.08/1.24 tff(16,plain,
% 1.08/1.24 ((~![A: $i] : (~predicate2(A, kill, |'AuntAgatha'|, |'AuntAgatha'|))) | (~predicate2(C!0, kill, |'AuntAgatha'|, |'AuntAgatha'|))),
% 1.08/1.24 inference(quant_inst,[status(thm)],[])).
% 1.08/1.24 tff(17,plain,
% 1.08/1.24 (~predicate2(C!0, kill, |'AuntAgatha'|, |'AuntAgatha'|)),
% 1.08/1.24 inference(unit_resolution,[status(thm)],[16, 15])).
% 1.08/1.24 tff(18,plain,
% 1.08/1.24 (~predicate2(C!0, kill, A!2, |'AuntAgatha'|)),
% 1.08/1.24 inference(modus_ponens,[status(thm)],[17, 4])).
% 1.08/1.24 tff(19,plain,
% 1.08/1.24 ((predicate1(B!1, live, A!2) & modifier_pp(B!1, in, |'DreadburyMansion'|) & predicate2(C!0, kill, A!2, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G)) & ![J: $i] : ![K: $i, L: $i] : (~(predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))) & ![Q: $i] : (~predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W)) & ![Z: $i] : ![B1: $i] : (~predicate2(B1, hate, Z, tptp_fun_A1_7(Z))) & (~(|'AuntAgatha'| = |'Butler'|))) <=> (predicate1(B!1, live, A!2) & modifier_pp(B!1, in, |'DreadburyMansion'|) & predicate2(C!0, kill, A!2, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G)) & ![J: $i, K: $i, L: $i] : (~(predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))) & ![Q: $i] : (~predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W)) & ![Z: $i, B1: $i] : (~predicate2(B1, hate, Z, tptp_fun_A1_7(Z))) & (~(|'AuntAgatha'| = |'Butler'|)))),
% 1.08/1.24 inference(rewrite,[status(thm)],[])).
% 1.08/1.24 tff(20,plain,
% 1.08/1.24 (?[A: $i, B: $i, C: $i] : (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)) & (~(|'AuntAgatha'| = |'Butler'|))) <=> ?[A: $i, B: $i, C: $i] : (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)) & (~(|'AuntAgatha'| = |'Butler'|)))),
% 1.08/1.24 inference(rewrite,[status(thm)],[])).
% 1.08/1.24 tff(21,plain,
% 1.08/1.24 (^[A: $i, B: $i, C: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|))), (((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|))), (((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|)))), quant_intro(proof_bind(^[D: $i, E: $i] : trans(monotonicity(rewrite((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) <=> (predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))), rewrite((((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)) <=> ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|))), (((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|))) <=> ((predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)) => ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|))))), rewrite(((predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)) => ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|))) <=> ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))))), (((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|))) <=> ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))))))), (![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|))) <=> ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))))), ((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))))), ((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))))))), trans(quant_intro(proof_bind(^[F: $i] : trans(monotonicity(quant_intro(proof_bind(^[G: $i, H: $i] : trans(monotonicity(rewrite(($true & predicate2(H, kill, F, G)) <=> predicate2(H, kill, F, G)), ((($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)) <=> (predicate2(H, kill, F, G) => ?[I: $i] : predicate2(I, hate, F, G)))), rewrite((predicate2(H, kill, F, G) => ?[I: $i] : predicate2(I, hate, F, G)) <=> ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))), ((($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)) <=> ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))))), (![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)) <=> ![G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)))), (($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G))) <=> ($true => ![G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))))), rewrite(($true => ![G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))) <=> ![G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))), (($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G))) <=> ![G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))))), (![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G))) <=> ![F: $i] : ![G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)))), pull_quant(![F: $i] : ![G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) <=> ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))), (![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G))) <=> ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)))), (((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)))), (((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))))), quant_intro(proof_bind(^[J: $i] : trans(monotonicity(rewrite((~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))) <=> (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))), (($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M)))) <=> ($true => (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))))), rewrite(($true => (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))) <=> (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))), (($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M)))) <=> (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))))), (![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M)))) <=> ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))))), ((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G))) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))))), ((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))))), quant_intro(proof_bind(^[N: $i, O: $i] : trans(monotonicity(rewrite(($true & predicate2(O, hate, |'AuntAgatha'|, N)) <=> predicate2(O, hate, |'AuntAgatha'|, N)), rewrite((~?[P: $i] : predicate2(P, hate, |'Charles'|, N)) <=> (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))), ((($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) <=> (predicate2(O, hate, |'AuntAgatha'|, N) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))))), rewrite((predicate2(O, hate, |'AuntAgatha'|, N) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) <=> ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))), ((($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) <=> ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))))), (![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) <=> ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))))), (((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))))), (((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))))), rewrite((~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) <=> (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))), ((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)))), ((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))))), quant_intro(proof_bind(^[R: $i] : trans(monotonicity(rewrite(($true & (~(R = |'Butler'|))) <=> (~(R = |'Butler'|))), ((($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) <=> ((~(R = |'Butler'|)) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)))), rewrite(((~(R = |'Butler'|)) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) <=> ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))), ((($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) <=> ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))))), (![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) <=> ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)))), (((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)))), (((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))))), quant_intro(proof_bind(^[T: $i] : trans(monotonicity(trans(monotonicity(rewrite((~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U))) <=> (~property2(T, rich, comp_than, |'AuntAgatha'|))), (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) <=> ($true & (~property2(T, rich, comp_than, |'AuntAgatha'|))))), rewrite(($true & (~property2(T, rich, comp_than, |'AuntAgatha'|))) <=> (~property2(T, rich, comp_than, |'AuntAgatha'|))), (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) <=> (~property2(T, rich, comp_than, |'AuntAgatha'|)))), ((($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) <=> ((~property2(T, rich, comp_than, |'AuntAgatha'|)) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T)))), rewrite(((~property2(T, rich, comp_than, |'AuntAgatha'|)) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) <=> (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T))), ((($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) <=> (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T))))), (![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) <=> ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)))), ((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)))), ((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T))))), quant_intro(proof_bind(^[W: $i, X: $i] : trans(monotonicity(rewrite(($true & predicate2(X, hate, |'AuntAgatha'|, W)) <=> predicate2(X, hate, |'AuntAgatha'|, W)), ((($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) <=> (predicate2(X, hate, |'AuntAgatha'|, W) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)))), rewrite((predicate2(X, hate, |'AuntAgatha'|, W) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) <=> ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))), ((($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) <=> ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))))), (![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) <=> ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)))), (((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)))), (((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))))), quant_intro(proof_bind(^[Z: $i] : trans(monotonicity(rewrite((~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1))) <=> (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))), (($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1)))) <=> ($true => (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))))), rewrite(($true => (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))) <=> (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))), (($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1)))) <=> (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))))), (![Z: $i] : ($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1)))) <=> ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)))), ((((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) & ![Z: $i] : ($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1))))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)))), ((((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) & ![Z: $i] : ($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1))))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))))), (((((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) & ![Z: $i] : ($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1))))) & (~(|'AuntAgatha'| = |'Butler'|))) <=> ((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))) & (~(|'AuntAgatha'| = |'Butler'|))))), rewrite(((predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1))) & (~(|'AuntAgatha'| = |'Butler'|))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)) & (~(|'AuntAgatha'| = |'Butler'|)))), (((((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) & ![Z: $i] : ($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1))))) & (~(|'AuntAgatha'| = |'Butler'|))) <=> (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)) & (~(|'AuntAgatha'| = |'Butler'|)))))),
% 1.08/1.26 inference(bind,[status(th)],[])).
% 1.08/1.26 tff(22,plain,
% 1.08/1.26 (?[A: $i, B: $i, C: $i] : ((((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) & ![Z: $i] : ($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1))))) & (~(|'AuntAgatha'| = |'Butler'|))) <=> ?[A: $i, B: $i, C: $i] : (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)) & (~(|'AuntAgatha'| = |'Butler'|)))),
% 1.08/1.26 inference(quant_intro,[status(thm)],[21])).
% 1.08/1.26 tff(23,axiom,(?[A: $i, B: $i, C: $i] : ((((((((((((($true & predicate1(B, live, A)) & modifier_pp(B, in, |'DreadburyMansion'|)) & predicate2(C, kill, A, |'AuntAgatha'|)) & ![D: $i, E: $i] : ((($true & predicate1(E, live, D)) & modifier_pp(E, in, |'DreadburyMansion'|)) => (((D = |'AuntAgatha'|) | (D = |'Butler'|)) | (D = |'Charles'|)))) & ![F: $i] : ($true => ![G: $i, H: $i] : (($true & predicate2(H, kill, F, G)) => ?[I: $i] : predicate2(I, hate, F, G)))) & ![J: $i] : ($true => (~?[K: $i, L: $i, M: $i] : ((($true & predicate2(L, kill, J, K)) & property2(M, rich, comp_than, K)) & (J = M))))) & ![N: $i, O: $i] : (($true & predicate2(O, hate, |'AuntAgatha'|, N)) => (~?[P: $i] : predicate2(P, hate, |'Charles'|, N)))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|))) & ![R: $i] : (($true & (~(R = |'Butler'|))) => ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R))) & ![T: $i] : (($true & (~?[U: $i] : (property2(U, rich, comp_than, |'AuntAgatha'|) & (T = U)))) => ?[V: $i] : predicate2(V, hate, |'Butler'|, T))) & ![W: $i, X: $i] : (($true & predicate2(X, hate, |'AuntAgatha'|, W)) => ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W))) & ![Z: $i] : ($true => (~![A1: $i] : ($true => ?[B1: $i] : predicate2(B1, hate, Z, A1))))) & (~(|'AuntAgatha'| = |'Butler'|)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','background')).
% 1.08/1.26 tff(24,plain,
% 1.08/1.26 (?[A: $i, B: $i, C: $i] : (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)) & (~(|'AuntAgatha'| = |'Butler'|)))),
% 1.08/1.26 inference(modus_ponens,[status(thm)],[23, 22])).
% 1.08/1.26 tff(25,plain,
% 1.08/1.26 (?[A: $i, B: $i, C: $i] : (predicate1(B, live, A) & modifier_pp(B, in, |'DreadburyMansion'|) & predicate2(C, kill, A, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | ?[I: $i] : predicate2(I, hate, F, G)) & ![J: $i] : (~?[K: $i, L: $i] : (predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | (~?[P: $i] : predicate2(P, hate, |'Charles'|, N))) & (~?[Q: $i] : predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | ?[S: $i] : predicate2(S, hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | ?[V: $i] : predicate2(V, hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | ?[Y: $i] : predicate2(Y, hate, |'Butler'|, W)) & ![Z: $i] : (~![A1: $i] : ?[B1: $i] : predicate2(B1, hate, Z, A1)) & (~(|'AuntAgatha'| = |'Butler'|)))),
% 1.08/1.26 inference(modus_ponens,[status(thm)],[24, 20])).
% 1.08/1.26 tff(26,plain,
% 1.08/1.26 (predicate1(B!1, live, A!2) & modifier_pp(B!1, in, |'DreadburyMansion'|) & predicate2(C!0, kill, A!2, |'AuntAgatha'|) & ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) & ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G)) & ![J: $i, K: $i, L: $i] : (~(predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) & ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))) & ![Q: $i] : (~predicate2(Q, hate, |'AuntAgatha'|, |'Butler'|)) & ![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R)) & ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T)) & ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W)) & ![Z: $i, B1: $i] : (~predicate2(B1, hate, Z, tptp_fun_A1_7(Z))) & (~(|'AuntAgatha'| = |'Butler'|))),
% 1.08/1.26 inference(modus_ponens,[status(thm)],[25, 19])).
% 1.08/1.26 tff(27,plain,
% 1.08/1.26 (predicate2(C!0, kill, A!2, |'AuntAgatha'|)),
% 1.08/1.26 inference(and_elim,[status(thm)],[26])).
% 1.08/1.26 tff(28,plain,
% 1.08/1.26 ($false),
% 1.08/1.26 inference(unit_resolution,[status(thm)],[27, 18])).
% 1.08/1.26 tff(29,plain,(~(A!2 = |'AuntAgatha'|)), inference(lemma,lemma(discharge,[]))).
% 1.08/1.26 tff(30,assumption,(A!2 = |'Charles'|), introduced(assumption)).
% 1.08/1.26 tff(31,plain,
% 1.08/1.26 (predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|) <=> predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, |'Charles'|, |'AuntAgatha'|)),
% 1.08/1.26 inference(monotonicity,[status(thm)],[30])).
% 1.08/1.26 tff(32,plain,
% 1.08/1.26 (predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, |'Charles'|, |'AuntAgatha'|) <=> predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|)),
% 1.08/1.26 inference(symmetry,[status(thm)],[31])).
% 1.08/1.26 tff(33,plain,
% 1.08/1.26 ((~predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, |'Charles'|, |'AuntAgatha'|)) <=> (~predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|))),
% 1.08/1.26 inference(monotonicity,[status(thm)],[32])).
% 1.08/1.26 tff(34,plain,
% 1.08/1.26 (~(|'AuntAgatha'| = |'Butler'|)),
% 1.08/1.26 inference(and_elim,[status(thm)],[26])).
% 1.08/1.26 tff(35,plain,
% 1.08/1.26 (![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))),
% 1.08/1.26 inference(and_elim,[status(thm)],[26])).
% 1.08/1.26 tff(36,plain,
% 1.08/1.26 (((~![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))) | ((|'AuntAgatha'| = |'Butler'|) | predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|))) <=> ((~![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))) | (|'AuntAgatha'| = |'Butler'|) | predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|))),
% 1.08/1.26 inference(rewrite,[status(thm)],[])).
% 1.08/1.26 tff(37,plain,
% 1.08/1.26 ((~![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))) | ((|'AuntAgatha'| = |'Butler'|) | predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|))),
% 1.08/1.26 inference(quant_inst,[status(thm)],[])).
% 1.08/1.26 tff(38,plain,
% 1.08/1.26 ((~![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))) | (|'AuntAgatha'| = |'Butler'|) | predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|)),
% 1.08/1.26 inference(modus_ponens,[status(thm)],[37, 36])).
% 1.08/1.26 tff(39,plain,
% 1.08/1.26 (predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|)),
% 1.08/1.26 inference(unit_resolution,[status(thm)],[38, 35, 34])).
% 1.08/1.26 tff(40,plain,
% 1.08/1.26 (^[N: $i, O: $i] : refl(((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))) <=> ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))))),
% 1.08/1.26 inference(bind,[status(th)],[])).
% 1.08/1.26 tff(41,plain,
% 1.08/1.26 (![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))) <=> ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))),
% 1.08/1.26 inference(quant_intro,[status(thm)],[40])).
% 1.08/1.26 tff(42,plain,
% 1.08/1.26 (^[N: $i, O: $i] : rewrite(((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))) <=> ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))))),
% 1.08/1.26 inference(bind,[status(th)],[])).
% 1.08/1.26 tff(43,plain,
% 1.08/1.26 (![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))) <=> ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))),
% 1.08/1.26 inference(quant_intro,[status(thm)],[42])).
% 1.08/1.26 tff(44,plain,
% 1.08/1.26 (![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N))) <=> ![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))),
% 1.08/1.26 inference(transitivity,[status(thm)],[43, 41])).
% 1.08/1.26 tff(45,plain,
% 1.08/1.26 (![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))),
% 1.08/1.26 inference(and_elim,[status(thm)],[26])).
% 1.08/1.26 tff(46,plain,
% 1.08/1.26 (![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))),
% 1.08/1.26 inference(modus_ponens,[status(thm)],[45, 44])).
% 1.08/1.26 tff(47,plain,
% 1.08/1.26 (((~![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))) | ((~predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, |'AuntAgatha'|)))) <=> ((~![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))) | (~predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, |'AuntAgatha'|)))),
% 1.08/1.26 inference(rewrite,[status(thm)],[])).
% 1.08/1.26 tff(48,plain,
% 1.08/1.26 ((~![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))) | ((~predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, |'AuntAgatha'|)))),
% 1.08/1.26 inference(quant_inst,[status(thm)],[])).
% 1.08/1.26 tff(49,plain,
% 1.08/1.26 ((~![N: $i, O: $i] : ((~predicate2(O, hate, |'AuntAgatha'|, N)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, N)))) | (~predicate2(tptp_fun_S_4(|'AuntAgatha'|), hate, |'AuntAgatha'|, |'AuntAgatha'|)) | ![P: $i] : (~predicate2(P, hate, |'Charles'|, |'AuntAgatha'|))),
% 1.08/1.26 inference(modus_ponens,[status(thm)],[48, 47])).
% 1.08/1.26 tff(50,plain,
% 1.08/1.26 (![P: $i] : (~predicate2(P, hate, |'Charles'|, |'AuntAgatha'|))),
% 1.08/1.26 inference(unit_resolution,[status(thm)],[49, 46, 39])).
% 1.08/1.26 tff(51,plain,
% 1.08/1.26 ((~![P: $i] : (~predicate2(P, hate, |'Charles'|, |'AuntAgatha'|))) | (~predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, |'Charles'|, |'AuntAgatha'|))),
% 1.08/1.26 inference(quant_inst,[status(thm)],[])).
% 1.08/1.26 tff(52,plain,
% 1.08/1.26 (~predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, |'Charles'|, |'AuntAgatha'|)),
% 1.08/1.26 inference(unit_resolution,[status(thm)],[51, 50])).
% 1.08/1.26 tff(53,plain,
% 1.08/1.26 (~predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|)),
% 1.08/1.26 inference(modus_ponens,[status(thm)],[52, 33])).
% 1.08/1.26 tff(54,plain,
% 1.08/1.26 (^[F: $i, G: $i, H: $i] : refl(((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G)) <=> ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G)))),
% 1.08/1.26 inference(bind,[status(th)],[])).
% 1.08/1.26 tff(55,plain,
% 1.08/1.26 (![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G)) <=> ![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G))),
% 1.08/1.26 inference(quant_intro,[status(thm)],[54])).
% 1.08/1.26 tff(56,plain,
% 1.08/1.26 (![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G))),
% 1.08/1.27 inference(and_elim,[status(thm)],[26])).
% 1.08/1.27 tff(57,plain,
% 1.08/1.27 (![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[56, 55])).
% 1.08/1.27 tff(58,plain,
% 1.08/1.27 (((~![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G))) | ((~predicate2(C!0, kill, A!2, |'AuntAgatha'|)) | predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|))) <=> ((~![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G))) | (~predicate2(C!0, kill, A!2, |'AuntAgatha'|)) | predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|))),
% 1.08/1.27 inference(rewrite,[status(thm)],[])).
% 1.08/1.27 tff(59,plain,
% 1.08/1.27 ((~![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G))) | ((~predicate2(C!0, kill, A!2, |'AuntAgatha'|)) | predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|))),
% 1.08/1.27 inference(quant_inst,[status(thm)],[])).
% 1.08/1.27 tff(60,plain,
% 1.08/1.27 ((~![F: $i, G: $i, H: $i] : ((~predicate2(H, kill, F, G)) | predicate2(tptp_fun_I_3(G, F), hate, F, G))) | (~predicate2(C!0, kill, A!2, |'AuntAgatha'|)) | predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|)),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[59, 58])).
% 1.08/1.27 tff(61,plain,
% 1.08/1.27 (predicate2(tptp_fun_I_3(|'AuntAgatha'|, A!2), hate, A!2, |'AuntAgatha'|)),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[60, 27, 57])).
% 1.08/1.27 tff(62,plain,
% 1.08/1.27 ($false),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[61, 53])).
% 1.08/1.27 tff(63,plain,(~(A!2 = |'Charles'|)), inference(lemma,lemma(discharge,[]))).
% 1.08/1.27 tff(64,plain,
% 1.08/1.27 (^[D: $i, E: $i] : refl(((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|))) <=> ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|))))),
% 1.08/1.27 inference(bind,[status(th)],[])).
% 1.08/1.27 tff(65,plain,
% 1.08/1.27 (![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|))) <=> ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))),
% 1.08/1.27 inference(quant_intro,[status(thm)],[64])).
% 1.08/1.27 tff(66,plain,
% 1.08/1.27 (^[D: $i, E: $i] : trans(monotonicity(trans(monotonicity(rewrite((predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)) <=> (~((~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|))))), ((~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))) <=> (~(~((~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|))))))), rewrite((~(~((~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|))))) <=> ((~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))), ((~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))) <=> ((~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|))))), (((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) <=> ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | ((~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))))), rewrite(((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | ((~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))) <=> ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))), (((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) <=> ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))))),
% 1.08/1.27 inference(bind,[status(th)],[])).
% 1.08/1.27 tff(67,plain,
% 1.08/1.27 (![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|)))) <=> ![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))),
% 1.08/1.27 inference(quant_intro,[status(thm)],[66])).
% 1.08/1.27 tff(68,plain,
% 1.08/1.27 (![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~(predicate1(E, live, D) & modifier_pp(E, in, |'DreadburyMansion'|))))),
% 1.08/1.27 inference(and_elim,[status(thm)],[26])).
% 1.08/1.27 tff(69,plain,
% 1.08/1.27 (![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[68, 67])).
% 1.08/1.27 tff(70,plain,
% 1.08/1.27 (![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[69, 65])).
% 1.08/1.27 tff(71,plain,
% 1.08/1.27 (modifier_pp(B!1, in, |'DreadburyMansion'|)),
% 1.08/1.27 inference(and_elim,[status(thm)],[26])).
% 1.08/1.27 tff(72,plain,
% 1.08/1.27 (predicate1(B!1, live, A!2)),
% 1.08/1.27 inference(and_elim,[status(thm)],[26])).
% 1.08/1.27 tff(73,plain,
% 1.08/1.27 (((~![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))) | ((A!2 = |'Charles'|) | (A!2 = |'Butler'|) | (A!2 = |'AuntAgatha'|) | (~predicate1(B!1, live, A!2)) | (~modifier_pp(B!1, in, |'DreadburyMansion'|)))) <=> ((~![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))) | (A!2 = |'Charles'|) | (A!2 = |'Butler'|) | (A!2 = |'AuntAgatha'|) | (~predicate1(B!1, live, A!2)) | (~modifier_pp(B!1, in, |'DreadburyMansion'|)))),
% 1.08/1.27 inference(rewrite,[status(thm)],[])).
% 1.08/1.27 tff(74,plain,
% 1.08/1.27 ((~![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))) | ((A!2 = |'Charles'|) | (A!2 = |'Butler'|) | (A!2 = |'AuntAgatha'|) | (~predicate1(B!1, live, A!2)) | (~modifier_pp(B!1, in, |'DreadburyMansion'|)))),
% 1.08/1.27 inference(quant_inst,[status(thm)],[])).
% 1.08/1.27 tff(75,plain,
% 1.08/1.27 ((~![D: $i, E: $i] : ((D = |'Charles'|) | (D = |'Butler'|) | (D = |'AuntAgatha'|) | (~predicate1(E, live, D)) | (~modifier_pp(E, in, |'DreadburyMansion'|)))) | (A!2 = |'Charles'|) | (A!2 = |'Butler'|) | (A!2 = |'AuntAgatha'|) | (~predicate1(B!1, live, A!2)) | (~modifier_pp(B!1, in, |'DreadburyMansion'|))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[74, 73])).
% 1.08/1.27 tff(76,plain,
% 1.08/1.27 ((A!2 = |'Charles'|) | (A!2 = |'Butler'|) | (A!2 = |'AuntAgatha'|)),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[75, 72, 71, 70])).
% 1.08/1.27 tff(77,plain,
% 1.08/1.27 (A!2 = |'Butler'|),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[76, 63, 29])).
% 1.08/1.27 tff(78,assumption,(A!2 = |'Butler'|), introduced(assumption)).
% 1.08/1.27 tff(79,plain,
% 1.08/1.27 (|'Butler'| = A!2),
% 1.08/1.27 inference(symmetry,[status(thm)],[78])).
% 1.08/1.27 tff(80,assumption,(tptp_fun_A1_7(|'Butler'|) = |'Butler'|), introduced(assumption)).
% 1.08/1.27 tff(81,plain,
% 1.08/1.27 (tptp_fun_A1_7(|'Butler'|) = A!2),
% 1.08/1.27 inference(transitivity,[status(thm)],[80, 79])).
% 1.08/1.27 tff(82,plain,
% 1.08/1.27 (predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|)) <=> predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, A!2)),
% 1.08/1.27 inference(monotonicity,[status(thm)],[81])).
% 1.08/1.27 tff(83,plain,
% 1.08/1.27 (predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, A!2) <=> predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|))),
% 1.08/1.27 inference(symmetry,[status(thm)],[82])).
% 1.08/1.27 tff(84,plain,
% 1.08/1.27 (^[J: $i, K: $i, L: $i] : refl(((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K))) <=> ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K))))),
% 1.08/1.27 inference(bind,[status(th)],[])).
% 1.08/1.27 tff(85,plain,
% 1.08/1.27 (![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K))) <=> ![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))),
% 1.08/1.27 inference(quant_intro,[status(thm)],[84])).
% 1.08/1.27 tff(86,plain,
% 1.08/1.27 (^[J: $i, K: $i, L: $i] : trans(monotonicity(rewrite((predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)) <=> (~((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K))))), ((~(predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) <=> (~(~((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K))))))), rewrite((~(~((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K))))) <=> ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))), ((~(predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) <=> ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))))),
% 1.08/1.27 inference(bind,[status(th)],[])).
% 1.08/1.27 tff(87,plain,
% 1.08/1.27 (![J: $i, K: $i, L: $i] : (~(predicate2(L, kill, J, K) & property2(J, rich, comp_than, K))) <=> ![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))),
% 1.08/1.27 inference(quant_intro,[status(thm)],[86])).
% 1.08/1.27 tff(88,plain,
% 1.08/1.27 (![J: $i, K: $i, L: $i] : (~(predicate2(L, kill, J, K) & property2(J, rich, comp_than, K)))),
% 1.08/1.27 inference(and_elim,[status(thm)],[26])).
% 1.08/1.27 tff(89,plain,
% 1.08/1.27 (![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[88, 87])).
% 1.08/1.27 tff(90,plain,
% 1.08/1.27 (![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[89, 85])).
% 1.08/1.27 tff(91,plain,
% 1.08/1.27 (((~![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))) | ((~predicate2(C!0, kill, A!2, |'AuntAgatha'|)) | (~property2(A!2, rich, comp_than, |'AuntAgatha'|)))) <=> ((~![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))) | (~predicate2(C!0, kill, A!2, |'AuntAgatha'|)) | (~property2(A!2, rich, comp_than, |'AuntAgatha'|)))),
% 1.08/1.27 inference(rewrite,[status(thm)],[])).
% 1.08/1.27 tff(92,plain,
% 1.08/1.27 ((~![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))) | ((~predicate2(C!0, kill, A!2, |'AuntAgatha'|)) | (~property2(A!2, rich, comp_than, |'AuntAgatha'|)))),
% 1.08/1.27 inference(quant_inst,[status(thm)],[])).
% 1.08/1.27 tff(93,plain,
% 1.08/1.27 ((~![J: $i, K: $i, L: $i] : ((~predicate2(L, kill, J, K)) | (~property2(J, rich, comp_than, K)))) | (~predicate2(C!0, kill, A!2, |'AuntAgatha'|)) | (~property2(A!2, rich, comp_than, |'AuntAgatha'|))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[92, 91])).
% 1.08/1.27 tff(94,plain,
% 1.08/1.27 (~property2(A!2, rich, comp_than, |'AuntAgatha'|)),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[93, 27, 90])).
% 1.08/1.27 tff(95,plain,
% 1.08/1.27 (^[T: $i] : refl((property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T)) <=> (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T)))),
% 1.08/1.27 inference(bind,[status(th)],[])).
% 1.08/1.27 tff(96,plain,
% 1.08/1.27 (![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T)) <=> ![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T))),
% 1.08/1.27 inference(quant_intro,[status(thm)],[95])).
% 1.08/1.27 tff(97,plain,
% 1.08/1.27 (![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T))),
% 1.08/1.27 inference(and_elim,[status(thm)],[26])).
% 1.08/1.27 tff(98,plain,
% 1.08/1.27 (![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[97, 96])).
% 1.08/1.27 tff(99,plain,
% 1.08/1.27 (((~![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T))) | (property2(A!2, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, A!2))) <=> ((~![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T))) | property2(A!2, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, A!2))),
% 1.08/1.27 inference(rewrite,[status(thm)],[])).
% 1.08/1.27 tff(100,plain,
% 1.08/1.27 ((~![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T))) | (property2(A!2, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, A!2))),
% 1.08/1.27 inference(quant_inst,[status(thm)],[])).
% 1.08/1.27 tff(101,plain,
% 1.08/1.27 ((~![T: $i] : (property2(T, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(T), hate, |'Butler'|, T))) | property2(A!2, rich, comp_than, |'AuntAgatha'|) | predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, A!2)),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[100, 99])).
% 1.08/1.27 tff(102,plain,
% 1.08/1.27 (predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, A!2)),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[101, 98, 94])).
% 1.08/1.27 tff(103,plain,
% 1.08/1.27 (predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[102, 83])).
% 1.08/1.27 tff(104,plain,
% 1.08/1.27 (![Z: $i, B1: $i] : (~predicate2(B1, hate, Z, tptp_fun_A1_7(Z)))),
% 1.08/1.27 inference(and_elim,[status(thm)],[26])).
% 1.08/1.27 tff(105,plain,
% 1.08/1.27 ((~![Z: $i, B1: $i] : (~predicate2(B1, hate, Z, tptp_fun_A1_7(Z)))) | (~predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|)))),
% 1.08/1.27 inference(quant_inst,[status(thm)],[])).
% 1.08/1.27 tff(106,plain,
% 1.08/1.27 (~predicate2(tptp_fun_V_5(A!2), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|))),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[105, 104])).
% 1.08/1.27 tff(107,plain,
% 1.08/1.27 ($false),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[106, 103])).
% 1.08/1.27 tff(108,plain,((~(tptp_fun_A1_7(|'Butler'|) = |'Butler'|)) | (~(A!2 = |'Butler'|))), inference(lemma,lemma(discharge,[]))).
% 1.08/1.27 tff(109,plain,
% 1.08/1.27 (~(tptp_fun_A1_7(|'Butler'|) = |'Butler'|)),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[108, 77])).
% 1.08/1.27 tff(110,plain,
% 1.08/1.27 (((~![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))) | ((tptp_fun_A1_7(|'Butler'|) = |'Butler'|) | predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|)))) <=> ((~![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))) | (tptp_fun_A1_7(|'Butler'|) = |'Butler'|) | predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|)))),
% 1.08/1.27 inference(rewrite,[status(thm)],[])).
% 1.08/1.27 tff(111,plain,
% 1.08/1.27 ((~![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))) | ((tptp_fun_A1_7(|'Butler'|) = |'Butler'|) | predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|)))),
% 1.08/1.27 inference(quant_inst,[status(thm)],[])).
% 1.08/1.27 tff(112,plain,
% 1.08/1.27 ((~![R: $i] : ((R = |'Butler'|) | predicate2(tptp_fun_S_4(R), hate, |'AuntAgatha'|, R))) | (tptp_fun_A1_7(|'Butler'|) = |'Butler'|) | predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[111, 110])).
% 1.08/1.27 tff(113,plain,
% 1.08/1.27 ((tptp_fun_A1_7(|'Butler'|) = |'Butler'|) | predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|))),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[112, 35])).
% 1.08/1.27 tff(114,plain,
% 1.08/1.27 (predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|))),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[113, 109])).
% 1.08/1.27 tff(115,plain,
% 1.08/1.27 (^[W: $i, X: $i] : refl(((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W)) <=> ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W)))),
% 1.08/1.27 inference(bind,[status(th)],[])).
% 1.08/1.27 tff(116,plain,
% 1.08/1.27 (![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W)) <=> ![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W))),
% 1.08/1.27 inference(quant_intro,[status(thm)],[115])).
% 1.08/1.27 tff(117,plain,
% 1.08/1.27 (![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W))),
% 1.08/1.27 inference(and_elim,[status(thm)],[26])).
% 1.08/1.27 tff(118,plain,
% 1.08/1.27 (![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[117, 116])).
% 1.08/1.27 tff(119,plain,
% 1.08/1.27 (((~![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W))) | ((~predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|))) | predicate2(tptp_fun_Y_6(tptp_fun_A1_7(|'Butler'|)), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|)))) <=> ((~![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W))) | (~predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|))) | predicate2(tptp_fun_Y_6(tptp_fun_A1_7(|'Butler'|)), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|)))),
% 1.08/1.27 inference(rewrite,[status(thm)],[])).
% 1.08/1.27 tff(120,plain,
% 1.08/1.27 ((~![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W))) | ((~predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|))) | predicate2(tptp_fun_Y_6(tptp_fun_A1_7(|'Butler'|)), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|)))),
% 1.08/1.27 inference(quant_inst,[status(thm)],[])).
% 1.08/1.27 tff(121,plain,
% 1.08/1.27 ((~![W: $i, X: $i] : ((~predicate2(X, hate, |'AuntAgatha'|, W)) | predicate2(tptp_fun_Y_6(W), hate, |'Butler'|, W))) | (~predicate2(tptp_fun_S_4(tptp_fun_A1_7(|'Butler'|)), hate, |'AuntAgatha'|, tptp_fun_A1_7(|'Butler'|))) | predicate2(tptp_fun_Y_6(tptp_fun_A1_7(|'Butler'|)), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|))),
% 1.08/1.27 inference(modus_ponens,[status(thm)],[120, 119])).
% 1.08/1.27 tff(122,plain,
% 1.08/1.27 (predicate2(tptp_fun_Y_6(tptp_fun_A1_7(|'Butler'|)), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|))),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[121, 118, 114])).
% 1.08/1.27 tff(123,plain,
% 1.08/1.27 ((~![Z: $i, B1: $i] : (~predicate2(B1, hate, Z, tptp_fun_A1_7(Z)))) | (~predicate2(tptp_fun_Y_6(tptp_fun_A1_7(|'Butler'|)), hate, |'Butler'|, tptp_fun_A1_7(|'Butler'|)))),
% 1.08/1.27 inference(quant_inst,[status(thm)],[])).
% 1.08/1.27 tff(124,plain,
% 1.08/1.27 ($false),
% 1.08/1.27 inference(unit_resolution,[status(thm)],[123, 104, 122])).
% 1.08/1.27 % SZS output end Proof
% 1.08/1.27 % E exiting
%------------------------------------------------------------------------------