%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : MGT005-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:38 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n011.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 21 01:20:40 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.53 % Refutation found
% 0.13/0.53 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.53 fof(f1,axiom,(
% 0.13/0.53 (![A,B]: (( ~ greater(A,B)| A != B ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f2,axiom,(
% 0.13/0.53 (![A,B]: (( ~ greater(A,B)| ~ greater(B,A) ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f3,axiom,(
% 0.13/0.53 (![A,B,C]: (( ~ greater(A,B)| ~ greater(B,C)| greater(A,C) ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f4,axiom,(
% 0.13/0.53 (![A,B]: (( ~ organization(A,B)| survival_chance(A,sk1(B,A),B) ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f5,axiom,(
% 0.13/0.53 (![A,B,C,D]: (( ~ organization(A,B)| ~ organization(A,C)| ~ greater(D,B)| ~ greater(C,D)| organization(A,D) ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f6,axiom,(
% 0.13/0.53 (![A,B,C]: (( ~ reorganization(A,B,C)| greater(C,B) ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f7,hypothesis,(
% 0.13/0.53 (![A,B,C,D,E]: (( ~ organization(A,B)| ~ organization(A,C)| ~ reorganization_free(A,B,C)| ~ survival_chance(A,D,B)| ~ survival_chance(A,E,C)| ~ greater(C,B)| greater(E,D) ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f8,hypothesis,(
% 0.13/0.53 (![A,B,C,D,E,F,G]: (( ~ organization(A,B)| ~ organization(A,C)| ~ reorganization(A,D,E)| ~ survival_chance(A,F,B)| ~ survival_chance(A,G,C)| greater(D,B)| ~ greater(C,B)| greater(C,E)| greater(F,G) ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f9,hypothesis,(
% 0.13/0.53 (![A,B,C,D,E,F,G,H,I]: (( ~ organization(A,B)| ~ organization(C,B)| ~ organization(C,D)| ~ class(A,E,B)| ~ class(C,E,B)| ~ reorganization(A,B,F)| ~ reorganization(C,B,D)| ~ reorganization_type(A,G,B)| ~ reorganization_type(C,G,B)| ~ complexity(A,H,B)| ~ complexity(C,I,B)| ~ greater(I,H)| greater(D,F) ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f10,hypothesis,(
% 0.13/0.53 (![A,B,C,D,E,F,G,H,I,J,K,L]: (( ~ organization(A,B)| ~ organization(C,B)| ~ organization(A,D)| ~ organization(C,D)| ~ class(A,E,B)| ~ class(C,E,B)| ~ survival_chance(A,F,B)| ~ survival_chance(C,F,B)| ~ reorganization(A,B,D)| ~ reorganization(C,B,G)| ~ reorganization_type(A,H,B)| ~ reorganization_type(C,H,B)| ~ survival_chance(A,I,D)| ~ survival_chance(C,J,D)| ~ complexity(A,K,B)| ~ complexity(C,L,B)| ~ greater(L,K)| greater(I,J)| I = J ) ))),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f11,negated_conjecture,(
% 0.13/0.53 organization(sk2,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f12,negated_conjecture,(
% 0.13/0.53 organization(sk3,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f13,negated_conjecture,(
% 0.13/0.53 organization(sk2,sk13) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f14,negated_conjecture,(
% 0.13/0.53 organization(sk3,sk13) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f15,negated_conjecture,(
% 0.13/0.53 class(sk2,sk5,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f16,negated_conjecture,(
% 0.13/0.53 class(sk3,sk5,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f17,negated_conjecture,(
% 0.13/0.53 survival_chance(sk2,sk6,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f18,negated_conjecture,(
% 0.13/0.53 survival_chance(sk3,sk6,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f19,negated_conjecture,(
% 0.13/0.53 reorganization(sk2,sk11,sk12) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f20,negated_conjecture,(
% 0.13/0.53 reorganization(sk3,sk11,sk13) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f21,negated_conjecture,(
% 0.13/0.53 reorganization_type(sk2,sk4,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f22,negated_conjecture,(
% 0.13/0.53 reorganization_type(sk3,sk4,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f23,negated_conjecture,(
% 0.13/0.53 reorganization_free(sk2,sk12,sk13) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f24,negated_conjecture,(
% 0.13/0.53 survival_chance(sk2,sk7,sk13) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f25,negated_conjecture,(
% 0.13/0.53 survival_chance(sk3,sk8,sk13) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f26,negated_conjecture,(
% 0.13/0.53 complexity(sk2,sk9,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f27,negated_conjecture,(
% 0.13/0.53 complexity(sk3,sk10,sk11) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f28,negated_conjecture,(
% 0.13/0.53 greater(sk10,sk9) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f29,negated_conjecture,(
% 0.13/0.53 ~ greater(sk7,sk8) ),
% 0.13/0.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.53 fof(f30,plain,(
% 0.13/0.53 ![X0,X1]: (~greater(X0,X1)|~X0=X1)),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.53 fof(f31,plain,(
% 0.13/0.53 ![X0,X1]: (~greater(X0,X1)|~greater(X1,X0))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.53 fof(f32,plain,(
% 0.13/0.53 ![A,C]: ((![B]: (~greater(A,B)|~greater(B,C)))|greater(A,C))),
% 0.13/0.53 inference(miniscoping,[status(thm)],[f3])).
% 0.13/0.53 fof(f33,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~greater(X0,X1)|~greater(X1,X2)|greater(X0,X2))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f32])).
% 0.13/0.53 fof(f34,plain,(
% 0.13/0.53 ![X0,X1]: (~organization(X0,X1)|survival_chance(X0,sk1(X1,X0),X1))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.53 fof(f35,plain,(
% 0.13/0.53 ![A,D]: ((![C]: ((![B]: ((~organization(A,B)|~organization(A,C))|~greater(D,B)))|~greater(C,D)))|organization(A,D))),
% 0.13/0.53 inference(miniscoping,[status(thm)],[f5])).
% 0.13/0.53 fof(f36,plain,(
% 0.13/0.53 ![X0,X1,X2,X3]: (~organization(X0,X1)|~organization(X0,X2)|~greater(X3,X1)|~greater(X2,X3)|organization(X0,X3))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f35])).
% 0.13/0.53 fof(f37,plain,(
% 0.13/0.53 ![B,C]: ((![A]: ~reorganization(A,B,C))|greater(C,B))),
% 0.13/0.53 inference(miniscoping,[status(thm)],[f6])).
% 0.13/0.53 fof(f38,plain,(
% 0.13/0.53 ![X0,X1,X2]: (~reorganization(X0,X1,X2)|greater(X2,X1))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f37])).
% 0.13/0.53 fof(f39,plain,(
% 0.13/0.53 ![D,E]: ((![B,C]: ((![A]: ((((~organization(A,B)|~organization(A,C))|~reorganization_free(A,B,C))|~survival_chance(A,D,B))|~survival_chance(A,E,C)))|~greater(C,B)))|greater(E,D))),
% 0.13/0.53 inference(miniscoping,[status(thm)],[f7])).
% 0.13/0.53 fof(f40,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4]: (~organization(X0,X1)|~organization(X0,X2)|~reorganization_free(X0,X1,X2)|~survival_chance(X0,X3,X1)|~survival_chance(X0,X4,X2)|~greater(X2,X1)|greater(X4,X3))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f39])).
% 0.13/0.53 fof(f41,plain,(
% 0.13/0.53 ![F,G]: ((![C,E]: ((![B]: ((![D]: ((![A]: ((((~organization(A,B)|~organization(A,C))|~reorganization(A,D,E))|~survival_chance(A,F,B))|~survival_chance(A,G,C)))|greater(D,B)))|~greater(C,B)))|greater(C,E)))|greater(F,G))),
% 0.13/0.53 inference(miniscoping,[status(thm)],[f8])).
% 0.13/0.53 fof(f42,plain,(
% 0.13/0.53 ![X0,X1,X2,X3,X4,X5,X6]: (~organization(X0,X1)|~organization(X0,X2)|~reorganization(X0,X3,X4)|~survival_chance(X0,X5,X1)|~survival_chance(X0,X6,X2)|greater(X3,X1)|~greater(X2,X1)|greater(X2,X4)|greater(X5,X6))),
% 0.13/0.53 inference(cnf_transformation,[status(thm)],[f41])).
% 0.13/0.53 fof(f43,plain,(
% 0.13/0.53 ![D,F]: ((![H,I]: ((![B,C]: ((![A]: ((![G]: (((((![E]: ((((~organization(A,B)|~organization(C,B))|~organization(C,D))|~class(A,E,B))|~class(C,E,B)))|~reorganization(A,B,F))|~reorganization(C,B,D))|~reorganization_type(A,G,B))|~reorganization_type(C,G,B)))|~complexity(A,H,B)))|~complexity(C,I,B)))|~greater(I,H)))|greater(D,F))),
% 0.13/0.54 inference(miniscoping,[status(thm)],[f9])).
% 0.13/0.54 fof(f44,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~organization(X0,X1)|~organization(X2,X1)|~organization(X2,X3)|~class(X0,X4,X1)|~class(X2,X4,X1)|~reorganization(X0,X1,X5)|~reorganization(X2,X1,X3)|~reorganization_type(X0,X6,X1)|~reorganization_type(X2,X6,X1)|~complexity(X0,X7,X1)|~complexity(X2,X8,X1)|~greater(X8,X7)|greater(X3,X5))),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f43])).
% 0.13/0.54 fof(f45,plain,(
% 0.13/0.54 ![I,J]: (((![K,L]: ((![B,C]: ((![A]: ((![D]: (((![H]: (((((![F]: (((![E]: (((((~organization(A,B)|~organization(C,B))|~organization(A,D))|~organization(C,D))|~class(A,E,B))|~class(C,E,B)))|~survival_chance(A,F,B))|~survival_chance(C,F,B)))|~reorganization(A,B,D))|(![G]: ~reorganization(C,B,G)))|~reorganization_type(A,H,B))|~reorganization_type(C,H,B)))|~survival_chance(A,I,D))|~survival_chance(C,J,D)))|~complexity(A,K,B)))|~complexity(C,L,B)))|~greater(L,K)))|greater(I,J))|I=J)),
% 0.13/0.54 inference(miniscoping,[status(thm)],[f10])).
% 0.13/0.54 fof(f46,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11]: (~organization(X0,X1)|~organization(X2,X1)|~organization(X0,X3)|~organization(X2,X3)|~class(X0,X4,X1)|~class(X2,X4,X1)|~survival_chance(X0,X5,X1)|~survival_chance(X2,X5,X1)|~reorganization(X0,X1,X3)|~reorganization(X2,X1,X6)|~reorganization_type(X0,X7,X1)|~reorganization_type(X2,X7,X1)|~survival_chance(X0,X8,X3)|~survival_chance(X2,X9,X3)|~complexity(X0,X10,X1)|~complexity(X2,X11,X1)|~greater(X11,X10)|greater(X8,X9)|X8=X9)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/0.54 fof(f47,plain,(
% 0.13/0.54 organization(sk2,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.54 fof(f48,plain,(
% 0.13/0.54 organization(sk3,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f12])).
% 0.13/0.54 fof(f49,plain,(
% 0.13/0.54 organization(sk2,sk13)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.54 fof(f50,plain,(
% 0.13/0.54 organization(sk3,sk13)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.54 fof(f51,plain,(
% 0.13/0.54 class(sk2,sk5,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.54 fof(f52,plain,(
% 0.13/0.54 class(sk3,sk5,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.54 fof(f53,plain,(
% 0.13/0.54 survival_chance(sk2,sk6,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.54 fof(f54,plain,(
% 0.13/0.54 survival_chance(sk3,sk6,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.54 fof(f55,plain,(
% 0.13/0.54 reorganization(sk2,sk11,sk12)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.54 fof(f56,plain,(
% 0.13/0.54 reorganization(sk3,sk11,sk13)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f20])).
% 0.13/0.54 fof(f57,plain,(
% 0.13/0.54 reorganization_type(sk2,sk4,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f21])).
% 0.13/0.54 fof(f58,plain,(
% 0.13/0.54 reorganization_type(sk3,sk4,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f22])).
% 0.13/0.54 fof(f59,plain,(
% 0.13/0.54 reorganization_free(sk2,sk12,sk13)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f23])).
% 0.13/0.54 fof(f60,plain,(
% 0.13/0.54 survival_chance(sk2,sk7,sk13)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/0.54 fof(f61,plain,(
% 0.13/0.54 survival_chance(sk3,sk8,sk13)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.54 fof(f62,plain,(
% 0.13/0.54 complexity(sk2,sk9,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/0.54 fof(f63,plain,(
% 0.13/0.54 complexity(sk3,sk10,sk11)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f27])).
% 0.13/0.54 fof(f64,plain,(
% 0.13/0.54 greater(sk10,sk9)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/0.54 fof(f65,plain,(
% 0.13/0.54 ~greater(sk7,sk8)),
% 0.13/0.54 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.54 fof(f66,plain,(
% 0.13/0.54 ![X0]: (~greater(X0,X0))),
% 0.13/0.54 inference(destructive_equality_resolution,[status(thm)],[f30])).
% 0.13/0.54 fof(f68,plain,(
% 0.13/0.54 ![X0,X1]: (~organization(sk3,X0)|~greater(X1,sk11)|~greater(X0,X1)|organization(sk3,X1))),
% 0.13/0.54 inference(resolution,[status(thm)],[f36,f48])).
% 0.13/0.54 fof(f70,plain,(
% 0.13/0.54 ![X0,X1]: (~organization(sk2,X0)|~greater(X1,sk11)|~greater(X0,X1)|organization(sk2,X1))),
% 0.13/0.54 inference(resolution,[status(thm)],[f36,f47])).
% 0.13/0.54 fof(f77,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5]: (~organization(sk2,sk11)|~organization(X0,sk11)|~organization(X0,X1)|~class(X0,sk5,sk11)|~reorganization(sk2,sk11,X2)|~reorganization(X0,sk11,X1)|~reorganization_type(sk2,X3,sk11)|~reorganization_type(X0,X3,sk11)|~complexity(sk2,X4,sk11)|~complexity(X0,X5,sk11)|~greater(X5,X4)|greater(X1,X2))),
% 0.13/0.54 inference(resolution,[status(thm)],[f51,f44])).
% 0.13/0.54 fof(f78,definition,(
% 0.13/0.54 sQ0_spl <=> (organization(sk2,sk11))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f80,plain,(
% 0.13/0.54 ~organization(sk2,sk11)|sQ0_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f78])).
% 0.13/0.54 fof(f81,definition,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5]: (sQ1_spl <=> (~organization(X0,sk11)|~organization(X0,X1)|~class(X0,sk5,sk11)|~reorganization(sk2,sk11,X2)|~reorganization(X0,sk11,X1)|~reorganization_type(sk2,X3,sk11)|~reorganization_type(X0,X3,sk11)|~complexity(sk2,X4,sk11)|~complexity(X0,X5,sk11)|~greater(X5,X4)|greater(X1,X2)))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f82,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5]: (~organization(X0,sk11)|~organization(X0,X1)|~class(X0,sk5,sk11)|~reorganization(sk2,sk11,X2)|~reorganization(X0,sk11,X1)|~reorganization_type(sk2,X3,sk11)|~reorganization_type(X0,X3,sk11)|~complexity(sk2,X4,sk11)|~complexity(X0,X5,sk11)|~greater(X5,X4)|greater(X1,X2)|~sQ1_spl)),
% 0.13/0.54 inference(component_clause,[status(thm)],[f81])).
% 0.13/0.54 fof(f84,plain,(
% 0.13/0.54 ~sQ0_spl|sQ1_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f77,f78,f81])).
% 0.13/0.54 fof(f85,plain,(
% 0.13/0.54 $false|sQ0_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f80,f47])).
% 0.13/0.54 fof(f86,plain,(
% 0.13/0.54 sQ0_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f85])).
% 0.13/0.54 fof(f88,definition,(
% 0.13/0.54 sQ2_spl <=> (organization(sk3,sk11))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f90,plain,(
% 0.13/0.54 ~organization(sk3,sk11)|sQ2_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f88])).
% 0.13/0.54 fof(f95,plain,(
% 0.13/0.54 $false|sQ2_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f90,f48])).
% 0.13/0.54 fof(f96,plain,(
% 0.13/0.54 sQ2_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f95])).
% 0.13/0.54 fof(f98,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~organization(sk2,sk11)|~organization(X0,sk11)|~organization(sk2,X1)|~organization(X0,X1)|~class(X0,sk5,sk11)|~survival_chance(sk2,X2,sk11)|~survival_chance(X0,X2,sk11)|~reorganization(sk2,sk11,X1)|~reorganization(X0,sk11,X3)|~reorganization_type(sk2,X4,sk11)|~reorganization_type(X0,X4,sk11)|~survival_chance(sk2,X5,X1)|~survival_chance(X0,X6,X1)|~complexity(sk2,X7,sk11)|~complexity(X0,X8,sk11)|~greater(X8,X7)|greater(X5,X6)|X5=X6)),
% 0.13/0.54 inference(resolution,[status(thm)],[f46,f51])).
% 0.13/0.54 fof(f103,definition,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (sQ5_spl <=> (~organization(X0,sk11)|~organization(sk2,X1)|~organization(X0,X1)|~class(X0,sk5,sk11)|~survival_chance(sk2,X2,sk11)|~survival_chance(X0,X2,sk11)|~reorganization(sk2,sk11,X1)|~reorganization(X0,sk11,X3)|~reorganization_type(sk2,X4,sk11)|~reorganization_type(X0,X4,sk11)|~survival_chance(sk2,X5,X1)|~survival_chance(X0,X6,X1)|~complexity(sk2,X7,sk11)|~complexity(X0,X8,sk11)|~greater(X8,X7)|greater(X5,X6)|X5=X6))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f104,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~organization(X0,sk11)|~organization(sk2,X1)|~organization(X0,X1)|~class(X0,sk5,sk11)|~survival_chance(sk2,X2,sk11)|~survival_chance(X0,X2,sk11)|~reorganization(sk2,sk11,X1)|~reorganization(X0,sk11,X3)|~reorganization_type(sk2,X4,sk11)|~reorganization_type(X0,X4,sk11)|~survival_chance(sk2,X5,X1)|~survival_chance(X0,X6,X1)|~complexity(sk2,X7,sk11)|~complexity(X0,X8,sk11)|~greater(X8,X7)|greater(X5,X6)|X5=X6|~sQ5_spl)),
% 0.13/0.54 inference(component_clause,[status(thm)],[f103])).
% 0.13/0.54 fof(f106,plain,(
% 0.13/0.54 ~sQ0_spl|sQ5_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f98,f78,f103])).
% 0.13/0.54 fof(f107,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~organization(X0,sk11)|~organization(sk2,X1)|~organization(X0,X1)|~class(X0,sk5,sk11)|~survival_chance(X0,sk6,sk11)|~reorganization(sk2,sk11,X1)|~reorganization(X0,sk11,X2)|~reorganization_type(sk2,X3,sk11)|~reorganization_type(X0,X3,sk11)|~survival_chance(sk2,X4,X1)|~survival_chance(X0,X5,X1)|~complexity(sk2,X6,sk11)|~complexity(X0,X7,sk11)|~greater(X7,X6)|greater(X4,X5)|X4=X5|~sQ5_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f104,f53])).
% 0.13/0.54 fof(f109,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6]: (~organization(X0,sk11)|~organization(sk2,sk12)|~organization(X0,sk12)|~class(X0,sk5,sk11)|~survival_chance(X0,sk6,sk11)|~reorganization(X0,sk11,X1)|~reorganization_type(sk2,X2,sk11)|~reorganization_type(X0,X2,sk11)|~survival_chance(sk2,X3,sk12)|~survival_chance(X0,X4,sk12)|~complexity(sk2,X5,sk11)|~complexity(X0,X6,sk11)|~greater(X6,X5)|greater(X3,X4)|X3=X4|~sQ5_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f55,f107])).
% 0.13/0.54 fof(f111,plain,(
% 0.13/0.54 greater(sk12,sk11)),
% 0.13/0.54 inference(resolution,[status(thm)],[f55,f38])).
% 0.13/0.54 fof(f112,definition,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6]: (sQ6_spl <=> (~organization(X0,sk11)|~organization(X0,sk12)|~class(X0,sk5,sk11)|~survival_chance(X0,sk6,sk11)|~reorganization(X0,sk11,X1)|~reorganization_type(sk2,X2,sk11)|~reorganization_type(X0,X2,sk11)|~survival_chance(sk2,X3,sk12)|~survival_chance(X0,X4,sk12)|~complexity(sk2,X5,sk11)|~complexity(X0,X6,sk11)|~greater(X6,X5)|greater(X3,X4)|X3=X4))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f113,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4,X5,X6]: (~organization(X0,sk11)|~organization(X0,sk12)|~class(X0,sk5,sk11)|~survival_chance(X0,sk6,sk11)|~reorganization(X0,sk11,X1)|~reorganization_type(sk2,X2,sk11)|~reorganization_type(X0,X2,sk11)|~survival_chance(sk2,X3,sk12)|~survival_chance(X0,X4,sk12)|~complexity(sk2,X5,sk11)|~complexity(X0,X6,sk11)|~greater(X6,X5)|greater(X3,X4)|X3=X4|~sQ6_spl)),
% 0.13/0.54 inference(component_clause,[status(thm)],[f112])).
% 0.13/0.54 fof(f115,definition,(
% 0.13/0.54 sQ7_spl <=> (organization(sk2,sk12))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f116,plain,(
% 0.13/0.54 organization(sk2,sk12)|~sQ7_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f115])).
% 0.13/0.54 fof(f118,plain,(
% 0.13/0.54 sQ6_spl|~sQ7_spl|~sQ5_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f109,f112,f115,f103])).
% 0.13/0.54 fof(f128,definition,(
% 0.13/0.54 sQ10_spl <=> (greater(sk11,sk12))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f129,plain,(
% 0.13/0.54 greater(sk11,sk12)|~sQ10_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f128])).
% 0.13/0.54 fof(f155,plain,(
% 0.13/0.54 ![X0,X1,X2,X3]: (~organization(sk3,X0)|~organization(sk3,X1)|~survival_chance(sk3,X2,X0)|~survival_chance(sk3,X3,X1)|greater(sk11,X0)|~greater(X1,X0)|greater(X1,sk13)|greater(X2,X3))),
% 0.13/0.54 inference(resolution,[status(thm)],[f56,f42])).
% 0.13/0.54 fof(f160,definition,(
% 0.13/0.54 sQ18_spl <=> (organization(sk3,sk13))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f162,plain,(
% 0.13/0.54 ~organization(sk3,sk13)|sQ18_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f160])).
% 0.13/0.54 fof(f180,definition,(
% 0.13/0.54 sQ21_spl <=> (class(sk3,sk5,sk11))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f182,plain,(
% 0.13/0.54 ~class(sk3,sk5,sk11)|sQ21_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f180])).
% 0.13/0.54 fof(f183,definition,(
% 0.13/0.54 sQ22_spl <=> (survival_chance(sk3,sk6,sk11))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f185,plain,(
% 0.13/0.54 ~survival_chance(sk3,sk6,sk11)|sQ22_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f183])).
% 0.13/0.54 fof(f196,definition,(
% 0.13/0.54 sQ26_spl <=> (organization(sk2,sk13))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f198,plain,(
% 0.13/0.54 ~organization(sk2,sk13)|sQ26_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f196])).
% 0.13/0.54 fof(f199,definition,(
% 0.13/0.54 ![X0]: (sQ27_spl <=> (~reorganization_type(sk3,X0,sk11)|~reorganization_type(sk2,X0,sk11)))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f200,plain,(
% 0.13/0.54 ![X0]: (~reorganization_type(sk3,X0,sk11)|~reorganization_type(sk2,X0,sk11)|~sQ27_spl)),
% 0.13/0.54 inference(component_clause,[status(thm)],[f199])).
% 0.13/0.54 fof(f209,plain,(
% 0.13/0.54 $false|sQ18_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f162,f50])).
% 0.13/0.54 fof(f210,plain,(
% 0.13/0.54 sQ18_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f209])).
% 0.13/0.54 fof(f215,plain,(
% 0.13/0.54 $false|sQ26_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f198,f49])).
% 0.13/0.54 fof(f216,plain,(
% 0.13/0.54 sQ26_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f215])).
% 0.13/0.54 fof(f222,plain,(
% 0.13/0.54 ~greater(sk11,sk12)),
% 0.13/0.54 inference(resolution,[status(thm)],[f111,f31])).
% 0.13/0.54 fof(f223,plain,(
% 0.13/0.54 $false|~sQ10_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f222,f129])).
% 0.13/0.54 fof(f224,plain,(
% 0.13/0.54 ~sQ10_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f223])).
% 0.13/0.54 fof(f225,plain,(
% 0.13/0.54 ![X0,X1]: (~organization(sk2,sk12)|~organization(sk2,sk13)|~survival_chance(sk2,X0,sk12)|~survival_chance(sk2,X1,sk13)|~greater(sk13,sk12)|greater(X1,X0))),
% 0.13/0.54 inference(resolution,[status(thm)],[f59,f40])).
% 0.13/0.54 fof(f226,definition,(
% 0.13/0.54 ![X0,X1]: (sQ30_spl <=> (~survival_chance(sk2,X0,sk12)|~survival_chance(sk2,X1,sk13)|greater(X1,X0)))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f227,plain,(
% 0.13/0.54 ![X0,X1]: (~survival_chance(sk2,X0,sk12)|~survival_chance(sk2,X1,sk13)|greater(X1,X0)|~sQ30_spl)),
% 0.13/0.54 inference(component_clause,[status(thm)],[f226])).
% 0.13/0.54 fof(f229,definition,(
% 0.13/0.54 sQ31_spl <=> (greater(sk13,sk12))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f232,plain,(
% 0.13/0.54 ~sQ7_spl|~sQ26_spl|sQ30_spl|~sQ31_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f225,f115,f196,f226,f229])).
% 0.13/0.54 fof(f250,definition,(
% 0.13/0.54 sQ35_spl <=> (greater(sk13,sk13))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f251,plain,(
% 0.13/0.54 greater(sk13,sk13)|~sQ35_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f250])).
% 0.13/0.54 fof(f294,plain,(
% 0.13/0.54 ![X0]: (~greater(X0,sk11)|~greater(sk13,X0)|organization(sk3,X0))),
% 0.13/0.54 inference(resolution,[status(thm)],[f68,f50])).
% 0.13/0.54 fof(f298,plain,(
% 0.13/0.54 ![X0]: (~greater(X0,sk11)|~greater(sk13,X0)|organization(sk2,X0))),
% 0.13/0.54 inference(resolution,[status(thm)],[f70,f49])).
% 0.13/0.54 fof(f349,plain,(
% 0.13/0.54 $false|sQ21_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f182,f52])).
% 0.13/0.54 fof(f350,plain,(
% 0.13/0.54 sQ21_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f349])).
% 0.13/0.54 fof(f448,plain,(
% 0.13/0.54 $false|~sQ35_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f251,f66])).
% 0.13/0.54 fof(f449,plain,(
% 0.13/0.54 ~sQ35_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f448])).
% 0.13/0.54 fof(f559,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4]: (~organization(X0,sk11)|~organization(X0,X1)|~class(X0,sk5,sk11)|~reorganization(X0,sk11,X1)|~reorganization_type(sk2,X2,sk11)|~reorganization_type(X0,X2,sk11)|~complexity(sk2,X3,sk11)|~complexity(X0,X4,sk11)|~greater(X4,X3)|greater(X1,sk12)|~sQ1_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f82,f55])).
% 0.13/0.54 fof(f572,plain,(
% 0.13/0.54 ~greater(sk13,sk12)|organization(sk3,sk12)),
% 0.13/0.54 inference(resolution,[status(thm)],[f294,f111])).
% 0.13/0.54 fof(f574,definition,(
% 0.13/0.54 sQ75_spl <=> (organization(sk3,sk12))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f575,plain,(
% 0.13/0.54 organization(sk3,sk12)|~sQ75_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f574])).
% 0.13/0.54 fof(f577,plain,(
% 0.13/0.54 ~sQ31_spl|sQ75_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f572,f229,f574])).
% 0.13/0.54 fof(f579,plain,(
% 0.13/0.54 ~greater(sk13,sk12)|organization(sk2,sk12)),
% 0.13/0.54 inference(resolution,[status(thm)],[f298,f111])).
% 0.13/0.54 fof(f581,plain,(
% 0.13/0.54 ~sQ31_spl|sQ7_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f579,f229,f115])).
% 0.13/0.54 fof(f594,plain,(
% 0.13/0.54 ![X0,X1,X2,X3,X4]: (~organization(sk3,sk11)|~organization(sk3,sk12)|~class(sk3,sk5,sk11)|~survival_chance(sk3,sk6,sk11)|~reorganization_type(sk2,X0,sk11)|~reorganization_type(sk3,X0,sk11)|~survival_chance(sk2,X1,sk12)|~survival_chance(sk3,X2,sk12)|~complexity(sk2,X3,sk11)|~complexity(sk3,X4,sk11)|~greater(X4,X3)|greater(X1,X2)|X1=X2|~sQ6_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f113,f56])).
% 0.13/0.54 fof(f596,definition,(
% 0.13/0.54 ![X1,X2]: (sQ77_spl <=> (~survival_chance(sk2,X1,sk12)|~survival_chance(sk3,X2,sk12)|greater(X1,X2)|X1=X2))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f597,plain,(
% 0.13/0.54 ![X0,X1]: (~survival_chance(sk2,X0,sk12)|~survival_chance(sk3,X1,sk12)|greater(X0,X1)|X0=X1|~sQ77_spl)),
% 0.13/0.54 inference(component_clause,[status(thm)],[f596])).
% 0.13/0.54 fof(f599,definition,(
% 0.13/0.54 ![X3,X4]: (sQ78_spl <=> (~complexity(sk2,X3,sk11)|~complexity(sk3,X4,sk11)|~greater(X4,X3)))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f600,plain,(
% 0.13/0.54 ![X0,X1]: (~complexity(sk2,X0,sk11)|~complexity(sk3,X1,sk11)|~greater(X1,X0)|~sQ78_spl)),
% 0.13/0.54 inference(component_clause,[status(thm)],[f599])).
% 0.13/0.54 fof(f602,plain,(
% 0.13/0.54 ~sQ2_spl|~sQ75_spl|~sQ21_spl|~sQ22_spl|sQ27_spl|sQ77_spl|sQ78_spl|~sQ6_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f594,f88,f574,f180,f183,f199,f596,f599,f112])).
% 0.13/0.54 fof(f606,plain,(
% 0.13/0.54 ![X0,X1,X2]: (~organization(sk3,sk11)|~organization(sk3,sk13)|~class(sk3,sk5,sk11)|~reorganization_type(sk2,X0,sk11)|~reorganization_type(sk3,X0,sk11)|~complexity(sk2,X1,sk11)|~complexity(sk3,X2,sk11)|~greater(X2,X1)|greater(sk13,sk12)|~sQ1_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f559,f56])).
% 0.13/0.54 fof(f611,plain,(
% 0.13/0.54 ~sQ2_spl|~sQ18_spl|~sQ21_spl|sQ27_spl|sQ78_spl|sQ31_spl|~sQ1_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f606,f88,f160,f180,f199,f599,f229,f81])).
% 0.13/0.54 fof(f620,plain,(
% 0.13/0.54 survival_chance(sk3,sk1(sk12,sk3),sk12)|~sQ75_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f575,f34])).
% 0.13/0.54 fof(f624,plain,(
% 0.13/0.54 survival_chance(sk2,sk1(sk12,sk2),sk12)|~sQ7_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f116,f34])).
% 0.13/0.54 fof(f645,plain,(
% 0.13/0.54 ![X0,X1]: (~organization(sk3,sk12)|~organization(sk3,X0)|~survival_chance(sk3,X1,X0)|greater(sk11,sk12)|~greater(X0,sk12)|greater(X0,sk13)|greater(sk1(sk12,sk3),X1)|~sQ75_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f620,f155])).
% 0.13/0.54 fof(f657,definition,(
% 0.13/0.54 ![X0,X1]: (sQ83_spl <=> (~organization(sk3,X0)|~survival_chance(sk3,X1,X0)|~greater(X0,sk12)|greater(X0,sk13)|greater(sk1(sk12,sk3),X1)))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f658,plain,(
% 0.13/0.54 ![X0,X1]: (~organization(sk3,X0)|~survival_chance(sk3,X1,X0)|~greater(X0,sk12)|greater(X0,sk13)|greater(sk1(sk12,sk3),X1)|~sQ83_spl)),
% 0.13/0.54 inference(component_clause,[status(thm)],[f657])).
% 0.13/0.54 fof(f660,plain,(
% 0.13/0.54 ~sQ75_spl|sQ83_spl|sQ10_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f645,f574,f657,f128])).
% 0.13/0.54 fof(f667,plain,(
% 0.13/0.54 ~organization(sk3,sk13)|~greater(sk13,sk12)|greater(sk13,sk13)|greater(sk1(sk12,sk3),sk8)|~sQ83_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f658,f61])).
% 0.13/0.54 fof(f677,definition,(
% 0.13/0.54 sQ86_spl <=> (greater(sk1(sk12,sk3),sk8))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f678,plain,(
% 0.13/0.54 greater(sk1(sk12,sk3),sk8)|~sQ86_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f677])).
% 0.13/0.54 fof(f680,plain,(
% 0.13/0.54 ~sQ18_spl|~sQ31_spl|sQ35_spl|sQ86_spl|~sQ83_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f667,f160,f229,f250,f677,f657])).
% 0.13/0.54 fof(f689,plain,(
% 0.13/0.54 ~reorganization_type(sk2,sk4,sk11)|~sQ27_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f200,f58])).
% 0.13/0.54 fof(f690,plain,(
% 0.13/0.54 $false|~sQ27_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f689,f57])).
% 0.13/0.54 fof(f691,plain,(
% 0.13/0.54 ~sQ27_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f690])).
% 0.13/0.54 fof(f705,plain,(
% 0.13/0.54 ![X0]: (~survival_chance(sk2,X0,sk13)|greater(X0,sk1(sk12,sk2))|~sQ7_spl|~sQ30_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f624,f227])).
% 0.13/0.54 fof(f745,plain,(
% 0.13/0.54 ![X0]: (~complexity(sk3,X0,sk11)|~greater(X0,sk9)|~sQ78_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f600,f62])).
% 0.13/0.54 fof(f759,plain,(
% 0.13/0.54 ~greater(sk10,sk9)|~sQ78_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f745,f63])).
% 0.13/0.54 fof(f760,plain,(
% 0.13/0.54 $false|~sQ78_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f759,f64])).
% 0.13/0.54 fof(f761,plain,(
% 0.13/0.54 ~sQ78_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f760])).
% 0.13/0.54 fof(f762,plain,(
% 0.13/0.54 $false|sQ22_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f185,f54])).
% 0.13/0.54 fof(f763,plain,(
% 0.13/0.54 sQ22_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f762])).
% 0.13/0.54 fof(f764,plain,(
% 0.13/0.54 ![X0]: (~survival_chance(sk3,X0,sk12)|greater(sk1(sk12,sk2),X0)|sk1(sk12,sk2)=X0|~sQ77_spl|~sQ7_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f597,f624])).
% 0.13/0.54 fof(f765,plain,(
% 0.13/0.54 greater(sk1(sk12,sk2),sk1(sk12,sk3))|sk1(sk12,sk2)=sk1(sk12,sk3)|~sQ77_spl|~sQ7_spl|~sQ75_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f764,f620])).
% 0.13/0.54 fof(f766,definition,(
% 0.13/0.54 sQ95_spl <=> (greater(sk1(sk12,sk2),sk1(sk12,sk3)))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f767,plain,(
% 0.13/0.54 greater(sk1(sk12,sk2),sk1(sk12,sk3))|~sQ95_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f766])).
% 0.13/0.54 fof(f769,definition,(
% 0.13/0.54 sQ96_spl <=> (sk1(sk12,sk2)=sk1(sk12,sk3))),
% 0.13/0.54 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.13/0.54 fof(f770,plain,(
% 0.13/0.54 sk1(sk12,sk2)=sk1(sk12,sk3)|~sQ96_spl),
% 0.13/0.54 inference(component_clause,[status(thm)],[f769])).
% 0.13/0.54 fof(f772,plain,(
% 0.13/0.54 sQ95_spl|sQ96_spl|~sQ77_spl|~sQ7_spl|~sQ75_spl),
% 0.13/0.54 inference(split_clause,[status(thm)],[f765,f766,f769,f596,f115,f574])).
% 0.13/0.54 fof(f777,plain,(
% 0.13/0.54 greater(sk7,sk1(sk12,sk2))|~sQ7_spl|~sQ30_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f705,f60])).
% 0.13/0.54 fof(f786,plain,(
% 0.13/0.54 ![X0]: (~greater(sk1(sk12,sk3),X0)|greater(sk1(sk12,sk2),X0)|~sQ95_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f767,f33])).
% 0.13/0.54 fof(f792,plain,(
% 0.13/0.54 ![X0]: (~greater(sk1(sk12,sk2),X0)|greater(sk7,X0)|~sQ7_spl|~sQ30_spl)),
% 0.13/0.54 inference(resolution,[status(thm)],[f777,f33])).
% 0.13/0.54 fof(f796,plain,(
% 0.13/0.54 greater(sk1(sk12,sk2),sk8)|~sQ95_spl|~sQ86_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f786,f678])).
% 0.13/0.54 fof(f815,plain,(
% 0.13/0.54 greater(sk1(sk12,sk2),sk8)|~sQ96_spl|~sQ86_spl),
% 0.13/0.54 inference(backward_demodulation,[status(thm)],[f770,f678])).
% 0.13/0.54 fof(f890,plain,(
% 0.13/0.54 greater(sk7,sk8)|~sQ95_spl|~sQ86_spl|~sQ7_spl|~sQ30_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f796,f792])).
% 0.13/0.54 fof(f896,plain,(
% 0.13/0.54 $false|~sQ95_spl|~sQ86_spl|~sQ7_spl|~sQ30_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f890,f65])).
% 0.13/0.54 fof(f897,plain,(
% 0.13/0.54 ~sQ95_spl|~sQ86_spl|~sQ7_spl|~sQ30_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f896])).
% 0.13/0.54 fof(f927,plain,(
% 0.13/0.54 greater(sk7,sk8)|~sQ96_spl|~sQ86_spl|~sQ7_spl|~sQ30_spl),
% 0.13/0.54 inference(resolution,[status(thm)],[f815,f792])).
% 0.13/0.54 fof(f933,plain,(
% 0.13/0.54 $false|~sQ96_spl|~sQ86_spl|~sQ7_spl|~sQ30_spl),
% 0.13/0.54 inference(forward_subsumption_resolution,[status(thm)],[f927,f65])).
% 0.13/0.54 fof(f934,plain,(
% 0.13/0.54 ~sQ96_spl|~sQ86_spl|~sQ7_spl|~sQ30_spl),
% 0.13/0.54 inference(contradiction_clause,[status(thm)],[f933])).
% 0.13/0.54 fof(f935,plain,(
% 0.13/0.54 $false),
% 0.13/0.54 inference(sat_refutation,[status(thm)],[f84,f86,f96,f106,f118,f210,f216,f224,f232,f350,f449,f577,f581,f602,f611,f660,f680,f691,f761,f763,f772,f897,f934])).
% 0.13/0.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.96/0.54 % Elapsed time: 0.184519 seconds
% 0.96/0.54 % CPU time: 1.202469 seconds
% 0.96/0.54 % Total memory used: 94.157 MB
% 0.96/0.54 % Net memory used: 92.141 MB
%------------------------------------------------------------------------------