%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : MGT117+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:31 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 : MGT117+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.16/0.33 % Computer : n022.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue Apr 28 19:33:05 EDT 2026 % 0.16/0.33 % CPUTime : % 0.44/1.02 ============================== Prover9 =============================== % 0.44/1.02 Prover9 (32) version 2009-11A, November 2009. % 0.44/1.02 Process 25261 was started by sandbox2 on n022.cluster.edu, % 0.44/1.02 Tue Apr 28 19:33:06 2026 % 0.44/1.02 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_25108_n022.cluster.edu". % 0.44/1.02 ============================== end of head =========================== % 0.44/1.02 % 0.44/1.02 ============================== INPUT ================================= % 0.44/1.02 % 0.44/1.02 % Reading from file /tmp/Prover9_25108_n022.cluster.edu % 0.44/1.02 % 0.44/1.02 set(prolog_style_variables). % 0.44/1.02 set(auto2). % 0.44/1.02 % set(auto2) -> set(auto). % 0.44/1.02 % set(auto) -> set(auto_inference). % 0.44/1.02 % set(auto) -> set(auto_setup). % 0.44/1.02 % set(auto_setup) -> set(predicate_elim). % 0.44/1.02 % set(auto_setup) -> assign(eq_defs, unfold). % 0.44/1.02 % set(auto) -> set(auto_limits). % 0.44/1.02 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.44/1.02 % set(auto_limits) -> assign(sos_limit, 20000). % 0.44/1.02 % set(auto) -> set(auto_denials). % 0.44/1.02 % set(auto) -> set(auto_process). % 0.44/1.02 % set(auto2) -> assign(new_constants, 1). % 0.44/1.02 % set(auto2) -> assign(fold_denial_max, 3). % 0.44/1.02 % set(auto2) -> assign(max_weight, "200.000"). % 0.44/1.02 % set(auto2) -> assign(max_hours, 1). % 0.44/1.02 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.44/1.02 % set(auto2) -> assign(max_seconds, 0). % 0.44/1.02 % set(auto2) -> assign(max_minutes, 5). % 0.44/1.02 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.44/1.02 % set(auto2) -> set(sort_initial_sos). % 0.44/1.02 % set(auto2) -> assign(sos_limit, -1). % 0.44/1.02 % set(auto2) -> assign(lrs_ticks, 3000). % 0.44/1.02 % set(auto2) -> assign(max_megs, 400). % 0.44/1.02 % set(auto2) -> assign(stats, some). % 0.44/1.02 % set(auto2) -> clear(echo_input). % 0.44/1.02 % set(auto2) -> set(quiet). % 0.44/1.02 % set(auto2) -> clear(print_initial_clauses). % 0.44/1.02 % set(auto2) -> clear(print_given). % 0.44/1.02 assign(lrs_ticks,-1). % 0.44/1.02 assign(sos_limit,10000). % 0.44/1.02 assign(order,kbo). % 0.44/1.02 set(lex_order_vars). % 0.44/1.02 clear(print_given). % 0.44/1.02 % 0.44/1.02 % formulas(sos). % not echoed (15 formulas) % 0.44/1.02 % 0.44/1.02 ============================== end of input ========================== % 0.44/1.02 % 0.44/1.02 % From the command line: assign(max_seconds, 300). % 0.44/1.02 % 0.44/1.02 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.44/1.02 % 0.44/1.02 % Formulas that are not ordinary clauses: % 0.44/1.02 1 (all P all X all Y all A all T all E (perm(P) & strong(P) & aee(P,X) & aer(P,Y) & act(P,A) & tgt(P,T) & activates(E,P) -> (exists RhoI exists Im exists Db (founds_imm(E,RhoI,P) & immunity(Im) & bearer(Im,X) & cnt(Im,A,T) & part_of(Im,RhoI) & disability(Db) & bearer(Db,Y) & cnt(Db,A,T) & part_of(Db,RhoI))))) # label(ax_perm_relator_strong) # label(axiom) # label(non_clause). [assumption]. % 0.44/1.02 2 -(exists RhoI exists Db (founds_imm(e1,RhoI,p1) & disability(Db) & bearer(Db,museen) & cnt(Db,read,museum_api) & part_of(Db,RhoI))) # label(conjecture) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.44/1.02 % 0.44/1.02 ============================== end of process non-clausal formulas === % 0.44/1.02 % 0.44/1.02 ============================== PROCESS INITIAL CLAUSES =============== % 0.44/1.02 % 0.44/1.02 ============================== PREDICATE ELIMINATION ================= % 0.44/1.02 3 -perm(A) | -strong(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | immunity(f2(A,B,C,D,E,F)) # label(ax_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 4 perm(p1) # label(perm_p1) # label(axiom). [assumption]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | immunity(f2(p1,A,B,C,D,E)). [resolve(3,a,4,a)]. % 0.44/1.02 5 -perm(A) | -strong(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | disability(f3(A,B,C,D,E,F)) # label(ax_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | disability(f3(p1,A,B,C,D,E)). [resolve(5,a,4,a)]. % 0.44/1.02 6 -perm(A) | -strong(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_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f2(p1,A,B,C,D,E),A). [resolve(6,a,4,a)]. % 0.44/1.02 7 -perm(A) | -strong(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_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f3(p1,A,B,C,D,E),B). [resolve(7,a,4,a)]. % 0.44/1.02 8 -perm(A) | -strong(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | founds_imm(F,f1(A,B,C,D,E,F),A) # label(ax_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | founds_imm(E,f1(p1,A,B,C,D,E),p1). [resolve(8,a,4,a)]. % 0.44/1.02 9 -perm(A) | -strong(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f2(A,B,C,D,E,F),D,E) # label(ax_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f2(p1,A,B,C,D,E),C,D). [resolve(9,a,4,a)]. % 0.44/1.02 10 -perm(A) | -strong(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f3(A,B,C,D,E,F),D,E) # label(ax_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f3(p1,A,B,C,D,E),C,D). [resolve(10,a,4,a)]. % 0.44/1.02 11 -perm(A) | -strong(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_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f2(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(11,a,4,a)]. % 0.44/1.02 12 -perm(A) | -strong(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_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 Derived: -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f3(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(12,a,4,a)]. % 0.44/1.02 13 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | immunity(f2(p1,A,B,C,D,E)). [resolve(3,a,4,a)]. % 0.44/1.02 14 strong(p1) # label(strong_p1) # label(axiom). [assumption]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | immunity(f2(p1,A,B,C,D,E)). [resolve(13,a,14,a)]. % 0.44/1.02 15 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | disability(f3(p1,A,B,C,D,E)). [resolve(5,a,4,a)]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | disability(f3(p1,A,B,C,D,E)). [resolve(15,a,14,a)]. % 0.44/1.02 16 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f2(p1,A,B,C,D,E),A). [resolve(6,a,4,a)]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f2(p1,A,B,C,D,E),A). [resolve(16,a,14,a)]. % 0.44/1.02 17 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f3(p1,A,B,C,D,E),B). [resolve(7,a,4,a)]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f3(p1,A,B,C,D,E),B). [resolve(17,a,14,a)]. % 0.44/1.02 18 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | founds_imm(E,f1(p1,A,B,C,D,E),p1). [resolve(8,a,4,a)]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | founds_imm(E,f1(p1,A,B,C,D,E),p1). [resolve(18,a,14,a)]. % 0.44/1.02 19 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f2(p1,A,B,C,D,E),C,D). [resolve(9,a,4,a)]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f2(p1,A,B,C,D,E),C,D). [resolve(19,a,14,a)]. % 0.44/1.02 20 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f3(p1,A,B,C,D,E),C,D). [resolve(10,a,4,a)]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f3(p1,A,B,C,D,E),C,D). [resolve(20,a,14,a)]. % 0.44/1.02 21 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f2(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(11,a,4,a)]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f2(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(21,a,14,a)]. % 0.44/1.02 22 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f3(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(12,a,4,a)]. % 0.44/1.02 Derived: -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f3(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(22,a,14,a)]. % 0.44/1.02 23 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | immunity(f2(p1,A,B,C,D,E)). [resolve(13,a,14,a)]. % 0.44/1.02 24 aee(p1,bibliothek) # label(aee_p1) # label(axiom). [assumption]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | immunity(f2(p1,bibliothek,A,B,C,D)). [resolve(23,a,24,a)]. % 0.44/1.02 25 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | disability(f3(p1,A,B,C,D,E)). [resolve(15,a,14,a)]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | disability(f3(p1,bibliothek,A,B,C,D)). [resolve(25,a,24,a)]. % 0.44/1.02 26 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f2(p1,A,B,C,D,E),A). [resolve(16,a,14,a)]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | bearer(f2(p1,bibliothek,A,B,C,D),bibliothek). [resolve(26,a,24,a)]. % 0.44/1.02 27 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f3(p1,A,B,C,D,E),B). [resolve(17,a,14,a)]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | bearer(f3(p1,bibliothek,A,B,C,D),A). [resolve(27,a,24,a)]. % 0.44/1.02 28 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | founds_imm(E,f1(p1,A,B,C,D,E),p1). [resolve(18,a,14,a)]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | founds_imm(D,f1(p1,bibliothek,A,B,C,D),p1). [resolve(28,a,24,a)]. % 0.44/1.02 29 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f2(p1,A,B,C,D,E),C,D). [resolve(19,a,14,a)]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | cnt(f2(p1,bibliothek,A,B,C,D),B,C). [resolve(29,a,24,a)]. % 0.44/1.02 30 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f3(p1,A,B,C,D,E),C,D). [resolve(20,a,14,a)]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | cnt(f3(p1,bibliothek,A,B,C,D),B,C). [resolve(30,a,24,a)]. % 0.44/1.02 31 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f2(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(21,a,14,a)]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | part_of(f2(p1,bibliothek,A,B,C,D),f1(p1,bibliothek,A,B,C,D)). [resolve(31,a,24,a)]. % 0.44/1.02 32 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f3(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(22,a,14,a)]. % 0.44/1.02 Derived: -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | part_of(f3(p1,bibliothek,A,B,C,D),f1(p1,bibliothek,A,B,C,D)). [resolve(32,a,24,a)]. % 0.44/1.02 33 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | immunity(f2(p1,bibliothek,A,B,C,D)). [resolve(23,a,24,a)]. % 0.44/1.02 34 aer(p1,museen) # label(aer_p1) # label(axiom). [assumption]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | immunity(f2(p1,bibliothek,museen,A,B,C)). [resolve(33,a,34,a)]. % 0.44/1.02 35 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | disability(f3(p1,bibliothek,A,B,C,D)). [resolve(25,a,24,a)]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | disability(f3(p1,bibliothek,museen,A,B,C)). [resolve(35,a,34,a)]. % 0.44/1.02 36 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | bearer(f2(p1,bibliothek,A,B,C,D),bibliothek). [resolve(26,a,24,a)]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | bearer(f2(p1,bibliothek,museen,A,B,C),bibliothek). [resolve(36,a,34,a)]. % 0.44/1.02 37 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | bearer(f3(p1,bibliothek,A,B,C,D),A). [resolve(27,a,24,a)]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | bearer(f3(p1,bibliothek,museen,A,B,C),museen). [resolve(37,a,34,a)]. % 0.44/1.02 38 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | founds_imm(D,f1(p1,bibliothek,A,B,C,D),p1). [resolve(28,a,24,a)]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | founds_imm(C,f1(p1,bibliothek,museen,A,B,C),p1). [resolve(38,a,34,a)]. % 0.44/1.02 39 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | cnt(f2(p1,bibliothek,A,B,C,D),B,C). [resolve(29,a,24,a)]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | cnt(f2(p1,bibliothek,museen,A,B,C),A,B). [resolve(39,a,34,a)]. % 0.44/1.02 40 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | cnt(f3(p1,bibliothek,A,B,C,D),B,C). [resolve(30,a,24,a)]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | cnt(f3(p1,bibliothek,museen,A,B,C),A,B). [resolve(40,a,34,a)]. % 0.44/1.02 41 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | part_of(f2(p1,bibliothek,A,B,C,D),f1(p1,bibliothek,A,B,C,D)). [resolve(31,a,24,a)]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | part_of(f2(p1,bibliothek,museen,A,B,C),f1(p1,bibliothek,museen,A,B,C)). [resolve(41,a,34,a)]. % 0.44/1.02 42 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | part_of(f3(p1,bibliothek,A,B,C,D),f1(p1,bibliothek,A,B,C,D)). [resolve(32,a,24,a)]. % 0.44/1.02 Derived: -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | part_of(f3(p1,bibliothek,museen,A,B,C),f1(p1,bibliothek,museen,A,B,C)). [resolve(42,a,34,a)]. % 0.44/1.02 43 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | immunity(f2(p1,bibliothek,museen,A,B,C)). [resolve(33,a,34,a)]. % 0.44/1.02 44 act(p1,read) # label(act_p1) # label(axiom). [assumption]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | immunity(f2(p1,bibliothek,museen,read,A,B)). [resolve(43,a,44,a)]. % 0.44/1.02 45 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | disability(f3(p1,bibliothek,museen,A,B,C)). [resolve(35,a,34,a)]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | disability(f3(p1,bibliothek,museen,read,A,B)). [resolve(45,a,44,a)]. % 0.44/1.02 46 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | bearer(f2(p1,bibliothek,museen,A,B,C),bibliothek). [resolve(36,a,34,a)]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | bearer(f2(p1,bibliothek,museen,read,A,B),bibliothek). [resolve(46,a,44,a)]. % 0.44/1.02 47 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | bearer(f3(p1,bibliothek,museen,A,B,C),museen). [resolve(37,a,34,a)]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | bearer(f3(p1,bibliothek,museen,read,A,B),museen). [resolve(47,a,44,a)]. % 0.44/1.02 48 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | founds_imm(C,f1(p1,bibliothek,museen,A,B,C),p1). [resolve(38,a,34,a)]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | founds_imm(B,f1(p1,bibliothek,museen,read,A,B),p1). [resolve(48,a,44,a)]. % 0.44/1.02 49 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | cnt(f2(p1,bibliothek,museen,A,B,C),A,B). [resolve(39,a,34,a)]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | cnt(f2(p1,bibliothek,museen,read,A,B),read,A). [resolve(49,a,44,a)]. % 0.44/1.02 50 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | cnt(f3(p1,bibliothek,museen,A,B,C),A,B). [resolve(40,a,34,a)]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | cnt(f3(p1,bibliothek,museen,read,A,B),read,A). [resolve(50,a,44,a)]. % 0.44/1.02 51 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | part_of(f2(p1,bibliothek,museen,A,B,C),f1(p1,bibliothek,museen,A,B,C)). [resolve(41,a,34,a)]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | part_of(f2(p1,bibliothek,museen,read,A,B),f1(p1,bibliothek,museen,read,A,B)). [resolve(51,a,44,a)]. % 0.44/1.02 52 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | part_of(f3(p1,bibliothek,museen,A,B,C),f1(p1,bibliothek,museen,A,B,C)). [resolve(42,a,34,a)]. % 0.44/1.02 Derived: -tgt(p1,A) | -activates(B,p1) | part_of(f3(p1,bibliothek,museen,read,A,B),f1(p1,bibliothek,museen,read,A,B)). [resolve(52,a,44,a)]. % 0.44/1.02 53 -tgt(p1,A) | -activates(B,p1) | immunity(f2(p1,bibliothek,museen,read,A,B)). [resolve(43,a,44,a)]. % 0.44/1.02 54 tgt(p1,museum_api) # label(tgt_p1) # label(axiom). [assumption]. % 0.44/1.02 Derived: -activates(A,p1) | immunity(f2(p1,bibliothek,museen,read,museum_api,A)). [resolve(53,a,54,a)]. % 0.44/1.02 55 -tgt(p1,A) | -activates(B,p1) | disability(f3(p1,bibliothek,museen,read,A,B)). [resolve(45,a,44,a)]. % 0.44/1.02 Derived: -activates(A,p1) | disability(f3(p1,bibliothek,museen,read,museum_api,A)). [resolve(55,a,54,a)]. % 0.44/1.02 56 -tgt(p1,A) | -activates(B,p1) | bearer(f2(p1,bibliothek,museen,read,A,B),bibliothek). [resolve(46,a,44,a)]. % 0.44/1.02 Derived: -activates(A,p1) | bearer(f2(p1,bibliothek,museen,read,museum_api,A),bibliothek). [resolve(56,a,54,a)]. % 0.44/1.02 57 -tgt(p1,A) | -activates(B,p1) | bearer(f3(p1,bibliothek,museen,read,A,B),museen). [resolve(47,a,44,a)]. % 0.44/1.02 Derived: -activates(A,p1) | bearer(f3(p1,bibliothek,museen,read,museum_api,A),museen). [resolve(57,a,54,a)]. % 0.44/1.02 58 -tgt(p1,A) | -activates(B,p1) | founds_imm(B,f1(p1,bibliothek,museen,read,A,B),p1). [resolve(48,a,44,a)]. % 0.44/1.02 Derived: -activates(A,p1) | founds_imm(A,f1(p1,bibliothek,museen,read,museum_api,A),p1). [resolve(58,a,54,a)]. % 0.44/1.02 59 -tgt(p1,A) | -activates(B,p1) | cnt(f2(p1,bibliothek,museen,read,A,B),read,A). [resolve(49,a,44,a)]. % 0.44/1.02 Derived: -activates(A,p1) | cnt(f2(p1,bibliothek,museen,read,museum_api,A),read,museum_api). [resolve(59,a,54,a)]. % 0.44/1.02 60 -tgt(p1,A) | -activates(B,p1) | cnt(f3(p1,bibliothek,museen,read,A,B),read,A). [resolve(50,a,44,a)]. % 0.44/1.02 Derived: -activates(A,p1) | cnt(f3(p1,bibliothek,museen,read,museum_api,A),read,museum_api). [resolve(60,a,54,a)]. % 0.44/1.02 61 -tgt(p1,A) | -activates(B,p1) | part_of(f2(p1,bibliothek,museen,read,A,B),f1(p1,bibliothek,museen,read,A,B)). [resolve(51,a,44,a)]. % 0.44/1.02 Derived: -activates(A,p1) | part_of(f2(p1,bibliothek,museen,read,museum_api,A),f1(p1,bibliothek,museen,read,museum_api,A)). [resolve(61,a,54,a)]. % 0.44/1.02 62 -tgt(p1,A) | -activates(B,p1) | part_of(f3(p1,bibliothek,museen,read,A,B),f1(p1,bibliothek,museen,read,A,B)). [resolve(52,a,44,a)]. % 0.44/1.02 Derived: -activates(A,p1) | part_of(f3(p1,bibliothek,museen,read,museum_api,A),f1(p1,bibliothek,museen,read,museum_api,A)). [resolve(62,a,54,a)]. % 0.44/1.02 63 -activates(A,p1) | immunity(f2(p1,bibliothek,museen,read,museum_api,A)). [resolve(53,a,54,a)]. % 0.44/1.02 64 activates(e1,p1) # label(act_e1_p1) # label(axiom). [assumption]. % 0.44/1.02 Derived: immunity(f2(p1,bibliothek,museen,read,museum_api,e1)). [resolve(63,a,64,a)]. % 0.44/1.02 65 -activates(A,p1) | disability(f3(p1,bibliothek,museen,read,museum_api,A)). [resolve(55,a,54,a)]. % 0.44/1.02 Derived: disability(f3(p1,bibliothek,museen,read,museum_api,e1)). [resolve(65,a,64,a)]. % 0.44/1.02 66 -activates(A,p1) | bearer(f2(p1,bibliothek,museen,read,museum_api,A),bibliothek). [resolve(56,a,54,a)]. % 0.44/1.02 Derived: bearer(f2(p1,bibliothek,museen,read,museum_api,e1),bibliothek). [resolve(66,a,64,a)]. % 0.44/1.02 67 -activates(A,p1) | bearer(f3(p1,bibliothek,museen,read,museum_api,A),museen). [resolve(57,a,54,a)]. % 0.44/1.02 Derived: bearer(f3(p1,bibliothek,museen,read,museum_api,e1),museen). [resolve(67,a,64,a)]. % 0.44/1.02 68 -activates(A,p1) | founds_imm(A,f1(p1,bibliothek,museen,read,museum_api,A),p1). [resolve(58,a,54,a)]. % 0.44/1.02 Derived: founds_imm(e1,f1(p1,bibliothek,museen,read,museum_api,e1),p1). [resolve(68,a,64,a)]. % 0.44/1.02 69 -activates(A,p1) | cnt(f2(p1,bibliothek,museen,read,museum_api,A),read,museum_api). [resolve(59,a,54,a)]. % 0.44/1.02 Derived: cnt(f2(p1,bibliothek,museen,read,museum_api,e1),read,museum_api). [resolve(69,a,64,a)]. % 0.44/1.02 70 -activates(A,p1) | cnt(f3(p1,bibliothek,museen,read,museum_api,A),read,museum_api). [resolve(60,a,54,a)]. % 0.44/1.02 Derived: cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api). [resolve(70,a,64,a)]. % 0.44/1.02 71 -activates(A,p1) | part_of(f2(p1,bibliothek,museen,read,museum_api,A),f1(p1,bibliothek,museen,read,museum_api,A)). [resolve(61,a,54,a)]. % 0.44/1.02 Derived: part_of(f2(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(71,a,64,a)]. % 0.44/1.02 72 -activates(A,p1) | part_of(f3(p1,bibliothek,museen,read,museum_api,A),f1(p1,bibliothek,museen,read,museum_api,A)). [resolve(62,a,54,a)]. % 0.44/1.02 Derived: part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(72,a,64,a)]. % 0.44/1.02 73 founds_imm(e1,f1(p1,bibliothek,museen,read,museum_api,e1),p1). [resolve(68,a,64,a)]. % 0.44/1.02 74 -founds_imm(e1,A,p1) | -disability(B) | -bearer(B,museen) | -cnt(B,read,museum_api) | -part_of(B,A) # label(conjecture) # label(negated_conjecture). [clausify(2)]. % 0.44/1.02 Derived: -disability(A) | -bearer(A,museen) | -cnt(A,read,museum_api) | -part_of(A,f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(73,a,74,a)]. % 0.44/1.02 75 -disability(A) | -bearer(A,museen) | -cnt(A,read,museum_api) | -part_of(A,f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(73,a,74,a)]. % 0.44/1.02 76 disability(f3(p1,bibliothek,museen,read,museum_api,e1)). [resolve(65,a,64,a)]. % 0.44/1.02 Derived: -bearer(f3(p1,bibliothek,museen,read,museum_api,e1),museen) | -cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) | -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(75,a,76,a)]. % 0.44/1.02 77 -bearer(f3(p1,bibliothek,museen,read,museum_api,e1),museen) | -cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) | -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(75,a,76,a)]. % 0.44/1.02 78 bearer(f2(p1,bibliothek,museen,read,museum_api,e1),bibliothek). [resolve(66,a,64,a)]. % 0.44/1.02 79 bearer(f3(p1,bibliothek,museen,read,museum_api,e1),museen). [resolve(67,a,64,a)]. % 0.44/1.02 Derived: -cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) | -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(77,a,79,a)]. % 0.44/1.02 80 -cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) | -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(77,a,79,a)]. % 0.44/1.02 81 cnt(f2(p1,bibliothek,museen,read,museum_api,e1),read,museum_api). [resolve(69,a,64,a)]. % 0.44/1.02 82 cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api). [resolve(70,a,64,a)]. % 0.44/1.02 Derived: -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(80,a,82,a)]. % 0.44/1.02 83 -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(80,a,82,a)]. % 0.44/1.02 84 part_of(f2(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(71,a,64,a)]. % 0.44/1.02 85 part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(72,a,64,a)]. % 0.44/1.02 Derived: $F. [resolve(83,a,85,a)]. % 0.44/1.02 % 0.44/1.02 ============================== end predicate elimination ============= % 0.44/1.02 % 0.44/1.02 Auto_denials: (no changes). % 0.44/1.02 % 0.44/1.02 Term ordering decisions: % 0.44/1.02 Function symbol KB weights: % 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 55. % 0.44/1.02 % Level of proof is 13. % 0.44/1.02 % Maximum clause weight is 0.000. % 0.44/1.02 % Given clauses 0. % 0.44/1.02 % 0.44/1.02 1 (all P all X all Y all A all T all E (perm(P) & strong(P) & aee(P,X) & aer(P,Y) & act(P,A) & tgt(P,T) & activates(E,P) -> (exists RhoI exists Im exists Db (founds_imm(E,RhoI,P) & immunity(Im) & bearer(Im,X) & cnt(Im,A,T) & part_of(Im,RhoI) & disability(Db) & bearer(Db,Y) & cnt(Db,A,T) & part_of(Db,RhoI))))) # label(ax_perm_relator_strong) # label(axiom) # label(non_clause). [assumption]. % 0.44/1.02 2 -(exists RhoI exists Db (founds_imm(e1,RhoI,p1) & disability(Db) & bearer(Db,museen) & cnt(Db,read,museum_api) & part_of(Db,RhoI))) # label(conjecture) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.44/1.02 4 perm(p1) # label(perm_p1) # label(axiom). [assumption]. % 0.44/1.02 5 -perm(A) | -strong(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | disability(f3(A,B,C,D,E,F)) # label(ax_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 7 -perm(A) | -strong(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_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 8 -perm(A) | -strong(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | founds_imm(F,f1(A,B,C,D,E,F),A) # label(ax_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 10 -perm(A) | -strong(A) | -aee(A,B) | -aer(A,C) | -act(A,D) | -tgt(A,E) | -activates(F,A) | cnt(f3(A,B,C,D,E,F),D,E) # label(ax_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 12 -perm(A) | -strong(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_perm_relator_strong) # label(axiom). [clausify(1)]. % 0.44/1.02 14 strong(p1) # label(strong_p1) # label(axiom). [assumption]. % 0.44/1.02 15 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | disability(f3(p1,A,B,C,D,E)). [resolve(5,a,4,a)]. % 0.44/1.02 17 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f3(p1,A,B,C,D,E),B). [resolve(7,a,4,a)]. % 0.44/1.02 18 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | founds_imm(E,f1(p1,A,B,C,D,E),p1). [resolve(8,a,4,a)]. % 0.44/1.02 20 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f3(p1,A,B,C,D,E),C,D). [resolve(10,a,4,a)]. % 0.44/1.02 22 -strong(p1) | -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f3(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(12,a,4,a)]. % 0.44/1.02 24 aee(p1,bibliothek) # label(aee_p1) # label(axiom). [assumption]. % 0.44/1.02 25 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | disability(f3(p1,A,B,C,D,E)). [resolve(15,a,14,a)]. % 0.44/1.02 27 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | bearer(f3(p1,A,B,C,D,E),B). [resolve(17,a,14,a)]. % 0.44/1.02 28 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | founds_imm(E,f1(p1,A,B,C,D,E),p1). [resolve(18,a,14,a)]. % 0.44/1.02 30 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | cnt(f3(p1,A,B,C,D,E),C,D). [resolve(20,a,14,a)]. % 0.44/1.02 32 -aee(p1,A) | -aer(p1,B) | -act(p1,C) | -tgt(p1,D) | -activates(E,p1) | part_of(f3(p1,A,B,C,D,E),f1(p1,A,B,C,D,E)). [resolve(22,a,14,a)]. % 0.44/1.02 34 aer(p1,museen) # label(aer_p1) # label(axiom). [assumption]. % 0.44/1.02 35 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | disability(f3(p1,bibliothek,A,B,C,D)). [resolve(25,a,24,a)]. % 0.44/1.02 37 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | bearer(f3(p1,bibliothek,A,B,C,D),A). [resolve(27,a,24,a)]. % 0.44/1.02 38 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | founds_imm(D,f1(p1,bibliothek,A,B,C,D),p1). [resolve(28,a,24,a)]. % 0.44/1.02 40 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | cnt(f3(p1,bibliothek,A,B,C,D),B,C). [resolve(30,a,24,a)]. % 0.44/1.02 42 -aer(p1,A) | -act(p1,B) | -tgt(p1,C) | -activates(D,p1) | part_of(f3(p1,bibliothek,A,B,C,D),f1(p1,bibliothek,A,B,C,D)). [resolve(32,a,24,a)]. % 0.44/1.02 44 act(p1,read) # label(act_p1) # label(axiom). [assumption]. % 0.44/1.02 45 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | disability(f3(p1,bibliothek,museen,A,B,C)). [resolve(35,a,34,a)]. % 0.44/1.02 47 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | bearer(f3(p1,bibliothek,museen,A,B,C),museen). [resolve(37,a,34,a)]. % 0.44/1.02 48 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | founds_imm(C,f1(p1,bibliothek,museen,A,B,C),p1). [resolve(38,a,34,a)]. % 0.44/1.02 50 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | cnt(f3(p1,bibliothek,museen,A,B,C),A,B). [resolve(40,a,34,a)]. % 0.44/1.02 52 -act(p1,A) | -tgt(p1,B) | -activates(C,p1) | part_of(f3(p1,bibliothek,museen,A,B,C),f1(p1,bibliothek,museen,A,B,C)). [resolve(42,a,34,a)]. % 0.44/1.02 54 tgt(p1,museum_api) # label(tgt_p1) # label(axiom). [assumption]. % 0.44/1.02 55 -tgt(p1,A) | -activates(B,p1) | disability(f3(p1,bibliothek,museen,read,A,B)). [resolve(45,a,44,a)]. % 0.44/1.02 57 -tgt(p1,A) | -activates(B,p1) | bearer(f3(p1,bibliothek,museen,read,A,B),museen). [resolve(47,a,44,a)]. % 0.44/1.02 58 -tgt(p1,A) | -activates(B,p1) | founds_imm(B,f1(p1,bibliothek,museen,read,A,B),p1). [resolve(48,a,44,a)]. % 0.44/1.02 60 -tgt(p1,A) | -activates(B,p1) | cnt(f3(p1,bibliothek,museen,read,A,B),read,A). [resolve(50,a,44,a)]. % 0.44/1.02 62 -tgt(p1,A) | -activates(B,p1) | part_of(f3(p1,bibliothek,museen,read,A,B),f1(p1,bibliothek,museen,read,A,B)). [resolve(52,a,44,a)]. % 0.44/1.02 64 activates(e1,p1) # label(act_e1_p1) # label(axiom). [assumption]. % 0.44/1.02 65 -activates(A,p1) | disability(f3(p1,bibliothek,museen,read,museum_api,A)). [resolve(55,a,54,a)]. % 0.44/1.02 67 -activates(A,p1) | bearer(f3(p1,bibliothek,museen,read,museum_api,A),museen). [resolve(57,a,54,a)]. % 0.44/1.02 68 -activates(A,p1) | founds_imm(A,f1(p1,bibliothek,museen,read,museum_api,A),p1). [resolve(58,a,54,a)]. % 0.44/1.02 70 -activates(A,p1) | cnt(f3(p1,bibliothek,museen,read,museum_api,A),read,museum_api). [resolve(60,a,54,a)]. % 0.44/1.02 72 -activates(A,p1) | part_of(f3(p1,bibliothek,museen,read,museum_api,A),f1(p1,bibliothek,museen,read,museum_api,A)). [resolve(62,a,54,a)]. % 0.44/1.02 73 founds_imm(e1,f1(p1,bibliothek,museen,read,museum_api,e1),p1). [resolve(68,a,64,a)]. % 0.44/1.02 74 -founds_imm(e1,A,p1) | -disability(B) | -bearer(B,museen) | -cnt(B,read,museum_api) | -part_of(B,A) # label(conjecture) # label(negated_conjecture). [clausify(2)]. % 0.44/1.02 75 -disability(A) | -bearer(A,museen) | -cnt(A,read,museum_api) | -part_of(A,f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(73,a,74,a)]. % 0.44/1.02 76 disability(f3(p1,bibliothek,museen,read,museum_api,e1)). [resolve(65,a,64,a)]. % 0.44/1.02 77 -bearer(f3(p1,bibliothek,museen,read,museum_api,e1),museen) | -cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) | -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(75,a,76,a)]. % 0.44/1.02 79 bearer(f3(p1,bibliothek,museen,read,museum_api,e1),museen). [resolve(67,a,64,a)]. % 0.44/1.02 80 -cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api) | -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(77,a,79,a)]. % 0.44/1.02 82 cnt(f3(p1,bibliothek,museen,read,museum_api,e1),read,museum_api). [resolve(70,a,64,a)]. % 0.44/1.02 83 -part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(80,a,82,a)]. % 0.44/1.02 85 part_of(f3(p1,bibliothek,museen,read,museum_api,e1),f1(p1,bibliothek,museen,read,museum_api,e1)). [resolve(72,a,64,a)]. % 0.44/1.02 86 $F. [resolve(83,a,85,a)]. % 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=1. Kept=0. proofs=1. % 0.44/1.02 Usable=0. Sos=0. Demods=0. Limbo=0, Disabled=91. Hints=0. % 0.44/1.02 Megabytes=0.07. % 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 25261 exit (max_proofs) Tue Apr 28 19:33:06 2026 % 0.44/1.02 Prover9 interrupted %------------------------------------------------------------------------------