%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : MGT005-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 : Thu Sep 24 01:25:12 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.43s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 29
% Syntax : Number of formulae : 130 ( 50 unt; 0 def)
% Number of atoms : 572 ( 27 equ)
% Maximal formula atoms : 19 ( 4 avg)
% Number of connectives : 850 ( 408 ~; 442 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 12 con; 0-2 aty)
% Number of variables : 281 ( 281 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] :
( A != B
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] :
( ~ greater(B,A)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B,C] :
( greater(A,C)
| ~ greater(B,C)
| ~ greater(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] :
( survival_chance(A,sk1(B,A),B)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [A,B,C,D] :
( organization(A,D)
| ~ greater(C,D)
| ~ greater(D,B)
| ~ organization(A,C)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A,B,C] :
( greater(C,B)
| ~ reorganization(A,B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
! [A,B,C,D,E] :
( greater(E,D)
| ~ greater(C,B)
| ~ survival_chance(A,E,C)
| ~ survival_chance(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
! [A,B,C,D,E,F,G] :
( greater(F,G)
| greater(C,E)
| ~ greater(C,B)
| greater(D,B)
| ~ survival_chance(A,G,C)
| ~ survival_chance(A,F,B)
| ~ reorganization(A,D,E)
| ~ organization(A,C)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
! [A,B,C,D,E,F,G,H,I] :
( greater(D,F)
| ~ greater(I,H)
| ~ complexity(C,I,B)
| ~ complexity(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/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
! [A,B,C,D,E,F,G,H,I,J,K,L] :
( I = J
| greater(I,J)
| ~ greater(L,K)
| ~ complexity(C,L,B)
| ~ complexity(A,K,B)
| ~ survival_chance(C,J,D)
| ~ survival_chance(A,I,D)
| ~ reorganization_type(C,H,B)
| ~ reorganization_type(A,H,B)
| ~ reorganization(C,B,G)
| ~ reorganization(A,B,D)
| ~ survival_chance(C,F,B)
| ~ survival_chance(A,F,B)
| ~ class(C,E,B)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(A,D)
| ~ organization(C,B)
| ~ organization(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
organization(sk2,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
organization(sk3,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
organization(sk2,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
organization(sk3,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
class(sk2,sk5,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
class(sk3,sk5,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
survival_chance(sk2,sk6,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
survival_chance(sk3,sk6,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
reorganization(sk2,sk11,sk12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
reorganization(sk3,sk11,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
reorganization_type(sk2,sk4,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
reorganization_type(sk3,sk4,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
reorganization_free(sk2,sk12,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
survival_chance(sk2,sk7,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
survival_chance(sk3,sk8,sk13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
complexity(sk2,sk9,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
complexity(sk3,sk10,sk11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
greater(sk10,sk9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
~ greater(sk7,sk8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,plain,
! [X0,X1] :
( X0 != X1
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f31,plain,
! [X0,X1] :
( ~ greater(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f32,plain,
! [A,C] :
( greater(A,C)
| ! [B] :
( ~ greater(B,C)
| ~ greater(A,B) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f33,plain,
! [X0,X1,X2] :
( greater(X0,X2)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f34,plain,
! [X0,X1] :
( survival_chance(X0,sk1(X1,X0),X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f35,plain,
! [A,D] :
( organization(A,D)
| ! [C] :
( ~ greater(C,D)
| ! [B] :
( ~ greater(D,B)
| ~ organization(A,C)
| ~ organization(A,B) ) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f36,plain,
! [X0,X1,X2,X3] :
( organization(X0,X3)
| ~ greater(X2,X3)
| ~ greater(X3,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [B,C] :
( greater(C,B)
| ! [A] : ~ reorganization(A,B,C) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f38,plain,
! [X0,X1,X2] :
( greater(X2,X1)
| ~ reorganization(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
! [D,E] :
( greater(E,D)
| ! [B,C] :
( ~ greater(C,B)
| ! [A] :
( ~ survival_chance(A,E,C)
| ~ survival_chance(A,D,B)
| ~ reorganization_free(A,B,C)
| ~ organization(A,C)
| ~ organization(A,B) ) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f40,plain,
! [X0,X1,X2,X3,X4] :
( greater(X4,X3)
| ~ greater(X2,X1)
| ~ survival_chance(X0,X4,X2)
| ~ survival_chance(X0,X3,X1)
| ~ reorganization_free(X0,X1,X2)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
! [F,G] :
( greater(F,G)
| ! [C,E] :
( greater(C,E)
| ! [B] :
( ~ greater(C,B)
| ! [D] :
( greater(D,B)
| ! [A] :
( ~ survival_chance(A,G,C)
| ~ survival_chance(A,F,B)
| ~ reorganization(A,D,E)
| ~ organization(A,C)
| ~ organization(A,B) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f42,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( greater(X5,X6)
| greater(X2,X4)
| ~ greater(X2,X1)
| greater(X3,X1)
| ~ survival_chance(X0,X6,X2)
| ~ survival_chance(X0,X5,X1)
| ~ reorganization(X0,X3,X4)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f43,plain,
! [D,F] :
( greater(D,F)
| ! [H,I] :
( ~ greater(I,H)
| ! [B,C] :
( ~ complexity(C,I,B)
| ! [A] :
( ~ complexity(A,H,B)
| ! [G] :
( ~ reorganization_type(C,G,B)
| ~ reorganization_type(A,G,B)
| ~ reorganization(C,B,D)
| ~ reorganization(A,B,F)
| ! [E] :
( ~ class(C,E,B)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(C,B)
| ~ organization(A,B) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f44,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( greater(X3,X5)
| ~ greater(X8,X7)
| ~ complexity(X2,X8,X1)
| ~ complexity(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(thm)],[f43]) ).
fof(f45,plain,
! [I,J] :
( I = J
| greater(I,J)
| ! [K,L] :
( ~ greater(L,K)
| ! [B,C] :
( ~ complexity(C,L,B)
| ! [A] :
( ~ complexity(A,K,B)
| ! [D] :
( ~ survival_chance(C,J,D)
| ~ survival_chance(A,I,D)
| ! [H] :
( ~ reorganization_type(C,H,B)
| ~ reorganization_type(A,H,B)
| ! [G] : ~ reorganization(C,B,G)
| ~ reorganization(A,B,D)
| ! [F] :
( ~ survival_chance(C,F,B)
| ~ survival_chance(A,F,B)
| ! [E] :
( ~ class(C,E,B)
| ~ class(A,E,B)
| ~ organization(C,D)
| ~ organization(A,D)
| ~ organization(C,B)
| ~ organization(A,B) ) ) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f46,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11] :
( X8 = X9
| greater(X8,X9)
| ~ greater(X11,X10)
| ~ complexity(X2,X11,X1)
| ~ complexity(X0,X10,X1)
| ~ survival_chance(X2,X9,X3)
| ~ survival_chance(X0,X8,X3)
| ~ reorganization_type(X2,X7,X1)
| ~ reorganization_type(X0,X7,X1)
| ~ reorganization(X2,X1,X6)
| ~ reorganization(X0,X1,X3)
| ~ survival_chance(X2,X5,X1)
| ~ survival_chance(X0,X5,X1)
| ~ class(X2,X4,X1)
| ~ class(X0,X4,X1)
| ~ organization(X2,X3)
| ~ organization(X0,X3)
| ~ organization(X2,X1)
| ~ organization(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
organization(sk2,sk11),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f48,plain,
organization(sk3,sk11),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f49,plain,
organization(sk2,sk13),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f50,plain,
organization(sk3,sk13),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f51,plain,
class(sk2,sk5,sk11),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f52,plain,
class(sk3,sk5,sk11),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f53,plain,
survival_chance(sk2,sk6,sk11),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f54,plain,
survival_chance(sk3,sk6,sk11),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f55,plain,
reorganization(sk2,sk11,sk12),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f56,plain,
reorganization(sk3,sk11,sk13),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f57,plain,
reorganization_type(sk2,sk4,sk11),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f58,plain,
reorganization_type(sk3,sk4,sk11),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f59,plain,
reorganization_free(sk2,sk12,sk13),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f60,plain,
survival_chance(sk2,sk7,sk13),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f61,plain,
survival_chance(sk3,sk8,sk13),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f62,plain,
complexity(sk2,sk9,sk11),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f63,plain,
complexity(sk3,sk10,sk11),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f64,plain,
greater(sk10,sk9),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f65,plain,
~ greater(sk7,sk8),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f66,plain,
! [X0] : ~ greater(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f30]) ).
fof(f70,plain,
! [X0,X1] :
( organization(sk3,X1)
| ~ greater(X0,X1)
| ~ greater(X1,sk11)
| ~ organization(sk3,X0) ),
inference(resolution,[status(thm)],[f36,f48]) ).
fof(f72,plain,
! [X0,X1] :
( organization(sk2,X1)
| ~ greater(X0,X1)
| ~ greater(X1,sk11)
| ~ organization(sk2,X0) ),
inference(resolution,[status(thm)],[f36,f47]) ).
fof(f74,plain,
greater(sk12,sk11),
inference(resolution,[status(thm)],[f38,f55]) ).
fof(f78,plain,
~ greater(sk11,sk12),
inference(resolution,[status(thm)],[f74,f31]) ).
fof(f83,plain,
! [X0] :
( organization(sk3,sk12)
| ~ greater(X0,sk12)
| ~ organization(sk3,X0) ),
inference(resolution,[status(thm)],[f70,f74]) ).
fof(f85,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ greater(sk13,sk12)
| ~ survival_chance(sk2,X1,sk13)
| ~ survival_chance(sk2,X0,sk12)
| ~ organization(sk2,sk13)
| ~ organization(sk2,sk12) ),
inference(resolution,[status(thm)],[f40,f59]) ).
fof(f86,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ greater(sk13,sk12)
| ~ survival_chance(sk2,X1,sk13)
| ~ survival_chance(sk2,X0,sk12)
| ~ organization(sk2,sk12) ),
inference(forward_subsumption_resolution,[status(thm)],[f85,f49]) ).
fof(f87,plain,
! [X0,X1,X2,X3] :
( greater(X2,X3)
| greater(X1,sk13)
| ~ greater(X1,X0)
| greater(sk11,X0)
| ~ survival_chance(sk3,X3,X1)
| ~ survival_chance(sk3,X2,X0)
| ~ organization(sk3,X1)
| ~ organization(sk3,X0) ),
inference(resolution,[status(thm)],[f42,f56]) ).
fof(f90,plain,
! [X0,X1,X2,X3,X4,X5] :
( greater(X1,X2)
| ~ greater(X5,X4)
| ~ complexity(X0,X5,sk11)
| ~ complexity(sk2,X4,sk11)
| ~ reorganization_type(X0,X3,sk11)
| ~ reorganization_type(sk2,X3,sk11)
| ~ reorganization(X0,sk11,X1)
| ~ reorganization(sk2,sk11,X2)
| ~ class(X0,sk5,sk11)
| ~ organization(X0,X1)
| ~ organization(X0,sk11)
| ~ organization(sk2,sk11) ),
inference(resolution,[status(thm)],[f44,f51]) ).
fof(f92,plain,
! [X0,X1,X2,X3,X4,X5] :
( greater(X1,X2)
| ~ greater(X5,X4)
| ~ complexity(X0,X5,sk11)
| ~ complexity(sk2,X4,sk11)
| ~ reorganization_type(X0,X3,sk11)
| ~ reorganization_type(sk2,X3,sk11)
| ~ reorganization(X0,sk11,X1)
| ~ reorganization(sk2,sk11,X2)
| ~ class(X0,sk5,sk11)
| ~ organization(X0,X1)
| ~ organization(X0,sk11) ),
inference(forward_subsumption_resolution,[status(thm)],[f90,f47]) ).
fof(f93,plain,
! [X0] :
( organization(sk2,sk12)
| ~ greater(X0,sk12)
| ~ organization(sk2,X0) ),
inference(resolution,[status(thm)],[f72,f74]) ).
fof(f151,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( X5 = X6
| greater(X5,X6)
| ~ greater(X8,X7)
| ~ complexity(X0,X8,sk11)
| ~ complexity(sk2,X7,sk11)
| ~ survival_chance(X0,X6,X1)
| ~ survival_chance(sk2,X5,X1)
| ~ reorganization_type(X0,X4,sk11)
| ~ reorganization_type(sk2,X4,sk11)
| ~ reorganization(X0,sk11,X3)
| ~ reorganization(sk2,sk11,X1)
| ~ survival_chance(X0,X2,sk11)
| ~ survival_chance(sk2,X2,sk11)
| ~ class(X0,sk5,sk11)
| ~ organization(X0,X1)
| ~ organization(sk2,X1)
| ~ organization(X0,sk11)
| ~ organization(sk2,sk11) ),
inference(resolution,[status(thm)],[f46,f51]) ).
fof(f153,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( X5 = X6
| greater(X5,X6)
| ~ greater(X8,X7)
| ~ complexity(X0,X8,sk11)
| ~ complexity(sk2,X7,sk11)
| ~ survival_chance(X0,X6,X1)
| ~ survival_chance(sk2,X5,X1)
| ~ reorganization_type(X0,X4,sk11)
| ~ reorganization_type(sk2,X4,sk11)
| ~ reorganization(X0,sk11,X3)
| ~ reorganization(sk2,sk11,X1)
| ~ survival_chance(X0,X2,sk11)
| ~ survival_chance(sk2,X2,sk11)
| ~ class(X0,sk5,sk11)
| ~ organization(X0,X1)
| ~ organization(sk2,X1)
| ~ organization(X0,sk11) ),
inference(forward_subsumption_resolution,[status(thm)],[f151,f47]) ).
fof(f185,plain,
! [X0,X1,X2,X3,X4] :
( greater(X1,sk12)
| ~ greater(X4,X3)
| ~ complexity(X0,X4,sk11)
| ~ complexity(sk2,X3,sk11)
| ~ reorganization_type(X0,X2,sk11)
| ~ reorganization_type(sk2,X2,sk11)
| ~ reorganization(X0,sk11,X1)
| ~ class(X0,sk5,sk11)
| ~ organization(X0,X1)
| ~ organization(X0,sk11) ),
inference(resolution,[status(thm)],[f92,f55]) ).
fof(f189,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( X4 = X5
| greater(X4,X5)
| ~ greater(X7,X6)
| ~ complexity(X0,X7,sk11)
| ~ complexity(sk2,X6,sk11)
| ~ survival_chance(X0,X5,X1)
| ~ survival_chance(sk2,X4,X1)
| ~ reorganization_type(X0,X3,sk11)
| ~ reorganization_type(sk2,X3,sk11)
| ~ reorganization(X0,sk11,X2)
| ~ reorganization(sk2,sk11,X1)
| ~ survival_chance(X0,sk6,sk11)
| ~ class(X0,sk5,sk11)
| ~ organization(X0,X1)
| ~ organization(sk2,X1)
| ~ organization(X0,sk11) ),
inference(resolution,[status(thm)],[f153,f53]) ).
fof(f217,plain,
! [X0,X1,X2] :
( greater(sk13,sk12)
| ~ greater(X2,X1)
| ~ complexity(sk3,X2,sk11)
| ~ complexity(sk2,X1,sk11)
| ~ reorganization_type(sk3,X0,sk11)
| ~ reorganization_type(sk2,X0,sk11)
| ~ class(sk3,sk5,sk11)
| ~ organization(sk3,sk13)
| ~ organization(sk3,sk11) ),
inference(resolution,[status(thm)],[f185,f56]) ).
fof(f219,plain,
! [X0,X1,X2] :
( greater(sk13,sk12)
| ~ greater(X2,X1)
| ~ complexity(sk3,X2,sk11)
| ~ complexity(sk2,X1,sk11)
| ~ reorganization_type(sk3,X0,sk11)
| ~ reorganization_type(sk2,X0,sk11)
| ~ class(sk3,sk5,sk11)
| ~ organization(sk3,sk13) ),
inference(forward_subsumption_resolution,[status(thm)],[f217,f48]) ).
fof(f233,plain,
! [X0,X1,X2] :
( greater(sk13,sk12)
| ~ greater(X2,X1)
| ~ complexity(sk3,X2,sk11)
| ~ complexity(sk2,X1,sk11)
| ~ reorganization_type(sk3,X0,sk11)
| ~ reorganization_type(sk2,X0,sk11)
| ~ class(sk3,sk5,sk11) ),
inference(forward_subsumption_resolution,[status(thm)],[f219,f50]) ).
fof(f234,plain,
! [X0,X1,X2] :
( greater(sk13,sk12)
| ~ greater(X2,X1)
| ~ complexity(sk3,X2,sk11)
| ~ complexity(sk2,X1,sk11)
| ~ reorganization_type(sk3,X0,sk11)
| ~ reorganization_type(sk2,X0,sk11) ),
inference(resolution,[status(thm)],[f233,f52]) ).
fof(f235,plain,
! [X0,X1] :
( greater(sk13,sk12)
| ~ greater(X1,X0)
| ~ complexity(sk3,X1,sk11)
| ~ complexity(sk2,X0,sk11)
| ~ reorganization_type(sk3,sk4,sk11) ),
inference(resolution,[status(thm)],[f234,f57]) ).
fof(f236,plain,
! [X0,X1] :
( greater(sk13,sk12)
| ~ greater(X1,X0)
| ~ complexity(sk3,X1,sk11)
| ~ complexity(sk2,X0,sk11) ),
inference(forward_subsumption_resolution,[status(thm)],[f235,f58]) ).
fof(f237,plain,
! [X0] :
( greater(sk13,sk12)
| ~ greater(X0,sk9)
| ~ complexity(sk3,X0,sk11) ),
inference(resolution,[status(thm)],[f236,f62]) ).
fof(f238,plain,
( greater(sk13,sk12)
| ~ greater(sk10,sk9) ),
inference(resolution,[status(thm)],[f237,f63]) ).
fof(f239,plain,
greater(sk13,sk12),
inference(forward_subsumption_resolution,[status(thm)],[f238,f64]) ).
fof(f240,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ survival_chance(sk2,X1,sk13)
| ~ survival_chance(sk2,X0,sk12)
| ~ organization(sk2,sk12) ),
inference(backward_subsumption_resolution,[status(thm)],[f86,f239]) ).
fof(f241,plain,
( organization(sk2,sk12)
| ~ organization(sk2,sk13) ),
inference(resolution,[status(thm)],[f239,f93]) ).
fof(f242,plain,
( organization(sk3,sk12)
| ~ organization(sk3,sk13) ),
inference(resolution,[status(thm)],[f239,f83]) ).
fof(f245,plain,
organization(sk2,sk12),
inference(forward_subsumption_resolution,[status(thm)],[f241,f49]) ).
fof(f246,plain,
organization(sk3,sk12),
inference(forward_subsumption_resolution,[status(thm)],[f242,f50]) ).
fof(f251,plain,
survival_chance(sk2,sk1(sk12,sk2),sk12),
inference(resolution,[status(thm)],[f245,f34]) ).
fof(f253,plain,
survival_chance(sk3,sk1(sk12,sk3),sk12),
inference(resolution,[status(thm)],[f246,f34]) ).
fof(f266,plain,
! [X0,X1] :
( greater(sk1(sk12,sk3),X1)
| greater(X0,sk13)
| ~ greater(X0,sk12)
| greater(sk11,sk12)
| ~ survival_chance(sk3,X1,X0)
| ~ organization(sk3,X0)
| ~ organization(sk3,sk12) ),
inference(resolution,[status(thm)],[f253,f87]) ).
fof(f269,plain,
! [X0,X1] :
( greater(sk1(sk12,sk3),X1)
| greater(X0,sk13)
| ~ greater(X0,sk12)
| greater(sk11,sk12)
| ~ survival_chance(sk3,X1,X0)
| ~ organization(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f266,f246]) ).
fof(f280,plain,
! [X0,X1] :
( greater(X1,X0)
| ~ survival_chance(sk2,X1,sk13)
| ~ survival_chance(sk2,X0,sk12) ),
inference(forward_subsumption_resolution,[status(thm)],[f240,f245]) ).
fof(f281,plain,
! [X0] :
( greater(X0,sk1(sk12,sk2))
| ~ survival_chance(sk2,X0,sk13) ),
inference(resolution,[status(thm)],[f280,f251]) ).
fof(f284,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X3 = X4
| greater(X3,X4)
| ~ greater(X6,X5)
| ~ complexity(sk3,X6,sk11)
| ~ complexity(sk2,X5,sk11)
| ~ survival_chance(sk3,X4,X0)
| ~ survival_chance(sk2,X3,X0)
| ~ reorganization_type(sk3,X2,sk11)
| ~ reorganization_type(sk2,X2,sk11)
| ~ reorganization(sk3,sk11,X1)
| ~ reorganization(sk2,sk11,X0)
| ~ class(sk3,sk5,sk11)
| ~ organization(sk3,X0)
| ~ organization(sk2,X0)
| ~ organization(sk3,sk11) ),
inference(resolution,[status(thm)],[f189,f54]) ).
fof(f286,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X3 = X4
| greater(X3,X4)
| ~ greater(X6,X5)
| ~ complexity(sk3,X6,sk11)
| ~ complexity(sk2,X5,sk11)
| ~ survival_chance(sk3,X4,X0)
| ~ survival_chance(sk2,X3,X0)
| ~ reorganization_type(sk3,X2,sk11)
| ~ reorganization_type(sk2,X2,sk11)
| ~ reorganization(sk3,sk11,X1)
| ~ reorganization(sk2,sk11,X0)
| ~ class(sk3,sk5,sk11)
| ~ organization(sk3,X0)
| ~ organization(sk2,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f284,f48]) ).
fof(f289,plain,
greater(sk7,sk1(sk12,sk2)),
inference(resolution,[status(thm)],[f281,f60]) ).
fof(f290,plain,
! [X0] :
( greater(sk7,X0)
| ~ greater(sk1(sk12,sk2),X0) ),
inference(resolution,[status(thm)],[f289,f33]) ).
fof(f313,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X3 = X4
| greater(X3,X4)
| ~ greater(X6,X5)
| ~ complexity(sk3,X6,sk11)
| ~ complexity(sk2,X5,sk11)
| ~ survival_chance(sk3,X4,X0)
| ~ survival_chance(sk2,X3,X0)
| ~ reorganization_type(sk3,X2,sk11)
| ~ reorganization_type(sk2,X2,sk11)
| ~ reorganization(sk3,sk11,X1)
| ~ reorganization(sk2,sk11,X0)
| ~ organization(sk3,X0)
| ~ organization(sk2,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f286,f52]) ).
fof(f314,plain,
! [X0,X1,X2,X3,X4,X5] :
( X2 = X3
| greater(X2,X3)
| ~ greater(X5,X4)
| ~ complexity(sk3,X5,sk11)
| ~ complexity(sk2,X4,sk11)
| ~ survival_chance(sk3,X3,X0)
| ~ survival_chance(sk2,X2,X0)
| ~ reorganization_type(sk3,X1,sk11)
| ~ reorganization_type(sk2,X1,sk11)
| ~ reorganization(sk2,sk11,X0)
| ~ organization(sk3,X0)
| ~ organization(sk2,X0) ),
inference(resolution,[status(thm)],[f313,f56]) ).
fof(f315,plain,
! [X0,X1] :
( greater(sk1(sk12,sk3),X1)
| greater(X0,sk13)
| ~ greater(X0,sk12)
| ~ survival_chance(sk3,X1,X0)
| ~ organization(sk3,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f269,f78]) ).
fof(f319,plain,
( greater(sk1(sk12,sk3),sk8)
| greater(sk13,sk13)
| ~ greater(sk13,sk12)
| ~ organization(sk3,sk13) ),
inference(resolution,[status(thm)],[f315,f61]) ).
fof(f322,plain,
( greater(sk1(sk12,sk3),sk8)
| greater(sk13,sk13)
| ~ greater(sk13,sk12) ),
inference(forward_subsumption_resolution,[status(thm)],[f319,f50]) ).
fof(f323,plain,
( greater(sk1(sk12,sk3),sk8)
| greater(sk13,sk13) ),
inference(forward_subsumption_resolution,[status(thm)],[f322,f239]) ).
fof(f337,plain,
! [X0,X1,X2,X3,X4] :
( X1 = X2
| greater(X1,X2)
| ~ greater(X4,X3)
| ~ complexity(sk3,X4,sk11)
| ~ complexity(sk2,X3,sk11)
| ~ survival_chance(sk3,X2,X0)
| ~ survival_chance(sk2,X1,X0)
| ~ reorganization_type(sk3,sk4,sk11)
| ~ reorganization(sk2,sk11,X0)
| ~ organization(sk3,X0)
| ~ organization(sk2,X0) ),
inference(resolution,[status(thm)],[f314,f57]) ).
fof(f338,plain,
! [X0,X1,X2,X3,X4] :
( X1 = X2
| greater(X1,X2)
| ~ greater(X4,X3)
| ~ complexity(sk3,X4,sk11)
| ~ complexity(sk2,X3,sk11)
| ~ survival_chance(sk3,X2,X0)
| ~ survival_chance(sk2,X1,X0)
| ~ reorganization(sk2,sk11,X0)
| ~ organization(sk3,X0)
| ~ organization(sk2,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f337,f58]) ).
fof(f339,plain,
! [X0,X1,X2] :
( sk1(sk12,sk2) = X0
| greater(sk1(sk12,sk2),X0)
| ~ greater(X2,X1)
| ~ complexity(sk3,X2,sk11)
| ~ complexity(sk2,X1,sk11)
| ~ survival_chance(sk3,X0,sk12)
| ~ reorganization(sk2,sk11,sk12)
| ~ organization(sk3,sk12)
| ~ organization(sk2,sk12) ),
inference(resolution,[status(thm)],[f338,f251]) ).
fof(f344,plain,
! [X0,X1,X2] :
( sk1(sk12,sk2) = X0
| greater(sk1(sk12,sk2),X0)
| ~ greater(X2,X1)
| ~ complexity(sk3,X2,sk11)
| ~ complexity(sk2,X1,sk11)
| ~ survival_chance(sk3,X0,sk12)
| ~ reorganization(sk2,sk11,sk12)
| ~ organization(sk3,sk12) ),
inference(forward_subsumption_resolution,[status(thm)],[f339,f245]) ).
fof(f356,plain,
! [X0,X1,X2] :
( sk1(sk12,sk2) = X0
| greater(sk1(sk12,sk2),X0)
| ~ greater(X2,X1)
| ~ complexity(sk3,X2,sk11)
| ~ complexity(sk2,X1,sk11)
| ~ survival_chance(sk3,X0,sk12)
| ~ reorganization(sk2,sk11,sk12) ),
inference(forward_subsumption_resolution,[status(thm)],[f344,f246]) ).
fof(f357,plain,
! [X0,X1] :
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| ~ greater(X1,X0)
| ~ complexity(sk3,X1,sk11)
| ~ complexity(sk2,X0,sk11)
| ~ reorganization(sk2,sk11,sk12) ),
inference(resolution,[status(thm)],[f356,f253]) ).
fof(f358,plain,
! [X0,X1] :
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| ~ greater(X1,X0)
| ~ complexity(sk3,X1,sk11)
| ~ complexity(sk2,X0,sk11) ),
inference(forward_subsumption_resolution,[status(thm)],[f357,f55]) ).
fof(f359,plain,
! [X0] :
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| ~ greater(X0,sk9)
| ~ complexity(sk3,X0,sk11) ),
inference(resolution,[status(thm)],[f358,f62]) ).
fof(f360,plain,
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3))
| ~ greater(sk10,sk9) ),
inference(resolution,[status(thm)],[f359,f63]) ).
fof(f361,plain,
( sk1(sk12,sk2) = sk1(sk12,sk3)
| greater(sk1(sk12,sk2),sk1(sk12,sk3)) ),
inference(forward_subsumption_resolution,[status(thm)],[f360,f64]) ).
fof(f364,plain,
( greater(sk7,sk1(sk12,sk3))
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[f361,f290]) ).
fof(f374,plain,
! [X0] :
( greater(sk7,X0)
| ~ greater(sk1(sk12,sk3),X0)
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[f364,f33]) ).
fof(f383,plain,
( greater(sk13,sk13)
| greater(sk7,sk8)
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(resolution,[status(thm)],[f374,f323]) ).
fof(f385,plain,
( greater(sk13,sk13)
| sk1(sk12,sk2) = sk1(sk12,sk3) ),
inference(forward_subsumption_resolution,[status(thm)],[f383,f65]) ).
fof(f400,plain,
! [X0] :
( greater(sk7,X0)
| ~ greater(sk1(sk12,sk3),X0) ),
inference(backward_demodulation,[status(thm)],[f409,f290]) ).
fof(f409,plain,
sk1(sk12,sk2) = sk1(sk12,sk3),
inference(forward_subsumption_resolution,[status(thm)],[f385,f66]) ).
fof(f430,plain,
( greater(sk13,sk13)
| greater(sk7,sk8) ),
inference(resolution,[status(thm)],[f400,f323]) ).
fof(f432,plain,
greater(sk13,sk13),
inference(forward_subsumption_resolution,[status(thm)],[f430,f65]) ).
fof(f433,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f432,f66]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n014.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 01:20:35 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.08/0.43 % Refutation found
% 0.08/0.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.08/0.46 % Elapsed time: 0.086140 seconds
% 0.08/0.46 % CPU time: 0.340668 seconds
% 0.08/0.46 % Total memory used: 85.134 MB
% 0.08/0.46 % Net memory used: 84.510 MB
%------------------------------------------------------------------------------