%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:24:15 AM UTC 2026
% Result : Unsatisfiable 0.13s 0.46s
% Output : Proof 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.10/0.35 % Computer : n020.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 7 14:09:15 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.13/0.46 % SZS status Unsatisfiable
% 0.13/0.46 % SZS output start Proof
% 0.13/0.46 tff(permission_type, type, (
% 0.13/0.46 permission: $i > $o)).
% 0.13/0.46 tff(tptp_fun_L2_1_type, type, (
% 0.13/0.46 tptp_fun_L2_1: ( $i * $i * $i * $i ) > $i)).
% 0.13/0.46 tff(rho1_type, type, (
% 0.13/0.46 rho1: $i)).
% 0.13/0.46 tff(some_action_type, type, (
% 0.13/0.46 some_action: $i)).
% 0.13/0.46 tff(some_target_type, type, (
% 0.13/0.46 some_target: $i)).
% 0.13/0.46 tff(l_type, type, (
% 0.13/0.46 l: $i)).
% 0.13/0.46 tff(cnt_type, type, (
% 0.13/0.46 cnt: ( $i * $i * $i ) > $o)).
% 0.13/0.46 tff(part_of_type, type, (
% 0.13/0.46 part_of: ( $i * $i ) > $o)).
% 0.13/0.46 tff(n2_type, type, (
% 0.13/0.46 n2: $i)).
% 0.13/0.46 tff(n1_type, type, (
% 0.13/0.46 n1: $i)).
% 0.13/0.46 tff(tptp_fun_N_2_type, type, (
% 0.13/0.46 tptp_fun_N_2: ( $i * $i * $i ) > $i)).
% 0.13/0.46 tff(no_right_type, type, (
% 0.13/0.46 no_right: $i > $o)).
% 0.13/0.46 tff(tptp_fun_L_0_type, type, (
% 0.13/0.46 tptp_fun_L_0: ( $i * $i * $i ) > $i)).
% 0.13/0.46 tff(tptp_fun_M_3_type, type, (
% 0.13/0.46 tptp_fun_M_3: ( $i * $i * $i * $i ) > $i)).
% 0.13/0.46 tff(odrl_rel_type, type, (
% 0.13/0.46 odrl_rel: $i > $o)).
% 0.13/0.46 tff(1,plain,
% 0.13/0.46 ((tptp_fun_N_2(some_target, some_action, rho1) = n2) <=> (n2 = tptp_fun_N_2(some_target, some_action, rho1))),
% 0.13/0.46 inference(commutativity,[status(thm)],[])).
% 0.13/0.46 tff(2,assumption,((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1)))), introduced(assumption)).
% 0.13/0.46 tff(3,plain,
% 0.13/0.46 (odrl_rel(rho1) <=> odrl_rel(rho1)),
% 0.13/0.46 inference(rewrite,[status(thm)],[])).
% 0.13/0.46 tff(4,axiom,(odrl_rel(rho1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','odrl_rho1')).
% 0.13/0.46 tff(5,plain,
% 0.13/0.46 (odrl_rel(rho1)),
% 0.13/0.46 inference(modus_ponens,[status(thm)],[4, 3])).
% 0.13/0.46 tff(6,plain,
% 0.13/0.46 (^[Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : rewrite(((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.13/0.46 inference(bind,[status(th)],[])).
% 0.13/0.46 tff(7,plain,
% 0.13/0.46 (![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))),
% 0.13/0.46 inference(quant_intro,[status(thm)],[6])).
% 0.13/0.46 tff(8,plain,
% 0.13/0.46 (^[Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : refl(((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))))),
% 0.13/0.46 inference(bind,[status(th)],[])).
% 0.13/0.46 tff(9,plain,
% 0.13/0.46 (![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.13/0.46 inference(quant_intro,[status(thm)],[8])).
% 0.13/0.46 tff(10,plain,
% 0.13/0.46 (![Rho: $i, A: $i, T: $i] : ![N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.13/0.46 inference(pull_quant,[status(thm)],[])).
% 0.13/0.46 tff(11,plain,
% 0.13/0.46 (^[Rho: $i, A: $i, T: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(pull_quant((~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))) <=> ?[M: $i] : (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))), (((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))) <=> ((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | ?[M: $i] : (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))), pull_quant(((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | ?[M: $i] : (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))) <=> ?[M: $i] : ((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))), (((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))) <=> ?[M: $i] : ((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))), ((~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))) <=> (~?[M: $i] : ((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))), pull_quant((~?[M: $i] : ((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))) <=> ![M: $i] : (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))), ((~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))) <=> ![M: $i] : (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))), ((![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))) <=> (![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | ![M: $i] : (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))))), pull_quant((![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | ![M: $i] : (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))) <=> ![M: $i, L: $i] : (((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))), ((![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))) <=> ![M: $i, L: $i] : (((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))))), ((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) <=> (~![M: $i, L: $i] : (((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))))), pull_quant((~![M: $i, L: $i] : (((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) <=> ?[M: $i, L: $i] : (~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M))))))))), ((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) <=> ?[M: $i, L: $i] : (~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))))), trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(pull_quant((~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))) <=> ?[L2: $i] : (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T))))), (((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T))))) <=> ((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | ?[L2: $i] : (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T))))))), pull_quant(((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | ?[L2: $i] : (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T))))) <=> ?[L2: $i] : ((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))), (((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T))))) <=> ?[L2: $i] : ((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T))))))), ((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) <=> (~?[L2: $i] : ((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))))), pull_quant((~?[L2: $i] : ((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) <=> ![L2: $i] : (~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T))))))), ((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) <=> ![L2: $i] : (~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))))), (((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))) <=> (![L2: $i] : (~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))), pull_quant((![L2: $i] : (~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))) <=> ![N: $i, L2: $i] : ((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))), (((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))) <=> ![N: $i, L2: $i] : ((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))), ((~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))) <=> (~![N: $i, L2: $i] : ((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))), pull_quant((~![N: $i, L2: $i] : ((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))) <=> ?[N: $i, L2: $i] : (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))), ((~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))) <=> ?[N: $i, L2: $i] : (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))), (((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))) <=> (?[M: $i, L: $i] : (~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | ?[N: $i, L2: $i] : (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))), pull_quant((?[M: $i, L: $i] : (~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | ?[N: $i, L2: $i] : (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))) <=> ?[N: $i, L2: $i, M: $i, L: $i] : ((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))), (((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))) <=> ?[N: $i, L2: $i, M: $i, L: $i] : ((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))), ((~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))) <=> (~?[N: $i, L2: $i, M: $i, L: $i] : ((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))), pull_quant((~?[N: $i, L2: $i, M: $i, L: $i] : ((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))) <=> ![N: $i, L2: $i, M: $i, L: $i] : (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))), ((~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))) <=> ![N: $i, L2: $i, M: $i, L: $i] : (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))), (((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ((~odrl_rel(Rho)) | ![N: $i, L2: $i, M: $i, L: $i] : (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))))), pull_quant(((~odrl_rel(Rho)) | ![N: $i, L2: $i, M: $i, L: $i] : (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))), (((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))))),
% 0.22/0.47 inference(bind,[status(th)],[])).
% 0.22/0.47 tff(12,plain,
% 0.22/0.47 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![Rho: $i, A: $i, T: $i] : ![N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.22/0.47 inference(quant_intro,[status(thm)],[11])).
% 0.22/0.47 tff(13,plain,
% 0.22/0.47 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.22/0.47 inference(transitivity,[status(thm)],[12, 10])).
% 0.22/0.47 tff(14,plain,
% 0.22/0.47 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.22/0.47 inference(transitivity,[status(thm)],[13, 9])).
% 0.22/0.47 tff(15,plain,
% 0.22/0.47 (^[Rho: $i, A: $i, T: $i] : rewrite(((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))))),
% 0.22/0.47 inference(bind,[status(th)],[])).
% 0.22/0.47 tff(16,plain,
% 0.22/0.47 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.22/0.47 inference(quant_intro,[status(thm)],[15])).
% 0.22/0.47 tff(17,plain,
% 0.22/0.47 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) <=> ![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.22/0.47 inference(transitivity,[status(thm)],[16, 14])).
% 0.22/0.47 tff(18,plain,
% 0.22/0.47 (^[Rho: $i, A: $i, T: $i] : rewrite(((~odrl_rel(Rho)) | ((![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((~(permission(tptp_fun_L2_1(L, T, A, Rho)) & part_of(tptp_fun_L2_1(L, T, A, Rho), Rho) & cnt(tptp_fun_L2_1(L, T, A, Rho), A, T))) | (tptp_fun_L2_1(L, T, A, Rho) = L)))) | (no_right(tptp_fun_N_2(T, A, Rho)) & part_of(tptp_fun_N_2(T, A, Rho), Rho) & cnt(tptp_fun_N_2(T, A, Rho), A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = tptp_fun_N_2(T, A, Rho))))) & ((permission(tptp_fun_L_0(T, A, Rho)) & part_of(tptp_fun_L_0(T, A, Rho), Rho) & cnt(tptp_fun_L_0(T, A, Rho), A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = tptp_fun_L_0(T, A, Rho)))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((~(no_right(tptp_fun_M_3(N, T, A, Rho)) & part_of(tptp_fun_M_3(N, T, A, Rho), Rho) & cnt(tptp_fun_M_3(N, T, A, Rho), A, T))) | (tptp_fun_M_3(N, T, A, Rho) = N))))))) <=> ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))))),
% 0.22/0.47 inference(bind,[status(th)],[])).
% 0.22/0.47 tff(19,plain,
% 0.22/0.47 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | ((![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((~(permission(tptp_fun_L2_1(L, T, A, Rho)) & part_of(tptp_fun_L2_1(L, T, A, Rho), Rho) & cnt(tptp_fun_L2_1(L, T, A, Rho), A, T))) | (tptp_fun_L2_1(L, T, A, Rho) = L)))) | (no_right(tptp_fun_N_2(T, A, Rho)) & part_of(tptp_fun_N_2(T, A, Rho), Rho) & cnt(tptp_fun_N_2(T, A, Rho), A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = tptp_fun_N_2(T, A, Rho))))) & ((permission(tptp_fun_L_0(T, A, Rho)) & part_of(tptp_fun_L_0(T, A, Rho), Rho) & cnt(tptp_fun_L_0(T, A, Rho), A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = tptp_fun_L_0(T, A, Rho)))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((~(no_right(tptp_fun_M_3(N, T, A, Rho)) & part_of(tptp_fun_M_3(N, T, A, Rho), Rho) & cnt(tptp_fun_M_3(N, T, A, Rho), A, T))) | (tptp_fun_M_3(N, T, A, Rho) = N))))))) <=> ![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.22/0.47 inference(quant_intro,[status(thm)],[18])).
% 0.22/0.47 tff(20,plain,
% 0.22/0.47 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N))))) <=> ![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N)))))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(21,plain,
% 0.22/0.47 (^[Rho: $i, A: $i, T: $i] : trans(monotonicity(rewrite((?[L: $i] : (((permission(L) & part_of(L, Rho)) & cnt(L, A, T)) & ![L2: $i] : (((permission(L2) & part_of(L2, Rho)) & cnt(L2, A, T)) => (L2 = L))) <=> ?[N: $i] : (((no_right(N) & part_of(N, Rho)) & cnt(N, A, T)) & ![M: $i] : (((no_right(M) & part_of(M, Rho)) & cnt(M, A, T)) => (M = N)))) <=> (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N))))), ((odrl_rel(Rho) => (?[L: $i] : (((permission(L) & part_of(L, Rho)) & cnt(L, A, T)) & ![L2: $i] : (((permission(L2) & part_of(L2, Rho)) & cnt(L2, A, T)) => (L2 = L))) <=> ?[N: $i] : (((no_right(N) & part_of(N, Rho)) & cnt(N, A, T)) & ![M: $i] : (((no_right(M) & part_of(M, Rho)) & cnt(M, A, T)) => (M = N))))) <=> (odrl_rel(Rho) => (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N))))))), rewrite((odrl_rel(Rho) => (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N))))) <=> ((~odrl_rel(Rho)) | (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N)))))), ((odrl_rel(Rho) => (?[L: $i] : (((permission(L) & part_of(L, Rho)) & cnt(L, A, T)) & ![L2: $i] : (((permission(L2) & part_of(L2, Rho)) & cnt(L2, A, T)) => (L2 = L))) <=> ?[N: $i] : (((no_right(N) & part_of(N, Rho)) & cnt(N, A, T)) & ![M: $i] : (((no_right(M) & part_of(M, Rho)) & cnt(M, A, T)) => (M = N))))) <=> ((~odrl_rel(Rho)) | (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N)))))))),
% 0.22/0.47 inference(bind,[status(th)],[])).
% 0.22/0.47 tff(22,plain,
% 0.22/0.47 (![Rho: $i, A: $i, T: $i] : (odrl_rel(Rho) => (?[L: $i] : (((permission(L) & part_of(L, Rho)) & cnt(L, A, T)) & ![L2: $i] : (((permission(L2) & part_of(L2, Rho)) & cnt(L2, A, T)) => (L2 = L))) <=> ?[N: $i] : (((no_right(N) & part_of(N, Rho)) & cnt(N, A, T)) & ![M: $i] : (((no_right(M) & part_of(M, Rho)) & cnt(M, A, T)) => (M = N))))) <=> ![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N)))))),
% 0.22/0.48 inference(quant_intro,[status(thm)],[21])).
% 0.22/0.48 tff(23,axiom,(![Rho: $i, A: $i, T: $i] : (odrl_rel(Rho) => (?[L: $i] : (((permission(L) & part_of(L, Rho)) & cnt(L, A, T)) & ![L2: $i] : (((permission(L2) & part_of(L2, Rho)) & cnt(L2, A, T)) => (L2 = L))) <=> ?[N: $i] : (((no_right(N) & part_of(N, Rho)) & cnt(N, A, T)) & ![M: $i] : (((no_right(M) & part_of(M, Rho)) & cnt(M, A, T)) => (M = N)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','ax_correlativity_permission')).
% 0.22/0.48 tff(24,plain,
% 0.22/0.48 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N)))))),
% 0.22/0.48 inference(modus_ponens,[status(thm)],[23, 22])).
% 0.22/0.48 tff(25,plain,
% 0.22/0.48 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (?[L: $i] : (permission(L) & part_of(L, Rho) & cnt(L, A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = L))) <=> ?[N: $i] : (no_right(N) & part_of(N, Rho) & cnt(N, A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = N)))))),
% 0.22/0.48 inference(modus_ponens,[status(thm)],[24, 20])).
% 0.22/0.48 tff(26,plain,(
% 0.22/0.48 ![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | ((![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((~(permission(tptp_fun_L2_1(L, T, A, Rho)) & part_of(tptp_fun_L2_1(L, T, A, Rho), Rho) & cnt(tptp_fun_L2_1(L, T, A, Rho), A, T))) | (tptp_fun_L2_1(L, T, A, Rho) = L)))) | (no_right(tptp_fun_N_2(T, A, Rho)) & part_of(tptp_fun_N_2(T, A, Rho), Rho) & cnt(tptp_fun_N_2(T, A, Rho), A, T) & ![M: $i] : ((~(no_right(M) & part_of(M, Rho) & cnt(M, A, T))) | (M = tptp_fun_N_2(T, A, Rho))))) & ((permission(tptp_fun_L_0(T, A, Rho)) & part_of(tptp_fun_L_0(T, A, Rho), Rho) & cnt(tptp_fun_L_0(T, A, Rho), A, T) & ![L2: $i] : ((~(permission(L2) & part_of(L2, Rho) & cnt(L2, A, T))) | (L2 = tptp_fun_L_0(T, A, Rho)))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((~(no_right(tptp_fun_M_3(N, T, A, Rho)) & part_of(tptp_fun_M_3(N, T, A, Rho), Rho) & cnt(tptp_fun_M_3(N, T, A, Rho), A, T))) | (tptp_fun_M_3(N, T, A, Rho) = N)))))))),
% 0.22/0.48 inference(skolemize,[status(sab)],[25])).
% 0.22/0.48 tff(27,plain,
% 0.22/0.48 (![Rho: $i, A: $i, T: $i] : ((~odrl_rel(Rho)) | (~((~(![L: $i] : ((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~![M: $i] : ((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~![L2: $i] : ((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ![N: $i] : ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.22/0.48 inference(modus_ponens,[status(thm)],[26, 19])).
% 0.22/0.48 tff(28,plain,
% 0.22/0.48 (![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~(((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho)))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)) | (~no_right(M)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | ((~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T))))))))))),
% 0.22/0.48 inference(modus_ponens,[status(thm)],[27, 17])).
% 0.22/0.48 tff(29,plain,
% 0.22/0.48 (![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))),
% 0.22/0.48 inference(modus_ponens,[status(thm)],[28, 7])).
% 0.22/0.48 tff(30,plain,
% 0.22/0.48 (((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))))) <=> ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | (~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(31,plain,
% 0.22/0.48 (((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((l = tptp_fun_L_0(some_target, some_action, rho1)) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)))))) | (~no_right(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target))))))))) <=> ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(32,plain,
% 0.22/0.48 (((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((l = tptp_fun_L_0(some_target, some_action, rho1)) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)))))) | (~no_right(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))))))))) <=> ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1))))))))))))),
% 0.22/0.49 inference(monotonicity,[status(thm)],[31])).
% 0.22/0.49 tff(33,plain,
% 0.22/0.49 (((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((l = tptp_fun_L_0(some_target, some_action, rho1)) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)))))) | (~no_right(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))))))))) <=> ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | (~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))))),
% 0.22/0.49 inference(transitivity,[status(thm)],[32, 30])).
% 0.22/0.49 tff(34,plain,
% 0.22/0.49 ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((l = tptp_fun_L_0(some_target, some_action, rho1)) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)))))) | (~no_right(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))))))))),
% 0.22/0.49 inference(quant_inst,[status(thm)],[])).
% 0.22/0.49 tff(35,plain,
% 0.22/0.49 ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | (~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1))))))))))),
% 0.22/0.49 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.22/0.49 tff(36,plain,
% 0.22/0.49 (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))),
% 0.22/0.49 inference(unit_resolution,[status(thm)],[35, 29, 5])).
% 0.22/0.49 tff(37,plain,
% 0.22/0.49 (((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1))))))))) | ((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))),
% 0.22/0.50 inference(tautology,[status(thm)],[])).
% 0.22/0.50 tff(38,plain,
% 0.22/0.50 ((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1))))))),
% 0.22/0.50 inference(unit_resolution,[status(thm)],[37, 36])).
% 0.22/0.50 tff(39,plain,
% 0.22/0.50 (cnt(l, some_action, some_target) <=> cnt(l, some_action, some_target)),
% 0.22/0.50 inference(rewrite,[status(thm)],[])).
% 0.22/0.50 tff(40,axiom,(cnt(l, some_action, some_target)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cnt_l')).
% 0.22/0.50 tff(41,plain,
% 0.22/0.50 (cnt(l, some_action, some_target)),
% 0.22/0.50 inference(modus_ponens,[status(thm)],[40, 39])).
% 0.22/0.50 tff(42,plain,
% 0.22/0.50 (part_of(l, rho1) <=> part_of(l, rho1)),
% 0.22/0.50 inference(rewrite,[status(thm)],[])).
% 0.22/0.50 tff(43,axiom,(part_of(l, rho1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','partof_l')).
% 0.22/0.50 tff(44,plain,
% 0.22/0.50 (part_of(l, rho1)),
% 0.22/0.50 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.22/0.50 tff(45,plain,
% 0.22/0.50 (permission(l) <=> permission(l)),
% 0.22/0.50 inference(rewrite,[status(thm)],[])).
% 0.22/0.50 tff(46,axiom,(permission(l)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','permission_l')).
% 0.22/0.50 tff(47,plain,
% 0.22/0.50 (permission(l)),
% 0.22/0.50 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.22/0.50 tff(48,plain,
% 0.22/0.50 ((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1))))))),
% 0.22/0.50 inference(tautology,[status(thm)],[])).
% 0.22/0.50 tff(49,plain,
% 0.22/0.50 ((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1))))))),
% 0.22/0.50 inference(unit_resolution,[status(thm)],[48, 47, 44, 41])).
% 0.22/0.50 tff(50,plain,
% 0.22/0.50 ((~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1))))))),
% 0.22/0.50 inference(unit_resolution,[status(thm)],[49, 38])).
% 0.22/0.50 tff(51,plain,
% 0.22/0.50 (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))))),
% 0.22/0.50 inference(unit_resolution,[status(thm)],[50, 2])).
% 0.22/0.50 tff(52,plain,
% 0.22/0.50 (((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1))))) | ((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))),
% 0.22/0.50 inference(tautology,[status(thm)],[])).
% 0.22/0.50 tff(53,plain,
% 0.22/0.50 ((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1))),
% 0.22/0.50 inference(unit_resolution,[status(thm)],[52, 51])).
% 0.22/0.50 tff(54,plain,
% 0.22/0.50 (cnt(n1, some_action, some_target) <=> cnt(n1, some_action, some_target)),
% 0.22/0.50 inference(rewrite,[status(thm)],[])).
% 0.22/0.50 tff(55,axiom,(cnt(n1, some_action, some_target)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cnt_n1')).
% 0.22/0.50 tff(56,plain,
% 0.22/0.50 (cnt(n1, some_action, some_target)),
% 0.22/0.50 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.22/0.50 tff(57,plain,
% 0.22/0.50 (part_of(n1, rho1) <=> part_of(n1, rho1)),
% 0.22/0.50 inference(rewrite,[status(thm)],[])).
% 0.22/0.50 tff(58,axiom,(part_of(n1, rho1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','partof_n1')).
% 0.22/0.50 tff(59,plain,
% 0.22/0.50 (part_of(n1, rho1)),
% 0.22/0.50 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.22/0.50 tff(60,plain,
% 0.22/0.50 (no_right(n1) <=> no_right(n1)),
% 0.22/0.50 inference(rewrite,[status(thm)],[])).
% 0.22/0.50 tff(61,axiom,(no_right(n1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','no_right_n1')).
% 0.22/0.50 tff(62,plain,
% 0.22/0.50 (no_right(n1)),
% 0.22/0.50 inference(modus_ponens,[status(thm)],[61, 60])).
% 0.22/0.50 tff(63,plain,
% 0.22/0.50 ((~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))) | (~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1))),
% 0.22/0.50 inference(tautology,[status(thm)],[])).
% 0.22/0.50 tff(64,plain,
% 0.22/0.50 ((~((~no_right(n1)) | (~part_of(n1, rho1)) | (~cnt(n1, some_action, some_target)) | (n1 = tptp_fun_N_2(some_target, some_action, rho1)))) | (n1 = tptp_fun_N_2(some_target, some_action, rho1))),
% 0.22/0.50 inference(unit_resolution,[status(thm)],[63, 62, 59, 56])).
% 0.22/0.50 tff(65,plain,
% 0.22/0.50 (n1 = tptp_fun_N_2(some_target, some_action, rho1)),
% 0.22/0.50 inference(unit_resolution,[status(thm)],[64, 53])).
% 0.22/0.50 tff(66,plain,
% 0.22/0.50 ((n1 = n2) <=> (tptp_fun_N_2(some_target, some_action, rho1) = n2)),
% 0.22/0.50 inference(monotonicity,[status(thm)],[65])).
% 0.22/0.50 tff(67,plain,
% 0.22/0.50 ((n1 = n2) <=> (n2 = tptp_fun_N_2(some_target, some_action, rho1))),
% 0.22/0.50 inference(transitivity,[status(thm)],[66, 1])).
% 0.22/0.50 tff(68,plain,
% 0.22/0.50 ((n2 = tptp_fun_N_2(some_target, some_action, rho1)) <=> (n1 = n2)),
% 0.22/0.50 inference(symmetry,[status(thm)],[67])).
% 0.22/0.50 tff(69,plain,
% 0.22/0.50 (((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))))) <=> ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | (~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))))),
% 0.22/0.51 inference(rewrite,[status(thm)],[])).
% 0.22/0.51 tff(70,plain,
% 0.22/0.51 (((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((l = tptp_fun_L_0(some_target, some_action, rho1)) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)))))) | (~no_right(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target))))))))) <=> ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))))),
% 0.22/0.51 inference(rewrite,[status(thm)],[])).
% 0.22/0.51 tff(71,plain,
% 0.22/0.51 (((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((l = tptp_fun_L_0(some_target, some_action, rho1)) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)))))) | (~no_right(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))))))))) <=> ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1))))))))))))),
% 0.22/0.51 inference(monotonicity,[status(thm)],[70])).
% 0.22/0.51 tff(72,plain,
% 0.22/0.51 (((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((l = tptp_fun_L_0(some_target, some_action, rho1)) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)))))) | (~no_right(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))))))))) <=> ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | (~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))))),
% 0.22/0.52 inference(transitivity,[status(thm)],[71, 69])).
% 0.22/0.52 tff(73,plain,
% 0.22/0.52 ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | ((~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((l = tptp_fun_L_0(some_target, some_action, rho1)) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)))))) | (~no_right(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))))))))),
% 0.22/0.52 inference(quant_inst,[status(thm)],[])).
% 0.22/0.52 tff(74,plain,
% 0.22/0.52 ((~![Rho: $i, A: $i, T: $i, N: $i, L2: $i, M: $i, L: $i] : ((~odrl_rel(Rho)) | (~((~((~permission(L)) | (~part_of(L, Rho)) | (~cnt(L, A, T)) | (~((tptp_fun_L2_1(L, T, A, Rho) = L) | (~part_of(tptp_fun_L2_1(L, T, A, Rho), Rho)) | (~cnt(tptp_fun_L2_1(L, T, A, Rho), A, T)) | (~permission(tptp_fun_L2_1(L, T, A, Rho))))) | (~((~no_right(tptp_fun_N_2(T, A, Rho))) | (~part_of(tptp_fun_N_2(T, A, Rho), Rho)) | (~cnt(tptp_fun_N_2(T, A, Rho), A, T)) | (~((~no_right(M)) | (~part_of(M, Rho)) | (~cnt(M, A, T)) | (M = tptp_fun_N_2(T, A, Rho)))))))) | (~((~((~permission(tptp_fun_L_0(T, A, Rho))) | (~part_of(tptp_fun_L_0(T, A, Rho), Rho)) | (~cnt(tptp_fun_L_0(T, A, Rho), A, T)) | (~((L2 = tptp_fun_L_0(T, A, Rho)) | (~permission(L2)) | (~part_of(L2, Rho)) | (~cnt(L2, A, T)))))) | (~no_right(N)) | (~part_of(N, Rho)) | (~cnt(N, A, T)) | (~((tptp_fun_M_3(N, T, A, Rho) = N) | (~no_right(tptp_fun_M_3(N, T, A, Rho))) | (~part_of(tptp_fun_M_3(N, T, A, Rho), Rho)) | (~cnt(tptp_fun_M_3(N, T, A, Rho), A, T)))))))))) | (~odrl_rel(rho1)) | (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1))))))))))),
% 0.22/0.52 inference(modus_ponens,[status(thm)],[73, 72])).
% 0.22/0.52 tff(75,plain,
% 0.22/0.52 (~((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1)))))))))),
% 0.22/0.52 inference(unit_resolution,[status(thm)],[74, 29, 5])).
% 0.22/0.52 tff(76,plain,
% 0.22/0.52 (((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~no_right(l)) | (~((tptp_fun_M_3(l, some_target, some_action, rho1) = l) | (~no_right(tptp_fun_M_3(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_M_3(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_M_3(l, some_target, some_action, rho1), some_action, some_target)))) | (~((~permission(tptp_fun_L_0(some_target, some_action, rho1))) | (~part_of(tptp_fun_L_0(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L_0(some_target, some_action, rho1), some_action, some_target)) | (~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (l = tptp_fun_L_0(some_target, some_action, rho1))))))))) | ((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))),
% 0.22/0.53 inference(tautology,[status(thm)],[])).
% 0.22/0.53 tff(77,plain,
% 0.22/0.53 ((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1))))))),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[76, 75])).
% 0.22/0.53 tff(78,plain,
% 0.22/0.53 ((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1))))))),
% 0.22/0.53 inference(tautology,[status(thm)],[])).
% 0.22/0.53 tff(79,plain,
% 0.22/0.53 ((~((~permission(l)) | (~part_of(l, rho1)) | (~cnt(l, some_action, some_target)) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))))) | (~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1))))))),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[78, 47, 44, 41])).
% 0.22/0.53 tff(80,plain,
% 0.22/0.53 ((~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) | (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1))))))),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[79, 77])).
% 0.22/0.53 tff(81,plain,
% 0.22/0.53 (~((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))))),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[80, 2])).
% 0.22/0.53 tff(82,plain,
% 0.22/0.53 (((~no_right(tptp_fun_N_2(some_target, some_action, rho1))) | (~part_of(tptp_fun_N_2(some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_N_2(some_target, some_action, rho1), some_action, some_target)) | (~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1))))) | ((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))),
% 0.22/0.53 inference(tautology,[status(thm)],[])).
% 0.22/0.53 tff(83,plain,
% 0.22/0.53 ((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1))),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[82, 81])).
% 0.22/0.53 tff(84,plain,
% 0.22/0.53 (cnt(n2, some_action, some_target) <=> cnt(n2, some_action, some_target)),
% 0.22/0.53 inference(rewrite,[status(thm)],[])).
% 0.22/0.53 tff(85,axiom,(cnt(n2, some_action, some_target)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cnt_n2')).
% 0.22/0.53 tff(86,plain,
% 0.22/0.53 (cnt(n2, some_action, some_target)),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[85, 84])).
% 0.22/0.53 tff(87,plain,
% 0.22/0.53 (part_of(n2, rho1) <=> part_of(n2, rho1)),
% 0.22/0.53 inference(rewrite,[status(thm)],[])).
% 0.22/0.53 tff(88,axiom,(part_of(n2, rho1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','partof_n2')).
% 0.22/0.53 tff(89,plain,
% 0.22/0.53 (part_of(n2, rho1)),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[88, 87])).
% 0.22/0.53 tff(90,plain,
% 0.22/0.53 (no_right(n2) <=> no_right(n2)),
% 0.22/0.53 inference(rewrite,[status(thm)],[])).
% 0.22/0.53 tff(91,axiom,(no_right(n2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','no_right_n2')).
% 0.22/0.53 tff(92,plain,
% 0.22/0.53 (no_right(n2)),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[91, 90])).
% 0.22/0.53 tff(93,plain,
% 0.22/0.53 ((~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))) | (~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1))),
% 0.22/0.53 inference(tautology,[status(thm)],[])).
% 0.22/0.53 tff(94,plain,
% 0.22/0.53 ((~((~no_right(n2)) | (~part_of(n2, rho1)) | (~cnt(n2, some_action, some_target)) | (n2 = tptp_fun_N_2(some_target, some_action, rho1)))) | (n2 = tptp_fun_N_2(some_target, some_action, rho1))),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[93, 92, 89, 86])).
% 0.22/0.53 tff(95,plain,
% 0.22/0.53 (n2 = tptp_fun_N_2(some_target, some_action, rho1)),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[94, 83])).
% 0.22/0.53 tff(96,plain,
% 0.22/0.53 (n1 = n2),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[95, 68])).
% 0.22/0.53 tff(97,plain,
% 0.22/0.53 ((~(n1 = n2)) <=> (~(n1 = n2))),
% 0.22/0.53 inference(rewrite,[status(thm)],[])).
% 0.22/0.53 tff(98,axiom,(~(n1 = n2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','n1_neq_n2')).
% 0.22/0.53 tff(99,plain,
% 0.22/0.53 (~(n1 = n2)),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[98, 97])).
% 0.22/0.53 tff(100,plain,
% 0.22/0.53 ($false),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[99, 96])).
% 0.22/0.53 tff(101,plain,(~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))), inference(lemma,lemma(discharge,[]))).
% 0.22/0.53 tff(102,plain,
% 0.22/0.53 (((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1)))) | (~(tptp_fun_L2_1(l, some_target, some_action, rho1) = l))),
% 0.22/0.53 inference(tautology,[status(thm)],[])).
% 0.22/0.53 tff(103,plain,
% 0.22/0.53 (~(tptp_fun_L2_1(l, some_target, some_action, rho1) = l)),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[102, 101])).
% 0.22/0.53 tff(104,assumption,(~((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))), introduced(assumption)).
% 0.22/0.53 tff(105,plain,
% 0.22/0.53 (((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1)))) | permission(tptp_fun_L2_1(l, some_target, some_action, rho1))),
% 0.22/0.53 inference(tautology,[status(thm)],[])).
% 0.22/0.53 tff(106,plain,
% 0.22/0.53 (permission(tptp_fun_L2_1(l, some_target, some_action, rho1))),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[105, 104])).
% 0.22/0.53 tff(107,plain,
% 0.22/0.53 (((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1)))) | cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)),
% 0.22/0.53 inference(tautology,[status(thm)],[])).
% 0.22/0.53 tff(108,plain,
% 0.22/0.53 (cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[107, 104])).
% 0.22/0.53 tff(109,plain,
% 0.22/0.53 (((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1)))) | part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)),
% 0.22/0.53 inference(tautology,[status(thm)],[])).
% 0.22/0.53 tff(110,plain,
% 0.22/0.53 (part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)),
% 0.22/0.53 inference(unit_resolution,[status(thm)],[109, 104])).
% 0.22/0.53 tff(111,assumption,(~(tptp_fun_L2_1(l, some_target, some_action, rho1) = l)), introduced(assumption)).
% 0.22/0.53 tff(112,plain,
% 0.22/0.53 (^[L2: $i] : refl(((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))) <=> ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))))),
% 0.22/0.53 inference(bind,[status(th)],[])).
% 0.22/0.53 tff(113,plain,
% 0.22/0.53 (![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))) <=> ![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))),
% 0.22/0.53 inference(quant_intro,[status(thm)],[112])).
% 0.22/0.53 tff(114,plain,
% 0.22/0.53 (^[L2: $i] : trans(monotonicity(trans(monotonicity(rewrite((permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target)) <=> (~((~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))))), ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) <=> (~(~((~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))))))), rewrite((~(~((~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))))) <=> ((~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))), ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) <=> ((~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))))), (((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l)) <=> (((~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))) | (L2 = l)))), rewrite((((~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target))) | (L2 = l)) <=> ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))), (((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l)) <=> ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))))),
% 0.22/0.53 inference(bind,[status(th)],[])).
% 0.22/0.53 tff(115,plain,
% 0.22/0.53 (![L2: $i] : ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l)) <=> ![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))),
% 0.22/0.53 inference(quant_intro,[status(thm)],[114])).
% 0.22/0.53 tff(116,plain,
% 0.22/0.53 (![L2: $i] : ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l)) <=> ![L2: $i] : ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l))),
% 0.22/0.53 inference(rewrite,[status(thm)],[])).
% 0.22/0.53 tff(117,plain,
% 0.22/0.53 (^[L2: $i] : trans(monotonicity(rewrite(((permission(L2) & part_of(L2, rho1)) & cnt(L2, some_action, some_target)) <=> (permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))), ((((permission(L2) & part_of(L2, rho1)) & cnt(L2, some_action, some_target)) => (L2 = l)) <=> ((permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target)) => (L2 = l)))), rewrite(((permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target)) => (L2 = l)) <=> ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l))), ((((permission(L2) & part_of(L2, rho1)) & cnt(L2, some_action, some_target)) => (L2 = l)) <=> ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l))))),
% 0.22/0.53 inference(bind,[status(th)],[])).
% 0.22/0.53 tff(118,plain,
% 0.22/0.53 (![L2: $i] : (((permission(L2) & part_of(L2, rho1)) & cnt(L2, some_action, some_target)) => (L2 = l)) <=> ![L2: $i] : ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l))),
% 0.22/0.53 inference(quant_intro,[status(thm)],[117])).
% 0.22/0.53 tff(119,axiom,(![L2: $i] : (((permission(L2) & part_of(L2, rho1)) & cnt(L2, some_action, some_target)) => (L2 = l))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','perm_l_unique')).
% 0.22/0.53 tff(120,plain,
% 0.22/0.53 (![L2: $i] : ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l))),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[119, 118])).
% 0.22/0.53 tff(121,plain,
% 0.22/0.53 (![L2: $i] : ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l))),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[120, 116])).
% 0.22/0.53 tff(122,plain,(
% 0.22/0.53 ![L2: $i] : ((~(permission(L2) & part_of(L2, rho1) & cnt(L2, some_action, some_target))) | (L2 = l))),
% 0.22/0.53 inference(skolemize,[status(sab)],[121])).
% 0.22/0.53 tff(123,plain,
% 0.22/0.53 (![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[122, 115])).
% 0.22/0.53 tff(124,plain,
% 0.22/0.53 (![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[123, 113])).
% 0.22/0.53 tff(125,plain,
% 0.22/0.53 (((~![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))) | ((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))) <=> ((~![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))) | (tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))),
% 0.22/0.54 inference(rewrite,[status(thm)],[])).
% 0.22/0.54 tff(126,plain,
% 0.22/0.54 (((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target))) <=> ((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))),
% 0.22/0.54 inference(rewrite,[status(thm)],[])).
% 0.22/0.54 tff(127,plain,
% 0.22/0.54 (((~![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))) | ((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)))) <=> ((~![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))) | ((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1)))))),
% 0.22/0.54 inference(monotonicity,[status(thm)],[126])).
% 0.22/0.54 tff(128,plain,
% 0.22/0.54 (((~![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))) | ((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)))) <=> ((~![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))) | (tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))))),
% 0.22/0.54 inference(transitivity,[status(thm)],[127, 125])).
% 0.22/0.54 tff(129,plain,
% 0.22/0.54 ((~![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))) | ((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1))) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)))),
% 0.22/0.54 inference(quant_inst,[status(thm)],[])).
% 0.22/0.54 tff(130,plain,
% 0.22/0.54 ((~![L2: $i] : ((L2 = l) | (~permission(L2)) | (~part_of(L2, rho1)) | (~cnt(L2, some_action, some_target)))) | (tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1)))),
% 0.22/0.54 inference(modus_ponens,[status(thm)],[129, 128])).
% 0.22/0.54 tff(131,plain,
% 0.22/0.54 ($false),
% 0.22/0.54 inference(unit_resolution,[status(thm)],[130, 124, 111, 110, 108, 106])).
% 0.22/0.54 tff(132,plain,(((tptp_fun_L2_1(l, some_target, some_action, rho1) = l) | (~part_of(tptp_fun_L2_1(l, some_target, some_action, rho1), rho1)) | (~cnt(tptp_fun_L2_1(l, some_target, some_action, rho1), some_action, some_target)) | (~permission(tptp_fun_L2_1(l, some_target, some_action, rho1)))) | (tptp_fun_L2_1(l, some_target, some_action, rho1) = l)), inference(lemma,lemma(discharge,[]))).
% 0.22/0.54 tff(133,plain,
% 0.22/0.54 ($false),
% 0.22/0.54 inference(unit_resolution,[status(thm)],[132, 103, 101])).
% 0.22/0.54 % SZS output end Proof
% 0.22/0.54 % E exiting
%------------------------------------------------------------------------------