%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n027.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.75s 1.05s % Output : Refutation 0.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : MGT113+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.34 % Computer : n027.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue Apr 28 19:30:50 EDT 2026 % 0.15/0.34 % CPUTime : % 0.43/1.03 ============================== Prover9 =============================== % 0.43/1.03 Prover9 (32) version 2009-11A, November 2009. % 0.43/1.03 Process 29303 was started by sandbox on n027.cluster.edu, % 0.43/1.03 Tue Apr 28 19:30:50 2026 % 0.43/1.03 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_29118_n027.cluster.edu". % 0.43/1.03 ============================== end of head =========================== % 0.43/1.03 % 0.43/1.03 ============================== INPUT ================================= % 0.43/1.03 % 0.43/1.03 % Reading from file /tmp/Prover9_29118_n027.cluster.edu % 0.43/1.03 % 0.43/1.03 set(prolog_style_variables). % 0.43/1.03 set(auto2). % 0.43/1.03 % set(auto2) -> set(auto). % 0.43/1.03 % set(auto) -> set(auto_inference). % 0.43/1.03 % set(auto) -> set(auto_setup). % 0.43/1.03 % set(auto_setup) -> set(predicate_elim). % 0.43/1.03 % set(auto_setup) -> assign(eq_defs, unfold). % 0.43/1.03 % set(auto) -> set(auto_limits). % 0.43/1.03 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.43/1.03 % set(auto_limits) -> assign(sos_limit, 20000). % 0.43/1.03 % set(auto) -> set(auto_denials). % 0.43/1.03 % set(auto) -> set(auto_process). % 0.43/1.03 % set(auto2) -> assign(new_constants, 1). % 0.43/1.03 % set(auto2) -> assign(fold_denial_max, 3). % 0.43/1.03 % set(auto2) -> assign(max_weight, "200.000"). % 0.43/1.03 % set(auto2) -> assign(max_hours, 1). % 0.43/1.03 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.43/1.03 % set(auto2) -> assign(max_seconds, 0). % 0.43/1.03 % set(auto2) -> assign(max_minutes, 5). % 0.43/1.03 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.43/1.03 % set(auto2) -> set(sort_initial_sos). % 0.43/1.03 % set(auto2) -> assign(sos_limit, -1). % 0.43/1.03 % set(auto2) -> assign(lrs_ticks, 3000). % 0.43/1.03 % set(auto2) -> assign(max_megs, 400). % 0.43/1.03 % set(auto2) -> assign(stats, some). % 0.43/1.03 % set(auto2) -> clear(echo_input). % 0.43/1.03 % set(auto2) -> set(quiet). % 0.43/1.03 % set(auto2) -> clear(print_initial_clauses). % 0.43/1.03 % set(auto2) -> clear(print_given). % 0.43/1.03 assign(lrs_ticks,-1). % 0.43/1.03 assign(sos_limit,10000). % 0.43/1.03 assign(order,kbo). % 0.43/1.03 set(lex_order_vars). % 0.43/1.03 clear(print_given). % 0.43/1.03 % 0.43/1.03 % formulas(sos). % not echoed (23 formulas) % 0.43/1.03 % 0.43/1.03 ============================== end of input ========================== % 0.43/1.03 % 0.43/1.03 % From the command line: assign(max_seconds, 300). % 0.43/1.03 % 0.43/1.03 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.43/1.03 % 0.43/1.03 % Formulas that are not ordinary clauses: % 0.43/1.03 1 (all F all X all Y all A all T all E (proh(F) & aee(F,X) & aer(F,Y) & act(F,A) & tgt(F,T) & activates(E,F) -> (exists Rho exists D exists C (founds(E,Rho,F) & duty(D) & bearer(D,X) & cnt(D,rfr(A),T) & part_of(D,Rho) & right(C) & bearer(C,Y) & cnt(C,rfr(A),T) & part_of(C,Rho))))) # label(ax_proh_relator_conduct) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.03 2 (all F all X all Y all A all T all E (proh(F) & has_rem(F) & aee(F,X) & aer(F,Y) & act(F,A) & tgt(F,T) & activates(E,F) -> (exists RhoR exists Pw exists S (founds_rem(E,RhoR,F) & power(Pw) & bearer(Pw,Y) & cnt(Pw,decl(A),T) & part_of(Pw,RhoR) & subjection(S) & bearer(S,X) & cnt(S,decl(A),T) & part_of(S,RhoR))))) # label(ax_proh_relator_remedy) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.03 3 (all X all A all T all Q (norm_state_change(X,A,T,Q) -> (exists E (inst_event(E) & triggers(E,X,A,T,Q))))) # label(ax_A1) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.03 4 (all E (inst_event(E) -> (exists Y competent_for(Y,E)))) # label(ax_A2) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.03 5 (all Y all E (competent_for(Y,E) -> (exists Pw exists S exists X (power(Pw) & bearer(Pw,Y) & about_event(Pw,E) & subjection(S) & bearer(S,X) & about_event(S,E))))) # label(ax_A3) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.03 6 (all F all X all A all T (proh(F) & has_rem(F) & act(F,A) & tgt(F,T) & aee(F,X) & does(X,A,T) -> (exists B (rem_act(F,B) & norm_state_change(X,B,T,duty_rem))))) # label(ax_B1) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.03 7 (all Pw all A all T all Rho all E all R (power(Pw) & cnt(Pw,decl(A),T) & part_of(Pw,Rho) & founds_rem(E,Rho,R) -> about_event(Pw,E))) # label(ax_B2) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.03 8 (all S all A all T all Rho all E all R (subjection(S) & cnt(S,decl(A),T) & part_of(S,Rho) & founds_rem(E,Rho,R) -> about_event(S,E))) # label(ax_B3) # label(axiom) # label(non_clause). [assumption]. % 0.43/1.03 9 -(exists RhoR exists Pw exists S (founds_rem(e1,RhoR,f1) & power(Pw) & bearer(Pw,philharmonie) & cnt(Pw,decl(distrib),concert_ds) & part_of(Pw,RhoR) & about_event(Pw,e1) & subjection(S) & bearer(S,marketplace) & cnt(S,decl(distrib),concert_ds) & part_of(S,RhoR) & about_event(S,e1))) # label(conjecture) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.03 % 0.75/1.03 ============================== end of process non-clausal formulas === % 0.75/1.03 % 0.75/1.03 ============================== PROCESS INITIAL CLAUSES =============== % 0.75/1.03 % 0.75/1.03 ============================== PREDICATE ELIMINATION ================= % 0.75/1.03 10 -proh(A) | -has_rem(A) | -act(A,B) | -tgt(A,C) | -aee(A,D) | -does(D,B,C) | rem_act(A,f12(A,D,B,C)) # label(ax_B1) # label(axiom). [clausify(6)]. % 0.75/1.03 11 proh(f1) # label(proh_f1) # label(axiom). [assumption]. % 0.75/1.03 Derived: -has_rem(f1) | -act(f1,A) | -tgt(f1,B) | -aee(f1,C) | -does(C,A,B) | rem_act(f1,f12(f1,C,A,B)). [resolve(10,a,11,a)]. % 0.75/1.03 12 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | duty(f2(A,B,C,D,E,F)) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | duty(f2(f1,A,B,C,D,E)). [resolve(12,a,11,a)]. % 0.75/1.03 13 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | right(f3(A,B,C,D,E,F)) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | right(f3(f1,A,B,C,D,E)). [resolve(13,a,11,a)]. % 0.75/1.03 14 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | bearer(f2(A,B,C,D,E,F),B) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f2(f1,A,B,C,D,E),A). [resolve(14,a,11,a)]. % 0.75/1.03 15 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | bearer(f3(A,B,C,D,E,F),C) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f3(f1,A,B,C,D,E),B). [resolve(15,a,11,a)]. % 0.75/1.03 16 -proh(A) | -has_rem(A) | -act(A,B) | -tgt(A,C) | -aee(A,D) | -does(D,B,C) | norm_state_change(D,f12(A,D,B,C),C,duty_rem) # label(ax_B1) # label(axiom). [clausify(6)]. % 0.75/1.03 Derived: -has_rem(f1) | -act(f1,A) | -tgt(f1,B) | -aee(f1,C) | -does(C,A,B) | norm_state_change(C,f12(f1,C,A,B),B,duty_rem). [resolve(16,a,11,a)]. % 0.75/1.03 17 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | founds(F,f1(A,B,C,D,E,F),A) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | founds(E,f1(f1,A,B,C,D,E),f1). [resolve(17,a,11,a)]. % 0.75/1.03 18 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | power(f5(A,B,C,D,E,F)) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | power(f5(f1,A,B,C,D,E)). [resolve(18,a,11,a)]. % 0.75/1.03 19 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | subjection(f6(A,B,C,D,E,F)) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | subjection(f6(f1,A,B,C,D,E)). [resolve(19,a,11,a)]. % 0.75/1.03 20 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f2(A,B,C,D,E,F),rfr(D),E) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f2(f1,A,B,C,D,E),rfr(C),D). [resolve(20,a,11,a)]. % 0.75/1.03 21 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f3(A,B,C,D,E,F),rfr(D),E) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f3(f1,A,B,C,D,E),rfr(C),D). [resolve(21,a,11,a)]. % 0.75/1.03 22 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | bearer(f5(A,B,C,D,E,F),C) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f5(f1,A,B,C,D,E),B). [resolve(22,a,11,a)]. % 0.75/1.03 23 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | bearer(f6(A,B,C,D,E,F),B) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f6(f1,A,B,C,D,E),A). [resolve(23,a,11,a)]. % 0.75/1.03 24 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | founds_rem(F,f4(A,B,C,D,E,F),A) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | founds_rem(E,f4(f1,A,B,C,D,E),f1). [resolve(24,a,11,a)]. % 0.75/1.03 25 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f5(A,B,C,D,E,F),decl(D),E) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f5(f1,A,B,C,D,E),decl(C),D). [resolve(25,a,11,a)]. % 0.75/1.03 26 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f6(A,B,C,D,E,F),decl(D),E) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f6(f1,A,B,C,D,E),decl(C),D). [resolve(26,a,11,a)]. % 0.75/1.03 27 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | part_of(f2(A,B,C,D,E,F),f1(A,B,C,D,E,F)) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f2(f1,A,B,C,D,E),f1(f1,A,B,C,D,E)). [resolve(27,a,11,a)]. % 0.75/1.03 28 -proh(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | part_of(f3(A,B,C,D,E,F),f1(A,B,C,D,E,F)) # label(ax_proh_relator_conduct) # label(axiom). [clausify(1)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f3(f1,A,B,C,D,E),f1(f1,A,B,C,D,E)). [resolve(28,a,11,a)]. % 0.75/1.03 29 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | part_of(f5(A,B,C,D,E,F),f4(A,B,C,D,E,F)) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f5(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(29,a,11,a)]. % 0.75/1.03 30 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | part_of(f6(A,B,C,D,E,F),f4(A,B,C,D,E,F)) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.03 Derived: -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f6(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(30,a,11,a)]. % 0.75/1.03 31 -has_rem(f1) | -act(f1,A) | -tgt(f1,B) | -aee(f1,C) | -does(C,A,B) | rem_act(f1,f12(f1,C,A,B)). [resolve(10,a,11,a)]. % 0.75/1.03 32 has_rem(f1) # label(rem_f1) # label(axiom). [assumption]. % 0.75/1.03 Derived: -act(f1,A) | -tgt(f1,B) | -aee(f1,C) | -does(C,A,B) | rem_act(f1,f12(f1,C,A,B)). [resolve(31,a,32,a)]. % 0.75/1.03 33 -has_rem(f1) | -act(f1,A) | -tgt(f1,B) | -aee(f1,C) | -does(C,A,B) | norm_state_change(C,f12(f1,C,A,B),B,duty_rem). [resolve(16,a,11,a)]. % 0.75/1.03 Derived: -act(f1,A) | -tgt(f1,B) | -aee(f1,C) | -does(C,A,B) | norm_state_change(C,f12(f1,C,A,B),B,duty_rem). [resolve(33,a,32,a)]. % 0.75/1.03 34 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | power(f5(f1,A,B,C,D,E)). [resolve(18,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | power(f5(f1,A,B,C,D,E)). [resolve(34,a,32,a)]. % 0.75/1.03 35 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | subjection(f6(f1,A,B,C,D,E)). [resolve(19,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | subjection(f6(f1,A,B,C,D,E)). [resolve(35,a,32,a)]. % 0.75/1.03 36 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f5(f1,A,B,C,D,E),B). [resolve(22,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f5(f1,A,B,C,D,E),B). [resolve(36,a,32,a)]. % 0.75/1.03 37 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f6(f1,A,B,C,D,E),A). [resolve(23,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f6(f1,A,B,C,D,E),A). [resolve(37,a,32,a)]. % 0.75/1.03 38 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | founds_rem(E,f4(f1,A,B,C,D,E),f1). [resolve(24,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | founds_rem(E,f4(f1,A,B,C,D,E),f1). [resolve(38,a,32,a)]. % 0.75/1.03 39 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f5(f1,A,B,C,D,E),decl(C),D). [resolve(25,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f5(f1,A,B,C,D,E),decl(C),D). [resolve(39,a,32,a)]. % 0.75/1.03 40 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f6(f1,A,B,C,D,E),decl(C),D). [resolve(26,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f6(f1,A,B,C,D,E),decl(C),D). [resolve(40,a,32,a)]. % 0.75/1.03 41 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f5(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(29,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f5(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(41,a,32,a)]. % 0.75/1.03 42 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f6(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(30,a,11,a)]. % 0.75/1.03 Derived: -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f6(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(42,a,32,a)]. % 0.75/1.03 43 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | duty(f2(f1,A,B,C,D,E)). [resolve(12,a,11,a)]. % 0.75/1.03 44 aee(f1,marketplace) # label(aee_f1) # label(axiom). [assumption]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | duty(f2(f1,marketplace,A,B,C,D)). [resolve(43,a,44,a)]. % 0.75/1.03 45 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | right(f3(f1,A,B,C,D,E)). [resolve(13,a,11,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | right(f3(f1,marketplace,A,B,C,D)). [resolve(45,a,44,a)]. % 0.75/1.03 46 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f2(f1,A,B,C,D,E),A). [resolve(14,a,11,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f2(f1,marketplace,A,B,C,D),marketplace). [resolve(46,a,44,a)]. % 0.75/1.03 47 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f3(f1,A,B,C,D,E),B). [resolve(15,a,11,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f3(f1,marketplace,A,B,C,D),A). [resolve(47,a,44,a)]. % 0.75/1.03 48 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | founds(E,f1(f1,A,B,C,D,E),f1). [resolve(17,a,11,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | founds(D,f1(f1,marketplace,A,B,C,D),f1). [resolve(48,a,44,a)]. % 0.75/1.03 49 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f2(f1,A,B,C,D,E),rfr(C),D). [resolve(20,a,11,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f2(f1,marketplace,A,B,C,D),rfr(B),C). [resolve(49,a,44,a)]. % 0.75/1.03 50 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f3(f1,A,B,C,D,E),rfr(C),D). [resolve(21,a,11,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f3(f1,marketplace,A,B,C,D),rfr(B),C). [resolve(50,a,44,a)]. % 0.75/1.03 51 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f2(f1,A,B,C,D,E),f1(f1,A,B,C,D,E)). [resolve(27,a,11,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f2(f1,marketplace,A,B,C,D),f1(f1,marketplace,A,B,C,D)). [resolve(51,a,44,a)]. % 0.75/1.03 52 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f3(f1,A,B,C,D,E),f1(f1,A,B,C,D,E)). [resolve(28,a,11,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f3(f1,marketplace,A,B,C,D),f1(f1,marketplace,A,B,C,D)). [resolve(52,a,44,a)]. % 0.75/1.03 53 -act(f1,A) | -tgt(f1,B) | -aee(f1,C) | -does(C,A,B) | rem_act(f1,f12(f1,C,A,B)). [resolve(31,a,32,a)]. % 0.75/1.03 Derived: -act(f1,A) | -tgt(f1,B) | -does(marketplace,A,B) | rem_act(f1,f12(f1,marketplace,A,B)). [resolve(53,c,44,a)]. % 0.75/1.03 54 -act(f1,A) | -tgt(f1,B) | -aee(f1,C) | -does(C,A,B) | norm_state_change(C,f12(f1,C,A,B),B,duty_rem). [resolve(33,a,32,a)]. % 0.75/1.03 Derived: -act(f1,A) | -tgt(f1,B) | -does(marketplace,A,B) | norm_state_change(marketplace,f12(f1,marketplace,A,B),B,duty_rem). [resolve(54,c,44,a)]. % 0.75/1.03 55 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | power(f5(f1,A,B,C,D,E)). [resolve(34,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | power(f5(f1,marketplace,A,B,C,D)). [resolve(55,a,44,a)]. % 0.75/1.03 56 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | subjection(f6(f1,A,B,C,D,E)). [resolve(35,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | subjection(f6(f1,marketplace,A,B,C,D)). [resolve(56,a,44,a)]. % 0.75/1.03 57 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f5(f1,A,B,C,D,E),B). [resolve(36,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f5(f1,marketplace,A,B,C,D),A). [resolve(57,a,44,a)]. % 0.75/1.03 58 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f6(f1,A,B,C,D,E),A). [resolve(37,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f6(f1,marketplace,A,B,C,D),marketplace). [resolve(58,a,44,a)]. % 0.75/1.03 59 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | founds_rem(E,f4(f1,A,B,C,D,E),f1). [resolve(38,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | founds_rem(D,f4(f1,marketplace,A,B,C,D),f1). [resolve(59,a,44,a)]. % 0.75/1.03 60 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f5(f1,A,B,C,D,E),decl(C),D). [resolve(39,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f5(f1,marketplace,A,B,C,D),decl(B),C). [resolve(60,a,44,a)]. % 0.75/1.03 61 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f6(f1,A,B,C,D,E),decl(C),D). [resolve(40,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f6(f1,marketplace,A,B,C,D),decl(B),C). [resolve(61,a,44,a)]. % 0.75/1.03 62 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f5(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(41,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f5(f1,marketplace,A,B,C,D),f4(f1,marketplace,A,B,C,D)). [resolve(62,a,44,a)]. % 0.75/1.03 63 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f6(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(42,a,32,a)]. % 0.75/1.03 Derived: -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f6(f1,marketplace,A,B,C,D),f4(f1,marketplace,A,B,C,D)). [resolve(63,a,44,a)]. % 0.75/1.03 64 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | duty(f2(f1,marketplace,A,B,C,D)). [resolve(43,a,44,a)]. % 0.75/1.03 65 aer(f1,philharmonie) # label(aer_f1) # label(axiom). [assumption]. % 0.75/1.03 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | duty(f2(f1,marketplace,philharmonie,A,B,C)). [resolve(64,a,65,a)]. % 0.75/1.03 66 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | right(f3(f1,marketplace,A,B,C,D)). [resolve(45,a,44,a)]. % 0.75/1.03 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | right(f3(f1,marketplace,philharmonie,A,B,C)). [resolve(66,a,65,a)]. % 0.75/1.03 67 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f2(f1,marketplace,A,B,C,D),marketplace). [resolve(46,a,44,a)]. % 0.75/1.03 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f2(f1,marketplace,philharmonie,A,B,C),marketplace). [resolve(67,a,65,a)]. % 0.75/1.03 68 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f3(f1,marketplace,A,B,C,D),A). [resolve(47,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f3(f1,marketplace,philharmonie,A,B,C),philharmonie). [resolve(68,a,65,a)]. % 0.75/1.04 69 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | founds(D,f1(f1,marketplace,A,B,C,D),f1). [resolve(48,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | founds(C,f1(f1,marketplace,philharmonie,A,B,C),f1). [resolve(69,a,65,a)]. % 0.75/1.04 70 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f2(f1,marketplace,A,B,C,D),rfr(B),C). [resolve(49,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f2(f1,marketplace,philharmonie,A,B,C),rfr(A),B). [resolve(70,a,65,a)]. % 0.75/1.04 71 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f3(f1,marketplace,A,B,C,D),rfr(B),C). [resolve(50,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f3(f1,marketplace,philharmonie,A,B,C),rfr(A),B). [resolve(71,a,65,a)]. % 0.75/1.04 72 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f2(f1,marketplace,A,B,C,D),f1(f1,marketplace,A,B,C,D)). [resolve(51,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f2(f1,marketplace,philharmonie,A,B,C),f1(f1,marketplace,philharmonie,A,B,C)). [resolve(72,a,65,a)]. % 0.75/1.04 73 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f3(f1,marketplace,A,B,C,D),f1(f1,marketplace,A,B,C,D)). [resolve(52,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f3(f1,marketplace,philharmonie,A,B,C),f1(f1,marketplace,philharmonie,A,B,C)). [resolve(73,a,65,a)]. % 0.75/1.04 74 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | power(f5(f1,marketplace,A,B,C,D)). [resolve(55,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | power(f5(f1,marketplace,philharmonie,A,B,C)). [resolve(74,a,65,a)]. % 0.75/1.04 75 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | subjection(f6(f1,marketplace,A,B,C,D)). [resolve(56,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | subjection(f6(f1,marketplace,philharmonie,A,B,C)). [resolve(75,a,65,a)]. % 0.75/1.04 76 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f5(f1,marketplace,A,B,C,D),A). [resolve(57,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f5(f1,marketplace,philharmonie,A,B,C),philharmonie). [resolve(76,a,65,a)]. % 0.75/1.04 77 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f6(f1,marketplace,A,B,C,D),marketplace). [resolve(58,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f6(f1,marketplace,philharmonie,A,B,C),marketplace). [resolve(77,a,65,a)]. % 0.75/1.04 78 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | founds_rem(D,f4(f1,marketplace,A,B,C,D),f1). [resolve(59,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | founds_rem(C,f4(f1,marketplace,philharmonie,A,B,C),f1). [resolve(78,a,65,a)]. % 0.75/1.04 79 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f5(f1,marketplace,A,B,C,D),decl(B),C). [resolve(60,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f5(f1,marketplace,philharmonie,A,B,C),decl(A),B). [resolve(79,a,65,a)]. % 0.75/1.04 80 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f6(f1,marketplace,A,B,C,D),decl(B),C). [resolve(61,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f6(f1,marketplace,philharmonie,A,B,C),decl(A),B). [resolve(80,a,65,a)]. % 0.75/1.04 81 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f5(f1,marketplace,A,B,C,D),f4(f1,marketplace,A,B,C,D)). [resolve(62,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f5(f1,marketplace,philharmonie,A,B,C),f4(f1,marketplace,philharmonie,A,B,C)). [resolve(81,a,65,a)]. % 0.75/1.04 82 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f6(f1,marketplace,A,B,C,D),f4(f1,marketplace,A,B,C,D)). [resolve(63,a,44,a)]. % 0.75/1.04 Derived: -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f6(f1,marketplace,philharmonie,A,B,C),f4(f1,marketplace,philharmonie,A,B,C)). [resolve(82,a,65,a)]. % 0.75/1.04 83 -act(f1,A) | -tgt(f1,B) | -does(marketplace,A,B) | rem_act(f1,f12(f1,marketplace,A,B)). [resolve(53,c,44,a)]. % 0.75/1.04 84 act(f1,distrib) # label(act_f1) # label(axiom). [assumption]. % 0.75/1.04 Derived: -tgt(f1,A) | -does(marketplace,distrib,A) | rem_act(f1,f12(f1,marketplace,distrib,A)). [resolve(83,a,84,a)]. % 0.75/1.04 85 -act(f1,A) | -tgt(f1,B) | -does(marketplace,A,B) | norm_state_change(marketplace,f12(f1,marketplace,A,B),B,duty_rem). [resolve(54,c,44,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -does(marketplace,distrib,A) | norm_state_change(marketplace,f12(f1,marketplace,distrib,A),A,duty_rem). [resolve(85,a,84,a)]. % 0.75/1.04 86 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | duty(f2(f1,marketplace,philharmonie,A,B,C)). [resolve(64,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | duty(f2(f1,marketplace,philharmonie,distrib,A,B)). [resolve(86,a,84,a)]. % 0.75/1.04 87 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | right(f3(f1,marketplace,philharmonie,A,B,C)). [resolve(66,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | right(f3(f1,marketplace,philharmonie,distrib,A,B)). [resolve(87,a,84,a)]. % 0.75/1.04 88 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f2(f1,marketplace,philharmonie,A,B,C),marketplace). [resolve(67,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | bearer(f2(f1,marketplace,philharmonie,distrib,A,B),marketplace). [resolve(88,a,84,a)]. % 0.75/1.04 89 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f3(f1,marketplace,philharmonie,A,B,C),philharmonie). [resolve(68,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | bearer(f3(f1,marketplace,philharmonie,distrib,A,B),philharmonie). [resolve(89,a,84,a)]. % 0.75/1.04 90 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | founds(C,f1(f1,marketplace,philharmonie,A,B,C),f1). [resolve(69,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | founds(B,f1(f1,marketplace,philharmonie,distrib,A,B),f1). [resolve(90,a,84,a)]. % 0.75/1.04 91 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f2(f1,marketplace,philharmonie,A,B,C),rfr(A),B). [resolve(70,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | cnt(f2(f1,marketplace,philharmonie,distrib,A,B),rfr(distrib),A). [resolve(91,a,84,a)]. % 0.75/1.04 92 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f3(f1,marketplace,philharmonie,A,B,C),rfr(A),B). [resolve(71,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | cnt(f3(f1,marketplace,philharmonie,distrib,A,B),rfr(distrib),A). [resolve(92,a,84,a)]. % 0.75/1.04 93 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f2(f1,marketplace,philharmonie,A,B,C),f1(f1,marketplace,philharmonie,A,B,C)). [resolve(72,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | part_of(f2(f1,marketplace,philharmonie,distrib,A,B),f1(f1,marketplace,philharmonie,distrib,A,B)). [resolve(93,a,84,a)]. % 0.75/1.04 94 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f3(f1,marketplace,philharmonie,A,B,C),f1(f1,marketplace,philharmonie,A,B,C)). [resolve(73,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | part_of(f3(f1,marketplace,philharmonie,distrib,A,B),f1(f1,marketplace,philharmonie,distrib,A,B)). [resolve(94,a,84,a)]. % 0.75/1.04 95 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | power(f5(f1,marketplace,philharmonie,A,B,C)). [resolve(74,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | power(f5(f1,marketplace,philharmonie,distrib,A,B)). [resolve(95,a,84,a)]. % 0.75/1.04 96 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | subjection(f6(f1,marketplace,philharmonie,A,B,C)). [resolve(75,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | subjection(f6(f1,marketplace,philharmonie,distrib,A,B)). [resolve(96,a,84,a)]. % 0.75/1.04 97 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f5(f1,marketplace,philharmonie,A,B,C),philharmonie). [resolve(76,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | bearer(f5(f1,marketplace,philharmonie,distrib,A,B),philharmonie). [resolve(97,a,84,a)]. % 0.75/1.04 98 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f6(f1,marketplace,philharmonie,A,B,C),marketplace). [resolve(77,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | bearer(f6(f1,marketplace,philharmonie,distrib,A,B),marketplace). [resolve(98,a,84,a)]. % 0.75/1.04 99 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | founds_rem(C,f4(f1,marketplace,philharmonie,A,B,C),f1). [resolve(78,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | founds_rem(B,f4(f1,marketplace,philharmonie,distrib,A,B),f1). [resolve(99,a,84,a)]. % 0.75/1.04 100 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f5(f1,marketplace,philharmonie,A,B,C),decl(A),B). [resolve(79,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | cnt(f5(f1,marketplace,philharmonie,distrib,A,B),decl(distrib),A). [resolve(100,a,84,a)]. % 0.75/1.04 101 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f6(f1,marketplace,philharmonie,A,B,C),decl(A),B). [resolve(80,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | cnt(f6(f1,marketplace,philharmonie,distrib,A,B),decl(distrib),A). [resolve(101,a,84,a)]. % 0.75/1.04 102 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f5(f1,marketplace,philharmonie,A,B,C),f4(f1,marketplace,philharmonie,A,B,C)). [resolve(81,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | part_of(f5(f1,marketplace,philharmonie,distrib,A,B),f4(f1,marketplace,philharmonie,distrib,A,B)). [resolve(102,a,84,a)]. % 0.75/1.04 103 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f6(f1,marketplace,philharmonie,A,B,C),f4(f1,marketplace,philharmonie,A,B,C)). [resolve(82,a,65,a)]. % 0.75/1.04 Derived: -tgt(f1,A) | -activates(B,f1) | part_of(f6(f1,marketplace,philharmonie,distrib,A,B),f4(f1,marketplace,philharmonie,distrib,A,B)). [resolve(103,a,84,a)]. % 0.75/1.04 104 -tgt(f1,A) | -does(marketplace,distrib,A) | rem_act(f1,f12(f1,marketplace,distrib,A)). [resolve(83,a,84,a)]. % 0.75/1.04 105 tgt(f1,concert_ds) # label(tgt_f1) # label(axiom). [assumption]. % 0.75/1.04 Derived: -does(marketplace,distrib,concert_ds) | rem_act(f1,f12(f1,marketplace,distrib,concert_ds)). [resolve(104,a,105,a)]. % 0.75/1.04 106 -tgt(f1,A) | -does(marketplace,distrib,A) | norm_state_change(marketplace,f12(f1,marketplace,distrib,A),A,duty_rem). [resolve(85,a,84,a)]. % 0.75/1.04 Derived: -does(marketplace,distrib,concert_ds) | norm_state_change(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem). [resolve(106,a,105,a)]. % 0.75/1.04 107 -tgt(f1,A) | -activates(B,f1) | duty(f2(f1,marketplace,philharmonie,distrib,A,B)). [resolve(86,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | duty(f2(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(107,a,105,a)]. % 0.75/1.04 108 -tgt(f1,A) | -activates(B,f1) | right(f3(f1,marketplace,philharmonie,distrib,A,B)). [resolve(87,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | right(f3(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(108,a,105,a)]. % 0.75/1.04 109 -tgt(f1,A) | -activates(B,f1) | bearer(f2(f1,marketplace,philharmonie,distrib,A,B),marketplace). [resolve(88,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | bearer(f2(f1,marketplace,philharmonie,distrib,concert_ds,A),marketplace). [resolve(109,a,105,a)]. % 0.75/1.04 110 -tgt(f1,A) | -activates(B,f1) | bearer(f3(f1,marketplace,philharmonie,distrib,A,B),philharmonie). [resolve(89,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | bearer(f3(f1,marketplace,philharmonie,distrib,concert_ds,A),philharmonie). [resolve(110,a,105,a)]. % 0.75/1.04 111 -tgt(f1,A) | -activates(B,f1) | founds(B,f1(f1,marketplace,philharmonie,distrib,A,B),f1). [resolve(90,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | founds(A,f1(f1,marketplace,philharmonie,distrib,concert_ds,A),f1). [resolve(111,a,105,a)]. % 0.75/1.04 112 -tgt(f1,A) | -activates(B,f1) | cnt(f2(f1,marketplace,philharmonie,distrib,A,B),rfr(distrib),A). [resolve(91,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | cnt(f2(f1,marketplace,philharmonie,distrib,concert_ds,A),rfr(distrib),concert_ds). [resolve(112,a,105,a)]. % 0.75/1.04 113 -tgt(f1,A) | -activates(B,f1) | cnt(f3(f1,marketplace,philharmonie,distrib,A,B),rfr(distrib),A). [resolve(92,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | cnt(f3(f1,marketplace,philharmonie,distrib,concert_ds,A),rfr(distrib),concert_ds). [resolve(113,a,105,a)]. % 0.75/1.04 114 -tgt(f1,A) | -activates(B,f1) | part_of(f2(f1,marketplace,philharmonie,distrib,A,B),f1(f1,marketplace,philharmonie,distrib,A,B)). [resolve(93,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | part_of(f2(f1,marketplace,philharmonie,distrib,concert_ds,A),f1(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(114,a,105,a)]. % 0.75/1.04 115 -tgt(f1,A) | -activates(B,f1) | part_of(f3(f1,marketplace,philharmonie,distrib,A,B),f1(f1,marketplace,philharmonie,distrib,A,B)). [resolve(94,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | part_of(f3(f1,marketplace,philharmonie,distrib,concert_ds,A),f1(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(115,a,105,a)]. % 0.75/1.04 116 -tgt(f1,A) | -activates(B,f1) | power(f5(f1,marketplace,philharmonie,distrib,A,B)). [resolve(95,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | power(f5(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(116,a,105,a)]. % 0.75/1.04 117 -tgt(f1,A) | -activates(B,f1) | subjection(f6(f1,marketplace,philharmonie,distrib,A,B)). [resolve(96,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | subjection(f6(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(117,a,105,a)]. % 0.75/1.04 118 -tgt(f1,A) | -activates(B,f1) | bearer(f5(f1,marketplace,philharmonie,distrib,A,B),philharmonie). [resolve(97,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),philharmonie). [resolve(118,a,105,a)]. % 0.75/1.04 119 -tgt(f1,A) | -activates(B,f1) | bearer(f6(f1,marketplace,philharmonie,distrib,A,B),marketplace). [resolve(98,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | bearer(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),marketplace). [resolve(119,a,105,a)]. % 0.75/1.04 120 -tgt(f1,A) | -activates(B,f1) | founds_rem(B,f4(f1,marketplace,philharmonie,distrib,A,B),f1). [resolve(99,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | founds_rem(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,A),f1). [resolve(120,a,105,a)]. % 0.75/1.04 121 -tgt(f1,A) | -activates(B,f1) | cnt(f5(f1,marketplace,philharmonie,distrib,A,B),decl(distrib),A). [resolve(100,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),decl(distrib),concert_ds). [resolve(121,a,105,a)]. % 0.75/1.04 122 -tgt(f1,A) | -activates(B,f1) | cnt(f6(f1,marketplace,philharmonie,distrib,A,B),decl(distrib),A). [resolve(101,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),decl(distrib),concert_ds). [resolve(122,a,105,a)]. % 0.75/1.04 123 -tgt(f1,A) | -activates(B,f1) | part_of(f5(f1,marketplace,philharmonie,distrib,A,B),f4(f1,marketplace,philharmonie,distrib,A,B)). [resolve(102,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),f4(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(123,a,105,a)]. % 0.75/1.04 124 -tgt(f1,A) | -activates(B,f1) | part_of(f6(f1,marketplace,philharmonie,distrib,A,B),f4(f1,marketplace,philharmonie,distrib,A,B)). [resolve(103,a,84,a)]. % 0.75/1.04 Derived: -activates(A,f1) | part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),f4(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(124,a,105,a)]. % 0.75/1.04 125 -activates(A,f1) | duty(f2(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(107,a,105,a)]. % 0.75/1.04 126 activates(e1,f1) # label(act_e1_f1) # label(axiom). [assumption]. % 0.75/1.04 Derived: duty(f2(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(125,a,126,a)]. % 0.75/1.04 127 -activates(A,f1) | right(f3(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(108,a,105,a)]. % 0.75/1.04 Derived: right(f3(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(127,a,126,a)]. % 0.75/1.04 128 -activates(A,f1) | bearer(f2(f1,marketplace,philharmonie,distrib,concert_ds,A),marketplace). [resolve(109,a,105,a)]. % 0.75/1.04 Derived: bearer(f2(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace). [resolve(128,a,126,a)]. % 0.75/1.04 129 -activates(A,f1) | bearer(f3(f1,marketplace,philharmonie,distrib,concert_ds,A),philharmonie). [resolve(110,a,105,a)]. % 0.75/1.04 Derived: bearer(f3(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie). [resolve(129,a,126,a)]. % 0.75/1.04 130 -activates(A,f1) | founds(A,f1(f1,marketplace,philharmonie,distrib,concert_ds,A),f1). [resolve(111,a,105,a)]. % 0.75/1.04 Derived: founds(e1,f1(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1). [resolve(130,a,126,a)]. % 0.75/1.04 131 -activates(A,f1) | cnt(f2(f1,marketplace,philharmonie,distrib,concert_ds,A),rfr(distrib),concert_ds). [resolve(112,a,105,a)]. % 0.75/1.04 Derived: cnt(f2(f1,marketplace,philharmonie,distrib,concert_ds,e1),rfr(distrib),concert_ds). [resolve(131,a,126,a)]. % 0.75/1.04 132 -activates(A,f1) | cnt(f3(f1,marketplace,philharmonie,distrib,concert_ds,A),rfr(distrib),concert_ds). [resolve(113,a,105,a)]. % 0.75/1.04 Derived: cnt(f3(f1,marketplace,philharmonie,distrib,concert_ds,e1),rfr(distrib),concert_ds). [resolve(132,a,126,a)]. % 0.75/1.04 133 -activates(A,f1) | part_of(f2(f1,marketplace,philharmonie,distrib,concert_ds,A),f1(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(114,a,105,a)]. % 0.75/1.04 Derived: part_of(f2(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(133,a,126,a)]. % 0.75/1.04 134 -activates(A,f1) | part_of(f3(f1,marketplace,philharmonie,distrib,concert_ds,A),f1(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(115,a,105,a)]. % 0.75/1.04 Derived: part_of(f3(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(134,a,126,a)]. % 0.75/1.04 135 -activates(A,f1) | power(f5(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(116,a,105,a)]. % 0.75/1.04 Derived: power(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(135,a,126,a)]. % 0.75/1.04 136 -activates(A,f1) | subjection(f6(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(117,a,105,a)]. % 0.75/1.04 Derived: subjection(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(136,a,126,a)]. % 0.75/1.04 137 -activates(A,f1) | bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),philharmonie). [resolve(118,a,105,a)]. % 0.75/1.04 Derived: bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie). [resolve(137,a,126,a)]. % 0.75/1.04 138 -activates(A,f1) | bearer(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),marketplace). [resolve(119,a,105,a)]. % 0.75/1.04 Derived: bearer(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace). [resolve(138,a,126,a)]. % 0.75/1.04 139 -activates(A,f1) | founds_rem(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,A),f1). [resolve(120,a,105,a)]. % 0.75/1.04 Derived: founds_rem(e1,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1). [resolve(139,a,126,a)]. % 0.75/1.04 140 -activates(A,f1) | cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),decl(distrib),concert_ds). [resolve(121,a,105,a)]. % 0.75/1.04 Derived: cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds). [resolve(140,a,126,a)]. % 0.75/1.04 141 -activates(A,f1) | cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),decl(distrib),concert_ds). [resolve(122,a,105,a)]. % 0.75/1.04 Derived: cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds). [resolve(141,a,126,a)]. % 0.75/1.04 142 -activates(A,f1) | part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),f4(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(123,a,105,a)]. % 0.75/1.04 Derived: part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(142,a,126,a)]. % 0.75/1.04 143 -activates(A,f1) | part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),f4(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(124,a,105,a)]. % 0.75/1.04 Derived: part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(143,a,126,a)]. % 0.75/1.04 144 -does(marketplace,distrib,concert_ds) | rem_act(f1,f12(f1,marketplace,distrib,concert_ds)). [resolve(104,a,105,a)]. % 0.75/1.04 145 does(marketplace,distrib,concert_ds) # label(marketplace_does) # label(axiom). [assumption]. % 0.75/1.04 Derived: rem_act(f1,f12(f1,marketplace,distrib,concert_ds)). [resolve(144,a,145,a)]. % 0.75/1.04 146 -does(marketplace,distrib,concert_ds) | norm_state_change(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem). [resolve(106,a,105,a)]. % 0.75/1.04 Derived: norm_state_change(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem). [resolve(146,a,145,a)]. % 0.75/1.04 147 founds_rem(e1,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1). [resolve(139,a,126,a)]. % 0.75/1.04 148 -founds_rem(e1,A,f1) | -power(B) | -bearer(B,philharmonie) | -cnt(B,decl(distrib),concert_ds) | -part_of(B,A) | -about_event(B,e1) | -subjection(C) | -bearer(C,marketplace) | -cnt(C,decl(distrib),concert_ds) | -part_of(C,A) | -about_event(C,e1) # label(conjecture) # label(negated_conjecture). [clausify(9)]. % 0.75/1.04 149 -power(A) | -cnt(A,decl(B),C) | -part_of(A,D) | -founds_rem(E,D,F) | about_event(A,E) # label(ax_B2) # label(axiom). [clausify(7)]. % 0.75/1.04 150 -subjection(A) | -cnt(A,decl(B),C) | -part_of(A,D) | -founds_rem(E,D,F) | about_event(A,E) # label(ax_B3) # label(axiom). [clausify(8)]. % 0.75/1.04 Derived: -power(A) | -bearer(A,philharmonie) | -cnt(A,decl(distrib),concert_ds) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(A,e1) | -subjection(B) | -bearer(B,marketplace) | -cnt(B,decl(distrib),concert_ds) | -part_of(B,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(B,e1). [resolve(147,a,148,a)]. % 0.75/1.04 Derived: -power(A) | -cnt(A,decl(B),C) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(A,e1). [resolve(147,a,149,d)]. % 0.75/1.04 Derived: -subjection(A) | -cnt(A,decl(B),C) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(A,e1). [resolve(147,a,150,d)]. % 0.75/1.04 151 -norm_state_change(A,B,C,D) | inst_event(f7(A,B,C,D)) # label(ax_A1) # label(axiom). [clausify(3)]. % 0.75/1.04 152 -inst_event(A) | competent_for(f8(A),A) # label(ax_A2) # label(axiom). [clausify(4)]. % 0.75/1.04 Derived: -norm_state_change(A,B,C,D) | competent_for(f8(f7(A,B,C,D)),f7(A,B,C,D)). [resolve(151,b,152,a)]. % 0.75/1.04 153 -norm_state_change(A,B,C,D) | competent_for(f8(f7(A,B,C,D)),f7(A,B,C,D)). [resolve(151,b,152,a)]. % 0.75/1.04 154 -competent_for(A,B) | power(f9(A,B)) # label(ax_A3) # label(axiom). [clausify(5)]. % 0.75/1.04 155 -competent_for(A,B) | subjection(f10(A,B)) # label(ax_A3) # label(axiom). [clausify(5)]. % 0.75/1.04 156 -competent_for(A,B) | bearer(f9(A,B),A) # label(ax_A3) # label(axiom). [clausify(5)]. % 0.75/1.04 157 -competent_for(A,B) | about_event(f9(A,B),B) # label(ax_A3) # label(axiom). [clausify(5)]. % 0.75/1.04 158 -competent_for(A,B) | about_event(f10(A,B),B) # label(ax_A3) # label(axiom). [clausify(5)]. % 0.75/1.04 159 -competent_for(A,B) | bearer(f10(A,B),f11(A,B)) # label(ax_A3) # label(axiom). [clausify(5)]. % 0.75/1.04 Derived: -norm_state_change(A,B,C,D) | power(f9(f8(f7(A,B,C,D)),f7(A,B,C,D))). [resolve(153,b,154,a)]. % 0.75/1.04 Derived: -norm_state_change(A,B,C,D) | subjection(f10(f8(f7(A,B,C,D)),f7(A,B,C,D))). [resolve(153,b,155,a)]. % 0.75/1.04 Derived: -norm_state_change(A,B,C,D) | bearer(f9(f8(f7(A,B,C,D)),f7(A,B,C,D)),f8(f7(A,B,C,D))). [resolve(153,b,156,a)]. % 0.75/1.04 Derived: -norm_state_change(A,B,C,D) | about_event(f9(f8(f7(A,B,C,D)),f7(A,B,C,D)),f7(A,B,C,D)). [resolve(153,b,157,a)]. % 0.75/1.04 Derived: -norm_state_change(A,B,C,D) | about_event(f10(f8(f7(A,B,C,D)),f7(A,B,C,D)),f7(A,B,C,D)). [resolve(153,b,158,a)]. % 0.75/1.04 Derived: -norm_state_change(A,B,C,D) | bearer(f10(f8(f7(A,B,C,D)),f7(A,B,C,D)),f11(f8(f7(A,B,C,D)),f7(A,B,C,D))). [resolve(153,b,159,a)]. % 0.75/1.04 160 norm_state_change(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem). [resolve(146,a,145,a)]. % 0.75/1.04 161 -norm_state_change(A,B,C,D) | triggers(f7(A,B,C,D),A,B,C,D) # label(ax_A1) # label(axiom). [clausify(3)]. % 0.75/1.04 Derived: triggers(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem),marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem). [resolve(160,a,161,a)]. % 0.75/1.04 162 -norm_state_change(A,B,C,D) | power(f9(f8(f7(A,B,C,D)),f7(A,B,C,D))). [resolve(153,b,154,a)]. % 0.75/1.04 Derived: power(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem))). [resolve(162,a,160,a)]. % 0.75/1.04 163 -norm_state_change(A,B,C,D) | subjection(f10(f8(f7(A,B,C,D)),f7(A,B,C,D))). [resolve(153,b,155,a)]. % 0.75/1.04 Derived: subjection(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem))). [resolve(163,a,160,a)]. % 0.75/1.04 164 -norm_state_change(A,B,C,D) | bearer(f9(f8(f7(A,B,C,D)),f7(A,B,C,D)),f8(f7(A,B,C,D))). [resolve(153,b,156,a)]. % 0.75/1.04 Derived: bearer(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem))). [resolve(164,a,160,a)]. % 0.75/1.04 165 -norm_state_change(A,B,C,D) | about_event(f9(f8(f7(A,B,C,D)),f7(A,B,C,D)),f7(A,B,C,D)). [resolve(153,b,157,a)]. % 0.75/1.04 Derived: about_event(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)). [resolve(165,a,160,a)]. % 0.75/1.04 166 -norm_state_change(A,B,C,D) | about_event(f10(f8(f7(A,B,C,D)),f7(A,B,C,D)),f7(A,B,C,D)). [resolve(153,b,158,a)]. % 0.75/1.04 Derived: about_event(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)). [resolve(166,a,160,a)]. % 0.75/1.04 167 -norm_state_change(A,B,C,D) | bearer(f10(f8(f7(A,B,C,D)),f7(A,B,C,D)),f11(f8(f7(A,B,C,D)),f7(A,B,C,D))). [resolve(153,b,159,a)]. % 0.75/1.04 Derived: bearer(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f11(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem))). [resolve(167,a,160,a)]. % 0.75/1.04 168 -power(A) | -bearer(A,philharmonie) | -cnt(A,decl(distrib),concert_ds) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(A,e1) | -subjection(B) | -bearer(B,marketplace) | -cnt(B,decl(distrib),concert_ds) | -part_of(B,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(B,e1). [resolve(147,a,148,a)]. % 0.75/1.04 169 power(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(135,a,126,a)]. % 0.75/1.04 Derived: -bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) | -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) | -subjection(A) | -bearer(A,marketplace) | -cnt(A,decl(distrib),concert_ds) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(A,e1). [resolve(168,a,169,a)]. % 0.75/1.04 170 -power(A) | -cnt(A,decl(B),C) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(A,e1). [resolve(147,a,149,d)]. % 0.75/1.04 Derived: -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) | -part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [resolve(170,a,169,a)]. % 0.75/1.04 171 power(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem))). [resolve(162,a,160,a)]. % 0.75/1.04 Derived: -bearer(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),philharmonie) | -cnt(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),decl(distrib),concert_ds) | -part_of(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),e1) | -subjection(A) | -bearer(A,marketplace) | -cnt(A,decl(distrib),concert_ds) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(A,e1). [resolve(171,a,168,a)]. % 0.75/1.04 Derived: -cnt(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),decl(A),B) | -part_of(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),e1). [resolve(171,a,170,a)]. % 0.75/1.04 172 -subjection(A) | -cnt(A,decl(B),C) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(A,e1). [resolve(147,a,150,d)]. % 0.75/1.04 173 subjection(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(136,a,126,a)]. % 0.75/1.04 Derived: -cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) | -part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [resolve(172,a,173,a)]. % 0.75/1.04 174 subjection(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem))). [resolve(163,a,160,a)]. % 0.75/1.04 Derived: -cnt(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),decl(A),B) | -part_of(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),e1). [resolve(174,a,172,a)]. % 0.75/1.04 175 -bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) | -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) | -subjection(A) | -bearer(A,marketplace) | -cnt(A,decl(distrib),concert_ds) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(A,e1). [resolve(168,a,169,a)]. % 0.75/1.04 Derived: -bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) | -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) | -bearer(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace) | -cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [resolve(175,e,173,a)]. % 0.75/1.04 Derived: -bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) | -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) | -bearer(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),marketplace) | -cnt(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),decl(distrib),concert_ds) | -part_of(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),e1). [resolve(175,e,174,a)]. % 0.75/1.04 176 -bearer(f9(f8(f7(marketplace,f12(f1,mar % 0.75/1.04 WARNING: denials share constants (see output). % 0.75/1.04 % 0.75/1.04 ketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),philharmonie) | -cnt(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),decl(distrib),concert_ds) | -part_of(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),e1) | -subjection(A) | -bearer(A,marketplace) | -cnt(A,decl(distrib),concert_ds) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(A,e1). [resolve(171,a,168,a)]. % 0.75/1.04 Derived: -bearer(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),philharmonie) | -cnt(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),decl(distrib),concert_ds) | -part_of(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),e1) | -bearer(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace) | -cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [resolve(176,e,173,a)]. % 0.75/1.04 Derived: -bearer(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),philharmonie) | -cnt(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),decl(distrib),concert_ds) | -part_of(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f9(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),e1) | -bearer(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),marketplace) | -cnt(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),decl(distrib),concert_ds) | -part_of(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f10(f8(f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),f7(marketplace,f12(f1,marketplace,distrib,concert_ds),concert_ds,duty_rem)),e1). [resolve(176,e,174,a)]. % 0.75/1.04 % 0.75/1.04 ============================== end predicate elimination ============= % 0.75/1.04 % 0.75/1.04 Auto_denials: % 0.75/1.04 % assign(max_proofs, 4). % (Horn set with more than one neg. clause) % 0.75/1.04 % 0.75/1.04 WARNING, because some of the denials share constants, % 0.75/1.04 some of the denials or their descendents may be subsumed, % 0.75/1.04 preventing the target number of proofs from being found. % 0.75/1.04 The shared constants are: duty_rem, e1, concert_ds, distrib, philharmonie, marketplace, f1. % 0.75/1.04 % 0.75/1.05 Term ordering decisions: % 0.75/1.05 Function symbol KB weights: concert_ds=1. marketplace=1. distrib=1. f1=1. e1=1. philharmonie=1. duty_rem=1. f9=1. f10=1. f11=1. decl=1. rfr=1. f8=1. f7=1. f12=1. f1=1. f2=1. f3=1. f4=1. f5=1. f6=1. % 0.75/1.05 % 0.75/1.05 ============================== end of process initial clauses ======== % 0.75/1.05 % 0.75/1.05 ============================== CLAUSES FOR SEARCH ==================== % 0.75/1.05 % 0.75/1.05 ============================== end of clauses for search ============= % 0.75/1.05 % 0.75/1.05 ============================== SEARCH ================================ % 0.75/1.05 % 0.75/1.05 % Starting search at 0.03 seconds. % 0.75/1.05 % 0.75/1.05 ============================== PROOF ================================= % 0.75/1.05 % SZS status Theorem % 0.75/1.05 % SZS output start Refutation % 0.75/1.05 % 0.75/1.05 % Proof 1 at 0.03 (+ 0.00) seconds. % 0.75/1.05 % Length of proof is 100. % 0.75/1.05 % Level of proof is 15. % 0.75/1.05 % Maximum clause weight is 20.000. % 0.75/1.05 % Given clauses 17. % 0.75/1.05 % 0.75/1.05 2 (all F all X all Y all A all T all E (proh(F) & has_rem(F) & aee(F,X) & aer(F,Y) & act(F,A) & tgt(F,T) & activates(E,F) -> (exists RhoR exists Pw exists S (founds_rem(E,RhoR,F) & power(Pw) & bearer(Pw,Y) & cnt(Pw,decl(A),T) & part_of(Pw,RhoR) & subjection(S) & bearer(S,X) & cnt(S,decl(A),T) & part_of(S,RhoR))))) # label(ax_proh_relator_remedy) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 7 (all Pw all A all T all Rho all E all R (power(Pw) & cnt(Pw,decl(A),T) & part_of(Pw,Rho) & founds_rem(E,Rho,R) -> about_event(Pw,E))) # label(ax_B2) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 8 (all S all A all T all Rho all E all R (subjection(S) & cnt(S,decl(A),T) & part_of(S,Rho) & founds_rem(E,Rho,R) -> about_event(S,E))) # label(ax_B3) # label(axiom) # label(non_clause). [assumption]. % 0.75/1.05 9 -(exists RhoR exists Pw exists S (founds_rem(e1,RhoR,f1) & power(Pw) & bearer(Pw,philharmonie) & cnt(Pw,decl(distrib),concert_ds) & part_of(Pw,RhoR) & about_event(Pw,e1) & subjection(S) & bearer(S,marketplace) & cnt(S,decl(distrib),concert_ds) & part_of(S,RhoR) & about_event(S,e1))) # label(conjecture) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.75/1.05 11 proh(f1) # label(proh_f1) # label(axiom). [assumption]. % 0.75/1.05 18 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | power(f5(A,B,C,D,E,F)) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 19 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | subjection(f6(A,B,C,D,E,F)) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 22 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | bearer(f5(A,B,C,D,E,F),C) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 23 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | bearer(f6(A,B,C,D,E,F),B) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 24 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | founds_rem(F,f4(A,B,C,D,E,F),A) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 25 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f5(A,B,C,D,E,F),decl(D),E) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 26 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f6(A,B,C,D,E,F),decl(D),E) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 29 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | part_of(f5(A,B,C,D,E,F),f4(A,B,C,D,E,F)) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 30 -proh(A) | -has_rem(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | part_of(f6(A,B,C,D,E,F),f4(A,B,C,D,E,F)) # label(ax_proh_relator_remedy) # label(axiom). [clausify(2)]. % 0.75/1.05 32 has_rem(f1) # label(rem_f1) # label(axiom). [assumption]. % 0.75/1.05 34 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | power(f5(f1,A,B,C,D,E)). [resolve(18,a,11,a)]. % 0.75/1.05 35 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | subjection(f6(f1,A,B,C,D,E)). [resolve(19,a,11,a)]. % 0.75/1.05 36 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f5(f1,A,B,C,D,E),B). [resolve(22,a,11,a)]. % 0.75/1.05 37 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f6(f1,A,B,C,D,E),A). [resolve(23,a,11,a)]. % 0.75/1.05 38 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | founds_rem(E,f4(f1,A,B,C,D,E),f1). [resolve(24,a,11,a)]. % 0.75/1.05 39 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f5(f1,A,B,C,D,E),decl(C),D). [resolve(25,a,11,a)]. % 0.75/1.05 40 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f6(f1,A,B,C,D,E),decl(C),D). [resolve(26,a,11,a)]. % 0.75/1.05 41 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f5(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(29,a,11,a)]. % 0.75/1.05 42 -has_rem(f1) | -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f6(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(30,a,11,a)]. % 0.75/1.05 44 aee(f1,marketplace) # label(aee_f1) # label(axiom). [assumption]. % 0.75/1.05 55 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | power(f5(f1,A,B,C,D,E)). [resolve(34,a,32,a)]. % 0.75/1.05 56 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | subjection(f6(f1,A,B,C,D,E)). [resolve(35,a,32,a)]. % 0.75/1.05 57 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f5(f1,A,B,C,D,E),B). [resolve(36,a,32,a)]. % 0.75/1.05 58 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | bearer(f6(f1,A,B,C,D,E),A). [resolve(37,a,32,a)]. % 0.75/1.05 59 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | founds_rem(E,f4(f1,A,B,C,D,E),f1). [resolve(38,a,32,a)]. % 0.75/1.05 60 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f5(f1,A,B,C,D,E),decl(C),D). [resolve(39,a,32,a)]. % 0.75/1.05 61 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | cnt(f6(f1,A,B,C,D,E),decl(C),D). [resolve(40,a,32,a)]. % 0.75/1.05 62 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f5(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(41,a,32,a)]. % 0.75/1.05 63 -aee(f1,A) | -aer(f1,B) | -act(f1,C) | -tgt(f1,D) | -activates(E,f1) | part_of(f6(f1,A,B,C,D,E),f4(f1,A,B,C,D,E)). [resolve(42,a,32,a)]. % 0.75/1.05 65 aer(f1,philharmonie) # label(aer_f1) # label(axiom). [assumption]. % 0.75/1.05 74 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | power(f5(f1,marketplace,A,B,C,D)). [resolve(55,a,44,a)]. % 0.75/1.05 75 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | subjection(f6(f1,marketplace,A,B,C,D)). [resolve(56,a,44,a)]. % 0.75/1.05 76 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f5(f1,marketplace,A,B,C,D),A). [resolve(57,a,44,a)]. % 0.75/1.05 77 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | bearer(f6(f1,marketplace,A,B,C,D),marketplace). [resolve(58,a,44,a)]. % 0.75/1.05 78 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | founds_rem(D,f4(f1,marketplace,A,B,C,D),f1). [resolve(59,a,44,a)]. % 0.75/1.05 79 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f5(f1,marketplace,A,B,C,D),decl(B),C). [resolve(60,a,44,a)]. % 0.75/1.05 80 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | cnt(f6(f1,marketplace,A,B,C,D),decl(B),C). [resolve(61,a,44,a)]. % 0.75/1.05 81 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f5(f1,marketplace,A,B,C,D),f4(f1,marketplace,A,B,C,D)). [resolve(62,a,44,a)]. % 0.75/1.05 82 -aer(f1,A) | -act(f1,B) | -tgt(f1,C) | -activates(D,f1) | part_of(f6(f1,marketplace,A,B,C,D),f4(f1,marketplace,A,B,C,D)). [resolve(63,a,44,a)]. % 0.75/1.05 84 act(f1,distrib) # label(act_f1) # label(axiom). [assumption]. % 0.75/1.05 95 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | power(f5(f1,marketplace,philharmonie,A,B,C)). [resolve(74,a,65,a)]. % 0.75/1.05 96 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | subjection(f6(f1,marketplace,philharmonie,A,B,C)). [resolve(75,a,65,a)]. % 0.75/1.05 97 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f5(f1,marketplace,philharmonie,A,B,C),philharmonie). [resolve(76,a,65,a)]. % 0.75/1.05 98 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | bearer(f6(f1,marketplace,philharmonie,A,B,C),marketplace). [resolve(77,a,65,a)]. % 0.75/1.05 99 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | founds_rem(C,f4(f1,marketplace,philharmonie,A,B,C),f1). [resolve(78,a,65,a)]. % 0.75/1.05 100 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f5(f1,marketplace,philharmonie,A,B,C),decl(A),B). [resolve(79,a,65,a)]. % 0.75/1.05 101 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | cnt(f6(f1,marketplace,philharmonie,A,B,C),decl(A),B). [resolve(80,a,65,a)]. % 0.75/1.05 102 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f5(f1,marketplace,philharmonie,A,B,C),f4(f1,marketplace,philharmonie,A,B,C)). [resolve(81,a,65,a)]. % 0.75/1.05 103 -act(f1,A) | -tgt(f1,B) | -activates(C,f1) | part_of(f6(f1,marketplace,philharmonie,A,B,C),f4(f1,marketplace,philharmonie,A,B,C)). [resolve(82,a,65,a)]. % 0.75/1.05 105 tgt(f1,concert_ds) # label(tgt_f1) # label(axiom). [assumption]. % 0.75/1.05 116 -tgt(f1,A) | -activates(B,f1) | power(f5(f1,marketplace,philharmonie,distrib,A,B)). [resolve(95,a,84,a)]. % 0.75/1.05 117 -tgt(f1,A) | -activates(B,f1) | subjection(f6(f1,marketplace,philharmonie,distrib,A,B)). [resolve(96,a,84,a)]. % 0.75/1.05 118 -tgt(f1,A) | -activates(B,f1) | bearer(f5(f1,marketplace,philharmonie,distrib,A,B),philharmonie). [resolve(97,a,84,a)]. % 0.75/1.05 119 -tgt(f1,A) | -activates(B,f1) | bearer(f6(f1,marketplace,philharmonie,distrib,A,B),marketplace). [resolve(98,a,84,a)]. % 0.75/1.05 120 -tgt(f1,A) | -activates(B,f1) | founds_rem(B,f4(f1,marketplace,philharmonie,distrib,A,B),f1). [resolve(99,a,84,a)]. % 0.75/1.05 121 -tgt(f1,A) | -activates(B,f1) | cnt(f5(f1,marketplace,philharmonie,distrib,A,B),decl(distrib),A). [resolve(100,a,84,a)]. % 0.75/1.05 122 -tgt(f1,A) | -activates(B,f1) | cnt(f6(f1,marketplace,philharmonie,distrib,A,B),decl(distrib),A). [resolve(101,a,84,a)]. % 0.75/1.05 123 -tgt(f1,A) | -activates(B,f1) | part_of(f5(f1,marketplace,philharmonie,distrib,A,B),f4(f1,marketplace,philharmonie,distrib,A,B)). [resolve(102,a,84,a)]. % 0.75/1.05 124 -tgt(f1,A) | -activates(B,f1) | part_of(f6(f1,marketplace,philharmonie,distrib,A,B),f4(f1,marketplace,philharmonie,distrib,A,B)). [resolve(103,a,84,a)]. % 0.75/1.05 126 activates(e1,f1) # label(act_e1_f1) # label(axiom). [assumption]. % 0.75/1.05 135 -activates(A,f1) | power(f5(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(116,a,105,a)]. % 0.75/1.05 136 -activates(A,f1) | subjection(f6(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(117,a,105,a)]. % 0.75/1.05 137 -activates(A,f1) | bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),philharmonie). [resolve(118,a,105,a)]. % 0.75/1.05 138 -activates(A,f1) | bearer(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),marketplace). [resolve(119,a,105,a)]. % 0.75/1.05 139 -activates(A,f1) | founds_rem(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,A),f1). [resolve(120,a,105,a)]. % 0.75/1.05 140 -activates(A,f1) | cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),decl(distrib),concert_ds). [resolve(121,a,105,a)]. % 0.75/1.05 141 -activates(A,f1) | cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),decl(distrib),concert_ds). [resolve(122,a,105,a)]. % 0.75/1.05 142 -activates(A,f1) | part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,A),f4(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(123,a,105,a)]. % 0.75/1.05 143 -activates(A,f1) | part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,A),f4(f1,marketplace,philharmonie,distrib,concert_ds,A)). [resolve(124,a,105,a)]. % 0.75/1.05 147 founds_rem(e1,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1),f1). [resolve(139,a,126,a)]. % 0.75/1.05 148 -founds_rem(e1,A,f1) | -power(B) | -bearer(B,philharmonie) | -cnt(B,decl(distrib),concert_ds) | -part_of(B,A) | -about_event(B,e1) | -subjection(C) | -bearer(C,marketplace) | -cnt(C,decl(distrib),concert_ds) | -part_of(C,A) | -about_event(C,e1) # label(conjecture) # label(negated_conjecture). [clausify(9)]. % 0.75/1.05 149 -power(A) | -cnt(A,decl(B),C) | -part_of(A,D) | -founds_rem(E,D,F) | about_event(A,E) # label(ax_B2) # label(axiom). [clausify(7)]. % 0.75/1.05 150 -subjection(A) | -cnt(A,decl(B),C) | -part_of(A,D) | -founds_rem(E,D,F) | about_event(A,E) # label(ax_B3) # label(axiom). [clausify(8)]. % 0.75/1.05 168 -power(A) | -bearer(A,philharmonie) | -cnt(A,decl(distrib),concert_ds) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(A,e1) | -subjection(B) | -bearer(B,marketplace) | -cnt(B,decl(distrib),concert_ds) | -part_of(B,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(B,e1). [resolve(147,a,148,a)]. % 0.75/1.05 169 power(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(135,a,126,a)]. % 0.75/1.05 170 -power(A) | -cnt(A,decl(B),C) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(A,e1). [resolve(147,a,149,d)]. % 0.75/1.05 172 -subjection(A) | -cnt(A,decl(B),C) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(A,e1). [resolve(147,a,150,d)]. % 0.75/1.05 173 subjection(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(136,a,126,a)]. % 0.75/1.05 175 -bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) | -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) | -subjection(A) | -bearer(A,marketplace) | -cnt(A,decl(distrib),concert_ds) | -part_of(A,f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(A,e1). [resolve(168,a,169,a)]. % 0.75/1.05 183 bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie). [resolve(137,a,126,a)]. % 0.75/1.05 184 bearer(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace). [resolve(138,a,126,a)]. % 0.75/1.05 185 cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds). [resolve(140,a,126,a)]. % 0.75/1.05 186 cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds). [resolve(141,a,126,a)]. % 0.75/1.05 187 part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(142,a,126,a)]. % 0.75/1.05 188 part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)). [resolve(143,a,126,a)]. % 0.75/1.05 193 -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) | -part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [resolve(170,a,169,a)]. % 0.75/1.05 194 -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) | about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [copy(193),unit_del(b,187)]. % 0.75/1.05 196 -cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) | -part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | about_event(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [resolve(172,a,173,a)]. % 0.75/1.05 197 -cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B) | about_event(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [copy(196),unit_del(b,188)]. % 0.75/1.05 199 -bearer(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),philharmonie) | -cnt(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) | -bearer(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),marketplace) | -cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(distrib),concert_ds) | -part_of(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),f4(f1,marketplace,philharmonie,distrib,concert_ds,e1)) | -about_event(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [resolve(175,e,173,a)]. % 0.75/1.05 200 -about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1) | -about_event(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [copy(199),unit_del(a,183),unit_del(b,185),unit_del(c,187),unit_del(e,184),unit_del(f,186),unit_del(g,188)]. % 0.75/1.05 206 about_event(f5(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [ur(194,a,185,a)]. % 0.75/1.05 208 -about_event(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),e1). [back_unit_del(200),unit_del(a,206)]. % 0.75/1.05 209 -cnt(f6(f1,marketplace,philharmonie,distrib,concert_ds,e1),decl(A),B). [back_unit_del(197),unit_del(b,208)]. % 0.75/1.05 210 $F. [resolve(209,a,186,a)]. % 0.75/1.05 % 0.75/1.05 % SZS output end Refutation % 0.75/1.05 ============================== end of proof ========================== % 0.75/1.05 % 0.75/1.05 % Disable descendants (x means already disabled): % 0.75/1.05 148x 168x 175x 176x 199x 200x 201x 202x 203x 204x % 0.75/1.05 205x 207 208 209 % 0.75/1.05 % 0.75/1.05 ============================== STATISTICS ============================ % 0.75/1.05 % 0.75/1.05 Given=20. Generated=28. Kept=28. proofs=1. % 0.75/1.05 Usable=19. Sos=0. Demods=0. Limbo=0, Disabled=211. Hints=0. % 0.75/1.05 Megabytes=0.28. % 0.75/1.05 User_CPU=0.03, System_CPU=0.00, Wall_clock=0. % 0.75/1.05 % 0.75/1.05 ============================== end of statistics ===================== % 0.75/1.05 % 0.75/1.05 ============================== end of search ========================= % 0.75/1.05 % 0.75/1.05 SEARCH FAILED % 0.75/1.05 % 0.75/1.05 Exiting with 1 proof. % 0.75/1.05 % 0.75/1.05 Process 29303 exit (sos_empty) Tue Apr 28 19:30:50 2026 % 0.75/1.05 Prover9 interrupted %------------------------------------------------------------------------------