%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MGT013-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:17 PM UTC 2026
% Result : Unsatisfiable 5.79s 6.32s
% Output : Proof 5.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 24
% Syntax : Number of formulae : 199 ( 167 unt; 0 def)
% Number of atoms : 299 ( 155 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 210 ( 110 ~; 100 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-4 aty)
% Number of variables : 218 ( 5 sgn 52 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t20,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t186,plain,
ifeq(not(X1),true,X1,false) = false,
inference(orient,[status(thm)],[t20]) ).
cnf(f0,axiom,
( A != B
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp6_1_18) ).
fof(f0_nnf,plain,
! [A,B] :
( A != B
| ~ greater(A,B) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] :
( A != B
| ~ greater(A,B) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( X0 != X1
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t23,plain,
or(not(greater(X1,X2)),not(eq(X1,X2))) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t77,plain,
or(not(greater(X1,X2)),not(eq(X1,X2))) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(f15,negated_conjecture,
greater(sk3,sk2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_33) ).
fof(f15_nnf,plain,
greater(sk3,sk2),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
greater(sk3,sk2),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(t5,plain,
greater(sk3,sk2) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t97,plain,
greater(sk3,sk2) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t101,plain,
true = or(not(true),not(eq(sk3,sk2))),
inference(cp,[status(thm)],[t77,t97]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t188,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t999,plain,
true = or(false,not(eq(sk3,sk2))),
inference(step,[status(thm)],[t101,t188]) ).
cnf(t9,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t45,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t1000,plain,
true = not(eq(sk3,sk2)),
inference(step,[status(thm)],[t999,t45]) ).
cnf(t235,plain,
not(eq(sk3,sk2)) = true,
inference(orient,[status(thm)],[t1000]) ).
cnf(t236,plain,
false = ifeq(true,true,eq(sk3,sk2),false),
inference(cp,[status(thm)],[t186,t235]) ).
cnf(t19,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t38,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t19]) ).
cnf(t1001,plain,
false = eq(sk3,sk2),
inference(step,[status(thm)],[t236,t38]) ).
cnf(t247,plain,
eq(sk3,sk2) = false,
inference(orient,[status(thm)],[t1001]) ).
cnf(f5,axiom,
( D = E
| B != C
| ~ complexity(A,E,C)
| ~ complexity(A,D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp18_23) ).
fof(f5_nnf,plain,
! [A,B,C,D,E] :
( D = E
| B != C
| ~ complexity(A,E,C)
| ~ complexity(A,D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C,D,E] :
( D = E
| B != C
| ~ complexity(A,E,C)
| ~ complexity(A,D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( X3 = X4
| X1 != X2
| ~ complexity(X0,X4,X2)
| ~ complexity(X0,X3,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t33,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X1,X3),true,ifeq(complexity(X1,X4,X2),true,ifeq(complexity(X1,X5,X3),true,ifeq(X2,X3,X4,X5),X5),X5),X5),X5) = X5,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t39,plain,
ifeq(organization(X1,X2),true,ifeq(organization(X1,X3),true,ifeq(complexity(X1,X4,X2),true,ifeq(complexity(X1,X5,X3),true,ifeq(X2,X3,X4,X5),X5),X5),X5),X5) = X5,
inference(orient,[status(thm)],[t33]) ).
cnf(f12,negated_conjecture,
complexity(sk1,sk3,sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_30) ).
fof(f12_nnf,plain,
complexity(sk1,sk3,sk7),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
complexity(sk1,sk3,sk7),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(t14,plain,
complexity(sk1,sk3,sk7) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t154,plain,
complexity(sk1,sk3,sk7) = true,
inference(orient,[status(thm)],[t14]) ).
cnf(t156,plain,
sk3 = ifeq(organization(sk1,X1),true,ifeq(organization(sk1,sk7),true,ifeq(complexity(sk1,X2,X1),true,ifeq(true,true,ifeq(X1,sk7,X2,sk3),sk3),sk3),sk3),sk3),
inference(cp,[status(thm)],[t39,t154]) ).
cnf(f9,negated_conjecture,
organization(sk1,sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_27) ).
fof(f9_nnf,plain,
organization(sk1,sk7),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
organization(sk1,sk7),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(t12,plain,
organization(sk1,sk7) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t127,plain,
organization(sk1,sk7) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(t1057,plain,
sk3 = ifeq(organization(sk1,X1),true,ifeq(true,true,ifeq(complexity(sk1,X2,X1),true,ifeq(true,true,ifeq(X1,sk7,X2,sk3),sk3),sk3),sk3),sk3),
inference(step,[status(thm)],[t156,t127]) ).
cnf(t1058,plain,
sk3 = ifeq(organization(sk1,X1),true,ifeq(complexity(sk1,X2,X1),true,ifeq(true,true,ifeq(X1,sk7,X2,sk3),sk3),sk3),sk3),
inference(step,[status(thm)],[t1057,t38]) ).
cnf(t1059,plain,
sk3 = ifeq(organization(sk1,X1),true,ifeq(complexity(sk1,X2,X1),true,ifeq(X1,sk7,X2,sk3),sk3),sk3),
inference(step,[status(thm)],[t1058,t38]) ).
cnf(t337,plain,
ifeq(organization(sk1,X1),true,ifeq(complexity(sk1,X2,X1),true,ifeq(X1,sk7,X2,sk3),sk3),sk3) = sk3,
inference(orient,[status(thm)],[t1059]) ).
cnf(f11,negated_conjecture,
complexity(sk1,sk2,sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_29) ).
fof(f11_nnf,plain,
complexity(sk1,sk2,sk6),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
complexity(sk1,sk2,sk6),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(t13,plain,
complexity(sk1,sk2,sk6) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t161,plain,
complexity(sk1,sk2,sk6) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t339,plain,
sk3 = ifeq(organization(sk1,sk6),true,ifeq(true,true,ifeq(sk6,sk7,sk2,sk3),sk3),sk3),
inference(cp,[status(thm)],[t337,t161]) ).
cnf(f8,negated_conjecture,
organization(sk1,sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_26) ).
fof(f8_nnf,plain,
organization(sk1,sk6),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
organization(sk1,sk6),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(t11,plain,
organization(sk1,sk6) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t115,plain,
organization(sk1,sk6) = true,
inference(orient,[status(thm)],[t11]) ).
cnf(t1060,plain,
sk3 = ifeq(true,true,ifeq(true,true,ifeq(sk6,sk7,sk2,sk3),sk3),sk3),
inference(step,[status(thm)],[t339,t115]) ).
cnf(t1061,plain,
sk3 = ifeq(true,true,ifeq(sk6,sk7,sk2,sk3),sk3),
inference(step,[status(thm)],[t1060,t38]) ).
cnf(t1062,plain,
sk3 = ifeq(sk6,sk7,sk2,sk3),
inference(step,[status(thm)],[t1061,t38]) ).
cnf(t341,plain,
ifeq(sk6,sk7,sk2,sk3) = sk3,
inference(orient,[status(thm)],[t1062]) ).
cnf(t21,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t42,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t21]) ).
cnf(f3,axiom,
( greater(B,A)
| A = B
| greater(A,B)
| ~ time(B)
| ~ time(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp16_21) ).
fof(f3_nnf,plain,
! [A,B] :
( greater(B,A)
| A = B
| greater(A,B)
| ~ time(B)
| ~ time(A) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] :
( greater(B,A)
| A = B
| greater(A,B)
| ~ time(B)
| ~ time(A) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( greater(X1,X0)
| X0 = X1
| greater(X0,X1)
| ~ time(X1)
| ~ time(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t32,plain,
ifeq(time(X1),true,ifeq(time(X2),true,or(greater(X1,X2),or(eq(X1,X2),greater(X2,X1))),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t64,plain,
ifeq(time(X1),true,ifeq(time(X2),true,or(greater(X1,X2),or(eq(X1,X2),greater(X2,X1))),true),true) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(f2,axiom,
( time(B)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp15_20) ).
fof(f2_nnf,plain,
! [A,B] :
( time(B)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] :
( time(B)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( time(X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi0,axiom,
ifeq(organization(X0,X1),true,time(X1),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(hi5,negated_conjecture,
organization(sk1,sk7) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t3,plain,
time(sk7) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi5]) ).
cnf(t182,plain,
time(sk7) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t185,plain,
true = ifeq(time(X1),true,ifeq(true,true,or(greater(X1,sk7),or(eq(X1,sk7),greater(sk7,X1))),true),true),
inference(cp,[status(thm)],[t64,t182]) ).
cnf(t1049,plain,
true = ifeq(time(X1),true,or(greater(X1,sk7),or(eq(X1,sk7),greater(sk7,X1))),true),
inference(step,[status(thm)],[t185,t38]) ).
cnf(t323,plain,
ifeq(time(X1),true,or(greater(X1,sk7),or(eq(X1,sk7),greater(sk7,X1))),true) = true,
inference(orient,[status(thm)],[t1049]) ).
cnf(f7,hypothesis,
( ~ greater(D,E)
| ~ greater(C,B)
| ~ complexity(A,E,C)
| ~ complexity(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_FOL_25) ).
fof(f7_nnf,plain,
! [A,B,C,D,E] :
( ~ greater(D,E)
| ~ greater(C,B)
| ~ complexity(A,E,C)
| ~ complexity(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B,C,D,E] :
( ~ greater(D,E)
| ~ greater(C,B)
| ~ complexity(A,E,C)
| ~ complexity(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( ~ greater(X3,X4)
| ~ greater(X2,X1)
| ~ complexity(X0,X4,X2)
| ~ complexity(X0,X3,X1)
| ~ reorganization_free(X0,X1,X2)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t34,plain,
or(not(organization(X1,X2)),or(not(organization(X1,X3)),or(not(reorganization_free(X1,X2,X3)),or(not(complexity(X1,X4,X2)),or(not(complexity(X1,X5,X3)),or(not(greater(X3,X2)),not(greater(X4,X5)))))))) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t78,plain,
or(not(organization(X1,X2)),or(not(organization(X1,X3)),or(not(reorganization_free(X1,X2,X3)),or(not(complexity(X1,X4,X2)),or(not(complexity(X1,X5,X3)),or(not(greater(X3,X2)),not(greater(X4,X5)))))))) = true,
inference(orient,[status(thm)],[t34]) ).
cnf(f4,axiom,
( reorganization_free(A,C,B)
| ~ reorganization_free(A,B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp17_22) ).
fof(f4_nnf,plain,
! [A,B,C] :
( reorganization_free(A,C,B)
| ~ reorganization_free(A,B,C) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C] :
( reorganization_free(A,C,B)
| ~ reorganization_free(A,B,C) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( reorganization_free(X0,X2,X1)
| ~ reorganization_free(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi2,axiom,
ifeq(reorganization_free(X0,X1,X2),true,reorganization_free(X0,X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(f10,negated_conjecture,
reorganization_free(sk1,sk6,sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_28) ).
fof(f10_nnf,plain,
reorganization_free(sk1,sk6,sk7),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
reorganization_free(sk1,sk6,sk7),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(hi6,negated_conjecture,
reorganization_free(sk1,sk6,sk7) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t16,plain,
reorganization_free(sk1,sk7,sk6) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi6]) ).
cnf(t149,plain,
reorganization_free(sk1,sk7,sk6) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t152,plain,
true = or(not(organization(sk1,sk7)),or(not(organization(sk1,sk6)),or(not(true),or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2)))))))),
inference(cp,[status(thm)],[t78,t149]) ).
cnf(t1211,plain,
true = or(not(true),or(not(organization(sk1,sk6)),or(not(true),or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2)))))))),
inference(step,[status(thm)],[t152,t127]) ).
cnf(t1212,plain,
true = or(false,or(not(organization(sk1,sk6)),or(not(true),or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2)))))))),
inference(step,[status(thm)],[t1211,t188]) ).
cnf(t1213,plain,
true = or(not(organization(sk1,sk6)),or(not(true),or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2))))))),
inference(step,[status(thm)],[t1212,t45]) ).
cnf(t1214,plain,
true = or(not(true),or(not(true),or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2))))))),
inference(step,[status(thm)],[t1213,t115]) ).
cnf(t1215,plain,
true = or(false,or(not(true),or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2))))))),
inference(step,[status(thm)],[t1214,t188]) ).
cnf(t1216,plain,
true = or(not(true),or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2)))))),
inference(step,[status(thm)],[t1215,t45]) ).
cnf(t1217,plain,
true = or(false,or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2)))))),
inference(step,[status(thm)],[t1216,t188]) ).
cnf(t1218,plain,
true = or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2))))),
inference(step,[status(thm)],[t1217,t45]) ).
cnf(t858,plain,
or(not(complexity(sk1,X1,sk7)),or(not(complexity(sk1,X2,sk6)),or(not(greater(sk6,sk7)),not(greater(X1,X2))))) = true,
inference(orient,[status(thm)],[t1218]) ).
cnf(t862,plain,
true = or(not(complexity(sk1,sk3,sk7)),or(not(complexity(sk1,sk2,sk6)),or(not(greater(sk6,sk7)),not(true)))),
inference(cp,[status(thm)],[t858,t97]) ).
cnf(t1219,plain,
true = or(not(true),or(not(complexity(sk1,sk2,sk6)),or(not(greater(sk6,sk7)),not(true)))),
inference(step,[status(thm)],[t862,t154]) ).
cnf(t1220,plain,
true = or(false,or(not(complexity(sk1,sk2,sk6)),or(not(greater(sk6,sk7)),not(true)))),
inference(step,[status(thm)],[t1219,t188]) ).
cnf(t1221,plain,
true = or(not(complexity(sk1,sk2,sk6)),or(not(greater(sk6,sk7)),not(true))),
inference(step,[status(thm)],[t1220,t45]) ).
cnf(t1222,plain,
true = or(not(true),or(not(greater(sk6,sk7)),not(true))),
inference(step,[status(thm)],[t1221,t161]) ).
cnf(t1223,plain,
true = or(false,or(not(greater(sk6,sk7)),not(true))),
inference(step,[status(thm)],[t1222,t188]) ).
cnf(t1224,plain,
true = or(not(greater(sk6,sk7)),not(true)),
inference(step,[status(thm)],[t1223,t45]) ).
cnf(t1225,plain,
true = or(not(greater(sk6,sk7)),false),
inference(step,[status(thm)],[t1224,t188]) ).
cnf(t7,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t44,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t1226,plain,
true = not(greater(sk6,sk7)),
inference(step,[status(thm)],[t1225,t44]) ).
cnf(t863,plain,
not(greater(sk6,sk7)) = true,
inference(orient,[status(thm)],[t1226]) ).
cnf(t864,plain,
false = ifeq(true,true,greater(sk6,sk7),false),
inference(cp,[status(thm)],[t186,t863]) ).
cnf(t1227,plain,
false = greater(sk6,sk7),
inference(step,[status(thm)],[t864,t38]) ).
cnf(t867,plain,
greater(sk6,sk7) = false,
inference(orient,[status(thm)],[t1227]) ).
cnf(t869,plain,
true = ifeq(time(sk6),true,or(false,or(eq(sk6,sk7),greater(sk7,sk6))),true),
inference(cp,[status(thm)],[t323,t867]) ).
cnf(hi4,negated_conjecture,
organization(sk1,sk6) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t2,plain,
time(sk6) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi4]) ).
cnf(t178,plain,
time(sk6) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t1244,plain,
true = ifeq(true,true,or(false,or(eq(sk6,sk7),greater(sk7,sk6))),true),
inference(step,[status(thm)],[t869,t178]) ).
cnf(t1245,plain,
true = or(false,or(eq(sk6,sk7),greater(sk7,sk6))),
inference(step,[status(thm)],[t1244,t38]) ).
cnf(t1246,plain,
true = or(eq(sk6,sk7),greater(sk7,sk6)),
inference(step,[status(thm)],[t1245,t45]) ).
cnf(f6,hypothesis,
( ~ greater(D,E)
| ~ greater(C,B)
| ~ size(A,E,C)
| ~ size(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t11_FOL_24) ).
fof(f6_nnf,plain,
! [A,B,C,D,E] :
( ~ greater(D,E)
| ~ greater(C,B)
| ~ size(A,E,C)
| ~ size(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C,D,E] :
( ~ greater(D,E)
| ~ greater(C,B)
| ~ size(A,E,C)
| ~ size(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( ~ greater(X3,X4)
| ~ greater(X2,X1)
| ~ size(X0,X4,X2)
| ~ size(X0,X3,X1)
| ~ reorganization_free(X0,X1,X2)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t35,plain,
or(not(organization(X1,X2)),or(not(organization(X1,X3)),or(not(reorganization_free(X1,X2,X3)),or(not(size(X1,X4,X2)),or(not(size(X1,X5,X3)),or(not(greater(X3,X2)),not(greater(X4,X5)))))))) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t79,plain,
or(not(organization(X1,X2)),or(not(organization(X1,X3)),or(not(reorganization_free(X1,X2,X3)),or(not(size(X1,X4,X2)),or(not(size(X1,X5,X3)),or(not(greater(X3,X2)),not(greater(X4,X5)))))))) = true,
inference(orient,[status(thm)],[t35]) ).
cnf(t15,plain,
reorganization_free(sk1,sk6,sk7) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t142,plain,
reorganization_free(sk1,sk6,sk7) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t146,plain,
true = or(not(organization(sk1,sk6)),or(not(organization(sk1,sk7)),or(not(true),or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2)))))))),
inference(cp,[status(thm)],[t79,t142]) ).
cnf(t1156,plain,
true = or(not(true),or(not(organization(sk1,sk7)),or(not(true),or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2)))))))),
inference(step,[status(thm)],[t146,t115]) ).
cnf(t1157,plain,
true = or(false,or(not(organization(sk1,sk7)),or(not(true),or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2)))))))),
inference(step,[status(thm)],[t1156,t188]) ).
cnf(t1158,plain,
true = or(not(organization(sk1,sk7)),or(not(true),or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2))))))),
inference(step,[status(thm)],[t1157,t45]) ).
cnf(t1159,plain,
true = or(not(true),or(not(true),or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2))))))),
inference(step,[status(thm)],[t1158,t127]) ).
cnf(t1160,plain,
true = or(false,or(not(true),or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2))))))),
inference(step,[status(thm)],[t1159,t188]) ).
cnf(t1161,plain,
true = or(not(true),or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2)))))),
inference(step,[status(thm)],[t1160,t45]) ).
cnf(t1162,plain,
true = or(false,or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2)))))),
inference(step,[status(thm)],[t1161,t188]) ).
cnf(t1163,plain,
true = or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2))))),
inference(step,[status(thm)],[t1162,t45]) ).
cnf(t764,plain,
or(not(size(sk1,X1,sk6)),or(not(size(sk1,X2,sk7)),or(not(greater(sk7,sk6)),not(greater(X1,X2))))) = true,
inference(orient,[status(thm)],[t1163]) ).
cnf(f16,negated_conjecture,
greater(sk4,sk5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_34) ).
fof(f16_nnf,plain,
greater(sk4,sk5),
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
greater(sk4,sk5),
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t6,plain,
greater(sk4,sk5) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t80,plain,
greater(sk4,sk5) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t767,plain,
true = or(not(size(sk1,sk4,sk6)),or(not(size(sk1,sk5,sk7)),or(not(greater(sk7,sk6)),not(true)))),
inference(cp,[status(thm)],[t764,t80]) ).
cnf(f13,negated_conjecture,
size(sk1,sk4,sk6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_31) ).
fof(f13_nnf,plain,
size(sk1,sk4,sk6),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
size(sk1,sk4,sk6),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t17,plain,
size(sk1,sk4,sk6) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t168,plain,
size(sk1,sk4,sk6) = true,
inference(orient,[status(thm)],[t17]) ).
cnf(t1164,plain,
true = or(not(true),or(not(size(sk1,sk5,sk7)),or(not(greater(sk7,sk6)),not(true)))),
inference(step,[status(thm)],[t767,t168]) ).
cnf(t1165,plain,
true = or(false,or(not(size(sk1,sk5,sk7)),or(not(greater(sk7,sk6)),not(true)))),
inference(step,[status(thm)],[t1164,t188]) ).
cnf(t1166,plain,
true = or(not(size(sk1,sk5,sk7)),or(not(greater(sk7,sk6)),not(true))),
inference(step,[status(thm)],[t1165,t45]) ).
cnf(f14,negated_conjecture,
size(sk1,sk5,sk7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_FOL_32) ).
fof(f14_nnf,plain,
size(sk1,sk5,sk7),
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
size(sk1,sk5,sk7),
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t18,plain,
size(sk1,sk5,sk7) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t173,plain,
size(sk1,sk5,sk7) = true,
inference(orient,[status(thm)],[t18]) ).
cnf(t1167,plain,
true = or(not(true),or(not(greater(sk7,sk6)),not(true))),
inference(step,[status(thm)],[t1166,t173]) ).
cnf(t1168,plain,
true = or(false,or(not(greater(sk7,sk6)),not(true))),
inference(step,[status(thm)],[t1167,t188]) ).
cnf(t1169,plain,
true = or(not(greater(sk7,sk6)),not(true)),
inference(step,[status(thm)],[t1168,t45]) ).
cnf(t1170,plain,
true = or(not(greater(sk7,sk6)),false),
inference(step,[status(thm)],[t1169,t188]) ).
cnf(t1171,plain,
true = not(greater(sk7,sk6)),
inference(step,[status(thm)],[t1170,t44]) ).
cnf(t769,plain,
not(greater(sk7,sk6)) = true,
inference(orient,[status(thm)],[t1171]) ).
cnf(t770,plain,
false = ifeq(true,true,greater(sk7,sk6),false),
inference(cp,[status(thm)],[t186,t769]) ).
cnf(t1172,plain,
false = greater(sk7,sk6),
inference(step,[status(thm)],[t770,t38]) ).
cnf(t773,plain,
greater(sk7,sk6) = false,
inference(orient,[status(thm)],[t1172]) ).
cnf(t1247,plain,
true = or(eq(sk6,sk7),false),
inference(step,[status(thm)],[t1246,t773]) ).
cnf(t1248,plain,
true = eq(sk6,sk7),
inference(step,[status(thm)],[t1247,t44]) ).
cnf(t906,plain,
eq(sk6,sk7) = true,
inference(orient,[status(thm)],[t1248]) ).
cnf(t907,plain,
sk7 = ifeq(true,true,sk6,sk7),
inference(cp,[status(thm)],[t42,t906]) ).
cnf(t1249,plain,
sk7 = sk6,
inference(step,[status(thm)],[t907,t38]) ).
cnf(t910,plain,
sk6 = sk7,
inference(orient,[status(thm)],[t1249]) ).
cnf(t1250,plain,
ifeq(sk7,sk7,sk2,sk3) = sk3,
inference(step,[status(thm)],[t341,t910]) ).
cnf(t1251,plain,
sk2 = sk3,
inference(step,[status(thm)],[t1250,t38]) ).
cnf(t911,plain,
sk2 = sk3,
inference(rw,[status(thm)],[t1251]) ).
cnf(t951,plain,
sk2 = sk3,
inference(orient,[status(thm)],[t911]) ).
cnf(t1306,plain,
eq(sk3,sk3) = false,
inference(step,[status(thm)],[t247,t951]) ).
cnf(t4,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t139,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t1307,plain,
true = false,
inference(step,[status(thm)],[t1306,t139]) ).
cnf(t953,plain,
true = false,
inference(rw,[status(thm)],[t1307]) ).
cnf(t960,plain,
false = true,
inference(orient,[status(thm)],[t953]) ).
cnf(f1,axiom,
( ~ greater(B,A)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mp6_2_19) ).
fof(f1_nnf,plain,
! [A,B] :
( ~ greater(B,A)
| ~ greater(A,B) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] :
( ~ greater(B,A)
| ~ greater(A,B) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c1,c6,c7]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t960]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : MGT013-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/5.38 % Computer : n015.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Thu Sep 24 01:02:46 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.79/6.32 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.79/6.32 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------