%------------------------------------------------------------------------------
% File : CSI_E---1.1
% Problem : MGT112+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar mcs_scs.jar %d %s
% Computer : n029.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:04:39 AM UTC 2026
% Result : Unsatisfiable 0.22s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT112+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.02 % Command : java -jar mcs_scs.jar %d %s
% 0.07/0.35 % Computer : n029.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 7 14:08:41 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.22/0.48 start to proof:theBenchmark.p
% 0.22/0.55 % Version : CSI_E---1.1
% 0.22/0.55 % Problem : theBenchmark.p
% 0.22/0.55 % Proof found!
% 0.22/0.55 # SZS status Unsatisfiable
% 0.22/0.55 % SZS output start Proof
% 0.22/0.55 fof(ax_disability_block, axiom, ![X1, X2, X3, X4, X5]:((((((proh(X1)&aee(X1,X2))&aer(X1,X3))&act(X1,X4))&tgt(X1,X5))=>~(?[X6]:(((disability(X6)&bearer(X6,X3))&cnt(X6,X4,X5)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax_disability_block)).
% 0.22/0.55 fof(cnt_db, axiom, cnt(db,read,museum_api), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cnt_db)).
% 0.22/0.55 fof(disability_db, axiom, disability(db), file('/export/starexec/sandbox/benchmark/theBenchmark.p', disability_db)).
% 0.22/0.55 fof(tgt_f2, axiom, tgt(f2,museum_api), file('/export/starexec/sandbox/benchmark/theBenchmark.p', tgt_f2)).
% 0.22/0.55 fof(act_f2, axiom, act(f2,read), file('/export/starexec/sandbox/benchmark/theBenchmark.p', act_f2)).
% 0.22/0.55 fof(proh_f2, axiom, proh(f2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', proh_f2)).
% 0.22/0.55 fof(aer_f2, axiom, aer(f2,museen), file('/export/starexec/sandbox/benchmark/theBenchmark.p', aer_f2)).
% 0.22/0.55 fof(bearer_db, axiom, bearer(db,museen), file('/export/starexec/sandbox/benchmark/theBenchmark.p', bearer_db)).
% 0.22/0.55 fof(aee_f2, axiom, aee(f2,bibliothek), file('/export/starexec/sandbox/benchmark/theBenchmark.p', aee_f2)).
% 0.22/0.55 fof(c_0_9, plain, ![X7, X8, X9, X10, X11, X12]:((~proh(X7)|~aee(X7,X8)|~aer(X7,X9)|~act(X7,X10)|~tgt(X7,X11)|(~disability(X12)|~bearer(X12,X9)|~cnt(X12,X10,X11)))), inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[ax_disability_block])])])])).
% 0.22/0.55 cnf(c_0_10, plain, (~proh(X1)|~aee(X1,X2)|~aer(X1,X3)|~act(X1,X4)|~tgt(X1,X5)|~disability(X6)|~bearer(X6,X3)|~cnt(X6,X4,X5)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.22/0.55 cnf(c_0_11, plain, (cnt(db,read,museum_api)), inference(split_conjunct,[status(thm)],[cnt_db])).
% 0.22/0.55 cnf(c_0_12, plain, (disability(db)), inference(split_conjunct,[status(thm)],[disability_db])).
% 0.22/0.55 cnf(c_0_13, plain, (~bearer(db,X1)|~tgt(X2,museum_api)|~act(X2,read)|~aer(X2,X1)|~aee(X2,X3)|~proh(X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_10, c_0_11]), c_0_12])])).
% 0.22/0.55 cnf(c_0_14, plain, (tgt(f2,museum_api)), inference(split_conjunct,[status(thm)],[tgt_f2])).
% 0.22/0.55 cnf(c_0_15, plain, (act(f2,read)), inference(split_conjunct,[status(thm)],[act_f2])).
% 0.22/0.55 cnf(c_0_16, plain, (proh(f2)), inference(split_conjunct,[status(thm)],[proh_f2])).
% 0.22/0.55 cnf(c_0_17, plain, (~bearer(db,X1)|~aer(f2,X1)|~aee(f2,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_13, c_0_14]), c_0_15]), c_0_16])])).
% 0.22/0.55 cnf(c_0_18, plain, (aer(f2,museen)), inference(split_conjunct,[status(thm)],[aer_f2])).
% 0.22/0.55 cnf(c_0_19, plain, (bearer(db,museen)), inference(split_conjunct,[status(thm)],[bearer_db])).
% 0.22/0.55 cnf(c_0_20, plain, (aee(f2,bibliothek)), inference(split_conjunct,[status(thm)],[aee_f2])).
% 0.22/0.55 cnf(c_0_21, plain, (~aee(f2,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17, c_0_18]), c_0_19])])).
% 0.22/0.55 cnf(c_0_22, plain, ($false), inference(sr,[status(thm)],[c_0_20, c_0_21]), ['proof']).
% 0.22/0.55 % SZS output end Proof
% 0.22/0.55 % User time : 0.004 s
% 0.22/0.55 % System time : 0.005 s
% 0.22/0.55 % Total time : 0.008 s
% 0.22/0.55 % User time : 0.019 s
% 0.22/0.55 % System time : 0.012 s
% 0.22/0.55 % Total time : 0.031 s
% 0.22/0.55
%------------------------------------------------------------------------------