%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : MGT116+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n017.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.78s 1.08s % Output : Refutation 0.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : MGT116+1 : TPTP v9.3.0. Released v9.3.0. % 0.11/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.16/0.34 % Computer : n017.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Apr 28 19:30:57 EDT 2026 % 0.16/0.34 % CPUTime : % 0.78/1.08 ============================== Prover9 =============================== % 0.78/1.08 Prover9 (32) version 2009-11A, November 2009. % 0.78/1.08 Process 18152 was started by sandbox on n017.cluster.edu, % 0.78/1.08 Tue Apr 28 19:30:58 2026 % 0.78/1.08 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_17971_n017.cluster.edu". % 0.78/1.08 ============================== end of head =========================== % 0.78/1.08 % 0.78/1.08 ============================== INPUT ================================= % 0.78/1.08 % 0.78/1.08 % Reading from file /tmp/Prover9_17971_n017.cluster.edu % 0.78/1.08 % 0.78/1.08 set(prolog_style_variables). % 0.78/1.08 set(auto2). % 0.78/1.08 % set(auto2) -> set(auto). % 0.78/1.08 % set(auto) -> set(auto_inference). % 0.78/1.08 % set(auto) -> set(auto_setup). % 0.78/1.08 % set(auto_setup) -> set(predicate_elim). % 0.78/1.08 % set(auto_setup) -> assign(eq_defs, unfold). % 0.78/1.08 % set(auto) -> set(auto_limits). % 0.78/1.08 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.78/1.08 % set(auto_limits) -> assign(sos_limit, 20000). % 0.78/1.08 % set(auto) -> set(auto_denials). % 0.78/1.08 % set(auto) -> set(auto_process). % 0.78/1.08 % set(auto2) -> assign(new_constants, 1). % 0.78/1.08 % set(auto2) -> assign(fold_denial_max, 3). % 0.78/1.08 % set(auto2) -> assign(max_weight, "200.000"). % 0.78/1.08 % set(auto2) -> assign(max_hours, 1). % 0.78/1.08 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.78/1.08 % set(auto2) -> assign(max_seconds, 0). % 0.78/1.08 % set(auto2) -> assign(max_minutes, 5). % 0.78/1.08 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.78/1.08 % set(auto2) -> set(sort_initial_sos). % 0.78/1.08 % set(auto2) -> assign(sos_limit, -1). % 0.78/1.08 % set(auto2) -> assign(lrs_ticks, 3000). % 0.78/1.08 % set(auto2) -> assign(max_megs, 400). % 0.78/1.08 % set(auto2) -> assign(stats, some). % 0.78/1.08 % set(auto2) -> clear(echo_input). % 0.78/1.08 % set(auto2) -> set(quiet). % 0.78/1.08 % set(auto2) -> clear(print_initial_clauses). % 0.78/1.08 % set(auto2) -> clear(print_given). % 0.78/1.08 assign(lrs_ticks,-1). % 0.78/1.08 assign(sos_limit,10000). % 0.78/1.08 assign(order,kbo). % 0.78/1.08 set(lex_order_vars). % 0.78/1.08 clear(print_given). % 0.78/1.08 % 0.78/1.08 % formulas(sos). % not echoed (12 formulas) % 0.78/1.08 % 0.78/1.08 ============================== end of input ========================== % 0.78/1.08 % 0.78/1.08 % From the command line: assign(max_seconds, 300). % 0.78/1.08 % 0.78/1.08 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.78/1.08 % 0.78/1.08 % Formulas that are not ordinary clauses: % 0.78/1.08 1 (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.78/1.08 % 0.78/1.08 ============================== end of process non-clausal formulas === % 0.78/1.08 % 0.78/1.08 ============================== PROCESS INITIAL CLAUSES =============== % 0.78/1.08 % 0.78/1.08 ============================== PREDICATE ELIMINATION ================= % 0.78/1.08 2 -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(1)]. % 0.78/1.08 3 subjection(s) # label(subj_s) # label(axiom). [assumption]. % 0.78/1.08 Derived: -cnt(s,decl(A),B) | -part_of(s,C) | -founds_rem(D,C,E) | about_event(s,D). [resolve(2,a,3,a)]. % 0.78/1.08 4 -cnt(s,decl(A),B) | -part_of(s,C) | -founds_rem(D,C,E) | about_event(s,D). [resolve(2,a,3,a)]. % 0.78/1.08 5 part_of(s,rho_r) # label(partof_s) # label(axiom). [assumption]. % 0.78/1.08 Derived: -cnt(s,decl(A),B) | -founds_rem(C,rho_r,D) | about_event(s,C). [resolve(4,b,5,a)]. % 0.78/1.08 6 -cnt(s,decl(A),B) | -founds_rem(C,rho_r,D) | about_event(s,C). [resolve(4,b,5,a)]. % 0.78/1.08 7 founds_rem(e1,rho_r,f1) # label(founds_rem1) # label(axiom). [assumption]. % 0.78/1.08 Derived: -cnt(s,decl(A),B) | about_event(s,e1). [resolve(6,b,7,a)]. % 0.78/1.08 8 -cnt(s,decl(A),B) | about_event(s,e1). [resolve(6,b,7,a)]. % 0.78/1.08 9 cnt(s,decl(some_action),some_target) # label(cnt_s) # label(axiom). [assumption]. % 0.78/1.08 Derived: about_event(s,e1). [resolve(8,a,9,a)]. % 0.78/1.08 10 about_event(s,e1). [resolve(8,a,9,a)]. % 0.78/1.08 11 -about_event(s,e1) # label(conjecture) # label(negated_conjecture). [assumption]. % 0.78/1.08 Derived: $F. [resolve(10,a,11,a)]. % 0.78/1.08 % 0.78/1.08 ============================== end predicate elimination ============= % 0.78/1.08 % 0.78/1.08 Auto_denials: (no changes). % 0.78/1.08 % 0.78/1.08 Term ordering decisions: % 0.78/1.08 Function symbol KB weights: % 0.78/1.08 % 0.78/1.08 ============================== PROOF ================================= % 0.78/1.08 % SZS status Theorem % 0.78/1.08 % SZS output start Refutation % 0.78/1.08 % 0.78/1.08 % Proof 1 at 0.01 (+ 0.00) seconds. % 0.78/1.08 % Length of proof is 12. % 0.78/1.08 % Level of proof is 6. % 0.78/1.08 % Maximum clause weight is 0.000. % 0.78/1.08 % Given clauses 0. % 0.78/1.08 % 0.78/1.08 1 (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.78/1.08 2 -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(1)]. % 0.78/1.08 3 subjection(s) # label(subj_s) # label(axiom). [assumption]. % 0.78/1.08 4 -cnt(s,decl(A),B) | -part_of(s,C) | -founds_rem(D,C,E) | about_event(s,D). [resolve(2,a,3,a)]. % 0.78/1.08 5 part_of(s,rho_r) # label(partof_s) # label(axiom). [assumption]. % 0.78/1.08 6 -cnt(s,decl(A),B) | -founds_rem(C,rho_r,D) | about_event(s,C). [resolve(4,b,5,a)]. % 0.78/1.08 7 founds_rem(e1,rho_r,f1) # label(founds_rem1) # label(axiom). [assumption]. % 0.78/1.08 8 -cnt(s,decl(A),B) | about_event(s,e1). [resolve(6,b,7,a)]. % 0.78/1.08 9 cnt(s,decl(some_action),some_target) # label(cnt_s) # label(axiom). [assumption]. % 0.78/1.08 10 about_event(s,e1). [resolve(8,a,9,a)]. % 0.78/1.08 11 -about_event(s,e1) # label(conjecture) # label(negated_conjecture). [assumption]. % 0.78/1.08 12 $F. [resolve(10,a,11,a)]. % 0.78/1.08 % 0.78/1.08 % SZS output end Refutation % 0.78/1.08 ============================== end of proof ========================== % 0.78/1.08 % 0.78/1.08 ============================== STATISTICS ============================ % 0.78/1.08 % 0.78/1.08 Given=0. Generated=1. Kept=0. proofs=1. % 0.78/1.08 Usable=0. Sos=0. Demods=0. Limbo=0, Disabled=17. Hints=0. % 0.78/1.08 Megabytes=0.02. % 0.78/1.08 User_CPU=0.01, System_CPU=0.00, Wall_clock=0. % 0.78/1.08 % 0.78/1.08 ============================== end of statistics ===================== % 0.78/1.08 % 0.78/1.08 ============================== end of search ========================= % 0.78/1.08 % 0.78/1.08 THEOREM PROVED % 0.78/1.08 % SZS status Theorem % 0.78/1.08 % 0.78/1.08 Exiting with 1 proof. % 0.78/1.08 % 0.78/1.08 Process 18152 exit (max_proofs) Tue Apr 28 19:30:58 2026 % 0.78/1.08 Prover9 interrupted %------------------------------------------------------------------------------