%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 29 02:10:30 PM UTC 2026 % Result : Theorem 0.44s 1.02s % Output : Refutation 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : MGT111+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.33 % Computer : n022.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Tue Apr 28 19:29:20 EDT 2026 % 0.17/0.34 % CPUTime : % 0.44/1.01 ============================== Prover9 =============================== % 0.44/1.01 Prover9 (32) version 2009-11A, November 2009. % 0.44/1.01 Process 9614 was started by sandbox2 on n022.cluster.edu, % 0.44/1.01 Tue Apr 28 19:29:21 2026 % 0.44/1.01 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_9459_n022.cluster.edu". % 0.44/1.01 ============================== end of head =========================== % 0.44/1.01 % 0.44/1.01 ============================== INPUT ================================= % 0.44/1.01 % 0.44/1.01 % Reading from file /tmp/Prover9_9459_n022.cluster.edu % 0.44/1.01 % 0.44/1.01 set(prolog_style_variables). % 0.44/1.01 set(auto2). % 0.44/1.01 % set(auto2) -> set(auto). % 0.44/1.01 % set(auto) -> set(auto_inference). % 0.44/1.01 % set(auto) -> set(auto_setup). % 0.44/1.01 % set(auto_setup) -> set(predicate_elim). % 0.44/1.01 % set(auto_setup) -> assign(eq_defs, unfold). % 0.44/1.01 % set(auto) -> set(auto_limits). % 0.44/1.01 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.44/1.01 % set(auto_limits) -> assign(sos_limit, 20000). % 0.44/1.01 % set(auto) -> set(auto_denials). % 0.44/1.01 % set(auto) -> set(auto_process). % 0.44/1.01 % set(auto2) -> assign(new_constants, 1). % 0.44/1.01 % set(auto2) -> assign(fold_denial_max, 3). % 0.44/1.01 % set(auto2) -> assign(max_weight, "200.000"). % 0.44/1.01 % set(auto2) -> assign(max_hours, 1). % 0.44/1.01 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.44/1.01 % set(auto2) -> assign(max_seconds, 0). % 0.44/1.01 % set(auto2) -> assign(max_minutes, 5). % 0.44/1.01 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.44/1.01 % set(auto2) -> set(sort_initial_sos). % 0.44/1.01 % set(auto2) -> assign(sos_limit, -1). % 0.44/1.01 % set(auto2) -> assign(lrs_ticks, 3000). % 0.44/1.01 % set(auto2) -> assign(max_megs, 400). % 0.44/1.01 % set(auto2) -> assign(stats, some). % 0.44/1.01 % set(auto2) -> clear(echo_input). % 0.44/1.01 % set(auto2) -> set(quiet). % 0.44/1.01 % set(auto2) -> clear(print_initial_clauses). % 0.44/1.01 % set(auto2) -> clear(print_given). % 0.44/1.01 assign(lrs_ticks,-1). % 0.44/1.01 assign(sos_limit,10000). % 0.44/1.01 assign(order,kbo). % 0.44/1.01 set(lex_order_vars). % 0.44/1.01 clear(print_given). % 0.44/1.01 % 0.44/1.01 % formulas(sos). % not echoed (7 formulas) % 0.44/1.01 % 0.44/1.01 ============================== end of input ========================== % 0.44/1.01 % 0.44/1.01 % From the command line: assign(max_seconds, 300). % 0.44/1.01 % 0.44/1.01 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.44/1.01 % 0.44/1.01 % Formulas that are not ordinary clauses: % 0.44/1.01 1 -(exists F exists E (proh(F) & aee(F,portal) & act(F,modify_act) & activates(E,F))) # label(no_proh_modify) # label(axiom) # label(non_clause). [assumption]. % 0.44/1.01 2 (all X all A all T (agent(X) & action(A) & target(T) & -(exists F exists E (proh(F) & aee(F,X) & act(F,A) & activates(E,F))) -> (exists L (permission(L) & bearer(L,X) & cnt(L,A,T))))) # label(open_world_closure) # label(axiom) # label(non_clause). [assumption]. % 0.44/1.01 3 -(exists L (permission(L) & bearer(L,portal) & cnt(L,modify_act,theater_ds))) # label(conjecture) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.44/1.01 % 0.44/1.01 ============================== end of process non-clausal formulas === % 0.44/1.01 % 0.44/1.01 ============================== PROCESS INITIAL CLAUSES =============== % 0.44/1.01 % 0.44/1.01 ============================== PREDICATE ELIMINATION ================= % 0.44/1.01 4 -agent(A) | -action(B) | -target(C) | proh(f1(A,B,C)) | permission(f3(A,B,C)) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 5 agent(portal) # label(agent_portal) # label(axiom). [assumption]. % 0.44/1.01 6 agent(ensemble) # label(agent_ensemble) # label(axiom). [assumption]. % 0.44/1.01 Derived: -action(A) | -target(B) | proh(f1(portal,A,B)) | permission(f3(portal,A,B)). [resolve(4,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | proh(f1(ensemble,A,B)) | permission(f3(ensemble,A,B)). [resolve(4,a,6,a)]. % 0.44/1.01 7 -agent(A) | -action(B) | -target(C) | proh(f1(A,B,C)) | bearer(f3(A,B,C),A) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | proh(f1(portal,A,B)) | bearer(f3(portal,A,B),portal). [resolve(7,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | proh(f1(ensemble,A,B)) | bearer(f3(ensemble,A,B),ensemble). [resolve(7,a,6,a)]. % 0.44/1.01 8 -agent(A) | -action(B) | -target(C) | aee(f1(A,B,C),A) | permission(f3(A,B,C)) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | aee(f1(portal,A,B),portal) | permission(f3(portal,A,B)). [resolve(8,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | aee(f1(ensemble,A,B),ensemble) | permission(f3(ensemble,A,B)). [resolve(8,a,6,a)]. % 0.44/1.01 9 -agent(A) | -action(B) | -target(C) | act(f1(A,B,C),B) | permission(f3(A,B,C)) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | act(f1(portal,A,B),A) | permission(f3(portal,A,B)). [resolve(9,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | act(f1(ensemble,A,B),A) | permission(f3(ensemble,A,B)). [resolve(9,a,6,a)]. % 0.44/1.01 10 -agent(A) | -action(B) | -target(C) | proh(f1(A,B,C)) | cnt(f3(A,B,C),B,C) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | proh(f1(portal,A,B)) | cnt(f3(portal,A,B),A,B). [resolve(10,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | proh(f1(ensemble,A,B)) | cnt(f3(ensemble,A,B),A,B). [resolve(10,a,6,a)]. % 0.44/1.01 11 -agent(A) | -action(B) | -target(C) | aee(f1(A,B,C),A) | bearer(f3(A,B,C),A) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | aee(f1(portal,A,B),portal) | bearer(f3(portal,A,B),portal). [resolve(11,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | aee(f1(ensemble,A,B),ensemble) | bearer(f3(ensemble,A,B),ensemble). [resolve(11,a,6,a)]. % 0.44/1.01 12 -agent(A) | -action(B) | -target(C) | act(f1(A,B,C),B) | bearer(f3(A,B,C),A) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | act(f1(portal,A,B),A) | bearer(f3(portal,A,B),portal). [resolve(12,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | act(f1(ensemble,A,B),A) | bearer(f3(ensemble,A,B),ensemble). [resolve(12,a,6,a)]. % 0.44/1.01 13 -agent(A) | -action(B) | -target(C) | aee(f1(A,B,C),A) | cnt(f3(A,B,C),B,C) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | aee(f1(portal,A,B),portal) | cnt(f3(portal,A,B),A,B). [resolve(13,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | aee(f1(ensemble,A,B),ensemble) | cnt(f3(ensemble,A,B),A,B). [resolve(13,a,6,a)]. % 0.44/1.01 14 -agent(A) | -action(B) | -target(C) | act(f1(A,B,C),B) | cnt(f3(A,B,C),B,C) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | act(f1(portal,A,B),A) | cnt(f3(portal,A,B),A,B). [resolve(14,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | act(f1(ensemble,A,B),A) | cnt(f3(ensemble,A,B),A,B). [resolve(14,a,6,a)]. % 0.44/1.01 15 -agent(A) | -action(B) | -target(C) | activates(f2(A,B,C),f1(A,B,C)) | permission(f3(A,B,C)) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | permission(f3(portal,A,B)). [resolve(15,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | activates(f2(ensemble,A,B),f1(ensemble,A,B)) | permission(f3(ensemble,A,B)). [resolve(15,a,6,a)]. % 0.44/1.01 16 -agent(A) | -action(B) | -target(C) | activates(f2(A,B,C),f1(A,B,C)) | bearer(f3(A,B,C),A) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | bearer(f3(portal,A,B),portal). [resolve(16,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | activates(f2(ensemble,A,B),f1(ensemble,A,B)) | bearer(f3(ensemble,A,B),ensemble). [resolve(16,a,6,a)]. % 0.44/1.01 17 -agent(A) | -action(B) | -target(C) | activates(f2(A,B,C),f1(A,B,C)) | cnt(f3(A,B,C),B,C) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.01 Derived: -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | cnt(f3(portal,A,B),A,B). [resolve(17,a,5,a)]. % 0.44/1.01 Derived: -action(A) | -target(B) | activates(f2(ensemble,A,B),f1(ensemble,A,B)) | cnt(f3(ensemble,A,B),A,B). [resolve(17,a,6,a)]. % 0.44/1.01 18 -action(A) | -target(B) | proh(f1(portal,A,B)) | permission(f3(portal,A,B)). [resolve(4,a,5,a)]. % 0.44/1.01 19 action(modify_act) # label(action_modify) # label(axiom). [assumption]. % 0.44/1.01 Derived: -target(A) | proh(f1(portal,modify_act,A)) | permission(f3(portal,modify_act,A)). [resolve(18,a,19,a)]. % 0.44/1.01 20 -action(A) | -target(B) | proh(f1(ensemble,A,B)) | permission(f3(ensemble,A,B)). [resolve(4,a,6,a)]. % 0.44/1.01 Derived: -target(A) | proh(f1(ensemble,modify_act,A)) | permission(f3(ensemble,modify_act,A)). [resolve(20,a,19,a)]. % 0.44/1.01 21 -action(A) | -target(B) | proh(f1(portal,A,B)) | bearer(f3(portal,A,B),portal). [resolve(7,a,5,a)]. % 0.44/1.01 Derived: -target(A) | proh(f1(portal,modify_act,A)) | bearer(f3(portal,modify_act,A),portal). [resolve(21,a,19,a)]. % 0.44/1.01 22 -action(A) | -target(B) | proh(f1(ensemble,A,B)) | bearer(f3(ensemble,A,B),ensemble). [resolve(7,a,6,a)]. % 0.44/1.01 Derived: -target(A) | proh(f1(ensemble,modify_act,A)) | bearer(f3(ensemble,modify_act,A),ensemble). [resolve(22,a,19,a)]. % 0.44/1.01 23 -action(A) | -target(B) | aee(f1(portal,A,B),portal) | permission(f3(portal,A,B)). [resolve(8,a,5,a)]. % 0.44/1.01 Derived: -target(A) | aee(f1(portal,modify_act,A),portal) | permission(f3(portal,modify_act,A)). [resolve(23,a,19,a)]. % 0.44/1.01 24 -action(A) | -target(B) | aee(f1(ensemble,A,B),ensemble) | permission(f3(ensemble,A,B)). [resolve(8,a,6,a)]. % 0.44/1.01 Derived: -target(A) | aee(f1(ensemble,modify_act,A),ensemble) | permission(f3(ensemble,modify_act,A)). [resolve(24,a,19,a)]. % 0.44/1.01 25 -action(A) | -target(B) | act(f1(portal,A,B),A) | permission(f3(portal,A,B)). [resolve(9,a,5,a)]. % 0.44/1.01 Derived: -target(A) | act(f1(portal,modify_act,A),modify_act) | permission(f3(portal,modify_act,A)). [resolve(25,a,19,a)]. % 0.44/1.01 26 -action(A) | -target(B) | act(f1(ensemble,A,B),A) | permission(f3(ensemble,A,B)). [resolve(9,a,6,a)]. % 0.44/1.01 Derived: -target(A) | act(f1(ensemble,modify_act,A),modify_act) | permission(f3(ensemble,modify_act,A)). [resolve(26,a,19,a)]. % 0.44/1.01 27 -action(A) | -target(B) | proh(f1(portal,A,B)) | cnt(f3(portal,A,B),A,B). [resolve(10,a,5,a)]. % 0.44/1.01 Derived: -target(A) | proh(f1(portal,modify_act,A)) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(27,a,19,a)]. % 0.44/1.01 28 -action(A) | -target(B) | proh(f1(ensemble,A,B)) | cnt(f3(ensemble,A,B),A,B). [resolve(10,a,6,a)]. % 0.44/1.01 Derived: -target(A) | proh(f1(ensemble,modify_act,A)) | cnt(f3(ensemble,modify_act,A),modify_act,A). [resolve(28,a,19,a)]. % 0.44/1.01 29 -action(A) | -target(B) | aee(f1(portal,A,B),portal) | bearer(f3(portal,A,B),portal). [resolve(11,a,5,a)]. % 0.44/1.01 Derived: -target(A) | aee(f1(portal,modify_act,A),portal) | bearer(f3(portal,modify_act,A),portal). [resolve(29,a,19,a)]. % 0.44/1.01 30 -action(A) | -target(B) | aee(f1(ensemble,A,B),ensemble) | bearer(f3(ensemble,A,B),ensemble). [resolve(11,a,6,a)]. % 0.44/1.01 Derived: -target(A) | aee(f1(ensemble,modify_act,A),ensemble) | bearer(f3(ensemble,modify_act,A),ensemble). [resolve(30,a,19,a)]. % 0.44/1.01 31 -action(A) | -target(B) | act(f1(portal,A,B),A) | bearer(f3(portal,A,B),portal). [resolve(12,a,5,a)]. % 0.44/1.01 Derived: -target(A) | act(f1(portal,modify_act,A),modify_act) | bearer(f3(portal,modify_act,A),portal). [resolve(31,a,19,a)]. % 0.44/1.01 32 -action(A) | -target(B) | act(f1(ensemble,A,B),A) | bearer(f3(ensemble,A,B),ensemble). [resolve(12,a,6,a)]. % 0.44/1.01 Derived: -target(A) | act(f1(ensemble,modify_act,A),modify_act) | bearer(f3(ensemble,modify_act,A),ensemble). [resolve(32,a,19,a)]. % 0.44/1.01 33 -action(A) | -target(B) | aee(f1(portal,A,B),portal) | cnt(f3(portal,A,B),A,B). [resolve(13,a,5,a)]. % 0.44/1.01 Derived: -target(A) | aee(f1(portal,modify_act,A),portal) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(33,a,19,a)]. % 0.44/1.01 34 -action(A) | -target(B) | aee(f1(ensemble,A,B),ensemble) | cnt(f3(ensemble,A,B),A,B). [resolve(13,a,6,a)]. % 0.44/1.01 Derived: -target(A) | aee(f1(ensemble,modify_act,A),ensemble) | cnt(f3(ensemble,modify_act,A),modify_act,A). [resolve(34,a,19,a)]. % 0.44/1.01 35 -action(A) | -target(B) | act(f1(portal,A,B),A) | cnt(f3(portal,A,B),A,B). [resolve(14,a,5,a)]. % 0.44/1.01 Derived: -target(A) | act(f1(portal,modify_act,A),modify_act) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(35,a,19,a)]. % 0.44/1.01 36 -action(A) | -target(B) | act(f1(ensemble,A,B),A) | cnt(f3(ensemble,A,B),A,B). [resolve(14,a,6,a)]. % 0.44/1.01 Derived: -target(A) | act(f1(ensemble,modify_act,A),modify_act) | cnt(f3(ensemble,modify_act,A),modify_act,A). [resolve(36,a,19,a)]. % 0.44/1.01 37 -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | permission(f3(portal,A,B)). [resolve(15,a,5,a)]. % 0.44/1.01 Derived: -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | permission(f3(portal,modify_act,A)). [resolve(37,a,19,a)]. % 0.44/1.01 38 -action(A) | -target(B) | activates(f2(ensemble,A,B),f1(ensemble,A,B)) | permission(f3(ensemble,A,B)). [resolve(15,a,6,a)]. % 0.44/1.01 Derived: -target(A) | activates(f2(ensemble,modify_act,A),f1(ensemble,modify_act,A)) | permission(f3(ensemble,modify_act,A)). [resolve(38,a,19,a)]. % 0.44/1.01 39 -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | bearer(f3(portal,A,B),portal). [resolve(16,a,5,a)]. % 0.44/1.01 Derived: -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | bearer(f3(portal,modify_act,A),portal). [resolve(39,a,19,a)]. % 0.44/1.01 40 -action(A) | -target(B) | activates(f2(ensemble,A,B),f1(ensemble,A,B)) | bearer(f3(ensemble,A,B),ensemble). [resolve(16,a,6,a)]. % 0.44/1.01 Derived: -target(A) | activates(f2(ensemble,modify_act,A),f1(ensemble,modify_act,A)) | bearer(f3(ensemble,modify_act,A),ensemble). [resolve(40,a,19,a)]. % 0.44/1.01 41 -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | cnt(f3(portal,A,B),A,B). [resolve(17,a,5,a)]. % 0.44/1.01 Derived: -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(41,a,19,a)]. % 0.44/1.01 42 -action(A) | -target(B) | activates(f2(ensemble,A,B),f1(ensemble,A,B)) | cnt(f3(ensemble,A,B),A,B). [resolve(17,a,6,a)]. % 0.44/1.01 Derived: -target(A) | activates(f2(ensemble,modify_act,A),f1(ensemble,modify_act,A)) | cnt(f3(ensemble,modify_act,A),modify_act,A). [resolve(42,a,19,a)]. % 0.44/1.01 43 -target(A) | proh(f1(portal,modify_act,A)) | permission(f3(portal,modify_act,A)). [resolve(18,a,19,a)]. % 0.44/1.01 44 target(theater_ds) # label(target_theater) # label(axiom). [assumption]. % 0.44/1.01 Derived: proh(f1(portal,modify_act,theater_ds)) | permission(f3(portal,modify_act,theater_ds)). [resolve(43,a,44,a)]. % 0.44/1.01 45 -target(A) | proh(f1(ensemble,modify_act,A)) | permission(f3(ensemble,modify_act,A)). [resolve(20,a,19,a)]. % 0.44/1.01 Derived: proh(f1(ensemble,modify_act,theater_ds)) | permission(f3(ensemble,modify_act,theater_ds)). [resolve(45,a,44,a)]. % 0.44/1.01 46 -target(A) | proh(f1(portal,modify_act,A)) | bearer(f3(portal,modify_act,A),portal). [resolve(21,a,19,a)]. % 0.44/1.01 Derived: proh(f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(46,a,44,a)]. % 0.44/1.01 47 -target(A) | proh(f1(ensemble,modify_act,A)) | bearer(f3(ensemble,modify_act,A),ensemble). [resolve(22,a,19,a)]. % 0.44/1.01 Derived: proh(f1(ensemble,modify_act,theater_ds)) | bearer(f3(ensemble,modify_act,theater_ds),ensemble). [resolve(47,a,44,a)]. % 0.44/1.01 48 -target(A) | aee(f1(portal,modify_act,A),portal) | permission(f3(portal,modify_act,A)). [resolve(23,a,19,a)]. % 0.44/1.01 Derived: aee(f1(portal,modify_act,theater_ds),portal) | permission(f3(portal,modify_act,theater_ds)). [resolve(48,a,44,a)]. % 0.44/1.01 49 -target(A) | aee(f1(ensemble,modify_act,A),ensemble) | permission(f3(ensemble,modify_act,A)). [resolve(24,a,19,a)]. % 0.44/1.01 Derived: aee(f1(ensemble,modify_act,theater_ds),ensemble) | permission(f3(ensemble,modify_act,theater_ds)). [resolve(49,a,44,a)]. % 0.44/1.01 50 -target(A) | act(f1(portal,modify_act,A),modify_act) | permission(f3(portal,modify_act,A)). [resolve(25,a,19,a)]. % 0.44/1.01 Derived: act(f1(portal,modify_act,theater_ds),modify_act) | permission(f3(portal,modify_act,theater_ds)). [resolve(50,a,44,a)]. % 0.44/1.01 51 -target(A) | act(f1(ensemble,modify_act,A),modify_act) | permission(f3(ensemble,modify_act,A)). [resolve(26,a,19,a)]. % 0.44/1.01 Derived: act(f1(ensemble,modify_act,theater_ds),modify_act) | permission(f3(ensemble,modify_act,theater_ds)). [resolve(51,a,44,a)]. % 0.44/1.01 52 -target(A) | proh(f1(portal,modify_act,A)) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(27,a,19,a)]. % 0.44/1.01 Derived: proh(f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(52,a,44,a)]. % 0.44/1.01 53 -target(A) | proh(f1(ensemble,modify_act,A)) | cnt(f3(ensemble,modify_act,A),modify_act,A). [resolve(28,a,19,a)]. % 0.44/1.01 Derived: proh(f1(ensemble,modify_act,theater_ds)) | cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(53,a,44,a)]. % 0.44/1.01 54 -target(A) | aee(f1(portal,modify_act,A),portal) | bearer(f3(portal,modify_act,A),portal). [resolve(29,a,19,a)]. % 0.44/1.01 Derived: aee(f1(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(54,a,44,a)]. % 0.44/1.01 55 -target(A) | aee(f1(ensemble,modify_act,A),ensemble) | bearer(f3(ensemble,modify_act,A),ensemble). [resolve(30,a,19,a)]. % 0.44/1.01 Derived: aee(f1(ensemble,modify_act,theater_ds),ensemble) | bearer(f3(ensemble,modify_act,theater_ds),ensemble). [resolve(55,a,44,a)]. % 0.44/1.01 56 -target(A) | act(f1(portal,modify_act,A),modify_act) | bearer(f3(portal,modify_act,A),portal). [resolve(31,a,19,a)]. % 0.44/1.01 Derived: act(f1(portal,modify_act,theater_ds),modify_act) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(56,a,44,a)]. % 0.44/1.01 57 -target(A) | act(f1(ensemble,modify_act,A),modify_act) | bearer(f3(ensemble,modify_act,A),ensemble). [resolve(32,a,19,a)]. % 0.44/1.01 Derived: act(f1(ensemble,modify_act,theater_ds),modify_act) | bearer(f3(ensemble,modify_act,theater_ds),ensemble). [resolve(57,a,44,a)]. % 0.44/1.01 58 -target(A) | aee(f1(portal,modify_act,A),portal) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(33,a,19,a)]. % 0.44/1.01 Derived: aee(f1(portal,modify_act,theater_ds),portal) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(58,a,44,a)]. % 0.44/1.01 59 -target(A) | aee(f1(ensemble,modify_act,A),ensemble) | cnt(f3(ensemble,modify_act,A),modify_act,A). [resolve(34,a,19,a)]. % 0.44/1.01 Derived: aee(f1(ensemble,modify_act,theater_ds),ensemble) | cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(59,a,44,a)]. % 0.44/1.01 60 -target(A) | act(f1(portal,modify_act,A),modify_act) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(35,a,19,a)]. % 0.44/1.01 Derived: act(f1(portal,modify_act,theater_ds),modify_act) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(60,a,44,a)]. % 0.44/1.01 61 -target(A) | act(f1(ensemble,modify_act,A),modify_act) | cnt(f3(ensemble,modify_act,A),modify_act,A). [resolve(36,a,19,a)]. % 0.44/1.01 Derived: act(f1(ensemble,modify_act,theater_ds),modify_act) | cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(61,a,44,a)]. % 0.44/1.01 62 -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | permission(f3(portal,modify_act,A)). [resolve(37,a,19,a)]. % 0.44/1.01 Derived: activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | permission(f3(portal,modify_act,theater_ds)). [resolve(62,a,44,a)]. % 0.44/1.01 63 -target(A) | activates(f2(ensemble,modify_act,A),f1(ensemble,modify_act,A)) | permission(f3(ensemble,modify_act,A)). [resolve(38,a,19,a)]. % 0.44/1.01 Derived: activates(f2(ensemble,modify_act,theater_ds),f1(ensemble,modify_act,theater_ds)) | permission(f3(ensemble,modify_act,theater_ds)). [resolve(63,a,44,a)]. % 0.44/1.01 64 -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | bearer(f3(portal,modify_act,A),portal). [resolve(39,a,19,a)]. % 0.44/1.01 Derived: activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(64,a,44,a)]. % 0.44/1.01 65 -target(A) | activates(f2(ensemble,modify_act,A),f1(ensemble,modify_act,A)) | bearer(f3(ensemble,modify_act,A),ensemble). [resolve(40,a,19,a)]. % 0.44/1.01 Derived: activates(f2(ensemble,modify_act,theater_ds),f1(ensemble,modify_act,theater_ds)) | bearer(f3(ensemble,modify_act,theater_ds),ensemble). [resolve(65,a,44,a)]. % 0.44/1.01 66 -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(41,a,19,a)]. % 0.44/1.01 Derived: activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(66,a,44,a)]. % 0.44/1.01 67 -target(A) | activates(f2(ensemble,modify_act,A),f1(ensemble,modify_act,A)) | cnt(f3(ensemble,modify_act,A),modify_act,A). [resolve(42,a,19,a)]. % 0.44/1.01 Derived: activates(f2(ensemble,modify_act,theater_ds),f1(ensemble,modify_act,theater_ds)) | cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(67,a,44,a)]. % 0.44/1.01 68 proh(f1(portal,modify_act,theater_ds)) | permission(f3(portal,modify_act,theater_ds)). [resolve(43,a,44,a)]. % 0.44/1.01 69 -permission(A) | -bearer(A,portal) | -cnt(A,modify_act,theater_ds) # label(conjecture) # label(negated_conjecture). [clausify(3)]. % 0.44/1.01 Derived: proh(f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(68,b,69,a)]. % 0.44/1.01 70 proh(f1(ensemble,modify_act,theater_ds)) | permission(f3(ensemble,modify_act,theater_ds)). [resolve(45,a,44,a)]. % 0.44/1.01 Derived: proh(f1(ensemble,modify_act,theater_ds)) | -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(70,b,69,a)]. % 0.44/1.01 71 aee(f1(portal,modify_act,theater_ds),portal) | permission(f3(portal,modify_act,theater_ds)). [resolve(48,a,44,a)]. % 0.44/1.01 Derived: aee(f1(portal,modify_act,theater_ds),portal) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(71,b,69,a)]. % 0.44/1.01 72 aee(f1(ensemble,modify_act,theater_ds),ensemble) | permission(f3(ensemble,modify_act,theater_ds)). [resolve(49,a,44,a)]. % 0.44/1.01 Derived: aee(f1(ensemble,modify_act,theater_ds),ensemble) | -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(72,b,69,a)]. % 0.44/1.01 73 act(f1(portal,modify_act,theater_ds),modify_act) | permission(f3(portal,modify_act,theater_ds)). [resolve(50,a,44,a)]. % 0.44/1.01 Derived: act(f1(portal,modify_act,theater_ds),modify_act) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(73,b,69,a)]. % 0.44/1.01 74 act(f1(ensemble,modify_act,theater_ds),modify_act) | permission(f3(ensemble,modify_act,theater_ds)). [resolve(51,a,44,a)]. % 0.44/1.01 Derived: act(f1(ensemble,modify_act,theater_ds),modify_act) | -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(74,b,69,a)]. % 0.44/1.01 75 activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | permission(f3(portal,modify_act,theater_ds)). [resolve(62,a,44,a)]. % 0.44/1.01 Derived: activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(75,b,69,a)]. % 0.44/1.01 76 activates(f2(ensemble,modify_act,theater_ds),f1(ensemble,modify_act,theater_ds)) | permission(f3(ensemble,modify_act,theater_ds)). [resolve(63,a,44,a)]. % 0.44/1.01 Derived: activates(f2(ensemble,modify_act,theater_ds),f1(ensemble,modify_act,theater_ds)) | -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(76,b,69,a)]. % 0.44/1.01 77 proh(f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(46,a,44,a)]. % 0.44/1.01 78 -proh(A) | -aee(A,portal) | -act(A,modify_act) | -activates(B,A) # label(no_proh_modify) # label(axiom). [clausify(1)]. % 0.44/1.01 Derived: bearer(f3(portal,modify_act,theater_ds),portal) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(77,a,78,a)]. % 0.44/1.01 79 proh(f1(ensemble,modify_act,theater_ds)) | bearer(f3(ensemble,modify_act,theater_ds),ensemble). [resolve(47,a,44,a)]. % 0.44/1.01 Derived: bearer(f3(ensemble,modify_act,theater_ds),ensemble) | -aee(f1(ensemble,modify_act,theater_ds),portal) | -act(f1(ensemble,modify_act,theater_ds),modify_act) | -activates(A,f1(ensemble,modify_act,theater_ds)). [resolve(79,a,78,a)]. % 0.44/1.01 80 proh(f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(52,a,44,a)]. % 0.44/1.01 Derived: cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(80,a,78,a)]. % 0.44/1.01 81 proh(f1(ensemble,modify_act,theater_ds)) | cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(53,a,44,a)]. % 0.44/1.01 Derived: cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(ensemble,modify_act,theater_ds),portal) | -act(f1(ensemble,modify_act,theater_ds),modify_act) | -activates(A,f1(ensemble,modify_act,theater_ds)). [resolve(81,a,78,a)]. % 0.44/1.01 82 proh(f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(68,b,69,a)]. % 0.44/1.01 Derived: -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(82,a,78,a)]. % 0.44/1.01 83 proh(f1(ensemble,modify_act,theater_ds)) | -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(70,b,69,a)]. % 0.44/1.01 Derived: -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(ensemble,modify_act,theater_ds),portal) | -act(f1(ensemble,modify_act,theater_ds),modify_act) | -activates(A,f1(ensemble,modify_act,theater_ds)). [resolve(83,a,78,a)]. % 0.44/1.01 84 bearer(f3(portal,modify_act,theater_ds),portal) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(77,a,78,a)]. % 0.44/1.01 85 aee(f1(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(54,a,44,a)]. % 0.44/1.01 86 aee(f1(ensemble,modify_act,theater_ds),ensemble) | bearer(f3(ensemble,modify_act,theater_ds),ensemble). [resolve(55,a,44,a)]. % 0.44/1.01 87 aee(f1(portal,modify_act,theater_ds),portal) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(58,a,44,a)]. % 0.44/1.01 88 aee(f1(ensemble,modify_act,theater_ds),ensemble) | cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(59,a,44,a)]. % 0.44/1.01 89 aee(f1(portal,modify_act,theater_ds),portal) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(71,b,69,a)]. % 0.44/1.01 90 aee(f1(ensemble,modify_act,theater_ds),ensemble) | -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(72,b,69,a)]. % 0.44/1.01 Derived: bearer(f3(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(84,b,85,a)]. % 0.44/1.01 91 bearer(f3(ensemble,modify_act,theater_ds),ensemble) | -aee(f1(ensemble,modify_act,theater_ds),portal) | -act(f1(ensemble,modify_act,theater_ds),modify_act) | -activates(A,f1(ensemble,modify_act,theater_ds)). [resolve(79,a,78,a)]. % 0.44/1.01 92 cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(80,a,78,a)]. % 0.44/1.01 Derived: cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(92,b,87,a)]. % 0.44/1.01 93 cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(ensemble,modify_act,theater_ds),portal) | -act(f1(ensemble,modify_act,theater_ds),modify_act) | -activates(A,f1(ensemble,modify_act,theater_ds)). [resolve(81,a,78,a)]. % 0.44/1.01 94 -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(82,a,78,a)]. % 0.44/1.01 Derived: -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(94,c,89,a)]. % 0.44/1.01 95 -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(ensemble,modify_act,theater_ds),portal) | -act(f1(ensemble,modify_act,theater_ds),modify_act) | -activates(A,f1(ensemble,modify_act,theater_ds)). [resolve(83,a,78,a)]. % 0.44/1.01 96 bearer(f3(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(84,b,85,a)]. % 0.44/1.01 97 act(f1(portal,modify_act,theater_ds),modify_act) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(56,a,44,a)]. % 0.44/1.01 98 act(f1(ensemble,modify_act,theater_ds),modify_act) | bearer(f3(ensemble,modify_act,theater_ds),ensemble). [resolve(57,a,44,a)]. % 0.44/1.01 99 act(f1(portal,modify_act,theater_ds),modify_act) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(60,a,44,a)]. % 0.44/1.01 100 act(f1(ensemble,modify_act,theater_ds),modify_act) | cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(61,a,44,a)]. % 0.44/1.01 101 act(f1(portal,modify_act,theater_ds),modify_act) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(73,b,69,a)]. % 0.44/1.01 102 act(f1(ensemble,modify_act,theater_ds),modify_act) | -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(74,b,69,a)]. % 0.44/1.01 Derived: bearer(f3(portal,modify_act,theater_ds),portal) | -activates(A,f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(96,b,97,a)]. % 0.44/1.01 103 cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(92,b,87,a)]. % 0.44/1.01 Derived: cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -activates(A,f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(103,b,99,a)]. % 0.44/1.01 104 -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(94,c,89,a)]. % 0.44/1.01 Derived: -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -activates(A,f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(104,c,101,a)]. % 0.44/1.01 105 bearer(f3(portal,modify_act,theater_ds),portal) | -activates(A,f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(96,b,97,a)]. % 0.44/1.01 106 activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(64,a,44,a)]. % 0.44/1.01 107 activates(f2(ensemble,modify_act,theater_ds),f1(ensemble,modify_act,theater_ds)) | bearer(f3(ensemble,modify_act,theater_ds),ensemble). [resolve(65,a,44,a)]. % 0.44/1.01 108 activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(66,a,44,a)]. % 0.44/1.01 109 activates(f2(ensemble,modify_act,theater_ds),f1(ensemble,modify_act,theater_ds)) | cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(67,a,44,a)]. % 0.44/1.01 110 activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(75,b,69,a)]. % 0.44/1.01 111 activates(f2(ensemble,modify_act,theater_ds),f1(ensemble,modify_act,theater_ds)) | -bearer(f3(ensemble,modify_act,theater_ds),portal) | -cnt(f3(ensemble,modify_act,theater_ds),modify_act,theater_ds). [resolve(76,b,69,a)]. % 0.44/1.01 Derived: bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(105,b,106,a)]. % 0.44/1.02 112 cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -activates(A,f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(103,b,99,a)]. % 0.44/1.02 Derived: cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(112,b,108,a)]. % 0.44/1.02 113 -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -activates(A,f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(104,c,101,a)]. % 0.44/1.02 Derived: -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(113,c,110,a)]. % 0.44/1.02 % 0.44/1.02 ============================== end predicate elimination ============= % 0.44/1.02 % 0.44/1.02 Auto_denials: (non-Horn, no changes). % 0.44/1.02 % 0.44/1.02 Term ordering decisions: % 0.44/1.02 Function symbol KB weights: modify_act=1. portal=1. theater_ds=1. f3=1. % 0.44/1.02 % 0.44/1.02 ============================== PROOF ================================= % 0.44/1.02 % SZS status Theorem % 0.44/1.02 % SZS output start Refutation % 0.44/1.02 % 0.44/1.02 % Proof 1 at 0.02 (+ 0.00) seconds. % 0.44/1.02 % Length of proof is 75. % 0.44/1.02 % Level of proof is 10. % 0.44/1.02 % Maximum clause weight is 7.000. % 0.44/1.02 % Given clauses 0. % 0.44/1.02 % 0.44/1.02 1 -(exists F exists E (proh(F) & aee(F,portal) & act(F,modify_act) & activates(E,F))) # label(no_proh_modify) # label(axiom) # label(non_clause). [assumption]. % 0.44/1.02 2 (all X all A all T (agent(X) & action(A) & target(T) & -(exists F exists E (proh(F) & aee(F,X) & act(F,A) & activates(E,F))) -> (exists L (permission(L) & bearer(L,X) & cnt(L,A,T))))) # label(open_world_closure) # label(axiom) # label(non_clause). [assumption]. % 0.44/1.02 3 -(exists L (permission(L) & bearer(L,portal) & cnt(L,modify_act,theater_ds))) # label(conjecture) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.44/1.02 4 -agent(A) | -action(B) | -target(C) | proh(f1(A,B,C)) | permission(f3(A,B,C)) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 5 agent(portal) # label(agent_portal) # label(axiom). [assumption]. % 0.44/1.02 7 -agent(A) | -action(B) | -target(C) | proh(f1(A,B,C)) | bearer(f3(A,B,C),A) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 8 -agent(A) | -action(B) | -target(C) | aee(f1(A,B,C),A) | permission(f3(A,B,C)) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 9 -agent(A) | -action(B) | -target(C) | act(f1(A,B,C),B) | permission(f3(A,B,C)) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 10 -agent(A) | -action(B) | -target(C) | proh(f1(A,B,C)) | cnt(f3(A,B,C),B,C) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 11 -agent(A) | -action(B) | -target(C) | aee(f1(A,B,C),A) | bearer(f3(A,B,C),A) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 12 -agent(A) | -action(B) | -target(C) | act(f1(A,B,C),B) | bearer(f3(A,B,C),A) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 13 -agent(A) | -action(B) | -target(C) | aee(f1(A,B,C),A) | cnt(f3(A,B,C),B,C) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 14 -agent(A) | -action(B) | -target(C) | act(f1(A,B,C),B) | cnt(f3(A,B,C),B,C) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 15 -agent(A) | -action(B) | -target(C) | activates(f2(A,B,C),f1(A,B,C)) | permission(f3(A,B,C)) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 16 -agent(A) | -action(B) | -target(C) | activates(f2(A,B,C),f1(A,B,C)) | bearer(f3(A,B,C),A) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 17 -agent(A) | -action(B) | -target(C) | activates(f2(A,B,C),f1(A,B,C)) | cnt(f3(A,B,C),B,C) # label(open_world_closure) # label(axiom). [clausify(2)]. % 0.44/1.02 18 -action(A) | -target(B) | proh(f1(portal,A,B)) | permission(f3(portal,A,B)). [resolve(4,a,5,a)]. % 0.44/1.02 19 action(modify_act) # label(action_modify) # label(axiom). [assumption]. % 0.44/1.02 21 -action(A) | -target(B) | proh(f1(portal,A,B)) | bearer(f3(portal,A,B),portal). [resolve(7,a,5,a)]. % 0.44/1.02 23 -action(A) | -target(B) | aee(f1(portal,A,B),portal) | permission(f3(portal,A,B)). [resolve(8,a,5,a)]. % 0.44/1.02 25 -action(A) | -target(B) | act(f1(portal,A,B),A) | permission(f3(portal,A,B)). [resolve(9,a,5,a)]. % 0.44/1.02 27 -action(A) | -target(B) | proh(f1(portal,A,B)) | cnt(f3(portal,A,B),A,B). [resolve(10,a,5,a)]. % 0.44/1.02 29 -action(A) | -target(B) | aee(f1(portal,A,B),portal) | bearer(f3(portal,A,B),portal). [resolve(11,a,5,a)]. % 0.44/1.02 31 -action(A) | -target(B) | act(f1(portal,A,B),A) | bearer(f3(portal,A,B),portal). [resolve(12,a,5,a)]. % 0.44/1.02 33 -action(A) | -target(B) | aee(f1(portal,A,B),portal) | cnt(f3(portal,A,B),A,B). [resolve(13,a,5,a)]. % 0.44/1.02 35 -action(A) | -target(B) | act(f1(portal,A,B),A) | cnt(f3(portal,A,B),A,B). [resolve(14,a,5,a)]. % 0.44/1.02 37 -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | permission(f3(portal,A,B)). [resolve(15,a,5,a)]. % 0.44/1.02 39 -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | bearer(f3(portal,A,B),portal). [resolve(16,a,5,a)]. % 0.44/1.02 41 -action(A) | -target(B) | activates(f2(portal,A,B),f1(portal,A,B)) | cnt(f3(portal,A,B),A,B). [resolve(17,a,5,a)]. % 0.44/1.02 43 -target(A) | proh(f1(portal,modify_act,A)) | permission(f3(portal,modify_act,A)). [resolve(18,a,19,a)]. % 0.44/1.02 44 target(theater_ds) # label(target_theater) # label(axiom). [assumption]. % 0.44/1.02 46 -target(A) | proh(f1(portal,modify_act,A)) | bearer(f3(portal,modify_act,A),portal). [resolve(21,a,19,a)]. % 0.44/1.02 48 -target(A) | aee(f1(portal,modify_act,A),portal) | permission(f3(portal,modify_act,A)). [resolve(23,a,19,a)]. % 0.44/1.02 50 -target(A) | act(f1(portal,modify_act,A),modify_act) | permission(f3(portal,modify_act,A)). [resolve(25,a,19,a)]. % 0.44/1.02 52 -target(A) | proh(f1(portal,modify_act,A)) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(27,a,19,a)]. % 0.44/1.02 54 -target(A) | aee(f1(portal,modify_act,A),portal) | bearer(f3(portal,modify_act,A),portal). [resolve(29,a,19,a)]. % 0.44/1.02 56 -target(A) | act(f1(portal,modify_act,A),modify_act) | bearer(f3(portal,modify_act,A),portal). [resolve(31,a,19,a)]. % 0.44/1.02 58 -target(A) | aee(f1(portal,modify_act,A),portal) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(33,a,19,a)]. % 0.44/1.02 60 -target(A) | act(f1(portal,modify_act,A),modify_act) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(35,a,19,a)]. % 0.44/1.02 62 -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | permission(f3(portal,modify_act,A)). [resolve(37,a,19,a)]. % 0.44/1.02 64 -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | bearer(f3(portal,modify_act,A),portal). [resolve(39,a,19,a)]. % 0.44/1.02 66 -target(A) | activates(f2(portal,modify_act,A),f1(portal,modify_act,A)) | cnt(f3(portal,modify_act,A),modify_act,A). [resolve(41,a,19,a)]. % 0.44/1.02 68 proh(f1(portal,modify_act,theater_ds)) | permission(f3(portal,modify_act,theater_ds)). [resolve(43,a,44,a)]. % 0.44/1.02 69 -permission(A) | -bearer(A,portal) | -cnt(A,modify_act,theater_ds) # label(conjecture) # label(negated_conjecture). [clausify(3)]. % 0.44/1.02 71 aee(f1(portal,modify_act,theater_ds),portal) | permission(f3(portal,modify_act,theater_ds)). [resolve(48,a,44,a)]. % 0.44/1.02 73 act(f1(portal,modify_act,theater_ds),modify_act) | permission(f3(portal,modify_act,theater_ds)). [resolve(50,a,44,a)]. % 0.44/1.02 75 activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | permission(f3(portal,modify_act,theater_ds)). [resolve(62,a,44,a)]. % 0.44/1.02 77 proh(f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(46,a,44,a)]. % 0.44/1.02 78 -proh(A) | -aee(A,portal) | -act(A,modify_act) | -activates(B,A) # label(no_proh_modify) # label(axiom). [clausify(1)]. % 0.44/1.02 80 proh(f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(52,a,44,a)]. % 0.44/1.02 82 proh(f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(68,b,69,a)]. % 0.44/1.02 84 bearer(f3(portal,modify_act,theater_ds),portal) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(77,a,78,a)]. % 0.44/1.02 85 aee(f1(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(54,a,44,a)]. % 0.44/1.02 87 aee(f1(portal,modify_act,theater_ds),portal) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(58,a,44,a)]. % 0.44/1.02 89 aee(f1(portal,modify_act,theater_ds),portal) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(71,b,69,a)]. % 0.44/1.02 92 cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(80,a,78,a)]. % 0.44/1.02 94 -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -aee(f1(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)). [resolve(82,a,78,a)]. % 0.44/1.02 96 bearer(f3(portal,modify_act,theater_ds),portal) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(84,b,85,a)]. % 0.44/1.02 97 act(f1(portal,modify_act,theater_ds),modify_act) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(56,a,44,a)]. % 0.44/1.02 99 act(f1(portal,modify_act,theater_ds),modify_act) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(60,a,44,a)]. % 0.44/1.02 101 act(f1(portal,modify_act,theater_ds),modify_act) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(73,b,69,a)]. % 0.44/1.02 103 cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(92,b,87,a)]. % 0.44/1.02 104 -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -act(f1(portal,modify_act,theater_ds),modify_act) | -activates(A,f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(94,c,89,a)]. % 0.44/1.02 105 bearer(f3(portal,modify_act,theater_ds),portal) | -activates(A,f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(96,b,97,a)]. % 0.44/1.02 106 activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(64,a,44,a)]. % 0.44/1.02 108 activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(66,a,44,a)]. % 0.44/1.02 110 activates(f2(portal,modify_act,theater_ds),f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(75,b,69,a)]. % 0.44/1.02 112 cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -activates(A,f1(portal,modify_act,theater_ds)) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(103,b,99,a)]. % 0.44/1.02 113 -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -activates(A,f1(portal,modify_act,theater_ds)) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(104,c,101,a)]. % 0.44/1.02 114 bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal) | bearer(f3(portal,modify_act,theater_ds),portal). [resolve(105,b,106,a)]. % 0.44/1.02 115 bearer(f3(portal,modify_act,theater_ds),portal). [copy(114),merge(b),merge(c),merge(d)]. % 0.44/1.02 116 cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(112,b,108,a)]. % 0.44/1.02 117 cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [copy(116),merge(b),merge(c),merge(d)]. % 0.44/1.02 118 -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds) | -bearer(f3(portal,modify_act,theater_ds),portal) | -cnt(f3(portal,modify_act,theater_ds),modify_act,theater_ds). [resolve(113,c,110,a)]. % 0.44/1.02 119 $F. [copy(118),merge(c),merge(d),merge(e),merge(f),merge(g),merge(h),unit_del(a,115),unit_del(b,117)]. % 0.44/1.02 % 0.44/1.02 % SZS output end Refutation % 0.44/1.02 ============================== end of proof ========================== % 0.44/1.02 % 0.44/1.02 ============================== STATISTICS ============================ % 0.44/1.02 % 0.44/1.02 Given=0. Generated=3. Kept=2. proofs=1. % 0.44/1.02 Usable=0. Sos=0. Demods=0. Limbo=2, Disabled=113. Hints=0. % 0.44/1.02 Megabytes=0.09. % 0.44/1.02 User_CPU=0.02, System_CPU=0.00, Wall_clock=0. % 0.44/1.02 % 0.44/1.02 ============================== end of statistics ===================== % 0.44/1.02 % 0.44/1.02 ============================== end of search ========================= % 0.44/1.02 % 0.44/1.02 THEOREM PROVED % 0.44/1.02 % SZS status Theorem % 0.44/1.02 % 0.44/1.02 Exiting with 1 proof. % 0.44/1.02 % 0.44/1.02 Process 9614 exit (max_proofs) Tue Apr 28 19:29:21 2026 % 0.44/1.02 Prover9 interrupted %------------------------------------------------------------------------------