%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT015-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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 : Fri Sep 25 02:11:18 PM UTC 2026
% Result : Unsatisfiable 19.76s 2.99s
% Output : Proof 19.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 17
% Syntax : Number of formulae : 145 ( 133 unt; 0 def)
% Number of atoms : 233 ( 92 equ)
% Maximal formula atoms : 13 ( 1 avg)
% Number of connectives : 182 ( 94 ~; 88 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 2 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-4 aty)
% Number of variables : 274 ( 2 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f2,hypothesis,
( greater(D,F)
| ~ greater(I,H)
| ~ inertia(C,I,B)
| ~ inertia(A,H,B)
| ~ reorganization_type(C,G,B)
| ~ reorganization_type(A,G,B)
| ~ reorganization(C,B,D)
| ~ reorganization(A,B,F)
| ~ class(C,E,B)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(C,B)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a13_FOL_3) ).
fof(f2_nnf,plain,
! [A,B,C,D,E,F,G,H,I] :
( greater(D,F)
| ~ greater(I,H)
| ~ inertia(C,I,B)
| ~ inertia(A,H,B)
| ~ reorganization_type(C,G,B)
| ~ reorganization_type(A,G,B)
| ~ reorganization(C,B,D)
| ~ reorganization(A,B,F)
| ~ class(C,E,B)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(C,B)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B,C,D,E,F,G,H,I] :
( greater(D,F)
| ~ greater(I,H)
| ~ inertia(C,I,B)
| ~ inertia(A,H,B)
| ~ reorganization_type(C,G,B)
| ~ reorganization_type(A,G,B)
| ~ reorganization(C,B,D)
| ~ reorganization(A,B,F)
| ~ class(C,E,B)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(C,B)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( greater(X3,X5)
| ~ greater(X8,X7)
| ~ inertia(X2,X8,X1)
| ~ inertia(X0,X7,X1)
| ~ reorganization_type(X2,X6,X1)
| ~ reorganization_type(X0,X6,X1)
| ~ reorganization(X2,X1,X3)
| ~ reorganization(X0,X1,X5)
| ~ class(X2,X4,X1)
| ~ class(X0,X4,X1)
| ~ organization(X2,X3)
| ~ organization(X2,X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t15,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X2),true,ifeq(organization(X3,X4),true,ifeq(class(X1,X5,X2),true,ifeq(class(X3,X5,X2),true,ifeq(reorganization(X1,X2,X6),true,ifeq(reorganization(X3,X2,X4),true,ifeq(reorganization_type(X1,X7,X2),true,ifeq(reorganization_type(X3,X7,X2),true,ifeq(inertia(X1,X8,X2),true,ifeq(inertia(X3,X9,X2),true,ifeq(greater(X9,X8),true,greater(X4,X6),true),true),true),true),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t79,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X2),true,ifeq(organization(X3,X4),true,ifeq(class(X1,X5,X2),true,ifeq(class(X3,X5,X2),true,ifeq(reorganization(X1,X2,X6),true,ifeq(reorganization(X3,X2,X4),true,ifeq(reorganization_type(X1,X7,X2),true,ifeq(reorganization_type(X3,X7,X2),true,ifeq(inertia(X1,X8,X2),true,ifeq(inertia(X3,X9,X2),true,ifeq(greater(X9,X8),true,greater(X4,X6),true),true),true),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(f5,negated_conjecture,
organization(sk3,sk10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_6) ).
fof(f5_nnf,plain,
organization(sk3,sk10),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
organization(sk3,sk10),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(t2,plain,
organization(sk3,sk10) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t18,plain,
organization(sk3,sk10) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t87,plain,
true = ifeq(organization(X1,X2),true,ifeq(organization(sk3,X2),true,ifeq(true,true,ifeq(class(X1,X3,X2),true,ifeq(class(sk3,X3,X2),true,ifeq(reorganization(X1,X2,X4),true,ifeq(reorganization(sk3,X2,sk10),true,ifeq(reorganization_type(X1,X5,X2),true,ifeq(reorganization_type(sk3,X5,X2),true,ifeq(inertia(X1,X6,X2),true,ifeq(inertia(sk3,X7,X2),true,ifeq(greater(X7,X6),true,greater(sk10,X4),true),true),true),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t79,t18]) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t28,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t1828,plain,
true = ifeq(organization(X1,X2),true,ifeq(organization(sk3,X2),true,ifeq(class(X1,X3,X2),true,ifeq(class(sk3,X3,X2),true,ifeq(reorganization(X1,X2,X4),true,ifeq(reorganization(sk3,X2,sk10),true,ifeq(reorganization_type(X1,X5,X2),true,ifeq(reorganization_type(sk3,X5,X2),true,ifeq(inertia(X1,X6,X2),true,ifeq(inertia(sk3,X7,X2),true,ifeq(greater(X7,X6),true,greater(sk10,X4),true),true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t87,t28]) ).
cnf(t1037,plain,
ifeq(organization(X1,X2),true,ifeq(organization(sk3,X2),true,ifeq(class(X1,X3,X2),true,ifeq(class(sk3,X3,X2),true,ifeq(reorganization(X1,X2,X4),true,ifeq(reorganization(sk3,X2,sk10),true,ifeq(reorganization_type(X1,X5,X2),true,ifeq(reorganization_type(sk3,X5,X2),true,ifeq(inertia(X1,X6,X2),true,ifeq(inertia(sk3,X7,X2),true,ifeq(greater(X7,X6),true,greater(sk10,X4),true),true),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t1828]) ).
cnf(f6,negated_conjecture,
class(sk2,sk5,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_7) ).
fof(f6_nnf,plain,
class(sk2,sk5,sk8),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
class(sk2,sk5,sk8),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t4,plain,
class(sk2,sk5,sk8) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t20,plain,
class(sk2,sk5,sk8) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t1039,plain,
true = ifeq(organization(sk2,sk8),true,ifeq(organization(sk3,sk8),true,ifeq(true,true,ifeq(class(sk3,sk5,sk8),true,ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization(sk3,sk8,sk10),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t1037,t20]) ).
cnf(f3,negated_conjecture,
organization(sk2,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_4) ).
fof(f3_nnf,plain,
organization(sk2,sk8),
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
organization(sk2,sk8),
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(t1,plain,
organization(sk2,sk8) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t17,plain,
organization(sk2,sk8) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t1852,plain,
true = ifeq(true,true,ifeq(organization(sk3,sk8),true,ifeq(true,true,ifeq(class(sk3,sk5,sk8),true,ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization(sk3,sk8,sk10),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1039,t17]) ).
cnf(t1853,plain,
true = ifeq(organization(sk3,sk8),true,ifeq(true,true,ifeq(class(sk3,sk5,sk8),true,ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization(sk3,sk8,sk10),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1852,t28]) ).
cnf(f4,negated_conjecture,
organization(sk3,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_5) ).
fof(f4_nnf,plain,
organization(sk3,sk8),
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
organization(sk3,sk8),
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(t3,plain,
organization(sk3,sk8) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t19,plain,
organization(sk3,sk8) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t1854,plain,
true = ifeq(true,true,ifeq(true,true,ifeq(class(sk3,sk5,sk8),true,ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization(sk3,sk8,sk10),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1853,t19]) ).
cnf(t1855,plain,
true = ifeq(true,true,ifeq(class(sk3,sk5,sk8),true,ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization(sk3,sk8,sk10),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1854,t28]) ).
cnf(t1856,plain,
true = ifeq(class(sk3,sk5,sk8),true,ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization(sk3,sk8,sk10),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1855,t28]) ).
cnf(f7,negated_conjecture,
class(sk3,sk5,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_8) ).
fof(f7_nnf,plain,
class(sk3,sk5,sk8),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
class(sk3,sk5,sk8),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(t5,plain,
class(sk3,sk5,sk8) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t21,plain,
class(sk3,sk5,sk8) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t1857,plain,
true = ifeq(true,true,ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization(sk3,sk8,sk10),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1856,t21]) ).
cnf(t1858,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization(sk3,sk8,sk10),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1857,t28]) ).
cnf(f9,negated_conjecture,
reorganization(sk3,sk8,sk10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_10) ).
fof(f9_nnf,plain,
reorganization(sk3,sk8,sk10),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
reorganization(sk3,sk8,sk10),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t9,plain,
reorganization(sk3,sk8,sk10) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t25,plain,
reorganization(sk3,sk8,sk10) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t1859,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(true,true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1858,t25]) ).
cnf(t1860,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true),
inference(step,[status(thm)],[t1859,t28]) ).
cnf(t1116,plain,
ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,X3,sk8),true,ifeq(inertia(sk3,X4,sk8),true,ifeq(greater(X4,X3),true,greater(sk10,X1),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t1860]) ).
cnf(f1,hypothesis,
( greater(I,H)
| ~ greater(G,F)
| ~ inertia(C,I,D)
| ~ inertia(A,H,B)
| ~ complexity(C,G,D)
| ~ complexity(A,F,B)
| ~ class(C,E,D)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a12_FOL_2) ).
fof(f1_nnf,plain,
! [A,B,C,D,E,F,G,H,I] :
( greater(I,H)
| ~ greater(G,F)
| ~ inertia(C,I,D)
| ~ inertia(A,H,B)
| ~ complexity(C,G,D)
| ~ complexity(A,F,B)
| ~ class(C,E,D)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C,D,E,F,G,H,I] :
( greater(I,H)
| ~ greater(G,F)
| ~ inertia(C,I,D)
| ~ inertia(A,H,B)
| ~ complexity(C,G,D)
| ~ complexity(A,F,B)
| ~ class(C,E,D)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( greater(X8,X7)
| ~ greater(X6,X5)
| ~ inertia(X2,X8,X3)
| ~ inertia(X0,X7,X1)
| ~ complexity(X2,X6,X3)
| ~ complexity(X0,X5,X1)
| ~ class(X2,X4,X3)
| ~ class(X0,X4,X1)
| ~ organization(X2,X3)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t14,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(class(X1,X5,X2),true,ifeq(class(X3,X5,X4),true,ifeq(complexity(X1,X6,X2),true,ifeq(complexity(X3,X7,X4),true,ifeq(inertia(X1,X8,X2),true,ifeq(inertia(X3,X9,X4),true,ifeq(greater(X7,X6),true,greater(X9,X8),true),true),true),true),true),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t36,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X3,X4),true,ifeq(class(X1,X5,X2),true,ifeq(class(X3,X5,X4),true,ifeq(complexity(X1,X6,X2),true,ifeq(complexity(X3,X7,X4),true,ifeq(inertia(X1,X8,X2),true,ifeq(inertia(X3,X9,X4),true,ifeq(greater(X7,X6),true,greater(X9,X8),true),true),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t14]) ).
cnf(t45,plain,
true = ifeq(organization(sk2,sk8),true,ifeq(organization(X1,X2),true,ifeq(true,true,ifeq(class(X1,sk5,X2),true,ifeq(complexity(sk2,X3,sk8),true,ifeq(complexity(X1,X4,X2),true,ifeq(inertia(sk2,X5,sk8),true,ifeq(inertia(X1,X6,X2),true,ifeq(greater(X4,X3),true,greater(X6,X5),true),true),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t36,t20]) ).
cnf(t1292,plain,
true = ifeq(true,true,ifeq(organization(X1,X2),true,ifeq(true,true,ifeq(class(X1,sk5,X2),true,ifeq(complexity(sk2,X3,sk8),true,ifeq(complexity(X1,X4,X2),true,ifeq(inertia(sk2,X5,sk8),true,ifeq(inertia(X1,X6,X2),true,ifeq(greater(X4,X3),true,greater(X6,X5),true),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t45,t17]) ).
cnf(t1293,plain,
true = ifeq(organization(X1,X2),true,ifeq(true,true,ifeq(class(X1,sk5,X2),true,ifeq(complexity(sk2,X3,sk8),true,ifeq(complexity(X1,X4,X2),true,ifeq(inertia(sk2,X5,sk8),true,ifeq(inertia(X1,X6,X2),true,ifeq(greater(X4,X3),true,greater(X6,X5),true),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1292,t28]) ).
cnf(t1294,plain,
true = ifeq(organization(X1,X2),true,ifeq(class(X1,sk5,X2),true,ifeq(complexity(sk2,X3,sk8),true,ifeq(complexity(X1,X4,X2),true,ifeq(inertia(sk2,X5,sk8),true,ifeq(inertia(X1,X6,X2),true,ifeq(greater(X4,X3),true,greater(X6,X5),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t1293,t28]) ).
cnf(t59,plain,
ifeq(organization(X1,X2),true,ifeq(class(X1,sk5,X2),true,ifeq(complexity(sk2,X3,sk8),true,ifeq(complexity(X1,X4,X2),true,ifeq(inertia(sk2,X5,sk8),true,ifeq(inertia(X1,X6,X2),true,ifeq(greater(X4,X3),true,greater(X6,X5),true),true),true),true),true),true),true) = true,
inference(orient,[status(thm)],[t1294]) ).
cnf(f13,negated_conjecture,
complexity(sk3,sk7,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_14) ).
fof(f13_nnf,plain,
complexity(sk3,sk7,sk8),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
complexity(sk3,sk7,sk8),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t7,plain,
complexity(sk3,sk7,sk8) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t23,plain,
complexity(sk3,sk7,sk8) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t67,plain,
true = ifeq(organization(sk3,sk8),true,ifeq(class(sk3,sk5,sk8),true,ifeq(complexity(sk2,X1,sk8),true,ifeq(true,true,ifeq(inertia(sk2,X2,sk8),true,ifeq(inertia(sk3,X3,sk8),true,ifeq(greater(sk7,X1),true,greater(X3,X2),true),true),true),true),true),true),true),
inference(cp,[status(thm)],[t59,t23]) ).
cnf(t1313,plain,
true = ifeq(true,true,ifeq(class(sk3,sk5,sk8),true,ifeq(complexity(sk2,X1,sk8),true,ifeq(true,true,ifeq(inertia(sk2,X2,sk8),true,ifeq(inertia(sk3,X3,sk8),true,ifeq(greater(sk7,X1),true,greater(X3,X2),true),true),true),true),true),true),true),
inference(step,[status(thm)],[t67,t19]) ).
cnf(t1314,plain,
true = ifeq(class(sk3,sk5,sk8),true,ifeq(complexity(sk2,X1,sk8),true,ifeq(true,true,ifeq(inertia(sk2,X2,sk8),true,ifeq(inertia(sk3,X3,sk8),true,ifeq(greater(sk7,X1),true,greater(X3,X2),true),true),true),true),true),true),
inference(step,[status(thm)],[t1313,t28]) ).
cnf(t1315,plain,
true = ifeq(true,true,ifeq(complexity(sk2,X1,sk8),true,ifeq(true,true,ifeq(inertia(sk2,X2,sk8),true,ifeq(inertia(sk3,X3,sk8),true,ifeq(greater(sk7,X1),true,greater(X3,X2),true),true),true),true),true),true),
inference(step,[status(thm)],[t1314,t21]) ).
cnf(t1316,plain,
true = ifeq(complexity(sk2,X1,sk8),true,ifeq(true,true,ifeq(inertia(sk2,X2,sk8),true,ifeq(inertia(sk3,X3,sk8),true,ifeq(greater(sk7,X1),true,greater(X3,X2),true),true),true),true),true),
inference(step,[status(thm)],[t1315,t28]) ).
cnf(t1317,plain,
true = ifeq(complexity(sk2,X1,sk8),true,ifeq(inertia(sk2,X2,sk8),true,ifeq(inertia(sk3,X3,sk8),true,ifeq(greater(sk7,X1),true,greater(X3,X2),true),true),true),true),
inference(step,[status(thm)],[t1316,t28]) ).
cnf(t130,plain,
ifeq(complexity(sk2,X1,sk8),true,ifeq(inertia(sk2,X2,sk8),true,ifeq(inertia(sk3,X3,sk8),true,ifeq(greater(sk7,X1),true,greater(X3,X2),true),true),true),true) = true,
inference(orient,[status(thm)],[t1317]) ).
cnf(f14,negated_conjecture,
greater(sk7,sk6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_15) ).
fof(f14_nnf,plain,
greater(sk7,sk6),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
greater(sk7,sk6),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t0,plain,
greater(sk7,sk6) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t16,plain,
greater(sk7,sk6) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t131,plain,
true = ifeq(complexity(sk2,sk6,sk8),true,ifeq(inertia(sk2,X1,sk8),true,ifeq(inertia(sk3,X2,sk8),true,ifeq(true,true,greater(X2,X1),true),true),true),true),
inference(cp,[status(thm)],[t130,t16]) ).
cnf(f12,negated_conjecture,
complexity(sk2,sk6,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_13) ).
fof(f12_nnf,plain,
complexity(sk2,sk6,sk8),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
complexity(sk2,sk6,sk8),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t6,plain,
complexity(sk2,sk6,sk8) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t22,plain,
complexity(sk2,sk6,sk8) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t1319,plain,
true = ifeq(true,true,ifeq(inertia(sk2,X1,sk8),true,ifeq(inertia(sk3,X2,sk8),true,ifeq(true,true,greater(X2,X1),true),true),true),true),
inference(step,[status(thm)],[t131,t22]) ).
cnf(t1320,plain,
true = ifeq(inertia(sk2,X1,sk8),true,ifeq(inertia(sk3,X2,sk8),true,ifeq(true,true,greater(X2,X1),true),true),true),
inference(step,[status(thm)],[t1319,t28]) ).
cnf(t1321,plain,
true = ifeq(inertia(sk2,X1,sk8),true,ifeq(inertia(sk3,X2,sk8),true,greater(X2,X1),true),true),
inference(step,[status(thm)],[t1320,t28]) ).
cnf(t152,plain,
ifeq(inertia(sk2,X1,sk8),true,ifeq(inertia(sk3,X2,sk8),true,greater(X2,X1),true),true) = true,
inference(orient,[status(thm)],[t1321]) ).
cnf(f0,axiom,
( inertia(A,sk1(B,A),B)
| ~ organization(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp5_1) ).
fof(f0_nnf,plain,
! [A,B] :
( inertia(A,sk1(B,A),B)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( inertia(A,sk1(B,A),B)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( inertia(X0,sk1(X1,X0),X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t13,plain,
ifeq(organization(X1,X2),true,inertia(X1,sk1(X2,X1),X2),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t29,plain,
ifeq(organization(X1,X2),true,inertia(X1,sk1(X2,X1),X2),true) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t30,plain,
true = ifeq(true,true,inertia(sk2,sk1(sk8,sk2),sk8),true),
inference(cp,[status(thm)],[t29,t17]) ).
cnf(t1289,plain,
true = inertia(sk2,sk1(sk8,sk2),sk8),
inference(step,[status(thm)],[t30,t28]) ).
cnf(t33,plain,
inertia(sk2,sk1(sk8,sk2),sk8) = true,
inference(orient,[status(thm)],[t1289]) ).
cnf(t154,plain,
true = ifeq(true,true,ifeq(inertia(sk3,X1,sk8),true,greater(X1,sk1(sk8,sk2)),true),true),
inference(cp,[status(thm)],[t152,t33]) ).
cnf(t1322,plain,
true = ifeq(inertia(sk3,X1,sk8),true,greater(X1,sk1(sk8,sk2)),true),
inference(step,[status(thm)],[t154,t28]) ).
cnf(t157,plain,
ifeq(inertia(sk3,X1,sk8),true,greater(X1,sk1(sk8,sk2)),true) = true,
inference(orient,[status(thm)],[t1322]) ).
cnf(t32,plain,
true = ifeq(true,true,inertia(sk3,sk1(sk8,sk3),sk8),true),
inference(cp,[status(thm)],[t29,t19]) ).
cnf(t1291,plain,
true = inertia(sk3,sk1(sk8,sk3),sk8),
inference(step,[status(thm)],[t32,t28]) ).
cnf(t35,plain,
inertia(sk3,sk1(sk8,sk3),sk8) = true,
inference(orient,[status(thm)],[t1291]) ).
cnf(t158,plain,
true = ifeq(true,true,greater(sk1(sk8,sk3),sk1(sk8,sk2)),true),
inference(cp,[status(thm)],[t157,t35]) ).
cnf(t1323,plain,
true = greater(sk1(sk8,sk3),sk1(sk8,sk2)),
inference(step,[status(thm)],[t158,t28]) ).
cnf(t160,plain,
greater(sk1(sk8,sk3),sk1(sk8,sk2)) = true,
inference(orient,[status(thm)],[t1323]) ).
cnf(t1122,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk2,sk1(sk8,sk2),sk8),true,ifeq(inertia(sk3,sk1(sk8,sk3),sk8),true,ifeq(true,true,greater(sk10,X1),true),true),true),true),true),true),
inference(cp,[status(thm)],[t1116,t160]) ).
cnf(t1861,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(true,true,ifeq(inertia(sk3,sk1(sk8,sk3),sk8),true,ifeq(true,true,greater(sk10,X1),true),true),true),true),true),true),
inference(step,[status(thm)],[t1122,t33]) ).
cnf(t1862,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(inertia(sk3,sk1(sk8,sk3),sk8),true,ifeq(true,true,greater(sk10,X1),true),true),true),true),true),
inference(step,[status(thm)],[t1861,t28]) ).
cnf(t1863,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(true,true,ifeq(true,true,greater(sk10,X1),true),true),true),true),true),
inference(step,[status(thm)],[t1862,t35]) ).
cnf(t1864,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,ifeq(true,true,greater(sk10,X1),true),true),true),true),
inference(step,[status(thm)],[t1863,t28]) ).
cnf(t1865,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,greater(sk10,X1),true),true),true),
inference(step,[status(thm)],[t1864,t28]) ).
cnf(t1123,plain,
ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk2,X2,sk8),true,ifeq(reorganization_type(sk3,X2,sk8),true,greater(sk10,X1),true),true),true) = true,
inference(orient,[status(thm)],[t1865]) ).
cnf(f10,negated_conjecture,
reorganization_type(sk2,sk4,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_11) ).
fof(f10_nnf,plain,
reorganization_type(sk2,sk4,sk8),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
reorganization_type(sk2,sk4,sk8),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t10,plain,
reorganization_type(sk2,sk4,sk8) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t26,plain,
reorganization_type(sk2,sk4,sk8) = true,
inference(orient,[status(thm)],[t10]) ).
cnf(t1125,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(true,true,ifeq(reorganization_type(sk3,sk4,sk8),true,greater(sk10,X1),true),true),true),
inference(cp,[status(thm)],[t1123,t26]) ).
cnf(t1866,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(reorganization_type(sk3,sk4,sk8),true,greater(sk10,X1),true),true),
inference(step,[status(thm)],[t1125,t28]) ).
cnf(f11,negated_conjecture,
reorganization_type(sk3,sk4,sk8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_12) ).
fof(f11_nnf,plain,
reorganization_type(sk3,sk4,sk8),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
reorganization_type(sk3,sk4,sk8),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t11,plain,
reorganization_type(sk3,sk4,sk8) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t27,plain,
reorganization_type(sk3,sk4,sk8) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t1867,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,ifeq(true,true,greater(sk10,X1),true),true),
inference(step,[status(thm)],[t1866,t27]) ).
cnf(t1868,plain,
true = ifeq(reorganization(sk2,sk8,X1),true,greater(sk10,X1),true),
inference(step,[status(thm)],[t1867,t28]) ).
cnf(t1126,plain,
ifeq(reorganization(sk2,sk8,X1),true,greater(sk10,X1),true) = true,
inference(orient,[status(thm)],[t1868]) ).
cnf(f8,negated_conjecture,
reorganization(sk2,sk8,sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_9) ).
fof(f8_nnf,plain,
reorganization(sk2,sk8,sk9),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
reorganization(sk2,sk8,sk9),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t8,plain,
reorganization(sk2,sk8,sk9) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t24,plain,
reorganization(sk2,sk8,sk9) = true,
inference(orient,[status(thm)],[t8]) ).
cnf(t1127,plain,
true = ifeq(true,true,greater(sk10,sk9),true),
inference(cp,[status(thm)],[t1126,t24]) ).
cnf(t1869,plain,
true = greater(sk10,sk9),
inference(step,[status(thm)],[t1127,t28]) ).
cnf(t1128,plain,
greater(sk10,sk9) = true,
inference(orient,[status(thm)],[t1869]) ).
cnf(f15,negated_conjecture,
~ greater(sk10,sk9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_FOL_16) ).
fof(f15_nnf,plain,
~ greater(sk10,sk9),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
~ greater(sk10,sk9),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
~ greater(sk10,sk9),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(goal_0,negated_conjecture,
greater(sk10,sk9) != true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1128]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT015-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n018.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 : Thu Sep 24 01:02:48 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 19.76/2.99 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.76/2.99 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------