%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 29 02:10:30 PM UTC 2026 % Result : Unsatisfiable 0.84s 1.29s % Output : Refutation 0.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : MGT114+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.34 % Computer : n022.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Apr 28 19:31:06 EDT 2026 % 0.17/0.34 % CPUTime : % 0.81/1.10 ============================== Prover9 =============================== % 0.81/1.10 Prover9 (32) version 2009-11A, November 2009. % 0.81/1.10 Process 17565 was started by sandbox on n022.cluster.edu, % 0.81/1.10 Tue Apr 28 19:31:06 2026 % 0.81/1.10 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_17219_n022.cluster.edu". % 0.81/1.10 ============================== end of head =========================== % 0.81/1.10 % 0.81/1.10 ============================== INPUT ================================= % 0.81/1.10 % 0.81/1.10 % Reading from file /tmp/Prover9_17219_n022.cluster.edu % 0.81/1.10 % 0.81/1.10 set(prolog_style_variables). % 0.81/1.10 set(auto2). % 0.81/1.10 % set(auto2) -> set(auto). % 0.81/1.10 % set(auto) -> set(auto_inference). % 0.81/1.10 % set(auto) -> set(auto_setup). % 0.81/1.10 % set(auto_setup) -> set(predicate_elim). % 0.81/1.10 % set(auto_setup) -> assign(eq_defs, unfold). % 0.81/1.10 % set(auto) -> set(auto_limits). % 0.81/1.10 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.81/1.10 % set(auto_limits) -> assign(sos_limit, 20000). % 0.81/1.10 % set(auto) -> set(auto_denials). % 0.81/1.10 % set(auto) -> set(auto_process). % 0.81/1.10 % set(auto2) -> assign(new_constants, 1). % 0.81/1.10 % set(auto2) -> assign(fold_denial_max, 3). % 0.81/1.10 % set(auto2) -> assign(max_weight, "200.000"). % 0.81/1.10 % set(auto2) -> assign(max_hours, 1). % 0.81/1.10 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.81/1.10 % set(auto2) -> assign(max_seconds, 0). % 0.81/1.10 % set(auto2) -> assign(max_minutes, 5). % 0.81/1.10 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.81/1.10 % set(auto2) -> set(sort_initial_sos). % 0.81/1.10 % set(auto2) -> assign(sos_limit, -1). % 0.81/1.10 % set(auto2) -> assign(lrs_ticks, 3000). % 0.81/1.10 % set(auto2) -> assign(max_megs, 400). % 0.81/1.10 % set(auto2) -> assign(stats, some). % 0.81/1.10 % set(auto2) -> clear(echo_input). % 0.81/1.10 % set(auto2) -> set(quiet). % 0.81/1.10 % set(auto2) -> clear(print_initial_clauses). % 0.81/1.10 % set(auto2) -> clear(print_given). % 0.81/1.10 assign(lrs_ticks,-1). % 0.81/1.10 assign(sos_limit,10000). % 0.81/1.10 assign(order,kbo). % 0.81/1.10 set(lex_order_vars). % 0.81/1.10 clear(print_given). % 0.81/1.10 % 0.81/1.10 % formulas(sos). % not echoed (19 formulas) % 0.81/1.10 % 0.81/1.10 ============================== end of input ========================== % 0.81/1.10 % 0.81/1.10 % From the command line: assign(max_seconds, 300). % 0.81/1.10 % 0.81/1.10 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.81/1.10 % 0.81/1.10 % Formulas that are not ordinary clauses: % 0.81/1.10 1 (all Rho all A all T (odrl_rel(Rho) -> ((exists L (permission(L) & part_of(L,Rho) & cnt(L,A,T) & (all L2 (permission(L2) & part_of(L2,Rho) & cnt(L2,A,T) -> L2 = L)))) <-> (exists N (no_right(N) & part_of(N,Rho) & cnt(N,A,T) & (all M (no_right(M) & part_of(M,Rho) & cnt(M,A,T) -> M = N))))))) # label(ax_correlativity_permission) # label(axiom) # label(non_clause). [assumption]. % 0.81/1.10 2 (all L2 (permission(L2) & part_of(L2,rho1) & cnt(L2,some_action,some_target) -> L2 = l)) # label(perm_l_unique) # label(axiom) # label(non_clause). [assumption]. % 0.81/1.10 % 0.81/1.10 ============================== end of process non-clausal formulas === % 0.81/1.10 % 0.81/1.10 ============================== PROCESS INITIAL CLAUSES =============== % 0.81/1.10 % 0.81/1.10 ============================== PREDICATE ELIMINATION ================= % 0.81/1.10 3 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | permission(f1(A,C,D,B)) | no_right(f2(A,C,D)) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 4 odrl_rel(rho1) # label(odrl_rho1) # label(axiom). [assumption]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | permission(f1(rho1,B,C,A)) | no_right(f2(rho1,B,C)). [resolve(3,a,4,a)]. % 0.81/1.10 5 -odrl_rel(A) | permission(f3(A,B,C)) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | no_right(f4(A,B,C,D)) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: permission(f3(rho1,A,B)) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | no_right(f4(rho1,A,B,C)). [resolve(5,a,4,a)]. % 0.81/1.10 6 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | permission(f1(A,C,D,B)) | part_of(f2(A,C,D),A) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | permission(f1(rho1,B,C,A)) | part_of(f2(rho1,B,C),rho1). [resolve(6,a,4,a)]. % 0.81/1.10 7 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | part_of(f1(A,C,D,B),A) | no_right(f2(A,C,D)) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | part_of(f1(rho1,B,C,A),rho1) | no_right(f2(rho1,B,C)). [resolve(7,a,4,a)]. % 0.81/1.10 8 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | f1(A,C,D,B) != B | no_right(f2(A,C,D)) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | f1(rho1,B,C,A) != A | no_right(f2(rho1,B,C)). [resolve(8,a,4,a)]. % 0.81/1.10 9 -odrl_rel(A) | permission(f3(A,B,C)) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | part_of(f4(A,B,C,D),A) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: permission(f3(rho1,A,B)) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | part_of(f4(rho1,A,B,C),rho1). [resolve(9,a,4,a)]. % 0.81/1.10 10 -odrl_rel(A) | permission(f3(A,B,C)) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | f4(A,B,C,D) != D # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: permission(f3(rho1,A,B)) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | f4(rho1,A,B,C) != C. [resolve(10,a,4,a)]. % 0.81/1.10 11 -odrl_rel(A) | part_of(f3(A,B,C),A) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | no_right(f4(A,B,C,D)) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: part_of(f3(rho1,A,B),rho1) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | no_right(f4(rho1,A,B,C)). [resolve(11,a,4,a)]. % 0.81/1.10 12 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | permission(f1(A,C,D,B)) | cnt(f2(A,C,D),C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | permission(f1(rho1,B,C,A)) | cnt(f2(rho1,B,C),B,C). [resolve(12,a,4,a)]. % 0.81/1.10 13 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | part_of(f1(A,C,D,B),A) | part_of(f2(A,C,D),A) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | part_of(f1(rho1,B,C,A),rho1) | part_of(f2(rho1,B,C),rho1). [resolve(13,a,4,a)]. % 0.81/1.10 14 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | cnt(f1(A,C,D,B),C,D) | no_right(f2(A,C,D)) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | cnt(f1(rho1,B,C,A),B,C) | no_right(f2(rho1,B,C)). [resolve(14,a,4,a)]. % 0.81/1.10 15 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | f1(A,C,D,B) != B | part_of(f2(A,C,D),A) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | f1(rho1,B,C,A) != A | part_of(f2(rho1,B,C),rho1). [resolve(15,a,4,a)]. % 0.81/1.10 16 -odrl_rel(A) | permission(f3(A,B,C)) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | cnt(f4(A,B,C,D),B,C) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: permission(f3(rho1,A,B)) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | cnt(f4(rho1,A,B,C),A,B). [resolve(16,a,4,a)]. % 0.81/1.10 17 -odrl_rel(A) | part_of(f3(A,B,C),A) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | part_of(f4(A,B,C,D),A) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: part_of(f3(rho1,A,B),rho1) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | part_of(f4(rho1,A,B,C),rho1). [resolve(17,a,4,a)]. % 0.81/1.10 18 -odrl_rel(A) | part_of(f3(A,B,C),A) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | f4(A,B,C,D) != D # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: part_of(f3(rho1,A,B),rho1) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | f4(rho1,A,B,C) != C. [resolve(18,a,4,a)]. % 0.81/1.10 19 -odrl_rel(A) | cnt(f3(A,B,C),B,C) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | no_right(f4(A,B,C,D)) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: cnt(f3(rho1,A,B),A,B) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | no_right(f4(rho1,A,B,C)). [resolve(19,a,4,a)]. % 0.81/1.10 20 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | part_of(f1(A,C,D,B),A) | cnt(f2(A,C,D),C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | part_of(f1(rho1,B,C,A),rho1) | cnt(f2(rho1,B,C),B,C). [resolve(20,a,4,a)]. % 0.81/1.10 21 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | cnt(f1(A,C,D,B),C,D) | part_of(f2(A,C,D),A) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | cnt(f1(rho1,B,C,A),B,C) | part_of(f2(rho1,B,C),rho1). [resolve(21,a,4,a)]. % 0.81/1.10 22 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | f1(A,C,D,B) != B | cnt(f2(A,C,D),C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | f1(rho1,B,C,A) != A | cnt(f2(rho1,B,C),B,C). [resolve(22,a,4,a)]. % 0.81/1.10 23 -odrl_rel(A) | part_of(f3(A,B,C),A) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | cnt(f4(A,B,C,D),B,C) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: part_of(f3(rho1,A,B),rho1) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | cnt(f4(rho1,A,B,C),A,B). [resolve(23,a,4,a)]. % 0.81/1.10 24 -odrl_rel(A) | cnt(f3(A,B,C),B,C) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | part_of(f4(A,B,C,D),A) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: cnt(f3(rho1,A,B),A,B) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | part_of(f4(rho1,A,B,C),rho1). [resolve(24,a,4,a)]. % 0.81/1.10 25 -odrl_rel(A) | cnt(f3(A,B,C),B,C) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | f4(A,B,C,D) != D # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: cnt(f3(rho1,A,B),A,B) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | f4(rho1,A,B,C) != C. [resolve(25,a,4,a)]. % 0.81/1.10 26 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | cnt(f1(A,C,D,B),C,D) | cnt(f2(A,C,D),C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | cnt(f1(rho1,B,C,A),B,C) | cnt(f2(rho1,B,C),B,C). [resolve(26,a,4,a)]. % 0.81/1.10 27 -odrl_rel(A) | cnt(f3(A,B,C),B,C) | -no_right(D) | -part_of(D,A) | -cnt(D,B,C) | cnt(f4(A,B,C,D),B,C) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: cnt(f3(rho1,A,B),A,B) | -no_right(C) | -part_of(C,rho1) | -cnt(C,A,B) | cnt(f4(rho1,A,B,C),A,B). [resolve(27,a,4,a)]. % 0.81/1.10 28 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | permission(f1(A,C,D,B)) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | E = f2(A,C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | permission(f1(rho1,B,C,A)) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | D = f2(rho1,B,C). [resolve(28,a,4,a)]. % 0.81/1.10 29 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | B = f3(A,C,D) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | no_right(f4(A,C,D,E)) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | A = f3(rho1,B,C) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | no_right(f4(rho1,B,C,D)). [resolve(29,a,4,a)]. % 0.81/1.10 30 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | part_of(f1(A,C,D,B),A) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | E = f2(A,C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | part_of(f1(rho1,B,C,A),rho1) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | D = f2(rho1,B,C). [resolve(30,a,4,a)]. % 0.81/1.10 31 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | f1(A,C,D,B) != B | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | E = f2(A,C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | f1(rho1,B,C,A) != A | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | D = f2(rho1,B,C). [resolve(31,a,4,a)]. % 0.81/1.10 32 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | B = f3(A,C,D) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | part_of(f4(A,C,D,E),A) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.81/1.10 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | A = f3(rho1,B,C) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | part_of(f4(rho1,B,C,D),rho1). [resolve(32,a,4,a)]. % 0.84/1.29 33 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | B = f3(A,C,D) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | f4(A,C,D,E) != E # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.84/1.29 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | A = f3(rho1,B,C) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | f4(rho1,B,C,D) != D. [resolve(33,a,4,a)]. % 0.84/1.29 34 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | cnt(f1(A,C,D,B),C,D) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | E = f2(A,C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.84/1.29 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | cnt(f1(rho1,B,C,A),B,C) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | D = f2(rho1,B,C). [resolve(34,a,4,a)]. % 0.84/1.29 35 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | B = f3(A,C,D) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | cnt(f4(A,C,D,E),C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.84/1.29 Derived: -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | A = f3(rho1,B,C) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | cnt(f4(rho1,B,C,D),B,C). [resolve(35,a,4,a)]. % 0.84/1.29 % 0.84/1.29 ============================== end predicate elimination ============= % 0.84/1.29 % 0.84/1.29 Auto_denials: (non-Horn, no changes). % 0.84/1.29 % 0.84/1.29 Term ordering decisions: % 0.84/1.29 Function symbol KB weights: rho1=1. l=1. some_action=1. some_target=1. n1=1. n2=1. f2=1. f3=1. f1=1. f4=1. % 0.84/1.29 % 0.84/1.29 ============================== end of process initial clauses ======== % 0.84/1.29 % 0.84/1.29 ============================== CLAUSES FOR SEARCH ==================== % 0.84/1.29 % 0.84/1.29 ============================== end of clauses for search ============= % 0.84/1.29 % 0.84/1.29 ============================== SEARCH ================================ % 0.84/1.29 % 0.84/1.29 % Starting search at 0.02 seconds. % 0.84/1.29 % 0.84/1.29 ============================== PROOF ================================= % 0.84/1.29 % SZS status Unsatisfiable % 0.84/1.29 % SZS output start Refutation % 0.84/1.29 % 0.84/1.29 % Proof 1 at 0.20 (+ 0.00) seconds. % 0.84/1.29 % Length of proof is 49. % 0.84/1.29 % Level of proof is 11. % 0.84/1.29 % Maximum clause weight is 32.000. % 0.84/1.29 % Given clauses 270. % 0.84/1.29 % 0.84/1.29 1 (all Rho all A all T (odrl_rel(Rho) -> ((exists L (permission(L) & part_of(L,Rho) & cnt(L,A,T) & (all L2 (permission(L2) & part_of(L2,Rho) & cnt(L2,A,T) -> L2 = L)))) <-> (exists N (no_right(N) & part_of(N,Rho) & cnt(N,A,T) & (all M (no_right(M) & part_of(M,Rho) & cnt(M,A,T) -> M = N))))))) # label(ax_correlativity_permission) # label(axiom) # label(non_clause). [assumption]. % 0.84/1.29 2 (all L2 (permission(L2) & part_of(L2,rho1) & cnt(L2,some_action,some_target) -> L2 = l)) # label(perm_l_unique) # label(axiom) # label(non_clause). [assumption]. % 0.84/1.29 4 odrl_rel(rho1) # label(odrl_rho1) # label(axiom). [assumption]. % 0.84/1.29 28 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | permission(f1(A,C,D,B)) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | E = f2(A,C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.84/1.29 30 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | part_of(f1(A,C,D,B),A) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | E = f2(A,C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.84/1.29 31 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | f1(A,C,D,B) != B | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | E = f2(A,C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.84/1.29 34 -odrl_rel(A) | -permission(B) | -part_of(B,A) | -cnt(B,C,D) | cnt(f1(A,C,D,B),C,D) | -no_right(E) | -part_of(E,A) | -cnt(E,C,D) | E = f2(A,C,D) # label(ax_correlativity_permission) # label(axiom). [clausify(1)]. % 0.84/1.29 36 permission(l) # label(permission_l) # label(axiom). [assumption]. % 0.84/1.29 37 no_right(n1) # label(no_right_n1) # label(axiom). [assumption]. % 0.84/1.29 38 no_right(n2) # label(no_right_n2) # label(axiom). [assumption]. % 0.84/1.29 39 part_of(l,rho1) # label(partof_l) # label(axiom). [assumption]. % 0.84/1.29 40 part_of(n1,rho1) # label(partof_n1) # label(axiom). [assumption]. % 0.84/1.29 41 part_of(n2,rho1) # label(partof_n2) # label(axiom). [assumption]. % 0.84/1.29 42 cnt(l,some_action,some_target) # label(cnt_l) # label(axiom). [assumption]. % 0.84/1.29 43 cnt(n1,some_action,some_target) # label(cnt_n1) # label(axiom). [assumption]. % 0.84/1.29 44 cnt(n2,some_action,some_target) # label(cnt_n2) # label(axiom). [assumption]. % 0.84/1.29 45 n1 != n2 # label(n1_neq_n2) # label(axiom). [assumption]. % 0.84/1.29 46 n2 != n1. [copy(45),flip(a)]. % 0.84/1.29 47 -permission(A) | -part_of(A,rho1) | -cnt(A,some_action,some_target) | l = A # label(perm_l_unique) # label(axiom). [clausify(2)]. % 0.84/1.29 72 -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | permission(f1(rho1,B,C,A)) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | D = f2(rho1,B,C). [resolve(28,a,4,a)]. % 0.84/1.29 73 -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | permission(f1(rho1,B,C,A)) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | f2(rho1,B,C) = D. [copy(72),flip(h)]. % 0.84/1.29 76 -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | part_of(f1(rho1,B,C,A),rho1) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | D = f2(rho1,B,C). [resolve(30,a,4,a)]. % 0.84/1.29 77 -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | part_of(f1(rho1,B,C,A),rho1) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | f2(rho1,B,C) = D. [copy(76),flip(h)]. % 0.84/1.29 78 -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | f1(rho1,B,C,A) != A | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | D = f2(rho1,B,C). [resolve(31,a,4,a)]. % 0.84/1.29 79 -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | f1(rho1,B,C,A) != A | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | f2(rho1,B,C) = D. [copy(78),flip(h)]. % 0.84/1.29 84 -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | cnt(f1(rho1,B,C,A),B,C) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | D = f2(rho1,B,C). [resolve(34,a,4,a)]. % 0.84/1.29 85 -permission(A) | -part_of(A,rho1) | -cnt(A,B,C) | cnt(f1(rho1,B,C,A),B,C) | -no_right(D) | -part_of(D,rho1) | -cnt(D,B,C) | f2(rho1,B,C) = D. [copy(84),flip(h)]. % 0.84/1.29 172 permission(f1(rho1,some_action,some_target,l)) | -no_right(A) | -part_of(A,rho1) | -cnt(A,some_action,some_target) | f2(rho1,some_action,some_target) = A. [resolve(73,c,42,a),unit_del(a,36),unit_del(b,39)]. % 0.84/1.29 184 part_of(f1(rho1,some_action,some_target,l),rho1) | -no_right(A) | -part_of(A,rho1) | -cnt(A,some_action,some_target) | f2(rho1,some_action,some_target) = A. [resolve(77,c,42,a),unit_del(a,36),unit_del(b,39)]. % 0.84/1.29 190 f1(rho1,some_action,some_target,l) != l | -no_right(A) | -part_of(A,rho1) | -cnt(A,some_action,some_target) | f2(rho1,some_action,some_target) = A. [resolve(79,c,42,a),unit_del(a,36),unit_del(b,39)]. % 0.84/1.29 208 cnt(f1(rho1,some_action,some_target,l),some_action,some_target) | -no_right(A) | -part_of(A,rho1) | -cnt(A,some_action,some_target) | f2(rho1,some_action,some_target) = A. [resolve(85,c,42,a),unit_del(a,36),unit_del(b,39)]. % 0.84/1.29 771 permission(f1(rho1,some_action,some_target,l)) | f2(rho1,some_action,some_target) = n2. [resolve(172,d,44,a),unit_del(b,38),unit_del(c,41)]. % 0.84/1.29 772 permission(f1(rho1,some_action,some_target,l)) | f2(rho1,some_action,some_target) = n1. [resolve(172,d,43,a),unit_del(b,37),unit_del(c,40)]. % 0.84/1.29 870 part_of(f1(rho1,some_action,some_target,l),rho1) | f2(rho1,some_action,some_target) = n2. [resolve(184,d,44,a),unit_del(b,38),unit_del(c,41)]. % 0.84/1.29 871 part_of(f1(rho1,some_action,some_target,l),rho1) | f2(rho1,some_action,some_target) = n1. [resolve(184,d,43,a),unit_del(b,37),unit_del(c,40)]. % 0.84/1.29 916 f1(rho1,some_action,some_target,l) != l | f2(rho1,some_action,some_target) = n2. [resolve(190,d,44,a),unit_del(b,38),unit_del(c,41)]. % 0.84/1.29 917 f1(rho1,some_action,some_target,l) != l | f2(rho1,some_action,some_target) = n1. [resolve(190,d,43,a),unit_del(b,37),unit_del(c,40)]. % 0.84/1.29 1060 cnt(f1(rho1,some_action,some_target,l),some_action,some_target) | f2(rho1,some_action,some_target) = n2. [resolve(208,d,44,a),unit_del(b,38),unit_del(c,41)]. % 0.84/1.29 1061 cnt(f1(rho1,some_action,some_target,l),some_action,some_target) | f2(rho1,some_action,some_target) = n1. [resolve(208,d,43,a),unit_del(b,37),unit_del(c,40)]. % 0.84/1.29 1110 f2(rho1,some_action,some_target) = n2 | -permission(f1(rho1,some_action,some_target,l)) | -part_of(f1(rho1,some_action,some_target,l),rho1) | f1(rho1,some_action,some_target,l) = l. [resolve(1060,a,47,c),flip(d)]. % 0.84/1.29 1157 f2(rho1,some_action,some_target) = n1 | -permission(f1(rho1,some_action,some_target,l)) | -part_of(f1(rho1,some_action,some_target,l),rho1) | f1(rho1,some_action,some_target,l) = l. [resolve(1061,a,47,c),flip(d)]. % 0.84/1.29 1433 f2(rho1,some_action,some_target) = n2 | -permission(f1(rho1,some_action,some_target,l)) | f1(rho1,some_action,some_target,l) = l. [resolve(1110,c,870,a),merge(d)]. % 0.84/1.29 1435 f2(rho1,some_action,some_target) = n2 | f1(rho1,some_action,some_target,l) = l. [resolve(1433,b,771,a),merge(c)]. % 0.84/1.29 1437 f2(rho1,some_action,some_target) = n2. [resolve(1435,b,916,a),merge(b)]. % 0.84/1.29 1546 -permission(f1(rho1,some_action,some_target,l)) | -part_of(f1(rho1,some_action,some_target,l),rho1) | f1(rho1,some_action,some_target,l) = l. [back_rewrite(1157),rewrite([1437(4)]),unit_del(a,46)]. % 0.84/1.29 1653 f1(rho1,some_action,some_target,l) != l. [back_rewrite(917),rewrite([1437(11)]),unit_del(b,46)]. % 0.84/1.29 1665 part_of(f1(rho1,some_action,some_target,l),rho1). [back_rewrite(871),rewrite([1437(11)]),unit_del(b,46)]. % 0.84/1.29 1698 permission(f1(rho1,some_action,some_target,l)). [back_rewrite(772),rewrite([1437(10)]),unit_del(b,46)]. % 0.84/1.29 1755 $F. [back_unit_del(1546),unit_del(a,1698),unit_del(b,1665),unit_del(c,1653)]. % 0.84/1.29 % 0.84/1.29 % SZS output end Refutation % 0.84/1.29 ============================== end of proof ========================== % 0.84/1.29 % 0.84/1.29 ============================== STATISTICS ============================ % 0.84/1.29 % 0.84/1.29 Given=270. Generated=3398. Kept=1710. proofs=1. % 0.84/1.29 Usable=153. Sos=193. Demods=1. Limbo=102, Disabled=1344. Hints=0. % 0.84/1.29 Megabytes=2.67. % 0.84/1.29 User_CPU=0.20, System_CPU=0.00, Wall_clock=0. % 0.84/1.29 % 0.84/1.29 ============================== end of statistics ===================== % 0.84/1.29 % 0.84/1.29 ============================== end of search ========================= % 0.84/1.29 % 0.84/1.29 THEOREM PROVED % 0.84/1.29 % SZS status Unsatisfiable % 0.84/1.29 % 0.84/1.29 Exiting with 1 proof. % 0.84/1.29 % 0.84/1.29 Process 17565 exit (max_proofs) Tue Apr 28 19:31:06 2026 % 0.84/1.29 Prover9 interrupted %------------------------------------------------------------------------------