%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : MGT116+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:18:53 AM UTC 2026
% Result : Theorem 0.33s 0.58s
% Output : CNFRefutation 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT116+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.04 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.08/0.34 % Computer : n009.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 7 14:09:22 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:155: SyntaxWarning: invalid escape sequence '\.'
% 0.13/0.40 (re.compile("\."), Token.FullStop),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:156: SyntaxWarning: invalid escape sequence '\('
% 0.13/0.40 (re.compile("\("), Token.OpenPar),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:157: SyntaxWarning: invalid escape sequence '\)'
% 0.13/0.40 (re.compile("\)"), Token.ClosePar),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:158: SyntaxWarning: invalid escape sequence '\['
% 0.13/0.40 (re.compile("\["), Token.OpenSquare),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:159: SyntaxWarning: invalid escape sequence '\]'
% 0.13/0.40 (re.compile("\]"), Token.CloseSquare),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:162: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.40 (re.compile("~\|"), Token.Nor),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:164: SyntaxWarning: invalid escape sequence '\|'
% 0.13/0.40 (re.compile("\|"), Token.Or),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:175: SyntaxWarning: invalid escape sequence '\?'
% 0.13/0.40 (re.compile("\?"), Token.Existential),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:176: SyntaxWarning: invalid escape sequence '\s'
% 0.13/0.40 (re.compile("\s+"), Token.WhiteSpace),
% 0.13/0.40 /export/starexec/sandbox/solver/bin/lexer.py:180: SyntaxWarning: invalid escape sequence '\$'
% 0.13/0.40 (re.compile("\$[_a-z0-9_A-Z]*"), Token.DefFunctor),
% 0.23/0.47 /export/starexec/sandbox/solver/bin/signature.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.47 """
% 0.23/0.47 /export/starexec/sandbox/solver/bin/literals.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.23/0.47 """
% 0.33/0.56 /export/starexec/sandbox/solver/bin/unification.py:6: SyntaxWarning: invalid escape sequence '\c'
% 0.33/0.56 """
% 0.33/0.58 % Version: 1.5
% 0.33/0.58 % SZS status Theorem
% 0.33/0.58 % SZS output start CNFRefutation
% 0.33/0.58 fof(conjecture,conjecture,about_event(s,e1),file('/export/starexec/sandbox/benchmark/theBenchmark.p', conjecture)).
% 0.33/0.58 fof(c0,negated_conjecture,(~about_event(s,e1)),inference(assume_negation,[status(cth)],[conjecture])).
% 0.33/0.58 fof(c1,negated_conjecture,~about_event(s,e1),inference(fof_simplification,[status(thm)],[c0])).
% 0.33/0.58 cnf(c2,negated_conjecture,~about_event(s,e1),inference(split_conjunct,[status(thm)],[c1])).
% 0.33/0.58 fof(subj_s,axiom,subjection(s),file('/export/starexec/sandbox/benchmark/theBenchmark.p', subj_s)).
% 0.33/0.58 cnf(c6,plain,subjection(s),inference(split_conjunct,[status(thm)],[subj_s])).
% 0.33/0.58 fof(partof_s,axiom,part_of(s,rho_r),file('/export/starexec/sandbox/benchmark/theBenchmark.p', partof_s)).
% 0.33/0.58 cnf(c4,plain,part_of(s,rho_r),inference(split_conjunct,[status(thm)],[partof_s])).
% 0.33/0.58 fof(founds_rem1,axiom,founds_rem(e1,rho_r,f1),file('/export/starexec/sandbox/benchmark/theBenchmark.p', founds_rem1)).
% 0.33/0.58 cnf(c3,plain,founds_rem(e1,rho_r,f1),inference(split_conjunct,[status(thm)],[founds_rem1])).
% 0.33/0.58 fof(cnt_s,axiom,cnt(s,decl(some_action),some_target),file('/export/starexec/sandbox/benchmark/theBenchmark.p', cnt_s)).
% 0.33/0.58 cnf(c5,plain,cnt(s,decl(some_action),some_target),inference(split_conjunct,[status(thm)],[cnt_s])).
% 0.33/0.58 fof(ax_B3,axiom,(![S]:(![A]:(![T]:(![Rho]:(![E]:(![R]:((((subjection(S)&cnt(S,decl(A),T))&part_of(S,Rho))&founds_rem(E,Rho,R))=>about_event(S,E)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax_B3)).
% 0.33/0.58 fof(c13,plain,(![S]:(![A]:(![T]:(![Rho]:(![E]:(![R]:((((~subjection(S)|~cnt(S,decl(A),T))|~part_of(S,Rho))|~founds_rem(E,Rho,R))|about_event(S,E)))))))),inference(fof_nnf,[status(thm)],[ax_B3])).
% 0.33/0.58 fof(c14,plain,(![S]:(![A]:(![T]:(![Rho]:(![E]:((((~subjection(S)|~cnt(S,decl(A),T))|~part_of(S,Rho))|(![R]:~founds_rem(E,Rho,R)))|about_event(S,E))))))),inference(shift_quantors,[status(thm)],[c13])).
% 0.33/0.58 fof(c16,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((((~subjection(X2)|~cnt(X2,decl(X3),X4))|~part_of(X2,X5))|~founds_rem(X6,X5,X7))|about_event(X2,X6)))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:((((~subjection(X2)|~cnt(X2,decl(X3),X4))|~part_of(X2,X5))|(![X7]:~founds_rem(X6,X5,X7)))|about_event(X2,X6))))))),inference(variable_rename,[status(thm)],[c14])).])).
% 0.33/0.58 cnf(c17,plain,~subjection(X8)|~cnt(X8,decl(X10),X12)|~part_of(X8,X11)|~founds_rem(X13,X11,X9)|about_event(X8,X13),inference(split_conjunct,[status(thm)],[c16])).
% 0.33/0.58 cnf(c18,plain,~subjection(s)|~part_of(s,X15)|~founds_rem(X14,X15,X16)|about_event(s,X14),inference(resolution,[status(thm)],[c17, c5])).
% 0.33/0.58 cnf(c19,plain,~subjection(s)|~part_of(s,rho_r)|about_event(s,e1),inference(resolution,[status(thm)],[c18, c3])).
% 0.33/0.58 cnf(c20,plain,~subjection(s)|about_event(s,e1),inference(resolution,[status(thm)],[c19, c4])).
% 0.33/0.58 cnf(c21,plain,about_event(s,e1),inference(resolution,[status(thm)],[c20, c6])).
% 0.33/0.58 cnf(c22,plain,$false,inference(resolution,[status(thm)],[c21, c2])).
% 0.33/0.58 % SZS output end CNFRefutation
% 0.33/0.58
% 0.33/0.58 % Initial clauses : 12
% 0.33/0.58 % Processed clauses : 16
% 0.33/0.58 % Factors computed : 0
% 0.33/0.58 % Resolvents computed: 5
% 0.33/0.58 % Tautologies deleted: 0
% 0.33/0.58 % Forward subsumed : 0
% 0.33/0.58 % Backward subsumed : 2
% 0.33/0.58 % -------- CPU Time ---------
% 0.33/0.58 % User time : 0.214 s
% 0.33/0.58 % System time : 0.027 s
% 0.33/0.58 % Total time : 0.241 s
%------------------------------------------------------------------------------