%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : MGT005-2 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n001.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:12:17 PM UTC 2026
% Result : Unsatisfiable 3.12s 1.19s
% Output : CNFRefutation 3.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 24
% Syntax : Number of formulae : 99 ( 66 unt; 0 def)
% Number of atoms : 329 ( 12 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 467 ( 237 ~; 230 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 13 con; 0-0 aty)
% Number of variables : 144 ( 0 sgn 144 !; 0 ?; 116 :)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X2,X3,X0,X1] :
( organization(X0,X3)
| ~ greater(X2,X3)
| ~ greater(X3,X1)
| ~ organization(X0,X2)
| ~ organization(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp13_31) ).
fof(f7,axiom,
! [X2,X0,X1] :
( greater(X2,X1)
| ~ reorganization(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mp7_32) ).
fof(f10,axiom,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a10_FOL_35) ).
fof(f11,axiom,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a11_FOL_36) ).
fof(f17,negated_conjecture,
organization(sk5,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_42) ).
fof(f18,negated_conjecture,
organization(sk6,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_43) ).
fof(f19,negated_conjecture,
organization(sk5,sk17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_44) ).
fof(f20,negated_conjecture,
organization(sk6,sk17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_45) ).
fof(f21,negated_conjecture,
class(sk5,sk8,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_46) ).
fof(f22,negated_conjecture,
class(sk6,sk8,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_47) ).
fof(f23,negated_conjecture,
survival_chance(sk5,sk9,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_48) ).
fof(f24,negated_conjecture,
survival_chance(sk6,sk9,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_49) ).
fof(f25,negated_conjecture,
reorganization(sk5,sk15,sk16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_50) ).
fof(f26,negated_conjecture,
reorganization(sk6,sk15,sk17),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_51) ).
fof(f27,negated_conjecture,
reorganization_type(sk5,sk7,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_52) ).
fof(f28,negated_conjecture,
reorganization_type(sk6,sk7,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_53) ).
fof(f30,negated_conjecture,
survival_chance(sk5,sk10,sk14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_55) ).
fof(f31,negated_conjecture,
survival_chance(sk6,sk11,sk14),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_56) ).
fof(f32,negated_conjecture,
complexity(sk5,sk12,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_57) ).
fof(f33,negated_conjecture,
complexity(sk6,sk13,sk15),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_58) ).
fof(f34,negated_conjecture,
greater(sk13,sk12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_59) ).
fof(f37,negated_conjecture,
sk14 = sk16,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_61) ).
fof(f38,plain,
sk16 = sk14,
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
~ greater(sk10,sk11),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_62) ).
fof(f40,negated_conjecture,
sk10 != sk11,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_plus_FOL_63) ).
fof(f41,plain,
reorganization(sk5,sk15,sk14),
inference(definition_unfolding,[],[f25,f38]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( organization(X3,X1)
| ~ organization(X3,X2)
| ~ organization(X3,X0)
| ~ greater(X1,X2)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(X2,X1)
| ~ reorganization(X0,X1,X2) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( greater(X4,X2)
| ~ organization(X3,X4)
| ~ organization(X3,X1)
| ~ organization(X0,X1)
| ~ greater(X8,X7)
| ~ complexity(X3,X8,X1)
| ~ complexity(X0,X7,X1)
| ~ reorganization_type(X3,X6,X1)
| ~ reorganization_type(X0,X6,X1)
| ~ class(X3,X5,X1)
| ~ class(X0,X5,X1)
| ~ reorganization(X3,X1,X4)
| ~ reorganization(X0,X1,X2) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] :
( greater(X3,X6)
| ( X3 = X6 )
| ~ organization(X5,X4)
| ~ organization(X5,X2)
| ~ organization(X0,X4)
| ~ organization(X0,X2)
| ~ greater(X11,X10)
| ~ complexity(X5,X11,X2)
| ~ complexity(X0,X10,X2)
| ~ reorganization_type(X5,X9,X2)
| ~ reorganization_type(X0,X9,X2)
| ~ class(X5,X8,X2)
| ~ class(X0,X8,X2)
| ~ reorganization(X5,X2,X7)
| ~ reorganization(X0,X2,X4)
| ~ survival_chance(X5,X6,X4)
| ~ survival_chance(X5,X1,X2)
| ~ survival_chance(X0,X3,X4)
| ~ survival_chance(X0,X1,X2) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_103,negated_conjecture,
organization(sk5,sk15),
inference(cnf_transformation,[],[f17]) ).
tcf(c_104,negated_conjecture,
organization(sk6,sk15),
inference(cnf_transformation,[],[f18]) ).
tcf(c_105,negated_conjecture,
organization(sk5,sk17),
inference(cnf_transformation,[],[f19]) ).
tcf(c_106,negated_conjecture,
organization(sk6,sk17),
inference(cnf_transformation,[],[f20]) ).
tcf(c_107,negated_conjecture,
class(sk5,sk8,sk15),
inference(cnf_transformation,[],[f21]) ).
tcf(c_108,negated_conjecture,
class(sk6,sk8,sk15),
inference(cnf_transformation,[],[f22]) ).
tcf(c_109,negated_conjecture,
survival_chance(sk5,sk9,sk15),
inference(cnf_transformation,[],[f23]) ).
tcf(c_110,negated_conjecture,
survival_chance(sk6,sk9,sk15),
inference(cnf_transformation,[],[f24]) ).
tcf(c_111,negated_conjecture,
reorganization(sk5,sk15,sk14),
inference(cnf_transformation,[],[f41]) ).
tcf(c_112,negated_conjecture,
reorganization(sk6,sk15,sk17),
inference(cnf_transformation,[],[f26]) ).
tcf(c_113,negated_conjecture,
reorganization_type(sk5,sk7,sk15),
inference(cnf_transformation,[],[f27]) ).
tcf(c_114,negated_conjecture,
reorganization_type(sk6,sk7,sk15),
inference(cnf_transformation,[],[f28]) ).
tcf(c_116,negated_conjecture,
survival_chance(sk5,sk10,sk14),
inference(cnf_transformation,[],[f30]) ).
tcf(c_117,negated_conjecture,
survival_chance(sk6,sk11,sk14),
inference(cnf_transformation,[],[f31]) ).
tcf(c_118,negated_conjecture,
complexity(sk5,sk12,sk15),
inference(cnf_transformation,[],[f32]) ).
tcf(c_119,negated_conjecture,
complexity(sk6,sk13,sk15),
inference(cnf_transformation,[],[f33]) ).
tcf(c_120,negated_conjecture,
greater(sk13,sk12),
inference(cnf_transformation,[],[f34]) ).
tcf(c_122,negated_conjecture,
~ greater(sk10,sk11),
inference(cnf_transformation,[],[f39]) ).
tcf(c_123,negated_conjecture,
sk10 != sk11,
inference(cnf_transformation,[],[f40]) ).
tcf(c_1114,negated_conjecture,
reorganization(sk5,sk15,sk14),
inference(demodulation,[status(thm)],[c_111]) ).
tcf(c_1115,negated_conjecture,
sk10 != sk11,
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_1116,negated_conjecture,
~ greater(sk10,sk11),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_1117,negated_conjecture,
greater(sk13,sk12),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_1118,negated_conjecture,
complexity(sk6,sk13,sk15),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_1119,negated_conjecture,
complexity(sk5,sk12,sk15),
inference(demodulation,[status(thm)],[c_118]) ).
tcf(c_1120,negated_conjecture,
survival_chance(sk6,sk11,sk14),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_1121,negated_conjecture,
survival_chance(sk5,sk10,sk14),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_1122,negated_conjecture,
reorganization_type(sk6,sk7,sk15),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_1123,negated_conjecture,
reorganization_type(sk5,sk7,sk15),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_1124,negated_conjecture,
reorganization(sk6,sk15,sk17),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_1125,negated_conjecture,
survival_chance(sk6,sk9,sk15),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_1126,negated_conjecture,
survival_chance(sk5,sk9,sk15),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_1127,negated_conjecture,
class(sk6,sk8,sk15),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_1128,negated_conjecture,
class(sk5,sk8,sk15),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_1129,negated_conjecture,
organization(sk6,sk17),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_1130,negated_conjecture,
organization(sk5,sk17),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_1131,negated_conjecture,
organization(sk6,sk15),
inference(demodulation,[status(thm)],[c_104]) ).
tcf(c_1132,negated_conjecture,
organization(sk5,sk15),
inference(demodulation,[status(thm)],[c_103]) ).
tcf(c_1849,plain,
greater(sk14,sk15),
inference(superposition,[status(thm)],[c_1114,c_93]) ).
tcf(c_2798,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( greater(X1,sk14)
| ~ organization(sk5,sk15)
| ~ organization(X0,sk15)
| ~ organization(X0,X1)
| ~ greater(X4,X5)
| ~ complexity(sk5,X5,sk15)
| ~ reorganization_type(sk5,X3,sk15)
| ~ class(sk5,X2,sk15)
| ~ complexity(X0,X4,sk15)
| ~ reorganization_type(X0,X3,sk15)
| ~ class(X0,X2,sk15)
| ~ reorganization(X0,sk15,X1) ),
inference(superposition,[status(thm)],[c_1114,c_96]) ).
tcf(c_2799,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( greater(X1,sk14)
| ~ organization(X0,sk15)
| ~ organization(X0,X1)
| ~ greater(X4,X5)
| ~ complexity(sk5,X5,sk15)
| ~ reorganization_type(sk5,X3,sk15)
| ~ class(sk5,X2,sk15)
| ~ complexity(X0,X4,sk15)
| ~ reorganization_type(X0,X3,sk15)
| ~ class(X0,X2,sk15)
| ~ reorganization(X0,sk15,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2798,c_1132]) ).
tcf(c_2864,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( greater(X3,X1)
| ( X1 = X3 )
| ~ organization(sk5,sk15)
| ~ organization(sk5,X2)
| ~ organization(X0,sk15)
| ~ organization(X0,X2)
| ~ greater(X7,X8)
| ~ complexity(sk5,X8,sk15)
| ~ reorganization_type(sk5,X6,sk15)
| ~ class(sk5,X5,sk15)
| ~ reorganization(sk5,sk15,X2)
| ~ survival_chance(X0,sk9,sk15)
| ~ complexity(X0,X7,sk15)
| ~ reorganization_type(X0,X6,sk15)
| ~ class(X0,X5,sk15)
| ~ reorganization(X0,sk15,X4)
| ~ survival_chance(sk5,X3,X2)
| ~ survival_chance(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_1126,c_97]) ).
tcf(c_2922,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( greater(X3,X1)
| ( X1 = X3 )
| ~ organization(sk5,X2)
| ~ organization(X0,sk15)
| ~ organization(X0,X2)
| ~ greater(X7,X8)
| ~ complexity(sk5,X8,sk15)
| ~ reorganization_type(sk5,X6,sk15)
| ~ class(sk5,X5,sk15)
| ~ reorganization(sk5,sk15,X2)
| ~ survival_chance(X0,sk9,sk15)
| ~ complexity(X0,X7,sk15)
| ~ reorganization_type(X0,X6,sk15)
| ~ class(X0,X5,sk15)
| ~ reorganization(X0,sk15,X4)
| ~ survival_chance(sk5,X3,X2)
| ~ survival_chance(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2864,c_1132]) ).
tcf(c_3596,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( greater(sk17,sk14)
| ~ organization(sk6,sk17)
| ~ organization(sk6,sk15)
| ~ greater(X3,X2)
| ~ complexity(sk6,X3,sk15)
| ~ complexity(sk5,X2,sk15)
| ~ reorganization_type(sk6,X1,sk15)
| ~ reorganization_type(sk5,X1,sk15)
| ~ class(sk6,X0,sk15)
| ~ class(sk5,X0,sk15) ),
inference(superposition,[status(thm)],[c_1124,c_2799]) ).
tcf(c_3605,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( greater(sk17,sk14)
| ~ greater(X3,X2)
| ~ complexity(sk6,X3,sk15)
| ~ complexity(sk5,X2,sk15)
| ~ reorganization_type(sk6,X1,sk15)
| ~ reorganization_type(sk5,X1,sk15)
| ~ class(sk6,X0,sk15)
| ~ class(sk5,X0,sk15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3596,c_1129,c_1131]) ).
tcf(c_3692,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(sk17,sk14)
| ~ greater(X2,X1)
| ~ class(sk5,sk8,sk15)
| ~ complexity(sk6,X2,sk15)
| ~ complexity(sk5,X1,sk15)
| ~ reorganization_type(sk6,X0,sk15)
| ~ reorganization_type(sk5,X0,sk15) ),
inference(superposition,[status(thm)],[c_1127,c_3605]) ).
tcf(c_3693,plain,
! [X0: $i,X1: $i,X2: $i] :
( greater(sk17,sk14)
| ~ greater(X2,X1)
| ~ complexity(sk6,X2,sk15)
| ~ complexity(sk5,X1,sk15)
| ~ reorganization_type(sk6,X0,sk15)
| ~ reorganization_type(sk5,X0,sk15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3692,c_1128]) ).
tcf(c_3924,plain,
! [X0: $i,X1: $i] :
( greater(sk17,sk14)
| ~ greater(sk13,X1)
| ~ complexity(sk5,X1,sk15)
| ~ reorganization_type(sk6,X0,sk15)
| ~ reorganization_type(sk5,X0,sk15) ),
inference(superposition,[status(thm)],[c_1118,c_3693]) ).
tcf(c_3941,plain,
! [X0: $i] :
( greater(sk17,sk14)
| ~ greater(sk13,X0)
| ~ reorganization_type(sk6,sk7,sk15)
| ~ complexity(sk5,X0,sk15) ),
inference(superposition,[status(thm)],[c_1123,c_3924]) ).
tcf(c_3942,plain,
! [X0: $i] :
( greater(sk17,sk14)
| ~ greater(sk13,X0)
| ~ complexity(sk5,X0,sk15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3941,c_1122]) ).
tcf(c_3956,plain,
( greater(sk17,sk14)
| ~ greater(sk13,sk12) ),
inference(superposition,[status(thm)],[c_1119,c_3942]) ).
tcf(c_3957,plain,
greater(sk17,sk14),
inference(forward_subsumption_resolution,[status(thm)],[c_3956,c_1117]) ).
tcf(c_3961,plain,
! [X0: $i,X1: $i] :
( organization(X0,sk14)
| ~ organization(X0,sk17)
| ~ greater(sk14,X1)
| ~ organization(X0,X1) ),
inference(superposition,[status(thm)],[c_3957,c_92]) ).
tcf(c_4517,plain,
( organization(sk5,sk14)
| ~ organization(sk5,sk17)
| ~ greater(sk14,sk15) ),
inference(superposition,[status(thm)],[c_1132,c_3961]) ).
tcf(c_4518,plain,
( organization(sk6,sk14)
| ~ organization(sk6,sk17)
| ~ greater(sk14,sk15) ),
inference(superposition,[status(thm)],[c_1131,c_3961]) ).
tcf(c_4521,plain,
organization(sk6,sk14),
inference(forward_subsumption_resolution,[status(thm)],[c_4518,c_1129,c_1849]) ).
tcf(c_4522,plain,
organization(sk5,sk14),
inference(forward_subsumption_resolution,[status(thm)],[c_4517,c_1130,c_1849]) ).
tcf(c_4911,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( greater(X0,sk11)
| ( X0 = sk11 )
| ~ organization(sk6,sk14)
| ~ organization(sk6,sk15)
| ~ organization(sk5,sk14)
| ~ greater(X5,X4)
| ~ reorganization(sk5,sk15,sk14)
| ~ survival_chance(sk6,sk9,sk15)
| ~ complexity(sk6,X5,sk15)
| ~ complexity(sk5,X4,sk15)
| ~ reorganization_type(sk6,X3,sk15)
| ~ reorganization_type(sk5,X3,sk15)
| ~ class(sk6,X2,sk15)
| ~ class(sk5,X2,sk15)
| ~ reorganization(sk6,sk15,X1)
| ~ survival_chance(sk5,X0,sk14) ),
inference(superposition,[status(thm)],[c_1120,c_2922]) ).
tcf(c_4946,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( greater(X0,sk11)
| ( X0 = sk11 )
| ~ greater(X5,X4)
| ~ complexity(sk6,X5,sk15)
| ~ complexity(sk5,X4,sk15)
| ~ reorganization_type(sk6,X3,sk15)
| ~ reorganization_type(sk5,X3,sk15)
| ~ class(sk6,X2,sk15)
| ~ class(sk5,X2,sk15)
| ~ reorganization(sk6,sk15,X1)
| ~ survival_chance(sk5,X0,sk14) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4911,c_4521,c_1131,c_4522,c_1114,c_1125]) ).
tcf(c_5202,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( greater(sk10,sk11)
| ( sk10 = sk11 )
| ~ greater(X4,X3)
| ~ complexity(sk6,X4,sk15)
| ~ complexity(sk5,X3,sk15)
| ~ reorganization_type(sk6,X2,sk15)
| ~ reorganization_type(sk5,X2,sk15)
| ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(superposition,[status(thm)],[c_1121,c_4946]) ).
tcf(c_5203,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ~ greater(X4,X3)
| ~ complexity(sk6,X4,sk15)
| ~ complexity(sk5,X3,sk15)
| ~ reorganization_type(sk6,X2,sk15)
| ~ reorganization_type(sk5,X2,sk15)
| ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5202,c_1116,c_1115]) ).
tcf(c_5236,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ greater(sk13,X3)
| ~ complexity(sk5,X3,sk15)
| ~ reorganization_type(sk6,X2,sk15)
| ~ reorganization_type(sk5,X2,sk15)
| ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(superposition,[status(thm)],[c_1118,c_5203]) ).
tcf(c_5259,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ greater(sk13,sk12)
| ~ reorganization_type(sk6,X2,sk15)
| ~ reorganization_type(sk5,X2,sk15)
| ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(superposition,[status(thm)],[c_1119,c_5236]) ).
tcf(c_5260,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ reorganization_type(sk6,X2,sk15)
| ~ reorganization_type(sk5,X2,sk15)
| ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5259,c_1117]) ).
tcf(c_5277,plain,
! [X0: $i,X1: $i] :
( ~ reorganization_type(sk6,sk7,sk15)
| ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(superposition,[status(thm)],[c_1123,c_5260]) ).
tcf(c_5278,plain,
! [X0: $i,X1: $i] :
( ~ class(sk6,X1,sk15)
| ~ class(sk5,X1,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5277,c_1122]) ).
tcf(c_5289,plain,
! [X0: $i] :
( ~ class(sk6,sk8,sk15)
| ~ reorganization(sk6,sk15,X0) ),
inference(superposition,[status(thm)],[c_1128,c_5278]) ).
tcf(c_5290,plain,
! [X0: $i] : ~ reorganization(sk6,sk15,X0),
inference(forward_subsumption_resolution,[status(thm)],[c_5289,c_1127]) ).
tcf(c_5291,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_1124,c_5290]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT005-2 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 01:02:36 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 3.12/1.19 % SZS status Started for theBenchmark.p
% 3.12/1.19 % SZS status Unsatisfiable for theBenchmark.p
% 3.12/1.19
% 3.12/1.19 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.12/1.19
% 3.12/1.19 % ------ iProver source info
% 3.12/1.19
% 3.12/1.19 % git: date: 2026-07-19 20:42:38 +0200
% 3.12/1.19 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.12/1.19 % git: non_committed_changes: false
% 3.12/1.19
% 3.12/1.19 % ------ Parsing...% successful
% 3.12/1.19
% 3.12/1.19
% 3.12/1.19 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.12/1.19
% 3.12/1.19 % ------ Preprocessing... sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe:1:0s pe_e sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe_e %
% 3.12/1.19
% 3.12/1.19 % ------ Preprocessing... gs_s sp: 2 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.12/1.19
% 3.12/1.19 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 3.12/1.19 % ------ Proving...
% 3.12/1.19 % ------ Problem Properties
% 3.12/1.19
% 3.12/1.19 %
% 3.12/1.19 % clauses 38
% 3.12/1.19 % conjectures 20
% 3.12/1.19 % EPR 32
% 3.12/1.19 % Horn 35
% 3.12/1.19 % unary 21
% 3.12/1.19 % binary 3
% 3.12/1.19 % lits 130
% 3.12/1.19 % lits eq 5
% 3.12/1.19 % fd_pure 0
% 3.12/1.19 % fd_pseudo 0
% 3.12/1.19 % fd_cond 0
% 3.12/1.19 % fd_pseudo_cond 1
% 3.12/1.19 % AC symbols 0
% 3.12/1.19
% 3.12/1.19 % ------ Schedule dynamic 5 is on
% 3.12/1.19
% 3.12/1.19 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 3.12/1.19
% 3.12/1.19
% 3.12/1.19 % ------
% 3.12/1.19 % Current options:
% 3.12/1.19 % ------
% 3.12/1.19
% 3.12/1.19
% 3.12/1.19 %
% 3.12/1.19
% 3.12/1.19 % ------ Proving...
% 3.12/1.19 %
% 3.12/1.19
% 3.12/1.19 % SZS status Unsatisfiable for theBenchmark.p
% 3.12/1.19
% 3.12/1.19 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.12/1.20
% 3.12/1.20
%------------------------------------------------------------------------------