%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : MGT010-1 : TPTP v3.4.2. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1003MB
% OS : Linux 2.6.17-1.2142_FC4
% CPULimit : 600s
% DateTime : Wed May 6 13:59:51 EDT 2009
% Result : Unsatisfiable 5.9s
% Output : Refutation 5.9s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 18
% Syntax : Number of formulae : 50 ( 30 unt; 0 def)
% Number of atoms : 161 ( 0 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 226 ( 115 ~; 111 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-2 aty)
% Number of variables : 109 ( 17 sgn 31 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(t10_FOL_10,plain,
class(sk2,sk4,sk11),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163263688,plain,
class(sk2,sk4,sk11),
inference(rewrite,[status(thm)],[t10_FOL_10]),
[] ).
fof(t10_FOL_6,plain,
organization(sk2,sk11),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163120048,plain,
organization(sk2,sk11),
inference(rewrite,[status(thm)],[t10_FOL_6]),
[] ).
fof(t10_FOL_16,plain,
size(sk2,sk9,sk11),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163299568,plain,
size(sk2,sk9,sk11),
inference(rewrite,[status(thm)],[t10_FOL_16]),
[] ).
fof(t10_FOL_17,plain,
size(sk3,sk10,sk12),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163304016,plain,
size(sk3,sk10,sk12),
inference(rewrite,[status(thm)],[t10_FOL_17]),
[] ).
fof(t10_FOL_7,plain,
organization(sk3,sk12),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163245688,plain,
organization(sk3,sk12),
inference(rewrite,[status(thm)],[t10_FOL_7]),
[] ).
fof(t10_FOL_9,plain,
reorganization_free(sk3,sk12,sk12),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163258968,plain,
reorganization_free(sk3,sk12,sk12),
inference(rewrite,[status(thm)],[t10_FOL_9]),
[] ).
fof(t9_FOL_5,plain,
! [A,B,C,D,E,F,G,H,I] :
( ~ organization(A,B)
| ~ organization(C,D)
| ~ reorganization_free(A,B,B)
| ~ reorganization_free(C,D,D)
| ~ class(A,E,B)
| ~ class(C,E,D)
| ~ reproducibility(A,F,B)
| ~ reproducibility(C,G,D)
| ~ size(A,H,B)
| ~ size(C,I,D)
| ~ greater(I,H)
| greater(G,F) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163232312,plain,
( ~ organization(A,B)
| ~ organization(C,D)
| ~ reorganization_free(A,B,B)
| ~ reorganization_free(C,D,D)
| ~ class(A,E,B)
| ~ class(C,E,D)
| ~ reproducibility(A,F,B)
| ~ reproducibility(C,G,D)
| ~ size(A,H,B)
| ~ size(C,I,D)
| ~ greater(I,H)
| greater(G,F) ),
inference(rewrite,[status(thm)],[t9_FOL_5]),
[] ).
fof(t10_FOL_11,plain,
class(sk3,sk4,sk12),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163268200,plain,
class(sk3,sk4,sk12),
inference(rewrite,[status(thm)],[t10_FOL_11]),
[] ).
cnf(206869680,plain,
( ~ organization(A,B)
| ~ reorganization_free(A,B,B)
| ~ class(A,sk4,B)
| ~ reproducibility(A,C,B)
| ~ reproducibility(sk3,D,sk12)
| ~ size(A,E,B)
| ~ size(sk3,F,sk12)
| ~ greater(F,E)
| greater(D,C) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[163245688,163258968,163232312,163268200]),
[] ).
fof(t10_FOL_18,plain,
greater(sk10,sk9),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163308752,plain,
greater(sk10,sk9),
inference(rewrite,[status(thm)],[t10_FOL_18]),
[] ).
cnf(206883328,plain,
( ~ organization(A,B)
| ~ reorganization_free(A,B,B)
| ~ class(A,sk4,B)
| ~ reproducibility(A,C,B)
| ~ reproducibility(sk3,D,sk12)
| ~ size(A,sk9,B)
| greater(D,C) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[163304016,206869680,163308752]),
[] ).
fof(t10_FOL_8,plain,
reorganization_free(sk2,sk11,sk11),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163250472,plain,
reorganization_free(sk2,sk11,sk11),
inference(rewrite,[status(thm)],[t10_FOL_8]),
[] ).
cnf(206895952,plain,
( ~ reproducibility(sk2,A,sk11)
| ~ reproducibility(sk3,B,sk12)
| greater(B,A) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[163263688,163120048,163299568,206883328,163250472]),
[] ).
fof(a2_FOL_3,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( ~ organization(A,B)
| ~ organization(C,D)
| ~ reliability(A,E,B)
| ~ reliability(C,F,D)
| ~ accountability(A,G,B)
| ~ accountability(C,H,D)
| ~ reproducibility(A,I,B)
| ~ reproducibility(C,J,D)
| ~ greater(J,I)
| greater(H,G) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163190528,plain,
( ~ organization(A,B)
| ~ organization(C,D)
| ~ reliability(A,E,B)
| ~ reliability(C,F,D)
| ~ accountability(A,G,B)
| ~ accountability(C,H,D)
| ~ reproducibility(A,I,B)
| ~ reproducibility(C,J,D)
| ~ greater(J,I)
| greater(H,G) ),
inference(rewrite,[status(thm)],[a2_FOL_3]),
[] ).
fof(t10_FOL_15,plain,
accountability(sk3,sk8,sk12),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163119376,plain,
accountability(sk3,sk8,sk12),
inference(rewrite,[status(thm)],[t10_FOL_15]),
[] ).
cnf(207485736,plain,
( ~ organization(A,B)
| ~ reliability(A,C,B)
| ~ reliability(sk3,D,sk12)
| ~ accountability(A,E,B)
| ~ reproducibility(A,F,B)
| ~ reproducibility(sk3,G,sk12)
| ~ greater(G,F)
| greater(sk8,E) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[163245688,163190528,163119376]),
[] ).
fof(t10_FOL_13,plain,
reliability(sk3,sk6,sk12),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163281408,plain,
reliability(sk3,sk6,sk12),
inference(rewrite,[status(thm)],[t10_FOL_13]),
[] ).
cnf(218116216,plain,
( ~ organization(A,B)
| ~ reliability(A,C,B)
| ~ accountability(A,D,B)
| ~ reproducibility(A,E,B)
| ~ reproducibility(sk3,F,sk12)
| ~ greater(F,E)
| greater(sk8,D) ),
inference(resolution,[status(thm)],[207485736,163281408]),
[] ).
fof(t10_FOL_14,plain,
accountability(sk2,sk7,sk11),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163286160,plain,
accountability(sk2,sk7,sk11),
inference(rewrite,[status(thm)],[t10_FOL_14]),
[] ).
cnf(218216816,plain,
( ~ reliability(sk2,A,sk11)
| ~ reproducibility(sk2,B,sk11)
| ~ reproducibility(sk3,C,sk12)
| greater(sk8,sk7) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[206895952,163120048,218116216,163286160]),
[] ).
fof(t10_FOL_12,plain,
reliability(sk2,sk5,sk11),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163277008,plain,
reliability(sk2,sk5,sk11),
inference(rewrite,[status(thm)],[t10_FOL_12]),
[] ).
fof(a2_FOL_2,plain,
! [A,B,C,D,E,F,G,H,I,J] :
( ~ organization(A,B)
| ~ organization(C,D)
| ~ reliability(A,E,B)
| ~ reliability(C,F,D)
| ~ accountability(A,G,B)
| ~ accountability(C,H,D)
| ~ reproducibility(A,I,B)
| ~ reproducibility(C,J,D)
| ~ greater(J,I)
| greater(F,E) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163180568,plain,
( ~ organization(A,B)
| ~ organization(C,D)
| ~ reliability(A,E,B)
| ~ reliability(C,F,D)
| ~ accountability(A,G,B)
| ~ accountability(C,H,D)
| ~ reproducibility(A,I,B)
| ~ reproducibility(C,J,D)
| ~ greater(J,I)
| greater(F,E) ),
inference(rewrite,[status(thm)],[a2_FOL_2]),
[] ).
cnf(207423792,plain,
( ~ organization(A,B)
| ~ reliability(A,C,B)
| ~ reliability(sk3,D,sk12)
| ~ accountability(A,E,B)
| ~ reproducibility(A,F,B)
| ~ reproducibility(sk3,G,sk12)
| ~ greater(G,F)
| greater(D,C) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[163245688,163180568,163119376]),
[] ).
cnf(218088048,plain,
( ~ organization(A,B)
| ~ reliability(A,C,B)
| ~ accountability(A,D,B)
| ~ reproducibility(A,E,B)
| ~ reproducibility(sk3,F,sk12)
| ~ greater(F,E)
| greater(sk6,C) ),
inference(resolution,[status(thm)],[207423792,163281408]),
[] ).
cnf(218163896,plain,
( ~ reliability(sk2,A,sk11)
| ~ reproducibility(sk2,B,sk11)
| ~ reproducibility(sk3,C,sk12)
| greater(sk6,A) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[206895952,163120048,218088048,163286160]),
[] ).
fof(t10_FOL_19,plain,
( ~ greater(sk6,sk5)
| ~ greater(sk8,sk7) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163319784,plain,
( ~ greater(sk6,sk5)
| ~ greater(sk8,sk7) ),
inference(rewrite,[status(thm)],[t10_FOL_19]),
[] ).
cnf(223173440,plain,
( ~ reproducibility(sk2,A,sk11)
| ~ reproducibility(sk3,B,sk12) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[218216816,163277008,218163896,163319784]),
[] ).
fof(mp3_1,plain,
! [A,B] :
( ~ organization(A,B)
| reproducibility(A,sk1(B,A),B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),
[] ).
cnf(163125776,plain,
( ~ organization(A,B)
| reproducibility(A,sk1(B,A),B) ),
inference(rewrite,[status(thm)],[mp3_1]),
[] ).
cnf(205690080,plain,
reproducibility(sk2,sk1(sk11,sk2),sk11),
inference(resolution,[status(thm)],[163125776,163120048]),
[] ).
cnf(225595512,plain,
~ reproducibility(sk3,A,sk12),
inference(resolution,[status(thm)],[223173440,205690080]),
[] ).
cnf(205899792,plain,
reproducibility(sk3,sk1(sk12,sk3),sk12),
inference(resolution,[status(thm)],[163125776,163245688]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[225595512,205899792]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 6 seconds
% START OF PROOF SEQUENCE
% fof(t10_FOL_10,plain,(class(sk2,sk4,sk11)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163263688,plain,(class(sk2,sk4,sk11)),inference(rewrite,[status(thm)],[t10_FOL_10]),[]).
%
% fof(t10_FOL_6,plain,(organization(sk2,sk11)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163120048,plain,(organization(sk2,sk11)),inference(rewrite,[status(thm)],[t10_FOL_6]),[]).
%
% fof(t10_FOL_16,plain,(size(sk2,sk9,sk11)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163299568,plain,(size(sk2,sk9,sk11)),inference(rewrite,[status(thm)],[t10_FOL_16]),[]).
%
% fof(t10_FOL_17,plain,(size(sk3,sk10,sk12)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163304016,plain,(size(sk3,sk10,sk12)),inference(rewrite,[status(thm)],[t10_FOL_17]),[]).
%
% fof(t10_FOL_7,plain,(organization(sk3,sk12)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163245688,plain,(organization(sk3,sk12)),inference(rewrite,[status(thm)],[t10_FOL_7]),[]).
%
% fof(t10_FOL_9,plain,(reorganization_free(sk3,sk12,sk12)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163258968,plain,(reorganization_free(sk3,sk12,sk12)),inference(rewrite,[status(thm)],[t10_FOL_9]),[]).
%
% fof(t9_FOL_5,plain,(~organization(A,B)|~organization(C,D)|~reorganization_free(A,B,B)|~reorganization_free(C,D,D)|~class(A,E,B)|~class(C,E,D)|~reproducibility(A,F,B)|~reproducibility(C,G,D)|~size(A,H,B)|~size(C,I,D)|~greater(I,H)|greater(G,F)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163232312,plain,(~organization(A,B)|~organization(C,D)|~reorganization_free(A,B,B)|~reorganization_free(C,D,D)|~class(A,E,B)|~class(C,E,D)|~reproducibility(A,F,B)|~reproducibility(C,G,D)|~size(A,H,B)|~size(C,I,D)|~greater(I,H)|greater(G,F)),inference(rewrite,[status(thm)],[t9_FOL_5]),[]).
%
% fof(t10_FOL_11,plain,(class(sk3,sk4,sk12)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163268200,plain,(class(sk3,sk4,sk12)),inference(rewrite,[status(thm)],[t10_FOL_11]),[]).
%
% cnf(206869680,plain,(~organization(A,B)|~reorganization_free(A,B,B)|~class(A,sk4,B)|~reproducibility(A,C,B)|~reproducibility(sk3,D,sk12)|~size(A,E,B)|~size(sk3,F,sk12)|~greater(F,E)|greater(D,C)),inference(forward_subsumption_resolution__resolution,[status(thm)],[163245688,163258968,163232312,163268200]),[]).
%
% fof(t10_FOL_18,plain,(greater(sk10,sk9)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163308752,plain,(greater(sk10,sk9)),inference(rewrite,[status(thm)],[t10_FOL_18]),[]).
%
% cnf(206883328,plain,(~organization(A,B)|~reorganization_free(A,B,B)|~class(A,sk4,B)|~reproducibility(A,C,B)|~reproducibility(sk3,D,sk12)|~size(A,sk9,B)|greater(D,C)),inference(forward_subsumption_resolution__resolution,[status(thm)],[163304016,206869680,163308752]),[]).
%
% fof(t10_FOL_8,plain,(reorganization_free(sk2,sk11,sk11)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163250472,plain,(reorganization_free(sk2,sk11,sk11)),inference(rewrite,[status(thm)],[t10_FOL_8]),[]).
%
% cnf(206895952,plain,(~reproducibility(sk2,A,sk11)|~reproducibility(sk3,B,sk12)|greater(B,A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[163263688,163120048,163299568,206883328,163250472]),[]).
%
% fof(a2_FOL_3,plain,(~organization(A,B)|~organization(C,D)|~reliability(A,E,B)|~reliability(C,F,D)|~accountability(A,G,B)|~accountability(C,H,D)|~reproducibility(A,I,B)|~reproducibility(C,J,D)|~greater(J,I)|greater(H,G)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163190528,plain,(~organization(A,B)|~organization(C,D)|~reliability(A,E,B)|~reliability(C,F,D)|~accountability(A,G,B)|~accountability(C,H,D)|~reproducibility(A,I,B)|~reproducibility(C,J,D)|~greater(J,I)|greater(H,G)),inference(rewrite,[status(thm)],[a2_FOL_3]),[]).
%
% fof(t10_FOL_15,plain,(accountability(sk3,sk8,sk12)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163119376,plain,(accountability(sk3,sk8,sk12)),inference(rewrite,[status(thm)],[t10_FOL_15]),[]).
%
% cnf(207485736,plain,(~organization(A,B)|~reliability(A,C,B)|~reliability(sk3,D,sk12)|~accountability(A,E,B)|~reproducibility(A,F,B)|~reproducibility(sk3,G,sk12)|~greater(G,F)|greater(sk8,E)),inference(forward_subsumption_resolution__resolution,[status(thm)],[163245688,163190528,163119376]),[]).
%
% fof(t10_FOL_13,plain,(reliability(sk3,sk6,sk12)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163281408,plain,(reliability(sk3,sk6,sk12)),inference(rewrite,[status(thm)],[t10_FOL_13]),[]).
%
% cnf(218116216,plain,(~organization(A,B)|~reliability(A,C,B)|~accountability(A,D,B)|~reproducibility(A,E,B)|~reproducibility(sk3,F,sk12)|~greater(F,E)|greater(sk8,D)),inference(resolution,[status(thm)],[207485736,163281408]),[]).
%
% fof(t10_FOL_14,plain,(accountability(sk2,sk7,sk11)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163286160,plain,(accountability(sk2,sk7,sk11)),inference(rewrite,[status(thm)],[t10_FOL_14]),[]).
%
% cnf(218216816,plain,(~reliability(sk2,A,sk11)|~reproducibility(sk2,B,sk11)|~reproducibility(sk3,C,sk12)|greater(sk8,sk7)),inference(forward_subsumption_resolution__resolution,[status(thm)],[206895952,163120048,218116216,163286160]),[]).
%
% fof(t10_FOL_12,plain,(reliability(sk2,sk5,sk11)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163277008,plain,(reliability(sk2,sk5,sk11)),inference(rewrite,[status(thm)],[t10_FOL_12]),[]).
%
% fof(a2_FOL_2,plain,(~organization(A,B)|~organization(C,D)|~reliability(A,E,B)|~reliability(C,F,D)|~accountability(A,G,B)|~accountability(C,H,D)|~reproducibility(A,I,B)|~reproducibility(C,J,D)|~greater(J,I)|greater(F,E)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163180568,plain,(~organization(A,B)|~organization(C,D)|~reliability(A,E,B)|~reliability(C,F,D)|~accountability(A,G,B)|~accountability(C,H,D)|~reproducibility(A,I,B)|~reproducibility(C,J,D)|~greater(J,I)|greater(F,E)),inference(rewrite,[status(thm)],[a2_FOL_2]),[]).
%
% cnf(207423792,plain,(~organization(A,B)|~reliability(A,C,B)|~reliability(sk3,D,sk12)|~accountability(A,E,B)|~reproducibility(A,F,B)|~reproducibility(sk3,G,sk12)|~greater(G,F)|greater(D,C)),inference(forward_subsumption_resolution__resolution,[status(thm)],[163245688,163180568,163119376]),[]).
%
% cnf(218088048,plain,(~organization(A,B)|~reliability(A,C,B)|~accountability(A,D,B)|~reproducibility(A,E,B)|~reproducibility(sk3,F,sk12)|~greater(F,E)|greater(sk6,C)),inference(resolution,[status(thm)],[207423792,163281408]),[]).
%
% cnf(218163896,plain,(~reliability(sk2,A,sk11)|~reproducibility(sk2,B,sk11)|~reproducibility(sk3,C,sk12)|greater(sk6,A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[206895952,163120048,218088048,163286160]),[]).
%
% fof(t10_FOL_19,plain,(~greater(sk6,sk5)|~greater(sk8,sk7)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163319784,plain,(~greater(sk6,sk5)|~greater(sk8,sk7)),inference(rewrite,[status(thm)],[t10_FOL_19]),[]).
%
% cnf(223173440,plain,(~reproducibility(sk2,A,sk11)|~reproducibility(sk3,B,sk12)),inference(forward_subsumption_resolution__resolution,[status(thm)],[218216816,163277008,218163896,163319784]),[]).
%
% fof(mp3_1,plain,(~organization(A,B)|reproducibility(A,sk1(B,A),B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/MGT/MGT010-1.tptp',unknown),[]).
%
% cnf(163125776,plain,(~organization(A,B)|reproducibility(A,sk1(B,A),B)),inference(rewrite,[status(thm)],[mp3_1]),[]).
%
% cnf(205690080,plain,(reproducibility(sk2,sk1(sk11,sk2),sk11)),inference(resolution,[status(thm)],[163125776,163120048]),[]).
%
% cnf(225595512,plain,(~reproducibility(sk3,A,sk12)),inference(resolution,[status(thm)],[223173440,205690080]),[]).
%
% cnf(205899792,plain,(reproducibility(sk3,sk1(sk12,sk3),sk12)),inference(resolution,[status(thm)],[163125776,163245688]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[225595512,205899792]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------