%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : MGT015+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:11:20 AM UTC 2026
% Result : Theorem 0.12s 0.36s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT015+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 7 11:55:54 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % launching worker at depth: 1
% 0.08/0.35 % launching worker at depth: 6
% 0.08/0.35 % launching worker at depth: 2
% 0.08/0.35 % launching worker at depth: 8
% 0.08/0.35 % launching worker at depth: 4
% 0.08/0.35 % launching worker at depth: 5
% 0.08/0.35 % launching worker at depth: 7
% 0.08/0.35 % launching worker at depth: 3
% 0.12/0.36 % launching worker at depth: 9
% 0.12/0.36 % SZS status Theorem for theBenchmark
% 0.12/0.36 % SZS output start CNFRefutation
% 0.12/0.36 fof(t15_FOL, plain, ![X,Y,Re,C,C1,C2,Ta,Tb,Tc]:((organization(X,Ta)&organization(Y,Ta)&organization(Y,Tc)&class(X,C,Ta)&class(Y,C,Ta)&reorganization(X,Ta,Tb)&reorganization(Y,Ta,Tc)&reorganization_type(X,Re,Ta)&reorganization_type(Y,Re,Ta)&complexity(X,C1,Ta)&complexity(Y,C2,Ta)&greater(C2,C1))=>greater(Tc,Tb)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t15_FOL)).
% 0.12/0.36 fof(t15_FOL_negated, plain, ~(![X,Y,Re,C,C1,C2,Ta,Tb,Tc]:((organization(X,Ta)&organization(Y,Ta)&organization(Y,Tc)&class(X,C,Ta)&class(Y,C,Ta)&reorganization(X,Ta,Tb)&reorganization(Y,Ta,Tc)&reorganization_type(X,Re,Ta)&reorganization_type(Y,Re,Ta)&complexity(X,C1,Ta)&complexity(Y,C2,Ta)&greater(C2,C1))=>greater(Tc,Tb))), inference(negate_conjecture, [status(cth)], [t15_FOL])).
% 0.12/0.36 cnf(3, plain, organization(sK2,sK8), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 % launching worker at depth: cnf(l0, plain, organization(sK2,sK8), inference(instantiation, [status(thm)], [3])).
% 0.12/0.36 10fof(mp5, plain, ![X,T]:(organization(X,T)=>?[I]:inertia(X,I,T)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mp5)).
% 0.12/0.36
% 0.12/0.36 cnf(0, plain, ~organization(X0,X1) | inertia(X0,sK1(X0,X1),X1), inference(cnf, [status(esa)], [mp5])).
% 0.12/0.36 cnf(l1, plain, ~organization(sK2,sK8) | inertia(sK2,sK1(sK2,sK8),sK8), inference(instantiation, [status(thm)], [0])).
% 0.12/0.36 fof(a13_FOL, plain, ![X,Y,Rt,C,I1,I2,Ta,Tb,Tc]:((organization(X,Ta)&organization(Y,Ta)&organization(Y,Tc)&class(X,C,Ta)&class(Y,C,Ta)&reorganization(X,Ta,Tb)&reorganization(Y,Ta,Tc)&reorganization_type(X,Rt,Ta)&reorganization_type(Y,Rt,Ta)&inertia(X,I1,Ta)&inertia(Y,I2,Ta)&greater(I2,I1))=>greater(Tc,Tb)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', a13_FOL)).
% 0.12/0.36 cnf(2, plain, ~class(X0,X1,X2) | ~class(X3,X1,X2) | ~greater(X4,X5) | ~organization(X0,X2) | ~organization(X3,X2) | ~organization(X3,X6) | ~reorganization(X0,X2,X7) | ~reorganization(X3,X2,X6) | ~inertia(X0,X5,X2) | ~inertia(X3,X4,X2) | ~reorganization_type(X0,X8,X2) | ~reorganization_type(X3,X8,X2) | greater(X6,X7), inference(cnf, [status(esa)], [a13_FOL])).
% 0.12/0.36 cnf(l2, plain, ~class(sK2,sK5,sK8) | ~class(sK3,sK5,sK8) | ~greater(sK1(sK3,sK8),sK1(sK2,sK8)) | ~organization(sK2,sK8) | ~organization(sK3,sK8) | ~organization(sK3,sK10) | ~reorganization(sK2,sK8,sK9) | ~reorganization(sK3,sK8,sK10) | ~inertia(sK2,sK1(sK2,sK8),sK8) | ~inertia(sK3,sK1(sK3,sK8),sK8) | ~reorganization_type(sK2,sK4,sK8) | ~reorganization_type(sK3,sK4,sK8) | greater(sK10,sK9), inference(instantiation, [status(thm)], [2])).
% 0.12/0.36 cnf(10, plain, reorganization_type(sK2,sK4,sK8), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l39, plain, reorganization_type(sK2,sK4,sK8), inference(instantiation, [status(thm)], [10])).
% 0.12/0.36 cnf(5, plain, organization(sK3,sK10), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l43, plain, organization(sK3,sK10), inference(instantiation, [status(thm)], [5])).
% 0.12/0.36 cnf(l6, plain, ~organization(sK3,sK8) | inertia(sK3,sK1(sK3,sK8),sK8), inference(instantiation, [status(thm)], [0])).
% 0.12/0.36 cnf(7, plain, class(sK3,sK5,sK8), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l7, plain, class(sK3,sK5,sK8), inference(instantiation, [status(thm)], [7])).
% 0.12/0.36 cnf(4, plain, organization(sK3,sK8), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l9, plain, organization(sK3,sK8), inference(instantiation, [status(thm)], [4])).
% 0.12/0.36 cnf(8, plain, reorganization(sK2,sK8,sK9), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l40, plain, reorganization(sK2,sK8,sK9), inference(instantiation, [status(thm)], [8])).
% 0.12/0.36 cnf(11, plain, reorganization_type(sK3,sK4,sK8), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l38, plain, reorganization_type(sK3,sK4,sK8), inference(instantiation, [status(thm)], [11])).
% 0.12/0.36 fof(a12_FOL, plain, ![X,Y,C,C1,C2,I1,I2,T1,T2]:((organization(X,T1)&organization(Y,T2)&class(X,C,T1)&class(Y,C,T2)&complexity(X,C1,T1)&complexity(Y,C2,T2)&inertia(X,I1,T1)&inertia(Y,I2,T2)&greater(C2,C1))=>greater(I2,I1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', a12_FOL)).
% 0.12/0.36 cnf(1, plain, ~class(X0,X1,X2) | ~class(X3,X1,X4) | ~complexity(X0,X5,X2) | ~complexity(X3,X6,X4) | ~greater(X6,X5) | ~organization(X0,X2) | ~organization(X3,X4) | ~inertia(X0,X7,X2) | ~inertia(X3,X8,X4) | greater(X8,X7), inference(cnf, [status(esa)], [a12_FOL])).
% 0.12/0.36 cnf(l3, plain, ~class(sK2,sK5,sK8) | ~class(sK3,sK5,sK8) | ~complexity(sK2,sK6,sK8) | ~complexity(sK3,sK7,sK8) | ~greater(sK7,sK6) | ~organization(sK2,sK8) | ~organization(sK3,sK8) | ~inertia(sK2,sK1(sK2,sK8),sK8) | ~inertia(sK3,sK1(sK3,sK8),sK8) | greater(sK1(sK3,sK8),sK1(sK2,sK8)), inference(instantiation, [status(thm)], [1])).
% 0.12/0.36 cnf(13, plain, complexity(sK3,sK7,sK8), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l55, plain, complexity(sK3,sK7,sK8), inference(instantiation, [status(thm)], [13])).
% 0.12/0.36 cnf(6, plain, class(sK2,sK5,sK8), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l4, plain, class(sK2,sK5,sK8), inference(instantiation, [status(thm)], [6])).
% 0.12/0.36 cnf(l56, plain, ~organization(sK3,sK8) | inertia(sK3,sK1(sK3,sK8),sK8), inference(instantiation, [status(thm)], [0])).
% 0.12/0.36 cnf(l13, plain, organization(sK3,sK8), inference(instantiation, [status(thm)], [4])).
% 0.12/0.36 cnf(l57, plain, class(sK2,sK5,sK8), inference(instantiation, [status(thm)], [6])).
% 0.12/0.36 cnf(l58, plain, organization(sK3,sK8), inference(instantiation, [status(thm)], [4])).
% 0.12/0.36 cnf(l59, plain, class(sK3,sK5,sK8), inference(instantiation, [status(thm)], [7])).
% 0.12/0.36 cnf(14, plain, greater(sK7,sK6), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l60, plain, greater(sK7,sK6), inference(instantiation, [status(thm)], [14])).
% 0.12/0.36 cnf(l73, plain, organization(sK3,sK8), inference(instantiation, [status(thm)], [4])).
% 0.12/0.36 cnf(12, plain, complexity(sK2,sK6,sK8), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l70, plain, complexity(sK2,sK6,sK8), inference(instantiation, [status(thm)], [12])).
% 0.12/0.36 cnf(15, plain, ~greater(sK10,sK9), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l44, plain, ~greater(sK10,sK9), inference(instantiation, [status(thm)], [15])).
% 0.12/0.36 cnf(9, plain, reorganization(sK3,sK8,sK10), inference(cnf, [status(esa)], [t15_FOL_negated])).
% 0.12/0.36 cnf(l42, plain, reorganization(sK3,sK8,sK10), inference(instantiation, [status(thm)], [9])).
% 0.12/0.36 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l2, l39, l43, l6, l7, l9, l40, l38, l3, l55, l4, l56, l13, l57, l58, l59, l60, l73, l70, l44, l42])).
% 0.12/0.36 % SZS output end CNFRefutation
%------------------------------------------------------------------------------